Theory Lenses_And_Other_Optics.Lens

(* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
   SPDX-License-Identifier: MIT *)

(*<*)
theory Lens
  imports Prism
begin
(*>*)

section‹Lenses: functional references›

text ‹We use a ▩‹lens› or ∗‹functional reference› to model in-place update or reads of
deeply-nested fields within our model of the Rust language.  A lens over a record or other
product-like type (e.g., a tuple), here represented by the polymorphic type \<^typ>‹'s›, consists of
two components:
\begin{enumerate*}
\item
A ∗‹view› function which allows us to view, or ``zoom in on'', some field of a record or
product-like datatype.  Here, the field of the record is modelled as a polymorphic type \<^typ>‹'a›.
\item
A ∗‹modification› function which allows us to modify a field nested (potentially deeply) within a
record.
\end{enumerate*}

Various laws, introduced later, will be used to ensure that these two functions behave correctly, as
one would expect for a reference-like object, and which will introduce a notion of ∗‹well-formed›
lens.

Mathematically, one can think of as a lens as a ∗‹quotient› with specified lifting operations.›
datatype_record ('s, 'a) lens =
  lens_view :: ‹'s ⇒ 'a›
  lens_update :: ‹'a ⇒ 's ⇒ 's›

text ‹We can define an ∗‹update› function which sets the value of a field nested within a record
easily using the modification function of the lens:›
definition lens_modify :: ‹('s, 'a) lens ⇒ ('a ⇒ 'a) ⇒ 's ⇒ 's› where
  ‹lens_modify l f v ≡ lens_update l (f (lens_view l v)) v›

text ‹The following predicate introduces a notion of ∗‹well-formed› lens.  In particular, we have:
\begin{itemize*}
\item
If one views the content of a field after modifying it then they observe the modification,
\item
If a modification to a field is unobservable then updating the field with that modification has no
effect,
\item
Modifying a field twice, with two modifications, is the same as modifying the field once with a
single compound modification.
\item
Modifying a field is the same as updating a viewed field (this is a form of extensionality).
\end{itemize*}›
definition is_valid_lens :: ‹('s, 'a) lens ⇒ bool› where
  ‹is_valid_lens l ⟷
     ((∀x y. lens_view l (lens_update l y x) = y) ∧
      (∀x. lens_update l (lens_view l x) x = x) ∧
      (∀x y0 y1. lens_update l y1 (lens_update l y0 x) = lens_update l y1 x))›

lemma is_valid_lensI:
  assumes ‹∀x y. lens_view l (lens_update l y x) = y›
      and ‹∀x. lens_update l (lens_view l x) x = x›
      and ‹∀x y0 y1. lens_update l y1 (lens_update l y0 x) = lens_update l y1 x›
    shows ‹is_valid_lens l›
  using assms unfolding is_valid_lens_def by simp

lemma is_valid_lensE:
  assumes ‹is_valid_lens l›
      and ‹(⋀x y. lens_view l (lens_update l y x) = y)
        ⟹ (⋀x. lens_update l (lens_view l x) x = x)
        ⟹ (⋀x y0 y1. lens_update l y1 (lens_update l y0 x) = lens_update l y1 x)
        ⟹ R›
    shows ‹R›
  using assms unfolding is_valid_lens_def by simp

definition is_valid_lens_view_modify :: ‹('a ⇒ 'b) ⇒ (('b ⇒ 'b) ⇒ ('a ⇒ 'a)) ⇒ bool›
  where ‹is_valid_lens_view_modify view modify ≡
     (∀f s. view (modify f s) = f (view s)) ∧
     (∀f s. f (view s) = view s ⟶ modify f s = s) ∧
     (∀f g s. modify f (modify g s) = modify (λx. (f (g x))) s)
  ›

lemma is_valid_lens_view_modify_modify_via_update:
  assumes ‹is_valid_lens_view_modify view modify›
  shows ‹modify f x = modify (λ_. f (view x)) x› (is ‹?lhs = ?rhs›)
