Consider the following silly Isabelle definition of trees and subtrees:
datatype tree = Leaf int
| Node tree tree
fun children :: "tree ⇒ tree set" where
"children (Leaf _) = {}" |
"children (Node a b) = {a, b}"
lemma children_decreasing_size:
assumes "c ∈ children t"
shows "size c < size t"
using assms
by (induction t, auto)
function subtrees :: "tree ⇒ tree set" where
"subtrees t = { s | c s. c ∈ children t ∧ s ∈ subtrees c }"
by auto
termination
apply (relation "measure size", simp)
The termination proof of subtrees gets stuck at this point although the recursive calls are only ever made on children, which are strictly smaller by the well-founded size relation (as the trivial lemma shows).
The proof state is as follows:
goal (1 subgoal):
1. ⋀t x xa xb. (xa, t) ∈ measure size
This is impossible to prove, of course, since the information that xa is a child of t is lost. Did I do something wrong? Is there anything I can do to save the proof? I note that I can formulate the same definition using lists instead of sets:
fun children_list :: "tree ⇒ tree list" where
"children_list (Leaf _) = []" |
"children_list (Node a b) = [a, b]"
function subtrees_list :: "tree ⇒ tree list" where
"subtrees_list t = concat (map subtrees_list (children_list t))"
by auto
termination
apply (relation "measure size", simp)
and get a more informative, provable termination goal:
goal (1 subgoal):
1. ⋀t x.
x ∈ set (children_list t) ⟹
(x, t) ∈ measure size
Is this some limitation in Isabelle that I should just work around by not using sets for this?
The restriction to c : children t in the set comprehension for subtrees does not show up in the termination proof obligation, because the function package does not know anything a priori about &. Congruence rules can be used to achieve this. In this case, you can locally declare conj_cong as [fundef_cong] to essentially emulate a left-to-right evaluation order (although there is no such thing as evaluation in HOL). For example,
context notes conj_cong[fundef_cong] begin
fun subtrees :: ...
termination ...
end
The context block ensures that the declaration conj_cong[fundef_cong] is only in effect for this function definition.
The version with lists works because it uses the function map for which there is a congruence rule in place by default. The same should have worked for sets, if you had used the monadic bind operation on sets (rather than a set comprehension).