COND_ELIM_CONV : conv
STRUCTURE
Arith
SYNOPSIS
Eliminates conditional statements from a formula.
DESCRIPTION
This function moves conditional statements up through a term and if at any point the branches of the conditional become Boolean-valued the conditional is eliminated. If the term is a formula, only an abstraction can prevent a conditional being moved up far enough to be eliminated.
FAILURE
Never fails.
EXAMPLE
#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)))

#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))
USES
Useful as a preprocessor to decision procedures which do not allow conditional statements in their argument formula.
SEEALSO
SUB_AND_COND_ELIM_CONV
HOL  Kananaskis-14