--- a/src/HOL/Euclidean_Division.thy Sat Jun 12 15:37:25 2021 +0200
+++ b/src/HOL/Euclidean_Division.thy Wed Jun 16 08:19:09 2021 +0000
@@ -1280,6 +1280,26 @@
by simp
qed
+lemma div_less_iff_less_mult:
+ \<open>m div q < n \<longleftrightarrow> m < n * q\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+ if \<open>q > 0\<close> for m n q :: nat
+proof
+ assume ?Q then show ?P
+ by (rule less_mult_imp_div_less)
+next
+ assume ?P
+ then obtain h where \<open>n = Suc (m div q + h)\<close>
+ using less_natE by blast
+ moreover have \<open>m < m + (Suc h * q - m mod q)\<close>
+ using that by (simp add: trans_less_add1)
+ ultimately show ?Q
+ by (simp add: algebra_simps flip: minus_mod_eq_mult_div)
+qed
+
+lemma less_eq_div_iff_mult_less_eq:
+ \<open>m \<le> n div q \<longleftrightarrow> m * q \<le> n\<close> if \<open>q > 0\<close> for m n q :: nat
+ using div_less_iff_less_mult [of q n m] that by auto
+
text \<open>A fact for the mutilated chess board\<close>
lemma mod_Suc:
--- a/src/HOL/Library/Word.thy Sat Jun 12 15:37:25 2021 +0200
+++ b/src/HOL/Library/Word.thy Wed Jun 16 08:19:09 2021 +0000
@@ -1150,6 +1150,11 @@
end
+lemma ucast_drop_bit_eq:
+ \<open>ucast (drop_bit n w) = drop_bit n (ucast w :: 'b::len word)\<close>
+ if \<open>LENGTH('a) \<le> LENGTH('b)\<close> for w :: \<open>'a::len word\<close>
+ by (rule bit_word_eqI) (use that in \<open>auto simp add: bit_unsigned_iff bit_drop_bit_eq dest: bit_imp_le_length\<close>)
+
context semiring_bit_operations
begin
@@ -3546,6 +3551,11 @@
(word_of_int (drop_bit (numeral n) (take_bit LENGTH('a) (numeral k))) :: 'a::len word)\<close>
by transfer simp
+lemma signed_drop_bit_word_numeral [simp]:
+ \<open>signed_drop_bit (numeral n) (numeral k) =
+ (word_of_int (drop_bit (numeral n) (signed_take_bit (LENGTH('a) - 1) (numeral k))) :: 'a::len word)\<close>
+ by transfer simp
+
lemma False_map2_or: "\<lbrakk>set xs \<subseteq> {False}; length ys = length xs\<rbrakk> \<Longrightarrow> map2 (\<or>) xs ys = ys"
by (induction xs arbitrary: ys) (auto simp: length_Suc_conv)
@@ -4167,8 +4177,6 @@
lemma word_rec_in2: "f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> (+) 1) n"
by (induct n) (simp_all add: word_rec_Suc)
-
-
lemma word_rec_twice:
"m \<le> n \<Longrightarrow> word_rec z f n = word_rec (word_rec z f (n - m)) (f \<circ> (+) (n - m)) m"
proof (induction n arbitrary: z f)
--- a/src/HOL/Parity.thy Sat Jun 12 15:37:25 2021 +0200
+++ b/src/HOL/Parity.thy Wed Jun 16 08:19:09 2021 +0000
@@ -1556,6 +1556,34 @@
by (simp add: min_def)
qed
+lemma take_bit_eq_self_iff_drop_bit_eq_0:
+ \<open>take_bit n a = a \<longleftrightarrow> drop_bit n a = 0\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+proof
+ assume ?P
+ show ?Q
+ proof (rule bit_eqI)
+ fix m
+ from \<open>?P\<close> have \<open>a = take_bit n a\<close> ..
+ also have \<open>\<not> bit (take_bit n a) (n + m)\<close>
+ unfolding bit_simps
+ by (simp add: bit_simps)
+ finally show \<open>bit (drop_bit n a) m \<longleftrightarrow> bit 0 m\<close>
+ by (simp add: bit_simps)
+ qed
+next
+ assume ?Q
+ show ?P
+ proof (rule bit_eqI)
+ fix m
+ from \<open>?Q\<close> have \<open>\<not> bit (drop_bit n a) (m - n)\<close>
+ by simp
+ then have \<open> \<not> bit a (n + (m - n))\<close>
+ by (simp add: bit_simps)
+ then show \<open>bit (take_bit n a) m \<longleftrightarrow> bit a m\<close>
+ by (cases \<open>m < n\<close>) (auto simp add: bit_simps)
+ qed
+qed
+
end
instantiation nat :: semiring_bit_shifts