Theory Word_Lib.Singleton_Bit_Shifts

theory Singleton_Bit_Shifts
  imports
    "HOL-Library.Word"
    Bit_Shifts_Infix_Syntax
begin

definition shiftl1 :: ‹'a::len word ⇒ 'a word›
  where shiftl1_eq_double: ‹shiftl1 = times 2›

lemma bit_shiftl1_iff [bit_simps]:
  ‹bit (shiftl1 w) n ⟷ 0 < n ∧ n < LENGTH('a) ∧ bit w (n - 1)›
  for w :: ‹'a::len word›
  by (auto simp add: shiftl1_eq_double bit_simps)

definition shiftr1 :: ‹'a::len word ⇒ 'a word›
  where shiftr1_eq_half: ‹shiftr1 w = w div 2›

lemma bit_shiftr1_iff [bit_simps]:
  ‹bit (shiftr1 w) n ⟷ bit w (Suc n)›
  for w :: ‹'a::len word›
  by (simp add: shiftr1_eq_half bit_Suc)

definition sshiftr1 :: ‹'a::len word ⇒ 'a word›
  where sshiftr1_def: ‹sshiftr1 = signed_drop_bit 1›

lemma bit_sshiftr1_iff [bit_simps]:
  ‹bit (sshiftr1 w) n ⟷ bit w (if n = LENGTH('a) - 1 then LENGTH('a) - 1 else Suc n)›
  for w :: ‹'a::len word›
  by (auto simp add: sshiftr1_def bit_simps)

lemma shiftl1_def:
  ‹shiftl1 = push_bit 1›
  by (rule ext, rule bit_word_eqI) (simp add: bit_simps mult.commute [of _ 2])

lemma shiftr1_def:
  ‹shiftr1 = drop_bit 1›
  by (rule ext, rule bit_word_eqI) (simp add: bit_simps)

lemma shiftr1_1:
  ‹shiftr1 (1::'a::len word) = 0›
  by (rule bit_word_eqI) (simp add: bit_simps)

lemma sshiftr1_eq:
  ‹sshiftr1 w = word_of_int (sint w div 2)›
  by (rule bit_word_eqI) (auto simp add: bit_simps min_def simp flip: bit_Suc elim: le_SucE)

lemma shiftl1_eq:
  ‹shiftl1 w = word_of_int (2 * uint w)›
  by (rule bit_word_eqI) (auto simp add: bit_simps)

lemma shiftr1_eq:
  ‹shiftr1 w = word_of_int (uint w div 2)›
  by (rule bit_word_eqI) (simp add: bit_simps flip: bit_Suc)

lemma shiftl1_rev:
  ‹shiftl1 w = word_reverse (shiftr1 (word_reverse w))›
  by (rule bit_word_eqI) (auto simp add: bit_simps Suc_diff_Suc simp flip: bit_Suc)

lemma shiftl1_p:
  ‹shiftl1 w = w + w›
  by (rule bit_word_eqI) (simp add: bit_simps)

lemma shiftr1_bintr:
  ‹(shiftr1 (numeral w) :: 'a::len word) =
    word_of_int (take_bit LENGTH('a) (numeral w) div 2)›
  apply (rule bit_word_eqI)
  apply (simp add: bit_simps flip: bit_Suc)
  done

lemma sshiftr1_sbintr:
  ‹(sshiftr1 (numeral w) :: 'a::len word) =
    word_of_int (signed_take_bit (LENGTH('a) - 1) (numeral w) div 2)›
  apply (rule bit_word_eqI)
  apply (simp add: bit_simps flip: bit_Suc)
  apply transfer
  apply auto
  done

lemma shiftl1_wi:
  ‹shiftl1 (word_of_int w) = word_of_int (2 * w)›
  by (rule bit_word_eqI) (simp add: bit_simps)

lemma shiftl1_numeral:
  ‹shiftl1 (numeral w) = numeral (Num.Bit0 w)›
  by (rule bit_word_eqI) (auto simp add: bit_simps bit_numeral_Bit0_iff)

lemma shiftl1_neg_numeral:
  ‹shiftl1 (- numeral w) = - numeral (Num.Bit0 w)›
  by (simp add: shiftl1_eq_double)

lemma shiftl1_0:
  ‹shiftl1 0 = 0›
  by (rule bit_word_eqI) (simp add: bit_simps)

lemma shiftl1_def_u:
  ‹shiftl1 w = word_of_int (2 * uint w)›
  by (rule bit_word_eqI) (simp add: bit_simps)

lemma shiftl1_def_s:
  ‹shiftl1 w = word_of_int (2 * sint w)›
  by (rule bit_word_eqI) (simp add: bit_simps)

lemma shiftr1_0:
  ‹shiftr1 0 = 0›
  by (rule bit_word_eqI) (simp add: bit_simps)

lemma sshiftr1_0:
  ‹sshiftr1 0 = 0›
  by (rule bit_word_eqI) (simp add: bit_simps)

lemma sshiftr1_n1:
  ‹sshiftr1 (- 1) = - 1›
  by (rule bit_word_eqI) (auto simp add: bit_simps)

lemma uint_shiftr1:
  ‹uint (shiftr1 w) = uint w div 2›
  by (rule bit_eqI) (simp add: bit_simps flip: bit_Suc)

lemma shiftr1_div_2:
  ‹uint (shiftr1 w) = uint w div 2›
  by (fact uint_shiftr1)

lemma sshiftr1_div_2:
  ‹sint (sshiftr1 w) = sint w div 2›
  by (rule bit_eqI) (auto simp add: bit_simps simp flip: bit_Suc)

lemma nth_shiftl1:
  ‹bit (shiftl1 w) n ⟷ n < size w ∧ n > 0 ∧ bit w (n - 1)›
  by (auto simp add: word_size bit_simps)

lemma nth_shiftr1:
  ‹bit (shiftr1 w) n = bit w (Suc n)›
  by (fact bit_shiftr1_iff)

lemma nth_sshiftr1:
  ‹bit (sshiftr1 w) n = (if n = size w - 1 then bit w n else bit w (Suc n))›
  by (auto simp add: word_size bit_simps)

lemma shiftl_power:
  ‹(shiftl1 ^^ x) (y::'a::len word) = 2 ^ x * y›
  by (simp add: shiftl1_eq_double funpow_double_eq_push_bit push_bit_eq_mult)

lemma le_shiftr1:
  ‹shiftr1 u ≤ shiftr1 v› if ‹u ≤ v›
  using that by (simp add: shiftr1_eq_half word_less_eq_imp_half_less_eq)

lemma le_shiftr1':
  ‹u ≤ v› if ‹shiftr1 u ≤ shiftr1 v› ‹shiftr1 u ≠ shiftr1 v›
  by (rule word_half_less_imp_less_eq) (use that in ‹simp add: shiftr1_eq_half›)

lemma sshiftr_eq_funpow_sshiftr1:
  ‹w >>> n = (sshiftr1 ^^ n) w›
proof -
  have ‹sshiftr1 ^^ n = (signed_drop_bit n :: 'a word ⇒ _)›
    by (induction n) (simp_all add: sshiftr1_def)
  then show ?thesis
    by (simp add: sshiftr_def)
qed

end