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