# HG changeset patch # User huffman # Date 1214495645 -7200 # Node ID 5794a0e3e26ce8b49793e45c15675894fe299272 # Parent 29a09358953f961563a0fa5d3cb40c8992f6fab7 remove cset theory; define ideal completions using typedef instead of cpodef diff -r 29a09358953f -r 5794a0e3e26c src/HOLCF/CompactBasis.thy --- a/src/HOLCF/CompactBasis.thy Thu Jun 26 15:06:30 2008 +0200 +++ b/src/HOLCF/CompactBasis.thy Thu Jun 26 17:54:05 2008 +0200 @@ -6,7 +6,7 @@ header {* Compact bases of domains *} theory CompactBasis -imports Bifinite Cset +imports Bifinite begin subsection {* Ideals over a preorder *} @@ -78,16 +78,6 @@ apply (simp add: f) done -lemma adm_ideal: "adm (\A. ideal (Rep_cset A))" -unfolding ideal_def by (intro adm_lemmas adm_set_lemmas) - -lemma cpodef_ideal_lemma: - "(\x. x \ {S. ideal (Rep_cset S)}) \ adm (\x. x \ {S. ideal (Rep_cset S)})" -apply (simp add: adm_ideal) -apply (rule exI [where x="Abs_cset {x. x \ arbitrary}"]) -apply (simp add: ideal_principal) -done - lemma lub_image_principal: assumes f: "\x y. x \ y \ f x \ f y" shows "(\x\{x. x \ y}. f x) = f y" @@ -99,6 +89,72 @@ apply (simp add: r_refl) done +text {* The set of ideals is a cpo *} + +lemma ideal_UN: + fixes A :: "nat \ 'a set" + assumes ideal_A: "\i. ideal (A i)" + assumes chain_A: "\i j. i \ j \ A i \ A j" + shows "ideal (\i. A i)" + apply (rule idealI) + apply (cut_tac idealD1 [OF ideal_A], fast) + apply (clarify, rename_tac i j) + apply (drule subsetD [OF chain_A [OF le_maxI1]]) + apply (drule subsetD [OF chain_A [OF le_maxI2]]) + apply (drule (1) idealD2 [OF ideal_A]) + apply blast + apply clarify + apply (drule (1) idealD3 [OF ideal_A]) + apply fast +done + +lemma typedef_ideal_po: + fixes Abs :: "'a set \ 'b::sq_ord" + assumes type: "type_definition Rep Abs {S. ideal S}" + assumes less: "\x y. x \ y \ Rep x \ Rep y" + shows "OFCLASS('b, po_class)" + apply (intro_classes, unfold less) + apply (rule subset_refl) + apply (erule (1) subset_trans) + apply (rule type_definition.Rep_inject [OF type, THEN iffD1]) + apply (erule (1) subset_antisym) +done + +lemma + fixes Abs :: "'a set \ 'b::po" + assumes type: "type_definition Rep Abs {S. ideal S}" + assumes less: "\x y. x \ y \ Rep x \ Rep y" + assumes S: "chain S" + shows typedef_ideal_lub: "range S <<| Abs (\i. Rep (S i))" + and typedef_ideal_rep_contlub: "Rep (\i. S i) = (\i. Rep (S i))" +proof - + have 1: "ideal (\i. Rep (S i))" + apply (rule ideal_UN) + apply (rule type_definition.Rep [OF type, unfolded mem_Collect_eq]) + apply (subst less [symmetric]) + apply (erule chain_mono [OF S]) + done + hence 2: "Rep (Abs (\i. Rep (S i))) = (\i. Rep (S i))" + by (simp add: type_definition.Abs_inverse [OF type]) + show 3: "range S <<| Abs (\i. Rep (S i))" + apply (rule is_lubI) + apply (rule is_ubI) + apply (simp add: less 2, fast) + apply (simp add: less 2 is_ub_def, fast) + done + hence 4: "(\i. S i) = Abs (\i. Rep (S i))" + by (rule thelubI) + show 5: "Rep (\i. S i) = (\i. Rep (S i))" + by (simp add: 4 2) +qed + +lemma typedef_ideal_cpo: + fixes Abs :: "'a set \ 'b::po" + assumes type: "type_definition Rep Abs {S. ideal S}" + assumes less: "\x y. x \ y \ Rep x \ Rep y" + shows "OFCLASS('b, cpo_class)" +by (default, rule exI, erule typedef_ideal_lub [OF type less]) + end interpretation sq_le: preorder ["sq_le :: 'a::po \ 'a \ bool"] diff -r 29a09358953f -r 5794a0e3e26c src/HOLCF/ConvexPD.thy --- a/src/HOLCF/ConvexPD.thy Thu Jun 26 15:06:30 2008 +0200 +++ b/src/HOLCF/ConvexPD.thy Thu Jun 26 17:54:05 2008 +0200 @@ -141,25 +141,46 @@ subsection {* Type definition *} -cpodef (open) 'a convex_pd = - "{S::'a pd_basis cset. convex_le.ideal (Rep_cset S)}" -by (rule convex_le.cpodef_ideal_lemma) +typedef (open) 'a convex_pd = + "{S::'a pd_basis set. convex_le.ideal S}" +by (fast intro: convex_le.ideal_principal) + +instantiation convex_pd :: (profinite) sq_ord +begin + +definition + "x \ y \ Rep_convex_pd x \ Rep_convex_pd y" + +instance .. +end -lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_cset (Rep_convex_pd xs))" +instance convex_pd :: (profinite) po +by (rule convex_le.typedef_ideal_po + [OF type_definition_convex_pd sq_le_convex_pd_def]) + +instance convex_pd :: (profinite) cpo +by (rule convex_le.typedef_ideal_cpo + [OF type_definition_convex_pd sq_le_convex_pd_def]) + +lemma Rep_convex_pd_lub: + "chain Y \ Rep_convex_pd (\i. Y i) = (\i. Rep_convex_pd (Y i))" +by (rule convex_le.typedef_ideal_rep_contlub + [OF type_definition_convex_pd sq_le_convex_pd_def]) + +lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)" by (rule Rep_convex_pd [unfolded mem_Collect_eq]) definition convex_principal :: "'a pd_basis \ 'a convex_pd" where - "convex_principal t = Abs_convex_pd (Abs_cset {u. u \\ t})" + "convex_principal t = Abs_convex_pd {u. u \\ t}" lemma Rep_convex_principal: - "Rep_cset (Rep_convex_pd (convex_principal t)) = {u. u \\ t}" + "Rep_convex_pd (convex_principal t) = {u. u \\ t}" unfolding convex_principal_def by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal) interpretation convex_pd: - ideal_completion - [convex_le approx_pd convex_principal "\x. Rep_cset (Rep_convex_pd x)"] + ideal_completion [convex_le approx_pd convex_principal Rep_convex_pd] apply unfold_locales apply (rule approx_pd_convex_le) apply (rule approx_pd_idem) @@ -168,9 +189,9 @@ apply (rule finite_range_approx_pd) apply (rule approx_pd_covers) apply (rule ideal_Rep_convex_pd) -apply (simp add: cont2contlubE [OF cont_Rep_convex_pd] Rep_cset_lub) +apply (erule Rep_convex_pd_lub) apply (rule Rep_convex_principal) -apply (simp only: less_convex_pd_def sq_le_cset_def) +apply (simp only: sq_le_convex_pd_def) done text {* Convex powerdomain is pointed *} @@ -210,8 +231,7 @@ by (rule convex_pd.completion_approx_principal) lemma approx_eq_convex_principal: - "\t\Rep_cset (Rep_convex_pd xs). - approx n\xs = convex_principal (approx_pd n t)" + "\t\Rep_convex_pd xs. approx n\xs = convex_principal (approx_pd n t)" unfolding approx_convex_pd_def by (rule convex_pd.completion_approx_eq_principal) diff -r 29a09358953f -r 5794a0e3e26c src/HOLCF/LowerPD.thy --- a/src/HOLCF/LowerPD.thy Thu Jun 26 15:06:30 2008 +0200 +++ b/src/HOLCF/LowerPD.thy Thu Jun 26 17:54:05 2008 +0200 @@ -96,25 +96,46 @@ subsection {* Type definition *} -cpodef (open) 'a lower_pd = - "{S::'a pd_basis cset. lower_le.ideal (Rep_cset S)}" -by (rule lower_le.cpodef_ideal_lemma) +typedef (open) 'a lower_pd = + "{S::'a pd_basis set. lower_le.ideal S}" +by (fast intro: lower_le.ideal_principal) + +instantiation lower_pd :: (profinite) sq_ord +begin + +definition + "x \ y \ Rep_lower_pd x \ Rep_lower_pd y" + +instance .. +end -lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_cset (Rep_lower_pd xs))" +instance lower_pd :: (profinite) po +by (rule lower_le.typedef_ideal_po + [OF type_definition_lower_pd sq_le_lower_pd_def]) + +instance lower_pd :: (profinite) cpo +by (rule lower_le.typedef_ideal_cpo + [OF type_definition_lower_pd sq_le_lower_pd_def]) + +lemma Rep_lower_pd_lub: + "chain Y \ Rep_lower_pd (\i. Y i) = (\i. Rep_lower_pd (Y i))" +by (rule lower_le.typedef_ideal_rep_contlub + [OF type_definition_lower_pd sq_le_lower_pd_def]) + +lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd xs)" by (rule Rep_lower_pd [unfolded mem_Collect_eq]) definition lower_principal :: "'a pd_basis \ 'a lower_pd" where - "lower_principal t = Abs_lower_pd (Abs_cset {u. u \\ t})" + "lower_principal t = Abs_lower_pd {u. u \\ t}" lemma Rep_lower_principal: - "Rep_cset (Rep_lower_pd (lower_principal t)) = {u. u \\ t}" + "Rep_lower_pd (lower_principal t) = {u. u \\ t}" unfolding lower_principal_def by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal) interpretation lower_pd: - ideal_completion - [lower_le approx_pd lower_principal "\x. Rep_cset (Rep_lower_pd x)"] + ideal_completion [lower_le approx_pd lower_principal Rep_lower_pd] apply unfold_locales apply (rule approx_pd_lower_le) apply (rule approx_pd_idem) @@ -123,9 +144,9 @@ apply (rule finite_range_approx_pd) apply (rule approx_pd_covers) apply (rule ideal_Rep_lower_pd) -apply (simp add: cont2contlubE [OF cont_Rep_lower_pd] Rep_cset_lub) +apply (erule Rep_lower_pd_lub) apply (rule Rep_lower_principal) -apply (simp only: less_lower_pd_def sq_le_cset_def) +apply (simp only: sq_le_lower_pd_def) done text {* Lower powerdomain is pointed *} @@ -165,8 +186,7 @@ by (rule lower_pd.completion_approx_principal) lemma approx_eq_lower_principal: - "\t\Rep_cset (Rep_lower_pd xs). - approx n\xs = lower_principal (approx_pd n t)" + "\t\Rep_lower_pd xs. approx n\xs = lower_principal (approx_pd n t)" unfolding approx_lower_pd_def by (rule lower_pd.completion_approx_eq_principal) diff -r 29a09358953f -r 5794a0e3e26c src/HOLCF/UpperPD.thy --- a/src/HOLCF/UpperPD.thy Thu Jun 26 15:06:30 2008 +0200 +++ b/src/HOLCF/UpperPD.thy Thu Jun 26 17:54:05 2008 +0200 @@ -94,25 +94,46 @@ subsection {* Type definition *} -cpodef (open) 'a upper_pd = - "{S::'a pd_basis cset. upper_le.ideal (Rep_cset S)}" -by (rule upper_le.cpodef_ideal_lemma) +typedef (open) 'a upper_pd = + "{S::'a pd_basis set. upper_le.ideal S}" +by (fast intro: upper_le.ideal_principal) + +instantiation upper_pd :: (profinite) sq_ord +begin + +definition + "x \ y \ Rep_upper_pd x \ Rep_upper_pd y" + +instance .. +end -lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_cset (Rep_upper_pd xs))" +instance upper_pd :: (profinite) po +by (rule upper_le.typedef_ideal_po + [OF type_definition_upper_pd sq_le_upper_pd_def]) + +instance upper_pd :: (profinite) cpo +by (rule upper_le.typedef_ideal_cpo + [OF type_definition_upper_pd sq_le_upper_pd_def]) + +lemma Rep_upper_pd_lub: + "chain Y \ Rep_upper_pd (\i. Y i) = (\i. Rep_upper_pd (Y i))" +by (rule upper_le.typedef_ideal_rep_contlub + [OF type_definition_upper_pd sq_le_upper_pd_def]) + +lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd xs)" by (rule Rep_upper_pd [unfolded mem_Collect_eq]) definition upper_principal :: "'a pd_basis \ 'a upper_pd" where - "upper_principal t = Abs_upper_pd (Abs_cset {u. u \\ t})" + "upper_principal t = Abs_upper_pd {u. u \\ t}" lemma Rep_upper_principal: - "Rep_cset (Rep_upper_pd (upper_principal t)) = {u. u \\ t}" + "Rep_upper_pd (upper_principal t) = {u. u \\ t}" unfolding upper_principal_def by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal) interpretation upper_pd: - ideal_completion - [upper_le approx_pd upper_principal "\x. Rep_cset (Rep_upper_pd x)"] + ideal_completion [upper_le approx_pd upper_principal Rep_upper_pd] apply unfold_locales apply (rule approx_pd_upper_le) apply (rule approx_pd_idem) @@ -121,9 +142,9 @@ apply (rule finite_range_approx_pd) apply (rule approx_pd_covers) apply (rule ideal_Rep_upper_pd) -apply (simp add: cont2contlubE [OF cont_Rep_upper_pd] Rep_cset_lub) +apply (erule Rep_upper_pd_lub) apply (rule Rep_upper_principal) -apply (simp only: less_upper_pd_def sq_le_cset_def) +apply (simp only: sq_le_upper_pd_def) done text {* Upper powerdomain is pointed *} @@ -163,8 +184,7 @@ by (rule upper_pd.completion_approx_principal) lemma approx_eq_upper_principal: - "\t\Rep_cset (Rep_upper_pd xs). - approx n\xs = upper_principal (approx_pd n t)" + "\t\Rep_upper_pd xs. approx n\xs = upper_principal (approx_pd n t)" unfolding approx_upper_pd_def by (rule upper_pd.completion_approx_eq_principal)