proof -
  let ?g = ‹λ_. f (view x)›
  have ‹?lhs = modify ?g ?lhs› 
    by (metis assms is_valid_lens_view_modify_def)
  moreover have ‹?rhs = modify ?g ?rhs›
    by (metis assms is_valid_lens_view_modify_def)
  moreover have ‹modify ?g ?lhs = ?rhs› 
    using assms by (clarsimp simp add: is_valid_lens_view_modify_def comp_def)
  ultimately show ?thesis
    by presburger
qed

definition make_lens_via_view_modify :: ‹('a ⇒ 'b) ⇒ (('b ⇒ 'b) ⇒ ('a ⇒ 'a)) ⇒ ('a, 'b) lens›
  where ‹make_lens_via_view_modify view modify ≡
    make_lens view (λy. modify (λ_. y))›

―‹Inline this definition during code generation to avoid bumping into ML value restriction for
polymorphic lens definitions (e.g. field lenses for polymorphic records):›
declare make_lens_via_view_modify_def[code_unfold]

lemma is_valid_lens_via_modifyI':
  assumes ‹is_valid_lens_view_modify view modify›
  shows ‹is_valid_lens (make_lens_via_view_modify view modify)›
  using assms unfolding is_valid_lens_view_modify_def
  by (intro is_valid_lensI; clarsimp simp add: make_lens_via_view_modify_def)

lemma make_lens_via_view_modify_components:
  shows ‹lens_view (make_lens_via_view_modify view modify) = view›
    and ‹lens_update (make_lens_via_view_modify view modify) = (λy. modify (λ_. y))›
    and ‹is_valid_lens_view_modify view modify
           ⟹ lens_modify (make_lens_via_view_modify view modify) = modify›
  apply (intro ext; clarsimp simp add: make_lens_via_view_modify_def lens_modify_def)+
  using is_valid_lens_view_modify_modify_via_update by fastforce
  
lemma is_valid_lens_via_modifyI'':
  assumes ‹is_valid_lens l›
  shows ‹is_valid_lens_view_modify (lens_view l) (lens_modify l)›
    and ‹l = make_lens_via_view_modify (lens_view l) (lens_modify l)›
proof -
  show ‹is_valid_lens_view_modify (lens_view l) (lens_modify l)›
  using assms by (elim is_valid_lensE; clarsimp simp add: is_valid_lens_view_modify_def
    lens_modify_def make_lens_via_view_modify_def) 
next
  have ‹lens_view (make_lens_via_view_modify (lens_view l) (lens_modify l)) = lens_view l›
    by (clarsimp simp add: is_valid_lens_view_modify_def
        lens_modify_def make_lens_via_view_modify_def)
  moreover have ‹lens_update (make_lens_via_view_modify (lens_view l) (lens_modify l)) = lens_update l›
    by (intro ext, clarsimp simp add: is_valid_lens_view_modify_def
        lens_modify_def make_lens_via_view_modify_def)
  ultimately show ‹l = make_lens_via_view_modify (lens_view l) (lens_modify l)› 
    by (simp add: lens.expand)
qed

lemma lens_laws_update:
  assumes ‹is_valid_lens l›
  shows ‹⋀x y. lens_view l (lens_update l y x) = y›
    and ‹⋀x. lens_update l (lens_view l x) x = x›
    and ‹⋀x y0 y1. lens_update l y1 (lens_update l y0 x) = lens_update l y1 x›
  using assms by (auto elim: is_valid_lensE)

lemma lens_laws_modify:
  assumes ‹is_valid_lens l›
  shows ‹⋀f s. lens_view l (lens_modify l f s) = f (lens_view l s)›
    and ‹⋀f s. f (lens_view l s) = lens_view l s ⟶ lens_modify l f s = s›
    and ‹⋀f g s. lens_modify l f (lens_modify l g s) = lens_modify l (λx. (f (g x))) s›
  using is_valid_lens_via_modifyI''(1)[OF assms]
  by (auto simp add: is_valid_lens_view_modify_def)

