# Theory Up

theory Up
imports UpDown_Scheme Triangular_Function
```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}"]
by (cases dir) (auto simp add: add_divide_distrib field_simps)
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
```