449 apply(rule iffI) |
449 apply(rule iffI) |
450 apply(auto simp add: alphas_abs alpha_abs_lst_stronger1)[1] |
450 apply(auto simp add: alphas_abs alpha_abs_lst_stronger1)[1] |
451 apply(auto simp add: alphas_abs)[1] |
451 apply(auto simp add: alphas_abs)[1] |
452 done |
452 done |
453 |
453 |
|
454 lemma alpha_res_alpha_set: |
|
455 "(bs, x) \<approx>res op = supp p (cs, y) \<longleftrightarrow> (bs \<inter> supp x, x) \<approx>set op = supp p (cs \<inter> supp y, y)" |
|
456 using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast |
|
457 |
454 section {* Quotient types *} |
458 section {* Quotient types *} |
455 |
459 |
456 quotient_type |
460 quotient_type |
457 'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set" |
461 'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set" |
458 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res" |
462 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res" |
495 and "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute" |
499 and "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute" |
496 unfolding fun_rel_def |
500 unfolding fun_rel_def |
497 by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt) |
501 by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt) |
498 |
502 |
499 lemma Abs_eq_iff: |
503 lemma Abs_eq_iff: |
500 shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y))" |
504 shows "[bs]set. x = [bs']set. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (bs', y))" |
501 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
505 and "[bs]res. x = [bs']res. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (bs', y))" |
502 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
506 and "[cs]lst. x = [cs']lst. y \<longleftrightarrow> (\<exists>p. (cs, x) \<approx>lst (op =) supp p (cs', y))" |
503 by (lifting alphas_abs) |
507 by (lifting alphas_abs) |
504 |
508 |
505 lemma Abs_eq_iff2: |
509 lemma Abs_eq_iff2: |
506 shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y) \<and> supp p \<subseteq> bs \<union> cs)" |
510 shows "[bs]set. x = [bs']set. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op=) supp p (bs', y) \<and> supp p \<subseteq> bs \<union> bs')" |
507 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y) \<and> supp p \<subseteq> bs \<union> cs)" |
511 and "[bs]res. x = [bs']res. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (bs', y) \<and> supp p \<subseteq> bs \<union> bs')" |
508 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> |
512 and "[cs]lst. x = [cs']lst. y \<longleftrightarrow> (\<exists>p. (cs, x) \<approx>lst (op=) supp p (cs', y) \<and> supp p \<subseteq> set cs \<union> set cs')" |
509 (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y) \<and> supp p \<subseteq> set bsl \<union> set csl)" |
|
510 by (lifting alphas_abs_stronger) |
513 by (lifting alphas_abs_stronger) |
511 |
514 |
512 lemma alpha_res_alpha_set: |
|
513 "(bs, x) \<approx>res op = supp p (cs, y) \<longleftrightarrow> (bs \<inter> supp x, x) \<approx>set op = supp p (cs \<inter> supp y, y)" |
|
514 using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast |
|
515 |
515 |
516 lemma Abs_eq_res_set: |
516 lemma Abs_eq_res_set: |
517 "(([bs]res. x) = ([cs]res. y)) = (([(bs \<inter> supp x)]set. x) = ([(cs \<inter> supp y)]set. y))" |
517 shows "[bs]res. x = [cs]res. y \<longleftrightarrow> [bs \<inter> supp x]set. x = [cs \<inter> supp y]set. y" |
518 unfolding Abs_eq_iff alpha_res_alpha_set by rule |
518 unfolding Abs_eq_iff alpha_res_alpha_set by rule |
519 |
519 |
520 lemma Abs_eq_res_supp: |
520 lemma Abs_eq_res_supp: |
521 assumes asm: "supp x \<subseteq> bs" |
521 assumes asm: "supp x \<subseteq> bs" |
522 shows "([as]res. x) = ([as \<inter> bs]res. x)" |
522 shows "[as]res. x = [as \<inter> bs]res. x" |
523 unfolding Abs_eq_iff alphas |
523 unfolding Abs_eq_iff alphas |
524 apply (rule_tac x="0::perm" in exI) |
524 apply (rule_tac x="0::perm" in exI) |
525 apply (simp add: fresh_star_zero) |
525 apply (simp add: fresh_star_zero) |
526 using asm by blast |
526 using asm by blast |
527 |
527 |
528 lemma Abs_exhausts: |
528 lemma Abs_exhausts: |
529 shows "(\<And>as (x::'a::pt). y1 = Abs_set as x \<Longrightarrow> P1) \<Longrightarrow> P1" |
529 shows "(\<And>as (x::'a::pt). y1 = [as]set. x \<Longrightarrow> P1) \<Longrightarrow> P1" |
530 and "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2" |
530 and "(\<And>as (x::'a::pt). y2 = [as]res. x \<Longrightarrow> P2) \<Longrightarrow> P2" |
531 and "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3" |
531 and "(\<And>bs (x::'a::pt). y3 = [bs]lst. x \<Longrightarrow> P3) \<Longrightarrow> P3" |
532 by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"] |
532 by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"] |
533 prod.exhaust[where 'a="atom set" and 'b="'a"] |
533 prod.exhaust[where 'a="atom set" and 'b="'a"] |
534 prod.exhaust[where 'a="atom list" and 'b="'a"]) |
534 prod.exhaust[where 'a="atom list" and 'b="'a"]) |
535 |
535 |
536 |
536 |
601 |
601 |
602 |
602 |
603 lemma Abs_swap1: |
603 lemma Abs_swap1: |
604 assumes a1: "a \<notin> (supp x) - bs" |
604 assumes a1: "a \<notin> (supp x) - bs" |
605 and a2: "b \<notin> (supp x) - bs" |
605 and a2: "b \<notin> (supp x) - bs" |
606 shows "Abs_set bs x = Abs_set ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
606 shows "[bs]set. x = [(a \<rightleftharpoons> b) \<bullet> bs]set. ((a \<rightleftharpoons> b) \<bullet> x)" |
607 and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
607 and "[bs]res. x = [(a \<rightleftharpoons> b) \<bullet> bs]res. ((a \<rightleftharpoons> b) \<bullet> x)" |
608 unfolding Abs_eq_iff |
608 unfolding Abs_eq_iff |
609 unfolding alphas |
609 unfolding alphas |
610 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] |
610 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] |
611 unfolding fresh_star_def fresh_def |
611 unfolding fresh_star_def fresh_def |
612 unfolding swap_set_not_in[OF a1 a2] |
612 unfolding swap_set_not_in[OF a1 a2] |
615 (auto simp add: supp_perm swap_atom) |
615 (auto simp add: supp_perm swap_atom) |
616 |
616 |
617 lemma Abs_swap2: |
617 lemma Abs_swap2: |
618 assumes a1: "a \<notin> (supp x) - (set bs)" |
618 assumes a1: "a \<notin> (supp x) - (set bs)" |
619 and a2: "b \<notin> (supp x) - (set bs)" |
619 and a2: "b \<notin> (supp x) - (set bs)" |
620 shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
620 shows "[bs]lst. x = [(a \<rightleftharpoons> b) \<bullet> bs]lst. ((a \<rightleftharpoons> b) \<bullet> x)" |
621 unfolding Abs_eq_iff |
621 unfolding Abs_eq_iff |
622 unfolding alphas |
622 unfolding alphas |
623 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric] |
623 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric] |
624 unfolding fresh_star_def fresh_def |
624 unfolding fresh_star_def fresh_def |
625 unfolding swap_set_not_in[OF a1 a2] |
625 unfolding swap_set_not_in[OF a1 a2] |
626 using a1 a2 |
626 using a1 a2 |
627 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI) |
627 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI) |
628 (auto simp add: supp_perm swap_atom) |
628 (auto simp add: supp_perm swap_atom) |
629 |
629 |
630 lemma Abs_supports: |
630 lemma Abs_supports: |
631 shows "((supp x) - as) supports (Abs_set as x)" |
631 shows "((supp x) - as) supports ([as]set. x)" |
632 and "((supp x) - as) supports (Abs_res as x)" |
632 and "((supp x) - as) supports ([as]res. x)" |
633 and "((supp x) - set bs) supports (Abs_lst bs x)" |
633 and "((supp x) - set bs) supports ([bs]lst. x)" |
634 unfolding supports_def |
634 unfolding supports_def |
635 unfolding permute_Abs |
635 unfolding permute_Abs |
636 by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric]) |
636 by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric]) |
637 |
637 |
638 function |
638 function |
639 supp_set :: "('a::pt) abs_set \<Rightarrow> atom set" |
639 supp_set :: "('a::pt) abs_set \<Rightarrow> atom set" |
640 where |
640 where |
641 "supp_set (Abs_set as x) = supp x - as" |
641 "supp_set ([as]set. x) = supp x - as" |
642 apply(case_tac x rule: Abs_exhausts(1)) |
642 apply(case_tac x rule: Abs_exhausts(1)) |
643 apply(simp) |
643 apply(simp) |
644 apply(simp add: Abs_eq_iff alphas_abs alphas) |
644 apply(simp add: Abs_eq_iff alphas_abs alphas) |
645 done |
645 done |
646 |
646 |
647 termination supp_set |
647 termination supp_set |
648 by (auto intro!: local.termination) |
648 by lexicographic_order |
649 |
649 |
650 function |
650 function |
651 supp_res :: "('a::pt) abs_res \<Rightarrow> atom set" |
651 supp_res :: "('a::pt) abs_res \<Rightarrow> atom set" |
652 where |
652 where |
653 "supp_res (Abs_res as x) = supp x - as" |
653 "supp_res ([as]res. x) = supp x - as" |
654 apply(case_tac x rule: Abs_exhausts(2)) |
654 apply(case_tac x rule: Abs_exhausts(2)) |
655 apply(simp) |
655 apply(simp) |
656 apply(simp add: Abs_eq_iff alphas_abs alphas) |
656 apply(simp add: Abs_eq_iff alphas_abs alphas) |
657 done |
657 done |
658 |
658 |
659 termination supp_res |
659 termination supp_res |
660 by (auto intro!: local.termination) |
660 by lexicographic_order |
661 |
661 |
662 function |
662 function |
663 supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set" |
663 supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set" |
664 where |
664 where |
665 "supp_lst (Abs_lst cs x) = (supp x) - (set cs)" |
665 "supp_lst (Abs_lst cs x) = (supp x) - (set cs)" |
666 apply(case_tac x rule: Abs_exhausts(3)) |
666 apply(case_tac x rule: Abs_exhausts(3)) |
667 apply(simp) |
667 apply(simp) |
668 apply(simp add: Abs_eq_iff alphas_abs alphas) |
668 apply(simp add: Abs_eq_iff alphas_abs alphas) |
669 done |
669 done |
670 |
670 |
671 termination supp_lst |
671 termination supp_lst |
672 by (auto intro!: local.termination) |
672 by lexicographic_order |
673 |
673 |
674 lemma supp_funs_eqvt[eqvt]: |
674 lemma supp_funs_eqvt[eqvt]: |
675 shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)" |
675 shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)" |
676 and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)" |
676 and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)" |
677 and "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)" |
677 and "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)" |
682 apply(case_tac z rule: Abs_exhausts(3)) |
682 apply(case_tac z rule: Abs_exhausts(3)) |
683 apply(simp add: supp_eqvt Diff_eqvt set_eqvt) |
683 apply(simp add: supp_eqvt Diff_eqvt set_eqvt) |
684 done |
684 done |
685 |
685 |
686 lemma Abs_fresh_aux: |
686 lemma Abs_fresh_aux: |
687 shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_set (Abs bs x)" |
687 shows "a \<sharp> [bs]set. x \<Longrightarrow> a \<sharp> supp_set ([bs]set. x)" |
688 and "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)" |
688 and "a \<sharp> [bs]res. x \<Longrightarrow> a \<sharp> supp_res ([bs]res. x)" |
689 and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)" |
689 and "a \<sharp> [cs]lst. x \<Longrightarrow> a \<sharp> supp_lst ([cs]lst. x)" |
690 by (rule_tac [!] fresh_fun_eqvt_app) |
690 by (rule_tac [!] fresh_fun_eqvt_app) |
691 (auto simp only: eqvt_def eqvts_raw) |
691 (auto simp only: eqvt_def eqvts_raw) |
692 |
692 |
693 lemma Abs_supp_subset1: |
693 lemma Abs_supp_subset1: |
694 assumes a: "finite (supp x)" |
694 assumes a: "finite (supp x)" |
695 shows "(supp x) - as \<subseteq> supp (Abs_set as x)" |
695 shows "(supp x) - as \<subseteq> supp ([as]set. x)" |
696 and "(supp x) - as \<subseteq> supp (Abs_res as x)" |
696 and "(supp x) - as \<subseteq> supp ([as]res. x)" |
697 and "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)" |
697 and "(supp x) - (set bs) \<subseteq> supp ([bs]lst. x)" |
698 unfolding supp_conv_fresh |
698 unfolding supp_conv_fresh |
699 by (auto dest!: Abs_fresh_aux) |
699 by (auto dest!: Abs_fresh_aux) |
700 (simp_all add: fresh_def supp_finite_atom_set a) |
700 (simp_all add: fresh_def supp_finite_atom_set a) |
701 |
701 |
702 lemma Abs_supp_subset2: |
702 lemma Abs_supp_subset2: |
703 assumes a: "finite (supp x)" |
703 assumes a: "finite (supp x)" |
704 shows "supp (Abs_set as x) \<subseteq> (supp x) - as" |
704 shows "supp ([as]set. x) \<subseteq> (supp x) - as" |
705 and "supp (Abs_res as x) \<subseteq> (supp x) - as" |
705 and "supp ([as]res. x) \<subseteq> (supp x) - as" |
706 and "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)" |
706 and "supp ([bs]lst. x) \<subseteq> (supp x) - (set bs)" |
707 by (rule_tac [!] supp_is_subset) |
707 by (rule_tac [!] supp_is_subset) |
708 (simp_all add: Abs_supports a) |
708 (simp_all add: Abs_supports a) |
709 |
709 |
710 lemma Abs_finite_supp: |
710 lemma Abs_finite_supp: |
711 assumes a: "finite (supp x)" |
711 assumes a: "finite (supp x)" |
712 shows "supp (Abs_set as x) = (supp x) - as" |
712 shows "supp ([as]set. x) = (supp x) - as" |
713 and "supp (Abs_res as x) = (supp x) - as" |
713 and "supp ([as]res. x) = (supp x) - as" |
714 and "supp (Abs_lst bs x) = (supp x) - (set bs)" |
714 and "supp ([bs]lst. x) = (supp x) - (set bs)" |
715 by (rule_tac [!] subset_antisym) |
715 using Abs_supp_subset1[OF a] Abs_supp_subset2[OF a] |
716 (simp_all add: Abs_supp_subset1[OF a] Abs_supp_subset2[OF a]) |
716 by blast+ |
717 |
717 |
718 lemma supp_Abs: |
718 lemma supp_Abs: |
719 fixes x::"'a::fs" |
719 fixes x::"'a::fs" |
720 shows "supp (Abs_set as x) = (supp x) - as" |
720 shows "supp ([as]set. x) = (supp x) - as" |
721 and "supp (Abs_res as x) = (supp x) - as" |
721 and "supp ([as]res. x) = (supp x) - as" |
722 and "supp (Abs_lst bs x) = (supp x) - (set bs)" |
722 and "supp ([bs]lst. x) = (supp x) - (set bs)" |
723 by (rule_tac [!] Abs_finite_supp) |
723 by (simp_all add: Abs_finite_supp finite_supp) |
724 (simp_all add: finite_supp) |
|
725 |
724 |
726 instance abs_set :: (fs) fs |
725 instance abs_set :: (fs) fs |
727 apply(default) |
726 apply(default) |
728 apply(case_tac x rule: Abs_exhausts(1)) |
727 apply(case_tac x rule: Abs_exhausts(1)) |
729 apply(simp add: supp_Abs finite_supp) |
728 apply(simp add: supp_Abs finite_supp) |
741 apply(simp add: supp_Abs finite_supp) |
740 apply(simp add: supp_Abs finite_supp) |
742 done |
741 done |
743 |
742 |
744 lemma Abs_fresh_iff: |
743 lemma Abs_fresh_iff: |
745 fixes x::"'a::fs" |
744 fixes x::"'a::fs" |
746 shows "a \<sharp> Abs_set bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)" |
745 shows "a \<sharp> [bs]set. x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)" |
747 and "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)" |
746 and "a \<sharp> [bs]res. x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)" |
748 and "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)" |
747 and "a \<sharp> [cs]lst. x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)" |
749 unfolding fresh_def |
748 unfolding fresh_def |
750 unfolding supp_Abs |
749 unfolding supp_Abs |
751 by auto |
750 by auto |
752 |
751 |
753 lemma Abs_fresh_star_iff: |
752 lemma Abs_fresh_star_iff: |
754 fixes x::"'a::fs" |
753 fixes x::"'a::fs" |
755 shows "as \<sharp>* Abs_set bs x \<longleftrightarrow> (as - bs) \<sharp>* x" |
754 shows "as \<sharp>* ([bs]set. x) \<longleftrightarrow> (as - bs) \<sharp>* x" |
756 and "as \<sharp>* Abs_res bs x \<longleftrightarrow> (as - bs) \<sharp>* x" |
755 and "as \<sharp>* ([bs]res. x) \<longleftrightarrow> (as - bs) \<sharp>* x" |
757 and "as \<sharp>* Abs_lst cs x \<longleftrightarrow> (as - set cs) \<sharp>* x" |
756 and "as \<sharp>* ([cs]lst. x) \<longleftrightarrow> (as - set cs) \<sharp>* x" |
758 unfolding fresh_star_def |
757 unfolding fresh_star_def |
759 by (auto simp add: Abs_fresh_iff) |
758 by (auto simp add: Abs_fresh_iff) |
760 |
759 |
761 lemma Abs_fresh_star: |
760 lemma Abs_fresh_star: |
762 fixes x::"'a::fs" |
761 fixes x::"'a::fs" |
763 shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_set as' x" |
762 shows "as \<subseteq> as' \<Longrightarrow> as \<sharp>* ([as']set. x)" |
764 and "as \<subseteq> as' \<Longrightarrow> as \<sharp>* Abs_res as' x" |
763 and "as \<subseteq> as' \<Longrightarrow> as \<sharp>* ([as']res. x)" |
765 and "bs \<subseteq> set bs' \<Longrightarrow> bs \<sharp>* Abs_lst bs' x" |
764 and "bs \<subseteq> set bs' \<Longrightarrow> bs \<sharp>* ([bs']lst. x)" |
766 unfolding fresh_star_def |
765 unfolding fresh_star_def |
767 by(auto simp add: Abs_fresh_iff) |
766 by(auto simp add: Abs_fresh_iff) |
768 |
767 |
769 lemma Abs_fresh_star2: |
768 lemma Abs_fresh_star2: |
770 fixes x::"'a::fs" |
769 fixes x::"'a::fs" |
771 shows "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* Abs_set bs x \<longleftrightarrow> as \<sharp>* x" |
770 shows "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* ([bs]set. x) \<longleftrightarrow> as \<sharp>* x" |
772 and "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* Abs_res bs x \<longleftrightarrow> as \<sharp>* x" |
771 and "as \<inter> bs = {} \<Longrightarrow> as \<sharp>* ([bs]res. x) \<longleftrightarrow> as \<sharp>* x" |
773 and "cs \<inter> set ds = {} \<Longrightarrow> cs \<sharp>* Abs_lst ds x \<longleftrightarrow> cs \<sharp>* x" |
772 and "cs \<inter> set ds = {} \<Longrightarrow> cs \<sharp>* ([ds]lst. x) \<longleftrightarrow> cs \<sharp>* x" |
774 unfolding fresh_star_def Abs_fresh_iff |
773 unfolding fresh_star_def Abs_fresh_iff |
775 by auto |
774 by auto |
776 |
775 |
|
776 |
|
777 section {* Abstractions of single atoms *} |
777 |
778 |
778 lemma Abs1_eq: |
779 lemma Abs1_eq: |
779 fixes x::"'a::fs" |
780 fixes x::"'a::fs" |
780 shows "Abs_set {a} x = Abs_set {a} y \<longleftrightarrow> x = y" |
781 shows "Abs_set {a} x = Abs_set {a} y \<longleftrightarrow> x = y" |
781 and "Abs_res {a} x = Abs_res {a} y \<longleftrightarrow> x = y" |
782 and "Abs_res {a} x = Abs_res {a} y \<longleftrightarrow> x = y" |
884 fixes x::"'a::fs" |
885 fixes x::"'a::fs" |
885 assumes a: "(p \<bullet> bs) \<sharp>* x" |
886 assumes a: "(p \<bullet> bs) \<sharp>* x" |
886 and b: "finite bs" |
887 and b: "finite bs" |
887 shows "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
888 shows "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
888 proof - |
889 proof - |
889 from b set_renaming_perm |
890 from set_renaming_perm2 |
890 obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast |
891 obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast |
891 have ***: "q \<bullet> bs = p \<bullet> bs" using b * by (induct) (simp add: permute_set_eq, simp add: insert_eqvt) |
892 have ***: "q \<bullet> bs = p \<bullet> bs" using b * by (induct) (simp add: permute_set_eq, simp add: insert_eqvt) |
892 have "[bs]set. x = q \<bullet> ([bs]set. x)" |
893 have "[bs]set. x = q \<bullet> ([bs]set. x)" |
893 apply(rule perm_supp_eq[symmetric]) |
894 apply(rule perm_supp_eq[symmetric]) |
894 using a ** |
895 using a ** |
904 fixes x::"'a::fs" |
905 fixes x::"'a::fs" |
905 assumes a: "(p \<bullet> bs) \<sharp>* x" |
906 assumes a: "(p \<bullet> bs) \<sharp>* x" |
906 and b: "finite bs" |
907 and b: "finite bs" |
907 shows "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
908 shows "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
908 proof - |
909 proof - |
909 from b set_renaming_perm |
910 from set_renaming_perm2 |
910 obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast |
911 obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast |
911 have ***: "q \<bullet> bs = p \<bullet> bs" using b * by (induct) (simp add: permute_set_eq, simp add: insert_eqvt) |
912 have ***: "q \<bullet> bs = p \<bullet> bs" using b * by (induct) (simp add: permute_set_eq, simp add: insert_eqvt) |
912 have "[bs]res. x = q \<bullet> ([bs]res. x)" |
913 have "[bs]res. x = q \<bullet> ([bs]res. x)" |
913 apply(rule perm_supp_eq[symmetric]) |
914 apply(rule perm_supp_eq[symmetric]) |
914 using a ** |
915 using a ** |
923 lemma Abs_rename_lst: |
924 lemma Abs_rename_lst: |
924 fixes x::"'a::fs" |
925 fixes x::"'a::fs" |
925 assumes a: "(p \<bullet> (set bs)) \<sharp>* x" |
926 assumes a: "(p \<bullet> (set bs)) \<sharp>* x" |
926 shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
927 shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
927 proof - |
928 proof - |
928 from a list_renaming_perm |
929 from list_renaming_perm |
929 obtain q where *: "\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by blast |
930 obtain q where *: "\<forall>b \<in> set bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by blast |
930 have ***: "q \<bullet> bs = p \<bullet> bs" using * by (induct bs) (simp_all add: insert_eqvt) |
931 have ***: "q \<bullet> bs = p \<bullet> bs" using * by (induct bs) (simp_all add: insert_eqvt) |
931 have "[bs]lst. x = q \<bullet> ([bs]lst. x)" |
932 have "[bs]lst. x = q \<bullet> ([bs]lst. x)" |
932 apply(rule perm_supp_eq[symmetric]) |
933 apply(rule perm_supp_eq[symmetric]) |
933 using a ** |
934 using a ** |