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