# HG changeset patch
# User haftmann
# Date 1594448464 0
# Node ID a851ce626b7808f7fa79c10ca6d5e9086eba8985
# Parent  febdd4eead565d58a03512a2f2e1b861beafe838
signed_take_bit

diff -r febdd4eead56 -r a851ce626b78 NEWS
--- a/NEWS	Sat Jul 11 06:21:02 2020 +0000
+++ b/NEWS	Sat Jul 11 06:21:04 2020 +0000
@@ -75,10 +75,10 @@
 into its components "drop_bit" and "take_bit".  INCOMPATIBILITY.
 
 * Session HOL-Word: Operations "bin_last", "bin_rest", "bin_nth",
-"bintrunc" and "max_word" are now mere input abbreviations.
+"bintrunc", "sbintrunc" and "max_word" are now mere input abbreviations.
 Minor INCOMPATIBILITY.
 
-* Session HOL-Word: Theory Z2 is not used any longer.
+* Session HOL-Word: Theory HOL-Library.Z2 is not imported any longer.
 Minor INCOMPATIBILITY.
 
 * Session HOL-Word: Operations lsb, msb and set_bit are separated
diff -r febdd4eead56 -r a851ce626b78 src/HOL/Library/Bit_Operations.thy
--- a/src/HOL/Library/Bit_Operations.thy	Sat Jul 11 06:21:02 2020 +0000
+++ b/src/HOL/Library/Bit_Operations.thy	Sat Jul 11 06:21:04 2020 +0000
@@ -9,6 +9,43 @@
     Main
 begin
 
+subsection \<open>Preliminiaries\<close> \<comment> \<open>TODO move\<close>
+
+lemma take_bit_int_less_exp:
+  \<open>take_bit n k < 2 ^ n\<close> for k :: int
+  by (simp add: take_bit_eq_mod)
+
+lemma take_bit_Suc_from_most:
+  \<open>take_bit (Suc n) k = 2 ^ n * of_bool (bit k n) + take_bit n k\<close> for k :: int
+  by (simp only: take_bit_eq_mod power_Suc2) (simp_all add: bit_iff_odd odd_iff_mod_2_eq_one zmod_zmult2_eq)
+
+lemma take_bit_greater_eq:
+  \<open>k + 2 ^ n \<le> take_bit n k\<close> if \<open>k < 0\<close> for k :: int
+proof -
+  have \<open>k + 2 ^ n \<le> take_bit n (k + 2 ^ n)\<close>
+  proof (cases \<open>k > - (2 ^ n)\<close>)
+    case False
+    then have \<open>k + 2 ^ n \<le> 0\<close>
+      by simp
+    also note take_bit_nonnegative
+    finally show ?thesis .
+  next
+    case True
+    with that have \<open>0 \<le> k + 2 ^ n\<close> and \<open>k + 2 ^ n < 2 ^ n\<close>
+      by simp_all
+    then show ?thesis
+      by (simp only: take_bit_eq_mod mod_pos_pos_trivial)
+  qed
+  then show ?thesis
+    by (simp add: take_bit_eq_mod)
+qed
+
+lemma take_bit_less_eq:
+  \<open>take_bit n k \<le> k - 2 ^ n\<close> if \<open>2 ^ n \<le> k\<close> and \<open>n > 0\<close> for k :: int
+  using that zmod_le_nonneg_dividend [of \<open>k - 2 ^ n\<close> \<open>2 ^ n\<close>]
+  by (simp add: take_bit_eq_mod)
+
+
 subsection \<open>Bit operations\<close>
 
 class semiring_bit_operations = semiring_bit_shifts +
@@ -240,29 +277,17 @@
   \<open>take_bit n (- 1) = mask n\<close>
   by (simp add: bit_eq_iff bit_mask_iff bit_take_bit_iff conj_commute)
 
+lemma minus_exp_eq_not_mask:
+  \<open>- (2 ^ n) = NOT (mask n)\<close>
+  by (rule bit_eqI) (simp add: bit_minus_iff bit_not_iff flip: mask_eq_exp_minus_1)
+
 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
+  by (simp add: push_bit_eq_mult minus_exp_eq_not_mask)
+
+lemma take_bit_not_mask_eq_0:
+  \<open>take_bit m (NOT (mask n)) = 0\<close> if \<open>n \<ge> m\<close>
+  by (rule bit_eqI) (use that in \<open>simp add: bit_take_bit_iff bit_not_iff bit_mask_iff\<close>)
 
 definition set_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
   where \<open>set_bit n a = a OR push_bit n 1\<close>
@@ -645,6 +670,10 @@
   \<open>k XOR l < 0 \<longleftrightarrow> (k < 0) \<noteq> (l < 0)\<close> for k l :: int
   by (subst Not_eq_iff [symmetric]) (auto simp add: not_less)
 
+lemma mask_nonnegative:
+  \<open>(mask n :: int) \<ge> 0\<close>
+ by (simp add: mask_eq_exp_minus_1)  
+
 lemma set_bit_nonnegative_int_iff [simp]:
   \<open>set_bit n k \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
   by (simp add: set_bit_def)
