NOT_CONV
reduceLib.NOT_CONV : conv
Simplifies certain boolean negation expressions.
If tm corresponds to one of the forms given below, where t is an
arbitrary term of type bool, then NOT_CONV tm returns the
corresponding theorem.
NOT_CONV "~F" = |- ~F = T
NOT_CONV "~T" = |- ~T = F
NOT_CONV "~~t" = |- ~~t = t
Failure
NOT_CONV tm fails unless tm has one of the forms indicated above.
Example
#NOT_CONV "~~~~T";;
|- ~~~~T = ~~T
#NOT_CONV "~~T";;
|- ~~T = T
#NOT_CONV "~T";;
|- ~T = F