Re: [isabelle] Termination Proof
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 = " |
"foo (Suc 0) = " |
"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]")
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
The following works for this example, assuming the [simp] rule mentioned
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]")
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
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