weaker precendence of syntax for big intersection and union on sets
authorhaftmann
Sat May 25 15:44:29 2013 +0200 (2013-05-25)
changeset 52141eff000cab70f
parent 52140 88a69da5d3fa
child 52148 893b15200ec1
weaker precendence of syntax for big intersection and union on sets
NEWS
src/HOL/BNF/BNF_Comp.thy
src/HOL/Complete_Lattices.thy
src/HOL/Hoare_Parallel/OG_Tran.thy
src/HOL/List.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Probability/Regularity.thy
     1.1 --- a/NEWS	Sat May 25 15:44:08 2013 +0200
     1.2 +++ b/NEWS	Sat May 25 15:44:29 2013 +0200
     1.3 @@ -57,6 +57,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Weaker precendence of syntax for big intersection and union on sets,
     1.8 +in accordance with corresponding lattice operations.  INCOMPATIBILITY.
     1.9 +
    1.10  * Nested case expressions are now translated in a separate check
    1.11    phase rather than during parsing. The data for case combinators
    1.12    is separated from the datatype package. The declaration attribute
     2.1 --- a/src/HOL/BNF/BNF_Comp.thy	Sat May 25 15:44:08 2013 +0200
     2.2 +++ b/src/HOL/BNF/BNF_Comp.thy	Sat May 25 15:44:29 2013 +0200
     2.3 @@ -24,7 +24,7 @@
     2.4    assumes fbd_Card_order: "Card_order fbd" and
     2.5      fset_bd: "\<And>x. |fset x| \<le>o fbd" and
     2.6      gset_bd: "\<And>x. |gset x| \<le>o gbd"
     2.7 -  shows "|\<Union>fset ` gset x| \<le>o gbd *c fbd"
     2.8 +  shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd"
     2.9  apply (subst sym[OF SUP_def])
    2.10  apply (rule ordLeq_transitive)
    2.11  apply (rule card_of_UNION_Sigma)
    2.12 @@ -42,10 +42,10 @@
    2.13  apply (rule Card_order_cprod)
    2.14  done
    2.15  
    2.16 -lemma Union_image_insert: "\<Union>f ` insert a B = f a \<union> \<Union>f ` B"
    2.17 +lemma Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)"
    2.18  by simp
    2.19  
    2.20 -lemma Union_image_empty: "A \<union> \<Union>f ` {} = A"
    2.21 +lemma Union_image_empty: "A \<union> \<Union>(f ` {}) = A"
    2.22  by simp
    2.23  
    2.24  lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F"
    2.25 @@ -54,10 +54,10 @@
    2.26  lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
    2.27  by blast
    2.28  
    2.29 -lemma UN_image_subset: "\<Union>f ` g x \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
    2.30 +lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
    2.31  by blast
    2.32  
    2.33 -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"
    2.34 +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"
    2.35  by (unfold o_apply collect_def SUP_def)
    2.36  
    2.37  lemma wpull_cong:
     3.1 --- a/src/HOL/Complete_Lattices.thy	Sat May 25 15:44:08 2013 +0200
     3.2 +++ b/src/HOL/Complete_Lattices.thy	Sat May 25 15:44:29 2013 +0200
     3.3 @@ -751,7 +751,7 @@
     3.4    "Inter S \<equiv> \<Sqinter>S"
     3.5    
     3.6  notation (xsymbols)
     3.7 -  Inter  ("\<Inter>_" [90] 90)
     3.8 +  Inter  ("\<Inter>_" [900] 900)
     3.9  
    3.10  lemma Inter_eq:
    3.11    "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
    3.12 @@ -934,7 +934,7 @@
    3.13    "Union S \<equiv> \<Squnion>S"
    3.14  
    3.15  notation (xsymbols)
    3.16 -  Union  ("\<Union>_" [90] 90)
    3.17 +  Union  ("\<Union>_" [900] 900)
    3.18  
    3.19  lemma Union_eq:
    3.20    "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
     4.1 --- a/src/HOL/Hoare_Parallel/OG_Tran.thy	Sat May 25 15:44:08 2013 +0200
     4.2 +++ b/src/HOL/Hoare_Parallel/OG_Tran.thy	Sat May 25 15:44:29 2013 +0200
     4.3 @@ -90,13 +90,13 @@
     4.4    "ann_sem c \<equiv> \<lambda>s. {t. (Some c, s) -*\<rightarrow> (None, t)}"
     4.5  
     4.6  definition ann_SEM :: "'a ann_com \<Rightarrow> 'a set \<Rightarrow> 'a set" where
     4.7 -  "ann_SEM c S \<equiv> \<Union>ann_sem c ` S"  
     4.8 +  "ann_SEM c S \<equiv> \<Union>(ann_sem c ` S)"
     4.9  
    4.10  definition sem :: "'a com \<Rightarrow> 'a \<Rightarrow> 'a set" where
    4.11    "sem c \<equiv> \<lambda>s. {t. \<exists>Ts. (c, s) -P*\<rightarrow> (Parallel Ts, t) \<and> All_None Ts}"
    4.12  
    4.13  definition SEM :: "'a com \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    4.14 -  "SEM c S \<equiv> \<Union>sem c ` S "
    4.15 +  "SEM c S \<equiv> \<Union>(sem c ` S)"
    4.16  
    4.17  abbreviation Omega :: "'a com"    ("\<Omega>" 63)
    4.18    where "\<Omega> \<equiv> While UNIV UNIV (Basic id)"
     5.1 --- a/src/HOL/List.thy	Sat May 25 15:44:08 2013 +0200
     5.2 +++ b/src/HOL/List.thy	Sat May 25 15:44:29 2013 +0200
     5.3 @@ -4312,7 +4312,7 @@
     5.4    moreover have "\<And>i. i \<in>Collect (?k_list k) \<Longrightarrow> card (A - set i) = card A - k"
     5.5      by (simp add: card_Diff_subset distinct_card)
     5.6    moreover have "{xs. ?k_list (Suc k) xs} =
     5.7 -      (\<lambda>(xs, n). n#xs) ` \<Union>(\<lambda>xs. {xs} \<times> (A - set xs)) ` {xs. ?k_list k xs}"
     5.8 +      (\<lambda>(xs, n). n#xs) ` \<Union>((\<lambda>xs. {xs} \<times> (A - set xs)) ` {xs. ?k_list k xs})"
     5.9      by (auto simp: length_Suc_conv)
    5.10    moreover
    5.11    have "Suc (card A - Suc k) = card A - k" using Suc.prems by simp
     6.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Sat May 25 15:44:08 2013 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sat May 25 15:44:29 2013 +0200
     6.3 @@ -1015,7 +1015,7 @@
     6.4      apply (rule that[of "d \<union> p"])
     6.5    proof -
     6.6      have *: "\<And>s f t. s \<noteq> {} \<Longrightarrow> (\<forall>i\<in>s. f i \<union> i = t) \<Longrightarrow> t = \<Inter> (f ` s) \<union> (\<Union>s)" by auto
     6.7 -    have *: "{a..b} = \<Inter> (\<lambda>i. \<Union>(q i - {i})) ` p \<union> \<Union>p"
     6.8 +    have *: "{a..b} = \<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p) \<union> \<Union>p"
     6.9        apply (rule *[OF False])
    6.10      proof
    6.11        fix i
    6.12 @@ -1032,7 +1032,7 @@
    6.13        fix k
    6.14        assume k: "k\<in>p"
    6.15        have *: "\<And>u t s. u \<subseteq> s \<Longrightarrow> s \<inter> t = {} \<Longrightarrow> u \<inter> t = {}" by auto
    6.16 -      show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<inter> interior k = {}"
    6.17 +      show "interior (\<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)) \<inter> interior k = {}"
    6.18          apply (rule *[of _ "interior (\<Union>(q k - {k}))"])
    6.19          defer
    6.20          apply (subst Int_commute)
    6.21 @@ -1044,7 +1044,7 @@
    6.22          show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}"
    6.23            using qk(5) using q(2)[OF k] by auto
    6.24          have *: "\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto
    6.25 -        show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<subseteq> interior (\<Union>(q k - {k}))"
    6.26 +        show "interior (\<Inter> ((\<lambda>i. \<Union>(q i - {i})) ` p)) \<subseteq> interior (\<Union>(q k - {k}))"
    6.27            apply (rule interior_mono *)+
    6.28            using k by auto
    6.29        qed
    6.30 @@ -1131,7 +1131,7 @@
    6.31  lemma elementary_union_interval: assumes "p division_of \<Union>p"
    6.32    obtains q where "q division_of ({a..b::'a::ordered_euclidean_space} \<union> \<Union>p)" proof-
    6.33    note assm=division_ofD[OF assms]
    6.34 -  have lem1:"\<And>f s. \<Union>\<Union> (f ` s) = \<Union>(\<lambda>x.\<Union>(f x)) ` s" by auto
    6.35 +  have lem1:"\<And>f s. \<Union>\<Union> (f ` s) = \<Union>((\<lambda>x.\<Union>(f x)) ` s)" by auto
    6.36    have lem2:"\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t |t. t \<in> f} = s \<union> \<Union>f" by auto
    6.37  { presume "p={} \<Longrightarrow> thesis" "{a..b} = {} \<Longrightarrow> thesis" "{a..b} \<noteq> {} \<Longrightarrow> interior {a..b} = {} \<Longrightarrow> thesis"
    6.38      "p\<noteq>{} \<Longrightarrow> interior {a..b}\<noteq>{} \<Longrightarrow> {a..b} \<noteq> {} \<Longrightarrow> thesis"
    6.39 @@ -1282,7 +1282,7 @@
    6.40  
    6.41  lemma division_of_tagged_division: assumes"s tagged_division_of i"  shows "(snd ` s) division_of i"
    6.42  proof(rule division_ofI) note assm=tagged_division_ofD[OF assms]
    6.43 -  show "\<Union>snd ` s = i" "finite (snd ` s)" using assm by auto
    6.44 +  show "\<Union>(snd ` s) = i" "finite (snd ` s)" using assm by auto
    6.45    fix k assume k:"k \<in> snd ` s" then obtain xk where xk:"(xk, k) \<in> s" by auto
    6.46    thus  "k \<subseteq> i" "k \<noteq> {}" "\<exists>a b. k = {a..b}" using assm apply- by fastforce+
    6.47    fix k' assume k':"k' \<in> snd ` s" "k \<noteq> k'" from this(1) obtain xk' where xk':"(xk', k') \<in> s" by auto
    6.48 @@ -1292,9 +1292,9 @@
    6.49  lemma partial_division_of_tagged_division: assumes "s tagged_partial_division_of i"
    6.50    shows "(snd ` s) division_of \<Union>(snd ` s)"
    6.51  proof(rule division_ofI) note assm=tagged_partial_division_ofD[OF assms]
    6.52 -  show "finite (snd ` s)" "\<Union>snd ` s = \<Union>snd ` s" using assm by auto
    6.53 +  show "finite (snd ` s)" "\<Union>(snd ` s) = \<Union>(snd ` s)" using assm by auto
    6.54    fix k assume k:"k \<in> snd ` s" then obtain xk where xk:"(xk, k) \<in> s" by auto
    6.55 -  thus "k\<noteq>{}" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>snd ` s" using assm by auto
    6.56 +  thus "k\<noteq>{}" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>(snd ` s)" using assm by auto
    6.57    fix k' assume k':"k' \<in> snd ` s" "k \<noteq> k'" from this(1) obtain xk' where xk':"(xk', k') \<in> s" by auto
    6.58    thus "interior k \<inter> interior k' = {}" apply-apply(rule assm(5)) apply(rule xk xk')+ using k' by auto
    6.59  qed
    6.60 @@ -1355,13 +1355,13 @@
    6.61    shows "\<Union>(pfn ` iset) tagged_division_of (\<Union>iset)"
    6.62  proof(rule tagged_division_ofI)
    6.63    note assm = tagged_division_ofD[OF assms(2)[rule_format]]
    6.64 -  show "finite (\<Union>pfn ` iset)" apply(rule finite_Union) using assms by auto
    6.65 -  have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>pfn ` iset} = \<Union>(\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` iset" by blast 
    6.66 +  show "finite (\<Union>(pfn ` iset))" apply(rule finite_Union) using assms by auto
    6.67 +  have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>((\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` iset)" by blast 
    6.68    also have "\<dots> = \<Union>iset" using assm(6) by auto
    6.69 -  finally show "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>pfn ` iset} = \<Union>iset" . 
    6.70 -  fix x k assume xk:"(x,k)\<in>\<Union>pfn ` iset" then obtain i where i:"i \<in> iset" "(x, k) \<in> pfn i" by auto
    6.71 +  finally show "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>iset" . 
    6.72 +  fix x k assume xk:"(x,k)\<in>\<Union>(pfn ` iset)" then obtain i where i:"i \<in> iset" "(x, k) \<in> pfn i" by auto
    6.73    show "x\<in>k" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>iset" using assm(2-4)[OF i] using i(1) by auto
    6.74 -  fix x' k' assume xk':"(x',k')\<in>\<Union>pfn ` iset" "(x, k) \<noteq> (x', k')" then obtain i' where i':"i' \<in> iset" "(x', k') \<in> pfn i'" by auto
    6.75 +  fix x' k' assume xk':"(x',k')\<in>\<Union>(pfn ` iset)" "(x, k) \<noteq> (x', k')" then obtain i' where i':"i' \<in> iset" "(x', k') \<in> pfn i'" by auto
    6.76    have *:"\<And>a b. i\<noteq>i' \<Longrightarrow> a\<subseteq> i \<Longrightarrow> b\<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}" using i(1) i'(1)
    6.77      using assms(3)[rule_format] interior_mono by blast
    6.78    show "interior k \<inter> interior k' = {}" apply(cases "i=i'")
    6.79 @@ -4975,7 +4975,7 @@
    6.80    shows "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x - integral k f) p) \<le> e" (is "?x \<le> e")
    6.81  proof-  { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" thus ?thesis by (blast intro: field_le_epsilon) }
    6.82    fix k::real assume k:"k>0" note p' = tagged_partial_division_ofD[OF p(1)]
    6.83 -  have "\<Union>snd ` p \<subseteq> {a..b}" using p'(3) by fastforce
    6.84 +  have "\<Union>(snd ` p) \<subseteq> {a..b}" using p'(3) by fastforce
    6.85    note partial_division_of_tagged_division[OF p(1)] this
    6.86    from partial_division_extend_interval[OF this] guess q . note q=this and q' = division_ofD[OF this(2)]
    6.87    def r \<equiv> "q - snd ` p" have "snd ` p \<inter> r = {}" unfolding r_def by auto
    6.88 @@ -4994,11 +4994,11 @@
    6.89      thus ?case apply(rule_tac x=qq in exI) using dd(2)[of qq] unfolding fine_inter uv by auto qed
    6.90    from bchoice[OF this] guess qq .. note qq=this[rule_format]
    6.91  
    6.92 -  let ?p = "p \<union> \<Union>qq ` r" have "norm ((\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) - integral {a..b} f) < e"
    6.93 +  let ?p = "p \<union> \<Union>(qq ` r)" have "norm ((\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) - integral {a..b} f) < e"
    6.94      apply(rule assms(4)[rule_format])
    6.95    proof show "d fine ?p" apply(rule fine_union,rule p) apply(rule fine_unions) using qq by auto 
    6.96      note * = tagged_partial_division_of_union_self[OF p(1)]
    6.97 -    have "p \<union> \<Union>qq ` r tagged_division_of \<Union>snd ` p \<union> \<Union>r"
    6.98 +    have "p \<union> \<Union>(qq ` r) tagged_division_of \<Union>(snd ` p) \<union> \<Union>r"
    6.99      proof(rule tagged_division_union[OF * tagged_division_unions])
   6.100        show "finite r" by fact case goal2 thus ?case using qq by auto
   6.101      next case goal3 thus ?case apply(rule,rule,rule) apply(rule q'(5)) unfolding r_def by auto
   6.102 @@ -5006,11 +5006,11 @@
   6.103          apply(rule,rule q') defer apply(rule,subst Int_commute) 
   6.104          apply(rule inter_interior_unions_intervals) apply(rule finite_imageI,rule p',rule) defer
   6.105          apply(rule,rule q') using q(1) p' unfolding r_def by auto qed
   6.106 -    moreover have "\<Union>snd ` p \<union> \<Union>r = {a..b}" "{qq i |i. i \<in> r} = qq ` r"
   6.107 +    moreover have "\<Union>(snd ` p) \<union> \<Union>r = {a..b}" "{qq i |i. i \<in> r} = qq ` r"
   6.108        unfolding Union_Un_distrib[THEN sym] r_def using q by auto
   6.109      ultimately show "?p tagged_division_of {a..b}" by fastforce qed
   6.110  
   6.111 -  hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>\<Union>qq ` r. content k *\<^sub>R f x) -
   6.112 +  hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>\<Union>(qq ` r). content k *\<^sub>R f x) -
   6.113      integral {a..b} f) < e" apply(subst setsum_Un_zero[THEN sym]) apply(rule p') prefer 3 
   6.114      apply assumption apply rule apply(rule finite_imageI,rule r) apply safe apply(drule qq)
   6.115    proof- fix x l k assume as:"(x,l)\<in>p" "(x,l)\<in>qq k" "k\<in>r"
     7.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat May 25 15:44:08 2013 +0200
     7.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat May 25 15:44:29 2013 +0200
     7.3 @@ -220,7 +220,7 @@
     7.4      fix a assume "a \<in> A"
     7.5      thus "x \<in> a" "open a" using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into)
     7.6    next
     7.7 -    let ?int = "\<lambda>N. \<Inter>from_nat_into A' ` N"
     7.8 +    let ?int = "\<lambda>N. \<Inter>(from_nat_into A' ` N)"
     7.9      fix a b assume "a \<in> A" "b \<in> A"
    7.10      then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)" by (auto simp: A_def)
    7.11      thus "a \<inter> b \<in> A" by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"])
    7.12 @@ -2617,7 +2617,7 @@
    7.13  proof (safe intro!: compact_eq_heine_borel[THEN iffD2])
    7.14    fix A assume "compact U" and A: "\<forall>a\<in>A. closed a" "U \<inter> \<Inter>A = {}"
    7.15      and fi: "\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}"
    7.16 -  from A have "(\<forall>a\<in>uminus`A. open a) \<and> U \<subseteq> \<Union>uminus`A"
    7.17 +  from A have "(\<forall>a\<in>uminus`A. open a) \<and> U \<subseteq> \<Union>(uminus`A)"
    7.18      by auto
    7.19    with `compact U` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<subseteq> \<Union>(uminus`B)"
    7.20      unfolding compact_eq_heine_borel by (metis subset_image_iff)
    7.21 @@ -2627,7 +2627,7 @@
    7.22    fix A assume ?R and cover: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A"
    7.23    from cover have "U \<inter> \<Inter>(uminus`A) = {}" "\<forall>a\<in>uminus`A. closed a"
    7.24      by auto
    7.25 -  with `?R` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<inter> \<Inter>uminus`B = {}"
    7.26 +  with `?R` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<inter> \<Inter>(uminus`B) = {}"
    7.27      by (metis subset_image_iff)
    7.28    then show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
    7.29      by  (auto intro!: exI[of _ B] inj_setminus dest: finite_imageD)
    7.30 @@ -3041,7 +3041,7 @@
    7.31    assumes "seq_compact s"
    7.32    shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))"
    7.33  proof(rule, rule, rule ccontr)
    7.34 -  fix e::real assume "e>0" and assm:"\<not> (\<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k)"
    7.35 +  fix e::real assume "e>0" and assm:"\<not> (\<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>((\<lambda>x. ball x e) ` k))"
    7.36    def x \<equiv> "helper_1 s e"
    7.37    { fix n
    7.38      have "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)"
    7.39 @@ -4586,7 +4586,7 @@
    7.40      moreover with c have "(\<Inter>y\<in>D. a y) \<times> t \<subseteq> (\<Union>y\<in>D. c y)"
    7.41        by (fastforce simp: subset_eq)
    7.42      ultimately show "\<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)"
    7.43 -      using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>a`D"] conjI) (auto intro!: open_INT)
    7.44 +      using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>(a`D)"] conjI) (auto intro!: open_INT)
    7.45    qed
    7.46    then obtain a d where a: "\<forall>x\<in>s. open (a x)" "s \<subseteq> (\<Union>x\<in>s. a x)"
    7.47      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"
     8.1 --- a/src/HOL/Probability/Caratheodory.thy	Sat May 25 15:44:08 2013 +0200
     8.2 +++ b/src/HOL/Probability/Caratheodory.thy	Sat May 25 15:44:29 2013 +0200
     8.3 @@ -707,9 +707,9 @@
     8.4    assumes A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" "disjoint_family_on A I" "finite I" "UNION I A \<in> M"
     8.5    shows "f (UNION I A) = (\<Sum>i\<in>I. f (A i))"
     8.6  proof -
     8.7 -  have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>A`I \<in> M"
     8.8 +  have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>(A`I) \<in> M"
     8.9      using A unfolding SUP_def by (auto simp: disjoint_family_on_disjoint_image)
    8.10 -  with `volume M f` have "f (\<Union>A`I) = (\<Sum>a\<in>A`I. f a)"
    8.11 +  with `volume M f` have "f (\<Union>(A`I)) = (\<Sum>a\<in>A`I. f a)"
    8.12      unfolding volume_def by blast
    8.13    also have "\<dots> = (\<Sum>i\<in>I. f (A i))"
    8.14    proof (subst setsum_reindex_nonzero)
     9.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Sat May 25 15:44:08 2013 +0200
     9.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Sat May 25 15:44:29 2013 +0200
     9.3 @@ -571,9 +571,9 @@
     9.4      show "(SUP i. emeasure M (?O i)) \<le> ?a" unfolding SUP_def
     9.5      proof (safe intro!: Sup_mono, unfold bex_simps)
     9.6        fix i
     9.7 -      have *: "(\<Union>Q' ` {..i}) = ?O i" by auto
     9.8 +      have *: "(\<Union>(Q' ` {..i})) = ?O i" by auto
     9.9        then show "\<exists>x. (x \<in> sets M \<and> N x \<noteq> \<infinity>) \<and>
    9.10 -        emeasure M (\<Union>Q' ` {..i}) \<le> emeasure M x"
    9.11 +        emeasure M (\<Union>(Q' ` {..i})) \<le> emeasure M x"
    9.12          using O_in_G[of i] by (auto intro!: exI[of _ "?O i"])
    9.13      qed
    9.14    qed
    10.1 --- a/src/HOL/Probability/Regularity.thy	Sat May 25 15:44:08 2013 +0200
    10.2 +++ b/src/HOL/Probability/Regularity.thy	Sat May 25 15:44:29 2013 +0200
    10.3 @@ -209,8 +209,8 @@
    10.4        from nat_approx_posE[OF this] guess n . note n = this
    10.5        let ?k = "from_nat_into X ` {0..k e (Suc n)}"
    10.6        have "finite ?k" by simp
    10.7 -      moreover have "K \<subseteq> \<Union>(\<lambda>x. ball x e') ` ?k" unfolding K_def B_def using n by force
    10.8 -      ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>(\<lambda>x. ball x e') ` k" by blast
    10.9 +      moreover have "K \<subseteq> \<Union>((\<lambda>x. ball x e') ` ?k)" unfolding K_def B_def using n by force
   10.10 +      ultimately show "\<exists>k. finite k \<and> K \<subseteq> \<Union>((\<lambda>x. ball x e') ` k)" by blast
   10.11      qed
   10.12      ultimately
   10.13      show "?thesis e " by (auto simp: sU)