1(* Title: HOL/Parity.thy 2 Author: Jeremy Avigad 3 Author: Jacques D. Fleuriot 4*) 5 6section \<open>Parity in rings and semirings\<close> 7 8theory Parity 9 imports Euclidean_Division 10begin 11 12subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close> 13 14class semiring_parity = semidom + semiring_char_0 + unique_euclidean_semiring + 15 assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n" 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" 18begin 19 20lemma 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 25lemma euclidean_size_of_nat [simp]: 26 "euclidean_size (of_nat n) = n" 27proof - 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 31qed 32 33lemma of_nat_euclidean_size: 34 "of_nat (euclidean_size a) = a div division_segment a" 35proof - 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 . 41qed 42 43lemma division_segment_1 [simp]: 44 "division_segment 1 = 1" 45 using division_segment_of_nat [of 1] by simp 46 47lemma division_segment_numeral [simp]: 48 "division_segment (numeral k) = 1" 49 using division_segment_of_nat [of "numeral k"] by simp 50 51lemma euclidean_size_1 [simp]: 52 "euclidean_size 1 = 1" 53 using euclidean_size_of_nat [of 1] by simp 54 55lemma euclidean_size_numeral [simp]: 56 "euclidean_size (numeral k) = numeral k" 57 using euclidean_size_of_nat [of "numeral k"] by simp 58 59lemma of_nat_dvd_iff: 60 "of_nat m dvd of_nat n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q") 61proof (cases "m = 0") 62 case True 63 then show ?thesis 64 by simp 65next 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 84qed 85 86lemma of_nat_mod: 87 "of_nat (m mod n) = of_nat m mod of_nat n" 88proof - 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 95qed 96 97lemma one_div_two_eq_zero [simp]: 98 "1 div 2 = 0" 99proof - 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 104qed 105 106lemma one_mod_two_eq_one [simp]: 107 "1 mod 2 = 1" 108proof - 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 113qed 114 115abbreviation even :: "'a \<Rightarrow> bool" 116 where "even a \<equiv> 2 dvd a" 117 118abbreviation odd :: "'a \<Rightarrow> bool" 119 where "odd a \<equiv> \<not> 2 dvd a" 120 121lemma even_iff_mod_2_eq_zero: 122 "even a \<longleftrightarrow> a mod 2 = 0" 123 by (fact dvd_eq_mod_eq_0) 124 125lemma odd_iff_mod_2_eq_one: 126 "odd a \<longleftrightarrow> a mod 2 = 1" 127proof 128 assume "a mod 2 = 1" 129 then show "odd a" 130 by auto 131next 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)" 138 using \<open>odd a\<close> by (simp add: Suc_le_eq dvd_eq_mod_eq_0) 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) 155qed 156 157lemma 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 163lemma 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 167lemma 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 170 171lemma evenE [elim?]: 172 assumes "even a" 173 obtains b where "a = 2 * b" 174 using assms by (rule dvdE) 175 176lemma oddE [elim?]: 177 assumes "odd a" 178 obtains b where "a = 2 * b + 1" 179proof - 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 .. 185qed 186 187lemma mod_2_eq_odd: 188 "a mod 2 = of_bool (odd a)" 189 by (auto elim: oddE) 190 191lemma of_bool_odd_eq_mod_2: 192 "of_bool (odd a) = a mod 2" 193 by (simp add: mod_2_eq_odd) 194 195lemma one_mod_2_pow_eq [simp]: 196 "1 mod (2 ^ n) = of_bool (n > 0)" 197proof - 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)" 201 by simp 202 finally show ?thesis . 203qed 204 205lemma 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 209lemma even_of_nat [simp]: 210 "even (of_nat a) \<longleftrightarrow> even a" 211proof - 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 . 217qed 218 219lemma even_zero [simp]: 220 "even 0" 221 by (fact dvd_0_right) 222 223lemma odd_one [simp]: 224 "odd 1" 225proof - 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 232qed 233 234lemma odd_even_add: 235 "even (a + b)" if "odd a" and "odd b" 236proof - 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 .. 244qed 245 246lemma 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 250lemma odd_add [simp]: 251 "odd (a + b) \<longleftrightarrow> \<not> (odd a \<longleftrightarrow> odd b)" 252 by simp 253 254lemma 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 258lemma even_mult_iff [simp]: 259 "even (a * b) \<longleftrightarrow> even a \<or> even b" (is "?P \<longleftrightarrow> ?Q") 260proof 261 assume ?Q 262 then show ?P 263 by auto 264next 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 282qed 283 284lemma even_numeral [simp]: "even (numeral (Num.Bit0 n))" 285proof - 286 have "even (2 * numeral n)" 287 unfolding even_mult_iff by simp 288 then have "even (numeral n + numeral n)" 289 unfolding mult_2 . 290 then show ?thesis 291 unfolding numeral.simps . 292qed 293 294lemma odd_numeral [simp]: "odd (numeral (Num.Bit1 n))" 295proof 296 assume "even (numeral (num.Bit1 n))" 297 then have "even (numeral n + numeral n + 1)" 298 unfolding numeral.simps . 299 then have "even (2 * numeral n + 1)" 300 unfolding mult_2 . 301 then have "2 dvd numeral n * 2 + 1" 302 by (simp add: ac_simps) 303 then have "2 dvd 1" 304 using dvd_add_times_triv_left_iff [of 2 "numeral n" 1] by simp 305 then show False by simp 306qed 307 308lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0" 309 by (induct n) auto 310 311lemma 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 315lemma 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 319lemma even_two_times_div_two: 320 "even a \<Longrightarrow> 2 * (a div 2) = a" 321 by (fact dvd_mult_div_cancel) 322 323lemma 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 328lemma coprime_left_2_iff_odd [simp]: 329 "coprime 2 a \<longleftrightarrow> odd a" 330proof 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 341next 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 354qed 355 356lemma 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 360lemma div_mult2_eq': 361 "a div (of_nat m * of_nat n) = a div of_nat m div of_nat n" 362proof (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) 367next 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 have "a mod (of_nat m * of_nat n) div (of_nat m * of_nat n) = 0" 375 by simp 376 with remainder(6) have "r div (of_nat m * of_nat n) = 0" 377 by simp 378 with \<open>of_nat (euclidean_size r) = r\<close> 379 have "of_nat (euclidean_size r) div (of_nat m * of_nat n) = 0" 380 by simp 381 then have "of_nat (euclidean_size r div (m * n)) = 0" 382 by (simp add: of_nat_div) 383 then have "of_nat (euclidean_size r div m div n) = 0" 384 by (simp add: div_mult2_eq) 385 with \<open>of_nat (euclidean_size r) = r\<close> have "r div of_nat m div of_nat n = 0" 386 by (simp add: of_nat_div) 387 with remainder(1) 388 have "q = (r div of_nat m + q * of_nat n * of_nat m div of_nat m) div of_nat n" 389 by simp 390 with remainder(5) remainder(7) show ?thesis 391 using div_plus_div_distrib_dvd_right [of "of_nat m" "q * (of_nat m * of_nat n)" r] 392 by (simp add: ac_simps) 393next 394 case by0 395 then show ?thesis 396 by auto 397qed 398 399lemma mod_mult2_eq': 400 "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" 401proof - 402 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)" 403 by (simp add: combine_common_factor div_mult_mod_eq) 404 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)" 405 by (simp add: ac_simps) 406 ultimately show ?thesis 407 by (simp add: div_mult2_eq' mult_commute) 408qed 409 410lemma div_mult2_numeral_eq: 411 "a div numeral k div numeral l = a div numeral (k * l)" (is "?A = ?B") 412proof - 413 have "?A = a div of_nat (numeral k) div of_nat (numeral l)" 414 by simp 415 also have "\<dots> = a div (of_nat (numeral k) * of_nat (numeral l))" 416 by (fact div_mult2_eq' [symmetric]) 417 also have "\<dots> = ?B" 418 by simp 419 finally show ?thesis . 420qed 421 422end 423 424class ring_parity = ring + semiring_parity 425begin 426 427subclass comm_ring_1 .. 428 429lemma even_minus: 430 "even (- a) \<longleftrightarrow> even a" 431 by (fact dvd_minus_iff) 432 433lemma even_diff [simp]: 434 "even (a - b) \<longleftrightarrow> even (a + b)" 435 using even_add [of a "- b"] by simp 436 437lemma minus_1_mod_2_eq [simp]: 438 "- 1 mod 2 = 1" 439 by (simp add: mod_2_eq_odd) 440 441lemma minus_1_div_2_eq [simp]: 442 "- 1 div 2 = - 1" 443proof - 444 from div_mult_mod_eq [of "- 1" 2] 445 have "- 1 div 2 * 2 = - 1 * 2" 446 using local.add_implies_diff by fastforce 447 then show ?thesis 448 using mult_right_cancel [of 2 "- 1 div 2" "- 1"] by simp 449qed 450 451end 452 453 454subsection \<open>Instance for @{typ nat}\<close> 455 456instance nat :: semiring_parity 457 by standard (simp_all add: dvd_eq_mod_eq_0) 458 459lemma even_Suc_Suc_iff [simp]: 460 "even (Suc (Suc n)) \<longleftrightarrow> even n" 461 using dvd_add_triv_right_iff [of 2 n] by simp 462 463lemma even_Suc [simp]: "even (Suc n) \<longleftrightarrow> odd n" 464 using even_plus_one_iff [of n] by simp 465 466lemma even_diff_nat [simp]: 467 "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)" for m n :: nat 468proof (cases "n \<le> m") 469 case True 470 then have "m - n + n * 2 = m + n" by (simp add: mult_2_right) 471 moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp 472 ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:) 473 then show ?thesis by auto 474next 475 case False 476 then show ?thesis by simp 477qed 478 479lemma odd_pos: 480 "odd n \<Longrightarrow> 0 < n" for n :: nat 481 by (auto elim: oddE) 482 483lemma Suc_double_not_eq_double: 484 "Suc (2 * m) \<noteq> 2 * n" 485proof 486 assume "Suc (2 * m) = 2 * n" 487 moreover have "odd (Suc (2 * m))" and "even (2 * n)" 488 by simp_all 489 ultimately show False by simp 490qed 491 492lemma double_not_eq_Suc_double: 493 "2 * m \<noteq> Suc (2 * n)" 494 using Suc_double_not_eq_double [of n m] by simp 495 496lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n" 497 by (auto elim: oddE) 498 499lemma even_Suc_div_two [simp]: 500 "even n \<Longrightarrow> Suc n div 2 = n div 2" 501 using even_succ_div_two [of n] by simp 502 503lemma odd_Suc_div_two [simp]: 504 "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)" 505 using odd_succ_div_two [of n] by simp 506 507lemma odd_two_times_div_two_nat [simp]: 508 assumes "odd n" 509 shows "2 * (n div 2) = n - (1 :: nat)" 510proof - 511 from assms have "2 * (n div 2) + 1 = n" 512 by (rule odd_two_times_div_two_succ) 513 then have "Suc (2 * (n div 2)) - 1 = n - 1" 514 by simp 515 then show ?thesis 516 by simp 517qed 518 519lemma parity_induct [case_names zero even odd]: 520 assumes zero: "P 0" 521 assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)" 522 assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))" 523 shows "P n" 524proof (induct n rule: less_induct) 525 case (less n) 526 show "P n" 527 proof (cases "n = 0") 528 case True with zero show ?thesis by simp 529 next 530 case False 531 with less have hyp: "P (n div 2)" by simp 532 show ?thesis 533 proof (cases "even n") 534 case True 535 with hyp even [of "n div 2"] show ?thesis 536 by simp 537 next 538 case False 539 with hyp odd [of "n div 2"] show ?thesis 540 by simp 541 qed 542 qed 543qed 544 545lemma not_mod2_eq_Suc_0_eq_0 [simp]: 546 "n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0" 547 using not_mod_2_eq_1_eq_0 [of n] by simp 548 549 550subsection \<open>Parity and powers\<close> 551 552context ring_1 553begin 554 555lemma power_minus_even [simp]: "even n \<Longrightarrow> (- a) ^ n = a ^ n" 556 by (auto elim: evenE) 557 558lemma power_minus_odd [simp]: "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)" 559 by (auto elim: oddE) 560 561lemma uminus_power_if: 562 "(- a) ^ n = (if even n then a ^ n else - (a ^ n))" 563 by auto 564 565lemma neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1" 566 by simp 567 568lemma neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1" 569 by simp 570 571lemma neg_one_power_add_eq_neg_one_power_diff: "k \<le> n \<Longrightarrow> (- 1) ^ (n + k) = (- 1) ^ (n - k)" 572 by (cases "even (n + k)") auto 573 574lemma minus_one_power_iff: "(- 1) ^ n = (if even n then 1 else - 1)" 575 by (induct n) auto 576 577end 578 579context linordered_idom 580begin 581 582lemma zero_le_even_power: "even n \<Longrightarrow> 0 \<le> a ^ n" 583 by (auto elim: evenE) 584 585lemma zero_le_odd_power: "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a" 586 by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE) 587 588lemma zero_le_power_eq: "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a" 589 by (auto simp add: zero_le_even_power zero_le_odd_power) 590 591lemma zero_less_power_eq: "0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a" 592proof - 593 have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0" 594 unfolding power_eq_0_iff [of a n, symmetric] by blast 595 show ?thesis 596 unfolding less_le zero_le_power_eq by auto 597qed 598 599lemma power_less_zero_eq [simp]: "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0" 600 unfolding not_le [symmetric] zero_le_power_eq by auto 601 602lemma power_le_zero_eq: "a ^ n \<le> 0 \<longleftrightarrow> n > 0 \<and> (odd n \<and> a \<le> 0 \<or> even n \<and> a = 0)" 603 unfolding not_less [symmetric] zero_less_power_eq by auto 604 605lemma power_even_abs: "even n \<Longrightarrow> \<bar>a\<bar> ^ n = a ^ n" 606 using power_abs [of a n] by (simp add: zero_le_even_power) 607 608lemma power_mono_even: 609 assumes "even n" and "\<bar>a\<bar> \<le> \<bar>b\<bar>" 610 shows "a ^ n \<le> b ^ n" 611proof - 612 have "0 \<le> \<bar>a\<bar>" by auto 613 with \<open>\<bar>a\<bar> \<le> \<bar>b\<bar>\<close> have "\<bar>a\<bar> ^ n \<le> \<bar>b\<bar> ^ n" 614 by (rule power_mono) 615 with \<open>even n\<close> show ?thesis 616 by (simp add: power_even_abs) 617qed 618 619lemma power_mono_odd: 620 assumes "odd n" and "a \<le> b" 621 shows "a ^ n \<le> b ^ n" 622proof (cases "b < 0") 623 case True 624 with \<open>a \<le> b\<close> have "- b \<le> - a" and "0 \<le> - b" by auto 625 then have "(- b) ^ n \<le> (- a) ^ n" by (rule power_mono) 626 with \<open>odd n\<close> show ?thesis by simp 627next 628 case False 629 then have "0 \<le> b" by auto 630 show ?thesis 631 proof (cases "a < 0") 632 case True 633 then have "n \<noteq> 0" and "a \<le> 0" using \<open>odd n\<close> [THEN odd_pos] by auto 634 then have "a ^ n \<le> 0" unfolding power_le_zero_eq using \<open>odd n\<close> by auto 635 moreover from \<open>0 \<le> b\<close> have "0 \<le> b ^ n" by auto 636 ultimately show ?thesis by auto 637 next 638 case False 639 then have "0 \<le> a" by auto 640 with \<open>a \<le> b\<close> show ?thesis 641 using power_mono by auto 642 qed 643qed 644 645text \<open>Simplify, when the exponent is a numeral\<close> 646 647lemma zero_le_power_eq_numeral [simp]: 648 "0 \<le> a ^ numeral w \<longleftrightarrow> even (numeral w :: nat) \<or> odd (numeral w :: nat) \<and> 0 \<le> a" 649 by (fact zero_le_power_eq) 650 651lemma zero_less_power_eq_numeral [simp]: 652 "0 < a ^ numeral w \<longleftrightarrow> 653 numeral w = (0 :: nat) \<or> 654 even (numeral w :: nat) \<and> a \<noteq> 0 \<or> 655 odd (numeral w :: nat) \<and> 0 < a" 656 by (fact zero_less_power_eq) 657 658lemma power_le_zero_eq_numeral [simp]: 659 "a ^ numeral w \<le> 0 \<longleftrightarrow> 660 (0 :: nat) < numeral w \<and> 661 (odd (numeral w :: nat) \<and> a \<le> 0 \<or> even (numeral w :: nat) \<and> a = 0)" 662 by (fact power_le_zero_eq) 663 664lemma power_less_zero_eq_numeral [simp]: 665 "a ^ numeral w < 0 \<longleftrightarrow> odd (numeral w :: nat) \<and> a < 0" 666 by (fact power_less_zero_eq) 667 668lemma power_even_abs_numeral [simp]: 669 "even (numeral w :: nat) \<Longrightarrow> \<bar>a\<bar> ^ numeral w = a ^ numeral w" 670 by (fact power_even_abs) 671 672end 673 674 675subsection \<open>Instance for @{typ int}\<close> 676 677instance int :: ring_parity 678 by standard (simp_all add: dvd_eq_mod_eq_0 divide_int_def division_segment_int_def) 679 680lemma even_diff_iff: 681 "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int 682 by (fact even_diff) 683 684lemma even_abs_add_iff: 685 "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int 686 by simp 687 688lemma even_add_abs_iff: 689 "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int 690 by simp 691 692lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k" 693 by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric]) 694 695 696subsection \<open>Abstract bit operations\<close> 697 698context semiring_parity 699begin 700 701text \<open>The primary purpose of the following operations is 702 to avoid ad-hoc simplification of concrete expressions @{term "2 ^ n"}\<close> 703 704definition push_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" 705 where push_bit_eq_mult: "push_bit n a = a * 2 ^ n" 706 707definition take_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" 708 where take_bit_eq_mod: "take_bit n a = a mod 2 ^ n" 709 710definition drop_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" 711 where drop_bit_eq_div: "drop_bit n a = a div 2 ^ n" 712 713lemma bit_ident: 714 "push_bit n (drop_bit n a) + take_bit n a = a" 715 using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div) 716 717lemma push_bit_push_bit [simp]: 718 "push_bit m (push_bit n a) = push_bit (m + n) a" 719 by (simp add: push_bit_eq_mult power_add ac_simps) 720 721lemma take_bit_take_bit [simp]: 722 "take_bit m (take_bit n a) = take_bit (min m n) a" 723proof (cases "m \<le> n") 724 case True 725 then show ?thesis 726 by (simp add: take_bit_eq_mod not_le min_def mod_mod_cancel le_imp_power_dvd) 727next 728 case False 729 then have "n < m" and "min m n = n" 730 by simp_all 731 then have "2 ^ m = of_nat (2 ^ n) * of_nat (2 ^ (m - n))" 732 by (simp add: power_add [symmetric]) 733 then have "a mod 2 ^ n mod 2 ^ m = a mod 2 ^ n mod (of_nat (2 ^ n) * of_nat (2 ^ (m - n)))" 734 by simp 735 also have "\<dots> = of_nat (2 ^ n) * (a mod 2 ^ n div of_nat (2 ^ n) mod of_nat (2 ^ (m - n))) + a mod 2 ^ n mod of_nat (2 ^ n)" 736 by (simp only: mod_mult2_eq') 737 finally show ?thesis 738 using \<open>min m n = n\<close> by (simp add: take_bit_eq_mod) 739qed 740 741lemma drop_bit_drop_bit [simp]: 742 "drop_bit m (drop_bit n a) = drop_bit (m + n) a" 743proof - 744 have "a div (2 ^ m * 2 ^ n) = a div (of_nat (2 ^ n) * of_nat (2 ^ m))" 745 by (simp add: ac_simps) 746 also have "\<dots> = a div of_nat (2 ^ n) div of_nat (2 ^ m)" 747 by (simp only: div_mult2_eq') 748 finally show ?thesis 749 by (simp add: drop_bit_eq_div power_add) 750qed 751 752lemma push_bit_take_bit: 753 "push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)" 754 by (simp add: push_bit_eq_mult take_bit_eq_mod power_add mult_mod_right ac_simps) 755 756lemma take_bit_push_bit: 757 "take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)" 758proof (cases "m \<le> n") 759 case True 760 then show ?thesis 761 by (simp_all add: push_bit_eq_mult take_bit_eq_mod mod_eq_0_iff_dvd dvd_power_le) 762next 763 case False 764 then show ?thesis 765 using push_bit_take_bit [of n "m - n" a] 766 by simp 767qed 768 769lemma take_bit_drop_bit: 770 "take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)" 771 using mod_mult2_eq' [of a "2 ^ n" "2 ^ m"] 772 by (simp add: drop_bit_eq_div take_bit_eq_mod power_add ac_simps) 773 774lemma drop_bit_take_bit: 775 "drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)" 776proof (cases "m \<le> n") 777 case True 778 then show ?thesis 779 using take_bit_drop_bit [of "n - m" m a] by simp 780next 781 case False 782 then have "a mod 2 ^ n div 2 ^ m = a mod 2 ^ n div 2 ^ (n + (m - n))" 783 by simp 784 also have "\<dots> = a mod 2 ^ n div (2 ^ n * 2 ^ (m - n))" 785 by (simp add: power_add) 786 also have "\<dots> = a mod 2 ^ n div (of_nat (2 ^ n) * of_nat (2 ^ (m - n)))" 787 by simp 788 also have "\<dots> = a mod 2 ^ n div of_nat (2 ^ n) div of_nat (2 ^ (m - n))" 789 by (simp only: div_mult2_eq') 790 finally show ?thesis 791 using False by (simp add: take_bit_eq_mod drop_bit_eq_div) 792qed 793 794lemma push_bit_0_id [simp]: 795 "push_bit 0 = id" 796 by (simp add: fun_eq_iff push_bit_eq_mult) 797 798lemma push_bit_of_0 [simp]: 799 "push_bit n 0 = 0" 800 by (simp add: push_bit_eq_mult) 801 802lemma push_bit_of_1: 803 "push_bit n 1 = 2 ^ n" 804 by (simp add: push_bit_eq_mult) 805 806lemma push_bit_Suc [simp]: 807 "push_bit (Suc n) a = push_bit n (a * 2)" 808 by (simp add: push_bit_eq_mult ac_simps) 809 810lemma push_bit_double: 811 "push_bit n (a * 2) = push_bit n a * 2" 812 by (simp add: push_bit_eq_mult ac_simps) 813 814lemma push_bit_eq_0_iff [simp]: 815 "push_bit n a = 0 \<longleftrightarrow> a = 0" 816 by (simp add: push_bit_eq_mult) 817 818lemma push_bit_add: 819 "push_bit n (a + b) = push_bit n a + push_bit n b" 820 by (simp add: push_bit_eq_mult algebra_simps) 821 822lemma push_bit_numeral [simp]: 823 "push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))" 824 by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric]) (simp add: ac_simps) 825 826lemma push_bit_of_nat: 827 "push_bit n (of_nat m) = of_nat (push_bit n m)" 828 by (simp add: push_bit_eq_mult Parity.push_bit_eq_mult) 829 830lemma take_bit_0 [simp]: 831 "take_bit 0 a = 0" 832 by (simp add: take_bit_eq_mod) 833 834lemma take_bit_Suc [simp]: 835 "take_bit (Suc n) a = take_bit n (a div 2) * 2 + of_bool (odd a)" 836proof - 837 have "1 + 2 * (a div 2) mod (2 * 2 ^ n) = (a div 2 * 2 + a mod 2) mod (2 * 2 ^ n)" 838 if "odd a" 839 using that mod_mult2_eq' [of "1 + 2 * (a div 2)" 2 "2 ^ n"] 840 by (simp add: ac_simps odd_iff_mod_2_eq_one mult_mod_right) 841 also have "\<dots> = a mod (2 * 2 ^ n)" 842 by (simp only: div_mult_mod_eq) 843 finally show ?thesis 844 by (simp add: take_bit_eq_mod algebra_simps mult_mod_right) 845qed 846 847lemma take_bit_of_0 [simp]: 848 "take_bit n 0 = 0" 849 by (simp add: take_bit_eq_mod) 850 851lemma take_bit_of_1 [simp]: 852 "take_bit n 1 = of_bool (n > 0)" 853 by (simp add: take_bit_eq_mod) 854 855lemma take_bit_add: 856 "take_bit n (take_bit n a + take_bit n b) = take_bit n (a + b)" 857 by (simp add: take_bit_eq_mod mod_simps) 858 859lemma take_bit_eq_0_iff: 860 "take_bit n a = 0 \<longleftrightarrow> 2 ^ n dvd a" 861 by (simp add: take_bit_eq_mod mod_eq_0_iff_dvd) 862 863lemma take_bit_of_1_eq_0_iff [simp]: 864 "take_bit n 1 = 0 \<longleftrightarrow> n = 0" 865 by (simp add: take_bit_eq_mod) 866 867lemma even_take_bit_eq [simp]: 868 "even (take_bit n a) \<longleftrightarrow> n = 0 \<or> even a" 869 by (cases n) (simp_all add: take_bit_eq_mod dvd_mod_iff) 870 871lemma take_bit_numeral_bit0 [simp]: 872 "take_bit (numeral l) (numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (numeral k) * 2" 873 by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric] take_bit_Suc 874 ac_simps even_mult_iff nonzero_mult_div_cancel_right [OF numeral_neq_zero]) simp 875 876lemma take_bit_numeral_bit1 [simp]: 877 "take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1" 878 by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] take_bit_Suc 879 ac_simps even_add even_mult_iff div_mult_self1 [OF numeral_neq_zero]) (simp add: ac_simps) 880 881lemma take_bit_of_nat: 882 "take_bit n (of_nat m) = of_nat (take_bit n m)" 883 by (simp add: take_bit_eq_mod Parity.take_bit_eq_mod of_nat_mod [of m "2 ^ n"]) 884 885lemma drop_bit_0 [simp]: 886 "drop_bit 0 = id" 887 by (simp add: fun_eq_iff drop_bit_eq_div) 888 889lemma drop_bit_of_0 [simp]: 890 "drop_bit n 0 = 0" 891 by (simp add: drop_bit_eq_div) 892 893lemma drop_bit_of_1 [simp]: 894 "drop_bit n 1 = of_bool (n = 0)" 895 by (simp add: drop_bit_eq_div) 896 897lemma drop_bit_Suc [simp]: 898 "drop_bit (Suc n) a = drop_bit n (a div 2)" 899proof (cases "even a") 900 case True 901 then obtain b where "a = 2 * b" .. 902 moreover have "drop_bit (Suc n) (2 * b) = drop_bit n b" 903 by (simp add: drop_bit_eq_div) 904 ultimately show ?thesis 905 by simp 906next 907 case False 908 then obtain b where "a = 2 * b + 1" .. 909 moreover have "drop_bit (Suc n) (2 * b + 1) = drop_bit n b" 910 using div_mult2_eq' [of "1 + b * 2" 2 "2 ^ n"] 911 by (auto simp add: drop_bit_eq_div ac_simps) 912 ultimately show ?thesis 913 by simp 914qed 915 916lemma drop_bit_half: 917 "drop_bit n (a div 2) = drop_bit n a div 2" 918 by (induction n arbitrary: a) simp_all 919 920lemma drop_bit_of_bool [simp]: 921 "drop_bit n (of_bool d) = of_bool (n = 0 \<and> d)" 922 by (cases n) simp_all 923 924lemma drop_bit_numeral_bit0 [simp]: 925 "drop_bit (numeral l) (numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (numeral k)" 926 by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric] drop_bit_Suc 927 nonzero_mult_div_cancel_left [OF numeral_neq_zero]) 928 929lemma drop_bit_numeral_bit1 [simp]: 930 "drop_bit (numeral l) (numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (numeral k)" 931 by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] drop_bit_Suc 932 div_mult_self4 [OF numeral_neq_zero]) simp 933 934lemma drop_bit_of_nat: 935 "drop_bit n (of_nat m) = of_nat (drop_bit n m)" 936 by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"]) 937 938end 939 940lemma push_bit_of_Suc_0 [simp]: 941 "push_bit n (Suc 0) = 2 ^ n" 942 using push_bit_of_1 [where ?'a = nat] by simp 943 944lemma take_bit_of_Suc_0 [simp]: 945 "take_bit n (Suc 0) = of_bool (0 < n)" 946 using take_bit_of_1 [where ?'a = nat] by simp 947 948lemma drop_bit_of_Suc_0 [simp]: 949 "drop_bit n (Suc 0) = of_bool (n = 0)" 950 using drop_bit_of_1 [where ?'a = nat] by simp 951 952end 953