*To*: TIMOTHY KREMANN <twksoa262 at verizon.net>*Subject*: Re: [isabelle] Factorial Equivalent Iterative Factorial*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Thu, 19 Mar 2009 02:01:10 -0700*Cc*: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <668979.2404.qm@web84007.mail.mud.yahoo.com>*References*: <668979.2404.qm@web84007.mail.mud.yahoo.com>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

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. - Brian Quoting TIMOTHY KREMANN <twksoa262 at 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 1I have not made much progress and am wondering if someone has donethis already or knows of a similar proof that would give me somehints.Thanks, TIm

**References**:**[isabelle] Factorial Equivalent Iterative Factorial***From:*TIMOTHY KREMANN

- Previous by Date: [isabelle] Factorial Equivalent Iterative Factorial
- Next by Date: [isabelle] About Generalization theory
- Previous by Thread: [isabelle] Factorial Equivalent Iterative Factorial
- Next by Thread: [isabelle] About Generalization theory
- Cl-isabelle-users March 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list