# 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 "(∑i∈S. sum (x i) (T i)) = (∑(i, j)∈Sigma S T. x i j)"
using assms
proof induct
case empty
then show ?case
by simp
next
case (insert a S)
show ?case
by (simp add: insert.hyps(1) insert.prems sum.Sigma)
qed

lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff

subsection✐‹tag 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 \<^term>‹u› and \<^term>‹v›.›
lemma scaling_mono:
fixes u::"'a::linordered_field"
assumes "u ≤ v" "0 ≤ r" "r ≤ s"
shows "u + r * (v - u) / s ≤ v"
proof -
have "r/s ≤ 1" using assms
using divide_le_eq_1 by fastforce
then have "(r/s) * (v - u) ≤ 1 * (v - u)"
by (meson diff_ge_0_iff_ge mult_right_mono ‹u ≤ v›)
then show ?thesis
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 = {s∈f. interior s = {}}"
then have "finite E" "E ⊆ {s∈f. interior s = {}}"
using ‹finite f› by auto
then have "interior (⋃f) = interior (⋃(f - E))"
proof (induction E rule: finite_subset_induct')
case (insert s f')
have "interior (⋃(f - insert s f') ∪ s) = interior (⋃(f - insert s f'))"
using insert.hyps ‹finite f› by (intro interior_closed_Un_empty_interior) auto
also have "⋃(f - insert s f') ∪ s = ⋃(f - f')"
using insert.hyps by auto
finally show ?case
qed simp
also have "… ⊆ ⋃(f - E)"
by (rule interior_subset)
also have "… ⊆ t"
proof (rule Union_least)
fix s assume "s ∈ f - E"
with f[of s] obtain a b where s: "s ∈ f" "s = cbox a b" "box a b ≠ {}"
by (fastforce simp: E_def)
have "closure (interior s) ⊆ closure t"
by (intro closure_mono f ‹s ∈ f›)
with s ‹closed t› show "s ⊆ t"
by simp
qed
finally show ?thesis .
qed

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

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

lemma interval_not_empty: "∀i∈Basis. a∙i ≤ b∙i ⟹ cbox a b ≠ {}"

subsection ‹Bounds on intervals where they exist›

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

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

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

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

lemmas interval_bounds = interval_upperbound interval_lowerbound

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

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

lemma interval_upperbound_Times:
assumes "A ≠ {}" and "B ≠ {}"
shows "interval_upperbound (A × B) = (interval_upperbound A, interval_upperbound B)"
proof-
from assms have fst_image_times': "A = fst ` (A × B)" by simp
have "(∑i∈Basis. (SUP x∈A × B. x ∙ (i, 0)) *⇩R i) = (∑i∈Basis. (SUP x∈A. x ∙ i) *⇩R i)"
by (subst (2) fst_image_times') (simp del: fst_image_times add: image_comp inner_Pair_0)
moreover from assms have snd_image_times': "B = snd ` (A × B)" by simp
have "(∑i∈Basis. (SUP x∈A × B. x ∙ (0, i)) *⇩R i) = (∑i∈Basis. (SUP x∈B. x ∙ i) *⇩R i)"
by (subst (2) snd_image_times') (simp del: snd_image_times add: 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 "(∑i∈Basis. (INF x∈A × B. x ∙ (i, 0)) *⇩R i) = (∑i∈Basis. (INF x∈A. x ∙ i) *⇩R i)"
by (subst (2) fst_image_times') (simp del: fst_image_times add: image_comp inner_Pair_0)
moreover from assms have snd_image_times': "B = snd ` (A × B)" by simp
have "(∑i∈Basis. (INF x∈A × B. x ∙ (0, i)) *⇩R i) = (∑i∈Basis. (INF x∈B. x ∙ i) *⇩R i)"
by (subst (2) snd_image_times') (simp del: snd_image_times add: 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›

definition✐‹tag 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. u∈S ⟹ gauge (f u)"
shows "gauge (λx. ⋂{f u x | u. u ∈ S})"
proof -
have *: "⋀x. {f u x |u. u ∈ S} = (λu. f u x) ` S"
by auto
show ?thesis
unfolding gauge_def unfolding *
using assms unfolding Ball_def Inter_iff mem_Collect_eq gauge_def by auto
qed

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

subsection ‹Attempt a systematic general set of "offset" results for components›
(*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›

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

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

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

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

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

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

lemma division_of_sing[simp]:
"s division_of cbox a (a::'a::euclidean_space) ⟷ s = {cbox a a}"
(is "?l = ?r")
proof
assume ?r
moreover
{ fix K
assume "s = {{a}}" "K∈s"
then have "∃x y. K = cbox x y"
apply (rule_tac x=a in exI)+
apply force
done
}
ultimately show ?l
unfolding division_of_def cbox_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 ⟹ ∀x∈i. ∃k∈s. x ∈ k"
unfolding division_of_def by auto

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma elementary_subset_cbox:
"p division_of S ⟹ ∃a b. S ⊆ cbox a (b::'a::euclidean_space)"
by (meson 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"
then show "insert (cbox a b) (p - {cbox u v}) division_of cbox a b ∪ ⋃(p - {cbox u v})"
by (metis (no_types) Diff_subset ‹interior (cbox a b) ∩ interior (⋃(p - {cbox u v})) = {}› division_disjoint_union division_of_subset insert_is_Un p(1) p(8))
qed
with that[of "p - {cbox u v}"] show ?thesis by (simp add: cbe)
qed
qed

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

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

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

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

lemma partial_division_extend:
fixes T :: "'a::euclidean_space set"
assumes "p division_of S"
and "q division_of T"
and "S ⊆ T"
obtains r where "p ⊆ r" and "r division_of T"
proof -
note divp = division_ofD[OF assms(1)] and divq = division_ofD[OF assms(2)]
obtain a b where ab: "T ⊆ cbox a b"
using elementary_subset_cbox[OF assms(2)] by auto
obtain r1 where "p ⊆ r1" "r1 division_of (cbox a b)"
using assms
by (metis ab dual_order.trans partial_division_extend_interval divp(6))
note r1 = this division_ofD[OF this(2)]
obtain p' where "p' division_of ⋃(r1 - p)"
apply (rule elementary_unions_intervals[of "r1 - p"])
using r1(3,6)
apply auto
done
then obtain r2 where r2: "r2 division_of (⋃(r1 - p)) ∩ (⋃q)"
by (metis assms(2) divq(6) elementary_Int)
{
fix x
assume x: "x ∈ T" "x ∉ S"
then obtain R where r: "R ∈ r1" "x ∈ R"
unfolding r1 using ab
by (meson division_contains r1(2) subsetCE)
moreover have "R ∉ p"
proof
assume "R ∈ p"
then have "x ∈ S" using divp(2) r by auto
then show False using x by auto
qed
ultimately have "x∈⋃(r1 - p)" by auto
}
then have Teq: "T = ⋃p ∪ (⋃(r1 - p) ∩ ⋃q)"
unfolding divp divq using assms(3) by auto
have "interior S ∩ interior (⋃(r1-p)) = {}"
proof (rule Int_interior_Union_intervals)
have *: "⋀S. (⋀x. x ∈ S ⟹ False) ⟹ S = {}"
by auto
show "interior S ∩ interior m = {}" if "m ∈ r1 - p" for m
proof -
have "interior m ∩ interior (⋃p) = {}"
proof (rule Int_interior_Union_intervals)
show "⋀T. T∈p ⟹ interior m ∩ interior T = {}"
by (metis DiffD1 DiffD2 that r1(1) r1(7) 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: "k∈Basis"
shows "{l ∩ {x. x∙k ≤ c} | l. l ∈ p ∧ l ∩ {x. x∙k ≤ c} ≠ {}} division_of(cbox a b ∩ {x. x∙k ≤ c})"
(is "?p1 division_of ?I1")
and "{l ∩ {x. x∙k ≥ c} | l. l ∈ p ∧ l ∩ {x. x∙k ≥ c} ≠ {}} division_of (cbox a b ∩ {x. x∙k ≥ c})"
(is "?p2 division_of ?I2")
proof (rule_tac[!] division_ofI)
note p = division_ofD[OF assms(1)]
show "finite ?p1" "finite ?p2"
using p(1) by auto
show "⋃?p1 = ?I1" "⋃?p2 = ?I2"
unfolding p(6)[symmetric] by auto
{
fix K
assume "K ∈ ?p1"
then obtain l where l: "K = l ∩ {x. x ∙ k ≤ c}" "l ∈ p" "l ∩ {x. x ∙ k ≤ c} ≠ {}"
by blast
obtain u v where uv: "l = cbox u v"
using assms(1) l(2) by blast
show "K ⊆ ?I1"
using l p(2) uv by force
show  "K ≠ {}"
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 ≠ {}"
show  "∃a b. K = cbox a b"
apply (simp add: l uv p(2-3)[OF l(2)])
apply (subst interval_split[OF k])
apply (auto intro: order.trans)
done
fix K'
assume "K' ∈ ?p2"
then obtain l' where l': "K' = l' ∩ {x. c ≤ x ∙ k}" "l' ∈ p" "l' ∩ {x. c ≤ x ∙ k} ≠ {}"
by blast
assume "K ≠ K'"
then show "interior K ∩ interior K' = {}"
unfolding l l' using p(5)[OF l(2) l'(2)] by auto
}
qed

subsection ‹Tagged (partial) divisions›

definition✐‹tag 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+

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

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

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

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

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

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

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

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

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

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

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

lemma✐‹tag 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: "(∀x∈s. ∃d::real. 0 < d ∧ q d x) ⟷ (∀x. ∃d>0. x∈s ⟶ q d x)"
by (meson zero_less_one)

paragraph ‹Division points›
text ‹%whitespace›
definition✐‹tag important› "division_points (k::('a::euclidean_space) set) d =
{(j,x). j ∈ Basis ∧ (interval_lowerbound k)∙j < x ∧ x < (interval_upperbound k)∙j ∧
(∃i∈d. (interval_lowerbound i)∙j = x ∨ (interval_upperbound i)∙j = x)}"

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

lemma division_points_subset:
fixes a :: "'a::euclidean_space"
assumes "d division_of (cbox a b)"
and "∀i∈Basis. a∙i < b∙i"  "a∙k < c" "c < b∙k"
and k: "k ∈ Basis"
shows "division_points (cbox a b ∩ {x. x∙k ≤ c}) {l ∩ {x. x∙k ≤ c} | l . l ∈ d ∧ l ∩ {x. x∙k ≤ c} ≠ {}} ⊆
division_points (cbox a b) d" (is ?t1)
and "division_points (cbox a b ∩ {x. x∙k ≥ c}) {l ∩ {x. x∙k ≥ c} | l . l ∈ d ∧ ¬(l ∩ {x. x∙k ≥ c} = {})} ⊆
division_points (cbox a b) d" (is ?t2)
proof -
note assm = division_ofD[OF assms(1)]
have *: "∀i∈Basis. a∙i ≤ b∙i"
"∀i∈Basis. a∙i ≤ (∑i∈Basis. (if i = k then min (b ∙ k) c else  b ∙ i) *⇩R i) ∙ i"
"∀i∈Basis. (∑i∈Basis. (if i = k then max (a ∙ k) c else a ∙ i) *⇩R i) ∙ i ≤ b∙i"
"min (b ∙ k) c = c" "max (a ∙ k) c = c"
using assms using less_imp_le by auto
have "∃i∈d. interval_lowerbound i ∙ x = y ∨ interval_upperbound i ∙ x = y"
if "a ∙ x < y" "y < (if x = k then c else b ∙ x)"
"interval_lowerbound i ∙ x = y ∨ interval_upperbound i ∙ x = y"
"i = l ∩ {x. x ∙ k ≤ c}" "l ∈ d" "l ∩ {x. x ∙ k ≤ c} ≠ {}"
"x ∈ Basis" for i l x y
proof -
obtain u v where l: "l = cbox u v"
using ‹l ∈ d› assms(1) by blast
have *: "∀i∈Basis. u ∙ i ≤ (∑i∈Basis. (if i = k then min (v ∙ k) c else v ∙ i) *⇩R i) ∙ i"
using that(6) unfolding l interval_split[OF k] box_ne_empty that .
have **: "∀i∈Basis. u∙i ≤ v∙i"
using l using that(6) unfolding box_ne_empty[```