src/HOL/ex/Note_on_signed_division_on_words.thy

note on signed division on words

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