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