1 (* Title: HOL/Complex/ex/BinEx.thy |
|
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 |
|
10 imports Complex_Main |
|
11 begin |
|
12 |
|
13 text {* |
|
14 Examples of performing binary arithmetic by simplification. This time |
|
15 we use the reals, though the representation is just of integers. |
|
16 *} |
|
17 |
|
18 subsection{*Real Arithmetic*} |
|
19 |
|
20 subsubsection {*Addition *} |
|
21 |
|
22 lemma "(1359::real) + -2468 = -1109" |
|
23 by simp |
|
24 |
|
25 lemma "(93746::real) + -46375 = 47371" |
|
26 by simp |
|
27 |
|
28 |
|
29 subsubsection {*Negation *} |
|
30 |
|
31 lemma "- (65745::real) = -65745" |
|
32 by simp |
|
33 |
|
34 lemma "- (-54321::real) = 54321" |
|
35 by simp |
|
36 |
|
37 |
|
38 subsubsection {*Multiplication *} |
|
39 |
|
40 lemma "(-84::real) * 51 = -4284" |
|
41 by simp |
|
42 |
|
43 lemma "(255::real) * 255 = 65025" |
|
44 by simp |
|
45 |
|
46 lemma "(1359::real) * -2468 = -3354012" |
|
47 by simp |
|
48 |
|
49 |
|
50 subsubsection {*Inequalities *} |
|
51 |
|
52 lemma "(89::real) * 10 \<noteq> 889" |
|
53 by simp |
|
54 |
|
55 lemma "(13::real) < 18 - 4" |
|
56 by simp |
|
57 |
|
58 lemma "(-345::real) < -242 + -100" |
|
59 by simp |
|
60 |
|
61 lemma "(13557456::real) < 18678654" |
|
62 by simp |
|
63 |
|
64 lemma "(999999::real) \<le> (1000001 + 1) - 2" |
|
65 by simp |
|
66 |
|
67 lemma "(1234567::real) \<le> 1234567" |
|
68 by simp |
|
69 |
|
70 |
|
71 subsubsection {*Powers *} |
|
72 |
|
73 lemma "2 ^ 15 = (32768::real)" |
|
74 by simp |
|
75 |
|
76 lemma "-3 ^ 7 = (-2187::real)" |
|
77 by simp |
|
78 |
|
79 lemma "13 ^ 7 = (62748517::real)" |
|
80 by simp |
|
81 |
|
82 lemma "3 ^ 15 = (14348907::real)" |
|
83 by simp |
|
84 |
|
85 lemma "-5 ^ 11 = (-48828125::real)" |
|
86 by simp |
|
87 |
|
88 |
|
89 subsubsection {*Tests *} |
|
90 |
|
91 lemma "(x + y = x) = (y = (0::real))" |
|
92 by arith |
|
93 |
|
94 lemma "(x + y = y) = (x = (0::real))" |
|
95 by arith |
|
96 |
|
97 lemma "(x + y = (0::real)) = (x = -y)" |
|
98 by arith |
|
99 |
|
100 lemma "(x + y = (0::real)) = (y = -x)" |
|
101 by arith |
|
102 |
|
103 lemma "((x + y) < (x + z)) = (y < (z::real))" |
|
104 by arith |
|
105 |
|
106 lemma "((x + z) < (y + z)) = (x < (y::real))" |
|
107 by arith |
|
108 |
|
109 lemma "(\<not> x < y) = (y \<le> (x::real))" |
|
110 by arith |
|
111 |
|
112 lemma "\<not> (x < y \<and> y < (x::real))" |
|
113 by arith |
|
114 |
|
115 lemma "(x::real) < y ==> \<not> y < x" |
|
116 by arith |
|
117 |
|
118 lemma "((x::real) \<noteq> y) = (x < y \<or> y < x)" |
|
119 by arith |
|
120 |
|
121 lemma "(\<not> x \<le> y) = (y < (x::real))" |
|
122 by arith |
|
123 |
|
124 lemma "x \<le> y \<or> y \<le> (x::real)" |
|
125 by arith |
|
126 |
|
127 lemma "x \<le> y \<or> y < (x::real)" |
|
128 by arith |
|
129 |
|
130 lemma "x < y \<or> y \<le> (x::real)" |
|
131 by arith |
|
132 |
|
133 lemma "x \<le> (x::real)" |
|
134 by arith |
|
135 |
|
136 lemma "((x::real) \<le> y) = (x < y \<or> x = y)" |
|
137 by arith |
|
138 |
|
139 lemma "((x::real) \<le> y \<and> y \<le> x) = (x = y)" |
|
140 by arith |
|
141 |
|
142 lemma "\<not>(x < y \<and> y \<le> (x::real))" |
|
143 by arith |
|
144 |
|
145 lemma "\<not>(x \<le> y \<and> y < (x::real))" |
|
146 by arith |
|
147 |
|
148 lemma "(-x < (0::real)) = (0 < x)" |
|
149 by arith |
|
150 |
|
151 lemma "((0::real) < -x) = (x < 0)" |
|
152 by arith |
|
153 |
|
154 lemma "(-x \<le> (0::real)) = (0 \<le> x)" |
|
155 by arith |
|
156 |
|
157 lemma "((0::real) \<le> -x) = (x \<le> 0)" |
|
158 by arith |
|
159 |
|
160 lemma "(x::real) = y \<or> x < y \<or> y < x" |
|
161 by arith |
|
162 |
|
163 lemma "(x::real) = 0 \<or> 0 < x \<or> 0 < -x" |
|
164 by arith |
|
165 |
|
166 lemma "(0::real) \<le> x \<or> 0 \<le> -x" |
|
167 by arith |
|
168 |
|
169 lemma "((x::real) + y \<le> x + z) = (y \<le> z)" |
|
170 by arith |
|
171 |
|
172 lemma "((x::real) + z \<le> y + z) = (x \<le> y)" |
|
173 by arith |
|
174 |
|
175 lemma "(w::real) < x \<and> y < z ==> w + y < x + z" |
|
176 by arith |
|
177 |
|
178 lemma "(w::real) \<le> x \<and> y \<le> z ==> w + y \<le> x + z" |
|
179 by arith |
|
180 |
|
181 lemma "(0::real) \<le> x \<and> 0 \<le> y ==> 0 \<le> x + y" |
|
182 by arith |
|
183 |
|
184 lemma "(0::real) < x \<and> 0 < y ==> 0 < x + y" |
|
185 by arith |
|
186 |
|
187 lemma "(-x < y) = (0 < x + (y::real))" |
|
188 by arith |
|
189 |
|
190 lemma "(x < -y) = (x + y < (0::real))" |
|
191 by arith |
|
192 |
|
193 lemma "(y < x + -z) = (y + z < (x::real))" |
|
194 by arith |
|
195 |
|
196 lemma "(x + -y < z) = (x < z + (y::real))" |
|
197 by arith |
|
198 |
|
199 lemma "x \<le> y ==> x < y + (1::real)" |
|
200 by arith |
|
201 |
|
202 lemma "(x - y) + y = (x::real)" |
|
203 by arith |
|
204 |
|
205 lemma "y + (x - y) = (x::real)" |
|
206 by arith |
|
207 |
|
208 lemma "x - x = (0::real)" |
|
209 by arith |
|
210 |
|
211 lemma "(x - y = 0) = (x = (y::real))" |
|
212 by arith |
|
213 |
|
214 lemma "((0::real) \<le> x + x) = (0 \<le> x)" |
|
215 by arith |
|
216 |
|
217 lemma "(-x \<le> x) = ((0::real) \<le> x)" |
|
218 by arith |
|
219 |
|
220 lemma "(x \<le> -x) = (x \<le> (0::real))" |
|
221 by arith |
|
222 |
|
223 lemma "(-x = (0::real)) = (x = 0)" |
|
224 by arith |
|
225 |
|
226 lemma "-(x - y) = y - (x::real)" |
|
227 by arith |
|
228 |
|
229 lemma "((0::real) < x - y) = (y < x)" |
|
230 by arith |
|
231 |
|
232 lemma "((0::real) \<le> x - y) = (y \<le> x)" |
|
233 by arith |
|
234 |
|
235 lemma "(x + y) - x = (y::real)" |
|
236 by arith |
|
237 |
|
238 lemma "(-x = y) = (x = (-y::real))" |
|
239 by arith |
|
240 |
|
241 lemma "x < (y::real) ==> \<not>(x = y)" |
|
242 by arith |
|
243 |
|
244 lemma "(x \<le> x + y) = ((0::real) \<le> y)" |
|
245 by arith |
|
246 |
|
247 lemma "(y \<le> x + y) = ((0::real) \<le> x)" |
|
248 by arith |
|
249 |
|
250 lemma "(x < x + y) = ((0::real) < y)" |
|
251 by arith |
|
252 |
|
253 lemma "(y < x + y) = ((0::real) < x)" |
|
254 by arith |
|
255 |
|
256 lemma "(x - y) - x = (-y::real)" |
|
257 by arith |
|
258 |
|
259 lemma "(x + y < z) = (x < z - (y::real))" |
|
260 by arith |
|
261 |
|
262 lemma "(x - y < z) = (x < z + (y::real))" |
|
263 by arith |
|
264 |
|
265 lemma "(x < y - z) = (x + z < (y::real))" |
|
266 by arith |
|
267 |
|
268 lemma "(x \<le> y - z) = (x + z \<le> (y::real))" |
|
269 by arith |
|
270 |
|
271 lemma "(x - y \<le> z) = (x \<le> z + (y::real))" |
|
272 by arith |
|
273 |
|
274 lemma "(-x < -y) = (y < (x::real))" |
|
275 by arith |
|
276 |
|
277 lemma "(-x \<le> -y) = (y \<le> (x::real))" |
|
278 by arith |
|
279 |
|
280 lemma "(a + b) - (c + d) = (a - c) + (b - (d::real))" |
|
281 by arith |
|
282 |
|
283 lemma "(0::real) - x = -x" |
|
284 by arith |
|
285 |
|
286 lemma "x - (0::real) = x" |
|
287 by arith |
|
288 |
|
289 lemma "w \<le> x \<and> y < z ==> w + y < x + (z::real)" |
|
290 by arith |
|
291 |
|
292 lemma "w < x \<and> y \<le> z ==> w + y < x + (z::real)" |
|
293 by arith |
|
294 |
|
295 lemma "(0::real) \<le> x \<and> 0 < y ==> 0 < x + (y::real)" |
|
296 by arith |
|
297 |
|
298 lemma "(0::real) < x \<and> 0 \<le> y ==> 0 < x + y" |
|
299 by arith |
|
300 |
|
301 lemma "-x - y = -(x + (y::real))" |
|
302 by arith |
|
303 |
|
304 lemma "x - (-y) = x + (y::real)" |
|
305 by arith |
|
306 |
|
307 lemma "-x - -y = y - (x::real)" |
|
308 by arith |
|
309 |
|
310 lemma "(a - b) + (b - c) = a - (c::real)" |
|
311 by arith |
|
312 |
|
313 lemma "(x = y - z) = (x + z = (y::real))" |
|
314 by arith |
|
315 |
|
316 lemma "(x - y = z) = (x = z + (y::real))" |
|
317 by arith |
|
318 |
|
319 lemma "x - (x - y) = (y::real)" |
|
320 by arith |
|
321 |
|
322 lemma "x - (x + y) = -(y::real)" |
|
323 by arith |
|
324 |
|
325 lemma "x = y ==> x \<le> (y::real)" |
|
326 by arith |
|
327 |
|
328 lemma "(0::real) < x ==> \<not>(x = 0)" |
|
329 by arith |
|
330 |
|
331 lemma "(x + y) * (x - y) = (x * x) - (y * y)" |
|
332 oops |
|
333 |
|
334 lemma "(-x = -y) = (x = (y::real))" |
|
335 by arith |
|
336 |
|
337 lemma "(-x < -y) = (y < (x::real))" |
|
338 by arith |
|
339 |
|
340 lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d" |
|
341 by (tactic "fast_arith_tac @{context} 1") |
|
342 |
|
343 lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)" |
|
344 by (tactic "fast_arith_tac @{context} 1") |
|
345 |
|
346 lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c" |
|
347 by (tactic "fast_arith_tac @{context} 1") |
|
348 |
|
349 lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j" |
|
350 by (tactic "fast_arith_tac @{context} 1") |
|
351 |
|
352 lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j" |
|
353 by (tactic "fast_arith_tac @{context} 1") |
|
354 |
|
355 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" |
|
356 by arith |
|
357 |
|
358 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
|
359 ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l" |
|
360 by (tactic "fast_arith_tac @{context} 1") |
|
361 |
|
362 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
|
363 ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l" |
|
364 by (tactic "fast_arith_tac @{context} 1") |
|
365 |
|
366 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
|
367 ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i" |
|
368 by (tactic "fast_arith_tac @{context} 1") |
|
369 |
|
370 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
|
371 ==> 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" |
|
372 by (tactic "fast_arith_tac @{context} 1") |
|
373 |
|
374 |
|
375 subsection{*Complex Arithmetic*} |
|
376 |
|
377 lemma "(1359 + 93746*ii) - (2468 + 46375*ii) = -1109 + 47371*ii" |
|
378 by simp |
|
379 |
|
380 lemma "- (65745 + -47371*ii) = -65745 + 47371*ii" |
|
381 by simp |
|
382 |
|
383 text{*Multiplication requires distributive laws. Perhaps versions instantiated |
|
384 to literal constants should be added to the simpset.*} |
|
385 |
|
386 lemma "(1 + ii) * (1 - ii) = 2" |
|
387 by (simp add: ring_distribs) |
|
388 |
|
389 lemma "(1 + 2*ii) * (1 + 3*ii) = -5 + 5*ii" |
|
390 by (simp add: ring_distribs) |
|
391 |
|
392 lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii" |
|
393 by (simp add: ring_distribs) |
|
394 |
|
395 text{*No inequalities or linear arithmetic: the complex numbers are unordered!*} |
|
396 |
|
397 text{*No powers (not supported yet)*} |
|
398 |
|
399 end |
|