Theory Tagged_Division

theory Tagged_Division
imports Topology_Euclidean_Space
(*  Title:      HOL/Analysis/Tagged_Division.thy
    Author:     John Harrison
    Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light); proofs reworked by LCP
*)

section ‹Tagged divisions used for the Henstock-Kurzweil gauge integration›

theory Tagged_Division
imports
  Topology_Euclidean_Space
begin

term comm_monoid

lemma sum_Sigma_product:
  assumes "finite S"
    and "⋀i. i ∈ S ⟹ finite (T i)"
  shows "(∑i∈S. sum (x i) (T i)) = (∑(i, j)∈Sigma S T. x i j)"
  using assms
proof induct
  case empty
  then show ?case
    by simp
next
  case (insert a S)
  show ?case
    by (simp add: insert.hyps(1) insert.prems sum.Sigma)
qed

lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
  scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
  scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one


subsection ‹Sundries›


text‹A transitive relation is well-founded if all initial segments are finite.›
lemma wf_finite_segments:
  assumes "irrefl r" and "trans r" and "⋀x. finite {y. (y, x) ∈ r}"
  shows "wf (r)"
  apply (simp add: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
  using acyclic_def assms irrefl_def trans_Restr by fastforce

text‹For creating values between @{term u} and @{term v}.›
lemma scaling_mono:
  fixes u::"'a::linordered_field"
  assumes "u ≤ v" "0 ≤ r" "r ≤ s"
    shows "u + r * (v - u) / s ≤ v"
proof -
  have "r/s ≤ 1" using assms
    using divide_le_eq_1 by fastforce
  then have "(r/s) * (v - u) ≤ 1 * (v - u)"
    by (meson diff_ge_0_iff_ge mult_right_mono ‹u ≤ v›)
  then show ?thesis
    by (simp add: field_simps)
qed

subsection ‹Some useful lemmas about intervals.›

lemma interior_subset_union_intervals:
  assumes "i = cbox a b"
    and "j = cbox c d"
    and "interior j ≠ {}"
    and "i ⊆ j ∪ S"
    and "interior i ∩ interior j = {}"
  shows "interior i ⊆ interior S"
proof -
  have "box a b ∩ cbox c d = {}"
     using inter_interval_mixed_eq_empty[of c d a b] assms
     unfolding interior_cbox by auto
  moreover
  have "box a b ⊆ cbox c d ∪ S"
    apply (rule order_trans,rule box_subset_cbox)
    using assms by auto
  ultimately
  show ?thesis
    unfolding assms interior_cbox
      by auto (metis IntI UnE empty_iff interior_maximal open_box subsetCE subsetI)
qed

lemma interior_Union_subset_cbox:
  assumes "finite f"
  assumes f: "⋀s. s ∈ f ⟹ ∃a b. s = cbox a b" "⋀s. s ∈ f ⟹ interior s ⊆ t"
    and t: "closed t"
  shows "interior (⋃f) ⊆ t"
proof -
  have [simp]: "s ∈ f ⟹ closed s" for s
    using f by auto
  define E where "E = {s∈f. interior s = {}}"
  then have "finite E" "E ⊆ {s∈f. interior s = {}}"
    using ‹finite f› by auto
  then have "interior (⋃f) = interior (⋃(f - E))"
  proof (induction E rule: finite_subset_induct')
    case (insert s f')
    have "interior (⋃(f - insert s f') ∪ s) = interior (⋃(f - insert s f'))"
      using insert.hyps ‹finite f› by (intro interior_closed_Un_empty_interior) auto
    also have "⋃(f - insert s f') ∪ s = ⋃(f - f')"
      using insert.hyps by auto
    finally show ?case
      by (simp add: insert.IH)
  qed simp
  also have "… ⊆ ⋃(f - E)"
    by (rule interior_subset)
  also have "… ⊆ t"
  proof (rule Union_least)
    fix s assume "s ∈ f - E"
    with f[of s] obtain a b where s: "s ∈ f" "s = cbox a b" "box a b ≠ {}"
      by (fastforce simp: E_def)
    have "closure (interior s) ⊆ closure t"
      by (intro closure_mono f ‹s ∈ f›)
    with s ‹closed t› show "s ⊆ t"
      by simp
  qed
  finally show ?thesis .
qed

lemma Int_interior_Union_intervals:
    "⟦finite ℱ; open S; ⋀T. T∈ℱ ⟹ ∃a b. T = cbox a b; ⋀T. T∈ℱ ⟹ S ∩ (interior T) = {}⟧ 
    ⟹ S ∩ interior (⋃ℱ) = {}"
  using interior_Union_subset_cbox[of  "UNIV - S"] by auto

lemma interval_split:
  fixes a :: "'a::euclidean_space"
  assumes "k ∈ Basis"
  shows
    "cbox a b ∩ {x. x∙k ≤ c} = cbox a (∑i∈Basis. (if i = k then min (b∙k) c else b∙i) *R i)"
    "cbox a b ∩ {x. x∙k ≥ c} = cbox (∑i∈Basis. (if i = k then max (a∙k) c else a∙i) *R i) b"
  using assms by (rule_tac set_eqI; auto simp: mem_box)+

lemma interval_not_empty: "∀i∈Basis. a∙i ≤ b∙i ⟹ cbox a b ≠ {}"
  by (simp add: box_ne_empty)

subsection ‹Bounds on intervals where they exist.›

definition interval_upperbound :: "('a::euclidean_space) set ⇒ 'a"
  where "interval_upperbound s = (∑i∈Basis. (SUP x:s. x∙i) *R i)"

definition interval_lowerbound :: "('a::euclidean_space) set ⇒ 'a"
  where "interval_lowerbound s = (∑i∈Basis. (INF x:s. x∙i) *R i)"

lemma interval_upperbound[simp]:
  "∀i∈Basis. a∙i ≤ b∙i ⟹
    interval_upperbound (cbox a b) = (b::'a::euclidean_space)"
  unfolding interval_upperbound_def euclidean_representation_sum cbox_def
  by (safe intro!: cSup_eq) auto

lemma interval_lowerbound[simp]:
  "∀i∈Basis. a∙i ≤ b∙i ⟹
    interval_lowerbound (cbox a b) = (a::'a::euclidean_space)"
  unfolding interval_lowerbound_def euclidean_representation_sum cbox_def
  by (safe intro!: cInf_eq) auto

lemmas interval_bounds = interval_upperbound interval_lowerbound

lemma
  fixes X::"real set"
  shows interval_upperbound_real[simp]: "interval_upperbound X = Sup X"
    and interval_lowerbound_real[simp]: "interval_lowerbound X = Inf X"
  by (auto simp: interval_upperbound_def interval_lowerbound_def)

lemma interval_bounds'[simp]:
  assumes "cbox a b ≠ {}"
  shows "interval_upperbound (cbox a b) = b"
    and "interval_lowerbound (cbox a b) = a"
  using assms unfolding box_ne_empty by auto

lemma interval_upperbound_Times:
  assumes "A ≠ {}" and "B ≠ {}"
  shows "interval_upperbound (A × B) = (interval_upperbound A, interval_upperbound B)"
proof-
  from assms have fst_image_times': "A = fst ` (A × B)" by simp
  have "(∑i∈Basis. (SUP x:A × B. x ∙ (i, 0)) *R i) = (∑i∈Basis. (SUP x:A. x ∙ i) *R i)"
      by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
  moreover from assms have snd_image_times': "B = snd ` (A × B)" by simp
  have "(∑i∈Basis. (SUP x:A × B. x ∙ (0, i)) *R i) = (∑i∈Basis. (SUP x:B. x ∙ i) *R i)"
      by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
  ultimately show ?thesis unfolding interval_upperbound_def
      by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
qed

lemma interval_lowerbound_Times:
  assumes "A ≠ {}" and "B ≠ {}"
  shows "interval_lowerbound (A × B) = (interval_lowerbound A, interval_lowerbound B)"
proof-
  from assms have fst_image_times': "A = fst ` (A × B)" by simp
  have "(∑i∈Basis. (INF x:A × B. x ∙ (i, 0)) *R i) = (∑i∈Basis. (INF x:A. x ∙ i) *R i)"
      by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
  moreover from assms have snd_image_times': "B = snd ` (A × B)" by simp
  have "(∑i∈Basis. (INF x:A × B. x ∙ (0, i)) *R i) = (∑i∈Basis. (INF x:B. x ∙ i) *R i)"
      by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
  ultimately show ?thesis unfolding interval_lowerbound_def
      by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
qed

subsection ‹The notion of a gauge --- simply an open set containing the point.›

definition "gauge γ ⟷ (∀x. x ∈ γ x ∧ open (γ x))"

lemma gaugeI:
  assumes "⋀x. x ∈ γ x"
    and "⋀x. open (γ x)"
  shows "gauge γ"
  using assms unfolding gauge_def by auto

lemma gaugeD[dest]:
  assumes "gauge γ"
  shows "x ∈ γ x"
    and "open (γ x)"
  using assms unfolding gauge_def by auto

lemma gauge_ball_dependent: "∀x. 0 < e x ⟹ gauge (λx. ball x (e x))"
  unfolding gauge_def by auto

lemma gauge_ball[intro]: "0 < e ⟹ gauge (λx. ball x e)"
  unfolding gauge_def by auto

lemma gauge_trivial[intro!]: "gauge (λx. ball x 1)"
  by (rule gauge_ball) auto

lemma gauge_Int[intro]: "gauge γ1 ⟹ gauge γ2 ⟹ gauge (λx. γ1 x ∩ γ2 x)"
  unfolding gauge_def by auto

lemma gauge_reflect:
  fixes γ :: "'a::euclidean_space ⇒ 'a set"
  shows "gauge γ ⟹ gauge (λx. uminus ` γ (- x))"
  using equation_minus_iff
  by (auto simp: gauge_def surj_def intro!: open_surjective_linear_image linear_uminus)

lemma gauge_Inter:
  assumes "finite S"
    and "⋀u. u∈S ⟹ gauge (f u)"
  shows "gauge (λx. ⋂{f u x | u. u ∈ S})"
proof -
  have *: "⋀x. {f u x |u. u ∈ S} = (λu. f u x) ` S"
    by auto
  show ?thesis
    unfolding gauge_def unfolding *
    using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto
qed

lemma gauge_existence_lemma:
  "(∀x. ∃d :: real. p x ⟶ 0 < d ∧ q d x) ⟷ (∀x. ∃d>0. p x ⟶ q d x)"
  by (metis zero_less_one)

subsection ‹Attempt a systematic general set of "offset" results for components.›

lemma gauge_modify:
  assumes "(∀S. open S ⟶ open {x. f(x) ∈ S})" "gauge d"
  shows "gauge (λx. {y. f y ∈ d (f x)})"
  using assms unfolding gauge_def by force

subsection ‹Divisions.›

definition division_of (infixl "division'_of" 40)
where
  "s division_of i ⟷
    finite s ∧
    (∀K∈s. K ⊆ i ∧ K ≠ {} ∧ (∃a b. K = cbox a b)) ∧
    (∀K1∈s. ∀K2∈s. K1 ≠ K2 ⟶ interior(K1) ∩ interior(K2) = {}) ∧
    (⋃s = i)"

lemma division_ofD[dest]:
  assumes "s division_of i"
  shows "finite s"
    and "⋀K. K ∈ s ⟹ K ⊆ i"
    and "⋀K. K ∈ s ⟹ K ≠ {}"
    and "⋀K. K ∈ s ⟹ ∃a b. K = cbox a b"
    and "⋀K1 K2. K1 ∈ s ⟹ K2 ∈ s ⟹ K1 ≠ K2 ⟹ interior(K1) ∩ interior(K2) = {}"
    and "⋃s = i"
  using assms unfolding division_of_def by auto

lemma division_ofI:
  assumes "finite s"
    and "⋀K. K ∈ s ⟹ K ⊆ i"
    and "⋀K. K ∈ s ⟹ K ≠ {}"
    and "⋀K. K ∈ s ⟹ ∃a b. K = cbox a b"
    and "⋀K1 K2. K1 ∈ s ⟹ K2 ∈ s ⟹ K1 ≠ K2 ⟹ interior K1 ∩ interior K2 = {}"
    and "⋃s = i"
  shows "s division_of i"
  using assms unfolding division_of_def by auto

lemma division_of_finite: "s division_of i ⟹ finite s"
  by auto

lemma division_of_self[intro]: "cbox a b ≠ {} ⟹ {cbox a b} division_of (cbox a b)"
  unfolding division_of_def by auto

lemma division_of_trivial[simp]: "s division_of {} ⟷ s = {}"
  unfolding division_of_def by auto

lemma division_of_sing[simp]:
  "s division_of cbox a (a::'a::euclidean_space) ⟷ s = {cbox a a}"
  (is "?l = ?r")
proof
  assume ?r
  moreover
  { fix K
    assume "s = {{a}}" "K∈s"
    then have "∃x y. K = cbox x y"
      apply (rule_tac x=a in exI)+
      apply force
      done
  }
  ultimately show ?l
    unfolding division_of_def cbox_sing by auto
next
  assume ?l
  have "x = {a}" if  "x ∈ s" for x
    by (metis ‹s division_of cbox a a› cbox_sing division_ofD(2) division_ofD(3) subset_singletonD that)
  moreover have "s ≠ {}"
    using ‹s division_of cbox a a› by auto
  ultimately show ?r
    unfolding cbox_sing by auto
qed

lemma elementary_empty: obtains p where "p division_of {}"
  unfolding division_of_trivial by auto

lemma elementary_interval: obtains p where "p division_of (cbox a b)"
  by (metis division_of_trivial division_of_self)

lemma division_contains: "s division_of i ⟹ ∀x∈i. ∃k∈s. x ∈ k"
  unfolding division_of_def by auto

lemma forall_in_division:
  "d division_of i ⟹ (∀x∈d. P x) ⟷ (∀a b. cbox a b ∈ d ⟶ P (cbox a b))"
  unfolding division_of_def by fastforce

lemma cbox_division_memE:
  assumes 𝒟: "K ∈ 𝒟" "𝒟 division_of S"
  obtains a b where "K = cbox a b" "K ≠ {}" "K ⊆ S"
  using assms unfolding division_of_def by metis

lemma division_of_subset:
  assumes "p division_of (⋃p)"
    and "q ⊆ p"
  shows "q division_of (⋃q)"
proof (rule division_ofI)
  note * = division_ofD[OF assms(1)]
  show "finite q"
    using "*"(1) assms(2) infinite_super by auto
  {
    fix k
    assume "k ∈ q"
    then have kp: "k ∈ p"
      using assms(2) by auto
    show "k ⊆ ⋃q"
      using ‹k ∈ q› by auto
    show "∃a b. k = cbox a b"
      using *(4)[OF kp] by auto
    show "k ≠ {}"
      using *(3)[OF kp] by auto
  }
  fix k1 k2
  assume "k1 ∈ q" "k2 ∈ q" "k1 ≠ k2"
  then have **: "k1 ∈ p" "k2 ∈ p" "k1 ≠ k2"
    using assms(2) by auto
  show "interior k1 ∩ interior k2 = {}"
    using *(5)[OF **] by auto
qed auto

lemma division_of_union_self[intro]: "p division_of s ⟹ p division_of (⋃p)"
  unfolding division_of_def by auto

lemma division_inter:
  fixes s1 s2 :: "'a::euclidean_space set"
  assumes "p1 division_of s1"
    and "p2 division_of s2"
  shows "{k1 ∩ k2 | k1 k2. k1 ∈ p1 ∧ k2 ∈ p2 ∧ k1 ∩ k2 ≠ {}} division_of (s1 ∩ s2)"
  (is "?A' division_of _")
proof -
  let ?A = "{s. s ∈  (λ(k1,k2). k1 ∩ k2) ` (p1 × p2) ∧ s ≠ {}}"
  have *: "?A' = ?A" by auto
  show ?thesis
    unfolding *
  proof (rule division_ofI)
    have "?A ⊆ (λ(x, y). x ∩ y) ` (p1 × p2)"
      by auto
    moreover have "finite (p1 × p2)"
      using assms unfolding division_of_def by auto
    ultimately show "finite ?A" by auto
    have *: "⋀s. ⋃{x∈s. x ≠ {}} = ⋃s"
      by auto
    show "⋃?A = s1 ∩ s2"
      unfolding * 
      using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] by auto
    {
      fix k
      assume "k ∈ ?A"
      then obtain k1 k2 where k: "k = k1 ∩ k2" "k1 ∈ p1" "k2 ∈ p2" "k ≠ {}"
        by auto
      then show "k ≠ {}"
        by auto
      show "k ⊆ s1 ∩ s2"
        using division_ofD(2)[OF assms(1) k(2)] and division_ofD(2)[OF assms(2) k(3)]
        unfolding k by auto
      obtain a1 b1 where k1: "k1 = cbox a1 b1"
        using division_ofD(4)[OF assms(1) k(2)] by blast
      obtain a2 b2 where k2: "k2 = cbox a2 b2"
        using division_ofD(4)[OF assms(2) k(3)] by blast
      show "∃a b. k = cbox a b"
        unfolding k k1 k2 unfolding Int_interval by auto
    }
    fix k1 k2
    assume "k1 ∈ ?A"
    then obtain x1 y1 where k1: "k1 = x1 ∩ y1" "x1 ∈ p1" "y1 ∈ p2" "k1 ≠ {}"
      by auto
    assume "k2 ∈ ?A"
    then obtain x2 y2 where k2: "k2 = x2 ∩ y2" "x2 ∈ p1" "y2 ∈ p2" "k2 ≠ {}"
      by auto
    assume "k1 ≠ k2"
    then have th: "x1 ≠ x2 ∨ y1 ≠ y2"
      unfolding k1 k2 by auto
    have *: "interior x1 ∩ interior x2 = {} ∨ interior y1 ∩ interior y2 = {} ⟹
      interior (x1 ∩ y1) ⊆ interior x1 ⟹ interior (x1 ∩ y1) ⊆ interior y1 ⟹
      interior (x2 ∩ y2) ⊆ interior x2 ⟹ interior (x2 ∩ y2) ⊆ interior y2 ⟹
      interior (x1 ∩ y1) ∩ interior (x2 ∩ y2) = {}" by auto
    show "interior k1 ∩ interior k2 = {}"
      unfolding k1 k2
      apply (rule *)
      using assms division_ofD(5) k1 k2(2) k2(3) th apply auto
      done
  qed
qed

lemma division_inter_1:
  assumes "d division_of i"
    and "cbox a (b::'a::euclidean_space) ⊆ i"
  shows "{cbox a b ∩ k | k. k ∈ d ∧ cbox a b ∩ k ≠ {}} division_of (cbox a b)"
proof (cases "cbox a b = {}")
  case True
  show ?thesis
    unfolding True and division_of_trivial by auto
next
  case False
  have *: "cbox a b ∩ i = cbox a b" using assms(2) by auto
  show ?thesis
    using division_inter[OF division_of_self[OF False] assms(1)]
    unfolding * by auto
qed

lemma elementary_Int:
  fixes s t :: "'a::euclidean_space set"
  assumes "p1 division_of s"
    and "p2 division_of t"
  shows "∃p. p division_of (s ∩ t)"
using assms division_inter by blast

lemma elementary_Inter:
  assumes "finite f"
    and "f ≠ {}"
    and "∀s∈f. ∃p. p division_of (s::('a::euclidean_space) set)"
  shows "∃p. p division_of (⋂f)"
  using assms
proof (induct f rule: finite_induct)
  case (insert x f)
  show ?case
  proof (cases "f = {}")
    case True
    then show ?thesis
      unfolding True using insert by auto
  next
    case False
    obtain p where "p division_of ⋂f"
      using insert(3)[OF False insert(5)[unfolded ball_simps,THEN conjunct2]] ..
    moreover obtain px where "px division_of x"
      using insert(5)[rule_format,OF insertI1] ..
    ultimately show ?thesis
      by (simp add: elementary_Int Inter_insert)
  qed
qed auto

lemma division_disjoint_union:
  assumes "p1 division_of s1"
    and "p2 division_of s2"
    and "interior s1 ∩ interior s2 = {}"
  shows "(p1 ∪ p2) division_of (s1 ∪ s2)"
proof (rule division_ofI)
  note d1 = division_ofD[OF assms(1)]
  note d2 = division_ofD[OF assms(2)]
  show "finite (p1 ∪ p2)"
    using d1(1) d2(1) by auto
  show "⋃(p1 ∪ p2) = s1 ∪ s2"
    using d1(6) d2(6) by auto
  {
    fix k1 k2
    assume as: "k1 ∈ p1 ∪ p2" "k2 ∈ p1 ∪ p2" "k1 ≠ k2"
    moreover
    let ?g="interior k1 ∩ interior k2 = {}"
    {
      assume as: "k1∈p1" "k2∈p2"
      have ?g
        using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
        using assms(3) by blast
    }
    moreover
    {
      assume as: "k1∈p2" "k2∈p1"
      have ?g
        using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
        using assms(3) by blast
    }
    ultimately show ?g
      using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto
  }
  fix k
  assume k: "k ∈ p1 ∪ p2"
  show "k ⊆ s1 ∪ s2"
    using k d1(2) d2(2) by auto
  show "k ≠ {}"
    using k d1(3) d2(3) by auto
  show "∃a b. k = cbox a b"
    using k d1(4) d2(4) by auto
qed

lemma partial_division_extend_1:
  fixes a b c d :: "'a::euclidean_space"
  assumes incl: "cbox c d ⊆ cbox a b"
    and nonempty: "cbox c d ≠ {}"
  obtains p where "p division_of (cbox a b)" "cbox c d ∈ p"
proof
  let ?B = "λf::'a⇒'a × 'a.
    cbox (∑i∈Basis. (fst (f i) ∙ i) *R i) (∑i∈Basis. (snd (f i) ∙ i) *R i)"
  define p where "p = ?B ` (Basis →E {(a, c), (c, d), (d, b)})"

  show "cbox c d ∈ p"
    unfolding p_def
    by (auto simp add: box_eq_empty cbox_def intro!: image_eqI[where x="λ(i::'a)∈Basis. (c, d)"])
  have ord: "a ∙ i ≤ c ∙ i" "c ∙ i ≤ d ∙ i" "d ∙ i ≤ b ∙ i" if "i ∈ Basis" for i
    using incl nonempty that
    unfolding box_eq_empty subset_box by (auto simp: not_le)

  show "p division_of (cbox a b)"
  proof (rule division_ofI)
    show "finite p"
      unfolding p_def by (auto intro!: finite_PiE)
    {
      fix k
      assume "k ∈ p"
      then obtain f where f: "f ∈ Basis →E {(a, c), (c, d), (d, b)}" and k: "k = ?B f"
        by (auto simp: p_def)
      then show "∃a b. k = cbox a b"
        by auto
      have "k ⊆ cbox a b ∧ k ≠ {}"
      proof (simp add: k box_eq_empty subset_box not_less, safe)
        fix i :: 'a
        assume i: "i ∈ Basis"
        with f have "f i = (a, c) ∨ f i = (c, d) ∨ f i = (d, b)"
          by (auto simp: PiE_iff)
        with i ord[of i]
        show "a ∙ i ≤ fst (f i) ∙ i" "snd (f i) ∙ i ≤ b ∙ i" "fst (f i) ∙ i ≤ snd (f i) ∙ i"
          by auto
      qed
      then show "k ≠ {}" "k ⊆ cbox a b"
        by auto
      {
        fix l
        assume "l ∈ p"
        then obtain g where g: "g ∈ Basis →E {(a, c), (c, d), (d, b)}" and l: "l = ?B g"
          by (auto simp: p_def)
        assume "l ≠ k"
        have "∃i∈Basis. f i ≠ g i"
        proof (rule ccontr)
          assume "¬ ?thesis"
          with f g have "f = g"
            by (auto simp: PiE_iff extensional_def fun_eq_iff)
          with ‹l ≠ k› show False
            by (simp add: l k)
        qed
        then obtain i where *: "i ∈ Basis" "f i ≠ g i" ..
        then have "f i = (a, c) ∨ f i = (c, d) ∨ f i = (d, b)"
                  "g i = (a, c) ∨ g i = (c, d) ∨ g i = (d, b)"
          using f g by (auto simp: PiE_iff)
        with * ord[of i] show "interior l ∩ interior k = {}"
          by (auto simp add: l k disjoint_interval intro!: bexI[of _ i])
      }
      note ‹k ⊆ cbox a b›
    }
    moreover
    {
      fix x assume x: "x ∈ cbox a b"
      have "∀i∈Basis. ∃l. x ∙ i ∈ {fst l ∙ i .. snd l ∙ i} ∧ l ∈ {(a, c), (c, d), (d, b)}"
      proof
        fix i :: 'a
        assume "i ∈ Basis"
        with x ord[of i]
        have "(a ∙ i ≤ x ∙ i ∧ x ∙ i ≤ c ∙ i) ∨ (c ∙ i ≤ x ∙ i ∧ x ∙ i ≤ d ∙ i) ∨
            (d ∙ i ≤ x ∙ i ∧ x ∙ i ≤ b ∙ i)"
          by (auto simp: cbox_def)
        then show "∃l. x ∙ i ∈ {fst l ∙ i .. snd l ∙ i} ∧ l ∈ {(a, c), (c, d), (d, b)}"
          by auto
      qed
      then obtain f where
        f: "∀i∈Basis. x ∙ i ∈ {fst (f i) ∙ i..snd (f i) ∙ i} ∧ f i ∈ {(a, c), (c, d), (d, b)}"
        unfolding bchoice_iff ..
      moreover from f have "restrict f Basis ∈ Basis →E {(a, c), (c, d), (d, b)}"
        by auto
      moreover from f have "x ∈ ?B (restrict f Basis)"
        by (auto simp: mem_box)
      ultimately have "∃k∈p. x ∈ k"
        unfolding p_def by blast
    }
    ultimately show "⋃p = cbox a b"
      by auto
  qed
qed

proposition partial_division_extend_interval:
  assumes "p division_of (⋃p)" "(⋃p) ⊆ cbox a b"
  obtains q where "p ⊆ q" "q division_of cbox a (b::'a::euclidean_space)"
proof (cases "p = {}")
  case True
  obtain q where "q division_of (cbox a b)"
    by (rule elementary_interval)
  then show ?thesis
    using True that by blast
next
  case False
  note p = division_ofD[OF assms(1)]
  have div_cbox: "∀k∈p. ∃q. q division_of cbox a b ∧ k ∈ q"
  proof
    fix k
    assume kp: "k ∈ p"
    obtain c d where k: "k = cbox c d"
      using p(4)[OF kp] by blast
    have *: "cbox c d ⊆ cbox a b" "cbox c d ≠ {}"
      using p(2,3)[OF kp, unfolded k] using assms(2)
      by (blast intro: order.trans)+
    obtain q where "q division_of cbox a b" "cbox c d ∈ q"
      by (rule partial_division_extend_1[OF *])
    then show "∃q. q division_of cbox a b ∧ k ∈ q"
      unfolding k by auto
  qed
  obtain q where q: "⋀x. x ∈ p ⟹ q x division_of cbox a b" "⋀x. x ∈ p ⟹ x ∈ q x"
    using bchoice[OF div_cbox] by blast
  have "q x division_of ⋃q x" if x: "x ∈ p" for x
    apply (rule division_ofI)
    using division_ofD[OF q(1)[OF x]] by auto
  then have di: "⋀x. x ∈ p ⟹ ∃d. d division_of ⋃(q x - {x})"
    by (meson Diff_subset division_of_subset)
  have "∃d. d division_of ⋂((λi. ⋃(q i - {i})) ` p)"
    apply (rule elementary_Inter [OF finite_imageI[OF p(1)]])
    apply (auto dest: di simp: False elementary_Inter [OF finite_imageI[OF p(1)]])
    done
  then obtain d where d: "d division_of ⋂((λi. ⋃(q i - {i})) ` p)" ..
  have "d ∪ p division_of cbox a b"
  proof -
    have te: "⋀S f T. S ≠ {} ⟹ ∀i∈S. f i ∪ i = T ⟹ T = ⋂(f ` S) ∪ ⋃S" by auto
    have cbox_eq: "cbox a b = ⋂((λi. ⋃(q i - {i})) ` p) ∪ ⋃p"
    proof (rule te[OF False], clarify)
      fix i
      assume i: "i ∈ p"
      show "⋃(q i - {i}) ∪ i = cbox a b"
        using division_ofD(6)[OF q(1)[OF i]] using q(2)[OF i] by auto
    qed
    { fix K
      assume K: "K ∈ p"
      note qk=division_ofD[OF q(1)[OF K]]
      have *: "⋀u T S. T ∩ S = {} ⟹ u ⊆ S ⟹ u ∩ T = {}"
        by auto
      have "interior (⋂i∈p. ⋃(q i - {i})) ∩ interior K = {}"
      proof (rule *[OF Int_interior_Union_intervals])
        show "⋀T. T∈q K - {K} ⟹ interior K ∩ interior T = {}"
          using qk(5) using q(2)[OF K] by auto
        show "interior (⋂i∈p. ⋃(q i - {i})) ⊆ interior (⋃(q K - {K}))"
          apply (rule interior_mono)+
          using K by auto
      qed (use qk in auto)} note [simp] = this
    show "d ∪ p division_of (cbox a b)"
      unfolding cbox_eq
      apply (rule division_disjoint_union[OF d assms(1)])
      apply (rule Int_interior_Union_intervals)
      apply (rule p open_interior ballI)+
      apply simp_all
      done
  qed
  then show ?thesis
    by (meson Un_upper2 that)
qed

lemma elementary_bounded[dest]:
  fixes S :: "'a::euclidean_space set"
  shows "p division_of S ⟹ bounded S"
  unfolding division_of_def by (metis bounded_Union bounded_cbox)

lemma elementary_subset_cbox:
  "p division_of S ⟹ ∃a b. S ⊆ cbox a (b::'a::euclidean_space)"
  by (meson elementary_bounded bounded_subset_cbox)

lemma division_union_intervals_exists:
  fixes a b :: "'a::euclidean_space"
  assumes "cbox a b ≠ {}"
  obtains p where "(insert (cbox a b) p) division_of (cbox a b ∪ cbox c d)"
proof (cases "cbox c d = {}")
  case True
  with assms that show ?thesis by force
next
  case False
  show ?thesis
  proof (cases "cbox a b ∩ cbox c d = {}")
    case True
    then show ?thesis
      by (metis that False assms division_disjoint_union division_of_self insert_is_Un interior_Int interior_empty)
  next
    case False
    obtain u v where uv: "cbox a b ∩ cbox c d = cbox u v"
      unfolding Int_interval by auto
    have uv_sub: "cbox u v ⊆ cbox c d" using uv by auto
    obtain p where pd: "p division_of cbox c d" and "cbox u v ∈ p"
      by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]])
    note p = this division_ofD[OF pd]
    have "interior (cbox a b ∩ ⋃(p - {cbox u v})) = interior(cbox u v ∩ ⋃(p - {cbox u v}))"
      apply (rule arg_cong[of _ _ interior])
      using p(8) uv by auto
    also have "… = {}"
      unfolding interior_Int
      apply (rule Int_interior_Union_intervals)
      using p(6) p(7)[OF p(2)] ‹finite p›
      apply auto
      done
    finally have [simp]: "interior (cbox a b) ∩ interior (⋃(p - {cbox u v})) = {}" by simp
    have cbe: "cbox a b ∪ cbox c d = cbox a b ∪ ⋃(p - {cbox u v})"
      using p(8) unfolding uv[symmetric] by auto
    have "insert (cbox a b) (p - {cbox u v}) division_of cbox a b ∪ ⋃(p - {cbox u v})"
    proof -
      have "{cbox a b} division_of cbox a b"
        by (simp add: assms division_of_self)
      then show "insert (cbox a b) (p - {cbox u v}) division_of cbox a b ∪ ⋃(p - {cbox u v})"
        by (metis (no_types) Diff_subset ‹interior (cbox a b) ∩ interior (⋃(p - {cbox u v})) = {}› division_disjoint_union division_of_subset insert_is_Un p(1) p(8))
    qed
    with that[of "p - {cbox u v}"] show ?thesis by (simp add: cbe)
  qed
qed

lemma division_of_Union:
  assumes "finite f"
    and "⋀p. p ∈ f ⟹ p division_of (⋃p)"
    and "⋀k1 k2. k1 ∈ ⋃f ⟹ k2 ∈ ⋃f ⟹ k1 ≠ k2 ⟹ interior k1 ∩ interior k2 = {}"
  shows "⋃f division_of ⋃⋃f"
  using assms  by (auto intro!: division_ofI)

lemma elementary_union_interval:
  fixes a b :: "'a::euclidean_space"
  assumes "p division_of ⋃p"
  obtains q where "q division_of (cbox a b ∪ ⋃p)"
proof (cases "p = {} ∨ cbox a b = {}")
  case True
  obtain p where "p division_of (cbox a b)"
    by (rule elementary_interval)
  then show thesis
    using True assms that by auto
next
  case False
  then have "p ≠ {}" "cbox a b ≠ {}"
    by auto
  note pdiv = division_ofD[OF assms]
  show ?thesis
  proof (cases "interior (cbox a b) = {}")
    case True
    show ?thesis
      apply (rule that [of "insert (cbox a b) p", OF division_ofI])
      using pdiv(1-4) True False apply auto
       apply (metis IntI equals0D pdiv(5))
      by (metis disjoint_iff_not_equal pdiv(5))
  next
    case False  
    have "∀K∈p. ∃q. (insert (cbox a b) q) division_of (cbox a b ∪ K)"
    proof
      fix K
      assume kp: "K ∈ p"
      from pdiv(4)[OF kp] obtain c d where "K = cbox c d" by blast
      then show "∃q. (insert (cbox a b) q) division_of (cbox a b ∪ K)"
        by (meson ‹cbox a b ≠ {}› division_union_intervals_exists)
    qed
    from bchoice[OF this] obtain q where "∀x∈p. insert (cbox a b) (q x) division_of (cbox a b) ∪ x" ..
    note q = division_ofD[OF this[rule_format]]
    let ?D = "⋃{insert (cbox a b) (q K) | K. K ∈ p}"
    show thesis
    proof (rule that[OF division_ofI])
      have *: "{insert (cbox a b) (q K) |K. K ∈ p} = (λK. insert (cbox a b) (q K)) ` p"
        by auto
      show "finite ?D"
        using "*" pdiv(1) q(1) by auto
      have "⋃?D = (⋃x∈p. ⋃insert (cbox a b) (q x))"
        by auto
      also have "... = ⋃{cbox a b ∪ t |t. t ∈ p}"
        using q(6) by auto
      also have "... = cbox a b ∪ ⋃p"
        using ‹p ≠ {}› by auto
      finally show "⋃?D = cbox a b ∪ ⋃p" .
      show "K ⊆ cbox a b ∪ ⋃p" "K ≠ {}" if "K ∈ ?D" for K
        using q that by blast+
      show "∃a b. K = cbox a b" if "K ∈ ?D" for K
        using q(4) that by auto
    next
      fix K' K
      assume K: "K ∈ ?D" and K': "K' ∈ ?D" "K ≠ K'"
      obtain x where x: "K ∈ insert (cbox a b) (q x)" "x∈p"
        using K by auto
      obtain x' where x': "K'∈insert (cbox a b) (q x')" "x'∈p"
        using K' by auto
      show "interior K ∩ interior K' = {}"
      proof (cases "x = x' ∨ K  = cbox a b ∨ K' = cbox a b")
        case True
        then show ?thesis
          using True K' q(5) x' x by auto
      next
        case False
        then have as': "K ≠ cbox a b" "K' ≠ cbox a b"
          by auto
        obtain c d where K: "K = cbox c d"
          using q(4) x by blast
        have "interior K ∩ interior (cbox a b) = {}"
          using as' K'(2) q(5) x by blast
        then have "interior K ⊆ interior x"
          by (metis ‹interior (cbox a b) ≠ {}› K q(2) x interior_subset_union_intervals)
        moreover
        obtain c d where c_d: "K' = cbox c d"
          using q(4)[OF x'(2,1)] by blast
        have "interior K' ∩ interior (cbox a b) = {}"
          using as'(2) q(5) x' by blast
        then have "interior K' ⊆ interior x'"
          by (metis ‹interior (cbox a b) ≠ {}› c_d interior_subset_union_intervals q(2) x'(1) x'(2))
        moreover have "interior x ∩ interior x' = {}"
          by (meson False assms division_ofD(5) x'(2) x(2))
        ultimately show ?thesis
          using ‹interior K ⊆ interior x› ‹interior K' ⊆ interior x'› by auto
      qed
    qed
  qed
qed



lemma elementary_unions_intervals:
  assumes fin: "finite f"
    and "⋀s. s ∈ f ⟹ ∃a b. s = cbox a (b::'a::euclidean_space)"
  obtains p where "p division_of (⋃f)"
proof -
  have "∃p. p division_of (⋃f)"
  proof (induct_tac f rule:finite_subset_induct)
    show "∃p. p division_of ⋃{}" using elementary_empty by auto
  next
    fix x F
    assume as: "finite F" "x ∉ F" "∃p. p division_of ⋃F" "x∈f"
    from this(3) obtain p where p: "p division_of ⋃F" ..
    from assms(2)[OF as(4)] obtain a b where x: "x = cbox a b" by blast
    have *: "⋃F = ⋃p"
      using division_ofD[OF p] by auto
    show "∃p. p division_of ⋃insert x F"
      using elementary_union_interval[OF p[unfolded *], of a b]
      unfolding Union_insert x * by metis
  qed (insert assms, auto)
  then show ?thesis
    using that by auto
qed

lemma elementary_union:
  fixes S T :: "'a::euclidean_space set"
  assumes "ps division_of S" "pt division_of T"
  obtains p where "p division_of (S ∪ T)"
proof -
  have *: "S ∪ T = ⋃ps ∪ ⋃pt"
    using assms unfolding division_of_def by auto
  show ?thesis
    apply (rule elementary_unions_intervals[of "ps ∪ pt"])
    using assms apply auto
    by (simp add: * that)
qed

lemma partial_division_extend:
  fixes T :: "'a::euclidean_space set"
  assumes "p division_of S"
    and "q division_of T"
    and "S ⊆ T"
  obtains r where "p ⊆ r" and "r division_of T"
proof -
  note divp = division_ofD[OF assms(1)] and divq = division_ofD[OF assms(2)]
  obtain a b where ab: "T ⊆ cbox a b"
    using elementary_subset_cbox[OF assms(2)] by auto
  obtain r1 where "p ⊆ r1" "r1 division_of (cbox a b)"
    using assms
    by (metis ab dual_order.trans partial_division_extend_interval divp(6))
  note r1 = this division_ofD[OF this(2)]
  obtain p' where "p' division_of ⋃(r1 - p)"
    apply (rule elementary_unions_intervals[of "r1 - p"])
    using r1(3,6)
      apply auto
    done
  then obtain r2 where r2: "r2 division_of (⋃(r1 - p)) ∩ (⋃q)"
    by (metis assms(2) divq(6) elementary_Int)
  {
    fix x
    assume x: "x ∈ T" "x ∉ S"
    then obtain R where r: "R ∈ r1" "x ∈ R"
      unfolding r1 using ab
      by (meson division_contains r1(2) subsetCE)
    moreover have "R ∉ p"
    proof
      assume "R ∈ p"
      then have "x ∈ S" using divp(2) r by auto
      then show False using x by auto
    qed
    ultimately have "x∈⋃(r1 - p)" by auto
  }
  then have Teq: "T = ⋃p ∪ (⋃(r1 - p) ∩ ⋃q)"
    unfolding divp divq using assms(3) by auto
  have "interior S ∩ interior (⋃(r1-p)) = {}"
  proof (rule Int_interior_Union_intervals)
    have *: "⋀S. (⋀x. x ∈ S ⟹ False) ⟹ S = {}"
      by auto
    show "interior S ∩ interior m = {}" if "m ∈ r1 - p" for m 
    proof -
      have "interior m ∩ interior (⋃p) = {}"
      proof (rule Int_interior_Union_intervals)
        show "⋀T. T∈p ⟹ interior m ∩ interior T = {}"
          by (metis DiffD1 DiffD2 that r1(1) r1(7) set_rev_mp)
      qed (use divp in auto)
      then show "interior S ∩ interior m = {}"
        unfolding divp by auto
    qed 
  qed (use r1 in auto)
  then have "interior S ∩ interior (⋃(r1-p) ∩ (⋃q)) = {}"
    using interior_subset by auto
  then have div: "p ∪ r2 division_of ⋃p ∪ ⋃(r1 - p) ∩ ⋃q"
    by (simp add: assms(1) division_disjoint_union divp(6) r2)
  show ?thesis
    apply (rule that[of "p ∪ r2"])
     apply (auto simp: div Teq)
    done
qed


lemma division_split:
  fixes a :: "'a::euclidean_space"
  assumes "p division_of (cbox a b)"
    and k: "k∈Basis"
  shows "{l ∩ {x. x∙k ≤ c} | l. l ∈ p ∧ l ∩ {x. x∙k ≤ c} ≠ {}} division_of(cbox a b ∩ {x. x∙k ≤ c})"
      (is "?p1 division_of ?I1")
    and "{l ∩ {x. x∙k ≥ c} | l. l ∈ p ∧ l ∩ {x. x∙k ≥ c} ≠ {}} division_of (cbox a b ∩ {x. x∙k ≥ c})"
      (is "?p2 division_of ?I2")
proof (rule_tac[!] division_ofI)
  note p = division_ofD[OF assms(1)]
  show "finite ?p1" "finite ?p2"
    using p(1) by auto
  show "⋃?p1 = ?I1" "⋃?p2 = ?I2"
    unfolding p(6)[symmetric] by auto
  {
    fix K
    assume "K ∈ ?p1"
    then obtain l where l: "K = l ∩ {x. x ∙ k ≤ c}" "l ∈ p" "l ∩ {x. x ∙ k ≤ c} ≠ {}"
      by blast
    obtain u v where uv: "l = cbox u v"
      using assms(1) l(2) by blast
    show "K ⊆ ?I1"
      using l p(2) uv by force
    show  "K ≠ {}"
      by (simp add: l)
    show  "∃a b. K = cbox a b"
      apply (simp add: l uv p(2-3)[OF l(2)])
      apply (subst interval_split[OF k])
      apply (auto intro: order.trans)
      done
    fix K'
    assume "K' ∈ ?p1"
    then obtain l' where l': "K' = l' ∩ {x. x ∙ k ≤ c}" "l' ∈ p" "l' ∩ {x. x ∙ k ≤ c} ≠ {}"
      by blast
    assume "K ≠ K'"
    then show "interior K ∩ interior K' = {}"
      unfolding l l' using p(5)[OF l(2) l'(2)] by auto
  }
  {
    fix K
    assume "K ∈ ?p2"
    then obtain l where l: "K = l ∩ {x. c ≤ x ∙ k}" "l ∈ p" "l ∩ {x. c ≤ x ∙ k} ≠ {}"
      by blast
    obtain u v where uv: "l = cbox u v"
      using l(2) p(4) by blast
    show "K ⊆ ?I2"
      using l p(2) uv by force
    show  "K ≠ {}"
      by (simp add: l)
    show  "∃a b. K = cbox a b"
      apply (simp add: l uv p(2-3)[OF l(2)])
      apply (subst interval_split[OF k])
      apply (auto intro: order.trans)
      done
    fix K'
    assume "K' ∈ ?p2"
    then obtain l' where l': "K' = l' ∩ {x. c ≤ x ∙ k}" "l' ∈ p" "l' ∩ {x. c ≤ x ∙ k} ≠ {}"
      by blast
    assume "K ≠ K'"
    then show "interior K ∩ interior K' = {}"
      unfolding l l' using p(5)[OF l(2) l'(2)] by auto
  }
qed

subsection ‹Tagged (partial) divisions.›

definition tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40)
  where "s tagged_partial_division_of i ⟷
    finite s ∧
    (∀x K. (x, K) ∈ s ⟶ x ∈ K ∧ K ⊆ i ∧ (∃a b. K = cbox a b)) ∧
    (∀x1 K1 x2 K2. (x1, K1) ∈ s ∧ (x2, K2) ∈ s ∧ (x1, K1) ≠ (x2, K2) ⟶
      interior K1 ∩ interior K2 = {})"

