(* 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
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
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.
