1(* Title: HOL/Corec_Examples/Stream_Processor.thy 2 Author: Andreas Lochbihler, ETH Zuerich 3 Author: Dmitriy Traytel, ETH Zuerich 4 Author: Andrei Popescu, TU Muenchen 5 Copyright 2014, 2016 6 7Stream processors---a syntactic representation of continuous functions on streams. 8*) 9 10section \<open>Stream Processors---A Syntactic Representation of Continuous Functions on Streams\<close> 11 12theory Stream_Processor 13imports "HOL-Library.BNF_Corec" "HOL-Library.Stream" 14begin 15 16datatype (discs_sels) ('a, 'b, 'c) sp\<^sub>\<mu> = 17 Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>" 18| Put "'b" "'c" 19 20codatatype ('a, 'b) sp\<^sub>\<nu> = 21 In (out: "('a, 'b, ('a, 'b) sp\<^sub>\<nu>) sp\<^sub>\<mu>") 22 23definition "sub \<equiv> {(f a, Get f) | a f. True}" 24 25lemma subI[intro]: "(f a, Get f) \<in> sub" 26 unfolding sub_def by blast 27 28lemma wf_sub[simp, intro]: "wf sub" 29proof (rule wfUNIVI) 30 fix P :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> bool" and x 31 assume "\<forall>x. (\<forall>y. (y, x) \<in> sub \<longrightarrow> P y) \<longrightarrow> P x" 32 hence I: "\<And>x. (\<forall>y. (\<exists>a f. y = f a \<and> x = Get f) \<longrightarrow> P y) \<Longrightarrow> P x" unfolding sub_def by blast 33 show "P x" by (induct x) (auto intro: I) 34qed 35 36definition get where 37 "get f = In (Get (\<lambda>a. out (f a)))" 38 39corecursive run :: "('a, 'b) sp\<^sub>\<nu> \<Rightarrow> 'a stream \<Rightarrow> 'b stream" where 40 "run sp s = (case out sp of 41 Get f \<Rightarrow> run (In (f (shd s))) (stl s) 42 | Put b sp \<Rightarrow> b ## run sp s)" 43 by (relation "map_prod In In ` sub <*lex*> {}") 44 (auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.splits intro: wf_map_prod_image) 45 46corec copy where 47 "copy = In (Get (\<lambda>a. Put a copy))" 48 49friend_of_corec get where 50 "get f = In (Get (\<lambda>a. out (f a)))" 51 by (auto simp: rel_fun_def get_def sp\<^sub>\<mu>.rel_map rel_prod.simps, metis sndI) 52 53lemma run_simps [simp]: 54 "run (In (Get f)) s = run (In (f (shd s))) (stl s)" 55 "run (In (Put b sp)) s = b ## run sp s" 56by(subst run.code; simp; fail)+ 57 58lemma copy_sel[simp]: "out copy = Get (\<lambda>a. Put a copy)" 59 by (subst copy.code; simp) 60 61corecursive sp_comp (infixl "oo" 65) where 62 "sp oo sp' = (case (out sp, out sp') of 63 (Put b sp, _) \<Rightarrow> In (Put b (sp oo sp')) 64 | (Get f, Put b sp) \<Rightarrow> In (f b) oo sp 65 | (_, Get g) \<Rightarrow> get (\<lambda>a. (sp oo In (g a))))" 66 by (relation "map_prod In In ` sub <*lex*> map_prod In In ` sub") 67 (auto simp: inj_on_def out_def split: sp\<^sub>\<nu>.splits intro: wf_map_prod_image) 68 69lemma run_copy_unique: 70 "(\<And>s. h s = shd s ## h (stl s)) \<Longrightarrow> h = run copy" 71apply corec_unique 72apply(rule ext) 73apply(subst copy.code) 74apply simp 75done 76 77end 78