# Re: [isabelle] Termination Proof

Jason Dagit schrieb:
> Hello,
>
> I was trying to prove termination for the following definition:
> \begin{code}
> theory Termination
> imports Nat Multiset Divides Datatype

Just a small remark: Nat, Divides and Datatype are subtheories of Main
and should not be imported selectively, they may not work as expect in
the absence of the rest of Main. In your case it was not a problem
because Multiset includes Main.

Tobias

> begin
>
> inductive_set even :: "nat set" where
> zero[intro!]: "0 ∈ even" |
> step[intro!]: "n ∈ even ⟹ (Suc (Suc n)) ∈ even"
>
> 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
> \end{code}
>
> I know I can change the definition slightly for foo to make it pass the
> termination checker using the standard lexicographical measure.  I'm
> learning about function package and specifically, how to write termination
> proofs so I want to avoid the easy route here.  I'm following this
> documentation in particular:
> http://isabelle.in.tum.de/doc/functions.pdf
>
> 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.
>
> 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?  Perhaps there is something that can be done with
> the function domain in the same way partial functions are handled?  Advice
> on how to get started with such a proof?  Perhaps there are examples of this