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:
 Nat.lfp_Kleene_iter: 
	âmono ?f; (?f ^^ Suc ?k) bot = (?f ^^ ?k) botâ 
	â lfp ?f = (?f ^^ ?k) bot

--
  Peter

On Mi, 2016-07-27 at 20:06 +0300, Alexander Kogtenkov via
Cl-isabelle-users wrote:
>  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?
> 
> Regards,
> Alexander Kogtenkov






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