Email Gateway (Aug 22 2022 at 18:52): Email Gateway (Aug 22 2022 at 18:52):From: Gerwin.Klein@data61.csiro.au
As set of 3 connected new AFP entries by Georg Struth:
Properties of Orderings and Lattices
https://www.isa-afp.org/entries/Order_Lattice_Props.html
These components add further fundamental order and lattice-theoretic concepts and properties to Isabelle's libraries. They follow by and large the introductory sections of the Compendium of Continuous Lattices, covering directed and filtered sets, down-closed and up-closed sets, ideals and filters, Galois connections, closure and co-closure operators. Some emphasis is on duality and morphisms between structures, as in the Compendium. To this end, three ad-hoc approaches to duality are compared.
Quantales
https://www.isa-afp.org/entries/Quantales.html
These mathematical components formalise basic properties of quantales, together with some important models, constructions, and concepts, including quantic nuclei and conuclei.
Transformer Semantics
https://www.isa-afp.org/entries/Transformer_Semantics.html
These mathematical components formalise predicate transformer semantics for programs, yet currently only for partial correctness and in the absence of faults. A first part for isotone (or monotone), Sup-preserving and Inf-preserving transformers follows Back and von Wright's approach, with additional emphasis on the quantalic structure of algebras of transformers. The second part develops Sup-preserving and Inf-preserving predicate transformers from the powerset monad, via its Kleisli category and Eilenberg-Moore algebras, with emphasis on adjunctions and dualities, as well as isomorphisms between relations, state transformers and predicate transformers.
Enjoy!
Gerwin
Last updated: Apr 19 2024 at 20:15 UTC