[isabelle] Setup termination prover for finitely branching tree recursion

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 ..

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:

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?


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