src/HOLCF/LowerPD.thy
changeset 27297 2c42b1505f25
parent 27289 c49d427867aa
child 27309 c74270fd72a8
     1.1 --- a/src/HOLCF/LowerPD.thy	Fri Jun 20 19:59:00 2008 +0200
     1.2 +++ b/src/HOLCF/LowerPD.thy	Fri Jun 20 20:03:13 2008 +0200
     1.3 @@ -97,27 +97,24 @@
     1.4  subsection {* Type definition *}
     1.5  
     1.6  cpodef (open) 'a lower_pd =
     1.7 -  "{S::'a::profinite pd_basis set. lower_le.ideal S}"
     1.8 -apply (simp add: lower_le.adm_ideal)
     1.9 -apply (fast intro: lower_le.ideal_principal)
    1.10 -done
    1.11 +  "{S::'a pd_basis cset. lower_le.ideal (Rep_cset S)}"
    1.12 +by (rule lower_le.cpodef_ideal_lemma)
    1.13  
    1.14 -lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd x)"
    1.15 +lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_cset (Rep_lower_pd xs))"
    1.16  by (rule Rep_lower_pd [unfolded mem_Collect_eq])
    1.17  
    1.18  definition
    1.19    lower_principal :: "'a pd_basis \<Rightarrow> 'a lower_pd" where
    1.20 -  "lower_principal t = Abs_lower_pd {u. u \<le>\<flat> t}"
    1.21 +  "lower_principal t = Abs_lower_pd (Abs_cset {u. u \<le>\<flat> t})"
    1.22  
    1.23  lemma Rep_lower_principal:
    1.24 -  "Rep_lower_pd (lower_principal t) = {u. u \<le>\<flat> t}"
    1.25 +  "Rep_cset (Rep_lower_pd (lower_principal t)) = {u. u \<le>\<flat> t}"
    1.26  unfolding lower_principal_def
    1.27 -apply (rule Abs_lower_pd_inverse [simplified])
    1.28 -apply (rule lower_le.ideal_principal)
    1.29 -done
    1.30 +by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal)
    1.31  
    1.32  interpretation lower_pd:
    1.33 -  ideal_completion [lower_le approx_pd lower_principal Rep_lower_pd]
    1.34 +  ideal_completion
    1.35 +    [lower_le approx_pd lower_principal "\<lambda>x. Rep_cset (Rep_lower_pd x)"]
    1.36  apply unfold_locales
    1.37  apply (rule approx_pd_lower_le)
    1.38  apply (rule approx_pd_idem)
    1.39 @@ -126,9 +123,9 @@
    1.40  apply (rule finite_range_approx_pd)
    1.41  apply (rule approx_pd_covers)
    1.42  apply (rule ideal_Rep_lower_pd)
    1.43 -apply (rule cont_Rep_lower_pd)
    1.44 +apply (simp add: cont2contlubE [OF cont_Rep_lower_pd] Rep_cset_lub)
    1.45  apply (rule Rep_lower_principal)
    1.46 -apply (simp only: less_lower_pd_def less_set_eq)
    1.47 +apply (simp only: less_lower_pd_def sq_le_cset_def)
    1.48  done
    1.49  
    1.50  text {* Lower powerdomain is pointed *}
    1.51 @@ -168,7 +165,8 @@
    1.52  by (rule lower_pd.completion_approx_principal)
    1.53  
    1.54  lemma approx_eq_lower_principal:
    1.55 -  "\<exists>t\<in>Rep_lower_pd xs. approx n\<cdot>xs = lower_principal (approx_pd n t)"
    1.56 +  "\<exists>t\<in>Rep_cset (Rep_lower_pd xs).
    1.57 +    approx n\<cdot>xs = lower_principal (approx_pd n t)"
    1.58  unfolding approx_lower_pd_def
    1.59  by (rule lower_pd.completion_approx_eq_principal)
    1.60