# HG changeset patch
# User huffman
# Date 1210973137 -7200
# Node ID 8684b5240f111266d155a43f738e670ad29dde33
# Parent  19d8783a30de8b7e74135ce1a775eba628803a10
rename locales;
add completion_approx constant to ideal_completion locale;
add new set-like syntax for powerdomains;
reorganized proofs

diff -r 19d8783a30de -r 8684b5240f11 src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Fri May 16 22:35:25 2008 +0200
+++ b/src/HOLCF/CompactBasis.thy	Fri May 16 23:25:37 2008 +0200
@@ -52,7 +52,7 @@
 lemma ideal_principal: "ideal {x. x \<sqsubseteq> z}"
 apply (rule idealI)
 apply (rule_tac x=z in exI)
-apply (fast intro: refl)
+apply fast
 apply (rule_tac x=z in bexI, fast)
 apply fast
 apply (fast intro: trans_less)
@@ -116,7 +116,7 @@
 lemma is_lub_thelub0: "\<lbrakk>\<exists>u. S <<| u; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> x"
 by (erule exE, drule lubI, erule is_lub_lub)
 
-locale plotkin_order = preorder r +
+locale basis_take = preorder r +
   fixes take :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'a"
   assumes take_less: "r (take n a) a"
   assumes take_take: "take n (take n a) = take n a"
@@ -125,28 +125,28 @@
   assumes finite_range_take: "finite (range (take n))"
   assumes take_covers: "\<exists>n. take n a = a"
 
-locale bifinite_basis = plotkin_order r +
+locale ideal_completion = basis_take r +
   fixes principal :: "'a::type \<Rightarrow> 'b::cpo"
-  fixes approxes :: "'b::cpo \<Rightarrow> 'a::type set"
-  assumes ideal_approxes: "\<And>x. preorder.ideal r (approxes x)"
-  assumes cont_approxes: "cont approxes"
-  assumes approxes_principal: "\<And>a. approxes (principal a) = {b. r b a}"
-  assumes subset_approxesD: "\<And>x y. approxes x \<subseteq> approxes y \<Longrightarrow> x \<sqsubseteq> y"
+  fixes rep :: "'b::cpo \<Rightarrow> 'a::type set"
+  assumes ideal_rep: "\<And>x. preorder.ideal r (rep x)"
+  assumes cont_rep: "cont rep"
+  assumes rep_principal: "\<And>a. rep (principal a) = {b. r b a}"
+  assumes subset_repD: "\<And>x y. rep x \<subseteq> rep y \<Longrightarrow> x \<sqsubseteq> y"
 begin
 
-lemma finite_take_approxes: "finite (take n ` approxes x)"
+lemma finite_take_rep: "finite (take n ` rep x)"
 by (rule finite_subset [OF image_mono [OF subset_UNIV] finite_range_take])
 
 lemma basis_fun_lemma0:
   fixes f :: "'a::type \<Rightarrow> 'c::cpo"
   assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
-  shows "\<exists>u. f ` take i ` approxes x <<| u"
+  shows "\<exists>u. f ` take i ` rep x <<| u"
 apply (rule finite_directed_has_lub)
 apply (rule finite_imageI)
-apply (rule finite_take_approxes)
+apply (rule finite_take_rep)
 apply (subst image_image)
 apply (rule directed_image_ideal)
-apply (rule ideal_approxes)
+apply (rule ideal_rep)
 apply (rule f_mono)
 apply (erule take_mono)
 done
@@ -154,7 +154,7 @@
 lemma basis_fun_lemma1:
   fixes f :: "'a::type \<Rightarrow> 'c::cpo"
   assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
-  shows "chain (\<lambda>i. lub (f ` take i ` approxes x))"
+  shows "chain (\<lambda>i. lub (f ` take i ` rep x))"
  apply (rule chainI)
  apply (rule is_lub_thelub0)
   apply (rule basis_fun_lemma0, erule f_mono)
@@ -168,7 +168,7 @@
 lemma basis_fun_lemma2:
   fixes f :: "'a::type \<Rightarrow> 'c::cpo"
   assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
-  shows "f ` approxes x <<| (\<Squnion>i. lub (f ` take i ` approxes x))"
+  shows "f ` rep x <<| (\<Squnion>i. lub (f ` take i ` rep x))"
  apply (rule is_lubI)
  apply (rule ub_imageI, rename_tac a)
   apply (cut_tac a=a in take_covers, erule exE, rename_tac i)
@@ -191,74 +191,80 @@
 lemma basis_fun_lemma:
   fixes f :: "'a::type \<Rightarrow> 'c::cpo"
   assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
-  shows "\<exists>u. f ` approxes x <<| u"
+  shows "\<exists>u. f ` rep x <<| u"
 by (rule exI, rule basis_fun_lemma2, erule f_mono)
 
-lemma approxes_mono: "x \<sqsubseteq> y \<Longrightarrow> approxes x \<subseteq> approxes y"
-apply (drule cont_approxes [THEN cont2mono, THEN monofunE])
+lemma rep_mono: "x \<sqsubseteq> y \<Longrightarrow> rep x \<subseteq> rep y"
+apply (drule cont_rep [THEN cont2mono, THEN monofunE])
 apply (simp add: set_cpo_simps)
 done
 
-lemma approxes_contlub:
-  "chain Y \<Longrightarrow> approxes (\<Squnion>i. Y i) = (\<Union>i. approxes (Y i))"
-by (simp add: cont2contlubE [OF cont_approxes] set_cpo_simps)
+lemma rep_contlub:
+  "chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))"
+by (simp add: cont2contlubE [OF cont_rep] set_cpo_simps)
 
-lemma less_def: "(x \<sqsubseteq> y) = (approxes x \<subseteq> approxes y)"
-by (rule iffI [OF approxes_mono subset_approxesD])
+lemma less_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y"
+by (rule iffI [OF rep_mono subset_repD])
 
-lemma approxes_eq: "approxes x = {a. principal a \<sqsubseteq> x}"
-unfolding less_def approxes_principal
+lemma rep_eq: "rep x = {a. principal a \<sqsubseteq> x}"
+unfolding less_def rep_principal
 apply safe
-apply (erule (1) idealD3 [OF ideal_approxes])
+apply (erule (1) idealD3 [OF ideal_rep])
 apply (erule subsetD, simp add: refl)
 done
 
-lemma mem_approxes_iff: "(a \<in> approxes x) = (principal a \<sqsubseteq> x)"
-by (simp add: approxes_eq)
+lemma mem_rep_iff_principal_less: "a \<in> rep x \<longleftrightarrow> principal a \<sqsubseteq> x"
+by (simp add: rep_eq)
+
+lemma principal_less_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x"
+by (simp add: rep_eq)
 
-lemma principal_less_iff: "(principal a \<sqsubseteq> x) = (a \<in> approxes x)"
-by (simp add: approxes_eq)
+lemma principal_less_iff: "principal a \<sqsubseteq> principal b \<longleftrightarrow> r a b"
+by (simp add: principal_less_iff_mem_rep rep_principal)
 
-lemma approxesD: "a \<in> approxes x \<Longrightarrow> principal a \<sqsubseteq> x"
-by (simp add: approxes_eq)
+lemma principal_eq_iff: "principal a = principal b \<longleftrightarrow> r a b \<and> r b a"
+unfolding po_eq_conv [where 'a='b] principal_less_iff ..
+
+lemma repD: "a \<in> rep x \<Longrightarrow> principal a \<sqsubseteq> x"
+by (simp add: rep_eq)
 
 lemma principal_mono: "r a b \<Longrightarrow> principal a \<sqsubseteq> principal b"
-by (rule approxesD, simp add: approxes_principal)
+by (simp add: principal_less_iff)
 
 lemma lessI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
-unfolding principal_less_iff
+unfolding principal_less_iff_mem_rep
 by (simp add: less_def subset_eq)
 
-lemma lub_principal_approxes: "principal ` approxes x <<| x"
+lemma lub_principal_rep: "principal ` rep x <<| x"
 apply (rule is_lubI)
 apply (rule ub_imageI)
-apply (erule approxesD)
+apply (erule repD)
 apply (subst less_def)
 apply (rule subsetI)
 apply (drule (1) ub_imageD)
-apply (simp add: approxes_eq)
+apply (simp add: rep_eq)
 done
 
 definition
   basis_fun :: "('a::type \<Rightarrow> 'c::cpo) \<Rightarrow> 'b \<rightarrow> 'c" where
-  "basis_fun = (\<lambda>f. (\<Lambda> x. lub (f ` approxes x)))"
+  "basis_fun = (\<lambda>f. (\<Lambda> x. lub (f ` rep x)))"
 
 lemma basis_fun_beta:
   fixes f :: "'a::type \<Rightarrow> 'c::cpo"
   assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
-  shows "basis_fun f\<cdot>x = lub (f ` approxes x)"
+  shows "basis_fun f\<cdot>x = lub (f ` rep x)"
 unfolding basis_fun_def
 proof (rule beta_cfun)
-  have lub: "\<And>x. \<exists>u. f ` approxes x <<| u"
+  have lub: "\<And>x. \<exists>u. f ` rep x <<| u"
     using f_mono by (rule basis_fun_lemma)
-  show cont: "cont (\<lambda>x. lub (f ` approxes x))"
+  show cont: "cont (\<lambda>x. lub (f ` rep x))"
     apply (rule contI2)
      apply (rule monofunI)
      apply (rule is_lub_thelub0 [OF lub ub_imageI])
      apply (rule is_ub_thelub0 [OF lub imageI])
-     apply (erule (1) subsetD [OF approxes_mono])
+     apply (erule (1) subsetD [OF rep_mono])
     apply (rule is_lub_thelub0 [OF lub ub_imageI])
-    apply (simp add: approxes_contlub, clarify)
+    apply (simp add: rep_contlub, clarify)
     apply (erule rev_trans_less [OF is_ub_thelub])
     apply (erule is_ub_thelub0 [OF lub imageI])
     done
@@ -269,7 +275,7 @@
   assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
   shows "basis_fun f\<cdot>(principal a) = f a"
 apply (subst basis_fun_beta, erule f_mono)
-apply (subst approxes_principal)
+apply (subst rep_principal)
 apply (rule lub_image_principal, erule f_mono)
 done
 
@@ -290,10 +296,24 @@
 done
 
 lemma compact_principal: "compact (principal a)"
-by (rule compactI2, simp add: principal_less_iff approxes_contlub)
+by (rule compactI2, simp add: principal_less_iff_mem_rep rep_contlub)
+
+definition
+  completion_approx :: "nat \<Rightarrow> 'b \<rightarrow> 'b" where
+  "completion_approx = (\<lambda>i. basis_fun (\<lambda>a. principal (take i a)))"
 
