653 using grewrite.cases by fastforce |
669 using grewrite.cases by fastforce |
654 |
670 |
655 |
671 |
656 lemma impossible_grewrite2: |
672 lemma impossible_grewrite2: |
657 shows "\<not> ([RALTS rs] \<leadsto>g (RALTS rs) # a # rs)" |
673 shows "\<not> ([RALTS rs] \<leadsto>g (RALTS rs) # a # rs)" |
658 |
|
659 using grewrite_singleton by blast |
674 using grewrite_singleton by blast |
660 thm grewrite.cases |
675 |
661 lemma impossible_grewrite3: |
676 |
662 shows "\<not> (RALTS rs # rs1 \<leadsto>g (RALTS rs) # a # rs1)" |
677 |
663 oops |
678 |
664 |
679 lemma wront_sublist_grewrites: |
665 |
|
666 lemma grewrites_singleton: |
|
667 shows "[r] \<leadsto>g* r # rs \<Longrightarrow> rs = []" |
|
668 apply(induct "[r]" "r # rs" rule: grewrites.induct) |
|
669 apply simp |
|
670 |
|
671 oops |
|
672 |
|
673 lemma grewrite_nonequal_elem: |
|
674 shows "r # rs2 \<leadsto>g r # rs3 \<Longrightarrow> rs2 \<leadsto>g rs3" |
|
675 oops |
|
676 |
|
677 lemma grewrites_nonequal_elem: |
|
678 shows "r # rs2 \<leadsto>g* r # rs3 \<Longrightarrow> rs2 \<leadsto>g* rs3" |
|
679 apply(induct r) |
|
680 |
|
681 oops |
|
682 |
|
683 |
|
684 |
|
685 |
|
686 lemma : |
|
687 shows "rs1 @ rs2 \<leadsto>g* rs1 @ rs3 \<Longrightarrow> rs2 \<leadsto>g* rs3" |
680 shows "rs1 @ rs2 \<leadsto>g* rs1 @ rs3 \<Longrightarrow> rs2 \<leadsto>g* rs3" |
688 apply(induct rs1 arbitrary: rs2 rs3 rule: rev_induct) |
681 apply(induct rs1 arbitrary: rs2 rs3 rule: rev_induct) |
689 apply simp |
682 apply simp |
690 apply(drule_tac x = "[x] @ rs2" in meta_spec) |
683 apply(drule_tac x = "[x] @ rs2" in meta_spec) |
691 apply(drule_tac x = "[x] @ rs3" in meta_spec) |
684 apply(drule_tac x = "[x] @ rs3" in meta_spec) |
693 |
686 |
694 oops |
687 oops |
695 |
688 |
696 |
689 |
697 |
690 |
698 lemma grewrites_shape3_aux: |
691 |
699 shows "rs @ (rdistinct rsa (insert (RALTS rs) rsc)) \<leadsto>g* rs @ rdistinct (rflts (rdistinct rsa rsc)) (set rs)" |
692 lemma concat_rdistinct_equality1: |
700 apply(induct rsa arbitrary: rsc rs) |
693 shows "rdistinct (rs @ rsa) rset = rdistinct rs rset @ rdistinct rsa (rset \<union> (set rs))" |
701 apply simp |
694 apply(induct rs arbitrary: rsa rset) |
702 apply(case_tac "a \<in> rsc") |
695 apply simp |
703 apply simp |
696 apply(case_tac "a \<in> rset") |
704 apply(case_tac "a = RALTS rs") |
697 apply simp |
705 apply simp |
698 apply (simp add: insert_absorb) |
706 apply(subgoal_tac " rdistinct (rs @ rflts (rdistinct rsa (insert (RALTS rs) rsc))) (set rs) \<leadsto>g* |
699 by auto |
707 rdistinct (rflts (rdistinct rsa (insert (RALTS rs) rsc))) (set rs)") |
700 |
708 apply (metis insertI1 insert_absorb rdistinct_concat2) |
701 |
709 apply (simp add: rdistinct_concat) |
702 lemma ends_removal: |
710 |
703 shows " rsb @ rdistinct rs (set rsb) @ RALTS rs # rsc \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rsc" |
711 apply simp |
704 sorry |
712 apply(case_tac "a = RZERO") |
705 |
713 apply (metis gmany_steps_later grewrite.intros(1) grewrite_append rflts.simps(2)) |
706 lemma grewrites_rev_append: |
714 apply(case_tac "\<exists>rs1. a = RALTS rs1") |
707 shows "rs1 \<leadsto>g* rs2 \<Longrightarrow> rs1 @ [x] \<leadsto>g* rs2 @ [x]" |
715 prefer 2 |
708 using grewritess_concat by auto |
716 apply simp |
709 |
717 apply(subgoal_tac "rflts (a # rdistinct rsa (insert a rsc)) = a # rflts (rdistinct rsa (insert a rsc))") |
710 lemma grewrites_inclusion: |
718 apply (simp only:) |
711 shows "set rs \<subseteq> set rs1 \<Longrightarrow> rs1 @ rs \<leadsto>g* rs1" |
719 apply(case_tac "a \<notin> set rs") |
712 apply(induct rs arbitrary: rs1) |
720 apply simp |
713 apply simp |
721 apply(drule_tac x = "insert a rsc" in meta_spec) |
714 by (meson gmany_steps_later grewrite_variant1 list.set_intros(1) set_subset_Cons subset_code(1)) |
722 apply(drule_tac x = "rs " in meta_spec) |
715 |
723 |
716 lemma distinct_keeps_last: |
724 apply(erule exE) |
717 shows "\<lbrakk>x \<notin> rset; x \<notin> set xs \<rbrakk> \<Longrightarrow> rdistinct (xs @ [x]) rset = rdistinct xs rset @ [x]" |
725 apply simp |
718 by (simp add: concat_rdistinct_equality1) |
726 apply(subgoal_tac "RALTS rs1 # |
|
727 rdistinct rsa |
|
728 (insert (RALTS rs) |
|
729 (insert (RALTS rs1) |
|
730 rsc)) \<leadsto>g* rs1 @ |
|
731 rdistinct rsa |
|
732 (insert (RALTS rs) |
|
733 (insert (RALTS rs1) |
|
734 rsc)) ") |
|
735 apply(subgoal_tac " rs1 @ |
|
736 rdistinct rsa |
|
737 (insert (RALTS rs) |
|
738 (insert (RALTS rs1) |
|
739 rsc)) \<leadsto>g* |
|
740 rs1 @ |
|
741 rdistinct rsa |
|
742 (insert (RALTS rs) |
|
743 (insert (RALTS rs1) |
|
744 rsc))") |
|
745 |
|
746 apply(case_tac "a \<in> set rs") |
|
747 |
|
748 |
|
749 |
|
750 sorry |
|
751 |
|
752 |
|
753 lemma grewrites_shape3: |
|
754 shows " RALTS rs \<notin> set rsb \<Longrightarrow> |
|
755 rsb @ |
|
756 RALTS rs # |
|
757 rdistinct rsa |
|
758 (insert (RALTS rs) |
|
759 (set rsb)) \<leadsto>g* rsb @ |
|
760 rdistinct rs (set rsb) @ |
|
761 rdistinct (rflts (rdistinct rsa (set rsb \<union> set rs))) (set rs)" |
|
762 apply(subgoal_tac "rsb @ RALTS rs # rdistinct rsa (insert (RALTS rs) (set rsb)) \<leadsto>g* |
|
763 rsb @ rs @ rdistinct rsa (insert (RALTS rs) (set rsb))") |
|
764 prefer 2 |
|
765 using gr_in_rstar grewrite.intros(2) grewrites_append apply presburger |
|
766 apply(subgoal_tac "rsb @ rs @ rdistinct rsa (insert (RALTS rs) (set rsb )) \<leadsto>g* |
|
767 rsb @ rs @ rdistinct rsa (insert (RALTS rs) (set rsb \<union> set rs))") |
|
768 prefer 2 |
|
769 apply (metis Un_insert_left grewrite_rdistinct_aux grewrites_append) |
|
770 |
|
771 apply(subgoal_tac "rsb @ rs @ rdistinct rsa (insert (RALTS rs) (set rsb \<union> set rs)) \<leadsto>g* |
|
772 rsb @ rs @ rdistinct (rflts (rdistinct rsa (set rsb \<union> set rs))) (set rs)") |
|
773 prefer 2 |
|
774 using grewrites_append grewrites_shape3_aux apply presburger |
|
775 apply(subgoal_tac "rsb @ rs \<leadsto>g* rsb @ rdistinct rs (set rsb)") |
|
776 apply (smt (verit, ccfv_SIG) append_eq_appendI greal_trans grewrites.simps grewritess_concat) |
|
777 using gstar_rdistinct_general by blast |
|
778 |
|
779 |
719 |
780 lemma grewrites_shape2: |
720 lemma grewrites_shape2: |
781 shows " RALTS rs \<notin> set rsb \<Longrightarrow> |
721 shows " RALTS rs \<notin> set rsb \<Longrightarrow> |
782 rsb @ |
722 rsb @ |
783 rdistinct (rs @ rsa) |
723 rdistinct (rs @ rsa) |
784 (set rsb) \<leadsto>g* rsb @ |
724 (set rsb) \<leadsto>g* rsb @ |
785 rdistinct rs (set rsb) @ |
725 rdistinct rs (set rsb) @ |
786 rdistinct (rflts (rdistinct rsa (set rsb \<union> set rs))) (set rs)" |
726 rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})" |
787 |
727 apply(subgoal_tac " rdistinct (rs @ rsa) (set rsb) = rdistinct rs (set rsb) @ rdistinct rsa (set rs \<union> set rsb)") |
788 (* by (smt (z3) append.assoc distinct_3list flts_gstar greal_trans grewrites_append rdistinct_concat_general same_append_eq set_append) |
728 apply (simp only:) |
789 *) |
729 prefer 2 |
790 sorry |
730 apply (simp add: Un_commute concat_rdistinct_equality1) |
791 |
731 apply(induct rsa arbitrary: rs rsb rule: rev_induct) |
|
732 apply simp |
|
733 apply(case_tac "x \<in> set rs") |
|
734 apply (simp add: distinct_removes_middle3) |
|
735 apply(case_tac "x = RALTS rs") |
|
736 apply simp |
|
737 apply(case_tac "x \<in> set rsb") |
|
738 apply simp |
|
739 apply (simp add: concat_rdistinct_equality1) |
|
740 apply (simp add: concat_rdistinct_equality1) |
|
741 apply simp |
|
742 apply(drule_tac x = "rs " in meta_spec) |
|
743 apply(drule_tac x = rsb in meta_spec) |
|
744 apply simp |
|
745 apply(subgoal_tac " rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rdistinct xs (insert (RALTS rs) (set rs \<union> set rsb))") |
|
746 prefer 2 |
|
747 apply (simp add: concat_rdistinct_equality1) |
|
748 apply(case_tac "x \<in> set xs") |
|
749 apply simp |
|
750 apply (simp add: distinct_removes_last2) |
|
751 apply(case_tac "x \<in> set rsb") |
|
752 apply (smt (verit, ccfv_threshold) Un_iff append.right_neutral concat_rdistinct_equality1 insert_is_Un rdistinct.simps(2)) |
|
753 apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rdistinct (xs @ [x]) (set rs \<union> set rsb) = rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) @ [x]") |
|
754 apply(simp only:) |
|
755 apply(case_tac "x = RALTS rs") |
|
756 apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) @ [x] \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) @ rs") |
|
757 apply(subgoal_tac "rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) @ rs \<leadsto>g* rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb) ") |
|
758 apply (smt (verit, ccfv_SIG) Un_insert_left append.right_neutral concat_rdistinct_equality1 greal_trans insert_iff rdistinct.simps(2)) |
|
759 apply(subgoal_tac "set rs \<subseteq> set ( rsb @ rdistinct rs (set rsb) @ rdistinct xs (set rs \<union> set rsb))") |
|
760 apply (metis append.assoc grewrites_inclusion) |
|
761 apply (metis Un_upper1 append.assoc dual_order.trans list_dlist_union set_append) |
|
762 apply (metis append_Nil2 gr_in_rstar grewrite.intros(2) grewrite_append) |
|
763 apply(subgoal_tac " rsb @ rdistinct rs (set rsb) @ rdistinct (xs @ [x]) (insert (RALTS rs) (set rs \<union> set rsb)) = rsb @ rdistinct rs (set rsb) @ rdistinct (xs) (insert (RALTS rs) (set rs \<union> set rsb)) @ [x]") |
|
764 apply(simp only:) |
|
765 apply (metis append.assoc grewrites_rev_append) |
|
766 apply (simp add: insert_absorb) |
|
767 apply (simp add: distinct_keeps_last)+ |
|
768 done |
|
769 |
|
770 lemma rdistinct_add_acc: |
|
771 shows "rset2 \<subseteq> set rsb \<Longrightarrow> rsb @ rdistinct rs rset \<leadsto>g* rsb @ rdistinct rs (rset \<union> rset2)" |
|
772 apply(induct rs arbitrary: rsb rset rset2) |
|
773 apply simp |
|
774 apply (case_tac "a \<in> rset") |
|
775 apply simp |
|
776 apply(case_tac "a \<in> rset2") |
|
777 apply simp |
|
778 apply (meson create_nonexistent_distinct_set gr_in_rstar greal_trans grewrite_variant1 in_mono) |
|
779 apply simp |
|
780 apply(drule_tac x = "rsb @ [a]" in meta_spec) |
|
781 by (metis Un_insert_left append.assoc append_Cons append_Nil set_append sup.coboundedI1) |
|
782 |
|
783 |
|
784 lemma frewrite_fun1: |
|
785 shows " RALTS rs \<in> set rsb \<Longrightarrow> |
|
786 rsb @ rdistinct rsa (set rsb) \<leadsto>g* rflts rsb @ rdistinct rsa (set rsb \<union> set rs)" |
|
787 apply(subgoal_tac "rsb @ rdistinct rsa (set rsb) \<leadsto>g* rflts rsb @ rdistinct rsa (set rsb)") |
|
788 apply(subgoal_tac " set rs \<subseteq> set (rflts rsb)") |
|
789 prefer 2 |
|
790 using spilled_alts_contained apply blast |
|
791 apply(subgoal_tac "rflts rsb @ rdistinct rsa (set rsb) \<leadsto>g* rflts rsb @ rdistinct rsa (set rsb \<union> set rs)") |
|
792 using greal_trans apply blast |
|
793 using rdistinct_add_acc apply presburger |
|
794 using flts_gstar grewritess_concat by auto |
|
795 |
792 |
796 |
793 |
797 |
794 |
798 |
795 |
799 |
796 lemma frewrite_rd_grewrites: |
800 lemma frewrite_rd_grewrites: |
811 apply(erule exE) |
815 apply(erule exE) |
812 apply(rule_tac x = "rs3" in exI) |
816 apply(rule_tac x = "rs3" in exI) |
813 apply simp |
817 apply simp |
814 apply(case_tac "RALTS rs \<in> set rsb") |
818 apply(case_tac "RALTS rs \<in> set rsb") |
815 apply simp |
819 apply simp |
816 apply(rule_tac x = "rflts rsb @ rdistinct rsa (set rsb)" in exI) |
820 apply(rule_tac x = "rflts rsb @ rdistinct rsa (set rsb \<union> set rs)" in exI) |
817 apply(rule conjI) |
821 apply(rule conjI) |
818 apply (simp add: flts_gstar grewritess_concat) |
822 using frewrite_fun1 apply force |
819 apply (meson flts_gstar greal_trans grewrites.intros(1) grewrites_middle_distinct grewritess_concat) |
823 apply (metis frewrite_fun1 rdistinct_concat sup_ge2) |
820 apply(simp) |
824 apply(simp) |
821 apply(rule_tac x = |
825 apply(rule_tac x = |
822 "rsb @ (rdistinct rs (set rsb)) @ |
826 "rsb @ |
823 (rdistinct (rflts (rdistinct rsa ( (set rsb \<union> set rs)) ) ) (set rs))" in exI) |
827 rdistinct rs (set rsb) @ |
|
828 rdistinct rsa (set rs \<union> set rsb \<union> {RALTS rs})" in exI) |
824 apply(rule conjI) |
829 apply(rule conjI) |
825 prefer 2 |
830 prefer 2 |
826 using grewrites_shape2 apply force |
831 using grewrites_shape2 apply force |
827 using grewrites_shape3 by auto |
832 by (metis Un_insert_left frewrite_rd_grewrites_aux inf_sup_aci(5) insert_is_Un rdistinct.simps(2)) |
828 |
833 |
829 |
834 |
830 |
|
831 lemma frewrite_simprd: |
|
832 shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS rs1) = rsimp (RALTS rs2)" |
|
833 by (meson frewrite_simpeq) |
|
834 |
835 |
835 |
836 |
836 lemma frewrites_rd_grewrites: |
837 lemma frewrites_rd_grewrites: |
837 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> |
838 shows "rs1 \<leadsto>f* rs2 \<Longrightarrow> |
838 rsimp (RALTS rs1) = rsimp (RALTS rs2)" |
839 rsimp (RALTS rs1) = rsimp (RALTS rs2)" |
839 apply(induct rs1 rs2 rule: frewrites.induct) |
840 apply(induct rs1 rs2 rule: frewrites.induct) |
840 apply simp |
841 apply simp |
841 using frewrite_simprd by presburger |
842 using frewrite_simpeq by presburger |
842 |
|
843 |
|
844 |
|
845 |
843 |
846 lemma frewrite_simpeq2: |
844 lemma frewrite_simpeq2: |
847 shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))" |
845 shows "rs1 \<leadsto>f rs2 \<Longrightarrow> rsimp (RALTS (rdistinct rs1 {})) = rsimp (RALTS (rdistinct rs2 {}))" |
848 apply(subgoal_tac "\<exists> rs3. (rdistinct rs1 {} \<leadsto>g* rs3) \<and> (rdistinct rs2 {} \<leadsto>g* rs3)") |
846 apply(subgoal_tac "\<exists> rs3. (rdistinct rs1 {} \<leadsto>g* rs3) \<and> (rdistinct rs2 {} \<leadsto>g* rs3)") |
849 using grewrites_equal_rsimp apply fastforce |
847 using grewrites_equal_rsimp apply fastforce |
850 using frewrite_rd_grewrites by presburger |
848 by (metis append_self_conv2 frewrite_rd_grewrites list.set(1)) |
|
849 |
|
850 |
|
851 |
851 |
852 |
852 (*a more refined notion of \<leadsto>* is needed, |
853 (*a more refined notion of \<leadsto>* is needed, |
853 this lemma fails when rs1 contains some RALTS rs where elements |
854 this lemma fails when rs1 contains some RALTS rs where elements |
854 of rs appear in later parts of rs1, which will be picked up by rs2 |
855 of rs appear in later parts of rs1, which will be picked up by rs2 |
855 and deduplicated*) |
856 and deduplicated*) |