src/ZF/Tools/twos_compl.ML
 author wenzelm Thu May 31 12:06:31 2007 +0200 (2007-05-31) changeset 23146 0bc590051d95 child 24584 01e83ffa6c54 permissions -rw-r--r--
moved Integ files to canonical place;
```     1 (*  Title:      ZF/ex/twos-compl.ML
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1993  University of Cambridge
```
```     5
```
```     6 ML code for Arithmetic on binary integers; the model for theory Bin
```
```     7
```
```     8    The sign Pls stands for an infinite string of leading 0s.
```
```     9    The sign Min stands for an infinite string of leading 1s.
```
```    10
```
```    11 See int_of_binary for the numerical interpretation.  A number can have
```
```    12 multiple representations, namely leading 0s with sign Pls and leading 1s with
```
```    13 sign Min.  A number is in NORMAL FORM if it has no such extra bits.
```
```    14
```
```    15 The representation expects that (m mod 2) is 0 or 1, even if m is negative;
```
```    16 For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
```
```    17
```
```    18 Still needs division!
```
```    19
```
```    20 print_depth 40;
```
```    21 System.Control.Print.printDepth := 350;
```
```    22 *)
```
```    23
```
```    24 infix 5 \$\$ \$\$\$
```
```    25
```
```    26 (*Recursive datatype of binary integers*)
```
```    27 datatype bin = Pls | Min | \$\$ of bin * int;
```
```    28
```
```    29 (** Conversions between bin and int **)
```
```    30
```
```    31 fun int_of_binary Pls = 0
```
```    32   | int_of_binary Min = ~1
```
```    33   | int_of_binary (w\$\$b) = 2 * int_of_binary w + b;
```
```    34
```
```    35 fun binary_of_int 0 = Pls
```
```    36   | binary_of_int ~1 = Min
```
```    37   | binary_of_int n = binary_of_int (n div 2) \$\$ (n mod 2);
```
```    38
```
```    39 (*** Addition ***)
```
```    40
```
```    41 (*Attach a bit while preserving the normal form.  Cases left as default
```
```    42   are Pls\$\$\$1 and Min\$\$\$0. *)
```
```    43 fun  Pls \$\$\$ 0 = Pls
```
```    44   | Min \$\$\$ 1 = Min
```
```    45   |     v \$\$\$ x = v\$\$x;
```
```    46
```
```    47 (*Successor of an integer, assumed to be in normal form.
```
```    48   If w\$\$1 is normal then w is not Min, so bin_succ(w) \$\$ 0 is normal.
```
```    49   But Min\$\$0 is normal while Min\$\$1 is not.*)
```
```    50 fun bin_succ Pls = Pls\$\$1
```
```    51   | bin_succ Min = Pls
```
```    52   | bin_succ (w\$\$1) = bin_succ(w) \$\$ 0
```
```    53   | bin_succ (w\$\$0) = w \$\$\$ 1;
```
```    54
```
```    55 (*Predecessor of an integer, assumed to be in normal form.
```
```    56   If w\$\$0 is normal then w is not Pls, so bin_pred(w) \$\$ 1 is normal.
```
```    57   But Pls\$\$1 is normal while Pls\$\$0 is not.*)
```
```    58 fun bin_pred Pls = Min
```
```    59   | bin_pred Min = Min\$\$0
```
```    60   | bin_pred (w\$\$1) = w \$\$\$ 0
```
```    61   | bin_pred (w\$\$0) = bin_pred(w) \$\$ 1;
```
```    62
```
```    63 (*Sum of two binary integers in normal form.
```
```    64   Ensure last \$\$ preserves normal form! *)
```
```    65 fun bin_add (Pls, w) = w
```
```    66   | bin_add (Min, w) = bin_pred w
```
```    67   | bin_add (v\$\$x, Pls) = v\$\$x
```
```    68   | bin_add (v\$\$x, Min) = bin_pred (v\$\$x)
```
```    69   | bin_add (v\$\$x, w\$\$y) =
```
```    70       bin_add(v, if x+y=2 then bin_succ w else w) \$\$\$ ((x+y) mod 2);
```
```    71
```
```    72 (*** Subtraction ***)
```
```    73
```
```    74 (*Unary minus*)
```
```    75 fun bin_minus Pls = Pls
```
```    76   | bin_minus Min = Pls\$\$1
```
```    77   | bin_minus (w\$\$1) = bin_pred (bin_minus(w) \$\$\$ 0)
```
```    78   | bin_minus (w\$\$0) = bin_minus(w) \$\$ 0;
```
```    79
```
```    80 (*** Multiplication ***)
```
```    81
```
```    82 (*product of two bins; a factor of 0 might cause leading 0s in result*)
```
```    83 fun bin_mult (Pls, _) = Pls
```
```    84   | bin_mult (Min, v) = bin_minus v
```
```    85   | bin_mult (w\$\$1, v) = bin_add(bin_mult(w,v) \$\$\$ 0,  v)
```
```    86   | bin_mult (w\$\$0, v) = bin_mult(w,v) \$\$\$ 0;
```
```    87
```
```    88 (*** Testing ***)
```
```    89
```
```    90 (*tests addition*)
```
```    91 fun checksum m n =
```
```    92     let val wm = binary_of_int m
```
```    93         and wn = binary_of_int n
```
```    94         val wsum = bin_add(wm,wn)
```
```    95     in  if m+n = int_of_binary wsum then (wm, wn, wsum, m+n)
```
```    96         else raise Match
```
```    97     end;
```
```    98
```
```    99 fun bfact n = if n=0 then  Pls\$\$1
```
```   100               else  bin_mult(binary_of_int n, bfact(n-1));
```
```   101
```
```   102 (*Examples...
```
```   103 bfact 5;
```
```   104 int_of_binary it;
```
```   105 bfact 69;
```
```   106 int_of_binary it;
```
```   107
```
```   108 (*For {HOL,ZF}/ex/BinEx.ML*)
```
```   109 bin_add(binary_of_int 13, binary_of_int 19);
```
```   110 bin_add(binary_of_int 1234, binary_of_int 5678);
```
```   111 bin_add(binary_of_int 1359, binary_of_int ~2468);
```
```   112 bin_add(binary_of_int 93746, binary_of_int ~46375);
```
```   113 bin_minus(binary_of_int 65745);
```
```   114 bin_minus(binary_of_int ~54321);
```
```   115 bin_mult(binary_of_int 13, binary_of_int 19);
```
```   116 bin_mult(binary_of_int ~84, binary_of_int 51);
```
```   117 bin_mult(binary_of_int 255, binary_of_int 255);
```
```   118 bin_mult(binary_of_int 1359, binary_of_int ~2468);
```
```   119
```
```   120
```
```   121 (*leading zeros??*)
```
```   122 bin_add(binary_of_int 1234, binary_of_int ~1234);
```
```   123 bin_mult(binary_of_int 1234, Pls);
```
```   124
```
```   125 (*leading ones??*)
```
```   126 bin_add(binary_of_int 1, binary_of_int ~2);
```
```   127 bin_add(binary_of_int 1234, binary_of_int ~1235);
```
```   128 *)
```