STRUCT_CASES_TAC : thm_tactic
STRUCTURE
SYNOPSIS
Performs very general structural case analysis.
DESCRIPTION
When it is applied to a theorem 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_TAC th splits a goal A ?- s into n subgoals as follows:
                             A ?- s
   ===============================================================
    A u {B11,...,B1k} ?- s[t1/x] ... A u {Bn1,...,Bnp} ?- s[tn/x]
that is, performs a case split over the possible constructions (the ti) of a term, providing as assumptions the given constraints, having split conjoined constraints into separate assumptions. Note that unless A' is a subset of A, this is an invalid tactic.
FAILURE
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:
  ?- ~(l:(*)list = []) ==> (LENGTH l) > 0
then we can get rid of the universal quantifier from the inbuilt list theorem list_CASES:
   list_CASES = !l. (l = []) \/ (?t h. l = CONS h t)
and then use STRUCT_CASES_TAC. This amounts to applying the following tactic:
   STRUCT_CASES_TAC (SPEC_ALL list_CASES)
which results in the following two subgoals:
   ?- ~(CONS h t = []) ==> (LENGTH(CONS h t)) > 0

   ?- ~([] = []) ==> (LENGTH[]) > 0
Note that this is a rather simple case, since there are no constraints, and therefore the resulting subgoals have no assumptions.
USES
Generating a case split from the axioms specifying a structure.
SEEALSO
HOL  Kananaskis-14