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