changed syntax of powerdomain binary union operators
authorhuffman
Thu Dec 23 11:51:59 2010 -0800 (2010-12-23)
changeset 41399ad093e4638e2
parent 41398 f2bb6541f532
child 41400 1a7557cc686a
changed syntax of powerdomain binary union operators
src/HOL/HOLCF/ConvexPD.thy
src/HOL/HOLCF/LowerPD.thy
src/HOL/HOLCF/UpperPD.thy
src/HOL/HOLCF/ex/Powerdomain_ex.thy
     1.1 --- a/src/HOL/HOLCF/ConvexPD.thy	Thu Dec 23 12:20:09 2010 +0100
     1.2 +++ b/src/HOL/HOLCF/ConvexPD.thy	Thu Dec 23 11:51:59 2010 -0800
     1.3 @@ -177,14 +177,14 @@
     1.4  
     1.5  abbreviation
     1.6    convex_add :: "'a convex_pd \<Rightarrow> 'a convex_pd \<Rightarrow> 'a convex_pd"
     1.7 -    (infixl "+\<natural>" 65) where
     1.8 -  "xs +\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
     1.9 +    (infixl "\<union>\<natural>" 65) where
    1.10 +  "xs \<union>\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
    1.11  
    1.12  syntax
    1.13    "_convex_pd" :: "args \<Rightarrow> 'a convex_pd" ("{_}\<natural>")
    1.14  
    1.15  translations
    1.16 -  "{x,xs}\<natural>" == "{x}\<natural> +\<natural> {xs}\<natural>"
    1.17 +  "{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>"
    1.18    "{x}\<natural>" == "CONST convex_unit\<cdot>x"
    1.19  
    1.20  lemma convex_unit_Rep_compact_basis [simp]:
    1.21 @@ -193,23 +193,23 @@
    1.22  by (simp add: compact_basis.extension_principal PDUnit_convex_mono)
    1.23  
    1.24  lemma convex_plus_principal [simp]:
    1.25 -  "convex_principal t +\<natural> convex_principal u = convex_principal (PDPlus t u)"
    1.26 +  "convex_principal t \<union>\<natural> convex_principal u = convex_principal (PDPlus t u)"
    1.27  unfolding convex_plus_def
    1.28  by (simp add: convex_pd.extension_principal
    1.29      convex_pd.extension_mono PDPlus_convex_mono)
    1.30  
    1.31  interpretation convex_add: semilattice convex_add proof
    1.32    fix xs ys zs :: "'a convex_pd"
    1.33 -  show "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)"
    1.34 +  show "(xs \<union>\<natural> ys) \<union>\<natural> zs = xs \<union>\<natural> (ys \<union>\<natural> zs)"
    1.35      apply (induct xs ys arbitrary: zs rule: convex_pd.principal_induct2, simp, simp)
    1.36      apply (rule_tac x=zs in convex_pd.principal_induct, simp)
    1.37      apply (simp add: PDPlus_assoc)
    1.38      done
    1.39 -  show "xs +\<natural> ys = ys +\<natural> xs"
    1.40 +  show "xs \<union>\<natural> ys = ys \<union>\<natural> xs"
    1.41      apply (induct xs ys rule: convex_pd.principal_induct2, simp, simp)
    1.42      apply (simp add: PDPlus_commute)
    1.43      done
    1.44 -  show "xs +\<natural> xs = xs"
    1.45 +  show "xs \<union>\<natural> xs = xs"
    1.46      apply (induct xs rule: convex_pd.principal_induct, simp)
    1.47      apply (simp add: PDPlus_absorb)
    1.48      done
    1.49 @@ -230,7 +230,7 @@
    1.50    convex_plus_ac convex_plus_absorb convex_plus_left_absorb
    1.51  
    1.52  lemma convex_unit_below_plus_iff [simp]:
    1.53 -  "{x}\<natural> \<sqsubseteq> ys +\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs"
    1.54 +  "{x}\<natural> \<sqsubseteq> ys \<union>\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs"
    1.55  apply (induct x rule: compact_basis.principal_induct, simp)
    1.56  apply (induct ys rule: convex_pd.principal_induct, simp)
    1.57  apply (induct zs rule: convex_pd.principal_induct, simp)
    1.58 @@ -238,7 +238,7 @@
    1.59  done
    1.60  
    1.61  lemma convex_plus_below_unit_iff [simp]:
    1.62 -  "xs +\<natural> ys \<sqsubseteq> {z}\<natural> \<longleftrightarrow> xs \<sqsubseteq> {z}\<natural> \<and> ys \<sqsubseteq> {z}\<natural>"
    1.63 +  "xs \<union>\<natural> ys \<sqsubseteq> {z}\<natural> \<longleftrightarrow> xs \<sqsubseteq> {z}\<natural> \<and> ys \<sqsubseteq> {z}\<natural>"
    1.64  apply (induct xs rule: convex_pd.principal_induct, simp)
    1.65  apply (induct ys rule: convex_pd.principal_induct, simp)
    1.66  apply (induct z rule: compact_basis.principal_induct, simp)
    1.67 @@ -271,7 +271,7 @@
    1.68  done
    1.69  
    1.70  lemma compact_convex_plus [simp]:
    1.71 -  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<natural> ys)"
    1.72 +  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs \<union>\<natural> ys)"
    1.73  by (auto dest!: convex_pd.compact_imp_principal)
    1.74  
    1.75  
    1.76 @@ -280,7 +280,7 @@
    1.77  lemma convex_pd_induct1:
    1.78    assumes P: "adm P"
    1.79    assumes unit: "\<And>x. P {x}\<natural>"
    1.80 -  assumes insert: "\<And>x ys. \<lbrakk>P {x}\<natural>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<natural> +\<natural> ys)"
    1.81 +  assumes insert: "\<And>x ys. \<lbrakk>P {x}\<natural>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<natural> \<union>\<natural> ys)"
    1.82    shows "P (xs::'a convex_pd)"
    1.83  apply (induct xs rule: convex_pd.principal_induct, rule P)
    1.84  apply (induct_tac a rule: pd_basis_induct1)
    1.85 @@ -295,7 +295,7 @@
    1.86    [case_names adm convex_unit convex_plus, induct type: convex_pd]:
    1.87    assumes P: "adm P"
    1.88    assumes unit: "\<And>x. P {x}\<natural>"
    1.89 -  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<natural> ys)"
    1.90 +  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<natural> ys)"
    1.91    shows "P (xs::'a convex_pd)"
    1.92  apply (induct xs rule: convex_pd.principal_induct, rule P)
    1.93  apply (induct_tac a rule: pd_basis_induct)
    1.94 @@ -311,10 +311,10 @@
    1.95    "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where
    1.96    "convex_bind_basis = fold_pd
    1.97      (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
    1.98 -    (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
    1.99 +    (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<natural> y\<cdot>f)"
   1.100  
   1.101  lemma ACI_convex_bind:
   1.102 -  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
   1.103 +  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<natural> y\<cdot>f)"
   1.104  apply unfold_locales
   1.105  apply (simp add: convex_plus_assoc)
   1.106  apply (simp add: convex_plus_commute)
   1.107 @@ -325,7 +325,7 @@
   1.108    "convex_bind_basis (PDUnit a) =
   1.109      (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   1.110    "convex_bind_basis (PDPlus t u) =
   1.111 -    (\<Lambda> f. convex_bind_basis t\<cdot>f +\<natural> convex_bind_basis u\<cdot>f)"
   1.112 +    (\<Lambda> f. convex_bind_basis t\<cdot>f \<union>\<natural> convex_bind_basis u\<cdot>f)"
   1.113  unfolding convex_bind_basis_def
   1.114  apply -
   1.115  apply (rule fold_pd_PDUnit [OF ACI_convex_bind])
   1.116 @@ -363,7 +363,7 @@
   1.117  by (induct x rule: compact_basis.principal_induct, simp, simp)
   1.118  
   1.119  lemma convex_bind_plus [simp]:
   1.120 -  "convex_bind\<cdot>(xs +\<natural> ys)\<cdot>f = convex_bind\<cdot>xs\<cdot>f +\<natural> convex_bind\<cdot>ys\<cdot>f"
   1.121 +  "convex_bind\<cdot>(xs \<union>\<natural> ys)\<cdot>f = convex_bind\<cdot>xs\<cdot>f \<union>\<natural> convex_bind\<cdot>ys\<cdot>f"
   1.122  by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
   1.123  
   1.124  lemma convex_bind_strict [simp]: "convex_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
   1.125 @@ -386,7 +386,7 @@
   1.126  unfolding convex_map_def by simp
   1.127  
   1.128  lemma convex_map_plus [simp]:
   1.129 -  "convex_map\<cdot>f\<cdot>(xs +\<natural> ys) = convex_map\<cdot>f\<cdot>xs +\<natural> convex_map\<cdot>f\<cdot>ys"
   1.130 +  "convex_map\<cdot>f\<cdot>(xs \<union>\<natural> ys) = convex_map\<cdot>f\<cdot>xs \<union>\<natural> convex_map\<cdot>f\<cdot>ys"
   1.131  unfolding convex_map_def by simp
   1.132  
   1.133  lemma convex_map_bottom [simp]: "convex_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<natural>"
   1.134 @@ -492,7 +492,7 @@
   1.135  unfolding convex_join_def by simp
   1.136  
   1.137  lemma convex_join_plus [simp]:
   1.138 -  "convex_join\<cdot>(xss +\<natural> yss) = convex_join\<cdot>xss +\<natural> convex_join\<cdot>yss"
   1.139 +  "convex_join\<cdot>(xss \<union>\<natural> yss) = convex_join\<cdot>xss \<union>\<natural> convex_join\<cdot>yss"
   1.140  unfolding convex_join_def by simp
   1.141  
   1.142  lemma convex_join_bottom [simp]: "convex_join\<cdot>\<bottom> = \<bottom>"
   1.143 @@ -536,7 +536,7 @@
   1.144  by (induct x rule: compact_basis.principal_induct, simp, simp)
   1.145  
   1.146  lemma convex_to_upper_plus [simp]:
   1.147 -  "convex_to_upper\<cdot>(xs +\<natural> ys) = convex_to_upper\<cdot>xs +\<sharp> convex_to_upper\<cdot>ys"
   1.148 +  "convex_to_upper\<cdot>(xs \<union>\<natural> ys) = convex_to_upper\<cdot>xs \<union>\<sharp> convex_to_upper\<cdot>ys"
   1.149  by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
   1.150  
   1.151  lemma convex_to_upper_bind [simp]:
   1.152 @@ -575,7 +575,7 @@
   1.153  by (induct x rule: compact_basis.principal_induct, simp, simp)
   1.154  
   1.155  lemma convex_to_lower_plus [simp]:
   1.156 -  "convex_to_lower\<cdot>(xs +\<natural> ys) = convex_to_lower\<cdot>xs +\<flat> convex_to_lower\<cdot>ys"
   1.157 +  "convex_to_lower\<cdot>(xs \<union>\<natural> ys) = convex_to_lower\<cdot>xs \<union>\<flat> convex_to_lower\<cdot>ys"
   1.158  by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
   1.159  
   1.160  lemma convex_to_lower_bind [simp]:
   1.161 @@ -604,7 +604,7 @@
   1.162  done
   1.163  
   1.164  lemmas convex_plus_below_plus_iff =
   1.165 -  convex_pd_below_iff [where xs="xs +\<natural> ys" and ys="zs +\<natural> ws", standard]
   1.166 +  convex_pd_below_iff [where xs="xs \<union>\<natural> ys" and ys="zs \<union>\<natural> ws", standard]
   1.167  
   1.168  lemmas convex_pd_below_simps =
   1.169    convex_unit_below_plus_iff
     2.1 --- a/src/HOL/HOLCF/LowerPD.thy	Thu Dec 23 12:20:09 2010 +0100
     2.2 +++ b/src/HOL/HOLCF/LowerPD.thy	Thu Dec 23 11:51:59 2010 -0800
     2.3 @@ -132,14 +132,14 @@
     2.4  
     2.5  abbreviation
     2.6    lower_add :: "'a lower_pd \<Rightarrow> 'a lower_pd \<Rightarrow> 'a lower_pd"
     2.7 -    (infixl "+\<flat>" 65) where
     2.8 -  "xs +\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
     2.9 +    (infixl "\<union>\<flat>" 65) where
    2.10 +  "xs \<union>\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
    2.11  
    2.12  syntax
    2.13    "_lower_pd" :: "args \<Rightarrow> 'a lower_pd" ("{_}\<flat>")
    2.14  
    2.15  translations
    2.16 -  "{x,xs}\<flat>" == "{x}\<flat> +\<flat> {xs}\<flat>"
    2.17 +  "{x,xs}\<flat>" == "{x}\<flat> \<union>\<flat> {xs}\<flat>"
    2.18    "{x}\<flat>" == "CONST lower_unit\<cdot>x"
    2.19  
    2.20  lemma lower_unit_Rep_compact_basis [simp]:
    2.21 @@ -148,23 +148,23 @@
    2.22  by (simp add: compact_basis.extension_principal PDUnit_lower_mono)
    2.23  
    2.24  lemma lower_plus_principal [simp]:
    2.25 -  "lower_principal t +\<flat> lower_principal u = lower_principal (PDPlus t u)"
    2.26 +  "lower_principal t \<union>\<flat> lower_principal u = lower_principal (PDPlus t u)"
    2.27  unfolding lower_plus_def
    2.28  by (simp add: lower_pd.extension_principal
    2.29      lower_pd.extension_mono PDPlus_lower_mono)
    2.30  
    2.31  interpretation lower_add: semilattice lower_add proof
    2.32    fix xs ys zs :: "'a lower_pd"
    2.33 -  show "(xs +\<flat> ys) +\<flat> zs = xs +\<flat> (ys +\<flat> zs)"
    2.34 +  show "(xs \<union>\<flat> ys) \<union>\<flat> zs = xs \<union>\<flat> (ys \<union>\<flat> zs)"
    2.35      apply (induct xs ys arbitrary: zs rule: lower_pd.principal_induct2, simp, simp)
    2.36      apply (rule_tac x=zs in lower_pd.principal_induct, simp)
    2.37      apply (simp add: PDPlus_assoc)
    2.38      done
    2.39 -  show "xs +\<flat> ys = ys +\<flat> xs"
    2.40 +  show "xs \<union>\<flat> ys = ys \<union>\<flat> xs"
    2.41      apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
    2.42      apply (simp add: PDPlus_commute)
    2.43      done
    2.44 -  show "xs +\<flat> xs = xs"
    2.45 +  show "xs \<union>\<flat> xs = xs"
    2.46      apply (induct xs rule: lower_pd.principal_induct, simp)
    2.47      apply (simp add: PDPlus_absorb)
    2.48      done
    2.49 @@ -184,21 +184,21 @@
    2.50  lemmas lower_plus_aci =
    2.51    lower_plus_ac lower_plus_absorb lower_plus_left_absorb
    2.52  
    2.53 -lemma lower_plus_below1: "xs \<sqsubseteq> xs +\<flat> ys"
    2.54 +lemma lower_plus_below1: "xs \<sqsubseteq> xs \<union>\<flat> ys"
    2.55  apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
    2.56  apply (simp add: PDPlus_lower_le)
    2.57  done
    2.58  
    2.59 -lemma lower_plus_below2: "ys \<sqsubseteq> xs +\<flat> ys"
    2.60 +lemma lower_plus_below2: "ys \<sqsubseteq> xs \<union>\<flat> ys"
    2.61  by (subst lower_plus_commute, rule lower_plus_below1)
    2.62  
    2.63 -lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs +\<flat> ys \<sqsubseteq> zs"
    2.64 +lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<union>\<flat> ys \<sqsubseteq> zs"
    2.65  apply (subst lower_plus_absorb [of zs, symmetric])
    2.66  apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
    2.67  done
    2.68  
    2.69  lemma lower_plus_below_iff [simp]:
    2.70 -  "xs +\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs"
    2.71 +  "xs \<union>\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs"
    2.72  apply safe
    2.73  apply (erule below_trans [OF lower_plus_below1])
    2.74  apply (erule below_trans [OF lower_plus_below2])
    2.75 @@ -206,7 +206,7 @@
    2.76  done
    2.77  
    2.78  lemma lower_unit_below_plus_iff [simp]:
    2.79 -  "{x}\<flat> \<sqsubseteq> ys +\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
    2.80 +  "{x}\<flat> \<sqsubseteq> ys \<union>\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
    2.81  apply (induct x rule: compact_basis.principal_induct, simp)
    2.82  apply (induct ys rule: lower_pd.principal_induct, simp)
    2.83  apply (induct zs rule: lower_pd.principal_induct, simp)
    2.84 @@ -235,19 +235,19 @@
    2.85  unfolding lower_unit_strict [symmetric] by (rule lower_unit_eq_iff)
    2.86  
    2.87  lemma lower_plus_bottom_iff [simp]:
    2.88 -  "xs +\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
    2.89 +  "xs \<union>\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
    2.90  apply safe
    2.91  apply (rule UU_I, erule subst, rule lower_plus_below1)
    2.92  apply (rule UU_I, erule subst, rule lower_plus_below2)
    2.93  apply (rule lower_plus_absorb)
    2.94  done
    2.95  
    2.96 -lemma lower_plus_strict1 [simp]: "\<bottom> +\<flat> ys = ys"
    2.97 +lemma lower_plus_strict1 [simp]: "\<bottom> \<union>\<flat> ys = ys"
    2.98  apply (rule below_antisym [OF _ lower_plus_below2])
    2.99  apply (simp add: lower_plus_least)
   2.100  done
   2.101  
   2.102 -lemma lower_plus_strict2 [simp]: "xs +\<flat> \<bottom> = xs"
   2.103 +lemma lower_plus_strict2 [simp]: "xs \<union>\<flat> \<bottom> = xs"
   2.104  apply (rule below_antisym [OF _ lower_plus_below1])
   2.105  apply (simp add: lower_plus_least)
   2.106  done
   2.107 @@ -262,7 +262,7 @@
   2.108  done
   2.109  
   2.110  lemma compact_lower_plus [simp]:
   2.111 -  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<flat> ys)"
   2.112 +  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs \<union>\<flat> ys)"
   2.113  by (auto dest!: lower_pd.compact_imp_principal)
   2.114  
   2.115  
   2.116 @@ -272,7 +272,7 @@
   2.117    assumes P: "adm P"
   2.118    assumes unit: "\<And>x. P {x}\<flat>"
   2.119    assumes insert:
   2.120 -    "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> +\<flat> ys)"
   2.121 +    "\<And>x ys. \<lbrakk>P {x}\<flat>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<flat> \<union>\<flat> ys)"
   2.122    shows "P (xs::'a lower_pd)"
   2.123  apply (induct xs rule: lower_pd.principal_induct, rule P)
   2.124  apply (induct_tac a rule: pd_basis_induct1)
   2.125 @@ -287,7 +287,7 @@
   2.126    [case_names adm lower_unit lower_plus, induct type: lower_pd]:
   2.127    assumes P: "adm P"
   2.128    assumes unit: "\<And>x. P {x}\<flat>"
   2.129 -  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<flat> ys)"
   2.130 +  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<flat> ys)"
   2.131    shows "P (xs::'a lower_pd)"
   2.132  apply (induct xs rule: lower_pd.principal_induct, rule P)
   2.133  apply (induct_tac a rule: pd_basis_induct)
   2.134 @@ -303,10 +303,10 @@
   2.135    "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b lower_pd" where
   2.136    "lower_bind_basis = fold_pd
   2.137      (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
   2.138 -    (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
   2.139 +    (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<flat> y\<cdot>f)"
   2.140  
   2.141  lemma ACI_lower_bind:
   2.142 -  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
   2.143 +  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<flat> y\<cdot>f)"
   2.144  apply unfold_locales
   2.145  apply (simp add: lower_plus_assoc)
   2.146  apply (simp add: lower_plus_commute)
   2.147 @@ -317,7 +317,7 @@
   2.148    "lower_bind_basis (PDUnit a) =
   2.149      (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   2.150    "lower_bind_basis (PDPlus t u) =
   2.151 -    (\<Lambda> f. lower_bind_basis t\<cdot>f +\<flat> lower_bind_basis u\<cdot>f)"
   2.152 +    (\<Lambda> f. lower_bind_basis t\<cdot>f \<union>\<flat> lower_bind_basis u\<cdot>f)"
   2.153  unfolding lower_bind_basis_def
   2.154  apply -
   2.155  apply (rule fold_pd_PDUnit [OF ACI_lower_bind])
   2.156 @@ -356,7 +356,7 @@
   2.157  by (induct x rule: compact_basis.principal_induct, simp, simp)
   2.158  
   2.159  lemma lower_bind_plus [simp]:
   2.160 -  "lower_bind\<cdot>(xs +\<flat> ys)\<cdot>f = lower_bind\<cdot>xs\<cdot>f +\<flat> lower_bind\<cdot>ys\<cdot>f"
   2.161 +  "lower_bind\<cdot>(xs \<union>\<flat> ys)\<cdot>f = lower_bind\<cdot>xs\<cdot>f \<union>\<flat> lower_bind\<cdot>ys\<cdot>f"
   2.162  by (induct xs ys rule: lower_pd.principal_induct2, simp, simp, simp)
   2.163  
   2.164  lemma lower_bind_strict [simp]: "lower_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
   2.165 @@ -378,7 +378,7 @@
   2.166  unfolding lower_map_def by simp
   2.167  
   2.168  lemma lower_map_plus [simp]:
   2.169 -  "lower_map\<cdot>f\<cdot>(xs +\<flat> ys) = lower_map\<cdot>f\<cdot>xs +\<flat> lower_map\<cdot>f\<cdot>ys"
   2.170 +  "lower_map\<cdot>f\<cdot>(xs \<union>\<flat> ys) = lower_map\<cdot>f\<cdot>xs \<union>\<flat> lower_map\<cdot>f\<cdot>ys"
   2.171  unfolding lower_map_def by simp
   2.172  
   2.173  lemma lower_map_bottom [simp]: "lower_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<flat>"
   2.174 @@ -484,7 +484,7 @@
   2.175  unfolding lower_join_def by simp
   2.176  
   2.177  lemma lower_join_plus [simp]:
   2.178 -  "lower_join\<cdot>(xss +\<flat> yss) = lower_join\<cdot>xss +\<flat> lower_join\<cdot>yss"
   2.179 +  "lower_join\<cdot>(xss \<union>\<flat> yss) = lower_join\<cdot>xss \<union>\<flat> lower_join\<cdot>yss"
   2.180  unfolding lower_join_def by simp
   2.181  
   2.182  lemma lower_join_bottom [simp]: "lower_join\<cdot>\<bottom> = \<bottom>"
     3.1 --- a/src/HOL/HOLCF/UpperPD.thy	Thu Dec 23 12:20:09 2010 +0100
     3.2 +++ b/src/HOL/HOLCF/UpperPD.thy	Thu Dec 23 11:51:59 2010 -0800
     3.3 @@ -130,14 +130,14 @@
     3.4  
     3.5  abbreviation
     3.6    upper_add :: "'a upper_pd \<Rightarrow> 'a upper_pd \<Rightarrow> 'a upper_pd"
     3.7 -    (infixl "+\<sharp>" 65) where
     3.8 -  "xs +\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys"
     3.9 +    (infixl "\<union>\<sharp>" 65) where
    3.10 +  "xs \<union>\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys"
    3.11  
    3.12  syntax
    3.13    "_upper_pd" :: "args \<Rightarrow> 'a upper_pd" ("{_}\<sharp>")
    3.14  
    3.15  translations
    3.16 -  "{x,xs}\<sharp>" == "{x}\<sharp> +\<sharp> {xs}\<sharp>"
    3.17 +  "{x,xs}\<sharp>" == "{x}\<sharp> \<union>\<sharp> {xs}\<sharp>"
    3.18    "{x}\<sharp>" == "CONST upper_unit\<cdot>x"
    3.19  
    3.20  lemma upper_unit_Rep_compact_basis [simp]:
    3.21 @@ -146,23 +146,23 @@
    3.22  by (simp add: compact_basis.extension_principal PDUnit_upper_mono)
    3.23  
    3.24  lemma upper_plus_principal [simp]:
    3.25 -  "upper_principal t +\<sharp> upper_principal u = upper_principal (PDPlus t u)"
    3.26 +  "upper_principal t \<union>\<sharp> upper_principal u = upper_principal (PDPlus t u)"
    3.27  unfolding upper_plus_def
    3.28  by (simp add: upper_pd.extension_principal
    3.29      upper_pd.extension_mono PDPlus_upper_mono)
    3.30  
    3.31  interpretation upper_add: semilattice upper_add proof
    3.32    fix xs ys zs :: "'a upper_pd"
    3.33 -  show "(xs +\<sharp> ys) +\<sharp> zs = xs +\<sharp> (ys +\<sharp> zs)"
    3.34 +  show "(xs \<union>\<sharp> ys) \<union>\<sharp> zs = xs \<union>\<sharp> (ys \<union>\<sharp> zs)"
    3.35      apply (induct xs ys arbitrary: zs rule: upper_pd.principal_induct2, simp, simp)
    3.36      apply (rule_tac x=zs in upper_pd.principal_induct, simp)
    3.37      apply (simp add: PDPlus_assoc)
    3.38      done
    3.39 -  show "xs +\<sharp> ys = ys +\<sharp> xs"
    3.40 +  show "xs \<union>\<sharp> ys = ys \<union>\<sharp> xs"
    3.41      apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
    3.42      apply (simp add: PDPlus_commute)
    3.43      done
    3.44 -  show "xs +\<sharp> xs = xs"
    3.45 +  show "xs \<union>\<sharp> xs = xs"
    3.46      apply (induct xs rule: upper_pd.principal_induct, simp)
    3.47      apply (simp add: PDPlus_absorb)
    3.48      done
    3.49 @@ -182,21 +182,21 @@
    3.50  lemmas upper_plus_aci =
    3.51    upper_plus_ac upper_plus_absorb upper_plus_left_absorb
    3.52  
    3.53 -lemma upper_plus_below1: "xs +\<sharp> ys \<sqsubseteq> xs"
    3.54 +lemma upper_plus_below1: "xs \<union>\<sharp> ys \<sqsubseteq> xs"
    3.55  apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
    3.56  apply (simp add: PDPlus_upper_le)
    3.57  done
    3.58  
    3.59 -lemma upper_plus_below2: "xs +\<sharp> ys \<sqsubseteq> ys"
    3.60 +lemma upper_plus_below2: "xs \<union>\<sharp> ys \<sqsubseteq> ys"
    3.61  by (subst upper_plus_commute, rule upper_plus_below1)
    3.62  
    3.63 -lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> ys +\<sharp> zs"
    3.64 +lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> ys \<union>\<sharp> zs"
    3.65  apply (subst upper_plus_absorb [of xs, symmetric])
    3.66  apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
    3.67  done
    3.68  
    3.69  lemma upper_below_plus_iff [simp]:
    3.70 -  "xs \<sqsubseteq> ys +\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs"
    3.71 +  "xs \<sqsubseteq> ys \<union>\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs"
    3.72  apply safe
    3.73  apply (erule below_trans [OF _ upper_plus_below1])
    3.74  apply (erule below_trans [OF _ upper_plus_below2])
    3.75 @@ -204,7 +204,7 @@
    3.76  done
    3.77  
    3.78  lemma upper_plus_below_unit_iff [simp]:
    3.79 -  "xs +\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>"
    3.80 +  "xs \<union>\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>"
    3.81  apply (induct xs rule: upper_pd.principal_induct, simp)
    3.82  apply (induct ys rule: upper_pd.principal_induct, simp)
    3.83  apply (induct z rule: compact_basis.principal_induct, simp)
    3.84 @@ -229,17 +229,17 @@
    3.85  using upper_unit_Rep_compact_basis [of compact_bot]
    3.86  by (simp add: inst_upper_pd_pcpo)
    3.87  
    3.88 -lemma upper_plus_strict1 [simp]: "\<bottom> +\<sharp> ys = \<bottom>"
    3.89 +lemma upper_plus_strict1 [simp]: "\<bottom> \<union>\<sharp> ys = \<bottom>"
    3.90  by (rule UU_I, rule upper_plus_below1)
    3.91  
    3.92 -lemma upper_plus_strict2 [simp]: "xs +\<sharp> \<bottom> = \<bottom>"
    3.93 +lemma upper_plus_strict2 [simp]: "xs \<union>\<sharp> \<bottom> = \<bottom>"
    3.94  by (rule UU_I, rule upper_plus_below2)
    3.95  
    3.96  lemma upper_unit_bottom_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
    3.97  unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
    3.98  
    3.99  lemma upper_plus_bottom_iff [simp]:
   3.100 -  "xs +\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>"
   3.101 +  "xs \<union>\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>"
   3.102  apply (rule iffI)
   3.103  apply (erule rev_mp)
   3.104  apply (rule upper_pd.principal_induct2 [where x=xs and y=ys], simp, simp)
   3.105 @@ -258,7 +258,7 @@
   3.106  done
   3.107  
   3.108  lemma compact_upper_plus [simp]:
   3.109 -  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs +\<sharp> ys)"
   3.110 +  "\<lbrakk>compact xs; compact ys\<rbrakk> \<Longrightarrow> compact (xs \<union>\<sharp> ys)"
   3.111  by (auto dest!: upper_pd.compact_imp_principal)
   3.112  
   3.113  
   3.114 @@ -267,7 +267,7 @@
   3.115  lemma upper_pd_induct1:
   3.116    assumes P: "adm P"
   3.117    assumes unit: "\<And>x. P {x}\<sharp>"
   3.118 -  assumes insert: "\<And>x ys. \<lbrakk>P {x}\<sharp>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<sharp> +\<sharp> ys)"
   3.119 +  assumes insert: "\<And>x ys. \<lbrakk>P {x}\<sharp>; P ys\<rbrakk> \<Longrightarrow> P ({x}\<sharp> \<union>\<sharp> ys)"
   3.120    shows "P (xs::'a upper_pd)"
   3.121  apply (induct xs rule: upper_pd.principal_induct, rule P)
   3.122  apply (induct_tac a rule: pd_basis_induct1)
   3.123 @@ -282,7 +282,7 @@
   3.124    [case_names adm upper_unit upper_plus, induct type: upper_pd]:
   3.125    assumes P: "adm P"
   3.126    assumes unit: "\<And>x. P {x}\<sharp>"
   3.127 -  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs +\<sharp> ys)"
   3.128 +  assumes plus: "\<And>xs ys. \<lbrakk>P xs; P ys\<rbrakk> \<Longrightarrow> P (xs \<union>\<sharp> ys)"
   3.129    shows "P (xs::'a upper_pd)"
   3.130  apply (induct xs rule: upper_pd.principal_induct, rule P)
   3.131  apply (induct_tac a rule: pd_basis_induct)
   3.132 @@ -298,10 +298,10 @@
   3.133    "'a pd_basis \<Rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where
   3.134    "upper_bind_basis = fold_pd
   3.135      (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a))
   3.136 -    (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
   3.137 +    (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<sharp> y\<cdot>f)"
   3.138  
   3.139  lemma ACI_upper_bind:
   3.140 -  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
   3.141 +  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<sharp> y\<cdot>f)"
   3.142  apply unfold_locales
   3.143  apply (simp add: upper_plus_assoc)
   3.144  apply (simp add: upper_plus_commute)
   3.145 @@ -312,7 +312,7 @@
   3.146    "upper_bind_basis (PDUnit a) =
   3.147      (\<Lambda> f. f\<cdot>(Rep_compact_basis a))"
   3.148    "upper_bind_basis (PDPlus t u) =
   3.149 -    (\<Lambda> f. upper_bind_basis t\<cdot>f +\<sharp> upper_bind_basis u\<cdot>f)"
   3.150 +    (\<Lambda> f. upper_bind_basis t\<cdot>f \<union>\<sharp> upper_bind_basis u\<cdot>f)"
   3.151  unfolding upper_bind_basis_def
   3.152  apply -
   3.153  apply (rule fold_pd_PDUnit [OF ACI_upper_bind])
   3.154 @@ -351,7 +351,7 @@
   3.155  by (induct x rule: compact_basis.principal_induct, simp, simp)
   3.156  
   3.157  lemma upper_bind_plus [simp]:
   3.158 -  "upper_bind\<cdot>(xs +\<sharp> ys)\<cdot>f = upper_bind\<cdot>xs\<cdot>f +\<sharp> upper_bind\<cdot>ys\<cdot>f"
   3.159 +  "upper_bind\<cdot>(xs \<union>\<sharp> ys)\<cdot>f = upper_bind\<cdot>xs\<cdot>f \<union>\<sharp> upper_bind\<cdot>ys\<cdot>f"
   3.160  by (induct xs ys rule: upper_pd.principal_induct2, simp, simp, simp)
   3.161  
   3.162  lemma upper_bind_strict [simp]: "upper_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
   3.163 @@ -373,7 +373,7 @@
   3.164  unfolding upper_map_def by simp
   3.165  
   3.166  lemma upper_map_plus [simp]:
   3.167 -  "upper_map\<cdot>f\<cdot>(xs +\<sharp> ys) = upper_map\<cdot>f\<cdot>xs +\<sharp> upper_map\<cdot>f\<cdot>ys"
   3.168 +  "upper_map\<cdot>f\<cdot>(xs \<union>\<sharp> ys) = upper_map\<cdot>f\<cdot>xs \<union>\<sharp> upper_map\<cdot>f\<cdot>ys"
   3.169  unfolding upper_map_def by simp
   3.170  
   3.171  lemma upper_map_bottom [simp]: "upper_map\<cdot>f\<cdot>\<bottom> = {f\<cdot>\<bottom>}\<sharp>"
   3.172 @@ -479,7 +479,7 @@
   3.173  unfolding upper_join_def by simp
   3.174  
   3.175  lemma upper_join_plus [simp]:
   3.176 -  "upper_join\<cdot>(xss +\<sharp> yss) = upper_join\<cdot>xss +\<sharp> upper_join\<cdot>yss"
   3.177 +  "upper_join\<cdot>(xss \<union>\<sharp> yss) = upper_join\<cdot>xss \<union>\<sharp> upper_join\<cdot>yss"
   3.178  unfolding upper_join_def by simp
   3.179  
   3.180  lemma upper_join_bottom [simp]: "upper_join\<cdot>\<bottom> = \<bottom>"
     4.1 --- a/src/HOL/HOLCF/ex/Powerdomain_ex.thy	Thu Dec 23 12:20:09 2010 +0100
     4.2 +++ b/src/HOL/HOLCF/ex/Powerdomain_ex.thy	Thu Dec 23 11:51:59 2010 -0800
     4.3 @@ -62,7 +62,7 @@
     4.4    pick :: "'a tree \<rightarrow> 'a convex_pd"
     4.5  where
     4.6    pick_Leaf: "pick\<cdot>(Leaf\<cdot>a) = {a}\<natural>"
     4.7 -| pick_Node: "pick\<cdot>(Node\<cdot>l\<cdot>r) = pick\<cdot>l +\<natural> pick\<cdot>r"
     4.8 +| pick_Node: "pick\<cdot>(Node\<cdot>l\<cdot>r) = pick\<cdot>l \<union>\<natural> pick\<cdot>r"
     4.9  
    4.10  lemma pick_strict [simp]: "pick\<cdot>\<bottom> = \<bottom>"
    4.11  by fixrec_simp