src/HOL/Library/Code_Bit_Shifts_for_Arithmetic.thy

typo

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

section \<open>Rewrite arithmetic operations to bit-shifts if feasible\<close>

theory Code_Bit_Shifts_for_Arithmetic
  imports Main
begin

context semiring_bit_operations
begin

context
  includes bit_operations_syntax
begin

lemma [code_unfold]:
  \<open>of_bool (odd a) = a AND 1\<close>
  by (simp add: and_one_eq mod2_eq_if)

lemma [code_unfold]:
  \<open>even a \<longleftrightarrow> a AND 1 = 0\<close>
  by (simp add: and_one_eq mod2_eq_if)

lemma [code_unfold]:
  \<open>2 * a = push_bit 1 a\<close>
  by (simp add: ac_simps)

lemma [code_unfold]:
  \<open>a * 2 = push_bit 1 a\<close>
  by simp

lemma [code_unfold]:
  \<open>2 ^ n * a = push_bit n a\<close>
  by (simp add: push_bit_eq_mult ac_simps)

lemma [code_unfold]:
  \<open>a * 2 ^ n = push_bit n a\<close>
  by (simp add: push_bit_eq_mult)

lemma [code_unfold]:
  \<open>a div 2 = drop_bit 1 a\<close>
  by (simp add: drop_bit_eq_div)

lemma [code_unfold]:
  \<open>a div 2 ^ n = drop_bit n a\<close>
  by (simp add: drop_bit_eq_div)

lemma [code_unfold]:
  \<open>a mod 2 = take_bit 1 a\<close>
  by (simp add: take_bit_eq_mod)

lemma [code_unfold]:
  \<open>a mod 2 ^ n  = take_bit n a\<close>
  by (simp add: take_bit_eq_mod)

end

end

end