# HG changeset patch
# User wenzelm
# Date 1506717958 -7200
# Node ID 18cc87e2335f9087e6f3747b3b8dc0ae57a89b39
# Parent  676258a1cf01efab9d9755d361594637ceb7ee12# Parent  9c661b74ce9230b17e4379242b49fca76d320290
merged

diff -r 9c661b74ce92 -r 18cc87e2335f src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri Sep 29 22:43:29 2017 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri Sep 29 22:45:58 2017 +0200
@@ -3749,12 +3749,14 @@
     by meson
   have exy: "\<exists>y. ((\<lambda>x. inverse (\<gamma> x - z) * ?D\<gamma> x) has_integral y) {a..b}"
     unfolding integrable_on_def [symmetric]
-    apply (rule contour_integral_local_primitive_any [OF piecewise_C1_imp_differentiable [OF \<gamma>], of "-{z}"])
-    apply (rename_tac w)
-    apply (rule_tac x="norm(w - z)" in exI)
-    apply (simp_all add: inverse_eq_divide)
-    apply (metis has_field_derivative_at_within h)
-    done
+  proof (rule contour_integral_local_primitive_any [OF piecewise_C1_imp_differentiable [OF \<gamma>]])
+    show "\<exists>d h. 0 < d \<and>
+               (\<forall>y. cmod (y - w) < d \<longrightarrow> (h has_field_derivative inverse (y - z))(at y within - {z}))" 
+          if "w \<in> - {z}" for w
+      apply (rule_tac x="norm(w - z)" in exI)
+      using that inverse_eq_divide has_field_derivative_at_within h
+      by (metis Compl_insert DiffD2 insertCI right_minus_eq zero_less_norm_iff)
+  qed simp
   have vg_int: "(\<lambda>x. ?D\<gamma> x / (\<gamma> x - z)) integrable_on {a..b}"
     unfolding box_real [symmetric] divide_inverse_commute
     by (auto intro!: exy integrable_subinterval simp add: integrable_on_def ab)
@@ -3774,20 +3776,29 @@
       assume x: "x \<notin> k" "a < x" "x < b"
       then have "x \<in> interior ({a..b} - k)"
         using open_subset_interior [OF o] by fastforce
-      then have con: "isCont (\<lambda>x. ?D\<gamma> x) x"
+      then have con: "isCont ?D\<gamma> x"
         using g_C1_diff x by (auto simp: C1_differentiable_on_eq intro: continuous_on_interior)
       then have con_vd: "continuous (at x within {a..b}) (\<lambda>x. ?D\<gamma> x)"
         by (rule continuous_at_imp_continuous_within)
       have gdx: "\<gamma> differentiable at x"
         using x by (simp add: g_diff_at)
-      have "((\<lambda>c. exp (- integral {a..c} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))) * (\<gamma> c - z)) has_derivative (\<lambda>h. 0))
+      have "\<And>d. \<lbrakk>x \<notin> k; a < x; x < b;
+          (\<gamma> has_vector_derivative d) (at x); a \<le> t; t \<le> b\<rbrakk>
+         \<Longrightarrow> ((\<lambda>x. integral {a..x}
+                     (\<lambda>x. ?D\<gamma> x /
+                           (\<gamma> x - z))) has_vector_derivative
+              d / (\<gamma> x - z))
+              (at x within {a..b})"
+        apply (rule has_vector_derivative_eq_rhs)
+         apply (rule integral_has_vector_derivative_continuous_at [where S = "{}", simplified])
+        apply (rule con_vd continuous_intros cong vg_int | simp add: continuous_at_imp_continuous_within has_vector_derivative_continuous vector_derivative_at)+
+        done
+      then have "((\<lambda>c. exp (- integral {a..c} (\<lambda>x. ?D\<gamma> x / (\<gamma> x - z))) * (\<gamma> c - z)) has_derivative (\<lambda>h. 0))
           (at x within {a..b})"
         using x gdx t
         apply (clarsimp simp add: differentiable_iff_scaleR)
         apply (rule exp_fg [unfolded has_vector_derivative_def, simplified], blast intro: has_derivative_at_within)
         apply (simp_all add: has_vector_derivative_def [symmetric])
-        apply (rule has_vector_derivative_eq_rhs [OF integral_has_vector_derivative_continuous_at])
-        apply (rule con_vd continuous_intros cong vg_int | simp add: continuous_at_imp_continuous_within has_vector_derivative_continuous vector_derivative_at)+
         done
       } note * = this
     have "exp (- (integral {a..t} (\<lambda>x. ?D\<gamma> x / (\<gamma> x - z)))) * (\<gamma> t - z) =\<gamma> a - z"
