src/HOL/Library/Word.thy

 section \<open>A type of finite bit strings\<close>
 
 theory Word
 imports
   "HOL-Library.Type_Length"
-  "HOL-Library.Boolean_Algebra"
-  "HOL-Library.Bit_Operations"
 begin
 
 subsection \<open>Preliminaries\<close>
 
 lemma signed_take_bit_decr_length_iff:

   proof (cases \<open>n \<le> m\<close>)
     case True
     with \<open>2 ^ m \<noteq> 0\<close> have \<open>2 ^ (m - n) \<noteq> 0\<close>
       by (metis (full_types) diff_add exp_add_not_zero_imp)
     with True show ?thesis
-      by (simp add: bit_unsigned_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_take_bit_iff not_le exp_eq_zero_iff ac_simps)
+      by (simp add: bit_unsigned_iff bit_push_bit_iff Bit_Operations.bit_push_bit_iff bit_take_bit_iff not_le ac_simps)
   next
     case False
     then show ?thesis
-      by (simp add: not_le bit_unsigned_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_take_bit_iff)
+      by (simp add: not_le bit_unsigned_iff bit_push_bit_iff Bit_Operations.bit_push_bit_iff bit_take_bit_iff)
   qed
 qed
 
 lemma unsigned_take_bit_eq:
   \<open>unsigned (take_bit n w) = take_bit n (unsigned w)\<close>
   for w :: \<open>'b::len word\<close>
-  by (rule bit_eqI) (simp add: bit_unsigned_iff bit_take_bit_iff Parity.bit_take_bit_iff)
+  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
 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)
+  by (rule bit_eqI) (auto simp add: bit_unsigned_iff bit_take_bit_iff bit_drop_bit_eq Bit_Operations.bit_drop_bit_eq dest: bit_imp_le_length)
 
 end
 
 lemma ucast_drop_bit_eq:
   \<open>ucast (drop_bit n w) = drop_bit n (ucast w :: 'b::len word)\<close>

 
 lemma unsigned_not_eq:
   \<open>unsigned (NOT w) = take_bit LENGTH('b) (NOT (unsigned w))\<close>
   for w :: \<open>'b::len word\<close>
   by (rule bit_eqI)
-    (simp add: bit_unsigned_iff bit_take_bit_iff bit_not_iff Bit_Operations.bit_not_iff exp_eq_zero_iff not_le)
+    (simp add: bit_unsigned_iff bit_take_bit_iff bit_not_iff Bit_Operations.bit_not_iff not_le)
 
 end
 
 end
 

       using exp_add_not_zero_imp_left [of q r] exp_add_not_zero_imp_right [of q r]
       by simp_all
     moreover from \<open>2 ^ q \<noteq> 0\<close> have \<open>2 ^ (q - n) \<noteq> 0\<close>
       by (rule exp_not_zero_imp_exp_diff_not_zero)
     ultimately show ?thesis
-      by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff
-      min_def * exp_eq_zero_iff le_diff_conv2)
+      by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Bit_Operations.bit_push_bit_iff
+        min_def * le_diff_conv2)
   next
     case False
     then show ?thesis
       using exp_not_zero_imp_exp_diff_not_zero [of m n]