lemma tagged_partial_division_ofD[dest]:
  assumes "s tagged_partial_division_of i"
  shows "finite s"
    and "⋀x K. (x,K) ∈ s ⟹ x ∈ K"
    and "⋀x K. (x,K) ∈ s ⟹ K ⊆ i"
    and "⋀x K. (x,K) ∈ s ⟹ ∃a b. K = cbox a b"
    and "⋀x1 K1 x2 K2. (x1,K1) ∈ s ⟹
      (x2, K2) ∈ s ⟹ (x1, K1) ≠ (x2, K2) ⟹ interior K1 ∩ interior K2 = {}"
  using assms unfolding tagged_partial_division_of_def by blast+

definition tagged_division_of (infixr "tagged'_division'_of" 40)
  where "s tagged_division_of i ⟷ s tagged_partial_division_of i ∧ (⋃{K. ∃x. (x,K) ∈ s} = i)"

lemma tagged_division_of_finite: "s tagged_division_of i ⟹ finite s"
  unfolding tagged_division_of_def tagged_partial_division_of_def by auto

lemma tagged_division_of:
  "s tagged_division_of i ⟷
    finite s ∧
    (∀x K. (x, K) ∈ s ⟶ x ∈ K ∧ K ⊆ i ∧ (∃a b. K = cbox a b)) ∧
    (∀x1 K1 x2 K2. (x1, K1) ∈ s ∧ (x2, K2) ∈ s ∧ (x1, K1) ≠ (x2, K2) ⟶
      interior K1 ∩ interior K2 = {}) ∧
    (⋃{K. ∃x. (x,K) ∈ s} = i)"
  unfolding tagged_division_of_def tagged_partial_division_of_def by auto

