[isabelle-dev] Efficient code for Discrete.log

[Manuel Eberl]

Hallo,

I'm considering adding efficient code for Discrete.log (the dual
logarithm on natural numbers). PolyML does provide an IntInf.log2
function that seems reasonably efficient so that one can set up code
printing. However, I am struggling with one detail:

Where would the code that does this actually reside? I cannot really put
it into Discrete.thy, because then that would have to import
Code_Target_Numeral. I could put it into Code_Target_Integer.thy, but
then that would have to import Discrete, which does not sound right to
me either.

I attached what I have so far.

Manuel

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170629/60a36e42/attachment.html>
-------------- next part --------------
theory Efficient_Log2
imports
  Main
  "~~/src/HOL/Library/Discrete" 
  "~~/src/HOL/Library/Code_Target_Numeral"
begin

context
includes integer.lifting
begin

qualified lift_definition intlog2 :: "integer \<Rightarrow> integer" is
  "\<lambda>n. int (Discrete.log (nat n))" .

qualified function intlog2_aux :: "integer \<Rightarrow> integer \<Rightarrow> integer" where
  "intlog2_aux n acc = (if n < 2 then acc else intlog2_aux (n div 2) (acc + 1))"
  by auto
termination proof (relation "measure (nat_of_integer \<circ> fst)")
  fix n acc :: integer
  assume "\<not>n < 2"
  hence "nat_of_integer (n div 2) < nat_of_integer n"
    by transfer auto
  thus "((n div 2, acc + 1), (n, acc)) \<in> measure (nat_of_integer \<circ> fst)" 
    by simp
qed simp_all

declare intlog2_aux.simps [simp del]
  
qualified lemma intlog2_aux_correct: "acc \<ge> 0 \<Longrightarrow> intlog2_aux n acc = intlog2 n + acc"
proof (induction n acc arbitrary: acc rule: intlog2_aux.induct)
  case (1 n acc)
  show ?case
  proof (cases "n < 2")
    case True
    hence "intlog2 n = 0" by transfer (simp add: Discrete.log.simps)
    with True show ?thesis by (subst intlog2_aux.simps) auto
  next
    case False
    hence "intlog2 n = intlog2 (n div 2) + 1"
    proof (transfer, goal_cases)
      case (1 m)
      hence "int (Discrete.log (nat m)) = int (Discrete.log (nat m div 2)) + 1"
        by (subst Discrete.log.simps) auto
      also have "nat m div 2 = nat (m div 2)" by simp
      finally show ?case .
    qed
    with False show ?thesis by (subst intlog2_aux.simps) (auto simp: 1)
  qed
qed
  
qualified lemma intlog2_code [code]: "intlog2 n = intlog2_aux n 0"
  by (simp add: intlog2_aux_correct)

lemma Discrete_log_code [code abstract]:
  "integer_of_nat (Discrete.log n) = (if n = 0 then 0 else intlog2 (of_nat n))"
  by transfer simp

end

code_printing
  constant "Efficient_Log2.intlog2 :: integer \<Rightarrow> _" \<rightharpoonup> 
    (SML) "IntInf.log2" and
    (Eval) "IntInf.log2"

value [code] "Discrete.log 12345"

export_code Discrete.log checking SML Eval Scala Haskell? OCaml?

end