-      by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff
-      min_def not_le not_less * le_diff_conv2 less_diff_conv2 Parity.exp_eq_0_imp_not_bit exp_eq_0_imp_not_bit
-      exp_eq_zero_iff)
+      by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Bit_Operations.bit_push_bit_iff
+        min_def not_le not_less * le_diff_conv2 less_diff_conv2 Bit_Operations.exp_eq_0_imp_not_bit exp_eq_0_imp_not_bit)
   qed
 qed
 
 lemma signed_take_bit_eq:
   \<open>signed (take_bit n w) = (if n < LENGTH('b) then take_bit n (signed w) else signed w)\<close>

       by simp
     moreover from \<open>2 ^ n \<noteq> 0\<close> \<open>n = r + Suc q\<close>
       have \<open>2 ^ Suc q \<noteq> 0\<close>
       using exp_add_not_zero_imp_right by blast 
     ultimately show ?thesis
-      by (simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def
-        exp_eq_zero_iff)
+      by (simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def)
   next
     case False
     then show ?thesis
-      by (auto simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def
-        exp_eq_zero_iff)
+      by (auto simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def)
   qed
 qed
 
 context
   includes bit_operations_syntax

 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>
-  by (rule bit_eqI) (simp add: bit_unsigned_iff Word.bit_unsigned_iff bit_take_bit_iff exp_eq_zero_iff not_le)
+  by (rule bit_eqI) (simp add: bit_unsigned_iff Word.bit_unsigned_iff bit_take_bit_iff not_le)
 
 end
 
 context ring_bit_operations
 begin

   assume \<open>2 ^ n \<noteq> 0\<close>
   then have \<open>2 ^ (min (LENGTH('c) - Suc 0) n) \<noteq> 0\<close>
     by (simp add: min_def)
       (metis (mono_tags) diff_diff_cancel exp_not_zero_imp_exp_diff_not_zero)
   then show \<open>bit (signed (ucast w :: 'c::len word)) n \<longleftrightarrow> bit (signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)) n\<close>
-    by (simp add: bit_signed_iff bit_unsigned_iff Word.bit_unsigned_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le)
+    by (simp add: bit_signed_iff bit_unsigned_iff Word.bit_unsigned_iff bit_signed_take_bit_iff not_le)
 qed
 
 lemma signed_scast_eq:
   \<open>signed (scast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (signed w)\<close>
   for w :: \<open>'b::len word\<close>

   assume \<open>2 ^ n \<noteq> 0\<close>
   then have \<open>2 ^ (min (LENGTH('c) - Suc 0) n) \<noteq> 0\<close>
     by (simp add: min_def)
       (metis (mono_tags) diff_diff_cancel exp_not_zero_imp_exp_diff_not_zero)
   then show \<open>bit (signed (scast w :: 'c::len word)) n \<longleftrightarrow> bit (signed_take_bit (LENGTH('c) - Suc 0) (signed w)) n\<close>
-    by (simp add: bit_signed_iff bit_unsigned_iff Word.bit_signed_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le)
+    by (simp add: bit_signed_iff bit_unsigned_iff Word.bit_signed_iff bit_signed_take_bit_iff not_le)
 qed
 
 end
 
 lemma uint_nonnegative: "0 \<le> uint w"

 lemma uint_word_rotr_eq:
   \<open>uint (word_rotr n w) = concat_bit (LENGTH('a) - n mod LENGTH('a))
     (drop_bit (n mod LENGTH('a)) (uint w))
     (uint (take_bit (n mod LENGTH('a)) w))\<close>
   for w :: \<open>'a::len word\<close>
-  apply transfer
-  by (simp add: min.absorb2 take_bit_concat_bit_eq)
+  by transfer (simp add: take_bit_concat_bit_eq)
 
 lemma [code]:
   \<open>Word.the_int (word_rotr n w) = concat_bit (LENGTH('a) - n mod LENGTH('a))
     (drop_bit (n mod LENGTH('a)) (Word.the_int w))
     (Word.the_int (take_bit (n mod LENGTH('a)) w))\<close>

   \<open>cast\<close> -- note, no arg for new length, as it's determined by type of result,
   thus in \<open>cast w = w\<close>, the type means cast to length of \<open>w\<close>!
 \<close>
 
 lemma bit_ucast_iff:
-  \<open>bit (ucast a :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a::len) \<and> Parity.bit a n\<close>
+  \<open>bit (ucast a :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a::len) \<and> bit a n\<close>
   by transfer (simp add: bit_take_bit_iff)
 
 lemma ucast_id [simp]: "ucast w = w"
   by transfer simp
 
 lemma scast_id [simp]: "scast w = w"
   by transfer (simp add: take_bit_signed_take_bit)
 
 lemma ucast_mask_eq:
   \<open>ucast (mask n :: 'b word) = mask (min LENGTH('b::len) n)\<close>
-  by (simp add: bit_eq_iff) (auto simp add: bit_mask_iff bit_ucast_iff exp_eq_zero_iff)
+  by (simp add: bit_eq_iff) (auto simp add: bit_mask_iff bit_ucast_iff)
 
 \<comment> \<open>literal u(s)cast\<close>
 lemma ucast_bintr [simp]:
   "ucast (numeral w :: 'a::len word) =
     word_of_int (take_bit (LENGTH('a)) (numeral w))"

 proof (cases \<open>LENGTH('a)\<close>)
   case (Suc n)
   then show ?thesis
     apply transfer
     apply (simp add: take_bit_drop_bit)
-    by (simp add: bit_iff_odd_drop_bit drop_bit_take_bit min.absorb2 odd_iff_mod_2_eq_one)
+    by (simp add: bit_iff_odd_drop_bit drop_bit_take_bit odd_iff_mod_2_eq_one)
 qed auto
 
 
 subsection \<open>Word Arithmetic\<close>
 

 
 subsubsection \<open>Mask\<close>
 
 lemma minus_1_eq_mask:
   \<open>- 1 = (mask LENGTH('a) :: 'a::len word)\<close>
-  by (rule bit_eqI) (simp add: bit_exp_iff bit_mask_iff exp_eq_zero_iff)
+  by (rule bit_eqI) (simp add: bit_exp_iff bit_mask_iff)
 
 lemma mask_eq_decr_exp:
   \<open>mask n = 2 ^ n - (1 :: 'a::len word)\<close>
   by (fact mask_eq_exp_minus_1)
 

 context
 begin
 
 qualified lemma bit_mask_iff [bit_simps]:
   \<open>bit (mask m :: 'a::len word) n \<longleftrightarrow> n < min LENGTH('a) m\<close>
-  by (simp add: bit_mask_iff exp_eq_zero_iff not_le)
+  by (simp add: bit_mask_iff not_le)
 
 end
 
 lemma mask_bin: "mask n = word_of_int (take_bit n (- 1))"
   by transfer (simp add: take_bit_minus_one_eq_mask) 

 
 lemma word_rec_Pred: "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
   by (metis add.commute diff_add_cancel word_rec_Suc)
 
 lemma word_rec_in: "f (word_rec z (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. f) n"
-  by (induct n) (simp_all add: word_rec_Suc)
+  by (induct n) simp_all
 
 lemma word_rec_in2: "f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> (+) 1) n"
-  by (induct n) (simp_all add: word_rec_Suc)
+  by (induct n) simp_all
 
 lemma word_rec_twice:
   "m \<le> n \<Longrightarrow> word_rec z f n = word_rec (word_rec z f (n - m)) (f \<circ> (+) (n - m)) m"
 proof (induction n arbitrary: z f)
   case zero