Theory Optics.Lens_Algebra

section ‹Lens Algebraic Operators›

theory Lens_Algebra
imports Lens_Laws
begin

subsection ‹Lens Composition, Plus, Unit, and Identity›

text ‹
  \begin{figure}
  \begin{center}
    \includegraphics[width=7cm]{figures/Composition}
  \end{center}
  \vspace{-5ex}
  \caption{Lens Composition}
  \label{fig:Comp}
  \end{figure}
  We introduce the algebraic lens operators; for more information please see our paper~\<^cite>‹"Foster16a"›.
  Lens composition, illustrated in Figure~\ref{fig:Comp}, constructs a lens by composing the source 
  of one lens with the view of another.›

definition lens_comp :: "('a ⟹ 'b) ⇒ ('b ⟹ 'c) ⇒ ('a ⟹ 'c)" (infixl ";⇩L" 80) where
[lens_defs]: "lens_comp Y X = ⦇ lens_get = get⇘Y⇙ ∘ lens_get X
                              , lens_put = (λ σ v. lens_put X σ (lens_put Y (lens_get X σ) v)) ⦈"

text ‹
  \begin{figure}
  \begin{center}
    \includegraphics[width=7cm]{figures/Sum}
  \end{center}
  \vspace{-5ex}
  \caption{Lens Sum}
  \label{fig:Sum}
  \end{figure}
  Lens plus, as illustrated in Figure~\ref{fig:Sum} parallel composes two independent lenses, 
  resulting in a lens whose view is the product of the two underlying lens views.›

definition lens_plus :: "('a ⟹ 'c) ⇒ ('b ⟹ 'c) ⇒ 'a × 'b ⟹ 'c" (infixr "+⇩L" 75) where
[lens_defs]: "X +⇩L Y = ⦇ lens_get = (λ σ. (lens_get X σ, lens_get Y σ))
                       , lens_put = (λ σ (u, v). lens_put X (lens_put Y σ v) u) ⦈"

text ‹The product functor lens similarly parallel composes two lenses, but in this case the lenses
  have different sources and so the resulting source is also a product.›

definition lens_prod :: "('a ⟹ 'c) ⇒ ('b ⟹ 'd) ⇒ ('a × 'b ⟹ 'c × 'd)" (infixr "×⇩L" 85) where
[lens_defs]: "lens_prod X Y = ⦇ lens_get = map_prod get⇘X⇙ get⇘Y⇙
                              , lens_put = λ (u, v) (x, y). (put⇘X⇙ u x, put⇘Y⇙ v y) ⦈"

text ‹The $\lfst$ and $\lsnd$ lenses project the first and second elements, respectively, of a
  product source type.›

definition fst_lens :: "'a ⟹ 'a × 'b" ("fst⇩L") where
[lens_defs]: "fst⇩L = ⦇ lens_get = fst, lens_put = (λ (σ, ρ) u. (u, ρ)) ⦈"

definition snd_lens :: "'b ⟹ 'a × 'b" ("snd⇩L") where
[lens_defs]: "snd⇩L = ⦇ lens_get = snd, lens_put = (λ (σ, ρ) u. (σ, u)) ⦈"

lemma get_fst_lens [simp]: "get⇘fst⇩L⇙ (x, y) = x"
  by (simp add: fst_lens_def)

lemma get_snd_lens [simp]: "get⇘snd⇩L⇙ (x, y) = y"
  by (simp add: snd_lens_def)

text ‹The swap lens is a bijective lens which swaps over the elements of the product source type.›

abbreviation swap_lens :: "'a × 'b ⟹ 'b × 'a" ("swap⇩L") where
"swap⇩L ≡ snd⇩L +⇩L fst⇩L"

text ‹The zero lens is an ineffectual lens whose view is a unit type. This means the zero lens
  cannot distinguish or change the source type.›

definition zero_lens :: "unit ⟹ 'a" ("0⇩L") where
[lens_defs]: "0⇩L = ⦇ lens_get = (λ _. ()), lens_put = (λ σ x. σ) ⦈"

text ‹The identity lens is a bijective lens where the source and view type are the same.›

definition id_lens :: "'a ⟹ 'a" ("1⇩L") where
[lens_defs]: "1⇩L = ⦇ lens_get = id, lens_put = (λ _. id) ⦈"

text ‹The quotient operator $X \lquot Y$ shortens lens $X$ by cutting off $Y$ from the end. It is
  thus the dual of the composition operator.›

