1\DOC PairCases_on
2
3\TYPE {PairCases_on : term quotation -> tactic}
4
5\SYNOPSIS
6Recursively split variables of product type.
7
8\KEYWORDS
9tactic
10
11\LIBRARY
12pairTools
13
14\DESCRIBE
15An application {PairCases_on q} first parses {q} in the context of the goal to
16obtain {v}, which should be a variable of product type. Then, it introduces
17new variables of the form {v}n, where n is a number, representing the atomic
18components of {v} after all nested pair structure is expanded away. Finally,
19all occurrences of {v} in the goal (including in the assumptions) are replaced
20by the explicit pair structure (with the new variables at its leaves).
21
22The new variables are numbered from zero according to a depth-first traversal.
23(Therefore, they should appear in increasing order from left to right when the
24tree is pretty-printed.) Primed variants of the new numbered variables are used
25if necessary (i.e. {v}n already occurs free in the goal).
26
27\FAILURE
28Fails if {v} is not a variable of product type.
29
30\EXAMPLE
31> val PairCases_on = pairLib.PairCases_on;
32> g(`(x = y) ==> ((x:((bool#bool)#bool#(bool#((bool#bool)#bool))))=z)`);
33
34     Initial goal:
35
36     (x = y) ==> (x = z)
37
38> e(DISCH_TAC);
39OK..
401 subgoal:
41
42x = z
43------------------------------------
44  x = y
45
46> e(PairCases_on `y`);
47OK..
481 subgoal:
49
50x = z
51------------------------------------
52  x = ((y0,y1),y2,y3,(y4,y5),y6)
53
54> e(PairCases_on`x`);
55OK..
561 subgoal:
57
58((x0,x1),x2,x3,(x4,x5),x6) = z
59------------------------------------
60  ((x0,x1),x2,x3,(x4,x5),x6) = ((y0,y1),y2,y3,(y4,y5),y6)
61
62\SEEALSO
63Tactic.FULL_STRUCT_CASES_TAC, Conv.RENAME_VARS_CONV.
64
65\ENDDOC
66