*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Proving termination of a recursive function*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Wed, 18 Nov 2015 13:29:51 +0100*In-reply-to*: <CAOOzCW41xr-RVGEK6w8GEH-o+31-7uWvMEnJ=xqJp8LjVioDiQ@mail.gmail.com>*References*: <CAOOzCW41xr-RVGEK6w8GEH-o+31-7uWvMEnJ=xqJp8LjVioDiQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

int-e's answer was: termination proof - let ?R = "{(y,POR runnable todo don) | runnable todo don y s. s â range don â y â set_option s }" { fix P x assume *: "âx. (ây. (y, x) â ?R â P y) â P x" have "P x" by (induct x rule: POR.induct) (auto intro: *) } then have "wf ?R" by (auto simp: wf_def) then show ?thesis by (relation ?R) (auto simp: ran_def image_def, metis) qed It's really stupid because it's a bona fide inductive definition on the data type definition; morally it *is* primitive recursive. but the underlying well-founded relation on POR is not readily available; that's what I'm defining as ?R in the proof (or so I believe, I'd be happy to be shown wrong) My answer was:

int-e is correct, this is a primitively-recursive function, so the easiest way to define it is to define it as one. The problem is that "primrec" is apparently not smart enough to figure out that your definition is primitively-recursive I just did it by hand and proved the "simp" rule separately afterwards Two more remarks: 1. your datatype is essentially an infinitely-branching tree, which means you can have potentially unbounded traversal paths in it, so there simply is no sensible "size" function for them, which makes proving termination more painful (although in this case, it can be done with relatively little effort, as shown by int-e) 2. your function implicitly enforces the domain of "done" to be finite, so you could actually define a "size" function for this case, and it would be something "size (POR _ _ done) = 1 + Max (size ` ran done)". But you'd also have to add conj_cong as a fundef_cong rule or rewrite your definition with if _ then _ else in order to be able to use the fact that "done" has finite domain On 17/11/15 20:52, Michael Walker wrote:

Hi, I've been getting into Isabelle recently, and I have a problem with function termination: I have a recursive data type, and a function checking some property of it, but I'm not sure how to approach the termination proof: ~~~~ theory MinimalExample imports Main "~~/src/HOL/Library/FSet" Map begin datatype ThreadId = UserThread nat datatype POR = POR "ThreadId fset" "ThreadId fset" "ThreadId â POR" function por_well_formed :: "POR â bool" where "por_well_formed por â (case por of (POR runnable todo done) â ( todo |â| runnable â dom done â fset runnable â fset todo â dom done = {}) â (â p â ran done. por_well_formed p))" by auto termination sorry end ~~~~ My informal termination argument goes like this: because POR is data, not codata, there can't be an infinite sequence POR1 -> POR2 -> POR3 -> ... (following the links in the map). This means that the recursive case in por_well_formed will terminate. However, I'm not sure how to formalise that. Any suggestions for this in particular, or termination proofs in general, would be greatly appreciated.

**Follow-Ups**:**Re: [isabelle] Proving termination of a recursive function***From:*Dmitriy Traytel

**References**:**[isabelle] Proving termination of a recursive function***From:*Michael Walker

- Previous by Date: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Next by Date: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Previous by Thread: [isabelle] Proving termination of a recursive function
- Next by Thread: Re: [isabelle] Proving termination of a recursive function
- Cl-isabelle-users November 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