Theory Domain_SF_cpo

           (*-------------------------------------------*
            |                CPO-Prover                 |
            |               December 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory Domain_SF_cpo = Domain_SF + Domain_T_cpo + Domain_F_cpo + CPO_pair:

(*****************************************************************

         1. 
         2. 
         3. 
         4. 

 *****************************************************************)

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite UnionT and InterT.                 *)
(*                  Union (B ` A) = (UN x:A. B x)                      *)
(*                  Inter (B ` A) = (INT x:A. B x)                     *)

declare Union_image_eq [simp del]
declare Inter_image_eq [simp del]

(*********************************************************
                      Bottom in Dom_SF
 *********************************************************)

instance domSF :: (type) bot0
by (intro_classes)

defs (overloaded)
  bottomSF_def : "Bot == ({[]t}t ,, {}f)"

lemma bottomSF: "Bot <= (SF::'a domSF)"
apply (simp add: bottomSF_def pairSF_def)
apply (simp add: subsetSF_def Abs_domSF_inverse)
done

instance domSF :: (type) bot
apply (intro_classes)
by (simp add: bottomSF)

(********************************************************** 
      lemmas used in a proof that domain_SF is a cpo.
 **********************************************************)

(* LUB_TF TFs is an upper bound of TFs *)

consts
  LUB_TF :: "'a domTF set => 'a domTF"
  LUB_SF :: "'a domSF set => 'a domSF"

defs
  LUB_TF_def : "LUB_TF TFs == (UnionT (fst ` TFs), UnionF (snd ` TFs))"
  LUB_SF_def : "LUB_SF SFs == Abs_domSF (LUB_TF (Rep_domSF ` SFs))"

(************* LUB_TF *************)

(*** LUB_TF --> LUB ***)

lemma LUB_TF_isLUB:
  "TFs ~= {} ==> LUB_TF TFs isLUB TFs"
apply (simp add: pair_LUB_decompo)
apply (simp add: LUB_TF_def)
apply (simp add: isLUB_UnionT isLUB_UnionF)
done

(*** LUB --> LUB_TF ***)

lemma isLUB_LUB_TF_only_if:
  "[| TFs ~= {} ; TF isLUB TFs |] ==> TF = LUB_TF TFs"
apply (insert LUB_TF_isLUB[of TFs])
by (simp add: LUB_unique)

(* iff *)

lemma isLUB_LUB_TF : "TFs ~= {} ==> TF isLUB TFs = (TF = LUB_TF TFs)"
apply (rule iffI)
apply (simp add: isLUB_LUB_TF_only_if)
apply (simp add: LUB_TF_isLUB)
done

(*** LUB TF = LUB_TF ***)

lemma LUB_LUB_TF:
  "TFs ~= {} ==> LUB TFs = LUB_TF TFs"
by (simp add: isLUB_LUB LUB_TF_isLUB)

(****** LUB_TF TFs in domSF ******)

(* T3_F4 *)

lemma LUB_TF_in_T3_F4: 
  "[| TFs ~= {} ; ALL TF:TFs. TF:domSF |] ==> HC_T3_F4 (LUB_TF TFs)"
apply (simp add: LUB_TF_def HC_T3_F4_def)
apply (intro allI impI)

apply (simp add: memT_UnionT)
apply (simp add: memF_UnionF)
apply (elim bexE conjE)
apply (drule_tac x="x" in bspec, simp)

apply (simp add: domSF_iff HC_T3_F4_def)
by (auto)

(* F3 *)

lemma LUB_TF_in_F3: 
  "[| TFs ~= {} ; ALL TF:TFs. TF:domSF |] ==> HC_F3 (LUB_TF TFs)"
apply (simp add: LUB_TF_def HC_F3_def)
apply (intro allI impI)

apply (simp add: memT_UnionT)
apply (simp add: memF_UnionF)
apply (elim bexE conjE)
apply (drule_tac x="x" in bspec, simp)

apply (simp add: domSF_def HC_F3_def)
apply (elim conjE)
apply (drule_tac x="s" in spec)
apply (drule_tac x="X" in spec)
apply (drule_tac x="Y" in spec)
by (auto)

(* T2 *)

lemma LUB_TF_in_T2: 
  "[| TFs ~= {} ; ALL TF:TFs. TF:domSF |] ==> HC_T2 (LUB_TF TFs)"
apply (simp add: LUB_TF_def HC_T2_def)
apply (intro allI impI)

