`STRUCT_CASES_TAC : thm_tactic`

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 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 `~(l:(A)list = []) ==> LENGTH l > 0`;;
```
then we can get rid of the universal quantifier from the inbuilt list theorem list_CASES:
```   list_CASES = !l. l = [] \/ (?h t. l = CONS h t)
```
and then use STRUCT_CASES_TAC. This amounts to applying the following tactic:
```  # e(STRUCT_CASES_TAC (SPEC_ALL list_CASES));;
val it : goalstack = 2 subgoals (2 total)

`~(CONS h t = []) ==> LENGTH (CONS h t) > 0`

`~([] = []) ==> LENGTH [] > 0`
```
and both of these are solvable by REWRITE_TAC[GT; LENGTH; LT_0].

USES
Generating a case split from the axioms specifying a structure.