--- a/src/HOL/Divides.thy Tue Sep 15 08:57:47 2020 +0200
+++ b/src/HOL/Divides.thy Thu Sep 17 09:57:30 2020 +0000
@@ -1251,6 +1251,87 @@
code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
+subsection \<open>More on bit operations\<close>
+
+lemma take_bit_incr_eq:
+ \<open>take_bit n (k + 1) = 1 + take_bit n k\<close> if \<open>take_bit n k \<noteq> 2 ^ n - 1\<close>
+ for k :: int
+proof -
+ from that have \<open>2 ^ n \<noteq> k mod 2 ^ n + 1\<close>
+ by (simp add: take_bit_eq_mod)
+ moreover have \<open>k mod 2 ^ n < 2 ^ n\<close>
+ by simp
+ ultimately have *: \<open>k mod 2 ^ n + 1 < 2 ^ n\<close>
+ by linarith
+ have \<open>(k + 1) mod 2 ^ n = (k mod 2 ^ n + 1) mod 2 ^ n\<close>
+ by (simp add: mod_simps)
+ also have \<open>\<dots> = k mod 2 ^ n + 1\<close>
+ using * by (simp add: zmod_trival_iff)
+ finally have \<open>(k + 1) mod 2 ^ n = k mod 2 ^ n + 1\<close> .
+ then show ?thesis
+ by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_decr_eq:
+ \<open>take_bit n (k - 1) = take_bit n k - 1\<close> if \<open>take_bit n k \<noteq> 0\<close>
+ for k :: int
+proof -
+ from that have \<open>k mod 2 ^ n \<noteq> 0\<close>
+ by (simp add: take_bit_eq_mod)
+ moreover have \<open>k mod 2 ^ n \<ge> 0\<close> \<open>k mod 2 ^ n < 2 ^ n\<close>
+ by simp_all
+ ultimately have *: \<open>k mod 2 ^ n > 0\<close>
+ by linarith
+ have \<open>(k - 1) mod 2 ^ n = (k mod 2 ^ n - 1) mod 2 ^ n\<close>
+ by (simp add: mod_simps)
+ also have \<open>\<dots> = k mod 2 ^ n - 1\<close>
+ by (simp add: zmod_trival_iff)
+ (use \<open>k mod 2 ^ n < 2 ^ n\<close> * in linarith)
+ finally have \<open>(k - 1) mod 2 ^ n = k mod 2 ^ n - 1\<close> .
+ then show ?thesis
+ by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_int_less_eq_self_iff:
+ \<open>take_bit n k \<le> k \<longleftrightarrow> 0 \<le> k\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+ for k :: int
+proof
+ assume ?P
+ show ?Q
+ proof (rule ccontr)
+ assume \<open>\<not> 0 \<le> k\<close>
+ then have \<open>k < 0\<close>
+ by simp
+ with \<open>?P\<close>
+ have \<open>take_bit n k < 0\<close>
+ by (rule le_less_trans)
+ then show False
+ by simp
+ qed
+next
+ assume ?Q
+ then show ?P
+ by (simp add: take_bit_eq_mod zmod_le_nonneg_dividend)
+qed
+
+lemma take_bit_int_less_self_iff:
+ \<open>take_bit n k < k \<longleftrightarrow> 2 ^ n \<le> k\<close>
+ for k :: int
+ by (auto simp add: less_le take_bit_int_less_eq_self_iff take_bit_int_eq_self_iff
+ intro: order_trans [of 0 \<open>2 ^ n\<close> k])
+
+lemma take_bit_int_greater_self_iff:
+ \<open>k < take_bit n k \<longleftrightarrow> k < 0\<close>
+ for k :: int
+ using take_bit_int_less_eq_self_iff [of n k] by auto
+
+lemma take_bit_int_greater_eq_self_iff:
+ \<open>k \<le> take_bit n k \<longleftrightarrow> k < 2 ^ n\<close>
+ for k :: int
+ by (auto simp add: le_less take_bit_int_greater_self_iff take_bit_int_eq_self_iff
+ dest: sym not_sym intro: less_trans [of k 0 \<open>2 ^ n\<close>])
+
+
subsection \<open>Lemmas of doubtful value\<close>
lemma div_geq: "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat