Theory Bit_Shifts_Infix_Syntax

(*
 * Copyright Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

(* Author: Jeremy Dawson, NICTA *)

section ‹Shift operations with infix syntax›

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

context semiring_bit_operations
begin

definition shiftl :: ‹'a ⇒ nat ⇒ 'a›  (infixl ‹<<› 55)
  where [code_unfold]: ‹a << n = push_bit n a›

lemma bit_shiftl_iff [bit_simps]:
  ‹bit (a << m) n ⟷ m ≤ n ∧ possible_bit TYPE('a) n ∧ bit a (n - m)›
  by (simp add: shiftl_def bit_simps)

definition shiftr :: ‹'a ⇒ nat ⇒ 'a›  (infixl ‹>>› 55)
  where [code_unfold]: ‹a >> n = drop_bit n a›

lemma bit_shiftr_eq [bit_simps]:
  ‹bit (a >> n) = bit a ∘ (+) n›
  by (simp add: shiftr_def bit_simps)

end

definition sshiftr :: ‹'a::len word ⇒ nat ⇒ 'a word›  (infixl ‹>>>› 55)
  where [code_unfold]: ‹w >>> n = signed_drop_bit n w›

lemma bit_sshiftr_iff [bit_simps]:
  ‹bit (w >>> m) n ⟷ bit w (if LENGTH('a) - m ≤ n ∧ n < LENGTH('a) then LENGTH('a) - 1 else m + n)›
  for w :: ‹'a::len word›
  by (simp add: sshiftr_def bit_simps)

context
  includes lifting_syntax
begin

lemma shiftl_word_transfer [transfer_rule]:
  ‹(pcr_word ===> (=) ===> pcr_word) (λk n. push_bit n k) (<<)›
  apply (unfold shiftl_def)
  apply transfer_prover
  done

lemma shiftr_word_transfer [transfer_rule]:
  ‹((pcr_word :: int ⇒ 'a::len word ⇒ _) ===> (=) ===> pcr_word)
    (λk n. drop_bit n (take_bit LENGTH('a) k))
    (>>)›
proof -
  have ‹((pcr_word :: int ⇒ 'a::len word ⇒ _) ===> (=) ===> pcr_word)
    (λk n. (drop_bit n ∘ take_bit LENGTH('a)) k)
    (>>)›
    by (unfold shiftr_def) transfer_prover
  then show ?thesis
    by simp
qed

lemma sshiftr_transfer [transfer_rule]:
  ‹((pcr_word :: int ⇒ 'a::len word ⇒ _) ===> (=) ===> pcr_word)
    (λk n. drop_bit n (signed_take_bit (LENGTH('a) - Suc 0) k))
    (>>>)›
proof -
  have ‹((pcr_word :: int ⇒ 'a::len word ⇒ _) ===> (=) ===> pcr_word)
    (λk n. (drop_bit n ∘ signed_take_bit (LENGTH('a) - Suc 0)) k)
    (>>>)›
    by (unfold sshiftr_def) transfer_prover
  then show ?thesis
    by simp
qed

end

context semiring_bit_operations
begin

lemma shiftl_0 [simp]:
  ‹0 << n = 0›
  by (simp add: shiftl_def)

lemma shiftl_of_0 [simp]:
  ‹a << 0 = a›
  by (simp add: shiftl_def)

lemma shiftl_of_Suc [simp]:
  ‹a << Suc n = (a * 2) << n›
  by (simp add: shiftl_def)

lemma shiftl_1 [simp]:
  ‹1 << n = 2 ^ n›
  by (simp add: shiftl_def)

lemma shiftl_numeral_Suc [simp]:
  ‹numeral m << Suc n = push_bit (Suc n) (numeral m)›
  by (fact shiftl_def)

lemma shiftl_numeral_numeral [simp]:
  ‹numeral m << numeral n = push_bit (numeral n) (numeral m)›
  by (fact shiftl_def)

lemma shiftr_0 [simp]:
  ‹0 >> n = 0›
  by (simp add: shiftr_def)

lemma shiftr_of_0 [simp]:
  ‹a >> 0 = a›
  by (simp add: shiftr_def)

lemma shiftr_1 [simp]:
  ‹1 >> n = of_bool (n = 0)›
  by (simp add: shiftr_def)

lemma shiftr_numeral_Suc [simp]:
  ‹numeral m >> Suc n = drop_bit (Suc n) (numeral m)›
  by (fact shiftr_def)

lemma shiftr_numeral_numeral [simp]:
  ‹numeral m >> numeral n = drop_bit (numeral n) (numeral m)›
  by (fact shiftr_def)

lemma shiftl_eq_mult:
  ‹x << n = x * 2 ^ n›
  unfolding shiftl_def by (fact push_bit_eq_mult)

lemma shiftr_eq_div:
  ‹x >> n = x div 2 ^ n›
  unfolding shiftr_def by (fact drop_bit_eq_div)

end

lemmas shiftl_int_def = shiftl_eq_mult[of x for x::int]
lemmas shiftr_int_def = shiftr_eq_div[of x for x::int]

lemma int_shiftl_BIT: fixes x :: int
  shows int_shiftl0: "x << 0 = x"
  and int_shiftl_Suc: "x << Suc n = 2 * x << n"
  by (auto simp add: shiftl_int_def)

context ring_bit_operations
begin

context
  includes bit_operations_syntax
begin

lemma shiftl_minus_1_numeral [simp]:
  ‹- 1 << numeral n = NOT (mask (numeral n))›
  by (simp add: shiftl_def)

end

end

lemma shiftl_Suc_0 [simp]:
  ‹Suc 0 << n = 2 ^ n›
  by (simp add: shiftl_def)

lemma shiftr_Suc_0 [simp]:
  ‹Suc 0 >> n = of_bool (n = 0)›
  by (simp add: shiftr_def)

lemma sshiftr_numeral_Suc [simp]:
  ‹numeral m >>> Suc n = signed_drop_bit (Suc n) (numeral m)›
  by (fact sshiftr_def)

lemma sshiftr_numeral_numeral [simp]:
  ‹numeral m >>> numeral n = signed_drop_bit (numeral n) (numeral m)›
  by (fact sshiftr_def)

context ring_bit_operations
begin

lemma shiftl_minus_numeral_Suc [simp]:
  ‹- numeral m << Suc n = push_bit (Suc n) (- numeral m)›
  by (fact shiftl_def)

lemma shiftl_minus_numeral_numeral [simp]:
  ‹- numeral m << numeral n = push_bit (numeral n) (- numeral m)›
  by (fact shiftl_def)

lemma shiftr_minus_numeral_Suc [simp]:
  ‹- numeral m >> Suc n = drop_bit (Suc n) (- numeral m)›
  by (fact shiftr_def)

lemma shiftr_minus_numeral_numeral [simp]:
  ‹- numeral m >> numeral n = drop_bit (numeral n) (- numeral m)›
  by (fact shiftr_def)

end

lemma sshiftr_0 [simp]:
  ‹0 >>> n = 0›
  by (simp add: sshiftr_def)

lemma sshiftr_of_0 [simp]:
  ‹w >>> 0 = w›
  by (simp add: sshiftr_def)

lemma sshiftr_1 [simp]:
  ‹(1 :: 'a::len word) >>> n = of_bool (LENGTH('a) = 1 ∨ n = 0)›
  by (simp add: sshiftr_def)

lemma sshiftr_minus_numeral_Suc [simp]:
  ‹- numeral m >>> Suc n = signed_drop_bit (Suc n) (- numeral m)›
  by (fact sshiftr_def)

lemma sshiftr_minus_numeral_numeral [simp]:
  ‹- numeral m >>> numeral n = signed_drop_bit (numeral n) (- numeral m)›
  by (fact sshiftr_def)

end