----------------------------------------------------------------------
X_CASES_THEN                                                (Thm_cont)
----------------------------------------------------------------------
X_CASES_THEN : term list list -> thm_tactical

SYNOPSIS
Applies a theorem-tactic to all disjuncts of a theorem, choosing witnesses.

KEYWORDS
theorem-tactic, cases, disjunction, quantifier, existential.

DESCRIBE
Let {[yl1,...,yln]} represent a list of variable lists,
each of length zero or more, and {xl1,...,xln} each represent a
vector of zero or more variables, so that the variables in each of
{yl1...yln} have the same types as the corresponding {xli}.
{X_CASES_THEN} expects such a list of variable lists, {[yl1,...,yln]}, a tactic
generating function {f:thm->tactic}, and a disjunctive theorem,
where each disjunct may be existentially quantified:

   th = |-(?xl1.B1)  \/...\/  (?xln.Bn)

each disjunct having the form {(?xi1 ... xim. Bi)}. If
applying {f} to the theorem obtained by introducing witness variables {yli}
for the objects {xli} whose existence is asserted by each disjunct, typically
{({Bi[yli/xli]} |- Bi[yli/xli])}, produce the following results when
applied to a goal {(A ?- t)}:

    A ?- t
   ========= f ({B1[yl1/xl1]} |- B1[yl1/xl1])
    A ?- t1

    ...

    A ?- t
   =========  f ({Bn[yln/xln]} |- Bn[yln/xln])
    A ?- tn

then applying {(X_CHOOSE_THEN [yl1,...,yln] f th)}
to the goal {(A ?- t)} produces {n} subgoals.

           A ?- t
   =======================  X_CHOOSE_THEN [yl1,...,yln] f th
    A ?- t1  ...  A ?- tn




FAILURE
Fails (with {X_CHOOSE_THEN}) if any {yli} has more variables than the
corresponding {xli}, or (with {SUBST}) if corresponding variables have
different types.  Failures may arise in the tactic-generating
function.  An invalid tactic is produced if any variable in any of the
{yli} is free in the corresponding {Bi} or in {t}, or if the theorem
has any hypothesis which is not alpha-convertible to an assumption of
the goal.

EXAMPLE
Given the goal {?- (x MOD 2) <= 1}, the following theorem may be
used to split into 2 cases:

   th = |- (?m. x = 2 * m) \/ (?m. x = (2 * m) + 1)

by the tactic

   X_CASES_THEN [[Term`n:num`],[Term`n:num]] ASSUME_TAC th

to produce the subgoals:

   {x = (2 * n) + 1} ?- (x MOD 2) <= 1

   {x = 2 * n} ?- (x MOD 2) <= 1




SEEALSO
Thm_cont.DISJ_CASES_THENL, Thm_cont.X_CASES_THENL,
Thm_cont.X_CHOOSE_THEN.

----------------------------------------------------------------------