DISJ_CASES

Thm.DISJ_CASES : (thm -> thm -> thm -> thm)

Eliminates disjunction by cases.

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:

   > val disj_th = SPEC “m:num” arithmeticTheory.num_CASES;
   val disj_th = ⊢ m = 0 ∨ ∃n. m = SUC n: thm

Using two additional theorems, each having one disjunct as a hypothesis:

   > show_assums := true;
   val it = (): unit
   > val th1 = EQT_ELIM $
       REWRITE_CONV [ASSUME “m = 0”, prim_recTheory.PRE] “PRE m = m ⇔ m = 0”;
   val th1 =  [m = 0] ⊢ PRE m = m ⇔ m = 0: thm

   > val th2_0 =
       REWRITE_CONV [ASSUME “m = SUC n”, prim_recTheory.PRE,
                     arithmeticTheory.SUC_NOT_ZERO,
                     GSYM prim_recTheory.SUC_ID]
                    “PRE m = m ⇔ m = 0”;
   val th2_0 =  [m = SUC n] ⊢ (PRE m = m ⇔ m = 0) ⇔ T: thm

   > val th2 = CHOOSE (“n:num”, ASSUME “∃n. m = SUC n”) (EQT_ELIM th2_0);
   val th2 =  [∃n. m = SUC n] ⊢ PRE m = m ⇔ m = 0: thm

a new theorem can be derived:

   > DISJ_CASES disj_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.

See also

Thm.CHOOSE, Tactic.DISJ_CASES_TAC, Thm_cont.DISJ_CASES_THEN, Thm_cont.DISJ_CASES_THEN2, Drule.DISJ_CASES_UNION, Thm.DISJ1, Thm.DISJ2