author  wenzelm 
Wed, 14 Nov 2001 18:46:07 +0100  
changeset 12182  3f820a21dcc1 
parent 11381  4ab3b7b0938f 
child 13560  d9651081578b 
permissions  rwrr 
5528  1 
(* Title: ZF/ex/Bin.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1994 University of Cambridge 

5 

6 
Arithmetic on binary integers. 

7 

8 
The sign Pls stands for an infinite string of leading 0's. 

9 
The sign Min stands for an infinite string of leading 1's. 

10 

11 
A number can have multiple representations, namely leading 0's with sign 

12 
Pls and leading 1's with sign Min. See twoscompl.ML/int_of_binary for 

13 
the numerical interpretation. 

14 

15 
The representation expects that (m mod 2) is 0 or 1, even if m is negative; 

16 
For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1 

17 
*) 

18 

9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset

19 
Bin = Int + Datatype + 
5528  20 

6117  21 
consts bin :: i 
22 
datatype 

23 
"bin" = Pls 

24 
 Min 

9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset

25 
 Bit ("w: bin", "b: bool") (infixl "BIT" 90) 
6117  26 

27 
syntax 

28 
"_Int" :: xnum => i ("_") 

29 

5528  30 
consts 
31 
integ_of :: i=>i 

32 
NCons :: [i,i]=>i 

33 
bin_succ :: i=>i 

34 
bin_pred :: i=>i 

35 
bin_minus :: i=>i 

36 
bin_add :: [i,i]=>i 

9207  37 
bin_adder :: i=>i 
5528  38 
bin_mult :: [i,i]=>i 
39 

6046  40 
primrec 
6153  41 
integ_of_Pls "integ_of (Pls) = $# 0" 
9548  42 
integ_of_Min "integ_of (Min) = $($#1)" 
6153  43 
integ_of_BIT "integ_of (w BIT b) = $#b $+ integ_of(w) $+ integ_of(w)" 
5528  44 

45 
(** recall that cond(1,b,c)=b and cond(0,b,c)=0 **) 

46 

6046  47 
primrec (*NCons adds a bit, suppressing leading 0s and 1s*) 
6153  48 
NCons_Pls "NCons (Pls,b) = cond(b,Pls BIT b,Pls)" 
49 
NCons_Min "NCons (Min,b) = cond(b,Min,Min BIT b)" 

50 
NCons_BIT "NCons (w BIT c,b) = w BIT c BIT b" 

5528  51 

6153  52 
primrec (*successor. If a BIT, can change a 0 to a 1 without recursion.*) 
53 
bin_succ_Pls "bin_succ (Pls) = Pls BIT 1" 

54 
bin_succ_Min "bin_succ (Min) = Pls" 

55 
bin_succ_BIT "bin_succ (w BIT b) = cond(b, bin_succ(w) BIT 0, NCons(w,1))" 

5528  56 

6046  57 
primrec (*predecessor*) 
6153  58 
bin_pred_Pls "bin_pred (Pls) = Min" 
59 
bin_pred_Min "bin_pred (Min) = Min BIT 0" 

60 
bin_pred_BIT "bin_pred (w BIT b) = cond(b, NCons(w,0), bin_pred(w) BIT 1)" 

5528  61 

6046  62 
primrec (*unary negation*) 
63 
bin_minus_Pls 

64 
"bin_minus (Pls) = Pls" 

65 
bin_minus_Min 

6153  66 
"bin_minus (Min) = Pls BIT 1" 
67 
bin_minus_BIT 

68 
"bin_minus (w BIT b) = cond(b, bin_pred(NCons(bin_minus(w),0)), 

69 
bin_minus(w) BIT 0)" 

6046  70 

71 
primrec (*sum*) 

9207  72 
bin_adder_Pls 
73 
"bin_adder (Pls) = (lam w:bin. w)" 

74 
bin_adder_Min 

75 
"bin_adder (Min) = (lam w:bin. bin_pred(w))" 

76 
bin_adder_BIT 

77 
"bin_adder (v BIT x) = 

78 
(lam w:bin. 

79 
bin_case (v BIT x, bin_pred(v BIT x), 

80 
%w y. NCons(bin_adder (v) ` cond(x and y, bin_succ(w), w), 

81 
x xor y), 

82 
w))" 

5528  83 

9207  84 
(*The bin_case above replaces the following mutually recursive function: 
85 
primrec 

6153  86 
"adding (v,x,Pls) = v BIT x" 
87 
"adding (v,x,Min) = bin_pred(v BIT x)" 

9207  88 
"adding (v,x,w BIT y) = NCons(bin_adder (v, cond(x and y, bin_succ(w), w)), 
6153  89 
x xor y)" 
9207  90 
*) 
91 

92 
defs 

93 
bin_add_def "bin_add(v,w) == bin_adder(v)`w" 

94 

5528  95 

6046  96 
primrec 
97 
bin_mult_Pls 

6153  98 
"bin_mult (Pls,w) = Pls" 
6046  99 
bin_mult_Min 
6153  100 
"bin_mult (Min,w) = bin_minus(w)" 
101 
bin_mult_BIT 

102 
"bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w), 

103 
NCons(bin_mult(v,w),0))" 

6046  104 

9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset

105 
setup NumeralSyntax.setup 
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset

106 

5528  107 
end 