equal
deleted
inserted
replaced
357 apply(case_tac r) |
357 apply(case_tac r) |
358 apply simp+ |
358 apply simp+ |
359 done |
359 done |
360 |
360 |
361 |
361 |
362 lemma "set (tint (seqFold (erase x42) [erase x43])) = |
362 lemma tint_seqFold_eq: shows"set (tint (seqFold (erase x42) [erase x43])) = |
363 set (tint (SEQ (erase x42) (erase x43)))" |
363 set (tint (SEQ (erase x42) (erase x43)))" |
364 apply(case_tac "erase x42 = ONE") |
364 apply(case_tac "erase x42 = ONE") |
365 apply simp |
365 apply simp |
366 apply simp |
366 using seqFold_concats |
|
367 apply simp |
|
368 done |
|
369 |
|
370 fun top :: "arexp \<Rightarrow> bit list" where |
|
371 "top AZERO = []" |
|
372 | "top (AONE bs) = bs" |
|
373 | "top (ASEQ bs r1 r2) = bs" |
|
374 | "top (ACHAR v va) = v" |
|
375 | "top (AALTs v va) = v" |
|
376 | "top (ASTAR v va) = v " |
|
377 |
|
378 |
|
379 |
|
380 lemma top_bitcodes_preserved_p6: |
|
381 shows "\<lbrakk> r = ASEQ bs a1 a2 \<rbrakk> \<Longrightarrow> p6 as r = AZERO \<or> (\<exists>bs3. top (p6 as r) = bs @ bs3)" |
|
382 apply(induct r arbitrary: as) |
|
383 apply simp |
|
384 apply simp |
|
385 apply simp |
|
386 |
|
387 apply(case_tac "a1") |
|
388 apply simp |
|
389 |
|
390 |
|
391 sorry |
|
392 |
|
393 |
367 |
394 |
368 lemma prune6_preserves_fuse: |
395 lemma prune6_preserves_fuse: |
369 shows "fuse bs (p6 as a) = p6 as (fuse bs a)" |
396 shows "fuse bs (p6 as a) = p6 as (fuse bs a)" |
370 using tint_fuse2 |
397 using tint_fuse2 |
371 apply simp |
398 apply simp |
375 apply simp |
402 apply simp |
376 |
403 |
377 using fused_bits_at_head |
404 using fused_bits_at_head |
378 |
405 |
379 apply simp |
406 apply simp |
380 apply(case_tac "erase x42 = ONE") |
407 using tint_seqFold_eq |
381 apply simp |
408 apply simp |
382 |
409 |
383 sorry |
410 sorry |
384 |
411 |
385 corollary prune6_preserves_fuse_srewrite: |
412 corollary prune6_preserves_fuse_srewrite: |