1.1 --- a/src/HOLCF/UpperPD.thy	Fri Jun 20 19:59:00 2008 +0200
     1.2 +++ b/src/HOLCF/UpperPD.thy	Fri Jun 20 20:03:13 2008 +0200
     1.3 @@ -95,27 +95,24 @@
     1.4  subsection {* Type definition *}
     1.5  
     1.6  cpodef (open) 'a upper_pd =
     1.7 -  "{S::'a::profinite pd_basis set. upper_le.ideal S}"
     1.8 -apply (simp add: upper_le.adm_ideal)
     1.9 -apply (fast intro: upper_le.ideal_principal)
    1.10 -done
    1.11 +  "{S::'a pd_basis cset. upper_le.ideal (Rep_cset S)}"
    1.12 +by (rule upper_le.cpodef_ideal_lemma)
    1.13  
    1.14 -lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd x)"
    1.15 +lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_cset (Rep_upper_pd xs))"
    1.16  by (rule Rep_upper_pd [unfolded mem_Collect_eq])
    1.17  
    1.18  definition
    1.19    upper_principal :: "'a pd_basis \<Rightarrow> 'a upper_pd" where
    1.20 -  "upper_principal t = Abs_upper_pd {u. u \<le>\<sharp> t}"
    1.21 +  "upper_principal t = Abs_upper_pd (Abs_cset {u. u \<le>\<sharp> t})"
    1.22  
    1.23  lemma Rep_upper_principal:
    1.24 -  "Rep_upper_pd (upper_principal t) = {u. u \<le>\<sharp> t}"
    1.25 +  "Rep_cset (Rep_upper_pd (upper_principal t)) = {u. u \<le>\<sharp> t}"
    1.26  unfolding upper_principal_def
    1.27 -apply (rule Abs_upper_pd_inverse [unfolded mem_Collect_eq])
    1.28 -apply (rule upper_le.ideal_principal)
    1.29 -done
    1.30 +by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal)
    1.31  
    1.32  interpretation upper_pd:
    1.33 -  ideal_completion [upper_le approx_pd upper_principal Rep_upper_pd]
    1.34 +  ideal_completion
    1.35 +    [upper_le approx_pd upper_principal "\<lambda>x. Rep_cset (Rep_upper_pd x)"]
    1.36  apply unfold_locales
    1.37  apply (rule approx_pd_upper_le)
    1.38  apply (rule approx_pd_idem)
    1.39 @@ -124,9 +121,9 @@
    1.40  apply (rule finite_range_approx_pd)
    1.41  apply (rule approx_pd_covers)
    1.42  apply (rule ideal_Rep_upper_pd)
    1.43 -apply (rule cont_Rep_upper_pd)
    1.44 +apply (simp add: cont2contlubE [OF cont_Rep_upper_pd] Rep_cset_lub)
    1.45  apply (rule Rep_upper_principal)
    1.46 -apply (simp only: less_upper_pd_def less_set_eq)
    1.47 +apply (simp only: less_upper_pd_def sq_le_cset_def)
    1.48  done
    1.49  
    1.50  text {* Upper powerdomain is pointed *}
    1.51 @@ -166,7 +163,8 @@
    1.52  by (rule upper_pd.completion_approx_principal)
    1.53  
    1.54  lemma approx_eq_upper_principal:
    1.55 -  "\<exists>t\<in>Rep_upper_pd xs. approx n\<cdot>xs = upper_principal (approx_pd n t)"
    1.56 +  "\<exists>t\<in>Rep_cset (Rep_upper_pd xs).
    1.57 +    approx n\<cdot>xs = upper_principal (approx_pd n t)"
    1.58  unfolding approx_upper_pd_def
    1.59  by (rule upper_pd.completion_approx_eq_principal)
    1.60