Re: [isabelle] Function Termination



Hi Rene,

  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.

Cheers,
Konrad.


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)
>
> Thanks,
> René
>
>





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