PSKOLEM_CONV : conv
STRUCTURE
PairRules
LIBRARY
pair
SYNOPSIS
Proves the existence of a pair of Skolem functions.
DESCRIPTION
When applied to an argument of the form !p1...pn. ?q. tm, the conversion PSKOLEM_CONV returns the theorem: 
   |- (!p1...pn. ?q. tm) = (?q'. !p1...pn. tm[q' p1 ... pn/yq)
where q' is a primed variant of the pair q not free in the input term.
FAILURE
PSKOLEM_CONV tm fails if tm is not a term of the form !p1...pn. ?q. tm.
EXAMPLE
Both q and any pi may be a paired structure of variables: 
   - PSKOLEM_CONV
      (Term `!(x11:'a,x12:'a) (x21:'a,x22:'a).
             ?(y1:'a,y2:'a). tm x11 x12 x21 x21 y1 y2`);

   > val it =
    |- (!(x11,x12) (x21,x22). ?(y1,y2). tm x11 x12 x21 x21 y1 y2) =
       ?(y1,y2).
         !(x11,x12) (x21,x22).
           tm x11 x12 x21 x21 (y1 (x11,x12) (x21,x22)) (y2 (x11,x12) (x21,x22))
     : thm

SEEALSO
SKOLEM_CONV, P_PSKOLEM_CONV
HOL  Kananaskis-14