[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:126.96.36.199) Gecko/20110808 Lightning/1.0b3pre Thunderbird/3.1.10
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)
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