Quelle  Streams.thy

(*<*)
(*
 * The worker/wrapper transformation, following Gill and Hutton.
 * (C)opyright 2009-2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory Streams
imports
  HOLCF
  Nats
  WorkerWrapper
begin
(*>*)

section‹Memoisation using streams.›

text ‹
 label{sec:memoisation-example}›

subsection‹Streams.›

text‹The type of infinite streams.›

domain 'a Stream = stcons (lazy sthead :: "'a") (lazy sttail :: "'a Stream") (infixr ‹&&› 65)

(*<*)
lemma Stream_bisimI[intro]:
  "(∧xs ys. R xs ys
     ==> (xs = ⊥ ∧ ys = ⊥)
       ∨ (∃h t t'. R t t' ∧ xs = h && t ∧ ys = h && t'))
  ==> Stream_bisim R"
  unfolding Stream.bisim_def by auto
(*>*)

fixrec smap :: "('a → 'b) → 'a Stream → 'b Stream"
where
  "smap⋅f⋅(x && xs) = f⋅x && smap⋅f⋅xs"

(*<*)
lemma smap_strict[simp]: "smap⋅f⋅⊥ = ⊥"
by fixrec_simp
(*>*)

lemma smap_smap: "smap⋅f⋅(smap⋅g⋅xs) = smap⋅(f oo g)⋅xs"
(*<*) by (induct xs, simp_all) (*>*)

fixrec i_th :: "'a Stream → Nat → 'a"
where
  "i_th⋅(x && xs) = Nat_case⋅x⋅(i_th⋅xs)"

abbreviation
  i_th_syn :: "'a Stream ==> Nat ==> 'a" (infixl ‹!!› 100) where
  "s !! i ≡ i_th⋅s⋅i"

(*<*)
lemma i_th_strict1[simp]: "⊥ !! i = ⊥"
by fixrec_simp

lemma i_th_strict2[simp]: "s !! ⊥ = ⊥" by (subst i_th.unfold, cases s, simp_all)
lemma i_th_0[simp]: "(s !! 0) = sthead⋅s" by (subst i_th.unfold, cases s, simp_all)
lemma i_th_suc[simp]: "i ≠ ⊥ ==> (x && xs) !! (i + 1) = xs !! i" by (subst i_th.unfold, simp)
(*>*)

text‹The infinite stream of natural numbers.›

fixrec nats :: "Nat Stream"
where
  "nats = 0 && smap⋅(Λ x. 1 + x)⋅nats"

(*<*)
declare nats.simps[simp del]
(*>*)

subsection‹The wrapper/unwrapper functions.›

definition
  unwrapS' :: "(Nat → 'a) → 'a Stream" where
  "unwrapS' ≡ Λ f . smap⋅f⋅nats"

lemma unwrapS'_unfold: "unwrapS'⋅f = f⋅0 && smap⋅(f oo (Λ x. 1 + x))⋅nats"
(*<*)by (unfold unwrapS'_def, subst nats.unfold, simp add: smap_smap)(*>*)

fixrec unwrapS :: "(Nat → 'a) → 'a Stream"
where
  "unwrapS⋅f = f⋅0 && unwrapS⋅(f oo (Λ x. 1 + x))"

(*<*)
declare unwrapS.simps[simp del]
(*>*)

text‹The two versions of @{term "unwrapS"} are equivalent. We could
  to fold some definitions here but it's easier if the stream
  is manifest.›

lemma unwrapS_unwrapS'_eq: "unwrapS = unwrapS'" (is "?lhs = ?rhs")
proof(rule cfun_eqI)
  fix f show "?lhs⋅f = ?rhs⋅f"
  proof(coinduct rule: Stream.coinduct)
    let ?R = "λs s'. (∃f. s = f⋅0 && unwrapS⋅(f oo (Λ x. 1 + x))
                        ∧ s' = f⋅0 && smap⋅(f oo (Λ x. 1 + x))⋅nats)"
    show "Stream_bisim ?R"
    proof
      fix s s' assume "?R s s'"
      then obtain f where fs:  "s = f⋅0 && unwrapS⋅(f oo (Λ x. 1 + x))"
                      and fs': "s' = f⋅0 && smap⋅(f oo (Λ x. 1 + x))⋅nats"
        by blast
      have "?R (unwrapS⋅(f oo (Λ x. 1 + x))) (smap⋅(f oo (Λ x. 1 + x))⋅nats)"
        by ( rule exI[where x="f oo (Λ x. 1 + x)"]
           , subst unwrapS.unfold, subst nats.unfold, simp add: smap_smap)
      with fs fs'
      show "(s = ⊥ ∧ s' = ⊥)
          ∨ (∃h t t'.
              (∃f. t = f⋅0 && unwrapS⋅(f oo (Λ x. 1 + x))
                 ∧ t' = f⋅0 && smap⋅(f oo (Λ x. 1 + x))⋅nats)
                 ∧ s = h && t ∧ s' = h && t')" by best
    qed
    show "?R (?lhs⋅f) (?rhs⋅f)"
    proof -
      have lhs: "?lhs⋅f = f⋅0 && unwrapS⋅(f oo (Λ x. 1 + x))" by (subst unwrapS.unfold, simp)
      have rhs: "?rhs⋅f = f⋅0 && smap⋅(f oo (Λ x. 1 + x))⋅nats" by (rule unwrapS'_unfold)
      from lhs rhs show ?thesis by best
    qed
  qed
qed

definition
  wrapS :: "'a Stream → Nat → 'a" where
  "wrapS ≡ Λ s i . s !! i"

text‹Note the identity requires that @{term "f"} be
 . 🍋‹‹\S6.1› in "GillHutton:2009"› do not make this requirement,
  oversight on their part.

  practice all functions worth memoising are strict in the memoised
 .›

lemma wrapS_unwrapS_id':
  assumes strictF: "(f::Nat → 'a)⋅⊥ = ⊥"
  shows "unwrapS⋅f !! n = f⋅n"
using strictF
proof(induct n arbitrary: f rule: Nat_induct)
  case bottom with strictF show ?case by simp
next
  case zero thus ?case by (subst unwrapS.unfold, simp)
next
  case (Suc i f)
  have "unwrapS⋅f !! (i + 1) = (f⋅0 && unwrapS⋅(f oo (Λ x. 1 + x))) !! (i + 1)"
    by (subst unwrapS.unfold, simp)
  also from Suc have "… = unwrapS⋅(f oo (Λ x. 1 + x)) !! i" by simp
  also from Suc have "… = (f oo (Λ x. 1 + x))⋅i" by simp
  also have "… = f⋅(i + 1)" by (simp add: plus_commute)
  finally show ?case .
qed

lemma wrapS_unwrapS_id: "f⋅⊥ = ⊥ ==> (wrapS oo unwrapS)⋅f = f"
  by (rule cfun_eqI, simp add: wrapS_unwrapS_id' wrapS_def)

subsection‹Fibonacci example.›

definition
  fib_body :: "(Nat → Nat) → Nat → Nat" where
  "fib_body ≡ Λ r. Nat_case⋅1⋅(Nat_case⋅1⋅(Λ n. r⋅n + r⋅(n + 1)))"

(*<*)
lemma fib_body_strict[simp]: "fib_body⋅r⋅⊥ = ⊥" by (simp add: fib_body_def)
(*>*)

definition
  fib :: "Nat → Nat" where
  "fib ≡ fix⋅fib_body"

(*<*)
lemma fib_strict[simp]: "fib⋅⊥ = ⊥"
  by (unfold fib_def, subst fix_eq, fold fib_def, simp add: fib_body_def)
(*>*)

text‹Apply worker/wrapper.›

definition
  fib_work :: "Nat Stream" where
  "fib_work ≡ fix⋅(unwrapS oo fib_body oo wrapS)"

definition
  fib_wrap :: "Nat → Nat" where
  "fib_wrap ≡ wrapS⋅fib_work"

lemma wrapS_unwrapS_fib_body: "wrapS oo unwrapS oo fib_body = fib_body"
proof(rule cfun_eqI)
  fix r show "(wrapS oo unwrapS oo fib_body)⋅r = fib_body⋅r"
    using wrapS_unwrapS_id[where f="fib_body⋅r"] by simp
qed

lemma fib_ww_eq: "fib = fib_wrap"
  using worker_wrapper_body[OF wrapS_unwrapS_fib_body]
  by (simp add: fib_def fib_wrap_def fib_work_def)

text‹Optimise.›

fixrec
  fib_work_final :: "Nat Stream"
and
  fib_f_final :: "Nat → Nat"
where
  "fib_work_final = smap⋅fib_f_final⋅nats"
| "fib_f_final = Nat_case⋅1⋅(Nat_case⋅1⋅(Λ n'. fib_work_final !! n' + fib_work_final !! (n' + 1)))"

declare fib_f_final.simps[simp del] fib_work_final.simps[simp del]

definition
  fib_final :: "Nat → Nat" where
  "fib_final ≡ Λ n. fib_work_final !! n"

text‹

  proof is only fiddly due to the way mutual recursion is encoded:
  need to use Beki\'{c}'s Theorem 🍋‹"Bekic:1969"›\footnote{The
  reader can find some historical commentary in
 🍋‹"Harel:1980" and "DBLP:journals/toplas/Sangiorgi09"›.} to massage the
  into their final form.

 ›

lemma fib_work_final_fib_work_eq: "fib_work_final = fib_work" (is "?lhs = ?rhs")
proof -
  let ?wb = "Λ r. Nat_case⋅1⋅(Nat_case⋅1⋅(Λ n'. r !! n' + r !! (n' + 1)))"
  let ?mr = "Λ (fwf :: Nat Stream, fff). (smap⋅fff⋅nats, ?wb⋅fwf)"
  have "?lhs = fst (fix⋅?mr)"
    by (simp add: fib_work_final_def split_def csplit_def)
  also have "… = (μ fwf. fst (?mr⋅(fwf, μ fff. snd (?mr⋅(fwf, fff)))))"
    using fix_cprod[where F="?mr"] by simp
  also have "… = (μ fwf. smap⋅(μ fff. ?wb⋅fwf)⋅nats)" by simp
  also have "… = (μ fwf. smap⋅(?wb⋅fwf)⋅nats)" by (simp add: fix_const)
  also have "… = ?rhs"
    unfolding fib_body_def fib_work_def unwrapS_unwrapS'_eq unwrapS'_def wrapS_def
    by (simp add: cfcomp1)
  finally show ?thesis .
qed

lemma fib_final_fib_eq: "fib_final = fib" (is "?lhs = ?rhs")
proof -
  have "?lhs = (Λ n. fib_work_final !! n)" by (simp add: fib_final_def)
  also have "… = (Λ n. fib_work !! n)" by (simp only: fib_work_final_fib_work_eq)
  also have "… = fib_wrap" by (simp add: fib_wrap_def wrapS_def)
  also have "… = ?rhs" by (simp only: fib_ww_eq)
  finally show ?thesis .
qed

(*<*)
end
(*>*)