# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1498572613 -3600
# Node ID 994322c172745fa4950e89b9748599bc8504bdf2
# Parent  4a5589dd8e1a8747fc63a0a499d2df6beb1bb996
Removed more "guess", etc.

diff -r 4a5589dd8e1a -r 994322c17274 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue Jun 27 00:07:34 2017 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue Jun 27 15:10:13 2017 +0100
@@ -1770,19 +1770,11 @@
           unfolding p'_def by auto
         then obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "k = i \<inter> l" by blast
         then show "\<exists>y i l. (x, k) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
-          apply (rule_tac x=x in exI)
-          apply (rule_tac x=i in exI)
-          apply (rule_tac x=l in exI)
-          using p'(2)[OF il(3)]
-          apply auto
-          done
+          using p'(2) by fastforce
       qed
       have sum_p': "(\<Sum>(x, k)\<in>p'. norm (integral k f)) = (\<Sum>k\<in>snd ` p'. norm (integral k f))"
         apply (subst sum.over_tagged_division_lemma[OF p'',of "\<lambda>k. norm (integral k f)"])
-        unfolding norm_eq_zero
-         apply (rule integral_null)
-        apply (simp add: content_eq_0_interior)
-        apply rule
+         apply (auto intro: integral_null simp: content_eq_0_interior)
         done
       note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
 
@@ -1849,11 +1841,7 @@
             case prems: (1 l y)
             have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
               apply (subst(2) interior_Int)
-              apply (rule Int_greatest)
-              defer
-              apply (subst prems(4))
-              apply auto
-              done
+              by (metis Int_lower2 Int_subset_iff interior_mono prems(4))
             then have *: "interior (k \<inter> l) = {}"
               using snd_p(5)[OF prems(1-3)] by auto
             from d'(4)[OF k] snd_p(4)[OF prems(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
@@ -1894,16 +1882,7 @@
           have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
             using as by auto
           then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
-            apply -
-            apply (erule disjE)
-            apply (rule disjI2)
-            apply (rule d'(5))
-            prefer 4
-            apply (rule disjI1)
-            apply (rule *)
-            using as
-            apply auto
-            done
+            by (metis Pair_inject \<open>k1 \<in> snd ` p\<close> \<open>l1 \<in> d\<close> as(4) d'(5) snd_p(5))
           moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
             using as(2) by auto
           ultimately have "interior(l1 \<inter> k1) = {}"
@@ -1934,14 +1913,13 @@
           case (1 x a b)
           then show ?case
             unfolding p'_def
-            apply safe
-            apply (rule_tac x=i in exI)
-            apply (rule_tac x=l in exI)
-            unfolding snd_conv image_iff
-            apply safe
-            apply (rule_tac x="(a,l)" in bexI)
-            apply auto
-            done
+          proof -
+            assume "(a, b) \<in> {(x, k) |x k. \<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l}"
+            then have "\<exists>n N. (a, b) = (n, N) \<and> (\<exists>Na Nb. n \<in> Na \<and> Na \<in> d \<and> (n, Nb) \<in> p \<and> N = Na \<inter> Nb)"
+              by force
+            then show ?thesis
+              by (metis (no_types) image_iff snd_conv)
+          qed
         qed
         finally show ?case .
       next
@@ -2019,15 +1997,7 @@
           note xl = p'(2-4)[OF this]
           from this(3) guess u v by (elim exE) note uv=this
           have "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar>) = (\<Sum>k\<in>d. content (k \<inter> cbox u v))"
-            apply (rule sum.cong)
-            apply (rule refl)
-            apply (drule d'(4))
-            apply safe
-            apply (subst Int_commute)
-            unfolding Int_interval uv
-            apply (subst abs_of_nonneg)
-            apply auto
-            done
+            by (simp add: Int_commute uv)
           also have "\<dots> = sum content {k \<inter> cbox u v| k. k \<in> d}"
             unfolding Setcompr_eq_image
             apply (rule sum.reindex_nontrivial [unfolded o_def, symmetric])
@@ -2095,13 +2065,11 @@
     by (intro bdd_aboveI2[where M=B] assms(2)[rule_format]) simp
   note D = D_1 D_2
   let ?S = "SUP d:?D. ?f d"
-  have f_int: "\<And>a b. f absolutely_integrable_on cbox a b"
+  have "\<And>a b. f integrable_on cbox a b"
+    using assms(1) integrable_on_subcbox by blast
+  then have f_int: "\<And>a b. f absolutely_integrable_on cbox a b"
     apply (rule bounded_variation_absolutely_integrable_interval[where B=B])
-    apply (rule integrable_on_subcbox[OF assms(1)])
-    defer
-    apply safe
-    apply (rule assms(2)[rule_format])
-    apply auto
+    using assms(2) apply blast
     done
   have "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
     apply (subst has_integral_alt')
diff -r 4a5589dd8e1a -r 994322c17274 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Jun 27 00:07:34 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Jun 27 15:10:13 2017 +0100
@@ -11,7 +11,6 @@
 
 (*FIXME DELETE*)
 lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
-lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
 
 (* try instead structured proofs below *)
 lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
@@ -1570,11 +1569,11 @@
 lemma has_integral_component_le:
   fixes f g :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes k: "k \<in> Basis"
-  assumes "(f has_integral i) s" "(g has_integral j) s"
-    and "\<forall>x\<in>s. (f x)\<bullet>k \<le> (g x)\<bullet>k"
+  assumes "(f has_integral i) S" "(g has_integral j) S"
+    and f_le_g: "\<And>x. x \<in> S \<Longrightarrow> (f x)\<bullet>k \<le> (g x)\<bullet>k"
   shows "i\<bullet>k \<le> j\<bullet>k"
 proof -
-  have lem: "i\<bullet>k \<le> j\<bullet>k"
+  have ik_le_jk: "i\<bullet>k \<le> j\<bullet>k"
     if f_i: "(f has_integral i) (cbox a b)"
     and g_j: "(g has_integral j) (cbox a b)"
     and le: "\<forall>x\<in>cbox a b. (f x)\<bullet>k \<le> (g x)\<bullet>k"
@@ -1583,25 +1582,29 @@
     assume "\<not> ?thesis"
     then have *: "0 < (i\<bullet>k - j\<bullet>k) / 3"
       by auto
-    guess d1 using f_i[unfolded has_integral,rule_format,OF *] by (elim exE conjE) note d1=this[rule_format]
-    guess d2 using g_j[unfolded has_integral,rule_format,OF *] by (elim exE conjE) note d2=this[rule_format]
-    obtain p where p: "p tagged_division_of cbox a b" "d1 fine p" "d2 fine p"
-       using fine_division_exists[OF gauge_Int[OF d1(1) d2(1)], of a b] unfolding fine_Int
+    obtain \<gamma>1 where "gauge \<gamma>1" 
+      and \<gamma>1: "\<And>p. \<lbrakk>p tagged_division_of cbox a b; \<gamma>1 fine p\<rbrakk>
+                \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i) < (i \<bullet> k - j \<bullet> k) / 3"
+      using f_i[unfolded has_integral,rule_format,OF *] by fastforce 
+    obtain \<gamma>2 where "gauge \<gamma>2" 
+      and \<gamma>2: "\<And>p. \<lbrakk>p tagged_division_of cbox a b; \<gamma>2 fine p\<rbrakk>
+                \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - j) < (i \<bullet> k - j \<bullet> k) / 3"
+      using g_j[unfolded has_integral,rule_format,OF *] by fastforce 
+    obtain p where p: "p tagged_division_of cbox a b" and "\<gamma>1 fine p" "\<gamma>2 fine p"
+       using fine_division_exists[OF gauge_Int[OF \<open>gauge \<gamma>1\<close> \<open>gauge \<gamma>2\<close>], of a b] unfolding fine_Int
        by metis
-    note le_less_trans[OF Basis_le_norm[OF k]]
     then have "\<bar>((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i) \<bullet> k\<bar> < (i \<bullet> k - j \<bullet> k) / 3"
-              "\<bar>((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - j) \<bullet> k\<bar> < (i \<bullet> k - j \<bullet> k) / 3"
-      using  k norm_bound_Basis_lt d1 d2 p
-      by blast+
+         "\<bar>((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - j) \<bullet> k\<bar> < (i \<bullet> k - j \<bullet> k) / 3"
+      using le_less_trans[OF Basis_le_norm[OF k]] k \<gamma>1 \<gamma>2 by metis+ 
     then show False
       unfolding inner_simps
-      using rsum_component_le[OF p(1)] le
-      by (force simp add: abs_real_def split: if_split_asm)
+      using rsum_component_le[OF p] le
+      by (fastforce simp add: abs_real_def split: if_split_asm)
   qed
   show ?thesis
-  proof (cases "\<exists>a b. s = cbox a b")
+  proof (cases "\<exists>a b. S = cbox a b")
     case True
-    with lem assms show ?thesis
+    with ik_le_jk assms show ?thesis
       by auto
   next
     case False
@@ -1610,22 +1613,34 @@
       assume "\<not> i\<bullet>k \<le> j\<bullet>k"
       then have ij: "(i\<bullet>k - j\<bullet>k) / 3 > 0"
         by auto
-      note has_integral_altD[OF _ False this]
-      from this[OF assms(2)] this[OF assms(3)] guess B1 B2 . note B=this[rule_format]
+      obtain B1 where "0 < B1" 
+           and B1: "\<And>a b. ball 0 B1 \<subseteq> cbox a b \<Longrightarrow>
+                    \<exists>z. ((\<lambda>x. if x \<in> S then f x else 0) has_integral z) (cbox a b) \<and>
+                        norm (z - i) < (i \<bullet> k - j \<bullet> k) / 3"
+        using has_integral_altD[OF _ False ij] assms by blast
+      obtain B2 where "0 < B2" 
+           and B2: "\<And>a b. ball 0 B2 \<subseteq> cbox a b \<Longrightarrow>
+                    \<exists>z. ((\<lambda>x. if x \<in> S then g x else 0) has_integral z) (cbox a b) \<and>
+                        norm (z - j) < (i \<bullet> k - j \<bullet> k) / 3"
+        using has_integral_altD[OF _ False ij] assms by blast
       have "bounded (ball 0 B1 \<union> ball (0::'a) B2)"
         unfolding bounded_Un by(rule conjI bounded_ball)+
-      from bounded_subset_cbox[OF this] guess a b by (elim exE)
-      then have ab: "ball 0 B1 \<subseteq> cbox a b" "ball 0 B2 \<subseteq> cbox a b"
+      from bounded_subset_cbox[OF this] 
+      obtain a b::'a where ab: "ball 0 B1 \<subseteq> cbox a b" "ball 0 B2 \<subseteq> cbox a b"
         by blast+
-      guess w1 using B(2)[OF ab(1)] .. note w1=conjunctD2[OF this]
-      guess w2 using B(4)[OF ab(2)] .. note w2=conjunctD2[OF this]
+      then obtain w1 w2 where int_w1: "((\<lambda>x. if x \<in> S then f x else 0) has_integral w1) (cbox a b)"
+                        and norm_w1:  "norm (w1 - i) < (i \<bullet> k - j \<bullet> k) / 3"
+                        and int_w2: "((\<lambda>x. if x \<in> S then g x else 0) has_integral w2) (cbox a b)"
+                        and norm_w2: "norm (w2 - j) < (i \<bullet> k - j \<bullet> k) / 3"
+        using B1 B2 by blast
       have *: "\<And>w1 w2 j i::real .\<bar>w1 - i\<bar> < (i - j) / 3 \<Longrightarrow> \<bar>w2 - j\<bar> < (i - j) / 3 \<Longrightarrow> w1 \<le> w2 \<Longrightarrow> False"
         by (simp add: abs_real_def split: if_split_asm)
-      note le_less_trans[OF Basis_le_norm[OF k]]
-      note this[OF w1(2)] this[OF w2(2)]
+      have "\<bar>(w1 - i) \<bullet> k\<bar> < (i \<bullet> k - j \<bullet> k) / 3"
+           "\<bar>(w2 - j) \<bullet> k\<bar> < (i \<bullet> k - j \<bullet> k) / 3"
+        using Basis_le_norm k le_less_trans norm_w1 norm_w2 by blast+
       moreover
       have "w1\<bullet>k \<le> w2\<bullet>k"
-        by (rule lem[OF w1(1) w2(1)]) (simp add: assms(4))
+        using ik_le_jk int_w1 int_w2 f_le_g by auto
       ultimately show False
         unfolding inner_simps by(rule *)
     qed
@@ -1635,9 +1650,9 @@
 lemma integral_component_le:
   fixes g f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "k \<in> Basis"
-    and "f integrable_on s" "g integrable_on s"
-    and "\<forall>x\<in>s. (f x)\<bullet>k \<le> (g x)\<bullet>k"
-  shows "(integral s f)\<bullet>k \<le> (integral s g)\<bullet>k"
+    and "f integrable_on S" "g integrable_on S"
+    and "\<And>x. x \<in> S \<Longrightarrow> (f x)\<bullet>k \<le> (g x)\<bullet>k"
+  shows "(integral S f)\<bullet>k \<le> (integral S g)\<bullet>k"
   apply (rule has_integral_component_le)
   using integrable_integral assms
   apply auto
@@ -1646,8 +1661,8 @@
 lemma has_integral_component_nonneg:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "k \<in> Basis"
-    and "(f has_integral i) s"
-    and "\<forall>x\<in>s. 0 \<le> (f x)\<bullet>k"
+    and "(f has_integral i) S"
+    and "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> (f x)\<bullet>k"
   shows "0 \<le> i\<bullet>k"
   using has_integral_component_le[OF assms(1) has_integral_0 assms(2)]
   using assms(3-)
@@ -1656,9 +1671,9 @@
 lemma integral_component_nonneg:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "k \<in> Basis"
-    and  "\<forall>x\<in>s. 0 \<le> (f x)\<bullet>k"
-  shows "0 \<le> (integral s f)\<bullet>k"
-proof (cases "f integrable_on s")
+    and  "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> (f x)\<bullet>k"
+  shows "0 \<le> (integral S f)\<bullet>k"
+proof (cases "f integrable_on S")
   case True show ?thesis
     apply (rule has_integral_component_nonneg)
     using assms True
@@ -1671,8 +1686,8 @@
 lemma has_integral_component_neg:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "k \<in> Basis"
-    and "(f has_integral i) s"
-    and "\<forall>x\<in>s. (f x)\<bullet>k \<le> 0"
+    and "(f has_integral i) S"
+    and "\<And>x. x \<in> S \<Longrightarrow> (f x)\<bullet>k \<le> 0"
   shows "i\<bullet>k \<le> 0"
   using has_integral_component_le[OF assms(1,2) has_integral_0] assms(2-)
   by auto
@@ -2149,7 +2164,11 @@
         by (meson Max_ge as(1) dual_order.trans finite_imageI tagged_division_of_finite)
       have "\<forall>i. \<exists>q. q tagged_division_of (cbox a b) \<and> (d i) fine q \<and> (\<forall>(x, k)\<in>p. k \<subseteq> (d i) x \<longrightarrow> (x, k) \<in> q)"
         by (auto intro: tagged_division_finer[OF as(1) d(1)])
-      from choice[OF this] guess q .. note q=conjunctD3[OF this[rule_format]]
+      from choice[OF this] 
+      obtain q where q: "\<And>n. q n tagged_division_of cbox a b"
+                      "\<And>n. d n fine q n"
+                      "\<And>n x k. \<lbrakk>(x, k) \<in> p; k \<subseteq> d n x\<rbrakk> \<Longrightarrow> (x, k) \<in> q n"
+        by fastforce
       have *: "\<And>i. (\<Sum>(x, k)\<in>q i. content k *\<^sub>R indicator s x) \<ge> (0::real)"
         apply (rule sum_nonneg)
         apply safe
@@ -2159,14 +2178,7 @@
         done
       have **: "finite s \<Longrightarrow> finite t \<Longrightarrow> (\<forall>(x,y) \<in> t. (0::real) \<le> g(x,y)) \<Longrightarrow>
         (\<forall>y\<in>s. \<exists>x. (x,y) \<in> t \<and> f(y) \<le> g(x,y)) \<Longrightarrow> sum f s \<le> sum g t" for f g s t
-        apply (rule sum_le_included[of s t g snd f])
-        prefer 4
-        apply safe
-        apply (erule_tac x=x in ballE)
-        apply (erule exE)
-        apply (rule_tac x="(xa,x)" in bexI)
-        apply auto
-        done
+        by (rule sum_le_included[of s t g snd f]; force)
       have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) \<le> sum (\<lambda>i. (real i + 1) *
         norm (sum (\<lambda>(x,k). content k *\<^sub>R indicator s x :: real) (q i))) {..N+1}"
         unfolding real_norm_def sum_distrib_left abs_of_nonneg[OF *] diff_0_right
@@ -2228,13 +2240,7 @@
         qed
         ultimately show "\<exists>y. (y, x, k) \<in> {(i, j) |i j. i \<in> {..N + 1} \<and> j \<in> q i} \<and> norm (content k *\<^sub>R f x) \<le>
           (real y + 1) * (content k *\<^sub>R indicator s x)"
-          apply (rule_tac x=n in exI)
-          apply safe
-          apply (rule_tac x=n in exI)
-          apply (rule_tac x="(x,k)" in exI)
-          apply safe
-          apply auto
-          done
+          by force
       qed (insert as, auto)
       also have "\<dots> \<le> sum (\<lambda>i. e / 2 / 2 ^ i) {..N+1}"
       proof (rule sum_mono, goal_cases)