Theory Tagged_Division

(*  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 for Henstock-Kurzweil Integration›

theory Tagged_Division
  imports Topology_Euclidean_Space
begin

lemma sum_Sigma_product:
  assumes "finite S"
    and "i. i  S  finite (T i)"
  shows "(iS. sum (x i) (T i)) = ((i, j)Sigma S T. x i j)"
  using assms
  by induction (auto simp: sum.Sigma)

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 ‹Some useful lemmas about intervals›

lemma interior_subset_union_intervals:
  fixes a b c d
  defines "i  cbox a b"
  defines "j  cbox c d"
  assumes "interior j  {}"
    and "i  j  S"
    and "interior i  interior j = {}"
  shows "interior i  interior S"
  by (smt (verit, del_insts) IntI Int_interval_mixed_eq_empty UnE assms empty_iff interior_cbox interior_maximal interior_subset open_interior subset_eq)

lemma interior_Union_subset_cbox:
  assumes "finite "
  assumes : "S. S    a b. S = cbox a b" "S. S    interior S  T"
    and T: "closed T"
  shows "interior ()  T"
proof -
  have clo[simp]: "S    closed S" for S
    using  by auto
  define E where "E = {s. interior s = {}}"
  then have "finite E" "E  {s. interior s = {}}"
    using finite  by auto
  then have "interior () = interior (( - E))"
  proof (induction E rule: finite_subset_induct')
    case (insert s f')
    have "interior (( - insert s f')  s) = interior (( - insert s f'))"
      using insert.hyps finite  by (intro interior_closed_Un_empty_interior) auto
    also have "( - insert s f')  s = ( - f')"
      using insert.hyps by auto
    finally show ?case
      by (simp add: insert.IH)
  qed simp
  also have "  ( - E)"
    by (rule interior_subset)
  also have "  T"
  proof (rule Union_least)
    fix s assume "s   - E"
    with [of s] obtain a b where s: "s  " "s = cbox a b" "box a b  {}"
      by (fastforce simp: E_def)
    have "closure (interior s)  closure T"
      by (intro closure_mono  s  )
    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. xk  c} = cbox a (iBasis. (if i = k then min (bk) c else bi) *R i)"
    "cbox a b  {x. xk  c} = cbox (iBasis. (if i = k then max (ak) c else ai) *R i) b"
  using assms by (rule_tac set_eqI; auto simp: mem_box)+

lemma interval_not_empty: "iBasis. ai  bi  cbox a b  {}"
  by (simp add: box_ne_empty)

subsection ‹Bounds on intervals where they exist›

definitiontag important› interval_upperbound :: "('a::euclidean_space) set  'a"
  where "interval_upperbound s = (iBasis. (SUP xs. xi) *R i)"

definitiontag important› interval_lowerbound :: "('a::euclidean_space) set  'a"
  where "interval_lowerbound s = (iBasis. (INF xs. xi) *R i)"

lemma interval_upperbound[simp]:
  "iBasis. ai  bi 
    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]:
  "iBasis. ai  bi 
    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 "(iBasis. (SUP xA × B. x  (i, 0)) *R i) = (iBasis. (SUP xA. x  i) *R i)"
      by (subst (2) fst_image_times') (simp del: fst_image_times add: image_comp inner_Pair_0)
  moreover from assms have snd_image_times': "B = snd ` (A × B)" by simp
  have "(iBasis. (SUP xA × B. x  (0, i)) *R i) = (iBasis. (SUP xB. x  i) *R i)"
      by (subst (2) snd_image_times') (simp del: snd_image_times add: image_comp 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 "(iBasis. (INF xA × B. x  (i, 0)) *R i) = (iBasis. (INF xA. x  i) *R i)"
      by (subst (2) fst_image_times') (simp del: fst_image_times add: image_comp inner_Pair_0)
  moreover from assms have snd_image_times': "B = snd ` (A × B)" by simp
  have "(iBasis. (INF xA × B. x  (0, i)) *R i) = (iBasis. (INF xB. x  i) *R i)"
      by (subst (2) snd_image_times') (simp del: snd_image_times add: image_comp 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›

definitiontag important› "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 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))"
  by (metis (mono_tags, lifting) gauge_def imageI open_negations minus_minus)

lemma gauge_Inter:
  assumes "finite S"
    and "u. uS  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 *
    by (simp add: assms gaugeD open_INT)
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›
(*FIXME Restructure, the subsection consists only of 1 lemma *)
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›

definitiontag important› division_of (infixl "division'_of" 40)
where
  "s division_of i 
    finite s 
    (Ks. K  i  K  {}  (a b. K = cbox a b)) 
    (K1s. K2s. 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 ?l
  have "x = {a}" if  "x  s" for x
    by (metis s division_of cbox a a cbox_idem 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_idem by auto
qed (use cbox_idem in blast)

lemma elementary_empty: obtains p where "p division_of {}"
  by simp

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  xi. ks. x  k"
  unfolding division_of_def by auto

lemma forall_in_division:
  "d division_of i  (xd. 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)
  show "finite q"
    using assms finite_subset by blast
next
  fix k
  assume "k  q"
  show "k  q"
    using k  q by auto
  show "a b. k = cbox a b" "k  {}"
    using assms k  q by blast+
next
  fix k1 k2
  assume "k1  q" "k2  q" "k1  k2"
  then show "interior k1  interior k2 = {}"
    using assms by blast
qed auto

lemma division_of_union_self[intro]: "p division_of s  p division_of (p)"
  by blast

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. {xs. x  {}} = s"
      by auto
    show UA: "?A = s1  s2"
      unfolding * 
      using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] by auto
    {
      fix k
      assume kA: "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 UA kA by blast
      show "a b. k = cbox a b"
        using k by (metis (no_types, lifting) Int_interval assms division_ofD(4))
    }
    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 show "interior k1  interior k2 = {}"
      unfolding k1 k2
      using assms division_ofD(5) k1 k2 by auto
  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 "
    and "  {}"
    and "s. p. p division_of (s::('a::euclidean_space) set)"
  shows "p. p division_of ()"
  using assms
proof (induct  rule: finite_induct)
  case (insert x )
  then show ?case
    by (metis cInf_singleton complete_lattice_class.Inf_insert elementary_Int insert_iff)
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)]
  fix k1 k2
  assume "k1  p1  p2" "k2  p1  p2" "k1  k2"
  with assms show "interior k1  interior k2 = {}"
    by (smt (verit, best) IntE Un_iff disjoint_iff_not_equal division_ofD(2) division_ofD(5) inf.orderE interior_Int)
qed (use division_ofD assms in auto)

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 (iBasis. (fst (f i)  i) *R i) (iBasis. (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
      {
        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 "iBasis. f i  g i"
          using l  K l k f g by auto
        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])
      }
      have "a  i  fst (f i)  i" "snd (f i)  i  b  i" "fst (f i)  i  snd (f i)  i"
        if "i  Basis" for i
      proof -
        have "f i = (a, c)  f i = (c, d)  f i = (d, b)"
          using that f by (auto simp: PiE_iff)
        with that 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 simp add: k box_eq_empty subset_box not_less)      
    }
    moreover
    have "kp. x  k" if x: "x  cbox a b" for x
    proof -
      have "l. x  i  {fst l  i .. snd l  i}  l  {(a, c), (c, d), (d, b)}" if "i  Basis" for i
      proof -
        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)"
          using that x ord[of 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: "iBasis. x  i  {fst (f i)  i..snd (f i)  i}  f i  {(a, c), (c, d), (d, b)}"
        by metis 
      moreover from f have "x  ?B (restrict f Basis)" "restrict f Basis  Basis E {(a,c), (c,d), (d,b)}"
        by (auto simp: mem_box)
      ultimately show ?thesis
        unfolding p_def by blast
    qed
    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
  then show ?thesis
    using elementary_interval that by auto
next
  case False
  note p = division_ofD[OF assms(1)]
  have "kp. 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
  then obtain q where q: "x. x  p  q x division_of cbox a b" "x. x  p  x  q x"
    by metis
  have "q x division_of (q x)" if x: "x  p" for x
    using q(1) x by blast
  then have di: "x. x  p  d. d division_of (q x - {x})"
    by (meson Diff_subset division_of_subset)
  have "s(λi.  (q i - {i})) ` p. d. d division_of s"
    using di by blast
  then obtain d where d: "d division_of ((λi. (q i - {i})) ` p)"
    by (meson False elementary_Inter finite_imageI image_is_empty p(1))
  have "d  p division_of cbox a b"
  proof -
    have te: "S f T. S  {}  iS. 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  p"
      then show "(q i - {i})  i = cbox a b"
        by (metis Un_commute complete_lattice_class.Sup_insert division_ofD(6) insert_Diff q)
    qed
      have [simp]: "interior (ip. (q i - {i}))  interior K = {}" if K: "K  p" for K
      proof -
      note qk = division_ofD[OF q(1)[OF K]]
      have *: "U T S. T  S = {}  U  S  U  T = {}"
        by auto
      show ?thesis
      proof (rule *[OF Int_interior_Union_intervals])
        show "T. Tq K - {K}  interior K  interior T = {}"
          using K q(2) qk(5) by auto
        show "interior (ip. (q i - {i}))  interior ((q K - {K}))"
          by (meson INF_lower K interior_mono)
      qed (use qk in auto)
    qed
    show "d  p division_of (cbox a b)"
      by (simp add: Int_interior_Union_intervals assms(1) cbox_eq d division_disjoint_union p(1) p(4))
  qed
  then show ?thesis
    by (meson Un_upper2 that)
qed

lemma elementary_bounded[dest]:
  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"
  by (meson bounded_subset_cbox_symmetric elementary_bounded)

proposition division_union_intervals_exists:
  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)  interior ((p - {cbox u v}))"
      by (metis Diff_subset Int_absorb1 Int_assoc Sup_subset_mono interior_Int p(8) uv)
    also have " = {}"
      using p(6) p(7)[OF p(2)] finite p
      by (intro Int_interior_Union_intervals) auto
    finally have disj: "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})"
      by (metis Diff_subset assms disj division_disjoint_union division_of_self division_of_subset insert_is_Un p(8) pd)
    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
      by (metis True assms division_disjoint_union elementary_interval inf_bot_left that)
  next
    case nonempty: False  
    have "Kp. q. (insert (cbox a b) q) division_of (cbox a b  K)"
      by (metis cbox a b  {} division_union_intervals_exists pdiv(4))
    then obtain q where "xp. insert (cbox a b) (q x) division_of (cbox a b)  x" 
      by metis
    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 = (xp. (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)" "xp"
        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) x'(1) x'(2) by presburger
        have "interior K'  interior (cbox a b) = {}"
          using as'(2) q(5) x' by blast
        then have "interior K'  interior x'"
          by (metis nonempty c_d interior_subset_union_intervals q(2) x')
        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 "
    and "s. s    a b. s = cbox a (b::'a::euclidean_space)"
  obtains p where "p division_of ()"
proof -
  have "p. p division_of ()"
  proof (induct_tac  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"
    then obtain a b where x: "x = cbox a b"
      by (meson assms(2)) 
    then show "p. p division_of (insert x F)"
      using elementary_union_interval by (metis Union_insert as(3) division_ofD(6))
  qed (use assms in auto)
  then show ?thesis
    using that by auto
qed

lemma elementary_union:
  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
  with elementary_unions_intervals[of "ps  pt"] assms 
  show ?thesis
    by (metis Un_iff Union_Un_distrib division_of_def finite_Un 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)"
    by (metis Diff_subset division_of_subset r1(2) r1(8))
  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"
      using divp(6) r(2) x(2) by blast
    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. Tp  interior m  interior T = {}"
          by (metis DiffD1 DiffD2 that r1(1) r1(7) rev_subsetD)
      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
    by (metis Teq div sup_ge1 that)
qed


lemma division_split:
  assumes "p division_of (cbox a b)"
    and k: "kBasis"
  shows "{l  {x. xk  c} | l. l  p  l  {x. xk  c}  {}} division_of(cbox a b  {x. xk  c})"
      (is "?p1 division_of ?I1")
    and "{l  {x. xk  c} | l. l  p  l  {x. xk  c}  {}} division_of (cbox a b  {x. xk  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)
    have "a b. cbox u v  {x. x  k  c} = cbox a b"
      unfolding interval_split[OF k] by (auto intro: order.trans)
    then show  "a b. K = cbox a b"
      by (simp add: l(1) uv)
    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)
    have "a b. cbox u v  {x. c  x  k} = cbox a b"
      unfolding interval_split[OF k] by (auto intro: order.trans)
    then show  "a b. K = cbox a b"
      by (simp add: l(1) uv)
    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›

definitiontag important› 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:
  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+

definitiontag important› 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]: 
  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 show "K  i" "K  {}" "a b. K = cbox a b"
    using assm by fastforce+
  fix K'
  assume k': "K'  snd ` s" "K  K'"
  then show "interior K  interior K' = {}"
    by (metis (no_types, lifting) assms imageE k prod.collapse tagged_division_ofD(5))
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 show "K  {}" "a b. K = cbox a b" "K  (snd ` s)"
    using assm by fastforce+
  fix K'
  assume "K'  snd ` s" "K  K'"
  then show "interior K  interior K' = {}"
    using assm(5) K by force
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}"
  by (metis box_real(2) 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" "K  s1  s2"
    using xK p1 p2 by auto
  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
  with assms show "interior K  interior K' = {}"
    by (metis Un_iff inf_commute p1(3) p2(3) tagged_division_ofD(5) xK xk')
qed

lemma tagged_division_Union:
  assumes "finite I"
    and tag: "i. iI  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))"
  using tagged_partial_division_ofD[OF assms]
  by (intro tagged_division_ofI) auto

lemma tagged_division_of_union_self:
  assumes "p tagged_division_of s"
  shows "p tagged_division_of ((snd ` p))"
  using tagged_division_ofD[OF assms]
  by (intro tagged_division_ofI) auto

lemma tagged_division_Un_interval:
  assumes "p1 tagged_division_of (cbox a b  {x. xk  (c::real)})"
    and "p2 tagged_division_of (cbox a b  {x. xk  c})"
    and k: "k  Basis"
  shows "(p1  p2) tagged_division_of (cbox a b)"
proof -
  have *: "cbox a b = (cbox a b  {x. xk  c})  (cbox a b  {x. xk  c})"
    by auto
  have "interior (cbox a b  {x. x  k  c})  interior (cbox a b  {x. c  x  k}) = {}"
    using k by (force simp: interval_split[OF k] box_def)
  with assms show ?thesis
    by (metis "*" tagged_division_Un)
qed

lemma tagged_division_Un_interval_real:
  fixes a :: real
  assumes "p1 tagged_division_of ({a .. b}  {x. xk  (c::real)})"
    and "p2 tagged_division_of ({a .. b}  {x. xk  c})"
    and k: "k  Basis"
  shows "(p1  p2) tagged_division_of {a .. b}"
  using assms by (metis box_real(2) 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. xk  c}) = {}"
  by (smt (verit) Int_Un_eq(1) Un_Int_distrib interior_Int prod.inject sup_bot.right_neutral tagged_division_ofD(5) assms)

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. xk  c} = K2  {x. xk  c}"
  shows "interior (K1  {x. xk  c}) = {}"
  by (smt (verit) Int_Un_eq(1) Un_Int_distrib interior_Int prod.inject sup_bot.right_neutral tagged_division_ofD(5) assms)

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 "xp" "yp" "xy" "snd x = snd y"
    obtain a b where ab: "snd x = cbox a b"
      using assm(4)[of "fst x" "snd x"] xp 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 xp yp have "box a b = {}"
      by (metis snd x = snd y ab assm(5) inf.idem interior_cbox prod.collapse)
    then show "d (snd x) = 1"
      by (simp add: ab assms(2))
  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, typreal, and
  typbool.›

