Theory Lens_Laws

(******************************************************************************)
(* 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" (‹𝒮ı›) where
"lens_source X = {s. ∃ v s'. s = put⇘X⇙ s' v}"

abbreviation some_source :: "('a ⟹ 'b) ⇒ 'b" (‹srcı›) where
"some_source X ≡ (SOME s. s ∈ 𝒮⇘X⇙)"

definition lens_create :: "('a ⟹ 'b) ⇒ 'a ⇒ 'b" (‹createı›) where
[lens_defs]: "create⇘X⇙ v = put⇘X⇙ (src⇘X⇙) 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 ∈ 𝒮"
    by (auto simp add: lens_source_def)

  lemma put_closure: "put σ v ∈ 𝒮"
    by (auto simp add: lens_source_def)

  lemma create_closure: "create v ∈ 𝒮"
    by (simp add: lens_create_def put_closure)

  lemma src_source [simp]: "src ∈ 𝒮"
    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]: "𝒮 = 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: "σ ∈ 𝒮 ⟹ put σ (get σ) = σ"
    by (auto simp add: lens_source_def put_get put_put)

  lemma weak_source_determination:
    assumes "σ ∈ 𝒮" "ρ ∈ 𝒮" "get σ = get ρ" "put σ v = put ρ v"
    shows "σ = ρ"
    by (metis assms put_put weak_get_put)

   lemma weak_put_eq:
     assumes "σ ∈ 𝒮" "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 ∈ 𝒮 ⟹ 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.  ∀ σ∈𝒮. 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: "σ ∈ 𝒮 ⟹ put σ v = create v"
    by (metis create_get strong_get_put)

  lemma get_create: "σ ∈ 𝒮 ⟹ 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 vwb_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⇘X⇙ (put⇘Y⇙ σ v) u = put⇘Y⇙ (put⇘X⇙ σ u) v"
  and lens_put_irr1: "get⇘X⇙ (put⇘Y⇙ σ v) = get⇘X⇙ σ"
  and lens_put_irr2: "get⇘Y⇙ (put⇘X⇙ σ u) = get⇘Y⇙ σ"

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