886 lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" |
886 lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" |
887 apply (simp add: supp_abs supp_Pair) |
887 apply (simp add: supp_abs supp_Pair) |
888 apply blast |
888 apply blast |
889 done |
889 done |
890 |
890 |
|
891 (* TODO: this is a hack, it assumes that only one type of Abs's is present |
|
892 in the type and chooses this supp_abs *) |
|
893 ML {* |
|
894 fun choose_alpha_abs eqiff = |
|
895 let |
|
896 fun exists_subterms f ts = true mem (map (exists_subterm f) ts); |
|
897 val terms = map prop_of eqiff; |
|
898 fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms |
|
899 val no = |
|
900 if check @{const_name alpha_gen} then 0 else |
|
901 if check @{const_name alpha_res} then 1 else |
|
902 if check @{const_name alpha_lst} then 2 else |
|
903 error "Failure choosing supp_abs" |
|
904 in |
|
905 nth @{thms supp_abs[symmetric]} no |
|
906 end |
|
907 *} |
|
908 |
891 ML {* |
909 ML {* |
892 fun supp_eq_tac ind fv perm eqiff ctxt = |
910 fun supp_eq_tac ind fv perm eqiff ctxt = |
893 rel_indtac ind THEN_ALL_NEW |
911 rel_indtac ind THEN_ALL_NEW |
894 asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
912 asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
895 asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs[symmetric]}) THEN_ALL_NEW |
913 asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW |
896 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
914 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
897 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
915 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
898 simp_tac (HOL_basic_ss addsimps (@{thm permute_abs} :: perm)) THEN_ALL_NEW |
916 simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW |
899 simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW |
917 simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW |
900 simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW |
918 simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW |
901 simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW |
919 simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW |
902 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW |
920 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW |
903 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW |
921 asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW |