# HG changeset patch
# User haftmann
# Date 1594032450 0
# Node ID 379d0c207c291a6efafd0c57f0332290879cdafb
# Parent  720b72513ae54e22a6a41361adec004aae5e89ae
separation of traditional bit operations

diff -r 720b72513ae5 -r 379d0c207c29 NEWS
--- a/NEWS	Sun Jul 05 11:06:09 2020 +0200
+++ b/NEWS	Mon Jul 06 10:47:30 2020 +0000
@@ -77,6 +77,10 @@
 * Session HOL-Word: Theory Z2 is not used any longer.
 Minor INCOMPATIBILITY.
 
+* Session HOL-Word: Operations lsb, msb and set_bit are separated
+into theories Misc_lsb, Misc_msb and Misc_set_bit respectively.
+INCOMPATIBILITY.
+
 * Simproc defined_all and rewrite rule subst_all perform
 more aggressive substitution with variables from assumptions.
 INCOMPATIBILITY, use something like
diff -r 720b72513ae5 -r 379d0c207c29 src/HOL/Word/Ancient_Numeral.thy
--- a/src/HOL/Word/Ancient_Numeral.thy	Sun Jul 05 11:06:09 2020 +0200
+++ b/src/HOL/Word/Ancient_Numeral.thy	Mon Jul 06 10:47:30 2020 +0000
@@ -1,5 +1,5 @@
 theory Ancient_Numeral
-  imports Main Bits_Int
+  imports Main Bits_Int Misc_lsb Misc_msb
 begin
 
 definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int"  (infixl "BIT" 90)
diff -r 720b72513ae5 -r 379d0c207c29 src/HOL/Word/Bit_Comprehension.thy
--- a/src/HOL/Word/Bit_Comprehension.thy	Sun Jul 05 11:06:09 2020 +0200
+++ b/src/HOL/Word/Bit_Comprehension.thy	Mon Jul 06 10:47:30 2020 +0000
@@ -8,7 +8,7 @@
   imports Bits_Int
 begin
 
-class bit_comprehension = bit_operations +
+class bit_comprehension = semiring_bits +
   fixes set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a"  (binder "BITS " 10)
 
 instantiation int :: bit_comprehension
diff -r 720b72513ae5 -r 379d0c207c29 src/HOL/Word/Bits.thy
--- a/src/HOL/Word/Bits.thy	Sun Jul 05 11:06:09 2020 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(*  Title:      HOL/Word/Bits.thy
-    Author:     Brian Huffman, PSU and Gerwin Klein, NICTA
-*)
-
-section \<open>Syntactic type classes for bit operations\<close>
-
-theory Bits
-  imports Main "HOL-Library.Bit_Operations"
-begin
-
-class bit_operations =
-  fixes shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixl "<<" 55)
-    and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixl ">>" 55)
-  fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool"  (infixl "!!" 100)
-    and lsb :: "'a \<Rightarrow> bool"
-    and msb :: "'a \<Rightarrow> bool"
-    and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
-
-text \<open>
-  We want the bitwise operations to bind slightly weaker
-  than \<open>+\<close> and \<open>-\<close>, but \<open>~~\<close> to
-  bind slightly stronger than \<open>*\<close>.
-\<close>
-
-end
diff -r 720b72513ae5 -r 379d0c207c29 src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Sun Jul 05 11:06:09 2020 +0200
+++ b/src/HOL/Word/Bits_Int.thy	Mon Jul 06 10:47:30 2020 +0000
@@ -1,15 +1,13 @@
 (*  Title:      HOL/Word/Bits_Int.thy
     Author:     Jeremy Dawson and Gerwin Klein, NICTA
-
-Definitions and basic theorems for bit-wise logical operations
-for integers expressed using Pls, Min, BIT,
-and converting them to and from lists of bools.
 *)
 
 section \<open>Bitwise Operations on integers\<close>
 
 theory Bits_Int
-  imports Bits
+  imports
+    "HOL-Library.Bit_Operations"
+    Traditional_Syntax
 begin
 
 subsection \<open>Generic auxiliary\<close>
@@ -599,7 +597,7 @@
 proof (induction n arbitrary: k)
   case 0
   then show ?case
-    by (simp add: mod_2_eq_odd and_one_eq)
+    by (simp add: mod_2_eq_odd)
 next
   case (Suc n)
   from Suc [of \<open>k div 2\<close>]
@@ -1068,32 +1066,27 @@
     of_bool (odd w) + 2 * bin_sc (pred_numeral k) b (w div 2)"
   by (simp add: numeral_eq_Suc)
 
-instantiation int :: bit_operations
+instantiation int :: semiring_bit_syntax
 begin
 
 definition [iff]: "i !! n \<longleftrightarrow> bin_nth i n"
 
-definition "lsb i = i !! 0" for i :: int
-
-definition "set_bit i n b = bin_sc n b i"
-
 definition "shiftl x n = x * 2 ^ n" for x :: int
 
 definition "shiftr x n = x div 2 ^ n" for x :: int
 
-definition "msb x \<longleftrightarrow> x < 0" for x :: int
-
-instance ..
+instance by standard
+  (simp_all add: fun_eq_iff shiftl_int_def shiftr_int_def push_bit_eq_mult drop_bit_eq_div)
 
 end
 
 lemma shiftl_eq_push_bit:
   \<open>k << n = push_bit n k\<close> for k :: int
-  by (simp add: shiftl_int_def push_bit_eq_mult)
+  by (fact shiftl_eq_push_bit)
 
 lemma shiftr_eq_drop_bit:
   \<open>k >> n = drop_bit n k\<close> for k :: int
-  by (simp add: shiftr_int_def drop_bit_eq_div)
+  by (fact shiftr_eq_drop_bit)
 
 
 subsubsection \<open>Basic simplification rules\<close>
@@ -1598,54 +1591,6 @@
 
 subsection \<open>Setting and clearing bits\<close>
 
