diff -r 5db8427fdfd3 -r 8e614c223000 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 09 13:41:23 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 09 23:41:47 2017 +0200
@@ -3811,7 +3811,7 @@
         then show "0 \<le> e * ((Sup k) - (Inf k))"
           unfolding uv using e by (auto simp add: field_simps)
       qed
-      have **: "norm (\<Sum>(x, k)\<in>p \<inter> {t. fst t \<in> {a, b}}. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b - a) / 2"
+      have norm_le: "norm (\<Sum>(x, k)\<in>p \<inter> {t. fst t \<in> {a, b}}. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b-a) / 2"
       proof -
         have *: "\<And>s f t e. sum f s = sum f t \<Longrightarrow> norm (sum f t) \<le> e \<Longrightarrow> norm (sum f s) \<le> e"
           by auto
@@ -3831,16 +3831,11 @@
             by auto
           then obtain u v where uv: "k = cbox u v"
             using p(4) by blast
-          have "k \<noteq> {}"
-            using p(2)[OF xk] by auto
-          then have *: "u = v"
-            using xk k0 by (auto simp: uv content_eq_0 box_eq_empty)
+          then have "u = v"
+            using xk k0 p(2) by force
           then show "content k *\<^sub>R (f' (x)) - (f ((Sup k)) - f ((Inf k))) = 0"
             using xk unfolding uv by auto
         next
-          have *: "p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0} =
-            {t. t\<in>p \<and> fst t = a \<and> content(snd t) \<noteq> 0} \<union> {t. t\<in>p \<and> fst t = b \<and> content(snd t) \<noteq> 0}"
-            by blast
           have **: "norm (sum f s) \<le> e"
             if "\<forall>x y. x \<in> s \<and> y \<in> s \<longrightarrow> x = y" "\<forall>x. x \<in> s \<longrightarrow> norm (f x) \<le> e" "e > 0"
             for s f and e :: real
@@ -3851,135 +3846,102 @@
             case False
             then obtain x where "x \<in> s"
               by auto
-            then have *: "s = {x}"
+            then have "s = {x}"
               using that(1) by auto
             then show ?thesis
               using \<open>x \<in> s\<close> that(2) by auto
           qed
           case 2
+            let ?B = "\<lambda>x. {t \<in> p. fst t = x \<and> content (snd t) \<noteq> 0}"
+          have *: "p \<inter> {t. fst t \<in> {a, b} \<and> content(snd t) \<noteq> 0} = ?B a \<union> ?B b"
+            by blast
           show ?case
             apply (subst *)
             apply (subst sum.union_disjoint)
             prefer 4
             apply (rule order_trans[of _ "e * (b - a)/4 + e * (b - a)/4"])
             apply (rule norm_triangle_le,rule add_mono)
-            apply (rule_tac[1-2] **)
+                 apply (rule_tac[1-2] **)
+
           proof -
-            let ?B = "\<lambda>x. {t \<in> p. fst t = x \<and> content (snd t) \<noteq> 0}"
             have pa: "\<exists>v. k = cbox a v \<and> a \<le> v" if "(a, k) \<in> p" for k
             proof -
               obtain u v where uv: "k = cbox u v"
                 using \<open>(a, k) \<in> p\<close> p(4) by blast
-              then have *: "u \<le> v"
-                using p(2)[OF that] by auto
-              have u: "u = a"
-              proof (rule ccontr)
-                have "u \<in> cbox u v"
-                  using p(2-3)[OF that(1)] unfolding uv by auto
-                have "u \<ge> a"
-                  using p(2-3)[OF that(1)] unfolding uv subset_eq by auto
-                moreover assume "\<not> ?thesis"
-                ultimately have "u > a" by auto
-                then show False
-                  using p(2)[OF that(1)] unfolding uv by (auto simp add:)
-              qed
-              then show ?thesis
-                apply (rule_tac x=v in exI)
-                unfolding uv
-                using *
-                apply auto
-                done
+              moreover have "u \<le> v"
+                using uv p(2)[OF that] by auto
+              moreover have "u = a"
+                using p(2) p(3) that uv by force
+              ultimately show ?thesis
+                by blast
             qed
             have pb: "\<exists>v. k = cbox v b \<and> b \<ge> v" if "(b, k) \<in> p" for k
             proof -
               obtain u v where uv: "k = cbox u v"
                 using \<open>(b, k) \<in> p\<close> p(4) by blast
-              have *: "u \<le> v"
+              moreover have "u \<le> v"
                 using p(2)[OF that] unfolding uv by auto
-              have u: "v = b"
-              proof (rule ccontr)
-                have "u \<in> cbox u v"
-                  using p(2-3)[OF that(1)] unfolding uv by auto
-                have "v \<le> b"
-                  using p(2-3)[OF that(1)] unfolding uv subset_eq by auto
-                moreover assume "\<not> ?thesis"
-                ultimately have "v < b" by auto
-                then show False
-                  using p(2)[OF that(1)] unfolding uv by (auto simp add:)
-              qed
-              then show ?thesis
-                apply (rule_tac x=u in exI)
-                unfolding uv
-                using *
-                apply auto
-                done
+              moreover have "v = b"
+                using p(2) p(3) that uv by force
+              ultimately show ?thesis
+                by blast
             qed
             show "\<forall>x y. x \<in> ?B a \<and> y \<in> ?B a \<longrightarrow> x = y"
-              apply (rule,rule,rule,unfold split_paired_all)
-              unfolding mem_Collect_eq fst_conv snd_conv
-              apply safe
-            proof -
+            proof (safe; clarsimp)
               fix x k k'
               assume k: "(a, k) \<in> p" "(a, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
