301 prefer 2 |
301 prefer 2 |
302 apply (metis append.assoc append.left_neutral append_Cons) |
302 apply (metis append.assoc append.left_neutral append_Cons) |
303 apply(subgoal_tac "(cc @ a # dB6 cc' (tset (cc @ [a]))) s\<leadsto>* (cc @ (p6 cc a) # dB6 cc' (tset (cc @ [a])))") |
303 apply(subgoal_tac "(cc @ a # dB6 cc' (tset (cc @ [a]))) s\<leadsto>* (cc @ (p6 cc a) # dB6 cc' (tset (cc @ [a])))") |
304 sorry |
304 sorry |
305 |
305 |
306 (* |
306 |
307 lemma ss6_stronger_aux: |
|
308 shows "(rs1 @ rs2) s\<leadsto>* (rs1 @ dB6 rs2 (set (map erase rs1)))" |
|
309 apply(induct rs2 arbitrary: rs1) |
|
310 apply simp |
|
311 apply(case_tac "erase a \<in> erase ` set rs1") |
|
312 apply(simp) |
|
313 apply(drule_tac x = "rs1" in meta_spec) |
|
314 apply(subgoal_tac "(rs1 @ a # rs2) s\<leadsto>* (rs1 @ rs2)") |
|
315 using srewrites_trans apply blast |
|
316 using deletes_dB apply presburger |
|
317 apply(case_tac "set (turnIntoTerms (erase a)) \<subseteq> erase ` set rs1") |
|
318 |
|
319 apply simp |
|
320 |
|
321 apply(auto) |
|
322 prefer 2 |
|
323 apply(drule_tac x="rs1 @ [a]" in meta_spec) |
|
324 apply(simp) |
|
325 sorry |
|
326 *) |
|
327 |
307 |
328 |
308 |
329 lemma ss6_stronger: |
309 lemma ss6_stronger: |
330 shows "rs1 s\<leadsto>* dB6 rs1 {}" |
310 shows "rs1 s\<leadsto>* dB6 rs1 {}" |
331 using ss6 |
311 using ss6 |
375 | "top (AALTs v va) = v" |
357 | "top (AALTs v va) = v" |
376 | "top (ASTAR v va) = v " |
358 | "top (ASTAR v va) = v " |
377 |
359 |
378 |
360 |
379 |
361 |
380 lemma top_bitcodes_preserved_p6: |
362 |
381 shows "\<lbrakk> r = ASEQ bs a1 a2 \<rbrakk> \<Longrightarrow> p6 as r = AZERO \<or> (\<exists>bs3. top (p6 as r) = bs @ bs3)" |
363 lemma p6fa_aux: |
382 apply(induct r arbitrary: as) |
364 shows " fuse bs |
383 apply simp |
365 (bsimp_AALTs bs\<^sub>0 as) = |
|
366 |
|
367 (bsimp_AALTs (bs @ bs\<^sub>0) as)" |
|
368 by (metis bsimp_AALTs.simps(1) bsimp_AALTs.simps(2) bsimp_AALTs.simps(3) fuse.simps(1) fuse.simps(4) fuse_append neq_Nil_conv) |
|
369 |
|
370 |
|
371 lemma p6pfuse_alts: |
|
372 shows |
|
373 " \<And>bs\<^sub>0 as\<^sub>0. |
|
374 \<lbrakk>\<And>a bs. set (tint (erase a)) = set (tint (erase (fuse bs a))); a = AALTs bs\<^sub>0 as\<^sub>0\<rbrakk> |
|
375 \<Longrightarrow> \<not> set (tint (erase a)) \<subseteq> (\<Union>x\<in>set as. set (tint (erase x))) \<longrightarrow> |
|
376 fuse bs |
|
377 (case a of AZERO \<Rightarrow> AZERO | AONE x \<Rightarrow> AONE x | ACHAR x xa \<Rightarrow> ACHAR x xa |
|
378 | ASEQ bs r1 r2 \<Rightarrow> bsimp_ASEQ bs (prune6 (\<Union>x\<in>set as. set (tint (erase x))) r1 [erase r2]) r2 |
|
379 | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r. prune6 (\<Union>x\<in>set as. set (tint (erase x))) r []) rs0)) | ASTAR x xa \<Rightarrow> ASTAR x xa) |
|
380 = |
|
381 (case fuse bs a of AZERO \<Rightarrow> AZERO | AONE x \<Rightarrow> AONE x | ACHAR x xa \<Rightarrow> ACHAR x xa |
|
382 | ASEQ bs r1 r2 \<Rightarrow> bsimp_ASEQ bs (prune6 (\<Union>x\<in>set as. set (tint (erase x))) r1 [erase r2]) r2 |
|
383 | AALTs bs rs0 \<Rightarrow> bsimp_AALTs bs (filter notZero (map (\<lambda>r. prune6 (\<Union>x\<in>set as. set (tint (erase x))) r []) rs0)) | ASTAR x xa \<Rightarrow> ASTAR x xa)" |
384 apply simp |
384 apply simp |
385 apply simp |
385 using p6fa_aux by presburger |
386 |
386 |
387 apply(case_tac "a1") |
|
388 apply simp |
|
389 |
|
390 |
|
391 sorry |
|
392 |
387 |
393 |
388 |
394 |
389 |
395 lemma prune6_preserves_fuse: |
390 lemma prune6_preserves_fuse: |
396 shows "fuse bs (p6 as a) = p6 as (fuse bs a)" |
391 shows "fuse bs (p6 as a) = p6 as (fuse bs a)" |
404 using fused_bits_at_head |
399 using fused_bits_at_head |
405 |
400 |
406 apply simp |
401 apply simp |
407 using tint_seqFold_eq |
402 using tint_seqFold_eq |
408 apply simp |
403 apply simp |
409 |
404 apply (smt (z3) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1 bsimp_ASEQ2 fuse.simps(1) fuse.simps(5) fuse_append) |
|
405 using p6pfuse_alts apply presburger |
|
406 by simp |
|
407 |
|
408 |
|
409 (* |
|
410 The top-level bitlist stays the same: |
|
411 \<^sub>b\<^sub>sa ------pruning-----> \<^sub>b\<^sub>s\<^sub>' b \<Longrightarrow> \<exists>bs3. bs' = bs @ bs3 |
|
412 *) |
|
413 lemma top_bitcodes_preserved_p6: |
|
414 shows "top r = bs \<Longrightarrow> p6 as r = AZERO \<or> (\<exists>bs3. top (p6 as r) = bs @ bs3)" |
|
415 |
|
416 |
|
417 apply(induct r arbitrary: as) |
|
418 |
|
419 (*this sorry requires more care *) |
|
420 |
410 sorry |
421 sorry |
|
422 |
|
423 |
411 |
424 |
412 corollary prune6_preserves_fuse_srewrite: |
425 corollary prune6_preserves_fuse_srewrite: |
413 shows "(as @ map (fuse bs) [a] @ as2) s\<leadsto>* (as @ map (fuse bs) [p6 as a] @ as2)" |
426 shows "(as @ map (fuse bs) [a] @ as2) s\<leadsto>* (as @ map (fuse bs) [p6 as a] @ as2)" |
414 apply(subgoal_tac "map (fuse bs) [a] = [fuse bs a]") |
427 apply(subgoal_tac "map (fuse bs) [a] = [fuse bs a]") |
415 apply(subgoal_tac "(as @ [fuse bs a] @ as2) s\<leadsto>* (as @ [ (p6 as (fuse bs a))] @ as2)") |
428 apply(subgoal_tac "(as @ [fuse bs a] @ as2) s\<leadsto>* (as @ [ (p6 as (fuse bs a))] @ as2)") |
565 by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse) |
578 by (simp add: bmkepss1 bmkepss2 bmkepss_fuse bnullable_fuse) |
566 next |
579 next |
567 case (ss6 a1 a2 rsa rsb rsc) |
580 case (ss6 a1 a2 rsa rsb rsc) |
568 then show ?case |
581 then show ?case |
569 by (smt (verit, best) Nil_is_append_conv bmkepss1 bmkepss2 bnullable_correctness in_set_conv_decomp list.distinct(1) list.set_intros(1) nullable_correctness set_ConsD subsetD) |
582 by (smt (verit, best) Nil_is_append_conv bmkepss1 bmkepss2 bnullable_correctness in_set_conv_decomp list.distinct(1) list.set_intros(1) nullable_correctness set_ConsD subsetD) |
570 qed (auto) |
583 next |
|
584 prefer 10 |
|
585 case (ss7 as a as1) |
|
586 then show ?case |
|
587 |
|
588 (*this sorry requires more effort*) |
|
589 sorry |
|
590 qed(auto) |
571 |
591 |
572 lemma rewrites_bmkeps: |
592 lemma rewrites_bmkeps: |
573 assumes "r1 \<leadsto>* r2" "bnullable r1" |
593 assumes "r1 \<leadsto>* r2" "bnullable r1" |
574 shows "bmkeps r1 = bmkeps r2" |
594 shows "bmkeps r1 = bmkeps r2" |
575 using assms |
595 using assms |
604 |
624 |
605 lemma map1: |
625 lemma map1: |
606 shows "(map f [a]) = [f a]" |
626 shows "(map f [a]) = [f a]" |
607 by (simp) |
627 by (simp) |
608 |
628 |
|
629 lemma "set (tint (erase a)) \<subseteq> (\<Union>x\<in>set as. set (tint (erase x))) \<Longrightarrow> |
|
630 set (tint (erase (bder c a))) \<subseteq> (\<Union>x\<in>set (map (bder c) as). set (tint (erase x)))" |
|
631 |
|
632 sorry |
|
633 |
|
634 |
609 lemma rewrite_preserves_bder: |
635 lemma rewrite_preserves_bder: |
610 shows "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)" |
636 shows "r1 \<leadsto> r2 \<Longrightarrow> (bder c r1) \<leadsto>* (bder c r2)" |
611 and "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2" |
637 and "rs1 s\<leadsto> rs2 \<Longrightarrow> map (bder c) rs1 s\<leadsto>* map (bder c) rs2" |
612 proof(induction rule: rrewrite_srewrite.inducts) |
638 proof(induction rule: rrewrite_srewrite.inducts) |
613 case (bs1 bs r2) |
639 case (bs1 bs r2) |
679 apply(rule srewrites_trans) |
705 apply(rule srewrites_trans) |
680 apply(rule rs_in_rstar) |
706 apply(rule rs_in_rstar) |
681 apply(rule_tac rrewrite_srewrite.ss6) |
707 apply(rule_tac rrewrite_srewrite.ss6) |
682 using Der_def der_correctness apply auto[1] |
708 using Der_def der_correctness apply auto[1] |
683 by blast |
709 by blast |
|
710 next |
|
711 case (ss7 as a as1) |
|
712 then show ?case |
|
713 apply simp |
|
714 sorry |
684 qed |
715 qed |
685 |
716 |
686 lemma rewrites_preserves_bder: |
717 lemma rewrites_preserves_bder: |
687 assumes "r1 \<leadsto>* r2" |
718 assumes "r1 \<leadsto>* r2" |
688 shows "bder c r1 \<leadsto>* bder c r2" |
719 shows "bder c r1 \<leadsto>* bder c r2" |
731 by (simp add: bsimp_ASEQ1) |
762 by (simp add: bsimp_ASEQ1) |
732 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)" using as1 as2 IH1 IH2 |
763 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimp_ASEQ bs1 (bsimpStrong6 r1) (bsimpStrong6 r2)" using as1 as2 IH1 IH2 |
733 by (metis rrewrites_trans star_seq star_seq2) |
764 by (metis rrewrites_trans star_seq star_seq2) |
734 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" by simp |
765 then have "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" by simp |
735 } |
766 } |
736 ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" sorry |
767 ultimately show "ASEQ bs1 r1 r2 \<leadsto>* bsimpStrong6 (ASEQ bs1 r1 r2)" |
|
768 by blast |
737 next |
769 next |
738 case (2 bs1 rs) |
770 case (2 bs1 rs) |
739 have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimpStrong6 x" by fact |
771 have IH: "\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* bsimpStrong6 x" by fact |
740 then have "rs s\<leadsto>* (map bsimpStrong6 rs)" by (simp add: trivialbsimp_srewrites) |
772 then have "rs s\<leadsto>* (map bsimpStrong6 rs)" by (simp add: trivialbsimp_srewrites) |
741 also have "... s\<leadsto>* flts (map bsimpStrong6 rs)" by (simp add: fltsfrewrites) |
773 also have "... s\<leadsto>* flts (map bsimpStrong6 rs)" by (simp add: fltsfrewrites) |
742 also have "... s\<leadsto>* distinctWith (flts (map bsimpStrong6 rs)) eq1 {}" by (simp add: ss6_stronger) |
774 also have "... s\<leadsto>* dB6 (flts (map bsimpStrong6 rs)) {}" by (simp add: ss6_stronger) |
743 finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})" |
775 finally have "AALTs bs1 rs \<leadsto>* AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {})" |
744 using contextrewrites0 by auto |
776 using contextrewrites0 by auto |
745 also have "... \<leadsto>* bsimp_AALTs bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})" |
777 also have "... \<leadsto>* bsimp_AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {})" |
746 by (simp add: bsimp_AALTs_rewrites) |
778 by (simp add: bsimp_AALTs_rewrites) |
747 finally show "AALTs bs1 rs \<leadsto>* bsimpStrong6 (AALTs bs1 rs)" sorry |
779 finally show "AALTs bs1 rs \<leadsto>* bsimpStrong6 (AALTs bs1 rs)" |
|
780 using bsimpStrong6.simps(2) by presburger |
748 qed (simp_all) |
781 qed (simp_all) |
749 |
782 |
750 |
783 |
751 |
784 |
752 |
785 |