*To*: Jason Dagit <dagitj at gmail.com>*Subject*: Re: [isabelle] Termination Proof*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sun, 19 Dec 2010 11:31:06 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <AANLkTi=kF1jUQCTKzKS0qUJ-eSLQRqr=_bPoJ7hQ_f_r@mail.gmail.com>*References*: <AANLkTi=kF1jUQCTKzKS0qUJ-eSLQRqr=_bPoJ7hQ_f_r@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.24 (Macintosh/20100228)

Jason Dagit schrieb: > Hello, > > I was trying to prove termination for the following definition: > \begin{code} > theory Termination > imports Nat Multiset Divides Datatype Just a small remark: Nat, Divides and Datatype are subtheories of Main and should not be imported selectively, they may not work as expect in the absence of the rest of Main. In your case it was not a problem because Multiset includes Main. I'll let Alex answer your actual question. Tobias > begin > > inductive_set even :: "nat set" where > zero[intro!]: "0 ∈ even" | > step[intro!]: "n ∈ even ⟹ (Suc (Suc n)) ∈ even" > > function (sequential) foo :: "nat ⇒ nat list" where > "foo 0 = [0]" | > "foo (Suc 0) = [1]" | > "foo n = (case n ∈ even of > True ⇒ n # foo (n div 2) | > False ⇒ n # foo (Suc n))" > by pat_completeness auto > termination > apply (relation "measures [Suc, λn. n div 2]") > apply auto > oops > \end{code} > > I know I can change the definition slightly for foo to make it pass the > termination checker using the standard lexicographical measure. I'm > learning about function package and specifically, how to write termination > proofs so I want to avoid the easy route here. I'm following this > documentation in particular: > http://isabelle.in.tum.de/doc/functions.pdf > > My understanding of the above proof attempt is that it will never work > because the well founded relation needs for the "n \<notin> even" case to > decrease or stay the same, but instead it gets larger in the recursive call. > > I can also imagine a proof of termination based on the fact that if n is odd > then Suc n will be even and the next call to foo will cause the argument to > shrink by more than it grew. Is it possible to write such a proof and lease > the termination checker? Perhaps there is something that can be done with > the function domain in the same way partial functions are handled? Advice > on how to get started with such a proof? Perhaps there are examples of this > somewhere already? > > Thanks, > Jason

**References**:**[isabelle] Termination Proof***From:*Jason Dagit

- Previous by Date: [isabelle] Termination Proof
- Next by Date: Re: [isabelle] Termination Proof
- Previous by Thread: [isabelle] Termination Proof
- Next by Thread: Re: [isabelle] Termination Proof
- Cl-isabelle-users December 2010 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