lemma tagged_division_ofI:
  assumes "finite s"
    and "⋀x K. (x,K) ∈ s ⟹ x ∈ K"
    and "⋀x K. (x,K) ∈ s ⟹ K ⊆ i"
    and "⋀x K. (x,K) ∈ s ⟹ ∃a b. K = cbox a b"
    and "⋀x1 K1 x2 K2. (x1,K1) ∈ s ⟹ (x2, K2) ∈ s ⟹ (x1, K1) ≠ (x2, K2) ⟹
      interior K1 ∩ interior K2 = {}"
    and "(⋃{K. ∃x. (x,K) ∈ s} = i)"
  shows "s tagged_division_of i"
  unfolding tagged_division_of
  using assms  by fastforce

lemma tagged_division_ofD[dest]:  (*FIXME USE A LOCALE*)
  assumes "s tagged_division_of i"
  shows "finite s"
    and "⋀x K. (x,K) ∈ s ⟹ x ∈ K"
    and "⋀x K. (x,K) ∈ s ⟹ K ⊆ i"
    and "⋀x K. (x,K) ∈ s ⟹ ∃a b. K = cbox a b"
    and "⋀x1 K1 x2 K2. (x1, K1) ∈ s ⟹ (x2, K2) ∈ s ⟹ (x1, K1) ≠ (x2, K2) ⟹
      interior K1 ∩ interior K2 = {}"
    and "(⋃{K. ∃x. (x,K) ∈ s} = i)"
  using assms unfolding tagged_division_of by blast+

lemma division_of_tagged_division:
  assumes "s tagged_division_of i"
  shows "(snd ` s) division_of i"
proof (rule division_ofI)
  note assm = tagged_division_ofD[OF assms]
  show "⋃(snd ` s) = i" "finite (snd ` s)"
    using assm by auto
  fix k
  assume k: "k ∈ snd ` s"
  then obtain xk where xk: "(xk, k) ∈ s"
    by auto
  then show "k ⊆ i" "k ≠ {}" "∃a b. k = cbox a b"
    using assm by fastforce+
  fix k'
  assume k': "k' ∈ snd ` s" "k ≠ k'"
  from this(1) obtain xk' where xk': "(xk', k') ∈ s"
    by auto
  then show "interior k ∩ interior k' = {}"
    using assm(5) k'(2) xk by blast
qed

lemma partial_division_of_tagged_division:
  assumes "s tagged_partial_division_of i"
  shows "(snd ` s) division_of ⋃(snd ` s)"
proof (rule division_ofI)
  note assm = tagged_partial_division_ofD[OF assms]
  show "finite (snd ` s)" "⋃(snd ` s) = ⋃(snd ` s)"
    using assm by auto
  fix k
  assume k: "k ∈ snd ` s"
  then obtain xk where xk: "(xk, k) ∈ s"
    by auto
  then show "k ≠ {}" "∃a b. k = cbox a b" "k ⊆ ⋃(snd ` s)"
    using assm by auto
  fix k'
  assume k': "k' ∈ snd ` s" "k ≠ k'"
  from this(1) obtain xk' where xk': "(xk', k') ∈ s"
    by auto
  then show "interior k ∩ interior k' = {}"
    using assm(5) k'(2) xk by auto
qed

lemma tagged_partial_division_subset:
  assumes "s tagged_partial_division_of i"
    and "t ⊆ s"
  shows "t tagged_partial_division_of i"
  using assms finite_subset[OF assms(2)]
  unfolding tagged_partial_division_of_def
  by blast

lemma tag_in_interval: "p tagged_division_of i ⟹ (x, k) ∈ p ⟹ x ∈ i"
  by auto

lemma tagged_division_of_empty: "{} tagged_division_of {}"
  unfolding tagged_division_of by auto

lemma tagged_partial_division_of_trivial[simp]: "p tagged_partial_division_of {} ⟷ p = {}"
  unfolding tagged_partial_division_of_def by auto

lemma tagged_division_of_trivial[simp]: "p tagged_division_of {} ⟷ p = {}"
  unfolding tagged_division_of by auto

lemma tagged_division_of_self: "x ∈ cbox a b ⟹ {(x,cbox a b)} tagged_division_of (cbox a b)"
  by (rule tagged_division_ofI) auto

lemma tagged_division_of_self_real: "x ∈ {a .. b::real} ⟹ {(x,{a .. b})} tagged_division_of {a .. b}"
  unfolding box_real[symmetric]
  by (rule tagged_division_of_self)

lemma tagged_division_Un:
  assumes "p1 tagged_division_of s1"
    and "p2 tagged_division_of s2"
    and "interior s1 ∩ interior s2 = {}"
  shows "(p1 ∪ p2) tagged_division_of (s1 ∪ s2)"
proof (rule tagged_division_ofI)
  note p1 = tagged_division_ofD[OF assms(1)]
  note p2 = tagged_division_ofD[OF assms(2)]
  show "finite (p1 ∪ p2)"
    using p1(1) p2(1) by auto
  show "⋃{k. ∃x. (x, k) ∈ p1 ∪ p2} = s1 ∪ s2"
    using p1(6) p2(6) by blast
  fix x k
  assume xk: "(x, k) ∈ p1 ∪ p2"
  show "x ∈ k" "∃a b. k = cbox a b"
    using xk p1(2,4) p2(2,4) by auto
  show "k ⊆ s1 ∪ s2"
    using xk p1(3) p2(3) by blast
  fix x' k'
  assume xk': "(x', k') ∈ p1 ∪ p2" "(x, k) ≠ (x', k')"
  have *: "⋀a b. a ⊆ s1 ⟹ b ⊆ s2 ⟹ interior a ∩ interior b = {}"
    using assms(3) interior_mono by blast
  show "interior k ∩ interior k' = {}"
    apply (cases "(x, k) ∈ p1")
    apply (meson "*" UnE assms(1) assms(2) p1(5) tagged_division_ofD(3) xk'(1) xk'(2))
    by (metis "*" UnE assms(1) assms(2) inf_sup_aci(1) p2(5) tagged_division_ofD(3) xk xk'(1) xk'(2))
qed

lemma tagged_division_Union:
  assumes "finite I"
    and tag: "⋀i. i∈I ⟹ pfn i tagged_division_of i"
    and disj: "⋀i1 i2. ⟦i1 ∈ I; i2 ∈ I; i1 ≠ i2⟧ ⟹ interior(i1) ∩ interior(i2) = {}"
  shows "⋃(pfn ` I) tagged_division_of (⋃I)"
