COND_CONV : conv
STRUCTURE
reduceLib
SYNOPSIS
Simplifies certain conditional expressions.
LIBRARY
reduce
DESCRIPTION
If tm corresponds to one of the forms given below, where b has type bool and t1 and t2 have the same type, then COND_CONV tm returns the corresponding theorem. Note that in the last case the arms need only be alpha-equivalent rather than strictly identical. 
   COND_CONV "F => t1 | t2" = |- (T => t1 | t2) = t2
   COND_CONV "T => t1 | t2" = |- (T => t1 | t2) = t1
   COND_CONV "b => t | t    = |- (b => t | t) = t
FAILURE
COND_CONV tm fails unless tm has one of the forms indicated above.
EXAMPLE
#COND_CONV "F => F | T";;
|- (F => F | T) = T

#COND_CONV "T => F | T";;
|- (T => F | T) = F

#COND_CONV "b => (\x. SUC x) | (\p. SUC p)";;
|- (b => (\x. SUC x) | (\p. SUC p)) = (\x. SUC x)
HOL  Trindemossen-1