definition lens_quotient :: "('a ⟹ 'c) ⇒ ('b ⟹ 'c) ⇒ 'a ⟹ 'b" (infixr "'/⇩L" 90) where
[lens_defs]: "X /⇩L Y = ⦇ lens_get = λ σ. get⇘X⇙ (create⇘Y⇙ σ)
                       , lens_put = λ σ v. get⇘Y⇙ (put⇘X⇙ (create⇘Y⇙ σ) v) ⦈"

text ‹Lens inverse take a bijective lens and swaps the source and view types.›

definition lens_inv :: "('a ⟹ 'b) ⇒ ('b ⟹ 'a)" ("inv⇩L") where
[lens_defs]: "lens_inv x = ⦇ lens_get = create⇘x⇙, lens_put = λ σ. get⇘x⇙ ⦈"

subsection ‹Closure Poperties›

text ‹We show that the core lenses combinators defined above are closed under the key lens classes.›
  
lemma id_wb_lens: "wb_lens 1⇩L"
  by (unfold_locales, simp_all add: id_lens_def)

lemma source_id_lens: "𝒮⇘1⇩L⇙ = UNIV"
  by (simp add: id_lens_def lens_source_def)

lemma unit_wb_lens: "wb_lens 0⇩L"
  by (unfold_locales, simp_all add: zero_lens_def)

lemma source_zero_lens: "𝒮⇘0⇩L⇙ = UNIV"
  by (simp_all add: zero_lens_def lens_source_def)

lemma comp_weak_lens: "⟦ weak_lens x; weak_lens y ⟧ ⟹ weak_lens (x ;⇩L y)"
  by (unfold_locales, simp_all add: lens_comp_def)

lemma comp_wb_lens: "⟦ wb_lens x; wb_lens y ⟧ ⟹ wb_lens (x ;⇩L y)"
  by (unfold_locales, auto simp add: lens_comp_def wb_lens_def weak_lens.put_closure)
   
lemma comp_mwb_lens: "⟦ mwb_lens x; mwb_lens y ⟧ ⟹ mwb_lens (x ;⇩L y)"
  by (unfold_locales, auto simp add: lens_comp_def mwb_lens_def weak_lens.put_closure)

lemma source_lens_comp: "⟦ mwb_lens x; mwb_lens y ⟧ ⟹ 𝒮⇘x ;⇩L y⇙ = {s ∈ 𝒮⇘y⇙. get⇘y⇙ s ∈ 𝒮⇘x⇙}"
  by (auto simp add: lens_comp_def lens_source_def, blast, metis mwb_lens.put_put mwb_lens_def weak_lens.put_get)

lemma id_vwb_lens [simp]: "vwb_lens 1⇩L"
  by (unfold_locales, simp_all add: id_lens_def)

lemma unit_vwb_lens [simp]: "vwb_lens 0⇩L"
  by (unfold_locales, simp_all add: zero_lens_def)

lemma comp_vwb_lens: "⟦ vwb_lens x; vwb_lens y ⟧ ⟹ vwb_lens (x ;⇩L y)"
  by (unfold_locales, simp_all add: lens_comp_def weak_lens.put_closure)

lemma unit_ief_lens: "ief_lens 0⇩L"
  by (unfold_locales, simp_all add: zero_lens_def)

text ‹Lens plus requires that the lenses be independent to show closure.›
    
lemma plus_mwb_lens:
  assumes "mwb_lens x" "mwb_lens y" "x ⨝ y"
  shows "mwb_lens (x +⇩L y)"
  using assms
  apply (unfold_locales)
   apply (simp_all add: lens_plus_def prod.case_eq_if lens_indep_sym)
  apply (simp add: lens_indep_comm)
done

lemma plus_wb_lens:
  assumes "wb_lens x" "wb_lens y" "x ⨝ y"
  shows "wb_lens (x +⇩L y)"
  using assms
  apply (unfold_locales, simp_all add: lens_plus_def)
  apply (simp add: lens_indep_sym prod.case_eq_if)
done

lemma plus_vwb_lens [simp]:
  assumes "vwb_lens x" "vwb_lens y" "x ⨝ y"
  shows "vwb_lens (x +⇩L y)"
  using assms
  apply (unfold_locales, simp_all add: lens_plus_def)
   apply (simp add: lens_indep_sym prod.case_eq_if)
  apply (simp add: lens_indep_comm prod.case_eq_if)
done

lemma source_plus_lens:
  assumes "mwb_lens x" "mwb_lens y" "x ⨝ y"
  shows "𝒮⇘x +⇩L y⇙ = 𝒮⇘x⇙ ∩ 𝒮⇘y⇙"
  apply (auto simp add: lens_source_def lens_plus_def)
  apply (meson assms(3) lens_indep_comm)
  apply (metis assms(1) mwb_lens.weak_get_put mwb_lens_weak weak_lens.put_closure)
