--- 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 (\<lambda>A. ideal (Rep_cset A))"
-unfolding ideal_def by (intro adm_lemmas adm_set_lemmas)
-
-lemma cpodef_ideal_lemma:
- "(\<exists>x. x \<in> {S. ideal (Rep_cset S)}) \<and> adm (\<lambda>x. x \<in> {S. ideal (Rep_cset S)})"
-apply (simp add: adm_ideal)
-apply (rule exI [where x="Abs_cset {x. x \<preceq> arbitrary}"])
-apply (simp add: ideal_principal)
-done
-
lemma lub_image_principal:
assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
shows "(\<Squnion>x\<in>{x. x \<preceq> 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 \<Rightarrow> 'a set"
+ assumes ideal_A: "\<And>i. ideal (A i)"
+ assumes chain_A: "\<And>i j. i \<le> j \<Longrightarrow> A i \<subseteq> A j"
+ shows "ideal (\<Union>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 \<Rightarrow> 'b::sq_ord"
+ assumes type: "type_definition Rep Abs {S. ideal S}"
+ assumes less: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> 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 \<Rightarrow> 'b::po"
+ assumes type: "type_definition Rep Abs {S. ideal S}"
+ assumes less: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
+ assumes S: "chain S"
+ shows typedef_ideal_lub: "range S <<| Abs (\<Union>i. Rep (S i))"
+ and typedef_ideal_rep_contlub: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))"
+proof -
+ have 1: "ideal (\<Union>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 (\<Union>i. Rep (S i))) = (\<Union>i. Rep (S i))"
+ by (simp add: type_definition.Abs_inverse [OF type])
+ show 3: "range S <<| Abs (\<Union>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: "(\<Squnion>i. S i) = Abs (\<Union>i. Rep (S i))"
+ by (rule thelubI)
+ show 5: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))"
+ by (simp add: 4 2)
+qed
+
+lemma typedef_ideal_cpo:
+ fixes Abs :: "'a set \<Rightarrow> 'b::po"
+ assumes type: "type_definition Rep Abs {S. ideal S}"
+ assumes less: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> 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 \<Rightarrow> 'a \<Rightarrow> bool"]
--- 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 \<sqsubseteq> y \<longleftrightarrow> Rep_convex_pd x \<subseteq> 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 \<Longrightarrow> Rep_convex_pd (\<Squnion>i. Y i) = (\<Union>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 \<Rightarrow> 'a convex_pd" where
- "convex_principal t = Abs_convex_pd (Abs_cset {u. u \<le>\<natural> t})"
+ "convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}"
lemma Rep_convex_principal:
- "Rep_cset (Rep_convex_pd (convex_principal t)) = {u. u \<le>\<natural> t}"
+ "Rep_convex_pd (convex_principal t) = {u. u \<le>\<natural> 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 "\<lambda>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:
- "\<exists>t\<in>Rep_cset (Rep_convex_pd xs).
- approx n\<cdot>xs = convex_principal (approx_pd n t)"
+ "\<exists>t\<in>Rep_convex_pd xs. approx n\<cdot>xs = convex_principal (approx_pd n t)"
unfolding approx_convex_pd_def
by (rule convex_pd.completion_approx_eq_principal)
--- 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 \<sqsubseteq> y \<longleftrightarrow> Rep_lower_pd x \<subseteq> 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 \<Longrightarrow> Rep_lower_pd (\<Squnion>i. Y i) = (\<Union>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 \<Rightarrow> 'a lower_pd" where
- "lower_principal t = Abs_lower_pd (Abs_cset {u. u \<le>\<flat> t})"
+ "lower_principal t = Abs_lower_pd {u. u \<le>\<flat> t}"
lemma Rep_lower_principal:
- "Rep_cset (Rep_lower_pd (lower_principal t)) = {u. u \<le>\<flat> t}"
+ "Rep_lower_pd (lower_principal t) = {u. u \<le>\<flat> 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 "\<lambda>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:
- "\<exists>t\<in>Rep_cset (Rep_lower_pd xs).
- approx n\<cdot>xs = lower_principal (approx_pd n t)"
+ "\<exists>t\<in>Rep_lower_pd xs. approx n\<cdot>xs = lower_principal (approx_pd n t)"
unfolding approx_lower_pd_def
by (rule lower_pd.completion_approx_eq_principal)
--- 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 \<sqsubseteq> y \<longleftrightarrow> Rep_upper_pd x \<subseteq> 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 \<Longrightarrow> Rep_upper_pd (\<Squnion>i. Y i) = (\<Union>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 \<Rightarrow> 'a upper_pd" where
- "upper_principal t = Abs_upper_pd (Abs_cset {u. u \<le>\<sharp> t})"
+ "upper_principal t = Abs_upper_pd {u. u \<le>\<sharp> t}"
lemma Rep_upper_principal:
- "Rep_cset (Rep_upper_pd (upper_principal t)) = {u. u \<le>\<sharp> t}"
+ "Rep_upper_pd (upper_principal t) = {u. u \<le>\<sharp> 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 "\<lambda>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:
- "\<exists>t\<in>Rep_cset (Rep_upper_pd xs).
- approx n\<cdot>xs = upper_principal (approx_pd n t)"
+ "\<exists>t\<in>Rep_upper_pd xs. approx n\<cdot>xs = upper_principal (approx_pd n t)"
unfolding approx_upper_pd_def
by (rule upper_pd.completion_approx_eq_principal)