Numerical analysis of ordinary differential equations in Isabelle/HOL. (English) Zbl 1360.68753

Beringer, Lennart (ed.) et al., Interactive theorem proving. Third international conference, ITP 2012, Princeton, NJ, USA, August 13–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32346-1/pbk). Lecture Notes in Computer Science 7406, 377-392 (2012).
Summary: Many ordinary differential equations (ODEs) do not have a closed solution, therefore approximating them is an important problem in numerical analysis. This work formalizes a method to approximate solutions of ODEs in Isabelle/HOL.
We formalize initial value problems (IVPs) of ODEs and prove the existence of a unique solution, i.e. the Picard-Lindelöf theorem. We introduce generic one-step methods for numerical approximation of the solution and provide an analysis regarding the local and global error of one-step methods.
We give an executable specification of the Euler method as an instance of one-step methods. With user-supplied proofs for bounds of the differential equation we can prove an explicit bound for the global error. We use arbitrary-precision floating-point numbers and also handle rounding errors when we truncate the numbers for efficiency reasons.
For the entire collection see [Zbl 1246.68023].


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
34-04 Software, source code, etc. for problems pertaining to ordinary differential equations
34A12 Initial value problems, existence, uniqueness, continuous dependence and continuation of solutions to ordinary differential equations
Full Text: DOI