paragraphtag important› ‹Using additivity of lifted function to encode definedness.›
text ‹%whitespace›
definitiontag important› 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)

lemmatag important› 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_set_and: "comm_monoid_set HOL.conj True"
  by (simp add: comm_monoid_set.intro conj.comm_monoid_axioms)


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}"
  by auto

lemma bgauge_existence_lemma: "(xs. d::real. 0 < d  q d x)  (x. d>0. xs  q d x)"
  by (meson zero_less_one)


paragraph ‹Division points›
text ‹%whitespace›
definitiontag important› "division_points (k::('a::euclidean_space) set) d =
   {(j,x). j  Basis  (interval_lowerbound k)j < x  x < (interval_upperbound k)j 
     (id. (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 
    (id. (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 "iBasis. ai < bi"  "ak < c" "c < bk"
    and k: "k  Basis"
  shows "division_points (cbox a b  {x. xk  c}) {l  {x. xk  c} | l . l  d  l  {x. xk  c}  {}} 
      division_points (cbox a b) d" (is ?t1)
    and "division_points (cbox a b  {x. xk  c}) {l  {x. xk  c} | l . l  d  ¬(l  {x. xk  c} = {})} 
      division_points (cbox a b) d" (is ?t2)
proof -
  note assm = division_ofD[OF assms(1)]
  have *: "iBasis. ai  bi"
    "iBasis. ai  (iBasis. (if i = k then min (b  k) c else  b  i) *R i)  i"
    "iBasis. (iBasis. (if i = k then max (a  k) c else a  i) *R i)  i  bi"
    "min (b  k) c = c" "max (a  k) c = c"
    using assms using less_imp_le by auto
   have "id. 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 "iBasis. ui  vi"
      using l using that(6) unfolding box_ne_empty[symmetric] by auto
    then show ?thesis
      using that x  Basis unfolding l interval_split[OF k] 
      by (force split: if_split_asm)
  qed
  moreover have "x y. y < (if x = k then c else b  x)  y < b  x"
    using c < bk 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 ak < c by (auto split: if_split_asm)
  moreover have "id. 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 "iBasis. ui  vi"
      using l using that(6) unfolding box_ne_empty[symmetric] by auto
    then show "id. interval_lowerbound i  x = y  interval_upperbound i  x = y"
      using that x  Basis unfolding l interval_split[OF k] 
      by (force split: if_split_asm)
  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: "iBasis. ai < bi"  "ak < c" "c < bk"
      and "l  d"
      and disj: "interval_lowerbound lk = c  interval_upperbound lk = c"
      and k: "k  Basis"
  shows "division_points (cbox a b  {x. xk  c}) {l  {x. xk  c} | l. ld  l  {x. xk  c}  {}} 
         division_points (cbox a b) d" (is "?D1  ?D")
    and "division_points (cbox a b  {x. xk  c}) {l  {x. xk  c} | l. ld  l  {x. xk  c}  {}} 
         division_points (cbox a b) d" (is "?D2  ?D")
proof -
  have ab: "iBasis. ai  bi"
    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: "iBasis. ui  vi" "iBasis. ai  ui  vi  bi"
    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. xk  c} = K2  {x. xk  c}"
    and "K1  𝒟" "K2  𝒟" "K1  K2"
  shows "interior (K1  {x. xk  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. xk  c} = K2  {x. xk  c}"
    and "K1  𝒟" "K2  𝒟" "K1  K2"
  shows "interior (K1  {x. xk  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 . ¦xk - c¦  (e::real)} =
    cbox (iBasis. (if i = k then max (ak) (c - e) else ai) *R i)
     (iBasis. (if i = k then min (bk) (c + e) else bi) *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. ¦xk - c¦  e}) ` {lp. l  {x. ¦xk - c¦  e}  {}}
         division_of  (cbox a b  {x. ¦xk - c¦  e})"
proof -
  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] cong: image_cong_simp)
      apply (rule equalityI)
      apply blast
      apply clarsimp
      apply (rename_tac S)
      apply (rule_tac x="S  {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. xk  c}) * g (cbox a b  {x. xk  c})"
begin

lemma empty [simp]: "g {} = 1"
  by (metis box_empty_imp box_subset_cbox empty_as_interval subset_empty)
       
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 "box a b = {}")
      case True
      { fix k assume "kd"
        then obtain a' b' where k: "k = cbox a' b'"
          using division_ofD(4)[OF less.prems] by blast
        then have "cbox a' b'  cbox a b"
          using k  d less.prems by blast
        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: True)
      }
      with True show "F g d = g (cbox a b)"
        by (auto intro!: neutral simp: box_empty_imp)
    next
      case False
      then have ab: "iBasis. ai < bi" and ab': "iBasis. ai  bi"
        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: "iBasis. ui  vi" "uj  vj"
            using j unfolding box_ne_empty by auto
          have *: "p r Q. ¬ jBasis  p  r  (xd. Q x)  p  r  Q (cbox u v)"
            using as j by auto
          have "(j, uj)  division_points (cbox a b) d"
               "(j, vj)  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 "aj  uj" "vj  bj"
            by (meson as division_ofD(2) j less.prems subset_box(1) uv(1))+
          ultimately have "uj = aj  vj = aj  uj = bj  vj = bj  uj = aj  vj = bj"
            using uv(2) by force
        }
        then have d': "id. u v. i = cbox u v 
          (jBasis. uj = aj  vj = aj  uj = bj  vj = bj  uj = aj  vj = bj)"
          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" 
                     "jBasis. 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]
            then show "u  j = a  j" and "v  j = b  j"
              by (smt (verit) False box_midpoint j mem_box(1) uv(2))+
          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 "xd"
            by auto note d'[rule_format,OF this]
          then obtain u v where uv: "x = cbox u v"
                      "jBasis. 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 "uj  aj  vj  bj" and j: "j  Basis"
            unfolding euclidean_eq_iff[where 'a='b] by auto
          then have "uj = vj"
            using uv(2)[rule_format,OF j] by auto
          then show "g x = 1"
            by (smt (verit) box_empty_imp box_eq_empty(1) j uv(1))
        qed
        then show "F g d = g (cbox a b)"
          by (metis deq division_of_finite insert_Diff_single insert_remove less.prems right_neutral)
      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"
                "id. 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. xk  c}" let ?gec = "{x. xk  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 = (iBasis. (if i = k then c else bi) *R i)"
        define ca where "ca = (iBasis. (if i = k then c else ai) *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 *: "xd. 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

proposition tagged_division:
  assumes "d tagged_division_of (cbox a b)"
  shows "F (λ(_, l). g l) d = g (cbox a b)"
  by (metis assms box_empty_imp division division_of_tagged_division over_tagged_division_lemma)

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"
  by (metis coalesce_less commute left_neutral less_eq_real_def neutral that)

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 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›
(*fix add explanation here *)

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 (+) 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))"
    using assms(2) tagged_division by force
  then show ?thesis
    using assms by (auto intro!: sum.cong)
qed


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

definitiontag important› 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  (ds. (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 "iI. p. p tagged_division_of i  d fine p"
    and "i1I. i2I. 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 assms by metis
  show thesis
  proof
    show " (pfn ` I) tagged_division_of i"
      using assms pfn(1) tagged_division_Union by force
    show "d fine  (pfn ` I)"
      by (metis (mono_tags, lifting) fine_Union imageE pfn(2))
  qed
qed

(* FIXME structure here, do not have one lemma in each subsection *)

subsectiontag unimportant› ‹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"
  by blast
(* FIXME structure here, do not have one lemma in each subsection *)

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

(* FIXME  move? *)
lemma interval_bisection_step:
  fixes type :: "'a::euclidean_space"
  assumes emp: "P {}"
    and Un: "S T. P S; P T; interior(S)  interior(T) = {}  P (S  T)"
    and non: "¬ P (cbox a (b::'a))"
  obtains c d where "¬ P (cbox c d)"
    and "i. i  Basis  ai  ci  ci  di  di  bi  2 * (di - ci)  bi - ai"
proof -
  have "cbox a b  {}"
    using emp non by metis
  then have ab: "i. iBasis  a  i  b  i"
    by (force simp: mem_box)
  have UN_cases: "finite ;
           S. S  P S;
           S. S  a b. S = cbox a b;
           S T. S  T  S  T  interior S  interior T = {}  P ()" for 
  proof (induct  rule: finite_induct)
    case empty show ?case
      using emp by auto
  next
    case (insert x f)
    then show ?case
      unfolding Union_insert by (metis Int_interior_Union_intervals Un insert_iff open_interior)
  qed
  let ?ab = "λi. (ai + bi) / 2"
  let ?A = "{cbox c d | c d::'a. iBasis. (ci = ai)  (di = ?ab i) 
    (ci = ?ab i)  (di = bi)}"
  have "P (?A)" 
    if "c d.  iBasis. ai  ci  ci  di  di  bi  2 * (di - ci)  bi - ai  P (cbox c d)"
  proof (rule UN_cases)
    let ?B = "(λS. cbox (iBasis. (if i  S then ai else ?ab i) *R i::'a)
                        (iBasis. (if i  S then ?ab i else bi) *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 = ?ab i  c  i = ?ab i  d  i = b  i" 
        by blast
      have "c = (iBasis. (if c  i = a  i then a  i else ?ab i) *R i)"
        "d = (iBasis. (if c  i = a  i then ?ab i else b  i) *R i)"
        using x(2) ab by (fastforce simp add: euclidean_eq_iff[where 'a='a])+
      then show "x  ?B"
        unfolding x by (rule_tac x="{i. iBasis  ci = ai}" in image_eqI) auto
    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 = ?ab i  c  i = ?ab i  d  i = b  i"
      by blast
    show "P S"
      unfolding s using ab s(2) by (fastforce intro!: that)
    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 = ?ab i  e  i = ?ab i  f  i = b  i"
      by blast
    assume "S  T"
    then have "¬ (c = e  d = f)"
      unfolding s t by auto
    then obtain i where "ci  ei  di  fi" and i': "i  Basis"
      unfolding euclidean_eq_iff[where 'a='a] by auto
    then have i: "ci  ei" "di  fi"
      using 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 "ci < fi" "ei < di"
        unfolding mem_box using i' by force+
      with i i' show False
        using s(2) t(2) by fastforce
    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 = ?ab i  c  i = ?ab i  d  i = b  i"
      by blast
    then show "xcbox a b"
      unfolding mem_box by force
  next
    fix x
    assume x: "x  cbox a b"
    then have "iBasis. c d. (c = ai  d = ?ab i  c = ?ab i  d = bi)  cxi  xi  d"
      (is "iBasis. c d. ?P i c d")
      unfolding mem_box by (metis linear)
    then obtain α β where "iBasis. (α  i = a  i  β  i = ?ab i 
         α  i = ?ab i  β  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 thesis
    by (metis (no_types, lifting) assms(3) that)
qed

lemma interval_bisection:
  fixes type :: "'a::euclidean_space"
  assumes "P {}"
    and Un: "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)) 
    (iBasis. fst xi  fst yi  fst yi  snd yi  snd yi  snd xi 
       2 * (snd yi - fst yi)  snd xi - fst xi))" (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 False
      obtain c d where "¬ P (cbox c d)"
        "i. 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 (blast intro: interval_bisection_step[of P, OF assms(1-2) False])
      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))) 
        (iBasis.
            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))) 
                  (iBasis. 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)
      then show ?case
        unfolding S
        by (force intro!: f[rule_format])
    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 "iBasis" 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. xcbox (A n) (B n). ycbox (A n) (B n). dist x y < e"
    if e: "0 < e" for e
  proof -
    obtain n where n: "(iBasis. b  i - a  i) / e < 2 ^ n"
      using real_arch_pow[of 2 "(sum (λi. bi - ai) Basis) / e"] by auto
    show ?thesis
    proof (rule exI [where x=n], clarify)
      fix x y
      assume xy: "xcbox (A n) (B n)" "ycbox (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 ni - A ni) Basis"
      proof (rule sum_mono)
        fix i :: 'a
        assume "i  Basis"
        with xy show "¦(x - y)  i¦  B n  i - A n  i"
          by (smt (verit, best) inner_diff_left mem_box(2))
      qed
      also have "  sum (λi. bi - ai) 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
  have ABsubset: "cbox (A n) (B n)  cbox (A m) (B m)" if "m  n" for m n
    using that
  proof (induction rule: inc_induct)
    case (step i) show ?case
      by (smt (verit, ccfv_SIG) ABRAW in_mono mem_box(2) step.IH subsetI)
  qed simp
  have "n. cbox (A n) (B n)  {}"
    by (meson AB dual_order.trans interval_not_empty)
  then obtain x0 where x0: "n. x0  cbox (A n) (B n)"
    using decreasing_closed_nest [OF closed_cbox] ABsubset interv by blast
  show thesis
  proof (intro that strip)
    show "x0  cbox a b"
      using A 0 = a B 0 = b x0 by blast
  next
    fix e :: real
    assume "e > 0"
    from interv[OF this] obtain n
      where n: "xcbox (A n) (B n). ycbox (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)"
      by (meson x0)
  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)"
  proof (rule interval_bisection[of "λs. p. p tagged_division_of s  _ p", OF _ _ False])
    show "p. p tagged_division_of {}  g fine p"
      by (simp add: fine_def)
  qed (meson tagged_division_Un fine_Un)+
  obtain e where e: "e > 0" "ball x e  g x"
    by (meson assms gauge_def openE)
  then 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 (meson x(2))
  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 simp
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 ptag: "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 -
  have p: "finite p" "p tagged_partial_division_of (cbox a b)"
    using ptag tagged_division_of_def by blast+
  have "(q. q tagged_division_of ({k. x. (x,k)  p})  d fine q  ((x,k)  p. k  d(x)  (x,k)  q))" 
    if "finite p" "p tagged_partial_division_of (cbox a b)" "gauge d" for p
    using that
  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 insert
      by (metis (mono_tags, lifting) case_prodD subset_insertI tagged_partial_division_subset)
    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) xk by blast
    have "{K. x. (x, K)  p}  snd ` p"
      by force
    then have "finite {K. x. (x, K)  p}"
      using finite_surj 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 = {}"
        using insert.hyps(2) p(5) uv xk by blast
    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}"
        by (smt (verit, best) "*" int q1 tagged_division_Un uv)
      moreover have "d fine ({(x,cbox u v)}  q1)"
        using True d fine q1 fine_def by fastforce
      ultimately show ?thesis
        by (metis (no_types, lifting) case_prodI2 insert_iff insert_is_Un q1I uv xk)
    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
      proof (intro exI conjI)
        show "q2  q1 tagged_division_of  {k. x. (x, k)  insert xk p}"
          by (smt (verit, best) "*" int q1 q2(1) tagged_division_Un uv)
        show "d fine q2  q1"
          by (simp add: d fine q1 fine_Un q2(2))
      qed (use False uv xk q1I in auto)
    qed
  qed
  with p 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 (meson gauge d)
  with ptag that show ?thesis by auto