-lemma chain_basis_fun_take:
-  "chain (\<lambda>i. basis_fun (\<lambda>a. principal (take i a)))"
+lemma completion_approx_beta:
+  "completion_approx i\<cdot>x = (\<Squnion>a\<in>rep x. principal (take i a))"
+unfolding completion_approx_def
+by (simp add: basis_fun_beta principal_mono take_mono)
+
+lemma completion_approx_principal:
+  "completion_approx i\<cdot>(principal a) = principal (take i a)"
+unfolding completion_approx_def
+by (simp add: basis_fun_principal principal_mono take_mono)
+
+lemma chain_completion_approx: "chain completion_approx"
+unfolding completion_approx_def
 apply (rule chainI)
 apply (rule basis_fun_mono)
 apply (erule principal_mono [OF take_mono])
@@ -301,53 +321,56 @@
 apply (rule principal_mono [OF take_chain])
 done
 
-lemma lub_basis_fun_take:
-  "(\<Squnion>i. basis_fun (\<lambda>a. principal (take i a))\<cdot>x) = x"
- apply (simp add: basis_fun_beta principal_mono take_mono)
+lemma lub_completion_approx: "(\<Squnion>i. completion_approx i\<cdot>x) = x"
+unfolding completion_approx_beta
  apply (subst image_image [where f=principal, symmetric])
- apply (rule unique_lub [OF _ lub_principal_approxes])
+ apply (rule unique_lub [OF _ lub_principal_rep])
  apply (rule basis_fun_lemma2, erule principal_mono)
 done
 
-lemma basis_fun_take_eq_principal:
-  "\<exists>a\<in>approxes x.
-    basis_fun (\<lambda>a. principal (take i a))\<cdot>x = principal (take i a)"
- apply (simp add: basis_fun_beta principal_mono take_mono)
+lemma completion_approx_eq_principal:
+  "\<exists>a\<in>rep x. completion_approx i\<cdot>x = principal (take i a)"
+unfolding completion_approx_beta
  apply (subst image_image [where f=principal, symmetric])
- apply (subgoal_tac "finite (principal ` take i ` approxes x)")
-  apply (subgoal_tac "directed (principal ` take i ` approxes x)")
+ apply (subgoal_tac "finite (principal ` take i ` rep x)")
+  apply (subgoal_tac "directed (principal ` take i ` rep x)")
    apply (drule (1) lub_finite_directed_in_self, fast)
   apply (subst image_image)
   apply (rule directed_image_ideal)
-   apply (rule ideal_approxes)
+   apply (rule ideal_rep)
   apply (erule principal_mono [OF take_mono])
  apply (rule finite_imageI)
- apply (rule finite_take_approxes)
+ apply (rule finite_take_rep)
+done
+
+lemma completion_approx_idem:
+  "completion_approx i\<cdot>(completion_approx i\<cdot>x) = completion_approx i\<cdot>x"
+using completion_approx_eq_principal [where i=i and x=x]
+by (auto simp add: completion_approx_principal take_take)
+
+lemma finite_fixes_completion_approx:
+  "finite {x. completion_approx i\<cdot>x = x}" (is "finite ?S")
+apply (subgoal_tac "?S \<subseteq> principal ` range (take i)")
+apply (erule finite_subset)
+apply (rule finite_imageI)
+apply (rule finite_range_take)
+apply (clarify, erule subst)
+apply (cut_tac x=x and i=i in completion_approx_eq_principal)
+apply fast
 done
 
 lemma principal_induct:
   assumes adm: "adm P"
   assumes P: "\<And>a. P (principal a)"
   shows "P x"
- apply (subgoal_tac "P (\<Squnion>i. basis_fun (\<lambda>a. principal (take i a))\<cdot>x)")
- apply (simp add: lub_basis_fun_take)
+ apply (subgoal_tac "P (\<Squnion>i. completion_approx i\<cdot>x)")
+ apply (simp add: lub_completion_approx)
  apply (rule admD [OF adm])
-  apply (simp add: chain_basis_fun_take)
- apply (cut_tac x=x and i=i in basis_fun_take_eq_principal)
+  apply (simp add: chain_completion_approx)
+ apply (cut_tac x=x and i=i in completion_approx_eq_principal)
  apply (clarify, simp add: P)
 done
 
-lemma finite_fixes_basis_fun_take:
-  "finite {x. basis_fun (\<lambda>a. principal (take i a))\<cdot>x = x}" (is "finite ?S")
-apply (subgoal_tac "?S \<subseteq> principal ` range (take i)")
-apply (erule finite_subset)
-apply (rule finite_imageI)
-apply (rule finite_range_take)
-apply (clarify, erule subst)
-apply (cut_tac x=x and i=i in basis_fun_take_eq_principal)
-apply fast
-done
-
 end
 
 
@@ -359,7 +382,7 @@
 by (fast intro: compact_approx)
 
 lemma compact_Rep_compact_basis [simp]: "compact (Rep_compact_basis a)"
-by (rule Rep_compact_basis [simplified])
+by (rule Rep_compact_basis [unfolded mem_Collect_eq])
 
 lemma Rep_Abs_compact_basis_approx [simp]:
   "Rep_compact_basis (Abs_compact_basis (approx n\<cdot>x)) = approx n\<cdot>x"
@@ -520,7 +543,7 @@
 done
 
 interpretation compact_basis:
-  bifinite_basis [sq_le compact_approx Rep_compact_basis compacts]
+  ideal_completion [sq_le compact_approx Rep_compact_basis compacts]
 proof (unfold_locales)
   fix n :: nat and a b :: "'a compact_basis" and x :: "'a"
   show "compact_approx n a \<sqsubseteq> a"
@@ -620,12 +643,14 @@
     "('a compact_basis \<Rightarrow> 'b::type) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a pd_basis \<Rightarrow> 'b"
   where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
 
-lemma (in ab_semigroup_idem_mult) fold_pd_PDUnit:
-  "fold_pd g (op *) (PDUnit x) = g x"
+lemma fold_pd_PDUnit:
+  includes ab_semigroup_idem_mult f
+  shows "fold_pd g f (PDUnit x) = g x"
 unfolding fold_pd_def Rep_PDUnit by simp
 
-lemma (in ab_semigroup_idem_mult) fold_pd_PDPlus:
-  "fold_pd g (op *) (PDPlus t u) = fold_pd g (op *) t * fold_pd g (op *) u"
+lemma fold_pd_PDPlus:
+  includes ab_semigroup_idem_mult f
+  shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
 unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
 
 text {* approx-pd *}
diff -r 19d8783a30de -r 8684b5240f11 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Fri May 16 22:35:25 2008 +0200
+++ b/src/HOLCF/ConvexPD.thy	Fri May 16 23:25:37 2008 +0200
@@ -148,14 +148,11 @@
 done
 
 lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)"
-by (rule Rep_convex_pd [simplified])
+by (rule Rep_convex_pd [unfolded mem_Collect_eq])
 
 lemma Rep_convex_pd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> Rep_convex_pd xs \<subseteq> Rep_convex_pd ys"
 unfolding less_convex_pd_def less_set_eq .
 
-
-subsection {* Principal ideals *}
-
 definition
   convex_principal :: "'a pd_basis \<Rightarrow> 'a convex_pd" where
   "convex_principal t = Abs_convex_pd {u. u \<le>\<natural> t}"
@@ -168,7 +165,7 @@
 done
 
 interpretation convex_pd:
-  bifinite_basis [convex_le approx_pd convex_principal Rep_convex_pd]
+  ideal_completion [convex_le approx_pd convex_principal Rep_convex_pd]
 apply unfold_locales
 apply (rule approx_pd_convex_le)
 apply (rule approx_pd_idem)
@@ -183,13 +180,16 @@
 done
 
 lemma convex_principal_less_iff [simp]:
-  "(convex_principal t \<sqsubseteq> convex_principal u) = (t \<le>\<natural> u)"
-unfolding less_convex_pd_def Rep_convex_principal less_set_eq
-by (fast intro: convex_le_refl elim: convex_le_trans)
+  "convex_principal t \<sqsubseteq> convex_principal u \<longleftrightarrow> t \<le>\<natural> u"
+by (rule convex_pd.principal_less_iff)
+
+lemma convex_principal_eq_iff [simp]:
+  "convex_principal t = convex_principal u \<longleftrightarrow> t \<le>\<natural> u \<and> u \<le>\<natural> t"
+by (rule convex_pd.principal_eq_iff)
 
 lemma convex_principal_mono:
   "t \<le>\<natural> u \<Longrightarrow> convex_principal t \<sqsubseteq> convex_principal u"
-by (rule convex_principal_less_iff [THEN iffD2])
+by (rule convex_pd.principal_mono)
 
 lemma compact_convex_principal: "compact (convex_principal t)"
 by (rule convex_pd.compact_principal)
@@ -198,7 +198,7 @@
 by (induct ys rule: convex_pd.principal_induct, simp, simp)
 
 instance convex_pd :: (bifinite) pcpo
-by (intro_classes, fast intro: convex_pd_minimal)
+by intro_classes (fast intro: convex_pd_minimal)
 
 lemma inst_convex_pd_pcpo: "\<bottom> = convex_principal (PDUnit compact_bot)"
 by (rule convex_pd_minimal [THEN UU_I, symmetric])
@@ -209,51 +209,27 @@
 instance convex_pd :: (profinite) approx ..
 
 defs (overloaded)
-  approx_convex_pd_def:
-    "approx \<equiv> (\<lambda>n. convex_pd.basis_fun (\<lambda>t. convex_principal (approx_pd n t)))"
+  approx_convex_pd_def: "approx \<equiv> convex_pd.completion_approx"
+
+instance convex_pd :: (profinite) profinite
+apply (intro_classes, unfold approx_convex_pd_def)
+apply (simp add: convex_pd.chain_completion_approx)
+apply (rule convex_pd.lub_completion_approx)
+apply (rule convex_pd.completion_approx_idem)
+apply (rule convex_pd.finite_fixes_completion_approx)
+done
+
+instance convex_pd :: (bifinite) bifinite ..
 
 lemma approx_convex_principal [simp]:
   "approx n\<cdot>(convex_principal t) = convex_principal (approx_pd n t)"
 unfolding approx_convex_pd_def
-apply (rule convex_pd.basis_fun_principal)
-apply (erule convex_principal_mono [OF approx_pd_convex_mono])
-done
-
-lemma chain_approx_convex_pd:
-  "chain (approx :: nat \<Rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd)"
-unfolding approx_convex_pd_def
-by (rule convex_pd.chain_basis_fun_take)
-
-lemma lub_approx_convex_pd:
-  "(\<Squnion>i. approx i\<cdot>xs) = (xs::'a convex_pd)"
-unfolding approx_convex_pd_def
-by (rule convex_pd.lub_basis_fun_take)
-
-lemma approx_convex_pd_idem:
-  "approx n\<cdot>(approx n\<cdot>xs) = approx n\<cdot>(xs::'a convex_pd)"
-apply (induct xs rule: convex_pd.principal_induct, simp)
-apply (simp add: approx_pd_idem)
-done
+by (rule convex_pd.completion_approx_principal)
 
 lemma approx_eq_convex_principal:
   "\<exists>t\<in>Rep_convex_pd xs. approx n\<cdot>xs = convex_principal (approx_pd n t)"
 unfolding approx_convex_pd_def
