# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1502010622 -7200
# Node ID a6c9d7206853c66a9c00047c0156953b5d50edc5
# Parent  c828efcb95f3179f2077efce4a599e5976950a34
further cleanup of "guess"

diff -r c828efcb95f3 -r a6c9d7206853 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Aug 06 10:41:15 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Aug 06 11:10:22 2017 +0200
@@ -3727,21 +3727,20 @@
     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
+                    \<Longrightarrow> dist (f x) (f b) < e * (b - a) / 8"
       by blast
-    have "\<exists>l. 0 < l \<and> norm (l *\<^sub>R f' b) \<le> (e * (b - a)) / 8"
+    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
@@ -3822,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)
@@ -3890,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"
@@ -3932,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"