bool_EQ_CONV

Conv.bool_EQ_CONV : conv

Simplifies expressions involving boolean equality.

The conversion bool_EQ_CONV simplifies equations of the form t1 = t2, where t1 and t2 are of type bool. When applied to a term of the form t = t, the conversion bool_EQ_CONV returns the theorem

   |- (t = t) = T

When applied to a term of the form t = T, the conversion returns

   |- (t = T) = t

And when applied to a term of the form T = t, it returns

   |- (T = t) = t

Failure

Fails unless applied to a term of the form t1 = t2, where t1 and t2 are boolean, and either t1 and t2 are syntactically identical terms or one of t1 and t2 is the constant T.

Example

> bool_EQ_CONV (Parse.Term `T = F`);
val it = ⊢ (T ⇔ F) ⇔ F: thm

> bool_EQ_CONV (Parse.Term `(0 < n) = T`);
val it = ⊢ (0 < n ⇔ T) ⇔ 0 < n: thm