# [isabelle] Function Termination

*To*: isabelle-users at cl.cam.ac.uk
*Subject*: [isabelle] Function Termination
*From*: René Neumann <lists at necoro.eu>
*Date*: Tue, 23 Aug 2011 23:19:19 +0200
*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.17) Gecko/20110808 Lightning/1.0b3pre Thunderbird/3.1.10

Hi all,
I had to define a function that needed its own proof of termination.
Thereby I noticed an issue, I'd like to show by example:
Let succs :: "('a × 'a) set ⇒ 'a ⇒ 'a set"
and then define some example function "foo":
function foo :: "('a × 'a) set ⇒ 'a ⇒ nat ⇒ nat" where
"foo E v n = (if n > 0 then
fold (λv'.λn. if n = 0 then 0
else foo E v' n) (n - 1) (succs E v)
else 0)"
This function might f.ex. being seen as walking depth-first through a
graph, doing at most n steps.
The problem now arises when showing termination: A 'termination proof'
wants me to show the following goal (the concrete measurement ?R should
be unimportant to my issue, but should probably rely on n):
⋀E v n x xa. ⟦0 < n; xa ≠ 0⟧ ⟹ ((E, x, xa), E, v, n) ∈ ?R
As you might notice there is no relation between xa and n, though it
should be something like "xa = n - 1".
Is it possible somehow to put the relation in again without doing some
heavy rewriting of the function? (As this might work for one case but
not for another)
Thanks,
René

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