equal
deleted
inserted
replaced
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 rel_indtac 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 alpha_gen2}) THEN_ALL_NEW |
65 asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
66 asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)) THEN_ALL_NEW |
66 asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ 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 |
69 TRY o blast_tac (claset_of ctxt) |
69 TRY o blast_tac (claset_of ctxt) |
70 *} |
70 *} |
71 |
71 |
81 simp_tac (HOL_ss addsimps inj) THEN' split_conj_tac THEN_ALL_NEW |
81 simp_tac (HOL_ss addsimps inj) THEN' split_conj_tac THEN_ALL_NEW |
82 (asm_simp_tac HOL_ss THEN_ALL_NEW ( |
82 (asm_simp_tac HOL_ss THEN_ALL_NEW ( |
83 REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW |
83 REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW |
84 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
84 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
85 asm_full_simp_tac (HOL_ss addsimps (rsp @ |
85 asm_full_simp_tac (HOL_ss addsimps (rsp @ |
86 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left})) |
86 @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left})) |
87 )) |
87 )) |
88 *} |
88 *} |
89 |
89 |
90 ML {* |
90 ML {* |
91 fun perm_arg arg = |
91 fun perm_arg arg = |
109 rel_indtac induct THEN_ALL_NEW |
109 rel_indtac induct THEN_ALL_NEW |
110 simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW |
110 simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW |
111 REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW |
111 REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW |
112 asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW |
112 asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW |
113 asm_full_simp_tac (HOL_ss addsimps |
113 asm_full_simp_tac (HOL_ss addsimps |
114 @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW |
114 @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas}) THEN_ALL_NEW |
115 (split_conj_tac THEN_ALL_NEW TRY o resolve_tac |
115 (split_conj_tac THEN_ALL_NEW TRY o resolve_tac |
116 @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]}) |
116 @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]}) |
117 THEN_ALL_NEW |
117 THEN_ALL_NEW |
118 asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps)) |
118 asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps)) |
119 *} |
119 *} |
259 *} |
259 *} |
260 |
260 |
261 ML {* |
261 ML {* |
262 fun fvbv_rsp_tac' simps ctxt = |
262 fun fvbv_rsp_tac' simps ctxt = |
263 asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
263 asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
264 asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: simps)) THEN_ALL_NEW |
264 asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ simps)) THEN_ALL_NEW |
265 REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW |
265 REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW |
266 asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW |
266 asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW |
267 TRY o blast_tac (claset_of ctxt) |
267 TRY o blast_tac (claset_of ctxt) |
268 *} |
268 *} |
269 |
269 |