src/HOLCF/ConvexPD.thy
changeset 27373 5794a0e3e26c
parent 27310 d0229bc6c461
child 27405 785f5dbec8f4
     1.1 --- a/src/HOLCF/ConvexPD.thy	Thu Jun 26 15:06:30 2008 +0200
     1.2 +++ b/src/HOLCF/ConvexPD.thy	Thu Jun 26 17:54:05 2008 +0200
     1.3 @@ -141,25 +141,46 @@
     1.4  
     1.5  subsection {* Type definition *}
     1.6  
     1.7 -cpodef (open) 'a convex_pd =
     1.8 -  "{S::'a pd_basis cset. convex_le.ideal (Rep_cset S)}"
     1.9 -by (rule convex_le.cpodef_ideal_lemma)
    1.10 +typedef (open) 'a convex_pd =
    1.11 +  "{S::'a pd_basis set. convex_le.ideal S}"
    1.12 +by (fast intro: convex_le.ideal_principal)
    1.13 +
    1.14 +instantiation convex_pd :: (profinite) sq_ord
    1.15 +begin
    1.16 +
    1.17 +definition
    1.18 +  "x \<sqsubseteq> y \<longleftrightarrow> Rep_convex_pd x \<subseteq> Rep_convex_pd y"
    1.19 +
    1.20 +instance ..
    1.21 +end
    1.22  
    1.23 -lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_cset (Rep_convex_pd xs))"
    1.24 +instance convex_pd :: (profinite) po
    1.25 +by (rule convex_le.typedef_ideal_po
    1.26 +    [OF type_definition_convex_pd sq_le_convex_pd_def])
    1.27 +
    1.28 +instance convex_pd :: (profinite) cpo
    1.29 +by (rule convex_le.typedef_ideal_cpo
    1.30 +    [OF type_definition_convex_pd sq_le_convex_pd_def])
    1.31 +
    1.32 +lemma Rep_convex_pd_lub:
    1.33 +  "chain Y \<Longrightarrow> Rep_convex_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_convex_pd (Y i))"
    1.34 +by (rule convex_le.typedef_ideal_rep_contlub
    1.35 +    [OF type_definition_convex_pd sq_le_convex_pd_def])
    1.36 +
    1.37 +lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)"
    1.38  by (rule Rep_convex_pd [unfolded mem_Collect_eq])
    1.39  
    1.40  definition
    1.41    convex_principal :: "'a pd_basis \<Rightarrow> 'a convex_pd" where
    1.42 -  "convex_principal t = Abs_convex_pd (Abs_cset {u. u \<le>\<natural> t})"
    1.43 +  "convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}"
    1.44  
    1.45  lemma Rep_convex_principal:
    1.46 -  "Rep_cset (Rep_convex_pd (convex_principal t)) = {u. u \<le>\<natural> t}"
    1.47 +  "Rep_convex_pd (convex_principal t) = {u. u \<le>\<natural> t}"
    1.48  unfolding convex_principal_def
    1.49  by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
    1.50  
    1.51  interpretation convex_pd:
    1.52 -  ideal_completion
    1.53 -    [convex_le approx_pd convex_principal "\<lambda>x. Rep_cset (Rep_convex_pd x)"]
    1.54 +  ideal_completion [convex_le approx_pd convex_principal Rep_convex_pd]
    1.55  apply unfold_locales
    1.56  apply (rule approx_pd_convex_le)
    1.57  apply (rule approx_pd_idem)
    1.58 @@ -168,9 +189,9 @@
    1.59  apply (rule finite_range_approx_pd)
    1.60  apply (rule approx_pd_covers)
    1.61  apply (rule ideal_Rep_convex_pd)
    1.62 -apply (simp add: cont2contlubE [OF cont_Rep_convex_pd] Rep_cset_lub)
    1.63 +apply (erule Rep_convex_pd_lub)
    1.64  apply (rule Rep_convex_principal)
    1.65 -apply (simp only: less_convex_pd_def sq_le_cset_def)
    1.66 +apply (simp only: sq_le_convex_pd_def)
    1.67  done
    1.68  
    1.69  text {* Convex powerdomain is pointed *}
    1.70 @@ -210,8 +231,7 @@
    1.71  by (rule convex_pd.completion_approx_principal)
    1.72  
    1.73  lemma approx_eq_convex_principal:
    1.74 -  "\<exists>t\<in>Rep_cset (Rep_convex_pd xs).
    1.75 -    approx n\<cdot>xs = convex_principal (approx_pd n t)"
    1.76 +  "\<exists>t\<in>Rep_convex_pd xs. approx n\<cdot>xs = convex_principal (approx_pd n t)"
    1.77  unfolding approx_convex_pd_def
    1.78  by (rule convex_pd.completion_approx_eq_principal)
    1.79