Theory Optics.Lens_Symmetric

section ‹ Symmetric Lenses ›

theory Lens_Symmetric
  imports Lens_Order
begin

text ‹ A characterisation of Hofmann's ``Symmetric Lenses''~cite"Hofmann2011", where
  a lens is accompanied by its complement. ›

record ('a, 'b, 's) slens = 
  view   :: "'a  's" ("𝒱ı") ― ‹ The region characterised ›
  coview :: "'b  's" ("𝒞ı") ― ‹ The complement of the region ›

type_notation
  slens ("<_, _>  _" [0, 0, 0] 0)

declare slens.defs [lens_defs]

definition slens_compl :: "(<'a, 'c>  'b)  <'c, 'a>  'b" ("-L _" [81] 80) where
[lens_defs]: "slens_compl a =  view = coview a, coview = view a "

lemma view_slens_compl [simp]: "𝒱-L a=  𝒞a⇙"
  by (simp add: slens_compl_def)

lemma coview_slens_compl [simp]: "𝒞-L a=  𝒱a⇙"
  by (simp add: slens_compl_def)

subsection ‹ Partial Symmetric Lenses ›

locale psym_lens =
  fixes S :: "<'a, 'b>  's" (structure)
  assumes 
    mwb_region [simp]: "mwb_lens 𝒱" and
    mwb_coregion [simp]: "mwb_lens 𝒞" and
    indep_region_coregion [simp]: "𝒱  𝒞" and
    pbij_region_coregion [simp]: "pbij_lens (𝒱 +L 𝒞)"

declare psym_lens.mwb_region [simp]
declare psym_lens.mwb_coregion [simp]
declare psym_lens.indep_region_coregion [simp]

lemma psym_lens_compl [simp]: "psym_lens a  psym_lens (-L a)"
  apply (simp add: slens_compl_def)
  apply (rule psym_lens.intro)
  apply (simp_all)
  using lens_indep_sym psym_lens.indep_region_coregion apply blast
  using lens_indep_sym pbij_plus_commute psym_lens_def apply blast
  done

subsection ‹ Symmetric Lenses ›

locale sym_lens =
  fixes S :: "<'a, 'b>  's" (structure)
  assumes 
    vwb_region: "vwb_lens 𝒱" and
    vwb_coregion: "vwb_lens 𝒞" and
    indep_region_coregion: "𝒱  𝒞" and
    bij_region_coregion: "bij_lens (𝒱 +L 𝒞)"
begin

sublocale psym_lens
proof (rule psym_lens.intro)
  show "mwb_lens 𝒱"
    by (simp add: vwb_region)
  show "mwb_lens 𝒞"
    by (simp add: vwb_coregion)
  show "𝒱  𝒞"
    using indep_region_coregion by blast
  show "pbij_lens (𝒱 +L 𝒞)"
    by (simp add: bij_region_coregion)
qed

lemma put_region_coregion_cover:
  "put𝒱(put𝒞s1 (get𝒞s2)) (get𝒱s2) = s2"
proof -
  have "put𝒱(put𝒞s1 (get𝒞s2)) (get𝒱s2) = put𝒱 +L 𝒞s1 (get𝒱 +L 𝒞s2)"
    by (simp add: lens_defs)
  also have "... = s2"
    by (simp add: bij_region_coregion)
  finally show ?thesis .
qed

end

declare sym_lens.vwb_region [simp]
declare sym_lens.vwb_coregion [simp]
declare sym_lens.indep_region_coregion [simp]

lemma sym_lens_psym [simp]: "sym_lens x  psym_lens x"
  by (simp add: psym_lens_def sym_lens.bij_region_coregion)

lemma sym_lens_compl [simp]: "sym_lens a  sym_lens (-L a)"
  apply (simp add: slens_compl_def)
  apply (rule sym_lens.intro, simp_all)
  using lens_indep_sym sym_lens.indep_region_coregion apply blast
  using bij_lens_equiv lens_plus_comm sym_lens_def apply blast
  done

end