# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1502100298 -7200
# Node ID d77a4ab4fe59e3704d778bfb83d55b5072fc93f9
# Parent  af5c71cffec57e87fa0369f68fa2d6052ea24046
more Henstock_Kurzweil_Integration cleanup

diff -r af5c71cffec5 -r d77a4ab4fe59 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Aug 06 22:54:17 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Aug 07 12:04:58 2017 +0200
@@ -2470,53 +2470,39 @@
 proof safe
   fix a b :: 'b
   show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
-    if "box a b = {}"
+    if "box a b = {}" for a b
     apply (rule_tac x=f in exI)
-    using assms that
-    apply (auto simp: content_eq_0_interior)
-    done
+    using assms that by (auto simp: content_eq_0_interior)
   {
-    fix c g
-    fix k :: 'b
-    assume as: "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" "g integrable_on cbox a b"
+    fix c g and k :: 'b
+    assume fg: "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" and g: "g integrable_on cbox a b"
     assume k: "k \<in> Basis"
     show "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
-      "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
-      apply (rule_tac[!] x=g in exI)
-      using as(1) integrable_split[OF as(2) k]
-      apply auto
-      done
+         "\<exists>g. (\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
+       apply (rule_tac[!] x=g in exI)
+      using fg integrable_split[OF g k] by auto
   }
-  fix c k g1 g2
-  assume as: "\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e" "g1 integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
-    "\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g2 x) \<le> e" "g2 integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}"
-  assume k: "k \<in> Basis"
-  let ?g = "\<lambda>x. if x\<bullet>k = c then f x else if x\<bullet>k \<le> c then g1 x else g2 x"
   show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
-    apply (rule_tac x="?g" in exI)
-    apply safe
-  proof goal_cases
-    case (1 x)
-    then show ?case
-      apply -
-      apply (cases "x\<bullet>k=c")
-      apply (case_tac "x\<bullet>k < c")
-      using as assms
-      apply auto
-      done
-  next
-    case 2
-    presume "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
-      and "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
-    then guess h1 h2 unfolding integrable_on_def by auto
-    from has_integral_split[OF this k] show ?case
-      unfolding integrable_on_def by auto
-  next
-    show "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
-      apply(rule_tac[!] integrable_spike[OF negligible_standard_hyperplane[of k c]])
-      using k as(2,4)
-      apply auto
-      done
+    if fg1: "\<forall>x\<in>cbox a b \<inter> {x. x \<bullet> k \<le> c}. norm (f x - g1 x) \<le> e" 
+      and g1: "g1 integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}"
+      and fg2: "\<forall>x\<in>cbox a b \<inter> {x. c \<le> x \<bullet> k}. norm (f x - g2 x) \<le> e" 
+      and g2: "g2 integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}" 
+      and k: "k \<in> Basis"
+    for c k g1 g2
+  proof -
+    let ?g = "\<lambda>x. if x\<bullet>k = c then f x else if x\<bullet>k \<le> c then g1 x else g2 x"
+    show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
+    proof (intro exI conjI ballI)
+      show "norm (f x - ?g x) \<le> e" if "x \<in> cbox a b" for x
+        by (auto simp: that assms fg1 fg2)
+      show "?g integrable_on cbox a b"
+      proof -
+        have "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c}" "?g integrable_on cbox a b \<inter> {x. x \<bullet> k \<ge> c}"
+          by(rule integrable_spike[OF negligible_standard_hyperplane[of k c]], use k g1 g2 in auto)+
+        with has_integral_split[OF _ _ k] show ?thesis
+          unfolding integrable_on_def by blast
+      qed
+    qed
   qed
 qed
 
@@ -2531,18 +2517,16 @@
 lemma approximable_on_division:
   fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
   assumes "0 \<le> e"
-    and "d division_of (cbox a b)"
-    and "\<forall>i\<in>d. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i"
+    and d: "d division_of (cbox a b)"
+    and f: "\<forall>i\<in>d. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i"
   obtains g where "\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e" "g integrable_on cbox a b"
 proof -
