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