543 subsection {* Renaming of bodies of abstractions *} |
543 subsection {* Renaming of bodies of abstractions *} |
544 |
544 |
545 |
545 |
546 lemma Abs_rename_set: |
546 lemma Abs_rename_set: |
547 fixes x::"'a::fs" |
547 fixes x::"'a::fs" |
548 assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" |
548 assumes a: "(p \<bullet> bs) \<sharp>* x" |
549 and b: "finite bs" |
549 and b: "finite bs" |
550 shows "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
550 shows "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
551 proof - |
551 proof - |
552 from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair) |
552 from b set_renaming_perm |
553 with set_renaming_perm |
553 obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast |
554 obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis |
|
555 have "[bs]set. x = q \<bullet> ([bs]set. x)" |
554 have "[bs]set. x = q \<bullet> ([bs]set. x)" |
556 apply(rule perm_supp_eq[symmetric]) |
555 apply(rule perm_supp_eq[symmetric]) |
557 using a ** |
556 using a ** |
558 unfolding fresh_star_Pair |
|
559 unfolding Abs_fresh_star_iff |
557 unfolding Abs_fresh_star_iff |
560 unfolding fresh_star_def |
558 unfolding fresh_star_def |
561 by auto |
559 by auto |
562 also have "\<dots> = [q \<bullet> bs]set. (q \<bullet> x)" by simp |
560 also have "\<dots> = [q \<bullet> bs]set. (q \<bullet> x)" by simp |
563 finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" by (simp add: *) |
561 finally have "[bs]set. x = [p \<bullet> bs]set. (q \<bullet> x)" by (simp add: *) |
564 then show "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using * by metis |
562 then show "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using * by metis |
565 qed |
563 qed |
566 |
564 |
567 lemma Abs_rename_res: |
565 lemma Abs_rename_res: |
568 fixes x::"'a::fs" |
566 fixes x::"'a::fs" |
569 assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" |
567 assumes a: "(p \<bullet> bs) \<sharp>* x" |
570 and b: "finite bs" |
568 and b: "finite bs" |
571 shows "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
569 shows "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
572 proof - |
570 proof - |
573 from a b have "p \<bullet> bs \<inter> bs = {}" using at_fresh_star_inter by (simp add: fresh_star_Pair) |
571 from b set_renaming_perm |
574 with set_renaming_perm |
572 obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast |
575 obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" using b by metis |
|
576 have "[bs]res. x = q \<bullet> ([bs]res. x)" |
573 have "[bs]res. x = q \<bullet> ([bs]res. x)" |
577 apply(rule perm_supp_eq[symmetric]) |
574 apply(rule perm_supp_eq[symmetric]) |
578 using a ** |
575 using a ** |
579 unfolding fresh_star_Pair |
|
580 unfolding Abs_fresh_star_iff |
576 unfolding Abs_fresh_star_iff |
581 unfolding fresh_star_def |
577 unfolding fresh_star_def |
582 by auto |
578 by auto |
583 also have "\<dots> = [q \<bullet> bs]res. (q \<bullet> x)" by simp |
579 also have "\<dots> = [q \<bullet> bs]res. (q \<bullet> x)" by simp |
584 finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" by (simp add: *) |
580 finally have "[bs]res. x = [p \<bullet> bs]res. (q \<bullet> x)" by (simp add: *) |
585 then show "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using * by metis |
581 then show "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" using * by metis |
586 qed |
582 qed |
587 |
583 |
588 lemma Abs_rename_lst: |
584 lemma Abs_rename_lst: |
589 fixes x::"'a::fs" |
585 fixes x::"'a::fs" |
590 assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" |
586 assumes a: "(p \<bullet> (set bs)) \<sharp>* x" |
591 shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
587 shows "\<exists>q. [bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
592 proof - |
588 proof - |
593 from a have "p \<bullet> (set bs) \<inter> (set bs) = {}" using at_fresh_star_inter |
589 from a list_renaming_perm |
594 by (simp add: fresh_star_Pair fresh_star_set) |
590 obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by blast |
595 with list_renaming_perm |
|
596 obtain q where *: "q \<bullet> bs = p \<bullet> bs" and **: "supp q \<subseteq> set bs \<union> (p \<bullet> set bs)" by metis |
|
597 have "[bs]lst. x = q \<bullet> ([bs]lst. x)" |
591 have "[bs]lst. x = q \<bullet> ([bs]lst. x)" |
598 apply(rule perm_supp_eq[symmetric]) |
592 apply(rule perm_supp_eq[symmetric]) |
599 using a ** |
593 using a ** |
600 unfolding fresh_star_Pair |
|
601 unfolding Abs_fresh_star_iff |
594 unfolding Abs_fresh_star_iff |
602 unfolding fresh_star_def |
595 unfolding fresh_star_def |
603 by auto |
596 by auto |
604 also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp |
597 also have "\<dots> = [q \<bullet> bs]lst. (q \<bullet> x)" by simp |
605 finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" by (simp add: *) |
598 finally have "[bs]lst. x = [p \<bullet> bs]lst. (q \<bullet> x)" by (simp add: *) |
609 |
602 |
610 text {* for deep recursive binders *} |
603 text {* for deep recursive binders *} |
611 |
604 |
612 lemma Abs_rename_set': |
605 lemma Abs_rename_set': |
613 fixes x::"'a::fs" |
606 fixes x::"'a::fs" |
614 assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" |
607 assumes a: "(p \<bullet> bs) \<sharp>* x" |
615 and b: "finite bs" |
608 and b: "finite bs" |
616 shows "\<exists>q. [bs]set. x = [q \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
609 shows "\<exists>q. [bs]set. x = [q \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
617 using Abs_rename_set[OF a b] by metis |
610 using Abs_rename_set[OF a b] by metis |
618 |
611 |
619 lemma Abs_rename_res': |
612 lemma Abs_rename_res': |
620 fixes x::"'a::fs" |
613 fixes x::"'a::fs" |
621 assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" |
614 assumes a: "(p \<bullet> bs) \<sharp>* x" |
622 and b: "finite bs" |
615 and b: "finite bs" |
623 shows "\<exists>q. [bs]res. x = [q \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
616 shows "\<exists>q. [bs]res. x = [q \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
624 using Abs_rename_res[OF a b] by metis |
617 using Abs_rename_res[OF a b] by metis |
625 |
618 |
626 lemma Abs_rename_lst': |
619 lemma Abs_rename_lst': |
627 fixes x::"'a::fs" |
620 fixes x::"'a::fs" |
628 assumes a: "(p \<bullet> (set bs)) \<sharp>* (bs, x)" |
621 assumes a: "(p \<bullet> (set bs)) \<sharp>* x" |
629 shows "\<exists>q. [bs]lst. x = [q \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
622 shows "\<exists>q. [bs]lst. x = [q \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
630 using Abs_rename_lst[OF a] by metis |
623 using Abs_rename_lst[OF a] by metis |
631 |
624 |
632 section {* Infrastructure for building tuples of relations and functions *} |
625 section {* Infrastructure for building tuples of relations and functions *} |
633 |
626 |