proof (rule tagged_division_ofI)
  note assm = tagged_division_ofD[OF tag]
  show "finite (⋃(pfn ` I))"
    using assms by auto
  have "⋃{k. ∃x. (x, k) ∈ ⋃(pfn ` I)} = ⋃((λi. ⋃{k. ∃x. (x, k) ∈ pfn i}) ` I)"
    by blast
  also have "… = ⋃I"
    using assm(6) by auto
  finally show "⋃{k. ∃x. (x, k) ∈ ⋃(pfn ` I)} = ⋃I" .
  fix x k
  assume xk: "(x, k) ∈ ⋃(pfn ` I)"
  then obtain i where i: "i ∈ I" "(x, k) ∈ pfn i"
    by auto
  show "x ∈ k" "∃a b. k = cbox a b" "k ⊆ ⋃I"
    using assm(2-4)[OF i] using i(1) by auto
  fix x' k'
  assume xk': "(x', k') ∈ ⋃(pfn ` I)" "(x, k) ≠ (x', k')"
  then obtain i' where i': "i' ∈ I" "(x', k') ∈ pfn i'"
    by auto
  have *: "⋀a b. i ≠ i' ⟹ a ⊆ i ⟹ b ⊆ i' ⟹ interior a ∩ interior b = {}"
    using i(1) i'(1) disj interior_mono by blast
  show "interior k ∩ interior k' = {}"
  proof (cases "i = i'")
    case True then show ?thesis 
      using assm(5) i' i xk'(2) by blast
  next
    case False then show ?thesis 
    using "*" assm(3) i' i by auto
  qed
qed

lemma tagged_partial_division_of_Union_self:
  assumes "p tagged_partial_division_of s"
  shows "p tagged_division_of (⋃(snd ` p))"
  apply (rule tagged_division_ofI)
  using tagged_partial_division_ofD[OF assms]
  apply auto
  done

lemma tagged_division_of_union_self:
  assumes "p tagged_division_of s"
  shows "p tagged_division_of (⋃(snd ` p))"
  apply (rule tagged_division_ofI)
  using tagged_division_ofD[OF assms]
  apply auto
  done

lemma tagged_division_Un_interval:
  fixes a :: "'a::euclidean_space"
  assumes "p1 tagged_division_of (cbox a b ∩ {x. x∙k ≤ (c::real)})"
    and "p2 tagged_division_of (cbox a b ∩ {x. x∙k ≥ c})"
    and k: "k ∈ Basis"
  shows "(p1 ∪ p2) tagged_division_of (cbox a b)"
proof -
  have *: "cbox a b = (cbox a b ∩ {x. x∙k ≤ c}) ∪ (cbox a b ∩ {x. x∙k ≥ c})"
    by auto
  show ?thesis
    apply (subst *)
    apply (rule tagged_division_Un[OF assms(1-2)])
    unfolding interval_split[OF k] interior_cbox
    using k
    apply (auto simp add: box_def elim!: ballE[where x=k])
    done
qed

lemma tagged_division_Un_interval_real:
  fixes a :: real
  assumes "p1 tagged_division_of ({a .. b} ∩ {x. x∙k ≤ (c::real)})"
    and "p2 tagged_division_of ({a .. b} ∩ {x. x∙k ≥ c})"
    and k: "k ∈ Basis"
  shows "(p1 ∪ p2) tagged_division_of {a .. b}"
  using assms
  unfolding box_real[symmetric]
  by (rule tagged_division_Un_interval)

lemma tagged_division_split_left_inj:
  assumes d: "d tagged_division_of i"
  and tags: "(x1, K1) ∈ d" "(x2, K2) ∈ d"
  and "K1 ≠ K2"
  and eq: "K1 ∩ {x. x ∙ k ≤ c} = K2 ∩ {x. x ∙ k ≤ c}"
    shows "interior (K1 ∩ {x. x∙k ≤ c}) = {}"
proof -
  have "interior (K1 ∩ K2) = {} ∨ (x2, K2) = (x1, K1)"
    using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
  then show ?thesis
    using eq ‹K1 ≠ K2› by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
qed

lemma tagged_division_split_right_inj:
  assumes d: "d tagged_division_of i"
  and tags: "(x1, K1) ∈ d" "(x2, K2) ∈ d"
  and "K1 ≠ K2"
  and eq: "K1 ∩ {x. x∙k ≥ c} = K2 ∩ {x. x∙k ≥ c}"
    shows "interior (K1 ∩ {x. x∙k ≥ c}) = {}"
proof -
  have "interior (K1 ∩ K2) = {} ∨ (x2, K2) = (x1, K1)"
    using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
  then show ?thesis
    using eq ‹K1 ≠ K2› by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
qed

lemma (in comm_monoid_set) over_tagged_division_lemma:
  assumes "p tagged_division_of i"
    and "⋀u v. box u v = {} ⟹ d (cbox u v) = 1"
  shows "F (λ(_, k). d k) p = F d (snd ` p)"
proof -
  have *: "(λ(_ ,k). d k) = d ∘ snd"
    by (simp add: fun_eq_iff)
  note assm = tagged_division_ofD[OF assms(1)]
  show ?thesis
    unfolding *
  proof (rule reindex_nontrivial[symmetric])
    show "finite p"
      using assm by auto
    fix x y
    assume "x∈p" "y∈p" "x≠y" "snd x = snd y"
    obtain a b where ab: "snd x = cbox a b"
      using assm(4)[of "fst x" "snd x"] ‹x∈p› by auto
    have "(fst x, snd y) ∈ p" "(fst x, snd y) ≠ y"
      using ‹x ∈ p› ‹x ≠ y› ‹snd x = snd y› [symmetric] by auto
    with ‹x∈p› ‹y∈p› have "interior (snd x) ∩ interior (snd y) = {}"
      by (intro assm(5)[of "fst x" _ "fst y"]) auto
    then have "box a b = {}"
      unfolding ‹snd x = snd y›[symmetric] ab by auto
    then have "d (cbox a b) = 1"
      using assm(2)[of "fst x" "snd x"] ‹x∈p› ab[symmetric] by (intro assms(2)) auto
    then show "d (snd x) = 1"
      unfolding ab by auto
  qed
qed


subsection ‹Functions closed on boxes: morphisms from boxes to monoids›

text ‹This auxiliary structure is used to sum up over the elements of a division. Main theorem is
  ‹operative_division›. Instances for the monoid are @{typ "'a option"}, @{typ real}, and
  @{typ bool}.›

paragraph ‹Using additivity of lifted function to encode definedness.›

definition lift_option :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a option ⇒ 'b option ⇒ 'c option"
where
  "lift_option f a' b' = Option.bind a' (λa. Option.bind b' (λb. Some (f a b)))"

lemma lift_option_simps[simp]:
  "lift_option f (Some a) (Some b) = Some (f a b)"
  "lift_option f None b' = None"
  "lift_option f a' None = None"
  by (auto simp: lift_option_def)

lemma comm_monoid_lift_option:
  assumes "comm_monoid f z"
  shows "comm_monoid (lift_option f) (Some z)"
proof -
  from assms interpret comm_monoid f z .
  show ?thesis
    by standard (auto simp: lift_option_def ac_simps split: bind_split)
qed

lemma comm_monoid_and: "comm_monoid HOL.conj True"
  by standard auto

lemma comm_monoid_set_and: "comm_monoid_set HOL.conj True"
  by (rule comm_monoid_set.intro) (fact comm_monoid_and)


paragraph ‹Misc›

lemma interval_real_split:
  "{a .. b::real} ∩ {x. x ≤ c} = {a .. min b c}"
  "{a .. b} ∩ {x. c ≤ x} = {max a c .. b}"
  apply (metis Int_atLeastAtMostL1 atMost_def)
  apply (metis Int_atLeastAtMostL2 atLeast_def)
  done

lemma bgauge_existence_lemma: "(∀x∈s. ∃d::real. 0 < d ∧ q d x) ⟷ (∀x. ∃d>0. x∈s ⟶ q d x)"
  by (meson zero_less_one)


paragraph ‹Division points›

definition "division_points (k::('a::euclidean_space) set) d =
   {(j,x). j ∈ Basis ∧ (interval_lowerbound k)∙j < x ∧ x < (interval_upperbound k)∙j ∧
     (∃i∈d. (interval_lowerbound i)∙j = x ∨ (interval_upperbound i)∙j = x)}"

lemma division_points_finite:
  fixes i :: "'a::euclidean_space set"
  assumes "d division_of i"
  shows "finite (division_points i d)"
proof -
  note assm = division_ofD[OF assms]
  let ?M = "λj. {(j,x)|x. (interval_lowerbound i)∙j < x ∧ x < (interval_upperbound i)∙j ∧
    (∃i∈d. (interval_lowerbound i)∙j = x ∨ (interval_upperbound i)∙j = x)}"
  have *: "division_points i d = ⋃(?M ` Basis)"
    unfolding division_points_def by auto
  show ?thesis
    unfolding * using assm by auto
qed

lemma division_points_subset:
  fixes a :: "'a::euclidean_space"
  assumes "d division_of (cbox a b)"
    and "∀i∈Basis. a∙i < b∙i"  "a∙k < c" "c < b∙k"
    and k: "k ∈ Basis"
  shows "division_points (cbox a b ∩ {x. x∙k ≤ c}) {l ∩ {x. x∙k ≤ c} | l . l ∈ d ∧ l ∩ {x. x∙k ≤ c} ≠ {}} ⊆
      division_points (cbox a b) d" (is ?t1)
    and "division_points (cbox a b ∩ {x. x∙k ≥ c}) {l ∩ {x. x∙k ≥ c} | l . l ∈ d ∧ ~(l ∩ {x. x∙k ≥ c} = {})} ⊆
      division_points (cbox a b) d" (is ?t2)
proof -
  note assm = division_ofD[OF assms(1)]
  have *: "∀i∈Basis. a∙i ≤ b∙i"
    "∀i∈Basis. a∙i ≤ (∑i∈Basis. (if i = k then min (b ∙ k) c else  b ∙ i) *R i) ∙ i"
    "∀i∈Basis. (∑i∈Basis. (if i = k then max (a ∙ k) c else a ∙ i) *R i) ∙ i ≤ b∙i"
    "min (b ∙ k) c = c" "max (a ∙ k) c = c"
    using assms using less_imp_le by auto
   have "∃i∈d. interval_lowerbound i ∙ x = y ∨ interval_upperbound i ∙ x = y"
     if "a ∙ x < y" "y < (if x = k then c else b ∙ x)"
        "interval_lowerbound i ∙ x = y ∨ interval_upperbound i ∙ x = y"
        "i = l ∩ {x. x ∙ k ≤ c}" "l ∈ d" "l ∩ {x. x ∙ k ≤ c} ≠ {}"
        "x ∈ Basis" for i l x y
  proof -
    obtain u v where l: "l = cbox u v"
      using ‹l ∈ d› assms(1) by blast
    have *: "∀i∈Basis. u ∙ i ≤ (∑i∈Basis. (if i = k then min (v ∙ k) c else v ∙ i) *R i) ∙ i"
      using that(6) unfolding l interval_split[OF k] box_ne_empty that .
    have **: "∀i∈Basis. u∙i ≤ v∙i"
      using l using that(6) unfolding box_ne_empty[symmetric] by auto
    show ?thesis
      apply (rule bexI[OF _ ‹l ∈ d›])
      using that(1-3,5) ‹x ∈ Basis›
      unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] that
      apply (auto split: if_split_asm)
      done
  qed
  moreover have "⋀x y. ⟦y < (if x = k then c else b ∙ x)⟧ ⟹ y < b ∙ x"
    using ‹c < b∙k› by (auto split: if_split_asm)
  ultimately show ?t1 
    unfolding division_points_def interval_split[OF k, of a b]
    unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
    unfolding * by force
  have "⋀x y i l. (if x = k then c else a ∙ x) < y ⟹ a ∙ x < y"
    using ‹a∙k < c› by (auto split: if_split_asm)
  moreover have "∃i∈d. interval_lowerbound i ∙ x = y ∨
                       interval_upperbound i ∙ x = y"
    if "(if x = k then c else a ∙ x) < y" "y < b ∙ x"
      "interval_lowerbound i ∙ x = y ∨ interval_upperbound i ∙ x = y"
      "i = l ∩ {x. c ≤ x ∙ k}" "l ∈ d" "l ∩ {x. c ≤ x ∙ k} ≠ {}"
      "x ∈ Basis" for x y i l
  proof -
    obtain u v where l: "l = cbox u v"
      using ‹l ∈ d› assm(4) by blast
    have *: "∀i∈Basis. (∑i∈Basis. (if i = k then max (u ∙ k) c else u ∙ i) *R i) ∙ i ≤ v ∙ i"
      using that(6) unfolding l interval_split[OF k] box_ne_empty that .
    have **: "∀i∈Basis. u∙i ≤ v∙i"
      using l using that(6) unfolding box_ne_empty[symmetric] by auto
    show "∃i∈d. interval_lowerbound i ∙ x = y ∨ interval_upperbound i ∙ x = y"
      apply (rule bexI[OF _ ‹l ∈ d›])
      using that(1-3,5) ‹x ∈ Basis›
      unfolding l interval_bounds[OF **] interval_bounds[OF *] interval_split[OF k] that
      apply (auto split: if_split_asm)
      done
  qed
  ultimately show ?t2
    unfolding division_points_def interval_split[OF k, of a b]
    unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
    unfolding *
    by force
qed

lemma division_points_psubset:
  fixes a :: "'a::euclidean_space"
  assumes d: "d division_of (cbox a b)"
      and altb: "∀i∈Basis. a∙i < b∙i"  "a∙k < c" "c < b∙k"
      and "l ∈ d"
      and disj: "interval_lowerbound l∙k = c ∨ interval_upperbound l∙k = c"
      and k: "k ∈ Basis"
  shows "division_points (cbox a b ∩ {x. x∙k ≤ c}) {l ∩ {x. x∙k ≤ c} | l. l∈d ∧ l ∩ {x. x∙k ≤ c} ≠ {}} ⊂
         division_points (cbox a b) d" (is "?D1 ⊂ ?D")
    and "division_points (cbox a b ∩ {x. x∙k ≥ c}) {l ∩ {x. x∙k ≥ c} | l. l∈d ∧ l ∩ {x. x∙k ≥ c} ≠ {}} ⊂
         division_points (cbox a b) d" (is "?D2 ⊂ ?D")
