# HG changeset patch
# User wenzelm
# Date 1502038607 -7200
# Node ID 8bf96de5019366491b1b2785f25fbc0bb060924c
# Parent  882abe912da90969a000e7631f4fdbd59756e004# Parent  6e114edae18b5015988d85b2ddcf782387950616
merged

diff -r 6e114edae18b -r 8bf96de50193 NEWS
--- a/NEWS	Sun Aug 06 18:51:32 2017 +0200
+++ b/NEWS	Sun Aug 06 18:56:47 2017 +0200
@@ -116,6 +116,11 @@
 
 *** HOL ***
 
+* Command and antiquotation "value" with modified default strategy:
+terms without free variables are always evaluated using plain evaluation
+only, with no fallback on normalization by evaluation.
+Minor INCOMPATIBILITY.
+
 * Notions of squarefreeness, n-th powers, and prime powers in
 HOL-Computational_Algebra and HOL-Number_Theory.
 
diff -r 6e114edae18b -r 8bf96de50193 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Aug 06 18:51:32 2017 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Aug 06 18:56:47 2017 +0200
@@ -1,30 +1,13 @@
 (*  Title:      HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
     Author:     Johannes Hölzl, TU München
     Author:     Robert Himmelmann, TU München
+    Huge cleanup by LCP
 *)
 
 theory Equivalence_Lebesgue_Henstock_Integration
   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)
 
@@ -90,7 +73,7 @@
   obtain d
     where "gauge d"
       and integral_f: "\<forall>p. p tagged_division_of cbox x y \<and> d fine p \<longrightarrow>
-        norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - I) < e"
+        norm ((\<Sum>(x,k) \<in> p. content k *\<^sub>R f x) - I) < e"
     using \<open>0<e\<close> f unfolding has_integral by auto
 
   define C where "C X m = X \<inter> {x. ball x (1/Suc m) \<subseteq> d x}" for X m
@@ -194,14 +177,14 @@
         then show "\<Union>{k. \<exists>x. (x, k) \<in> ?p} = cbox x y"
           using p(1) by auto
       qed
-      ultimately have I: "norm ((\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) - I) < e"
+      ultimately have I: "norm ((\<Sum>(x,k) \<in> ?p. content k *\<^sub>R f x) - I) < e"
         using integral_f by auto
 
-      have "(\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) =
-        (\<Sum>(x, k)\<in>?T ` (p \<inter> s). content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p - s. content k *\<^sub>R f x)"
+      have "(\<Sum>(x,k) \<in> ?p. content k *\<^sub>R f x) =
+        (\<Sum>(x,k) \<in> ?T ` (p \<inter> s). content k *\<^sub>R f x) + (\<Sum>(x,k) \<in> p - s. content k *\<^sub>R f x)"
         using p(1)[THEN tagged_division_ofD(1)]
         by (safe intro!: sum.union_inter_neutral) (auto simp: s_def T_def)
-      also have "(\<Sum>(x, k)\<in>?T ` (p \<inter> s). content k *\<^sub>R f x) = (\<Sum>(x, k)\<in>p \<inter> s. content k *\<^sub>R f (T X k))"
+      also have "(\<Sum>(x,k) \<in> ?T ` (p \<inter> s). content k *\<^sub>R f x) = (\<Sum>(x,k) \<in> p \<inter> s. content k *\<^sub>R f (T X k))"
       proof (subst sum.reindex_nontrivial, safe)
         fix x1 x2 k assume 1: "(x1, k) \<in> p" "(x1, k) \<in> s" and 2: "(x2, k) \<in> p" "(x2, k) \<in> s"
           and eq: "content k *\<^sub>R f (T X k) \<noteq> 0"
@@ -209,8 +192,8 @@
         show "x1 = x2"
           by (auto simp: content_eq_0_interior)
       qed (use p in \<open>auto intro!: sum.cong\<close>)
-      finally have eq: "(\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) =
-        (\<Sum>(x, k)\<in>p \<inter> s. content k *\<^sub>R f (T X k)) + (\<Sum>(x, k)\<in>p - s. content k *\<^sub>R f x)" .
+      finally have eq: "(\<Sum>(x,k) \<in> ?p. content k *\<^sub>R f x) =
+        (\<Sum>(x,k) \<in> p \<inter> s. content k *\<^sub>R f (T X k)) + (\<Sum>(x,k) \<in> p - s. content k *\<^sub>R f x)" .
 
       have in_T: "(x, k) \<in> s \<Longrightarrow> T X k \<in> X" for x k
         using in_s[of x k] by (auto simp: C_def)
@@ -224,7 +207,7 @@
     have [simp]: "finite p"
       using tagged_division_ofD(1)[OF p(1)] .
 
-    have "(M - 3*e) * (b - a) \<le> (\<Sum>(x, k)\<in>p \<inter> s. content k) * (b - a)"
+    have "(M - 3*e) * (b - a) \<le> (\<Sum>(x,k) \<in> p \<inter> s. content k) * (b - a)"
     proof (intro mult_right_mono)
       have fin: "?\<mu> (E \<inter> \<Union>{k\<in>snd`p. k \<inter> C X m = {}}) < \<infinity>" for X
         using \<open>?\<mu> E < \<infinity>\<close> by (rule le_less_trans[rotated]) (auto intro!: emeasure_mono \<open>E \<in> sets ?L\<close>)
@@ -287,15 +270,15 @@
       finally show "M - 3 * e \<le> (\<Sum>(x, y)\<in>p \<inter> s. content y)"
         using \<open>0 < e\<close> by (simp add: split_beta)
     qed (use \<open>a < b\<close> in auto)
