# HG changeset patch
# User paulson
# Date 1502044887 -7200
# Node ID 3817ee41236d3753339324c7f78545fc28255765
# Parent  8bf96de5019366491b1b2785f25fbc0bb060924c# Parent  a6c9d7206853c66a9c00047c0156953b5d50edc5
merged

diff -r 8bf96de50193 -r 3817ee41236d src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Aug 06 18:56:47 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Aug 06 20:41:27 2017 +0200
@@ -2669,18 +2669,22 @@
 lemma fundamental_theorem_of_calculus:
   fixes f :: "real \<Rightarrow> 'a::banach"
   assumes "a \<le> b"
-    and "\<forall>x\<in>{a .. b}. (f has_vector_derivative f' x) (at x within {a .. b})"
+    and vecd: "\<forall>x\<in>{a .. b}. (f has_vector_derivative f' x) (at x within {a .. b})"
   shows "(f' has_integral (f b - f a)) {a .. b}"
   unfolding has_integral_factor_content box_real[symmetric]
 proof safe
   fix e :: real
-  assume e: "e > 0"
-  note assm = assms(2)[unfolded has_vector_derivative_def has_derivative_within_alt]
-  have *: "\<And>P Q. \<forall>x\<in>{a .. b}. P x \<and> (\<forall>e>0. \<exists>d>0. Q x e d) \<Longrightarrow> \<forall>x. \<exists>(d::real)>0. x\<in>{a .. b} \<longrightarrow> Q x e d"
-    using e by blast
-  note this[OF assm,unfolded gauge_existence_lemma]
-  from choice[OF this,unfolded Ball_def[symmetric]] guess d ..
-  note d=conjunctD2[OF this[rule_format],rule_format]
+  assume "e > 0"
+  then have "\<forall>x. \<exists>d>0.
+         x \<in> {a..b} \<longrightarrow>
+         (\<forall>y\<in>{a..b}.
+             norm (y - x) < d \<longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e * norm (y - x))"
+    using vecd[unfolded has_vector_derivative_def has_derivative_within_alt] by blast
+  then obtain d where d: "\<And>x. 0 < d x"
+                 "\<And>x y. \<lbrakk>x \<in> {a..b}; y \<in> {a..b}; norm (y - x) < d x\<rbrakk>
+                        \<Longrightarrow> norm (f y - f x - (y - x) *\<^sub>R f' x) \<le> e * norm (y - x)"
+    by metis
+  
   show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
     norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content (cbox a b))"
     apply (rule_tac x="\<lambda>x. ball x (d x)" in exI)
@@ -2701,7 +2705,7 @@
       fix x k
       assume "(x, k) \<in> p"
       note xk = tagged_division_ofD(2-4)[OF as(1) this]
-      from this(3) guess u v by (elim exE) note k=this
+      then obtain u v where k: "k = cbox u v" by blast
       have *: "u \<le> v"
         using xk unfolding k by auto
       have ball: "\<forall>xa\<in>k. xa \<in> ball x (d x)"
@@ -2907,10 +2911,9 @@
       done
   }
   assume noteq: "{k \<in> s. content k \<noteq> 0} \<noteq> s"
-  then obtain k where k: "k \<in> s" "content k = 0"
-    by auto
-  from s(4)[OF k(1)] guess c d by (elim exE) note k=k this
-  from k have "card s > 0"
+  then obtain k c d where k: "k \<in> s" "content k = 0" "k = cbox c d"
+    using s(4) by blast
+  then have "card s > 0"
     unfolding card_gt_0_iff using assm(1) by auto
   then have card: "card (s - {k}) < card s"
     using assm(1) k(1)
@@ -2933,9 +2936,9 @@
     fix x
     fix e :: real
     assume as: "x \<in> k" "e > 0"
-    from k(2)[unfolded k content_eq_0] guess i ..
-    then have i:"c\<bullet>i = d\<bullet>i" "i\<in>Basis"
-      using s(3)[OF k(1),unfolded k] unfolding box_ne_empty by auto
+    obtain i where i: "c\<bullet>i = d\<bullet>i" "i\<in>Basis"
+      using k(2) s(3)[OF k(1)] unfolding box_ne_empty k
+      by (metis dual_order.antisym content_eq_0) 
     then have xi: "x\<bullet>i = d\<bullet>i"
       using as unfolding k mem_box by (metis antisym)
     define y where "y = (\<Sum>j\<in>Basis. (if j = i then if c\<bullet>i \<le> (a\<bullet>i + b\<bullet>i) / 2 then c\<bullet>i +
