|
1 (* Title: HOL/BNF/Examples/Stream_Processor.thy |
|
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 |
|
12 imports Stream |
|
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'" |
|
65 proof (rule ext, unfold o_apply) |
|
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'" |
|
98 proof (rule ext, unfold o_apply) |
|
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" |
|
160 unfolding \<theta>_def F.map_comp o_def id_apply convol_def map_pair_def split_beta fst_conv snd_conv .. |
|
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" |
|
166 unfolding \<theta>_def F.map_comp F.map_id o_def id_apply convol_def fst_conv sym[OF id_def] .. |
|
167 |
|
168 lemma \<theta>_assl: "F id assl o \<theta> = \<theta> o map_pair \<theta> id o assl" |
|
169 unfolding assl_def \<theta>_def F.map_comp o_def id_apply convol_def map_pair_def split fst_conv snd_conv .. |
|
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 |