-              guess v using pa[OF k(1)] .. note v = conjunctD2[OF this]
-              guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = "min v v'"
+              obtain v where v: "k = cbox a v" "a \<le> v"
+                using pa[OF k(1)] by blast
+              obtain v' where v': "k' = cbox a v'" "a \<le> v'"
+                using pa[OF k(2)] by blast              
+              let ?v = "min v v'"
               have "box a ?v \<subseteq> k \<inter> k'"
                 unfolding v v' by (auto simp add: mem_box)
-              note interior_mono[OF this,unfolded interior_Int]
+              then have "interior (box a (min v v')) \<subseteq> interior k \<inter> interior k'"
+                using interior_Int interior_mono by blast
               moreover have "(a + ?v)/2 \<in> box a ?v"
                 using k(3-)
                 unfolding v v' content_eq_0 not_le
                 by (auto simp add: mem_box)
               ultimately have "(a + ?v)/2 \<in> interior k \<inter> interior k'"
                 unfolding interior_open[OF open_box] by auto
-              then have *: "k = k'"
-                apply -
-                apply (rule ccontr)
-                using p(5)[OF k(1-2)]
-                apply auto
-                done
-              { assume "x \<in> k" then show "x \<in> k'" unfolding * . }
-              { assume "x \<in> k'" then show "x \<in> k" unfolding * . }
+              then have eq: "k = k'"
+                using p(5)[OF k(1-2)] by auto
+              { assume "x \<in> k" then show "x \<in> k'" unfolding eq . }
+              { assume "x \<in> k'" then show "x \<in> k" unfolding eq . }
             qed
+
             show "\<forall>x y. x \<in> ?B b \<and> y \<in> ?B b \<longrightarrow> x = y"
-              apply rule
-              apply rule
-              apply rule
-              apply (unfold split_paired_all)
-              unfolding mem_Collect_eq fst_conv snd_conv
-              apply safe
-            proof -
+            proof (safe; clarsimp)
               fix x k k'
               assume k: "(b, k) \<in> p" "(b, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
-              guess v using pb[OF k(1)] .. note v = conjunctD2[OF this]
-              guess v' using pb[OF k(2)] .. note v' = conjunctD2[OF this]
+              obtain v where v: "k = cbox v b" "v \<le> b"
+                using pb[OF k(1)] by blast
+              obtain v' where v': "k' = cbox v' b" "v' \<le> b"
+                using pb[OF k(2)] by blast 
               let ?v = "max v v'"
               have "box ?v b \<subseteq> k \<inter> k'"
                 unfolding v v' by (auto simp: mem_box)
-                note interior_mono[OF this,unfolded interior_Int]
+              then have "interior (box (max v v') b) \<subseteq> interior k \<inter> interior k'"
+                using interior_Int interior_mono by blast
               moreover have " ((b + ?v)/2) \<in> box ?v b"
                 using k(3-) unfolding v v' content_eq_0 not_le by (auto simp: mem_box)
               ultimately have " ((b + ?v)/2) \<in> interior k \<inter> interior k'"
                 unfolding interior_open[OF open_box] by auto
-              then have *: "k = k'"
-                apply -
-                apply (rule ccontr)
-                using p(5)[OF k(1-2)]
-                apply auto
-                done
-              { assume "x \<in> k" then show "x \<in> k'" unfolding * . }
-              { assume "x \<in> k'" then show "x\<in>k" unfolding * . }
+              then have eq: "k = k'"
+                using p(5)[OF k(1-2)] by auto
+              { assume "x \<in> k" then show "x \<in> k'" unfolding eq . }
+              { assume "x \<in> k'" then show "x\<in>k" unfolding eq . }
             qed
 
-            let ?a = a and ?b = b (* a is something else while proofing the next theorem. *)
             have "norm (content c *\<^sub>R f' a - (f (Sup c) - f (Inf c))) \<le> e * (b - a) / 4"
               if "(a, c) \<in> p" and ne0: "content c \<noteq> 0" for c
             proof -
               obtain v where v: "c = cbox a v" and "a \<le> v"
                 using pa[OF \<open>(a, c) \<in> p\<close>] by metis 
-              then have "?a \<in> {?a..v}" "v \<le> ?b"
+              then have "a \<in> {a..v}" "v \<le> b"
                 using p(3)[OF \<open>(a, c) \<in> p\<close>] by auto
-              moreover have "{?a..v} \<subseteq> ball ?a da"
+              moreover have "{a..v} \<subseteq> ball a da"
                 using fineD[OF \<open>?d fine p\<close> \<open>(a, c) \<in> p\<close>] by (simp add: v split: if_split_asm)
               ultimately show ?thesis
                 unfolding v interval_bounds_real[OF \<open>a \<le> v\<close>] box_real
@@ -3994,9 +3956,9 @@
             proof -
               obtain v where v: "c = cbox v b" and "v \<le> b"
                 using \<open>(b, c) \<in> p\<close> pb by blast
-              then have "v \<ge> ?a""?b \<in> {v.. ?b}"  
+              then have "v \<ge> a""b \<in> {v.. b}"  
                 using p(3)[OF \<open>(b, c) \<in> p\<close>] by auto
-              moreover have "{v..?b} \<subseteq> ball ?b db"
+              moreover have "{v..b} \<subseteq> ball b db"
                 using fineD[OF \<open>?d fine p\<close> \<open>(b, c) \<in> p\<close>] box_real(2) v False by force
               ultimately show ?thesis
                 using db v by auto
@@ -4019,7 +3981,7 @@
         unfolding sum_distrib_left[symmetric]
         apply (subst additive_tagged_division_1[OF _ as(1)])
          apply (rule assms)
-        apply (rule **)
+        apply (rule norm_le)
         done
     qed
     show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b}"