COND_REWR_CANON : thm -> thm
STRUCTURE
SYNOPSIS
Transform a theorem into a form accepted by COND_REWR_TAC.
DESCRIPTION
COND_REWR_CANON transforms a theorem into a form accepted by COND_REWR_TAC. The input theorem should be an implication of the following form
   !x1 ... xn. P1[xi] ==> ... ==> !y1 ... ym. Pr[xi,yi] ==>
     (!z1 ... zk. u[xi,yi,zi] = v[xi,yi,zi])
where each antecedent Pi itself may be a conjunction or disjunction. The output theorem will have all universal quantifications moved to the outer most level with possible renaming to prevent variable capture, and have all antecedents which are a conjunction transformed to implications. The output theorem will be in the following form
   !x1 ... xn y1 ... ym z1 ... zk. 
    P11[xi] ==> ... ==> P1p[xi] ==> ... ==>
     Pr1[xi,yi] ==> ... ==> Prq[x1,yi] ==> (u[xi,yi,zi] = v[xi,yi,zi])
FAILURE
This function fails if the input theorem is not in the correct form.
EXAMPLE
COND_REWR_CANON transforms the built-in theorem CANCL_SUB into the form for conditional rewriting:
   #COND_REWR_CANON CANCEL_SUB;;
   Theorem CANCEL_SUB autoloading from theory `arithmetic` ...
   CANCEL_SUB = |- !p n m. p <= n /\ p <= m ==> ((n - p = m - p) = (n = m))

   |- !p n m. p <= n ==> p <= m ==> ((n - p = m - p) = (n = m))
SEEALSO
HOL  Kananaskis-10