[isabelle] Setup termination prover for finitely branching tree recursion
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Setup termination prover for finitely branching tree recursion
- From: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
- Date: Mon, 7 Dec 2015 09:08:16 +0100
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0
Dear experts of the simplifier and/or the function package,
For a datatype of finitely branching trees, I would like to setup the terminiation prover
of the function package such that it can automatically prove termination of my recursive
functions. My problem is that I cannot mimick the setup for other datatypes like lists and
I am running out of ideas how this can be fit into lexicographic order.
Here is my usecase and the analysis of the problem. The datatype tree recurses through the
function type, but the domain of the functions is finite. Thus, it is possible to define a
size function, although this must be done manually in Isabelle2015 (using setsum for
summing the sizes of the subtrees).
datatype (plugins del: size) 'a tree = Leaf | Node 'a "char â 'a tree"
instantiation tree :: (type) size begin
primrec size_tree :: "'a tree â nat" where
"size_tree Leaf = 0"
| "size_tree (Node x ts) = Suc (setsum (size_tree â ts) UNIV)"
Now, I would like lexicographic_order to prove termination of a function definition such
as the following:
fun zip_tree :: "'a tree â 'b tree â ('a Ã 'b) tree"
"zip_tree (Node x ts) (Node y ts') = Node (x, y) (Îz. zip_tree (ts z) (ts' z))"
| "zip_tree _ _ = Leaf"
Without further setup, the termination proof fails because the proof tactic cannot solve
goals such as the following.
1. âts' xa. size (ts' xa) < Suc (âxâUNIV. size (ts' x))
For recursion through lists, there is a custom setup, namely the theorems
size_list_estimation and size_list_estimation' which are declared as [termination_simp].
thm size_list_estimation' â?x â set ?xs; ?y â ?f ?xâ â ?y â size_list ?f ?xs
Now I tried to mimick this setup for the setsum operator:
"(y :: nat) â f x â finite (UNIV :: 'a set) â y â setsum f (UNIV :: 'a set)"
From what I could see from the code, these *_estimation rules work as follows:
* lexicographic_order internally uses the proof method (auto simp add: termination_simp)
to solve the goals, that is, the termination proof are solved mostly by conditional rewriting.
* In particular, termination_simp contains the rule ?m â ?n â ?m < Suc ?n, so the above
subgoal 1. can be solved if the simplifier can prove "size (ts' xa) <= (âxâUNIV. size (ts'
x))". And this is where *_estimation' triggers.
Unfortunately, the simplifier does not like setsum_estimation' as much as it likes
size_list_estimation'. Both rules contain the free variable ?x in the assumptions that is
not bound by the conclusion, so trouble is to be expected.
In the case of size_list_estimation', the first premise `?x : set ?xs` instantiates the ?x
because the termination goal typically contains an assumption `x : set xs` due to a
congrence rule (and the simplifier calls the HOL unsafe solver, which instantiates the
variable as a matching assumption is available). Thus, the second assumption `?y <= ?f ?x`
no longer contains schematic variables and the simplifier can usually discharge the goal.
In case of setsum_estimation', there is no such first premise that could instantiate ?x
(because the corresponding assumption would be "?x : UNIV" which holds trivially). Thus,
the recursive invocation of the simplifier is left with a goal such as
"!!x. f x <= f (?x x)"
Simplification fails (because there is no suitable solver) and thus it cannot prove
If I add a solver to the simpset which applies the rule "order_refl", then the termination
proof succeeds. Yet, my feeling says that such a solver is not a good idea in general,
because it will instantiate variables too aggressively. So this looks like a hack that is
Are there ideas for a better size function or a better setup for termination_simp? Has
anyone else run into this problem before?
This archive was generated by a fusion of
Pipermail (Mailman edition) and