src/HOL/Integ/Bin.thy
 author wenzelm Thu Jan 23 14:19:16 1997 +0100 (1997-01-23) changeset 2545 d10abc8c11fb parent 1632 39e146ac224c child 2988 d38f330e58b3 permissions -rw-r--r--
```     1 (*  Title:	HOL/Integ/Bin.thy
```
```     2     Authors:	Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     3 		David Spelt, University of Twente
```
```     4     Copyright	1994  University of Cambridge
```
```     5     Copyright   1996 University of Twente
```
```     6
```
```     7 Arithmetic on binary integers.
```
```     8
```
```     9    The sign Plus stands for an infinite string of leading F's.
```
```    10    The sign Minus stands for an infinite string of leading T's.
```
```    11
```
```    12 A number can have multiple representations, namely leading F's with sign
```
```    13 Plus and leading T's with sign Minus.  See twos-compl.ML/int_of_binary for
```
```    14 the numerical interpretation.
```
```    15
```
```    16 The representation expects that (m mod 2) is 0 or 1, even if m is negative;
```
```    17 For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
```
```    18
```
```    19 Division is not defined yet!
```
```    20 *)
```
```    21
```
```    22 Bin = Integ +
```
```    23
```
```    24 syntax
```
```    25   "_Int"           :: xnum => int        ("_")
```
```    26
```
```    27 datatype
```
```    28    bin = Plus
```
```    29         | Minus
```
```    30         | Bcons bin bool
```
```    31
```
```    32 consts
```
```    33   integ_of_bin     :: bin=>int
```
```    34   norm_Bcons       :: [bin,bool]=>bin
```
```    35   bin_succ         :: bin=>bin
```
```    36   bin_pred         :: bin=>bin
```
```    37   bin_minus        :: bin=>bin
```
```    38   bin_add,bin_mult :: [bin,bin]=>bin
```
```    39   h_bin :: [bin,bool,bin]=>bin
```
```    40
```
```    41 (*norm_Bcons adds a bit, suppressing leading 0s and 1s*)
```
```    42
```
```    43 primrec norm_Bcons bin
```
```    44   norm_Plus  "norm_Bcons Plus  b = (if b then (Bcons Plus b) else Plus)"
```
```    45   norm_Minus "norm_Bcons Minus b = (if b then Minus else (Bcons Minus b))"
```
```    46   norm_Bcons "norm_Bcons (Bcons w' x') b = Bcons (Bcons w' x') b"
```
```    47
```
```    48 primrec integ_of_bin bin
```
```    49   iob_Plus  "integ_of_bin Plus = \$#0"
```
```    50   iob_Minus "integ_of_bin Minus = \$~(\$#1)"
```
```    51   iob_Bcons "integ_of_bin(Bcons w x) = (if x then \$#1 else \$#0) + (integ_of_bin w) + (integ_of_bin w)"
```
```    52
```
```    53 primrec bin_succ bin
```
```    54   succ_Plus  "bin_succ Plus = Bcons Plus True"
```
```    55   succ_Minus "bin_succ Minus = Plus"
```
```    56   succ_Bcons "bin_succ(Bcons w x) = (if x then (Bcons (bin_succ w) False) else (norm_Bcons w True))"
```
```    57
```
```    58 primrec bin_pred bin
```
```    59   pred_Plus  "bin_pred(Plus) = Minus"
```
```    60   pred_Minus "bin_pred(Minus) = Bcons Minus False"
```
```    61   pred_Bcons "bin_pred(Bcons w x) = (if x then (norm_Bcons w False) else (Bcons (bin_pred w) True))"
```
```    62
```
```    63 primrec bin_minus bin
```
```    64   min_Plus  "bin_minus Plus = Plus"
```
```    65   min_Minus "bin_minus Minus = Bcons Plus True"
```
```    66   min_Bcons "bin_minus(Bcons w x) = (if x then (bin_pred (Bcons (bin_minus w) False)) else (Bcons (bin_minus w) False))"
```
```    67
```
```    68 primrec bin_add bin
```
```    69   add_Plus  "bin_add Plus w = w"
```
```    70   add_Minus "bin_add Minus w = bin_pred w"
```
```    71   add_Bcons "bin_add (Bcons v x) w = h_bin v x w"
```
```    72
```
```    73 primrec bin_mult bin
```
```    74   mult_Plus "bin_mult Plus w = Plus"
```
```    75   mult_Minus "bin_mult Minus w = bin_minus w"
```
```    76   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))"
```
```    77
```
```    78 primrec h_bin bin
```
```    79   h_Plus  "h_bin v x Plus =  Bcons v x"
```
```    80   h_Minus "h_bin v x Minus = bin_pred (Bcons v x)"
```
```    81   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)"
```
```    82
```
```    83 end
```
```    84
```
```    85 ML
```
```    86
```
```    87 (** Concrete syntax for integers **)
```
```    88
```
```    89 local
```
```    90   open Syntax;
```
```    91
```
```    92   (* Bits *)
```
```    93
```
```    94   fun mk_bit 0 = const "False"
```
```    95     | mk_bit 1 = const "True"
```
```    96     | mk_bit _ = sys_error "mk_bit";
```
```    97
```
```    98   fun dest_bit (Const ("False", _)) = 0
```
```    99     | dest_bit (Const ("True", _)) = 1
```
```   100     | dest_bit _ = raise Match;
```
```   101
```
```   102
```
```   103   (* Bit strings *)   (*we try to handle superfluous leading digits nicely*)
```
```   104
```
```   105   fun prefix_len _ [] = 0
```
```   106     | prefix_len pred (x :: xs) =
```
```   107         if pred x then 1 + prefix_len pred xs else 0;
```
```   108
```
```   109   fun mk_bin str =
```
```   110     let
```
```   111       val (sign, digs) =
```
```   112         (case explode str of
```
```   113           "#" :: "~" :: cs => (~1, cs)
```
```   114         | "#" :: cs => (1, cs)
```
```   115         | _ => raise ERROR);
```
```   116
```
```   117       val zs = prefix_len (equal "0") digs;
```
```   118
```
```   119       fun bin_of 0 = replicate zs 0
```
```   120         | bin_of ~1 = replicate zs 1 @ [~1]
```
```   121         | bin_of n = (n mod 2) :: bin_of (n div 2);
```
```   122
```
```   123       fun term_of [] = const "Plus"
```
```   124         | term_of [~1] = const "Minus"
```
```   125         | term_of (b :: bs) = const "Bcons" \$ term_of bs \$ mk_bit b;
```
```   126     in
```
```   127       term_of (bin_of (sign * (#1 (scan_int digs))))
```
```   128     end;
```
```   129
```
```   130   fun dest_bin tm =
```
```   131     let
```
```   132       fun bin_of (Const ("Plus", _)) = []
```
```   133         | bin_of (Const ("Minus", _)) = [~1]
```
```   134         | bin_of (Const ("Bcons", _) \$ bs \$ b) = dest_bit b :: bin_of bs
```
```   135         | bin_of _ = raise Match;
```
```   136
```
```   137       fun int_of [] = 0
```
```   138         | int_of (b :: bs) = b + 2 * int_of bs;
```
```   139
```
```   140       val rev_digs = bin_of tm;
```
```   141       val (sign, zs) =
```
```   142         (case rev rev_digs of
```
```   143           ~1 :: bs => ("~", prefix_len (equal 1) bs)
```
```   144         | bs => ("", prefix_len (equal 0) bs));
```
```   145       val num = string_of_int (abs (int_of rev_digs));
```
```   146     in
```
```   147       "#" ^ sign ^ implode (replicate zs "0") ^ num
```
```   148     end;
```
```   149
```
```   150
```
```   151   (* translation of integer constant tokens to and from binary *)
```
```   152
```
```   153   fun int_tr (*"_Int"*) [t as Free (str, _)] =
```
```   154         (const "integ_of_bin" \$
```
```   155           (mk_bin str handle ERROR => raise_term "int_tr" [t]))
```
```   156     | int_tr (*"_Int"*) ts = raise_term "int_tr" ts;
```
```   157
```
```   158   fun int_tr' (*"integ_of"*) [t] = const "_Int" \$ free (dest_bin t)
```
```   159     | int_tr' (*"integ_of"*) _ = raise Match;
```
```   160 in
```
```   161   val parse_translation = [("_Int", int_tr)];
```
```   162   val print_translation = [("integ_of_bin", int_tr')];
```
```   163 end;
```