--- 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;