# [isabelle-dev] Isabelle2016-RC0: potential changes

Manuel Eberl eberlm at in.tum.de
Mon Jan 11 11:16:56 CET 2016

```> I’m puzzled. In ~~/src/HOL/Library/Poly_Deriv.thy I found no notion of algebraic number.
Oh, yes, you're right. It's in
https://bitbucket.org/isa-afp/afp-devel/src/363fdbc2f28c2503095a245f00db3d2805ed3ff9/thys/Liouville_Numbers/Liouville_Numbers_Misc.thy
.

> Its definitely not optimal, and you’re right that one can improve it
> by using an inline-version of listprod [k+1..n], but even the version
> that is mentioned in Algebraic_Numbers/Improved_Code_Equations.html is
> by far better than the current setup, since that just uses the
> recursive direct definition of binomial. (I noticed this since I got
> timeouts in my experiments with algebraic numbers and one of the
> culprits was binomial!)

I suggest this:

function fold_atLeastAtMost_nat where
[simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc =
(if a > b then acc else fold_atLeastAtMost_nat f (a+1)
b (f a acc))"
by pat_completeness auto
termination by (relation "measure (λ(_,a,b,_). Suc b - a)") auto

lemma fold_atLeastAtMost_nat:
assumes "comp_fun_commute f"
shows   "fold_atLeastAtMost_nat f a b acc = Finite_Set.fold f acc {a..b}"
using assms
proof (induction f a b acc rule: fold_atLeastAtMost_nat.induct, goal_cases)
case (1 f a b acc)
interpret comp_fun_commute f by fact
show ?case
proof (cases "a > b")
case True
thus ?thesis by (subst fold_atLeastAtMost_nat.simps) auto
next
case False
with 1 show ?thesis
by (subst fold_atLeastAtMost_nat.simps)
(auto simp: atLeastAtMost_insertL[symmetric] fold_fun_left_comm)
qed
qed

lemma setprod_atLeastAtMost_code:
"setprod f {a..b} = fold_atLeastAtMost_nat (λa acc. f a * acc) a b 1"
proof -
have "comp_fun_commute (λa. op * (f a))"
by unfold_locales (auto simp: o_def mult_ac)
thus ?thesis
by (simp add: setprod.eq_fold fold_atLeastAtMost_nat o_def)
qed

lemma fact_altdef': "fact n = of_nat (∏{1..n})"
by (induction n)
One_nat_def [symmetric]

lemma fact_code [code]:
"fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a ::
semiring_char_0)"
proof -
have "fact n = (of_nat (∏{1..n}) :: 'a)" by (simp add: fact_altdef')
also have "∏{1..n} = ∏{2..n}"
by (intro setprod.mono_neutral_right) auto
also have "… = fold_atLeastAtMost_nat (op *) 2 n 1"
finally show ?thesis .
qed

lemma binomial_code [code]:
"(n choose k) =
(if k > n then 0
else if 2 * k > n then (n choose (n - k))
else (fold_atLeastAtMost_nat (op *) (n-k+1) n 1 div fact k))"
proof -
{
assume "k ≤ n"
hence "{1..n} = {1..n-k} ∪ {n-k+1..n}" by auto
hence "(fact n :: nat) = fact (n-k) * ∏{n-k+1..n}"