[isabelle] Termination of function on DAG nodes



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.