Theory Optimize_Integer

section ‹Optimizations for Code Integer›
theory Optimize_Integer
imports
  Complex_Main
  "HOL-Library.Code_Target_Numeral"
begin

text ‹shallowly embed log and power›

definition log2::"int ⇒ int"
  where "log2 a = floor (log 2 (of_int a))"

context includes integer.lifting begin

lift_definition log2_integer :: "integer ⇒ integer"
  is "log2 :: int ⇒ int"
  .

end

lemma [code]: "log2 (int_of_integer a) = int_of_integer (log2_integer a)"
  by (simp add: log2_integer.rep_eq)

code_printing
  constant "log2_integer :: integer ⇒ _" ⇀
    (SML) "IntInf.log2"

definition power_int::"int ⇒ int ⇒ int"
  where "power_int a b = a ^ (nat b)"

context includes integer.lifting begin

lift_definition power_integer :: "integer ⇒ integer ⇒ integer"
  is "power_int :: int ⇒ int ⇒ int"
  .

end

code_printing
  constant "power_integer :: integer ⇒ _ ⇒ _" ⇀
    (SML) "IntInf.pow ((_), (_))"

lemma [code]: "power_int (int_of_integer a) (int_of_integer b) = int_of_integer (power_integer a b)"
  by (simp add: power_integer.rep_eq)

end