Email Gateway (Mar 17 2025 at 23:24): Email Gateway (Mar 17 2025 at 23:24):From: Gerwin Klein <cl-isabelle-users@lists.cam.ac.uk>
Following the Isabelle release, the AFP is now available for Isabelle2025 from https://isa-afp.org <https://isa-afp.org/>
There are now more than 4.66 million lines of Isabelle proof in 892 entries by 527 authors.
Two new entries have become available from the home page that were previously only available in the development version:
First Order Clause
by Balazs Toth
This entry provides reusable theories that lift properties of first-order (ground and nonground) terms to atoms, literals, and clauses. These properties include substitutions, orders, entailment, and typing. The sessions AFP/First_Order_Terms and AFP/Abstract_Substitution are the basis of this entry.
https://www.isa-afp.org/entries/First_Order_Clause.html
and
Elementary Graph Traversal Algorithms
by Mohammad Abdulaziz
In this entry, we verify the correctness of: Depth-first search and Breadth-first search The entry's main aim is pedagogical. It has the formal material presented in one chapter of the book Functional Data Structures and Algorithms: A Proof Assistant Approach. The verification is based on a simple set-based representation of directed graphs. The main feature is that a graph's set of vertices is implicitly represented by its edges. The main focus of the development is to develop a representation suitable for mathematical reasoning and for executable algorithms. The entry also shows the verification of executable algorithms that need background mathematical libraries with basic Isabelle tools. Two main features are its automation setup aimed at verifying executable graph algorithms in a human-readable way and to verify the algorithms w.r.t. the same graph representation, making all of them compatible. The setup we use here includes using the function package to model loops and reason about their termination, using records to model program states, and using locales to implement parametric as well as step-wise refinement based verification. The material presented here is a part of an ongoing development of formal results on graphs and graph algorithms in Isabelle/HOL: https://github.com/mabdula/Isabelle-Graph-Library.
https://www.isa-afp.org/entries/Graph_Algorithms.html
Enjoy!
Gerwin
Last updated: Apr 17 2025 at 20:22 UTC