SUB_AND_COND_ELIM_CONVArith.SUB_AND_COND_ELIM_CONV : convEliminates natural number subtraction, PRE, and conditional statements from a formula.
This function eliminates natural number subtraction and the
predecessor function, PRE, from a formula, but in doing so
may generate conditional statements, so these are eliminated too. The
conditional statements are moved up through the term and if at any point
the branches of the conditional become Boolean-valued the conditional is
eliminated. Subtraction operators are moved up until a relation (such as
less-than) is reached. The subtraction can then be transformed into an
addition. Provided the argument term is a formula, only an abstraction
can prevent a conditional being moved up far enough to be eliminated. If
the term is not a formula it may not be possible to eliminate the
subtraction. The function is also incapable of eliminating subtractions
that appear in arguments to functions other than the standard operators
of arithmetic.
The function is not as delicate as it could be; it tries to eliminate all conditionals in a formula when it need only eliminate those that have to be removed in order to eliminate subtraction.
Never fails.
#SUB_AND_COND_ELIM_CONV
# "((p + 3) <= n) ==> (!m. ((m = 0) => (n - 1) | (n - 2)) > p)";;
|- (p + 3) <= n ==> (!m. ((m = 0) => n - 1 | n - 2) > p) =
(p + 3) <= n ==>
(!m. (~(m = 0) \/ n > (1 + p)) /\ ((m = 0) \/ n > (2 + p)))
#SUB_AND_COND_ELIM_CONV
# "!f n. f ((SUC n = 0) => 0 | (SUC n - 1)) < (f n) + 1";;
|- (!f n. (f((SUC n = 0) => 0 | (SUC n) - 1)) < ((f n) + 1)) =
(!f n.
(~(SUC n = 0) \/ (f 0) < ((f n) + 1)) /\
((SUC n = 0) \/ (f((SUC n) - 1)) < ((f n) + 1)))
#SUB_AND_COND_ELIM_CONV
# "!f n. (\m. f ((m = 0) => 0 | (m - 1))) (SUC n) < (f n) + 1";;
|- (!f n. ((\m. f((m = 0) => 0 | m - 1))(SUC n)) < ((f n) + 1)) =
(!f n. ((\m. ((m = 0) => f 0 | f(m - 1)))(SUC n)) < ((f n) + 1))Useful as a preprocessor to decision procedures which do not allow natural number subtraction in their argument formula.