removed SetPcpo.thy and cpo instance for type bool;
authorhuffman
Fri Jun 20 20:03:13 2008 +0200 (2008-06-20)
changeset 272972c42b1505f25
parent 27296 eec7a1889ca5
child 27298 a5373b60e66c
removed SetPcpo.thy and cpo instance for type bool;
added Cset.thy with pcpo type 'a cset isomorphic to 'a set;
updated ideal completion theory to use cset
src/HOLCF/CompactBasis.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/Cset.thy
src/HOLCF/LowerPD.thy
src/HOLCF/SetPcpo.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOLCF/CompactBasis.thy	Fri Jun 20 19:59:00 2008 +0200
     1.2 +++ b/src/HOLCF/CompactBasis.thy	Fri Jun 20 20:03:13 2008 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Compact bases of domains *}
     1.5  
     1.6  theory CompactBasis
     1.7 -imports Bifinite SetPcpo
     1.8 +imports Bifinite Cset
     1.9  begin
    1.10  
    1.11  subsection {* Ideals over a preorder *}
    1.12 @@ -78,9 +78,16 @@
    1.13  apply (simp add: f)
    1.14  done
    1.15  
    1.16 -lemma adm_ideal: "adm (\<lambda>A. ideal A)"
    1.17 +lemma adm_ideal: "adm (\<lambda>A. ideal (Rep_cset A))"
    1.18  unfolding ideal_def by (intro adm_lemmas adm_set_lemmas)
    1.19  
    1.20 +lemma cpodef_ideal_lemma:
    1.21 +  "(\<exists>x. x \<in> {S. ideal (Rep_cset S)}) \<and> adm (\<lambda>x. x \<in> {S. ideal (Rep_cset S)})"
    1.22 +apply (simp add: adm_ideal)
    1.23 +apply (rule exI [where x="Abs_cset {x. x \<preceq> arbitrary}"])
    1.24 +apply (simp add: ideal_principal)
    1.25 +done
    1.26 +
    1.27  lemma lub_image_principal:
    1.28    assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
    1.29    shows "(\<Squnion>x\<in>{x. x \<preceq> y}. f x) = f y"
    1.30 @@ -150,7 +157,7 @@
    1.31    fixes principal :: "'a::type \<Rightarrow> 'b::cpo"
    1.32    fixes rep :: "'b::cpo \<Rightarrow> 'a::type set"
    1.33    assumes ideal_rep: "\<And>x. preorder.ideal r (rep x)"
    1.34 -  assumes cont_rep: "cont rep"
    1.35 +  assumes rep_contlub: "\<And>Y. chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))"
    1.36    assumes rep_principal: "\<And>a. rep (principal a) = {b. b \<preceq> a}"
    1.37    assumes subset_repD: "\<And>x y. rep x \<subseteq> rep y \<Longrightarrow> x \<sqsubseteq> y"
    1.38  begin
    1.39 @@ -216,14 +223,12 @@
    1.40  by (rule exI, rule basis_fun_lemma2, erule f_mono)
    1.41  
    1.42  lemma rep_mono: "x \<sqsubseteq> y \<Longrightarrow> rep x \<subseteq> rep y"
    1.43 -apply (drule cont_rep [THEN cont2mono, THEN monofunE])
    1.44 -apply (simp add: set_cpo_simps)
    1.45 +apply (frule bin_chain)
    1.46 +apply (drule rep_contlub)
    1.47 +apply (simp only: thelubI [OF lub_bin_chain])
    1.48 +apply (rule subsetI, rule UN_I [where a=0], simp_all)
    1.49  done
    1.50  
    1.51 -lemma rep_contlub:
    1.52 -  "chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))"
    1.53 -by (simp add: cont2contlubE [OF cont_rep] set_cpo_simps)
    1.54 -
    1.55  lemma less_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y"
    1.56  by (rule iffI [OF rep_mono subset_repD])
    1.57  
    1.58 @@ -537,16 +542,13 @@
    1.59        done
    1.60    qed
    1.61  next
    1.62 -  show "cont compacts"
    1.63 +  fix Y :: "nat \<Rightarrow> 'a"
    1.64 +  assume Y: "chain Y"
    1.65 +  show "compacts (\<Squnion>i. Y i) = (\<Union>i. compacts (Y i))"
    1.66      unfolding compacts_def
    1.67 -    apply (rule contI2)
    1.68 -    apply (rule monofunI)
    1.69 -    apply (simp add: set_cpo_simps)
    1.70 -    apply (fast intro: trans_less)
    1.71 -    apply (simp add: set_cpo_simps)
    1.72 -    apply clarify
    1.73 -    apply simp
    1.74 -    apply (erule (1) compactD2 [OF compact_Rep_compact_basis])
    1.75 +    apply safe
    1.76 +    apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
    1.77 +    apply (erule trans_less, rule is_ub_thelub [OF Y])
    1.78      done
    1.79  next
    1.80    fix a :: "'a compact_basis"
     2.1 --- a/src/HOLCF/ConvexPD.thy	Fri Jun 20 19:59:00 2008 +0200
     2.2 +++ b/src/HOLCF/ConvexPD.thy	Fri Jun 20 20:03:13 2008 +0200
     2.3 @@ -142,30 +142,24 @@
     2.4  subsection {* Type definition *}
     2.5  
     2.6  cpodef (open) 'a convex_pd =
     2.7 -  "{S::'a::profinite pd_basis set. convex_le.ideal S}"
     2.8 -apply (simp add: convex_le.adm_ideal)
     2.9 -apply (fast intro: convex_le.ideal_principal)
    2.10 -done
    2.11 +  "{S::'a pd_basis cset. convex_le.ideal (Rep_cset S)}"
    2.12 +by (rule convex_le.cpodef_ideal_lemma)
    2.13  
    2.14 -lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)"
    2.15 +lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_cset (Rep_convex_pd xs))"
    2.16  by (rule Rep_convex_pd [unfolded mem_Collect_eq])
    2.17  
    2.18 -lemma Rep_convex_pd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> Rep_convex_pd xs \<subseteq> Rep_convex_pd ys"
    2.19 -unfolding less_convex_pd_def less_set_eq .
    2.20 -
    2.21  definition
    2.22    convex_principal :: "'a pd_basis \<Rightarrow> 'a convex_pd" where
    2.23 -  "convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}"
    2.24 +  "convex_principal t = Abs_convex_pd (Abs_cset {u. u \<le>\<natural> t})"
    2.25  
    2.26  lemma Rep_convex_principal:
    2.27 -  "Rep_convex_pd (convex_principal t) = {u. u \<le>\<natural> t}"
    2.28 +  "Rep_cset (Rep_convex_pd (convex_principal t)) = {u. u \<le>\<natural> t}"
    2.29  unfolding convex_principal_def
    2.30 -apply (rule Abs_convex_pd_inverse [simplified])
    2.31 -apply (rule convex_le.ideal_principal)
    2.32 -done
    2.33 +by (simp add: Abs_convex_pd_inverse convex_le.ideal_principal)
    2.34  
    2.35  interpretation convex_pd:
    2.36 -  ideal_completion [convex_le approx_pd convex_principal Rep_convex_pd]
    2.37 +  ideal_completion
    2.38 +    [convex_le approx_pd convex_principal "\<lambda>x. Rep_cset (Rep_convex_pd x)"]
    2.39  apply unfold_locales
    2.40  apply (rule approx_pd_convex_le)
    2.41  apply (rule approx_pd_idem)
    2.42 @@ -174,9 +168,9 @@
    2.43  apply (rule finite_range_approx_pd)
    2.44  apply (rule approx_pd_covers)
    2.45  apply (rule ideal_Rep_convex_pd)
    2.46 -apply (rule cont_Rep_convex_pd)
    2.47 +apply (simp add: cont2contlubE [OF cont_Rep_convex_pd] Rep_cset_lub)
    2.48  apply (rule Rep_convex_principal)
    2.49 -apply (simp only: less_convex_pd_def less_set_eq)
    2.50 +apply (simp only: less_convex_pd_def sq_le_cset_def)
    2.51  done
    2.52  
    2.53  text {* Convex powerdomain is pointed *}
    2.54 @@ -216,7 +210,8 @@
    2.55  by (rule convex_pd.completion_approx_principal)
    2.56  
    2.57  lemma approx_eq_convex_principal:
    2.58 -  "\<exists>t\<in>Rep_convex_pd xs. approx n\<cdot>xs = convex_principal (approx_pd n t)"
    2.59 +  "\<exists>t\<in>Rep_cset (Rep_convex_pd xs).
    2.60 +    approx n\<cdot>xs = convex_principal (approx_pd n t)"
    2.61  unfolding approx_convex_pd_def
    2.62  by (rule convex_pd.completion_approx_eq_principal)
    2.63  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOLCF/Cset.thy	Fri Jun 20 20:03:13 2008 +0200
     3.3 @@ -0,0 +1,117 @@
     3.4 +(*  Title:      HOLCF/Cset.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Brian Huffman
     3.7 +*)
     3.8 +
     3.9 +header {* Set as a pointed cpo *}
    3.10 +
    3.11 +theory Cset
    3.12 +imports Adm
    3.13 +begin
    3.14 +
    3.15 +subsection {* Type definition *}
    3.16 +
    3.17 +defaultsort type
    3.18 +
    3.19 +typedef (open) 'a cset = "UNIV :: 'a set set" ..
    3.20 +
    3.21 +declare Rep_cset_inverse [simp]
    3.22 +declare Abs_cset_inverse [simplified, simp]
    3.23 +
    3.24 +instantiation cset :: (type) po
    3.25 +begin
    3.26 +
    3.27 +definition
    3.28 +  sq_le_cset_def:
    3.29 +    "x \<sqsubseteq> y \<longleftrightarrow> Rep_cset x \<subseteq> Rep_cset y"
    3.30 +
    3.31 +instance proof
    3.32 +  fix x :: "'a cset"
    3.33 +  show "x \<sqsubseteq> x"
    3.34 +    unfolding sq_le_cset_def
    3.35 +    by (rule subset_refl)
    3.36 +next
    3.37 +  fix x y z :: "'a cset"
    3.38 +  assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
    3.39 +    unfolding sq_le_cset_def
    3.40 +    by (rule subset_trans)
    3.41 +next
    3.42 +  fix x y :: "'a cset"
    3.43 +  assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
    3.44 +    unfolding sq_le_cset_def Rep_cset_inject [symmetric]
    3.45 +    by (rule subset_antisym)
    3.46 +qed
    3.47 +
    3.48 +end
    3.49 +
    3.50 +lemma is_lub_UNION: "A <<| Abs_cset (UNION A Rep_cset)"
    3.51 +unfolding is_lub_def is_ub_def sq_le_cset_def by auto
    3.52 +
    3.53 +instance cset :: (type) cpo
    3.54 +proof
    3.55 +  fix S :: "nat \<Rightarrow> 'a cset"
    3.56 +  show "\<exists>x. range S <<| x"
    3.57 +    by (fast intro: is_lub_UNION)
    3.58 +qed
    3.59 +
    3.60 +lemma lub_cset: "lub A = Abs_cset (UNION A Rep_cset)"
    3.61 +by (rule thelubI [OF is_lub_UNION])
    3.62 +
    3.63 +lemma Rep_cset_lub: "Rep_cset (lub A) = UNION A Rep_cset"
    3.64 +by (simp add: lub_cset)
    3.65 +
    3.66 +text {* cset is pointed *}
    3.67 +
    3.68 +lemma cset_minimal: "Abs_cset {} \<sqsubseteq> x"
    3.69 +unfolding sq_le_cset_def by simp
    3.70 +
    3.71 +instance cset :: (type) pcpo
    3.72 +by intro_classes (fast intro: cset_minimal)
    3.73 +
    3.74 +lemma inst_cset_pcpo: "\<bottom> = Abs_cset {}"
    3.75 +by (rule cset_minimal [THEN UU_I, symmetric])
    3.76 +
    3.77 +lemma Rep_cset_UU: "Rep_cset \<bottom> = {}"
    3.78 +unfolding inst_cset_pcpo by simp
    3.79 +
    3.80 +lemmas Rep_cset_simps = Rep_cset_lub Rep_cset_UU
    3.81 +
    3.82 +subsection {* Admissibility of set predicates *}
    3.83 +
    3.84 +lemma adm_nonempty: "adm (\<lambda>A. \<exists>x. x \<in> Rep_cset A)"
    3.85 +by (rule admI, simp add: Rep_cset_lub, fast)
    3.86 +
    3.87 +lemma adm_in: "adm (\<lambda>A. x \<in> Rep_cset A)"
    3.88 +by (rule admI, simp add: Rep_cset_lub)
    3.89 +
    3.90 +lemma adm_not_in: "adm (\<lambda>A. x \<notin> Rep_cset A)"
    3.91 +by (rule admI, simp add: Rep_cset_lub)
    3.92 +
    3.93 +lemma adm_Ball: "(\<And>x. adm (\<lambda>A. P A x)) \<Longrightarrow> adm (\<lambda>A. \<forall>x\<in>Rep_cset A. P A x)"
    3.94 +unfolding Ball_def by (simp add: adm_not_in)
    3.95 +
    3.96 +lemma adm_Bex: "adm (\<lambda>A. \<exists>x\<in>Rep_cset A. P x)"
    3.97 +by (rule admI, simp add: Rep_cset_lub)
    3.98 +
    3.99 +lemma adm_subset: "adm (\<lambda>A. Rep_cset A \<subseteq> B)"
   3.100 +by (rule admI, auto simp add: Rep_cset_lub)
   3.101 +
   3.102 +lemma adm_superset: "adm (\<lambda>A. B \<subseteq> Rep_cset A)"
   3.103 +by (rule admI, auto simp add: Rep_cset_lub)
   3.104 +
   3.105 +lemmas adm_set_lemmas =
   3.106 +  adm_nonempty adm_in adm_not_in adm_Bex adm_Ball adm_subset adm_superset
   3.107 +
   3.108 +subsection {* Compactness *}
   3.109 +
   3.110 +lemma compact_empty: "compact (Abs_cset {})"
   3.111 +by (fold inst_cset_pcpo, simp)
   3.112 +
   3.113 +lemma compact_insert: "compact (Abs_cset A) \<Longrightarrow> compact (Abs_cset (insert x A))"
   3.114 +unfolding compact_def sq_le_cset_def
   3.115 +by (simp add: adm_set_lemmas)
   3.116 +
   3.117 +lemma finite_imp_compact: "finite A \<Longrightarrow> compact (Abs_cset A)"
   3.118 +by (induct A set: finite, rule compact_empty, erule compact_insert)
   3.119 +
   3.120 +end
     4.1 --- a/src/HOLCF/LowerPD.thy	Fri Jun 20 19:59:00 2008 +0200
     4.2 +++ b/src/HOLCF/LowerPD.thy	Fri Jun 20 20:03:13 2008 +0200
     4.3 @@ -97,27 +97,24 @@
     4.4  subsection {* Type definition *}
     4.5  
     4.6  cpodef (open) 'a lower_pd =
     4.7 -  "{S::'a::profinite pd_basis set. lower_le.ideal S}"
     4.8 -apply (simp add: lower_le.adm_ideal)
     4.9 -apply (fast intro: lower_le.ideal_principal)
    4.10 -done
    4.11 +  "{S::'a pd_basis cset. lower_le.ideal (Rep_cset S)}"
    4.12 +by (rule lower_le.cpodef_ideal_lemma)
    4.13  
    4.14 -lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd x)"
    4.15 +lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_cset (Rep_lower_pd xs))"
    4.16  by (rule Rep_lower_pd [unfolded mem_Collect_eq])
    4.17  
    4.18  definition
    4.19    lower_principal :: "'a pd_basis \<Rightarrow> 'a lower_pd" where
    4.20 -  "lower_principal t = Abs_lower_pd {u. u \<le>\<flat> t}"
    4.21 +  "lower_principal t = Abs_lower_pd (Abs_cset {u. u \<le>\<flat> t})"
    4.22  
    4.23  lemma Rep_lower_principal:
    4.24 -  "Rep_lower_pd (lower_principal t) = {u. u \<le>\<flat> t}"
    4.25 +  "Rep_cset (Rep_lower_pd (lower_principal t)) = {u. u \<le>\<flat> t}"
    4.26  unfolding lower_principal_def
    4.27 -apply (rule Abs_lower_pd_inverse [simplified])
    4.28 -apply (rule lower_le.ideal_principal)
    4.29 -done
    4.30 +by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal)
    4.31  
    4.32  interpretation lower_pd:
    4.33 -  ideal_completion [lower_le approx_pd lower_principal Rep_lower_pd]
    4.34 +  ideal_completion
    4.35 +    [lower_le approx_pd lower_principal "\<lambda>x. Rep_cset (Rep_lower_pd x)"]
    4.36  apply unfold_locales
    4.37  apply (rule approx_pd_lower_le)
    4.38  apply (rule approx_pd_idem)
    4.39 @@ -126,9 +123,9 @@
    4.40  apply (rule finite_range_approx_pd)
    4.41  apply (rule approx_pd_covers)
    4.42  apply (rule ideal_Rep_lower_pd)
    4.43 -apply (rule cont_Rep_lower_pd)
    4.44 +apply (simp add: cont2contlubE [OF cont_Rep_lower_pd] Rep_cset_lub)
    4.45  apply (rule Rep_lower_principal)
    4.46 -apply (simp only: less_lower_pd_def less_set_eq)
    4.47 +apply (simp only: less_lower_pd_def sq_le_cset_def)
    4.48  done
    4.49  
    4.50  text {* Lower powerdomain is pointed *}
    4.51 @@ -168,7 +165,8 @@
    4.52  by (rule lower_pd.completion_approx_principal)
    4.53  
    4.54  lemma approx_eq_lower_principal:
    4.55 -  "\<exists>t\<in>Rep_lower_pd xs. approx n\<cdot>xs = lower_principal (approx_pd n t)"
    4.56 +  "\<exists>t\<in>Rep_cset (Rep_lower_pd xs).
    4.57 +    approx n\<cdot>xs = lower_principal (approx_pd n t)"
    4.58  unfolding approx_lower_pd_def
    4.59  by (rule lower_pd.completion_approx_eq_principal)
    4.60  
     5.1 --- a/src/HOLCF/SetPcpo.thy	Fri Jun 20 19:59:00 2008 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,85 +0,0 @@
     5.4 -(*  Title:      HOLCF/SetPcpo.thy
     5.5 -    ID:         $Id$
     5.6 -    Author:     Brian Huffman
     5.7 -*)
     5.8 -
     5.9 -header {* Set as a pointed cpo *}
    5.10 -
    5.11 -theory SetPcpo
    5.12 -imports Adm Ffun
    5.13 -begin
    5.14 -
    5.15 -instantiation bool :: po
    5.16 -begin
    5.17 -
    5.18 -definition
    5.19 -  less_bool_def: "(op \<sqsubseteq>) = (op \<longrightarrow>)"
    5.20 -
    5.21 -instance
    5.22 -by (intro_classes, unfold less_bool_def, safe)
    5.23 -
    5.24 -end
    5.25 -
    5.26 -lemma less_set_eq: "(op \<sqsubseteq>) = (op \<subseteq>)"
    5.27 -  by (simp add: less_fun_def less_bool_def le_fun_def le_bool_def expand_fun_eq)
    5.28 -
    5.29 -instance bool :: finite_po ..
    5.30 -
    5.31 -lemma Union_is_lub: "A <<| Union A"
    5.32 -unfolding is_lub_def is_ub_def less_set_eq by fast
    5.33 -
    5.34 -instance bool :: cpo ..
    5.35 -
    5.36 -lemma lub_eq_Union: "lub = Union"
    5.37 -by (rule ext, rule thelubI [OF Union_is_lub])
    5.38 -
    5.39 -instance bool :: pcpo
    5.40 -proof
    5.41 -  have "\<forall>y::bool. False \<sqsubseteq> y" unfolding less_bool_def by simp
    5.42 -  thus "\<exists>x::bool. \<forall>y. x \<sqsubseteq> y" ..
    5.43 -qed
    5.44 -
    5.45 -lemma UU_eq_empty: "\<bottom> = {}"
    5.46 -by (rule UU_I [symmetric], simp add: less_set_eq)
    5.47 -
    5.48 -lemmas set_cpo_simps = less_set_eq lub_eq_Union UU_eq_empty
    5.49 -
    5.50 -subsection {* Admissibility of set predicates *}
    5.51 -
    5.52 -lemma adm_nonempty: "adm (\<lambda>A. \<exists>x. x \<in> A)"
    5.53 -by (rule admI, force simp add: lub_eq_Union)
    5.54 -
    5.55 -lemma adm_in: "adm (\<lambda>A. x \<in> A)"
    5.56 -by (rule admI, simp add: lub_eq_Union)
    5.57 -
    5.58 -lemma adm_not_in: "adm (\<lambda>A. x \<notin> A)"
    5.59 -by (rule admI, simp add: lub_eq_Union)
    5.60 -
    5.61 -lemma adm_Ball: "(\<And>x. adm (\<lambda>A. P A x)) \<Longrightarrow> adm (\<lambda>A. \<forall>x\<in>A. P A x)"
    5.62 -unfolding Ball_def by (simp add: adm_not_in)
    5.63 -
    5.64 -lemma adm_Bex: "adm (\<lambda>A. Bex A P)"
    5.65 -by (rule admI, simp add: lub_eq_Union)
    5.66 -
    5.67 -lemma adm_subset: "adm (\<lambda>A. A \<subseteq> B)"
    5.68 -by (rule admI, auto simp add: lub_eq_Union)
    5.69 -
    5.70 -lemma adm_superset: "adm (\<lambda>A. B \<subseteq> A)"
    5.71 -by (rule admI, auto simp add: lub_eq_Union)
    5.72 -
    5.73 -lemmas adm_set_lemmas =
    5.74 -  adm_nonempty adm_in adm_not_in adm_Bex adm_Ball adm_subset adm_superset
    5.75 -
    5.76 -subsection {* Compactness *}
    5.77 -
    5.78 -lemma compact_empty: "compact {}"
    5.79 -by (fold UU_eq_empty, simp)
    5.80 -
    5.81 -lemma compact_insert: "compact A \<Longrightarrow> compact (insert x A)"
    5.82 -unfolding compact_def set_cpo_simps
    5.83 -by (simp add: adm_set_lemmas)
    5.84 -
    5.85 -lemma finite_imp_compact: "finite A \<Longrightarrow> compact A"
    5.86 -by (induct A set: finite, rule compact_empty, erule compact_insert)
    5.87 -
    5.88 -end
     6.1 --- a/src/HOLCF/UpperPD.thy	Fri Jun 20 19:59:00 2008 +0200
     6.2 +++ b/src/HOLCF/UpperPD.thy	Fri Jun 20 20:03:13 2008 +0200
     6.3 @@ -95,27 +95,24 @@
     6.4  subsection {* Type definition *}
     6.5  
     6.6  cpodef (open) 'a upper_pd =
     6.7 -  "{S::'a::profinite pd_basis set. upper_le.ideal S}"
     6.8 -apply (simp add: upper_le.adm_ideal)
     6.9 -apply (fast intro: upper_le.ideal_principal)
    6.10 -done
    6.11 +  "{S::'a pd_basis cset. upper_le.ideal (Rep_cset S)}"
    6.12 +by (rule upper_le.cpodef_ideal_lemma)
    6.13  
    6.14 -lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd x)"
    6.15 +lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_cset (Rep_upper_pd xs))"
    6.16  by (rule Rep_upper_pd [unfolded mem_Collect_eq])
    6.17  
    6.18  definition
    6.19    upper_principal :: "'a pd_basis \<Rightarrow> 'a upper_pd" where
    6.20 -  "upper_principal t = Abs_upper_pd {u. u \<le>\<sharp> t}"
    6.21 +  "upper_principal t = Abs_upper_pd (Abs_cset {u. u \<le>\<sharp> t})"
    6.22  
    6.23  lemma Rep_upper_principal:
    6.24 -  "Rep_upper_pd (upper_principal t) = {u. u \<le>\<sharp> t}"
    6.25 +  "Rep_cset (Rep_upper_pd (upper_principal t)) = {u. u \<le>\<sharp> t}"
    6.26  unfolding upper_principal_def
    6.27 -apply (rule Abs_upper_pd_inverse [unfolded mem_Collect_eq])
    6.28 -apply (rule upper_le.ideal_principal)
    6.29 -done
    6.30 +by (simp add: Abs_upper_pd_inverse upper_le.ideal_principal)
    6.31  
    6.32  interpretation upper_pd:
    6.33 -  ideal_completion [upper_le approx_pd upper_principal Rep_upper_pd]
    6.34 +  ideal_completion
    6.35 +    [upper_le approx_pd upper_principal "\<lambda>x. Rep_cset (Rep_upper_pd x)"]
    6.36  apply unfold_locales
    6.37  apply (rule approx_pd_upper_le)
    6.38  apply (rule approx_pd_idem)
    6.39 @@ -124,9 +121,9 @@
    6.40  apply (rule finite_range_approx_pd)
    6.41  apply (rule approx_pd_covers)
    6.42  apply (rule ideal_Rep_upper_pd)
    6.43 -apply (rule cont_Rep_upper_pd)
    6.44 +apply (simp add: cont2contlubE [OF cont_Rep_upper_pd] Rep_cset_lub)
    6.45  apply (rule Rep_upper_principal)
    6.46 -apply (simp only: less_upper_pd_def less_set_eq)
    6.47 +apply (simp only: less_upper_pd_def sq_le_cset_def)
    6.48  done
    6.49  
    6.50  text {* Upper powerdomain is pointed *}
    6.51 @@ -166,7 +163,8 @@
    6.52  by (rule upper_pd.completion_approx_principal)
    6.53  
    6.54  lemma approx_eq_upper_principal:
    6.55 -  "\<exists>t\<in>Rep_upper_pd xs. approx n\<cdot>xs = upper_principal (approx_pd n t)"
    6.56 +  "\<exists>t\<in>Rep_cset (Rep_upper_pd xs).
    6.57 +    approx n\<cdot>xs = upper_principal (approx_pd n t)"
    6.58  unfolding approx_upper_pd_def
    6.59  by (rule upper_pd.completion_approx_eq_principal)
    6.60