877 using assms by (auto simp add: Abs1_eq_iff fresh_permute_left) |
877 using assms by (auto simp add: Abs1_eq_iff fresh_permute_left) |
878 |
878 |
879 |
879 |
880 subsection {* Renaming of bodies of abstractions *} |
880 subsection {* Renaming of bodies of abstractions *} |
881 |
881 |
882 (* FIXME: finiteness assumption is not needed *) |
|
883 |
|
884 lemma Abs_rename_set: |
882 lemma Abs_rename_set: |
885 fixes x::"'a::fs" |
883 fixes x::"'a::fs" |
886 assumes a: "(p \<bullet> bs) \<sharp>* x" |
884 assumes a: "(p \<bullet> bs) \<sharp>* x" |
887 and b: "finite bs" |
885 (*and b: "finite bs"*) |
888 shows "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
886 shows "\<exists>q. [bs]set. x = [p \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
889 proof - |
887 proof - |
890 from set_renaming_perm2 |
888 from set_renaming_perm2 |
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 |
889 obtain q where *: "\<forall>b \<in> bs. q \<bullet> b = p \<bullet> b" and **: "supp q \<subseteq> bs \<union> (p \<bullet> bs)" by blast |
892 have ***: "q \<bullet> bs = p \<bullet> bs" using b * by (induct) (simp add: permute_set_eq, simp add: insert_eqvt) |
890 have ***: "q \<bullet> bs = p \<bullet> bs" using * |
|
891 unfolding permute_set_eq_image image_def by auto |
893 have "[bs]set. x = q \<bullet> ([bs]set. x)" |
892 have "[bs]set. x = q \<bullet> ([bs]set. x)" |
894 apply(rule perm_supp_eq[symmetric]) |
893 apply(rule perm_supp_eq[symmetric]) |
895 using a ** |
894 using a ** |
896 unfolding Abs_fresh_star_iff |
895 unfolding Abs_fresh_star_iff |
897 unfolding fresh_star_def |
896 unfolding fresh_star_def |
902 qed |
901 qed |
903 |
902 |
904 lemma Abs_rename_res: |
903 lemma Abs_rename_res: |
905 fixes x::"'a::fs" |
904 fixes x::"'a::fs" |
906 assumes a: "(p \<bullet> bs) \<sharp>* x" |
905 assumes a: "(p \<bullet> bs) \<sharp>* x" |
907 and b: "finite bs" |
906 (*and b: "finite bs"*) |
908 shows "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
907 shows "\<exists>q. [bs]res. x = [p \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
909 proof - |
908 proof - |
910 from set_renaming_perm2 |
909 from set_renaming_perm2 |
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 |
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 |
912 have ***: "q \<bullet> bs = p \<bullet> bs" using b * by (induct) (simp add: permute_set_eq, simp add: insert_eqvt) |
911 have ***: "q \<bullet> bs = p \<bullet> bs" using * |
|
912 unfolding permute_set_eq_image image_def by auto |
913 have "[bs]res. x = q \<bullet> ([bs]res. x)" |
913 have "[bs]res. x = q \<bullet> ([bs]res. x)" |
914 apply(rule perm_supp_eq[symmetric]) |
914 apply(rule perm_supp_eq[symmetric]) |
915 using a ** |
915 using a ** |
916 unfolding Abs_fresh_star_iff |
916 unfolding Abs_fresh_star_iff |
917 unfolding fresh_star_def |
917 unfolding fresh_star_def |
944 text {* for deep recursive binders *} |
944 text {* for deep recursive binders *} |
945 |
945 |
946 lemma Abs_rename_set': |
946 lemma Abs_rename_set': |
947 fixes x::"'a::fs" |
947 fixes x::"'a::fs" |
948 assumes a: "(p \<bullet> bs) \<sharp>* x" |
948 assumes a: "(p \<bullet> bs) \<sharp>* x" |
949 and b: "finite bs" |
949 (*and b: "finite bs"*) |
950 shows "\<exists>q. [bs]set. x = [q \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
950 shows "\<exists>q. [bs]set. x = [q \<bullet> bs]set. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
951 using Abs_rename_set[OF a b] by metis |
951 using Abs_rename_set[OF a] by metis |
952 |
952 |
953 lemma Abs_rename_res': |
953 lemma Abs_rename_res': |
954 fixes x::"'a::fs" |
954 fixes x::"'a::fs" |
955 assumes a: "(p \<bullet> bs) \<sharp>* x" |
955 assumes a: "(p \<bullet> bs) \<sharp>* x" |
956 and b: "finite bs" |
956 (*and b: "finite bs"*) |
957 shows "\<exists>q. [bs]res. x = [q \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
957 shows "\<exists>q. [bs]res. x = [q \<bullet> bs]res. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
958 using Abs_rename_res[OF a b] by metis |
958 using Abs_rename_res[OF a] by metis |
959 |
959 |
960 lemma Abs_rename_lst': |
960 lemma Abs_rename_lst': |
961 fixes x::"'a::fs" |
961 fixes x::"'a::fs" |
962 assumes a: "(p \<bullet> (set bs)) \<sharp>* x" |
962 assumes a: "(p \<bullet> (set bs)) \<sharp>* x" |
963 shows "\<exists>q. [bs]lst. x = [q \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |
963 shows "\<exists>q. [bs]lst. x = [q \<bullet> bs]lst. (q \<bullet> x) \<and> q \<bullet> bs = p \<bullet> bs" |