1.1 --- a/src/HOLCF/ConvexPD.thy	Fri Jun 20 19:59:00 2008 +0200
     1.2 +++ b/src/HOLCF/ConvexPD.thy	Fri Jun 20 20:03:13 2008 +0200
     1.3 @@ -142,30 +142,24 @@
     1.4  subsection {* Type definition *}
     1.5  
     1.6  cpodef (open) 'a convex_pd =
     1.7 -  "{S::'a::profinite pd_basis set. convex_le.ideal S}"
     1.8 -apply (simp add: convex_le.adm_ideal)
     1.9 -apply (fast intro: convex_le.ideal_principal)
    1.10 -done
    1.11 +  "{S::'a pd_basis cset. convex_le.ideal (Rep_cset S)}"
    1.12 +by (rule convex_le.cpodef_ideal_lemma)
    1.13  
    1.14 -lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)"
    1.15 +lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_cset (Rep_convex_pd xs))"
    1.16  by (rule Rep_convex_pd [unfolded mem_Collect_eq])
    1.17  
    1.18 -lemma Rep_convex_pd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> Rep_convex_pd xs \<subseteq> Rep_convex_pd ys"
    1.19 -unfolding less_convex_pd_def less_set_eq .
    1.20 -
    1.21  definition
    1.22    convex_principal :: "'a pd_basis \<Rightarrow> 'a convex_pd" where
    1.23 -  "convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}"
    1.24 +  "convex_principal t = Abs_convex_pd (Abs_cset {u. u \<le>\<natural> t})"
    1.25  
    1.26  lemma Rep_convex_principal:
    1.27 -  "Rep_convex_pd (convex_principal t) = {u. u \<le>\<natural> t}"
    1.28 +  "Rep_cset (Rep_convex_pd (convex_principal t)) = {u. u \<le>\<natural> t}"
    1.29  unfolding convex_principal_def
    1.30 -apply (rule Abs_convex_pd_inverse [simplified])
    1.31 -apply (rule convex_le.ideal_principal)
    1.32 -done
    1.33 +by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
    1.34  
    1.35  interpretation convex_pd:
    1.36 -  ideal_completion [convex_le approx_pd convex_principal Rep_convex_pd]
    1.37 +  ideal_completion
    1.38 +    [convex_le approx_pd convex_principal "\<lambda>x. Rep_cset (Rep_convex_pd x)"]
    1.39  apply unfold_locales
    1.40  apply (rule approx_pd_convex_le)
    1.41  apply (rule approx_pd_idem)
    1.42 @@ -174,9 +168,9 @@
    1.43  apply (rule finite_range_approx_pd)
    1.44  apply (rule approx_pd_covers)
    1.45  apply (rule ideal_Rep_convex_pd)
    1.46 -apply (rule cont_Rep_convex_pd)
    1.47 +apply (simp add: cont2contlubE [OF cont_Rep_convex_pd] Rep_cset_lub)
    1.48  apply (rule Rep_convex_principal)
    1.49 -apply (simp only: less_convex_pd_def less_set_eq)
    1.50 +apply (simp only: less_convex_pd_def sq_le_cset_def)
    1.51  done
    1.52  
    1.53  text {* Convex powerdomain is pointed *}
    1.54 @@ -216,7 +210,8 @@
    1.55  by (rule convex_pd.completion_approx_principal)
    1.56  
    1.57  lemma approx_eq_convex_principal:
    1.58 -  "\<exists>t\<in>Rep_convex_pd xs. approx n\<cdot>xs = convex_principal (approx_pd n t)"
    1.59 +  "\<exists>t\<in>Rep_cset (Rep_convex_pd xs).
    1.60 +    approx n\<cdot>xs = convex_principal (approx_pd n t)"
    1.61  unfolding approx_convex_pd_def
    1.62  by (rule convex_pd.completion_approx_eq_principal)
    1.63