done

lemma prod_mwb_lens:
  "⟦ mwb_lens X; mwb_lens Y ⟧ ⟹ mwb_lens (X ×⇩L Y)"
  by (unfold_locales, simp_all add: lens_prod_def prod.case_eq_if)

lemma prod_wb_lens:
  "⟦ wb_lens X; wb_lens Y ⟧ ⟹ wb_lens (X ×⇩L Y)"
  by (unfold_locales, simp_all add: lens_prod_def prod.case_eq_if)

lemma prod_vwb_lens:
  "⟦ vwb_lens X; vwb_lens Y ⟧ ⟹ vwb_lens (X ×⇩L Y)"
  by (unfold_locales, simp_all add: lens_prod_def prod.case_eq_if)

lemma prod_bij_lens:
  "⟦ bij_lens X; bij_lens Y ⟧ ⟹ bij_lens (X ×⇩L Y)"
  by (unfold_locales, simp_all add: lens_prod_def prod.case_eq_if)

lemma fst_vwb_lens: "vwb_lens fst⇩L"
  by (unfold_locales, simp_all add: fst_lens_def prod.case_eq_if)

lemma snd_vwb_lens: "vwb_lens snd⇩L"
  by (unfold_locales, simp_all add: snd_lens_def prod.case_eq_if)

lemma id_bij_lens: "bij_lens 1⇩L"
  by (unfold_locales, simp_all add: id_lens_def)

lemma inv_id_lens: "inv⇩L 1⇩L = 1⇩L"
  by (auto simp add: lens_inv_def id_lens_def lens_create_def)

lemma inv_inv_lens: "bij_lens X ⟹ inv⇩L (inv⇩L X) = X"
  apply (cases X)
  apply (auto simp add: lens_defs fun_eq_iff)
  apply (metis (no_types) bij_lens.strong_get_put bij_lens_def select_convs(2) weak_lens.put_get)
  done

lemma lens_inv_bij: "bij_lens X ⟹ bij_lens (inv⇩L X)"
  by (unfold_locales, simp_all add: lens_inv_def lens_create_def)

lemma swap_bij_lens: "bij_lens swap⇩L"
  by (unfold_locales, simp_all add: lens_plus_def prod.case_eq_if fst_lens_def snd_lens_def)

subsection ‹Composition Laws›

text ‹Lens composition is monoidal, with unit @{term "1⇩L"}, as the following theorems demonstrate. 
  It also has @{term "0⇩L"} as a right annihilator. ›
  
lemma lens_comp_assoc: "X ;⇩L (Y ;⇩L Z) = (X ;⇩L Y) ;⇩L Z"
  by (auto simp add: lens_comp_def)

lemma lens_comp_left_id [simp]: "1⇩L ;⇩L X = X"
  by (simp add: id_lens_def lens_comp_def)

lemma lens_comp_right_id [simp]: "X ;⇩L 1⇩L = X"
  by (simp add: id_lens_def lens_comp_def)

lemma lens_comp_anhil [simp]: "wb_lens X ⟹ 0⇩L ;⇩L X = 0⇩L"
  by (simp add: zero_lens_def lens_comp_def comp_def)

lemma lens_comp_anhil_right [simp]: "wb_lens X ⟹ X ;⇩L 0⇩L = 0⇩L"
  by (simp add: zero_lens_def lens_comp_def comp_def)

subsection ‹Independence Laws›

text ‹The zero lens @{term "0⇩L"} is independent of any lens. This is because nothing can be observed
  or changed using @{term "0⇩L"}. ›
  
lemma zero_lens_indep [simp]: "0⇩L ⨝ X"
  by (auto simp add: zero_lens_def lens_indep_def)

lemma zero_lens_indep' [simp]: "X ⨝ 0⇩L"
  by (auto simp add: zero_lens_def lens_indep_def)

text ‹Lens independence is irreflexive, but only for effectual lenses as otherwise nothing can
  be observed.›
    
lemma lens_indep_quasi_irrefl: "⟦ wb_lens x; eff_lens x ⟧ ⟹ ¬ (x ⨝ x)"
  unfolding lens_indep_def ief_lens_def ief_lens_axioms_def
  by (simp, metis (full_types) wb_lens.get_put)

text ‹Lens independence is a congruence with respect to composition, as the following properties demonstrate.›
    
