DISJ_CASES_TAC : thm_tactic

- STRUCTURE
- SYNOPSIS
- Produces a case split based on a disjunctive theorem.
- DESCRIPTION
- Given a theorem th of the form A |- u \/ v, DISJ_CASES_TAC th applied to a goal produces two subgoals, one with u as an assumption and one with v:
A ?- t ============================ DISJ_CASES_TAC (A |- u \/ v) A u {u} ?- t A u {v}?- t

- FAILURE
- Fails if the given theorem does not have a disjunctive conclusion.
- EXAMPLE
- Given the simple fact about arithmetic th, |- (m = 0) \/ (?n. m = SUC n), the tactic DISJ_CASES_TAC th can be used to produce a case split:
- DISJ_CASES_TAC th ([],Term`(P:num -> bool) m`); ([([`m = 0`], `P m`), ([`?n. m = SUC n`], `P m`)], fn) : tactic_result

- USES
- Performing a case analysis according to a disjunctive theorem.
- SEEALSO

HOL Kananaskis-14