@@ -3114,42 +3117,30 @@
     f integrable_on cbox u v"
   shows "f integrable_on cbox a b"
 proof -
-  have "\<forall>x. \<exists>d. x\<in>cbox a b \<longrightarrow> d>0 \<and> (\<forall>u v. x \<in> cbox u v \<and> cbox u v \<subseteq> ball x d \<and> cbox u v \<subseteq> cbox a b \<longrightarrow>
+  have "\<forall>x. \<exists>d>0. x\<in>cbox a b \<longrightarrow> (\<forall>u v. x \<in> cbox u v \<and> cbox u v \<subseteq> ball x d \<and> cbox u v \<subseteq> cbox a b \<longrightarrow>
     f integrable_on cbox u v)"
-    using assms by auto
-  note this[unfolded gauge_existence_lemma]
-  from choice[OF this] guess d .. note d=this[rule_format]
-  guess p
-    apply (rule fine_division_exists[OF gauge_ball_dependent,of d a b])
-    using d
+    using assms by (metis zero_less_one)
+  then obtain d where d: "\<And>x. 0 < d x"
+     "\<And>x u v. \<lbrakk>x \<in> cbox a b; x \<in> cbox u v; cbox u v \<subseteq> ball x (d x); cbox u v \<subseteq> cbox a b\<rbrakk> 
+               \<Longrightarrow> f integrable_on cbox u v"
+    by metis
+  obtain p where p: "p tagged_division_of cbox a b" "(\<lambda>x. ball x (d x)) fine p"
+    using fine_division_exists[OF gauge_ball_dependent,of d a b] d(1) by blast 
+  then have sndp: "snd ` p division_of cbox a b"
+    by (metis division_of_tagged_division)
+  have "f integrable_on k" if "(x, k) \<in> p" for x k
+    using tagged_division_ofD(2-4)[OF p(1) that] fineD[OF p(2) that] d[of x] by auto
+  then show ?thesis
+    unfolding comm_monoid_set.operative_division[OF comm_monoid_set_and operative_integrable sndp,  symmetric]
+              comm_monoid_set_F_and
     by auto
-  note p=this(1-2)
-  note division_of_tagged_division[OF this(1)]
-  note * = comm_monoid_set.operative_division[OF comm_monoid_set_and operative_integrable, OF this, symmetric, of f]
-  show ?thesis
-    unfolding * comm_monoid_set_F_and
-    apply safe
-    unfolding snd_conv
-  proof -
-    fix x k
-    assume "(x, k) \<in> p"
-    note tagged_division_ofD(2-4)[OF p(1) this] fineD[OF p(2) this]
-    then show "f integrable_on k"
-      apply safe
-      apply (rule d[THEN conjunct2,rule_format,of x])
-      apply (auto intro: order.trans)
-      done
-  qed
 qed
 
 
 subsection \<open>Second FTC or existence of antiderivative.\<close>
 
 lemma integrable_const[intro]: "(\<lambda>x. c) integrable_on cbox a b"
-  unfolding integrable_on_def
-  apply rule
-  apply (rule has_integral_const)
-  done
+  unfolding integrable_on_def by blast
 
 lemma integral_has_vector_derivative_continuous_at:
   fixes f :: "real \<Rightarrow> 'a::banach"
@@ -3239,22 +3230,18 @@
   assumes "continuous_on {a .. b} f"
   obtains g where "\<forall>u\<in>{a .. b}. \<forall>v \<in> {a .. b}. u \<le> v \<longrightarrow> (f has_integral (g v - g u)) {u .. v}"
 proof -
-  from antiderivative_continuous[OF assms] guess g . note g=this
-  show ?thesis
-    apply (rule that[of g])
-    apply safe
-  proof goal_cases
-    case prems: (1 u v)
+  obtain g 
+    where g: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative f x) (at x within {a..b})" 
+    using  antiderivative_continuous[OF assms] by metis
+  have "(f has_integral g v - g u) {u..v}" if "u \<in> {a..b}" "v \<in> {a..b}" "u \<le> v" for u v
+  proof -
     have "\<forall>x\<in>cbox u v. (g has_vector_derivative f x) (at x within cbox u v)"
