DISJ_CASES : thm -> thm -> thm -> 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 |- t      A2 |- t
   --------------------------------------------------  DISJ_CASES
         A u (A1 - {t1}) u (A2 - {t2}) |- t

FAILURE CONDITIONS

Fails if the first argument is not a disjunctive theorem, or if the conclusions of the other two theorems are not alpha-convertible.

EXAMPLE

Let us create several theorems. Note that th1 and th2 draw the same conclusion from different hypotheses, while th proves the disjunction of the two hypotheses:

  # let [th; th1; th2] = map (UNDISCH_ALL o REAL_FIELD)
      [`~(x = &0) \/ x = &0`;
       `~(x = &0) ==> x * (inv(x) * x - &1) = &0`;
       `x = &0 ==> x * (inv(x) * x - &1) = &0`];;
    ...
  val th : thm = |- ~(x = &0) \/ x = &0
  val th1 : thm = ~(x = &0) |- x * (inv x * x - &1) = &0
  val th2 : thm = x = &0 |- x * (inv x * x - &1) = &0

so we can apply DISJ_CASES:

  # DISJ_CASES th th1 th2;;
  val it : thm = |- x * (inv x * x - &1) = &0

COMMENTS

Neither of the `case' theorems is required to have either disjunct as a hypothesis, but otherwise DISJ_CASES is pointless.