-    also have "\<dots> = (\<Sum>(x, k)\<in>p \<inter> s. content k * (b - a))"
+    also have "\<dots> = (\<Sum>(x,k) \<in> p \<inter> s. content k * (b - a))"
       by (simp add: sum_distrib_right split_beta')
-    also have "\<dots> \<le> (\<Sum>(x, k)\<in>p \<inter> s. content k * (f (T ?F k) - f (T ?E k)))"
+    also have "\<dots> \<le> (\<Sum>(x,k) \<in> p \<inter> s. content k * (f (T ?F k) - f (T ?E k)))"
       using parts(3) by (auto intro!: sum_mono mult_left_mono diff_mono)
-    also have "\<dots> = (\<Sum>(x, k)\<in>p \<inter> s. content k * f (T ?F k)) - (\<Sum>(x, k)\<in>p \<inter> s. content k * f (T ?E k))"
+    also have "\<dots> = (\<Sum>(x,k) \<in> p \<inter> s. content k * f (T ?F k)) - (\<Sum>(x,k) \<in> p \<inter> s. content k * f (T ?E k))"
       by (auto intro!: sum.cong simp: field_simps sum_subtractf[symmetric])
-    also have "\<dots> = (\<Sum>(x, k)\<in>?B. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>?A. content k *\<^sub>R f x)"
+    also have "\<dots> = (\<Sum>(x,k) \<in> ?B. content k *\<^sub>R f x) - (\<Sum>(x,k) \<in> ?A. content k *\<^sub>R f x)"
       by (subst (1 2) parts) auto
-    also have "\<dots> \<le> norm ((\<Sum>(x, k)\<in>?B. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>?A. content k *\<^sub>R f x))"
+    also have "\<dots> \<le> norm ((\<Sum>(x,k) \<in> ?B. content k *\<^sub>R f x) - (\<Sum>(x,k) \<in> ?A. content k *\<^sub>R f x))"
       by auto
     also have "\<dots> \<le> e + e"
       using parts(1)[of ?E] parts(1)[of ?F] by (intro norm_diff_triangle_le[of _ I]) auto
@@ -1202,13 +1185,13 @@
   assume "0 < e"
   have "S \<in> lmeasurable"
     using \<open>negligible S\<close> by (simp add: negligible_iff_null_sets fmeasurableI_null_sets)
-  have e22: "0 < e / 2 / (2 * B * real DIM('M)) ^ DIM('N)"
+  have e22: "0 < e/2 / (2 * B * real DIM('M)) ^ DIM('N)"
     using \<open>0 < e\<close> \<open>0 < B\<close> by (simp add: divide_simps)
   obtain T
     where "open T" "S \<subseteq> T" "T \<in> lmeasurable"
-      and "measure lebesgue T \<le> measure lebesgue S + e / 2 / (2 * B * DIM('M)) ^ DIM('N)"
+      and "measure lebesgue T \<le> measure lebesgue S + e/2 / (2 * B * DIM('M)) ^ DIM('N)"
     by (rule lmeasurable_outer_open [OF \<open>S \<in> lmeasurable\<close> e22])
-  then have T: "measure lebesgue T \<le> e / 2 / (2 * B * DIM('M)) ^ DIM('N)"
+  then have T: "measure lebesgue T \<le> e/2 / (2 * B * DIM('M)) ^ DIM('N)"
     using \<open>negligible S\<close> by (simp add: negligible_iff_null_sets measure_eq_0_null_sets)
   have "\<exists>r. 0 < r \<and> r \<le> 1/2 \<and>
             (x \<in> S \<longrightarrow> (\<forall>y. norm(y - x) < r
@@ -1289,7 +1272,7 @@
   qed
   have countbl: "countable (fbx ` \<D>)"
     using \<open>countable \<D>\<close> by blast
-  have "(\<Sum>k\<in>fbx`\<D>'. measure lebesgue k) \<le> e / 2" if "\<D>' \<subseteq> \<D>" "finite \<D>'" for \<D>'
+  have "(\<Sum>k\<in>fbx`\<D>'. measure lebesgue k) \<le> e/2" if "\<D>' \<subseteq> \<D>" "finite \<D>'" for \<D>'
   proof -
     have BM_ge0: "0 \<le> B * (DIM('M) * prj1 (vf X - uf X))" if "X \<in> \<D>'" for X
       using \<open>0 < B\<close> \<open>\<D>' \<subseteq> \<D>\<close> that vu_pos by fastforce
@@ -1333,7 +1316,7 @@
     qed
     also have "\<dots> = (2 * B * DIM('M)) ^ DIM('N) * sum (measure lebesgue) \<D>'"
       by (simp add: sum_distrib_left)
-    also have "\<dots> \<le> e / 2"
+    also have "\<dots> \<le> e/2"
     proof -
       have div: "\<D>' division_of \<Union>\<D>'"
         apply (auto simp: \<open>finite \<D>'\<close> \<open>{} \<notin> \<D>'\<close> division_of_def)
@@ -1366,13 +1349,13 @@
         using \<open>0 < B\<close>
         apply (simp add: algebra_simps)
         done
-      also have "\<dots> \<le> e / 2"
+      also have "\<dots> \<le> e/2"
         using T \<open>0 < B\<close> by (simp add: field_simps)
       finally show ?thesis .
     qed
     finally show ?thesis .
   qed
-  then have e2: "sum (measure lebesgue) \<G> \<le> e / 2" if "\<G> \<subseteq> fbx ` \<D>" "finite \<G>" for \<G>
+  then have e2: "sum (measure lebesgue) \<G> \<le> e/2" if "\<G> \<subseteq> fbx ` \<D>" "finite \<G>" for \<G>
     by (metis finite_subset_image that)
   show "\<exists>W\<in>lmeasurable. f ` S \<subseteq> W \<and> measure lebesgue W < e"
   proof (intro bexI conjI)
@@ -1616,28 +1599,27 @@
   apply (rule norm_triangle_ineq3)
   done
 
-text\<open>FIXME: needs refactoring and use of Sigma\<close>
-lemma bounded_variation_absolutely_integrable_interval:
+proposition bounded_variation_absolutely_integrable_interval:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   assumes f: "f integrable_on cbox a b"
-    and *: "\<forall>d. d division_of (cbox a b) \<longrightarrow> sum (\<lambda>k. norm(integral k f)) d \<le> B"
+    and *: "\<And>d. d division_of (cbox a b) \<Longrightarrow> sum (\<lambda>K. norm(integral K f)) d \<le> B"
   shows "f absolutely_integrable_on cbox a b"
 proof -
-  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of (cbox a b)}"
+  let ?f = "\<lambda>d. \<Sum>K\<in>d. norm (integral K f)" and ?D = "{d. d division_of (cbox a b)}"
   have D_1: "?D \<noteq> {}"
     by (rule elementary_interval[of a b]) auto
   have D_2: "bdd_above (?f`?D)"
     by (metis * mem_Collect_eq bdd_aboveI2)
   note D = D_1 D_2
   let ?S = "SUP x:?D. ?f x"
-  have *: "\<exists>d. gauge d \<and>
+  have *: "\<exists>\<gamma>. gauge \<gamma> \<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 norm (f x)) - ?S) < e)"
+                  \<gamma> fine p \<longrightarrow>
+                  norm ((\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - ?S) < e)"
     if e: "e > 0" for e
   proof -
-    have "?S - e / 2 < ?S" using \<open>e > 0\<close> by simp
-    then obtain d where d: "d division_of (cbox a b)" "?S - e / 2 < (\<Sum>k\<in>d. norm (integral k f))"
+    have "?S - e/2 < ?S" using \<open>e > 0\<close> by simp
+    then obtain d where d: "d division_of (cbox a b)" "?S - e/2 < (\<Sum>k\<in>d. norm (integral k f))"
       unfolding less_cSUP_iff[OF D] by auto
     note d' = division_ofD[OF this(1)]
 
@@ -1661,72 +1643,65 @@
       by metis
     have "e/2 > 0"
       using e by auto
-    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"
+    with henstock_lemma[OF f] 
+    obtain \<gamma> where g: "gauge \<gamma>"
+      "\<And>p. \<lbrakk>p tagged_partial_division_of cbox a b; \<gamma> 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)"
+    let ?g = "\<lambda>x. \<gamma> x \<inter> ball x (k x)"
     show ?thesis 
-      apply (rule_tac x="?g" in exI)
-      apply safe
-    proof -
+    proof (intro exI conjI allI impI)
       show "gauge ?g"
-        using g(1) k(1)
-        unfolding gauge_def
-        by auto
+        using g(1) k(1) by (auto simp: gauge_def)
+    next
       fix p
-      assume "p tagged_division_of (cbox a b)" and "?g fine p"
-      note p = this(1) conjunctD2[OF this(2)[unfolded fine_Int]]
+      assume "p tagged_division_of (cbox a b) \<and> ?g fine p"
+      then have p: "p tagged_division_of cbox a b" "\<gamma> fine p" "(\<lambda>x. ball x (k x)) fine p"
+        by (auto simp: fine_Int)
       note p' = tagged_division_ofD[OF p(1)]
       define p' where "p' = {(x,k) | x k. \<exists>i l. x \<in> i \<and> i \<in> d \<and> (x,l) \<in> p \<and> k = i \<inter> l}"
-      have gp': "g fine p'"
-        using p(2)
-        unfolding p'_def fine_def
-        by auto
+      have gp': "\<gamma> fine p'"
+        using p(2) by (auto simp: p'_def fine_def)
       have p'': "p' tagged_division_of (cbox a b)"
       proof (rule tagged_division_ofI)
         show "finite p'"
-          apply (rule finite_subset[of _ "(\<lambda>(k,(x,l)). (x,k \<inter> l)) `
-            {(k,xl) | k xl. k \<in> d \<and> xl \<in> p}"])
-          unfolding p'_def
-           defer
-           apply (rule finite_imageI,rule finite_product_dependent[OF d'(1) p'(1)])
-          apply safe
-          unfolding image_iff
-          apply (rule_tac x="(i,x,l)" in bexI)
-           apply auto
-          done
-        fix x k
-        assume "(x, k) \<in> p'"
-        then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
+        proof (rule finite_subset)
+          show "p' \<subseteq> (\<lambda>(k, x, l). (x, k \<inter> l)) ` (d \<times> p)"
+            by (force simp: p'_def image_iff)
+          show "finite ((\<lambda>(k, x, l). (x, k \<inter> l)) ` (d \<times> p))"
+            by (simp add: d'(1) p'(1))
+        qed
+      next
+        fix x K
+        assume "(x, K) \<in> p'"
+        then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> K = i \<inter> l"
           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
-        show "x \<in> k" and "k \<subseteq> cbox a b"
+        then obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "K = i \<inter> l" by blast
+        show "x \<in> K" and "K \<subseteq> cbox a b"
           using p'(2-3)[OF il(3)] il by auto
-        show "\<exists>a b. k = cbox a b"
+        show "\<exists>a b. K = cbox a b"
           unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)]
           by (meson Int_interval)
       next
-        fix x1 k1
-        assume "(x1, k1) \<in> p'"
-        then have "\<exists>i l. x1 \<in> i \<and> i \<in> d \<and> (x1, l) \<in> p \<and> k1 = i \<inter> l"
+        fix x1 K1
+        assume "(x1, K1) \<in> p'"
+        then have "\<exists>i l. x1 \<in> i \<and> i \<in> d \<and> (x1, l) \<in> p \<and> K1 = i \<inter> l"
           unfolding p'_def by auto
-        then obtain i1 l1 where il1: "x1 \<in> i1" "i1 \<in> d" "(x1, l1) \<in> p" "k1 = i1 \<inter> l1" by blast
-        fix x2 k2
-        assume "(x2,k2)\<in>p'"
-        then have "\<exists>i l. x2 \<in> i \<and> i \<in> d \<and> (x2, l) \<in> p \<and> k2 = i \<inter> l"
+        then obtain i1 l1 where il1: "x1 \<in> i1" "i1 \<in> d" "(x1, l1) \<in> p" "K1 = i1 \<inter> l1" by blast
+        fix x2 K2
+        assume "(x2,K2) \<in> p'"
+        then have "\<exists>i l. x2 \<in> i \<and> i \<in> d \<and> (x2, l) \<in> p \<and> K2 = i \<inter> l"
           unfolding p'_def by auto
-        then obtain i2 l2 where il2: "x2 \<in> i2" "i2 \<in> d" "(x2, l2) \<in> p" "k2 = i2 \<inter> l2" by blast
-        assume "(x1, k1) \<noteq> (x2, k2)"
+        then obtain i2 l2 where il2: "x2 \<in> i2" "i2 \<in> d" "(x2, l2) \<in> p" "K2 = i2 \<inter> l2" by blast
+        assume "(x1, K1) \<noteq> (x2, K2)"
         then have "interior i1 \<inter> interior i2 = {} \<or> interior l1 \<inter> interior l2 = {}"
           using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)]  by (auto simp: il1 il2)
-        then show "interior k1 \<inter> interior k2 = {}"
+        then show "interior K1 \<inter> interior K2 = {}"
           unfolding il1 il2 by auto
       next
         have *: "\<forall>(x, X) \<in> p'. X \<subseteq> cbox a b"
-          unfolding p'_def using d' by auto
-        have "y \<in> \<Union>{k. \<exists>x. (x, k) \<in> p'}" if y: "y \<in> cbox a b" for y
+          unfolding p'_def using d' by blast
+        have "y \<in> \<Union>{K. \<exists>x. (x, K) \<in> p'}" if y: "y \<in> cbox a b" for y
         proof -
           obtain x l where xl: "(x, l) \<in> p" "y \<in> l" 
             using y unfolding p'(6)[symmetric] by auto
@@ -1735,10 +1710,10 @@
           have "x \<in> i"
             using fineD[OF p(3) xl(1)] using k(2) i xl by auto
           then show ?thesis
-            apply (rule_tac X="i \<inter> l" in UnionI)
-            using i xl by (auto simp: p'_def)
+            unfolding p'_def
+            by (rule_tac X="i \<inter> l" in UnionI) (use i xl in auto)
         qed
-        show "\<Union>{k. \<exists>x. (x, k) \<in> p'} = cbox a b"
+        show "\<Union>{K. \<exists>x. (x, K) \<in> p'} = cbox a b"
         proof
           show "\<Union>{k. \<exists>x. (x, k) \<in> p'} \<subseteq> cbox a b"
             using * by auto
@@ -1747,26 +1722,23 @@
           proof 
             fix y
             assume y: "y \<in> cbox a b"
-            obtain x l where xl: "(x, l) \<in> p" "y \<in> l" 
+            obtain x L where xl: "(x, L) \<in> p" "y \<in> L" 
               using y unfolding p'(6)[symmetric] by auto
-            obtain i where i: "i \<in> d" "y \<in> i" 
+            obtain I where i: "I \<in> d" "y \<in> I" 
               using y unfolding d'(6)[symmetric] by auto
-            have "x \<in> i"
+            have "x \<in> I"
               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'}"
-              apply (rule_tac X="i \<inter> l" in UnionI)
+              apply (rule_tac X="I \<inter> L" in UnionI)
               using i xl by (auto simp: p'_def)
           qed
         qed
       qed
 
-      then have sum_less_e2: "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
+      then have sum_less_e2: "(\<Sum>(x,K) \<in> p'. norm (content K *\<^sub>R f x - integral K f)) < e/2"
         using g(2) gp' tagged_division_of_def by blast
-      then have XXX: "\<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'' by (force intro!: absdiff_norm_less)
 
-      have p'alt: "p' = {(x,(i \<inter> l)) | x i l. (x,l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}}"
+      have p'alt: "p' = {(x, I \<inter> L) | x I L. (x,L) \<in> p \<and> I \<in> d \<and> I \<inter> L \<noteq> {}}"
       proof (safe, goal_cases)
         case prems: (2 _ _ x i l)
         have "x \<in> i"
@@ -1783,79 +1755,75 @@
         then show ?case
           using prems(3) by auto
       next
-        fix x k
-        assume "(x, k) \<in> p'"
-        then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
+        fix x K
+        assume "(x, K) \<in> p'"
+        then obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "K = i \<inter> l" 
           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> {}"
+        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> {}"
           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))"
+      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)"])
          apply (auto intro: integral_null simp: content_eq_0_interior)
         done
-      note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
-
+      have snd_p_div: "snd ` p division_of cbox a b"
+        by (rule division_of_tagged_division[OF p(1)])
+      note snd_p = division_ofD[OF snd_p_div]
+      have fin_d_sndp: "finite (d \<times> snd ` p)"
+        by (simp add: d'(1) snd_p(1))
 
-      have *: "\<And>sni sni' sf sf'. \<lbrakk>\<bar>sf' - sni'\<bar> < e / 2; ?S - e / 2 < sni; sni' \<le> ?S;
-        sni \<le> sni'; sf' = sf\<rbrakk> \<Longrightarrow> \<bar>sf - ?S\<bar> < e"
+      have *: "\<And>sni sni' sf sf'. \<lbrakk>\<bar>sf' - sni'\<bar> < e/2; ?S - e/2 < sni; sni' \<le> ?S;
+                       sni \<le> sni'; sf' = sf\<rbrakk> \<Longrightarrow> \<bar>sf - ?S\<bar> < e"
         by arith
-      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - ?S) < e"
+      show "norm ((\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - ?S) < e"
         unfolding real_norm_def
       proof (rule *)
-        show "\<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"
-          by (rule XXX)
-        show "(\<Sum>(x, k)\<in>p'. norm (integral k f)) \<le>?S"
+        show "\<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"
+          using p'' sum_less_e2 unfolding split_def by (force intro!: absdiff_norm_less)
+        show "(\<Sum>(x,k) \<in> p'. norm (integral k f)) \<le>?S"
           by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper)
