equal
deleted
inserted
replaced
245 lemma bmkeps_retrieve: |
245 lemma bmkeps_retrieve: |
246 assumes "nullable (erase r)" |
246 assumes "nullable (erase r)" |
247 shows "bmkeps r = retrieve r (mkeps (erase r))" |
247 shows "bmkeps r = retrieve r (mkeps (erase r))" |
248 using assms |
248 using assms |
249 apply(induct r) |
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) |
250 apply(auto simp add: bnullable_correctness) |
256 apply(auto simp add: bnullable_correctness) |
251 done |
257 done |
252 |
258 |
253 lemma bder_retrieve: |
259 lemma bder_retrieve: |
254 assumes "\<Turnstile> v : der c (erase r)" |
260 assumes "\<Turnstile> v : der c (erase r)" |