OR_CONV

reduceLib.OR_CONV : conv

Simplifies certain boolean disjunction expressions.

If tm corresponds to one of the forms given below, where t is an arbitrary term of type bool, then OR_CONV tm returns the corresponding theorem. Note that in the last case the disjuncts need only be alpha-equivalent rather than strictly identical.

   OR_CONV "T \/ t" = |- T \/ t = T
   OR_CONV "t \/ T" = |- t \/ T = T
   OR_CONV "F \/ t" = |- F \/ t = t
   OR_CONV "t \/ F" = |- t \/ F = t
   OR_CONV "t \/ t" = |- t \/ t = t

Failure

OR_CONV tm fails unless tm has one of the forms indicated above.

Example

#OR_CONV "F \/ T";;
|- F \/ T = T

#OR_CONV "X \/ F";;
|- X \/ F = X

#OR_CONV "(!n. n + 1 = SUC n) \/ (!m. m + 1 = SUC m)";;
|- (!n. n + 1 = SUC n) \/ (!m. m + 1 = SUC m) = (!n. n + 1 = SUC n)