----------------------------------------------------------------------
PairCases_on                                                 (pairLib)
----------------------------------------------------------------------
PairCases_on : term quotation -> tactic

SYNOPSIS
Recursively split variables of product type.

KEYWORDS
tactic

LIBRARY
pairTools

DESCRIBE
An application {PairCases_on q} first parses {q} in the context of the goal to
obtain {v}, which should be a variable of product type. Then, it introduces
new variables of the form {v}n, where n is a number, representing the atomic
components of {v} after all nested pair structure is expanded away. Finally,
all occurrences of {v} in the goal (including in the assumptions) are replaced
by the explicit pair structure (with the new variables at its leaves).

The new variables are numbered from zero according to a depth-first traversal.
(Therefore, they should appear in increasing order from left to right when the
tree is pretty-printed.) Primed variants of the new numbered variables are used
if necessary (i.e. {v}n already occurs free in the goal).

FAILURE
Fails if {v} is not a variable of product type.

EXAMPLE
> val PairCases_on = pairLib.PairCases_on;
> g(‘(x = y) ==> ((x:((bool#bool)#bool#(bool#((bool#bool)#bool))))=z)‘);

Initial goal:

(x = y) ==> (x = z)

> e(DISCH_TAC);
OK..
1 subgoal:

x = z
------------------------------------
  x = y

> e(PairCases_on ‘y‘);
OK..
1 subgoal:

x = z
------------------------------------
  x = ((y0,y1),y2,y3,(y4,y5),y6)

> e(PairCases_on‘x‘);
OK..
1 subgoal:

((x0,x1),x2,x3,(x4,x5),x6) = z
------------------------------------
  ((x0,x1),x2,x3,(x4,x5),x6) = ((y0,y1),y2,y3,(y4,y5),y6)

SEEALSO
Tactic.FULL_STRUCT_CASES_TAC, Conv.RENAME_VARS_CONV.

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