9 theory Records = Main: |
9 theory Records = Main: |
10 |
10 |
11 subsection {* Points *} |
11 subsection {* Points *} |
12 |
12 |
13 record point = |
13 record point = |
14 x :: nat |
14 xpos :: nat |
15 y :: nat |
15 ypos :: nat |
16 |
16 |
17 text {* |
17 text {* |
18 Apart many other things, above record declaration produces the |
18 Apart many other things, above record declaration produces the |
19 following theorems: |
19 following theorems: |
20 *} |
20 *} |
21 |
21 |
22 thm "point.simps" |
22 thm "point.simps" |
23 thm "point.iffs" |
23 thm "point.iffs" |
24 thm "point.update_defs" |
24 thm "point.derived_defs" |
25 |
25 |
26 text {* |
26 text {* |
27 The set of theorems @{thm [source] point.simps} is added |
27 The set of theorems @{thm [source] point.simps} is added |
28 automatically to the standard simpset, @{thm [source] point.iffs} is |
28 automatically to the standard simpset, @{thm [source] point.iffs} is |
29 added to the Classical Reasoner and Simplifier context. |
29 added to the Classical Reasoner and Simplifier context. |
30 *} |
30 |
31 |
31 \medskip Record declarations define new type abbreviations: |
32 text {* |
|
33 Record declarations define new type abbreviations: |
|
34 @{text [display] |
32 @{text [display] |
35 " point = (| x :: nat, y :: nat |) |
33 " point = (| xpos :: nat, ypos :: nat |) |
36 'a point_scheme = (| x :: nat, y :: nat, ... :: 'a |)"} |
34 'a point_scheme = (| xpos :: nat, ypos :: nat, ... :: 'a |)"} |
37 Extensions `...' must be in type class @{text more}. |
|
38 *} |
35 *} |
39 |
36 |
40 consts foo1 :: point |
37 consts foo1 :: point |
41 consts foo2 :: "(| x :: nat, y :: nat |)" |
38 consts foo2 :: "(| xpos :: nat, ypos :: nat |)" |
42 consts foo3 :: "'a => ('a::more) point_scheme" |
39 consts foo3 :: "'a => 'a point_scheme" |
43 consts foo4 :: "'a => (| x :: nat, y :: nat, ... :: 'a |)" |
40 consts foo4 :: "'a => (| xpos :: nat, ypos :: nat, ... :: 'a |)" |
44 |
41 |
45 |
42 |
46 subsubsection {* Introducing concrete records and record schemes *} |
43 subsubsection {* Introducing concrete records and record schemes *} |
47 |
44 |
48 defs |
45 defs |
49 foo1_def: "foo1 == (| x = 1, y = 0 |)" |
46 foo1_def: "foo1 == (| xpos = 1, ypos = 0 |)" |
50 foo3_def: "foo3 ext == (| x = 1, y = 0, ... = ext |)" |
47 foo3_def: "foo3 ext == (| xpos = 1, ypos = 0, ... = ext |)" |
51 |
48 |
52 |
49 |
53 subsubsection {* Record selection and record update *} |
50 subsubsection {* Record selection and record update *} |
54 |
51 |
55 constdefs |
52 constdefs |
56 getX :: "('a::more) point_scheme => nat" |
53 getX :: "'a point_scheme => nat" |
57 "getX r == x r" |
54 "getX r == xpos r" |
58 setX :: "('a::more) point_scheme => nat => 'a point_scheme" |
55 setX :: "'a point_scheme => nat => 'a point_scheme" |
59 "setX r n == r (| x := n |)" |
56 "setX r n == r (| xpos := n |)" |
60 |
57 |
61 |
58 |
62 subsubsection {* Some lemmas about records *} |
59 subsubsection {* Some lemmas about records *} |
63 |
60 |
64 text {* Basic simplifications. *} |
61 text {* Basic simplifications. *} |
65 |
62 |
66 lemma "point.make n p = (| x = n, y = p |)" |
63 lemma "point.make n p = (| xpos = n, ypos = p |)" |
67 by (simp add: point.make_def) |
64 by (simp only: point.make_def) |
68 |
65 |
69 lemma "x (| x = m, y = n, ... = p |) = m" |
66 lemma "xpos (| xpos = m, ypos = n, ... = p |) = m" |
70 by simp |
67 by simp |
71 |
68 |
72 lemma "(| x = m, y = n, ... = p |) (| x:= 0 |) = (| x = 0, y = n, ... = p |)" |
69 lemma "(| xpos = m, ypos = n, ... = p |) (| xpos:= 0 |) = (| xpos = 0, ypos = n, ... = p |)" |
73 by simp |
70 by simp |
74 |
71 |
75 |
72 |
76 text {* \medskip Equality of records. *} |
73 text {* \medskip Equality of records. *} |
77 |
74 |
78 lemma "n = n' ==> p = p' ==> (| x = n, y = p |) = (| x = n', y = p' |)" |
75 lemma "n = n' ==> p = p' ==> (| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |)" |
79 -- "introduction of concrete record equality" |
76 -- "introduction of concrete record equality" |
80 by simp |
77 by simp |
81 |
78 |
82 lemma "(| x = n, y = p |) = (| x = n', y = p' |) ==> n = n'" |
79 lemma "(| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |) ==> n = n'" |
83 -- "elimination of concrete record equality" |
80 -- "elimination of concrete record equality" |
84 by simp |
81 by simp |
85 |
82 |
86 lemma "r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)" |
83 lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)" |
87 -- "introduction of abstract record equality" |
84 -- "introduction of abstract record equality" |
88 by simp |
85 by simp |
89 |
86 |
90 lemma "r (| x := n |) = r (| x := n' |) ==> n = n'" |
87 lemma "r (| xpos := n |) = r (| xpos := n' |) ==> n = n'" |
91 -- "elimination of abstract record equality (manual proof)" |
88 -- "elimination of abstract record equality (manual proof)" |
92 proof - |
89 proof - |
93 assume "r (| x := n |) = r (| x := n' |)" (is "?lhs = ?rhs") |
90 assume "r (| xpos := n |) = r (| xpos := n' |)" (is "?lhs = ?rhs") |
94 hence "x ?lhs = x ?rhs" by simp |
91 hence "xpos ?lhs = xpos ?rhs" by simp |
95 thus ?thesis by simp |
92 thus ?thesis by simp |
96 qed |
93 qed |
97 |
94 |
98 |
95 |
99 text {* \medskip Surjective pairing *} |
96 text {* \medskip Surjective pairing *} |
100 |
97 |
101 lemma "r = (| x = x r, y = y r |)" |
98 lemma "r = (| xpos = xpos r, ypos = ypos r |)" |
102 by simp |
99 by simp |
103 |
100 |
104 lemma "r = (| x = x r, y = y r, ... = more r |)" |
101 lemma "r = (| xpos = xpos r, ypos = ypos r, ... = more r |)" |
105 by simp |
102 by simp |
106 |
103 |
107 |
104 |
108 text {* |
105 text {* |
109 \medskip Splitting quantifiers: the @{text "!!r"} is \emph{necessary} |
106 \medskip Representation of records by cases or (degenerate) |
110 here! |
107 induction. |
111 *} |
108 *} |
112 |
109 |
113 lemma "!!r. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)" |
110 lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)" |
114 proof record_split |
111 proof (cases r) |
115 fix x y more |
112 fix xpos ypos more |
116 show "(| x = x, y = y, ... = more |)(| x := n, y := m |) = |
113 assume "r = (| xpos = xpos, ypos = ypos, ... = more |)" |
117 (| x = x, y = y, ... = more |)(| y := m, x := n |)" |
114 thus ?thesis by simp |
|
115 qed |
|
116 |
|
117 lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)" |
|
118 proof (induct r) |
|
119 fix xpos ypos more |
|
120 show "(| xpos = xpos, ypos = ypos, ... = more |) (| xpos := n, ypos := m |) = |
|
121 (| xpos = xpos, ypos = ypos, ... = more |) (| ypos := m, xpos := n |)" |
118 by simp |
122 by simp |
119 qed |
123 qed |
120 |
124 |
121 lemma "!!r. r (| x := n |) (| x := m |) = r (| x := m |)" |
125 lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)" |
122 proof record_split |
126 proof (cases r) |
123 fix x y more |
127 fix xpos ypos more |
124 show "(| x = x, y = y, ... = more |)(| x := n, x := m |) = |
128 assume "r = \<lparr>xpos = xpos, ypos = ypos, \<dots> = more\<rparr>" |
125 (| x = x, y = y, ... = more |)(| x := m |)" |
129 thus ?thesis by simp |
126 by simp |
130 qed |
127 qed |
131 |
|
132 lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)" |
|
133 proof (cases r) |
|
134 case fields |
|
135 thus ?thesis by simp |
|
136 qed |
|
137 |
|
138 lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)" |
|
139 by (cases r) simp |
128 |
140 |
129 |
141 |
130 text {* |
142 text {* |
131 \medskip Concrete records are type instances of record schemes. |
143 \medskip Concrete records are type instances of record schemes. |
132 *} |
144 *} |
133 |
145 |
134 constdefs |
146 constdefs |
135 foo5 :: nat |
147 foo5 :: nat |
136 "foo5 == getX (| x = 1, y = 0 |)" |
148 "foo5 == getX (| xpos = 1, ypos = 0 |)" |
137 |
149 |
138 |
150 |
139 text {* \medskip Manipulating the `...' (more) part. *} |
151 text {* \medskip Manipulating the ``@{text "..."}'' (more) part. *} |
140 |
152 |
141 constdefs |
153 constdefs |
142 incX :: "('a::more) point_scheme => 'a point_scheme" |
154 incX :: "'a point_scheme => 'a point_scheme" |
143 "incX r == (| x = Suc (x r), y = y r, ... = point.more r |)" |
155 "incX r == (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)" |
144 |
156 |
145 lemma "!!r n. incX r = setX r (Suc (getX r))" |
157 lemma "incX r = setX r (Suc (getX r))" |
146 proof (unfold getX_def setX_def incX_def) |
158 by (simp add: getX_def setX_def incX_def) |
147 show "!!r n. (| x = Suc (x r), y = y r, ... = more r |) = r(| x := Suc (x r) |)" |
159 |
148 by record_split simp |
|
149 qed |
|
150 |
160 |
151 text {* An alternative definition. *} |
161 text {* An alternative definition. *} |
152 |
162 |
153 constdefs |
163 constdefs |
154 incX' :: "('a::more) point_scheme => 'a point_scheme" |
164 incX' :: "'a point_scheme => 'a point_scheme" |
155 "incX' r == r (| x := Suc (x r) |)" |
165 "incX' r == r (| xpos := xpos r + 1 |)" |
156 |
166 |
157 |
167 |
158 subsection {* Coloured points: record extension *} |
168 subsection {* Coloured points: record extension *} |
159 |
169 |
160 datatype colour = Red | Green | Blue |
170 datatype colour = Red | Green | Blue |