147 moreover have "a div b = a div b" .. |
147 moreover have "a div b = a div b" .. |
148 moreover have "a mod b = a mod b" .. |
148 moreover have "a mod b = a mod b" .. |
149 note that ultimately show thesis by blast |
149 note that ultimately show thesis by blast |
150 qed |
150 qed |
151 |
151 |
152 lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0" |
152 lemma dvd_imp_mod_0 [simp]: |
|
153 assumes "a dvd b" |
|
154 shows "b mod a = 0" |
|
155 proof - |
|
156 from assms obtain c where "b = a * c" .. |
|
157 then have "b mod a = a * c mod a" by simp |
|
158 then show "b mod a = 0" by simp |
|
159 qed |
|
160 |
|
161 lemma dvd_eq_mod_eq_0 [code]: |
|
162 "a dvd b \<longleftrightarrow> b mod a = 0" |
153 proof |
163 proof |
154 assume "b mod a = 0" |
164 assume "b mod a = 0" |
155 with mod_div_equality [of b a] have "b div a * a = b" by simp |
165 with mod_div_equality [of b a] have "b div a * a = b" by simp |
156 then have "b = a * (b div a)" unfolding mult.commute .. |
166 then have "b = a * (b div a)" unfolding mult.commute .. |
157 then have "\<exists>c. b = a * c" .. |
167 then show "a dvd b" .. |
158 then show "a dvd b" unfolding dvd_def . |
168 next |
159 next |
169 assume "a dvd b" then show "b mod a = 0" by simp |
160 assume "a dvd b" |
|
161 then have "\<exists>c. b = a * c" unfolding dvd_def . |
|
162 then obtain c where "b = a * c" .. |
|
163 then have "b mod a = a * c mod a" by simp |
|
164 then have "b mod a = c * a mod a" by (simp add: mult.commute) |
|
165 then show "b mod a = 0" by simp |
|
166 qed |
170 qed |
167 |
171 |
168 lemma mod_div_trivial [simp]: "a mod b div b = 0" |
172 lemma mod_div_trivial [simp]: "a mod b div b = 0" |
169 proof (cases "b = 0") |
173 proof (cases "b = 0") |
170 assume "b = 0" |
174 assume "b = 0" |
188 also have "\<dots> = a mod b" |
192 also have "\<dots> = a mod b" |
189 by (simp only: mod_div_equality') |
193 by (simp only: mod_div_equality') |
190 finally show ?thesis . |
194 finally show ?thesis . |
191 qed |
195 qed |
192 |
196 |
193 lemma dvd_imp_mod_0: "a dvd b \<Longrightarrow> b mod a = 0" |
197 lemma dvd_div_mult_self [simp]: |
194 by (rule dvd_eq_mod_eq_0[THEN iffD1]) |
198 "a dvd b \<Longrightarrow> (b div a) * a = b" |
195 |
199 using mod_div_equality [of b a, symmetric] by simp |
196 lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b" |
200 |
197 by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0) |
201 lemma dvd_mult_div_cancel [simp]: |
198 |
202 "a dvd b \<Longrightarrow> a * (b div a) = b" |
199 lemma dvd_mult_div_cancel: "a dvd b \<Longrightarrow> a * (b div a) = b" |
203 using dvd_div_mult_self by (simp add: ac_simps) |
200 by (drule dvd_div_mult_self) (simp add: mult.commute) |
204 |
201 |
205 lemma dvd_div_mult: |
202 lemma dvd_div_mult: "a dvd b \<Longrightarrow> (b div a) * c = b * c div a" |
206 "a dvd b \<Longrightarrow> (b div a) * c = (b * c) div a" |
203 apply (cases "a = 0") |
207 by (cases "a = 0") (auto elim!: dvdE simp add: mult.assoc) |
204 apply simp |
208 |
205 apply (auto simp: dvd_def mult.assoc) |
209 lemma div_dvd_div [simp]: |
206 done |
210 assumes "a dvd b" and "a dvd c" |
207 |
211 shows "b div a dvd c div a \<longleftrightarrow> b dvd c" |
208 lemma div_dvd_div[simp]: |
212 using assms apply (cases "a = 0") |
209 "a dvd b \<Longrightarrow> a dvd c \<Longrightarrow> (b div a dvd c div a) = (b dvd c)" |
213 apply auto |
210 apply (cases "a = 0") |
|
211 apply simp |
|
212 apply (unfold dvd_def) |
214 apply (unfold dvd_def) |
213 apply auto |
215 apply auto |
214 apply(blast intro:mult.assoc[symmetric]) |
216 apply(blast intro:mult.assoc[symmetric]) |
215 apply(fastforce simp add: mult.assoc) |
217 apply(fastforce simp add: mult.assoc) |
216 done |
218 done |
217 |
219 |
218 lemma dvd_mod_imp_dvd: "[| k dvd m mod n; k dvd n |] ==> k dvd m" |
220 lemma dvd_mod_imp_dvd: |
219 apply (subgoal_tac "k dvd (m div n) *n + m mod n") |
221 assumes "k dvd m mod n" and "k dvd n" |
220 apply (simp add: mod_div_equality) |
222 shows "k dvd m" |
221 apply (simp only: dvd_add dvd_mult) |
223 proof - |
222 done |
224 from assms have "k dvd (m div n) * n + m mod n" |
|
225 by (simp only: dvd_add dvd_mult) |
|
226 then show ?thesis by (simp add: mod_div_equality) |
|
227 qed |
223 |
228 |
224 text {* Addition respects modular equivalence. *} |
229 text {* Addition respects modular equivalence. *} |
225 |
230 |
226 lemma mod_add_left_eq: "(a + b) mod c = (a mod c + b) mod c" |
231 lemma mod_add_left_eq: "(a + b) mod c = (a mod c + b) mod c" |
227 proof - |
232 proof - |
591 |
596 |
592 lemma even_two_times_div_two: |
597 lemma even_two_times_div_two: |
593 "even a \<Longrightarrow> 2 * (a div 2) = a" |
598 "even a \<Longrightarrow> 2 * (a div 2) = a" |
594 by (fact dvd_mult_div_cancel) |
599 by (fact dvd_mult_div_cancel) |
595 |
600 |
596 lemma odd_two_times_div_two_succ: |
601 lemma odd_two_times_div_two_succ [simp]: |
597 "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a" |
602 "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a" |
598 using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero) |
603 using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero) |
599 |
604 |
600 end |
605 end |
601 |
606 |
1526 |
1531 |
1527 lemma odd_Suc_div_two [simp]: |
1532 lemma odd_Suc_div_two [simp]: |
1528 "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)" |
1533 "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)" |
1529 using odd_succ_div_two [of n] by simp |
1534 using odd_succ_div_two [of n] by simp |
1530 |
1535 |
1531 lemma odd_two_times_div_two_Suc: |
1536 lemma odd_two_times_div_two_nat [simp]: |
1532 "odd n \<Longrightarrow> Suc (2 * (n div 2)) = n" |
1537 "odd n \<Longrightarrow> 2 * (n div 2) = n - (1 :: nat)" |
1533 using odd_two_times_div_two_succ [of n] by simp |
1538 using odd_two_times_div_two_succ [of n] by simp |
|
1539 |
|
1540 lemma odd_Suc_minus_one [simp]: |
|
1541 "odd n \<Longrightarrow> Suc (n - Suc 0) = n" |
|
1542 by (auto elim: oddE) |
1534 |
1543 |
1535 lemma parity_induct [case_names zero even odd]: |
1544 lemma parity_induct [case_names zero even odd]: |
1536 assumes zero: "P 0" |
1545 assumes zero: "P 0" |
1537 assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)" |
1546 assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)" |
1538 assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))" |
1547 assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))" |