# HG changeset patch
# User haftmann
# Date 1592632588 0
# Node ID e18e9ac8c2051910725631b7c9ab22833a3d8a26
# Parent  d45f5d4c41bd41ae2e1a25feaf023062acda1e63
simp rules for conversions

diff -r d45f5d4c41bd -r e18e9ac8c205 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sat Jun 20 05:56:28 2020 +0000
+++ b/src/HOL/Parity.thy	Sat Jun 20 05:56:28 2020 +0000
@@ -1649,20 +1649,24 @@
   by (simp add: drop_bit_eq_div minus_1_div_exp_eq_int)
 
 lemma take_bit_minus:
-  "take_bit n (- (take_bit n k)) = take_bit n (- k)"
+  \<open>take_bit n (- take_bit n k) = take_bit n (- k)\<close>
     for k :: int
   by (simp add: take_bit_eq_mod mod_minus_eq)
 
 lemma take_bit_diff:
-  "take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)"
+  \<open>take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)\<close>
     for k l :: int
   by (simp add: take_bit_eq_mod mod_diff_eq)
 
 lemma take_bit_nonnegative [simp]:
-  "take_bit n k \<ge> 0"
+  \<open>take_bit n k \<ge> 0\<close>
     for k :: int
   by (simp add: take_bit_eq_mod)
 
+lemma (in ring_1) of_nat_nat_take_bit_eq [simp]:
+  \<open>of_nat (nat (take_bit n k)) = of_int (take_bit n k)\<close>
+  by simp
+
 lemma take_bit_minus_small_eq:
   \<open>take_bit n (- k) = 2 ^ n - k\<close> if \<open>0 < k\<close> \<open>k \<le> 2 ^ n\<close> for k :: int
 proof -