Re: [isabelle] Termination of function on DAG nodes



That's brilliant. Thank you very much for the explanation.

Rupert

Tobias Nipkow <nipkow at in.tum.de> writes:
> You are in luck, the solution is easy, once you understand what's missing:
>
> declare setsum.cong[fundef_cong]
>
> You definition uses higher-order recursion, i.e. the recursive
> function foo is not applied directly to any arguments but passed to
> setsum, and who knows what setsum might be doing with it. The
> congruence rule setsum.cong explains that setsum applies foo only to
> elements of the set. The attribute [fundef_cong] passes this
> information on to fun/function. I will enable it in the distribution
> to prevent other people stumbling over it again.
>
> Tobias
>
> On 25/06/2016 22:33, Rupert Swarbrick wrote:
>> Hi there,
>>
>> I have a DAG (directed acyclic graph) with an associated height function
>> (a function from nodes to nat such that children have a lower height
>> than their parents). It's easy enough to prove that this gives an
>> induction rule of the form "(P on every child => P on parent) => P".
>>
>> What I want to do, however, is to define a function on graph nodes of
>> the form:
>>
>>    foo x = bar x + setsum foo (children x)
>>
>> Informally, this is well defined because I can define it for each height
>> inductively. However, I can't see how to prove this using
>> function/termination.
>>
>> Here's a cut down example:
>>
>>   theory foo
>>     imports Main
>>   begin
>>
>>   text {*
>>     A really simple locale that represents a DAG by requiring it to have a
>>     height function. The nodes of the graph are the universe of 'a.
>>   *}
>>   locale dag =
>>     fixes children :: "'a â 'a set"
>>     fixes height :: "'a â nat"
>>     assumes "x â children y â height x < height y"
>>     fixes label :: "'a â nat"
>>
>>   context dag begin
>>
>>   function foo :: "'a â nat" where
>>     "foo x = label x + setsum foo (children x)"
>>     by auto
>>   termination
>>     apply (relation "measure (Î x. height x)")
>>
>> This isn't looking promising. Ignoring the fact that I might have chosen
>> a slightly wrong measure, I end up with the following goals:
>>
>>   proof (prove)
>>   goal (2 subgoals):
>>    1. wf (measure height)
>>    2. âx xa. (xa, x) â measure height
>>
>> Note that the second goal doesn't say anything about xa being a child of
>> x.
>>
>> Am I doing something wrong? How can I tell the function/termination
>> machinery what I'm trying to say?
>>
>> Also, a meta-question: I couldn't figure out the answer from the
>> otherwise extremely helpful "Defining Recursive Functions in
>> Isabelle/HOL" document. Is there somewhere else I should be looking for
>> such things?
>>
>>
>> Many thanks,
>>
>> Rupert
>>
>>





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