(* Title: HOL/Corec_Examples/Stream_Processor.thy Author: Andreas Lochbihler, ETH Zuerich Author: Dmitriy Traytel, ETH Zuerich Author: Andrei Popescu, TU Muenchen Copyright 2014, 2016
Stream processors---a syntactic representation of continuous functions on streams.
*)
section \<open>Stream Processors---A Syntactic Representation of Continuous Functions on Streams\<close>
theory Stream_Processor imports"HOL-Library.BNF_Corec""HOL-Library.Stream" begin
datatype (discs_sels) ('a, 'b, 'c) sp\<^sub>\ =
Get "'a \ ('a, 'b, 'c) sp\<^sub>\"
| Put "'b""'c"
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\<^sub>\ \ 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
lemma Get_neq: "Get f \ f a" by (metis subI wf_not_sym wf_sub)
definition get where "get f = In (Get (\a. out (f a)))"
corecursive run :: "('a, 'b) sp\<^sub>\ \ 'a stream \ 'b stream" where "run sp s = (case out sp of
Get f \<Rightarrow> run (In (f (shd s))) (stl s)
| Put b sp \<Rightarrow> b ## run sp s)" by (relation "inv_image (map_prod In In ` sub) fst")
(auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.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\<^sub>\<mu>.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\<open>oo\<close> 65) where "sp oo sp' = (case (out sp, out sp') of
(Put b sp, _) \<Rightarrow> In (Put b (sp oo sp'))
| (Get f, Put b sp) \<Rightarrow> In (f b) oo sp
| (_, Get g) \<Rightarrow> get (\<lambda>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\<^sub>\<nu>.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
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
