--- a/src/HOLCF/LowerPD.thy Fri Jun 20 19:59:00 2008 +0200
+++ b/src/HOLCF/LowerPD.thy Fri Jun 20 20:03:13 2008 +0200
@@ -97,27 +97,24 @@
subsection {* Type definition *}
cpodef (open) 'a lower_pd =
- "{S::'a::profinite pd_basis set. lower_le.ideal S}"
-apply (simp add: lower_le.adm_ideal)
-apply (fast intro: lower_le.ideal_principal)
-done
+ "{S::'a pd_basis cset. lower_le.ideal (Rep_cset S)}"
+by (rule lower_le.cpodef_ideal_lemma)
-lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd x)"
+lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_cset (Rep_lower_pd xs))"
by (rule Rep_lower_pd [unfolded mem_Collect_eq])
definition
lower_principal :: "'a pd_basis \<Rightarrow> 'a lower_pd" where
- "lower_principal t = Abs_lower_pd {u. u \<le>\<flat> t}"
+ "lower_principal t = Abs_lower_pd (Abs_cset {u. u \<le>\<flat> t})"
lemma Rep_lower_principal:
- "Rep_lower_pd (lower_principal t) = {u. u \<le>\<flat> t}"
+ "Rep_cset (Rep_lower_pd (lower_principal t)) = {u. u \<le>\<flat> t}"
unfolding lower_principal_def
-apply (rule Abs_lower_pd_inverse [simplified])
-apply (rule lower_le.ideal_principal)
-done
+by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal)
interpretation lower_pd:
- ideal_completion [lower_le approx_pd lower_principal Rep_lower_pd]
+ ideal_completion
+ [lower_le approx_pd lower_principal "\<lambda>x. Rep_cset (Rep_lower_pd x)"]
apply unfold_locales
apply (rule approx_pd_lower_le)
apply (rule approx_pd_idem)
@@ -126,9 +123,9 @@
apply (rule finite_range_approx_pd)
apply (rule approx_pd_covers)
apply (rule ideal_Rep_lower_pd)
-apply (rule cont_Rep_lower_pd)
+apply (simp add: cont2contlubE [OF cont_Rep_lower_pd] Rep_cset_lub)
apply (rule Rep_lower_principal)
-apply (simp only: less_lower_pd_def less_set_eq)
+apply (simp only: less_lower_pd_def sq_le_cset_def)
done
text {* Lower powerdomain is pointed *}
@@ -168,7 +165,8 @@
by (rule lower_pd.completion_approx_principal)
lemma approx_eq_lower_principal:
- "\<exists>t\<in>Rep_lower_pd xs. approx n\<cdot>xs = lower_principal (approx_pd n t)"
+ "\<exists>t\<in>Rep_cset (Rep_lower_pd xs).
+ approx n\<cdot>xs = lower_principal (approx_pd n t)"
unfolding approx_lower_pd_def
by (rule lower_pd.completion_approx_eq_principal)