# HG changeset patch
# User haftmann
# Date 1623831549 0
# Node ID 52b829b18066a2385bec05e978bb4e6b8e4706f0
# Parent  adb34395b622183206f97e8ec185dd79ff915e7a
more lemmas

diff -r adb34395b622 -r 52b829b18066 src/HOL/Euclidean_Division.thy
--- 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:
diff -r adb34395b622 -r 52b829b18066 src/HOL/Library/Word.thy
--- 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)
diff -r adb34395b622 -r 52b829b18066 src/HOL/Parity.thy
--- 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