author | paulson |
Thu, 15 Jul 1999 10:34:37 +0200 | |
changeset 7010 | 63120b6dca50 |
parent 6988 | eed63543a3af |
child 9207 | 0c294bd701ea |
permissions | -rw-r--r-- |
1632 | 1 |
(* Title: HOL/Integ/Bin.thy |
6910 | 2 |
ID: $Id$ |
1632 | 3 |
Authors: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 |
David Spelt, University of Twente |
|
5 |
Copyright 1994 University of Cambridge |
|
6 |
Copyright 1996 University of Twente |
|
7 |
||
8 |
Arithmetic on binary integers. |
|
9 |
||
5512 | 10 |
The sign Pls stands for an infinite string of leading F's. |
11 |
The sign Min stands for an infinite string of leading T's. |
|
1632 | 12 |
|
13 |
A number can have multiple representations, namely leading F's with sign |
|
5512 | 14 |
Pls and leading T's with sign Min. See ZF/ex/twos-compl.ML/int_of_binary |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
15 |
for the numerical interpretation. |
1632 | 16 |
|
17 |
The representation expects that (m mod 2) is 0 or 1, even if m is negative; |
|
18 |
For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1 |
|
19 |
||
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
20 |
Division is not defined yet! To do it efficiently requires computing the |
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
21 |
quotient and remainder using ML and checking the answer using multiplication |
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
22 |
by proof. Then uniqueness of the quotient and remainder yields theorems |
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
23 |
quoting the previously computed values. (Or code an oracle...) |
1632 | 24 |
*) |
25 |
||
6910 | 26 |
Bin = Int + Numeral + |
1632 | 27 |
|
28 |
consts |
|
5512 | 29 |
NCons :: [bin,bool]=>bin |
1632 | 30 |
bin_succ :: bin=>bin |
31 |
bin_pred :: bin=>bin |
|
32 |
bin_minus :: bin=>bin |
|
33 |
bin_add,bin_mult :: [bin,bin]=>bin |
|
6910 | 34 |
adding :: [bin,bool,bin]=>bin |
1632 | 35 |
|
5512 | 36 |
(*NCons inserts a bit, suppressing leading 0s and 1s*) |
5184 | 37 |
primrec |
5540 | 38 |
NCons_Pls "NCons Pls b = (if b then (Pls BIT b) else Pls)" |
39 |
NCons_Min "NCons Min b = (if b then Min else (Min BIT b))" |
|
40 |
NCons_BIT "NCons (w BIT x) b = (w BIT x) BIT b" |
|
6910 | 41 |
|
42 |
instance |
|
6988 | 43 |
int :: number |
44 |
||
5184 | 45 |
primrec |
6910 | 46 |
number_of_Pls "number_of Pls = int 0" |
47 |
number_of_Min "number_of Min = - (int 1)" |
|
48 |
number_of_BIT "number_of(w BIT x) = (if x then int 1 else int 0) + |
|
49 |
(number_of w) + (number_of w)" |
|
1632 | 50 |
|
5184 | 51 |
primrec |
5546 | 52 |
bin_succ_Pls "bin_succ Pls = Pls BIT True" |
53 |
bin_succ_Min "bin_succ Min = Pls" |
|
54 |
bin_succ_BIT "bin_succ(w BIT x) = |
|
55 |
(if x then bin_succ w BIT False |
|
56 |
else NCons w True)" |
|
1632 | 57 |
|
5184 | 58 |
primrec |
5546 | 59 |
bin_pred_Pls "bin_pred Pls = Min" |
60 |
bin_pred_Min "bin_pred Min = Min BIT False" |
|
61 |
bin_pred_BIT "bin_pred(w BIT x) = |
|
62 |
(if x then NCons w False |
|
63 |
else (bin_pred w) BIT True)" |
|
1632 | 64 |
|
5184 | 65 |
primrec |
5546 | 66 |
bin_minus_Pls "bin_minus Pls = Pls" |
67 |
bin_minus_Min "bin_minus Min = Pls BIT True" |
|
68 |
bin_minus_BIT "bin_minus(w BIT x) = |
|
69 |
(if x then bin_pred (NCons (bin_minus w) False) |
|
70 |
else bin_minus w BIT False)" |
|
1632 | 71 |
|
5184 | 72 |
primrec |
5546 | 73 |
bin_add_Pls "bin_add Pls w = w" |
74 |
bin_add_Min "bin_add Min w = bin_pred w" |
|
75 |
bin_add_BIT "bin_add (v BIT x) w = adding v x w" |
|
1632 | 76 |
|
5184 | 77 |
primrec |
5546 | 78 |
"adding v x Pls = v BIT x" |
79 |
"adding v x Min = bin_pred (v BIT x)" |
|
80 |
"adding v x (w BIT y) = |
|
81 |
NCons (bin_add v (if (x & y) then bin_succ w else w)) |
|
5512 | 82 |
(x~=y)" |
1632 | 83 |
|
5184 | 84 |
primrec |
5546 | 85 |
bin_mult_Pls "bin_mult Pls w = Pls" |
86 |
bin_mult_Min "bin_mult Min w = bin_minus w" |
|
87 |
bin_mult_BIT "bin_mult (v BIT x) w = |
|
88 |
(if x then (bin_add (NCons (bin_mult v w) False) w) |
|
89 |
else (NCons (bin_mult v w) False))" |
|
5491 | 90 |
|
1632 | 91 |
|
92 |
end |