src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
changeset 63957 c3da799b1b45
parent 63956 b235e845c8e8
child 64267 b9a1486e79be
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Sep 28 16:15:51 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Sep 29 13:02:43 2016 +0200
     1.3 @@ -6,201 +6,49 @@
     1.4  
     1.5  theory Henstock_Kurzweil_Integration
     1.6  imports
     1.7 -  Lebesgue_Measure
     1.8 +  Lebesgue_Measure Tagged_Division
     1.9  begin
    1.10  
    1.11 -lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
    1.12 -  scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
    1.13 -  scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
    1.14 -
    1.15 -
    1.16 -subsection \<open>Sundries\<close>
    1.17 -
    1.18 -
    1.19 -text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
    1.20 -lemma wf_finite_segments:
    1.21 -  assumes "irrefl r" and "trans r" and "\<And>x. finite {y. (y, x) \<in> r}"
    1.22 -  shows "wf (r)"
    1.23 -  apply (simp add: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
    1.24 -  using acyclic_def assms irrefl_def trans_Restr by fastforce
    1.25 -
    1.26 -text\<open>For creating values between @{term u} and @{term v}.\<close>
    1.27 -lemma scaling_mono:
    1.28 -  fixes u::"'a::linordered_field"
    1.29 -  assumes "u \<le> v" "0 \<le> r" "r \<le> s"
    1.30 -    shows "u + r * (v - u) / s \<le> v"
    1.31 +(* BEGIN MOVE *)
    1.32 +lemma swap_continuous:
    1.33 +  assumes "continuous_on (cbox (a,c) (b,d)) (\<lambda>(x,y). f x y)"
    1.34 +    shows "continuous_on (cbox (c,a) (d,b)) (\<lambda>(x, y). f y x)"
    1.35  proof -
    1.36 -  have "r/s \<le> 1" using assms
    1.37 -    using divide_le_eq_1 by fastforce
    1.38 -  then have "(r/s) * (v - u) \<le> 1 * (v - u)"
    1.39 -    by (meson diff_ge_0_iff_ge mult_right_mono \<open>u \<le> v\<close>)
    1.40 +  have "(\<lambda>(x, y). f y x) = (\<lambda>(x, y). f x y) \<circ> prod.swap"
    1.41 +    by auto
    1.42    then show ?thesis
    1.43 -    by (simp add: field_simps)
    1.44 +    apply (rule ssubst)
    1.45 +    apply (rule continuous_on_compose)
    1.46 +    apply (simp add: split_def)
    1.47 +    apply (rule continuous_intros | simp add: assms)+
    1.48 +    done
    1.49  qed
    1.50  
    1.51 -lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
    1.52 -lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
    1.53 -lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
    1.54 -
    1.55 -lemma cond_cases: "(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)"
    1.56 +
    1.57 +lemma norm_minus2: "norm (x1-x2, y1-y2) = norm (x2-x1, y2-y1)"
    1.58 +  by (simp add: norm_minus_eqI)
    1.59 +
    1.60 +lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
    1.61 +  \<Longrightarrow> norm(y - x) \<le> e"
    1.62 +  using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"]
    1.63 +  by (simp add: add_diff_add)
    1.64 +
    1.65 +lemma setcomp_dot1: "{z. P (z \<bullet> (i,0))} = {(x,y). P(x \<bullet> i)}"
    1.66    by auto
    1.67  
    1.68 -declare norm_triangle_ineq4[intro]
    1.69 -
    1.70 -lemma transitive_stepwise_le:
    1.71 -  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" and "\<And>n. R n (Suc n)"
    1.72 -  shows "\<forall>n\<ge>m. R m n"
    1.73 -proof (intro allI impI)
    1.74 -  show "m \<le> n \<Longrightarrow> R m n" for n
    1.75 -    by (induction rule: dec_induct)
    1.76 -       (use assms in blast)+
    1.77 -qed
    1.78 -
    1.79 -subsection \<open>Some useful lemmas about intervals.\<close>
    1.80 +lemma setcomp_dot2: "{z. P (z \<bullet> (0,i))} = {(x,y). P(y \<bullet> i)}"
    1.81 +  by auto
    1.82 +
    1.83 +lemma Sigma_Int_Paircomp1: "(Sigma A B) \<inter> {(x, y). P x} = Sigma (A \<inter> {x. P x}) B"
    1.84 +  by blast
    1.85 +
    1.86 +lemma Sigma_Int_Paircomp2: "(Sigma A B) \<inter> {(x, y). P y} = Sigma A (\<lambda>z. B z \<inter> {y. P y})"
    1.87 +  by blast
    1.88  
    1.89  lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
    1.90    using nonempty_Basis
    1.91    by (fastforce simp add: set_eq_iff mem_box)
    1.92 -
    1.93 -lemma interior_subset_union_intervals:
    1.94 -  assumes "i = cbox a b"
    1.95 -    and "j = cbox c d"
    1.96 -    and "interior j \<noteq> {}"
    1.97 -    and "i \<subseteq> j \<union> s"
    1.98 -    and "interior i \<inter> interior j = {}"
    1.99 -  shows "interior i \<subseteq> interior s"
   1.100 -proof -
   1.101 -  have "box a b \<inter> cbox c d = {}"
   1.102 -     using inter_interval_mixed_eq_empty[of c d a b] and assms(3,5)
   1.103 -     unfolding assms(1,2) interior_cbox by auto
   1.104 -  moreover
   1.105 -  have "box a b \<subseteq> cbox c d \<union> s"
   1.106 -    apply (rule order_trans,rule box_subset_cbox)
   1.107 -    using assms(4) unfolding assms(1,2)
   1.108 -    apply auto
   1.109 -    done
   1.110 -  ultimately
   1.111 -  show ?thesis
   1.112 -    unfolding assms interior_cbox
   1.113 -      by auto (metis IntI UnE empty_iff interior_maximal open_box subsetCE subsetI)
   1.114 -qed
   1.115 -
   1.116 -lemma interior_Union_subset_cbox:
   1.117 -  assumes "finite f"
   1.118 -  assumes f: "\<And>s. s \<in> f \<Longrightarrow> \<exists>a b. s = cbox a b" "\<And>s. s \<in> f \<Longrightarrow> interior s \<subseteq> t"
   1.119 -    and t: "closed t"
   1.120 -  shows "interior (\<Union>f) \<subseteq> t"
   1.121 -proof -
   1.122 -  have [simp]: "s \<in> f \<Longrightarrow> closed s" for s
   1.123 -    using f by auto
   1.124 -  define E where "E = {s\<in>f. interior s = {}}"
   1.125 -  then have "finite E" "E \<subseteq> {s\<in>f. interior s = {}}"
   1.126 -    using \<open>finite f\<close> by auto
   1.127 -  then have "interior (\<Union>f) = interior (\<Union>(f - E))"
   1.128 -  proof (induction E rule: finite_subset_induct')
   1.129 -    case (insert s f')
   1.130 -    have "interior (\<Union>(f - insert s f') \<union> s) = interior (\<Union>(f - insert s f'))"
   1.131 -      using insert.hyps \<open>finite f\<close> by (intro interior_closed_Un_empty_interior) auto
   1.132 -    also have "\<Union>(f - insert s f') \<union> s = \<Union>(f - f')"
   1.133 -      using insert.hyps by auto
   1.134 -    finally show ?case
   1.135 -      by (simp add: insert.IH)
   1.136 -  qed simp
   1.137 -  also have "\<dots> \<subseteq> \<Union>(f - E)"
   1.138 -    by (rule interior_subset)
   1.139 -  also have "\<dots> \<subseteq> t"
   1.140 -  proof (rule Union_least)
   1.141 -    fix s assume "s \<in> f - E"
   1.142 -    with f[of s] obtain a b where s: "s \<in> f" "s = cbox a b" "box a b \<noteq> {}"
   1.143 -      by (fastforce simp: E_def)
   1.144 -    have "closure (interior s) \<subseteq> closure t"
   1.145 -      by (intro closure_mono f \<open>s \<in> f\<close>)
   1.146 -    with s \<open>closed t\<close> show "s \<subseteq> t"
   1.147 -      by (simp add: closure_box)
   1.148 -  qed
   1.149 -  finally show ?thesis .
   1.150 -qed
   1.151 -
   1.152 -lemma inter_interior_unions_intervals:
   1.153 -    "finite f \<Longrightarrow> open s \<Longrightarrow> \<forall>t\<in>f. \<exists>a b. t = cbox a b \<Longrightarrow> \<forall>t\<in>f. s \<inter> (interior t) = {} \<Longrightarrow> s \<inter> interior (\<Union>f) = {}"
   1.154 -  using interior_Union_subset_cbox[of f "UNIV - s"] by auto
   1.155 -
   1.156 -lemma interval_split:
   1.157 -  fixes a :: "'a::euclidean_space"
   1.158 -  assumes "k \<in> Basis"
   1.159 -  shows
   1.160 -    "cbox a b \<inter> {x. x\<bullet>k \<le> c} = cbox a (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) c else b\<bullet>i) *\<^sub>R i)"
   1.161 -    "cbox a b \<inter> {x. x\<bullet>k \<ge> c} = cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) c else a\<bullet>i) *\<^sub>R i) b"
   1.162 -  apply (rule_tac[!] set_eqI)
   1.163 -  unfolding Int_iff mem_box mem_Collect_eq
   1.164 -  using assms
   1.165 -  apply auto
   1.166 -  done
   1.167 -
   1.168 -lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
   1.169 -  by (simp add: box_ne_empty)
   1.170 -
   1.171 -subsection \<open>Bounds on intervals where they exist.\<close>
   1.172 -
   1.173 -definition interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
   1.174 -  where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
   1.175 -
   1.176 -definition interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
   1.177 -  where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
   1.178 -
   1.179 -lemma interval_upperbound[simp]:
   1.180 -  "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
   1.181 -    interval_upperbound (cbox a b) = (b::'a::euclidean_space)"
   1.182 -  unfolding interval_upperbound_def euclidean_representation_setsum cbox_def
   1.183 -  by (safe intro!: cSup_eq) auto
   1.184 -
   1.185 -lemma interval_lowerbound[simp]:
   1.186 -  "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
   1.187 -    interval_lowerbound (cbox a b) = (a::'a::euclidean_space)"
   1.188 -  unfolding interval_lowerbound_def euclidean_representation_setsum cbox_def
   1.189 -  by (safe intro!: cInf_eq) auto
   1.190 -
   1.191 -lemmas interval_bounds = interval_upperbound interval_lowerbound
   1.192 -
   1.193 -lemma
   1.194 -  fixes X::"real set"
   1.195 -  shows interval_upperbound_real[simp]: "interval_upperbound X = Sup X"
   1.196 -    and interval_lowerbound_real[simp]: "interval_lowerbound X = Inf X"
   1.197 -  by (auto simp: interval_upperbound_def interval_lowerbound_def)
   1.198 -
   1.199 -lemma interval_bounds'[simp]:
   1.200 -  assumes "cbox a b \<noteq> {}"
   1.201 -  shows "interval_upperbound (cbox a b) = b"
   1.202 -    and "interval_lowerbound (cbox a b) = a"
   1.203 -  using assms unfolding box_ne_empty by auto
   1.204 -
   1.205 -lemma interval_upperbound_Times:
   1.206 -  assumes "A \<noteq> {}" and "B \<noteq> {}"
   1.207 -  shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)"
   1.208 -proof-
   1.209 -  from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
   1.210 -  have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:A. x \<bullet> i) *\<^sub>R i)"
   1.211 -      by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
   1.212 -  moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
   1.213 -  have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:B. x \<bullet> i) *\<^sub>R i)"
   1.214 -      by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
   1.215 -  ultimately show ?thesis unfolding interval_upperbound_def
   1.216 -      by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
   1.217 -qed
   1.218 -
   1.219 -lemma interval_lowerbound_Times:
   1.220 -  assumes "A \<noteq> {}" and "B \<noteq> {}"
   1.221 -  shows "interval_lowerbound (A \<times> B) = (interval_lowerbound A, interval_lowerbound B)"
   1.222 -proof-
   1.223 -  from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
   1.224 -  have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:A. x \<bullet> i) *\<^sub>R i)"
   1.225 -      by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
   1.226 -  moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
   1.227 -  have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:B. x \<bullet> i) *\<^sub>R i)"
   1.228 -      by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
   1.229 -  ultimately show ?thesis unfolding interval_lowerbound_def
   1.230 -      by (subst setsum_Basis_prod_eq) (auto simp add: setsum_prod)
   1.231 -qed
   1.232 +(* END MOVE *)
   1.233  
   1.234  subsection \<open>Content (length, area, volume...) of an interval.\<close>
   1.235  
   1.236 @@ -322,1508 +170,34 @@
   1.237      by (auto simp: not_le)
   1.238  qed
   1.239  
   1.240 -subsection \<open>The notion of a gauge --- simply an open set containing the point.\<close>
   1.241 -
   1.242 -definition "gauge d \<longleftrightarrow> (\<forall>x. x \<in> d x \<and> open (d x))"
   1.243 -
   1.244 -lemma gaugeI:
   1.245 -  assumes "\<And>x. x \<in> g x"
   1.246 -    and "\<And>x. open (g x)"
   1.247 -  shows "gauge g"
   1.248 -  using assms unfolding gauge_def by auto
   1.249 -
   1.250 -lemma gaugeD[dest]:
   1.251 -  assumes "gauge d"
   1.252 -  shows "x \<in> d x"
   1.253 -    and "open (d x)"
   1.254 -  using assms unfolding gauge_def by auto
   1.255 -
   1.256 -lemma gauge_ball_dependent: "\<forall>x. 0 < e x \<Longrightarrow> gauge (\<lambda>x. ball x (e x))"
   1.257 -  unfolding gauge_def by auto
   1.258 -
   1.259 -lemma gauge_ball[intro]: "0 < e \<Longrightarrow> gauge (\<lambda>x. ball x e)"
   1.260 -  unfolding gauge_def by auto
   1.261 -
   1.262 -lemma gauge_trivial[intro!]: "gauge (\<lambda>x. ball x 1)"
   1.263 -  by (rule gauge_ball) auto
   1.264 -
   1.265 -lemma gauge_inter[intro]: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. d1 x \<inter> d2 x)"
   1.266 -  unfolding gauge_def by auto
   1.267 -
   1.268 -lemma gauge_inters:
   1.269 -  assumes "finite s"
   1.270 -    and "\<forall>d\<in>s. gauge (f d)"
   1.271 -  shows "gauge (\<lambda>x. \<Inter>{f d x | d. d \<in> s})"
   1.272 -proof -
   1.273 -  have *: "\<And>x. {f d x |d. d \<in> s} = (\<lambda>d. f d x) ` s"
   1.274 -    by auto
   1.275 -  show ?thesis
   1.276 -    unfolding gauge_def unfolding *
   1.277 -    using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto
   1.278 -qed
   1.279 -
   1.280 -lemma gauge_existence_lemma:
   1.281 -  "(\<forall>x. \<exists>d :: real. p x \<longrightarrow> 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. p x \<longrightarrow> q d x)"
   1.282 -  by (metis zero_less_one)
   1.283 -
   1.284 -
   1.285 -subsection \<open>Divisions.\<close>
   1.286 -
   1.287 -definition division_of (infixl "division'_of" 40)
   1.288 -where
   1.289 -  "s division_of i \<longleftrightarrow>
   1.290 -    finite s \<and>
   1.291 -    (\<forall>k\<in>s. k \<subseteq> i \<and> k \<noteq> {} \<and> (\<exists>a b. k = cbox a b)) \<and>
   1.292 -    (\<forall>k1\<in>s. \<forall>k2\<in>s. k1 \<noteq> k2 \<longrightarrow> interior(k1) \<inter> interior(k2) = {}) \<and>
   1.293 -    (\<Union>s = i)"
   1.294 -
   1.295 -lemma division_ofD[dest]:
   1.296 -  assumes "s division_of i"
   1.297 -  shows "finite s"
   1.298 -    and "\<And>k. k \<in> s \<Longrightarrow> k \<subseteq> i"
   1.299 -    and "\<And>k. k \<in> s \<Longrightarrow> k \<noteq> {}"
   1.300 -    and "\<And>k. k \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
   1.301 -    and "\<And>k1 k2. k1 \<in> s \<Longrightarrow> k2 \<in> s \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior(k1) \<inter> interior(k2) = {}"
   1.302 -    and "\<Union>s = i"
   1.303 -  using assms unfolding division_of_def by auto
   1.304 -
   1.305 -lemma division_ofI:
   1.306 -  assumes "finite s"
   1.307 -    and "\<And>k. k \<in> s \<Longrightarrow> k \<subseteq> i"
   1.308 -    and "\<And>k. k \<in> s \<Longrightarrow> k \<noteq> {}"
   1.309 -    and "\<And>k. k \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
   1.310 -    and "\<And>k1 k2. k1 \<in> s \<Longrightarrow> k2 \<in> s \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
   1.311 -    and "\<Union>s = i"
   1.312 -  shows "s division_of i"
   1.313 -  using assms unfolding division_of_def by auto
   1.314 -
   1.315 -lemma division_of_finite: "s division_of i \<Longrightarrow> finite s"
   1.316 -  unfolding division_of_def by auto
   1.317 -
   1.318 -lemma division_of_self[intro]: "cbox a b \<noteq> {} \<Longrightarrow> {cbox a b} division_of (cbox a b)"
   1.319 -  unfolding division_of_def by auto
   1.320 -
   1.321 -lemma division_of_trivial[simp]: "s division_of {} \<longleftrightarrow> s = {}"
   1.322 -  unfolding division_of_def by auto
   1.323 -
   1.324 -lemma division_of_sing[simp]:
   1.325 -  "s division_of cbox a (a::'a::euclidean_space) \<longleftrightarrow> s = {cbox a a}"
   1.326 -  (is "?l = ?r")
   1.327 -proof
   1.328 -  assume ?r
   1.329 -  moreover
   1.330 -  { fix k
   1.331 -    assume "s = {{a}}" "k\<in>s"
   1.332 -    then have "\<exists>x y. k = cbox x y"
   1.333 -      apply (rule_tac x=a in exI)+
   1.334 -      apply (force simp: cbox_sing)
   1.335 -      done
   1.336 -  }
   1.337 -  ultimately show ?l
   1.338 -    unfolding division_of_def cbox_sing by auto
   1.339 -next
   1.340 -  assume ?l
   1.341 -  note * = conjunctD4[OF this[unfolded division_of_def cbox_sing]]
   1.342 -  {
   1.343 -    fix x
   1.344 -    assume x: "x \<in> s" have "x = {a}"
   1.345 -      using *(2)[rule_format,OF x] by auto
   1.346 -  }
   1.347 -  moreover have "s \<noteq> {}"
   1.348 -    using *(4) by auto
   1.349 -  ultimately show ?r
   1.350 -    unfolding cbox_sing by auto
   1.351 -qed
   1.352 -
   1.353 -lemma elementary_empty: obtains p where "p division_of {}"
   1.354 -  unfolding division_of_trivial by auto
   1.355 -
   1.356 -lemma elementary_interval: obtains p where "p division_of (cbox a b)"
   1.357 -  by (metis division_of_trivial division_of_self)
   1.358 -
   1.359 -lemma division_contains: "s division_of i \<Longrightarrow> \<forall>x\<in>i. \<exists>k\<in>s. x \<in> k"
   1.360 -  unfolding division_of_def by auto
   1.361 -
   1.362 -lemma forall_in_division:
   1.363 -  "d division_of i \<Longrightarrow> (\<forall>x\<in>d. P x) \<longleftrightarrow> (\<forall>a b. cbox a b \<in> d \<longrightarrow> P (cbox a b))"
   1.364 -  unfolding division_of_def by fastforce
   1.365 -
   1.366 -lemma division_of_subset:
   1.367 -  assumes "p division_of (\<Union>p)"
   1.368 -    and "q \<subseteq> p"
   1.369 -  shows "q division_of (\<Union>q)"
   1.370 -proof (rule division_ofI)
   1.371 -  note * = division_ofD[OF assms(1)]
   1.372 -  show "finite q"
   1.373 -    using "*"(1) assms(2) infinite_super by auto
   1.374 -  {
   1.375 -    fix k
   1.376 -    assume "k \<in> q"
   1.377 -    then have kp: "k \<in> p"
   1.378 -      using assms(2) by auto
   1.379 -    show "k \<subseteq> \<Union>q"
   1.380 -      using \<open>k \<in> q\<close> by auto
   1.381 -    show "\<exists>a b. k = cbox a b"
   1.382 -      using *(4)[OF kp] by auto
   1.383 -    show "k \<noteq> {}"
   1.384 -      using *(3)[OF kp] by auto
   1.385 -  }
   1.386 -  fix k1 k2
   1.387 -  assume "k1 \<in> q" "k2 \<in> q" "k1 \<noteq> k2"
   1.388 -  then have **: "k1 \<in> p" "k2 \<in> p" "k1 \<noteq> k2"
   1.389 -    using assms(2) by auto
   1.390 -  show "interior k1 \<inter> interior k2 = {}"
   1.391 -    using *(5)[OF **] by auto
   1.392 -qed auto
   1.393 -
   1.394 -lemma division_of_union_self[intro]: "p division_of s \<Longrightarrow> p division_of (\<Union>p)"
   1.395 -  unfolding division_of_def by auto
   1.396 -
   1.397  lemma division_of_content_0:
   1.398    assumes "content (cbox a b) = 0" "d division_of (cbox a b)"
   1.399    shows "\<forall>k\<in>d. content k = 0"
   1.400    unfolding forall_in_division[OF assms(2)]
   1.401    by (metis antisym_conv assms content_pos_le content_subset division_ofD(2))
   1.402  
   1.403 -lemma division_inter:
   1.404 -  fixes s1 s2 :: "'a::euclidean_space set"
   1.405 -  assumes "p1 division_of s1"
   1.406 -    and "p2 division_of s2"
   1.407 -  shows "{k1 \<inter> k2 | k1 k2. k1 \<in> p1 \<and> k2 \<in> p2 \<and> k1 \<inter> k2 \<noteq> {}} division_of (s1 \<inter> s2)"
   1.408 -  (is "?A' division_of _")
   1.409 -proof -
   1.410 -  let ?A = "{s. s \<in>  (\<lambda>(k1,k2). k1 \<inter> k2) ` (p1 \<times> p2) \<and> s \<noteq> {}}"
   1.411 -  have *: "?A' = ?A" by auto
   1.412 -  show ?thesis
   1.413 -    unfolding *
   1.414 -  proof (rule division_ofI)
   1.415 -    have "?A \<subseteq> (\<lambda>(x, y). x \<inter> y) ` (p1 \<times> p2)"
   1.416 -      by auto
   1.417 -    moreover have "finite (p1 \<times> p2)"
   1.418 -      using assms unfolding division_of_def by auto
   1.419 -    ultimately show "finite ?A" by auto
   1.420 -    have *: "\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s"
   1.421 -      by auto
   1.422 -    show "\<Union>?A = s1 \<inter> s2"
   1.423 -      apply (rule set_eqI)
   1.424 -      unfolding * and UN_iff
   1.425 -      using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)]
   1.426 -      apply auto
   1.427 -      done
   1.428 -    {
   1.429 -      fix k
   1.430 -      assume "k \<in> ?A"
   1.431 -      then obtain k1 k2 where k: "k = k1 \<inter> k2" "k1 \<in> p1" "k2 \<in> p2" "k \<noteq> {}"
   1.432 -        by auto
   1.433 -      then show "k \<noteq> {}"
   1.434 -        by auto
   1.435 -      show "k \<subseteq> s1 \<inter> s2"
   1.436 -        using division_ofD(2)[OF assms(1) k(2)] and division_ofD(2)[OF assms(2) k(3)]
   1.437 -        unfolding k by auto
   1.438 -      obtain a1 b1 where k1: "k1 = cbox a1 b1"
   1.439 -        using division_ofD(4)[OF assms(1) k(2)] by blast
   1.440 -      obtain a2 b2 where k2: "k2 = cbox a2 b2"
   1.441 -        using division_ofD(4)[OF assms(2) k(3)] by blast
   1.442 -      show "\<exists>a b. k = cbox a b"
   1.443 -        unfolding k k1 k2 unfolding Int_interval by auto
   1.444 -    }
   1.445 -    fix k1 k2
   1.446 -    assume "k1 \<in> ?A"
   1.447 -    then obtain x1 y1 where k1: "k1 = x1 \<inter> y1" "x1 \<in> p1" "y1 \<in> p2" "k1 \<noteq> {}"
   1.448 -      by auto
   1.449 -    assume "k2 \<in> ?A"
   1.450 -    then obtain x2 y2 where k2: "k2 = x2 \<inter> y2" "x2 \<in> p1" "y2 \<in> p2" "k2 \<noteq> {}"
   1.451 -      by auto
   1.452 -    assume "k1 \<noteq> k2"
   1.453 -    then have th: "x1 \<noteq> x2 \<or> y1 \<noteq> y2"
   1.454 -      unfolding k1 k2 by auto
   1.455 -    have *: "interior x1 \<inter> interior x2 = {} \<or> interior y1 \<inter> interior y2 = {} \<Longrightarrow>
   1.456 -      interior (x1 \<inter> y1) \<subseteq> interior x1 \<Longrightarrow> interior (x1 \<inter> y1) \<subseteq> interior y1 \<Longrightarrow>
   1.457 -      interior (x2 \<inter> y2) \<subseteq> interior x2 \<Longrightarrow> interior (x2 \<inter> y2) \<subseteq> interior y2 \<Longrightarrow>
   1.458 -      interior (x1 \<inter> y1) \<inter> interior (x2 \<inter> y2) = {}" by auto
   1.459 -    show "interior k1 \<inter> interior k2 = {}"
   1.460 -      unfolding k1 k2
   1.461 -      apply (rule *)
   1.462 -      using assms division_ofD(5) k1 k2(2) k2(3) th apply auto
   1.463 -      done
   1.464 -  qed
   1.465 -qed
   1.466 -
   1.467 -lemma division_inter_1:
   1.468 -  assumes "d division_of i"
   1.469 -    and "cbox a (b::'a::euclidean_space) \<subseteq> i"
   1.470 -  shows "{cbox a b \<inter> k | k. k \<in> d \<and> cbox a b \<inter> k \<noteq> {}} division_of (cbox a b)"
   1.471 -proof (cases "cbox a b = {}")
   1.472 -  case True
   1.473 -  show ?thesis
   1.474 -    unfolding True and division_of_trivial by auto
   1.475 -next
   1.476 -  case False
   1.477 -  have *: "cbox a b \<inter> i = cbox a b" using assms(2) by auto
   1.478 -  show ?thesis
   1.479 -    using division_inter[OF division_of_self[OF False] assms(1)]
   1.480 -    unfolding * by auto
   1.481 -qed
   1.482 -
   1.483 -lemma elementary_inter:
   1.484 -  fixes s t :: "'a::euclidean_space set"
   1.485 -  assumes "p1 division_of s"
   1.486 -    and "p2 division_of t"
   1.487 -  shows "\<exists>p. p division_of (s \<inter> t)"
   1.488 -using assms division_inter by blast
   1.489 -
   1.490 -lemma elementary_inters:
   1.491 -  assumes "finite f"
   1.492 -    and "f \<noteq> {}"
   1.493 -    and "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::euclidean_space) set)"
   1.494 -  shows "\<exists>p. p division_of (\<Inter>f)"
   1.495 -  using assms
   1.496 -proof (induct f rule: finite_induct)
   1.497 -  case (insert x f)
   1.498 -  show ?case
   1.499 -  proof (cases "f = {}")
   1.500 -    case True
   1.501 -    then show ?thesis
   1.502 -      unfolding True using insert by auto
   1.503 -  next
   1.504 -    case False
   1.505 -    obtain p where "p division_of \<Inter>f"
   1.506 -      using insert(3)[OF False insert(5)[unfolded ball_simps,THEN conjunct2]] ..
   1.507 -    moreover obtain px where "px division_of x"
   1.508 -      using insert(5)[rule_format,OF insertI1] ..
   1.509 -    ultimately show ?thesis
   1.510 -      by (simp add: elementary_inter Inter_insert)
   1.511 -  qed
   1.512 -qed auto
   1.513 -
   1.514 -lemma division_disjoint_union:
   1.515 -  assumes "p1 division_of s1"
   1.516 -    and "p2 division_of s2"
   1.517 -    and "interior s1 \<inter> interior s2 = {}"
   1.518 -  shows "(p1 \<union> p2) division_of (s1 \<union> s2)"
   1.519 -proof (rule division_ofI)
   1.520 -  note d1 = division_ofD[OF assms(1)]
   1.521 -  note d2 = division_ofD[OF assms(2)]
   1.522 -  show "finite (p1 \<union> p2)"
   1.523 -    using d1(1) d2(1) by auto
   1.524 -  show "\<Union>(p1 \<union> p2) = s1 \<union> s2"
   1.525 -    using d1(6) d2(6) by auto
   1.526 -  {
   1.527 -    fix k1 k2
   1.528 -    assume as: "k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2"
   1.529 -    moreover
   1.530 -    let ?g="interior k1 \<inter> interior k2 = {}"
   1.531 -    {
   1.532 -      assume as: "k1\<in>p1" "k2\<in>p2"
   1.533 -      have ?g
   1.534 -        using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
   1.535 -        using assms(3) by blast
   1.536 -    }
   1.537 -    moreover
   1.538 -    {
   1.539 -      assume as: "k1\<in>p2" "k2\<in>p1"
   1.540 -      have ?g
   1.541 -        using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
   1.542 -        using assms(3) by blast
   1.543 -    }
   1.544 -    ultimately show ?g
   1.545 -      using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto
   1.546 -  }
   1.547 -  fix k
   1.548 -  assume k: "k \<in> p1 \<union> p2"
   1.549 -  show "k \<subseteq> s1 \<union> s2"
   1.550 -    using k d1(2) d2(2) by auto
   1.551 -  show "k \<noteq> {}"
   1.552 -    using k d1(3) d2(3) by auto
   1.553 -  show "\<exists>a b. k = cbox a b"
   1.554 -    using k d1(4) d2(4) by auto
   1.555 -qed
   1.556 -
   1.557 -lemma partial_division_extend_1:
   1.558 -  fixes a b c d :: "'a::euclidean_space"
   1.559 -  assumes incl: "cbox c d \<subseteq> cbox a b"
   1.560 -    and nonempty: "cbox c d \<noteq> {}"
   1.561 -  obtains p where "p division_of (cbox a b)" "cbox c d \<in> p"
   1.562 -proof
   1.563 -  let ?B = "\<lambda>f::'a\<Rightarrow>'a \<times> 'a.
   1.564 -    cbox (\<Sum>i\<in>Basis. (fst (f i) \<bullet> i) *\<^sub>R i) (\<Sum>i\<in>Basis. (snd (f i) \<bullet> i) *\<^sub>R i)"
   1.565 -  define p where "p = ?B ` (Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)})"
   1.566 -
   1.567 -  show "cbox c d \<in> p"
   1.568 -    unfolding p_def
   1.569 -    by (auto simp add: box_eq_empty cbox_def intro!: image_eqI[where x="\<lambda>(i::'a)\<in>Basis. (c, d)"])
   1.570 -  {
   1.571 -    fix i :: 'a
   1.572 -    assume "i \<in> Basis"
   1.573 -    with incl nonempty have "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> d \<bullet> i" "d \<bullet> i \<le> b \<bullet> i"
   1.574 -      unfolding box_eq_empty subset_box by (auto simp: not_le)
   1.575 -  }
   1.576 -  note ord = this
   1.577 -
   1.578 -  show "p division_of (cbox a b)"
   1.579 -  proof (rule division_ofI)
   1.580 -    show "finite p"
   1.581 -      unfolding p_def by (auto intro!: finite_PiE)
   1.582 -    {
   1.583 -      fix k
   1.584 -      assume "k \<in> p"
   1.585 -      then obtain f where f: "f \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and k: "k = ?B f"
   1.586 -        by (auto simp: p_def)
   1.587 -      then show "\<exists>a b. k = cbox a b"
   1.588 -        by auto
   1.589 -      have "k \<subseteq> cbox a b \<and> k \<noteq> {}"
   1.590 -      proof (simp add: k box_eq_empty subset_box not_less, safe)
   1.591 -        fix i :: 'a
   1.592 -        assume i: "i \<in> Basis"
   1.593 -        with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
   1.594 -          by (auto simp: PiE_iff)
   1.595 -        with i ord[of i]
   1.596 -        show "a \<bullet> i \<le> fst (f i) \<bullet> i" "snd (f i) \<bullet> i \<le> b \<bullet> i" "fst (f i) \<bullet> i \<le> snd (f i) \<bullet> i"
   1.597 -          by auto
   1.598 -      qed
   1.599 -      then show "k \<noteq> {}" "k \<subseteq> cbox a b"
   1.600 -        by auto
   1.601 -      {
   1.602 -        fix l
   1.603 -        assume "l \<in> p"
   1.604 -        then obtain g where g: "g \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}" and l: "l = ?B g"
   1.605 -          by (auto simp: p_def)
   1.606 -        assume "l \<noteq> k"
   1.607 -        have "\<exists>i\<in>Basis. f i \<noteq> g i"
   1.608 -        proof (rule ccontr)
   1.609 -          assume "\<not> ?thesis"
   1.610 -          with f g have "f = g"
   1.611 -            by (auto simp: PiE_iff extensional_def intro!: ext)
   1.612 -          with \<open>l \<noteq> k\<close> show False
   1.613 -            by (simp add: l k)
   1.614 -        qed
   1.615 -        then obtain i where *: "i \<in> Basis" "f i \<noteq> g i" ..
   1.616 -        then have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
   1.617 -                  "g i = (a, c) \<or> g i = (c, d) \<or> g i = (d, b)"
   1.618 -          using f g by (auto simp: PiE_iff)
   1.619 -        with * ord[of i] show "interior l \<inter> interior k = {}"
   1.620 -          by (auto simp add: l k interior_cbox disjoint_interval intro!: bexI[of _ i])
   1.621 -      }
   1.622 -      note \<open>k \<subseteq> cbox a b\<close>
   1.623 -    }
   1.624 -    moreover
   1.625 -    {
   1.626 -      fix x assume x: "x \<in> cbox a b"
   1.627 -      have "\<forall>i\<in>Basis. \<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}"
   1.628 -      proof
   1.629 -        fix i :: 'a
   1.630 -        assume "i \<in> Basis"
   1.631 -        with x ord[of i]
   1.632 -        have "(a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> c \<bullet> i) \<or> (c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i) \<or>
   1.633 -            (d \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i)"
   1.634 -          by (auto simp: cbox_def)
   1.635 -        then show "\<exists>l. x \<bullet> i \<in> {fst l \<bullet> i .. snd l \<bullet> i} \<and> l \<in> {(a, c), (c, d), (d, b)}"
   1.636 -          by auto
   1.637 -      qed
   1.638 -      then obtain f where
   1.639 -        f: "\<forall>i\<in>Basis. x \<bullet> i \<in> {fst (f i) \<bullet> i..snd (f i) \<bullet> i} \<and> f i \<in> {(a, c), (c, d), (d, b)}"
   1.640 -        unfolding bchoice_iff ..
   1.641 -      moreover from f have "restrict f Basis \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}"
   1.642 -        by auto
   1.643 -      moreover from f have "x \<in> ?B (restrict f Basis)"
   1.644 -        by (auto simp: mem_box)
   1.645 -      ultimately have "\<exists>k\<in>p. x \<in> k"
   1.646 -        unfolding p_def by blast
   1.647 -    }
   1.648 -    ultimately show "\<Union>p = cbox a b"
   1.649 -      by auto
   1.650 -  qed
   1.651 -qed
   1.652 -
   1.653 -lemma partial_division_extend_interval:
   1.654 -  assumes "p division_of (\<Union>p)" "(\<Union>p) \<subseteq> cbox a b"
   1.655 -  obtains q where "p \<subseteq> q" "q division_of cbox a (b::'a::euclidean_space)"
   1.656 -proof (cases "p = {}")
   1.657 -  case True
   1.658 -  obtain q where "q division_of (cbox a b)"
   1.659 -    by (rule elementary_interval)
   1.660 -  then show ?thesis
   1.661 -    using True that by blast
   1.662 -next
   1.663 -  case False
   1.664 -  note p = division_ofD[OF assms(1)]
   1.665 -  have div_cbox: "\<forall>k\<in>p. \<exists>q. q division_of cbox a b \<and> k \<in> q"
   1.666 -  proof
   1.667 -    fix k
   1.668 -    assume kp: "k \<in> p"
   1.669 -    obtain c d where k: "k = cbox c d"
   1.670 -      using p(4)[OF kp] by blast
   1.671 -    have *: "cbox c d \<subseteq> cbox a b" "cbox c d \<noteq> {}"
   1.672 -      using p(2,3)[OF kp, unfolded k] using assms(2)
   1.673 -      by (blast intro: order.trans)+
   1.674 -    obtain q where "q division_of cbox a b" "cbox c d \<in> q"
   1.675 -      by (rule partial_division_extend_1[OF *])
   1.676 -    then show "\<exists>q. q division_of cbox a b \<and> k \<in> q"
   1.677 -      unfolding k by auto
   1.678 -  qed
   1.679 -  obtain q where q: "\<And>x. x \<in> p \<Longrightarrow> q x division_of cbox a b" "\<And>x. x \<in> p \<Longrightarrow> x \<in> q x"
   1.680 -    using bchoice[OF div_cbox] by blast
   1.681 -  { fix x
   1.682 -    assume x: "x \<in> p"
   1.683 -    have "q x division_of \<Union>q x"
   1.684 -      apply (rule division_ofI)
   1.685 -      using division_ofD[OF q(1)[OF x]]
   1.686 -      apply auto
   1.687 -      done }
   1.688 -  then have "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
   1.689 -    by (meson Diff_subset division_of_subset)
   1.690 -  then have "\<exists>d. d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)"
   1.691 -    apply -
   1.692 -    apply (rule elementary_inters [OF finite_imageI[OF p(1)]])
   1.693 -    apply (auto simp: False elementary_inters [OF finite_imageI[OF p(1)]])
   1.694 -    done
   1.695 -  then obtain d where d: "d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)" ..
   1.696 -  have "d \<union> p division_of cbox a b"
   1.697 -  proof -
   1.698 -    have te: "\<And>s f t. s \<noteq> {} \<Longrightarrow> \<forall>i\<in>s. f i \<union> i = t \<Longrightarrow> t = \<Inter>(f ` s) \<union> \<Union>s" by auto
   1.699 -    have cbox_eq: "cbox a b = \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p) \<union> \<Union>p"
   1.700 -    proof (rule te[OF False], clarify)
   1.701 -      fix i
   1.702 -      assume i: "i \<in> p"
   1.703 -      show "\<Union>(q i - {i}) \<union> i = cbox a b"
   1.704 -        using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto
   1.705 -    qed
   1.706 -    { fix k
   1.707 -      assume k: "k \<in> p"
   1.708 -      have *: "\<And>u t s. t \<inter> s = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<inter> t = {}"
   1.709 -        by auto
   1.710 -      have "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<inter> interior k = {}"
   1.711 -      proof (rule *[OF inter_interior_unions_intervals])
   1.712 -        note qk=division_ofD[OF q(1)[OF k]]
   1.713 -        show "finite (q k - {k})" "open (interior k)" "\<forall>t\<in>q k - {k}. \<exists>a b. t = cbox a b"
   1.714 -          using qk by auto
   1.715 -        show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}"
   1.716 -          using qk(5) using q(2)[OF k] by auto
   1.717 -        show "interior (\<Inter>i\<in>p. \<Union>(q i - {i})) \<subseteq> interior (\<Union>(q k - {k}))"
   1.718 -          apply (rule interior_mono)+
   1.719 -          using k
   1.720 -          apply auto
   1.721 -          done
   1.722 -      qed } note [simp] = this
   1.723 -    show "d \<union> p division_of (cbox a b)"
   1.724 -      unfolding cbox_eq
   1.725 -      apply (rule division_disjoint_union[OF d assms(1)])
   1.726 -      apply (rule inter_interior_unions_intervals)
   1.727 -      apply (rule p open_interior ballI)+
   1.728 -      apply simp_all
   1.729 -      done
   1.730 -  qed
   1.731 -  then show ?thesis
   1.732 -    by (meson Un_upper2 that)
   1.733 -qed
   1.734 -
   1.735 -lemma elementary_bounded[dest]:
   1.736 -  fixes s :: "'a::euclidean_space set"
   1.737 -  shows "p division_of s \<Longrightarrow> bounded s"
   1.738 -  unfolding division_of_def by (metis bounded_Union bounded_cbox)
   1.739 -
   1.740 -lemma elementary_subset_cbox:
   1.741 -  "p division_of s \<Longrightarrow> \<exists>a b. s \<subseteq> cbox a (b::'a::euclidean_space)"
   1.742 -  by (meson elementary_bounded bounded_subset_cbox)
   1.743 -
   1.744 -lemma division_union_intervals_exists:
   1.745 -  fixes a b :: "'a::euclidean_space"
   1.746 -  assumes "cbox a b \<noteq> {}"
   1.747 -  obtains p where "(insert (cbox a b) p) division_of (cbox a b \<union> cbox c d)"
   1.748 -proof (cases "cbox c d = {}")
   1.749 -  case True
   1.750 -  show ?thesis
   1.751 -    apply (rule that[of "{}"])
   1.752 -    unfolding True
   1.753 -    using assms
   1.754 -    apply auto
   1.755 -    done
   1.756 -next
   1.757 -  case False
   1.758 -  show ?thesis
   1.759 -  proof (cases "cbox a b \<inter> cbox c d = {}")
   1.760 -    case True
   1.761 -    then show ?thesis
   1.762 -      by (metis that False assms division_disjoint_union division_of_self insert_is_Un interior_Int interior_empty)
   1.763 -  next
   1.764 -    case False
   1.765 -    obtain u v where uv: "cbox a b \<inter> cbox c d = cbox u v"
   1.766 -      unfolding Int_interval by auto
   1.767 -    have uv_sub: "cbox u v \<subseteq> cbox c d" using uv by auto
   1.768 -    obtain p where "p division_of cbox c d" "cbox u v \<in> p"
   1.769 -      by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]])
   1.770 -    note p = this division_ofD[OF this(1)]
   1.771 -    have "interior (cbox a b \<inter> \<Union>(p - {cbox u v})) = interior(cbox u v \<inter> \<Union>(p - {cbox u v}))"
   1.772 -      apply (rule arg_cong[of _ _ interior])
   1.773 -      using p(8) uv by auto
   1.774 -    also have "\<dots> = {}"
   1.775 -      unfolding interior_Int
   1.776 -      apply (rule inter_interior_unions_intervals)
   1.777 -      using p(6) p(7)[OF p(2)] p(3)
   1.778 -      apply auto
   1.779 -      done
   1.780 -    finally have [simp]: "interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}" by simp
   1.781 -    have cbe: "cbox a b \<union> cbox c d = cbox a b \<union> \<Union>(p - {cbox u v})"
   1.782 -      using p(8) unfolding uv[symmetric] by auto
   1.783 -    have "insert (cbox a b) (p - {cbox u v}) division_of cbox a b \<union> \<Union>(p - {cbox u v})"
   1.784 -    proof -
   1.785 -      have "{cbox a b} division_of cbox a b"
   1.786 -        by (simp add: assms division_of_self)
   1.787 -      then show "insert (cbox a b) (p - {cbox u v}) division_of cbox a b \<union> \<Union>(p - {cbox u v})"
   1.788 -        by (metis (no_types) Diff_subset \<open>interior (cbox a b) \<inter> interior (\<Union>(p - {cbox u v})) = {}\<close> division_disjoint_union division_of_subset insert_is_Un p(1) p(8))
   1.789 -    qed
   1.790 -    with that[of "p - {cbox u v}"] show ?thesis by (simp add: cbe)
   1.791 -  qed
   1.792 -qed
   1.793 -
   1.794 -lemma division_of_unions:
   1.795 -  assumes "finite f"
   1.796 -    and "\<And>p. p \<in> f \<Longrightarrow> p division_of (\<Union>p)"
   1.797 -    and "\<And>k1 k2. k1 \<in> \<Union>f \<Longrightarrow> k2 \<in> \<Union>f \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
   1.798 -  shows "\<Union>f division_of \<Union>\<Union>f"
   1.799 -  using assms
   1.800 -  by (auto intro!: division_ofI)
   1.801 -
   1.802 -lemma elementary_union_interval:
   1.803 -  fixes a b :: "'a::euclidean_space"
   1.804 -  assumes "p division_of \<Union>p"
   1.805 -  obtains q where "q division_of (cbox a b \<union> \<Union>p)"
   1.806 -proof -
   1.807 -  note assm = division_ofD[OF assms]
   1.808 -  have lem1: "\<And>f s. \<Union>\<Union>(f ` s) = \<Union>((\<lambda>x. \<Union>(f x)) ` s)"
   1.809 -    by auto
   1.810 -  have lem2: "\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t |t. t \<in> f} = s \<union> \<Union>f"
   1.811 +lemma setsum_content_null:
   1.812 +  assumes "content (cbox a b) = 0"
   1.813 +    and "p tagged_division_of (cbox a b)"
   1.814 +  shows "setsum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)"
   1.815 +proof (rule setsum.neutral, rule)
   1.816 +  fix y
   1.817 +  assume y: "y \<in> p"
   1.818 +  obtain x k where xk: "y = (x, k)"
   1.819 +    using surj_pair[of y] by blast
   1.820 +  note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]]
   1.821 +  from this(2) obtain c d where k: "k = cbox c d" by blast
   1.822 +  have "(\<lambda>(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x"
   1.823 +    unfolding xk by auto
   1.824 +  also have "\<dots> = 0"
   1.825 +    using content_subset[OF assm(1)[unfolded k]] content_pos_le[of c d]
   1.826 +    unfolding assms(1) k
   1.827      by auto
   1.828 -  {
   1.829 -    presume "p = {} \<Longrightarrow> thesis"
   1.830 -      "cbox a b = {} \<Longrightarrow> thesis"
   1.831 -      "cbox a b \<noteq> {} \<Longrightarrow> interior (cbox a b) = {} \<Longrightarrow> thesis"
   1.832 -      "p \<noteq> {} \<Longrightarrow> interior (cbox a b)\<noteq>{} \<Longrightarrow> cbox a b \<noteq> {} \<Longrightarrow> thesis"
   1.833 -    then show thesis by auto
   1.834 -  next
   1.835 -    assume as: "p = {}"
   1.836 -    obtain p where "p division_of (cbox a b)"
   1.837 -      by (rule elementary_interval)
   1.838 -    then show thesis
   1.839 -      using as that by auto
   1.840 -  next
   1.841 -    assume as: "cbox a b = {}"
   1.842 -    show thesis
   1.843 -      using as assms that by auto
   1.844 -  next
   1.845 -    assume as: "interior (cbox a b) = {}" "cbox a b \<noteq> {}"
   1.846 -    show thesis
   1.847 -      apply (rule that[of "insert (cbox a b) p"],rule division_ofI)
   1.848 -      unfolding finite_insert
   1.849 -      apply (rule assm(1)) unfolding Union_insert
   1.850 -      using assm(2-4) as
   1.851 -      apply -
   1.852 -      apply (fast dest: assm(5))+
   1.853 -      done
   1.854 -  next
   1.855 -    assume as: "p \<noteq> {}" "interior (cbox a b) \<noteq> {}" "cbox a b \<noteq> {}"
   1.856 -    have "\<forall>k\<in>p. \<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)"
   1.857 -    proof
   1.858 -      fix k
   1.859 -      assume kp: "k \<in> p"
   1.860 -      from assm(4)[OF kp] obtain c d where "k = cbox c d" by blast
   1.861 -      then show "\<exists>q. (insert (cbox a b) q) division_of (cbox a b \<union> k)"
   1.862 -        by (meson as(3) division_union_intervals_exists)
   1.863 -    qed
   1.864 -    from bchoice[OF this] obtain q where "\<forall>x\<in>p. insert (cbox a b) (q x) division_of (cbox a b) \<union> x" ..
   1.865 -    note q = division_ofD[OF this[rule_format]]
   1.866 -    let ?D = "\<Union>{insert (cbox a b) (q k) | k. k \<in> p}"
   1.867 -    show thesis
   1.868 -    proof (rule that[OF division_ofI])
   1.869 -      have *: "{insert (cbox a b) (q k) |k. k \<in> p} = (\<lambda>k. insert (cbox a b) (q k)) ` p"
   1.870 -        by auto
   1.871 -      show "finite ?D"
   1.872 -        using "*" assm(1) q(1) by auto
   1.873 -      show "\<Union>?D = cbox a b \<union> \<Union>p"
   1.874 -        unfolding * lem1
   1.875 -        unfolding lem2[OF as(1), of "cbox a b", symmetric]
   1.876 -        using q(6)
   1.877 -        by auto
   1.878 -      fix k
   1.879 -      assume k: "k \<in> ?D"
   1.880 -      then show "k \<subseteq> cbox a b \<union> \<Union>p"
   1.881 -        using q(2) by auto
   1.882 -      show "k \<noteq> {}"
   1.883 -        using q(3) k by auto
   1.884 -      show "\<exists>a b. k = cbox a b"
   1.885 -        using q(4) k by auto
   1.886 -      fix k'
   1.887 -      assume k': "k' \<in> ?D" "k \<noteq> k'"
   1.888 -      obtain x where x: "k \<in> insert (cbox a b) (q x)" "x\<in>p"
   1.889 -        using k by auto
   1.890 -      obtain x' where x': "k'\<in>insert (cbox a b) (q x')" "x'\<in>p"
   1.891 -        using k' by auto
   1.892 -      show "interior k \<inter> interior k' = {}"
   1.893 -      proof (cases "x = x'")
   1.894 -        case True
   1.895 -        show ?thesis
   1.896 -          using True k' q(5) x' x by auto
   1.897 -      next
   1.898 -        case False
   1.899 -        {
   1.900 -          presume "k = cbox a b \<Longrightarrow> ?thesis"
   1.901 -            and "k' = cbox a b \<Longrightarrow> ?thesis"
   1.902 -            and "k \<noteq> cbox a b \<Longrightarrow> k' \<noteq> cbox a b \<Longrightarrow> ?thesis"
   1.903 -          then show ?thesis by linarith
   1.904 -        next
   1.905 -          assume as': "k  = cbox a b"
   1.906 -          show ?thesis
   1.907 -            using as' k' q(5) x' by blast
   1.908 -        next
   1.909 -          assume as': "k' = cbox a b"
   1.910 -          show ?thesis
   1.911 -            using as' k'(2) q(5) x by blast
   1.912 -        }
   1.913 -        assume as': "k \<noteq> cbox a b" "k' \<noteq> cbox a b"
   1.914 -        obtain c d where k: "k = cbox c d"
   1.915 -          using q(4)[OF x(2,1)] by blast
   1.916 -        have "interior k \<inter> interior (cbox a b) = {}"
   1.917 -          using as' k'(2) q(5) x by blast
   1.918 -        then have "interior k \<subseteq> interior x"
   1.919 -        using interior_subset_union_intervals
   1.920 -          by (metis as(2) k q(2) x interior_subset_union_intervals)
   1.921 -        moreover
   1.922 -        obtain c d where c_d: "k' = cbox c d"
   1.923 -          using q(4)[OF x'(2,1)] by blast
   1.924 -        have "interior k' \<inter> interior (cbox a b) = {}"
   1.925 -          using as'(2) q(5) x' by blast
   1.926 -        then have "interior k' \<subseteq> interior x'"
   1.927 -          by (metis as(2) c_d interior_subset_union_intervals q(2) x'(1) x'(2))
   1.928 -        ultimately show ?thesis
   1.929 -          using assm(5)[OF x(2) x'(2) False] by auto
   1.930 -      qed
   1.931 -    qed
   1.932 -  }
   1.933 -qed
   1.934 -
   1.935 -lemma elementary_unions_intervals:
   1.936 -  assumes fin: "finite f"
   1.937 -    and "\<And>s. s \<in> f \<Longrightarrow> \<exists>a b. s = cbox a (b::'a::euclidean_space)"
   1.938 -  obtains p where "p division_of (\<Union>f)"
   1.939 -proof -
   1.940 -  have "\<exists>p. p division_of (\<Union>f)"
   1.941 -  proof (induct_tac f rule:finite_subset_induct)
   1.942 -    show "\<exists>p. p division_of \<Union>{}" using elementary_empty by auto
   1.943 -  next
   1.944 -    fix x F
   1.945 -    assume as: "finite F" "x \<notin> F" "\<exists>p. p division_of \<Union>F" "x\<in>f"
   1.946 -    from this(3) obtain p where p: "p division_of \<Union>F" ..
   1.947 -    from assms(2)[OF as(4)] obtain a b where x: "x = cbox a b" by blast
   1.948 -    have *: "\<Union>F = \<Union>p"
   1.949 -      using division_ofD[OF p] by auto
   1.950 -    show "\<exists>p. p division_of \<Union>insert x F"
   1.951 -      using elementary_union_interval[OF p[unfolded *], of a b]
   1.952 -      unfolding Union_insert x * by metis
   1.953 -  qed (insert assms, auto)
   1.954 -  then show ?thesis
   1.955 -    using that by auto
   1.956 -qed
   1.957 -
   1.958 -lemma elementary_union:
   1.959 -  fixes s t :: "'a::euclidean_space set"
   1.960 -  assumes "ps division_of s" "pt division_of t"
   1.961 -  obtains p where "p division_of (s \<union> t)"
   1.962 -proof -
   1.963 -  have *: "s \<union> t = \<Union>ps \<union> \<Union>pt"
   1.964 -    using assms unfolding division_of_def by auto
   1.965 -  show ?thesis
   1.966 -    apply (rule elementary_unions_intervals[of "ps \<union> pt"])
   1.967 -    using assms apply auto
   1.968 -    by (simp add: * that)
   1.969 -qed
   1.970 -
   1.971 -lemma partial_division_extend:
   1.972 -  fixes t :: "'a::euclidean_space set"
   1.973 -  assumes "p division_of s"
   1.974 -    and "q division_of t"
   1.975 -    and "s \<subseteq> t"
   1.976 -  obtains r where "p \<subseteq> r" and "r division_of t"
   1.977 -proof -
   1.978 -  note divp = division_ofD[OF assms(1)] and divq = division_ofD[OF assms(2)]
   1.979 -  obtain a b where ab: "t \<subseteq> cbox a b"
   1.980 -    using elementary_subset_cbox[OF assms(2)] by auto
   1.981 -  obtain r1 where "p \<subseteq> r1" "r1 division_of (cbox a b)"
   1.982 -    using assms
   1.983 -    by (metis ab dual_order.trans partial_division_extend_interval divp(6))
   1.984 -  note r1 = this division_ofD[OF this(2)]
   1.985 -  obtain p' where "p' division_of \<Union>(r1 - p)"
   1.986 -    apply (rule elementary_unions_intervals[of "r1 - p"])
   1.987 -    using r1(3,6)
   1.988 -    apply auto
   1.989 -    done
   1.990 -  then obtain r2 where r2: "r2 division_of (\<Union>(r1 - p)) \<inter> (\<Union>q)"
   1.991 -    by (metis assms(2) divq(6) elementary_inter)
   1.992 -  {
   1.993 -    fix x
   1.994 -    assume x: "x \<in> t" "x \<notin> s"
   1.995 -    then have "x\<in>\<Union>r1"
   1.996 -      unfolding r1 using ab by auto
   1.997 -    then obtain r where r: "r \<in> r1" "x \<in> r"
   1.998 -      unfolding Union_iff ..
   1.999 -    moreover
  1.1000 -    have "r \<notin> p"
  1.1001 -    proof
  1.1002 -      assume "r \<in> p"
  1.1003 -      then have "x \<in> s" using divp(2) r by auto
  1.1004 -      then show False using x by auto
  1.1005 -    qed
  1.1006 -    ultimately have "x\<in>\<Union>(r1 - p)" by auto
  1.1007 -  }
  1.1008 -  then have *: "t = \<Union>p \<union> (\<Union>(r1 - p) \<inter> \<Union>q)"
  1.1009 -    unfolding divp divq using assms(3) by auto
  1.1010 -  show ?thesis
  1.1011 -    apply (rule that[of "p \<union> r2"])
  1.1012 -    unfolding *
  1.1013 -    defer
  1.1014 -    apply (rule division_disjoint_union)
  1.1015 -    unfolding divp(6)
  1.1016 -    apply(rule assms r2)+
  1.1017 -  proof -
  1.1018 -    have "interior s \<inter> interior (\<Union>(r1-p)) = {}"
  1.1019 -    proof (rule inter_interior_unions_intervals)
  1.1020 -      show "finite (r1 - p)" and "open (interior s)" and "\<forall>t\<in>r1-p. \<exists>a b. t = cbox a b"
  1.1021 -        using r1 by auto
  1.1022 -      have *: "\<And>s. (\<And>x. x \<in> s \<Longrightarrow> False) \<Longrightarrow> s = {}"
  1.1023 -        by auto
  1.1024 -      show "\<forall>t\<in>r1-p. interior s \<inter> interior t = {}"
  1.1025 -      proof
  1.1026 -        fix m x
  1.1027 -        assume as: "m \<in> r1 - p"
  1.1028 -        have "interior m \<inter> interior (\<Union>p) = {}"
  1.1029 -        proof (rule inter_interior_unions_intervals)
  1.1030 -          show "finite p" and "open (interior m)" and "\<forall>t\<in>p. \<exists>a b. t = cbox a b"
  1.1031 -            using divp by auto
  1.1032 -          show "\<forall>t\<in>p. interior m \<inter> interior t = {}"
  1.1033 -            by (metis DiffD1 DiffD2 as r1(1) r1(7) set_rev_mp)
  1.1034 -        qed
  1.1035 -        then show "interior s \<inter> interior m = {}"
  1.1036 -          unfolding divp by auto
  1.1037 -      qed
  1.1038 -    qed
  1.1039 -    then show "interior s \<inter> interior (\<Union>(r1-p) \<inter> (\<Union>q)) = {}"
  1.1040 -      using interior_subset by auto
  1.1041 -  qed auto
  1.1042 -qed
  1.1043 -
  1.1044 -lemma division_split_left_inj:
  1.1045 -  fixes type :: "'a::euclidean_space"
  1.1046 -  assumes "d division_of i"
  1.1047 -    and "k1 \<in> d"
  1.1048 -    and "k2 \<in> d"
  1.1049 -    and "k1 \<noteq> k2"
  1.1050 -    and "k1 \<inter> {x::'a. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c}"
  1.1051 -    and k: "k\<in>Basis"
  1.1052 -  shows "content(k1 \<inter> {x. x\<bullet>k \<le> c}) = 0"
  1.1053 -proof -
  1.1054 -  note d=division_ofD[OF assms(1)]
  1.1055 -  have *: "\<And>(a::'a) b c. content (cbox a b \<inter> {x. x\<bullet>k \<le> c}) = 0 \<longleftrightarrow>
  1.1056 -    interior(cbox a b \<inter> {x. x\<bullet>k \<le> c}) = {}"
  1.1057 -    unfolding  interval_split[OF k] content_eq_0_interior by auto
  1.1058 -  guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this
  1.1059 -  guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this
  1.1060 -  have **: "\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> u = {}"
  1.1061 -    by auto
  1.1062 -  show ?thesis
  1.1063 -    unfolding uv1 uv2 *
  1.1064 -    apply (rule **[OF d(5)[OF assms(2-4)]])
  1.1065 -    apply (simp add: uv1)
  1.1066 -    using assms(5) uv1 by auto
  1.1067 -qed
  1.1068 -
  1.1069 -lemma division_split_right_inj:
  1.1070 -  fixes type :: "'a::euclidean_space"
  1.1071 -  assumes "d division_of i"
  1.1072 -    and "k1 \<in> d"
  1.1073 -    and "k2 \<in> d"
  1.1074 -    and "k1 \<noteq> k2"
  1.1075 -    and "k1 \<inter> {x::'a. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}"
  1.1076 -    and k: "k \<in> Basis"
  1.1077 -  shows "content (k1 \<inter> {x. x\<bullet>k \<ge> c}) = 0"
  1.1078 -proof -
  1.1079 -  note d=division_ofD[OF assms(1)]
  1.1080 -  have *: "\<And>a b::'a. \<And>c. content(cbox a b \<inter> {x. x\<bullet>k \<ge> c}) = 0 \<longleftrightarrow>
  1.1081 -    interior(cbox a b \<inter> {x. x\<bullet>k \<ge> c}) = {}"
  1.1082 -    unfolding interval_split[OF k] content_eq_0_interior by auto
  1.1083 -  guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this
  1.1084 -  guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this
  1.1085 -  have **: "\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> u = {}"
  1.1086 -    by auto
  1.1087 -  show ?thesis
  1.1088 -    unfolding uv1 uv2 *
  1.1089 -    apply (rule **[OF d(5)[OF assms(2-4)]])
  1.1090 -    apply (simp add: uv1)
  1.1091 -    using assms(5) uv1 by auto
  1.1092 +  finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" .
  1.1093  qed
  1.1094  
  1.1095 -
  1.1096 -lemma division_split:
  1.1097 -  fixes a :: "'a::euclidean_space"
  1.1098 -  assumes "p division_of (cbox a b)"
  1.1099 -    and k: "k\<in>Basis"
  1.1100 -  shows "{l \<inter> {x. x\<bullet>k \<le> c} | l. l \<in> p \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}} division_of(cbox a b \<inter> {x. x\<bullet>k \<le> c})"
  1.1101 -      (is "?p1 division_of ?I1")
  1.1102 -    and "{l \<inter> {x. x\<bullet>k \<ge> c} | l. l \<in> p \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}} division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
  1.1103 -      (is "?p2 division_of ?I2")
  1.1104 -proof (rule_tac[!] division_ofI)
  1.1105 -  note p = division_ofD[OF assms(1)]
  1.1106 -  show "finite ?p1" "finite ?p2"
  1.1107 -    using p(1) by auto
  1.1108 -  show "\<Union>?p1 = ?I1" "\<Union>?p2 = ?I2"
  1.1109 -    unfolding p(6)[symmetric] by auto
  1.1110 -  {
  1.1111 -    fix k
  1.1112 -    assume "k \<in> ?p1"
  1.1113 -    then guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this
  1.1114 -    guess u v using p(4)[OF l(2)] by (elim exE) note uv=this
  1.1115 -    show "k \<subseteq> ?I1"
  1.1116 -      using l p(2) uv by force
  1.1117 -    show  "k \<noteq> {}"
  1.1118 -      by (simp add: l)
  1.1119 -    show  "\<exists>a b. k = cbox a b"
  1.1120 -      apply (simp add: l uv p(2-3)[OF l(2)])
  1.1121 -      apply (subst interval_split[OF k])
  1.1122 -      apply (auto intro: order.trans)
  1.1123 -      done
  1.1124 -    fix k'
  1.1125 -    assume "k' \<in> ?p1"
  1.1126 -    then guess l' unfolding mem_Collect_eq by (elim exE conjE) note l'=this
  1.1127 -    assume "k \<noteq> k'"
  1.1128 -    then show "interior k \<inter> interior k' = {}"
  1.1129 -      unfolding l l' using p(5)[OF l(2) l'(2)] by auto
  1.1130 -  }
  1.1131 -  {
  1.1132 -    fix k
  1.1133 -    assume "k \<in> ?p2"
  1.1134 -    then guess l unfolding mem_Collect_eq by (elim exE conjE) note l=this
  1.1135 -    guess u v using p(4)[OF l(2)] by (elim exE) note uv=this
  1.1136 -    show "k \<subseteq> ?I2"
  1.1137 -      using l p(2) uv by force
  1.1138 -    show  "k \<noteq> {}"
  1.1139 -      by (simp add: l)
  1.1140 -    show  "\<exists>a b. k = cbox a b"
  1.1141 -      apply (simp add: l uv p(2-3)[OF l(2)])
  1.1142 -      apply (subst interval_split[OF k])
  1.1143 -      apply (auto intro: order.trans)
  1.1144 -      done
  1.1145 -    fix k'
  1.1146 -    assume "k' \<in> ?p2"
  1.1147 -    then guess l' unfolding mem_Collect_eq by (elim exE conjE) note l'=this
  1.1148 -    assume "k \<noteq> k'"
  1.1149 -    then show "interior k \<inter> interior k' = {}"
  1.1150 -      unfolding l l' using p(5)[OF l(2) l'(2)] by auto
  1.1151 -  }
  1.1152 -qed
  1.1153 -
  1.1154 -subsection \<open>Tagged (partial) divisions.\<close>
  1.1155 -
  1.1156 -definition tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40)
  1.1157 -  where "s tagged_partial_division_of i \<longleftrightarrow>
  1.1158 -    finite s \<and>
  1.1159 -    (\<forall>x k. (x, k) \<in> s \<longrightarrow> x \<in> k \<and> k \<subseteq> i \<and> (\<exists>a b. k = cbox a b)) \<and>
  1.1160 -    (\<forall>x1 k1 x2 k2. (x1, k1) \<in> s \<and> (x2, k2) \<in> s \<and> (x1, k1) \<noteq> (x2, k2) \<longrightarrow>
  1.1161 -      interior k1 \<inter> interior k2 = {})"
  1.1162 -
  1.1163 -lemma tagged_partial_division_ofD[dest]:
  1.1164 -  assumes "s tagged_partial_division_of i"
  1.1165 -  shows "finite s"
  1.1166 -    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k"
  1.1167 -    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
  1.1168 -    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
  1.1169 -    and "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow>
  1.1170 -      (x2, k2) \<in> s \<Longrightarrow> (x1, k1) \<noteq> (x2, k2) \<Longrightarrow> interior k1 \<inter> interior k2 = {}"
  1.1171 -  using assms unfolding tagged_partial_division_of_def by blast+
  1.1172 -
  1.1173 -definition tagged_division_of (infixr "tagged'_division'_of" 40)
  1.1174 -  where "s tagged_division_of i \<longleftrightarrow> s tagged_partial_division_of i \<and> (\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
  1.1175 -
  1.1176 -lemma tagged_division_of_finite: "s tagged_division_of i \<Longrightarrow> finite s"
  1.1177 -  unfolding tagged_division_of_def tagged_partial_division_of_def by auto
  1.1178 -
  1.1179 -lemma tagged_division_of:
  1.1180 -  "s tagged_division_of i \<longleftrightarrow>
  1.1181 -    finite s \<and>
  1.1182 -    (\<forall>x k. (x, k) \<in> s \<longrightarrow> x \<in> k \<and> k \<subseteq> i \<and> (\<exists>a b. k = cbox a b)) \<and>
  1.1183 -    (\<forall>x1 k1 x2 k2. (x1, k1) \<in> s \<and> (x2, k2) \<in> s \<and> (x1, k1) \<noteq> (x2, k2) \<longrightarrow>
  1.1184 -      interior k1 \<inter> interior k2 = {}) \<and>
  1.1185 -    (\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
  1.1186 -  unfolding tagged_division_of_def tagged_partial_division_of_def by auto
  1.1187 -
  1.1188 -lemma tagged_division_ofI:
  1.1189 -  assumes "finite s"
  1.1190 -    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k"
  1.1191 -    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
  1.1192 -    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
  1.1193 -    and "\<And>x1 k1 x2 k2. (x1,k1) \<in> s \<Longrightarrow> (x2, k2) \<in> s \<Longrightarrow> (x1, k1) \<noteq> (x2, k2) \<Longrightarrow>
  1.1194 -      interior k1 \<inter> interior k2 = {}"
  1.1195 -    and "(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
  1.1196 -  shows "s tagged_division_of i"
  1.1197 -  unfolding tagged_division_of
  1.1198 -  using assms
  1.1199 -  apply auto
  1.1200 -  apply fastforce+
  1.1201 -  done
  1.1202 -
  1.1203 -lemma tagged_division_ofD[dest]:  (*FIXME USE A LOCALE*)
  1.1204 -  assumes "s tagged_division_of i"
  1.1205 -  shows "finite s"
  1.1206 -    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> x \<in> k"
  1.1207 -    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> i"
  1.1208 -    and "\<And>x k. (x,k) \<in> s \<Longrightarrow> \<exists>a b. k = cbox a b"
  1.1209 -    and "\<And>x1 k1 x2 k2. (x1, k1) \<in> s \<Longrightarrow> (x2, k2) \<in> s \<Longrightarrow> (x1, k1) \<noteq> (x2, k2) \<Longrightarrow>
  1.1210 -      interior k1 \<inter> interior k2 = {}"
  1.1211 -    and "(\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
  1.1212 -  using assms unfolding tagged_division_of by blast+
  1.1213 -
  1.1214 -lemma division_of_tagged_division:
  1.1215 -  assumes "s tagged_division_of i"
  1.1216 -  shows "(snd ` s) division_of i"
  1.1217 -proof (rule division_ofI)
  1.1218 -  note assm = tagged_division_ofD[OF assms]
  1.1219 -  show "\<Union>(snd ` s) = i" "finite (snd ` s)"
  1.1220 -    using assm by auto
  1.1221 -  fix k
  1.1222 -  assume k: "k \<in> snd ` s"
  1.1223 -  then obtain xk where xk: "(xk, k) \<in> s"
  1.1224 -    by auto
  1.1225 -  then show "k \<subseteq> i" "k \<noteq> {}" "\<exists>a b. k = cbox a b"
  1.1226 -    using assm by fastforce+
  1.1227 -  fix k'
  1.1228 -  assume k': "k' \<in> snd ` s" "k \<noteq> k'"
  1.1229 -  from this(1) obtain xk' where xk': "(xk', k') \<in> s"
  1.1230 -    by auto
  1.1231 -  then show "interior k \<inter> interior k' = {}"
  1.1232 -    using assm(5) k'(2) xk by blast
  1.1233 -qed
  1.1234 -
  1.1235 -lemma partial_division_of_tagged_division:
  1.1236 -  assumes "s tagged_partial_division_of i"
  1.1237 -  shows "(snd ` s) division_of \<Union>(snd ` s)"
  1.1238 -proof (rule division_ofI)
  1.1239 -  note assm = tagged_partial_division_ofD[OF assms]
  1.1240 -  show "finite (snd ` s)" "\<Union>(snd ` s) = \<Union>(snd ` s)"
  1.1241 -    using assm by auto
  1.1242 -  fix k
  1.1243 -  assume k: "k \<in> snd ` s"
  1.1244 -  then obtain xk where xk: "(xk, k) \<in> s"
  1.1245 -    by auto
  1.1246 -  then show "k \<noteq> {}" "\<exists>a b. k = cbox a b" "k \<subseteq> \<Union>(snd ` s)"
  1.1247 -    using assm by auto
  1.1248 -  fix k'
  1.1249 -  assume k': "k' \<in> snd ` s" "k \<noteq> k'"
  1.1250 -  from this(1) obtain xk' where xk': "(xk', k') \<in> s"
  1.1251 -    by auto
  1.1252 -  then show "interior k \<inter> interior k' = {}"
  1.1253 -    using assm(5) k'(2) xk by auto
  1.1254 -qed
  1.1255 -
  1.1256 -lemma tagged_partial_division_subset:
  1.1257 -  assumes "s tagged_partial_division_of i"
  1.1258 -    and "t \<subseteq> s"
  1.1259 -  shows "t tagged_partial_division_of i"
  1.1260 -  using assms
  1.1261 -  unfolding tagged_partial_division_of_def
  1.1262 -  using finite_subset[OF assms(2)]
  1.1263 -  by blast
  1.1264 -
  1.1265 -lemma (in comm_monoid_set) over_tagged_division_lemma:
  1.1266 -  assumes "p tagged_division_of i"
  1.1267 -    and "\<And>u v. cbox u v \<noteq> {} \<Longrightarrow> content (cbox u v) = 0 \<Longrightarrow> d (cbox u v) = \<^bold>1"
  1.1268 -  shows "F (\<lambda>(x,k). d k) p = F d (snd ` p)"
  1.1269 -proof -
  1.1270 -  have *: "(\<lambda>(x,k). d k) = d \<circ> snd"
  1.1271 -    unfolding o_def by (rule ext) auto
  1.1272 -  note assm = tagged_division_ofD[OF assms(1)]
  1.1273 -  show ?thesis
  1.1274 -    unfolding *
  1.1275 -  proof (rule reindex_nontrivial[symmetric])
  1.1276 -    show "finite p"
  1.1277 -      using assm by auto
  1.1278 -    fix x y
  1.1279 -    assume "x\<in>p" "y\<in>p" "x\<noteq>y" "snd x = snd y"
  1.1280 -    obtain a b where ab: "snd x = cbox a b"
  1.1281 -      using assm(4)[of "fst x" "snd x"] \<open>x\<in>p\<close> by auto
  1.1282 -    have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y"
  1.1283 -      by (metis prod.collapse \<open>x\<in>p\<close> \<open>snd x = snd y\<close> \<open>x \<noteq> y\<close>)+
  1.1284 -    with \<open>x\<in>p\<close> \<open>y\<in>p\<close> have "interior (snd x) \<inter> interior (snd y) = {}"
  1.1285 -      by (intro assm(5)[of "fst x" _ "fst y"]) auto
  1.1286 -    then have "content (cbox a b) = 0"
  1.1287 -      unfolding \<open>snd x = snd y\<close>[symmetric] ab content_eq_0_interior by auto
  1.1288 -    then have "d (cbox a b) = \<^bold>1"
  1.1289 -      using assm(2)[of "fst x" "snd x"] \<open>x\<in>p\<close> ab[symmetric] by (intro assms(2)) auto
  1.1290 -    then show "d (snd x) = \<^bold>1"
  1.1291 -      unfolding ab by auto
  1.1292 -  qed
  1.1293 -qed
  1.1294 -
  1.1295 -lemma tag_in_interval: "p tagged_division_of i \<Longrightarrow> (x, k) \<in> p \<Longrightarrow> x \<in> i"
  1.1296 -  by auto
  1.1297 -
  1.1298 -lemma tagged_division_of_empty: "{} tagged_division_of {}"
  1.1299 -  unfolding tagged_division_of by auto
  1.1300 -
  1.1301 -lemma tagged_partial_division_of_trivial[simp]: "p tagged_partial_division_of {} \<longleftrightarrow> p = {}"
  1.1302 -  unfolding tagged_partial_division_of_def by auto
  1.1303 -
  1.1304 -lemma tagged_division_of_trivial[simp]: "p tagged_division_of {} \<longleftrightarrow> p = {}"
  1.1305 -  unfolding tagged_division_of by auto
  1.1306 -
  1.1307 -lemma tagged_division_of_self: "x \<in> cbox a b \<Longrightarrow> {(x,cbox a b)} tagged_division_of (cbox a b)"
  1.1308 -  by (rule tagged_division_ofI) auto
  1.1309 -
  1.1310 -lemma tagged_division_of_self_real: "x \<in> {a .. b::real} \<Longrightarrow> {(x,{a .. b})} tagged_division_of {a .. b}"
  1.1311 -  unfolding box_real[symmetric]
  1.1312 -  by (rule tagged_division_of_self)
  1.1313 -
  1.1314 -lemma tagged_division_union:
  1.1315 -  assumes "p1 tagged_division_of s1"
  1.1316 -    and "p2 tagged_division_of s2"
  1.1317 -    and "interior s1 \<inter> interior s2 = {}"
  1.1318 -  shows "(p1 \<union> p2) tagged_division_of (s1 \<union> s2)"
  1.1319 -proof (rule tagged_division_ofI)
  1.1320 -  note p1 = tagged_division_ofD[OF assms(1)]
  1.1321 -  note p2 = tagged_division_ofD[OF assms(2)]
  1.1322 -  show "finite (p1 \<union> p2)"
  1.1323 -    using p1(1) p2(1) by auto
  1.1324 -  show "\<Union>{k. \<exists>x. (x, k) \<in> p1 \<union> p2} = s1 \<union> s2"
  1.1325 -    using p1(6) p2(6) by blast
  1.1326 -  fix x k
  1.1327 -  assume xk: "(x, k) \<in> p1 \<union> p2"
  1.1328 -  show "x \<in> k" "\<exists>a b. k = cbox a b"
  1.1329 -    using xk p1(2,4) p2(2,4) by auto
  1.1330 -  show "k \<subseteq> s1 \<union> s2"
  1.1331 -    using xk p1(3) p2(3) by blast
  1.1332 -  fix x' k'
  1.1333 -  assume xk': "(x', k') \<in> p1 \<union> p2" "(x, k) \<noteq> (x', k')"
  1.1334 -  have *: "\<And>a b. a \<subseteq> s1 \<Longrightarrow> b \<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}"
  1.1335 -    using assms(3) interior_mono by blast
  1.1336 -  show "interior k \<inter> interior k' = {}"
  1.1337 -    apply (cases "(x, k) \<in> p1")
  1.1338 -    apply (meson "*" UnE assms(1) assms(2) p1(5) tagged_division_ofD(3) xk'(1) xk'(2))
  1.1339 -    by (metis "*" UnE assms(1) assms(2) inf_sup_aci(1) p2(5) tagged_division_ofD(3) xk xk'(1) xk'(2))
  1.1340 -qed
  1.1341 -
  1.1342 -lemma tagged_division_unions:
  1.1343 -  assumes "finite iset"
  1.1344 -    and "\<forall>i\<in>iset. pfn i tagged_division_of i"
  1.1345 -    and "\<forall>i1\<in>iset. \<forall>i2\<in>iset. i1 \<noteq> i2 \<longrightarrow> interior(i1) \<inter> interior(i2) = {}"
  1.1346 -  shows "\<Union>(pfn ` iset) tagged_division_of (\<Union>iset)"
  1.1347 -proof (rule tagged_division_ofI)
  1.1348 -  note assm = tagged_division_ofD[OF assms(2)[rule_format]]
  1.1349 -  show "finite (\<Union>(pfn ` iset))"
  1.1350 -    using assms by auto
  1.1351 -  have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>((\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` iset)"
  1.1352 -    by blast
  1.1353 -  also have "\<dots> = \<Union>iset"
  1.1354 -    using assm(6) by auto
  1.1355 -  finally show "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>iset" .
  1.1356 -  fix x k
  1.1357 -  assume xk: "(x, k) \<in> \<Union>(pfn ` iset)"
  1.1358 -  then obtain i where i: "i \<in> iset" "(x, k) \<in> pfn i"
  1.1359 -    by auto
  1.1360 -  show "x \<in> k" "\<exists>a b. k = cbox a b" "k \<subseteq> \<Union>iset"
  1.1361 -    using assm(2-4)[OF i] using i(1) by auto
  1.1362 -  fix x' k'
  1.1363 -  assume xk': "(x', k') \<in> \<Union>(pfn ` iset)" "(x, k) \<noteq> (x', k')"
  1.1364 -  then obtain i' where i': "i' \<in> iset" "(x', k') \<in> pfn i'"
  1.1365 -    by auto
  1.1366 -  have *: "\<And>a b. i \<noteq> i' \<Longrightarrow> a \<subseteq> i \<Longrightarrow> b \<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}"
  1.1367 -    using i(1) i'(1)
  1.1368 -    using assms(3)[rule_format] interior_mono
  1.1369 -    by blast
  1.1370 -  show "interior k \<inter> interior k' = {}"
  1.1371 -    apply (cases "i = i'")
  1.1372 -    using assm(5) i' i(2) xk'(2) apply blast
  1.1373 -    using "*" assm(3) i' i by auto
  1.1374 -qed
  1.1375 -
  1.1376 -lemma tagged_partial_division_of_union_self:
  1.1377 -  assumes "p tagged_partial_division_of s"
  1.1378 -  shows "p tagged_division_of (\<Union>(snd ` p))"
  1.1379 -  apply (rule tagged_division_ofI)
  1.1380 -  using tagged_partial_division_ofD[OF assms]
  1.1381 -  apply auto
  1.1382 -  done
  1.1383 -
  1.1384 -lemma tagged_division_of_union_self:
  1.1385 -  assumes "p tagged_division_of s"
  1.1386 -  shows "p tagged_division_of (\<Union>(snd ` p))"
  1.1387 -  apply (rule tagged_division_ofI)
  1.1388 -  using tagged_division_ofD[OF assms]
  1.1389 -  apply auto
  1.1390 -  done
  1.1391 -
  1.1392 -subsection \<open>Functions closed on boxes: morphisms from boxes to monoids\<close>
  1.1393 -
  1.1394 -text \<open>This auxiliary structure is used to sum up over the elements of a division. Main theorem is
  1.1395 -  @{text operative_division}. Instances for the monoid are @{typ "'a option"}, @{typ real}, and
  1.1396 -  @{typ bool}.\<close>
  1.1397 -
  1.1398 -lemma property_empty_interval: "\<forall>a b. content (cbox a b) = 0 \<longrightarrow> P (cbox a b) \<Longrightarrow> P {}"
  1.1399 -  using content_empty unfolding empty_as_interval by auto
  1.1400 -
  1.1401 -paragraph \<open>Using additivity of lifted function to encode definedness.\<close>
  1.1402 -
  1.1403 -definition lift_option :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> 'c option"
  1.1404 -where
  1.1405 -  "lift_option f a' b' = Option.bind a' (\<lambda>a. Option.bind b' (\<lambda>b. Some (f a b)))"
  1.1406 -
  1.1407 -lemma lift_option_simps[simp]:
  1.1408 -  "lift_option f (Some a) (Some b) = Some (f a b)"
  1.1409 -  "lift_option f None b' = None"
  1.1410 -  "lift_option f a' None = None"
  1.1411 -  by (auto simp: lift_option_def)
  1.1412 -
  1.1413 -lemma comm_monoid_lift_option:
  1.1414 -  assumes "comm_monoid f z"
  1.1415 -  shows "comm_monoid (lift_option f) (Some z)"
  1.1416 -proof -
  1.1417 -  from assms interpret comm_monoid f z .
  1.1418 -  show ?thesis
  1.1419 -    by standard (auto simp: lift_option_def ac_simps split: bind_split)
  1.1420 -qed
  1.1421 -
  1.1422 -lemma comm_monoid_and: "comm_monoid HOL.conj True"
  1.1423 -  by standard auto
  1.1424 -
  1.1425 -lemma comm_monoid_set_and: "comm_monoid_set HOL.conj True"
  1.1426 -  by (rule comm_monoid_set.intro) (fact comm_monoid_and)
  1.1427 -
  1.1428 -paragraph \<open>Operative\<close>
  1.1429 -
  1.1430 -definition (in comm_monoid) operative :: "('b::euclidean_space set \<Rightarrow> 'a) \<Rightarrow> bool"
  1.1431 -  where "operative g \<longleftrightarrow>
  1.1432 -    (\<forall>a b. content (cbox a b) = 0 \<longrightarrow> g (cbox a b) = \<^bold>1) \<and>
  1.1433 -    (\<forall>a b c. \<forall>k\<in>Basis. g (cbox a b) = g (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. x\<bullet>k \<ge> c}))"
  1.1434 -
  1.1435 -lemma (in comm_monoid) operativeD[dest]:
  1.1436 -  assumes "operative g"
  1.1437 -  shows "\<And>a b. content (cbox a b) = 0 \<Longrightarrow> g (cbox a b) = \<^bold>1"
  1.1438 -    and "\<And>a b c k. k \<in> Basis \<Longrightarrow> g (cbox a b) = g (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<^bold>* g (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
  1.1439 -  using assms unfolding operative_def by auto
  1.1440 -
  1.1441 -lemma (in comm_monoid) operative_empty: "operative g \<Longrightarrow> g {} = \<^bold>1"
  1.1442 -  unfolding operative_def by (rule property_empty_interval) auto
  1.1443 -
  1.1444  lemma operative_content[intro]: "add.operative content"
  1.1445 -  by (force simp add: add.operative_def content_split[symmetric])
  1.1446 -
  1.1447 -definition "division_points (k::('a::euclidean_space) set) d =
  1.1448 -   {(j,x). j \<in> Basis \<and> (interval_lowerbound k)\<bullet>j < x \<and> x < (interval_upperbound k)\<bullet>j \<and>
  1.1449 -     (\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"
  1.1450 -
  1.1451 -lemma division_points_finite:
  1.1452 -  fixes i :: "'a::euclidean_space set"
  1.1453 -  assumes "d division_of i"
  1.1454 -  shows "finite (division_points i d)"
  1.1455 -proof -
  1.1456 -  note assm = division_ofD[OF assms]
  1.1457 -  let ?M = "\<lambda>j. {(j,x)|x. (interval_lowerbound i)\<bullet>j < x \<and> x < (interval_upperbound i)\<bullet>j \<and>
  1.1458 -    (\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"
  1.1459 -  have *: "division_points i d = \<Union>(?M ` Basis)"
  1.1460 -    unfolding division_points_def by auto
  1.1461 -  show ?thesis
  1.1462 -    unfolding * using assm by auto
  1.1463 -qed
  1.1464 -
  1.1465 -lemma division_points_subset:
  1.1466 -  fixes a :: "'a::euclidean_space"
  1.1467 -  assumes "d division_of (cbox a b)"
  1.1468 -    and "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"  "a\<bullet>k < c" "c < b\<bullet>k"
  1.1469 -    and k: "k \<in> Basis"
  1.1470 -  shows "division_points (cbox a b \<inter> {x. x\<bullet>k \<le> c}) {l \<inter> {x. x\<bullet>k \<le> c} | l . l \<in> d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}} \<subseteq>
  1.1471 -      division_points (cbox a b) d" (is ?t1)
  1.1472 -    and "division_points (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) {l \<inter> {x. x\<bullet>k \<ge> c} | l . l \<in> d \<and> ~(l \<inter> {x. x\<bullet>k \<ge> c} = {})} \<subseteq>
  1.1473 -      division_points (cbox a b) d" (is ?t2)
  1.1474 -proof -
  1.1475 -  note assm = division_ofD[OF assms(1)]
  1.1476 -  have *: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
  1.1477 -    "\<forall>i\<in>Basis. a\<bullet>i \<le> (\<Sum>i\<in>Basis. (if i = k then min (b \<bullet> k) c else  b \<bullet> i) *\<^sub>R i) \<bullet> i"
  1.1478 -    "\<forall>i\<in>Basis. (\<Sum>i\<in>Basis. (if i = k then max (a \<bullet> k) c else a \<bullet> i) *\<^sub>R i) \<bullet> i \<le> b\<bullet>i"
  1.1479 -    "min (b \<bullet> k) c = c" "max (a \<bullet> k) c = c"
  1.1480 -    using assms using less_imp_le by auto
  1.1481 -  show ?t1 (*FIXME a horrible mess*)
  1.1482 -    unfolding division_points_def interval_split[OF k, of a b]
  1.1483 -    unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
  1.1484 -    unfolding *
  1.1485 -    apply (rule subsetI)
  1.1486 -    unfolding mem_Collect_eq split_beta
  1.1487 -    apply (erule bexE conjE)+
  1.1488 -    apply (simp add: )
  1.1489 -    apply (erule exE conjE)+
  1.1490 -  proof
  1.1491 -    fix i l x
  1.1492 -    assume as:
  1.1493 -      "a \<bullet> fst x < snd x" "snd x < (if fst x = k then c else b \<bullet> fst x)"
  1.1494 -      "interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
  1.1495 -      "i = l \<inter> {x. x \<bullet> k \<le> c}" "l \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} \<noteq> {}"
  1.1496 -      and fstx: "fst x \<in> Basis"
  1.1497 -    from assm(4)[OF this(5)] guess u v apply-by(erule exE)+ note l=this
  1.1498 -    have *: "\<forall>i\<in>Basis. u \<bullet> i \<le> (\<Sum>i\<in>Basis. (if i = k then min (v \<bullet> k) c else v \<bullet> i) *\<^sub>R i) \<bullet> i"
  1.1499 -      using as(6) unfolding l interval_split[OF k] box_ne_empty as .
  1.1500 -    have **: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
  1.1501 -      using l using as(6) unfolding box_ne_empty[symmetric] by auto
  1.1502 -    show "\<exists>i\<in>d. interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
  1.1503 -      apply (rule bexI[OF _ \<open>l \<in> d\<close>])
  1.1504 -      using as(1-3,5) fstx
  1.1505 -      unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as
  1.1506 -      apply (auto split: if_split_asm)
  1.1507 -      done
  1.1508 -    show "snd x < b \<bullet> fst x"
  1.1509 -      using as(2) \<open>c < b\<bullet>k\<close> by (auto split: if_split_asm)
  1.1510 -  qed
  1.1511 -  show ?t2
  1.1512 -    unfolding division_points_def interval_split[OF k, of a b]
  1.1513 -    unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
  1.1514 -    unfolding *
  1.1515 -    unfolding subset_eq
  1.1516 -    apply rule
  1.1517 -    unfolding mem_Collect_eq split_beta
  1.1518 -    apply (erule bexE conjE)+
  1.1519 -    apply (simp only: mem_Collect_eq inner_setsum_left_Basis simp_thms)
  1.1520 -    apply (erule exE conjE)+
  1.1521 -  proof
  1.1522 -    fix i l x
  1.1523 -    assume as:
  1.1524 -      "(if fst x = k then c else a \<bullet> fst x) < snd x" "snd x < b \<bullet> fst x"
  1.1525 -      "interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
  1.1526 -      "i = l \<inter> {x. c \<le> x \<bullet> k}" "l \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} \<noteq> {}"
  1.1527 -      and fstx: "fst x \<in> Basis"
  1.1528 -    from assm(4)[OF this(5)] guess u v by (elim exE) note l=this
  1.1529 -    have *: "\<forall>i\<in>Basis. (\<Sum>i\<in>Basis. (if i = k then max (u \<bullet> k) c else u \<bullet> i) *\<^sub>R i) \<bullet> i \<le> v \<bullet> i"
  1.1530 -      using as(6) unfolding l interval_split[OF k] box_ne_empty as .
  1.1531 -    have **: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i"
  1.1532 -      using l using as(6) unfolding box_ne_empty[symmetric] by auto
  1.1533 -    show "\<exists>i\<in>d. interval_lowerbound i \<bullet> fst x = snd x \<or> interval_upperbound i \<bullet> fst x = snd x"
  1.1534 -      apply (rule bexI[OF _ \<open>l \<in> d\<close>])
  1.1535 -      using as(1-3,5) fstx
  1.1536 -      unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] as
  1.1537 -      apply (auto split: if_split_asm)
  1.1538 -      done
  1.1539 -    show "a \<bullet> fst x < snd x"
  1.1540 -      using as(1) \<open>a\<bullet>k < c\<close> by (auto split: if_split_asm)
  1.1541 -   qed
  1.1542 -qed
  1.1543 -
  1.1544 -lemma division_points_psubset:
  1.1545 -  fixes a :: "'a::euclidean_space"
  1.1546 -  assumes "d division_of (cbox a b)"
  1.1547 -      and "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"  "a\<bullet>k < c" "c < b\<bullet>k"
  1.1548 -      and "l \<in> d"
  1.1549 -      and "interval_lowerbound l\<bullet>k = c \<or> interval_upperbound l\<bullet>k = c"
  1.1550 -      and k: "k \<in> Basis"
  1.1551 -  shows "division_points (cbox a b \<inter> {x. x\<bullet>k \<le> c}) {l \<inter> {x. x\<bullet>k \<le> c} | l. l\<in>d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}} \<subset>
  1.1552 -         division_points (cbox a b) d" (is "?D1 \<subset> ?D")
  1.1553 -    and "division_points (cbox a b \<inter> {x. x\<bullet>k \<ge> c}) {l \<inter> {x. x\<bullet>k \<ge> c} | l. l\<in>d \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}} \<subset>
  1.1554 -         division_points (cbox a b) d" (is "?D2 \<subset> ?D")
  1.1555 -proof -
  1.1556 -  have ab: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
  1.1557 -    using assms(2) by (auto intro!:less_imp_le)
  1.1558 -  guess u v using division_ofD(4)[OF assms(1,5)] by (elim exE) note l=this
  1.1559 -  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"
  1.1560 -    using division_ofD(2,2,3)[OF assms(1,5)] unfolding l box_ne_empty
  1.1561 -    using subset_box(1)
  1.1562 -    apply auto
  1.1563 -    apply blast+
  1.1564 -    done
  1.1565 -  have *: "interval_upperbound (cbox a b \<inter> {x. x \<bullet> k \<le> interval_upperbound l \<bullet> k}) \<bullet> k = interval_upperbound l \<bullet> k"
  1.1566 -          "interval_upperbound (cbox a b \<inter> {x. x \<bullet> k \<le> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> k"
  1.1567 -    unfolding l interval_split[OF k] interval_bounds[OF uv(1)]
  1.1568 -    using uv[rule_format, of k] ab k
  1.1569 -    by auto
  1.1570 -  have "\<exists>x. x \<in> ?D - ?D1"
  1.1571 -    using assms(3-)
  1.1572 -    unfolding division_points_def interval_bounds[OF ab]
  1.1573 -    apply -
  1.1574 -    apply (erule disjE)
  1.1575 -    apply (rule_tac x="(k,(interval_lowerbound l)\<bullet>k)" in exI, force simp add: *)
  1.1576 -    apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI, force simp add: *)
  1.1577 -    done
  1.1578 -  moreover have "?D1 \<subseteq> ?D"
  1.1579 -    by (auto simp add: assms division_points_subset)
  1.1580 -  ultimately show "?D1 \<subset> ?D"
  1.1581 -    by blast
  1.1582 -  have *: "interval_lowerbound (cbox a b \<inter> {x. x \<bullet> k \<ge> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> k"
  1.1583 -    "interval_lowerbound (cbox a b \<inter> {x. x \<bullet> k \<ge> interval_upperbound l \<bullet> k}) \<bullet> k = interval_upperbound l \<bullet> k"
  1.1584 -    unfolding l interval_split[OF k] interval_bounds[OF uv(1)]
  1.1585 -    using uv[rule_format, of k] ab k
  1.1586 -    by auto
  1.1587 -  have "\<exists>x. x \<in> ?D - ?D2"
  1.1588 -    using assms(3-)
  1.1589 -    unfolding division_points_def interval_bounds[OF ab]
  1.1590 -    apply -
  1.1591 -    apply (erule disjE)
  1.1592 -    apply (rule_tac x="(k,(interval_lowerbound l)\<bullet>k)" in exI, force simp add: *)
  1.1593 -    apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI, force simp add: *)
  1.1594 -    done
  1.1595 -  moreover have "?D2 \<subseteq> ?D"
  1.1596 -    by (auto simp add: assms division_points_subset)
  1.1597 -  ultimately show "?D2 \<subset> ?D"
  1.1598 -    by blast
  1.1599 -qed
  1.1600 -
  1.1601 -lemma (in comm_monoid_set) operative_division:
  1.1602 -  fixes g :: "'b::euclidean_space set \<Rightarrow> 'a"
  1.1603 -  assumes g: "operative g" and d: "d division_of (cbox a b)" shows "F g d = g (cbox a b)"
  1.1604 -proof -
  1.1605 -  define C where [abs_def]: "C = card (division_points (cbox a b) d)"
  1.1606 -  then show ?thesis
  1.1607 -    using d
  1.1608 -  proof (induction C arbitrary: a b d rule: less_induct)
  1.1609 -    case (less a b d)
  1.1610 -    show ?case
  1.1611 -    proof cases
  1.1612 -      show "content (cbox a b) = 0 \<Longrightarrow> F g d = g (cbox a b)"
  1.1613 -        using division_of_content_0[OF _ less.prems] operativeD(1)[OF  g] division_ofD(4)[OF less.prems]
  1.1614 -        by (fastforce intro!: neutral)
  1.1615 -    next
  1.1616 -      assume "content (cbox a b) \<noteq> 0"
  1.1617 -      note ab = this[unfolded content_lt_nz[symmetric] content_pos_lt_eq]
  1.1618 -      then have ab': "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
  1.1619 -        by (auto intro!: less_imp_le)
  1.1620 -      show "F g d = g (cbox a b)"
  1.1621 -      proof (cases "division_points (cbox a b) d = {}")
  1.1622 -        case True
  1.1623 -        { fix u v and j :: 'b
  1.1624 -          assume j: "j \<in> Basis" and as: "cbox u v \<in> d"
  1.1625 -          then have "cbox u v \<noteq> {}"
  1.1626 -            using less.prems by blast
  1.1627 -          then have uv: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" "u\<bullet>j \<le> v\<bullet>j"
  1.1628 -            using j unfolding box_ne_empty by auto
  1.1629 -          have *: "\<And>p r Q. \<not> j\<in>Basis \<or> p \<or> r \<or> (\<forall>x\<in>d. Q x) \<Longrightarrow> p \<or> r \<or> Q (cbox u v)"
  1.1630 -            using as j by auto
  1.1631 -          have "(j, u\<bullet>j) \<notin> division_points (cbox a b) d"
  1.1632 -               "(j, v\<bullet>j) \<notin> division_points (cbox a b) d" using True by auto
  1.1633 -          note this[unfolded de_Morgan_conj division_points_def mem_Collect_eq split_conv interval_bounds[OF ab'] bex_simps]
  1.1634 -          note *[OF this(1)] *[OF this(2)] note this[unfolded interval_bounds[OF uv(1)]]
  1.1635 -          moreover
  1.1636 -          have "a\<bullet>j \<le> u\<bullet>j" "v\<bullet>j \<le> b\<bullet>j"
  1.1637 -            using division_ofD(2,2,3)[OF \<open>d division_of cbox a b\<close> as]
  1.1638 -            apply (metis j subset_box(1) uv(1))
  1.1639 -            by (metis \<open>cbox u v \<subseteq> cbox a b\<close> j subset_box(1) uv(1))
  1.1640 -          ultimately have "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"
  1.1641 -            unfolding not_less de_Morgan_disj using ab[rule_format,of j] uv(2) j by force }
  1.1642 -        then have d': "\<forall>i\<in>d. \<exists>u v. i = cbox u v \<and>
  1.1643 -          (\<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)"
  1.1644 -          unfolding forall_in_division[OF less.prems] by blast
  1.1645 -        have "(1/2) *\<^sub>R (a+b) \<in> cbox a b"
  1.1646 -          unfolding mem_box using ab by(auto intro!: less_imp_le simp: inner_simps)
  1.1647 -        note this[unfolded division_ofD(6)[OF \<open>d division_of cbox a b\<close>,symmetric] Union_iff]
  1.1648 -        then guess i .. note i=this
  1.1649 -        guess u v using d'[rule_format,OF i(1)] by (elim exE conjE) note uv=this
  1.1650 -        have "cbox a b \<in> d"
  1.1651 -        proof -
  1.1652 -          have "u = a" "v = b"
  1.1653 -            unfolding euclidean_eq_iff[where 'a='b]
  1.1654 -          proof safe
  1.1655 -            fix j :: 'b
  1.1656 -            assume j: "j \<in> Basis"
  1.1657 -            note i(2)[unfolded uv mem_box,rule_format,of j]
  1.1658 -            then show "u \<bullet> j = a \<bullet> j" and "v \<bullet> j = b \<bullet> j"
  1.1659 -              using uv(2)[rule_format,of j] j by (auto simp: inner_simps)
  1.1660 -          qed
  1.1661 -          then have "i = cbox a b" using uv by auto
  1.1662 -          then show ?thesis using i by auto
  1.1663 -        qed
  1.1664 -        then have deq: "d = insert (cbox a b) (d - {cbox a b})"
  1.1665 -          by auto
  1.1666 -        have "F g (d - {cbox a b}) = \<^bold>1"
  1.1667 -        proof (intro neutral ballI)
  1.1668 -          fix x
  1.1669 -          assume x: "x \<in> d - {cbox a b}"
  1.1670 -          then have "x\<in>d"
  1.1671 -            by auto note d'[rule_format,OF this]
  1.1672 -          then guess u v by (elim exE conjE) note uv=this
  1.1673 -          have "u \<noteq> a \<or> v \<noteq> b"
  1.1674 -            using x[unfolded uv] by auto
  1.1675 -          then obtain j where "u\<bullet>j \<noteq> a\<bullet>j \<or> v\<bullet>j \<noteq> b\<bullet>j" and j: "j \<in> Basis"
  1.1676 -            unfolding euclidean_eq_iff[where 'a='b] by auto
  1.1677 -          then have "u\<bullet>j = v\<bullet>j"
  1.1678 -            using uv(2)[rule_format,OF j] by auto
  1.1679 -          then have "content (cbox u v) = 0"
  1.1680 -            unfolding content_eq_0 using j
  1.1681 -            by force
  1.1682 -          then show "g x = \<^bold>1"
  1.1683 -            unfolding uv(1) by (rule operativeD(1)[OF g])
  1.1684 -        qed
  1.1685 -        then show "F g d = g (cbox a b)"
  1.1686 -          using division_ofD[OF less.prems]
  1.1687 -          apply (subst deq)
  1.1688 -          apply (subst insert)
  1.1689 -          apply auto
  1.1690 -          done
  1.1691 -      next
  1.1692 -        case False
  1.1693 -        then have "\<exists>x. x \<in> division_points (cbox a b) d"
  1.1694 -          by auto
  1.1695 -        then guess k c
  1.1696 -          unfolding split_paired_Ex division_points_def mem_Collect_eq split_conv
  1.1697 -          apply (elim exE conjE)
  1.1698 -          done
  1.1699 -        note this(2-4,1) note kc=this[unfolded interval_bounds[OF ab']]
  1.1700 -        from this(3) guess j .. note j=this
  1.1701 -        define d1 where "d1 = {l \<inter> {x. x\<bullet>k \<le> c} | l. l \<in> d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
  1.1702 -        define d2 where "d2 = {l \<inter> {x. x\<bullet>k \<ge> c} | l. l \<in> d \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
  1.1703 -        define cb where "cb = (\<Sum>i\<in>Basis. (if i = k then c else b\<bullet>i) *\<^sub>R i)"
  1.1704 -        define ca where "ca = (\<Sum>i\<in>Basis. (if i = k then c else a\<bullet>i) *\<^sub>R i)"
  1.1705 -        note division_points_psubset[OF \<open>d division_of cbox a b\<close> ab kc(1-2) j]
  1.1706 -        note psubset_card_mono[OF _ this(1)] psubset_card_mono[OF _ this(2)]
  1.1707 -        then have *: "F g d1 = g (cbox a b \<inter> {x. x\<bullet>k \<le> c})" "F g d2 = g (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
  1.1708 -          unfolding interval_split[OF kc(4)]
  1.1709 -          apply (rule_tac[!] "less.hyps"[rule_format])
  1.1710 -          using division_split[OF \<open>d division_of cbox a b\<close>, where k=k and c=c]
  1.1711 -          apply (simp_all add: interval_split kc d1_def d2_def division_points_finite[OF \<open>d division_of cbox a b\<close>])
  1.1712 -          done
  1.1713 -        { fix l y
  1.1714 -          assume as: "l \<in> d" "y \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} = y \<inter> {x. x \<bullet> k \<le> c}" "l \<noteq> y"
  1.1715 -          from division_ofD(4)[OF \<open>d division_of cbox a b\<close> this(1)] guess u v by (elim exE) note leq=this
  1.1716 -          have "g (l \<inter> {x. x \<bullet> k \<le> c}) = \<^bold>1"
  1.1717 -            unfolding leq interval_split[OF kc(4)]
  1.1718 -            apply (rule operativeD[OF g])
  1.1719 -            unfolding interval_split[symmetric, OF kc(4)]
  1.1720 -            using division_split_left_inj less as kc leq by blast
  1.1721 -        } note fxk_le = this
  1.1722 -        { fix l y
  1.1723 -          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"
  1.1724 -          from division_ofD(4)[OF \<open>d division_of cbox a b\<close> this(1)] guess u v by (elim exE) note leq=this
  1.1725 -          have "g (l \<inter> {x. x \<bullet> k \<ge> c}) = \<^bold>1"
  1.1726 -            unfolding leq interval_split[OF kc(4)]
  1.1727 -            apply (rule operativeD(1)[OF g])
  1.1728 -            unfolding interval_split[symmetric,OF kc(4)]
  1.1729 -            using division_split_right_inj less leq as kc by blast
  1.1730 -        } note fxk_ge = this
  1.1731 -        have d1_alt: "d1 = (\<lambda>l. l \<inter> {x. x\<bullet>k \<le> c}) ` {l \<in> d. l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
  1.1732 -          using d1_def by auto
  1.1733 -        have d2_alt: "d2 = (\<lambda>l. l \<inter> {x. x\<bullet>k \<ge> c}) ` {l \<in> d. l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
  1.1734 -          using d2_def by auto
  1.1735 -        have "g (cbox a b) = F g d1 \<^bold>* F g d2" (is "_ = ?prev")
  1.1736 -          unfolding * using g kc(4) by blast
  1.1737 -        also have "F g d1 = F (\<lambda>l. g (l \<inter> {x. x\<bullet>k \<le> c})) d"
  1.1738 -          unfolding d1_alt using division_of_finite[OF less.prems] fxk_le
  1.1739 -          by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left simp: operative_empty[OF g])
  1.1740 -        also have "F g d2 = F (\<lambda>l. g (l \<inter> {x. x\<bullet>k \<ge> c})) d"
  1.1741 -          unfolding d2_alt using division_of_finite[OF less.prems] fxk_ge
  1.1742 -          by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left simp: operative_empty[OF g])
  1.1743 -        also have *: "\<forall>x\<in>d. g x = g (x \<inter> {x. x \<bullet> k \<le> c}) \<^bold>* g (x \<inter> {x. c \<le> x \<bullet> k})"
  1.1744 -          unfolding forall_in_division[OF \<open>d division_of cbox a b\<close>]
  1.1745 -          using g kc(4) by blast
  1.1746 -        have "F (\<lambda>l. g (l \<inter> {x. x\<bullet>k \<le> c})) d \<^bold>* F (\<lambda>l. g (l \<inter> {x. x\<bullet>k \<ge> c})) d = F g d"
  1.1747 -          using * by (simp add: distrib)
  1.1748 -        finally show ?thesis by auto
  1.1749 -      qed
  1.1750 -    qed
  1.1751 -  qed
  1.1752 -qed
  1.1753 -
  1.1754 -lemma (in comm_monoid_set) operative_tagged_division:
  1.1755 -  assumes f: "operative g" and d: "d tagged_division_of (cbox a b)"
  1.1756 -  shows "F (\<lambda>(x, l). g l) d = g (cbox a b)"
  1.1757 -  unfolding d[THEN division_of_tagged_division, THEN operative_division[OF f], symmetric]
  1.1758 -  by (simp add: f[THEN operativeD(1)] over_tagged_division_lemma[OF d])
  1.1759 +  by (force simp add: add.operative_def content_split[symmetric] content_eq_0_interior)
  1.1760  
  1.1761  lemma additive_content_division: "d division_of (cbox a b) \<Longrightarrow> setsum content d = content (cbox a b)"
  1.1762    by (metis operative_content setsum.operative_division)
  1.1763 @@ -1835,537 +209,8 @@
  1.1764  lemma content_real_eq_0: "content {a .. b::real} = 0 \<longleftrightarrow> a \<ge> b"
  1.1765    by (metis atLeastatMost_empty_iff2 content_empty content_real diff_self eq_iff le_cases le_iff_diff_le_0)
  1.1766  
  1.1767 -lemma interval_real_split:
  1.1768 -  "{a .. b::real} \<inter> {x. x \<le> c} = {a .. min b c}"
  1.1769 -  "{a .. b} \<inter> {x. c \<le> x} = {max a c .. b}"
  1.1770 -  apply (metis Int_atLeastAtMostL1 atMost_def)
  1.1771 -  apply (metis Int_atLeastAtMostL2 atLeast_def)
  1.1772 -  done
  1.1773 -
  1.1774 -lemma (in comm_monoid) operative_1_lt:
  1.1775 -  "operative (g :: real set \<Rightarrow> 'a) \<longleftrightarrow>
  1.1776 -    ((\<forall>a b. b \<le> a \<longrightarrow> g {a .. b} = \<^bold>1) \<and> (\<forall>a b c. a < c \<and> c < b \<longrightarrow> g {a .. c} \<^bold>* g {c .. b} = g {a .. b}))"
  1.1777 -  apply (simp add: operative_def content_real_eq_0 atMost_def[symmetric] atLeast_def[symmetric]
  1.1778 -              del: content_real_if)
  1.1779 -proof safe
  1.1780 -  fix a b c :: real
  1.1781 -  assume *: "\<forall>a b c. g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}"
  1.1782 -  assume "a < c" "c < b"
  1.1783 -  with *[rule_format, of a b c] show "g {a..c} \<^bold>* g {c..b} = g {a..b}"
  1.1784 -    by (simp add: less_imp_le min.absorb2 max.absorb2)
  1.1785 -next
  1.1786 -  fix a b c :: real
  1.1787 -  assume as: "\<forall>a b. b \<le> a \<longrightarrow> g {a..b} = \<^bold>1"
  1.1788 -    "\<forall>a b c. a < c \<and> c < b \<longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
  1.1789 -  from as(1)[rule_format, of 0 1] as(1)[rule_format, of a a for a] as(2)
  1.1790 -  have [simp]: "g {} = \<^bold>1" "\<And>a. g {a} = \<^bold>1"
  1.1791 -    "\<And>a b c. a < c \<Longrightarrow> c < b \<Longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
  1.1792 -    by auto
  1.1793 -  show "g {a..b} = g {a..min b c} \<^bold>* g {max a c..b}"
  1.1794 -    by (auto simp: min_def max_def le_less)
  1.1795 -qed
  1.1796 -
  1.1797 -lemma (in comm_monoid) operative_1_le:
  1.1798 -  "operative (g :: real set \<Rightarrow> 'a) \<longleftrightarrow>
  1.1799 -    ((\<forall>a b. b \<le> a \<longrightarrow> g {a..b} = \<^bold>1) \<and> (\<forall>a b c. a \<le> c \<and> c \<le> b \<longrightarrow> g {a .. c} \<^bold>* g {c .. b} = g {a .. b}))"
  1.1800 -  unfolding operative_1_lt
  1.1801 -proof safe
  1.1802 -  fix a b c :: real
  1.1803 -  assume as: "\<forall>a b c. a \<le> c \<and> c \<le> b \<longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}" "a < c" "c < b"
  1.1804 -  show "g {a..c} \<^bold>* g {c..b} = g {a..b}"
  1.1805 -    apply (rule as(1)[rule_format])
  1.1806 -    using as(2-)
  1.1807 -    apply auto
  1.1808 -    done
  1.1809 -next
  1.1810 -  fix a b c :: real
  1.1811 -  assume "\<forall>a b. b \<le> a \<longrightarrow> g {a .. b} = \<^bold>1"
  1.1812 -    and "\<forall>a b c. a < c \<and> c < b \<longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
  1.1813 -    and "a \<le> c"
  1.1814 -    and "c \<le> b"
  1.1815 -  note as = this[rule_format]
  1.1816 -  show "g {a..c} \<^bold>* g {c..b} = g {a..b}"
  1.1817 -  proof (cases "c = a \<or> c = b")
  1.1818 -    case False
  1.1819 -    then show ?thesis
  1.1820 -      apply -
  1.1821 -      apply (subst as(2))
  1.1822 -      using as(3-)
  1.1823 -      apply auto
  1.1824 -      done
  1.1825 -  next
  1.1826 -    case True
  1.1827 -    then show ?thesis
  1.1828 -    proof
  1.1829 -      assume *: "c = a"
  1.1830 -      then have "g {a .. c} = \<^bold>1"
  1.1831 -        apply -
  1.1832 -        apply (rule as(1)[rule_format])
  1.1833 -        apply auto
  1.1834 -        done
  1.1835 -      then show ?thesis
  1.1836 -        unfolding * by auto
  1.1837 -    next
  1.1838 -      assume *: "c = b"
  1.1839 -      then have "g {c .. b} = \<^bold>1"
  1.1840 -        apply -
  1.1841 -        apply (rule as(1)[rule_format])
  1.1842 -        apply auto
  1.1843 -        done
  1.1844 -      then show ?thesis
  1.1845 -        unfolding * by auto
  1.1846 -    qed
  1.1847 -  qed
  1.1848 -qed
  1.1849 -
  1.1850 -subsection \<open>Fine-ness of a partition w.r.t. a gauge.\<close>
  1.1851 -
  1.1852 -definition fine  (infixr "fine" 46)
  1.1853 -  where "d fine s \<longleftrightarrow> (\<forall>(x,k) \<in> s. k \<subseteq> d x)"
  1.1854 -
  1.1855 -lemma fineI:
  1.1856 -  assumes "\<And>x k. (x, k) \<in> s \<Longrightarrow> k \<subseteq> d x"
  1.1857 -  shows "d fine s"
  1.1858 -  using assms unfolding fine_def by auto
  1.1859 -
  1.1860 -lemma fineD[dest]:
  1.1861 -  assumes "d fine s"
  1.1862 -  shows "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> d x"
  1.1863 -  using assms unfolding fine_def by auto
  1.1864 -
  1.1865 -lemma fine_inter: "(\<lambda>x. d1 x \<inter> d2 x) fine p \<longleftrightarrow> d1 fine p \<and> d2 fine p"
  1.1866 -  unfolding fine_def by auto
  1.1867 -
  1.1868 -lemma fine_inters:
  1.1869 - "(\<lambda>x. \<Inter>{f d x | d.  d \<in> s}) fine p \<longleftrightarrow> (\<forall>d\<in>s. (f d) fine p)"
  1.1870 -  unfolding fine_def by blast
  1.1871 -
  1.1872 -lemma fine_union: "d fine p1 \<Longrightarrow> d fine p2 \<Longrightarrow> d fine (p1 \<union> p2)"
  1.1873 -  unfolding fine_def by blast
  1.1874 -
  1.1875 -lemma fine_unions: "(\<And>p. p \<in> ps \<Longrightarrow> d fine p) \<Longrightarrow> d fine (\<Union>ps)"
  1.1876 -  unfolding fine_def by auto
  1.1877 -
  1.1878 -lemma fine_subset: "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p"
  1.1879 -  unfolding fine_def by blast
  1.1880 -
  1.1881 -subsection \<open>Some basic combining lemmas.\<close>
  1.1882 -
  1.1883 -lemma tagged_division_unions_exists:
  1.1884 -  assumes "finite iset"
  1.1885 -    and "\<forall>i\<in>iset. \<exists>p. p tagged_division_of i \<and> d fine p"
  1.1886 -    and "\<forall>i1\<in>iset. \<forall>i2\<in>iset. i1 \<noteq> i2 \<longrightarrow> interior i1 \<inter> interior i2 = {}"
  1.1887 -    and "\<Union>iset = i"
  1.1888 -   obtains p where "p tagged_division_of i" and "d fine p"
  1.1889 -proof -
  1.1890 -  obtain pfn where pfn:
  1.1891 -    "\<And>x. x \<in> iset \<Longrightarrow> pfn x tagged_division_of x"
  1.1892 -    "\<And>x. x \<in> iset \<Longrightarrow> d fine pfn x"
  1.1893 -    using bchoice[OF assms(2)] by auto
  1.1894 -  show thesis
  1.1895 -    apply (rule_tac p="\<Union>(pfn ` iset)" in that)
  1.1896 -    using assms(1) assms(3) assms(4) pfn(1) tagged_division_unions apply force
  1.1897 -    by (metis (mono_tags, lifting) fine_unions imageE pfn(2))
  1.1898 -qed
  1.1899 -
  1.1900 -
  1.1901 -subsection \<open>The set we're concerned with must be closed.\<close>
  1.1902 -
  1.1903 -lemma division_of_closed:
  1.1904 -  fixes i :: "'n::euclidean_space set"
  1.1905 -  shows "s division_of i \<Longrightarrow> closed i"
  1.1906 -  unfolding division_of_def by fastforce
  1.1907 -
  1.1908 -subsection \<open>General bisection principle for intervals; might be useful elsewhere.\<close>
  1.1909 -
  1.1910 -lemma interval_bisection_step:
  1.1911 -  fixes type :: "'a::euclidean_space"
  1.1912 -  assumes "P {}"
  1.1913 -    and "\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P (s \<union> t)"
  1.1914 -    and "\<not> P (cbox a (b::'a))"
  1.1915 -  obtains c d where "\<not> P (cbox c d)"
  1.1916 -    and "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
  1.1917 -proof -
  1.1918 -  have "cbox a b \<noteq> {}"
  1.1919 -    using assms(1,3) by metis
  1.1920 -  then have ab: "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
  1.1921 -    by (force simp: mem_box)
  1.1922 -  { fix f
  1.1923 -    have "\<lbrakk>finite f;
  1.1924 -           \<And>s. s\<in>f \<Longrightarrow> P s;
  1.1925 -           \<And>s. s\<in>f \<Longrightarrow> \<exists>a b. s = cbox a b;
  1.1926 -           \<And>s t. s\<in>f \<Longrightarrow> t\<in>f \<Longrightarrow> s \<noteq> t \<Longrightarrow> interior s \<inter> interior t = {}\<rbrakk> \<Longrightarrow> P (\<Union>f)"
  1.1927 -    proof (induct f rule: finite_induct)
  1.1928 -      case empty
  1.1929 -      show ?case
  1.1930 -        using assms(1) by auto
  1.1931 -    next
  1.1932 -      case (insert x f)
  1.1933 -      show ?case
  1.1934 -        unfolding Union_insert
  1.1935 -        apply (rule assms(2)[rule_format])
  1.1936 -        using inter_interior_unions_intervals [of f "interior x"]
  1.1937 -        apply (auto simp: insert)
  1.1938 -        by (metis IntI empty_iff insert.hyps(2) insert.prems(3) insert_iff)
  1.1939 -    qed
  1.1940 -  } note UN_cases = this
  1.1941 -  let ?A = "{cbox c d | c d::'a. \<forall>i\<in>Basis. (c\<bullet>i = a\<bullet>i) \<and> (d\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<or>
  1.1942 -    (c\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<and> (d\<bullet>i = b\<bullet>i)}"
  1.1943 -  let ?PP = "\<lambda>c d. \<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
  1.1944 -  {
  1.1945 -    presume "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d) \<Longrightarrow> False"
  1.1946 -    then show thesis
  1.1947 -      unfolding atomize_not not_all
  1.1948 -      by (blast intro: that)
  1.1949 -  }
  1.1950 -  assume as: "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d)"
  1.1951 -  have "P (\<Union>?A)"
  1.1952 -  proof (rule UN_cases)
  1.1953 -    let ?B = "(\<lambda>s. cbox (\<Sum>i\<in>Basis. (if i \<in> s then a\<bullet>i else (a\<bullet>i + b\<bullet>i) / 2) *\<^sub>R i::'a)
  1.1954 -      (\<Sum>i\<in>Basis. (if i \<in> s then (a\<bullet>i + b\<bullet>i) / 2 else b\<bullet>i) *\<^sub>R i)) ` {s. s \<subseteq> Basis}"
  1.1955 -    have "?A \<subseteq> ?B"
  1.1956 -    proof
  1.1957 -      fix x
  1.1958 -      assume "x \<in> ?A"
  1.1959 -      then obtain c d
  1.1960 -        where x:  "x = cbox c d"
  1.1961 -                  "\<And>i. i \<in> Basis \<Longrightarrow>
  1.1962 -                        c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
  1.1963 -                        c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i" by blast
  1.1964 -      show "x \<in> ?B"
  1.1965 -        unfolding image_iff x
  1.1966 -        apply (rule_tac x="{i. i\<in>Basis \<and> c\<bullet>i = a\<bullet>i}" in bexI)
  1.1967 -        apply (rule arg_cong2 [where f = cbox])
  1.1968 -        using x(2) ab
  1.1969 -        apply (auto simp add: euclidean_eq_iff[where 'a='a])
  1.1970 -        by fastforce
  1.1971 -    qed
  1.1972 -    then show "finite ?A"
  1.1973 -      by (rule finite_subset) auto
  1.1974 -  next
  1.1975 -    fix s
  1.1976 -    assume "s \<in> ?A"
  1.1977 -    then obtain c d
  1.1978 -      where s: "s = cbox c d"
  1.1979 -               "\<And>i. i \<in> Basis \<Longrightarrow>
  1.1980 -                     c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
  1.1981 -                     c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
  1.1982 -      by blast
  1.1983 -    show "P s"
  1.1984 -      unfolding s
  1.1985 -      apply (rule as[rule_format])
  1.1986 -      using ab s(2) by force
  1.1987 -    show "\<exists>a b. s = cbox a b"
  1.1988 -      unfolding s by auto
  1.1989 -    fix t
  1.1990 -    assume "t \<in> ?A"
  1.1991 -    then obtain e f where t:
  1.1992 -      "t = cbox e f"
  1.1993 -      "\<And>i. i \<in> Basis \<Longrightarrow>
  1.1994 -        e \<bullet> i = a \<bullet> i \<and> f \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
  1.1995 -        e \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> f \<bullet> i = b \<bullet> i"
  1.1996 -      by blast
  1.1997 -    assume "s \<noteq> t"
  1.1998 -    then have "\<not> (c = e \<and> d = f)"
  1.1999 -      unfolding s t by auto
  1.2000 -    then obtain i where "c\<bullet>i \<noteq> e\<bullet>i \<or> d\<bullet>i \<noteq> f\<bullet>i" and i': "i \<in> Basis"
  1.2001 -      unfolding euclidean_eq_iff[where 'a='a] by auto
  1.2002 -    then have i: "c\<bullet>i \<noteq> e\<bullet>i" "d\<bullet>i \<noteq> f\<bullet>i"
  1.2003 -      using s(2) t(2) apply fastforce
  1.2004 -      using t(2)[OF i'] \<open>c \<bullet> i \<noteq> e \<bullet> i \<or> d \<bullet> i \<noteq> f \<bullet> i\<close> i' s(2) t(2) by fastforce
  1.2005 -    have *: "\<And>s t. (\<And>a. a \<in> s \<Longrightarrow> a \<in> t \<Longrightarrow> False) \<Longrightarrow> s \<inter> t = {}"
  1.2006 -      by auto
  1.2007 -    show "interior s \<inter> interior t = {}"
  1.2008 -      unfolding s t interior_cbox
  1.2009 -    proof (rule *)
  1.2010 -      fix x
  1.2011 -      assume "x \<in> box c d" "x \<in> box e f"
  1.2012 -      then have x: "c\<bullet>i < d\<bullet>i" "e\<bullet>i < f\<bullet>i" "c\<bullet>i < f\<bullet>i" "e\<bullet>i < d\<bullet>i"
  1.2013 -        unfolding mem_box using i'
  1.2014 -        by force+
  1.2015 -      show False  using s(2)[OF i']
  1.2016 -      proof safe
  1.2017 -        assume as: "c \<bullet> i = a \<bullet> i" "d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2"
  1.2018 -        show False
  1.2019 -          using t(2)[OF i'] and i x unfolding as by (fastforce simp add:field_simps)
  1.2020 -      next
  1.2021 -        assume as: "c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2" "d \<bullet> i = b \<bullet> i"
  1.2022 -        show False
  1.2023 -          using t(2)[OF i'] and i x unfolding as by(fastforce simp add:field_simps)
  1.2024 -      qed
  1.2025 -    qed
  1.2026 -  qed
  1.2027 -  also have "\<Union>?A = cbox a b"
  1.2028 -  proof (rule set_eqI,rule)
  1.2029 -    fix x
  1.2030 -    assume "x \<in> \<Union>?A"
  1.2031 -    then obtain c d where x:
  1.2032 -      "x \<in> cbox c d"
  1.2033 -      "\<And>i. i \<in> Basis \<Longrightarrow>
  1.2034 -        c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
  1.2035 -        c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
  1.2036 -      by blast
  1.2037 -    show "x\<in>cbox a b"
  1.2038 -      unfolding mem_box
  1.2039 -    proof safe
  1.2040 -      fix i :: 'a
  1.2041 -      assume i: "i \<in> Basis"
  1.2042 -      then show "a \<bullet> i \<le> x \<bullet> i" "x \<bullet> i \<le> b \<bullet> i"
  1.2043 -        using x(2)[OF i] x(1)[unfolded mem_box,THEN bspec, OF i] by auto
  1.2044 -    qed
  1.2045 -  next
  1.2046 -    fix x
  1.2047 -    assume x: "x \<in> cbox a b"
  1.2048 -    have "\<forall>i\<in>Basis.
  1.2049 -      \<exists>c d. (c = a\<bullet>i \<and> d = (a\<bullet>i + b\<bullet>i) / 2 \<or> c = (a\<bullet>i + b\<bullet>i) / 2 \<and> d = b\<bullet>i) \<and> c\<le>x\<bullet>i \<and> x\<bullet>i \<le> d"
  1.2050 -      (is "\<forall>i\<in>Basis. \<exists>c d. ?P i c d")
  1.2051 -      unfolding mem_box
  1.2052 -    proof
  1.2053 -      fix i :: 'a
  1.2054 -      assume i: "i \<in> Basis"
  1.2055 -      have "?P i (a\<bullet>i) ((a \<bullet> i + b \<bullet> i) / 2) \<or> ?P i ((a \<bullet> i + b \<bullet> i) / 2) (b\<bullet>i)"
  1.2056 -        using x[unfolded mem_box,THEN bspec, OF i] by auto
  1.2057 -      then show "\<exists>c d. ?P i c d"
  1.2058 -        by blast
  1.2059 -    qed
  1.2060 -    then show "x\<in>\<Union>?A"
  1.2061 -      unfolding Union_iff Bex_def mem_Collect_eq choice_Basis_iff
  1.2062 -      apply auto
  1.2063 -      apply (rule_tac x="cbox xa xaa" in exI)
  1.2064 -      unfolding mem_box
  1.2065 -      apply auto
  1.2066 -      done
  1.2067 -  qed
  1.2068 -  finally show False
  1.2069 -    using assms by auto
  1.2070 -qed
  1.2071 -
  1.2072 -lemma interval_bisection:
  1.2073 -  fixes type :: "'a::euclidean_space"
  1.2074 -  assumes "P {}"
  1.2075 -    and "(\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P(s \<union> t))"
  1.2076 -    and "\<not> P (cbox a (b::'a))"
  1.2077 -  obtains x where "x \<in> cbox a b"
  1.2078 -    and "\<forall>e>0. \<exists>c d. x \<in> cbox c d \<and> cbox c d \<subseteq> ball x e \<and> cbox c d \<subseteq> cbox a b \<and> \<not> P (cbox c d)"
  1.2079 -proof -
  1.2080 -  have "\<forall>x. \<exists>y. \<not> P (cbox (fst x) (snd x)) \<longrightarrow> (\<not> P (cbox (fst y) (snd y)) \<and>
  1.2081 -    (\<forall>i\<in>Basis. fst x\<bullet>i \<le> fst y\<bullet>i \<and> fst y\<bullet>i \<le> snd y\<bullet>i \<and> snd y\<bullet>i \<le> snd x\<bullet>i \<and>
  1.2082 -       2 * (snd y\<bullet>i - fst y\<bullet>i) \<le> snd x\<bullet>i - fst x\<bullet>i))" (is "\<forall>x. ?P x")
  1.2083 -  proof
  1.2084 -    show "?P x" for x
  1.2085 -    proof (cases "P (cbox (fst x) (snd x))")
  1.2086 -      case True
  1.2087 -      then show ?thesis by auto
  1.2088 -    next
  1.2089 -      case as: False
  1.2090 -      obtain c d where "\<not> P (cbox c d)"
  1.2091 -        "\<forall>i\<in>Basis.
  1.2092 -           fst x \<bullet> i \<le> c \<bullet> i \<and>
  1.2093 -           c \<bullet> i \<le> d \<bullet> i \<and>
  1.2094 -           d \<bullet> i \<le> snd x \<bullet> i \<and>
  1.2095 -           2 * (d \<bullet> i - c \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i"
  1.2096 -        by (rule interval_bisection_step[of P, OF assms(1-2) as])
  1.2097 -      then show ?thesis
  1.2098 -        apply -
  1.2099 -        apply (rule_tac x="(c,d)" in exI)
  1.2100 -        apply auto
  1.2101 -        done
  1.2102 -    qed
  1.2103 -  qed
  1.2104 -  then obtain f where f:
  1.2105 -    "\<forall>x.
  1.2106 -      \<not> P (cbox (fst x) (snd x)) \<longrightarrow>
  1.2107 -      \<not> P (cbox (fst (f x)) (snd (f x))) \<and>
  1.2108 -        (\<forall>i\<in>Basis.
  1.2109 -            fst x \<bullet> i \<le> fst (f x) \<bullet> i \<and>
  1.2110 -            fst (f x) \<bullet> i \<le> snd (f x) \<bullet> i \<and>
  1.2111 -            snd (f x) \<bullet> i \<le> snd x \<bullet> i \<and>
  1.2112 -            2 * (snd (f x) \<bullet> i - fst (f x) \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i)"
  1.2113 -    apply -
  1.2114 -    apply (drule choice)
  1.2115 -    apply blast
  1.2116 -    done
  1.2117 -  define AB A B where ab_def: "AB n = (f ^^ n) (a,b)" "A n = fst(AB n)" "B n = snd(AB n)" for n
  1.2118 -  have "A 0 = a" "B 0 = b" "\<And>n. \<not> P (cbox (A(Suc n)) (B(Suc n))) \<and>
  1.2119 -    (\<forall>i\<in>Basis. A(n)\<bullet>i \<le> A(Suc n)\<bullet>i \<and> A(Suc n)\<bullet>i \<le> B(Suc n)\<bullet>i \<and> B(Suc n)\<bullet>i \<le> B(n)\<bullet>i \<and>
  1.2120 -    2 * (B(Suc n)\<bullet>i - A(Suc n)\<bullet>i) \<le> B(n)\<bullet>i - A(n)\<bullet>i)" (is "\<And>n. ?P n")
  1.2121 -  proof -
  1.2122 -    show "A 0 = a" "B 0 = b"
  1.2123 -      unfolding ab_def by auto
  1.2124 -    note S = ab_def funpow.simps o_def id_apply
  1.2125 -    show "?P n" for n
  1.2126 -    proof (induct n)
  1.2127 -      case 0
  1.2128 -      then show ?case
  1.2129 -        unfolding S
  1.2130 -        apply (rule f[rule_format]) using assms(3)
  1.2131 -        apply auto
  1.2132 -        done
  1.2133 -    next
  1.2134 -      case (Suc n)
  1.2135 -      show ?case
  1.2136 -        unfolding S
  1.2137 -        apply (rule f[rule_format])
  1.2138 -        using Suc
  1.2139 -        unfolding S
  1.2140 -        apply auto
  1.2141 -        done
  1.2142 -    qed
  1.2143 -  qed
  1.2144 -  note AB = this(1-2) conjunctD2[OF this(3),rule_format]
  1.2145 -
  1.2146 -  have interv: "\<exists>n. \<forall>x\<in>cbox (A n) (B n). \<forall>y\<in>cbox (A n) (B n). dist x y < e"
  1.2147 -    if e: "0 < e" for e
  1.2148 -  proof -
  1.2149 -    obtain n where n: "(\<Sum>i\<in>Basis. b \<bullet> i - a \<bullet> i) / e < 2 ^ n"
  1.2150 -      using real_arch_pow[of 2 "(setsum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis) / e"] by auto
  1.2151 -    show ?thesis
  1.2152 -    proof (rule exI [where x=n], clarify)
  1.2153 -      fix x y
  1.2154 -      assume xy: "x\<in>cbox (A n) (B n)" "y\<in>cbox (A n) (B n)"
  1.2155 -      have "dist x y \<le> setsum (\<lambda>i. \<bar>(x - y)\<bullet>i\<bar>) Basis"
  1.2156 -        unfolding dist_norm by(rule norm_le_l1)
  1.2157 -      also have "\<dots> \<le> setsum (\<lambda>i. B n\<bullet>i - A n\<bullet>i) Basis"
  1.2158 -      proof (rule setsum_mono)
  1.2159 -        fix i :: 'a
  1.2160 -        assume i: "i \<in> Basis"
  1.2161 -        show "\<bar>(x - y) \<bullet> i\<bar> \<le> B n \<bullet> i - A n \<bullet> i"
  1.2162 -          using xy[unfolded mem_box,THEN bspec, OF i]
  1.2163 -          by (auto simp: inner_diff_left)
  1.2164 -      qed
  1.2165 -      also have "\<dots> \<le> setsum (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis / 2^n"
  1.2166 -        unfolding setsum_divide_distrib
  1.2167 -      proof (rule setsum_mono)
  1.2168 -        show "B n \<bullet> i - A n \<bullet> i \<le> (b \<bullet> i - a \<bullet> i) / 2 ^ n" if i: "i \<in> Basis" for i
  1.2169 -        proof (induct n)
  1.2170 -          case 0
  1.2171 -          then show ?case
  1.2172 -            unfolding AB by auto
  1.2173 -        next
  1.2174 -          case (Suc n)
  1.2175 -          have "B (Suc n) \<bullet> i - A (Suc n) \<bullet> i \<le> (B n \<bullet> i - A n \<bullet> i) / 2"
  1.2176 -            using AB(4)[of i n] using i by auto
  1.2177 -          also have "\<dots> \<le> (b \<bullet> i - a \<bullet> i) / 2 ^ Suc n"
  1.2178 -            using Suc by (auto simp add: field_simps)
  1.2179 -          finally show ?case .
  1.2180 -        qed
  1.2181 -      qed
  1.2182 -      also have "\<dots> < e"
  1.2183 -        using n using e by (auto simp add: field_simps)
  1.2184 -      finally show "dist x y < e" .
  1.2185 -    qed
  1.2186 -  qed
  1.2187 -  {
  1.2188 -    fix n m :: nat
  1.2189 -    assume "m \<le> n" then have "cbox (A n) (B n) \<subseteq> cbox (A m) (B m)"
  1.2190 -    proof (induction rule: inc_induct)
  1.2191 -      case (step i)
  1.2192 -      show ?case
  1.2193 -        using AB(4) by (intro order_trans[OF step.IH] subset_box_imp) auto
  1.2194 -    qed simp
  1.2195 -  } note ABsubset = this
  1.2196 -  have "\<exists>a. \<forall>n. a\<in> cbox (A n) (B n)"
  1.2197 -    by (rule decreasing_closed_nest[rule_format,OF closed_cbox _ ABsubset interv])
  1.2198 -      (metis nat.exhaust AB(1-3) assms(1,3))
  1.2199 -  then obtain x0 where x0: "\<And>n. x0 \<in> cbox (A n) (B n)"
  1.2200 -    by blast
  1.2201 -  show thesis
  1.2202 -  proof (rule that[rule_format, of x0])
  1.2203 -    show "x0\<in>cbox a b"
  1.2204 -      using x0[of 0] unfolding AB .
  1.2205 -    fix e :: real
  1.2206 -    assume "e > 0"
  1.2207 -    from interv[OF this] obtain n
  1.2208 -      where n: "\<forall>x\<in>cbox (A n) (B n). \<forall>y\<in>cbox (A n) (B n). dist x y < e" ..
  1.2209 -    have "\<not> P (cbox (A n) (B n))"
  1.2210 -      apply (cases "0 < n")
  1.2211 -      using AB(3)[of "n - 1"] assms(3) AB(1-2)
  1.2212 -      apply auto
  1.2213 -      done
  1.2214 -    moreover have "cbox (A n) (B n) \<subseteq> ball x0 e"
  1.2215 -      using n using x0[of n] by auto
  1.2216 -    moreover have "cbox (A n) (B n) \<subseteq> cbox a b"
  1.2217 -      unfolding AB(1-2)[symmetric] by (rule ABsubset) auto
  1.2218 -    ultimately show "\<exists>c d. x0 \<in> cbox c d \<and> cbox c d \<subseteq> ball x0 e \<and> cbox c d \<subseteq> cbox a b \<and> \<not> P (cbox c d)"
  1.2219 -      apply (rule_tac x="A n" in exI)
  1.2220 -      apply (rule_tac x="B n" in exI)
  1.2221 -      apply (auto simp: x0)
  1.2222 -      done
  1.2223 -  qed
  1.2224 -qed
  1.2225 -
  1.2226 -
  1.2227 -subsection \<open>Cousin's lemma.\<close>
  1.2228 -
  1.2229 -lemma fine_division_exists:
  1.2230 -  fixes a b :: "'a::euclidean_space"
  1.2231 -  assumes "gauge g"
  1.2232 -  obtains p where "p tagged_division_of (cbox a b)" "g fine p"
  1.2233 -proof -
  1.2234 -  presume "\<not> (\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p) \<Longrightarrow> False"
  1.2235 -  then obtain p where "p tagged_division_of (cbox a b)" "g fine p"
  1.2236 -    by blast
  1.2237 -  then show thesis ..
  1.2238 -next
  1.2239 -  assume as: "\<not> (\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p)"
  1.2240 -  obtain x where x:
  1.2241 -      "x \<in> (cbox a b)"
  1.2242 -      "\<And>e. 0 < e \<Longrightarrow>
  1.2243 -        \<exists>c d.
  1.2244 -          x \<in> cbox c d \<and>
  1.2245 -          cbox c d \<subseteq> ball x e \<and>
  1.2246 -          cbox c d \<subseteq> (cbox a b) \<and>
  1.2247 -          \<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
  1.2248 -    apply (rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p", OF _ _ as])
  1.2249 -    apply (simp add: fine_def)
  1.2250 -    apply (metis tagged_division_union fine_union)
  1.2251 -    apply (auto simp: )
  1.2252 -    done
  1.2253 -  obtain e where e: "e > 0" "ball x e \<subseteq> g x"
  1.2254 -    using gaugeD[OF assms, of x] unfolding open_contains_ball by auto
  1.2255 -  from x(2)[OF e(1)]
  1.2256 -  obtain c d where c_d: "x \<in> cbox c d"
  1.2257 -                        "cbox c d \<subseteq> ball x e"
  1.2258 -                        "cbox c d \<subseteq> cbox a b"
  1.2259 -                        "\<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
  1.2260 -    by blast
  1.2261 -  have "g fine {(x, cbox c d)}"
  1.2262 -    unfolding fine_def using e using c_d(2) by auto
  1.2263 -  then show False
  1.2264 -    using tagged_division_of_self[OF c_d(1)] using c_d by auto
  1.2265 -qed
  1.2266 -
  1.2267 -lemma fine_division_exists_real:
  1.2268 -  fixes a b :: real
  1.2269 -  assumes "gauge g"
  1.2270 -  obtains p where "p tagged_division_of {a .. b}" "g fine p"
  1.2271 -  by (metis assms box_real(2) fine_division_exists)
  1.2272 -
  1.2273 -subsection \<open>Division filter\<close>
  1.2274 -
  1.2275 -text \<open>Divisions over all gauges towards finer divisions.\<close>
  1.2276 -
  1.2277 -definition division_filter :: "'a::euclidean_space set \<Rightarrow> ('a \<times> 'a set) set filter"
  1.2278 -  where "division_filter s = (INF g:{g. gauge g}. principal {p. p tagged_division_of s \<and> g fine p})"
  1.2279 -
  1.2280 -lemma eventually_division_filter:
  1.2281 -  "(\<forall>\<^sub>F p in division_filter s. P p) \<longleftrightarrow>
  1.2282 -    (\<exists>g. gauge g \<and> (\<forall>p. p tagged_division_of s \<and> g fine p \<longrightarrow> P p))"
  1.2283 -  unfolding division_filter_def
  1.2284 -proof (subst eventually_INF_base; clarsimp)
  1.2285 -  fix g1 g2 :: "'a \<Rightarrow> 'a set" show "gauge g1 \<Longrightarrow> gauge g2 \<Longrightarrow> \<exists>x. gauge x \<and>
  1.2286 -    {p. p tagged_division_of s \<and> x fine p} \<subseteq> {p. p tagged_division_of s \<and> g1 fine p} \<and>
  1.2287 -    {p. p tagged_division_of s \<and> x fine p} \<subseteq> {p. p tagged_division_of s \<and> g2 fine p}"
  1.2288 -    by (intro exI[of _ "\<lambda>x. g1 x \<inter> g2 x"]) (auto simp: fine_inter)
  1.2289 -qed (auto simp: eventually_principal)
  1.2290 -
  1.2291 -lemma division_filter_not_empty: "division_filter (cbox a b) \<noteq> bot"
  1.2292 -  unfolding trivial_limit_def eventually_division_filter
  1.2293 -  by (auto elim: fine_division_exists)
  1.2294 -
  1.2295 -lemma eventually_division_filter_tagged_division:
  1.2296 -  "eventually (\<lambda>p. p tagged_division_of s) (division_filter s)"
  1.2297 -  unfolding eventually_division_filter by (intro exI[of _ "\<lambda>x. ball x 1"]) auto
  1.2298 +lemma property_empty_interval: "\<forall>a b. content (cbox a b) = 0 \<longrightarrow> P (cbox a b) \<Longrightarrow> P {}"
  1.2299 +  using content_empty unfolding empty_as_interval by auto
  1.2300  
  1.2301  subsection \<open>Gauge integral\<close>
  1.2302  
  1.2303 @@ -2443,26 +288,6 @@
  1.2304  lemma has_integral_integral: "f integrable_on s \<longleftrightarrow> (f has_integral (integral s f)) s"
  1.2305    by auto
  1.2306  
  1.2307 -lemma setsum_content_null:
  1.2308 -  assumes "content (cbox a b) = 0"
  1.2309 -    and "p tagged_division_of (cbox a b)"
  1.2310 -  shows "setsum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)"
  1.2311 -proof (rule setsum.neutral, rule)
  1.2312 -  fix y
  1.2313 -  assume y: "y \<in> p"
  1.2314 -  obtain x k where xk: "y = (x, k)"
  1.2315 -    using surj_pair[of y] by blast
  1.2316 -  note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]]
  1.2317 -  from this(2) obtain c d where k: "k = cbox c d" by blast
  1.2318 -  have "(\<lambda>(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x"
  1.2319 -    unfolding xk by auto
  1.2320 -  also have "\<dots> = 0"
  1.2321 -    using content_subset[OF assm(1)[unfolded k]] content_pos_le[of c d]
  1.2322 -    unfolding assms(1) k
  1.2323 -    by auto
  1.2324 -  finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" .
  1.2325 -qed
  1.2326 -
  1.2327  subsection \<open>Basic theorems about integrals.\<close>
  1.2328  
  1.2329  lemma has_integral_unique:
  1.2330 @@ -3175,38 +1000,32 @@
  1.2331  
  1.2332  subsection \<open>Additivity of integral on abutting intervals.\<close>
  1.2333  
  1.2334 -lemma tagged_division_split_left_inj:
  1.2335 -  fixes x1 :: "'a::euclidean_space"
  1.2336 +lemma tagged_division_split_left_inj_content:
  1.2337    assumes d: "d tagged_division_of i"
  1.2338 -    and k12: "(x1, k1) \<in> d"
  1.2339 -             "(x2, k2) \<in> d"
  1.2340 -             "k1 \<noteq> k2"
  1.2341 -             "k1 \<inter> {x. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c}"
  1.2342 -             "k \<in> Basis"
  1.2343 +    and "(x1, k1) \<in> d" "(x2, k2) \<in> d" "k1 \<noteq> k2" "k1 \<inter> {x. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c}" "k \<in> Basis"
  1.2344    shows "content (k1 \<inter> {x. x\<bullet>k \<le> c}) = 0"
  1.2345  proof -
  1.2346 -  have *: "\<And>a b c. (a,b) \<in> c \<Longrightarrow> b \<in> snd ` c"
  1.2347 -    by force
  1.2348 +  from tagged_division_ofD(4)[OF d \<open>(x1, k1) \<in> d\<close>] obtain a b where k1: "k1 = cbox a b"
  1.2349 +    by auto
  1.2350    show ?thesis
  1.2351 -    using k12
  1.2352 -    by (fastforce intro!:  division_split_left_inj[OF division_of_tagged_division[OF d]] *)
  1.2353 +    unfolding k1 interval_split[OF \<open>k \<in> Basis\<close>]
  1.2354 +    unfolding content_eq_0_interior
  1.2355 +    unfolding interval_split[OF \<open>k \<in> Basis\<close>, symmetric] k1[symmetric]
  1.2356 +    by (rule tagged_division_split_left_inj[OF assms])
  1.2357  qed
  1.2358  
  1.2359 -lemma tagged_division_split_right_inj:
  1.2360 -  fixes x1 :: "'a::euclidean_space"
  1.2361 +lemma tagged_division_split_right_inj_content:
  1.2362    assumes d: "d tagged_division_of i"
  1.2363 -    and k12: "(x1, k1) \<in> d"
  1.2364 -             "(x2, k2) \<in> d"
  1.2365 -             "k1 \<noteq> k2"
  1.2366 -             "k1 \<inter> {x. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}"
  1.2367 -             "k \<in> Basis"
  1.2368 +    and "(x1, k1) \<in> d" "(x2, k2) \<in> d" "k1 \<noteq> k2" "k1 \<inter> {x. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}" "k \<in> Basis"
  1.2369    shows "content (k1 \<inter> {x. x\<bullet>k \<ge> c}) = 0"
  1.2370  proof -
  1.2371 -  have *: "\<And>a b c. (a,b) \<in> c \<Longrightarrow> b \<in> snd ` c"
  1.2372 -    by force
  1.2373 +  from tagged_division_ofD(4)[OF d \<open>(x1, k1) \<in> d\<close>] obtain a b where k1: "k1 = cbox a b"
  1.2374 +    by auto
  1.2375    show ?thesis
  1.2376 -    using k12
  1.2377 -    by (fastforce intro!:  division_split_right_inj[OF division_of_tagged_division[OF d]] *)
  1.2378 +    unfolding k1 interval_split[OF \<open>k \<in> Basis\<close>]
  1.2379 +    unfolding content_eq_0_interior
  1.2380 +    unfolding interval_split[OF \<open>k \<in> Basis\<close>, symmetric] k1[symmetric]
  1.2381 +    by (rule tagged_division_split_right_inj[OF assms])
  1.2382  qed
  1.2383  
  1.2384  lemma has_integral_split:
  1.2385 @@ -3284,7 +1103,8 @@
  1.2386      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>
  1.2387                           (\<forall>x k. P x k \<longrightarrow> Q x (f k))"
  1.2388        by auto
  1.2389 -    have fin_finite: "finite {(x,f k) | x k. (x,k) \<in> s \<and> P x k}" if "finite s" for f s P
  1.2390 +    have fin_finite: "finite {(x,f k) | x k. (x,k) \<in> s \<and> P x k}"
  1.2391 +      if "finite s" for s and f :: "'a set \<Rightarrow> 'a set" and P :: "'a \<Rightarrow> 'a set \<Rightarrow> bool"
  1.2392      proof -
  1.2393        from that have "finite ((\<lambda>(x, k). (x, f k)) ` s)"
  1.2394          by auto
  1.2395 @@ -3398,8 +1218,9 @@
  1.2396        also have "\<dots> = (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) +
  1.2397          (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. c \<le> x \<bullet> k}) *\<^sub>R f x) - (i + j)"
  1.2398          unfolding lem3[OF p(3)]
  1.2399 -        by (subst setsum.reindex_nontrivial[OF p(3)], auto intro!: k eq0 tagged_division_split_left_inj[OF p(1)] tagged_division_split_right_inj[OF p(1)]
  1.2400 -              simp: cont_eq)+
  1.2401 +        by (subst (1 2) setsum.reindex_nontrivial[OF p(3)])
  1.2402 +           (auto intro!: k eq0 tagged_division_split_left_inj_content[OF p(1)] tagged_division_split_right_inj_content[OF p(1)]
  1.2403 +                 simp: cont_eq)+
  1.2404        also note setsum.distrib[symmetric]
  1.2405        also have "\<And>x. x \<in> p \<Longrightarrow>
  1.2406                      (\<lambda>(x,ka). content (ka \<inter> {x. x \<bullet> k \<le> c}) *\<^sub>R f x) x +
  1.2407 @@ -3429,34 +1250,6 @@
  1.2408  
  1.2409  subsection \<open>A sort of converse, integrability on subintervals.\<close>
  1.2410  
  1.2411 -lemma tagged_division_union_interval:
  1.2412 -  fixes a :: "'a::euclidean_space"
  1.2413 -  assumes "p1 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<le> (c::real)})"
  1.2414 -    and "p2 tagged_division_of (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
  1.2415 -    and k: "k \<in> Basis"
  1.2416 -  shows "(p1 \<union> p2) tagged_division_of (cbox a b)"
  1.2417 -proof -
  1.2418 -  have *: "cbox a b = (cbox a b \<inter> {x. x\<bullet>k \<le> c}) \<union> (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
  1.2419 -    by auto
  1.2420 -  show ?thesis
  1.2421 -    apply (subst *)
  1.2422 -    apply (rule tagged_division_union[OF assms(1-2)])
  1.2423 -    unfolding interval_split[OF k] interior_cbox
  1.2424 -    using k
  1.2425 -    apply (auto simp add: box_def elim!: ballE[where x=k])
  1.2426 -    done
  1.2427 -qed
  1.2428 -
  1.2429 -lemma tagged_division_union_interval_real:
  1.2430 -  fixes a :: real
  1.2431 -  assumes "p1 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<le> (c::real)})"
  1.2432 -    and "p2 tagged_division_of ({a .. b} \<inter> {x. x\<bullet>k \<ge> c})"
  1.2433 -    and k: "k \<in> Basis"
  1.2434 -  shows "(p1 \<union> p2) tagged_division_of {a .. b}"
  1.2435 -  using assms
  1.2436 -  unfolding box_real[symmetric]
  1.2437 -  by (rule tagged_division_union_interval)
  1.2438 -
  1.2439  lemma has_integral_separate_sides:
  1.2440    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
  1.2441    assumes "(f has_integral i) (cbox a b)"
  1.2442 @@ -3621,10 +1414,10 @@
  1.2443      qed
  1.2444    next
  1.2445      fix a b :: 'a
  1.2446 -    assume "content (cbox a b) = 0"
  1.2447 +    assume "box a b = {}"
  1.2448      then show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) = Some 0"
  1.2449        using has_integral_null_eq
  1.2450 -      by (auto simp: integrable_on_null)
  1.2451 +      by (auto simp: integrable_on_null content_eq_0_interior)
  1.2452    qed
  1.2453  qed
  1.2454  
  1.2455 @@ -4069,47 +1862,6 @@
  1.2456  
  1.2457  subsection \<open>Negligibility of hyperplane.\<close>
  1.2458  
  1.2459 -lemma interval_doublesplit:
  1.2460 -  fixes a :: "'a::euclidean_space"
  1.2461 -  assumes "k \<in> Basis"
  1.2462 -  shows "cbox a b \<inter> {x . \<bar>x\<bullet>k - c\<bar> \<le> (e::real)} =
  1.2463 -    cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) (c - e) else a\<bullet>i) *\<^sub>R i)
  1.2464 -     (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) (c + e) else b\<bullet>i) *\<^sub>R i)"
  1.2465 -proof -
  1.2466 -  have *: "\<And>x c e::real. \<bar>x - c\<bar> \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e"
  1.2467 -    by auto
  1.2468 -  have **: "\<And>s P Q. s \<inter> {x. P x \<and> Q x} = (s \<inter> {x. Q x}) \<inter> {x. P x}"
  1.2469 -    by blast
  1.2470 -  show ?thesis
  1.2471 -    unfolding * ** interval_split[OF assms] by (rule refl)
  1.2472 -qed
  1.2473 -
  1.2474 -lemma division_doublesplit:
  1.2475 -  fixes a :: "'a::euclidean_space"
  1.2476 -  assumes "p division_of (cbox a b)"
  1.2477 -    and k: "k \<in> Basis"
  1.2478 -  shows "(\<lambda>l. l \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e}) ` {l\<in>p. l \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e} \<noteq> {}}
  1.2479 -         division_of  (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> e})"
  1.2480 -proof -
  1.2481 -  have *: "\<And>x c. \<bar>x - c\<bar> \<le> e \<longleftrightarrow> x \<ge> c - e \<and> x \<le> c + e"
  1.2482 -    by auto
  1.2483 -  have **: "\<And>p q p' q'. p division_of q \<Longrightarrow> p = p' \<Longrightarrow> q = q' \<Longrightarrow> p' division_of q'"
  1.2484 -    by auto
  1.2485 -  note division_split(1)[OF assms, where c="c+e",unfolded interval_split[OF k]]
  1.2486 -  note division_split(2)[OF this, where c="c-e" and k=k,OF k]
  1.2487 -  then show ?thesis
  1.2488 -    apply (rule **)
  1.2489 -    subgoal
  1.2490 -      apply (simp add: abs_diff_le_iff field_simps Collect_conj_eq setcompr_eq_image[symmetric])
  1.2491 -      apply (rule equalityI)
  1.2492 -      apply blast
  1.2493 -      apply clarsimp
  1.2494 -      apply (rule_tac x="l \<inter> {x. c + e \<ge> x \<bullet> k}" in exI)
  1.2495 -      apply auto
  1.2496 -      done
  1.2497 -    by (simp add: interval_split k interval_doublesplit)
  1.2498 -qed
  1.2499 -
  1.2500  lemma content_doublesplit:
  1.2501    fixes a :: "'a::euclidean_space"
  1.2502    assumes "0 < e"
  1.2503 @@ -4262,6 +2014,8 @@
  1.2504        also have "\<dots> < e"
  1.2505        proof (subst setsum.over_tagged_division_lemma[OF p[THEN conjunct1]], goal_cases)
  1.2506          case prems: (1 u v)
  1.2507 +        then have *: "content (cbox u v) = 0"
  1.2508 +          unfolding content_eq_0_interior by simp
  1.2509          have "content (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<le> content (cbox u v)"
  1.2510            unfolding interval_doublesplit[OF k]
  1.2511            apply (rule content_subset)
  1.2512 @@ -4269,7 +2023,7 @@
  1.2513            apply auto
  1.2514            done
  1.2515          then show ?case
  1.2516 -          unfolding prems interval_doublesplit[OF k]
  1.2517 +          unfolding * interval_doublesplit[OF k]
  1.2518            by (blast intro: antisym)
  1.2519        next
  1.2520          have "(\<Sum>l\<in>snd ` p. content (l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) =
  1.2521 @@ -4303,188 +2057,9 @@
  1.2522  qed
  1.2523  
  1.2524  
  1.2525 -subsection \<open>A technical lemma about "refinement" of division.\<close>
  1.2526 -
  1.2527 -lemma tagged_division_finer:
  1.2528 -  fixes p :: "('a::euclidean_space \<times> ('a::euclidean_space set)) set"
  1.2529 -  assumes "p tagged_division_of (cbox a b)"
  1.2530 -    and "gauge d"
  1.2531 -  obtains q where "q tagged_division_of (cbox a b)"
  1.2532 -    and "d fine q"
  1.2533 -    and "\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q"
  1.2534 -proof -
  1.2535 -  let ?P = "\<lambda>p. p tagged_partial_division_of (cbox a b) \<longrightarrow> gauge d \<longrightarrow>
  1.2536 -    (\<exists>q. q tagged_division_of (\<Union>{k. \<exists>x. (x,k) \<in> p}) \<and> d fine q \<and>
  1.2537 -      (\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q))"
  1.2538 -  {
  1.2539 -    have *: "finite p" "p tagged_partial_division_of (cbox a b)"
  1.2540 -      using assms(1)
  1.2541 -      unfolding tagged_division_of_def
  1.2542 -      by auto
  1.2543 -    presume "\<And>p. finite p \<Longrightarrow> ?P p"
  1.2544 -    from this[rule_format,OF * assms(2)] guess q .. note q=this
  1.2545 -    then show ?thesis
  1.2546 -      apply -
  1.2547 -      apply (rule that[of q])
  1.2548 -      unfolding tagged_division_ofD[OF assms(1)]
  1.2549 -      apply auto
  1.2550 -      done
  1.2551 -  }
  1.2552 -  fix p :: "('a::euclidean_space \<times> ('a::euclidean_space set)) set"
  1.2553 -  assume as: "finite p"
  1.2554 -  show "?P p"
  1.2555 -    apply rule
  1.2556 -    apply rule
  1.2557 -    using as
  1.2558 -  proof (induct p)
  1.2559 -    case empty
  1.2560 -    show ?case
  1.2561 -      apply (rule_tac x="{}" in exI)
  1.2562 -      unfolding fine_def
  1.2563 -      apply auto
  1.2564 -      done
  1.2565 -  next
  1.2566 -    case (insert xk p)
  1.2567 -    guess x k using surj_pair[of xk] by (elim exE) note xk=this
  1.2568 -    note tagged_partial_division_subset[OF insert(4) subset_insertI]
  1.2569 -    from insert(3)[OF this insert(5)] guess q1 .. note q1 = conjunctD3[OF this]
  1.2570 -    have *: "\<Union>{l. \<exists>y. (y,l) \<in> insert xk p} = k \<union> \<Union>{l. \<exists>y. (y,l) \<in> p}"
  1.2571 -      unfolding xk by auto
  1.2572 -    note p = tagged_partial_division_ofD[OF insert(4)]
  1.2573 -    from p(4)[unfolded xk, OF insertI1] guess u v by (elim exE) note uv=this
  1.2574 -
  1.2575 -    have "finite {k. \<exists>x. (x, k) \<in> p}"
  1.2576 -      apply (rule finite_subset[of _ "snd ` p"])
  1.2577 -      using p
  1.2578 -      apply safe
  1.2579 -      apply (metis image_iff snd_conv)
  1.2580 -      apply auto
  1.2581 -      done
  1.2582 -    then have int: "interior (cbox u v) \<inter> interior (\<Union>{k. \<exists>x. (x, k) \<in> p}) = {}"
  1.2583 -      apply (rule inter_interior_unions_intervals)
  1.2584 -      apply (rule open_interior)
  1.2585 -      apply (rule_tac[!] ballI)
  1.2586 -      unfolding mem_Collect_eq
  1.2587 -      apply (erule_tac[!] exE)
  1.2588 -      apply (drule p(4)[OF insertI2])
  1.2589 -      apply assumption
  1.2590 -      apply (rule p(5))
  1.2591 -      unfolding uv xk
  1.2592 -      apply (rule insertI1)
  1.2593 -      apply (rule insertI2)
  1.2594 -      apply assumption
  1.2595 -      using insert(2)
  1.2596 -      unfolding uv xk
  1.2597 -      apply auto
  1.2598 -      done
  1.2599 -    show ?case
  1.2600 -    proof (cases "cbox u v \<subseteq> d x")
  1.2601 -      case True
  1.2602 -      then show ?thesis
  1.2603 -        apply (rule_tac x="{(x,cbox u v)} \<union> q1" in exI)
  1.2604 -        apply rule
  1.2605 -        unfolding * uv
  1.2606 -        apply (rule tagged_division_union)
  1.2607 -        apply (rule tagged_division_of_self)
  1.2608 -        apply (rule p[unfolded xk uv] insertI1)+
  1.2609 -        apply (rule q1)
  1.2610 -        apply (rule int)
  1.2611 -        apply rule
  1.2612 -        apply (rule fine_union)
  1.2613 -        apply (subst fine_def)
  1.2614 -        defer
  1.2615 -        apply (rule q1)
  1.2616 -        unfolding Ball_def split_paired_All split_conv
  1.2617 -        apply rule
  1.2618 -        apply rule
  1.2619 -        apply rule
  1.2620 -        apply rule
  1.2621 -        apply (erule insertE)
  1.2622 -        apply (simp add: uv xk)
  1.2623 -        apply (rule UnI2)
  1.2624 -        apply (drule q1(3)[rule_format])
  1.2625 -        unfolding xk uv
  1.2626 -        apply auto
  1.2627 -        done
  1.2628 -    next
  1.2629 -      case False
  1.2630 -      from fine_division_exists[OF assms(2), of u v] guess q2 . note q2=this
  1.2631 -      show ?thesis
  1.2632 -        apply (rule_tac x="q2 \<union> q1" in exI)
  1.2633 -        apply rule
  1.2634 -        unfolding * uv
  1.2635 -        apply (rule tagged_division_union q2 q1 int fine_union)+
  1.2636 -        unfolding Ball_def split_paired_All split_conv
  1.2637 -        apply rule
  1.2638 -        apply (rule fine_union)
  1.2639 -        apply (rule q1 q2)+
  1.2640 -        apply rule
  1.2641 -        apply rule
  1.2642 -        apply rule
  1.2643 -        apply rule
  1.2644 -        apply (erule insertE)
  1.2645 -        apply (rule UnI2)
  1.2646 -        apply (simp add: False uv xk)
  1.2647 -        apply (drule q1(3)[rule_format])
  1.2648 -        using False
  1.2649 -        unfolding xk uv
  1.2650 -        apply auto
  1.2651 -        done
  1.2652 -    qed
  1.2653 -  qed
  1.2654 -qed
  1.2655 -
  1.2656  
  1.2657  subsection \<open>Hence the main theorem about negligible sets.\<close>
  1.2658  
  1.2659 -lemma finite_product_dependent:
  1.2660 -  assumes "finite s"
  1.2661 -    and "\<And>x. x \<in> s \<Longrightarrow> finite (t x)"
  1.2662 -  shows "finite {(i, j) |i j. i \<in> s \<and> j \<in> t i}"
  1.2663 -  using assms
  1.2664 -proof induct
  1.2665 -  case (insert x s)
  1.2666 -  have *: "{(i, j) |i j. i \<in> insert x s \<and> j \<in> t i} =
  1.2667 -    (\<lambda>y. (x,y)) ` (t x) \<union> {(i, j) |i j. i \<in> s \<and> j \<in> t i}" by auto
  1.2668 -  show ?case
  1.2669 -    unfolding *
  1.2670 -    apply (rule finite_UnI)
  1.2671 -    using insert
  1.2672 -    apply auto
  1.2673 -    done
  1.2674 -qed auto
  1.2675 -
  1.2676 -lemma sum_sum_product:
  1.2677 -  assumes "finite s"
  1.2678 -    and "\<forall>i\<in>s. finite (t i)"
  1.2679 -  shows "setsum (\<lambda>i. setsum (x i) (t i)::real) s =
  1.2680 -    setsum (\<lambda>(i,j). x i j) {(i,j) | i j. i \<in> s \<and> j \<in> t i}"
  1.2681 -  using assms
  1.2682 -proof induct
  1.2683 -  case (insert a s)
  1.2684 -  have *: "{(i, j) |i j. i \<in> insert a s \<and> j \<in> t i} =
  1.2685 -    (\<lambda>y. (a,y)) ` (t a) \<union> {(i, j) |i j. i \<in> s \<and> j \<in> t i}" by auto
  1.2686 -  show ?case
  1.2687 -    unfolding *
  1.2688 -    apply (subst setsum.union_disjoint)
  1.2689 -    unfolding setsum.insert[OF insert(1-2)]
  1.2690 -    prefer 4
  1.2691 -    apply (subst insert(3))
  1.2692 -    unfolding add_right_cancel
  1.2693 -  proof -
  1.2694 -    show "setsum (x a) (t a) = (\<Sum>(xa, y)\<in> Pair a ` t a. x xa y)"
  1.2695 -      apply (subst setsum.reindex)
  1.2696 -      unfolding inj_on_def
  1.2697 -      apply auto
  1.2698 -      done
  1.2699 -    show "finite {(i, j) |i j. i \<in> s \<and> j \<in> t i}"
  1.2700 -      apply (rule finite_product_dependent)
  1.2701 -      using insert
  1.2702 -      apply auto
  1.2703 -      done
  1.2704 -  qed (insert insert, auto)
  1.2705 -qed auto
  1.2706 -
  1.2707  lemma has_integral_negligible:
  1.2708    fixes f :: "'b::euclidean_space \<Rightarrow> 'a::real_normed_vector"
  1.2709    assumes "negligible s"
  1.2710 @@ -4937,10 +2512,10 @@
  1.2711  proof safe
  1.2712    fix a b :: 'b
  1.2713    show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
  1.2714 -    if "content (cbox a b) = 0"
  1.2715 +    if "box a b = {}"
  1.2716      apply (rule_tac x=f in exI)
  1.2717      using assms that
  1.2718 -    apply (auto intro!: integrable_on_null)
  1.2719 +    apply (auto simp: content_eq_0_interior)
  1.2720      done
  1.2721    {
  1.2722      fix c g
  1.2723 @@ -5059,33 +2634,6 @@
  1.2724  
  1.2725  subsection \<open>Specialization of additivity to one dimension.\<close>
  1.2726  
  1.2727 -subsection \<open>Special case of additivity we need for the FTC.\<close>
  1.2728 -
  1.2729 -lemma additive_tagged_division_1:
  1.2730 -  fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
  1.2731 -  assumes "a \<le> b"
  1.2732 -    and "p tagged_division_of {a..b}"
  1.2733 -  shows "setsum (\<lambda>(x,k). f(Sup k) - f(Inf k)) p = f b - f a"
  1.2734 -proof -
  1.2735 -  let ?f = "(\<lambda>k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
  1.2736 -  have ***: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
  1.2737 -    using assms by auto
  1.2738 -  have *: "add.operative ?f"
  1.2739 -    unfolding add.operative_1_lt box_eq_empty
  1.2740 -    by auto
  1.2741 -  have **: "cbox a b \<noteq> {}"
  1.2742 -    using assms(1) by auto
  1.2743 -  note setsum.operative_tagged_division[OF * assms(2)[simplified box_real[symmetric]]]
  1.2744 -  note * = this[unfolded if_not_P[OF **] interval_bounds[OF ***],symmetric]
  1.2745 -  show ?thesis
  1.2746 -    unfolding *
  1.2747 -    apply (rule setsum.cong)
  1.2748 -    unfolding split_paired_all split_conv
  1.2749 -    using assms(2)
  1.2750 -    apply auto
  1.2751 -    done
  1.2752 -qed
  1.2753 -
  1.2754  
  1.2755  subsection \<open>A useful lemma allowing us to factor out the content size.\<close>
  1.2756  
  1.2757 @@ -5373,20 +2921,6 @@
  1.2758  qed
  1.2759  
  1.2760  
  1.2761 -subsection \<open>Attempt a systematic general set of "offset" results for components.\<close>
  1.2762 -
  1.2763 -lemma gauge_modify:
  1.2764 -  assumes "(\<forall>s. open s \<longrightarrow> open {x. f(x) \<in> s})" "gauge d"
  1.2765 -  shows "gauge (\<lambda>x. {y. f y \<in> d (f x)})"
  1.2766 -  using assms
  1.2767 -  unfolding gauge_def
  1.2768 -  apply safe
  1.2769 -  defer
  1.2770 -  apply (erule_tac x="f x" in allE)
  1.2771 -  apply (erule_tac x="d (f x)" in allE)
  1.2772 -  apply auto
  1.2773 -  done
  1.2774 -
  1.2775  
  1.2776  subsection \<open>Only need trivial subintervals if the interval itself is trivial.\<close>
  1.2777  
  1.2778 @@ -5524,10 +3058,12 @@
  1.2779    shows "comm_monoid.operative op \<and> True (\<lambda>i. f integrable_on i)"
  1.2780    unfolding comm_monoid.operative_def[OF comm_monoid_and]
  1.2781    apply safe
  1.2782 -  apply (subst integrable_on_def)
  1.2783 -  unfolding has_integral_null_eq
  1.2784 -  apply (rule, rule refl)
  1.2785 -  apply (rule, assumption, assumption)+
  1.2786 +     apply (subst integrable_on_def)
  1.2787 +     apply rule
  1.2788 +     apply (rule has_integral_null_eq[where i=0, THEN iffD2])
  1.2789 +      apply (simp add: content_eq_0_interior)
  1.2790 +     apply rule
  1.2791 +    apply (rule, assumption, assumption)+
  1.2792    unfolding integrable_on_def
  1.2793    by (auto intro!: has_integral_split)
  1.2794  
  1.2795 @@ -6121,18 +3657,6 @@
  1.2796  
  1.2797  subsection \<open>Stronger form of FCT; quite a tedious proof.\<close>
  1.2798  
  1.2799 -lemma bgauge_existence_lemma: "(\<forall>x\<in>s. \<exists>d::real. 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. x\<in>s \<longrightarrow> q d x)"
  1.2800 -  by (meson zero_less_one)
  1.2801 -
  1.2802 -lemma additive_tagged_division_1':
  1.2803 -  fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
  1.2804 -  assumes "a \<le> b"
  1.2805 -    and "p tagged_division_of {a..b}"
  1.2806 -  shows "setsum (\<lambda>(x,k). f (Sup k) - f(Inf k)) p = f b - f a"
  1.2807 -  using additive_tagged_division_1[OF _ assms(2), of f]
  1.2808 -  using assms(1)
  1.2809 -  by auto
  1.2810 -
  1.2811  lemma split_minus[simp]: "(\<lambda>(x, k). f x k) x - (\<lambda>(x, k). g x k) x = (\<lambda>(x, k). f x k - g x k) x"
  1.2812    by (simp add: split_def)
  1.2813  
  1.2814 @@ -7717,39 +5241,6 @@
  1.2815    shows "f integrable_on s \<longleftrightarrow> f integrable_on t"
  1.2816  by (blast intro: integrable_spike_set assms negligible_subset)
  1.2817  
  1.2818 -(*lemma integral_spike_set:
  1.2819 - "\<forall>f:real^M->real^N g s t.
  1.2820 -        negligible(s DIFF t \<union> t DIFF s)
  1.2821 -        \<longrightarrow> integral s f = integral t f"
  1.2822 -qed  REPEAT STRIP_TAC THEN REWRITE_TAC[integral] THEN
  1.2823 -  AP_TERM_TAC THEN ABS_TAC THEN MATCH_MP_TAC HAS_INTEGRAL_SPIKE_SET_EQ THEN
  1.2824 -  ASM_MESON_TAC[]);;
  1.2825 -
  1.2826 -lemma has_integral_interior:
  1.2827 - "\<forall>f:real^M->real^N y s.
  1.2828 -        negligible(frontier s)
  1.2829 -        \<longrightarrow> ((f has_integral y) (interior s) \<longleftrightarrow> (f has_integral y) s)"
  1.2830 -qed  REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_INTEGRAL_SPIKE_SET_EQ THEN
  1.2831 -  FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
  1.2832 -    NEGLIGIBLE_SUBSET)) THEN
  1.2833 -  REWRITE_TAC[frontier] THEN
  1.2834 -  MP_TAC(ISPEC `s:real^M->bool` INTERIOR_SUBSET) THEN
  1.2835 -  MP_TAC(ISPEC `s:real^M->bool` CLOSURE_SUBSET) THEN
  1.2836 -  SET_TAC[]);;
  1.2837 -
  1.2838 -lemma has_integral_closure:
  1.2839 - "\<forall>f:real^M->real^N y s.
  1.2840 -        negligible(frontier s)
  1.2841 -        \<longrightarrow> ((f has_integral y) (closure s) \<longleftrightarrow> (f has_integral y) s)"
  1.2842 -qed  REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_INTEGRAL_SPIKE_SET_EQ THEN
  1.2843 -  FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
  1.2844 -    NEGLIGIBLE_SUBSET)) THEN
  1.2845 -  REWRITE_TAC[frontier] THEN
  1.2846 -  MP_TAC(ISPEC `s:real^M->bool` INTERIOR_SUBSET) THEN
  1.2847 -  MP_TAC(ISPEC `s:real^M->bool` CLOSURE_SUBSET) THEN
  1.2848 -  SET_TAC[]);;*)
  1.2849 -
  1.2850 -
  1.2851  subsection \<open>More lemmas that are useful later\<close>
  1.2852  
  1.2853  lemma has_integral_subset_component_le:
  1.2854 @@ -8434,34 +5925,26 @@
  1.2855  
  1.2856  subsection \<open>Also tagged divisions\<close>
  1.2857  
  1.2858 +lemma has_integral_iff: "(f has_integral i) s \<longleftrightarrow> (f integrable_on s \<and> integral s f = i)"
  1.2859 +  by blast
  1.2860 +
  1.2861  lemma has_integral_combine_tagged_division:
  1.2862    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
  1.2863    assumes "p tagged_division_of s"
  1.2864      and "\<forall>(x,k) \<in> p. (f has_integral (i k)) k"
  1.2865 -  shows "(f has_integral (setsum (\<lambda>(x,k). i k) p)) s"
  1.2866 +  shows "(f has_integral (\<Sum>(x,k)\<in>p. i k)) s"
  1.2867  proof -
  1.2868 -  have *: "(f has_integral (setsum (\<lambda>k. integral k f) (snd ` p))) s"
  1.2869 -    apply (rule has_integral_combine_division)
  1.2870 -    apply (rule division_of_tagged_division[OF assms(1)])
  1.2871 +  have *: "(f has_integral (\<Sum>k\<in>snd`p. integral k f)) s"
  1.2872      using assms(2)
  1.2873 -    unfolding has_integral_integral[symmetric]
  1.2874 -    apply safe
  1.2875 +    apply (intro has_integral_combine_division)
  1.2876 +    apply (auto simp: has_integral_integral[symmetric] intro: division_of_tagged_division[OF assms(1)])
  1.2877      apply auto
  1.2878      done
  1.2879 -  then show ?thesis
  1.2880 -    apply -
  1.2881 -    apply (rule subst[where P="\<lambda>i. (f has_integral i) s"])
  1.2882 -    defer
  1.2883 -    apply assumption
  1.2884 -    apply (rule trans[of _ "setsum (\<lambda>(x,k). integral k f) p"])
  1.2885 -    apply (subst eq_commute)
  1.2886 -    apply (rule setsum.over_tagged_division_lemma[OF assms(1)])
  1.2887 -    apply (rule integral_null)
  1.2888 -    apply assumption
  1.2889 -    apply (rule setsum.cong)
  1.2890 -    using assms(2)
  1.2891 -    apply auto
  1.2892 -    done
  1.2893 +  also have "(\<Sum>k\<in>snd`p. integral k f) = (\<Sum>(x, k)\<in>p. integral k f)"
  1.2894 +    by (intro setsum.over_tagged_division_lemma[OF assms(1), symmetric] integral_null)
  1.2895 +       (simp add: content_eq_0_interior)
  1.2896 +  finally show ?thesis
  1.2897 +    using assms by (auto simp add: has_integral_iff intro!: setsum.cong)
  1.2898  qed
  1.2899  
  1.2900  lemma integral_combine_tagged_division_bottomup:
  1.2901 @@ -9616,84 +7099,6 @@
  1.2902  
  1.2903  subsection \<open>differentiation under the integral sign\<close>
  1.2904  
  1.2905 -lemma tube_lemma:
  1.2906 -  assumes "compact K"
  1.2907 -  assumes "open W"
  1.2908 -  assumes "{x0} \<times> K \<subseteq> W"
  1.2909 -  shows "\<exists>X0. x0 \<in> X0 \<and> open X0 \<and> X0 \<times> K \<subseteq> W"
  1.2910 -proof -
  1.2911 -  {
  1.2912 -    fix y assume "y \<in> K"
  1.2913 -    then have "(x0, y) \<in> W" using assms by auto
  1.2914 -    with \<open>open W\<close>
  1.2915 -    have "\<exists>X0 Y. open X0 \<and> open Y \<and> x0 \<in> X0 \<and> y \<in> Y \<and> X0 \<times> Y \<subseteq> W"
  1.2916 -      by (rule open_prod_elim) blast
  1.2917 -  }
  1.2918 -  then obtain X0 Y where
  1.2919 -    *: "\<forall>y \<in> K. open (X0 y) \<and> open (Y y) \<and> x0 \<in> X0 y \<and> y \<in> Y y \<and> X0 y \<times> Y y \<subseteq> W"
  1.2920 -    by metis
  1.2921 -  from * have "\<forall>t\<in>Y ` K. open t" "K \<subseteq> \<Union>(Y ` K)" by auto
  1.2922 -  with \<open>compact K\<close> obtain CC where CC: "CC \<subseteq> Y ` K" "finite CC" "K \<subseteq> \<Union>CC"
  1.2923 -    by (rule compactE)
  1.2924 -  then obtain c where c: "\<And>C. C \<in> CC \<Longrightarrow> c C \<in> K \<and> C = Y (c C)"
  1.2925 -    by (force intro!: choice)
  1.2926 -  with * CC show ?thesis
  1.2927 -    by (force intro!: exI[where x="\<Inter>C\<in>CC. X0 (c C)"]) (* SLOW *)
  1.2928 -qed
  1.2929 -
  1.2930 -lemma continuous_on_prod_compactE:
  1.2931 -  fixes fx::"'a::topological_space \<times> 'b::topological_space \<Rightarrow> 'c::metric_space"
  1.2932 -    and e::real
  1.2933 -  assumes cont_fx: "continuous_on (U \<times> C) fx"
  1.2934 -  assumes "compact C"
  1.2935 -  assumes [intro]: "x0 \<in> U"
  1.2936 -  notes [continuous_intros] = continuous_on_compose2[OF cont_fx]
  1.2937 -  assumes "e > 0"
  1.2938 -  obtains X0 where "x0 \<in> X0" "open X0"
  1.2939 -    "\<forall>x\<in>X0 \<inter> U. \<forall>t \<in> C. dist (fx (x, t)) (fx (x0, t)) \<le> e"
  1.2940 -proof -
  1.2941 -  define psi where "psi = (\<lambda>(x, t). dist (fx (x, t)) (fx (x0, t)))"
  1.2942 -  define W0 where "W0 = {(x, t) \<in> U \<times> C. psi (x, t) < e}"
  1.2943 -  have W0_eq: "W0 = psi -` {..<e} \<inter> U \<times> C"
  1.2944 -    by (auto simp: vimage_def W0_def)
  1.2945 -  have "open {..<e}" by simp
  1.2946 -  have "continuous_on (U \<times> C) psi"
  1.2947 -    by (auto intro!: continuous_intros simp: psi_def split_beta')
  1.2948 -  from this[unfolded continuous_on_open_invariant, rule_format, OF \<open>open {..<e}\<close>]
  1.2949 -  obtain W where W: "open W" "W \<inter> U \<times> C = W0 \<inter> U \<times> C"
  1.2950 -    unfolding W0_eq by blast
  1.2951 -  have "{x0} \<times> C \<subseteq> W \<inter> U \<times> C"
  1.2952 -    unfolding W
  1.2953 -    by (auto simp: W0_def psi_def \<open>0 < e\<close>)
  1.2954 -  then have "{x0} \<times> C \<subseteq> W" by blast
  1.2955 -  from tube_lemma[OF \<open>compact C\<close> \<open>open W\<close> this]
  1.2956 -  obtain X0 where X0: "x0 \<in> X0" "open X0" "X0 \<times> C \<subseteq> W"
  1.2957 -    by blast
  1.2958 -
  1.2959 -  have "\<forall>x\<in>X0 \<inter> U. \<forall>t \<in> C. dist (fx (x, t)) (fx (x0, t)) \<le> e"
  1.2960 -  proof safe
  1.2961 -    fix x assume x: "x \<in> X0" "x \<in> U"
  1.2962 -    fix t assume t: "t \<in> C"
  1.2963 -    have "dist (fx (x, t)) (fx (x0, t)) = psi (x, t)"
  1.2964 -      by (auto simp: psi_def)
  1.2965 -    also
  1.2966 -    {
  1.2967 -      have "(x, t) \<in> X0 \<times> C"
  1.2968 -        using t x
  1.2969 -        by auto
  1.2970 -      also note \<open>\<dots> \<subseteq> W\<close>
  1.2971 -      finally have "(x, t) \<in> W" .
  1.2972 -      with t x have "(x, t) \<in> W \<inter> U \<times> C"
  1.2973 -        by blast
  1.2974 -      also note \<open>W \<inter> U \<times> C = W0 \<inter> U \<times> C\<close>
  1.2975 -      finally  have "psi (x, t) < e"
  1.2976 -        by (auto simp: W0_def)
  1.2977 -    }
  1.2978 -    finally show "dist (fx (x, t)) (fx (x0, t)) \<le> e" by simp
  1.2979 -  qed
  1.2980 -  from X0(1,2) this show ?thesis ..
  1.2981 -qed
  1.2982 -
  1.2983  lemma integral_continuous_on_param:
  1.2984    fixes f::"'a::topological_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::banach"
  1.2985    assumes cont_fx: "continuous_on (U \<times> cbox a b) (\<lambda>(x, t). f x t)"
  1.2986 @@ -9743,26 +7148,6 @@
  1.2987    qed
  1.2988  qed (auto intro!: continuous_on_const)
  1.2989  
  1.2990 -lemma eventually_closed_segment:
  1.2991 -  fixes x0::"'a::real_normed_vector"
  1.2992 -  assumes "open X0" "x0 \<in> X0"
  1.2993 -  shows "\<forall>\<^sub>F x in at x0 within U. closed_segment x0 x \<subseteq> X0"
  1.2994 -proof -
  1.2995 -  from openE[OF assms]
  1.2996 -  obtain e where e: "0 < e" "ball x0 e \<subseteq> X0" .
  1.2997 -  then have "\<forall>\<^sub>F x in at x0 within U. x \<in> ball x0 e"
  1.2998 -    by (auto simp: dist_commute eventually_at)
  1.2999 -  then show ?thesis
  1.3000 -  proof eventually_elim
  1.3001 -    case (elim x)
  1.3002 -    have "x0 \<in> ball x0 e" using \<open>e > 0\<close> by simp
  1.3003 -    from convex_ball[unfolded convex_contains_segment, rule_format, OF this elim]
  1.3004 -    have "closed_segment x0 x \<subseteq> ball x0 e" .
  1.3005 -    also note \<open>\<dots> \<subseteq> X0\<close>
  1.3006 -    finally show ?case .
  1.3007 -  qed
  1.3008 -qed
  1.3009 -
  1.3010  lemma leibniz_rule:
  1.3011    fixes f::"'a::banach \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::banach"
  1.3012    assumes fx: "\<And>x t. x \<in> U \<Longrightarrow> t \<in> cbox a b \<Longrightarrow>
  1.3013 @@ -9856,8 +7241,7 @@
  1.3014    qed (rule blinfun.bounded_linear_right)
  1.3015  qed (auto intro!: derivative_eq_intros simp: blinfun.bilinear_simps)
  1.3016  
  1.3017 -lemma
  1.3018 -  has_vector_derivative_eq_has_derivative_blinfun:
  1.3019 +lemma has_vector_derivative_eq_has_derivative_blinfun:
  1.3020    "(f has_vector_derivative f') (at x within U) \<longleftrightarrow>
  1.3021      (f has_derivative blinfun_scaleR_left f') (at x within U)"
  1.3022    by (simp add: has_vector_derivative_def)
  1.3023 @@ -9889,8 +7273,7 @@
  1.3024      done
  1.3025  qed
  1.3026  
  1.3027 -lemma
  1.3028 -  has_field_derivative_eq_has_derivative_blinfun:
  1.3029 +lemma has_field_derivative_eq_has_derivative_blinfun:
  1.3030    "(f has_field_derivative f') (at x within U) \<longleftrightarrow> (f has_derivative blinfun_mult_right f') (at x within U)"
  1.3031    by (simp add: has_field_derivative_def)
  1.3032  
  1.3033 @@ -9922,8 +7305,7 @@
  1.3034  
  1.3035  subsection \<open>Exchange uniform limit and integral\<close>
  1.3036  
  1.3037 -lemma
  1.3038 -  uniform_limit_integral:
  1.3039 +lemma uniform_limit_integral:
  1.3040    fixes f::"'a \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::banach"
  1.3041    assumes u: "uniform_limit (cbox a b) f g F"
  1.3042    assumes c: "\<And>n. continuous_on (cbox a b) (f n)"
  1.3043 @@ -10117,18 +7499,6 @@
  1.3044  
  1.3045  subsection \<open>Compute a double integral using iterated integrals and switching the order of integration\<close>
  1.3046  
  1.3047 -lemma setcomp_dot1: "{z. P (z \<bullet> (i,0))} = {(x,y). P(x \<bullet> i)}"
  1.3048 -  by auto
  1.3049 -
  1.3050 -lemma setcomp_dot2: "{z. P (z \<bullet> (0,i))} = {(x,y). P(y \<bullet> i)}"
  1.3051 -  by auto
  1.3052 -
  1.3053 -lemma Sigma_Int_Paircomp1: "(Sigma A B) \<inter> {(x, y). P x} = Sigma (A \<inter> {x. P x}) B"
  1.3054 -  by blast
  1.3055 -
  1.3056 -lemma Sigma_Int_Paircomp2: "(Sigma A B) \<inter> {(x, y). P y} = Sigma A (\<lambda>z. B z \<inter> {y. P y})"
  1.3057 -  by blast
  1.3058 -
  1.3059  lemma continuous_on_imp_integrable_on_Pair1:
  1.3060    fixes f :: "_ \<Rightarrow> 'b::banach"
  1.3061    assumes con: "continuous_on (cbox (a,c) (b,d)) f" and x: "x \<in> cbox a b"
  1.3062 @@ -10180,11 +7550,6 @@
  1.3063      done
  1.3064  qed
  1.3065  
  1.3066 -lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
  1.3067 -            \<Longrightarrow> norm(y - x) \<le> e"
  1.3068 -using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"]
  1.3069 -  by (simp add: add_diff_add)
  1.3070 -
  1.3071  lemma integral_split:
  1.3072    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{real_normed_vector,complete_space}"
  1.3073    assumes f: "f integrable_on (cbox a b)"
  1.3074 @@ -10208,9 +7573,11 @@
  1.3075                      \<le> e * content (cbox (a,c) (b,d)))"
  1.3076  proof (auto simp: comm_monoid.operative_def[OF comm_monoid_and])
  1.3077    fix a::'a and c::'b and b::'a and d::'b and u::'a and v::'a and w::'b and z::'b
  1.3078 -  assume c0: "content (cbox (a, c) (b, d)) = 0"
  1.3079 +  assume *: "box (a, c) (b, d) = {}"
  1.3080       and cb1: "cbox (u, w) (v, z) \<subseteq> cbox (a, c) (b, d)"
  1.3081       and cb2: "cbox (u, w) (v, z) \<subseteq> s"
  1.3082 +  then have c0: "content (cbox (a, c) (b, d)) = 0"
  1.3083 +    using * unfolding content_eq_0_interior by simp
  1.3084    have c0': "content (cbox (u, w) (v, z)) = 0"
  1.3085      by (fact content_0_subset [OF c0 cb1])
  1.3086    show "norm (integral (cbox (u,w) (v,z)) f - integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x, y))))
  1.3087 @@ -10296,9 +7663,6 @@
  1.3088       integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. k))"
  1.3089    by (simp add: content_Pair)
  1.3090  
  1.3091 -lemma norm_minus2: "norm (x1-x2, y1-y2) = norm (x2-x1, y2-y1)"
  1.3092 -  by (simp add: norm_minus_eqI)
  1.3093 -
  1.3094  lemma integral_prod_continuous:
  1.3095    fixes f :: "('a::euclidean_space * 'b::euclidean_space) \<Rightarrow> 'c::banach"
  1.3096    assumes "continuous_on (cbox (a,c) (b,d)) f" (is "continuous_on ?CBOX f")
  1.3097 @@ -10414,20 +7778,6 @@
  1.3098      by simp
  1.3099  qed
  1.3100  
  1.3101 -lemma swap_continuous:
  1.3102 -  assumes "continuous_on (cbox (a,c) (b,d)) (\<lambda>(x,y). f x y)"
  1.3103 -    shows "continuous_on (cbox (c,a) (d,b)) (\<lambda>(x, y). f y x)"
  1.3104 -proof -
  1.3105 -  have "(\<lambda>(x, y). f y x) = (\<lambda>(x, y). f x y) \<circ> prod.swap"
  1.3106 -    by auto
  1.3107 -  then show ?thesis
  1.3108 -    apply (rule ssubst)
  1.3109 -    apply (rule continuous_on_compose)
  1.3110 -    apply (simp add: split_def)
  1.3111 -    apply (rule continuous_intros | simp add: assms)+
  1.3112 -    done
  1.3113 -qed
  1.3114 -
  1.3115  lemma integral_swap_2dim:
  1.3116    fixes f :: "['a::euclidean_space, 'b::euclidean_space] \<Rightarrow> 'c::banach"
  1.3117    assumes "continuous_on (cbox (a,c) (b,d)) (\<lambda>(x,y). f x y)"
  1.3118 @@ -10731,277 +8081,6 @@
  1.3119         (insert assms, simp_all add: powr_minus powr_realpow divide_simps)
  1.3120  qed
  1.3121  
  1.3122 -subsubsection \<open>Covering lemma\<close>
  1.3123 -
  1.3124 -
  1.3125 -text\<open> Some technical lemmas used in the approximation results that follow. Proof of the covering
  1.3126 -  lemma is an obvious multidimensional generalization of Lemma 3, p65 of Swartz's
  1.3127 -  "Introduction to Gauge Integrals". \<close>
  1.3128 -
  1.3129 -proposition covering_lemma:
  1.3130 -  assumes "S \<subseteq> cbox a b" "box a b \<noteq> {}" "gauge g"
  1.3131 -  obtains \<D> where
  1.3132 -    "countable \<D>"  "\<Union>\<D> \<subseteq> cbox a b"
  1.3133 -    "\<And>K. K \<in> \<D> \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
  1.3134 -    "pairwise (\<lambda>A B. interior A \<inter> interior B = {}) \<D>"
  1.3135 -    "\<And>K. K \<in> \<D> \<Longrightarrow> \<exists>x \<in> S \<inter> K. K \<subseteq> g x"
  1.3136 -    "\<And>u v. cbox u v \<in> \<D> \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
  1.3137 -    "S \<subseteq> \<Union>\<D>"
  1.3138 -proof -
  1.3139 -  have aibi: "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" and normab: "0 < norm(b - a)"
  1.3140 -    using \<open>box a b \<noteq> {}\<close> box_eq_empty box_sing by fastforce+
  1.3141 -  let ?K0 = "\<lambda>(n, f::'a\<Rightarrow>nat).
  1.3142 -                    cbox (\<Sum>i \<in> Basis. (a \<bullet> i + (f i / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)
  1.3143 -                         (\<Sum>i \<in> Basis. (a \<bullet> i + ((f i + 1) / 2^n) * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)"
  1.3144 -  let ?D0 = "?K0 ` (SIGMA n:UNIV. PiE Basis (\<lambda>i::'a. lessThan (2^n)))"
  1.3145 -  obtain \<D>0 where count: "countable \<D>0"
  1.3146 -             and sub: "\<Union>\<D>0 \<subseteq> cbox a b"
  1.3147 -             and int:  "\<And>K. K \<in> \<D>0 \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
  1.3148 -             and intdj: "\<And>A B. \<lbrakk>A \<in> \<D>0; B \<in> \<D>0\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
  1.3149 -             and SK: "\<And>x. x \<in> S \<Longrightarrow> \<exists>K \<in> \<D>0. x \<in> K \<and> K \<subseteq> g x"
  1.3150 -             and cbox: "\<And>u v. cbox u v \<in> \<D>0 \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
  1.3151 -             and fin: "\<And>K. K \<in> \<D>0 \<Longrightarrow> finite {L \<in> \<D>0. K \<subseteq> L}"
  1.3152 -  proof
  1.3153 -    show "countable ?D0"
  1.3154 -      by (simp add: countable_PiE)
  1.3155 -  next
  1.3156 -    show "\<Union>?D0 \<subseteq> cbox a b"
  1.3157 -      apply (simp add: UN_subset_iff)
  1.3158 -      apply (intro conjI allI ballI subset_box_imp)
  1.3159 -       apply (simp add: divide_simps zero_le_mult_iff aibi)
  1.3160 -      apply (force simp: aibi scaling_mono nat_less_real_le dest: PiE_mem)
  1.3161 -      done
  1.3162 -  next
  1.3163 -    show "\<And>K. K \<in> ?D0 \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
  1.3164 -      using \<open>box a b \<noteq> {}\<close>
  1.3165 -      by (clarsimp simp: box_eq_empty) (fastforce simp add: divide_simps dest: PiE_mem)
  1.3166 -  next
  1.3167 -    have realff: "(real w) * 2^m < (real v) * 2^n \<longleftrightarrow> w * 2^m < v * 2^n" for m n v w
  1.3168 -      using of_nat_less_iff less_imp_of_nat_less by fastforce
  1.3169 -    have *: "\<forall>v w. ?K0(m,v) \<subseteq> ?K0(n,w) \<or> ?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
  1.3170 -      for m n --\<open>The symmetry argument requires a single HOL formula\<close>
  1.3171 -    proof (rule linorder_wlog [where a=m and b=n], intro allI impI)
  1.3172 -      fix v w m and n::nat
  1.3173 -      assume "m \<le> n" --\<open>WLOG we can assume @{term"m \<le> n"}, when the first disjunct becomes impossible\<close>
  1.3174 -      have "?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
  1.3175 -        apply (simp add: subset_box disjoint_interval)
  1.3176 -        apply (rule ccontr)
  1.3177 -        apply (clarsimp simp add: aibi mult_le_cancel_right divide_le_cancel not_less not_le)
  1.3178 -        apply (drule_tac x=i in bspec, assumption)
  1.3179 -        using \<open>m\<le>n\<close> realff [of _ _ "1+_"] realff [of "1+_"_ "1+_"]
  1.3180 -        apply (auto simp: divide_simps add.commute not_le nat_le_iff_add realff)
  1.3181 -        apply (simp add: power_add, metis (no_types, hide_lams) mult_Suc mult_less_cancel2 not_less_eq mult.assoc)+
  1.3182 -        done
  1.3183 -      then show "?K0(m,v) \<subseteq> ?K0(n,w) \<or> ?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
  1.3184 -        by meson
  1.3185 -    qed auto
  1.3186 -    show "\<And>A B. \<lbrakk>A \<in> ?D0; B \<in> ?D0\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
  1.3187 -      apply (erule imageE SigmaE)+
  1.3188 -      using * by simp
  1.3189 -  next
  1.3190 -    show "\<exists>K \<in> ?D0. x \<in> K \<and> K \<subseteq> g x" if "x \<in> S" for x
  1.3191 -    proof (simp only: bex_simps split_paired_Bex_Sigma)
  1.3192 -      show "\<exists>n. \<exists>f \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ n}. x \<in> ?K0(n,f) \<and> ?K0(n,f) \<subseteq> g x"
  1.3193 -      proof -
  1.3194 -        obtain e where "0 < e"
  1.3195 -                   and e: "\<And>y. (\<And>i. i \<in> Basis \<Longrightarrow> \<bar>x \<bullet> i - y \<bullet> i\<bar> \<le> e) \<Longrightarrow> y \<in> g x"
  1.3196 -        proof -
  1.3197 -          have "x \<in> g x" "open (g x)"
  1.3198 -            using \<open>gauge g\<close> by (auto simp: gauge_def)
  1.3199 -          then obtain \<epsilon> where "0 < \<epsilon>" and \<epsilon>: "ball x \<epsilon> \<subseteq> g x"
  1.3200 -            using openE by blast
  1.3201 -          have "norm (x - y) < \<epsilon>"
  1.3202 -               if "(\<And>i. i \<in> Basis \<Longrightarrow> \<bar>x \<bullet> i - y \<bullet> i\<bar> \<le> \<epsilon> / (2 * real DIM('a)))" for y
  1.3203 -          proof -
  1.3204 -            have "norm (x - y) \<le> (\<Sum>i\<in>Basis. \<bar>x \<bullet> i - y \<bullet> i\<bar>)"
  1.3205 -              by (metis (no_types, lifting) inner_diff_left norm_le_l1 setsum.cong)
  1.3206 -            also have "... \<le> DIM('a) * (\<epsilon> / (2 * real DIM('a)))"
  1.3207 -              by (meson setsum_bounded_above that)
  1.3208 -            also have "... = \<epsilon> / 2"
  1.3209 -              by (simp add: divide_simps)
  1.3210 -            also have "... < \<epsilon>"
  1.3211 -              by (simp add: \<open>0 < \<epsilon>\<close>)
  1.3212 -            finally show ?thesis .
  1.3213 -          qed
  1.3214 -          then show ?thesis
  1.3215 -            by (rule_tac e = "\<epsilon> / 2 / DIM('a)" in that) (simp_all add:  \<open>0 < \<epsilon>\<close> dist_norm subsetD [OF \<epsilon>])
  1.3216 -        qed
  1.3217 -        have xab: "x \<in> cbox a b"
  1.3218 -          using \<open>x \<in> S\<close> \<open>S \<subseteq> cbox a b\<close> by blast
  1.3219 -        obtain n where n: "norm (b - a) / 2^n < e"
  1.3220 -          using real_arch_pow_inv [of "e / norm(b - a)" "1/2"] normab \<open>0 < e\<close>
  1.3221 -          by (auto simp: divide_simps)
  1.3222 -        then have "norm (b - a) < e * 2^n"
  1.3223 -          by (auto simp: divide_simps)
  1.3224 -        then have bai: "b \<bullet> i - a \<bullet> i < e * 2 ^ n" if "i \<in> Basis" for i
  1.3225 -        proof -
  1.3226 -          have "b \<bullet> i - a \<bullet> i \<le> norm (b - a)"
  1.3227 -            by (metis abs_of_nonneg dual_order.trans inner_diff_left linear norm_ge_zero Basis_le_norm that)
  1.3228 -          also have "... < e * 2 ^ n"
  1.3229 -            using \<open>norm (b - a) < e * 2 ^ n\<close> by blast
  1.3230 -          finally show ?thesis .
  1.3231 -        qed
  1.3232 -        have D: "(a + n \<le> x \<and> x \<le> a + m) \<Longrightarrow> (a + n \<le> y \<and> y \<le> a + m) \<Longrightarrow> abs(x - y) \<le> m - n"
  1.3233 -                 for a m n x and y::real
  1.3234 -          by auto
  1.3235 -        have "\<forall>i\<in>Basis. \<exists>k<2 ^ n. (a \<bullet> i + real k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i \<and>
  1.3236 -               x \<bullet> i \<le> a \<bullet> i + (real k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n)"
  1.3237 -        proof
  1.3238 -          fix i::'a assume "i \<in> Basis"
  1.3239 -          consider "x \<bullet> i = b \<bullet> i" | "x \<bullet> i < b \<bullet> i"
  1.3240 -            using \<open>i \<in> Basis\<close> mem_box(2) xab by force
  1.3241 -          then show "\<exists>k<2 ^ n. (a \<bullet> i + real k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i \<and>
  1.3242 -                          x \<bullet> i \<le> a \<bullet> i + (real k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n)"
  1.3243 -          proof cases
  1.3244 -            case 1 then show ?thesis
  1.3245 -              by (rule_tac x = "2^n - 1" in exI) (auto simp: algebra_simps divide_simps of_nat_diff \<open>i \<in> Basis\<close> aibi)
  1.3246 -          next
  1.3247 -            case 2
  1.3248 -            then have abi_less: "a \<bullet> i < b \<bullet> i"
  1.3249 -              using \<open>i \<in> Basis\<close> xab by (auto simp: mem_box)
  1.3250 -            let ?k = "nat \<lfloor>2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)\<rfloor>"
  1.3251 -            show ?thesis
  1.3252 -            proof (intro exI conjI)
  1.3253 -              show "?k < 2 ^ n"
  1.3254 -                using aibi xab \<open>i \<in> Basis\<close>
  1.3255 -                by (force simp: nat_less_iff floor_less_iff divide_simps 2 mem_box)
  1.3256 -            next
  1.3257 -              have "a \<bullet> i + real ?k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le>
  1.3258 -                    a \<bullet> i + (2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
  1.3259 -                apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
  1.3260 -                using aibi [OF \<open>i \<in> Basis\<close>] xab 2
  1.3261 -                  apply (simp_all add: \<open>i \<in> Basis\<close> mem_box divide_simps)
  1.3262 -                done
  1.3263 -              also have "... = x \<bullet> i"
  1.3264 -                using abi_less by (simp add: divide_simps)
  1.3265 -              finally show "a \<bullet> i + real ?k * (b \<bullet> i - a \<bullet> i) / 2 ^ n \<le> x \<bullet> i" .
  1.3266 -            next
  1.3267 -              have "x \<bullet> i \<le> a \<bullet> i + (2 ^ n * (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
  1.3268 -                using abi_less by (simp add: divide_simps algebra_simps)
  1.3269 -              also have "... \<le> a \<bullet> i + (real ?k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n"
  1.3270 -                apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
  1.3271 -                using aibi [OF \<open>i \<in> Basis\<close>] xab
  1.3272 -                  apply (auto simp: \<open>i \<in> Basis\<close> mem_box divide_simps)
  1.3273 -                done
  1.3274 -              finally show "x \<bullet> i \<le> a \<bullet> i + (real ?k + 1) * (b \<bullet> i - a \<bullet> i) / 2 ^ n" .
  1.3275 -            qed
  1.3276 -          qed
  1.3277 -        qed
  1.3278 -        then have "\<exists>f\<in>Basis \<rightarrow>\<^sub>E {..<2 ^ n}. x \<in> ?K0(n,f)"
  1.3279 -          apply (simp add: mem_box Bex_def)
  1.3280 -          apply (clarify dest!: bchoice)
  1.3281 -          apply (rule_tac x="restrict f Basis" in exI, simp)
  1.3282 -          done
  1.3283 -        moreover have "\<And>f. x \<in> ?K0(n,f) \<Longrightarrow> ?K0(n,f) \<subseteq> g x"
  1.3284 -          apply (clarsimp simp add: mem_box)
  1.3285 -          apply (rule e)
  1.3286 -          apply (drule bspec D, assumption)+
  1.3287 -          apply (erule order_trans)
  1.3288 -          apply (simp add: divide_simps)
  1.3289 -          using bai by (force simp: algebra_simps)
  1.3290 -        ultimately show ?thesis by auto
  1.3291 -      qed
  1.3292 -    qed
  1.3293 -  next
  1.3294 -    show "\<And>u v. cbox u v \<in> ?D0 \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
  1.3295 -      by (force simp: eq_cbox box_eq_empty field_simps dest!: aibi)
  1.3296 -  next
  1.3297 -    obtain j::'a where "j \<in> Basis"
  1.3298 -      using nonempty_Basis by blast
  1.3299 -    have "finite {L \<in> ?D0. ?K0(n,f) \<subseteq> L}" if "f \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ n}" for n f
  1.3300 -    proof (rule finite_subset)
  1.3301 -      let ?B = "(\<lambda>(n, f::'a\<Rightarrow>nat). cbox (\<Sum>i\<in>Basis. (a \<bullet> i + (f i) / 2^n * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i)
  1.3302 -                                        (\<Sum>i\<in>Basis. (a \<bullet> i + ((f i) + 1) / 2^n * (b \<bullet> i - a \<bullet> i)) *\<^sub>R i))
  1.3303 -                ` (SIGMA m:atMost n. PiE Basis (\<lambda>i::'a. lessThan (2^m)))"
  1.3304 -      have "?K0(m,g) \<in> ?B" if "g \<in> Basis \<rightarrow>\<^sub>E {..<2 ^ m}" "?K0(n,f) \<subseteq> ?K0(m,g)" for m g
  1.3305 -      proof -
  1.3306 -        have dd: "w / m \<le> v / n \<and> (v+1) / n \<le> (w+1) / m
  1.3307 -                  \<Longrightarrow> inverse n \<le> inverse m" for w m v n::real
  1.3308 -          by (auto simp: divide_simps algebra_simps)
  1.3309 -        have bjaj: "b \<bullet> j - a \<bullet> j > 0"
  1.3310 -          using \<open>j \<in> Basis\<close> \<open>box a b \<noteq> {}\<close> box_eq_empty(1) by fastforce
  1.3311 -        have "((g j) / 2 ^ m) * (b \<bullet> j - a \<bullet> j) \<le> ((f j) / 2 ^ n) * (b \<bullet> j - a \<bullet> j) \<and>
  1.3312 -              (((f j) + 1) / 2 ^ n) * (b \<bullet> j - a \<bullet> j) \<le> (((g j) + 1) / 2 ^ m) * (b \<bullet> j - a \<bullet> j)"
  1.3313 -          using that \<open>j \<in> Basis\<close> by (simp add: subset_box algebra_simps divide_simps aibi)
  1.3314 -        then have "((g j) / 2 ^ m) \<le> ((f j) / 2 ^ n) \<and>
  1.3315 -          ((real(f j) + 1) / 2 ^ n) \<le> ((real(g j) + 1) / 2 ^ m)"
  1.3316 -          by (metis bjaj mult.commute of_nat_1 of_nat_add real_mult_le_cancel_iff2)
  1.3317 -        then have "inverse (2^n) \<le> (inverse (2^m) :: real)"
  1.3318 -          by (rule dd)
  1.3319 -        then have "m \<le> n"
  1.3320 -          by auto
  1.3321 -        show ?thesis
  1.3322 -          by (rule imageI) (simp add: \<open>m \<le> n\<close> that)
  1.3323 -      qed
  1.3324 -      then show "{L \<in> ?D0. ?K0(n,f) \<subseteq> L} \<subseteq> ?B"
  1.3325 -        by auto
  1.3326 -      show "finite ?B"
  1.3327 -        by (intro finite_imageI finite_SigmaI finite_atMost finite_lessThan finite_PiE finite_Basis)
  1.3328 -    qed
  1.3329 -    then show "finite {L \<in> ?D0. K \<subseteq> L}" if "K \<in> ?D0" for K
  1.3330 -      using that by auto
  1.3331 -  qed
  1.3332 -  let ?D1 = "{K \<in> \<D>0. \<exists>x \<in> S \<inter> K. K \<subseteq> g x}"
  1.3333 -  obtain \<D> where count: "countable \<D>"
  1.3334 -             and sub: "\<Union>\<D> \<subseteq> cbox a b"  "S \<subseteq> \<Union>\<D>"
  1.3335 -             and int:  "\<And>K. K \<in> \<D> \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
  1.3336 -             and intdj: "\<And>A B. \<lbrakk>A \<in> \<D>; B \<in> \<D>\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
  1.3337 -             and SK: "\<And>K. K \<in> \<D> \<Longrightarrow> \<exists>x. x \<in> S \<inter> K \<and> K \<subseteq> g x"
  1.3338 -             and cbox: "\<And>u v. cbox u v \<in> \<D> \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
  1.3339 -             and fin: "\<And>K. K \<in> \<D> \<Longrightarrow> finite {L. L \<in> \<D> \<and> K \<subseteq> L}"
  1.3340 -  proof
  1.3341 -    show "countable ?D1" using count countable_subset
  1.3342 -      by (simp add: count countable_subset)
  1.3343 -    show "\<Union>?D1 \<subseteq> cbox a b"
  1.3344 -      using sub by blast
  1.3345 -    show "S \<subseteq> \<Union>?D1"
  1.3346 -      using SK by (force simp:)
  1.3347 -    show "\<And>K. K \<in> ?D1 \<Longrightarrow> (interior K \<noteq> {}) \<and> (\<exists>c d. K = cbox c d)"
  1.3348 -      using int by blast
  1.3349 -    show "\<And>A B. \<lbrakk>A \<in> ?D1; B \<in> ?D1\<rbrakk> \<Longrightarrow> A \<subseteq> B \<or> B \<subseteq> A \<or> interior A \<inter> interior B = {}"
  1.3350 -      using intdj by blast
  1.3351 -    show "\<And>K. K \<in> ?D1 \<Longrightarrow> \<exists>x. x \<in> S \<inter> K \<and> K \<subseteq> g x"
  1.3352 -      by auto
  1.3353 -    show "\<And>u v. cbox u v \<in> ?D1 \<Longrightarrow> \<exists>n. \<forall>i \<in> Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
  1.3354 -      using cbox by blast
  1.3355 -    show "\<And>K. K \<in> ?D1 \<Longrightarrow> finite {L. L \<in> ?D1 \<and> K \<subseteq> L}"
  1.3356 -      using fin by simp (metis (mono_tags, lifting) Collect_mono rev_finite_subset)
  1.3357 -  qed
  1.3358 -  let ?\<D> = "{K \<in> \<D>. \<forall>K'. K' \<in> \<D> \<and> K \<noteq> K' \<longrightarrow> ~(K \<subseteq> K')}"
  1.3359 -  show ?thesis
  1.3360 -  proof (rule that)
  1.3361 -    show "countable ?\<D>"
  1.3362 -      by (blast intro: countable_subset [OF _ count])
  1.3363 -    show "\<Union>?\<D> \<subseteq> cbox a b"
  1.3364 -      using sub by blast
  1.3365 -    show "S \<subseteq> \<Union>?\<D>"
  1.3366 -    proof clarsimp
  1.3367 -      fix x
  1.3368 -      assume "x \<in> S"
  1.3369 -      then obtain X where "x \<in> X" "X \<in> \<D>" using \<open>S \<subseteq> \<Union>\<D>\<close> by blast
  1.3370 -      let ?R = "{(K,L). K \<in> \<D> \<and> L \<in> \<D> \<and> L \<subset> K}"
  1.3371 -      have irrR: "irrefl ?R" by (force simp: irrefl_def)
  1.3372 -      have traR: "trans ?R" by (force simp: trans_def)
  1.3373 -      have finR: "\<And>x. finite {y. (y, x) \<in> ?R}"
  1.3374 -        by simp (metis (mono_tags, lifting) fin \<open>X \<in> \<D>\<close> finite_subset mem_Collect_eq psubset_imp_subset subsetI)
  1.3375 -      have "{X \<in> \<D>. x \<in> X} \<noteq> {}"
  1.3376 -        using \<open>X \<in> \<D>\<close> \<open>x \<in> X\<close> by blast
  1.3377 -      then obtain Y where "Y \<in> {X \<in> \<D>. x \<in> X}" "\<And>Y'. (Y', Y) \<in> ?R \<Longrightarrow> Y' \<notin> {X \<in> \<D>. x \<in> X}"
  1.3378 -        by (rule wfE_min' [OF wf_finite_segments [OF irrR traR finR]]) blast
  1.3379 -      then show "\<exists>Y. Y \<in> \<D> \<and> (\<forall>K'. K' \<in> \<D> \<and> Y \<noteq> K' \<longrightarrow> \<not> Y \<subseteq> K') \<and> x \<in> Y"
  1.3380 -        by blast
  1.3381 -    qed
  1.3382 -    show "\<And>K. K \<in> ?\<D> \<Longrightarrow> interior K \<noteq> {} \<and> (\<exists>c d. K = cbox c d)"
  1.3383 -      by (blast intro: dest: int)
  1.3384 -    show "pairwise (\<lambda>A B. interior A \<inter> interior B = {}) ?\<D>"
  1.3385 -      using intdj by (simp add: pairwise_def) metis
  1.3386 -    show "\<And>K. K \<in> ?\<D> \<Longrightarrow> \<exists>x \<in> S \<inter> K. K \<subseteq> g x"
  1.3387 -      using SK by force
  1.3388 -    show "\<And>u v. cbox u v \<in> ?\<D> \<Longrightarrow> \<exists>n. \<forall>i\<in>Basis. v \<bullet> i - u \<bullet> i = (b \<bullet> i - a \<bullet> i) / 2^n"
  1.3389 -      using cbox by force
  1.3390 -    qed
  1.3391 -qed
  1.3392 -
  1.3393  subsubsection \<open>Adaption to ordered Euclidean spaces and the Cartesian Euclidean space\<close>
  1.3394  
  1.3395  lemma integral_component_eq_cart[simp]: