*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Termination of function on DAG nodes*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sun, 26 Jun 2016 00:55:34 +0200*In-reply-to*: <od634d-qs6.ln1@halibut.with-a-lisp.net>*References*: <od634d-qs6.ln1@halibut.with-a-lisp.net>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:45.0) Gecko/20100101 Thunderbird/45.1.1

You are in luck, the solution is easy, once you understand what's missing: declare setsum.cong[fundef_cong]

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

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] Termination of function on DAG nodes***From:*Rupert Swarbrick

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

- Previous by Date: [isabelle] Termination of function on DAG nodes
- Next by Date: [isabelle] 2 new AFP entries
- Previous by Thread: [isabelle] Termination of function on DAG nodes
- Next by Thread: Re: [isabelle] Termination of function on DAG nodes
- 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