|
1 |
|
2 theory Sulzmann |
|
3 imports "Lexer" |
|
4 begin |
|
5 |
|
6 section {* Bit-Encodings *} |
|
7 |
|
8 datatype bit = Z | S |
|
9 |
|
10 fun |
|
11 code :: "val \<Rightarrow> bit list" |
|
12 where |
|
13 "code Void = []" |
|
14 | "code (Char c) = []" |
|
15 | "code (Left v) = Z # (code v)" |
|
16 | "code (Right v) = S # (code v)" |
|
17 | "code (Seq v1 v2) = (code v1) @ (code v2)" |
|
18 | "code (Stars []) = [S]" |
|
19 | "code (Stars (v # vs)) = (Z # code v) @ code (Stars vs)" |
|
20 |
|
21 |
|
22 fun |
|
23 Stars_add :: "val \<Rightarrow> val \<Rightarrow> val" |
|
24 where |
|
25 "Stars_add v (Stars vs) = Stars (v # vs)" |
|
26 |
|
27 function |
|
28 decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)" |
|
29 where |
|
30 "decode' ds ZERO = (Void, [])" |
|
31 | "decode' ds ONE = (Void, ds)" |
|
32 | "decode' ds (CH d) = (Char d, ds)" |
|
33 | "decode' [] (ALT r1 r2) = (Void, [])" |
|
34 | "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))" |
|
35 | "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))" |
|
36 | "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in |
|
37 let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))" |
|
38 | "decode' [] (STAR r) = (Void, [])" |
|
39 | "decode' (S # ds) (STAR r) = (Stars [], ds)" |
|
40 | "decode' (Z # ds) (STAR r) = (let (v, ds') = decode' ds r in |
|
41 let (vs, ds'') = decode' ds' (STAR r) |
|
42 in (Stars_add v vs, ds''))" |
|
43 by pat_completeness auto |
|
44 |
|
45 lemma decode'_smaller: |
|
46 assumes "decode'_dom (ds, r)" |
|
47 shows "length (snd (decode' ds r)) \<le> length ds" |
|
48 using assms |
|
49 apply(induct ds r) |
|
50 apply(auto simp add: decode'.psimps split: prod.split) |
|
51 using dual_order.trans apply blast |
|
52 by (meson dual_order.trans le_SucI) |
|
53 |
|
54 termination "decode'" |
|
55 apply(relation "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))") |
|
56 apply(auto dest!: decode'_smaller) |
|
57 by (metis less_Suc_eq_le snd_conv) |
|
58 |
|
59 definition |
|
60 decode :: "bit list \<Rightarrow> rexp \<Rightarrow> val option" |
|
61 where |
|
62 "decode ds r \<equiv> (let (v, ds') = decode' ds r |
|
63 in (if ds' = [] then Some v else None))" |
|
64 |
|
65 lemma decode'_code_Stars: |
|
66 assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> (\<forall>x. decode' (code v @ x) r = (v, x)) \<and> flat v \<noteq> []" |
|
67 shows "decode' (code (Stars vs) @ ds) (STAR r) = (Stars vs, ds)" |
|
68 using assms |
|
69 apply(induct vs) |
|
70 apply(auto) |
|
71 done |
|
72 |
|
73 lemma decode'_code: |
|
74 assumes "\<Turnstile> v : r" |
|
75 shows "decode' ((code v) @ ds) r = (v, ds)" |
|
76 using assms |
|
77 apply(induct v r arbitrary: ds) |
|
78 apply(auto) |
|
79 using decode'_code_Stars by blast |
|
80 |
|
81 lemma decode_code: |
|
82 assumes "\<Turnstile> v : r" |
|
83 shows "decode (code v) r = Some v" |
|
84 using assms unfolding decode_def |
|
85 by (smt append_Nil2 decode'_code old.prod.case) |
|
86 |
|
87 |
|
88 datatype arexp = |
|
89 AZERO |
|
90 | AONE "bit list" |
|
91 | ACH "bit list" char |
|
92 | ASEQ "bit list" arexp arexp |
|
93 | AALT "bit list" arexp arexp |
|
94 | ASTAR "bit list" arexp |
|
95 |
|
96 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where |
|
97 "fuse bs AZERO = AZERO" |
|
98 | "fuse bs (AONE cs) = AONE (bs @ cs)" |
|
99 | "fuse bs (ACH cs c) = ACH (bs @ cs) c" |
|
100 | "fuse bs (AALT cs r1 r2) = AALT (bs @ cs) r1 r2" |
|
101 | "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2" |
|
102 | "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r" |
|
103 |
|
104 fun intern :: "rexp \<Rightarrow> arexp" where |
|
105 "intern ZERO = AZERO" |
|
106 | "intern ONE = AONE []" |
|
107 | "intern (CH c) = ACH [] c" |
|
108 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) |
|
109 (fuse [S] (intern r2))" |
|
110 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)" |
|
111 | "intern (STAR r) = ASTAR [] (intern r)" |
|
112 |
|
113 |
|
114 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where |
|
115 "retrieve (AONE bs) Void = bs" |
|
116 | "retrieve (ACH bs c) (Char d) = bs" |
|
117 | "retrieve (AALT bs r1 r2) (Left v) = bs @ retrieve r1 v" |
|
118 | "retrieve (AALT bs r1 r2) (Right v) = bs @ retrieve r2 v" |
|
119 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2" |
|
120 | "retrieve (ASTAR bs r) (Stars []) = bs @ [S]" |
|
121 | "retrieve (ASTAR bs r) (Stars (v#vs)) = |
|
122 bs @ [Z] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)" |
|
123 |
|
124 fun |
|
125 erase :: "arexp \<Rightarrow> rexp" |
|
126 where |
|
127 "erase AZERO = ZERO" |
|
128 | "erase (AONE _) = ONE" |
|
129 | "erase (ACH _ c) = CH c" |
|
130 | "erase (AALT _ r1 r2) = ALT (erase r1) (erase r2)" |
|
131 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)" |
|
132 | "erase (ASTAR _ r) = STAR (erase r)" |
|
133 |
|
134 fun |
|
135 bnullable :: "arexp \<Rightarrow> bool" |
|
136 where |
|
137 "bnullable (AZERO) = False" |
|
138 | "bnullable (AONE bs) = True" |
|
139 | "bnullable (ACH bs c) = False" |
|
140 | "bnullable (AALT bs r1 r2) = (bnullable r1 \<or> bnullable r2)" |
|
141 | "bnullable (ASEQ bs r1 r2) = (bnullable r1 \<and> bnullable r2)" |
|
142 | "bnullable (ASTAR bs r) = True" |
|
143 |
|
144 fun |
|
145 bmkeps :: "arexp \<Rightarrow> bit list" |
|
146 where |
|
147 "bmkeps(AONE bs) = bs" |
|
148 | "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)" |
|
149 | "bmkeps(AALT bs r1 r2) = (if bnullable(r1) then bs @ (bmkeps r1) else bs @ (bmkeps r2))" |
|
150 | "bmkeps(ASTAR bs r) = bs @ [S]" |
|
151 |
|
152 |
|
153 fun |
|
154 bder :: "char \<Rightarrow> arexp \<Rightarrow> arexp" |
|
155 where |
|
156 "bder c (AZERO) = AZERO" |
|
157 | "bder c (AONE bs) = AZERO" |
|
158 | "bder c (ACH bs d) = (if c = d then AONE bs else AZERO)" |
|
159 | "bder c (AALT bs r1 r2) = AALT bs (bder c r1) (bder c r2)" |
|
160 | "bder c (ASEQ bs r1 r2) = |
|
161 (if bnullable r1 |
|
162 then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2)) |
|
163 else ASEQ bs (bder c r1) r2)" |
|
164 | "bder c (ASTAR bs r) = ASEQ bs (fuse [Z] (bder c r)) (ASTAR [] r)" |
|
165 |
|
166 |
|
167 fun |
|
168 bders :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
|
169 where |
|
170 "bders r [] = r" |
|
171 | "bders r (c#s) = bders (bder c r) s" |
|
172 |
|
173 lemma bders_append: |
|
174 "bders r (s1 @ s2) = bders (bders r s1) s2" |
|
175 apply(induct s1 arbitrary: r s2) |
|
176 apply(simp_all) |
|
177 done |
|
178 |
|
179 lemma bnullable_correctness: |
|
180 shows "nullable (erase r) = bnullable r" |
|
181 apply(induct r) |
|
182 apply(simp_all) |
|
183 done |
|
184 |
|
185 lemma erase_fuse: |
|
186 shows "erase (fuse bs r) = erase r" |
|
187 apply(induct r) |
|
188 apply(simp_all) |
|
189 done |
|
190 |
|
191 lemma erase_intern[simp]: |
|
192 shows "erase (intern r) = r" |
|
193 apply(induct r) |
|
194 apply(simp_all add: erase_fuse) |
|
195 done |
|
196 |
|
197 lemma erase_bder[simp]: |
|
198 shows "erase (bder a r) = der a (erase r)" |
|
199 apply(induct r) |
|
200 apply(simp_all add: erase_fuse bnullable_correctness) |
|
201 done |
|
202 |
|
203 lemma erase_bders[simp]: |
|
204 shows "erase (bders r s) = ders s (erase r)" |
|
205 apply(induct s arbitrary: r ) |
|
206 apply(simp_all) |
|
207 done |
|
208 |
|
209 lemma retrieve_encode_STARS: |
|
210 assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (intern r) v" |
|
211 shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)" |
|
212 using assms |
|
213 apply(induct vs) |
|
214 apply(simp_all) |
|
215 done |
|
216 |
|
217 lemma retrieve_fuse2: |
|
218 assumes "\<Turnstile> v : (erase r)" |
|
219 shows "retrieve (fuse bs r) v = bs @ retrieve r v" |
|
220 using assms |
|
221 apply(induct r arbitrary: v bs) |
|
222 using retrieve_encode_STARS |
|
223 apply(auto elim!: Prf_elims) |
|
224 apply(case_tac vs) |
|
225 apply(simp) |
|
226 apply(simp) |
|
227 done |
|
228 |
|
229 lemma retrieve_fuse: |
|
230 assumes "\<Turnstile> v : r" |
|
231 shows "retrieve (fuse bs (intern r)) v = bs @ retrieve (intern r) v" |
|
232 using assms |
|
233 by (simp_all add: retrieve_fuse2) |
|
234 |
|
235 |
|
236 lemma retrieve_code: |
|
237 assumes "\<Turnstile> v : r" |
|
238 shows "code v = retrieve (intern r) v" |
|
239 using assms |
|
240 apply(induct v r) |
|
241 apply(simp_all add: retrieve_fuse retrieve_encode_STARS) |
|
242 done |
|
243 |
|
244 |
|
245 lemma bmkeps_retrieve: |
|
246 assumes "nullable (erase r)" |
|
247 shows "bmkeps r = retrieve r (mkeps (erase r))" |
|
248 using assms |
|
249 apply(induct r) |
|
250 apply(simp) |
|
251 apply(simp) |
|
252 apply(simp) |
|
253 apply(simp) |
|
254 apply(simp only: bmkeps.simps bnullable_correctness) |
|
255 apply(auto simp only: split: if_split) |
|
256 apply(auto simp add: bnullable_correctness) |
|
257 done |
|
258 |
|
259 lemma bder_retrieve: |
|
260 assumes "\<Turnstile> v : der c (erase r)" |
|
261 shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)" |
|
262 using assms |
|
263 apply(induct r arbitrary: v) |
|
264 apply(auto elim!: Prf_elims simp add: retrieve_fuse2 bnullable_correctness bmkeps_retrieve) |
|
265 done |
|
266 |
|
267 lemma MAIN_decode: |
|
268 assumes "\<Turnstile> v : ders s r" |
|
269 shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" |
|
270 using assms |
|
271 proof (induct s arbitrary: v rule: rev_induct) |
|
272 case Nil |
|
273 have "\<Turnstile> v : ders [] r" by fact |
|
274 then have "\<Turnstile> v : r" by simp |
|
275 then have "Some v = decode (retrieve (intern r) v) r" |
|
276 using decode_code retrieve_code by auto |
|
277 then show "Some (flex r id [] v) = decode (retrieve (bders (intern r) []) v) r" |
|
278 by simp |
|
279 next |
|
280 case (snoc c s v) |
|
281 have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow> |
|
282 Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" by fact |
|
283 have asm: "\<Turnstile> v : ders (s @ [c]) r" by fact |
|
284 then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r" |
|
285 by(simp add: Prf_injval ders_append) |
|
286 have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))" |
|
287 by (simp add: flex_append) |
|
288 also have "... = decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r" |
|
289 using asm2 IH by simp |
|
290 also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r" |
|
291 using asm by(simp_all add: bder_retrieve ders_append) |
|
292 finally show "Some (flex r id (s @ [c]) v) = |
|
293 decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append) |
|
294 qed |
|
295 |
|
296 |
|
297 definition blexer where |
|
298 "blexer r s \<equiv> if bnullable (bders (intern r) s) then |
|
299 decode (bmkeps (bders (intern r) s)) r else None" |
|
300 |
|
301 lemma blexer_correctness: |
|
302 shows "blexer r s = lexer r s" |
|
303 proof - |
|
304 { define bds where "bds \<equiv> bders (intern r) s" |
|
305 define ds where "ds \<equiv> ders s r" |
|
306 assume asm: "nullable ds" |
|
307 have era: "erase bds = ds" |
|
308 unfolding ds_def bds_def by simp |
|
309 have mke: "\<Turnstile> mkeps ds : ds" |
|
310 using asm by (simp add: mkeps_nullable) |
|
311 have "decode (bmkeps bds) r = decode (retrieve bds (mkeps ds)) r" |
|
312 using bmkeps_retrieve |
|
313 using asm era by (simp add: bmkeps_retrieve) |
|
314 also have "... = Some (flex r id s (mkeps ds))" |
|
315 using mke by (simp_all add: MAIN_decode ds_def bds_def) |
|
316 finally have "decode (bmkeps bds) r = Some (flex r id s (mkeps ds))" |
|
317 unfolding bds_def ds_def . |
|
318 } |
|
319 then show "blexer r s = lexer r s" |
|
320 unfolding blexer_def lexer_flex |
|
321 apply(subst bnullable_correctness[symmetric]) |
|
322 apply(simp) |
|
323 done |
|
324 qed |
|
325 |
|
326 |
|
327 |
|
328 end |