COND_CONV : conv

- STRUCTURE
- 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 Kananaskis-14