*To*: Tjark Weber <webertj at in.tum.de>*Subject*: Re: [isabelle] Termination of Recursive Function with Set Comprehension*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 7 Feb 2013 12:26:12 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <1360235312.1972.28.camel@weber>*References*: <1360235312.1972.28.camel@weber>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130106 Thunderbird/17.0.2

Hi Tjark, you are missing a congruence rule for setsum such as the following: declare setsum_cong[fundef_cong]

Hope this helps, Andreas On 02/07/2013 12:08 PM, Tjark Weber wrote:

Hi, Consider this (simplified) example of a recursive function whose definition involves set comprehension: function (sequential) f :: "nat ⇒ nat" where "f 0 = 1" | "f n = ∑{f k | k. k < n}" by pat_completeness auto How to prove termination? In particular, termination f apply (relation "measure id") results in an unprovable goal. Best regards, Tjark

**References**:**[isabelle] Termination of Recursive Function with Set Comprehension***From:*Tjark Weber

- Previous by Date: Re: [isabelle] Termination of Recursive Function with Set Comprehension
- Next by Date: Re: [isabelle] Termination of Recursive Function with Set Comprehension
- Previous by Thread: Re: [isabelle] Termination of Recursive Function with Set Comprehension
- Next by Thread: [isabelle] Isabelle2013-RC3 available for testing
- Cl-isabelle-users February 2013 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