Re: [isabelle] Termination of function on DAG nodes



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



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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