Re: [isabelle] Call for real limit problems



I'm afraid these examples are too abstract. I can only work with
concrete functions, i.e. "the limit of Îx::real. max x (exp x) / ln (min
(exp (-x)) (exp (-exp x)))".

Manuel


On 23/12/16 10:07, David Cock wrote:
> The pGCL formalisation in the AFP relies on limits in showing the
> continuity of expectation transformers.  The transformers are built from
> linear combinations (*,+), infimum and least fixed point.  The
> non-recursive cases are in thys/pGCL/Continuity.thy, and the recursive
> case (that a loop is equivalent to the limit of its iterates) is in
> thys/pGCL/LoopInduction.thy.  The proofs are long, but there's nothing
> especially funky in there - it's mostly just dancing around not having
> the extended reals.
> 
> David




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