# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1503700236 -3600
# Node ID 89b6455b63b6f1bd20c369cac17681f9d8f6a7b8
# Parent  65b6d48fc9a90aba13376f81033d84135a520fbd
starting to unscramble bounded_variation_absolutely_integrable_interval

diff -r 65b6d48fc9a9 -r 89b6455b63b6 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Aug 25 13:01:13 2017 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Aug 25 23:30:36 2017 +0100
@@ -1623,20 +1623,16 @@
       unfolding less_cSUP_iff[OF D] by auto
     note d' = division_ofD[OF this(1)]
 
-    have "\<forall>x. \<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
-    proof
-      fix x
-      have "\<exists>da>0. \<forall>xa\<in>\<Union>{i \<in> d. x \<notin> i}. da \<le> dist x xa"
+    have "\<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}" for x
+    proof -
+      have "\<exists>d'>0. \<forall>x'\<in>\<Union>{i \<in> d. x \<notin> i}. d' \<le> dist x x'"
       proof (rule separate_point_closed)
         show "closed (\<Union>{i \<in> d. x \<notin> i})"
-          apply (rule closed_Union)
-           apply (simp add: d'(1))
-          using d'(4) apply auto
-          done
+          using d' by force
         show "x \<notin> \<Union>{i \<in> d. x \<notin> i}"
           by auto
       qed 
-      then show "\<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
+      then show ?thesis
         by force
     qed
     then obtain k where k: "\<And>x. 0 < k x" "\<And>i x. \<lbrakk>i \<in> d; x \<notin> i\<rbrakk> \<Longrightarrow> ball x (k x) \<inter> i = {}"
@@ -1680,8 +1676,7 @@
         show "x \<in> K" and "K \<subseteq> cbox a b"
           using p'(2-3)[OF il(3)] il by auto
         show "\<exists>a b. K = cbox a b"
-          unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)]
-          by (meson Int_interval)
+          unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)] by (meson Int_interval)
       next
         fix x1 K1
         assume "(x1, K1) \<in> p'"
@@ -1710,8 +1705,7 @@
           have "x \<in> i"
             using fineD[OF p(3) xl(1)] using k(2) i xl by auto
           then show ?thesis
-            unfolding p'_def
-            by (rule_tac X="i \<inter> l" in UnionI) (use i xl in auto)
+            unfolding p'_def by (rule_tac X="i \<inter> l" in UnionI) (use i xl in auto)
         qed
         show "\<Union>{K. \<exists>x. (x, K) \<in> p'} = cbox a b"
         proof
@@ -1738,22 +1732,23 @@
       then have sum_less_e2: "(\<Sum>(x,K) \<in> p'. norm (content K *\<^sub>R f x - integral K f)) < e/2"
         using g(2) gp' tagged_division_of_def by blast
 
