equal
deleted
inserted
replaced
58 end |
58 end |
59 *} |
59 *} |
60 |
60 |
61 ML {* |
61 ML {* |
62 fun fvbv_rsp_tac induct fvbv_simps ctxt = |
62 fun fvbv_rsp_tac induct fvbv_simps ctxt = |
63 rel_indtac induct THEN_ALL_NEW |
63 rtac induct THEN_ALL_NEW |
64 (TRY o rtac @{thm TrueI}) THEN_ALL_NEW |
64 (TRY o rtac @{thm TrueI}) THEN_ALL_NEW |
65 asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW |
65 asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW |
66 asm_full_simp_tac (HOL_ss addsimps (@{thms alphas prod_rel.simps prod_fv.simps} @ fvbv_simps)) THEN_ALL_NEW |
66 asm_full_simp_tac (HOL_ss addsimps (@{thms alphas prod_rel.simps prod_fv.simps} @ fvbv_simps)) THEN_ALL_NEW |
67 REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW |
67 REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW |
68 asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW |
68 asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW |
94 by auto |
94 by auto |
95 |
95 |
96 |
96 |
97 ML {* |
97 ML {* |
98 fun alpha_eqvt_tac induct simps ctxt = |
98 fun alpha_eqvt_tac induct simps ctxt = |
99 rel_indtac induct THEN_ALL_NEW |
99 rtac induct THEN_ALL_NEW |
100 simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW |
100 simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW |
101 REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW |
101 REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW |
102 asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW |
102 asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW |
103 asm_full_simp_tac (HOL_ss addsimps |
103 asm_full_simp_tac (HOL_ss addsimps |
104 @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas prod_rel.simps prod_fv.simps}) THEN_ALL_NEW |
104 @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas prod_rel.simps prod_fv.simps}) THEN_ALL_NEW |