889 in |
889 in |
890 (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all |
890 (fv_ts_nobn ~~ alpha_ts_nobn) ~~ fv_alpha_bn_all |
891 end |
891 end |
892 *} |
892 *} |
893 |
893 |
894 lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" |
|
895 apply (simp add: supp_abs supp_Pair) |
|
896 apply blast |
|
897 done |
|
898 |
|
899 (* TODO: this is a hack, it assumes that only one type of Abs's is present |
894 (* TODO: this is a hack, it assumes that only one type of Abs's is present |
900 in the type and chooses this supp_abs *) |
895 in the type and chooses this supp_abs. Additionally single atoms are |
|
896 treated properly. *) |
901 ML {* |
897 ML {* |
902 fun choose_alpha_abs eqiff = |
898 fun choose_alpha_abs eqiff = |
903 let |
899 let |
904 fun exists_subterms f ts = true mem (map (exists_subterm f) ts); |
900 fun exists_subterms f ts = true mem (map (exists_subterm f) ts); |
905 val terms = map prop_of eqiff; |
901 val terms = map prop_of eqiff; |
906 fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms |
902 fun check cname = exists_subterms (fn x => fst(dest_Const x) = cname handle _ => false) terms |
907 val no = |
903 val no = |
|
904 if check @{const_name alpha_lst} then 2 else |
|
905 if check @{const_name alpha_res} then 1 else |
908 if check @{const_name alpha_gen} then 0 else |
906 if check @{const_name alpha_gen} then 0 else |
909 if check @{const_name alpha_res} then 1 else |
|
910 if check @{const_name alpha_lst} then 2 else |
|
911 error "Failure choosing supp_abs" |
907 error "Failure choosing supp_abs" |
912 in |
908 in |
913 nth @{thms supp_abs[symmetric]} no |
909 nth @{thms supp_abs[symmetric]} no |
914 end |
910 end |
915 *} |
911 *} |
|
912 lemma supp_abs_atom: "supp (Abs {atom a} (x :: 'a :: fs)) = supp x - {atom a}" |
|
913 by (rule supp_abs(1)) |
|
914 |
|
915 lemma supp_abs_sum: |
|
916 "supp (Abs x (a :: 'a :: fs)) \<union> supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" |
|
917 "supp (Abs_res x (a :: 'a :: fs)) \<union> supp (Abs_res x (b :: 'b :: fs)) = supp (Abs_res x (a, b))" |
|
918 "supp (Abs_lst y (a :: 'a :: fs)) \<union> supp (Abs_lst y (b :: 'b :: fs)) = supp (Abs_lst y (a, b))" |
|
919 apply (simp_all add: supp_abs supp_Pair) |
|
920 apply blast+ |
|
921 done |
|
922 |
916 |
923 |
917 ML {* |
924 ML {* |
918 fun supp_eq_tac ind fv perm eqiff ctxt = |
925 fun supp_eq_tac ind fv perm eqiff ctxt = |
919 rel_indtac ind THEN_ALL_NEW |
926 rel_indtac ind THEN_ALL_NEW |
920 asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
927 asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW |
|
928 asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs_atom[symmetric]}) THEN_ALL_NEW |
921 asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW |
929 asm_full_simp_tac (HOL_basic_ss addsimps [choose_alpha_abs eqiff]) THEN_ALL_NEW |
922 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
930 simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW |
923 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
931 simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW |
924 simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW |
932 simp_tac (HOL_basic_ss addsimps (@{thms permute_abs} @ perm)) THEN_ALL_NEW |
925 simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW |
933 simp_tac (HOL_basic_ss addsimps (@{thms Abs_eq_iff} @ eqiff)) THEN_ALL_NEW |