-by (rule convex_pd.basis_fun_take_eq_principal)
-
-lemma finite_fixes_approx_convex_pd:
-  "finite {xs::'a convex_pd. approx n\<cdot>xs = xs}"
-unfolding approx_convex_pd_def
-by (rule convex_pd.finite_fixes_basis_fun_take)
-
-instance convex_pd :: (profinite) profinite
-apply intro_classes
-apply (simp add: chain_approx_convex_pd)
-apply (rule lub_approx_convex_pd)
-apply (rule approx_convex_pd_idem)
-apply (rule finite_fixes_approx_convex_pd)
-done
-
-instance convex_pd :: (bifinite) bifinite ..
+by (rule convex_pd.completion_approx_eq_principal)
 
 lemma compact_imp_convex_principal:
   "compact xs \<Longrightarrow> \<exists>t. xs = convex_principal t"
@@ -266,10 +242,7 @@
 
 lemma convex_principal_induct:
   "\<lbrakk>adm P; \<And>t. P (convex_principal t)\<rbrakk> \<Longrightarrow> P xs"
-apply (erule approx_induct, rename_tac xs)
-apply (cut_tac n=n and xs=xs in approx_eq_convex_principal)
-apply (clarify, simp)
-done
+by (rule convex_pd.principal_induct)
 
 lemma convex_principal_induct2:
   "\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
@@ -282,54 +255,12 @@
 done
 
 
-subsection {* Monadic unit *}
+subsection {* Monadic unit and plus *}
 
 definition
   convex_unit :: "'a \<rightarrow> 'a convex_pd" where
   "convex_unit = compact_basis.basis_fun (\<lambda>a. convex_principal (PDUnit a))"
 
-lemma convex_unit_Rep_compact_basis [simp]:
-  "convex_unit\<cdot>(Rep_compact_basis a) = convex_principal (PDUnit a)"
-unfolding convex_unit_def
-apply (rule compact_basis.basis_fun_principal)
-apply (rule convex_principal_mono)
-apply (erule PDUnit_convex_mono)
-done
-
-lemma convex_unit_strict [simp]: "convex_unit\<cdot>\<bottom> = \<bottom>"
-unfolding inst_convex_pd_pcpo Rep_compact_bot [symmetric] by simp
-
-lemma approx_convex_unit [simp]:
-  "approx n\<cdot>(convex_unit\<cdot>x) = convex_unit\<cdot>(approx n\<cdot>x)"
-apply (induct x rule: compact_basis_induct, simp)
-apply (simp add: approx_Rep_compact_basis)
-done
-
-lemma convex_unit_less_iff [simp]:
-  "(convex_unit\<cdot>x \<sqsubseteq> convex_unit\<cdot>y) = (x \<sqsubseteq> y)"
- apply (rule iffI)
-  apply (rule bifinite_less_ext)
-  apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
-  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
-  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
-  apply (clarify, simp add: compact_le_def)
- apply (erule monofun_cfun_arg)
-done
-
-lemma convex_unit_eq_iff [simp]:
-  "(convex_unit\<cdot>x = convex_unit\<cdot>y) = (x = y)"
-unfolding po_eq_conv by simp
-
-lemma convex_unit_strict_iff [simp]: "(convex_unit\<cdot>x = \<bottom>) = (x = \<bottom>)"
-unfolding convex_unit_strict [symmetric] by (rule convex_unit_eq_iff)
-
-lemma compact_convex_unit_iff [simp]:
-  "compact (convex_unit\<cdot>x) = compact x"
-unfolding bifinite_compact_iff by simp
-
-
-subsection {* Monadic plus *}
-
 definition
   convex_plus :: "'a convex_pd \<rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd" where
   "convex_plus = convex_pd.basis_fun (\<lambda>t. convex_pd.basis_fun (\<lambda>u.
@@ -340,40 +271,69 @@
     (infixl "+\<natural>" 65) where
   "xs +\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
 
+syntax
+  "_convex_pd" :: "args \<Rightarrow> 'a convex_pd" ("{_}\<natural>")
+
+translations
+  "{x,xs}\<natural>" == "{x}\<natural> +\<natural> {xs}\<natural>"
+  "{x}\<natural>" == "CONST convex_unit\<cdot>x"
+
+lemma convex_unit_Rep_compact_basis [simp]:
+  "{Rep_compact_basis a}\<natural> = convex_principal (PDUnit a)"
+unfolding convex_unit_def
+by (simp add: compact_basis.basis_fun_principal
+    convex_principal_mono PDUnit_convex_mono)
+
 lemma convex_plus_principal [simp]:
-  "convex_plus\<cdot>(convex_principal t)\<cdot>(convex_principal u) =
-   convex_principal (PDPlus t u)"
+  "convex_principal t +\<natural> convex_principal u = convex_principal (PDPlus t u)"
 unfolding convex_plus_def
 by (simp add: convex_pd.basis_fun_principal
     convex_pd.basis_fun_mono PDPlus_convex_mono)
 
+lemma approx_convex_unit [simp]:
+  "approx n\<cdot>{x}\<natural> = {approx n\<cdot>x}\<natural>"
+apply (induct x rule: compact_basis_induct, simp)
+apply (simp add: approx_Rep_compact_basis)
+done
+
 lemma approx_convex_plus [simp]:
-  "approx n\<cdot>(convex_plus\<cdot>xs\<cdot>ys) = convex_plus\<cdot>(approx n\<cdot>xs)\<cdot>(approx n\<cdot>ys)"
+  "approx n\<cdot>(xs +\<natural> ys) = approx n\<cdot>xs +\<natural> approx n\<cdot>ys"
 by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
 
-lemma convex_plus_commute: "convex_plus\<cdot>xs\<cdot>ys = convex_plus\<cdot>ys\<cdot>xs"
-apply (induct xs ys rule: convex_principal_induct2, simp, simp)
-apply (simp add: PDPlus_commute)
-done
-
 lemma convex_plus_assoc:
-  "convex_plus\<cdot>(convex_plus\<cdot>xs\<cdot>ys)\<cdot>zs = convex_plus\<cdot>xs\<cdot>(convex_plus\<cdot>ys\<cdot>zs)"
+  "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)"
 apply (induct xs ys arbitrary: zs rule: convex_principal_induct2, simp, simp)
 apply (rule_tac xs=zs in convex_principal_induct, simp)
 apply (simp add: PDPlus_assoc)
 done
 
-lemma convex_plus_absorb: "convex_plus\<cdot>xs\<cdot>xs = xs"
+lemma convex_plus_commute: "xs +\<natural> ys = ys +\<natural> xs"
+apply (induct xs ys rule: convex_principal_induct2, simp, simp)
+apply (simp add: PDPlus_commute)
+done
+
+lemma convex_plus_absorb: "xs +\<natural> xs = xs"
 apply (induct xs rule: convex_principal_induct, simp)
 apply (simp add: PDPlus_absorb)
 done
 
+interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\<natural>"]
+  by unfold_locales
+    (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+
+
+lemma convex_plus_left_commute: "xs +\<natural> (ys +\<natural> zs) = ys +\<natural> (xs +\<natural> zs)"
+by (rule aci_convex_plus.mult_left_commute)
+
+lemma convex_plus_left_absorb: "xs +\<natural> (xs +\<natural> ys) = xs +\<natural> ys"
+by (rule aci_convex_plus.mult_left_idem)
+
+lemmas convex_plus_aci = aci_convex_plus.mult_ac_idem
+
 lemma convex_unit_less_plus_iff [simp]:
-  "(convex_unit\<cdot>x \<sqsubseteq> convex_plus\<cdot>ys\<cdot>zs) =
-   (convex_unit\<cdot>x \<sqsubseteq> ys \<and> convex_unit\<cdot>x \<sqsubseteq> zs)"
+  "{x}\<natural> \<sqsubseteq> ys +\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs"
  apply (rule iffI)
   apply (subgoal_tac
-    "adm (\<lambda>f. f\<cdot>(convex_unit\<cdot>x) \<sqsubseteq> f\<cdot>ys \<and> f\<cdot>(convex_unit\<cdot>x) \<sqsubseteq> f\<cdot>zs)")
+    "adm (\<lambda>f. f\<cdot>{x}\<natural> \<sqsubseteq> f\<cdot>ys \<and> f\<cdot>{x}\<natural> \<sqsubseteq> f\<cdot>zs)")
    apply (drule admD, rule chain_approx)
     apply (drule_tac f="approx i" in monofun_cfun_arg)
     apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
@@ -383,16 +343,15 @@
    apply simp
   apply simp
  apply (erule conjE)
- apply (subst convex_plus_absorb [of "convex_unit\<cdot>x", symmetric])
+ apply (subst convex_plus_absorb [of "{x}\<natural>", symmetric])
  apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
 done
 
 lemma convex_plus_less_unit_iff [simp]:
-  "(convex_plus\<cdot>xs\<cdot>ys \<sqsubseteq> convex_unit\<cdot>z) =
-   (xs \<sqsubseteq> convex_unit\<cdot>z \<and> ys \<sqsubseteq> convex_unit\<cdot>z)"
+  "xs +\<natural> ys \<sqsubseteq> {z}\<natural> \<longleftrightarrow> xs \<sqsubseteq> {z}\<natural> \<and> ys \<sqsubseteq> {z}\<natural>"
  apply (rule iffI)
   apply (subgoal_tac
-    "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>(convex_unit\<cdot>z) \<and> f\<cdot>ys \<sqsubseteq> f\<cdot>(convex_unit\<cdot>z))")
+    "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>{z}\<natural> \<and> f\<cdot>ys \<sqsubseteq> f\<cdot>{z}\<natural>)")
    apply (drule admD, rule chain_approx)
     apply (drule_tac f="approx i" in monofun_cfun_arg)
     apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_convex_principal, simp)
@@ -402,18 +361,46 @@
    apply simp
   apply simp
  apply (erule conjE)
- apply (subst convex_plus_absorb [of "convex_unit\<cdot>z", symmetric])
+ apply (subst convex_plus_absorb [of "{z}\<natural>", symmetric])
  apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
 done
 
+lemma convex_unit_less_iff [simp]: "{x}\<natural> \<sqsubseteq> {y}\<natural> \<longleftrightarrow> x \<sqsubseteq> y"
+ apply (rule iffI)
+  apply (rule bifinite_less_ext)
+  apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
+  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
+  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
+  apply (clarify, simp add: compact_le_def)
+ apply (erule monofun_cfun_arg)
+done
+
+lemma convex_unit_eq_iff [simp]: "{x}\<natural> = {y}\<natural> \<longleftrightarrow> x = y"
+unfolding po_eq_conv by simp
+
+lemma convex_unit_strict [simp]: "{\<bottom>}\<natural> = \<bottom>"
+unfolding inst_convex_pd_pcpo Rep_compact_bot [symmetric] by simp
+
+lemma convex_unit_strict_iff [simp]: "{x}\<natural> = \<bottom> \<longleftrightarrow> x = \<bottom>"
+unfolding convex_unit_strict [symmetric] by (rule convex_unit_eq_iff)
+
+lemma compact_convex_unit_iff [simp]:
+  "compact {x}\<natural> \<longleftrightarrow> compact x"
+unfolding bifinite_compact_iff by simp
+
+lemma compact_convex_plus [simp]:
+  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<natural> ys)"
+apply (drule compact_imp_convex_principal)+
+apply (auto simp add: compact_convex_principal)
+done
+
 
 subsection {* Induction rules *}
 
 lemma convex_pd_induct1:
   assumes P: "adm P"
