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