1 (* Title: ZF/ex/BinEx.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 Examples of performing binary arithmetic by simplification |
|
7 *) |
|
8 |
|
9 context Main.thy; |
|
10 |
|
11 (*All runtimes below are on a 300MHz Pentium*) |
|
12 |
|
13 Goal "#13 $+ #19 = #32"; |
|
14 by (Simp_tac 1); (*0 secs*) |
|
15 result(); |
|
16 |
|
17 Goal "#1234 $+ #5678 = #6912"; |
|
18 by (Simp_tac 1); (*190 msec*) |
|
19 result(); |
|
20 |
|
21 Goal "#1359 $+ #-2468 = #-1109"; |
|
22 by (Simp_tac 1); (*160 msec*) |
|
23 result(); |
|
24 |
|
25 Goal "#93746 $+ #-46375 = #47371"; |
|
26 by (Simp_tac 1); (*300 msec*) |
|
27 result(); |
|
28 |
|
29 Goal "$- #65745 = #-65745"; |
|
30 by (Simp_tac 1); (*80 msec*) |
|
31 result(); |
|
32 |
|
33 (* negation of ~54321 *) |
|
34 Goal "$- #-54321 = #54321"; |
|
35 by (Simp_tac 1); (*90 msec*) |
|
36 result(); |
|
37 |
|
38 Goal "#13 $* #19 = #247"; |
|
39 by (Simp_tac 1); (*110 msec*) |
|
40 result(); |
|
41 |
|
42 Goal "#-84 $* #51 = #-4284"; |
|
43 by (Simp_tac 1); (*210 msec*) |
|
44 result(); |
|
45 |
|
46 (*The worst case for 8-bit operands *) |
|
47 Goal "#255 $* #255 = #65025"; |
|
48 by (Simp_tac 1); (*730 msec*) |
|
49 result(); |
|
50 |
|
51 Goal "#1359 $* #-2468 = #-3354012"; |
|
52 by (Simp_tac 1); (*1.04 secs*) |
|
53 result(); |
|
54 |
|
55 |
|
56 (** Comparisons **) |
|
57 |
|
58 Goal "(#89) $* #10 \\<noteq> #889"; |
|
59 by (Simp_tac 1); |
|
60 result(); |
|
61 |
|
62 Goal "(#13) $< #18 $- #4"; |
|
63 by (Simp_tac 1); |
|
64 result(); |
|
65 |
|
66 Goal "(#-345) $< #-242 $+ #-100"; |
|
67 by (Simp_tac 1); |
|
68 result(); |
|
69 |
|
70 Goal "(#13557456) $< #18678654"; |
|
71 by (Simp_tac 1); |
|
72 result(); |
|
73 |
|
74 Goal "(#999999) $<= (#1000001 $+ #1) $- #2"; |
|
75 by (Simp_tac 1); |
|
76 result(); |
|
77 |
|
78 Goal "(#1234567) $<= #1234567"; |
|
79 by (Simp_tac 1); |
|
80 result(); |
|
81 |
|
82 |
|
83 (*** Quotient and remainder!! [they could be faster] ***) |
|
84 |
|
85 Goal "#23 zdiv #3 = #7"; |
|
86 by (Simp_tac 1); |
|
87 result(); |
|
88 |
|
89 Goal "#23 zmod #3 = #2"; |
|
90 by (Simp_tac 1); |
|
91 result(); |
|
92 |
|
93 (** negative dividend **) |
|
94 |
|
95 Goal "#-23 zdiv #3 = #-8"; |
|
96 by (Simp_tac 1); |
|
97 result(); |
|
98 |
|
99 Goal "#-23 zmod #3 = #1"; |
|
100 by (Simp_tac 1); |
|
101 result(); |
|
102 |
|
103 (** negative divisor **) |
|
104 |
|
105 Goal "#23 zdiv #-3 = #-8"; |
|
106 by (Simp_tac 1); |
|
107 result(); |
|
108 |
|
109 Goal "#23 zmod #-3 = #-1"; |
|
110 by (Simp_tac 1); |
|
111 result(); |
|
112 |
|
113 (** Negative dividend and divisor **) |
|
114 |
|
115 Goal "#-23 zdiv #-3 = #7"; |
|
116 by (Simp_tac 1); |
|
117 result(); |
|
118 |
|
119 Goal "#-23 zmod #-3 = #-2"; |
|
120 by (Simp_tac 1); |
|
121 result(); |
|
122 |
|