-lemma bin_last_conv_lsb: "bin_last = lsb"
-by(clarsimp simp add: lsb_int_def fun_eq_iff)
-
-lemma int_lsb_numeral [simp]:
-  "lsb (0 :: int) = False"
-  "lsb (1 :: int) = True"
-  "lsb (Numeral1 :: int) = True"
-  "lsb (- 1 :: int) = True"
-  "lsb (- Numeral1 :: int) = True"
-  "lsb (numeral (num.Bit0 w) :: int) = False"
-  "lsb (numeral (num.Bit1 w) :: int) = True"
-  "lsb (- numeral (num.Bit0 w) :: int) = False"
-  "lsb (- numeral (num.Bit1 w) :: int) = True"
-  by (simp_all add: lsb_int_def)
-
-lemma int_set_bit_0 [simp]: fixes x :: int shows
-  "set_bit x 0 b = of_bool b + 2 * (x div 2)"
-  by (auto simp add: set_bit_int_def intro: bin_rl_eqI)
-
-lemma int_set_bit_Suc: fixes x :: int shows
-  "set_bit x (Suc n) b = of_bool (odd x) + 2 * set_bit (x div 2) n b"
-  by (auto simp add: set_bit_int_def intro: bin_rl_eqI)
-
-lemma bin_last_set_bit:
-  "bin_last (set_bit x n b) = (if n > 0 then bin_last x else b)"
-  by (cases n) (simp_all add: int_set_bit_Suc)
-
-lemma bin_rest_set_bit: 
-  "bin_rest (set_bit x n b) = (if n > 0 then set_bit (x div 2) (n - 1) b else x div 2)"
-  by (cases n) (simp_all add: int_set_bit_Suc)
-
-lemma int_set_bit_numeral: fixes x :: int shows
-  "set_bit x (numeral w) b = of_bool (odd x) + 2 * set_bit (x div 2) (pred_numeral w) b"
-  by (simp add: set_bit_int_def)
-
-lemmas int_set_bit_numerals [simp] =
-  int_set_bit_numeral[where x="numeral w'"] 
-  int_set_bit_numeral[where x="- numeral w'"]
-  int_set_bit_numeral[where x="Numeral1"]
-  int_set_bit_numeral[where x="1"]
-  int_set_bit_numeral[where x="0"]
-  int_set_bit_Suc[where x="numeral w'"]
-  int_set_bit_Suc[where x="- numeral w'"]
-  int_set_bit_Suc[where x="Numeral1"]
-  int_set_bit_Suc[where x="1"]
-  int_set_bit_Suc[where x="0"]
-  for w'
-
 lemma int_shiftl_BIT: fixes x :: int
   shows int_shiftl0 [simp]: "x << 0 = x"
   and int_shiftl_Suc [simp]: "x << Suc n = 2 * (x << n)"
@@ -1766,47 +1711,6 @@
   "bin_sc n True i = i OR (1 << n)"
   by (induct n arbitrary: i) (rule bin_rl_eqI; simp)+
 
-lemma msb_conv_bin_sign: "msb x \<longleftrightarrow> bin_sign x = -1"
-by(simp add: bin_sign_def not_le msb_int_def)
-
-lemma msb_bin_rest [simp]: "msb (bin_rest x) = msb x"
-by(simp add: msb_int_def)
-
-lemma int_msb_and [simp]: "msb ((x :: int) AND y) \<longleftrightarrow> msb x \<and> msb y"
-by(simp add: msb_int_def)
-
-lemma int_msb_or [simp]: "msb ((x :: int) OR y) \<longleftrightarrow> msb x \<or> msb y"
-by(simp add: msb_int_def)
-
-lemma int_msb_xor [simp]: "msb ((x :: int) XOR y) \<longleftrightarrow> msb x \<noteq> msb y"
-by(simp add: msb_int_def)
-
-lemma int_msb_not [simp]: "msb (NOT (x :: int)) \<longleftrightarrow> \<not> msb x"
-by(simp add: msb_int_def not_less)
-
-lemma msb_shiftl [simp]: "msb ((x :: int) << n) \<longleftrightarrow> msb x"
-by(simp add: msb_int_def)
-
-lemma msb_shiftr [simp]: "msb ((x :: int) >> r) \<longleftrightarrow> msb x"
-by(simp add: msb_int_def)
-
-lemma msb_bin_sc [simp]: "msb (bin_sc n b x) \<longleftrightarrow> msb x"
-by(simp add: msb_conv_bin_sign)
-
-lemma msb_set_bit [simp]: "msb (set_bit (x :: int) n b) \<longleftrightarrow> msb x"
-by(simp add: msb_conv_bin_sign set_bit_int_def)
-
-lemma msb_0 [simp]: "msb (0 :: int) = False"
-by(simp add: msb_int_def)
-
-lemma msb_1 [simp]: "msb (1 :: int) = False"
-by(simp add: msb_int_def)
-
-lemma msb_numeral [simp]:
-  "msb (numeral n :: int) = False"
-  "msb (- numeral n :: int) = True"
-by(simp_all add: msb_int_def)
-
 
 subsection \<open>Semantic interpretation of \<^typ>\<open>bool list\<close> as \<^typ>\<open>int\<close>\<close>
 