-      have p'alt: "p' = {(x, I \<inter> L) | x I L. (x,L) \<in> p \<and> I \<in> d \<and> I \<inter> L \<noteq> {}}"
+      have XX: "(x, I \<inter> L) \<in> p'" if "(x, L) \<in> p" "I \<in> d" "y \<in> I" "y \<in> L"
+        for x I L y
+      proof -
+        have "x \<in> I"
+          using fineD[OF p(3) that(1)] k(2)[OF that(2), of x] that(3-) by auto
+        then have "(\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> I \<inter> L = i \<inter> l)"
+          using that(1) that(2) by blast
+        then have "(x, I \<inter> L) \<in> p'"
+          by (simp add: p'_def)
+        then show ?thesis
+          using that(3) by auto
+      qed
+  have p'alt: "p' = {(x, I \<inter> L) | x I L. (x,L) \<in> p \<and> I \<in> d \<and> I \<inter> L \<noteq> {}}"
       proof (safe, goal_cases)
         case prems: (2 _ _ x i l)
-        have "x \<in> i"
-          using fineD[OF p(3) prems(1)] k(2)[OF prems(2), of x] prems(4-)
-          by auto
-        then have "(x, i \<inter> l) \<in> p'"
-          unfolding p'_def
-          using prems
-          apply safe
-          apply (rule_tac x=x in exI)
-          apply (rule_tac x="i \<inter> l" in exI)
-          apply auto
-          done
         then show ?case
-          using prems(3) by auto
+          using XX by auto
       next
         fix x K
         assume "(x, K) \<in> p'"
@@ -2027,14 +2022,13 @@
       then show False
         using prems by auto
     qed
-    then obtain K where *: "\<exists>x\<in>{d. d division_of \<Union>d}. K = (\<Sum>k\<in>x. norm (integral k f))"
+    then obtain d K where ddiv: "d division_of \<Union>d" and "K = (\<Sum>k\<in>d. norm (integral k f))"
       "SUPREMUM {d. d division_of \<Union>d} (sum (\<lambda>k. norm (integral k f))) - e < K"
       by (auto simp add: image_iff not_le)
-    from this(1) obtain d where "d division_of \<Union>d"
-      and "K = (\<Sum>k\<in>d. norm (integral k f))"
+    then have d: "SUPREMUM {d. d division_of \<Union>d} (sum (\<lambda>k. norm (integral k f))) - e 
+                  < (\<Sum>k\<in>d. norm (integral k f))"
       by auto
-    note d = this(1) *(2)[unfolded this(2)]
-    note d'=division_ofD[OF this(1)]
+    note d'=division_ofD[OF ddiv]
     have "bounded (\<Union>d)"
       by (rule elementary_bounded,fact)
     from this[unfolded bounded_pos] obtain K where
@@ -2051,7 +2045,7 @@
         unfolding real_norm_def
         apply (rule *[rule_format])
         apply safe
-        apply (rule d(2))
+        apply (rule d)
       proof goal_cases
         case 1
         have "(\<Sum>k\<in>d. norm (integral k f)) \<le> sum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
@@ -2061,31 +2055,15 @@
             by (auto simp: absolutely_integrable_on_def integral_norm_bound_integral)
           done
         also have "\<dots> = integral (\<Union>d) (\<lambda>x. norm (f x))"
-          apply (rule integral_combine_division_bottomup[symmetric])
-          apply (rule d)
-          unfolding forall_in_division[OF d(1)]
-          using f_int unfolding absolutely_integrable_on_def
-          apply auto
-          done
+          apply (rule integral_combine_division_bottomup[OF ddiv, symmetric])
+          using absolutely_integrable_on_def d'(4) f_int by blast
         also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)"
         proof -
           have "\<Union>d \<subseteq> cbox a b"
-            apply rule
-            apply (drule K(2)[rule_format])
-            apply (rule ab[unfolded subset_eq,rule_format])
-            apply (auto simp add: dist_norm)
-            done
+            using K(2) ab by fastforce
           then show ?thesis
-            apply -
-            apply (subst if_P)
-            apply rule
-            apply (rule integral_subset_le)
-            defer
-            apply (rule integrable_on_subdivision[of _ _ _ "cbox a b"])
-            apply (rule d)
-            using f_int[of a b] unfolding absolutely_integrable_on_def
-            apply auto
-            done
+            using integrable_on_subdivision[OF ddiv] f_int[of a b] unfolding absolutely_integrable_on_def
+            by (auto intro!: integral_subset_le)
         qed
         finally show ?case .
       next
@@ -2119,11 +2097,7 @@
           show "\<bar>(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))\<bar> < e/2"
             using d1[OF p(1,2)] by (simp only: real_norm_def)
           show "(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) = (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x))"
-            apply (rule sum.cong)
-            apply (rule refl)
-            unfolding split_paired_all split_conv
-            apply (drule tagged_division_ofD(4)[OF p(1)])
-            by simp
+            by (auto simp: split_paired_all sum.cong [OF refl])
           show "(\<Sum>(x,k) \<in> p. norm (integral k f)) \<le> ?S"
             using partial_division_of_tagged_division[of p "cbox a b"] p(1)
             apply (subst sum.over_tagged_division_lemma[OF p(1)])
diff -r 65b6d48fc9a9 -r 89b6455b63b6 src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Fri Aug 25 13:01:13 2017 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy	Fri Aug 25 23:30:36 2017 +0100
@@ -719,22 +719,22 @@
   hence "(\<lambda>n. of_real (ln (real n / (real n + 1)))) \<longlonglongrightarrow> (0 :: 'a)" by (simp add: add_ac)
   hence lim: "(\<lambda>n. of_real (ln (real n)) - of_real (ln (real n + 1))) \<longlonglongrightarrow> (0::'a)"
   proof (rule Lim_transform_eventually [rotated])
