[isabelle] Function Termination

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)


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