basic_rewrites : unit -> thm list
Returns the set of built-in theorems used, by default, in rewriting.
The list of theorems returned by basic_rewrites() is applied by default in
rewriting conversions, rules and tactics such as ONCE_REWRITE_CONV,
REWRITE_RULE and SIMP_TAC, though not in the `pure' variants like
PURE_REWRITE_TAC. This default set can be modified using
extend_basic_rewrites, set_basic_rewrites. Other conversions, not
necessarily expressible as rewriting with a theorem, can be added using
set_basic_convs and extend_basic_convs and examined by basic_convs.
The following shows the list of default rewrites in the standard HOL Light
state. Most of them are basic logical tautologies.
val it : thm list =
[|- FST (x,y) = x; |- SND (x,y) = y; |- FST x,SND x = x;
|- (if x = x then y else z) = y; |- (if T then t1 else t2) = t1;
|- (if F then t1 else t2) = t2; |- ~ ~t <=> t; |- ~T <=> F; |- ~F <=> T;
|- (@y. y = x) = x; |- x = x <=> T; |- (T <=> t) <=> t;
|- (t <=> T) <=> t; |- (F <=> t) <=> ~t; |- (t <=> F) <=> ~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;
|- (!x. t) <=> t; |- (?x. t) <=> t; |- (\x. f x) y = f y;
|- x = x ==> p <=> p]
The basic_rewrites are included in the set of equations used by some
of the rewriting tools.
- SEE ALSO
extend_basic_rewrites, set_basic_rewrites, set_basic_convs, extend_basic_convs,
basic_convs, REWRITE_CONV, REWRITE_RULE, REWRITE_TAC, SIMP_CONV, SIMP_RULE,