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

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
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. 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 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. 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 *
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›

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 ?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 ⟹ ∀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)
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. ⋃{x∈s. 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 (∑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
{
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"
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 "∃k∈p. 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: "∀i∈Basis. 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 "∀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
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 ≠ {} ⟹ ∀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 ∈ 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 (⋂i∈p. ⋃(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. T∈q K - {K} ⟹ interior K ∩ interior T = {}"
using K q(2) qk(5) by auto
show "interior (⋂i∈p. ⋃(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
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 "∀K∈p. ∃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 "∀x∈p. 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 = (⋃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) 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. 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
by (metis Teq div sup_ge1 that)
qed

lemma division_split:
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 ≠ {}"
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"
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 ≠ {}"
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"
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]:
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. 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))"
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. 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
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. 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 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. x∙k ≤ 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. x∙k ≥ c} = K2 ∩ {x. x∙k ≥ c}"
shows "interior (K1 ∩ {x. x∙k ≥ 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"
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 "box a b = {}"
by (metis ‹snd x = snd y› ab assm(5) inf.idem interior_cbox prod.collapse)
then show "d (snd x) = ❙1"
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_set_and: "comm_monoid_set HOL.conj True"

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: "(∀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 ≤ v∙i"
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 < b∙k› by (auto split: if_split_asm)
ultimately show ?t1
unfolding division_points_def interval_split[OF k, of a b]
unfolding interval_bounds[OF *(1)] interval_bounds[OF *(2)] interval_bounds[OF *(3)]
unfolding * by force
have "⋀x y i l. (if x = k then c else a ∙ x) < y ⟹ a ∙ x < y"
using ‹a∙k < c› by (auto split: if_split_asm)
moreover have "∃i∈d. interval_lowerbound i ∙ x = y ∨
interval_upperbound i ∙ x = y"
if "(if x = k then c else a ∙ x) < y" "y < b ∙ x"
"interval_lowerbound i ∙ x = y ∨ interval_upperbound i ∙ x = y"
"i = l ∩ {x. c ≤ x ∙ k}" "l ∈ d" "l ∩ {x. c ≤ x ∙ k} ≠ {}"
"x ∈ Basis" for x y i l
proof -
obtain u v where l: "l = cbox u v"
using ‹l ∈ d› assm(4) by blast
have "∀i∈Basis. u∙i ≤ v∙i"
using l using that(6) unfolding box_ne_empty[symmetric] by auto
then show "∃i∈d. 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: "∀i∈Basis. a∙i < b∙i"  "a∙k < c" "c < b∙k"
and "l ∈ d"
and disj: "interval_lowerbound l∙k = c ∨ interval_upperbound l∙k = c"
and k: "k ∈ Basis"
shows "division_points (cbox a b ∩ {x. x∙k ≤ c}) {l ∩ {x. x∙k ≤ c} | l. l∈d ∧ l ∩ {x. x∙k ≤ c} ≠ {}} ⊂
division_points (cbox a b) d" (is "?D1 ⊂ ?D")
and "division_points (cbox a b ∩ {x. x∙k ≥ c}) {l ∩ {x. x∙k ≥ c} | l. l∈d ∧ l ∩ {x. x∙k ≥ c} ≠ {}} ⊂
division_points (cbox a b) d" (is "?D2 ⊂ ?D")
proof -
have ab: "∀i∈Basis. a∙i ≤ b∙i"
using altb by (auto intro!:less_imp_le)
obtain u v where l: "l = cbox u v"
using d ‹l ∈ d› by blast
have uv: "∀i∈Basis. u∙i ≤ v∙i" "∀i∈Basis. a∙i ≤ u∙i ∧ v∙i ≤ b∙i"
apply (metis assms(5) box_ne_empty(1) cbox_division_memE d l)
by (metis assms(5) box_ne_empty(1) cbox_division_memE d l subset_box(1))
have *: "interval_upperbound (cbox a b ∩ {x. x ∙ k ≤ interval_upperbound l ∙ k}) ∙ k = interval_upperbound l ∙ k"
"interval_upperbound (cbox a b ∩ {x. x ∙ k ≤ interval_lowerbound l ∙ k}) ∙ k = interval_lowerbound l ∙ k"
unfolding l interval_split[OF k] interval_bounds[OF uv(1)]
using uv[rule_format, of k] ab k
by auto
have "∃x. x ∈ ?D - ?D1"
using assms(3-)
unfolding division_points_def interval_bounds[OF ab]
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]
moreover have "?D2 ⊆ ?D"
by (auto simp add: assms division_points_subset)
ultimately show "?D2 ⊂ ?D"
by blast
qed

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

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

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

lemma division_doublesplit:
fixes a :: "'a::euclidean_space"
assumes "p division_of (cbox a b)"
and k: "k ∈ Basis"
shows "(λl. l ∩ {x. ¦x∙k - c¦ ≤ e}) ` {l∈p. l ∩ {x. ¦x∙k - c¦ ≤ e} ≠ {}}
division_of  (cbox a b ∩ {x. ¦x∙k - c¦ ≤ e})"
proof -
have **: "⋀p q p' q'. p division_of q ⟹ p = p' ⟹ q = q' ⟹ p' division_of q'"
by auto```