Theory Lens_Laws

section ‹Core Lens Laws›

theory Lens_Laws
imports
  Two Interp
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" and "Fischer2015" and "Gibbons17"›.›
  
record ('a, 'b) lens =
  lens_get :: "'b ⇒ 'a" (‹getı›)
  lens_put :: "'b ⇒ 'a ⇒ 'b" (‹putı›)

type_notation
  lens (infixr ‹⟹› 0)

text ‹ Alternative parameters ordering, inspired by Back and von Wright's refinement 
  calculus~\<^cite>‹"Back1998"›, which similarly uses two functions to characterise updates to variables. ›

abbreviation (input) lens_set :: "('a ⟹ 'b) ⇒ 'a ⇒ 'b ⇒ 'b" (‹lsetı›) where
"lens_set ≡ (λ X v s. put⇘X⇙ s v)"

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" and "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 ‹ @{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}"

text ‹ A partial version of @{const lens_get}, which can be useful for partial lenses. ›

definition lens_partial_get :: "('a ⟹ 'b) ⇒ 'b ⇒ 'a option" (‹pgetı›) where
"lens_partial_get x s = (if s ∈ 𝒮⇘x⇙ then Some (get⇘x⇙ s) else None)"

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. ›
    
definition lens_update :: "('a ⟹ 'b) ⇒ ('a ⇒ 'a) ⇒ ('b ⇒ 'b)" (‹updateı›) where
[lens_defs]: "lens_update X f σ = put⇘X⇙ σ (f (get⇘X⇙ σ))"

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 lens_obs_eq :: "('b ⟹ 'a) ⇒ 'a ⇒ 'a ⇒ bool" (infix ‹≃ı› 50) where
[lens_defs]: "s⇩1 ≃⇘X⇙ s⇩2 = (s⇩1 = put⇘X⇙ s⇩2 (get⇘X⇙ s⇩1))"

text ‹ This relation states that two sources are equivalent outside of the region characterised
  by lens $X$. ›

definition lens_override :: "('b ⟹ 'a) ⇒ 'a ⇒ 'a ⇒ 'a" (infixl ‹◃ı› 95) where
[lens_defs]: "S⇩1 ◃⇘X⇙ S⇩2 = put⇘X⇙ S⇩1 (get⇘X⇙ S⇩2)"

abbreviation (input) lens_override' :: "'a ⇒ 'a ⇒ ('b ⟹ 'a) ⇒ 'a" (‹_ ⊕⇩L _ on _› [95,0,96] 95) where
"S⇩1 ⊕⇩L S⇩2 on X ≡ S⇩1 ◃⇘X⇙ S⇩2"

text ‹Lens override uses a lens to replace part of a source type with a given value for the
  corresponding view.›

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" and "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)

  lemma get_update: "get (update f σ) = f (get σ)"
    by (simp add: put_get lens_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]

lemma dom_pget: "dom pget⇘x⇙ = 𝒮⇘x⇙"
  by (simp add: lens_partial_get_def dom_def)

subsection ‹Well-behaved Lenses›

text ‹ Well-behaved lenses add to weak lenses that requirement that the GetPut law~\<^cite>‹"Foster09" and "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 lens_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

abbreviation (input) "partial_lens ≡ mwb_lens"

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" and "Fischer2015"›.
  The same set of axioms can be found in Back and von Wright's refinement calculus~\<^cite>‹"Back1998"›, 
  though with different names for the functions. ›

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)

  lemma get_surj: "surj get"
    by (metis put_get surjI)

  text ‹ Observation equivalence is an equivalence relation. ›

  lemma lens_obs_equiv: "equivp (≃)"
  proof (rule equivpI)
    show "reflp (≃)"
      by (rule reflpI, simp add: lens_obs_eq_def get_put)
    show "symp (≃)"
      by (rule sympI, simp add: lens_obs_eq_def, metis get_put put_put)
    show "transp (≃)"
      by (rule transpI, simp add: lens_obs_eq_def, metis put_put)
  qed

end

abbreviation (input) "total_lens ≡ vwb_lens"

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

lemma mwb_UNIV_src_is_vwb_lens: 
  "⟦ mwb_lens X; 𝒮⇘X⇙ = UNIV ⟧ ⟹ vwb_lens X"
  using vwb_lens_def wb_lens_axioms_def wb_lens_def by fastforce

text ‹ Alternative characterisation: a very well-behaved (i.e. total) lens is a mainly well-behaved
  (i.e. partial) lens whose source is the universe set. ›

lemma vwb_lens_iff_mwb_UNIV_src: 
  "vwb_lens X ⟷ (mwb_lens X ∧ 𝒮⇘X⇙ = UNIV)"
  by (meson mwb_UNIV_src_is_vwb_lens vwb_lens_def wb_lens.source_UNIV)

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

lemma ief_then_vwb: "vwb_lens x"
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

sublocale vwb_lens by (fact ief_then_vwb)

lemma ineffectual_const_get:
  "∃ v.  ∀ σ∈𝒮. get σ = v"
  using put_get put_inef by auto

end

declare ief_lens.ief_then_vwb [simp]

text ‹ There is no ineffectual lens when the view type has two or more elements. ›

lemma no_ief_two_view:
  assumes "ief_lens (x :: 'a::two ⟹ 's)"
  shows "False"
proof -
  obtain x y :: "'a::two" where "x ≠ y"
    using two_diff by auto
  with assms show ?thesis
    by (metis (full_types) ief_lens.axioms(1) ief_lens.put_inef weak_lens.put_get)
qed

abbreviation "eff_lens X ≡ (weak_lens X ∧ (¬ ief_lens X))"

subsection ‹ Partially Bijective Lenses ›

locale pbij_lens = weak_lens +
  assumes put_det: "put σ v = put ρ v"
