15013
|
1 |
(* Title: HOL/Integ/Numeral.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1994 University of Cambridge
|
|
5 |
*)
|
|
6 |
|
|
7 |
header{*Arithmetic on Binary Integers*}
|
|
8 |
|
15131
|
9 |
theory Numeral
|
15140
|
10 |
imports IntDef
|
15131
|
11 |
files "Tools/numeral_syntax.ML"
|
|
12 |
begin
|
15013
|
13 |
|
|
14 |
text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
|
|
15 |
Only qualified access Numeral.Pls and Numeral.Min is allowed.
|
|
16 |
We do not hide Bit because we need the BIT infix syntax.*}
|
|
17 |
|
|
18 |
text{*This formalization defines binary arithmetic in terms of the integers
|
|
19 |
rather than using a datatype. This avoids multiple representations (leading
|
|
20 |
zeroes, etc.) See @{text "ZF/Integ/twos-compl.ML"}, function @{text
|
|
21 |
int_of_binary}, for the numerical interpretation.
|
|
22 |
|
|
23 |
The representation expects that @{text "(m mod 2)"} is 0 or 1,
|
|
24 |
even if m is negative;
|
|
25 |
For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
|
|
26 |
@{text "-5 = (-3)*2 + 1"}.
|
|
27 |
*}
|
|
28 |
|
|
29 |
|
|
30 |
typedef (Bin)
|
|
31 |
bin = "UNIV::int set"
|
|
32 |
by (auto)
|
|
33 |
|
|
34 |
constdefs
|
|
35 |
Pls :: "bin"
|
|
36 |
"Pls == Abs_Bin 0"
|
|
37 |
|
|
38 |
Min :: "bin"
|
|
39 |
"Min == Abs_Bin (- 1)"
|
|
40 |
|
|
41 |
Bit :: "[bin,bool] => bin" (infixl "BIT" 90)
|
|
42 |
--{*That is, 2w+b*}
|
|
43 |
"w BIT b == Abs_Bin ((if b then 1 else 0) + Rep_Bin w + Rep_Bin w)"
|
|
44 |
|
|
45 |
|
|
46 |
axclass
|
|
47 |
number < type -- {* for numeric types: nat, int, real, \dots *}
|
|
48 |
|
|
49 |
consts
|
|
50 |
number_of :: "bin => 'a::number"
|
|
51 |
|
|
52 |
syntax
|
|
53 |
"_Numeral" :: "num_const => 'a" ("_")
|
|
54 |
Numeral0 :: 'a
|
|
55 |
Numeral1 :: 'a
|
|
56 |
|
|
57 |
translations
|
|
58 |
"Numeral0" == "number_of Numeral.Pls"
|
|
59 |
"Numeral1" == "number_of (Numeral.Pls BIT True)"
|
|
60 |
|
|
61 |
|
|
62 |
setup NumeralSyntax.setup
|
|
63 |
|
|
64 |
syntax (xsymbols)
|
|
65 |
"_square" :: "'a => 'a" ("(_\<twosuperior>)" [1000] 999)
|
|
66 |
syntax (HTML output)
|
|
67 |
"_square" :: "'a => 'a" ("(_\<twosuperior>)" [1000] 999)
|
|
68 |
syntax (output)
|
|
69 |
"_square" :: "'a => 'a" ("(_ ^/ 2)" [81] 80)
|
|
70 |
translations
|
|
71 |
"x\<twosuperior>" == "x^2"
|
|
72 |
"x\<twosuperior>" <= "x^(2::nat)"
|
|
73 |
|
|
74 |
|
|
75 |
lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
|
|
76 |
-- {* Unfold all @{text let}s involving constants *}
|
|
77 |
by (simp add: Let_def)
|
|
78 |
|
|
79 |
lemma Let_0 [simp]: "Let 0 f == f 0"
|
|
80 |
by (simp add: Let_def)
|
|
81 |
|
|
82 |
lemma Let_1 [simp]: "Let 1 f == f 1"
|
|
83 |
by (simp add: Let_def)
|
|
84 |
|
|
85 |
|
|
86 |
constdefs
|
|
87 |
bin_succ :: "bin=>bin"
|
|
88 |
"bin_succ w == Abs_Bin(Rep_Bin w + 1)"
|
|
89 |
|
|
90 |
bin_pred :: "bin=>bin"
|
|
91 |
"bin_pred w == Abs_Bin(Rep_Bin w - 1)"
|
|
92 |
|
|
93 |
bin_minus :: "bin=>bin"
|
|
94 |
"bin_minus w == Abs_Bin(- (Rep_Bin w))"
|
|
95 |
|
|
96 |
bin_add :: "[bin,bin]=>bin"
|
|
97 |
"bin_add v w == Abs_Bin(Rep_Bin v + Rep_Bin w)"
|
|
98 |
|
|
99 |
bin_mult :: "[bin,bin]=>bin"
|
|
100 |
"bin_mult v w == Abs_Bin(Rep_Bin v * Rep_Bin w)"
|
|
101 |
|
|
102 |
|
|
103 |
lemmas Bin_simps =
|
|
104 |
bin_succ_def bin_pred_def bin_minus_def bin_add_def bin_mult_def
|
|
105 |
Pls_def Min_def Bit_def Abs_Bin_inverse Rep_Bin_inverse Bin_def
|
|
106 |
|
|
107 |
text{*Removal of leading zeroes*}
|
|
108 |
lemma Pls_0_eq [simp]: "Numeral.Pls BIT False = Numeral.Pls"
|
|
109 |
by (simp add: Bin_simps)
|
|
110 |
|
|
111 |
lemma Min_1_eq [simp]: "Numeral.Min BIT True = Numeral.Min"
|
|
112 |
by (simp add: Bin_simps)
|
|
113 |
|
|
114 |
subsection{*The Functions @{term bin_succ}, @{term bin_pred} and @{term bin_minus}*}
|
|
115 |
|
|
116 |
lemma bin_succ_Pls [simp]: "bin_succ Numeral.Pls = Numeral.Pls BIT True"
|
|
117 |
by (simp add: Bin_simps)
|
|
118 |
|
|
119 |
lemma bin_succ_Min [simp]: "bin_succ Numeral.Min = Numeral.Pls"
|
|
120 |
by (simp add: Bin_simps)
|
|
121 |
|
|
122 |
lemma bin_succ_1 [simp]: "bin_succ(w BIT True) = (bin_succ w) BIT False"
|
|
123 |
by (simp add: Bin_simps add_ac)
|
|
124 |
|
|
125 |
lemma bin_succ_0 [simp]: "bin_succ(w BIT False) = w BIT True"
|
|
126 |
by (simp add: Bin_simps add_ac)
|
|
127 |
|
|
128 |
lemma bin_pred_Pls [simp]: "bin_pred Numeral.Pls = Numeral.Min"
|
|
129 |
by (simp add: Bin_simps)
|
|
130 |
|
|
131 |
lemma bin_pred_Min [simp]: "bin_pred Numeral.Min = Numeral.Min BIT False"
|
|
132 |
by (simp add: Bin_simps diff_minus)
|
|
133 |
|
|
134 |
lemma bin_pred_1 [simp]: "bin_pred(w BIT True) = w BIT False"
|
|
135 |
by (simp add: Bin_simps)
|
|
136 |
|
|
137 |
lemma bin_pred_0 [simp]: "bin_pred(w BIT False) = (bin_pred w) BIT True"
|
|
138 |
by (simp add: Bin_simps diff_minus add_ac)
|
|
139 |
|
|
140 |
lemma bin_minus_Pls [simp]: "bin_minus Numeral.Pls = Numeral.Pls"
|
|
141 |
by (simp add: Bin_simps)
|
|
142 |
|
|
143 |
lemma bin_minus_Min [simp]: "bin_minus Numeral.Min = Numeral.Pls BIT True"
|
|
144 |
by (simp add: Bin_simps)
|
|
145 |
|
|
146 |
lemma bin_minus_1 [simp]:
|
|
147 |
"bin_minus (w BIT True) = bin_pred (bin_minus w) BIT True"
|
|
148 |
by (simp add: Bin_simps add_ac diff_minus)
|
|
149 |
|
|
150 |
lemma bin_minus_0 [simp]: "bin_minus(w BIT False) = (bin_minus w) BIT False"
|
|
151 |
by (simp add: Bin_simps)
|
|
152 |
|
|
153 |
|
|
154 |
subsection{*Binary Addition and Multiplication:
|
|
155 |
@{term bin_add} and @{term bin_mult}*}
|
|
156 |
|
|
157 |
lemma bin_add_Pls [simp]: "bin_add Numeral.Pls w = w"
|
|
158 |
by (simp add: Bin_simps)
|
|
159 |
|
|
160 |
lemma bin_add_Min [simp]: "bin_add Numeral.Min w = bin_pred w"
|
|
161 |
by (simp add: Bin_simps diff_minus add_ac)
|
|
162 |
|
|
163 |
lemma bin_add_BIT_11 [simp]:
|
|
164 |
"bin_add (v BIT True) (w BIT True) = bin_add v (bin_succ w) BIT False"
|
|
165 |
by (simp add: Bin_simps add_ac)
|
|
166 |
|
|
167 |
lemma bin_add_BIT_10 [simp]:
|
|
168 |
"bin_add (v BIT True) (w BIT False) = (bin_add v w) BIT True"
|
|
169 |
by (simp add: Bin_simps add_ac)
|
|
170 |
|
|
171 |
lemma bin_add_BIT_0 [simp]:
|
|
172 |
"bin_add (v BIT False) (w BIT y) = bin_add v w BIT y"
|
|
173 |
by (simp add: Bin_simps add_ac)
|
|
174 |
|
|
175 |
lemma bin_add_Pls_right [simp]: "bin_add w Numeral.Pls = w"
|
|
176 |
by (simp add: Bin_simps)
|
|
177 |
|
|
178 |
lemma bin_add_Min_right [simp]: "bin_add w Numeral.Min = bin_pred w"
|
|
179 |
by (simp add: Bin_simps diff_minus)
|
|
180 |
|
|
181 |
lemma bin_mult_Pls [simp]: "bin_mult Numeral.Pls w = Numeral.Pls"
|
|
182 |
by (simp add: Bin_simps)
|
|
183 |
|
|
184 |
lemma bin_mult_Min [simp]: "bin_mult Numeral.Min w = bin_minus w"
|
|
185 |
by (simp add: Bin_simps)
|
|
186 |
|
|
187 |
lemma bin_mult_1 [simp]:
|
|
188 |
"bin_mult (v BIT True) w = bin_add ((bin_mult v w) BIT False) w"
|
|
189 |
by (simp add: Bin_simps add_ac left_distrib)
|
|
190 |
|
|
191 |
lemma bin_mult_0 [simp]: "bin_mult (v BIT False) w = (bin_mult v w) BIT False"
|
|
192 |
by (simp add: Bin_simps left_distrib)
|
|
193 |
|
|
194 |
|
|
195 |
|
|
196 |
subsection{*Converting Numerals to Rings: @{term number_of}*}
|
|
197 |
|
|
198 |
axclass number_ring \<subseteq> number, comm_ring_1
|
|
199 |
number_of_eq: "number_of w = of_int (Rep_Bin w)"
|
|
200 |
|
|
201 |
lemma number_of_succ:
|
|
202 |
"number_of(bin_succ w) = (1 + number_of w ::'a::number_ring)"
|
|
203 |
by (simp add: number_of_eq Bin_simps)
|
|
204 |
|
|
205 |
lemma number_of_pred:
|
|
206 |
"number_of(bin_pred w) = (- 1 + number_of w ::'a::number_ring)"
|
|
207 |
by (simp add: number_of_eq Bin_simps)
|
|
208 |
|
|
209 |
lemma number_of_minus:
|
|
210 |
"number_of(bin_minus w) = (- (number_of w)::'a::number_ring)"
|
|
211 |
by (simp add: number_of_eq Bin_simps)
|
|
212 |
|
|
213 |
lemma number_of_add:
|
|
214 |
"number_of(bin_add v w) = (number_of v + number_of w::'a::number_ring)"
|
|
215 |
by (simp add: number_of_eq Bin_simps)
|
|
216 |
|
|
217 |
lemma number_of_mult:
|
|
218 |
"number_of(bin_mult v w) = (number_of v * number_of w::'a::number_ring)"
|
|
219 |
by (simp add: number_of_eq Bin_simps)
|
|
220 |
|
|
221 |
text{*The correctness of shifting. But it doesn't seem to give a measurable
|
|
222 |
speed-up.*}
|
|
223 |
lemma double_number_of_BIT:
|
|
224 |
"(1+1) * number_of w = (number_of (w BIT False) ::'a::number_ring)"
|
|
225 |
by (simp add: number_of_eq Bin_simps left_distrib)
|
|
226 |
|
|
227 |
text{*Converting numerals 0 and 1 to their abstract versions*}
|
|
228 |
lemma numeral_0_eq_0 [simp]: "Numeral0 = (0::'a::number_ring)"
|
|
229 |
by (simp add: number_of_eq Bin_simps)
|
|
230 |
|
|
231 |
lemma numeral_1_eq_1 [simp]: "Numeral1 = (1::'a::number_ring)"
|
|
232 |
by (simp add: number_of_eq Bin_simps)
|
|
233 |
|
|
234 |
text{*Special-case simplification for small constants*}
|
|
235 |
|
|
236 |
text{*Unary minus for the abstract constant 1. Cannot be inserted
|
|
237 |
as a simprule until later: it is @{text number_of_Min} re-oriented!*}
|
|
238 |
lemma numeral_m1_eq_minus_1: "(-1::'a::number_ring) = - 1"
|
|
239 |
by (simp add: number_of_eq Bin_simps)
|
|
240 |
|
|
241 |
|
|
242 |
lemma mult_minus1 [simp]: "-1 * z = -(z::'a::number_ring)"
|
|
243 |
by (simp add: numeral_m1_eq_minus_1)
|
|
244 |
|
|
245 |
lemma mult_minus1_right [simp]: "z * -1 = -(z::'a::number_ring)"
|
|
246 |
by (simp add: numeral_m1_eq_minus_1)
|
|
247 |
|
|
248 |
(*Negation of a coefficient*)
|
|
249 |
lemma minus_number_of_mult [simp]:
|
|
250 |
"- (number_of w) * z = number_of(bin_minus w) * (z::'a::number_ring)"
|
|
251 |
by (simp add: number_of_minus)
|
|
252 |
|
|
253 |
text{*Subtraction*}
|
|
254 |
lemma diff_number_of_eq:
|
|
255 |
"number_of v - number_of w =
|
|
256 |
(number_of(bin_add v (bin_minus w))::'a::number_ring)"
|
|
257 |
by (simp add: diff_minus number_of_add number_of_minus)
|
|
258 |
|
|
259 |
|
|
260 |
lemma number_of_Pls: "number_of Numeral.Pls = (0::'a::number_ring)"
|
|
261 |
by (simp add: number_of_eq Bin_simps)
|
|
262 |
|
|
263 |
lemma number_of_Min: "number_of Numeral.Min = (- 1::'a::number_ring)"
|
|
264 |
by (simp add: number_of_eq Bin_simps)
|
|
265 |
|
|
266 |
lemma number_of_BIT:
|
|
267 |
"number_of(w BIT x) = (if x then 1 else (0::'a::number_ring)) +
|
|
268 |
(number_of w) + (number_of w)"
|
|
269 |
by (simp add: number_of_eq Bin_simps)
|
|
270 |
|
|
271 |
|
|
272 |
|
|
273 |
subsection{*Equality of Binary Numbers*}
|
|
274 |
|
|
275 |
text{*First version by Norbert Voelker*}
|
|
276 |
|
|
277 |
lemma eq_number_of_eq:
|
|
278 |
"((number_of x::'a::number_ring) = number_of y) =
|
|
279 |
iszero (number_of (bin_add x (bin_minus y)) :: 'a)"
|
|
280 |
by (simp add: iszero_def compare_rls number_of_add number_of_minus)
|
|
281 |
|
|
282 |
lemma iszero_number_of_Pls: "iszero ((number_of Numeral.Pls)::'a::number_ring)"
|
|
283 |
by (simp add: iszero_def numeral_0_eq_0)
|
|
284 |
|
|
285 |
lemma nonzero_number_of_Min: "~ iszero ((number_of Numeral.Min)::'a::number_ring)"
|
|
286 |
by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)
|
|
287 |
|
|
288 |
|
|
289 |
subsection{*Comparisons, for Ordered Rings*}
|
|
290 |
|
|
291 |
lemma double_eq_0_iff: "(a + a = 0) = (a = (0::'a::ordered_idom))"
|
|
292 |
proof -
|
|
293 |
have "a + a = (1+1)*a" by (simp add: left_distrib)
|
|
294 |
with zero_less_two [where 'a = 'a]
|
|
295 |
show ?thesis by force
|
|
296 |
qed
|
|
297 |
|
|
298 |
lemma le_imp_0_less:
|
|
299 |
assumes le: "0 \<le> z" shows "(0::int) < 1 + z"
|
|
300 |
proof -
|
|
301 |
have "0 \<le> z" .
|
|
302 |
also have "... < z + 1" by (rule less_add_one)
|
|
303 |
also have "... = 1 + z" by (simp add: add_ac)
|
|
304 |
finally show "0 < 1 + z" .
|
|
305 |
qed
|
|
306 |
|
|
307 |
lemma odd_nonzero: "1 + z + z \<noteq> (0::int)";
|
|
308 |
proof (cases z rule: int_cases)
|
|
309 |
case (nonneg n)
|
|
310 |
have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
|
|
311 |
thus ?thesis using le_imp_0_less [OF le]
|
|
312 |
by (auto simp add: add_assoc)
|
|
313 |
next
|
|
314 |
case (neg n)
|
|
315 |
show ?thesis
|
|
316 |
proof
|
|
317 |
assume eq: "1 + z + z = 0"
|
|
318 |
have "0 < 1 + (int n + int n)"
|
|
319 |
by (simp add: le_imp_0_less add_increasing)
|
|
320 |
also have "... = - (1 + z + z)"
|
|
321 |
by (simp add: neg add_assoc [symmetric])
|
|
322 |
also have "... = 0" by (simp add: eq)
|
|
323 |
finally have "0<0" ..
|
|
324 |
thus False by blast
|
|
325 |
qed
|
|
326 |
qed
|
|
327 |
|
|
328 |
|
|
329 |
text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
|
|
330 |
lemma Ints_odd_nonzero: "a \<in> Ints ==> 1 + a + a \<noteq> (0::'a::ordered_idom)"
|
|
331 |
proof (unfold Ints_def)
|
|
332 |
assume "a \<in> range of_int"
|
|
333 |
then obtain z where a: "a = of_int z" ..
|
|
334 |
show ?thesis
|
|
335 |
proof
|
|
336 |
assume eq: "1 + a + a = 0"
|
|
337 |
hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
|
|
338 |
hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
|
|
339 |
with odd_nonzero show False by blast
|
|
340 |
qed
|
|
341 |
qed
|
|
342 |
|
|
343 |
lemma Ints_number_of: "(number_of w :: 'a::number_ring) \<in> Ints"
|
|
344 |
by (simp add: number_of_eq Ints_def)
|
|
345 |
|
|
346 |
|
|
347 |
lemma iszero_number_of_BIT:
|
|
348 |
"iszero (number_of (w BIT x)::'a) =
|
|
349 |
(~x & iszero (number_of w::'a::{ordered_idom,number_ring}))"
|
|
350 |
by (simp add: iszero_def number_of_eq Bin_simps double_eq_0_iff
|
|
351 |
Ints_odd_nonzero Ints_def)
|
|
352 |
|
|
353 |
lemma iszero_number_of_0:
|
|
354 |
"iszero (number_of (w BIT False) :: 'a::{ordered_idom,number_ring}) =
|
|
355 |
iszero (number_of w :: 'a)"
|
|
356 |
by (simp only: iszero_number_of_BIT simp_thms)
|
|
357 |
|
|
358 |
lemma iszero_number_of_1:
|
|
359 |
"~ iszero (number_of (w BIT True)::'a::{ordered_idom,number_ring})"
|
|
360 |
by (simp only: iszero_number_of_BIT simp_thms)
|
|
361 |
|
|
362 |
|
|
363 |
|
|
364 |
subsection{*The Less-Than Relation*}
|
|
365 |
|
|
366 |
lemma less_number_of_eq_neg:
|
|
367 |
"((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
|
|
368 |
= neg (number_of (bin_add x (bin_minus y)) :: 'a)"
|
|
369 |
apply (subst less_iff_diff_less_0)
|
|
370 |
apply (simp add: neg_def diff_minus number_of_add number_of_minus)
|
|
371 |
done
|
|
372 |
|
|
373 |
text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
|
|
374 |
@{term Numeral0} IS @{term "number_of Numeral.Pls"} *}
|
|
375 |
lemma not_neg_number_of_Pls:
|
|
376 |
"~ neg (number_of Numeral.Pls ::'a::{ordered_idom,number_ring})"
|
|
377 |
by (simp add: neg_def numeral_0_eq_0)
|
|
378 |
|
|
379 |
lemma neg_number_of_Min:
|
|
380 |
"neg (number_of Numeral.Min ::'a::{ordered_idom,number_ring})"
|
|
381 |
by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
|
|
382 |
|
|
383 |
lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))"
|
|
384 |
proof -
|
|
385 |
have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
|
|
386 |
also have "... = (a < 0)"
|
|
387 |
by (simp add: mult_less_0_iff zero_less_two
|
|
388 |
order_less_not_sym [OF zero_less_two])
|
|
389 |
finally show ?thesis .
|
|
390 |
qed
|
|
391 |
|
|
392 |
lemma odd_less_0: "(1 + z + z < 0) = (z < (0::int))";
|
|
393 |
proof (cases z rule: int_cases)
|
|
394 |
case (nonneg n)
|
|
395 |
thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
|
|
396 |
le_imp_0_less [THEN order_less_imp_le])
|
|
397 |
next
|
|
398 |
case (neg n)
|
|
399 |
thus ?thesis by (simp del: int_Suc
|
|
400 |
add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
|
|
401 |
qed
|
|
402 |
|
|
403 |
text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
|
|
404 |
lemma Ints_odd_less_0:
|
|
405 |
"a \<in> Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_idom))";
|
|
406 |
proof (unfold Ints_def)
|
|
407 |
assume "a \<in> range of_int"
|
|
408 |
then obtain z where a: "a = of_int z" ..
|
|
409 |
hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
|
|
410 |
by (simp add: a)
|
|
411 |
also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
|
|
412 |
also have "... = (a < 0)" by (simp add: a)
|
|
413 |
finally show ?thesis .
|
|
414 |
qed
|
|
415 |
|
|
416 |
lemma neg_number_of_BIT:
|
|
417 |
"neg (number_of (w BIT x)::'a) =
|
|
418 |
neg (number_of w :: 'a::{ordered_idom,number_ring})"
|
|
419 |
by (simp add: neg_def number_of_eq Bin_simps double_less_0_iff
|
|
420 |
Ints_odd_less_0 Ints_def)
|
|
421 |
|
|
422 |
|
|
423 |
text{*Less-Than or Equals*}
|
|
424 |
|
|
425 |
text{*Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals*}
|
|
426 |
lemmas le_number_of_eq_not_less =
|
|
427 |
linorder_not_less [of "number_of w" "number_of v", symmetric,
|
|
428 |
standard]
|
|
429 |
|
|
430 |
lemma le_number_of_eq:
|
|
431 |
"((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
|
|
432 |
= (~ (neg (number_of (bin_add y (bin_minus x)) :: 'a)))"
|
|
433 |
by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
|
|
434 |
|
|
435 |
|
|
436 |
text{*Absolute value (@{term abs})*}
|
|
437 |
|
|
438 |
lemma abs_number_of:
|
|
439 |
"abs(number_of x::'a::{ordered_idom,number_ring}) =
|
|
440 |
(if number_of x < (0::'a) then -number_of x else number_of x)"
|
|
441 |
by (simp add: abs_if)
|
|
442 |
|
|
443 |
|
|
444 |
text{*Re-orientation of the equation nnn=x*}
|
|
445 |
lemma number_of_reorient: "(number_of w = x) = (x = number_of w)"
|
|
446 |
by auto
|
|
447 |
|
|
448 |
|
|
449 |
|
|
450 |
|
|
451 |
subsection{*Simplification of arithmetic operations on integer constants.*}
|
|
452 |
|
|
453 |
lemmas bin_arith_extra_simps =
|
|
454 |
number_of_add [symmetric]
|
|
455 |
number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
|
|
456 |
number_of_mult [symmetric]
|
|
457 |
diff_number_of_eq abs_number_of
|
|
458 |
|
|
459 |
text{*For making a minimal simpset, one must include these default simprules.
|
|
460 |
Also include @{text simp_thms} or at least @{term "(~False)=True"} *}
|
|
461 |
lemmas bin_arith_simps =
|
|
462 |
Pls_0_eq Min_1_eq
|
|
463 |
bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
|
|
464 |
bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
|
|
465 |
bin_add_Pls bin_add_Min bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
|
|
466 |
bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
|
|
467 |
bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0
|
|
468 |
bin_add_Pls_right bin_add_Min_right
|
|
469 |
abs_zero abs_one bin_arith_extra_simps
|
|
470 |
|
|
471 |
text{*Simplification of relational operations*}
|
|
472 |
lemmas bin_rel_simps =
|
|
473 |
eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
|
|
474 |
iszero_number_of_0 iszero_number_of_1
|
|
475 |
less_number_of_eq_neg
|
|
476 |
not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
|
|
477 |
neg_number_of_Min neg_number_of_BIT
|
|
478 |
le_number_of_eq
|
|
479 |
|
|
480 |
declare bin_arith_extra_simps [simp]
|
|
481 |
declare bin_rel_simps [simp]
|
|
482 |
|
|
483 |
|
|
484 |
subsection{*Simplification of arithmetic when nested to the right*}
|
|
485 |
|
|
486 |
lemma add_number_of_left [simp]:
|
|
487 |
"number_of v + (number_of w + z) =
|
|
488 |
(number_of(bin_add v w) + z::'a::number_ring)"
|
|
489 |
by (simp add: add_assoc [symmetric])
|
|
490 |
|
|
491 |
lemma mult_number_of_left [simp]:
|
|
492 |
"number_of v * (number_of w * z) =
|
|
493 |
(number_of(bin_mult v w) * z::'a::number_ring)"
|
|
494 |
by (simp add: mult_assoc [symmetric])
|
|
495 |
|
|
496 |
lemma add_number_of_diff1:
|
|
497 |
"number_of v + (number_of w - c) =
|
|
498 |
number_of(bin_add v w) - (c::'a::number_ring)"
|
|
499 |
by (simp add: diff_minus add_number_of_left)
|
|
500 |
|
|
501 |
lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) =
|
|
502 |
number_of (bin_add v (bin_minus w)) + (c::'a::number_ring)"
|
|
503 |
apply (subst diff_number_of_eq [symmetric])
|
|
504 |
apply (simp only: compare_rls)
|
|
505 |
done
|
|
506 |
|
|
507 |
end
|