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