Theory HOL-Library.Code_Bit_Shifts_for_Arithmetic

(*  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