*To*: Manuel Eberl <eberlm at in.tum.de>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Setup termination prover for finitely branching tree recursion*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 7 Dec 2015 11:05:17 +0100*In-reply-to*: <56654E0C.30508@in.tum.de>*References*: <56653E70.7030507@inf.ethz.ch> <56654E0C.30508@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

Hi Manuel,

"[| y <= f (g x); f (g x) <= (âxâA. f (g x)) |] ==> y <= (âxâA. f (g x))"

datatype (plugins del: size) 'a tree2 = Leaf2 | Node2 'a "char â 'a tree2 Ã 'a" instantiation tree2 :: (type) size begin primrec size_tree2 :: "'a tree2 â nat" where "size_tree2 Leaf2 = 0" | "size_tree2 (Node2 x ts) = Suc (setsum (Suc â fst â (map_prod size_tree2 id â ts)) UNIV)" instance .. end fun zip_prod where "zip_prod f g (x, y) (u, v) = (f x u, g y v)" fun zip_tree2 :: "'a tree2 â 'b tree2 â ('a Ã 'b) tree2" where "zip_tree2 (Node2 x ts) (Node2 y ts') = Node2 (x, y) (Îz. zip_prod zip_tree2 Pair (ts z) (ts' z))" | "zip_tree2 _ _ = Leaf2"

Best, Andreas On 07/12/15 10:14, Manuel Eberl wrote:

No idea about why what you are doing does not work, but the following does work: lemma le_setsum_nat [termination_simp]: assumes "finite A" "x â A" shows "f (g x) â (âxâA. f (g x) :: nat)" proof - have "f (g x) = (âxâ{x}. f (g x))" by simp also from assms have "â â (âxâA. f (g x))" by (intro setsum_mono2) auto finally show ?thesis by simp qed Note that it doesn't work if you replace "f (g x)" with just "f x". Unification problem, perhaps? Cheers, Manuel On 07/12/15 09:08, Andreas Lochbihler wrote: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

**References**:**[isabelle] Setup termination prover for finitely branching tree recursion***From:*Andreas Lochbihler

**Re: [isabelle] Setup termination prover for finitely branching tree recursion***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Setup termination prover for finitely branching tree recursion
- Next by Date: Re: [isabelle] Failing afp-2015 build
- Previous by Thread: Re: [isabelle] Setup termination prover for finitely branching tree recursion
- Next by Thread: Re: [isabelle] Failing afp-2015 build
- Cl-isabelle-users December 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list