Optics/Lens_Record_Example.thy at main · isabelle-utp/Optics · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
theory Lens_Record_Example
  imports Optics
begin

text \<open>The alphabet command supports syntax illustrated in the following comments.\<close>

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 +\<^sub>L y +\<^sub>L more\<^sub>L \<approx>\<^sub>L 1\<^sub>L" (is "?P \<approx>\<^sub>L ?Q")
proof -
  have "?Q \<approx>\<^sub>L base\<^sub>L +\<^sub>L more\<^sub>L"
    by (simp add: lens_equiv_sym)
  also have "... \<approx>\<^sub>L (x +\<^sub>L y) +\<^sub>L more\<^sub>L"
    by (simp add: lens_plus_eq_left)
  also have "... \<approx>\<^sub>L x +\<^sub>L y +\<^sub>L more\<^sub>L"
    by (simp add: lens_plus_assoc)
  finally show ?thesis
    using lens_equiv_sym
    by blast
qed

lemma mylens_bij_lens:
  "bij_lens (x +\<^sub>L y +\<^sub>L more\<^sub>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