Theory Lens_Record_Example

theory Lens_Record_Example
  imports Optics
begin

text ‹The alphabet command supports syntax illustrated in the following comments.›

alphabet mylens =
  x :: nat
  y :: string

thm base_more_bij_lens
thm indeps
thm equivs
thm sublenses
thm quotients
thm compositions
thm lens

lemma mylens_composition: 
  "x +⇩L y +⇩L more⇩L ≈⇩L 1⇩L" (is "?P ≈⇩L ?Q")
proof -
  have "?Q ≈⇩L base⇩L +⇩L more⇩L"
    by (simp add: lens_equiv_sym)
  also have "... ≈⇩L (x +⇩L y) +⇩L more⇩L"
    by (simp add: lens_plus_eq_left)
  also have "... ≈⇩L x +⇩L y +⇩L more⇩L"
    by (simp add: lens_plus_assoc)
  finally show ?thesis
    using lens_equiv_sym
    by blast 
qed

lemma mylens_bij_lens:
  "bij_lens (x +⇩L y +⇩L more⇩L)"
  using bij_lens_equiv_id mylens_composition by auto

alphabet mylens_2 = mylens +
  z :: int
  k :: "string list"

thm base_more_bij_lens
thm bij_lenses
thm indeps
thm equivs
thm sublenses

alphabet mylens_3 = mylens_2 +
  n :: real
  h :: nat

thm base_more_bij_lens
thm indeps
thm equivs
thm sublenses

alphabet 't::monoid_add mylens_4 = 
  mn :: "'t"

end