Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Z Mathematical Toolkit in Isab...


view this post on Zulip Email Gateway (Oct 17 2025 at 11:45):

From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce this new contribution, by Simon Foster, Pedro Ribeiro, Frank Zeyda and Jim Woodcock.

Abstract
The objective of this theory development is an implementation of the Z mathematical toolkit in Isabelle/HOL that is both efficient for proof and faithful to the standard. We construct the Z metalanguage and type universe on top of HOL, and link this to corresponding concrete types (finite functions, lists etc.) in Isabelle, to enable efficient proof automation. We then utilise coercive subtyping and overloading to support processing of Z-like expressions in Isabelle/HOL. We then use this to develop the mathematical toolkit for sets, relations, functions, and sequences.

https://www.isa-afp.org//entries/Z_Toolkit.html

Larry


Last updated: Oct 20 2025 at 16:27 UTC