# HG changeset patch
# User haftmann
# Date 1633889817 0
# Node ID 9c04a82c312850bd2c9e23e9c061be090cbe1998
# Parent  807b094a9b78d264e62e76acb34f8f64690bb5ec
more complete simp rules

diff -r 807b094a9b78 -r 9c04a82c3128 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Sun Oct 10 14:45:53 2021 +0000
+++ b/src/HOL/Bit_Operations.thy	Sun Oct 10 18:16:57 2021 +0000
@@ -310,10 +310,6 @@
   \<open>bit (2 ^ m - 1) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n < m\<close>
   by (simp add: bit_iff_odd even_mask_div_iff not_le possible_bit_def)
 
-lemma bit_Numeral1_iff [simp]:
-  \<open>bit (numeral Num.One) n \<longleftrightarrow> n = 0\<close>
-  by (simp add: bit_rec)
-
 lemma exp_add_not_zero_imp:
   \<open>2 ^ m \<noteq> 0\<close> and \<open>2 ^ n \<noteq> 0\<close> if \<open>2 ^ (m + n) \<noteq> 0\<close>
 proof -
@@ -474,6 +470,14 @@
   "possible_bit TYPE(nat) n"
   by (simp add: possible_bit_def)
 
+lemma not_bit_Suc_0_Suc [simp]:
+  \<open>\<not> bit (Suc 0) (Suc n)\<close>
+  by (simp add: bit_Suc)
+
+lemma not_bit_Suc_0_numeral [simp]:
+  \<open>\<not> bit (Suc 0) (numeral n)\<close>
+  by (simp add: numeral_eq_Suc)
+
 lemma int_bit_induct [case_names zero minus even odd]:
   "P k" if zero_int: "P 0"
     and minus_int: "P (- 1)"
@@ -1234,6 +1238,14 @@
   \<open>take_bit n (flip_bit m a) = (if n \<le> m then take_bit n a else flip_bit m (take_bit n a))\<close>
   by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_flip_bit_iff)
 
+lemma not_bit_1_Suc [simp]:
+  \<open>\<not> bit 1 (Suc n)\<close>
+  by (simp add: bit_Suc)
+
+lemma push_bit_Suc_numeral [simp]:
+  \<open>push_bit (Suc n) (numeral k) = push_bit n (numeral (Num.Bit0 k))\<close>
+  by (simp add: numeral_eq_Suc mult_2_right) (simp add: numeral_Bit0)
+
 end
 
 class ring_bit_operations = semiring_bit_operations + ring_parity +
@@ -1389,6 +1401,17 @@
 
 lemmas unset_bit_def = unset_bit_eq_and_not
 
+lemma push_bit_Suc_minus_numeral [simp]:
+  \<open>push_bit (Suc n) (- numeral k) = push_bit n (- numeral (Num.Bit0 k))\<close>
+  apply (simp only: numeral_Bit0)
+  apply simp
+  apply (simp only: numeral_mult mult_2_right numeral_add)
+  done
+
+lemma push_bit_minus_numeral [simp]:
+  \<open>push_bit (numeral l) (- numeral k) = push_bit (pred_numeral l) (- numeral (Num.Bit0 k))\<close>
+  by (simp only: numeral_eq_Suc push_bit_Suc_minus_numeral)
+
 end
 
 
@@ -2223,6 +2246,22 @@
   "take_bit n 1 = 0 \<longleftrightarrow> n = 0"
   by (simp add: take_bit_eq_mod)
 
