1\DOC DISJ_CASES_TAC 2 3\TYPE {DISJ_CASES_TAC : thm_tactic} 4 5\SYNOPSIS 6Produces a case split based on a disjunctive theorem. 7 8\KEYWORDS 9tactic, disjunction, cases. 10 11\DESCRIBE 12Given a theorem {th} of the form {A |- u \/ v}, {DISJ_CASES_TAC th} 13applied to a goal 14produces two subgoals, one with {u} as an assumption and one with {v}: 15{ 16 A ?- t 17 ============================ DISJ_CASES_TAC (A |- u \/ v) 18 A u {u} ?- t A u {v}?- t 19} 20 21 22\FAILURE 23Fails if the given theorem does not have a disjunctive conclusion. 24 25\EXAMPLE 26Given the simple fact about arithmetic {th}, {|- (m = 0) \/ (?n. m = SUC n)}, 27the tactic {DISJ_CASES_TAC th} can be used to produce a case split: 28{ 29 - DISJ_CASES_TAC th ([],Term`(P:num -> bool) m`); 30 ([([`m = 0`], `P m`), 31 ([`?n. m = SUC n`], `P m`)], fn) : tactic_result 32} 33 34 35\USES 36Performing a case analysis according to a disjunctive theorem. 37 38\SEEALSO 39Tactic.ASSUME_TAC, Tactic.ASM_CASES_TAC, Tactic.COND_CASES_TAC, Thm_cont.DISJ_CASES_THEN, Tactic.STRUCT_CASES_TAC. 40\ENDDOC 41