-      apply rule
-      apply (rule has_vector_derivative_within_subset)
-      apply (rule g[rule_format])
-      using prems(1,2)
-      apply auto
-      done
-    then show ?case
-      using fundamental_theorem_of_calculus[OF prems(3), of g f] by auto
+      by (meson g has_vector_derivative_within_subset interval_subset_is_interval is_interval_closed_interval subsetCE that(1) that(2))
+    then show ?thesis
+      by (simp add: fundamental_theorem_of_calculus that(3))
   qed
+  then show ?thesis
+    using that by blast
 qed
 
 
@@ -3268,7 +3255,7 @@
     and "\<forall>u v. \<exists>w z. g ` cbox u v = cbox w z"
     and h: "\<forall>u v. \<exists>w z. h ` cbox u v = cbox w z"
     and "\<forall>u v. content(g ` cbox u v) = r * content (cbox u v)"
-    and "(f has_integral i) (cbox a b)"
+    and intfi: "(f has_integral i) (cbox a b)"
   shows "((\<lambda>x. f(g x)) has_integral (1 / r) *\<^sub>R i) (h ` cbox a b)"
 proof -
   show ?thesis when *: "cbox a b \<noteq> {} \<Longrightarrow> ?thesis"
@@ -3282,22 +3269,11 @@
       unfolding prems assms(8)[unfolded prems has_integral_empty_eq] by auto
   qed
   assume "cbox a b \<noteq> {}"
-  from assms(6)[rule_format,of a b] guess w z by (elim exE) note wz=this
+  obtain w z where wz: "h ` cbox a b = cbox w z"
+    using h by blast
   have inj: "inj g" "inj h"
-    unfolding inj_on_def
-    apply safe
-    apply(rule_tac[!] ccontr)
-    using assms(2)
-    apply(erule_tac x=x in allE)
-    using assms(2)
-    apply(erule_tac x=y in allE)
-    defer
-    using assms(3)
-    apply (erule_tac x=x in allE)
-    using assms(3)
-    apply(erule_tac x=y in allE)
-    apply auto
-    done
+    apply (metis assms(2) injI)
+    by (metis assms(3) injI)
   from h obtain ha hb where h_eq: "h ` cbox a b = cbox ha hb" by blast
   show ?thesis
     unfolding h_eq has_integral
@@ -3305,12 +3281,17 @@
   proof safe
     fix e :: real
     assume e: "e > 0"
-    with assms(1) have "e * r > 0" by simp
-    from assms(8)[unfolded has_integral,rule_format,OF this] guess d by (elim exE conjE) note d=this[rule_format]
+    with \<open>0 < r\<close> have "e * r > 0" by simp
+    with intfi[unfolded has_integral]
+    obtain d where d: "gauge d"
+                   "\<And>p. p tagged_division_of cbox a b \<and> d fine p 
+                        \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i) < e * r" 
+      by metis
     define d' where "d' x = {y. g y \<in> d (g x)}" for x
     have d': "\<And>x. d' x = {y. g y \<in> (d (g x))}"
       unfolding d'_def ..
