Theory UpDown_Scheme

theory UpDown_Scheme
imports Grid
section ‹ UpDown Scheme ›

theory UpDown_Scheme
  imports Grid
begin

fun down' :: "nat ⇒ nat ⇒ grid_point ⇒ real ⇒ real ⇒ vector ⇒ vector"
where
  "down' d 0       p fl fr α = α"
| "down' d (Suc l) p fl fr α = (let
      fm = (fl + fr) / 2 + (α p);
      α = α(p := ((fl + fr) / 4 + (1 / 3) * (α p)) / 2 ^ (lv p d));
      α = down' d l (child p left d) fl fm α;
      α = down' d l (child p right d) fm fr α
    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
      ((fl, fml), α) = up' d l (child p left d) α;
      ((fmr, fr), α) = up' d l (child p right d) α;
      result = (fml + fmr + (α p) / 2 ^ (lv p d) / 2) / 2
    in ((fl + result, fr + result), α(p := fml + fmr)))"


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