SSL Code_Bit_Shifts_for_Arithmetic.thy

(*  Title:      HOL/Library/Code_Bit_Shifts_for_Arithmetic.thy
  Author: Florian Haftmann, TU Muenchen
*)

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