[isabelle] announcing AFP 2016-1
The Archive of Formal Proofs is now available for Isabelle2016-1 from http://isa-afp.org
As always, previous releases for previous Isabelle versions remain available, and there is a whole host of (ten) new entries available from the front page.
Our new statistics page is now also available for the release version. You can watch the archive growing and prospering at https://www.isa-afp.org/statistics.shtml
Abstract Interpretation of Annotated Commands
by Tobias Nipkow
This is the Isabelle formalization of the material decribed in the eponymous ITP 2012 paper. It develops a generic abstract interpreter for a while-language, including widening and narrowing. The collecting semantics and the abstract interpreter operate on annotated commands: the program is represented as a syntax tree with the semantic information directly embedded, without auxiliary labels. The aim of the formalization is simplicity, not efficiency or precision. This is motivated by the inclusion of the material in a theorem prover based course on semantics. A similar (but more polished) development is covered in the book Concrete Semantics.
The Factorization Algorithm of Berlekamp and Zassenhaus
by Jose DivasÃn, Sebastiaan Joosten, RenÃ Thiemann, and Akihisa Yamada
We formalize the Berlekamp-Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yunâs square-free factorization algorithm to integer polynomials, and thus provide an efficient and certified factorization algorithm for arbitrary univariate polynomials.
The algorithm first performs a factorization in the prime field GF(p) and then performs computations in the integer ring modulo p^k, where both p and k are determined at runtime. Since a natural modeling of these structures via dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using Isabelleâs recent addition of local type definitions.
Through experiments we verify that our algorithm factors polynomials of degree 100 within seconds.
by Manuel Eberl
In this work, we define the Catalan numbers Cn and prove several equivalent definitions (including some closed-form formulae). We also show one of their applications (counting the number of binary trees of size n), prove the asymptotic growth approximation Cn â 4n / (âÏ Â n1.5), and provide reasonably efficient executable code to compute them.
The derivation of the closed-form formulae uses algebraic manipulations of the ordinary generating function of the Catalan numbers, and the asymptotic approximation is then done using generalised binomial coefficients and the Gamma function. Thanks to these highly non-elementary mathematical tools, the proofs are very short and simple.
by Manuel Eberl
This work defines and proves the correctness of the FisherâYates algorithm for shuffling â i.e. producing a random permutation â of a list. The algorithm proceeds by traversing the list and in each step swapping the current element with a random element from the remaining list.
Formalization of KnuthâBendix Orders for Lambda-Free Higher-Order Terms
by Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand
This Isabelle/HOL formalization defines KnuthâBendix orders for higher-order terms without lambda-abstraction and proves many useful properties about them. The main order fully coincides with the standard transfinite KBO with subterm coefficients on first-order terms. It appears promising as the basis of a higher-order superposition calculus.
Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms
by Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand
This Isabelle/HOL formalization defines recursive path orders (RPOs) for higher-order terms without lambda-abstraction and proves many useful properties about them. The main order fully coincides with the standard RPO on first-order terms also in the presence of currying, distinguishing it from previous work. An optimized variant is formalized as well. It appears promising as the basis of a higher-order superposition calculus.
by Sebastien Gouezel
Lp is the space of functions whose p-th power is integrable. It is one of the most fundamental Banach spaces that is used in analysis and probability. We develop a framework for function spaces, and then implement the Lp spaces in this framework using the existing integration theory in Isabelle/HOL. Our development contains most fundamental properties of Lp spaces, notably the HÃlder and Minkowski inequalities, completeness of Lp, duality, stability under almost sure convergence, multiplication of functions in Lp and Lq, stability under conditional expectation.
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals
by Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel
This Isabelle/HOL formalization introduces a nested multiset datatype and defines Dershowitz and Manna's nested multiset order. The order is proved well founded and linear. By removing one constructor, we transform the nested multisets into hereditary multisets. These are isomorphic to the syntactic ordinalsâthe ordinals can be recursively expressed in Cantor normal form. Addition, subtraction, multiplication, and linear orders are provided on this type.
by Hauke Brinkop and Tobias Nipkow
This library defines three different versions of pairing heaps: a functional version of the original design based on binary trees [Fredman et al. 1986], the version by Okasaki  and a modified version of the latter that is free of structural invariants.
The amortized complexity of pairing heaps is analyzed in the AFP article Amortized Complexity.
by Manuel Eberl
This work contains a proof of Stirling's formula both for the factorial n! â â2Ïn (n/e)n on natural numbers and the real Gamma function Î(x) â â2Ï/x (x/e)x. The proof is based on work by Graham Jameson.
This archive was generated by a fusion of
Pipermail (Mailman edition) and