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 = comm_semiring_1 + semiring_modulo + 15 assumes even_iff_mod_2_eq_zero: "2 dvd a \<longleftrightarrow> a mod 2 = 0" 16 and odd_iff_mod_2_eq_one: "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1" 17 and odd_one [simp]: "\<not> 2 dvd 1" 18begin 19 20abbreviation even :: "'a \<Rightarrow> bool" 21 where "even a \<equiv> 2 dvd a" 22 23abbreviation odd :: "'a \<Rightarrow> bool" 24 where "odd a \<equiv> \<not> 2 dvd a" 25 26lemma parity_cases [case_names even odd]: 27 assumes "even a \<Longrightarrow> a mod 2 = 0 \<Longrightarrow> P" 28 assumes "odd a \<Longrightarrow> a mod 2 = 1 \<Longrightarrow> P" 29 shows P 30 using assms by (cases "even a") 31 (simp_all add: even_iff_mod_2_eq_zero [symmetric] odd_iff_mod_2_eq_one [symmetric]) 32 33lemma odd_of_bool_self [simp]: 34 \<open>odd (of_bool p) \<longleftrightarrow> p\<close> 35 by (cases p) simp_all 36 37lemma not_mod_2_eq_0_eq_1 [simp]: 38 "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1" 39 by (cases a rule: parity_cases) simp_all 40 41lemma not_mod_2_eq_1_eq_0 [simp]: 42 "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0" 43 by (cases a rule: parity_cases) simp_all 44 45lemma evenE [elim?]: 46 assumes "even a" 47 obtains b where "a = 2 * b" 48 using assms by (rule dvdE) 49 50lemma oddE [elim?]: 51 assumes "odd a" 52 obtains b where "a = 2 * b + 1" 53proof - 54 have "a = 2 * (a div 2) + a mod 2" 55 by (simp add: mult_div_mod_eq) 56 with assms have "a = 2 * (a div 2) + 1" 57 by (simp add: odd_iff_mod_2_eq_one) 58 then show ?thesis .. 59qed 60 61lemma mod_2_eq_odd: 62 "a mod 2 = of_bool (odd a)" 63 by (auto elim: oddE simp add: even_iff_mod_2_eq_zero) 64 65lemma of_bool_odd_eq_mod_2: 66 "of_bool (odd a) = a mod 2" 67 by (simp add: mod_2_eq_odd) 68 69lemma even_mod_2_iff [simp]: 70 \<open>even (a mod 2) \<longleftrightarrow> even a\<close> 71 by (simp add: mod_2_eq_odd) 72 73lemma mod2_eq_if: 74 "a mod 2 = (if even a then 0 else 1)" 75 by (simp add: mod_2_eq_odd) 76 77lemma even_zero [simp]: 78 "even 0" 79 by (fact dvd_0_right) 80 81lemma odd_even_add: 82 "even (a + b)" if "odd a" and "odd b" 83proof - 84 from that obtain c d where "a = 2 * c + 1" and "b = 2 * d + 1" 85 by (blast elim: oddE) 86 then have "a + b = 2 * c + 2 * d + (1 + 1)" 87 by (simp only: ac_simps) 88 also have "\<dots> = 2 * (c + d + 1)" 89 by (simp add: algebra_simps) 90 finally show ?thesis .. 91qed 92 93lemma even_add [simp]: 94 "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)" 95 by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add) 96 97lemma odd_add [simp]: 98 "odd (a + b) \<longleftrightarrow> \<not> (odd a \<longleftrightarrow> odd b)" 99 by simp 100 101lemma even_plus_one_iff [simp]: 102 "even (a + 1) \<longleftrightarrow> odd a" 103 by (auto simp add: dvd_add_right_iff intro: odd_even_add) 104 105lemma even_mult_iff [simp]: 106 "even (a * b) \<longleftrightarrow> even a \<or> even b" (is "?P \<longleftrightarrow> ?Q") 107proof 108 assume ?Q 109 then show ?P 110 by auto 111next 112 assume ?P 113 show ?Q 114 proof (rule ccontr) 115 assume "\<not> (even a \<or> even b)" 116 then have "odd a" and "odd b" 117 by auto 118 then obtain r s where "a = 2 * r + 1" and "b = 2 * s + 1" 119 by (blast elim: oddE) 120 then have "a * b = (2 * r + 1) * (2 * s + 1)" 121 by simp 122 also have "\<dots> = 2 * (2 * r * s + r + s) + 1" 123 by (simp add: algebra_simps) 124 finally have "odd (a * b)" 125 by simp 126 with \<open>?P\<close> show False 127 by auto 128 qed 129qed 130 131lemma even_numeral [simp]: "even (numeral (Num.Bit0 n))" 132proof - 133 have "even (2 * numeral n)" 134 unfolding even_mult_iff by simp 135 then have "even (numeral n + numeral n)" 136 unfolding mult_2 . 137 then show ?thesis 138 unfolding numeral.simps . 139qed 140 141lemma odd_numeral [simp]: "odd (numeral (Num.Bit1 n))" 142proof 143 assume "even (numeral (num.Bit1 n))" 144 then have "even (numeral n + numeral n + 1)" 145 unfolding numeral.simps . 146 then have "even (2 * numeral n + 1)" 147 unfolding mult_2 . 148 then have "2 dvd numeral n * 2 + 1" 149 by (simp add: ac_simps) 150 then have "2 dvd 1" 151 using dvd_add_times_triv_left_iff [of 2 "numeral n" 1] by simp 152 then show False by simp 153qed 154 155lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0" 156 by (induct n) auto 157 158lemma mask_eq_sum_exp: 159 \<open>2 ^ n - 1 = (\<Sum>m\<in>{q. q < n}. 2 ^ m)\<close> 160proof - 161 have *: \<open>{q. q < Suc m} = insert m {q. q < m}\<close> for m 162 by auto 163 have \<open>2 ^ n = (\<Sum>m\<in>{q. q < n}. 2 ^ m) + 1\<close> 164 by (induction n) (simp_all add: ac_simps mult_2 *) 165 then have \<open>2 ^ n - 1 = (\<Sum>m\<in>{q. q < n}. 2 ^ m) + 1 - 1\<close> 166 by simp 167 then show ?thesis 168 by simp 169qed 170 171lemma mask_eq_seq_sum: 172 \<open>2 ^ n - 1 = ((\<lambda>k. 1 + k * 2) ^^ n) 0\<close> 173proof - 174 have \<open>2 ^ n = ((\<lambda>k. 1 + k * 2) ^^ n) 0 + 1\<close> 175 by (induction n) (simp_all add: ac_simps mult_2) 176 then show ?thesis 177 by simp 178qed 179 180end 181 182class ring_parity = ring + semiring_parity 183begin 184 185subclass comm_ring_1 .. 186 187lemma even_minus: 188 "even (- a) \<longleftrightarrow> even a" 189 by (fact dvd_minus_iff) 190 191lemma even_diff [simp]: 192 "even (a - b) \<longleftrightarrow> even (a + b)" 193 using even_add [of a "- b"] by simp 194 195end 196 197 198subsection \<open>Special case: euclidean rings containing the natural numbers\<close> 199 200context unique_euclidean_semiring_with_nat 201begin 202 203subclass semiring_parity 204proof 205 show "2 dvd a \<longleftrightarrow> a mod 2 = 0" for a 206 by (fact dvd_eq_mod_eq_0) 207 show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1" for a 208 proof 209 assume "a mod 2 = 1" 210 then show "\<not> 2 dvd a" 211 by auto 212 next 213 assume "\<not> 2 dvd a" 214 have eucl: "euclidean_size (a mod 2) = 1" 215 proof (rule order_antisym) 216 show "euclidean_size (a mod 2) \<le> 1" 217 using mod_size_less [of 2 a] by simp 218 show "1 \<le> euclidean_size (a mod 2)" 219 using \<open>\<not> 2 dvd a\<close> by (simp add: Suc_le_eq dvd_eq_mod_eq_0) 220 qed 221 from \<open>\<not> 2 dvd a\<close> have "\<not> of_nat 2 dvd division_segment a * of_nat (euclidean_size a)" 222 by simp 223 then have "\<not> of_nat 2 dvd of_nat (euclidean_size a)" 224 by (auto simp only: dvd_mult_unit_iff' is_unit_division_segment) 225 then have "\<not> 2 dvd euclidean_size a" 226 using of_nat_dvd_iff [of 2] by simp 227 then have "euclidean_size a mod 2 = 1" 228 by (simp add: semidom_modulo_class.dvd_eq_mod_eq_0) 229 then have "of_nat (euclidean_size a mod 2) = of_nat 1" 230 by simp 231 then have "of_nat (euclidean_size a) mod 2 = 1" 232 by (simp add: of_nat_mod) 233 from \<open>\<not> 2 dvd a\<close> eucl 234 show "a mod 2 = 1" 235 by (auto intro: division_segment_eq_iff simp add: division_segment_mod) 236 qed 237 show "\<not> is_unit 2" 238 proof (rule notI) 239 assume "is_unit 2" 240 then have "of_nat 2 dvd of_nat 1" 241 by simp 242 then have "is_unit (2::nat)" 243 by (simp only: of_nat_dvd_iff) 244 then show False 245 by simp 246 qed 247qed 248 249lemma even_of_nat [simp]: 250 "even (of_nat a) \<longleftrightarrow> even a" 251proof - 252 have "even (of_nat a) \<longleftrightarrow> of_nat 2 dvd of_nat a" 253 by simp 254 also have "\<dots> \<longleftrightarrow> even a" 255 by (simp only: of_nat_dvd_iff) 256 finally show ?thesis . 257qed 258 259lemma even_succ_div_two [simp]: 260 "even a \<Longrightarrow> (a + 1) div 2 = a div 2" 261 by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero) 262 263lemma odd_succ_div_two [simp]: 264 "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1" 265 by (auto elim!: oddE simp add: add.assoc) 266 267lemma even_two_times_div_two: 268 "even a \<Longrightarrow> 2 * (a div 2) = a" 269 by (fact dvd_mult_div_cancel) 270 271lemma odd_two_times_div_two_succ [simp]: 272 "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a" 273 using mult_div_mod_eq [of 2 a] 274 by (simp add: even_iff_mod_2_eq_zero) 275 276lemma coprime_left_2_iff_odd [simp]: 277 "coprime 2 a \<longleftrightarrow> odd a" 278proof 279 assume "odd a" 280 show "coprime 2 a" 281 proof (rule coprimeI) 282 fix b 283 assume "b dvd 2" "b dvd a" 284 then have "b dvd a mod 2" 285 by (auto intro: dvd_mod) 286 with \<open>odd a\<close> show "is_unit b" 287 by (simp add: mod_2_eq_odd) 288 qed 289next 290 assume "coprime 2 a" 291 show "odd a" 292 proof (rule notI) 293 assume "even a" 294 then obtain b where "a = 2 * b" .. 295 with \<open>coprime 2 a\<close> have "coprime 2 (2 * b)" 296 by simp 297 moreover have "\<not> coprime 2 (2 * b)" 298 by (rule not_coprimeI [of 2]) simp_all 299 ultimately show False 300 by blast 301 qed 302qed 303 304lemma coprime_right_2_iff_odd [simp]: 305 "coprime a 2 \<longleftrightarrow> odd a" 306 using coprime_left_2_iff_odd [of a] by (simp add: ac_simps) 307 308end 309 310context unique_euclidean_ring_with_nat 311begin 312 313subclass ring_parity .. 314 315lemma minus_1_mod_2_eq [simp]: 316 "- 1 mod 2 = 1" 317 by (simp add: mod_2_eq_odd) 318 319lemma minus_1_div_2_eq [simp]: 320 "- 1 div 2 = - 1" 321proof - 322 from div_mult_mod_eq [of "- 1" 2] 323 have "- 1 div 2 * 2 = - 1 * 2" 324 using add_implies_diff by fastforce 325 then show ?thesis 326 using mult_right_cancel [of 2 "- 1 div 2" "- 1"] by simp 327qed 328 329end 330 331 332subsection \<open>Instance for \<^typ>\<open>nat\<close>\<close> 333 334instance nat :: unique_euclidean_semiring_with_nat 335 by standard (simp_all add: dvd_eq_mod_eq_0) 336 337lemma even_Suc_Suc_iff [simp]: 338 "even (Suc (Suc n)) \<longleftrightarrow> even n" 339 using dvd_add_triv_right_iff [of 2 n] by simp 340 341lemma even_Suc [simp]: "even (Suc n) \<longleftrightarrow> odd n" 342 using even_plus_one_iff [of n] by simp 343 344lemma even_diff_nat [simp]: 345 "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)" for m n :: nat 346proof (cases "n \<le> m") 347 case True 348 then have "m - n + n * 2 = m + n" by (simp add: mult_2_right) 349 moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp 350 ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:) 351 then show ?thesis by auto 352next 353 case False 354 then show ?thesis by simp 355qed 356 357lemma odd_pos: 358 "odd n \<Longrightarrow> 0 < n" for n :: nat 359 by (auto elim: oddE) 360 361lemma Suc_double_not_eq_double: 362 "Suc (2 * m) \<noteq> 2 * n" 363proof 364 assume "Suc (2 * m) = 2 * n" 365 moreover have "odd (Suc (2 * m))" and "even (2 * n)" 366 by simp_all 367 ultimately show False by simp 368qed 369 370lemma double_not_eq_Suc_double: 371 "2 * m \<noteq> Suc (2 * n)" 372 using Suc_double_not_eq_double [of n m] by simp 373 374lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n" 375 by (auto elim: oddE) 376 377lemma even_Suc_div_two [simp]: 378 "even n \<Longrightarrow> Suc n div 2 = n div 2" 379 using even_succ_div_two [of n] by simp 380 381lemma odd_Suc_div_two [simp]: 382 "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)" 383 using odd_succ_div_two [of n] by simp 384 385lemma odd_two_times_div_two_nat [simp]: 386 assumes "odd n" 387 shows "2 * (n div 2) = n - (1 :: nat)" 388proof - 389 from assms have "2 * (n div 2) + 1 = n" 390 by (rule odd_two_times_div_two_succ) 391 then have "Suc (2 * (n div 2)) - 1 = n - 1" 392 by simp 393 then show ?thesis 394 by simp 395qed 396 397lemma not_mod2_eq_Suc_0_eq_0 [simp]: 398 "n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0" 399 using not_mod_2_eq_1_eq_0 [of n] by simp 400 401lemma odd_card_imp_not_empty: 402 \<open>A \<noteq> {}\<close> if \<open>odd (card A)\<close> 403 using that by auto 404 405lemma nat_induct2 [case_names 0 1 step]: 406 assumes "P 0" "P 1" and step: "\<And>n::nat. P n \<Longrightarrow> P (n + 2)" 407 shows "P n" 408proof (induct n rule: less_induct) 409 case (less n) 410 show ?case 411 proof (cases "n < Suc (Suc 0)") 412 case True 413 then show ?thesis 414 using assms by (auto simp: less_Suc_eq) 415 next 416 case False 417 then obtain k where k: "n = Suc (Suc k)" 418 by (force simp: not_less nat_le_iff_add) 419 then have "k<n" 420 by simp 421 with less assms have "P (k+2)" 422 by blast 423 then show ?thesis 424 by (simp add: k) 425 qed 426qed 427 428lemma mask_eq_sum_exp_nat: 429 \<open>2 ^ n - Suc 0 = (\<Sum>m\<in>{q. q < n}. 2 ^ m)\<close> 430 using mask_eq_sum_exp [where ?'a = nat] by simp 431 432context semiring_parity 433begin 434 435lemma even_sum_iff: 436 \<open>even (sum f A) \<longleftrightarrow> even (card {a\<in>A. odd (f a)})\<close> if \<open>finite A\<close> 437using that proof (induction A) 438 case empty 439 then show ?case 440 by simp 441next 442 case (insert a A) 443 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> 444 by auto 445 ultimately show ?case 446 by simp 447qed 448 449lemma even_prod_iff: 450 \<open>even (prod f A) \<longleftrightarrow> (\<exists>a\<in>A. even (f a))\<close> if \<open>finite A\<close> 451 using that by (induction A) simp_all 452 453lemma even_mask_iff [simp]: 454 \<open>even (2 ^ n - 1) \<longleftrightarrow> n = 0\<close> 455proof (cases \<open>n = 0\<close>) 456 case True 457 then show ?thesis 458 by simp 459next 460 case False 461 then have \<open>{a. a = 0 \<and> a < n} = {0}\<close> 462 by auto 463 then show ?thesis 464 by (auto simp add: mask_eq_sum_exp even_sum_iff) 465qed 466 467end 468 469 470subsection \<open>Parity and powers\<close> 471 472context ring_1 473begin 474 475lemma power_minus_even [simp]: "even n \<Longrightarrow> (- a) ^ n = a ^ n" 476 by (auto elim: evenE) 477 478lemma power_minus_odd [simp]: "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)" 479 by (auto elim: oddE) 480 481lemma uminus_power_if: 482 "(- a) ^ n = (if even n then a ^ n else - (a ^ n))" 483 by auto 484 485lemma neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1" 486 by simp 487 488lemma neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1" 489 by simp 490 491lemma neg_one_power_add_eq_neg_one_power_diff: "k \<le> n \<Longrightarrow> (- 1) ^ (n + k) = (- 1) ^ (n - k)" 492 by (cases "even (n + k)") auto 493 494lemma minus_one_power_iff: "(- 1) ^ n = (if even n then 1 else - 1)" 495 by (induct n) auto 496 497end 498 499context linordered_idom 500begin 501 502lemma zero_le_even_power: "even n \<Longrightarrow> 0 \<le> a ^ n" 503 by (auto elim: evenE) 504 505lemma zero_le_odd_power: "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a" 506 by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE) 507 508lemma zero_le_power_eq: "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a" 509 by (auto simp add: zero_le_even_power zero_le_odd_power) 510 511lemma zero_less_power_eq: "0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a" 512proof - 513 have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0" 514 unfolding power_eq_0_iff [of a n, symmetric] by blast 515 show ?thesis 516 unfolding less_le zero_le_power_eq by auto 517qed 518 519lemma power_less_zero_eq [simp]: "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0" 520 unfolding not_le [symmetric] zero_le_power_eq by auto 521 522lemma power_le_zero_eq: "a ^ n \<le> 0 \<longleftrightarrow> n > 0 \<and> (odd n \<and> a \<le> 0 \<or> even n \<and> a = 0)" 523 unfolding not_less [symmetric] zero_less_power_eq by auto 524 525lemma power_even_abs: "even n \<Longrightarrow> \<bar>a\<bar> ^ n = a ^ n" 526 using power_abs [of a n] by (simp add: zero_le_even_power) 527 528lemma power_mono_even: 529 assumes "even n" and "\<bar>a\<bar> \<le> \<bar>b\<bar>" 530 shows "a ^ n \<le> b ^ n" 531proof - 532 have "0 \<le> \<bar>a\<bar>" by auto 533 with \<open>\<bar>a\<bar> \<le> \<bar>b\<bar>\<close> have "\<bar>a\<bar> ^ n \<le> \<bar>b\<bar> ^ n" 534 by (rule power_mono) 535 with \<open>even n\<close> show ?thesis 536 by (simp add: power_even_abs) 537qed 538 539lemma power_mono_odd: 540 assumes "odd n" and "a \<le> b" 541 shows "a ^ n \<le> b ^ n" 542proof (cases "b < 0") 543 case True 544 with \<open>a \<le> b\<close> have "- b \<le> - a" and "0 \<le> - b" by auto 545 then have "(- b) ^ n \<le> (- a) ^ n" by (rule power_mono) 546 with \<open>odd n\<close> show ?thesis by simp 547next 548 case False 549 then have "0 \<le> b" by auto 550 show ?thesis 551 proof (cases "a < 0") 552 case True 553 then have "n \<noteq> 0" and "a \<le> 0" using \<open>odd n\<close> [THEN odd_pos] by auto 554 then have "a ^ n \<le> 0" unfolding power_le_zero_eq using \<open>odd n\<close> by auto 555 moreover from \<open>0 \<le> b\<close> have "0 \<le> b ^ n" by auto 556 ultimately show ?thesis by auto 557 next 558 case False 559 then have "0 \<le> a" by auto 560 with \<open>a \<le> b\<close> show ?thesis 561 using power_mono by auto 562 qed 563qed 564 565text \<open>Simplify, when the exponent is a numeral\<close> 566 567lemma zero_le_power_eq_numeral [simp]: 568 "0 \<le> a ^ numeral w \<longleftrightarrow> even (numeral w :: nat) \<or> odd (numeral w :: nat) \<and> 0 \<le> a" 569 by (fact zero_le_power_eq) 570 571lemma zero_less_power_eq_numeral [simp]: 572 "0 < a ^ numeral w \<longleftrightarrow> 573 numeral w = (0 :: nat) \<or> 574 even (numeral w :: nat) \<and> a \<noteq> 0 \<or> 575 odd (numeral w :: nat) \<and> 0 < a" 576 by (fact zero_less_power_eq) 577 578lemma power_le_zero_eq_numeral [simp]: 579 "a ^ numeral w \<le> 0 \<longleftrightarrow> 580 (0 :: nat) < numeral w \<and> 581 (odd (numeral w :: nat) \<and> a \<le> 0 \<or> even (numeral w :: nat) \<and> a = 0)" 582 by (fact power_le_zero_eq) 583 584lemma power_less_zero_eq_numeral [simp]: 585 "a ^ numeral w < 0 \<longleftrightarrow> odd (numeral w :: nat) \<and> a < 0" 586 by (fact power_less_zero_eq) 587 588lemma power_even_abs_numeral [simp]: 589 "even (numeral w :: nat) \<Longrightarrow> \<bar>a\<bar> ^ numeral w = a ^ numeral w" 590 by (fact power_even_abs) 591 592end 593 594context unique_euclidean_semiring_with_nat 595begin 596 597lemma even_mask_div_iff': 598 \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> m \<le> n\<close> 599proof - 600 have \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> even (of_nat ((2 ^ m - Suc 0) div 2 ^ n))\<close> 601 by (simp only: of_nat_div) (simp add: of_nat_diff) 602 also have \<open>\<dots> \<longleftrightarrow> even ((2 ^ m - Suc 0) div 2 ^ n)\<close> 603 by simp 604 also have \<open>\<dots> \<longleftrightarrow> m \<le> n\<close> 605 proof (cases \<open>m \<le> n\<close>) 606 case True 607 then show ?thesis 608 by (simp add: Suc_le_lessD) 609 next 610 case False 611 then obtain r where r: \<open>m = n + Suc r\<close> 612 using less_imp_Suc_add by fastforce 613 from r have \<open>{q. q < m} \<inter> {q. 2 ^ n dvd (2::nat) ^ q} = {q. n \<le> q \<and> q < m}\<close> 614 by (auto simp add: dvd_power_iff_le) 615 moreover from r have \<open>{q. q < m} \<inter> {q. \<not> 2 ^ n dvd (2::nat) ^ q} = {q. q < n}\<close> 616 by (auto simp add: dvd_power_iff_le) 617 moreover from False have \<open>{q. n \<le> q \<and> q < m \<and> q \<le> n} = {n}\<close> 618 by auto 619 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> 620 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]) 621 ultimately have \<open>odd (sum ((^) (2::nat)) {q. q < m} div 2 ^ n)\<close> 622 by (subst euclidean_semiring_cancel_class.sum_div_partition) simp_all 623 with False show ?thesis 624 by (simp add: mask_eq_sum_exp_nat) 625 qed 626 finally show ?thesis . 627qed 628 629end 630 631 632subsection \<open>Instance for \<^typ>\<open>int\<close>\<close> 633 634lemma even_diff_iff: 635 "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int 636 by (fact even_diff) 637 638lemma even_abs_add_iff: 639 "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int 640 by simp 641 642lemma even_add_abs_iff: 643 "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int 644 by simp 645 646lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k" 647 by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric]) 648 649lemma zdiv_zmult2_eq: 650 \<open>a div (b * c) = (a div b) div c\<close> if \<open>c \<ge> 0\<close> for a b c :: int 651proof (cases \<open>b \<ge> 0\<close>) 652 case True 653 with that show ?thesis 654 using div_mult2_eq' [of a \<open>nat b\<close> \<open>nat c\<close>] by simp 655next 656 case False 657 with that show ?thesis 658 using div_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp 659qed 660 661lemma zmod_zmult2_eq: 662 \<open>a mod (b * c) = b * (a div b mod c) + a mod b\<close> if \<open>c \<ge> 0\<close> for a b c :: int 663proof (cases \<open>b \<ge> 0\<close>) 664 case True 665 with that show ?thesis 666 using mod_mult2_eq' [of a \<open>nat b\<close> \<open>nat c\<close>] by simp 667next 668 case False 669 with that show ?thesis 670 using mod_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp 671qed 672 673 674subsection \<open>Abstract bit structures\<close> 675 676class semiring_bits = semiring_parity + 677 assumes bits_induct [case_names stable rec]: 678 \<open>(\<And>a. a div 2 = a \<Longrightarrow> P a) 679 \<Longrightarrow> (\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a)) 680 \<Longrightarrow> P a\<close> 681 assumes bits_div_0 [simp]: \<open>0 div a = 0\<close> 682 and bits_div_by_1 [simp]: \<open>a div 1 = a\<close> 683 and bits_mod_div_trivial [simp]: \<open>a mod b div b = 0\<close> 684 and even_succ_div_2 [simp]: \<open>even a \<Longrightarrow> (1 + a) div 2 = a div 2\<close> 685 and even_mask_div_iff: \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0 \<or> m \<le> n\<close> 686 and exp_div_exp_eq: \<open>2 ^ m div 2 ^ n = of_bool (2 ^ m \<noteq> 0 \<and> m \<ge> n) * 2 ^ (m - n)\<close> 687 and div_exp_eq: \<open>a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)\<close> 688 and mod_exp_eq: \<open>a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n\<close> 689 and mult_exp_mod_exp_eq: \<open>m \<le> n \<Longrightarrow> (a * 2 ^ m) mod (2 ^ n) = (a mod 2 ^ (n - m)) * 2 ^ m\<close> 690 and div_exp_mod_exp_eq: \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close> 691 and even_mult_exp_div_exp_iff: \<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> m > n \<or> 2 ^ n = 0 \<or> (m \<le> n \<and> even (a div 2 ^ (n - m)))\<close> 692begin 693 694lemma bits_div_by_0 [simp]: 695 \<open>a div 0 = 0\<close> 696 by (metis add_cancel_right_right bits_mod_div_trivial mod_mult_div_eq mult_not_zero) 697 698lemma bits_1_div_2 [simp]: 699 \<open>1 div 2 = 0\<close> 700 using even_succ_div_2 [of 0] by simp 701 702lemma bits_1_div_exp [simp]: 703 \<open>1 div 2 ^ n = of_bool (n = 0)\<close> 704 using div_exp_eq [of 1 1] by (cases n) simp_all 705 706lemma even_succ_div_exp [simp]: 707 \<open>(1 + a) div 2 ^ n = a div 2 ^ n\<close> if \<open>even a\<close> and \<open>n > 0\<close> 708proof (cases n) 709 case 0 710 with that show ?thesis 711 by simp 712next 713 case (Suc n) 714 with \<open>even a\<close> have \<open>(1 + a) div 2 ^ Suc n = a div 2 ^ Suc n\<close> 715 proof (induction n) 716 case 0 717 then show ?case 718 by simp 719 next 720 case (Suc n) 721 then show ?case 722 using div_exp_eq [of _ 1 \<open>Suc n\<close>, symmetric] 723 by simp 724 qed 725 with Suc show ?thesis 726 by simp 727qed 728 729lemma even_succ_mod_exp [simp]: 730 \<open>(1 + a) mod 2 ^ n = 1 + (a mod 2 ^ n)\<close> if \<open>even a\<close> and \<open>n > 0\<close> 731 using div_mult_mod_eq [of \<open>1 + a\<close> \<open>2 ^ n\<close>] that 732 apply simp 733 by (metis local.add.left_commute local.add_left_cancel local.div_mult_mod_eq) 734 735lemma bits_mod_by_1 [simp]: 736 \<open>a mod 1 = 0\<close> 737 using div_mult_mod_eq [of a 1] by simp 738 739lemma bits_mod_0 [simp]: 740 \<open>0 mod a = 0\<close> 741 using div_mult_mod_eq [of 0 a] by simp 742 743lemma bits_one_mod_two_eq_one [simp]: 744 \<open>1 mod 2 = 1\<close> 745 by (simp add: mod2_eq_if) 746 747definition bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close> 748 where \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close> 749 750lemma bit_0 [simp]: 751 \<open>bit a 0 \<longleftrightarrow> odd a\<close> 752 by (simp add: bit_def) 753 754lemma bit_Suc: 755 \<open>bit a (Suc n) \<longleftrightarrow> bit (a div 2) n\<close> 756 using div_exp_eq [of a 1 n] by (simp add: bit_def) 757 758lemma bit_rec: 759 \<open>bit a n \<longleftrightarrow> (if n = 0 then odd a else bit (a div 2) (n - 1))\<close> 760 by (cases n) (simp_all add: bit_Suc) 761 762lemma bit_0_eq [simp]: 763 \<open>bit 0 = bot\<close> 764 by (simp add: fun_eq_iff bit_def) 765 766context 767 fixes a 768 assumes stable: \<open>a div 2 = a\<close> 769begin 770 771lemma bits_stable_imp_add_self: 772 \<open>a + a mod 2 = 0\<close> 773proof - 774 have \<open>a div 2 * 2 + a mod 2 = a\<close> 775 by (fact div_mult_mod_eq) 776 then have \<open>a * 2 + a mod 2 = a\<close> 777 by (simp add: stable) 778 then show ?thesis 779 by (simp add: mult_2_right ac_simps) 780qed 781 782lemma stable_imp_bit_iff_odd: 783 \<open>bit a n \<longleftrightarrow> odd a\<close> 784 by (induction n) (simp_all add: stable bit_Suc) 785 786end 787 788lemma bit_iff_idd_imp_stable: 789 \<open>a div 2 = a\<close> if \<open>\<And>n. bit a n \<longleftrightarrow> odd a\<close> 790using that proof (induction a rule: bits_induct) 791 case (stable a) 792 then show ?case 793 by simp 794next 795 case (rec a b) 796 from rec.prems [of 1] have [simp]: \<open>b = odd a\<close> 797 by (simp add: rec.hyps bit_Suc) 798 from rec.hyps have hyp: \<open>(of_bool (odd a) + 2 * a) div 2 = a\<close> 799 by simp 800 have \<open>bit a n \<longleftrightarrow> odd a\<close> for n 801 using rec.prems [of \<open>Suc n\<close>] by (simp add: hyp bit_Suc) 802 then have \<open>a div 2 = a\<close> 803 by (rule rec.IH) 804 then have \<open>of_bool (odd a) + 2 * a = 2 * (a div 2) + of_bool (odd a)\<close> 805 by (simp add: ac_simps) 806 also have \<open>\<dots> = a\<close> 807 using mult_div_mod_eq [of 2 a] 808 by (simp add: of_bool_odd_eq_mod_2) 809 finally show ?case 810 using \<open>a div 2 = a\<close> by (simp add: hyp) 811qed 812 813lemma exp_eq_0_imp_not_bit: 814 \<open>\<not> bit a n\<close> if \<open>2 ^ n = 0\<close> 815 using that by (simp add: bit_def) 816 817lemma bit_eqI: 818 \<open>a = b\<close> if \<open>\<And>n. 2 ^ n \<noteq> 0 \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close> 819proof - 820 have \<open>bit a n \<longleftrightarrow> bit b n\<close> for n 821 proof (cases \<open>2 ^ n = 0\<close>) 822 case True 823 then show ?thesis 824 by (simp add: exp_eq_0_imp_not_bit) 825 next 826 case False 827 then show ?thesis 828 by (rule that) 829 qed 830 then show ?thesis proof (induction a arbitrary: b rule: bits_induct) 831 case (stable a) 832 from stable(2) [of 0] have **: \<open>even b \<longleftrightarrow> even a\<close> 833 by simp 834 have \<open>b div 2 = b\<close> 835 proof (rule bit_iff_idd_imp_stable) 836 fix n 837 from stable have *: \<open>bit b n \<longleftrightarrow> bit a n\<close> 838 by simp 839 also have \<open>bit a n \<longleftrightarrow> odd a\<close> 840 using stable by (simp add: stable_imp_bit_iff_odd) 841 finally show \<open>bit b n \<longleftrightarrow> odd b\<close> 842 by (simp add: **) 843 qed 844 from ** have \<open>a mod 2 = b mod 2\<close> 845 by (simp add: mod2_eq_if) 846 then have \<open>a mod 2 + (a + b) = b mod 2 + (a + b)\<close> 847 by simp 848 then have \<open>a + a mod 2 + b = b + b mod 2 + a\<close> 849 by (simp add: ac_simps) 850 with \<open>a div 2 = a\<close> \<open>b div 2 = b\<close> show ?case 851 by (simp add: bits_stable_imp_add_self) 852 next 853 case (rec a p) 854 from rec.prems [of 0] have [simp]: \<open>p = odd b\<close> 855 by simp 856 from rec.hyps have \<open>bit a n \<longleftrightarrow> bit (b div 2) n\<close> for n 857 using rec.prems [of \<open>Suc n\<close>] by (simp add: bit_Suc) 858 then have \<open>a = b div 2\<close> 859 by (rule rec.IH) 860 then have \<open>2 * a = 2 * (b div 2)\<close> 861 by simp 862 then have \<open>b mod 2 + 2 * a = b mod 2 + 2 * (b div 2)\<close> 863 by simp 864 also have \<open>\<dots> = b\<close> 865 by (fact mod_mult_div_eq) 866 finally show ?case 867 by (auto simp add: mod2_eq_if) 868 qed 869qed 870 871lemma bit_eq_iff: 872 \<open>a = b \<longleftrightarrow> (\<forall>n. bit a n \<longleftrightarrow> bit b n)\<close> 873 by (auto intro: bit_eqI) 874 875lemma bit_exp_iff: 876 \<open>bit (2 ^ m) n \<longleftrightarrow> 2 ^ m \<noteq> 0 \<and> m = n\<close> 877 by (auto simp add: bit_def exp_div_exp_eq) 878 879lemma bit_1_iff: 880 \<open>bit 1 n \<longleftrightarrow> 1 \<noteq> 0 \<and> n = 0\<close> 881 using bit_exp_iff [of 0 n] by simp 882 883lemma bit_2_iff: 884 \<open>bit 2 n \<longleftrightarrow> 2 \<noteq> 0 \<and> n = 1\<close> 885 using bit_exp_iff [of 1 n] by auto 886 887lemma even_bit_succ_iff: 888 \<open>bit (1 + a) n \<longleftrightarrow> bit a n \<or> n = 0\<close> if \<open>even a\<close> 889 using that by (cases \<open>n = 0\<close>) (simp_all add: bit_def) 890 891lemma odd_bit_iff_bit_pred: 892 \<open>bit a n \<longleftrightarrow> bit (a - 1) n \<or> n = 0\<close> if \<open>odd a\<close> 893proof - 894 from \<open>odd a\<close> obtain b where \<open>a = 2 * b + 1\<close> .. 895 moreover have \<open>bit (2 * b) n \<or> n = 0 \<longleftrightarrow> bit (1 + 2 * b) n\<close> 896 using even_bit_succ_iff by simp 897 ultimately show ?thesis by (simp add: ac_simps) 898qed 899 900lemma bit_double_iff: 901 \<open>bit (2 * a) n \<longleftrightarrow> bit a (n - 1) \<and> n \<noteq> 0 \<and> 2 ^ n \<noteq> 0\<close> 902 using even_mult_exp_div_exp_iff [of a 1 n] 903 by (cases n, auto simp add: bit_def ac_simps) 904 905lemma bit_eq_rec: 906 \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close> (is \<open>?P = ?Q\<close>) 907proof 908 assume ?P 909 then show ?Q 910 by simp 911next 912 assume ?Q 913 then have \<open>even a \<longleftrightarrow> even b\<close> and \<open>a div 2 = b div 2\<close> 914 by simp_all 915 show ?P 916 proof (rule bit_eqI) 917 fix n 918 show \<open>bit a n \<longleftrightarrow> bit b n\<close> 919 proof (cases n) 920 case 0 921 with \<open>even a \<longleftrightarrow> even b\<close> show ?thesis 922 by simp 923 next 924 case (Suc n) 925 moreover from \<open>a div 2 = b div 2\<close> have \<open>bit (a div 2) n = bit (b div 2) n\<close> 926 by simp 927 ultimately show ?thesis 928 by (simp add: bit_Suc) 929 qed 930 qed 931qed 932 933lemma bit_mask_iff: 934 \<open>bit (2 ^ m - 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close> 935 by (simp add: bit_def even_mask_div_iff not_le) 936 937end 938 939lemma nat_bit_induct [case_names zero even odd]: 940 "P n" if zero: "P 0" 941 and even: "\<And>n. P n \<Longrightarrow> n > 0 \<Longrightarrow> P (2 * n)" 942 and odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))" 943proof (induction n rule: less_induct) 944 case (less n) 945 show "P n" 946 proof (cases "n = 0") 947 case True with zero show ?thesis by simp 948 next 949 case False 950 with less have hyp: "P (n div 2)" by simp 951 show ?thesis 952 proof (cases "even n") 953 case True 954 then have "n \<noteq> 1" 955 by auto 956 with \<open>n \<noteq> 0\<close> have "n div 2 > 0" 957 by simp 958 with \<open>even n\<close> hyp even [of "n div 2"] show ?thesis 959 by simp 960 next 961 case False 962 with hyp odd [of "n div 2"] show ?thesis 963 by simp 964 qed 965 qed 966qed 967 968instance nat :: semiring_bits 969proof 970 show \<open>P n\<close> if stable: \<open>\<And>n. n div 2 = n \<Longrightarrow> P n\<close> 971 and rec: \<open>\<And>n b. P n \<Longrightarrow> (of_bool b + 2 * n) div 2 = n \<Longrightarrow> P (of_bool b + 2 * n)\<close> 972 for P and n :: nat 973 proof (induction n rule: nat_bit_induct) 974 case zero 975 from stable [of 0] show ?case 976 by simp 977 next 978 case (even n) 979 with rec [of n False] show ?case 980 by simp 981 next 982 case (odd n) 983 with rec [of n True] show ?case 984 by simp 985 qed 986 show \<open>q mod 2 ^ m mod 2 ^ n = q mod 2 ^ min m n\<close> 987 for q m n :: nat 988 apply (auto simp add: less_iff_Suc_add power_add mod_mod_cancel split: split_min_lin) 989 apply (metis div_mult2_eq mod_div_trivial mod_eq_self_iff_div_eq_0 mod_mult_self2_is_0 power_commutes) 990 done 991 show \<open>(q * 2 ^ m) mod (2 ^ n) = (q mod 2 ^ (n - m)) * 2 ^ m\<close> if \<open>m \<le> n\<close> 992 for q m n :: nat 993 using that 994 apply (auto simp add: mod_mod_cancel div_mult2_eq power_add mod_mult2_eq le_iff_add split: split_min_lin) 995 apply (simp add: mult.commute) 996 done 997 show \<open>even ((2 ^ m - (1::nat)) div 2 ^ n) \<longleftrightarrow> 2 ^ n = (0::nat) \<or> m \<le> n\<close> 998 for m n :: nat 999 using even_mask_div_iff' [where ?'a = nat, of m n] by simp 1000 show \<open>even (q * 2 ^ m div 2 ^ n) \<longleftrightarrow> n < m \<or> (2::nat) ^ n = 0 \<or> m \<le> n \<and> even (q div 2 ^ (n - m))\<close> 1001 for m n q r :: nat 1002 apply (auto simp add: not_less power_add ac_simps dest!: le_Suc_ex) 1003 apply (metis (full_types) dvd_mult dvd_mult_imp_div dvd_power_iff_le not_less not_less_eq order_refl power_Suc) 1004 done 1005qed (auto simp add: div_mult2_eq mod_mult2_eq power_add power_diff) 1006 1007lemma int_bit_induct [case_names zero minus even odd]: 1008 "P k" if zero_int: "P 0" 1009 and minus_int: "P (- 1)" 1010 and even_int: "\<And>k. P k \<Longrightarrow> k \<noteq> 0 \<Longrightarrow> P (k * 2)" 1011 and odd_int: "\<And>k. P k \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> P (1 + (k * 2))" for k :: int 1012proof (cases "k \<ge> 0") 1013 case True 1014 define n where "n = nat k" 1015 with True have "k = int n" 1016 by simp 1017 then show "P k" 1018 proof (induction n arbitrary: k rule: nat_bit_induct) 1019 case zero 1020 then show ?case 1021 by (simp add: zero_int) 1022 next 1023 case (even n) 1024 have "P (int n * 2)" 1025 by (rule even_int) (use even in simp_all) 1026 with even show ?case 1027 by (simp add: ac_simps) 1028 next 1029 case (odd n) 1030 have "P (1 + (int n * 2))" 1031 by (rule odd_int) (use odd in simp_all) 1032 with odd show ?case 1033 by (simp add: ac_simps) 1034 qed 1035next 1036 case False 1037 define n where "n = nat (- k - 1)" 1038 with False have "k = - int n - 1" 1039 by simp 1040 then show "P k" 1041 proof (induction n arbitrary: k rule: nat_bit_induct) 1042 case zero 1043 then show ?case 1044 by (simp add: minus_int) 1045 next 1046 case (even n) 1047 have "P (1 + (- int (Suc n) * 2))" 1048 by (rule odd_int) (use even in \<open>simp_all add: algebra_simps\<close>) 1049 also have "\<dots> = - int (2 * n) - 1" 1050 by (simp add: algebra_simps) 1051 finally show ?case 1052 using even by simp 1053 next 1054 case (odd n) 1055 have "P (- int (Suc n) * 2)" 1056 by (rule even_int) (use odd in \<open>simp_all add: algebra_simps\<close>) 1057 also have "\<dots> = - int (Suc (2 * n)) - 1" 1058 by (simp add: algebra_simps) 1059 finally show ?case 1060 using odd by simp 1061 qed 1062qed 1063 1064instance int :: semiring_bits 1065proof 1066 show \<open>P k\<close> if stable: \<open>\<And>k. k div 2 = k \<Longrightarrow> P k\<close> 1067 and rec: \<open>\<And>k b. P k \<Longrightarrow> (of_bool b + 2 * k) div 2 = k \<Longrightarrow> P (of_bool b + 2 * k)\<close> 1068 for P and k :: int 1069 proof (induction k rule: int_bit_induct) 1070 case zero 1071 from stable [of 0] show ?case 1072 by simp 1073 next 1074 case minus 1075 from stable [of \<open>- 1\<close>] show ?case 1076 by simp 1077 next 1078 case (even k) 1079 with rec [of k False] show ?case 1080 by (simp add: ac_simps) 1081 next 1082 case (odd k) 1083 with rec [of k True] show ?case 1084 by (simp add: ac_simps) 1085 qed 1086 show \<open>(2::int) ^ m div 2 ^ n = of_bool ((2::int) ^ m \<noteq> 0 \<and> n \<le> m) * 2 ^ (m - n)\<close> 1087 for m n :: nat 1088 proof (cases \<open>m < n\<close>) 1089 case True 1090 then have \<open>n = m + (n - m)\<close> 1091 by simp 1092 then have \<open>(2::int) ^ m div 2 ^ n = (2::int) ^ m div 2 ^ (m + (n - m))\<close> 1093 by simp 1094 also have \<open>\<dots> = (2::int) ^ m div (2 ^ m * 2 ^ (n - m))\<close> 1095 by (simp add: power_add) 1096 also have \<open>\<dots> = (2::int) ^ m div 2 ^ m div 2 ^ (n - m)\<close> 1097 by (simp add: zdiv_zmult2_eq) 1098 finally show ?thesis using \<open>m < n\<close> by simp 1099 next 1100 case False 1101 then show ?thesis 1102 by (simp add: power_diff) 1103 qed 1104 show \<open>k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n\<close> 1105 for m n :: nat and k :: int 1106 using mod_exp_eq [of \<open>nat k\<close> m n] 1107 apply (auto simp add: mod_mod_cancel zdiv_zmult2_eq power_add zmod_zmult2_eq le_iff_add split: split_min_lin) 1108 apply (auto simp add: less_iff_Suc_add mod_mod_cancel power_add) 1109 apply (simp only: flip: mult.left_commute [of \<open>2 ^ m\<close>]) 1110 apply (subst zmod_zmult2_eq) apply simp_all 1111 done 1112 show \<open>(k * 2 ^ m) mod (2 ^ n) = (k mod 2 ^ (n - m)) * 2 ^ m\<close> 1113 if \<open>m \<le> n\<close> for m n :: nat and k :: int 1114 using that 1115 apply (auto simp add: power_add zmod_zmult2_eq le_iff_add split: split_min_lin) 1116 apply (simp add: ac_simps) 1117 done 1118 show \<open>even ((2 ^ m - (1::int)) div 2 ^ n) \<longleftrightarrow> 2 ^ n = (0::int) \<or> m \<le> n\<close> 1119 for m n :: nat 1120 using even_mask_div_iff' [where ?'a = int, of m n] by simp 1121 show \<open>even (k * 2 ^ m div 2 ^ n) \<longleftrightarrow> n < m \<or> (2::int) ^ n = 0 \<or> m \<le> n \<and> even (k div 2 ^ (n - m))\<close> 1122 for m n :: nat and k l :: int 1123 apply (auto simp add: not_less power_add ac_simps dest!: le_Suc_ex) 1124 apply (metis Suc_leI dvd_mult dvd_mult_imp_div dvd_power_le dvd_refl power.simps(2)) 1125 done 1126qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add power_diff not_le) 1127 1128class semiring_bit_shifts = semiring_bits + 1129 fixes push_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close> 1130 assumes push_bit_eq_mult: \<open>push_bit n a = a * 2 ^ n\<close> 1131 fixes drop_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close> 1132 assumes drop_bit_eq_div: \<open>drop_bit n a = a div 2 ^ n\<close> 1133begin 1134 1135definition take_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close> 1136 where take_bit_eq_mod: \<open>take_bit n a = a mod 2 ^ n\<close> 1137 1138text \<open> 1139 Logically, \<^const>\<open>push_bit\<close>, 1140 \<^const>\<open>drop_bit\<close> and \<^const>\<open>take_bit\<close> are just aliases; having them 1141 as separate operations makes proofs easier, otherwise proof automation 1142 would fiddle with concrete expressions \<^term>\<open>2 ^ n\<close> in a way obfuscating the basic 1143 algebraic relationships between those operations. 1144 Having 1145 \<^const>\<open>push_bit\<close> and \<^const>\<open>drop_bit\<close> as definitional class operations 1146 takes into account that specific instances of these can be implemented 1147 differently wrt. code generation. 1148\<close> 1149 1150lemma bit_iff_odd_drop_bit: 1151 \<open>bit a n \<longleftrightarrow> odd (drop_bit n a)\<close> 1152 by (simp add: bit_def drop_bit_eq_div) 1153 1154lemma even_drop_bit_iff_not_bit: 1155 \<open>even (drop_bit n a) \<longleftrightarrow> \<not> bit a n\<close> 1156 by (simp add: bit_iff_odd_drop_bit) 1157 1158lemma div_push_bit_of_1_eq_drop_bit: 1159 \<open>a div push_bit n 1 = drop_bit n a\<close> 1160 by (simp add: push_bit_eq_mult drop_bit_eq_div) 1161 1162lemma bits_ident: 1163 "push_bit n (drop_bit n a) + take_bit n a = a" 1164 using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div) 1165 1166lemma push_bit_push_bit [simp]: 1167 "push_bit m (push_bit n a) = push_bit (m + n) a" 1168 by (simp add: push_bit_eq_mult power_add ac_simps) 1169 1170lemma push_bit_0_id [simp]: 1171 "push_bit 0 = id" 1172 by (simp add: fun_eq_iff push_bit_eq_mult) 1173 1174lemma push_bit_of_0 [simp]: 1175 "push_bit n 0 = 0" 1176 by (simp add: push_bit_eq_mult) 1177 1178lemma push_bit_of_1: 1179 "push_bit n 1 = 2 ^ n" 1180 by (simp add: push_bit_eq_mult) 1181 1182lemma push_bit_Suc [simp]: 1183 "push_bit (Suc n) a = push_bit n (a * 2)" 1184 by (simp add: push_bit_eq_mult ac_simps) 1185 1186lemma push_bit_double: 1187 "push_bit n (a * 2) = push_bit n a * 2" 1188 by (simp add: push_bit_eq_mult ac_simps) 1189 1190lemma push_bit_add: 1191 "push_bit n (a + b) = push_bit n a + push_bit n b" 1192 by (simp add: push_bit_eq_mult algebra_simps) 1193 1194lemma take_bit_0 [simp]: 1195 "take_bit 0 a = 0" 1196 by (simp add: take_bit_eq_mod) 1197 1198lemma take_bit_Suc: 1199 \<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + of_bool (odd a)\<close> 1200proof - 1201 have \<open>take_bit (Suc n) (a div 2 * 2 + of_bool (odd a)) = take_bit n (a div 2) * 2 + of_bool (odd a)\<close> 1202 using even_succ_mod_exp [of \<open>2 * (a div 2)\<close> \<open>Suc n\<close>] 1203 mult_exp_mod_exp_eq [of 1 \<open>Suc n\<close> \<open>a div 2\<close>] 1204 by (auto simp add: take_bit_eq_mod ac_simps) 1205 then show ?thesis 1206 using div_mult_mod_eq [of a 2] by (simp add: mod_2_eq_odd) 1207qed 1208 1209lemma take_bit_rec: 1210 \<open>take_bit n a = (if n = 0 then 0 else take_bit (n - 1) (a div 2) * 2 + of_bool (odd a))\<close> 1211 by (cases n) (simp_all add: take_bit_Suc) 1212 1213lemma take_bit_of_0 [simp]: 1214 "take_bit n 0 = 0" 1215 by (simp add: take_bit_eq_mod) 1216 1217lemma take_bit_of_1 [simp]: 1218 "take_bit n 1 = of_bool (n > 0)" 1219 by (cases n) (simp_all add: take_bit_Suc) 1220 1221lemma drop_bit_of_0 [simp]: 1222 "drop_bit n 0 = 0" 1223 by (simp add: drop_bit_eq_div) 1224 1225lemma drop_bit_of_1 [simp]: 1226 "drop_bit n 1 = of_bool (n = 0)" 1227 by (simp add: drop_bit_eq_div) 1228 1229lemma drop_bit_0 [simp]: 1230 "drop_bit 0 = id" 1231 by (simp add: fun_eq_iff drop_bit_eq_div) 1232 1233lemma drop_bit_Suc: 1234 "drop_bit (Suc n) a = drop_bit n (a div 2)" 1235 using div_exp_eq [of a 1] by (simp add: drop_bit_eq_div) 1236 1237lemma drop_bit_rec: 1238 "drop_bit n a = (if n = 0 then a else drop_bit (n - 1) (a div 2))" 1239 by (cases n) (simp_all add: drop_bit_Suc) 1240 1241lemma drop_bit_half: 1242 "drop_bit n (a div 2) = drop_bit n a div 2" 1243 by (induction n arbitrary: a) (simp_all add: drop_bit_Suc) 1244 1245lemma drop_bit_of_bool [simp]: 1246 "drop_bit n (of_bool b) = of_bool (n = 0 \<and> b)" 1247 by (cases n) simp_all 1248 1249lemma take_bit_eq_0_imp_dvd: 1250 "take_bit n a = 0 \<Longrightarrow> 2 ^ n dvd a" 1251 by (simp add: take_bit_eq_mod mod_0_imp_dvd) 1252 1253lemma even_take_bit_eq [simp]: 1254 \<open>even (take_bit n a) \<longleftrightarrow> n = 0 \<or> even a\<close> 1255 by (simp add: take_bit_rec [of n a]) 1256 1257lemma take_bit_take_bit [simp]: 1258 "take_bit m (take_bit n a) = take_bit (min m n) a" 1259 by (simp add: take_bit_eq_mod mod_exp_eq ac_simps) 1260 1261lemma drop_bit_drop_bit [simp]: 1262 "drop_bit m (drop_bit n a) = drop_bit (m + n) a" 1263 by (simp add: drop_bit_eq_div power_add div_exp_eq ac_simps) 1264 1265lemma push_bit_take_bit: 1266 "push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)" 1267 apply (simp add: push_bit_eq_mult take_bit_eq_mod power_add ac_simps) 1268 using mult_exp_mod_exp_eq [of m \<open>m + n\<close> a] apply (simp add: ac_simps power_add) 1269 done 1270 1271lemma take_bit_push_bit: 1272 "take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)" 1273proof (cases "m \<le> n") 1274 case True 1275 then show ?thesis 1276 apply (simp add:) 1277 apply (simp_all add: push_bit_eq_mult take_bit_eq_mod) 1278 apply (auto dest!: le_Suc_ex simp add: power_add ac_simps) 1279 using mult_exp_mod_exp_eq [of m m \<open>a * 2 ^ n\<close> for n] 1280 apply (simp add: ac_simps) 1281 done 1282next 1283 case False 1284 then show ?thesis 1285 using push_bit_take_bit [of n "m - n" a] 1286 by simp 1287qed 1288 1289lemma take_bit_drop_bit: 1290 "take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)" 1291 by (simp add: drop_bit_eq_div take_bit_eq_mod ac_simps div_exp_mod_exp_eq) 1292 1293lemma drop_bit_take_bit: 1294 "drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)" 1295proof (cases "m \<le> n") 1296 case True 1297 then show ?thesis 1298 using take_bit_drop_bit [of "n - m" m a] by simp 1299next 1300 case False 1301 then obtain q where \<open>m = n + q\<close> 1302 by (auto simp add: not_le dest: less_imp_Suc_add) 1303 then have \<open>drop_bit m (take_bit n a) = 0\<close> 1304 using div_exp_eq [of \<open>a mod 2 ^ n\<close> n q] 1305 by (simp add: take_bit_eq_mod drop_bit_eq_div) 1306 with False show ?thesis 1307 by simp 1308qed 1309 1310lemma even_push_bit_iff [simp]: 1311 \<open>even (push_bit n a) \<longleftrightarrow> n \<noteq> 0 \<or> even a\<close> 1312 by (simp add: push_bit_eq_mult) auto 1313 1314lemma bit_push_bit_iff: 1315 \<open>bit (push_bit m a) n \<longleftrightarrow> n \<ge> m \<and> 2 ^ n \<noteq> 0 \<and> (n < m \<or> bit a (n - m))\<close> 1316 by (auto simp add: bit_def push_bit_eq_mult even_mult_exp_div_exp_iff) 1317 1318lemma bit_drop_bit_eq: 1319 \<open>bit (drop_bit n a) = bit a \<circ> (+) n\<close> 1320 by (simp add: bit_def fun_eq_iff ac_simps flip: drop_bit_eq_div) 1321 1322lemma bit_take_bit_iff: 1323 \<open>bit (take_bit m a) n \<longleftrightarrow> n < m \<and> bit a n\<close> 1324 by (simp add: bit_def drop_bit_take_bit not_le flip: drop_bit_eq_div) 1325 1326lemma stable_imp_drop_bit_eq: 1327 \<open>drop_bit n a = a\<close> 1328 if \<open>a div 2 = a\<close> 1329 by (induction n) (simp_all add: that drop_bit_Suc) 1330 1331lemma stable_imp_take_bit_eq: 1332 \<open>take_bit n a = (if even a then 0 else 2 ^ n - 1)\<close> 1333 if \<open>a div 2 = a\<close> 1334proof (rule bit_eqI) 1335 fix m 1336 assume \<open>2 ^ m \<noteq> 0\<close> 1337 with that show \<open>bit (take_bit n a) m \<longleftrightarrow> bit (if even a then 0 else 2 ^ n - 1) m\<close> 1338 by (simp add: bit_take_bit_iff bit_mask_iff stable_imp_bit_iff_odd) 1339qed 1340 1341end 1342 1343instantiation nat :: semiring_bit_shifts 1344begin 1345 1346definition push_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close> 1347 where \<open>push_bit_nat n m = m * 2 ^ n\<close> 1348 1349definition drop_bit_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close> 1350 where \<open>drop_bit_nat n m = m div 2 ^ n\<close> 1351 1352instance proof 1353 show \<open>push_bit n m = m * 2 ^ n\<close> for n m :: nat 1354 by (simp add: push_bit_nat_def) 1355 show \<open>drop_bit n m = m div 2 ^ n\<close> for n m :: nat 1356 by (simp add: drop_bit_nat_def) 1357qed 1358 1359end 1360 1361instantiation int :: semiring_bit_shifts 1362begin 1363 1364definition push_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close> 1365 where \<open>push_bit_int n k = k * 2 ^ n\<close> 1366 1367definition drop_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close> 1368 where \<open>drop_bit_int n k = k div 2 ^ n\<close> 1369 1370instance proof 1371 show \<open>push_bit n k = k * 2 ^ n\<close> for n :: nat and k :: int 1372 by (simp add: push_bit_int_def) 1373 show \<open>drop_bit n k = k div 2 ^ n\<close> for n :: nat and k :: int 1374 by (simp add: drop_bit_int_def) 1375qed 1376 1377end 1378 1379lemma bit_push_bit_iff_nat: 1380 \<open>bit (push_bit m q) n \<longleftrightarrow> m \<le> n \<and> bit q (n - m)\<close> for q :: nat 1381 by (auto simp add: bit_push_bit_iff) 1382 1383lemma bit_push_bit_iff_int: 1384 \<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int 1385 by (auto simp add: bit_push_bit_iff) 1386 1387class unique_euclidean_semiring_with_bit_shifts = 1388 unique_euclidean_semiring_with_nat + semiring_bit_shifts 1389begin 1390 1391lemma take_bit_of_exp [simp]: 1392 \<open>take_bit m (2 ^ n) = of_bool (n < m) * 2 ^ n\<close> 1393 by (simp add: take_bit_eq_mod exp_mod_exp) 1394 1395lemma take_bit_of_2 [simp]: 1396 \<open>take_bit n 2 = of_bool (2 \<le> n) * 2\<close> 1397 using take_bit_of_exp [of n 1] by simp 1398 1399lemma take_bit_of_mask: 1400 \<open>take_bit m (2 ^ n - 1) = 2 ^ min m n - 1\<close> 1401 by (simp add: take_bit_eq_mod mask_mod_exp) 1402 1403lemma push_bit_eq_0_iff [simp]: 1404 "push_bit n a = 0 \<longleftrightarrow> a = 0" 1405 by (simp add: push_bit_eq_mult) 1406 1407lemma push_bit_numeral [simp]: 1408 "push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))" 1409 by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric]) (simp add: ac_simps) 1410 1411lemma push_bit_of_nat: 1412 "push_bit n (of_nat m) = of_nat (push_bit n m)" 1413 by (simp add: push_bit_eq_mult Parity.push_bit_eq_mult) 1414 1415lemma take_bit_add: 1416 "take_bit n (take_bit n a + take_bit n b) = take_bit n (a + b)" 1417 by (simp add: take_bit_eq_mod mod_simps) 1418 1419lemma take_bit_eq_0_iff: 1420 "take_bit n a = 0 \<longleftrightarrow> 2 ^ n dvd a" 1421 by (simp add: take_bit_eq_mod mod_eq_0_iff_dvd) 1422 1423lemma take_bit_of_1_eq_0_iff [simp]: 1424 "take_bit n 1 = 0 \<longleftrightarrow> n = 0" 1425 by (simp add: take_bit_eq_mod) 1426 1427lemma take_bit_numeral_bit0 [simp]: 1428 "take_bit (numeral l) (numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (numeral k) * 2" 1429 by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric] take_bit_Suc 1430 ac_simps even_mult_iff nonzero_mult_div_cancel_right [OF numeral_neq_zero]) simp 1431 1432lemma take_bit_numeral_bit1 [simp]: 1433 "take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1" 1434 by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] take_bit_Suc 1435 ac_simps even_add even_mult_iff div_mult_self1 [OF numeral_neq_zero]) (simp add: ac_simps) 1436 1437lemma take_bit_of_nat: 1438 "take_bit n (of_nat m) = of_nat (take_bit n m)" 1439 by (simp add: take_bit_eq_mod Parity.take_bit_eq_mod of_nat_mod [of m "2 ^ n"]) 1440 1441lemma drop_bit_numeral_bit0 [simp]: 1442 "drop_bit (numeral l) (numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (numeral k)" 1443 by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric] drop_bit_Suc 1444 nonzero_mult_div_cancel_left [OF numeral_neq_zero]) 1445 1446lemma drop_bit_numeral_bit1 [simp]: 1447 "drop_bit (numeral l) (numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (numeral k)" 1448 by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] drop_bit_Suc 1449 div_mult_self4 [OF numeral_neq_zero]) simp 1450 1451lemma drop_bit_of_nat: 1452 "drop_bit n (of_nat m) = of_nat (drop_bit n m)" 1453 by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"]) 1454 1455lemma bit_of_nat_iff_bit [simp]: 1456 \<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close> 1457proof - 1458 have \<open>even (m div 2 ^ n) \<longleftrightarrow> even (of_nat (m div 2 ^ n))\<close> 1459 by simp 1460 also have \<open>of_nat (m div 2 ^ n) = of_nat m div of_nat (2 ^ n)\<close> 1461 by (simp add: of_nat_div) 1462 finally show ?thesis 1463 by (simp add: bit_def semiring_bits_class.bit_def) 1464qed 1465 1466lemma of_nat_push_bit: 1467 \<open>of_nat (push_bit m n) = push_bit m (of_nat n)\<close> 1468 by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult) 1469 1470lemma of_nat_drop_bit: 1471 \<open>of_nat (drop_bit m n) = drop_bit m (of_nat n)\<close> 1472 by (simp add: drop_bit_eq_div semiring_bit_shifts_class.drop_bit_eq_div of_nat_div) 1473 1474lemma of_nat_take_bit: 1475 \<open>of_nat (take_bit m n) = take_bit m (of_nat n)\<close> 1476 by (simp add: take_bit_eq_mod semiring_bit_shifts_class.take_bit_eq_mod of_nat_mod) 1477 1478lemma bit_push_bit_iff_of_nat_iff: 1479 \<open>bit (push_bit m (of_nat r)) n \<longleftrightarrow> m \<le> n \<and> bit (of_nat r) (n - m)\<close> 1480 by (auto simp add: bit_push_bit_iff) 1481 1482end 1483 1484instance nat :: unique_euclidean_semiring_with_bit_shifts .. 1485 1486instance int :: unique_euclidean_semiring_with_bit_shifts .. 1487 1488lemma push_bit_of_Suc_0 [simp]: 1489 "push_bit n (Suc 0) = 2 ^ n" 1490 using push_bit_of_1 [where ?'a = nat] by simp 1491 1492lemma take_bit_of_Suc_0 [simp]: 1493 "take_bit n (Suc 0) = of_bool (0 < n)" 1494 using take_bit_of_1 [where ?'a = nat] by simp 1495 1496lemma drop_bit_of_Suc_0 [simp]: 1497 "drop_bit n (Suc 0) = of_bool (n = 0)" 1498 using drop_bit_of_1 [where ?'a = nat] by simp 1499 1500lemma take_bit_eq_self: 1501 \<open>take_bit n m = m\<close> if \<open>m < 2 ^ n\<close> for n m :: nat 1502 using that by (simp add: take_bit_eq_mod) 1503 1504lemma push_bit_minus_one: 1505 "push_bit n (- 1 :: int) = - (2 ^ n)" 1506 by (simp add: push_bit_eq_mult) 1507 1508lemma minus_1_div_exp_eq_int: 1509 \<open>- 1 div (2 :: int) ^ n = - 1\<close> 1510 by (induction n) (use div_exp_eq [symmetric, of \<open>- 1 :: int\<close> 1] in \<open>simp_all add: ac_simps\<close>) 1511 1512lemma drop_bit_minus_one [simp]: 1513 \<open>drop_bit n (- 1 :: int) = - 1\<close> 1514 by (simp add: drop_bit_eq_div minus_1_div_exp_eq_int) 1515 1516lemma take_bit_minus: 1517 "take_bit n (- (take_bit n k)) = take_bit n (- k)" 1518 for k :: int 1519 by (simp add: take_bit_eq_mod mod_minus_eq) 1520 1521lemma take_bit_diff: 1522 "take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)" 1523 for k l :: int 1524 by (simp add: take_bit_eq_mod mod_diff_eq) 1525 1526lemma take_bit_nonnegative [simp]: 1527 "take_bit n k \<ge> 0" 1528 for k :: int 1529 by (simp add: take_bit_eq_mod) 1530 1531lemma drop_bit_push_bit_int: 1532 \<open>drop_bit m (push_bit n k) = drop_bit (m - n) (push_bit (n - m) k)\<close> for k :: int 1533 by (cases \<open>m \<le> n\<close>) (auto simp add: mult.left_commute [of _ \<open>2 ^ n\<close>] mult.commute [of _ \<open>2 ^ n\<close>] mult.assoc 1534 mult.commute [of k] drop_bit_eq_div push_bit_eq_mult not_le power_add dest!: le_Suc_ex less_imp_Suc_add) 1535 1536end 1537