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
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


subsectiontag unimportant› ‹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 termu and termv.›
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 Int_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 = {sf. interior s = {}}"
  then have "finite E" "E  {sf. 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. 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 (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. 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 *
    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›
(*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 ?r
  moreover
  { fix K
    assume "s = {{a}}" "Ks"
    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_idem by auto
next
  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

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  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)
  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. {xs. 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 "sf. 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: "k1p1" "k2p2"
      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: "k1p2" "k2p1"
      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 (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
      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 "iBasis. 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 "iBasis. 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: "iBasis. 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 "kp. 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: "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
  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  {}  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: "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 (ip. (q i - {i}))  interior K = {}"
      proof (rule *[OF Int_interior_Union_intervals])
        show "T. Tq K - {K}  interior K  interior T = {}"
          using qk(5) using q(2)[OF K] by auto
        show "interior (ip. (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 bounded_subset_cbox_symmetric elementary_bounded)

proposition 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 "Kp. 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 "xp. 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 = (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)[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" "xf"
    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. 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
    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: "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)
    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›

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]:  (*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. 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))"
  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. 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
  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. 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
  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. xk  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. xk  c} = K2  {x. xk  c}"
    shows "interior (K1  {x. xk  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 "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 "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"] xp 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, 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_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: "(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. u  i  (iBasis. (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 **: "iBasis. ui  vi"
      using l using that(6) unfolding box_ne_empty[