48 | "decode' (Z # bs) (STAR r) = (let (v, bs') = decode' bs r in |
48 | "decode' (Z # bs) (STAR r) = (let (v, bs') = decode' bs r in |
49 let (vs, bs'') = decode' bs' (STAR r) |
49 let (vs, bs'') = decode' bs' (STAR r) |
50 in (Stars_add v vs, bs''))" |
50 in (Stars_add v vs, bs''))" |
51 | "decode' [] (NTIMES r n) = (Void, [])" |
51 | "decode' [] (NTIMES r n) = (Void, [])" |
52 | "decode' (S # bs) (NTIMES r n) = (Stars [], bs)" |
52 | "decode' (S # bs) (NTIMES r n) = (Stars [], bs)" |
53 (*| "decode' (Z # bs) (NTIMES r 0) = (undefined, bs)"*) |
|
54 | "decode' (Z # bs) (NTIMES r n) = (let (v, bs') = decode' bs r in |
53 | "decode' (Z # bs) (NTIMES r n) = (let (v, bs') = decode' bs r in |
55 let (vs, bs'') = decode' bs' (NTIMES r (n - 1)) |
54 let (vs, bs'') = decode' bs' (NTIMES r (n - 1)) |
56 in (Stars_add v vs, bs''))" |
55 in (Stars_add v vs, bs''))" |
57 by pat_completeness auto |
56 by pat_completeness auto |
58 |
57 |
213 "bmkeps(AONE bs) = bs" |
212 "bmkeps(AONE bs) = bs" |
214 | "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)" |
213 | "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)" |
215 | "bmkeps(AALTs bs (r#rs)) = |
214 | "bmkeps(AALTs bs (r#rs)) = |
216 (if bnullable(r) then (bs @ bmkeps r) else (bmkeps (AALTs bs rs)))" |
215 (if bnullable(r) then (bs @ bmkeps r) else (bmkeps (AALTs bs rs)))" |
217 | "bmkeps(ASTAR bs r) = bs @ [S]" |
216 | "bmkeps(ASTAR bs r) = bs @ [S]" |
218 | "bmkeps(ANTIMES bs r 0) = bs @ [S]" |
217 | "bmkeps(ANTIMES bs r n) = |
219 | "bmkeps(ANTIMES bs r (Suc n)) = bs @ [Z] @ (bmkeps r) @ bmkeps(ANTIMES [] r n)" |
218 (if n = 0 then bs @ [S] else bs @ [Z] @ (bmkeps r) @ bmkeps(ANTIMES [] r (n - 1)))" |
220 apply(pat_completeness) |
219 apply(pat_completeness) |
221 apply(auto) |
220 apply(auto) |
222 done |
221 done |
223 |
222 |
224 termination "bmkeps" |
223 termination "bmkeps" |
426 using assms |
425 using assms |
427 apply(induct r rule: bmkeps.induct) |
426 apply(induct r rule: bmkeps.induct) |
428 apply(auto) |
427 apply(auto) |
429 apply (simp add: retrieve_AALTs_bnullable1) |
428 apply (simp add: retrieve_AALTs_bnullable1) |
430 using retrieve_AALTs_bnullable1 apply force |
429 using retrieve_AALTs_bnullable1 apply force |
431 by (metis retrieve_AALTs_bnullable2) |
430 apply(metis retrieve_AALTs_bnullable2) |
|
431 by (metis Cons_eq_appendI One_nat_def Suc_diff_1 eq_Nil_appendI replicate_Suc retrieve.simps(10)) |
432 |
432 |
433 |
433 |
434 lemma bder_retrieve: |
434 lemma bder_retrieve: |
435 assumes "\<Turnstile> v : der c (erase r)" |
435 assumes "\<Turnstile> v : der c (erase r)" |
436 shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)" |
436 shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)" |