Useful lemmas. The theorem concerning swapping the variables in a double integral.
authorpaulson <lp15@cam.ac.uk>
Tue Jun 30 13:56:16 2015 +0100 (2015-06-30)
changeset 60615e5fa1d5d3952
parent 60605 9627a75eb32a
child 60616 5a65c496d96f
Useful lemmas. The theorem concerning swapping the variables in a double integral.
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NthRoot.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Set_Integral.thy
src/HOL/Rings.thy
src/HOL/Set_Interval.thy
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Mon Jun 29 13:49:21 2015 +0200
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Jun 30 13:56:16 2015 +0100
     1.3 @@ -302,10 +302,10 @@
     1.4  lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> SUPREMUM A f"
     1.5    by (auto intro: cSUP_upper assms order_trans)
     1.6  
     1.7 -lemma cSUP_const: "A \<noteq> {} \<Longrightarrow> (SUP x:A. c) = c"
     1.8 +lemma cSUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (SUP x:A. c) = c"
     1.9    by (intro antisym cSUP_least) (auto intro: cSUP_upper)
    1.10  
    1.11 -lemma cINF_const: "A \<noteq> {} \<Longrightarrow> (INF x:A. c) = c"
    1.12 +lemma cINF_const [simp]: "A \<noteq> {} \<Longrightarrow> (INF x:A. c) = c"
    1.13    by (intro antisym cINF_greatest) (auto intro: cINF_lower)
    1.14  
    1.15  lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> INFIMUM A f \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)"
    1.16 @@ -634,4 +634,16 @@
    1.17      by (elim exE disjE) auto
    1.18  qed
    1.19  
    1.20 +lemma cSUP_eq_cINF_D:
    1.21 +  fixes f :: "_ \<Rightarrow> 'b::conditionally_complete_lattice"
    1.22 +  assumes eq: "(SUP x:A. f x) = (INF x:A. f x)"
    1.23 +     and bdd: "bdd_above (f ` A)" "bdd_below (f ` A)"
    1.24 +     and a: "a \<in> A"
    1.25 +  shows "f a = (INF x:A. f x)"
    1.26 +apply (rule antisym)
    1.27 +using a bdd
    1.28 +apply (auto simp: cINF_lower)
    1.29 +apply (metis eq cSUP_upper)
    1.30 +done 
    1.31 +
    1.32  end
     2.1 --- a/src/HOL/Library/Product_Vector.thy	Mon Jun 29 13:49:21 2015 +0200
     2.2 +++ b/src/HOL/Library/Product_Vector.thy	Tue Jun 30 13:56:16 2015 +0100
     2.3 @@ -213,6 +213,9 @@
     2.4  lemma continuous_on_Pair[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. (f x, g x))"
     2.5    unfolding continuous_on_def by (auto intro: tendsto_Pair)
     2.6  
     2.7 +lemma continuous_on_swap[continuous_intros]: "continuous_on A prod.swap"
     2.8 +  by (simp add: prod.swap_def continuous_on_fst continuous_on_snd continuous_on_Pair continuous_on_id)
     2.9 +
    2.10  lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
    2.11    by (fact continuous_fst)
    2.12  
    2.13 @@ -254,6 +257,9 @@
    2.14      by (fast dest: hausdorff elim: open_vimage_fst open_vimage_snd)
    2.15  qed
    2.16  
    2.17 +lemma isCont_swap[continuous_intros]: "isCont prod.swap a"
    2.18 +  using continuous_on_eq_continuous_within continuous_on_swap by blast
    2.19 +
    2.20  subsection \<open>Product is a metric space\<close>
    2.21  
    2.22  instantiation prod :: (metric_space, metric_space) metric_space
    2.23 @@ -439,15 +445,6 @@
    2.24    using snd_add snd_scaleR
    2.25    by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
    2.26  
    2.27 -text \<open>TODO: move to NthRoot\<close>
    2.28 -lemma sqrt_add_le_add_sqrt:
    2.29 -  assumes x: "0 \<le> x" and y: "0 \<le> y"
    2.30 -  shows "sqrt (x + y) \<le> sqrt x + sqrt y"
    2.31 -apply (rule power2_le_imp_le)
    2.32 -apply (simp add: power2_sum x y)
    2.33 -apply (simp add: x y)
    2.34 -done
    2.35 -
    2.36  lemma bounded_linear_Pair:
    2.37    assumes f: "bounded_linear f"
    2.38    assumes g: "bounded_linear g"
    2.39 @@ -541,5 +538,11 @@
    2.40  lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a"
    2.41      by (cases x, simp)+
    2.42  
    2.43 +lemma 
    2.44 +  fixes x :: "'a::real_normed_vector"
    2.45 +  shows norm_Pair1 [simp]: "norm (0,x) = norm x" 
    2.46 +    and norm_Pair2 [simp]: "norm (x,0) = norm x"
    2.47 +by (auto simp: norm_Pair)
    2.48 +
    2.49  
    2.50  end
     3.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Jun 29 13:49:21 2015 +0200
     3.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Jun 30 13:56:16 2015 +0100
     3.3 @@ -394,7 +394,7 @@
     3.4            then have "x \<in> s \<inter> interior (\<Union>f)"
     3.5              unfolding lem1[where U="\<Union>f", symmetric]
     3.6              using centre_in_ball e by auto
     3.7 -          then show ?thesis 
     3.8 +          then show ?thesis
     3.9              using insert.hyps(3) insert.prems(1) by blast
    3.10          qed
    3.11        qed
    3.12 @@ -445,7 +445,7 @@
    3.13    using assms unfolding box_ne_empty by auto
    3.14  
    3.15  
    3.16 -lemma interval_upperbound_Times: 
    3.17 +lemma interval_upperbound_Times:
    3.18    assumes "A \<noteq> {}" and "B \<noteq> {}"
    3.19    shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)"
    3.20  proof-
    3.21 @@ -459,7 +459,7 @@
    3.22        by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
    3.23  qed
    3.24  
    3.25 -lemma interval_lowerbound_Times: 
    3.26 +lemma interval_lowerbound_Times:
    3.27    assumes "A \<noteq> {}" and "B \<noteq> {}"
    3.28    shows "interval_lowerbound (A \<times> B) = (interval_lowerbound A, interval_lowerbound B)"
    3.29  proof-
    3.30 @@ -505,7 +505,7 @@
    3.31    then show ?thesis by (simp add: cbox_sing)
    3.32  qed
    3.33  
    3.34 -lemma content_unit[intro]: "content(cbox 0 (One::'a::euclidean_space)) = 1"
    3.35 +lemma content_unit[iff]: "content(cbox 0 (One::'a::euclidean_space)) = 1"
    3.36   proof -
    3.37     have *: "\<forall>i\<in>Basis. (0::'a)\<bullet>i \<le> (One::'a)\<bullet>i"
    3.38      by auto
    3.39 @@ -532,6 +532,11 @@
    3.40    finally show ?thesis .
    3.41  qed (simp add: content_def)
    3.42  
    3.43 +corollary content_nonneg [simp]:
    3.44 +  fixes a::"'a::euclidean_space"
    3.45 +  shows "~ content (cbox a b) < 0"
    3.46 +using not_le by blast
    3.47 +
    3.48  lemma content_pos_lt:
    3.49    fixes a :: "'a::euclidean_space"
    3.50    assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
    3.51 @@ -607,7 +612,7 @@
    3.52    let ?ub1 = "interval_upperbound" and ?lb1 = "interval_lowerbound"
    3.53    let ?ub2 = "interval_upperbound" and ?lb2 = "interval_lowerbound"
    3.54    assume nonempty: "A \<times> B \<noteq> {}"
    3.55 -  hence "content (A \<times> B) = (\<Prod>i\<in>Basis. (?ub1 A, ?ub2 B) \<bullet> i - (?lb1 A, ?lb2 B) \<bullet> i)" 
    3.56 +  hence "content (A \<times> B) = (\<Prod>i\<in>Basis. (?ub1 A, ?ub2 B) \<bullet> i - (?lb1 A, ?lb2 B) \<bullet> i)"
    3.57        unfolding content_def by (simp add: interval_upperbound_Times interval_lowerbound_Times)
    3.58    also have "... = content A * content B" unfolding content_def using nonempty
    3.59      apply (subst Basis_prod_def, subst setprod.union_disjoint, force, force, force, simp)
    3.60 @@ -616,6 +621,50 @@
    3.61    finally show ?thesis .
    3.62  qed (auto simp: content_def)
    3.63  
    3.64 +lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)"
    3.65 +  by (simp add: cbox_Pair_eq)
    3.66 +
    3.67 +lemma content_cbox_pair_eq0_D:
    3.68 +   "content (cbox (a,c) (b,d)) = 0 \<Longrightarrow> content (cbox a b) = 0 \<or> content (cbox c d) = 0"
    3.69 +  by (simp add: content_Pair)
    3.70 +
    3.71 +lemma content_eq_0_gen:
    3.72 +  fixes s :: "'a::euclidean_space set"
    3.73 +  assumes "bounded s"
    3.74 +  shows "content s = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. \<exists>v. \<forall>x \<in> s. x \<bullet> i = v)"  (is "_ = ?rhs")
    3.75 +proof safe
    3.76 +  assume "content s = 0" then show ?rhs
    3.77 +    apply (clarsimp simp: ex_in_conv content_def split: split_if_asm)
    3.78 +    apply (rule_tac x=a in bexI)
    3.79 +    apply (rule_tac x="interval_lowerbound s \<bullet> a" in exI)
    3.80 +    apply (clarsimp simp: interval_upperbound_def interval_lowerbound_def)
    3.81 +    apply (drule cSUP_eq_cINF_D)
    3.82 +    apply (auto simp: bounded_inner_imp_bdd_above [OF assms]  bounded_inner_imp_bdd_below [OF assms])
    3.83 +    done
    3.84 +next
    3.85 +  fix i a
    3.86 +  assume "i \<in> Basis" "\<forall>x\<in>s. x \<bullet> i = a"
    3.87 +  then show "content s = 0"
    3.88 +    apply (clarsimp simp: content_def)
    3.89 +    apply (rule_tac x=i in bexI)
    3.90 +    apply (auto simp: interval_upperbound_def interval_lowerbound_def)
    3.91 +    done
    3.92 +qed
    3.93 +
    3.94 +lemma content_0_subset_gen:
    3.95 +  fixes a :: "'a::euclidean_space"
    3.96 +  assumes "content t = 0" "s \<subseteq> t" "bounded t" shows "content s = 0"
    3.97 +proof -
    3.98 +  have "bounded s"
    3.99 +    using assms by (metis bounded_subset)
   3.100 +  then show ?thesis
   3.101 +    using assms
   3.102 +    by (auto simp: content_eq_0_gen)
   3.103 +qed
   3.104 +
   3.105 +lemma content_0_subset: "\<lbrakk>content(cbox a b) = 0; s \<subseteq> cbox a b\<rbrakk> \<Longrightarrow> content s = 0"
   3.106 +  by (simp add: content_0_subset_gen bounded_cbox)
   3.107 +
   3.108  
   3.109  subsection \<open>The notion of a gauge --- simply an open set containing the point.\<close>
   3.110  
   3.111 @@ -1104,7 +1153,7 @@
   3.112        apply (rule division_disjoint_union[OF d assms(1)])
   3.113        apply (rule inter_interior_unions_intervals)
   3.114        apply (rule p open_interior ballI)+
   3.115 -      apply simp_all 
   3.116 +      apply simp_all
   3.117        done
   3.118    qed
   3.119    then show ?thesis
   3.120 @@ -1162,7 +1211,7 @@
   3.121        apply auto
   3.122        done
   3.123      finally have [simp]: "interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}" by simp
   3.124 -    have cbe: "cbox a b \<union> cbox c d = cbox a b \<union> \<Union>(p - {cbox u v})" 
   3.125 +    have cbe: "cbox a b \<union> cbox c d = cbox a b \<union> \<Union>(p - {cbox u v})"
   3.126        using p(8) unfolding uv[symmetric] by auto
   3.127      show ?thesis
   3.128        apply (rule that[of "p - {cbox u v}"])
   3.129 @@ -1221,7 +1270,7 @@
   3.130    next
   3.131      assume as: "p \<noteq> {}" "interior (cbox a b) \<noteq> {}" "cbox a b \<noteq> {}"
   3.132      have "\<forall>k\<in>p. \<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)"
   3.133 -    proof 
   3.134 +    proof
   3.135        case goal1
   3.136        from assm(4)[OF this] obtain c d where "k = cbox c d" by blast
   3.137        then show ?case
   3.138 @@ -1230,7 +1279,7 @@
   3.139      from bchoice[OF this] obtain q where "\<forall>x\<in>p. insert (cbox a b) (q x) division_of (cbox a b) \<union> x" ..
   3.140      note q = division_ofD[OF this[rule_format]]
   3.141      let ?D = "\<Union>{insert (cbox a b) (q k) | k. k \<in> p}"
   3.142 -    show thesis 
   3.143 +    show thesis
   3.144      proof (rule that[OF division_ofI])
   3.145        have *: "{insert (cbox a b) (q k) |k. k \<in> p} = (\<lambda>k. insert (cbox a b) (q k)) ` p"
   3.146          by auto
   3.147 @@ -1858,7 +1907,7 @@
   3.148      have "?A \<subseteq> ?B"
   3.149      proof
   3.150        case goal1
   3.151 -      then obtain c d 
   3.152 +      then obtain c d
   3.153          where x:  "x = cbox c d"
   3.154                    "\<And>i. i \<in> Basis \<Longrightarrow>
   3.155                          c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
   3.156 @@ -1934,7 +1983,7 @@
   3.157        "x \<in> cbox c d"
   3.158        "\<And>i. i \<in> Basis \<Longrightarrow>
   3.159          c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
   3.160 -        c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i" 
   3.161 +        c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
   3.162        by blast
   3.163      show "x\<in>cbox a b"
   3.164        unfolding mem_box
   3.165 @@ -2160,7 +2209,7 @@
   3.166      done
   3.167    obtain e where e: "e > 0" "ball x e \<subseteq> g x"
   3.168      using gaugeD[OF assms, of x] unfolding open_contains_ball by auto
   3.169 -  from x(2)[OF e(1)] 
   3.170 +  from x(2)[OF e(1)]
   3.171    obtain c d where c_d: "x \<in> cbox c d"
   3.172                          "cbox c d \<subseteq> ball x e"
   3.173                          "cbox c d \<subseteq> cbox a b"
   3.174 @@ -2346,7 +2395,7 @@
   3.175      obtain B where B: "0 < B" "\<And>x. norm (h x) \<le> norm x * B"
   3.176        by blast
   3.177      have "e / B > 0" using goal1(2) B by simp
   3.178 -    then obtain g 
   3.179 +    then obtain g
   3.180        where g: "gauge g"
   3.181                 "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> g fine p \<Longrightarrow>
   3.182                      norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - y) < e / B"
   3.183 @@ -2404,7 +2453,7 @@
   3.184    qed
   3.185  qed
   3.186  
   3.187 -lemma has_integral_scaleR_left: 
   3.188 +lemma has_integral_scaleR_left:
   3.189    "(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x *\<^sub>R c) has_integral (y *\<^sub>R c)) s"
   3.190    using has_integral_linear[OF _ bounded_linear_scaleR_left] by (simp add: comp_def)
   3.191  
   3.192 @@ -2413,6 +2462,11 @@
   3.193    shows "(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x * c) has_integral (y * c)) s"
   3.194    using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def)
   3.195  
   3.196 +corollary integral_mult_left:
   3.197 +  fixes c:: "'a::real_normed_algebra"
   3.198 +  shows "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. f x * c) = integral s f * c"
   3.199 +  by (blast intro:  has_integral_mult_left)
   3.200 +
   3.201  lemma has_integral_cmul: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_integral (c *\<^sub>R k)) s"
   3.202    unfolding o_def[symmetric]
   3.203    by (metis has_integral_linear bounded_linear_scaleR_right)
   3.204 @@ -2478,7 +2532,7 @@
   3.205            unfolding * by (auto simp add: algebra_simps)
   3.206          also have "\<dots> < e/2 + e/2"
   3.207            apply (rule le_less_trans[OF norm_triangle_ineq])
   3.208 -          using as d1 d2 fine 
   3.209 +          using as d1 d2 fine
   3.210            apply (blast intro: add_strict_mono)
   3.211            done
   3.212          finally show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) < e"
   3.213 @@ -2628,7 +2682,7 @@
   3.214    done
   3.215  
   3.216  lemma has_integral_eq:
   3.217 -  assumes "\<forall>x\<in>s. f x = g x"
   3.218 +  assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
   3.219      and "(f has_integral k) s"
   3.220    shows "(g has_integral k) s"
   3.221    using has_integral_sub[OF assms(2), of "\<lambda>x. f x - g x" 0]
   3.222 @@ -2636,16 +2690,23 @@
   3.223    using assms(1)
   3.224    by auto
   3.225  
   3.226 -lemma integrable_eq: "\<forall>x\<in>s. f x = g x \<Longrightarrow> f integrable_on s \<Longrightarrow> g integrable_on s"
   3.227 +lemma integrable_eq: "(\<And>x. x \<in> s \<Longrightarrow> f x = g x) \<Longrightarrow> f integrable_on s \<Longrightarrow> g integrable_on s"
   3.228    unfolding integrable_on_def
   3.229 -  using has_integral_eq[of s f g]
   3.230 +  using has_integral_eq[of s f g] has_integral_eq by blast
   3.231 +
   3.232 +lemma has_integral_cong:
   3.233 +  assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
   3.234 +  shows "(f has_integral i) s = (g has_integral i) s"
   3.235 +  using has_integral_eq[of s f g] has_integral_eq[of s g f] assms
   3.236    by auto
   3.237  
   3.238 -lemma has_integral_eq_eq: "\<forall>x\<in>s. f x = g x \<Longrightarrow> (f has_integral k) s \<longleftrightarrow> (g has_integral k) s"
   3.239 -  using has_integral_eq[of s f g] has_integral_eq[of s g f]
   3.240 -  by auto
   3.241 -
   3.242 -lemma has_integral_null[dest]:
   3.243 +lemma integral_cong:
   3.244 +  assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
   3.245 +  shows "integral s f = integral s g"
   3.246 +  unfolding integral_def
   3.247 +  by (metis assms has_integral_cong)
   3.248 +
   3.249 +lemma has_integral_null [intro]:
   3.250    assumes "content(cbox a b) = 0"
   3.251    shows "(f has_integral 0) (cbox a b)"
   3.252  proof -
   3.253 @@ -2667,7 +2728,7 @@
   3.254      by (auto simp: has_integral)
   3.255  qed
   3.256  
   3.257 -lemma has_integral_null_real[dest]:
   3.258 +lemma has_integral_null_real [intro]:
   3.259    assumes "content {a .. b::real} = 0"
   3.260    shows "(f has_integral 0) {a .. b}"
   3.261    by (metis assms box_real(2) has_integral_null)
   3.262 @@ -2675,14 +2736,11 @@
   3.263  lemma has_integral_null_eq[simp]: "content (cbox a b) = 0 \<Longrightarrow> (f has_integral i) (cbox a b) \<longleftrightarrow> i = 0"
   3.264    by (auto simp add: has_integral_null dest!: integral_unique)
   3.265  
   3.266 -lemma integral_null[dest]: "content (cbox a b) = 0 \<Longrightarrow> integral (cbox a b) f = 0"
   3.267 +lemma integral_null [simp]: "content (cbox a b) = 0 \<Longrightarrow> integral (cbox a b) f = 0"
   3.268    by (metis has_integral_null integral_unique)
   3.269  
   3.270 -lemma integrable_on_null[dest]: "content (cbox a b) = 0 \<Longrightarrow> f integrable_on (cbox a b)"
   3.271 -  unfolding integrable_on_def
   3.272 -  apply (drule has_integral_null)
   3.273 -  apply auto
   3.274 -  done
   3.275 +lemma integrable_on_null [intro]: "content (cbox a b) = 0 \<Longrightarrow> f integrable_on (cbox a b)"
   3.276 +  by (simp add: has_integral_integrable)
   3.277  
   3.278  lemma has_integral_empty[intro]: "(f has_integral 0) {}"
   3.279    by (simp add: has_integral_is_0)
   3.280 @@ -2798,7 +2856,7 @@
   3.281    proof (rule_tac x=y in exI, clarify)
   3.282      fix e :: real
   3.283      assume "e>0"
   3.284 -    then have *:"e/2 > 0" by auto 
   3.285 +    then have *:"e/2 > 0" by auto
   3.286      then guess N1 unfolding real_arch_inv[of "e/2"] .. note N1=this
   3.287      then have N1': "N1 = N1 - 1 + 1"
   3.288        by auto
   3.289 @@ -2818,7 +2876,7 @@
   3.290          apply (rule norm_triangle_half_r)
   3.291          apply (rule less_trans[OF _ *])
   3.292          apply (subst N1', rule d(2)[of "p (N1+N2)"])
   3.293 -        using N1' as(1) as(2) dp 
   3.294 +        using N1' as(1) as(2) dp
   3.295          apply (simp add: `\<forall>x. p x tagged_division_of cbox a b \<and> (\<lambda>xa. \<Inter>{d i xa |i. i \<in> {0..x}}) fine p x`)
   3.296          using N2 le_add2 by blast
   3.297      }
   3.298 @@ -2992,9 +3050,9 @@
   3.299      assume "k \<in> ?p1"
   3.300      then guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this
   3.301      guess u v using p(4)[OF l(2)] by (elim exE) note uv=this
   3.302 -    show "k \<subseteq> ?I1" 
   3.303 +    show "k \<subseteq> ?I1"
   3.304        using l p(2) uv by force
   3.305 -    show  "k \<noteq> {}" 
   3.306 +    show  "k \<noteq> {}"
   3.307        by (simp add: l)
   3.308      show  "\<exists>a b. k = cbox a b"
   3.309        apply (simp add: l uv p(2-3)[OF l(2)])
   3.310 @@ -3013,9 +3071,9 @@
   3.311      assume "k \<in> ?p2"
   3.312      then guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this
   3.313      guess u v using p(4)[OF l(2)] by (elim exE) note uv=this
   3.314 -    show "k \<subseteq> ?I2" 
   3.315 +    show "k \<subseteq> ?I2"
   3.316        using l p(2) uv by force
   3.317 -    show  "k \<noteq> {}" 
   3.318 +    show  "k \<noteq> {}"
   3.319        by (simp add: l)
   3.320      show  "\<exists>a b. k = cbox a b"
   3.321        apply (simp add: l uv p(2-3)[OF l(2)])
   3.322 @@ -3041,17 +3099,17 @@
   3.323    case goal1
   3.324    then have e: "e/2 > 0"
   3.325      by auto
   3.326 -    obtain d1 
   3.327 +    obtain d1
   3.328      where d1: "gauge d1"
   3.329 -      and d1norm: 
   3.330 +      and d1norm:
   3.331          "\<And>p. \<lbrakk>p tagged_division_of cbox a b \<inter> {x. x \<bullet> k \<le> c};
   3.332                 d1 fine p\<rbrakk> \<Longrightarrow> norm ((\<Sum>(x, k) \<in> p. content k *\<^sub>R f x) - i) < e / 2"
   3.333         apply (rule has_integralD[OF fi[unfolded interval_split[OF k]] e])
   3.334         apply (simp add: interval_split[symmetric] k)
   3.335         done
   3.336 -    obtain d2 
   3.337 +    obtain d2
   3.338      where d2: "gauge d2"
   3.339 -      and d2norm: 
   3.340 +      and d2norm:
   3.341          "\<And>p. \<lbrakk>p tagged_division_of cbox a b \<inter> {x. c \<le> x \<bullet> k};
   3.342                 d2 fine p\<rbrakk> \<Longrightarrow> norm ((\<Sum>(x, k) \<in> p. content k *\<^sub>R f x) - j) < e / 2"
   3.343         apply (rule has_integralD[OF fj[unfolded interval_split[OF k]] e])
   3.344 @@ -3077,12 +3135,12 @@
   3.345            using p(2)[unfolded fine_def, rule_format,OF as] by auto
   3.346          with kk obtain y where y: "y \<in> ball x \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<le> c"
   3.347            by blast
   3.348 -        then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>" 
   3.349 +        then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>"
   3.350            using Basis_le_norm[OF k, of "x - y"]
   3.351            by (auto simp add: dist_norm inner_diff_left intro: le_less_trans)
   3.352          with y show False
   3.353            using ** by (auto simp add: field_simps)
   3.354 -      qed 
   3.355 +      qed
   3.356      qed
   3.357      have xk_ge_c: "\<And>x kk. (x, kk) \<in> p \<Longrightarrow> kk \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {} \<Longrightarrow> x\<bullet>k \<ge> c"
   3.358      proof -
   3.359 @@ -3095,7 +3153,7 @@
   3.360            using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto
   3.361          with kk obtain y where y: "y \<in> ball x \<bar>x \<bullet> k - c\<bar>" "y\<bullet>k \<ge> c"
   3.362            by blast
   3.363 -        then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>" 
   3.364 +        then have "\<bar>x \<bullet> k - y \<bullet> k\<bar> < \<bar>x \<bullet> k - c\<bar>"
   3.365            using Basis_le_norm[OF k, of "x - y"]
   3.366            by (auto simp add: dist_norm inner_diff_left intro: le_less_trans)
   3.367          with y show False
   3.368 @@ -3104,7 +3162,7 @@
   3.369      qed
   3.370  
   3.371      have lem1: "\<And>f P Q. (\<forall>x k. (x, k) \<in> {(x, f k) | x k. P x k} \<longrightarrow> Q x k) \<longleftrightarrow>
   3.372 -                         (\<forall>x k. P x k \<longrightarrow> Q x (f k))" 
   3.373 +                         (\<forall>x k. P x k \<longrightarrow> Q x (f k))"
   3.374        by auto
   3.375      have fin_finite: "\<And>f s P f. finite s \<Longrightarrow> finite {(x,f k) | x k. (x,k) \<in> s \<and> P x k}"
   3.376      proof -
   3.377 @@ -3342,7 +3400,7 @@
   3.378      also have "\<dots> < e"
   3.379        by (rule k d(2) p12 fine_union p1 p2)+
   3.380      finally have "norm ((\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - i) < e" .
   3.381 -   } 
   3.382 +   }
   3.383    then show ?thesis
   3.384      by (auto intro: that[of d] d elim: )
   3.385  qed
   3.386 @@ -3602,7 +3660,7 @@
   3.387    fix a b :: 'a
   3.388    assume "content (cbox a b) = 0"
   3.389    then show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) = Some 0"
   3.390 -    using has_integral_null_eq 
   3.391 +    using has_integral_null_eq
   3.392      by (auto simp: integrable_on_null)
   3.393  qed
   3.394  
   3.395 @@ -3723,7 +3781,7 @@
   3.396    guess u v using division_ofD(4)[OF assms(1,5)] by (elim exE) note l=this
   3.397    have uv: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" "\<forall>i\<in>Basis. a\<bullet>i \<le> u\<bullet>i \<and> v\<bullet>i \<le> b\<bullet>i"
   3.398      using division_ofD(2,2,3)[OF assms(1,5)] unfolding l box_ne_empty
   3.399 -    using subset_box(1)    
   3.400 +    using subset_box(1)
   3.401      apply auto
   3.402      apply blast+
   3.403      done
   3.404 @@ -3836,7 +3894,7 @@
   3.405  qed
   3.406  
   3.407  lemma iterate_op:
   3.408 -   "\<lbrakk>monoidal opp; finite s\<rbrakk> 
   3.409 +   "\<lbrakk>monoidal opp; finite s\<rbrakk>
   3.410      \<Longrightarrow> iterate opp s (\<lambda>x. opp (f x) (g x)) = opp (iterate opp s f) (iterate opp s g)"
   3.411  by (erule finite_induct) (auto simp: monoidal_ac(4) monoidal_ac(5))
   3.412  
   3.413 @@ -3857,13 +3915,13 @@
   3.414      def su \<equiv> "support opp f s"
   3.415      have fsu: "finite su"
   3.416        using True by (simp add: su_def)
   3.417 -    moreover    
   3.418 +    moreover
   3.419      { assume "finite su" "su \<subseteq> s"
   3.420        then have "iterate opp su f = iterate opp su g"
   3.421          by (induct su) (auto simp: assms)
   3.422      }
   3.423      ultimately have "iterate opp (support opp f s) f = iterate opp (support opp g s) g"
   3.424 -      by (simp add: "*" su_def support_subset)    
   3.425 +      by (simp add: "*" su_def support_subset)
   3.426      then show ?thesis
   3.427        by simp
   3.428    qed
   3.429 @@ -3884,17 +3942,17 @@
   3.430    def C \<equiv> "card (division_points (cbox a b) d)"
   3.431    then show ?thesis
   3.432      using assms
   3.433 -  proof (induct C arbitrary: a b d rule: full_nat_induct) 
   3.434 +  proof (induct C arbitrary: a b d rule: full_nat_induct)
   3.435      case (1 a b d)
   3.436      show ?case
   3.437      proof (cases "content (cbox a b) = 0")
   3.438        case True
   3.439        show "iterate opp d f = f (cbox a b)"
   3.440          unfolding operativeD(1)[OF assms(2) True]
   3.441 -      proof (rule iterate_eq_neutral[OF `monoidal opp`]) 
   3.442 +      proof (rule iterate_eq_neutral[OF `monoidal opp`])
   3.443          fix x
   3.444          assume x: "x \<in> d"
   3.445 -        then show "f x = neutral opp" 
   3.446 +        then show "f x = neutral opp"
   3.447            by (metis division_ofD(4) 1(4) division_of_content_0[OF True] operativeD(1)[OF assms(2)] x)
   3.448        qed
   3.449      next
   3.450 @@ -3927,7 +3985,7 @@
   3.451          then have d': "\<forall>i\<in>d. \<exists>u v. i = cbox u v \<and>
   3.452            (\<forall>j\<in>Basis. u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = a\<bullet>j \<or> u\<bullet>j = b\<bullet>j \<and> v\<bullet>j = b\<bullet>j \<or> u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = b\<bullet>j)"
   3.453            unfolding forall_in_division[OF 1(4)]
   3.454 -          by blast 
   3.455 +          by blast
   3.456          have "(1/2) *\<^sub>R (a+b) \<in> cbox a b"
   3.457            unfolding mem_box using ab by(auto intro!: less_imp_le simp: inner_simps)
   3.458          note this[unfolded division_ofD(6)[OF `d division_of cbox a b`,symmetric] Union_iff]
   3.459 @@ -4004,7 +4062,7 @@
   3.460              unfolding leq interval_split[OF kc(4)]
   3.461              apply (rule operativeD(1) 1)+
   3.462              unfolding interval_split[symmetric,OF kc(4)]
   3.463 -            using division_split_left_inj 1 as kc leq by blast 
   3.464 +            using division_split_left_inj 1 as kc leq by blast
   3.465          } note fxk_le = this
   3.466          { fix l y
   3.467            assume as: "l \<in> d" "y \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} = y \<inter> {x. c \<le> x \<bullet> k}" "l \<noteq> y"
   3.468 @@ -4061,14 +4119,14 @@
   3.469  proof -
   3.470    have *: "(\<lambda>(x,l). f l) = f \<circ> snd"
   3.471      unfolding o_def by rule auto note tagged = tagged_division_ofD[OF assms(3)]
   3.472 -  { fix a b a' 
   3.473 -    assume as: "(a, b) \<in> d" "(a', b) \<in> d" "(a, b) \<noteq> (a', b)" 
   3.474 +  { fix a b a'
   3.475 +    assume as: "(a, b) \<in> d" "(a', b) \<in> d" "(a, b) \<noteq> (a', b)"
   3.476      have "f b = neutral opp"
   3.477 -      using tagged(4)[OF as(1)] 
   3.478 +      using tagged(4)[OF as(1)]
   3.479        apply clarify
   3.480        apply (rule operativeD(1)[OF assms(2)])
   3.481        by (metis content_eq_0_interior inf.idem tagged_division_ofD(5)[OF assms(3) as(1-3)])
   3.482 -  } 
   3.483 +  }
   3.484    then have "iterate opp d (\<lambda>(x,l). f l) = iterate opp (snd ` d) f"
   3.485      unfolding *
   3.486      by (force intro!: assms iterate_image_nonzero[symmetric, OF _ tagged_division_of_finite])
   3.487 @@ -4184,7 +4242,7 @@
   3.488      apply (rule mult_left_mono[OF _ abs_ge_zero, of _ e])
   3.489      apply (metis norm)
   3.490      unfolding setsum_left_distrib[symmetric]
   3.491 -    using con setsum_le 
   3.492 +    using con setsum_le
   3.493      apply (auto simp: mult.commute intro: mult_left_mono [OF _ e])
   3.494      done
   3.495    finally show ?thesis .
   3.496 @@ -4219,13 +4277,21 @@
   3.497      using d(2)[OF conjI[OF p]] *[OF rsum_bound[OF p(1) assms(3)]] by auto
   3.498  qed
   3.499  
   3.500 -lemma has_integral_bound_real:
   3.501 +corollary has_integral_bound_real:
   3.502    fixes f :: "real \<Rightarrow> 'b::real_normed_vector"
   3.503    assumes "0 \<le> B"
   3.504        and "(f has_integral i) {a .. b}"
   3.505        and "\<forall>x\<in>{a .. b}. norm (f x) \<le> B"
   3.506      shows "norm i \<le> B * content {a .. b}"
   3.507 -  by (metis assms(1) assms(2) assms(3) box_real(2) has_integral_bound)
   3.508 +  by (metis assms box_real(2) has_integral_bound)
   3.509 +
   3.510 +corollary integrable_bound:
   3.511 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   3.512 +  assumes "0 \<le> B"
   3.513 +      and "f integrable_on (cbox a b)"
   3.514 +      and "\<And>x. x\<in>cbox a b \<Longrightarrow> norm (f x) \<le> B"
   3.515 +    shows "norm (integral (cbox a b) f) \<le> B * content (cbox a b)"
   3.516 +by (metis integrable_integral has_integral_bound assms)
   3.517  
   3.518  
   3.519  subsection \<open>Similar theorems about relationship among components.\<close>
   3.520 @@ -4244,7 +4310,7 @@
   3.521    show "(content b *\<^sub>R f a) \<bullet> i \<le> (content b *\<^sub>R g a) \<bullet> i"
   3.522      unfolding b inner_simps real_scaleR_def
   3.523      apply (rule mult_left_mono)
   3.524 -    using assms(2) tagged 
   3.525 +    using assms(2) tagged
   3.526      by (auto simp add: content_pos_le)
   3.527  qed
   3.528  
   3.529 @@ -4263,9 +4329,9 @@
   3.530        by auto
   3.531      guess d1 using goal1(1)[unfolded has_integral,rule_format,OF *] by (elim exE conjE) note d1=this[rule_format]
   3.532      guess d2 using goal1(2)[unfolded has_integral,rule_format,OF *] by (elim exE conjE) note d2=this[rule_format]
   3.533 -    obtain p where p: "p tagged_division_of cbox a b" "d1 fine p" "d2 fine p"   
   3.534 -       using fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] unfolding fine_inter 
   3.535 -       by metis    
   3.536 +    obtain p where p: "p tagged_division_of cbox a b" "d1 fine p" "d2 fine p"
   3.537 +       using fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] unfolding fine_inter
   3.538 +       by metis
   3.539      note le_less_trans[OF Basis_le_norm[OF k]]
   3.540      then have "\<bar>((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - i) \<bullet> k\<bar> < (i \<bullet> k - j \<bullet> k) / 3"
   3.541                "\<bar>((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - j) \<bullet> k\<bar> < (i \<bullet> k - j \<bullet> k) / 3"
   3.542 @@ -4423,7 +4489,7 @@
   3.543    have *: "\<And>P. \<forall>e>(0::real). P e \<Longrightarrow> \<forall>n::nat. P (inverse (real n + 1))"
   3.544      by auto
   3.545    from choice[OF *[OF assms]] guess g .. note g=conjunctD2[OF this[rule_format],rule_format]
   3.546 -  from choice[OF allI[OF g(2)[unfolded integrable_on_def], of "\<lambda>x. x"]] 
   3.547 +  from choice[OF allI[OF g(2)[unfolded integrable_on_def], of "\<lambda>x. x"]]
   3.548    obtain i where i: "\<And>x. (g x has_integral i x) (cbox a b)"
   3.549        by auto
   3.550    have "Cauchy i"
   3.551 @@ -4444,7 +4510,7 @@
   3.552        note * = i[unfolded has_integral,rule_format,OF this]
   3.553        from *[of m] guess gm by (elim conjE exE) note gm=this[rule_format]
   3.554        from *[of n] guess gn by (elim conjE exE) note gn=this[rule_format]
   3.555 -      from fine_division_exists[OF gauge_inter[OF gm(1) gn(1)], of a b] 
   3.556 +      from fine_division_exists[OF gauge_inter[OF gm(1) gn(1)], of a b]
   3.557        obtain p where p: "p tagged_division_of cbox a b" "(\<lambda>x. gm x \<inter> gn x) fine p"
   3.558          by auto
   3.559        { fix s1 s2 i1 and i2::'b
   3.560 @@ -4485,7 +4551,7 @@
   3.561          by (auto intro!: triangle3)
   3.562      qed
   3.563    qed
   3.564 -  then obtain s where s: "i ----> s" 
   3.565 +  then obtain s where s: "i ----> s"
   3.566      using convergent_eq_cauchy[symmetric] by blast
   3.567    show ?thesis
   3.568      unfolding integrable_on_def has_integral
   3.569 @@ -4512,7 +4578,7 @@
   3.570          unfolding norm_minus_commute
   3.571          by (auto simp add: algebra_simps)
   3.572        finally have "norm (sf - s) < e" .
   3.573 -    } note lem = this 
   3.574 +    } note lem = this
   3.575      { fix p
   3.576        assume p: "p tagged_division_of (cbox a b) \<and> g' fine p"
   3.577        then have norm_less: "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g (N1 + N2) x) - i (N1 + N2)) < e / 3"
   3.578 @@ -4554,7 +4620,7 @@
   3.579      and "\<forall>x\<in>s. \<forall>y\<in>s. f x = f y \<and> x \<noteq> y \<longrightarrow> g (f x) = 0"
   3.580    shows "setsum g {f x |x. x \<in> s \<and> f x \<noteq> a} = setsum (g o f) s"
   3.581    apply (subst setsum_iterate)
   3.582 -  using assms monoidal_monoid 
   3.583 +  using assms monoidal_monoid
   3.584    unfolding setsum_iterate[OF assms(1)]
   3.585    apply (auto intro!: iterate_nonzero_image_lemma)
   3.586    done
   3.587 @@ -4648,14 +4714,14 @@
   3.588          using assms by simp
   3.589      next
   3.590        case False
   3.591 -      then have 
   3.592 +      then have
   3.593            "(\<Prod>i\<in>Basis - {k}. interval_upperbound (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i -
   3.594 -                interval_lowerbound (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i) 
   3.595 +                interval_lowerbound (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i)
   3.596             = (\<Prod>i\<in>Basis - {k}. b\<bullet>i - a\<bullet>i)"
   3.597          by (simp add: box_eq_empty interval_doublesplit[OF k])
   3.598        then show "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
   3.599          unfolding content_def
   3.600 -        using assms False 
   3.601 +        using assms False
   3.602          apply (subst *)
   3.603          apply (subst setprod.insert)
   3.604          apply (simp_all add: interval_doublesplit[OF k] box_eq_empty not_less less_e)
   3.605 @@ -4997,7 +5063,6 @@
   3.606    let ?f = "(\<lambda>x. if x \<in> t then f x else 0)"
   3.607    show ?thesis
   3.608      apply (rule_tac f="?f" in has_integral_eq)
   3.609 -    apply rule
   3.610      unfolding if_P
   3.611      apply (rule refl)
   3.612      apply (subst has_integral_alt)
   3.613 @@ -5095,7 +5160,7 @@
   3.614            apply (erule_tac x=x in ballE)
   3.615            apply (erule exE)
   3.616            apply (rule_tac x="(xa,x)" in bexI)
   3.617 -          apply auto  
   3.618 +          apply auto
   3.619            done
   3.620        qed
   3.621        have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) \<le> setsum (\<lambda>i. (real i + 1) *
   3.622 @@ -8197,10 +8262,7 @@
   3.623    proof -
   3.624      assume ?l
   3.625      then have "?g integrable_on cbox c d"
   3.626 -      apply -
   3.627 -      apply (rule integrable_subinterval[OF _ assms])
   3.628 -      apply auto
   3.629 -      done
   3.630 +      using assms has_integral_integrable integrable_subinterval by blast
   3.631      then have *: "f integrable_on cbox c d"
   3.632        apply -
   3.633        apply (rule integrable_eq)
   3.634 @@ -10503,7 +10565,7 @@
   3.635  
   3.636  lemma bounded_variation_absolutely_integrable_interval:
   3.637    fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   3.638 -  assumes "f integrable_on cbox a b"
   3.639 +  assumes f: "f integrable_on cbox a b"
   3.640      and *: "\<forall>d. d division_of (cbox a b) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
   3.641    shows "f absolutely_integrable_on cbox a b"
   3.642  proof -
   3.643 @@ -10515,9 +10577,7 @@
   3.644    note D = D_1 D_2
   3.645    let ?S = "SUP x:?D. ?f x"
   3.646    show ?thesis
   3.647 -    apply rule
   3.648 -    apply (rule assms)
   3.649 -    apply rule
   3.650 +    apply (rule absolutely_integrable_onI [OF f has_integral_integrable])
   3.651      apply (subst has_integral[of _ ?S])
   3.652    proof safe
   3.653      case goal1
   3.654 @@ -10533,17 +10593,11 @@
   3.655          apply (rule separate_point_closed)
   3.656          apply (rule closed_Union)
   3.657          apply (rule finite_subset[OF _ d'(1)])
   3.658 -        apply safe
   3.659 -        apply (drule d'(4))
   3.660 +        using d'(4)
   3.661          apply auto
   3.662          done
   3.663        then show ?case
   3.664 -        apply safe
   3.665 -        apply (rule_tac x=da in exI)
   3.666 -        apply safe
   3.667 -        apply (erule_tac x=xa in ballE)
   3.668 -        apply auto
   3.669 -        done
   3.670 +        by force
   3.671      qed
   3.672      from choice[OF this] guess k .. note k=conjunctD2[OF this[rule_format],rule_format]
   3.673  
   3.674 @@ -10556,9 +10610,8 @@
   3.675        apply safe
   3.676      proof -
   3.677        show "gauge ?g"
   3.678 -        using g(1)
   3.679 +        using g(1) k(1)
   3.680          unfolding gauge_def
   3.681 -        using k(1)
   3.682          by auto
   3.683        fix p
   3.684        assume "p tagged_division_of (cbox a b)" and "?g fine p"
   3.685 @@ -10641,13 +10694,6 @@
   3.686            then show "y \<in> \<Union>{k. \<exists>x. (x, k) \<in> p'}"
   3.687              unfolding p'_def Union_iff
   3.688              apply (rule_tac x="i \<inter> l" in bexI)
   3.689 -            defer
   3.690 -            unfolding mem_Collect_eq
   3.691 -            apply (rule_tac x=x in exI)+
   3.692 -            apply (rule_tac x="i\<inter>l" in exI)
   3.693 -            apply safe
   3.694 -            apply (rule_tac x=i in exI)
   3.695 -            apply (rule_tac x=l in exI)
   3.696              using i xl
   3.697              apply auto
   3.698              done
   3.699 @@ -10663,10 +10709,8 @@
   3.700          done
   3.701        then have **: "\<bar>(\<Sum>(x,k)\<in>p'. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p'. norm (integral k f))\<bar> < e / 2"
   3.702          unfolding split_def
   3.703 -        apply (rule helplemma)
   3.704          using p''
   3.705 -        apply auto
   3.706 -        done
   3.707 +        by (force intro!: helplemma)
   3.708  
   3.709        have p'alt: "p' = {(x,(i \<inter> l)) | x i l. (x,l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}}"
   3.710        proof safe
   3.711 @@ -10676,6 +10720,7 @@
   3.712            by auto
   3.713          then have "(x, i \<inter> l) \<in> p'"
   3.714            unfolding p'_def
   3.715 +          using goal2
   3.716            apply safe
   3.717            apply (rule_tac x=x in exI)
   3.718            apply (rule_tac x="i \<inter> l" in exI)
   3.719 @@ -11289,13 +11334,7 @@
   3.720      and "\<And>a. a \<in> t \<Longrightarrow> (f a) absolutely_integrable_on s"
   3.721    shows "(\<lambda>x. setsum (\<lambda>a. f a x) t) absolutely_integrable_on s"
   3.722    using assms(1,2)
   3.723 -  apply induct
   3.724 -  defer
   3.725 -  apply (subst setsum.insert)
   3.726 -  apply assumption+
   3.727 -  apply rule
   3.728 -  apply auto
   3.729 -  done
   3.730 +  by induct auto
   3.731  
   3.732  lemma bounded_linear_setsum:
   3.733    fixes f :: "'i \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   3.734 @@ -11460,7 +11499,7 @@
   3.735    shows "f absolutely_integrable_on s"
   3.736    unfolding absolutely_integrable_abs_eq
   3.737    apply rule
   3.738 -  apply (rule assms)
   3.739 +  apply (rule assms)thm integrable_eq
   3.740    apply (rule integrable_eq[of _ f])
   3.741    using assms
   3.742    apply (auto simp: euclidean_eq_iff[where 'a='m])
   3.743 @@ -11524,18 +11563,6 @@
   3.744    qed
   3.745  qed
   3.746  
   3.747 -lemma absolutely_integrable_integrable_bound_real:
   3.748 -  fixes f :: "'n::euclidean_space \<Rightarrow> real"
   3.749 -  assumes "\<forall>x\<in>s. norm (f x) \<le> g x"
   3.750 -    and "f integrable_on s"
   3.751 -    and "g integrable_on s"
   3.752 -  shows "f absolutely_integrable_on s"
   3.753 -  apply (rule absolutely_integrable_integrable_bound[where g=g])
   3.754 -  using assms
   3.755 -  unfolding o_def
   3.756 -  apply auto
   3.757 -  done
   3.758 -
   3.759  lemma absolutely_integrable_absolutely_integrable_bound:
   3.760    fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   3.761      and g :: "'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
   3.762 @@ -11670,7 +11697,7 @@
   3.763          apply (rule cInf_abs_ge)
   3.764          prefer 5
   3.765          apply rule
   3.766 -        apply (rule_tac g = h in absolutely_integrable_integrable_bound_real)
   3.767 +        apply (rule_tac g = h in absolutely_integrable_integrable_bound)
   3.768          using assms
   3.769          unfolding real_norm_def
   3.770          apply auto
   3.771 @@ -11682,7 +11709,7 @@
   3.772        apply (rule absolutely_integrable_onD)
   3.773        apply (rule absolutely_integrable_inf_real)
   3.774        prefer 3
   3.775 -      using absolutely_integrable_integrable_bound_real[OF assms(3,1,2)]
   3.776 +      using absolutely_integrable_integrable_bound[OF assms(3,1,2)]
   3.777        apply auto
   3.778        done
   3.779      fix x
   3.780 @@ -11739,7 +11766,7 @@
   3.781          apply (rule cSup_abs_le)
   3.782          prefer 5
   3.783          apply rule
   3.784 -        apply (rule_tac g=h in absolutely_integrable_integrable_bound_real)
   3.785 +        apply (rule_tac g=h in absolutely_integrable_integrable_bound)
   3.786          using assms
   3.787          unfolding real_norm_def
   3.788          apply auto
   3.789 @@ -11751,7 +11778,7 @@
   3.790        apply (rule absolutely_integrable_onD)
   3.791        apply (rule absolutely_integrable_sup_real)
   3.792        prefer 3
   3.793 -      using absolutely_integrable_integrable_bound_real[OF assms(3,1,2)]
   3.794 +      using absolutely_integrable_integrable_bound[OF assms(3,1,2)]
   3.795        apply auto
   3.796        done
   3.797      fix x
   3.798 @@ -11926,4 +11953,351 @@
   3.799      by simp
   3.800  qed
   3.801  
   3.802 +subsection{*Compute a double integral using iterated integrals and switching the order of integration*}
   3.803 +
   3.804 +lemma setcomp_dot1: "{z. P (z \<bullet> (i,0))} = {(x,y). P(x \<bullet> i)}"
   3.805 +  by auto
   3.806 +
   3.807 +lemma setcomp_dot2: "{z. P (z \<bullet> (0,i))} = {(x,y). P(y \<bullet> i)}"
   3.808 +  by auto
   3.809 +
   3.810 +lemma Sigma_Int_Paircomp1: "(Sigma A B) \<inter> {(x, y). P x} = Sigma (A \<inter> {x. P x}) B"
   3.811 +  by blast
   3.812 +
   3.813 +lemma Sigma_Int_Paircomp2: "(Sigma A B) \<inter> {(x, y). P y} = Sigma A (\<lambda>z. B z \<inter> {y. P y})"
   3.814 +  by blast
   3.815 +
   3.816 +lemma continuous_on_imp_integrable_on_Pair1:
   3.817 +  fixes f :: "_ \<Rightarrow> 'b::banach"
   3.818 +  assumes con: "continuous_on (cbox (a,c) (b,d)) f" and x: "x \<in> cbox a b"
   3.819 +  shows "(\<lambda>y. f (x, y)) integrable_on (cbox c d)"
   3.820 +proof -
   3.821 +  have "f o (\<lambda>y. (x, y)) integrable_on (cbox c d)"
   3.822 +    apply (rule integrable_continuous)
   3.823 +    apply (rule continuous_on_compose [OF _ continuous_on_subset [OF con]])
   3.824 +    using x
   3.825 +    apply (auto intro: continuous_on_Pair continuous_on_const continuous_on_id continuous_on_subset con)
   3.826 +    done
   3.827 +  then show ?thesis
   3.828 +    by (simp add: o_def)
   3.829 +qed
   3.830 +
   3.831 +lemma integral_integrable_2dim:
   3.832 +  fixes f :: "('a::euclidean_space * 'b::euclidean_space) \<Rightarrow> 'c::banach"
   3.833 +  assumes "continuous_on (cbox (a,c) (b,d)) f"
   3.834 +    shows "(\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y))) integrable_on cbox a b"
   3.835 +proof (cases "content(cbox c d) = 0")
   3.836 +case True
   3.837 +  then show ?thesis
   3.838 +    by (simp add: True integrable_const)
   3.839 +next
   3.840 +  case False
   3.841 +  have uc: "uniformly_continuous_on (cbox (a,c) (b,d)) f"
   3.842 +    by (simp add: assms compact_cbox compact_uniformly_continuous)
   3.843 +  { fix x::'a and e::real
   3.844 +    assume x: "x \<in> cbox a b" and e: "0 < e"
   3.845 +    then have e2_gt: "0 < e / 2 / content (cbox c d)" and e2_less: "e / 2 / content (cbox c d) * content (cbox c d) < e"
   3.846 +      by (auto simp: False content_lt_nz e)
   3.847 +    then obtain dd
   3.848 +    where dd: "\<And>x x'. \<lbrakk>x\<in>cbox (a, c) (b, d); x'\<in>cbox (a, c) (b, d); norm (x' - x) < dd\<rbrakk>
   3.849 +                       \<Longrightarrow> norm (f x' - f x) \<le> e / (2 * content (cbox c d))"  "dd>0"
   3.850 +      using uc [unfolded uniformly_continuous_on_def, THEN spec, of "e / (2 * content (cbox c d))"]
   3.851 +      by (auto simp: dist_norm intro: less_imp_le)
   3.852 +    have "\<exists>delta>0. \<forall>x'\<in>cbox a b. norm (x' - x) < delta \<longrightarrow> norm (integral (cbox c d) (\<lambda>u. f (x', u) - f (x, u))) < e"
   3.853 +      apply (rule_tac x=dd in exI)
   3.854 +      using dd e2_gt assms x
   3.855 +      apply clarify
   3.856 +      apply (rule le_less_trans [OF _ e2_less])
   3.857 +      apply (rule integrable_bound)
   3.858 +      apply (auto intro: integrable_sub continuous_on_imp_integrable_on_Pair1)
   3.859 +      done
   3.860 +  } note * = this
   3.861 +  show ?thesis
   3.862 +    apply (rule integrable_continuous)
   3.863 +    apply (simp add: * continuous_on_iff dist_norm integral_sub [symmetric] continuous_on_imp_integrable_on_Pair1 [OF assms])
   3.864 +    done
   3.865 +qed
   3.866 +
   3.867 +lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
   3.868 +            \<Longrightarrow> norm(y - x) \<le> e"
   3.869 +using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"]
   3.870 +  by (simp add: add_diff_add)
   3.871 +
   3.872 +lemma integral_split:
   3.873 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{real_normed_vector,complete_space}"
   3.874 +  assumes f: "f integrable_on (cbox a b)"
   3.875 +      and k: "k \<in> Basis"
   3.876 +  shows "integral (cbox a b) f =
   3.877 +           integral (cbox a b \<inter> {x. x\<bullet>k \<le> c}) f +
   3.878 +           integral (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) f"
   3.879 +  apply (rule integral_unique [OF has_integral_split [where c=c]])
   3.880 +  using k f
   3.881 +  apply (auto simp: has_integral_integral [symmetric])
   3.882 +  done
   3.883 +
   3.884 +lemma integral_swap_operative:
   3.885 +  fixes f :: "('a::euclidean_space * 'b::euclidean_space) \<Rightarrow> 'c::banach"
   3.886 +  assumes f: "continuous_on s f" and e: "0 < e"
   3.887 +    shows "operative(op \<and>)
   3.888 +           (\<lambda>k. \<forall>a b c d.
   3.889 +                cbox (a,c) (b,d) \<subseteq> k \<and> cbox (a,c) (b,d) \<subseteq> s
   3.890 +                \<longrightarrow> norm(integral (cbox (a,c) (b,d)) f -
   3.891 +                         integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f((x,y)))))
   3.892 +                    \<le> e * content (cbox (a,c) (b,d)))"
   3.893 +proof (auto simp: operative_def)
   3.894 +  fix a::'a and c::'b and b::'a and d::'b and u::'a and v::'a and w::'b and z::'b
   3.895 +  assume c0: "content (cbox (a, c) (b, d)) = 0"
   3.896 +     and cb1: "cbox (u, w) (v, z) \<subseteq> cbox (a, c) (b, d)"
   3.897 +     and cb2: "cbox (u, w) (v, z) \<subseteq> s"
   3.898 +  have c0': "content (cbox (u, w) (v, z)) = 0"
   3.899 +    by (fact content_0_subset [OF c0 cb1])
   3.900 +  show "norm (integral (cbox (u,w) (v,z)) f - integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))))
   3.901 +          \<le> e * content (cbox (u,w) (v,z))"
   3.902 +    using content_cbox_pair_eq0_D [OF c0']
   3.903 +    by (force simp add: c0')
   3.904 +next
   3.905 +  fix a::'a and c::'b and b::'a and d::'b
   3.906 +  and M::real and i::'a and j::'b
   3.907 +  and u::'a and v::'a and w::'b and z::'b
   3.908 +  assume ij: "(i,j) \<in> Basis"
   3.909 +     and n1: "\<forall>a' b' c' d'.
   3.910 +                cbox (a',c') (b',d') \<subseteq> cbox (a,c) (b,d) \<and>
   3.911 +                cbox (a',c') (b',d') \<subseteq> {x. x \<bullet> (i,j) \<le> M} \<and> cbox (a',c') (b',d') \<subseteq> s \<longrightarrow>
   3.912 +                norm (integral (cbox (a',c') (b',d')) f - integral (cbox a' b') (\<lambda>x. integral (cbox c' d') (\<lambda>y. f (x,y))))
   3.913 +                \<le> e * content (cbox (a',c') (b',d'))"
   3.914 +     and n2: "\<forall>a' b' c' d'.
   3.915 +                cbox (a',c') (b',d') \<subseteq> cbox (a,c) (b,d) \<and>
   3.916 +                cbox (a',c') (b',d') \<subseteq> {x. M \<le> x \<bullet> (i,j)} \<and> cbox (a',c') (b',d') \<subseteq> s \<longrightarrow>
   3.917 +                norm (integral (cbox (a',c') (b',d')) f - integral (cbox a' b') (\<lambda>x. integral (cbox c' d') (\<lambda>y. f (x,y))))
   3.918 +                \<le> e * content (cbox (a',c') (b',d'))"
   3.919 +     and subs: "cbox (u,w) (v,z) \<subseteq> cbox (a,c) (b,d)"  "cbox (u,w) (v,z) \<subseteq> s"
   3.920 +  have fcont: "continuous_on (cbox (u, w) (v, z)) f"
   3.921 +    using assms(1) continuous_on_subset  subs(2) by blast
   3.922 +  then have fint: "f integrable_on cbox (u, w) (v, z)"
   3.923 +    by (metis integrable_continuous)
   3.924 +  consider "i \<in> Basis" "j=0" | "j \<in> Basis" "i=0"  using ij
   3.925 +    by (auto simp: Euclidean_Space.Basis_prod_def)
   3.926 +  then show "norm (integral (cbox (u,w) (v,z)) f - integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))))
   3.927 +             \<le> e * content (cbox (u,w) (v,z))" (is ?normle)
   3.928 +  proof cases
   3.929 +    case 1
   3.930 +    then have e: "e * content (cbox (u, w) (v, z)) =
   3.931 +                  e * (content (cbox u v \<inter> {x. x \<bullet> i \<le> M}) * content (cbox w z)) +
   3.932 +                  e * (content (cbox u v \<inter> {x. M \<le> x \<bullet> i}) * content (cbox w z))"
   3.933 +      by (simp add: content_split [where c=M] content_Pair algebra_simps)
   3.934 +    have *: "integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))) =
   3.935 +                integral (cbox u v \<inter> {x. x \<bullet> i \<le> M}) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))) +
   3.936 +                integral (cbox u v \<inter> {x. M \<le> x \<bullet> i}) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y)))"
   3.937 +      using 1 f subs integral_integrable_2dim continuous_on_subset
   3.938 +      by (blast intro: integral_split)
   3.939 +    show ?normle
   3.940 +      apply (rule norm_diff2 [OF integral_split [where c=M, OF fint ij] * e])
   3.941 +      using 1 subs
   3.942 +      apply (simp_all add: cbox_Pair_eq setcomp_dot1 [of "\<lambda>u. M\<le>u"] setcomp_dot1 [of "\<lambda>u. u\<le>M"] Sigma_Int_Paircomp1)
   3.943 +      apply (simp_all add: interval_split ij)
   3.944 +      apply (simp_all add: cbox_Pair_eq [symmetric] content_Pair [symmetric])
   3.945 +      apply (force simp add: interval_split [symmetric] intro!: n1 [rule_format])
   3.946 +      apply (force simp add: interval_split [symmetric] intro!: n2 [rule_format])
   3.947 +      done
   3.948 +  next
   3.949 +    case 2
   3.950 +    then have e: "e * content (cbox (u, w) (v, z)) =
   3.951 +                  e * (content (cbox u v) * content (cbox w z \<inter> {x. x \<bullet> j \<le> M})) +
   3.952 +                  e * (content (cbox u v) * content (cbox w z \<inter> {x. M \<le> x \<bullet> j}))"
   3.953 +      by (simp add: content_split [where c=M] content_Pair algebra_simps)
   3.954 +    have "(\<lambda>x. integral (cbox w z \<inter> {x. x \<bullet> j \<le> M}) (\<lambda>y. f (x, y))) integrable_on cbox u v"
   3.955 +                "(\<lambda>x. integral (cbox w z \<inter> {x. M \<le> x \<bullet> j}) (\<lambda>y. f (x, y))) integrable_on cbox u v"
   3.956 +      using 2 subs
   3.957 +      apply (simp_all add: interval_split)
   3.958 +      apply (rule_tac [!] integral_integrable_2dim [OF continuous_on_subset [OF f]])
   3.959 +      apply (auto simp: cbox_Pair_eq interval_split [symmetric])
   3.960 +      done
   3.961 +    with 2 have *: "integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))) =
   3.962 +                   integral (cbox u v) (\<lambda>x. integral (cbox w z \<inter> {x. x \<bullet> j \<le> M}) (\<lambda>y. f (x, y))) +
   3.963 +                   integral (cbox u v) (\<lambda>x. integral (cbox w z \<inter> {x. M \<le> x \<bullet> j}) (\<lambda>y. f (x, y)))"
   3.964 +      by (simp add: integral_add [symmetric] integral_split [symmetric]
   3.965 +                    continuous_on_imp_integrable_on_Pair1 [OF fcont] cong: integral_cong)
   3.966 +    show ?normle
   3.967 +      apply (rule norm_diff2 [OF integral_split [where c=M, OF fint ij] * e])
   3.968 +      using 2 subs
   3.969 +      apply (simp_all add: cbox_Pair_eq setcomp_dot2 [of "\<lambda>u. M\<le>u"] setcomp_dot2 [of "\<lambda>u. u\<le>M"] Sigma_Int_Paircomp2)
   3.970 +      apply (simp_all add: interval_split ij)
   3.971 +      apply (simp_all add: cbox_Pair_eq [symmetric] content_Pair [symmetric])
   3.972 +      apply (force simp add: interval_split [symmetric] intro!: n1 [rule_format])
   3.973 +      apply (force simp add: interval_split [symmetric] intro!: n2 [rule_format])
   3.974 +      done
   3.975 +  qed
   3.976 +qed
   3.977 +
   3.978 +lemma dense_eq0_I:
   3.979 +  fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
   3.980 +  shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) ==> x = 0"
   3.981 +by (metis dense not_less zero_less_abs_iff)
   3.982 +
   3.983 +lemma integral_Pair_const:
   3.984 +    "integral (cbox (a,c) (b,d)) (\<lambda>x. k) =
   3.985 +     integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. k))"
   3.986 +  by (simp add: content_Pair)
   3.987 +
   3.988 +lemma norm_minus2: "norm (x1-x2, y1-y2) = norm (x2-x1, y2-y1)"
   3.989 +  by (simp add: norm_minus_eqI)
   3.990 +
   3.991 +lemma integral_prod_continuous:
   3.992 +  fixes f :: "('a::euclidean_space * 'b::euclidean_space) \<Rightarrow> 'c::banach"
   3.993 +  assumes "continuous_on (cbox (a,c) (b,d)) f" (is "continuous_on ?CBOX f")
   3.994 +    shows "integral (cbox (a,c) (b,d)) f = integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f(x,y)))"
   3.995 +proof (cases "content ?CBOX = 0")
   3.996 +  case True
   3.997 +  then show ?thesis
   3.998 +    by (auto simp: content_Pair)
   3.999 +next
  3.1000 +  case False
  3.1001 +  then have cbp: "content ?CBOX > 0"
  3.1002 +    using content_lt_nz by blast
  3.1003 +  have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) = 0"
  3.1004 +  proof (rule dense_eq0_I, simp)
  3.1005 +    fix e::real  assume "0 < e"
  3.1006 +    with cbp have e': "0 < e / content ?CBOX"
  3.1007 +      by simp
  3.1008 +    have f_int_acbd: "f integrable_on cbox (a,c) (b,d)"
  3.1009 +      by (rule integrable_continuous [OF assms])
  3.1010 +    { fix p
  3.1011 +      assume p: "p division_of cbox (a,c) (b,d)"
  3.1012 +      note opd1 = operative_division_and [OF integral_swap_operative [OF assms e'], THEN iffD1,
  3.1013 +                       THEN spec, THEN spec, THEN spec, THEN spec, of p "(a,c)" "(b,d)" a c b d]
  3.1014 +      have "(\<And>t u v w z.
  3.1015 +              \<lbrakk>t \<in> p; cbox (u,w) (v,z) \<subseteq> t;  cbox (u,w) (v,z) \<subseteq> cbox (a,c) (b,d)\<rbrakk> \<Longrightarrow>
  3.1016 +              norm (integral (cbox (u,w) (v,z)) f - integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))))
  3.1017 +              \<le> e * content (cbox (u,w) (v,z)) / content?CBOX)
  3.1018 +            \<Longrightarrow>
  3.1019 +            norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e"
  3.1020 +        using opd1 [OF p] False  by simp
  3.1021 +    } note op_acbd = this
  3.1022 +    { fix k::real and p and u::'a and v w and z::'b and t1 t2 l
  3.1023 +      assume k: "0 < k"
  3.1024 +         and nf: "\<And>x y u v.
  3.1025 +                  \<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.1026 +                  \<Longrightarrow> norm (f(u,v) - f(x,y)) < e / (2 * (content ?CBOX))"
  3.1027 +         and p_acbd: "p tagged_division_of cbox (a,c) (b,d)"
  3.1028 +         and fine: "(\<lambda>x. ball x k) fine p"  "((t1,t2), l) \<in> p"
  3.1029 +         and uwvz_sub: "cbox (u,w) (v,z) \<subseteq> l" "cbox (u,w) (v,z) \<subseteq> cbox (a,c) (b,d)"
  3.1030 +      have t: "t1 \<in> cbox a b" "t2 \<in> cbox c d"
  3.1031 +        by (meson fine p_acbd cbox_Pair_iff tag_in_interval)+
  3.1032 +      have ls: "l \<subseteq> ball (t1,t2) k"
  3.1033 +        using fine by (simp add: fine_def Ball_def)
  3.1034 +      { fix x1 x2
  3.1035 +        assume xuvwz: "x1 \<in> cbox u v" "x2 \<in> cbox w z"
  3.1036 +        then have x: "x1 \<in> cbox a b" "x2 \<in> cbox c d"
  3.1037 +          using uwvz_sub by auto
  3.1038 +        have "norm (x1 - t1, x2 - t2) < k"
  3.1039 +          using xuvwz ls uwvz_sub unfolding ball_def
  3.1040 +          by (force simp add: cbox_Pair_eq dist_norm norm_minus2)
  3.1041 +        then have "norm (f (x1,x2) - f (t1,t2)) \<le> e / content ?CBOX / 2"
  3.1042 +          using nf [OF t x]  by simp
  3.1043 +      } note nf' = this
  3.1044 +      have f_int_uwvz: "f integrable_on cbox (u,w) (v,z)"
  3.1045 +        using f_int_acbd uwvz_sub integrable_on_subcbox by blast
  3.1046 +      have f_int_uv: "\<And>x. x \<in> cbox u v \<Longrightarrow> (\<lambda>y. f (x,y)) integrable_on cbox w z"
  3.1047 +        using assms continuous_on_subset uwvz_sub
  3.1048 +        by (blast intro: continuous_on_imp_integrable_on_Pair1)
  3.1049 +      have 1: "norm (integral (cbox (u,w) (v,z)) f - integral (cbox (u,w) (v,z)) (\<lambda>x. f (t1,t2)))
  3.1050 +         \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
  3.1051 +        apply (simp only: integral_sub [symmetric] f_int_uwvz integrable_const)
  3.1052 +        apply (rule order_trans [OF integrable_bound [of "e / content ?CBOX / 2"]])
  3.1053 +        using cbp e' nf'
  3.1054 +        apply (auto simp: integrable_sub f_int_uwvz integrable_const)
  3.1055 +        done
  3.1056 +      have int_integrable: "(\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))) integrable_on cbox u v"
  3.1057 +        using assms integral_integrable_2dim continuous_on_subset uwvz_sub(2) by blast
  3.1058 +      have normint_wz:
  3.1059 +         "\<And>x. x \<in> cbox u v \<Longrightarrow>
  3.1060 +               norm (integral (cbox w z) (\<lambda>y. f (x, y)) - integral (cbox w z) (\<lambda>y. f (t1, t2)))
  3.1061 +               \<le> e * content (cbox w z) / content (cbox (a, c) (b, d)) / 2"
  3.1062 +        apply (simp only: integral_sub [symmetric] f_int_uv integrable_const)
  3.1063 +        apply (rule order_trans [OF integrable_bound [of "e / content ?CBOX / 2"]])
  3.1064 +        using cbp e' nf'
  3.1065 +        apply (auto simp: integrable_sub f_int_uv integrable_const)
  3.1066 +        done
  3.1067 +      have "norm (integral (cbox u v)
  3.1068 +               (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y)) - integral (cbox w z) (\<lambda>y. f (t1,t2))))
  3.1069 +            \<le> e * content (cbox w z) / content ?CBOX / 2 * content (cbox u v)"
  3.1070 +        apply (rule integrable_bound [OF _ _ normint_wz])
  3.1071 +        using cbp e'
  3.1072 +        apply (auto simp: divide_simps content_pos_le integrable_sub int_integrable integrable_const)
  3.1073 +        done
  3.1074 +      also have "... \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
  3.1075 +        by (simp add: content_Pair divide_simps)
  3.1076 +      finally have 2: "norm (integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))) -
  3.1077 +                      integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (t1,t2))))
  3.1078 +                \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
  3.1079 +        by (simp only: integral_sub [symmetric] int_integrable integrable_const)
  3.1080 +      have norm_xx: "\<lbrakk>x' = y'; norm(x - x') \<le> e/2; norm(y - y') \<le> e/2\<rbrakk> \<Longrightarrow> norm(x - y) \<le> e" for x::'c and y x' y' e
  3.1081 +        using norm_triangle_mono [of "x-y'" "e/2" "y'-y" "e/2"] real_sum_of_halves
  3.1082 +        by (simp add: norm_minus_commute)
  3.1083 +      have "norm (integral (cbox (u,w) (v,z)) f - integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))))
  3.1084 +            \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX"
  3.1085 +        by (rule norm_xx [OF integral_Pair_const 1 2])
  3.1086 +    } note * = this
  3.1087 +    show "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e"
  3.1088 +      using compact_uniformly_continuous [OF assms compact_cbox]
  3.1089 +      apply (simp add: uniformly_continuous_on_def dist_norm)
  3.1090 +      apply (drule_tac x="e / 2 / content?CBOX" in spec)
  3.1091 +      using cbp `0 < e`
  3.1092 +      apply (auto simp: zero_less_mult_iff)
  3.1093 +      apply (rename_tac k)
  3.1094 +      apply (rule_tac e1=k in fine_division_exists [OF gauge_ball, where a = "(a,c)" and b = "(b,d)"])
  3.1095 +      apply assumption
  3.1096 +      apply (rule op_acbd)
  3.1097 +      apply (erule division_of_tagged_division)
  3.1098 +      using *
  3.1099 +      apply auto
  3.1100 +      done
  3.1101 +  qed
  3.1102 +  then show ?thesis
  3.1103 +    by simp
  3.1104 +qed
  3.1105 +
  3.1106 +lemma swap_continuous:
  3.1107 +  assumes "continuous_on (cbox (a,c) (b,d)) (\<lambda>(x,y). f x y)"
  3.1108 +    shows "continuous_on (cbox (c,a) (d,b)) (\<lambda>(x, y). f y x)"
  3.1109 +proof -
  3.1110 +  have "(\<lambda>(x, y). f y x) = (\<lambda>(x, y). f x y) o prod.swap"
  3.1111 +    by auto
  3.1112 +  then show ?thesis
  3.1113 +    apply (rule ssubst)
  3.1114 +    apply (rule continuous_on_compose)
  3.1115 +    apply (simp add: split_def)
  3.1116 +    apply (rule continuous_intros | simp add: assms)+
  3.1117 +    done
  3.1118 +qed
  3.1119 +
  3.1120 +lemma integral_swap_2dim:
  3.1121 +  fixes f :: "['a::euclidean_space, 'b::euclidean_space] \<Rightarrow> 'c::banach"
  3.1122 +  assumes "continuous_on (cbox (a,c) (b,d)) (\<lambda>(x,y). f x y)"
  3.1123 +    shows "integral (cbox (a, c) (b, d)) (\<lambda>(x, y). f x y) = integral (cbox (c, a) (d, b)) (\<lambda>(x, y). f y x)"
  3.1124 +proof -
  3.1125 +  have "((\<lambda>(x, y). f x y) has_integral integral (cbox (c, a) (d, b)) (\<lambda>(x, y). f y x)) (prod.swap ` (cbox (c, a) (d, b)))"
  3.1126 +    apply (rule has_integral_twiddle [of 1 prod.swap prod.swap "\<lambda>(x,y). f y x" "integral (cbox (c, a) (d, b)) (\<lambda>(x, y). f y x)", simplified])
  3.1127 +    apply (auto simp: isCont_swap content_Pair has_integral_integral [symmetric] integrable_continuous swap_continuous assms)
  3.1128 +    done
  3.1129 + then show ?thesis
  3.1130 +   by force
  3.1131 +qed
  3.1132 +
  3.1133 +theorem integral_swap_continuous:
  3.1134 +  fixes f :: "['a::euclidean_space, 'b::euclidean_space] \<Rightarrow> 'c::banach"
  3.1135 +  assumes "continuous_on (cbox (a,c) (b,d)) (\<lambda>(x,y). f x y)"
  3.1136 +    shows "integral (cbox a b) (\<lambda>x. integral (cbox c d) (f x)) =
  3.1137 +           integral (cbox c d) (\<lambda>y. integral (cbox a b) (\<lambda>x. f x y))"
  3.1138 +proof -
  3.1139 +  have "integral (cbox a b) (\<lambda>x. integral (cbox c d) (f x)) = integral (cbox (a, c) (b, d)) (\<lambda>(x, y). f x y)"
  3.1140 +    using integral_prod_continuous [OF assms] by auto
  3.1141 +  also have "... = integral (cbox (c, a) (d, b)) (\<lambda>(x, y). f y x)"
  3.1142 +    by (rule integral_swap_2dim [OF assms])
  3.1143 +  also have "... = integral (cbox c d) (\<lambda>y. integral (cbox a b) (\<lambda>x. f x y))"
  3.1144 +    using integral_prod_continuous [OF swap_continuous] assms
  3.1145 +    by auto
  3.1146 +  finally show ?thesis .
  3.1147 +qed
  3.1148 +
  3.1149  end
     4.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 29 13:49:21 2015 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Jun 30 13:56:16 2015 +0100
     4.3 @@ -840,6 +840,18 @@
     4.4      "x \<in> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)"
     4.5    by (auto simp: box_eucl_less eucl_less_def cbox_def)
     4.6  
     4.7 +lemma cbox_Pair_eq: "cbox (a, c) (b, d) = cbox a b \<times> cbox c d"
     4.8 +  by (force simp: cbox_def Basis_prod_def)
     4.9 +
    4.10 +lemma cbox_Pair_iff [iff]: "(x, y) \<in> cbox (a, c) (b, d) \<longleftrightarrow> x \<in> cbox a b \<and> y \<in> cbox c d"
    4.11 +  by (force simp: cbox_Pair_eq)
    4.12 +
    4.13 +lemma cbox_Pair_eq_0: "cbox (a, c) (b, d) = {} \<longleftrightarrow> cbox a b = {} \<or> cbox c d = {}"
    4.14 +  by (force simp: cbox_Pair_eq)
    4.15 +
    4.16 +lemma swap_cbox_Pair [simp]: "prod.swap ` cbox (c, a) (d, b) = cbox (a,c) (b,d)"
    4.17 +  by auto
    4.18 +
    4.19  lemma mem_box_real[simp]:
    4.20    "(x::real) \<in> box a b \<longleftrightarrow> a < x \<and> x < b"
    4.21    "(x::real) \<in> cbox a b \<longleftrightarrow> a \<le> x \<and> x \<le> b"
    4.22 @@ -2794,6 +2806,11 @@
    4.23      by (auto intro!: exI[of _ "b + norm a"])
    4.24  qed
    4.25  
    4.26 +lemma bounded_uminus [simp]:
    4.27 +  fixes X :: "'a::euclidean_space set"
    4.28 +  shows "bounded (uminus ` X) \<longleftrightarrow> bounded X"
    4.29 +by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp add: add.commute norm_minus_commute)
    4.30 +
    4.31  
    4.32  text\<open>Some theorems on sups and infs using the notion "bounded".\<close>
    4.33  
    4.34 @@ -2808,7 +2825,15 @@
    4.35    by (auto simp: bounded_def bdd_below_def dist_real_def)
    4.36       (metis abs_le_D1 add.commute diff_le_eq)
    4.37  
    4.38 -(* TODO: remove the following lemmas about Inf and Sup, is now in conditionally complete lattice *)
    4.39 +lemma bounded_inner_imp_bdd_above:
    4.40 +  assumes "bounded s" 
    4.41 +    shows "bdd_above ((\<lambda>x. x \<bullet> a) ` s)"
    4.42 +by (simp add: assms bounded_imp_bdd_above bounded_linear_image bounded_linear_inner_left)
    4.43 +
    4.44 +lemma bounded_inner_imp_bdd_below:
    4.45 +  assumes "bounded s" 
    4.46 +    shows "bdd_below ((\<lambda>x. x \<bullet> a) ` s)"
    4.47 +by (simp add: assms bounded_imp_bdd_below bounded_linear_image bounded_linear_inner_left)
    4.48  
    4.49  lemma bounded_has_Sup:
    4.50    fixes S :: "real set"
     5.1 --- a/src/HOL/NthRoot.thy	Mon Jun 29 13:49:21 2015 +0200
     5.2 +++ b/src/HOL/NthRoot.thy	Tue Jun 30 13:56:16 2015 +0100
     5.3 @@ -448,6 +448,11 @@
     5.4  lemmas real_sqrt_le_1_iff [simp] = real_sqrt_le_iff [where y=1, unfolded real_sqrt_one]
     5.5  lemmas real_sqrt_eq_1_iff [simp] = real_sqrt_eq_iff [where y=1, unfolded real_sqrt_one]
     5.6  
     5.7 +lemma sqrt_add_le_add_sqrt:
     5.8 +  assumes "0 \<le> x" "0 \<le> y"
     5.9 +  shows "sqrt (x + y) \<le> sqrt x + sqrt y"
    5.10 +by (rule power2_le_imp_le) (simp_all add: power2_sum assms)
    5.11 +
    5.12  lemma isCont_real_sqrt: "isCont sqrt x"
    5.13  unfolding sqrt_def by (rule isCont_real_root)
    5.14  
     6.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon Jun 29 13:49:21 2015 +0200
     6.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Jun 30 13:56:16 2015 +0100
     6.3 @@ -19,7 +19,7 @@
     6.4  lemma emeasure_interval_measure_Ioc:
     6.5    assumes "a \<le> b"
     6.6    assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y"
     6.7 -  assumes right_cont_F : "\<And>a. continuous (at_right a) F" 
     6.8 +  assumes right_cont_F : "\<And>a. continuous (at_right a) F"
     6.9    shows "emeasure (interval_measure F) {a <.. b} = F b - F a"
    6.10  proof (rule extend_measure_caratheodory_pair[OF interval_measure_def `a \<le> b`])
    6.11    show "semiring_of_sets UNIV {{a<..b} |a b :: real. a \<le> b}"
    6.12 @@ -40,10 +40,10 @@
    6.13        thus ?thesis ..
    6.14      qed
    6.15    qed (auto simp: Ioc_inj, metis linear)
    6.16 -  
    6.17 +
    6.18  next
    6.19    fix l r :: "nat \<Rightarrow> real" and a b :: real
    6.20 -  assume l_r[simp]: "\<And>n. l n \<le> r n" and "a \<le> b" and disj: "disjoint_family (\<lambda>n. {l n<..r n})" 
    6.21 +  assume l_r[simp]: "\<And>n. l n \<le> r n" and "a \<le> b" and disj: "disjoint_family (\<lambda>n. {l n<..r n})"
    6.22    assume lr_eq_ab: "(\<Union>i. {l i<..r i}) = {a<..b}"
    6.23  
    6.24    have [intro, simp]: "\<And>a b. a \<le> b \<Longrightarrow> 0 \<le> F b - F a"
    6.25 @@ -171,7 +171,7 @@
    6.26  
    6.27    { fix epsilon :: real assume egt0: "epsilon > 0"
    6.28      have "\<forall>i. \<exists>d. d > 0 &  F (r i + d) < F (r i) + epsilon / 2^(i+2)"
    6.29 -    proof 
    6.30 +    proof
    6.31        fix i
    6.32        note right_cont_F [of "r i"]
    6.33        thus "\<exists>d. d > 0 \<and> F (r i + d) < F (r i) + epsilon / 2^(i+2)"
    6.34 @@ -182,7 +182,7 @@
    6.35          apply (erule impE)
    6.36          using egt0 by (auto simp add: field_simps)
    6.37      qed
    6.38 -    then obtain delta where 
    6.39 +    then obtain delta where
    6.40          deltai_gt0: "\<And>i. delta i > 0" and
    6.41          deltai_prop: "\<And>i. F (r i + delta i) < F (r i) + epsilon / 2^(i+2)"
    6.42        by metis
    6.43 @@ -192,12 +192,12 @@
    6.44        using mono_F apply force
    6.45        apply (drule_tac x = "epsilon / 2" in spec)
    6.46        using egt0 unfolding mult.commute [of 2] by force
    6.47 -    then obtain a' where a'lea [arith]: "a' > a" and 
    6.48 +    then obtain a' where a'lea [arith]: "a' > a" and
    6.49        a_prop: "F a' - F a < epsilon / 2"
    6.50        by auto
    6.51      def S' \<equiv> "{i. l i < r i}"
    6.52 -    obtain S :: "nat set" where 
    6.53 -      "S \<subseteq> S'" and finS: "finite S" and 
    6.54 +    obtain S :: "nat set" where
    6.55 +      "S \<subseteq> S'" and finS: "finite S" and
    6.56        Sprop: "{a'..b} \<subseteq> (\<Union>i \<in> S. {l i<..<r i + delta i})"
    6.57      proof (rule compactE_image)
    6.58        show "compact {a'..b}"
    6.59 @@ -216,7 +216,7 @@
    6.60        finally show "{a'..b} \<subseteq> (\<Union>i \<in> S'. {l i<..<r i + delta i})" .
    6.61      qed
    6.62      with S'_def have Sprop2: "\<And>i. i \<in> S \<Longrightarrow> l i < r i" by auto
    6.63 -    from finS have "\<exists>n. \<forall>i \<in> S. i \<le> n" 
    6.64 +    from finS have "\<exists>n. \<forall>i \<in> S. i \<le> n"
    6.65        by (subst finite_nat_set_iff_bounded_le [symmetric])
    6.66      then obtain n where Sbound [rule_format]: "\<forall>i \<in> S. i \<le> n" ..
    6.67      have "F b - F a' \<le> (\<Sum>i\<in>S. F (r i + delta i) - F (l i))"
    6.68 @@ -233,14 +233,14 @@
    6.69        apply (rule less_imp_le)
    6.70        apply (rule deltai_prop)
    6.71        by auto
    6.72 -    also have "... = (SUM i : S. F(r i) - F(l i)) + 
    6.73 +    also have "... = (SUM i : S. F(r i) - F(l i)) +
    6.74          (epsilon / 4) * (SUM i : S. (1 / 2)^i)" (is "_ = ?t + _")
    6.75        by (subst setsum.distrib) (simp add: field_simps setsum_right_distrib)
    6.76      also have "... \<le> ?t + (epsilon / 4) * (\<Sum> i < Suc n. (1 / 2)^i)"
    6.77        apply (rule add_left_mono)
    6.78        apply (rule mult_left_mono)
    6.79        apply (rule setsum_mono2)
    6.80 -      using egt0 apply auto 
    6.81 +      using egt0 apply auto
    6.82        by (frule Sbound, auto)
    6.83      also have "... \<le> ?t + (epsilon / 2)"
    6.84        apply (rule add_left_mono)
    6.85 @@ -285,7 +285,7 @@
    6.86  lemma measure_interval_measure_Ioc:
    6.87    assumes "a \<le> b"
    6.88    assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y"
    6.89 -  assumes right_cont_F : "\<And>a. continuous (at_right a) F" 
    6.90 +  assumes right_cont_F : "\<And>a. continuous (at_right a) F"
    6.91    shows "measure (interval_measure F) {a <.. b} = F b - F a"
    6.92    unfolding measure_def
    6.93    apply (subst emeasure_interval_measure_Ioc)
    6.94 @@ -312,7 +312,7 @@
    6.95  lemma emeasure_interval_measure_Icc:
    6.96    assumes "a \<le> b"
    6.97    assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y"
    6.98 -  assumes cont_F : "continuous_on UNIV F" 
    6.99 +  assumes cont_F : "continuous_on UNIV F"
   6.100    shows "emeasure (interval_measure F) {a .. b} = F b - F a"
   6.101  proof (rule tendsto_unique)
   6.102    { fix a b :: real assume "a \<le> b" then have "emeasure (interval_measure F) {a <.. b} = F b - F a"
   6.103 @@ -349,10 +349,10 @@
   6.104      by (intro lim_ereal[THEN iffD2] tendsto_intros )
   6.105         (auto simp: continuous_on_def intro: tendsto_within_subset)
   6.106  qed (rule trivial_limit_at_left_real)
   6.107 -  
   6.108 +
   6.109  lemma sigma_finite_interval_measure:
   6.110    assumes mono_F: "\<And>x y. x \<le> y \<Longrightarrow> F x \<le> F y"
   6.111 -  assumes right_cont_F : "\<And>a. continuous (at_right a) F" 
   6.112 +  assumes right_cont_F : "\<And>a. continuous (at_right a) F"
   6.113    shows "sigma_finite_measure (interval_measure F)"
   6.114    apply unfold_locales
   6.115    apply (intro exI[of _ "(\<lambda>(a, b). {a <.. b}) ` (\<rat> \<times> \<rat>)"])
   6.116 @@ -364,7 +364,7 @@
   6.117  definition lborel :: "('a :: euclidean_space) measure" where
   6.118    "lborel = distr (\<Pi>\<^sub>M b\<in>Basis. interval_measure (\<lambda>x. x)) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)"
   6.119  
   6.120 -lemma 
   6.121 +lemma
   6.122    shows sets_lborel[simp, measurable_cong]: "sets lborel = sets borel"
   6.123      and space_lborel[simp]: "space lborel = space borel"
   6.124      and measurable_lborel1[simp]: "measurable M lborel = measurable M borel"
   6.125 @@ -395,7 +395,7 @@
   6.126    by (simp add: lborel_def nn_integral_distr product_nn_integral_setprod
   6.127                  product_nn_integral_singleton)
   6.128  
   6.129 -lemma emeasure_lborel_Icc[simp]: 
   6.130 +lemma emeasure_lborel_Icc[simp]:
   6.131    fixes l u :: real
   6.132    assumes [simp]: "l \<le> u"
   6.133    shows "emeasure lborel {l .. u} = u - l"
   6.134 @@ -486,7 +486,7 @@
   6.135      and measure_lborel_Ioo[simp]: "measure lborel {l <..< u} = u - l"
   6.136    by (simp_all add: measure_def)
   6.137  
   6.138 -lemma 
   6.139 +lemma
   6.140    assumes [simp]: "\<And>b. b \<in> Basis \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b"
   6.141    shows measure_lborel_box[simp]: "measure lborel (box l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
   6.142      and measure_lborel_cbox[simp]: "measure lborel (cbox l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
   6.143 @@ -507,7 +507,7 @@
   6.144      let ?Ba = "Basis :: 'a set"
   6.145      have "real n \<le> (2::real) ^ card ?Ba * real n"
   6.146        by (simp add: mult_le_cancel_right1)
   6.147 -    also 
   6.148 +    also
   6.149      have "... \<le> (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba"
   6.150        apply (rule mult_left_mono)
   6.151        apply (metis DIM_positive One_nat_def less_eq_Suc_le less_imp_le real_of_nat_le_iff real_of_nat_power self_le_power zero_less_Suc)
   6.152 @@ -518,9 +518,9 @@
   6.153    show ?thesis
   6.154      unfolding UN_box_eq_UNIV[symmetric]
   6.155      apply (subst SUP_emeasure_incseq[symmetric])
   6.156 -    apply (auto simp: incseq_def subset_box inner_add_left setprod_constant 
   6.157 +    apply (auto simp: incseq_def subset_box inner_add_left setprod_constant
   6.158                 intro!: SUP_PInfty)
   6.159 -    done 
   6.160 +    done
   6.161  qed
   6.162  
   6.163  lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0"
   6.164 @@ -551,7 +551,7 @@
   6.165    assume asm: "lborel = count_space A"
   6.166    have "space lborel = UNIV" by simp
   6.167    hence [simp]: "A = UNIV" by (subst (asm) asm) (simp only: space_count_space)
   6.168 -  have "emeasure lborel {undefined::'a} = 1" 
   6.169 +  have "emeasure lborel {undefined::'a} = 1"
   6.170        by (subst asm, subst emeasure_count_space_finite) auto
   6.171    moreover have "emeasure lborel {undefined} \<noteq> 1" by simp
   6.172    ultimately show False by contradiction
   6.173 @@ -607,7 +607,7 @@
   6.174      then have "\<And>x. indicator (box l u) (t + c *\<^sub>R x) = (indicator (box ((u - t) /\<^sub>R c) ((l - t) /\<^sub>R c)) x :: ereal)"
   6.175        by (auto split: split_indicator)
   6.176      moreover
   6.177 -    { have "(- c) ^ card ?B * (\<Prod>x\<in>?B. l \<bullet> x - u \<bullet> x) = 
   6.178 +    { have "(- c) ^ card ?B * (\<Prod>x\<in>?B. l \<bullet> x - u \<bullet> x) =
   6.179           (-1 * c) ^ card ?B * (\<Prod>x\<in>?B. -1 * (u \<bullet> x - l \<bullet> x))"
   6.180           by simp
   6.181        also have "\<dots> = (-1 * -1)^card ?B * c ^ card ?B * (\<Prod>x\<in>?B. u \<bullet> x - l \<bullet> x)"
   6.182 @@ -626,7 +626,7 @@
   6.183    "c \<noteq> 0 \<Longrightarrow> lborel = density (distr lborel borel (\<lambda>x. t + c * x)) (\<lambda>_. \<bar>c\<bar>)"
   6.184    using lborel_affine[of c t] by simp
   6.185  
   6.186 -lemma AE_borel_affine: 
   6.187 +lemma AE_borel_affine:
   6.188    fixes P :: "real \<Rightarrow> bool"
   6.189    shows "c \<noteq> 0 \<Longrightarrow> Measurable.pred borel P \<Longrightarrow> AE x in lborel. P x \<Longrightarrow> AE x in lborel. P (t + c * x)"
   6.190    by (subst lborel_real_affine[where t="- t / c" and c="1 / c"])
   6.191 @@ -666,7 +666,7 @@
   6.192      by (simp add: lborel_integrable_real_affine_iff not_integrable_integral_eq)
   6.193  qed
   6.194  
   6.195 -lemma divideR_right: 
   6.196 +lemma divideR_right:
   6.197    fixes x y :: "'a::real_normed_vector"
   6.198    shows "r \<noteq> 0 \<Longrightarrow> y = x /\<^sub>R r \<longleftrightarrow> r *\<^sub>R y = x"
   6.199    using scaleR_cancel_left[of r y "x /\<^sub>R r"] by simp
   6.200 @@ -680,10 +680,10 @@
   6.201    by (simp_all add: lborel_integral_real_affine[symmetric] divideR_right cong: conj_cong)
   6.202  
   6.203  lemma lborel_distr_uminus: "distr lborel borel uminus = (lborel :: real measure)"
   6.204 -  by (subst lborel_real_affine[of "-1" 0]) 
   6.205 +  by (subst lborel_real_affine[of "-1" 0])
   6.206       (auto simp: density_1 one_ereal_def[symmetric])
   6.207  
   6.208 -lemma lborel_distr_mult: 
   6.209 +lemma lborel_distr_mult:
   6.210    assumes "(c::real) \<noteq> 0"
   6.211    shows "distr lborel borel (op * c) = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
   6.212  proof-
   6.213 @@ -693,7 +693,7 @@
   6.214    finally show ?thesis .
   6.215  qed
   6.216  
   6.217 -lemma lborel_distr_mult': 
   6.218 +lemma lborel_distr_mult':
   6.219    assumes "(c::real) \<noteq> 0"
   6.220    shows "lborel = density (distr lborel borel (op * c)) (\<lambda>_. abs c)"
   6.221  proof-
   6.222 @@ -789,7 +789,7 @@
   6.223        ultimately have "((\<lambda>x. 1 - (if x \<in> A \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
   6.224          by (rule has_integral_sub)
   6.225        then have "((\<lambda>x. (if x \<in> (UNIV - A) \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
   6.226 -        by (rule has_integral_eq_eq[THEN iffD1, rotated 1]) auto
   6.227 +        by (rule has_integral_cong[THEN iffD1, rotated 1]) auto
   6.228        then have "((\<lambda>x. 1) has_integral ?M (box a b) - ?M A) ((UNIV - A) \<inter> box a b)"
   6.229          by (subst (asm) has_integral_restrict) auto
   6.230        also have "?M (box a b) - ?M A = ?M (UNIV - A)"
   6.231 @@ -887,7 +887,7 @@
   6.232    case (seq U)
   6.233    note seq(1)[measurable] and f[measurable]
   6.234  
   6.235 -  { fix i x 
   6.236 +  { fix i x
   6.237      have "U i x \<le> f x"
   6.238        using seq(5)
   6.239        apply (rule LIMSEQ_le_const)
   6.240 @@ -895,7 +895,7 @@
   6.241        apply (auto intro!: exI[of _ i] simp: incseq_def le_fun_def)
   6.242        done }
   6.243    note U_le_f = this
   6.244 -  
   6.245 +
   6.246    { fix i
   6.247      have "(\<integral>\<^sup>+x. ereal (U i x) \<partial>lborel) \<le> (\<integral>\<^sup>+x. ereal (f x) \<partial>lborel)"
   6.248        using U_le_f by (intro nn_integral_mono) simp
   6.249 @@ -951,7 +951,7 @@
   6.250      by (intro has_integral_integrable[where i=r] nn_integral_has_integral[where r=r] f)
   6.251  qed
   6.252  
   6.253 -lemma nn_integral_has_integral_lborel: 
   6.254 +lemma nn_integral_has_integral_lborel:
   6.255    fixes f :: "'a::euclidean_space \<Rightarrow> real"
   6.256    assumes f_borel: "f \<in> borel_measurable borel" and nonneg: "\<And>x. 0 \<le> f x"
   6.257    assumes I: "(f has_integral I) UNIV"
   6.258 @@ -996,7 +996,7 @@
   6.259        have "emeasure lborel {x \<in> space lborel. ereal (real (F i x) * indicator (?B i) x) \<noteq> 0} \<le>
   6.260          emeasure lborel (?B i)"
   6.261          by (intro emeasure_mono)  (auto split: split_indicator)
   6.262 -      then show "emeasure lborel {x \<in> space lborel. ereal (real (F i x) * indicator (?B i) x) \<noteq> 0} < \<infinity>"  
   6.263 +      then show "emeasure lborel {x \<in> space lborel. ereal (real (F i x) * indicator (?B i) x) \<noteq> 0} < \<infinity>"
   6.264          by auto
   6.265      qed (auto split: split_indicator
   6.266                intro!: real_of_ereal_pos F simple_function_compose1[where g="real"] simple_function_ereal)
   6.267 @@ -1004,8 +1004,8 @@
   6.268      have int_F: "(\<lambda>x. real (F i x) * indicator (?B i) x) integrable_on UNIV"
   6.269        using F(5) finite_F
   6.270        by (intro nn_integral_integrable_on) (auto split: split_indicator intro: real_of_ereal_pos)
   6.271 -    
   6.272 -    have "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) = 
   6.273 +
   6.274 +    have "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) =
   6.275        (\<integral>\<^sup>+ x. ereal (real (F i x) * indicator (?B i) x) \<partial>lborel)"
   6.276        using F(3,5)
   6.277        by (intro nn_integral_cong) (auto simp: image_iff ereal_real eq_commute split: split_indicator)
   6.278 @@ -1100,7 +1100,7 @@
   6.279  
   6.280  lemma integrable_on_lborel: "integrable lborel f \<Longrightarrow> f integrable_on UNIV"
   6.281    using has_integral_integral_lborel by (auto intro: has_integral_integrable)
   6.282 -  
   6.283 +
   6.284  lemma integral_lborel: "integrable lborel f \<Longrightarrow> integral UNIV f = (\<integral>x. f x \<partial>lborel)"
   6.285    using has_integral_integral_lborel by auto
   6.286  
   6.287 @@ -1161,7 +1161,7 @@
   6.288  
   6.289  text {*
   6.290  
   6.291 -For the positive integral we replace continuity with Borel-measurability. 
   6.292 +For the positive integral we replace continuity with Borel-measurability.
   6.293  
   6.294  *}
   6.295  
   6.296 @@ -1177,7 +1177,7 @@
   6.297  proof -
   6.298    have *: "(\<lambda>x. f x * indicator {a..b} x) \<in> borel_measurable borel" "\<And>x. 0 \<le> f x * indicator {a..b} x"
   6.299      using f(2) by (auto split: split_indicator)
   6.300 -    
   6.301 +
   6.302    have "(f has_integral F b - F a) {a..b}"
   6.303      by (intro fundamental_theorem_of_calculus)
   6.304         (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric]
   6.305 @@ -1209,7 +1209,7 @@
   6.306      using borel_integrable_compact[OF _ cont] by auto
   6.307    have "(f has_integral F b - F a) {a..b}"
   6.308      using assms(1,2) by (intro fundamental_theorem_of_calculus) auto
   6.309 -  moreover 
   6.310 +  moreover
   6.311    have "(f has_integral integral\<^sup>L lborel ?f) {a..b}"
   6.312      using has_integral_integral_lborel[OF int]
   6.313      unfolding indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a]
   6.314 @@ -1242,7 +1242,7 @@
   6.315  lemma nn_integral_FTC_atLeast:
   6.316    fixes f :: "real \<Rightarrow> real"
   6.317    assumes f_borel: "f \<in> borel_measurable borel"
   6.318 -  assumes f: "\<And>x. a \<le> x \<Longrightarrow> DERIV F x :> f x" 
   6.319 +  assumes f: "\<And>x. a \<le> x \<Longrightarrow> DERIV F x :> f x"
   6.320    assumes nonneg: "\<And>x. a \<le> x \<Longrightarrow> 0 \<le> f x"
   6.321    assumes lim: "(F ---> T) at_top"
   6.322    shows "(\<integral>\<^sup>+x. ereal (f x) * indicator {a ..} x \<partial>lborel) = T - F a"
   6.323 @@ -1280,7 +1280,7 @@
   6.324        with f nonneg show "F (a + real m) \<le> F (a + real n)"
   6.325          by (intro DERIV_nonneg_imp_nondecreasing[where f=F])
   6.326             (simp, metis add_increasing2 order_refl order_trans real_of_nat_ge_zero)
   6.327 -    qed 
   6.328 +    qed
   6.329      have "(\<lambda>x. F (a + real x)) ----> T"
   6.330        apply (rule filterlim_compose[OF lim filterlim_tendsto_add_at_top])
   6.331        apply (rule LIMSEQ_const_iff[THEN iffD2, OF refl])
   6.332 @@ -1320,10 +1320,10 @@
   6.333    assumes [intro]: "!!x. DERIV F x :> f x"
   6.334    assumes [intro]: "!!x. DERIV G x :> g x"
   6.335    shows "(\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel)
   6.336 -            =  F b * G b - F a * G a - \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel" 
   6.337 +            =  F b * G b - F a * G a - \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
   6.338  proof-
   6.339    have 0: "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = F b * G b - F a * G a"
   6.340 -    by (rule integral_FTC_Icc_real, auto intro!: derivative_eq_intros continuous_intros) 
   6.341 +    by (rule integral_FTC_Icc_real, auto intro!: derivative_eq_intros continuous_intros)
   6.342        (auto intro!: DERIV_isCont)
   6.343  
   6.344    have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) =
   6.345 @@ -1343,7 +1343,7 @@
   6.346    assumes "!!x. DERIV F x :> f x"
   6.347    assumes "!!x. DERIV G x :> g x"
   6.348    shows "(\<integral>x. indicator {a .. b} x *\<^sub>R (F x * g x) \<partial>lborel)
   6.349 -            =  F b * G b - F a * G a - \<integral>x. indicator {a .. b} x *\<^sub>R (f x * G x) \<partial>lborel" 
   6.350 +            =  F b * G b - F a * G a - \<integral>x. indicator {a .. b} x *\<^sub>R (f x * G x) \<partial>lborel"
   6.351    using integral_by_parts[OF assms] by (simp add: ac_simps)
   6.352  
   6.353  lemma has_bochner_integral_even_function:
   6.354 @@ -1379,7 +1379,7 @@
   6.355         (auto simp: indicator odd f)
   6.356    from has_bochner_integral_minus[OF this]
   6.357    have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) (- x)"
   6.358 -    by simp 
   6.359 +    by simp
   6.360    with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + - x)"
   6.361      by (rule has_bochner_integral_add)
   6.362    then have "has_bochner_integral lborel f (x + - x)"
     7.1 --- a/src/HOL/Probability/Set_Integral.thy	Mon Jun 29 13:49:21 2015 +0200
     7.2 +++ b/src/HOL/Probability/Set_Integral.thy	Tue Jun 30 13:56:16 2015 +0100
     7.3 @@ -10,7 +10,7 @@
     7.4    imports Bochner_Integration Lebesgue_Measure
     7.5  begin
     7.6  
     7.7 -(* 
     7.8 +(*
     7.9      Notation
    7.10  *)
    7.11  
    7.12 @@ -67,8 +67,8 @@
    7.13  translations
    7.14  "LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
    7.15  
    7.16 -(* 
    7.17 -    Basic properties 
    7.18 +(*
    7.19 +    Basic properties
    7.20  *)
    7.21  
    7.22  (*
    7.23 @@ -93,13 +93,13 @@
    7.24  
    7.25  lemma set_integrable_cong_AE:
    7.26      "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
    7.27 -    AE x \<in> A in M. f x = g x \<Longrightarrow> A \<in> sets M \<Longrightarrow> 
    7.28 +    AE x \<in> A in M. f x = g x \<Longrightarrow> A \<in> sets M \<Longrightarrow>
    7.29      set_integrable M A f = set_integrable M A g"
    7.30    by (rule integrable_cong_AE) auto
    7.31  
    7.32 -lemma set_integrable_subset: 
    7.33 +lemma set_integrable_subset:
    7.34    fixes M A B and f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
    7.35 -  assumes "set_integrable M A f" "B \<in> sets M" "B \<subseteq> A"  
    7.36 +  assumes "set_integrable M A f" "B \<in> sets M" "B \<subseteq> A"
    7.37    shows "set_integrable M B f"
    7.38  proof -
    7.39    have "set_integrable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
    7.40 @@ -114,17 +114,17 @@
    7.41  lemma set_integral_scaleR_right [simp]: "LINT t:A|M. a *\<^sub>R f t = a *\<^sub>R (LINT t:A|M. f t)"
    7.42    by (subst integral_scaleR_right[symmetric]) (auto intro!: integral_cong)
    7.43  
    7.44 -lemma set_integral_mult_right [simp]: 
    7.45 +lemma set_integral_mult_right [simp]:
    7.46    fixes a :: "'a::{real_normed_field, second_countable_topology}"
    7.47    shows "LINT t:A|M. a * f t = a * (LINT t:A|M. f t)"
    7.48    by (subst integral_mult_right_zero[symmetric]) (auto intro!: integral_cong)
    7.49  
    7.50 -lemma set_integral_mult_left [simp]: 
    7.51 +lemma set_integral_mult_left [simp]:
    7.52    fixes a :: "'a::{real_normed_field, second_countable_topology}"
    7.53    shows "LINT t:A|M. f t * a = (LINT t:A|M. f t) * a"
    7.54    by (subst integral_mult_left_zero[symmetric]) (auto intro!: integral_cong)
    7.55  
    7.56 -lemma set_integral_divide_zero [simp]: 
    7.57 +lemma set_integral_divide_zero [simp]:
    7.58    fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
    7.59    shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a"
    7.60    by (subst integral_divide_zero[symmetric], intro integral_cong)
    7.61 @@ -198,7 +198,7 @@
    7.62    shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
    7.63  using assms by (auto intro: integral_mono split: split_indicator)
    7.64  
    7.65 -lemma set_integral_mono_AE: 
    7.66 +lemma set_integral_mono_AE:
    7.67    fixes f g :: "_ \<Rightarrow> real"
    7.68    assumes "set_integrable M A f" "set_integrable M A g"
    7.69      "AE x \<in> A in M. f x \<le> g x"
    7.70 @@ -210,12 +210,12 @@
    7.71  
    7.72  lemma set_integrable_abs_iff:
    7.73    fixes f :: "_ \<Rightarrow> real"
    7.74 -  shows "set_borel_measurable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f" 
    7.75 +  shows "set_borel_measurable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
    7.76    by (subst (2) integrable_abs_iff[symmetric]) (simp_all add: abs_mult ac_simps)
    7.77  
    7.78  lemma set_integrable_abs_iff':
    7.79    fixes f :: "_ \<Rightarrow> real"
    7.80 -  shows "f \<in> borel_measurable M \<Longrightarrow> A \<in> sets M \<Longrightarrow> 
    7.81 +  shows "f \<in> borel_measurable M \<Longrightarrow> A \<in> sets M \<Longrightarrow>
    7.82      set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
    7.83  by (intro set_integrable_abs_iff) auto
    7.84  
    7.85 @@ -303,7 +303,7 @@
    7.86    then have f': "set_borel_measurable M (A \<union> B) f"
    7.87      by (rule borel_measurable_integrable)
    7.88    have "LINT x:A\<union>B|M. f x = LINT x:(A - A \<inter> B) \<union> (B - A \<inter> B)|M. f x"
    7.89 -  proof (rule set_integral_cong_set)  
    7.90 +  proof (rule set_integral_cong_set)
    7.91      show "AE x in M. (x \<in> A - A \<inter> B \<union> (B - A \<inter> B)) = (x \<in> A \<union> B)"
    7.92        using ae by auto
    7.93      show "set_borel_measurable M (A - A \<inter> B \<union> (B - A \<inter> B)) f"
    7.94 @@ -389,7 +389,7 @@
    7.95      fix n
    7.96      show "0 \<le> LINT x|M. norm (indicator (A n) x *\<^sub>R f x)"
    7.97        using norm_f by (auto intro!: integral_nonneg_AE)
    7.98 -    
    7.99 +
   7.100      have "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) =
   7.101        (\<Sum>i<n. set_lebesgue_integral M (A i) (\<lambda>x. norm (f x)))"
   7.102        by (simp add: abs_mult)
   7.103 @@ -423,7 +423,7 @@
   7.104    then show "\<And>i. set_borel_measurable M (A i) f" "set_borel_measurable M (\<Union>i. A i) f"
   7.105      "set_integrable M (\<Union>i. A i) (\<lambda>x. norm (f x))"
   7.106      using intgbl integrable_norm[OF intgbl] by auto
   7.107 -  
   7.108 +
   7.109    { fix x i assume "x \<in> A i"
   7.110      with A have "(\<lambda>xa. indicator (A xa) x::real) ----> 1 \<longleftrightarrow> (\<lambda>xa. 1::real) ----> 1"
   7.111        by (intro filterlim_cong refl)
   7.112 @@ -431,7 +431,7 @@
   7.113    then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) ----> indicator (\<Union>i. A i) x *\<^sub>R f x"
   7.114      by (intro AE_I2 tendsto_intros) (auto split: split_indicator)
   7.115  qed (auto split: split_indicator)
   7.116 -        
   7.117 +
   7.118  (* Can the int0 hypothesis be dropped? *)
   7.119  lemma set_integral_cont_down:
   7.120    fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   7.121 @@ -549,7 +549,7 @@
   7.122    have "(f has_integral F b - F a) {a .. b}"
   7.123      by (intro fundamental_theorem_of_calculus ballI assms) auto
   7.124    then have "(?f has_integral F b - F a) {a .. b}"
   7.125 -    by (subst has_integral_eq_eq[where g=f]) auto
   7.126 +    by (subst has_integral_cong[where g=f]) auto
   7.127    then have "(?f has_integral F b - F a) UNIV"
   7.128      by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto
   7.129    ultimately show "integral\<^sup>L lborel ?f = F b - F a"
     8.1 --- a/src/HOL/Rings.thy	Mon Jun 29 13:49:21 2015 +0200
     8.2 +++ b/src/HOL/Rings.thy	Tue Jun 30 13:56:16 2015 +0100
     8.3 @@ -1362,7 +1362,30 @@
     8.4  
     8.5  lemma add_diff_inverse: "~ a<b \<Longrightarrow> b + (a - b) = a"
     8.6    by simp
     8.7 -  
     8.8 +
     8.9 +lemma add_le_imp_le_diff: 
    8.10 +  shows "i + k \<le> n \<Longrightarrow> i \<le> n - k"
    8.11 +  apply (subst add_le_cancel_right [where c=k, symmetric])
    8.12 +  apply (frule le_add_diff_inverse2)
    8.13 +  apply (simp only: add.assoc [symmetric])
    8.14 +  using add_implies_diff by fastforce
    8.15 +
    8.16 +lemma add_le_add_imp_diff_le: 
    8.17 +  assumes a1: "i + k \<le> n"
    8.18 +      and a2: "n \<le> j + k"
    8.19 +  shows "\<lbrakk>i + k \<le> n; n \<le> j + k\<rbrakk> \<Longrightarrow> n - k \<le> j"
    8.20 +proof -
    8.21 +  have "n - (i + k) + (i + k) = n"
    8.22 +    using a1 by simp
    8.23 +  moreover have "n - k = n - k - i + i"
    8.24 +    using a1 by (simp add: add_le_imp_le_diff)
    8.25 +  ultimately show ?thesis
    8.26 +    using a2
    8.27 +    apply (simp add: add.assoc [symmetric])
    8.28 +    apply (rule add_le_imp_le_diff [of _ k "j+k", simplified add_diff_cancel_right'])
    8.29 +    by (simp add: add.commute diff_diff_add)
    8.30 +qed
    8.31 +
    8.32  lemma pos_add_strict:
    8.33    shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
    8.34    using add_strict_mono [of 0 a b c] by simp
     9.1 --- a/src/HOL/Set_Interval.thy	Mon Jun 29 13:49:21 2015 +0200
     9.2 +++ b/src/HOL/Set_Interval.thy	Tue Jun 30 13:56:16 2015 +0100
     9.3 @@ -810,15 +810,25 @@
     9.4  subsubsection {* Image *}
     9.5  
     9.6  lemma image_add_atLeastAtMost:
     9.7 -  "(%n::nat. n+k) ` {i..j} = {i+k..j+k}" (is "?A = ?B")
     9.8 +  fixes k ::"'a::linordered_semidom"
     9.9 +  shows "(\<lambda>n. n+k) ` {i..j} = {i+k..j+k}" (is "?A = ?B")
    9.10  proof
    9.11    show "?A \<subseteq> ?B" by auto
    9.12  next
    9.13    show "?B \<subseteq> ?A"
    9.14    proof
    9.15      fix n assume a: "n : ?B"
    9.16 -    hence "n - k : {i..j}" by auto
    9.17 -    moreover have "n = (n - k) + k" using a by auto
    9.18 +    hence "n - k : {i..j}"
    9.19 +      by (auto simp: add_le_imp_le_diff add_le_add_imp_diff_le)
    9.20 +    moreover have "n = (n - k) + k" using a
    9.21 +    proof -
    9.22 +      have "k + i \<le> n"
    9.23 +        by (metis a add.commute atLeastAtMost_iff)
    9.24 +      hence "k + (n - k) = n"
    9.25 +        by (metis (no_types) ab_semigroup_add_class.add_ac(1) add_diff_cancel_left' le_add_diff_inverse)
    9.26 +      thus ?thesis
    9.27 +        by (simp add: add.commute)
    9.28 +    qed
    9.29      ultimately show "n : ?A" by blast
    9.30    qed
    9.31  qed