65 qed ""; |
65 qed ""; |
66 |
66 |
67 Goal "(#1234567::real) <= #1234567"; |
67 Goal "(#1234567::real) <= #1234567"; |
68 by (Simp_tac 1); |
68 by (Simp_tac 1); |
69 qed ""; |
69 qed ""; |
|
70 |
|
71 (** Tests **) |
|
72 Goal "(x + y = x) = (y = (#0::real))"; |
|
73 by(arith_tac 1); |
|
74 |
|
75 Goal "(x + y = y) = (x = (#0::real))"; |
|
76 by(arith_tac 1); |
|
77 |
|
78 Goal "(x + y = (#0::real)) = (x = -y)"; |
|
79 by(arith_tac 1); |
|
80 |
|
81 Goal "(x + y = (#0::real)) = (y = -x)"; |
|
82 by(arith_tac 1); |
|
83 |
|
84 Goal "((x + y) < (x + z)) = (y < (z::real))"; |
|
85 by(arith_tac 1); |
|
86 |
|
87 Goal "((x + z) < (y + z)) = (x < (y::real))"; |
|
88 by(arith_tac 1); |
|
89 |
|
90 Goal "(~ x < y) = (y <= (x::real))"; |
|
91 by(arith_tac 1); |
|
92 |
|
93 Goal "~(x < y & y < (x::real))"; |
|
94 by(arith_tac 1); |
|
95 |
|
96 Goal "(x::real) < y ==> ~ y < x"; |
|
97 by(arith_tac 1); |
|
98 |
|
99 Goal "((x::real) ~= y) = (x < y | y < x)"; |
|
100 by(arith_tac 1); |
|
101 |
|
102 Goal "(~ x <= y) = (y < (x::real))"; |
|
103 by(arith_tac 1); |
|
104 |
|
105 Goal "x <= y | y <= (x::real)"; |
|
106 by(arith_tac 1); |
|
107 |
|
108 Goal "x <= y | y < (x::real)"; |
|
109 by(arith_tac 1); |
|
110 |
|
111 Goal "x < y | y <= (x::real)"; |
|
112 by(arith_tac 1); |
|
113 |
|
114 Goal "x <= (x::real)"; |
|
115 by(arith_tac 1); |
|
116 |
|
117 Goal "((x::real) <= y) = (x < y | x = y)"; |
|
118 by(arith_tac 1); |
|
119 |
|
120 Goal "((x::real) <= y & y <= x) = (x = y)"; |
|
121 by(arith_tac 1); |
|
122 |
|
123 Goal "~(x < y & y <= (x::real))"; |
|
124 by(arith_tac 1); |
|
125 |
|
126 Goal "~(x <= y & y < (x::real))"; |
|
127 by(arith_tac 1); |
|
128 |
|
129 Goal "(-x < (#0::real)) = (#0 < x)"; |
|
130 by(arith_tac 1); |
|
131 |
|
132 Goal "((#0::real) < -x) = (x < #0)"; |
|
133 by(arith_tac 1); |
|
134 |
|
135 Goal "(-x <= (#0::real)) = (#0 <= x)"; |
|
136 by(arith_tac 1); |
|
137 |
|
138 Goal "((#0::real) <= -x) = (x <= #0)"; |
|
139 by(arith_tac 1); |
|
140 |
|
141 Goal "(x::real) = y | x < y | y < x"; |
|
142 by(arith_tac 1); |
|
143 |
|
144 Goal "(x::real) = #0 | #0 < x | #0 < -x"; |
|
145 by(arith_tac 1); |
|
146 |
|
147 Goal "(#0::real) <= x | #0 <= -x"; |
|
148 by(arith_tac 1); |
|
149 |
|
150 Goal "((x::real) + y <= x + z) = (y <= z)"; |
|
151 by(arith_tac 1); |
|
152 |
|
153 Goal "((x::real) + z <= y + z) = (x <= y)"; |
|
154 by(arith_tac 1); |
|
155 |
|
156 Goal "(w::real) < x & y < z ==> w + y < x + z"; |
|
157 by(arith_tac 1); |
|
158 |
|
159 Goal "(w::real) <= x & y <= z ==> w + y <= x + z"; |
|
160 by(arith_tac 1); |
|
161 |
|
162 Goal "(#0::real) <= x & #0 <= y ==> #0 <= x + y"; |
|
163 by(arith_tac 1); |
|
164 |
|
165 Goal "(#0::real) < x & #0 < y ==> #0 < x + y"; |
|
166 by(arith_tac 1); |
|
167 |
|
168 Goal "(-x < y) = (#0 < x + (y::real))"; |
|
169 by(arith_tac 1); |
|
170 |
|
171 Goal "(x < -y) = (x + y < (#0::real))"; |
|
172 by(arith_tac 1); |
|
173 |
|
174 Goal "(y < x + -z) = (y + z < (x::real))"; |
|
175 by(arith_tac 1); |
|
176 |
|
177 Goal "(x + -y < z) = (x < z + (y::real))"; |
|
178 by(arith_tac 1); |
|
179 |
|
180 Goal "x <= y ==> x < y + (#1::real)"; |
|
181 by(arith_tac 1); |
|
182 |
|
183 Goal "(x - y) + y = (x::real)"; |
|
184 by(arith_tac 1); |
|
185 |
|
186 Goal "y + (x - y) = (x::real)"; |
|
187 by(arith_tac 1); |
|
188 |
|
189 Goal "x - x = (#0::real)"; |
|
190 by(arith_tac 1); |
|
191 |
|
192 Goal "(x - y = #0) = (x = (y::real))"; |
|
193 by(arith_tac 1); |
|
194 |
|
195 Goal "((#0::real) <= x + x) = (#0 <= x)"; |
|
196 by(arith_tac 1); |
|
197 |
|
198 Goal "(-x <= x) = ((#0::real) <= x)"; |
|
199 by(arith_tac 1); |
|
200 |
|
201 Goal "(x <= -x) = (x <= (#0::real))"; |
|
202 by(arith_tac 1); |
|
203 |
|
204 Goal "(-x = (#0::real)) = (x = #0)"; |
|
205 by(arith_tac 1); |
|
206 |
|
207 Goal "-(x - y) = y - (x::real)"; |
|
208 by(arith_tac 1); |
|
209 |
|
210 Goal "((#0::real) < x - y) = (y < x)"; |
|
211 by(arith_tac 1); |
|
212 |
|
213 Goal "((#0::real) <= x - y) = (y <= x)"; |
|
214 by(arith_tac 1); |
|
215 |
|
216 Goal "(x + y) - x = (y::real)"; |
|
217 by(arith_tac 1); |
|
218 |
|
219 Goal "(-x = y) = (x = (-y::real))"; |
|
220 by(arith_tac 1); |
|
221 |
|
222 Goal "x < (y::real) ==> ~(x = y)"; |
|
223 by(arith_tac 1); |
|
224 |
|
225 Goal "(x <= x + y) = ((#0::real) <= y)"; |
|
226 by(arith_tac 1); |
|
227 |
|
228 Goal "(y <= x + y) = ((#0::real) <= x)"; |
|
229 by(arith_tac 1); |
|
230 |
|
231 Goal "(x < x + y) = ((#0::real) < y)"; |
|
232 by(arith_tac 1); |
|
233 |
|
234 Goal "(y < x + y) = ((#0::real) < x)"; |
|
235 by(arith_tac 1); |
|
236 |
|
237 Goal "(x - y) - x = (-y::real)"; |
|
238 by(arith_tac 1); |
|
239 |
|
240 Goal "(x + y < z) = (x < z - (y::real))"; |
|
241 by(arith_tac 1); |
|
242 |
|
243 Goal "(x - y < z) = (x < z + (y::real))"; |
|
244 by(arith_tac 1); |
|
245 |
|
246 Goal "(x < y - z) = (x + z < (y::real))"; |
|
247 by(arith_tac 1); |
|
248 |
|
249 Goal "(x <= y - z) = (x + z <= (y::real))"; |
|
250 by(arith_tac 1); |
|
251 |
|
252 Goal "(x - y <= z) = (x <= z + (y::real))"; |
|
253 by(arith_tac 1); |
|
254 |
|
255 Goal "(-x < -y) = (y < (x::real))"; |
|
256 by(arith_tac 1); |
|
257 |
|
258 Goal "(-x <= -y) = (y <= (x::real))"; |
|
259 by(arith_tac 1); |
|
260 |
|
261 Goal "(a + b) - (c + d) = (a - c) + (b - (d::real))"; |
|
262 by(arith_tac 1); |
|
263 |
|
264 Goal "(#0::real) - x = -x"; |
|
265 by(arith_tac 1); |
|
266 |
|
267 Goal "x - (#0::real) = x"; |
|
268 by(arith_tac 1); |
|
269 |
|
270 Goal "w <= x & y < z ==> w + y < x + (z::real)"; |
|
271 by(arith_tac 1); |
|
272 |
|
273 Goal "w < x & y <= z ==> w + y < x + (z::real)"; |
|
274 by(arith_tac 1); |
|
275 |
|
276 Goal "(#0::real) <= x & #0 < y ==> #0 < x + (y::real)"; |
|
277 by(arith_tac 1); |
|
278 |
|
279 Goal "(#0::real) < x & #0 <= y ==> #0 < x + y"; |
|
280 by(arith_tac 1); |
|
281 |
|
282 Goal "-x - y = -(x + (y::real))"; |
|
283 by(arith_tac 1); |
|
284 |
|
285 Goal "x - (-y) = x + (y::real)"; |
|
286 by(arith_tac 1); |
|
287 |
|
288 Goal "-x - -y = y - (x::real)"; |
|
289 by(arith_tac 1); |
|
290 |
|
291 Goal "(a - b) + (b - c) = a - (c::real)"; |
|
292 by(arith_tac 1); |
|
293 |
|
294 Goal "(x = y - z) = (x + z = (y::real))"; |
|
295 by(arith_tac 1); |
|
296 |
|
297 Goal "(x - y = z) = (x = z + (y::real))"; |
|
298 by(arith_tac 1); |
|
299 |
|
300 Goal "x - (x - y) = (y::real)"; |
|
301 by(arith_tac 1); |
|
302 |
|
303 Goal "x - (x + y) = -(y::real)"; |
|
304 by(arith_tac 1); |
|
305 |
|
306 Goal "x = y ==> x <= (y::real)"; |
|
307 by(arith_tac 1); |
|
308 |
|
309 Goal "(#0::real) < x ==> ~(x = #0)"; |
|
310 by(arith_tac 1); |
|
311 |
|
312 Goal "(x + y) * (x - y) = (x * x) - (y * y)"; |
|
313 |
|
314 Goal "(-x = -y) = (x = (y::real))"; |
|
315 by(arith_tac 1); |
|
316 |
|
317 Goal "(-x < -y) = (y < (x::real))"; |
|
318 by(arith_tac 1); |
|
319 |
|
320 Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"; |
|
321 by (fast_arith_tac 1); |
|
322 |
|
323 Goal "!!a::real. [| a < b; c < d |] ==> a-d <= b+(-c)"; |
|
324 by (fast_arith_tac 1); |
|
325 |
|
326 Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c"; |
|
327 by (fast_arith_tac 1); |
|
328 |
|
329 Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] \ |
|
330 \ ==> a+a <= j+j"; |
|
331 by (fast_arith_tac 1); |
|
332 |
|
333 Goal "!!a::real. [| a+b < i+j; a<b; i<j |] \ |
|
334 \ ==> a+a < j+j"; |
|
335 by (fast_arith_tac 1); |
|
336 |
|
337 Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"; |
|
338 by (arith_tac 1); |
|
339 |
|
340 Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
|
341 \ ==> a <= l"; |
|
342 by (fast_arith_tac 1); |
|
343 |
|
344 Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
|
345 \ ==> a+a+a+a <= l+l+l+l"; |
|
346 by (fast_arith_tac 1); |
|
347 |
|
348 (* Too slow. Needs "combine_coefficients" simproc |
|
349 Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
|
350 \ ==> a+a+a+a+a <= l+l+l+l+i"; |
|
351 by (fast_arith_tac 1); |
|
352 |
|
353 Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
|
354 \ ==> a+a+a+a+a+a <= l+l+l+l+i+l"; |
|
355 by (fast_arith_tac 1); |
|
356 *) |
|
357 |