author lcp Mon, 27 Feb 1995 17:08:51 +0100 changeset 905 80b581036036 parent 904 5240dcd12adb child 906 6cd9c397f36a
Added integer numerals (mostly due to Markus Wenzel) renamed the infix 2239 to the constant Bcons, as numerals eliminate the need for the infix.
 src/ZF/ex/Bin.thy file | annotate | diff | comparison | revisions
```--- 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

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		   :: "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_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_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_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;```