diff -r 9c661b74ce92 -r 18cc87e2335f src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Sep 29 22:43:29 2017 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Sep 29 22:45:58 2017 +0200
@@ -2253,9 +2253,7 @@
     have "(\<lambda>x. \<bar>f x \<bullet> i\<bar>) integrable_on S" 
       using assms integrable_component [OF fcomp, where y=i] that by simp
     then have "(\<lambda>x. f x \<bullet> i) absolutely_integrable_on S"
-      apply -
-      apply (rule abs_absolutely_integrableI_1, auto)
-      by (simp add: f integrable_component)
+      using abs_absolutely_integrableI_1 f integrable_component by blast
     then show ?thesis
       by (rule absolutely_integrable_scaleR_right)
   qed
diff -r 9c661b74ce92 -r 18cc87e2335f src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Sep 29 22:43:29 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Sep 29 22:45:58 2017 +0200
@@ -10,10 +10,6 @@
   Lebesgue_Measure Tagged_Division
 begin
 
-(*FIXME DELETE*)
-lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
-(* try instead structured proofs below *)
-
 lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
   \<Longrightarrow> norm(y-x) \<le> e"
   using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"]
@@ -1541,14 +1537,6 @@
     using \<gamma> [OF p \<open>\<gamma> fine p\<close>] rsum_bound[OF p] assms by metis
 qed
 
-corollary has_integral_bound_real:
-  fixes f :: "real \<Rightarrow> 'b::real_normed_vector"
-  assumes "0 \<le> B"
-      and "(f has_integral i) {a..b}"
-      and "\<forall>x\<in>{a..b}. norm (f x) \<le> B"
-    shows "norm i \<le> B * content {a..b}"
-  by (metis assms box_real(2) has_integral_bound)
-
 corollary integrable_bound:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes "0 \<le> B"
@@ -2384,6 +2372,31 @@
   shows "g integrable_on T"
   using assms has_integral_spike_finite by blast
 
+lemma has_integral_bound_spike_finite:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
+  assumes "0 \<le> B" "finite S"
+      and f: "(f has_integral i) (cbox a b)"
+      and leB: "\<And>x. x \<in> cbox a b - S \<Longrightarrow> norm (f x) \<le> B"
+    shows "norm i \<le> B * content (cbox a b)"
+proof -
+  define g where "g \<equiv> (\<lambda>x. if x \<in> S then 0 else f x)"
+  then have "\<And>x. x \<in> cbox a b - S \<Longrightarrow> norm (g x) \<le> B"
+    using leB by simp
+  moreover have "(g has_integral i) (cbox a b)"
+    using has_integral_spike_finite [OF \<open>finite S\<close> _ f]
+    by (simp add: g_def)
+  ultimately show ?thesis
+    by (simp add: \<open>0 \<le> B\<close> g_def has_integral_bound)
+qed
+
+corollary has_integral_bound_real:
+  fixes f :: "real \<Rightarrow> 'b::real_normed_vector"
+  assumes "0 \<le> B" "finite S"
+      and "(f has_integral i) {a..b}"
+      and "\<And>x. x \<in> {a..b} - S \<Longrightarrow> norm (f x) \<le> B"
+    shows "norm i \<le> B * content {a..b}"
+  by (metis assms box_real(2) has_integral_bound_spike_finite)
+
 
 subsection \<open>In particular, the boundary of an interval is negligible.\<close>
 
@@ -3049,17 +3062,18 @@
 lemma integral_has_vector_derivative_continuous_at:
   fixes f :: "real \<Rightarrow> 'a::banach"
   assumes f: "f integrable_on {a..b}"
-      and x: "x \<in> {a..b}"
-      and fx: "continuous (at x within {a..b}) f"
-  shows "((\<lambda>u. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})"
+     and x: "x \<in> {a..b} - S"
+     and "finite S"
+     and fx: "continuous (at x within ({a..b} - S)) f"
+ shows "((\<lambda>u. integral {a..u} f) has_vector_derivative f x) (at x within ({a..b} - S))"
 proof -
   let ?I = "\<lambda>a b. integral {a..b} f"
   { fix e::real
     assume "e > 0"
-    obtain d where "d>0" and d: "\<And>x'. \<lbrakk>x' \<in> {a..b}; \<bar>x' - x\<bar> < d\<rbrakk> \<Longrightarrow> norm(f x' - f x) \<le> e"
+    obtain d where "d>0" and d: "\<And>x'. \<lbrakk>x' \<in> {a..b} - S; \<bar>x' - x\<bar> < d\<rbrakk> \<Longrightarrow> norm(f x' - f x) \<le> e"
       using \<open>e>0\<close> fx by (auto simp: continuous_within_eps_delta dist_norm less_imp_le)
     have "norm (integral {a..y} f - integral {a..x} f - (y-x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
-           if y: "y \<in> {a..b}" and yx: "\<bar>y - x\<bar> < d" for y
+           if y: "y \<in> {a..b} - S" and yx: "\<bar>y - x\<bar> < d" for y
     proof (cases "y < x")
       case False
       have "f integrable_on {a..y}"
@@ -3070,14 +3084,15 @@
         apply (rule has_integral_diff)
         using x y apply (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]])
         using has_integral_const_real [of "f x" x y] False