-  assumes unit: "\<And>x. P (convex_unit\<cdot>x)"
-  assumes insert:
-    "\<And>x ys. \<lbrakk>P (convex_unit\<cdot>x); P ys\<rbrakk> \<Longrightarrow> P (convex_plus\<cdot>(convex_unit\<cdot>x)\<cdot>ys)"
+  assumes unit: "\<And>x. P {x}\<natural>"
+  assumes insert: "\<And>x ys. \<lbrakk>P {x}\<natural>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<natural> +\<natural> ys)"
   shows "P (xs::'a convex_pd)"
 apply (induct xs rule: convex_principal_induct, rule P)
 apply (induct_tac t rule: pd_basis_induct1)
@@ -426,8 +413,8 @@
 
 lemma convex_pd_induct:
   assumes P: "adm P"
-  assumes unit: "\<And>x. P (convex_unit\<cdot>x)"
-  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (convex_plus\<cdot>xs\<cdot>ys)"
+  assumes unit: "\<And>x. P {x}\<natural>"
+  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<natural> ys)"
   shows "P (xs::'a convex_pd)"
 apply (induct xs rule: convex_principal_induct, rule P)
 apply (induct_tac t rule: pd_basis_induct)
@@ -443,9 +430,10 @@
   "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where
   "convex_bind_basis = fold_pd
     (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
-    (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
+    (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
 
-lemma ACI_convex_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. convex_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
+lemma ACI_convex_bind:
+  "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
 apply unfold_locales
 apply (simp add: convex_plus_assoc)
 apply (simp add: convex_plus_commute)
@@ -456,11 +444,11 @@
   "convex_bind_basis (PDUnit a) =
     (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   "convex_bind_basis (PDPlus t u) =
-    (\<Lambda> f. convex_plus\<cdot>(convex_bind_basis t\<cdot>f)\<cdot>(convex_bind_basis u\<cdot>f))"
+    (\<Lambda> f. convex_bind_basis t\<cdot>f +\<natural> convex_bind_basis u\<cdot>f)"
 unfolding convex_bind_basis_def
 apply -
-apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_convex_bind])
-apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_convex_bind])
+apply (rule fold_pd_PDUnit [OF ACI_convex_bind])
+apply (rule fold_pd_PDPlus [OF ACI_convex_bind])
 done
 
 lemma monofun_LAM:
@@ -487,12 +475,11 @@
 done
 
 lemma convex_bind_unit [simp]:
-  "convex_bind\<cdot>(convex_unit\<cdot>x)\<cdot>f = f\<cdot>x"
+  "convex_bind\<cdot>{x}\<natural>\<cdot>f = f\<cdot>x"
 by (induct x rule: compact_basis_induct, simp, simp)
 
 lemma convex_bind_plus [simp]:
-  "convex_bind\<cdot>(convex_plus\<cdot>xs\<cdot>ys)\<cdot>f =
-   convex_plus\<cdot>(convex_bind\<cdot>xs\<cdot>f)\<cdot>(convex_bind\<cdot>ys\<cdot>f)"
+  "convex_bind\<cdot>(xs +\<natural> ys)\<cdot>f = convex_bind\<cdot>xs\<cdot>f +\<natural> convex_bind\<cdot>ys\<cdot>f"
 by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
 
 lemma convex_bind_strict [simp]: "convex_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
@@ -503,7 +490,7 @@
 
 definition
   convex_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a convex_pd \<rightarrow> 'b convex_pd" where
-  "convex_map = (\<Lambda> f xs. convex_bind\<cdot>xs\<cdot>(\<Lambda> x. convex_unit\<cdot>(f\<cdot>x)))"
+  "convex_map = (\<Lambda> f xs. convex_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<natural>))"
 
 definition
   convex_join :: "'a convex_pd convex_pd \<rightarrow> 'a convex_pd" where
@@ -514,17 +501,15 @@
 unfolding convex_map_def by simp
 
 lemma convex_map_plus [simp]:
-  "convex_map\<cdot>f\<cdot>(convex_plus\<cdot>xs\<cdot>ys) =
-   convex_plus\<cdot>(convex_map\<cdot>f\<cdot>xs)\<cdot>(convex_map\<cdot>f\<cdot>ys)"
+  "convex_map\<cdot>f\<cdot>(xs +\<natural> ys) = convex_map\<cdot>f\<cdot>xs +\<natural> convex_map\<cdot>f\<cdot>ys"
 unfolding convex_map_def by simp
 
 lemma convex_join_unit [simp]:
-  "convex_join\<cdot>(convex_unit\<cdot>xs) = xs"
+  "convex_join\<cdot>{xs}\<natural> = xs"
 unfolding convex_join_def by simp
 
 lemma convex_join_plus [simp]:
-  "convex_join\<cdot>(convex_plus\<cdot>xss\<cdot>yss) =
-   convex_plus\<cdot>(convex_join\<cdot>xss)\<cdot>(convex_join\<cdot>yss)"
+  "convex_join\<cdot>(xss +\<natural> yss) = convex_join\<cdot>xss +\<natural> convex_join\<cdot>yss"
 unfolding convex_join_def by simp
 
 lemma convex_map_ident: "convex_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
@@ -571,12 +556,11 @@
 done
 
 lemma convex_to_upper_unit [simp]:
-  "convex_to_upper\<cdot>(convex_unit\<cdot>x) = upper_unit\<cdot>x"
+  "convex_to_upper\<cdot>{x}\<natural> = {x}\<sharp>"
 by (induct x rule: compact_basis_induct, simp, simp)
 
 lemma convex_to_upper_plus [simp]:
-  "convex_to_upper\<cdot>(convex_plus\<cdot>xs\<cdot>ys) =
-   upper_plus\<cdot>(convex_to_upper\<cdot>xs)\<cdot>(convex_to_upper\<cdot>ys)"
+  "convex_to_upper\<cdot>(xs +\<natural> ys) = convex_to_upper\<cdot>xs +\<sharp> convex_to_upper\<cdot>ys"
 by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
 
 lemma approx_convex_to_upper:
@@ -601,12 +585,11 @@
 done
 
 lemma convex_to_lower_unit [simp]:
-  "convex_to_lower\<cdot>(convex_unit\<cdot>x) = lower_unit\<cdot>x"
+  "convex_to_lower\<cdot>{x}\<natural> = {x}\<flat>"
 by (induct x rule: compact_basis_induct, simp, simp)
 
 lemma convex_to_lower_plus [simp]:
-  "convex_to_lower\<cdot>(convex_plus\<cdot>xs\<cdot>ys) =
-   lower_plus\<cdot>(convex_to_lower\<cdot>xs)\<cdot>(convex_to_lower\<cdot>ys)"
+  "convex_to_lower\<cdot>(xs +\<natural> ys) = convex_to_lower\<cdot>xs +\<flat> convex_to_lower\<cdot>ys"
 by (induct xs ys rule: convex_principal_induct2, simp, simp, simp)
 
 lemma approx_convex_to_lower:
@@ -629,4 +612,19 @@
  apply (simp add: approx_convex_to_upper approx_convex_to_lower convex_le_def)
 done
 
+lemmas convex_plus_less_plus_iff =
+  convex_pd_less_iff [where xs="xs +\<natural> ys" and ys="zs +\<natural> ws", standard]
+
+lemmas convex_pd_less_simps =
+  convex_unit_less_plus_iff
+  convex_plus_less_unit_iff
+  convex_plus_less_plus_iff
+  convex_unit_less_iff
+  convex_to_upper_unit
+  convex_to_upper_plus
+  convex_to_lower_unit
+  convex_to_lower_plus
+  upper_pd_less_simps
+  lower_pd_less_simps
+
 end
diff -r 19d8783a30de -r 8684b5240f11 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Fri May 16 22:35:25 2008 +0200
+++ b/src/HOLCF/LowerPD.thy	Fri May 16 23:25:37 2008 +0200
@@ -103,13 +103,7 @@
 done
 
 lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd x)"
-by (rule Rep_lower_pd [simplified])
-
-lemma Rep_lower_pd_mono: "x \<sqsubseteq> y \<Longrightarrow> Rep_lower_pd x \<subseteq> Rep_lower_pd y"
-unfolding less_lower_pd_def less_set_eq .
-
-
-subsection {* Principal ideals *}
+by (rule Rep_lower_pd [unfolded mem_Collect_eq])
 
 definition
   lower_principal :: "'a pd_basis \<Rightarrow> 'a lower_pd" where
@@ -123,7 +117,7 @@
 done
 
 interpretation lower_pd:
-  bifinite_basis [lower_le approx_pd lower_principal Rep_lower_pd]
+  ideal_completion [lower_le approx_pd lower_principal Rep_lower_pd]
 apply unfold_locales
 apply (rule approx_pd_lower_le)
 apply (rule approx_pd_idem)
@@ -138,32 +132,25 @@
 done
 
 lemma lower_principal_less_iff [simp]:
-  "(lower_principal t \<sqsubseteq> lower_principal u) = (t \<le>\<flat> u)"
-unfolding less_lower_pd_def Rep_lower_principal less_set_eq
-by (fast intro: lower_le_refl elim: lower_le_trans)
+  "lower_principal t \<sqsubseteq> lower_principal u \<longleftrightarrow> t \<le>\<flat> u"
+by (rule lower_pd.principal_less_iff)
+
+lemma lower_principal_eq_iff:
+  "lower_principal t = lower_principal u \<longleftrightarrow> t \<le>\<flat> u \<and> u \<le>\<flat> t"
+by (rule lower_pd.principal_eq_iff)
 
 lemma lower_principal_mono:
   "t \<le>\<flat> u \<Longrightarrow> lower_principal t \<sqsubseteq> lower_principal u"
-by (rule lower_principal_less_iff [THEN iffD2])
+by (rule lower_pd.principal_mono)
 
 lemma compact_lower_principal: "compact (lower_principal t)"
-apply (rule compactI2)
-apply (simp add: less_lower_pd_def)
-apply (simp add: cont2contlubE [OF cont_Rep_lower_pd])
-apply (simp add: Rep_lower_principal set_cpo_simps)
-apply (simp add: subset_eq)
-apply (drule spec, drule mp, rule lower_le_refl)
-apply (erule exE, rename_tac i)
-apply (rule_tac x=i in exI)
-apply clarify
-apply (erule (1) lower_le.idealD3 [OF ideal_Rep_lower_pd])
-done
+by (rule lower_pd.compact_principal)
 
 lemma lower_pd_minimal: "lower_principal (PDUnit compact_bot) \<sqsubseteq> ys"
 by (induct ys rule: lower_pd.principal_induct, simp, simp)
 
 instance lower_pd :: (bifinite) pcpo