+lemma drop_bit_Suc_bit0 [simp]:
+  \<open>drop_bit (Suc n) (numeral (Num.Bit0 k)) = drop_bit n (numeral k)\<close>
+  by (simp add: drop_bit_Suc numeral_Bit0_div_2)
+
+lemma drop_bit_Suc_bit1 [simp]:
+  \<open>drop_bit (Suc n) (numeral (Num.Bit1 k)) = drop_bit n (numeral k)\<close>
+  by (simp add: drop_bit_Suc numeral_Bit1_div_2)
+
+lemma drop_bit_numeral_bit0 [simp]:
+  \<open>drop_bit (numeral l) (numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (numeral k)\<close>
+  by (simp add: drop_bit_rec numeral_Bit0_div_2)
+
+lemma drop_bit_numeral_bit1 [simp]:
+  \<open>drop_bit (numeral l) (numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (numeral k)\<close>
+  by (simp add: drop_bit_rec numeral_Bit1_div_2)
+
 lemma take_bit_Suc_1 [simp]:
   \<open>take_bit (Suc n) 1 = 1\<close>
   by (simp add: take_bit_Suc)
@@ -2247,26 +2286,6 @@
   \<open>take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1\<close>
   by (simp add: take_bit_rec numeral_Bit1_div_2 mod_2_eq_odd)
 
-lemma drop_bit_Suc_bit0 [simp]:
-  \<open>drop_bit (Suc n) (numeral (Num.Bit0 k)) = drop_bit n (numeral k)\<close>
-  by (simp add: drop_bit_Suc numeral_Bit0_div_2)
-
-lemma drop_bit_Suc_bit1 [simp]:
-  \<open>drop_bit (Suc n) (numeral (Num.Bit1 k)) = drop_bit n (numeral k)\<close>
-  by (simp add: drop_bit_Suc numeral_Bit1_div_2)
-
-lemma drop_bit_numeral_bit0 [simp]:
-  \<open>drop_bit (numeral l) (numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (numeral k)\<close>
-  by (simp add: drop_bit_rec numeral_Bit0_div_2)
-
-lemma drop_bit_numeral_bit1 [simp]:
-  \<open>drop_bit (numeral l) (numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (numeral k)\<close>
-  by (simp add: drop_bit_rec numeral_Bit1_div_2)
-
-lemma drop_bit_of_nat:
-  "drop_bit n (of_nat m) = of_nat (drop_bit n m)"
-  by (simp add: drop_bit_eq_div Bit_Operations.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
-
 lemma bit_of_nat_iff_bit [bit_simps]:
   \<open>bit (of_nat m) n \<longleftrightarrow> bit m n\<close>
 proof -
@@ -2278,6 +2297,10 @@
     by (simp add: bit_iff_odd semiring_bits_class.bit_iff_odd)
 qed
 
+lemma drop_bit_of_nat:
+  "drop_bit n (of_nat m) = of_nat (drop_bit n m)"
+  by (simp add: drop_bit_eq_div Bit_Operations.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
+
 lemma of_nat_drop_bit:
   \<open>of_nat (drop_bit m n) = drop_bit m (of_nat n)\<close>
   by (simp add: drop_bit_eq_div Bit_Operations.drop_bit_eq_div of_nat_div)
@@ -2307,6 +2330,38 @@
 
 instance int :: unique_euclidean_semiring_with_bit_operations ..
 
+lemma drop_bit_Suc_minus_bit0 [simp]:
+  \<open>drop_bit (Suc n) (- numeral (Num.Bit0 k)) = drop_bit n (- numeral k :: int)\<close>
+  by (simp add: drop_bit_Suc numeral_Bit0_div_2)
+
+lemma drop_bit_Suc_minus_bit1 [simp]:
+  \<open>drop_bit (Suc n) (- numeral (Num.Bit1 k)) = drop_bit n (- numeral (Num.inc k) :: int)\<close>
+  by (simp add: drop_bit_Suc numeral_Bit1_div_2 add_One)
+
+lemma drop_bit_numeral_minus_bit0 [simp]:
+  \<open>drop_bit (numeral l) (- numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (- numeral k :: int)\<close>
+  by (simp add: numeral_eq_Suc numeral_Bit0_div_2)
+
+lemma drop_bit_numeral_minus_bit1 [simp]:
+  \<open>drop_bit (numeral l) (- numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (- numeral (Num.inc k) :: int)\<close>
+  by (simp add: numeral_eq_Suc numeral_Bit1_div_2)
+
+lemma take_bit_Suc_minus_bit0 [simp]:
+  \<open>take_bit (Suc n) (- numeral (Num.Bit0 k)) = take_bit n (- numeral k) * (2 :: int)\<close>
+  by (simp add: take_bit_Suc numeral_Bit0_div_2)
+
+lemma take_bit_Suc_minus_bit1 [simp]:
+  \<open>take_bit (Suc n) (- numeral (Num.Bit1 k)) = take_bit n (- numeral (Num.inc k)) * 2 + (1 :: int)\<close>
+  by (simp add: take_bit_Suc numeral_Bit1_div_2 add_One)
+
+lemma take_bit_numeral_minus_bit0 [simp]:
+  \<open>take_bit (numeral l) (- numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (- numeral k) * (2 :: int)\<close>
+  by (simp add: numeral_eq_Suc numeral_Bit0_div_2)
+
+lemma take_bit_numeral_minus_bit1 [simp]:
+  \<open>take_bit (numeral l) (- numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (- numeral (Num.inc k)) * 2 + (1 :: int)\<close>
+  by (simp add: numeral_eq_Suc numeral_Bit1_div_2)
+
 
 subsection \<open>Symbolic computations on numeral expressions\<close>
 
@@ -3146,6 +3201,10 @@
   \<open>signed_take_bit (Suc n) 1 = 1\<close>
   by (simp add: signed_take_bit_Suc)
 
+lemma signed_take_bit_numeral_of_1 [simp]:
+  \<open>signed_take_bit (numeral k) 1 = 1\<close>
+  by (simp add: bit_1_iff signed_take_bit_eq_if_positive)
+
 lemma signed_take_bit_rec:
   \<open>signed_take_bit n a = (if n = 0 then - (a mod 2) else a mod 2 + 2 * signed_take_bit (n - 1) (a div 2))\<close>
   by (cases n) (simp_all add: signed_take_bit_Suc)