# HG changeset patch
# User haftmann
# Date 1591299532 0
# Node ID 2c6a5c709f2271abd05ed1826b622d7544ae1e9a
# Parent  a238074c5a9d8c4468196025e716c6de2e372597
more theorems

diff -r a238074c5a9d -r 2c6a5c709f22 src/HOL/ex/Bit_Operations.thy
--- a/src/HOL/ex/Bit_Operations.thy	Thu Jun 04 19:38:50 2020 +0000
+++ b/src/HOL/ex/Bit_Operations.thy	Thu Jun 04 19:38:52 2020 +0000
@@ -230,6 +230,34 @@
   apply (use local.exp_eq_0_imp_not_bit in blast)
   done
 
+lemma take_bit_minus_one_eq_mask:
+  \<open>take_bit n (- 1) = mask n\<close>
+  by (simp add: bit_eq_iff bit_mask_iff bit_take_bit_iff conj_commute)
+
+lemma push_bit_minus_one_eq_not_mask:
+  \<open>push_bit n (- 1) = NOT (mask n)\<close>
+proof (rule bit_eqI)
+  fix m
+  assume \<open>2 ^ m \<noteq> 0\<close>
+  show \<open>bit (push_bit n (- 1)) m \<longleftrightarrow> bit (NOT (mask n)) m\<close>
+  proof (cases \<open>n \<le> m\<close>)
+    case True
+    moreover define q where \<open>q = m - n\<close>
+    ultimately have \<open>m = n + q\<close> \<open>m - n = q\<close>
+      by simp_all
+    with \<open>2 ^ m \<noteq> 0\<close> have \<open>2 ^ n * 2 ^ q \<noteq> 0\<close>
+      by (simp add: power_add)
+    then have \<open>2 ^ q \<noteq> 0\<close>
+      using mult_not_zero by blast
+    with \<open>m - n = q\<close> show ?thesis
+      by (auto simp add: bit_not_iff bit_mask_iff bit_push_bit_iff not_less)
+  next
+    case False
+    then show ?thesis
+      by (simp add: bit_not_iff bit_mask_iff bit_push_bit_iff not_le)
+  qed
+qed
+
 definition set_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   where \<open>set_bit n a = a OR 2 ^ n\<close>