DISJ_CASES_TAC : thm_tactic

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 CONDITIONS
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:
  # let th = SPEC `m:num` num_CASES;;
  val th : thm = |- m = 0 \/ (?n. m = SUC n)

  # g `(P:num -> bool) m`;;
  Warning: Free variables in goal: P, m
  val it : goalstack = 1 subgoal (1 total)

  `P m`

  # e(DISJ_CASES_TAC th);;
  val it : goalstack = 2 subgoals (2 total)

   0 [`?n. m = SUC n`]

  `P m`

   0 [`m = 0`]

  `P m`

USES
Performing a case analysis according to a disjunctive theorem.

SEE ALSO
ASSUME_TAC, ASM_CASES_TAC, COND_CASES_TAC, DISJ_CASES_THEN, STRUCT_CASES_TAC.