870 (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all |
870 (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all |
871 end |
871 end |
872 *} |
872 *} |
873 |
873 |
874 lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" |
874 lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" |
875 apply (simp add: supp_Abs supp_Pair) |
875 apply (simp add: supp_abs supp_Pair) |
876 apply blast |
876 apply blast |
877 done |
877 done |
878 |
878 |
879 ML {* |
879 ML {* |
880 fun supp_eq_tac ind fv perm eqiff ctxt = |
880 fun supp_eq_tac ind fv perm eqiff ctxt = |
881 rel_indtac ind THEN_ALL_NEW |
881 rel_indtac ind THEN_ALL_NEW |
882 asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
882 asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
883 asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_Abs[symmetric]}) THEN_ALL_NEW |
883 asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs[symmetric]}) THEN_ALL_NEW |
884 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
884 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
885 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
885 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
886 simp_tac (HOL_basic_ss addsimps (@{thm permute_ABS} :: perm)) THEN_ALL_NEW |
886 simp_tac (HOL_basic_ss addsimps (@{thm permute_Abs} :: perm)) THEN_ALL_NEW |
887 simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW |
887 simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW |
888 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
888 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
889 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen}) THEN_ALL_NEW |
889 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen}) THEN_ALL_NEW |
890 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW |
890 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW |
891 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW |
891 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW |