BEQ_CONV

reduceLib.BEQ_CONV : conv

Simplifies certain expressions involving boolean equality.

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

   BEQ_CONV "T = t" = |- T = t = t
   BEQ_CONV "t = T" = |- t = T = t
   BEQ_CONV "F = t" = |- F = t = ~t
   BEQ_CONV "t = F" = |- t = F = ~t
   BEQ_CONV "t = t" = |- t = t = T

Failure

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

Example

#BEQ_CONV "T = T";;
|- (T = T) = T

#BEQ_CONV "F = T";;
|- (F = T) = F

#BEQ_CONV "(!x:*#**. x = (FST x,SND x)) = (!y:*#**. y = (FST y,SND y))";;
|- ((!x. x = FST x,SND x) = (!y. y = FST y,SND y)) = T