### Abstract

*get*, the return a value from the source type, and

*put*that updates the value. We mechanise the underlying theory of lenses, in terms of an algebraic hierarchy of lenses, including well-behaved and very well-behaved lenses, each lens class being characterised by a set of lens laws. We also mechanise a lens algebra in Isabelle that enables their composition and comparison, so as to allow construction of complex lenses. This is accompanied by a large library of algebraic laws. Moreover we also show how the lens classes can be applied by instantiating them with a number of Isabelle data types.

### Change history

[2020-03-02]
Added partial bijective and symmetric lenses.
Improved alphabet command generating additional lenses and results.
Several additional lens relations, including observational equivalence.
Additional theorems throughout.
Adaptations for Isabelle 2020.
(revision 44e2e5c)

[2021-01-27]
Addition of new theorems throughout, particularly for prisms.
New "chantype" command allows the definition of an algebraic datatype with generated prisms.
New "dataspace" command allows the definition of a local-based state space, including lenses and prisms.
Addition of various examples for the above.
(revision 89cf045a)

[2021-11-15]
Improvement of alphabet and chantype commands to support code generation.
Addition of a tactic "rename_alpha_vars" that removes the subscript vs in proof goals.
Bug fixes and improvements to alphabet command ML implementation.
Additional laws for scenes.
(revisions 9f8bcd71c121 and c061bf9f46f3)