more simp rules for concrete numerical values
authorhaftmann
Sun, 12 Jul 2020 18:10:06 +0000
changeset 72256 5689f0db4508
parent 72255 b4ed07cbe954
child 72257 759532ef0885
more simp rules for concrete numerical values
src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sun Jul 12 18:10:06 2020 +0000
+++ b/src/HOL/Parity.thy	Sun Jul 12 18:10:06 2020 +0000
@@ -1499,6 +1499,10 @@
   "take_bit n 1 = 0 \<longleftrightarrow> n = 0"
   by (simp add: take_bit_eq_mod)
 
+lemma take_bit_Suc_1 [simp]:
+  \<open>take_bit (Suc n) 1 = 1\<close>
+  by (simp add: take_bit_Suc)
+
 lemma take_bit_Suc_bit0 [simp]:
   \<open>take_bit (Suc n) (numeral (Num.Bit0 k)) = take_bit n (numeral k) * 2\<close>
   by (simp add: take_bit_Suc numeral_Bit0_div_2)
@@ -1507,6 +1511,10 @@
   \<open>take_bit (Suc n) (numeral (Num.Bit1 k)) = take_bit n (numeral k) * 2 + 1\<close>
   by (simp add: take_bit_Suc numeral_Bit1_div_2 mod_2_eq_odd)
 
+lemma take_bit_numeral_1 [simp]:
+  \<open>take_bit (numeral l) 1 = 1\<close>
+  by (simp add: take_bit_rec [of \<open>numeral l\<close> 1])
+
 lemma take_bit_numeral_bit0 [simp]:
   \<open>take_bit (numeral l) (numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (numeral k) * 2\<close>
   by (simp add: take_bit_rec numeral_Bit0_div_2)