483 |
483 |
484 end |
484 end |
485 |
485 |
486 |
486 |
487 subsection \<open>Instance \<^typ>\<open>int\<close>\<close> |
487 subsection \<open>Instance \<^typ>\<open>int\<close>\<close> |
|
488 |
|
489 lemma int_bit_bound: |
|
490 fixes k :: int |
|
491 obtains n where \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close> |
|
492 and \<open>n > 0 \<Longrightarrow> bit k (n - 1) \<noteq> bit k n\<close> |
|
493 proof - |
|
494 obtain q where *: \<open>\<And>m. q \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k q\<close> |
|
495 proof (cases \<open>k \<ge> 0\<close>) |
|
496 case True |
|
497 moreover from power_gt_expt [of 2 \<open>nat k\<close>] |
|
498 have \<open>k < 2 ^ nat k\<close> by simp |
|
499 ultimately have *: \<open>k div 2 ^ nat k = 0\<close> |
|
500 by simp |
|
501 show thesis |
|
502 proof (rule that [of \<open>nat k\<close>]) |
|
503 fix m |
|
504 assume \<open>nat k \<le> m\<close> |
|
505 then show \<open>bit k m \<longleftrightarrow> bit k (nat k)\<close> |
|
506 by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq dest!: le_Suc_ex) |
|
507 qed |
|
508 next |
|
509 case False |
|
510 moreover from power_gt_expt [of 2 \<open>nat (- k)\<close>] |
|
511 have \<open>- k \<le> 2 ^ nat (- k)\<close> |
|
512 by simp |
|
513 ultimately have \<open>- k div - (2 ^ nat (- k)) = - 1\<close> |
|
514 by (subst div_pos_neg_trivial) simp_all |
|
515 then have *: \<open>k div 2 ^ nat (- k) = - 1\<close> |
|
516 by simp |
|
517 show thesis |
|
518 proof (rule that [of \<open>nat (- k)\<close>]) |
|
519 fix m |
|
520 assume \<open>nat (- k) \<le> m\<close> |
|
521 then show \<open>bit k m \<longleftrightarrow> bit k (nat (- k))\<close> |
|
522 by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq minus_1_div_exp_eq_int dest!: le_Suc_ex) |
|
523 qed |
|
524 qed |
|
525 show thesis |
|
526 proof (cases \<open>\<forall>m. bit k m \<longleftrightarrow> bit k q\<close>) |
|
527 case True |
|
528 then have \<open>bit k 0 \<longleftrightarrow> bit k q\<close> |
|
529 by blast |
|
530 with True that [of 0] show thesis |
|
531 by simp |
|
532 next |
|
533 case False |
|
534 then obtain r where **: \<open>bit k r \<noteq> bit k q\<close> |
|
535 by blast |
|
536 have \<open>r < q\<close> |
|
537 by (rule ccontr) (use * [of r] ** in simp) |
|
538 define N where \<open>N = {n. n < q \<and> bit k n \<noteq> bit k q}\<close> |
|
539 moreover have \<open>finite N\<close> \<open>r \<in> N\<close> |
|
540 using ** N_def \<open>r < q\<close> by auto |
|
541 moreover define n where \<open>n = Suc (Max N)\<close> |
|
542 ultimately have \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close> |
|
543 apply auto |
|
544 apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \<open>finite N\<close> all_not_in_conv mem_Collect_eq not_le) |
|
545 apply (metis "*" Max_ge Suc_n_not_le_n \<open>finite N\<close> linorder_not_less mem_Collect_eq) |
|
546 apply (metis "*" Max_ge Suc_n_not_le_n \<open>finite N\<close> linorder_not_less mem_Collect_eq) |
|
547 apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \<open>finite N\<close> all_not_in_conv mem_Collect_eq not_le) |
|
548 done |
|
549 have \<open>bit k (Max N) \<noteq> bit k n\<close> |
|
550 by (metis (mono_tags, lifting) "*" Max_in N_def \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m = bit k n\<close> \<open>finite N\<close> \<open>r \<in> N\<close> empty_iff le_cases mem_Collect_eq) |
|
551 show thesis apply (rule that [of n]) |
|
552 using \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m = bit k n\<close> apply blast |
|
553 using \<open>bit k (Max N) \<noteq> bit k n\<close> n_def by auto |
|
554 qed |
|
555 qed |
488 |
556 |
489 instantiation int :: ring_bit_operations |
557 instantiation int :: ring_bit_operations |
490 begin |
558 begin |
491 |
559 |
492 definition not_int :: \<open>int \<Rightarrow> int\<close> |
560 definition not_int :: \<open>int \<Rightarrow> int\<close> |