Rewrite.implicit

`implicit_rewrites`

Rewrite.implicit_rewrites: unit -> rewrites

Contains a number of theorems used, by default, in rewriting.

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.

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

implicit_rewrites

See also

`implicit_rewrites`