Theory HOL-Library.Code_Bit_Shifts_for_Arithmetic
section ‹Rewrite arithmetic operations to bit-shifts if feasible›
theory Code_Bit_Shifts_for_Arithmetic
imports Main
begin
context semiring_bit_operations
begin
context
includes bit_operations_syntax
begin
lemma [code_unfold]:
‹of_bool (odd a) = a AND 1›
by (simp add: and_one_eq mod2_eq_if)
lemma [code_unfold]:
‹even a ⟷ a AND 1 = 0›
by (simp add: and_one_eq mod2_eq_if)
lemma [code_unfold]:
‹2 * a = push_bit 1 a›
by (simp add: ac_simps)
lemma [code_unfold]:
‹a * 2 = push_bit 1 a›
by simp
lemma [code_unfold]:
‹2 ^ n * a = push_bit n a›
by (simp add: push_bit_eq_mult ac_simps)
lemma [code_unfold]:
‹a * 2 ^ n = push_bit n a›
by (simp add: push_bit_eq_mult)
lemma [code_unfold]:
‹a div 2 = drop_bit 1 a›
by (simp add: drop_bit_eq_div)
lemma [code_unfold]:
‹a div 2 ^ n = drop_bit n a›
by (simp add: drop_bit_eq_div)
lemma [code_unfold]:
‹a mod 2 = take_bit 1 a›
by (simp add: take_bit_eq_mod)
lemma [code_unfold]:
‹a mod 2 ^ n = take_bit n a›
by (simp add: take_bit_eq_mod)
end
end
end