*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Termination of function on DAG nodes*From*: Rupert Swarbrick <rswarbrick at gmail.com>*Date*: Mon, 27 Jun 2016 20:50:42 +0100*References*: <od634d-qs6.ln1@halibut.with-a-lisp.net> <69ea265d-c1ec-c204-7993-17e4e0f763de@in.tum.de>*User-agent*: Gnus/5.13 (Gnus v5.13) Emacs/24.5 (gnu/linux)

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 >> >>

**References**:**[isabelle] Termination of function on DAG nodes***From:*Rupert Swarbrick

**Re: [isabelle] Termination of function on DAG nodes***From:*Tobias Nipkow

- Previous by Date: [isabelle] Strange behaviour of Isabelle (Polyml) on Windows 8.1
- Next by Date: [isabelle] new AFP entry: IP Addresses
- Previous by Thread: Re: [isabelle] Termination of function on DAG nodes
- Next by Thread: [isabelle] 2 new AFP entries
- Cl-isabelle-users June 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list