-    show "eventually (\<lambda>n. of_real (ln (real n / (real n + 1))) = 
+    show "eventually (\<lambda>n. of_real (ln (real n / (real n + 1))) =
             of_real (ln (real n)) - (of_real (ln (real n + 1)) :: 'a)) at_top"
       using eventually_gt_at_top[of "0::nat"] by eventually_elim (simp add: ln_div)
   qed
 
   from summable_Digamma[OF z]
-    have "(\<lambda>n. inverse (of_nat (n+1)) - inverse (z + of_nat n)) 
+    have "(\<lambda>n. inverse (of_nat (n+1)) - inverse (z + of_nat n))
               sums (Digamma z + euler_mascheroni)"
     by (simp add: Digamma_def summable_sums)
   from sums_diff[OF this euler_mascheroni_sum]
     have "(\<lambda>n. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1)) - inverse (z + of_nat n))
             sums Digamma z" by (simp add: add_ac)
-  hence "(\<lambda>m. (\<Sum>n<m. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1))) - 
+  hence "(\<lambda>m. (\<Sum>n<m. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1))) -
               (\<Sum>n<m. inverse (z + of_nat n))) \<longlonglongrightarrow> Digamma z"
     by (simp add: sums_def sum_subtractf)
-  also have "(\<lambda>m. (\<Sum>n<m. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1)))) = 
+  also have "(\<lambda>m. (\<Sum>n<m. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1)))) =
                  (\<lambda>m. of_real (ln (m + 1)) :: 'a)"
     by (subst sum_lessThan_telescope) simp_all
   finally show ?thesis by (rule Lim_transform) (insert lim, simp)
@@ -977,17 +977,17 @@
   shows "A \<inter> \<real>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> continuous_on A ln_Gamma"
   by (intro continuous_at_imp_continuous_on ballI isCont_ln_Gamma_complex[OF continuous_ident])
      fastforce
-     
+
 lemma deriv_Polygamma:
   assumes "z \<notin> \<int>\<^sub>\<le>\<^sub>0"
-  shows   "deriv (Polygamma m) z = 
+  shows   "deriv (Polygamma m) z =
              Polygamma (Suc m) (z :: 'a :: {real_normed_field,euclidean_space})"
   by (intro DERIV_imp_deriv has_field_derivative_Polygamma assms)
     thm has_field_derivative_Polygamma
 
 lemma higher_deriv_Polygamma:
   assumes "z \<notin> \<int>\<^sub>\<le>\<^sub>0"
-  shows   "(deriv ^^ n) (Polygamma m) z = 
+  shows   "(deriv ^^ n) (Polygamma m) z =
              Polygamma (m + n) (z :: 'a :: {real_normed_field,euclidean_space})"
 proof -
   have "eventually (\<lambda>u. (deriv ^^ n) (Polygamma m) u = Polygamma (m + n) u) (nhds z)"
@@ -995,7 +995,7 @@
     case (Suc n)
     from Suc.IH have "eventually (\<lambda>z. eventually (\<lambda>u. (deriv ^^ n) (Polygamma m) u = Polygamma (m + n) u) (nhds z)) (nhds z)"
       by (simp add: eventually_eventually)
-    hence "eventually (\<lambda>z. deriv ((deriv ^^ n) (Polygamma m)) z = 
+    hence "eventually (\<lambda>z. deriv ((deriv ^^ n) (Polygamma m)) z =
              deriv (Polygamma (m + n)) z) (nhds z)"
       by eventually_elim (intro deriv_cong_ev refl)
     moreover have "eventually (\<lambda>z. z \<in> UNIV - \<int>\<^sub>\<le>\<^sub>0) (nhds z)" using assms
@@ -1478,9 +1478,9 @@
 lemma analytic_Gamma: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> Gamma analytic_on A"
   by (rule analytic_on_subset[of _ "UNIV - \<int>\<^sub>\<le>\<^sub>0"], subst analytic_on_open)
      (auto intro!: holomorphic_Gamma)
-     
-
-lemma field_differentiable_ln_Gamma_complex: 
+
+
+lemma field_differentiable_ln_Gamma_complex:
   "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ln_Gamma field_differentiable (at (z::complex) within A)"
   by (rule field_differentiable_within_subset[of _ _ UNIV])
      (force simp: field_differentiable_def intro!: derivative_intros)+
@@ -1648,8 +1648,8 @@
 
 lemma ln_Gamma_complex_conv_fact: "n > 0 \<Longrightarrow> ln_Gamma (of_nat n :: complex) = ln (fact (n - 1))"
   using ln_Gamma_complex_of_real[of "real n"] Gamma_fact[of "n - 1", where 'a = real]
-  by (simp add: ln_Gamma_real_pos of_nat_diff Ln_of_real [symmetric])    
-    
+  by (simp add: ln_Gamma_real_pos of_nat_diff Ln_of_real [symmetric])
+
 lemma ln_Gamma_real_conv_fact: "n > 0 \<Longrightarrow> ln_Gamma (real n) = ln (fact (n - 1))"
   using Gamma_fact[of "n - 1", where 'a = real]
   by (simp add: ln_Gamma_real_pos of_nat_diff Ln_of_real [symmetric])
@@ -1668,14 +1668,14 @@
     show "eventually (\<lambda>y. ln_Gamma y = (Re \<circ> ln_Gamma \<circ> of_real) y) (nhds x)"
     by (auto elim!: eventually_mono simp: ln_Gamma_complex_of_real interior_open)
 qed
-  
-lemma field_differentiable_ln_Gamma_real: 
+
+lemma field_differentiable_ln_Gamma_real:
   "x > 0 \<Longrightarrow> ln_Gamma field_differentiable (at (x::real) within A)"
   by (rule field_differentiable_within_subset[of _ _ UNIV])
      (auto simp: field_differentiable_def intro!: derivative_intros)+
 
 declare has_field_derivative_ln_Gamma_real[THEN DERIV_chain2, derivative_intros]
-  
+
 lemma deriv_ln_Gamma_real:
   assumes "z > 0"
   shows   "deriv ln_Gamma z = Digamma (z :: real)"
@@ -1785,12 +1785,12 @@
 subsection \<open>The uniqueness of the real Gamma function\<close>
 
 text \<open>
-  The following is a proof of the Bohr--Mollerup theorem, which states that 
+  The following is a proof of the Bohr--Mollerup theorem, which states that
   any log-convex function $G$ on the positive reals that fulfils $G(1) = 1$ and
-  satisfies the functional equation $G(x+1) = x G(x)$ must be equal to the 
+  satisfies the functional equation $G(x+1) = x G(x)$ must be equal to the
   Gamma function.
-  In principle, if $G$ is a holomorphic complex function, one could then extend 
-  this from the positive reals to the entire complex plane (minus the non-positive 
+  In principle, if $G$ is a holomorphic complex function, one could then extend
+  this from the positive reals to the entire complex plane (minus the non-positive
   integers, where the Gamma function is not defined).
 \<close>
 
@@ -1809,7 +1809,7 @@
 private definition S :: "real \<Rightarrow> real \<Rightarrow> real" where
   "S x y = (ln (G y) - ln (G x)) / (y - x)"
 
-private lemma S_eq: 
+private lemma S_eq:
   "n \<ge> 2 \<Longrightarrow> S (of_nat n) (of_nat n + x) = (ln (G (real n + x)) - ln (fact (n - 1))) / x"
   by (subst G_fact [symmetric]) (simp add: S_def add_ac of_nat_diff)
 
@@ -1821,16 +1821,16 @@
           (ln \<circ> G) (real (Suc n) - 1)) / (real (Suc n) + x - (real (Suc n) - 1)) *
            (real (Suc n) - (real (Suc n) - 1)) + (ln \<circ> G) (real (Suc n) - 1)"
     using x n by (intro convex_onD_Icc' convex_on_subset[OF log_convex_G]) auto
-  hence "S (of_nat n) (of_nat (Suc n)) \<le> S (of_nat (Suc n)) (of_nat (Suc n) + x)" 
+  hence "S (of_nat n) (of_nat (Suc n)) \<le> S (of_nat (Suc n)) (of_nat (Suc n) + x)"
     unfolding S_def using x by (simp add: field_simps)
   also have "S (of_nat n) (of_nat (Suc n)) = ln (fact n) - ln (fact (n-1))"
-    unfolding S_def using n 
+    unfolding S_def using n
     by (subst (1 2) G_fact [symmetric]) (simp_all add: add_ac of_nat_diff)
   also have "\<dots> = ln (fact n / fact (n-1))" by (subst ln_div) simp_all
   also from n have "fact n / fact (n - 1) = n" by (cases n) simp_all
   finally have "x * ln (real n) + ln (fact n) \<le> ln (G (real (Suc n) + x))"
     using x n by (subst (asm) S_eq) (simp_all add: field_simps)
-  also have "x * ln (real n) + ln (fact n) = ln (exp (x * ln (real n)) * fact n)" 
+  also have "x * ln (real n) + ln (fact n) = ln (exp (x * ln (real n)) * fact n)"
     using x by (simp add: ln_mult)
   finally have "exp (x * ln (real n)) * fact n \<le> G (real (Suc n) + x)" using x
     by (subst (asm) ln_le_cancel_iff) (simp_all add: G_pos)
@@ -1847,15 +1847,15 @@
 proof -
   have "(ln \<circ> G) (real n + x) \<le> ((ln \<circ> G) (real n + 1) -
           (ln \<circ> G) (real n)) / (real n + 1 - (real n)) *
-           ((real n + x) - real n) + (ln \<circ> G) (real n)" 
+           ((real n + x) - real n) + (ln \<circ> G) (real n)"
     using x n by (intro convex_onD_Icc' convex_on_subset[OF log_convex_G]) auto
-  hence "S (of_nat n) (of_nat n + x) \<le> S (of_nat n) (of_nat n + 1)" 
+  hence "S (of_nat n) (of_nat n + x) \<le> S (of_nat n) (of_nat n + 1)"
     unfolding S_def using x by (simp add: field_simps)
   also from n have "S (of_nat n) (of_nat n + 1) = ln (fact n) - ln (fact (n-1))"
     by (subst (1 2) G_fact [symmetric]) (simp add: S_def add_ac of_nat_diff)
   also have "\<dots> = ln (fact n / (fact (n-1)))" using n by (subst ln_div) simp_all
   also from n have "fact n / fact (n - 1) = n" by (cases n) simp_all
-  finally have "ln (G (real n + x)) \<le> x * ln (real n) + ln (fact (n - 1))" 
+  finally have "ln (G (real n + x)) \<le> x * ln (real n) + ln (fact (n - 1))"
     using x n by (subst (asm) S_eq) (simp_all add: field_simps)
   also have "\<dots> = ln (exp (x * ln (real n)) * fact (n - 1))" using x
     by (simp add: ln_mult)
@@ -1867,7 +1867,7 @@
   finally have "G x \<le> exp (x * ln (real n)) * fact (n- 1) / pochhammer x n"
     using x by (simp add: field_simps pochhammer_pos)
   also from n have "fact (n - 1) = fact n / n" by (cases n) simp_all
-  also have "exp (x * ln (real n)) * \<dots> / pochhammer x n = 
+  also have "exp (x * ln (real n)) * \<dots> / pochhammer x n =
                Gamma_series x n * (1 + x / real n)" using n x
     by (simp add: Gamma_series_def divide_simps pochhammer_Suc)
   finally show ?thesis .
@@ -1886,7 +1886,7 @@
   show "G x \<le> Gamma x"
   proof (rule tendsto_lowerbound)
     have "(\<lambda>n. Gamma_series x n * (1 + x / real n)) \<longlonglongrightarrow> Gamma x * (1 + 0)"
-      by (rule tendsto_intros real_tendsto_divide_at_top 
+      by (rule tendsto_intros real_tendsto_divide_at_top
                Gamma_series_LIMSEQ filterlim_real_sequentially)+
     thus "(\<lambda>n. Gamma_series x n * (1 + x / real n)) \<longlonglongrightarrow> Gamma x" by simp
   next
@@ -1907,7 +1907,7 @@
     with Suc show ?case using G_plus1[of "real n + x"] Gamma_plus1[of "real n + x"]
       by (auto simp: add_ac)
   qed (simp_all add: G_eq_Gamma_aux)
-  
+
   show ?thesis
   proof (cases "frac x = 0")
     case True
@@ -2129,9 +2129,9 @@
     also have "g \<circ> (\<lambda>x. x - of_int n) = g" by (intro ext) (simp add: g.minus_of_int)
     finally show "(g has_field_derivative (h z * g z)) (at z)" by (simp add: z h_def)
   qed
-    
+
   have g_holo [holomorphic_intros]: "g holomorphic_on A" for A
-    by (rule holomorphic_on_subset[of _ UNIV]) 
+    by (rule holomorphic_on_subset[of _ UNIV])
        (force simp: holomorphic_on_open intro!: derivative_intros)+
 
   have g_eq: "g (z/2) * g ((z+1)/2) = Gamma (1/2)^2 * g z" if "Re z > -1" "Re z < 2" for z
@@ -2193,10 +2193,10 @@
   have g_nz [simp]: "g z \<noteq> 0" for z :: complex
   unfolding g_def using Ints_diff[of 1 "1 - z"]
     by (auto simp: Gamma_eq_zero_iff sin_eq_0 dest!: nonpos_Ints_Int)
-  
+
   have h_altdef: "h z = deriv g z / g z" for z :: complex
     using DERIV_imp_deriv[OF g_g', of z] by simp
-  
+
   have h_eq: "h z = (h (z/2) + h ((z+1)/2)) / 2" for z
   proof -
     have "((\<lambda>t. g (t/2) * g ((t+1)/2)) has_field_derivative
@@ -2485,7 +2485,7 @@
   let ?r' = "\<lambda>n. exp (z * of_real (ln (of_nat (Suc n) / of_nat n)))"
   from z have z': "z \<noteq> 0" by auto
 
-  have "eventually (\<lambda>n. ?r' n = ?r n) sequentially" 
+  have "eventually (\<lambda>n. ?r' n = ?r n) sequentially"
     using z by (auto simp: divide_simps Gamma_series_def ring_distribs exp_diff ln_div add_ac
                      intro: eventually_mono eventually_gt_at_top[of "0::nat"] dest: pochhammer_eq_0_imp_nonpos_Int)
   moreover have "?r' \<longlonglongrightarrow> exp (z * of_real (ln 1))"
@@ -2711,7 +2711,7 @@
   have "f integrable_on {c..}"
     by (rule integrable_spike_finite[of "{c}", OF _ _ A]) (simp_all add: f_def)
   ultimately show "f integrable_on {0..}"
-    by (rule integrable_union') (insert c, auto simp: max_def)
+    by (rule integrable_Un') (insert c, auto simp: max_def)
 qed
 
 lemma Gamma_integral_complex:
@@ -2948,9 +2948,9 @@
 
 theorem wallis: "(\<lambda>n. \<Prod>k=1..n. (4*real k^2) / (4*real k^2 - 1)) \<longlonglongrightarrow> pi / 2"
 proof -
-  from tendsto_inverse[OF tendsto_mult[OF 
+  from tendsto_inverse[OF tendsto_mult[OF
          sin_product_formula_real[of "1/2"] tendsto_const[of "2/pi"]]]
-    have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) \<longlonglongrightarrow> pi/2" 
+    have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) \<longlonglongrightarrow> pi/2"
     by (simp add: prod_inversef [symmetric])
   also have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) =
                (\<lambda>n. (\<Prod>k=1..n. (4*real k^2)/(4*real k^2 - 1)))"
diff -r 65b6d48fc9a9 -r 89b6455b63b6 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Aug 25 13:01:13 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Aug 25 23:30:36 2017 +0100
@@ -1,5 +1,6 @@
 (*  Author:     John Harrison
-    Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light); proofs reworked by LCP
+    Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light)
+                Huge cleanup by LCP
 *)
 
 section \<open>Henstock-Kurzweil gauge integration in many dimensions.\<close>
@@ -165,23 +166,23 @@
 qed
 
 lemma division_of_content_0:
-  assumes "content (cbox a b) = 0" "d division_of (cbox a b)"
-  shows "\<forall>k\<in>d. content k = 0"
+  assumes "content (cbox a b) = 0" "d division_of (cbox a b)" "K \<in> d"
+  shows "content K = 0"
   unfolding forall_in_division[OF assms(2)]
-  by (metis antisym_conv assms content_pos_le content_subset division_ofD(2))
+  by (meson assms content_0_subset division_of_def)
 
 lemma sum_content_null:
   assumes "content (cbox a b) = 0"
     and "p tagged_division_of (cbox a b)"
-  shows "(\<Sum>(x,k)\<in>p. content k *\<^sub>R f x) = (0::'a::real_normed_vector)"
+  shows "(\<Sum>(x,K)\<in>p. content K *\<^sub>R f x) = (0::'a::real_normed_vector)"
 proof (rule sum.neutral, rule)
   fix y
   assume y: "y \<in> p"
-  obtain x k where xk: "y = (x, k)"
+  obtain x K where xk: "y = (x, K)"
     using surj_pair[of y] by blast
-  then obtain c d where k: "k = cbox c d" "k \<subseteq> cbox a b"
+  then obtain c d where k: "K = cbox c d" "K \<subseteq> cbox a b"
     by (metis assms(2) tagged_division_ofD(3) tagged_division_ofD(4) y)
-  have "(\<lambda>(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x"
+  have "(\<lambda>(x',K'). content K' *\<^sub>R f x') y = content K *\<^sub>R f x"
     unfolding xk by auto
   also have "\<dots> = 0"
     using assms(1) content_0_subset k(2) by auto
@@ -5337,11 +5338,10 @@
 
 subsection \<open>Adding integrals over several sets\<close>
 
-lemma has_integral_union:
+lemma has_integral_Un:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "(f has_integral i) s"
-    and "(f has_integral j) t"
-    and "negligible (s \<inter> t)"
+  assumes f: "(f has_integral i) s" "(f has_integral j) t"
+    and neg: "negligible (s \<inter> t)"
   shows "(f has_integral (i + j)) (s \<union> t)"
 proof -
   note * = has_integral_restrict_UNIV[symmetric, of f]
@@ -5349,28 +5349,28 @@
     unfolding *
     apply (rule has_integral_spike[OF assms(3)])
     defer
-    apply (rule has_integral_add[OF assms(1-2)[unfolded *]])
+    apply (rule has_integral_add[OF f[unfolded *]])
     apply auto
     done
 qed
 
-lemma integrable_union:
+lemma integrable_Un:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: banach"
   assumes "negligible (A \<inter> B)" "f integrable_on A" "f integrable_on B"
   shows   "f integrable_on (A \<union> B)"
 proof -
   from assms obtain y z where "(f has_integral y) A" "(f has_integral z) B"
      by (auto simp: integrable_on_def)
-  from has_integral_union[OF this assms(1)] show ?thesis by (auto simp: integrable_on_def)
+  from has_integral_Un[OF this assms(1)] show ?thesis by (auto simp: integrable_on_def)
 qed
 
-lemma integrable_union':
+lemma integrable_Un':
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: banach"
   assumes "f integrable_on A" "f integrable_on B" "negligible (A \<inter> B)" "C = A \<union> B"
   shows   "f integrable_on C"
-  using integrable_union[of A B f] assms by simp
-
-lemma has_integral_unions:
+  using integrable_Un[of A B f] assms by simp
+
+lemma has_integral_Union:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   assumes "finite t"
     and "\<forall>s\<in>t. (f has_integral (i s)) s"
@@ -5401,22 +5401,12 @@
     then show ?case
     proof (cases "x \<in> \<Union>t")
       case True
-      then guess s unfolding Union_iff..note s=this
-      then have *: "\<forall>b\<in>t. x \<in> b \<longleftrightarrow> b = s"
+      then obtain s where "s \<in> t" "x \<in> s"
+        by blast
+      moreover then have "\<forall>b\<in>t. x \<in> b \<longleftrightarrow> b = s"
         using prems(3) by blast
-      show ?thesis
-        unfolding if_P[OF True]
-        apply (rule trans)
-        defer
-        apply (rule sum.cong)
-        apply (rule refl)
-        apply (subst *)
-        apply assumption
-        apply (rule refl)
-        unfolding sum.delta[OF assms(1)]
-        using s
-        apply auto
-        done
+      ultimately show ?thesis
+        by (simp add: sum.delta[OF assms(1)])
     qed auto
   qed
 qed
@@ -5426,36 +5416,29 @@
 
 lemma has_integral_combine_division:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "d division_of s"
-    and "\<forall>k\<in>d. (f has_integral (i k)) k"
-  shows "(f has_integral (sum i d)) s"
+  assumes "d division_of S"
+    and "\<And>k. k \<in> d \<Longrightarrow> (f has_integral (i k)) k"
+  shows "(f has_integral (sum i d)) S"
 proof -
   note d = division_ofD[OF assms(1)]
+  have neg: "negligible (S \<inter> s')" if "S \<in> d" "s' \<in> d" "S \<noteq> s'" for S s'
+  proof -
+    obtain a c b d where obt: "S = cbox a b" "s' = cbox c d"
+      by (meson \<open>S \<in> d\<close> \<open>s' \<in> d\<close> d(4))
+    from d(5)[OF that] show ?thesis
+      unfolding obt interior_cbox
+      by (metis (no_types, lifting) Diff_empty Int_interval box_Int_box negligible_frontier_interval)
+  qed
   show ?thesis
     unfolding d(6)[symmetric]
-    apply (rule has_integral_unions)
-    apply (rule d assms)+
-    apply rule
-    apply rule
-    apply rule
-  proof goal_cases
-    case prems: (1 s s')
-    from d(4)[OF this(1)] d(4)[OF this(2)] guess a c b d by (elim exE) note obt=this
-    from d(5)[OF prems] show ?case
-      unfolding obt interior_cbox
-      apply -
-      apply (rule negligible_subset[of "(cbox a b-box a b) \<union> (cbox c d-box c d)"])
-      apply (rule negligible_Un negligible_frontier_interval)+
-      apply auto
-      done
-  qed
+    by (auto intro: d neg assms has_integral_Union)
 qed
 
 lemma integral_combine_division_bottomup:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "d division_of s"
-    and "\<forall>k\<in>d. f integrable_on k"
-  shows "integral s f = sum (\<lambda>i. integral i f) d"
+  assumes "d division_of S"
+    and "\<And>k. k \<in> d \<Longrightarrow> f integrable_on k"
+  shows "integral S f = sum (\<lambda>i. integral i f) d"
   apply (rule integral_unique)
   apply (rule has_integral_combine_division[OF assms(1)])
   using assms(2)
@@ -5465,12 +5448,11 @@
 
 lemma has_integral_combine_division_topdown:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "f integrable_on s"
+  assumes "f integrable_on S"
     and "d division_of k"
-    and "k \<subseteq> s"
+    and "k \<subseteq> S"
   shows "(f has_integral (sum (\<lambda>i. integral i f) d)) k"
   apply (rule has_integral_combine_division[OF assms(2)])
-  apply safe
   unfolding has_integral_integral[symmetric]
 proof goal_cases
   case (1 k)
@@ -5486,9 +5468,9 @@
 
 lemma integral_combine_division_topdown:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "f integrable_on s"
-    and "d division_of s"
-  shows "integral s f = sum (\<lambda>i. integral i f) d"
+  assumes "f integrable_on S"
+    and "d division_of S"
+  shows "integral S f = sum (\<lambda>i. integral i f) d"
   apply (rule integral_unique)
   apply (rule has_integral_combine_division_topdown)
   using assms
@@ -5497,9 +5479,9 @@
 
 lemma integrable_combine_division:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "d division_of s"
+  assumes "d division_of S"
     and "\<forall>i\<in>d. f integrable_on i"
-  shows "f integrable_on s"
+  shows "f integrable_on S"
   using assms(2)
   unfolding integrable_on_def
   by (metis has_integral_combine_division[OF assms(1)])
@@ -5507,8 +5489,8 @@
 lemma integrable_on_subdivision:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   assumes "d division_of i"
-    and "f integrable_on s"
-    and "i \<subseteq> s"
+    and "f integrable_on S"
+    and "i \<subseteq> S"
   shows "f integrable_on i"
   apply (rule integrable_combine_division assms)+
   apply safe
@@ -5526,16 +5508,16 @@
 
 subsection \<open>Also tagged divisions\<close>
 
-lemma has_integral_iff: "(f has_integral i) s \<longleftrightarrow> (f integrable_on s \<and> integral s f = i)"
+lemma has_integral_iff: "(f has_integral i) S \<longleftrightarrow> (f integrable_on S \<and> integral S f = i)"
   by blast
 
 lemma has_integral_combine_tagged_division:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "p tagged_division_of s"
+  assumes "p tagged_division_of S"
     and "\<forall>(x,k) \<in> p. (f has_integral (i k)) k"
-  shows "(f has_integral (\<Sum>(x,k)\<in>p. i k)) s"
+  shows "(f has_integral (\<Sum>(x,k)\<in>p. i k)) S"
 proof -
-  have *: "(f has_integral (\<Sum>k\<in>snd`p. integral k f)) s"
+  have *: "(f has_integral (\<Sum>k\<in>snd`p. integral k f)) S"
     using assms(2)
     apply (intro has_integral_combine_division)
     apply (auto simp: has_integral_integral[symmetric] intro: division_of_tagged_division[OF assms(1)])
@@ -5603,8 +5585,9 @@
   note p' = tagged_partial_division_ofD[OF p(1)]
   have "\<Union>(snd ` p) \<subseteq> cbox a b"
     using p'(3) by fastforce
-  note partial_division_of_tagged_division[OF p(1)] this
-  from partial_division_extend_interval[OF this] guess q . note q=this and q' = division_ofD[OF this(2)]
+  then obtain q where q: "snd ` p \<subseteq> q" "q division_of cbox a b"
+    by (meson p(1) partial_division_extend_interval partial_division_of_tagged_division)
+  note q' = division_ofD[OF this(2)]
   define r where "r = q - snd ` p"
   have "snd ` p \<inter> r = {}"
     unfolding r_def by auto