begin

  sublocale mwb_lens
  proof
    fix σ v u
    show "put (put σ v) u = put σ u"
      using put_det by blast
  qed
  
  lemma put_is_create: "put σ v = create v"
    by (simp add: lens_create_def put_det)

  lemma partial_get_put: "ρ ∈ 𝒮 ⟹ put σ (get ρ) = ρ"
    by (metis put_det weak_get_put)

end

lemma pbij_lens_weak [simp]:
  "pbij_lens x ⟹ weak_lens x"
  by (simp_all add: pbij_lens_def)

lemma pbij_lens_mwb [simp]: "pbij_lens x ⟹ mwb_lens x"
  by (simp add: mwb_lens_axioms.intro mwb_lens_def pbij_lens.put_is_create)

lemma pbij_alt_intro:
  "⟦ weak_lens X; ⋀ s. s ∈ 𝒮⇘X⇙ ⟹ create⇘X⇙ (get⇘X⇙ s) = s ⟧ ⟹ pbij_lens X"
  by (metis pbij_lens_axioms_def pbij_lens_def weak_lens.put_closure weak_lens.put_get)

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" and "Fischer2015"›.›

locale bij_lens = weak_lens +
  assumes strong_get_put: "put σ (get ρ) = ρ"
begin

sublocale pbij_lens
proof
  fix σ v ρ
  show "put σ v = put ρ v"
    by (metis put_get strong_get_put)
qed

sublocale vwb_lens
proof
  fix σ v u
  show "put σ (get σ) = σ"
    by (simp add: strong_get_put)
qed

  lemma put_bij: "bij_betw (put σ) UNIV UNIV"
    by (metis bijI put_inj strong_get_put surj_def)

  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_pbij [simp]:
  "bij_lens x ⟹ pbij_lens x"
  by (metis bij_lens.get_create bij_lens_def pbij_lens_axioms.intro pbij_lens_def weak_lens.put_get)

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)

text ‹ Alternative characterisation: a bijective lens is a partial bijective lens that is also
  very well-behaved (i.e. total). ›

lemma pbij_vwb_is_bij_lens:
  "⟦ pbij_lens X; vwb_lens X ⟧ ⟹ bij_lens X"
  by (unfold_locales, simp_all, meson pbij_lens.put_det vwb_lens.put_eq)

lemma bij_lens_iff_pbij_vwb:
  "bij_lens X ⟷ (pbij_lens X ∧ vwb_lens X)"
  using pbij_vwb_is_bij_lens by auto

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 σ. put⇘x⇙ (put⇘y⇙ σ v) u = put⇘y⇙ (put⇘x⇙ σ u) v;
     ⋀ v σ. get⇘x⇙ (put⇘y⇙ σ v) = get⇘x⇙ σ;
     ⋀ u σ. get⇘y⇙ (put⇘x⇙ σ u) = 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_comm:
  "x ⨝ y ⟹ put⇘x⇙ (put⇘y⇙ σ v) u = put⇘y⇙ (put⇘x⇙ σ u) v"
  by (simp add: lens_indep_def)

lemma lens_indep_get [simp]:
  assumes "x ⨝ y"
  shows "get⇘x⇙ (put⇘y⇙ σ v) = get⇘x⇙ σ"
  using assms lens_indep_def by fastforce

text ‹ Characterisation of independence for two very well-behaved lenses ›

lemma lens_indep_vwb_iff:
  assumes "vwb_lens x" "vwb_lens y"
  shows "x ⨝ y ⟷ (∀ u v σ. put⇘x⇙ (put⇘y⇙ σ v) u = put⇘y⇙ (put⇘x⇙ σ u) v)"
proof
  assume "x ⨝ y"
  thus "∀ u v σ. put⇘x⇙ (put⇘y⇙ σ v) u = put⇘y⇙ (put⇘x⇙ σ u) v"
    by (simp add: lens_indep_comm)
next
  assume a: "∀ u v σ. put⇘x⇙ (put⇘y⇙ σ v) u = put⇘y⇙ (put⇘x⇙ σ u) v"
  show "x ⨝ y"
  proof (unfold_locales)
    fix σ v u
    from a show "put⇘x⇙ (put⇘y⇙ σ v) u = put⇘y⇙ (put⇘x⇙ σ u) v" 
      by auto
    show "get⇘x⇙ (put⇘y⇙ σ v) = get⇘x⇙ σ"
      by (metis a assms(1) vwb_lens.put_eq vwb_lens_wb wb_lens_def weak_lens.put_get)
    show "get⇘y⇙ (put⇘x⇙ σ u) = get⇘y⇙ σ"
      by (metis a assms(2) vwb_lens.put_eq vwb_lens_wb wb_lens_def weak_lens.put_get)
  qed
qed

subsection ‹ Lens Compatibility ›

text ‹ Lens compatibility is a weaker notion than independence. It allows that two lenses can overlap
  so long as they manipulate the source in the same way in that region. It is most easily defined
  in terms of a function for copying a region from one source to another using a lens. ›

definition lens_compat (infix ‹##⇩L› 50) where
[lens_defs]: "lens_compat X Y = (∀s⇩1 s⇩2. s⇩1 ◃⇘X⇙ s⇩2 ◃⇘Y⇙ s⇩2 = s⇩1 ◃⇘Y⇙ s⇩2 ◃⇘X⇙ s⇩2)"

lemma lens_compat_idem [simp]: "x ##⇩L x"
  by (simp add: lens_defs)

lemma lens_compat_sym: "x ##⇩L y ⟹ y ##⇩L x"
  by (simp add: lens_defs)

lemma lens_indep_compat [simp]: "x ⨝ y ⟹ x ##⇩L y"
  by (simp add: lens_override_def lens_compat_def lens_indep_comm)

end