Re: [isabelle] Factorial Equivalent Iterative Factorial
Try proving something like this as a lemma, using induction on n:
ALL a. Fi n a = a * F n
Then F n = Fi n 1 easily follows from this.
Quoting TIMOTHY KREMANN <twksoa262 at verizon.net>:
I have the following two primrecs (n! and a iterative version)
primrec F::"nat => nat"
"F 0 = 1"
| "F (Suc n) = Suc n * F n"
primrec Fi::"nat => nat => nat"
"Fi 0 a = a"
| "Fi (Suc n) a = Fi n (Suc n * a)"
I want to prove
F n = Fi n 1
I have not made much progress and am wondering if someone has done
this already or knows of a similar proof that would give me some
This archive was generated by a fusion of
Pipermail (Mailman edition) and