src/ZF/ex/BinEx.ML
author paulson
Tue Sep 22 15:24:39 1998 +0200 (1998-09-22)
changeset 5533 bce36a019b03
child 6153 bff90585cce5
permissions -rw-r--r--
re-organized for the new directory Integ
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
set proof_timing;
paulson@5533
    12
(*All runtimes below are on a 300MHz Pentium*)
paulson@5533
    13
paulson@5533
    14
Goal "#13  $+  #19 = #32";
paulson@5533
    15
by (simp_tac bin_comp_ss 1);    (*0 secs*)
paulson@5533
    16
result();
paulson@5533
    17
paulson@5533
    18
Goal "#1234  $+  #5678 = #6912";
paulson@5533
    19
by (simp_tac bin_comp_ss 1);    (*190 msec*)
paulson@5533
    20
result();
paulson@5533
    21
paulson@5533
    22
Goal "#1359  $+  #-2468 = #-1109";
paulson@5533
    23
by (simp_tac bin_comp_ss 1);    (*160 msec*)
paulson@5533
    24
result();
paulson@5533
    25
paulson@5533
    26
Goal "#93746  $+  #-46375 = #47371";
paulson@5533
    27
by (simp_tac bin_comp_ss 1);    (*300 msec*)
paulson@5533
    28
result();
paulson@5533
    29
paulson@5533
    30
Goal "$~ #65745 = #-65745";
paulson@5533
    31
by (simp_tac bin_comp_ss 1);    (*80 msec*)
paulson@5533
    32
result();
paulson@5533
    33
paulson@5533
    34
(* negation of ~54321 *)
paulson@5533
    35
Goal "$~ #-54321 = #54321";
paulson@5533
    36
by (simp_tac bin_comp_ss 1);    (*90 msec*)
paulson@5533
    37
result();
paulson@5533
    38
paulson@5533
    39
Goal "#13  $*  #19 = #247";
paulson@5533
    40
by (simp_tac bin_comp_ss 1);    (*110 msec*)
paulson@5533
    41
result();
paulson@5533
    42
paulson@5533
    43
Goal "#-84  $*  #51 = #-4284";
paulson@5533
    44
by (simp_tac bin_comp_ss 1);    (*210 msec*)
paulson@5533
    45
result();
paulson@5533
    46
paulson@5533
    47
(*The worst case for 8-bit operands *)
paulson@5533
    48
Goal "#255  $*  #255 = #65025";
paulson@5533
    49
by (simp_tac bin_comp_ss 1);    (*730 msec*)
paulson@5533
    50
result();
paulson@5533
    51
paulson@5533
    52
Goal "#1359  $*  #-2468 = #-3354012";
paulson@5533
    53
by (simp_tac bin_comp_ss 1);    (*1.04 secs*)
paulson@5533
    54
result();