Quelle  Lens_Symmetric.thy

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" (‹V🍋›) ― ‹ The region characterised ›
  coview :: "'b ==> 's" (‹C🍋›) ― ‹ 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]: "V_{L a} = C"
  by (simp add: slens_compl_def)

lemma coview_slens_compl [simp]: "C_{L a} = V"
  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 V" and
    mwb_coregion [simp]: "mwb_lens C" and
    indep_region_coregion [simp]: "V ⋈ C" and
    pbij_region_coregion [simp]: "pbij_lens (V +_L C)"

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 V" and
    vwb_coregion: "vwb_lens C" and
    indep_region_coregion: "V ⋈ C" and
    bij_region_coregion: "bij_lens (V +_L C)"
begin

sublocale psym_lens
proof (rule psym_lens.intro)
  show "mwb_lens V"
    by (simp add: vwb_region)
  show "mwb_lens C"
    by (simp add: vwb_coregion)
  show "V ⋈ C"
    using indep_region_coregion by blast
  show "pbij_lens (V +_L C)"
    by (simp add: bij_region_coregion)
qed

lemma put_region_coregion_cover:
  "put_<V> (put_<C> s₁ (get_<C> s₂)) (get_<V> s₂) = s₂"
proof -
  have "put_<V> (put_<C> s₁ (get_<C> s₂)) (get_<V> s₂) = put_{<V> +L C} s₁ (get_{<V> +L C} s₂)"
    by (simp add: lens_defs)
  also have "... = s₂"
    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