Re: [isabelle] lemma about least fixed point



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.