add lemma typedef_ideal_completion
authorhuffman
Thu Oct 07 13:33:06 2010 -0700 (2010-10-07)
changeset 399840300d5170622
parent 39983 910d3ea1efa8
child 39985 310f98585107
add lemma typedef_ideal_completion
src/HOLCF/Algebraic.thy
src/HOLCF/Completion.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/LowerPD.thy
src/HOLCF/Universal.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOLCF/Algebraic.thy	Thu Oct 07 13:22:13 2010 -0700
     1.2 +++ b/src/HOLCF/Algebraic.thy	Thu Oct 07 13:33:06 2010 -0700
     1.3 @@ -99,23 +99,10 @@
     1.4  using type_definition_sfp below_sfp_def
     1.5  by (rule below.typedef_ideal_cpo)
     1.6  
     1.7 -lemma Rep_sfp_lub:
     1.8 -  "chain Y \<Longrightarrow> Rep_sfp (\<Squnion>i. Y i) = (\<Union>i. Rep_sfp (Y i))"
     1.9 -using type_definition_sfp below_sfp_def
    1.10 -by (rule below.typedef_ideal_rep_contlub)
    1.11 -
    1.12 -lemma ideal_Rep_sfp: "below.ideal (Rep_sfp xs)"
    1.13 -by (rule Rep_sfp [unfolded mem_Collect_eq])
    1.14 -
    1.15  definition
    1.16    sfp_principal :: "fin_defl \<Rightarrow> sfp" where
    1.17    "sfp_principal t = Abs_sfp {u. u \<sqsubseteq> t}"
    1.18  
    1.19 -lemma Rep_sfp_principal:
    1.20 -  "Rep_sfp (sfp_principal t) = {u. u \<sqsubseteq> t}"
    1.21 -unfolding sfp_principal_def
    1.22 -by (simp add: Abs_sfp_inverse below.ideal_principal)
    1.23 -
    1.24  lemma fin_defl_countable: "\<exists>f::fin_defl \<Rightarrow> nat. inj f"
    1.25  proof
    1.26    have *: "\<And>d. finite (approx_chain.place udom_approx `
    1.27 @@ -144,13 +131,9 @@
    1.28  qed
    1.29  
    1.30  interpretation sfp: ideal_completion below sfp_principal Rep_sfp
    1.31 -apply default
    1.32 -apply (rule ideal_Rep_sfp)
    1.33 -apply (erule Rep_sfp_lub)
    1.34 -apply (rule Rep_sfp_principal)
    1.35 -apply (simp only: below_sfp_def)
    1.36 -apply (rule fin_defl_countable)
    1.37 -done
    1.38 +using type_definition_sfp below_sfp_def
    1.39 +using sfp_principal_def fin_defl_countable
    1.40 +by (rule below.typedef_ideal_completion)
    1.41  
    1.42  text {* Algebraic deflations are pointed *}
    1.43  
     2.1 --- a/src/HOLCF/Completion.thy	Thu Oct 07 13:22:13 2010 -0700
     2.2 +++ b/src/HOLCF/Completion.thy	Thu Oct 07 13:33:06 2010 -0700
     2.3 @@ -410,4 +410,26 @@
     2.4  
     2.5  end
     2.6  
     2.7 +lemma (in preorder) typedef_ideal_completion:
     2.8 +  fixes Abs :: "'a set \<Rightarrow> 'b::cpo"
     2.9 +  assumes type: "type_definition Rep Abs {S. ideal S}"
    2.10 +  assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
    2.11 +  assumes principal: "\<And>a. principal a = Abs {b. b \<preceq> a}"
    2.12 +  assumes countable: "\<exists>f::'a \<Rightarrow> nat. inj f"
    2.13 +  shows "ideal_completion r principal Rep"
    2.14 +proof
    2.15 +  interpret type_definition Rep Abs "{S. ideal S}" by fact
    2.16 +  fix a b :: 'a and x y :: 'b and Y :: "nat \<Rightarrow> 'b"
    2.17 +  show "ideal (Rep x)"
    2.18 +    using Rep [of x] by simp
    2.19 +  show "chain Y \<Longrightarrow> Rep (\<Squnion>i. Y i) = (\<Union>i. Rep (Y i))"
    2.20 +    using type below by (rule typedef_ideal_rep_contlub)
    2.21 +  show "Rep (principal a) = {b. b \<preceq> a}"
    2.22 +    by (simp add: principal Abs_inverse ideal_principal)
    2.23 +  show "Rep x \<subseteq> Rep y \<Longrightarrow> x \<sqsubseteq> y"
    2.24 +    by (simp only: below)
    2.25 +  show "\<exists>f::'a \<Rightarrow> nat. inj f"
    2.26 +    by (rule countable)
    2.27 +qed
    2.28 +
    2.29  end
     3.1 --- a/src/HOLCF/ConvexPD.thy	Thu Oct 07 13:22:13 2010 -0700
     3.2 +++ b/src/HOLCF/ConvexPD.thy	Thu Oct 07 13:33:06 2010 -0700
     3.3 @@ -140,32 +140,15 @@
     3.4  using type_definition_convex_pd below_convex_pd_def
     3.5  by (rule convex_le.typedef_ideal_cpo)
     3.6  
     3.7 -lemma Rep_convex_pd_lub:
     3.8 -  "chain Y \<Longrightarrow> Rep_convex_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_convex_pd (Y i))"
     3.9 -using type_definition_convex_pd below_convex_pd_def
    3.10 -by (rule convex_le.typedef_ideal_rep_contlub)
    3.11 -
    3.12 -lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)"
    3.13 -by (rule Rep_convex_pd [unfolded mem_Collect_eq])
    3.14 -
    3.15  definition
    3.16    convex_principal :: "'a pd_basis \<Rightarrow> 'a convex_pd" where
    3.17    "convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}"
    3.18  
    3.19 -lemma Rep_convex_principal:
    3.20 -  "Rep_convex_pd (convex_principal t) = {u. u \<le>\<natural> t}"
    3.21 -unfolding convex_principal_def
    3.22 -by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
    3.23 -
    3.24  interpretation convex_pd:
    3.25    ideal_completion convex_le convex_principal Rep_convex_pd
    3.26 -apply unfold_locales
    3.27 -apply (rule ideal_Rep_convex_pd)
    3.28 -apply (erule Rep_convex_pd_lub)
    3.29 -apply (rule Rep_convex_principal)
    3.30 -apply (simp only: below_convex_pd_def)
    3.31 -apply (rule pd_basis_countable)
    3.32 -done
    3.33 +using type_definition_convex_pd below_convex_pd_def
    3.34 +using convex_principal_def pd_basis_countable
    3.35 +by (rule convex_le.typedef_ideal_completion)
    3.36  
    3.37  text {* Convex powerdomain is pointed *}
    3.38  
     4.1 --- a/src/HOLCF/LowerPD.thy	Thu Oct 07 13:22:13 2010 -0700
     4.2 +++ b/src/HOLCF/LowerPD.thy	Thu Oct 07 13:33:06 2010 -0700
     4.3 @@ -88,39 +88,22 @@
     4.4  end
     4.5  
     4.6  instance lower_pd :: (sfp) po
     4.7 -by (rule lower_le.typedef_ideal_po
     4.8 -    [OF type_definition_lower_pd below_lower_pd_def])
     4.9 +using type_definition_lower_pd below_lower_pd_def
    4.10 +by (rule lower_le.typedef_ideal_po)
    4.11  
    4.12  instance lower_pd :: (sfp) cpo
    4.13 -by (rule lower_le.typedef_ideal_cpo
    4.14 -    [OF type_definition_lower_pd below_lower_pd_def])
    4.15 -
    4.16 -lemma Rep_lower_pd_lub:
    4.17 -  "chain Y \<Longrightarrow> Rep_lower_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_lower_pd (Y i))"
    4.18 -by (rule lower_le.typedef_ideal_rep_contlub
    4.19 -    [OF type_definition_lower_pd below_lower_pd_def])
    4.20 -
    4.21 -lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd xs)"
    4.22 -by (rule Rep_lower_pd [unfolded mem_Collect_eq])
    4.23 +using type_definition_lower_pd below_lower_pd_def
    4.24 +by (rule lower_le.typedef_ideal_cpo)
    4.25  
    4.26  definition
    4.27    lower_principal :: "'a pd_basis \<Rightarrow> 'a lower_pd" where
    4.28    "lower_principal t = Abs_lower_pd {u. u \<le>\<flat> t}"
    4.29  
    4.30 -lemma Rep_lower_principal:
    4.31 -  "Rep_lower_pd (lower_principal t) = {u. u \<le>\<flat> t}"
    4.32 -unfolding lower_principal_def
    4.33 -by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal)
    4.34 -
    4.35  interpretation lower_pd:
    4.36    ideal_completion lower_le lower_principal Rep_lower_pd
    4.37 -apply unfold_locales
    4.38 -apply (rule ideal_Rep_lower_pd)
    4.39 -apply (erule Rep_lower_pd_lub)
    4.40 -apply (rule Rep_lower_principal)
    4.41 -apply (simp only: below_lower_pd_def)
    4.42 -apply (rule pd_basis_countable)
    4.43 -done
    4.44 +using type_definition_lower_pd below_lower_pd_def
    4.45 +using lower_principal_def pd_basis_countable
    4.46 +by (rule lower_le.typedef_ideal_completion)
    4.47  
    4.48  text {* Lower powerdomain is pointed *}
    4.49  
     5.1 --- a/src/HOLCF/Universal.thy	Thu Oct 07 13:22:13 2010 -0700
     5.2 +++ b/src/HOLCF/Universal.thy	Thu Oct 07 13:33:06 2010 -0700
     5.3 @@ -218,32 +218,18 @@
     5.4  using type_definition_udom below_udom_def
     5.5  by (rule udom.typedef_ideal_cpo)
     5.6  
     5.7 -lemma Rep_udom_lub:
     5.8 -  "chain Y \<Longrightarrow> Rep_udom (\<Squnion>i. Y i) = (\<Union>i. Rep_udom (Y i))"
     5.9 -using type_definition_udom below_udom_def
    5.10 -by (rule udom.typedef_ideal_rep_contlub)
    5.11 -
    5.12 -lemma ideal_Rep_udom: "udom.ideal (Rep_udom xs)"
    5.13 -by (rule Rep_udom [unfolded mem_Collect_eq])
    5.14 -
    5.15  definition
    5.16    udom_principal :: "nat \<Rightarrow> udom" where
    5.17    "udom_principal t = Abs_udom {u. ubasis_le u t}"
    5.18  
    5.19 -lemma Rep_udom_principal:
    5.20 -  "Rep_udom (udom_principal t) = {u. ubasis_le u t}"
    5.21 -unfolding udom_principal_def
    5.22 -by (simp add: Abs_udom_inverse udom.ideal_principal)
    5.23 +lemma ubasis_countable: "\<exists>f::ubasis \<Rightarrow> nat. inj f"
    5.24 +by (rule exI, rule inj_on_id)
    5.25  
    5.26  interpretation udom:
    5.27    ideal_completion ubasis_le udom_principal Rep_udom
    5.28 -apply unfold_locales
    5.29 -apply (rule ideal_Rep_udom)
    5.30 -apply (erule Rep_udom_lub)
    5.31 -apply (rule Rep_udom_principal)
    5.32 -apply (simp only: below_udom_def)
    5.33 -apply (rule exI, rule inj_on_id)
    5.34 -done
    5.35 +using type_definition_udom below_udom_def
    5.36 +using udom_principal_def ubasis_countable
    5.37 +by (rule udom.typedef_ideal_completion)
    5.38  
    5.39  text {* Universal domain is pointed *}
    5.40  
     6.1 --- a/src/HOLCF/UpperPD.thy	Thu Oct 07 13:22:13 2010 -0700
     6.2 +++ b/src/HOLCF/UpperPD.thy	Thu Oct 07 13:33:06 2010 -0700
     6.3 @@ -93,32 +93,15 @@
     6.4  using type_definition_upper_pd below_upper_pd_def
     6.5  by (rule upper_le.typedef_ideal_cpo)
     6.6  
     6.7 -lemma Rep_upper_pd_lub:
     6.8 -  "chain Y \<Longrightarrow> Rep_upper_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_upper_pd (Y i))"
     6.9 -using type_definition_upper_pd below_upper_pd_def
    6.10 -by (rule upper_le.typedef_ideal_rep_contlub)
    6.11 -
    6.12 -lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd xs)"
    6.13 -by (rule Rep_upper_pd [unfolded mem_Collect_eq])
    6.14 -
    6.15  definition
    6.16    upper_principal :: "'a pd_basis \<Rightarrow> 'a upper_pd" where
    6.17    "upper_principal t = Abs_upper_pd {u. u \<le>\<sharp> t}"
    6.18  
    6.19 -lemma Rep_upper_principal:
    6.20 -  "Rep_upper_pd (upper_principal t) = {u. u \<le>\<sharp> t}"
    6.21 -unfolding upper_principal_def
    6.22 -by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal)
    6.23 -
    6.24  interpretation upper_pd:
    6.25    ideal_completion upper_le upper_principal Rep_upper_pd
    6.26 -apply unfold_locales
    6.27 -apply (rule ideal_Rep_upper_pd)
    6.28 -apply (erule Rep_upper_pd_lub)
    6.29 -apply (rule Rep_upper_principal)
    6.30 -apply (simp only: below_upper_pd_def)
    6.31 -apply (rule pd_basis_countable)
    6.32 -done
    6.33 +using type_definition_upper_pd below_upper_pd_def
    6.34 +using upper_principal_def pd_basis_countable
    6.35 +by (rule upper_le.typedef_ideal_completion)
    6.36  
    6.37  text {* Upper powerdomain is pointed *}
    6.38