590 apply(rule_tac p="- p" in permute_boolI) |
590 apply(rule_tac p="- p" in permute_boolI) |
591 apply(simp add: mem_eqvt supp_eqvt) |
591 apply(simp add: mem_eqvt supp_eqvt) |
592 done |
592 done |
593 |
593 |
594 lemma ww: |
594 lemma ww: |
595 assumes "a \<notin> supp x" "b \<in> supp x" "a \<noteq> b" |
595 assumes "a \<notin> supp x" "b \<in> supp x" "a \<noteq> b" "sort_of a = sort_of b" |
596 shows "((a \<rightleftharpoons> b) \<bullet> x) \<noteq> x" |
596 shows "((a \<rightleftharpoons> b) \<bullet> x) \<noteq> x" |
597 apply(subgoal_tac "(supp x) supports x") |
597 apply(subgoal_tac "(supp x) supports x") |
598 apply(simp add: supports_def) |
598 apply(simp add: supports_def) |
599 using assms |
599 using assms |
600 apply - |
600 apply - |
601 apply(drule_tac x="a" in spec) |
601 apply(drule_tac x="a" in spec) |
602 apply(simp) |
602 defer |
603 sorry |
603 apply(rule supp_supports) |
604 |
604 apply(auto) |
605 |
605 apply(rotate_tac 1) |
606 lemma |
606 apply(drule_tac p="(a \<rightleftharpoons> b)" in permute_boolE) |
607 assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" |
607 apply(simp add: mem_eqvt supp_eqvt) |
608 shows "(a, x) \<approx>abs1 (b, y)" |
608 done |
|
609 |
|
610 lemma zz: |
|
611 assumes "p \<bullet> x \<noteq> p \<bullet> y" |
|
612 shows "x \<noteq> y" |
|
613 using assms |
|
614 apply(auto) |
|
615 done |
|
616 |
|
617 lemma alpha_abs_sym: |
|
618 assumes a: "({a}, x) \<approx>abs ({b}, y)" |
|
619 shows "({b}, y) \<approx>abs ({a}, x)" |
609 using a |
620 using a |
610 apply(case_tac "a = b") |
621 apply(simp) |
|
622 apply(erule exE) |
|
623 apply(rule_tac x="- p" in exI) |
|
624 apply(simp add: alpha_gen) |
|
625 apply(simp add: fresh_star_def fresh_minus_perm) |
|
626 apply (metis permute_minus_cancel(2)) |
|
627 done |
|
628 |
|
629 lemma alpha_abs_trans: |
|
630 assumes a: "({a1}, x1) \<approx>abs ({a2}, x2)" |
|
631 assumes b: "({a2}, x2) \<approx>abs ({a3}, x3)" |
|
632 shows "({a1}, x1) \<approx>abs ({a3}, x3)" |
|
633 using a b |
|
634 apply(simp) |
|
635 apply(erule exE)+ |
|
636 apply(rule_tac x="pa + p" in exI) |
|
637 apply(simp add: alpha_gen) |
|
638 apply(simp add: fresh_star_def fresh_plus_perm) |
|
639 done |
|
640 |
|
641 lemma alpha_equal: |
|
642 assumes a: "({a}, x) \<approx>abs ({a}, y)" |
|
643 shows "(a, x) \<approx>abs1 (a, y)" |
|
644 using a |
611 apply(simp) |
645 apply(simp) |
612 apply(erule exE) |
646 apply(erule exE) |
613 apply(simp add: alpha_gen) |
647 apply(simp add: alpha_gen) |
614 apply(erule conjE)+ |
648 apply(erule conjE)+ |
615 apply(case_tac "b \<notin> supp x \<and> b \<notin> supp y") |
649 apply(case_tac "a \<notin> supp x") |
|
650 apply(simp) |
|
651 apply(subgoal_tac "supp x \<sharp>* p") |
|
652 apply(drule tt1) |
|
653 apply(simp) |
|
654 apply(simp) |
|
655 apply(simp) |
|
656 apply(case_tac "a \<notin> supp y") |
616 apply(simp) |
657 apply(simp) |
617 apply(drule tt1) |
658 apply(drule tt1) |
618 apply(clarify) |
659 apply(clarify) |
619 apply(simp) |
660 apply(simp (no_asm_use)) |
620 apply(simp) |
661 apply(simp) |
621 apply(erule disjE) |
662 apply(simp) |
622 apply(case_tac "b \<in> supp y") |
663 apply(drule yy) |
623 apply(drule_tac yy) |
664 apply(simp) |
624 apply(simp) |
665 apply(simp) |
625 apply(simp) |
666 apply(simp) |
626 apply(simp) |
667 apply(case_tac "a \<sharp> p") |
627 apply(case_tac "b \<sharp> p") |
|
628 apply(subgoal_tac "supp y \<sharp>* p") |
668 apply(subgoal_tac "supp y \<sharp>* p") |
629 apply(drule tt1) |
669 apply(drule tt1) |
630 apply(clarify) |
670 apply(clarify) |
631 apply(drule sym) |
671 apply(simp (no_asm_use)) |
632 apply(drule sym) |
672 apply(metis) |
633 apply(simp) |
|
634 apply(auto simp add: fresh_star_def)[1] |
673 apply(auto simp add: fresh_star_def)[1] |
635 apply(frule_tac kk) |
674 apply(frule_tac kk) |
636 apply(drule_tac x="b" in bspec) |
675 apply(drule_tac x="a" in bspec) |
637 apply(simp) |
676 apply(simp) |
638 apply(simp add: fresh_def) |
677 apply(simp add: fresh_def) |
639 apply(simp add: supp_perm) |
678 apply(simp add: supp_perm) |
640 apply(subgoal_tac "((p \<bullet> b) \<sharp> p)") |
679 apply(subgoal_tac "((p \<bullet> a) \<sharp> p)") |
641 apply(simp add: fresh_def supp_perm) |
680 apply(simp add: fresh_def supp_perm) |
642 apply(simp add: fresh_star_def) |
681 apply(simp add: fresh_star_def) |
643 apply(simp) |
682 done |
644 apply(drule tt1) |
683 |
645 apply(clarify) |
684 lemma alpha_unequal: |
646 apply(drule sym) |
685 assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" "a \<noteq> b" |
647 apply(drule sym) |
686 shows "(a, x) \<approx>abs1 (b, y)" |
648 apply(simp) |
687 using a |
649 apply(case_tac "b \<in> supp x") |
688 apply - |
650 apply(drule_tac yy) |
689 apply(subgoal_tac "a \<notin> supp x - {a}") |
651 apply(simp) |
690 apply(subgoal_tac "b \<notin> supp x - {a}") |
652 apply(simp) |
691 defer |
653 apply(simp) |
692 apply(simp add: alpha_gen) |
654 apply(case_tac "b \<sharp> p") |
693 apply(simp) |
655 apply(subgoal_tac "supp y \<sharp>* p") |
694 apply(drule_tac alpha_abs_swap) |
656 apply(drule tt1) |
695 apply(assumption) |
657 apply(clarify) |
696 apply(simp only: insert_eqvt empty_eqvt swap_atom_simps) |
658 apply(drule sym) |
697 apply(drule alpha_abs_sym) |
659 apply(drule sym) |
698 apply(rotate_tac 4) |
660 apply(simp) |
699 apply(drule_tac alpha_abs_trans) |
661 apply(auto simp add: fresh_star_def)[1] |
700 apply(assumption) |
662 apply(frule_tac kk) |
701 apply(drule alpha_equal) |
663 apply(drule_tac x="b" in bspec) |
702 apply(simp) |
664 apply(simp) |
703 apply(rule_tac p="(a \<rightleftharpoons> b)" in permute_boolI) |
|
704 apply(simp add: fresh_eqvt) |
665 apply(simp add: fresh_def) |
705 apply(simp add: fresh_def) |
666 apply(simp add: supp_perm) |
706 done |
667 apply(subgoal_tac "((p \<bullet> b) \<sharp> p)") |
707 |
668 apply(simp add: fresh_def supp_perm) |
708 lemma alpha_new_old: |
669 apply(simp add: fresh_star_def) |
709 assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" |
670 apply(simp) |
710 shows "(a, x) \<approx>abs1 (b, y)" |
671 apply(drule sym) |
711 using a |
672 apply(drule sym) |
712 apply(case_tac "a=b") |
673 apply(subgoal_tac "supp x \<sharp>* p") |
713 apply(simp only: alpha_equal) |
674 apply(drule tt1) |
714 apply(drule alpha_unequal) |
675 apply(clarify) |
715 apply(simp) |
676 apply(simp) |
716 apply(simp) |
677 apply(simp) |
717 apply(simp) |
678 apply(simp) |
718 done |
679 apply(erule exE) |
|
680 apply(simp add: alpha_gen) |
|
681 apply(erule conjE)+ |
|
682 apply(simp add: fresh_def) |
|
683 apply(rule conjI) |
|
684 defer |
|
685 apply(clarify) |
|
686 apply(subgoal_tac "a=b") |
|
687 prefer 2 |
|
688 apply(blast) |
|
689 apply(simp) |
|
690 apply(clarify) |
|
691 apply(subgoal_tac "b \<notin> supp x") |
|
692 prefer 2 |
|
693 apply(blast) |
|
694 apply(subgoal_tac "a \<notin> supp (p \<bullet> x)") |
|
695 prefer 2 |
|
696 apply(blast) |
|
697 oops |
|
698 |
|
699 |
719 |
700 fun |
720 fun |
701 distinct_perms |
721 distinct_perms |
702 where |
722 where |
703 "distinct_perms [] = True" |
723 "distinct_perms [] = True" |