author haftmann Thu, 04 Jun 2020 19:38:52 +0000 changeset 71922 2c6a5c709f22 parent 71921 a238074c5a9d child 71923 7b34a932eeb6
more theorems
```--- 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

+  \<open>take_bit n (- 1) = mask n\<close>
+
+  \<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>
+    then have \<open>2 ^ q \<noteq> 0\<close>
+      using mult_not_zero by blast
+    with \<open>m - n = q\<close> show ?thesis