*To*: uuomul at yahoo.com*Subject*: Re: [isabelle] context-sensitive termination proof*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Wed, 28 May 2008 15:51:08 +0200*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>*User-agent*: Icedove 1.5.0.14eol (X11/20080509)

Andrei,

I am having trouble proving termination of a function whose recursive call argument decreases conditionally, in a context which is essentially the following:

[...]

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"

Hope this helps Alex

theory Scratch imports Main begin 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" declare conj_cong[fundef_cong] function f :: "A => B set" where "f a = {u a c| c. P a c \<and> w c : f (v c)}" by auto termination by (relation "measure size") (auto simp: conditional_decrease)

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

- Previous by Date: Re: [isabelle] context-sensitive termination proof
- Next by Date: [isabelle] Herlihy, Milner, Hoare, O'Hearn etc.: LASER summer school
- Previous by Thread: Re: [isabelle] context-sensitive termination proof
- Next by Thread: [isabelle] Herlihy, Milner, Hoare, O'Hearn etc.: LASER summer school
- 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