Email Gateway (Aug 18 2022 at 19:57): Email Gateway (Aug 18 2022 at 19:57):From: Gerwin Klein <gerwin.klein@nicta.com.au>
The entries in the Archive of Formal proofs are now available for Isabelle2012 at [http://afp.sf.net].
The following new entries are available from the front page:
Ordinary Differential Equations
by Fabian Immler and Johannes Hoelzl (submitted 2012-04-26)
Abstract:
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 general
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 to approximate the solution
of IVPs and 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.
Well-Quasi-Orders
by Christian Sternagel (submitted 2012-04-13)
Abstract:
Based on Isabelle/HOL's type class for preorders, we introduce a type class for
well-quasi-orders (wqo) which is characterized by the absence of "bad" sequences
(our proofs are along the lines of the proof of Nash-Williams, from which we
also borrow terminology). Our two main results are instantiations for the
product type and the list type, which (almost) directly follow from our proofs
of (1) Dickson's Lemma and (2) Higman's Lemma. More concretely:
If the sets A and B are wqo then their Cartesian product is wqo.
If the set A is wqo then the set of finite lists over A is wqo.
Cheers,
Gerwin
Last updated: Nov 21 2024 at 12:39 UTC