lemmas lens_laws = lens_laws_update lens_laws_modify

lemma is_valid_lens_via_modifyI:
  assumes ‹⋀f s. lens_view l (lens_modify l f s) = f (lens_view l s)›
    and ‹⋀f s. f (lens_view l s) = lens_view l s ⟶ (lens_modify l f s = s)›
    and ‹⋀f g s. lens_modify l f (lens_modify l g s) = lens_modify l (λx. f (g x)) s›
  shows ‹is_valid_lens l›
  using assms by (auto simp add: is_valid_lens_def lens_modify_def)

lemma is_valid_lens_via_modifyE:
  assumes ‹is_valid_lens l›
    and ‹(⋀f s. lens_view l (lens_modify l f s) = f (lens_view l s)) ⟹
         (⋀f s. f (lens_view l s) = lens_view l s ⟶ (lens_modify l f s = s)) ⟹
         (⋀f g s. lens_modify l f (lens_modify l g s) = lens_modify l (λx. f (g x)) s) ⟹
         R›
  shows ‹R›
  using is_valid_lens_via_modifyI''[OF assms(1)] assms (2)
  by (auto simp add: lens_modify_def make_lens_via_view_modify_def is_valid_lens_view_modify_def)

text‹The following is a ∗‹congruence› rule which describes what it means for two modifications to a
well-formed lens to be identical:›
lemma lens_modify_congI [focus_intros]:
  assumes ‹is_valid_lens l›
      and ‹f (lens_view l s) = g (lens_view l s)›
    shows ‹lens_modify l f s = lens_modify l g s›
  using assms by (simp add: lens_modify_def)

subsection‹Lens disjointness›

text ‹We say that two lenses are disjoint if modifications to the underlying state
using those lenses commute.›
definition disjoint_lenses :: ‹('s, 'a) lens ⇒ ('s,'b) lens ⇒ bool› where
  ‹disjoint_lenses l⇩1 l⇩2 ⟷
     (∀f g s. lens_modify l⇩1 f (lens_modify l⇩2 g s) = lens_modify l⇩2 g (lens_modify l⇩1 f s))›

text ‹The following are introduction and elimination rules for the disjoint lens predicate:›
lemma disjoint_lensesI [focus_intros]:
  assumes ‹⋀f g s. lens_modify l⇩1 f (lens_modify l⇩2 g s) = lens_modify l⇩2 g (lens_modify l⇩1 f s)›
    shows ‹disjoint_lenses l⇩1 l⇩2›
  using assms by (simp add: disjoint_lenses_def)

lemma disjoint_lensesE [focus_elims]:
  assumes ‹disjoint_lenses l⇩1 l⇩2›
      and ‹(⋀f g s. lens_modify l⇩1 f (lens_modify l⇩2 g s) = lens_modify l⇩2 g (lens_modify l⇩1 f s)) ⟹ R›
    shows ‹R›
  using assms by (simp add: disjoint_lenses_def)

text‹The disjoint lens predicate is commutative:›
lemma disjoint_lens_commute:
  shows ‹disjoint_lenses l⇩1 l⇩2 = disjoint_lenses l⇩2 l⇩1›
  by (auto simp add: disjoint_lenses_def)

text ‹The following pair of results capture the fact that, for disjoint and valid lenses, modifying
through one lens will not affect view through the other lens:›
lemma disjoint_lens_view1:
  assumes ‹disjoint_lenses l⇩1 l⇩2›
      and ‹is_valid_lens l⇩1›
    shows ‹lens_view l⇩1 (lens_modify l⇩2 f s) = lens_view l⇩1 s›
