# HG changeset patch # User lcp # Date 793901331 -3600 # Node ID 80b581036036253cca65204315243041a3c0064f # Parent 5240dcd12adbd83e0cae87fb20d2e43592b45368 Added integer numerals (mostly due to Markus Wenzel) renamed the infix 2239 to the constant Bcons, as numerals eliminate the need for the infix. diff -r 5240dcd12adb -r 80b581036036 src/ZF/ex/Bin.thy --- a/src/ZF/ex/Bin.thy Mon Feb 27 17:06:19 1995 +0100 +++ b/src/ZF/ex/Bin.thy Mon Feb 27 17:08:51 1995 +0100 @@ -1,60 +1,171 @@ -(* Title: ZF/ex/Bin.thy +(* Title: ZF/ex/Bin.thy ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge Arithmetic on binary integers. + + The sign Plus stands for an infinite string of leading 0's. + The sign Minus stands for an infinite string of leading 1's. + +A number can have multiple representations, namely leading 0's with sign +Plus and leading 1's with sign Minus. See twos-compl.ML/int_of_binary for +the numerical interpretation. + +The representation expects that (m mod 2) is 0 or 1, even if m is negative; +For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1 + +Division is not defined yet! *) Bin = Integ + Univ + "twos_compl" + + consts bin_rec :: "[i, i, i, [i,i,i]=>i] => i" integ_of_bin :: "i=>i" + norm_Bcons :: "[i,i]=>i" bin_succ :: "i=>i" bin_pred :: "i=>i" bin_minus :: "i=>i" bin_add,bin_mult :: "[i,i]=>i" - bin :: "i" + bin :: "i" + +syntax + "_Int" :: "xnum => i" ("_") datatype "bin" = Plus | Minus - | "$$" ("w: bin", "b: bool") (infixl 60) + | Bcons ("w: bin", "b: bool") type_intrs "[bool_into_univ]" - + + defs bin_rec_def "bin_rec(z,a,b,h) == \ \ Vrec(z, %z g. bin_case(a, b, %w x. h(w, x, g`w), z))" - integ_of_bin_def + integ_of_bin_def "integ_of_bin(w) == bin_rec(w, $#0, $~($#1), %w x r. $#x $+ r $+ r)" + (** recall that cond(1,b,c)=b and cond(0,b,c)=0 **) + + (*norm_Bcons adds a bit, suppressing leading 0s and 1s*) + norm_Bcons_def + "norm_Bcons(w,b) == \ +\ bin_case(cond(b,Bcons(w,b),w), cond(b,w,Bcons(w,b)), \ +\ %w' x'. Bcons(w,b), w)" + bin_succ_def - "bin_succ(w0) == bin_rec(w0, Plus$$1, Plus, %w x r. cond(x, r$$0, w$$1))" + "bin_succ(w0) == \ +\ bin_rec(w0, Bcons(Plus,1), Plus, \ +\ %w x r. cond(x, Bcons(r,0), norm_Bcons(w,1)))" bin_pred_def "bin_pred(w0) == \ -\ bin_rec(w0, Minus, Minus$$0, %w x r. cond(x, w$$0, r$$1))" +\ bin_rec(w0, Minus, Bcons(Minus,0), \ +\ %w x r. cond(x, norm_Bcons(w,0), Bcons(r,1)))" bin_minus_def "bin_minus(w0) == \ -\ bin_rec(w0, Plus, Plus$$1, %w x r. cond(x, bin_pred(r$$0), r$$0))" +\ bin_rec(w0, Plus, Bcons(Plus,1), \ +\ %w x r. cond(x, bin_pred(Bcons(r,0)), Bcons(r,0)))" bin_add_def - "bin_add(v0,w0) == \ -\ bin_rec(v0, \ -\ lam w:bin. w, \ -\ lam w:bin. bin_pred(w), \ -\ %v x r. lam w1:bin. \ -\ bin_rec(w1, v$$x, bin_pred(v$$x), \ -\ %w y s. (r`cond(x and y, bin_succ(w), w)) \ -\ $$ (x xor y))) ` w0" + "bin_add(v0,w0) == \ +\ bin_rec(v0, \ +\ lam w:bin. w, \ +\ lam w:bin. bin_pred(w), \ +\ %v x r. lam w1:bin. \ +\ bin_rec(w1, Bcons(v,x), bin_pred(Bcons(v,x)), \ +\ %w y s. norm_Bcons(r`cond(x and y, bin_succ(w), w), \ +\ x xor y))) ` w0" bin_mult_def - "bin_mult(v0,w) == \ -\ bin_rec(v0, Plus, bin_minus(w), \ -\ %v x r. cond(x, bin_add(r$$0,w), r$$0))" + "bin_mult(v0,w) == \ +\ bin_rec(v0, Plus, bin_minus(w), \ +\ %v x r. cond(x, bin_add(norm_Bcons(r,0),w), norm_Bcons(r,0)))" end + + +ML + +(** Concrete syntax for integers **) + +local + open Syntax; + + (* Bits *) + + fun mk_bit 0 = const "0" + | mk_bit 1 = const "succ" $ const "0" + | mk_bit _ = sys_error "mk_bit"; + + fun dest_bit (Const ("0", _)) = 0 + | dest_bit (Const ("succ", _) $ Const ("0", _)) = 1 + | dest_bit _ = raise Match; + + + (* Bit strings *) (*we try to handle superfluous leading digits nicely*) + + fun prefix_len _ [] = 0 + | prefix_len pred (x :: xs) = + if pred x then 1 + prefix_len pred xs else 0; + + fun mk_bin str = + let + val (sign, digs) = + (case explode str of + "#" :: "~" :: cs => (~1, cs) + | "#" :: cs => (1, cs) + | _ => raise ERROR); + + val zs = prefix_len (equal "0") digs; + + fun bin_of 0 = replicate zs 0 + | bin_of ~1 = replicate zs 1 @ [~1] + | bin_of n = (n mod 2) :: bin_of (n div 2); + + fun term_of [] = const "Plus" + | term_of [~1] = const "Minus" + | term_of (b :: bs) = const "Bcons" $ term_of bs $ mk_bit b; + in + term_of (bin_of (sign * (#1 (scan_int digs)))) + end; + + fun dest_bin tm = + let + fun bin_of (Const ("Plus", _)) = [] + | bin_of (Const ("Minus", _)) = [~1] + | bin_of (Const ("Bcons", _) $ bs $ b) = dest_bit b :: bin_of bs + | bin_of _ = raise Match; + + fun int_of [] = 0 + | int_of (b :: bs) = b + 2 * int_of bs; + + val rev_digs = bin_of tm; + val (sign, zs) = + (case rev rev_digs of + ~1 :: bs => ("~", prefix_len (equal 1) bs) + | bs => ("", prefix_len (equal 0) bs)); + val num = string_of_int (abs (int_of rev_digs)); + in + "#" ^ sign ^ implode (replicate zs "0") ^ num + end; + + + (* translation of integer constant tokens to and from binary *) + + fun int_tr (*"_Int"*) [t as Free (str, _)] = + (const "integ_of_bin" $ + (mk_bin str handle ERROR => raise_term "int_tr" [t])) + | int_tr (*"_Int"*) ts = raise_term "int_tr" ts; + + fun int_tr' (*"integ_of"*) [t] = const "_Int" $ free (dest_bin t) + | int_tr' (*"integ_of"*) _ = raise Match; +in + val parse_translation = [("_Int", int_tr)]; + val print_translation = [("integ_of_bin", int_tr')]; +end;