363 apply(simp) |
371 apply(simp) |
364 apply(simp only: disjoint_iff_not_equal) |
372 apply(simp only: disjoint_iff_not_equal) |
365 apply(simp) |
373 apply(simp) |
366 apply(metis permute_minus_cancel) |
374 apply(metis permute_minus_cancel) |
367 done |
375 done |
368 |
|
369 lemma alpha_abs_swap: |
|
370 assumes a1: "(supp x - bs) \<sharp>* p" |
|
371 and a2: "(supp x - bs) \<sharp>* p" |
|
372 shows "(bs, x) \<approx>abs (p \<bullet> bs, p \<bullet> x)" |
|
373 apply(simp) |
|
374 apply(rule_tac x="p" in exI) |
|
375 apply(simp add: alpha_gen) |
|
376 apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) |
|
377 apply(rule conjI) |
|
378 apply(rule sym) |
|
379 apply(rule qq) |
|
380 using a1 a2 |
|
381 apply(auto)[1] |
|
382 oops |
|
383 |
|
384 |
|
385 |
376 |
386 lemma |
377 lemma |
387 assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b" |
378 assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b" |
388 shows "({a}, x) \<approx>abs ({b}, y)" |
379 shows "({a}, x) \<approx>abs ({b}, y)" |
389 using a |
380 using a |
549 apply(induct F\<equiv>"supp p" arbitrary: p rule: finite_induct) |
540 apply(induct F\<equiv>"supp p" arbitrary: p rule: finite_induct) |
550 apply(simp add: supp_perm) |
541 apply(simp add: supp_perm) |
551 apply(drule perm_zero) |
542 apply(drule perm_zero) |
552 apply(simp add: zero) |
543 apply(simp add: zero) |
553 apply(rotate_tac 3) |
544 apply(rotate_tac 3) |
554 sorry |
545 oops |
555 |
|
556 |
|
557 (* |
|
558 lemma tt: |
546 lemma tt: |
559 "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x" |
547 "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x" |
560 apply(induct p rule: perm_induct_test) |
548 oops |
561 apply(simp) |
549 |
562 apply(rule swap_fresh_fresh) |
|
563 apply(case_tac "a \<in> supp x") |
|
564 apply(simp add: fresh_star_def) |
|
565 apply(drule_tac x="a" in bspec) |
|
566 apply(simp) |
|
567 apply(simp add: fresh_def) |
|
568 apply(simp add: supp_swap) |
|
569 apply(simp add: fresh_def) |
|
570 apply(case_tac "b \<in> supp x") |
|
571 apply(simp add: fresh_star_def) |
|
572 apply(drule_tac x="b" in bspec) |
|
573 apply(simp) |
|
574 apply(simp add: fresh_def) |
|
575 apply(simp add: supp_swap) |
|
576 apply(simp add: fresh_def) |
|
577 apply(simp) |
|
578 apply(drule meta_mp) |
|
579 apply(simp add: fresh_star_def fresh_def) |
|
580 apply(drule meta_mp) |
|
581 apply(simp add: fresh_star_def fresh_def) |
|
582 apply(simp) |
|
583 done |
|
584 *) |
|
585 lemma yy: |
550 lemma yy: |
586 assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2" |
551 assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2" |
587 shows "S1 = S2" |
552 shows "S1 = S2" |
588 using assms |
553 using assms |
589 apply (metis insert_Diff_single insert_absorb) |
554 apply (metis insert_Diff_single insert_absorb) |
590 done |
555 done |
591 |
556 |
|
557 lemma permute_boolI: |
|
558 fixes P::"bool" |
|
559 shows "p \<bullet> P \<Longrightarrow> P" |
|
560 apply(simp add: permute_bool_def) |
|
561 done |
|
562 |
|
563 lemma permute_boolE: |
|
564 fixes P::"bool" |
|
565 shows "P \<Longrightarrow> p \<bullet> P" |
|
566 apply(simp add: permute_bool_def) |
|
567 done |
|
568 |
|
569 lemma fresh_star_eqvt: |
|
570 shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)" |
|
571 apply(simp add: permute_bool_def) |
|
572 apply(auto simp add: fresh_star_def) |
|
573 apply(drule_tac x="(- p) \<bullet> xa" in bspec) |
|
574 apply(rule_tac p="p" in permute_boolI) |
|
575 apply(simp add: mem_eqvt) |
|
576 apply(rule_tac p="- p" in permute_boolI) |
|
577 apply(simp add: fresh_eqvt) |
|
578 apply(drule_tac x="p \<bullet> xa" in bspec) |
|
579 apply(rule_tac p="- p" in permute_boolI) |
|
580 apply(simp add: mem_eqvt) |
|
581 apply(rule_tac p="p" in permute_boolI) |
|
582 apply(simp add: fresh_eqvt) |
|
583 done |
|
584 |
|
585 lemma kk: |
|
586 assumes a: "p \<bullet> x = y" |
|
587 shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y" |
|
588 using a |
|
589 apply(auto) |
|
590 apply(rule_tac p="- p" in permute_boolI) |
|
591 apply(simp add: mem_eqvt supp_eqvt) |
|
592 done |
|
593 |
|
594 lemma ww: |
|
595 assumes "a \<notin> supp x" "b \<in> supp x" "a \<noteq> b" |
|
596 shows "((a \<rightleftharpoons> b) \<bullet> x) \<noteq> x" |
|
597 apply(subgoal_tac "(supp x) supports x") |
|
598 apply(simp add: supports_def) |
|
599 using assms |
|
600 apply - |
|
601 apply(drule_tac x="a" in spec) |
|
602 apply(simp) |
|
603 sorry |
|
604 |
592 |
605 |
593 lemma |
606 lemma |
594 assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" |
607 assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" |
595 shows "(a, x) \<approx>abs1 (b, y)" |
608 shows "(a, x) \<approx>abs1 (b, y)" |
596 using a |
609 using a |
597 apply(case_tac "a = b") |
610 apply(case_tac "a = b") |
598 apply(simp) |
611 apply(simp) |
|
612 apply(erule exE) |
|
613 apply(simp add: alpha_gen) |
|
614 apply(erule conjE)+ |
|
615 apply(case_tac "b \<notin> supp x \<and> b \<notin> supp y") |
|
616 apply(simp) |
|
617 apply(drule tt1) |
|
618 apply(clarify) |
|
619 apply(simp) |
|
620 apply(simp) |
|
621 apply(erule disjE) |
|
622 apply(case_tac "b \<in> supp y") |
|
623 apply(drule_tac yy) |
|
624 apply(simp) |
|
625 apply(simp) |
|
626 apply(simp) |
|
627 apply(case_tac "b \<sharp> p") |
|
628 apply(subgoal_tac "supp y \<sharp>* p") |
|
629 apply(drule tt1) |
|
630 apply(clarify) |
|
631 apply(drule sym) |
|
632 apply(drule sym) |
|
633 apply(simp) |
|
634 apply(auto simp add: fresh_star_def)[1] |
|
635 apply(frule_tac kk) |
|
636 apply(drule_tac x="b" in bspec) |
|
637 apply(simp) |
|
638 apply(simp add: fresh_def) |
|
639 apply(simp add: supp_perm) |
|
640 apply(subgoal_tac "((p \<bullet> b) \<sharp> p)") |
|
641 apply(simp add: fresh_def supp_perm) |
|
642 apply(simp add: fresh_star_def) |
|
643 apply(simp) |
|
644 apply(drule tt1) |
|
645 apply(clarify) |
|
646 apply(drule sym) |
|
647 apply(drule sym) |
|
648 apply(simp) |
|
649 apply(case_tac "b \<in> supp x") |
|
650 apply(drule_tac yy) |
|
651 apply(simp) |
|
652 apply(simp) |
|
653 apply(simp) |
|
654 apply(case_tac "b \<sharp> p") |
|
655 apply(subgoal_tac "supp y \<sharp>* p") |
|
656 apply(drule tt1) |
|
657 apply(clarify) |
|
658 apply(drule sym) |
|
659 apply(drule sym) |
|
660 apply(simp) |
|
661 apply(auto simp add: fresh_star_def)[1] |
|
662 apply(frule_tac kk) |
|
663 apply(drule_tac x="b" in bspec) |
|
664 apply(simp) |
|
665 apply(simp add: fresh_def) |
|
666 apply(simp add: supp_perm) |
|
667 apply(subgoal_tac "((p \<bullet> b) \<sharp> p)") |
|
668 apply(simp add: fresh_def supp_perm) |
|
669 apply(simp add: fresh_star_def) |
|
670 apply(simp) |
|
671 apply(drule sym) |
|
672 apply(drule sym) |
|
673 apply(subgoal_tac "supp x \<sharp>* p") |
|
674 apply(drule tt1) |
|
675 apply(clarify) |
|
676 apply(simp) |
|
677 apply(simp) |
|
678 apply(simp) |
|
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) |
599 oops |
697 oops |
600 |
698 |
601 |
699 |
602 fun |
700 fun |
603 distinct_perms |
701 distinct_perms |