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