src/ZF/Integ/twos_compl.ML
 changeset 23146 0bc590051d95 parent 23145 5d8faadf3ecf child 23147 a5db2f7d7654
```     1.1 --- a/src/ZF/Integ/twos_compl.ML	Thu May 31 11:00:06 2007 +0200
1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,128 +0,0 @@
1.4 -(*  Title:      ZF/ex/twos-compl.ML
1.5 -    ID:         \$Id\$
1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 -    Copyright   1993  University of Cambridge
1.8 -
1.9 -ML code for Arithmetic on binary integers; the model for theory Bin
1.10 -
1.11 -   The sign Pls stands for an infinite string of leading 0s.
1.12 -   The sign Min stands for an infinite string of leading 1s.
1.13 -
1.14 -See int_of_binary for the numerical interpretation.  A number can have
1.15 -multiple representations, namely leading 0s with sign Pls and leading 1s with
1.16 -sign Min.  A number is in NORMAL FORM if it has no such extra bits.
1.17 -
1.18 -The representation expects that (m mod 2) is 0 or 1, even if m is negative;
1.19 -For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
1.20 -
1.21 -Still needs division!
1.22 -
1.23 -print_depth 40;
1.24 -System.Control.Print.printDepth := 350;
1.25 -*)
1.26 -
1.27 -infix 5 \$\$ \$\$\$
1.28 -
1.29 -(*Recursive datatype of binary integers*)
1.30 -datatype bin = Pls | Min | \$\$ of bin * int;
1.31 -
1.32 -(** Conversions between bin and int **)
1.33 -
1.34 -fun int_of_binary Pls = 0
1.35 -  | int_of_binary Min = ~1
1.36 -  | int_of_binary (w\$\$b) = 2 * int_of_binary w + b;
1.37 -
1.38 -fun binary_of_int 0 = Pls
1.39 -  | binary_of_int ~1 = Min
1.40 -  | binary_of_int n = binary_of_int (n div 2) \$\$ (n mod 2);
1.41 -
1.43 -
1.44 -(*Attach a bit while preserving the normal form.  Cases left as default
1.45 -  are Pls\$\$\$1 and Min\$\$\$0. *)
1.46 -fun  Pls \$\$\$ 0 = Pls
1.47 -  | Min \$\$\$ 1 = Min
1.48 -  |     v \$\$\$ x = v\$\$x;
1.49 -
1.50 -(*Successor of an integer, assumed to be in normal form.
1.51 -  If w\$\$1 is normal then w is not Min, so bin_succ(w) \$\$ 0 is normal.
1.52 -  But Min\$\$0 is normal while Min\$\$1 is not.*)
1.53 -fun bin_succ Pls = Pls\$\$1
1.54 -  | bin_succ Min = Pls
1.55 -  | bin_succ (w\$\$1) = bin_succ(w) \$\$ 0
1.56 -  | bin_succ (w\$\$0) = w \$\$\$ 1;
1.57 -
1.58 -(*Predecessor of an integer, assumed to be in normal form.
1.59 -  If w\$\$0 is normal then w is not Pls, so bin_pred(w) \$\$ 1 is normal.
1.60 -  But Pls\$\$1 is normal while Pls\$\$0 is not.*)
1.61 -fun bin_pred Pls = Min
1.62 -  | bin_pred Min = Min\$\$0
1.63 -  | bin_pred (w\$\$1) = w \$\$\$ 0
1.64 -  | bin_pred (w\$\$0) = bin_pred(w) \$\$ 1;
1.65 -
1.66 -(*Sum of two binary integers in normal form.
1.67 -  Ensure last \$\$ preserves normal form! *)
1.68 -fun bin_add (Pls, w) = w
1.69 -  | bin_add (Min, w) = bin_pred w
1.70 -  | bin_add (v\$\$x, Pls) = v\$\$x
1.71 -  | bin_add (v\$\$x, Min) = bin_pred (v\$\$x)
1.72 -  | bin_add (v\$\$x, w\$\$y) =
1.73 -      bin_add(v, if x+y=2 then bin_succ w else w) \$\$\$ ((x+y) mod 2);
1.74 -
1.75 -(*** Subtraction ***)
1.76 -
1.77 -(*Unary minus*)
1.78 -fun bin_minus Pls = Pls
1.79 -  | bin_minus Min = Pls\$\$1
1.80 -  | bin_minus (w\$\$1) = bin_pred (bin_minus(w) \$\$\$ 0)
1.81 -  | bin_minus (w\$\$0) = bin_minus(w) \$\$ 0;
1.82 -
1.83 -(*** Multiplication ***)
1.84 -
1.85 -(*product of two bins; a factor of 0 might cause leading 0s in result*)
1.86 -fun bin_mult (Pls, _) = Pls
1.87 -  | bin_mult (Min, v) = bin_minus v
1.88 -  | bin_mult (w\$\$1, v) = bin_add(bin_mult(w,v) \$\$\$ 0,  v)
1.89 -  | bin_mult (w\$\$0, v) = bin_mult(w,v) \$\$\$ 0;
1.90 -
1.91 -(*** Testing ***)
1.92 -
1.94 -fun checksum m n =
1.95 -    let val wm = binary_of_int m
1.96 -        and wn = binary_of_int n
1.97 -        val wsum = bin_add(wm,wn)
1.98 -    in  if m+n = int_of_binary wsum then (wm, wn, wsum, m+n)
1.99 -        else raise Match
1.100 -    end;
1.101 -
1.102 -fun bfact n = if n=0 then  Pls\$\$1
1.103 -              else  bin_mult(binary_of_int n, bfact(n-1));
1.104 -
1.105 -(*Examples...
1.106 -bfact 5;
1.107 -int_of_binary it;
1.108 -bfact 69;
1.109 -int_of_binary it;
1.110 -
1.111 -(*For {HOL,ZF}/ex/BinEx.ML*)
1.116 -bin_minus(binary_of_int 65745);
1.117 -bin_minus(binary_of_int ~54321);
1.118 -bin_mult(binary_of_int 13, binary_of_int 19);
1.119 -bin_mult(binary_of_int ~84, binary_of_int 51);
1.120 -bin_mult(binary_of_int 255, binary_of_int 255);
1.121 -bin_mult(binary_of_int 1359, binary_of_int ~2468);
1.122 -
1.123 -