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
apply (relation "measures [Suc, λn. n div 2]")
apply auto

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:

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

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: 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...

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