lemma lens_indep_left_comp [simp]:
  "⟦ mwb_lens z; x ⨝ y ⟧ ⟹ (x ;⇩L z) ⨝ (y ;⇩L z)"
  apply (rule lens_indepI)
    apply (auto simp add: lens_comp_def)
   apply (simp add: lens_indep_comm)
  apply (simp add: lens_indep_sym)
done

lemma lens_indep_right_comp:
  "y ⨝ z ⟹ (x ;⇩L y) ⨝ (x ;⇩L z)"
  apply (auto intro!: lens_indepI simp add: lens_comp_def)
    using lens_indep_comm lens_indep_sym apply fastforce
  apply (simp add: lens_indep_sym)
done

lemma lens_indep_left_ext [intro]:
  "y ⨝ z ⟹ (x ;⇩L y) ⨝ z"
  apply (auto intro!: lens_indepI simp add: lens_comp_def)
   apply (simp add: lens_indep_comm)
  apply (simp add: lens_indep_sym)
done

lemma lens_indep_right_ext [intro]:
  "x ⨝ z ⟹ x ⨝ (y ;⇩L z)"
  by (simp add: lens_indep_left_ext lens_indep_sym)

lemma lens_comp_indep_cong_left:
  "⟦ mwb_lens Z; X ;⇩L Z ⨝ Y ;⇩L Z ⟧ ⟹ X ⨝ Y"
  apply (rule lens_indepI)
    apply (rename_tac u v σ)
    apply (drule_tac u=u and v=v and σ="create⇘Z⇙ σ" in lens_indep_comm)
    apply (simp add: lens_comp_def)
    apply (meson mwb_lens_weak weak_lens.view_determination)
   apply (rename_tac v σ)
   apply (drule_tac v=v and σ="create⇘Z⇙ σ" in lens_indep_get)
   apply (simp add: lens_comp_def)
  apply (drule lens_indep_sym)
  apply (rename_tac u σ)
  apply (drule_tac v=u and σ="create⇘Z⇙ σ" in lens_indep_get)
  apply (simp add: lens_comp_def)
done

lemma lens_comp_indep_cong:
  "mwb_lens Z ⟹ (X ;⇩L Z) ⨝ (Y ;⇩L Z) ⟷ X ⨝ Y"
  using lens_comp_indep_cong_left lens_indep_left_comp by blast

text ‹The first and second lenses are independent since the view different parts of a product source.›
    
lemma fst_snd_lens_indep [simp]:
  "fst⇩L ⨝ snd⇩L"
  by (simp add: lens_indep_def fst_lens_def snd_lens_def)

lemma snd_fst_lens_indep [simp]:
  "snd⇩L ⨝ fst⇩L"
  by (simp add: lens_indep_def fst_lens_def snd_lens_def)

lemma split_prod_lens_indep:
  assumes "mwb_lens X"
  shows "(fst⇩L ;⇩L X) ⨝ (snd⇩L ;⇩L X)"
  using assms fst_snd_lens_indep lens_indep_left_comp vwb_lens_mwb by blast
    
text ‹Lens independence is preserved by summation.›
    
lemma plus_pres_lens_indep [simp]: "⟦ X ⨝ Z; Y ⨝ Z ⟧ ⟹ (X +⇩L Y) ⨝ Z"
  apply (rule lens_indepI)
    apply (simp_all add: lens_plus_def prod.case_eq_if)
   apply (simp add: lens_indep_comm)
  apply (simp add: lens_indep_sym)
done

lemma plus_pres_lens_indep' [simp]:
  "⟦ X ⨝ Y; X ⨝ Z ⟧ ⟹ X ⨝ Y +⇩L Z"
  by (auto intro: lens_indep_sym plus_pres_lens_indep)

text ‹Lens independence is preserved by product.›
    
lemma lens_indep_prod:
  "⟦ X⇩1 ⨝ X⇩2; Y⇩1 ⨝ Y⇩2 ⟧ ⟹ X⇩1 ×⇩L Y⇩1 ⨝ X⇩2 ×⇩L Y⇩2"
  apply (rule lens_indepI)
    apply (auto simp add: lens_prod_def prod.case_eq_if lens_indep_comm map_prod_def)
   apply (simp_all add: lens_indep_sym)
  done

subsection ‹ Compatibility Laws ›

lemma zero_lens_compat [simp]: "0⇩L ##⇩L X"
  by (auto simp add: zero_lens_def lens_override_def lens_compat_def)

lemma id_lens_compat [simp]: "vwb_lens X ⟹ 1⇩L ##⇩L X"
  by (auto simp add: id_lens_def lens_override_def lens_compat_def)