-by (intro_classes, fast intro: lower_pd_minimal)
+by intro_classes (fast intro: lower_pd_minimal)
 
 lemma inst_lower_pd_pcpo: "\<bottom> = lower_principal (PDUnit compact_bot)"
 by (rule lower_pd_minimal [THEN UU_I, symmetric])
@@ -174,51 +161,27 @@
 instance lower_pd :: (profinite) approx ..
 
 defs (overloaded)
-  approx_lower_pd_def:
-    "approx \<equiv> (\<lambda>n. lower_pd.basis_fun (\<lambda>t. lower_principal (approx_pd n t)))"
+  approx_lower_pd_def: "approx \<equiv> lower_pd.completion_approx"
+
+instance lower_pd :: (profinite) profinite
+apply (intro_classes, unfold approx_lower_pd_def)
+apply (simp add: lower_pd.chain_completion_approx)
+apply (rule lower_pd.lub_completion_approx)
+apply (rule lower_pd.completion_approx_idem)
+apply (rule lower_pd.finite_fixes_completion_approx)
+done
+
+instance lower_pd :: (bifinite) bifinite ..
 
 lemma approx_lower_principal [simp]:
   "approx n\<cdot>(lower_principal t) = lower_principal (approx_pd n t)"
 unfolding approx_lower_pd_def
-apply (rule lower_pd.basis_fun_principal)
-apply (erule lower_principal_mono [OF approx_pd_lower_mono])
-done
-
-lemma chain_approx_lower_pd:
-  "chain (approx :: nat \<Rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd)"
-unfolding approx_lower_pd_def
-by (rule lower_pd.chain_basis_fun_take)
-
-lemma lub_approx_lower_pd:
-  "(\<Squnion>i. approx i\<cdot>xs) = (xs::'a lower_pd)"
-unfolding approx_lower_pd_def
-by (rule lower_pd.lub_basis_fun_take)
-
-lemma approx_lower_pd_idem:
-  "approx n\<cdot>(approx n\<cdot>xs) = approx n\<cdot>(xs::'a lower_pd)"
-apply (induct xs rule: lower_pd.principal_induct, simp)
-apply (simp add: approx_pd_idem)
-done
+by (rule lower_pd.completion_approx_principal)
 
 lemma approx_eq_lower_principal:
   "\<exists>t\<in>Rep_lower_pd xs. approx n\<cdot>xs = lower_principal (approx_pd n t)"
 unfolding approx_lower_pd_def
-by (rule lower_pd.basis_fun_take_eq_principal)
-
-lemma finite_fixes_approx_lower_pd:
-  "finite {xs::'a lower_pd. approx n\<cdot>xs = xs}"
-unfolding approx_lower_pd_def
-by (rule lower_pd.finite_fixes_basis_fun_take)
-
-instance lower_pd :: (profinite) profinite
-apply intro_classes
-apply (simp add: chain_approx_lower_pd)
-apply (rule lub_approx_lower_pd)
-apply (rule approx_lower_pd_idem)
-apply (rule finite_fixes_approx_lower_pd)
-done
-
-instance lower_pd :: (bifinite) bifinite ..
+by (rule lower_pd.completion_approx_eq_principal)
 
 lemma compact_imp_lower_principal:
   "compact xs \<Longrightarrow> \<exists>t. xs = lower_principal t"
@@ -231,10 +194,7 @@
 
 lemma lower_principal_induct:
   "\<lbrakk>adm P; \<And>t. P (lower_principal t)\<rbrakk> \<Longrightarrow> P xs"
-apply (erule approx_induct, rename_tac xs)
-apply (cut_tac n=n and xs=xs in approx_eq_lower_principal)
-apply (clarify, simp)
-done
+by (rule lower_pd.principal_induct)
 
 lemma lower_principal_induct2:
   "\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
@@ -247,54 +207,12 @@
 done
 
 
-subsection {* Monadic unit *}
+subsection {* Monadic unit and plus *}
 
 definition
   lower_unit :: "'a \<rightarrow> 'a lower_pd" where
   "lower_unit = compact_basis.basis_fun (\<lambda>a. lower_principal (PDUnit a))"
 
-lemma lower_unit_Rep_compact_basis [simp]:
-  "lower_unit\<cdot>(Rep_compact_basis a) = lower_principal (PDUnit a)"
-unfolding lower_unit_def
-apply (rule compact_basis.basis_fun_principal)
-apply (rule lower_principal_mono)
-apply (erule PDUnit_lower_mono)
-done
-
-lemma lower_unit_strict [simp]: "lower_unit\<cdot>\<bottom> = \<bottom>"
-unfolding inst_lower_pd_pcpo Rep_compact_bot [symmetric] by simp
-
-lemma approx_lower_unit [simp]:
-  "approx n\<cdot>(lower_unit\<cdot>x) = lower_unit\<cdot>(approx n\<cdot>x)"
-apply (induct x rule: compact_basis_induct, simp)
-apply (simp add: approx_Rep_compact_basis)
-done
-
-lemma lower_unit_less_iff [simp]:
-  "(lower_unit\<cdot>x \<sqsubseteq> lower_unit\<cdot>y) = (x \<sqsubseteq> y)"
- apply (rule iffI)
-  apply (rule bifinite_less_ext)
-  apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
-  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
-  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
-  apply (clarify, simp add: compact_le_def)
- apply (erule monofun_cfun_arg)
-done
-
-lemma lower_unit_eq_iff [simp]:
-  "(lower_unit\<cdot>x = lower_unit\<cdot>y) = (x = y)"
-unfolding po_eq_conv by simp
-
-lemma lower_unit_strict_iff [simp]: "(lower_unit\<cdot>x = \<bottom>) = (x = \<bottom>)"
-unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff)
-
-lemma compact_lower_unit_iff [simp]:
-  "compact (lower_unit\<cdot>x) = compact x"
-unfolding bifinite_compact_iff by simp
-
-
-subsection {* Monadic plus *}
-
 definition
   lower_plus :: "'a lower_pd \<rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd" where
   "lower_plus = lower_pd.basis_fun (\<lambda>t. lower_pd.basis_fun (\<lambda>u.
@@ -305,79 +223,89 @@
     (infixl "+\<flat>" 65) where
   "xs +\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
 
+syntax
+  "_lower_pd" :: "args \<Rightarrow> 'a lower_pd" ("{_}\<flat>")
+
+translations
+  "{x,xs}\<flat>" == "{x}\<flat> +\<flat> {xs}\<flat>"
+  "{x}\<flat>" == "CONST lower_unit\<cdot>x"
+
+lemma lower_unit_Rep_compact_basis [simp]:
+  "{Rep_compact_basis a}\<flat> = lower_principal (PDUnit a)"
+unfolding lower_unit_def
+by (simp add: compact_basis.basis_fun_principal
+    lower_principal_mono PDUnit_lower_mono)
+
 lemma lower_plus_principal [simp]:
-  "lower_plus\<cdot>(lower_principal t)\<cdot>(lower_principal u) =
-   lower_principal (PDPlus t u)"
+  "lower_principal t +\<flat> lower_principal u = lower_principal (PDPlus t u)"
 unfolding lower_plus_def
 by (simp add: lower_pd.basis_fun_principal
     lower_pd.basis_fun_mono PDPlus_lower_mono)
 
+lemma approx_lower_unit [simp]:
+  "approx n\<cdot>{x}\<flat> = {approx n\<cdot>x}\<flat>"
+apply (induct x rule: compact_basis_induct, simp)
+apply (simp add: approx_Rep_compact_basis)
+done
+
 lemma approx_lower_plus [simp]:
-  "approx n\<cdot>(lower_plus\<cdot>xs\<cdot>ys) = lower_plus\<cdot>(approx n\<cdot>xs)\<cdot>(approx n\<cdot>ys)"
+  "approx n\<cdot>(xs +\<flat> ys) = (approx n\<cdot>xs) +\<flat> (approx n\<cdot>ys)"
 by (induct xs ys rule: lower_principal_induct2, simp, simp, simp)
 
-lemma lower_plus_commute: "lower_plus\<cdot>xs\<cdot>ys = lower_plus\<cdot>ys\<cdot>xs"
-apply (induct xs ys rule: lower_principal_induct2, simp, simp)
-apply (simp add: PDPlus_commute)
-done
-
-lemma lower_plus_assoc:
-  "lower_plus\<cdot>(lower_plus\<cdot>xs\<cdot>ys)\<cdot>zs = lower_plus\<cdot>xs\<cdot>(lower_plus\<cdot>ys\<cdot>zs)"
+lemma lower_plus_assoc: "(xs +\<flat> ys) +\<flat> zs = xs +\<flat> (ys +\<flat> zs)"
 apply (induct xs ys arbitrary: zs rule: lower_principal_induct2, simp, simp)
 apply (rule_tac xs=zs in lower_principal_induct, simp)
 apply (simp add: PDPlus_assoc)
 done
 
-lemma lower_plus_absorb: "lower_plus\<cdot>xs\<cdot>xs = xs"
+lemma lower_plus_commute: "xs +\<flat> ys = ys +\<flat> xs"
+apply (induct xs ys rule: lower_principal_induct2, simp, simp)
+apply (simp add: PDPlus_commute)
+done
+
+lemma lower_plus_absorb: "xs +\<flat> xs = xs"
 apply (induct xs rule: lower_principal_induct, simp)
 apply (simp add: PDPlus_absorb)
 done
 
-lemma lower_plus_less1: "xs \<sqsubseteq> lower_plus\<cdot>xs\<cdot>ys"
+interpretation aci_lower_plus: ab_semigroup_idem_mult ["op +\<flat>"]
+  by unfold_locales
+    (rule lower_plus_assoc lower_plus_commute lower_plus_absorb)+
+
+lemma lower_plus_left_commute: "xs +\<flat> (ys +\<flat> zs) = ys +\<flat> (xs +\<flat> zs)"
+by (rule aci_lower_plus.mult_left_commute)
+
+lemma lower_plus_left_absorb: "xs +\<flat> (xs +\<flat> ys) = xs +\<flat> ys"
+by (rule aci_lower_plus.mult_left_idem)
+
+lemmas lower_plus_aci = aci_lower_plus.mult_ac_idem
+
+lemma lower_plus_less1: "xs \<sqsubseteq> xs +\<flat> ys"
 apply (induct xs ys rule: lower_principal_induct2, simp, simp)
 apply (simp add: PDPlus_lower_less)
 done
 
-lemma lower_plus_less2: "ys \<sqsubseteq> lower_plus\<cdot>xs\<cdot>ys"
+lemma lower_plus_less2: "ys \<sqsubseteq> xs +\<flat> ys"
 by (subst lower_plus_commute, rule lower_plus_less1)
 
-lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> lower_plus\<cdot>xs\<cdot>ys \<sqsubseteq> zs"
+lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs +\<flat> ys \<sqsubseteq> zs"
 apply (subst lower_plus_absorb [of zs, symmetric])
 apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
 done
 
 lemma lower_plus_less_iff:
