*To*: Andrei Popescu <uuomul at yahoo.com>*Subject*: Re: [isabelle] context-sensitive termination proof*From*: Thomas Arthur Leck Sewell <tsewell at cse.unsw.EDU.AU>*Date*: Wed, 28 May 2008 23:06:52 +1000 (EST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <631833.35983.qm@web56115.mail.re3.yahoo.com>*References*: <631833.35983.qm@web56115.mail.re3.yahoo.com>

The function package does build up context information for you.

Yours, Thomas. On Tue, 27 May 2008, Andrei Popescu wrote:

Hello, I am having trouble proving termination of a function whose recursive call argument decreases conditionally, in a context which is essentially the following: typedecl A typedecl B typedecl C consts u :: "A => C => B" v :: "C => A" w :: "C => B" P :: "A => C => bool" size :: "A => nat" axioms conditional_decrease: "P a c ==> size (v c) < size a" function f :: "A => B set" where "f a = {u a c| c. P a c & w c : f (v c)}" The only tool I see available for proving termination of f is the lemma f.termination: "[|wf ?R; !! a x c. (v c, a) : ?R|] ==> ALL x. f_dom x" while I would need something like: f.context_sensitive_termination: "[|wf ?R; !! a x c. P a c ==> (v c, a) : ?R|] ==> ALL x. f_dom x" or rather "[|wf (?R Int {(v c,a)| a c. P a c}); !! a x c. (v c, a) : ?R|] ==> ALL x. f_dom x" Thanks in advance for any hint on how to handle this. Andrei Popescu

**References**:**[isabelle] context-sensitive termination proof***From:*Andrei Popescu

- Previous by Date: [isabelle] context-sensitive termination proof
- Next by Date: Re: [isabelle] context-sensitive termination proof
- Previous by Thread: [isabelle] context-sensitive termination proof
- Next by Thread: Re: [isabelle] context-sensitive termination proof
- Cl-isabelle-users May 2008 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