equal
deleted
inserted
replaced
348 |
348 |
349 val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac |
349 val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac |
350 |
350 |
351 val bound_tac = |
351 val bound_tac = |
352 EVERY' [ rtac exi_zero, |
352 EVERY' [ rtac exi_zero, |
353 resolve_tac @{thms alpha_gen_refl}, |
353 resolve_tac @{thms alpha_refl}, |
354 asm_full_simp_tac (HOL_ss addsimps prod_simps) ] |
354 asm_full_simp_tac (HOL_ss addsimps prod_simps) ] |
355 in |
355 in |
356 REPEAT o FIRST' [rtac @{thm conjI}, |
356 REPEAT o FIRST' [rtac @{thm conjI}, |
357 resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]] |
357 resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]] |
358 end |
358 end |
405 end) ctxt |
405 end) ctxt |
406 val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel.simps alphas} |
406 val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel.simps alphas} |
407 in |
407 in |
408 EVERY' |
408 EVERY' |
409 [ etac exi_neg, |
409 [ etac exi_neg, |
410 resolve_tac @{thms alpha_gen_sym_eqvt}, |
410 resolve_tac @{thms alpha_sym_eqvt}, |
411 asm_full_simp_tac (HOL_ss addsimps prod_simps), |
411 asm_full_simp_tac (HOL_ss addsimps prod_simps), |
412 Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl}, |
412 Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl}, |
413 trans_prem_tac pred_names ctxt ] |
413 trans_prem_tac pred_names ctxt ] |
414 end |
414 end |
415 |
415 |