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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
%****************************************************************************%
% FILE : theorems.ml %
% DESCRIPTION : Theorems for arithmetic formulae. %
% %
% READS FILES : <none> %
% WRITES FILES : <none> %
% %
% AUTHOR : R.J.Boulton %
% DATE : 4th March 1991 %
% %
% LAST MODIFIED : R.J.Boulton %
% DATE : 8th October 1992 %
%****************************************************************************%
%============================================================================%
% Theorems for normalizing arithmetic %
%============================================================================%
%----------------------------------------------------------------------------%
% ONE_PLUS = |- !n. SUC n = 1 + n %
%----------------------------------------------------------------------------%
ONE_PLUS := theorem `arithmetic` `SUC_ONE_ADD`;;
%----------------------------------------------------------------------------%
% ZERO_PLUS = |- !m. 0 + m = m %
%----------------------------------------------------------------------------%
ZERO_PLUS := GEN_ALL (el 1 (CONJUNCTS (theorem `arithmetic` `ADD_CLAUSES`)));;
%----------------------------------------------------------------------------%
% PLUS_ZERO = |- !m. m + 0 = m %
%----------------------------------------------------------------------------%
PLUS_ZERO := GEN_ALL (el 2 (CONJUNCTS (theorem `arithmetic` `ADD_CLAUSES`)));;
%----------------------------------------------------------------------------%
% SUC_ADD1 = |- !m n. SUC (m + n) = (SUC m) + n %
%----------------------------------------------------------------------------%
SUC_ADD1 :=
GEN_ALL (SYM (el 3 (CONJUNCTS (theorem `arithmetic` `ADD_CLAUSES`))));;
%----------------------------------------------------------------------------%
% SUC_ADD2 = |- !m n. SUC (m + n) = (SUC n) + m %
%----------------------------------------------------------------------------%
SUC_ADD2 := theorem `arithmetic` `SUC_ADD_SYM`;;
%----------------------------------------------------------------------------%
% ZERO_MULT = |- !m. 0 * m = 0 %
% MULT_ZERO = |- !m. m * 0 = 0 %
% ONE_MULT = |- !m. 1 * m = m %
% MULT_ONE = |- !m. m * 1 = m %
% MULT_SUC = |- !m n. (SUC m) * n = (m * n) + n %
%----------------------------------------------------------------------------%
[ZERO_MULT;MULT_ZERO;ONE_MULT;MULT_ONE;MULT_SUC] :=
map GEN_ALL
(butlast (CONJUNCTS (SPEC_ALL (theorem `arithmetic` `MULT_CLAUSES`))));;
%----------------------------------------------------------------------------%
% MULT_COMM = |- !m n. (m * n) = (n * m) %
%----------------------------------------------------------------------------%
MULT_COMM := theorem `arithmetic` `MULT_SYM`;;
%----------------------------------------------------------------------------%
% SUC_ADD_LESS_EQ_F = |- !m n. ((SUC(m + n)) <= m) = F %
%----------------------------------------------------------------------------%
SUC_ADD_LESS_EQ_F :=
GEN_ALL (EQF_INTRO (SPEC_ALL (theorem `arithmetic` `NOT_SUC_ADD_LESS_EQ`)));;
%----------------------------------------------------------------------------%
% MULT_LEQ_SUC = |- !m n p. m <= n = ((SUC p) * m) <= ((SUC p) * m) %
%----------------------------------------------------------------------------%
MULT_LEQ_SUC := theorem `arithmetic` `MULT_LESS_EQ_SUC`;;
%----------------------------------------------------------------------------%
% ZERO_LESS_EQ_T = |- !n. (0 <= n) = T %
%----------------------------------------------------------------------------%
ZERO_LESS_EQ_T :=
GEN_ALL (EQT_INTRO (SPEC_ALL (theorem `arithmetic` `ZERO_LESS_EQ`)));;
%----------------------------------------------------------------------------%
% SUC_LESS_EQ_ZERO_F = |- !n. ((SUC n) <= 0) = F %
%----------------------------------------------------------------------------%
SUC_LESS_EQ_ZERO_F :=
GEN_ALL (EQF_INTRO (SPEC_ALL (theorem `arithmetic` `NOT_SUC_LESS_EQ_0`)));;
%----------------------------------------------------------------------------%
% ZERO_LESS_EQ_ONE_TIMES = |- !n. 0 <= (1 * n) %
%----------------------------------------------------------------------------%
ZERO_LESS_EQ_ONE_TIMES :=
GEN_ALL
(SUBS [SYM (el 3 (CONJUNCTS (SPECL ["n:num";"m:num"]
(theorem `arithmetic` `MULT_CLAUSES`))))]
(SPEC_ALL (theorem `arithmetic` `ZERO_LESS_EQ`)));;
%----------------------------------------------------------------------------%
% LESS_EQ_PLUS = |- !m n. m <= (m + n) %
%----------------------------------------------------------------------------%
LESS_EQ_PLUS := theorem `arithmetic` `LESS_EQ_ADD`;;
%----------------------------------------------------------------------------%
% LESS_EQ_TRANSIT = |- !m n p. m <= n /\ n <= p ==> m <= p %
%----------------------------------------------------------------------------%
LESS_EQ_TRANSIT := theorem `arithmetic` `LESS_EQ_TRANS`;;
%============================================================================%
% Theorems for manipulating Boolean expressions %
%============================================================================%
%----------------------------------------------------------------------------%
% NOT_T_F = |- ~T = F %
%----------------------------------------------------------------------------%
NOT_T_F := el 2 (CONJUNCTS NOT_CLAUSES);;
%----------------------------------------------------------------------------%
% NOT_F_T = |- ~F = T %
%----------------------------------------------------------------------------%
NOT_F_T := el 3 (CONJUNCTS NOT_CLAUSES);;
|
