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 |
set proof_timing;
|
|
12 |
(*All runtimes below are on a 300MHz Pentium*)
|
|
13 |
|
|
14 |
Goal "#13 $+ #19 = #32";
|
6153
|
15 |
by (Simp_tac 1); (*0 secs*)
|
5533
|
16 |
result();
|
|
17 |
|
|
18 |
Goal "#1234 $+ #5678 = #6912";
|
6153
|
19 |
by (Simp_tac 1); (*190 msec*)
|
5533
|
20 |
result();
|
|
21 |
|
|
22 |
Goal "#1359 $+ #-2468 = #-1109";
|
6153
|
23 |
by (Simp_tac 1); (*160 msec*)
|
5533
|
24 |
result();
|
|
25 |
|
|
26 |
Goal "#93746 $+ #-46375 = #47371";
|
6153
|
27 |
by (Simp_tac 1); (*300 msec*)
|
5533
|
28 |
result();
|
|
29 |
|
|
30 |
Goal "$~ #65745 = #-65745";
|
6153
|
31 |
by (Simp_tac 1); (*80 msec*)
|
5533
|
32 |
result();
|
|
33 |
|
|
34 |
(* negation of ~54321 *)
|
|
35 |
Goal "$~ #-54321 = #54321";
|
6153
|
36 |
by (Simp_tac 1); (*90 msec*)
|
5533
|
37 |
result();
|
|
38 |
|
|
39 |
Goal "#13 $* #19 = #247";
|
6153
|
40 |
by (Simp_tac 1); (*110 msec*)
|
5533
|
41 |
result();
|
|
42 |
|
|
43 |
Goal "#-84 $* #51 = #-4284";
|
6153
|
44 |
by (Simp_tac 1); (*210 msec*)
|
5533
|
45 |
result();
|
|
46 |
|
|
47 |
(*The worst case for 8-bit operands *)
|
|
48 |
Goal "#255 $* #255 = #65025";
|
6153
|
49 |
by (Simp_tac 1); (*730 msec*)
|
5533
|
50 |
result();
|
|
51 |
|
|
52 |
Goal "#1359 $* #-2468 = #-3354012";
|
6153
|
53 |
by (Simp_tac 1); (*1.04 secs*)
|
5533
|
54 |
result();
|