# HG changeset patch
# User haftmann
# Date 1664874762 0
# Node ID 4a064fad28b2b7c4a7a969334fdf22fc4165afc8
# Parent  da4e57d30579badb88dbe7e50b4c4548cc9fd390
note on signed division on words

diff -r da4e57d30579 -r 4a064fad28b2 src/HOL/ex/Note_on_signed_division_on_words.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Note_on_signed_division_on_words.thy	Tue Oct 04 09:12:42 2022 +0000
@@ -0,0 +1,50 @@
+theory Note_on_signed_division_on_words
+  imports "HOL-Library.Word" "HOL-Library.Rounded_Division"
+begin
+
+unbundle bit_operations_syntax
+
+context semiring_bit_operations
+begin
+	
+lemma take_bit_Suc_from_most:
+  \<open>take_bit (Suc n) a = 2 ^ n * of_bool (bit a n) OR take_bit n a\<close>
+  by (rule bit_eqI) (auto simp add: bit_simps less_Suc_eq)
+	
+end
+	
+context ring_bit_operations
+begin
+	
+lemma signed_take_bit_exp_eq_int:
+  \<open>signed_take_bit m (2 ^ n) =
+    (if n < m then 2 ^ n else if n = m then - (2 ^ n) else 0)\<close>
+  by (rule bit_eqI) (auto simp add: bit_simps simp flip: mask_eq_exp_minus_1)
+	
+end
+
+lift_definition signed_divide_word :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>  (infixl \<open>wdiv\<close> 70)
+  is \<open>\<lambda>a b. signed_take_bit (LENGTH('a) - Suc 0) a rdiv signed_take_bit (LENGTH('a) - Suc 0) b\<close>
+  by (simp flip: signed_take_bit_decr_length_iff)
+
+lift_definition signed_modulo_word :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>  (infixl \<open>wmod\<close> 70)
+  is \<open>\<lambda>a b. signed_take_bit (LENGTH('a) - Suc 0) a rmod signed_take_bit (LENGTH('a) - Suc 0) b\<close>
+  by (simp flip: signed_take_bit_decr_length_iff)
+
+lemma signed_take_bit_eq_wmod:
+  \<open>signed_take_bit n w = w wmod (2 ^ Suc n)\<close>
+proof (transfer fixing: n)
+  show \<open>take_bit LENGTH('a) (signed_take_bit n (take_bit LENGTH('a) k)) =
+    take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - Suc 0) k rmod signed_take_bit (LENGTH('a) - Suc 0) (2 ^ Suc n))\<close> for k :: int
+  proof (cases \<open>LENGTH('a) = Suc (Suc n)\<close>)
+    case True
+    then show ?thesis
+      by (simp add: signed_take_bit_exp_eq_int signed_take_bit_take_bit rmod_minus_eq flip: power_Suc signed_take_bit_eq_rmod)
+  next
+    case False
+    then show ?thesis
+      by (auto simp add: signed_take_bit_exp_eq_int signed_take_bit_take_bit take_bit_signed_take_bit simp flip: power_Suc signed_take_bit_eq_rmod)
+  qed
+qed
+  
+end