author | haftmann |
Tue, 24 Jan 2023 10:30:56 +0000 | |
changeset 77061 | 5de3772609ea |
parent 76387 | 8cb141384682 |
child 78082 | a51d2e96203e |
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 |
|
77061
5de3772609ea
generalized theory name: euclidean division denotes one particular division definition on integers
haftmann
parents:
76387
diff
changeset
|
9 |
imports Euclidean_Rings |
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 |
|
70341
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
14 |
class semiring_parity = comm_semiring_1 + semiring_modulo + |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
15 |
assumes even_iff_mod_2_eq_zero: "2 dvd a \<longleftrightarrow> a mod 2 = 0" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
16 |
and odd_iff_mod_2_eq_one: "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
17 |
and odd_one [simp]: "\<not> 2 dvd 1" |
66839 | 18 |
begin |
19 |
||
58740 | 20 |
abbreviation even :: "'a \<Rightarrow> bool" |
63654 | 21 |
where "even a \<equiv> 2 dvd a" |
54228 | 22 |
|
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
23 |
abbreviation odd :: "'a \<Rightarrow> bool" |
63654 | 24 |
where "odd a \<equiv> \<not> 2 dvd a" |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
25 |
|
76387 | 26 |
end |
27 |
||
28 |
class ring_parity = ring + semiring_parity |
|
29 |
begin |
|
30 |
||
31 |
subclass comm_ring_1 .. |
|
32 |
||
33 |
end |
|
34 |
||
35 |
instance nat :: semiring_parity |
|
36 |
by standard (simp_all add: dvd_eq_mod_eq_0) |
|
37 |
||
38 |
instance int :: ring_parity |
|
39 |
by standard (auto simp add: dvd_eq_mod_eq_0) |
|
40 |
||
41 |
context semiring_parity |
|
42 |
begin |
|
43 |
||
66815 | 44 |
lemma parity_cases [case_names even odd]: |
45 |
assumes "even a \<Longrightarrow> a mod 2 = 0 \<Longrightarrow> P" |
|
46 |
assumes "odd a \<Longrightarrow> a mod 2 = 1 \<Longrightarrow> P" |
|
47 |
shows P |
|
70341
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
48 |
using assms by (cases "even a") |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
49 |
(simp_all add: even_iff_mod_2_eq_zero [symmetric] odd_iff_mod_2_eq_one [symmetric]) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
50 |
|
71181 | 51 |
lemma odd_of_bool_self [simp]: |
52 |
\<open>odd (of_bool p) \<longleftrightarrow> p\<close> |
|
53 |
by (cases p) simp_all |
|
54 |
||
70341
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
55 |
lemma not_mod_2_eq_0_eq_1 [simp]: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
56 |
"a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
57 |
by (cases a rule: parity_cases) simp_all |
66815 | 58 |
|
59 |
lemma not_mod_2_eq_1_eq_0 [simp]: |
|
60 |
"a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0" |
|
61 |
by (cases a rule: parity_cases) simp_all |
|
62 |
||
58690 | 63 |
lemma evenE [elim?]: |
64 |
assumes "even a" |
|
65 |
obtains b where "a = 2 * b" |
|
58740 | 66 |
using assms by (rule dvdE) |
58690 | 67 |
|
58681 | 68 |
lemma oddE [elim?]: |
58680 | 69 |
assumes "odd a" |
70 |
obtains b where "a = 2 * b + 1" |
|
58787 | 71 |
proof - |
66815 | 72 |
have "a = 2 * (a div 2) + a mod 2" |
73 |
by (simp add: mult_div_mod_eq) |
|
74 |
with assms have "a = 2 * (a div 2) + 1" |
|
75 |
by (simp add: odd_iff_mod_2_eq_one) |
|
76 |
then show ?thesis .. |
|
77 |
qed |
|
78 |
||
79 |
lemma mod_2_eq_odd: |
|
80 |
"a mod 2 = of_bool (odd a)" |
|
70341
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
81 |
by (auto elim: oddE simp add: even_iff_mod_2_eq_zero) |
66815 | 82 |
|
67816 | 83 |
lemma of_bool_odd_eq_mod_2: |
84 |
"of_bool (odd a) = a mod 2" |
|
85 |
by (simp add: mod_2_eq_odd) |
|
86 |
||
71426 | 87 |
lemma even_mod_2_iff [simp]: |
88 |
\<open>even (a mod 2) \<longleftrightarrow> even a\<close> |
|
89 |
by (simp add: mod_2_eq_odd) |
|
90 |
||
91 |
lemma mod2_eq_if: |
|
92 |
"a mod 2 = (if even a then 0 else 1)" |
|
93 |
by (simp add: mod_2_eq_odd) |
|
94 |
||
66815 | 95 |
lemma even_zero [simp]: |
96 |
"even 0" |
|
97 |
by (fact dvd_0_right) |
|
98 |
||
99 |
lemma odd_even_add: |
|
100 |
"even (a + b)" if "odd a" and "odd b" |
|
101 |
proof - |
|
102 |
from that obtain c d where "a = 2 * c + 1" and "b = 2 * d + 1" |
|
103 |
by (blast elim: oddE) |
|
104 |
then have "a + b = 2 * c + 2 * d + (1 + 1)" |
|
105 |
by (simp only: ac_simps) |
|
106 |
also have "\<dots> = 2 * (c + d + 1)" |
|
107 |
by (simp add: algebra_simps) |
|
108 |
finally show ?thesis .. |
|
109 |
qed |
|
110 |
||
111 |
lemma even_add [simp]: |
|
112 |
"even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)" |
|
113 |
by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add) |
|
114 |
||
115 |
lemma odd_add [simp]: |
|
116 |
"odd (a + b) \<longleftrightarrow> \<not> (odd a \<longleftrightarrow> odd b)" |
|
117 |
by simp |
|
118 |
||
119 |
lemma even_plus_one_iff [simp]: |
|
120 |
"even (a + 1) \<longleftrightarrow> odd a" |
|
121 |
by (auto simp add: dvd_add_right_iff intro: odd_even_add) |
|
122 |
||
123 |
lemma even_mult_iff [simp]: |
|
124 |
"even (a * b) \<longleftrightarrow> even a \<or> even b" (is "?P \<longleftrightarrow> ?Q") |
|
125 |
proof |
|
126 |
assume ?Q |
|
127 |
then show ?P |
|
128 |
by auto |
|
129 |
next |
|
130 |
assume ?P |
|
131 |
show ?Q |
|
132 |
proof (rule ccontr) |
|
133 |
assume "\<not> (even a \<or> even b)" |
|
134 |
then have "odd a" and "odd b" |
|
135 |
by auto |
|
136 |
then obtain r s where "a = 2 * r + 1" and "b = 2 * s + 1" |
|
137 |
by (blast elim: oddE) |
|
138 |
then have "a * b = (2 * r + 1) * (2 * s + 1)" |
|
139 |
by simp |
|
140 |
also have "\<dots> = 2 * (2 * r * s + r + s) + 1" |
|
141 |
by (simp add: algebra_simps) |
|
142 |
finally have "odd (a * b)" |
|
143 |
by simp |
|
144 |
with \<open>?P\<close> show False |
|
145 |
by auto |
|
146 |
qed |
|
147 |
qed |
|
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
148 |
|
63654 | 149 |
lemma even_numeral [simp]: "even (numeral (Num.Bit0 n))" |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
150 |
proof - |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
151 |
have "even (2 * numeral n)" |
66815 | 152 |
unfolding even_mult_iff by simp |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
153 |
then have "even (numeral n + numeral n)" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
154 |
unfolding mult_2 . |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
155 |
then show ?thesis |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
156 |
unfolding numeral.simps . |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
157 |
qed |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
158 |
|
63654 | 159 |
lemma odd_numeral [simp]: "odd (numeral (Num.Bit1 n))" |
58678
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
160 |
proof |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
161 |
assume "even (numeral (num.Bit1 n))" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
162 |
then have "even (numeral n + numeral n + 1)" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
163 |
unfolding numeral.simps . |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
164 |
then have "even (2 * numeral n + 1)" |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
165 |
unfolding mult_2 . |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
166 |
then have "2 dvd numeral n * 2 + 1" |
58740 | 167 |
by (simp add: ac_simps) |
63654 | 168 |
then have "2 dvd 1" |
169 |
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
|
170 |
then show False by simp |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
171 |
qed |
398e05aa84d4
purely algebraic characterization of even and odd
haftmann
parents:
58645
diff
changeset
|
172 |
|
71755 | 173 |
lemma odd_numeral_BitM [simp]: |
174 |
\<open>odd (numeral (Num.BitM w))\<close> |
|
175 |
by (cases w) simp_all |
|
176 |
||
63654 | 177 |
lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0" |
58680 | 178 |
by (induct n) auto |
179 |
||
76387 | 180 |
lemma even_prod_iff: |
181 |
\<open>even (prod f A) \<longleftrightarrow> (\<exists>a\<in>A. even (f a))\<close> if \<open>finite A\<close> |
|
182 |
using that by (induction A) simp_all |
|
183 |
||
71412 | 184 |
lemma mask_eq_sum_exp: |
185 |
\<open>2 ^ n - 1 = (\<Sum>m\<in>{q. q < n}. 2 ^ m)\<close> |
|
186 |
proof - |
|
187 |
have *: \<open>{q. q < Suc m} = insert m {q. q < m}\<close> for m |
|
188 |
by auto |
|
189 |
have \<open>2 ^ n = (\<Sum>m\<in>{q. q < n}. 2 ^ m) + 1\<close> |
|
190 |
by (induction n) (simp_all add: ac_simps mult_2 *) |
|
191 |
then have \<open>2 ^ n - 1 = (\<Sum>m\<in>{q. q < n}. 2 ^ m) + 1 - 1\<close> |
|
192 |
by simp |
|
193 |
then show ?thesis |
|
194 |
by simp |
|
195 |
qed |
|
196 |
||
76387 | 197 |
lemma (in -) mask_eq_sum_exp_nat: |
198 |
\<open>2 ^ n - Suc 0 = (\<Sum>m\<in>{q. q < n}. 2 ^ m)\<close> |
|
199 |
using mask_eq_sum_exp [where ?'a = nat] by simp |
|
200 |
||
70341
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
201 |
end |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
202 |
|
76387 | 203 |
context ring_parity |
70341
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
204 |
begin |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
205 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
206 |
lemma even_minus: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
207 |
"even (- a) \<longleftrightarrow> even a" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
208 |
by (fact dvd_minus_iff) |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
209 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
210 |
lemma even_diff [simp]: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
211 |
"even (a - b) \<longleftrightarrow> even (a + b)" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
212 |
using even_add [of a "- b"] by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
213 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
214 |
end |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
215 |
|
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
216 |
|
69593 | 217 |
subsection \<open>Instance for \<^typ>\<open>nat\<close>\<close> |
66808
1907167b6038
elementary definition of division on natural numbers
haftmann
parents:
66582
diff
changeset
|
218 |
|
66815 | 219 |
lemma even_Suc_Suc_iff [simp]: |
220 |
"even (Suc (Suc n)) \<longleftrightarrow> even n" |
|
58787 | 221 |
using dvd_add_triv_right_iff [of 2 n] by simp |
58687 | 222 |
|
66815 | 223 |
lemma even_Suc [simp]: "even (Suc n) \<longleftrightarrow> odd n" |
224 |
using even_plus_one_iff [of n] by simp |
|
58787 | 225 |
|
66815 | 226 |
lemma even_diff_nat [simp]: |
227 |
"even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)" for m n :: nat |
|
58787 | 228 |
proof (cases "n \<le> m") |
229 |
case True |
|
230 |
then have "m - n + n * 2 = m + n" by (simp add: mult_2_right) |
|
66815 | 231 |
moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp |
232 |
ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:) |
|
58787 | 233 |
then show ?thesis by auto |
234 |
next |
|
235 |
case False |
|
236 |
then show ?thesis by simp |
|
63654 | 237 |
qed |
238 |
||
66815 | 239 |
lemma odd_pos: |
240 |
"odd n \<Longrightarrow> 0 < n" for n :: nat |
|
58690 | 241 |
by (auto elim: oddE) |
60343
063698416239
correct sort constraints for abbreviations in type classes
haftmann
parents:
59816
diff
changeset
|
242 |
|
66815 | 243 |
lemma Suc_double_not_eq_double: |
244 |
"Suc (2 * m) \<noteq> 2 * n" |
|
62597 | 245 |
proof |
246 |
assume "Suc (2 * m) = 2 * n" |
|
247 |
moreover have "odd (Suc (2 * m))" and "even (2 * n)" |
|
248 |
by simp_all |
|
249 |
ultimately show False by simp |
|
250 |
qed |
|
251 |
||
66815 | 252 |
lemma double_not_eq_Suc_double: |
253 |
"2 * m \<noteq> Suc (2 * n)" |
|
62597 | 254 |
using Suc_double_not_eq_double [of n m] by simp |
255 |
||
66815 | 256 |
lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n" |
257 |
by (auto elim: oddE) |
|
60343
063698416239
correct sort constraints for abbreviations in type classes
haftmann
parents:
59816
diff
changeset
|
258 |
|
66815 | 259 |
lemma even_Suc_div_two [simp]: |
260 |
"even n \<Longrightarrow> Suc n div 2 = n div 2" |
|
76387 | 261 |
by auto |
60343
063698416239
correct sort constraints for abbreviations in type classes
haftmann
parents:
59816
diff
changeset
|
262 |
|
66815 | 263 |
lemma odd_Suc_div_two [simp]: |
264 |
"odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)" |
|
76387 | 265 |
by (auto elim: oddE) |
60343
063698416239
correct sort constraints for abbreviations in type classes
haftmann
parents:
59816
diff
changeset
|
266 |
|
66815 | 267 |
lemma odd_two_times_div_two_nat [simp]: |
268 |
assumes "odd n" |
|
269 |
shows "2 * (n div 2) = n - (1 :: nat)" |
|
270 |
proof - |
|
271 |
from assms have "2 * (n div 2) + 1 = n" |
|
76387 | 272 |
by (auto elim: oddE) |
66815 | 273 |
then have "Suc (2 * (n div 2)) - 1 = n - 1" |
58787 | 274 |
by simp |
66815 | 275 |
then show ?thesis |
276 |
by simp |
|
58787 | 277 |
qed |
58680 | 278 |
|
70341
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
279 |
lemma not_mod2_eq_Suc_0_eq_0 [simp]: |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
280 |
"n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0" |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
281 |
using not_mod_2_eq_1_eq_0 [of n] by simp |
972c0c744e7c
generalized type classes for parity to cover word types also, which contain zero divisors
haftmann
parents:
70340
diff
changeset
|
282 |
|
69502 | 283 |
lemma odd_card_imp_not_empty: |
284 |
\<open>A \<noteq> {}\<close> if \<open>odd (card A)\<close> |
|
285 |
using that by auto |
|
286 |
||
70365
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
287 |
lemma nat_induct2 [case_names 0 1 step]: |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
288 |
assumes "P 0" "P 1" and step: "\<And>n::nat. P n \<Longrightarrow> P (n + 2)" |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
289 |
shows "P n" |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
290 |
proof (induct n rule: less_induct) |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
291 |
case (less n) |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
292 |
show ?case |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
293 |
proof (cases "n < Suc (Suc 0)") |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
294 |
case True |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
295 |
then show ?thesis |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
296 |
using assms by (auto simp: less_Suc_eq) |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
297 |
next |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
298 |
case False |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
299 |
then obtain k where k: "n = Suc (Suc k)" |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
300 |
by (force simp: not_less nat_le_iff_add) |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
301 |
then have "k<n" |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
302 |
by simp |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
303 |
with less assms have "P (k+2)" |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
304 |
by blast |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
305 |
then show ?thesis |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
306 |
by (simp add: k) |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
307 |
qed |
4df0628e8545
a few new lemmas and a bit of tidying
paulson <lp15@cam.ac.uk>
parents:
70353
diff
changeset
|
308 |
qed |
58687 | 309 |
|
71412 | 310 |
context semiring_parity |
311 |
begin |
|
312 |
||
313 |
lemma even_sum_iff: |
|
314 |
\<open>even (sum f A) \<longleftrightarrow> even (card {a\<in>A. odd (f a)})\<close> if \<open>finite A\<close> |
|
315 |
using that proof (induction A) |
|
316 |
case empty |
|
317 |
then show ?case |
|
318 |
by simp |
|
319 |
next |
|
320 |
case (insert a A) |
|
321 |
moreover have \<open>{b \<in> insert a A. odd (f b)} = (if odd (f a) then {a} else {}) \<union> {b \<in> A. odd (f b)}\<close> |
|
322 |
by auto |
|
323 |
ultimately show ?case |
|
324 |
by simp |
|
325 |
qed |
|
326 |
||
327 |
lemma even_mask_iff [simp]: |
|
328 |
\<open>even (2 ^ n - 1) \<longleftrightarrow> n = 0\<close> |
|
329 |
proof (cases \<open>n = 0\<close>) |
|
330 |
case True |
|
331 |
then show ?thesis |
|
332 |
by simp |
|
333 |
next |
|
334 |
case False |
|
335 |
then have \<open>{a. a = 0 \<and> a < n} = {0}\<close> |
|
336 |
by auto |
|
337 |
then show ?thesis |
|
338 |
by (auto simp add: mask_eq_sum_exp even_sum_iff) |
|
339 |
qed |
|
340 |
||
76387 | 341 |
lemma even_of_nat_iff [simp]: |
342 |
"even (of_nat n) \<longleftrightarrow> even n" |
|
343 |
by (induction n) simp_all |
|
344 |
||
71412 | 345 |
end |
346 |
||
71138 | 347 |
|
60758 | 348 |
subsection \<open>Parity and powers\<close> |
58689 | 349 |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
350 |
context ring_1 |
58689 | 351 |
begin |
352 |
||
63654 | 353 |
lemma power_minus_even [simp]: "even n \<Longrightarrow> (- a) ^ n = a ^ n" |
58690 | 354 |
by (auto elim: evenE) |
58689 | 355 |
|
63654 | 356 |
lemma power_minus_odd [simp]: "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)" |
58690 | 357 |
by (auto elim: oddE) |
358 |
||
66815 | 359 |
lemma uminus_power_if: |
360 |
"(- a) ^ n = (if even n then a ^ n else - (a ^ n))" |
|
361 |
by auto |
|
362 |
||
63654 | 363 |
lemma neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1" |
58690 | 364 |
by simp |
58689 | 365 |
|
63654 | 366 |
lemma neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1" |
58690 | 367 |
by simp |
58689 | 368 |
|
66582 | 369 |
lemma neg_one_power_add_eq_neg_one_power_diff: "k \<le> n \<Longrightarrow> (- 1) ^ (n + k) = (- 1) ^ (n - k)" |
370 |
by (cases "even (n + k)") auto |
|
371 |
||
67371
2d9cf74943e1
moved in some material from Euler-MacLaurin
paulson <lp15@cam.ac.uk>
parents:
67083
diff
changeset
|
372 |
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
|
373 |
by (induct n) auto |
2d9cf74943e1
moved in some material from Euler-MacLaurin
paulson <lp15@cam.ac.uk>
parents:
67083
diff
changeset
|
374 |
|
63654 | 375 |
end |
58689 | 376 |
|
377 |
context linordered_idom |
|
378 |
begin |
|
379 |
||
63654 | 380 |
lemma zero_le_even_power: "even n \<Longrightarrow> 0 \<le> a ^ n" |
58690 | 381 |
by (auto elim: evenE) |
58689 | 382 |
|
63654 | 383 |
lemma zero_le_odd_power: "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a" |
58689 | 384 |
by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE) |
385 |
||
63654 | 386 |
lemma zero_le_power_eq: "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a" |
58787 | 387 |
by (auto simp add: zero_le_even_power zero_le_odd_power) |
63654 | 388 |
|
389 |
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 | 390 |
proof - |
391 |
have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0" |
|
58787 | 392 |
unfolding power_eq_0_iff [of a n, symmetric] by blast |
58689 | 393 |
show ?thesis |
63654 | 394 |
unfolding less_le zero_le_power_eq by auto |
58689 | 395 |
qed |
396 |
||
63654 | 397 |
lemma power_less_zero_eq [simp]: "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0" |
58689 | 398 |
unfolding not_le [symmetric] zero_le_power_eq by auto |
399 |
||
63654 | 400 |
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)" |
401 |
unfolding not_less [symmetric] zero_less_power_eq by auto |
|
402 |
||
403 |
lemma power_even_abs: "even n \<Longrightarrow> \<bar>a\<bar> ^ n = a ^ n" |
|
58689 | 404 |
using power_abs [of a n] by (simp add: zero_le_even_power) |
405 |
||
406 |
lemma power_mono_even: |
|
407 |
assumes "even n" and "\<bar>a\<bar> \<le> \<bar>b\<bar>" |
|
408 |
shows "a ^ n \<le> b ^ n" |
|
409 |
proof - |
|
410 |
have "0 \<le> \<bar>a\<bar>" by auto |
|
63654 | 411 |
with \<open>\<bar>a\<bar> \<le> \<bar>b\<bar>\<close> have "\<bar>a\<bar> ^ n \<le> \<bar>b\<bar> ^ n" |
412 |
by (rule power_mono) |
|
413 |
with \<open>even n\<close> show ?thesis |
|
414 |
by (simp add: power_even_abs) |
|
58689 | 415 |
qed |
416 |
||
417 |
lemma power_mono_odd: |
|
418 |
assumes "odd n" and "a \<le> b" |
|
419 |
shows "a ^ n \<le> b ^ n" |
|
420 |
proof (cases "b < 0") |
|
63654 | 421 |
case True |
422 |
with \<open>a \<le> b\<close> have "- b \<le> - a" and "0 \<le> - b" by auto |
|
423 |
then have "(- b) ^ n \<le> (- a) ^ n" by (rule power_mono) |
|
60758 | 424 |
with \<open>odd n\<close> show ?thesis by simp |
58689 | 425 |
next |
63654 | 426 |
case False |
427 |
then have "0 \<le> b" by auto |
|
58689 | 428 |
show ?thesis |
429 |
proof (cases "a < 0") |
|
63654 | 430 |
case True |
431 |
then have "n \<noteq> 0" and "a \<le> 0" using \<open>odd n\<close> [THEN odd_pos] by auto |
|
60758 | 432 |
then have "a ^ n \<le> 0" unfolding power_le_zero_eq using \<open>odd n\<close> by auto |
63654 | 433 |
moreover from \<open>0 \<le> b\<close> have "0 \<le> b ^ n" by auto |
58689 | 434 |
ultimately show ?thesis by auto |
435 |
next |
|
63654 | 436 |
case False |
437 |
then have "0 \<le> a" by auto |
|
438 |
with \<open>a \<le> b\<close> show ?thesis |
|
439 |
using power_mono by auto |
|
58689 | 440 |
qed |
441 |
qed |
|
62083 | 442 |
|
60758 | 443 |
text \<open>Simplify, when the exponent is a numeral\<close> |
58689 | 444 |
|
445 |
lemma zero_le_power_eq_numeral [simp]: |
|
446 |
"0 \<le> a ^ numeral w \<longleftrightarrow> even (numeral w :: nat) \<or> odd (numeral w :: nat) \<and> 0 \<le> a" |
|
447 |
by (fact zero_le_power_eq) |
|
448 |
||
449 |
lemma zero_less_power_eq_numeral [simp]: |
|
63654 | 450 |
"0 < a ^ numeral w \<longleftrightarrow> |
451 |
numeral w = (0 :: nat) \<or> |
|
452 |
even (numeral w :: nat) \<and> a \<noteq> 0 \<or> |
|
453 |
odd (numeral w :: nat) \<and> 0 < a" |
|
58689 | 454 |
by (fact zero_less_power_eq) |
455 |
||
456 |
lemma power_le_zero_eq_numeral [simp]: |
|
63654 | 457 |
"a ^ numeral w \<le> 0 \<longleftrightarrow> |
458 |
(0 :: nat) < numeral w \<and> |
|
459 |
(odd (numeral w :: nat) \<and> a \<le> 0 \<or> even (numeral w :: nat) \<and> a = 0)" |
|
58689 | 460 |
by (fact power_le_zero_eq) |
461 |
||
462 |
lemma power_less_zero_eq_numeral [simp]: |
|
463 |
"a ^ numeral w < 0 \<longleftrightarrow> odd (numeral w :: nat) \<and> a < 0" |
|
464 |
by (fact power_less_zero_eq) |
|
465 |
||
466 |
lemma power_even_abs_numeral [simp]: |
|
467 |
"even (numeral w :: nat) \<Longrightarrow> \<bar>a\<bar> ^ numeral w = a ^ numeral w" |
|
468 |
by (fact power_even_abs) |
|
469 |
||
470 |
end |
|
471 |
||
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
472 |
|
69593 | 473 |
subsection \<open>Instance for \<^typ>\<open>int\<close>\<close> |
76387 | 474 |
|
67816 | 475 |
lemma even_diff_iff: |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
476 |
"even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int |
67816 | 477 |
by (fact even_diff) |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
478 |
|
67816 | 479 |
lemma even_abs_add_iff: |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
480 |
"even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int |
67816 | 481 |
by simp |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
482 |
|
67816 | 483 |
lemma even_add_abs_iff: |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
484 |
"even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int |
67816 | 485 |
by simp |
66816
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
486 |
|
212a3334e7da
more fundamental definition of div and mod on int
haftmann
parents:
66815
diff
changeset
|
487 |
lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k" |
74592 | 488 |
by (simp add: even_of_nat_iff [of "nat k", where ?'a = int, symmetric]) |
71138 | 489 |
|
71837
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
490 |
context |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
491 |
assumes "SORT_CONSTRAINT('a::division_ring)" |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
492 |
begin |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
493 |
|
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
494 |
lemma power_int_minus_left: |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
495 |
"power_int (-a :: 'a) n = (if even n then power_int a n else -power_int a n)" |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
496 |
by (auto simp: power_int_def minus_one_power_iff even_nat_iff) |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
497 |
|
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
498 |
lemma power_int_minus_left_even [simp]: "even n \<Longrightarrow> power_int (-a :: 'a) n = power_int a n" |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
499 |
by (simp add: power_int_minus_left) |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
500 |
|
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
501 |
lemma power_int_minus_left_odd [simp]: "odd n \<Longrightarrow> power_int (-a :: 'a) n = -power_int a n" |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
502 |
by (simp add: power_int_minus_left) |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
503 |
|
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
504 |
lemma power_int_minus_left_distrib: |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
505 |
"NO_MATCH (-1) x \<Longrightarrow> power_int (-a :: 'a) n = power_int (-1) n * power_int a n" |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
506 |
by (simp add: power_int_minus_left) |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
507 |
|
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
508 |
lemma power_int_minus_one_minus: "power_int (-1 :: 'a) (-n) = power_int (-1) n" |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
509 |
by (simp add: power_int_minus_left) |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
510 |
|
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
511 |
lemma power_int_minus_one_diff_commute: "power_int (-1 :: 'a) (a - b) = power_int (-1) (b - a)" |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
512 |
by (subst power_int_minus_one_minus [symmetric]) auto |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
513 |
|
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
514 |
lemma power_int_minus_one_mult_self [simp]: |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
515 |
"power_int (-1 :: 'a) m * power_int (-1) m = 1" |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
516 |
by (simp add: power_int_minus_left) |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
517 |
|
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
518 |
lemma power_int_minus_one_mult_self' [simp]: |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
519 |
"power_int (-1 :: 'a) m * (power_int (-1) m * b) = b" |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
520 |
by (simp add: power_int_minus_left) |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
521 |
|
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
522 |
end |
dca11678c495
new constant power_int in HOL
Manuel Eberl <eberlm@in.tum.de>
parents:
71822
diff
changeset
|
523 |
|
75937 | 524 |
|
76387 | 525 |
subsection \<open>Special case: euclidean rings containing the natural numbers\<close> |
526 |
||
527 |
class unique_euclidean_semiring_with_nat = semidom + semiring_char_0 + unique_euclidean_semiring + |
|
528 |
assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n" |
|
529 |
and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1" |
|
530 |
and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a" |
|
531 |
begin |
|
532 |
||
533 |
lemma division_segment_eq_iff: |
|
534 |
"a = b" if "division_segment a = division_segment b" |
|
535 |
and "euclidean_size a = euclidean_size b" |
|
536 |
using that division_segment_euclidean_size [of a] by simp |
|
537 |
||
538 |
lemma euclidean_size_of_nat [simp]: |
|
539 |
"euclidean_size (of_nat n) = n" |
|
540 |
proof - |
|
541 |
have "division_segment (of_nat n) * of_nat (euclidean_size (of_nat n)) = of_nat n" |
|
542 |
by (fact division_segment_euclidean_size) |
|
543 |
then show ?thesis by simp |
|
544 |
qed |
|
545 |
||
546 |
lemma of_nat_euclidean_size: |
|
547 |
"of_nat (euclidean_size a) = a div division_segment a" |
|
548 |
proof - |
|
549 |
have "of_nat (euclidean_size a) = division_segment a * of_nat (euclidean_size a) div division_segment a" |
|
550 |
by (subst nonzero_mult_div_cancel_left) simp_all |
|
551 |
also have "\<dots> = a div division_segment a" |
|
552 |
by simp |
|
553 |
finally show ?thesis . |
|
554 |
qed |
|
555 |
||
556 |
lemma division_segment_1 [simp]: |
|
557 |
"division_segment 1 = 1" |
|
558 |
using division_segment_of_nat [of 1] by simp |
|
559 |
||
560 |
lemma division_segment_numeral [simp]: |
|
561 |
"division_segment (numeral k) = 1" |
|
562 |
using division_segment_of_nat [of "numeral k"] by simp |
|
563 |
||
564 |
lemma euclidean_size_1 [simp]: |
|
565 |
"euclidean_size 1 = 1" |
|
566 |
using euclidean_size_of_nat [of 1] by simp |
|
567 |
||
568 |
lemma euclidean_size_numeral [simp]: |
|
569 |
"euclidean_size (numeral k) = numeral k" |
|
570 |
using euclidean_size_of_nat [of "numeral k"] by simp |
|
571 |
||
572 |
lemma of_nat_dvd_iff: |
|
573 |
"of_nat m dvd of_nat n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q") |
|
574 |
proof (cases "m = 0") |
|
575 |
case True |
|
576 |
then show ?thesis |
|
577 |
by simp |
|
578 |
next |
|
579 |
case False |
|
580 |
show ?thesis |
|
581 |
proof |
|
582 |
assume ?Q |
|
583 |
then show ?P |
|
584 |
by auto |
|
585 |
next |
|
586 |
assume ?P |
|
587 |
with False have "of_nat n = of_nat n div of_nat m * of_nat m" |
|
588 |
by simp |
|
589 |
then have "of_nat n = of_nat (n div m * m)" |
|
590 |
by (simp add: of_nat_div) |
|
591 |
then have "n = n div m * m" |
|
592 |
by (simp only: of_nat_eq_iff) |
|
593 |
then have "n = m * (n div m)" |
|
594 |
by (simp add: ac_simps) |
|
595 |
then show ?Q .. |
|
596 |
qed |
|
597 |
qed |
|
598 |
||
599 |
lemma of_nat_mod: |
|
600 |
"of_nat (m mod n) = of_nat m mod of_nat n" |
|
601 |
proof - |
|
602 |
have "of_nat m div of_nat n * of_nat n + of_nat m mod of_nat n = of_nat m" |
|
603 |
by (simp add: div_mult_mod_eq) |
|
604 |
also have "of_nat m = of_nat (m div n * n + m mod n)" |
|
605 |
by simp |
|
606 |
finally show ?thesis |
|
607 |
by (simp only: of_nat_div of_nat_mult of_nat_add) simp |
|
608 |
qed |
|
609 |
||
610 |
lemma one_div_two_eq_zero [simp]: |
|
611 |
"1 div 2 = 0" |
|
612 |
proof - |
|
613 |
from of_nat_div [symmetric] have "of_nat 1 div of_nat 2 = of_nat 0" |
|
614 |
by (simp only:) simp |
|
615 |
then show ?thesis |
|
616 |
by simp |
|
617 |
qed |
|
618 |
||
619 |
lemma one_mod_two_eq_one [simp]: |
|
620 |
"1 mod 2 = 1" |
|
621 |
proof - |
|
622 |
from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1" |
|
623 |
by (simp only:) simp |
|
624 |
then show ?thesis |
|
625 |
by simp |
|
626 |
qed |
|
627 |
||
628 |
lemma one_mod_2_pow_eq [simp]: |
|
629 |
"1 mod (2 ^ n) = of_bool (n > 0)" |
|
630 |
proof - |
|
631 |
have "1 mod (2 ^ n) = of_nat (1 mod (2 ^ n))" |
|
632 |
using of_nat_mod [of 1 "2 ^ n"] by simp |
|
633 |
also have "\<dots> = of_bool (n > 0)" |
|
634 |
by simp |
|
635 |
finally show ?thesis . |
|
636 |
qed |
|
637 |
||
638 |
lemma one_div_2_pow_eq [simp]: |
|
639 |
"1 div (2 ^ n) = of_bool (n = 0)" |
|
640 |
using div_mult_mod_eq [of 1 "2 ^ n"] by auto |
|
641 |
||
642 |
lemma div_mult2_eq': |
|
643 |
\<open>a div (of_nat m * of_nat n) = a div of_nat m div of_nat n\<close> |
|
644 |
proof (cases \<open>m = 0 \<or> n = 0\<close>) |
|
645 |
case True |
|
646 |
then show ?thesis |
|
647 |
by auto |
|
648 |
next |
|
649 |
case False |
|
650 |
then have \<open>m > 0\<close> \<open>n > 0\<close> |
|
651 |
by simp_all |
|
652 |
show ?thesis |
|
653 |
proof (cases \<open>of_nat m * of_nat n dvd a\<close>) |
|
654 |
case True |
|
655 |
then obtain b where \<open>a = (of_nat m * of_nat n) * b\<close> .. |
|
656 |
then have \<open>a = of_nat m * (of_nat n * b)\<close> |
|
657 |
by (simp add: ac_simps) |
|
658 |
then show ?thesis |
|
659 |
by simp |
|
660 |
next |
|
661 |
case False |
|
662 |
define q where \<open>q = a div (of_nat m * of_nat n)\<close> |
|
663 |
define r where \<open>r = a mod (of_nat m * of_nat n)\<close> |
|
664 |
from \<open>m > 0\<close> \<open>n > 0\<close> \<open>\<not> of_nat m * of_nat n dvd a\<close> r_def have "division_segment r = 1" |
|
665 |
using division_segment_of_nat [of "m * n"] by (simp add: division_segment_mod) |
|
666 |
with division_segment_euclidean_size [of r] |
|
667 |
have "of_nat (euclidean_size r) = r" |
|
668 |
by simp |
|
669 |
have "a mod (of_nat m * of_nat n) div (of_nat m * of_nat n) = 0" |
|
670 |
by simp |
|
671 |
with \<open>m > 0\<close> \<open>n > 0\<close> r_def have "r div (of_nat m * of_nat n) = 0" |
|
672 |
by simp |
|
673 |
with \<open>of_nat (euclidean_size r) = r\<close> |
|
674 |
have "of_nat (euclidean_size r) div (of_nat m * of_nat n) = 0" |
|
675 |
by simp |
|
676 |
then have "of_nat (euclidean_size r div (m * n)) = 0" |
|
677 |
by (simp add: of_nat_div) |
|
678 |
then have "of_nat (euclidean_size r div m div n) = 0" |
|
679 |
by (simp add: div_mult2_eq) |
|
680 |
with \<open>of_nat (euclidean_size r) = r\<close> have "r div of_nat m div of_nat n = 0" |
|
681 |
by (simp add: of_nat_div) |
|
682 |
with \<open>m > 0\<close> \<open>n > 0\<close> q_def |
|
683 |
have "q = (r div of_nat m + q * of_nat n * of_nat m div of_nat m) div of_nat n" |
|
684 |
by simp |
|
685 |
moreover have \<open>a = q * (of_nat m * of_nat n) + r\<close> |
|
686 |
by (simp add: q_def r_def div_mult_mod_eq) |
|
687 |
ultimately show \<open>a div (of_nat m * of_nat n) = a div of_nat m div of_nat n\<close> |
|
688 |
using q_def [symmetric] div_plus_div_distrib_dvd_right [of \<open>of_nat m\<close> \<open>q * (of_nat m * of_nat n)\<close> r] |
|
689 |
by (simp add: ac_simps) |
|
690 |
qed |
|
691 |
qed |
|
692 |
||
693 |
lemma mod_mult2_eq': |
|
694 |
"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" |
|
695 |
proof - |
|
696 |
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)" |
|
697 |
by (simp add: combine_common_factor div_mult_mod_eq) |
|
698 |
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)" |
|
699 |
by (simp add: ac_simps) |
|
700 |
ultimately show ?thesis |
|
701 |
by (simp add: div_mult2_eq' mult_commute) |
|
702 |
qed |
|
703 |
||
704 |
lemma div_mult2_numeral_eq: |
|
705 |
"a div numeral k div numeral l = a div numeral (k * l)" (is "?A = ?B") |
|
706 |
proof - |
|
707 |
have "?A = a div of_nat (numeral k) div of_nat (numeral l)" |
|
708 |
by simp |
|
709 |
also have "\<dots> = a div (of_nat (numeral k) * of_nat (numeral l))" |
|
710 |
by (fact div_mult2_eq' [symmetric]) |
|
711 |
also have "\<dots> = ?B" |
|
712 |
by simp |
|
713 |
finally show ?thesis . |
|
714 |
qed |
|
715 |
||
716 |
lemma numeral_Bit0_div_2: |
|
717 |
"numeral (num.Bit0 n) div 2 = numeral n" |
|
718 |
proof - |
|
719 |
have "numeral (num.Bit0 n) = numeral n + numeral n" |
|
720 |
by (simp only: numeral.simps) |
|
721 |
also have "\<dots> = numeral n * 2" |
|
722 |
by (simp add: mult_2_right) |
|
723 |
finally have "numeral (num.Bit0 n) div 2 = numeral n * 2 div 2" |
|
724 |
by simp |
|
725 |
also have "\<dots> = numeral n" |
|
726 |
by (rule nonzero_mult_div_cancel_right) simp |
|
727 |
finally show ?thesis . |
|
728 |
qed |
|
729 |
||
730 |
lemma numeral_Bit1_div_2: |
|
731 |
"numeral (num.Bit1 n) div 2 = numeral n" |
|
732 |
proof - |
|
733 |
have "numeral (num.Bit1 n) = numeral n + numeral n + 1" |
|
734 |
by (simp only: numeral.simps) |
|
735 |
also have "\<dots> = numeral n * 2 + 1" |
|
736 |
by (simp add: mult_2_right) |
|
737 |
finally have "numeral (num.Bit1 n) div 2 = (numeral n * 2 + 1) div 2" |
|
738 |
by simp |
|
739 |
also have "\<dots> = numeral n * 2 div 2 + 1 div 2" |
|
740 |
using dvd_triv_right by (rule div_plus_div_distrib_dvd_left) |
|
741 |
also have "\<dots> = numeral n * 2 div 2" |
|
742 |
by simp |
|
743 |
also have "\<dots> = numeral n" |
|
744 |
by (rule nonzero_mult_div_cancel_right) simp |
|
745 |
finally show ?thesis . |
|
746 |
qed |
|
747 |
||
748 |
lemma exp_mod_exp: |
|
749 |
\<open>2 ^ m mod 2 ^ n = of_bool (m < n) * 2 ^ m\<close> |
|
750 |
proof - |
|
751 |
have \<open>(2::nat) ^ m mod 2 ^ n = of_bool (m < n) * 2 ^ m\<close> (is \<open>?lhs = ?rhs\<close>) |
|
752 |
by (auto simp add: not_less monoid_mult_class.power_add dest!: le_Suc_ex) |
|
753 |
then have \<open>of_nat ?lhs = of_nat ?rhs\<close> |
|
754 |
by simp |
|
755 |
then show ?thesis |
|
756 |
by (simp add: of_nat_mod) |
|
757 |
qed |
|
758 |
||
759 |
lemma mask_mod_exp: |
|
760 |
\<open>(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - 1\<close> |
|
761 |
proof - |
|
762 |
have \<open>(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - (1::nat)\<close> (is \<open>?lhs = ?rhs\<close>) |
|
763 |
proof (cases \<open>n \<le> m\<close>) |
|
764 |
case True |
|
765 |
then show ?thesis |
|
766 |
by (simp add: Suc_le_lessD) |
|
767 |
next |
|
768 |
case False |
|
769 |
then have \<open>m < n\<close> |
|
770 |
by simp |
|
771 |
then obtain q where n: \<open>n = Suc q + m\<close> |
|
772 |
by (auto dest: less_imp_Suc_add) |
|
773 |
then have \<open>min m n = m\<close> |
|
774 |
by simp |
|
775 |
moreover have \<open>(2::nat) ^ m \<le> 2 * 2 ^ q * 2 ^ m\<close> |
|
776 |
using mult_le_mono1 [of 1 \<open>2 * 2 ^ q\<close> \<open>2 ^ m\<close>] by simp |
|
777 |
with n have \<open>2 ^ n - 1 = (2 ^ Suc q - 1) * 2 ^ m + (2 ^ m - (1::nat))\<close> |
|
778 |
by (simp add: monoid_mult_class.power_add algebra_simps) |
|
779 |
ultimately show ?thesis |
|
780 |
by (simp only: euclidean_semiring_cancel_class.mod_mult_self3) simp |
|
781 |
qed |
|
782 |
then have \<open>of_nat ?lhs = of_nat ?rhs\<close> |
|
783 |
by simp |
|
784 |
then show ?thesis |
|
785 |
by (simp add: of_nat_mod of_nat_diff) |
|
786 |
qed |
|
787 |
||
788 |
lemma of_bool_half_eq_0 [simp]: |
|
789 |
\<open>of_bool b div 2 = 0\<close> |
|
790 |
by simp |
|
791 |
||
792 |
end |
|
793 |
||
794 |
class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat |
|
795 |
||
796 |
instance nat :: unique_euclidean_semiring_with_nat |
|
797 |
by standard (simp_all add: dvd_eq_mod_eq_0) |
|
798 |
||
799 |
instance int :: unique_euclidean_ring_with_nat |
|
800 |
by standard (auto simp add: divide_int_def division_segment_int_def elim: contrapos_np) |
|
801 |
||
802 |
||
803 |
context unique_euclidean_semiring_with_nat |
|
804 |
begin |
|
805 |
||
806 |
subclass semiring_parity |
|
807 |
proof |
|
808 |
show "2 dvd a \<longleftrightarrow> a mod 2 = 0" for a |
|
809 |
by (fact dvd_eq_mod_eq_0) |
|
810 |
show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1" for a |
|
811 |
proof |
|
812 |
assume "a mod 2 = 1" |
|
813 |
then show "\<not> 2 dvd a" |
|
814 |
by auto |
|
815 |
next |
|
816 |
assume "\<not> 2 dvd a" |
|
817 |
have eucl: "euclidean_size (a mod 2) = 1" |
|
818 |
proof (rule order_antisym) |
|
819 |
show "euclidean_size (a mod 2) \<le> 1" |
|
820 |
using mod_size_less [of 2 a] by simp |
|
821 |
show "1 \<le> euclidean_size (a mod 2)" |
|
822 |
using \<open>\<not> 2 dvd a\<close> by (simp add: Suc_le_eq dvd_eq_mod_eq_0) |
|
823 |
qed |
|
824 |
from \<open>\<not> 2 dvd a\<close> have "\<not> of_nat 2 dvd division_segment a * of_nat (euclidean_size a)" |
|
825 |
by simp |
|
826 |
then have "\<not> of_nat 2 dvd of_nat (euclidean_size a)" |
|
827 |
by (auto simp only: dvd_mult_unit_iff' is_unit_division_segment) |
|
828 |
then have "\<not> 2 dvd euclidean_size a" |
|
829 |
using of_nat_dvd_iff [of 2] by simp |
|
830 |
then have "euclidean_size a mod 2 = 1" |
|
831 |
by (simp add: semidom_modulo_class.dvd_eq_mod_eq_0) |
|
832 |
then have "of_nat (euclidean_size a mod 2) = of_nat 1" |
|
833 |
by simp |
|
834 |
then have "of_nat (euclidean_size a) mod 2 = 1" |
|
835 |
by (simp add: of_nat_mod) |
|
836 |
from \<open>\<not> 2 dvd a\<close> eucl |
|
837 |
show "a mod 2 = 1" |
|
838 |
by (auto intro: division_segment_eq_iff simp add: division_segment_mod) |
|
839 |
qed |
|
840 |
show "\<not> is_unit 2" |
|
841 |
proof (rule notI) |
|
842 |
assume "is_unit 2" |
|
843 |
then have "of_nat 2 dvd of_nat 1" |
|
844 |
by simp |
|
845 |
then have "is_unit (2::nat)" |
|
846 |
by (simp only: of_nat_dvd_iff) |
|
847 |
then show False |
|
848 |
by simp |
|
849 |
qed |
|
850 |
qed |
|
851 |
||
852 |
lemma even_succ_div_two [simp]: |
|
853 |
"even a \<Longrightarrow> (a + 1) div 2 = a div 2" |
|
854 |
by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero) |
|
855 |
||
856 |
lemma odd_succ_div_two [simp]: |
|
857 |
"odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1" |
|
858 |
by (auto elim!: oddE simp add: add.assoc) |
|
859 |
||
860 |
lemma even_two_times_div_two: |
|
861 |
"even a \<Longrightarrow> 2 * (a div 2) = a" |
|
862 |
by (fact dvd_mult_div_cancel) |
|
863 |
||
864 |
lemma odd_two_times_div_two_succ [simp]: |
|
865 |
"odd a \<Longrightarrow> 2 * (a div 2) + 1 = a" |
|
866 |
using mult_div_mod_eq [of 2 a] |
|
867 |
by (simp add: even_iff_mod_2_eq_zero) |
|
868 |
||
869 |
lemma coprime_left_2_iff_odd [simp]: |
|
870 |
"coprime 2 a \<longleftrightarrow> odd a" |
|
871 |
proof |
|
872 |
assume "odd a" |
|
873 |
show "coprime 2 a" |
|
874 |
proof (rule coprimeI) |
|
875 |
fix b |
|
876 |
assume "b dvd 2" "b dvd a" |
|
877 |
then have "b dvd a mod 2" |
|
878 |
by (auto intro: dvd_mod) |
|
879 |
with \<open>odd a\<close> show "is_unit b" |
|
880 |
by (simp add: mod_2_eq_odd) |
|
881 |
qed |
|
882 |
next |
|
883 |
assume "coprime 2 a" |
|
884 |
show "odd a" |
|
885 |
proof (rule notI) |
|
886 |
assume "even a" |
|
887 |
then obtain b where "a = 2 * b" .. |
|
888 |
with \<open>coprime 2 a\<close> have "coprime 2 (2 * b)" |
|
889 |
by simp |
|
890 |
moreover have "\<not> coprime 2 (2 * b)" |
|
891 |
by (rule not_coprimeI [of 2]) simp_all |
|
892 |
ultimately show False |
|
893 |
by blast |
|
894 |
qed |
|
895 |
qed |
|
896 |
||
897 |
lemma coprime_right_2_iff_odd [simp]: |
|
898 |
"coprime a 2 \<longleftrightarrow> odd a" |
|
899 |
using coprime_left_2_iff_odd [of a] by (simp add: ac_simps) |
|
900 |
||
901 |
end |
|
902 |
||
903 |
context unique_euclidean_ring_with_nat |
|
904 |
begin |
|
905 |
||
906 |
subclass ring_parity .. |
|
907 |
||
908 |
lemma minus_1_mod_2_eq [simp]: |
|
909 |
"- 1 mod 2 = 1" |
|
910 |
by (simp add: mod_2_eq_odd) |
|
911 |
||
912 |
lemma minus_1_div_2_eq [simp]: |
|
913 |
"- 1 div 2 = - 1" |
|
914 |
proof - |
|
915 |
from div_mult_mod_eq [of "- 1" 2] |
|
916 |
have "- 1 div 2 * 2 = - 1 * 2" |
|
917 |
using add_implies_diff by fastforce |
|
918 |
then show ?thesis |
|
919 |
using mult_right_cancel [of 2 "- 1 div 2" "- 1"] by simp |
|
920 |
qed |
|
921 |
||
922 |
end |
|
923 |
||
924 |
context unique_euclidean_semiring_with_nat |
|
925 |
begin |
|
926 |
||
927 |
lemma even_mask_div_iff': |
|
928 |
\<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> m \<le> n\<close> |
|
929 |
proof - |
|
930 |
have \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> even (of_nat ((2 ^ m - Suc 0) div 2 ^ n))\<close> |
|
931 |
by (simp only: of_nat_div) (simp add: of_nat_diff) |
|
932 |
also have \<open>\<dots> \<longleftrightarrow> even ((2 ^ m - Suc 0) div 2 ^ n)\<close> |
|
933 |
by simp |
|
934 |
also have \<open>\<dots> \<longleftrightarrow> m \<le> n\<close> |
|
935 |
proof (cases \<open>m \<le> n\<close>) |
|
936 |
case True |
|
937 |
then show ?thesis |
|
938 |
by (simp add: Suc_le_lessD) |
|
939 |
next |
|
940 |
case False |
|
941 |
then obtain r where r: \<open>m = n + Suc r\<close> |
|
942 |
using less_imp_Suc_add by fastforce |
|
943 |
from r have \<open>{q. q < m} \<inter> {q. 2 ^ n dvd (2::nat) ^ q} = {q. n \<le> q \<and> q < m}\<close> |
|
944 |
by (auto simp add: dvd_power_iff_le) |
|
945 |
moreover from r have \<open>{q. q < m} \<inter> {q. \<not> 2 ^ n dvd (2::nat) ^ q} = {q. q < n}\<close> |
|
946 |
by (auto simp add: dvd_power_iff_le) |
|
947 |
moreover from False have \<open>{q. n \<le> q \<and> q < m \<and> q \<le> n} = {n}\<close> |
|
948 |
by auto |
|
949 |
then have \<open>odd ((\<Sum>a\<in>{q. n \<le> q \<and> q < m}. 2 ^ a div (2::nat) ^ n) + sum ((^) 2) {q. q < n} div 2 ^ n)\<close> |
|
950 |
by (simp_all add: euclidean_semiring_cancel_class.power_diff_power_eq semiring_parity_class.even_sum_iff not_less mask_eq_sum_exp_nat [symmetric]) |
|
951 |
ultimately have \<open>odd (sum ((^) (2::nat)) {q. q < m} div 2 ^ n)\<close> |
|
952 |
by (subst euclidean_semiring_cancel_class.sum_div_partition) simp_all |
|
953 |
with False show ?thesis |
|
954 |
by (simp add: mask_eq_sum_exp_nat) |
|
955 |
qed |
|
956 |
finally show ?thesis . |
|
957 |
qed |
|
958 |
||
959 |
end |
|
960 |
||
961 |
||
962 |
subsection \<open>Generic symbolic computations\<close> |
|
963 |
||
964 |
text \<open> |
|
965 |
The following type class contains everything necessary to formulate |
|
966 |
a division algorithm in ring structures with numerals, restricted |
|
967 |
to its positive segments. |
|
968 |
\<close> |
|
969 |
||
970 |
class unique_euclidean_semiring_with_nat_division = unique_euclidean_semiring_with_nat + |
|
971 |
fixes divmod :: \<open>num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a\<close> |
|
972 |
and divmod_step :: \<open>'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a\<close> \<comment> \<open> |
|
973 |
These are conceptually definitions but force generated code |
|
974 |
to be monomorphic wrt. particular instances of this class which |
|
975 |
yields a significant speedup.\<close> |
|
976 |
assumes divmod_def: \<open>divmod m n = (numeral m div numeral n, numeral m mod numeral n)\<close> |
|
977 |
and divmod_step_def [simp]: \<open>divmod_step l (q, r) = |
|
978 |
(if euclidean_size l \<le> euclidean_size r then (2 * q + 1, r - l) |
|
979 |
else (2 * q, r))\<close> \<comment> \<open> |
|
980 |
This is a formulation of one step (referring to one digit position) |
|
981 |
in school-method division: compare the dividend at the current |
|
982 |
digit position with the remainder from previous division steps |
|
983 |
and evaluate accordingly.\<close> |
|
984 |
begin |
|
985 |
||
986 |
lemma fst_divmod: |
|
987 |
\<open>fst (divmod m n) = numeral m div numeral n\<close> |
|
988 |
by (simp add: divmod_def) |
|
989 |
||
990 |
lemma snd_divmod: |
|
991 |
\<open>snd (divmod m n) = numeral m mod numeral n\<close> |
|
992 |
by (simp add: divmod_def) |
|
993 |
||
994 |
text \<open> |
|
995 |
Following a formulation of school-method division. |
|
996 |
If the divisor is smaller than the dividend, terminate. |
|
997 |
If not, shift the dividend to the right until termination |
|
998 |
occurs and then reiterate single division steps in the |
|
999 |
opposite direction. |
|
1000 |
\<close> |
|
1001 |
||
1002 |
lemma divmod_divmod_step: |
|
1003 |
\<open>divmod m n = (if m < n then (0, numeral m) |
|
1004 |
else divmod_step (numeral n) (divmod m (Num.Bit0 n)))\<close> |
|
1005 |
proof (cases \<open>m < n\<close>) |
|
1006 |
case True |
|
1007 |
then show ?thesis |
|
1008 |
by (simp add: prod_eq_iff fst_divmod snd_divmod flip: of_nat_numeral of_nat_div of_nat_mod) |
|
1009 |
next |
|
1010 |
case False |
|
1011 |
define r s t where \<open>r = (numeral m :: nat)\<close> \<open>s = (numeral n :: nat)\<close> \<open>t = 2 * s\<close> |
|
1012 |
then have *: \<open>numeral m = of_nat r\<close> \<open>numeral n = of_nat s\<close> \<open>numeral (num.Bit0 n) = of_nat t\<close> |
|
1013 |
and \<open>\<not> s \<le> r mod s\<close> |
|
1014 |
by (simp_all add: not_le) |
|
1015 |
have t: \<open>2 * (r div t) = r div s - r div s mod 2\<close> |
|
1016 |
\<open>r mod t = s * (r div s mod 2) + r mod s\<close> |
|
77061
5de3772609ea
generalized theory name: euclidean division denotes one particular division definition on integers
haftmann
parents:
76387
diff
changeset
|
1017 |
by (simp add: Rings.minus_mod_eq_mult_div Groups.mult.commute [of 2] Euclidean_Rings.div_mult2_eq \<open>t = 2 * s\<close>) |
76387 | 1018 |
(use mod_mult2_eq [of r s 2] in \<open>simp add: ac_simps \<open>t = 2 * s\<close>\<close>) |
1019 |
have rs: \<open>r div s mod 2 = 0 \<or> r div s mod 2 = Suc 0\<close> |
|
1020 |
by auto |
|
1021 |
from \<open>\<not> s \<le> r mod s\<close> have \<open>s \<le> r mod t \<Longrightarrow> |
|
1022 |
r div s = Suc (2 * (r div t)) \<and> |
|
1023 |
r mod s = r mod t - s\<close> |
|
1024 |
using rs |
|
1025 |
by (auto simp add: t) |
|
1026 |
moreover have \<open>r mod t < s \<Longrightarrow> |
|
1027 |
r div s = 2 * (r div t) \<and> |
|
1028 |
r mod s = r mod t\<close> |
|
1029 |
using rs |
|
1030 |
by (auto simp add: t) |
|
1031 |
ultimately show ?thesis |
|
1032 |
by (simp add: divmod_def prod_eq_iff split_def Let_def |
|
1033 |
not_less mod_eq_0_iff_dvd Rings.mod_eq_0_iff_dvd False not_le *) |
|
1034 |
(simp add: flip: of_nat_numeral of_nat_mult add.commute [of 1] of_nat_div of_nat_mod of_nat_Suc of_nat_diff) |
|
1035 |
qed |
|
1036 |
||
1037 |
text \<open>The division rewrite proper -- first, trivial results involving \<open>1\<close>\<close> |
|
1038 |
||
1039 |
lemma divmod_trivial [simp]: |
|
1040 |
"divmod m Num.One = (numeral m, 0)" |
|
1041 |
"divmod num.One (num.Bit0 n) = (0, Numeral1)" |
|
1042 |
"divmod num.One (num.Bit1 n) = (0, Numeral1)" |
|
1043 |
using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def) |
|
1044 |
||
1045 |
text \<open>Division by an even number is a right-shift\<close> |
|
1046 |
||
1047 |
lemma divmod_cancel [simp]: |
|
1048 |
\<open>divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))\<close> (is ?P) |
|
1049 |
\<open>divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))\<close> (is ?Q) |
|
1050 |
proof - |
|
1051 |
define r s where \<open>r = (numeral m :: nat)\<close> \<open>s = (numeral n :: nat)\<close> |
|
1052 |
then have *: \<open>numeral m = of_nat r\<close> \<open>numeral n = of_nat s\<close> |
|
1053 |
\<open>numeral (num.Bit0 m) = of_nat (2 * r)\<close> \<open>numeral (num.Bit0 n) = of_nat (2 * s)\<close> |
|
1054 |
\<open>numeral (num.Bit1 m) = of_nat (Suc (2 * r))\<close> |
|
1055 |
by simp_all |
|
1056 |
have **: \<open>Suc (2 * r) div 2 = r\<close> |
|
1057 |
by simp |
|
1058 |
show ?P and ?Q |
|
1059 |
by (simp_all add: divmod_def *) |
|
1060 |
(simp_all flip: of_nat_numeral of_nat_div of_nat_mod of_nat_mult add.commute [of 1] of_nat_Suc |
|
77061
5de3772609ea
generalized theory name: euclidean division denotes one particular division definition on integers
haftmann
parents:
76387
diff
changeset
|
1061 |
add: Euclidean_Rings.mod_mult_mult1 div_mult2_eq [of _ 2] mod_mult2_eq [of _ 2] **) |
76387 | 1062 |
qed |
1063 |
||
1064 |
text \<open>The really hard work\<close> |
|
1065 |
||
1066 |
lemma divmod_steps [simp]: |
|
1067 |
"divmod (num.Bit0 m) (num.Bit1 n) = |
|
1068 |
(if m \<le> n then (0, numeral (num.Bit0 m)) |
|
1069 |
else divmod_step (numeral (num.Bit1 n)) |
|
1070 |
(divmod (num.Bit0 m) |
|
1071 |
(num.Bit0 (num.Bit1 n))))" |
|
1072 |
"divmod (num.Bit1 m) (num.Bit1 n) = |
|
1073 |
(if m < n then (0, numeral (num.Bit1 m)) |
|
1074 |
else divmod_step (numeral (num.Bit1 n)) |
|
1075 |
(divmod (num.Bit1 m) |
|
1076 |
(num.Bit0 (num.Bit1 n))))" |
|
1077 |
by (simp_all add: divmod_divmod_step) |
|
1078 |
||
1079 |
lemmas divmod_algorithm_code = divmod_trivial divmod_cancel divmod_steps |
|
1080 |
||
1081 |
text \<open>Special case: divisibility\<close> |
|
1082 |
||
1083 |
definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool" |
|
1084 |
where |
|
1085 |
"divides_aux qr \<longleftrightarrow> snd qr = 0" |
|
1086 |
||
1087 |
lemma divides_aux_eq [simp]: |
|
1088 |
"divides_aux (q, r) \<longleftrightarrow> r = 0" |
|
1089 |
by (simp add: divides_aux_def) |
|
1090 |
||
1091 |
lemma dvd_numeral_simp [simp]: |
|
1092 |
"numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)" |
|
1093 |
by (simp add: divmod_def mod_eq_0_iff_dvd) |
|
1094 |
||
1095 |
text \<open>Generic computation of quotient and remainder\<close> |
|
1096 |
||
1097 |
lemma numeral_div_numeral [simp]: |
|
1098 |
"numeral k div numeral l = fst (divmod k l)" |
|
1099 |
by (simp add: fst_divmod) |
|
1100 |
||
1101 |
lemma numeral_mod_numeral [simp]: |
|
1102 |
"numeral k mod numeral l = snd (divmod k l)" |
|
1103 |
by (simp add: snd_divmod) |
|
1104 |
||
1105 |
lemma one_div_numeral [simp]: |
|
1106 |
"1 div numeral n = fst (divmod num.One n)" |
|
1107 |
by (simp add: fst_divmod) |
|
1108 |
||
1109 |
lemma one_mod_numeral [simp]: |
|
1110 |
"1 mod numeral n = snd (divmod num.One n)" |
|
1111 |
by (simp add: snd_divmod) |
|
1112 |
||
1113 |
end |
|
1114 |
||
1115 |
instantiation nat :: unique_euclidean_semiring_with_nat_division |
|
1116 |
begin |
|
1117 |
||
1118 |
definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat" |
|
1119 |
where |
|
1120 |
divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)" |
|
1121 |
||
1122 |
definition divmod_step_nat :: "nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat" |
|
1123 |
where |
|
1124 |
"divmod_step_nat l qr = (let (q, r) = qr |
|
1125 |
in if r \<ge> l then (2 * q + 1, r - l) |
|
1126 |
else (2 * q, r))" |
|
1127 |
||
1128 |
instance |
|
1129 |
by standard (simp_all add: divmod'_nat_def divmod_step_nat_def) |
|
1130 |
||
1131 |
end |
|
1132 |
||
1133 |
declare divmod_algorithm_code [where ?'a = nat, code] |
|
1134 |
||
1135 |
lemma Suc_0_div_numeral [simp]: |
|
1136 |
\<open>Suc 0 div numeral Num.One = 1\<close> |
|
1137 |
\<open>Suc 0 div numeral (Num.Bit0 n) = 0\<close> |
|
1138 |
\<open>Suc 0 div numeral (Num.Bit1 n) = 0\<close> |
|
1139 |
by simp_all |
|
1140 |
||
1141 |
lemma Suc_0_mod_numeral [simp]: |
|
1142 |
\<open>Suc 0 mod numeral Num.One = 0\<close> |
|
1143 |
\<open>Suc 0 mod numeral (Num.Bit0 n) = 1\<close> |
|
1144 |
\<open>Suc 0 mod numeral (Num.Bit1 n) = 1\<close> |
|
1145 |
by simp_all |
|
1146 |
||
1147 |
instantiation int :: unique_euclidean_semiring_with_nat_division |
|
1148 |
begin |
|
1149 |
||
1150 |
definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int" |
|
1151 |
where |
|
1152 |
"divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)" |
|
1153 |
||
1154 |
definition divmod_step_int :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" |
|
1155 |
where |
|
1156 |
"divmod_step_int l qr = (let (q, r) = qr |
|
1157 |
in if \<bar>l\<bar> \<le> \<bar>r\<bar> then (2 * q + 1, r - l) |
|
1158 |
else (2 * q, r))" |
|
1159 |
||
1160 |
instance |
|
1161 |
by standard (auto simp add: divmod_int_def divmod_step_int_def) |
|
1162 |
||
1163 |
end |
|
1164 |
||
1165 |
declare divmod_algorithm_code [where ?'a = int, code] |
|
1166 |
||
1167 |
context |
|
1168 |
begin |
|
1169 |
||
1170 |
qualified definition adjust_div :: "int \<times> int \<Rightarrow> int" |
|
1171 |
where |
|
1172 |
"adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))" |
|
1173 |
||
1174 |
qualified lemma adjust_div_eq [simp, code]: |
|
1175 |
"adjust_div (q, r) = q + of_bool (r \<noteq> 0)" |
|
1176 |
by (simp add: adjust_div_def) |
|
1177 |
||
1178 |
qualified definition adjust_mod :: "num \<Rightarrow> int \<Rightarrow> int" |
|
1179 |
where |
|
1180 |
[simp]: "adjust_mod l r = (if r = 0 then 0 else numeral l - r)" |
|
1181 |
||
1182 |
lemma minus_numeral_div_numeral [simp]: |
|
1183 |
"- numeral m div numeral n = - (adjust_div (divmod m n) :: int)" |
|
1184 |
proof - |
|
1185 |
have "int (fst (divmod m n)) = fst (divmod m n)" |
|
1186 |
by (simp only: fst_divmod divide_int_def) auto |
|
1187 |
then show ?thesis |
|
1188 |
by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def) |
|
1189 |
qed |
|
1190 |
||
1191 |
lemma minus_numeral_mod_numeral [simp]: |
|
1192 |
"- numeral m mod numeral n = adjust_mod n (snd (divmod m n) :: int)" |
|
1193 |
proof (cases "snd (divmod m n) = (0::int)") |
|
1194 |
case True |
|
1195 |
then show ?thesis |
|
1196 |
by (simp add: mod_eq_0_iff_dvd divides_aux_def) |
|
1197 |
next |
|
1198 |
case False |
|
1199 |
then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)" |
|
1200 |
by (simp only: snd_divmod modulo_int_def) auto |
|
1201 |
then show ?thesis |
|
1202 |
by (simp add: divides_aux_def adjust_div_def) |
|
1203 |
(simp add: divides_aux_def modulo_int_def) |
|
1204 |
qed |
|
1205 |
||
1206 |
lemma numeral_div_minus_numeral [simp]: |
|
1207 |
"numeral m div - numeral n = - (adjust_div (divmod m n) :: int)" |
|
1208 |
proof - |
|
1209 |
have "int (fst (divmod m n)) = fst (divmod m n)" |
|
1210 |
by (simp only: fst_divmod divide_int_def) auto |
|
1211 |
then show ?thesis |
|
1212 |
by (auto simp add: split_def Let_def adjust_div_def divides_aux_def divide_int_def) |
|
1213 |
qed |
|
1214 |
||
1215 |
lemma numeral_mod_minus_numeral [simp]: |
|
1216 |
"numeral m mod - numeral n = - adjust_mod n (snd (divmod m n) :: int)" |
|
1217 |
proof (cases "snd (divmod m n) = (0::int)") |
|
1218 |
case True |
|
1219 |
then show ?thesis |
|
1220 |
by (simp add: mod_eq_0_iff_dvd divides_aux_def) |
|
1221 |
next |
|
1222 |
case False |
|
1223 |
then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) \<noteq> (0::int)" |
|
1224 |
by (simp only: snd_divmod modulo_int_def) auto |
|
1225 |
then show ?thesis |
|
1226 |
by (simp add: divides_aux_def adjust_div_def) |
|
1227 |
(simp add: divides_aux_def modulo_int_def) |
|
1228 |
qed |
|
1229 |
||
1230 |
lemma minus_one_div_numeral [simp]: |
|
1231 |
"- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)" |
|
1232 |
using minus_numeral_div_numeral [of Num.One n] by simp |
|
1233 |
||
1234 |
lemma minus_one_mod_numeral [simp]: |
|
1235 |
"- 1 mod numeral n = adjust_mod n (snd (divmod Num.One n) :: int)" |
|
1236 |
using minus_numeral_mod_numeral [of Num.One n] by simp |
|
1237 |
||
1238 |
lemma one_div_minus_numeral [simp]: |
|
1239 |
"1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)" |
|
1240 |
using numeral_div_minus_numeral [of Num.One n] by simp |
|
1241 |
||
1242 |
lemma one_mod_minus_numeral [simp]: |
|
1243 |
"1 mod - numeral n = - adjust_mod n (snd (divmod Num.One n) :: int)" |
|
1244 |
using numeral_mod_minus_numeral [of Num.One n] by simp |
|
1245 |
||
1246 |
lemma [code]: |
|
1247 |
fixes k :: int |
|
1248 |
shows |
|
1249 |
"k div 0 = 0" |
|
1250 |
"k mod 0 = k" |
|
1251 |
"0 div k = 0" |
|
1252 |
"0 mod k = 0" |
|
1253 |
"k div Int.Pos Num.One = k" |
|
1254 |
"k mod Int.Pos Num.One = 0" |
|
1255 |
"k div Int.Neg Num.One = - k" |
|
1256 |
"k mod Int.Neg Num.One = 0" |
|
1257 |
"Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)" |
|
1258 |
"Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)" |
|
1259 |
"Int.Neg m div Int.Pos n = - (adjust_div (divmod m n) :: int)" |
|
1260 |
"Int.Neg m mod Int.Pos n = adjust_mod n (snd (divmod m n) :: int)" |
|
1261 |
"Int.Pos m div Int.Neg n = - (adjust_div (divmod m n) :: int)" |
|
1262 |
"Int.Pos m mod Int.Neg n = - adjust_mod n (snd (divmod m n) :: int)" |
|
1263 |
"Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)" |
|
1264 |
"Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)" |
|
1265 |
by simp_all |
|
1266 |
||
1267 |
end |
|
1268 |
||
1269 |
lemma divmod_BitM_2_eq [simp]: |
|
1270 |
\<open>divmod (Num.BitM m) (Num.Bit0 Num.One) = (numeral m - 1, (1 :: int))\<close> |
|
1271 |
by (cases m) simp_all |
|
1272 |
||
1273 |
||
1274 |
subsubsection \<open>Computation by simplification\<close> |
|
1275 |
||
1276 |
lemma euclidean_size_nat_less_eq_iff: |
|
1277 |
\<open>euclidean_size m \<le> euclidean_size n \<longleftrightarrow> m \<le> n\<close> for m n :: nat |
|
1278 |
by simp |
|
1279 |
||
1280 |
lemma euclidean_size_int_less_eq_iff: |
|
1281 |
\<open>euclidean_size k \<le> euclidean_size l \<longleftrightarrow> \<bar>k\<bar> \<le> \<bar>l\<bar>\<close> for k l :: int |
|
1282 |
by auto |
|
1283 |
||
1284 |
simproc_setup numeral_divmod |
|
1285 |
("0 div 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | |
|
1286 |
"0 div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | |
|
1287 |
"0 div - 1 :: int" | "0 mod - 1 :: int" | |
|
1288 |
"0 div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | |
|
1289 |
"0 div - numeral b :: int" | "0 mod - numeral b :: int" | |
|
1290 |
"1 div 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | |
|
1291 |
"1 div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | |
|
1292 |
"1 div - 1 :: int" | "1 mod - 1 :: int" | |
|
1293 |
"1 div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | |
|
1294 |
"1 div - numeral b :: int" |"1 mod - numeral b :: int" | |
|
1295 |
"- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" | |
|
1296 |
"- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" | |
|
1297 |
"- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" | |
|
1298 |
"numeral a div 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | |
|
1299 |
"numeral a div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | |
|
1300 |
"numeral a div - 1 :: int" | "numeral a mod - 1 :: int" | |
|
1301 |
"numeral a div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | |
|
1302 |
"numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" | |
|
1303 |
"- numeral a div 0 :: int" | "- numeral a mod 0 :: int" | |
|
1304 |
"- numeral a div 1 :: int" | "- numeral a mod 1 :: int" | |
|
1305 |
"- numeral a div - 1 :: int" | "- numeral a mod - 1 :: int" | |
|
1306 |
"- numeral a div numeral b :: int" | "- numeral a mod numeral b :: int" | |
|
1307 |
"- numeral a div - numeral b :: int" | "- numeral a mod - numeral b :: int") = \<open> |
|
1308 |
let |
|
1309 |
val if_cong = the (Code.get_case_cong \<^theory> \<^const_name>\<open>If\<close>); |
|
1310 |
fun successful_rewrite ctxt ct = |
|
1311 |
let |
|
1312 |
val thm = Simplifier.rewrite ctxt ct |
|
1313 |
in if Thm.is_reflexive thm then NONE else SOME thm end; |
|
1314 |
in fn phi => |
|
1315 |
let |
|
1316 |
val simps = Morphism.fact phi (@{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1 |
|
1317 |
one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral |
|
1318 |
one_div_minus_numeral one_mod_minus_numeral |
|
1319 |
numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral |
|
1320 |
numeral_div_minus_numeral numeral_mod_minus_numeral |
|
1321 |
div_minus_minus mod_minus_minus Parity.adjust_div_eq of_bool_eq one_neq_zero |
|
1322 |
numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial |
|
1323 |
divmod_cancel divmod_steps divmod_step_def fst_conv snd_conv numeral_One |
|
1324 |
case_prod_beta rel_simps Parity.adjust_mod_def div_minus1_right mod_minus1_right |
|
1325 |
minus_minus numeral_times_numeral mult_zero_right mult_1_right |
|
1326 |
euclidean_size_nat_less_eq_iff euclidean_size_int_less_eq_iff diff_nat_numeral nat_numeral} |
|
1327 |
@ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]); |
|
1328 |
fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt |
|
1329 |
(Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps) |
|
1330 |
in fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt) end |
|
1331 |
end |
|
1332 |
\<close> \<comment> \<open> |
|
1333 |
There is space for improvement here: the calculation itself |
|
1334 |
could be carried out outside the logic, and a generic simproc |
|
1335 |
(simplifier setup) for generic calculation would be helpful. |
|
1336 |
\<close> |
|
1337 |
||
1338 |
||
75937 | 1339 |
subsection \<open>Computing congruences modulo \<open>2 ^ q\<close>\<close> |
1340 |
||
1341 |
context unique_euclidean_semiring_with_nat_division |
|
1342 |
begin |
|
1343 |
||
1344 |
lemma cong_exp_iff_simps: |
|
1345 |
"numeral n mod numeral Num.One = 0 |
|
1346 |
\<longleftrightarrow> True" |
|
1347 |
"numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0 |
|
1348 |
\<longleftrightarrow> numeral n mod numeral q = 0" |
|
1349 |
"numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0 |
|
1350 |
\<longleftrightarrow> False" |
|
1351 |
"numeral m mod numeral Num.One = (numeral n mod numeral Num.One) |
|
1352 |
\<longleftrightarrow> True" |
|
1353 |
"numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q)) |
|
1354 |
\<longleftrightarrow> True" |
|
1355 |
"numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q)) |
|
1356 |
\<longleftrightarrow> False" |
|
1357 |
"numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q)) |
|
1358 |
\<longleftrightarrow> (numeral n mod numeral q) = 0" |
|
1359 |
"numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q)) |
|
1360 |
\<longleftrightarrow> False" |
|
1361 |
"numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q)) |
|
1362 |
\<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)" |
|
1363 |
"numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q)) |
|
1364 |
\<longleftrightarrow> False" |
|
1365 |
"numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q)) |
|
1366 |
\<longleftrightarrow> (numeral m mod numeral q) = 0" |
|
1367 |
"numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q)) |
|
1368 |
\<longleftrightarrow> False" |
|
1369 |
"numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q)) |
|
1370 |
\<longleftrightarrow> numeral m mod numeral q = (numeral n mod numeral q)" |
|
1371 |
by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even]) |
|
1372 |
||
1373 |
end |
|
1374 |
||
1375 |
||
71853 | 1376 |
code_identifier |
1377 |
code_module Parity \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith |
|
1378 |
||
74592 | 1379 |
lemmas even_of_nat = even_of_nat_iff |
1380 |
||
67816 | 1381 |
end |