DISJ_CASES_THEN : thm_tactical

SYNOPSIS
Applies a theorem-tactic to each disjunct of a disjunctive theorem.

DESCRIPTION
If the theorem-tactic f:thm->tactic applied to either ASSUMEd disjunct produces results as follows when applied to a goal (A ?- t):
    A ?- t                                A ?- t
   =========  f (u |- u)      and        =========  f (v |- v)
    A ?- t1                               A ?- t2
then applying DISJ_CASES_THEN f (|- u \/ v) to the goal (A ?- t) produces two subgoals.
           A ?- t
   ======================  DISJ_CASES_THEN f (|- u \/ v)
    A ?- t1      A ?- t2

FAILURE CONDITIONS
Fails if the theorem is not a disjunction. An invalid tactic is produced if the theorem has any hypothesis which is not alpha-convertible to an assumption of the goal.

EXAMPLE
Given the theorem
   th = |- (m = 0) \/ (?n. m = SUC n)
and a goal of the form ?- (PRE m = m) = (m = 0), applying the tactic
   DISJ_CASES_THEN MP_TAC th
produces two subgoals, each with one disjunct as an added antecedent
  # let th = SPEC `m:num` num_CASES;;
  val th : thm = |- m = 0 \/ (?n. m = SUC n)
  # g `PRE m = m <=> m = 0`;;
  Warning: Free variables in goal: m
  val it : goalstack = 1 subgoal (1 total)

  `PRE m = m <=> m = 0`

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

  `(?n. m = SUC n) ==> (PRE m = m <=> m = 0)`

  `m = 0 ==> (PRE m = m <=> m = 0)`

USES
Building cases tactics. For example, DISJ_CASES_TAC could be defined by:
   let DISJ_CASES_TAC = DISJ_CASES_THEN ASSUME_TAC

COMMENTS
Use DISJ_CASES_THEN2 to apply different tactic generating functions to each case.

SEE ALSO
STRIP_THM_THEN, CHOOSE_THEN, CONJUNCTS_THEN, CONJUNCTS_THEN2, DISJ_CASES_TAC, DISJ_CASES_THEN2, DISJ_CASES_THENL.