Theory Word_Lib.Bit_Shifts_Infix_Syntax
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
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