# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1501789085 -7200
# Node ID 9786b06c7b5ad1d1a4fe67e6e6490d38156f35a2
# Parent  b66e0e5941a2efa8722be56cc1522bc46c9d80a7
eliminated more "guess", etc.

diff -r b66e0e5941a2 -r 9786b06c7b5a src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Aug 03 14:15:25 2017 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Aug 03 21:38:05 2017 +0200
@@ -7,6 +7,24 @@
   imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure Set_Integral
 begin
 
+lemma finite_product_dependent: (*FIXME DELETE*)
+  assumes "finite s"
+    and "\<And>x. x \<in> s \<Longrightarrow> finite (t x)"
+  shows "finite {(i, j) |i j. i \<in> s \<and> j \<in> t i}"
+  using assms
+proof induct
+  case (insert x s)
+  have *: "{(i, j) |i j. i \<in> insert x s \<and> j \<in> t i} =
+    (\<lambda>y. (x,y)) ` (t x) \<union> {(i, j) |i j. i \<in> s \<and> j \<in> t i}" by auto
+  show ?case
+    unfolding *
+    apply (rule finite_UnI)
+    using insert
+    apply auto
+    done
+qed auto
+
+
 lemma le_left_mono: "x \<le> y \<Longrightarrow> y \<le> a \<longrightarrow> x \<le> (a::'a::preorder)"
   by (auto intro: order_trans)
 
@@ -1633,11 +1651,16 @@
       then show "\<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
         by force
     qed
-    from choice[OF this] guess k .. note k=conjunctD2[OF this[rule_format],rule_format]
-
+    then obtain k where k: "\<And>x. 0 < k x"
+                       "\<And>i x. \<lbrakk>i \<in> d; x \<notin> i\<rbrakk> \<Longrightarrow> ball x (k x) \<inter> i = {}"
+      by metis
     have "e/2 > 0"
       using e by auto
-    from henstock_lemma[OF assms(1) this] guess g . note g=this[rule_format]
+    from henstock_lemma[OF assms(1) this] 
+    obtain g where g: "gauge g"
+          "\<And>p. \<lbrakk>p tagged_partial_division_of cbox a b; g fine p\<rbrakk> 
+                \<Longrightarrow> (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
+      by (metis (no_types, lifting))      
     let ?g = "\<lambda>x. g x \<inter> ball x (k x)"
     show ?case
       apply (rule_tac x="?g" in exI)
@@ -1716,15 +1739,12 @@
           assume y: "y \<in> cbox a b"
           then have "\<exists>x l. (x, l) \<in> p \<and> y\<in>l"
             unfolding p'(6)[symmetric] by auto
-          then guess x l by (elim exE) note xl=conjunctD2[OF this]
+          then obtain x l where xl: "(x, l) \<in> p" "y \<in> l" by metis
           then have "\<exists>k. k \<in> d \<and> y \<in> k"
             using y unfolding d'(6)[symmetric] by auto
-          then guess i .. note i = conjunctD2[OF this]
+          then obtain i where i: "i \<in> d" "y \<in> i" by metis
           have "x \<in> i"
-            using fineD[OF p(3) xl(1)]
-            using k(2)[OF i(1), of x]
-            using i(2) xl(2)
-            by auto
+            using fineD[OF p(3) xl(1)] using k(2) i xl by auto
           then show "y \<in> \<Union>{k. \<exists>x. (x, k) \<in> p'}"
             unfolding p'_def Union_iff
             apply (rule_tac x="i \<inter> l" in bexI)
@@ -1735,12 +1755,7 @@
       qed
 
       then have "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
-        apply -
-        apply (rule g(2)[rule_format])
-        unfolding tagged_division_of_def
-        apply safe
-        apply (rule gp')
-        done
+        using g(2) gp' tagged_division_of_def by blast
       then have **: "\<bar>(\<Sum>(x,k)\<in>p'. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p'. norm (integral k f))\<bar> < e / 2"
         unfolding split_def
         using p''
diff -r b66e0e5941a2 -r 9786b06c7b5a src/HOL/Analysis/Lebesgue_Integral_Substitution.thy
--- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Thu Aug 03 14:15:25 2017 +0200
+++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Thu Aug 03 21:38:05 2017 +0200
@@ -13,23 +13,6 @@
 begin
 
 
-lemma finite_product_dependent: (*FIXME DELETE*)
-  assumes "finite s"
-    and "\<And>x. x \<in> s \<Longrightarrow> finite (t x)"
-  shows "finite {(i, j) |i j. i \<in> s \<and> j \<in> t i}"
-  using assms
-proof induct
-  case (insert x s)
-  have *: "{(i, j) |i j. i \<in> insert x s \<and> j \<in> t i} =
-    (\<lambda>y. (x,y)) ` (t x) \<union> {(i, j) |i j. i \<in> s \<and> j \<in> t i}" by auto
-  show ?case
-    unfolding *
-    apply (rule finite_UnI)
-    using insert
-    apply auto
-    done
-qed auto
-
 lemma nn_integral_substitution_aux:
   fixes f :: "real \<Rightarrow> ennreal"
   assumes Mf: "f \<in> borel_measurable borel"