# HG changeset patch
# User huffman
# Date 1293133919 28800
# Node ID ad093e4638e25297aa605620749b6e268e7aabdd
# Parent  f2bb6541f5325306f01b57696d4346ee07fcca41
changed syntax of powerdomain binary union operators

diff -r f2bb6541f532 -r ad093e4638e2 src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Thu Dec 23 12:20:09 2010 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy	Thu Dec 23 11:51:59 2010 -0800
@@ -177,14 +177,14 @@
 
 abbreviation
   convex_add :: "'a convex_pd \<Rightarrow> 'a convex_pd \<Rightarrow> 'a convex_pd"
-    (infixl "+\<natural>" 65) where
-  "xs +\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
+    (infixl "\<union>\<natural>" 65) where
+  "xs \<union>\<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,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>"
   "{x}\<natural>" == "CONST convex_unit\<cdot>x"
 
 lemma convex_unit_Rep_compact_basis [simp]:
@@ -193,23 +193,23 @@
 by (simp add: compact_basis.extension_principal PDUnit_convex_mono)
 
 lemma convex_plus_principal [simp]:
-  "convex_principal t +\<natural> convex_principal u = convex_principal (PDPlus t u)"
+  "convex_principal t \<union>\<natural> convex_principal u = convex_principal (PDPlus t u)"
 unfolding convex_plus_def
 by (simp add: convex_pd.extension_principal
     convex_pd.extension_mono PDPlus_convex_mono)
 
 interpretation convex_add: semilattice convex_add proof
   fix xs ys zs :: "'a convex_pd"
-  show "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)"
+  show "(xs \<union>\<natural> ys) \<union>\<natural> zs = xs \<union>\<natural> (ys \<union>\<natural> zs)"
     apply (induct xs ys arbitrary: zs rule: convex_pd.principal_induct2, simp, simp)
     apply (rule_tac x=zs in convex_pd.principal_induct, simp)
     apply (simp add: PDPlus_assoc)
     done
-  show "xs +\<natural> ys = ys +\<natural> xs"
+  show "xs \<union>\<natural> ys = ys \<union>\<natural> xs"
     apply (induct xs ys rule: convex_pd.principal_induct2, simp, simp)
     apply (simp add: PDPlus_commute)
     done
-  show "xs +\<natural> xs = xs"
+  show "xs \<union>\<natural> xs = xs"
     apply (induct xs rule: convex_pd.principal_induct, simp)
     apply (simp add: PDPlus_absorb)
     done
@@ -230,7 +230,7 @@
   convex_plus_ac convex_plus_absorb convex_plus_left_absorb
 
 lemma convex_unit_below_plus_iff [simp]:
-  "{x}\<natural> \<sqsubseteq> ys +\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs"
+  "{x}\<natural> \<sqsubseteq> ys \<union>\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs"
 apply (induct x rule: compact_basis.principal_induct, simp)
 apply (induct ys rule: convex_pd.principal_induct, simp)
 apply (induct zs rule: convex_pd.principal_induct, simp)
@@ -238,7 +238,7 @@
 done
 
 lemma convex_plus_below_unit_iff [simp]:
-  "xs +\<natural> ys \<sqsubseteq> {z}\<natural> \<longleftrightarrow> xs \<sqsubseteq> {z}\<natural> \<and> ys \<sqsubseteq> {z}\<natural>"
+  "xs \<union>\<natural> ys \<sqsubseteq> {z}\<natural> \<longleftrightarrow> xs \<sqsubseteq> {z}\<natural> \<and> ys \<sqsubseteq> {z}\<natural>"
 apply (induct xs rule: convex_pd.principal_induct, simp)
 apply (induct ys rule: convex_pd.principal_induct, simp)
 apply (induct z rule: compact_basis.principal_induct, simp)
@@ -271,7 +271,7 @@
 done
 
 lemma compact_convex_plus [simp]:
-  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<natural> ys)"
+  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs \<union>\<natural> ys)"
 by (auto dest!: convex_pd.compact_imp_principal)
 
 
