--- a/src/HOL/Algebra/Lattice.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Algebra/Lattice.thy Fri Jun 26 10:20:33 2015 +0200
@@ -589,7 +589,7 @@
lemma (in weak_upper_semilattice) finite_sup_insertI:
assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L"
- shows "P (\<Squnion> (insert x A))"
+ shows "P (\<Squnion>(insert x A))"
proof (cases "A = {}")
case True with P and xA show ?thesis
by (simp add: finite_sup_least)
@@ -828,7 +828,7 @@
lemma (in weak_lower_semilattice) finite_inf_insertI:
assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L"
- shows "P (\<Sqinter> (insert x A))"
+ shows "P (\<Sqinter>(insert x A))"
proof (cases "A = {}")
case True with P and xA show ?thesis
by (simp add: finite_inf_greatest)
@@ -856,7 +856,7 @@
lemma (in weak_lower_semilattice) inf_of_two_greatest:
"[| x \<in> carrier L; y \<in> carrier L |] ==>
- greatest L (\<Sqinter> {x, y}) (Lower L {x, y})"
+ greatest L (\<Sqinter>{x, y}) (Lower L {x, y})"
proof (unfold inf_def)
assume L: "x \<in> carrier L" "y \<in> carrier L"
with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast
@@ -904,8 +904,8 @@
proof -
(* FIXME: improved simp, see weak_join_assoc above *)
have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
- also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma)
- also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
+ also from L have "... .= \<Sqinter>{z, x, y}" by (simp add: weak_meet_assoc_lemma)
+ also from L have "... = \<Sqinter>{x, y, z}" by (simp add: insert_commute)
also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric])
finally show ?thesis by (simp add: L)
qed
@@ -1286,15 +1286,15 @@
next
fix B
assume "B \<subseteq> carrier ?L"
- then have "least ?L (\<Union> B) (Upper ?L B)"
+ then have "least ?L (\<Union>B) (Upper ?L B)"
by (fastforce intro!: least_UpperI simp: Upper_def)
then show "EX s. least ?L s (Upper ?L B)" ..
next
fix B
assume "B \<subseteq> carrier ?L"
- then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
- txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
- @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
+ then have "greatest ?L (\<Inter>B \<inter> A) (Lower ?L B)"
+ txt {* @{term "\<Inter>B"} is not the infimum of @{term B}:
+ @{term "\<Inter>{} = UNIV"} which is in general bigger than @{term "A"}! *}
by (fastforce intro!: greatest_LowerI simp: Lower_def)
then show "EX i. greatest ?L i (Lower ?L B)" ..
qed
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Fri Jun 26 10:20:33 2015 +0200
@@ -1051,10 +1051,10 @@
lemma card_of_UNION_ordLeq_infinite:
assumes INF: "\<not>finite B" and
LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
-shows "|\<Union> i \<in> I. A i| \<le>o |B|"
+shows "|\<Union>i \<in> I. A i| \<le>o |B|"
proof(cases "I = {}", simp add: card_of_empty)
assume *: "I \<noteq> {}"
- have "|\<Union> i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
+ have "|\<Union>i \<in> I. A i| \<le>o |SIGMA i : I. A i|"
using card_of_UNION_Sigma by blast
moreover have "|SIGMA i : I. A i| \<le>o |B|"
using assms card_of_Sigma_ordLeq_infinite by blast
@@ -1064,14 +1064,14 @@
corollary card_of_UNION_ordLeq_infinite_Field:
assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
-shows "|\<Union> i \<in> I. A i| \<le>o r"
+shows "|\<Union>i \<in> I. A i| \<le>o r"
proof-
let ?B = "Field r"
have 1: "r =o |?B| \<and> |?B| =o r" using r card_of_Field_ordIso
ordIso_symmetric by blast
hence "|I| \<le>o |?B|" "\<forall>i \<in> I. |A i| \<le>o |?B|"
using LEQ_I LEQ ordLeq_ordIso_trans by blast+
- hence "|\<Union> i \<in> I. A i| \<le>o |?B|" using INF LEQ
+ hence "|\<Union>i \<in> I. A i| \<le>o |?B|" using INF LEQ
card_of_UNION_ordLeq_infinite by blast
thus ?thesis using 1 ordLeq_ordIso_trans by blast
qed
--- a/src/HOL/BNF_Wellorder_Embedding.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/BNF_Wellorder_Embedding.thy Fri Jun 26 10:20:33 2015 +0200
@@ -26,7 +26,7 @@
assumes WELL: "Well_order r" and
OF: "\<And> i. i \<in> I \<Longrightarrow> wo_rel.ofilter r (A i)" and
INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
-shows "inj_on f (\<Union> i \<in> I. A i)"
+shows "inj_on f (\<Union>i \<in> I. A i)"
proof-
have "wo_rel r" using WELL by (simp add: wo_rel_def)
hence "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i <= A j \<or> A j <= A i"
@@ -487,7 +487,7 @@
have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
have OF: "wo_rel.ofilter r (underS r a)"
by (auto simp add: Well wo_rel.underS_ofilter)
- hence UN: "underS r a = (\<Union> b \<in> underS r a. under r b)"
+ hence UN: "underS r a = (\<Union>b \<in> underS r a. under r b)"
using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast
(* Gather facts about elements of underS r a *)
{fix b assume *: "b \<in> underS r a"
@@ -520,13 +520,13 @@
(* *)
have OF': "wo_rel.ofilter r' (f`(underS r a))"
proof-
- have "f`(underS r a) = f`(\<Union> b \<in> underS r a. under r b)"
+ have "f`(underS r a) = f`(\<Union>b \<in> underS r a. under r b)"
using UN by auto
- also have "\<dots> = (\<Union> b \<in> underS r a. f`(under r b))" by blast
- also have "\<dots> = (\<Union> b \<in> underS r a. (under r' (f b)))"
+ also have "\<dots> = (\<Union>b \<in> underS r a. f`(under r b))" by blast
+ also have "\<dots> = (\<Union>b \<in> underS r a. (under r' (f b)))"
using bFact by auto
finally
- have "f`(underS r a) = (\<Union> b \<in> underS r a. (under r' (f b)))" .
+ have "f`(underS r a) = (\<Union>b \<in> underS r a. (under r' (f b)))" .
thus ?thesis
using Well' bFact
wo_rel.ofilter_UNION[of r' "underS r a" "\<lambda> b. under r' (f b)"] by fastforce
--- a/src/HOL/BNF_Wellorder_Relation.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/BNF_Wellorder_Relation.thy Fri Jun 26 10:20:33 2015 +0200
@@ -478,20 +478,20 @@
qed
lemma ofilter_UNION:
-"(\<And> i. i \<in> I \<Longrightarrow> ofilter(A i)) \<Longrightarrow> ofilter (\<Union> i \<in> I. A i)"
+"(\<And> i. i \<in> I \<Longrightarrow> ofilter(A i)) \<Longrightarrow> ofilter (\<Union>i \<in> I. A i)"
unfolding ofilter_def by blast
lemma ofilter_under_UNION:
assumes "ofilter A"
-shows "A = (\<Union> a \<in> A. under a)"
+shows "A = (\<Union>a \<in> A. under a)"
proof
have "\<forall>a \<in> A. under a \<le> A"
using assms ofilter_def by auto
- thus "(\<Union> a \<in> A. under a) \<le> A" by blast
+ thus "(\<Union>a \<in> A. under a) \<le> A" by blast
next
have "\<forall>a \<in> A. a \<in> under a"
using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast
- thus "A \<le> (\<Union> a \<in> A. under a)" by blast
+ thus "A \<le> (\<Union>a \<in> A. under a)" by blast
qed
subsubsection{* Other properties *}
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Fri Jun 26 10:20:33 2015 +0200
@@ -297,8 +297,8 @@
assumes "|A| \<le>o k" and "\<forall> a \<in> A. |vimage f {a}| \<le>o k" and "Cinfinite k"
shows "|vimage f A| \<le>o k"
proof-
- have "vimage f A = (\<Union> a \<in> A. vimage f {a})" by auto
- also have "|\<Union> a \<in> A. vimage f {a}| \<le>o k"
+ have "vimage f A = (\<Union>a \<in> A. vimage f {a})" by auto
+ also have "|\<Union>a \<in> A. vimage f {a}| \<le>o k"
using UNION_Cinfinite_bound[OF assms] .
finally show ?thesis .
qed
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Fri Jun 26 10:20:33 2015 +0200
@@ -715,7 +715,7 @@
lemma lists_def2: "lists A = {l. set l \<le> A}"
using in_listsI by blast
-lemma lists_UNION_nlists: "lists A = (\<Union> n. nlists A n)"
+lemma lists_UNION_nlists: "lists A = (\<Union>n. nlists A n)"
unfolding lists_def2 nlists_def by blast
lemma card_of_lists: "|A| \<le>o |lists A|"
@@ -1455,7 +1455,7 @@
unfolding Func_option_def Pfunc_def by auto
lemma Pfunc_Func_option:
-"Pfunc A B = (\<Union> A' \<in> Pow A. Func_option A' B)"
+"Pfunc A B = (\<Union>A' \<in> Pow A. Func_option A' B)"
proof safe
fix f assume f: "f \<in> Pfunc A B"
show "f \<in> (\<Union>A'\<in>Pow A. Func_option A' B)"
@@ -1504,7 +1504,7 @@
assumes "B \<noteq> {}"
shows "|Pfunc A B| \<le>o |Pow A <*> Func_option A B|"
proof-
- have "|Pfunc A B| =o |\<Union> A' \<in> Pow A. Func_option A' B|" (is "_ =o ?K")
+ have "|Pfunc A B| =o |\<Union>A' \<in> Pow A. Func_option A' B|" (is "_ =o ?K")
unfolding Pfunc_Func_option by(rule card_of_refl)
also have "?K \<le>o |Sigma (Pow A) (\<lambda> A'. Func_option A' B)|" using card_of_UNION_Sigma .
also have "|Sigma (Pow A) (\<lambda> A'. Func_option A' B)| \<le>o |Pow A <*> Func_option A B|"
@@ -1635,14 +1635,14 @@
qed
lemma relChain_stabilize:
-assumes rc: "relChain r As" and AsB: "(\<Union> i \<in> Field r. As i) \<subseteq> B" and Br: "|B| <o r"
+assumes rc: "relChain r As" and AsB: "(\<Union>i \<in> Field r. As i) \<subseteq> B" and Br: "|B| <o r"
and ir: "\<not>finite (Field r)" and cr: "Card_order r"
shows "\<exists> i \<in> Field r. As (succ r i) = As i"
proof(rule ccontr, auto)
have 0: "wo_rel r" and 00: "Well_order r"
unfolding wo_rel_def by (metis card_order_on_well_order_on cr)+
have L: "isLimOrd r" using ir cr by (metis card_order_infinite_isLimOrd)
- have AsBs: "(\<Union> i \<in> Field r. As (succ r i)) \<subseteq> B"
+ have AsBs: "(\<Union>i \<in> Field r. As (succ r i)) \<subseteq> B"
using AsB L apply safe by (metis "0" UN_I set_mp wo_rel.isLimOrd_succ)
assume As_s: "\<forall>i\<in>Field r. As (succ r i) \<noteq> As i"
have 1: "\<forall>i j. (i,j) \<in> r \<and> i \<noteq> j \<longrightarrow> As i \<subset> As j"
@@ -1719,7 +1719,7 @@
obtain j0 where j0: "j0 \<in> Field r" using Fi by auto
def g \<equiv> "\<lambda> a. if F a \<noteq> {} then gg a else j0"
have g: "\<forall> a \<in> A. \<forall> u \<in> F a. (f (a,u),g a) \<in> r" using gg unfolding g_def by auto
- hence 1: "Field r \<subseteq> (\<Union> a \<in> A. under r (g a))"
+ hence 1: "Field r \<subseteq> (\<Union>a \<in> A. under r (g a))"
using f[symmetric] unfolding under_def image_def by auto
have gA: "g ` A \<subseteq> Field r" using gg j0 unfolding Field_def g_def by auto
moreover have "cofinal (g ` A) r" unfolding cofinal_def proof safe
@@ -1751,10 +1751,10 @@
{assume Kr: "|K| <o r"
then obtain f where "\<forall> a \<in> Field r. f a \<in> K \<and> a \<noteq> f a \<and> (a, f a) \<in> r"
using cof unfolding cofinal_def by metis
- hence "Field r \<subseteq> (\<Union> a \<in> K. underS r a)" unfolding underS_def by auto
- hence "r \<le>o |\<Union> a \<in> K. underS r a|" using cr
+ hence "Field r \<subseteq> (\<Union>a \<in> K. underS r a)" unfolding underS_def by auto
+ hence "r \<le>o |\<Union>a \<in> K. underS r a|" using cr
by (metis Card_order_iff_ordLeq_card_of card_of_mono1 ordLeq_transitive)
- also have "|\<Union> a \<in> K. underS r a| \<le>o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma)
+ also have "|\<Union>a \<in> K. underS r a| \<le>o |SIGMA a: K. underS r a|" by (rule card_of_UNION_Sigma)
also
{have "\<forall> a \<in> K. |underS r a| <o r" using K by (metis card_of_underS cr subsetD)
hence "|SIGMA a: K. underS r a| <o r" using st Kr unfolding stable_def by auto
@@ -1818,9 +1818,9 @@
lemma stable_UNION:
assumes ST: "stable r" and A_LESS: "|A| <o r" and
F_LESS: "\<And> a. a \<in> A \<Longrightarrow> |F a| <o r"
-shows "|\<Union> a \<in> A. F a| <o r"
+shows "|\<Union>a \<in> A. F a| <o r"
proof-
- have "|\<Union> a \<in> A. F a| \<le>o |SIGMA a : A. F a|"
+ have "|\<Union>a \<in> A. F a| \<le>o |SIGMA a : A. F a|"
using card_of_UNION_Sigma by blast
thus ?thesis using assms stable_elim ordLeq_ordLess_trans by blast
qed
--- a/src/HOL/Cardinals/Order_Relation_More.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Cardinals/Order_Relation_More.thy Fri Jun 26 10:20:33 2015 +0200
@@ -133,12 +133,12 @@
lemma Refl_under_Under:
assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "Under r A = (\<Inter> a \<in> A. under r a)"
+shows "Under r A = (\<Inter>a \<in> A. under r a)"
proof
- show "Under r A \<subseteq> (\<Inter> a \<in> A. under r a)"
+ show "Under r A \<subseteq> (\<Inter>a \<in> A. under r a)"
by(unfold Under_def under_def, auto)
next
- show "(\<Inter> a \<in> A. under r a) \<subseteq> Under r A"
+ show "(\<Inter>a \<in> A. under r a) \<subseteq> Under r A"
proof(auto)
fix x
assume *: "\<forall>xa \<in> A. x \<in> under r xa"
@@ -157,12 +157,12 @@
lemma Refl_underS_UnderS:
assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "UnderS r A = (\<Inter> a \<in> A. underS r a)"
+shows "UnderS r A = (\<Inter>a \<in> A. underS r a)"
proof
- show "UnderS r A \<subseteq> (\<Inter> a \<in> A. underS r a)"
+ show "UnderS r A \<subseteq> (\<Inter>a \<in> A. underS r a)"
by(unfold UnderS_def underS_def, auto)
next
- show "(\<Inter> a \<in> A. underS r a) \<subseteq> UnderS r A"
+ show "(\<Inter>a \<in> A. underS r a) \<subseteq> UnderS r A"
proof(auto)
fix x
assume *: "\<forall>xa \<in> A. x \<in> underS r xa"
@@ -181,12 +181,12 @@
lemma Refl_above_Above:
assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "Above r A = (\<Inter> a \<in> A. above r a)"
+shows "Above r A = (\<Inter>a \<in> A. above r a)"
proof
- show "Above r A \<subseteq> (\<Inter> a \<in> A. above r a)"
+ show "Above r A \<subseteq> (\<Inter>a \<in> A. above r a)"
by(unfold Above_def above_def, auto)
next
- show "(\<Inter> a \<in> A. above r a) \<subseteq> Above r A"
+ show "(\<Inter>a \<in> A. above r a) \<subseteq> Above r A"
proof(auto)
fix x
assume *: "\<forall>xa \<in> A. x \<in> above r xa"
@@ -205,12 +205,12 @@
lemma Refl_aboveS_AboveS:
assumes REFL: "Refl r" and NE: "A \<noteq> {}"
-shows "AboveS r A = (\<Inter> a \<in> A. aboveS r a)"
+shows "AboveS r A = (\<Inter>a \<in> A. aboveS r a)"
proof
- show "AboveS r A \<subseteq> (\<Inter> a \<in> A. aboveS r a)"
+ show "AboveS r A \<subseteq> (\<Inter>a \<in> A. aboveS r a)"
by(unfold AboveS_def aboveS_def, auto)
next
- show "(\<Inter> a \<in> A. aboveS r a) \<subseteq> AboveS r A"
+ show "(\<Inter>a \<in> A. aboveS r a) \<subseteq> AboveS r A"
proof(auto)
fix x
assume *: "\<forall>xa \<in> A. x \<in> aboveS r xa"
--- a/src/HOL/Cardinals/Wellorder_Embedding.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Cardinals/Wellorder_Embedding.thy Fri Jun 26 10:20:33 2015 +0200
@@ -17,7 +17,7 @@
assumes WELL: "Well_order r" and
OF: "\<And> i. i \<in> I \<Longrightarrow> ofilter r (A i)" and
BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
-shows "bij_betw f (\<Union> i \<in> I. A i) (\<Union> i \<in> I. A' i)"
+shows "bij_betw f (\<Union>i \<in> I. A i) (\<Union>i \<in> I. A' i)"
proof-
have "wo_rel r" using WELL by (simp add: wo_rel_def)
hence "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i"
--- a/src/HOL/Cardinals/Wellorder_Relation.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy Fri Jun 26 10:20:33 2015 +0200
@@ -437,7 +437,7 @@
unfolding ofilter_def by blast
lemma ofilter_INTER:
-"\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter> i \<in> I. A i)"
+"\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> ofilter(A i)\<rbrakk> \<Longrightarrow> ofilter (\<Inter>i \<in> I. A i)"
unfolding ofilter_def by blast
lemma ofilter_Inter:
--- a/src/HOL/Complete_Lattices.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Complete_Lattices.thy Fri Jun 26 10:20:33 2015 +0200
@@ -1204,7 +1204,7 @@
"\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
by (fact Sup_image_eq)
-lemma Union_SetCompr_eq: "\<Union> {f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}"
+lemma Union_SetCompr_eq: "\<Union>{f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}"
by blast
lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<exists>x\<in>A. b \<in> B x)"
@@ -1360,7 +1360,7 @@
lemma inj_on_UNION_chain:
assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
- shows "inj_on f (\<Union> i \<in> I. A i)"
+ shows "inj_on f (\<Union>i \<in> I. A i)"
proof -
{
fix i j x y
@@ -1390,11 +1390,11 @@
lemma bij_betw_UNION_chain:
assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
- shows "bij_betw f (\<Union> i \<in> I. A i) (\<Union> i \<in> I. A' i)"
+ shows "bij_betw f (\<Union>i \<in> I. A i) (\<Union>i \<in> I. A' i)"
proof (unfold bij_betw_def, auto)
have "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
using BIJ bij_betw_def[of f] by auto
- thus "inj_on f (\<Union> i \<in> I. A i)"
+ thus "inj_on f (\<Union>i \<in> I. A i)"
using CH inj_on_UNION_chain[of I A f] by auto
next
fix i x
--- a/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy Fri Jun 26 10:20:33 2015 +0200
@@ -257,7 +257,7 @@
qed
corollary Fr_subtr:
-"Fr ns tr = \<Union> {Fr ns tr' | tr'. subtr ns tr' tr}"
+"Fr ns tr = \<Union>{Fr ns tr' | tr'. subtr ns tr' tr}"
unfolding Fr_def proof safe
fix t assume t: "inFr ns tr t" hence "root tr \<in> ns" by (rule inFr_root_in)
thus "t \<in> \<Union>{{t. inFr ns tr' t} |tr'. subtr ns tr' tr}"
@@ -272,7 +272,7 @@
by (metis (lifting) subtr.Step)
corollary Fr_subtr_cont:
-"Fr ns tr = \<Union> {Inl -` cont tr' | tr'. subtr ns tr' tr}"
+"Fr ns tr = \<Union>{Inl -` cont tr' | tr'. subtr ns tr' tr}"
unfolding Fr_def
apply safe
apply (frule inFr_subtr)
@@ -290,7 +290,7 @@
qed
corollary Itr_subtr:
-"Itr ns tr = \<Union> {Itr ns tr' | tr'. subtr ns tr' tr}"
+"Itr ns tr = \<Union>{Itr ns tr' | tr'. subtr ns tr' tr}"
unfolding Itr_def apply safe
apply (metis (lifting, mono_tags) UnionI inItr_root_in mem_Collect_eq subtr.Refl)
by (metis subtr_inItr)
@@ -1121,7 +1121,7 @@
assumes r: "regular tr" and In: "root tr \<in> ns"
shows "Fr ns tr =
Inl -` (cont tr) \<union>
- \<Union> {Fr (ns - {root tr}) tr' | tr'. Inr tr' \<in> cont tr}"
+ \<Union>{Fr (ns - {root tr}) tr' | tr'. Inr tr' \<in> cont tr}"
unfolding Fr_def
using In inFr.Base regular_inFr[OF assms] apply safe
apply (simp, metis (full_types) mem_Collect_eq)
@@ -1161,7 +1161,7 @@
lemma Lr_rec_in:
assumes n: "n \<in> ns"
shows "Lr ns n \<subseteq>
-{Inl -` tns \<union> (\<Union> {K n' | n'. Inr n' \<in> tns}) | tns K.
+{Inl -` tns \<union> (\<Union>{K n' | n'. Inr n' \<in> tns}) | tns K.
(n,tns) \<in> P \<and>
(\<forall> n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> Lr (ns - {n}) n')}"
(is "Lr ns n \<subseteq> {?F tns K | tns K. (n,tns) \<in> P \<and> ?\<phi> tns K}")
@@ -1207,7 +1207,7 @@
lemma L_rec_in:
assumes n: "n \<in> ns"
shows "
-{Inl -` tns \<union> (\<Union> {K n' | n'. Inr n' \<in> tns}) | tns K.
+{Inl -` tns \<union> (\<Union>{K n' | n'. Inr n' \<in> tns}) | tns K.
(n,tns) \<in> P \<and>
(\<forall> n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> L (ns - {n}) n')}
\<subseteq> L ns n"
@@ -1247,7 +1247,7 @@
function LL where
"LL ns n =
(if n \<notin> ns then {{}} else
- {Inl -` tns \<union> (\<Union> {K n' | n'. Inr n' \<in> tns}) | tns K.
+ {Inl -` tns \<union> (\<Union>{K n' | n'. Inr n' \<in> tns}) | tns K.
(n,tns) \<in> P \<and>
(\<forall> n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> LL (ns - {n}) n')})"
by(pat_completeness, auto)
--- a/src/HOL/Datatype_Examples/Lambda_Term.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Datatype_Examples/Lambda_Term.thy Fri Jun 26 10:20:33 2015 +0200
@@ -27,14 +27,14 @@
"varsOf (Var a) = {a}"
| "varsOf (App f x) = varsOf f \<union> varsOf x"
| "varsOf (Lam x b) = {x} \<union> varsOf b"
-| "varsOf (Lt F t) = varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| fimage (map_prod id varsOf) F})"
+| "varsOf (Lt F t) = varsOf t \<union> (\<Union>{{x} \<union> X | x X. (x,X) |\<in>| fimage (map_prod id varsOf) F})"
primrec fvarsOf :: "'a trm \<Rightarrow> 'a set" where
"fvarsOf (Var x) = {x}"
| "fvarsOf (App t1 t2) = fvarsOf t1 \<union> fvarsOf t2"
| "fvarsOf (Lam x t) = fvarsOf t - {x}"
| "fvarsOf (Lt xts t) = fvarsOf t - {x | x X. (x,X) |\<in>| fimage (map_prod id varsOf) xts} \<union>
- (\<Union> {X | x X. (x,X) |\<in>| fimage (map_prod id varsOf) xts})"
+ (\<Union>{X | x X. (x,X) |\<in>| fimage (map_prod id varsOf) xts})"
lemma diff_Un_incl_triv: "\<lbrakk>A \<subseteq> D; C \<subseteq> E\<rbrakk> \<Longrightarrow> A - B \<union> C \<subseteq> D \<union> E" by blast
--- a/src/HOL/Finite_Set.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Finite_Set.thy Fri Jun 26 10:20:33 2015 +0200
@@ -1433,7 +1433,7 @@
lemma insert_partition:
"\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
- \<Longrightarrow> x \<inter> \<Union> F = {}"
+ \<Longrightarrow> x \<inter> \<Union>F = {}"
by auto
lemma finite_psubset_induct[consumes 1, case_names psubset]:
@@ -1486,13 +1486,13 @@
text{* main cardinality theorem *}
lemma card_partition [rule_format]:
"finite C ==>
- finite (\<Union> C) -->
+ finite (\<Union>C) -->
(\<forall>c\<in>C. card c = k) -->
(\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->
- k * card(C) = card (\<Union> C)"
+ k * card(C) = card (\<Union>C)"
apply (erule finite_induct, simp)
apply (simp add: card_Un_disjoint insert_partition
- finite_subset [of _ "\<Union> (insert x F)"])
+ finite_subset [of _ "\<Union>(insert x F)"])
done
lemma card_eq_UNIV_imp_eq_UNIV:
--- a/src/HOL/HOLCF/Cont.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/HOLCF/Cont.thy Fri Jun 26 10:20:33 2015 +0200
@@ -91,7 +91,7 @@
text {* continuity implies preservation of lubs *}
lemma cont2contlubE:
- "\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion> i. Y i) = (\<Squnion> i. f (Y i))"
+ "\<lbrakk>cont f; chain Y\<rbrakk> \<Longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))"
apply (rule lub_eqI [symmetric])
apply (erule (1) contE)
done
--- a/src/HOL/Hilbert_Choice.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Hilbert_Choice.thy Fri Jun 26 10:20:33 2015 +0200
@@ -408,20 +408,20 @@
qed
lemma Ex_inj_on_UNION_Sigma:
- "\<exists>f. (inj_on f (\<Union> i \<in> I. A i) \<and> f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i))"
+ "\<exists>f. (inj_on f (\<Union>i \<in> I. A i) \<and> f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i))"
proof
let ?phi = "\<lambda> a i. i \<in> I \<and> a \<in> A i"
let ?sm = "\<lambda> a. SOME i. ?phi a i"
let ?f = "\<lambda>a. (?sm a, a)"
- have "inj_on ?f (\<Union> i \<in> I. A i)" unfolding inj_on_def by auto
+ have "inj_on ?f (\<Union>i \<in> I. A i)" unfolding inj_on_def by auto
moreover
{ { fix i a assume "i \<in> I" and "a \<in> A i"
hence "?sm a \<in> I \<and> a \<in> A(?sm a)" using someI[of "?phi a" i] by auto
}
- hence "?f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i)" by auto
+ hence "?f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i)" by auto
}
ultimately
- show "inj_on ?f (\<Union> i \<in> I. A i) \<and> ?f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i)"
+ show "inj_on ?f (\<Union>i \<in> I. A i) \<and> ?f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i)"
by auto
qed
--- a/src/HOL/Hoare/SchorrWaite.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Hoare/SchorrWaite.thy Fri Jun 26 10:20:33 2015 +0200
@@ -17,7 +17,7 @@
definition
relS :: "('a \<Rightarrow> 'a ref) set \<Rightarrow> ('a \<times> 'a) set"
- where "relS M = (\<Union> m \<in> M. rel m)"
+ where "relS M = (\<Union>m \<in> M. rel m)"
definition
addrs :: "'a ref set \<Rightarrow> 'a set"
--- a/src/HOL/Library/Indicator_Function.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Library/Indicator_Function.thy Fri Jun 26 10:20:33 2015 +0200
@@ -87,18 +87,18 @@
by auto
then have
"\<And>n. (indicator (A (n + i)) x :: 'a) = 1"
- "(indicator (\<Union> i. A i) x :: 'a) = 1"
+ "(indicator (\<Union>i. A i) x :: 'a) = 1"
using incseqD[OF \<open>incseq A\<close>, of i "n + i" for n] \<open>x \<in> A i\<close> by (auto simp: indicator_def)
then show ?thesis
by (rule_tac LIMSEQ_offset[of _ i]) simp
qed (auto simp: indicator_def)
lemma LIMSEQ_indicator_UN:
- "(\<lambda>k. indicator (\<Union> i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
+ "(\<lambda>k. indicator (\<Union>i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
proof -
- have "(\<lambda>k. indicator (\<Union> i<k. A i) x::'a) ----> indicator (\<Union>k. \<Union> i<k. A i) x"
+ have "(\<lambda>k. indicator (\<Union>i<k. A i) x::'a) ----> indicator (\<Union>k. \<Union>i<k. A i) x"
by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def intro: less_le_trans)
- also have "(\<Union>k. \<Union> i<k. A i) = (\<Union>i. A i)"
+ also have "(\<Union>k. \<Union>i<k. A i) = (\<Union>i. A i)"
by auto
finally show ?thesis .
qed
@@ -123,7 +123,7 @@
proof -
have "(\<lambda>k. indicator (\<Inter>i<k. A i) x::'a) ----> indicator (\<Inter>k. \<Inter>i<k. A i) x"
by (intro LIMSEQ_indicator_decseq) (auto simp: decseq_def intro: less_le_trans)
- also have "(\<Inter>k. \<Inter> i<k. A i) = (\<Inter>i. A i)"
+ also have "(\<Inter>k. \<Inter>i<k. A i) = (\<Inter>i. A i)"
by auto
finally show ?thesis .
qed
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Fri Jun 26 10:20:33 2015 +0200
@@ -604,7 +604,7 @@
lemma analytic_on_Un: "f analytic_on (s \<union> t) \<longleftrightarrow> f analytic_on s \<and> f analytic_on t"
by (auto simp: analytic_on_def)
-lemma analytic_on_Union: "f analytic_on (\<Union> s) \<longleftrightarrow> (\<forall>t \<in> s. f analytic_on t)"
+lemma analytic_on_Union: "f analytic_on (\<Union>s) \<longleftrightarrow> (\<forall>t \<in> s. f analytic_on t)"
by (auto simp: analytic_on_def)
lemma analytic_on_UN: "f analytic_on (\<Union>i\<in>I. s i) \<longleftrightarrow> (\<forall>i\<in>I. f analytic_on (s i))"
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jun 26 10:20:33 2015 +0200
@@ -384,7 +384,7 @@
lemma affine_UNIV[intro]: "affine UNIV"
unfolding affine_def by auto
-lemma affine_Inter[intro]: "(\<forall>s\<in>f. affine s) \<Longrightarrow> affine (\<Inter> f)"
+lemma affine_Inter[intro]: "(\<forall>s\<in>f. affine s) \<Longrightarrow> affine (\<Inter>f)"
unfolding affine_def by auto
lemma affine_Int[intro]: "affine s \<Longrightarrow> affine t \<Longrightarrow> affine (s \<inter> t)"
@@ -4552,7 +4552,7 @@
shows "\<exists>a. a \<noteq> 0 \<and> (\<forall>x\<in>s. 0 \<le> inner a x)"
proof -
let ?k = "\<lambda>c. {x::'a. 0 \<le> inner c x}"
- have "frontier (cball 0 1) \<inter> (\<Inter> (?k ` s)) \<noteq> {}"
+ have "frontier (cball 0 1) \<inter> (\<Inter>(?k ` s)) \<noteq> {}"
apply (rule compact_imp_fip)
apply (rule compact_frontier[OF compact_cball])
defer
@@ -4758,7 +4758,7 @@
lemma convex_halfspace_intersection:
fixes s :: "('a::euclidean_space) set"
assumes "closed s" "convex s"
- shows "s = \<Inter> {h. s \<subseteq> h \<and> (\<exists>a b. h = {x. inner a x \<le> b})}"
+ shows "s = \<Inter>{h. s \<subseteq> h \<and> (\<exists>a b. h = {x. inner a x \<le> b})}"
apply (rule set_eqI)
apply rule
unfolding Inter_iff Ball_def mem_Collect_eq
@@ -4935,7 +4935,7 @@
fixes f :: "'a::euclidean_space set set"
assumes "card f = n"
and "n \<ge> DIM('a) + 1"
- and "\<forall>s\<in>f. convex s" "\<forall>t\<subseteq>f. card t = DIM('a) + 1 \<longrightarrow> \<Inter> t \<noteq> {}"
+ and "\<forall>s\<in>f. convex s" "\<forall>t\<subseteq>f. card t = DIM('a) + 1 \<longrightarrow> \<Inter>t \<noteq> {}"
shows "\<Inter>f \<noteq> {}"
using assms
proof (induct n arbitrary: f)
@@ -5033,7 +5033,7 @@
lemma helly:
fixes f :: "'a::euclidean_space set set"
assumes "card f \<ge> DIM('a) + 1" "\<forall>s\<in>f. convex s"
- and "\<forall>t\<subseteq>f. card t = DIM('a) + 1 \<longrightarrow> \<Inter> t \<noteq> {}"
+ and "\<forall>t\<subseteq>f. card t = DIM('a) + 1 \<longrightarrow> \<Inter>t \<noteq> {}"
shows "\<Inter>f \<noteq> {}"
apply (rule helly_induct)
using assms
@@ -7756,7 +7756,7 @@
have "\<Inter>{closure S |S. S \<in> I} \<le> closure (\<Inter>{rel_interior S |S. S \<in> I})"
using convex_closure_rel_interior_inter assms by auto
moreover
- have "closure (\<Inter>{rel_interior S |S. S \<in> I}) \<le> closure (\<Inter> I)"
+ have "closure (\<Inter>{rel_interior S |S. S \<in> I}) \<le> closure (\<Inter>I)"
using rel_interior_inter_aux closure_mono[of "\<Inter>{rel_interior S |S. S \<in> I}" "\<Inter>I"]
by auto
ultimately show ?thesis
@@ -8750,7 +8750,7 @@
done
ultimately have "convex hull (\<Union>(K ` I)) \<supseteq> K0"
unfolding K0_def
- using hull_minimal[of _ "convex hull (\<Union> (K ` I))" "cone"]
+ using hull_minimal[of _ "convex hull (\<Union>(K ` I))" "cone"]
by blast
then have "K0 = convex hull (\<Union>(K ` I))"
using geq by auto
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Jun 26 10:20:33 2015 +0200
@@ -648,7 +648,7 @@
lemma gauge_inters:
assumes "finite s"
and "\<forall>d\<in>s. gauge (f d)"
- shows "gauge (\<lambda>x. \<Inter> {f d x | d. d \<in> s})"
+ shows "gauge (\<lambda>x. \<Inter>{f d x | d. d \<in> s})"
proof -
have *: "\<And>x. {f d x |d. d \<in> s} = (\<lambda>d. f d x) ` s"
by auto
@@ -871,7 +871,7 @@
assumes "finite f"
and "f \<noteq> {}"
and "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::euclidean_space) set)"
- shows "\<exists>p. p division_of (\<Inter> f)"
+ shows "\<exists>p. p division_of (\<Inter>f)"
using assms
proof (induct f rule: finite_induct)
case (insert x f)
@@ -1066,7 +1066,7 @@
done }
then have "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
by (meson Diff_subset division_of_subset)
- then have "\<exists>d. d division_of \<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)"
+ then have "\<exists>d. d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)"
apply -
apply (rule elementary_inters [OF finite_imageI[OF p(1)]])
apply (auto simp: False elementary_inters [OF finite_imageI[OF p(1)]])
@@ -1669,7 +1669,7 @@
unfolding fine_def by auto
lemma fine_inters:
- "(\<lambda>x. \<Inter> {f d x | d. d \<in> s}) fine p \<longleftrightarrow> (\<forall>d\<in>s. (f d) fine p)"
+ "(\<lambda>x. \<Inter>{f d x | d. d \<in> s}) fine p \<longleftrightarrow> (\<forall>d\<in>s. (f d) fine p)"
unfolding fine_def by blast
lemma fine_union: "d fine p1 \<Longrightarrow> d fine p2 \<Longrightarrow> d fine (p1 \<union> p2)"
@@ -1851,7 +1851,7 @@
by (blast intro: that)
}
assume as: "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d)"
- have "P (\<Union> ?A)"
+ have "P (\<Union>?A)"
proof (rule UN_cases)
let ?B = "(\<lambda>s. cbox (\<Sum>i\<in>Basis. (if i \<in> s then a\<bullet>i else (a\<bullet>i + b\<bullet>i) / 2) *\<^sub>R i::'a)
(\<Sum>i\<in>Basis. (if i \<in> s then (a\<bullet>i + b\<bullet>i) / 2 else b\<bullet>i) *\<^sub>R i)) ` {s. s \<subseteq> Basis}"
@@ -1926,7 +1926,7 @@
qed
qed
qed
- also have "\<Union> ?A = cbox a b"
+ also have "\<Union>?A = cbox a b"
proof (rule set_eqI,rule)
fix x
assume "x \<in> \<Union>?A"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jun 26 10:20:33 2015 +0200
@@ -413,7 +413,7 @@
subsection \<open>General notion of a topology as a value\<close>
definition "istopology L \<longleftrightarrow>
- L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
+ L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union>K))"
typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
morphisms "openin" "topology"
@@ -462,7 +462,7 @@
lemma openin_Int[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<inter> T)"
using openin_clauses by simp
-lemma openin_Union[intro]: "(\<forall>S \<in>K. openin U S) \<Longrightarrow> openin U (\<Union> K)"
+lemma openin_Union[intro]: "(\<forall>S \<in>K. openin U S) \<Longrightarrow> openin U (\<Union>K)"
using openin_clauses by simp
lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)"
@@ -501,13 +501,13 @@
lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)"
by (auto simp add: Diff_Un closedin_def)
-lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union> {A - s|s. s\<in>S}"
+lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union>{A - s|s. s\<in>S}"
by auto
lemma closedin_Inter[intro]:
assumes Ke: "K \<noteq> {}"
and Kc: "\<forall>S \<in>K. closedin U S"
- shows "closedin U (\<Inter> K)"
+ shows "closedin U (\<Inter>K)"
using Ke Kc unfolding closedin_def Diff_Inter by auto
lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)"
@@ -575,7 +575,7 @@
by blast
have "\<Union>K = (\<Union>Sk) \<inter> V"
using Sk by auto
- moreover have "openin U (\<Union> Sk)"
+ moreover have "openin U (\<Union>Sk)"
using Sk by (auto simp add: subset_eq)
ultimately have "?L (\<Union>K)" by blast
}
--- a/src/HOL/Nominal/Examples/Class2.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Nominal/Examples/Class2.thy Fri Jun 26 10:20:33 2015 +0200
@@ -2888,8 +2888,8 @@
and X::"('a::pt_name) set set"
and pi2::"coname prm"
and Y::"('b::pt_coname) set set"
- shows "(pi1\<bullet>(\<Inter> X)) = \<Inter> (pi1\<bullet>X)"
- and "(pi2\<bullet>(\<Inter> Y)) = \<Inter> (pi2\<bullet>Y)"
+ shows "(pi1\<bullet>(\<Inter>X)) = \<Inter>(pi1\<bullet>X)"
+ and "(pi2\<bullet>(\<Inter>Y)) = \<Inter>(pi2\<bullet>Y)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="(rev pi1)\<bullet>x" in exI)
apply(perm_simp)
--- a/src/HOL/Nominal/Nominal.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Nominal/Nominal.thy Fri Jun 26 10:20:33 2015 +0200
@@ -1888,9 +1888,9 @@
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE ('x)"
and fs: "fs TYPE('a) TYPE('x)"
- shows "((supp x)::'x set) = (\<Inter> {S. finite S \<and> S supports x})"
+ shows "((supp x)::'x set) = (\<Inter>{S. finite S \<and> S supports x})"
proof (rule equalityI)
- show "((supp x)::'x set) \<subseteq> (\<Inter> {S. finite S \<and> S supports x})"
+ show "((supp x)::'x set) \<subseteq> (\<Inter>{S. finite S \<and> S supports x})"
proof (clarify)
fix S c
assume b: "c\<in>((supp x)::'x set)" and "finite (S::'x set)" and "S supports x"
@@ -1898,7 +1898,7 @@
with b show "c\<in>S" by force
qed
next
- show "(\<Inter> {S. finite S \<and> S supports x}) \<subseteq> ((supp x)::'x set)"
+ show "(\<Inter>{S. finite S \<and> S supports x}) \<subseteq> ((supp x)::'x set)"
proof (clarify, simp)
fix c
assume d: "\<forall>(S::'x set). finite S \<and> S supports x \<longrightarrow> c\<in>S"
--- a/src/HOL/Probability/Bochner_Integration.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy Fri Jun 26 10:20:33 2015 +0200
@@ -83,7 +83,7 @@
by (rule finite_subset) auto }
{ fix N i n x assume "i \<le> N" "n \<le> N" "x \<in> B i n"
- then have 1: "\<exists>m\<le>N. x \<in> (\<Union> n\<le>N. B m n)" by auto
+ then have 1: "\<exists>m\<le>N. x \<in> (\<Union>n\<le>N. B m n)" by auto
from m[OF this] obtain n where n: "m N x \<le> N" "n \<le> N" "x \<in> B (m N x) n" by auto
moreover
def L \<equiv> "LEAST n. x \<in> B (m N x) n"
--- a/src/HOL/Probability/Caratheodory.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Probability/Caratheodory.thy Fri Jun 26 10:20:33 2015 +0200
@@ -804,7 +804,7 @@
with Ca Cb have "Ca \<inter> Cb \<subseteq> {{}}" by auto
then have C_Int_cases: "Ca \<inter> Cb = {{}} \<or> Ca \<inter> Cb = {}" by auto
- from `a \<inter> b = {}` have "\<mu>' (\<Union> (Ca \<union> Cb)) = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c)"
+ from `a \<inter> b = {}` have "\<mu>' (\<Union>(Ca \<union> Cb)) = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c)"
using Ca Cb by (intro \<mu>') (auto intro!: disjoint_union)
also have "\<dots> = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c) + (\<Sum>c\<in>Ca \<inter> Cb. \<mu> c)"
using C_Int_cases volume_empty[OF `volume M \<mu>`] by (elim disjE) simp_all
@@ -915,7 +915,7 @@
then have "disjoint_family f"
by (auto simp: disjoint_family_on_def f_def)
moreover
- have Ai_eq: "A i = (\<Union> x<card C. f x)"
+ have Ai_eq: "A i = (\<Union>x<card C. f x)"
using f C Ai unfolding bij_betw_def by (simp add: Union_image_eq[symmetric])
then have "\<Union>range f = A i"
using f C Ai unfolding bij_betw_def by (auto simp: f_def)
--- a/src/HOL/Probability/Measure_Space.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Probability/Measure_Space.thy Fri Jun 26 10:20:33 2015 +0200
@@ -172,17 +172,17 @@
case empty thus ?case using f by (auto simp: positive_def)
next
case (insert x F)
- hence in_M: "A x \<in> M" "(\<Union> i\<in>F. A i) \<in> M" "(\<Union> i\<in>F. A i) - A x \<in> M" using A by force+
- have subs: "(\<Union> i\<in>F. A i) - A x \<subseteq> (\<Union> i\<in>F. A i)" by auto
- have "(\<Union> i\<in>(insert x F). A i) = A x \<union> ((\<Union> i\<in>F. A i) - A x)" by auto
- hence "f (\<Union> i\<in>(insert x F). A i) = f (A x \<union> ((\<Union> i\<in>F. A i) - A x))"
+ hence in_M: "A x \<in> M" "(\<Union>i\<in>F. A i) \<in> M" "(\<Union>i\<in>F. A i) - A x \<in> M" using A by force+
+ have subs: "(\<Union>i\<in>F. A i) - A x \<subseteq> (\<Union>i\<in>F. A i)" by auto
+ have "(\<Union>i\<in>(insert x F). A i) = A x \<union> ((\<Union>i\<in>F. A i) - A x)" by auto
+ hence "f (\<Union>i\<in>(insert x F). A i) = f (A x \<union> ((\<Union>i\<in>F. A i) - A x))"
by simp
- also have "\<dots> = f (A x) + f ((\<Union> i\<in>F. A i) - A x)"
+ also have "\<dots> = f (A x) + f ((\<Union>i\<in>F. A i) - A x)"
using f(2) by (rule additiveD) (insert in_M, auto)
- also have "\<dots> \<le> f (A x) + f (\<Union> i\<in>F. A i)"
+ also have "\<dots> \<le> f (A x) + f (\<Union>i\<in>F. A i)"
using additive_increasing[OF f] in_M subs by (auto simp: increasing_def intro: add_left_mono)
also have "\<dots> \<le> f (A x) + (\<Sum>i\<in>F. f (A i))" using insert by (auto intro: add_left_mono)
- finally show "f (\<Union> i\<in>(insert x F). A i) \<le> (\<Sum>i\<in>(insert x F). f (A i))" using insert by simp
+ finally show "f (\<Union>i\<in>(insert x F). A i) \<le> (\<Sum>i\<in>(insert x F). f (A i))" using insert by simp
qed
lemma (in ring_of_sets) countably_additive_additive:
@@ -292,7 +292,7 @@
have *: "(\<Union>n. (\<Union>i<n. A i)) = (\<Union>i. A i)" by auto
have "(\<lambda>n. f (\<Union>i<n. A i)) ----> f (\<Union>i. A i)"
proof (unfold *[symmetric], intro cont[rule_format])
- show "range (\<lambda>i. \<Union> i<i. A i) \<subseteq> M" "(\<Union>i. \<Union> i<i. A i) \<in> M"
+ show "range (\<lambda>i. \<Union>i<i. A i) \<subseteq> M" "(\<Union>i. \<Union>i<i. A i) \<in> M"
using A * by auto
qed (force intro!: incseq_SucI)
moreover have "\<And>n. f (\<Union>i<n. A i) = (\<Sum>i<n. f (A i))"
@@ -657,10 +657,10 @@
lemma emeasure_UN_eq_0:
assumes "\<And>i::nat. emeasure M (N i) = 0" and "range N \<subseteq> sets M"
- shows "emeasure M (\<Union> i. N i) = 0"
+ shows "emeasure M (\<Union>i. N i) = 0"
proof -
- have "0 \<le> emeasure M (\<Union> i. N i)" using assms by auto
- moreover have "emeasure M (\<Union> i. N i) \<le> 0"
+ have "0 \<le> emeasure M (\<Union>i. N i)" using assms by auto
+ moreover have "emeasure M (\<Union>i. N i) \<le> 0"
using emeasure_subadditive_countably[OF assms(2)] assms(1) by simp
ultimately show ?thesis by simp
qed
@@ -1173,9 +1173,9 @@
from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto
with F show ?thesis by fastforce
qed
- show "emeasure M (\<Union> i\<le>n. F i) \<noteq> \<infinity>" for n
+ show "emeasure M (\<Union>i\<le>n. F i) \<noteq> \<infinity>" for n
proof -
- have "emeasure M (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. emeasure M (F i))"
+ have "emeasure M (\<Union>i\<le>n. F i) \<le> (\<Sum>i\<le>n. emeasure M (F i))"
using F by (auto intro!: emeasure_subadditive_finite)
also have "\<dots> < \<infinity>"
using F by (auto simp: setsum_Pinfty)
@@ -1579,12 +1579,12 @@
assumes "range f \<subseteq> sets M" "range g \<subseteq> sets M"
assumes "disjoint_family f" "disjoint_family g"
assumes "\<And> n :: nat. measure M (f n) = measure M (g n)"
- shows "measure M (\<Union> i. f i) = measure M (\<Union> i. g i)"
+ shows "measure M (\<Union>i. f i) = measure M (\<Union>i. g i)"
using assms
proof -
- have a: "(\<lambda> i. measure M (f i)) sums (measure M (\<Union> i. f i))"
+ have a: "(\<lambda> i. measure M (f i)) sums (measure M (\<Union>i. f i))"
by (rule finite_measure_UNION[OF assms(1,3)])
- have b: "(\<lambda> i. measure M (g i)) sums (measure M (\<Union> i. g i))"
+ have b: "(\<lambda> i. measure M (g i)) sums (measure M (\<Union>i. g i))"
by (rule finite_measure_UNION[OF assms(2,4)])
show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp
qed
@@ -1592,9 +1592,9 @@
lemma (in finite_measure) measure_countably_zero:
assumes "range c \<subseteq> sets M"
assumes "\<And> i. measure M (c i) = 0"
- shows "measure M (\<Union> i :: nat. c i) = 0"
+ shows "measure M (\<Union>i :: nat. c i) = 0"
proof (rule antisym)
- show "measure M (\<Union> i :: nat. c i) \<le> 0"
+ show "measure M (\<Union>i :: nat. c i) \<le> 0"
using finite_measure_subadditive_countably[OF assms(1)] by (simp add: assms(2))
qed (simp add: measure_nonneg)
@@ -1633,12 +1633,12 @@
assumes "\<And> x. x \<in> s \<Longrightarrow> e \<inter> f x \<in> sets M"
assumes "finite s"
assumes disjoint: "\<And> x y. \<lbrakk>x \<in> s ; y \<in> s ; x \<noteq> y\<rbrakk> \<Longrightarrow> f x \<inter> f y = {}"
- assumes upper: "space M \<subseteq> (\<Union> i \<in> s. f i)"
+ assumes upper: "space M \<subseteq> (\<Union>i \<in> s. f i)"
shows "measure M e = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
proof -
- have e: "e = (\<Union> i \<in> s. e \<inter> f i)"
+ have e: "e = (\<Union>i \<in> s. e \<inter> f i)"
using `e \<in> sets M` sets.sets_into_space upper by blast
- hence "measure M e = measure M (\<Union> i \<in> s. e \<inter> f i)" by simp
+ hence "measure M e = measure M (\<Union>i \<in> s. e \<inter> f i)" by simp
also have "\<dots> = (\<Sum> x \<in> s. measure M (e \<inter> f x))"
proof (rule finite_measure_finite_Union)
show "finite s" by fact
--- a/src/HOL/Probability/Projective_Limit.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Probability/Projective_Limit.thy Fri Jun 26 10:20:33 2015 +0200
@@ -282,15 +282,15 @@
have Y_notempty: "\<And>n. n \<ge> 1 \<Longrightarrow> (Y n) \<noteq> {}"
proof -
fix n::nat assume "n \<ge> 1" hence "Y n \<subseteq> Z n" by fact
- have "Y n = (\<Inter> i\<in>{1..n}. emb I (J n) (emb (J n) (J i) (K i)))" using J J_mono
+ have "Y n = (\<Inter>i\<in>{1..n}. emb I (J n) (emb (J n) (J i) (K i)))" using J J_mono
by (auto simp: Y_def Z'_def)
- also have "\<dots> = prod_emb I (\<lambda>_. borel) (J n) (\<Inter> i\<in>{1..n}. emb (J n) (J i) (K i))"
+ also have "\<dots> = prod_emb I (\<lambda>_. borel) (J n) (\<Inter>i\<in>{1..n}. emb (J n) (J i) (K i))"
using `n \<ge> 1`
by (subst prod_emb_INT) auto
finally
have Y_emb:
"Y n = prod_emb I (\<lambda>_. borel) (J n)
- (\<Inter> i\<in>{1..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i))" .
+ (\<Inter>i\<in>{1..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i))" .
hence "Y n \<in> ?G" using J J_mono K_sets `n \<ge> 1` by (intro generatorI[OF _ _ _ _ Y_emb]) auto
hence "\<bar>\<mu>G (Y n)\<bar> \<noteq> \<infinity>" unfolding Y_emb using J J_mono K_sets `n \<ge> 1`
by (subst mu_G_eq) (auto simp: limP_finite proj_sets mu_G_eq)
@@ -317,11 +317,11 @@
(auto dest!: bspec[where x=n]
simp: extensional_restrict emeasure_eq_measure prod_emb_iff simp del: limP_finite
intro!: measure_Diff[symmetric] set_mp[OF K_B])
- also have subs: "Z n - Y n \<subseteq> (\<Union> i\<in>{1..n}. (Z i - Z' i))" using Z' Z `n \<ge> 1`
+ also have subs: "Z n - Y n \<subseteq> (\<Union>i\<in>{1..n}. (Z i - Z' i))" using Z' Z `n \<ge> 1`
unfolding Y_def by (force simp: decseq_def)
- have "Z n - Y n \<in> ?G" "(\<Union> i\<in>{1..n}. (Z i - Z' i)) \<in> ?G"
+ have "Z n - Y n \<in> ?G" "(\<Union>i\<in>{1..n}. (Z i - Z' i)) \<in> ?G"
using `Z' _ \<in> ?G` `Z _ \<in> ?G` `Y _ \<in> ?G` by auto
- hence "\<mu>G (Z n - Y n) \<le> \<mu>G (\<Union> i\<in>{1..n}. (Z i - Z' i))"
+ hence "\<mu>G (Z n - Y n) \<le> \<mu>G (\<Union>i\<in>{1..n}. (Z i - Z' i))"
using subs G.additive_increasing[OF positive_mu_G[OF `I \<noteq> {}`] additive_mu_G[OF `I \<noteq> {}`]]
unfolding increasing_def by auto
also have "\<dots> \<le> (\<Sum> i\<in>{1..n}. \<mu>G (Z i - Z' i))" using `Z _ \<in> ?G` `Z' _ \<in> ?G`
--- a/src/HOL/Probability/Radon_Nikodym.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy Fri Jun 26 10:20:33 2015 +0200
@@ -625,7 +625,7 @@
next
case (Suc n)
with `?O n \<in> ?Q` `?O (Suc n) \<in> ?Q`
- emeasure_Diff[OF _ _ _ O_mono, of N n] emeasure_nonneg[of N "(\<Union> x\<le>n. Q' x)"]
+ emeasure_Diff[OF _ _ _ O_mono, of N n] emeasure_nonneg[of N "(\<Union>x\<le>n. Q' x)"]
show ?thesis
by (auto simp: sets_eq ereal_minus_eq_PInfty_iff Q_def)
qed }
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Fri Jun 26 10:20:33 2015 +0200
@@ -289,12 +289,12 @@
have [simp]: "length xs = n" using assms
by (auto simp: dc_crypto inversion_def [abs_def])
- have "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union> i < n. ?set i)"
+ have "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union>i < n. ?set i)"
unfolding dc_crypto payer_def by auto
- also have "\<dots> = (\<Union> ?sets)" by auto
- finally have eq_Union: "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union> ?sets)" by simp
+ also have "\<dots> = (\<Union>?sets)" by auto
+ finally have eq_Union: "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union>?sets)" by simp
- have card_double: "2 * card ?sets = card (\<Union> ?sets)"
+ have card_double: "2 * card ?sets = card (\<Union>?sets)"
proof (rule card_partition)
show "finite ?sets" by simp
{ fix i assume "i < n"
--- a/src/HOL/Topological_Spaces.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy Fri Jun 26 10:20:33 2015 +0200
@@ -20,7 +20,7 @@
class topological_space = "open" +
assumes open_UNIV [simp, intro]: "open UNIV"
assumes open_Int [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)"
- assumes open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union> K)"
+ assumes open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union>K)"
begin
definition
@@ -66,7 +66,7 @@
lemma closed_INT [continuous_intros, intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)"
unfolding closed_def by auto
-lemma closed_Inter [continuous_intros, intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)"
+lemma closed_Inter [continuous_intros, intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter>K)"
unfolding closed_def uminus_Inf by auto
lemma closed_Union [continuous_intros, intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
@@ -1067,12 +1067,12 @@
by (auto simp: decseq_def)
show "\<And>n. x \<in> (\<Inter>i\<le>n. A i)" "\<And>n. open (\<Inter>i\<le>n. A i)"
using A by auto
- show "nhds x = (INF n. principal (\<Inter> i\<le>n. A i))"
+ show "nhds x = (INF n. principal (\<Inter>i\<le>n. A i))"
using A unfolding nhds_def
apply (intro INF_eq)
apply simp_all
apply force
- apply (intro exI[of _ "\<Inter> i\<le>n. A i" for n] conjI open_INT)
+ apply (intro exI[of _ "\<Inter>i\<le>n. A i" for n] conjI open_INT)
apply auto
done
qed
@@ -1521,7 +1521,7 @@
"compact S \<longleftrightarrow> (\<forall>C. (\<forall>c\<in>C. open c) \<and> S \<subseteq> \<Union>C \<longrightarrow> (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
lemma compactI:
- assumes "\<And>C. \<forall>t\<in>C. open t \<Longrightarrow> s \<subseteq> \<Union> C \<Longrightarrow> \<exists>C'. C' \<subseteq> C \<and> finite C' \<and> s \<subseteq> \<Union> C'"
+ assumes "\<And>C. \<forall>t\<in>C. open t \<Longrightarrow> s \<subseteq> \<Union>C \<Longrightarrow> \<exists>C'. C' \<subseteq> C \<and> finite C' \<and> s \<subseteq> \<Union>C'"
shows "compact s"
unfolding compact_eq_heine_borel using assms by metis
@@ -1584,8 +1584,8 @@
qed
lemma compact_imp_fip:
- "compact s \<Longrightarrow> \<forall>t \<in> f. closed t \<Longrightarrow> \<forall>f'. finite f' \<and> f' \<subseteq> f \<longrightarrow> (s \<inter> (\<Inter> f') \<noteq> {}) \<Longrightarrow>
- s \<inter> (\<Inter> f) \<noteq> {}"
+ "compact s \<Longrightarrow> \<forall>t \<in> f. closed t \<Longrightarrow> \<forall>f'. finite f' \<and> f' \<subseteq> f \<longrightarrow> (s \<inter> (\<Inter>f') \<noteq> {}) \<Longrightarrow>
+ s \<inter> (\<Inter>f) \<noteq> {}"
unfolding compact_fip by auto
lemma compact_imp_fip_image:
--- a/src/HOL/ZF/Games.thy Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/ZF/Games.thy Fri Jun 26 10:20:33 2015 +0200
@@ -831,10 +831,10 @@
Pg_less_def: "G < H \<longleftrightarrow> G \<le> H \<and> G \<noteq> (H::Pg)"
definition
- Pg_minus_def: "- G = the_elem (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
+ Pg_minus_def: "- G = the_elem (\<Union>g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
definition
- Pg_plus_def: "G + H = the_elem (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})"
+ Pg_plus_def: "G + H = the_elem (\<Union>g \<in> Rep_Pg G. \<Union>h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})"
definition
Pg_diff_def: "G - H = G + (- (H::Pg))"