-  "(lower_plus\<cdot>xs\<cdot>ys \<sqsubseteq> zs) = (xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs)"
+  "xs +\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs"
 apply safe
 apply (erule trans_less [OF lower_plus_less1])
 apply (erule trans_less [OF lower_plus_less2])
 apply (erule (1) lower_plus_least)
 done
 
-lemma lower_plus_strict_iff [simp]:
-  "(lower_plus\<cdot>xs\<cdot>ys = \<bottom>) = (xs = \<bottom> \<and> ys = \<bottom>)"
-apply safe
-apply (rule UU_I, erule subst, rule lower_plus_less1)
-apply (rule UU_I, erule subst, rule lower_plus_less2)
-apply (rule lower_plus_absorb)
-done
-
-lemma lower_plus_strict1 [simp]: "lower_plus\<cdot>\<bottom>\<cdot>ys = ys"
-apply (rule antisym_less [OF _ lower_plus_less2])
-apply (simp add: lower_plus_least)
-done
-
-lemma lower_plus_strict2 [simp]: "lower_plus\<cdot>xs\<cdot>\<bottom> = xs"
-apply (rule antisym_less [OF _ lower_plus_less1])
-apply (simp add: lower_plus_least)
-done
-
 lemma lower_unit_less_plus_iff:
-  "(lower_unit\<cdot>x \<sqsubseteq> lower_plus\<cdot>ys\<cdot>zs) =
-    (lower_unit\<cdot>x \<sqsubseteq> ys \<or> lower_unit\<cdot>x \<sqsubseteq> zs)"
+  "{x}\<flat> \<sqsubseteq> ys +\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
  apply (rule iffI)
   apply (subgoal_tac
-    "adm (\<lambda>f. f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>ys \<or> f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>zs)")
+    "adm (\<lambda>f. f\<cdot>{x}\<flat> \<sqsubseteq> f\<cdot>ys \<or> f\<cdot>{x}\<flat> \<sqsubseteq> f\<cdot>zs)")
    apply (drule admD, rule chain_approx)
     apply (drule_tac f="approx i" in monofun_cfun_arg)
     apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
@@ -391,19 +319,65 @@
  apply (erule trans_less [OF _ lower_plus_less2])
 done
 
+lemma lower_unit_less_iff [simp]: "{x}\<flat> \<sqsubseteq> {y}\<flat> \<longleftrightarrow> x \<sqsubseteq> y"
+ apply (rule iffI)
+  apply (rule bifinite_less_ext)
+  apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
+  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
+  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
+  apply (clarify, simp add: compact_le_def)
+ apply (erule monofun_cfun_arg)
+done
+
 lemmas lower_pd_less_simps =
   lower_unit_less_iff
   lower_plus_less_iff
   lower_unit_less_plus_iff
 
+lemma lower_unit_eq_iff [simp]: "{x}\<flat> = {y}\<flat> \<longleftrightarrow> x = y"
+unfolding po_eq_conv by simp
+
+lemma lower_unit_strict [simp]: "{\<bottom>}\<flat> = \<bottom>"
+unfolding inst_lower_pd_pcpo Rep_compact_bot [symmetric] by simp
+
+lemma lower_unit_strict_iff [simp]: "{x}\<flat> = \<bottom> \<longleftrightarrow> x = \<bottom>"
+unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff)
+
+lemma lower_plus_strict_iff [simp]:
+  "xs +\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
+apply safe
+apply (rule UU_I, erule subst, rule lower_plus_less1)
+apply (rule UU_I, erule subst, rule lower_plus_less2)
+apply (rule lower_plus_absorb)
+done
+
+lemma lower_plus_strict1 [simp]: "\<bottom> +\<flat> ys = ys"
+apply (rule antisym_less [OF _ lower_plus_less2])
+apply (simp add: lower_plus_least)
+done
+
+lemma lower_plus_strict2 [simp]: "xs +\<flat> \<bottom> = xs"
+apply (rule antisym_less [OF _ lower_plus_less1])
+apply (simp add: lower_plus_least)
+done
+
+lemma compact_lower_unit_iff [simp]: "compact {x}\<flat> \<longleftrightarrow> compact x"
+unfolding bifinite_compact_iff by simp
+
+lemma compact_lower_plus [simp]:
+  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<flat> ys)"
+apply (drule compact_imp_lower_principal)+
+apply (auto simp add: compact_lower_principal)
+done
+
 
 subsection {* Induction rules *}
 
 lemma lower_pd_induct1:
   assumes P: "adm P"
-  assumes unit: "\<And>x. P (lower_unit\<cdot>x)"
+  assumes unit: "\<And>x. P {x}\<flat>"
   assumes insert:
-    "\<And>x ys. \<lbrakk>P (lower_unit\<cdot>x); P ys\<rbrakk> \<Longrightarrow> P (lower_plus\<cdot>(lower_unit\<cdot>x)\<cdot>ys)"
+    "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> +\<flat> ys)"
   shows "P (xs::'a lower_pd)"
 apply (induct xs rule: lower_principal_induct, rule P)
 apply (induct_tac t rule: pd_basis_induct1)
@@ -416,8 +390,8 @@
 
 lemma lower_pd_induct:
   assumes P: "adm P"
-  assumes unit: "\<And>x. P (lower_unit\<cdot>x)"
-  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (lower_plus\<cdot>xs\<cdot>ys)"
+  assumes unit: "\<And>x. P {x}\<flat>"
+  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<flat> ys)"
   shows "P (xs::'a lower_pd)"
 apply (induct xs rule: lower_principal_induct, rule P)
 apply (induct_tac t rule: pd_basis_induct)
@@ -433,9 +407,10 @@
   "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b lower_pd" where
   "lower_bind_basis = fold_pd
     (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
-    (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
+    (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
 
-lemma ACI_lower_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. lower_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
+lemma ACI_lower_bind:
+  "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
 apply unfold_locales
 apply (simp add: lower_plus_assoc)
 apply (simp add: lower_plus_commute)
@@ -446,11 +421,11 @@
   "lower_bind_basis (PDUnit a) =
     (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   "lower_bind_basis (PDPlus t u) =
-    (\<Lambda> f. lower_plus\<cdot>(lower_bind_basis t\<cdot>f)\<cdot>(lower_bind_basis u\<cdot>f))"
+    (\<Lambda> f. lower_bind_basis t\<cdot>f +\<flat> lower_bind_basis u\<cdot>f)"
 unfolding lower_bind_basis_def
 apply -
-apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_lower_bind])
-apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_lower_bind])
+apply (rule fold_pd_PDUnit [OF ACI_lower_bind])
+apply (rule fold_pd_PDPlus [OF ACI_lower_bind])
 done
 
 lemma lower_bind_basis_mono:
@@ -474,12 +449,11 @@
 done
 
 lemma lower_bind_unit [simp]:
-  "lower_bind\<cdot>(lower_unit\<cdot>x)\<cdot>f = f\<cdot>x"
+  "lower_bind\<cdot>{x}\<flat>\<cdot>f = f\<cdot>x"
 by (induct x rule: compact_basis_induct, simp, simp)
 
 lemma lower_bind_plus [simp]:
-  "lower_bind\<cdot>(lower_plus\<cdot>xs\<cdot>ys)\<cdot>f =
-   lower_plus\<cdot>(lower_bind\<cdot>xs\<cdot>f)\<cdot>(lower_bind\<cdot>ys\<cdot>f)"
+  "lower_bind\<cdot>(xs +\<flat> ys)\<cdot>f = lower_bind\<cdot>xs\<cdot>f +\<flat> lower_bind\<cdot>ys\<cdot>f"
 by (induct xs ys rule: lower_principal_induct2, simp, simp, simp)
 
 lemma lower_bind_strict [simp]: "lower_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
@@ -490,28 +464,26 @@
 
 definition
   lower_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a lower_pd \<rightarrow> 'b lower_pd" where
-  "lower_map = (\<Lambda> f xs. lower_bind\<cdot>xs\<cdot>(\<Lambda> x. lower_unit\<cdot>(f\<cdot>x)))"
+  "lower_map = (\<Lambda> f xs. lower_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<flat>))"
 
 definition
   lower_join :: "'a lower_pd lower_pd \<rightarrow> 'a lower_pd" where
   "lower_join = (\<Lambda> xss. lower_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"
 
 lemma lower_map_unit [simp]:
-  "lower_map\<cdot>f\<cdot>(lower_unit\<cdot>x) = lower_unit\<cdot>(f\<cdot>x)"
+  "lower_map\<cdot>f\<cdot>{x}\<flat> = {f\<cdot>x}\<flat>"
 unfolding lower_map_def by simp
 
 lemma lower_map_plus [simp]:
-  "lower_map\<cdot>f\<cdot>(lower_plus\<cdot>xs\<cdot>ys) =
-   lower_plus\<cdot>(lower_map\<cdot>f\<cdot>xs)\<cdot>(lower_map\<cdot>f\<cdot>ys)"
+  "lower_map\<cdot>f\<cdot>(xs +\<flat> ys) = lower_map\<cdot>f\<cdot>xs +\<flat> lower_map\<cdot>f\<cdot>ys"
 unfolding lower_map_def by simp
 
 lemma lower_join_unit [simp]:
-  "lower_join\<cdot>(lower_unit\<cdot>xs) = xs"
+  "lower_join\<cdot>{xs}\<flat> = xs"
 unfolding lower_join_def by simp
 
 lemma lower_join_plus [simp]:
-  "lower_join\<cdot>(lower_plus\<cdot>xss\<cdot>yss) =
-   lower_plus\<cdot>(lower_join\<cdot>xss)\<cdot>(lower_join\<cdot>yss)"
+  "lower_join\<cdot>(xss +\<flat> yss) = lower_join\<cdot>xss +\<flat> lower_join\<cdot>yss"
 unfolding lower_join_def by simp
 
 lemma lower_map_ident: "lower_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"
diff -r 19d8783a30de -r 8684b5240f11 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Fri May 16 22:35:25 2008 +0200
+++ b/src/HOLCF/UpperPD.thy	Fri May 16 23:25:37 2008 +0200
@@ -101,7 +101,7 @@
 done
 
 lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd x)"
-by (rule Rep_upper_pd [simplified])
+by (rule Rep_upper_pd [unfolded mem_Collect_eq])
 
 definition
   upper_principal :: "'a pd_basis \<Rightarrow> 'a upper_pd" where
@@ -110,12 +110,12 @@
 lemma Rep_upper_principal:
   "Rep_upper_pd (upper_principal t) = {u. u \<le>\<sharp> t}"
 unfolding upper_principal_def
-apply (rule Abs_upper_pd_inverse [simplified])
+apply (rule Abs_upper_pd_inverse [unfolded mem_Collect_eq])
 apply (rule upper_le.ideal_principal)
 done
 
 interpretation upper_pd:
-  bifinite_basis [upper_le approx_pd upper_principal Rep_upper_pd]
+  ideal_completion [upper_le approx_pd upper_principal Rep_upper_pd]
 apply unfold_locales
 apply (rule approx_pd_upper_le)
 apply (rule approx_pd_idem)