@@ -280,7 +280,7 @@
 lemma convex_pd_induct1:
   assumes P: "adm P"
   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)"
+  assumes insert: "\<And>x ys. \<lbrakk>P {x}\<natural>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<natural> \<union>\<natural> ys)"
   shows "P (xs::'a convex_pd)"
 apply (induct xs rule: convex_pd.principal_induct, rule P)
 apply (induct_tac a rule: pd_basis_induct1)
@@ -295,7 +295,7 @@
   [case_names adm convex_unit convex_plus, induct type: convex_pd]:
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<natural>"
-  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<natural> ys)"
+  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<natural> ys)"
   shows "P (xs::'a convex_pd)"
 apply (induct xs rule: convex_pd.principal_induct, rule P)
 apply (induct_tac a rule: pd_basis_induct)
@@ -311,10 +311,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. x\<cdot>f +\<natural> y\<cdot>f)"
+    (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<natural> y\<cdot>f)"
 
 lemma ACI_convex_bind:
-  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
+  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<natural> y\<cdot>f)"
 apply unfold_locales
 apply (simp add: convex_plus_assoc)
 apply (simp add: convex_plus_commute)
@@ -325,7 +325,7 @@
   "convex_bind_basis (PDUnit a) =
     (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   "convex_bind_basis (PDPlus t u) =
-    (\<Lambda> f. convex_bind_basis t\<cdot>f +\<natural> convex_bind_basis u\<cdot>f)"
+    (\<Lambda> f. convex_bind_basis t\<cdot>f \<union>\<natural> convex_bind_basis u\<cdot>f)"
 unfolding convex_bind_basis_def
 apply -
 apply (rule fold_pd_PDUnit [OF ACI_convex_bind])
@@ -363,7 +363,7 @@
 by (induct x rule: compact_basis.principal_induct, simp, simp)
 
 lemma convex_bind_plus [simp]:
-  "convex_bind\<cdot>(xs +\<natural> ys)\<cdot>f = convex_bind\<cdot>xs\<cdot>f +\<natural> convex_bind\<cdot>ys\<cdot>f"
+  "convex_bind\<cdot>(xs \<union>\<natural> ys)\<cdot>f = convex_bind\<cdot>xs\<cdot>f \<union>\<natural> convex_bind\<cdot>ys\<cdot>f"
 by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
 
 lemma convex_bind_strict [simp]: "convex_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
@@ -386,7 +386,7 @@
 unfolding convex_map_def by simp
 
 lemma convex_map_plus [simp]:
-  "convex_map\<cdot>f\<cdot>(xs +\<natural> ys) = convex_map\<cdot>f\<cdot>xs +\<natural> convex_map\<cdot>f\<cdot>ys"
+  "convex_map\<cdot>f\<cdot>(xs \<union>\<natural> ys) = convex_map\<cdot>f\<cdot>xs \<union>\<natural> convex_map\<cdot>f\<cdot>ys"
 unfolding convex_map_def by simp
 
 lemma convex_map_bottom [simp]: "convex_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<natural>"
@@ -492,7 +492,7 @@
 unfolding convex_join_def by simp
 
 lemma convex_join_plus [simp]:
-  "convex_join\<cdot>(xss +\<natural> yss) = convex_join\<cdot>xss +\<natural> convex_join\<cdot>yss"
+  "convex_join\<cdot>(xss \<union>\<natural> yss) = convex_join\<cdot>xss \<union>\<natural> convex_join\<cdot>yss"
 unfolding convex_join_def by simp
 
 lemma convex_join_bottom [simp]: "convex_join\<cdot>\<bottom> = \<bottom>"
@@ -536,7 +536,7 @@
 by (induct x rule: compact_basis.principal_induct, simp, simp)
 
 lemma convex_to_upper_plus [simp]:
-  "convex_to_upper\<cdot>(xs +\<natural> ys) = convex_to_upper\<cdot>xs +\<sharp> convex_to_upper\<cdot>ys"
+  "convex_to_upper\<cdot>(xs \<union>\<natural> ys) = convex_to_upper\<cdot>xs \<union>\<sharp> convex_to_upper\<cdot>ys"
 by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
 
 lemma convex_to_upper_bind [simp]:
@@ -575,7 +575,7 @@
 by (induct x rule: compact_basis.principal_induct, simp, simp)
 
 lemma convex_to_lower_plus [simp]:
-  "convex_to_lower\<cdot>(xs +\<natural> ys) = convex_to_lower\<cdot>xs +\<flat> convex_to_lower\<cdot>ys"
+  "convex_to_lower\<cdot>(xs \<union>\<natural> ys) = convex_to_lower\<cdot>xs \<union>\<flat> convex_to_lower\<cdot>ys"
 by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
 
 lemma convex_to_lower_bind [simp]:
@@ -604,7 +604,7 @@
 done
 
 lemmas convex_plus_below_plus_iff =
-  convex_pd_below_iff [where xs="xs +\<natural> ys" and ys="zs +\<natural> ws", standard]
+  convex_pd_below_iff [where xs="xs \<union>\<natural> ys" and ys="zs \<union>\<natural> ws", standard]
 
 lemmas convex_pd_below_simps =
   convex_unit_below_plus_iff
diff -r f2bb6541f532 -r ad093e4638e2 src/HOL/HOLCF/LowerPD.thy
--- a/src/HOL/HOLCF/LowerPD.thy	Thu Dec 23 12:20:09 2010 +0100
+++ b/src/HOL/HOLCF/LowerPD.thy	Thu Dec 23 11:51:59 2010 -0800
@@ -132,14 +132,14 @@
 
 abbreviation
   lower_add :: "'a lower_pd \<Rightarrow> 'a lower_pd \<Rightarrow> 'a lower_pd"
-    (infixl "+\<flat>" 65) where
-  "xs +\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
+    (infixl "\<union>\<flat>" 65) where
+  "xs \<union>\<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,xs}\<flat>" == "{x}\<flat> \<union>\<flat> {xs}\<flat>"
   "{x}\<flat>" == "CONST lower_unit\<cdot>x"
 
 lemma lower_unit_Rep_compact_basis [simp]:
@@ -148,23 +148,23 @@
 by (simp add: compact_basis.extension_principal PDUnit_lower_mono)
 
 lemma lower_plus_principal [simp]:
-  "lower_principal t +\<flat> lower_principal u = lower_principal (PDPlus t u)"
+  "lower_principal t \<union>\<flat> lower_principal u = lower_principal (PDPlus t u)"
 unfolding lower_plus_def
 by (simp add: lower_pd.extension_principal
     lower_pd.extension_mono PDPlus_lower_mono)
 
 interpretation lower_add: semilattice lower_add proof
   fix xs ys zs :: "'a lower_pd"
-  show "(xs +\<flat> ys) +\<flat> zs = xs +\<flat> (ys +\<flat> zs)"
+  show "(xs \<union>\<flat> ys) \<union>\<flat> zs = xs \<union>\<flat> (ys \<union>\<flat> zs)"
     apply (induct xs ys arbitrary: zs rule: lower_pd.principal_induct2, simp, simp)
     apply (rule_tac x=zs in lower_pd.principal_induct, simp)
     apply (simp add: PDPlus_assoc)
     done
-  show "xs +\<flat> ys = ys +\<flat> xs"
+  show "xs \<union>\<flat> ys = ys \<union>\<flat> xs"
     apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
     apply (simp add: PDPlus_commute)
     done
-  show "xs +\<flat> xs = xs"
+  show "xs \<union>\<flat> xs = xs"
     apply (induct xs rule: lower_pd.principal_induct, simp)
     apply (simp add: PDPlus_absorb)
     done
@@ -184,21 +184,21 @@
 lemmas lower_plus_aci =
   lower_plus_ac lower_plus_absorb lower_plus_left_absorb
 
-lemma lower_plus_below1: "xs \<sqsubseteq> xs +\<flat> ys"
+lemma lower_plus_below1: "xs \<sqsubseteq> xs \<union>\<flat> ys"
 apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
 apply (simp add: PDPlus_lower_le)
 done
 
-lemma lower_plus_below2: "ys \<sqsubseteq> xs +\<flat> ys"
+lemma lower_plus_below2: "ys \<sqsubseteq> xs \<union>\<flat> ys"
 by (subst lower_plus_commute, rule lower_plus_below1)
 
-lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs +\<flat> ys \<sqsubseteq> zs"
+lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<union>\<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_below_iff [simp]:
-  "xs +\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs"
+  "xs \<union>\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs"
 apply safe
 apply (erule below_trans [OF lower_plus_below1])
 apply (erule below_trans [OF lower_plus_below2])
@@ -206,7 +206,7 @@
 done
 
 lemma lower_unit_below_plus_iff [simp]:
-  "{x}\<flat> \<sqsubseteq> ys +\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
+  "{x}\<flat> \<sqsubseteq> ys \<union>\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
 apply (induct x rule: compact_basis.principal_induct, simp)
 apply (induct ys rule: lower_pd.principal_induct, simp)
 apply (induct zs rule: lower_pd.principal_induct, simp)
@@ -235,19 +235,19 @@
 unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff)
 
 lemma lower_plus_bottom_iff [simp]:
