bool_rewrites: rewrites
STRUCTURE
SYNOPSIS
Contains a number of basic equalities useful in rewriting.
DESCRIPTION
The variable bool_rewrites is a basic collection of rewrite rules useful in expression simplification. The current collection is
   - bool_rewrites;

   > val it =
       |- (x = x) = T;  |- (T = t) = t;  |- (t = T) = t;  |- (F = t) = ~t;
       |- (t = F) = ~t;  |- ~~t = t;  |- ~T = F;  |- ~F = T;  |- T /\ t = t;
       |- t /\ T = t;  |- F /\ t = F;  |- t /\ F = F;  |- t /\ t = t;
       |- T \/ t = T;  |- t \/ T = T;  |- F \/ t = t;  |- t \/ F = t;
       |- t \/ t = t;  |- T ==> t = t;  |- t ==> T = T;  |- F ==> t = T;
       |- t ==> t = T;  |- t ==> F = ~t;  |- (if T then t1 else t2) = t1;
       |- (if F then t1 else t2) = t2;  |- (!x. t) = t;  |- (?x. t) = t;
       |- (\x. t1) t2 = t1
       Number of rewrite rules = 28
        : rewrites

USES
The contents of bool_rewrites provide a standard basis upon which to build bespoke rewrite rule sets for use by the functions in Rewrite.
SEEALSO
HOL  Kananaskis-13