src/ZF/ex/BinEx.ML
author wenzelm
Tue May 30 16:08:38 2000 +0200 (2000-05-30)
changeset 9000 c20d58286a51
parent 6153 bff90585cce5
child 9548 15bee2731e43
permissions -rw-r--r--
cleaned up;
paulson@5533
     1
(*  Title:      ZF/ex/BinEx.ML
paulson@5533
     2
    ID:         $Id$
paulson@5533
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5533
     4
    Copyright   1994  University of Cambridge
paulson@5533
     5
paulson@5533
     6
Examples of performing binary arithmetic by simplification
paulson@5533
     7
*)
paulson@5533
     8
paulson@5533
     9
context Bin.thy;
paulson@5533
    10
paulson@5533
    11
(*All runtimes below are on a 300MHz Pentium*)
paulson@5533
    12
paulson@5533
    13
Goal "#13  $+  #19 = #32";
paulson@6153
    14
by (Simp_tac 1);    (*0 secs*)
paulson@5533
    15
result();
paulson@5533
    16
paulson@5533
    17
Goal "#1234  $+  #5678 = #6912";
paulson@6153
    18
by (Simp_tac 1);    (*190 msec*)
paulson@5533
    19
result();
paulson@5533
    20
paulson@5533
    21
Goal "#1359  $+  #-2468 = #-1109";
paulson@6153
    22
by (Simp_tac 1);    (*160 msec*)
paulson@5533
    23
result();
paulson@5533
    24
paulson@5533
    25
Goal "#93746  $+  #-46375 = #47371";
paulson@6153
    26
by (Simp_tac 1);    (*300 msec*)
paulson@5533
    27
result();
paulson@5533
    28
paulson@5533
    29
Goal "$~ #65745 = #-65745";
paulson@6153
    30
by (Simp_tac 1);    (*80 msec*)
paulson@5533
    31
result();
paulson@5533
    32
paulson@5533
    33
(* negation of ~54321 *)
paulson@5533
    34
Goal "$~ #-54321 = #54321";
paulson@6153
    35
by (Simp_tac 1);    (*90 msec*)
paulson@5533
    36
result();
paulson@5533
    37
paulson@5533
    38
Goal "#13  $*  #19 = #247";
paulson@6153
    39
by (Simp_tac 1);    (*110 msec*)
paulson@5533
    40
result();
paulson@5533
    41
paulson@5533
    42
Goal "#-84  $*  #51 = #-4284";
paulson@6153
    43
by (Simp_tac 1);    (*210 msec*)
paulson@5533
    44
result();
paulson@5533
    45
paulson@5533
    46
(*The worst case for 8-bit operands *)
paulson@5533
    47
Goal "#255  $*  #255 = #65025";
paulson@6153
    48
by (Simp_tac 1);    (*730 msec*)
paulson@5533
    49
result();
paulson@5533
    50
paulson@5533
    51
Goal "#1359  $*  #-2468 = #-3354012";
paulson@6153
    52
by (Simp_tac 1);    (*1.04 secs*)
paulson@5533
    53
result();