proof -
  from assms have ‹s = lens_modify l⇩1 (λ_. lens_view l⇩1 s) s›
    by (metis is_valid_lensE lens_modify_def)
  from this and assms have
       ‹lens_modify l⇩2 f s = lens_modify l⇩1 (λ_. lens_view l⇩1 s) (lens_modify l⇩2 f s)›
    by (auto elim: focus_elims)
  from this and assms show ?thesis
    by (metis is_valid_lens_via_modifyE)
qed

lemma disjoint_lens_view2:
  assumes ‹disjoint_lenses l⇩2 l⇩1›
      and ‹is_valid_lens l⇩1›
    shows ‹lens_view l⇩1 (lens_modify l⇩2 f s) = lens_view l⇩1 s›
  using assms by (meson disjoint_lens_commute disjoint_lens_view1)

subsection‹Basic lenses, and building more complex ones›

text ‹With a dedicate type of lenses we may now also introduce a few basic lenses, and an ∗‹algebra›
of operations over lenses satisfying various laws that allows us to combine them together.

First, we introduce the ∗‹unit› lens which makes no modification and has no effect:›

definition lens_id :: ‹('a, 'a) lens› ("id⇩L") where
  ‹id⇩L ≡ make_lens (λx. x) (λy _. y)›

text ‹Note that this unit lens is valid:›
lemma unit_lens_is_valid_lensI [focus_intros, intro]:
  shows ‹is_valid_lens id⇩L›
  by (simp add: lens_id_def is_valid_lens_def)

text‹Second, the ∗‹zero› lens which projects to the singleton type:›

