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