# Theory Stream_Processor

theory Stream_Processor
imports BNF_Corec Stream
```(*  Title:      HOL/Corec_Examples/Stream_Processor.thy
Author:     Andreas Lochbihler, ETH Zuerich
Author:     Dmitriy Traytel, ETH Zuerich
Author:     Andrei Popescu, TU Muenchen

Stream processors---a syntactic representation of continuous functions on streams.
*)

section ‹Stream Processors---A Syntactic Representation of Continuous Functions on Streams›

theory Stream_Processor
imports "HOL-Library.BNF_Corec" "HOL-Library.Stream"
begin

datatype (discs_sels) ('a, 'b, 'c) sp⇩μ =
Get "'a ⇒ ('a, 'b, 'c) sp⇩μ"
| Put "'b" "'c"

codatatype ('a, 'b) sp⇩ν =
In (out: "('a, 'b, ('a, 'b) sp⇩ν) sp⇩μ")

definition "sub ≡ {(f a, Get f) | a f. True}"

lemma subI[intro]: "(f a, Get f) ∈ sub"
unfolding sub_def by blast

lemma wf_sub[simp, intro]: "wf sub"
proof (rule wfUNIVI)
fix P  :: "('a, 'b, 'c) sp⇩μ ⇒ bool" and x
assume "∀x. (∀y. (y, x) ∈ sub ⟶ P y) ⟶ P x"
hence I: "⋀x. (∀y. (∃a f. y = f a ∧ x = Get f) ⟶ P y) ⟹ P x" unfolding sub_def by blast
show "P x" by (induct x) (auto intro: I)
qed

definition get where
"get f = In (Get (λa. out (f a)))"

corecursive run :: "('a, 'b) sp⇩ν ⇒ 'a stream ⇒ 'b stream" where
"run sp s = (case out sp of
Get f ⇒ run (In (f (shd s))) (stl s)
| Put b sp ⇒ b ## run sp s)"
by (relation "map_prod In In ` sub <*lex*> {}")
(auto simp: inj_on_def out_def split: sp⇩ν.splits intro: wf_map_prod_image)

corec copy where
"copy = In (Get (λa. Put a copy))"

friend_of_corec get where
"get f = In (Get (λa. out (f a)))"
by (auto simp: rel_fun_def get_def sp⇩μ.rel_map rel_prod.simps, metis sndI)

lemma run_simps [simp]:
"run (In (Get f)) s = run (In (f (shd s))) (stl s)"
"run (In (Put b sp)) s = b ## run sp s"
by(subst run.code; simp; fail)+

lemma copy_sel[simp]: "out copy = Get (λa. Put a copy)"
by (subst copy.code; simp)

corecursive sp_comp (infixl "oo" 65) where
"sp oo sp' = (case (out sp, out sp') of
(Put b sp, _) ⇒ In (Put b (sp oo sp'))
| (Get f, Put b sp) ⇒ In (f b) oo sp
| (_, Get g) ⇒ get (λa. (sp oo In (g a))))"
by (relation "map_prod In In ` sub <*lex*> map_prod In In ` sub")
(auto simp: inj_on_def out_def split: sp⇩ν.splits intro: wf_map_prod_image)

lemma run_copy_unique:
"(⋀s. h s = shd s ## h (stl s)) ⟹ h = run copy"
apply corec_unique
apply(rule ext)
apply(subst copy.code)
apply simp
done

end
```