--- 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
--- 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>"
--- 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>"
--- 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