proof -
  have ab: "∀i∈Basis. a∙i ≤ b∙i"
    using altb by (auto intro!:less_imp_le)
  obtain u v where l: "l = cbox u v"
    using d ‹l ∈ d› by blast
  have uv: "∀i∈Basis. u∙i ≤ v∙i" "∀i∈Basis. a∙i ≤ u∙i ∧ v∙i ≤ b∙i"
    apply (metis assms(5) box_ne_empty(1) cbox_division_memE d l)
    by (metis assms(5) box_ne_empty(1) cbox_division_memE d l subset_box(1))
  have *: "interval_upperbound (cbox a b ∩ {x. x ∙ k ≤ interval_upperbound l ∙ k}) ∙ k = interval_upperbound l ∙ k"
          "interval_upperbound (cbox a b ∩ {x. x ∙ k ≤ interval_lowerbound l ∙ k}) ∙ k = interval_lowerbound l ∙ k"
    unfolding l interval_split[OF k] interval_bounds[OF uv(1)]
    using uv[rule_format, of k] ab k
    by auto
  have "∃x. x ∈ ?D - ?D1"
    using assms(3-)
    unfolding division_points_def interval_bounds[OF ab]
    by (force simp add: *)
  moreover have "?D1 ⊆ ?D"
    by (auto simp add: assms division_points_subset)
  ultimately show "?D1 ⊂ ?D"
    by blast
  have *: "interval_lowerbound (cbox a b ∩ {x. x ∙ k ≥ interval_lowerbound l ∙ k}) ∙ k = interval_lowerbound l ∙ k"
    "interval_lowerbound (cbox a b ∩ {x. x ∙ k ≥ interval_upperbound l ∙ k}) ∙ k = interval_upperbound l ∙ k"
    unfolding l interval_split[OF k] interval_bounds[OF uv(1)]
    using uv[rule_format, of k] ab k
    by auto
  have "∃x. x ∈ ?D - ?D2"
    using assms(3-)
    unfolding division_points_def interval_bounds[OF ab]
    by (force simp add: *)
  moreover have "?D2 ⊆ ?D"
    by (auto simp add: assms division_points_subset)
  ultimately show "?D2 ⊂ ?D"
    by blast
qed

lemma division_split_left_inj:
  fixes S :: "'a::euclidean_space set"
  assumes div: "𝒟 division_of S"
    and eq: "K1 ∩ {x::'a. x∙k ≤ c} = K2 ∩ {x. x∙k ≤ c}"
    and "K1 ∈ 𝒟" "K2 ∈ 𝒟" "K1 ≠ K2"
  shows "interior (K1 ∩ {x. x∙k ≤ c}) = {}"
proof -
  have "interior K2 ∩ interior {a. a ∙ k ≤ c} = interior K1 ∩ interior {a. a ∙ k ≤ c}"
    by (metis (no_types) eq interior_Int)
  moreover have "⋀A. interior A ∩ interior K2 = {} ∨ A = K2 ∨ A ∉ 𝒟"
    by (meson div ‹K2 ∈ 𝒟› division_of_def)
  ultimately show ?thesis
    using ‹K1 ∈ 𝒟› ‹K1 ≠ K2› by auto
qed

lemma division_split_right_inj:
  fixes S :: "'a::euclidean_space set"
  assumes div: "𝒟 division_of S"
    and eq: "K1 ∩ {x::'a. x∙k ≥ c} = K2 ∩ {x. x∙k ≥ c}"
    and "K1 ∈ 𝒟" "K2 ∈ 𝒟" "K1 ≠ K2"
  shows "interior (K1 ∩ {x. x∙k ≥ c}) = {}"
proof -
  have "interior K2 ∩ interior {a. a ∙ k ≥ c} = interior K1 ∩ interior {a. a ∙ k ≥ c}"
    by (metis (no_types) eq interior_Int)
  moreover have "⋀A. interior A ∩ interior K2 = {} ∨ A = K2 ∨ A ∉ 𝒟"
    by (meson div ‹K2 ∈ 𝒟› division_of_def)
  ultimately show ?thesis
    using ‹K1 ∈ 𝒟› ‹K1 ≠ K2› by auto
qed

lemma interval_doublesplit:
  fixes a :: "'a::euclidean_space"
  assumes "k ∈ Basis"
  shows "cbox a b ∩ {x . ¦x∙k - c¦ ≤ (e::real)} =
    cbox (∑i∈Basis. (if i = k then max (a∙k) (c - e) else a∙i) *R i)
     (∑i∈Basis. (if i = k then min (b∙k) (c + e) else b∙i) *R i)"
proof -
  have *: "⋀x c e::real. ¦x - c¦ ≤ e ⟷ x ≥ c - e ∧ x ≤ c + e"
    by auto
  have **: "⋀s P Q. s ∩ {x. P x ∧ Q x} = (s ∩ {x. Q x}) ∩ {x. P x}"
    by blast
  show ?thesis
    unfolding * ** interval_split[OF assms] by (rule refl)
qed

lemma division_doublesplit:
  fixes a :: "'a::euclidean_space"
  assumes "p division_of (cbox a b)"
    and k: "k ∈ Basis"
  shows "(λl. l ∩ {x. ¦x∙k - c¦ ≤ e}) ` {l∈p. l ∩ {x. ¦x∙k - c¦ ≤ e} ≠ {}}
         division_of  (cbox a b ∩ {x. ¦x∙k - c¦ ≤ e})"
proof -
  have *: "⋀x c. ¦x - c¦ ≤ e ⟷ x ≥ c - e ∧ x ≤ c + e"
    by auto
  have **: "⋀p q p' q'. p division_of q ⟹ p = p' ⟹ q = q' ⟹ p' division_of q'"
    by auto
  note division_split(1)[OF assms, where c="c+e",unfolded interval_split[OF k]]
  note division_split(2)[OF this, where c="c-e" and k=k,OF k]
  then show ?thesis
    apply (rule **)
    subgoal
      apply (simp add: abs_diff_le_iff field_simps Collect_conj_eq setcompr_eq_image[symmetric])
      apply (rule equalityI)
      apply blast
      apply clarsimp
      apply (rule_tac x="l ∩ {x. c + e ≥ x ∙ k}" in exI)
      apply auto
      done
    by (simp add: interval_split k interval_doublesplit)
qed
              
paragraph ‹Operative›

locale operative = comm_monoid_set +
  fixes g :: "'b::euclidean_space set ⇒ 'a"
  assumes box_empty_imp: "⋀a b. box a b = {} ⟹ g (cbox a b) = 1"
    and Basis_imp: "⋀a b c k. k ∈ Basis ⟹ g (cbox a b) = g (cbox a b ∩ {x. x∙k ≤ c}) * g (cbox a b ∩ {x. x∙k ≥ c})"
begin

lemma empty [simp]:
  "g {} = 1"
proof -
  have *: "cbox One (-One) = ({}::'b set)"
    by (auto simp: box_eq_empty inner_sum_left inner_Basis sum.If_cases ex_in_conv)
  moreover have "box One (-One) = ({}::'b set)"
    using box_subset_cbox[of One "-One"] by (auto simp: *)
  ultimately show ?thesis
    using box_empty_imp [of One "-One"] by simp
qed
       
lemma division:
  "F g d = g (cbox a b)" if "d division_of (cbox a b)"