-  "xs +\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
+  "xs \<union>\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
 apply safe
 apply (rule UU_I, erule subst, rule lower_plus_below1)
 apply (rule UU_I, erule subst, rule lower_plus_below2)
 apply (rule lower_plus_absorb)
 done
 
-lemma lower_plus_strict1 [simp]: "\<bottom> +\<flat> ys = ys"
+lemma lower_plus_strict1 [simp]: "\<bottom> \<union>\<flat> ys = ys"
 apply (rule below_antisym [OF _ lower_plus_below2])
 apply (simp add: lower_plus_least)
 done
 
-lemma lower_plus_strict2 [simp]: "xs +\<flat> \<bottom> = xs"
+lemma lower_plus_strict2 [simp]: "xs \<union>\<flat> \<bottom> = xs"
 apply (rule below_antisym [OF _ lower_plus_below1])
 apply (simp add: lower_plus_least)
 done
@@ -262,7 +262,7 @@
 done
 
 lemma compact_lower_plus [simp]:
-  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<flat> ys)"
+  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs \<union>\<flat> ys)"
 by (auto dest!: lower_pd.compact_imp_principal)
 
 
@@ -272,7 +272,7 @@
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<flat>"
   assumes insert:
-    "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> +\<flat> ys)"
+    "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> \<union>\<flat> ys)"
   shows "P (xs::'a lower_pd)"
 apply (induct xs rule: lower_pd.principal_induct, rule P)
 apply (induct_tac a rule: pd_basis_induct1)
