542 |
542 |
543 lemma many_steps_later: "\<lbrakk>r1 \<leadsto>f r2; r2 \<leadsto>f* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>f* r3" |
543 lemma many_steps_later: "\<lbrakk>r1 \<leadsto>f r2; r2 \<leadsto>f* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>f* r3" |
544 by (meson fr_in_rstar freal_trans) |
544 by (meson fr_in_rstar freal_trans) |
545 |
545 |
546 |
546 |
|
547 lemma gr_in_rstar : "r1 \<leadsto>g r2 \<Longrightarrow> r1 \<leadsto>g* r2" |
|
548 using grewrites.intros(1) grewrites.intros(2) by blast |
|
549 |
|
550 lemma greal_trans[trans]: |
|
551 assumes a1: "r1 \<leadsto>g* r2" and a2: "r2 \<leadsto>g* r3" |
|
552 shows "r1 \<leadsto>g* r3" |
|
553 using a2 a1 |
|
554 apply(induct r2 r3 arbitrary: r1 rule: grewrites.induct) |
|
555 apply(auto) |
|
556 done |
|
557 |
|
558 |
|
559 lemma gmany_steps_later: "\<lbrakk>r1 \<leadsto>g r2; r2 \<leadsto>g* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>g* r3" |
|
560 by (meson gr_in_rstar greal_trans) |
|
561 |
|
562 |
|
563 |
547 lemma frewrite_append: |
564 lemma frewrite_append: |
548 shows "\<lbrakk> rsa \<leadsto>f rsb \<rbrakk> \<Longrightarrow> rs @ rsa \<leadsto>f rs @ rsb" |
565 shows "\<lbrakk> rsa \<leadsto>f rsb \<rbrakk> \<Longrightarrow> rs @ rsa \<leadsto>f rs @ rsb" |
549 apply(induct rs) |
566 apply(induct rs) |
550 apply simp+ |
567 apply simp+ |
551 using frewrite.intros(3) by blast |
568 using frewrite.intros(3) by blast |
|
569 |
|
570 lemma grewrite_append: |
|
571 shows "\<lbrakk> rsa \<leadsto>g rsb \<rbrakk> \<Longrightarrow> rs @ rsa \<leadsto>g rs @ rsb" |
|
572 apply(induct rs) |
|
573 apply simp+ |
|
574 using grewrite.intros(3) by blast |
552 |
575 |
553 |
576 |
554 |
577 |
555 lemma frewrites_cons: |
578 lemma frewrites_cons: |
556 shows "\<lbrakk> rsa \<leadsto>f* rsb \<rbrakk> \<Longrightarrow> r # rsa \<leadsto>f* r # rsb" |
579 shows "\<lbrakk> rsa \<leadsto>f* rsb \<rbrakk> \<Longrightarrow> r # rsa \<leadsto>f* r # rsb" |
557 apply(induct rsa rsb rule: frewrites.induct) |
580 apply(induct rsa rsb rule: frewrites.induct) |
558 apply simp |
581 apply simp |
559 using frewrite.intros(3) by blast |
582 using frewrite.intros(3) by blast |
560 |
583 |
561 |
584 |
|
585 lemma grewrites_cons: |
|
586 shows "\<lbrakk> rsa \<leadsto>g* rsb \<rbrakk> \<Longrightarrow> r # rsa \<leadsto>g* r # rsb" |
|
587 apply(induct rsa rsb rule: grewrites.induct) |
|
588 apply simp |
|
589 using grewrite.intros(3) by blast |
|
590 |
|
591 |
562 lemma frewrites_append: |
592 lemma frewrites_append: |
563 shows " \<lbrakk>rsa \<leadsto>f* rsb\<rbrakk> \<Longrightarrow> (rs @ rsa) \<leadsto>f* (rs @ rsb)" |
593 shows " \<lbrakk>rsa \<leadsto>f* rsb\<rbrakk> \<Longrightarrow> (rs @ rsa) \<leadsto>f* (rs @ rsb)" |
564 apply(induct rs) |
594 apply(induct rs) |
565 apply simp |
595 apply simp |
566 by (simp add: frewrites_cons) |
596 by (simp add: frewrites_cons) |
|
597 |
|
598 lemma grewrites_append: |
|
599 shows " \<lbrakk>rsa \<leadsto>g* rsb\<rbrakk> \<Longrightarrow> (rs @ rsa) \<leadsto>g* (rs @ rsb)" |
|
600 apply(induct rs) |
|
601 apply simp |
|
602 by (simp add: grewrites_cons) |
567 |
603 |
568 |
604 |
569 |
605 |
570 lemma frewrites_concat: |
606 lemma frewrites_concat: |
571 shows "\<lbrakk>rs1 \<leadsto>f rs2; rsa \<leadsto>f* rsb \<rbrakk> \<Longrightarrow> (rs1 @ rsa) \<leadsto>f* (rs2 @ rsb)" |
607 shows "\<lbrakk>rs1 \<leadsto>f rs2; rsa \<leadsto>f* rsb \<rbrakk> \<Longrightarrow> (rs1 @ rsa) \<leadsto>f* (rs2 @ rsb)" |
578 using many_steps_later apply blast |
614 using many_steps_later apply blast |
579 apply (simp add: frewrites_append) |
615 apply (simp add: frewrites_append) |
580 apply (metis append.assoc append_Cons frewrite.intros(2) frewrites_append many_steps_later) |
616 apply (metis append.assoc append_Cons frewrite.intros(2) frewrites_append many_steps_later) |
581 using frewrites_cons by auto |
617 using frewrites_cons by auto |
582 |
618 |
|
619 lemma grewrites_concat: |
|
620 shows "\<lbrakk>rs1 \<leadsto>g rs2; rsa \<leadsto>g* rsb \<rbrakk> \<Longrightarrow> (rs1 @ rsa) \<leadsto>g* (rs2 @ rsb)" |
|
621 apply(induct rs1 rs2 rule: grewrite.induct) |
|
622 apply(simp) |
|
623 apply(subgoal_tac "(RZERO # rs @ rsa) \<leadsto>g (rs @ rsa)") |
|
624 prefer 2 |
|
625 using grewrite.intros(1) apply blast |
|
626 apply(subgoal_tac "(rs @ rsa) \<leadsto>g* (rs @ rsb)") |
|
627 using gmany_steps_later apply blast |
|
628 apply (simp add: grewrites_append) |
|
629 apply (metis append.assoc append_Cons grewrite.intros(2) grewrites_append gmany_steps_later) |
|
630 using grewrites_cons apply auto |
|
631 apply(subgoal_tac "rsaa @ a # rsba @ a # rsc @ rsa \<leadsto>g* rsaa @ a # rsba @ a # rsc @ rsb") |
|
632 using grewrite.intros(4) grewrites.intros(2) apply force |
|
633 using grewrites_append by auto |
|
634 |
|
635 |
|
636 lemma grewritess_concat: |
|
637 shows "\<lbrakk>rsa \<leadsto>g* rsb; rsc \<leadsto>g* rsd \<rbrakk> \<Longrightarrow> (rsa @ rsc) \<leadsto>g* (rsb @ rsd)" |
|
638 apply(induct rsa rsb rule: grewrites.induct) |
|
639 apply(case_tac rs) |
|
640 apply simp |
|
641 using grewrites_append apply blast |
|
642 by (meson greal_trans grewrites.simps grewrites_concat) |
|
643 |
|
644 lemma grewrites_equal_rsimp: |
|
645 shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)" |
|
646 apply simp |
|
647 sorry |
|
648 |
|
649 |
583 lemma frewrites_middle: |
650 lemma frewrites_middle: |
584 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> r # (RALTS rs # rs1) \<leadsto>f* r # (rs @ rs1)" |
651 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> r # (RALTS rs # rs1) \<leadsto>f* r # (rs @ rs1)" |
585 by (simp add: fr_in_rstar frewrite.intros(2) frewrite.intros(3)) |
652 by (simp add: fr_in_rstar frewrite.intros(2) frewrite.intros(3)) |
586 |
653 |
587 lemma frewrites_alt: |
654 lemma frewrites_alt: |
588 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> (RALT r1 r2) # rs1 \<leadsto>f* r1 # r2 # rs2" |
655 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> (RALT r1 r2) # rs1 \<leadsto>f* r1 # r2 # rs2" |
589 by (metis Cons_eq_appendI append_self_conv2 frewrite.intros(2) frewrites_cons many_steps_later) |
656 by (metis Cons_eq_appendI append_self_conv2 frewrite.intros(2) frewrites_cons many_steps_later) |
590 |
|
591 lemma many_steps_later1: |
|
592 shows " \<lbrakk>rs1 \<leadsto>f* rs2\<rbrakk> |
|
593 \<Longrightarrow> (RONE # rs1) \<leadsto>f* (RONE # rs2)" |
|
594 oops |
|
595 |
657 |
596 lemma early_late_der_frewrites: |
658 lemma early_late_der_frewrites: |
597 shows "map (rder x) (rflts rs) \<leadsto>f* rflts (map (rder x) rs)" |
659 shows "map (rder x) (rflts rs) \<leadsto>f* rflts (map (rder x) rs)" |
598 apply(induct rs) |
660 apply(induct rs) |
599 apply simp |
661 apply simp |
618 | "alt_set r = {r}" |
680 | "alt_set r = {r}" |
619 |
681 |
620 |
682 |
621 |
683 |
622 lemma rd_flts_set: |
684 lemma rd_flts_set: |
623 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rdistinct rs1 (insert RZERO (rset \<union> (\<Union>(alt_set ` rset)))) \<leadsto>f* |
685 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rdistinct rs1 ({RZERO} \<union> (rset \<union> \<Union>(alt_set ` rset))) \<leadsto>g* |
624 rdistinct rs2 (rset \<union> (\<Union>(alt_set ` rset)))" |
686 rdistinct rs2 ({RZERO} \<union> (rset \<union> \<Union>(alt_set ` rset)))" |
625 |
687 sorry |
626 oops |
|
627 |
|
628 |
|
629 |
|
630 lemma rd_flts_set2: |
|
631 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rdistinct rs1 ((rset \<union> (\<Union>(alt_set ` rset)))) \<leadsto>f* |
|
632 rdistinct rs2 (rset \<union> (\<Union>(alt_set ` rset)))" |
|
633 oops |
|
634 |
|
635 |
|
636 |
|
637 lemma flts_does_rewrite: |
|
638 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> rflts rs1 = rflts rs2" |
|
639 oops |
|
640 |
688 |
641 lemma with_wo0_distinct: |
689 lemma with_wo0_distinct: |
642 shows "rdistinct rs rset \<leadsto>f* rdistinct rs (insert RZERO rset)" |
690 shows "rdistinct rs rset \<leadsto>f* rdistinct rs (insert RZERO rset)" |
643 apply(induct rs arbitrary: rset) |
691 apply(induct rs arbitrary: rset) |
644 apply simp |
692 apply simp |
661 apply(case_tac "a \<in> rset") |
709 apply(case_tac "a \<in> rset") |
662 apply simp |
710 apply simp |
663 apply (simp add: frewrites_cons) |
711 apply (simp add: frewrites_cons) |
664 done |
712 done |
665 |
713 |
666 lemma rdistinct_concat: |
|
667 shows "set rs \<subseteq> rset \<Longrightarrow> rdistinct (rs @ rsa) rset = rdistinct rsa rset" |
|
668 apply(induct rs) |
|
669 apply simp+ |
|
670 done |
|
671 |
|
672 lemma rdistinct_concat2: |
|
673 shows "\<forall>r \<in> set rs. r \<in> rset \<Longrightarrow> rdistinct (rs @ rsa) rset = rdistinct rsa rset" |
|
674 by (simp add: rdistinct_concat subsetI) |
|
675 |
714 |
676 lemma frewrite_with_distinct: |
715 lemma frewrite_with_distinct: |
677 shows " \<lbrakk>rs2 \<leadsto>f rs3\<rbrakk> |
716 shows " \<lbrakk>rs2 \<leadsto>f rs3\<rbrakk> |
678 \<Longrightarrow> rdistinct rs2 |
717 \<Longrightarrow> rdistinct rs2 |
679 (insert RZERO (rset \<union> \<Union> (alt_set ` rset))) \<leadsto>f* |
718 (insert RZERO (rset \<union> \<Union> (alt_set ` rset))) \<leadsto>f* |