62694
|
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 |
|
|
7 |
Stream processors---a syntactic representation of continuous functions on streams.
|
|
8 |
*)
|
|
9 |
|
62726
|
10 |
section \<open>Stream Processors---A Syntactic Representation of Continuous Functions on Streams\<close>
|
62694
|
11 |
|
|
12 |
theory Stream_Processor
|
|
13 |
imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/Stream"
|
|
14 |
begin
|
|
15 |
|
|
16 |
datatype (discs_sels) ('a, 'b, 'c) sp\<^sub>\<mu> =
|
|
17 |
Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>"
|
|
18 |
| Put "'b" "'c"
|
|
19 |
|
|
20 |
codatatype ('a, 'b) sp\<^sub>\<nu> =
|
|
21 |
In (out: "('a, 'b, ('a, 'b) sp\<^sub>\<nu>) sp\<^sub>\<mu>")
|
|
22 |
|
|
23 |
definition "sub \<equiv> {(f a, Get f) | a f. True}"
|
|
24 |
|
|
25 |
lemma subI[intro]: "(f a, Get f) \<in> sub"
|
|
26 |
unfolding sub_def by blast
|
|
27 |
|
|
28 |
lemma wf_sub[simp, intro]: "wf sub"
|
|
29 |
proof (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)
|
|
34 |
qed
|
|
35 |
|
|
36 |
definition get where
|
|
37 |
"get f = In (Get (\<lambda>a. out (f a)))"
|
|
38 |
|
|
39 |
corecursive 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 |
|
|
46 |
corec copy where
|
|
47 |
"copy = In (Get (\<lambda>a. Put a copy))"
|
|
48 |
|
|
49 |
friend_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 |
|
|
53 |
lemma 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"
|
|
56 |
by(subst run.code; simp; fail)+
|
|
57 |
|
|
58 |
lemma copy_sel[simp]: "out copy = Get (\<lambda>a. Put a copy)"
|
|
59 |
by (subst copy.code; simp)
|
|
60 |
|
|
61 |
corecursive 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 |
|
62698
|
69 |
lemma run_copy_unique:
|
62694
|
70 |
"(\<And>s. h s = shd s ## h (stl s)) \<Longrightarrow> h = run copy"
|
|
71 |
apply corec_unique
|
|
72 |
apply(rule ext)
|
|
73 |
apply(subst copy.code)
|
|
74 |
apply simp
|
|
75 |
done
|
|
76 |
|
|
77 |
end
|