Theory Streams
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
try to fold some definitions here but it's easier if the stream
constructor 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
strict. \<^citet>‹‹\S6.1› in "GillHutton:2009"› do not make this requirement,
an oversight on their part.
In practice all functions worth memoising are strict in the memoised
argument.›
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‹
This proof is only fiddly due to the way mutual recursion is encoded:
we need to use Beki\'{c}'s Theorem \<^citep>‹"Bekic:1969"›\footnote{The
interested reader can find some historical commentary in
\<^citet>‹"Harel:1980" and "DBLP:journals/toplas/Sangiorgi09"›.} to massage the
definitions 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