Re: [isabelle] lemma about least fixed point



Just as a small note: Library/Continuity.thy will be
Library/Order_Continuity.thy in the next Isabelle release. Continuity is
often associated with a topology.

 - Johannes


Am Dienstag, den 10.06.2014, 08:00 +1000 schrieb David Cock:
> 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
> >
> 
> 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.