Re: [isabelle] Call for real limit problems

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.


On 23/12/16 08:20, Manuel Eberl wrote:

I'm currently working on some more automation for real limits. For that
purpose, I'd like to collect some âreal-world problemsâ from Isabelle users.

I am looking for problems involving the limit of functions of type "real
â real" built from arithmetic (+-*/^), powr, sqrt, root, ln, exp, abs,
min, max as well as sin, cos, tan at finite points. Real parameters
(i.e. free variables of type "real") are also allowed.



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