-    show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of h ` cbox a b \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)"
+    show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of h ` cbox a b \<and> d fine p 
+              \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)"
     proof (rule_tac x=d' in exI, safe)
       show "gauge d'"
         using d(1)
@@ -3377,16 +3358,10 @@
         assume "x \<in> cbox a b"
         then have "h x \<in>  \<Union>{k. \<exists>x. (x, k) \<in> p}"
           using p(6) by auto
-        then guess X unfolding Union_iff .. note X=this
-        from this(1) guess y unfolding mem_Collect_eq ..
+        then obtain X y where "h x \<in> X" "(y, X) \<in> p" by blast
         then show "x \<in> \<Union>{k. \<exists>x. (x, k) \<in> (\<lambda>(x, k). (g x, g ` k)) ` p}"
-          apply -
-          apply (rule_tac X="g ` X" in UnionI)
-          defer
-          apply (rule_tac x="h x" in image_eqI)
-          using X(2) assms(3)[rule_format,of x]
-          apply auto
-          done
+          apply (clarsimp simp: )
+          by (metis (no_types, lifting) assms(3) image_eqI pair_imageI)
       qed
         note ** = d(2)[OF this]
         have *: "inj_on (\<lambda>(x, k). (g x, g ` k)) p"
@@ -3676,8 +3651,9 @@
     using compact_cbox assms
     apply auto
     done
-  from this[unfolded bounded_pos] guess B .. note B = this[rule_format]
-
+  from this[unfolded bounded_pos] obtain B 
+    where "0 < B" and B: "\<And>x. x \<in> f ` cbox a b \<Longrightarrow> norm x \<le> B"
+    by metis
   have "\<exists>da. 0 < da \<and> (\<forall>c. a \<le> c \<and> {a .. c} \<subseteq> {a .. b} \<and> {a .. c} \<subseteq> ball a da \<longrightarrow>
     norm (content {a .. c} *\<^sub>R f' a - (f c - f a)) \<le> (e * (b - a)) / 4)"
   proof -
@@ -3748,20 +3724,23 @@
     note assms(2)[unfolded continuous_on_eq_continuous_within,rule_format,OF this]
     note * = this[unfolded continuous_within Lim_within,rule_format] have "(e * (b - a)) / 8 > 0"
       using e ab by (auto simp add: field_simps)
-    from *[OF this] guess k .. note k = conjunctD2[OF this,rule_format]
-    have "\<exists>l. 0 < l \<and> norm (l *\<^sub>R f' b) \<le> (e * (b - a)) / 8"
+    from *[OF this] obtain k
+      where k: "0 < k"
+               "\<And>x. \<lbrakk>x \<in> {a..b}; 0 < dist x b \<and> dist x b < k\<rbrakk>
+                    \<Longrightarrow> dist (f x) (f b) < e * (b - a) / 8"
+      by blast
+    obtain l where l: "0 < l" "norm (l *\<^sub>R f' b) \<le> (e * (b - a)) / 8"
     proof (cases "f' b = 0")
       case True
-      thus ?thesis using ab e by auto
+      thus ?thesis using ab e that by auto
     next
       case False
       then show ?thesis
-        apply (rule_tac x="(e * (b - a)) / 8 / norm (f' b)" in exI)
+        apply (rule_tac l="(e * (b - a)) / 8 / norm (f' b)" in that)
         using ab e
         apply (auto simp add: field_simps)
         done
     qed
-    then guess l .. note l = conjunctD2[OF this]
     show ?thesis
       apply (rule_tac x="min k l" in exI)
       apply safe
@@ -3842,11 +3821,12 @@
         assume xk: "(x, k) \<in> p"
           "e * (Sup k -  Inf k) / 2 <
             norm (content k *\<^sub>R f' x - (f (Sup k) - f (Inf k)))"
-        from p(4)[OF this(1)] guess u v by (elim exE) note k=this
+        obtain u v where k: "k = cbox u v"
+          using p(4) xk(1) by blast
         then have "u \<le> v" and uv: "{u, v} \<subseteq> cbox u v"
           using p(2)[OF xk(1)] by auto
-        note result = xk(2)[unfolded k box_real interval_bounds_real[OF this(1)] content_real[OF this(1)]]
-
+        then have result: "e * (v - u) / 2 < norm ((v - u) *\<^sub>R f' x - (f v - f u))"
+          using xk(2)[unfolded k box_real interval_bounds_real content_real] by auto
         assume as': "x \<noteq> a" "x \<noteq> b"
         then have "x \<in> box a b"
           using p(2-3)[OF xk(1)] by (auto simp: mem_box)
@@ -3910,7 +3890,8 @@
           assume "(x, k) \<in> p \<inter> {t. fst t \<in> {a, b}} - p \<inter> {t. fst t \<in> {a, b} \<and> content (snd t) \<noteq> 0}"
           then have xk: "(x, k) \<in> p" "content k = 0"
             by auto
-          from p(4)[OF xk(1)] guess u v by (elim exE) note uv=this
+          then obtain u v where uv: "k = cbox u v"
+            using p(4) by blast
           have "k \<noteq> {}"
             using p(2)[OF xk(1)] by auto
           then have *: "u = v"
@@ -3952,9 +3933,10 @@
             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 -
-              guess u v using p(4)[OF that] by (elim exE) note uv=this
-              have *: "u \<le> v"
-                using p(2)[OF that] unfolding uv by auto
+              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"