# [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)"
instance ..
end

`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"
where
"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:
lemma setsum_estimation'[termination_simp]:
"(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
``termination.
`

`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
``better avoided.
`

`Are there ideas for a better size function or a better setup for termination_simp? Has
``anyone else run into this problem before?
`
Best,
Andreas

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