(* Title: HOL/Integ/Bin.thy
ID: $Id$
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 Pls stands for an infinite string of leading F's.
The sign Min stands for an infinite string of leading T's.
A number can have multiple representations, namely leading F's with sign
Pls and leading T's with sign Min. See ZF/ex/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! To do it efficiently requires computing the
quotient and remainder using ML and checking the answer using multiplication
by proof. Then uniqueness of the quotient and remainder yields theorems
quoting the previously computed values. (Or code an oracle...)
*)
Bin = Int + Numeral +
consts
NCons :: [bin,bool]=>bin
bin_succ :: bin=>bin
bin_pred :: bin=>bin
bin_minus :: bin=>bin
bin_add,bin_mult :: [bin,bin]=>bin
adding :: [bin,bool,bin]=>bin
(*NCons inserts a bit, suppressing leading 0s and 1s*)
primrec
NCons_Pls "NCons Pls b = (if b then (Pls BIT b) else Pls)"
NCons_Min "NCons Min b = (if b then Min else (Min BIT b))"
NCons_BIT "NCons (w BIT x) b = (w BIT x) BIT b"
instance
int :: numeral
primrec
number_of_Pls "number_of Pls = int 0"
number_of_Min "number_of Min = - (int 1)"
number_of_BIT "number_of(w BIT x) = (if x then int 1 else int 0) +
(number_of w) + (number_of w)"
primrec
bin_succ_Pls "bin_succ Pls = Pls BIT True"
bin_succ_Min "bin_succ Min = Pls"
bin_succ_BIT "bin_succ(w BIT x) =
(if x then bin_succ w BIT False
else NCons w True)"
primrec
bin_pred_Pls "bin_pred Pls = Min"
bin_pred_Min "bin_pred Min = Min BIT False"
bin_pred_BIT "bin_pred(w BIT x) =
(if x then NCons w False
else (bin_pred w) BIT True)"
primrec
bin_minus_Pls "bin_minus Pls = Pls"
bin_minus_Min "bin_minus Min = Pls BIT True"
bin_minus_BIT "bin_minus(w BIT x) =
(if x then bin_pred (NCons (bin_minus w) False)
else bin_minus w BIT False)"
primrec
bin_add_Pls "bin_add Pls w = w"
bin_add_Min "bin_add Min w = bin_pred w"
bin_add_BIT "bin_add (v BIT x) w = adding v x w"
primrec
"adding v x Pls = v BIT x"
"adding v x Min = bin_pred (v BIT x)"
"adding v x (w BIT y) =
NCons (bin_add v (if (x & y) then bin_succ w else w))
(x~=y)"
primrec
bin_mult_Pls "bin_mult Pls w = Pls"
bin_mult_Min "bin_mult Min w = bin_minus w"
bin_mult_BIT "bin_mult (v BIT x) w =
(if x then (bin_add (NCons (bin_mult v w) False) w)
else (NCons (bin_mult v w) False))"
end