-  note * = comm_monoid_set.operative_division[OF comm_monoid_set_and operative_approximable[OF assms(1)] assms(2)]
-  from assms(3) this[unfolded comm_monoid_set_F_and, of f] division_of_finite[OF assms(2)]
-  guess g by auto
-  then show thesis
-    apply -
-    apply (rule that[of g])
-    apply auto
-    done
+  note * = comm_monoid_set.operative_division
+             [OF comm_monoid_set_and operative_approximable[OF \<open>0 \<le> e\<close>] d]
+  have "finite d"
+    by (rule division_of_finite[OF d])
+  with f *[unfolded comm_monoid_set_F_and, of f] that show thesis
+    by auto
 qed
 
 lemma integrable_continuous:
@@ -3608,8 +3592,8 @@
 lemma fundamental_theorem_of_calculus_interior:
   fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
   assumes "a \<le> b"
-    and "continuous_on {a .. b} f"
-    and "\<forall>x\<in>{a <..< b}. (f has_vector_derivative f'(x)) (at x)"
+    and contf: "continuous_on {a .. b} f"
+    and derf: "\<And>x. x \<in> {a <..< b} \<Longrightarrow> (f has_vector_derivative f'(x)) (at x)"
   shows "(f' has_integral (f b - f a)) {a .. b}"
 proof -
   {
@@ -3637,22 +3621,22 @@
   { presume "\<And>e. e > 0 \<Longrightarrow> ?P e" then show ?thesis unfolding has_integral_factor_content_real by auto }
   fix e :: real
   assume e: "e > 0"
-  note assms(3)[unfolded has_vector_derivative_def has_derivative_at_alt ball_conj_distrib]
-  note conjunctD2[OF this]
-  note bounded=this(1) and this(2)
-  from this(2) have "\<forall>x\<in>box a b. \<exists>d>0. \<forall>y. norm (y - x) < d \<longrightarrow>
-    norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e/2 * norm (y - x)"
-    apply -
-    apply safe
-    apply (erule_tac x=x in ballE)
-    apply (erule_tac x="e/2" in allE)
-    using e
-    apply auto
-    done
-  note this[unfolded bgauge_existence_lemma]
-  from choice[OF this] guess d ..
-  note conjunctD2[OF this[rule_format]]
-  note d = this[rule_format]
+  note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt]
+  have bounded: "\<And>x. x \<in> {a<..<b} \<Longrightarrow> bounded_linear (\<lambda>u. u *\<^sub>R f' x)"
+    using derf_exp by simp
+  have "\<forall>x \<in> box a b. \<exists>d>0. \<forall>y. norm (y - x) < d \<longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e/2 * norm (y - x)"
+       (is "\<forall>x \<in> box a b. ?Q x")
+  proof
+    fix x assume x: "x \<in> box a b"
+    show "?Q x"
+      apply (rule allE [where x="e/2", OF derf_exp [THEN conjunct2, of x]])
+      using x e by auto
+  qed
+  from this [unfolded bgauge_existence_lemma]
+  obtain d where d: "\<And>x. 0 < d x"
+     "\<And>x y. \<lbrakk>x \<in> box a b; norm (y - x) < d x\<rbrakk>
+               \<Longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e / 2 * norm (y - x)"
+    by metis
   have "bounded (f ` cbox a b)"
     apply (rule compact_imp_bounded compact_continuous_image)+
     using compact_cbox assms
@@ -3683,7 +3667,7 @@
         apply (auto simp add: field_simps)
         done
     qed
-    then guess l .. note l = conjunctD2[OF this]
+    then obtain l where l: "0 < l" "norm (l *\<^sub>R f' a) \<le> e * (b - a) / 8" by metis
     show ?thesis
       apply (rule_tac x="min k l" in exI)
       apply safe