-        apply (simp add: )
+        apply simp
         done
+      have "\<And>xa. y - x < d \<Longrightarrow> (\<And>x'. a \<le> x' \<and> x' \<le> b \<and> x' \<notin> S \<Longrightarrow> \<bar>x' - x\<bar> < d \<Longrightarrow> norm (f x' - f x) \<le> e) \<Longrightarrow> 0 < e \<Longrightarrow> xa \<notin> S \<Longrightarrow> a \<le> x \<Longrightarrow> x \<notin> S \<Longrightarrow> y \<le> b \<Longrightarrow> y \<notin> S \<Longrightarrow> x \<le> xa \<Longrightarrow> xa \<le> y \<Longrightarrow> norm (f xa - f x) \<le> e"
+        using assms by auto
       show ?thesis
         using False
         apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc)
         apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
-        using yx False d x y \<open>e>0\<close> apply (auto simp add: Idiff fux_int)
-        done
+        using yx False d x y \<open>e>0\<close> assms by (auto simp: Idiff fux_int)
     next
       case True
       have "f integrable_on {a..x}"
@@ -3088,33 +3103,31 @@
         apply (rule has_integral_diff)
         using x y apply (auto intro: integrable_integral [OF integrable_subinterval_real [OF f]])
         using has_integral_const_real [of "f x" y x] True
-        apply (simp add: )
+        apply simp
         done
       have "norm (integral {a..x} f - integral {a..y} f - (x - y) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
         using True
         apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc)
         apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
-        using yx True d x y \<open>e>0\<close> apply (auto simp add: Idiff fux_int)
-        done
+        using yx True d x y \<open>e>0\<close> assms by (auto simp: Idiff fux_int)
       then show ?thesis
         by (simp add: algebra_simps norm_minus_commute)
     qed
-    then have "\<exists>d>0. \<forall>y\<in>{a..b}. \<bar>y - x\<bar> < d \<longrightarrow> norm (integral {a..y} f - integral {a..x} f - (y-x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
+    then have "\<exists>d>0. \<forall>y\<in>{a..b} - S. \<bar>y - x\<bar> < d \<longrightarrow> norm (integral {a..y} f - integral {a..x} f - (y-x) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
       using \<open>d>0\<close> by blast
   }
   then show ?thesis
     by (simp add: has_vector_derivative_def has_derivative_within_alt bounded_linear_scaleR_left)
 qed
 
+
 lemma integral_has_vector_derivative:
   fixes f :: "real \<Rightarrow> 'a::banach"
   assumes "continuous_on {a..b} f"
     and "x \<in> {a..b}"
   shows "((\<lambda>u. integral {a..u} f) has_vector_derivative f(x)) (at x within {a..b})"
-apply (rule integral_has_vector_derivative_continuous_at [OF integrable_continuous_real])
-using assms
-apply (auto simp: continuous_on_eq_continuous_within)
-done
+using assms integral_has_vector_derivative_continuous_at [OF integrable_continuous_real]
+  by (fastforce simp: continuous_on_eq_continuous_within)
 
 lemma antiderivative_continuous:
   fixes q b :: real
@@ -6049,8 +6062,7 @@
   have "norm (integral S f) \<le> integral S ((\<lambda>x. x \<bullet> k) \<circ> g)"
     apply (rule integral_norm_bound_integral[OF f integrable_linear[OF g]])
     apply (simp add: bounded_linear_inner_left)
-    unfolding o_def
-    apply (metis fg)
+    apply (metis fg o_def)
     done
   then show ?thesis
     unfolding o_def integral_component_eq[OF g] .
@@ -6167,7 +6179,6 @@
       have "closed_segment x0 x \<subseteq> U"
         by (rule \<open>convex U\<close>[unfolded convex_contains_segment, rule_format, OF \<open>x0 \<in> U\<close> \<open>x \<in> U\<close>])
       from elim have [intro]: "x \<in> U" by auto
-
       have "?F x - ?F x0 - ?dF (x - x0) =
         integral (cbox a b) (\<lambda>y. f x y - f x0 y - fx x0 y (x - x0))"
         (is "_ = ?id")
@@ -6204,7 +6215,7 @@
       also have "\<dots> < e' * norm (x - x0)"
         using \<open>e' > 0\<close>
         apply (intro mult_strict_right_mono[OF _ \<open>0 < norm (x - x0)\<close>])
-        apply  (auto simp: divide_simps e_def)
+        apply (auto simp: divide_simps e_def)
         by (metis \<open>0 < e\<close> e_def order.asym zero_less_divide_iff)
       finally have "norm (?F x - ?F x0 - ?dF (x - x0)) < e' * norm (x - x0)" .
       then show ?case
