### Abstract

Lenses provide an abstract interface for manipulating data types
through spatially-separated views. They are defined abstractly in
terms of two functions,

*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.### License

### History

- October 5, 2022
- Added Scene Spaces, which are used to model variable sets algebraically.
Improvements to the alphabet command, including additional theorems.
Additional prisms and associated laws. (revision 771b88d61c21)

- November 15, 2021
- 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)

- January 27, 2021
- 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)

- March 2, 2020
- 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)