src/HOLCF/LowerPD.thy

--- 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 *}