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
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% FILE: pre.ml %
% EDITOR: Paul Curzon %
% DATE: July 1991 %
% DESCRIPTION : Theorems about PRE %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%********************************* HISTORY ********************************%
% %
% This file is based on the theories of %
% %
% Rachel Cardell-Oliver %
% Wim Ploegaerts %
% Wai Wong %
% %
%****************************************************************************%
% %
% PC 12/8/92 %
% The tactic for PRE_MONO_LESS_EQ has been changed to remove the %
% dependancy on the auxiliary library %
% %
% PC 21/4/93 %
% New theorem added: LESS_IMP_LESS_EQ_PRE %
% %
%****************************************************************************%
% %
% PC 21/4/93 %
% Removed dependencies on several external files/theories %
% Added extra theorems by Wai Wong %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%****************************************************************************%
% %
% DEPENDANCIES : %
% %
% %
%****************************************************************************%
system `rm -f pre.th`;;
new_theory `pre`;;
% PC 12/8/92 %
%load_library `auxiliary`;;%
% PC 22-4-92 These are no longer used%
%loadf (library_pathname() ^ `/group/start_groups`);;%
%new_parent `ineq`;;%
%loadf `tools`;;%
%autoload_defs_and_thms `ineq`;;%
%============================================================================%
% %
% Theorems dealing with PRE %
% %
%============================================================================%
%<WP>%
%New proof by PC 22-4-93%
let SUC_PRE = prove_thm (
`SUC_PRE`,
"!n . (0 < n) ==> ((SUC (PRE n)) = n)",
REPEAT STRIP_TAC THEN
(ACCEPT_TAC
(REWRITE_RULE[]
(MATCH_MP (SPECL["PRE n";"n:num"] PRE_SUC_EQ)
(ASSUME "0 < n") )))
);;
% IMP_RES_TAC (SPEC "PRE n" PRE_SUC_EQ) THEN%
% FIRST_ASSUM (\thm . SUBST_MATCH_TAC (GSYM thm) ? NO_TAC ) THEN%
% REFL_TAC%
%);;%
%<-------------------------------------------------------------------------->%
%<WP>%
let PRE_MONO = prove_thm (
`PRE_MONO`,
"! m n . (PRE m < PRE n) ==> (m < n)",
INDUCT_TAC THEN
INDUCT_TAC THEN
REWRITE_TAC [PRE;NOT_LESS_0;LESS_0;LESS_MONO]
);;
%<-------------------------------------------------------------------------->%
%<WP>%
let PRE_MONO_LESS_EQ = prove_thm (
`PRE_MONO_LESS_EQ`,
"! m n . (m < n) ==> (PRE m <= PRE n)",
% PC 12/8/92 Changed to remove the dependancy on the auxiliary library %
% (2 TIMES INDUCT_TAC) THEN %
INDUCT_TAC THEN INDUCT_TAC THEN
REWRITE_TAC [NOT_LESS_0;PRE;LESS_MONO_EQ;ZERO_LESS_EQ] THEN
DISCH_THEN \thm . REWRITE_TAC [LESS_OR_EQ;thm]
);;
%<-------------------------------------------------------------------------->%
%<WP>%
%< PRE_LESS_EQ = |- !n. (PRE n) <= n >%
let PRE_LESS_EQ = save_thm (
`PRE_LESS_EQ`,
GEN_ALL (REWRITE_RULE [PRE]
(MATCH_MP PRE_MONO_LESS_EQ (SPEC "n:num" LESS_SUC_REFL)))
);;
%<-------------------------------------------------------------------------->%
%<WP>%
let PRE_ADD = prove_thm (
`PRE_ADD`,
"!n m . (0 < n) ==> (PRE ( n + m ) = (PRE n) + m)",
INDUCT_TAC THEN
REWRITE_TAC [NOT_LESS_0;PRE;ADD_CLAUSES]
);;
%============================================================================%
% %
% relation SUC / PRE %
% %
%============================================================================%
%<WP>%
let SUC_LESS_PRE = prove_thm (
`SUC_LESS_PRE`,
"! m n . (SUC m < n) ==> (m < PRE n)",
GEN_TAC THEN
INDUCT_TAC THEN
REWRITE_TAC [NOT_LESS_0;PRE;LESS_MONO_EQ]
);;
%<-------------------------------------------------------------------------->%
%<WP>%
let SUC_LESS_EQ_PRE = prove_thm (
`SUC_LESS_EQ_PRE`,
"! m n . (0 < n) ==> (SUC m <= n) ==> (m <= PRE n)",
REPEAT GEN_TAC THEN
DISCH_THEN \thm . REWRITE_TAC [LESS_OR_EQ;MATCH_MP PRE_SUC_EQ thm] THEN
STRIP_TAC THEN
IMP_RES_TAC SUC_LESS_PRE THEN
ASM_REWRITE_TAC []
);;
%<-------------------------------------------------------------------------->%
%<WP>%
let PRE_K_K = prove_thm (
`PRE_K_K`,
"!k . (0<k) ==> (PRE k < k)",
INDUCT_THEN INDUCTION MP_TAC THEN
REWRITE_TAC [LESS_REFL;LESS_0;PRE;LESS_SUC_REFL]
);;
%****************************************************************************%
% %
% AUTHOR : Rachel Cardell-Oliver %
% DATE : 1990 %
% %
%****************************************************************************%
let NOT_LESS_SUB = PROVE
("!m n. ~( m < (m-n) )" ,
REPEAT GEN_TAC THEN
ASM_CASES_TAC "m<=n" THENL
[ POP_ASSUM(\thm. REWRITE_TAC[REWRITE_RULE[GSYM SUB_EQ_0]thm;NOT_LESS_0]);
% PC 12/8/92 NOT_LESS_EQ_LESS -> NOT_LESS_EQUAL %
% POP_ASSUM(ASSUME_TAC o REWRITE_RULE[NOT_LESS_EQ_LESS]) THEN %
POP_ASSUM(ASSUME_TAC o REWRITE_RULE[NOT_LESS_EQUAL]) THEN
IMP_RES_TAC LESS_IMP_LESS_OR_EQ THEN
IMP_RES_TAC SUB_ADD THEN
REWRITE_TAC[NOT_LESS] THEN
ONCE_REWRITE_TAC[GSYM(SPECL["m-n";"m:num";"n:num"]LESS_EQ_MONO_ADD_EQ)]
THEN ASM_REWRITE_TAC[LESS_EQ_ADD] ] );;
let PRE_LESS = prove_thm(`PRE_LESS`,
"!b:num. ( (0<b) /\ (b<a) ==> ((PRE b) < a))",
REPEAT STRIP_TAC THEN
ASSUME_TAC (REWRITE_RULE [NOT_LESS]
(SPECL ["b:num";"1"] NOT_LESS_SUB)) THEN
IMP_RES_TAC LESS_EQ_LESS_TRANS THEN
ASM_REWRITE_TAC[PRE_SUB1] );;
%****************************************************************************%
% %
% AUTHOR : Wai Wong %
% DATE : April 1993 %
% %
%****************************************************************************%
let LESS_IMP_LESS_EQ_PRE = prove_thm(`LESS_IMP_LESS_EQ_PRE`,
"!m n. 0 < n ==> ((m < n) = (m <= (PRE n)))",
REPEAT INDUCT_TAC THEN REWRITE_TAC[NOT_LESS_0] THENL[
DISCH_TAC THEN REWRITE_TAC[PRE;ZERO_LESS_EQ;LESS_0];
REWRITE_TAC[PRE;LESS_MONO_EQ] THEN STRIP_TAC
THEN MATCH_ACCEPT_TAC LESS_EQ]);;
close_theory();;
|
