author | paulson |
Fri, 18 Sep 1998 16:05:08 +0200 | |
changeset 5510 | ad120f7c52ad |
parent 5491 | 22f8331cdf47 |
child 5512 | 4327eec06849 |
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 |
||
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
9 |
The sign PlusSign stands for an infinite string of leading F's. |
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
10 |
The sign MinusSign stands for an infinite string of leading T's. |
1632 | 11 |
|
12 |
A number can have multiple representations, namely leading F's with sign |
|
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
13 |
PlusSign and leading T's with sign MinusSign. See twos-compl.ML/int_of_binary |
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 |
|
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
31 |
bin = PlusSign |
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
32 |
| MinusSign |
1632 | 33 |
| Bcons bin bool |
34 |
||
35 |
consts |
|
5491 | 36 |
integ_of :: bin=>int |
1632 | 37 |
norm_Bcons :: [bin,bool]=>bin |
38 |
bin_succ :: bin=>bin |
|
39 |
bin_pred :: bin=>bin |
|
40 |
bin_minus :: bin=>bin |
|
41 |
bin_add,bin_mult :: [bin,bin]=>bin |
|
42 |
h_bin :: [bin,bool,bin]=>bin |
|
43 |
||
44 |
(*norm_Bcons adds a bit, suppressing leading 0s and 1s*) |
|
45 |
||
5184 | 46 |
primrec |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
47 |
norm_Plus "norm_Bcons PlusSign b = (if b then (Bcons PlusSign b) else PlusSign)" |
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
48 |
norm_Minus "norm_Bcons MinusSign b = (if b then MinusSign else (Bcons MinusSign b))" |
1632 | 49 |
norm_Bcons "norm_Bcons (Bcons w' x') b = Bcons (Bcons w' x') b" |
50 |
||
5184 | 51 |
primrec |
5491 | 52 |
integ_of_Plus "integ_of PlusSign = $# 0" |
53 |
integ_of_Minus "integ_of MinusSign = - ($# 1)" |
|
54 |
integ_of_Bcons "integ_of(Bcons w x) = (if x then $# 1 else $# 0) + |
|
55 |
(integ_of w) + (integ_of w)" |
|
1632 | 56 |
|
5184 | 57 |
primrec |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
58 |
succ_Plus "bin_succ PlusSign = Bcons PlusSign True" |
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
59 |
succ_Minus "bin_succ MinusSign = PlusSign" |
1632 | 60 |
succ_Bcons "bin_succ(Bcons w x) = (if x then (Bcons (bin_succ w) False) else (norm_Bcons w True))" |
61 |
||
5184 | 62 |
primrec |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
63 |
pred_Plus "bin_pred(PlusSign) = MinusSign" |
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
64 |
pred_Minus "bin_pred(MinusSign) = Bcons MinusSign False" |
1632 | 65 |
pred_Bcons "bin_pred(Bcons w x) = (if x then (norm_Bcons w False) else (Bcons (bin_pred w) True))" |
66 |
||
5184 | 67 |
primrec |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
68 |
min_Plus "bin_minus PlusSign = PlusSign" |
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
69 |
min_Minus "bin_minus MinusSign = Bcons PlusSign True" |
1632 | 70 |
min_Bcons "bin_minus(Bcons w x) = (if x then (bin_pred (Bcons (bin_minus w) False)) else (Bcons (bin_minus w) False))" |
71 |
||
5184 | 72 |
primrec |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
73 |
add_Plus "bin_add PlusSign w = w" |
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
74 |
add_Minus "bin_add MinusSign w = bin_pred w" |
1632 | 75 |
add_Bcons "bin_add (Bcons v x) w = h_bin v x w" |
76 |
||
5184 | 77 |
primrec |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
78 |
mult_Plus "bin_mult PlusSign w = PlusSign" |
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
79 |
mult_Minus "bin_mult MinusSign w = bin_minus w" |
1632 | 80 |
mult_Bcons "bin_mult (Bcons v x) w = (if x then (bin_add (norm_Bcons (bin_mult v w) False) w) else (norm_Bcons (bin_mult v w) False))" |
81 |
||
5184 | 82 |
primrec |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
83 |
h_Plus "h_bin v x PlusSign = Bcons v x" |
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
84 |
h_Minus "h_bin v x MinusSign = bin_pred (Bcons v x)" |
5491 | 85 |
h_BCons "h_bin v x (Bcons w y) = norm_Bcons |
86 |
(bin_add v (if (x & y) then bin_succ w else w)) (x~=y)" |
|
87 |
||
1632 | 88 |
|
89 |
end |
|
90 |
||
91 |
ML |
|
92 |
||
93 |
(** Concrete syntax for integers **) |
|
94 |
||
95 |
local |
|
96 |
open Syntax; |
|
97 |
||
98 |
(* Bits *) |
|
99 |
||
100 |
fun mk_bit 0 = const "False" |
|
101 |
| mk_bit 1 = const "True" |
|
102 |
| mk_bit _ = sys_error "mk_bit"; |
|
103 |
||
104 |
fun dest_bit (Const ("False", _)) = 0 |
|
105 |
| dest_bit (Const ("True", _)) = 1 |
|
106 |
| dest_bit _ = raise Match; |
|
107 |
||
108 |
||
109 |
(* Bit strings *) (*we try to handle superfluous leading digits nicely*) |
|
110 |
||
111 |
fun prefix_len _ [] = 0 |
|
112 |
| prefix_len pred (x :: xs) = |
|
113 |
if pred x then 1 + prefix_len pred xs else 0; |
|
114 |
||
115 |
fun mk_bin str = |
|
116 |
let |
|
117 |
val (sign, digs) = |
|
4709 | 118 |
(case Symbol.explode str of |
1632 | 119 |
"#" :: "~" :: cs => (~1, cs) |
120 |
| "#" :: cs => (1, cs) |
|
121 |
| _ => raise ERROR); |
|
122 |
||
123 |
val zs = prefix_len (equal "0") digs; |
|
124 |
||
125 |
fun bin_of 0 = replicate zs 0 |
|
126 |
| bin_of ~1 = replicate zs 1 @ [~1] |
|
127 |
| bin_of n = (n mod 2) :: bin_of (n div 2); |
|
128 |
||
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
129 |
fun term_of [] = const "PlusSign" |
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
130 |
| term_of [~1] = const "MinusSign" |
1632 | 131 |
| term_of (b :: bs) = const "Bcons" $ term_of bs $ mk_bit b; |
132 |
in |
|
4709 | 133 |
term_of (bin_of (sign * (#1 (read_int digs)))) |
1632 | 134 |
end; |
135 |
||
136 |
fun dest_bin tm = |
|
137 |
let |
|
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
138 |
fun bin_of (Const ("PlusSign", _)) = [] |
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
139 |
| bin_of (Const ("MinusSign", _)) = [~1] |
1632 | 140 |
| bin_of (Const ("Bcons", _) $ bs $ b) = dest_bit b :: bin_of bs |
141 |
| bin_of _ = raise Match; |
|
142 |
||
143 |
fun int_of [] = 0 |
|
144 |
| int_of (b :: bs) = b + 2 * int_of bs; |
|
145 |
||
146 |
val rev_digs = bin_of tm; |
|
147 |
val (sign, zs) = |
|
148 |
(case rev rev_digs of |
|
149 |
~1 :: bs => ("~", prefix_len (equal 1) bs) |
|
150 |
| bs => ("", prefix_len (equal 0) bs)); |
|
151 |
val num = string_of_int (abs (int_of rev_digs)); |
|
152 |
in |
|
153 |
"#" ^ sign ^ implode (replicate zs "0") ^ num |
|
154 |
end; |
|
155 |
||
156 |
||
157 |
(* translation of integer constant tokens to and from binary *) |
|
158 |
||
159 |
fun int_tr (*"_Int"*) [t as Free (str, _)] = |
|
5491 | 160 |
(const "integ_of" $ |
3795 | 161 |
(mk_bin str handle ERROR => raise TERM ("int_tr", [t]))) |
162 |
| int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts); |
|
1632 | 163 |
|
164 |
fun int_tr' (*"integ_of"*) [t] = const "_Int" $ free (dest_bin t) |
|
165 |
| int_tr' (*"integ_of"*) _ = raise Match; |
|
166 |
in |
|
167 |
val parse_translation = [("_Int", int_tr)]; |
|
5491 | 168 |
val print_translation = [("integ_of", int_tr')]; |
1632 | 169 |
end; |