-        show "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>(x, k)\<in>p'. norm (integral k f))"
+        show "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>(x,k) \<in> p'. norm (integral k f))"
         proof -
-          have *: "{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} =
-          (\<lambda>(k,l). k \<inter> l) ` {(k,l)|k l. k \<in> d \<and> l \<in> snd ` p}"
+          have *: "{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} = (\<lambda>(k,l). k \<inter> l) ` (d \<times> snd ` p)"
             by auto
-          have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. \<Sum>l\<in>snd ` p. norm (integral (i \<inter> l) f))"
-          proof (rule sum_mono, goal_cases)
-            case k: (1 k)
-            from d'(4)[OF this] obtain u v where uv: "k = cbox u v" by metis
+          have "(\<Sum>K\<in>d. norm (integral K f)) \<le> (\<Sum>i\<in>d. \<Sum>l\<in>snd ` p. norm (integral (i \<inter> l) f))"
+          proof (rule sum_mono)
+            fix K assume k: "K \<in> d"
+            from d'(4)[OF this] obtain u v where uv: "K = cbox u v" by metis
             define d' where "d' = {cbox u v \<inter> l |l. l \<in> snd ` p \<and>  cbox u v \<inter> l \<noteq> {}}"
-            note uvab = d'(2)[OF k[unfolded uv]]
+            have uvab: "cbox u v \<subseteq> cbox a b"
+              using d(1) k uv by blast
             have "d' division_of cbox u v"
-              apply (subst d'_def)
-              apply (rule division_inter_1)
-               apply (rule division_of_tagged_division[OF p(1)])
-              apply (rule uvab)
-              done
-            then have "norm (integral k f) \<le> sum (\<lambda>k. norm (integral k f)) d'"
-              unfolding uv
+              unfolding d'_def by (rule division_inter_1 [OF snd_p_div uvab])
+            moreover then have "norm (\<Sum>i\<in>d'. integral i f) \<le> (\<Sum>k\<in>d'. norm (integral k f))"
+              by (simp add: sum_norm_le)
+            ultimately have "norm (integral K f) \<le> sum (\<lambda>k. norm (integral k f)) d'"
               apply (subst integral_combine_division_topdown[of _ _ d'])
-                apply (rule integrable_on_subcbox[OF assms(1) uvab])
-               apply assumption
-              apply (rule sum_norm_le)
-              apply auto
+                apply (auto simp: uv intro: integrable_on_subcbox[OF assms(1) uvab])
               done
-            also have "\<dots> = (\<Sum>k\<in>{k \<inter> l |l. l \<in> snd ` p}. norm (integral k f))"
+            also have "\<dots> = (\<Sum>I\<in>{K \<inter> L |L. L \<in> snd ` p}. norm (integral I f))"
             proof -
