author | wenzelm |
Wed, 17 Mar 1999 16:53:46 +0100 | |
changeset 6394 | 3d9fd50fcc43 |
parent 5582 | a356fb49e69e |
child 6396 | fee481d8ea7a |
permissions | -rw-r--r-- |
1632 | 1 |
(* Title: HOL/Integ/Bin.thy |
2 |
Authors: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 |
David Spelt, University of Twente |
|
4 |
Copyright 1994 University of Cambridge |
|
5 |
Copyright 1996 University of Twente |
|
6 |
||
7 |
Arithmetic on binary integers. |
|
8 |
||
5512 | 9 |
The sign Pls stands for an infinite string of leading F's. |
10 |
The sign Min stands for an infinite string of leading T's. |
|
1632 | 11 |
|
12 |
A number can have multiple representations, namely leading F's with sign |
|
5512 | 13 |
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
|
14 |
for the numerical interpretation. |
1632 | 15 |
|
16 |
The representation expects that (m mod 2) is 0 or 1, even if m is negative; |
|
17 |
For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1 |
|
18 |
||
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
19 |
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
|
20 |
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
|
21 |
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
|
22 |
quoting the previously computed values. (Or code an oracle...) |
1632 | 23 |
*) |
24 |
||
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5546
diff
changeset
|
25 |
Bin = Int + Datatype + |
1632 | 26 |
|
27 |
syntax |
|
28 |
"_Int" :: xnum => int ("_") |
|
29 |
||
30 |
datatype |
|
5512 | 31 |
bin = Pls |
32 |
| Min |
|
33 |
| BIT bin bool (infixl 90) |
|
1632 | 34 |
|
35 |
consts |
|
5512 | 36 |
integ_of :: bin=>int |
37 |
NCons :: [bin,bool]=>bin |
|
1632 | 38 |
bin_succ :: bin=>bin |
39 |
bin_pred :: bin=>bin |
|
40 |
bin_minus :: bin=>bin |
|
41 |
bin_add,bin_mult :: [bin,bin]=>bin |
|
5546 | 42 |
adding :: [bin,bool,bin]=>bin |
1632 | 43 |
|
5512 | 44 |
(*NCons inserts a bit, suppressing leading 0s and 1s*) |
5184 | 45 |
primrec |
5540 | 46 |
NCons_Pls "NCons Pls b = (if b then (Pls BIT b) else Pls)" |
47 |
NCons_Min "NCons Min b = (if b then Min else (Min BIT b))" |
|
48 |
NCons_BIT "NCons (w BIT x) b = (w BIT x) BIT b" |
|
1632 | 49 |
|
5184 | 50 |
primrec |
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
51 |
integ_of_Pls "integ_of Pls = int 0" |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
52 |
integ_of_Min "integ_of Min = - (int 1)" |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
53 |
integ_of_BIT "integ_of(w BIT x) = (if x then int 1 else int 0) + |
5512 | 54 |
(integ_of w) + (integ_of w)" |
1632 | 55 |
|
5184 | 56 |
primrec |
5546 | 57 |
bin_succ_Pls "bin_succ Pls = Pls BIT True" |
58 |
bin_succ_Min "bin_succ Min = Pls" |
|
59 |
bin_succ_BIT "bin_succ(w BIT x) = |
|
60 |
(if x then bin_succ w BIT False |
|
61 |
else NCons w True)" |
|
1632 | 62 |
|
5184 | 63 |
primrec |
5546 | 64 |
bin_pred_Pls "bin_pred Pls = Min" |
65 |
bin_pred_Min "bin_pred Min = Min BIT False" |
|
66 |
bin_pred_BIT "bin_pred(w BIT x) = |
|
67 |
(if x then NCons w False |
|
68 |
else (bin_pred w) BIT True)" |
|
1632 | 69 |
|
5184 | 70 |
primrec |
5546 | 71 |
bin_minus_Pls "bin_minus Pls = Pls" |
72 |
bin_minus_Min "bin_minus Min = Pls BIT True" |
|
73 |
bin_minus_BIT "bin_minus(w BIT x) = |
|
74 |
(if x then bin_pred (NCons (bin_minus w) False) |
|
75 |
else bin_minus w BIT False)" |
|
1632 | 76 |
|
5184 | 77 |
primrec |
5546 | 78 |
bin_add_Pls "bin_add Pls w = w" |
79 |
bin_add_Min "bin_add Min w = bin_pred w" |
|
80 |
bin_add_BIT "bin_add (v BIT x) w = adding v x w" |
|
1632 | 81 |
|
5184 | 82 |
primrec |
5546 | 83 |
"adding v x Pls = v BIT x" |
84 |
"adding v x Min = bin_pred (v BIT x)" |
|
85 |
"adding v x (w BIT y) = |
|
86 |
NCons (bin_add v (if (x & y) then bin_succ w else w)) |
|
5512 | 87 |
(x~=y)" |
1632 | 88 |
|
5184 | 89 |
primrec |
5546 | 90 |
bin_mult_Pls "bin_mult Pls w = Pls" |
91 |
bin_mult_Min "bin_mult Min w = bin_minus w" |
|
92 |
bin_mult_BIT "bin_mult (v BIT x) w = |
|
93 |
(if x then (bin_add (NCons (bin_mult v w) False) w) |
|
94 |
else (NCons (bin_mult v w) False))" |
|
5491 | 95 |
|
1632 | 96 |
|
97 |
end |
|
98 |
||
99 |
ML |
|
100 |
||
101 |
(** Concrete syntax for integers **) |
|
102 |
||
103 |
local |
|
104 |
open Syntax; |
|
105 |
||
106 |
(* Bits *) |
|
107 |
||
108 |
fun mk_bit 0 = const "False" |
|
109 |
| mk_bit 1 = const "True" |
|
110 |
| mk_bit _ = sys_error "mk_bit"; |
|
111 |
||
112 |
fun dest_bit (Const ("False", _)) = 0 |
|
113 |
| dest_bit (Const ("True", _)) = 1 |
|
114 |
| dest_bit _ = raise Match; |
|
115 |
||
116 |
||
117 |
(* Bit strings *) (*we try to handle superfluous leading digits nicely*) |
|
118 |
||
119 |
fun prefix_len _ [] = 0 |
|
120 |
| prefix_len pred (x :: xs) = |
|
121 |
if pred x then 1 + prefix_len pred xs else 0; |
|
122 |
||
123 |
fun mk_bin str = |
|
124 |
let |
|
125 |
val (sign, digs) = |
|
4709 | 126 |
(case Symbol.explode str of |
5512 | 127 |
"#" :: "-" :: cs => (~1, cs) |
1632 | 128 |
| "#" :: cs => (1, cs) |
129 |
| _ => raise ERROR); |
|
130 |
||
5512 | 131 |
fun bin_of 0 = [] |
132 |
| bin_of ~1 = [~1] |
|
133 |
| bin_of n = (n mod 2) :: bin_of (n div 2); |
|
1632 | 134 |
|
5512 | 135 |
fun term_of [] = const "Bin.bin.Pls" |
136 |
| term_of [~1] = const "Bin.bin.Min" |
|
137 |
| term_of (b :: bs) = const "Bin.bin.op BIT" $ term_of bs $ mk_bit b; |
|
1632 | 138 |
in |
4709 | 139 |
term_of (bin_of (sign * (#1 (read_int digs)))) |
1632 | 140 |
end; |
141 |
||
142 |
fun dest_bin tm = |
|
143 |
let |
|
5540 | 144 |
(*We consider both "spellings", since Min might be declared elsewhere*) |
145 |
fun bin_of (Const ("Pls", _)) = [] |
|
146 |
| bin_of (Const ("bin.Pls", _)) = [] |
|
147 |
| bin_of (Const ("Min", _)) = [~1] |
|
148 |
| bin_of (Const ("bin.Min", _)) = [~1] |
|
149 |
| bin_of (Const ("op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs |
|
150 |
| bin_of (Const ("bin.op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs |
|
1632 | 151 |
| bin_of _ = raise Match; |
152 |
||
153 |
fun int_of [] = 0 |
|
154 |
| int_of (b :: bs) = b + 2 * int_of bs; |
|
155 |
||
156 |
val rev_digs = bin_of tm; |
|
157 |
val (sign, zs) = |
|
158 |
(case rev rev_digs of |
|
5512 | 159 |
~1 :: bs => ("-", prefix_len (equal 1) bs) |
1632 | 160 |
| bs => ("", prefix_len (equal 0) bs)); |
161 |
val num = string_of_int (abs (int_of rev_digs)); |
|
162 |
in |
|
163 |
"#" ^ sign ^ implode (replicate zs "0") ^ num |
|
164 |
end; |
|
165 |
||
166 |
||
167 |
(* translation of integer constant tokens to and from binary *) |
|
168 |
||
169 |
fun int_tr (*"_Int"*) [t as Free (str, _)] = |
|
5491 | 170 |
(const "integ_of" $ |
3795 | 171 |
(mk_bin str handle ERROR => raise TERM ("int_tr", [t]))) |
172 |
| int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts); |
|
1632 | 173 |
|
174 |
fun int_tr' (*"integ_of"*) [t] = const "_Int" $ free (dest_bin t) |
|
175 |
| int_tr' (*"integ_of"*) _ = raise Match; |
|
176 |
in |
|
177 |
val parse_translation = [("_Int", int_tr)]; |
|
5491 | 178 |
val print_translation = [("integ_of", int_tr')]; |
1632 | 179 |
end; |