@@ -6293,14 +6304,12 @@
     by atomize_elim (auto simp: integrable_on_def intro!: choice)
 
   moreover
-
   have gi[simp]: "g integrable_on (cbox a b)"
     by (auto intro!: integrable_continuous uniform_limit_theorem[OF _ u] eventuallyI c)
   then obtain J where J: "(g has_integral J) (cbox a b)"
     by blast
 
   moreover
-
   have "(I \<longlongrightarrow> J) F"
   proof cases
     assume "content (cbox a b) = 0"
@@ -6432,7 +6441,6 @@
 
 subsection \<open>Integration by substitution\<close>
 
-
 lemma has_integral_substitution_general:
   fixes f :: "real \<Rightarrow> 'a::euclidean_space" and g :: "real \<Rightarrow> real"
   assumes s: "finite s" and le: "a \<le> b"
@@ -6449,20 +6457,17 @@
           f integrable_continuous_real)+
   have deriv: "(((\<lambda>x. integral {c..x} f) \<circ> g) has_vector_derivative g' x *\<^sub>R f (g x))
                  (at x within {a..b})" if "x \<in> {a..b} - s" for x
-    apply (rule has_vector_derivative_eq_rhs)
-    apply (rule vector_diff_chain_within)
-    apply (subst has_field_derivative_iff_has_vector_derivative [symmetric])
-    apply (rule deriv that)+
-    apply (rule has_vector_derivative_within_subset)
-    apply (rule integral_has_vector_derivative f)+
-    using that le subset
-    apply blast+
-    done
+  proof (rule has_vector_derivative_eq_rhs [OF vector_diff_chain_within refl])
+    show "(g has_vector_derivative g' x) (at x within {a..b})"
+      using deriv has_field_derivative_iff_has_vector_derivative that by blast
+    show "((\<lambda>x. integral {c..x} f) has_vector_derivative f (g x)) 
+          (at (g x) within g ` {a..b})"
+      using that le subset
+      by (blast intro: has_vector_derivative_within_subset integral_has_vector_derivative f)
+  qed
   have deriv: "(?F has_vector_derivative g' x *\<^sub>R f (g x))
                   (at x)" if "x \<in> {a..b} - (s \<union> {a,b})" for x
     using deriv[of x] that by (simp add: at_within_closed_interval o_def)
-
-
   have "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (?F b - ?F a)) {a..b}"
     using le cont_int s deriv cont_int
     by (intro fundamental_theorem_of_calculus_interior_strong[of "s \<union> {a,b}"]) simp_all
@@ -6794,20 +6799,21 @@
             \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX"
         by (rule norm_xx [OF integral_Pair_const 1 2])
     } note * = this
-    show "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e"
+    have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e" 
+      if "\<forall>x\<in>?CBOX. \<forall>x'\<in>?CBOX. norm (x' - x) < k \<longrightarrow> norm (f x' - f x) < e /(2 * content (?CBOX))" "0 < k" for k
+    proof -
+      obtain p where ptag: "p tagged_division_of cbox (a, c) (b, d)" 
+                 and fine: "(\<lambda>x. ball x k) fine p"
+        using fine_division_exists \<open>0 < k\<close> by blast
+      show ?thesis
+        apply (rule op_acbd [OF division_of_tagged_division [OF ptag]])
+        using that fine ptag \<open>0 < k\<close> by (auto simp: *)
+    qed
+    then show "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e"
       using compact_uniformly_continuous [OF assms compact_cbox]
       apply (simp add: uniformly_continuous_on_def dist_norm)
       apply (drule_tac x="e/2 / content?CBOX" in spec)
-      using cbp \<open>0 < e\<close>
-      apply (auto simp: zero_less_mult_iff)
-      apply (rename_tac k)
-      apply (rule_tac e1=k in fine_division_exists [OF gauge_ball, where a = "(a,c)" and b = "(b,d)"])
-      apply assumption
-      apply (rule op_acbd)
-      apply (erule division_of_tagged_division)
-      using *
-      apply auto
-      done
+      using cbp \<open>0 < e\<close> by (auto simp: zero_less_mult_iff)
   qed
   then show ?thesis
     by simp
@@ -6850,7 +6856,6 @@
   shows   "((\<lambda>x::real. exp (-a*x)) has_integral exp (-a*c)/a) {c..}"
 proof -
   define f where "f = (\<lambda>k x. if x \<in> {c..real k} then exp (-a*x) else 0)"
-
   {
     fix k :: nat assume k: "of_nat k \<ge> c"
     from k a
diff -r 9c661b74ce92 -r 18cc87e2335f src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Fri Sep 29 22:43:29 2017 +0200
+++ b/src/HOL/Analysis/Homeomorphism.thy	Fri Sep 29 22:45:58 2017 +0200
@@ -827,7 +827,7 @@
   fixes a :: "'a :: euclidean_space"
   assumes "0 < r" "b \<in> sphere a r" "affine T" "a \<in> T" "b \<in> T" "affine p"
       and aff: "aff_dim T = aff_dim p + 1"
-    shows "((sphere a r \<inter> T) - {b}) homeomorphic p"
+    shows "(sphere a r \<inter> T) - {b} homeomorphic p"
 proof -
   have "a \<noteq> b" using assms by auto
   then have inj: "inj (\<lambda>x::'a. x /\<^sub>R norm (a - b))"
@@ -847,6 +847,23 @@
   finally show ?thesis .
 qed
 
+corollary homeomorphic_punctured_sphere_affine:
+  fixes a :: "'a :: euclidean_space"
+  assumes "0 < r" and b: "b \<in> sphere a r"
+      and "affine T" and affS: "aff_dim T + 1 = DIM('a)"
+    shows "(sphere a r - {b}) homeomorphic T"
+  using homeomorphic_punctured_affine_sphere_affine [of r b a UNIV T] assms by auto
+
+corollary homeomorphic_punctured_sphere_hyperplane:
+  fixes a :: "'a :: euclidean_space"
+  assumes "0 < r" and b: "b \<in> sphere a r"
+      and "c \<noteq> 0"
+    shows "(sphere a r - {b}) homeomorphic {x::'a. c \<bullet> x = d}"
+apply (rule homeomorphic_punctured_sphere_affine)
+using assms
+apply (auto simp: affine_hyperplane of_nat_diff)
+done
+
 proposition homeomorphic_punctured_sphere_affine_gen:
   fixes a :: "'a :: euclidean_space"
   assumes "convex S" "bounded S" and a: "a \<in> rel_frontier S"
@@ -892,24 +909,6 @@
   finally show ?thesis .
 qed
 
-corollary homeomorphic_punctured_sphere_affine:
-  fixes a :: "'a :: euclidean_space"
-  assumes "0 < r" and b: "b \<in> sphere a r"
-      and "affine T" and affS: "aff_dim T + 1 = DIM('a)"
-    shows "(sphere a r - {b}) homeomorphic T"
-using homeomorphic_punctured_sphere_affine_gen [of "cball a r" b T]
-  assms aff_dim_cball by force
-
-corollary homeomorphic_punctured_sphere_hyperplane:
-  fixes a :: "'a :: euclidean_space"
-  assumes "0 < r" and b: "b \<in> sphere a r"
-      and "c \<noteq> 0"
-    shows "(sphere a r - {b}) homeomorphic {x::'a. c \<bullet> x = d}"
-apply (rule homeomorphic_punctured_sphere_affine)
-using assms
-apply (auto simp: affine_hyperplane of_nat_diff)
-done
-
 
 text\<open> When dealing with AR, ANR and ANR later, it's useful to know that every set
   is homeomorphic to a closed subset of a convex set, and
diff -r 9c661b74ce92 -r 18cc87e2335f src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Fri Sep 29 22:43:29 2017 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy	Fri Sep 29 22:45:58 2017 +0200
@@ -1919,89 +1919,71 @@
 
 lemma interval_bisection_step:
   fixes type :: "'a::euclidean_space"
-  assumes "P {}"
-    and "\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P (s \<union> t)"
-    and "\<not> P (cbox a (b::'a))"
+  assumes emp: "P {}"
+    and Un: "\<And>S T. \<lbrakk>P S; P T; interior(S) \<inter> interior(T) = {}\<rbrakk> \<Longrightarrow> P (S \<union> T)"
+    and non: "\<not> P (cbox a (b::'a))"
   obtains c d where "\<not> P (cbox c d)"
-    and "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
+    and "\<And>i. i \<in> Basis \<Longrightarrow> a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
 proof -
   have "cbox a b \<noteq> {}"
-    using assms(1,3) by metis
+    using emp non by metis
   then have ab: "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
     by (force simp: mem_box)
-  have UN_cases: "\<lbrakk>finite f;
-           \<And>s. s\<in>f \<Longrightarrow> P s;
-           \<And>s. s\<in>f \<Longrightarrow> \<exists>a b. s = cbox a b;
-           \<And>s t. s\<in>f \<Longrightarrow> t\<in>f \<Longrightarrow> s \<noteq> t \<Longrightarrow> interior s \<inter> interior t = {}\<rbrakk> \<Longrightarrow> P (\<Union>f)" for f
-  proof (induct f rule: finite_induct)
-    case empty
-    show ?case
-      using assms(1) by auto
+  have UN_cases: "\<lbrakk>finite \<F>;
+           \<And>S. S\<in>\<F> \<Longrightarrow> P S;
+           \<And>S. S\<in>\<F> \<Longrightarrow> \<exists>a b. S = cbox a b;
+           \<And>S T. S\<in>\<F> \<Longrightarrow> T\<in>\<F> \<Longrightarrow> S \<noteq> T \<Longrightarrow> interior S \<inter> interior T = {}\<rbrakk> \<Longrightarrow> P (\<Union>\<F>)" for \<F>
+  proof (induct \<F> rule: finite_induct)
+    case empty show ?case
+      using emp by auto
   next
     case (insert x f)
-    show ?case
-      unfolding Union_insert
-      apply (rule assms(2)[rule_format])
-      using Int_interior_Union_intervals [of f "interior x"]
-      by (metis (no_types, lifting) insert insert_iff open_interior)
+    then show ?case
+      unfolding Union_insert by (metis Int_interior_Union_intervals Un insert_iff open_interior)
   qed
-  let ?A = "{cbox c d | c d::'a. \<forall>i\<in>Basis. (c\<bullet>i = a\<bullet>i) \<and> (d\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<or>
-    (c\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<and> (d\<bullet>i = b\<bullet>i)}"
-  let ?PP = "\<lambda>c d. \<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
-  {
-    presume "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d) \<Longrightarrow> False"
-    then show thesis
-      unfolding atomize_not not_all
-      by (blast intro: that)
-  }
-  assume as: "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d)"
-  have "P (\<Union>?A)"
+  let ?ab = "\<lambda>i. (a\<bullet>i + b\<bullet>i) / 2"
+  let ?A = "{cbox c d | c d::'a. \<forall>i\<in>Basis. (c\<bullet>i = a\<bullet>i) \<and> (d\<bullet>i = ?ab i) \<or>
+    (c\<bullet>i = ?ab i) \<and> (d\<bullet>i = b\<bullet>i)}"
+  have "P (\<Union>?A)" 
+    if "\<And>c d.  \<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i \<Longrightarrow> P (cbox c d)"
   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}"
+    let ?B = "(\<lambda>S. cbox (\<Sum>i\<in>Basis. (if i \<in> S then a\<bullet>i else ?ab i) *\<^sub>R i::'a)
+                        (\<Sum>i\<in>Basis. (if i \<in> S then ?ab i else b\<bullet>i) *\<^sub>R i)) ` {s. s \<subseteq> Basis}"
     have "?A \<subseteq> ?B"
     proof
       fix x
       assume "x \<in> ?A"
       then obtain c d
         where x:  "x = cbox c d"
-                  "\<And>i. i \<in> Basis \<Longrightarrow>
-                        c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
-                        c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i" by blast
-      show "x \<in> ?B"
-        unfolding image_iff x
-        apply (rule_tac x="{i. i\<in>Basis \<and> c\<bullet>i = a\<bullet>i}" in bexI)
-        apply (rule arg_cong2 [where f = cbox])
-        using x(2) ab
-        apply (auto simp add: euclidean_eq_iff[where 'a='a])
-        by fastforce
+          "\<And>i. i \<in> Basis \<Longrightarrow>
+                        c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i" 
+        by blast
+      have "c = (\<Sum>i\<in>Basis. (if c \<bullet> i = a \<bullet> i then a \<bullet> i else ?ab i) *\<^sub>R i)"
+           "d = (\<Sum>i\<in>Basis. (if c \<bullet> i = a \<bullet> i then ?ab i else b \<bullet> i) *\<^sub>R i)"
+        using x(2) ab by (fastforce simp add: euclidean_eq_iff[where 'a='a])+
+      then show "x \<in> ?B"
+        unfolding x by (rule_tac x="{i. i\<in>Basis \<and> c\<bullet>i = a\<bullet>i}" in image_eqI) auto
     qed
     then show "finite ?A"
       by (rule finite_subset) auto
   next
-    fix s
-    assume "s \<in> ?A"
+    fix S
+    assume "S \<in> ?A"
     then obtain c d
-      where s: "s = cbox c d"
-               "\<And>i. i \<in> Basis \<Longrightarrow>
-                     c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
-                     c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
+      where s: "S = cbox c d"
+               "\<And>i. i \<in> Basis \<Longrightarrow> c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i"
       by blast
-    show "P s"
-      unfolding s
-      apply (rule as[rule_format])
-      using ab s(2) by force
-    show "\<exists>a b. s = cbox a b"
+    show "P S"
+      unfolding s using ab s(2) by (fastforce intro!: that)
+    show "\<exists>a b. S = cbox a b"
       unfolding s by auto
-    fix t
-    assume "t \<in> ?A"
+    fix T
+    assume "T \<in> ?A"
     then obtain e f where t:
-      "t = cbox e f"
-      "\<And>i. i \<in> Basis \<Longrightarrow>
-        e \<bullet> i = a \<bullet> i \<and> f \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
-        e \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> f \<bullet> i = b \<bullet> i"
+      "T = cbox e f"
+      "\<And>i. i \<in> Basis \<Longrightarrow> e \<bullet> i = a \<bullet> i \<and> f \<bullet> i = ?ab i \<or> e \<bullet> i = ?ab i \<and> f \<bullet> i = b \<bullet> i"
       by blast
-    assume "s \<noteq> t"
+    assume "S \<noteq> T"
     then have "\<not> (c = e \<and> d = f)"
       unfolding s t by auto
     then obtain i where "c\<bullet>i \<noteq> e\<bullet>i \<or> d\<bullet>i \<noteq> f\<bullet>i" and i': "i \<in> Basis"
@@ -2011,24 +1993,15 @@
       using t(2)[OF i'] \<open>c \<bullet> i \<noteq> e \<bullet> i \<or> d \<bullet> i \<noteq> f \<bullet> i\<close> i' s(2) t(2) by fastforce
     have *: "\<And>s t. (\<And>a. a \<in> s \<Longrightarrow> a \<in> t \<Longrightarrow> False) \<Longrightarrow> s \<inter> t = {}"
       by auto
-    show "interior s \<inter> interior t = {}"
+    show "interior S \<inter> interior T = {}"
       unfolding s t interior_cbox
     proof (rule *)
       fix x
       assume "x \<in> box c d" "x \<in> box e f"
       then have x: "c\<bullet>i < d\<bullet>i" "e\<bullet>i < f\<bullet>i" "c\<bullet>i < f\<bullet>i" "e\<bullet>i < d\<bullet>i"
-        unfolding mem_box using i'
-        by force+
-      show False  using s(2)[OF i']
-      proof safe
-        assume as: "c \<bullet> i = a \<bullet> i" "d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2"
-        show False
-          using t(2)[OF i'] and i x unfolding as by (fastforce simp add:field_simps)
-      next
-        assume as: "c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2" "d \<bullet> i = b \<bullet> i"
-        show False
-          using t(2)[OF i'] and i x unfolding as by(fastforce simp add:field_simps)
-      qed
+        unfolding mem_box using i'  by force+
+      show False  using s(2)[OF i'] t(2)[OF i'] and i x  
+        by auto
     qed
   qed
   also have "\<Union>?A = cbox a b"
@@ -2037,48 +2010,30 @@
     assume "x \<in> \<Union>?A"
     then obtain c d where x:
       "x \<in> cbox c d"
-      "\<And>i. i \<in> Basis \<Longrightarrow>
-        c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
-        c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
+      "\<And>i. i \<in> Basis \<Longrightarrow> c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i"
       by blast
-    show "x\<in>cbox a b"
-      unfolding mem_box
-    proof safe
-      fix i :: 'a
-      assume i: "i \<in> Basis"
-      then show "a \<bullet> i \<le> x \<bullet> i" "x \<bullet> i \<le> b \<bullet> i"
-        using x(2)[OF i] x(1)[unfolded mem_box,THEN bspec, OF i] by auto
-    qed
+    then show "x\<in>cbox a b"
+      unfolding mem_box by force
   next
     fix x
     assume x: "x \<in> cbox a b"
-    have "\<forall>i\<in>Basis.
-      \<exists>c d. (c = a\<bullet>i \<and> d = (a\<bullet>i + b\<bullet>i) / 2 \<or> c = (a\<bullet>i + b\<bullet>i) / 2 \<and> d = b\<bullet>i) \<and> c\<le>x\<bullet>i \<and> x\<bullet>i \<le> d"
+    then have "\<forall>i\<in>Basis. \<exists>c d. (c = a\<bullet>i \<and> d = ?ab i \<or> c = ?ab i \<and> d = b\<bullet>i) \<and> c\<le>x\<bullet>i \<and> x\<bullet>i \<le> d"
       (is "\<forall>i\<in>Basis. \<exists>c d. ?P i c d")
-      unfolding mem_box
-    proof
-      fix i :: 'a
-      assume i: "i \<in> Basis"
-      have "?P i (a\<bullet>i) ((a \<bullet> i + b \<bullet> i) / 2) \<or> ?P i ((a \<bullet> i + b \<bullet> i) / 2) (b\<bullet>i)"
-        using x[unfolded mem_box,THEN bspec, OF i] by auto
-      then show "\<exists>c d. ?P i c d"
-        by blast
-    qed
-    then obtain \<alpha> \<beta> where
-     "\<forall>i\<in>Basis. (\<alpha> \<bullet> i = a \<bullet> i \<and> \<beta> \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
-         \<alpha> \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> \<beta> \<bullet> i = b \<bullet> i) \<and> \<alpha> \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> \<beta> \<bullet> i"
+      unfolding mem_box by (metis linear)
+    then obtain \<alpha> \<beta> where "\<forall>i\<in>Basis. (\<alpha> \<bullet> i = a \<bullet> i \<and> \<beta> \<bullet> i = ?ab i \<or>
+         \<alpha> \<bullet> i = ?ab i \<and> \<beta> \<bullet> i = b \<bullet> i) \<and> \<alpha> \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> \<beta> \<bullet> i"
       by (auto simp: choice_Basis_iff)
     then show "x\<in>\<Union>?A"
       by (force simp add: mem_box)
   qed
-  finally show False
-    using assms by auto
+  finally show thesis
+      by (metis (no_types, lifting) assms(3) that)
 qed
 
 lemma interval_bisection:
   fixes type :: "'a::euclidean_space"
   assumes "P {}"
-    and "(\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P(s \<union> t))"
+    and Un: "\<And>S T. \<lbrakk>P S; P T; interior(S) \<inter> interior(T) = {}\<rbrakk> \<Longrightarrow> P (S \<union> T)"
     and "\<not> P (cbox a (b::'a))"
   obtains x where "x \<in> cbox a b"
     and "\<forall>e>0. \<exists>c d. x \<in> cbox c d \<and> cbox c d \<subseteq> ball x e \<and> cbox c d \<subseteq> cbox a b \<and> \<not> P (cbox c d)"
@@ -2092,14 +2047,14 @@
       case True
       then show ?thesis by auto
     next
-      case as: False
+      case False
       obtain c d where "\<not> P (cbox c d)"
-        "\<forall>i\<in>Basis.
+        "\<And>i. i \<in> Basis \<Longrightarrow>
            fst x \<bullet> i \<le> c \<bullet> i \<and>
            c \<bullet> i \<le> d \<bullet> i \<and>
            d \<bullet> i \<le> snd x \<bullet> i \<and>
            2 * (d \<bullet> i - c \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i"
-        by (rule interval_bisection_step[of P, OF assms(1-2) as])
+        by (blast intro: interval_bisection_step[of P, OF assms(1-2) False])
       then show ?thesis
         by (rule_tac x="(c,d)" in exI) auto
     qed
@@ -2281,33 +2236,17 @@
 
 lemma tagged_division_finer:
   fixes p :: "('a::euclidean_space \<times> ('a::euclidean_space set)) set"
-  assumes "p tagged_division_of (cbox a b)"
+  assumes ptag: "p tagged_division_of (cbox a b)"
     and "gauge d"
   obtains q where "q tagged_division_of (cbox a b)"
     and "d fine q"
     and "\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q"
 proof -
-  let ?P = "\<lambda>p. p tagged_partial_division_of (cbox a b) \<longrightarrow> gauge d \<longrightarrow>
-    (\<exists>q. q tagged_division_of (\<Union>{k. \<exists>x. (x,k) \<in> p}) \<and> d fine q \<and>
-      (\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q))"
-  {
-    have *: "finite p" "p tagged_partial_division_of (cbox a b)"
-      using assms(1)
-      unfolding tagged_division_of_def
-      by auto
-    presume "\<And>p. finite p \<Longrightarrow> ?P p"
-    from this[rule_format,OF * assms(2)] 
-    obtain q where q: "q tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> p}" "d fine q" "(\<forall>(x, k)\<in>p. k \<subseteq> d x \<longrightarrow> (x, k) \<in> q)"
-      by auto
-    with that[of q] show ?thesis
-      using assms(1) by auto
-  }
-  fix p :: "('a::euclidean_space \<times> ('a::euclidean_space set)) set"
-  assume as: "finite p"
-  show "?P p"
-    apply rule
-    apply rule
-    using as
+  have p: "finite p" "p tagged_partial_division_of (cbox a b)"
+    using ptag unfolding tagged_division_of_def by auto
+  have "(\<exists>q. q tagged_division_of (\<Union>{k. \<exists>x. (x,k) \<in> p}) \<and> d fine q \<and> (\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q))" 
+    if "finite p" "p tagged_partial_division_of (cbox a b)" "gauge d" for p
+    using that
   proof (induct p)
     case empty
     show ?case
@@ -2325,7 +2264,7 @@
       unfolding xk by auto
     note p = tagged_partial_division_ofD[OF insert(4)]
     obtain u v where uv: "k = cbox u v"
-      using p(4)[unfolded xk, OF insertI1] by blast
+      using p(4) xk by blast
     have "finite {k. \<exists>x. (x, k) \<in> p}"
       apply (rule finite_subset[of _ "snd ` p"])
       using image_iff apply fastforce
@@ -2363,6 +2302,9 @@
         done
     qed
   qed
+  with p obtain q where q: "q tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> p}" "d fine q" "\<forall>(x, k)\<in>p. k \<subseteq> d x \<longrightarrow> (x, k) \<in> q"
+    by (meson \<open>gauge d\<close>)
+  with ptag that show ?thesis by auto
 qed
 
 subsubsection \<open>Covering lemma\<close>