src/HOLCF/ConvexPD.thy

--- a/src/HOLCF/ConvexPD.thy	Thu Jun 26 15:06:30 2008 +0200
+++ b/src/HOLCF/ConvexPD.thy	Thu Jun 26 17:54:05 2008 +0200
@@ -141,25 +141,46 @@
 
 subsection {* Type definition *}
 
-cpodef (open) 'a convex_pd =
-  "{S::'a pd_basis cset. convex_le.ideal (Rep_cset S)}"
-by (rule convex_le.cpodef_ideal_lemma)
+typedef (open) 'a convex_pd =
+  "{S::'a pd_basis set. convex_le.ideal S}"
+by (fast intro: convex_le.ideal_principal)
+
+instantiation convex_pd :: (profinite) sq_ord
+begin
+
+definition
+  "x \<sqsubseteq> y \<longleftrightarrow> Rep_convex_pd x \<subseteq> Rep_convex_pd y"
+
+instance ..
+end
 
-lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_cset (Rep_convex_pd xs))"
+instance convex_pd :: (profinite) po
+by (rule convex_le.typedef_ideal_po
+    [OF type_definition_convex_pd sq_le_convex_pd_def])
+
+instance convex_pd :: (profinite) cpo
+by (rule convex_le.typedef_ideal_cpo
+    [OF type_definition_convex_pd sq_le_convex_pd_def])
+
+lemma Rep_convex_pd_lub:
+  "chain Y \<Longrightarrow> Rep_convex_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_convex_pd (Y i))"
+by (rule convex_le.typedef_ideal_rep_contlub
+    [OF type_definition_convex_pd sq_le_convex_pd_def])
+
+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 (Abs_cset {u. u \<le>\<natural> t})"
+  "convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}"
 
 lemma Rep_convex_principal:
-  "Rep_cset (Rep_convex_pd (convex_principal t)) = {u. u \<le>\<natural> t}"
+  "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 approx_pd convex_principal "\<lambda>x. Rep_cset (Rep_convex_pd x)"]
+  ideal_completion [convex_le approx_pd convex_principal Rep_convex_pd]
 apply unfold_locales
 apply (rule approx_pd_convex_le)
 apply (rule approx_pd_idem)
@@ -168,9 +189,9 @@
 apply (rule finite_range_approx_pd)
 apply (rule approx_pd_covers)
 apply (rule ideal_Rep_convex_pd)
-apply (simp add: cont2contlubE [OF cont_Rep_convex_pd] Rep_cset_lub)
+apply (erule Rep_convex_pd_lub)
 apply (rule Rep_convex_principal)
-apply (simp only: less_convex_pd_def sq_le_cset_def)
+apply (simp only: sq_le_convex_pd_def)
 done
 
 text {* Convex powerdomain is pointed *}
@@ -210,8 +231,7 @@
 by (rule convex_pd.completion_approx_principal)
 
 lemma approx_eq_convex_principal:
-  "\<exists>t\<in>Rep_cset (Rep_convex_pd xs).
-    approx n\<cdot>xs = convex_principal (approx_pd n t)"
+  "\<exists>t\<in>Rep_convex_pd xs. approx n\<cdot>xs = convex_principal (approx_pd n t)"
 unfolding approx_convex_pd_def
 by (rule convex_pd.completion_approx_eq_principal)