PRENEX_CONV : conv
STRUCTURE
Arith
SYNOPSIS
Puts a formula into prenex normal form.
DESCRIPTION
This function puts a formula into prenex normal form, and in the process splits any Boolean equalities (if-and-only-if) into two implications. If there is a Boolean-valued subterm present as the condition of a conditional, the subterm will be put in prenex normal form, but quantifiers will not be moved out of the condition. Some renaming of variables may take place.
FAILURE
Never fails.
EXAMPLE
> PRENEX_CONV ``!m n. (m <= n) ==> !p. (m < SUC(n + p))``;
val it = |- (!m n. m <= n ==> (!p. m < (SUC(n + p)))) =
            (!m n p. m <= n ==> m < (SUC(n + p)))

> PRENEX_CONV ``!p. (!m. m >= p) = (p = 0)``;
val it = |- (!p. (!m. m >= p) = (p = 0)) =
            (!p m. ?m'. (m' >= p ==> (p = 0)) /\ ((p = 0) ==> m >= p))
USES
Useful as a preprocessor to decision procedures which require their argument formula to be in prenex normal form.
SEEALSO
is_prenex
HOL  Trindemossen-1