Thm_cont.X_CASES

STRUCTURE

SYNOPSIS

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

DESCRIPTION

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

DISJ_CASES_THENL, X_CASES_THENL, X_CHOOSE_THEN