*To*: Alexander Krauss <krauss at in.tum.de>*Subject*: Re: [isabelle] Defining finite list functions recursively*From*: John Matthews <matthews at galois.com>*Date*: Thu, 12 Jun 2008 17:39:30 -0700*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4850D2ED.6010607@in.tum.de>*References*: <61B02660-073D-476B-89A4-57D44646AB2C@galois.com> <4850D2ED.6010607@in.tum.de>

-john On Jun 12, 2008, at 12:40 AM, Alexander Krauss wrote:

Hi John,I'm having problems proving termination of the well-foundedrecursive function xs_strm defined below, and other functions likeit.Good to see that you are driving all available tools to their limitsand beyond, as usual :-) But it might actually work...The problem is that nth_take_cong has the premise about the lengthsbeing equal. In the function definition, a "recursive call" will begenerated by this premise because the instance occuring contains thefunction being defined. But this simplifies away in your manualproof because "length (strm_to_list n f)" does not depend on f.So you need just one more cong rule to tell function about this: lemma length_strm_to_list_cong[fundef_cong]: "n = n' ==> length (strm_to_list n f) = length (strm_to_list n' f')" by simp Then it works. Alex

**References**:**[isabelle] Defining finite list functions recursively***From:*John Matthews

**Re: [isabelle] Defining finite list functions recursively***From:*Alexander Krauss

- Previous by Date: Re: [isabelle] Converting fixed variables to ?-wildcards
- Next by Date: Re: [isabelle] Recursion on finite, lazy lists (llists)
- Previous by Thread: Re: [isabelle] Defining finite list functions recursively
- Next by Thread: [isabelle] Recursion on finite, lazy lists (llists)
- Cl-isabelle-users June 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