@@ -724,6 +753,194 @@
 qed
 
 
+subsection \<open>Taking bit with sign propagation\<close>
+
+definition signed_take_bit :: "nat \<Rightarrow> int \<Rightarrow> int"
+  where \<open>signed_take_bit n k = take_bit n k OR (NOT (mask n) * of_bool (bit k n))\<close>
+
+lemma signed_take_bit_eq:
+  \<open>signed_take_bit n k = take_bit n k\<close> if \<open>\<not> bit k n\<close>
+  using that by (simp add: signed_take_bit_def)
+
+lemma signed_take_bit_eq_or:
+  \<open>signed_take_bit n k = take_bit n k OR NOT (mask n)\<close> if \<open>bit k n\<close>
+  using that by (simp add: signed_take_bit_def)
+
+lemma signed_take_bit_0 [simp]:
+  \<open>signed_take_bit 0 k = - (k mod 2)\<close>
+  by (simp add: signed_take_bit_def odd_iff_mod_2_eq_one)
+
+lemma mask_half_int:
+  \<open>mask n div 2 = (mask (n - 1) :: int)\<close>
+  by (cases n) (simp_all add: mask_eq_exp_minus_1 algebra_simps)
+
+lemma signed_take_bit_Suc:
+  \<open>signed_take_bit (Suc n) k = k mod 2 + 2 * signed_take_bit n (k div 2)\<close>
+  by (unfold signed_take_bit_def or_int_rec [of \<open>take_bit (Suc n) k\<close>])
+    (simp add: bit_Suc take_bit_Suc even_or_iff even_mask_iff odd_iff_mod_2_eq_one not_int_div_2 mask_half_int)
+
+lemma signed_take_bit_rec:
+  \<open>signed_take_bit n k = (if n = 0 then - (k mod 2) else k mod 2 + 2 * signed_take_bit (n - 1) (k div 2))\<close>
+  by (cases n) (simp_all add: signed_take_bit_Suc)
+
+lemma bit_signed_take_bit_iff:
+  \<open>bit (signed_take_bit m k) n = bit k (min m n)\<close>
+  by (simp add: signed_take_bit_def bit_or_iff bit_take_bit_iff bit_not_iff bit_mask_iff min_def)
+
+text \<open>Modulus centered around 0\<close>
+
+lemma signed_take_bit_eq_take_bit_minus:
+  \<open>signed_take_bit n k = take_bit (Suc n) k - 2 ^ Suc n * of_bool (bit k n)\<close>
+proof (cases \<open>bit k n\<close>)
+  case True
+  have \<open>signed_take_bit n k = take_bit (Suc n) k OR NOT (mask (Suc n))\<close>
+    by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff bit_or_iff bit_not_iff bit_mask_iff less_Suc_eq True)
+  then have \<open>signed_take_bit n k = take_bit (Suc n) k + NOT (mask (Suc n))\<close>
+    by (simp add: disjunctive_add bit_take_bit_iff bit_not_iff bit_mask_iff)
+  with True show ?thesis
+    by (simp flip: minus_exp_eq_not_mask)
+next
+  case False
+  then show ?thesis
+    by (simp add: bit_eq_iff bit_take_bit_iff bit_signed_take_bit_iff min_def)
+      (auto intro: bit_eqI simp add: less_Suc_eq)
+qed
+
+lemma signed_take_bit_eq_take_bit_shift:
+  \<open>signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n\<close>
+proof -
+  have *: \<open>take_bit n k OR 2 ^ n = take_bit n k + 2 ^ n\<close>
+    by (simp add: disjunctive_add bit_exp_iff bit_take_bit_iff)
+  have \<open>take_bit n k - 2 ^ n = take_bit n k + NOT (mask n)\<close>
+    by (simp add: minus_exp_eq_not_mask)
+  also have \<open>\<dots> = take_bit n k OR NOT (mask n)\<close>
+    by (rule disjunctive_add)
+      (simp add: bit_exp_iff bit_take_bit_iff bit_not_iff bit_mask_iff)
+  finally have **: \<open>take_bit n k - 2 ^ n = take_bit n k OR NOT (mask n)\<close> .
+  have \<open>take_bit (Suc n) (k + 2 ^ n) = take_bit (Suc n) (take_bit (Suc n) k + take_bit (Suc n) (2 ^ n))\<close>
+    by (simp only: take_bit_add)
+  also have \<open>take_bit (Suc n) k = 2 ^ n * of_bool (bit k n) + take_bit n k\<close>
+    by (simp add: take_bit_Suc_from_most)
+  finally have \<open>take_bit (Suc n) (k + 2 ^ n) = take_bit (Suc n) (2 ^ (n + of_bool (bit k n)) + take_bit n k)\<close>
+    by (simp add: ac_simps)
+  also have \<open>2 ^ (n + of_bool (bit k n)) + take_bit n k = 2 ^ (n + of_bool (bit k n)) OR take_bit n k\<close>
+    by (rule disjunctive_add)
+      (auto simp add: disjunctive_add bit_take_bit_iff bit_double_iff bit_exp_iff)
+  finally show ?thesis
+    using * ** by (simp add: signed_take_bit_def take_bit_Suc min_def ac_simps)
+qed
+
+lemma signed_take_bit_of_0 [simp]:
+  \<open>signed_take_bit n 0 = 0\<close>
+  by (simp add: signed_take_bit_def)
+
+lemma signed_take_bit_of_minus_1 [simp]:
+  \<open>signed_take_bit n (- 1) = - 1\<close>
+  by (simp add: signed_take_bit_def take_bit_minus_one_eq_mask)
+
+lemma signed_take_bit_eq_iff_take_bit_eq:
+  \<open>signed_take_bit n k = signed_take_bit n l \<longleftrightarrow> take_bit (Suc n) k = take_bit (Suc n) l\<close>
+proof (cases \<open>bit k n \<longleftrightarrow> bit l n\<close>)
+  case True
+  moreover have \<open>take_bit n k OR NOT (mask n) = take_bit n k - 2 ^ n\<close>
+    for k :: int
+    by (auto simp add: disjunctive_add [symmetric] bit_not_iff bit_mask_iff bit_take_bit_iff minus_exp_eq_not_mask)
+  ultimately show ?thesis
+    by (simp add: signed_take_bit_def take_bit_Suc_from_most)
+next
+  case False
+  then have \<open>signed_take_bit n k \<noteq> signed_take_bit n l\<close> and \<open>take_bit (Suc n) k \<noteq> take_bit (Suc n) l\<close>
+    by (auto simp add: bit_eq_iff bit_take_bit_iff bit_signed_take_bit_iff min_def)
+  then show ?thesis
+    by simp
+qed
+
+lemma signed_take_bit_signed_take_bit [simp]:
+  \<open>signed_take_bit m (signed_take_bit n k) = signed_take_bit (min m n) k\<close>
+  by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_or_iff bit_not_iff bit_mask_iff bit_take_bit_iff)
+
+lemma take_bit_signed_take_bit:
+  \<open>take_bit m (signed_take_bit n k) = take_bit m k\<close> if \<open>m \<le> n\<close>
+  using that by (auto simp add: bit_eq_iff bit_take_bit_iff bit_signed_take_bit_iff min_def)
+
+lemma take_bit_Suc_signed_take_bit [simp]:
+  \<open>take_bit (Suc n) (signed_take_bit n a) = take_bit (Suc n) a\<close>
+  by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def less_Suc_eq)
+
+lemma signed_take_bit_take_bit:
+  \<open>signed_take_bit m (take_bit n k) = (if n \<le> m then take_bit n else signed_take_bit m) k\<close>
+  by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff)
+
+lemma signed_take_bit_nonnegative_iff [simp]:
+  \<open>0 \<le> signed_take_bit n k \<longleftrightarrow> \<not> bit k n\<close>
+  by (simp add: signed_take_bit_def not_less mask_nonnegative)
+
+lemma signed_take_bit_negative_iff [simp]:
+  \<open>signed_take_bit n k < 0 \<longleftrightarrow> bit k n\<close>
+  by (simp add: signed_take_bit_def not_less mask_nonnegative)
+
+lemma signed_take_bit_greater_eq:
+  \<open>k + 2 ^ Suc n \<le> signed_take_bit n k\<close> if \<open>k < - (2 ^ n)\<close>
+  using that take_bit_greater_eq [of \<open>k + 2 ^ n\<close> \<open>Suc n\<close>]
+  by (simp add: signed_take_bit_eq_take_bit_shift)
+
+lemma signed_take_bit_less_eq:
+  \<open>signed_take_bit n k \<le> k - 2 ^ Suc n\<close> if \<open>k \<ge> 2 ^ n\<close>
+  using that take_bit_less_eq [of \<open>Suc n\<close> \<open>k + 2 ^ n\<close>]
+  by (simp add: signed_take_bit_eq_take_bit_shift)
+
+lemma signed_take_bit_Suc_1 [simp]:
+  \<open>signed_take_bit (Suc n) 1 = 1\<close>
+  by (simp add: signed_take_bit_Suc)
+
+lemma signed_take_bit_Suc_bit0 [simp]:
+  \<open>signed_take_bit (Suc n) (numeral (Num.Bit0 k)) = signed_take_bit n (numeral k) * 2\<close>
+  by (simp add: signed_take_bit_Suc)
+
+lemma signed_take_bit_Suc_bit1 [simp]:
+  \<open>signed_take_bit (Suc n) (numeral (Num.Bit1 k)) = signed_take_bit n (numeral k) * 2 + 1\<close>
+  by (simp add: signed_take_bit_Suc)
+
+lemma signed_take_bit_Suc_minus_bit0 [simp]:
+  \<open>signed_take_bit (Suc n) (- numeral (Num.Bit0 k)) = signed_take_bit n (- numeral k) * 2\<close>
+  by (simp add: signed_take_bit_Suc)
+
+lemma signed_take_bit_Suc_minus_bit1 [simp]:
+  \<open>signed_take_bit (Suc n) (- numeral (Num.Bit1 k)) = signed_take_bit n (- numeral k - 1) * 2 + 1\<close>
+  by (simp add: signed_take_bit_Suc)
+
+lemma signed_take_bit_numeral_bit0 [simp]:
+  \<open>signed_take_bit (numeral l) (numeral (Num.Bit0 k)) = signed_take_bit (pred_numeral l) (numeral k) * 2\<close>
+  by (simp add: signed_take_bit_rec)
+
+lemma signed_take_bit_numeral_bit1 [simp]:
+  \<open>signed_take_bit (numeral l) (numeral (Num.Bit1 k)) = signed_take_bit (pred_numeral l) (numeral k) * 2 + 1\<close>
+  by (simp add: signed_take_bit_rec)
+
+lemma signed_take_bit_numeral_minus_bit0 [simp]:
+  \<open>signed_take_bit (numeral l) (- numeral (Num.Bit0 k)) = signed_take_bit (pred_numeral l) (- numeral k) * 2\<close>
+  by (simp add: signed_take_bit_rec)
+
+lemma signed_take_bit_numeral_minus_bit1 [simp]:
+  \<open>signed_take_bit (numeral l) (- numeral (Num.Bit1 k)) = signed_take_bit (pred_numeral l) (- numeral k - 1) * 2 + 1\<close>
+  by (simp add: signed_take_bit_rec)
+
+lemma signed_take_bit_code [code]:
+  \<open>signed_take_bit n k =
+  (let l = k AND mask (Suc n)
+   in if bit l n then l - (push_bit n 2) else l)\<close>
+proof -
+  have *: \<open>(k AND mask (Suc n)) - 2 * 2 ^ n = k AND mask (Suc n) OR NOT (mask (Suc n))\<close>
+    apply (subst disjunctive_add [symmetric])
+    apply (simp_all add: bit_and_iff bit_mask_iff bit_not_iff)
+    apply (simp flip: minus_exp_eq_not_mask)
+    done
+  show ?thesis
+    by (rule bit_eqI)
+     (auto simp add: Let_def bit_and_iff bit_signed_take_bit_iff push_bit_eq_mult min_def not_le bit_mask_iff bit_exp_iff less_Suc_eq * bit_or_iff bit_not_iff)
+qed
+
+
 subsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
 
 instantiation nat :: semiring_bit_operations
