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--
added AxClasses test;
     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;