DISJ_CASES : (thm -> thm -> thm -> thm)
STRUCTURE
Thm
SYNOPSIS
Eliminates disjunction by cases.
DESCRIPTION
The rule DISJ_CASES takes a disjunctive theorem, and two ‘case’ theorems, each with one of the disjuncts as a hypothesis while sharing alpha-equivalent conclusions. A new theorem is returned with the same conclusion as the ‘case’ theorems, and the union of all assumptions excepting the disjuncts. 
    A |- t1 \/ t2     A1 u {t1} |- t      A2 u {t2} |- t
   ------------------------------------------------------  DISJ_CASES
                    A u A1 u A2 |- t

FAILURE
Fails if the first argument is not a disjunctive theorem, or if the conclusions of the other two theorems are not alpha-convertible.
EXAMPLE
Specializing the built-in theorem num_CASES gives the theorem: 
   th = |- (m = 0) \/ (?n. m = SUC n)
Using two additional theorems, each having one disjunct as a hypothesis: 
   th1 = (m = 0 |- (PRE m = m) = (m = 0))
   th2 = (?n. m = SUC n" |- (PRE m = m) = (m = 0))
a new theorem can be derived: 
   - DISJ_CASES th th1 th2;
   > val it = |- (PRE m = m) = (m = 0) : thm

COMMENTS
Neither of the ‘case’ theorems is required to have either disjunct as a hypothesis, but otherwise DISJ_CASES is pointless.
SEEALSO
DISJ_CASES_TAC, DISJ_CASES_THEN, DISJ_CASES_THEN2, DISJ_CASES_UNION, DISJ1, DISJ2
HOL  Kananaskis-10