proof -
  define C where [abs_def]: "C = card (division_points (cbox a b) d)"
  then show ?thesis
  using that proof (induction C arbitrary: a b d rule: less_induct)
    case (less a b d)
    show ?case
    proof cases
      assume "box a b = {}"
      { fix k assume "k∈d"
        then obtain a' b' where k: "k = cbox a' b'"
          using division_ofD(4)[OF less.prems] by blast
        with ‹k∈d› division_ofD(2)[OF less.prems] have "cbox a' b' ⊆ cbox a b"
          by auto
        then have "box a' b' ⊆ box a b"
          unfolding subset_box by auto
        then have "g k = 1"
          using box_empty_imp [of a' b'] k by (simp add: ‹box a b = {}›) }
      then show "box a b = {} ⟹ F g d = g (cbox a b)"
        by (auto intro!: neutral simp: box_empty_imp)
    next
      assume "box a b ≠ {}"
      then have ab: "∀i∈Basis. a∙i < b∙i" and ab': "∀i∈Basis. a∙i ≤ b∙i"
        by (auto simp: box_ne_empty)
      show "F g d = g (cbox a b)"
      proof (cases "division_points (cbox a b) d = {}")
        case True
        { fix u v and j :: 'b
          assume j: "j ∈ Basis" and as: "cbox u v ∈ d"
          then have "cbox u v ≠ {}"
            using less.prems by blast
          then have uv: "∀i∈Basis. u∙i ≤ v∙i" "u∙j ≤ v∙j"
            using j unfolding box_ne_empty by auto
          have *: "⋀p r Q. ¬ j∈Basis ∨ p ∨ r ∨ (∀x∈d. Q x) ⟹ p ∨ r ∨ Q (cbox u v)"
            using as j by auto
          have "(j, u∙j) ∉ division_points (cbox a b) d"
               "(j, v∙j) ∉ division_points (cbox a b) d" using True by auto
          note this[unfolded de_Morgan_conj division_points_def mem_Collect_eq split_conv interval_bounds[OF ab'] bex_simps]
          note *[OF this(1)] *[OF this(2)] note this[unfolded interval_bounds[OF uv(1)]]
          moreover
          have "a∙j ≤ u∙j" "v∙j ≤ b∙j"
            using division_ofD(2,2,3)[OF ‹d division_of cbox a b› as]
            apply (metis j subset_box(1) uv(1))
            by (metis ‹cbox u v ⊆ cbox a b› j subset_box(1) uv(1))
          ultimately have "u∙j = a∙j ∧ v∙j = a∙j ∨ u∙j = b∙j ∧ v∙j = b∙j ∨ u∙j = a∙j ∧ v∙j = b∙j"
            unfolding not_less de_Morgan_disj using ab[rule_format,of j] uv(2) j by force }
        then have d': "∀i∈d. ∃u v. i = cbox u v ∧
          (∀j∈Basis. u∙j = a∙j ∧ v∙j = a∙j ∨ u∙j = b∙j ∧ v∙j = b∙j ∨ u∙j = a∙j ∧ v∙j = b∙j)"
          unfolding forall_in_division[OF less.prems] by blast
        have "(1/2) *R (a+b) ∈ cbox a b"
          unfolding mem_box using ab by (auto simp: inner_simps)
        note this[unfolded division_ofD(6)[OF ‹d division_of cbox a b›,symmetric] Union_iff]
        then obtain i where i: "i ∈ d" "(1 / 2) *R (a + b) ∈ i" ..
        obtain u v where uv: "i = cbox u v" 
                     "∀j∈Basis. u ∙ j = a ∙ j ∧ v ∙ j = a ∙ j ∨
                                u ∙ j = b ∙ j ∧ v ∙ j = b ∙ j ∨
                                u ∙ j = a ∙ j ∧ v ∙ j = b ∙ j"
          using d' i(1) by auto
        have "cbox a b ∈ d"
        proof -
          have "u = a" "v = b"
            unfolding euclidean_eq_iff[where 'a='b]
          proof safe
            fix j :: 'b
            assume j: "j ∈ Basis"
            note i(2)[unfolded uv mem_box,rule_format,of j]
            then show "u ∙ j = a ∙ j" and "v ∙ j = b ∙ j"
              using uv(2)[rule_format,of j] j by (auto simp: inner_simps)
          qed
          then have "i = cbox a b" using uv by auto
          then show ?thesis using i by auto
        qed
        then have deq: "d = insert (cbox a b) (d - {cbox a b})"
          by auto
        have "F g (d - {cbox a b}) = 1"
        proof (intro neutral ballI)
          fix x
          assume x: "x ∈ d - {cbox a b}"
          then have "x∈d"
            by auto note d'[rule_format,OF this]
          then obtain u v where uv: "x = cbox u v"
                      "∀j∈Basis. u ∙ j = a ∙ j ∧ v ∙ j = a ∙ j ∨
                                 u ∙ j = b ∙ j ∧ v ∙ j = b ∙ j ∨
                                 u ∙ j = a ∙ j ∧ v ∙ j = b ∙ j" 
            by blast
          have "u ≠ a ∨ v ≠ b"
            using x[unfolded uv] by auto
          then obtain j where "u∙j ≠ a∙j ∨ v∙j ≠ b∙j" and j: "j ∈ Basis"
            unfolding euclidean_eq_iff[where 'a='b] by auto
          then have "u∙j = v∙j"
            using uv(2)[rule_format,OF j] by auto
          then have "box u v = {}"
            using j unfolding box_eq_empty by (auto intro!: bexI[of _ j])
          then show "g x = 1"
            unfolding uv(1) by (rule box_empty_imp)
        qed
        then show "F g d = g (cbox a b)"
          using division_ofD[OF less.prems]
          apply (subst deq)
          apply (subst insert)
          apply auto
          done
      next
        case False
        then have "∃x. x ∈ division_points (cbox a b) d"
          by auto
        then obtain k c 
          where "k ∈ Basis" "interval_lowerbound (cbox a b) ∙ k < c"
                "c < interval_upperbound (cbox a b) ∙ k"
                "∃i∈d. interval_lowerbound i ∙ k = c ∨ interval_upperbound i ∙ k = c"
          unfolding division_points_def by auto
        then obtain j where "a ∙ k < c" "c < b ∙ k" 
              and "j ∈ d" and j: "interval_lowerbound j ∙ k = c ∨ interval_upperbound j ∙ k = c"
          by (metis division_of_trivial empty_iff interval_bounds' less.prems)
        let ?lec = "{x. x∙k ≤ c}" let ?gec = "{x. x∙k ≥ c}"
        define d1 where "d1 = {l ∩ ?lec | l. l ∈ d ∧ l ∩ ?lec ≠ {}}"
        define d2 where "d2 = {l ∩ ?gec | l. l ∈ d ∧ l ∩ ?gec ≠ {}}"
        define cb where "cb = (∑i∈Basis. (if i = k then c else b∙i) *R i)"
        define ca where "ca = (∑i∈Basis. (if i = k then c else a∙i) *R i)"
        have "division_points (cbox a b ∩ ?lec) {l ∩ ?lec |l. l ∈ d ∧ l ∩ ?lec ≠ {}} 
              ⊂ division_points (cbox a b) d"
          by (rule division_points_psubset[OF ‹d division_of cbox a b› ab ‹a ∙ k < c› ‹c < b ∙ k› ‹j ∈ d› j ‹k ∈ Basis›])
        with division_points_finite[OF ‹d division_of cbox a b›] 
        have "card
         (division_points (cbox a b ∩ ?lec) {l ∩ ?lec |l. l ∈ d ∧ l ∩ ?lec ≠ {}})
           < card (division_points (cbox a b) d)"
          by (rule psubset_card_mono)
        moreover have "division_points (cbox a b ∩ {x. c ≤ x ∙ k}) {l ∩ {x. c ≤ x ∙ k} |l. l ∈ d ∧ l ∩ {x. c ≤ x ∙ k} ≠ {}}
              ⊂ division_points (cbox a b) d"
          by (rule division_points_psubset[OF ‹d division_of cbox a b› ab ‹a ∙ k < c› ‹c < b ∙ k› ‹j ∈ d› j ‹k ∈ Basis›])
        with division_points_finite[OF ‹d division_of cbox a b›] 
        have "card (division_points (cbox a b ∩ ?gec) {l ∩ ?gec |l. l ∈ d ∧ l ∩ ?gec ≠ {}})
              < card (division_points (cbox a b) d)"
          by (rule psubset_card_mono)
        ultimately have *: "F g d1 = g (cbox a b ∩ ?lec)" "F g d2 = g (cbox a b ∩ ?gec)"
          unfolding interval_split[OF ‹k ∈ Basis›]
          apply (rule_tac[!] less.hyps)
          using division_split[OF ‹d division_of cbox a b›, where k=k and c=c] ‹k ∈ Basis›
          by (simp_all add: interval_split  d1_def d2_def division_points_finite[OF ‹d division_of cbox a b›])
        have fxk_le: "g (l ∩ ?lec) = 1" 
          if "l ∈ d" "y ∈ d" "l ∩ ?lec = y ∩ ?lec" "l ≠ y" for l y
        proof -
          obtain u v where leq: "l = cbox u v"
            using ‹l ∈ d› less.prems by auto
          have "interior (cbox u v ∩ ?lec) = {}"
            using that division_split_left_inj leq less.prems by blast
          then show ?thesis
            unfolding leq interval_split [OF ‹k ∈ Basis›]
            by (auto intro: box_empty_imp)
        qed
        have fxk_ge: "g (l ∩ {x. x ∙ k ≥ c}) = 1"
          if "l ∈ d" "y ∈ d" "l ∩ ?gec = y ∩ ?gec" "l ≠ y" for l y
        proof -
          obtain u v where leq: "l = cbox u v"
            using ‹l ∈ d› less.prems by auto
          have "interior (cbox u v ∩ ?gec) = {}"
            using that division_split_right_inj leq less.prems by blast
          then show ?thesis
            unfolding leq interval_split[OF ‹k ∈ Basis›]
            by (auto intro: box_empty_imp)
        qed
        have d1_alt: "d1 = (λl. l ∩ ?lec) ` {l ∈ d. l ∩ ?lec ≠ {}}"
          using d1_def by auto
        have d2_alt: "d2 = (λl. l ∩ ?gec) ` {l ∈ d. l ∩ ?gec ≠ {}}"
          using d2_def by auto
        have "g (cbox a b) = F g d1 * F g d2" (is "_ = ?prev")
          unfolding * using ‹k ∈ Basis›
          by (auto dest: Basis_imp)
        also have "F g d1 = F (λl. g (l ∩ ?lec)) d"
          unfolding d1_alt using division_of_finite[OF less.prems] fxk_le
          by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left)
        also have "F g d2 = F (λl. g (l ∩ ?gec)) d"
          unfolding d2_alt using division_of_finite[OF less.prems] fxk_ge
          by (subst reindex_nontrivial) (auto intro!: mono_neutral_cong_left)
        also have *: "∀x∈d. g x = g (x ∩ ?lec) * g (x ∩ ?gec)"
          unfolding forall_in_division[OF ‹d division_of cbox a b›]
          using ‹k ∈ Basis›
          by (auto dest: Basis_imp)
        have "F (λl. g (l ∩ ?lec)) d * F (λl. g (l ∩ ?gec)) d = F g d"
          using * by (simp add: distrib)
        finally show ?thesis by auto
      qed
    qed
  qed
qed

lemma tagged_division:
  assumes "d tagged_division_of (cbox a b)"
  shows "F (λ(_, l). g l) d = g (cbox a b)"
proof -
  have "F (λ(_, k). g k) d = F g (snd ` d)"
    using assms box_empty_imp by (rule over_tagged_division_lemma)
  then show ?thesis
    unfolding assms [THEN division_of_tagged_division, THEN division] .
  qed

end

locale operative_real = comm_monoid_set +
  fixes g :: "real set ⇒ 'a"
  assumes neutral: "b ≤ a ⟹ g {a..b} = 1"
  assumes coalesce_less: "a < c ⟹ c < b ⟹ g {a..c} * g {c..b} = g {a..b}"
begin

sublocale operative where g = g
  rewrites "box = (greaterThanLessThan :: real ⇒ _)"
    and "cbox = (atLeastAtMost :: real ⇒ _)"
    and "⋀x::real. x ∈ Basis ⟷ x = 1"
proof -
  show "operative f z g"
  proof
    show "g (cbox a b) = 1" if "box a b = {}" for a b
      using that by (simp add: neutral)
    show "g (cbox a b) = g (cbox a b ∩ {x. x ∙ k ≤ c}) * g (cbox a b ∩ {x. c ≤ x ∙ k})"
      if "k ∈ Basis" for a b c k
    proof -
      from that have [simp]: "k = 1"
        by simp
      from neutral [of 0 1] neutral [of a a for a] coalesce_less
  have [simp]: "g {} = 1" "⋀a. g {a} = 1"
    "⋀a b c. a < c ⟹ c < b ⟹ g {a..c} * g {c..b} = g {a..b}"
    by auto
      have "g {a..b} = g {a..min b c} * g {max a c..b}"
    by (auto simp: min_def max_def le_less)
      then show "g (cbox a b) = g (cbox a b ∩ {x. x ∙ k ≤ c}) * g (cbox a b ∩ {x. c ≤ x ∙ k})"
        by (simp add: atMost_def [symmetric] atLeast_def [symmetric])
qed
  qed
  show "box = (greaterThanLessThan :: real ⇒ _)"
    and "cbox = (atLeastAtMost :: real ⇒ _)"
    and "⋀x::real. x ∈ Basis ⟷ x = 1"
    by (simp_all add: fun_eq_iff)
qed

lemma coalesce_less_eq:
  "g {a..c} * g {c..b} = g {a..b}" if "a ≤ c" "c ≤ b"
  proof (cases "c = a ∨ c = b")
    case False
  with that have "a < c" "c < b"
    by auto
    then show ?thesis
    by (rule coalesce_less)
  next
    case True
  with that box_empty_imp [of a a] box_empty_imp [of b b] show ?thesis
    by safe simp_all
    qed

end

lemma operative_realI:
  "operative_real f z g" if "operative f z g"
proof -
  interpret operative f z g
    using that .
  show ?thesis
  proof
    show "g {a..b} = z" if "b ≤ a" for a b
      using that box_empty_imp by simp
    show "f (g {a..c}) (g {c..b}) = g {a..b}" if "a < c" "c < b" for a b c
      using that
    using Basis_imp [of 1 a b c]
      by (simp_all add: atMost_def [symmetric] atLeast_def [symmetric] max_def min_def)
qed
qed


subsection ‹Special case of additivity we need for the FTC.›

lemma additive_tagged_division_1:
  fixes f :: "real ⇒ 'a::real_normed_vector"
  assumes "a ≤ b"
    and "p tagged_division_of {a..b}"
  shows "sum (λ(x,k). f(Sup k) - f(Inf k)) p = f b - f a"
proof -
  let ?f = "(λk::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
  interpret operative_real plus 0 ?f
    rewrites "comm_monoid_set.F op + 0 = sum"
    by standard[1] (auto simp add: sum_def)
  have p_td: "p tagged_division_of cbox a b"
    using assms(2) box_real(2) by presburger
  have **: "cbox a b ≠ {}"
    using assms(1) by auto
  then have "f b - f a = (∑(x, l)∈p. if l = {} then 0 else f (interval_upperbound l) - f (interval_lowerbound l))"
    proof -
      have "(if cbox a b = {} then 0 else f (interval_upperbound (cbox a b)) - f (interval_lowerbound (cbox a b))) = f b - f a"
        using assms by auto
      then show ?thesis
        using p_td assms by (simp add: tagged_division) 
    qed 
  then show ?thesis
    using assms by (auto intro!: sum.cong)
qed


subsection ‹Fine-ness of a partition w.r.t. a gauge.›

definition fine  (infixr "fine" 46)
  where "d fine s ⟷ (∀(x,k) ∈ s. k ⊆ d x)"

lemma fineI:
  assumes "⋀x k. (x, k) ∈ s ⟹ k ⊆ d x"
  shows "d fine s"
  using assms unfolding fine_def by auto

lemma fineD[dest]:
  assumes "d fine s"
  shows "⋀x k. (x,k) ∈ s ⟹ k ⊆ d x"
  using assms unfolding fine_def by auto

lemma fine_Int: "(λx. d1 x ∩ d2 x) fine p ⟷ d1 fine p ∧ d2 fine p"
  unfolding fine_def by auto

lemma fine_Inter:
 "(λx. ⋂{f d x | d.  d ∈ s}) fine p ⟷ (∀d∈s. (f d) fine p)"
  unfolding fine_def by blast

lemma fine_Un: "d fine p1 ⟹ d fine p2 ⟹ d fine (p1 ∪ p2)"
  unfolding fine_def by blast

lemma fine_Union: "(⋀p. p ∈ ps ⟹ d fine p) ⟹ d fine (⋃ps)"
  unfolding fine_def by auto

lemma fine_subset: "p ⊆ q ⟹ d fine q ⟹ d fine p"
  unfolding fine_def by blast

subsection ‹Some basic combining lemmas.›

lemma tagged_division_Union_exists:
  assumes "finite I"
    and "∀i∈I. ∃p. p tagged_division_of i ∧ d fine p"
    and "∀i1∈I. ∀i2∈I. i1 ≠ i2 ⟶ interior i1 ∩ interior i2 = {}"
    and "⋃I = i"
   obtains p where "p tagged_division_of i" and "d fine p"
proof -
  obtain pfn where pfn:
    "⋀x. x ∈ I ⟹ pfn x tagged_division_of x"
    "⋀x. x ∈ I ⟹ d fine pfn x"
    using bchoice[OF assms(2)] by auto
  show thesis
    apply (rule_tac p="⋃(pfn ` I)" in that)
    using assms(1) assms(3) assms(4) pfn(1) tagged_division_Union apply force
    by (metis (mono_tags, lifting) fine_Union imageE pfn(2))
qed


subsection ‹The set we're concerned with must be closed.›

lemma division_of_closed:
  fixes i :: "'n::euclidean_space set"
  shows "s division_of i ⟹ closed i"
  unfolding division_of_def by fastforce

subsection ‹General bisection principle for intervals; might be useful elsewhere.›

lemma interval_bisection_step:
  fixes type :: "'a::euclidean_space"
  assumes "P {}"
    and "∀s t. P s ∧ P t ∧ interior(s) ∩ interior(t) = {} ⟶ P (s ∪ t)"
    and "¬ P (cbox a (b::'a))"
  obtains c d where "¬ P (cbox c d)"
    and "∀i∈Basis. a∙i ≤ c∙i ∧ c∙i ≤ d∙i ∧ d∙i ≤ b∙i ∧ 2 * (d∙i - c∙i) ≤ b∙i - a∙i"
proof -
  have "cbox a b ≠ {}"
    using assms(1,3) by metis
  then have ab: "⋀i. i∈Basis ⟹ a ∙ i ≤ b ∙ i"
    by (force simp: mem_box)
  have UN_cases: "⟦finite f;
           ⋀s. s∈f ⟹ P s;
           ⋀s. s∈f ⟹ ∃a b. s = cbox a b;
           ⋀s t. s∈f ⟹ t∈f ⟹ s ≠ t ⟹ interior s ∩ interior t = {}⟧ ⟹ P (⋃f)" for f
  proof (induct f rule: finite_induct)
    case empty
    show ?case
      using assms(1) by auto
  next
    case (insert x f)
    show ?case
      unfolding Union_insert
      apply (rule assms(2)[rule_format])
      using Int_interior_Union_intervals [of f "interior x"]
      by (metis (no_types, lifting) insert insert_iff open_interior)
  qed
  let ?A = "{cbox c d | c d::'a. ∀i∈Basis. (c∙i = a∙i) ∧ (d∙i = (a∙i + b∙i) / 2) ∨
    (c∙i = (a∙i + b∙i) / 2) ∧ (d∙i = b∙i)}"
  let ?PP = "λc d. ∀i∈Basis. a∙i ≤ c∙i ∧ c∙i ≤ d∙i ∧ d∙i ≤ b∙i ∧ 2 * (d∙i - c∙i) ≤ b∙i - a∙i"
  {
    presume "∀c d. ?PP c d ⟶ P (cbox c d) ⟹ False"
    then show thesis
      unfolding atomize_not not_all
      by (blast intro: that)
  }
  assume as: "∀c d. ?PP c d ⟶ P (cbox c d)"
  have "P (⋃?A)"
  proof (rule UN_cases)
    let ?B = "(λs. cbox (∑i∈Basis. (if i ∈ s then a∙i else (a∙i + b∙i) / 2) *R i::'a)
      (∑i∈Basis. (if i ∈ s then (a∙i + b∙i) / 2 else b∙i) *R i)) ` {s. s ⊆ Basis}"
    have "?A ⊆ ?B"
    proof
      fix x
      assume "x ∈ ?A"
      then obtain c d
        where x:  "x = cbox c d"
                  "⋀i. i ∈ Basis ⟹
                        c ∙ i = a ∙ i ∧ d ∙ i = (a ∙ i + b ∙ i) / 2 ∨
                        c ∙ i = (a ∙ i + b ∙ i) / 2 ∧ d ∙ i = b ∙ i" by blast
      show "x ∈ ?B"
        unfolding image_iff x
        apply (rule_tac x="{i. i∈Basis ∧ c∙i = a∙i}" in bexI)
        apply (rule arg_cong2 [where f = cbox])
        using x(2) ab
        apply (auto simp add: euclidean_eq_iff[where 'a='a])
        by fastforce
    qed
    then show "finite ?A"
      by (rule finite_subset) auto
  next
    fix s
    assume "s ∈ ?A"
    then obtain c d
      where s: "s = cbox c d"
               "⋀i. i ∈ Basis ⟹
                     c ∙ i = a ∙ i ∧ d ∙ i = (a ∙ i + b ∙ i) / 2 ∨
                     c ∙ i = (a ∙ i + b ∙ i) / 2 ∧ d ∙ i = b ∙ i"
      by blast
    show "P s"
      unfolding s
      apply (rule as[rule_format])
      using ab s(2) by force
    show "∃a b. s = cbox a b"
      unfolding s by auto
    fix t
    assume "t ∈ ?A"
    then obtain e f where t:
      "t = cbox e f"
      "⋀i. i ∈ Basis ⟹
        e ∙ i = a ∙ i ∧ f ∙ i = (a ∙ i + b ∙ i) / 2 ∨
        e ∙ i = (a ∙ i + b ∙ i) / 2 ∧ f ∙ i = b ∙ i"
      by blast
    assume "s ≠ t"
    then have "¬ (c = e ∧ d = f)"
      unfolding s t by auto
    then obtain i where "c∙i ≠ e∙i ∨ d∙i ≠ f∙i" and i': "i ∈ Basis"
      unfolding euclidean_eq_iff[where 'a='a] by auto
    then have i: "c∙i ≠ e∙i" "d∙i ≠ f∙i"
      using s(2) t(2) apply fastforce
      using t(2)[OF i'] ‹c ∙ i ≠ e ∙ i ∨ d ∙ i ≠ f ∙ i› i' s(2) t(2) by fastforce
    have *: "⋀s t. (⋀a. a ∈ s ⟹ a ∈ t ⟹ False) ⟹ s ∩ t = {}"
      by auto
    show "interior s ∩ interior t = {}"
      unfolding s t interior_cbox
    proof (rule *)
      fix x
      assume "x ∈ box c d" "x ∈ box e f"
      then have x: "c∙i < d∙i" "e∙i < f∙i" "c∙i < f∙i" "e∙i < d∙i"
        unfolding mem_box using i'
        by force+
      show False  using s(2)[OF i']
      proof safe
        assume as: "c ∙ i = a ∙ i" "d ∙ i = (a ∙ i + b ∙ i) / 2"
        show False
          using t(2)[OF i'] and i x unfolding as by (fastforce simp add:field_simps)
      next
        assume as: "c ∙ i = (a ∙ i + b ∙ i) / 2" "d ∙ i = b ∙ i"
        show False
          using t(2)[OF i'] and i x unfolding as by(fastforce simp add:field_simps)
      qed
    qed
  qed
  also have "⋃?A = cbox a b"
  proof (rule set_eqI,rule)
    fix x
    assume "x ∈ ⋃?A"
    then obtain c d where x:
      "x ∈ cbox c d"
      "⋀i. i ∈ Basis ⟹
        c ∙ i = a ∙ i ∧ d ∙ i = (a ∙ i + b ∙ i) / 2 ∨
        c ∙ i = (a ∙ i + b ∙ i) / 2 ∧ d ∙ i = b ∙ i"
      by blast
    show "x∈cbox a b"
      unfolding mem_box
    proof safe
      fix i :: 'a
      assume i: "i ∈ Basis"
      then show "a ∙ i ≤ x ∙ i" "x ∙ i ≤ b ∙ i"
        using x(2)[OF i] x(1)[unfolded mem_box,THEN bspec, OF i] by auto
    qed
  next
    fix x
    assume x: "x ∈ cbox a b"
    have "∀i∈Basis.
      ∃c d. (c = a∙i ∧ d = (a∙i + b∙i) / 2 ∨ c = (a∙i + b∙i) / 2 ∧ d = b∙i) ∧ c≤x∙i ∧ x∙i ≤ d"
      (is "∀i∈Basis. ∃c d. ?P i c d")
      unfolding mem_box
    proof
      fix i :: 'a
      assume i: "i ∈ Basis"
      have "?P i (a∙i) ((a ∙ i + b ∙ i) / 2) ∨ ?P i ((a ∙ i + b ∙ i) / 2) (b∙i)"
        using x[unfolded mem_box,THEN bspec, OF i] by auto
      then show "∃c d. ?P i c d"
        by blast
    qed
    then obtain α β where
     "∀i∈Basis. (α ∙ i = a ∙ i ∧ β ∙ i = (a ∙ i + b ∙ i) / 2 ∨
         α ∙ i = (a ∙ i + b ∙ i) / 2 ∧ β ∙ i = b ∙ i) ∧ α ∙ i ≤ x ∙ i ∧ x ∙ i ≤ β ∙ i"
      by (auto simp: choice_Basis_iff)
    then show "x∈⋃?A"
      by (force simp add: mem_box)
  qed
  finally show False
    using assms by auto
qed

lemma interval_bisection:
  fixes type :: "'a::euclidean_space"
  assumes "P {}"
    and "(∀s t. P s ∧ P t ∧ interior(s) ∩ interior(t) = {} ⟶ P(s ∪ t))"
    and "¬ P (cbox a (b::'a))"
  obtains x where "x ∈ cbox a b"
    and "∀e>0. ∃c d. x ∈ cbox c d ∧ cbox c d ⊆ ball x e ∧ cbox c d ⊆ cbox a b ∧ ¬ P (cbox c d)"
proof -
  have "∀x. ∃y. ¬ P (cbox (fst x) (snd x)) ⟶ (¬ P (cbox (fst y) (snd y)) ∧
    (∀i∈Basis. fst x∙i ≤ fst y∙i ∧ fst y∙i ≤ snd y∙i ∧ snd y∙i ≤ snd x∙i ∧
       2 * (snd y∙i - fst y∙i) ≤ snd x∙i - fst x∙i))" (is "∀x. ?P x")
  proof
    show "?P x" for x
    proof (cases "P (cbox (fst x) (snd x))")
      case True
      then show ?thesis by auto
    next
      case as: False
      obtain c d where "¬ P (cbox c d)"
        "∀i∈Basis.
           fst x ∙ i ≤ c ∙ i ∧
           c ∙ i ≤ d ∙ i ∧
           d ∙ i ≤ snd x ∙ i ∧
           2 * (d ∙ i - c ∙ i) ≤ snd x ∙ i - fst x ∙ i"
        by (rule interval_bisection_step[of P, OF assms(1-2) as])
      then show ?thesis
        by (rule_tac x="(c,d)" in exI) auto
    qed
  qed
  then obtain f where f:
    "∀x.
      ¬ P (cbox (fst x) (snd x)) ⟶
      ¬ P (cbox (fst (f x)) (snd (f x))) ∧
        (∀i∈Basis.
            fst x ∙ i ≤ fst (f x) ∙ i ∧
            fst (f x) ∙ i ≤ snd (f x) ∙ i ∧
            snd (f x) ∙ i ≤ snd x ∙ i ∧
            2 * (snd (f x) ∙ i - fst (f x) ∙ i) ≤ snd x ∙ i - fst x ∙ i)" by metis
  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
  have [simp]: "A 0 = a" "B 0 = b" and ABRAW: "⋀n. ¬ P (cbox (A(Suc n)) (B(Suc n))) ∧
    (∀i∈Basis. A(n)∙i ≤ A(Suc n)∙i ∧ A(Suc n)∙i ≤ B(Suc n)∙i ∧ B(Suc n)∙i ≤ B(n)∙i ∧
    2 * (B(Suc n)∙i - A(Suc n)∙i) ≤ B(n)∙i - A(n)∙i)" (is "⋀n. ?P n")
  proof -
    show "A 0 = a" "B 0 = b"
      unfolding ab_def by auto
    note S = ab_def funpow.simps o_def id_apply
    show "?P n" for n
    proof (induct n)
      case 0
      then show ?case
        unfolding S using ‹¬ P (cbox a b)› f by auto
    next
      case (Suc n)
      show ?case
        unfolding S
        apply (rule f[rule_format])
        using Suc
        unfolding S
        apply auto
        done
    qed
  qed
  then have AB: "A(n)∙i ≤ A(Suc n)∙i" "A(Suc n)∙i ≤ B(Suc n)∙i" 
                 "B(Suc n)∙i ≤ B(n)∙i" "2 * (B(Suc n)∙i - A(Suc n)∙i) ≤ B(n)∙i - A(n)∙i" 
                if "i∈Basis" for i n
    using that by blast+
  have notPAB: "¬ P (cbox (A(Suc n)) (B(Suc n)))" for n
    using ABRAW by blast
  have interv: "∃n. ∀x∈cbox (A n) (B n). ∀y∈cbox (A n) (B n). dist x y < e"
    if e: "0 < e" for e
  proof -
    obtain n where n: "(∑i∈Basis. b ∙ i - a ∙ i) / e < 2 ^ n"
      using real_arch_pow[of 2 "(sum (λi. b∙i - a∙i) Basis) / e"] by auto
    show ?thesis
    proof (rule exI [where x=n], clarify)
      fix x y
      assume xy: "x∈cbox (A n) (B n)" "y∈cbox (A n) (B n)"
      have "dist x y ≤ sum (λi. ¦(x - y)∙i¦) Basis"
        unfolding dist_norm by(rule norm_le_l1)
      also have "… ≤ sum (λi. B n∙i - A n∙i) Basis"
      proof (rule sum_mono)
        fix i :: 'a
        assume i: "i ∈ Basis"
        show "¦(x - y) ∙ i¦ ≤ B n ∙ i - A n ∙ i"
          using xy[unfolded mem_box,THEN bspec, OF i]
          by (auto simp: inner_diff_left)
      qed
      also have "… ≤ sum (λi. b∙i - a∙i) Basis / 2^n"
        unfolding sum_divide_distrib
      proof (rule sum_mono)
        show "B n ∙ i - A n ∙ i ≤ (b ∙ i - a ∙ i) / 2 ^ n" if i: "i ∈ Basis" for i
        proof (induct n)
          case 0
          then show ?case
            unfolding AB by auto
        next
          case (Suc n)
          have "B (Suc n) ∙ i - A (Suc n) ∙ i ≤ (B n ∙ i - A n ∙ i) / 2"
            using AB(3) that AB(4)[of i n] using i by auto
          also have "… ≤ (b ∙ i - a ∙ i) / 2 ^ Suc n"
            using Suc by (auto simp add: field_simps)
          finally show ?case .
        qed
      qed
      also have "… < e"
        using n using e by (auto simp add: field_simps)
      finally show "dist x y < e" .
    qed
  qed
  {
    fix n m :: nat
    assume "m ≤ n" then have "cbox (A n) (B n) ⊆ cbox (A m) (B m)"
    proof (induction rule: inc_induct)
      case (step i)
      show ?case
        using AB by (intro order_trans[OF step.IH] subset_box_imp) auto
    qed simp
  } note ABsubset = this
  have "∃a. ∀n. a∈ cbox (A n) (B n)"
  proof (rule decreasing_closed_nest)
    show "∀n. closed (cbox (A n) (B n))"
      by (simp add: closed_cbox)
    show "∀n. cbox (A n) (B n) ≠ {}"
      by (meson AB dual_order.trans interval_not_empty)
  qed (use ABsubset interv in auto)
  then obtain x0 where x0: "⋀n. x0 ∈ cbox (A n) (B n)"
    by blast
  show thesis
  proof (rule that[rule_format, of x0])
    show "x0∈cbox a b"
      using ‹A 0 = a› ‹B 0 = b› x0 by blast
    fix e :: real
    assume "e > 0"
    from interv[OF this] obtain n
      where n: "∀x∈cbox (A n) (B n). ∀y∈cbox (A n) (B n). dist x y < e" ..
    have "¬ P (cbox (A n) (B n))"
    proof (cases "0 < n")
      case True then show ?thesis 
        by (metis Suc_pred' notPAB) 
    next
      case False then show ?thesis
        using ‹A 0 = a› ‹B 0 = b› ‹¬ P (cbox a b)› by blast
    qed
    moreover have "cbox (A n) (B n) ⊆ ball x0 e"
      using n using x0[of n] by auto
    moreover have "cbox (A n) (B n) ⊆ cbox a b"
      using ABsubset ‹A 0 = a› ‹B 0 = b› by blast
    ultimately show "∃c d. x0 ∈ cbox c d ∧ cbox c d ⊆ ball x0 e ∧ cbox c d ⊆ cbox a b ∧ ¬ P (cbox c d)"
      apply (rule_tac x="A n" in exI)
      apply (rule_tac x="B n" in exI)
      apply (auto simp: x0)
      done
  qed
qed


subsection ‹Cousin's lemma.›

lemma fine_division_exists:
  fixes a b :: "'a::euclidean_space"
  assumes "gauge g"
  obtains p where "p tagged_division_of (cbox a b)" "g fine p"
proof (cases "∃p. p tagged_division_of (cbox a b) ∧ g fine p")
  case True
  then show ?thesis
    using that by auto
next
  case False
  assume "¬ (∃p. p tagged_division_of (cbox a b) ∧ g fine p)"
  obtain x where x:
      "x ∈ (cbox a b)"
      "⋀e. 0 < e ⟹
        ∃c d.
          x ∈ cbox c d ∧
          cbox c d ⊆ ball x e ∧
          cbox c d ⊆ (cbox a b) ∧
          ¬ (∃p. p tagged_division_of cbox c d ∧ g fine p)"
    apply (rule interval_bisection[of "λs. ∃p. p tagged_division_of s ∧ g fine p", OF _ _ False])
    apply (simp add: fine_def)
    apply (metis tagged_division_Un fine_Un)
    apply auto
    done
  obtain e where e: "e > 0" "ball x e ⊆ g x"
    using gaugeD[OF assms, of x] unfolding open_contains_ball by auto
  from x(2)[OF e(1)]
  obtain c d where c_d: "x ∈ cbox c d"
                        "cbox c d ⊆ ball x e"
                        "cbox c d ⊆ cbox a b"
                        "¬ (∃p. p tagged_division_of cbox c d ∧ g fine p)"
    by blast
  have "g fine {(x, cbox c d)}"
    unfolding fine_def using e using c_d(2) by auto
  then show ?thesis
    using tagged_division_of_self[OF c_d(1)] using c_d by auto
qed

lemma fine_division_exists_real:
  fixes a b :: real
  assumes "gauge g"
  obtains p where "p tagged_division_of {a .. b}" "g fine p"
  by (metis assms box_real(2) fine_division_exists)

subsection ‹A technical lemma about "refinement" of division.›

lemma tagged_division_finer:
  fixes p :: "('a::euclidean_space × ('a::euclidean_space set)) set"
  assumes "p tagged_division_of (cbox a b)"
    and "gauge d"
  obtains q where "q tagged_division_of (cbox a b)"
    and "d fine q"
    and "∀(x,k) ∈ p. k ⊆ d(x) ⟶ (x,k) ∈ q"
proof -
  let ?P = "λp. p tagged_partial_division_of (cbox a b) ⟶ gauge d ⟶
    (∃q. q tagged_division_of (⋃{k. ∃x. (x,k) ∈ p}) ∧ d fine q ∧
      (∀(x,k) ∈ p. k ⊆ d(x) ⟶ (x,k) ∈ q))"
  {
    have *: "finite p" "p tagged_partial_division_of (cbox a b)"
      using assms(1)
      unfolding tagged_division_of_def
      by auto
    presume "⋀p. finite p ⟹ ?P p"
    from this[rule_format,OF * assms(2)] 
    obtain q where q: "q tagged_division_of ⋃{k. ∃x. (x, k) ∈ p}" "d fine q" "(∀(x, k)∈p. k ⊆ d x ⟶ (x, k) ∈ q)"
      by auto
    with that[of q] show ?thesis
      using assms(1) by auto
  }
  fix p :: "('a::euclidean_space × ('a::euclidean_space set)) set"
  assume as: "finite p"
  show "?P p"
    apply rule
    apply rule
    using as
  proof (induct p)
    case empty
    show ?case
      by (force simp add: fine_def)
  next
    case (insert xk p)
    obtain x k where xk: "xk = (x, k)"
      using surj_pair[of xk] by metis 
    obtain q1 where q1: "q1 tagged_division_of ⋃{k. ∃x. (x, k) ∈ p}"
                and "d fine q1"
                and q1I: "⋀x k. ⟦(x, k)∈p;  k ⊆ d x⟧ ⟹ (x, k) ∈ q1"
      using case_prodD tagged_partial_division_subset[OF insert(4) subset_insertI]
      by (metis (mono_tags, lifting) insert.hyps(3) insert.prems(2))
    have *: "⋃{l. ∃y. (y,l) ∈ insert xk p} = k ∪ ⋃{l. ∃y. (y,l) ∈ p}"
      unfolding xk by auto
    note p = tagged_partial_division_ofD[OF insert(4)]
    obtain u v where uv: "k = cbox u v"
      using p(4)[unfolded xk, OF insertI1] by blast
    have "finite {k. ∃x. (x, k) ∈ p}"
      apply (rule finite_subset[of _ "snd ` p"])
      using image_iff apply fastforce
      using insert.hyps(1) by blast
    then have int: "interior (cbox u v) ∩ interior (⋃{k. ∃x. (x, k) ∈ p}) = {}"
    proof (rule Int_interior_Union_intervals)
      show "open (interior (cbox u v))"
        by auto
      show "⋀T. T ∈ {k. ∃x. (x, k) ∈ p} ⟹ ∃a b. T = cbox a b"
        using p(4) by auto
      show "⋀T. T ∈ {k. ∃x. (x, k) ∈ p} ⟹ interior (cbox u v) ∩ interior T = {}"
        by clarify (metis insert.hyps(2) insert_iff interior_cbox p(5) uv xk)
    qed
    show ?case
    proof (cases "cbox u v ⊆ d x")
      case True
      have "{(x, cbox u v)} tagged_division_of cbox u v"
        by (simp add: p(2) uv xk tagged_division_of_self)
      then have "{(x, cbox u v)} ∪ q1 tagged_division_of ⋃{k. ∃x. (x, k) ∈ insert xk p}"
        unfolding * uv by (metis (no_types, lifting) int q1 tagged_division_Un)
      with True show ?thesis
        apply (rule_tac x="{(x,cbox u v)} ∪ q1" in exI)
        using ‹d fine q1› fine_def q1I uv xk apply fastforce
        done
    next
      case False
      obtain q2 where q2: "q2 tagged_division_of cbox u v" "d fine q2"
        using fine_division_exists[OF assms(2)] by blast
      show ?thesis
        apply (rule_tac x="q2 ∪ q1" in exI)
        apply (intro conjI)
        unfolding * uv
        apply (rule tagged_division_Un q2 q1 int fine_Un)+
          apply (auto intro: q1 q2 fine_Un ‹d fine q1› simp add: False q1I uv xk)
        done
    qed
  qed
