src/HOL/Library/Word.thy

 lemma bit_neg_numeral_word_iff [simp]:
   \<open>bit (- numeral w :: 'a::len word) n
     \<longleftrightarrow> n < LENGTH('a) \<and> bit (- numeral w :: int) n\<close>
   by transfer simp
 
-instantiation word :: (len) semiring_bit_shifts
+instantiation word :: (len) ring_bit_operations
 begin
+
+lift_definition not_word :: \<open>'a word \<Rightarrow> 'a word\<close>
+  is not
+  by (simp add: take_bit_not_iff)
+
+lift_definition and_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+  is \<open>and\<close>
+  by simp
+
+lift_definition or_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+  is or
+  by simp
+
+lift_definition xor_word ::  \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+  is xor
+  by simp
+
+lift_definition mask_word :: \<open>nat \<Rightarrow> 'a word\<close>
+  is mask
+  .
+
+lift_definition set_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+  is set_bit
+  by (simp add: set_bit_def)
+
+lift_definition unset_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+  is unset_bit
+  by (simp add: unset_bit_def)
+
+lift_definition flip_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
+  is flip_bit
+  by (simp add: flip_bit_def)
 
 lift_definition push_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
   is push_bit
 proof -
   show \<open>take_bit LENGTH('a) (push_bit n k) = take_bit LENGTH('a) (push_bit n l)\<close>

 
 lift_definition take_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
   is \<open>\<lambda>n. take_bit (min LENGTH('a) n)\<close>
   by (simp add: ac_simps) (simp only: flip: take_bit_take_bit)
 
-instance proof
-  show \<open>push_bit n a = a * 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close>
-    by transfer (simp add: push_bit_eq_mult)
-  show \<open>drop_bit n a = a div 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close>
-    by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit)
-  show \<open>take_bit n a = a mod 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close>
-    by transfer (auto simp flip: take_bit_eq_mod)
-qed
+instance apply (standard; transfer)
+  apply (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1
+    bit_simps set_bit_def flip_bit_def take_bit_drop_bit
+    simp flip: drop_bit_eq_div take_bit_eq_mod)
+   apply (simp_all add: drop_bit_take_bit flip: push_bit_eq_mult)
+  done
 
 end
 
 lemma [code]:
   \<open>push_bit n w = w * 2 ^ n\<close> for w :: \<open>'a::len word\<close>

 
 lemma [code]:
   \<open>Word.the_int (take_bit n w) = (if n < LENGTH('a::len) then take_bit n (Word.the_int w) else Word.the_int w)\<close>
   for w :: \<open>'a::len word\<close>
   by transfer (simp add: not_le not_less ac_simps min_absorb2)
-
-
-instantiation word :: (len) ring_bit_operations
-begin
-
-lift_definition not_word :: \<open>'a word \<Rightarrow> 'a word\<close>
-  is not
-  by (simp add: take_bit_not_iff)
-
-lift_definition and_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
-  is \<open>and\<close>
-  by simp
-
-lift_definition or_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
-  is or
-  by simp
-
-lift_definition xor_word ::  \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
-  is xor
-  by simp
-
-lift_definition mask_word :: \<open>nat \<Rightarrow> 'a word\<close>
-  is mask
-  .
-
-lift_definition set_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
-  is set_bit
-  by (simp add: set_bit_def)
-
-lift_definition unset_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
-  is unset_bit
-  by (simp add: unset_bit_def)
-
-lift_definition flip_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
-  is flip_bit
-  by (simp add: flip_bit_def)
-
-instance by (standard; transfer)
-  (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1
-    bit_simps set_bit_def flip_bit_def)
-
-end
 
 lemma [code_abbrev]:
   \<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close>
   by (fact push_bit_of_1)
 

   for w :: \<open>'b::len word\<close>
   by (transfer fixing: bit) (simp add: bit_of_nat_iff bit_nat_iff bit_take_bit_iff)
 
 end
 
-context semiring_bit_shifts
+context semiring_bit_operations
 begin
 
 lemma unsigned_push_bit_eq:
   \<open>unsigned (push_bit n w) = take_bit LENGTH('b) (push_bit n (unsigned w))\<close>
   for w :: \<open>'b::len word\<close>

   for w :: \<open>'b::len word\<close>
   by (rule bit_eqI) (simp add: bit_unsigned_iff bit_take_bit_iff Bit_Operations.bit_take_bit_iff)
 
 end
 
-context unique_euclidean_semiring_with_bit_shifts
+context unique_euclidean_semiring_with_bit_operations
 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 (simp add: unat_mod_distrib)
   then show ?thesis
     by (simp add: of_nat_mod)
 qed
 
-context semiring_bit_shifts
+context semiring_bit_operations
 begin
 
 lemma unsigned_ucast_eq:
   \<open>unsigned (ucast w :: 'c::len word) = take_bit LENGTH('c) (unsigned w)\<close>
   for w :: \<open>'b::len word\<close>