-              have *: "norm (integral i f) = 0"
-                if "i \<in> {cbox u v \<inter> l |l. l \<in> snd ` p}"
-                  "i \<notin> {cbox u v \<inter> l |l. l \<in> snd ` p \<and> cbox u v \<inter> l \<noteq> {}}" for i
+              have *: "norm (integral I f) = 0"
+                if "I \<in> {cbox u v \<inter> l |l. l \<in> snd ` p}"
+                  "I \<notin> {cbox u v \<inter> l |l. l \<in> snd ` p \<and> cbox u v \<inter> l \<noteq> {}}" for I
                 using that by auto
               show ?thesis
                 apply (rule sum.mono_neutral_left)
                   apply (simp add: snd_p(1))
                 unfolding d'_def uv using * by auto 
             qed
-            also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (k \<inter> l) f))"
+            also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (K \<inter> l) f))"
             proof -
-              have *: "norm (integral (k \<inter> l) f) = 0"
-                if "l \<in> snd ` p" "y \<in> snd ` p" "l \<noteq> y" "k \<inter> l = k \<inter> y" for l y
+              have *: "norm (integral (K \<inter> l) f) = 0"
+                if "l \<in> snd ` p" "y \<in> snd ` p" "l \<noteq> y" "K \<inter> l = K \<inter> y" for l y
               proof -
