`implicit_rewrites: unit -> rewrites`
SYNOPSIS
Contains a number of theorems used, by default, in rewriting.
LIBRARY
bool
STRUCTURE
DESCRIPTION
The variable implicit_rewrites holds a collection of rewrite rules commonly used to simplify expressions. These rules include the clause for reflexivity:
```   |- !x. (x = x) = T
```
as well as rules to reason about equality:
```   |- !t.
((T = t) = t) /\ ((t = T) = t) /\ ((F = t) = ~t) /\ ((t = F) = ~t)
```

Negations are manipulated by the following clauses:

```   |- (!t. ~~t = t) /\ (~T = F) /\ (~F = T)
```

The set of tautologies includes truth tables for conjunctions, disjunctions, and implications:

```   |- !t.
(T /\ t = t) /\
(t /\ T = t) /\
(F /\ t = F) /\
(t /\ F = F) /\
(t /\ t = t)
|- !t.
(T \/ t = T) /\
(t \/ T = T) /\
(F \/ t = t) /\
(t \/ F = t) /\
(t \/ t = t)
|- !t.
(T ==> t = t) /\
(t ==> T = T) /\
(F ==> t = T) /\
(t ==> t = T) /\
(t ==> F = ~t)
```

Simple rules for reasoning about conditionals are given by:

```   |- !t1 t2. ((T => t1 | t2) = t1) /\ ((F => t1 | t2) = t2)
```

Rewriting with the following tautologies allows simplification of universally and existentially quantified variables and abstractions:

```   |- !t. (!x. t) = t
|- !t. (?x. t) = t
|- !t1 t2. (\x. t1)t2 = t1
```

The value of implicit_rewrites can be augmented by add_implicit_rewrites and altered by set_implicit_rewrites.

The initial value of implicit_rewrites is bool_rewrites.

USES
The rewrite rules held in implicit_rewrites are automatically included in the simplifications performed by some of the rewriting tools.
SEEALSO