Quelle  Lens_Algebra.thy

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 ∘ 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 get
                              , lens_put = λ (u, v) (x, y). (put u x, put 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_L (x, y) = x"
  by (simp add: fst_lens_def)

lemma get_snd_lens [simp]: "get_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 (create σ)
                       , lens_put = λ σ v. get (put (create σ) 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, lens_put = λ σ. get )"

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: "S_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: "S_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 ] ==> S _{;L y} = {s ∈ S. get s ∈ S}"
  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 "S _{+L y} = S ∩ S"
  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 σ" 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 σ" 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 σ" 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₁ ⋈ X₂; Y₁ ⋈ Y₂ ] ==> X₁ ×_L Y₁ ⋈ X₂ ×_L Y₂"
  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₂ ⋈ Y₂ ==> ((X₁ ×_L Y₁) ;_L (X₂ +_L Y₂)) = (X₁ ;_L X₂) +_L (Y₁ ;_L Y₂)"
  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₁ ≃_L s₂ = (s₁ = s₂)"
  by (simp add: lens_defs)

lemma lens_obs_eq_one: "s₁ ≃_L s₂"
  by (simp add: lens_defs)

lemma lens_obs_eq_as_override: "vwb_lens X ==> s₁ ≃ s₂ ⟷ (s₂ = s₁ ⊕_L s₂ on X)"
  by (auto simp add: lens_defs; metis vwb_lens.put_eq)

end