@@ -287,7 +287,7 @@
   [case_names adm lower_unit lower_plus, induct type: lower_pd]:
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<flat>"
-  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<flat> ys)"
+  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<flat> ys)"
   shows "P (xs::'a lower_pd)"
 apply (induct xs rule: lower_pd.principal_induct, rule P)
 apply (induct_tac a rule: pd_basis_induct)
@@ -303,10 +303,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. x\<cdot>f +\<flat> y\<cdot>f)"
+    (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<flat> y\<cdot>f)"
 
 lemma ACI_lower_bind:
-  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
+  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<flat> y\<cdot>f)"
 apply unfold_locales
 apply (simp add: lower_plus_assoc)
 apply (simp add: lower_plus_commute)
@@ -317,7 +317,7 @@
   "lower_bind_basis (PDUnit a) =
     (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   "lower_bind_basis (PDPlus t u) =
-    (\<Lambda> f. lower_bind_basis t\<cdot>f +\<flat> lower_bind_basis u\<cdot>f)"
+    (\<Lambda> f. lower_bind_basis t\<cdot>f \<union>\<flat> lower_bind_basis u\<cdot>f)"
 unfolding lower_bind_basis_def
 apply -
 apply (rule fold_pd_PDUnit [OF ACI_lower_bind])
@@ -356,7 +356,7 @@
 by (induct x rule: compact_basis.principal_induct, simp, simp)
 
 lemma lower_bind_plus [simp]:
-  "lower_bind\<cdot>(xs +\<flat> ys)\<cdot>f = lower_bind\<cdot>xs\<cdot>f +\<flat> lower_bind\<cdot>ys\<cdot>f"
+  "lower_bind\<cdot>(xs \<union>\<flat> ys)\<cdot>f = lower_bind\<cdot>xs\<cdot>f \<union>\<flat> lower_bind\<cdot>ys\<cdot>f"
 by (induct xs ys rule: lower_pd.principal_induct2, simp, simp, simp)
 
 lemma lower_bind_strict [simp]: "lower_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
@@ -378,7 +378,7 @@
 unfolding lower_map_def by simp
 
 lemma lower_map_plus [simp]:
-  "lower_map\<cdot>f\<cdot>(xs +\<flat> ys) = lower_map\<cdot>f\<cdot>xs +\<flat> lower_map\<cdot>f\<cdot>ys"
+  "lower_map\<cdot>f\<cdot>(xs \<union>\<flat> ys) = lower_map\<cdot>f\<cdot>xs \<union>\<flat> lower_map\<cdot>f\<cdot>ys"
 unfolding lower_map_def by simp
 
 lemma lower_map_bottom [simp]: "lower_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<flat>"
@@ -484,7 +484,7 @@
 unfolding lower_join_def by simp
 
 lemma lower_join_plus [simp]:
-  "lower_join\<cdot>(xss +\<flat> yss) = lower_join\<cdot>xss +\<flat> lower_join\<cdot>yss"
+  "lower_join\<cdot>(xss \<union>\<flat> yss) = lower_join\<cdot>xss \<union>\<flat> lower_join\<cdot>yss"
 unfolding lower_join_def by simp
 
 lemma lower_join_bottom [simp]: "lower_join\<cdot>\<bottom> = \<bottom>"
diff -r f2bb6541f532 -r ad093e4638e2 src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Thu Dec 23 12:20:09 2010 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy	Thu Dec 23 11:51:59 2010 -0800
@@ -130,14 +130,14 @@
 
 abbreviation
   upper_add :: "'a upper_pd \<Rightarrow> 'a upper_pd \<Rightarrow> 'a upper_pd"
-    (infixl "+\<sharp>" 65) where
-  "xs +\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys"
+    (infixl "\<union>\<sharp>" 65) where
+  "xs \<union>\<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,xs}\<sharp>" == "{x}\<sharp> \<union>\<sharp> {xs}\<sharp>"
   "{x}\<sharp>" == "CONST upper_unit\<cdot>x"
 
 lemma upper_unit_Rep_compact_basis [simp]:
@@ -146,23 +146,23 @@
 by (simp add: compact_basis.extension_principal PDUnit_upper_mono)
 
 lemma upper_plus_principal [simp]:
-  "upper_principal t +\<sharp> upper_principal u = upper_principal (PDPlus t u)"
+  "upper_principal t \<union>\<sharp> upper_principal u = upper_principal (PDPlus t u)"
 unfolding upper_plus_def
 by (simp add: upper_pd.extension_principal
     upper_pd.extension_mono PDPlus_upper_mono)
 
 interpretation upper_add: semilattice upper_add proof
   fix xs ys zs :: "'a upper_pd"
-  show "(xs +\<sharp> ys) +\<sharp> zs = xs +\<sharp> (ys +\<sharp> zs)"
+  show "(xs \<union>\<sharp> ys) \<union>\<sharp> zs = xs \<union>\<sharp> (ys \<union>\<sharp> zs)"
     apply (induct xs ys arbitrary: zs rule: upper_pd.principal_induct2, simp, simp)
     apply (rule_tac x=zs in upper_pd.principal_induct, simp)
     apply (simp add: PDPlus_assoc)
     done
-  show "xs +\<sharp> ys = ys +\<sharp> xs"
+  show "xs \<union>\<sharp> ys = ys \<union>\<sharp> xs"
     apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
     apply (simp add: PDPlus_commute)
     done
-  show "xs +\<sharp> xs = xs"
+  show "xs \<union>\<sharp> xs = xs"
     apply (induct xs rule: upper_pd.principal_induct, simp)
     apply (simp add: PDPlus_absorb)
     done
@@ -182,21 +182,21 @@
 lemmas upper_plus_aci =
   upper_plus_ac upper_plus_absorb upper_plus_left_absorb
 
-lemma upper_plus_below1: "xs +\<sharp> ys \<sqsubseteq> xs"
+lemma upper_plus_below1: "xs \<union>\<sharp> ys \<sqsubseteq> xs"
 apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
 apply (simp add: PDPlus_upper_le)
 done
 
-lemma upper_plus_below2: "xs +\<sharp> ys \<sqsubseteq> ys"
+lemma upper_plus_below2: "xs \<union>\<sharp> ys \<sqsubseteq> ys"
 by (subst upper_plus_commute, rule upper_plus_below1)
 
-lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> ys +\<sharp> zs"
+lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> ys \<union>\<sharp> zs"
 apply (subst upper_plus_absorb [of xs, symmetric])
 apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
 done
 
 lemma upper_below_plus_iff [simp]:
-  "xs \<sqsubseteq> ys +\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs"
+  "xs \<sqsubseteq> ys \<union>\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs"
 apply safe
 apply (erule below_trans [OF _ upper_plus_below1])
 apply (erule below_trans [OF _ upper_plus_below2])
@@ -204,7 +204,7 @@
 done
 
 lemma upper_plus_below_unit_iff [simp]:
-  "xs +\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>"
+  "xs \<union>\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>"
 apply (induct xs rule: upper_pd.principal_induct, simp)
 apply (induct ys rule: upper_pd.principal_induct, simp)
 apply (induct z rule: compact_basis.principal_induct, simp)
@@ -229,17 +229,17 @@
 using upper_unit_Rep_compact_basis [of compact_bot]
 by (simp add: inst_upper_pd_pcpo)
 
-lemma upper_plus_strict1 [simp]: "\<bottom> +\<sharp> ys = \<bottom>"
+lemma upper_plus_strict1 [simp]: "\<bottom> \<union>\<sharp> ys = \<bottom>"
 by (rule UU_I, rule upper_plus_below1)
 
-lemma upper_plus_strict2 [simp]: "xs +\<sharp> \<bottom> = \<bottom>"
+lemma upper_plus_strict2 [simp]: "xs \<union>\<sharp> \<bottom> = \<bottom>"
 by (rule UU_I, rule upper_plus_below2)
 
 lemma upper_unit_bottom_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
 unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
 
 lemma upper_plus_bottom_iff [simp]:
-  "xs +\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>"
+  "xs \<union>\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>"
 apply (rule iffI)
 apply (erule rev_mp)
 apply (rule upper_pd.principal_induct2 [where x=xs and y=ys], simp, simp)
@@ -258,7 +258,7 @@
 done
 
 lemma compact_upper_plus [simp]:
-  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<sharp> ys)"
+  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs \<union>\<sharp> ys)"
 by (auto dest!: upper_pd.compact_imp_principal)
 
 
