author | wenzelm |
Tue, 21 Nov 2000 19:03:27 +0100 | |
changeset 10506 | 01333dbe1431 |
parent 9570 | e16e168984e1 |
child 11315 | fbca0f74bcef |
permissions | -rw-r--r-- |
5533 | 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 Bin.thy; |
|
10 |
||
11 |
(*All runtimes below are on a 300MHz Pentium*) |
|
12 |
||
13 |
Goal "#13 $+ #19 = #32"; |
|
6153 | 14 |
by (Simp_tac 1); (*0 secs*) |
5533 | 15 |
result(); |
16 |
||
17 |
Goal "#1234 $+ #5678 = #6912"; |
|
6153 | 18 |
by (Simp_tac 1); (*190 msec*) |
5533 | 19 |
result(); |
20 |
||
21 |
Goal "#1359 $+ #-2468 = #-1109"; |
|
6153 | 22 |
by (Simp_tac 1); (*160 msec*) |
5533 | 23 |
result(); |
24 |
||
25 |
Goal "#93746 $+ #-46375 = #47371"; |
|
6153 | 26 |
by (Simp_tac 1); (*300 msec*) |
5533 | 27 |
result(); |
28 |
||
9548 | 29 |
Goal "$- #65745 = #-65745"; |
6153 | 30 |
by (Simp_tac 1); (*80 msec*) |
5533 | 31 |
result(); |
32 |
||
33 |
(* negation of ~54321 *) |
|
9548 | 34 |
Goal "$- #-54321 = #54321"; |
6153 | 35 |
by (Simp_tac 1); (*90 msec*) |
5533 | 36 |
result(); |
37 |
||
38 |
Goal "#13 $* #19 = #247"; |
|
6153 | 39 |
by (Simp_tac 1); (*110 msec*) |
5533 | 40 |
result(); |
41 |
||
42 |
Goal "#-84 $* #51 = #-4284"; |
|
6153 | 43 |
by (Simp_tac 1); (*210 msec*) |
5533 | 44 |
result(); |
45 |
||
46 |
(*The worst case for 8-bit operands *) |
|
47 |
Goal "#255 $* #255 = #65025"; |
|
6153 | 48 |
by (Simp_tac 1); (*730 msec*) |
5533 | 49 |
result(); |
50 |
||
51 |
Goal "#1359 $* #-2468 = #-3354012"; |
|
6153 | 52 |
by (Simp_tac 1); (*1.04 secs*) |
5533 | 53 |
result(); |
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
54 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
55 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
56 |
(** Comparisons **) |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
57 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
58 |
Goal "(#89) $* #10 ~= #889"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
59 |
by (Simp_tac 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
60 |
result(); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
61 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
62 |
Goal "(#13) $< #18 $- #4"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
63 |
by (Simp_tac 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
64 |
result(); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
65 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
66 |
Goal "(#-345) $< #-242 $+ #-100"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
67 |
by (Simp_tac 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
68 |
result(); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
69 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
70 |
Goal "(#13557456) $< #18678654"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
71 |
by (Simp_tac 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
72 |
result(); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
73 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
74 |
Goal "(#999999) $<= (#1000001 $+ #1) $- #2"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
75 |
by (Simp_tac 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
76 |
result(); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
77 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
78 |
Goal "(#1234567) $<= #1234567"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
79 |
by (Simp_tac 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
80 |
result(); |