equal
deleted
inserted
replaced
742 shows "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)" |
742 shows "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)" |
743 and "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)" |
743 and "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)" |
744 and "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y)" |
744 and "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y)" |
745 proof - |
745 proof - |
746 { assume "a = b" |
746 { assume "a = b" |
747 then have "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y)" |
747 then have "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq) |
748 by (simp add: Abs1_eq) |
|
749 } |
748 } |
750 moreover |
749 moreover |
751 { assume *: "a \<noteq> b" and **: "Abs_set {a} x = Abs_set {b} y" |
750 { assume *: "a \<noteq> b" and **: "Abs_set {a} x = Abs_set {b} y" |
752 have #: "a \<sharp> Abs_set {b} y" by (simp add: **[symmetric] Abs_fresh_iff) |
751 have #: "a \<sharp> Abs_set {b} y" by (simp add: **[symmetric] Abs_fresh_iff) |
753 have "Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_set {b} y)" by (simp add: permute_set_eq assms) |
752 have "Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_set {b} y)" by (simp add: permute_set_eq assms) |
767 ultimately |
766 ultimately |
768 show "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)" |
767 show "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)" |
769 by blast |
768 by blast |
770 next |
769 next |
771 { assume "a = b" |
770 { assume "a = b" |
772 then have "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y)" |
771 then have "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq) |
773 by (simp add: Abs1_eq) |
|
774 } |
772 } |
775 moreover |
773 moreover |
776 { assume *: "a \<noteq> b" and **: "Abs_res {a} x = Abs_res {b} y" |
774 { assume *: "a \<noteq> b" and **: "Abs_res {a} x = Abs_res {b} y" |
777 have #: "a \<sharp> Abs_res {b} y" by (simp add: **[symmetric] Abs_fresh_iff) |
775 have #: "a \<sharp> Abs_res {b} y" by (simp add: **[symmetric] Abs_fresh_iff) |
778 have "Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_res {b} y)" by (simp add: permute_set_eq assms) |
776 have "Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_res {b} y)" by (simp add: permute_set_eq assms) |
792 ultimately |
790 ultimately |
793 show "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)" |
791 show "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)" |
794 by blast |
792 by blast |
795 next |
793 next |
796 { assume "c = d" |
794 { assume "c = d" |
797 then have "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y)" |
795 then have "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y)" by (simp add: Abs1_eq) |
798 by (simp add: Abs1_eq) |
|
799 } |
796 } |
800 moreover |
797 moreover |
801 { assume *: "c \<noteq> d" and **: "Abs_lst [c] x = Abs_lst [d] y" |
798 { assume *: "c \<noteq> d" and **: "Abs_lst [c] x = Abs_lst [d] y" |
802 have #: "c \<sharp> Abs_lst [d] y" by (simp add: **[symmetric] Abs_fresh_iff) |
799 have #: "c \<sharp> Abs_lst [d] y" by (simp add: **[symmetric] Abs_fresh_iff) |
803 have "Abs_lst [c] ((c \<rightleftharpoons> d) \<bullet> y) = (c \<rightleftharpoons> d) \<bullet> (Abs_lst [d] y)" by (simp add: assms) |
800 have "Abs_lst [c] ((c \<rightleftharpoons> d) \<bullet> y) = (c \<rightleftharpoons> d) \<bullet> (Abs_lst [d] y)" by (simp add: assms) |
817 ultimately |
814 ultimately |
818 show "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y)" |
815 show "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y)" |
819 by blast |
816 by blast |
820 qed |
817 qed |
821 |
818 |
|
819 lemma Abs1_eq_iff': |
|
820 fixes x::"'a::fs" |
|
821 assumes "sort_of a = sort_of b" |
|
822 and "sort_of c = sort_of d" |
|
823 shows "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<rightleftharpoons> a) \<bullet> x = y \<and> b \<sharp> x)" |
|
824 and "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<rightleftharpoons> a) \<bullet> x = y \<and> b \<sharp> x)" |
|
825 and "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> (d \<rightleftharpoons> c) \<bullet> x = y \<and> d \<sharp> x)" |
|
826 using assms by (auto simp add: Abs1_eq_iff fresh_permute_left) |
|
827 |
822 |
828 |
823 subsection {* Renaming of bodies of abstractions *} |
829 subsection {* Renaming of bodies of abstractions *} |
824 |
830 |
825 (* FIXME: finiteness assumption is not needed *) |
831 (* FIXME: finiteness assumption is not needed *) |
826 |
832 |