theory Note_on_signed_division_on_words
  imports "HOL-Library.Word" "HOL-Library.Centered_Division"
begin

unbundle bit_operations_syntax

context semiring_bit_operations
begin

lemma take_bit_Suc_from_most:
  ‹take_bit (Suc n) a = 2 ^ n * of_bool (bit a n) OR take_bit n a›
  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:
  ‹signed_take_bit m (2 ^ n) =
 (if n < m then 2 ^ n else if n = m then - (2 ^ n) else 0)›
  by (rule bit_eqI) (auto simp add: bit_simps simp flip: mask_eq_exp_minus_1)

end

lift_definition signed_divide_word :: ‹'a::len word → 'a word → 'a word›  (infixl ‹wdiv› 70)
  is ‹λa b. signed_take_bit (LENGTH('a) - Suc 0) a cdiv signed_take_bit (LENGTH('a) - Suc 0) b›
  by (simp flip: signed_take_bit_decr_length_iff)

lift_definition signed_modulo_word :: ‹'a::len word → 'a word → 'a word›  (infixl ‹wmod› 70)
  is ‹λa b. signed_take_bit (LENGTH('a) - Suc 0) a cmod signed_take_bit (LENGTH('a) - Suc 0) b›
  by (simp flip: signed_take_bit_decr_length_iff)

lemma signed_take_bit_eq_wmod:
  ‹signed_take_bit n w = w wmod (2 ^ Suc n)›
proof (transfer fixing: n)
  show ‹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 cmod signed_take_bit (LENGTH('a) - Suc 0) (2 ^ Suc n))› for k :: int
  proof (cases ‹LENGTH('a) = Suc (Suc n)›)
    case True
    then show ?thesis
      by (simp add: signed_take_bit_exp_eq_int signed_take_bit_take_bit cmod_minus_eq flip: power_Suc signed_take_bit_eq_cmod)
  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_cmod)
  qed
qed

end