Re: [isabelle] Call for real limit problems



Fair enough.

David


On 23/12/16 10:20, Manuel Eberl wrote:
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.