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: |
804 lemma Abs1_eq_iff_fresh: |
805 fixes x y::"'a::fs" |
805 fixes x y::"'a::fs" |
806 and a b c::"'b::at" |
806 and a b c::"'b::at" |
807 assumes "atom c \<sharp> (a, b, x, y)" |
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" |
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" |
809 and "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y" |
841 ultimately |
841 ultimately |
842 show "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y" |
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) |
843 by (simp add: Abs1_eq) |
844 qed |
844 qed |
845 |
845 |
846 lemma Abs1_eq_all: |
846 lemma Abs1_eq_iff_all: |
847 fixes x y::"'a::fs" |
847 fixes x y::"'a::fs" |
848 and z::"'c::fs" |
848 and z::"'c::fs" |
849 and a b::"'b::at" |
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)" |
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)" |
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)" |
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 - |
853 apply - |
854 apply(auto) |
854 apply(auto) |
855 apply(simp add: Abs1_eq_fresh(1)[symmetric]) |
855 apply(simp add: Abs1_eq_iff_fresh(1)[symmetric]) |
856 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh) |
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) |
857 apply(drule_tac x="aa" in spec) |
858 apply(simp) |
858 apply(simp) |
859 apply(subst Abs1_eq_fresh(1)) |
859 apply(subst Abs1_eq_iff_fresh(1)) |
860 apply(auto simp add: fresh_Pair)[1] |
860 apply(auto simp add: fresh_Pair)[1] |
861 apply(assumption) |
861 apply(assumption) |
862 apply(simp add: Abs1_eq_fresh(2)[symmetric]) |
862 apply(simp add: Abs1_eq_iff_fresh(2)[symmetric]) |
863 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh) |
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) |
864 apply(drule_tac x="aa" in spec) |
865 apply(simp) |
865 apply(simp) |
866 apply(subst Abs1_eq_fresh(2)) |
866 apply(subst Abs1_eq_iff_fresh(2)) |
867 apply(auto simp add: fresh_Pair)[1] |
867 apply(auto simp add: fresh_Pair)[1] |
868 apply(assumption) |
868 apply(assumption) |
869 apply(simp add: Abs1_eq_fresh(3)[symmetric]) |
869 apply(simp add: Abs1_eq_iff_fresh(3)[symmetric]) |
870 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh) |
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) |
871 apply(drule_tac x="aa" in spec) |
872 apply(simp) |
872 apply(simp) |
873 apply(subst Abs1_eq_fresh(3)) |
873 apply(subst Abs1_eq_iff_fresh(3)) |
874 apply(auto simp add: fresh_Pair)[1] |
874 apply(auto simp add: fresh_Pair)[1] |
875 apply(assumption) |
875 apply(assumption) |
876 done |
876 done |
877 |
877 |
878 lemma Abs1_eq_iff: |
878 lemma Abs1_eq_iff: |
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)" |
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)" |
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)" |
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)" |
964 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) |
965 |
965 |
966 |
966 |
|
967 ML {* |
|
968 fun alpha_single_simproc thm _ ss ctrm = |
|
969 let |
|
970 val ctxt = Simplifier.the_context ss |
|
971 val thy = Proof_Context.theory_of ctxt |
|
972 val _ $ (_ $ x) $ (_ $ y) = term_of ctrm |
|
973 val cvrs = union (op =) (Term.add_frees x []) (Term.add_frees y []) |
|
974 |> filter (fn (_, ty) => Sign.of_sort thy (ty, @{sort fs})) |
|
975 |> map Free |
|
976 |> HOLogic.mk_tuple |
|
977 |> Thm.cterm_of thy |
|
978 val cvrs_ty = ctyp_of_term cvrs |
|
979 val thm' = thm |
|
980 |> Drule.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs] |
|
981 in |
|
982 SOME thm' |
|
983 end |
|
984 *} |
|
985 |
|
986 simproc_setup alpha_set ("[{atom a}]set. x = [{atom b}]set. y") = |
|
987 {* alpha_single_simproc @{thm Abs1_eq_iff_all(1)[THEN eq_reflection]} *} |
|
988 |
|
989 simproc_setup alpha_res ("[{atom a}]res. x = [{atom b}]res. y") = |
|
990 {* alpha_single_simproc @{thm Abs1_eq_iff_all(2)[THEN eq_reflection]} *} |
|
991 |
|
992 simproc_setup alpha_lst ("[[atom a]]lst. x = [[atom b]]lst. y") = |
|
993 {* alpha_single_simproc @{thm Abs1_eq_iff_all(3)[THEN eq_reflection]} *} |
|
994 |
|
995 |
967 subsection {* Renaming of bodies of abstractions *} |
996 subsection {* Renaming of bodies of abstractions *} |
968 |
997 |
969 lemma Abs_rename_set: |
998 lemma Abs_rename_set: |
970 fixes x::"'a::fs" |
999 fixes x::"'a::fs" |
971 assumes a: "(p \<bullet> bs) \<sharp>* x" |
1000 assumes a: "(p \<bullet> bs) \<sharp>* x" |