# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1503924041 -3600
# Node ID c485474cd91dff8915d6d4a83fb55777bf842865
# Parent  8a6ce2d9a9f54f8862f2a6a6f223d9f6c7c8bc8f
Giant cleanup of fundamental_theorem_of_calculus_interior

diff -r 8a6ce2d9a9f5 -r c485474cd91d src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Aug 28 00:12:07 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Aug 28 13:40:41 2017 +0100
@@ -3758,7 +3758,7 @@
         let ?C = "{t \<in> p. fst t \<in> {a, b} \<and> content (snd t) \<noteq> 0}"
         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"
         proof -
-          have *: "\<And>s f e. sum f s = sum f (p \<inter> ?C) \<Longrightarrow> norm (sum f (p \<inter> ?C)) \<le> e \<Longrightarrow> norm (sum f s) \<le> e"
+          have *: "\<And>S f e. sum f S = sum f (p \<inter> ?C) \<Longrightarrow> norm (sum f (p \<inter> ?C)) \<le> e \<Longrightarrow> norm (sum f S) \<le> e"
             by auto
           have 1: "content K *\<^sub>R (f' x) - (f ((Sup K)) - f ((Inf K))) = 0"
             if "(x,K) \<in> p \<inter> {t. fst t \<in> {a, b}} - p \<inter> ?C" for x K
@@ -3774,39 +3774,36 @@
           qed
           have 2: "norm(\<Sum>(x,K)\<in>p \<inter> ?C. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))  \<le> e * (b-a)/2"
           proof -
-            have *: "p \<inter> ?C = ?B a \<union> ?B b"
-              by blast
-            have norm_le: "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
-            proof (cases "s = {}")
+            have norm_le: "norm (sum f S) \<le> e"
+              if "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x = y" "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> e" "e > 0"
+              for S f and e :: real
+            proof (cases "S = {}")
               case True
               with that show ?thesis by auto
             next
-              case False then obtain x where "x \<in> s"
+              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
+                using \<open>x \<in> S\<close> that(2) by auto
             qed
-            show "norm (\<Sum>(x,k)\<in>p \<inter> ?C.
-                        content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b-a)/2"
-              apply (subst *)
+            have *: "p \<inter> ?C = ?B a \<union> ?B b"
+              by blast
+            then have "norm (\<Sum>(x,K)\<in>p \<inter> ?C. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) =
+                       norm (\<Sum>(x,K) \<in> ?B a \<union> ?B b. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))"
+              by simp
+            also have "... = norm ((\<Sum>(x,K) \<in> ?B a. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) + 
+                                   (\<Sum>(x,K) \<in> ?B b. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))))"
               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] norm_le)
-
-            proof -
+              using p(1) ab e by auto
+            also have "... \<le> e * (b - a) / 4 + e * (b - a) / 4"
+            proof (rule norm_triangle_le [OF add_mono])
               have pa: "\<exists>v. k = cbox a v \<and> a \<le> v" if "(a, k) \<in> p" for k
                 using p(2) p(3) p(4) that by fastforce
-              have pb: "\<exists>v. k = cbox v b \<and> b \<ge> v" if "(b, k) \<in> p" for k
-                using p(2) p(3) p(4) that by fastforce
-              show "\<forall>x y. x \<in> ?B a \<and> y \<in> ?B a \<longrightarrow> x = y"
-              proof (safe; clarsimp)
-                fix x K K'
+              show "norm (\<Sum>(x,K) \<in> ?B a. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) \<le> e * (b - a) / 4"
+              proof (intro norm_le; clarsimp)
+                fix K K'
                 assume K: "(a, K) \<in> p" "(a, K') \<in> p" and ne0: "content K \<noteq> 0" "content K' \<noteq> 0"
                 with pa obtain v v' where v: "K = cbox a v" "a \<le> v" and v': "K' = cbox a v'" "a \<le> v'"
                   by blast
@@ -3820,14 +3817,31 @@
                   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 eq: "K = K'"
+                then show "K = K'"
                   using p(5)[OF K] by auto
