src/HOL/Integ/Bin.thy

Removed obsolete function "Funs".

(*  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
*)

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

(*NCons inserts a bit, suppressing leading 0s and 1s*)
primrec
  NCons_Pls "NCons bin.Pls b = (if b then (bin.Pls BIT b) else bin.Pls)"
  NCons_Min "NCons bin.Min b = (if b then bin.Min else (bin.Min BIT b))"
  NCons_BIT "NCons (w BIT x) b = (w BIT x) BIT b"

instance
  int :: number

primrec (*the type constraint is essential!*)
  number_of_Pls  "number_of bin.Pls = 0"
  number_of_Min  "number_of bin.Min = - (1::int)"
  number_of_BIT  "number_of(w BIT x) = (if x then 1 else 0) +
	                               (number_of w) + (number_of w)" 

primrec
  bin_succ_Pls  "bin_succ bin.Pls = bin.Pls BIT True" 
  bin_succ_Min  "bin_succ bin.Min = bin.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 bin.Pls = bin.Min"
  bin_pred_Min  "bin_pred bin.Min = bin.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 bin.Pls = bin.Pls"
  bin_minus_Min  "bin_minus bin.Min = bin.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 bin.Pls w = w"
  bin_add_Min  "bin_add bin.Min w = bin_pred w"
  bin_add_BIT
    "bin_add (v BIT x) w = 
       (case w of Pls => v BIT x
                | Min => bin_pred (v BIT 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 bin.Pls w = bin.Pls"
  bin_mult_Min  "bin_mult bin.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