*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] lemma about least fixed point*From*: David Cock <davec at cse.unsw.edu.au>*Date*: Tue, 10 Jun 2014 08:00:52 +1000*In-reply-to*: <CAAMXsibgA2EPFWxnSU03bAwD_cPKdXy3hR2s+e4siZ9y1eGcMQ@mail.gmail.com>*References*: <00F65626-4573-486D-AC0E-811D48167ABE@cantab.net> <CAAMXsibgA2EPFWxnSU03bAwD_cPKdXy3hR2s+e4siZ9y1eGcMQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Icedove/24.5.0

John, The lemma you want is continuous_lfp in Library/Continuity.thy. Dave On 10/06/14 02:23, Brian Huffman wrote:

This theorem needs a stronger assumption, namely that the function f be *continuous*, i.e. it preserves least upper bounds (at the very least, it must preserve lubs of countable chains). On a general complete lattice, a monotone function may need to be iterated transfinitely many times before a fixed point is reached. - Brian On Mon, Jun 9, 2014 at 9:03 AM, John Wickerson <johnwickerson at cantab.net> wrote:Dear all, I'd like to use the following in my proof: lemma johns_lemma: "mono f ⟹ lfp f = (⋃k. (f ^^ k) {})" I *think* it's a pretty bog-standard theorem about least fixed points over complete lattices. But I can't find it in the library or the AFP. Does anybody know how I can obtain it? Best wishes, John

**Follow-Ups**:**Re: [isabelle] lemma about least fixed point***From:*Johannes Hölzl

**References**:**[isabelle] lemma about least fixed point***From:*John Wickerson

**Re: [isabelle] lemma about least fixed point***From:*Brian Huffman

- Previous by Date: Re: [isabelle] lemma about least fixed point
- Next by Date: [isabelle] ACM SAC 2015: Software Verification and Testing Track - First CfP
- Previous by Thread: Re: [isabelle] lemma about least fixed point
- Next by Thread: Re: [isabelle] lemma about least fixed point
- Cl-isabelle-users June 2014 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