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}"]
      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