[isabelle] Factorial Equivalent Iterative Factorial



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 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.