Re: [isabelle] Base case in termination proof..



Hi Daniel,

> and have been trying to prove the result is always >=0 and <= 4. Ran
> into a bit of trouble and after some investigation found that it was
> because Isabelle couldn't automatically prove termination..

if you use the "function" command, Isabelle doesn't even attempt to
prove termination. Only the "fun" command performs automatic proofs
(which fail in this case, however).

If your function is total (it is), you can use the "termination" command
to establish a termination proof.

Here's how it works for your example:

  termination index
  by (relation "measure (În. nat (- n))") auto

As you can see, you just have to specify a suitable measure function
under which the function arguments decrease on each call. The rest is
automatic.

You can then use the total induction rule for your lemmas:

  lemma "index n â 0"
  by (induct n rule: index.induct) auto

  lemma "index n â 4"
  by (induct n rule: index.induct) auto

Cheers
Lars




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