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.42 -(*** Addition ***)
    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.93 -(*tests addition*)
    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.112 -bin_add(binary_of_int 13, binary_of_int 19);
   1.113 -bin_add(binary_of_int 1234, binary_of_int 5678);
   1.114 -bin_add(binary_of_int 1359, binary_of_int ~2468);
   1.115 -bin_add(binary_of_int 93746, binary_of_int ~46375);
   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 -
   1.124 -(*leading zeros??*)
   1.125 -bin_add(binary_of_int 1234, binary_of_int ~1234);
   1.126 -bin_mult(binary_of_int 1234, Pls);
   1.127 -
   1.128 -(*leading ones??*)
   1.129 -bin_add(binary_of_int 1, binary_of_int ~2);
   1.130 -bin_add(binary_of_int 1234, binary_of_int ~1235);
   1.131 -*)