118 |
118 |
119 |
119 |
120 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where |
120 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where |
121 "retrieve (AONE bs) Void = bs" |
121 "retrieve (AONE bs) Void = bs" |
122 | "retrieve (ACHAR bs c) (Char d) = bs" |
122 | "retrieve (ACHAR bs c) (Char d) = bs" |
|
123 | "retrieve (AALTs bs [r]) v = bs @ retrieve r v" |
123 | "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v" |
124 | "retrieve (AALTs bs (r#rs)) (Left v) = bs @ retrieve r v" |
124 | "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v" |
125 | "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v" |
125 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2" |
126 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2" |
126 | "retrieve (ASTAR bs r) (Stars []) = bs @ [S]" |
127 | "retrieve (ASTAR bs r) (Stars []) = bs @ [S]" |
127 | "retrieve (ASTAR bs r) (Stars (v#vs)) = |
128 | "retrieve (ASTAR bs r) (Stars (v#vs)) = |
133 "erase AZERO = ZERO" |
134 "erase AZERO = ZERO" |
134 | "erase (AONE _) = ONE" |
135 | "erase (AONE _) = ONE" |
135 | "erase (ACHAR _ c) = CHAR c" |
136 | "erase (ACHAR _ c) = CHAR c" |
136 | "erase (AALTs _ []) = ZERO" |
137 | "erase (AALTs _ []) = ZERO" |
137 | "erase (AALTs _ [r]) = (erase r)" |
138 | "erase (AALTs _ [r]) = (erase r)" |
138 | "erase (AALTs _ (r#rs)) = ALT (erase r) (erase (AALTs [] rs))" |
139 | "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))" |
139 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)" |
140 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)" |
140 | "erase (ASTAR _ r) = STAR (erase r)" |
141 | "erase (ASTAR _ r) = STAR (erase r)" |
141 |
142 |
142 fun |
143 fun |
143 bnullable :: "arexp \<Rightarrow> bool" |
144 bnullable :: "arexp \<Rightarrow> bool" |
224 |
226 |
225 lemma retrieve_fuse2: |
227 lemma retrieve_fuse2: |
226 assumes "\<Turnstile> v : (erase r)" |
228 assumes "\<Turnstile> v : (erase r)" |
227 shows "retrieve (fuse bs r) v = bs @ retrieve r v" |
229 shows "retrieve (fuse bs r) v = bs @ retrieve r v" |
228 using assms |
230 using assms |
229 apply(induct r arbitrary: v bs rule: erase.induct) |
231 apply(induct r arbitrary: v bs) |
230 apply(auto elim: Prf_elims)[1] |
232 apply(auto elim: Prf_elims)[4] |
231 sorry |
233 defer |
|
234 using retrieve_encode_STARS |
|
235 apply(auto elim!: Prf_elims)[1] |
|
236 apply(case_tac vs) |
|
237 apply(simp) |
|
238 apply(simp) |
|
239 (* AALTs case *) |
|
240 apply(simp) |
|
241 apply(case_tac x2a) |
|
242 apply(simp) |
|
243 apply(auto elim!: Prf_elims)[1] |
|
244 apply(simp) |
|
245 apply(case_tac list) |
|
246 apply(simp) |
|
247 apply(auto) |
|
248 apply(auto elim!: Prf_elims)[1] |
|
249 done |
232 |
250 |
233 lemma retrieve_fuse: |
251 lemma retrieve_fuse: |
234 assumes "\<Turnstile> v : r" |
252 assumes "\<Turnstile> v : r" |
235 shows "retrieve (fuse bs (intern r)) v = bs @ retrieve (intern r) v" |
253 shows "retrieve (fuse bs (intern r)) v = bs @ retrieve (intern r) v" |
236 using assms |
254 using assms |
241 assumes "\<Turnstile> v : r" |
259 assumes "\<Turnstile> v : r" |
242 shows "code v = retrieve (intern r) v" |
260 shows "code v = retrieve (intern r) v" |
243 using assms |
261 using assms |
244 apply(induct v r ) |
262 apply(induct v r ) |
245 apply(simp_all add: retrieve_fuse retrieve_encode_STARS) |
263 apply(simp_all add: retrieve_fuse retrieve_encode_STARS) |
246 sorry |
264 done |
247 |
265 |
|
266 lemma r: |
|
267 assumes "bnullable (AALTs bs (a # rs))" |
|
268 shows "bnullable a \<or> (\<not> bnullable a \<and> bnullable (AALTs bs rs))" |
|
269 using assms |
|
270 apply(induct rs) |
|
271 apply(auto) |
|
272 done |
|
273 |
|
274 lemma r0: |
|
275 assumes "bnullable a" |
|
276 shows "bmkeps (AALTs bs (a # rs)) = bs @ (bmkeps a)" |
|
277 using assms |
|
278 by (metis bmkeps.simps(3) bmkeps.simps(4) list.exhaust) |
|
279 |
|
280 lemma r1: |
|
281 assumes "\<not> bnullable a" "bnullable (AALTs bs rs)" |
|
282 shows "bmkeps (AALTs bs (a # rs)) = bmkeps (AALTs bs rs)" |
|
283 using assms |
|
284 apply(induct rs) |
|
285 apply(auto) |
|
286 done |
|
287 |
|
288 lemma r2: |
|
289 assumes "x \<in> set rs" "bnullable x" |
|
290 shows "bnullable (AALTs bs rs)" |
|
291 using assms |
|
292 apply(induct rs) |
|
293 apply(auto) |
|
294 done |
|
295 |
|
296 lemma r3: |
|
297 assumes "\<not> bnullable r" |
|
298 " \<exists> x \<in> set rs. bnullable x" |
|
299 shows "retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs))) = |
|
300 retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs))))" |
|
301 using assms |
|
302 apply(induct rs arbitrary: r bs) |
|
303 apply(auto)[1] |
|
304 apply(auto) |
|
305 using bnullable_correctness apply blast |
|
306 apply(auto simp add: bnullable_correctness mkeps_nullable retrieve_fuse2) |
|
307 apply(subst retrieve_fuse2[symmetric]) |
|
308 apply (smt bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable) |
|
309 apply(simp) |
|
310 apply(case_tac "bnullable a") |
|
311 apply (smt append_Nil2 bnullable.simps(4) bnullable_correctness erase.simps(5) erase.simps(6) fuse.simps(4) insert_iff list.exhaust list.set(2) mkeps.simps(3) mkeps_nullable retrieve_fuse2) |
|
312 apply(drule_tac x="a" in meta_spec) |
|
313 apply(drule_tac x="bs" in meta_spec) |
|
314 apply(drule meta_mp) |
|
315 apply(simp) |
|
316 apply(drule meta_mp) |
|
317 apply(auto) |
|
318 apply(subst retrieve_fuse2[symmetric]) |
|
319 apply(case_tac rs) |
|
320 apply(simp) |
|
321 apply(auto)[1] |
|
322 apply (simp add: bnullable_correctness) |
|
323 apply (metis append_Nil2 bnullable_correctness erase_fuse fuse.simps(4) list.set_intros(1) mkeps.simps(3) mkeps_nullable nullable.simps(4) r2) |
|
324 apply (simp add: bnullable_correctness) |
|
325 apply (metis append_Nil2 bnullable_correctness erase.simps(6) erase_fuse fuse.simps(4) list.set_intros(2) mkeps.simps(3) mkeps_nullable r2) |
|
326 apply(simp) |
|
327 done |
|
328 |
|
329 |
|
330 lemma t: |
|
331 assumes "\<forall>r \<in> set rs. nullable (erase r) \<longrightarrow> bmkeps r = retrieve r (mkeps (erase r))" |
|
332 "nullable (erase (AALTs bs rs))" |
|
333 shows " bmkeps (AALTs bs rs) = retrieve (AALTs bs rs) (mkeps (erase (AALTs bs rs)))" |
|
334 using assms |
|
335 apply(induct rs arbitrary: bs) |
|
336 apply(simp) |
|
337 apply(auto simp add: bnullable_correctness) |
|
338 apply(case_tac rs) |
|
339 apply(auto simp add: bnullable_correctness)[2] |
|
340 apply(subst r1) |
|
341 apply(simp) |
|
342 apply(rule r2) |
|
343 apply(assumption) |
|
344 apply(simp) |
|
345 apply(drule_tac x="bs" in meta_spec) |
|
346 apply(drule meta_mp) |
|
347 apply(auto)[1] |
|
348 prefer 2 |
|
349 apply(case_tac "bnullable a") |
|
350 apply(subst r0) |
|
351 apply blast |
|
352 apply(subgoal_tac "nullable (erase a)") |
|
353 prefer 2 |
|
354 using bnullable_correctness apply blast |
|
355 apply (metis (no_types, lifting) erase.simps(5) erase.simps(6) list.exhaust mkeps.simps(3) retrieve.simps(3) retrieve.simps(4)) |
|
356 apply(subst r1) |
|
357 apply(simp) |
|
358 using r2 apply blast |
|
359 apply(drule_tac x="bs" in meta_spec) |
|
360 apply(drule meta_mp) |
|
361 apply(auto)[1] |
|
362 apply(simp) |
|
363 using r3 apply blast |
|
364 apply(auto) |
|
365 using r3 by blast |
248 |
366 |
249 lemma bmkeps_retrieve: |
367 lemma bmkeps_retrieve: |
250 assumes "nullable (erase r)" |
368 assumes "nullable (erase r)" |
251 shows "bmkeps r = retrieve r (mkeps (erase r))" |
369 shows "bmkeps r = retrieve r (mkeps (erase r))" |
252 using assms |
370 using assms |
253 apply(induct r) |
371 apply(induct r) |
254 apply(auto simp add: bnullable_correctness) |
372 apply(simp) |
255 sorry |
373 apply(simp) |
256 |
374 apply(simp) |
|
375 apply(simp) |
|
376 defer |
|
377 apply(simp) |
|
378 apply(rule t) |
|
379 apply(auto) |
|
380 done |
|
381 |
257 lemma bder_retrieve: |
382 lemma bder_retrieve: |
258 assumes "\<Turnstile> v : der c (erase r)" |
383 assumes "\<Turnstile> v : der c (erase r)" |
259 shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)" |
384 shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)" |
260 using assms |
385 using assms |
261 apply(induct r arbitrary: v) |
386 apply(induct r arbitrary: v rule: erase.induct) |
262 apply(auto elim!: Prf_elims simp add: retrieve_fuse2 bnullable_correctness bmkeps_retrieve) |
387 apply(auto elim!: Prf_elims simp add: retrieve_fuse2 bnullable_correctness bmkeps_retrieve) |
263 sorry |
388 apply(case_tac va) |
|
389 apply(simp) |
|
390 apply(auto) |
|
391 by (smt Prf_elims(3) injval.simps(2) injval.simps(3) retrieve.simps(4) retrieve.simps(5) same_append_eq) |
|
392 |
264 |
393 |
265 lemma MAIN_decode: |
394 lemma MAIN_decode: |
266 assumes "\<Turnstile> v : ders s r" |
395 assumes "\<Turnstile> v : ders s r" |
267 shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" |
396 shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" |
268 using assms |
397 using assms |