qed

subsubsectiontag important› ‹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_idem by fastforce+
  let ?K0 = "λ(n, f::'anat).
                    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: field_simps aibi mult_right_mono)
      apply (force simp: aibi scaling_mono nat_less_real_le dest: PiE_mem intro: mult_right_mono)
      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: field_split_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 termm  n, when the first disjunct becomes impossible›
      have "?K0(n,w)  ?K0(m,v)  interior(?K0(m,v))  interior(?K0(n,w)) = {}"
        apply (rule ccontr)
        apply (simp add: subset_box disjoint_interval)
        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 mn realff [of _ _ "1+_"] realff [of "1+_"_ "1+_"]
        apply (auto simp: divide_simps add.commute not_le nat_le_iff_add realff)
        apply (metis (no_types, opaque_lifting) power_add 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 = {}"
      using * by fastforce
  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)  (iBasis. ¦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: field_split_simps)
            finally show ?thesis
              using 0 < ε by linarith 
          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: field_split_simps)
        then have "norm (b - a) < e * 2^n"
          by (auto simp: field_split_simps)
        then have bai: "b  i - a  i < e * 2 ^ n" if "i  Basis" for i
          by (smt (verit, del_insts) Basis_le_norm diff_add_cancel inner_simps(1) that)
        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 "iBasis. 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 field_split_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 field_split_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"
                using aibi [OF i  Basis] xab 2
                apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
                  apply (auto simp: i  Basis mem_box field_split_simps)
                done
              also have "... = x  i"
                using abi_less by (simp add: field_split_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: field_split_simps)
              also have "...  a  i + (real ?k + 1) * (b  i - a  i) / 2 ^ n"
                using aibi [OF i  Basis] xab
                apply (intro add_left_mono mult_right_mono divide_right_mono of_nat_floor)
                  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 "fBasis 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 apply (force simp add: algebra_simps)
          done
        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::'anat). cbox (iBasis. (a  i + (f i) / 2^n * (b  i - a  i)) *R i)
                                        (iBasis. (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: field_split_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 field_split_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 mult_le_cancel_left_pos)
        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 
    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. iBasis. 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.›

definitiontag important› 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})"

proposition 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)"
  using eventually_division_filter by auto

end