src/HOL/Integ/Bin.thy
 changeset 1632 39e146ac224c child 2988 d38f330e58b3
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Integ/Bin.thy	Fri Mar 29 13:18:26 1996 +0100
1.3 @@ -0,0 +1,163 @@
1.4 +(*  Title:	HOL/Integ/Bin.thy
1.5 +    Authors:	Lawrence C Paulson, Cambridge University Computer Laboratory
1.6 +		David Spelt, University of Twente
1.7 +    Copyright	1994  University of Cambridge
1.8 +    Copyright   1996 University of Twente
1.9 +
1.10 +Arithmetic on binary integers.
1.11 +
1.12 +   The sign Plus stands for an infinite string of leading F's.
1.13 +   The sign Minus stands for an infinite string of leading T's.
1.14 +
1.15 +A number can have multiple representations, namely leading F's with sign
1.16 +Plus and leading T's with sign Minus.  See twos-compl.ML/int_of_binary for
1.17 +the numerical interpretation.
1.18 +
1.19 +The representation expects that (m mod 2) is 0 or 1, even if m is negative;
1.20 +For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
1.21 +
1.22 +Division is not defined yet!
1.23 +*)
1.24 +
1.25 +Bin = Integ +
1.26 +
1.27 +syntax
1.28 +  "_Int"           :: xnum => int        ("_")
1.29 +
1.30 +datatype
1.31 +   bin = Plus
1.32 +        | Minus
1.33 +        | Bcons bin bool
1.34 +
1.35 +consts
1.36 +  integ_of_bin     :: bin=>int
1.37 +  norm_Bcons       :: [bin,bool]=>bin
1.38 +  bin_succ         :: bin=>bin
1.39 +  bin_pred         :: bin=>bin
1.40 +  bin_minus        :: bin=>bin
1.42 +  h_bin :: [bin,bool,bin]=>bin
1.43 +
1.45 +
1.46 +primrec norm_Bcons bin
1.47 +  norm_Plus  "norm_Bcons Plus  b = (if b then (Bcons Plus b) else Plus)"
1.48 +  norm_Minus "norm_Bcons Minus b = (if b then Minus else (Bcons Minus b))"
1.49 +  norm_Bcons "norm_Bcons (Bcons w' x') b = Bcons (Bcons w' x') b"
1.50 +
1.51 +primrec integ_of_bin bin
1.52 +  iob_Plus  "integ_of_bin Plus = \$#0"
1.53 +  iob_Minus "integ_of_bin Minus = \$~(\$#1)"
1.54 +  iob_Bcons "integ_of_bin(Bcons w x) = (if x then \$#1 else \$#0) + (integ_of_bin w) + (integ_of_bin w)"
1.55 +
1.56 +primrec bin_succ bin
1.57 +  succ_Plus  "bin_succ Plus = Bcons Plus True"
1.58 +  succ_Minus "bin_succ Minus = Plus"
1.59 +  succ_Bcons "bin_succ(Bcons w x) = (if x then (Bcons (bin_succ w) False) else (norm_Bcons w True))"
1.60 +
1.61 +primrec bin_pred bin
1.62 +  pred_Plus  "bin_pred(Plus) = Minus"
1.63 +  pred_Minus "bin_pred(Minus) = Bcons Minus False"
1.64 +  pred_Bcons "bin_pred(Bcons w x) = (if x then (norm_Bcons w False) else (Bcons (bin_pred w) True))"
1.65 +
1.66 +primrec bin_minus bin
1.67 +  min_Plus  "bin_minus Plus = Plus"
1.68 +  min_Minus "bin_minus Minus = Bcons Plus True"
1.69 +  min_Bcons "bin_minus(Bcons w x) = (if x then (bin_pred (Bcons (bin_minus w) False)) else (Bcons (bin_minus w) False))"
1.70 +
1.74 +  add_Bcons "bin_add (Bcons v x) w = h_bin v x w"
1.75 +
1.76 +primrec bin_mult bin
1.77 +  mult_Plus "bin_mult Plus w = Plus"
1.78 +  mult_Minus "bin_mult Minus w = bin_minus w"
1.79 +  mult_Bcons "bin_mult (Bcons v x) w = (if x then (bin_add (norm_Bcons (bin_mult v w) False) w) else (norm_Bcons (bin_mult v w) False))"
1.80 +
1.81 +primrec h_bin bin
1.82 +  h_Plus  "h_bin v x Plus =  Bcons v x"
1.83 +  h_Minus "h_bin v x Minus = bin_pred (Bcons v x)"
1.84 +  h_BCons "h_bin v x (Bcons w y) = norm_Bcons (bin_add v (if (x & y) then bin_succ w else w)) (x~=y)"
1.85 +
1.86 +end
1.87 +
1.88 +ML
1.89 +
1.90 +(** Concrete syntax for integers **)
1.91 +
1.92 +local
1.93 +  open Syntax;
1.94 +
1.95 +  (* Bits *)
1.96 +
1.97 +  fun mk_bit 0 = const "False"
1.98 +    | mk_bit 1 = const "True"
1.99 +    | mk_bit _ = sys_error "mk_bit";
1.100 +
1.101 +  fun dest_bit (Const ("False", _)) = 0
1.102 +    | dest_bit (Const ("True", _)) = 1
1.103 +    | dest_bit _ = raise Match;
1.104 +
1.105 +
1.106 +  (* Bit strings *)   (*we try to handle superfluous leading digits nicely*)
1.107 +
1.108 +  fun prefix_len _ [] = 0
1.109 +    | prefix_len pred (x :: xs) =
1.110 +        if pred x then 1 + prefix_len pred xs else 0;
1.111 +
1.112 +  fun mk_bin str =
1.113 +    let
1.114 +      val (sign, digs) =
1.115 +        (case explode str of
1.116 +          "#" :: "~" :: cs => (~1, cs)
1.117 +        | "#" :: cs => (1, cs)
1.118 +        | _ => raise ERROR);
1.119 +
1.120 +      val zs = prefix_len (equal "0") digs;
1.121 +
1.122 +      fun bin_of 0 = replicate zs 0
1.123 +        | bin_of ~1 = replicate zs 1 @ [~1]
1.124 +        | bin_of n = (n mod 2) :: bin_of (n div 2);
1.125 +
1.126 +      fun term_of [] = const "Plus"
1.127 +        | term_of [~1] = const "Minus"
1.128 +        | term_of (b :: bs) = const "Bcons" \$ term_of bs \$ mk_bit b;
1.129 +    in
1.130 +      term_of (bin_of (sign * (#1 (scan_int digs))))
1.131 +    end;
1.132 +
1.133 +  fun dest_bin tm =
1.134 +    let
1.135 +      fun bin_of (Const ("Plus", _)) = []
1.136 +        | bin_of (Const ("Minus", _)) = [~1]
1.137 +        | bin_of (Const ("Bcons", _) \$ bs \$ b) = dest_bit b :: bin_of bs
1.138 +        | bin_of _ = raise Match;
1.139 +
1.140 +      fun int_of [] = 0
1.141 +        | int_of (b :: bs) = b + 2 * int_of bs;
1.142 +
1.143 +      val rev_digs = bin_of tm;
1.144 +      val (sign, zs) =
1.145 +        (case rev rev_digs of
1.146 +          ~1 :: bs => ("~", prefix_len (equal 1) bs)
1.147 +        | bs => ("", prefix_len (equal 0) bs));
1.148 +      val num = string_of_int (abs (int_of rev_digs));
1.149 +    in
1.150 +      "#" ^ sign ^ implode (replicate zs "0") ^ num
1.151 +    end;
1.152 +
1.153 +
1.154 +  (* translation of integer constant tokens to and from binary *)
1.155 +
1.156 +  fun int_tr (*"_Int"*) [t as Free (str, _)] =
1.157 +        (const "integ_of_bin" \$
1.158 +          (mk_bin str handle ERROR => raise_term "int_tr" [t]))
1.159 +    | int_tr (*"_Int"*) ts = raise_term "int_tr" ts;
1.160 +
1.161 +  fun int_tr' (*"integ_of"*) [t] = const "_Int" \$ free (dest_bin t)
1.162 +    | int_tr' (*"integ_of"*) _ = raise Match;
1.163 +in
1.164 +  val parse_translation = [("_Int", int_tr)];
1.165 +  val print_translation = [("integ_of_bin", int_tr')];
1.166 +end;
```