# HG changeset patch
# User haftmann
# Date 1594577406 0
# Node ID 5689f0db45082c35b5767d6a60fab4f7f75f8496
# Parent  b4ed07cbe95475d37f9e130b6ccbc2de388d2097
more simp rules for concrete numerical values

diff -r b4ed07cbe954 -r 5689f0db4508 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)