(******************************************************************************)
(* Project: The Isabelle/UTP Proof System *)
(* File: Lens_Laws *)
(* Authors: Simon Foster and Frank Zeyda *)
(* Authors: Burkhart Wolff (slight modifications) *)
(* Emails: simon.foster@york.ac.uk frank.zeyda@york.ac.uk *)
(******************************************************************************)
(* LAST REVIEWED: 7/12/2016 *)
text‹ This file is an except from the "Optics" module of the AFP
🪙‹https://www.isa-afp.org/entries/Optics.html›. ›
section ‹Core Lens Laws›
theory Lens_Laws
imports Main
begin
subsection ‹Lens Signature›
text ‹This theory introduces the signature of lenses and indentifies the core algebraic hierarchy of lens
classes, including laws for well-behaved, very well-behaved, and bijective lenses~\cite{Foster07,Fischer2015,Gibbons17}.›
record ('a, 'b) lens =
lens_get ::
"'b ==> 'a" (
‹get🍋›)
lens_put ::
"'b ==> 'a ==> 'b" (
‹put🍋›)
type_notation
lens (
infixr ‹==>› 0)
text ‹
\begin{figure}
\begin{center}
\includegraphics[width=6cm]{figures/Lens}
\end{center}
\vspace{-5ex}
\caption{Visualisation of a simple lens}
\label{fig:Lens}
\end{figure}
A lens $X : \view \lto \src$, for source type $\src$ and view type $\view$, identifies
$\view$ with a subregion of $\src$~\cite{Foster07,Foster09}, as illustrated in Figure~\ref{fig:Lens}. The arrow denotes
$X$ and the hatched area denotes the subregion $\view$ it characterises. Transformations on
$\view$ can be performed without affecting the parts of $\src$ outside the hatched area. The lens
signature consists of a pair of functions $\lget_X : \src \Rightarrow \view$ that extracts a view
from a source, and $\lput_X : \src \Rightarrow \view \Rightarrow \src$ that updates a view within
a given source. ›
named_theorems lens_defs
text ‹ ‹lens_source› gives the set of constructible sources; that is those that can be built
by putting a value into an arbitrary source. ›
definition lens_source ::
"('a ==> 'b) ==> 'b set" (
‹S🍋›)
where
"lens_source X = {s. ∃ v s'. s = put s' v}"
abbreviation some_source ::
"('a ==> 'b) ==> 'b" (
‹src🍋›)
where
"some_source X ≡ (SOME s. s ∈ S)"
definition lens_create ::
"('a ==> 'b) ==> 'a ==> 'b" (
‹create🍋›)
where
[lens_defs]:
"create v = put (src) v"
text ‹ Function $\lcreate_X~v$ creates an instance of the source type of $X$ by injecting $v$
as the view, and leaving the remaining context arbitrary. ›
subsection ‹Weak Lenses›
text ‹ Weak lenses are the least constrained class of lenses in our algebraic hierarchy. They
simply require that the PutGet law~\cite{Foster09,Fischer2015} is satisfied, meaning that
$\lget$ is the inverse of $\lput$. ›
locale weak_lens =
fixes x ::
"'a ==> 'b" (
structure)
assumes put_get:
"get (put σ v) = v"
begin
lemma source_nonempty:
"∃ s. s ∈ S"
by (auto simp add: lens_source_def)
lemma put_closure:
"put σ v ∈ S"
by (auto simp add: lens_source_def)
lemma create_closure:
"create v ∈ S"
by (simp add: lens_create_def put_closure)
lemma src_source [simp]:
"src ∈ S"
using some_in_eq source_nonempty
by auto
lemma create_get:
"get (create v) = v"
by (simp add: lens_create_def put_get)
lemma create_inj:
"inj create"
by (metis create_get injI)
text ‹ The update function is analogous to the record update function which lifts a function
on a view type to one on the source type. ›
definition update ::
"('a ==> 'a) ==> ('b ==> 'b)" where
[lens_defs]:
"update f σ = put σ (f (get σ))"
lemma get_update:
"get (update f σ) = f (get σ)"
by (simp add: put_get update_def)
lemma view_determination:
assumes "put σ u = put ρ v"
shows "u = v"
by (metis assms put_get)
lemma put_inj:
"inj (put σ)"
by (simp add: injI view_determination)
end
declare weak_lens.put_get [simp]
declare weak_lens.create_get [simp]
subsection ‹Well-behaved Lenses›
text ‹ Well-behaved lenses add to weak lenses that requirement that the GetPut law~\cite{Foster09,Fischer2015}
is satisfied, meaning that $\lput$ is the inverse of $\lget$. ›
locale wb_lens = weak_lens +
assumes get_put:
"put σ (get σ) = σ"
begin
lemma put_twice:
"put (put σ v) v = put σ v"
by (metis get_put put_get)
lemma put_surjectivity:
"∃ ρ v. put ρ v = σ"
using get_put
by blast
lemma source_stability:
"∃ v. put σ v = σ"
using get_put
by auto
lemma source_UNIV [simp]:
"S = UNIV"
by (metis UNIV_eq_I put_closure wb_lens.source_stability wb_lens_axioms)
end
declare wb_lens.get_put [simp]
lemma wb_lens_weak [simp]:
"wb_lens x ==> weak_lens x"
by (simp add: wb_lens_def)
subsection ‹ Mainly Well-behaved Lenses ›
text ‹ Mainly well-behaved lenses extend weak lenses with the PutPut law that shows how one put
override a previous one. ›
locale mwb_lens = weak_lens +
assumes put_put:
"put (put σ v) u = put σ u"
begin
lemma update_comp:
"update f (update g σ) = update (f ∘ g) σ"
by (simp add: put_get put_put update_def)
text ‹ Mainly well-behaved lenses give rise to a weakened version of the $get-put$ law,
where the source must be within the set of constructible sources. ›
lemma weak_get_put:
"σ ∈ S ==> put σ (get σ) = σ"
by (auto simp add: lens_source_def put_get put_put)
lemma weak_source_determination:
assumes "σ ∈ S" "ρ ∈ S" "get σ = get ρ" "put σ v = put ρ v"
shows "σ = ρ"
by (metis assms put_put weak_get_put)
lemma weak_put_eq:
assumes "σ ∈ S" "get σ = k" "put σ u = put ρ v"
shows "put ρ k = σ"
by (metis assms put_put weak_get_put)
text ‹ Provides $s$ is constructible, then @{term get} can be uniquely determined from @{term put} ›
lemma weak_get_via_put:
"s ∈ S ==> get s = (THE v. put s v = s)"
by (rule sym, auto intro!: the_equality weak_get_put, metis put_get)
end
declare mwb_lens.put_put [simp]
declare mwb_lens.weak_get_put [simp]
lemma mwb_lens_weak [simp]:
"mwb_lens x ==> weak_lens x"
by (simp add: mwb_lens.
axioms(
1))
subsection ‹Very Well-behaved Lenses›
text ‹Very well-behaved lenses combine all three laws, as in the literature~\cite{Foster09,Fischer2015}.›
locale vwb_lens = wb_lens + mwb_lens
begin
lemma source_determination:
assumes "get σ = get ρ" "put σ v = put ρ v"
shows "σ = ρ"
by (metis assms get_put put_put)
lemma put_eq:
assumes "get σ = k" "put σ u = put ρ v"
shows "put ρ k = σ"
using assms weak_put_eq[of σ k u ρ v]
by (simp)
text ‹ @{term get} can be uniquely determined from @{term put} ›
lemma get_via_put:
"get s = (THE v. put s v = s)"
by (simp add: weak_get_via_put)
end
lemma vwb_lens_wb [simp]:
"vwb_lens x ==> wb_lens x"
by (simp add: vwb_lens_def)
lemma vwb_lens_mwb [simp]:
"vwb_lens x ==> mwb_lens x"
using vwb_lens_def
by auto
subsection ‹ Ineffectual Lenses ›
text ‹Ineffectual lenses can have no effect on the view type -- application of the $\lput$ function
always yields the same source. They are thus, trivially, very well-behaved lenses.›
locale ief_lens = weak_lens +
assumes put_inef:
"put σ v = σ"
begin
sublocale vwb_lens
proof
fix σ v u
show "put σ (get σ) = σ"
by (simp add: put_inef)
show "put (put σ v) u = put σ u"
by (simp add: put_inef)
qed
lemma ineffectual_const_get:
"∃ v. ∀ σ∈S. get σ = v"
using put_get put_inef
by auto
end
abbreviation "eff_lens X ≡ (weak_lens X ∧ (¬ ief_lens X))"
subsection ‹ Bijective Lenses ›
text ‹Bijective lenses characterise the situation where the source and view type are equivalent:
in other words the view type full characterises the whole source type. It is often useful
when the view type and source type are syntactically different, but nevertheless correspond
precisely in terms of what they observe. Bijective lenses are formulates using
the strong GetPut law~\cite{Foster09,Fischer2015}.›
locale bij_lens = weak_lens +
assumes strong_get_put:
"put σ (get ρ) = ρ"
begin
sublocale vwb_lens
proof
fix σ v u
show "put σ (get σ) = σ"
by (simp add: strong_get_put)
show "put (put σ v) u = put σ u"
by (metis bij_lens.strong_get_put bij_lens_axioms put_get)
qed
lemma put_bij:
"bij_betw (put σ) UNIV UNIV"
by (metis bijI put_inj strong_get_put surj_def)
lemma put_is_create:
"σ ∈ S ==> put σ v = create v"
by (metis create_get strong_get_put)
lemma get_create:
"σ ∈ S ==> create (get σ) = σ"
by (simp add: lens_create_def strong_get_put)
end
declare bij_lens.strong_get_put [simp]
declare bij_lens.get_create [simp]
lemma bij_lens_weak [simp]:
"bij_lens x ==> weak_lens x"
by (simp_all add: bij_lens_def)
lemma bij_lens_vwb [simp]:
"bij_lens x ==> vwb_lens x"
by (metis bij_lens.strong_get_put bij_lens_weak mwb_lens.intro mwb_lens_axioms.intro v
wb_lens_def wb_lens.intro wb_lens_axioms.intro weak_lens.put_get)
subsection ‹Lens Independence›
text ‹
\begin{figure}
\begin{center}
\includegraphics[width=6cm]{figures/Independence}
\end{center}
\vspace{-5ex}
\caption{Lens Independence}
\label{fig:Indep}
\end{figure}
Lens independence shows when two lenses $X$ and $Y$ characterise disjoint regions of the
source type, as illustrated in Figure~\ref{fig:Indep}. We specify this by requiring that the $\lput$
functions of the two lenses commute, and that the $\lget$ function of each lens is unaffected by
application of $\lput$ from the corresponding lens. ›
locale lens_indep =
fixes X :: "'a ==> 'c" and Y :: "'b ==> 'c"
assumes lens_put_comm: "put (put σ v) u = put (put σ u) v"
and lens_put_irr1: "get (put σ v) = get σ"
and lens_put_irr2: "get (put σ u) = get σ"
notation lens_indep (infix ‹⋈› 50)
lemma lens_indepI:
"[ ∧ u v σ. lens_put x (lens_put y σ v) u = lens_put y (lens_put x σ u) v;
∧ v σ. lens_get x (lens_put y σ v) = lens_get x σ;
∧ u σ. lens_get y (lens_put x σ u) = lens_get y σ ] ==> x ⋈ y"
by (simp add: lens_indep_def)
text ‹Lens independence is symmetric.›
lemma lens_indep_sym: "x ⋈ y ==> y ⋈ x"
by (simp add: lens_indep_def)
lemma lens_indep_sym': "(x ⋈ y) = (y ⋈ x)"
by (auto simp: lens_indep_def)
lemma lens_indep_comm:
"x ⋈ y ==> lens_put x (lens_put y σ v) u = lens_put y (lens_put x σ u) v"
by (simp add: lens_indep_def)
lemma lens_indep_get [simp]:
assumes "x ⋈ y"
shows "lens_get x (lens_put y σ v) = lens_get x σ"
using assms lens_indep_def by fastforce
end
