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:

## Advertising

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

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

_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev