rename locales;
authorhuffman
Fri May 16 23:25:37 2008 +0200 (2008-05-16)
changeset 269278684b5240f11
parent 26926 19d8783a30de
child 26928 ca87aff1ad2d
rename locales;
add completion_approx constant to ideal_completion locale;
add new set-like syntax for powerdomains;
reorganized proofs
src/HOLCF/CompactBasis.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/LowerPD.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOLCF/CompactBasis.thy	Fri May 16 22:35:25 2008 +0200
     1.2 +++ b/src/HOLCF/CompactBasis.thy	Fri May 16 23:25:37 2008 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4  lemma ideal_principal: "ideal {x. x \<sqsubseteq> z}"
     1.5  apply (rule idealI)
     1.6  apply (rule_tac x=z in exI)
     1.7 -apply (fast intro: refl)
     1.8 +apply fast
     1.9  apply (rule_tac x=z in bexI, fast)
    1.10  apply fast
    1.11  apply (fast intro: trans_less)
    1.12 @@ -116,7 +116,7 @@
    1.13  lemma is_lub_thelub0: "\<lbrakk>\<exists>u. S <<| u; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> x"
    1.14  by (erule exE, drule lubI, erule is_lub_lub)
    1.15  
    1.16 -locale plotkin_order = preorder r +
    1.17 +locale basis_take = preorder r +
    1.18    fixes take :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'a"
    1.19    assumes take_less: "r (take n a) a"
    1.20    assumes take_take: "take n (take n a) = take n a"
    1.21 @@ -125,28 +125,28 @@
    1.22    assumes finite_range_take: "finite (range (take n))"
    1.23    assumes take_covers: "\<exists>n. take n a = a"
    1.24  
    1.25 -locale bifinite_basis = plotkin_order r +
    1.26 +locale ideal_completion = basis_take r +
    1.27    fixes principal :: "'a::type \<Rightarrow> 'b::cpo"
    1.28 -  fixes approxes :: "'b::cpo \<Rightarrow> 'a::type set"
    1.29 -  assumes ideal_approxes: "\<And>x. preorder.ideal r (approxes x)"
    1.30 -  assumes cont_approxes: "cont approxes"
    1.31 -  assumes approxes_principal: "\<And>a. approxes (principal a) = {b. r b a}"
    1.32 -  assumes subset_approxesD: "\<And>x y. approxes x \<subseteq> approxes y \<Longrightarrow> x \<sqsubseteq> y"
    1.33 +  fixes rep :: "'b::cpo \<Rightarrow> 'a::type set"
    1.34 +  assumes ideal_rep: "\<And>x. preorder.ideal r (rep x)"
    1.35 +  assumes cont_rep: "cont rep"
    1.36 +  assumes rep_principal: "\<And>a. rep (principal a) = {b. r b a}"
    1.37 +  assumes subset_repD: "\<And>x y. rep x \<subseteq> rep y \<Longrightarrow> x \<sqsubseteq> y"
    1.38  begin
    1.39  
    1.40 -lemma finite_take_approxes: "finite (take n ` approxes x)"
    1.41 +lemma finite_take_rep: "finite (take n ` rep x)"
    1.42  by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range_take])
    1.43  
    1.44  lemma basis_fun_lemma0:
    1.45    fixes f :: "'a::type \<Rightarrow> 'c::cpo"
    1.46    assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
    1.47 -  shows "\<exists>u. f ` take i ` approxes x <<| u"
    1.48 +  shows "\<exists>u. f ` take i ` rep x <<| u"
    1.49  apply (rule finite_directed_has_lub)
    1.50  apply (rule finite_imageI)
    1.51 -apply (rule finite_take_approxes)
    1.52 +apply (rule finite_take_rep)
    1.53  apply (subst image_image)
    1.54  apply (rule directed_image_ideal)
    1.55 -apply (rule ideal_approxes)
    1.56 +apply (rule ideal_rep)
    1.57  apply (rule f_mono)
    1.58  apply (erule take_mono)
    1.59  done
    1.60 @@ -154,7 +154,7 @@
    1.61  lemma basis_fun_lemma1:
    1.62    fixes f :: "'a::type \<Rightarrow> 'c::cpo"
    1.63    assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
    1.64 -  shows "chain (\<lambda>i. lub (f ` take i ` approxes x))"
    1.65 +  shows "chain (\<lambda>i. lub (f ` take i ` rep x))"
    1.66   apply (rule chainI)
    1.67   apply (rule is_lub_thelub0)
    1.68    apply (rule basis_fun_lemma0, erule f_mono)
    1.69 @@ -168,7 +168,7 @@
    1.70  lemma basis_fun_lemma2:
    1.71    fixes f :: "'a::type \<Rightarrow> 'c::cpo"
    1.72    assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
    1.73 -  shows "f ` approxes x <<| (\<Squnion>i. lub (f ` take i ` approxes x))"
    1.74 +  shows "f ` rep x <<| (\<Squnion>i. lub (f ` take i ` rep x))"
    1.75   apply (rule is_lubI)
    1.76   apply (rule ub_imageI, rename_tac a)
    1.77    apply (cut_tac a=a in take_covers, erule exE, rename_tac i)
    1.78 @@ -191,74 +191,80 @@
    1.79  lemma basis_fun_lemma:
    1.80    fixes f :: "'a::type \<Rightarrow> 'c::cpo"
    1.81    assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
    1.82 -  shows "\<exists>u. f ` approxes x <<| u"
    1.83 +  shows "\<exists>u. f ` rep x <<| u"
    1.84  by (rule exI, rule basis_fun_lemma2, erule f_mono)
    1.85  
    1.86 -lemma approxes_mono: "x \<sqsubseteq> y \<Longrightarrow> approxes x \<subseteq> approxes y"
    1.87 -apply (drule cont_approxes [THEN cont2mono, THEN monofunE])
    1.88 +lemma rep_mono: "x \<sqsubseteq> y \<Longrightarrow> rep x \<subseteq> rep y"
    1.89 +apply (drule cont_rep [THEN cont2mono, THEN monofunE])
    1.90  apply (simp add: set_cpo_simps)
    1.91  done
    1.92  
    1.93 -lemma approxes_contlub:
    1.94 -  "chain Y \<Longrightarrow> approxes (\<Squnion>i. Y i) = (\<Union>i. approxes (Y i))"
    1.95 -by (simp add: cont2contlubE [OF cont_approxes] set_cpo_simps)
    1.96 +lemma rep_contlub:
    1.97 +  "chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))"
    1.98 +by (simp add: cont2contlubE [OF cont_rep] set_cpo_simps)
    1.99  
   1.100 -lemma less_def: "(x \<sqsubseteq> y) = (approxes x \<subseteq> approxes y)"
   1.101 -by (rule iffI [OF approxes_mono subset_approxesD])
   1.102 +lemma less_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y"
   1.103 +by (rule iffI [OF rep_mono subset_repD])
   1.104  
   1.105 -lemma approxes_eq: "approxes x = {a. principal a \<sqsubseteq> x}"
   1.106 -unfolding less_def approxes_principal
   1.107 +lemma rep_eq: "rep x = {a. principal a \<sqsubseteq> x}"
   1.108 +unfolding less_def rep_principal
   1.109  apply safe
   1.110 -apply (erule (1) idealD3 [OF ideal_approxes])
   1.111 +apply (erule (1) idealD3 [OF ideal_rep])
   1.112  apply (erule subsetD, simp add: refl)
   1.113  done
   1.114  
   1.115 -lemma mem_approxes_iff: "(a \<in> approxes x) = (principal a \<sqsubseteq> x)"
   1.116 -by (simp add: approxes_eq)
   1.117 +lemma mem_rep_iff_principal_less: "a \<in> rep x \<longleftrightarrow> principal a \<sqsubseteq> x"
   1.118 +by (simp add: rep_eq)
   1.119 +
   1.120 +lemma principal_less_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x"
   1.121 +by (simp add: rep_eq)
   1.122  
   1.123 -lemma principal_less_iff: "(principal a \<sqsubseteq> x) = (a \<in> approxes x)"
   1.124 -by (simp add: approxes_eq)
   1.125 +lemma principal_less_iff: "principal a \<sqsubseteq> principal b \<longleftrightarrow> r a b"
   1.126 +by (simp add: principal_less_iff_mem_rep rep_principal)
   1.127  
   1.128 -lemma approxesD: "a \<in> approxes x \<Longrightarrow> principal a \<sqsubseteq> x"
   1.129 -by (simp add: approxes_eq)
   1.130 +lemma principal_eq_iff: "principal a = principal b \<longleftrightarrow> r a b \<and> r b a"
   1.131 +unfolding po_eq_conv [where 'a='b] principal_less_iff ..
   1.132 +
   1.133 +lemma repD: "a \<in> rep x \<Longrightarrow> principal a \<sqsubseteq> x"
   1.134 +by (simp add: rep_eq)
   1.135  
   1.136  lemma principal_mono: "r a b \<Longrightarrow> principal a \<sqsubseteq> principal b"
   1.137 -by (rule approxesD, simp add: approxes_principal)
   1.138 +by (simp add: principal_less_iff)
   1.139  
   1.140  lemma lessI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
   1.141 -unfolding principal_less_iff
   1.142 +unfolding principal_less_iff_mem_rep
   1.143  by (simp add: less_def subset_eq)
   1.144  
   1.145 -lemma lub_principal_approxes: "principal ` approxes x <<| x"
   1.146 +lemma lub_principal_rep: "principal ` rep x <<| x"
   1.147  apply (rule is_lubI)
   1.148  apply (rule ub_imageI)
   1.149 -apply (erule approxesD)
   1.150 +apply (erule repD)
   1.151  apply (subst less_def)
   1.152  apply (rule subsetI)
   1.153  apply (drule (1) ub_imageD)
   1.154 -apply (simp add: approxes_eq)
   1.155 +apply (simp add: rep_eq)
   1.156  done
   1.157  
   1.158  definition
   1.159    basis_fun :: "('a::type \<Rightarrow> 'c::cpo) \<Rightarrow> 'b \<rightarrow> 'c" where
   1.160 -  "basis_fun = (\<lambda>f. (\<Lambda> x. lub (f ` approxes x)))"
   1.161 +  "basis_fun = (\<lambda>f. (\<Lambda> x. lub (f ` rep x)))"
   1.162  
   1.163  lemma basis_fun_beta:
   1.164    fixes f :: "'a::type \<Rightarrow> 'c::cpo"
   1.165    assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
   1.166 -  shows "basis_fun f\<cdot>x = lub (f ` approxes x)"
   1.167 +  shows "basis_fun f\<cdot>x = lub (f ` rep x)"
   1.168  unfolding basis_fun_def
   1.169  proof (rule beta_cfun)
   1.170 -  have lub: "\<And>x. \<exists>u. f ` approxes x <<| u"
   1.171 +  have lub: "\<And>x. \<exists>u. f ` rep x <<| u"
   1.172      using f_mono by (rule basis_fun_lemma)
   1.173 -  show cont: "cont (\<lambda>x. lub (f ` approxes x))"
   1.174 +  show cont: "cont (\<lambda>x. lub (f ` rep x))"
   1.175      apply (rule contI2)
   1.176       apply (rule monofunI)
   1.177       apply (rule is_lub_thelub0 [OF lub ub_imageI])
   1.178       apply (rule is_ub_thelub0 [OF lub imageI])
   1.179 -     apply (erule (1) subsetD [OF approxes_mono])
   1.180 +     apply (erule (1) subsetD [OF rep_mono])
   1.181      apply (rule is_lub_thelub0 [OF lub ub_imageI])
   1.182 -    apply (simp add: approxes_contlub, clarify)
   1.183 +    apply (simp add: rep_contlub, clarify)
   1.184      apply (erule rev_trans_less [OF is_ub_thelub])
   1.185      apply (erule is_ub_thelub0 [OF lub imageI])
   1.186      done
   1.187 @@ -269,7 +275,7 @@
   1.188    assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
   1.189    shows "basis_fun f\<cdot>(principal a) = f a"
   1.190  apply (subst basis_fun_beta, erule f_mono)
   1.191 -apply (subst approxes_principal)
   1.192 +apply (subst rep_principal)
   1.193  apply (rule lub_image_principal, erule f_mono)
   1.194  done
   1.195  
   1.196 @@ -290,10 +296,24 @@
   1.197  done
   1.198  
   1.199  lemma compact_principal: "compact (principal a)"
   1.200 -by (rule compactI2, simp add: principal_less_iff approxes_contlub)
   1.201 +by (rule compactI2, simp add: principal_less_iff_mem_rep rep_contlub)
   1.202 +
   1.203 +definition
   1.204 +  completion_approx :: "nat \<Rightarrow> 'b \<rightarrow> 'b" where
   1.205 +  "completion_approx = (\<lambda>i. basis_fun (\<lambda>a. principal (take i a)))"
   1.206  
   1.207 -lemma chain_basis_fun_take:
   1.208 -  "chain (\<lambda>i. basis_fun (\<lambda>a. principal (take i a)))"
   1.209 +lemma completion_approx_beta:
   1.210 +  "completion_approx i\<cdot>x = (\<Squnion>a\<in>rep x. principal (take i a))"
   1.211 +unfolding completion_approx_def
   1.212 +by (simp add: basis_fun_beta principal_mono take_mono)
   1.213 +
   1.214 +lemma completion_approx_principal:
   1.215 +  "completion_approx i\<cdot>(principal a) = principal (take i a)"
   1.216 +unfolding completion_approx_def
   1.217 +by (simp add: basis_fun_principal principal_mono take_mono)
   1.218 +
   1.219 +lemma chain_completion_approx: "chain completion_approx"
   1.220 +unfolding completion_approx_def
   1.221  apply (rule chainI)
   1.222  apply (rule basis_fun_mono)
   1.223  apply (erule principal_mono [OF take_mono])
   1.224 @@ -301,53 +321,56 @@
   1.225  apply (rule principal_mono [OF take_chain])
   1.226  done
   1.227  
   1.228 -lemma lub_basis_fun_take:
   1.229 -  "(\<Squnion>i. basis_fun (\<lambda>a. principal (take i a))\<cdot>x) = x"
   1.230 - apply (simp add: basis_fun_beta principal_mono take_mono)
   1.231 +lemma lub_completion_approx: "(\<Squnion>i. completion_approx i\<cdot>x) = x"
   1.232 +unfolding completion_approx_beta
   1.233   apply (subst image_image [where f=principal, symmetric])
   1.234 - apply (rule unique_lub [OF _ lub_principal_approxes])
   1.235 + apply (rule unique_lub [OF _ lub_principal_rep])
   1.236   apply (rule basis_fun_lemma2, erule principal_mono)
   1.237  done
   1.238  
   1.239 -lemma basis_fun_take_eq_principal:
   1.240 -  "\<exists>a\<in>approxes x.
   1.241 -    basis_fun (\<lambda>a. principal (take i a))\<cdot>x = principal (take i a)"
   1.242 - apply (simp add: basis_fun_beta principal_mono take_mono)
   1.243 +lemma completion_approx_eq_principal:
   1.244 +  "\<exists>a\<in>rep x. completion_approx i\<cdot>x = principal (take i a)"
   1.245 +unfolding completion_approx_beta
   1.246   apply (subst image_image [where f=principal, symmetric])
   1.247 - apply (subgoal_tac "finite (principal ` take i ` approxes x)")
   1.248 -  apply (subgoal_tac "directed (principal ` take i ` approxes x)")
   1.249 + apply (subgoal_tac "finite (principal ` take i ` rep x)")
   1.250 +  apply (subgoal_tac "directed (principal ` take i ` rep x)")
   1.251     apply (drule (1) lub_finite_directed_in_self, fast)
   1.252    apply (subst image_image)
   1.253    apply (rule directed_image_ideal)
   1.254 -   apply (rule ideal_approxes)
   1.255 +   apply (rule ideal_rep)
   1.256    apply (erule principal_mono [OF take_mono])
   1.257   apply (rule finite_imageI)
   1.258 - apply (rule finite_take_approxes)
   1.259 + apply (rule finite_take_rep)
   1.260 +done
   1.261 +
   1.262 +lemma completion_approx_idem:
   1.263 +  "completion_approx i\<cdot>(completion_approx i\<cdot>x) = completion_approx i\<cdot>x"
   1.264 +using completion_approx_eq_principal [where i=i and x=x]
   1.265 +by (auto simp add: completion_approx_principal take_take)
   1.266 +
   1.267 +lemma finite_fixes_completion_approx:
   1.268 +  "finite {x. completion_approx i\<cdot>x = x}" (is "finite ?S")
   1.269 +apply (subgoal_tac "?S \<subseteq> principal ` range (take i)")
   1.270 +apply (erule finite_subset)
   1.271 +apply (rule finite_imageI)
   1.272 +apply (rule finite_range_take)
   1.273 +apply (clarify, erule subst)
   1.274 +apply (cut_tac x=x and i=i in completion_approx_eq_principal)
   1.275 +apply fast
   1.276  done
   1.277  
   1.278  lemma principal_induct:
   1.279    assumes adm: "adm P"
   1.280    assumes P: "\<And>a. P (principal a)"
   1.281    shows "P x"
   1.282 - apply (subgoal_tac "P (\<Squnion>i. basis_fun (\<lambda>a. principal (take i a))\<cdot>x)")
   1.283 - apply (simp add: lub_basis_fun_take)
   1.284 + apply (subgoal_tac "P (\<Squnion>i. completion_approx i\<cdot>x)")
   1.285 + apply (simp add: lub_completion_approx)
   1.286   apply (rule admD [OF adm])
   1.287 -  apply (simp add: chain_basis_fun_take)
   1.288 - apply (cut_tac x=x and i=i in basis_fun_take_eq_principal)
   1.289 +  apply (simp add: chain_completion_approx)
   1.290 + apply (cut_tac x=x and i=i in completion_approx_eq_principal)
   1.291   apply (clarify, simp add: P)
   1.292  done
   1.293  
   1.294 -lemma finite_fixes_basis_fun_take:
   1.295 -  "finite {x. basis_fun (\<lambda>a. principal (take i a))\<cdot>x = x}" (is "finite ?S")
   1.296 -apply (subgoal_tac "?S \<subseteq> principal ` range (take i)")
   1.297 -apply (erule finite_subset)
   1.298 -apply (rule finite_imageI)
   1.299 -apply (rule finite_range_take)
   1.300 -apply (clarify, erule subst)
   1.301 -apply (cut_tac x=x and i=i in basis_fun_take_eq_principal)
   1.302 -apply fast
   1.303 -done
   1.304 -
   1.305  end
   1.306  
   1.307  
   1.308 @@ -359,7 +382,7 @@
   1.309  by (fast intro: compact_approx)
   1.310  
   1.311  lemma compact_Rep_compact_basis [simp]: "compact (Rep_compact_basis a)"
   1.312 -by (rule Rep_compact_basis [simplified])
   1.313 +by (rule Rep_compact_basis [unfolded mem_Collect_eq])
   1.314  
   1.315  lemma Rep_Abs_compact_basis_approx [simp]:
   1.316    "Rep_compact_basis (Abs_compact_basis (approx n\<cdot>x)) = approx n\<cdot>x"
   1.317 @@ -520,7 +543,7 @@
   1.318  done
   1.319  
   1.320  interpretation compact_basis:
   1.321 -  bifinite_basis [sq_le compact_approx Rep_compact_basis compacts]
   1.322 +  ideal_completion [sq_le compact_approx Rep_compact_basis compacts]
   1.323  proof (unfold_locales)
   1.324    fix n :: nat and a b :: "'a compact_basis" and x :: "'a"
   1.325    show "compact_approx n a \<sqsubseteq> a"
   1.326 @@ -620,12 +643,14 @@
   1.327      "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
   1.328    where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
   1.329  
   1.330 -lemma (in ab_semigroup_idem_mult) fold_pd_PDUnit:
   1.331 -  "fold_pd g (op *) (PDUnit x) = g x"
   1.332 +lemma fold_pd_PDUnit:
   1.333 +  includes ab_semigroup_idem_mult f
   1.334 +  shows "fold_pd g f (PDUnit x) = g x"
   1.335  unfolding fold_pd_def Rep_PDUnit by simp
   1.336  
   1.337 -lemma (in ab_semigroup_idem_mult) fold_pd_PDPlus:
   1.338 -  "fold_pd g (op *) (PDPlus t u) = fold_pd g (op *) t * fold_pd g (op *) u"
   1.339 +lemma fold_pd_PDPlus:
   1.340 +  includes ab_semigroup_idem_mult f
   1.341 +  shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
   1.342  unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
   1.343  
   1.344  text {* approx-pd *}
     2.1 --- a/src/HOLCF/ConvexPD.thy	Fri May 16 22:35:25 2008 +0200
     2.2 +++ b/src/HOLCF/ConvexPD.thy	Fri May 16 23:25:37 2008 +0200
     2.3 @@ -148,14 +148,11 @@
     2.4  done
     2.5  
     2.6  lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)"
     2.7 -by (rule Rep_convex_pd [simplified])
     2.8 +by (rule Rep_convex_pd [unfolded mem_Collect_eq])
     2.9  
    2.10  lemma Rep_convex_pd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> Rep_convex_pd xs \<subseteq> Rep_convex_pd ys"
    2.11  unfolding less_convex_pd_def less_set_eq .
    2.12  
    2.13 -
    2.14 -subsection {* Principal ideals *}
    2.15 -
    2.16  definition
    2.17    convex_principal :: "'a pd_basis \<Rightarrow> 'a convex_pd" where
    2.18    "convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}"
    2.19 @@ -168,7 +165,7 @@
    2.20  done
    2.21  
    2.22  interpretation convex_pd:
    2.23 -  bifinite_basis [convex_le approx_pd convex_principal Rep_convex_pd]
    2.24 +  ideal_completion [convex_le approx_pd convex_principal Rep_convex_pd]
    2.25  apply unfold_locales
    2.26  apply (rule approx_pd_convex_le)
    2.27  apply (rule approx_pd_idem)
    2.28 @@ -183,13 +180,16 @@
    2.29  done
    2.30  
    2.31  lemma convex_principal_less_iff [simp]:
    2.32 -  "(convex_principal t \<sqsubseteq> convex_principal u) = (t \<le>\<natural> u)"
    2.33 -unfolding less_convex_pd_def Rep_convex_principal less_set_eq
    2.34 -by (fast intro: convex_le_refl elim: convex_le_trans)
    2.35 +  "convex_principal t \<sqsubseteq> convex_principal u \<longleftrightarrow> t \<le>\<natural> u"
    2.36 +by (rule convex_pd.principal_less_iff)
    2.37 +
    2.38 +lemma convex_principal_eq_iff [simp]:
    2.39 +  "convex_principal t = convex_principal u \<longleftrightarrow> t \<le>\<natural> u \<and> u \<le>\<natural> t"
    2.40 +by (rule convex_pd.principal_eq_iff)
    2.41  
    2.42  lemma convex_principal_mono:
    2.43    "t \<le>\<natural> u \<Longrightarrow> convex_principal t \<sqsubseteq> convex_principal u"
    2.44 -by (rule convex_principal_less_iff [THEN iffD2])
    2.45 +by (rule convex_pd.principal_mono)
    2.46  
    2.47  lemma compact_convex_principal: "compact (convex_principal t)"
    2.48  by (rule convex_pd.compact_principal)
    2.49 @@ -198,7 +198,7 @@
    2.50  by (induct ys rule: convex_pd.principal_induct, simp, simp)
    2.51  
    2.52  instance convex_pd :: (bifinite) pcpo
    2.53 -by (intro_classes, fast intro: convex_pd_minimal)
    2.54 +by intro_classes (fast intro: convex_pd_minimal)
    2.55  
    2.56  lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
    2.57  by (rule convex_pd_minimal [THEN UU_I, symmetric])
    2.58 @@ -209,51 +209,27 @@
    2.59  instance convex_pd :: (profinite) approx ..
    2.60  
    2.61  defs (overloaded)
    2.62 -  approx_convex_pd_def:
    2.63 -    "approx \<equiv> (\<lambda>n. convex_pd.basis_fun (\<lambda>t. convex_principal (approx_pd n t)))"
    2.64 +  approx_convex_pd_def: "approx \<equiv> convex_pd.completion_approx"
    2.65 +
    2.66 +instance convex_pd :: (profinite) profinite
    2.67 +apply (intro_classes, unfold approx_convex_pd_def)
    2.68 +apply (simp add: convex_pd.chain_completion_approx)
    2.69 +apply (rule convex_pd.lub_completion_approx)
    2.70 +apply (rule convex_pd.completion_approx_idem)
    2.71 +apply (rule convex_pd.finite_fixes_completion_approx)
    2.72 +done
    2.73 +
    2.74 +instance convex_pd :: (bifinite) bifinite ..
    2.75  
    2.76  lemma approx_convex_principal [simp]:
    2.77    "approx n\<cdot>(convex_principal t) = convex_principal (approx_pd n t)"
    2.78  unfolding approx_convex_pd_def
    2.79 -apply (rule convex_pd.basis_fun_principal)
    2.80 -apply (erule convex_principal_mono [OF approx_pd_convex_mono])
    2.81 -done
    2.82 -
    2.83 -lemma chain_approx_convex_pd:
    2.84 -  "chain (approx :: nat \<Rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd)"
    2.85 -unfolding approx_convex_pd_def
    2.86 -by (rule convex_pd.chain_basis_fun_take)
    2.87 -
    2.88 -lemma lub_approx_convex_pd:
    2.89 -  "(\<Squnion>i. approx i\<cdot>xs) = (xs::'a convex_pd)"
    2.90 -unfolding approx_convex_pd_def
    2.91 -by (rule convex_pd.lub_basis_fun_take)
    2.92 -
    2.93 -lemma approx_convex_pd_idem:
    2.94 -  "approx n\<cdot>(approx n\<cdot>xs) = approx n\<cdot>(xs::'a convex_pd)"
    2.95 -apply (induct xs rule: convex_pd.principal_induct, simp)
    2.96 -apply (simp add: approx_pd_idem)
    2.97 -done
    2.98 +by (rule convex_pd.completion_approx_principal)
    2.99  
   2.100  lemma approx_eq_convex_principal:
   2.101    "\<exists>t\<in>Rep_convex_pd xs. approx n\<cdot>xs = convex_principal (approx_pd n t)"
   2.102  unfolding approx_convex_pd_def
   2.103 -by (rule convex_pd.basis_fun_take_eq_principal)
   2.104 -
   2.105 -lemma finite_fixes_approx_convex_pd:
   2.106 -  "finite {xs::'a convex_pd. approx n\<cdot>xs = xs}"
   2.107 -unfolding approx_convex_pd_def
   2.108 -by (rule convex_pd.finite_fixes_basis_fun_take)
   2.109 -
   2.110 -instance convex_pd :: (profinite) profinite
   2.111 -apply intro_classes
   2.112 -apply (simp add: chain_approx_convex_pd)
   2.113 -apply (rule lub_approx_convex_pd)
   2.114 -apply (rule approx_convex_pd_idem)
   2.115 -apply (rule finite_fixes_approx_convex_pd)
   2.116 -done
   2.117 -
   2.118 -instance convex_pd :: (bifinite) bifinite ..
   2.119 +by (rule convex_pd.completion_approx_eq_principal)
   2.120  
   2.121  lemma compact_imp_convex_principal:
   2.122    "compact xs \<Longrightarrow> \<exists>t. xs = convex_principal t"
   2.123 @@ -266,10 +242,7 @@
   2.124  
   2.125  lemma convex_principal_induct:
   2.126    "\<lbrakk>adm P; \<And>t. P (convex_principal t)\<rbrakk> \<Longrightarrow> P xs"
   2.127 -apply (erule approx_induct, rename_tac xs)
   2.128 -apply (cut_tac n=n and xs=xs in approx_eq_convex_principal)
   2.129 -apply (clarify, simp)
   2.130 -done
   2.131 +by (rule convex_pd.principal_induct)
   2.132  
   2.133  lemma convex_principal_induct2:
   2.134    "\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
   2.135 @@ -282,54 +255,12 @@
   2.136  done
   2.137  
   2.138  
   2.139 -subsection {* Monadic unit *}
   2.140 +subsection {* Monadic unit and plus *}
   2.141  
   2.142  definition
   2.143    convex_unit :: "'a \<rightarrow> 'a convex_pd" where
   2.144    "convex_unit = compact_basis.basis_fun (\<lambda>a. convex_principal (PDUnit a))"
   2.145  
   2.146 -lemma convex_unit_Rep_compact_basis [simp]:
   2.147 -  "convex_unit\<cdot>(Rep_compact_basis a) = convex_principal (PDUnit a)"
   2.148 -unfolding convex_unit_def
   2.149 -apply (rule compact_basis.basis_fun_principal)
   2.150 -apply (rule convex_principal_mono)
   2.151 -apply (erule PDUnit_convex_mono)
   2.152 -done
   2.153 -
   2.154 -lemma convex_unit_strict [simp]: "convex_unit\<cdot>\<bottom> = \<bottom>"
   2.155 -unfolding inst_convex_pd_pcpo Rep_compact_bot [symmetric] by simp
   2.156 -
   2.157 -lemma approx_convex_unit [simp]:
   2.158 -  "approx n\<cdot>(convex_unit\<cdot>x) = convex_unit\<cdot>(approx n\<cdot>x)"
   2.159 -apply (induct x rule: compact_basis_induct, simp)
   2.160 -apply (simp add: approx_Rep_compact_basis)
   2.161 -done
   2.162 -
   2.163 -lemma convex_unit_less_iff [simp]:
   2.164 -  "(convex_unit\<cdot>x \<sqsubseteq> convex_unit\<cdot>y) = (x \<sqsubseteq> y)"
   2.165 - apply (rule iffI)
   2.166 -  apply (rule bifinite_less_ext)
   2.167 -  apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   2.168 -  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   2.169 -  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
   2.170 -  apply (clarify, simp add: compact_le_def)
   2.171 - apply (erule monofun_cfun_arg)
   2.172 -done
   2.173 -
   2.174 -lemma convex_unit_eq_iff [simp]:
   2.175 -  "(convex_unit\<cdot>x = convex_unit\<cdot>y) = (x = y)"
   2.176 -unfolding po_eq_conv by simp
   2.177 -
   2.178 -lemma convex_unit_strict_iff [simp]: "(convex_unit\<cdot>x = \<bottom>) = (x = \<bottom>)"
   2.179 -unfolding convex_unit_strict [symmetric] by (rule convex_unit_eq_iff)
   2.180 -
   2.181 -lemma compact_convex_unit_iff [simp]:
   2.182 -  "compact (convex_unit\<cdot>x) = compact x"
   2.183 -unfolding bifinite_compact_iff by simp
   2.184 -
   2.185 -
   2.186 -subsection {* Monadic plus *}
   2.187 -
   2.188  definition
   2.189    convex_plus :: "'a convex_pd \<rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd" where
   2.190    "convex_plus = convex_pd.basis_fun (\<lambda>t. convex_pd.basis_fun (\<lambda>u.
   2.191 @@ -340,40 +271,69 @@
   2.192      (infixl "+\<natural>" 65) where
   2.193    "xs +\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
   2.194  
   2.195 +syntax
   2.196 +  "_convex_pd" :: "args \<Rightarrow> 'a convex_pd" ("{_}\<natural>")
   2.197 +
   2.198 +translations
   2.199 +  "{x,xs}\<natural>" == "{x}\<natural> +\<natural> {xs}\<natural>"
   2.200 +  "{x}\<natural>" == "CONST convex_unit\<cdot>x"
   2.201 +
   2.202 +lemma convex_unit_Rep_compact_basis [simp]:
   2.203 +  "{Rep_compact_basis a}\<natural> = convex_principal (PDUnit a)"
   2.204 +unfolding convex_unit_def
   2.205 +by (simp add: compact_basis.basis_fun_principal
   2.206 +    convex_principal_mono PDUnit_convex_mono)
   2.207 +
   2.208  lemma convex_plus_principal [simp]:
   2.209 -  "convex_plus\<cdot>(convex_principal t)\<cdot>(convex_principal u) =
   2.210 -   convex_principal (PDPlus t u)"
   2.211 +  "convex_principal t +\<natural> convex_principal u = convex_principal (PDPlus t u)"
   2.212  unfolding convex_plus_def
   2.213  by (simp add: convex_pd.basis_fun_principal
   2.214      convex_pd.basis_fun_mono PDPlus_convex_mono)
   2.215  
   2.216 +lemma approx_convex_unit [simp]:
   2.217 +  "approx n\<cdot>{x}\<natural> = {approx n\<cdot>x}\<natural>"
   2.218 +apply (induct x rule: compact_basis_induct, simp)
   2.219 +apply (simp add: approx_Rep_compact_basis)
   2.220 +done
   2.221 +
   2.222  lemma approx_convex_plus [simp]:
   2.223 -  "approx n\<cdot>(convex_plus\<cdot>xs\<cdot>ys) = convex_plus\<cdot>(approx n\<cdot>xs)\<cdot>(approx n\<cdot>ys)"
   2.224 +  "approx n\<cdot>(xs +\<natural> ys) = approx n\<cdot>xs +\<natural> approx n\<cdot>ys"
   2.225  by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
   2.226  
   2.227 -lemma convex_plus_commute: "convex_plus\<cdot>xs\<cdot>ys = convex_plus\<cdot>ys\<cdot>xs"
   2.228 -apply (induct xs ys rule: convex_principal_induct2, simp, simp)
   2.229 -apply (simp add: PDPlus_commute)
   2.230 -done
   2.231 -
   2.232  lemma convex_plus_assoc:
   2.233 -  "convex_plus\<cdot>(convex_plus\<cdot>xs\<cdot>ys)\<cdot>zs = convex_plus\<cdot>xs\<cdot>(convex_plus\<cdot>ys\<cdot>zs)"
   2.234 +  "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)"
   2.235  apply (induct xs ys arbitrary: zs rule: convex_principal_induct2, simp, simp)
   2.236  apply (rule_tac xs=zs in convex_principal_induct, simp)
   2.237  apply (simp add: PDPlus_assoc)
   2.238  done
   2.239  
   2.240 -lemma convex_plus_absorb: "convex_plus\<cdot>xs\<cdot>xs = xs"
   2.241 +lemma convex_plus_commute: "xs +\<natural> ys = ys +\<natural> xs"
   2.242 +apply (induct xs ys rule: convex_principal_induct2, simp, simp)
   2.243 +apply (simp add: PDPlus_commute)
   2.244 +done
   2.245 +
   2.246 +lemma convex_plus_absorb: "xs +\<natural> xs = xs"
   2.247  apply (induct xs rule: convex_principal_induct, simp)
   2.248  apply (simp add: PDPlus_absorb)
   2.249  done
   2.250  
   2.251 +interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\<natural>"]
   2.252 +  by unfold_locales
   2.253 +    (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+
   2.254 +
   2.255 +lemma convex_plus_left_commute: "xs +\<natural> (ys +\<natural> zs) = ys +\<natural> (xs +\<natural> zs)"
   2.256 +by (rule aci_convex_plus.mult_left_commute)
   2.257 +
   2.258 +lemma convex_plus_left_absorb: "xs +\<natural> (xs +\<natural> ys) = xs +\<natural> ys"
   2.259 +by (rule aci_convex_plus.mult_left_idem)
   2.260 +
   2.261 +lemmas convex_plus_aci = aci_convex_plus.mult_ac_idem
   2.262 +
   2.263  lemma convex_unit_less_plus_iff [simp]:
   2.264 -  "(convex_unit\<cdot>x \<sqsubseteq> convex_plus\<cdot>ys\<cdot>zs) =
   2.265 -   (convex_unit\<cdot>x \<sqsubseteq> ys \<and> convex_unit\<cdot>x \<sqsubseteq> zs)"
   2.266 +  "{x}\<natural> \<sqsubseteq> ys +\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs"
   2.267   apply (rule iffI)
   2.268    apply (subgoal_tac
   2.269 -    "adm (\<lambda>f. f\<cdot>(convex_unit\<cdot>x) \<sqsubseteq> f\<cdot>ys \<and> f\<cdot>(convex_unit\<cdot>x) \<sqsubseteq> f\<cdot>zs)")
   2.270 +    "adm (\<lambda>f. f\<cdot>{x}\<natural> \<sqsubseteq> f\<cdot>ys \<and> f\<cdot>{x}\<natural> \<sqsubseteq> f\<cdot>zs)")
   2.271     apply (drule admD, rule chain_approx)
   2.272      apply (drule_tac f="approx i" in monofun_cfun_arg)
   2.273      apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   2.274 @@ -383,16 +343,15 @@
   2.275     apply simp
   2.276    apply simp
   2.277   apply (erule conjE)
   2.278 - apply (subst convex_plus_absorb [of "convex_unit\<cdot>x", symmetric])
   2.279 + apply (subst convex_plus_absorb [of "{x}\<natural>", symmetric])
   2.280   apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
   2.281  done
   2.282  
   2.283  lemma convex_plus_less_unit_iff [simp]:
   2.284 -  "(convex_plus\<cdot>xs\<cdot>ys \<sqsubseteq> convex_unit\<cdot>z) =
   2.285 -   (xs \<sqsubseteq> convex_unit\<cdot>z \<and> ys \<sqsubseteq> convex_unit\<cdot>z)"
   2.286 +  "xs +\<natural> ys \<sqsubseteq> {z}\<natural> \<longleftrightarrow> xs \<sqsubseteq> {z}\<natural> \<and> ys \<sqsubseteq> {z}\<natural>"
   2.287   apply (rule iffI)
   2.288    apply (subgoal_tac
   2.289 -    "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>(convex_unit\<cdot>z) \<and> f\<cdot>ys \<sqsubseteq> f\<cdot>(convex_unit\<cdot>z))")
   2.290 +    "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>{z}\<natural> \<and> f\<cdot>ys \<sqsubseteq> f\<cdot>{z}\<natural>)")
   2.291     apply (drule admD, rule chain_approx)
   2.292      apply (drule_tac f="approx i" in monofun_cfun_arg)
   2.293      apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_convex_principal, simp)
   2.294 @@ -402,18 +361,46 @@
   2.295     apply simp
   2.296    apply simp
   2.297   apply (erule conjE)
   2.298 - apply (subst convex_plus_absorb [of "convex_unit\<cdot>z", symmetric])
   2.299 + apply (subst convex_plus_absorb [of "{z}\<natural>", symmetric])
   2.300   apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
   2.301  done
   2.302  
   2.303 +lemma convex_unit_less_iff [simp]: "{x}\<natural> \<sqsubseteq> {y}\<natural> \<longleftrightarrow> x \<sqsubseteq> y"
   2.304 + apply (rule iffI)
   2.305 +  apply (rule bifinite_less_ext)
   2.306 +  apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   2.307 +  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   2.308 +  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
   2.309 +  apply (clarify, simp add: compact_le_def)
   2.310 + apply (erule monofun_cfun_arg)
   2.311 +done
   2.312 +
   2.313 +lemma convex_unit_eq_iff [simp]: "{x}\<natural> = {y}\<natural> \<longleftrightarrow> x = y"
   2.314 +unfolding po_eq_conv by simp
   2.315 +
   2.316 +lemma convex_unit_strict [simp]: "{\<bottom>}\<natural> = \<bottom>"
   2.317 +unfolding inst_convex_pd_pcpo Rep_compact_bot [symmetric] by simp
   2.318 +
   2.319 +lemma convex_unit_strict_iff [simp]: "{x}\<natural> = \<bottom> \<longleftrightarrow> x = \<bottom>"
   2.320 +unfolding convex_unit_strict [symmetric] by (rule convex_unit_eq_iff)
   2.321 +
   2.322 +lemma compact_convex_unit_iff [simp]:
   2.323 +  "compact {x}\<natural> \<longleftrightarrow> compact x"
   2.324 +unfolding bifinite_compact_iff by simp
   2.325 +
   2.326 +lemma compact_convex_plus [simp]:
   2.327 +  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<natural> ys)"
   2.328 +apply (drule compact_imp_convex_principal)+
   2.329 +apply (auto simp add: compact_convex_principal)
   2.330 +done
   2.331 +
   2.332  
   2.333  subsection {* Induction rules *}
   2.334  
   2.335  lemma convex_pd_induct1:
   2.336    assumes P: "adm P"
   2.337 -  assumes unit: "\<And>x. P (convex_unit\<cdot>x)"
   2.338 -  assumes insert:
   2.339 -    "\<And>x ys. \<lbrakk>P (convex_unit\<cdot>x); P ys\<rbrakk> \<Longrightarrow> P (convex_plus\<cdot>(convex_unit\<cdot>x)\<cdot>ys)"
   2.340 +  assumes unit: "\<And>x. P {x}\<natural>"
   2.341 +  assumes insert: "\<And>x ys. \<lbrakk>P {x}\<natural>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<natural> +\<natural> ys)"
   2.342    shows "P (xs::'a convex_pd)"
   2.343  apply (induct xs rule: convex_principal_induct, rule P)
   2.344  apply (induct_tac t rule: pd_basis_induct1)
   2.345 @@ -426,8 +413,8 @@
   2.346  
   2.347  lemma convex_pd_induct:
   2.348    assumes P: "adm P"
   2.349 -  assumes unit: "\<And>x. P (convex_unit\<cdot>x)"
   2.350 -  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (convex_plus\<cdot>xs\<cdot>ys)"
   2.351 +  assumes unit: "\<And>x. P {x}\<natural>"
   2.352 +  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<natural> ys)"
   2.353    shows "P (xs::'a convex_pd)"
   2.354  apply (induct xs rule: convex_principal_induct, rule P)
   2.355  apply (induct_tac t rule: pd_basis_induct)
   2.356 @@ -443,9 +430,10 @@
   2.357    "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where
   2.358    "convex_bind_basis = fold_pd
   2.359      (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
   2.360 -    (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
   2.361 +    (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
   2.362  
   2.363 -lemma ACI_convex_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
   2.364 +lemma ACI_convex_bind:
   2.365 +  "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
   2.366  apply unfold_locales
   2.367  apply (simp add: convex_plus_assoc)
   2.368  apply (simp add: convex_plus_commute)
   2.369 @@ -456,11 +444,11 @@
   2.370    "convex_bind_basis (PDUnit a) =
   2.371      (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   2.372    "convex_bind_basis (PDPlus t u) =
   2.373 -    (\<Lambda> f. convex_plus\<cdot>(convex_bind_basis t\<cdot>f)\<cdot>(convex_bind_basis u\<cdot>f))"
   2.374 +    (\<Lambda> f. convex_bind_basis t\<cdot>f +\<natural> convex_bind_basis u\<cdot>f)"
   2.375  unfolding convex_bind_basis_def
   2.376  apply -
   2.377 -apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_convex_bind])
   2.378 -apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_convex_bind])
   2.379 +apply (rule fold_pd_PDUnit [OF ACI_convex_bind])
   2.380 +apply (rule fold_pd_PDPlus [OF ACI_convex_bind])
   2.381  done
   2.382  
   2.383  lemma monofun_LAM:
   2.384 @@ -487,12 +475,11 @@
   2.385  done
   2.386  
   2.387  lemma convex_bind_unit [simp]:
   2.388 -  "convex_bind\<cdot>(convex_unit\<cdot>x)\<cdot>f = f\<cdot>x"
   2.389 +  "convex_bind\<cdot>{x}\<natural>\<cdot>f = f\<cdot>x"
   2.390  by (induct x rule: compact_basis_induct, simp, simp)
   2.391  
   2.392  lemma convex_bind_plus [simp]:
   2.393 -  "convex_bind\<cdot>(convex_plus\<cdot>xs\<cdot>ys)\<cdot>f =
   2.394 -   convex_plus\<cdot>(convex_bind\<cdot>xs\<cdot>f)\<cdot>(convex_bind\<cdot>ys\<cdot>f)"
   2.395 +  "convex_bind\<cdot>(xs +\<natural> ys)\<cdot>f = convex_bind\<cdot>xs\<cdot>f +\<natural> convex_bind\<cdot>ys\<cdot>f"
   2.396  by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
   2.397  
   2.398  lemma convex_bind_strict [simp]: "convex_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
   2.399 @@ -503,7 +490,7 @@
   2.400  
   2.401  definition
   2.402    convex_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a convex_pd \<rightarrow> 'b convex_pd" where
   2.403 -  "convex_map = (\<Lambda> f xs. convex_bind\<cdot>xs\<cdot>(\<Lambda> x. convex_unit\<cdot>(f\<cdot>x)))"
   2.404 +  "convex_map = (\<Lambda> f xs. convex_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<natural>))"
   2.405  
   2.406  definition
   2.407    convex_join :: "'a convex_pd convex_pd \<rightarrow> 'a convex_pd" where
   2.408 @@ -514,17 +501,15 @@
   2.409  unfolding convex_map_def by simp
   2.410  
   2.411  lemma convex_map_plus [simp]:
   2.412 -  "convex_map\<cdot>f\<cdot>(convex_plus\<cdot>xs\<cdot>ys) =
   2.413 -   convex_plus\<cdot>(convex_map\<cdot>f\<cdot>xs)\<cdot>(convex_map\<cdot>f\<cdot>ys)"
   2.414 +  "convex_map\<cdot>f\<cdot>(xs +\<natural> ys) = convex_map\<cdot>f\<cdot>xs +\<natural> convex_map\<cdot>f\<cdot>ys"
   2.415  unfolding convex_map_def by simp
   2.416  
   2.417  lemma convex_join_unit [simp]:
   2.418 -  "convex_join\<cdot>(convex_unit\<cdot>xs) = xs"
   2.419 +  "convex_join\<cdot>{xs}\<natural> = xs"
   2.420  unfolding convex_join_def by simp
   2.421  
   2.422  lemma convex_join_plus [simp]:
   2.423 -  "convex_join\<cdot>(convex_plus\<cdot>xss\<cdot>yss) =
   2.424 -   convex_plus\<cdot>(convex_join\<cdot>xss)\<cdot>(convex_join\<cdot>yss)"
   2.425 +  "convex_join\<cdot>(xss +\<natural> yss) = convex_join\<cdot>xss +\<natural> convex_join\<cdot>yss"
   2.426  unfolding convex_join_def by simp
   2.427  
   2.428  lemma convex_map_ident: "convex_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
   2.429 @@ -571,12 +556,11 @@
   2.430  done
   2.431  
   2.432  lemma convex_to_upper_unit [simp]:
   2.433 -  "convex_to_upper\<cdot>(convex_unit\<cdot>x) = upper_unit\<cdot>x"
   2.434 +  "convex_to_upper\<cdot>{x}\<natural> = {x}\<sharp>"
   2.435  by (induct x rule: compact_basis_induct, simp, simp)
   2.436  
   2.437  lemma convex_to_upper_plus [simp]:
   2.438 -  "convex_to_upper\<cdot>(convex_plus\<cdot>xs\<cdot>ys) =
   2.439 -   upper_plus\<cdot>(convex_to_upper\<cdot>xs)\<cdot>(convex_to_upper\<cdot>ys)"
   2.440 +  "convex_to_upper\<cdot>(xs +\<natural> ys) = convex_to_upper\<cdot>xs +\<sharp> convex_to_upper\<cdot>ys"
   2.441  by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
   2.442  
   2.443  lemma approx_convex_to_upper:
   2.444 @@ -601,12 +585,11 @@
   2.445  done
   2.446  
   2.447  lemma convex_to_lower_unit [simp]:
   2.448 -  "convex_to_lower\<cdot>(convex_unit\<cdot>x) = lower_unit\<cdot>x"
   2.449 +  "convex_to_lower\<cdot>{x}\<natural> = {x}\<flat>"
   2.450  by (induct x rule: compact_basis_induct, simp, simp)
   2.451  
   2.452  lemma convex_to_lower_plus [simp]:
   2.453 -  "convex_to_lower\<cdot>(convex_plus\<cdot>xs\<cdot>ys) =
   2.454 -   lower_plus\<cdot>(convex_to_lower\<cdot>xs)\<cdot>(convex_to_lower\<cdot>ys)"
   2.455 +  "convex_to_lower\<cdot>(xs +\<natural> ys) = convex_to_lower\<cdot>xs +\<flat> convex_to_lower\<cdot>ys"
   2.456  by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
   2.457  
   2.458  lemma approx_convex_to_lower:
   2.459 @@ -629,4 +612,19 @@
   2.460   apply (simp add: approx_convex_to_upper approx_convex_to_lower convex_le_def)
   2.461  done
   2.462  
   2.463 +lemmas convex_plus_less_plus_iff =
   2.464 +  convex_pd_less_iff [where xs="xs +\<natural> ys" and ys="zs +\<natural> ws", standard]
   2.465 +
   2.466 +lemmas convex_pd_less_simps =
   2.467 +  convex_unit_less_plus_iff
   2.468 +  convex_plus_less_unit_iff
   2.469 +  convex_plus_less_plus_iff
   2.470 +  convex_unit_less_iff
   2.471 +  convex_to_upper_unit
   2.472 +  convex_to_upper_plus
   2.473 +  convex_to_lower_unit
   2.474 +  convex_to_lower_plus
   2.475 +  upper_pd_less_simps
   2.476 +  lower_pd_less_simps
   2.477 +
   2.478  end
     3.1 --- a/src/HOLCF/LowerPD.thy	Fri May 16 22:35:25 2008 +0200
     3.2 +++ b/src/HOLCF/LowerPD.thy	Fri May 16 23:25:37 2008 +0200
     3.3 @@ -103,13 +103,7 @@
     3.4  done
     3.5  
     3.6  lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd x)"
     3.7 -by (rule Rep_lower_pd [simplified])
     3.8 -
     3.9 -lemma Rep_lower_pd_mono: "x \<sqsubseteq> y \<Longrightarrow> Rep_lower_pd x \<subseteq> Rep_lower_pd y"
    3.10 -unfolding less_lower_pd_def less_set_eq .
    3.11 -
    3.12 -
    3.13 -subsection {* Principal ideals *}
    3.14 +by (rule Rep_lower_pd [unfolded mem_Collect_eq])
    3.15  
    3.16  definition
    3.17    lower_principal :: "'a pd_basis \<Rightarrow> 'a lower_pd" where
    3.18 @@ -123,7 +117,7 @@
    3.19  done
    3.20  
    3.21  interpretation lower_pd:
    3.22 -  bifinite_basis [lower_le approx_pd lower_principal Rep_lower_pd]
    3.23 +  ideal_completion [lower_le approx_pd lower_principal Rep_lower_pd]
    3.24  apply unfold_locales
    3.25  apply (rule approx_pd_lower_le)
    3.26  apply (rule approx_pd_idem)
    3.27 @@ -138,32 +132,25 @@
    3.28  done
    3.29  
    3.30  lemma lower_principal_less_iff [simp]:
    3.31 -  "(lower_principal t \<sqsubseteq> lower_principal u) = (t \<le>\<flat> u)"
    3.32 -unfolding less_lower_pd_def Rep_lower_principal less_set_eq
    3.33 -by (fast intro: lower_le_refl elim: lower_le_trans)
    3.34 +  "lower_principal t \<sqsubseteq> lower_principal u \<longleftrightarrow> t \<le>\<flat> u"
    3.35 +by (rule lower_pd.principal_less_iff)
    3.36 +
    3.37 +lemma lower_principal_eq_iff:
    3.38 +  "lower_principal t = lower_principal u \<longleftrightarrow> t \<le>\<flat> u \<and> u \<le>\<flat> t"
    3.39 +by (rule lower_pd.principal_eq_iff)
    3.40  
    3.41  lemma lower_principal_mono:
    3.42    "t \<le>\<flat> u \<Longrightarrow> lower_principal t \<sqsubseteq> lower_principal u"
    3.43 -by (rule lower_principal_less_iff [THEN iffD2])
    3.44 +by (rule lower_pd.principal_mono)
    3.45  
    3.46  lemma compact_lower_principal: "compact (lower_principal t)"
    3.47 -apply (rule compactI2)
    3.48 -apply (simp add: less_lower_pd_def)
    3.49 -apply (simp add: cont2contlubE [OF cont_Rep_lower_pd])
    3.50 -apply (simp add: Rep_lower_principal set_cpo_simps)
    3.51 -apply (simp add: subset_eq)
    3.52 -apply (drule spec, drule mp, rule lower_le_refl)
    3.53 -apply (erule exE, rename_tac i)
    3.54 -apply (rule_tac x=i in exI)
    3.55 -apply clarify
    3.56 -apply (erule (1) lower_le.idealD3 [OF ideal_Rep_lower_pd])
    3.57 -done
    3.58 +by (rule lower_pd.compact_principal)
    3.59  
    3.60  lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \<sqsubseteq> ys"
    3.61  by (induct ys rule: lower_pd.principal_induct, simp, simp)
    3.62  
    3.63  instance lower_pd :: (bifinite) pcpo
    3.64 -by (intro_classes, fast intro: lower_pd_minimal)
    3.65 +by intro_classes (fast intro: lower_pd_minimal)
    3.66  
    3.67  lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)"
    3.68  by (rule lower_pd_minimal [THEN UU_I, symmetric])
    3.69 @@ -174,51 +161,27 @@
    3.70  instance lower_pd :: (profinite) approx ..
    3.71  
    3.72  defs (overloaded)
    3.73 -  approx_lower_pd_def:
    3.74 -    "approx \<equiv> (\<lambda>n. lower_pd.basis_fun (\<lambda>t. lower_principal (approx_pd n t)))"
    3.75 +  approx_lower_pd_def: "approx \<equiv> lower_pd.completion_approx"
    3.76 +
    3.77 +instance lower_pd :: (profinite) profinite
    3.78 +apply (intro_classes, unfold approx_lower_pd_def)
    3.79 +apply (simp add: lower_pd.chain_completion_approx)
    3.80 +apply (rule lower_pd.lub_completion_approx)
    3.81 +apply (rule lower_pd.completion_approx_idem)
    3.82 +apply (rule lower_pd.finite_fixes_completion_approx)
    3.83 +done
    3.84 +
    3.85 +instance lower_pd :: (bifinite) bifinite ..
    3.86  
    3.87  lemma approx_lower_principal [simp]:
    3.88    "approx n\<cdot>(lower_principal t) = lower_principal (approx_pd n t)"
    3.89  unfolding approx_lower_pd_def
    3.90 -apply (rule lower_pd.basis_fun_principal)
    3.91 -apply (erule lower_principal_mono [OF approx_pd_lower_mono])
    3.92 -done
    3.93 -
    3.94 -lemma chain_approx_lower_pd:
    3.95 -  "chain (approx :: nat \<Rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd)"
    3.96 -unfolding approx_lower_pd_def
    3.97 -by (rule lower_pd.chain_basis_fun_take)
    3.98 -
    3.99 -lemma lub_approx_lower_pd:
   3.100 -  "(\<Squnion>i. approx i\<cdot>xs) = (xs::'a lower_pd)"
   3.101 -unfolding approx_lower_pd_def
   3.102 -by (rule lower_pd.lub_basis_fun_take)
   3.103 -
   3.104 -lemma approx_lower_pd_idem:
   3.105 -  "approx n\<cdot>(approx n\<cdot>xs) = approx n\<cdot>(xs::'a lower_pd)"
   3.106 -apply (induct xs rule: lower_pd.principal_induct, simp)
   3.107 -apply (simp add: approx_pd_idem)
   3.108 -done
   3.109 +by (rule lower_pd.completion_approx_principal)
   3.110  
   3.111  lemma approx_eq_lower_principal:
   3.112    "\<exists>t\<in>Rep_lower_pd xs. approx n\<cdot>xs = lower_principal (approx_pd n t)"
   3.113  unfolding approx_lower_pd_def
   3.114 -by (rule lower_pd.basis_fun_take_eq_principal)
   3.115 -
   3.116 -lemma finite_fixes_approx_lower_pd:
   3.117 -  "finite {xs::'a lower_pd. approx n\<cdot>xs = xs}"
   3.118 -unfolding approx_lower_pd_def
   3.119 -by (rule lower_pd.finite_fixes_basis_fun_take)
   3.120 -
   3.121 -instance lower_pd :: (profinite) profinite
   3.122 -apply intro_classes
   3.123 -apply (simp add: chain_approx_lower_pd)
   3.124 -apply (rule lub_approx_lower_pd)
   3.125 -apply (rule approx_lower_pd_idem)
   3.126 -apply (rule finite_fixes_approx_lower_pd)
   3.127 -done
   3.128 -
   3.129 -instance lower_pd :: (bifinite) bifinite ..
   3.130 +by (rule lower_pd.completion_approx_eq_principal)
   3.131  
   3.132  lemma compact_imp_lower_principal:
   3.133    "compact xs \<Longrightarrow> \<exists>t. xs = lower_principal t"
   3.134 @@ -231,10 +194,7 @@
   3.135  
   3.136  lemma lower_principal_induct:
   3.137    "\<lbrakk>adm P; \<And>t. P (lower_principal t)\<rbrakk> \<Longrightarrow> P xs"
   3.138 -apply (erule approx_induct, rename_tac xs)
   3.139 -apply (cut_tac n=n and xs=xs in approx_eq_lower_principal)
   3.140 -apply (clarify, simp)
   3.141 -done
   3.142 +by (rule lower_pd.principal_induct)
   3.143  
   3.144  lemma lower_principal_induct2:
   3.145    "\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
   3.146 @@ -247,54 +207,12 @@
   3.147  done
   3.148  
   3.149  
   3.150 -subsection {* Monadic unit *}
   3.151 +subsection {* Monadic unit and plus *}
   3.152  
   3.153  definition
   3.154    lower_unit :: "'a \<rightarrow> 'a lower_pd" where
   3.155    "lower_unit = compact_basis.basis_fun (\<lambda>a. lower_principal (PDUnit a))"
   3.156  
   3.157 -lemma lower_unit_Rep_compact_basis [simp]:
   3.158 -  "lower_unit\<cdot>(Rep_compact_basis a) = lower_principal (PDUnit a)"
   3.159 -unfolding lower_unit_def
   3.160 -apply (rule compact_basis.basis_fun_principal)
   3.161 -apply (rule lower_principal_mono)
   3.162 -apply (erule PDUnit_lower_mono)
   3.163 -done
   3.164 -
   3.165 -lemma lower_unit_strict [simp]: "lower_unit\<cdot>\<bottom> = \<bottom>"
   3.166 -unfolding inst_lower_pd_pcpo Rep_compact_bot [symmetric] by simp
   3.167 -
   3.168 -lemma approx_lower_unit [simp]:
   3.169 -  "approx n\<cdot>(lower_unit\<cdot>x) = lower_unit\<cdot>(approx n\<cdot>x)"
   3.170 -apply (induct x rule: compact_basis_induct, simp)
   3.171 -apply (simp add: approx_Rep_compact_basis)
   3.172 -done
   3.173 -
   3.174 -lemma lower_unit_less_iff [simp]:
   3.175 -  "(lower_unit\<cdot>x \<sqsubseteq> lower_unit\<cdot>y) = (x \<sqsubseteq> y)"
   3.176 - apply (rule iffI)
   3.177 -  apply (rule bifinite_less_ext)
   3.178 -  apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   3.179 -  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   3.180 -  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
   3.181 -  apply (clarify, simp add: compact_le_def)
   3.182 - apply (erule monofun_cfun_arg)
   3.183 -done
   3.184 -
   3.185 -lemma lower_unit_eq_iff [simp]:
   3.186 -  "(lower_unit\<cdot>x = lower_unit\<cdot>y) = (x = y)"
   3.187 -unfolding po_eq_conv by simp
   3.188 -
   3.189 -lemma lower_unit_strict_iff [simp]: "(lower_unit\<cdot>x = \<bottom>) = (x = \<bottom>)"
   3.190 -unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff)
   3.191 -
   3.192 -lemma compact_lower_unit_iff [simp]:
   3.193 -  "compact (lower_unit\<cdot>x) = compact x"
   3.194 -unfolding bifinite_compact_iff by simp
   3.195 -
   3.196 -
   3.197 -subsection {* Monadic plus *}
   3.198 -
   3.199  definition
   3.200    lower_plus :: "'a lower_pd \<rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd" where
   3.201    "lower_plus = lower_pd.basis_fun (\<lambda>t. lower_pd.basis_fun (\<lambda>u.
   3.202 @@ -305,79 +223,89 @@
   3.203      (infixl "+\<flat>" 65) where
   3.204    "xs +\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
   3.205  
   3.206 +syntax
   3.207 +  "_lower_pd" :: "args \<Rightarrow> 'a lower_pd" ("{_}\<flat>")
   3.208 +
   3.209 +translations
   3.210 +  "{x,xs}\<flat>" == "{x}\<flat> +\<flat> {xs}\<flat>"
   3.211 +  "{x}\<flat>" == "CONST lower_unit\<cdot>x"
   3.212 +
   3.213 +lemma lower_unit_Rep_compact_basis [simp]:
   3.214 +  "{Rep_compact_basis a}\<flat> = lower_principal (PDUnit a)"
   3.215 +unfolding lower_unit_def
   3.216 +by (simp add: compact_basis.basis_fun_principal
   3.217 +    lower_principal_mono PDUnit_lower_mono)
   3.218 +
   3.219  lemma lower_plus_principal [simp]:
   3.220 -  "lower_plus\<cdot>(lower_principal t)\<cdot>(lower_principal u) =
   3.221 -   lower_principal (PDPlus t u)"
   3.222 +  "lower_principal t +\<flat> lower_principal u = lower_principal (PDPlus t u)"
   3.223  unfolding lower_plus_def
   3.224  by (simp add: lower_pd.basis_fun_principal
   3.225      lower_pd.basis_fun_mono PDPlus_lower_mono)
   3.226  
   3.227 +lemma approx_lower_unit [simp]:
   3.228 +  "approx n\<cdot>{x}\<flat> = {approx n\<cdot>x}\<flat>"
   3.229 +apply (induct x rule: compact_basis_induct, simp)
   3.230 +apply (simp add: approx_Rep_compact_basis)
   3.231 +done
   3.232 +
   3.233  lemma approx_lower_plus [simp]:
   3.234 -  "approx n\<cdot>(lower_plus\<cdot>xs\<cdot>ys) = lower_plus\<cdot>(approx n\<cdot>xs)\<cdot>(approx n\<cdot>ys)"
   3.235 +  "approx n\<cdot>(xs +\<flat> ys) = (approx n\<cdot>xs) +\<flat> (approx n\<cdot>ys)"
   3.236  by (induct xs ys rule: lower_principal_induct2, simp, simp, simp)
   3.237  
   3.238 -lemma lower_plus_commute: "lower_plus\<cdot>xs\<cdot>ys = lower_plus\<cdot>ys\<cdot>xs"
   3.239 -apply (induct xs ys rule: lower_principal_induct2, simp, simp)
   3.240 -apply (simp add: PDPlus_commute)
   3.241 -done
   3.242 -
   3.243 -lemma lower_plus_assoc:
   3.244 -  "lower_plus\<cdot>(lower_plus\<cdot>xs\<cdot>ys)\<cdot>zs = lower_plus\<cdot>xs\<cdot>(lower_plus\<cdot>ys\<cdot>zs)"
   3.245 +lemma lower_plus_assoc: "(xs +\<flat> ys) +\<flat> zs = xs +\<flat> (ys +\<flat> zs)"
   3.246  apply (induct xs ys arbitrary: zs rule: lower_principal_induct2, simp, simp)
   3.247  apply (rule_tac xs=zs in lower_principal_induct, simp)
   3.248  apply (simp add: PDPlus_assoc)
   3.249  done
   3.250  
   3.251 -lemma lower_plus_absorb: "lower_plus\<cdot>xs\<cdot>xs = xs"
   3.252 +lemma lower_plus_commute: "xs +\<flat> ys = ys +\<flat> xs"
   3.253 +apply (induct xs ys rule: lower_principal_induct2, simp, simp)
   3.254 +apply (simp add: PDPlus_commute)
   3.255 +done
   3.256 +
   3.257 +lemma lower_plus_absorb: "xs +\<flat> xs = xs"
   3.258  apply (induct xs rule: lower_principal_induct, simp)
   3.259  apply (simp add: PDPlus_absorb)
   3.260  done
   3.261  
   3.262 -lemma lower_plus_less1: "xs \<sqsubseteq> lower_plus\<cdot>xs\<cdot>ys"
   3.263 +interpretation aci_lower_plus: ab_semigroup_idem_mult ["op +\<flat>"]
   3.264 +  by unfold_locales
   3.265 +    (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+
   3.266 +
   3.267 +lemma lower_plus_left_commute: "xs +\<flat> (ys +\<flat> zs) = ys +\<flat> (xs +\<flat> zs)"
   3.268 +by (rule aci_lower_plus.mult_left_commute)
   3.269 +
   3.270 +lemma lower_plus_left_absorb: "xs +\<flat> (xs +\<flat> ys) = xs +\<flat> ys"
   3.271 +by (rule aci_lower_plus.mult_left_idem)
   3.272 +
   3.273 +lemmas lower_plus_aci = aci_lower_plus.mult_ac_idem
   3.274 +
   3.275 +lemma lower_plus_less1: "xs \<sqsubseteq> xs +\<flat> ys"
   3.276  apply (induct xs ys rule: lower_principal_induct2, simp, simp)
   3.277  apply (simp add: PDPlus_lower_less)
   3.278  done
   3.279  
   3.280 -lemma lower_plus_less2: "ys \<sqsubseteq> lower_plus\<cdot>xs\<cdot>ys"
   3.281 +lemma lower_plus_less2: "ys \<sqsubseteq> xs +\<flat> ys"
   3.282  by (subst lower_plus_commute, rule lower_plus_less1)
   3.283  
   3.284 -lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> lower_plus\<cdot>xs\<cdot>ys \<sqsubseteq> zs"
   3.285 +lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs +\<flat> ys \<sqsubseteq> zs"
   3.286  apply (subst lower_plus_absorb [of zs, symmetric])
   3.287  apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
   3.288  done
   3.289  
   3.290  lemma lower_plus_less_iff:
   3.291 -  "(lower_plus\<cdot>xs\<cdot>ys \<sqsubseteq> zs) = (xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs)"
   3.292 +  "xs +\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs"
   3.293  apply safe
   3.294  apply (erule trans_less [OF lower_plus_less1])
   3.295  apply (erule trans_less [OF lower_plus_less2])
   3.296  apply (erule (1) lower_plus_least)
   3.297  done
   3.298  
   3.299 -lemma lower_plus_strict_iff [simp]:
   3.300 -  "(lower_plus\<cdot>xs\<cdot>ys = \<bottom>) = (xs = \<bottom> \<and> ys = \<bottom>)"
   3.301 -apply safe
   3.302 -apply (rule UU_I, erule subst, rule lower_plus_less1)
   3.303 -apply (rule UU_I, erule subst, rule lower_plus_less2)
   3.304 -apply (rule lower_plus_absorb)
   3.305 -done
   3.306 -
   3.307 -lemma lower_plus_strict1 [simp]: "lower_plus\<cdot>\<bottom>\<cdot>ys = ys"
   3.308 -apply (rule antisym_less [OF _ lower_plus_less2])
   3.309 -apply (simp add: lower_plus_least)
   3.310 -done
   3.311 -
   3.312 -lemma lower_plus_strict2 [simp]: "lower_plus\<cdot>xs\<cdot>\<bottom> = xs"
   3.313 -apply (rule antisym_less [OF _ lower_plus_less1])
   3.314 -apply (simp add: lower_plus_least)
   3.315 -done
   3.316 -
   3.317  lemma lower_unit_less_plus_iff:
   3.318 -  "(lower_unit\<cdot>x \<sqsubseteq> lower_plus\<cdot>ys\<cdot>zs) =
   3.319 -    (lower_unit\<cdot>x \<sqsubseteq> ys \<or> lower_unit\<cdot>x \<sqsubseteq> zs)"
   3.320 +  "{x}\<flat> \<sqsubseteq> ys +\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
   3.321   apply (rule iffI)
   3.322    apply (subgoal_tac
   3.323 -    "adm (\<lambda>f. f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>ys \<or> f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>zs)")
   3.324 +    "adm (\<lambda>f. f\<cdot>{x}\<flat> \<sqsubseteq> f\<cdot>ys \<or> f\<cdot>{x}\<flat> \<sqsubseteq> f\<cdot>zs)")
   3.325     apply (drule admD, rule chain_approx)
   3.326      apply (drule_tac f="approx i" in monofun_cfun_arg)
   3.327      apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   3.328 @@ -391,19 +319,65 @@
   3.329   apply (erule trans_less [OF _ lower_plus_less2])
   3.330  done
   3.331  
   3.332 +lemma lower_unit_less_iff [simp]: "{x}\<flat> \<sqsubseteq> {y}\<flat> \<longleftrightarrow> x \<sqsubseteq> y"
   3.333 + apply (rule iffI)
   3.334 +  apply (rule bifinite_less_ext)
   3.335 +  apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   3.336 +  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   3.337 +  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
   3.338 +  apply (clarify, simp add: compact_le_def)
   3.339 + apply (erule monofun_cfun_arg)
   3.340 +done
   3.341 +
   3.342  lemmas lower_pd_less_simps =
   3.343    lower_unit_less_iff
   3.344    lower_plus_less_iff
   3.345    lower_unit_less_plus_iff
   3.346  
   3.347 +lemma lower_unit_eq_iff [simp]: "{x}\<flat> = {y}\<flat> \<longleftrightarrow> x = y"
   3.348 +unfolding po_eq_conv by simp
   3.349 +
   3.350 +lemma lower_unit_strict [simp]: "{\<bottom>}\<flat> = \<bottom>"
   3.351 +unfolding inst_lower_pd_pcpo Rep_compact_bot [symmetric] by simp
   3.352 +
   3.353 +lemma lower_unit_strict_iff [simp]: "{x}\<flat> = \<bottom> \<longleftrightarrow> x = \<bottom>"
   3.354 +unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff)
   3.355 +
   3.356 +lemma lower_plus_strict_iff [simp]:
   3.357 +  "xs +\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
   3.358 +apply safe
   3.359 +apply (rule UU_I, erule subst, rule lower_plus_less1)
   3.360 +apply (rule UU_I, erule subst, rule lower_plus_less2)
   3.361 +apply (rule lower_plus_absorb)
   3.362 +done
   3.363 +
   3.364 +lemma lower_plus_strict1 [simp]: "\<bottom> +\<flat> ys = ys"
   3.365 +apply (rule antisym_less [OF _ lower_plus_less2])
   3.366 +apply (simp add: lower_plus_least)
   3.367 +done
   3.368 +
   3.369 +lemma lower_plus_strict2 [simp]: "xs +\<flat> \<bottom> = xs"
   3.370 +apply (rule antisym_less [OF _ lower_plus_less1])
   3.371 +apply (simp add: lower_plus_least)
   3.372 +done
   3.373 +
   3.374 +lemma compact_lower_unit_iff [simp]: "compact {x}\<flat> \<longleftrightarrow> compact x"
   3.375 +unfolding bifinite_compact_iff by simp
   3.376 +
   3.377 +lemma compact_lower_plus [simp]:
   3.378 +  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<flat> ys)"
   3.379 +apply (drule compact_imp_lower_principal)+
   3.380 +apply (auto simp add: compact_lower_principal)
   3.381 +done
   3.382 +
   3.383  
   3.384  subsection {* Induction rules *}
   3.385  
   3.386  lemma lower_pd_induct1:
   3.387    assumes P: "adm P"
   3.388 -  assumes unit: "\<And>x. P (lower_unit\<cdot>x)"
   3.389 +  assumes unit: "\<And>x. P {x}\<flat>"
   3.390    assumes insert:
   3.391 -    "\<And>x ys. \<lbrakk>P (lower_unit\<cdot>x); P ys\<rbrakk> \<Longrightarrow> P (lower_plus\<cdot>(lower_unit\<cdot>x)\<cdot>ys)"
   3.392 +    "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> +\<flat> ys)"
   3.393    shows "P (xs::'a lower_pd)"
   3.394  apply (induct xs rule: lower_principal_induct, rule P)
   3.395  apply (induct_tac t rule: pd_basis_induct1)
   3.396 @@ -416,8 +390,8 @@
   3.397  
   3.398  lemma lower_pd_induct:
   3.399    assumes P: "adm P"
   3.400 -  assumes unit: "\<And>x. P (lower_unit\<cdot>x)"
   3.401 -  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (lower_plus\<cdot>xs\<cdot>ys)"
   3.402 +  assumes unit: "\<And>x. P {x}\<flat>"
   3.403 +  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<flat> ys)"
   3.404    shows "P (xs::'a lower_pd)"
   3.405  apply (induct xs rule: lower_principal_induct, rule P)
   3.406  apply (induct_tac t rule: pd_basis_induct)
   3.407 @@ -433,9 +407,10 @@
   3.408    "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b lower_pd" where
   3.409    "lower_bind_basis = fold_pd
   3.410      (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
   3.411 -    (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
   3.412 +    (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
   3.413  
   3.414 -lemma ACI_lower_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
   3.415 +lemma ACI_lower_bind:
   3.416 +  "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
   3.417  apply unfold_locales
   3.418  apply (simp add: lower_plus_assoc)
   3.419  apply (simp add: lower_plus_commute)
   3.420 @@ -446,11 +421,11 @@
   3.421    "lower_bind_basis (PDUnit a) =
   3.422      (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   3.423    "lower_bind_basis (PDPlus t u) =
   3.424 -    (\<Lambda> f. lower_plus\<cdot>(lower_bind_basis t\<cdot>f)\<cdot>(lower_bind_basis u\<cdot>f))"
   3.425 +    (\<Lambda> f. lower_bind_basis t\<cdot>f +\<flat> lower_bind_basis u\<cdot>f)"
   3.426  unfolding lower_bind_basis_def
   3.427  apply -
   3.428 -apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_lower_bind])
   3.429 -apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_lower_bind])
   3.430 +apply (rule fold_pd_PDUnit [OF ACI_lower_bind])
   3.431 +apply (rule fold_pd_PDPlus [OF ACI_lower_bind])
   3.432  done
   3.433  
   3.434  lemma lower_bind_basis_mono:
   3.435 @@ -474,12 +449,11 @@
   3.436  done
   3.437  
   3.438  lemma lower_bind_unit [simp]:
   3.439 -  "lower_bind\<cdot>(lower_unit\<cdot>x)\<cdot>f = f\<cdot>x"
   3.440 +  "lower_bind\<cdot>{x}\<flat>\<cdot>f = f\<cdot>x"
   3.441  by (induct x rule: compact_basis_induct, simp, simp)
   3.442  
   3.443  lemma lower_bind_plus [simp]:
   3.444 -  "lower_bind\<cdot>(lower_plus\<cdot>xs\<cdot>ys)\<cdot>f =
   3.445 -   lower_plus\<cdot>(lower_bind\<cdot>xs\<cdot>f)\<cdot>(lower_bind\<cdot>ys\<cdot>f)"
   3.446 +  "lower_bind\<cdot>(xs +\<flat> ys)\<cdot>f = lower_bind\<cdot>xs\<cdot>f +\<flat> lower_bind\<cdot>ys\<cdot>f"
   3.447  by (induct xs ys rule: lower_principal_induct2, simp, simp, simp)
   3.448  
   3.449  lemma lower_bind_strict [simp]: "lower_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
   3.450 @@ -490,28 +464,26 @@
   3.451  
   3.452  definition
   3.453    lower_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a lower_pd \<rightarrow> 'b lower_pd" where
   3.454 -  "lower_map = (\<Lambda> f xs. lower_bind\<cdot>xs\<cdot>(\<Lambda> x. lower_unit\<cdot>(f\<cdot>x)))"
   3.455 +  "lower_map = (\<Lambda> f xs. lower_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<flat>))"
   3.456  
   3.457  definition
   3.458    lower_join :: "'a lower_pd lower_pd \<rightarrow> 'a lower_pd" where
   3.459    "lower_join = (\<Lambda> xss. lower_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"
   3.460  
   3.461  lemma lower_map_unit [simp]:
   3.462 -  "lower_map\<cdot>f\<cdot>(lower_unit\<cdot>x) = lower_unit\<cdot>(f\<cdot>x)"
   3.463 +  "lower_map\<cdot>f\<cdot>{x}\<flat> = {f\<cdot>x}\<flat>"
   3.464  unfolding lower_map_def by simp
   3.465  
   3.466  lemma lower_map_plus [simp]:
   3.467 -  "lower_map\<cdot>f\<cdot>(lower_plus\<cdot>xs\<cdot>ys) =
   3.468 -   lower_plus\<cdot>(lower_map\<cdot>f\<cdot>xs)\<cdot>(lower_map\<cdot>f\<cdot>ys)"
   3.469 +  "lower_map\<cdot>f\<cdot>(xs +\<flat> ys) = lower_map\<cdot>f\<cdot>xs +\<flat> lower_map\<cdot>f\<cdot>ys"
   3.470  unfolding lower_map_def by simp
   3.471  
   3.472  lemma lower_join_unit [simp]:
   3.473 -  "lower_join\<cdot>(lower_unit\<cdot>xs) = xs"
   3.474 +  "lower_join\<cdot>{xs}\<flat> = xs"
   3.475  unfolding lower_join_def by simp
   3.476  
   3.477  lemma lower_join_plus [simp]:
   3.478 -  "lower_join\<cdot>(lower_plus\<cdot>xss\<cdot>yss) =
   3.479 -   lower_plus\<cdot>(lower_join\<cdot>xss)\<cdot>(lower_join\<cdot>yss)"
   3.480 +  "lower_join\<cdot>(xss +\<flat> yss) = lower_join\<cdot>xss +\<flat> lower_join\<cdot>yss"
   3.481  unfolding lower_join_def by simp
   3.482  
   3.483  lemma lower_map_ident: "lower_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
     4.1 --- a/src/HOLCF/UpperPD.thy	Fri May 16 22:35:25 2008 +0200
     4.2 +++ b/src/HOLCF/UpperPD.thy	Fri May 16 23:25:37 2008 +0200
     4.3 @@ -101,7 +101,7 @@
     4.4  done
     4.5  
     4.6  lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd x)"
     4.7 -by (rule Rep_upper_pd [simplified])
     4.8 +by (rule Rep_upper_pd [unfolded mem_Collect_eq])
     4.9  
    4.10  definition
    4.11    upper_principal :: "'a pd_basis \<Rightarrow> 'a upper_pd" where
    4.12 @@ -110,12 +110,12 @@
    4.13  lemma Rep_upper_principal:
    4.14    "Rep_upper_pd (upper_principal t) = {u. u \<le>\<sharp> t}"
    4.15  unfolding upper_principal_def
    4.16 -apply (rule Abs_upper_pd_inverse [simplified])
    4.17 +apply (rule Abs_upper_pd_inverse [unfolded mem_Collect_eq])
    4.18  apply (rule upper_le.ideal_principal)
    4.19  done
    4.20  
    4.21  interpretation upper_pd:
    4.22 -  bifinite_basis [upper_le approx_pd upper_principal Rep_upper_pd]
    4.23 +  ideal_completion [upper_le approx_pd upper_principal Rep_upper_pd]
    4.24  apply unfold_locales
    4.25  apply (rule approx_pd_upper_le)
    4.26  apply (rule approx_pd_idem)
    4.27 @@ -130,9 +130,12 @@
    4.28  done
    4.29  
    4.30  lemma upper_principal_less_iff [simp]:
    4.31 -  "(upper_principal t \<sqsubseteq> upper_principal u) = (t \<le>\<sharp> u)"
    4.32 -unfolding less_upper_pd_def Rep_upper_principal less_set_eq
    4.33 -by (fast intro: upper_le_refl elim: upper_le_trans)
    4.34 +  "upper_principal t \<sqsubseteq> upper_principal u \<longleftrightarrow> t \<le>\<sharp> u"
    4.35 +by (rule upper_pd.principal_less_iff)
    4.36 +
    4.37 +lemma upper_principal_eq_iff:
    4.38 +  "upper_principal t = upper_principal u \<longleftrightarrow> t \<le>\<sharp> u \<and> u \<le>\<sharp> t"
    4.39 +by (rule upper_pd.principal_eq_iff)
    4.40  
    4.41  lemma upper_principal_mono:
    4.42    "t \<le>\<sharp> u \<Longrightarrow> upper_principal t \<sqsubseteq> upper_principal u"
    4.43 @@ -145,7 +148,7 @@
    4.44  by (induct ys rule: upper_pd.principal_induct, simp, simp)
    4.45  
    4.46  instance upper_pd :: (bifinite) pcpo
    4.47 -by (intro_classes, fast intro: upper_pd_minimal)
    4.48 +by intro_classes (fast intro: upper_pd_minimal)
    4.49  
    4.50  lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
    4.51  by (rule upper_pd_minimal [THEN UU_I, symmetric])
    4.52 @@ -156,51 +159,27 @@
    4.53  instance upper_pd :: (profinite) approx ..
    4.54  
    4.55  defs (overloaded)
    4.56 -  approx_upper_pd_def:
    4.57 -    "approx \<equiv> (\<lambda>n. upper_pd.basis_fun (\<lambda>t. upper_principal (approx_pd n t)))"
    4.58 +  approx_upper_pd_def: "approx \<equiv> upper_pd.completion_approx"
    4.59 +
    4.60 +instance upper_pd :: (profinite) profinite
    4.61 +apply (intro_classes, unfold approx_upper_pd_def)
    4.62 +apply (simp add: upper_pd.chain_completion_approx)
    4.63 +apply (rule upper_pd.lub_completion_approx)
    4.64 +apply (rule upper_pd.completion_approx_idem)
    4.65 +apply (rule upper_pd.finite_fixes_completion_approx)
    4.66 +done
    4.67 +
    4.68 +instance upper_pd :: (bifinite) bifinite ..
    4.69  
    4.70  lemma approx_upper_principal [simp]:
    4.71    "approx n\<cdot>(upper_principal t) = upper_principal (approx_pd n t)"
    4.72  unfolding approx_upper_pd_def
    4.73 -apply (rule upper_pd.basis_fun_principal)
    4.74 -apply (erule upper_principal_mono [OF approx_pd_upper_mono])
    4.75 -done
    4.76 -
    4.77 -lemma chain_approx_upper_pd:
    4.78 -  "chain (approx :: nat \<Rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd)"
    4.79 -unfolding approx_upper_pd_def
    4.80 -by (rule upper_pd.chain_basis_fun_take)
    4.81 -
    4.82 -lemma lub_approx_upper_pd:
    4.83 -  "(\<Squnion>i. approx i\<cdot>xs) = (xs::'a upper_pd)"
    4.84 -unfolding approx_upper_pd_def
    4.85 -by (rule upper_pd.lub_basis_fun_take)
    4.86 -
    4.87 -lemma approx_upper_pd_idem:
    4.88 -  "approx n\<cdot>(approx n\<cdot>xs) = approx n\<cdot>(xs::'a upper_pd)"
    4.89 -apply (induct xs rule: upper_pd.principal_induct, simp)
    4.90 -apply (simp add: approx_pd_idem)
    4.91 -done
    4.92 +by (rule upper_pd.completion_approx_principal)
    4.93  
    4.94  lemma approx_eq_upper_principal:
    4.95    "\<exists>t\<in>Rep_upper_pd xs. approx n\<cdot>xs = upper_principal (approx_pd n t)"
    4.96  unfolding approx_upper_pd_def
    4.97 -by (rule upper_pd.basis_fun_take_eq_principal)
    4.98 -
    4.99 -lemma finite_fixes_approx_upper_pd:
   4.100 -  "finite {xs::'a upper_pd. approx n\<cdot>xs = xs}"
   4.101 -unfolding approx_upper_pd_def
   4.102 -by (rule upper_pd.finite_fixes_basis_fun_take)
   4.103 -
   4.104 -instance upper_pd :: (profinite) profinite
   4.105 -apply intro_classes
   4.106 -apply (simp add: chain_approx_upper_pd)
   4.107 -apply (rule lub_approx_upper_pd)
   4.108 -apply (rule approx_upper_pd_idem)
   4.109 -apply (rule finite_fixes_approx_upper_pd)
   4.110 -done
   4.111 -
   4.112 -instance upper_pd :: (bifinite) bifinite ..
   4.113 +by (rule upper_pd.completion_approx_eq_principal)
   4.114  
   4.115  lemma compact_imp_upper_principal:
   4.116    "compact xs \<Longrightarrow> \<exists>t. xs = upper_principal t"
   4.117 @@ -213,10 +192,7 @@
   4.118  
   4.119  lemma upper_principal_induct:
   4.120    "\<lbrakk>adm P; \<And>t. P (upper_principal t)\<rbrakk> \<Longrightarrow> P xs"
   4.121 -apply (erule approx_induct, rename_tac xs)
   4.122 -apply (cut_tac n=n and xs=xs in approx_eq_upper_principal)
   4.123 -apply (clarify, simp)
   4.124 -done
   4.125 +by (rule upper_pd.principal_induct)
   4.126  
   4.127  lemma upper_principal_induct2:
   4.128    "\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
   4.129 @@ -229,54 +205,12 @@
   4.130  done
   4.131  
   4.132  
   4.133 -subsection {* Monadic unit *}
   4.134 +subsection {* Monadic unit and plus *}
   4.135  
   4.136  definition
   4.137    upper_unit :: "'a \<rightarrow> 'a upper_pd" where
   4.138    "upper_unit = compact_basis.basis_fun (\<lambda>a. upper_principal (PDUnit a))"
   4.139  
   4.140 -lemma upper_unit_Rep_compact_basis [simp]:
   4.141 -  "upper_unit\<cdot>(Rep_compact_basis a) = upper_principal (PDUnit a)"
   4.142 -unfolding upper_unit_def
   4.143 -apply (rule compact_basis.basis_fun_principal)
   4.144 -apply (rule upper_principal_mono)
   4.145 -apply (erule PDUnit_upper_mono)
   4.146 -done
   4.147 -
   4.148 -lemma upper_unit_strict [simp]: "upper_unit\<cdot>\<bottom> = \<bottom>"
   4.149 -unfolding inst_upper_pd_pcpo Rep_compact_bot [symmetric] by simp
   4.150 -
   4.151 -lemma approx_upper_unit [simp]:
   4.152 -  "approx n\<cdot>(upper_unit\<cdot>x) = upper_unit\<cdot>(approx n\<cdot>x)"
   4.153 -apply (induct x rule: compact_basis_induct, simp)
   4.154 -apply (simp add: approx_Rep_compact_basis)
   4.155 -done
   4.156 -
   4.157 -lemma upper_unit_less_iff [simp]:
   4.158 -  "(upper_unit\<cdot>x \<sqsubseteq> upper_unit\<cdot>y) = (x \<sqsubseteq> y)"
   4.159 - apply (rule iffI)
   4.160 -  apply (rule bifinite_less_ext)
   4.161 -  apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   4.162 -  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   4.163 -  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
   4.164 -  apply (clarify, simp add: compact_le_def)
   4.165 - apply (erule monofun_cfun_arg)
   4.166 -done
   4.167 -
   4.168 -lemma upper_unit_eq_iff [simp]:
   4.169 -  "(upper_unit\<cdot>x = upper_unit\<cdot>y) = (x = y)"
   4.170 -unfolding po_eq_conv by simp
   4.171 -
   4.172 -lemma upper_unit_strict_iff [simp]: "(upper_unit\<cdot>x = \<bottom>) = (x = \<bottom>)"
   4.173 -unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
   4.174 -
   4.175 -lemma compact_upper_unit_iff [simp]:
   4.176 -  "compact (upper_unit\<cdot>x) = compact x"
   4.177 -unfolding bifinite_compact_iff by simp
   4.178 -
   4.179 -
   4.180 -subsection {* Monadic plus *}
   4.181 -
   4.182  definition
   4.183    upper_plus :: "'a upper_pd \<rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd" where
   4.184    "upper_plus = upper_pd.basis_fun (\<lambda>t. upper_pd.basis_fun (\<lambda>u.
   4.185 @@ -287,67 +221,89 @@
   4.186      (infixl "+\<sharp>" 65) where
   4.187    "xs +\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys"
   4.188  
   4.189 +syntax
   4.190 +  "_upper_pd" :: "args \<Rightarrow> 'a upper_pd" ("{_}\<sharp>")
   4.191 +
   4.192 +translations
   4.193 +  "{x,xs}\<sharp>" == "{x}\<sharp> +\<sharp> {xs}\<sharp>"
   4.194 +  "{x}\<sharp>" == "CONST upper_unit\<cdot>x"
   4.195 +
   4.196 +lemma upper_unit_Rep_compact_basis [simp]:
   4.197 +  "{Rep_compact_basis a}\<sharp> = upper_principal (PDUnit a)"
   4.198 +unfolding upper_unit_def
   4.199 +by (simp add: compact_basis.basis_fun_principal
   4.200 +    upper_principal_mono PDUnit_upper_mono)
   4.201 +
   4.202  lemma upper_plus_principal [simp]:
   4.203 -  "upper_plus\<cdot>(upper_principal t)\<cdot>(upper_principal u) =
   4.204 -   upper_principal (PDPlus t u)"
   4.205 +  "upper_principal t +\<sharp> upper_principal u = upper_principal (PDPlus t u)"
   4.206  unfolding upper_plus_def
   4.207  by (simp add: upper_pd.basis_fun_principal
   4.208      upper_pd.basis_fun_mono PDPlus_upper_mono)
   4.209  
   4.210 +lemma approx_upper_unit [simp]:
   4.211 +  "approx n\<cdot>{x}\<sharp> = {approx n\<cdot>x}\<sharp>"
   4.212 +apply (induct x rule: compact_basis_induct, simp)
   4.213 +apply (simp add: approx_Rep_compact_basis)
   4.214 +done
   4.215 +
   4.216  lemma approx_upper_plus [simp]:
   4.217 -  "approx n\<cdot>(upper_plus\<cdot>xs\<cdot>ys) = upper_plus\<cdot>(approx n\<cdot>xs)\<cdot>(approx n\<cdot>ys)"
   4.218 +  "approx n\<cdot>(xs +\<sharp> ys) = (approx n\<cdot>xs) +\<sharp> (approx n\<cdot>ys)"
   4.219  by (induct xs ys rule: upper_principal_induct2, simp, simp, simp)
   4.220  
   4.221 -lemma upper_plus_commute: "upper_plus\<cdot>xs\<cdot>ys = upper_plus\<cdot>ys\<cdot>xs"
   4.222 -apply (induct xs ys rule: upper_principal_induct2, simp, simp)
   4.223 -apply (simp add: PDPlus_commute)
   4.224 -done
   4.225 -
   4.226 -lemma upper_plus_assoc:
   4.227 -  "upper_plus\<cdot>(upper_plus\<cdot>xs\<cdot>ys)\<cdot>zs = upper_plus\<cdot>xs\<cdot>(upper_plus\<cdot>ys\<cdot>zs)"
   4.228 +lemma upper_plus_assoc: "(xs +\<sharp> ys) +\<sharp> zs = xs +\<sharp> (ys +\<sharp> zs)"
   4.229  apply (induct xs ys arbitrary: zs rule: upper_principal_induct2, simp, simp)
   4.230  apply (rule_tac xs=zs in upper_principal_induct, simp)
   4.231  apply (simp add: PDPlus_assoc)
   4.232  done
   4.233  
   4.234 -lemma upper_plus_absorb: "upper_plus\<cdot>xs\<cdot>xs = xs"
   4.235 +lemma upper_plus_commute: "xs +\<sharp> ys = ys +\<sharp> xs"
   4.236 +apply (induct xs ys rule: upper_principal_induct2, simp, simp)
   4.237 +apply (simp add: PDPlus_commute)
   4.238 +done
   4.239 +
   4.240 +lemma upper_plus_absorb: "xs +\<sharp> xs = xs"
   4.241  apply (induct xs rule: upper_principal_induct, simp)
   4.242  apply (simp add: PDPlus_absorb)
   4.243  done
   4.244  
   4.245 -lemma upper_plus_less1: "upper_plus\<cdot>xs\<cdot>ys \<sqsubseteq> xs"
   4.246 +interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\<sharp>"]
   4.247 +  by unfold_locales
   4.248 +    (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+
   4.249 +
   4.250 +lemma upper_plus_left_commute: "xs +\<sharp> (ys +\<sharp> zs) = ys +\<sharp> (xs +\<sharp> zs)"
   4.251 +by (rule aci_upper_plus.mult_left_commute)
   4.252 +
   4.253 +lemma upper_plus_left_absorb: "xs +\<sharp> (xs +\<sharp> ys) = xs +\<sharp> ys"
   4.254 +by (rule aci_upper_plus.mult_left_idem)
   4.255 +
   4.256 +lemmas upper_plus_aci = aci_upper_plus.mult_ac_idem
   4.257 +
   4.258 +lemma upper_plus_less1: "xs +\<sharp> ys \<sqsubseteq> xs"
   4.259  apply (induct xs ys rule: upper_principal_induct2, simp, simp)
   4.260  apply (simp add: PDPlus_upper_less)
   4.261  done
   4.262  
   4.263 -lemma upper_plus_less2: "upper_plus\<cdot>xs\<cdot>ys \<sqsubseteq> ys"
   4.264 +lemma upper_plus_less2: "xs +\<sharp> ys \<sqsubseteq> ys"
   4.265  by (subst upper_plus_commute, rule upper_plus_less1)
   4.266  
   4.267 -lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> upper_plus\<cdot>ys\<cdot>zs"
   4.268 +lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> ys +\<sharp> zs"
   4.269  apply (subst upper_plus_absorb [of xs, symmetric])
   4.270  apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
   4.271  done
   4.272  
   4.273  lemma upper_less_plus_iff:
   4.274 -  "(xs \<sqsubseteq> upper_plus\<cdot>ys\<cdot>zs) = (xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs)"
   4.275 +  "xs \<sqsubseteq> ys +\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs"
   4.276  apply safe
   4.277  apply (erule trans_less [OF _ upper_plus_less1])
   4.278  apply (erule trans_less [OF _ upper_plus_less2])
   4.279  apply (erule (1) upper_plus_greatest)
   4.280  done
   4.281  
   4.282 -lemma upper_plus_strict1 [simp]: "upper_plus\<cdot>\<bottom>\<cdot>ys = \<bottom>"
   4.283 -by (rule UU_I, rule upper_plus_less1)
   4.284 -
   4.285 -lemma upper_plus_strict2 [simp]: "upper_plus\<cdot>xs\<cdot>\<bottom> = \<bottom>"
   4.286 -by (rule UU_I, rule upper_plus_less2)
   4.287 -
   4.288  lemma upper_plus_less_unit_iff:
   4.289 -  "(upper_plus\<cdot>xs\<cdot>ys \<sqsubseteq> upper_unit\<cdot>z) =
   4.290 -    (xs \<sqsubseteq> upper_unit\<cdot>z \<or> ys \<sqsubseteq> upper_unit\<cdot>z)"
   4.291 +  "xs +\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>"
   4.292   apply (rule iffI)
   4.293    apply (subgoal_tac
   4.294 -    "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>(upper_unit\<cdot>z) \<or> f\<cdot>ys \<sqsubseteq> f\<cdot>(upper_unit\<cdot>z))")
   4.295 +    "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>{z}\<sharp> \<or> f\<cdot>ys \<sqsubseteq> f\<cdot>{z}\<sharp>)")
   4.296     apply (drule admD, rule chain_approx)
   4.297      apply (drule_tac f="approx i" in monofun_cfun_arg)
   4.298      apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_upper_principal, simp)
   4.299 @@ -361,19 +317,62 @@
   4.300   apply (erule trans_less [OF upper_plus_less2])
   4.301  done
   4.302  
   4.303 +lemma upper_unit_less_iff [simp]: "{x}\<sharp> \<sqsubseteq> {y}\<sharp> \<longleftrightarrow> x \<sqsubseteq> y"
   4.304 + apply (rule iffI)
   4.305 +  apply (rule bifinite_less_ext)
   4.306 +  apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
   4.307 +  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
   4.308 +  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
   4.309 +  apply (clarify, simp add: compact_le_def)
   4.310 + apply (erule monofun_cfun_arg)
   4.311 +done
   4.312 +
   4.313  lemmas upper_pd_less_simps =
   4.314    upper_unit_less_iff
   4.315    upper_less_plus_iff
   4.316    upper_plus_less_unit_iff
   4.317  
   4.318 +lemma upper_unit_eq_iff [simp]: "{x}\<sharp> = {y}\<sharp> \<longleftrightarrow> x = y"
   4.319 +unfolding po_eq_conv by simp
   4.320 +
   4.321 +lemma upper_unit_strict [simp]: "{\<bottom>}\<sharp> = \<bottom>"
   4.322 +unfolding inst_upper_pd_pcpo Rep_compact_bot [symmetric] by simp
   4.323 +
   4.324 +lemma upper_plus_strict1 [simp]: "\<bottom> +\<sharp> ys = \<bottom>"
   4.325 +by (rule UU_I, rule upper_plus_less1)
   4.326 +
   4.327 +lemma upper_plus_strict2 [simp]: "xs +\<sharp> \<bottom> = \<bottom>"
   4.328 +by (rule UU_I, rule upper_plus_less2)
   4.329 +
   4.330 +lemma upper_unit_strict_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
   4.331 +unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
   4.332 +
   4.333 +lemma upper_plus_strict_iff [simp]:
   4.334 +  "xs +\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>"
   4.335 +apply (rule iffI)
   4.336 +apply (erule rev_mp)
   4.337 +apply (rule upper_principal_induct2 [where xs=xs and ys=ys], simp, simp)
   4.338 +apply (simp add: inst_upper_pd_pcpo upper_principal_eq_iff
   4.339 +                 upper_le_PDPlus_PDUnit_iff)
   4.340 +apply auto
   4.341 +done
   4.342 +
   4.343 +lemma compact_upper_unit_iff [simp]: "compact {x}\<sharp> \<longleftrightarrow> compact x"
   4.344 +unfolding bifinite_compact_iff by simp
   4.345 +
   4.346 +lemma compact_upper_plus [simp]:
   4.347 +  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<sharp> ys)"
   4.348 +apply (drule compact_imp_upper_principal)+
   4.349 +apply (auto simp add: compact_upper_principal)
   4.350 +done
   4.351 +
   4.352  
   4.353  subsection {* Induction rules *}
   4.354  
   4.355  lemma upper_pd_induct1:
   4.356    assumes P: "adm P"
   4.357 -  assumes unit: "\<And>x. P (upper_unit\<cdot>x)"
   4.358 -  assumes insert:
   4.359 -    "\<And>x ys. \<lbrakk>P (upper_unit\<cdot>x); P ys\<rbrakk> \<Longrightarrow> P (upper_plus\<cdot>(upper_unit\<cdot>x)\<cdot>ys)"
   4.360 +  assumes unit: "\<And>x. P {x}\<sharp>"
   4.361 +  assumes insert: "\<And>x ys. \<lbrakk>P {x}\<sharp>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<sharp> +\<sharp> ys)"
   4.362    shows "P (xs::'a upper_pd)"
   4.363  apply (induct xs rule: upper_principal_induct, rule P)
   4.364  apply (induct_tac t rule: pd_basis_induct1)
   4.365 @@ -386,8 +385,8 @@
   4.366  
   4.367  lemma upper_pd_induct:
   4.368    assumes P: "adm P"
   4.369 -  assumes unit: "\<And>x. P (upper_unit\<cdot>x)"
   4.370 -  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (upper_plus\<cdot>xs\<cdot>ys)"
   4.371 +  assumes unit: "\<And>x. P {x}\<sharp>"
   4.372 +  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<sharp> ys)"
   4.373    shows "P (xs::'a upper_pd)"
   4.374  apply (induct xs rule: upper_principal_induct, rule P)
   4.375  apply (induct_tac t rule: pd_basis_induct)
   4.376 @@ -403,9 +402,10 @@
   4.377    "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where
   4.378    "upper_bind_basis = fold_pd
   4.379      (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
   4.380 -    (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
   4.381 +    (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
   4.382  
   4.383 -lemma ACI_upper_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
   4.384 +lemma ACI_upper_bind:
   4.385 +  "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
   4.386  apply unfold_locales
   4.387  apply (simp add: upper_plus_assoc)
   4.388  apply (simp add: upper_plus_commute)
   4.389 @@ -416,11 +416,11 @@
   4.390    "upper_bind_basis (PDUnit a) =
   4.391      (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   4.392    "upper_bind_basis (PDPlus t u) =
   4.393 -    (\<Lambda> f. upper_plus\<cdot>(upper_bind_basis t\<cdot>f)\<cdot>(upper_bind_basis u\<cdot>f))"
   4.394 +    (\<Lambda> f. upper_bind_basis t\<cdot>f +\<sharp> upper_bind_basis u\<cdot>f)"
   4.395  unfolding upper_bind_basis_def
   4.396  apply -
   4.397 -apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_upper_bind])
   4.398 -apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_upper_bind])
   4.399 +apply (rule fold_pd_PDUnit [OF ACI_upper_bind])
   4.400 +apply (rule fold_pd_PDPlus [OF ACI_upper_bind])
   4.401  done
   4.402  
   4.403  lemma upper_bind_basis_mono:
   4.404 @@ -444,12 +444,11 @@
   4.405  done
   4.406  
   4.407  lemma upper_bind_unit [simp]:
   4.408 -  "upper_bind\<cdot>(upper_unit\<cdot>x)\<cdot>f = f\<cdot>x"
   4.409 +  "upper_bind\<cdot>{x}\<sharp>\<cdot>f = f\<cdot>x"
   4.410  by (induct x rule: compact_basis_induct, simp, simp)
   4.411  
   4.412  lemma upper_bind_plus [simp]:
   4.413 -  "upper_bind\<cdot>(upper_plus\<cdot>xs\<cdot>ys)\<cdot>f =
   4.414 -   upper_plus\<cdot>(upper_bind\<cdot>xs\<cdot>f)\<cdot>(upper_bind\<cdot>ys\<cdot>f)"
   4.415 +  "upper_bind\<cdot>(xs +\<sharp> ys)\<cdot>f = upper_bind\<cdot>xs\<cdot>f +\<sharp> upper_bind\<cdot>ys\<cdot>f"
   4.416  by (induct xs ys rule: upper_principal_induct2, simp, simp, simp)
   4.417  
   4.418  lemma upper_bind_strict [simp]: "upper_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
   4.419 @@ -460,28 +459,26 @@
   4.420  
   4.421  definition
   4.422    upper_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a upper_pd \<rightarrow> 'b upper_pd" where
   4.423 -  "upper_map = (\<Lambda> f xs. upper_bind\<cdot>xs\<cdot>(\<Lambda> x. upper_unit\<cdot>(f\<cdot>x)))"
   4.424 +  "upper_map = (\<Lambda> f xs. upper_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<sharp>))"
   4.425  
   4.426  definition
   4.427    upper_join :: "'a upper_pd upper_pd \<rightarrow> 'a upper_pd" where
   4.428    "upper_join = (\<Lambda> xss. upper_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"
   4.429  
   4.430  lemma upper_map_unit [simp]:
   4.431 -  "upper_map\<cdot>f\<cdot>(upper_unit\<cdot>x) = upper_unit\<cdot>(f\<cdot>x)"
   4.432 +  "upper_map\<cdot>f\<cdot>{x}\<sharp> = {f\<cdot>x}\<sharp>"
   4.433  unfolding upper_map_def by simp
   4.434  
   4.435  lemma upper_map_plus [simp]:
   4.436 -  "upper_map\<cdot>f\<cdot>(upper_plus\<cdot>xs\<cdot>ys) =
   4.437 -   upper_plus\<cdot>(upper_map\<cdot>f\<cdot>xs)\<cdot>(upper_map\<cdot>f\<cdot>ys)"
   4.438 +  "upper_map\<cdot>f\<cdot>(xs +\<sharp> ys) = upper_map\<cdot>f\<cdot>xs +\<sharp> upper_map\<cdot>f\<cdot>ys"
   4.439  unfolding upper_map_def by simp
   4.440  
   4.441  lemma upper_join_unit [simp]:
   4.442 -  "upper_join\<cdot>(upper_unit\<cdot>xs) = xs"
   4.443 +  "upper_join\<cdot>{xs}\<sharp> = xs"
   4.444  unfolding upper_join_def by simp
   4.445  
   4.446  lemma upper_join_plus [simp]:
   4.447 -  "upper_join\<cdot>(upper_plus\<cdot>xss\<cdot>yss) =
   4.448 -   upper_plus\<cdot>(upper_join\<cdot>xss)\<cdot>(upper_join\<cdot>yss)"
   4.449 +  "upper_join\<cdot>(xss +\<sharp> yss) = upper_join\<cdot>xss +\<sharp> upper_join\<cdot>yss"
   4.450  unfolding upper_join_def by simp
   4.451  
   4.452  lemma upper_map_ident: "upper_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"