-                then show "x \<in> K \<Longrightarrow> x \<in> K'" "x \<in> K' \<Longrightarrow> x \<in> K" 
-                  using eq by auto
-              qed
-              show "\<forall>x y. x \<in> ?B b \<and> y \<in> ?B b \<longrightarrow> x = y"
-              proof (safe; clarsimp)
-                fix x K K'
+              next
+                fix K 
+                assume K: "(a, K) \<in> p" and ne0: "content K \<noteq> 0"
+                show "norm (content c *\<^sub>R f' a - (f (Sup c) - f (Inf c))) * 4 \<le> e * (b-a)"
+                  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"
+                    using p(3)[OF \<open>(a, c) \<in> p\<close>] by auto
+                  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
+                    using da \<open>a \<le> v\<close> by auto
+                qed
+              qed (use ab e in auto)
+            next
+              have pb: "\<exists>v. k = cbox v b \<and> b \<ge> v" if "(b, k) \<in> p" for k
+                using p(2) p(3) p(4) that by fastforce
+              show "norm (\<Sum>(x,K) \<in> ?B b. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) \<le> e * (b - a) / 4"
+              proof (intro norm_le; clarsimp)
+                fix K K'
                 assume K: "(b, K) \<in> p" "(b, K') \<in> p" and ne0: "content K \<noteq> 0" "content K' \<noteq> 0"
                 with pb obtain v v' where v: "K = cbox v b" "v \<le> b" and v': "K' = cbox v' b" "v' \<le> b"
                   by blast
@@ -3840,31 +3854,14 @@
                   using ne0 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 eq: "K = K'"
+                then show "K = K'"
                   using p(5)[OF K] by auto
-                then show "x \<in> K \<Longrightarrow> x \<in> K'" "x \<in> K' \<Longrightarrow> x \<in> K" 
-                  using eq by auto
-              qed
-              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"
-                  using p(3)[OF \<open>(a, c) \<in> p\<close>] by auto
-                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
-                  using da \<open>a \<le> v\<close> by auto
-              qed
-              then show "\<forall>x. x \<in> ?B a \<longrightarrow> norm ((\<lambda>(x, k). content k *\<^sub>R f' x - (f (Sup k) -
-              f (Inf k))) x) \<le> e * (b-a) / 4"
-                by auto
-
-              have "norm (content c *\<^sub>R f' b - (f (Sup c) - f (Inf c))) \<le> e * (b-a) / 4"
-                if "(b, c) \<in> p" and ne0: "content c \<noteq> 0" for c
-              proof -
+              next
+                fix K 
+                assume K: "(b, K) \<in> p" and ne0: "content K \<noteq> 0"
+                show "norm (content c *\<^sub>R f' b - (f (Sup c) - f (Inf c))) * 4 \<le> e * (b-a)"
+                  if "(b, c) \<in> p" and ne0: "content c \<noteq> 0" for c
+                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}"  
@@ -3873,12 +3870,13 @@
                   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
-              qed
-              then show "\<forall>x. x \<in> ?B b \<longrightarrow> 
-                           norm ((\<lambda>(x, k). content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) x) 
-                           \<le> e * (b-a) / 4"
-                by auto
-            qed (insert p(1) ab e, auto simp add: field_simps)
+                qed
+              qed (use ab e in auto)
+            qed
+            also have "... = e * (b-a)/2"
+              by simp
+            finally show "norm (\<Sum>(x,k)\<in>p \<inter> ?C.
+                        content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b-a)/2" .
           qed
           show "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x - (f ((Sup k)) - f ((Inf k)))) \<le> e * (b-a)/2"
             apply (rule * [OF sum.mono_neutral_right[OF pA(2)]])
@@ -4006,109 +4004,101 @@
     by (meson gauge_def open_contains_ball)
 
   let ?d = "min k (c - a)/2"
-  show ?thesis
+  show thesis
   proof (intro that[of ?d] allI impI, safe)
     show "?d > 0"
-      using \<open>0 < k\<close> using assms(2) by auto
+      using \<open>0 < k\<close> \<open>a < c\<close> by auto
+  next
     fix t
