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-14