src/HOL/Integ/Bin.thy

added if_cancel later to simpset

(*  Title:	HOL/Integ/Bin.thy
    Authors:	Lawrence C Paulson, Cambridge University Computer Laboratory
		David Spelt, University of Twente 
    Copyright	1994  University of Cambridge
    Copyright   1996 University of Twente

Arithmetic on binary integers.

   The sign Plus stands for an infinite string of leading F's.
   The sign Minus stands for an infinite string of leading T's.

A number can have multiple representations, namely leading F's with sign
Plus and leading T'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 + 

syntax
  "_Int"           :: xnum => int        ("_")

datatype
   bin = Plus
        | Minus
        | Bcons bin bool

consts
  integ_of_bin     :: bin=>int
  norm_Bcons       :: [bin,bool]=>bin
  bin_succ         :: bin=>bin
  bin_pred         :: bin=>bin
  bin_minus        :: bin=>bin
  bin_add,bin_mult :: [bin,bin]=>bin
  h_bin :: [bin,bool,bin]=>bin

(*norm_Bcons adds a bit, suppressing leading 0s and 1s*)

primrec norm_Bcons bin
  norm_Plus  "norm_Bcons Plus  b = (if b then (Bcons Plus b) else Plus)"
  norm_Minus "norm_Bcons Minus b = (if b then Minus else (Bcons Minus b))"
  norm_Bcons "norm_Bcons (Bcons w' x') b = Bcons (Bcons w' x') b"
 
primrec integ_of_bin bin
  iob_Plus  "integ_of_bin Plus = $#0"
  iob_Minus "integ_of_bin Minus = $~($#1)"
  iob_Bcons "integ_of_bin(Bcons w x) = (if x then $#1 else $#0) + (integ_of_bin w) + (integ_of_bin w)" 

primrec bin_succ bin
  succ_Plus  "bin_succ Plus = Bcons Plus True" 
  succ_Minus "bin_succ Minus = Plus"
  succ_Bcons "bin_succ(Bcons w x) = (if x then (Bcons (bin_succ w) False) else (norm_Bcons w True))"

primrec bin_pred bin
  pred_Plus  "bin_pred(Plus) = Minus"
  pred_Minus "bin_pred(Minus) = Bcons Minus False"
  pred_Bcons "bin_pred(Bcons w x) = (if x then (norm_Bcons w False) else (Bcons (bin_pred w) True))"
 
primrec bin_minus bin
  min_Plus  "bin_minus Plus = Plus"
  min_Minus "bin_minus Minus = Bcons Plus True"
  min_Bcons "bin_minus(Bcons w x) = (if x then (bin_pred (Bcons (bin_minus w) False)) else (Bcons (bin_minus w) False))"

primrec bin_add bin
  add_Plus  "bin_add Plus w = w"
  add_Minus "bin_add Minus w = bin_pred w"
  add_Bcons "bin_add (Bcons v x) w = h_bin v x w"

primrec bin_mult bin
  mult_Plus "bin_mult Plus w = Plus"
  mult_Minus "bin_mult Minus w = bin_minus w"
  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))"

primrec h_bin bin
  h_Plus  "h_bin v x Plus =  Bcons v x"
  h_Minus "h_bin v x Minus = bin_pred (Bcons v x)"
  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)" 

end

ML

(** Concrete syntax for integers **)

local
  open Syntax;

  (* Bits *)

  fun mk_bit 0 = const "False"
    | mk_bit 1 = const "True"
    | mk_bit _ = sys_error "mk_bit";

  fun dest_bit (Const ("False", _)) = 0
    | dest_bit (Const ("True", _)) = 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;