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:as well as rules to reason about equality:
|- !x. (x = x) = T

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

HOL Kananaskis-14