@@ -130,9 +130,12 @@
 done
 
 lemma upper_principal_less_iff [simp]:
-  "(upper_principal t \<sqsubseteq> upper_principal u) = (t \<le>\<sharp> u)"
-unfolding less_upper_pd_def Rep_upper_principal less_set_eq
-by (fast intro: upper_le_refl elim: upper_le_trans)
+  "upper_principal t \<sqsubseteq> upper_principal u \<longleftrightarrow> t \<le>\<sharp> u"
+by (rule upper_pd.principal_less_iff)
+
+lemma upper_principal_eq_iff:
+  "upper_principal t = upper_principal u \<longleftrightarrow> t \<le>\<sharp> u \<and> u \<le>\<sharp> t"
+by (rule upper_pd.principal_eq_iff)
 
 lemma upper_principal_mono:
   "t \<le>\<sharp> u \<Longrightarrow> upper_principal t \<sqsubseteq> upper_principal u"
@@ -145,7 +148,7 @@
 by (induct ys rule: upper_pd.principal_induct, simp, simp)
 
 instance upper_pd :: (bifinite) pcpo
-by (intro_classes, fast intro: upper_pd_minimal)
+by intro_classes (fast intro: upper_pd_minimal)
 
 lemma inst_upper_pd_pcpo: "\<bottom> = upper_principal (PDUnit compact_bot)"
 by (rule upper_pd_minimal [THEN UU_I, symmetric])
@@ -156,51 +159,27 @@
 instance upper_pd :: (profinite) approx ..
 
 defs (overloaded)
-  approx_upper_pd_def:
-    "approx \<equiv> (\<lambda>n. upper_pd.basis_fun (\<lambda>t. upper_principal (approx_pd n t)))"
+  approx_upper_pd_def: "approx \<equiv> upper_pd.completion_approx"
+
+instance upper_pd :: (profinite) profinite
+apply (intro_classes, unfold approx_upper_pd_def)
+apply (simp add: upper_pd.chain_completion_approx)
+apply (rule upper_pd.lub_completion_approx)
+apply (rule upper_pd.completion_approx_idem)
+apply (rule upper_pd.finite_fixes_completion_approx)
+done
+
+instance upper_pd :: (bifinite) bifinite ..
 
 lemma approx_upper_principal [simp]:
   "approx n\<cdot>(upper_principal t) = upper_principal (approx_pd n t)"
 unfolding approx_upper_pd_def
-apply (rule upper_pd.basis_fun_principal)
-apply (erule upper_principal_mono [OF approx_pd_upper_mono])
-done
-
-lemma chain_approx_upper_pd:
-  "chain (approx :: nat \<Rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd)"
-unfolding approx_upper_pd_def
-by (rule upper_pd.chain_basis_fun_take)
-
-lemma lub_approx_upper_pd:
-  "(\<Squnion>i. approx i\<cdot>xs) = (xs::'a upper_pd)"
-unfolding approx_upper_pd_def
-by (rule upper_pd.lub_basis_fun_take)
-
-lemma approx_upper_pd_idem:
-  "approx n\<cdot>(approx n\<cdot>xs) = approx n\<cdot>(xs::'a upper_pd)"
-apply (induct xs rule: upper_pd.principal_induct, simp)
-apply (simp add: approx_pd_idem)
-done
+by (rule upper_pd.completion_approx_principal)
 
 lemma approx_eq_upper_principal:
   "\<exists>t\<in>Rep_upper_pd xs. approx n\<cdot>xs = upper_principal (approx_pd n t)"
 unfolding approx_upper_pd_def
-by (rule upper_pd.basis_fun_take_eq_principal)
-
-lemma finite_fixes_approx_upper_pd:
-  "finite {xs::'a upper_pd. approx n\<cdot>xs = xs}"
-unfolding approx_upper_pd_def
-by (rule upper_pd.finite_fixes_basis_fun_take)
-
-instance upper_pd :: (profinite) profinite
-apply intro_classes
-apply (simp add: chain_approx_upper_pd)
-apply (rule lub_approx_upper_pd)
-apply (rule approx_upper_pd_idem)
-apply (rule finite_fixes_approx_upper_pd)
-done
-
-instance upper_pd :: (bifinite) bifinite ..
+by (rule upper_pd.completion_approx_eq_principal)
 
 lemma compact_imp_upper_principal:
   "compact xs \<Longrightarrow> \<exists>t. xs = upper_principal t"
@@ -213,10 +192,7 @@
 
 lemma upper_principal_induct:
   "\<lbrakk>adm P; \<And>t. P (upper_principal t)\<rbrakk> \<Longrightarrow> P xs"
-apply (erule approx_induct, rename_tac xs)
-apply (cut_tac n=n and xs=xs in approx_eq_upper_principal)
-apply (clarify, simp)
-done
+by (rule upper_pd.principal_induct)
 
 lemma upper_principal_induct2:
   "\<lbrakk>\<And>ys. adm (\<lambda>xs. P xs ys); \<And>xs. adm (\<lambda>ys. P xs ys);
@@ -229,54 +205,12 @@
 done
 
 
-subsection {* Monadic unit *}
+subsection {* Monadic unit and plus *}
 
 definition
   upper_unit :: "'a \<rightarrow> 'a upper_pd" where
   "upper_unit = compact_basis.basis_fun (\<lambda>a. upper_principal (PDUnit a))"
 
-lemma upper_unit_Rep_compact_basis [simp]:
-  "upper_unit\<cdot>(Rep_compact_basis a) = upper_principal (PDUnit a)"
-unfolding upper_unit_def
-apply (rule compact_basis.basis_fun_principal)
-apply (rule upper_principal_mono)
-apply (erule PDUnit_upper_mono)
-done
-
-lemma upper_unit_strict [simp]: "upper_unit\<cdot>\<bottom> = \<bottom>"
-unfolding inst_upper_pd_pcpo Rep_compact_bot [symmetric] by simp
-
-lemma approx_upper_unit [simp]:
-  "approx n\<cdot>(upper_unit\<cdot>x) = upper_unit\<cdot>(approx n\<cdot>x)"
-apply (induct x rule: compact_basis_induct, simp)
-apply (simp add: approx_Rep_compact_basis)
-done
-
-lemma upper_unit_less_iff [simp]:
-  "(upper_unit\<cdot>x \<sqsubseteq> upper_unit\<cdot>y) = (x \<sqsubseteq> y)"
- apply (rule iffI)
-  apply (rule bifinite_less_ext)
-  apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
-  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
-  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
-  apply (clarify, simp add: compact_le_def)
- apply (erule monofun_cfun_arg)
-done
-
-lemma upper_unit_eq_iff [simp]:
-  "(upper_unit\<cdot>x = upper_unit\<cdot>y) = (x = y)"
-unfolding po_eq_conv by simp
-
-lemma upper_unit_strict_iff [simp]: "(upper_unit\<cdot>x = \<bottom>) = (x = \<bottom>)"
-unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
-
-lemma compact_upper_unit_iff [simp]:
-  "compact (upper_unit\<cdot>x) = compact x"
-unfolding bifinite_compact_iff by simp
-
-
-subsection {* Monadic plus *}
-
 definition
   upper_plus :: "'a upper_pd \<rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd" where
   "upper_plus = upper_pd.basis_fun (\<lambda>t. upper_pd.basis_fun (\<lambda>u.
@@ -287,67 +221,89 @@
     (infixl "+\<sharp>" 65) where
   "xs +\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys"
 
+syntax
+  "_upper_pd" :: "args \<Rightarrow> 'a upper_pd" ("{_}\<sharp>")
+
+translations
+  "{x,xs}\<sharp>" == "{x}\<sharp> +\<sharp> {xs}\<sharp>"
+  "{x}\<sharp>" == "CONST upper_unit\<cdot>x"
+
+lemma upper_unit_Rep_compact_basis [simp]:
+  "{Rep_compact_basis a}\<sharp> = upper_principal (PDUnit a)"
+unfolding upper_unit_def
+by (simp add: compact_basis.basis_fun_principal
+    upper_principal_mono PDUnit_upper_mono)
+
 lemma upper_plus_principal [simp]:
-  "upper_plus\<cdot>(upper_principal t)\<cdot>(upper_principal u) =
-   upper_principal (PDPlus t u)"
+  "upper_principal t +\<sharp> upper_principal u = upper_principal (PDPlus t u)"
 unfolding upper_plus_def
 by (simp add: upper_pd.basis_fun_principal
     upper_pd.basis_fun_mono PDPlus_upper_mono)
 
+lemma approx_upper_unit [simp]:
+  "approx n\<cdot>{x}\<sharp> = {approx n\<cdot>x}\<sharp>"
+apply (induct x rule: compact_basis_induct, simp)
+apply (simp add: approx_Rep_compact_basis)
+done
+
 lemma approx_upper_plus [simp]:
-  "approx n\<cdot>(upper_plus\<cdot>xs\<cdot>ys) = upper_plus\<cdot>(approx n\<cdot>xs)\<cdot>(approx n\<cdot>ys)"
+  "approx n\<cdot>(xs +\<sharp> ys) = (approx n\<cdot>xs) +\<sharp> (approx n\<cdot>ys)"
 by (induct xs ys rule: upper_principal_induct2, simp, simp, simp)
 
-lemma upper_plus_commute: "upper_plus\<cdot>xs\<cdot>ys = upper_plus\<cdot>ys\<cdot>xs"
-apply (induct xs ys rule: upper_principal_induct2, simp, simp)
-apply (simp add: PDPlus_commute)
-done
-
-lemma upper_plus_assoc:
-  "upper_plus\<cdot>(upper_plus\<cdot>xs\<cdot>ys)\<cdot>zs = upper_plus\<cdot>xs\<cdot>(upper_plus\<cdot>ys\<cdot>zs)"
+lemma upper_plus_assoc: "(xs +\<sharp> ys) +\<sharp> zs = xs +\<sharp> (ys +\<sharp> zs)"
 apply (induct xs ys arbitrary: zs rule: upper_principal_induct2, simp, simp)
 apply (rule_tac xs=zs in upper_principal_induct, simp)
 apply (simp add: PDPlus_assoc)
 done
 
-lemma upper_plus_absorb: "upper_plus\<cdot>xs\<cdot>xs = xs"
+lemma upper_plus_commute: "xs +\<sharp> ys = ys +\<sharp> xs"
+apply (induct xs ys rule: upper_principal_induct2, simp, simp)
+apply (simp add: PDPlus_commute)
+done
+
+lemma upper_plus_absorb: "xs +\<sharp> xs = xs"
 apply (induct xs rule: upper_principal_induct, simp)
 apply (simp add: PDPlus_absorb)
 done
 
