author | wenzelm |
Sat, 25 May 2013 15:37:53 +0200 | |
changeset 52143 | 36ffe23b25f8 |
parent 51717 | 9e7d1c139569 |
permissions | -rw-r--r-- |
22141 | 1 |
(* Title: HOL/ex/Binary.thy |
2 |
Author: Makarius |
|
3 |
*) |
|
4 |
||
5 |
header {* Simple and efficient binary numerals *} |
|
6 |
||
7 |
theory Binary |
|
8 |
imports Main |
|
9 |
begin |
|
10 |
||
11 |
subsection {* Binary representation of natural numbers *} |
|
12 |
||
13 |
definition |
|
14 |
bit :: "nat \<Rightarrow> bool \<Rightarrow> nat" where |
|
15 |
"bit n b = (if b then 2 * n + 1 else 2 * n)" |
|
16 |
||
17 |
lemma bit_simps: |
|
18 |
"bit n False = 2 * n" |
|
19 |
"bit n True = 2 * n + 1" |
|
20 |
unfolding bit_def by simp_all |
|
21 |
||
22205 | 22 |
ML {* |
26187 | 23 |
fun dest_bit (Const (@{const_name False}, _)) = 0 |
24 |
| dest_bit (Const (@{const_name True}, _)) = 1 |
|
22205 | 25 |
| dest_bit t = raise TERM ("dest_bit", [t]); |
26 |
||
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35113
diff
changeset
|
27 |
fun dest_binary (Const (@{const_name Groups.zero}, Type (@{type_name nat}, _))) = 0 |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35113
diff
changeset
|
28 |
| dest_binary (Const (@{const_name Groups.one}, Type (@{type_name nat}, _))) = 1 |
26187 | 29 |
| dest_binary (Const (@{const_name bit}, _) $ bs $ b) = 2 * dest_binary bs + dest_bit b |
22205 | 30 |
| dest_binary t = raise TERM ("dest_binary", [t]); |
31 |
||
32 |
fun mk_bit 0 = @{term False} |
|
33 |
| mk_bit 1 = @{term True} |
|
34 |
| mk_bit _ = raise TERM ("mk_bit", []); |
|
35 |
||
36 |
fun mk_binary 0 = @{term "0::nat"} |
|
37 |
| mk_binary 1 = @{term "1::nat"} |
|
38 |
| mk_binary n = |
|
39 |
if n < 0 then raise TERM ("mk_binary", []) |
|
40 |
else |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24227
diff
changeset
|
41 |
let val (q, r) = Integer.div_mod n 2 |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24227
diff
changeset
|
42 |
in @{term bit} $ mk_binary q $ mk_bit r end; |
22205 | 43 |
*} |
44 |
||
22141 | 45 |
|
46 |
subsection {* Direct operations -- plain normalization *} |
|
47 |
||
48 |
lemma binary_norm: |
|
49 |
"bit 0 False = 0" |
|
50 |
"bit 0 True = 1" |
|
51 |
unfolding bit_def by simp_all |
|
52 |
||
53 |
lemma binary_add: |
|
54 |
"n + 0 = n" |
|
55 |
"0 + n = n" |
|
56 |
"1 + 1 = bit 1 False" |
|
57 |
"bit n False + 1 = bit n True" |
|
58 |
"bit n True + 1 = bit (n + 1) False" |
|
59 |
"1 + bit n False = bit n True" |
|
60 |
"1 + bit n True = bit (n + 1) False" |
|
61 |
"bit m False + bit n False = bit (m + n) False" |
|
62 |
"bit m False + bit n True = bit (m + n) True" |
|
63 |
"bit m True + bit n False = bit (m + n) True" |
|
64 |
"bit m True + bit n True = bit ((m + n) + 1) False" |
|
65 |
by (simp_all add: bit_simps) |
|
66 |
||
67 |
lemma binary_mult: |
|
68 |
"n * 0 = 0" |
|
69 |
"0 * n = 0" |
|
70 |
"n * 1 = n" |
|
71 |
"1 * n = n" |
|
72 |
"bit m True * n = bit (m * n) False + n" |
|
73 |
"bit m False * n = bit (m * n) False" |
|
74 |
"n * bit m True = bit (m * n) False + n" |
|
75 |
"n * bit m False = bit (m * n) False" |
|
76 |
by (simp_all add: bit_simps) |
|
77 |
||
78 |
lemmas binary_simps = binary_norm binary_add binary_mult |
|
79 |
||
80 |
||
81 |
subsection {* Indirect operations -- ML will produce witnesses *} |
|
82 |
||
83 |
lemma binary_less_eq: |
|
84 |
fixes n :: nat |
|
85 |
shows "n \<equiv> m + k \<Longrightarrow> (m \<le> n) \<equiv> True" |
|
86 |
and "m \<equiv> n + k + 1 \<Longrightarrow> (m \<le> n) \<equiv> False" |
|
87 |
by simp_all |
|
52143 | 88 |
|
22141 | 89 |
lemma binary_less: |
90 |
fixes n :: nat |
|
91 |
shows "m \<equiv> n + k \<Longrightarrow> (m < n) \<equiv> False" |
|
92 |
and "n \<equiv> m + k + 1 \<Longrightarrow> (m < n) \<equiv> True" |
|
93 |
by simp_all |
|
94 |
||
95 |
lemma binary_diff: |
|
96 |
fixes n :: nat |
|
97 |
shows "m \<equiv> n + k \<Longrightarrow> m - n \<equiv> k" |
|
98 |
and "n \<equiv> m + k \<Longrightarrow> m - n \<equiv> 0" |
|
99 |
by simp_all |
|
100 |
||
101 |
lemma binary_divmod: |
|
102 |
fixes n :: nat |
|
103 |
assumes "m \<equiv> n * k + l" and "0 < n" and "l < n" |
|
104 |
shows "m div n \<equiv> k" |
|
105 |
and "m mod n \<equiv> l" |
|
106 |
proof - |
|
107 |
from `m \<equiv> n * k + l` have "m = l + k * n" by simp |
|
108 |
with `0 < n` and `l < n` show "m div n \<equiv> k" and "m mod n \<equiv> l" by simp_all |
|
109 |
qed |
|
110 |
||
111 |
ML {* |
|
22205 | 112 |
local |
113 |
infix ==; |
|
114 |
val op == = Logic.mk_equals; |
|
115 |
fun plus m n = @{term "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"} $ m $ n; |
|
116 |
fun mult m n = @{term "times :: nat \<Rightarrow> nat \<Rightarrow> nat"} $ m $ n; |
|
22141 | 117 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46236
diff
changeset
|
118 |
val binary_ss = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46236
diff
changeset
|
119 |
simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms binary_simps}); |
22156 | 120 |
fun prove ctxt prop = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46236
diff
changeset
|
121 |
Goal.prove ctxt [] [] prop |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46236
diff
changeset
|
122 |
(fn _ => ALLGOALS (full_simp_tac (put_simpset binary_ss ctxt))); |
22141 | 123 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46236
diff
changeset
|
124 |
fun binary_proc proc ctxt ct = |
22205 | 125 |
(case Thm.term_of ct of |
126 |
_ $ t $ u => |
|
35113 | 127 |
(case try (pairself (`dest_binary)) (t, u) of |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46236
diff
changeset
|
128 |
SOME args => proc ctxt args |
22205 | 129 |
| NONE => NONE) |
130 |
| _ => NONE); |
|
131 |
in |
|
22141 | 132 |
|
22205 | 133 |
val less_eq_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) => |
134 |
let val k = n - m in |
|
135 |
if k >= 0 then |
|
35113 | 136 |
SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (mk_binary k))]) |
22205 | 137 |
else |
138 |
SOME (@{thm binary_less_eq(2)} OF |
|
35113 | 139 |
[prove ctxt (t == plus (plus u (mk_binary (~ k - 1))) (mk_binary 1))]) |
22205 | 140 |
end); |
22141 | 141 |
|
22205 | 142 |
val less_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) => |
143 |
let val k = m - n in |
|
144 |
if k >= 0 then |
|
35113 | 145 |
SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (mk_binary k))]) |
22205 | 146 |
else |
147 |
SOME (@{thm binary_less(2)} OF |
|
35113 | 148 |
[prove ctxt (u == plus (plus t (mk_binary (~ k - 1))) (mk_binary 1))]) |
22205 | 149 |
end); |
22141 | 150 |
|
22205 | 151 |
val diff_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) => |
152 |
let val k = m - n in |
|
153 |
if k >= 0 then |
|
35113 | 154 |
SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (mk_binary k))]) |
22205 | 155 |
else |
35113 | 156 |
SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (mk_binary (~ k)))]) |
22205 | 157 |
end); |
22141 | 158 |
|
22205 | 159 |
fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) => |
160 |
if n = 0 then NONE |
|
161 |
else |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24227
diff
changeset
|
162 |
let val (k, l) = Integer.div_mod m n |
35113 | 163 |
in SOME (rule OF [prove ctxt (t == plus (mult u (mk_binary k)) (mk_binary l))]) end); |
22205 | 164 |
|
165 |
end; |
|
166 |
*} |
|
22141 | 167 |
|
22205 | 168 |
simproc_setup binary_nat_less_eq ("m <= (n::nat)") = {* K less_eq_proc *} |
169 |
simproc_setup binary_nat_less ("m < (n::nat)") = {* K less_proc *} |
|
170 |
simproc_setup binary_nat_diff ("m - (n::nat)") = {* K diff_proc *} |
|
171 |
simproc_setup binary_nat_div ("m div (n::nat)") = {* K (divmod_proc @{thm binary_divmod(1)}) *} |
|
172 |
simproc_setup binary_nat_mod ("m mod (n::nat)") = {* K (divmod_proc @{thm binary_divmod(2)}) *} |
|
22141 | 173 |
|
22205 | 174 |
method_setup binary_simp = {* |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46236
diff
changeset
|
175 |
Scan.succeed (fn ctxt => SIMPLE_METHOD' |
22205 | 176 |
(full_simp_tac |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46236
diff
changeset
|
177 |
(put_simpset HOL_basic_ss ctxt |
22205 | 178 |
addsimps @{thms binary_simps} |
179 |
addsimprocs |
|
180 |
[@{simproc binary_nat_less_eq}, |
|
181 |
@{simproc binary_nat_less}, |
|
182 |
@{simproc binary_nat_diff}, |
|
183 |
@{simproc binary_nat_div}, |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46236
diff
changeset
|
184 |
@{simproc binary_nat_mod}]))) |
42814 | 185 |
*} |
22141 | 186 |
|
187 |
||
188 |
subsection {* Concrete syntax *} |
|
189 |
||
190 |
syntax |
|
191 |
"_Binary" :: "num_const \<Rightarrow> 'a" ("$_") |
|
192 |
||
193 |
parse_translation {* |
|
52143 | 194 |
let |
195 |
val syntax_consts = |
|
196 |
map_aterms (fn Const (c, T) => Const (Lexicon.mark_const c, T) | a => a); |
|
22141 | 197 |
|
52143 | 198 |
fun binary_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ binary_tr [t] $ u |
199 |
| binary_tr [Const (num, _)] = |
|
200 |
let |
|
201 |
val {leading_zeros = z, value = n, ...} = Lexicon.read_xnum num; |
|
202 |
val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num); |
|
203 |
in syntax_consts (mk_binary n) end |
|
204 |
| binary_tr ts = raise TERM ("binary_tr", ts); |
|
22141 | 205 |
|
52143 | 206 |
in [(@{syntax_const "_Binary"}, K binary_tr)] end |
22141 | 207 |
*} |
208 |
||
209 |
||
210 |
subsection {* Examples *} |
|
211 |
||
212 |
lemma "$6 = 6" |
|
213 |
by (simp add: bit_simps) |
|
214 |
||
215 |
lemma "bit (bit (bit 0 False) False) True = 1" |
|
216 |
by (simp add: bit_simps) |
|
217 |
||
218 |
lemma "bit (bit (bit 0 False) False) True = bit 0 True" |
|
219 |
by (simp add: bit_simps) |
|
220 |
||
221 |
lemma "$5 + $3 = $8" |
|
222 |
by binary_simp |
|
223 |
||
224 |
lemma "$5 * $3 = $15" |
|
225 |
by binary_simp |
|
226 |
||
227 |
lemma "$5 - $3 = $2" |
|
228 |
by binary_simp |
|
229 |
||
230 |
lemma "$3 - $5 = 0" |
|
231 |
by binary_simp |
|
232 |
||
233 |
lemma "$123456789 - $123 = $123456666" |
|
234 |
by binary_simp |
|
235 |
||
236 |
lemma "$1111111111222222222233333333334444444444 - $998877665544332211 = |
|
237 |
$1111111111222222222232334455668900112233" |
|
238 |
by binary_simp |
|
239 |
||
240 |
lemma "(1111111111222222222233333333334444444444::nat) - 998877665544332211 = |
|
241 |
1111111111222222222232334455668900112233" |
|
242 |
by simp |
|
243 |
||
244 |
lemma "(1111111111222222222233333333334444444444::int) - 998877665544332211 = |
|
245 |
1111111111222222222232334455668900112233" |
|
246 |
by simp |
|
247 |
||
248 |
lemma "$1111111111222222222233333333334444444444 * $998877665544332211 = |
|
249 |
$1109864072938022197293802219729380221972383090160869185684" |
|
250 |
by binary_simp |
|
251 |
||
252 |
lemma "$1111111111222222222233333333334444444444 * $998877665544332211 - |
|
253 |
$5555555555666666666677777777778888888888 = |
|
254 |
$1109864072938022191738246664062713555294605312381980296796" |
|
255 |
by binary_simp |
|
256 |
||
257 |
lemma "$42 < $4 = False" |
|
258 |
by binary_simp |
|
259 |
||
260 |
lemma "$4 < $42 = True" |
|
261 |
by binary_simp |
|
262 |
||
263 |
lemma "$42 <= $4 = False" |
|
264 |
by binary_simp |
|
265 |
||
266 |
lemma "$4 <= $42 = True" |
|
267 |
by binary_simp |
|
268 |
||
269 |
lemma "$1111111111222222222233333333334444444444 < $998877665544332211 = False" |
|
270 |
by binary_simp |
|
271 |
||
272 |
lemma "$998877665544332211 < $1111111111222222222233333333334444444444 = True" |
|
273 |
by binary_simp |
|
274 |
||
275 |
lemma "$1111111111222222222233333333334444444444 <= $998877665544332211 = False" |
|
276 |
by binary_simp |
|
277 |
||
278 |
lemma "$998877665544332211 <= $1111111111222222222233333333334444444444 = True" |
|
279 |
by binary_simp |
|
280 |
||
281 |
lemma "$1234 div $23 = $53" |
|
282 |
by binary_simp |
|
283 |
||
284 |
lemma "$1234 mod $23 = $15" |
|
285 |
by binary_simp |
|
286 |
||
287 |
lemma "$1111111111222222222233333333334444444444 div $998877665544332211 = |
|
288 |
$1112359550673033707875" |
|
289 |
by binary_simp |
|
290 |
||
291 |
lemma "$1111111111222222222233333333334444444444 mod $998877665544332211 = |
|
292 |
$42245174317582819" |
|
293 |
by binary_simp |
|
294 |
||
22153 | 295 |
lemma "(1111111111222222222233333333334444444444::int) div 998877665544332211 = |
296 |
1112359550673033707875" |
|
297 |
by simp -- {* legacy numerals: 30 times slower *} |
|
298 |
||
22141 | 299 |
lemma "(1111111111222222222233333333334444444444::int) mod 998877665544332211 = |
300 |
42245174317582819" |
|
22153 | 301 |
by simp -- {* legacy numerals: 30 times slower *} |
22141 | 302 |
|
303 |
end |