remove cset theory; define ideal completions using typedef instead of cpodef
authorhuffman
Thu Jun 26 17:54:05 2008 +0200 (2008-06-26)
changeset 273735794a0e3e26c
parent 27372 29a09358953f
child 27374 2a3c22fd95ab
remove cset theory; define ideal completions using typedef instead of cpodef
src/HOLCF/CompactBasis.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/LowerPD.thy
src/HOLCF/UpperPD.thy
     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 +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