Re: [isabelle] lemma about least fixed point



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.