add lemma typedef_ideal_completion

--- a/src/HOLCF/Algebraic.thy	Thu Oct 07 13:22:13 2010 -0700
+++ b/src/HOLCF/Algebraic.thy	Thu Oct 07 13:33:06 2010 -0700
@@ -99,23 +99,10 @@
 using type_definition_sfp below_sfp_def
 by (rule below.typedef_ideal_cpo)
 
-lemma Rep_sfp_lub:
-  "chain Y \<Longrightarrow> Rep_sfp (\<Squnion>i. Y i) = (\<Union>i. Rep_sfp (Y i))"
-using type_definition_sfp below_sfp_def
-by (rule below.typedef_ideal_rep_contlub)
-
-lemma ideal_Rep_sfp: "below.ideal (Rep_sfp xs)"
-by (rule Rep_sfp [unfolded mem_Collect_eq])
-
 definition
   sfp_principal :: "fin_defl \<Rightarrow> sfp" where
   "sfp_principal t = Abs_sfp {u. u \<sqsubseteq> t}"
 
-lemma Rep_sfp_principal:
-  "Rep_sfp (sfp_principal t) = {u. u \<sqsubseteq> t}"
-unfolding sfp_principal_def
-by (simp add: Abs_sfp_inverse below.ideal_principal)
-
 lemma fin_defl_countable: "\<exists>f::fin_defl \<Rightarrow> nat. inj f"
 proof
   have *: "\<And>d. finite (approx_chain.place udom_approx `
@@ -144,13 +131,9 @@
 qed
 
 interpretation sfp: ideal_completion below sfp_principal Rep_sfp
-apply default
-apply (rule ideal_Rep_sfp)
-apply (erule Rep_sfp_lub)
-apply (rule Rep_sfp_principal)
-apply (simp only: below_sfp_def)
-apply (rule fin_defl_countable)
-done
+using type_definition_sfp below_sfp_def
+using sfp_principal_def fin_defl_countable
+by (rule below.typedef_ideal_completion)
 
 text {* Algebraic deflations are pointed *}
 

--- a/src/HOLCF/Completion.thy	Thu Oct 07 13:22:13 2010 -0700
+++ b/src/HOLCF/Completion.thy	Thu Oct 07 13:33:06 2010 -0700
@@ -410,4 +410,26 @@
 
 end
 
+lemma (in preorder) typedef_ideal_completion:
+  fixes Abs :: "'a set \<Rightarrow> 'b::cpo"
+  assumes type: "type_definition Rep Abs {S. ideal S}"
+  assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
+  assumes principal: "\<And>a. principal a = Abs {b. b \<preceq> a}"
+  assumes countable: "\<exists>f::'a \<Rightarrow> nat. inj f"
+  shows "ideal_completion r principal Rep"
+proof
+  interpret type_definition Rep Abs "{S. ideal S}" by fact
+  fix a b :: 'a and x y :: 'b and Y :: "nat \<Rightarrow> 'b"
+  show "ideal (Rep x)"
+    using Rep [of x] by simp
+  show "chain Y \<Longrightarrow> Rep (\<Squnion>i. Y i) = (\<Union>i. Rep (Y i))"
+    using type below by (rule typedef_ideal_rep_contlub)
+  show "Rep (principal a) = {b. b \<preceq> a}"
+    by (simp add: principal Abs_inverse ideal_principal)
+  show "Rep x \<subseteq> Rep y \<Longrightarrow> x \<sqsubseteq> y"
+    by (simp only: below)
+  show "\<exists>f::'a \<Rightarrow> nat. inj f"
+    by (rule countable)
+qed
+
 end

--- a/src/HOLCF/ConvexPD.thy	Thu Oct 07 13:22:13 2010 -0700
+++ b/src/HOLCF/ConvexPD.thy	Thu Oct 07 13:33:06 2010 -0700
@@ -140,32 +140,15 @@
 using type_definition_convex_pd below_convex_pd_def
 by (rule convex_le.typedef_ideal_cpo)
 
-lemma Rep_convex_pd_lub:
-  "chain Y \<Longrightarrow> Rep_convex_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_convex_pd (Y i))"
-using type_definition_convex_pd below_convex_pd_def
-by (rule convex_le.typedef_ideal_rep_contlub)
-
-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 {u. u \<le>\<natural> t}"
 
-lemma Rep_convex_principal:
-  "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 convex_principal Rep_convex_pd
-apply unfold_locales
-apply (rule ideal_Rep_convex_pd)
-apply (erule Rep_convex_pd_lub)
-apply (rule Rep_convex_principal)
-apply (simp only: below_convex_pd_def)
-apply (rule pd_basis_countable)
-done
+using type_definition_convex_pd below_convex_pd_def
+using convex_principal_def pd_basis_countable
+by (rule convex_le.typedef_ideal_completion)
 
 text {* Convex powerdomain is pointed *}
 

