336 TRY o simp_tac (add_simpset ctxt thms2), |
336 TRY o simp_tac (add_simpset ctxt thms2), |
337 TRY o asm_full_simp_tac (add_simpset ctxt (thms1 @ (symmetric fv_bn_eqvts)))] i |
337 TRY o asm_full_simp_tac (add_simpset ctxt (thms1 @ (symmetric fv_bn_eqvts)))] i |
338 end) |
338 end) |
339 in |
339 in |
340 induct_prove qtys (goals1 @ goals2) qinduct tac ctxt |
340 induct_prove qtys (goals1 @ goals2) qinduct tac ctxt |
341 |> map atomize |
341 |> map (atomize ctxt) |
342 |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms fun_eq_iff[symmetric]})) |
342 |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms fun_eq_iff[symmetric]})) |
343 end |
343 end |
344 |
344 |
345 |
345 |
346 fun prove_bns_finite qtys qbns qinduct qbn_simps ctxt = |
346 fun prove_bns_finite qtys qbns qinduct qbn_simps ctxt = |
589 @ map (eqvt_rule ctxt (eqvt_strict_config addpres bn_eqvt)) fprops |
589 @ map (eqvt_rule ctxt (eqvt_strict_config addpres bn_eqvt)) fprops |
590 |
590 |
591 (* for freshness conditions *) |
591 (* for freshness conditions *) |
592 val tac1 = SOLVED' (EVERY' |
592 val tac1 = SOLVED' (EVERY' |
593 [ simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps peqs), |
593 [ simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps peqs), |
594 rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}), |
594 rewrite_goal_tac ctxt'' (@{thms fresh_star_Un[THEN eq_reflection]}), |
595 conj_tac (DETERM o resolve_tac fprops') ]) |
595 conj_tac (DETERM o resolve_tac fprops') ]) |
596 |
596 |
597 (* for equalities between constructors *) |
597 (* for equalities between constructors *) |
598 val tac2 = SOLVED' (EVERY' |
598 val tac2 = SOLVED' (EVERY' |
599 [ rtac (@{thm ssubst} OF prems), |
599 [ rtac (@{thm ssubst} OF prems), |
600 rewrite_goal_tac (map safe_mk_equiv eq_iff_thms), |
600 rewrite_goal_tac ctxt'' (map safe_mk_equiv eq_iff_thms), |
601 rewrite_goal_tac (map safe_mk_equiv abs_eqs), |
601 rewrite_goal_tac ctxt'' (map safe_mk_equiv abs_eqs), |
602 conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ]) |
602 conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ]) |
603 |
603 |
604 (* proves goal "P" *) |
604 (* proves goal "P" *) |
605 val side_thm = Goal.prove ctxt'' [] [] (term_of concl) |
605 val side_thm = Goal.prove ctxt'' [] [] (term_of concl) |
606 (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ])) |
606 (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ])) |