--- a/src/HOL/Algebra/Ideal.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Algebra/Ideal.thy Mon Dec 28 17:43:30 2015 +0100
@@ -47,7 +47,7 @@
subsubsection (in ring) \<open>Ideals Generated by a Subset of @{term "carrier R"}\<close>
definition genideal :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("Idl\<index> _" [80] 79)
- where "genideal R S = Inter {I. ideal I R \<and> S \<subseteq> I}"
+ where "genideal R S = \<Inter>{I. ideal I R \<and> S \<subseteq> I}"
subsubsection \<open>Principal Ideals\<close>
@@ -218,7 +218,7 @@
lemma (in ring) i_Intersect:
assumes Sideals: "\<And>I. I \<in> S \<Longrightarrow> ideal I R"
and notempty: "S \<noteq> {}"
- shows "ideal (Inter S) R"
+ shows "ideal (\<Inter>S) R"
apply (unfold_locales)
apply (simp_all add: Inter_eq)
apply rule unfolding mem_Collect_eq defer 1
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Mon Dec 28 17:43:30 2015 +0100
@@ -785,9 +785,9 @@
lemma Card_order_lists: "Card_order r \<Longrightarrow> r \<le>o |lists(Field r) |"
using card_of_lists card_of_Field_ordIso ordIso_ordLeq_trans ordIso_symmetric by blast
-lemma Union_set_lists:
-"Union(set ` (lists A)) = A"
-unfolding lists_def2 proof(auto)
+lemma Union_set_lists: "\<Union>(set ` (lists A)) = A"
+ unfolding lists_def2
+proof(auto)
fix a assume "a \<in> A"
hence "set [a] \<le> A \<and> a \<in> set [a]" by auto
thus "\<exists>l. set l \<le> A \<and> a \<in> set l" by blast
--- a/src/HOL/Cardinals/Wellorder_Relation.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy Mon Dec 28 17:43:30 2015 +0100
@@ -441,15 +441,15 @@
unfolding ofilter_def by blast
lemma ofilter_Inter:
-"\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> ofilter A\<rbrakk> \<Longrightarrow> ofilter (Inter S)"
+"\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> ofilter A\<rbrakk> \<Longrightarrow> ofilter (\<Inter>S)"
unfolding ofilter_def by blast
lemma ofilter_Union:
-"(\<And> A. A \<in> S \<Longrightarrow> ofilter A) \<Longrightarrow> ofilter (Union S)"
+"(\<And> A. A \<in> S \<Longrightarrow> ofilter A) \<Longrightarrow> ofilter (\<Union>S)"
unfolding ofilter_def by blast
lemma ofilter_under_Union:
-"ofilter A \<Longrightarrow> A = Union {under a| a. a \<in> A}"
+"ofilter A \<Longrightarrow> A = \<Union>{under a| a. a \<in> A}"
using ofilter_under_UNION[of A]
by(unfold Union_eq, auto)
--- a/src/HOL/Complete_Lattices.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Complete_Lattices.thy Mon Dec 28 17:43:30 2015 +0100
@@ -901,12 +901,9 @@
subsubsection \<open>Inter\<close>
-abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
- "Inter S \<equiv> \<Sqinter>S"
+abbreviation Inter :: "'a set set \<Rightarrow> 'a set" ("\<Inter>_" [900] 900)
+ where "\<Inter>S \<equiv> \<Sqinter>S"
-notation (xsymbols)
- Inter ("\<Inter>_" [900] 900)
-
lemma Inter_eq:
"\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
proof (rule set_eqI)
@@ -944,7 +941,7 @@
"(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> B) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Inter>A \<subseteq> B"
by (fact Inf_less_eq)
-lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> Inter A"
+lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> \<Inter>A"
by (fact Inf_greatest)
lemma Inter_empty: "\<Inter>{} = UNIV"
@@ -1080,11 +1077,8 @@
subsubsection \<open>Union\<close>
-abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
- "Union S \<equiv> \<Squnion>S"
-
-notation (xsymbols)
- Union ("\<Union>_" [900] 900)
+abbreviation Union :: "'a set set \<Rightarrow> 'a set" ("\<Union>_" [900] 900)
+ where "\<Union>S \<equiv> \<Squnion>S"
lemma Union_eq:
"\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
--- a/src/HOL/Equiv_Relations.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Equiv_Relations.thy Mon Dec 28 17:43:30 2015 +0100
@@ -108,7 +108,7 @@
"X \<in> A//r ==> (!!x. X = r``{x} ==> x \<in> A ==> P) ==> P"
by (unfold quotient_def) blast
-lemma Union_quotient: "equiv A r ==> Union (A//r) = A"
+lemma Union_quotient: "equiv A r ==> \<Union>(A//r) = A"
by (unfold equiv_def refl_on_def quotient_def) blast
lemma quotient_disj:
--- a/src/HOL/Groups_Big.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Groups_Big.thy Mon Dec 28 17:43:30 2015 +0100
@@ -172,7 +172,7 @@
lemma Union_disjoint:
assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
- shows "F g (Union C) = (F \<circ> F) g C"
+ shows "F g (\<Union>C) = (F \<circ> F) g C"
proof cases
assume "finite C"
from UNION_disjoint [OF this assms]
@@ -994,7 +994,7 @@
lemma card_Union_disjoint:
"finite C ==> (ALL A:C. finite A) ==>
(ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
- ==> card (Union C) = setsum card C"
+ ==> card (\<Union>C) = setsum card C"
apply (frule card_UN_disjoint [of C id])
apply simp_all
done
--- a/src/HOL/Inductive.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Inductive.thy Mon Dec 28 17:43:30 2015 +0100
@@ -87,16 +87,16 @@
lemma lfp_induct_set:
assumes lfp: "a: lfp(f)"
- and mono: "mono(f)"
- and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
+ and mono: "mono(f)"
+ and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
shows "P(a)"
by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
(auto simp: intro: indhyp)
lemma lfp_ordinal_induct_set:
assumes mono: "mono f"
- and P_f: "!!S. P S ==> P(f S)"
- and P_Union: "!!M. !S:M. P S ==> P(Union M)"
+ and P_f: "!!S. P S ==> P(f S)"
+ and P_Union: "!!M. !S:M. P S ==> P (\<Union>M)"
shows "P(lfp f)"
using assms by (rule lfp_ordinal_induct)
--- a/src/HOL/Library/Countable_Set_Type.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy Mon Dec 28 17:43:30 2015 +0100
@@ -118,7 +118,7 @@
is "UNION" parametric UNION_transfer by simp
definition cUnion :: "'a cset cset \<Rightarrow> 'a cset" where "cUnion A = cUNION A id"
-lemma Union_conv_UNION: "Union A = UNION A id"
+lemma Union_conv_UNION: "\<Union>A = UNION A id"
by auto
lemma cUnion_transfer [transfer_rule]:
--- a/src/HOL/Library/FSet.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Library/FSet.thy Mon Dec 28 17:43:30 2015 +0100
@@ -79,7 +79,7 @@
lemma right_total_Inf_fset_transfer:
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
shows "(rel_set (rel_set A) ===> rel_set A)
- (\<lambda>S. if finite (Inter S \<inter> Collect (Domainp A)) then Inter S \<inter> Collect (Domainp A) else {})
+ (\<lambda>S. if finite (\<Inter>S \<inter> Collect (Domainp A)) then \<Inter>S \<inter> Collect (Domainp A) else {})
(\<lambda>S. if finite (Inf S) then Inf S else {})"
by transfer_prover
--- a/src/HOL/Library/Old_Datatype.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Library/Old_Datatype.thy Mon Dec 28 17:43:30 2015 +0100
@@ -76,7 +76,7 @@
In1_def: "In1(M) == Scons (Numb 1) M"
(*Function spaces*)
- Lim_def: "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}"
+ Lim_def: "Lim f == \<Union>{z. ? x. z = Push_Node (Inl x) ` (f x)}"
(*the set of nodes with depth less than k*)
ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"
--- a/src/HOL/Lifting_Set.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Lifting_Set.thy Mon Dec 28 17:43:30 2015 +0100
@@ -237,7 +237,7 @@
lemma right_total_Inter_transfer [transfer_rule]:
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
- shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>S. Inter S \<inter> Collect (Domainp A)) Inter"
+ shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>S. \<Inter>S \<inter> Collect (Domainp A)) Inter"
unfolding Inter_eq[abs_def]
by (subst Collect_conj_eq[symmetric]) transfer_prover
--- a/src/HOL/MicroJava/BV/BVExample.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy Mon Dec 28 17:43:30 2015 +0100
@@ -424,7 +424,7 @@
apply (case_tac "\<not> stable r step ss p")
apply simp_all
done
- also have "\<And>f. (UN p:{..<size ss}. f p) = Union (set (map f [0..<size ss]))" by auto
+ also have "\<And>f. (UN p:{..<size ss}. f p) = \<Union>(set (map f [0..<size ss]))" by auto
also note Sup_set_fold also note fold_map
also have "op \<union> \<circ> (\<lambda>p. if \<not> stable r step ss p then {p} else {}) =
(\<lambda>p A. if \<not>stable r step ss p then insert p A else A)"
--- a/src/HOL/MicroJava/BV/JVMType.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy Mon Dec 28 17:43:30 2015 +0100
@@ -62,7 +62,7 @@
lemma JVM_states_unfold:
- "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) \<times>
+ "states S maxs maxr == err(opt((\<Union>{list n (types S) |n. n <= maxs}) \<times>
list maxr (err(types S))))"
apply (unfold states_def sl_def Opt.esl_def Err.sl_def
stk_esl_def reg_sl_def Product.esl_def
--- a/src/HOL/MicroJava/DFA/Err.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/MicroJava/DFA/Err.thy Mon Dec 28 17:43:30 2015 +0100
@@ -283,7 +283,7 @@
done
qed
-subsection \<open>semilat (err(Union AS))\<close>
+subsection \<open>semilat (err (Union AS))\<close>
(* FIXME? *)
lemma all_bex_swap_lemma [iff]:
@@ -293,7 +293,7 @@
lemma closed_err_Union_lift2I:
"\<lbrakk> !A:AS. closed (err A) (lift2 f); AS ~= {};
!A:AS.!B:AS. A~=B \<longrightarrow> (!a:A.!b:B. a +_f b = Err) \<rbrakk>
- \<Longrightarrow> closed (err(Union AS)) (lift2 f)"
+ \<Longrightarrow> closed (err (\<Union>AS)) (lift2 f)"
apply (unfold closed_def err_def)
apply simp
apply clarify
@@ -309,7 +309,7 @@
lemma err_semilat_UnionI:
"\<lbrakk> !A:AS. err_semilat(A, r, f); AS ~= {};
!A:AS.!B:AS. A~=B \<longrightarrow> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) \<rbrakk>
- \<Longrightarrow> err_semilat(Union AS, r, f)"
+ \<Longrightarrow> err_semilat (\<Union>AS, r, f)"
apply (unfold semilat_def sl_def)
apply (simp add: closed_err_Union_lift2I)
apply (rule conjI)
--- a/src/HOL/MicroJava/DFA/Listn.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/MicroJava/DFA/Listn.thy Mon Dec 28 17:43:30 2015 +0100
@@ -44,7 +44,7 @@
"sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err"
definition upto_esl :: "nat \<Rightarrow> 'a esl \<Rightarrow> 'a list esl" where
-"upto_esl m == %(A,r,f). (Union{list n A |n. n <= m}, le r, sup f)"
+"upto_esl m == %(A,r,f). (\<Union>{list n A |n. n <= m}, le r, sup f)"
lemmas [simp] = set_update_subsetI
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Dec 28 17:43:30 2015 +0100
@@ -74,7 +74,7 @@
finally show ?thesis .
qed
-lemma subspace_Inter: "\<forall>s \<in> f. subspace s \<Longrightarrow> subspace (Inter f)"
+lemma subspace_Inter: "\<forall>s \<in> f. subspace s \<Longrightarrow> subspace (\<Inter>f)"
unfolding subspace_def by auto
lemma span_eq[simp]: "span s = s \<longleftrightarrow> subspace s"
@@ -1110,7 +1110,7 @@
lemma cone_0: "cone {0}"
unfolding cone_def by auto
-lemma cone_Union[intro]: "(\<forall>s\<in>f. cone s) \<longrightarrow> cone (Union f)"
+lemma cone_Union[intro]: "(\<forall>s\<in>f. cone s) \<longrightarrow> cone (\<Union>f)"
unfolding cone_def by blast
lemma cone_iff:
@@ -8075,7 +8075,7 @@
assume z: "z \<in> \<Inter>{rel_interior S |S. S \<in> I}"
{
fix x
- assume x: "x \<in> Inter I"
+ assume x: "x \<in> \<Inter>I"
{
fix S
assume S: "S \<in> I"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Dec 28 17:43:30 2015 +0100
@@ -203,13 +203,13 @@
lemma open_countable_basis_ex:
assumes "open X"
- shows "\<exists>B' \<subseteq> B. X = Union B'"
+ shows "\<exists>B' \<subseteq> B. X = \<Union>B'"
using assms countable_basis is_basis
unfolding topological_basis_def by blast
lemma open_countable_basisE:
assumes "open X"
- obtains B' where "B' \<subseteq> B" "X = Union B'"
+ obtains B' where "B' \<subseteq> B" "X = \<Union>B'"
using assms open_countable_basis_ex
by (atomize_elim) simp
@@ -1885,7 +1885,7 @@
lemma connected_component_of_subset: "\<lbrakk>connected_component s x y; s \<subseteq> t\<rbrakk> \<Longrightarrow> connected_component t x y"
by (auto simp: connected_component_def)
-lemma connected_component_Union: "connected_component_set s x = Union {t. connected t \<and> x \<in> t \<and> t \<subseteq> s}"
+lemma connected_component_Union: "connected_component_set s x = \<Union>{t. connected t \<and> x \<in> t \<and> t \<subseteq> s}"
by (auto simp: connected_component_def)
lemma connected_connected_component [iff]: "connected (connected_component_set s x)"
@@ -2024,7 +2024,7 @@
by (metis (no_types, hide_lams) connected_component_eq_eq connected_component_in connected_component_maximal subsetD mem_Collect_eq)
-lemma Union_connected_component: "Union (connected_component_set s ` s) = s"
+lemma Union_connected_component: "\<Union>(connected_component_set s ` s) = s"
apply (rule subset_antisym)
apply (simp add: SUP_least connected_component_subset)
using connected_component_refl_eq
@@ -2033,7 +2033,7 @@
lemma complement_connected_component_unions:
"s - connected_component_set s x =
- Union (connected_component_set s ` s - {connected_component_set s x})"
+ \<Union>(connected_component_set s ` s - {connected_component_set s x})"
apply (subst Union_connected_component [symmetric], auto)
apply (metis connected_component_eq_eq connected_component_in)
by (metis connected_component_eq mem_Collect_eq)
@@ -2053,7 +2053,7 @@
lemma components_iff: "s \<in> components u \<longleftrightarrow> (\<exists>x. x \<in> u \<and> s = connected_component_set u x)"
by (auto simp: components_def)
-lemma Union_components: "u = Union (components u)"
+lemma Union_components: "u = \<Union>(components u)"
apply (rule subset_antisym)
apply (metis Union_connected_component components_def set_eq_subset)
using Union_connected_component components_def by fastforce
@@ -2142,7 +2142,7 @@
apply (auto simp: components_iff)
by (metis connected_component_eq_empty connected_component_intermediate_subset)
-lemma in_components_unions_complement: "c \<in> components s \<Longrightarrow> s - c = Union(components s - {c})"
+lemma in_components_unions_complement: "c \<in> components s \<Longrightarrow> s - c = \<Union>(components s - {c})"
by (metis complement_connected_component_unions components_def components_iff)
lemma connected_intermediate_closure:
--- a/src/HOL/Number_Theory/MiscAlgebra.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy Mon Dec 28 17:43:30 2015 +0100
@@ -257,7 +257,7 @@
lemma (in comm_monoid) finprod_Union_disjoint:
"[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G));
(ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
- ==> finprod G f (Union C) = finprod G (finprod G f) C"
+ ==> finprod G f (\<Union>C) = finprod G (finprod G f) C"
apply (frule finprod_UN_disjoint [of C id f])
apply (auto simp add: SUP_def)
done
--- a/src/HOL/Old_Number_Theory/Euler.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Old_Number_Theory/Euler.thy Mon Dec 28 17:43:30 2015 +0100
@@ -49,7 +49,7 @@
by (auto simp add: MultInvPair_prop1b)
lemma MultInvPair_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>
- Union ( SetS a p) = SRStar p"
+ \<Union>(SetS a p) = SRStar p"
apply (auto simp add: SetS_def MultInvPair_def StandardRes_SRStar_prop4
SRStar_mult_prop2)
apply (frule StandardRes_SRStar_prop3)
@@ -105,7 +105,7 @@
apply (rule MultInvPair_card_two, auto)
done
-lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))"
+lemma Union_SetS_finite: "2 < p ==> finite (\<Union>(SetS a p))"
by (auto simp add: SetS_finite SetS_elems_finite)
lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set);
@@ -118,7 +118,7 @@
proof -
have "(p - 1) = 2 * int(card(SetS a p))"
proof -
- have "p - 1 = int(card(Union (SetS a p)))"
+ have "p - 1 = int(card(\<Union>(SetS a p)))"
by (auto simp add: assms MultInvPair_prop2 SRStar_card)
also have "... = int (setsum card (SetS a p))"
by (auto simp add: assms SetS_finite SetS_elems_finite
@@ -177,9 +177,9 @@
lemma Union_SetS_setprod_prop1:
assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and
"~(QuadRes p a)"
- shows "[\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
+ shows "[\<Prod>(\<Union>(SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
proof -
- from assms have "[\<Prod>(Union (SetS a p)) = setprod (setprod (%x. x)) (SetS a p)] (mod p)"
+ from assms have "[\<Prod>(\<Union>(SetS a p)) = setprod (setprod (%x. x)) (SetS a p)] (mod p)"
by (auto simp add: SetS_finite SetS_elems_finite
MultInvPair_prop1c setprod.Union_disjoint)
also have "[setprod (setprod (%x. x)) (SetS a p) =
@@ -199,9 +199,9 @@
lemma Union_SetS_setprod_prop2:
assumes "zprime p" and "2 < p" and "~([a = 0](mod p))"
- shows "\<Prod>(Union (SetS a p)) = zfact (p - 1)"
+ shows "\<Prod>(\<Union>(SetS a p)) = zfact (p - 1)"
proof -
- from assms have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)"
+ from assms have "\<Prod>(\<Union>(SetS a p)) = \<Prod>(SRStar p)"
by (auto simp add: MultInvPair_prop2)
also have "... = \<Prod>({1} \<union> (d22set (p - 1)))"
by (auto simp add: assms SRStar_d22set_prop)
--- a/src/HOL/Probability/Sigma_Algebra.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Mon Dec 28 17:43:30 2015 +0100
@@ -75,7 +75,7 @@
assumes Un [intro]: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<union> b \<in> M"
lemma (in ring_of_sets) finite_Union [intro]:
- "finite X \<Longrightarrow> X \<subseteq> M \<Longrightarrow> Union X \<in> M"
+ "finite X \<Longrightarrow> X \<subseteq> M \<Longrightarrow> \<Union>X \<in> M"
by (induct set: finite) (auto simp add: Un)
lemma (in ring_of_sets) finite_UN[intro]:
@@ -261,7 +261,7 @@
qed
lemma (in sigma_algebra) countable_Union [intro]:
- assumes "countable X" "X \<subseteq> M" shows "Union X \<in> M"
+ assumes "countable X" "X \<subseteq> M" shows "\<Union>X \<in> M"
proof cases
assume "X \<noteq> {}"
hence "\<Union>X = (\<Union>n. from_nat_into X n)"
--- a/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Mon Dec 28 17:43:30 2015 +0100
@@ -105,7 +105,7 @@
primrec used :: "event list => msg set"
where
- used_Nil: "used [] = Union (parts ` initState ` agents)"
+ used_Nil: "used [] = \<Union>(parts ` initState ` agents)"
| used_Cons: "used (ev # evs) =
(case ev of
Says A B X => parts {X} \<union> used evs
@@ -172,13 +172,13 @@
lemma [code]:
"analz H = (let
- H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
+ H' = H \<union> (\<Union>((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => if Key (invKey K) : H then {X} else {} | _ => {}) ` H))
in if H' = H then H else analz H')"
sorry
lemma [code]:
"parts H = (let
- H' = H \<union> (Union ((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
+ H' = H \<union> (\<Union>((%m. case m of {|X, Y|} => {X, Y} | Crypt K X => {X} | _ => {}) ` H))
in if H' = H then H else parts H')"
sorry
--- a/src/HOL/UNITY/ELT.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/UNITY/ELT.thy Mon Dec 28 17:43:30 2015 +0100
@@ -133,7 +133,7 @@
(*The Union introduction rule as we should have liked to state it*)
lemma leadsETo_Union:
- "(!!A. A : S ==> F : A leadsTo[CC] B) ==> F : (Union S) leadsTo[CC] B"
+ "(!!A. A : S ==> F : A leadsTo[CC] B) ==> F : (\<Union>S) leadsTo[CC] B"
apply (unfold leadsETo_def)
apply (blast intro: elt.Union)
done
@@ -151,7 +151,7 @@
!!A B. [| F : A ensures B; A-B : insert {} CC |] ==> P A B;
!!A B C. [| F : A leadsTo[CC] B; P A B; F : B leadsTo[CC] C; P B C |]
==> P A C;
- !!B S. ALL A:S. F : A leadsTo[CC] B & P A B ==> P (Union S) B
+ !!B S. ALL A:S. F : A leadsTo[CC] B & P A B ==> P (\<Union>S) B
|] ==> P za zb"
apply (unfold leadsETo_def)
apply (drule CollectD)
@@ -176,7 +176,7 @@
lemma leadsETo_Union_Int:
"(!!A. A : S ==> F : (A Int C) leadsTo[CC] B)
- ==> F : (Union S Int C) leadsTo[CC] B"
+ ==> F : (\<Union>S Int C) leadsTo[CC] B"
apply (unfold leadsETo_def)
apply (simp only: Int_Union_Union)
apply (blast intro: elt.Union)
@@ -223,7 +223,7 @@
by (blast intro: leadsETo_UN leadsETo_weaken_L)
lemma leadsETo_Union_distrib:
- "F : (Union S) leadsTo[CC] B = (ALL A : S. F : A leadsTo[CC] B)"
+ "F : (\<Union>S) leadsTo[CC] B = (ALL A : S. F : A leadsTo[CC] B)"
by (blast intro: leadsETo_Union leadsETo_weaken_L)
lemma leadsETo_weaken:
@@ -388,7 +388,7 @@
done
lemma LeadsETo_Union:
- "(!!A. A : S ==> F : A LeadsTo[CC] B) ==> F : (Union S) LeadsTo[CC] B"
+ "(!!A. A : S ==> F : A LeadsTo[CC] B) ==> F : (\<Union>S) LeadsTo[CC] B"
apply (simp add: LeadsETo_def)
apply (subst Int_Union)
apply (blast intro: leadsETo_UN)
--- a/src/HOL/UNITY/Extend.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/UNITY/Extend.thy Mon Dec 28 17:43:30 2015 +0100
@@ -255,7 +255,7 @@
lemma extend_set_Diff_distrib: "extend_set h (A - B) = extend_set h A - extend_set h B"
by auto
-lemma extend_set_Union: "extend_set h (Union A) = (\<Union>X \<in> A. extend_set h X)"
+lemma extend_set_Union: "extend_set h (\<Union>A) = (\<Union>X \<in> A. extend_set h X)"
by blast
lemma extend_set_subset_Compl_eq: "(extend_set h A \<subseteq> - extend_set h B) = (A \<subseteq> - B)"
@@ -361,7 +361,7 @@
lemma (in -) project_set_UNIV [simp]: "project_set h UNIV = UNIV"
by auto
-lemma (in -) project_set_Union: "project_set h (Union A) = (\<Union>X \<in> A. project_set h X)"
+lemma (in -) project_set_Union: "project_set h (\<Union>A) = (\<Union>X \<in> A. project_set h X)"
by blast
@@ -561,7 +561,7 @@
lemma slice_iff [iff]: "(x \<in> slice C y) = (h(x,y) \<in> C)"
by (simp add: slice_def)
-lemma slice_Union: "slice (Union S) y = (\<Union>x \<in> S. slice x y)"
+lemma slice_Union: "slice (\<Union>S) y = (\<Union>x \<in> S. slice x y)"
by auto
lemma slice_extend_set: "slice (extend_set h A) y = A"
--- a/src/HOL/UNITY/FP.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/UNITY/FP.thy Mon Dec 28 17:43:30 2015 +0100
@@ -10,7 +10,7 @@
theory FP imports UNITY begin
definition FP_Orig :: "'a program => 'a set" where
- "FP_Orig F == Union{A. ALL B. F : stable (A Int B)}"
+ "FP_Orig F == \<Union>{A. ALL B. F : stable (A Int B)}"
definition FP :: "'a program => 'a set" where
"FP F == {s. F : stable {s}}"
--- a/src/HOL/UNITY/Guar.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/UNITY/Guar.thy Mon Dec 28 17:43:30 2015 +0100
@@ -45,11 +45,11 @@
(* Weakest guarantees *)
definition wg :: "['a program, 'a program set] => 'a program set" where
- "wg F Y == Union({X. F \<in> X guarantees Y})"
+ "wg F Y == \<Union>({X. F \<in> X guarantees Y})"
(* Weakest existential property stronger than X *)
definition wx :: "('a program) set => ('a program)set" where
- "wx X == Union({Y. Y \<subseteq> X & ex_prop Y})"
+ "wx X == \<Union>({Y. Y \<subseteq> X & ex_prop Y})"
(*Ill-defined programs can arise through "Join"*)
definition welldef :: "'a program set" where
--- a/src/HOL/UNITY/SubstAx.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/UNITY/SubstAx.thy Mon Dec 28 17:43:30 2015 +0100
@@ -61,7 +61,7 @@
done
lemma LeadsTo_Union:
- "(!!A. A \<in> S ==> F \<in> A LeadsTo B) ==> F \<in> (Union S) LeadsTo B"
+ "(!!A. A \<in> S ==> F \<in> A LeadsTo B) ==> F \<in> (\<Union>S) LeadsTo B"
apply (simp add: LeadsTo_def)
apply (subst Int_Union)
apply (blast intro: leadsTo_UN)
@@ -152,7 +152,7 @@
by (blast intro: LeadsTo_UN LeadsTo_weaken_L)
lemma LeadsTo_Union_distrib:
- "(F \<in> (Union S) LeadsTo B) = (\<forall>A \<in> S. F \<in> A LeadsTo B)"
+ "(F \<in> (\<Union>S) LeadsTo B) = (\<forall>A \<in> S. F \<in> A LeadsTo B)"
by (blast intro: LeadsTo_Union LeadsTo_weaken_L)
--- a/src/HOL/UNITY/UNITY.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/UNITY/UNITY.thy Mon Dec 28 17:43:30 2015 +0100
@@ -48,7 +48,7 @@
"stable A == A co A"
definition strongest_rhs :: "['a program, 'a set] => 'a set" where
- "strongest_rhs F A == Inter {B. F \<in> A co B}"
+ "strongest_rhs F A == \<Inter>{B. F \<in> A co B}"
definition invariant :: "'a set => 'a program set" where
"invariant A == {F. Init F \<subseteq> A} \<inter> stable A"
@@ -343,7 +343,7 @@
lemma Un_Diff_Diff [simp]: "A \<union> B - (A - B) = B"
by blast
-lemma Int_Union_Union: "Union(B) \<inter> A = Union((%C. C \<inter> A)`B)"
+lemma Int_Union_Union: "\<Union>B \<inter> A = \<Union>((%C. C \<inter> A)`B)"
by blast
text{*Needed for WF reasoning in WFair.thy*}
--- a/src/HOL/UNITY/WFair.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/UNITY/WFair.thy Mon Dec 28 17:43:30 2015 +0100
@@ -65,7 +65,7 @@
definition wlt :: "['a program, 'a set] => 'a set" where
--{*predicate transformer: the largest set that leads to @{term B}*}
- "wlt F B == Union {A. F \<in> A leadsTo B}"
+ "wlt F B == \<Union>{A. F \<in> A leadsTo B}"
notation leadsTo (infixl "\<longmapsto>" 60)
@@ -189,13 +189,13 @@
text{*The Union introduction rule as we should have liked to state it*}
lemma leadsTo_Union:
- "(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (Union S) leadsTo B"
+ "(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (\<Union>S) leadsTo B"
apply (unfold leadsTo_def)
apply (blast intro: leads.Union)
done
lemma leadsTo_Union_Int:
- "(!!A. A \<in> S ==> F \<in> (A \<inter> C) leadsTo B) ==> F \<in> (Union S \<inter> C) leadsTo B"
+ "(!!A. A \<in> S ==> F \<in> (A \<inter> C) leadsTo B) ==> F \<in> (\<Union>S \<inter> C) leadsTo B"
apply (unfold leadsTo_def)
apply (simp only: Int_Union_Union)
apply (blast intro: leads.Union)
@@ -223,7 +223,7 @@
!!A B. F \<in> A ensures B ==> P A B;
!!A B C. [| F \<in> A leadsTo B; P A B; F \<in> B leadsTo C; P B C |]
==> P A C;
- !!B S. \<forall>A \<in> S. F \<in> A leadsTo B & P A B ==> P (Union S) B
+ !!B S. \<forall>A \<in> S. F \<in> A leadsTo B & P A B ==> P (\<Union>S) B
|] ==> P za zb"
apply (unfold leadsTo_def)
apply (drule CollectD, erule leads.induct)
@@ -251,7 +251,7 @@
"[| F \<in> za leadsTo zb;
P zb;
!!A B. [| F \<in> A ensures B; P B |] ==> P A;
- !!S. \<forall>A \<in> S. P A ==> P (Union S)
+ !!S. \<forall>A \<in> S. P A ==> P (\<Union>S)
|] ==> P za"
txt{*by induction on this formula*}
apply (subgoal_tac "P zb --> P za")
@@ -265,7 +265,7 @@
"[| F \<in> za leadsTo zb;
P zb;
!!A B. [| F \<in> A ensures B; F \<in> B leadsTo zb; P B |] ==> P A;
- !!S. \<forall>A \<in> S. F \<in> A leadsTo zb & P A ==> P (Union S)
+ !!S. \<forall>A \<in> S. F \<in> A leadsTo zb & P A ==> P (\<Union>S)
|] ==> P za"
apply (subgoal_tac "F \<in> za leadsTo zb & P za")
apply (erule conjunct2)
@@ -293,7 +293,7 @@
by (blast intro: leadsTo_UN leadsTo_weaken_L)
lemma leadsTo_Union_distrib:
- "F \<in> (Union S) leadsTo B = (\<forall>A \<in> S. F \<in> A leadsTo B)"
+ "F \<in> (\<Union>S) leadsTo B = (\<forall>A \<in> S. F \<in> A leadsTo B)"
by (blast intro: leadsTo_Union leadsTo_weaken_L)
--- a/src/HOL/Wellfounded.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Wellfounded.thy Mon Dec 28 17:43:30 2015 +0100
@@ -305,7 +305,7 @@
lemma wf_Union:
"[| ALL r:R. wf r;
ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}
- |] ==> wf(Union R)"
+ |] ==> wf (\<Union> R)"
using wf_UN[of R "\<lambda>i. i"] by simp
(*Intuition: we find an (R u S)-min element of a nonempty subset A