STRUCT_CASES_THEN : thm_tactic -> thm_tactic

SYNOPSIS

Performs structural case analysis, applying theorem-tactic to results.

DESCRIPTION

When it is applied to a theorem-tactic ttac and a theorem th of the form:

   th = A' |- ?y11...y1m. x = t1 /\ (B11 /\ ... /\ B1k) \/ ... \/
              ?yn1...ynp. x = tn /\ (Bn1 /\ ... /\ Bnp)

in which there may be no existential quantifiers where a `vector' of them is shown above, STRUCT_CASES_THEN ttac th splits a goal A ?- s into n subgoals, where goal k results the initial goal by applying ttac to the theorem x = tn |- x = tn. That is, it performs a case split over the possible constructions (the ti) of a term and applies ttac to the resulting case assumptions. Note that unless A' is a subset of A, this is an invalid tactic.

FAILURE CONDITIONS

Fails unless the theorem has the above form, namely a conjunction of (possibly multiply existentially quantified) terms which assert the equality of the same variable x and the given terms.

EXAMPLE

Suppose we have the goal:

  # g `n > 0 ==> PRE(n) + 1 = n`;;

We can use the inbuilt theorem num_CASES to perform a case analysis on n, adding each case as a new assumption by ASSUME_TAC like this:

  # e(STRUCT_CASES_THEN ASSUME_TAC (SPEC `n:num` num_CASES));;
  val it : goalstack = 2 subgoals (2 total)

    0 [`n = SUC n'`]

  `n > 0 ==> PRE n + 1 = n`

    0 [`n = 0`]

  `n > 0 ==> PRE n + 1 = n`

USES

Generating a case split from the axioms specifying a structure.