next up previous contents
Next: Theorems about Successor Up: The Natural Numbers Previous: Iteration Principles

Induction Principles

This short file gives some induction principles which deal with the recursor and iterator on the natural numbers. For their use in inductive proofs using deliverables see (##mckinnaphd ##mckinnaphd).

 ** Module lib_more_induction Imports lib_nat
  nat_iter_induction = ... :
    [Pred=[a:Type]a->Prop]{gamma|Type}{z|gamma}{s|gamma->gamma}
    {phi:Pred gamma}(phi z)->({g:gamma}(phi g)->phi (s g))->
    [rec=nat_iter z s]{n:nat}phi (rec n)
  nat_rec_induction = ... :
    [Rel=[a:Type][b:Type]a->b->Prop]{gamma|Type}{z|gamma}
    {s|nat->gamma->gamma}{phi:Rel nat gamma}(phi zero z)->
    ({m:nat}{g:gamma}(phi m g)->phi (suc m) (s m g))->[rec=nat_rec z s]
    {n:nat}phi n (rec n)
  nat_iter_induction_rev = ... :
    [Pred=[a:Type]a->Prop]{gamma|Type}{z|gamma}{s|gamma->gamma}
    {phi:Pred gamma}{n:nat}(phi (nat_iter z s n))->
    ({g:gamma}(phi (s g))->phi g)->phi z



Conor McBride
11/13/1998