author | wenzelm |
Sat, 17 Mar 2018 20:32:39 +0100 | |
changeset 67895 | cd00999d2d30 |
parent 67828 | 655d03493d0f |
child 67905 | fe0f4eeceeb7 |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Parity.thy |
2 |
Author: Jeremy Avigad |
|
3 |
Author: Jacques D. Fleuriot |
|
21256 | 4 |
*) |
5 |
||
60758 | 6 |
section \<open>Parity in rings and semirings\<close> |
21256 | 7 |
|
8 |
theory Parity |
|
66815 | 9 |
imports Euclidean_Division |
21256 | 10 |
begin |
11 |
||
61799 | 12 |
subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close> |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
13 |
|
66815 | 14 |
class semiring_parity = linordered_semidom + unique_euclidean_semiring + |
15 |
assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n" |
|
66839 | 16 |
and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1" |
17 |
and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a" |
|
18 |
begin |
|
19 |
||
20 |
lemma division_segment_eq_iff: |
|
21 |
"a = b" if "division_segment a = division_segment b" |
|
22 |
and "euclidean_size a = euclidean_size b" |
|
23 |
using that division_segment_euclidean_size [of a] by simp |
|
24 |
||
25 |
lemma euclidean_size_of_nat [simp]: |
|
26 |
"euclidean_size (of_nat n) = n" |
|
27 |
proof - |
|
28 |
have "division_segment (of_nat n) * of_nat (euclidean_size (of_nat n)) = of_nat n" |
|
29 |
by (fact division_segment_euclidean_size) |
|
30 |
then show ?thesis by simp |
|
31 |
qed |
|
66815 | 32 |
|
66839 | 33 |
lemma of_nat_euclidean_size: |
34 |
"of_nat (euclidean_size a) = a div division_segment a" |
|
35 |
proof - |
|
36 |
have "of_nat (euclidean_size a) = division_segment a * of_nat (euclidean_size a) div division_segment a" |
|
37 |
by (subst nonzero_mult_div_cancel_left) simp_all |
|
38 |
also have "\<dots> = a div division_segment a" |
|
39 |
by simp |
|
40 |
finally show ?thesis . |
|
41 |
qed |
|
42 |
||
43 |
lemma division_segment_1 [simp]: |
|
44 |
"division_segment 1 = 1" |
|
45 |
using division_segment_of_nat [of 1] by simp |
|
46 |
||
47 |
lemma division_segment_numeral [simp]: |
|
48 |
"division_segment (numeral k) = 1" |
|
49 |
using division_segment_of_nat [of "numeral k"] by simp |
|
50 |
||
51 |
lemma euclidean_size_1 [simp]: |
|
52 |
"euclidean_size 1 = 1" |
|
53 |
using euclidean_size_of_nat [of 1] by simp |
|
54 |
||
55 |
lemma euclidean_size_numeral [simp]: |
|
56 |
"euclidean_size (numeral k) = numeral k" |
|
57 |
using euclidean_size_of_nat [of "numeral k"] by simp |
|
21256 | 58 |
|
66815 | 59 |
lemma of_nat_dvd_iff: |
60 |
"of_nat m dvd of_nat n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q") |
|
61 |
proof (cases "m = 0") |
|
62 |
case True |
|
63 |
then show ?thesis |
|
64 |
by simp |
|
65 |
next |
|
66 |
case False |
|
67 |
show ?thesis |
|
68 |
proof |
|
69 |
assume ?Q |
|
70 |
then show ?P |
|
71 |
by (auto elim: dvd_class.dvdE) |
|
72 |
next |
|
73 |
assume ?P |
|
74 |
with False have "of_nat n = of_nat n div of_nat m * of_nat m" |
|
75 |
by simp |
|
76 |
then have "of_nat n = of_nat (n div m * m)" |
|
77 |
by (simp add: of_nat_div) |
|
78 |
then have "n = n div m * m" |
|
79 |
by (simp only: of_nat_eq_iff) |
|
80 |
then have "n = m * (n div m)" |
|
81 |
by (simp add: ac_simps) |
|
82 |
then show ?Q .. |
|
83 |
qed |
|
84 |
qed |
|
85 |
||
86 |
lemma of_nat_mod: |
|
87 |
"of_nat (m mod n) = of_nat m mod of_nat n" |
|
88 |
proof - |
|
89 |
have "of_nat m div of_nat n * of_nat n + of_nat m mod of_nat n = of_nat m" |
|
90 |
by (simp add: div_mult_mod_eq) |
|
91 |
also have "of_nat m = of_nat (m div n * n + m mod n)" |
|
92 |
by simp |
|
93 |
finally show ?thesis |
|
94 |
by (simp only: of_nat_div of_nat_mult of_nat_add) simp |
|
95 |
qed |
|
96 |
||
97 |
lemma one_div_two_eq_zero [simp]: |
|
98 |
"1 div 2 = 0" |
|
99 |
proof - |
|
100 |
from of_nat_div [symmetric] have "of_nat 1 div of_nat 2 = of_nat 0" |
|
101 |
by (simp only:) simp |
|
102 |
then show ?thesis |
|
103 |
by simp |
|
104 |
qed |
|
105 |
||
106 |
lemma one_mod_two_eq_one [simp]: |
|
107 |
"1 mod 2 = 1" |
|
108 |
proof - |
|
109 |
from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1" |
|
110 |
by (simp only:) simp |
|
111 |
then show ?thesis |
|
112 |
by simp |
|
113 |
qed |
|
59816
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
58889
diff
changeset
|
114 |
|
58740 | 115 |
abbreviation even :: "'a \<Rightarrow> bool" |
63654 | 116 |
where "even a \<equiv> 2 dvd a" |
54228 | 117 |
|
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
118 |
abbreviation odd :: "'a \<Rightarrow> bool" |
63654 | 119 |
where "odd a \<equiv> \<not> 2 dvd a" |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
120 |
|
66815 | 121 |
lemma even_iff_mod_2_eq_zero: |
122 |
"even a \<longleftrightarrow> a mod 2 = 0" |
|
123 |
by (fact dvd_eq_mod_eq_0) |
|
124 |
||
125 |
lemma odd_iff_mod_2_eq_one: |
|
126 |
"odd a \<longleftrightarrow> a mod 2 = 1" |
|
66839 | 127 |
proof |
128 |
assume "a mod 2 = 1" |
|
129 |
then show "odd a" |
|
130 |
by auto |
|
131 |
next |
|
132 |
assume "odd a" |
|
133 |
have eucl: "euclidean_size (a mod 2) = 1" |
|
134 |
proof (rule order_antisym) |
|
135 |
show "euclidean_size (a mod 2) \<le> 1" |
|
136 |
using mod_size_less [of 2 a] by simp |
|
137 |
show "1 \<le> euclidean_size (a mod 2)" |
|
66840 | 138 |
using \<open>odd a\<close> by (simp add: Suc_le_eq dvd_eq_mod_eq_0) |
66839 | 139 |
qed |
140 |
from \<open>odd a\<close> have "\<not> of_nat 2 dvd division_segment a * of_nat (euclidean_size a)" |
|
141 |
by simp |
|
142 |
then have "\<not> of_nat 2 dvd of_nat (euclidean_size a)" |
|
143 |
by (auto simp only: dvd_mult_unit_iff' is_unit_division_segment) |
|
144 |
then have "\<not> 2 dvd euclidean_size a" |
|
145 |
using of_nat_dvd_iff [of 2] by simp |
|
146 |
then have "euclidean_size a mod 2 = 1" |
|
147 |
by (simp add: semidom_modulo_class.dvd_eq_mod_eq_0) |
|
148 |
then have "of_nat (euclidean_size a mod 2) = of_nat 1" |
|
149 |
by simp |
|
150 |
then have "of_nat (euclidean_size a) mod 2 = 1" |
|
151 |
by (simp add: of_nat_mod) |
|
152 |
from \<open>odd a\<close> eucl |
|
153 |
show "a mod 2 = 1" |
|
154 |
by (auto intro: division_segment_eq_iff simp add: division_segment_mod) |
|
155 |
qed |
|
58787 | 156 |
|
66815 | 157 |
lemma parity_cases [case_names even odd]: |
158 |
assumes "even a \<Longrightarrow> a mod 2 = 0 \<Longrightarrow> P" |
|
159 |
assumes "odd a \<Longrightarrow> a mod 2 = 1 \<Longrightarrow> P" |
|
160 |
shows P |
|
161 |
using assms by (cases "even a") (simp_all add: odd_iff_mod_2_eq_one) |
|
162 |
||
163 |
lemma not_mod_2_eq_1_eq_0 [simp]: |
|
164 |
"a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0" |
|
165 |
by (cases a rule: parity_cases) simp_all |
|
166 |
||
167 |
lemma not_mod_2_eq_0_eq_1 [simp]: |
|
168 |
"a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1" |
|
169 |
by (cases a rule: parity_cases) simp_all |
|
58787 | 170 |
|
58690 | 171 |
lemma evenE [elim?]: |
172 |
assumes "even a" |
|
173 |
obtains b where "a = 2 * b" |
|
58740 | 174 |
using assms by (rule dvdE) |
58690 | 175 |
|
58681 | 176 |
lemma oddE [elim?]: |
58680 | 177 |
assumes "odd a" |
178 |
obtains b where "a = 2 * b + 1" |
|
58787 | 179 |
proof - |
66815 | 180 |
have "a = 2 * (a div 2) + a mod 2" |
181 |
by (simp add: mult_div_mod_eq) |
|
182 |
with assms have "a = 2 * (a div 2) + 1" |
|
183 |
by (simp add: odd_iff_mod_2_eq_one) |
|
184 |
then show ?thesis .. |
|
185 |
qed |
|
186 |
||
187 |
lemma mod_2_eq_odd: |
|
188 |
"a mod 2 = of_bool (odd a)" |
|
189 |
by (auto elim: oddE) |
|
190 |
||
67816 | 191 |
lemma of_bool_odd_eq_mod_2: |
192 |
"of_bool (odd a) = a mod 2" |
|
193 |
by (simp add: mod_2_eq_odd) |
|
194 |
||
66815 | 195 |
lemma one_mod_2_pow_eq [simp]: |
196 |
"1 mod (2 ^ n) = of_bool (n > 0)" |
|
197 |
proof - |
|
67083 | 198 |
have "1 mod (2 ^ n) = of_nat (1 mod (2 ^ n))" |
199 |
using of_nat_mod [of 1 "2 ^ n"] by simp |
|
200 |
also have "\<dots> = of_bool (n > 0)" |
|
66815 | 201 |
by simp |
67083 | 202 |
finally show ?thesis . |
66815 | 203 |
qed |
204 |
||
67816 | 205 |
lemma one_div_2_pow_eq [simp]: |
206 |
"1 div (2 ^ n) = of_bool (n = 0)" |
|
207 |
using div_mult_mod_eq [of 1 "2 ^ n"] by auto |
|
208 |
||
66815 | 209 |
lemma even_of_nat [simp]: |
210 |
"even (of_nat a) \<longleftrightarrow> even a" |
|
211 |
proof - |
|
212 |
have "even (of_nat a) \<longleftrightarrow> of_nat 2 dvd of_nat a" |
|
213 |
by simp |
|
214 |
also have "\<dots> \<longleftrightarrow> even a" |
|
215 |
by (simp only: of_nat_dvd_iff) |
|
216 |
finally show ?thesis . |
|
217 |
qed |
|
218 |
||
219 |
lemma even_zero [simp]: |
|
220 |
"even 0" |
|
221 |
by (fact dvd_0_right) |
|
222 |
||
223 |
lemma odd_one [simp]: |
|
224 |
"odd 1" |
|
225 |
proof - |
|
226 |
have "\<not> (2 :: nat) dvd 1" |
|
227 |
by simp |
|
228 |
then have "\<not> of_nat 2 dvd of_nat 1" |
|
229 |
unfolding of_nat_dvd_iff by simp |
|
230 |
then show ?thesis |
|
231 |
by simp |
|
58787 | 232 |
qed |
63654 | 233 |
|
66815 | 234 |
lemma odd_even_add: |
235 |
"even (a + b)" if "odd a" and "odd b" |
|
236 |
proof - |
|
237 |
from that obtain c d where "a = 2 * c + 1" and "b = 2 * d + 1" |
|
238 |
by (blast elim: oddE) |
|
239 |
then have "a + b = 2 * c + 2 * d + (1 + 1)" |
|
240 |
by (simp only: ac_simps) |
|
241 |
also have "\<dots> = 2 * (c + d + 1)" |
|
242 |
by (simp add: algebra_simps) |
|
243 |
finally show ?thesis .. |
|
244 |
qed |
|
245 |
||
246 |
lemma even_add [simp]: |
|
247 |
"even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)" |
|
248 |
by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add) |
|
249 |
||
250 |
lemma odd_add [simp]: |
|
251 |
"odd (a + b) \<longleftrightarrow> \<not> (odd a \<longleftrightarrow> odd b)" |
|
252 |
by simp |
|
253 |
||
254 |
lemma even_plus_one_iff [simp]: |
|
255 |
"even (a + 1) \<longleftrightarrow> odd a" |
|
256 |
by (auto simp add: dvd_add_right_iff intro: odd_even_add) |
|
257 |
||
258 |
lemma even_mult_iff [simp]: |
|
259 |
"even (a * b) \<longleftrightarrow> even a \<or> even b" (is "?P \<longleftrightarrow> ?Q") |
|
260 |
proof |
|
261 |
assume ?Q |
|
262 |
then show ?P |
|
263 |
by auto |
|
264 |
next |
|
265 |
assume ?P |
|
266 |
show ?Q |
|
267 |
proof (rule ccontr) |
|
268 |
assume "\<not> (even a \<or> even b)" |
|
269 |
then have "odd a" and "odd b" |
|
270 |
by auto |
|
271 |
then obtain r s where "a = 2 * r + 1" and "b = 2 * s + 1" |
|
272 |
by (blast elim: oddE) |
|
273 |
then have "a * b = (2 * r + 1) * (2 * s + 1)" |
|
274 |
by simp |
|
275 |
also have "\<dots> = 2 * (2 * r * s + r + s) + 1" |
|
276 |
by (simp add: algebra_simps) |
|
277 |
finally have "odd (a * b)" |
|
278 |
by simp |
|
279 |
with \<open>?P\<close> show False |
|
280 |
by auto |
|
281 |
qed |
|
282 |
qed |
|
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
283 |
|
63654 | 284 |
lemma even_numeral [simp]: "even (numeral (Num.Bit0 n))" |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
285 |
proof - |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
286 |
have "even (2 * numeral n)" |
66815 | 287 |
unfolding even_mult_iff by simp |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
288 |
then have "even (numeral n + numeral n)" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
289 |
unfolding mult_2 . |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
290 |
then show ?thesis |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
291 |
unfolding numeral.simps . |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
292 |
qed |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
293 |
|
63654 | 294 |
lemma odd_numeral [simp]: "odd (numeral (Num.Bit1 n))" |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
295 |
proof |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
296 |
assume "even (numeral (num.Bit1 n))" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
297 |
then have "even (numeral n + numeral n + 1)" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
298 |
unfolding numeral.simps . |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
299 |
then have "even (2 * numeral n + 1)" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
300 |
unfolding mult_2 . |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
301 |
then have "2 dvd numeral n * 2 + 1" |
58740 | 302 |
by (simp add: ac_simps) |
63654 | 303 |
then have "2 dvd 1" |
304 |
using dvd_add_times_triv_left_iff [of 2 "numeral n" 1] by simp |
|
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
305 |
then show False by simp |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
306 |
qed |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
307 |
|
63654 | 308 |
lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0" |
58680 | 309 |
by (induct n) auto |
310 |
||
66815 | 311 |
lemma even_succ_div_two [simp]: |
312 |
"even a \<Longrightarrow> (a + 1) div 2 = a div 2" |
|
313 |
by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero) |
|
314 |
||
315 |
lemma odd_succ_div_two [simp]: |
|
316 |
"odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1" |
|
317 |
by (auto elim!: oddE simp add: add.assoc) |
|
318 |
||
319 |
lemma even_two_times_div_two: |
|
320 |
"even a \<Longrightarrow> 2 * (a div 2) = a" |
|
321 |
by (fact dvd_mult_div_cancel) |
|
322 |
||
323 |
lemma odd_two_times_div_two_succ [simp]: |
|
324 |
"odd a \<Longrightarrow> 2 * (a div 2) + 1 = a" |
|
325 |
using mult_div_mod_eq [of 2 a] |
|
326 |
by (simp add: even_iff_mod_2_eq_zero) |
|
327 |
||
67051 | 328 |
lemma coprime_left_2_iff_odd [simp]: |
329 |
"coprime 2 a \<longleftrightarrow> odd a" |
|
330 |
proof |
|
331 |
assume "odd a" |
|
332 |
show "coprime 2 a" |
|
333 |
proof (rule coprimeI) |
|
334 |
fix b |
|
335 |
assume "b dvd 2" "b dvd a" |
|
336 |
then have "b dvd a mod 2" |
|
337 |
by (auto intro: dvd_mod) |
|
338 |
with \<open>odd a\<close> show "is_unit b" |
|
339 |
by (simp add: mod_2_eq_odd) |
|
340 |
qed |
|
341 |
next |
|
342 |
assume "coprime 2 a" |
|
343 |
show "odd a" |
|
344 |
proof (rule notI) |
|
345 |
assume "even a" |
|
346 |
then obtain b where "a = 2 * b" .. |
|
347 |
with \<open>coprime 2 a\<close> have "coprime 2 (2 * b)" |
|
348 |
by simp |
|
349 |
moreover have "\<not> coprime 2 (2 * b)" |
|
350 |
by (rule not_coprimeI [of 2]) simp_all |
|
351 |
ultimately show False |
|
352 |
by blast |
|
353 |
qed |
|
354 |
qed |
|
355 |
||
356 |
lemma coprime_right_2_iff_odd [simp]: |
|
357 |
"coprime a 2 \<longleftrightarrow> odd a" |
|
358 |
using coprime_left_2_iff_odd [of a] by (simp add: ac_simps) |
|
359 |
||
67828 | 360 |
lemma div_mult2_eq': |
361 |
"a div (of_nat m * of_nat n) = a div of_nat m div of_nat n" |
|
362 |
proof (cases a "of_nat m * of_nat n" rule: divmod_cases) |
|
363 |
case (divides q) |
|
364 |
then show ?thesis |
|
365 |
using nonzero_mult_div_cancel_right [of "of_nat m" "q * of_nat n"] |
|
366 |
by (simp add: ac_simps) |
|
367 |
next |
|
368 |
case (remainder q r) |
|
369 |
then have "division_segment r = 1" |
|
370 |
using division_segment_of_nat [of "m * n"] by simp |
|
371 |
with division_segment_euclidean_size [of r] |
|
372 |
have "of_nat (euclidean_size r) = r" |
|
373 |
by simp |
|
374 |
then have "r div of_nat m = of_nat (euclidean_size r) div of_nat m" |
|
375 |
by simp |
|
376 |
also have "\<dots> = of_nat (euclidean_size r div m)" |
|
377 |
by (simp add: of_nat_div) |
|
378 |
finally have "r div of_nat m = of_nat (euclidean_size r div m)" |
|
379 |
. |
|
380 |
with remainder(1-3) have "r div of_nat m div of_nat n = 0" |
|
381 |
by (auto intro!: div_eqI [of _ "of_nat (euclidean_size r div m)"]) |
|
382 |
(simp add: division_segment_mult euclidean_size_mult ac_simps less_mult_imp_div_less ) |
|
383 |
with remainder(1) |
|
384 |
have "q = (r div of_nat m + q * of_nat n * of_nat m div of_nat m) div of_nat n" |
|
385 |
by simp |
|
386 |
with remainder(5-7) show ?thesis |
|
387 |
using div_plus_div_distrib_dvd_right [of "of_nat m" "q * (of_nat m * of_nat n)" r] |
|
388 |
by (simp add: ac_simps) |
|
389 |
next |
|
390 |
case by0 |
|
391 |
then show ?thesis |
|
392 |
by auto |
|
393 |
qed |
|
394 |
||
395 |
lemma mod_mult2_eq': |
|
396 |
"a mod (of_nat m * of_nat n) = of_nat m * (a div of_nat m mod of_nat n) + a mod of_nat m" |
|
397 |
proof - |
|
398 |
have "a div (of_nat m * of_nat n) * (of_nat m * of_nat n) + a mod (of_nat m * of_nat n) = a div of_nat m div of_nat n * of_nat n * of_nat m + (a div of_nat m mod of_nat n * of_nat m + a mod of_nat m)" |
|
399 |
by (simp add: combine_common_factor div_mult_mod_eq) |
|
400 |
moreover have "a div of_nat m div of_nat n * of_nat n * of_nat m = of_nat n * of_nat m * (a div of_nat m div of_nat n)" |
|
401 |
by (simp add: ac_simps) |
|
402 |
ultimately show ?thesis |
|
403 |
by (simp add: div_mult2_eq' mult_commute) |
|
404 |
qed |
|
405 |
||
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
406 |
end |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
407 |
|
59816
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
58889
diff
changeset
|
408 |
class ring_parity = ring + semiring_parity |
58679 | 409 |
begin |
410 |
||
59816
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
58889
diff
changeset
|
411 |
subclass comm_ring_1 .. |
034b13f4efae
distributivity of partial minus establishes desired properties of dvd in semirings
haftmann
parents:
58889
diff
changeset
|
412 |
|
67816 | 413 |
lemma even_minus: |
66815 | 414 |
"even (- a) \<longleftrightarrow> even a" |
58740 | 415 |
by (fact dvd_minus_iff) |
58679 | 416 |
|
66815 | 417 |
lemma even_diff [simp]: |
418 |
"even (a - b) \<longleftrightarrow> even (a + b)" |
|
58680 | 419 |
using even_add [of a "- b"] by simp |
420 |
||
58679 | 421 |
end |
422 |
||
66808
1907167b6038
elementary definition of division on natural numbers
haftmann
parents:
66582
diff
changeset
|
423 |
|
66815 | 424 |
subsection \<open>Instance for @{typ nat}\<close> |
66808
1907167b6038
elementary definition of division on natural numbers
haftmann
parents:
66582
diff
changeset
|
425 |
|
66815 | 426 |
instance nat :: semiring_parity |
427 |
by standard (simp_all add: dvd_eq_mod_eq_0) |
|
66808
1907167b6038
elementary definition of division on natural numbers
haftmann
parents:
66582
diff
changeset
|
428 |
|
66815 | 429 |
lemma even_Suc_Suc_iff [simp]: |
430 |
"even (Suc (Suc n)) \<longleftrightarrow> even n" |
|
58787 | 431 |
using dvd_add_triv_right_iff [of 2 n] by simp |
58687 | 432 |
|
66815 | 433 |
lemma even_Suc [simp]: "even (Suc n) \<longleftrightarrow> odd n" |
434 |
using even_plus_one_iff [of n] by simp |
|
58787 | 435 |
|
66815 | 436 |
lemma even_diff_nat [simp]: |
437 |
"even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)" for m n :: nat |
|
58787 | 438 |
proof (cases "n \<le> m") |
439 |
case True |
|
440 |
then have "m - n + n * 2 = m + n" by (simp add: mult_2_right) |
|
66815 | 441 |
moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp |
442 |
ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:) |
|
58787 | 443 |
then show ?thesis by auto |
444 |
next |
|
445 |
case False |
|
446 |
then show ?thesis by simp |
|
63654 | 447 |
qed |
448 |
||
66815 | 449 |
lemma odd_pos: |
450 |
"odd n \<Longrightarrow> 0 < n" for n :: nat |
|
58690 | 451 |
by (auto elim: oddE) |
60343
063698416239
correct sort constraints for abbreviations in type classes
haftmann
parents:
59816
diff
changeset
|
452 |
|
66815 | 453 |
lemma Suc_double_not_eq_double: |
454 |
"Suc (2 * m) \<noteq> 2 * n" |
|
62597 | 455 |
proof |
456 |
assume "Suc (2 * m) = 2 * n" |
|
457 |
moreover have "odd (Suc (2 * m))" and "even (2 * n)" |
|
458 |
by simp_all |
|
459 |
ultimately show False by simp |
|
460 |
qed |
|
461 |
||
66815 | 462 |
lemma double_not_eq_Suc_double: |
463 |
"2 * m \<noteq> Suc (2 * n)" |
|
62597 | 464 |
using Suc_double_not_eq_double [of n m] by simp |
465 |
||
66815 | 466 |
lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n" |
467 |
by (auto elim: oddE) |
|
60343
063698416239
correct sort constraints for abbreviations in type classes
haftmann
parents:
59816
diff
changeset
|
468 |
|
66815 | 469 |
lemma even_Suc_div_two [simp]: |
470 |
"even n \<Longrightarrow> Suc n div 2 = n div 2" |
|
471 |
using even_succ_div_two [of n] by simp |
|
60343
063698416239
correct sort constraints for abbreviations in type classes
haftmann
parents:
59816
diff
changeset
|
472 |
|
66815 | 473 |
lemma odd_Suc_div_two [simp]: |
474 |
"odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)" |
|
475 |
using odd_succ_div_two [of n] by simp |
|
60343
063698416239
correct sort constraints for abbreviations in type classes
haftmann
parents:
59816
diff
changeset
|
476 |
|
66815 | 477 |
lemma odd_two_times_div_two_nat [simp]: |
478 |
assumes "odd n" |
|
479 |
shows "2 * (n div 2) = n - (1 :: nat)" |
|
480 |
proof - |
|
481 |
from assms have "2 * (n div 2) + 1 = n" |
|
482 |
by (rule odd_two_times_div_two_succ) |
|
483 |
then have "Suc (2 * (n div 2)) - 1 = n - 1" |
|
58787 | 484 |
by simp |
66815 | 485 |
then show ?thesis |
486 |
by simp |
|
58787 | 487 |
qed |
58680 | 488 |
|
66815 | 489 |
lemma parity_induct [case_names zero even odd]: |
490 |
assumes zero: "P 0" |
|
491 |
assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)" |
|
492 |
assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))" |
|
493 |
shows "P n" |
|
494 |
proof (induct n rule: less_induct) |
|
495 |
case (less n) |
|
496 |
show "P n" |
|
497 |
proof (cases "n = 0") |
|
498 |
case True with zero show ?thesis by simp |
|
499 |
next |
|
500 |
case False |
|
501 |
with less have hyp: "P (n div 2)" by simp |
|
502 |
show ?thesis |
|
503 |
proof (cases "even n") |
|
504 |
case True |
|
505 |
with hyp even [of "n div 2"] show ?thesis |
|
506 |
by simp |
|
507 |
next |
|
508 |
case False |
|
509 |
with hyp odd [of "n div 2"] show ?thesis |
|
510 |
by simp |
|
511 |
qed |
|
512 |
qed |
|
513 |
qed |
|
58687 | 514 |
|
515 |
||
60758 | 516 |
subsection \<open>Parity and powers\<close> |
58689 | 517 |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
518 |
context ring_1 |
58689 | 519 |
begin |
520 |
||
63654 | 521 |
lemma power_minus_even [simp]: "even n \<Longrightarrow> (- a) ^ n = a ^ n" |
58690 | 522 |
by (auto elim: evenE) |
58689 | 523 |
|
63654 | 524 |
lemma power_minus_odd [simp]: "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)" |
58690 | 525 |
by (auto elim: oddE) |
526 |
||
66815 | 527 |
lemma uminus_power_if: |
528 |
"(- a) ^ n = (if even n then a ^ n else - (a ^ n))" |
|
529 |
by auto |
|
530 |
||
63654 | 531 |
lemma neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1" |
58690 | 532 |
by simp |
58689 | 533 |
|
63654 | 534 |
lemma neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1" |
58690 | 535 |
by simp |
58689 | 536 |
|
66582 | 537 |
lemma neg_one_power_add_eq_neg_one_power_diff: "k \<le> n \<Longrightarrow> (- 1) ^ (n + k) = (- 1) ^ (n - k)" |
538 |
by (cases "even (n + k)") auto |
|
539 |
||
67371
2d9cf74943e1
moved in some material from Euler-MacLaurin
paulson <lp15@cam.ac.uk>
parents:
67083
diff
changeset
|
540 |
lemma minus_one_power_iff: "(- 1) ^ n = (if even n then 1 else - 1)" |
2d9cf74943e1
moved in some material from Euler-MacLaurin
paulson <lp15@cam.ac.uk>
parents:
67083
diff
changeset
|
541 |
by (induct n) auto |
2d9cf74943e1
moved in some material from Euler-MacLaurin
paulson <lp15@cam.ac.uk>
parents:
67083
diff
changeset
|
542 |
|
63654 | 543 |
end |
58689 | 544 |
|
545 |
context linordered_idom |
|
546 |
begin |
|
547 |
||
63654 | 548 |
lemma zero_le_even_power: "even n \<Longrightarrow> 0 \<le> a ^ n" |
58690 | 549 |
by (auto elim: evenE) |
58689 | 550 |
|
63654 | 551 |
lemma zero_le_odd_power: "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a" |
58689 | 552 |
by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE) |
553 |
||
63654 | 554 |
lemma zero_le_power_eq: "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a" |
58787 | 555 |
by (auto simp add: zero_le_even_power zero_le_odd_power) |
63654 | 556 |
|
557 |
lemma zero_less_power_eq: "0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a" |
|
58689 | 558 |
proof - |
559 |
have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0" |
|
58787 | 560 |
unfolding power_eq_0_iff [of a n, symmetric] by blast |
58689 | 561 |
show ?thesis |
63654 | 562 |
unfolding less_le zero_le_power_eq by auto |
58689 | 563 |
qed |
564 |
||
63654 | 565 |
lemma power_less_zero_eq [simp]: "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0" |
58689 | 566 |
unfolding not_le [symmetric] zero_le_power_eq by auto |
567 |
||
63654 | 568 |
lemma power_le_zero_eq: "a ^ n \<le> 0 \<longleftrightarrow> n > 0 \<and> (odd n \<and> a \<le> 0 \<or> even n \<and> a = 0)" |
569 |
unfolding not_less [symmetric] zero_less_power_eq by auto |
|
570 |
||
571 |
lemma power_even_abs: "even n \<Longrightarrow> \<bar>a\<bar> ^ n = a ^ n" |
|
58689 | 572 |
using power_abs [of a n] by (simp add: zero_le_even_power) |
573 |
||
574 |
lemma power_mono_even: |
|
575 |
assumes "even n" and "\<bar>a\<bar> \<le> \<bar>b\<bar>" |
|
576 |
shows "a ^ n \<le> b ^ n" |
|
577 |
proof - |
|
578 |
have "0 \<le> \<bar>a\<bar>" by auto |
|
63654 | 579 |
with \<open>\<bar>a\<bar> \<le> \<bar>b\<bar>\<close> have "\<bar>a\<bar> ^ n \<le> \<bar>b\<bar> ^ n" |
580 |
by (rule power_mono) |
|
581 |
with \<open>even n\<close> show ?thesis |
|
582 |
by (simp add: power_even_abs) |
|
58689 | 583 |
qed |
584 |
||
585 |
lemma power_mono_odd: |
|
586 |
assumes "odd n" and "a \<le> b" |
|
587 |
shows "a ^ n \<le> b ^ n" |
|
588 |
proof (cases "b < 0") |
|
63654 | 589 |
case True |
590 |
with \<open>a \<le> b\<close> have "- b \<le> - a" and "0 \<le> - b" by auto |
|
591 |
then have "(- b) ^ n \<le> (- a) ^ n" by (rule power_mono) |
|
60758 | 592 |
with \<open>odd n\<close> show ?thesis by simp |
58689 | 593 |
next |
63654 | 594 |
case False |
595 |
then have "0 \<le> b" by auto |
|
58689 | 596 |
show ?thesis |
597 |
proof (cases "a < 0") |
|
63654 | 598 |
case True |
599 |
then have "n \<noteq> 0" and "a \<le> 0" using \<open>odd n\<close> [THEN odd_pos] by auto |
|
60758 | 600 |
then have "a ^ n \<le> 0" unfolding power_le_zero_eq using \<open>odd n\<close> by auto |
63654 | 601 |
moreover from \<open>0 \<le> b\<close> have "0 \<le> b ^ n" by auto |
58689 | 602 |
ultimately show ?thesis by auto |
603 |
next |
|
63654 | 604 |
case False |
605 |
then have "0 \<le> a" by auto |
|
606 |
with \<open>a \<le> b\<close> show ?thesis |
|
607 |
using power_mono by auto |
|
58689 | 608 |
qed |
609 |
qed |
|
62083 | 610 |
|
60758 | 611 |
text \<open>Simplify, when the exponent is a numeral\<close> |
58689 | 612 |
|
613 |
lemma zero_le_power_eq_numeral [simp]: |
|
614 |
"0 \<le> a ^ numeral w \<longleftrightarrow> even (numeral w :: nat) \<or> odd (numeral w :: nat) \<and> 0 \<le> a" |
|
615 |
by (fact zero_le_power_eq) |
|
616 |
||
617 |
lemma zero_less_power_eq_numeral [simp]: |
|
63654 | 618 |
"0 < a ^ numeral w \<longleftrightarrow> |
619 |
numeral w = (0 :: nat) \<or> |
|
620 |
even (numeral w :: nat) \<and> a \<noteq> 0 \<or> |
|
621 |
odd (numeral w :: nat) \<and> 0 < a" |
|
58689 | 622 |
by (fact zero_less_power_eq) |
623 |
||
624 |
lemma power_le_zero_eq_numeral [simp]: |
|
63654 | 625 |
"a ^ numeral w \<le> 0 \<longleftrightarrow> |
626 |
(0 :: nat) < numeral w \<and> |
|
627 |
(odd (numeral w :: nat) \<and> a \<le> 0 \<or> even (numeral w :: nat) \<and> a = 0)" |
|
58689 | 628 |
by (fact power_le_zero_eq) |
629 |
||
630 |
lemma power_less_zero_eq_numeral [simp]: |
|
631 |
"a ^ numeral w < 0 \<longleftrightarrow> odd (numeral w :: nat) \<and> a < 0" |
|
632 |
by (fact power_less_zero_eq) |
|
633 |
||
634 |
lemma power_even_abs_numeral [simp]: |
|
635 |
"even (numeral w :: nat) \<Longrightarrow> \<bar>a\<bar> ^ numeral w = a ^ numeral w" |
|
636 |
by (fact power_even_abs) |
|
637 |
||
638 |
end |
|
639 |
||
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
640 |
|
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
641 |
subsection \<open>Instance for @{typ int}\<close> |
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
642 |
|
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
643 |
instance int :: ring_parity |
66839 | 644 |
by standard (simp_all add: dvd_eq_mod_eq_0 divide_int_def division_segment_int_def) |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
645 |
|
67816 | 646 |
lemma even_diff_iff: |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
647 |
"even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int |
67816 | 648 |
by (fact even_diff) |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
649 |
|
67816 | 650 |
lemma even_abs_add_iff: |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
651 |
"even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int |
67816 | 652 |
by simp |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
653 |
|
67816 | 654 |
lemma even_add_abs_iff: |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
655 |
"even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int |
67816 | 656 |
by simp |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
657 |
|
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
658 |
lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k" |
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
659 |
by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric]) |
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
660 |
|
67816 | 661 |
|
67828 | 662 |
subsection \<open>Abstract bit operations\<close> |
663 |
||
664 |
context semiring_parity |
|
67816 | 665 |
begin |
666 |
||
667 |
text \<open>The primary purpose of the following operations is |
|
668 |
to avoid ad-hoc simplification of concrete expressions @{term "2 ^ n"}\<close> |
|
669 |
||
670 |
definition bit_push :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" |
|
671 |
where bit_push_eq_mult: "bit_push n a = a * 2 ^ n" |
|
672 |
||
673 |
definition bit_take :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" |
|
674 |
where bit_take_eq_mod: "bit_take n a = a mod of_nat (2 ^ n)" |
|
675 |
||
676 |
definition bit_drop :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" |
|
677 |
where bit_drop_eq_div: "bit_drop n a = a div of_nat (2 ^ n)" |
|
678 |
||
679 |
lemma bit_ident: |
|
680 |
"bit_push n (bit_drop n a) + bit_take n a = a" |
|
681 |
using div_mult_mod_eq by (simp add: bit_push_eq_mult bit_take_eq_mod bit_drop_eq_div) |
|
682 |
||
683 |
lemma bit_take_bit_take [simp]: |
|
684 |
"bit_take n (bit_take n a) = bit_take n a" |
|
685 |
by (simp add: bit_take_eq_mod) |
|
686 |
||
687 |
lemma bit_take_0 [simp]: |
|
688 |
"bit_take 0 a = 0" |
|
689 |
by (simp add: bit_take_eq_mod) |
|
690 |
||
691 |
lemma bit_take_Suc [simp]: |
|
692 |
"bit_take (Suc n) a = bit_take n (a div 2) * 2 + of_bool (odd a)" |
|
693 |
proof - |
|
694 |
have "1 + 2 * (a div 2) mod (2 * 2 ^ n) = (a div 2 * 2 + a mod 2) mod (2 * 2 ^ n)" |
|
695 |
if "odd a" |
|
696 |
using that mod_mult2_eq' [of "1 + 2 * (a div 2)" 2 "2 ^ n"] |
|
697 |
by (simp add: ac_simps odd_iff_mod_2_eq_one mult_mod_right) |
|
698 |
also have "\<dots> = a mod (2 * 2 ^ n)" |
|
699 |
by (simp only: div_mult_mod_eq) |
|
700 |
finally show ?thesis |
|
701 |
by (simp add: bit_take_eq_mod algebra_simps mult_mod_right) |
|
702 |
qed |
|
703 |
||
704 |
lemma bit_take_of_0 [simp]: |
|
705 |
"bit_take n 0 = 0" |
|
706 |
by (simp add: bit_take_eq_mod) |
|
707 |
||
708 |
lemma bit_take_plus: |
|
709 |
"bit_take n (bit_take n a + bit_take n b) = bit_take n (a + b)" |
|
710 |
by (simp add: bit_take_eq_mod mod_simps) |
|
711 |
||
712 |
lemma bit_take_of_1_eq_0_iff [simp]: |
|
713 |
"bit_take n 1 = 0 \<longleftrightarrow> n = 0" |
|
714 |
by (simp add: bit_take_eq_mod) |
|
715 |
||
716 |
lemma bit_push_eq_0_iff [simp]: |
|
717 |
"bit_push n a = 0 \<longleftrightarrow> a = 0" |
|
718 |
by (simp add: bit_push_eq_mult) |
|
719 |
||
720 |
lemma bit_drop_0 [simp]: |
|
721 |
"bit_drop 0 = id" |
|
722 |
by (simp add: fun_eq_iff bit_drop_eq_div) |
|
723 |
||
724 |
lemma bit_drop_of_0 [simp]: |
|
725 |
"bit_drop n 0 = 0" |
|
726 |
by (simp add: bit_drop_eq_div) |
|
727 |
||
728 |
lemma bit_drop_Suc [simp]: |
|
729 |
"bit_drop (Suc n) a = bit_drop n (a div 2)" |
|
730 |
proof (cases "even a") |
|
731 |
case True |
|
732 |
then obtain b where "a = 2 * b" .. |
|
733 |
moreover have "bit_drop (Suc n) (2 * b) = bit_drop n b" |
|
734 |
by (simp add: bit_drop_eq_div) |
|
735 |
ultimately show ?thesis |
|
736 |
by simp |
|
737 |
next |
|
738 |
case False |
|
739 |
then obtain b where "a = 2 * b + 1" .. |
|
740 |
moreover have "bit_drop (Suc n) (2 * b + 1) = bit_drop n b" |
|
741 |
using div_mult2_eq' [of "1 + b * 2" 2 "2 ^ n"] |
|
742 |
by (auto simp add: bit_drop_eq_div ac_simps) |
|
743 |
ultimately show ?thesis |
|
744 |
by simp |
|
745 |
qed |
|
746 |
||
747 |
lemma bit_drop_half: |
|
748 |
"bit_drop n (a div 2) = bit_drop n a div 2" |
|
749 |
by (induction n arbitrary: a) simp_all |
|
750 |
||
751 |
lemma bit_drop_of_bool [simp]: |
|
752 |
"bit_drop n (of_bool d) = of_bool (n = 0 \<and> d)" |
|
753 |
by (cases n) simp_all |
|
754 |
||
755 |
lemma even_bit_take_eq [simp]: |
|
756 |
"even (bit_take n a) \<longleftrightarrow> n = 0 \<or> even a" |
|
757 |
by (cases n) (simp_all add: bit_take_eq_mod dvd_mod_iff) |
|
758 |
||
759 |
lemma bit_push_0_id [simp]: |
|
760 |
"bit_push 0 = id" |
|
761 |
by (simp add: fun_eq_iff bit_push_eq_mult) |
|
762 |
||
763 |
lemma bit_push_of_0 [simp]: |
|
764 |
"bit_push n 0 = 0" |
|
765 |
by (simp add: bit_push_eq_mult) |
|
766 |
||
767 |
lemma bit_push_of_1: |
|
768 |
"bit_push n 1 = 2 ^ n" |
|
769 |
by (simp add: bit_push_eq_mult) |
|
770 |
||
771 |
lemma bit_push_Suc [simp]: |
|
772 |
"bit_push (Suc n) a = bit_push n (a * 2)" |
|
773 |
by (simp add: bit_push_eq_mult ac_simps) |
|
774 |
||
775 |
lemma bit_push_double: |
|
776 |
"bit_push n (a * 2) = bit_push n a * 2" |
|
777 |
by (simp add: bit_push_eq_mult ac_simps) |
|
778 |
||
779 |
lemma bit_drop_bit_take [simp]: |
|
780 |
"bit_drop n (bit_take n a) = 0" |
|
781 |
by (simp add: bit_drop_eq_div bit_take_eq_mod) |
|
782 |
||
783 |
lemma bit_take_bit_drop_commute: |
|
784 |
"bit_drop m (bit_take n a) = bit_take (n - m) (bit_drop m a)" |
|
785 |
for m n :: nat |
|
786 |
proof (cases "n \<ge> m") |
|
787 |
case True |
|
788 |
moreover define q where "q = n - m" |
|
789 |
ultimately have "n - m = q" and "n = m + q" |
|
790 |
by simp_all |
|
791 |
moreover have "bit_drop m (bit_take (m + q) a) = bit_take q (bit_drop m a)" |
|
792 |
using mod_mult2_eq' [of a "2 ^ m" "2 ^ q"] |
|
793 |
by (simp add: bit_drop_eq_div bit_take_eq_mod power_add) |
|
794 |
ultimately show ?thesis |
|
795 |
by simp |
|
796 |
next |
|
797 |
case False |
|
798 |
moreover define q where "q = m - n" |
|
799 |
ultimately have "m - n = q" and "m = n + q" |
|
800 |
by simp_all |
|
801 |
moreover have "bit_drop (n + q) (bit_take n a) = 0" |
|
802 |
using div_mult2_eq' [of "a mod 2 ^ n" "2 ^ n" "2 ^ q"] |
|
803 |
by (simp add: bit_drop_eq_div bit_take_eq_mod power_add div_mult2_eq) |
|
804 |
ultimately show ?thesis |
|
805 |
by simp |
|
806 |
qed |
|
807 |
||
58770 | 808 |
end |
67816 | 809 |
|
810 |
end |