# Theory Grid_Point

section ‹ Grid Points ›

theory Grid_Point
imports "HOL-Analysis.Multivariate_Analysis"
begin

type_synonym grid_point = "(nat × int) list"

definition lv :: "grid_point ⇒ nat ⇒ nat"
where "lv p d = fst (p ! d)"

definition ix :: "grid_point ⇒ nat ⇒ int"
where "ix p d = snd (p ! d)"

definition level :: "grid_point ⇒ nat"
where "level p = (∑ i < length p. lv p i)"

lemma level_all_eq:
assumes "⋀d. d < length p ⟹ lv p d = lv p' d"
and "length p = length p'"
shows "level p' = level p"
unfolding level_def using assms by auto

datatype dir = left | right

fun sgn :: "dir ⇒ int"
where
"sgn left  = -1"
| "sgn right =  1"

fun inv :: "dir ⇒ dir"
where
"inv left = right"
| "inv right = left"

lemma inv_inv[simp]: "inv (inv dir) = dir"
by (cases dir) simp_all

lemma sgn_inv[simp]: "sgn (inv dir) = - sgn dir"
by (cases dir, auto)

definition child :: "grid_point ⇒ dir ⇒ nat ⇒ grid_point"
where "child p dir d = p[d := (lv p d + 1, 2 * (ix p d) + sgn dir)]"

lemma child_length[simp]: "length (child p dir d) = length p"
unfolding child_def by simp

lemma child_odd[simp]: "d < length p ⟹ odd (ix (child p dir d) d)"
unfolding child_def ix_def by (cases dir, auto)

lemma child_eq: "p ! d = (l, i) ⟹ ∃ j. child p dir d = p[d := (l + 1, j)]"
by (auto simp add: child_def ix_def lv_def)

lemma child_other: "d ≠ d' ⟹ child p dir d ! d' = p ! d'"
unfolding child_def lv_def ix_def by (cases "d' < length p", auto)

lemma child_invariant: assumes "d' < length p" shows "(child p dir d ! d' = p ! d') = (d ≠ d')"
proof -
obtain l i where "p ! d' = (l, i)" using prod.exhaust .
with assms show ?thesis
unfolding child_def ix_def lv_def by auto
qed

lemma child_single_level: "d < length p ⟹ lv (child p dir d) d > lv p d"
unfolding lv_def child_def by simp

lemma child_lv: "d < length p ⟹ lv (child p dir d) d = lv p d + 1"
unfolding child_def lv_def by simp

lemma child_lv_other: assumes "d' ≠ d" shows "lv (child p dir d') d = lv p d"
using child_other[OF assms] unfolding lv_def by simp

lemma child_ix_left: "d < length p ⟹ ix (child p left d) d = 2 * ix p d - 1"
unfolding child_def ix_def by simp

lemma child_ix_right: "d < length p ⟹ ix (child p right d) d = 2 * ix p d + 1"
unfolding child_def ix_def by simp

lemma child_ix: "d < length p ⟹ ix (child p dir d) d = 2 * ix p d + sgn dir"
unfolding child_def ix_def by simp

lemma child_level[simp]: assumes "d < length p"
shows "level (child p dir d) = level p + 1"
proof -
have inter: "{0..<length p} ∩ {d} = {d}" using assms by auto

