Re: [isabelle] Are there more general version of lfp/gfp lemmas with "while" combinator?
Reminds me of kleene fp iteration.
This one might help in proving the lemma you have in mind:
âmono ?f; (?f ^^ Suc ?k) bot = (?f ^^ ?k) botâ
â lfp ?f = (?f ^^ ?k) bot
On Mi, 2016-07-27 at 20:06 +0300, Alexander Kogtenkov via
> Dear Isabelle users,
> Theory While_Combinator proves lemmas for least fixed point (e.g. lfp_while) using finite sets (BTW, the dual versions for gfp are missing for some reason). Are there more general versions of the lemmas that use finite lattices instead?
> Alexander Kogtenkov
This archive was generated by a fusion of
Pipermail (Mailman edition) and