src/HOL/Probability/Caratheodory.thy

--- a/src/HOL/Probability/Caratheodory.thy	Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Caratheodory.thy	Wed Feb 17 21:51:56 2016 +0100
@@ -396,8 +396,8 @@
   from \<open>outer_measure M f X \<noteq> \<infinity>\<close> have fin: "\<bar>outer_measure M f X\<bar> \<noteq> \<infinity>"
     using outer_measure_nonneg[OF posf, of X] by auto
   show ?thesis
-    using Inf_ereal_close[OF fin[unfolded outer_measure_def INF_def], OF \<open>0 < e\<close>]
-    unfolding INF_def[symmetric] outer_measure_def[symmetric] by (auto intro: less_imp_le)
+    using Inf_ereal_close [OF fin [unfolded outer_measure_def], OF \<open>0 < e\<close>]
+    by (auto intro: less_imp_le simp add: outer_measure_def)
 qed
 
 lemma (in ring_of_sets) countably_subadditive_outer_measure:
@@ -574,7 +574,7 @@
   shows "f (UNION I A) = (\<Sum>i\<in>I. f (A i))"
 proof -
   have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>(A`I) \<in> M"
-    using A unfolding SUP_def by (auto simp: disjoint_family_on_disjoint_image)
+    using A by (auto simp: disjoint_family_on_disjoint_image)
   with \<open>volume M f\<close> have "f (\<Union>(A`I)) = (\<Sum>a\<in>A`I. f a)"
     unfolding volume_def by blast
   also have "\<dots> = (\<Sum>i\<in>I. f (A i))"
@@ -713,7 +713,7 @@
     then have "disjoint_family F"
       using F'_disj by (auto simp: disjoint_family_on_def)
     moreover from F' have "(\<Union>i. F i) = \<Union>C"
-      by (auto simp: F_def set_eq_iff split: split_if_asm)
+      by (auto simp add: F_def split: split_if_asm) blast
     moreover have sets_F: "\<And>i. F i \<in> M"
       using F' sets_C by (auto simp: F_def)
     moreover note sets_C
@@ -783,9 +783,10 @@
           by (auto simp: disjoint_family_on_def f_def)
         moreover
         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])
+          using f C Ai unfolding bij_betw_def by auto
         then have "\<Union>range f = A i"
-          using f C Ai unfolding bij_betw_def by (auto simp: f_def)
+          using f C Ai unfolding bij_betw_def
+            by (auto simp add: f_def cong del: strong_SUP_cong)
         moreover 
         { have "(\<Sum>j. \<mu>_r (f j)) = (\<Sum>j. if j \<in> {..< card C} then \<mu>_r (f j) else 0)"
             using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def)
@@ -841,7 +842,7 @@
     have "(\<Sum>n. \<mu>_r (A' n)) = (\<Sum>n. \<Sum>c\<in>C'. \<mu>_r (A' n \<inter> c))"
       using C' A'
       by (subst volume_finite_additive[symmetric, OF V(1)])
-         (auto simp: disjoint_def disjoint_family_on_def Union_image_eq[symmetric] simp del: Sup_image_eq Union_image_eq
+         (auto simp: disjoint_def disjoint_family_on_def
                intro!: G.Int G.finite_Union arg_cong[where f="\<lambda>X. suminf (\<lambda>i. \<mu>_r (X i))"] ext
                intro: generated_ringI_Basic)
     also have "\<dots> = (\<Sum>c\<in>C'. \<Sum>n. \<mu>_r (A' n \<inter> c))"
@@ -853,7 +854,7 @@
     also have "\<dots> = \<mu>_r (\<Union>C')"
       using C' Un_A
       by (subst volume_finite_additive[symmetric, OF V(1)])
-         (auto simp: disjoint_family_on_def disjoint_def Union_image_eq[symmetric] simp del: Sup_image_eq Union_image_eq 
+         (auto simp: disjoint_family_on_def disjoint_def
                intro: generated_ringI_Basic)
     finally show "(\<Sum>n. \<mu>_r (A' n)) = \<mu>_r (\<Union>i. A' i)"
       using C' by simp