IMP_CONV : conv

- STRUCTURE
- SYNOPSIS
- Simplifies certain implicational expressions.
- LIBRARY
- reduce
- DESCRIPTION
- If tm corresponds to one of the forms given below, where t is an arbitrary term of type bool, then IMP_CONV tm returns the corresponding theorem. Note that in the last case the antecedent and consequent need only be alpha-equivalent rather than strictly identical.
IMP_CONV "T ==> t" = |- T ==> t = t IMP_CONV "t ==> T" = |- t ==> T = T IMP_CONV "F ==> t" = |- F ==> t = T IMP_CONV "t ==> F" = |- t ==> F = ~t IMP_CONV "t ==> t" = |- t ==> t = T

- FAILURE
- IMP_CONV tm fails unless tm has one of the forms indicated above.
- EXAMPLE
#IMP_CONV "T ==> F";; |- T ==> F = F #IMP_CONV "F ==> x";; |- F ==> x = T #IMP_CONV "(!z:(num)list. z = z) ==> (!x:(num)list. x = x)";; |- (!z. z = z) ==> (!x. x = x) = T

HOL Kananaskis-14