-                have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
+                have "interior (K \<inter> l) \<subseteq> interior (l \<inter> y)"
                   by (metis Int_lower2 interior_mono le_inf_iff that(4))
-                then have "interior (k \<inter> l) = {}"
+                then have "interior (K \<inter> l) = {}"
                   by (simp add: snd_p(5) that) 
                 moreover from d'(4)[OF k] snd_p(4)[OF that(1)] 
                 obtain u1 v1 u2 v2
-                  where uv: "k = cbox u1 u2" "l = cbox v1 v2" by metis
+                  where uv: "K = cbox u1 u2" "l = cbox v1 v2" by metis
                 ultimately show ?thesis
                   using that integral_null
                   unfolding uv Int_interval content_eq_0_interior
@@ -1868,12 +1836,12 @@
                  apply (rule p')
                 using * by auto
             qed
-            finally show ?case .
+            finally show "norm (integral K f) \<le> (\<Sum>l\<in>snd ` p. norm (integral (K \<inter> l) f))" .
           qed
-          also have "\<dots> = (\<Sum>(i,l) \<in> d \<times> (snd ` p). norm (integral (i\<inter>l) f))"
+          also have "\<dots> = (\<Sum>(i,l) \<in> d \<times> snd ` p. norm (integral (i\<inter>l) f))"
             by (simp add: sum.cartesian_product)
-          also have "\<dots> = (\<Sum>x\<in>{(i, l) |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral (case_prod op \<inter> x) f))"
-            by (force simp: split_def Sigma_def intro!: sum.cong)
+          also have "\<dots> = (\<Sum>x \<in> d \<times> snd ` p. norm (integral (case_prod op \<inter> x) f))"
+            by (force simp: split_def intro!: sum.cong)
           also have "\<dots> = (\<Sum>k\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral k f))"
           proof -
             have eq0: " (integral (l1 \<inter> k1) f) = 0"
@@ -1896,142 +1864,123 @@
             qed
             show ?thesis
               unfolding *
-              apply (rule sum.reindex_nontrivial [symmetric, unfolded o_def])
-               apply (rule finite_product_dependent [OF \<open>finite d\<close>])
-               apply (rule finite_imageI [OF \<open>finite p\<close>])
+              apply (rule sum.reindex_nontrivial [OF fin_d_sndp, symmetric, unfolded o_def])
               apply clarsimp
               by (metis eq0 fst_conv snd_conv)
           qed
-          also have "\<dots> = (\<Sum>(x, k)\<in>p'. norm (integral k f))"
+          also have "\<dots> = (\<Sum>(x,k) \<in> p'. norm (integral k f))"
           proof -
             have 0: "integral (ia \<inter> snd (a, b)) f = 0"
-              if "ia \<inter> snd (a, b) \<notin> snd ` p'" "ia \<in> d" "(a, b) \<in> p" for  ia a b
+              if "ia \<inter> snd (a, b) \<notin> snd ` p'" "ia \<in> d" "(a, b) \<in> p" for ia a b
             proof -
               have "ia \<inter> b = {}"
-                using that
-                unfolding p'alt image_iff Bex_def not_ex
+                using that unfolding p'alt image_iff Bex_def not_ex
                 apply (erule_tac x="(a, ia \<inter> b)" in allE)
                 apply auto
                 done
-              then show ?thesis
-                by auto
+              then show ?thesis by auto
             qed
             have 1: "\<exists>i l. snd (a, b) = i \<inter> l \<and> i \<in> d \<and> l \<in> snd ` p" if "(a, b) \<in> p'" for a b
-            proof -
-              have "\<exists>n N Na. (a, b) = (n, N \<inter> Na) \<and> (n, Na) \<in> p \<and> N \<in> d \<and> N \<inter> Na \<noteq> {}"
-                using that p'alt by blast
-              then show "\<exists>N Na. snd (a, b) = N \<inter> Na \<and> N \<in> d \<and> Na \<in> snd ` p"
-                by (metis (no_types) imageI prod.sel(2))
-            qed
+              using that 
+              apply (clarsimp simp: p'_def image_iff)
+              by (metis (no_types, hide_lams) snd_conv)
             show ?thesis
               unfolding sum_p'
               apply (rule sum.mono_neutral_right)
-                apply (subst *)
-                apply (rule finite_imageI[OF finite_product_dependent])
-                 apply fact
-                apply (rule finite_imageI[OF p'(1)])
+                apply (metis * finite_imageI[OF fin_d_sndp])
               using 0 1 by auto
           qed
           finally show ?thesis .
         qed
-        show "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x)) = (\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x))"
+        show "(\<Sum>(x,k) \<in> p'. norm (content k *\<^sub>R f x)) = (\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x))"
         proof -
           let ?S = "{(x, i \<inter> l) |x i l. (x, l) \<in> p \<and> i \<in> d}"
           have *: "?S = (\<lambda>(xl,i). (fst xl, snd xl \<inter> i)) ` (p \<times> d)"
             by force
-          have pdfin: "finite (p \<times> d)"
+          have fin_pd: "finite (p \<times> d)"
             using finite_cartesian_product[OF p'(1) d'(1)] by metis
-          have "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x)) = (\<Sum>(x, k)\<in>?S. \<bar>content k\<bar> * norm (f x))"
+          have "(\<Sum>(x,k) \<in> p'. norm (content k *\<^sub>R f x)) = (\<Sum>(x,k) \<in> ?S. \<bar>content k\<bar> * norm (f x))"
             unfolding norm_scaleR
             apply (rule sum.mono_neutral_left)
               apply (subst *)
-              apply (rule finite_imageI)
-              apply fact
-            unfolding p'alt apply blast
+              apply (rule finite_imageI [OF fin_pd])
+            unfolding p'alt apply auto
             by fastforce
           also have "\<dots> = (\<Sum>((x,l),i)\<in>p \<times> d. \<bar>content (l \<inter> i)\<bar> * norm (f x))"
-            unfolding *
-            apply (subst sum.reindex_nontrivial)
-              apply fact
-            unfolding split_paired_all
-            unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff prod.inject
-             apply (elim conjE)
           proof -
-            fix x1 l1 k1 x2 l2 k2
-            assume as: "(x1, l1) \<in> p" "(x2, l2) \<in> p" "k1 \<in> d" "k2 \<in> d"
-              "x1 = x2" "l1 \<inter> k1 = l2 \<inter> k2" "\<not> ((x1 = x2 \<and> l1 = l2) \<and> k1 = k2)"
-            from d'(4)[OF as(3)] p'(4)[OF as(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
-            from as have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
-              by auto
-            then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
-              apply -
-              apply (erule disjE)
-               apply (rule disjI2)
-               defer
-               apply (rule disjI1)
-               apply (rule d'(5)[OF as(3-4)])
-               apply assumption
-              apply (rule p'(5)[OF as(1-2)])
-              apply auto
+            have "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0"
+              if "(x1, l1) \<in> p" "(x2, l2) \<in> p" "k1 \<in> d" "k2 \<in> d"
+                "x1 = x2" "l1 \<inter> k1 = l2 \<inter> k2" "x1 \<noteq> x2 \<or> l1 \<noteq> l2 \<or> k1 \<noteq> k2"
+              for x1 l1 k1 x2 l2 k2
+            proof -
+              obtain u1 v1 u2 v2 where uv: "k1 = cbox u1 u2" "l1 = cbox v1 v2"
+                by (meson \<open>(x1, l1) \<in> p\<close> \<open>k1 \<in> d\<close> d(1) division_ofD(4) p'(4))
+              have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
+                using that by auto
+              then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
+                apply (rule disjE)
+                using that p'(5) d'(5) by auto
+              moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
+                unfolding that ..
+              ultimately have "interior (l1 \<inter> k1) = {}"
+                by auto
+              then show "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0"
+                unfolding uv Int_interval content_eq_0_interior[symmetric] by auto
+            qed 
+            then show ?thesis
+              unfolding *
+              apply (subst sum.reindex_nontrivial [OF fin_pd])
+              unfolding split_paired_all o_def split_def prod.inject
+               apply force+
               done
-            moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
-              unfolding  as ..
-            ultimately have "interior (l1 \<inter> k1) = {}"
-              by auto
-            then show "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0"
-              unfolding uv Int_interval
-              unfolding content_eq_0_interior[symmetric]
-              by auto
-          qed safe
-          also have "\<dots> = (\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x))"
-            apply (subst sum_Sigma_product[symmetric])
-              apply (rule p')
-             apply (rule d')
-            apply (rule sum.cong)
-             apply (rule refl)
-            unfolding split_paired_all split_conv
+          qed
+          also have "\<dots> = (\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x))"
           proof -
-            fix x l
-            assume as: "(x, l) \<in> p"
-            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))"
-              by (simp add: Int_commute uv)
-            also have "\<dots> = sum content {k \<inter> cbox u v| k. k \<in> d}"
+            have sumeq: "(\<Sum>i\<in>d. content (l \<inter> i) * norm (f x)) = content l * norm (f x)"
+              if "(x, l) \<in> p" for x l
             proof -
-              have eq0: "content (k \<inter> cbox u v) = 0"
-                if "k \<in> d" "y \<in> d" "k \<noteq> y" and eq: "k \<inter> cbox u v = y \<inter> cbox u v" for k y
+              note xl = p'(2-4)[OF that]
+              then obtain u v where uv: "l = cbox u v" by blast
+              have "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar>) = (\<Sum>k\<in>d. content (k \<inter> cbox u v))"
+                by (simp add: Int_commute uv)
+              also have "\<dots> = sum content {k \<inter> cbox u v| k. k \<in> d}"
               proof -
-              from d'(4)[OF that(1)] d'(4)[OF that(2)]
-              obtain \<alpha> \<beta> where \<alpha>: "k \<inter> cbox u v = cbox \<alpha> \<beta>"
-                by (meson Int_interval)
-              have "{} = interior ((k \<inter> y) \<inter> cbox u v)"
-                by (simp add: d'(5) that)
-              also have "\<dots> = interior (y \<inter> (k \<inter> cbox u v))"
-                by auto
-              also have "\<dots> = interior (k \<inter> cbox u v)"
-                unfolding eq by auto
-              finally show ?thesis
-                unfolding \<alpha> content_eq_0_interior ..
+                have eq0: "content (k \<inter> cbox u v) = 0"
+                  if "k \<in> d" "y \<in> d" "k \<noteq> y" and eq: "k \<inter> cbox u v = y \<inter> cbox u v" for k y
+                proof -
+                  from d'(4)[OF that(1)] d'(4)[OF that(2)]
+                  obtain \<alpha> \<beta> where \<alpha>: "k \<inter> cbox u v = cbox \<alpha> \<beta>"
+                    by (meson Int_interval)
+                  have "{} = interior ((k \<inter> y) \<inter> cbox u v)"
+                    by (simp add: d'(5) that)
+                  also have "\<dots> = interior (y \<inter> (k \<inter> cbox u v))"
+                    by auto
+                  also have "\<dots> = interior (k \<inter> cbox u v)"
+                    unfolding eq by auto
+                  finally show ?thesis
+                    unfolding \<alpha> content_eq_0_interior ..
+                qed
+                then show ?thesis
+                  unfolding Setcompr_eq_image
+                  apply (rule sum.reindex_nontrivial [OF \<open>finite d\<close>, unfolded o_def, symmetric])
+                  by auto
+              qed
+              also have "\<dots> = sum content {cbox u v \<inter> k |k. k \<in> d \<and> cbox u v \<inter> k \<noteq> {}}"
+                apply (rule sum.mono_neutral_right)
+                unfolding Setcompr_eq_image
+                  apply (rule finite_imageI [OF \<open>finite d\<close>])
+                 apply (fastforce simp: inf.commute)+
+                done
+              finally show "(\<Sum>i\<in>d. content (l \<inter> i) * norm (f x)) = content l * norm (f x)"
+                unfolding sum_distrib_right[symmetric] real_scaleR_def
+                apply (subst(asm) additive_content_division[OF division_inter_1[OF d(1)]])
+                using xl(2)[unfolded uv] unfolding uv apply auto
+                done
             qed
-            then show ?thesis
-              unfolding Setcompr_eq_image
-              apply (rule sum.reindex_nontrivial [OF \<open>finite d\<close>, unfolded o_def, symmetric])
-              by auto
+            show ?thesis
+              by (subst sum_Sigma_product[symmetric]) (auto intro!: sumeq sum.cong p' d')
           qed
-          also have "\<dots> = sum content {cbox u v \<inter> k |k. k \<in> d \<and> cbox u v \<inter> k \<noteq> {}}"
-            apply (rule sum.mono_neutral_right)
-            unfolding Setcompr_eq_image
-              apply (rule finite_imageI [OF \<open>finite d\<close>])
-             apply (fastforce simp: inf.commute)+
-            done
-          finally show "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar> * norm (f x)) = content l *\<^sub>R norm (f x)"
-            unfolding sum_distrib_right[symmetric] real_scaleR_def
-            apply (subst(asm) additive_content_division[OF division_inter_1[OF d(1)]])
-            using xl(2)[unfolded uv] unfolding uv apply auto
-            done
-        qed
-        finally show ?thesis .
+          finally show ?thesis .
         qed
       qed (rule d)
     qed 
@@ -2147,23 +2096,23 @@
           using \<open>e > 0\<close> by auto
         from * [OF this] obtain d1 where
           d1: "gauge d1" "\<forall>p. p tagged_division_of (cbox a b) \<and> d1 fine p \<longrightarrow>
-            norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm (f x))) < e / 2"
+            norm ((\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm (f x))) < e/2"
           by auto
         from henstock_lemma [OF f(1) \<open>e/2>0\<close>] obtain d2 where
           d2: "gauge d2" "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d2 fine p \<longrightarrow>
-            (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2" .
+            (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x - integral k f)) < e/2" .
          obtain p where
           p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
           by (rule fine_division_exists [OF gauge_Int [OF d1(1) d2(1)], of a b])
             (auto simp add: fine_Int)
-        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> \<bar>sf - si\<bar> < e / 2 \<longrightarrow>
-          \<bar>sf' - di\<bar> < e / 2 \<longrightarrow> di < ?S + e"
+        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> \<bar>sf - si\<bar> < e/2 \<longrightarrow>
+          \<bar>sf' - di\<bar> < e/2 \<longrightarrow> di < ?S + e"
           by arith
         show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
           apply (subst if_P)
           apply rule
         proof (rule *[rule_format])
-          show "\<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"
+          show "\<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
             apply (rule absdiff_norm_less)
             using d2(2)[rule_format,of p]
@@ -2171,19 +2120,16 @@
             unfolding tagged_division_of_def split_def
             apply auto
             done
-          show "\<bar>(\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))\<bar> < e / 2"
+          show "\<bar>(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))\<bar> < e/2"
             using d1(2)[rule_format,OF conjI[OF p(1,2)]]
             by (simp only: real_norm_def)
-          show "(\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) = (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x))"
+          show "(\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) = (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x))"
             apply (rule sum.cong)
             apply (rule refl)
             unfolding split_paired_all split_conv
             apply (drule tagged_division_ofD(4)[OF p(1)])
-            unfolding norm_scaleR
-            apply (subst abs_of_nonneg)
-            apply auto
-            done
-          show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> ?S"
+            by simp
+          show "(\<Sum>(x,k) \<in> p. norm (integral k f)) \<le> ?S"
             using partial_division_of_tagged_division[of p "cbox a b"] p(1)
             apply (subst sum.over_tagged_division_lemma[OF p(1)])
             apply (simp add: content_eq_0_interior)
@@ -2656,11 +2602,12 @@
     using f nonneg by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
   then have F_le_T: "a \<le> x \<Longrightarrow> F x \<le> T" for x
     by (intro tendsto_lowerbound[OF lim])
-       (auto simp: trivial_limit_at_top_linorder eventually_at_top_linorder)
+       (auto simp: eventually_at_top_linorder)
 
   have "(SUP i::nat. ?f i x) = ?fR x" for x
   proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
-    from reals_Archimedean2[of "x - a"] guess n ..
+    obtain n where "x - a < real n"
+      using reals_Archimedean2[of "x - a"] ..
     then have "eventually (\<lambda>n. ?f n x = ?fR x) sequentially"
       by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator)
     then show "(\<lambda>n. ?f n x) \<longlonglongrightarrow> ?fR x"
diff -r 6e114edae18b -r 8bf96de50193 src/HOL/Tools/value_command.ML
--- a/src/HOL/Tools/value_command.ML	Sun Aug 06 18:51:32 2017 +0200
+++ b/src/HOL/Tools/value_command.ML	Sun Aug 06 18:56:47 2017 +0200
@@ -17,9 +17,7 @@
 
 fun default_value ctxt t =
   if null (Term.add_frees t [])
-  then case try (Code_Evaluation.dynamic_value_strict ctxt) t of
-    SOME t' => t'
-  | NONE => Nbe.dynamic_value ctxt t
+  then Code_Evaluation.dynamic_value_strict ctxt t
   else Nbe.dynamic_value ctxt t;
 
 structure Evaluator = Theory_Data
diff -r 6e114edae18b -r 8bf96de50193 src/HOL/ex/Adhoc_Overloading_Examples.thy
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Sun Aug 06 18:51:32 2017 +0200
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Sun Aug 06 18:56:47 2017 +0200
@@ -38,7 +38,7 @@
 adhoc_overloading
   vars term_vars
 
-value "vars (Fun ''f'' [Var 0, Var 1])"
+value [nbe] "vars (Fun ''f'' [Var 0, Var 1])"
 
 fun rule_vars :: "('a, 'b) term \<times> ('a, 'b) term \<Rightarrow> 'b set" where
   "rule_vars (l, r) = vars l \<union> vars r"
@@ -46,7 +46,7 @@
 adhoc_overloading
   vars rule_vars
 
-value "vars (Var 1, Var 0)"
+value [nbe] "vars (Var 1, Var 0)"
 
 definition trs_vars :: "(('a, 'b) term \<times> ('a, 'b) term) set \<Rightarrow> 'b set" where
   "trs_vars R = \<Union>(rule_vars ` R)"
@@ -54,7 +54,7 @@
 adhoc_overloading
   vars trs_vars
 
-value "vars {(Var 1, Var 0)}"
+value [nbe] "vars {(Var 1, Var 0)}"
 
 text \<open>Sometimes it is necessary to add explicit type constraints
 before a variant can be determined.\<close>
diff -r 6e114edae18b -r 8bf96de50193 src/HOL/ex/Normalization_by_Evaluation.thy
--- a/src/HOL/ex/Normalization_by_Evaluation.thy	Sun Aug 06 18:51:32 2017 +0200
+++ b/src/HOL/ex/Normalization_by_Evaluation.thy	Sun Aug 06 18:56:47 2017 +0200
@@ -68,20 +68,20 @@
 lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
   by normalization rule
 lemma "rev [a, b, c] = [c, b, a]" by normalization
-value "rev (a#b#cs) = rev cs @ [b, a]"
-value "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
-value "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
-value "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
+value [nbe] "rev (a#b#cs) = rev cs @ [b, a]"
+value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
+value [nbe] "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
+value [nbe] "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
 lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]" 
   by normalization
-value "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
-value "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
+value [nbe] "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
+value [nbe] "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
 lemma "let x = y in [x, x] = [y, y]" by normalization
 lemma "Let y (%x. [x,x]) = [y, y]" by normalization
-value "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
+value [nbe] "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
 lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization
-value "filter (%x. x) ([True,False,x]@xs)"
-value "filter Not ([True,False,x]@xs)"
+value [nbe] "filter (%x. x) ([True,False,x]@xs)"
+value [nbe] "filter Not ([True,False,x]@xs)"
 
 lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b, c]" by normalization
 lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization
@@ -106,7 +106,7 @@
 lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization
 lemma "max (Suc 0) 0 = Suc 0" by normalization
 lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
-value "Suc 0 \<in> set ms"
+value [nbe] "Suc 0 \<in> set ms"
 
 (* non-left-linear patterns, equality by extensionality *)
 
@@ -115,13 +115,13 @@
 lemma "(f o g) x = f (g x)" by normalization
 lemma "(f o id) x = f x" by normalization
 lemma "(id :: bool \<Rightarrow> bool) = id" by normalization
-value "(\<lambda>x. x)"
+value [nbe] "(\<lambda>x. x)"
 
 (* Church numerals: *)
 
-value "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
-value "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
-value "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+value [nbe] "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+value [nbe] "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+value [nbe] "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
 
 (* handling of type classes in connection with equality *)
 
diff -r 6e114edae18b -r 8bf96de50193 src/HOL/ex/Transitive_Closure_Table_Ex.thy
--- a/src/HOL/ex/Transitive_Closure_Table_Ex.thy	Sun Aug 06 18:51:32 2017 +0200
+++ b/src/HOL/ex/Transitive_Closure_Table_Ex.thy	Sun Aug 06 18:56:47 2017 +0200
@@ -24,7 +24,7 @@
 values "{x. test\<^sup>*\<^sup>* A x}"
 values "{x. test\<^sup>*\<^sup>* x C}"
 
-value "test\<^sup>*\<^sup>* A C"
-value "test\<^sup>*\<^sup>* C A"
+value [nbe] "test\<^sup>*\<^sup>* A C"
+value [nbe] "test\<^sup>*\<^sup>* C A"
 
 end