575 lemma alphas3: |
576 lemma alphas3: |
576 "(bsl, x1, x2, x3) \<approx>lst (\<lambda>(x1, y1, z1) (x2, y2, z2). R1 x1 x2 \<and> R2 y1 y2 \<and> R3 z1 z2) (\<lambda>(a, b, c). f1 a \<union> (f2 b \<union> f3 c)) pi (csl, y1, y2, y3) = (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl = f1 y1 \<union> (f2 y2 \<union> f3 y3) - set csl \<and> |
577 "(bsl, x1, x2, x3) \<approx>lst (\<lambda>(x1, y1, z1) (x2, y2, z2). R1 x1 x2 \<and> R2 y1 y2 \<and> R3 z1 z2) (\<lambda>(a, b, c). f1 a \<union> (f2 b \<union> f3 c)) pi (csl, y1, y2, y3) = (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl = f1 y1 \<union> (f2 y2 \<union> f3 y3) - set csl \<and> |
577 (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl) \<sharp>* pi \<and> |
578 (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl) \<sharp>* pi \<and> |
578 R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 \<and> R3 (pi \<bullet> x3) y3 \<and> pi \<bullet> bsl = csl)" |
579 R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 \<and> R3 (pi \<bullet> x3) y3 \<and> pi \<bullet> bsl = csl)" |
579 by (simp add: alphas) |
580 by (simp add: alphas) |
580 |
|
581 lemma alpha_gen_compose_sym: |
|
582 fixes pi |
|
583 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
|
584 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
585 shows "(ab, s) \<approx>gen R f (- pi) (aa, t)" |
|
586 using b apply - |
|
587 apply(simp add: alphas) |
|
588 apply(erule conjE)+ |
|
589 apply(rule conjI) |
|
590 apply(simp add: fresh_star_def fresh_minus_perm) |
|
591 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
|
592 apply simp |
|
593 apply(clarify) |
|
594 apply(simp) |
|
595 apply(rule a) |
|
596 apply assumption |
|
597 done |
|
598 |
|
599 lemma alpha_res_compose_sym: |
|
600 fixes pi |
|
601 assumes b: "(aa, t) \<approx>res (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
|
602 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
603 shows "(ab, s) \<approx>res R f (- pi) (aa, t)" |
|
604 using b apply - |
|
605 apply(simp add: alphas) |
|
606 apply(erule conjE)+ |
|
607 apply(rule conjI) |
|
608 apply(simp add: fresh_star_def fresh_minus_perm) |
|
609 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
|
610 apply simp |
|
611 apply(rule a) |
|
612 apply assumption |
|
613 done |
|
614 |
|
615 lemma alpha_lst_compose_sym: |
|
616 fixes pi |
|
617 assumes b: "(aa, t) \<approx>lst (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
|
618 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
619 shows "(ab, s) \<approx>lst R f (- pi) (aa, t)" |
|
620 using b apply - |
|
621 apply(simp add: alphas) |
|
622 apply(erule conjE)+ |
|
623 apply(rule conjI) |
|
624 apply(simp add: fresh_star_def fresh_minus_perm) |
|
625 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
|
626 apply simp |
|
627 apply(clarify) |
|
628 apply(simp) |
|
629 apply(rule a) |
|
630 apply assumption |
|
631 done |
|
632 |
|
633 lemmas alphas_compose_sym = alpha_gen_compose_sym alpha_res_compose_sym alpha_lst_compose_sym |
|
634 |
|
635 lemma alpha_gen_compose_sym2: |
|
636 assumes a: "(aa, t1, t2) \<approx>gen (\<lambda>(x11, x12) (x21, x22). |
|
637 (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)" |
|
638 and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)" |
|
639 and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)" |
|
640 shows "(ab, s1, s2) \<approx>gen (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)" |
|
641 using a |
|
642 apply(simp add: alphas) |
|
643 apply clarify |
|
644 apply (rule conjI) |
|
645 apply(simp add: fresh_star_def fresh_minus_perm) |
|
646 apply (rule conjI) |
|
647 apply (rotate_tac 3) |
|
648 apply (drule_tac pi="- pi" in r1) |
|
649 apply simp |
|
650 apply (rule conjI) |
|
651 apply (rotate_tac -1) |
|
652 apply (drule_tac pi="- pi" in r2) |
|
653 apply simp_all |
|
654 done |
|
655 |
|
656 lemma alpha_res_compose_sym2: |
|
657 assumes a: "(aa, t1, t2) \<approx>res (\<lambda>(x11, x12) (x21, x22). |
|
658 (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)" |
|
659 and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)" |
|
660 and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)" |
|
661 shows "(ab, s1, s2) \<approx>res (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)" |
|
662 using a |
|
663 apply(simp add: alphas) |
|
664 apply clarify |
|
665 apply (rule conjI) |
|
666 apply(simp add: fresh_star_def fresh_minus_perm) |
|
667 apply (rule conjI) |
|
668 apply (rotate_tac 3) |
|
669 apply (drule_tac pi="- pi" in r1) |
|
670 apply simp |
|
671 apply (rotate_tac -1) |
|
672 apply (drule_tac pi="- pi" in r2) |
|
673 apply simp |
|
674 done |
|
675 |
|
676 lemma alpha_lst_compose_sym2: |
|
677 assumes a: "(aa, t1, t2) \<approx>lst (\<lambda>(x11, x12) (x21, x22). |
|
678 (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)" |
|
679 and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)" |
|
680 and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)" |
|
681 shows "(ab, s1, s2) \<approx>lst (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)" |
|
682 using a |
|
683 apply(simp add: alphas) |
|
684 apply clarify |
|
685 apply (rule conjI) |
|
686 apply(simp add: fresh_star_def fresh_minus_perm) |
|
687 apply (rule conjI) |
|
688 apply (rotate_tac 3) |
|
689 apply (drule_tac pi="- pi" in r1) |
|
690 apply simp |
|
691 apply (rule conjI) |
|
692 apply (rotate_tac -1) |
|
693 apply (drule_tac pi="- pi" in r2) |
|
694 apply simp_all |
|
695 done |
|
696 |
|
697 lemmas alphas_compose_sym2 = alpha_gen_compose_sym2 alpha_res_compose_sym2 alpha_lst_compose_sym2 |
|
698 |
|
699 lemma alpha_gen_compose_trans: |
|
700 fixes pi pia |
|
701 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)" |
|
702 and c: "(ab, ta) \<approx>gen R f pia (ac, sa)" |
|
703 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
704 shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)" |
|
705 using b c apply - |
|
706 apply(simp add: alphas) |
|
707 apply(erule conjE)+ |
|
708 apply(simp add: fresh_star_plus) |
|
709 apply(drule_tac x="- pia \<bullet> sa" in spec) |
|
710 apply(drule mp) |
|
711 apply(rotate_tac 5) |
|
712 apply(drule_tac pi="- pia" in a) |
|
713 apply(simp) |
|
714 apply(rotate_tac 7) |
|
715 apply(drule_tac pi="pia" in a) |
|
716 apply(simp) |
|
717 done |
|
718 |
|
719 lemma alpha_res_compose_trans: |
|
720 fixes pi pia |
|
721 assumes b: "(aa, t) \<approx>res (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)" |
|
722 and c: "(ab, ta) \<approx>res R f pia (ac, sa)" |
|
723 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
724 shows "(aa, t) \<approx>res R f (pia + pi) (ac, sa)" |
|
725 using b c apply - |
|
726 apply(simp add: alphas) |
|
727 apply(erule conjE)+ |
|
728 apply(simp add: fresh_star_plus) |
|
729 apply(drule_tac x="- pia \<bullet> sa" in spec) |
|
730 apply(drule mp) |
|
731 apply(drule_tac pi="- pia" in a) |
|
732 apply(simp) |
|
733 apply(rotate_tac 6) |
|
734 apply(drule_tac pi="pia" in a) |
|
735 apply(simp) |
|
736 done |
|
737 |
|
738 lemma alpha_lst_compose_trans: |
|
739 fixes pi pia |
|
740 assumes b: "(aa, t) \<approx>lst (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)" |
|
741 and c: "(ab, ta) \<approx>lst R f pia (ac, sa)" |
|
742 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
743 shows "(aa, t) \<approx>lst R f (pia + pi) (ac, sa)" |
|
744 using b c apply - |
|
745 apply(simp add: alphas) |
|
746 apply(erule conjE)+ |
|
747 apply(simp add: fresh_star_plus) |
|
748 apply(drule_tac x="- pia \<bullet> sa" in spec) |
|
749 apply(drule mp) |
|
750 apply(rotate_tac 5) |
|
751 apply(drule_tac pi="- pia" in a) |
|
752 apply(simp) |
|
753 apply(rotate_tac 7) |
|
754 apply(drule_tac pi="pia" in a) |
|
755 apply(simp) |
|
756 done |
|
757 |
|
758 lemmas alphas_compose_trans = alpha_gen_compose_trans alpha_res_compose_trans alpha_lst_compose_trans |
|
759 |
|
760 lemma alpha_gen_compose_trans2: |
|
761 fixes pi pia |
|
762 assumes b: "(aa, (t1, t2)) \<approx>gen |
|
763 (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z)) |
|
764 (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))" |
|
765 and c: "(ab, (ta1, ta2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a) |
|
766 pia (ac, (sa1, sa2))" |
|
767 and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)" |
|
768 and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)" |
|
769 shows "(aa, (t1, t2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a) |
|
770 (pia + pi) (ac, (sa1, sa2))" |
|
771 using b c apply - |
|
772 apply(simp add: alphas2) |
|
773 apply(simp add: alphas) |
|
774 apply(erule conjE)+ |
|
775 apply(simp add: fresh_star_plus) |
|
776 apply(drule_tac x="- pia \<bullet> sa1" in spec) |
|
777 apply(drule mp) |
|
778 apply(rotate_tac 5) |
|
779 apply(drule_tac pi="- pia" in r1) |
|
780 apply(simp) |
|
781 apply(rotate_tac -1) |
|
782 apply(drule_tac pi="pia" in r1) |
|
783 apply(simp) |
|
784 apply(drule_tac x="- pia \<bullet> sa2" in spec) |
|
785 apply(drule mp) |
|
786 apply(rotate_tac 6) |
|
787 apply(drule_tac pi="- pia" in r2) |
|
788 apply(simp) |
|
789 apply(rotate_tac -1) |
|
790 apply(drule_tac pi="pia" in r2) |
|
791 apply(simp) |
|
792 done |
|
793 |
|
794 lemma alpha_res_compose_trans2: |
|
795 fixes pi pia |
|
796 assumes b: "(aa, (t1, t2)) \<approx>res |
|
797 (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z)) |
|
798 (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))" |
|
799 and c: "(ab, (ta1, ta2)) \<approx>res (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a) |
|
800 pia (ac, (sa1, sa2))" |
|
801 and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)" |
|
802 and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)" |
|
803 shows "(aa, (t1, t2)) \<approx>res (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a) |
|
804 (pia + pi) (ac, (sa1, sa2))" |
|
805 using b c apply - |
|
806 apply(simp add: alphas2) |
|
807 apply(simp add: alphas) |
|
808 apply(erule conjE)+ |
|
809 apply(simp add: fresh_star_plus) |
|
810 apply(drule_tac x="- pia \<bullet> sa1" in spec) |
|
811 apply(drule mp) |
|
812 apply(rotate_tac 5) |
|
813 apply(drule_tac pi="- pia" in r1) |
|
814 apply(simp) |
|
815 apply(rotate_tac -1) |
|
816 apply(drule_tac pi="pia" in r1) |
|
817 apply(simp) |
|
818 apply(drule_tac x="- pia \<bullet> sa2" in spec) |
|
819 apply(drule mp) |
|
820 apply(rotate_tac 6) |
|
821 apply(drule_tac pi="- pia" in r2) |
|
822 apply(simp) |
|
823 apply(rotate_tac -1) |
|
824 apply(drule_tac pi="pia" in r2) |
|
825 apply(simp) |
|
826 done |
|
827 |
|
828 lemma alpha_lst_compose_trans2: |
|
829 fixes pi pia |
|
830 assumes b: "(aa, (t1, t2)) \<approx>lst |
|
831 (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z)) |
|
832 (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))" |
|
833 and c: "(ab, (ta1, ta2)) \<approx>lst (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a) |
|
834 pia (ac, (sa1, sa2))" |
|
835 and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)" |
|
836 and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)" |
|
837 shows "(aa, (t1, t2)) \<approx>lst (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a) |
|
838 (pia + pi) (ac, (sa1, sa2))" |
|
839 using b c apply - |
|
840 apply(simp add: alphas2) |
|
841 apply(simp add: alphas) |
|
842 apply(erule conjE)+ |
|
843 apply(simp add: fresh_star_plus) |
|
844 apply(drule_tac x="- pia \<bullet> sa1" in spec) |
|
845 apply(drule mp) |
|
846 apply(rotate_tac 5) |
|
847 apply(drule_tac pi="- pia" in r1) |
|
848 apply(simp) |
|
849 apply(rotate_tac -1) |
|
850 apply(drule_tac pi="pia" in r1) |
|
851 apply(simp) |
|
852 apply(drule_tac x="- pia \<bullet> sa2" in spec) |
|
853 apply(drule mp) |
|
854 apply(rotate_tac 6) |
|
855 apply(drule_tac pi="- pia" in r2) |
|
856 apply(simp) |
|
857 apply(rotate_tac -1) |
|
858 apply(drule_tac pi="pia" in r2) |
|
859 apply(simp) |
|
860 done |
|
861 |
|
862 lemmas alphas_compose_trans2 = alpha_gen_compose_trans2 alpha_res_compose_trans2 alpha_lst_compose_trans2 |
|
863 |
|
864 |
|
865 |
581 |
866 lemma alpha_gen_simpler: |
582 lemma alpha_gen_simpler: |
867 assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y" |
583 assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y" |
868 and fin_fv: "finite (f x)" |
584 and fin_fv: "finite (f x)" |
869 and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)" |
585 and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)" |