-lemma upper_plus_less1: "upper_plus\<cdot>xs\<cdot>ys \<sqsubseteq> xs"
+interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\<sharp>"]
+  by unfold_locales
+    (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+
+
+lemma upper_plus_left_commute: "xs +\<sharp> (ys +\<sharp> zs) = ys +\<sharp> (xs +\<sharp> zs)"
+by (rule aci_upper_plus.mult_left_commute)
+
+lemma upper_plus_left_absorb: "xs +\<sharp> (xs +\<sharp> ys) = xs +\<sharp> ys"
+by (rule aci_upper_plus.mult_left_idem)
+
+lemmas upper_plus_aci = aci_upper_plus.mult_ac_idem
+
+lemma upper_plus_less1: "xs +\<sharp> ys \<sqsubseteq> xs"
 apply (induct xs ys rule: upper_principal_induct2, simp, simp)
 apply (simp add: PDPlus_upper_less)
 done
 
-lemma upper_plus_less2: "upper_plus\<cdot>xs\<cdot>ys \<sqsubseteq> ys"
+lemma upper_plus_less2: "xs +\<sharp> ys \<sqsubseteq> ys"
 by (subst upper_plus_commute, rule upper_plus_less1)
 
-lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> upper_plus\<cdot>ys\<cdot>zs"
+lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> ys +\<sharp> zs"
 apply (subst upper_plus_absorb [of xs, symmetric])
 apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
 done
 
 lemma upper_less_plus_iff:
-  "(xs \<sqsubseteq> upper_plus\<cdot>ys\<cdot>zs) = (xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs)"
+  "xs \<sqsubseteq> ys +\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs"
 apply safe
 apply (erule trans_less [OF _ upper_plus_less1])
 apply (erule trans_less [OF _ upper_plus_less2])
 apply (erule (1) upper_plus_greatest)
 done
 
-lemma upper_plus_strict1 [simp]: "upper_plus\<cdot>\<bottom>\<cdot>ys = \<bottom>"
-by (rule UU_I, rule upper_plus_less1)
-
-lemma upper_plus_strict2 [simp]: "upper_plus\<cdot>xs\<cdot>\<bottom> = \<bottom>"
-by (rule UU_I, rule upper_plus_less2)
-
 lemma upper_plus_less_unit_iff:
-  "(upper_plus\<cdot>xs\<cdot>ys \<sqsubseteq> upper_unit\<cdot>z) =
-    (xs \<sqsubseteq> upper_unit\<cdot>z \<or> ys \<sqsubseteq> upper_unit\<cdot>z)"
+  "xs +\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>"
  apply (rule iffI)
   apply (subgoal_tac
-    "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>(upper_unit\<cdot>z) \<or> f\<cdot>ys \<sqsubseteq> f\<cdot>(upper_unit\<cdot>z))")
+    "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>{z}\<sharp> \<or> f\<cdot>ys \<sqsubseteq> f\<cdot>{z}\<sharp>)")
    apply (drule admD, rule chain_approx)
     apply (drule_tac f="approx i" in monofun_cfun_arg)
     apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_upper_principal, simp)
@@ -361,19 +317,62 @@
  apply (erule trans_less [OF upper_plus_less2])
 done
 
+lemma upper_unit_less_iff [simp]: "{x}\<sharp> \<sqsubseteq> {y}\<sharp> \<longleftrightarrow> x \<sqsubseteq> y"
+ apply (rule iffI)
+  apply (rule bifinite_less_ext)
+  apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
+  apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
+  apply (cut_tac x="approx i\<cdot>y" in compact_imp_Rep_compact_basis, simp)
+  apply (clarify, simp add: compact_le_def)
+ apply (erule monofun_cfun_arg)
+done
+
 lemmas upper_pd_less_simps =
   upper_unit_less_iff
   upper_less_plus_iff
   upper_plus_less_unit_iff
 
+lemma upper_unit_eq_iff [simp]: "{x}\<sharp> = {y}\<sharp> \<longleftrightarrow> x = y"
+unfolding po_eq_conv by simp
+
+lemma upper_unit_strict [simp]: "{\<bottom>}\<sharp> = \<bottom>"
+unfolding inst_upper_pd_pcpo Rep_compact_bot [symmetric] by simp
+
+lemma upper_plus_strict1 [simp]: "\<bottom> +\<sharp> ys = \<bottom>"
+by (rule UU_I, rule upper_plus_less1)
+
+lemma upper_plus_strict2 [simp]: "xs +\<sharp> \<bottom> = \<bottom>"
+by (rule UU_I, rule upper_plus_less2)
+
+lemma upper_unit_strict_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
+unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
+
+lemma upper_plus_strict_iff [simp]:
+  "xs +\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>"
+apply (rule iffI)
+apply (erule rev_mp)
+apply (rule upper_principal_induct2 [where xs=xs and ys=ys], simp, simp)
+apply (simp add: inst_upper_pd_pcpo upper_principal_eq_iff
+                 upper_le_PDPlus_PDUnit_iff)
+apply auto
+done
+
+lemma compact_upper_unit_iff [simp]: "compact {x}\<sharp> \<longleftrightarrow> compact x"
+unfolding bifinite_compact_iff by simp
+
+lemma compact_upper_plus [simp]:
+  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<sharp> ys)"
+apply (drule compact_imp_upper_principal)+
+apply (auto simp add: compact_upper_principal)
+done
+
 
 subsection {* Induction rules *}
 
 lemma upper_pd_induct1:
   assumes P: "adm P"
-  assumes unit: "\<And>x. P (upper_unit\<cdot>x)"
-  assumes insert:
-    "\<And>x ys. \<lbrakk>P (upper_unit\<cdot>x); P ys\<rbrakk> \<Longrightarrow> P (upper_plus\<cdot>(upper_unit\<cdot>x)\<cdot>ys)"
+  assumes unit: "\<And>x. P {x}\<sharp>"
+  assumes insert: "\<And>x ys. \<lbrakk>P {x}\<sharp>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<sharp> +\<sharp> ys)"
   shows "P (xs::'a upper_pd)"
 apply (induct xs rule: upper_principal_induct, rule P)
 apply (induct_tac t rule: pd_basis_induct1)
@@ -386,8 +385,8 @@
 
 lemma upper_pd_induct:
   assumes P: "adm P"
-  assumes unit: "\<And>x. P (upper_unit\<cdot>x)"
-  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (upper_plus\<cdot>xs\<cdot>ys)"
+  assumes unit: "\<And>x. P {x}\<sharp>"
+  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<sharp> ys)"
   shows "P (xs::'a upper_pd)"
 apply (induct xs rule: upper_principal_induct, rule P)
 apply (induct_tac t rule: pd_basis_induct)
@@ -403,9 +402,10 @@
   "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where
   "upper_bind_basis = fold_pd
     (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
-    (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
+    (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
 
-lemma ACI_upper_bind: "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. upper_plus\<cdot>(x\<cdot>f)\<cdot>(y\<cdot>f))"
+lemma ACI_upper_bind:
+  "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
 apply unfold_locales
 apply (simp add: upper_plus_assoc)
 apply (simp add: upper_plus_commute)
@@ -416,11 +416,11 @@
   "upper_bind_basis (PDUnit a) =
     (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   "upper_bind_basis (PDPlus t u) =
-    (\<Lambda> f. upper_plus\<cdot>(upper_bind_basis t\<cdot>f)\<cdot>(upper_bind_basis u\<cdot>f))"
+    (\<Lambda> f. upper_bind_basis t\<cdot>f +\<sharp> upper_bind_basis u\<cdot>f)"
 unfolding upper_bind_basis_def
 apply -
-apply (rule ab_semigroup_idem_mult.fold_pd_PDUnit [OF ACI_upper_bind])
-apply (rule ab_semigroup_idem_mult.fold_pd_PDPlus [OF ACI_upper_bind])
+apply (rule fold_pd_PDUnit [OF ACI_upper_bind])
+apply (rule fold_pd_PDPlus [OF ACI_upper_bind])
 done
 
 lemma upper_bind_basis_mono:
@@ -444,12 +444,11 @@
 done
 
 lemma upper_bind_unit [simp]:
-  "upper_bind\<cdot>(upper_unit\<cdot>x)\<cdot>f = f\<cdot>x"
+  "upper_bind\<cdot>{x}\<sharp>\<cdot>f = f\<cdot>x"
 by (induct x rule: compact_basis_induct, simp, simp)
 
 lemma upper_bind_plus [simp]:
-  "upper_bind\<cdot>(upper_plus\<cdot>xs\<cdot>ys)\<cdot>f =
-   upper_plus\<cdot>(upper_bind\<cdot>xs\<cdot>f)\<cdot>(upper_bind\<cdot>ys\<cdot>f)"
+  "upper_bind\<cdot>(xs +\<sharp> ys)\<cdot>f = upper_bind\<cdot>xs\<cdot>f +\<sharp> upper_bind\<cdot>ys\<cdot>f"
 by (induct xs ys rule: upper_principal_induct2, simp, simp, simp)
 
 lemma upper_bind_strict [simp]: "upper_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
@@ -460,28 +459,26 @@
 
 definition
   upper_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a upper_pd \<rightarrow> 'b upper_pd" where
-  "upper_map = (\<Lambda> f xs. upper_bind\<cdot>xs\<cdot>(\<Lambda> x. upper_unit\<cdot>(f\<cdot>x)))"
+  "upper_map = (\<Lambda> f xs. upper_bind\<cdot>xs\<cdot>(\<Lambda> x. {f\<cdot>x}\<sharp>))"
 
 definition
   upper_join :: "'a upper_pd upper_pd \<rightarrow> 'a upper_pd" where
   "upper_join = (\<Lambda> xss. upper_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))"
 
 lemma upper_map_unit [simp]:
-  "upper_map\<cdot>f\<cdot>(upper_unit\<cdot>x) = upper_unit\<cdot>(f\<cdot>x)"
+  "upper_map\<cdot>f\<cdot>{x}\<sharp> = {f\<cdot>x}\<sharp>"
 unfolding upper_map_def by simp
 
 lemma upper_map_plus [simp]:
-  "upper_map\<cdot>f\<cdot>(upper_plus\<cdot>xs\<cdot>ys) =
-   upper_plus\<cdot>(upper_map\<cdot>f\<cdot>xs)\<cdot>(upper_map\<cdot>f\<cdot>ys)"
+  "upper_map\<cdot>f\<cdot>(xs +\<sharp> ys) = upper_map\<cdot>f\<cdot>xs +\<sharp> upper_map\<cdot>f\<cdot>ys"
 unfolding upper_map_def by simp
 
 lemma upper_join_unit [simp]:
-  "upper_join\<cdot>(upper_unit\<cdot>xs) = xs"
+  "upper_join\<cdot>{xs}\<sharp> = xs"
 unfolding upper_join_def by simp
 
 lemma upper_join_plus [simp]:
-  "upper_join\<cdot>(upper_plus\<cdot>xss\<cdot>yss) =
-   upper_plus\<cdot>(upper_join\<cdot>xss)\<cdot>(upper_join\<cdot>yss)"
+  "upper_join\<cdot>(xss +\<sharp> yss) = upper_join\<cdot>xss +\<sharp> upper_join\<cdot>yss"
 unfolding upper_join_def by simp
 
 lemma upper_map_ident: "upper_map\<cdot>(\<Lambda> x. x)\<cdot>xs = xs"