author | haftmann |
Fri, 20 Apr 2007 11:21:42 +0200 | |
changeset 22744 | 5cbe966d67a2 |
parent 22473 | 753123c89d72 |
child 22801 | caffcb450ef4 |
permissions | -rw-r--r-- |
20485 | 1 |
(* Title: HOL/Integ/Numeral.thy |
15013 | 2 |
ID: $Id$ |
20485 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 |
Copyright 1994 University of Cambridge |
|
15013 | 5 |
*) |
6 |
||
20485 | 7 |
header {* Arithmetic on Binary Integers *} |
15013 | 8 |
|
15131 | 9 |
theory Numeral |
15620
8ccdc8bc66a2
replaced bool by a new datatype "bit" for binary numerals
paulson
parents:
15140
diff
changeset
|
10 |
imports IntDef Datatype |
16417 | 11 |
uses "../Tools/numeral_syntax.ML" |
15131 | 12 |
begin |
15013 | 13 |
|
20485 | 14 |
text {* |
15 |
This formalization defines binary arithmetic in terms of the integers |
|
16 |
rather than using a datatype. This avoids multiple representations (leading |
|
17 |
zeroes, etc.) See @{text "ZF/Integ/twos-compl.ML"}, function @{text |
|
18 |
int_of_binary}, for the numerical interpretation. |
|
15013 | 19 |
|
20485 | 20 |
The representation expects that @{text "(m mod 2)"} is 0 or 1, |
21 |
even if m is negative; |
|
22 |
For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus |
|
23 |
@{text "-5 = (-3)*2 + 1"}. |
|
15013 | 24 |
*} |
25 |
||
20485 | 26 |
text{* |
21834 | 27 |
This type avoids the use of type @{typ bool}, which would make |
20485 | 28 |
all of the rewrite rules higher-order. |
29 |
*} |
|
15013 | 30 |
|
15620
8ccdc8bc66a2
replaced bool by a new datatype "bit" for binary numerals
paulson
parents:
15140
diff
changeset
|
31 |
datatype bit = B0 | B1 |
8ccdc8bc66a2
replaced bool by a new datatype "bit" for binary numerals
paulson
parents:
15140
diff
changeset
|
32 |
|
21779 | 33 |
definition |
21820
2f2b6a965ccc
introduced mk/dest_numeral/number for mk/dest_binum etc.
haftmann
parents:
21779
diff
changeset
|
34 |
Pls :: int where |
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22473
diff
changeset
|
35 |
[code nofunc]:"Pls = 0" |
21779 | 36 |
|
37 |
definition |
|
21820
2f2b6a965ccc
introduced mk/dest_numeral/number for mk/dest_binum etc.
haftmann
parents:
21779
diff
changeset
|
38 |
Min :: int where |
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22473
diff
changeset
|
39 |
[code nofunc]:"Min = - 1" |
21779 | 40 |
|
41 |
definition |
|
42 |
Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where |
|
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22473
diff
changeset
|
43 |
[code nofunc]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k" |
15013 | 44 |
|
22473 | 45 |
class number = type + -- {* for numeric types: nat, int, real, \dots *} |
21820
2f2b6a965ccc
introduced mk/dest_numeral/number for mk/dest_binum etc.
haftmann
parents:
21779
diff
changeset
|
46 |
fixes number_of :: "int \<Rightarrow> 'a" |
15013 | 47 |
|
48 |
syntax |
|
20485 | 49 |
"_Numeral" :: "num_const \<Rightarrow> 'a" ("_") |
15013 | 50 |
|
51 |
setup NumeralSyntax.setup |
|
52 |
||
19380 | 53 |
abbreviation |
20485 | 54 |
"Numeral0 \<equiv> number_of Pls" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20900
diff
changeset
|
55 |
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20900
diff
changeset
|
56 |
abbreviation |
20485 | 57 |
"Numeral1 \<equiv> number_of (Pls BIT B1)" |
15013 | 58 |
|
20485 | 59 |
lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)" |
15013 | 60 |
-- {* Unfold all @{text let}s involving constants *} |
20485 | 61 |
unfolding Let_def .. |
62 |
||
63 |
lemma Let_0 [simp]: "Let 0 f = f 0" |
|
64 |
unfolding Let_def .. |
|
65 |
||
66 |
lemma Let_1 [simp]: "Let 1 f = f 1" |
|
67 |
unfolding Let_def .. |
|
15013 | 68 |
|
20485 | 69 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20900
diff
changeset
|
70 |
succ :: "int \<Rightarrow> int" where |
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22473
diff
changeset
|
71 |
[code nofunc]: "succ k = k + 1" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20900
diff
changeset
|
72 |
|
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20900
diff
changeset
|
73 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20900
diff
changeset
|
74 |
pred :: "int \<Rightarrow> int" where |
22744
5cbe966d67a2
Isar definitions are now added explicitly to code theorem table
haftmann
parents:
22473
diff
changeset
|
75 |
[code nofunc]: "pred k = k - 1" |
20485 | 76 |
|
22187 | 77 |
declare |
78 |
max_def[of "number_of u" "number_of v", standard, simp] |
|
79 |
min_def[of "number_of u" "number_of v", standard, simp] |
|
80 |
-- {* unfolding @{text minx} and @{text max} on numerals *} |
|
81 |
||
20485 | 82 |
lemmas numeral_simps = |
83 |
succ_def pred_def Pls_def Min_def Bit_def |
|
15013 | 84 |
|
20485 | 85 |
text {* Removal of leading zeroes *} |
86 |
||
20699 | 87 |
lemma Pls_0_eq [simp, code func]: |
20485 | 88 |
"Pls BIT B0 = Pls" |
89 |
unfolding numeral_simps by simp |
|
90 |
||
20699 | 91 |
lemma Min_1_eq [simp, code func]: |
20485 | 92 |
"Min BIT B1 = Min" |
93 |
unfolding numeral_simps by simp |
|
15013 | 94 |
|
95 |
||
20485 | 96 |
subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *} |
15013 | 97 |
|
20485 | 98 |
lemma succ_Pls [simp]: |
99 |
"succ Pls = Pls BIT B1" |
|
100 |
unfolding numeral_simps by simp |
|
15013 | 101 |
|
20485 | 102 |
lemma succ_Min [simp]: |
103 |
"succ Min = Pls" |
|
104 |
unfolding numeral_simps by simp |
|
15013 | 105 |
|
20485 | 106 |
lemma succ_1 [simp]: |
107 |
"succ (k BIT B1) = succ k BIT B0" |
|
108 |
unfolding numeral_simps by simp |
|
15013 | 109 |
|
20485 | 110 |
lemma succ_0 [simp]: |
111 |
"succ (k BIT B0) = k BIT B1" |
|
112 |
unfolding numeral_simps by simp |
|
15013 | 113 |
|
20485 | 114 |
lemma pred_Pls [simp]: |
115 |
"pred Pls = Min" |
|
116 |
unfolding numeral_simps by simp |
|
15013 | 117 |
|
20485 | 118 |
lemma pred_Min [simp]: |
119 |
"pred Min = Min BIT B0" |
|
120 |
unfolding numeral_simps by simp |
|
15013 | 121 |
|
20485 | 122 |
lemma pred_1 [simp]: |
123 |
"pred (k BIT B1) = k BIT B0" |
|
124 |
unfolding numeral_simps by simp |
|
15013 | 125 |
|
20485 | 126 |
lemma pred_0 [simp]: |
127 |
"pred (k BIT B0) = pred k BIT B1" |
|
128 |
unfolding numeral_simps by simp |
|
15013 | 129 |
|
20485 | 130 |
lemma minus_Pls [simp]: |
131 |
"- Pls = Pls" |
|
132 |
unfolding numeral_simps by simp |
|
15013 | 133 |
|
20485 | 134 |
lemma minus_Min [simp]: |
135 |
"- Min = Pls BIT B1" |
|
136 |
unfolding numeral_simps by simp |
|
15013 | 137 |
|
20485 | 138 |
lemma minus_1 [simp]: |
139 |
"- (k BIT B1) = pred (- k) BIT B1" |
|
140 |
unfolding numeral_simps by simp |
|
15013 | 141 |
|
20485 | 142 |
lemma minus_0 [simp]: |
143 |
"- (k BIT B0) = (- k) BIT B0" |
|
144 |
unfolding numeral_simps by simp |
|
15013 | 145 |
|
146 |
||
20485 | 147 |
subsection {* |
148 |
Binary Addition and Multiplication: @{term "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"} |
|
149 |
and @{term "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"} |
|
150 |
*} |
|
15013 | 151 |
|
20485 | 152 |
lemma add_Pls [simp]: |
153 |
"Pls + k = k" |
|
154 |
unfolding numeral_simps by simp |
|
15013 | 155 |
|
20485 | 156 |
lemma add_Min [simp]: |
157 |
"Min + k = pred k" |
|
158 |
unfolding numeral_simps by simp |
|
15013 | 159 |
|
20485 | 160 |
lemma add_BIT_11 [simp]: |
161 |
"(k BIT B1) + (l BIT B1) = (k + succ l) BIT B0" |
|
162 |
unfolding numeral_simps by simp |
|
15013 | 163 |
|
20485 | 164 |
lemma add_BIT_10 [simp]: |
165 |
"(k BIT B1) + (l BIT B0) = (k + l) BIT B1" |
|
166 |
unfolding numeral_simps by simp |
|
15013 | 167 |
|
20485 | 168 |
lemma add_BIT_0 [simp]: |
169 |
"(k BIT B0) + (l BIT b) = (k + l) BIT b" |
|
170 |
unfolding numeral_simps by simp |
|
15013 | 171 |
|
20485 | 172 |
lemma add_Pls_right [simp]: |
173 |
"k + Pls = k" |
|
174 |
unfolding numeral_simps by simp |
|
15013 | 175 |
|
20485 | 176 |
lemma add_Min_right [simp]: |
177 |
"k + Min = pred k" |
|
178 |
unfolding numeral_simps by simp |
|
15013 | 179 |
|
20485 | 180 |
lemma mult_Pls [simp]: |
181 |
"Pls * w = Pls" |
|
182 |
unfolding numeral_simps by simp |
|
15013 | 183 |
|
20485 | 184 |
lemma mult_Min [simp]: |
185 |
"Min * k = - k" |
|
186 |
unfolding numeral_simps by simp |
|
15013 | 187 |
|
20485 | 188 |
lemma mult_num1 [simp]: |
189 |
"(k BIT B1) * l = ((k * l) BIT B0) + l" |
|
190 |
unfolding numeral_simps int_distrib by simp |
|
15013 | 191 |
|
20485 | 192 |
lemma mult_num0 [simp]: |
193 |
"(k BIT B0) * l = (k * l) BIT B0" |
|
194 |
unfolding numeral_simps int_distrib by simp |
|
15013 | 195 |
|
196 |
||
197 |
||
20485 | 198 |
subsection {* Converting Numerals to Rings: @{term number_of} *} |
15013 | 199 |
|
200 |
axclass number_ring \<subseteq> number, comm_ring_1 |
|
20485 | 201 |
number_of_eq: "number_of k = of_int k" |
15013 | 202 |
|
203 |
lemma number_of_succ: |
|
20485 | 204 |
"number_of (succ k) = (1 + number_of k ::'a::number_ring)" |
205 |
unfolding number_of_eq numeral_simps by simp |
|
15013 | 206 |
|
207 |
lemma number_of_pred: |
|
20485 | 208 |
"number_of (pred w) = (- 1 + number_of w ::'a::number_ring)" |
209 |
unfolding number_of_eq numeral_simps by simp |
|
15013 | 210 |
|
211 |
lemma number_of_minus: |
|
20485 | 212 |
"number_of (uminus w) = (- (number_of w)::'a::number_ring)" |
213 |
unfolding number_of_eq numeral_simps by simp |
|
15013 | 214 |
|
215 |
lemma number_of_add: |
|
20485 | 216 |
"number_of (v + w) = (number_of v + number_of w::'a::number_ring)" |
217 |
unfolding number_of_eq numeral_simps by simp |
|
15013 | 218 |
|
219 |
lemma number_of_mult: |
|
20485 | 220 |
"number_of (v * w) = (number_of v * number_of w::'a::number_ring)" |
221 |
unfolding number_of_eq numeral_simps by simp |
|
15013 | 222 |
|
20485 | 223 |
text {* |
224 |
The correctness of shifting. |
|
225 |
But it doesn't seem to give a measurable speed-up. |
|
226 |
*} |
|
227 |
||
15013 | 228 |
lemma double_number_of_BIT: |
20485 | 229 |
"(1 + 1) * number_of w = (number_of (w BIT B0) ::'a::number_ring)" |
230 |
unfolding number_of_eq numeral_simps left_distrib by simp |
|
15013 | 231 |
|
20485 | 232 |
text {* |
233 |
Converting numerals 0 and 1 to their abstract versions. |
|
234 |
*} |
|
235 |
||
236 |
lemma numeral_0_eq_0 [simp]: |
|
237 |
"Numeral0 = (0::'a::number_ring)" |
|
238 |
unfolding number_of_eq numeral_simps by simp |
|
15013 | 239 |
|
20485 | 240 |
lemma numeral_1_eq_1 [simp]: |
241 |
"Numeral1 = (1::'a::number_ring)" |
|
242 |
unfolding number_of_eq numeral_simps by simp |
|
15013 | 243 |
|
20485 | 244 |
text {* |
245 |
Special-case simplification for small constants. |
|
246 |
*} |
|
15013 | 247 |
|
20485 | 248 |
text{* |
249 |
Unary minus for the abstract constant 1. Cannot be inserted |
|
250 |
as a simprule until later: it is @{text number_of_Min} re-oriented! |
|
251 |
*} |
|
15013 | 252 |
|
20485 | 253 |
lemma numeral_m1_eq_minus_1: |
254 |
"(-1::'a::number_ring) = - 1" |
|
255 |
unfolding number_of_eq numeral_simps by simp |
|
15013 | 256 |
|
20485 | 257 |
lemma mult_minus1 [simp]: |
258 |
"-1 * z = -(z::'a::number_ring)" |
|
259 |
unfolding number_of_eq numeral_simps by simp |
|
260 |
||
261 |
lemma mult_minus1_right [simp]: |
|
262 |
"z * -1 = -(z::'a::number_ring)" |
|
263 |
unfolding number_of_eq numeral_simps by simp |
|
15013 | 264 |
|
265 |
(*Negation of a coefficient*) |
|
266 |
lemma minus_number_of_mult [simp]: |
|
20485 | 267 |
"- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)" |
268 |
unfolding number_of_eq by simp |
|
269 |
||
270 |
text {* Subtraction *} |
|
271 |
||
272 |
lemma diff_number_of_eq: |
|
273 |
"number_of v - number_of w = |
|
274 |
(number_of (v + uminus w)::'a::number_ring)" |
|
275 |
unfolding number_of_eq by simp |
|
15013 | 276 |
|
20485 | 277 |
lemma number_of_Pls: |
278 |
"number_of Pls = (0::'a::number_ring)" |
|
279 |
unfolding number_of_eq numeral_simps by simp |
|
280 |
||
281 |
lemma number_of_Min: |
|
282 |
"number_of Min = (- 1::'a::number_ring)" |
|
283 |
unfolding number_of_eq numeral_simps by simp |
|
284 |
||
285 |
lemma number_of_BIT: |
|
286 |
"number_of(w BIT x) = (case x of B0 => 0 | B1 => (1::'a::number_ring)) |
|
287 |
+ (number_of w) + (number_of w)" |
|
288 |
unfolding number_of_eq numeral_simps by (simp split: bit.split) |
|
15013 | 289 |
|
290 |
||
20485 | 291 |
subsection {* Equality of Binary Numbers *} |
15013 | 292 |
|
20485 | 293 |
text {* First version by Norbert Voelker *} |
15013 | 294 |
|
295 |
lemma eq_number_of_eq: |
|
296 |
"((number_of x::'a::number_ring) = number_of y) = |
|
20485 | 297 |
iszero (number_of (x + uminus y) :: 'a)" |
298 |
unfolding iszero_def number_of_add number_of_minus |
|
299 |
by (simp add: compare_rls) |
|
15013 | 300 |
|
20485 | 301 |
lemma iszero_number_of_Pls: |
302 |
"iszero ((number_of Pls)::'a::number_ring)" |
|
303 |
unfolding iszero_def numeral_0_eq_0 .. |
|
15013 | 304 |
|
20485 | 305 |
lemma nonzero_number_of_Min: |
306 |
"~ iszero ((number_of Min)::'a::number_ring)" |
|
307 |
unfolding iszero_def numeral_m1_eq_minus_1 by simp |
|
15013 | 308 |
|
309 |
||
20485 | 310 |
subsection {* Comparisons, for Ordered Rings *} |
15013 | 311 |
|
20485 | 312 |
lemma double_eq_0_iff: |
313 |
"(a + a = 0) = (a = (0::'a::ordered_idom))" |
|
15013 | 314 |
proof - |
20485 | 315 |
have "a + a = (1 + 1) * a" unfolding left_distrib by simp |
15013 | 316 |
with zero_less_two [where 'a = 'a] |
317 |
show ?thesis by force |
|
318 |
qed |
|
319 |
||
320 |
lemma le_imp_0_less: |
|
20485 | 321 |
assumes le: "0 \<le> z" |
322 |
shows "(0::int) < 1 + z" |
|
15013 | 323 |
proof - |
324 |
have "0 \<le> z" . |
|
325 |
also have "... < z + 1" by (rule less_add_one) |
|
326 |
also have "... = 1 + z" by (simp add: add_ac) |
|
327 |
finally show "0 < 1 + z" . |
|
328 |
qed |
|
329 |
||
20485 | 330 |
lemma odd_nonzero: |
331 |
"1 + z + z \<noteq> (0::int)"; |
|
15013 | 332 |
proof (cases z rule: int_cases) |
333 |
case (nonneg n) |
|
334 |
have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) |
|
335 |
thus ?thesis using le_imp_0_less [OF le] |
|
336 |
by (auto simp add: add_assoc) |
|
337 |
next |
|
338 |
case (neg n) |
|
339 |
show ?thesis |
|
340 |
proof |
|
341 |
assume eq: "1 + z + z = 0" |
|
342 |
have "0 < 1 + (int n + int n)" |
|
343 |
by (simp add: le_imp_0_less add_increasing) |
|
344 |
also have "... = - (1 + z + z)" |
|
345 |
by (simp add: neg add_assoc [symmetric]) |
|
346 |
also have "... = 0" by (simp add: eq) |
|
347 |
finally have "0<0" .. |
|
348 |
thus False by blast |
|
349 |
qed |
|
350 |
qed |
|
351 |
||
20485 | 352 |
text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *} |
15013 | 353 |
|
20485 | 354 |
lemma Ints_odd_nonzero: |
355 |
assumes in_Ints: "a \<in> Ints" |
|
356 |
shows "1 + a + a \<noteq> (0::'a::ordered_idom)" |
|
357 |
proof - |
|
358 |
from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] . |
|
15013 | 359 |
then obtain z where a: "a = of_int z" .. |
360 |
show ?thesis |
|
361 |
proof |
|
362 |
assume eq: "1 + a + a = 0" |
|
363 |
hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a) |
|
364 |
hence "1 + z + z = 0" by (simp only: of_int_eq_iff) |
|
365 |
with odd_nonzero show False by blast |
|
366 |
qed |
|
367 |
qed |
|
368 |
||
20485 | 369 |
lemma Ints_number_of: |
370 |
"(number_of w :: 'a::number_ring) \<in> Ints" |
|
371 |
unfolding number_of_eq Ints_def by simp |
|
15013 | 372 |
|
373 |
lemma iszero_number_of_BIT: |
|
20485 | 374 |
"iszero (number_of (w BIT x)::'a) = |
375 |
(x = B0 \<and> iszero (number_of w::'a::{ordered_idom,number_ring}))" |
|
376 |
by (simp add: iszero_def number_of_eq numeral_simps double_eq_0_iff |
|
377 |
Ints_odd_nonzero Ints_def split: bit.split) |
|
15013 | 378 |
|
379 |
lemma iszero_number_of_0: |
|
20485 | 380 |
"iszero (number_of (w BIT B0) :: 'a::{ordered_idom,number_ring}) = |
381 |
iszero (number_of w :: 'a)" |
|
382 |
by (simp only: iszero_number_of_BIT simp_thms) |
|
15013 | 383 |
|
384 |
lemma iszero_number_of_1: |
|
20485 | 385 |
"~ iszero (number_of (w BIT B1)::'a::{ordered_idom,number_ring})" |
386 |
by (simp add: iszero_number_of_BIT) |
|
15013 | 387 |
|
388 |
||
20485 | 389 |
subsection {* The Less-Than Relation *} |
15013 | 390 |
|
391 |
lemma less_number_of_eq_neg: |
|
20485 | 392 |
"((number_of x::'a::{ordered_idom,number_ring}) < number_of y) |
393 |
= neg (number_of (x + uminus y) :: 'a)" |
|
15013 | 394 |
apply (subst less_iff_diff_less_0) |
395 |
apply (simp add: neg_def diff_minus number_of_add number_of_minus) |
|
396 |
done |
|
397 |
||
20485 | 398 |
text {* |
399 |
If @{term Numeral0} is rewritten to 0 then this rule can't be applied: |
|
400 |
@{term Numeral0} IS @{term "number_of Pls"} |
|
401 |
*} |
|
402 |
||
15013 | 403 |
lemma not_neg_number_of_Pls: |
20485 | 404 |
"~ neg (number_of Pls ::'a::{ordered_idom,number_ring})" |
405 |
by (simp add: neg_def numeral_0_eq_0) |
|
15013 | 406 |
|
407 |
lemma neg_number_of_Min: |
|
20485 | 408 |
"neg (number_of Min ::'a::{ordered_idom,number_ring})" |
409 |
by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1) |
|
15013 | 410 |
|
20485 | 411 |
lemma double_less_0_iff: |
412 |
"(a + a < 0) = (a < (0::'a::ordered_idom))" |
|
15013 | 413 |
proof - |
414 |
have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib) |
|
415 |
also have "... = (a < 0)" |
|
416 |
by (simp add: mult_less_0_iff zero_less_two |
|
417 |
order_less_not_sym [OF zero_less_two]) |
|
418 |
finally show ?thesis . |
|
419 |
qed |
|
420 |
||
20485 | 421 |
lemma odd_less_0: |
422 |
"(1 + z + z < 0) = (z < (0::int))"; |
|
15013 | 423 |
proof (cases z rule: int_cases) |
424 |
case (nonneg n) |
|
425 |
thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing |
|
426 |
le_imp_0_less [THEN order_less_imp_le]) |
|
427 |
next |
|
428 |
case (neg n) |
|
429 |
thus ?thesis by (simp del: int_Suc |
|
20485 | 430 |
add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls) |
15013 | 431 |
qed |
432 |
||
20485 | 433 |
text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *} |
434 |
||
15013 | 435 |
lemma Ints_odd_less_0: |
20485 | 436 |
assumes in_Ints: "a \<in> Ints" |
437 |
shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))"; |
|
438 |
proof - |
|
439 |
from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] . |
|
15013 | 440 |
then obtain z where a: "a = of_int z" .. |
441 |
hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))" |
|
442 |
by (simp add: a) |
|
443 |
also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0) |
|
444 |
also have "... = (a < 0)" by (simp add: a) |
|
445 |
finally show ?thesis . |
|
446 |
qed |
|
447 |
||
448 |
lemma neg_number_of_BIT: |
|
20485 | 449 |
"neg (number_of (w BIT x)::'a) = |
450 |
neg (number_of w :: 'a::{ordered_idom,number_ring})" |
|
451 |
by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff |
|
452 |
Ints_odd_less_0 Ints_def split: bit.split) |
|
15013 | 453 |
|
20596 | 454 |
|
20485 | 455 |
text {* Less-Than or Equals *} |
456 |
||
457 |
text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *} |
|
15013 | 458 |
|
459 |
lemmas le_number_of_eq_not_less = |
|
20485 | 460 |
linorder_not_less [of "number_of w" "number_of v", symmetric, |
461 |
standard] |
|
15013 | 462 |
|
463 |
lemma le_number_of_eq: |
|
464 |
"((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y) |
|
20485 | 465 |
= (~ (neg (number_of (y + uminus x) :: 'a)))" |
15013 | 466 |
by (simp add: le_number_of_eq_not_less less_number_of_eq_neg) |
467 |
||
468 |
||
20485 | 469 |
text {* Absolute value (@{term abs}) *} |
15013 | 470 |
|
471 |
lemma abs_number_of: |
|
20485 | 472 |
"abs(number_of x::'a::{ordered_idom,number_ring}) = |
473 |
(if number_of x < (0::'a) then -number_of x else number_of x)" |
|
474 |
by (simp add: abs_if) |
|
15013 | 475 |
|
476 |
||
20485 | 477 |
text {* Re-orientation of the equation nnn=x *} |
15013 | 478 |
|
20485 | 479 |
lemma number_of_reorient: |
480 |
"(number_of w = x) = (x = number_of w)" |
|
481 |
by auto |
|
15013 | 482 |
|
483 |
||
20485 | 484 |
subsection {* Simplification of arithmetic operations on integer constants. *} |
15013 | 485 |
|
20900 | 486 |
lemmas arith_extra_simps [standard] = |
20485 | 487 |
number_of_add [symmetric] |
488 |
number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric] |
|
489 |
number_of_mult [symmetric] |
|
490 |
diff_number_of_eq abs_number_of |
|
491 |
||
492 |
text {* |
|
493 |
For making a minimal simpset, one must include these default simprules. |
|
494 |
Also include @{text simp_thms}. |
|
495 |
*} |
|
15013 | 496 |
|
20485 | 497 |
lemmas arith_simps = |
498 |
bit.distinct |
|
499 |
Pls_0_eq Min_1_eq |
|
500 |
pred_Pls pred_Min pred_1 pred_0 |
|
501 |
succ_Pls succ_Min succ_1 succ_0 |
|
502 |
add_Pls add_Min add_BIT_0 add_BIT_10 add_BIT_11 |
|
503 |
minus_Pls minus_Min minus_1 minus_0 |
|
504 |
mult_Pls mult_Min mult_num1 mult_num0 |
|
505 |
add_Pls_right add_Min_right |
|
506 |
abs_zero abs_one arith_extra_simps |
|
15013 | 507 |
|
20485 | 508 |
text {* Simplification of relational operations *} |
15013 | 509 |
|
20485 | 510 |
lemmas rel_simps = |
511 |
eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min |
|
512 |
iszero_number_of_0 iszero_number_of_1 |
|
513 |
less_number_of_eq_neg |
|
514 |
not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1 |
|
515 |
neg_number_of_Min neg_number_of_BIT |
|
516 |
le_number_of_eq |
|
517 |
||
518 |
declare arith_extra_simps [simp] |
|
519 |
declare rel_simps [simp] |
|
15013 | 520 |
|
521 |
||
20485 | 522 |
subsection {* Simplification of arithmetic when nested to the right. *} |
15013 | 523 |
|
524 |
lemma add_number_of_left [simp]: |
|
20485 | 525 |
"number_of v + (number_of w + z) = |
526 |
(number_of(v + w) + z::'a::number_ring)" |
|
527 |
by (simp add: add_assoc [symmetric]) |
|
15013 | 528 |
|
529 |
lemma mult_number_of_left [simp]: |
|
20485 | 530 |
"number_of v * (number_of w * z) = |
531 |
(number_of(v * w) * z::'a::number_ring)" |
|
532 |
by (simp add: mult_assoc [symmetric]) |
|
15013 | 533 |
|
534 |
lemma add_number_of_diff1: |
|
20485 | 535 |
"number_of v + (number_of w - c) = |
536 |
number_of(v + w) - (c::'a::number_ring)" |
|
537 |
by (simp add: diff_minus add_number_of_left) |
|
15013 | 538 |
|
20485 | 539 |
lemma add_number_of_diff2 [simp]: |
540 |
"number_of v + (c - number_of w) = |
|
541 |
number_of (v + uminus w) + (c::'a::number_ring)" |
|
15013 | 542 |
apply (subst diff_number_of_eq [symmetric]) |
543 |
apply (simp only: compare_rls) |
|
544 |
done |
|
545 |
||
19380 | 546 |
|
20500 | 547 |
hide (open) const Pls Min B0 B1 succ pred |
19380 | 548 |
|
15013 | 549 |
end |