Email Gateway (Aug 22 2022 at 13:28): Email Gateway (Aug 22 2022 at 13:28):From: Rupert Swarbrick <rswarbrick@gmail.com>
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
Email Gateway (Aug 22 2022 at 13:28):From: Tobias Nipkow <nipkow@in.tum.de>
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
smime.p7s
Email Gateway (Aug 22 2022 at 13:29):From: Rupert Swarbrick <rswarbrick@gmail.com>
That's brilliant. Thank you very much for the explanation.
Rupert
Tobias Nipkow <nipkow@in.tum.de> writes:
Last updated: Nov 21 2024 at 12:39 UTC