19 text \<open> |
19 text \<open> |
20 Apart many other things, above record declaration produces the |
20 Apart many other things, above record declaration produces the |
21 following theorems: |
21 following theorems: |
22 \<close> |
22 \<close> |
23 |
23 |
24 |
|
25 thm point.simps |
24 thm point.simps |
26 thm point.iffs |
25 thm point.iffs |
27 thm point.defs |
26 thm point.defs |
28 |
27 |
29 text \<open> |
28 text \<open> |
30 The set of theorems @{thm [source] point.simps} is added |
29 The set of theorems @{thm [source] point.simps} is added |
31 automatically to the standard simpset, @{thm [source] point.iffs} is |
30 automatically to the standard simpset, @{thm [source] point.iffs} is |
32 added to the Classical Reasoner and Simplifier context. |
31 added to the Classical Reasoner and Simplifier context. |
33 |
32 |
34 \medskip Record declarations define new types and type abbreviations: |
33 \<^medskip> Record declarations define new types and type abbreviations: |
35 @{text [display] |
34 @{text [display] |
36 \<open>point = \<lparr>xpos :: nat, ypos :: nat\<rparr> = () point_ext_type |
35 \<open>point = \<lparr>xpos :: nat, ypos :: nat\<rparr> = () point_ext_type |
37 'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr> = 'a point_ext_type\<close>} |
36 'a point_scheme = \<lparr>xpos :: nat, ypos :: nat, ... :: 'a\<rparr> = 'a point_ext_type\<close>} |
38 \<close> |
37 \<close> |
39 |
38 |
40 consts foo2 :: "(| xpos :: nat, ypos :: nat |)" |
39 consts foo2 :: "\<lparr>xpos :: nat, ypos :: nat\<rparr>" |
41 consts foo4 :: "'a => (| xpos :: nat, ypos :: nat, ... :: 'a |)" |
40 consts foo4 :: "'a \<Rightarrow> \<lparr>xpos :: nat, ypos :: nat, \<dots> :: 'a\<rparr>" |
42 |
41 |
43 |
42 |
44 subsubsection \<open>Introducing concrete records and record schemes\<close> |
43 subsubsection \<open>Introducing concrete records and record schemes\<close> |
45 |
44 |
46 definition foo1 :: point |
45 definition foo1 :: point |
47 where "foo1 = (| xpos = 1, ypos = 0 |)" |
46 where "foo1 = \<lparr>xpos = 1, ypos = 0\<rparr>" |
48 |
47 |
49 definition foo3 :: "'a => 'a point_scheme" |
48 definition foo3 :: "'a \<Rightarrow> 'a point_scheme" |
50 where "foo3 ext = (| xpos = 1, ypos = 0, ... = ext |)" |
49 where "foo3 ext = \<lparr>xpos = 1, ypos = 0, \<dots> = ext\<rparr>" |
51 |
50 |
52 |
51 |
53 subsubsection \<open>Record selection and record update\<close> |
52 subsubsection \<open>Record selection and record update\<close> |
54 |
53 |
55 definition getX :: "'a point_scheme => nat" |
54 definition getX :: "'a point_scheme \<Rightarrow> nat" |
56 where "getX r = xpos r" |
55 where "getX r = xpos r" |
57 |
56 |
58 definition setX :: "'a point_scheme => nat => 'a point_scheme" |
57 definition setX :: "'a point_scheme \<Rightarrow> nat \<Rightarrow> 'a point_scheme" |
59 where "setX r n = r (| xpos := n |)" |
58 where "setX r n = r \<lparr>xpos := n\<rparr>" |
60 |
59 |
61 |
60 |
62 subsubsection \<open>Some lemmas about records\<close> |
61 subsubsection \<open>Some lemmas about records\<close> |
63 |
62 |
64 text \<open>Basic simplifications.\<close> |
63 text \<open>Basic simplifications.\<close> |
65 |
64 |
66 lemma "point.make n p = (| xpos = n, ypos = p |)" |
65 lemma "point.make n p = \<lparr>xpos = n, ypos = p\<rparr>" |
67 by (simp only: point.make_def) |
66 by (simp only: point.make_def) |
68 |
67 |
69 lemma "xpos (| xpos = m, ypos = n, ... = p |) = m" |
68 lemma "xpos \<lparr>xpos = m, ypos = n, \<dots> = p\<rparr> = m" |
70 by simp |
69 by simp |
71 |
70 |
72 lemma "(| xpos = m, ypos = n, ... = p |) (| xpos:= 0 |) = (| xpos = 0, ypos = n, ... = p |)" |
71 lemma "\<lparr>xpos = m, ypos = n, \<dots> = p\<rparr>\<lparr>xpos:= 0\<rparr> = \<lparr>xpos = 0, ypos = n, \<dots> = p\<rparr>" |
73 by simp |
72 by simp |
74 |
73 |
75 |
74 |
76 text \<open>\medskip Equality of records.\<close> |
75 text \<open>\<^medskip> Equality of records.\<close> |
77 |
76 |
78 lemma "n = n' ==> p = p' ==> (| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |)" |
77 lemma "n = n' \<Longrightarrow> p = p' \<Longrightarrow> \<lparr>xpos = n, ypos = p\<rparr> = \<lparr>xpos = n', ypos = p'\<rparr>" |
79 \<comment> \<open>introduction of concrete record equality\<close> |
78 \<comment> \<open>introduction of concrete record equality\<close> |
80 by simp |
79 by simp |
81 |
80 |
82 lemma "(| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |) ==> n = n'" |
81 lemma "\<lparr>xpos = n, ypos = p\<rparr> = \<lparr>xpos = n', ypos = p'\<rparr> \<Longrightarrow> n = n'" |
83 \<comment> \<open>elimination of concrete record equality\<close> |
82 \<comment> \<open>elimination of concrete record equality\<close> |
84 by simp |
83 by simp |
85 |
84 |
86 lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)" |
85 lemma "r\<lparr>xpos := n\<rparr>\<lparr>ypos := m\<rparr> = r\<lparr>ypos := m\<rparr>\<lparr>xpos := n\<rparr>" |
87 \<comment> \<open>introduction of abstract record equality\<close> |
86 \<comment> \<open>introduction of abstract record equality\<close> |
88 by simp |
87 by simp |
89 |
88 |
90 lemma "r (| xpos := n |) = r (| xpos := n' |) ==> n = n'" |
89 lemma "r\<lparr>xpos := n\<rparr> = r\<lparr>xpos := n'\<rparr>" if "n = n'" |
91 \<comment> \<open>elimination of abstract record equality (manual proof)\<close> |
90 \<comment> \<open>elimination of abstract record equality (manual proof)\<close> |
92 proof - |
91 proof - |
93 assume "r (| xpos := n |) = r (| xpos := n' |)" (is "?lhs = ?rhs") |
92 let "?lhs = ?rhs" = ?thesis |
94 then have "xpos ?lhs = xpos ?rhs" by simp |
93 from that have "xpos ?lhs = xpos ?rhs" by simp |
95 then show ?thesis by simp |
94 then show ?thesis by simp |
96 qed |
95 qed |
97 |
96 |
98 |
97 |
99 text \<open>\medskip Surjective pairing\<close> |
98 text \<open>\<^medskip> Surjective pairing\<close> |
100 |
99 |
101 lemma "r = (| xpos = xpos r, ypos = ypos r |)" |
100 lemma "r = \<lparr>xpos = xpos r, ypos = ypos r\<rparr>" |
102 by simp |
101 by simp |
103 |
102 |
104 lemma "r = (| xpos = xpos r, ypos = ypos r, ... = point.more r |)" |
103 lemma "r = \<lparr>xpos = xpos r, ypos = ypos r, \<dots> = point.more r\<rparr>" |
105 by simp |
104 by simp |
106 |
105 |
107 |
106 |
108 text \<open> |
107 text \<open>\<^medskip> Representation of records by cases or (degenerate) induction.\<close> |
109 \medskip Representation of records by cases or (degenerate) |
108 |
110 induction. |
109 lemma "r\<lparr>xpos := n\<rparr>\<lparr>ypos := m\<rparr> = r\<lparr>ypos := m\<rparr>\<lparr>xpos := n\<rparr>" |
111 \<close> |
|
112 |
|
113 lemma "r(| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)" |
|
114 proof (cases r) |
|
115 fix xpos ypos more |
|
116 assume "r = (| xpos = xpos, ypos = ypos, ... = more |)" |
|
117 then show ?thesis by simp |
|
118 qed |
|
119 |
|
120 lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)" |
|
121 proof (induct r) |
|
122 fix xpos ypos more |
|
123 show "(| xpos = xpos, ypos = ypos, ... = more |) (| xpos := n, ypos := m |) = |
|
124 (| xpos = xpos, ypos = ypos, ... = more |) (| ypos := m, xpos := n |)" |
|
125 by simp |
|
126 qed |
|
127 |
|
128 lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)" |
|
129 proof (cases r) |
110 proof (cases r) |
130 fix xpos ypos more |
111 fix xpos ypos more |
131 assume "r = \<lparr>xpos = xpos, ypos = ypos, \<dots> = more\<rparr>" |
112 assume "r = \<lparr>xpos = xpos, ypos = ypos, \<dots> = more\<rparr>" |
132 then show ?thesis by simp |
113 then show ?thesis by simp |
133 qed |
114 qed |
134 |
115 |
135 lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)" |
116 lemma "r\<lparr>xpos := n\<rparr>\<lparr>ypos := m\<rparr> = r\<lparr>ypos := m\<rparr>\<lparr>xpos := n\<rparr>" |
|
117 proof (induct r) |
|
118 fix xpos ypos more |
|
119 show "\<lparr>xpos = xpos, ypos = ypos, \<dots> = more\<rparr>\<lparr>xpos := n, ypos := m\<rparr> = |
|
120 \<lparr>xpos = xpos, ypos = ypos, \<dots> = more\<rparr>\<lparr>ypos := m, xpos := n\<rparr>" |
|
121 by simp |
|
122 qed |
|
123 |
|
124 lemma "r\<lparr>xpos := n\<rparr>\<lparr>xpos := m\<rparr> = r\<lparr>xpos := m\<rparr>" |
|
125 proof (cases r) |
|
126 fix xpos ypos more |
|
127 assume "r = \<lparr>xpos = xpos, ypos = ypos, \<dots> = more\<rparr>" |
|
128 then show ?thesis by simp |
|
129 qed |
|
130 |
|
131 lemma "r\<lparr>xpos := n\<rparr>\<lparr>xpos := m\<rparr> = r\<lparr>xpos := m\<rparr>" |
136 proof (cases r) |
132 proof (cases r) |
137 case fields |
133 case fields |
138 then show ?thesis by simp |
134 then show ?thesis by simp |
139 qed |
135 qed |
140 |
136 |
141 lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)" |
137 lemma "r\<lparr>xpos := n\<rparr>\<lparr>xpos := m\<rparr> = r\<lparr>xpos := m\<rparr>" |
142 by (cases r) simp |
138 by (cases r) simp |
143 |
139 |
144 |
140 |
145 text \<open> |
141 text \<open>\<^medskip> Concrete records are type instances of record schemes.\<close> |
146 \medskip Concrete records are type instances of record schemes. |
|
147 \<close> |
|
148 |
142 |
149 definition foo5 :: nat |
143 definition foo5 :: nat |
150 where "foo5 = getX (| xpos = 1, ypos = 0 |)" |
144 where "foo5 = getX \<lparr>xpos = 1, ypos = 0\<rparr>" |
151 |
145 |
152 |
146 |
153 text \<open>\medskip Manipulating the ``\<open>...\<close>'' (more) part.\<close> |
147 text \<open>\<^medskip> Manipulating the ``\<open>...\<close>'' (more) part.\<close> |
154 |
148 |
155 definition incX :: "'a point_scheme => 'a point_scheme" |
149 definition incX :: "'a point_scheme \<Rightarrow> 'a point_scheme" |
156 where "incX r = (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)" |
150 where "incX r = \<lparr>xpos = xpos r + 1, ypos = ypos r, \<dots> = point.more r\<rparr>" |
157 |
151 |
158 lemma "incX r = setX r (Suc (getX r))" |
152 lemma "incX r = setX r (Suc (getX r))" |
159 by (simp add: getX_def setX_def incX_def) |
153 by (simp add: getX_def setX_def incX_def) |
160 |
154 |
161 |
155 |
162 text \<open>An alternative definition.\<close> |
156 text \<open>\<^medskip> An alternative definition.\<close> |
163 |
157 |
164 definition incX' :: "'a point_scheme => 'a point_scheme" |
158 definition incX' :: "'a point_scheme \<Rightarrow> 'a point_scheme" |
165 where "incX' r = r (| xpos := xpos r + 1 |)" |
159 where "incX' r = r\<lparr>xpos := xpos r + 1\<rparr>" |
166 |
160 |
167 |
161 |
168 subsection \<open>Coloured points: record extension\<close> |
162 subsection \<open>Coloured points: record extension\<close> |
169 |
163 |
170 datatype colour = Red | Green | Blue |
164 datatype colour = Red | Green | Blue |
174 |
168 |
175 |
169 |
176 text \<open> |
170 text \<open> |
177 The record declaration defines a new type constructor and abbreviations: |
171 The record declaration defines a new type constructor and abbreviations: |
178 @{text [display] |
172 @{text [display] |
179 \<open>cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) = |
173 \<open>cpoint = \<lparr>xpos :: nat, ypos :: nat, colour :: colour\<rparr> = |
180 () cpoint_ext_type point_ext_type |
174 () cpoint_ext_type point_ext_type |
181 'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |) = |
175 'a cpoint_scheme = \<lparr>xpos :: nat, ypos :: nat, colour :: colour, \<dots> :: 'a\<rparr> = |
182 'a cpoint_ext_type point_ext_type\<close>} |
176 'a cpoint_ext_type point_ext_type\<close>} |
183 \<close> |
177 \<close> |
184 |
178 |
185 consts foo6 :: cpoint |
179 consts foo6 :: cpoint |
186 consts foo7 :: "(| xpos :: nat, ypos :: nat, colour :: colour |)" |
180 consts foo7 :: "\<lparr>xpos :: nat, ypos :: nat, colour :: colour\<rparr>" |
187 consts foo8 :: "'a cpoint_scheme" |
181 consts foo8 :: "'a cpoint_scheme" |
188 consts foo9 :: "(| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |)" |
182 consts foo9 :: "\<lparr>xpos :: nat, ypos :: nat, colour :: colour, \<dots> :: 'a\<rparr>" |
189 |
183 |
190 |
184 |
191 text \<open> |
185 text \<open>Functions on \<open>point\<close> schemes work for \<open>cpoints\<close> as well.\<close> |
192 Functions on \<open>point\<close> schemes work for \<open>cpoints\<close> as well. |
|
193 \<close> |
|
194 |
186 |
195 definition foo10 :: nat |
187 definition foo10 :: nat |
196 where "foo10 = getX (| xpos = 2, ypos = 0, colour = Blue |)" |
188 where "foo10 = getX \<lparr>xpos = 2, ypos = 0, colour = Blue\<rparr>" |
197 |
189 |
198 |
190 |
199 subsubsection \<open>Non-coercive structural subtyping\<close> |
191 subsubsection \<open>Non-coercive structural subtyping\<close> |
200 |
192 |
201 text \<open> |
193 text \<open>Term \<^term>\<open>foo11\<close> has type \<^typ>\<open>cpoint\<close>, not type \<^typ>\<open>point\<close> --- Great!\<close> |
202 Term \<^term>\<open>foo11\<close> has type \<^typ>\<open>cpoint\<close>, not type \<^typ>\<open>point\<close> --- |
|
203 Great! |
|
204 \<close> |
|
205 |
194 |
206 definition foo11 :: cpoint |
195 definition foo11 :: cpoint |
207 where "foo11 = setX (| xpos = 2, ypos = 0, colour = Blue |) 0" |
196 where "foo11 = setX \<lparr>xpos = 2, ypos = 0, colour = Blue\<rparr> 0" |
208 |
197 |
209 |
198 |
210 subsection \<open>Other features\<close> |
199 subsection \<open>Other features\<close> |
211 |
200 |
212 text \<open>Field names contribute to record identity.\<close> |
201 text \<open>Field names contribute to record identity.\<close> |
214 record point' = |
203 record point' = |
215 xpos' :: nat |
204 xpos' :: nat |
216 ypos' :: nat |
205 ypos' :: nat |
217 |
206 |
218 text \<open> |
207 text \<open> |
219 \noindent May not apply \<^term>\<open>getX\<close> to @{term [source] "(| xpos' = |
208 \<^noindent> May not apply \<^term>\<open>getX\<close> to @{term [source] "\<lparr>xpos' = 2, ypos' = 0\<rparr>"} |
220 2, ypos' = 0 |)"} -- type error. |
209 --- type error. |
221 \<close> |
210 \<close> |
222 |
211 |
223 text \<open>\medskip Polymorphic records.\<close> |
212 text \<open>\<^medskip> Polymorphic records.\<close> |
224 |
213 |
225 record 'a point'' = point + |
214 record 'a point'' = point + |
226 content :: 'a |
215 content :: 'a |
227 |
216 |
228 type_synonym cpoint'' = "colour point''" |
217 type_synonym cpoint'' = "colour point''" |
229 |
218 |
230 |
219 |
231 |
|
232 text \<open>Updating a record field with an identical value is simplified.\<close> |
220 text \<open>Updating a record field with an identical value is simplified.\<close> |
233 lemma "r (| xpos := xpos r |) = r" |
221 lemma "r\<lparr>xpos := xpos r\<rparr> = r" |
234 by simp |
222 by simp |
235 |
223 |
236 text \<open>Only the most recent update to a component survives simplification.\<close> |
224 text \<open>Only the most recent update to a component survives simplification.\<close> |
237 lemma "r (| xpos := x, ypos := y, xpos := x' |) = r (| ypos := y, xpos := x' |)" |
225 lemma "r\<lparr>xpos := x, ypos := y, xpos := x'\<rparr> = r\<lparr>ypos := y, xpos := x'\<rparr>" |
238 by simp |
226 by simp |
239 |
227 |
240 text \<open>In some cases its convenient to automatically split |
228 text \<open> |
241 (quantified) records. For this purpose there is the simproc @{ML [source] |
229 In some cases its convenient to automatically split (quantified) records. |
242 "Record.split_simproc"} and the tactic @{ML [source] |
230 For this purpose there is the simproc @{ML [source] "Record.split_simproc"} |
243 "Record.split_simp_tac"}. The simplification procedure |
231 and the tactic @{ML [source] "Record.split_simp_tac"}. The simplification |
244 only splits the records, whereas the tactic also simplifies the |
232 procedure only splits the records, whereas the tactic also simplifies the |
245 resulting goal with the standard record simplification rules. A |
233 resulting goal with the standard record simplification rules. A |
246 (generalized) predicate on the record is passed as parameter that |
234 (generalized) predicate on the record is passed as parameter that decides |
247 decides whether or how `deep' to split the record. It can peek on the |
235 whether or how `deep' to split the record. It can peek on the subterm |
248 subterm starting at the quantified occurrence of the record (including |
236 starting at the quantified occurrence of the record (including the |
249 the quantifier). The value \<^ML>\<open>0\<close> indicates no split, a value |
237 quantifier). The value \<^ML>\<open>0\<close> indicates no split, a value greater |
250 greater \<^ML>\<open>0\<close> splits up to the given bound of record extension and |
238 \<^ML>\<open>0\<close> splits up to the given bound of record extension and finally the |
251 finally the value \<^ML>\<open>~1\<close> completely splits the record. |
239 value \<^ML>\<open>~1\<close> completely splits the record. @{ML [source] |
252 @{ML [source] "Record.split_simp_tac"} additionally takes a list of |
240 "Record.split_simp_tac"} additionally takes a list of equations for |
253 equations for simplification and can also split fixed record variables. |
241 simplification and can also split fixed record variables. |
254 |
|
255 \<close> |
242 \<close> |
256 |
243 |
257 lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)" |
244 lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)" |
258 apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context> |
245 apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context> |
259 addsimprocs [Record.split_simproc (K ~1)]) 1\<close>) |
246 addsimprocs [Record.split_simproc (K ~1)]) 1\<close>) |