next up previous contents
Next: Boolean-valued Relations 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 [McKinna, 1992].

 ** Module lib_more_induction Imports lib_nat/lib_nat
  nat_iter_induction = ... :
    {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 = ... :
    {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 = ... :
    {phi:Pred gamma}{n:nat}(phi (nat_iter z s n))->
    ({g:gamma}(phi (s g))->phi g)->phi z

Fri May 24 19:01:27 BST 1996