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