1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
|
\DOC basic_rewrites
\TYPE {basic_rewrites: thm list}
\SYNOPSIS
Contains a number of built-in tautologies used, by default, in rewriting.
\DESCRIBE
The variable {basic_rewrites} contains polymorphic tautologies which
are often used for simplifying and solving a goal through rewriting.
They include the clause for reflexivity:
{
|- !x. (x = x) = T;
}
\noindent 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 list {basic_rewrites} also includes rules for reasoning about
pairs in HOL:
{
|- !x. FST x,SND x = x;
|- !x y. FST(x,y) = x;
|- !x y. SND(x,y) = y]
}
\USES
The {basic_rewrites} are included in the set of equations used by some
of the rewriting tools.
\SEEALSO
ABS_SIMP, AND_CLAUSES, COND_CLAUSES, EQ_CLAUSES, EXISTS_SIMP,
FORALL_SIMP, FST, GEN_REWRITE_RULE, GEN_REWRITE_TAC, IMP_CLAUSES,
NOT_CLAUSES, OR_CLAUSES, PAIR, REFL_CLAUSE, REWRITE_RULE, REWRITE_TAC,
SND.
\ENDDOC
|
