Up to index of Isabelle/HOL/HOL-Complex/CSP-Prover
theory Domain_F_cpo = 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
lemma bottomF:
∀F. Bot ≤ F
lemma UnionF_isUB:
UnionF Fs isUB Fs
lemma UnionF_isLUB:
UnionF Fs isLUB Fs
lemma isLUB_UnionF_only_if:
F isLUB Fs ==> F = UnionF Fs
lemma isLUB_UnionF:
F isLUB Fs = (F = UnionF Fs)
lemma LUB_UnionF:
LUB Fs = UnionF Fs