--- a/src/HOL/Analysis/Abstract_Topology.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy Mon Jan 28 10:27:47 2019 +0100
@@ -3090,7 +3090,7 @@
assume \<U>: "Ball \<U> (openin X) \<and> C \<subseteq> \<Union>\<U>"
have "(\<forall>U\<in>insert (topspace X - C) \<U>. openin X U)"
using XC \<U> by blast
- moreover have "K \<subseteq> \<Union>insert (topspace X - C) \<U>"
+ moreover have "K \<subseteq> \<Union>(insert (topspace X - C) \<U>)"
using \<U> XK compactin_subset_topspace by fastforce
ultimately obtain \<F> where "finite \<F>" "\<F> \<subseteq> insert (topspace X - C) \<U>" "K \<subseteq> \<Union>\<F>"
using assms unfolding compactin_def by metis
--- a/src/HOL/Analysis/Arcwise_Connected.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Arcwise_Connected.thy Mon Jan 28 10:27:47 2019 +0100
@@ -13,7 +13,7 @@
theorem Brouwer_reduction_theorem_gen:
fixes S :: "'a::euclidean_space set"
assumes "closed S" "\<phi> S"
- and \<phi>: "\<And>F. \<lbrakk>\<And>n. closed(F n); \<And>n. \<phi>(F n); \<And>n. F(Suc n) \<subseteq> F n\<rbrakk> \<Longrightarrow> \<phi>(\<Inter>range F)"
+ and \<phi>: "\<And>F. \<lbrakk>\<And>n. closed(F n); \<And>n. \<phi>(F n); \<And>n. F(Suc n) \<subseteq> F n\<rbrakk> \<Longrightarrow> \<phi>(\<Inter>(range F))"
obtains T where "T \<subseteq> S" "closed T" "\<phi> T" "\<And>U. \<lbrakk>U \<subseteq> S; closed U; \<phi> U\<rbrakk> \<Longrightarrow> \<not> (U \<subset> T)"
proof -
obtain B :: "nat \<Rightarrow> 'a set"
@@ -36,7 +36,7 @@
by (induction n) (auto simp: assms ASuc dest!: someI_ex)
show ?thesis
proof
- show "\<Inter>range A \<subseteq> S"
+ show "\<Inter>(range A) \<subseteq> S"
using \<open>\<And>n. A n \<subseteq> S\<close> by blast
show "closed (\<Inter>(A ` UNIV))"
using clo by blast
@@ -81,7 +81,7 @@
corollary Brouwer_reduction_theorem:
fixes S :: "'a::euclidean_space set"
assumes "compact S" "\<phi> S" "S \<noteq> {}"
- and \<phi>: "\<And>F. \<lbrakk>\<And>n. compact(F n); \<And>n. F n \<noteq> {}; \<And>n. \<phi>(F n); \<And>n. F(Suc n) \<subseteq> F n\<rbrakk> \<Longrightarrow> \<phi>(\<Inter>range F)"
+ and \<phi>: "\<And>F. \<lbrakk>\<And>n. compact(F n); \<And>n. F n \<noteq> {}; \<And>n. \<phi>(F n); \<And>n. F(Suc n) \<subseteq> F n\<rbrakk> \<Longrightarrow> \<phi>(\<Inter>(range F))"
obtains T where "T \<subseteq> S" "compact T" "T \<noteq> {}" "\<phi> T"
"\<And>U. \<lbrakk>U \<subseteq> S; closed U; U \<noteq> {}; \<phi> U\<rbrakk> \<Longrightarrow> \<not> (U \<subset> T)"
proof (rule Brouwer_reduction_theorem_gen [of S "\<lambda>T. T \<noteq> {} \<and> T \<subseteq> S \<and> \<phi> T"])
--- a/src/HOL/Analysis/Borel_Space.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy Mon Jan 28 10:27:47 2019 +0100
@@ -529,7 +529,7 @@
from ex_countable_basis obtain B :: "'a set set" where
B: "\<And>b. b \<in> B \<Longrightarrow> open b" "\<And>X. open X \<Longrightarrow> \<exists>b\<subseteq>B. (\<Union>b) = X" and "countable B"
by (auto simp: topological_basis_def)
- from B(2)[OF K] obtain m where m: "\<And>k. k \<in> K \<Longrightarrow> m k \<subseteq> B" "\<And>k. k \<in> K \<Longrightarrow> (\<Union>m k) = k"
+ from B(2)[OF K] obtain m where m: "\<And>k. k \<in> K \<Longrightarrow> m k \<subseteq> B" "\<And>k. k \<in> K \<Longrightarrow> \<Union>(m k) = k"
by metis
define U where "U = (\<Union>k\<in>K. m k)"
with m have "countable U"
--- a/src/HOL/Analysis/Caratheodory.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Caratheodory.thy Mon Jan 28 10:27:47 2019 +0100
@@ -550,7 +550,7 @@
then show "\<mu> (\<Union>C) = sum \<mu> C"
proof (induct C)
case (insert c C)
- from insert(1,2,4,5) have "\<mu> (\<Union>insert c C) = \<mu> c + \<mu> (\<Union>C)"
+ from insert(1,2,4,5) have "\<mu> (\<Union>(insert c C)) = \<mu> c + \<mu> (\<Union>C)"
by (auto intro!: add simp: disjoint_def)
with insert show ?case
by (simp add: disjoint_def)
@@ -712,7 +712,7 @@
from A C' \<open>c \<in> C'\<close> have UN_eq: "(\<Union>i. A i) = c"
by (auto simp: A_def)
- have "\<forall>i::nat. \<exists>f::nat \<Rightarrow> 'a set. \<mu>_r (A i) = (\<Sum>j. \<mu>_r (f j)) \<and> disjoint_family f \<and> \<Union>range f = A i \<and> (\<forall>j. f j \<in> M)"
+ have "\<forall>i::nat. \<exists>f::nat \<Rightarrow> 'a set. \<mu>_r (A i) = (\<Sum>j. \<mu>_r (f j)) \<and> disjoint_family f \<and> \<Union>(range f) = A i \<and> (\<forall>j. f j \<in> M)"
(is "\<forall>i. ?P i")
proof
fix i
@@ -735,7 +735,7 @@
moreover
have Ai_eq: "A i = (\<Union>x<card C. f x)"
using f C Ai unfolding bij_betw_def by auto
- then have "\<Union>range f = A i"
+ then have "\<Union>(range f) = A i"
using f C Ai unfolding bij_betw_def
by (auto simp add: f_def cong del: SUP_cong_simp)
moreover
--- a/src/HOL/Analysis/Conformal_Mappings.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Mon Jan 28 10:27:47 2019 +0100
@@ -457,7 +457,7 @@
ultimately show ?thesis
by (rule *)
qed
- then have "open (f ` \<Union>components U)"
+ then have "open (f ` \<Union>(components U))"
by (metis (no_types, lifting) imageE image_Union open_Union)
then show ?thesis
by force
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Mon Jan 28 10:27:47 2019 +0100
@@ -898,7 +898,7 @@
lemma compact_nest:
fixes F :: "'a::linorder \<Rightarrow> 'b::heine_borel set"
assumes F: "\<And>n. compact(F n)" "\<And>n. F n \<noteq> {}" and mono: "\<And>m n. m \<le> n \<Longrightarrow> F n \<subseteq> F m"
- shows "\<Inter>range F \<noteq> {}"
+ shows "\<Inter>(range F) \<noteq> {}"
proof -
have *: "\<And>S T. S \<in> range F \<and> T \<in> range F \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
by (metis mono image_iff le_cases)
--- a/src/HOL/Analysis/Elementary_Topology.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy Mon Jan 28 10:27:47 2019 +0100
@@ -2248,7 +2248,7 @@
using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>(a`D)"] conjI) (auto intro!: open_INT)
qed
then obtain a d where a: "\<And>x. x\<in>s \<Longrightarrow> open (a x)" "s \<subseteq> (\<Union>x\<in>s. a x)"
- and d: "\<And>x. x \<in> s \<Longrightarrow> d x \<subseteq> C \<and> finite (d x) \<and> a x \<times> t \<subseteq> \<Union>d x"
+ and d: "\<And>x. x \<in> s \<Longrightarrow> d x \<subseteq> C \<and> finite (d x) \<and> a x \<times> t \<subseteq> \<Union>(d x)"
unfolding subset_eq UN_iff by metis
moreover
from compactE_image[OF \<open>compact s\<close> a]
@@ -2258,9 +2258,9 @@
{
from s have "s \<times> t \<subseteq> (\<Union>x\<in>e. a x \<times> t)"
by auto
- also have "\<dots> \<subseteq> (\<Union>x\<in>e. \<Union>d x)"
+ also have "\<dots> \<subseteq> (\<Union>x\<in>e. \<Union>(d x))"
using d \<open>e \<subseteq> s\<close> by (intro UN_mono) auto
- finally have "s \<times> t \<subseteq> (\<Union>x\<in>e. \<Union>d x)" .
+ finally have "s \<times> t \<subseteq> (\<Union>x\<in>e. \<Union>(d x))" .
}
ultimately show "\<exists>C'\<subseteq>C. finite C' \<and> s \<times> t \<subseteq> \<Union>C'"
by (intro exI[of _ "(\<Union>x\<in>e. d x)"]) (auto simp: subset_eq)
--- a/src/HOL/Analysis/Finite_Product_Measure.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Mon Jan 28 10:27:47 2019 +0100
@@ -970,7 +970,7 @@
obtain F where F: "\<And>j. countable (F j)" "\<And>j f. f \<in> F j \<Longrightarrow> f \<in> sets (M j)"
"\<And>j f. f \<in> F j \<Longrightarrow> emeasure (M j) f \<noteq> \<infinity>" and
- in_space: "\<And>j. space (M j) = (\<Union>F j)"
+ in_space: "\<And>j. space (M j) = \<Union>(F j)"
using sigma_finite_countable by (metis subset_eq)
moreover have "(\<Union>(Pi\<^sub>E I ` Pi\<^sub>E I F)) = space (Pi\<^sub>M I M)"
using in_space by (auto simp: space_PiM PiE_iff intro!: PiE_choice[THEN iffD2])
--- a/src/HOL/Analysis/Function_Topology.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy Mon Jan 28 10:27:47 2019 +0100
@@ -671,7 +671,7 @@
let ?U = "\<lambda>j. U j \<inter> (if j = i then V else topspace(X j))"
show ?case
proof (intro exI conjI)
- show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>insert F \<F> = Pi\<^sub>E I ?U"
+ show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>(insert F \<F>) = Pi\<^sub>E I ?U"
using eq PiE_mem \<open>i \<in> I\<close> by (auto simp: \<open>F = {f. f i \<in> V}\<close>) fastforce
next
show "finite {i \<in> I. ?U i \<noteq> topspace (X i)}"
--- a/src/HOL/Analysis/Further_Topology.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy Mon Jan 28 10:27:47 2019 +0100
@@ -655,11 +655,11 @@
using contf apply (force simp: elim: continuous_on_subset)
using contg apply (force simp: elim: continuous_on_subset)
using fh gh insert.hyps pwX by fastforce
- then show "continuous_on (\<Union>insert X \<F> - insert a C) (\<lambda>a. if a \<in> X then f a else g a)"
+ then show "continuous_on (\<Union>(insert X \<F>) - insert a C) (\<lambda>a. if a \<in> X then f a else g a)"
by (blast intro: continuous_on_subset)
- show "\<forall>x\<in>(\<Union>insert X \<F> - insert a C) \<inter> K. (if x \<in> X then f x else g x) = h x"
+ show "\<forall>x\<in>(\<Union>(insert X \<F>) - insert a C) \<inter> K. (if x \<in> X then f x else g x) = h x"
using gh by (auto simp: fh)
- show "(\<lambda>a. if a \<in> X then f a else g a) ` (\<Union>insert X \<F> - insert a C) \<subseteq> T"
+ show "(\<lambda>a. if a \<in> X then f a else g a) ` (\<Union>(insert X \<F>) - insert a C) \<subseteq> T"
using fim gim by auto force
qed
qed
--- a/src/HOL/Analysis/Polytope.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Polytope.thy Mon Jan 28 10:27:47 2019 +0100
@@ -468,28 +468,28 @@
by (simp add: aff_dim_le_DIM)
next
case (Suc n)
- have fs: "\<Inter>d (Suc n) face_of S"
+ have fs: "\<Inter>(d (Suc n)) face_of S"
by (meson Suc.prems cfaI dn_le_Suc dn_notempty face_of_Inter subsetCE)
- have condn: "convex (\<Inter>d n)"
+ have condn: "convex (\<Inter>(d n))"
using Suc.prems nat_le_linear not_less_eq_eq
by (blast intro: face_of_imp_convex cfaI convex_Inter dest: dn_le_Suc)
- have fdn: "\<Inter>d (Suc n) face_of \<Inter>d n"
+ have fdn: "\<Inter>(d (Suc n)) face_of \<Inter>(d n)"
by (metis (no_types, lifting) Inter_anti_mono Suc.prems dSuc cfaI dn_le_Suc dn_notempty face_of_Inter face_of_imp_subset face_of_subset subset_iff subset_insertI)
- have ne: "\<Inter>d (Suc n) \<noteq> \<Inter>d n"
+ have ne: "\<Inter>(d (Suc n)) \<noteq> \<Inter>(d n)"
by (metis (no_types, lifting) Suc.prems Suc_leD c complete_lattice_class.Inf_insert dSuc dn_le_Suc less_irrefl order.trans)
have *: "\<And>m::int. \<And>d. \<And>d'::int. d < d' \<and> d' \<le> m - n \<Longrightarrow> d \<le> m - of_nat(n+1)"
by arith
- have "aff_dim (\<Inter>d (Suc n)) < aff_dim (\<Inter>d n)"
+ have "aff_dim (\<Inter>(d (Suc n))) < aff_dim (\<Inter>(d n))"
by (rule face_of_aff_dim_lt [OF condn fdn ne])
- moreover have "aff_dim (\<Inter>d n) \<le> int (DIM('a)) - int n"
+ moreover have "aff_dim (\<Inter>(d n)) \<le> int (DIM('a)) - int n"
using Suc by auto
ultimately
- have "aff_dim (\<Inter>d (Suc n)) \<le> int (DIM('a)) - (n+1)" by arith
+ have "aff_dim (\<Inter>(d (Suc n))) \<le> int (DIM('a)) - (n+1)" by arith
then show ?case by linarith
qed
- have "aff_dim (\<Inter>d (DIM('a) + 2)) \<le> -2"
+ have "aff_dim (\<Inter>(d (DIM('a) + 2))) \<le> -2"
using aff_dim_le [OF order_refl] by simp
- with aff_dim_geq [of "\<Inter>d (DIM('a) + 2)"] show ?thesis
+ with aff_dim_geq [of "\<Inter>(d (DIM('a) + 2))"] show ?thesis
using order.trans by fastforce
next
case False
--- a/src/HOL/Analysis/Radon_Nikodym.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Radon_Nikodym.thy Mon Jan 28 10:27:47 2019 +0100
@@ -837,7 +837,7 @@
show "range (\<lambda>(i, j). A i \<inter> Q j) \<subseteq> sets (density M f)"
using A_in_sets by auto
next
- have "\<Union>range (\<lambda>(i, j). A i \<inter> Q j) = (\<Union>i j. A i \<inter> Q j)"
+ have "\<Union>(range (\<lambda>(i, j). A i \<inter> Q j)) = (\<Union>i j. A i \<inter> Q j)"
by auto
also have "\<dots> = (\<Union>i. A i) \<inter> space M" using Q by auto
also have "(\<Union>i. A i) = space M"
@@ -856,7 +856,7 @@
using x real by (auto simp: A_def ennreal_of_nat_eq_real_of_nat intro!: exI[of _ "Suc n"])
qed
qed (auto simp: A_def)
- finally show "\<Union>range (\<lambda>(i, j). A i \<inter> Q j) = space ?N" by simp
+ finally show "\<Union>(range (\<lambda>(i, j). A i \<inter> Q j)) = space ?N" by simp
next
fix X assume "X \<in> range (\<lambda>(i, j). A i \<inter> Q j)"
then obtain i j where [simp]:"X = A i \<inter> Q j" by auto
--- a/src/HOL/Analysis/Starlike.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy Mon Jan 28 10:27:47 2019 +0100
@@ -4866,7 +4866,7 @@
let ?\<C> = "insert (U \<union> V) ((\<lambda>S. N - S) ` \<F>)"
obtain \<D> where "\<D> \<subseteq> ?\<C>" "finite \<D>" "K \<subseteq> \<Union>\<D>"
proof (rule compactE [OF \<open>compact K\<close>])
- show "K \<subseteq> \<Union>insert (U \<union> V) ((-) N ` \<F>)"
+ show "K \<subseteq> \<Union>(insert (U \<union> V) ((-) N ` \<F>))"
using \<open>K \<subseteq> N\<close> ABeq \<open>A \<subseteq> U\<close> \<open>B \<subseteq> V\<close> by auto
show "\<And>B. B \<in> insert (U \<union> V) ((-) N ` \<F>) \<Longrightarrow> open B"
by (auto simp: \<open>open U\<close> \<open>open V\<close> open_Un \<open>open N\<close> cc compact_imp_closed open_Diff)
@@ -6818,7 +6818,7 @@
by metis
obtain K where K: "closed K" "U \<inter> K = S"
using cin by (auto simp: closedin_closed)
- have 1: "U \<subseteq> \<Union>insert (- K) (F ` \<C>)"
+ have 1: "U \<subseteq> \<Union>(insert (- K) (F ` \<C>))"
by clarsimp (metis Int_iff Union_iff \<open>U \<inter> K = S\<close> \<open>S \<subseteq> \<Union>\<C>\<close> subsetD intF)
have 2: "\<And>T. T \<in> insert (- K) (F ` \<C>) \<Longrightarrow> open T"
using \<open>closed K\<close> by (auto simp: opF)
--- a/src/HOL/Analysis/Tagged_Division.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy Mon Jan 28 10:27:47 2019 +0100
@@ -633,7 +633,7 @@
qed
obtain q where q: "\<And>x. x \<in> p \<Longrightarrow> q x division_of cbox a b" "\<And>x. x \<in> p \<Longrightarrow> x \<in> q x"
using bchoice[OF div_cbox] by blast
- have "q x division_of \<Union>q x" if x: "x \<in> p" for x
+ have "q x division_of \<Union>(q x)" if x: "x \<in> p" for x
apply (rule division_ofI)
using division_ofD[OF q(1)[OF x]] by auto
then have di: "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
@@ -736,7 +736,7 @@
assumes "finite f"
and "\<And>p. p \<in> f \<Longrightarrow> p division_of (\<Union>p)"
and "\<And>k1 k2. k1 \<in> \<Union>f \<Longrightarrow> k2 \<in> \<Union>f \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
- shows "\<Union>f division_of \<Union>\<Union>f"
+ shows "\<Union>f division_of \<Union>(\<Union>f)"
using assms by (auto intro!: division_ofI)
lemma elementary_union_interval:
@@ -781,7 +781,7 @@
by auto
show "finite ?D"
using "*" pdiv(1) q(1) by auto
- have "\<Union>?D = (\<Union>x\<in>p. \<Union>insert (cbox a b) (q x))"
+ have "\<Union>?D = (\<Union>x\<in>p. \<Union>(insert (cbox a b) (q x)))"
by auto
also have "... = \<Union>{cbox a b \<union> t |t. t \<in> p}"
using q(6) by auto
@@ -847,7 +847,7 @@
from assms(2)[OF as(4)] obtain a b where x: "x = cbox a b" by blast
have *: "\<Union>F = \<Union>p"
using division_ofD[OF p] by auto
- show "\<exists>p. p division_of \<Union>insert x F"
+ show "\<exists>p. p division_of \<Union>(insert x F)"
using elementary_union_interval[OF p[unfolded *], of a b]
unfolding Union_insert x * by metis
qed (insert assms, auto)
--- a/src/HOL/BNF_Composition.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/BNF_Composition.thy Mon Jan 28 10:27:47 2019 +0100
@@ -75,7 +75,7 @@
lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
by blast
-lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
+lemma comp_set_bd_Union_o_collect: "|\<Union>(\<Union>((\<lambda>f. f x) ` X))| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
by (unfold comp_apply collect_def) simp
lemma Collect_inj: "Collect P = Collect Q \<Longrightarrow> P = Q"
--- a/src/HOL/Complete_Lattices.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Complete_Lattices.thy Mon Jan 28 10:27:47 2019 +0100
@@ -15,10 +15,10 @@
subsection \<open>Syntactic infimum and supremum operations\<close>
class Inf =
- fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter> _" [900] 900)
+ fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>")
class Sup =
- fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion> _" [900] 900)
+ fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>")
syntax (ASCII)
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _./ _)" [0, 10] 10)
@@ -40,10 +40,10 @@
translations
"\<Sqinter>x y. f" \<rightleftharpoons> "\<Sqinter>x. \<Sqinter>y. f"
- "\<Sqinter>x. f" \<rightleftharpoons> "\<Sqinter>CONST range (\<lambda>x. f)"
+ "\<Sqinter>x. f" \<rightleftharpoons> "\<Sqinter>(CONST range (\<lambda>x. f))"
"\<Sqinter>x\<in>A. f" \<rightleftharpoons> "CONST Inf ((\<lambda>x. f) ` A)"
"\<Squnion>x y. f" \<rightleftharpoons> "\<Squnion>x. \<Squnion>y. f"
- "\<Squnion>x. f" \<rightleftharpoons> "\<Squnion>CONST range (\<lambda>x. f)"
+ "\<Squnion>x. f" \<rightleftharpoons> "\<Squnion>(CONST range (\<lambda>x. f))"
"\<Squnion>x\<in>A. f" \<rightleftharpoons> "CONST Sup ((\<lambda>x. f) ` A)"
context Inf
@@ -175,13 +175,13 @@
lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<le> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<le> u)"
using Sup_le_iff [of "f ` A"] by simp
-lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
+lemma Inf_insert [simp]: "\<Sqinter>(insert a A) = a \<sqinter> \<Sqinter>A"
by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> \<Sqinter>(f ` A)"
by (simp cong del: INF_cong_simp)
-lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
+lemma Sup_insert [simp]: "\<Squnion>(insert a A) = a \<squnion> \<Squnion>A"
by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> \<Squnion>(f ` A)"
@@ -779,7 +779,7 @@
subsubsection \<open>Inter\<close>
-abbreviation Inter :: "'a set set \<Rightarrow> 'a set" ("\<Inter> _" [900] 900)
+abbreviation Inter :: "'a set set \<Rightarrow> 'a set" ("\<Inter>")
where "\<Inter>S \<equiv> \<Sqinter>S"
lemma Inter_eq: "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
@@ -860,7 +860,7 @@
translations
"\<Inter>x y. f" \<rightleftharpoons> "\<Inter>x. \<Inter>y. f"
- "\<Inter>x. f" \<rightleftharpoons> "\<Inter>CONST range (\<lambda>x. f)"
+ "\<Inter>x. f" \<rightleftharpoons> "\<Inter>(CONST range (\<lambda>x. f))"
"\<Inter>x\<in>A. f" \<rightleftharpoons> "CONST Inter ((\<lambda>x. f) ` A)"
lemma INTER_eq: "(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
@@ -933,7 +933,7 @@
subsubsection \<open>Union\<close>
-abbreviation Union :: "'a set set \<Rightarrow> 'a set" ("\<Union> _" [900] 900)
+abbreviation Union :: "'a set set \<Rightarrow> 'a set" ("\<Union>")
where "\<Union>S \<equiv> \<Squnion>S"
lemma Union_eq: "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
@@ -968,7 +968,7 @@
lemma Union_UNIV: "\<Union>UNIV = UNIV"
by (fact Sup_UNIV) (* already simp *)
-lemma Union_insert: "\<Union>insert a B = a \<union> \<Union>B"
+lemma Union_insert: "\<Union>(insert a B) = a \<union> \<Union>B"
by (fact Sup_insert) (* already simp *)
lemma Union_Un_distrib [simp]: "\<Union>(A \<union> B) = \<Union>A \<union> \<Union>B"
@@ -1017,7 +1017,7 @@
translations
"\<Union>x y. f" \<rightleftharpoons> "\<Union>x. \<Union>y. f"
- "\<Union>x. f" \<rightleftharpoons> "\<Union>CONST range (\<lambda>x. f)"
+ "\<Union>x. f" \<rightleftharpoons> "\<Union>(CONST range (\<lambda>x. f))"
"\<Union>x\<in>A. f" \<rightleftharpoons> "CONST Union ((\<lambda>x. f) ` A)"
text \<open>
@@ -1268,7 +1268,7 @@
proof -
from assms have "inj_on f A"
by (rule bij_betw_imp_inj_on)
- then have "inj_on f (\<Union>Pow A)"
+ then have "inj_on f (\<Union>(Pow A))"
by simp
then have "inj_on (image f) (Pow A)"
by (rule inj_on_image)
--- a/src/HOL/Library/Disjoint_Sets.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Library/Disjoint_Sets.thy Mon Jan 28 10:27:47 2019 +0100
@@ -169,7 +169,7 @@
qed
lemma disjoint_UN:
- assumes F: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)" and *: "disjoint_family_on (\<lambda>i. \<Union>F i) I"
+ assumes F: "\<And>i. i \<in> I \<Longrightarrow> disjoint (F i)" and *: "disjoint_family_on (\<lambda>i. \<Union>(F i)) I"
shows "disjoint (\<Union>i\<in>I. F i)"
proof (safe intro!: disjointI del: equalityI)
fix A B i j assume "A \<noteq> B" "A \<in> F i" "i \<in> I" "B \<in> F j" "j \<in> I"
@@ -179,7 +179,7 @@
by (auto dest: disjointD)
next
assume "i \<noteq> j"
- with * \<open>i\<in>I\<close> \<open>j\<in>I\<close> have "(\<Union>F i) \<inter> (\<Union>F j) = {}"
+ with * \<open>i\<in>I\<close> \<open>j\<in>I\<close> have "(\<Union>(F i)) \<inter> (\<Union>(F j)) = {}"
by (rule disjoint_family_onD)
with \<open>A\<in>F i\<close> \<open>i\<in>I\<close> \<open>B\<in>F j\<close> \<open>j\<in>I\<close>
show "A \<inter> B = {}"
--- a/src/HOL/Main.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Main.thy Mon Jan 28 10:27:47 2019 +0100
@@ -60,8 +60,8 @@
top ("\<top>") and
inf (infixl "\<sqinter>" 70) and
sup (infixl "\<squnion>" 65) and
- Inf ("\<Sqinter> _" [900] 900) and
- Sup ("\<Squnion> _" [900] 900) and
+ Inf ("\<Sqinter>") and
+ Sup ("\<Squnion>") and
ordLeq2 (infix "<=o" 50) and
ordLeq3 (infix "\<le>o" 50) and
ordLess2 (infix "<o" 50) and
--- a/src/HOL/Partial_Function.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/Partial_Function.thy Mon Jan 28 10:27:47 2019 +0100
@@ -32,15 +32,15 @@
show ?thesis
proof(cases "x \<le> \<Squnion>A")
case True
- have "\<Squnion>insert x A \<le> \<Squnion>A" using chain
+ have "\<Squnion>(insert x A) \<le> \<Squnion>A" using chain
by(rule ccpo_Sup_least)(auto simp add: True intro: ccpo_Sup_upper[OF chain'])
- hence "\<Squnion>insert x A = \<Squnion>A"
+ hence "\<Squnion>(insert x A) = \<Squnion>A"
by(rule antisym)(blast intro: ccpo_Sup_upper[OF chain] ccpo_Sup_least[OF chain'])
with \<open>\<Squnion>A \<in> A\<close> show ?thesis by simp
next
case False
with chainD[OF chain, of x "\<Squnion>A"] \<open>\<Squnion>A \<in> A\<close>
- have "\<Squnion>insert x A = x"
+ have "\<Squnion>(insert x A) = x"
by(auto intro: antisym ccpo_Sup_least[OF chain] order_trans[OF ccpo_Sup_upper[OF chain']] ccpo_Sup_upper[OF chain])
thus ?thesis by simp
qed
--- a/src/HOL/UNITY/Transformers.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/UNITY/Transformers.thy Mon Jan 28 10:27:47 2019 +0100
@@ -383,7 +383,7 @@
by (simp add: wens_single_finite_Suc [symmetric])
lemma wens_single_eq_Union:
- "wens_single act B = \<Union>range (wens_single_finite act B)"
+ "wens_single act B = \<Union>(range (wens_single_finite act B))"
by (simp add: wens_single_finite_def wens_single_def, blast)
lemma wens_single_finite_eq_Union:
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy Mon Jan 28 10:27:47 2019 +0100
@@ -26,7 +26,7 @@
text \<open>The set of variables of a term might be computed as follows.\<close>
fun term_vars :: "('a, 'b) term \<Rightarrow> 'b set" where
"term_vars (Var x) = {x}" |
- "term_vars (Fun f ts) = \<Union>set (map term_vars ts)"
+ "term_vars (Fun f ts) = \<Union>(set (map term_vars ts))"
text \<open>However, also for \emph{rules} (i.e., pairs of terms) and term
rewrite systems (i.e., sets of rules), the set of variables makes
--- a/src/HOL/ex/Perm_Fragments.thy Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/ex/Perm_Fragments.thy Mon Jan 28 10:27:47 2019 +0100
@@ -221,7 +221,7 @@
qed
lemma Union_orbits [simp]:
- "\<Union>orbits f = affected f"
+ "\<Union>(orbits f) = affected f"
by (auto simp add: orbits.simps intro: in_orbitsI in_orbit_affected)
lemma finite_orbits [simp]: