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





On 03/04/2016 22:16, Lars Hupel wrote:
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).

Yes. I initially tried defining it as fun, but switched it over to function when one of the automatic proofs failed, and had auto do the completeness proof like this:

function (domintros) index:: "int â int" where
"index a = (if (a<0) then (index (a+5)) else (a mod 5))"
apply(auto)
done



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.

Ah. I did see in the "Defining Recursive Functions in Isabelle/HOL" manual that fun is equivalent to function with "termination by lexicographic_order". Somehow I completely missed the section "the relation method" section further down the same page.

Thanks for the assist.

--
DH




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