--- a/src/HOLCF/LowerPD.thy	Thu Oct 07 13:22:13 2010 -0700
+++ b/src/HOLCF/LowerPD.thy	Thu Oct 07 13:33:06 2010 -0700
@@ -88,39 +88,22 @@
 end
 
 instance lower_pd :: (sfp) po
-by (rule lower_le.typedef_ideal_po
-    [OF type_definition_lower_pd below_lower_pd_def])
+using type_definition_lower_pd below_lower_pd_def
+by (rule lower_le.typedef_ideal_po)
 
 instance lower_pd :: (sfp) cpo
-by (rule lower_le.typedef_ideal_cpo
-    [OF type_definition_lower_pd below_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 below_lower_pd_def])
-
-lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd xs)"
-by (rule Rep_lower_pd [unfolded mem_Collect_eq])
+using type_definition_lower_pd below_lower_pd_def
+by (rule lower_le.typedef_ideal_cpo)
 
 definition
   lower_principal :: "'a pd_basis \<Rightarrow> 'a lower_pd" where
   "lower_principal t = Abs_lower_pd {u. u \<le>\<flat> t}"
 
-lemma Rep_lower_principal:
-  "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 lower_principal Rep_lower_pd
-apply unfold_locales
-apply (rule ideal_Rep_lower_pd)
-apply (erule Rep_lower_pd_lub)
-apply (rule Rep_lower_principal)
-apply (simp only: below_lower_pd_def)
-apply (rule pd_basis_countable)
-done
+using type_definition_lower_pd below_lower_pd_def
+using lower_principal_def pd_basis_countable
+by (rule lower_le.typedef_ideal_completion)
 
 text {* Lower powerdomain is pointed *}
 

--- a/src/HOLCF/Universal.thy	Thu Oct 07 13:22:13 2010 -0700
+++ b/src/HOLCF/Universal.thy	Thu Oct 07 13:33:06 2010 -0700
@@ -218,32 +218,18 @@
 using type_definition_udom below_udom_def
 by (rule udom.typedef_ideal_cpo)
 
-lemma Rep_udom_lub:
-  "chain Y \<Longrightarrow> Rep_udom (\<Squnion>i. Y i) = (\<Union>i. Rep_udom (Y i))"
-using type_definition_udom below_udom_def
-by (rule udom.typedef_ideal_rep_contlub)
-
-lemma ideal_Rep_udom: "udom.ideal (Rep_udom xs)"
-by (rule Rep_udom [unfolded mem_Collect_eq])
-
 definition
   udom_principal :: "nat \<Rightarrow> udom" where
   "udom_principal t = Abs_udom {u. ubasis_le u t}"
 
-lemma Rep_udom_principal:
-  "Rep_udom (udom_principal t) = {u. ubasis_le u t}"
-unfolding udom_principal_def
-by (simp add: Abs_udom_inverse udom.ideal_principal)
+lemma ubasis_countable: "\<exists>f::ubasis \<Rightarrow> nat. inj f"
+by (rule exI, rule inj_on_id)
 
 interpretation udom:
   ideal_completion ubasis_le udom_principal Rep_udom
-apply unfold_locales
-apply (rule ideal_Rep_udom)
-apply (erule Rep_udom_lub)
-apply (rule Rep_udom_principal)
-apply (simp only: below_udom_def)
-apply (rule exI, rule inj_on_id)
-done
+using type_definition_udom below_udom_def
+using udom_principal_def ubasis_countable
+by (rule udom.typedef_ideal_completion)
 
 text {* Universal domain is pointed *}
 

--- a/src/HOLCF/UpperPD.thy	Thu Oct 07 13:22:13 2010 -0700
+++ b/src/HOLCF/UpperPD.thy	Thu Oct 07 13:33:06 2010 -0700
@@ -93,32 +93,15 @@
 using type_definition_upper_pd below_upper_pd_def
 by (rule upper_le.typedef_ideal_cpo)
 
-lemma Rep_upper_pd_lub:
-  "chain Y \<Longrightarrow> Rep_upper_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_upper_pd (Y i))"
-using type_definition_upper_pd below_upper_pd_def
-by (rule upper_le.typedef_ideal_rep_contlub)
-
-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 {u. u \<le>\<sharp> t}"
 
-lemma Rep_upper_principal:
-  "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 upper_principal Rep_upper_pd
-apply unfold_locales
-apply (rule ideal_Rep_upper_pd)
-apply (erule Rep_upper_pd_lub)
-apply (rule Rep_upper_principal)
-apply (simp only: below_upper_pd_def)
-apply (rule pd_basis_countable)
-done
+using type_definition_upper_pd below_upper_pd_def
+using upper_principal_def pd_basis_countable
+by (rule upper_le.typedef_ideal_completion)
 
 text {* Upper powerdomain is pointed *}