@@ -267,7 +267,7 @@
 lemma upper_pd_induct1:
   assumes P: "adm P"
   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)"
+  assumes insert: "\<And>x ys. \<lbrakk>P {x}\<sharp>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<sharp> \<union>\<sharp> ys)"
   shows "P (xs::'a upper_pd)"
 apply (induct xs rule: upper_pd.principal_induct, rule P)
 apply (induct_tac a rule: pd_basis_induct1)
@@ -282,7 +282,7 @@
   [case_names adm upper_unit upper_plus, induct type: upper_pd]:
   assumes P: "adm P"
   assumes unit: "\<And>x. P {x}\<sharp>"
-  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<sharp> ys)"
+  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<sharp> ys)"
   shows "P (xs::'a upper_pd)"
 apply (induct xs rule: upper_pd.principal_induct, rule P)
 apply (induct_tac a rule: pd_basis_induct)
@@ -298,10 +298,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. x\<cdot>f +\<sharp> y\<cdot>f)"
+    (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<sharp> y\<cdot>f)"
 
 lemma ACI_upper_bind:
-  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
+  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<sharp> y\<cdot>f)"
 apply unfold_locales
 apply (simp add: upper_plus_assoc)
 apply (simp add: upper_plus_commute)
@@ -312,7 +312,7 @@
   "upper_bind_basis (PDUnit a) =
     (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   "upper_bind_basis (PDPlus t u) =
-    (\<Lambda> f. upper_bind_basis t\<cdot>f +\<sharp> upper_bind_basis u\<cdot>f)"
+    (\<Lambda> f. upper_bind_basis t\<cdot>f \<union>\<sharp> upper_bind_basis u\<cdot>f)"
 unfolding upper_bind_basis_def
 apply -
 apply (rule fold_pd_PDUnit [OF ACI_upper_bind])
@@ -351,7 +351,7 @@
 by (induct x rule: compact_basis.principal_induct, simp, simp)
 
 lemma upper_bind_plus [simp]:
-  "upper_bind\<cdot>(xs +\<sharp> ys)\<cdot>f = upper_bind\<cdot>xs\<cdot>f +\<sharp> upper_bind\<cdot>ys\<cdot>f"
+  "upper_bind\<cdot>(xs \<union>\<sharp> ys)\<cdot>f = upper_bind\<cdot>xs\<cdot>f \<union>\<sharp> upper_bind\<cdot>ys\<cdot>f"
 by (induct xs ys rule: upper_pd.principal_induct2, simp, simp, simp)
 
 lemma upper_bind_strict [simp]: "upper_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
@@ -373,7 +373,7 @@
 unfolding upper_map_def by simp
 
 lemma upper_map_plus [simp]:
-  "upper_map\<cdot>f\<cdot>(xs +\<sharp> ys) = upper_map\<cdot>f\<cdot>xs +\<sharp> upper_map\<cdot>f\<cdot>ys"
+  "upper_map\<cdot>f\<cdot>(xs \<union>\<sharp> ys) = upper_map\<cdot>f\<cdot>xs \<union>\<sharp> upper_map\<cdot>f\<cdot>ys"
 unfolding upper_map_def by simp
 
 lemma upper_map_bottom [simp]: "upper_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<sharp>"
@@ -479,7 +479,7 @@
 unfolding upper_join_def by simp
 
 lemma upper_join_plus [simp]:
-  "upper_join\<cdot>(xss +\<sharp> yss) = upper_join\<cdot>xss +\<sharp> upper_join\<cdot>yss"
+  "upper_join\<cdot>(xss \<union>\<sharp> yss) = upper_join\<cdot>xss \<union>\<sharp> upper_join\<cdot>yss"
 unfolding upper_join_def by simp
 
 lemma upper_join_bottom [simp]: "upper_join\<cdot>\<bottom> = \<bottom>"
diff -r f2bb6541f532 -r ad093e4638e2 src/HOL/HOLCF/ex/Powerdomain_ex.thy
--- a/src/HOL/HOLCF/ex/Powerdomain_ex.thy	Thu Dec 23 12:20:09 2010 +0100
+++ b/src/HOL/HOLCF/ex/Powerdomain_ex.thy	Thu Dec 23 11:51:59 2010 -0800
@@ -62,7 +62,7 @@
   pick :: "'a tree \<rightarrow> 'a convex_pd"
 where
   pick_Leaf: "pick\<cdot>(Leaf\<cdot>a) = {a}\<natural>"
-| pick_Node: "pick\<cdot>(Node\<cdot>l\<cdot>r) = pick\<cdot>l +\<natural> pick\<cdot>r"
+| pick_Node: "pick\<cdot>(Node\<cdot>l\<cdot>r) = pick\<cdot>l \<union>\<natural> pick\<cdot>r"
 
 lemma pick_strict [simp]: "pick\<cdot>\<bottom> = \<bottom>"
 by fixrec_simp