790 |
790 |
791 |
791 |
792 section {* Abstractions of single atoms *} |
792 section {* Abstractions of single atoms *} |
793 |
793 |
794 lemma Abs1_eq: |
794 lemma Abs1_eq: |
795 fixes x::"'a::fs" |
795 fixes x y::"'a::fs" |
796 shows "Abs_set {a} x = Abs_set {a} y \<longleftrightarrow> x = y" |
796 shows "[{atom a}]set. x = [{atom a}]set. y \<longleftrightarrow> x = y" |
797 and "Abs_res {a} x = Abs_res {a} y \<longleftrightarrow> x = y" |
797 and "[{atom a}]res. x = [{atom a}]res. y \<longleftrightarrow> x = y" |
798 and "Abs_lst [c] x = Abs_lst [c] y \<longleftrightarrow> x = y" |
798 and "[[atom a]]lst. x = [[atom a]]lst. y \<longleftrightarrow> x = y" |
799 unfolding Abs_eq_iff2 alphas |
799 unfolding Abs_eq_iff2 alphas |
800 apply(simp_all add: supp_perm_singleton fresh_star_def fresh_zero_perm) |
800 apply(simp_all add: supp_perm_singleton fresh_star_def fresh_zero_perm) |
801 apply(blast)+ |
801 apply(blast)+ |
802 done |
802 done |
803 |
803 |
|
804 lemma Abs1_eq_fresh: |
|
805 fixes x y::"'a::fs" |
|
806 and a b c::"'b::at" |
|
807 assumes "atom c \<sharp> (a, b, x, y)" |
|
808 shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y" |
|
809 and "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y" |
|
810 and "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y" |
|
811 proof - |
|
812 have "[{atom a}]set. x = (a \<leftrightarrow> c) \<bullet> ([{atom a}]set. x)" |
|
813 by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms) |
|
814 then have "[{atom a}]set. x = [{atom c}]set. ((a \<leftrightarrow> c) \<bullet> x)" by simp |
|
815 moreover |
|
816 have "[{atom b}]set. y = (b \<leftrightarrow> c) \<bullet> ([{atom b}]set. y)" |
|
817 by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms) |
|
818 then have "[{atom b}]set. y = [{atom c}]set. ((b \<leftrightarrow> c) \<bullet> y)" by simp |
|
819 ultimately |
|
820 show "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y" |
|
821 by (simp add: Abs1_eq) |
|
822 next |
|
823 have "[{atom a}]res. x = (a \<leftrightarrow> c) \<bullet> ([{atom a}]res. x)" |
|
824 by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms) |
|
825 then have "[{atom a}]res. x = [{atom c}]res. ((a \<leftrightarrow> c) \<bullet> x)" by simp |
|
826 moreover |
|
827 have "[{atom b}]res. y = (b \<leftrightarrow> c) \<bullet> ([{atom b}]res. y)" |
|
828 by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms) |
|
829 then have "[{atom b}]res. y = [{atom c}]res. ((b \<leftrightarrow> c) \<bullet> y)" by simp |
|
830 ultimately |
|
831 show "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y" |
|
832 by (simp add: Abs1_eq) |
|
833 next |
|
834 have "[[atom a]]lst. x = (a \<leftrightarrow> c) \<bullet> ([[atom a]]lst. x)" |
|
835 by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms) |
|
836 then have "[[atom a]]lst. x = [[atom c]]lst. ((a \<leftrightarrow> c) \<bullet> x)" by simp |
|
837 moreover |
|
838 have "[[atom b]]lst. y = (b \<leftrightarrow> c) \<bullet> ([[atom b]]lst. y)" |
|
839 by (rule_tac flip_fresh_fresh[symmetric]) (simp_all add: Abs_fresh_iff assms) |
|
840 then have "[[atom b]]lst. y = [[atom c]]lst. ((b \<leftrightarrow> c) \<bullet> y)" by simp |
|
841 ultimately |
|
842 show "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y" |
|
843 by (simp add: Abs1_eq) |
|
844 qed |
|
845 |
|
846 lemma Abs1_eq_all: |
|
847 fixes x y::"'a::fs" |
|
848 and z::"'c::fs" |
|
849 and a b::"'b::at" |
|
850 shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)" |
|
851 and "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)" |
|
852 and "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)" |
|
853 apply - |
|
854 apply(auto) |
|
855 apply(simp add: Abs1_eq_fresh(1)[symmetric]) |
|
856 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh) |
|
857 apply(drule_tac x="aa" in spec) |
|
858 apply(simp) |
|
859 apply(subst Abs1_eq_fresh(1)) |
|
860 apply(auto simp add: fresh_Pair)[1] |
|
861 apply(assumption) |
|
862 apply(simp add: Abs1_eq_fresh(2)[symmetric]) |
|
863 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh) |
|
864 apply(drule_tac x="aa" in spec) |
|
865 apply(simp) |
|
866 apply(subst Abs1_eq_fresh(2)) |
|
867 apply(auto simp add: fresh_Pair)[1] |
|
868 apply(assumption) |
|
869 apply(simp add: Abs1_eq_fresh(3)[symmetric]) |
|
870 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh) |
|
871 apply(drule_tac x="aa" in spec) |
|
872 apply(simp) |
|
873 apply(subst Abs1_eq_fresh(3)) |
|
874 apply(auto simp add: fresh_Pair)[1] |
|
875 apply(assumption) |
|
876 done |
|
877 |
804 lemma Abs1_eq_iff: |
878 lemma Abs1_eq_iff: |
805 fixes x::"'a::fs" |
879 fixes x y::"'a::fs" |
806 assumes "sort_of a = sort_of b" |
880 and a b::"'b::at" |
807 and "sort_of c = sort_of d" |
881 shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)" |
808 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)" |
882 and "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)" |
809 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)" |
883 and "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)" |
810 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)" |
|
811 proof - |
884 proof - |
812 { assume "a = b" |
885 { assume "a = b" |
813 then have "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq) |
886 then have "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq) |
814 } |
887 } |
815 moreover |
888 moreover |
816 { assume *: "a \<noteq> b" and **: "Abs_set {a} x = Abs_set {b} y" |
889 { assume *: "a \<noteq> b" and **: "Abs_set {atom a} x = Abs_set {atom b} y" |
817 have #: "a \<sharp> Abs_set {b} y" by (simp add: **[symmetric] Abs_fresh_iff) |
890 have #: "atom a \<sharp> Abs_set {atom b} y" by (simp add: **[symmetric] Abs_fresh_iff) |
818 have "Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_set {b} y)" by (simp add: permute_set_def assms) |
891 have "Abs_set {atom a} ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> (Abs_set {atom b} y)" by (simp) |
819 also have "\<dots> = Abs_set {b} y" |
892 also have "\<dots> = Abs_set {atom b} y" |
820 by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff) |
893 by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff) |
821 also have "\<dots> = Abs_set {a} x" using ** by simp |
894 also have "\<dots> = Abs_set {atom a} x" using ** by simp |
822 finally have "a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff) |
895 finally have "a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff) |
823 } |
896 } |
824 moreover |
897 moreover |
825 { assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y" |
898 { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" |
826 have "Abs_set {a} x = Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp |
899 have "Abs_set {atom a} x = Abs_set {atom a} ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp |
827 also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_set {b} y" by (simp add: permute_set_def assms) |
900 also have "\<dots> = (a \<leftrightarrow> b) \<bullet> Abs_set {atom b} y" by (simp add: permute_set_def assms) |
828 also have "\<dots> = Abs_set {b} y" |
901 also have "\<dots> = Abs_set {atom b} y" |
829 by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff) |
902 by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff) |
830 finally have "Abs_set {a} x = Abs_set {b} y" . |
903 finally have "Abs_set {atom a} x = Abs_set {atom b} y" . |
831 } |
904 } |
832 ultimately |
905 ultimately |
833 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)" |
906 show "Abs_set {atom a} x = Abs_set {atom b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)" |
834 by blast |
907 by blast |
835 next |
908 next |
836 { assume "a = b" |
909 { assume "a = b" |
837 then have "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq) |
910 then have "Abs_res {atom a} x = Abs_res {atom b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq) |
838 } |
911 } |
839 moreover |
912 moreover |
840 { assume *: "a \<noteq> b" and **: "Abs_res {a} x = Abs_res {b} y" |
913 { assume *: "a \<noteq> b" and **: "Abs_res {atom a} x = Abs_res {atom b} y" |
841 have #: "a \<sharp> Abs_res {b} y" by (simp add: **[symmetric] Abs_fresh_iff) |
914 have #: "atom a \<sharp> Abs_res {atom b} y" by (simp add: **[symmetric] Abs_fresh_iff) |
842 have "Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_res {b} y)" by (simp add: permute_set_def assms) |
915 have "Abs_res {atom a} ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> (Abs_res {atom b} y)" by (simp add: assms) |
843 also have "\<dots> = Abs_res {b} y" |
916 also have "\<dots> = Abs_res {atom b} y" |
844 by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff) |
917 by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff) |
845 also have "\<dots> = Abs_res {a} x" using ** by simp |
918 also have "\<dots> = Abs_res {atom a} x" using ** by simp |
846 finally have "a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff) |
919 finally have "a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff) |
847 } |
920 } |
848 moreover |
921 moreover |
849 { assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y" |
922 { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" |
850 have "Abs_res {a} x = Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp |
923 have "Abs_res {atom a} x = Abs_res {atom a} ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp |
851 also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_res {b} y" by (simp add: permute_set_def assms) |
924 also have "\<dots> = (a \<leftrightarrow> b) \<bullet> Abs_res {atom b} y" by (simp add: permute_set_def assms) |
852 also have "\<dots> = Abs_res {b} y" |
925 also have "\<dots> = Abs_res {atom b} y" |
853 by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff) |
926 by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff) |
854 finally have "Abs_res {a} x = Abs_res {b} y" . |
927 finally have "Abs_res {atom a} x = Abs_res {atom b} y" . |
855 } |
928 } |
856 ultimately |
929 ultimately |
857 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)" |
930 show "Abs_res {atom a} x = Abs_res {atom b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)" |
858 by blast |
931 by blast |
859 next |
932 next |
860 { assume "c = d" |
933 { assume "a = b" |
861 then have "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y)" by (simp add: Abs1_eq) |
934 then have "Abs_lst [atom a] x = Abs_lst [atom b] y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq) |
862 } |
935 } |
863 moreover |
936 moreover |
864 { assume *: "c \<noteq> d" and **: "Abs_lst [c] x = Abs_lst [d] y" |
937 { assume *: "a \<noteq> b" and **: "Abs_lst [atom a] x = Abs_lst [atom b] y" |
865 have #: "c \<sharp> Abs_lst [d] y" by (simp add: **[symmetric] Abs_fresh_iff) |
938 have #: "atom a \<sharp> Abs_lst [atom b] y" by (simp add: **[symmetric] Abs_fresh_iff) |
866 have "Abs_lst [c] ((c \<rightleftharpoons> d) \<bullet> y) = (c \<rightleftharpoons> d) \<bullet> (Abs_lst [d] y)" by (simp add: assms) |
939 have "Abs_lst [atom a] ((a \<leftrightarrow> b) \<bullet> y) = (a \<leftrightarrow> b) \<bullet> (Abs_lst [atom b] y)" by (simp add: assms) |
867 also have "\<dots> = Abs_lst [d] y" |
940 also have "\<dots> = Abs_lst [atom b] y" |
868 by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff) |
941 by (rule flip_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff) |
869 also have "\<dots> = Abs_lst [c] x" using ** by simp |
942 also have "\<dots> = Abs_lst [atom a] x" using ** by simp |
870 finally have "c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff) |
943 finally have "a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" using # * by (simp add: Abs1_eq Abs_fresh_iff) |
871 } |
944 } |
872 moreover |
945 moreover |
873 { assume *: "c \<noteq> d" and **: "x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y" |
946 { assume *: "a \<noteq> b" and **: "x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y" |
874 have "Abs_lst [c] x = Abs_lst [c] ((c \<rightleftharpoons> d) \<bullet> y)" using ** by simp |
947 have "Abs_lst [atom a] x = Abs_lst [atom a] ((a \<leftrightarrow> b) \<bullet> y)" using ** by simp |
875 also have "\<dots> = (c \<rightleftharpoons> d) \<bullet> Abs_lst [d] y" by (simp add: assms) |
948 also have "\<dots> = (a \<leftrightarrow> b) \<bullet> Abs_lst [atom b] y" by (simp add: assms) |
876 also have "\<dots> = Abs_lst [d] y" |
949 also have "\<dots> = Abs_lst [atom b] y" |
877 by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff) |
950 by (rule flip_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff) |
878 finally have "Abs_lst [c] x = Abs_lst [d] y" . |
951 finally have "Abs_lst [atom a] x = Abs_lst [atom b] y" . |
879 } |
952 } |
880 ultimately |
953 ultimately |
881 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)" |
954 show "Abs_lst [atom a] x = Abs_lst [atom b] y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<leftrightarrow> b) \<bullet> y \<and> atom a \<sharp> y)" |
882 by blast |
955 by blast |
883 qed |
956 qed |
884 |
957 |
885 lemma Abs1_eq_iff': |
958 lemma Abs1_eq_iff': |
886 fixes x::"'a::fs" |
959 fixes x::"'a::fs" |
887 assumes "sort_of a = sort_of b" |
960 and a b::"'b::at" |
888 and "sort_of c = sort_of d" |
961 shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)" |
889 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)" |
962 and "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)" |
890 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)" |
963 and "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)" |
891 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)" |
|
892 using assms by (auto simp add: Abs1_eq_iff fresh_permute_left) |
964 using assms by (auto simp add: Abs1_eq_iff fresh_permute_left) |
893 |
965 |
894 |
966 |
895 subsection {* Renaming of bodies of abstractions *} |
967 subsection {* Renaming of bodies of abstractions *} |
896 |
968 |