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