Re: [isabelle] Call for real limit problems
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)))".
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