NEGATE_CONV
Arith.NEGATE_CONV : (conv -> conv)
Function for negating the operation of a conversion that proves a formula to be either true or false.
This function negates the operation of a conversion that proves a
formula to be either true or false. For example, if conv proves "t"
to be equal to "T" then NEGATE_CONV conv will prove "~t" to be
"F".
Failure
Fails if the application of the conversion to the negation of the
formula does not yield either "T" or "F".
Example
> Arith.ARITH_CONV “!n. 0 <= n”;
val it = ⊢ (∀n. 0 ≤ n) ⇔ T: thm
> Arith.NEGATE_CONV Arith.ARITH_CONV “~(!n. 0 <= n)”;
val it = ⊢ ¬(∀n. 0 ≤ n) ⇔ F: thm
> Arith.NEGATE_CONV Arith.ARITH_CONV “∃n. ~(0 <= n)”;
val it = ⊢ (∃n. ¬(0 ≤ n)) ⇔ F: thm