diff -r febdd4eead56 -r a851ce626b78 src/HOL/Word/Ancient_Numeral.thy
--- a/src/HOL/Word/Ancient_Numeral.thy	Sat Jul 11 06:21:02 2020 +0000
+++ b/src/HOL/Word/Ancient_Numeral.thy	Sat Jul 11 06:21:04 2020 +0000
@@ -163,21 +163,21 @@
   by (cases n) auto
 
 lemmas sbintrunc_Suc_BIT [simp] =
-  sbintrunc.Suc [where bin="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b
+  signed_take_bit_Suc [where k="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b
 
 lemmas sbintrunc_0_BIT_B0 [simp] =
-  sbintrunc.Z [where bin="w BIT False", simplified bin_last_numeral_simps bin_rest_numeral_simps]
+  signed_take_bit_0 [where k="w BIT False", simplified bin_last_numeral_simps bin_rest_numeral_simps]
   for w
 
 lemmas sbintrunc_0_BIT_B1 [simp] =
-  sbintrunc.Z [where bin="w BIT True", simplified bin_last_BIT bin_rest_numeral_simps]
+  signed_take_bit_0 [where k="w BIT True", simplified bin_last_BIT bin_rest_numeral_simps]
   for w
 
 lemma sbintrunc_Suc_minus_Is:
   \<open>0 < n \<Longrightarrow>
   sbintrunc (n - 1) w = y \<Longrightarrow>
   sbintrunc n (w BIT b) = y BIT b\<close>
-  by (cases n) (simp_all add: Bit_def)
+  by (cases n) (simp_all add: Bit_def signed_take_bit_Suc)
 
 lemma bin_cat_Suc_Bit: "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
   by (auto simp add: Bit_def)
diff -r febdd4eead56 -r a851ce626b78 src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Sat Jul 11 06:21:02 2020 +0000
+++ b/src/HOL/Word/Bits_Int.thy	Sat Jul 11 06:21:04 2020 +0000
@@ -237,45 +237,33 @@
 lemma bin_sign_rest [simp]: "bin_sign (bin_rest w) = bin_sign w"
   by (simp add: bin_sign_def)
 
-abbreviation (input) bintrunc :: "nat \<Rightarrow> int \<Rightarrow> int"
+abbreviation (input) bintrunc :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
   where \<open>bintrunc \<equiv> take_bit\<close>
 
 lemma bintrunc_mod2p: "bintrunc n w = w mod 2 ^ n"
   by (fact take_bit_eq_mod)
 
-primrec sbintrunc :: "nat \<Rightarrow> int \<Rightarrow> int"
-  where
-    Z : "sbintrunc 0 bin = (if odd bin then - 1 else 0)"
-  | Suc : "sbintrunc (Suc n) bin = of_bool (odd bin) + 2 * sbintrunc n (bin div 2)"
+abbreviation (input) sbintrunc :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>sbintrunc \<equiv> signed_take_bit\<close>
 
 lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n"
-proof (induction n arbitrary: w)
-  case 0
-  then show ?case
-    by (auto simp add: odd_iff_mod_2_eq_one)
-next
-  case (Suc n)
-  from Suc [of \<open>w div 2\<close>]
-  show ?case
-    using even_succ_mod_exp [of \<open>(b * 2 + 2 * 2 ^ n)\<close> \<open>Suc (Suc n)\<close> for b :: int]
-    by (auto elim!: evenE oddE simp add: mult_mod_right ac_simps)
-qed
-
+  by (simp add: bintrunc_mod2p signed_take_bit_eq_take_bit_shift)
+  
 lemma sbintrunc_eq_take_bit:
   \<open>sbintrunc n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n\<close>
-  by (simp add: sbintrunc_mod2p take_bit_eq_mod)
+  by (fact signed_take_bit_eq_take_bit_shift)
 
 lemma sign_bintr: "bin_sign (bintrunc n w) = 0"
-  by (simp add: bintrunc_mod2p bin_sign_def)
+  by (simp add: bin_sign_def)
 
-lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0"
-  by (simp add: bintrunc_mod2p)
+lemma bintrunc_n_0: "bintrunc n 0 = 0"
+  by (fact take_bit_of_0)
 
-lemma sbintrunc_n_0 [simp]: "sbintrunc n 0 = 0"
-  by (simp add: sbintrunc_mod2p)
+lemma sbintrunc_n_0: "sbintrunc n 0 = 0"
+  by (fact signed_take_bit_of_0)
 
-lemma sbintrunc_n_minus1 [simp]: "sbintrunc n (- 1) = -1"
-  by (induct n) auto
+lemma sbintrunc_n_minus1: "sbintrunc n (- 1) = -1"
+  by (fact signed_take_bit_of_minus_1)
 
 lemma bintrunc_Suc_numeral:
   "bintrunc (Suc n) 1 = 1"
@@ -300,24 +288,16 @@
   "sbintrunc (Suc n) (numeral (Num.Bit1 w)) = 1 + 2 * sbintrunc n (numeral w)"
   "sbintrunc (Suc n) (- numeral (Num.Bit0 w)) = 2 * sbintrunc n (- numeral w)"
   "sbintrunc (Suc n) (- numeral (Num.Bit1 w)) = 1 + 2 * sbintrunc n (- numeral (w + Num.One))"
-  by simp_all
+  by (simp_all add: signed_take_bit_Suc)
 
-lemma bin_sign_lem: "(bin_sign (sbintrunc n bin) = -1) = bin_nth bin n"
-  apply (rule sym)
-  apply (induct n arbitrary: bin)
-   apply (simp_all add: bit_Suc bin_sign_def)
-  done
+lemma bin_sign_lem: "(bin_sign (sbintrunc n bin) = -1) = bit bin n"
+  using mask_nonnegative [of n] by (simp add: bin_sign_def not_le signed_take_bit_def)
 
 lemma nth_bintr: "bin_nth (bintrunc m w) n \<longleftrightarrow> n < m \<and> bin_nth w n"
   by (fact bit_take_bit_iff)
 
 lemma nth_sbintr: "bin_nth (sbintrunc m w) n = (if n < m then bin_nth w n else bin_nth w m)"
-  apply (induct n arbitrary: w m)
-   apply (case_tac m)
-    apply simp_all
-  apply (case_tac m)
-   apply (simp_all add: bit_Suc)
-  done
+  by (simp add: bit_signed_take_bit_iff min_def)
 
 lemma bin_nth_Bit0:
   "bin_nth (numeral (Num.Bit0 w)) n \<longleftrightarrow>
@@ -336,7 +316,7 @@
   by (simp add: min.absorb2)
 
 lemma sbintrunc_sbintrunc_l: "n \<le> m \<Longrightarrow> sbintrunc m (sbintrunc n w) = sbintrunc n w"
-  by (rule bin_eqI) (auto simp: nth_sbintr)
+  by (simp add: min_def)
 
 lemma bintrunc_bintrunc_ge: "n \<le> m \<Longrightarrow> bintrunc n (bintrunc m w) = bintrunc n w"
   by (rule bin_eqI) (auto simp: nth_bintr)
@@ -348,19 +328,19 @@
   by (rule bin_eqI) (auto simp: nth_sbintr min.absorb1 min.absorb2)
 
 lemmas sbintrunc_Suc_Pls =
-  sbintrunc.Suc [where bin="0", simplified bin_last_numeral_simps bin_rest_numeral_simps]
+  signed_take_bit_Suc [where k="0", simplified bin_last_numeral_simps bin_rest_numeral_simps]
 
 lemmas sbintrunc_Suc_Min =
-  sbintrunc.Suc [where bin="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps]
+  signed_take_bit_Suc [where k="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps]
 
 lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min
   sbintrunc_Suc_numeral
 
 lemmas sbintrunc_Pls =
-  sbintrunc.Z [where bin="0", simplified bin_last_numeral_simps bin_rest_numeral_simps]
+  signed_take_bit_0 [where k="0", simplified bin_last_numeral_simps bin_rest_numeral_simps]
 
 lemmas sbintrunc_Min =
-  sbintrunc.Z [where bin="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps]
+  signed_take_bit_0 [where k="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps]
 
 lemmas sbintrunc_0_simps =
   sbintrunc_Pls sbintrunc_Min
@@ -443,7 +423,7 @@
 
 lemma sbintrunc_numeral:
   "sbintrunc (numeral k) x = of_bool (odd x) + 2 * sbintrunc (pred_numeral k) (x div 2)"
-  by (simp add: numeral_eq_Suc)
+  by (simp add: numeral_eq_Suc signed_take_bit_Suc mod2_eq_if)
 
 lemma bintrunc_numeral_simps [simp]:
   "bintrunc (numeral k) (numeral (Num.Bit0 w)) =
@@ -490,42 +470,14 @@
     apply presburger
     done
 qed
-
-lemma take_bit_greater_eq:
-  \<open>k + 2 ^ n \<le> take_bit n k\<close> if \<open>k < 0\<close> for k :: int
-proof -
-  have \<open>k + 2 ^ n \<le> take_bit n (k + 2 ^ n)\<close>
-  proof (cases \<open>k > - (2 ^ n)\<close>)
-    case False
-    then have \<open>k + 2 ^ n \<le> 0\<close>
-      by simp
-    also note take_bit_nonnegative
-    finally show ?thesis .
-  next
-    case True
-    with that have \<open>0 \<le> k + 2 ^ n\<close> and \<open>k + 2 ^ n < 2 ^ n\<close>
-      by simp_all
-    then show ?thesis
-      by (simp only: take_bit_eq_mod mod_pos_pos_trivial)
-  qed
-  then show ?thesis
-    by (simp add: take_bit_eq_mod)
-qed
-
-lemma take_bit_less_eq:
-  \<open>take_bit n k \<le> k - 2 ^ n\<close> if \<open>2 ^ n \<le> k\<close> and \<open>n > 0\<close> for k :: int
-  using that zmod_le_nonneg_dividend [of \<open>k - 2 ^ n\<close> \<open>2 ^ n\<close>]
-  by (simp add: take_bit_eq_mod)
-    
+  
 lemma sbintrunc_inc:
   \<open>k + 2 ^ Suc n \<le> sbintrunc n k\<close> if \<open>k < - (2 ^ n)\<close>
-  using that take_bit_greater_eq [of \<open>k + 2 ^ n\<close> \<open>Suc n\<close>]
-  by (simp add: sbintrunc_eq_take_bit)
-
+  using that by (fact signed_take_bit_greater_eq)
+  
 lemma sbintrunc_dec:
   \<open>sbintrunc n k \<le> k - 2 ^ (Suc n)\<close> if \<open>k \<ge> 2 ^ n\<close>
-  using that take_bit_less_eq [of \<open>Suc n\<close> \<open>k + 2 ^ n\<close>]
-  by (simp add: sbintrunc_eq_take_bit)
+  using that by (fact signed_take_bit_less_eq)
 
 lemma bintr_ge0: "0 \<le> bintrunc n w"
   by (simp add: bintrunc_mod2p)
@@ -561,13 +513,13 @@
   by (auto simp add: take_bit_Suc)
 
 lemma bin_rest_strunc: "bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)"
-  by simp
+  by (simp add: signed_take_bit_Suc)
 
 lemma bintrunc_rest [simp]: "bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)"
   by (induct n arbitrary: bin) (simp_all add: take_bit_Suc)
 
 lemma sbintrunc_rest [simp]: "sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)"
-  by (induct n arbitrary: bin) simp_all
+  by (induct n arbitrary: bin) (simp_all add: signed_take_bit_Suc mod2_eq_if)
 
 lemma bintrunc_rest': "bintrunc n \<circ> bin_rest \<circ> bintrunc n = bin_rest \<circ> bintrunc n"
   by (rule ext) auto
@@ -590,21 +542,6 @@
 lemmas rco_sbintr = sbintrunc_rest'
   [THEN rco_lem [THEN fun_cong], unfolded o_def]
 
-lemma sbintrunc_code [code]:
-  "sbintrunc n k =
-  (let l = take_bit (Suc n) k
-   in if bit l n then l - push_bit n 2 else l)"
-proof (induction n arbitrary: k)
-  case 0
-  then show ?case
-    by (simp add: mod_2_eq_odd)
-next
-  case (Suc n)
-  from Suc [of \<open>k div 2\<close>]
-  show ?case
-    by (auto simp add: Let_def push_bit_eq_mult algebra_simps take_bit_Suc [of \<open>Suc n\<close>] bit_Suc elim!: evenE oddE)
-qed
-
 
 subsection \<open>Splitting and concatenation\<close>
 
@@ -1759,7 +1696,7 @@
   by (simp add: bl_to_bin_def sign_bl_bin')
 
 lemma bl_sbin_sign_aux: "hd (bin_to_bl_aux (Suc n) w bs) = (bin_sign (sbintrunc n w) = -1)"
-  by (induction n arbitrary: w bs) (simp_all add: bin_sign_def)
+  by (induction n arbitrary: w bs) (auto simp add: bin_sign_def even_iff_mod_2_eq_zero bit_Suc)
 
 lemma bl_sbin_sign: "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
   unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
diff -r febdd4eead56 -r a851ce626b78 src/HOL/Word/More_Word.thy
--- a/src/HOL/Word/More_Word.thy	Sat Jul 11 06:21:02 2020 +0000
+++ b/src/HOL/Word/More_Word.thy	Sat Jul 11 06:21:04 2020 +0000
@@ -13,4 +13,6 @@
   Misc_lsb
 begin
 
+declare signed_take_bit_Suc [simp]
+
 end
diff -r febdd4eead56 -r a851ce626b78 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sat Jul 11 06:21:02 2020 +0000
+++ b/src/HOL/Word/Word.thy	Sat Jul 11 06:21:04 2020 +0000
@@ -1757,7 +1757,7 @@
   have \<open>?P \<longleftrightarrow> bit (uint w) (LENGTH('a) - Suc 0)\<close>
     by (simp add: bit_uint_iff)
   also have \<open>\<dots> \<longleftrightarrow> ?Q\<close>
-    by (simp add: sint_uint bin_sign_def flip: bin_sign_lem)
+    by (simp add: sint_uint)
   finally show ?thesis .
 qed
 
@@ -4099,31 +4099,20 @@
 proof -
   obtain n where n: \<open>LENGTH('a) = Suc n\<close>
     by (cases \<open>LENGTH('a)\<close>) simp_all
+  have *: \<open>sint x + sint y + 2 ^ Suc n > signed_take_bit n (sint x + sint y) \<Longrightarrow> sint x + sint y \<ge> - (2 ^ n)\<close>
+    \<open>signed_take_bit n (sint x + sint y) > sint x + sint y - 2 ^ Suc n \<Longrightarrow> 2 ^ n > sint x + sint y\<close>
+    using signed_take_bit_greater_eq [of \<open>sint x + sint y\<close> n] signed_take_bit_less_eq [of n \<open>sint x + sint y\<close>]
+    by (auto intro: ccontr)
   have \<open>sint x + sint y = sint (x + y) \<longleftrightarrow>
     (sint (x + y) < 0 \<longleftrightarrow> sint x < 0) \<or>
     (sint (x + y) < 0 \<longleftrightarrow> sint y < 0)\<close>
-    apply safe
-         apply simp_all
-       apply (unfold sint_word_ariths)
-       apply (unfold word_sbin.set_iff_norm [symmetric] sints_num)
-       apply safe
-           apply (insert sint_range' [where x=x])
-           apply (insert sint_range' [where x=y])
-           defer
-           apply (simp (no_asm), arith)
-          apply (simp (no_asm), arith)
-         defer
-         defer
-         apply (simp (no_asm), arith)
-        apply (simp (no_asm), arith)
-       apply (simp_all add: n not_less)
-       apply (rule notI [THEN notnotD],
-         drule leI not_le_imp_less,
-         drule sbintrunc_inc sbintrunc_dec,
-         simp)+
+    using sint_range' [of x] sint_range' [of y]
+    apply (auto simp add: not_less)
+       apply (unfold sint_word_ariths word_sbin.set_iff_norm [symmetric] sints_num)
+       apply (auto simp add: signed_take_bit_eq_take_bit_minus take_bit_Suc_from_most n not_less intro!: *)
     done
   then show ?thesis
-    apply (simp add: word_size shiftr_word_eq  drop_bit_eq_zero_iff_not_bit_last bit_and_iff bit_xor_iff)
+    apply (simp add: word_size shiftr_word_eq drop_bit_eq_zero_iff_not_bit_last bit_and_iff bit_xor_iff)
     apply (simp add: bit_last_iff)
     done
 qed
diff -r febdd4eead56 -r a851ce626b78 src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy	Sat Jul 11 06:21:02 2020 +0000
+++ b/src/HOL/ex/Word.thy	Sat Jul 11 06:21:04 2020 +0000
@@ -10,92 +10,6 @@
     "HOL-Library.Bit_Operations"
 begin
 
-subsection \<open>Preliminaries\<close>
-
-definition signed_take_bit :: "nat \<Rightarrow> int \<Rightarrow> int"
-  where signed_take_bit_eq_take_bit:
-    "signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n"
-
-lemma signed_take_bit_eq_take_bit':
-  "signed_take_bit (n - Suc 0) k = take_bit n (k + 2 ^ (n - 1)) - 2 ^ (n - 1)" if "n > 0"
-  using that by (simp add: signed_take_bit_eq_take_bit)
-
-lemma signed_take_bit_0 [simp]:
-  "signed_take_bit 0 k = - (k mod 2)"
-proof (cases "even k")
-  case True
-  then have "odd (k + 1)"
-    by simp
-  then have "(k + 1) mod 2 = 1"
-    by (simp add: even_iff_mod_2_eq_zero)
-  with True show ?thesis
-    by (simp add: signed_take_bit_eq_take_bit take_bit_Suc)
-next
-  case False
-  then show ?thesis
-    by (simp add: signed_take_bit_eq_take_bit odd_iff_mod_2_eq_one take_bit_Suc)
-qed
-
-lemma signed_take_bit_Suc:
-  "signed_take_bit (Suc n) k = k mod 2 + 2 * signed_take_bit n (k div 2)"
-  by (simp add: odd_iff_mod_2_eq_one signed_take_bit_eq_take_bit algebra_simps take_bit_Suc)
-
-lemma signed_take_bit_of_0 [simp]:
-  "signed_take_bit n 0 = 0"
-  by (simp add: signed_take_bit_eq_take_bit take_bit_eq_mod)
-
-lemma signed_take_bit_of_minus_1 [simp]:
-  "signed_take_bit n (- 1) = - 1"
-  by (induct n) (simp_all add: signed_take_bit_Suc)
-
-lemma signed_take_bit_eq_iff_take_bit_eq:
-  "signed_take_bit (n - Suc 0) k = signed_take_bit (n - Suc 0) l \<longleftrightarrow> take_bit n k = take_bit n l" (is "?P \<longleftrightarrow> ?Q")
-  if "n > 0"
-proof -
-  from that obtain m where m: "n = Suc m"
-    by (cases n) auto
-  show ?thesis
-  proof
-    assume ?Q
-    have "take_bit (Suc m) (k + 2 ^ m) =
-      take_bit (Suc m) (take_bit (Suc m) k + take_bit (Suc m) (2 ^ m))"
-      by (simp only: take_bit_add)
-    also have "\<dots> =
-      take_bit (Suc m) (take_bit (Suc m) l + take_bit (Suc m) (2 ^ m))"
-      by (simp only: \<open>?Q\<close> m [symmetric])
-    also have "\<dots> = take_bit (Suc m) (l + 2 ^ m)"
-      by (simp only: take_bit_add)
-    finally show ?P
-      by (simp only: signed_take_bit_eq_take_bit m) simp
-  next
-    assume ?P
-    with that have "(k + 2 ^ (n - Suc 0)) mod 2 ^ n = (l + 2 ^ (n - Suc 0)) mod 2 ^ n"
-      by (simp add: signed_take_bit_eq_take_bit' take_bit_eq_mod)
-    then have "(i + (k + 2 ^ (n - Suc 0))) mod 2 ^ n = (i + (l + 2 ^ (n - Suc 0))) mod 2 ^ n" for i
-      by (metis mod_add_eq)
-    then have "k mod 2 ^ n = l mod 2 ^ n"
-      by (metis add_diff_cancel_right' uminus_add_conv_diff)
-    then show ?Q
-      by (simp add: take_bit_eq_mod)
-  qed
-qed
-
-lemma signed_take_bit_code [code]:
-  \<open>signed_take_bit n k =
-  (let l = take_bit (Suc n) k
-   in if bit l n then l - push_bit n 2 else l)\<close>
-proof (induction n arbitrary: k)
-  case 0
-  then show ?case
-    by (simp add: mod_2_eq_odd and_one_eq)
-next
-  case (Suc n)
-  from Suc [of \<open>k div 2\<close>]
-  show ?case
-    by (auto simp add: Let_def push_bit_eq_mult algebra_simps take_bit_Suc [of \<open>Suc n\<close>] bit_Suc signed_take_bit_Suc elim!: evenE oddE)
-qed
-
-
 subsection \<open>Bit strings as quotient type\<close>
 
 subsubsection \<open>Basic properties\<close>
@@ -234,7 +148,8 @@
 
 lift_definition signed :: "'b::len word \<Rightarrow> 'a"
   is "of_int \<circ> signed_take_bit (LENGTH('b) - 1)"
-  by (simp add: signed_take_bit_eq_iff_take_bit_eq [symmetric])
+  by (cases \<open>LENGTH('b)\<close>)
+    (simp_all add: signed_take_bit_eq_iff_take_bit_eq [symmetric])
 
 lemma signed_0 [simp]:
   "signed 0 = 0"
@@ -277,7 +192,7 @@
 
 lemma of_int_signed [simp]:
   "of_int (signed a) = a"
-  by transfer (simp add: signed_take_bit_eq_take_bit take_bit_eq_mod mod_simps)
+  by (transfer; cases \<open>LENGTH('a)\<close>) simp_all
 
 
 subsubsection \<open>Properties\<close>