[isabelle] AFP 2012

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)

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.

by Christian Sternagel (submitted 2012-04-13)

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.


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