--- a/src/HOL/ex/Word.thy Fri Jul 03 06:18:27 2020 +0000
+++ b/src/HOL/ex/Word.thy Fri Jul 03 06:18:29 2020 +0000
@@ -37,7 +37,7 @@
qed
lemma signed_take_bit_Suc:
- "signed_take_bit (Suc n) k = signed_take_bit n (k div 2) * 2 + k mod 2"
+ "signed_take_bit (Suc n) k = k mod 2 + 2 * signed_take_bit n (k div 2)"
by (simp add: odd_iff_mod_2_eq_one signed_take_bit_eq_take_bit algebra_simps take_bit_Suc)
lemma signed_take_bit_of_0 [simp]:
@@ -80,6 +80,21 @@
qed
qed
+lemma signed_take_bit_code [code]:
+ \<open>signed_take_bit n k =
+ (let l = take_bit (Suc n) k
+ in if bit l n then l - push_bit n 2 else l)\<close>
+proof (induction n arbitrary: k)
+ case 0
+ then show ?case
+ by (simp add: mod_2_eq_odd and_one_eq)
+next
+ case (Suc n)
+ from Suc [of \<open>k div 2\<close>]
+ show ?case
+ by (auto simp add: Let_def push_bit_eq_mult algebra_simps take_bit_Suc [of \<open>Suc n\<close>] bit_Suc signed_take_bit_Suc elim!: evenE oddE)
+qed
+
subsection \<open>Bit strings as quotient type\<close>