definition zero_lens :: ‹('a, unit) lens› ("0⇩L") where
  ‹0⇩L ≡ make_lens (λ_. ()) (λ_ x. x)›

text ‹Note that this unit lens is valid:›
lemma zero_lens_is_valid_lensI [focus_intros, intro]:
  shows ‹is_valid_lens 0⇩L›
  by (simp add: zero_lens_def is_valid_lensI lens_update_def)

text ‹We can also ∗‹compose› lenses together.  If we are given one lens that modifies a field, ▩‹F›,
nested within a record, ▩‹R›, and another lens that modifies a field, ▩‹G›, nested deeply within the
record type of the first field, ▩‹F›, then we can obtain a derived lens that performs the update of
field ▩‹G› with respect to ▩‹R›.  Note that this allows us to model in-place updates and reads of
fields within nested hierarchies of records using the ``dot operator'', ▩‹R.F.G›, familiar from
languages like Java and Rust:›
definition compose_lens :: ‹('a, 'b) lens ⇒ ('b, 'c) lens ⇒ ('a, 'c) lens› (infixr ‹∘⇩L› 54) where
  ‹l⇩1 ∘⇩L l⇩2 ≡ make_lens_via_view_modify
      (lens_view l⇩2 ∘ lens_view l⇩1) (lens_modify l⇩1 ∘ lens_modify l⇩2)›

lemma compose_lens_is_valid_core:
  assumes ‹is_valid_lens l1›
      and ‹is_valid_lens l2›
    shows ‹is_valid_lens_view_modify (lens_view l2 ∘ lens_view l1) (lens_modify l1 ∘ lens_modify l2)›
  using assms unfolding is_valid_lens_view_modify_def
  by (elim is_valid_lensE; clarsimp simp add: comp_def
    make_lens_via_view_modify_def lens_modify_def)

text ‹If two lenses are valid then their composition is, also:›
lemma compose_lens_is_valid_lens_preserving [focus_intros, intro]:
  assumes ‹is_valid_lens l⇩1›
      and ‹is_valid_lens l⇩2›
  shows ‹is_valid_lens (l⇩1 ∘⇩L l⇩2)›
  by (simp add: assms compose_lens_def compose_lens_is_valid_core is_valid_lens_via_modifyI')

lemma compose_lens_components:
  shows ‹lens_update (l⇩1 ∘⇩L l⇩2) y x = lens_update l⇩1 (lens_update l⇩2 y (lens_view l⇩1 x)) x›
    and ‹lens_view (l⇩1 ∘⇩L l⇩2) = lens_view l⇩2 ∘ lens_view l⇩1›
    and ‹is_valid_lens l⇩1 ⟹ is_valid_lens l⇩2 ⟹ 
         lens_modify (l⇩1 ∘⇩L l⇩2) = lens_modify l⇩1 ∘ lens_modify l⇩2›
  by (auto simp add: compose_lens_def lens_modify_def compose_lens_is_valid_core
      make_lens_via_view_modify_components)

text ‹The following pair of lemmas captures the fact that composing any lens, ▩‹L›, with the unit
lens that does nothing is equivalent to ▩‹L›:›
lemma compose_lens_unit [focus_simps]:
  shows ‹id⇩L ∘⇩L l = l›
  by (cases l; auto intro!: ext simp add: compose_lens_def lens_id_def 
    make_lens_via_view_modify_def lens_modify_def)

lemma compose_lens_unit2 [focus_simps]:
  shows ‹l ∘⇩L id⇩L = l›
  by (cases l; auto intro!: ext simp add: compose_lens_def lens_id_def 
    make_lens_via_view_modify_def lens_modify_def)

lemma compose_lens_zero:
  assumes ‹is_valid_lens l›
  shows ‹l ∘⇩L 0⇩L = 0⇩L›
  using assms by (cases l; auto elim!: is_valid_lensE intro!: ext simp add: compose_lens_def 
    zero_lens_def make_lens_via_view_modify_def lens_modify_def)

text ‹Composition is associative for lenses.  This captures the idea that the ``dot operator'' of
Java and Rust is also associative, so ▩‹(R.F).G› is equivalent to ▩‹R.(F.G)› and therefore the
parentheses can be dispensed with:›
lemma compose_lens_assoc [focus_simps]:
  shows ‹(l⇩1 ∘⇩L l⇩2) ∘⇩L l⇩3 = l⇩1 ∘⇩L (l⇩2 ∘⇩L l⇩3)›
  by (auto simp add: compose_lens_def make_lens_via_view_modify_def lens_modify_def intro!: ext)

text ‹Moreover, if we have a pair of disjoint lenses then composing either one of them with a third
lens retains their disjoint character:›
lemma disjoint_compose:
  assumes ‹disjoint_lenses l⇩1 l⇩2›
    shows ‹disjoint_lenses l⇩1 (l⇩2 ∘⇩L l⇩3)›
  using assms by (auto simp add: make_lens_via_view_modify_def disjoint_lenses_def compose_lens_def
    lens_modify_def) (metis lens_modify_def)

text ‹The following pair of lenses can be used to view or modify the first- and second-projections
of a tuple type, respectively:›
definition lens_fst :: ‹('a × 'b, 'a) lens› ("fst⇩L") where
  ‹fst⇩L ≡ make_lens fst (λy0 (y, x). (y0, x))›

definition lens_snd :: ‹('a × 'b, 'b) lens› ("snd⇩L") where
  ‹snd⇩L ≡ make_lens snd (λy0 (x, y). (x, y0))›

text ‹Both of these lenses are also valid:›
lemma lens_fst_is_valid_lensI [focus_intros, intro]:
  shows ‹is_valid_lens fst⇩L›
  by (auto simp add: lens_fst_def lens_update_def is_valid_lens_def)

lemma lens_snd_is_valid_lensI [focus_intros, intro]:
  shows ‹is_valid_lens snd⇩L›
  by (auto simp add: lens_snd_def lens_update_def is_valid_lens_def)

subsection‹The lens locale›
locale lens_defs =
  fixes
    view :: ‹'s ⇒ 't› and
    update :: ‹'t ⇒ 's ⇒ 's›
begin

abbreviation ‹get_lens ≡ make_lens view update›
abbreviation ‹modify ≡ lens_modify get_lens›

end

locale lens = lens_defs +
  assumes
    lens_valid: ‹is_valid_lens (make_lens view update)›

(*<*)
end
(*>*)