author | wenzelm |
Fri, 18 Aug 2017 20:47:47 +0200 | |
changeset 66453 | cc19f7ca2ed6 |
parent 63167 | 0909deb8059b |
child 67399 | eab6ce8368fa |
permissions | -rw-r--r-- |
58309
a09ec6daaa19
renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
blanchet
parents:
57641
diff
changeset
|
1 |
(* Title: HOL/Datatype_Examples/Stream_Processor.thy |
54961 | 2 |
Author: Dmitriy Traytel, TU Muenchen |
3 |
Author: Andrei Popescu, TU Muenchen |
|
4 |
Copyright 2014 |
|
5 |
||
57634 | 6 |
Stream processors---a syntactic representation of continuous functions on streams. |
54961 | 7 |
*) |
8 |
||
63167 | 9 |
section \<open>Stream Processors---A Syntactic Representation of Continuous Functions on Streams\<close> |
54961 | 10 |
|
11 |
theory Stream_Processor |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63167
diff
changeset
|
12 |
imports "HOL-Library.Stream" "HOL-Library.BNF_Axiomatization" |
54961 | 13 |
begin |
14 |
||
61260 | 15 |
declare [[typedef_overloaded]] |
16 |
||
17 |
||
63167 | 18 |
section \<open>Continuous Functions on Streams\<close> |
54961 | 19 |
|
62694 | 20 |
datatype ('a, 'b, 'c) sp\<^sub>\<mu> = |
21 |
Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>" |
|
22 |
| Put "'b" "'c" |
|
23 |
||
24 |
codatatype ('a, 'b) sp\<^sub>\<nu> = |
|
25 |
In (out: "('a, 'b, ('a, 'b) sp\<^sub>\<nu>) sp\<^sub>\<mu>") |
|
54961 | 26 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55091
diff
changeset
|
27 |
primrec run\<^sub>\<mu> :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> 'a stream \<Rightarrow> ('b \<times> 'c) \<times> 'a stream" where |
54961 | 28 |
"run\<^sub>\<mu> (Get f) s = run\<^sub>\<mu> (f (shd s)) (stl s)" |
29 |
| "run\<^sub>\<mu> (Put b sp) s = ((b, sp), s)" |
|
30 |
||
31 |
primcorec run\<^sub>\<nu> :: "('a, 'b) sp\<^sub>\<nu> \<Rightarrow> 'a stream \<Rightarrow> 'b stream" where |
|
32 |
"run\<^sub>\<nu> sp s = (let ((h, sp), s) = run\<^sub>\<mu> (out sp) s in h ## run\<^sub>\<nu> sp s)" |
|
33 |
||
34 |
primcorec copy :: "('a, 'a) sp\<^sub>\<nu>" where |
|
35 |
"copy = In (Get (\<lambda>a. Put a copy))" |
|
36 |
||
37 |
lemma run\<^sub>\<nu>_copy: "run\<^sub>\<nu> copy s = s" |
|
38 |
by (coinduction arbitrary: s) simp |
|
39 |
||
63167 | 40 |
text \<open> |
54961 | 41 |
To use the function package for the definition of composition the |
42 |
wellfoundedness of the subtree relation needs to be proved first. |
|
63167 | 43 |
\<close> |
54961 | 44 |
|
45 |
definition "sub \<equiv> {(f a, Get f) | a f. True}" |
|
46 |
||
47 |
lemma subI[intro]: "(f a, Get f) \<in> sub" |
|
48 |
unfolding sub_def by blast |
|
49 |
||
50 |
lemma wf_sub[simp, intro]: "wf sub" |
|
51 |
proof (rule wfUNIVI) |
|
52 |
fix P :: "('a, 'b, 'c) sp\<^sub>\<mu> \<Rightarrow> bool" and x |
|
53 |
assume "\<forall>x. (\<forall>y. (y, x) \<in> sub \<longrightarrow> P y) \<longrightarrow> P x" |
|
54 |
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 |
|
55 |
show "P x" by (induct x) (auto intro: I) |
|
56 |
qed |
|
57 |
||
58 |
function |
|
59 |
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>" |
|
60 |
(infixl "o\<^sub>\<mu>" 65) |
|
61 |
where |
|
62 |
"Put b sp o\<^sub>\<mu> fsp = Put b (sp, In fsp)" |
|
63 |
| "Get f o\<^sub>\<mu> Put b sp = f b o\<^sub>\<mu> out sp" |
|
64 |
| "Get f o\<^sub>\<mu> Get g = Get (\<lambda>a. Get f o\<^sub>\<mu> g a)" |
|
65 |
by pat_completeness auto |
|
66 |
termination by (relation "lex_prod sub sub") auto |
|
67 |
||
68 |
primcorec sp\<^sub>\<nu>_comp (infixl "o\<^sub>\<nu>" 65) where |
|
69 |
"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')" |
|
70 |
||
71 |
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 | 72 |
proof (rule ext, unfold comp_apply) |
54961 | 73 |
fix s |
74 |
show "run\<^sub>\<nu> (sp o\<^sub>\<nu> sp') s = run\<^sub>\<nu> sp (run\<^sub>\<nu> sp' s)" |
|
75 |
proof (coinduction arbitrary: sp sp' s) |
|
76 |
case Eq_stream |
|
77 |
show ?case |
|
78 |
proof (induct "out sp" "out sp'" arbitrary: sp sp' s rule: sp\<^sub>\<mu>_comp.induct) |
|
79 |
case (1 b sp'') |
|
80 |
show ?case by (auto simp add: 1[symmetric]) |
|
81 |
next |
|
82 |
case (2 f b sp'') |
|
83 |
from 2(1)[of "In (f b)" sp''] show ?case by (simp add: 2(2,3)[symmetric]) |
|
84 |
next |
|
85 |
case (3 f h) |
|
86 |
from 3(1)[of _ "shd s" "In (h (shd s))", OF 3(2)] show ?case by (simp add: 3(2,3)[symmetric]) |
|
87 |
qed |
|
88 |
qed |
|
89 |
qed |
|
90 |
||
63167 | 91 |
text \<open>Alternative definition of composition using primrec instead of function\<close> |
54961 | 92 |
|
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55091
diff
changeset
|
93 |
primrec sp\<^sub>\<mu>_comp2R where |
54961 | 94 |
"sp\<^sub>\<mu>_comp2R f (Put b sp) = f b (out sp)" |
95 |
| "sp\<^sub>\<mu>_comp2R f (Get h) = Get (sp\<^sub>\<mu>_comp2R f o h)" |
|
96 |
||
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55091
diff
changeset
|
97 |
primrec sp\<^sub>\<mu>_comp2 (infixl "o\<^sup>*\<^sub>\<mu>" 65) where |
54961 | 98 |
"Put b sp o\<^sup>*\<^sub>\<mu> fsp = Put b (sp, In fsp)" |
99 |
| "Get f o\<^sup>*\<^sub>\<mu> fsp = sp\<^sub>\<mu>_comp2R (op o\<^sup>*\<^sub>\<mu> o f) fsp" |
|
100 |
||
101 |
primcorec sp\<^sub>\<nu>_comp2 (infixl "o\<^sup>*\<^sub>\<nu>" 65) where |
|
102 |
"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')" |
|
103 |
||
104 |
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 | 105 |
proof (rule ext, unfold comp_apply) |
54961 | 106 |
fix s |
107 |
show "run\<^sub>\<nu> (sp o\<^sup>*\<^sub>\<nu> sp') s = run\<^sub>\<nu> sp (run\<^sub>\<nu> sp' s)" |
|
108 |
proof (coinduction arbitrary: sp sp' s) |
|
109 |
case Eq_stream |
|
110 |
show ?case |
|
111 |
proof (induct "out sp" arbitrary: sp sp' s) |
|
112 |
case (Put b sp'') |
|
113 |
show ?case by (auto simp add: Put[symmetric]) |
|
114 |
next |
|
115 |
case (Get f) |
|
116 |
then show ?case |
|
117 |
proof (induct "out sp'" arbitrary: sp sp' s) |
|
118 |
case (Put b sp'') |
|
119 |
from Put(2)[of "In (f b)" sp''] show ?case by (simp add: Put(1,3)[symmetric]) |
|
120 |
next |
|
121 |
case (Get h) |
|
122 |
from Get(1)[OF _ Get(3,4), of "In (h (shd s))"] show ?case by (simp add: Get(2,4)[symmetric]) |
|
123 |
qed |
|
124 |
qed |
|
125 |
qed |
|
126 |
qed |
|
127 |
||
63167 | 128 |
text \<open>The two definitions are equivalent\<close> |
54961 | 129 |
|
130 |
lemma sp\<^sub>\<mu>_comp_sp\<^sub>\<mu>_comp2[simp]: "sp o\<^sub>\<mu> sp' = sp o\<^sup>*\<^sub>\<mu> sp'" |
|
131 |
by (induct sp sp' rule: sp\<^sub>\<mu>_comp.induct) auto |
|
132 |
||
133 |
(*will be provided by the package*) |
|
134 |
lemma sp\<^sub>\<mu>_rel_map_map[unfolded vimage2p_def, simp]: |
|
135 |
"rel_sp\<^sub>\<mu> R1 R2 (map_sp\<^sub>\<mu> f1 f2 sp) (map_sp\<^sub>\<mu> g1 g2 sp') = |
|
57398 | 136 |
rel_sp\<^sub>\<mu> (BNF_Def.vimage2p f1 g1 R1) (BNF_Def.vimage2p f2 g2 R2) sp sp'" |
63167 | 137 |
by (tactic \<open> |
60754 | 138 |
let |
139 |
val ks = 1 upto 2; |
|
140 |
val ctxt = @{context}; |
|
54961 | 141 |
in |
60754 | 142 |
BNF_Tactics.unfold_thms_tac ctxt |
54961 | 143 |
@{thms sp\<^sub>\<mu>.rel_compp sp\<^sub>\<mu>.rel_conversep sp\<^sub>\<mu>.rel_Grp vimage2p_Grp} THEN |
60754 | 144 |
HEADGOAL (EVERY' [resolve_tac ctxt [iffI], |
145 |
resolve_tac ctxt @{thms relcomppI}, |
|
146 |
resolve_tac ctxt @{thms GrpI}, |
|
147 |
resolve_tac ctxt [refl], |
|
148 |
resolve_tac ctxt [CollectI], |
|
149 |
BNF_Util.CONJ_WRAP' (K (resolve_tac ctxt @{thms subset_UNIV})) ks, |
|
150 |
resolve_tac ctxt @{thms relcomppI}, assume_tac ctxt, |
|
151 |
resolve_tac ctxt @{thms conversepI}, |
|
152 |
resolve_tac ctxt @{thms GrpI}, |
|
153 |
resolve_tac ctxt [refl], |
|
154 |
resolve_tac ctxt [CollectI], |
|
155 |
BNF_Util.CONJ_WRAP' (K (resolve_tac ctxt @{thms subset_UNIV})) ks, |
|
156 |
REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE conversepE GrpE}, |
|
157 |
hyp_subst_tac ctxt, |
|
158 |
assume_tac ctxt]) |
|
54961 | 159 |
end |
63167 | 160 |
\<close>) |
54961 | 161 |
|
162 |
lemma sp\<^sub>\<mu>_rel_self: "\<lbrakk>op = \<le> R1; op = \<le> R2\<rbrakk> \<Longrightarrow> rel_sp\<^sub>\<mu> R1 R2 x x" |
|
163 |
by (erule (1) predicate2D[OF sp\<^sub>\<mu>.rel_mono]) (simp only: sp\<^sub>\<mu>.rel_eq) |
|
164 |
||
165 |
lemma sp\<^sub>\<nu>_comp_sp\<^sub>\<nu>_comp2: "sp o\<^sub>\<nu> sp' = sp o\<^sup>*\<^sub>\<nu> sp'" |
|
166 |
by (coinduction arbitrary: sp sp') (auto intro!: sp\<^sub>\<mu>_rel_self) |
|
167 |
||
168 |
||
63167 | 169 |
section \<open>Generalization to an Arbitrary BNF as Codomain\<close> |
54961 | 170 |
|
57206
d9be905d6283
changed syntax of map: and rel: arguments to BNF-based datatypes
blanchet
parents:
56942
diff
changeset
|
171 |
bnf_axiomatization ('a, 'b) F for map: F |
54961 | 172 |
|
57641
dc59f147b27d
more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
wenzelm
parents:
57634
diff
changeset
|
173 |
notation BNF_Def.convol ("\<langle>(_,/ _)\<rangle>") |
55091 | 174 |
|
54961 | 175 |
definition \<theta> :: "('p,'a) F * 'b \<Rightarrow> ('p,'a * 'b) F" where |
57641
dc59f147b27d
more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
wenzelm
parents:
57634
diff
changeset
|
176 |
"\<theta> xb = F id \<langle>id, \<lambda> a. (snd xb)\<rangle> (fst xb)" |
54961 | 177 |
|
178 |
(* The strength laws for \<theta>: *) |
|
55932 | 179 |
lemma \<theta>_natural: "F id (map_prod f g) o \<theta> = \<theta> o map_prod (F id f) g" |
180 |
unfolding \<theta>_def F.map_comp comp_def id_apply convol_def map_prod_def split_beta fst_conv snd_conv .. |
|
54961 | 181 |
|
182 |
definition assl :: "'a * ('b * 'c) \<Rightarrow> ('a * 'b) * 'c" where |
|
183 |
"assl abc = ((fst abc, fst (snd abc)), snd (snd abc))" |
|
184 |
||
185 |
lemma \<theta>_rid: "F id fst o \<theta> = fst" |
|
55066 | 186 |
unfolding \<theta>_def F.map_comp F.map_id comp_def id_apply convol_def fst_conv sym[OF id_def] .. |
54961 | 187 |
|
55932 | 188 |
lemma \<theta>_assl: "F id assl o \<theta> = \<theta> o map_prod \<theta> id o assl" |
189 |
unfolding assl_def \<theta>_def F.map_comp comp_def id_apply convol_def map_prod_def split fst_conv snd_conv .. |
|
54961 | 190 |
|
58310 | 191 |
datatype ('a, 'b, 'c) spF\<^sub>\<mu> = GetF "'a \<Rightarrow> ('a, 'b, 'c) spF\<^sub>\<mu>" | PutF "('b,'c) F" |
54961 | 192 |
codatatype ('a, 'b) spF\<^sub>\<nu> = InF (outF: "('a, 'b, ('a, 'b) spF\<^sub>\<nu>) spF\<^sub>\<mu>") |
193 |
||
194 |
codatatype 'b JF = Ctor (dtor: "('b, 'b JF) F") |
|
195 |
||
196 |
(* Definition of run for an arbitrary final coalgebra as codomain: *) |
|
197 |
||
55530
3dfb724db099
renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents:
55091
diff
changeset
|
198 |
primrec |
54961 | 199 |
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" |
200 |
where |
|
201 |
"runF\<^sub>\<mu> (GetF f) s = (runF\<^sub>\<mu> o f) (shd s) (stl s)" |
|
202 |
| "runF\<^sub>\<mu> (PutF x) s = (x, s)" |
|
203 |
||
204 |
primcorec runF\<^sub>\<nu> :: "('a, 'b) spF\<^sub>\<nu> \<Rightarrow> 'a stream \<Rightarrow> 'b JF" where |
|
205 |
"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))" |
|
206 |
||
207 |
end |