equal
deleted
inserted
replaced
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 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 alphas2}) THEN_ALL_NEW |
66 asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ 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 *} |
79 fun constr_rsp_tac inj rsp = |
79 fun constr_rsp_tac inj rsp = |
80 REPEAT o rtac impI THEN' |
80 REPEAT o rtac impI THEN' |
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 alphas2}) THEN_ALL_NEW |
85 asm_full_simp_tac (HOL_ss addsimps (rsp @ |
85 asm_full_simp_tac (HOL_ss addsimps (rsp @ |
86 @{thms alphas 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 |
258 end |
258 end |
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 alphas2}) THEN_ALL_NEW |
264 asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ 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 *} |