1 |
1 (* Title: HOL/Real/ex/BinEx.thy |
2 BinEx = Real |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1999 University of Cambridge |
|
5 *) |
|
6 |
|
7 header {* Binary arithmetic examples *} |
|
8 |
|
9 theory BinEx = Real: |
|
10 |
|
11 text {* |
|
12 Examples of performing binary arithmetic by simplification This time |
|
13 we use the reals, though the representation is just of integers. |
|
14 *} |
|
15 |
|
16 text {* \medskip Addition *} |
|
17 |
|
18 lemma "(#1359::real) + #-2468 = #-1109" |
|
19 by simp |
|
20 |
|
21 lemma "(#93746::real) + #-46375 = #47371" |
|
22 by simp |
|
23 |
|
24 |
|
25 text {* \medskip Negation *} |
|
26 |
|
27 lemma "- (#65745::real) = #-65745" |
|
28 by simp |
|
29 |
|
30 lemma "- (#-54321::real) = #54321" |
|
31 by simp |
|
32 |
|
33 |
|
34 text {* \medskip Multiplication *} |
|
35 |
|
36 lemma "(#-84::real) * #51 = #-4284" |
|
37 by simp |
|
38 |
|
39 lemma "(#255::real) * #255 = #65025" |
|
40 by simp |
|
41 |
|
42 lemma "(#1359::real) * #-2468 = #-3354012" |
|
43 by simp |
|
44 |
|
45 |
|
46 text {* \medskip Inequalities *} |
|
47 |
|
48 lemma "(#89::real) * #10 \<noteq> #889" |
|
49 by simp |
|
50 |
|
51 lemma "(#13::real) < #18 - #4" |
|
52 by simp |
|
53 |
|
54 lemma "(#-345::real) < #-242 + #-100" |
|
55 by simp |
|
56 |
|
57 lemma "(#13557456::real) < #18678654" |
|
58 by simp |
|
59 |
|
60 lemma "(#999999::real) \<le> (#1000001 + #1)-#2" |
|
61 by simp |
|
62 |
|
63 lemma "(#1234567::real) \<le> #1234567" |
|
64 by simp |
|
65 |
|
66 |
|
67 text {* \medskip Tests *} |
|
68 |
|
69 lemma "(x + y = x) = (y = (#0::real))" |
|
70 by arith |
|
71 |
|
72 lemma "(x + y = y) = (x = (#0::real))" |
|
73 by arith |
|
74 |
|
75 lemma "(x + y = (#0::real)) = (x = -y)" |
|
76 by arith |
|
77 |
|
78 lemma "(x + y = (#0::real)) = (y = -x)" |
|
79 by arith |
|
80 |
|
81 lemma "((x + y) < (x + z)) = (y < (z::real))" |
|
82 by arith |
|
83 |
|
84 lemma "((x + z) < (y + z)) = (x < (y::real))" |
|
85 by arith |
|
86 |
|
87 lemma "(\<not> x < y) = (y \<le> (x::real))" |
|
88 by arith |
|
89 |
|
90 lemma "\<not> (x < y \<and> y < (x::real))" |
|
91 by arith |
|
92 |
|
93 lemma "(x::real) < y ==> \<not> y < x" |
|
94 by arith |
|
95 |
|
96 lemma "((x::real) \<noteq> y) = (x < y \<or> y < x)" |
|
97 by arith |
|
98 |
|
99 lemma "(\<not> x \<le> y) = (y < (x::real))" |
|
100 by arith |
|
101 |
|
102 lemma "x \<le> y \<or> y \<le> (x::real)" |
|
103 by arith |
|
104 |
|
105 lemma "x \<le> y \<or> y < (x::real)" |
|
106 by arith |
|
107 |
|
108 lemma "x < y \<or> y \<le> (x::real)" |
|
109 by arith |
|
110 |
|
111 lemma "x \<le> (x::real)" |
|
112 by arith |
|
113 |
|
114 lemma "((x::real) \<le> y) = (x < y \<or> x = y)" |
|
115 by arith |
|
116 |
|
117 lemma "((x::real) \<le> y \<and> y \<le> x) = (x = y)" |
|
118 by arith |
|
119 |
|
120 lemma "\<not>(x < y \<and> y \<le> (x::real))" |
|
121 by arith |
|
122 |
|
123 lemma "\<not>(x \<le> y \<and> y < (x::real))" |
|
124 by arith |
|
125 |
|
126 lemma "(-x < (#0::real)) = (#0 < x)" |
|
127 by arith |
|
128 |
|
129 lemma "((#0::real) < -x) = (x < #0)" |
|
130 by arith |
|
131 |
|
132 lemma "(-x \<le> (#0::real)) = (#0 \<le> x)" |
|
133 by arith |
|
134 |
|
135 lemma "((#0::real) \<le> -x) = (x \<le> #0)" |
|
136 by arith |
|
137 |
|
138 lemma "(x::real) = y \<or> x < y \<or> y < x" |
|
139 by arith |
|
140 |
|
141 lemma "(x::real) = #0 \<or> #0 < x \<or> #0 < -x" |
|
142 by arith |
|
143 |
|
144 lemma "(#0::real) \<le> x \<or> #0 \<le> -x" |
|
145 by arith |
|
146 |
|
147 lemma "((x::real) + y \<le> x + z) = (y \<le> z)" |
|
148 by arith |
|
149 |
|
150 lemma "((x::real) + z \<le> y + z) = (x \<le> y)" |
|
151 by arith |
|
152 |
|
153 lemma "(w::real) < x \<and> y < z ==> w + y < x + z" |
|
154 by arith |
|
155 |
|
156 lemma "(w::real) \<le> x \<and> y \<le> z ==> w + y \<le> x + z" |
|
157 by arith |
|
158 |
|
159 lemma "(#0::real) \<le> x \<and> #0 \<le> y ==> #0 \<le> x + y" |
|
160 by arith |
|
161 |
|
162 lemma "(#0::real) < x \<and> #0 < y ==> #0 < x + y" |
|
163 by arith |
|
164 |
|
165 lemma "(-x < y) = (#0 < x + (y::real))" |
|
166 by arith |
|
167 |
|
168 lemma "(x < -y) = (x + y < (#0::real))" |
|
169 by arith |
|
170 |
|
171 lemma "(y < x + -z) = (y + z < (x::real))" |
|
172 by arith |
|
173 |
|
174 lemma "(x + -y < z) = (x < z + (y::real))" |
|
175 by arith |
|
176 |
|
177 lemma "x \<le> y ==> x < y + (#1::real)" |
|
178 by arith |
|
179 |
|
180 lemma "(x - y) + y = (x::real)" |
|
181 by arith |
|
182 |
|
183 lemma "y + (x - y) = (x::real)" |
|
184 by arith |
|
185 |
|
186 lemma "x - x = (#0::real)" |
|
187 by arith |
|
188 |
|
189 lemma "(x - y = #0) = (x = (y::real))" |
|
190 by arith |
|
191 |
|
192 lemma "((#0::real) \<le> x + x) = (#0 \<le> x)" |
|
193 by arith |
|
194 |
|
195 lemma "(-x \<le> x) = ((#0::real) \<le> x)" |
|
196 by arith |
|
197 |
|
198 lemma "(x \<le> -x) = (x \<le> (#0::real))" |
|
199 by arith |
|
200 |
|
201 lemma "(-x = (#0::real)) = (x = #0)" |
|
202 by arith |
|
203 |
|
204 lemma "-(x - y) = y - (x::real)" |
|
205 by arith |
|
206 |
|
207 lemma "((#0::real) < x - y) = (y < x)" |
|
208 by arith |
|
209 |
|
210 lemma "((#0::real) \<le> x - y) = (y \<le> x)" |
|
211 by arith |
|
212 |
|
213 lemma "(x + y) - x = (y::real)" |
|
214 by arith |
|
215 |
|
216 lemma "(-x = y) = (x = (-y::real))" |
|
217 by arith |
|
218 |
|
219 lemma "x < (y::real) ==> \<not>(x = y)" |
|
220 by arith |
|
221 |
|
222 lemma "(x \<le> x + y) = ((#0::real) \<le> y)" |
|
223 by arith |
|
224 |
|
225 lemma "(y \<le> x + y) = ((#0::real) \<le> x)" |
|
226 by arith |
|
227 |
|
228 lemma "(x < x + y) = ((#0::real) < y)" |
|
229 by arith |
|
230 |
|
231 lemma "(y < x + y) = ((#0::real) < x)" |
|
232 by arith |
|
233 |
|
234 lemma "(x - y) - x = (-y::real)" |
|
235 by arith |
|
236 |
|
237 lemma "(x + y < z) = (x < z - (y::real))" |
|
238 by arith |
|
239 |
|
240 lemma "(x - y < z) = (x < z + (y::real))" |
|
241 by arith |
|
242 |
|
243 lemma "(x < y - z) = (x + z < (y::real))" |
|
244 by arith |
|
245 |
|
246 lemma "(x \<le> y - z) = (x + z \<le> (y::real))" |
|
247 by arith |
|
248 |
|
249 lemma "(x - y \<le> z) = (x \<le> z + (y::real))" |
|
250 by arith |
|
251 |
|
252 lemma "(-x < -y) = (y < (x::real))" |
|
253 by arith |
|
254 |
|
255 lemma "(-x \<le> -y) = (y \<le> (x::real))" |
|
256 by arith |
|
257 |
|
258 lemma "(a + b) - (c + d) = (a - c) + (b - (d::real))" |
|
259 by arith |
|
260 |
|
261 lemma "(#0::real) - x = -x" |
|
262 by arith |
|
263 |
|
264 lemma "x - (#0::real) = x" |
|
265 by arith |
|
266 |
|
267 lemma "w \<le> x \<and> y < z ==> w + y < x + (z::real)" |
|
268 by arith |
|
269 |
|
270 lemma "w < x \<and> y \<le> z ==> w + y < x + (z::real)" |
|
271 by arith |
|
272 |
|
273 lemma "(#0::real) \<le> x \<and> #0 < y ==> #0 < x + (y::real)" |
|
274 by arith |
|
275 |
|
276 lemma "(#0::real) < x \<and> #0 \<le> y ==> #0 < x + y" |
|
277 by arith |
|
278 |
|
279 lemma "-x - y = -(x + (y::real))" |
|
280 by arith |
|
281 |
|
282 lemma "x - (-y) = x + (y::real)" |
|
283 by arith |
|
284 |
|
285 lemma "-x - -y = y - (x::real)" |
|
286 by arith |
|
287 |
|
288 lemma "(a - b) + (b - c) = a - (c::real)" |
|
289 by arith |
|
290 |
|
291 lemma "(x = y - z) = (x + z = (y::real))" |
|
292 by arith |
|
293 |
|
294 lemma "(x - y = z) = (x = z + (y::real))" |
|
295 by arith |
|
296 |
|
297 lemma "x - (x - y) = (y::real)" |
|
298 by arith |
|
299 |
|
300 lemma "x - (x + y) = -(y::real)" |
|
301 by arith |
|
302 |
|
303 lemma "x = y ==> x \<le> (y::real)" |
|
304 by arith |
|
305 |
|
306 lemma "(#0::real) < x ==> \<not>(x = #0)" |
|
307 by arith |
|
308 |
|
309 lemma "(x + y) * (x - y) = (x * x) - (y * y)" |
|
310 oops |
|
311 |
|
312 lemma "(-x = -y) = (x = (y::real))" |
|
313 by arith |
|
314 |
|
315 lemma "(-x < -y) = (y < (x::real))" |
|
316 by arith |
|
317 |
|
318 lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d" |
|
319 by (tactic "fast_arith_tac 1") |
|
320 |
|
321 lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)" |
|
322 by (tactic "fast_arith_tac 1") |
|
323 |
|
324 lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c" |
|
325 by (tactic "fast_arith_tac 1") |
|
326 |
|
327 lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j" |
|
328 by (tactic "fast_arith_tac 1") |
|
329 |
|
330 lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j" |
|
331 by (tactic "fast_arith_tac 1") |
|
332 |
|
333 lemma "!!a::real. a + b + c \<le> i + j + k \<and> a \<le> b \<and> b \<le> c \<and> i \<le> j \<and> j \<le> k --> a + a + a \<le> k + k + k" |
|
334 by arith |
|
335 |
|
336 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
|
337 ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l" |
|
338 by (tactic "fast_arith_tac 1") |
|
339 |
|
340 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
|
341 ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l" |
|
342 by (tactic "fast_arith_tac 1") |
|
343 |
|
344 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
|
345 ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i" |
|
346 by (tactic "fast_arith_tac 1") |
|
347 |
|
348 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
|
349 ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a + a \<le> l + l + l + l + i + l" |
|
350 by (tactic "fast_arith_tac 1") |
|
351 |
|
352 end |