165 else ASEQ bs (ader c r1) r2)" |
165 else ASEQ bs (ader c r1) r2)" |
166 | "ader c (ASTAR bs r) = ASEQ bs (fuse [False] (ader c r)) (ASTAR [] r)" |
166 | "ader c (ASTAR bs r) = ASEQ bs (fuse [False] (ader c r)) (ASTAR [] r)" |
167 |
167 |
168 |
168 |
169 fun |
169 fun |
170 aders :: "string \<Rightarrow> arexp \<Rightarrow> arexp" |
170 aders :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
171 where |
171 where |
172 "aders [] r = r" |
172 "aders r [] = r" |
173 | "aders (c # s) r = aders s (ader c r)" |
173 | "aders r (c#s) = aders (ader c r) s" |
174 |
174 |
175 fun |
175 lemma aders_append: |
176 alex :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
176 "aders r (s1 @ s2) = aders (aders r s1) s2" |
177 where |
177 apply(induct s1 arbitrary: r s2) |
178 "alex r [] = r" |
178 apply(simp_all) |
179 | "alex r (c#s) = alex (ader c r) s" |
179 done |
180 |
180 |
181 lemma anullable_correctness: |
181 lemma anullable_correctness: |
182 shows "nullable (aerase r) = anullable r" |
182 shows "nullable (aerase r) = anullable r" |
183 apply(induct r) |
183 apply(induct r) |
184 apply(simp_all) |
184 apply(simp_all) |
188 shows "aerase (fuse bs r) = aerase r" |
188 shows "aerase (fuse bs r) = aerase r" |
189 apply(induct r) |
189 apply(induct r) |
190 apply(simp_all) |
190 apply(simp_all) |
191 done |
191 done |
192 |
192 |
|
193 lemma aerase_internalise: |
|
194 shows "aerase (internalise r) = r" |
|
195 apply(induct r) |
|
196 apply(simp_all add: aerase_fuse) |
|
197 done |
193 |
198 |
194 lemma aerase_ader: |
199 lemma aerase_ader: |
195 shows "aerase (ader a r) = der a (aerase r)" |
200 shows "aerase (ader a r) = der a (aerase r)" |
196 apply(induct r) |
201 apply(induct r) |
197 apply(simp_all add: aerase_fuse anullable_correctness) |
202 apply(simp_all add: aerase_fuse anullable_correctness) |
198 done |
203 done |
199 |
204 |
200 lemma aerase_internalise: |
205 lemma aerase_aders: |
201 shows "aerase (internalise r) = r" |
206 shows "aerase (aders r s) = ders s (aerase r)" |
202 apply(induct r) |
|
203 apply(simp_all add: aerase_fuse) |
|
204 done |
|
205 |
|
206 |
|
207 lemma aerase_alex: |
|
208 shows "aerase (alex r s) = ders s (aerase r)" |
|
209 apply(induct s arbitrary: r ) |
207 apply(induct s arbitrary: r ) |
210 apply(simp_all add: aerase_ader) |
208 apply(simp_all add: aerase_ader) |
211 done |
209 done |
212 |
210 |
213 lemma retrieve_encode_STARS: |
211 lemma retrieve_encode_STARS: |
253 apply(induct v r) |
251 apply(induct v r) |
254 apply(simp_all add: retrieve_afuse retrieve_encode_STARS) |
252 apply(simp_all add: retrieve_afuse retrieve_encode_STARS) |
255 done |
253 done |
256 |
254 |
257 |
255 |
258 lemma alex_append: |
|
259 "alex r (s1 @ s2) = alex (alex r s1) s2" |
|
260 apply(induct s1 arbitrary: r s2) |
|
261 apply(simp_all) |
|
262 done |
|
263 |
|
264 lemma ders_append: |
|
265 shows "ders (s1 @ s2) r = ders s2 (ders s1 r)" |
|
266 apply(induct s1 arbitrary: s2 r) |
|
267 apply(auto) |
|
268 done |
|
269 |
|
270 |
256 |
271 |
257 |
272 |
258 |
273 lemma Q00: |
259 lemma Q00: |
274 assumes "s \<in> r \<rightarrow> v" |
260 assumes "s \<in> r \<rightarrow> v" |
275 shows "\<Turnstile> v : r" |
261 shows "\<Turnstile> v : r" |
276 using assms |
262 using assms |
277 apply(induct) |
263 apply(induct) |
278 apply(auto intro: Prf.intros) |
264 apply(auto intro: Prf.intros) |
279 by (metis Prf.intros(6) Prf_elims(6) insert_iff list.simps(15) val.inject(5)) |
265 by (metis Prf.intros(6) Prf_elims(6) insert_iff list.simps(15) val.inject(5)) |
280 |
266 |
281 lemma Qa: |
267 lemma Qa: |
282 assumes "anullable r" |
268 assumes "anullable r" |
283 shows "retrieve r (mkeps (aerase r)) = amkeps r" |
269 shows "retrieve r (mkeps (aerase r)) = amkeps r" |
318 apply(auto elim!: Prf_elims)[1] |
304 apply(auto elim!: Prf_elims)[1] |
319 apply(auto elim!: Prf_elims)[1] |
305 apply(auto elim!: Prf_elims)[1] |
320 apply(auto elim!: Prf_elims)[1] |
306 apply(auto elim!: Prf_elims)[1] |
321 by (simp add: retrieve_afuse2 aerase_ader) |
307 by (simp add: retrieve_afuse2 aerase_ader) |
322 |
308 |
323 |
|
324 |
|
325 |
|
326 lemma MAIN: |
309 lemma MAIN: |
327 assumes "\<Turnstile> v : ders s r" |
310 assumes "\<Turnstile> v : ders s r" |
328 shows "code (flex r id s v) = retrieve (alex (internalise r) s) v" |
311 shows "code (flex r id s v) = retrieve (aders (internalise r) s) v" |
329 using assms |
312 using assms |
330 apply(induct s arbitrary: r v rule: rev_induct) |
313 apply(induct s arbitrary: v rule: rev_induct) |
331 apply(simp) |
314 apply(simp) |
332 apply (simp add: retrieve_encode) |
315 apply(simp add: retrieve_encode) |
333 apply(simp add: flex_append alex_append) |
316 apply(simp add: flex_append aders_append) |
334 apply(subst Qb) |
317 apply(subst Qb) |
335 apply (simp add: aerase_internalise ders_append aerase_alex) |
318 apply(simp add: aerase_internalise ders_append aerase_aders) |
336 apply(simp add: aerase_alex aerase_internalise) |
319 apply(simp add: aerase_aders aerase_internalise) |
337 apply(drule_tac x="r" in meta_spec) |
|
338 apply(drule_tac x="injval (ders xs r) x v" in meta_spec) |
320 apply(drule_tac x="injval (ders xs r) x v" in meta_spec) |
339 apply(drule meta_mp) |
321 apply(drule meta_mp) |
340 apply (simp add: Prf_injval ders_append) |
322 apply(simp add: Prf_injval ders_append) |
341 apply(simp) |
323 apply(simp) |
342 done |
324 done |
343 |
325 |
344 fun alexer where |
326 fun alexer where |
345 "alexer r s = (if anullable (alex (internalise r) s) then |
327 "alexer r s = (if anullable (aders (internalise r) s) then |
346 decode (amkeps (alex (internalise r) s)) r else None)" |
328 decode (amkeps (aders (internalise r) s)) r else None)" |
347 |
329 |
348 |
330 |
349 lemma FIN: |
331 lemma FIN: |
350 "alexer r s = lexer r s" |
332 "alexer r s = lexer r s" |
351 apply(auto split: prod.splits) |
333 apply(auto simp add: lexer_flex) |
352 apply (smt MAIN Q00 Qa aerase_alex aerase_internalise anullable_correctness decode_code lexer_correctness(1) lexer_flex mkeps_nullable) |
334 apply (smt MAIN Q00 Qa aerase_aders aerase_internalise decode_code lexer_correctness(1) lexer_flex mkeps_nullable) |
353 apply (simp add: aerase_internalise anullable_correctness[symmetric] lexer_flex aerase_alex) |
335 apply (metis aerase_aders aerase_internalise anullable_correctness) |
354 done |
336 using aerase_aders aerase_internalise anullable_correctness by force |
355 |
337 |
356 unused_thms |
338 unused_thms |
357 |
339 |
358 end |
340 end |