[isabelle-dev] Isabelle2016-RC0: potential changes

[Manuel Eberl]

> 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)
      (simp_all add: setprod_nat_ivl_Suc' of_nat_mult [symmetric] 
One_nat_def [symmetric]
                del: of_nat_Suc of_nat_add of_nat_mult One_nat_def)

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"
     by (simp add: setprod_atLeastAtMost_code)
   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}"
       by (simp add: setprod.union_disjoint fact_altdef_nat)
   }
   thus ?thesis by (auto simp: binomial_altdef_nat mult_ac 
setprod_atLeastAtMost_code)
qed