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)))".
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and