-    assume as: "c - ?d < t" "t \<le> c"
-    let ?thesis = "norm (integral ({a..c}) f - integral ({a..t}) f) < e"
-    {
-      presume *: "t < c \<Longrightarrow> ?thesis"
-      show ?thesis
-      proof (cases "t = c")
-        case True
-        then show ?thesis
-          by (simp add: \<open>e > 0\<close>)
+    assume t: "c - ?d < t" "t \<le> c"
+    show "norm (integral ({a..c}) f - integral ({a..t}) f) < e"
+    proof (cases "t < c")
+      case False with \<open>t \<le> c\<close> show ?thesis
+        by (simp add: \<open>e > 0\<close>)
+    next
+      case True
+      have "f integrable_on {a..t}"
+        apply (rule integrable_subinterval_real[OF intf])
+        using \<open>t < c\<close> \<open>c \<le> b\<close> by auto
+      then obtain d2 where d2: "gauge d2"
+        "\<And>p. p tagged_division_of {a..t} \<and> d2 fine p \<Longrightarrow> norm (?SUM p - integral {a..t} f) < e/3"
+        using integrable_integral has_integral_real e3 by metis
+      define d3 where "d3 x = (if x \<le> t then d1 x \<inter> d2 x else d1 x)" for x
+      have "gauge d3"
+        using \<open>gauge d1\<close> \<open>gauge d2\<close> unfolding d3_def gauge_def by auto
+      then obtain p where ptag: "p tagged_division_of {a..t}" and pfine: "d3 fine p"
+        by (metis box_real(2) fine_division_exists)
+      note p' = tagged_division_ofD[OF ptag]
+      have pt: "(x,K)\<in>p \<Longrightarrow> x \<le> t" for x K
+        by (meson atLeastAtMost_iff p'(2) p'(3) subsetCE)
+      with pfine have "d2 fine p"
+        unfolding fine_def d3_def by fastforce
+      then have d2_fin: "norm (?SUM p - integral {a..t} f) < e/3"
+        using d2(2) ptag by auto
+      have eqs: "{a..c} \<inter> {x. x \<le> t} = {a..t}" "{a..c} \<inter> {x. x \<ge> t} = {t..c}"
+        using t by (auto simp add: field_simps)
+      have "p \<union> {(c, {t..c})} tagged_division_of {a..c}"
+        apply (rule tagged_division_Un_interval_real[of _ _ _ 1 "t"])
+        using  \<open>t \<le> c\<close> by (auto simp: eqs ptag tagged_division_of_self_real)
+      moreover
+      have "d1 fine p \<union> {(c, {t..c})}"
+        unfolding fine_def
+      proof safe
+        fix x K y
+        assume "(x,K) \<in> p" and "y \<in> K" then show "y \<in> d1 x"
+          by (metis Int_iff d3_def subsetD fineD pfine)
       next
-        case False
-        then show ?thesis
-          using "*" \<open>t \<le> c\<close> by linarith
+        fix x assume "x \<in> {t..c}"
+        then have "dist c x < k"
+          using t(1) by (auto simp add: field_simps dist_real_def)
+        with k show "x \<in> d1 c"
+          unfolding d_def by auto
+      qed  
+      ultimately have d1_fin: "norm (?SUM(p \<union> {(c, {t..c})}) - integral {a..c} f) < e/3"
+        using d1 by metis
+      have SUMEQ: "?SUM(p \<union> {(c, {t..c})}) = (c - t) *\<^sub>R f c + ?SUM p"
+      proof -
+        have "?SUM(p \<union> {(c, {t..c})}) = (content{t..c} *\<^sub>R f c) + ?SUM p"
+        proof (subst sum.union_disjoint)
+          show "p \<inter> {(c, {t..c})} = {}"
+            using \<open>t < c\<close> pt by force
+        qed (use p'(1) in auto)
+        also have "... = (c - t) *\<^sub>R f c + ?SUM p"
+          using \<open>t \<le> c\<close> by auto
+        finally show ?thesis .
       qed
-    }
-    assume "t < c"
-
-    have "f integrable_on {a..t}"
-      apply (rule integrable_subinterval_real[OF intf])
-      using \<open>t < c\<close> \<open>c \<le> b\<close> by auto
-    then obtain d2 where d2: "gauge d2"
-      "\<And>p. p tagged_division_of {a..t} \<and> d2 fine p \<Longrightarrow> norm (?SUM p - integral {a..t} f) < e/3"
-      using integrable_integral has_integral_real e3 by metis
-    define d3 where "d3 x = (if x \<le> t then d1 x \<inter> d2 x else d1 x)" for x
-    have "gauge d3"
-      using \<open>gauge d1\<close> \<open>gauge d2\<close> unfolding d3_def gauge_def by auto
-    then obtain p where ptag: "p tagged_division_of {a..t}" and pfine: "d3 fine p"
-      by (metis box_real(2) fine_division_exists)
-    note p'=tagged_division_ofD[OF ptag]
-    have pt: "(x,k)\<in>p \<Longrightarrow> x \<le> t" for x k
-      by (meson atLeastAtMost_iff p'(2) p'(3) subsetCE)
-    with pfine have "d2 fine p"
-      unfolding fine_def d3_def by fastforce
-    then have d2_fin: "norm (?SUM p - integral {a..t} f) < e/3"
-      using d2(2) ptag by auto
-    have eqs: "{a..c} \<inter> {x. x \<le> t} = {a..t}" "{a..c} \<inter> {x. x \<ge> t} = {t..c}"
-      using as by (auto simp add: field_simps)
-    have "p \<union> {(c, {t..c})} tagged_division_of {a..c}"
-      apply (rule tagged_division_Un_interval_real[of _ _ _ 1 "t"])
-      using  \<open>t \<le> c\<close> by (auto simp: eqs ptag tagged_division_of_self_real)
-    moreover
-    have "d1 fine p \<union> {(c, {t..c})}"
-      unfolding fine_def
-    proof safe
-      fix x K y
-      assume "(x,K) \<in> p" and "y \<in> K" then show "y \<in> d1 x"
-        by (metis Int_iff d3_def subsetD fineD pfine)
-    next
-      fix x assume "x \<in> {t..c}"
-      then have "dist c x < k"
-        using as(1) by (auto simp add: field_simps dist_real_def)
-      with k show "x \<in> d1 c"
-        unfolding d_def by auto
-    qed  
-    ultimately have d1_fin: "norm (?SUM(p \<union> {(c, {t..c})}) - integral {a..c} f) < e/3"
-      using d1 by metis
-    have 1: "integral {a..c} f - integral {a..t} f = -(((c - t) *\<^sub>R f c + ?SUM p) -
+      have "c - k < t"
+        using \<open>k>0\<close> t(1) by (auto simp add: field_simps)
+      moreover have "k \<le> w"
+      proof (rule ccontr)
+        assume "\<not> k \<le> w"
+        then have "c + (k + w) / 2 \<notin> d c"
+          by (auto simp add: field_simps not_le not_less dist_real_def d_def)
+        then have "c + (k + w) / 2 \<notin> ball c k"
+          using k by blast
+        then show False
+          using \<open>0 < w\<close> \<open>\<not> k \<le> w\<close> dist_real_def by auto
+      qed
+      ultimately have cwt: "c - w < t"
+        by (auto simp add: field_simps)
+      have eq: "integral {a..c} f - integral {a..t} f = -(((c - t) *\<^sub>R f c + ?SUM p) -
              integral {a..c} f) + (?SUM p - integral {a..t} f) + (c - t) *\<^sub>R f c"
