Theory Domain_F_cpo

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

theory Domain_F_cpo = Domain_F + CPO:

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

         1. Domain_F is a pointed cpo.
         2. 
         3. 
         4. 

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

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite UnionF and InterF.                 *)
(*                  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]

(*  The following simplification is sometimes unexpected.              *)
(*                                                                     *)
(*             not_None_eq: (x ~= None) = (EX y. x = Some y)           *)

declare not_None_eq [simp del]

(*********************************************************
                      Bottom in Dom_F
 *********************************************************)

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

defs (overloaded)
  bottomF_def   :  "Bot == {}f"

lemma bottomF : "ALL (F::'a domF). Bot <= F"
by (simp add: bottomF_def)

instance domF :: (type) bot
apply (intro_classes)
by (simp add: bottomF)

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

(* UnionF Fs is an upper bound of Fs *)

lemma UnionF_isUB : "(UnionF Fs) isUB Fs"
apply (simp add: isUB_def)
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (subgoal_tac "Fs ~= {}")
apply (simp add: memF_UnionF)
apply (rule_tac x=y in bexI)
by (auto)

(* UnionF Fs is the least upper bound of Fs *)

lemma UnionF_isLUB : "UnionF Fs isLUB Fs"
apply (simp add: isLUB_def UnionF_isUB)
apply (simp add: isUB_def)
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: memF_UnionF)
apply (erule bexE)
apply (drule_tac x="F" in spec)
by (simp)

(* the least upper bound of Fs is UnionF Fs *)

lemma isLUB_UnionF_only_if: "F isLUB Fs ==> F = UnionF Fs"
apply (insert UnionF_isLUB[of Fs])
apply (rule LUB_unique)
by (simp_all)

(* iff *)

lemma isLUB_UnionF : "(F isLUB Fs) = (F = UnionF Fs)"
apply (rule iffI)
apply (simp add: isLUB_UnionF_only_if)
apply (simp add: UnionF_isLUB)
done

(* LUB is UnionF Fs *)

lemma LUB_UnionF : "LUB Fs = UnionF Fs"
by (simp add: isLUB_LUB UnionF_isLUB)

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

instance domF :: (type) cpo
apply (intro_classes)
apply (simp add: hasLUB_def)
apply (rule_tac x="UnionF X" in exI)
apply (simp add: directed_def UnionF_isLUB)
done

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

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

(***********************************************************
                          lemmas
 ***********************************************************)

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

declare Union_image_eq [simp]
declare Inter_image_eq [simp]
declare not_None_eq    [simp]

end