### Abstract

Session Ordinary-Differential-Equations formalizes ordinary differential equations (ODEs) and initial value problems. This work comprises proofs for local and global existence of unique solutions (Picard-Lindelöf theorem). Moreover, it contains a formalization of the (continuous or even differentiable) dependency of the flow on initial conditions as the flow of ODEs.

Not in the generated document are the following sessions:

- HOL-ODE-Numerics: Rigorous numerical algorithms for computing enclosures of solutions based on Runge-Kutta methods and affine arithmetic. Reachability analysis with splitting and reduction at hyperplanes.
- HOL-ODE-Examples: Applications of the numerical algorithms to concrete systems of ODEs.
- Lorenz_C0, Lorenz_C1: Verified algorithms for checking C1-information according to Tucker's proof, computation of C0-information.

### License

BSD License

### History

September 20, 2017
  added Poincare map and propagation of variational equation in reachability analysis, verified algorithms for C1-information and computations for C0-information of the Lorenz attractor.
August 3, 2016
  numerical algorithms for reachability analysis (using second-order Runge-Kutta methods, splitting, and reduction) implemented using Lammich's framework for automatic refinement
April 14, 2016
  added flow and variational equation
February 13, 2014
  added an implementation of the Euler method based on affine arithmetic

### Topics

- Mathematics/Analysis

### Session Ordinary_Differential_Equations

- ODE_Auxiliarities
- MVT_Ex
- Vector_Derivative_On
- Interval_Integral_HK
- Gronwall
- Initial_Value_Problem
- Picard_Lindeloef_Qualitative
- Bounded_Linear_Operator
- Multivariate_Taylor
- Flow
- Upper_Lower_Solution
- Poincare_Map
- Reachability_Analysis
- Flow_Congs
- Cones
- Linear_ODE
- ODE_Analysis

### Session HOL-ODE-Numerics

- GenCF_No_Comp
- Refine_Dflt_No_Comp
- Autoref_Misc
- Weak_Set
- Enclosure_Operations
- Refine_Vector_List
- Transfer_Analysis
- Transfer_ODE
- Transfer_Euclidean_Space_Vector
- Refine_Hyperplane
- Refine_Unions
- Refine_Intersection
- Refine_Invar
- Refine_Interval
- Refine_Info
- Abstract_Rigorous_Numerics
- Refine_Rigorous_Numerics
- Refine_Rigorous_Numerics_Aform
- Concrete_Rigorous_Numerics
- Refine_String
- Refine_Folds
- One_Step_Method
- Runge_Kutta
- Abstract_Reachability_Analysis
- Concrete_Reachability_Analysis
- Refine_Parallel
- Refine_Default
- Refine_Phantom
- Refine_ScaleR2
- Abstract_Reachability_Analysis_C1
- Concrete_Reachability_Analysis_C1
- Refine_Reachability_Analysis
- Refine_Reachability_Analysis_C1
- Init_ODE_Solver
- Example_Utilities
- ODE_Numerics

### Session Lorenz_Approximation

- Result_Elements
- Result_File_Coarse
- Lorenz_Approximation

### Session HOL-ODE-Examples

- Examples_Integral
- Examples_One_Step_Method
- Examples_Poincare_Map
- ODE_Examples

### Session HOL-ODE-ARCH-COMP

- Examples_ARCH_COMP

### Session Lorenz_C0

- Lorenz_C0

### Session Lorenz_C1

- Lorenz_C1

### Depends on

- Affine Arithmetic
- List Index
- Basic Geometric Properties of Triangles
- Collections Framework
- Deriving class instances for datatypes
- Haskell’s Show Class in Isabelle/HOL

### Used by

- The Poincaré-Bendixson Theorem
- Verification Components for Hybrid Systems
- Differential Dynamic Logic

### Auto-related entries

- Matrices for ODEs
- The Poincaré-Bendixson Theorem

## Cite

×

Ordinary_Differential_Equations-AFP

    @article{Ordinary_Differential_Equations-AFP,
      author  = {Fabian Immler and Johannes Hölzl},
      title   = {Ordinary Differential Equations},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2012},
      note    = {\url{https://isa-afp.org/entries/Ordinary_Differential_Equations.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012