have "level (child p dir d) =
(∑ d' = 0..<length p. if d' ∈ {d} then lv p d + 1 else lv p d')"
by (auto intro!: sum.cong simp add: child_lv_other child_lv level_def)
moreover have "level p + 1 =
(∑ d' = 0..<length p. if d' ∈ {d} then lv p d else lv p d') + 1"
by (auto intro!: sum.cong simp add: child_lv_other child_lv level_def)
ultimately show ?thesis
unfolding sum.If_cases[OF finite_atLeastLessThan] inter
using assms by auto
qed

lemma child_ex_neighbour: "∃ b'. child b dir d = child b' (inv dir) d"
proof
show "child b dir d = child (b[d := (lv b d, ix b d + sgn dir)]) (inv dir) d"
unfolding child_def ix_def lv_def by (cases "d < length b", auto simp add: algebra_simps)
qed

lemma child_level_gt[simp]: "level (child p dir d) >= level p"
by (cases "d < length p", simp, simp add: child_def)

lemma child_estimate_child:
assumes "d < length p"
and "l ≤ lv p d"
and i'_range: "ix p d < (i + 1) * 2^(lv p d - l) ∧
ix p d > (i - 1) * 2^(lv p d - l)"
(is "?top p ∧ ?bottom p")
and is_child: "p' = child p dir d"
shows "?top p' ∧ ?bottom p'"
proof
from is_child and ‹d < length p›
have "lv p' d = lv p d + 1" by (auto simp add: child_def ix_def lv_def)
hence "lv p' d - l = lv p d - l + 1" using ‹lv p d >= l› by auto
hence pow_l'': "(2^(lv p' d - l) :: int) = 2 * 2^(lv p d - l)" by auto

show "?top p'"
proof -
from is_child and ‹d < length p›
have "ix p' d ≤ 2 * (ix p d) + 1"
by (cases dir, auto simp add: child_def lv_def ix_def)
also have "… < (i + 1) * (2 * 2^(lv p d - l))" using i'_range by auto
finally show ?thesis using pow_l'' by auto
qed

show "?bottom p'"
proof -
have "(i - 1) * 2^(lv p' d - l) = 2 * ((i - 1) * 2^(lv p d - l))"
using pow_l'' by simp
also have "… < 2 * ix p d - 1" using i'_range by auto
finally show ?thesis using is_child and ‹d < length p›
by (cases dir, auto simp add: child_def lv_def ix_def)
qed
qed

lemma child_neighbour: assumes "child p (inv dir) d = child ps dir d" (is "?c_p = ?c_ps")
shows "ps = p[d := (lv p d, ix p d - sgn dir)]" (is "_ = ?ps")
proof (rule nth_equalityI)
have "length ?c_ps = length ?c_p" using ‹?c_p = ?c_ps› by simp
hence len_eq: "length ps = length p" by simp
thus "length ps = length ?ps" by simp

show "ps ! i = ?ps ! i" if "i < length ps" for i
proof -
have "i < length p"
using that len_eq by auto

show "ps ! i = ?ps ! i"
proof (cases "d = i")
case [simp]: True

have "?c_p ! i = ?c_ps ! i" using ‹?c_p = ?c_ps› by auto
hence "ix p i = ix ps d + sgn dir" and "lv p i = lv ps i"
nth_list_update_eq[OF ‹i < length p›]
nth_list_update_eq[OF ‹i < length ps›])
thus ?thesis by (simp add: lv_def ix_def ‹i < length p›)
next
assume "d ≠ i"
with child_other[OF this, of ps dir] child_other[OF this, of p "inv dir"]
show ?thesis using assms by auto
qed
qed
qed

definition start :: "nat ⇒ grid_point"
where
"start dm = replicate dm (0, 1)"

lemma start_lv[simp]: "d < dm ⟹ lv (start dm) d = 0"
unfolding start_def lv_def by simp

lemma start_ix[simp]: "d < dm ⟹ ix (start dm) d = 1"
unfolding start_def ix_def by simp

lemma start_length[simp]: "length (start dm) = dm"
unfolding start_def by auto

lemma level_start_0[simp]: "level (start dm) = 0"
using level_def by auto

end


# Theory Grid

section ‹ Sparse Grids ›

theory Grid
imports Grid_Point
begin

subsection "Vectors"

type_synonym vector = "grid_point ⇒ real"

definition null_vector :: "vector"
where "null_vector ≡ λ p. 0"

definition sum_vector :: "vector ⇒ vector ⇒ vector"
where "sum_vector α β ≡ λ p. α p + β p"

subsection ‹ Inductive enumeration of all grid points ›

inductive_set
grid :: "grid_point ⇒ nat set ⇒ grid_point set"
for b :: "grid_point" and ds :: "nat set"
where
Start[intro!]: "b ∈ grid b ds"
| Child[intro!]: "⟦ p ∈ grid b ds ; d ∈ ds ⟧ ⟹ child p dir d ∈ grid b ds"

lemma grid_length[simp]: "p' ∈ grid p ds ⟹ length p' = length p"
by (erule grid.induct, auto)

lemma grid_union_dims: "⟦ ds ⊆ ds' ; p ∈ grid b ds ⟧ ⟹ p ∈ grid b ds'"
by (erule grid.induct, auto)

lemma grid_transitive: "⟦ a ∈ grid b ds ; b ∈ grid c ds' ; ds' ⊆ ds'' ; ds ⊆ ds'' ⟧ ⟹ a ∈ grid c ds''"
by (erule grid.induct, auto simp add: grid_union_dims)

lemma grid_child[intro?]: assumes "d ∈ ds" and p_grid: "p ∈ grid (child b dir d) ds"
shows "p ∈ grid b ds"
using ‹d ∈ ds› grid_transitive[OF p_grid] by auto

lemma grid_single_level[simp]: assumes "p ∈ grid b ds" and "d < length b"
shows "lv b d ≤ lv p d"
using assms
proof induct
case (Child p' d' dir)
thus ?case by (cases "d' = d", auto simp add: child_def ix_def lv_def)
qed auto

lemma grid_child_level:
assumes "d < length b"
and p_grid: "p ∈ grid (child b dir d) ds"
shows "lv b d < lv p d"
proof -
have "lv b d < lv (child b dir d) d" using child_lv[OF ‹d < length b›] by auto
also have "… ≤ lv p d" using p_grid assms by (intro grid_single_level) auto
finally show ?thesis .
qed

lemma child_out: "length p ≤ d ⟹ child p dir d = p"
unfolding child_def by auto

lemma grid_dim_remove:
assumes inset: "p ∈ grid b ({d} ∪ ds)"
and eq: "d < length b ⟹ p ! d = b ! d"
shows "p ∈ grid b ds"
using inset eq
proof induct
case (Child p' d' dir)
show ?case
proof (cases "d' ≥ length p'")
case True with child_out[OF this]
show ?thesis using Child by auto
next
case False hence "d' < length p'" by simp
show ?thesis
proof (cases "d' = d")
case True
hence "lv b d ≤ lv p' d" and "lv p' d < lv (child p' dir d) d"
using child_single_level Child ‹d' < length p'› by auto
hence False using Child and ‹d' = d› and lv_def and ‹¬ d' ≥ length p'› by auto
thus ?thesis ..
next
case False
hence "d' ∈ ds" using Child by auto
moreover have "d < length b ⟹ p' ! d = b ! d"
proof -
assume "d < length b"
hence "d < length p'" using Child by auto
hence "child p' dir d' ! d = p' ! d" using child_invariant and False by auto
thus ?thesis using Child and ‹d < length b› by auto
qed
hence "p' ∈ grid b ds" using Child by auto
ultimately show ?thesis using grid.Child by auto
qed
qed
qed auto

lemma gridgen_dim_restrict:
assumes inset: "p ∈ grid b (ds' ∪ ds)"
and eq: "∀ d ∈ ds'. d ≥ length b"
shows "p ∈ grid b ds"
using inset eq
proof induct
case (Child p' d dir)
thus ?case
proof (cases "d ∈ ds")
case False thus ?thesis using Child and child_def by auto
qed auto
qed auto

lemma grid_dim_remove_outer: "grid b ds = grid b {d ∈ ds. d < length b}"
proof
have "{d ∈ ds. d < length b} ⊆ ds" by auto
from grid_union_dims[OF this]
show "grid b {d ∈ ds. d < length b} ⊆ grid b ds" by auto

have "ds = (ds - {d ∈ ds. d < length b}) ∪ {d ∈ ds. d < length b}" by auto
moreover
have "grid b ((ds - {d ∈ ds. d < length b}) ∪ {d ∈ ds. d < length b}) ⊆ grid b {d ∈ ds. d < length b}"
proof
fix p
assume "p ∈ grid b (ds - {d ∈ ds. d < length b} ∪ {d ∈ ds. d < length b})"
moreover have "∀ d ∈ (ds - {d ∈ ds. d < length b}). d ≥ length b" by auto
ultimately show "p ∈ grid b {d ∈ ds. d < length b}" by (rule gridgen_dim_restrict)
qed
ultimately show "grid b ds ⊆ grid b {d ∈ ds. d < length b}" by auto
qed

lemma grid_level[intro]: assumes "p ∈ grid b ds" shows "level b ≤ level p"
proof -
have *: "length p = length b" using grid_length assms by auto
{ fix i assume "i ∈ {0 ..< length p}"
hence "lv b i ≤ lv p i" using ‹p ∈ grid b ds› and grid_single_level * by auto
} thus ?thesis unfolding level_def * by (auto intro!: sum_mono)
qed
lemma grid_empty_ds[simp]: "grid b {} = { b }"
proof -
have "!! z. z ∈ grid b {} ⟹ z = b"
by (erule grid.induct, auto)
thus ?thesis by auto
qed
lemma grid_Start: assumes inset: "p ∈ grid b ds" and eq: "level p = level b" shows "p = b"
using inset eq
proof induct
case (Child p d dir)
show ?case
proof (cases "d < length b")
case True
from Child
have "level p ≥ level b" by auto
moreover
have "level p ≤ level (child p dir d)" by (rule child_level_gt)
hence "level p ≤ level b" using Child by auto
ultimately have "level p = level b" by auto
hence "p = b " using Child(2) by auto
with Child(4) have "level (child b dir d) = level b" by auto
moreover have "level (child b dir d) ≠  level b" using child_level and ‹d < length b› by auto
ultimately show ?thesis by auto
next
case False
with Child have "length p = length b" by auto
with False have "child p dir d = p" using child_def by auto
moreover with Child have "level p = level b" by auto
with Child(2) have "p = b" by auto
ultimately show ?thesis by auto
qed
qed auto
lemma grid_estimate:
assumes "d < length b" and p_grid: "p ∈ grid b ds"
shows "ix p d < (ix b d + 1) * 2^(lv p d - lv b d) ∧ ix p d > (ix b d - 1) * 2^(lv p d - lv b d)"
using p_grid
proof induct
case (Child p d' dir)
show ?case
proof (cases "d = d'")
case False with Child show ?thesis unfolding child_def lv_def ix_def by auto
next
case True with child_estimate_child and Child and ‹d < length b›
show ?thesis using grid_single_level by auto
qed
qed auto
lemma grid_odd: assumes "d < length b" and p_diff: "p ! d ≠ b ! d" and p_grid: "p ∈ grid b ds"
shows "odd (ix p d)"
using p_grid and p_diff
proof induct
case (Child p d' dir)
show ?case
proof (cases "d = d'")
case True with child_odd and ‹d < length b› and Child show ?thesis by auto
next
case False with Child and ‹d < length b› show ?thesis using child_def and ix_def and lv_def by auto
qed
qed auto
lemma grid_invariant: assumes "d < length b" and "d ∉ ds" and p_grid: "p ∈ grid b ds"
shows "p ! d = b ! d"
using p_grid
proof (induct)
case (Child p d' dir) hence "d' ≠ d" using ‹d ∉ ds› by auto
thus ?case using child_def and Child by auto
qed auto
lemma grid_part: assumes "d < length b" and p_valid: "p ∈ grid b {d}" and p'_valid: "p' ∈ grid b {d}"
and level: "lv p' d ≥ lv p d"
and right: "ix p' d ≤ (ix p d + 1) * 2^(lv p' d - lv p d)" (is "?right p p' d")
and left: "ix p' d ≥ (ix p d - 1) * 2^(lv p' d - lv p d)" (is "?left p p' d")
shows "p' ∈ grid p {d}"
using p'_valid left right level and p_valid
proof induct
case (Child p' d' dir)
hence "d = d'" by auto
let ?child = "child p' dir d'"

show ?case
proof (cases "lv p d = lv ?child d")
case False
moreover have "lv ?child d = lv p' d + 1" using child_lv and ‹d < length b› and Child and ‹d = d'› by auto
ultimately have "lv p d < lv p' d + 1" using Child by auto
hence lv: "Suc (lv p' d) - lv p d = Suc (lv p' d - lv p d)" by auto

have "?left p p' d ∧ ?right p p' d"
proof (cases dir)
case left
with Child have "2 * ix p' d - 1 ≤ (ix p d + 1) * 2^(Suc (lv p' d) - lv p d)"
using ‹d = d'› and ‹d < length b› by (auto simp add: child_def ix_def lv_def)
also have "… = 2 * (ix p d + 1) * 2^(lv p' d - lv p d)" using lv by auto
finally have "2 * ix p' d - 2 < 2 * (ix p d + 1) * 2^(lv p' d - lv p d)" by auto
also have "… = 2 * ((ix p d + 1) * 2^(lv p' d - lv p d))" by auto
finally have left_r: "ix p' d ≤ (ix p d + 1) * 2^(lv p' d - lv p d)" by auto

have "2 * ((ix p d - 1) * 2^(lv p' d - lv p d)) = 2 * (ix p d - 1) * 2^(lv p' d - lv p d)" by auto
also have "… = (ix p d - 1) * 2^(Suc (lv p' d) - lv p d)" using lv by auto
also have "… ≤ 2 * ix p' d - 1"
using left and Child and ‹d = d'› and ‹d < length b› by (auto simp add: child_def ix_def lv_def)
finally have right_r: "((ix p d - 1) * 2^(lv p' d - lv p d)) ≤ ix p' d" by auto

show ?thesis using left_r and right_r by auto
next
case right
with Child have "2 * ix p' d + 1 ≤ (ix p d + 1) * 2^(Suc (lv p' d) - lv p d)"
using ‹d = d'› and ‹d < length b› by (auto simp add: child_def ix_def lv_def)
also have "… = 2 * (ix p d + 1) * 2^(lv p' d - lv p d)" using lv by auto
finally have "2 * ix p' d < 2 * (ix p d + 1) * 2^(lv p' d - lv p d)" by auto
also have "… = 2 * ((ix p d + 1) * 2^(lv p' d - lv p d))" by auto
finally have left_r: "ix p' d ≤ (ix p d + 1) * 2^(lv p' d - lv p d)" by auto

have "2 * ((ix p d - 1) * 2^(lv p' d - lv p d)) = 2 * (ix p d - 1) * 2^(lv p' d - lv p d)" by auto
also have "… = (ix p d - 1) * 2^(Suc (lv p' d) - lv p d)" using lv by auto
also have "… ≤ 2 * ix p' d + 1"
using right and Child and ‹d = d'› and ‹d < length b› by (auto simp add: child_def ix_def lv_def)
also have "… < 2 * (ix p' d + 1)" by auto
finally have right_r: "((ix p d - 1) * 2^(lv p' d - lv p d)) ≤ ix p' d" by auto

show ?thesis using left_r and right_r by auto
qed
with Child and lv have "p' ∈ grid p {d}" by auto
thus ?thesis using ‹d = d'› by auto
next
case True
moreover with Child have "?left p ?child d ∧ ?right p ?child d" by auto
ultimately have range: "ix p d - 1 ≤ ix ?child d ∧ ix ?child d ≤ ix p d + 1" by auto

have "p ! d ≠ b ! d"
proof (rule ccontr)
assume "¬ (p ! d ≠ b ! d)"
with ‹lv p d = lv ?child d› have "lv b d = lv ?child d" by (auto simp add: lv_def)
hence "lv b d = lv p' d + 1" using ‹d = d'› and Child and ‹d < length b› and child_lv by auto
moreover have "lv b d ≤ lv p' d" using ‹d = d'› and Child and ‹d < length b› and grid_single_level by auto
ultimately show False by auto
qed
hence "odd (ix p d)" using grid_odd and ‹p ∈ grid b {d}› and ‹d < length b› by auto
hence "¬ odd (ix p d + 1)" and "¬ odd (ix p d - 1)" by auto

have "d < length p'" using ‹p' ∈ grid b {d}› and ‹d < length b› by auto
hence odd_child: "odd (ix ?child d)" using child_odd and ‹d = d'› by auto

have "ix p d - 1 ≠ ix ?child d"
proof (rule ccontr)
assume "¬ (ix p d - 1 ≠ ix ?child d)"
hence "odd (ix p d - 1)" using odd_child by auto
thus False using ‹¬ odd (ix p d - 1)› by auto
qed
moreover
have "ix p d + 1 ≠ ix ?child d"
proof (rule ccontr)
assume "¬ (ix p d + 1 ≠ ix ?child d)"
hence "odd (ix p d + 1)" using odd_child by auto
thus False using ‹¬ odd (ix p d + 1)› by auto
qed
ultimately have "ix p d = ix ?child d" using range by auto
with True have d_eq: "p ! d = (?child) ! d" by (auto simp add: prod_eqI ix_def lv_def)

have "length p = length ?child" using ‹p ∈ grid b {d}› and ‹p' ∈ grid b {d}› by auto
moreover have "p ! d'' = ?child ! d''" if "d'' < length p" for d''
proof -
have "d'' < length b" using that ‹p ∈ grid b {d}› by auto
show "p ! d'' = ?child ! d''"
proof (cases "d = d''")
case True with d_eq show ?thesis by auto
next
case False hence "d'' ∉ {d}" by auto
from ‹d'' < length b› and this and ‹p ∈ grid b {d}›
have "p ! d'' = b ! d''" by (rule grid_invariant)
also have "… = p' ! d''" using ‹d'' < length b› and ‹d'' ∉ {d}› and ‹p' ∈ grid b {d}›
by (rule grid_invariant[symmetric])
also have "… = ?child ! d''"
proof -
have "d'' < length p'" using ‹d'' < length b› and ‹p' ∈ grid b {d}› by auto
hence "?child ! d'' = p' ! d''" using child_invariant and ‹d ≠ d''› and ‹d = d'› by auto
thus ?thesis by auto
qed
finally show ?thesis .
qed
qed
ultimately have "p = ?child" by (rule nth_equalityI)
thus "?child ∈ grid p {d}" by auto
qed
next
case Start
moreover hence "lv b d ≤ lv p d" using grid_single_level and ‹d < length b› by auto
ultimately have "lv b d = lv p d" by auto

have "level p = level b"
proof -
{ fix d'
assume "d' < length b"
have "lv b d' = lv p d'"
proof (cases "d = d'")
case True with ‹lv b d = lv p d› show ?thesis by auto
next
case False hence "d' ∉ {d}" by auto
from ‹d' < length b› and this and ‹p ∈ grid b {d}›
have "p ! d' = b ! d'" by (rule grid_invariant)
thus ?thesis by (auto simp add: lv_def)
qed }
moreover have "length b = length p" using ‹p ∈ grid b {d}› by auto
ultimately show ?thesis by (rule level_all_eq)
qed
hence "p = b" using grid_Start and ‹p ∈ grid b {d}› by auto
thus ?case by auto
qed
lemma grid_disjunct: assumes "d < length p"
shows "grid (child p left d) ds ∩ grid (child p right d) ds = {}"
(is "grid ?l ds ∩ grid ?r ds = {}")
proof (intro set_eqI iffI)
fix x
assume "x ∈ grid ?l ds ∩ grid ?r ds"
hence "ix x d < (ix ?l d + 1) * 2^(lv x d - lv ?l d)"
and "ix x d > (ix ?r d - 1) * 2^(lv x d - lv ?r d)"
using grid_estimate ‹d < length p› by auto
thus "x ∈ {}" using ‹d < length p› and child_lv and child_ix by auto
qed auto

lemma grid_level_eq: assumes eq: "∀ d ∈ ds. lv p d = lv b d" and grid: "p ∈ grid b ds"
shows "level p = level b"
proof (rule level_all_eq)
{ fix i assume "i < length b"
show "lv b i = lv p i"
proof (cases "i ∈ ds")
case True with eq show ?thesis by auto
next case False with ‹i < length b› and grid show ?thesis
using lv_def ix_def grid_invariant by auto
qed }
show "length b = length p" using grid by auto
qed

lemma grid_partition:
"grid p {d} = {p} ∪ grid (child p left d) {d} ∪ grid (child p right d) {d}"
(is "_ = _ ∪ grid ?l {d} ∪ grid ?r {d}")
proof -
have "!! x. ⟦ x ∈ grid p {d} ; x ≠ p ; x ∉ grid ?r {d} ⟧ ⟹ x ∈ grid ?l {d}"
proof (cases "d < length p")
case True
fix x

let "?nr_r p" = "ix x d > (ix p d + 1) * 2 ^ (lv x d - lv p d)"
let "?nr_l p" = "(ix p d - 1) * 2 ^ (lv x d - lv p d) > ix x d"

have ix_r_eq: "ix ?r d = 2 * ix p d + 1" using ‹d < length p› and child_ix by auto
have lv_r_eq: "lv ?r d = lv p d + 1" using ‹d < length p› and child_lv by auto

have ix_l_eq: "ix ?l d = 2 * ix p d - 1" using ‹d < length p› and child_ix by auto
have lv_l_eq: "lv ?l d = lv p d + 1" using ‹d < length p› and child_lv by auto

assume "x ∈ grid p {d}" and "x ≠ p" and "x ∉ grid ?r {d}"
hence "lv p d ≤ lv x d" using grid_single_level and ‹d < length p› by auto
moreover have "lv p d ≠ lv x d"
proof (rule ccontr)
assume "¬ lv p d ≠ lv x d"
hence "level x = level p" using ‹x ∈ grid p {d}› and grid_level_eq[where ds="{d}"] by auto
hence "x = p" using grid_Start and ‹x ∈ grid p {d}› by auto
thus False using ‹x ≠ p› by auto
qed
ultimately have "lv p d < lv x d" by auto
hence "lv ?r d ≤ lv x d" and "?r ∈ grid p {d}" using child_lv and ‹d < length p› by auto
with ‹d < length p› and ‹x ∈ grid p {d}›
have r_range: "¬ ?nr_r ?r ∧ ¬ ?nr_l ?r ⟹ x ∈ grid ?r {d}"
using grid_part[where p="?r" and p'=x and b=p and d=d] by auto
have "x ∉ grid ?r {d} ⟹ ?nr_l ?r ∨ ?nr_r ?r" by (rule ccontr, auto simp add: r_range)
hence "?nr_l ?r ∨ ?nr_r ?r" using ‹x ∉ grid ?r {d}› by auto

have gt0: "lv x d - lv p d > 0" using ‹lv p d < lv x d› by auto

have ix_shift: "ix ?r d = ix ?l d + 2" and lv_lr: "lv ?r d = lv ?l d" and right1: "!! x :: int. x + 2 - 1 = x + 1"
using ‹d < length p› and child_ix and child_lv by auto

have "lv x d - lv p d = Suc (lv x d - (lv p d + 1))"
using gt0 by auto
hence lv_shift: "!! y :: int. y * 2 ^ (lv x d - lv p d) = y * 2 * 2 ^ (lv x d - (lv p d + 1))"
by auto

have "ix x d < (ix p d + 1) * 2 ^ (lv x d - lv p d)"
using ‹x ∈ grid p {d}› grid_estimate and ‹d < length p› by auto
also have "… = (ix ?r d + 1) * 2 ^ (lv x d - lv ?r d)"
using ‹lv p d < lv x d› and ix_r_eq and lv_r_eq lv_shift[where y="ix p d + 1"] by auto
finally have "?nr_l ?r" using ‹?nr_l ?r ∨ ?nr_r ?r› by auto
hence r_bound: "(ix ?l d + 1) * 2 ^ (lv x d - lv ?l d) > ix x d"
unfolding ix_shift lv_lr using right1 by auto

have "(ix ?l d - 1) * 2 ^ (lv x d - lv ?l d) = (ix p d - 1) * 2 * 2 ^ (lv x d - (lv p d + 1))"
unfolding ix_l_eq lv_l_eq by auto
also have "… = (ix p d - 1) * 2 ^ (lv x d - lv p d)"
using lv_shift[where y="ix p d - 1"] by auto
also have " … < ix x d"
using ‹x ∈ grid p {d}› grid_estimate and ‹d < length p› by auto
finally have l_bound: "(ix ?l d - 1) * 2 ^ (lv x d - lv ?l d) < ix x d" .

from l_bound r_bound ‹d < length p› and ‹x ∈ grid p {d}› ‹lv ?r d ≤ lv x d› and lv_lr
show "x ∈ grid ?l {d}" using grid_part[where p="?l" and p'=x and d=d] by auto
thus ?thesis by (auto intro: grid_child)
qed
lemma grid_change_dim: assumes grid: "p ∈ grid b ds"
shows "p[d := X] ∈ grid (b[d := X]) ds"
using grid
proof induct
case (Child p d' dir)
show ?case
proof (cases "d ≠ d'")
case True
have "(child p dir d')[d := X] = child (p[d := X]) dir d'"
unfolding child_def and ix_def and lv_def
unfolding list_update_swap[OF ‹d ≠ d'›] and nth_list_update_neq[OF ‹d ≠ d'›] ..
thus ?thesis using Child by auto
next
case False hence "d = d'" by auto
with Child show ?thesis unfolding child_def ‹d = d'› list_update_overwrite by auto
qed
qed auto
lemma grid_change_dim_child: assumes grid: "p ∈ grid b ds" and "d ∉ ds"
shows "child p dir d ∈ grid (child b dir d) ds"
proof (cases "d < length b")
case True thus ?thesis using grid_change_dim[OF grid]
unfolding child_def lv_def ix_def grid_invariant[OF True ‹d ∉ ds› grid] by auto
next
case False hence "length b ≤ d" and "length p ≤ d" using grid by auto
thus ?thesis unfolding child_def using list_update_beyond assms by auto
qed
lemma grid_split: assumes grid: "p ∈ grid b (ds' ∪ ds)" shows "∃ x ∈ grid b ds. p ∈ grid x ds'"
using grid
proof induct
case (Child p d dir)
show ?case
proof (cases "d ∈ ds'")
case True with Child show ?thesis by auto
next
case False
hence "d ∈ ds" using Child by auto
obtain x where "x ∈ grid b ds" and "p ∈ grid x ds'" using Child by auto
hence "child x dir d ∈ grid b ds" using ‹d ∈ ds› by auto
moreover have "child p dir d ∈ grid (child x dir d) ds'"
using ‹p ∈ grid x ds'› False and grid_change_dim_child by auto
ultimately show ?thesis by auto
qed
qed auto
lemma grid_union_eq: "(⋃ p ∈ grid b ds. grid p ds') = grid b (ds' ∪ ds)"
using grid_split and grid_transitive[where ds''="ds' ∪ ds" and ds=ds' and ds'=ds, OF _ _ Un_upper2 Un_upper1] by auto
lemma grid_onedim_split:
"grid b (ds ∪ {d}) = grid b ds ∪ grid (child b left d) (ds ∪ {d}) ∪ grid (child b right d) (ds ∪ {d})"
(is "_ = ?g ∪ ?l (ds ∪ {d}) ∪ ?r (ds ∪ {d})")
proof -
have "?g ∪ ?l (ds ∪ {d}) ∪ ?r (ds ∪ {d}) = ?g ∪ (⋃ p ∈ ?l {d}. grid p ds) ∪ (⋃ p ∈ ?r {d}. grid p ds)"
unfolding grid_union_eq ..
also have "… = (⋃ p ∈ ({b} ∪ ?l {d} ∪ ?r {d}). grid p ds)" by auto
also have "… = (⋃ p ∈ grid b {d}. grid p ds)" unfolding grid_partition[where p=b] ..
finally show ?thesis unfolding grid_union_eq by auto
qed
lemma grid_child_without_parent: assumes grid: "p ∈ grid (child b dir d) ds" (is "p ∈ grid ?c ds") and "d < length b"
shows "p ≠ b"
proof -
have "level ?c ≤ level p" using grid by (rule grid_level)
hence "level b < level p" using child_level and ‹d < length b› by auto
thus ?thesis by auto
qed
lemma grid_disjunct':
assumes "p ∈ grid b ds" and "p' ∈ grid b ds" and "x ∈ grid p ds'" and "p ≠ p'" and "ds ∩ ds' = {}"
shows "x ∉ grid p' ds'"
proof (rule ccontr)
assume "¬ x ∉ grid p' ds'" hence "x ∈ grid p' ds'" by auto
have l: "length b = length p" and l': "length b = length p'" using ‹p ∈ grid b ds› and ‹p' ∈ grid b ds› by auto
hence "length p' = length p" by auto
moreover have "∀ d < length p'. p' ! d = p ! d"
proof (rule allI, rule impI)
fix d assume dl': "d < length p'" hence "d < length b" using l' by auto
hence dl: "d < length p" using l by auto
show "p' ! d = p ! d"
proof (cases "d ∈ ds'")
case True with ‹ds ∩ ds' = {}› have "d ∉ ds" by auto
hence "p' ! d = b ! d" and "p ! d = b ! d"
using ‹d < length b› ‹p' ∈ grid b ds› and ‹p ∈ grid b ds› and grid_invariant by auto
thus ?thesis by auto
next
case False
show ?thesis
using grid_invariant[OF dl' False ‹x ∈ grid p' ds'›]
and grid_invariant[OF dl False ‹x ∈ grid p ds'›] by auto
qed
qed
ultimately have "p' = p" by (metis nth_equalityI)
thus False using ‹p ≠ p'› by auto
qed
lemma grid_split1: assumes grid: "p ∈ grid b (ds' ∪ ds)" and "ds ∩ ds' = {}"
shows "∃! x ∈ grid b ds. p ∈ grid x ds'"
proof (rule ex_ex1I)
obtain x where "x ∈ grid b ds" and "p ∈ grid x ds'" using grid_split[OF grid] by auto
thus "∃ x. x ∈ grid b ds ∧ p ∈ grid x ds'" by auto
next
fix x y
assume "x ∈ grid b ds ∧ p ∈ grid x ds'" and "y ∈ grid b ds ∧ p ∈ grid y ds'"
hence "x ∈ grid b ds" and "p ∈ grid x ds'" and "y ∈ grid b ds" and "p ∈ grid y ds'" by auto
show "x = y"
proof (rule ccontr)
assume "x ≠ y"
from grid_disjunct'[OF ‹x ∈ grid b ds› ‹y ∈ grid b ds› ‹p ∈ grid x ds'› this ‹ds ∩ ds' = {}›]
show False using ‹p ∈ grid y ds'› by auto
qed
qed

subsection ‹ Grid Restricted to a Level ›

definition lgrid :: "grid_point ⇒ nat set ⇒ nat ⇒ grid_point set"
where "lgrid b ds lm = { p ∈ grid b ds. level p < lm }"

lemma lgridI[intro]:
"⟦ p ∈ grid b ds ; level p < lm ⟧ ⟹ p ∈ lgrid b ds lm"
unfolding lgrid_def by simp

lemma lgridE[elim]:
assumes "p ∈ lgrid b ds lm"
assumes "⟦ p ∈ grid b ds ; level p < lm ⟧ ⟹ P"
shows P
using assms unfolding lgrid_def by auto

lemma lgridI_child[intro]:
"d ∈ ds ⟹ p ∈ lgrid (child b dir d) ds lm ⟹ p ∈ lgrid b ds lm"
by (auto intro: grid_child)

lemma lgrid_empty[simp]: "lgrid p ds (level p) = {}"
proof (rule equals0I)
fix p' assume "p' ∈ lgrid p ds (level p)"
hence "level p' < level p" and "level p ≤ level p'" by auto
thus False by auto
qed

lemma lgrid_empty': assumes "lm ≤ level p" shows "lgrid p ds lm = {}"
proof (rule equals0I)
fix p' assume "p' ∈ lgrid p ds lm"
hence "level p' < lm" and "level p ≤ level p'" by auto
thus False using ‹lm ≤ level p› by auto
qed

lemma grid_not_child:
assumes [simp]: "d < length p"
shows "p ∉ grid (child p dir d) ds"
proof (rule ccontr)
assume "¬ ?thesis"
have "level p < level (child p dir d)" by auto
with grid_level[OF ‹¬ ?thesis›[unfolded not_not]]
show False by auto
qed

subsection ‹ Unbounded Sparse Grid ›

definition sparsegrid' :: "nat ⇒ grid_point set"
where
"sparsegrid' dm = grid (start dm) { 0 ..< dm }"

lemma grid_subset_alldim:
assumes p: "p ∈ grid b ds"
defines "dm ≡ length b"
shows "p ∈ grid b {0..<dm}"
proof -
have "ds ∩ {dm..} ∪ ds ∩ {0..<dm} = ds" by auto
from gridgen_dim_restrict[where ds="ds ∩ {0..<dm}" and ds'="ds ∩ {dm..}"] this
have "ds ∩ {0..<dm} ⊆ {0..<dm}"
and "p ∈ grid b (ds ∩ {0..<dm})" using p unfolding dm_def by auto
thus ?thesis by (rule grid_union_dims)
qed

lemma sparsegrid'_length[simp]:
"b ∈ sparsegrid' dm ⟹ length b = dm" unfolding sparsegrid'_def by auto

lemma sparsegrid'I[intro]:
assumes b: "b ∈ sparsegrid' dm" and p: "p ∈ grid b ds"
shows "p ∈ sparsegrid' dm"
using sparsegrid'_length[OF b] b
grid_transitive[OF grid_subset_alldim[OF p], where c="start dm" and ds''="{0..<dm}"]
unfolding sparsegrid'_def by auto

lemma sparsegrid'_start:
assumes "b ∈ grid (start dm) ds"
shows "b ∈ sparsegrid' dm"
unfolding sparsegrid'_def
using grid_subset_alldim[OF assms] by simp

subsection ‹ Sparse Grid ›

definition sparsegrid :: "nat ⇒ nat ⇒ grid_point set"
where
"sparsegrid dm lm = lgrid (start dm) { 0 ..< dm } lm"

lemma sparsegrid_length: "p ∈ sparsegrid dm lm ⟹ length p = dm"
by (auto simp: sparsegrid_def)

lemma sparsegrid_subset[intro]: "p ∈ sparsegrid dm lm ⟹ p ∈ sparsegrid' dm"
unfolding sparsegrid_def sparsegrid'_def lgrid_def by auto

lemma sparsegridI[intro]:
assumes "p ∈ sparsegrid' dm" and "level p < lm"
shows "p ∈ sparsegrid dm lm"
using assms unfolding sparsegrid'_def sparsegrid_def lgrid_def by auto

lemma sparsegrid_start:
assumes "b ∈ lgrid (start dm) ds lm"
shows "b ∈ sparsegrid dm lm"
proof
have "b ∈ grid (start dm) ds" using assms by auto
thus "b ∈ sparsegrid' dm" by (rule sparsegrid'_start)
qed (insert assms, auto)

lemma sparsegridE[elim]:
assumes "p ∈ sparsegrid dm lm"
shows "p ∈ sparsegrid' dm" and "level p < lm"
using assms unfolding sparsegrid'_def sparsegrid_def lgrid_def by auto

subsection ‹ Compute Sparse Grid Points ›

fun gridgen :: "grid_point ⇒ nat set ⇒ nat ⇒ grid_point list"
where
"gridgen p ds 0 = []"
| "gridgen p ds (Suc l) = (let
sub = λ d. gridgen (child p left d) { d' ∈ ds . d' ≤ d } l @
gridgen (child p right d) { d' ∈ ds . d' ≤ d } l
in p # concat (map sub [ d ← [0 ..< length p]. d ∈ ds]))"

lemma gridgen_lgrid_eq: "set (gridgen p ds l) = lgrid p ds (level p + l)"
proof (induct l arbitrary: p ds)
case (Suc l)
let "?subg dir d" = "set (gridgen (child p dir d) { d' ∈ ds . d' ≤  d } l)"
let "?sub dir d" = "lgrid (child p dir d) { d' ∈ ds . d' ≤  d } (level p + Suc l)"
let "?union F dm" = "{p} ∪ (⋃ d ∈ { d ∈ ds. d < dm }. F left d ∪ F right d)"

have hyp: "!! dir d. d < length p ⟹ ?subg dir d = ?sub dir d"
using Suc.hyps using child_level by auto

{ fix dm assume "dm ≤ length p"
hence "?union ?sub dm = lgrid p {d ∈ ds. d < dm} (level p + Suc l)"
proof (induct dm)
case (Suc dm)
hence "dm ≤ length p" by auto

let ?l = "child p left dm" and ?r = "child p right dm"

have p_lgrid: "p ∈ lgrid p {d ∈ ds. d < dm} (level p + Suc l)" by auto

show ?case
proof (cases "dm ∈ ds")
case True
let ?ds = "{d ∈ ds. d < dm} ∪ {dm}"
have ds_eq: "{d' ∈ ds. d' ≤ dm} = ?ds" using True by auto
have ds_eq': "{d ∈ ds. d < Suc dm} = {d ∈ ds. d < dm } ∪ {dm}" using True by auto

have "?union ?sub (Suc dm) = ?union ?sub dm ∪ ({p} ∪ ?sub left dm ∪ ?sub right dm)"
unfolding ds_eq' by auto
also have "… = lgrid p {d ∈ ds. d < dm} (level p + Suc l) ∪ ?sub left dm ∪ ?sub right dm"
unfolding Suc.hyps[OF ‹dm ≤ length p›] using p_lgrid by auto
also have "… = {p' ∈ grid p {d ∈ ds. d<dm} ∪ (grid ?l ?ds) ∪ (grid ?r ?ds).
level p' < level p + Suc l}" unfolding lgrid_def ds_eq by auto
also have "… = lgrid p {d ∈ ds. d < Suc dm} (level p + Suc l)"
unfolding lgrid_def ds_eq' unfolding grid_onedim_split[where b=p] ..
finally show ?thesis .
next
case False hence "{d ∈ ds. d < Suc dm} = {d ∈ ds. d < dm ∨ d = dm}" by auto
hence ds_eq: "{d ∈ ds. d < Suc dm} = {d ∈ ds. d < dm}" using ‹dm ∉ ds› by auto
show ?thesis unfolding ds_eq Suc.hyps[OF ‹dm ≤ length p›] ..
qed
next case 0 thus ?case unfolding lgrid_def by auto
qed }
hence "?union ?sub (length p) = lgrid p {d ∈ ds. d < length p} (level p + Suc l)" by auto
hence union_lgrid_eq: "?union ?sub (length p) = lgrid p ds (level p + Suc l)"
unfolding lgrid_def using grid_dim_remove_outer by auto

have "set (gridgen p ds (Suc l)) = ?union ?subg (length p)"
unfolding gridgen.simps and Let_def by auto
hence "set (gridgen p ds (Suc l)) = ?union ?sub (length p)"
using hyp by auto
also have "… = lgrid p ds (level p + Suc l)"
using union_lgrid_eq .
finally show ?case .
qed auto

lemma gridgen_distinct: "distinct (gridgen p ds l)"
proof (induct l arbitrary: p ds)
case (Suc l)
let ?ds = "[d ← [0..<length p]. d ∈ ds]"
let "?left d" = "gridgen (child p left d) { d' ∈ ds . d' ≤ d } l"
and "?right d" = "gridgen (child p right d) { d' ∈ ds . d' ≤ d } l"
let "?sub d" = "?left d @ ?right d"

have "distinct (concat (map ?sub ?ds))"
proof (cases l)
case (Suc l')

have inj_on: "inj_on ?sub (set ?ds)"
proof (rule inj_onI, rule ccontr)
fix d d' assume "d ∈ set ?ds" and "d' ∈ set ?ds"
hence "d < length p" and "d ∈ set ?ds" and "d' < length p" by auto
assume *: "?sub d = ?sub d'"
have in_d: "child p left d ∈ set (?sub d)"
using ‹d ∈ set ?ds› Suc
by (auto simp add: gridgen_lgrid_eq lgrid_def grid_Start)

have in_d': "child p left d' ∈ set (?sub d')"
using ‹d ∈ set ?ds› Suc
by (auto simp add: gridgen_lgrid_eq lgrid_def grid_Start)

{ fix p' d assume "d ∈ set ?ds" and "p' ∈ set (?sub d)"
hence "lv p d < lv p' d"
using grid_child_level
by (auto simp add: gridgen_lgrid_eq lgrid_def grid_child_level) }
note level_less = this

assume "d ≠ d'"
show False
proof (cases "d' < d")
case True
with in_d' ‹?sub d = ?sub d'› level_less[OF ‹d ∈ set ?ds›]
have "lv p d < lv (child p left d') d" by simp
thus False unfolding lv_def
using child_invariant[OF ‹d < length p›, of left d'] ‹d ≠ d'›
by auto
next
case False hence "d < d'" using ‹d ≠ d'› by auto
with in_d ‹?sub d = ?sub d'› level_less[OF ‹d' ∈ set ?ds›]
have "lv p d' < lv (child p left d) d'" by simp
thus False unfolding lv_def
using child_invariant[OF ‹d' < length p›, of left d] ‹d ≠ d'›
by auto
qed
qed

show ?thesis
proof (rule distinct_concat)
show "distinct (map ?sub ?ds)"
unfolding distinct_map using inj_on by simp
next
fix ys assume "ys ∈ set (map ?sub ?ds)"
then obtain d where "d ∈ ds" and "d < length p"
and *: "ys = ?sub d" by auto

show "distinct ys" unfolding *
using grid_disjunct[OF ‹d < length p›, of "{d' ∈ ds. d' ≤ d}"]
gridgen_lgrid_eq lgrid_def ‹distinct (?left d)› ‹distinct (?right d)›
by auto
next
fix ys zs
assume "ys ∈ set (map ?sub ?ds)"
then obtain d where ys: "ys = ?sub d" and "d ∈ set ?ds" by auto
hence "d < length p" by auto

assume "zs ∈ set (map ?sub ?ds)"
then obtain d' where zs: "zs = ?sub d'" and "d' ∈ set ?ds" by auto
hence "d' < length p" by auto

assume "ys ≠ zs"
hence "d' ≠ d" unfolding ys zs by auto

show "set ys ∩ set zs = {}"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain p' where "p' ∈ set (?sub d)" and "p' ∈ set (?sub d')"
unfolding ys zs by auto

hence "lv p d < lv p' d" "lv p d' < lv p' d'"
using grid_child_level ‹d ∈ set ?ds› ‹d' ∈ set ?ds›
by (auto simp add: gridgen_lgrid_eq lgrid_def grid_child_level)

show False
proof (cases "d < d'")
case True
from ‹p' ∈ set (?sub d)›
have "p ! d' = p' ! d'"
using grid_invariant[of d' "child p right d" "{d' ∈ ds. d' ≤ d}"]
using grid_invariant[of d' "child p left d" "{d' ∈ ds. d' ≤ d}"]
using child_invariant[of d' _ _ d] ‹d < d'› ‹d' < length p›
using gridgen_lgrid_eq lgrid_def by auto
thus False using ‹lv p d' < lv p' d'› unfolding lv_def by auto
next
case False hence "d' < d" using ‹d' ≠ d› by simp
from ‹p' ∈ set (?sub d')›
have "p ! d = p' ! d"
using grid_invariant[of d "child p right d'" "{d ∈ ds. d ≤ d'}"]
using grid_invariant[of d "child p left d'" "{d ∈ ds. d ≤ d'}"]
using child_invariant[of d _ _ d'] ‹d' < d› ‹d < length p›
using gridgen_lgrid_eq lgrid_def by auto
thus False using ‹lv p d < lv p' d› unfolding lv_def by auto
qed
qed
qed
moreover
have "p ∉ set (concat (map ?sub ?ds))"
using gridgen_lgrid_eq lgrid_def grid_not_child[of _ p] by simp
ultimately show ?case
unfolding gridgen.simps Let_def distinct.simps by simp
qed auto

lemma lgrid_finite: "finite (lgrid b ds lm)"
proof (cases "level b ≤ lm")
case True from iffD1[OF le_iff_add True]
obtain l where l: "lm = level b + l" by auto
show ?thesis unfolding l gridgen_lgrid_eq[symmetric] by auto
next
case False hence "!! x. x ∈ grid b ds ⟹ (¬ level x < lm)"
proof -
fix x assume "x ∈ grid b ds"
from grid_level[OF this] show "¬ level x < lm" using False by auto
qed
hence "lgrid b ds lm = {}" unfolding lgrid_def by auto
thus ?thesis by auto
qed

lemma lgrid_sum:
fixes F :: "grid_point ⇒ real"
assumes "d < length b" and "level b < lm"
shows "(∑ p ∈ lgrid b {d} lm. F p) =
(∑ p ∈ lgrid (child b left d) {d} lm. F p) + (∑ p ∈ lgrid (child b right d) {d} lm. F p) + F b"
(is "(∑ p ∈ ?grid b. F p) = (∑ p ∈ ?grid ?l . F p) + (?sum (?grid ?r)) + F b")
proof -
have "!! dir. b ∉ ?grid (child b dir d)"
using grid_child_without_parent[where ds="{d}"] and ‹d < length b› and lgrid_def by auto
hence b_distinct: "b ∉ (?grid ?l ∪ ?grid ?r)" by auto

have "?grid ?l ∩ ?grid ?r = {}"
unfolding lgrid_def using grid_disjunct and ‹d < length b› by auto
from lgrid_finite lgrid_finite and this
have child_eq: "?sum ((?grid ?l) ∪ (?grid ?r)) = ?sum (?grid ?l) + ?sum (?grid ?r)"
by (rule sum.union_disjoint)

have "?grid b = {b} ∪ (?grid ?l) ∪ (?grid ?r)" unfolding lgrid_def grid_partition[where p=b] using assms by auto
hence "?sum (?grid b) = F b + ?sum ((?grid ?l) ∪ (?grid ?r))" using b_distinct and lgrid_finite by auto
thus ?thesis using child_eq by auto
qed

subsection ‹ Base Points ›

definition base :: "nat set ⇒ grid_point ⇒ grid_point"
where "base ds p = (THE b. b ∈ grid (start (length p)) ({0 ..< length p} - ds) ∧ p ∈ grid b ds)"

lemma baseE: assumes p_grid: "p ∈ sparsegrid' dm"
shows "base ds p ∈ grid (start dm) ({0..<dm} - ds)"
and "p ∈ grid (base ds p) ds"
proof -
from p_grid[unfolded sparsegrid'_def]
have *: "∃! x ∈ grid (start dm) ({0..<dm} - ds). p ∈ grid x ds"
by (intro grid_split1) (auto intro: grid_union_dims)
then obtain x where x_eq: "x ∈ grid (start dm) ({0..<dm} - ds) ∧ p ∈ grid x ds"
by auto
with * have "base ds p = x" unfolding base_def by auto
thus "base ds p ∈ grid (start dm) ({0..<dm} - ds)" and "p ∈ grid (base ds p) ds"
using x_eq by auto
qed

lemma baseI: assumes x_grid: "x ∈ grid (start dm) ({0..<dm} - ds)" and p_xgrid: "p ∈ grid x ds"
shows "base ds p = x"
proof -
have "p ∈ grid (start dm) (ds ∪ ({0..<dm} - ds))"
using grid_transitive[OF p_xgrid x_grid, where ds''="ds ∪ ({0..<dm} - ds)"] by auto
moreover have "ds ∩ ({0..<dm} - ds) = {}" by auto
ultimately have "∃! x ∈ grid (start dm) ({0..<dm} - ds). p ∈ grid x ds"
using grid_split1[where p=p and b="start dm" and ds'=ds and ds="{0..<dm} - ds"] by auto
thus "base ds p = x" using x_grid p_xgrid unfolding base_def by auto
qed

lemma base_empty: assumes p_grid: "p ∈ sparsegrid' dm" shows "base {} p = p"
using grid_empty_ds and p_grid and grid_split1[where ds="{0..<dm}" and ds'="{}"] unfolding base_def sparsegrid'_def by auto

lemma base_start_eq: assumes p_spg: "p ∈ sparsegrid dm lm"
shows "start dm = base {0..<dm} p"
proof -
from p_spg
have "start dm ∈ grid (start dm) ({0..<dm} - {0..<dm})"
and "p ∈ grid (start dm) {0..<dm}" using sparsegrid'_def by auto
from baseI[OF this(1) this(2)] show ?thesis by auto
qed

lemma base_in_grid: assumes p_grid: "p ∈ sparsegrid' dm" shows "base ds p ∈ grid (start dm) {0..<dm}"
proof -
let ?ds = "ds ∪ {0..<dm}"
have ds_eq: "{ d ∈ ?ds. d < length (start dm) } = { 0..< dm}"
unfolding start_def by auto
have "base ds p ∈ grid (start dm) ?ds"
using grid_union_dims[OF _ baseE(1)[OF p_grid, where ds=ds], where ds'="?ds"] by auto
thus ?thesis using grid_dim_remove_outer[where b="start dm" and ds="?ds"] unfolding ds_eq by auto
qed

lemma base_grid: assumes p_grid: "p ∈ sparsegrid' dm" shows "grid (base ds p) ds ⊆ sparsegrid' dm"
proof
fix x assume xgrid: "x ∈ grid (base ds p) ds"
have ds_eq: "{ d ∈ {0..<dm} ∪ ds. d < length (start dm) } = {0..<dm}" by auto
from grid_transitive[OF xgrid base_in_grid[OF p_grid], where ds''="{0..<dm} ∪ ds"]
show "x ∈ sparsegrid' dm" unfolding sparsegrid'_def
using grid_dim_remove_outer[where b="start dm" and ds="{0..<dm} ∪ ds"] unfolding ds_eq unfolding Un_ac(3)[of "{0..<dm}"]
by auto
qed
lemma base_length[simp]: assumes p_grid: "p ∈ sparsegrid' dm" shows "length (base ds p) = dm"
proof -
from baseE[OF p_grid] have "base ds p ∈ grid (start dm) ({0..<dm} - ds)" by auto
thus ?thesis by auto
qed
lemma base_in[simp]: assumes "d < dm" and "d ∈ ds" and p_grid: "p ∈ sparsegrid' dm" shows "base ds p ! d = start dm ! d"
proof -
have ds: "d ∉ {0..<dm} - ds" using ‹d ∈ ds› by auto
have "d < length (start dm)" using ‹d < dm› by auto
with grid_invariant[OF this ds] baseE(1)[OF p_grid] show ?thesis by auto
qed
lemma base_out[simp]: assumes "d < dm" and "d ∉ ds" and p_grid: "p ∈ sparsegrid' dm" shows "base ds p ! d = p ! d"
proof -
have "d < length (base ds p)" using base_length[OF p_grid] ‹d < dm› by auto
with grid_invariant[OF this ‹d ∉ ds›] baseE(2)[OF p_grid] show ?thesis by auto
qed
lemma base_base: assumes p_grid: "p ∈ sparsegrid' dm" shows "base ds (base ds' p) = base (ds ∪ ds') p"
proof (rule nth_equalityI)
have b_spg: "base ds' p ∈ sparsegrid' dm" unfolding sparsegrid'_def
using grid_union_dims[OF Diff_subset[where A="{0..<dm}" and B="ds'"] baseE(1)[OF p_grid]] .
from base_length[OF b_spg] base_length[OF p_grid] show "length (base ds (base ds' p)) = length (base (ds ∪ ds') p)" by auto

show "base ds (base ds' p) ! i = base (ds ∪ ds') p ! i" if "i < length (base ds (base ds' p))" for i
proof -
have "i < dm" using that base_length[OF b_spg] by auto
show "base ds (base ds' p) ! i = base (ds ∪ ds') p ! i"
proof (cases "i ∈ ds ∪ ds'")
case True
show ?thesis
proof (cases "i ∈ ds")
case True from base_in[OF ‹i < dm› ‹i ∈ ds ∪ ds'› p_grid] base_in[OF ‹i < dm› this b_spg] show ?thesis by auto
next
case False hence "i ∈ ds'" using ‹i ∈ ds ∪ ds'› by auto
from base_in[OF ‹i < dm› ‹i ∈ ds ∪ ds'› p_grid] base_out[OF ‹i < dm› ‹i ∉ ds› b_spg] base_in[OF ‹i < dm› ‹i ∈ ds'› p_grid] show ?thesis by auto
qed
next
case False hence "i ∉ ds" and "i ∉ ds'" by auto
from base_out[OF ‹i < dm› ‹i ∉ ds ∪ ds'› p_grid] base_out[OF ‹i < dm› ‹i ∉ ds› b_spg] base_out[OF ‹i < dm› ‹i ∉ ds'› p_grid] show ?thesis by auto
qed
qed
qed
lemma grid_base_out: assumes "d < dm" and "d ∉ ds" and p_grid: "b ∈ sparsegrid' dm" and "p ∈ grid (base ds b) ds"
shows "p ! d = b ! d"
proof -
have "base ds b ! d = b ! d" using assms by auto
moreover have "d < length (base ds b)" using assms by auto
from grid_invariant[OF this]
have "p ! d = base ds b ! d" using assms by auto
ultimately show ?thesis by auto
qed

lemma grid_grid_inj_on: assumes "ds ∩ ds' = {}" shows "inj_on snd (⋃p'∈grid b ds. ⋃p''∈grid p' ds'. {(p', p'')})"
proof (rule inj_onI)
fix x y
assume "x ∈ (⋃p'∈grid b ds. ⋃p''∈grid p' ds'. {(p', p'')})"
hence "snd x ∈ grid (fst x) ds'" and "fst x ∈ grid b ds" by auto

assume "y ∈ (⋃p'∈grid b ds. ⋃p''∈grid p' ds'. {(p', p'')})"
hence "snd y ∈ grid (fst y) ds'" and "fst y ∈ grid b ds" by auto

assume "snd x = snd y"
have "fst x = fst y"
proof (rule ccontr)
assume "fst x ≠ fst y"
from grid_disjunct'[OF ‹fst x ∈ grid b ds› ‹fst y ∈ grid b ds› ‹snd x ∈ grid (fst x) ds'› this ‹ds ∩ ds' = {}›]
show False using ‹snd y ∈ grid (fst y) ds'› unfolding ‹snd x = snd y› by auto
qed
show "x = y" using prod_eqI[OF ‹fst x = fst y› ‹snd x = snd y›] .
qed

lemma grid_level_d: assumes "d < length b" and p_grid: "p ∈ grid b {d}" and "p ≠ b" shows "lv p d > lv b d"
proof -
from p_grid[unfolded grid_partition[where p=b]]
show ?thesis using grid_child_level using assms by auto
qed

lemma grid_base_base: assumes "b ∈ sparsegrid' dm"
shows "base ds' b ∈ grid (base ds (base ds' b)) (ds ∪ ds')"
proof -
from base_grid[OF ‹b ∈ sparsegrid' dm›] have "base ds' b ∈ sparsegrid' dm" by auto
from grid_union_dims[OF _ baseE(2)[OF this], of ds "ds ∪ ds'"] show ?thesis by auto
qed

lemma grid_base_union: assumes b_spg: "b ∈ sparsegrid' dm" and p_grid: "p ∈ grid (base ds b) ds" and x_grid: "x ∈ grid (base ds' p) ds'"
shows "x ∈ grid (base (ds ∪ ds') b) (ds ∪ ds')"
proof -
have ds_union: "ds ∪ ds' = ds' ∪ (ds ∪ ds')" by auto

from base_grid[OF b_spg] p_grid have p_spg: "p ∈ sparsegrid' dm"  by auto
with assms and grid_base_base have base_b': "base ds' p ∈ grid (base ds (base ds' p)) (ds ∪ ds')" by auto
moreover have "base ds' (base ds b) = base ds' (base ds p)" (is "?b = ?p")
proof (rule nth_equalityI)
have bb_spg: "base ds b ∈ sparsegrid' dm" using base_grid[OF b_spg] grid.Start by auto
hence "dm = length (base ds b)" by auto
have bp_spg: "base ds p ∈ sparsegrid' dm" using base_grid[OF p_spg] grid.Start by auto

show "length ?b = length ?p" using base_length[OF bp_spg] base_length[OF bb_spg] by auto
show "?b ! i = ?p ! i" if "i < length ?b" for i
proof -
have "i < dm" and "i < length (base ds b)" using that base_length[OF bb_spg] ‹dm = length (base ds b)› by auto
show "?b ! i = ?p ! i"
proof (cases "i ∈ ds ∪ ds'")
case True
hence "!! x. base ds x ∈ sparsegrid' dm ⟹ x ∈ sparsegrid' dm ⟹ base ds' (base ds x) ! i = (start dm) ! i"
proof - fix x assume x_spg: "x ∈ sparsegrid' dm" and xb_spg: "base ds x ∈ sparsegrid' dm"
show "base ds' (base ds x) ! i = (start dm) ! i"
proof (cases "i ∈ ds'")
case True from base_in[OF ‹i < dm› this xb_spg] show ?thesis .
next
case False hence "i ∈ ds" using ‹i ∈ ds ∪ ds'› by auto
from base_out[OF ‹i < dm› False xb_spg] base_in[OF ‹i < dm› this x_spg] show ?thesis by auto
qed
qed
from this[OF bp_spg p_spg] this[OF bb_spg b_spg] show ?thesis by auto
next
case False hence "i ∉ ds" and "i ∉ ds'" by auto
from grid_invariant[OF ‹i < length (base ds b)› ‹i ∉ ds› p_grid]
base_out[OF ‹i < dm› ‹i ∉ ds'› bp_spg] base_out[OF ‹i < dm› ‹i ∉ ds› p_spg] base_out[OF ‹i < dm› ‹i ∉ ds'› bb_spg]
show ?thesis by auto
qed
qed
qed
ultimately have "base ds' p ∈ grid (base (ds ∪ ds') b) (ds ∪ ds')"
by (simp only: base_base[OF p_spg] base_base[OF b_spg] Un_ac(3))
from grid_transitive[OF x_grid this] show ?thesis using ds_union by auto
qed
lemma grid_base_dim_add: assumes "ds' ⊆ ds" and b_spg: "b ∈ sparsegrid' dm" and p_grid: "p ∈ grid (base ds' b) ds'"
shows "p ∈ grid (base ds b) ds"
proof -
have ds_eq: "ds' ∪ ds = ds" using assms by auto

have "p ∈ sparsegrid' dm" using base_grid[OF b_spg] p_grid by auto
hence "p ∈ grid (base ds p) ds" using baseE by auto
from grid_base_union[OF b_spg p_grid this]
show ?thesis using ds_eq by auto
qed
lemma grid_replace_dim: assumes "d < length b'" and "d < length b" and p_grid: "p ∈ grid b ds" and p'_grid: "p' ∈ grid b' ds"
shows "p[d := p' ! d] ∈ grid (b[d := b' ! d]) ds" (is "_ ∈ grid ?b ds")
using p'_grid and p_grid
proof induct
case (Child p'' d' dir)
hence p''_grid: "p[d := p'' ! d] ∈ grid ?b ds" and "d < length p''" using assms by auto
have "d < length p" using p_grid assms by auto
thus ?case
proof (cases "d' = d")
case True
from grid.Child[OF p''_grid ‹d' ∈ ds›]
show ?thesis unfolding child_def ix_def lv_def list_update_overwrite ‹d' = d› nth_list_update_eq[OF ‹d < length p''›] nth_list_update_eq[OF ‹d < length p›] .
next
case False
show ?thesis unfolding child_def nth_list_update_neq[OF False] using Child by auto
qed
qed (rule grid_change_dim)
lemma grid_shift_base:
assumes ds_dj: "ds ∩ ds' = {}" and b_spg: "b ∈ sparsegrid' dm" and p_grid: "p ∈ grid (base (ds' ∪ ds) b) (ds' ∪ ds)"
shows "base ds' p ∈ grid (base (ds ∪ ds') b) ds"
proof -
from grid_split[OF p_grid]
obtain x where x_grid: "x ∈ grid (base (ds' ∪ ds) b) ds" and p_xgrid: "p ∈ grid x ds'" by auto
from grid_union_dims[OF _ this(1)]
have x_spg: "x ∈ sparsegrid' dm" using base_grid[OF b_spg] by auto

have b_len: "length (base (ds' ∪ ds) b) = dm" using base_length[OF b_spg] by auto

define d' where "d' = dm"
moreover have "d' ≤ dm ⟹ x ∈ grid (start dm) ({0..<dm} - {d ∈ ds'. d < d'})"
proof (induct d')
case (Suc d')
with b_len have d'_b: "d' < length (base (ds' ∪ ds) b)" by auto
show ?case
proof (cases "d' ∈ ds'")
case True hence "d' ∉ ds" and "d' ∈ ds' ∪ ds" using ds_dj by auto
have "{0..<dm} - {d ∈ ds'. d < d'} = ({0..<dm} - {d ∈ ds'. d < d'}) - {d'} ∪ {d'}" using ‹Suc d' ≤ dm› by auto
also have "… = ({0..<dm} - {d ∈ ds'. d < Suc d'}) ∪ {d'}" by auto
finally have x_g: "x ∈ grid (start dm) ({d'} ∪ ({0..<dm} - {d ∈ ds'. d < Suc d'}))" using Suc by auto
from grid_invariant[OF d'_b ‹d' ∉ ds› x_grid] base_in[OF _ ‹d' ∈ ds' ∪ ds› b_spg] ‹Suc d' ≤ dm›
have "x ! d' = start dm ! d'" by auto
from grid_dim_remove[OF x_g this] show ?thesis .
next
case False
hence "{d ∈ ds'. d < Suc d'} = {d ∈ ds'. d < d' ∨ d = d'}" by auto
also have "… = {d ∈ ds'. d < d'}" using False by auto
finally show ?thesis using Suc by auto
qed
next
case 0 show ?case using x_spg[unfolded sparsegrid'_def] by auto
qed
moreover have "{0..<dm} - ds' = {0..<dm} - {d ∈ ds'. d < dm}" by auto
ultimately have "x ∈ grid (start dm) ({0..<dm} - ds')" by auto
from baseI[OF this p_xgrid] and x_grid
show ?thesis by (auto simp: Un_ac(3))
qed

subsection ‹ Lift Operation over all Grid Points ›

definition lift :: "(nat ⇒ nat ⇒ grid_point ⇒ vector ⇒ vector) ⇒ nat ⇒ nat ⇒ nat ⇒ vector ⇒ vector"
where "lift f dm lm d = foldr (λ p. f d (lm - level p) p) (gridgen (start dm) ({ 0 ..< dm } - { d }) lm)"

lemma lift:
assumes "d < dm" and "p ∈ sparsegrid dm lm"
and Fintro: "⋀ l b p α. ⟦ b ∈ lgrid (start dm) ({0..<dm} - {d}) lm ;
l + level b = lm ; p ∈ sparsegrid dm lm ⟧
⟹ F d l b α p = (if b = base {d} p
then (∑ p' ∈ lgrid b {d} lm. S (α p') p p')
else α p)"
shows "lift F dm lm d α p = (∑ p' ∈ lgrid (base {d} p) {d} lm. S (α p') p p')"
(is "?lift = ?S p α")
proof -
let ?gridgen = "gridgen (start dm) ({0..<dm} - {d}) lm"
let "?f p" = "F d (lm - level p) p"

{ fix bs β b
assume "set bs ⊆ set ?gridgen" and "distinct bs" and "p ∈ sparsegrid dm lm"
hence "foldr ?f bs β p = (if base {d} p ∈ set bs then ?S p β else β p)"
proof (induct bs arbitrary: p)
case (Cons b bs)
hence "b ∈ lgrid (start dm) ({0..<dm} - {d}) lm"
and "(lm - level b) + level b = lm"
and b_grid: "b ∈ grid (start dm) ({0..<dm} - {d})"
using lgrid_def gridgen_lgrid_eq by auto
note F = Fintro[OF this(1,2) ‹p ∈ sparsegrid dm lm›]

have "b ∉ set bs" using ‹distinct (b#bs)› by auto

show ?case
proof (cases "base {d} p ∈ set (b#bs)")
case True note base_in_set = this

show ?thesis
proof (cases "b = base {d} p")
case True
moreover
{ fix p' assume "p' ∈ lgrid b {d} lm"
hence "p' ∈ grid b {d}" and "level p' < lm" unfolding lgrid_def by auto
from grid_transitive[OF this(1) b_grid, of "{0..<dm}"] ‹d < dm›
baseI[OF b_grid ‹p' ∈ grid b {d}›] ‹b ∉ set bs›
Cons.prems Cons.hyps[of p'] this(2)
have "foldr ?f bs β p' = β p'" unfolding sparsegrid_def lgrid_def by auto }
ultimately show ?thesis
using F base_in_set by auto
next
case False
with base_in_set have "base {d} p ∈ set bs" by auto
with Cons.hyps[of p] Cons.prems
have "foldr ?f bs β p = ?S p β" by auto
thus ?thesis using F base_in_set False by auto
qed
next
case False
hence "b ≠ base {d} p" by auto
from False Cons.hyps[of p] Cons.prems
have "foldr ?f bs β p = β p" by auto
thus ?thesis using False F ‹b ≠ base {d} p› by auto
qed
qed auto
}
moreover have "base {d} p ∈ set ?gridgen"
proof -
have "p ∈ grid (base {d} p) {d}"
using ‹p ∈ sparsegrid dm lm›[THEN sparsegrid_subset] by (rule baseE)
from grid_level[OF this] baseE(1)[OF sparsegrid_subset[OF ‹p ∈ sparsegrid dm lm›]]
show ?thesis using ‹p ∈ sparsegrid dm lm›
unfolding gridgen_lgrid_eq sparsegrid'_def lgrid_def sparsegrid_def
by auto
qed
ultimately show ?thesis unfolding lift_def
using gridgen_distinct ‹p ∈ sparsegrid dm lm› by auto
qed

subsection ‹ Parent Points ›

definition parents :: "nat ⇒ grid_point ⇒ grid_point ⇒ grid_point set"
where "parents d b p = { x ∈ grid b {d}. p ∈ grid x {d} }"

lemma parents_split: assumes p_grid: "p ∈ grid (child b dir d) {d}"
shows "parents d b p = { b } ∪ parents d (child b dir d) p"
proof (intro set_eqI iffI)
let ?chd = "child b dir d" and ?chid = "child b (inv dir) d"
fix x assume "x ∈ parents d b p"
hence "x ∈ grid b {d}" and "p ∈ grid x {d}" unfolding parents_def by auto
hence x_split: "x ∈ {b} ∪ grid ?chd {d} ∪ grid ?chid {d}" using grid_onedim_split[where ds="{}" and b=b] and grid_empty_ds
by (cases dir, auto)
thus "x ∈ {b} ∪ parents d (child b dir d) p"
proof (cases "x = b")
case False
have "d < length b"
proof (rule ccontr)
assume "¬ d < length b" hence empty: "{d' ∈ {d}. d' < length b} = {}" by auto
have "x = b" using ‹x ∈ grid b {d}›
unfolding grid_dim_remove_outer[where ds="{d}" and b=b] empty
using grid_empty_ds by auto
thus False using ‹¬ x = b› by auto
qed
have "x ∉ grid ?chid {d}"
proof (rule ccontr)
assume "¬ x ∉ grid ?chid {d}"
hence "p ∈ grid ?chid {d}" using grid_transitive[OF ‹p ∈ grid x {d}›, where ds'="{d}"]
by auto
hence "p ∉ grid ?chd {d}" using grid_disjunct[OF ‹d < length b›] by (cases dir, auto)
thus False using ‹p ∈ grid ?chd {d}› ..
qed
with False and x_split
have "x ∈ grid ?chd {d}" by auto
thus ?thesis unfolding parents_def using ‹p ∈ grid x {d}› by auto
qed auto
next
let ?chd = "child b dir d" and ?chid = "child b (inv dir) d"
fix x assume x_in: "x ∈ {b} ∪ parents d ?chd p"
thus "x ∈ parents d b p"
proof (cases "x = b")
case False
hence "x ∈ parents d ?chd p" using x_in by auto
thus ?thesis unfolding parents_def using grid_child[where b=b] by auto
next
from p_grid have "p ∈ grid b {d}" using grid_child[where b=b] by auto
case True thus ?thesis unfolding parents_def using ‹p ∈ grid b {d}› by auto
qed
qed

lemma parents_no_parent: assumes "d < length b" shows "b ∉ parents d (child b dir d) p" (is "_ ∉ parents _ ?ch _")
proof
assume "b ∈ parents d ?ch p" hence "b ∈ grid ?ch {d}" unfolding parents_def by auto
from grid_level[OF this]
have "level b + 1 ≤ level b" unfolding child_level[OF ‹d < length b›] .
thus False by auto
qed

lemma parents_subset_lgrid: "parents d b p ⊆ lgrid b {d} (level p + 1)"
proof
fix x assume "x ∈ parents d b p"
hence "x ∈ grid b {d}" and "p ∈ grid x {d}" unfolding parents_def by auto
moreover hence "level x ≤ level p" using grid_level by auto
hence "level x < level p + 1" by auto
ultimately show "x ∈ lgrid b {d} (level p + 1)" unfolding lgrid_def by auto
qed

lemma parents_finite: "finite (parents d b p)"
using finite_subset[OF parents_subset_lgrid lgrid_finite] .

lemma parent_sum: assumes p_grid: "p ∈ grid (child b dir d) {d}" and "d < length b"
shows "(∑ x ∈ parents d b p. F x) = F b + (∑ x ∈ parents d (child b dir d) p. F x)"
unfolding parents_split[OF p_grid] using parents_no_parent[OF ‹d < length b›, where dir=dir and p=p] using parents_finite
by auto

lemma parents_single: "parents d b b = { b }"
proof
have "parents d b b ⊆ lgrid b {d} (level b + (Suc 0))" using parents_subset_lgrid by auto
also have "… = {b}" unfolding gridgen_lgrid_eq[symmetric] gridgen.simps Let_def by auto
finally show "parents d b b ⊆ { b }" .
next
have "b ∈ parents d b b" unfolding parents_def by auto
thus "{ b } ⊆ parents d b b" by auto
qed

lemma grid_single_dimensional_specification:
assumes "d < length b"
and "odd i"
and "lv b d + l' = l"
and "i < (ix b d + 1) * 2^l'"
and "i > (ix b d - 1) * 2^l'"
shows "b[d := (l,i)] ∈ grid b {d}"
using assms proof (induct l' arbitrary: b)
case 0
hence "i = ix b d" and "l = lv b d" by auto
thus ?case unfolding ix_def lv_def by auto
next
case (Suc l')

have "d ∈ {d}" by auto

show ?case
proof (rule linorder_cases)
assume "i = ix b d * 2^(Suc l')"
hence "even i" by auto
thus ?thesis using ‹odd i› by blast
next
assume *: "i < ix b d * 2^(Suc l')"

let ?b = "child b left d"

have "d < length ?b" using Suc by auto
moreover note ‹odd i›
moreover have "lv ?b d + l' = l"
and "i < (ix ?b d + 1) * 2^l'"
and "(ix ?b d - 1) * 2^l' < i"
unfolding child_ix_left[OF Suc.prems(1)]
using Suc.prems * child_lv by (auto simp add: field_simps)
ultimately have "?b[d := (l,i)] ∈ grid ?b {d}"
by (rule Suc.hyps)
thus ?thesis
by (auto intro!: grid_child[OF ‹d ∈ {d}›, of _ b left]
next
assume *: "ix b d * 2^(Suc l') < i"

let ?b = "child b right d"

have "d < length ?b" using Suc by auto
moreover note ‹odd i›
moreover have "lv ?b d + l' = l"
and "i < (ix ?b d + 1) * 2^l'"
and "(ix ?b d - 1) * 2^l' < i"
unfolding child_ix_right[OF Suc.prems(1)]
using Suc.prems * child_lv by (auto simp add: field_simps)
ultimately have "?b[d := (l,i)] ∈ grid ?b {d}"
by (rule Suc.hyps)
thus ?thesis
by (auto intro!: grid_child[OF ‹d ∈ {d}›, of _ b right]
qed
qed

lemma grid_multi_dimensional_specification:
assumes "dm ≤ length b" and "length p = length b"
and "⋀ d. d < dm ⟹
odd (ix p d) ∧
lv b d ≤ lv p d ∧
ix p d < (ix b d + 1) * 2^(lv p d - lv b d) ∧
ix p d > (ix b d - 1) * 2^(lv p d - lv b d)"
(is "⋀ d. d < dm ⟹ ?bounded p d")
and "⋀ d. ⟦ dm ≤ d ; d < length b ⟧ ⟹ p ! d = b ! d"
shows "p ∈ grid b {0..<dm}"
using assms proof (induct dm arbitrary: p)
case 0
hence "p = b" by (auto intro!: nth_equalityI)
thus ?case by auto
next
case (Suc dm)
hence "dm ≤ length b"
and "dm < length p" by auto

let ?p = "p[dm := b ! dm]"

note ‹dm ≤ length b›
moreover have "length ?p = length b" using ‹length p = length b› by simp
moreover
{
fix d assume "d < dm"
hence *: "d < Suc dm" and "dm ≠ d" by auto
have "?p ! d = p ! d"
by (rule nth_list_update_neq[OF ‹dm ≠ d›])
hence "?bounded ?p d"
using Suc.prems(3)[OF *] lv_def ix_def
by simp
}
moreover
{
fix d assume "dm ≤ d" and "d < length b"
have "?p ! d = b ! d"
proof (cases "d = dm")
case True thus ?thesis using ‹d < length b› ‹length p = length b› by auto
next
case False
hence "Suc dm ≤ d" using ‹dm ≤ d› by auto
thus ?thesis using Suc.prems(4) ‹d < length b› by auto
qed
}
ultimately
have *: "?p ∈ grid b {0..<dm}"
by (auto intro!: Suc.hyps)

have "lv b dm ≤ lv p dm" using Suc.prems(3)[OF lessI] by simp

have [simp]: "lv ?p dm = lv b dm" using lv_def ‹dm < length p› by auto
have [simp]: "ix ?p dm = ix b dm" using ix_def ‹dm < length p› by auto
have [simp]: "p[dm := (lv p dm, ix p dm)] = p"
using lv_def ix_def ‹dm < length p› by auto
have "dm < length ?p" and
[simp]: "lv b dm + (lv p dm - lv b dm) = lv p dm"
using ‹dm < length p› ‹lv b dm ≤ lv p dm› by auto
from grid_single_dimensional_specification[OF this(1),
where l="lv p dm" and i="ix p dm" and l'="lv p dm - lv b dm", simplified]
have "p ∈ grid ?p {dm}"
using Suc.prems(3)[OF lessI] by blast
from grid_transitive[OF this *]
show ?case by auto
qed

lemma sparsegrid:
"sparsegrid dm lm = {p.
length p = dm ∧ level p < lm ∧
(∀ d < dm. odd (ix p d) ∧ 0 < ix p d ∧ ix p d < 2^(lv p d + 1))}"
(is "_ = ?set")
proof (rule equalityI[OF subsetI subsetI])
fix p
assume *: "p ∈ sparsegrid dm lm"
hence "length p = dm" and "level p < lm" unfolding sparsegrid_def by auto
moreover
{ fix d assume "d < dm"
hence **: "p ∈ grid (start dm) {0..<dm}" and "d < length (start dm)"
using * unfolding sparsegrid_def by auto
have "odd (ix p d)"
proof (cases "p ! d = start dm ! d")
case True
thus ?thesis unfolding start_def using ‹d < dm› ix_def by auto
next
case False
from grid_odd[OF _ this **]
show ?thesis using ‹d < dm› by auto
qed
hence "odd (ix p d) ∧ 0 < ix p d ∧ ix p d < 2^(lv p d + 1)"
using grid_estimate[OF ‹d < length (start dm)› **]
unfolding ix_def lv_def start_def using ‹d < dm› by auto
}
ultimately show "p ∈ ?set"
using sparsegrid_def lgrid_def by auto
next
fix p
assume "p ∈ ?set"
with grid_multi_dimensional_specification[of dm "start dm" p]
have "p ∈ grid (start dm) {0..<dm}" and "level p < lm"
by auto
thus "p ∈ sparsegrid dm lm"
unfolding sparsegrid_def lgrid_def by auto
qed

end


# Theory Triangular_Function

section ‹ Hat Functions ›

theory Triangular_Function
imports
"HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration"
Grid
begin

lemma continuous_on_max[continuous_intros]:
fixes f :: "_ ⇒ 'a::linorder_topology"
shows "continuous_on S f ⟹ continuous_on S g ⟹ continuous_on S (λx. max (f x) (g x))"
by (auto simp: continuous_on_def intro: tendsto_max)

definition φ :: "(nat × int) ⇒ real ⇒ real" where
"φ ≡ (λ(l,i) x. max 0 (1 - ¦ x * 2^(l + 1) - real_of_int i ¦))"

definition Φ :: "(nat × int) list ⇒ (nat ⇒ real) ⇒ real" where
"Φ p x = (∏d<length p. φ (p ! d) (x d))"

definition l2_φ where
"l2_φ p1 p2 = (∫x. φ p1 x * φ p2 x ∂lborel)"

definition l2 where
"l2 a b = (∫x. Φ a x * Φ b x ∂(Π⇩M d∈{..<length a}. lborel))"

lemma measurable_φ[measurable]: "φ p ∈ borel_measurable borel"
by (cases p) (simp add: φ_def)

lemma φ_nonneg: "0 ≤ φ p x"
by (simp add: φ_def split: prod.split)

lemma φ_zero_iff:
"φ (l,i) x = 0 ⟷ x ∉ {real_of_int (i - 1) / 2^(l + 1) <..< real_of_int (i + 1) / 2^(l + 1)}"
by (auto simp: φ_def field_simps split: split_max)

lemma φ_zero: "x ∉ {real_of_int (i - 1) / 2^(l + 1) <..< real_of_int (i + 1) / 2^(l + 1)} ⟹ φ (l,i) x = 0"
unfolding φ_zero_iff by simp

lemma φ_eq_0: assumes x: "x < 0 ∨ 1 < x" and i: "0 < i" "i < 2^Suc l" shows "φ (l, i) x = 0"
using x
proof
assume "x < 0"
also have "0 ≤ real_of_int (i - 1) / 2^(l + 1)"
using i by (auto simp: field_simps)
finally show ?thesis
by (auto intro!: φ_zero simp: field_simps)
next
have "real_of_int (i + 1) / 2^(l + 1) ≤ 1"
using i by (subst divide_le_eq_1_pos) (auto simp del: of_int_add power_Suc)
also assume "1 < x"
finally show ?thesis
by (auto intro!: φ_zero simp: field_simps)
qed

lemma ix_lt: "p ∈ sparsegrid dm lm ⟹ d < dm ⟹ ix p d < 2^(lv p d + 1)"
unfolding sparsegrid_def lgrid_def
using grid_estimate[of d "start dm" p "{0 ..< dm}"] by auto

lemma ix_gt: "p ∈ sparsegrid dm lm ⟹ d < dm ⟹ 0 < ix p d"
unfolding sparsegrid_def lgrid_def
using grid_estimate[of d "start dm" p "{0 ..< dm}"] by auto

lemma Φ_eq_0: assumes x: "∃d<length p. x d < 0 ∨ 1 < x d" and p: "p ∈ sparsegrid dm lm" shows "Φ p x = 0"
unfolding Φ_def
proof (rule prod_zero)
from x guess d ..
with p[THEN ix_lt, of d] p[THEN ix_gt, of d] p
show "∃a∈{..<length p}. φ (p ! a) (x a) = 0"
apply (cases "p!d")
apply (intro bexI[of _ d])
apply (auto intro!: φ_eq_0 simp: sparsegrid_length ix_def lv_def)
done
qed simp

lemma φ_left_support':
"x ∈ {real_of_int (i - 1) / 2^(l + 1) .. real_of_int i / 2^(l + 1)} ⟹ φ (l,i) x = 1 + x * 2^(l + 1) - real_of_int i"
by (auto simp: φ_def field_simps split: split_max)

lemma φ_left_support: "x ∈ {-1 .. 0::real} ⟹ φ (l,i) ((x + real_of_int i) / 2^(l + 1)) = 1 + x"
by (auto simp: φ_def field_simps split: split_max)

lemma φ_right_support':
"x ∈ {real_of_int i / 2^(l + 1) .. real_of_int (i + 1) / 2^(l + 1)} ⟹ φ (l,i) x = 1 - x * 2^(l + 1) + real_of_int i"
by (auto simp: φ_def field_simps split: split_max)

lemma φ_right_support:
"x ∈ {0 .. 1::real} ⟹ φ (l,i) ((x + real i) / 2^(l + 1)) = 1 - x"
by (auto simp: φ_def field_simps split: split_max)

lemma integrable_φ: "integrable lborel (φ p)"
proof (induct p)
case (Pair l i)
have "integrable lborel (λx. indicator {real_of_int (i - 1) / 2^(l + 1) .. real_of_int (i + 1) / 2^(l + 1)} x *⇩R φ (l, i) x)"
unfolding φ_def by (intro borel_integrable_compact) (auto intro!: continuous_intros)
then show ?case
by (rule integrable_cong[THEN iffD1, rotated -1]) (auto simp: φ_zero_iff)
qed

lemma integrable_φ2: "integrable lborel (λx. φ p x * φ q x)"
proof (cases p q rule: prod.exhaust[case_product prod.exhaust])
case (Pair_Pair l i l' i')
have "integrable lborel
(λx. indicator {real_of_int (i - 1) / 2^(l + 1) .. real_of_int (i + 1) / 2^(l + 1)} x *⇩R (φ (l, i) x * φ (l', i') x))"
unfolding φ_def by (intro borel_integrable_compact) (auto intro!: continuous_intros)
then show ?thesis unfolding Pair_Pair
by (rule integrable_cong[THEN iffD1, rotated -1]) (auto simp: φ_zero_iff)
qed

lemma l2_φI_DERIV:
assumes n: "⋀ x. x ∈ { (real_of_int i' - 1) / 2^(l' + 1) .. real_of_int i' / 2^(l' + 1) } ⟹
DERIV Φ_n x :> (φ (l', i') x * φ (l, i) x)" (is "⋀ x. x ∈ {?a..?b} ⟹ DERIV _ _ :> ?P x")
and p: "⋀ x. x ∈ { real_of_int i' / 2^(l' + 1) .. (real_of_int i' + 1) / 2^(l' + 1) } ⟹
DERIV Φ_p x :> (φ (l', i') x * φ (l, i) x)" (is "⋀ x. x ∈ {?b..?c} ⟹ _")
shows "l2_φ (l', i') (l, i) = (Φ_n ?b - Φ_n ?a) + (Φ_p ?c - Φ_p ?b)"
proof -
have "has_bochner_integral lborel
(λx. ?P x * indicator {?a..?b} x + ?P x * indicator {?b..?c} x)
((Φ_n ?b - Φ_n ?a) + (Φ_p ?c - Φ_p ?b))"
by (intro has_bochner_integral_add has_bochner_integral_FTC_Icc_nonneg n p)
(auto simp: φ_nonneg field_simps)
then have "has_bochner_integral lborel?P ((Φ_n ?b - Φ_n ?a) + (Φ_p ?c - Φ_p ?b))"
by (rule has_bochner_integral_discrete_difference[where X="{?b}", THEN iffD1, rotated -1])
(auto simp: power_add intro!: φ_zero integral_cong split: split_indicator)
then show ?thesis by (simp add: has_bochner_integral_iff l2_φ_def)
qed

lemma l2_eq: "length a = length b ⟹ l2 a b = (∏d<length a. l2_φ (a!d) (b!d))"
unfolding l2_def l2_φ_def Φ_def
proof (rule product_sigma_finite.product_integral_prod)
show "product_sigma_finite (λd. lborel)" ..
qed (auto intro: integrable_φ2)

lemma l2_when_disjoint:
assumes "l ≤ l'"
defines "d == l' - l"
assumes "(i + 1) * 2^d < i' ∨ i' < (i - 1) * 2^d" (is "?right ∨ ?left")
shows "l2_φ (l', i') (l, i) = 0"
proof -
let ?sup = "λl i. {real_of_int (i - 1) / 2^(l + 1) <..< real_of_int (i + 1) / 2^(l + 1)}"

have l': "l' = l + d"
using assms by simp
have *: "⋀i l. 2 ^ l = real_of_int (2 ^ l::int)"
by simp
have [arith]: "0 < (2^d::int)"
by simp

from ‹?right ∨ ?left› ‹l ≤ l'› have empty_support: "?sup l i ∩ ?sup l' i' = {}"
simp del: of_int_diff of_int_add of_int_mult of_int_power)
then have "⋀x. φ (l', i') x * φ (l, i) x = 0"
unfolding φ_zero_iff mult_eq_0_iff by blast
then show ?thesis
by (simp add: l2_φ_def del: mult_eq_0_iff vector_space_over_itself.scale_eq_0_iff)
qed

lemma l2_commutative: "l2_φ p q = l2_φ q p"

lemma l2_when_same: "l2_φ (l, i) (l, i) = 1/3 / 2^l"
proof (subst l2_φI_DERIV)
let ?l = "(2 :: real)^(l + 1)"
let ?in = "real_of_int i - 1"
let ?ip = "real_of_int i + 1"
let ?φ = "φ (l,i)"
let ?φ2 = "λx. ?φ x * ?φ x"

{ fix x assume "x ∈ {?in / ?l .. real_of_int i / ?l}"
hence φ_eq: "?φ x = ?l * x  - ?in" using φ_left_support' by auto
show "DERIV (λx. x^3 / 3 * ?l^2 + x * ?in^2 - x^2/2 * 2 * ?l * ?in) x :> ?φ2 x"
by (auto intro!: derivative_eq_intros simp add: power2_eq_square field_simps φ_eq) }

{ fix x assume "x ∈ {real_of_int i / ?l .. ?ip / ?l}"
hence φ_eq: "?φ x = ?ip - ?l * x" using φ_right_support' by auto
show "DERIV (λx. x^3 / 3 * ?l^2 + x * ?ip^2 - x^2/2 * 2 * ?l * ?ip) x :> ?φ2 x"
by (auto intro!: derivative_eq_intros simp add: power2_eq_square field_simps φ_eq) }
qed (simp_all add: field_simps power_eq_if[of _ 2] power_eq_if[of _ 3])

lemma l2_when_left_child:
assumes "l < l'"
and i'_bot: "i' > (i - 1) * 2^(l' - l)"
and i'_top: "i' < i * 2^(l' - l)"
shows "l2_φ (l', i') (l, i) = (1 + real_of_int i' / 2^(l' - l) - real_of_int i) / 2^(l' + 1)"
proof (subst l2_φI_DERIV)
let ?l' = "(2 :: real)^(l' + 1)"
let ?in' = "real_of_int i' - 1"
let ?ip' = "real_of_int i' + 1"
let ?l = "(2 :: real)^(l + 1)"
let ?i = "real_of_int i - 1"
let ?φ' = "φ (l',i')"
let ?φ = "φ (l, i)"
let "?φ2 x" = "?φ' x * ?φ x"
define Φ_n where "Φ_n x = x^3 / 3 * ?l' * ?l + x * ?i * ?in' - x^2 / 2 * (?in' * ?l + ?i * ?l')" for x
define Φ_p where "Φ_p x = x^2 / 2 * (?ip' * ?l + ?i * ?l') - x^3 / 3 * ?l' * ?l - x * ?i * ?ip'" for x

have level_diff: "2^(l' - l) = 2^l' / (2^l :: real)" using power_diff[of "2::real" l l'] ‹l < l'› by auto

{ fix x assume x: "x ∈ {?in' / ?l' .. ?ip' / ?l'}"
have "?i * 2^(l' - l) ≤ ?in'"
using i'_bot int_less_real_le by auto
hence "?i / ?l ≤ ?in' / ?l'"
using level_diff by (auto simp: field_simps)
hence "?i / ?l ≤ x" using x by auto
moreover
have "?ip' ≤ real_of_int i * 2^(l' - l)"
using i'_top int_less_real_le by auto
hence ip'_le_i: "?ip' / ?l' ≤ real_of_int i / ?l"
using level_diff by (auto simp: field_simps)
hence "x ≤ real_of_int i / ?l" using x by auto
ultimately have "?φ x = ?l * x  - ?i" using φ_left_support' by auto
} note φ_eq = this

{ fix x assume x: "x ∈ {?in' / ?l' .. real_of_int i' / ?l'}"
hence φ'_eq: "?φ' x = ?l' * x  - ?in'" using φ_left_support' by auto
from x have x': "x ∈ {?in' / ?l' .. ?ip' / ?l'}" by (auto simp add: field_simps)
show "DERIV Φ_n x :> ?φ2 x" unfolding φ_eq[OF x'] φ'_eq Φ_n_def
by (auto intro!: derivative_eq_intros simp add: power2_eq_square algebra_simps) }

{ fix x assume x: "x ∈ {real_of_int i' / ?l' .. ?ip' / ?l'}"
hence φ'_eq: "?φ' x = ?ip' - ?l' * x" using φ_right_support' by auto
from x have x': "x ∈ {?in' / ?l' .. ?ip' / ?l'}" by (simp add: field_simps)
show "DERIV Φ_p x :> ?φ2 x" unfolding φ_eq[OF x'] φ'_eq Φ_p_def
by (auto intro!: derivative_eq_intros simp add: power2_eq_square algebra_simps) }
qed (simp_all add: field_simps power_eq_if[of _ 2] power_eq_if[of _ 3] power_diff[of "2::real", OF _ ‹l < l'›[THEN less_imp_le]] )

lemma l2_when_right_child:
assumes "l < l'"
and i'_bot: "i' > i * 2^(l' - l)"
and i'_top: "i' < (i + 1) * 2^(l' - l)"
shows "l2_φ (l', i') (l, i) = (1 - real_of_int i' / 2^(l' - l) + real_of_int i) / 2^(l' + 1)"
proof (subst l2_φI_DERIV)
let ?l' = "(2 :: real)^(l' + 1)"
let ?in' = "real_of_int i' - 1"
let ?ip' = "real_of_int i' + 1"
let ?l = "(2 :: real)^(l + 1)"
let ?i = "real_of_int i + 1"
let ?φ' = "φ (l',i')"
let ?φ = "φ (l, i)"
let ?φ2 = "λx. ?φ' x * ?φ x"
define Φ_n where "Φ_n x = x^2 / 2 * (?in' * ?l + ?i * ?l') - x^3 / 3 * ?l' * ?l - x * ?i * ?in'" for x
define Φ_p where "Φ_p x = x^3 / 3 * ?l' * ?l + x * ?i * ?ip' - x^2 / 2 * (?ip' * ?l + ?i * ?l')" for x

have level_diff: "2^(l' - l) = 2^l' / (2^l :: real)" using power_diff[of "2::real" l l'] ‹l < l'› by auto

{ fix x assume x: "x ∈ {?in' / ?l' .. ?ip' / ?l'}"
have "real_of_int i * 2^(l' - l) ≤ ?in'"
using i'_bot int_less_real_le by auto
hence "real_of_int i / ?l ≤ ?in' / ?l'"
using level_diff by (auto simp: field_simps)
hence "real_of_int i / ?l ≤ x" using x by auto
moreover
have "?ip' ≤ ?i * 2^(l' - l)"
using i'_top int_less_real_le by auto
hence ip'_le_i: "?ip' / ?l' ≤ ?i / ?l"
using level_diff by (auto simp: field_simps)
hence "x ≤ ?i / ?l" using x by auto
ultimately have "?φ x = ?i - ?l * x" using φ_right_support' by auto
} note φ_eq = this

{ fix x assume x: "x ∈ {?in' / ?l' .. real_of_int i' / ?l'}"
hence φ'_eq: "?φ' x = ?l' * x  - ?in'" using φ_left_support' by auto

from x have x': "x ∈ {?in' / ?l' .. ?ip' / ?l'}" by (simp add: field_simps)
show "DERIV Φ_n x :> ?φ2 x" unfolding Φ_n_def φ_eq[OF x'] φ'_eq

{ fix x assume x: "x ∈ {real_of_int i' / ?l' .. ?ip' / ?l'}"
hence φ'_eq: "?φ' x = ?ip' - ?l' * x" using φ_right_support' by auto
from x have x': "x ∈ {?in' / ?l' .. ?ip' / ?l'}" by (auto simp: field_simps)
show "DERIV Φ_p x :> ?φ2 x" unfolding φ_eq[OF x'] φ'_eq Φ_p_def
by (auto intro!: derivative_eq_intros simp add: power2_eq_square algebra_simps) }
qed (simp_all add: field_simps power_eq_if[of _ 2] power_eq_if[of _ 3] power_diff[of "2::real", OF _ ‹l < l'›[THEN less_imp_le]] )

lemma level_shift: "lc > l ⟹ (x :: real) / 2 ^ (lc - Suc l) = x * 2 / 2 ^ (lc - l)"

lemma l2_child: assumes "d < length b"
and p_grid: "p ∈ grid (child b dir d) ds" (is "p ∈ grid ?child ds")
shows "l2_φ (p ! d) (b ! d) = (1 - real_of_int (sgn dir) * (real_of_int (ix p d) / 2^(lv p d - lv b d) - real_of_int (ix b d))) /
2^(lv p d + 1)"
proof -
have "lv ?child d ≤ lv p d" using ‹d < length b› and p_grid
using grid_single_level by auto
hence "lv b d < lv p d" using ‹d < length b› and p_grid
using child_lv by auto

let ?i_c = "ix ?child d" and ?l_c = "lv ?child d"
let ?i_p = "ix p d" and ?l_p = "lv p d"
let ?i_b = "ix b d" and ?l_b = "lv b d"

have "(2::int) * 2^(?l_p - ?l_c) = 2^Suc (?l_p - ?l_c)" by auto
also have "… = 2^(Suc ?l_p - ?l_c)"
proof -
have "Suc (?l_p - ?l_c) = Suc ?l_p - ?l_c"
using ‹lv ?child d ≤ lv p d› by auto
thus ?thesis by auto
qed
also have "… = 2^(?l_p - ?l_b)"
using ‹d < length b› and ‹lv b d < lv p d›
by (auto simp add: child_def lv_def)
finally have level: "2^(?l_p - ?l_b) = (2::int) * 2^(?l_p - ?l_c)" ..

from ‹d < length b› and p_grid
have range_left: "?i_p > (?i_c - 1) * 2^(?l_p - ?l_c)" and
range_right: "?i_p < (?i_c + 1) * 2^(?l_p - ?l_c)"
using grid_estimate by auto

show ?thesis
proof (cases dir)
case left
with child_ix_left[OF ‹d < length b›]
have "(?i_b - 1) * 2^(?l_p - ?l_b) = (?i_c - 1) * 2^(?l_p - ?l_c)" and
"?i_b * 2^(?l_p - ?l_b) = (?i_c + 1) * 2^(?l_p - ?l_c)" using level by auto
hence "?i_p > (?i_b - 1) * 2^(?l_p - ?l_b)" and
"?i_p < ?i_b * 2^(?l_p - ?l_b)"
using range_left and range_right by auto
with ‹?l_b < ?l_p›
have "l2_φ (?l_p, ?i_p) (?l_b, ?i_b) =
(1 + real_of_int ?i_p / 2^(?l_p - ?l_b) - real_of_int ?i_b) / 2^(?l_p + 1)"
by (rule l2_when_left_child)
thus ?thesis using left by (auto simp add: ix_def lv_def)
next
case right
hence "?i_c = 2 * ?i_b + 1" using child_ix_right and ‹d < length b› by auto
hence "?i_b * 2^(?l_p - ?l_b) = (?i_c - 1) * 2^(?l_p - ?l_c)" and
"(?i_b + 1) * 2^(?l_p - ?l_b) = (?i_c + 1) * 2^(?l_p - ?l_c)" using level by auto
hence "?i_p > ?i_b * 2^(?l_p - ?l_b)" and
"?i_p < (?i_b + 1) * 2^(?l_p - ?l_b)"
using range_left and range_right by auto
with ‹?l_b < ?l_p›
have "l2_φ (?l_p, ?i_p) (?l_b, ?i_b) =
(1 - real_of_int ?i_p / 2^(?l_p - ?l_b) + real_of_int ?i_b) / 2^(?l_p + 1)"
by (rule l2_when_right_child)
thus ?thesis using right by (auto simp add: ix_def lv_def)
qed
qed

lemma l2_same: "l2_φ (p!d) (p!d) = 1/3 / 2^(lv p d)"
proof -
have "l2_φ (p!d) (p!d) = l2_φ (lv p d, ix p d) (lv p d, ix p d)"
by (auto simp add: lv_def ix_def)
thus ?thesis using l2_when_same by auto
qed

lemma l2_disjoint: assumes "d < length b" and "p ∈ grid b {d}" and "p' ∈ grid b {d}"
and "p' ∉ grid p {d}" and "lv p' d ≥ lv p d"
shows "l2_φ (p' ! d) (p ! d) = 0"
proof -
have range: "ix p' d > (ix p d + 1) * 2^(lv p' d - lv p d) ∨ ix p' d < (ix p d - 1) * 2^(lv p' d - lv p d)"
proof (rule ccontr)
assume "¬ ?thesis"
hence "ix p' d ≤ (ix p d + 1) * 2^(lv p' d - lv p d)" and "ix p' d ≥ (ix p d - 1) * 2^(lv p' d - lv p d)" by auto
with ‹p' ∈ grid b {d}› and ‹p ∈ grid b {d}› and ‹lv p' d ≥ lv p d› and ‹d < length b›
have "p' ∈ grid p {d}" using grid_part[where p=p and b=b and d=d and p'=p'] by auto
with ‹p' ∉ grid p {d}› show False by auto
qed

have "l2_φ (p' ! d) (p ! d) = l2_φ (lv p' d, ix p' d) (lv p d, ix p d)" by (auto simp add: ix_def lv_def)
also have "… = 0" using range and ‹lv p' d ≥ lv p d› and l2_when_disjoint by auto
finally show ?thesis .
qed

lemma l2_down2:
fixes pc pd p
assumes "d < length pd"
assumes pc_in_grid: "pc ∈ grid (child pd dir d) {d}"
assumes pd_is_child: "pd = child p dir d" (is "pd = ?pd")
shows "l2_φ (pc ! d) (pd ! d) / 2 = l2_φ (pc ! d) (p ! d)"
proof -
have "d < length p" using pd_is_child ‹d < length pd› by auto

moreover
have "pc ∈ grid ?pd {d}" using pd_is_child and grid_child and pc_in_grid by auto
hence "lv p d < lv pc d" using grid_child_level and ‹d < length pd› and pd_is_child by auto

moreover
have "real_of_int (sgn dir) * real_of_int (sgn dir) = 1" by (cases dir, auto)

ultimately show ?thesis
unfolding l2_child[OF ‹d < length pd› pc_in_grid]
l2_child[OF ‹d < length p› ‹pc ∈ grid ?pd {d}›]
using child_lv and child_ix and pd_is_child and level_shift
qed

lemma l2_zigzag:
assumes "d < length p" and p_child: "p = child p_p dir d"
and p'_grid: "p' ∈ grid (child p (inv dir) d) {d}"
and ps_intro: "child p (inv dir) d = child ps dir d" (is "?c_p = ?c_ps")
shows "l2_φ (p' ! d) (p_p ! d) = l2_φ (p' ! d) (ps ! d) + l2_φ (p' ! d) (p ! d) / 2"
proof -
have "length p = length ?c_p" by auto
also have "… = length ?c_ps" using ps_intro by auto
finally have "length p = length ps" using ps_intro by auto
hence "d < length p_p" using p_child and ‹d < length p› by auto

moreover
from ps_intro have "ps = p[d := (lv p d, ix p d - sgn dir)]" by (rule child_neighbour)
hence "lv ps d = lv p d" and "real_of_int (ix ps d) = real_of_int (ix p d) - real_of_int (sgn dir)"
using lv_def and ix_def and ‹length p = length ps› and ‹d < length p› by auto

moreover
have "d < length ps" and *: "p' ∈ grid (child ps dir d) {d}"
using p'_grid ps_intro ‹length p = length ps› ‹d < length p› by auto

have "p' ∈ grid p {d}" using p'_grid and grid_child by auto
hence p_p_grid: "p' ∈ grid (child p_p dir d) {d}" using p_child by auto
hence "lv p' d > lv p_p d" using grid_child_level and ‹d < length p_p› by auto

moreover
have "real_of_int (sgn dir) * real_of_int (sgn dir) = 1" by (cases dir, auto)

ultimately show ?thesis
unfolding l2_child[OF ‹d < length p› p'_grid] l2_child[OF ‹d < length ps› *]
l2_child[OF ‹d < length p_p› p_p_grid]
using child_lv and child_ix and p_child level_shift
qed

end


# Theory UpDown_Scheme

section ‹ UpDown Scheme ›

theory UpDown_Scheme
imports Grid
begin

fun down' :: "nat ⇒ nat ⇒ grid_point ⇒ real ⇒ real ⇒ vector ⇒ vector"
where
"down' d 0       p f⇩l f⇩r α = α"
| "down' d (Suc l) p f⇩l f⇩r α = (let
f⇩m = (f⇩l + f⇩r) / 2 + (α p);
α = α(p := ((f⇩l + f⇩r) / 4 + (1 / 3) * (α p)) / 2 ^ (lv p d));
α = down' d l (child p left d) f⇩l f⇩m α;
α = down' d l (child p right d) f⇩m f⇩r α
in α)"

definition down :: "nat ⇒ nat ⇒ nat ⇒ vector ⇒ vector" where
"down = lift (λ d l p. down' d l p 0 0)"

fun up' :: "nat ⇒ nat ⇒ grid_point ⇒ vector ⇒ (real * real) * vector" where
"up' d       0 p α = ((0, 0), α)"
| "up' d (Suc l) p α = (let
((f⇩l, f⇩m⇩l), α) = up' d l (child p left d) α;
((f⇩m⇩r, f⇩r), α) = up' d l (child p right d) α;
result = (f⇩m⇩l + f⇩m⇩r + (α p) / 2 ^ (lv p d) / 2) / 2
in ((f⇩l + result, f⇩r + result), α(p := f⇩m⇩l + f⇩m⇩r)))"

definition up :: "nat ⇒ nat ⇒ nat ⇒ vector ⇒ vector" where
"up = lift (λ d lm p α. snd (up' d lm p α))"

fun updown' :: "nat ⇒ nat ⇒ nat ⇒ vector ⇒ vector" where
"updown' dm lm 0 α = α"
| "updown' dm lm (Suc d) α =
(sum_vector (updown' dm lm d (up dm lm d α)) (down dm lm d (updown' dm lm d α)))"

definition updown :: "nat ⇒ nat ⇒ vector ⇒ vector" where
"updown dm lm α = updown' dm lm dm α"

end


# Theory Up

section ‹ Up Part ›

theory Up
imports UpDown_Scheme Triangular_Function
begin

lemma up'_inplace:
assumes p'_in: "p' ∉ grid p ds" and "d ∈ ds"
shows "snd (up' d l p α) p' = α p'"
using p'_in
proof (induct l arbitrary: p α)
case (Suc l)
let "?ch dir" = "child p dir d"
let "?up dir α" = "up' d l (?ch dir) α"
let "?upl" = "snd (?up left α)"

from contrapos_nn[OF ‹p' ∉ grid p ds› grid_child[OF ‹d ∈ ds›]]
have left: "p' ∉ grid (?ch left) ds" and
right: "p' ∉ grid (?ch right) ds" by auto

have "p ≠ p'" using grid.Start Suc.prems by auto
with Suc.hyps[OF left, of α] Suc.hyps[OF right, of ?upl]
show ?case
by (cases "?up left α", cases "?up right ?upl", auto simp add: Let_def)
qed auto

lemma up'_fl_fr:
"⟦ d < length p ; p = (child p_r right d) ; p = (child p_l left d) ⟧
⟹ fst (up' d lm p α) =
(∑ p' ∈ lgrid p {d} (lm + level p). (α p') * l2_φ (p' ! d) (p_r ! d),
∑ p' ∈ lgrid p {d} (lm + level p). (α p') * l2_φ (p' ! d) (p_l ! d))"
proof (induct lm arbitrary: p p_l p_r α)
case (Suc lm)
note ‹d < length p›[simp]

from child_ex_neighbour
obtain pc_r pc_l
where pc_r_def: "child p right d = child pc_r (inv right) d"
and pc_l_def: "child p left d = child pc_l (inv left) d" by blast

define pc where "pc dir = (case dir of right ⇒ pc_r | left ⇒ pc_l)" for dir
{ fix dir have "child p (inv dir) d = child (pc (inv dir)) dir d"
by (cases dir, auto simp add: pc_def pc_r_def pc_l_def) } note pc_child = this
{ fix dir have "child p dir d = child (pc dir) (inv dir) d"
by (cases dir, auto simp add: pc_def pc_r_def pc_l_def) } note pc_child_inv = this
hence "!! dir. length (child p dir d) = length (child (pc dir) (inv dir) d)" by auto
hence "!! dir. length p = length (pc dir)" by auto
hence [simp]: "!! dir. d < length (pc dir)" by auto

let ?l = "λs. lm + level s"
let ?C = "λp p'. (α p) * l2_φ (p ! d) (p' ! d)"
let ?sum' = "λs p''. ∑ p' ∈ lgrid s {d} (Suc lm + level p). ?C p' p''"
let ?sum = "λs dir p. ∑ p' ∈ lgrid (child s dir d) {d} (?l (child s dir d)). ?C p' p"
let ?ch = "λdir. child p dir d"
let ?f = "λdir. ?sum p dir (pc dir)"
let ?fm = "λdir. ?sum p dir p"
let ?result = "(?fm left + ?fm right + (α p) / 2 ^ (lv p d) / 2) / 2"
let ?up = "λlm p α. up' d lm p α"

define βl where "βl = snd (?up lm (?ch left) α)"
define βr where "βr = snd (?up lm (?ch right) βl)"

define p_d where "p_d dir = (case dir of right ⇒ p_r | left ⇒ p_l)" for dir
have p_d_child: "p = child (p_d dir) dir d" for dir
using Suc.prems p_d_def by (cases dir) auto
hence "⋀ dir. length p = length (child (p_d dir) dir d)" by auto
hence "⋀ dir. d < length (p_d dir)" by auto

{ fix dir

{ fix p' assume "p' ∈ lgrid (?ch (inv dir)) {d} (?l (?ch (inv dir))) "
hence "?C p' (pc (inv dir)) + (?C p' p) / 2 = ?C p' (p_d dir)"
using l2_zigzag[OF _ p_d_child[of dir] _ pc_child[of dir]]
by (cases dir) (auto simp add: algebra_simps) }
hence inv_dir_sum: "?sum p (inv dir) (pc (inv dir)) + (?sum p (inv dir) p) / 2
= ?sum p (inv dir) (p_d dir)"
by (auto simp add: sum.distrib[symmetric] sum_divide_distrib)

have "?sum p dir p / 2 = ?sum p dir (p_d dir)"
using l2_down2[OF _ _ ‹p = child (p_d dir) dir d›]
by (force intro!: sum.cong simp add: sum_divide_distrib)
moreover
have "?C p (p_d dir) = (α p) / 2 ^ (lv p d) / 4"
using l2_child[OF ‹d < length (p_d dir)›, of p dir "{d}"] p_d_child[of dir]
‹d < length (p_d dir)› child_lv child_ix grid.Start[of p "{d}"]
ultimately
have "?sum' p (p_d dir) =
?sum p (inv dir) (pc (inv dir)) +
(?sum p (inv dir) p) / 2 + ?sum p dir p / 2 + (α p) / 2 ^ (lv p d) / 4"
using lgrid_sum[where b=p] and child_level and inv_dir_sum
by (cases dir) auto
hence "?sum p (inv dir) (pc (inv dir)) + ?result = ?sum' p (p_d dir)"
by (cases dir) auto }
note this[of left] this[of right]
moreover
note eq = up'_inplace[OF grid_not_child[OF ‹d < length p›], of d "{d}" lm]
{ fix p' assume "p' ∈ lgrid (?ch right) {d} (lm + level (?ch right))"
with grid_disjunct[of d p] up'_inplace[of p' "?ch left" "{d}" d lm α] βl_def
have "βl p' = α p'" by auto }
hence "fst (?up (Suc lm) p α) = (?f left + ?result, ?f right + ?result)"
using βl_def pc_child_inv[of left] pc_child_inv[of right]
Suc.hyps[of "?ch left" "pc left" p α] eq[of left α]
Suc.hyps[of "?ch right" p "pc right" βl] eq[of right βl]
by (cases "?up lm (?ch left) α", cases "?up lm (?ch right) βl") (simp add: Let_def)
ultimately show ?case by (auto simp add: p_d_def)
next
case 0
show ?case by simp
qed

lemma up'_β:
"⟦ d < length b ; l + level b = lm ; b ∈ sparsegrid' dm ; p ∈ sparsegrid' dm ⟧
⟹
(snd (up' d l b α)) p =
(if p ∈ lgrid b {d} lm
then ∑ p' ∈ (lgrid p {d} lm) - {p}. α p' * l2_φ (p' ! d) (p ! d)
else α p)"
(is "⟦ _ ; _ ; _ ; _ ⟧ ⟹ (?goal l b p α)")
proof (induct l arbitrary: b p α)
case (Suc l)

let ?l = "child b left d" and ?r = "child b right d"
obtain p_l where p_l_def: "?r = child p_l left d" using child_ex_neighbour[where dir=right] by auto
obtain p_r where p_r_def: "?l = child p_r right d" using child_ex_neighbour[where dir=left] by auto

let ?ul = "up' d l ?l α"
let ?ur = "up' d l ?r (snd ?ul)"

let "?C p'" = "α p' * l2_φ (p' ! d) (p ! d)"
let "?s s" = "∑ p' ∈ (lgrid s {d} lm). ?C p'"

from ‹b ∈ sparsegrid' dm› have "length b = dm" unfolding sparsegrid'_def start_def
by auto
hence "d < dm" using ‹d < length b› by auto

{ fix p' assume "p' ∈ grid ?r {d}"
hence "p' ∉ grid ?l {d}"
using grid_disjunct[OF ‹d < length b›] by auto
hence "snd ?ul p' = α p'" using up'_inplace by auto
} note eq = this

show "?goal (Suc l) b p α"
proof (cases "p = b")
case True

let "?C p'" = "α p' * l2_φ (p' ! d) (b ! d)"
let "?s s" = "∑ p' ∈ (lgrid s {d} lm). ?C p'"

have "d < length ?l" using ‹d < length b› by auto
from up'_fl_fr[OF this p_r_def]
have fml: "snd (fst ?ul) = (∑ p' ∈ lgrid ?l {d} (l + level ?l). ?C p')" by simp

have "d < length ?r" using ‹d < length b› by auto
from up'_fl_fr[OF this _ p_l_def, where α="snd ?ul"]
have fmr: "fst (fst ?ur) = (∑ p' ∈ lgrid ?r {d} (l + level ?r).
((snd ?ul) p') * l2_φ (p' ! d) (b ! d))" by simp

have "level b < lm" using ‹Suc l + level b = lm› by auto
hence "{ b } ⊆ lgrid b {d} lm" unfolding lgrid_def by auto
from sum_diff[OF lgrid_finite this]
have "(∑ p' ∈ (lgrid b {d} lm) - {b}. ?C p') = ?s b - ?C b" by simp
also have "… = ?s ?l + ?s ?r"
using lgrid_sum and ‹level b < lm› and ‹d < length b› by auto
also have "… = snd (fst ?ul) + fst (fst ?ur)" using fml and fmr
and ‹Suc l + level b = lm› and child_level[OF ‹d < length b›]
using eq unfolding True lgrid_def by auto

finally show ?thesis unfolding up'.simps Let_def and fun_upd_def lgrid_def
using ‹p = b› and ‹level b < lm›
by (cases ?ul, cases ?ur, auto)
next
case False

have "?r ∈ sparsegrid' dm" and "?l ∈ sparsegrid' dm"
using ‹b ∈ sparsegrid' dm› and ‹d < dm› unfolding sparsegrid'_def by auto
from Suc.hyps[OF _ _ this(1)] Suc.hyps[OF _ _ this(2)]
have "?goal l ?l p α" and "?goal l ?r p (snd ?ul)"
using ‹d < length b› and ‹Suc l + level b = lm› and ‹p ∈ sparsegrid' dm› by auto

show ?thesis
proof (cases "p ∈ lgrid b {d} lm")
case True
hence "level p < lm" and "p ∈ grid b {d}" unfolding lgrid_def by auto
hence "p ∈ grid ?l {d} ∨ p ∈ grid ?r {d}"
unfolding grid_partition[of b] using ‹p ≠ b› by auto
thus ?thesis
proof (rule disjE)
assume "p ∈ grid (child b left d) {d}"
hence "p ∉ grid (child b right d) {d}"
using grid_disjunct[OF ‹d < length b›] by auto
thus ?thesis
using ‹?goal l ?l p α› and ‹?goal l ?r p (snd ?ul)›
using ‹p ≠ b› ‹p ∈ lgrid b {d} lm›
unfolding lgrid_def grid_partition[of b]
by (cases ?ul, cases ?ur, auto simp add: Let_def)
next
assume *: "p ∈ grid (child b right d) {d}"
hence "p ∉ grid (child b left d) {d}"
using grid_disjunct[OF ‹d < length b›] by auto
moreover
{ fix p' assume "p' ∈ grid p {d}"
from grid_transitive[OF this *] eq[of p']
have "snd ?ul p' = α p'" by simp
}
ultimately show ?thesis
using ‹?goal l ?l p α› and ‹?goal l ?r p (snd ?ul)›
using ‹p ≠ b› ‹p ∈ lgrid b {d} lm› *
unfolding lgrid_def
by (cases ?ul, cases ?ur, auto simp add: Let_def)
qed
next
case False
then have "p ∉ lgrid ?l {d} lm" and "p ∉ lgrid ?r {d} lm"
unfolding lgrid_def and grid_partition[where p=b] by auto
with False show ?thesis using ‹?goal l ?l p α› and ‹?goal l ?r p (snd ?ul)›
using ‹p ≠ b› ‹p ∉ lgrid b {d} lm›
unfolding lgrid_def
by (cases ?ul, cases ?ur, auto simp add: Let_def)
qed
qed
next
case 0
then have "lgrid b {d} lm = {}"
using lgrid_empty'[where p=b and lm=lm and ds="{d}"] by auto
with 0 show ?case unfolding up'.simps by auto
qed

lemma up:
assumes "d < dm" and "p ∈ sparsegrid dm lm"
shows "(up dm lm d α) p = (∑ p' ∈ (lgrid p {d} lm) - {p}. α p' * l2_φ (p' ! d) (p ! d))"
proof -
let ?S = "λ x p p'. if p' ∈ grid p {d} - {p} then x * l2_φ (p'!d) (p!d) else 0"
let ?F = "λ d lm p α. snd (up' d lm p α)"

{ fix p b assume "p ∈ grid b {d}"
from grid_transitive[OF _ this subset_refl subset_refl]
have "lgrid b {d} lm ∩ (grid p {d} - {p}) = lgrid p {d} lm - {p}"
unfolding lgrid_def by auto
} note lgrid_eq = this

{ fix l b p α
assume b: "b ∈ lgrid (start dm) ({0..<dm} - {d}) lm"
hence "b ∈ sparsegrid' dm" and "d < length b" using sparsegrid'_start ‹d < dm› by auto
assume l: "l + level b = lm" and p: "p ∈ sparsegrid dm lm"
note sparsegridE[OF p]

note up' = up'_β[OF ‹d < length b› l ‹b ∈ sparsegrid' dm› ‹p ∈ sparsegrid' dm›]

have "?F d l b α p =
(if b = base {d} p then (∑p'∈lgrid b {d} lm. ?S (α p') p p') else α p)"
proof (cases "b = base {d} p")
case True with baseE(2)[OF ‹p ∈ sparsegrid' dm›] ‹level p < lm›
have "p ∈ lgrid b {d} lm" and "p ∈ grid b {d}" by auto
show ?thesis
using lgrid_eq[OF ‹p ∈ grid b {d}›]
unfolding up' if_P[OF True] if_P[OF ‹p ∈ lgrid b {d} lm›]
by (intro sum.mono_neutral_cong_left lgrid_finite) auto
next
case False
moreover have "p ∉ lgrid b {d} lm"
proof (rule ccontr)
assume "¬ ?thesis"
hence "base {d} p = b" using b by (auto intro!: baseI)
thus False using False by auto
qed
ultimately show ?thesis unfolding up' by auto
qed }
with lift[where F = ?F, OF ‹d < dm› ‹p ∈ sparsegrid dm lm›]
have lift_eq: "lift ?F dm lm d α p =
(∑p'∈lgrid (base {d} p) {d} lm. ?S (α p') p p')" by auto
from lgrid_eq[OF baseE(2)[OF sparsegrid_subset[OF ‹p ∈ sparsegrid dm lm›]]]
show ?thesis
unfolding up_def lift_eq by (intro sum.mono_neutral_cong_right lgrid_finite) auto
qed

end


# Theory Down

section ‹ Down part ›

theory Down
imports Triangular_Function UpDown_Scheme
begin

lemma sparsegrid'_parents:
assumes b: "b ∈ sparsegrid' dm" and p': "p' ∈ parents d b p"
shows "p' ∈ sparsegrid' dm"
using assms parents_def sparsegrid'I by auto

lemma down'_β: "⟦ d < length b ; l + level b = lm ; b ∈ sparsegrid' dm ; p ∈ sparsegrid' dm ⟧ ⟹
down' d l b fl fr α p = (if p ∈ lgrid b {d} lm
then
(fl + (fr - fl) / 2 * (real_of_int (ix p d) / 2^(lv p d - lv b d) - real_of_int (ix b d) + 1)) / 2 ^ (lv p d + 1) +
(∑ p' ∈ parents d b p. (α p') * l2_φ (p ! d) (p' ! d))
else α p)"
proof (induct l arbitrary: b α fl fr p)
case (Suc l)

let ?l = "child b left d" and ?r = "child b right d"
let ?result = "((fl + fr) / 4 + (1 / 3) * (α b)) / 2 ^ (lv b d)"
let ?fm = "(fl + fr) / 2 + (α b)"
let ?down_l = "down' d l (child b left d) fl ?fm (α(b := ?result))"

have "length b = dm" using ‹b ∈ sparsegrid' dm›
unfolding sparsegrid'_def start_def by auto
hence "d < dm" using ‹d < length b› by auto

have "!!dir. d < length (child b dir d)" using ‹d < length b› by auto
have "!!dir. l + level (child b dir d) = lm"
using ‹d < length b› and ‹Suc l + level b = lm› and child_level by auto
have "!!dir. (child b dir d) ∈ sparsegrid' dm"
using ‹b ∈ sparsegrid' dm› and ‹d < dm› and sparsegrid'_def by auto
note hyps = Suc.hyps[OF ‹!! dir. d < length (child b dir d)›
‹!!dir. l + level (child b dir d) = lm›
‹!!dir. (child b dir d) ∈ sparsegrid' dm›]

show ?case
proof (cases "p ∈ lgrid b {d} lm")
case False
moreover hence "p ≠ b" and "p ∉ lgrid ?l {d} lm"
and "p ∉ lgrid ?r {d} lm" unfolding lgrid_def
unfolding grid_partition[where p=b] using ‹Suc l + level b = lm› by auto
ultimately show ?thesis
unfolding down'.simps Let_def fun_upd_def hyps[OF ‹p ∈ sparsegrid' dm›]
by auto
next
case True hence "level p < lm" and "p ∈ grid b {d}" unfolding lgrid_def by auto
let ?lb = "lv b d"   and ?ib = "real_of_int (ix b d)"
let ?lp   = "lv p d"  and ?ip   = "real_of_int (ix p d)"
show ?thesis
proof (cases "∃ dir. p ∈ grid (child b dir d){d}")
case True
obtain dir where p_grid: "p ∈ grid (child b dir d) {d}" using True by auto
hence "p ∈ lgrid (child b dir d) {d} lm" using ‹level p < lm› unfolding lgrid_def by auto
have "lv b d < lv p d" using child_lv[OF ‹d < length b›] and grid_single_level[OF p_grid ‹d < length (child b dir d)›] by auto

let ?ch = "child b dir d"
let ?ich = "child b (inv dir) d"

show ?thesis
proof (cases dir)
case right
hence "p ∈ lgrid ?r {d} lm" and "p ∈ grid ?r {d}"
using ‹p ∈ grid ?ch {d}› and ‹level p < lm› unfolding lgrid_def by auto

{ fix p' fix fl fr x assume p': "p' ∈ parents d (child b right d) p"
hence "p' ∈ grid (child b right d) {d}" unfolding parents_def by simp
hence "p' ∉ lgrid (child b left d) {d} lm" and "p' ≠ b"
unfolding lgrid_def
using grid_disjunct[OF ‹d < length b›] grid_not_child by auto

from hyps[OF sparsegrid'_parents[OF ‹child b right d ∈ sparsegrid' dm›
p']] this
have "down' d l (child b left d) fl fr (α(b := x)) p' = α p'" by auto }
thus  ?thesis
unfolding down'.simps Let_def hyps[OF ‹p ∈ sparsegrid' dm›]
parent_sum[OF ‹p ∈ grid ?r {d}› ‹d < length b›]
l2_child[OF ‹d < length b› ‹p ∈ grid ?r {d}›]
using child_ix child_lv ‹d < length b› level_shift[OF ‹lv b d < lv p d›]
sgn.simps ‹p ∈ lgrid b {d} lm› ‹p ∈ lgrid ?r {d} lm›
next
case left
hence "p ∈ lgrid ?l {d} lm" and "p ∈ grid ?l {d}"
using ‹p ∈ grid ?ch {d}› and ‹level p < lm› unfolding lgrid_def by auto
hence "¬ p ∈ lgrid ?r {d} lm"
using grid_disjunct[OF ‹d < length b›] unfolding lgrid_def by auto
{ fix p' assume p': "p' ∈ parents d (child b left d) p"
hence "p' ∈ grid (child b left d) {d}" unfolding parents_def by simp
hence "p' ≠ b" using grid_not_child[OF ‹d < length b›] by auto }
thus ?thesis
unfolding down'.simps Let_def hyps[OF ‹p ∈ sparsegrid' dm›]
parent_sum[OF ‹p ∈ grid ?l {d}› ‹d < length b›]
l2_child[OF ‹d < length b› ‹p ∈ grid ?l {d}›] sgn.simps
if_P[OF ‹p ∈ lgrid b {d} lm›] if_P[OF ‹p ∈ lgrid ?l {d} lm›]
if_not_P[OF ‹p ∉ lgrid ?r {d} lm›]
using child_ix child_lv ‹d < length b› level_shift[OF ‹lv b d < lv p d›]
qed
next
case False hence not_child: "!! dir. ¬ p ∈ grid (child b dir d) {d}" by auto
hence "p = b" using grid_onedim_split[where ds="{}" and d=d and b=b] ‹p ∈ grid b {d}› unfolding grid_empty_ds[where b=b] by auto
from not_child have lnot_child: "!! dir. ¬ p ∈ lgrid (child b dir d) {d} lm" unfolding lgrid_def by auto
have result: "((fl + fr) / 4 + 1 / 3 * α b) / 2 ^ lv b d = (fl + (fr - fl) / 2) / 2 ^ (lv b d + 1) + α b * l2_φ (b ! d) (b ! d)"
by (auto simp: l2_same diff_divide_distrib add_divide_distrib times_divide_eq_left[symmetric] algebra_simps)
show ?thesis
unfolding down'.simps Let_def fun_upd_def hyps[OF ‹p ∈ sparsegrid' dm›] if_P[OF ‹p ∈ lgrid b {d} lm›] if_not_P[OF lnot_child] if_P[OF ‹p = b›]
unfolding ‹p = b› parents_single unfolding result by auto
qed
qed
next
case 0
have "p ∉ lgrid b {d} lm"
proof (rule ccontr)
assume "¬ p ∉ lgrid b {d} lm"
hence "p ∈ grid b {d}" and "level p < lm" unfolding lgrid_def by auto
moreover from grid_level[OF ‹p ∈ grid b {d}›] and ‹0 + level b = lm› have "lm ≤ level p" by auto
ultimately show False by auto
qed
thus ?case unfolding down'.simps by auto
qed

lemma down: assumes "d < dm" and p: "p ∈ sparsegrid dm lm"
shows "(down dm lm d α) p = (∑ p' ∈ parents d (base {d} p) p. (α p') * l2_φ (p ! d) (p' ! d))"
proof -
let "?F d l p" = "down' d l p 0 0"
let "?S x p p'" = "if p' ∈ parents d (base {d} p) p then x * l2_φ (p ! d) (p' ! d) else 0"

{ fix p α assume "p ∈ sparsegrid dm lm"
from le_less_trans[OF grid_level sparsegridE(2)[OF this]]
have "parents d (base {d} p) p ⊆  lgrid (base {d} p) {d} lm"
unfolding lgrid_def parents_def by auto
hence "(∑p'∈lgrid (base {d} p) {d} lm. ?S (α p') p p') =
(∑p'∈parents d (base {d} p) p. α p' * l2_φ (p ! d) (p' ! d))"
using lgrid_finite by (intro sum.mono_neutral_cong_right) auto
} note sum_eq = this

{ fix l p b α
assume b: "b ∈ lgrid (start dm) ({0..<dm} - {d}) lm" and "l + level b = lm"
and "p ∈ sparsegrid dm lm"
hence b_spg: "b ∈ sparsegrid' dm" and p_spg: "p ∈ sparsegrid' dm" and
"d < length b" and "level p < lm"
using sparsegrid'_start sparsegrid_subset ‹d < dm› by auto
have "?F d l b α p = (if b = base {d} p then ∑p'∈lgrid b {d} lm. ?S (α p') p p' else α p)"
proof (cases "b = base {d} p")
case True
have "p ∈ lgrid (base {d} p) {d} lm"
using baseE(2)[OF p_spg] and ‹level p < lm›
unfolding lgrid_def by auto
thus ?thesis unfolding if_P[OF True]
unfolding True sum_eq[OF ‹p ∈ sparsegrid dm lm›]
unfolding down'_β[OF ‹d < length b› ‹l + level b = lm› b_spg p_spg,
unfolded True] by auto
next
case False
have "p ∉ lgrid b {d} lm"
proof (rule ccontr)
assume "¬ ?thesis" hence "p ∈ grid b {d}" by auto
from b this have "b = base {d} p" using baseI by auto
thus False using False by simp
qed
thus ?thesis
unfolding if_not_P[OF False]
unfolding down'_β[OF ‹d < length b› ‹l + level b = lm› b_spg p_spg]
by auto
qed }
from lift[OF ‹d < dm› ‹p ∈ sparsegrid dm lm›, where F = ?F and S = ?S, OF this]
show ?thesis
unfolding down_def
unfolding sum_eq[OF p] by simp
qed

end


# Theory Up_Down

section ‹ UpDown  ›

(* Definition of sparse grids, hierarchical bases and the up-down algorithm.
*
* Based on "updown_L2-Skalarprodukt.mws" from Dirk Pflüger <pflueged@in.tum.de>
*
* Author: Johannes Hölzl <hoelzl@in.tum.de>
*)
theory Up_Down
imports Up Down
begin

lemma updown': "⟦ d ≤ dm; p ∈ sparsegrid dm lm ⟧
⟹ (updown' dm lm d α) p = (∑ p' ∈ lgrid (base {0 ..< d} p) {0 ..< d} lm. α p' * (∏ d' ∈ {0 ..< d}. l2_φ (p' ! d') (p ! d')))"
(is "⟦ _ ; _ ⟧ ⟹ _ = (∑ p' ∈ ?subgrid d p. α p' * ?prod d p' p)")
proof (induct d arbitrary: α p)
case 0 hence "?subgrid 0 p = {p}" using base_empty unfolding lgrid_def and sparsegrid_def sparsegrid'_def by auto
thus ?case unfolding updown'.simps by auto
next
case (Suc d)
let "?leafs p" = "(lgrid p {d} lm) - {p}"
let "?parents" = "parents d (base {d} p) p"
let ?b = "base {0..<d} p"
have "d < dm" using ‹Suc d ≤ dm› by auto

have p_spg: "p ∈ grid (start dm) {0..<dm}" and p_spg': "p ∈ sparsegrid' dm" and "level p < lm" using ‹p ∈ sparsegrid dm lm›
unfolding sparsegrid_def and sparsegrid'_def and lgrid_def by auto
have p'_in_spg: "!! p'. p' ∈ ?subgrid d p ⟹ p' ∈ sparsegrid dm lm"
using base_grid[OF p_spg'] unfolding sparsegrid'_def sparsegrid_def lgrid_def by auto

from baseE[OF p_spg', where ds="{0..<d}"]
have "?b ∈ grid (start dm) {d..<dm}" and p_bgrid: "p ∈ grid ?b {0..<d}" by auto
hence "d < length ?b" using ‹Suc d ≤ dm› by auto
have "p ! d = ?b ! d" using base_out[OF _ _ p_spg'] ‹Suc d ≤ dm› by auto

have "length p = dm" using ‹p ∈ sparsegrid dm lm› unfolding sparsegrid_def lgrid_def by auto
hence "d < length p" using ‹d < dm› by auto

have "updown' dm lm d (up dm lm d α) p =
(∑ p' ∈ ?subgrid d p. (up dm lm d α) p' * (?prod d p' p))"
using Suc by auto
also have "… = (∑ p' ∈ ?subgrid d p. (∑ p'' ∈ ?leafs p'. α p'' * ?prod (Suc d) p'' p))"
proof (intro sum.cong refl)
fix p' assume "p' ∈ ?subgrid d p"
hence "d < length p'" unfolding lgrid_def using base_length[OF p_spg'] ‹Suc d ≤ dm› by auto

have "up dm lm d α p' * ?prod d p' p =
(∑ p'' ∈ ?leafs p'. α p'' * l2_φ (p'' ! d) (p' ! d)) * ?prod d p' p"
using ‹p' ∈ ?subgrid d p› up ‹Suc d ≤ dm› p'_in_spg by auto
also have "… = (∑ p'' ∈ ?leafs p'. α p'' * l2_φ (p'' ! d) (p' ! d) * ?prod d p' p)"
using sum_distrib_right by auto
also have "… = (∑ p'' ∈ ?leafs p'. α p'' * ?prod (Suc d) p'' p)"
proof (intro sum.cong refl)
fix p'' assume "p'' ∈ ?leafs p'"
have "?prod d p' p = ?prod d p'' p"
proof (intro prod.cong refl)
fix d' assume "d' ∈ {0..<d}"
hence d_lt_p: "d' < length p'" and d'_not_d: "d' ∉ {d}" using ‹d < length p'› by auto
hence "p' ! d' = p'' ! d'" using ‹p'' ∈ ?leafs p'› grid_invariant[OF d_lt_p d'_not_d] unfolding lgrid_def by auto
thus "l2_φ (p'!d') (p!d') = l2_φ (p''!d') (p!d')" by auto
qed
moreover have "p' ! d = p ! d"
using ‹p' ∈ ?subgrid d p› and grid_invariant[OF ‹d < length ?b›, where p=p' and ds="{0..<d}"] unfolding lgrid_def ‹p ! d = ?b ! d› by auto
ultimately have "l2_φ (p'' ! d) (p' ! d) * ?prod d p' p =
l2_φ (p'' ! d) (p ! d) * ?prod d p'' p" by auto
also have "… = ?prod (Suc d) p'' p"
proof -
have "insert d {0..<d} = {0..<Suc d}" by auto
moreover from prod.insert
have "prod (λ d'. l2_φ (p'' ! d') (p ! d')) (insert d {0..<d}) =
(λ d'. l2_φ (p'' ! d') (p ! d')) d * prod (λ d'. l2_φ (p'' ! d') (p ! d')) {0..<d}"
by auto
ultimately show ?thesis by auto
qed
finally show "α p'' * l2_φ (p'' ! d) (p' ! d) * ?prod d p' p = α p'' * ?prod (Suc d) p'' p" by auto
qed
finally show "(up dm lm d α) p' * (?prod d p' p) = (∑ p'' ∈ ?leafs p'. α p'' * ?prod (Suc d) p'' p)" by auto
qed
also have "… = (∑ (p', p'') ∈ Sigma (?subgrid d p) (λp'. (?leafs p')). (α p'') * (?prod (Suc d) p'' p))"
by (rule sum.Sigma, auto simp add: lgrid_finite)
also have "… = (∑ p''' ∈ (⋃ p' ∈ ?subgrid d p. (⋃ p'' ∈ ?leafs p'. { (p', p'') })).
(((λ p''. α p'' * ?prod (Suc d) p'' p) o snd) p''') )" unfolding Sigma_def by (rule sum.cong[OF refl], auto)
also have "… = (∑ p'' ∈ snd  (⋃ p' ∈ ?subgrid d p. (⋃ p'' ∈ ?leafs p'. { (p', p'') })).
α p'' * (?prod (Suc d) p'' p))" unfolding lgrid_def
by (rule sum.reindex[symmetric],
rule subset_inj_on[OF grid_grid_inj_on[OF ivl_disj_int(15)[where l=0 and m="d" and u="d"], where b="?b"]])
auto
also have "… = (∑ p'' ∈ (⋃ p' ∈ ?subgrid d p. (⋃ p'' ∈ ?leafs p'. snd  { (p', p'') })).
α p'' * (?prod (Suc d) p'' p))" by (auto simp only: image_UN)
also have "… = (∑ p'' ∈ (⋃ p' ∈ ?subgrid d p. ?leafs p'). α p'' * (?prod (Suc d) p'' p))" by auto
finally have up_part: "updown' dm lm d (up dm lm d α) p = (∑ p'' ∈ (⋃ p' ∈ ?subgrid d p. ?leafs p'). α p'' * (?prod (Suc d) p'' p))" .

have "down dm lm d (updown' dm lm d α) p = (∑ p' ∈ ?parents. (updown' dm lm d α p') * l2_φ (p ! d) (p' ! d))"
using ‹Suc d ≤ dm› and down and ‹p ∈ sparsegrid dm lm› by auto
also have "… = (∑ p' ∈ ?parents. ∑ p'' ∈ ?subgrid d p'. α p'' * ?prod (Suc d) p'' p)"
proof (rule sum.cong[OF refl])
fix p' let ?b' = "base {d} p"
assume "p' ∈ ?parents"
hence p_lgrid: "p' ∈ lgrid ?b' {d} (level p + 1)" using parents_subset_lgrid by auto
hence "p' ∈ sparsegrid dm lm" and p'_spg': "p' ∈ sparsegrid' dm" using ‹level p < lm› base_grid[OF p_spg'] unfolding sparsegrid_def lgrid_def sparsegrid'_def by auto
hence "length p' = dm" unfolding sparsegrid_def lgrid_def by auto
hence "d < length p'" using ‹Suc d ≤ dm› by auto

from p_lgrid have p'_grid: "p' ∈ grid ?b' {d}" unfolding lgrid_def by auto

have "(updown' dm lm d α p') * l2_φ (p ! d) (p' !  d) = (∑ p'' ∈ ?subgrid d p'. α p'' * ?prod d p'' p') * l2_φ (p ! d) (p' ! d)"
using ‹p' ∈ sparsegrid dm lm› Suc by auto
also have "… = (∑ p'' ∈ ?subgrid d p'. α p'' * ?prod d p'' p' * l2_φ (p ! d) (p' ! d))"
using sum_distrib_right by auto
also have "… = (∑ p'' ∈ ?subgrid d p'. α p'' * ?prod (Suc d) p'' p)"
proof (rule sum.cong[OF refl])
fix p'' assume "p'' ∈ ?subgrid d p'"

have "?prod d p'' p' = ?prod d p'' p"
proof (rule prod.cong, rule refl)
fix d' assume "d' ∈ {0..<d}"
hence "d' < dm" and "d' ∉ {d}" using ‹Suc d ≤ dm› by auto
from grid_base_out[OF this p_spg' p'_grid]
show "l2_φ (p''!d') (p'!d') = l2_φ (p''!d') (p!d')" by auto
qed
moreover
have "l2_φ (p ! d) (p' ! d) = l2_φ (p'' ! d) (p ! d)"
proof -
have "d < dm" and "d ∉ {0..<d}" using ‹Suc d ≤ dm› base_length p'_spg' by auto
from grid_base_out[OF this p'_spg'] ‹p'' ∈ ?subgrid d p'›[unfolded lgrid_def]
show ?thesis using l2_commutative by auto
qed
moreover have "?prod d p'' p * l2_φ (p'' ! d) (p ! d) = ?prod (Suc d) p'' p"
proof -
have "insert d {0..<d} = {0..<Suc d}" by auto
moreover from prod.insert
have "(λ d'. l2_φ (p'' ! d') (p ! d')) d * prod (λ d'. l2_φ (p'' ! d') (p ! d')) {0..<d} =
prod (λ d'. l2_φ (p'' ! d') (p ! d')) (insert d {0..<d})"
by auto
hence "(prod (λ d'. l2_φ (p'' ! d') (p ! d')) {0..<d}) * (λ d'. l2_φ (p'' ! d') (p ! d')) d =
prod (λ d'. l2_φ (p'' ! d') (p ! d')) (insert d {0..<d})"
by auto
ultimately show ?thesis by auto
qed
ultimately show "α p'' * ?prod d p'' p' * l2_φ (p ! d) (p' ! d) = α p'' * ?prod (Suc d) p'' p" by auto
qed
finally show "(updown' dm lm d α p') * l2_φ (p ! d) (p' ! d) = (∑ p'' ∈ ?subgrid d p'. α p'' * ?prod (Suc d) p'' p)" by auto
qed
also have "… = (∑ (p', p'') ∈ (Sigma ?parents (?subgrid d)). α p'' * ?prod (Suc d) p'' p)"
by (rule sum.Sigma, auto simp add: parents_finite lgrid_finite)
also have "… = (∑ p''' ∈ (⋃ p' ∈ ?parents. (⋃ p'' ∈ ?subgrid d p'. { (p', p'') })).
( ((λ p''. α p'' * ?prod (Suc d) p'' p) o snd) p''') )" unfolding Sigma_def by (rule sum.cong[OF refl], auto)
also have "… = (∑ p'' ∈ snd  (⋃ p' ∈ ?parents. (⋃ p'' ∈ ?subgrid d p'. { (p', p'') })). α p'' * (?prod (Suc d) p'' p))"
proof (rule sum.reindex[symmetric], rule inj_onI)
fix x y
assume "x ∈ (⋃p'∈parents d (base {d} p) p. ⋃p''∈lgrid (base {0..<d} p') {0..<d} lm. {(p', p'')})"
hence x_snd: "snd x ∈ grid (base {0..<d} (fst x)) {0..<d}" and "fst x ∈ grid (base {d} p) {d}" and "p ∈ grid (fst x) {d}"
unfolding parents_def lgrid_def by auto
hence x_spg: "fst x ∈ sparsegrid' dm" using base_grid[OF p_spg'] by auto

assume "y ∈ (⋃p'∈parents d (base {d} p) p. ⋃p''∈lgrid (base {0..<d} p') {0..<d} lm. {(p', p'')})"
hence y_snd: "snd y ∈ grid (base {0..<d} (fst y)) {0..<d}" and "fst y ∈ grid (base {d} p) {d}" and "p ∈ grid (fst y) {d}"
unfolding parents_def lgrid_def by auto
hence y_spg: "fst y ∈ sparsegrid' dm" using base_grid[OF p_spg'] by auto
hence "length (fst y) = dm" unfolding sparsegrid'_def by auto

assume "snd x = snd y"
have "fst x = fst y"
proof (rule nth_equalityI)
show l_eq: "length (fst x) = length (fst y)" using grid_length[OF ‹p ∈ grid (fst y) {d}›] grid_length[OF ‹p ∈ grid (fst x) {d}›]
by auto
show "fst x ! i = fst y ! i" if "i < length (fst x)" for i
proof -
have "i < length (fst y)" and "i < dm" using that l_eq and ‹length (fst y) = dm› by auto
show "fst x ! i = fst y ! i"
proof (cases "i = d")
case False hence "i ∉ {d}" by auto
with grid_invariant[OF ‹i < length (fst x)› this ‹p ∈ grid (fst x) {d}›]
grid_invariant[OF ‹i < length (fst y)› this ‹p ∈ grid (fst y) {d}›]
show ?thesis by auto
next
case True with grid_base_out[OF ‹i < dm› _ y_spg y_snd] grid_base_out[OF ‹i < dm› _ x_spg x_snd]
show ?thesis using ‹snd x = snd y› by auto
qed
qed
qed
show "x = y" using prod_eqI[OF ‹fst x = fst y› ‹snd x = snd y›] .
qed
also have "… = (∑ p'' ∈ (⋃ p' ∈ ?parents. (⋃ p'' ∈ ?subgrid d p'. snd  { (p', p'') })).
α p'' * (?prod (Suc d) p'' p))" by (auto simp only: image_UN)
also have "… = (∑ p'' ∈ (⋃ p' ∈ ?parents. ?subgrid d p'). α p'' * ?prod (Suc d) p'' p)" by auto
finally have down_part: "down dm lm d (updown' dm lm d α) p =
(∑ p'' ∈ (⋃ p' ∈ ?parents. ?subgrid d p'). α p'' * ?prod (Suc d) p'' p)" .

have "updown' dm lm (Suc d) α p =
(∑ p'' ∈ (⋃ p' ∈ ?subgrid d p. ?leafs p'). α p'' * ?prod (Suc d) p'' p) +
(∑ p'' ∈ (⋃ p' ∈ ?parents. ?subgrid d p'). α p'' * ?prod (Suc d) p'' p)"
unfolding sum_vector_def updown'.simps down_part and up_part ..
also have "… = (∑ p'' ∈ (⋃ p' ∈ ?subgrid d p. ?leafs p') ∪ (⋃ p' ∈ ?parents. ?subgrid d p'). α p'' * ?prod (Suc d) p'' p)"
rule iffD2[OF disjoint_iff_not_equal], rule ballI, rule ballI)
fix x y
assume "x ∈ (⋃ p' ∈ ?subgrid d p. ?leafs p')"
then obtain px where "px ∈ grid (base {0..<d} p) {0..<d}" and "x ∈ grid px {d}" and "x ≠ px" unfolding lgrid_def by auto
with grid_base_out[OF _ _ p_spg' this(1)] ‹Suc d ≤ dm› base_length[OF p_spg'] grid_level_d
have "lv px d < lv x d" and "px ! d = p ! d" by auto
hence "lv p d < lv x d" unfolding lv_def by auto
moreover
assume "y ∈ (⋃ p' ∈ ?parents. ?subgrid d p')"
then obtain py where y_grid: "y ∈ grid (base {0..<d} py) {0..<d}" and "py ∈ ?parents" unfolding lgrid_def by auto
hence "py ∈ grid (base {d} p) {d}" and "p ∈ grid py {d}" unfolding parents_def by auto
hence py_spg: "py ∈ sparsegrid' dm" using base_grid[OF p_spg'] by auto
have "y ! d = py ! d" using grid_base_out[OF _ _ py_spg y_grid] ‹Suc d ≤ dm› by auto
hence "lv y d ≤ lv p d" using grid_single_level[OF ‹p ∈ grid py {d}›] ‹Suc d ≤ dm› and sparsegrid'_length[OF py_spg] unfolding lv_def by auto
ultimately
show "x ≠ y" by auto
qed
also have "… = (∑ p' ∈ ?subgrid (Suc d) p. α p' * ?prod (Suc d) p' p)" (is "(∑ x ∈ ?in. ?F x) = (∑ x ∈ ?out. ?F x)")
proof (rule sum.mono_neutral_left, simp add: lgrid_finite)
show "?in ⊆ ?out" (is "?children ∪ ?siblings ⊆ _")
proof (rule subsetI)
fix x assume "x ∈ ?in"
show "x ∈ ?out"
proof (cases "x ∈ ?children")
case False hence "x ∈ ?siblings" using ‹x ∈ ?in› by auto
then obtain px where "px ∈ parents d (base {d} p) p" and "x ∈ lgrid (base {0..<d} px) {0..<d} lm" by auto
hence "level x < lm" and "px ∈ grid (base {d} p) {d}" and "x ∈ grid (base {0..<d} px) {0..<d}" and "{d} ∪ {0..<d} = {0..<Suc d}" unfolding lgrid_def parents_def by auto
with grid_base_union[OF p_spg' this(2) this(3)] show ?thesis unfolding lgrid_def by auto
next
have d_eq: "{0..<Suc d} ∪ {d} = {0..<Suc d}" by auto
case True
then obtain px where "px ∈ ?subgrid d p" and "x ∈ lgrid px {d} lm" and "x ≠ px" by auto
hence "px ∈ grid (base {0..<d} p) {0..<d}" and "x ∈ grid px {d}" and "level x < lm" and "{d} ∪ {0..<d} = {0..<Suc d}" unfolding lgrid_def by auto
have "px ∈ grid (base {0..<Suc d} p) {0..<Suc d}" by auto
from grid_transitive[OF ‹x ∈ grid px {d}› this]
show ?thesis unfolding lgrid_def using ‹level x < lm› d_eq by auto
qed
qed

show "∀ x ∈ ?out - ?in. ?F x = 0"
proof
fix x assume "x ∈ ?out - ?in"

hence "x ∈ ?out" and up_ps': "!! p'. p' ∈ ?subgrid d p ⟹ x ∉ lgrid p' {d} lm - {p'}"
and down_ps': "!! p'. p' ∈ ?parents ⟹ x ∉ ?subgrid d p'" by auto
hence x_eq: "x ∈ grid (base {0..<Suc d} p) {0..<Suc d}" and "level x < lm" unfolding lgrid_def by auto
hence up_ps: "!! p'. p' ∈ ?subgrid d p ⟹ x ∉ grid p' {d} - {p'}" and
down_ps: "!! p'. p' ∈ ?parents ⟹ x ∉ grid (base {0..<d} p') {0..<d}"
using up_ps' down_ps' unfolding lgrid_def by auto

have ds_eq: "{0..<Suc d} = {0..<d} ∪ {d}" by auto
have "x ∉ grid (base {0..<d} p) {0..<Suc d} - grid (base {0..<d} p) {0..<d}"
proof
assume "x ∈ grid (base {0..<d} p) {0..<Suc d} - grid (base {0..<d} p) {0..<d}"
hence "x ∈ grid (base {0..<d} p) ({d} ∪ {0..<d})" and x_ngrid: "x ∉ grid (base {0..<d} p) {0..<d}" using ds_eq by auto
from grid_split[OF this(1)] obtain px where px_grid: "px ∈ grid (base {0..<d} p) {0..<d}" and "x ∈ grid px {d}" by auto
from grid_level[OF this(2)] ‹level x < lm› have "level px < lm" by auto
hence "px ∈ ?subgrid d p" using px_grid unfolding lgrid_def by auto
hence "x ∉ grid px {d} - {px}" using up_ps by auto
moreover have "x ≠ px" proof (rule ccontr) assume "¬ x ≠ px" with px_grid and x_ngrid show False by auto qed
ultimately show False using ‹x ∈ grid px {d}› by auto
qed
moreover have "p ∈ ?parents" unfolding parents_def using baseE(2)[OF p_spg'] by auto
hence "x ∉ grid (base {0..<d} p) {0..<d}" by (rule down_ps)
ultimately have x_ngrid: "x ∉ grid (base {0..<d} p) {0..<Suc d}" by auto

have x_spg: "x ∈ sparsegrid' dm" using base_grid[OF p_spg'] x_eq by auto
hence "length x = dm" using grid_length by auto

let ?bx = "base {0..<d} x" and ?bp = "base {0..<d} p" and ?bx1 = "base {d} x" and ?bp1 = "base {d} p" and ?px = "p[d := x ! d]"

have x_nochild_p: "?bx ∉ grid ?bp {d}"
proof (rule ccontr)
assume "¬ base {0..<d} x ∉ grid (base {0..<d} p) {d}"
hence "base {0..<d} x ∈ grid (base {0..<d} p) {d}" by auto
from grid_transitive[OF baseE(2)[OF x_spg] this]
have "x ∈ grid (base {0..<d} p) {0..<Suc d}" using ds_eq by auto
thus False using x_ngrid by auto
qed

have "d < length ?bx" and "d < length ?bp" and "d < length ?bx1" and "d < length ?bp1"