author | paulson |
Mon, 21 Sep 1998 10:43:09 +0200 | |
changeset 5512 | 4327eec06849 |
parent 5510 | ad120f7c52ad |
child 5540 | 0f16c3b66ab4 |
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 |
||
5184 | 25 |
Bin = Integ + 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 |
|
5512 | 42 |
h_bin :: [bin,bool,bin]=>bin |
1632 | 43 |
|
5512 | 44 |
(*NCons inserts a bit, suppressing leading 0s and 1s*) |
5184 | 45 |
primrec |
5512 | 46 |
norm_Pls "NCons Pls b = (if b then (Pls BIT b) else Pls)" |
47 |
norm_Min "NCons Min b = (if b then Min else (Min BIT b))" |
|
48 |
NCons "NCons (w' BIT x') b = (w' BIT x') BIT b" |
|
1632 | 49 |
|
5184 | 50 |
primrec |
5512 | 51 |
integ_of_Pls "integ_of Pls = $# 0" |
52 |
integ_of_Min "integ_of Min = - ($# 1)" |
|
53 |
integ_of_BIT "integ_of(w BIT x) = (if x then $# 1 else $# 0) + |
|
54 |
(integ_of w) + (integ_of w)" |
|
1632 | 55 |
|
5184 | 56 |
primrec |
5512 | 57 |
succ_Pls "bin_succ Pls = Pls BIT True" |
58 |
succ_Min "bin_succ Min = Pls" |
|
59 |
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 |
5512 | 64 |
pred_Pls "bin_pred Pls = Min" |
65 |
pred_Min "bin_pred Min = Min BIT False" |
|
66 |
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 |
5512 | 71 |
minus_Pls "bin_minus Pls = Pls" |
72 |
minus_Min "bin_minus Min = Pls BIT True" |
|
73 |
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 |
5512 | 78 |
add_Pls "bin_add Pls w = w" |
79 |
add_Min "bin_add Min w = bin_pred w" |
|
80 |
add_BIT "bin_add (v BIT x) w = h_bin v x w" |
|
1632 | 81 |
|
5184 | 82 |
primrec |
5512 | 83 |
"h_bin v x Pls = v BIT x" |
84 |
"h_bin v x Min = bin_pred (v BIT x)" |
|
85 |
"h_bin v x (w BIT y) = |
|
86 |
NCons (bin_add v (if (x & y) then bin_succ w else w)) |
|
87 |
(x~=y)" |
|
1632 | 88 |
|
5184 | 89 |
primrec |
5512 | 90 |
mult_Pls "bin_mult Pls w = Pls" |
91 |
mult_Min "bin_mult Min w = bin_minus w" |
|
92 |
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 |
|
5512 | 144 |
fun bin_of (Const ("Pls", _)) = [] |
145 |
| bin_of (Const ("Min", _)) = [~1] |
|
146 |
| bin_of (Const ("op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs |
|
1632 | 147 |
| bin_of _ = raise Match; |
148 |
||
149 |
fun int_of [] = 0 |
|
150 |
| int_of (b :: bs) = b + 2 * int_of bs; |
|
151 |
||
152 |
val rev_digs = bin_of tm; |
|
153 |
val (sign, zs) = |
|
154 |
(case rev rev_digs of |
|
5512 | 155 |
~1 :: bs => ("-", prefix_len (equal 1) bs) |
1632 | 156 |
| bs => ("", prefix_len (equal 0) bs)); |
157 |
val num = string_of_int (abs (int_of rev_digs)); |
|
158 |
in |
|
159 |
"#" ^ sign ^ implode (replicate zs "0") ^ num |
|
160 |
end; |
|
161 |
||
162 |
||
163 |
(* translation of integer constant tokens to and from binary *) |
|
164 |
||
165 |
fun int_tr (*"_Int"*) [t as Free (str, _)] = |
|
5491 | 166 |
(const "integ_of" $ |
3795 | 167 |
(mk_bin str handle ERROR => raise TERM ("int_tr", [t]))) |
168 |
| int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts); |
|
1632 | 169 |
|
170 |
fun int_tr' (*"integ_of"*) [t] = const "_Int" $ free (dest_bin t) |
|
171 |
| int_tr' (*"integ_of"*) _ = raise Match; |
|
172 |
in |
|
173 |
val parse_translation = [("_Int", int_tr)]; |
|
5491 | 174 |
val print_translation = [("integ_of", int_tr')]; |
1632 | 175 |
end; |