equal
deleted
inserted
replaced
261 shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)" |
261 shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)" |
262 using assms |
262 using assms |
263 apply(induct vs) |
263 apply(induct vs) |
264 apply(simp_all) |
264 apply(simp_all) |
265 done |
265 done |
|
266 |
|
267 lemma retrieve_codestars2: |
|
268 assumes "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> code v = retrieve (intern r) v" |
|
269 shows "retrieve (ASTAR bs (intern r)) (Stars []) = bs @ [S]" |
|
270 apply simp |
|
271 done |
|
272 |
266 |
273 |
267 lemma retrieve_fuse2: |
274 lemma retrieve_fuse2: |
268 assumes "\<Turnstile> v : (erase r)" |
275 assumes "\<Turnstile> v : (erase r)" |
269 shows "retrieve (fuse bs r) v = bs @ retrieve r v" |
276 shows "retrieve (fuse bs r) v = bs @ retrieve r v" |
270 using assms |
277 using assms |