DESTRUCT_TAC : string -> thm_tactic

SYNOPSIS

Performs elimination on a theorem within a tactic proof.

DESCRIPTION

Given a string s and a theorem th, DESTRUCT_TAC s th performs the elimination of th according with the pattern given in s. The syntax of the pattern s is the following:

An identifier l other than `_` and `+` assumes a hypothesis with label l
The identifier `_' does nothing (discard the hypothesis)
The identifier `+' adds the theorem as antecedent as with MP\_TAC
A sequence of patterns (separated by spaces) destructs a conjunction
A sequence of pattern separated by | destructs a disjunction
A prefix @x. introduces an existential

FAILURE CONDITIONS

Fails if the pattern is ill-formed or does not match the form of the theorem.

EXAMPLE

Here we use the cases theorem for numerals, performing a disjunctive split and introducing names for the resulting hypotheses:

  # let th = SPEC `n:num` (cases "num");;
  # g `n = 0 \/ (1 <= n /\ ?m. n = m + 1)`;;
  # e (DESTRUCT_TAC "neq0 | @m. neqsuc" th);;
  val it : goalstack = 2 subgoals (2 total)

    0 [`n = SUC m`] (neqsuc)

  `n = 0 \/ 1 <= n /\ (?m. n = m + 1)`

    0 [`n = 0`] (neq0)

  `n = 0 \/ 1 <= n /\ (?m. n = m + 1)`

Here we use the theorem

  # let th = SPEC `n+2` EVEN_EXISTS_LEMMA;;
  val th : thm =
    |- (EVEN (n + 2) ==> (?m. n + 2 = 2 * m)) /\
       (~EVEN (n + 2) ==> (?m. n + 2 = SUC (2 * m)))

\noindent adding as antecedent the right-hand side of the disjunction

  # g `!n. ~EVEN n ==> ?a. n + 2 = 2 * a + 1`;;
  # e (REPEAT STRIP_TAC THEN DESTRUCT_TAC "_ +" th);;

  val it : goalstack = 1 subgoal (1 total)

    0 [`~EVEN n`]

  `(~EVEN (n + 2) ==> (?m. n + 2 = SUC (2 * m))) ==> (?a. n + 2 = 2 * a + 1)`