1.1 --- a/src/HOLCF/CompactBasis.thy Thu Jun 26 15:06:30 2008 +0200
1.2 +++ b/src/HOLCF/CompactBasis.thy Thu Jun 26 17:54:05 2008 +0200
1.3 @@ -6,7 +6,7 @@
1.4 header {* Compact bases of domains *}
1.5
1.6 theory CompactBasis
1.7 -imports Bifinite Cset
1.8 +imports Bifinite
1.9 begin
1.10
1.11 subsection {* Ideals over a preorder *}
1.12 @@ -78,16 +78,6 @@
1.13 apply (simp add: f)
1.14 done
1.15
1.16 -lemma adm_ideal: "adm (\<lambda>A. ideal (Rep_cset A))"
1.17 -unfolding ideal_def by (intro adm_lemmas adm_set_lemmas)
1.18 -
1.19 -lemma cpodef_ideal_lemma:
1.20 - "(\<exists>x. x \<in> {S. ideal (Rep_cset S)}) \<and> adm (\<lambda>x. x \<in> {S. ideal (Rep_cset S)})"
1.21 -apply (simp add: adm_ideal)
1.22 -apply (rule exI [where x="Abs_cset {x. x \<preceq> arbitrary}"])
1.23 -apply (simp add: ideal_principal)
1.24 -done
1.25 -
1.26 lemma lub_image_principal:
1.27 assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
1.28 shows "(\<Squnion>x\<in>{x. x \<preceq> y}. f x) = f y"
1.29 @@ -99,6 +89,72 @@
1.30 apply (simp add: r_refl)
1.31 done
1.32
1.33 +text {* The set of ideals is a cpo *}
1.34 +
1.35 +lemma ideal_UN:
1.36 + fixes A :: "nat \<Rightarrow> 'a set"
1.37 + assumes ideal_A: "\<And>i. ideal (A i)"
1.38 + assumes chain_A: "\<And>i j. i \<le> j \<Longrightarrow> A i \<subseteq> A j"
1.39 + shows "ideal (\<Union>i. A i)"
1.40 + apply (rule idealI)
1.41 + apply (cut_tac idealD1 [OF ideal_A], fast)
1.42 + apply (clarify, rename_tac i j)
1.43 + apply (drule subsetD [OF chain_A [OF le_maxI1]])
1.44 + apply (drule subsetD [OF chain_A [OF le_maxI2]])
1.45 + apply (drule (1) idealD2 [OF ideal_A])
1.46 + apply blast
1.47 + apply clarify
1.48 + apply (drule (1) idealD3 [OF ideal_A])
1.49 + apply fast
1.50 +done
1.51 +
1.52 +lemma typedef_ideal_po:
1.53 + fixes Abs :: "'a set \<Rightarrow> 'b::sq_ord"
1.54 + assumes type: "type_definition Rep Abs {S. ideal S}"
1.55 + assumes less: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
1.56 + shows "OFCLASS('b, po_class)"
1.57 + apply (intro_classes, unfold less)
1.58 + apply (rule subset_refl)
1.59 + apply (erule (1) subset_trans)
1.60 + apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
1.61 + apply (erule (1) subset_antisym)
1.62 +done
1.63 +
1.64 +lemma
1.65 + fixes Abs :: "'a set \<Rightarrow> 'b::po"
1.66 + assumes type: "type_definition Rep Abs {S. ideal S}"
1.67 + assumes less: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
1.68 + assumes S: "chain S"
1.69 + shows typedef_ideal_lub: "range S <<| Abs (\<Union>i. Rep (S i))"
1.70 + and typedef_ideal_rep_contlub: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))"
1.71 +proof -
1.72 + have 1: "ideal (\<Union>i. Rep (S i))"
1.73 + apply (rule ideal_UN)
1.74 + apply (rule type_definition.Rep [OF type, unfolded mem_Collect_eq])
1.75 + apply (subst less [symmetric])
1.76 + apply (erule chain_mono [OF S])
1.77 + done
1.78 + hence 2: "Rep (Abs (\<Union>i. Rep (S i))) = (\<Union>i. Rep (S i))"
1.79 + by (simp add: type_definition.Abs_inverse [OF type])
1.80 + show 3: "range S <<| Abs (\<Union>i. Rep (S i))"
1.81 + apply (rule is_lubI)
1.82 + apply (rule is_ubI)
1.83 + apply (simp add: less 2, fast)
1.84 + apply (simp add: less 2 is_ub_def, fast)
1.85 + done
1.86 + hence 4: "(\<Squnion>i. S i) = Abs (\<Union>i. Rep (S i))"
1.87 + by (rule thelubI)
1.88 + show 5: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))"
1.89 + by (simp add: 4 2)
1.90 +qed
1.91 +
1.92 +lemma typedef_ideal_cpo:
1.93 + fixes Abs :: "'a set \<Rightarrow> 'b::po"
1.94 + assumes type: "type_definition Rep Abs {S. ideal S}"
1.95 + assumes less: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
1.96 + shows "OFCLASS('b, cpo_class)"
1.97 +by (default, rule exI, erule typedef_ideal_lub [OF type less])
1.98 +
1.99 end
1.100
1.101 interpretation sq_le: preorder ["sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"]
2.1 --- a/src/HOLCF/ConvexPD.thy Thu Jun 26 15:06:30 2008 +0200
2.2 +++ b/src/HOLCF/ConvexPD.thy Thu Jun 26 17:54:05 2008 +0200
2.3 @@ -141,25 +141,46 @@
2.4
2.5 subsection {* Type definition *}
2.6
2.7 -cpodef (open) 'a convex_pd =
2.8 - "{S::'a pd_basis cset. convex_le.ideal (Rep_cset S)}"
2.9 -by (rule convex_le.cpodef_ideal_lemma)
2.10 +typedef (open) 'a convex_pd =
2.11 + "{S::'a pd_basis set. convex_le.ideal S}"
2.12 +by (fast intro: convex_le.ideal_principal)
2.13
2.14 -lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_cset (Rep_convex_pd xs))"
2.15 +instantiation convex_pd :: (profinite) sq_ord
2.16 +begin
2.17 +
2.18 +definition
2.19 + "x \<sqsubseteq> y \<longleftrightarrow> Rep_convex_pd x \<subseteq> Rep_convex_pd y"
2.20 +
2.21 +instance ..
2.22 +end
2.23 +
2.24 +instance convex_pd :: (profinite) po
2.25 +by (rule convex_le.typedef_ideal_po
2.26 + [OF type_definition_convex_pd sq_le_convex_pd_def])
2.27 +
2.28 +instance convex_pd :: (profinite) cpo
2.29 +by (rule convex_le.typedef_ideal_cpo
2.30 + [OF type_definition_convex_pd sq_le_convex_pd_def])
2.31 +
2.32 +lemma Rep_convex_pd_lub:
2.33 + "chain Y \<Longrightarrow> Rep_convex_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_convex_pd (Y i))"
2.34 +by (rule convex_le.typedef_ideal_rep_contlub
2.35 + [OF type_definition_convex_pd sq_le_convex_pd_def])
2.36 +
2.37 +lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)"
2.38 by (rule Rep_convex_pd [unfolded mem_Collect_eq])
2.39
2.40 definition
2.41 convex_principal :: "'a pd_basis \<Rightarrow> 'a convex_pd" where
2.42 - "convex_principal t = Abs_convex_pd (Abs_cset {u. u \<le>\<natural> t})"
2.43 + "convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}"
2.44
2.45 lemma Rep_convex_principal:
2.46 - "Rep_cset (Rep_convex_pd (convex_principal t)) = {u. u \<le>\<natural> t}"
2.47 + "Rep_convex_pd (convex_principal t) = {u. u \<le>\<natural> t}"
2.48 unfolding convex_principal_def
2.49 by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
2.50
2.51 interpretation convex_pd:
2.52 - ideal_completion
2.53 - [convex_le approx_pd convex_principal "\<lambda>x. Rep_cset (Rep_convex_pd x)"]
2.54 + ideal_completion [convex_le approx_pd convex_principal Rep_convex_pd]
2.55 apply unfold_locales
2.56 apply (rule approx_pd_convex_le)
2.57 apply (rule approx_pd_idem)
2.58 @@ -168,9 +189,9 @@
2.59 apply (rule finite_range_approx_pd)
2.60 apply (rule approx_pd_covers)
2.61 apply (rule ideal_Rep_convex_pd)
2.62 -apply (simp add: cont2contlubE [OF cont_Rep_convex_pd] Rep_cset_lub)
2.63 +apply (erule Rep_convex_pd_lub)
2.64 apply (rule Rep_convex_principal)
2.65 -apply (simp only: less_convex_pd_def sq_le_cset_def)
2.66 +apply (simp only: sq_le_convex_pd_def)
2.67 done
2.68
2.69 text {* Convex powerdomain is pointed *}
2.70 @@ -210,8 +231,7 @@
2.71 by (rule convex_pd.completion_approx_principal)
2.72
2.73 lemma approx_eq_convex_principal:
2.74 - "\<exists>t\<in>Rep_cset (Rep_convex_pd xs).
2.75 - approx n\<cdot>xs = convex_principal (approx_pd n t)"
2.76 + "\<exists>t\<in>Rep_convex_pd xs. approx n\<cdot>xs = convex_principal (approx_pd n t)"
2.77 unfolding approx_convex_pd_def
2.78 by (rule convex_pd.completion_approx_eq_principal)
2.79
3.1 --- a/src/HOLCF/LowerPD.thy Thu Jun 26 15:06:30 2008 +0200
3.2 +++ b/src/HOLCF/LowerPD.thy Thu Jun 26 17:54:05 2008 +0200
3.3 @@ -96,25 +96,46 @@
3.4
3.5 subsection {* Type definition *}
3.6
3.7 -cpodef (open) 'a lower_pd =
3.8 - "{S::'a pd_basis cset. lower_le.ideal (Rep_cset S)}"
3.9 -by (rule lower_le.cpodef_ideal_lemma)
3.10 +typedef (open) 'a lower_pd =
3.11 + "{S::'a pd_basis set. lower_le.ideal S}"
3.12 +by (fast intro: lower_le.ideal_principal)
3.13
3.14 -lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_cset (Rep_lower_pd xs))"
3.15 +instantiation lower_pd :: (profinite) sq_ord
3.16 +begin
3.17 +
3.18 +definition
3.19 + "x \<sqsubseteq> y \<longleftrightarrow> Rep_lower_pd x \<subseteq> Rep_lower_pd y"
3.20 +
3.21 +instance ..
3.22 +end
3.23 +
3.24 +instance lower_pd :: (profinite) po
3.25 +by (rule lower_le.typedef_ideal_po
3.26 + [OF type_definition_lower_pd sq_le_lower_pd_def])
3.27 +
3.28 +instance lower_pd :: (profinite) cpo
3.29 +by (rule lower_le.typedef_ideal_cpo
3.30 + [OF type_definition_lower_pd sq_le_lower_pd_def])
3.31 +
3.32 +lemma Rep_lower_pd_lub:
3.33 + "chain Y \<Longrightarrow> Rep_lower_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_lower_pd (Y i))"
3.34 +by (rule lower_le.typedef_ideal_rep_contlub
3.35 + [OF type_definition_lower_pd sq_le_lower_pd_def])
3.36 +
3.37 +lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd xs)"
3.38 by (rule Rep_lower_pd [unfolded mem_Collect_eq])
3.39
3.40 definition
3.41 lower_principal :: "'a pd_basis \<Rightarrow> 'a lower_pd" where
3.42 - "lower_principal t = Abs_lower_pd (Abs_cset {u. u \<le>\<flat> t})"
3.43 + "lower_principal t = Abs_lower_pd {u. u \<le>\<flat> t}"
3.44
3.45 lemma Rep_lower_principal:
3.46 - "Rep_cset (Rep_lower_pd (lower_principal t)) = {u. u \<le>\<flat> t}"
3.47 + "Rep_lower_pd (lower_principal t) = {u. u \<le>\<flat> t}"
3.48 unfolding lower_principal_def
3.49 by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal)
3.50
3.51 interpretation lower_pd:
3.52 - ideal_completion
3.53 - [lower_le approx_pd lower_principal "\<lambda>x. Rep_cset (Rep_lower_pd x)"]
3.54 + ideal_completion [lower_le approx_pd lower_principal Rep_lower_pd]
3.55 apply unfold_locales
3.56 apply (rule approx_pd_lower_le)
3.57 apply (rule approx_pd_idem)
3.58 @@ -123,9 +144,9 @@
3.59 apply (rule finite_range_approx_pd)
3.60 apply (rule approx_pd_covers)
3.61 apply (rule ideal_Rep_lower_pd)
3.62 -apply (simp add: cont2contlubE [OF cont_Rep_lower_pd] Rep_cset_lub)
3.63 +apply (erule Rep_lower_pd_lub)
3.64 apply (rule Rep_lower_principal)
3.65 -apply (simp only: less_lower_pd_def sq_le_cset_def)
3.66 +apply (simp only: sq_le_lower_pd_def)
3.67 done
3.68
3.69 text {* Lower powerdomain is pointed *}
3.70 @@ -165,8 +186,7 @@
3.71 by (rule lower_pd.completion_approx_principal)
3.72
3.73 lemma approx_eq_lower_principal:
3.74 - "\<exists>t\<in>Rep_cset (Rep_lower_pd xs).
3.75 - approx n\<cdot>xs = lower_principal (approx_pd n t)"
3.76 + "\<exists>t\<in>Rep_lower_pd xs. approx n\<cdot>xs = lower_principal (approx_pd n t)"
3.77 unfolding approx_lower_pd_def
3.78 by (rule lower_pd.completion_approx_eq_principal)
3.79
4.1 --- a/src/HOLCF/UpperPD.thy Thu Jun 26 15:06:30 2008 +0200
4.2 +++ b/src/HOLCF/UpperPD.thy Thu Jun 26 17:54:05 2008 +0200
4.3 @@ -94,25 +94,46 @@
4.4
4.5 subsection {* Type definition *}
4.6
4.7 -cpodef (open) 'a upper_pd =
4.8 - "{S::'a pd_basis cset. upper_le.ideal (Rep_cset S)}"
4.9 -by (rule upper_le.cpodef_ideal_lemma)
4.10 +typedef (open) 'a upper_pd =
4.11 + "{S::'a pd_basis set. upper_le.ideal S}"
4.12 +by (fast intro: upper_le.ideal_principal)
4.13
4.14 -lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_cset (Rep_upper_pd xs))"
4.15 +instantiation upper_pd :: (profinite) sq_ord
4.16 +begin
4.17 +
4.18 +definition
4.19 + "x \<sqsubseteq> y \<longleftrightarrow> Rep_upper_pd x \<subseteq> Rep_upper_pd y"
4.20 +
4.21 +instance ..
4.22 +end
4.23 +
4.24 +instance upper_pd :: (profinite) po
4.25 +by (rule upper_le.typedef_ideal_po
4.26 + [OF type_definition_upper_pd sq_le_upper_pd_def])
4.27 +
4.28 +instance upper_pd :: (profinite) cpo
4.29 +by (rule upper_le.typedef_ideal_cpo
4.30 + [OF type_definition_upper_pd sq_le_upper_pd_def])
4.31 +
4.32 +lemma Rep_upper_pd_lub:
4.33 + "chain Y \<Longrightarrow> Rep_upper_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_upper_pd (Y i))"
4.34 +by (rule upper_le.typedef_ideal_rep_contlub
4.35 + [OF type_definition_upper_pd sq_le_upper_pd_def])
4.36 +
4.37 +lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd xs)"
4.38 by (rule Rep_upper_pd [unfolded mem_Collect_eq])
4.39
4.40 definition
4.41 upper_principal :: "'a pd_basis \<Rightarrow> 'a upper_pd" where
4.42 - "upper_principal t = Abs_upper_pd (Abs_cset {u. u \<le>\<sharp> t})"
4.43 + "upper_principal t = Abs_upper_pd {u. u \<le>\<sharp> t}"
4.44
4.45 lemma Rep_upper_principal:
4.46 - "Rep_cset (Rep_upper_pd (upper_principal t)) = {u. u \<le>\<sharp> t}"
4.47 + "Rep_upper_pd (upper_principal t) = {u. u \<le>\<sharp> t}"
4.48 unfolding upper_principal_def
4.49 by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal)
4.50
4.51 interpretation upper_pd:
4.52 - ideal_completion
4.53 - [upper_le approx_pd upper_principal "\<lambda>x. Rep_cset (Rep_upper_pd x)"]
4.54 + ideal_completion [upper_le approx_pd upper_principal Rep_upper_pd]
4.55 apply unfold_locales
4.56 apply (rule approx_pd_upper_le)
4.57 apply (rule approx_pd_idem)
4.58 @@ -121,9 +142,9 @@
4.59 apply (rule finite_range_approx_pd)
4.60 apply (rule approx_pd_covers)
4.61 apply (rule ideal_Rep_upper_pd)
4.62 -apply (simp add: cont2contlubE [OF cont_Rep_upper_pd] Rep_cset_lub)
4.63 +apply (erule Rep_upper_pd_lub)
4.64 apply (rule Rep_upper_principal)
4.65 -apply (simp only: less_upper_pd_def sq_le_cset_def)
4.66 +apply (simp only: sq_le_upper_pd_def)
4.67 done
4.68
4.69 text {* Upper powerdomain is pointed *}
4.70 @@ -163,8 +184,7 @@
4.71 by (rule upper_pd.completion_approx_principal)
4.72
4.73 lemma approx_eq_upper_principal:
4.74 - "\<exists>t\<in>Rep_cset (Rep_upper_pd xs).
4.75 - approx n\<cdot>xs = upper_principal (approx_pd n t)"
4.76 + "\<exists>t\<in>Rep_upper_pd xs. approx n\<cdot>xs = upper_principal (approx_pd n t)"
4.77 unfolding approx_upper_pd_def
4.78 by (rule upper_pd.completion_approx_eq_principal)
4.79