Merge (non-trivial)
authorpaulson <lp15@cam.ac.uk>
Thu Aug 24 12:45:46 2017 +0100 (22 months ago)
changeset 6649897fc319d6089
parent 66494 8645dc296dca
parent 66497 18a6478a574c
child 66499 8367a4f25781
child 66503 7685861f337d
Merge (non-trivial)
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Tagged_Division.thy
     1.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Aug 24 10:47:56 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Aug 24 12:45:46 2017 +0100
     1.3 @@ -1643,7 +1643,7 @@
     1.4        by metis
     1.5      have "e/2 > 0"
     1.6        using e by auto
     1.7 -    with henstock_lemma[OF f] 
     1.8 +    with Henstock_lemma[OF f] 
     1.9      obtain \<gamma> where g: "gauge \<gamma>"
    1.10        "\<And>p. \<lbrakk>p tagged_partial_division_of cbox a b; \<gamma> fine p\<rbrakk> 
    1.11                  \<Longrightarrow> (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x - integral k f)) < e/2"
    1.12 @@ -2101,7 +2101,7 @@
    1.13          obtain d2 where "gauge d2" 
    1.14            and d2: "\<And>p. \<lbrakk>p tagged_partial_division_of (cbox a b); d2 fine p\<rbrakk> \<Longrightarrow>
    1.15              (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x - integral k f)) < e/2"
    1.16 -          by (blast intro: henstock_lemma [OF f(1) \<open>e/2>0\<close>])
    1.17 +          by (blast intro: Henstock_lemma [OF f(1) \<open>e/2>0\<close>])
    1.18          obtain p where
    1.19            p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
    1.20            by (rule fine_division_exists [OF gauge_Int [OF \<open>gauge d1\<close> \<open>gauge d2\<close>], of a b])
     2.1 --- a/src/HOL/Analysis/Harmonic_Numbers.thy	Thu Aug 24 10:47:56 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Thu Aug 24 12:45:46 2017 +0100
     2.3 @@ -38,7 +38,7 @@
     2.4    unfolding harm_def by simp
     2.5  
     2.6  lemma abs_harm [simp]: "(abs (harm n) :: real) = harm n"
     2.7 -  using harm_nonneg[of n] by (rule abs_of_nonneg)    
     2.8 +  using harm_nonneg[of n] by (rule abs_of_nonneg)
     2.9  
    2.10  lemma norm_harm: "norm (harm n) = harm n"
    2.11    by (subst of_real_harm [symmetric]) (simp add: harm_nonneg)
    2.12 @@ -99,12 +99,12 @@
    2.13    show "eventually (\<lambda>n. harm n \<ge> ln (real (Suc n))) at_top"
    2.14      using ln_le_harm by (intro always_eventually allI) (simp_all add: add_ac)
    2.15    show "filterlim (\<lambda>n. ln (real (Suc n))) at_top sequentially"
    2.16 -    by (intro filterlim_compose[OF ln_at_top] filterlim_compose[OF filterlim_real_sequentially] 
    2.17 +    by (intro filterlim_compose[OF ln_at_top] filterlim_compose[OF filterlim_real_sequentially]
    2.18                filterlim_Suc)
    2.19  qed
    2.20  
    2.21  
    2.22 -subsection \<open>The Euler--Mascheroni constant\<close>
    2.23 +subsection \<open>The Euler-Mascheroni constant\<close>
    2.24  
    2.25  text \<open>
    2.26    The limit of the difference between the partial harmonic sum and the natural logarithm
    2.27 @@ -250,7 +250,7 @@
    2.28  qed
    2.29  
    2.30  
    2.31 -subsection \<open>Bounds on the Euler--Mascheroni constant\<close>
    2.32 +subsection \<open>Bounds on the Euler-Mascheroni constant\<close>
    2.33  
    2.34  (* TODO: Move? *)
    2.35  lemma ln_inverse_approx_le:
    2.36 @@ -295,7 +295,7 @@
    2.37      finally show "inverse t \<le> (t - x) * f' + inverse x" .
    2.38    qed
    2.39    hence "integral {x..x+a} inverse \<le> integral {x..x+a} ?f" using f'_nonpos assms
    2.40 -    by (intro integral_le has_integral_integrable[OF int1] has_integral_integrable[OF int2] ineq)
    2.41 +    by (blast intro: integral_le has_integral_integrable[OF int1] has_integral_integrable[OF int2] ineq)
    2.42    also have "\<dots> = ?A" using int1 by (rule integral_unique)
    2.43    finally show ?thesis .
    2.44  qed
    2.45 @@ -332,7 +332,7 @@
    2.46      thus "(t - m) * f' + inverse m \<le> inverse t" by (simp add: algebra_simps)
    2.47    qed
    2.48    hence "integral {x..y} inverse \<ge> integral {x..y} (\<lambda>t. (t - m) * f' + inverse m)"
    2.49 -    using int1 int2 by (intro integral_le has_integral_integrable)
    2.50 +    using int1 int2 by (blast intro: integral_le has_integral_integrable)
    2.51    also have "integral {x..y} (\<lambda>t. (t - m) * f' + inverse m) = ?A"
    2.52      using integral_unique[OF int1] by simp
    2.53    finally show ?thesis .
    2.54 @@ -359,7 +359,7 @@
    2.55    from euler_mascheroni_sum_real have "euler_mascheroni = (\<Sum>k. D k)"
    2.56      by (simp add: sums_iff D_def)
    2.57    also have "\<dots> = (\<Sum>k. D (k + Suc n)) + (\<Sum>k\<le>n. D k)"
    2.58 -    by (subst suminf_split_initial_segment[OF summable, of "Suc n"], 
    2.59 +    by (subst suminf_split_initial_segment[OF summable, of "Suc n"],
    2.60          subst lessThan_Suc_atMost) simp
    2.61    finally have sum: "(\<Sum>k\<le>n. D k) - euler_mascheroni = -(\<Sum>k. D (k + Suc n))" by simp
    2.62  
    2.63 @@ -524,7 +524,7 @@
    2.64  
    2.65  
    2.66  text \<open>
    2.67 -  Approximation of the Euler--Mascheroni constant. The lower bound is accurate to about 0.0015;
    2.68 +  Approximation of the Euler-Mascheroni constant. The lower bound is accurate to about 0.0015;
    2.69    the upper bound is accurate to about 0.015.
    2.70  \<close>
    2.71  lemma euler_mascheroni_gt_19_over_33: "(euler_mascheroni :: real) > 19/33" (is ?th1)
     3.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Aug 24 10:47:56 2017 +0200
     3.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Aug 24 12:45:46 2017 +0100
     3.3 @@ -253,26 +253,25 @@
     3.4  
     3.5  lemma has_integral:
     3.6    "(f has_integral y) (cbox a b) \<longleftrightarrow>
     3.7 -    (\<forall>e>0. \<exists>d. gauge d \<and>
     3.8 -      (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
     3.9 -        norm (sum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
    3.10 +    (\<forall>e>0. \<exists>\<gamma>. gauge \<gamma> \<and>
    3.11 +      (\<forall>\<D>. \<D> tagged_division_of (cbox a b) \<and> \<gamma> fine \<D> \<longrightarrow>
    3.12 +        norm (sum (\<lambda>(x,k). content(k) *\<^sub>R f x) \<D> - y) < e))"
    3.13    by (auto simp: dist_norm eventually_division_filter has_integral_def tendsto_iff)
    3.14  
    3.15  lemma has_integral_real:
    3.16    "(f has_integral y) {a..b::real} \<longleftrightarrow>
    3.17 -    (\<forall>e>0. \<exists>d. gauge d \<and>
    3.18 -      (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow>
    3.19 -        norm (sum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
    3.20 -  unfolding box_real[symmetric]
    3.21 -  by (rule has_integral)
    3.22 +    (\<forall>e>0. \<exists>\<gamma>. gauge \<gamma> \<and>
    3.23 +      (\<forall>\<D>. \<D> tagged_division_of {a..b} \<and> \<gamma> fine \<D> \<longrightarrow>
    3.24 +        norm (sum (\<lambda>(x,k). content(k) *\<^sub>R f x) \<D> - y) < e))"
    3.25 +  unfolding box_real[symmetric] by (rule has_integral)
    3.26  
    3.27  lemma has_integralD[dest]:
    3.28    assumes "(f has_integral y) (cbox a b)"
    3.29      and "e > 0"
    3.30 -  obtains d
    3.31 -    where "gauge d"
    3.32 -      and "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> d fine p \<Longrightarrow>
    3.33 -        norm ((\<Sum>(x,k)\<in>p. content k *\<^sub>R f x) - y) < e"
    3.34 +  obtains \<gamma>
    3.35 +    where "gauge \<gamma>"
    3.36 +      and "\<And>\<D>. \<D> tagged_division_of (cbox a b) \<Longrightarrow> \<gamma> fine \<D> \<Longrightarrow>
    3.37 +        norm ((\<Sum>(x,k)\<in>\<D>. content k *\<^sub>R f x) - y) < e"
    3.38    using assms unfolding has_integral by auto
    3.39  
    3.40  lemma has_integral_alt:
    3.41 @@ -914,28 +913,28 @@
    3.42  
    3.43  subsection \<open>Cauchy-type criterion for integrability.\<close>
    3.44  
    3.45 -lemma integrable_Cauchy:
    3.46 +proposition integrable_Cauchy:
    3.47    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::{real_normed_vector,complete_space}"
    3.48    shows "f integrable_on cbox a b \<longleftrightarrow>
    3.49          (\<forall>e>0. \<exists>\<gamma>. gauge \<gamma> \<and>
    3.50 -          (\<forall>p1 p2. p1 tagged_division_of (cbox a b) \<and> \<gamma> fine p1 \<and>
    3.51 -            p2 tagged_division_of (cbox a b) \<and> \<gamma> fine p2 \<longrightarrow>
    3.52 -            norm ((\<Sum>(x,K)\<in>p1. content K *\<^sub>R f x) - (\<Sum>(x,K)\<in>p2. content K *\<^sub>R f x)) < e))"
    3.53 +          (\<forall>\<D>1 \<D>2. \<D>1 tagged_division_of (cbox a b) \<and> \<gamma> fine \<D>1 \<and>
    3.54 +            \<D>2 tagged_division_of (cbox a b) \<and> \<gamma> fine \<D>2 \<longrightarrow>
    3.55 +            norm ((\<Sum>(x,K)\<in>\<D>1. content K *\<^sub>R f x) - (\<Sum>(x,K)\<in>\<D>2. content K *\<^sub>R f x)) < e))"
    3.56    (is "?l = (\<forall>e>0. \<exists>\<gamma>. ?P e \<gamma>)")
    3.57  proof (intro iffI allI impI)
    3.58    assume ?l
    3.59    then obtain y
    3.60      where y: "\<And>e. e > 0 \<Longrightarrow>
    3.61          \<exists>\<gamma>. gauge \<gamma> \<and>
    3.62 -            (\<forall>p. p tagged_division_of cbox a b \<and> \<gamma> fine p \<longrightarrow>
    3.63 -                 norm ((\<Sum>(x,K) \<in> p. content K *\<^sub>R f x) - y) < e)"
    3.64 +            (\<forall>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D> \<longrightarrow>
    3.65 +                 norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - y) < e)"
    3.66      by (auto simp: integrable_on_def has_integral)
    3.67    show "\<exists>\<gamma>. ?P e \<gamma>" if "e > 0" for e
    3.68    proof -
    3.69      have "e/2 > 0" using that by auto
    3.70      with y obtain \<gamma> where "gauge \<gamma>"
    3.71 -      and \<gamma>: "\<And>p. p tagged_division_of cbox a b \<and> \<gamma> fine p \<Longrightarrow>
    3.72 -                  norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f x) - y) < e/2"
    3.73 +      and \<gamma>: "\<And>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D> \<Longrightarrow>
    3.74 +                  norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f x) - y) < e/2"
    3.75        by meson
    3.76      show ?thesis
    3.77      apply (rule_tac x=\<gamma> in exI, clarsimp simp: \<open>gauge \<gamma>\<close>)
    3.78 @@ -947,9 +946,9 @@
    3.79      by auto
    3.80    then obtain \<gamma> :: "nat \<Rightarrow> 'n \<Rightarrow> 'n set" where \<gamma>:
    3.81      "\<And>m. gauge (\<gamma> m)"
    3.82 -    "\<And>m p1 p2. \<lbrakk>p1 tagged_division_of cbox a b;
    3.83 -              \<gamma> m fine p1; p2 tagged_division_of cbox a b; \<gamma> m fine p2\<rbrakk>
    3.84 -              \<Longrightarrow> norm ((\<Sum>(x,K) \<in> p1. content K *\<^sub>R f x) - (\<Sum>(x,K) \<in> p2. content K *\<^sub>R f x))
    3.85 +    "\<And>m \<D>1 \<D>2. \<lbrakk>\<D>1 tagged_division_of cbox a b;
    3.86 +              \<gamma> m fine \<D>1; \<D>2 tagged_division_of cbox a b; \<gamma> m fine \<D>2\<rbrakk>
    3.87 +              \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>1. content K *\<^sub>R f x) - (\<Sum>(x,K) \<in> \<D>2. content K *\<^sub>R f x))
    3.88                    < 1 / (m + 1)"
    3.89      by metis
    3.90    have "\<And>n. gauge (\<lambda>x. \<Inter>{\<gamma> i x |i. i \<in> {0..n}})"
    3.91 @@ -993,8 +992,8 @@
    3.92      obtain N2::nat where N2: "\<And>n. n \<ge> N2 \<Longrightarrow> norm ((\<Sum>(x,K) \<in> p n. content K *\<^sub>R f x) - y) < e/2"
    3.93        using y[OF e2] by metis
    3.94      show "\<exists>\<gamma>. gauge \<gamma> \<and>
    3.95 -              (\<forall>p. p tagged_division_of (cbox a b) \<and> \<gamma> fine p \<longrightarrow>
    3.96 -                norm ((\<Sum>(x,K) \<in> p. content K *\<^sub>R f x) - y) < e)"
    3.97 +              (\<forall>\<D>. \<D> tagged_division_of (cbox a b) \<and> \<gamma> fine \<D> \<longrightarrow>
    3.98 +                norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - y) < e)"
    3.99      proof (intro exI conjI allI impI)
   3.100        show "gauge (\<gamma> (N1+N2))"
   3.101          using \<gamma> by auto
   3.102 @@ -1059,15 +1058,15 @@
   3.103      by auto
   3.104      obtain \<gamma>1 where \<gamma>1: "gauge \<gamma>1"
   3.105        and \<gamma>1norm:
   3.106 -        "\<And>p. \<lbrakk>p tagged_division_of cbox a b \<inter> {x. x \<bullet> k \<le> c}; \<gamma>1 fine p\<rbrakk>
   3.107 -             \<Longrightarrow> norm ((\<Sum>(x,K) \<in> p. content K *\<^sub>R f x) - i) < e/2"
   3.108 +        "\<And>\<D>. \<lbrakk>\<D> tagged_division_of cbox a b \<inter> {x. x \<bullet> k \<le> c}; \<gamma>1 fine \<D>\<rbrakk>
   3.109 +             \<Longrightarrow> norm ((\<Sum>(x,K) \<in> \<D>. content K *\<^sub>R f x) - i) < e/2"
   3.110         apply (rule has_integralD[OF fi[unfolded interval_split[OF k]] e])
   3.111         apply (simp add: interval_split[symmetric] k)
   3.112        done
   3.113      obtain \<gamma>2 where \<gamma>2: "gauge \<gamma>2"
   3.114        and \<gamma>2norm:
   3.115 -        "\<And>p. \<lbrakk>p tagged_division_of cbox a b \<inter> {x. c \<le> x \<bullet> k}; \<gamma>2 fine p\<rbrakk>
   3.116 -             \<Longrightarrow> norm ((\<Sum>(x, k) \<in> p. content k *\<^sub>R f x) - j) < e/2"
   3.117 +        "\<And>\<D>. \<lbrakk>\<D> tagged_division_of cbox a b \<inter> {x. c \<le> x \<bullet> k}; \<gamma>2 fine \<D>\<rbrakk>
   3.118 +             \<Longrightarrow> norm ((\<Sum>(x, k) \<in> \<D>. content k *\<^sub>R f x) - j) < e/2"
   3.119         apply (rule has_integralD[OF fj[unfolded interval_split[OF k]] e])
   3.120         apply (simp add: interval_split[symmetric] k)
   3.121         done
   3.122 @@ -1075,8 +1074,8 @@
   3.123    have "gauge ?\<gamma>"
   3.124      using \<gamma>1 \<gamma>2 unfolding gauge_def by auto
   3.125    then show "\<exists>\<gamma>. gauge \<gamma> \<and>
   3.126 -                 (\<forall>p. p tagged_division_of cbox a b \<and> \<gamma> fine p \<longrightarrow>
   3.127 -                      norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (i + j)) < e)"
   3.128 +                 (\<forall>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D> \<longrightarrow>
   3.129 +                      norm ((\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R f x) - (i + j)) < e)"
   3.130    proof (rule_tac x="?\<gamma>" in exI, safe)
   3.131      fix p
   3.132      assume p: "p tagged_division_of (cbox a b)" and "?\<gamma> fine p"
   3.133 @@ -1285,7 +1284,7 @@
   3.134      note p1=tagged_division_ofD[OF this(1)] 
   3.135      assume tdiv2: "p2 tagged_division_of (cbox a b) \<inter> {x. c \<le> x \<bullet> k}" and "\<gamma> fine p2"
   3.136      note p2=tagged_division_ofD[OF this(1)] 
   3.137 -    note tagged_division_union_interval[OF tdiv1 tdiv2] 
   3.138 +    note tagged_division_Un_interval[OF tdiv1 tdiv2] 
   3.139      note p12 = tagged_division_ofD[OF this] this
   3.140      { fix a b
   3.141        assume ab: "(a, b) \<in> p1 \<inter> p2"
   3.142 @@ -4140,7 +4139,7 @@
   3.143        using as by (auto simp add: field_simps)
   3.144  
   3.145      have "p \<union> {(c, {t..c})} tagged_division_of {a..c}"
   3.146 -      apply (rule tagged_division_union_interval_real[of _ _ _ 1 "t"])
   3.147 +      apply (rule tagged_division_Un_interval_real[of _ _ _ 1 "t"])
   3.148        using  \<open>t \<le> c\<close> by (auto simp: * ptag tagged_division_of_self_real)
   3.149      moreover
   3.150      have "d1 fine p \<union> {(c, {t..c})}"
   3.151 @@ -4762,9 +4761,9 @@
   3.152  
   3.153  lemma has_integral_le:
   3.154    fixes f :: "'n::euclidean_space \<Rightarrow> real"
   3.155 -  assumes "(f has_integral i) s"
   3.156 -    and "(g has_integral j) s"
   3.157 -    and "\<forall>x\<in>s. f x \<le> g x"
   3.158 +  assumes "(f has_integral i) S"
   3.159 +    and "(g has_integral j) S"
   3.160 +    and "\<And>x. x \<in> S \<Longrightarrow> f x \<le> g x"
   3.161    shows "i \<le> j"
   3.162    using has_integral_component_le[OF _ assms(1-2), of 1]
   3.163    using assms(3)
   3.164 @@ -4772,27 +4771,27 @@
   3.165  
   3.166  lemma integral_le:
   3.167    fixes f :: "'n::euclidean_space \<Rightarrow> real"
   3.168 -  assumes "f integrable_on s"
   3.169 -    and "g integrable_on s"
   3.170 -    and "\<forall>x\<in>s. f x \<le> g x"
   3.171 -  shows "integral s f \<le> integral s g"
   3.172 +  assumes "f integrable_on S"
   3.173 +    and "g integrable_on S"
   3.174 +    and "\<And>x. x \<in> S \<Longrightarrow> f x \<le> g x"
   3.175 +  shows "integral S f \<le> integral S g"
   3.176    by (rule has_integral_le[OF assms(1,2)[unfolded has_integral_integral] assms(3)])
   3.177  
   3.178  lemma has_integral_nonneg:
   3.179    fixes f :: "'n::euclidean_space \<Rightarrow> real"
   3.180 -  assumes "(f has_integral i) s"
   3.181 -    and "\<forall>x\<in>s. 0 \<le> f x"
   3.182 +  assumes "(f has_integral i) S"
   3.183 +    and "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x"
   3.184    shows "0 \<le> i"
   3.185 -  using has_integral_component_nonneg[of 1 f i s]
   3.186 +  using has_integral_component_nonneg[of 1 f i S]
   3.187    unfolding o_def
   3.188    using assms
   3.189    by auto
   3.190  
   3.191  lemma integral_nonneg:
   3.192    fixes f :: "'n::euclidean_space \<Rightarrow> real"
   3.193 -  assumes "f integrable_on s"
   3.194 -    and "\<forall>x\<in>s. 0 \<le> f x"
   3.195 -  shows "0 \<le> integral s f"
   3.196 +  assumes "f integrable_on S"
   3.197 +    and "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x"
   3.198 +  shows "0 \<le> integral S f"
   3.199    by (rule has_integral_nonneg[OF assms(1)[unfolded has_integral_integral] assms(2)])
   3.200  
   3.201  
   3.202 @@ -5686,9 +5685,9 @@
   3.203  
   3.204  subsection \<open>Henstock's lemma\<close>
   3.205  
   3.206 -lemma henstock_lemma_part1:
   3.207 +lemma Henstock_lemma_part1:
   3.208    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   3.209 -  assumes "f integrable_on cbox a b"
   3.210 +  assumes intf: "f integrable_on cbox a b"
   3.211      and "e > 0"
   3.212      and "gauge d"
   3.213      and less_e: "\<And>p. \<lbrakk>p tagged_division_of (cbox a b); d fine p\<rbrakk> \<Longrightarrow>
   3.214 @@ -5711,59 +5710,52 @@
   3.215    have r: "finite r"
   3.216      using q' unfolding r_def by auto
   3.217  
   3.218 -  have "\<forall>i\<in>r. \<exists>p. p tagged_division_of i \<and> d fine p \<and>
   3.219 -    norm (sum (\<lambda>(x,j). content j *\<^sub>R f x) p - integral i f) < k / (real (card r) + 1)"
   3.220 -    apply safe
   3.221 -  proof goal_cases
   3.222 -    case (1 i)
   3.223 -    then have i: "i \<in> q"
   3.224 -      unfolding r_def by auto
   3.225 -    from q'(4)[OF this] guess u v by (elim exE) note uv=this
   3.226 +  have "\<exists>p. p tagged_division_of i \<and> d fine p \<and>
   3.227 +        norm (sum (\<lambda>(x,j). content j *\<^sub>R f x) p - integral i f) < k / (real (card r) + 1)"
   3.228 +    if "i\<in>r" for i
   3.229 +  proof -
   3.230      have *: "k / (real (card r) + 1) > 0" using k by simp
   3.231 -    have "f integrable_on cbox u v"
   3.232 -      apply (rule integrable_subinterval[OF assms(1)])
   3.233 -      using q'(2)[OF i]
   3.234 -      unfolding uv
   3.235 -      apply auto
   3.236 -      done
   3.237 +    have i: "i \<in> q"
   3.238 +      using that unfolding r_def by auto
   3.239 +    then obtain u v where uv: "i = cbox u v"
   3.240 +      using q'(4) by blast
   3.241 +    then have "cbox u v \<subseteq> cbox a b"
   3.242 +      using i q'(2) by auto  
   3.243 +    then have "f integrable_on cbox u v"
   3.244 +      by (rule integrable_subinterval[OF intf])
   3.245      note integrable_integral[OF this, unfolded has_integral[of f]]
   3.246      from this[rule_format,OF *] guess dd..note dd=conjunctD2[OF this,rule_format]
   3.247      note gauge_Int[OF \<open>gauge d\<close> dd(1)]
   3.248      from fine_division_exists[OF this,of u v] guess qq .
   3.249 -    then show ?case
   3.250 +    then show ?thesis
   3.251        apply (rule_tac x=qq in exI)
   3.252        using dd(2)[of qq]
   3.253        unfolding fine_Int uv
   3.254        apply auto
   3.255        done
   3.256    qed
   3.257 -  from bchoice[OF this] guess qq..note qq=this[rule_format]
   3.258 +  then obtain qq where qq: "\<And>i. i \<in> r \<Longrightarrow> qq i tagged_division_of i \<and>
   3.259 +      d fine qq i \<and>
   3.260 +      norm
   3.261 +       ((\<Sum>(x, j) \<in> qq i. content j *\<^sub>R f x) -
   3.262 +        integral i f)
   3.263 +      < k / (real (card r) + 1)"
   3.264 +    by metis
   3.265  
   3.266    let ?p = "p \<union> \<Union>(qq ` r)"
   3.267    have "norm ((\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) - integral (cbox a b) f) < e"
   3.268    proof (rule less_e)
   3.269      show "d fine ?p"
   3.270        by (metis (mono_tags, hide_lams) qq fine_Un fine_Union imageE p(2))
   3.271 -    note * = tagged_partial_division_of_union_self[OF p(1)]
   3.272 +    note * = tagged_partial_division_of_Union_self[OF p(1)]
   3.273      have "p \<union> \<Union>(qq ` r) tagged_division_of \<Union>(snd ` p) \<union> \<Union>r"
   3.274        using r
   3.275 -    proof (rule tagged_division_union[OF * tagged_division_unions], goal_cases)
   3.276 -      case 1
   3.277 -      then show ?case
   3.278 +    proof (rule tagged_division_Un[OF * tagged_division_Union])
   3.279 +      show "\<And>i. i \<in> r \<Longrightarrow> qq i tagged_division_of i"
   3.280          using qq by auto
   3.281 -    next
   3.282 -      case 2
   3.283 -      then show ?case
   3.284 -        apply rule
   3.285 -        apply rule
   3.286 -        apply rule
   3.287 -        apply(rule q'(5))
   3.288 -        unfolding r_def
   3.289 -        apply auto
   3.290 -        done
   3.291 -    next
   3.292 -      case 3
   3.293 -      then show ?case
   3.294 +      show "\<And>i1 i2. \<lbrakk>i1 \<in> r; i2 \<in> r; i1 \<noteq> i2\<rbrakk> \<Longrightarrow> interior i1 \<inter> interior i2 = {}"
   3.295 +        by (simp add: q'(5) r_def)
   3.296 +      show "interior (UNION p snd) \<inter> interior (\<Union>r) = {}"
   3.297        proof (rule Int_interior_Union_intervals [OF \<open>finite r\<close>])
   3.298          show "open (interior (UNION p snd))"
   3.299            by blast
   3.300 @@ -5780,9 +5772,7 @@
   3.301        qed
   3.302      qed
   3.303      moreover have "\<Union>(snd ` p) \<union> \<Union>r = cbox a b" and "{qq i |i. i \<in> r} = qq ` r"
   3.304 -      unfolding Union_Un_distrib[symmetric] r_def
   3.305 -      using q
   3.306 -      by auto
   3.307 +      using q  unfolding Union_Un_distrib[symmetric] r_def by auto
   3.308      ultimately show "?p tagged_division_of (cbox a b)"
   3.309        by fastforce
   3.310    qed
   3.311 @@ -5915,11 +5905,11 @@
   3.312    finally show "?x \<le> e + k" .
   3.313  qed
   3.314  
   3.315 -lemma henstock_lemma_part2:
   3.316 +lemma Henstock_lemma_part2:
   3.317    fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
   3.318    assumes fed: "f integrable_on cbox a b" "e > 0" "gauge d"
   3.319 -    and less_e: "\<And>p. \<lbrakk>p tagged_division_of (cbox a b); d fine p\<rbrakk> \<Longrightarrow>
   3.320 -                     norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral (cbox a b) f) < e"
   3.321 +    and less_e: "\<And>\<D>. \<lbrakk>\<D> tagged_division_of (cbox a b); d fine \<D>\<rbrakk> \<Longrightarrow>
   3.322 +                     norm (sum (\<lambda>(x,k). content k *\<^sub>R f x) \<D> - integral (cbox a b) f) < e"
   3.323      and tag: "p tagged_partial_division_of (cbox a b)"
   3.324      and "d fine p"
   3.325    shows "sum (\<lambda>(x,k). norm (content k *\<^sub>R f x - integral k f)) p \<le> 2 * real (DIM('n)) * e"
   3.326 @@ -5934,13 +5924,13 @@
   3.327      then have fine: "d fine Q"
   3.328        by (simp add: \<open>d fine p\<close> fine_subset)
   3.329      show "norm (\<Sum>x\<in>Q. content (snd x) *\<^sub>R f (fst x) - integral (snd x) f) \<le> e"
   3.330 -      apply (rule henstock_lemma_part1[OF fed less_e, unfolded split_def])
   3.331 +      apply (rule Henstock_lemma_part1[OF fed less_e, unfolded split_def])
   3.332        using Q tag tagged_partial_division_subset apply (force simp add: fine)+
   3.333        done
   3.334    qed
   3.335  qed
   3.336  
   3.337 -lemma henstock_lemma:
   3.338 +lemma Henstock_lemma:
   3.339    fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
   3.340    assumes intf: "f integrable_on cbox a b"
   3.341      and "e > 0"
   3.342 @@ -5951,8 +5941,8 @@
   3.343    have *: "e/(2 * (real DIM('n) + 1)) > 0" using \<open>e > 0\<close> by simp
   3.344    with integrable_integral[OF intf, unfolded has_integral]
   3.345    obtain \<gamma> where "gauge \<gamma>"
   3.346 -    and \<gamma>: "\<And>p. \<lbrakk>p tagged_division_of cbox a b; \<gamma> fine p\<rbrakk> \<Longrightarrow>
   3.347 -         norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f x) - integral (cbox a b) f)
   3.348 +    and \<gamma>: "\<And>\<D>. \<lbrakk>\<D> tagged_division_of cbox a b; \<gamma> fine \<D>\<rbrakk> \<Longrightarrow>
   3.349 +         norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f x) - integral (cbox a b) f)
   3.350           < e/(2 * (real DIM('n) + 1))"
   3.351      by metis
   3.352    show thesis
   3.353 @@ -5961,7 +5951,7 @@
   3.354      assume p: "p tagged_partial_division_of cbox a b" "\<gamma> fine p"
   3.355      have "(\<Sum>(x,K)\<in>p. norm (content K *\<^sub>R f x - integral K f)) 
   3.356            \<le> 2 * real DIM('n) * (e/(2 * (real DIM('n) + 1)))"
   3.357 -      using henstock_lemma_part2[OF intf * \<open>gauge \<gamma>\<close> \<gamma> p] by metis
   3.358 +      using Henstock_lemma_part2[OF intf * \<open>gauge \<gamma>\<close> \<gamma> p] by metis
   3.359      also have "... < e"
   3.360        using \<open>e > 0\<close> by (auto simp add: field_simps)
   3.361      finally
   3.362 @@ -5972,14 +5962,12 @@
   3.363  
   3.364  subsection \<open>Monotone convergence (bounded interval first)\<close>
   3.365  
   3.366 -(* TODO: is this lemma necessary? *)
   3.367  lemma bounded_increasing_convergent:
   3.368    fixes f :: "nat \<Rightarrow> real"
   3.369    shows "\<lbrakk>bounded (range f); \<And>n. f n \<le> f (Suc n)\<rbrakk> \<Longrightarrow> \<exists>l. f \<longlonglongrightarrow> l"
   3.370    using Bseq_mono_convergent[of f] incseq_Suc_iff[of f]
   3.371    by (auto simp: image_def Bseq_eq_bounded convergent_def incseq_def)
   3.372  
   3.373 -(*FIXME: why so much " \<bullet> 1"? *)
   3.374  lemma monotone_convergence_interval:
   3.375    fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
   3.376    assumes intf: "\<And>k. (f k) integrable_on cbox a b"
   3.377 @@ -5988,57 +5976,53 @@
   3.378      and bou: "bounded (range (\<lambda>k. integral (cbox a b) (f k)))"
   3.379    shows "g integrable_on cbox a b \<and> ((\<lambda>k. integral (cbox a b) (f k)) \<longlongrightarrow> integral (cbox a b) g) sequentially"
   3.380  proof (cases "content (cbox a b) = 0")
   3.381 -  case True
   3.382 -  then show ?thesis
   3.383 +  case True then show ?thesis
   3.384      by auto
   3.385  next
   3.386    case False
   3.387 -  have fg1: "(f k x) \<bullet> 1 \<le> (g x) \<bullet> 1" if x: "x \<in> cbox a b" for x k
   3.388 +  have fg1: "(f k x) \<le> (g x)" if x: "x \<in> cbox a b" for x k
   3.389    proof -
   3.390 -    have "\<forall>\<^sub>F xa in sequentially. f k x \<bullet> 1 \<le> f xa x \<bullet> 1"
   3.391 -      unfolding eventually_sequentially
   3.392 -      apply (rule_tac x=k in exI)
   3.393 +    have "\<forall>\<^sub>F j in sequentially. f k x \<le> f j x"
   3.394 +      apply (rule eventually_sequentiallyI [of k])
   3.395        using le x apply (force intro: transitive_stepwise_le)
   3.396        done
   3.397 -    with Lim_component_ge [OF fg] x
   3.398 -    show "f k x \<bullet> 1 \<le> g x \<bullet> 1"
   3.399 -      using trivial_limit_sequentially by blast
   3.400 +    then show "f k x \<le> g x"
   3.401 +      using tendsto_lowerbound [OF fg] x trivial_limit_sequentially by blast
   3.402    qed
   3.403    have int_inc: "\<And>n. integral (cbox a b) (f n) \<le> integral (cbox a b) (f (Suc n))"
   3.404 -    by (metis integral_le assms(1-2))
   3.405 +    by (metis integral_le intf le)
   3.406    then obtain i where i: "(\<lambda>k. integral (cbox a b) (f k)) \<longlonglongrightarrow> i"
   3.407      using bounded_increasing_convergent bou by blast
   3.408 -  have "\<And>k. \<forall>\<^sub>F x in sequentially. integral (cbox a b) (f k) \<le> integral (cbox a b) (f x) \<bullet> 1"
   3.409 +  have "\<And>k. \<forall>\<^sub>F x in sequentially. integral (cbox a b) (f k) \<le> integral (cbox a b) (f x)"
   3.410      unfolding eventually_sequentially
   3.411      by (force intro: transitive_stepwise_le int_inc)
   3.412 -  then have i': "\<And>k. (integral(cbox a b) (f k)) \<le> i\<bullet>1"
   3.413 -    using Lim_component_ge [OF i] trivial_limit_sequentially by blast
   3.414 +  then have i': "\<And>k. (integral(cbox a b) (f k)) \<le> i"
   3.415 +    using tendsto_le [OF trivial_limit_sequentially i] by blast
   3.416    have "(g has_integral i) (cbox a b)"
   3.417      unfolding has_integral real_norm_def
   3.418    proof clarify
   3.419      fix e::real
   3.420      assume e: "e > 0"
   3.421 -    have "\<And>k. (\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
   3.422 -      abs ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f k x) - integral (cbox a b) (f k)) < e/2 ^ (k + 2)))"
   3.423 +    have "\<And>k. (\<exists>\<gamma>. gauge \<gamma> \<and> (\<forall>\<D>. \<D> tagged_division_of (cbox a b) \<and> \<gamma> fine \<D> \<longrightarrow>
   3.424 +      abs ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f k x) - integral (cbox a b) (f k)) < e/2 ^ (k + 2)))"
   3.425        using intf e by (auto simp: has_integral_integral has_integral)
   3.426 -    then obtain c where c:
   3.427 -          "\<And>x. gauge (c x)"
   3.428 -          "\<And>x p. \<lbrakk>p tagged_division_of cbox a b; c x fine p\<rbrakk> \<Longrightarrow>
   3.429 -              abs ((\<Sum>(u, ka)\<in>p. content ka *\<^sub>R f x u) - integral (cbox a b) (f x))
   3.430 +    then obtain c where c: "\<And>x. gauge (c x)"
   3.431 +          "\<And>x \<D>. \<lbrakk>\<D> tagged_division_of cbox a b; c x fine \<D>\<rbrakk> \<Longrightarrow>
   3.432 +              abs ((\<Sum>(u,K)\<in>\<D>. content K *\<^sub>R f x u) - integral (cbox a b) (f x))
   3.433                < e/2 ^ (x + 2)"
   3.434        by metis
   3.435  
   3.436 -    have "\<exists>r. \<forall>k\<ge>r. 0 \<le> i\<bullet>1 - (integral (cbox a b) (f k)) \<and> i\<bullet>1 - (integral (cbox a b) (f k)) < e/4"
   3.437 +    have "\<exists>r. \<forall>k\<ge>r. 0 \<le> i - (integral (cbox a b) (f k)) \<and> i - (integral (cbox a b) (f k)) < e/4"
   3.438      proof -
   3.439        have "e/4 > 0"
   3.440          using e by auto
   3.441        show ?thesis
   3.442          using LIMSEQ_D [OF i \<open>e/4 > 0\<close>] i' by auto
   3.443      qed
   3.444 -    then obtain r where r: "\<And>k. r \<le> k \<Longrightarrow> 0 \<le> i \<bullet> 1 - integral (cbox a b) (f k)"
   3.445 -                       "\<And>k. r \<le> k \<Longrightarrow> i \<bullet> 1 - integral (cbox a b) (f k) < e/4" 
   3.446 +    then obtain r where r: "\<And>k. r \<le> k \<Longrightarrow> 0 \<le> i - integral (cbox a b) (f k)"
   3.447 +                       "\<And>k. r \<le> k \<Longrightarrow> i - integral (cbox a b) (f k) < e/4" 
   3.448        by metis
   3.449 -    have "\<exists>n\<ge>r. \<forall>k\<ge>n. 0 \<le> (g x)\<bullet>1 - (f k x)\<bullet>1 \<and> (g x)\<bullet>1 - (f k x)\<bullet>1 < e/(4 * content(cbox a b))"
   3.450 +    have "\<exists>n\<ge>r. \<forall>k\<ge>n. 0 \<le> (g x) - (f k x) \<and> (g x) - (f k x) < e/(4 * content(cbox a b))"
   3.451        if "x \<in> cbox a b" for x
   3.452      proof -
   3.453        have "e/(4 * content (cbox a b)) > 0"
   3.454 @@ -6048,8 +6032,8 @@
   3.455          by metis
   3.456        then show "\<exists>n\<ge>r.
   3.457              \<forall>k\<ge>n.
   3.458 -               0 \<le> g x \<bullet> 1 - f k x \<bullet> 1 \<and>
   3.459 -               g x \<bullet> 1 - f k x \<bullet> 1
   3.460 +               0 \<le> g x - f k x \<and>
   3.461 +               g x - f k x
   3.462                 < e/(4 * content (cbox a b))"
   3.463          apply (rule_tac x="N + r" in exI)
   3.464          using fg1[OF that] apply (auto simp add: field_simps)
   3.465 @@ -6057,127 +6041,119 @@
   3.466      qed
   3.467      then obtain m where r_le_m: "\<And>x. x \<in> cbox a b \<Longrightarrow> r \<le> m x"
   3.468         and m: "\<And>x k. \<lbrakk>x \<in> cbox a b; m x \<le> k\<rbrakk>
   3.469 -                     \<Longrightarrow> 0 \<le> g x \<bullet> 1 - f k x \<bullet> 1 \<and> g x \<bullet> 1 - f k x \<bullet> 1 < e/(4 * content (cbox a b))"
   3.470 +                     \<Longrightarrow> 0 \<le> g x - f k x \<and> g x - f k x < e/(4 * content (cbox a b))"
   3.471        by metis
   3.472      define d where "d x = c (m x) x" for x
   3.473      show "\<exists>\<gamma>. gauge \<gamma> \<and>
   3.474 -             (\<forall>p. p tagged_division_of cbox a b \<and>
   3.475 -                  \<gamma> fine p \<longrightarrow> abs ((\<Sum>(x,K)\<in>p. content K *\<^sub>R g x) - i) < e)"
   3.476 +             (\<forall>\<D>. \<D> tagged_division_of cbox a b \<and>
   3.477 +                  \<gamma> fine \<D> \<longrightarrow> abs ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x) - i) < e)"
   3.478      proof (rule exI, safe)
   3.479        show "gauge d"
   3.480          using c(1) unfolding gauge_def d_def by auto
   3.481      next
   3.482 -      fix p
   3.483 -      assume p: "p tagged_division_of (cbox a b)" "d fine p"
   3.484 -      note p'=tagged_division_ofD[OF p(1)]
   3.485 -      obtain s where s: "\<And>x. x \<in> p \<Longrightarrow> m (fst x) \<le> s"
   3.486 +      fix \<D>
   3.487 +      assume ptag: "\<D> tagged_division_of (cbox a b)" and "d fine \<D>"
   3.488 +      note p'=tagged_division_ofD[OF ptag]
   3.489 +      obtain s where s: "\<And>x. x \<in> \<D> \<Longrightarrow> m (fst x) \<le> s"
   3.490          by (metis finite_imageI finite_nat_set_iff_bounded_le p'(1) rev_image_eqI)
   3.491        have *: "\<bar>a - d\<bar> < e" if "\<bar>a - b\<bar> \<le> e/4" "\<bar>b - c\<bar> < e/2" "\<bar>c - d\<bar> < e/4" for a b c d
   3.492          using that norm_triangle_lt[of "a - b" "b - c" "3* e/4"]
   3.493            norm_triangle_lt[of "a - b + (b - c)" "c - d" e]
   3.494          by (auto simp add: algebra_simps)
   3.495 -      show "abs ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - i) < e"
   3.496 +      show "\<bar>(\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R g x) - i\<bar> < e"
   3.497        proof (rule *)
   3.498 -        show "\<bar>(\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - (\<Sum>(x, K)\<in>p. content K *\<^sub>R f (m x) x)\<bar>
   3.499 -              \<le> e/4"
   3.500 -          apply (rule order_trans[of _ "\<Sum>(x, k)\<in>p. content k * (e/(4 * content (cbox a b)))"])
   3.501 -          unfolding sum_subtractf[symmetric]
   3.502 -          apply (rule order_trans)
   3.503 -          apply (rule sum_abs)
   3.504 -          apply (rule sum_mono)
   3.505 -          unfolding split_paired_all split_conv
   3.506 -          unfolding split_def sum_distrib_right[symmetric] scaleR_diff_right[symmetric]
   3.507 -          unfolding additive_content_tagged_division[OF p(1), unfolded split_def]
   3.508 -        proof -
   3.509 +        have "\<bar>(\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x) - (\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x)\<bar> 
   3.510 +              \<le> (\<Sum>i\<in>\<D>. \<bar>(case i of (x, K) \<Rightarrow> content K *\<^sub>R g x) - (case i of (x, K) \<Rightarrow> content K *\<^sub>R f (m x) x)\<bar>)"
   3.511 +          by (metis (mono_tags) sum_subtractf sum_abs) 
   3.512 +        also have "... \<le> (\<Sum>(x, k)\<in>\<D>. content k * (e/(4 * content (cbox a b))))"
   3.513 +        proof (rule sum_mono, simp add: split_paired_all)
   3.514            fix x K
   3.515 -          assume xk: "(x, K) \<in> p"
   3.516 -          then have x: "x \<in> cbox a b"
   3.517 -            using p'(2-3)[OF xk] by auto
   3.518 -          with p'(4)[OF xk] obtain u v where "K = cbox u v" by metis
   3.519 -          then show "abs (content K *\<^sub>R (g x - f (m x) x)) \<le> content K * (e/(4 * content (cbox a b)))"
   3.520 -            unfolding abs_scaleR using m[OF x]
   3.521 -            by (metis real_inner_1_right real_scaleR_def abs_of_nonneg inner_real_def less_eq_real_def measure_nonneg mult_left_mono order_refl)
   3.522 -        qed (insert False, auto)
   3.523 +          assume xk: "(x,K) \<in> \<D>"
   3.524 +          with ptag have x: "x \<in> cbox a b"
   3.525 +            by blast
   3.526 +          then have "abs (content K * (g x - f (m x) x)) \<le> content K * (e/(4 * content (cbox a b)))"
   3.527 +            by (metis m[OF x] mult_nonneg_nonneg abs_of_nonneg less_eq_real_def measure_nonneg mult_left_mono order_refl)
   3.528 +          then show "\<bar>content K * g x - content K * f (m x) x\<bar> \<le> content K * e / (4 * content (cbox a b))"
   3.529 +            by (simp add: algebra_simps)
   3.530 +        qed
   3.531 +        also have "... = (e / (4 * content (cbox a b))) * (\<Sum>(x, k)\<in>\<D>. content k)"
   3.532 +          by (simp add: sum_distrib_left sum_divide_distrib split_def mult.commute)
   3.533 +        also have "... \<le> e/4"
   3.534 +          by (metis False additive_content_tagged_division [OF ptag] nonzero_mult_divide_mult_cancel_right order_refl times_divide_eq_left)
   3.535 +        finally show "\<bar>(\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R g x) - (\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x)\<bar> \<le> e/4" .
   3.536  
   3.537        next
   3.538 -        have "norm ((\<Sum>(x, K)\<in>p. content K *\<^sub>R f (m x) x) - (\<Sum>(x, k)\<in>p. integral k (f (m x))))
   3.539 -              \<le> norm
   3.540 -                  (\<Sum>j = 0..s.
   3.541 -                      \<Sum>(x, K)\<in>{xk \<in> p. m (fst xk) = j}.
   3.542 -                        content K *\<^sub>R f (m x) x - integral K (f (m x)))"
   3.543 +        have "norm ((\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x) - (\<Sum>(x,K)\<in>\<D>. integral K (f (m x))))
   3.544 +              \<le> norm (\<Sum>j = 0..s. \<Sum>(x,K)\<in>{xk \<in> \<D>. m (fst xk) = j}. content K *\<^sub>R f (m x) x - integral K (f (m x)))"
   3.545            apply (subst sum_group)
   3.546            using s by (auto simp: sum_subtractf split_def p'(1))
   3.547          also have "\<dots> < e/2"
   3.548          proof -
   3.549 -          have "norm (\<Sum>j = 0..s. \<Sum>(x, k)\<in>{xk \<in> p. m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x)))
   3.550 +          have "norm (\<Sum>j = 0..s. \<Sum>(x, k)\<in>{xk \<in> \<D>. m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x)))
   3.551                  \<le> (\<Sum>i = 0..s. e/2 ^ (i + 2))"
   3.552            proof (rule sum_norm_le)
   3.553              fix t
   3.554              assume "t \<in> {0..s}"
   3.555 -            have "norm (\<Sum>(x,k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f (m x) x - integral k (f (m x))) =
   3.556 -                  norm (\<Sum>(x,k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f t x - integral k (f t))"
   3.557 +            have "norm (\<Sum>(x,k)\<in>{xk \<in> \<D>. m (fst xk) = t}. content k *\<^sub>R f (m x) x - integral k (f (m x))) =
   3.558 +                  norm (\<Sum>(x,k)\<in>{xk \<in> \<D>. m (fst xk) = t}. content k *\<^sub>R f t x - integral k (f t))"
   3.559                by (force intro!: sum.cong arg_cong[where f=norm])
   3.560              also have "... \<le> e/2 ^ (t + 2)"
   3.561 -            proof (rule henstock_lemma_part1 [OF intf])
   3.562 -              show "{xk \<in> p. m (fst xk) = t} tagged_partial_division_of cbox a b"
   3.563 -                apply (rule tagged_partial_division_subset[of p])
   3.564 -                using p by (auto simp: tagged_division_of_def)
   3.565 -              show "c t fine {xk \<in> p. m (fst xk) = t}"
   3.566 -                using p(2) by (auto simp: fine_def d_def)
   3.567 +            proof (rule Henstock_lemma_part1 [OF intf])
   3.568 +              show "{xk \<in> \<D>. m (fst xk) = t} tagged_partial_division_of cbox a b"
   3.569 +                apply (rule tagged_partial_division_subset[of \<D>])
   3.570 +                using ptag by (auto simp: tagged_division_of_def)
   3.571 +              show "c t fine {xk \<in> \<D>. m (fst xk) = t}"
   3.572 +                using \<open>d fine \<D>\<close> by (auto simp: fine_def d_def)
   3.573              qed (use c e in auto)
   3.574 -            finally show "norm (\<Sum>(x,K)\<in>{xk \<in> p. m (fst xk) = t}. content K *\<^sub>R f (m x) x -
   3.575 +            finally show "norm (\<Sum>(x,K)\<in>{xk \<in> \<D>. m (fst xk) = t}. content K *\<^sub>R f (m x) x -
   3.576                                  integral K (f (m x))) \<le> e/2 ^ (t + 2)" .
   3.577            qed
   3.578            also have "... = (e/2/2) * (\<Sum>i = 0..s. (1/2) ^ i)"
   3.579              by (simp add: sum_distrib_left field_simps)
   3.580            also have "\<dots> < e/2"
   3.581              by (simp add: sum_gp mult_strict_left_mono[OF _ e])
   3.582 -          finally show "norm (\<Sum>j = 0..s. \<Sum>(x, k)\<in>{xk \<in> p.
   3.583 +          finally show "norm (\<Sum>j = 0..s. \<Sum>(x, k)\<in>{xk \<in> \<D>.
   3.584              m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x))) < e/2" .
   3.585          qed 
   3.586 -        finally show "\<bar>(\<Sum>(x,K)\<in>p. content K *\<^sub>R f (m x) x) - (\<Sum>(x,K)\<in>p. integral K (f (m x)))\<bar> < e/2"
   3.587 +        finally show "\<bar>(\<Sum>(x,K)\<in>\<D>. content K *\<^sub>R f (m x) x) - (\<Sum>(x,K)\<in>\<D>. integral K (f (m x)))\<bar> < e/2"
   3.588            by simp
   3.589        next
   3.590 -        note comb = integral_combine_tagged_division_topdown[OF assms(1)[rule_format] p(1)]
   3.591 -        have *: "\<And>sr sx ss ks kr. \<lbrakk>kr = sr; ks = ss;
   3.592 -          ks \<le> i; sr \<le> sx; sx \<le> ss; 0 \<le> i\<bullet>1 - kr\<bullet>1; i\<bullet>1 - kr\<bullet>1 < e/4\<rbrakk> \<Longrightarrow> \<bar>sx - i\<bar> < e/4"
   3.593 -          by auto
   3.594 -        show "\<bar>(\<Sum>(x, k)\<in>p. integral k (f (m x))) - i\<bar> < e/4"
   3.595 -          unfolding real_norm_def
   3.596 -          apply (rule *)
   3.597 -          apply (rule comb[of r])
   3.598 -          apply (rule comb[of s])
   3.599 -          apply (rule i'[unfolded real_inner_1_right])
   3.600 -          apply (rule_tac[1-2] sum_mono)
   3.601 -          unfolding split_paired_all split_conv
   3.602 -          apply (rule_tac[1-2] integral_le[OF ])
   3.603 -        proof safe
   3.604 -          show "0 \<le> i\<bullet>1 - (integral (cbox a b) (f r))\<bullet>1" "i\<bullet>1 - (integral (cbox a b) (f r))\<bullet>1 < e/4"
   3.605 -            using r by auto
   3.606 +        have comb: "integral (cbox a b) (f y) = (\<Sum>(x, k)\<in>\<D>. integral k (f y))" for y
   3.607 +          using integral_combine_tagged_division_topdown[OF intf ptag] by metis
   3.608 +        have f_le: "\<And>y m n. \<lbrakk>y \<in> cbox a b; n\<ge>m\<rbrakk> \<Longrightarrow> f m y \<le> f n y"
   3.609 +          using le by (auto intro: transitive_stepwise_le)        
   3.610 +        have "(\<Sum>(x, k)\<in>\<D>. integral k (f r)) \<le> (\<Sum>(x, K)\<in>\<D>. integral K (f (m x)))"
   3.611 +        proof (rule sum_mono, simp add: split_paired_all)
   3.612            fix x K
   3.613 -          assume xk: "(x, K) \<in> p"
   3.614 -          from p'(4)[OF this] guess u v by (elim exE) note uv=this
   3.615 -          show "f r integrable_on K"
   3.616 -            and "f s integrable_on K"
   3.617 -            and "f (m x) integrable_on K"
   3.618 -            and "f (m x) integrable_on K"
   3.619 -            unfolding uv
   3.620 -            apply (rule_tac[!] integrable_on_subcbox[OF assms(1)[rule_format]])
   3.621 -            using p'(3)[OF xk]
   3.622 -            unfolding uv
   3.623 -            apply auto
   3.624 -            done
   3.625 -          fix y
   3.626 -          assume "y \<in> K"
   3.627 -          then have "y \<in> cbox a b"
   3.628 -            using p'(3)[OF xk] by auto
   3.629 -          then have *: "\<And>m n. n\<ge>m \<Longrightarrow> f m y \<le> f n y"
   3.630 -            using assms(2) by (auto intro: transitive_stepwise_le)
   3.631 -          show "f r y \<le> f (m x) y" "f (m x) y \<le> f s y"
   3.632 -            using s[rule_format,OF xk] r_le_m[of x] p'(2-3)[OF xk]
   3.633 -            apply (auto intro!: *)
   3.634 -            done
   3.635 +          assume xK: "(x, K) \<in> \<D>"
   3.636 +          show "integral K (f r) \<le> integral K (f (m x))"
   3.637 +          proof (rule integral_le)
   3.638 +            show "f r integrable_on K"
   3.639 +              by (metis integrable_on_subcbox intf p'(3) p'(4) xK)
   3.640 +            show "f (m x) integrable_on K"
   3.641 +              by (metis elementary_interval integrable_on_subdivision intf p'(3) p'(4) xK)
   3.642 +            show "f r y \<le> f (m x) y" if "y \<in> K" for y
   3.643 +              using that r_le_m[of x] p'(2-3)[OF xK] f_le by auto
   3.644 +          qed
   3.645          qed
   3.646 +        moreover have "(\<Sum>(x, K)\<in>\<D>. integral K (f (m x))) \<le> (\<Sum>(x, k)\<in>\<D>. integral k (f s))"
   3.647 +        proof (rule sum_mono, simp add: split_paired_all)
   3.648 +          fix x K
   3.649 +          assume xK: "(x, K) \<in> \<D>"
   3.650 +          show "integral K (f (m x)) \<le> integral K (f s)"
   3.651 +          proof (rule integral_le)
   3.652 +            show "f (m x) integrable_on K"
   3.653 +              by (metis elementary_interval integrable_on_subdivision intf p'(3) p'(4) xK)
   3.654 +            show "f s integrable_on K"
   3.655 +              by (metis integrable_on_subcbox intf p'(3) p'(4) xK)
   3.656 +            show "f (m x) y \<le> f s y" if "y \<in> K" for y
   3.657 +              using that s xK f_le p'(3) by fastforce
   3.658 +          qed
   3.659 +        qed
   3.660 +        moreover have "0 \<le> i - integral (cbox a b) (f r)" "i - integral (cbox a b) (f r) < e / 4"
   3.661 +          using r by auto
   3.662 +        ultimately show "\<bar>(\<Sum>(x,K)\<in>\<D>. integral K (f (m x))) - i\<bar> < e/4"
   3.663 +          using comb i'[of s] by auto
   3.664        qed
   3.665      qed
   3.666    qed 
   3.667 @@ -6201,23 +6177,19 @@
   3.668      and bou: "bounded (range(\<lambda>k. integral S (f k)))"
   3.669      for f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real" and g S
   3.670    proof -
   3.671 -    have fg: "(f k x)\<bullet>1 \<le> (g x)\<bullet>1" if "x \<in> S" for x k
   3.672 -      apply (rule Lim_component_ge [OF lim [OF that] trivial_limit_sequentially])
   3.673 -      unfolding eventually_sequentially
   3.674 -      apply (rule_tac x=k in exI)
   3.675 -      using le  by (force intro: transitive_stepwise_le that) 
   3.676 -
   3.677 +    have fg: "(f k x) \<le> (g x)" if "x \<in> S" for x k
   3.678 +      apply (rule tendsto_lowerbound [OF lim [OF that]])
   3.679 +      apply (rule eventually_sequentiallyI [of k])
   3.680 +      using le  by (force intro: transitive_stepwise_le that)+
   3.681      obtain i where i: "(\<lambda>k. integral S (f k)) \<longlonglongrightarrow> i"
   3.682        using bounded_increasing_convergent [OF bou] le int_f integral_le by blast
   3.683 -    have i': "(integral S (f k))\<bullet>1 \<le> i\<bullet>1" for k
   3.684 +    have i': "(integral S (f k)) \<le> i" for k
   3.685      proof -
   3.686 -      have *: "\<And>k. \<forall>x\<in>S. \<forall>n\<ge>k. f k x \<le> f n x"
   3.687 +      have "\<And>k. \<forall>x\<in>S. \<forall>n\<ge>k. f k x \<le> f n x"
   3.688          using le  by (force intro: transitive_stepwise_le)
   3.689 -      show ?thesis
   3.690 -        apply (rule Lim_component_ge [OF i trivial_limit_sequentially])
   3.691 -        unfolding eventually_sequentially
   3.692 -        apply (rule_tac x=k in exI)
   3.693 -        using * by (simp add: int_f integral_le)
   3.694 +      then show ?thesis
   3.695 +        using tendsto_lowerbound [OF i eventually_sequentiallyI trivial_limit_sequentially]
   3.696 +        by (meson int_f integral_le)
   3.697      qed
   3.698  
   3.699      let ?f = "(\<lambda>k x. if x \<in> S then f k x else 0)"
   3.700 @@ -6277,7 +6249,7 @@
   3.701            show "integral (cbox a b) (?f N) \<le> integral (cbox a b) (?f (M + N))"
   3.702            proof (intro ballI integral_le[OF int int])
   3.703              fix x assume "x \<in> cbox a b"
   3.704 -            have "(f m x)\<bullet>1 \<le> (f n x)\<bullet>1" if "x \<in> S" "n \<ge> m" for m n
   3.705 +            have "(f m x) \<le> (f n x)" if "x \<in> S" "n \<ge> m" for m n
   3.706                apply (rule transitive_stepwise_le [OF \<open>n \<ge> m\<close> order_refl])
   3.707                using dual_order.trans apply blast
   3.708                by (simp add: le \<open>x \<in> S\<close>)
   3.709 @@ -6416,41 +6388,41 @@
   3.710        by auto
   3.711      with integrable_integral[OF f,unfolded has_integral[of f]]
   3.712      obtain \<gamma> where \<gamma>: "gauge \<gamma>"
   3.713 -              "\<And>p. p tagged_division_of cbox a b \<and> \<gamma> fine p 
   3.714 -           \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - integral (cbox a b) f) < e/2"
   3.715 +              "\<And>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D> 
   3.716 +           \<Longrightarrow> norm ((\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R f x) - integral (cbox a b) f) < e/2"
   3.717        by meson 
   3.718      moreover
   3.719      from integrable_integral[OF g,unfolded has_integral[of g]] e
   3.720      obtain \<delta> where \<delta>: "gauge \<delta>"
   3.721 -              "\<And>p. p tagged_division_of cbox a b \<and> \<delta> fine p 
   3.722 -           \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - integral (cbox a b) g) < e/2"
   3.723 +              "\<And>\<D>. \<D> tagged_division_of cbox a b \<and> \<delta> fine \<D> 
   3.724 +           \<Longrightarrow> norm ((\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R g x) - integral (cbox a b) g) < e/2"
   3.725        by meson
   3.726      ultimately have "gauge (\<lambda>x. \<gamma> x \<inter> \<delta> x)"
   3.727        using gauge_Int by blast
   3.728 -    with fine_division_exists obtain p 
   3.729 -      where p: "p tagged_division_of cbox a b" "(\<lambda>x. \<gamma> x \<inter> \<delta> x) fine p" 
   3.730 +    with fine_division_exists obtain \<D> 
   3.731 +      where p: "\<D> tagged_division_of cbox a b" "(\<lambda>x. \<gamma> x \<inter> \<delta> x) fine \<D>" 
   3.732        by metis
   3.733 -    have "\<gamma> fine p" "\<delta> fine p"
   3.734 +    have "\<gamma> fine \<D>" "\<delta> fine \<D>"
   3.735        using fine_Int p(2) by blast+
   3.736      show "norm (integral (cbox a b) f) < integral (cbox a b) g + e"
   3.737      proof (rule norm)
   3.738 -      have "norm (content K *\<^sub>R f x) \<le> content K *\<^sub>R g x" if  "(x, K) \<in> p" for x K
   3.739 +      have "norm (content K *\<^sub>R f x) \<le> content K *\<^sub>R g x" if  "(x, K) \<in> \<D>" for x K
   3.740        proof-
   3.741          have K: "x \<in> K" "K \<subseteq> cbox a b"
   3.742 -          using \<open>(x, K) \<in> p\<close> p(1) by blast+
   3.743 +          using \<open>(x, K) \<in> \<D>\<close> p(1) by blast+
   3.744          obtain u v where  "K = cbox u v"
   3.745 -          using \<open>(x, K) \<in> p\<close> p(1) by blast
   3.746 +          using \<open>(x, K) \<in> \<D>\<close> p(1) by blast
   3.747          moreover have "content K * norm (f x) \<le> content K * g x"
   3.748            by (metis K subsetD dual_order.antisym measure_nonneg mult_zero_left nle not_le real_mult_le_cancel_iff2)
   3.749          then show ?thesis
   3.750            by simp
   3.751        qed
   3.752 -      then show "norm (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) \<le> (\<Sum>(x, k)\<in>p. content k *\<^sub>R g x)"
   3.753 +      then show "norm (\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R f x) \<le> (\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R g x)"
   3.754          by (simp add: sum_norm_le split_def)
   3.755 -      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - integral (cbox a b) f) < e/2"
   3.756 -        using \<open>\<gamma> fine p\<close> \<gamma> p(1) by simp
   3.757 -      show "\<bar>(\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - integral (cbox a b) g\<bar> < e/2"
   3.758 -        using \<open>\<delta> fine p\<close> \<delta> p(1) by simp
   3.759 +      show "norm ((\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R f x) - integral (cbox a b) f) < e/2"
   3.760 +        using \<open>\<gamma> fine \<D>\<close> \<gamma> p(1) by simp
   3.761 +      show "\<bar>(\<Sum>(x, k)\<in>\<D>. content k *\<^sub>R g x) - integral (cbox a b) g\<bar> < e/2"
   3.762 +        using \<open>\<delta> fine \<D>\<close> \<delta> p(1) by simp
   3.763      qed
   3.764    qed
   3.765    show ?thesis
   3.766 @@ -7184,13 +7156,13 @@
   3.767                \<le> e * content (cbox (u, w) (v, z)) / content ?CBOX"
   3.768          using that by (simp add: e'_def)
   3.769      } note op_acbd = this
   3.770 -    { fix k::real and p and u::'a and v w and z::'b and t1 t2 l
   3.771 +    { fix k::real and \<D> and u::'a and v w and z::'b and t1 t2 l
   3.772        assume k: "0 < k"
   3.773           and nf: "\<And>x y u v.
   3.774                    \<lbrakk>x \<in> cbox a b; y \<in> cbox c d; u \<in> cbox a b; v\<in>cbox c d; norm (u-x, v-y) < k\<rbrakk>
   3.775                    \<Longrightarrow> norm (f(u,v) - f(x,y)) < e/(2 * (content ?CBOX))"
   3.776 -         and p_acbd: "p tagged_division_of cbox (a,c) (b,d)"
   3.777 -         and fine: "(\<lambda>x. ball x k) fine p"  "((t1,t2), l) \<in> p"
   3.778 +         and p_acbd: "\<D> tagged_division_of cbox (a,c) (b,d)"
   3.779 +         and fine: "(\<lambda>x. ball x k) fine \<D>"  "((t1,t2), l) \<in> \<D>"
   3.780           and uwvz_sub: "cbox (u,w) (v,z) \<subseteq> l" "cbox (u,w) (v,z) \<subseteq> cbox (a,c) (b,d)"
   3.781        have t: "t1 \<in> cbox a b" "t2 \<in> cbox c d"
   3.782          by (meson fine p_acbd cbox_Pair_iff tag_in_interval)+
     4.1 --- a/src/HOL/Analysis/Improper_Integral.thy	Thu Aug 24 10:47:56 2017 +0200
     4.2 +++ b/src/HOL/Analysis/Improper_Integral.thy	Thu Aug 24 12:45:46 2017 +0100
     4.3 @@ -658,7 +658,7 @@
     4.4             if "S tagged_partial_division_of cbox a b" "\<gamma> fine S" "h \<in> F" for S h
     4.5        proof -
     4.6          have "(\<Sum>(x,K) \<in> S. norm (content K *\<^sub>R h x - integral K h)) \<le> 2 * real DIM('b) * (\<epsilon>/(5 * Suc DIM('b)))"
     4.7 -        proof (rule henstock_lemma_part2 [of h a b])
     4.8 +        proof (rule Henstock_lemma_part2 [of h a b])
     4.9            show "h integrable_on cbox a b"
    4.10              using that F equiintegrable_on_def by metis
    4.11            show "gauge \<gamma>"
    4.12 @@ -778,7 +778,7 @@
    4.13        qed
    4.14        also have "... = (\<Sum>K\<in>snd ` S. \<epsilon>/4 * (b \<bullet> i - a \<bullet> i) / content (cbox a b) * content K
    4.15                                       / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i))"
    4.16 -        apply (rule sum.over_tagged_division_lemma [OF tagged_partial_division_of_union_self [OF S]])
    4.17 +        apply (rule sum.over_tagged_division_lemma [OF tagged_partial_division_of_Union_self [OF S]])
    4.18          apply (simp add: box_eq_empty(1) content_eq_0)
    4.19          done
    4.20        also have "... = \<epsilon>/2 * ((b \<bullet> i - a \<bullet> i) / (2 * content (cbox a b)) * (\<Sum>K\<in>snd ` S. content K / (interval_upperbound K \<bullet> i - interval_lowerbound K \<bullet> i)))"
    4.21 @@ -789,7 +789,7 @@
    4.22                \<le> 2 * content (cbox a b)"
    4.23          proof (rule sum_content_area_over_thin_division)
    4.24            show "snd ` S division_of \<Union>(snd ` S)"
    4.25 -            by (auto intro: S tagged_partial_division_of_union_self division_of_tagged_division)
    4.26 +            by (auto intro: S tagged_partial_division_of_Union_self division_of_tagged_division)
    4.27            show "UNION S snd \<subseteq> cbox a b"
    4.28              using S by force
    4.29            show "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> b \<bullet> i"
    4.30 @@ -861,7 +861,7 @@
    4.31          if "T tagged_partial_division_of cbox a b" "\<gamma>1 fine T" "h \<in> F" for T h
    4.32        proof -
    4.33          have "(\<Sum>(x,K) \<in> T. norm (?CI K h x)) \<le> 2 * real DIM('b) * (\<epsilon>/(7 * Suc DIM('b)))"
    4.34 -        proof (rule henstock_lemma_part2 [of h a b])
    4.35 +        proof (rule Henstock_lemma_part2 [of h a b])
    4.36            show "h integrable_on cbox a b"
    4.37              using that F equiintegrable_on_def by metis
    4.38            show "gauge \<gamma>1"
    4.39 @@ -985,7 +985,7 @@
    4.40                      obtain u v where uv: "L = cbox u v"
    4.41                        using T'_tagged \<open>(x, L) \<in> A\<close> \<open>A \<subseteq> T''\<close> \<open>T'' \<subseteq> T'\<close> by blast
    4.42                      have "A tagged_division_of UNION A snd"
    4.43 -                      using A_tagged tagged_partial_division_of_union_self by auto
    4.44 +                      using A_tagged tagged_partial_division_of_Union_self by auto
    4.45                      then have "interior (K \<inter> {x. x \<bullet> i \<le> c}) = {}"
    4.46                        apply (rule tagged_division_split_left_inj [OF _ \<open>(x,K) \<in> A\<close> \<open>(x,L) \<in> A\<close>])
    4.47                        using that eq \<open>i \<in> Basis\<close> by auto
    4.48 @@ -1014,7 +1014,7 @@
    4.49                      obtain u v where uv: "L = cbox u v"
    4.50                        using T'_tagged \<open>(x, L) \<in> B\<close> \<open>B \<subseteq> T''\<close> \<open>T'' \<subseteq> T'\<close> by blast
    4.51                      have "B tagged_division_of UNION B snd"
    4.52 -                      using B_tagged tagged_partial_division_of_union_self by auto
    4.53 +                      using B_tagged tagged_partial_division_of_Union_self by auto
    4.54                      then have "interior (K \<inter> {x. c \<le> x \<bullet> i}) = {}"
    4.55                        apply (rule tagged_division_split_right_inj [OF _ \<open>(x,K) \<in> B\<close> \<open>(x,L) \<in> B\<close>])
    4.56                        using that eq \<open>i \<in> Basis\<close> by auto
     5.1 --- a/src/HOL/Analysis/Tagged_Division.thy	Thu Aug 24 10:47:56 2017 +0200
     5.2 +++ b/src/HOL/Analysis/Tagged_Division.thy	Thu Aug 24 12:45:46 2017 +0100
     5.3 @@ -1122,7 +1122,7 @@
     5.4    unfolding box_real[symmetric]
     5.5    by (rule tagged_division_of_self)
     5.6  
     5.7 -lemma tagged_division_union:
     5.8 +lemma tagged_division_Un:
     5.9    assumes "p1 tagged_division_of s1"
    5.10      and "p2 tagged_division_of s2"
    5.11      and "interior s1 \<inter> interior s2 = {}"
    5.12 @@ -1150,13 +1150,13 @@
    5.13      by (metis "*" UnE assms(1) assms(2) inf_sup_aci(1) p2(5) tagged_division_ofD(3) xk xk'(1) xk'(2))
    5.14  qed
    5.15  
    5.16 -lemma tagged_division_unions:
    5.17 +lemma tagged_division_Union:
    5.18    assumes "finite I"
    5.19 -    and "\<forall>i\<in>I. pfn i tagged_division_of i"
    5.20 -    and "\<forall>i1\<in>I. \<forall>i2\<in>I. i1 \<noteq> i2 \<longrightarrow> interior(i1) \<inter> interior(i2) = {}"
    5.21 +    and tag: "\<And>i. i\<in>I \<Longrightarrow> pfn i tagged_division_of i"
    5.22 +    and disj: "\<And>i1 i2. \<lbrakk>i1 \<in> I; i2 \<in> I; i1 \<noteq> i2\<rbrakk> \<Longrightarrow> interior(i1) \<inter> interior(i2) = {}"
    5.23    shows "\<Union>(pfn ` I) tagged_division_of (\<Union>I)"
    5.24  proof (rule tagged_division_ofI)
    5.25 -  note assm = tagged_division_ofD[OF assms(2)[rule_format]]
    5.26 +  note assm = tagged_division_ofD[OF tag]
    5.27    show "finite (\<Union>(pfn ` I))"
    5.28      using assms by auto
    5.29    have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` I)} = \<Union>((\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` I)"
    5.30 @@ -1175,16 +1175,18 @@
    5.31    then obtain i' where i': "i' \<in> I" "(x', k') \<in> pfn i'"
    5.32      by auto
    5.33    have *: "\<And>a b. i \<noteq> i' \<Longrightarrow> a \<subseteq> i \<Longrightarrow> b \<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}"
    5.34 -    using i(1) i'(1)
    5.35 -    using assms(3)[rule_format] interior_mono
    5.36 -    by blast
    5.37 +    using i(1) i'(1) disj interior_mono by blast
    5.38    show "interior k \<inter> interior k' = {}"
    5.39 -    apply (cases "i = i'")
    5.40 -    using assm(5) i' i(2) xk'(2) apply blast
    5.41 +  proof (cases "i = i'")
    5.42 +    case True then show ?thesis 
    5.43 +      using assm(5) i' i xk'(2) by blast
    5.44 +  next
    5.45 +    case False then show ?thesis 
    5.46      using "*" assm(3) i' i by auto
    5.47 +  qed
    5.48  qed
    5.49  
    5.50 -lemma tagged_partial_division_of_union_self:
    5.51 +lemma tagged_partial_division_of_Union_self:
    5.52    assumes "p tagged_partial_division_of s"
    5.53    shows "p tagged_division_of (\<Union>(snd ` p))"
    5.54    apply (rule tagged_division_ofI)
    5.55 @@ -1200,7 +1202,7 @@
    5.56    apply auto
    5.57    done
    5.58  
    5.59 -lemma tagged_division_union_interval:
    5.60 +lemma tagged_division_Un_interval:
    5.61    fixes a :: "'a::euclidean_space"
    5.62    assumes "p1 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<le> (c::real)})"
    5.63      and "p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
    5.64 @@ -1211,14 +1213,14 @@
    5.65      by auto
    5.66    show ?thesis
    5.67      apply (subst *)
    5.68 -    apply (rule tagged_division_union[OF assms(1-2)])
    5.69 +    apply (rule tagged_division_Un[OF assms(1-2)])
    5.70      unfolding interval_split[OF k] interior_cbox
    5.71      using k
    5.72      apply (auto simp add: box_def elim!: ballE[where x=k])
    5.73      done
    5.74  qed
    5.75  
    5.76 -lemma tagged_division_union_interval_real:
    5.77 +lemma tagged_division_Un_interval_real:
    5.78    fixes a :: real
    5.79    assumes "p1 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<le> (c::real)})"
    5.80      and "p2 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<ge> c})"
    5.81 @@ -1226,7 +1228,7 @@
    5.82    shows "(p1 \<union> p2) tagged_division_of {a .. b}"
    5.83    using assms
    5.84    unfolding box_real[symmetric]
    5.85 -  by (rule tagged_division_union_interval)
    5.86 +  by (rule tagged_division_Un_interval)
    5.87  
    5.88  lemma tagged_division_split_left_inj:
    5.89    assumes d: "d tagged_division_of i"
    5.90 @@ -1539,7 +1541,7 @@
    5.91        done
    5.92      by (simp add: interval_split k interval_doublesplit)
    5.93  qed
    5.94 -
    5.95 +              
    5.96  paragraph \<open>Operative\<close>
    5.97  
    5.98  locale operative = comm_monoid_set +
    5.99 @@ -1571,7 +1573,7 @@
   5.100        assume "box a b = {}"
   5.101        { fix k assume "k\<in>d"
   5.102          then obtain a' b' where k: "k = cbox a' b'"
   5.103 -          using division_ofD(4) [OF less.prems] by blast
   5.104 +          using division_ofD(4)[OF less.prems] by blast
   5.105          with \<open>k\<in>d\<close> division_ofD(2)[OF less.prems] have "cbox a' b' \<subseteq> cbox a b"
   5.106            by auto
   5.107          then have "box a' b' \<subseteq> box a b"
   5.108 @@ -1754,7 +1756,7 @@
   5.109      using assms box_empty_imp by (rule over_tagged_division_lemma)
   5.110    then show ?thesis
   5.111      unfolding assms [THEN division_of_tagged_division, THEN division] .
   5.112 -qed
   5.113 +  qed
   5.114  
   5.115  end
   5.116  
   5.117 @@ -1779,14 +1781,14 @@
   5.118        from that have [simp]: "k = 1"
   5.119          by simp
   5.120        from neutral [of 0 1] neutral [of a a for a] coalesce_less
   5.121 -      have [simp]: "g {} = \<^bold>1" "\<And>a. g {a} = \<^bold>1"
   5.122 -        "\<And>a b c. a < c \<Longrightarrow> c < b \<Longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
   5.123 -        by auto
   5.124 +  have [simp]: "g {} = \<^bold>1" "\<And>a. g {a} = \<^bold>1"
   5.125 +    "\<And>a b c. a < c \<Longrightarrow> c < b \<Longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
   5.126 +    by auto
   5.127        have "g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}"
   5.128 -        by (auto simp: min_def max_def le_less)
   5.129 +    by (auto simp: min_def max_def le_less)
   5.130        then show "g (cbox a b) = g (cbox a b \<inter> {x. x \<bullet> k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. c \<le> x \<bullet> k})"
   5.131          by (simp add: atMost_def [symmetric] atLeast_def [symmetric])
   5.132 -    qed
   5.133 +qed
   5.134    qed
   5.135    show "box = (greaterThanLessThan :: real \<Rightarrow> _)"
   5.136      and "cbox = (atLeastAtMost :: real \<Rightarrow> _)"
   5.137 @@ -1796,17 +1798,17 @@
   5.138  
   5.139  lemma coalesce_less_eq:
   5.140    "g {a..c} \<^bold>* g {c..b} = g {a..b}" if "a \<le> c" "c \<le> b"
   5.141 -proof (cases "c = a \<or> c = b")
   5.142 -  case False
   5.143 +  proof (cases "c = a \<or> c = b")
   5.144 +    case False
   5.145    with that have "a < c" "c < b"
   5.146      by auto
   5.147 -  then show ?thesis
   5.148 +    then show ?thesis
   5.149      by (rule coalesce_less)
   5.150 -next
   5.151 -  case True
   5.152 +  next
   5.153 +    case True
   5.154    with that box_empty_imp [of a a] box_empty_imp [of b b] show ?thesis
   5.155      by safe simp_all
   5.156 -qed
   5.157 +    qed
   5.158  
   5.159  end
   5.160  
   5.161 @@ -1823,7 +1825,7 @@
   5.162        using that
   5.163      using Basis_imp [of 1 a b c]
   5.164        by (simp_all add: atMost_def [symmetric] atLeast_def [symmetric] max_def min_def)
   5.165 -  qed
   5.166 +qed
   5.167  qed
   5.168  
   5.169  
   5.170 @@ -1901,7 +1903,7 @@
   5.171      using bchoice[OF assms(2)] by auto
   5.172    show thesis
   5.173      apply (rule_tac p="\<Union>(pfn ` I)" in that)
   5.174 -    using assms(1) assms(3) assms(4) pfn(1) tagged_division_unions apply force
   5.175 +    using assms(1) assms(3) assms(4) pfn(1) tagged_division_Union apply force
   5.176      by (metis (mono_tags, lifting) fine_Union imageE pfn(2))
   5.177  qed
   5.178  
   5.179 @@ -2252,7 +2254,7 @@
   5.180            \<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
   5.181      apply (rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p", OF _ _ False])
   5.182      apply (simp add: fine_def)
   5.183 -    apply (metis tagged_division_union fine_Un)
   5.184 +    apply (metis tagged_division_Un fine_Un)
   5.185      apply auto
   5.186      done
   5.187    obtain e where e: "e > 0" "ball x e \<subseteq> g x"
   5.188 @@ -2343,7 +2345,7 @@
   5.189        have "{(x, cbox u v)} tagged_division_of cbox u v"
   5.190          by (simp add: p(2) uv xk tagged_division_of_self)
   5.191        then have "{(x, cbox u v)} \<union> q1 tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> insert xk p}"
   5.192 -        unfolding * uv by (metis (no_types, lifting) int q1 tagged_division_union)
   5.193 +        unfolding * uv by (metis (no_types, lifting) int q1 tagged_division_Un)
   5.194        with True show ?thesis
   5.195          apply (rule_tac x="{(x,cbox u v)} \<union> q1" in exI)
   5.196          using \<open>d fine q1\<close> fine_def q1I uv xk apply fastforce
   5.197 @@ -2356,7 +2358,7 @@
   5.198          apply (rule_tac x="q2 \<union> q1" in exI)
   5.199          apply (intro conjI)
   5.200          unfolding * uv
   5.201 -        apply (rule tagged_division_union q2 q1 int fine_Un)+
   5.202 +        apply (rule tagged_division_Un q2 q1 int fine_Un)+
   5.203            apply (auto intro: q1 q2 fine_Un \<open>d fine q1\<close> simp add: False q1I uv xk)
   5.204          done
   5.205      qed