55075
|
1 |
(* Title: HOL/BNF_Examples/Stream_Processor.thy
|
54961
|
2 |
Author: Dmitriy Traytel, TU Muenchen
|
|
3 |
Author: Andrei Popescu, TU Muenchen
|
|
4 |
Copyright 2014
|
|
5 |
|
|
6 |
Stream processors---a syntactic representation of continuous functions on streams
|
|
7 |
*)
|
|
8 |
|
|
9 |
header {* Stream Processors *}
|
|
10 |
|
|
11 |
theory Stream_Processor
|
55070
|
12 |
imports Stream "../BNF_Decl"
|
54961
|
13 |
begin
|
|
14 |
|
|
15 |
section {* Continuous Functions on Streams *}
|
|
16 |
|
|
17 |
datatype_new ('a, 'b, 'c) sp\<^sub>\<mu> = Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>" | Put "'b" "'c"
|
|
18 |
codatatype ('a, 'b) sp\<^sub>\<nu> = In (out: "('a, 'b, ('a, 'b) sp\<^sub>\<nu>) sp\<^sub>\<mu>")
|
|
19 |
|
|
20 |
primrec_new run\<^sub>\<mu> :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> 'a stream \<Rightarrow> ('b \<times> 'c) \<times> 'a stream" where
|
|
21 |
"run\<^sub>\<mu> (Get f) s = run\<^sub>\<mu> (f (shd s)) (stl s)"
|
|
22 |
| "run\<^sub>\<mu> (Put b sp) s = ((b, sp), s)"
|
|
23 |
|
|
24 |
primcorec run\<^sub>\<nu> :: "('a, 'b) sp\<^sub>\<nu> \<Rightarrow> 'a stream \<Rightarrow> 'b stream" where
|
|
25 |
"run\<^sub>\<nu> sp s = (let ((h, sp), s) = run\<^sub>\<mu> (out sp) s in h ## run\<^sub>\<nu> sp s)"
|
|
26 |
|
|
27 |
primcorec copy :: "('a, 'a) sp\<^sub>\<nu>" where
|
|
28 |
"copy = In (Get (\<lambda>a. Put a copy))"
|
|
29 |
|
|
30 |
lemma run\<^sub>\<nu>_copy: "run\<^sub>\<nu> copy s = s"
|
|
31 |
by (coinduction arbitrary: s) simp
|
|
32 |
|
|
33 |
text {*
|
|
34 |
To use the function package for the definition of composition the
|
|
35 |
wellfoundedness of the subtree relation needs to be proved first.
|
|
36 |
*}
|
|
37 |
|
|
38 |
definition "sub \<equiv> {(f a, Get f) | a f. True}"
|
|
39 |
|
|
40 |
lemma subI[intro]: "(f a, Get f) \<in> sub"
|
|
41 |
unfolding sub_def by blast
|
|
42 |
|
|
43 |
lemma wf_sub[simp, intro]: "wf sub"
|
|
44 |
proof (rule wfUNIVI)
|
|
45 |
fix P :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> bool" and x
|
|
46 |
assume "\<forall>x. (\<forall>y. (y, x) \<in> sub \<longrightarrow> P y) \<longrightarrow> P x"
|
|
47 |
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
|
|
48 |
show "P x" by (induct x) (auto intro: I)
|
|
49 |
qed
|
|
50 |
|
|
51 |
function
|
|
52 |
sp\<^sub>\<mu>_comp :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> ('d, 'a, ('d, 'a) sp\<^sub>\<nu>) sp\<^sub>\<mu> \<Rightarrow> ('d, 'b, 'c \<times> ('d, 'a) sp\<^sub>\<nu>) sp\<^sub>\<mu>"
|
|
53 |
(infixl "o\<^sub>\<mu>" 65)
|
|
54 |
where
|
|
55 |
"Put b sp o\<^sub>\<mu> fsp = Put b (sp, In fsp)"
|
|
56 |
| "Get f o\<^sub>\<mu> Put b sp = f b o\<^sub>\<mu> out sp"
|
|
57 |
| "Get f o\<^sub>\<mu> Get g = Get (\<lambda>a. Get f o\<^sub>\<mu> g a)"
|
|
58 |
by pat_completeness auto
|
|
59 |
termination by (relation "lex_prod sub sub") auto
|
|
60 |
|
|
61 |
primcorec sp\<^sub>\<nu>_comp (infixl "o\<^sub>\<nu>" 65) where
|
|
62 |
"out (sp o\<^sub>\<nu> sp') = map_sp\<^sub>\<mu> id (\<lambda>(sp, sp'). sp o\<^sub>\<nu> sp') (out sp o\<^sub>\<mu> out sp')"
|
|
63 |
|
|
64 |
lemma run\<^sub>\<nu>_sp\<^sub>\<nu>_comp: "run\<^sub>\<nu> (sp o\<^sub>\<nu> sp') = run\<^sub>\<nu> sp o run\<^sub>\<nu> sp'"
|
55066
|
65 |
proof (rule ext, unfold comp_apply)
|
54961
|
66 |
fix s
|
|
67 |
show "run\<^sub>\<nu> (sp o\<^sub>\<nu> sp') s = run\<^sub>\<nu> sp (run\<^sub>\<nu> sp' s)"
|
|
68 |
proof (coinduction arbitrary: sp sp' s)
|
|
69 |
case Eq_stream
|
|
70 |
show ?case
|
|
71 |
proof (induct "out sp" "out sp'" arbitrary: sp sp' s rule: sp\<^sub>\<mu>_comp.induct)
|
|
72 |
case (1 b sp'')
|
|
73 |
show ?case by (auto simp add: 1[symmetric])
|
|
74 |
next
|
|
75 |
case (2 f b sp'')
|
|
76 |
from 2(1)[of "In (f b)" sp''] show ?case by (simp add: 2(2,3)[symmetric])
|
|
77 |
next
|
|
78 |
case (3 f h)
|
|
79 |
from 3(1)[of _ "shd s" "In (h (shd s))", OF 3(2)] show ?case by (simp add: 3(2,3)[symmetric])
|
|
80 |
qed
|
|
81 |
qed
|
|
82 |
qed
|
|
83 |
|
|
84 |
text {* Alternative definition of composition using primrec_new instead of function *}
|
|
85 |
|
|
86 |
primrec_new sp\<^sub>\<mu>_comp2R where
|
|
87 |
"sp\<^sub>\<mu>_comp2R f (Put b sp) = f b (out sp)"
|
|
88 |
| "sp\<^sub>\<mu>_comp2R f (Get h) = Get (sp\<^sub>\<mu>_comp2R f o h)"
|
|
89 |
|
|
90 |
primrec_new sp\<^sub>\<mu>_comp2 (infixl "o\<^sup>*\<^sub>\<mu>" 65) where
|
|
91 |
"Put b sp o\<^sup>*\<^sub>\<mu> fsp = Put b (sp, In fsp)"
|
|
92 |
| "Get f o\<^sup>*\<^sub>\<mu> fsp = sp\<^sub>\<mu>_comp2R (op o\<^sup>*\<^sub>\<mu> o f) fsp"
|
|
93 |
|
|
94 |
primcorec sp\<^sub>\<nu>_comp2 (infixl "o\<^sup>*\<^sub>\<nu>" 65) where
|
|
95 |
"out (sp o\<^sup>*\<^sub>\<nu> sp') = map_sp\<^sub>\<mu> id (\<lambda>(sp, sp'). sp o\<^sup>*\<^sub>\<nu> sp') (out sp o\<^sup>*\<^sub>\<mu> out sp')"
|
|
96 |
|
|
97 |
lemma run\<^sub>\<nu>_sp\<^sub>\<nu>_comp2: "run\<^sub>\<nu> (sp o\<^sup>*\<^sub>\<nu> sp') = run\<^sub>\<nu> sp o run\<^sub>\<nu> sp'"
|
55066
|
98 |
proof (rule ext, unfold comp_apply)
|
54961
|
99 |
fix s
|
|
100 |
show "run\<^sub>\<nu> (sp o\<^sup>*\<^sub>\<nu> sp') s = run\<^sub>\<nu> sp (run\<^sub>\<nu> sp' s)"
|
|
101 |
proof (coinduction arbitrary: sp sp' s)
|
|
102 |
case Eq_stream
|
|
103 |
show ?case
|
|
104 |
proof (induct "out sp" arbitrary: sp sp' s)
|
|
105 |
case (Put b sp'')
|
|
106 |
show ?case by (auto simp add: Put[symmetric])
|
|
107 |
next
|
|
108 |
case (Get f)
|
|
109 |
then show ?case
|
|
110 |
proof (induct "out sp'" arbitrary: sp sp' s)
|
|
111 |
case (Put b sp'')
|
|
112 |
from Put(2)[of "In (f b)" sp''] show ?case by (simp add: Put(1,3)[symmetric])
|
|
113 |
next
|
|
114 |
case (Get h)
|
|
115 |
from Get(1)[OF _ Get(3,4), of "In (h (shd s))"] show ?case by (simp add: Get(2,4)[symmetric])
|
|
116 |
qed
|
|
117 |
qed
|
|
118 |
qed
|
|
119 |
qed
|
|
120 |
|
|
121 |
text {* The two definitions are equivalent *}
|
|
122 |
|
|
123 |
lemma sp\<^sub>\<mu>_comp_sp\<^sub>\<mu>_comp2[simp]: "sp o\<^sub>\<mu> sp' = sp o\<^sup>*\<^sub>\<mu> sp'"
|
|
124 |
by (induct sp sp' rule: sp\<^sub>\<mu>_comp.induct) auto
|
|
125 |
|
|
126 |
(*will be provided by the package*)
|
|
127 |
lemma sp\<^sub>\<mu>_rel_map_map[unfolded vimage2p_def, simp]:
|
|
128 |
"rel_sp\<^sub>\<mu> R1 R2 (map_sp\<^sub>\<mu> f1 f2 sp) (map_sp\<^sub>\<mu> g1 g2 sp') =
|
|
129 |
rel_sp\<^sub>\<mu> (BNF_Def.vimage2p f1 g1 R1) (BNF_Def.vimage2p f2 g2 R2) sp sp'"
|
|
130 |
by (tactic {*
|
|
131 |
let val ks = 1 upto 2;
|
|
132 |
in
|
|
133 |
BNF_Tactics.unfold_thms_tac @{context}
|
|
134 |
@{thms sp\<^sub>\<mu>.rel_compp sp\<^sub>\<mu>.rel_conversep sp\<^sub>\<mu>.rel_Grp vimage2p_Grp} THEN
|
|
135 |
HEADGOAL (EVERY' [rtac iffI, rtac @{thm relcomppI}, rtac @{thm GrpI}, rtac refl, rtac CollectI,
|
|
136 |
BNF_Util.CONJ_WRAP' (K (rtac @{thm subset_UNIV})) ks, rtac @{thm relcomppI}, atac,
|
|
137 |
rtac @{thm conversepI}, rtac @{thm GrpI}, rtac refl, rtac CollectI,
|
|
138 |
BNF_Util.CONJ_WRAP' (K (rtac @{thm subset_UNIV})) ks,
|
|
139 |
REPEAT_DETERM o eresolve_tac @{thms relcomppE conversepE GrpE},
|
|
140 |
hyp_subst_tac @{context}, atac])
|
|
141 |
end
|
|
142 |
*})
|
|
143 |
|
|
144 |
lemma sp\<^sub>\<mu>_rel_self: "\<lbrakk>op = \<le> R1; op = \<le> R2\<rbrakk> \<Longrightarrow> rel_sp\<^sub>\<mu> R1 R2 x x"
|
|
145 |
by (erule (1) predicate2D[OF sp\<^sub>\<mu>.rel_mono]) (simp only: sp\<^sub>\<mu>.rel_eq)
|
|
146 |
|
|
147 |
lemma sp\<^sub>\<nu>_comp_sp\<^sub>\<nu>_comp2: "sp o\<^sub>\<nu> sp' = sp o\<^sup>*\<^sub>\<nu> sp'"
|
|
148 |
by (coinduction arbitrary: sp sp') (auto intro!: sp\<^sub>\<mu>_rel_self)
|
|
149 |
|
|
150 |
|
|
151 |
section {* Generalization to an Arbitrary BNF as Codomain *}
|
|
152 |
|
|
153 |
bnf_decl ('a, 'b) F (map: F)
|
|
154 |
|
|
155 |
definition \<theta> :: "('p,'a) F * 'b \<Rightarrow> ('p,'a * 'b) F" where
|
|
156 |
"\<theta> xb = F id <id, \<lambda> a. (snd xb)> (fst xb)"
|
|
157 |
|
|
158 |
(* The strength laws for \<theta>: *)
|
|
159 |
lemma \<theta>_natural: "F id (map_pair f g) o \<theta> = \<theta> o map_pair (F id f) g"
|
55066
|
160 |
unfolding \<theta>_def F.map_comp comp_def id_apply convol_def map_pair_def split_beta fst_conv snd_conv ..
|
54961
|
161 |
|
|
162 |
definition assl :: "'a * ('b * 'c) \<Rightarrow> ('a * 'b) * 'c" where
|
|
163 |
"assl abc = ((fst abc, fst (snd abc)), snd (snd abc))"
|
|
164 |
|
|
165 |
lemma \<theta>_rid: "F id fst o \<theta> = fst"
|
55066
|
166 |
unfolding \<theta>_def F.map_comp F.map_id comp_def id_apply convol_def fst_conv sym[OF id_def] ..
|
54961
|
167 |
|
|
168 |
lemma \<theta>_assl: "F id assl o \<theta> = \<theta> o map_pair \<theta> id o assl"
|
55066
|
169 |
unfolding assl_def \<theta>_def F.map_comp comp_def id_apply convol_def map_pair_def split fst_conv snd_conv ..
|
54961
|
170 |
|
|
171 |
datatype_new ('a, 'b, 'c) spF\<^sub>\<mu> = GetF "'a \<Rightarrow> ('a, 'b, 'c) spF\<^sub>\<mu>" | PutF "('b,'c) F"
|
|
172 |
codatatype ('a, 'b) spF\<^sub>\<nu> = InF (outF: "('a, 'b, ('a, 'b) spF\<^sub>\<nu>) spF\<^sub>\<mu>")
|
|
173 |
|
|
174 |
codatatype 'b JF = Ctor (dtor: "('b, 'b JF) F")
|
|
175 |
|
|
176 |
(* Definition of run for an arbitrary final coalgebra as codomain: *)
|
|
177 |
|
|
178 |
primrec_new
|
|
179 |
runF\<^sub>\<mu> :: "('a, 'b, ('a, 'b) spF\<^sub>\<nu>) spF\<^sub>\<mu> \<Rightarrow> 'a stream \<Rightarrow> (('b, ('a, 'b) spF\<^sub>\<nu>) F) \<times> 'a stream"
|
|
180 |
where
|
|
181 |
"runF\<^sub>\<mu> (GetF f) s = (runF\<^sub>\<mu> o f) (shd s) (stl s)"
|
|
182 |
| "runF\<^sub>\<mu> (PutF x) s = (x, s)"
|
|
183 |
|
|
184 |
primcorec runF\<^sub>\<nu> :: "('a, 'b) spF\<^sub>\<nu> \<Rightarrow> 'a stream \<Rightarrow> 'b JF" where
|
|
185 |
"runF\<^sub>\<nu> sp s = (let (x, s) = runF\<^sub>\<mu> (outF sp) s in Ctor (F id (\<lambda> sp. runF\<^sub>\<nu> sp s) x))"
|
|
186 |
|
|
187 |
end
|