author huffman Thu Jun 26 17:54:05 2008 +0200 (2008-06-26) changeset 27373 5794a0e3e26c parent 27372 29a09358953f child 27374 2a3c22fd95ab
remove cset theory; define ideal completions using typedef instead of cpodef
 src/HOLCF/CompactBasis.thy file | annotate | diff | revisions src/HOLCF/ConvexPD.thy file | annotate | diff | revisions src/HOLCF/LowerPD.thy file | annotate | diff | revisions src/HOLCF/UpperPD.thy file | annotate | diff | revisions
```     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.14  done
1.15
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.22 -apply (rule exI [where x="Abs_cset {x. x \<preceq> arbitrary}"])
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.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 +instantiation convex_pd :: (profinite) sq_ord
2.15 +begin
2.16 +
2.17 +definition
2.18 +  "x \<sqsubseteq> y \<longleftrightarrow> Rep_convex_pd x \<subseteq> Rep_convex_pd y"
2.19 +
2.20 +instance ..
2.21 +end
2.22
2.23 -lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_cset (Rep_convex_pd xs))"
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 +instantiation lower_pd :: (profinite) sq_ord
3.15 +begin
3.16 +
3.17 +definition
3.18 +  "x \<sqsubseteq> y \<longleftrightarrow> Rep_lower_pd x \<subseteq> Rep_lower_pd y"
3.19 +
3.20 +instance ..
3.21 +end
3.22
3.23 -lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_cset (Rep_lower_pd xs))"
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 +instantiation upper_pd :: (profinite) sq_ord
4.15 +begin
4.16 +
4.17 +definition
4.18 +  "x \<sqsubseteq> y \<longleftrightarrow> Rep_upper_pd x \<subseteq> Rep_upper_pd y"
4.19 +
4.20 +instance ..
4.21 +end
4.22
4.23 -lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_cset (Rep_upper_pd xs))"
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
```