# HG changeset patch
# User haftmann
# Date 1603817984 0
# Node ID 83b5911c0164f833f7002832375cf798ba803182
# Parent  460d743010bc570fdad6e26fc16fdea435026d8f
more lemmas

diff -r 460d743010bc -r 83b5911c0164 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Oct 27 22:34:37 2020 +0100
+++ b/src/HOL/Int.thy	Tue Oct 27 16:59:44 2020 +0000
@@ -2102,6 +2102,10 @@
   "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
   by (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
 
+lemma sub_BitM_One_eq:
+  \<open>(Num.sub (Num.BitM n) num.One) = 2 * (Num.sub n Num.One :: int)\<close>
+  by (cases n) simp_all
+
 text \<open>Implementations.\<close>
 
 lemma one_int_code [code]: "1 = Pos Num.One"
diff -r 460d743010bc -r 83b5911c0164 src/HOL/Library/Bit_Operations.thy
--- a/src/HOL/Library/Bit_Operations.thy	Tue Oct 27 22:34:37 2020 +0100
+++ b/src/HOL/Library/Bit_Operations.thy	Tue Oct 27 16:59:44 2020 +0000
@@ -5,45 +5,10 @@
 
 theory Bit_Operations
   imports
+    Main
     "HOL-Library.Boolean_Algebra"
-    Main
 begin
 
-lemma sub_BitM_One_eq:
-  \<open>(Num.sub (Num.BitM n) num.One) = 2 * (Num.sub n Num.One :: int)\<close>
-  by (cases n) simp_all
-
-lemma bit_not_int_iff':
-  \<open>bit (- k - 1) n \<longleftrightarrow> \<not> bit k n\<close>
-  for k :: int
-proof (induction n arbitrary: k)
-  case 0
-  show ?case
-    by simp
-next
-  case (Suc n)
-  have \<open>(- k - 1) div 2 = - (k div 2) - 1\<close>
-    by simp
-  with Suc show ?case
-    by (simp add: bit_Suc)
-qed
-
-lemma bit_minus_int_iff:
-  \<open>bit (- k) n \<longleftrightarrow> \<not> bit (k - 1) n\<close>
-  for k :: int
-  using bit_not_int_iff' [of \<open>k - 1\<close>] by simp
-
-lemma bit_numeral_int_simps [simp]:
-  \<open>bit (1 :: int) (numeral n) \<longleftrightarrow> bit (0 :: int) (pred_numeral n)\<close>
-  \<open>bit (numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close>
-  \<open>bit (numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close>
-  \<open>bit (numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (- numeral w :: int) (pred_numeral n)\<close>
-  \<open>bit (- numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (- numeral w :: int) (pred_numeral n)\<close>
-  \<open>bit (- numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (numeral w :: int) (pred_numeral n)\<close>
-  \<open>bit (- numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> bit (- (numeral w) :: int) (pred_numeral n)\<close>
-  by (simp_all add: bit_1_iff numeral_eq_Suc bit_Suc add_One sub_inc_One_eq bit_minus_int_iff)
-
-
 subsection \<open>Bit operations\<close>
 
 class semiring_bit_operations = semiring_bit_shifts +
@@ -1570,6 +1535,10 @@
       (auto simp add: Let_def * bit_signed_take_bit_iff bit_take_bit_iff min_def less_Suc_eq bit_not_iff bit_mask_iff bit_or_iff)
 qed
 
+lemma not_minus_numeral_inc_eq:
+  \<open>NOT (- numeral (Num.inc n)) = (numeral n :: int)\<close>
+  by (simp add: not_int_def sub_inc_One_eq)
+
 
 subsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
 
diff -r 460d743010bc -r 83b5911c0164 src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Tue Oct 27 22:34:37 2020 +0100
+++ b/src/HOL/Numeral_Simprocs.thy	Tue Oct 27 16:59:44 2020 +0000
@@ -299,4 +299,14 @@
        Numeral_Simprocs.field_divide_cancel_numeral_factor])
 \<close>
 
+lemma bit_numeral_int_simps [simp]:
+  \<open>bit (1 :: int) (numeral n) \<longleftrightarrow> bit (0 :: int) (pred_numeral n)\<close>
+  \<open>bit (numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close>
+  \<open>bit (numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> bit (numeral w :: int) (pred_numeral n)\<close>
+  \<open>bit (numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (- numeral w :: int) (pred_numeral n)\<close>
+  \<open>bit (- numeral (num.Bit0 w) :: int) (numeral n) \<longleftrightarrow> bit (- numeral w :: int) (pred_numeral n)\<close>
+  \<open>bit (- numeral (num.Bit1 w) :: int) (numeral n) \<longleftrightarrow> \<not> bit (numeral w :: int) (pred_numeral n)\<close>
+  \<open>bit (- numeral (Num.BitM w) :: int) (numeral n) \<longleftrightarrow> bit (- (numeral w) :: int) (pred_numeral n)\<close>
+  by (simp_all add: bit_1_iff numeral_eq_Suc bit_Suc add_One sub_inc_One_eq bit_minus_int_iff)
+
 end
diff -r 460d743010bc -r 83b5911c0164 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Tue Oct 27 22:34:37 2020 +0100
+++ b/src/HOL/Parity.thy	Tue Oct 27 16:59:44 2020 +0000
@@ -1788,6 +1788,49 @@
 
 instance int :: unique_euclidean_semiring_with_bit_shifts ..
 
+lemma bit_not_int_iff':
+  \<open>bit (- k - 1) n \<longleftrightarrow> \<not> bit k n\<close>
+  for k :: int
+proof (induction n arbitrary: k)
+  case 0
+  show ?case
+    by simp
+next
+  case (Suc n)
+  have \<open>- k - 1 = - (k + 2) + 1\<close>
+    by simp
+  also have \<open>(- (k + 2) + 1) div 2 = - (k div 2) - 1\<close>
+  proof (cases \<open>even k\<close>)
+    case True
+    then have \<open>- k div 2 = - (k div 2)\<close>
+      by rule (simp flip: mult_minus_right)
+    with True show ?thesis
+      by simp
+  next
+    case False
+    have \<open>4 = 2 * (2::int)\<close>
+      by simp
+    also have \<open>2 * 2 div 2 = (2::int)\<close>
+      by (simp only: nonzero_mult_div_cancel_left)
+    finally have *: \<open>4 div 2 = (2::int)\<close> .
+    from False obtain l where k: \<open>k = 2 * l + 1\<close> ..
+    then have \<open>- k - 2 = 2 * - (l + 2) + 1\<close>
+      by simp
+    then have \<open>(- k - 2) div 2 + 1 = - (k div 2) - 1\<close>
+      by (simp flip: mult_minus_right add: *) (simp add: k)
+    with False show ?thesis
+      by simp
+  qed
+  finally have \<open>(- k - 1) div 2 = - (k div 2) - 1\<close> .
+  with Suc show ?case
+    by (simp add: bit_Suc)
+qed
+
+lemma bit_minus_int_iff:
+  \<open>bit (- k) n \<longleftrightarrow> \<not> bit (k - 1) n\<close>
+  for k :: int
+  using bit_not_int_iff' [of \<open>k - 1\<close>] by simp
+
 lemma bit_nat_iff:
   \<open>bit (nat k) n \<longleftrightarrow> k \<ge> 0 \<and> bit k n\<close>
 proof (cases \<open>k \<ge> 0\<close>)
diff -r 460d743010bc -r 83b5911c0164 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Oct 27 22:34:37 2020 +0100
+++ b/src/HOL/Word/Word.thy	Tue Oct 27 16:59:44 2020 +0000
@@ -120,13 +120,13 @@
 
 end
 
+lemma exp_eq_zero_iff [simp]:
+  \<open>2 ^ n = (0 :: 'a::len word) \<longleftrightarrow> n \<ge> LENGTH('a)\<close>
+  by transfer simp
+
 lemma word_exp_length_eq_0 [simp]:
   \<open>(2 :: 'a::len word) ^ LENGTH('a) = 0\<close>
-  by transfer simp
-
-lemma exp_eq_zero_iff:
-  \<open>2 ^ n = (0 :: 'a::len word) \<longleftrightarrow> n \<ge> LENGTH('a)\<close>
-  by transfer simp
+  by simp
 
 
 subsubsection \<open>Basic tool setup\<close>
@@ -1102,6 +1102,16 @@
 
 end
 
+context unique_euclidean_semiring_with_bit_shifts
+begin
+
+lemma unsigned_drop_bit_eq:
+  \<open>unsigned (drop_bit n w) = drop_bit n (take_bit LENGTH('b) (unsigned w))\<close>
+  for w :: \<open>'b::len word\<close>
+  by (rule bit_eqI) (auto simp add: bit_unsigned_iff bit_take_bit_iff bit_drop_bit_eq Parity.bit_drop_bit_eq dest: bit_imp_le_length)
+
+end
+
 context semiring_bit_operations
 begin
 
@@ -4548,15 +4558,29 @@
 subsection \<open>More\<close>
 
 lemma mask_1: "mask 1 = 1"
-  by transfer (simp add: min_def mask_Suc_exp)
+  by simp
 
 lemma mask_Suc_0: "mask (Suc 0) = 1"
-  using mask_1 by simp
+  by simp
 
 lemma bin_last_bintrunc: "odd (take_bit l n) \<longleftrightarrow> l > 0 \<and> odd n"
   by simp
 
 
+lemma push_bit_word_beyond [simp]:
+  \<open>push_bit n w = 0\<close> if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
+  using that by (transfer fixing: n) (simp add: take_bit_push_bit)
+
+lemma drop_bit_word_beyond [simp]:
+  \<open>drop_bit n w = 0\<close> if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
+  using that by (transfer fixing: n) (simp add: drop_bit_take_bit)
+
+lemma signed_drop_bit_beyond:
+  \<open>signed_drop_bit n w = (if bit w (LENGTH('a) - Suc 0) then - 1 else 0)\<close>
+  if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
+  by (rule bit_word_eqI) (simp add: bit_signed_drop_bit_iff that)
+
+
 subsection \<open>SMT support\<close>
 
 ML_file \<open>Tools/smt_word.ML\<close>