Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Factorial Equivalent Iterative Factorial

view this post on Zulip Email Gateway (Aug 18 2022 at 13:13):

From: TIMOTHY KREMANN <twksoa262@verizon.net>
I have the following two primrecs (n! and a iterative version)

primrec F::"nat => nat"
where
"F 0 = 1"
| "F (Suc n) = Suc n * F n"

primrec Fi::"nat => nat => nat"
where
"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 hints.

Thanks,
TIm

view this post on Zulip Email Gateway (Aug 18 2022 at 13:13):

From: Brian Huffman <brianh@cs.pdx.edu>
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@verizon.net>:

Last updated: May 03 2024 at 12:27 UTC