-    and 2: "e = (e/3 + e/3) + e/3"
-      by auto
-    have **: "?SUM(p \<union> {(c, {t..c})}) = (c - t) *\<^sub>R f c + ?SUM p"
-    proof -
-      have "?SUM(p \<union> {(c, {t..c})}) = (content{t..c} *\<^sub>R f c) + ?SUM p"
-      proof (subst sum.union_disjoint)
-        show "p \<inter> {(c, {t..c})} = {}"
-          using \<open>t < c\<close> pt by force
-      qed (use p'(1) in auto)
-      also have "... = (c - t) *\<^sub>R f c + ?SUM p"
-        using \<open>t \<le> c\<close> by auto
-      finally show ?thesis .
+        by auto
+      have "norm (integral {a..c} f - integral {a..t} f) < e/3 + e/3 + e/3"
+        unfolding eq
+      proof (intro norm_triangle_lt add_strict_mono)
+        show "norm (- ((c - t) *\<^sub>R f c + ?SUM p - integral {a..c} f)) < e/3"
+          by (metis SUMEQ d1_fin norm_minus_cancel)
+        show "norm (?SUM p - integral {a..t} f) < e/3"
+          using d2_fin by blast
+        show "norm ((c - t) *\<^sub>R f c) < e/3"
+          using w cwt \<open>t < c\<close> by (auto simp add: field_simps)
+      qed
+      then show ?thesis by simp
     qed
-    have "c - k < t"
-      using \<open>k>0\<close> as(1) by (auto simp add: field_simps)
-    moreover have "k \<le> w"
-    proof (rule ccontr)
-      assume "\<not> k \<le> w"
-      then have "c + (k + w) / 2 \<notin> d c"
-        by (auto simp add: field_simps not_le not_less dist_real_def d_def)
-      then have "c + (k + w) / 2 \<notin> ball c k"
-        using k by blast
-      then show False
-        using \<open>0 < w\<close> \<open>\<not> k \<le> w\<close> dist_real_def by auto
-    qed
-    ultimately have cwt: "c - w < t"
-      by (auto simp add: field_simps)
-    show ?thesis
-      unfolding 1 
-      apply (subst 2)
-      apply (rule norm_triangle_lt add_strict_mono)+
-      apply (metis "**" d1_fin norm_minus_cancel)
-      using d2_fin apply blast
-      using w cwt \<open>t < c\<close>
-      apply (auto simp add: field_simps)
-      done
   qed
 qed
 
-
 lemma indefinite_integral_continuous_right:
   fixes f :: "real \<Rightarrow> 'a::banach"
   assumes "f integrable_on {a..b}"