[isabelle] lemma about least fixed point



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.