diff -r 720b72513ae5 -r 379d0c207c29 src/HOL/Word/Misc_lsb.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Misc_lsb.thy	Mon Jul 06 10:47:30 2020 +0000
@@ -0,0 +1,87 @@
+(*  Author:     Jeremy Dawson, NICTA
+*)
+
+section \<open>Operation variant for the least significant bit\<close>
+
+theory Misc_lsb
+  imports Word
+begin
+
+class lsb = semiring_bits +
+  fixes lsb :: \<open>'a \<Rightarrow> bool\<close>
+  assumes lsb_odd: \<open>lsb = odd\<close>
+
+instantiation int :: lsb
+begin
+
+definition lsb_int :: \<open>int \<Rightarrow> bool\<close>
+  where \<open>lsb i = i !! 0\<close> for i :: int
+
+instance
+  by standard (simp add: fun_eq_iff lsb_int_def)
+
+end
+
+lemma bin_last_conv_lsb: "bin_last = lsb"
+  by (simp add: lsb_odd)
+
+lemma int_lsb_numeral [simp]:
+  "lsb (0 :: int) = False"
+  "lsb (1 :: int) = True"
+  "lsb (Numeral1 :: int) = True"
+  "lsb (- 1 :: int) = True"
+  "lsb (- Numeral1 :: int) = True"
+  "lsb (numeral (num.Bit0 w) :: int) = False"
+  "lsb (numeral (num.Bit1 w) :: int) = True"
+  "lsb (- numeral (num.Bit0 w) :: int) = False"
+  "lsb (- numeral (num.Bit1 w) :: int) = True"
+  by (simp_all add: lsb_int_def)
+
+instantiation word :: (len) lsb
+begin
+
+definition lsb_word :: \<open>'a word \<Rightarrow> bool\<close>
+  where word_lsb_def: \<open>lsb a \<longleftrightarrow> odd (uint a)\<close> for a :: \<open>'a word\<close>
+
+instance
+  apply standard
+  apply (simp add: fun_eq_iff word_lsb_def)
+  apply transfer apply simp
+  done
+
+end
+  
+lemma lsb_word_eq:
+  \<open>lsb = (odd :: 'a word \<Rightarrow> bool)\<close> for w :: \<open>'a::len word\<close>
+  by (fact lsb_odd)
+
+lemma word_lsb_alt: "lsb w = test_bit w 0"
+  for w :: "'a::len word"
+  by (auto simp: word_test_bit_def word_lsb_def)
+
+lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) \<and> \<not> lsb (0::'b::len word)"
+  unfolding word_lsb_def uint_eq_0 uint_1 by simp
+
+lemma word_lsb_last:
+  \<open>lsb w \<longleftrightarrow> last (to_bl w)\<close>
+  for w :: \<open>'a::len word\<close>
+  using nth_to_bl [of \<open>LENGTH('a) - Suc 0\<close> w]
+  by (simp add: lsb_odd last_conv_nth)
+
+lemma word_lsb_int: "lsb w \<longleftrightarrow> uint w mod 2 = 1"
+  apply (simp add: lsb_odd flip: odd_iff_mod_2_eq_one)
+  apply transfer
+  apply simp
+  done
+
+lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
+
+lemma word_lsb_numeral [simp]:
+  "lsb (numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (numeral bin)"
+  unfolding word_lsb_alt test_bit_numeral by simp
+
+lemma word_lsb_neg_numeral [simp]:
+  "lsb (- numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (- numeral bin)"
+  by (simp add: word_lsb_alt)
+
+end
diff -r 720b72513ae5 -r 379d0c207c29 src/HOL/Word/Misc_msb.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Misc_msb.thy	Mon Jul 06 10:47:30 2020 +0000
@@ -0,0 +1,126 @@
+(*  Author:     Jeremy Dawson, NICTA
+*)
+
+section \<open>Operation variant for the most significant bit\<close>
+
+theory Misc_msb
+  imports Word
+begin
+
+class msb =
+  fixes msb :: \<open>'a \<Rightarrow> bool\<close>
+
+instantiation int :: msb
+begin
+
+definition \<open>msb x \<longleftrightarrow> x < 0\<close> for x :: int
+
+instance ..
+
+end
+
+lemma msb_conv_bin_sign: "msb x \<longleftrightarrow> bin_sign x = -1"
+by(simp add: bin_sign_def not_le msb_int_def)
+
+lemma msb_bin_rest [simp]: "msb (bin_rest x) = msb x"
+by(simp add: msb_int_def)
+
+lemma int_msb_and [simp]: "msb ((x :: int) AND y) \<longleftrightarrow> msb x \<and> msb y"
+by(simp add: msb_int_def)
+
+lemma int_msb_or [simp]: "msb ((x :: int) OR y) \<longleftrightarrow> msb x \<or> msb y"
+by(simp add: msb_int_def)
+
+lemma int_msb_xor [simp]: "msb ((x :: int) XOR y) \<longleftrightarrow> msb x \<noteq> msb y"
+by(simp add: msb_int_def)
+
+lemma int_msb_not [simp]: "msb (NOT (x :: int)) \<longleftrightarrow> \<not> msb x"
+by(simp add: msb_int_def not_less)
+
+lemma msb_shiftl [simp]: "msb ((x :: int) << n) \<longleftrightarrow> msb x"
+by(simp add: msb_int_def)
+
+lemma msb_shiftr [simp]: "msb ((x :: int) >> r) \<longleftrightarrow> msb x"
+by(simp add: msb_int_def)
+
+lemma msb_bin_sc [simp]: "msb (bin_sc n b x) \<longleftrightarrow> msb x"
+by(simp add: msb_conv_bin_sign)
+
+lemma msb_0 [simp]: "msb (0 :: int) = False"
+by(simp add: msb_int_def)
+
+lemma msb_1 [simp]: "msb (1 :: int) = False"
+by(simp add: msb_int_def)
+
+lemma msb_numeral [simp]:
+  "msb (numeral n :: int) = False"
+  "msb (- numeral n :: int) = True"
+by(simp_all add: msb_int_def)
+
+instantiation word :: (len) msb
+begin
+
+definition msb_word :: \<open>'a word \<Rightarrow> bool\<close>
+  where \<open>msb a \<longleftrightarrow> bin_sign (sbintrunc (LENGTH('a) - 1) (uint a)) = - 1\<close>
+
+lemma msb_word_eq:
+  \<open>msb w \<longleftrightarrow> bit w (LENGTH('a) - 1)\<close> for w :: \<open>'a::len word\<close>
+  by (simp add: msb_word_def bin_sign_lem bit_uint_iff)
+
+instance ..
+
+end
+
+lemma word_msb_def:
+  "msb a \<longleftrightarrow> bin_sign (sint a) = - 1"
+  by (simp add: msb_word_def sint_uint)
+
+lemma word_msb_sint: "msb w \<longleftrightarrow> sint w < 0"
+  by (simp add: msb_word_eq bit_last_iff)
+
+lemma msb_word_of_int: "msb (word_of_int x::'a::len word) = bin_nth x (LENGTH('a) - 1)"
+  by (simp add: word_msb_def word_sbin.eq_norm bin_sign_lem)
+
+lemma word_msb_numeral [simp]:
+  "msb (numeral w::'a::len word) = bin_nth (numeral w) (LENGTH('a) - 1)"
+  unfolding word_numeral_alt by (rule msb_word_of_int)
+
+lemma word_msb_neg_numeral [simp]:
+  "msb (- numeral w::'a::len word) = bin_nth (- numeral w) (LENGTH('a) - 1)"
+  unfolding word_neg_numeral_alt by (rule msb_word_of_int)
+
+lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)"
+  by (simp add: word_msb_def bin_sign_def sint_uint sbintrunc_eq_take_bit)
+
+lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> LENGTH('a) = 1"
+  unfolding word_1_wi msb_word_of_int eq_iff [where 'a=nat]
+  by (simp add: Suc_le_eq)
+
+lemma word_msb_nth: "msb w = bin_nth (uint w) (LENGTH('a) - 1)"
+  for w :: "'a::len word"
+  by (simp add: word_msb_def sint_uint bin_sign_lem)
+
+lemma word_msb_alt: "msb w \<longleftrightarrow> hd (to_bl w)"
+  for w :: "'a::len word"
+  apply (simp add: msb_word_eq)
+  apply (subst hd_conv_nth)
+   apply simp
+  apply (subst nth_to_bl)
+   apply simp
+  apply simp
+  done
+
+lemma msb_nth: "msb w = w !! (LENGTH('a) - 1)"
+  for w :: "'a::len word"
+  by (simp add: word_msb_nth word_test_bit_def)
+
+lemma word_msb_n1 [simp]: "msb (-1::'a::len word)"
+  by (simp add: msb_word_eq exp_eq_zero_iff not_le)
+
+lemma msb_shift: "msb w \<longleftrightarrow> w >> (LENGTH('a) - 1) \<noteq> 0"
+  for w :: "'a::len word"
+  by (simp add: msb_word_eq shiftr_word_eq bit_iff_odd_drop_bit drop_bit_eq_zero_iff_not_bit_last)
+
+lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]]
+
+end
diff -r 720b72513ae5 -r 379d0c207c29 src/HOL/Word/Misc_set_bit.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Misc_set_bit.thy	Mon Jul 06 10:47:30 2020 +0000
@@ -0,0 +1,167 @@
+(*  Author:     Jeremy Dawson, NICTA
+*)
+
+section \<open>Operation variant for setting and unsetting bits\<close>
+
+theory Misc_set_bit
+  imports Word Misc_msb
+begin
+
+class set_bit = ring_bit_operations +
+  fixes set_bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a\<close>
+  assumes set_bit_eq: \<open>set_bit a n b = (if b then Bit_Operations.set_bit else unset_bit) n a\<close>
+
+instantiation int :: set_bit
+begin
+
+definition set_bit_int :: \<open>int \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> int\<close>
+  where \<open>set_bit i n b = bin_sc n b i\<close>
+
+instance
+  by standard (simp add: set_bit_int_def bin_sc_eq)
+
+end
+
+lemma int_set_bit_0 [simp]: fixes x :: int shows
+  "set_bit x 0 b = of_bool b + 2 * (x div 2)"
+  by (auto simp add: set_bit_int_def intro: bin_rl_eqI)
+
+lemma int_set_bit_Suc: fixes x :: int shows
+  "set_bit x (Suc n) b = of_bool (odd x) + 2 * set_bit (x div 2) n b"
+  by (auto simp add: set_bit_int_def intro: bin_rl_eqI)
+
+lemma bin_last_set_bit:
+  "bin_last (set_bit x n b) = (if n > 0 then bin_last x else b)"
+  by (cases n) (simp_all add: int_set_bit_Suc)
+
+lemma bin_rest_set_bit: 
+  "bin_rest (set_bit x n b) = (if n > 0 then set_bit (x div 2) (n - 1) b else x div 2)"
+  by (cases n) (simp_all add: int_set_bit_Suc)
+
+lemma int_set_bit_numeral: fixes x :: int shows
+  "set_bit x (numeral w) b = of_bool (odd x) + 2 * set_bit (x div 2) (pred_numeral w) b"
+  by (simp add: set_bit_int_def)
+
+lemmas int_set_bit_numerals [simp] =
+  int_set_bit_numeral[where x="numeral w'"] 
+  int_set_bit_numeral[where x="- numeral w'"]
+  int_set_bit_numeral[where x="Numeral1"]
+  int_set_bit_numeral[where x="1"]
+  int_set_bit_numeral[where x="0"]
+  int_set_bit_Suc[where x="numeral w'"]
+  int_set_bit_Suc[where x="- numeral w'"]
+  int_set_bit_Suc[where x="Numeral1"]
+  int_set_bit_Suc[where x="1"]
+  int_set_bit_Suc[where x="0"]
+  for w'
+
+lemma msb_set_bit [simp]: "msb (set_bit (x :: int) n b) \<longleftrightarrow> msb x"
+by(simp add: msb_conv_bin_sign set_bit_int_def)
+
+instantiation word :: (len) set_bit
+begin
+
+definition set_bit_word :: \<open>'a word \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a word\<close>
+  where word_set_bit_def: \<open>set_bit a n x = word_of_int (bin_sc n x (uint a))\<close>
+
+instance
+  apply standard
+  apply (simp add: word_set_bit_def bin_sc_eq Bit_Operations.set_bit_def unset_bit_def)
+  apply transfer
+  apply simp
+  done
+
+end
+
+lemma set_bit_unfold:
+  \<open>set_bit w n b = (if b then Bit_Operations.set_bit n w else unset_bit n w)\<close>
+  for w :: \<open>'a::len word\<close>
+  by (simp add: set_bit_eq)
+
+lemma bit_set_bit_word_iff:
+  \<open>bit (set_bit w m b) n \<longleftrightarrow> (if m = n then n < LENGTH('a) \<and> b else bit w n)\<close>
+  for w :: \<open>'a::len word\<close>
+  by (auto simp add: set_bit_unfold bit_unset_bit_iff bit_set_bit_iff exp_eq_zero_iff not_le bit_imp_le_length)
+
+lemma word_set_nth [simp]: "set_bit w n (test_bit w n) = w"
+  for w :: "'a::len word"
+  by (auto simp: word_test_bit_def word_set_bit_def)
+
+lemma test_bit_set: "(set_bit w n x) !! n \<longleftrightarrow> n < size w \<and> x"
+  for w :: "'a::len word"
+  by (auto simp: word_size word_test_bit_def word_set_bit_def word_ubin.eq_norm nth_bintr)
+
+lemma test_bit_set_gen:
+  "test_bit (set_bit w n x) m = (if m = n then n < size w \<and> x else test_bit w m)"
+  for w :: "'a::len word"
+  apply (unfold word_size word_test_bit_def word_set_bit_def)
+  apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen)
+  apply (auto elim!: test_bit_size [unfolded word_size]
+      simp add: word_test_bit_def [symmetric])
+  done
+
+lemma word_set_set_same [simp]: "set_bit (set_bit w n x) n y = set_bit w n y"
+  for w :: "'a::len word"
+  by (rule word_eqI) (simp add : test_bit_set_gen word_size)
+
+lemma word_set_set_diff:
+  fixes w :: "'a::len word"
+  assumes "m \<noteq> n"
+  shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x"
+  by (rule word_eqI) (auto simp: test_bit_set_gen word_size assms)
+
+lemma set_bit_word_of_int: "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)"
+  unfolding word_set_bit_def
+  by (rule word_eqI)(simp add: word_size bin_nth_sc_gen word_ubin.eq_norm nth_bintr)
+
+lemma word_set_numeral [simp]:
+  "set_bit (numeral bin::'a::len word) n b =
+    word_of_int (bin_sc n b (numeral bin))"
+  unfolding word_numeral_alt by (rule set_bit_word_of_int)
+
+lemma word_set_neg_numeral [simp]:
+  "set_bit (- numeral bin::'a::len word) n b =
+    word_of_int (bin_sc n b (- numeral bin))"
+  unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)
+
+lemma word_set_bit_0 [simp]: "set_bit 0 n b = word_of_int (bin_sc n b 0)"
+  unfolding word_0_wi by (rule set_bit_word_of_int)
+
+lemma word_set_bit_1 [simp]: "set_bit 1 n b = word_of_int (bin_sc n b 1)"
+  unfolding word_1_wi by (rule set_bit_word_of_int)
+
+lemma word_set_nth_iff: "set_bit w n b = w \<longleftrightarrow> w !! n = b \<or> n \<ge> size w"
+  for w :: "'a::len word"
+  apply (rule iffI)
+   apply (rule disjCI)
+   apply (drule word_eqD)
+   apply (erule sym [THEN trans])
+   apply (simp add: test_bit_set)
+  apply (erule disjE)
+   apply clarsimp
+  apply (rule word_eqI)
+  apply (clarsimp simp add : test_bit_set_gen)
+  apply (drule test_bit_size)
+  apply force
+  done
+
+lemma word_clr_le: "w \<ge> set_bit w n False"
+  for w :: "'a::len word"
+  apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
+  apply (rule order_trans)
+   apply (rule bintr_bin_clr_le)
+  apply simp
+  done
+
+lemma word_set_ge: "w \<le> set_bit w n True"
+  for w :: "'a::len word"
+  apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
+  apply (rule order_trans [OF _ bintr_bin_set_ge])
+  apply simp
+  done
+
+lemma set_bit_beyond:
+  "size x \<le> n \<Longrightarrow> set_bit x n b = x" for x :: "'a :: len word"
+  by (auto intro: word_eqI simp add: test_bit_set_gen word_size)
+
+end
diff -r 720b72513ae5 -r 379d0c207c29 src/HOL/Word/More_Word.thy
--- a/src/HOL/Word/More_Word.thy	Sun Jul 05 11:06:09 2020 +0200
+++ b/src/HOL/Word/More_Word.thy	Mon Jul 06 10:47:30 2020 +0000
@@ -9,6 +9,8 @@
   Ancient_Numeral
   Misc_Auxiliary
   Misc_Arithmetic
+  Misc_set_bit
+  Misc_lsb
 begin
 
 end
diff -r 720b72513ae5 -r 379d0c207c29 src/HOL/Word/Traditional_Syntax.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Traditional_Syntax.thy	Mon Jul 06 10:47:30 2020 +0000
@@ -0,0 +1,18 @@
+(*  Author:     Jeremy Dawson, NICTA
+*)
+
+section \<open>Operation variants with traditional syntax\<close>
+
+theory Traditional_Syntax
+  imports Main
+begin
+
+class semiring_bit_syntax = semiring_bit_shifts +
+  fixes test_bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close>  (infixl "!!" 100)
+    and shiftl :: \<open>'a \<Rightarrow> nat \<Rightarrow> 'a\<close>  (infixl "<<" 55)
+    and shiftr :: \<open>'a \<Rightarrow> nat \<Rightarrow> 'a\<close>  (infixl ">>" 55)
+  assumes test_bit_eq_bit: \<open>test_bit = bit\<close>
+    and shiftl_eq_push_bit: \<open>a << n = push_bit n a\<close>
+    and shiftr_eq_drop_bit: \<open>a >> n = drop_bit n a\<close>
+
+end
diff -r 720b72513ae5 -r 379d0c207c29 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sun Jul 05 11:06:09 2020 +0200
+++ b/src/HOL/Word/Word.thy	Mon Jul 06 10:47:30 2020 +0000
@@ -919,25 +919,15 @@
 
 end
 
-instantiation word :: (len) bit_operations
+instantiation word :: (len) semiring_bit_syntax
 begin
 
 definition word_test_bit_def: "test_bit a = bin_nth (uint a)"
 
-definition word_set_bit_def: "set_bit a n x = word_of_int (bin_sc n x (uint a))"
-
-definition word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a)"
-
-definition "msb a \<longleftrightarrow> bin_sign (sbintrunc (LENGTH('a) - 1) (uint a)) = - 1"
-
 definition shiftl_def: "w << n = (shiftl1 ^^ n) w"
 
 definition shiftr_def: "w >> n = (shiftr1 ^^ n) w"
 
-instance ..
-
-end
-
 lemma test_bit_word_eq:
   \<open>test_bit w = bit w\<close> for w :: \<open>'a::len word\<close>
   apply (simp add: word_test_bit_def fun_eq_iff)
@@ -945,36 +935,19 @@
   apply (simp add: bit_take_bit_iff)
   done
 
-lemma set_bit_unfold:
-  \<open>set_bit w n b = (if b then Bit_Operations.set_bit n w else unset_bit n w)\<close>
-  for w :: \<open>'a::len word\<close>
-  apply (auto simp add: word_set_bit_def bin_clr_conv_NAND bin_set_conv_OR unset_bit_def set_bit_def shiftl_int_def push_bit_of_1; transfer)
-   apply simp_all
-  done
-
-lemma bit_set_bit_word_iff:
-  \<open>bit (set_bit w m b) n \<longleftrightarrow> (if m = n then n < LENGTH('a) \<and> b else bit w n)\<close>
-  for w :: \<open>'a::len word\<close>
-  by (auto simp add: set_bit_unfold bit_unset_bit_iff bit_set_bit_iff exp_eq_zero_iff not_le bit_imp_le_length)
-
-lemma lsb_word_eq:
-  \<open>lsb = (odd :: 'a word \<Rightarrow> bool)\<close> for w :: \<open>'a::len word\<close>
-  apply (simp add: word_lsb_def fun_eq_iff)
-  apply transfer
-  apply simp
-  done
-
-lemma msb_word_eq:
-  \<open>msb w \<longleftrightarrow> bit w (LENGTH('a) - 1)\<close> for w :: \<open>'a::len word\<close>
-  apply (simp add: msb_word_def bin_sign_lem)
-  apply transfer
-  apply (simp add: bit_take_bit_iff)
-  done
-
 lemma shiftl_word_eq:
   \<open>w << n = push_bit n w\<close> for w :: \<open>'a::len word\<close>
   by (induction n) (simp_all add: shiftl_def shiftl1_eq_mult_2 push_bit_double)
 
+lemma shiftr_word_eq:
+  \<open>w >> n = drop_bit n w\<close> for w :: \<open>'a::len word\<close>
+  by (induction n) (simp_all add: shiftr_def shiftr1_eq_div_2 drop_bit_Suc drop_bit_half)
+
+instance by standard
+  (simp_all add: fun_eq_iff test_bit_word_eq shiftl_word_eq shiftr_word_eq)
+
+end
+
 lemma bit_shiftl_word_iff:
   \<open>bit (w << m) n \<longleftrightarrow> m \<le> n \<and> n < LENGTH('a) \<and> bit w (n - m)\<close>
   for w :: \<open>'a::len word\<close>
@@ -984,10 +957,6 @@
   \<open>push_bit n w = w << n\<close> for w :: \<open>'a::len word\<close>
   by (simp add: shiftl_word_eq)
 
-lemma shiftr_word_eq:
-  \<open>w >> n = drop_bit n w\<close> for w :: \<open>'a::len word\<close>
-  by (induction n) (simp_all add: shiftr_def shiftr1_eq_div_2 drop_bit_Suc drop_bit_half)
-
 lemma bit_shiftr_word_iff:
   \<open>bit (w >> m) n \<longleftrightarrow> bit w (m + n)\<close>
   for w :: \<open>'a::len word\<close>
@@ -1005,10 +974,6 @@
   \<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close>
   by (fact push_bit_of_1)
 
-lemma word_msb_def:
-  "msb a \<longleftrightarrow> bin_sign (sint a) = - 1"
-  by (simp add: msb_word_def sint_uint)
-
 lemma [code]:
   shows word_not_def: "NOT (a::'a::len word) = word_of_int (NOT (uint a))"
     and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)"
@@ -1017,30 +982,20 @@
   by (transfer, simp add: take_bit_not_take_bit)+
 
 definition setBit :: "'a::len word \<Rightarrow> nat \<Rightarrow> 'a word"
-  where "setBit w n = set_bit w n True"
-
-lemma setBit_eq_set_bit:
-  \<open>setBit w n = Bit_Operations.set_bit n w\<close>
-  for w :: \<open>'a::len word\<close>
-  by (simp add: setBit_def set_bit_unfold)
+  where \<open>setBit w n = Bit_Operations.set_bit n w\<close>
 
 lemma bit_setBit_iff:
   \<open>bit (setBit w m) n \<longleftrightarrow> (m = n \<and> n < LENGTH('a) \<or> bit w n)\<close>
   for w :: \<open>'a::len word\<close>
-  by (simp add: setBit_eq_set_bit bit_set_bit_iff exp_eq_zero_iff not_le ac_simps)
+  by (simp add: setBit_def bit_set_bit_iff exp_eq_zero_iff not_le ac_simps)
 
 definition clearBit :: "'a::len word \<Rightarrow> nat \<Rightarrow> 'a word"
-  where "clearBit w n = set_bit w n False"
-
-lemma clearBit_eq_unset_bit:
-  \<open>clearBit w n = unset_bit n w\<close>
-  for w :: \<open>'a::len word\<close>
-  by (simp add: clearBit_def set_bit_unfold)
+  where \<open>clearBit w n = unset_bit n w\<close>
 
 lemma bit_clearBit_iff:
   \<open>bit (clearBit w m) n \<longleftrightarrow> m \<noteq> n \<and> bit w n\<close>
   for w :: \<open>'a::len word\<close>
-  by (simp add: clearBit_eq_unset_bit bit_unset_bit_iff ac_simps)
+  by (simp add: clearBit_def bit_unset_bit_iff ac_simps)
 
 definition even_word :: \<open>'a::len word \<Rightarrow> bool\<close>
   where [code_abbrev]: \<open>even_word = even\<close>
@@ -1777,6 +1732,30 @@
 
 lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def
 
+lemma bit_last_iff:
+  \<open>bit w (LENGTH('a) - Suc 0) \<longleftrightarrow> sint w < 0\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+  for w :: \<open>'a::len word\<close>
+proof -
+  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)
+  finally show ?thesis .
+qed
+
+lemma drop_bit_eq_zero_iff_not_bit_last:
+  \<open>drop_bit (LENGTH('a) - Suc 0) w = 0 \<longleftrightarrow> \<not> bit w (LENGTH('a) - Suc 0)\<close>
+  for w :: "'a::len word"
+    apply (cases \<open>LENGTH('a)\<close>)
+    apply simp_all
+    apply (simp add: bit_iff_odd_drop_bit)
+    apply transfer
+    apply (simp add: take_bit_drop_bit)
+    apply (auto simp add: drop_bit_eq_div take_bit_eq_mod min_def)
+    apply (auto elim!: evenE)
+    apply (metis div_exp_eq mod_div_trivial mult.commute nonzero_mult_div_cancel_left power_Suc0_right power_add zero_neq_numeral)
+    done
+
 
 subsection \<open>Word Arithmetic\<close>
 
@@ -2919,6 +2898,9 @@
   for x :: "'a::len word"
   by transfer (auto simp add: bin_nth_ops)
 
+lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]]
+lemmas msb1 = msb0 [where i = 0]
+
 lemma test_bit_numeral [simp]:
   "(numeral w :: 'a::len word) !! n \<longleftrightarrow>
     n < LENGTH('a) \<and> bin_nth (numeral w) n"
@@ -3061,63 +3043,6 @@
   unfolding to_bl_def word_log_defs bl_and_bin
   by (simp add: word_ubin.eq_norm)
 
-lemma word_lsb_alt: "lsb w = test_bit w 0"
-  for w :: "'a::len word"
-  by (auto simp: word_test_bit_def word_lsb_def)
-
-lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) \<and> \<not> lsb (0::'b::len word)"
-  unfolding word_lsb_def uint_eq_0 uint_1 by simp
-
-lemma word_lsb_last: "lsb w = last (to_bl w)"
-  for w :: "'a::len word"
-  apply (unfold word_lsb_def uint_bl bin_to_bl_def)
-  apply (rule_tac bin="uint w" in bin_exhaust)
-  apply (cases "size w")
-   apply auto
-   apply (auto simp add: bin_to_bl_aux_alt)
-  done
-
-lemma word_lsb_int: "lsb w \<longleftrightarrow> uint w mod 2 = 1"
-  by (auto simp: word_lsb_def bin_last_def)
-
-lemma word_msb_sint: "msb w \<longleftrightarrow> sint w < 0"
-  by (simp only: word_msb_def sign_Min_lt_0)
-
-lemma msb_word_of_int: "msb (word_of_int x::'a::len word) = bin_nth x (LENGTH('a) - 1)"
-  by (simp add: word_msb_def word_sbin.eq_norm bin_sign_lem)
-
-lemma word_msb_numeral [simp]:
-  "msb (numeral w::'a::len word) = bin_nth (numeral w) (LENGTH('a) - 1)"
-  unfolding word_numeral_alt by (rule msb_word_of_int)
-
-lemma word_msb_neg_numeral [simp]:
-  "msb (- numeral w::'a::len word) = bin_nth (- numeral w) (LENGTH('a) - 1)"
-  unfolding word_neg_numeral_alt by (rule msb_word_of_int)
-
-lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)"
-  by (simp add: word_msb_def)
-
-lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> LENGTH('a) = 1"
-  unfolding word_1_wi msb_word_of_int eq_iff [where 'a=nat]
-  by (simp add: Suc_le_eq)
-
-lemma word_msb_nth: "msb w = bin_nth (uint w) (LENGTH('a) - 1)"
-  for w :: "'a::len word"
-  by (simp add: word_msb_def sint_uint bin_sign_lem)
-
-lemma word_msb_alt: "msb w = hd (to_bl w)"
-  for w :: "'a::len word"
-  apply (unfold word_msb_nth uint_bl)
-  apply (subst hd_conv_nth)
-   apply (rule length_greater_0_conv [THEN iffD1])
-   apply simp
-  apply (simp add : nth_bin_to_bl word_size)
-  done
-
-lemma word_set_nth [simp]: "set_bit w n (test_bit w n) = w"
-  for w :: "'a::len word"
-  by (auto simp: word_test_bit_def word_set_bit_def)
-
 lemma bin_nth_uint': "bin_nth (uint w) n \<longleftrightarrow> rev (bin_to_bl (size w) (uint w)) ! n \<and> n < size w"
   apply (unfold word_size)
   apply (safe elim!: bin_nth_uint_imp)
@@ -3163,19 +3088,6 @@
   if \<open>n < LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
   using that by (simp add: to_bl_unfold rev_nth)
 
-lemma test_bit_set: "(set_bit w n x) !! n \<longleftrightarrow> n < size w \<and> x"
-  for w :: "'a::len word"
-  by (auto simp: word_size word_test_bit_def word_set_bit_def word_ubin.eq_norm nth_bintr)
-
-lemma test_bit_set_gen:
-  "test_bit (set_bit w n x) m = (if m = n then n < size w \<and> x else test_bit w m)"
-  for w :: "'a::len word"
-  apply (unfold word_size word_test_bit_def word_set_bit_def)
-  apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen)
-  apply (auto elim!: test_bit_size [unfolded word_size]
-      simp add: word_test_bit_def [symmetric])
-  done
-
 lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
   by (auto simp: of_bl_def bl_to_bin_rep_F)
 
@@ -3202,26 +3114,8 @@
   for w :: \<open>'a::len word\<close>
   by (simp add: slice_def word_size bit_slice1_iff)
 
-lemma msb_nth: "msb w = w !! (LENGTH('a) - 1)"
-  for w :: "'a::len word"
-  by (simp add: word_msb_nth word_test_bit_def)
-
-lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]]
-lemmas msb1 = msb0 [where i = 0]
-lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]]
 
 lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]]
-lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
-
-lemma word_set_set_same [simp]: "set_bit (set_bit w n x) n y = set_bit w n y"
-  for w :: "'a::len word"
-  by (rule word_eqI) (simp add : test_bit_set_gen word_size)
-
-lemma word_set_set_diff:
-  fixes w :: "'a::len word"
-  assumes "m \<noteq> n"
-  shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x"
-  by (rule word_eqI) (auto simp: test_bit_set_gen word_size assms)
 
 lemma nth_sint:
   fixes w :: "'a::len word"
@@ -3230,40 +3124,18 @@
   unfolding sint_uint l_def
   by (auto simp: nth_sbintr word_test_bit_def [symmetric])
 
-lemma word_lsb_numeral [simp]:
-  "lsb (numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (numeral bin)"
-  unfolding word_lsb_alt test_bit_numeral by simp
-
-lemma word_lsb_neg_numeral [simp]:
-  "lsb (- numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (- numeral bin)"
-  by (simp add: word_lsb_alt)
-
-lemma set_bit_word_of_int: "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)"
-  unfolding word_set_bit_def
-  by (rule word_eqI)(simp add: word_size bin_nth_sc_gen word_ubin.eq_norm nth_bintr)
-
-lemma word_set_numeral [simp]:
-  "set_bit (numeral bin::'a::len word) n b =
-    word_of_int (bin_sc n b (numeral bin))"
-  unfolding word_numeral_alt by (rule set_bit_word_of_int)
-
-lemma word_set_neg_numeral [simp]:
-  "set_bit (- numeral bin::'a::len word) n b =
-    word_of_int (bin_sc n b (- numeral bin))"
-  unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)
-
-lemma word_set_bit_0 [simp]: "set_bit 0 n b = word_of_int (bin_sc n b 0)"
-  unfolding word_0_wi by (rule set_bit_word_of_int)
-
-lemma word_set_bit_1 [simp]: "set_bit 1 n b = word_of_int (bin_sc n b 1)"
-  unfolding word_1_wi by (rule set_bit_word_of_int)
-
 lemma setBit_no [simp]: "setBit (numeral bin) n = word_of_int (bin_sc n True (numeral bin))"
-  by (simp add: setBit_def)
-
+  apply (simp add: setBit_def bin_sc_eq set_bit_def)
+  apply transfer
+  apply simp
+  done
+ 
 lemma clearBit_no [simp]:
   "clearBit (numeral bin) n = word_of_int (bin_sc n False (numeral bin))"
-  by (simp add: clearBit_def)
+  apply (simp add: clearBit_def bin_sc_eq unset_bit_def)
+  apply transfer
+  apply simp
+  done
 
 lemma to_bl_n1 [simp]: "to_bl (-1::'a::len word) = replicate (LENGTH('a)) True"
   apply (rule word_bl.Abs_inverse')
@@ -3273,24 +3145,6 @@
   apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)
   done
 
-lemma word_msb_n1 [simp]: "msb (-1::'a::len word)"
-  unfolding word_msb_alt to_bl_n1 by simp
-
-lemma word_set_nth_iff: "set_bit w n b = w \<longleftrightarrow> w !! n = b \<or> n \<ge> size w"
-  for w :: "'a::len word"
-  apply (rule iffI)
-   apply (rule disjCI)
-   apply (drule word_eqD)
-   apply (erule sym [THEN trans])
-   apply (simp add: test_bit_set)
-  apply (erule disjE)
-   apply clarsimp
-  apply (rule word_eqI)
-  apply (clarsimp simp add : test_bit_set_gen)
-  apply (drule test_bit_size)
-  apply force
-  done
-
 lemma test_bit_2p: "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < LENGTH('a)"
   by (auto simp: word_test_bit_def word_ubin.eq_norm nth_bintr nth_2p_bin)
 
@@ -3328,25 +3182,6 @@
   apply (auto simp add: word_ao_nth nth_w2p word_size)
   done
 
-lemma word_clr_le: "w \<ge> set_bit w n False"
-  for w :: "'a::len word"
-  apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
-  apply (rule order_trans)
-   apply (rule bintr_bin_clr_le)
-  apply simp
-  done
-
-lemma word_set_ge: "w \<le> set_bit w n True"
-  for w :: "'a::len word"
-  apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
-  apply (rule order_trans [OF _ bintr_bin_set_ge])
-  apply simp
-  done
-
-lemma set_bit_beyond:
-  "size x \<le> n \<Longrightarrow> set_bit x n b = x" for x :: "'a :: len word"
-  by (auto intro: word_eqI simp add: test_bit_set_gen word_size)
-
 lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 (\<or>) (rev (to_bl x)) (rev (to_bl y))"
   by (simp add: zip_rev bl_word_or rev_map)
 
@@ -3815,14 +3650,6 @@
   for x :: "'a::len word"
   using shiftr_bl_of [where 'a='a, of "to_bl x"] by simp
 
-lemma msb_shift: "msb w \<longleftrightarrow> w >> (LENGTH('a) - 1) \<noteq> 0"
-  for w :: "'a::len word"
-  apply (unfold shiftr_bl word_msb_alt)
-  apply (simp add: word_size Suc_le_eq take_Suc)
-  apply (cases "hd (to_bl w)")
-   apply (auto simp: word_1_bl of_bl_rep_False [where n=1 and bs="[]", simplified])
-  done
-
 lemma zip_replicate: "n \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>y. (x, y)) ys"
   apply (induct ys arbitrary: n)
    apply simp_all
@@ -4248,33 +4075,40 @@
       criterion for overflow of addition of signed integers\<close>
 
 lemma sofl_test:
-  "(sint x + sint y = sint (x + y)) =
-     ((((x + y) XOR x) AND ((x + y) XOR y)) >> (size x - 1) = 0)"
-  for x y :: "'a::len word"
-  apply (unfold word_size)
-  apply (cases "LENGTH('a)", simp)
-  apply (subst msb_shift [THEN sym_notr])
-  apply (simp add: word_ops_msb)
-  apply (simp add: word_msb_sint)
-  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])
+  \<open>sint x + sint y = sint (x + y) \<longleftrightarrow>
+    (x + y XOR x) AND (x + y XOR y) >> (size x - 1) = 0\<close>
+  for x y :: \<open>'a::len word\<close>
+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 = 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)
-       defer
-       defer
-       apply (simp (no_asm), arith)
-      apply (simp (no_asm), arith)
-     apply (rule notI [THEN notnotD],
-      drule leI not_le_imp_less,
-      drule sbintrunc_inc sbintrunc_dec,
-      simp)+
-  done
+       apply (simp_all add: n not_less)
+       apply (rule notI [THEN notnotD],
+         drule leI not_le_imp_less,
+         drule sbintrunc_inc sbintrunc_dec,
+         simp)+
+    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: bit_last_iff)
+    done
+qed
 
 lemma shiftr_zero_size: "size x \<le> n \<Longrightarrow> x >> n = 0"
   for x :: "'a :: len word"
diff -r 720b72513ae5 -r 379d0c207c29 src/HOL/Word/Word_Examples.thy
--- a/src/HOL/Word/Word_Examples.thy	Sun Jul 05 11:06:09 2020 +0200
+++ b/src/HOL/Word/Word_Examples.thy	Mon Jul 06 10:47:30 2020 +0000
@@ -7,7 +7,7 @@
 section "Examples of word operations"
 
 theory Word_Examples
-  imports Word
+  imports Word Misc_lsb Misc_set_bit
 begin
 
 type_synonym word32 = "32 word"