subsection ‹Algebraic Laws›

text ‹Lens plus distributes to the right through composition.›
  
lemma plus_lens_distr: "mwb_lens Z ⟹ (X +⇩L Y) ;⇩L Z = (X ;⇩L Z) +⇩L (Y ;⇩L Z)"
  by (auto simp add: lens_comp_def lens_plus_def comp_def)

text ‹The first lens projects the first part of a summation.›
  
lemma fst_lens_plus:
  "wb_lens y ⟹ fst⇩L ;⇩L (x +⇩L y) = x"
  by (simp add: fst_lens_def lens_plus_def lens_comp_def comp_def)

text ‹The second law requires independence as we have to apply x first, before y›

lemma snd_lens_plus:
  "⟦ wb_lens x; x ⨝ y ⟧ ⟹ snd⇩L ;⇩L (x +⇩L y) = y"
  apply (simp add: snd_lens_def lens_plus_def lens_comp_def comp_def)
  apply (subst lens_indep_comm)
   apply (simp_all)
done

text ‹The swap lens switches over a summation.›
  
lemma lens_plus_swap:
  "X ⨝ Y ⟹ swap⇩L ;⇩L (X +⇩L Y) = (Y +⇩L X)"
  by (auto simp add: lens_plus_def fst_lens_def snd_lens_def id_lens_def lens_comp_def lens_indep_comm)

text ‹The first, second, and swap lenses are all closely related.›
    
lemma fst_snd_id_lens: "fst⇩L +⇩L snd⇩L = 1⇩L"
  by (auto simp add: lens_plus_def fst_lens_def snd_lens_def id_lens_def)

lemma swap_lens_idem: "swap⇩L ;⇩L swap⇩L = 1⇩L"
  by (simp add: fst_snd_id_lens lens_indep_sym lens_plus_swap)

lemma swap_lens_fst: "fst⇩L ;⇩L swap⇩L = snd⇩L"
  by (simp add: fst_lens_plus fst_vwb_lens)

lemma swap_lens_snd: "snd⇩L ;⇩L swap⇩L = fst⇩L"
  by (simp add: lens_indep_sym snd_lens_plus snd_vwb_lens)

text ‹The product lens can be rewritten as a sum lens.›
    
lemma prod_as_plus: "X ×⇩L Y = X ;⇩L fst⇩L +⇩L Y ;⇩L snd⇩L"
  by (auto simp add: lens_prod_def fst_lens_def snd_lens_def lens_comp_def lens_plus_def)

lemma prod_lens_id_equiv:
  "1⇩L ×⇩L 1⇩L = 1⇩L"
  by (auto simp add: lens_prod_def id_lens_def)

lemma prod_lens_comp_plus:
  "X⇩2 ⨝ Y⇩2 ⟹ ((X⇩1 ×⇩L Y⇩1) ;⇩L (X⇩2 +⇩L Y⇩2)) = (X⇩1 ;⇩L X⇩2) +⇩L (Y⇩1 ;⇩L Y⇩2)"
  by (auto simp add: lens_comp_def lens_plus_def lens_prod_def prod.case_eq_if fun_eq_iff)

text ‹The following laws about quotient are similar to their arithmetic analogues. Lens quotient 
  reverse the effect of a composition.›

lemma lens_comp_quotient:
  "weak_lens Y ⟹ (X ;⇩L Y) /⇩L Y = X"
  by (simp add: lens_quotient_def lens_comp_def)
    
lemma lens_quotient_id [simp]: "weak_lens X ⟹ (X /⇩L X) = 1⇩L"
  by (force simp add: lens_quotient_def id_lens_def)

lemma lens_quotient_id_denom: "X /⇩L 1⇩L = X"
  by (simp add: lens_quotient_def id_lens_def lens_create_def)

lemma lens_quotient_unit: "weak_lens X ⟹ (0⇩L /⇩L X) = 0⇩L"
  by (simp add: lens_quotient_def zero_lens_def)

lemma lens_obs_eq_zero: "s⇩1 ≃⇘0⇩L⇙ s⇩2 = (s⇩1 = s⇩2)"
  by (simp add: lens_defs)

lemma lens_obs_eq_one: "s⇩1 ≃⇘1⇩L⇙ s⇩2"
  by (simp add: lens_defs)

lemma lens_obs_eq_as_override: "vwb_lens X ⟹ s⇩1 ≃⇘X⇙ s⇩2 ⟷ (s⇩2 = s⇩1 ⊕⇩L s⇩2 on X)"
  by (auto simp add: lens_defs; metis vwb_lens.put_eq)

end