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))";;
|- (!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)";;
|- (!p. (!m. m >= p) = (p = 0)) =
   (!p m. ?m'. (m' >= p ==> (p = 0)) /\ ((p = 0) ==> m >= p))

#PRENEX_CONV "!m. (((m = 0) ==> (!n. m <= n)) => 0 | m) + m = m";;
|- (!m. (((m = 0) ==> (!n. m <= n)) => 0 | m) + m = m) =
   (!m. ((!n. (m = 0) ==> m <= n) => 0 | m) + m = m)
USES
Useful as a preprocessor to decision procedures which require their argument formula to be in prenex normal form.
SEEALSO
is_prenex
HOL  Kananaskis-8