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.
License
Topics
Related publications
- Foster, S., Baxter, J., Cavalcanti, A., Woodcock, J., & Zeyda, F. (2020). Unifying semantic foundations for automated verification tools in Isabelle/UTP. Science of Computer Programming, 197, 102510. https://doi.org/10.1016/j.scico.2020.102510
- Foster, S., Hur, C.-K., & Woodcock, J. (2025). Unifying Model Execution and Deductive Verification with Interaction Trees in Isabelle/HOL. ACM Transactions on Software Engineering and Methodology, 34(4), 1–40. https://doi.org/10.1145/3702981
Session Z_Toolkit
- Z_Toolkit_Overview
- List_Extra
- Infinite_Sequence
- Countable_Set_Extra
- Infinity
- Positive
- Haskell_Show
- Enum_Type
- Record_Default_Instance
- Def_Const
- Overriding
- Relation_Extra
- Map_Extra
- Partial_Fun
- Partial_Inj
- Finite_Fun
- Finite_Inj
- Total_Fun
- Bounded_List
- Tabulate_Command
- Relation_Lib
- Set_Toolkit
- Relation_Toolkit
- Function_Toolkit
- Number_Toolkit
- Sequence_Toolkit
- Z_Toolkit_Pretty
- Partial_Function_Command
- Z_Toolkit