@@ -3698,24 +3682,28 @@
         by (rule norm_triangle_ineq4)
       also have "\<dots> \<le> e * (b - a) / 8 + e * (b - a) / 8"
       proof (rule add_mono)
-        have "\<bar>c - a\<bar> \<le> \<bar>l\<bar>"
-          using as' by auto
-        then show "norm ((c - a) *\<^sub>R f' a) \<le> e * (b - a) / 8"
-          apply -
-          apply (rule order_trans[OF _ l(2)])
+        have "norm ((c - a) *\<^sub>R f' a) \<le> norm (l *\<^sub>R f' a)"
           unfolding norm_scaleR
           apply (rule mult_right_mono)
-          apply auto
-          done
+          using as' by auto
+        also have "... \<le> e * (b - a) / 8"
+          by (rule l)
+        finally show "norm ((c - a) *\<^sub>R f' a) \<le> e * (b - a) / 8" .
       next
-        show "norm (f c - f a) \<le> e * (b - a) / 8"
-          apply (rule less_imp_le)
-          apply (cases "a = c")
-          defer
-          apply (rule k(2)[unfolded dist_norm])
-          using as' e ab
-          apply (auto simp add: field_simps)
-          done
+        have "norm (f c - f a) < e * (b - a) / 8"
+        proof (cases "a = c")
+          case True
+          then show ?thesis
+            using \<open>0 < e * (b - a) / 8\<close> by auto
+        next
+          case False
+          show ?thesis
+            apply (rule k(2)[unfolded dist_norm])
+            using as' False
+             apply (auto simp add: field_simps)
+            done
+        qed
+        then show "norm (f c - f a) \<le> e * (b - a) / 8" by simp
       qed
       finally show "norm (content {a .. c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b - a) / 4"
         unfolding content_real[OF as(1)] by auto
@@ -3804,7 +3792,7 @@
     note p = tagged_division_ofD[OF as(1)]
     have pA: "p = (p \<inter> ?A) \<union> (p - ?A)" "finite (p \<inter> ?A)" "finite (p - ?A)" "(p \<inter> ?A) \<inter> (p - ?A) = {}"
       using as by auto
-    note * = additive_tagged_division_1'[OF assms(1) as(1), symmetric]
+    note * = additive_tagged_division_1[OF assms(1) as(1), symmetric]
     have **: "\<And>n1 s1 n2 s2::real. n2 \<le> s2 / 2 \<Longrightarrow> n1 - s1 \<le> s2 / 2 \<Longrightarrow> n1 + n2 \<le> s1 + s2"
       by arith
     show ?case
@@ -3964,7 +3952,8 @@
             qed
             have pb: "\<exists>v. k = cbox v b \<and> b \<ge> v" if "(b, k) \<in> p" for k
             proof -
-              guess u v using p(4)[OF that] by (elim exE) note uv=this
+              obtain u v where uv: "k = cbox u v"
+                using \<open>(b, k) \<in> p\<close> p(4) by blast
               have *: "u \<le> v"
                 using p(2)[OF that] unfolding uv by auto
               have u: "v = b"
diff -r af5c71cffec5 -r d77a4ab4fe59 src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Sun Aug 06 22:54:17 2017 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy	Mon Aug 07 12:04:58 2017 +0200
@@ -1836,15 +1836,6 @@
 lemma bgauge_existence_lemma: "(\<forall>x\<in>s. \<exists>d::real. 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. x\<in>s \<longrightarrow> q d x)"
   by (meson zero_less_one)
 
-lemma additive_tagged_division_1':
-  fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
-  assumes "a \<le> b"
-    and "p tagged_division_of {a..b}"
-  shows "sum (\<lambda>(x,k). f (Sup k) - f(Inf k)) p = f b - f a"
-  using additive_tagged_division_1[OF _ assms(2), of f]
-  using assms(1)
-  by auto
-
 subsection \<open>Fine-ness of a partition w.r.t. a gauge.\<close>
 
 definition fine  (infixr "fine" 46)