author | paulson |
Mon, 22 Oct 2001 11:54:22 +0200 | |
changeset 11868 | 56db9f3a6b3e |
parent 11704 | 3c50a2cd6f00 |
child 12613 | 279facb4253a |
permissions | -rw-r--r-- |
5545 | 1 |
(* Title: HOL/ex/BinEx.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
*) |
|
6 |
||
11024 | 7 |
header {* Binary arithmetic examples *} |
8 |
||
9 |
theory BinEx = Main: |
|
10 |
||
11 |
subsection {* The Integers *} |
|
12 |
||
13 |
text {* Addition *} |
|
14 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
15 |
lemma "(13::int) + 19 = 32" |
11024 | 16 |
by simp |
17 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
18 |
lemma "(1234::int) + 5678 = 6912" |
11024 | 19 |
by simp |
20 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
21 |
lemma "(1359::int) + -2468 = -1109" |
11024 | 22 |
by simp |
23 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
24 |
lemma "(93746::int) + -46375 = 47371" |
11024 | 25 |
by simp |
26 |
||
27 |
||
28 |
text {* \medskip Negation *} |
|
29 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
30 |
lemma "- (65745::int) = -65745" |
11024 | 31 |
by simp |
32 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
33 |
lemma "- (-54321::int) = 54321" |
11024 | 34 |
by simp |
35 |
||
36 |
||
37 |
text {* \medskip Multiplication *} |
|
38 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
39 |
lemma "(13::int) * 19 = 247" |
11024 | 40 |
by simp |
41 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
42 |
lemma "(-84::int) * 51 = -4284" |
11024 | 43 |
by simp |
44 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
45 |
lemma "(255::int) * 255 = 65025" |
11024 | 46 |
by simp |
47 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
48 |
lemma "(1359::int) * -2468 = -3354012" |
11024 | 49 |
by simp |
50 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
51 |
lemma "(89::int) * 10 \<noteq> 889" |
11024 | 52 |
by simp |
53 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
54 |
lemma "(13::int) < 18 - 4" |
11024 | 55 |
by simp |
56 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
57 |
lemma "(-345::int) < -242 + -100" |
11024 | 58 |
by simp |
59 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
60 |
lemma "(13557456::int) < 18678654" |
11024 | 61 |
by simp |
62 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
63 |
lemma "(999999::int) \<le> (1000001 + 1) - 2" |
11024 | 64 |
by simp |
65 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
66 |
lemma "(1234567::int) \<le> 1234567" |
11024 | 67 |
by simp |
68 |
||
69 |
||
70 |
text {* \medskip Quotient and Remainder *} |
|
71 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
72 |
lemma "(10::int) div 3 = 3" |
11024 | 73 |
by simp |
74 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
75 |
lemma "(10::int) mod 3 = 1" |
11024 | 76 |
by simp |
77 |
||
78 |
text {* A negative divisor *} |
|
79 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
80 |
lemma "(10::int) div -3 = -4" |
11024 | 81 |
by simp |
82 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
83 |
lemma "(10::int) mod -3 = -2" |
11024 | 84 |
by simp |
5545 | 85 |
|
11024 | 86 |
text {* |
87 |
A negative dividend\footnote{The definition agrees with mathematical |
|
88 |
convention but not with the hardware of most computers} |
|
89 |
*} |
|
90 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
91 |
lemma "(-10::int) div 3 = -4" |
11024 | 92 |
by simp |
93 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
94 |
lemma "(-10::int) mod 3 = 2" |
11024 | 95 |
by simp |
96 |
||
97 |
text {* A negative dividend \emph{and} divisor *} |
|
98 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
99 |
lemma "(-10::int) div -3 = 3" |
11024 | 100 |
by simp |
101 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
102 |
lemma "(-10::int) mod -3 = -1" |
11024 | 103 |
by simp |
104 |
||
105 |
text {* A few bigger examples *} |
|
106 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
107 |
lemma "(8452::int) mod 3 = 1" |
11024 | 108 |
by simp |
109 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
110 |
lemma "(59485::int) div 434 = 137" |
11024 | 111 |
by simp |
112 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
113 |
lemma "(1000006::int) mod 10 = 6" |
11024 | 114 |
by simp |
115 |
||
116 |
||
117 |
text {* \medskip Division by shifting *} |
|
118 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
119 |
lemma "10000000 div 2 = (5000000::int)" |
11024 | 120 |
by simp |
121 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
122 |
lemma "10000001 mod 2 = (1::int)" |
11024 | 123 |
by simp |
124 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
125 |
lemma "10000055 div 32 = (312501::int)" |
11024 | 126 |
by simp |
127 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
128 |
lemma "10000055 mod 32 = (23::int)" |
11024 | 129 |
by simp |
130 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
131 |
lemma "100094 div 144 = (695::int)" |
11024 | 132 |
by simp |
133 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
134 |
lemma "100094 mod 144 = (14::int)" |
11024 | 135 |
by simp |
136 |
||
137 |
||
138 |
subsection {* The Natural Numbers *} |
|
139 |
||
140 |
text {* Successor *} |
|
141 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
142 |
lemma "Suc 99999 = 100000" |
11024 | 143 |
by (simp add: Suc_nat_number_of) |
144 |
-- {* not a default rewrite since sometimes we want to have @{text "Suc #nnn"} *} |
|
145 |
||
146 |
||
147 |
text {* \medskip Addition *} |
|
148 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
149 |
lemma "(13::nat) + 19 = 32" |
11024 | 150 |
by simp |
151 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
152 |
lemma "(1234::nat) + 5678 = 6912" |
11024 | 153 |
by simp |
154 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
155 |
lemma "(973646::nat) + 6475 = 980121" |
11024 | 156 |
by simp |
157 |
||
158 |
||
159 |
text {* \medskip Subtraction *} |
|
160 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
161 |
lemma "(32::nat) - 14 = 18" |
11024 | 162 |
by simp |
163 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
164 |
lemma "(14::nat) - 15 = 0" |
11024 | 165 |
by simp |
5545 | 166 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
167 |
lemma "(14::nat) - 1576644 = 0" |
11024 | 168 |
by simp |
169 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
170 |
lemma "(48273776::nat) - 3873737 = 44400039" |
11024 | 171 |
by simp |
172 |
||
173 |
||
174 |
text {* \medskip Multiplication *} |
|
175 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
176 |
lemma "(12::nat) * 11 = 132" |
11024 | 177 |
by simp |
178 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
179 |
lemma "(647::nat) * 3643 = 2357021" |
11024 | 180 |
by simp |
181 |
||
182 |
||
183 |
text {* \medskip Quotient and Remainder *} |
|
184 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
185 |
lemma "(10::nat) div 3 = 3" |
11024 | 186 |
by simp |
187 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
188 |
lemma "(10::nat) mod 3 = 1" |
11024 | 189 |
by simp |
190 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
191 |
lemma "(10000::nat) div 9 = 1111" |
11024 | 192 |
by simp |
193 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
194 |
lemma "(10000::nat) mod 9 = 1" |
11024 | 195 |
by simp |
196 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
197 |
lemma "(10000::nat) div 16 = 625" |
11024 | 198 |
by simp |
199 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
200 |
lemma "(10000::nat) mod 16 = 0" |
11024 | 201 |
by simp |
202 |
||
5545 | 203 |
|
11024 | 204 |
text {* \medskip Testing the cancellation of complementary terms *} |
205 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
206 |
lemma "y + (x + -x) = (0::int) + y" |
11024 | 207 |
by simp |
208 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
209 |
lemma "y + (-x + (- y + x)) = (0::int)" |
11024 | 210 |
by simp |
211 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
212 |
lemma "-x + (y + (- y + x)) = (0::int)" |
11024 | 213 |
by simp |
214 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
215 |
lemma "x + (x + (- x + (- x + (- y + - z)))) = (0::int) - y - z" |
11024 | 216 |
by simp |
217 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
218 |
lemma "x + x - x - x - y - z = (0::int) - y - z" |
11024 | 219 |
by simp |
220 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
221 |
lemma "x + y + z - (x + z) = y - (0::int)" |
11024 | 222 |
by simp |
223 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
224 |
lemma "x + (y + (y + (y + (-x + -x)))) = (0::int) + y - x + y + y" |
11024 | 225 |
by simp |
226 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
227 |
lemma "x + (y + (y + (y + (-y + -x)))) = y + (0::int) + y" |
11024 | 228 |
by simp |
229 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
230 |
lemma "x + y - x + z - x - y - z + x < (1::int)" |
11024 | 231 |
by simp |
232 |
||
233 |
||
234 |
subsection {* Normal form of bit strings *} |
|
235 |
||
236 |
text {* |
|
237 |
Definition of normal form for proving that binary arithmetic on |
|
238 |
normalized operands yields normalized results. Normal means no |
|
239 |
leading 0s on positive numbers and no leading 1s on negatives. |
|
240 |
*} |
|
5545 | 241 |
|
11024 | 242 |
consts normal :: "bin set" |
11637 | 243 |
inductive normal |
244 |
intros |
|
245 |
Pls [simp]: "Pls: normal" |
|
246 |
Min [simp]: "Min: normal" |
|
247 |
BIT_F [simp]: "w: normal ==> w \<noteq> Pls ==> w BIT False : normal" |
|
248 |
BIT_T [simp]: "w: normal ==> w \<noteq> Min ==> w BIT True : normal" |
|
11024 | 249 |
|
250 |
text {* |
|
251 |
\medskip Binary arithmetic on normalized operands yields normalized |
|
252 |
results. |
|
253 |
*} |
|
254 |
||
255 |
lemma normal_BIT_I [simp]: "w BIT b \<in> normal ==> w BIT b BIT c \<in> normal" |
|
256 |
apply (case_tac c) |
|
257 |
apply auto |
|
258 |
done |
|
259 |
||
260 |
lemma normal_BIT_D: "w BIT b \<in> normal ==> w \<in> normal" |
|
261 |
apply (erule normal.cases) |
|
262 |
apply auto |
|
263 |
done |
|
264 |
||
265 |
lemma NCons_normal [simp]: "w \<in> normal ==> NCons w b \<in> normal" |
|
266 |
apply (induct w) |
|
267 |
apply (auto simp add: NCons_Pls NCons_Min) |
|
268 |
done |
|
269 |
||
270 |
lemma NCons_True: "NCons w True \<noteq> Pls" |
|
271 |
apply (induct w) |
|
272 |
apply auto |
|
273 |
done |
|
274 |
||
275 |
lemma NCons_False: "NCons w False \<noteq> Min" |
|
276 |
apply (induct w) |
|
277 |
apply auto |
|
278 |
done |
|
5545 | 279 |
|
11024 | 280 |
lemma bin_succ_normal [simp]: "w \<in> normal ==> bin_succ w \<in> normal" |
281 |
apply (erule normal.induct) |
|
282 |
apply (case_tac [4] w) |
|
283 |
apply (auto simp add: NCons_True bin_succ_BIT) |
|
284 |
done |
|
285 |
||
286 |
lemma bin_pred_normal [simp]: "w \<in> normal ==> bin_pred w \<in> normal" |
|
287 |
apply (erule normal.induct) |
|
288 |
apply (case_tac [3] w) |
|
289 |
apply (auto simp add: NCons_False bin_pred_BIT) |
|
290 |
done |
|
291 |
||
292 |
lemma bin_add_normal [rule_format]: |
|
293 |
"w \<in> normal --> (\<forall>z. z \<in> normal --> bin_add w z \<in> normal)" |
|
294 |
apply (induct w) |
|
295 |
apply simp |
|
296 |
apply simp |
|
297 |
apply (rule impI) |
|
298 |
apply (rule allI) |
|
299 |
apply (induct_tac z) |
|
300 |
apply (simp_all add: bin_add_BIT) |
|
301 |
apply (safe dest!: normal_BIT_D) |
|
302 |
apply simp_all |
|
303 |
done |
|
304 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
305 |
lemma normal_Pls_eq_0: "w \<in> normal ==> (w = Pls) = (number_of w = (0::int))" |
11024 | 306 |
apply (erule normal.induct) |
307 |
apply auto |
|
308 |
done |
|
309 |
||
310 |
lemma bin_minus_normal: "w \<in> normal ==> bin_minus w \<in> normal" |
|
311 |
apply (erule normal.induct) |
|
312 |
apply (simp_all add: bin_minus_BIT) |
|
313 |
apply (rule normal.intros) |
|
314 |
apply assumption |
|
315 |
apply (simp add: normal_Pls_eq_0) |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
316 |
apply (simp only: number_of_minus iszero_def zminus_equation [of _ "0"]) |
11024 | 317 |
apply (rule not_sym) |
318 |
apply simp |
|
319 |
done |
|
320 |
||
321 |
lemma bin_mult_normal [rule_format]: |
|
322 |
"w \<in> normal ==> z \<in> normal --> bin_mult w z \<in> normal" |
|
323 |
apply (erule normal.induct) |
|
324 |
apply (simp_all add: bin_minus_normal bin_mult_BIT) |
|
325 |
apply (safe dest!: normal_BIT_D) |
|
326 |
apply (simp add: bin_add_normal) |
|
327 |
done |
|
5545 | 328 |
|
329 |
end |