532 (fn _ => assume_tac 1); |
532 (fn _ => assume_tac 1); |
533 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE]; |
533 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE]; |
534 val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls; |
534 val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls; |
535 |
535 |
536 fun simp_case_tac ctxt i = |
536 fun simp_case_tac ctxt i = |
537 EVERY' [elim_tac, asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac] i; |
537 EVERY' [elim_tac, asm_full_simp_tac ctxt, elim_tac, REPEAT o bound_hyp_subst_tac ctxt] i; |
538 |
538 |
539 in |
539 in |
540 |
540 |
541 fun mk_cases ctxt prop = |
541 fun mk_cases ctxt prop = |
542 let |
542 let |
722 rewrite_goals_tac simp_thms2, |
722 rewrite_goals_tac simp_thms2, |
723 (*This disjE separates out the introduction rules*) |
723 (*This disjE separates out the introduction rules*) |
724 REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])), |
724 REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])), |
725 (*Now break down the individual cases. No disjE here in case |
725 (*Now break down the individual cases. No disjE here in case |
726 some premise involves disjunction.*) |
726 some premise involves disjunction.*) |
727 REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)), |
727 REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt'')), |
728 REPEAT (FIRSTGOAL |
728 REPEAT (FIRSTGOAL |
729 (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))), |
729 (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))), |
730 EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule |
730 EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule |
731 (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem, |
731 (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem, |
732 conjI, refl] 1)) prems)]); |
732 conjI, refl] 1)) prems)]); |