Re: [isabelle] Function Termination
Since there is an occurrence of fold, you need to have
a congruence rule for fold installed so the termination
extraction machinery will do the right thing. I imagine
the documentation discusses this.
On Tue, Aug 23, 2011 at 4:19 PM, René Neumann <lists at necoro.eu> wrote:
> 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