# Re: [isabelle] Termination Proof

Hi Jason,

theory Termination
imports Nat Multiset Divides Datatype

`First, you should import Parity, which already has the "even" predicate.
``And as Tobias said, if you don't import Main, you may not get the tools
``you expect, just some unfinished pieces lying around.
`

inductive_set even :: "nat set" where
zero[intro!]: "0 ∈ even" |
step[intro!]: "n ∈ even ⟹ (Suc (Suc n)) ∈ even"

If you define even yourself, proving a rewrite rule
"Suc n : even <-> ~ n : even" helps in the termination proof.

function (sequential) foo :: "nat ⇒ nat list" where
"foo 0 = [0]" |
"foo (Suc 0) = [1]" |
"foo n = (case n ∈ even of
True ⇒ n # foo (n div 2) |
False ⇒ n # foo (Suc n))"
by pat_completeness auto
termination
apply (relation "measures [Suc, λn. n div 2]")
apply auto
oops

My understanding of the above proof attempt is that it will never work
because the well founded relation needs for the "n \<notin> even" case to
decrease or stay the same, but instead it gets larger in the recursive call.

`Yes. This measure does not work. In such a situation where there is a
``temporary increase like this, you can anticipate this in the definition
``of the measure, and assign a measure that already corresponds to the
``increased value.
`

`The following works for this example, assuming the [simp] rule mentioned
``above:
`
termination
apply (relation "measures
[%n. if n <= 1 then 0 else if n : even then n else Suc n,
%n. if n : even then 0 else 1]")
apply auto
done

I can also imagine a proof of termination based on the fact that if n is odd
then Suc n will be even and the next call to foo will cause the argument to
shrink by more than it grew. Is it possible to write such a proof and lease
the termination checker?

I would assume that the idea above works in general.

`There is also a different approach to handle this in the termination
``prower itself, not in the measure function. It is sketched in Sect. 6 of
``this paper:
``http://www4.informatik.tu-muenchen.de/~krauss/shallowdp/shallowdp.pdf
``But I never finished the implementation, mainly because these functions
``don't arise so often, and if they do, there is always a simple manual
``solution. Moreover, detecting the situation automatically is not so easy.
`
Hope this helps...
Alex

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