apply (simp add: memT_UnionT)
apply (simp add: memF_UnionF)
apply (elim exE bexE)
apply (drule_tac x="x" in bspec, simp)

apply (simp add: domSF_def HC_T2_def)
apply (elim conjE)
apply (drule_tac x="s" in spec)
by (auto)

(*** LUB_TF TFs in domSF ***)

lemma LUB_TF_in: 
  "[| TFs ~= {} ; ALL TF:TFs. TF:domSF |] ==> (LUB_TF TFs): domSF"
apply (simp (no_asm) add: domSF_iff)
apply (simp add: LUB_TF_in_T2)
apply (simp add: LUB_TF_in_F3)
apply (simp add: LUB_TF_in_T3_F4)
done

(************* LUB_SF *************)

(* isLUB lemma *)

lemma TF_isLUB_SFs:
  "[| TF:domSF ; TF isLUB Rep_domSF ` SFs |] ==> Abs_domSF TF isLUB SFs"
apply (simp add: isUB_def isLUB_def)
apply (rule conjI)

(* ub *)
apply (intro allI impI)
apply (elim bexE conjE)
apply (drule_tac x="fst (Rep_domSF y)" in spec)
apply (drule_tac x="snd (Rep_domSF y)" in spec)
apply (simp add: subsetSF_def Abs_domSF_inverse)

(* lub *)
apply (intro allI impI)
apply (elim bexE conjE)
apply (rotate_tac -1)
apply (drule_tac x="fst (Rep_domSF y)" in spec)
apply (rotate_tac -1)
apply (drule_tac x="snd (Rep_domSF y)" in spec)
apply (simp)
apply (drule mp)
 apply (intro allI impI)
 apply (simp add: image_def)
 apply (elim bexE conjE)
 apply (drule_tac x="x" in spec)
 apply (simp)
 apply (simp add: subsetSF_def)
apply (simp add: subsetSF_def Abs_domSF_inverse)
done

(*** LUB_SF --> LUB ***)

lemma LUB_SF_isLUB:
  "SFs ~= {} ==> LUB_SF SFs isLUB SFs"
apply (simp add: LUB_SF_def)
apply (rule TF_isLUB_SFs)
apply (simp add: LUB_TF_in)
apply (simp add: LUB_TF_isLUB)
done

(*** LUB --> LUB_SF ***)

lemma isLUB_LUB_SF_only_if:
  "[| SFs ~= {} ; SF isLUB SFs |] ==> SF = LUB_SF SFs"
apply (insert LUB_SF_isLUB[of SFs])
by (simp add: LUB_unique)

(* iff *)

lemma isLUB_LUB_SF : "SFs ~= {} ==> SF isLUB SFs = (SF = LUB_SF SFs)"
apply (rule iffI)
apply (simp add: isLUB_LUB_SF_only_if)
apply (simp add: LUB_SF_isLUB)
done

(********************************************************** 
                ( domSF, <= ) is a CPO
 **********************************************************)

instance domSF :: (type) cpo
apply (intro_classes)
apply (simp add: hasLUB_def)
apply (rule_tac x="LUB_SF X" in exI)
by (simp add: directed_def LUB_SF_isLUB)

(********************************************************** 
             ( domSF, <= ) is a pointed CPO
 **********************************************************)

instance domSF :: (type) cpo_bot
by (intro_classes)

(********************************************************** 
                 continuity of Abs_domSF
 **********************************************************)

(*** Abs_domSF ***)

lemma continuous_Abs_domSF:
 "[| ALL x. f x: domSF ; continuous f |] ==> continuous (Abs_domSF o f)"
apply (simp add: continuous_iff)
apply (intro allI impI)
apply (drule_tac x="X" in spec, simp)
apply (elim conjE exE)
apply (rule_tac x="x" in exI, simp)
apply (rule TF_isLUB_SFs)
apply (simp)

apply (subgoal_tac "Rep_domSF ` (Abs_domSF o f) ` X = f ` X")
by (auto simp add: image_def Abs_domSF_inverse)

(*** Rep_domSF ***)

lemma cont_Rep_domSF: "continuous Rep_domSF"
apply (simp add: continuous_iff)
apply (intro allI impI)
apply (rule_tac x="LUB_SF X" in exI)

apply (simp add: directed_def LUB_SF_isLUB)
apply (simp add: isLUB_LUB_TF)
apply (simp add: LUB_SF_def)
apply (simp add: LUB_TF_in Abs_domSF_inverse)
done

(****************** to add them again ******************)

declare Union_image_eq [simp]
declare Inter_image_eq [simp]

end