90 fun mk_Pair (t1, t2) = |
90 fun mk_Pair (t1, t2) = |
91 let val T1 = fastype_of t1 |
91 let val T1 = fastype_of t1 |
92 and T2 = fastype_of t2 |
92 and T2 = fastype_of t2 |
93 in Const ("Pair", [T1, T2] ---> mk_prodT (T1,T2)) $ t1 $ t2 end; |
93 in Const ("Pair", [T1, T2] ---> mk_prodT (T1,T2)) $ t1 $ t2 end; |
94 |
94 |
|
95 val mk_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq; |
|
96 |
95 fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2) |
97 fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2) |
96 | dest_prodT T = raise TYPE ("dest_prodT: product type expected", [T], []); |
98 | dest_prodT T = raise TYPE ("dest_prodT: product type expected", [T], []); |
97 |
99 |
98 fun mk_fst pT = Const ("fst", pT --> fst (dest_prodT pT)); |
100 fun mk_fst pT = Const ("fst", pT --> fst (dest_prodT pT)); |
99 fun mk_snd pT = Const ("snd", pT --> snd (dest_prodT pT)); |
101 fun mk_snd pT = Const ("snd", pT --> snd (dest_prodT pT)); |
107 fun selT T recT = recT --> T; |
109 fun selT T recT = recT --> T; |
108 fun updateT T recT = T --> recT --> recT; |
110 fun updateT T recT = T --> recT --> recT; |
109 val base_free = Free o apfst base; |
111 val base_free = Free o apfst base; |
110 val make_scheme_name = "make_scheme"; |
112 val make_scheme_name = "make_scheme"; |
111 val make_name = "make"; |
113 val make_name = "make"; |
112 val update_suffix = "_update"; |
114 fun def_suffix s = s ^ "_def"; |
|
115 fun update_suffix s = s ^ "_update"; |
113 fun make_schemeC full make_schemeT = Const (full make_scheme_name, make_schemeT); |
116 fun make_schemeC full make_schemeT = Const (full make_scheme_name, make_schemeT); |
114 fun makeC full makeT = Const (full make_name, makeT); |
117 fun makeC full makeT = Const (full make_name, makeT); |
|
118 fun make_args_scheme full make_schemeT base_frees z = |
|
119 list_comb (make_schemeC full make_schemeT, base_frees) $ z; |
|
120 fun make_args full makeT base_frees = |
|
121 list_comb (makeC full makeT, base_frees); |
115 fun selC s T recT = Const (s, selT T recT); |
122 fun selC s T recT = Const (s, selT T recT); |
116 fun updateC full s T recT = Const (full (base s ^ update_suffix), updateT T recT); |
123 fun updateC s T recT = Const (update_suffix s, updateT T recT); |
117 fun frees xs = foldr add_typ_tfree_names (xs, []); |
124 fun frees xs = foldr add_typ_tfree_names (xs, []); |
118 |
125 |
119 |
126 |
120 |
127 |
121 (** constants, definitions, axioms **) |
128 (** constants, definitions, axioms **) |
125 fun decls make_schemeT makeT selT updateT recT current_fields = |
132 fun decls make_schemeT makeT selT updateT recT current_fields = |
126 let val make_scheme_decl = (make_scheme_name, make_schemeT, NoSyn); |
133 let val make_scheme_decl = (make_scheme_name, make_schemeT, NoSyn); |
127 val make_decl = (make_name, makeT, NoSyn); |
134 val make_decl = (make_name, makeT, NoSyn); |
128 val sel_decls = map (fn (c, T) => (c, selT T recT, NoSyn)) current_fields; |
135 val sel_decls = map (fn (c, T) => (c, selT T recT, NoSyn)) current_fields; |
129 val update_decls = |
136 val update_decls = |
130 map (fn (c, T) => (c ^ update_suffix, updateT T recT, NoSyn)) current_fields |
137 map (fn (c, T) => (update_suffix c, updateT T recT, NoSyn)) current_fields |
131 in |
138 in |
132 make_scheme_decl :: make_decl :: sel_decls @ update_decls |
139 make_scheme_decl :: make_decl :: sel_decls @ update_decls |
133 end; |
140 end; |
134 |
141 |
135 |
142 |
138 (*make*) |
145 (*make*) |
139 fun make_defs make_schemeT makeT base_frees z thy = |
146 fun make_defs make_schemeT makeT base_frees z thy = |
140 let |
147 let |
141 val sign = sign_of thy; |
148 val sign = sign_of thy; |
142 val full = Sign.full_name sign; |
149 val full = Sign.full_name sign; |
143 val make_args_scheme = list_comb (make_schemeC full make_schemeT, base_frees) $ z; |
|
144 val make_args = list_comb (makeC full makeT, base_frees); |
|
145 val make_scheme_def = |
150 val make_scheme_def = |
146 mk_defpair (make_args_scheme, foldr mk_Pair (base_frees, z)); |
151 mk_defpair (make_args_scheme full make_schemeT base_frees z, |
|
152 foldr mk_Pair (base_frees, z)); |
147 val make_def = |
153 val make_def = |
148 mk_defpair (make_args, foldr mk_Pair (base_frees, unit)) |
154 mk_defpair (make_args full makeT base_frees, |
|
155 foldr mk_Pair (base_frees, unit)) |
149 in |
156 in |
150 make_scheme_def :: [make_def] |
157 make_scheme_def :: [make_def] |
151 end; |
158 end; |
152 |
159 |
153 (*selectors*) |
160 (*selectors*) |
164 end; |
171 end; |
165 |
172 |
166 (*update*) |
173 (*update*) |
167 fun update_defs recT r all_fields current_fullfields thy = |
174 fun update_defs recT r all_fields current_fullfields thy = |
168 let |
175 let |
169 val sign = sign_of thy; |
|
170 val full = Sign.full_name sign; |
|
171 val len_all_fields = length all_fields; |
176 val len_all_fields = length all_fields; |
172 fun sel_last r = funpow len_all_fields ap_snd r; |
177 fun sel_last r = funpow len_all_fields ap_snd r; |
173 fun update_def_s (s, T) = |
178 fun update_def_s (s, T) = |
174 let val updates = map (fn (s', T') => |
179 let val updates = map (fn (s', T') => |
175 if s = s' then base_free (s, T) else selC s' T' recT $ r) |
180 if s = s' then base_free (s, T) else selC s' T' recT $ r) |
176 all_fields |
181 all_fields |
177 in |
182 in |
178 mk_defpair (updateC full s T recT $ base_free (s, T) $ r, |
183 mk_defpair (updateC s T recT $ base_free (s, T) $ r, |
179 foldr mk_Pair (updates, sel_last r)) |
184 foldr mk_Pair (updates, sel_last r)) |
180 end; |
185 end; |
181 in |
186 in |
182 map update_def_s current_fullfields |
187 map update_def_s current_fullfields |
183 end |
188 end |
|
189 |
|
190 |
|
191 (* theorems for make, selectors and update *) |
|
192 |
|
193 (*preparations*) |
|
194 fun get_all_selector_defs all_fields full thy = |
|
195 map (fn (s, T) => get_axiom thy (def_suffix s)) all_fields; |
|
196 fun get_all_update_defs all_fields full thy = |
|
197 map (fn (s, T) => get_axiom thy (def_suffix (update_suffix s))) all_fields; |
|
198 fun get_make_scheme_def full thy = get_axiom thy (full (def_suffix make_scheme_name)); |
|
199 fun get_make_def full thy = get_axiom thy (full (def_suffix make_name)); |
|
200 fun all_rec_defs all_fields full thy = |
|
201 get_make_scheme_def full thy :: get_make_def full thy :: |
|
202 get_all_selector_defs all_fields full thy @ get_all_update_defs all_fields full thy; |
|
203 fun prove_goal_s goal_s all_fields full thy = |
|
204 map (fn (s,T) => |
|
205 (prove_goalw_cterm (all_rec_defs all_fields full thy) |
|
206 (cterm_of (sign_of thy) (mk_eq (goal_s (s,T)))) |
|
207 (K [simp_tac (HOL_basic_ss addsimps [fst_conv,snd_conv]) 1]))) |
|
208 all_fields; |
|
209 |
|
210 (*si (make(_scheme) x1 ... xi ... xn) = xi*) |
|
211 fun sel_make_scheme_thms recT make_schemeT base_frees z all_fields full thy = |
|
212 let |
|
213 fun sel_make_scheme_s (s, T) = |
|
214 (selC s T recT $ make_args_scheme full make_schemeT base_frees z, base_free(s,T)) |
|
215 in |
|
216 prove_goal_s sel_make_scheme_s all_fields full thy |
|
217 end; |
|
218 |
|
219 fun sel_make_thms recT_unitT makeT base_frees all_fields full thy = |
|
220 let |
|
221 fun sel_make_s (s, T) = |
|
222 (selC s T recT_unitT $ make_args full makeT base_frees, Free(base s,T)) |
|
223 in |
|
224 prove_goal_s sel_make_s all_fields full thy |
|
225 end; |
|
226 |
|
227 (*si_update xia (make(_scheme) x1 ... xi ... xn) = (make x1 ... xia ... xn)*) |
|
228 fun update_make_scheme_thms recT make_schemeT base_frees z all_fields full thy = |
|
229 let |
|
230 fun update_make_scheme_s (s, T) = |
|
231 (updateC s T recT $ base_free(s ^ "'", T) $ |
|
232 make_args_scheme full make_schemeT base_frees z, |
|
233 make_args_scheme full make_schemeT |
|
234 (map (fn t => if t = base_free(s, T) then base_free(s ^ "'", T) else t) base_frees) z) |
|
235 in |
|
236 prove_goal_s update_make_scheme_s all_fields full thy |
|
237 end; |
|
238 |
|
239 fun update_make_thms recT_unitT makeT base_frees all_fields full thy = |
|
240 let |
|
241 fun update_make_s (s, T) = |
|
242 (updateC s T recT_unitT $ base_free(s ^ "'", T) $ |
|
243 make_args full makeT base_frees, |
|
244 make_args full makeT |
|
245 (map (fn t => if t = base_free(s, T) then base_free(s ^ "'", T) else t) base_frees)) |
|
246 in |
|
247 prove_goal_s update_make_s all_fields full thy |
|
248 end; |
184 |
249 |
185 |
250 |
186 |
251 |
187 (** errors **) |
252 (** errors **) |
188 |
253 |
273 |
338 |
274 val errors = check_duplicate_fields (map base (record_field_names thy info)) |
339 val errors = check_duplicate_fields (map base (record_field_names thy info)) |
275 in |
340 in |
276 if not (null errors) |
341 if not (null errors) |
277 then error (cat_lines errors) else |
342 then error (cat_lines errors) else |
|
343 let val thy = |
278 thy |> Theory.add_path ".." |
344 thy |> Theory.add_path ".." |
279 |> Theory.add_tyabbrs_i [(name, tfrees @ [zeta], recT, NoSyn)] |
345 |> Theory.add_tyabbrs_i [(name ^ "_scheme", tfrees @ [zeta], recT, NoSyn)] |
|
346 |> Theory.add_tyabbrs_i [(name, tfrees, recT_unitT, NoSyn)] |
280 |> Theory.add_path name |
347 |> Theory.add_path name |
281 |> Theory.add_consts_i (decls make_schemeT makeT selT updateT recT current_fields) |
348 |> Theory.add_consts_i (decls make_schemeT makeT selT updateT recT current_fields) |
282 |> Theory.add_defs_i |
349 |> Theory.add_defs_i |
283 ((make_defs make_schemeT makeT base_frees z thy) @ |
350 ((make_defs make_schemeT makeT base_frees z thy) @ |
284 (sel_defs recT r all_fields current_fullfields) @ |
351 (sel_defs recT r all_fields current_fullfields) @ |
285 (update_defs recT r all_fields current_fullfields thy)) |
352 (update_defs recT r all_fields current_fullfields thy)) |
|
353 in |
|
354 thy |> PureThy.store_thmss |
|
355 [("record_simps", |
|
356 sel_make_scheme_thms recT make_schemeT base_frees z all_fields full thy @ |
|
357 sel_make_thms recT_unitT makeT base_frees all_fields full thy @ |
|
358 update_make_scheme_thms recT make_schemeT base_frees z all_fields full thy @ |
|
359 update_make_thms recT_unitT makeT base_frees all_fields full thy )] |
286 |> Theory.add_path ".." |
360 |> Theory.add_path ".." |
|
361 end |
|
362 |
|
363 (* @ update_make_thms @ |
|
364 update_update_thms @ sel_update_thms)] *) |
|
365 |
287 end; |
366 end; |
288 |
367 |
289 |
368 |
290 |
369 |
291 (** external interfaces **) |
370 (** external interfaces **) |