qed

subsubsection ‹Covering lemma›

text‹ Some technical lemmas used in the approximation results that follow. Proof of the covering
  lemma is an obvious multidimensional generalization of Lemma 3, p65 of Swartz's
  "Introduction to Gauge Integrals". ›

proposition covering_lemma:
  assumes "S ⊆ cbox a b" "box a b ≠ {}" "gauge g"
  obtains 𝒟 where
    "countable 𝒟"  "⋃𝒟 ⊆ cbox a b"
    "⋀K. K ∈ 𝒟 ⟹ interior K ≠ {} ∧ (∃c d. K = cbox c d)"
    "pairwise (λA B. interior A ∩ interior B = {}) 𝒟"
    "⋀K. K ∈ 𝒟 ⟹ ∃x ∈ S ∩ K. K ⊆ g x"
    "⋀u v. cbox u v ∈ 𝒟 ⟹ ∃n. ∀i ∈ Basis. v ∙ i - u ∙ i = (b ∙ i - a ∙ i) / 2^n"
    "S ⊆ ⋃𝒟"
proof -
  have aibi: "⋀i. i ∈ Basis ⟹ a ∙ i ≤ b ∙ i" and normab: "0 < norm(b - a)"
    using ‹box a b ≠ {}› box_eq_empty box_sing by fastforce+
  let ?K0 = "λ(n, f::'a⇒nat).
                    cbox (∑i ∈ Basis. (a ∙ i + (f i / 2^n) * (b ∙ i - a ∙ i)) *R i)
                         (∑i ∈ Basis. (a ∙ i + ((f i + 1) / 2^n) * (b ∙ i - a ∙ i)) *R i)"
  let ?D0 = "?K0 ` (SIGMA n:UNIV. PiE Basis (λi::'a. lessThan (2^n)))"
  obtain 𝒟0 where count: "countable 𝒟0"
             and sub: "⋃𝒟0 ⊆ cbox a b"
             and int:  "⋀K. K ∈ 𝒟0 ⟹ (interior K ≠ {}) ∧ (∃c d. K = cbox c d)"
             and intdj: "⋀A B. ⟦A ∈ 𝒟0; B ∈ 𝒟0⟧ ⟹ A ⊆ B ∨ B ⊆ A ∨ interior A ∩ interior B = {}"
             and SK: "⋀x. x ∈ S ⟹ ∃K ∈ 𝒟0. x ∈ K ∧ K ⊆ g x"
             and cbox: "⋀u v. cbox u v ∈ 𝒟0 ⟹ ∃n. ∀i ∈ Basis. v ∙ i - u ∙ i = (b ∙ i - a ∙ i) / 2^n"
             and fin: "⋀K. K ∈ 𝒟0 ⟹ finite {L ∈ 𝒟0. K ⊆ L}"
  proof
    show "countable ?D0"
      by (simp add: countable_PiE)
  next
    show "⋃?D0 ⊆ cbox a b"
      apply (simp add: UN_subset_iff)
      apply (intro conjI allI ballI subset_box_imp)
       apply (simp add: divide_simps zero_le_mult_iff aibi)
      apply (force simp: aibi scaling_mono nat_less_real_le dest: PiE_mem)
      done
  next
    show "⋀K. K ∈ ?D0 ⟹ interior K ≠ {} ∧ (∃c d. K = cbox c d)"
      using ‹box a b ≠ {}›
      by (clarsimp simp: box_eq_empty) (fastforce simp add: divide_simps dest: PiE_mem)
  next
    have realff: "(real w) * 2^m < (real v) * 2^n ⟷ w * 2^m < v * 2^n" for m n v w
      using of_nat_less_iff less_imp_of_nat_less by fastforce
    have *: "∀v w. ?K0(m,v) ⊆ ?K0(n,w) ∨ ?K0(n,w) ⊆ ?K0(m,v) ∨ interior(?K0(m,v)) ∩ interior(?K0(n,w)) = {}"
      for m n ‹The symmetry argument requires a single HOL formula›
    proof (rule linorder_wlog [where a=m and b=n], intro allI impI)
      fix v w m and n::nat
      assume "m ≤ n" ‹WLOG we can assume @{term"m ≤ n"}, when the first disjunct becomes impossible›
      have "?K0(n,w) ⊆ ?K0(m,v) ∨ interior(?K0(m,v)) ∩ interior(?K0(n,w)) = {}"
        apply (simp add: subset_box disjoint_interval)
        apply (rule ccontr)
        apply (clarsimp simp add: aibi mult_le_cancel_right divide_le_cancel not_less not_le)
        apply (drule_tac x=i in bspec, assumption)
        using ‹m≤n› realff [of _ _ "1+_"] realff [of "1+_"_ "1+_"]
        apply (auto simp: divide_simps add.commute not_le nat_le_iff_add realff)
        apply (simp add: power_add, metis (no_types, hide_lams) mult_Suc mult_less_cancel2 not_less_eq mult.assoc)+
        done
      then show "?K0(m,v) ⊆ ?K0(n,w) ∨ ?K0(n,w) ⊆ ?K0(m,v) ∨ interior(?K0(m,v)) ∩ interior(?K0(n,w)) = {}"
        by meson
    qed auto
    show "⋀A B. ⟦A ∈ ?D0; B ∈ ?D0⟧ ⟹ A ⊆ B ∨ B ⊆ A ∨ interior A ∩ interior B = {}"
      apply (erule imageE SigmaE)+
      using * by simp
  next
    show "∃K ∈ ?D0. x ∈ K ∧ K ⊆ g x" if "x ∈ S" for x
    proof (simp only: bex_simps split_paired_Bex_Sigma)
      show "∃n. ∃f ∈ Basis →E {..<2 ^ n}. x ∈ ?K0(n,f) ∧ ?K0(n,f) ⊆ g x"
      proof -
        obtain e where "0 < e"
                   and e: "⋀y. (⋀i. i ∈ Basis ⟹ ¦x ∙ i - y ∙ i¦ ≤ e) ⟹ y ∈ g x"
        proof -
          have "x ∈ g x" "open (g x)"
            using ‹gauge g› by (auto simp: gauge_def)
          then obtain ε where "0 < ε" and ε: "ball x ε ⊆ g x"
            using openE by blast
          have "norm (x - y) < ε"
               if "(⋀i. i ∈ Basis ⟹ ¦x ∙ i - y ∙ i¦ ≤ ε / (2 * real DIM('a)))" for y
          proof -
            have "norm (x - y) ≤ (∑i∈Basis. ¦x ∙ i - y ∙ i¦)"
              by (metis (no_types, lifting) inner_diff_left norm_le_l1 sum.cong)
            also have "... ≤ DIM('a) * (ε / (2 * real DIM('a)))"
              by (meson sum_bounded_above that)
            also have "... = ε / 2"
              by (simp add: divide_simps)
            also have "... < ε"
              by (simp add: ‹0 < ε›)
            finally show ?thesis .
          qed
          then show ?thesis
            by (rule_tac e = "ε / 2 / DIM('a)" in that) (simp_all add:  ‹0 < ε› dist_norm subsetD [OF ε])
        qed
        have xab: "x ∈ cbox a b"
          using ‹x ∈ S› ‹S ⊆ cbox a b› by blast
        obtain n where n: "norm (b - a) / 2^n < e"
          using real_arch_pow_inv [of "e / norm(b - a)" "1/2"] normab ‹0 < e›
          by (auto simp: divide_simps)
        then have "norm (b - a) < e * 2^n"
          by (auto simp: divide_simps)
        then have bai: "b ∙ i - a ∙ i < e * 2 ^ n" if "i ∈ Basis" for i
        proof -
          have "b ∙ i - a ∙ i ≤ norm (b - a)"
            by (metis abs_of_nonneg dual_order.trans inner_diff_left linear norm_ge_zero Basis_le_norm that)
          also have "... < e * 2 ^ n"
            using ‹norm (b - a) < e * 2 ^ n› by blast
          finally show ?thesis .
        qed
        have D: "(a + n ≤ x ∧ x ≤ a + m) ⟹ (a + n ≤ y ∧ y ≤ a + m) ⟹ abs(x - y) ≤ m - n"
                 for a m n x and y::real
          by auto
        have "∀i∈Basis. ∃k<2 ^ n. (a ∙ i + real k * (b ∙ i - a ∙ i) / 2 ^ n ≤ x ∙ i ∧
               x ∙ i ≤ a ∙ i + (real k + 1) * (b ∙ i - a ∙ i) / 2 ^ n)"
        proof
          fix i::'a assume "i ∈ Basis"
          consider "x ∙ i = b ∙ i" | "x ∙ i < b ∙ i"
            using ‹i ∈ Basis› mem_box(2) xab by force
          then show "∃k<2 ^ n. (a ∙ i + real k * (b ∙ i - a ∙ i) / 2 ^ n ≤ x ∙ i ∧
                          x ∙ i ≤ a ∙ i + (real k + 1) * (b ∙ i - a ∙ i) / 2 ^ n)"
          proof cases
            case 1 then show ?thesis
              by (rule_tac x = "2^n - 1" in exI) (auto simp: algebra_simps divide_simps of_nat_diff ‹i ∈ Basis› aibi)
          next
            case 2
            then have abi_less: "a ∙ i < b ∙ i"
              using ‹i ∈ Basis› xab by (auto simp: mem_box)
            let ?k = "nat ⌊2 ^ n * (x ∙ i - a ∙ i) / (b ∙ i - a ∙ i)⌋"
            show ?thesis
            proof (intro exI conjI)
              show "?k < 2 ^ n"
                using aibi xab ‹i ∈ Basis›
                by (force simp: nat_less_iff floor_less_iff divide_simps 2 mem_box)
            next
              have "a ∙ i + real ?k * (b ∙ i - a ∙ i) / 2 ^ n ≤
                    a ∙ i + (2 ^ n * (x ∙ i - a ∙ i) / (b ∙ i - a ∙ i)) * (b ∙ i - a ∙ i) / 2 ^ n"
                apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
                using aibi [OF ‹i ∈ Basis›] xab 2
                  apply (simp_all add: ‹i ∈ Basis› mem_box divide_simps)
                done
              also have "... = x ∙ i"
                using abi_less by (simp add: divide_simps)
              finally show "a ∙ i + real ?k * (b ∙ i - a ∙ i) / 2 ^ n ≤ x ∙ i" .
            next
              have "x ∙ i ≤ a ∙ i + (2 ^ n * (x ∙ i - a ∙ i) / (b ∙ i - a ∙ i)) * (b ∙ i - a ∙ i) / 2 ^ n"
                using abi_less by (simp add: divide_simps algebra_simps)
              also have "... ≤ a ∙ i + (real ?k + 1) * (b ∙ i - a ∙ i) / 2 ^ n"
                apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
                using aibi [OF ‹i ∈ Basis›] xab
                  apply (auto simp: ‹i ∈ Basis› mem_box divide_simps)
                done
              finally show "x ∙ i ≤ a ∙ i + (real ?k + 1) * (b ∙ i - a ∙ i) / 2 ^ n" .
            qed
          qed
        qed
        then have "∃f∈Basis →E {..<2 ^ n}. x ∈ ?K0(n,f)"
          apply (simp add: mem_box Bex_def)
          apply (clarify dest!: bchoice)
          apply (rule_tac x="restrict f Basis" in exI, simp)
          done
        moreover have "⋀f. x ∈ ?K0(n,f) ⟹ ?K0(n,f) ⊆ g x"
          apply (clarsimp simp add: mem_box)
          apply (rule e)
          apply (drule bspec D, assumption)+
          apply (erule order_trans)
          apply (simp add: divide_simps)
          using bai by (force simp: algebra_simps)
        ultimately show ?thesis by auto
      qed
    qed
  next
    show "⋀u v. cbox u v ∈ ?D0 ⟹ ∃n. ∀i ∈ Basis. v ∙ i - u ∙ i = (b ∙ i - a ∙ i) / 2^n"
      by (force simp: eq_cbox box_eq_empty field_simps dest!: aibi)
  next
    obtain j::'a where "j ∈ Basis"
      using nonempty_Basis by blast
    have "finite {L ∈ ?D0. ?K0(n,f) ⊆ L}" if "f ∈ Basis →E {..<2 ^ n}" for n f
    proof (rule finite_subset)
      let ?B = "(λ(n, f::'a⇒nat). cbox (∑i∈Basis. (a ∙ i + (f i) / 2^n * (b ∙ i - a ∙ i)) *R i)
                                        (∑i∈Basis. (a ∙ i + ((f i) + 1) / 2^n * (b ∙ i - a ∙ i)) *R i))
                ` (SIGMA m:atMost n. PiE Basis (λi::'a. lessThan (2^m)))"
      have "?K0(m,g) ∈ ?B" if "g ∈ Basis →E {..<2 ^ m}" "?K0(n,f) ⊆ ?K0(m,g)" for m g
      proof -
        have dd: "w / m ≤ v / n ∧ (v+1) / n ≤ (w+1) / m
                  ⟹ inverse n ≤ inverse m" for w m v n::real
          by (auto simp: divide_simps algebra_simps)
        have bjaj: "b ∙ j - a ∙ j > 0"
          using ‹j ∈ Basis› ‹box a b ≠ {}› box_eq_empty(1) by fastforce
        have "((g j) / 2 ^ m) * (b ∙ j - a ∙ j) ≤ ((f j) / 2 ^ n) * (b ∙ j - a ∙ j) ∧
              (((f j) + 1) / 2 ^ n) * (b ∙ j - a ∙ j) ≤ (((g j) + 1) / 2 ^ m) * (b ∙ j - a ∙ j)"
          using that ‹j ∈ Basis› by (simp add: subset_box algebra_simps divide_simps aibi)
        then have "((g j) / 2 ^ m) ≤ ((f j) / 2 ^ n) ∧
          ((real(f j) + 1) / 2 ^ n) ≤ ((real(g j) + 1) / 2 ^ m)"
          by (metis bjaj mult.commute of_nat_1 of_nat_add real_mult_le_cancel_iff2)
        then have "inverse (2^n) ≤ (inverse (2^m) :: real)"
          by (rule dd)
        then have "m ≤ n"
          by auto
        show ?thesis
          by (rule imageI) (simp add: ‹m ≤ n› that)
      qed
      then show "{L ∈ ?D0. ?K0(n,f) ⊆ L} ⊆ ?B"
        by auto
      show "finite ?B"
        by (intro finite_imageI finite_SigmaI finite_atMost finite_lessThan finite_PiE finite_Basis)
    qed
    then show "finite {L ∈ ?D0. K ⊆ L}" if "K ∈ ?D0" for K
      using that by auto
  qed
  let ?D1 = "{K ∈ 𝒟0. ∃x ∈ S ∩ K. K ⊆ g x}"
  obtain 𝒟 where count: "countable 𝒟"
             and sub: "⋃𝒟 ⊆ cbox a b"  "S ⊆ ⋃𝒟"
             and int:  "⋀K. K ∈ 𝒟 ⟹ (interior K ≠ {}) ∧ (∃c d. K = cbox c d)"
             and intdj: "⋀A B. ⟦A ∈ 𝒟; B ∈ 𝒟⟧ ⟹ A ⊆ B ∨ B ⊆ A ∨ interior A ∩ interior B = {}"
             and SK: "⋀K. K ∈ 𝒟 ⟹ ∃x. x ∈ S ∩ K ∧ K ⊆ g x"
             and cbox: "⋀u v. cbox u v ∈ 𝒟 ⟹ ∃n. ∀i ∈ Basis. v ∙ i - u ∙ i = (b ∙ i - a ∙ i) / 2^n"
             and fin: "⋀K. K ∈ 𝒟 ⟹ finite {L. L ∈ 𝒟 ∧ K ⊆ L}"
  proof
    show "countable ?D1" using count countable_subset
      by (simp add: count countable_subset)
    show "⋃?D1 ⊆ cbox a b"
      using sub by blast
    show "S ⊆ ⋃?D1"
      using SK by (force simp:)
    show "⋀K. K ∈ ?D1 ⟹ (interior K ≠ {}) ∧ (∃c d. K = cbox c d)"
      using int by blast
    show "⋀A B. ⟦A ∈ ?D1; B ∈ ?D1⟧ ⟹ A ⊆ B ∨ B ⊆ A ∨ interior A ∩ interior B = {}"
      using intdj by blast
    show "⋀K. K ∈ ?D1 ⟹ ∃x. x ∈ S ∩ K ∧ K ⊆ g x"
      by auto
    show "⋀u v. cbox u v ∈ ?D1 ⟹ ∃n. ∀i ∈ Basis. v ∙ i - u ∙ i = (b ∙ i - a ∙ i) / 2^n"
      using cbox by blast
    show "⋀K. K ∈ ?D1 ⟹ finite {L. L ∈ ?D1 ∧ K ⊆ L}"
      using fin by simp (metis (mono_tags, lifting) Collect_mono rev_finite_subset)
  qed
  let ?𝒟 = "{K ∈ 𝒟. ∀K'. K' ∈ 𝒟 ∧ K ≠ K' ⟶ ~(K ⊆ K')}"
  show ?thesis
  proof (rule that)
    show "countable ?𝒟"
      by (blast intro: countable_subset [OF _ count])
    show "⋃?𝒟 ⊆ cbox a b"
      using sub by blast
    show "S ⊆ ⋃?𝒟"
    proof clarsimp
      fix x
      assume "x ∈ S"
      then obtain X where "x ∈ X" "X ∈ 𝒟" using ‹S ⊆ ⋃𝒟› by blast
      let ?R = "{(K,L). K ∈ 𝒟 ∧ L ∈ 𝒟 ∧ L ⊂ K}"
      have irrR: "irrefl ?R" by (force simp: irrefl_def)
      have traR: "trans ?R" by (force simp: trans_def)
      have finR: "⋀x. finite {y. (y, x) ∈ ?R}"
        by simp (metis (mono_tags, lifting) fin ‹X ∈ 𝒟› finite_subset mem_Collect_eq psubset_imp_subset subsetI)
      have "{X ∈ 𝒟. x ∈ X} ≠ {}"
        using ‹X ∈ 𝒟› ‹x ∈ X› by blast
      then obtain Y where "Y ∈ {X ∈ 𝒟. x ∈ X}" "⋀Y'. (Y', Y) ∈ ?R ⟹ Y' ∉ {X ∈ 𝒟. x ∈ X}"
        by (rule wfE_min' [OF wf_finite_segments [OF irrR traR finR]]) blast
      then show "∃Y. Y ∈ 𝒟 ∧ (∀K'. K' ∈ 𝒟 ∧ Y ≠ K' ⟶ ¬ Y ⊆ K') ∧ x ∈ Y"
        by blast
    qed
    show "⋀K. K ∈ ?𝒟 ⟹ interior K ≠ {} ∧ (∃c d. K = cbox c d)"
      by (blast intro: dest: int)
    show "pairwise (λA B. interior A ∩ interior B = {}) ?𝒟"
      using intdj by (simp add: pairwise_def) metis
    show "⋀K. K ∈ ?𝒟 ⟹ ∃x ∈ S ∩ K. K ⊆ g x"
      using SK by force
    show "⋀u v. cbox u v ∈ ?𝒟 ⟹ ∃n. ∀i∈Basis. v ∙ i - u ∙ i = (b ∙ i - a ∙ i) / 2^n"
      using cbox by force
    qed
qed

subsection ‹Division filter›

text ‹Divisions over all gauges towards finer divisions.›

definition division_filter :: "'a::euclidean_space set ⇒ ('a × 'a set) set filter"
  where "division_filter s = (INF g:{g. gauge g}. principal {p. p tagged_division_of s ∧ g fine p})"

lemma eventually_division_filter:
  "(∀F p in division_filter s. P p) ⟷
    (∃g. gauge g ∧ (∀p. p tagged_division_of s ∧ g fine p ⟶ P p))"
  unfolding division_filter_def
proof (subst eventually_INF_base; clarsimp)
  fix g1 g2 :: "'a ⇒ 'a set" show "gauge g1 ⟹ gauge g2 ⟹ ∃x. gauge x ∧
    {p. p tagged_division_of s ∧ x fine p} ⊆ {p. p tagged_division_of s ∧ g1 fine p} ∧
    {p. p tagged_division_of s ∧ x fine p} ⊆ {p. p tagged_division_of s ∧ g2 fine p}"
    by (intro exI[of _ "λx. g1 x ∩ g2 x"]) (auto simp: fine_Int)
qed (auto simp: eventually_principal)

lemma division_filter_not_empty: "division_filter (cbox a b) ≠ bot"
  unfolding trivial_limit_def eventually_division_filter
  by (auto elim: fine_division_exists)

lemma eventually_division_filter_tagged_division:
  "eventually (λp. p tagged_division_of s) (division_filter s)"
  unfolding eventually_division_filter by (intro exI[of _ "λx. ball x 1"]) auto

end