2269 by (simp add: algebra_simps mult_2_right) |
2269 by (simp add: algebra_simps mult_2_right) |
2270 finally show ?case . |
2270 finally show ?case . |
2271 qed |
2271 qed |
2272 |
2272 |
2273 lemma Sum_Icc_nat: |
2273 lemma Sum_Icc_nat: |
2274 "\<Sum>{m..n} = (n * (n + 1) - m * (m - 1)) div 2" |
2274 "\<Sum>{m..n} = (n * (n + 1) - m * (m - 1)) div 2" for m n :: nat |
2275 if "m \<le> n" for m n :: nat |
2275 proof (cases "m \<le> n") |
2276 proof - |
2276 case True |
2277 have *: "m * (m - 1) \<le> n * (n + 1)" |
2277 then have *: "m * (m - 1) \<le> n * (n + 1)" |
2278 using that by (meson diff_le_self order_trans le_add1 mult_le_mono) |
2278 by (meson diff_le_self order_trans le_add1 mult_le_mono) |
2279 have "int (\<Sum>{m..n}) = (\<Sum>{int m..int n})" |
2279 have "int (\<Sum>{m..n}) = (\<Sum>{int m..int n})" |
2280 by (simp add: sum.atLeast_int_atMost_int_shift) |
2280 by (simp add: sum.atLeast_int_atMost_int_shift) |
2281 also have "\<dots> = (int n * (int n + 1) - int m * (int m - 1)) div 2" |
2281 also have "\<dots> = (int n * (int n + 1) - int m * (int m - 1)) div 2" |
2282 using that by (simp add: Sum_Icc_int) |
2282 using \<open>m \<le> n\<close> by (simp add: Sum_Icc_int) |
2283 also have "\<dots> = int ((n * (n + 1) - m * (m - 1)) div 2)" |
2283 also have "\<dots> = int ((n * (n + 1) - m * (m - 1)) div 2)" |
2284 using le_square * by (simp add: algebra_simps of_nat_div of_nat_diff) |
2284 using le_square * by (simp add: algebra_simps of_nat_div of_nat_diff) |
2285 finally show ?thesis |
2285 finally show ?thesis |
2286 by (simp only: of_nat_eq_iff) |
2286 by (simp only: of_nat_eq_iff) |
|
2287 next |
|
2288 case False |
|
2289 then show ?thesis |
|
2290 by (auto dest: less_imp_Suc_add simp add: not_le algebra_simps) |
2287 qed |
2291 qed |
2288 |
2292 |
2289 lemma Sum_Ico_nat: |
2293 lemma Sum_Ico_nat: |
2290 "\<Sum>{m..<n} = (n * (n - 1) - m * (m - 1)) div 2" |
2294 "\<Sum>{m..<n} = (n * (n - 1) - m * (m - 1)) div 2" for m n :: nat |
2291 if "m \<le> n" for m n :: nat |
2295 by (cases n) (simp_all add: atLeastLessThanSuc_atLeastAtMost Sum_Icc_nat) |
2292 proof - |
|
2293 from that consider "m < n" | "m = n" |
|
2294 by (auto simp add: less_le) |
|
2295 then show ?thesis proof cases |
|
2296 case 1 |
|
2297 then have "{m..<n} = {m..n - 1}" |
|
2298 by auto |
|
2299 then have "\<Sum>{m..<n} = \<Sum>{m..n - 1}" |
|
2300 by simp |
|
2301 also have "\<dots> = (n * (n - 1) - m * (m - 1)) div 2" |
|
2302 using \<open>m < n\<close> by (simp add: Sum_Icc_nat mult.commute) |
|
2303 finally show ?thesis . |
|
2304 next |
|
2305 case 2 |
|
2306 then show ?thesis |
|
2307 by simp |
|
2308 qed |
|
2309 qed |
|
2310 |
2296 |
2311 |
2297 |
2312 subsubsection \<open>Division remainder\<close> |
2298 subsubsection \<open>Division remainder\<close> |
2313 |
2299 |
2314 lemma range_mod: |
2300 lemma range_mod: |