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.