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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
