1 (* Title: HOL/Tools/record_package.ML |
|
2 Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen |
|
3 |
|
4 Extensible records with structural subtyping in HOL. |
|
5 *) |
|
6 |
|
7 |
|
8 signature BASIC_RECORD_PACKAGE = |
|
9 sig |
|
10 val record_simproc: simproc |
|
11 val record_eq_simproc: simproc |
|
12 val record_upd_simproc: simproc |
|
13 val record_split_simproc: (term -> int) -> simproc |
|
14 val record_ex_sel_eq_simproc: simproc |
|
15 val record_split_tac: int -> tactic |
|
16 val record_split_simp_tac: thm list -> (term -> int) -> int -> tactic |
|
17 val record_split_name: string |
|
18 val record_split_wrapper: string * wrapper |
|
19 val print_record_type_abbr: bool ref |
|
20 val print_record_type_as_fields: bool ref |
|
21 end; |
|
22 |
|
23 signature RECORD_PACKAGE = |
|
24 sig |
|
25 include BASIC_RECORD_PACKAGE |
|
26 val timing: bool ref |
|
27 val record_quick_and_dirty_sensitive: bool ref |
|
28 val updateN: string |
|
29 val updN: string |
|
30 val ext_typeN: string |
|
31 val extN: string |
|
32 val makeN: string |
|
33 val moreN: string |
|
34 val ext_dest: string |
|
35 |
|
36 val last_extT: typ -> (string * typ list) option |
|
37 val dest_recTs : typ -> (string * typ list) list |
|
38 val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ) |
|
39 val get_recT_fields: theory -> typ -> (string * typ) list * (string * typ) |
|
40 val get_parent: theory -> string -> (typ list * string) option |
|
41 val get_extension: theory -> string -> (string * typ list) option |
|
42 val get_extinjects: theory -> thm list |
|
43 val get_simpset: theory -> simpset |
|
44 val print_records: theory -> unit |
|
45 val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list |
|
46 val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list |
|
47 val add_record: bool -> string list * string -> string option -> (string * string * mixfix) list |
|
48 -> theory -> theory |
|
49 val add_record_i: bool -> string list * string -> (typ list * string) option |
|
50 -> (string * typ * mixfix) list -> theory -> theory |
|
51 val setup: theory -> theory |
|
52 end; |
|
53 |
|
54 |
|
55 structure RecordPackage: RECORD_PACKAGE = |
|
56 struct |
|
57 |
|
58 val eq_reflection = thm "eq_reflection"; |
|
59 val rec_UNIV_I = thm "rec_UNIV_I"; |
|
60 val rec_True_simp = thm "rec_True_simp"; |
|
61 val Pair_eq = thm "Product_Type.prod.inject"; |
|
62 val atomize_all = thm "HOL.atomize_all"; |
|
63 val atomize_imp = thm "HOL.atomize_imp"; |
|
64 val meta_allE = thm "Pure.meta_allE"; |
|
65 val prop_subst = thm "prop_subst"; |
|
66 val Pair_sel_convs = [fst_conv,snd_conv]; |
|
67 val K_record_comp = @{thm "K_record_comp"}; |
|
68 val K_comp_convs = [@{thm o_apply}, K_record_comp] |
|
69 |
|
70 (** name components **) |
|
71 |
|
72 val rN = "r"; |
|
73 val wN = "w"; |
|
74 val moreN = "more"; |
|
75 val schemeN = "_scheme"; |
|
76 val ext_typeN = "_ext_type"; |
|
77 val extN ="_ext"; |
|
78 val casesN = "_cases"; |
|
79 val ext_dest = "_sel"; |
|
80 val updateN = "_update"; |
|
81 val updN = "_upd"; |
|
82 val makeN = "make"; |
|
83 val fields_selN = "fields"; |
|
84 val extendN = "extend"; |
|
85 val truncateN = "truncate"; |
|
86 |
|
87 (*see typedef_package.ML*) |
|
88 val RepN = "Rep_"; |
|
89 val AbsN = "Abs_"; |
|
90 |
|
91 (*** utilities ***) |
|
92 |
|
93 fun but_last xs = fst (split_last xs); |
|
94 |
|
95 fun varifyT midx = |
|
96 let fun varify (a, S) = TVar ((a, midx + 1), S); |
|
97 in map_type_tfree varify end; |
|
98 |
|
99 fun domain_type' T = |
|
100 domain_type T handle Match => T; |
|
101 |
|
102 fun range_type' T = |
|
103 range_type T handle Match => T; |
|
104 |
|
105 (* messages *) |
|
106 |
|
107 fun trace_thm str thm = |
|
108 tracing (str ^ (Pretty.string_of (Display.pretty_thm thm))); |
|
109 |
|
110 fun trace_thms str thms = |
|
111 (tracing str; map (trace_thm "") thms); |
|
112 |
|
113 fun trace_term str t = |
|
114 tracing (str ^ Syntax.string_of_term_global Pure.thy t); |
|
115 |
|
116 (* timing *) |
|
117 |
|
118 val timing = ref false; |
|
119 fun timeit_msg s x = if !timing then (warning s; timeit x) else x (); |
|
120 fun timing_msg s = if !timing then warning s else (); |
|
121 |
|
122 (* syntax *) |
|
123 |
|
124 fun prune n xs = Library.drop (n, xs); |
|
125 fun prefix_base s = Long_Name.map_base_name (fn bname => s ^ bname); |
|
126 |
|
127 val Trueprop = HOLogic.mk_Trueprop; |
|
128 fun All xs t = Term.list_all_free (xs, t); |
|
129 |
|
130 infix 9 $$; |
|
131 infix 0 :== ===; |
|
132 infixr 0 ==>; |
|
133 |
|
134 val (op $$) = Term.list_comb; |
|
135 val (op :==) = PrimitiveDefs.mk_defpair; |
|
136 val (op ===) = Trueprop o HOLogic.mk_eq; |
|
137 val (op ==>) = Logic.mk_implies; |
|
138 |
|
139 (* morphisms *) |
|
140 |
|
141 fun mk_RepN name = suffix ext_typeN (prefix_base RepN name); |
|
142 fun mk_AbsN name = suffix ext_typeN (prefix_base AbsN name); |
|
143 |
|
144 fun mk_Rep name repT absT = |
|
145 Const (suffix ext_typeN (prefix_base RepN name),absT --> repT); |
|
146 |
|
147 fun mk_Abs name repT absT = |
|
148 Const (mk_AbsN name,repT --> absT); |
|
149 |
|
150 (* constructor *) |
|
151 |
|
152 fun mk_extC (name,T) Ts = (suffix extN name, Ts ---> T); |
|
153 |
|
154 fun mk_ext (name,T) ts = |
|
155 let val Ts = map fastype_of ts |
|
156 in list_comb (Const (mk_extC (name,T) Ts),ts) end; |
|
157 |
|
158 (* cases *) |
|
159 |
|
160 fun mk_casesC (name,T,vT) Ts = (suffix casesN name, (Ts ---> vT) --> T --> vT) |
|
161 |
|
162 fun mk_cases (name,T,vT) f = |
|
163 let val Ts = binder_types (fastype_of f) |
|
164 in Const (mk_casesC (name,T,vT) Ts) $ f end; |
|
165 |
|
166 (* selector *) |
|
167 |
|
168 fun mk_selC sT (c,T) = (c,sT --> T); |
|
169 |
|
170 fun mk_sel s (c,T) = |
|
171 let val sT = fastype_of s |
|
172 in Const (mk_selC sT (c,T)) $ s end; |
|
173 |
|
174 (* updates *) |
|
175 |
|
176 fun mk_updC sfx sT (c,T) = (suffix sfx c, (T --> T) --> sT --> sT); |
|
177 |
|
178 fun mk_upd' sfx c v sT = |
|
179 let val vT = domain_type (fastype_of v); |
|
180 in Const (mk_updC sfx sT (c, vT)) $ v end; |
|
181 |
|
182 fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s |
|
183 |
|
184 (* types *) |
|
185 |
|
186 fun dest_recT (typ as Type (c_ext_type, Ts as (T::_))) = |
|
187 (case try (unsuffix ext_typeN) c_ext_type of |
|
188 NONE => raise TYPE ("RecordPackage.dest_recT", [typ], []) |
|
189 | SOME c => ((c, Ts), List.last Ts)) |
|
190 | dest_recT typ = raise TYPE ("RecordPackage.dest_recT", [typ], []); |
|
191 |
|
192 fun is_recT T = |
|
193 (case try dest_recT T of NONE => false | SOME _ => true); |
|
194 |
|
195 fun dest_recTs T = |
|
196 let val ((c, Ts), U) = dest_recT T |
|
197 in (c, Ts) :: dest_recTs U |
|
198 end handle TYPE _ => []; |
|
199 |
|
200 fun last_extT T = |
|
201 let val ((c, Ts), U) = dest_recT T |
|
202 in (case last_extT U of |
|
203 NONE => SOME (c,Ts) |
|
204 | SOME l => SOME l) |
|
205 end handle TYPE _ => NONE |
|
206 |
|
207 fun rec_id i T = |
|
208 let val rTs = dest_recTs T |
|
209 val rTs' = if i < 0 then rTs else Library.take (i,rTs) |
|
210 in Library.foldl (fn (s,(c,T)) => s ^ c) ("",rTs') end; |
|
211 |
|
212 (*** extend theory by record definition ***) |
|
213 |
|
214 (** record info **) |
|
215 |
|
216 (* type record_info and parent_info *) |
|
217 |
|
218 type record_info = |
|
219 {args: (string * sort) list, |
|
220 parent: (typ list * string) option, |
|
221 fields: (string * typ) list, |
|
222 extension: (string * typ list), |
|
223 induct: thm |
|
224 }; |
|
225 |
|
226 fun make_record_info args parent fields extension induct = |
|
227 {args = args, parent = parent, fields = fields, extension = extension, |
|
228 induct = induct}: record_info; |
|
229 |
|
230 |
|
231 type parent_info = |
|
232 {name: string, |
|
233 fields: (string * typ) list, |
|
234 extension: (string * typ list), |
|
235 induct: thm |
|
236 }; |
|
237 |
|
238 fun make_parent_info name fields extension induct = |
|
239 {name = name, fields = fields, extension = extension, induct = induct}: parent_info; |
|
240 |
|
241 |
|
242 (* theory data *) |
|
243 |
|
244 type record_data = |
|
245 {records: record_info Symtab.table, |
|
246 sel_upd: |
|
247 {selectors: unit Symtab.table, |
|
248 updates: string Symtab.table, |
|
249 simpset: Simplifier.simpset}, |
|
250 equalities: thm Symtab.table, |
|
251 extinjects: thm list, |
|
252 extsplit: thm Symtab.table, (* maps extension name to split rule *) |
|
253 splits: (thm*thm*thm*thm) Symtab.table, (* !!,!,EX - split-equalities,induct rule *) |
|
254 extfields: (string*typ) list Symtab.table, (* maps extension to its fields *) |
|
255 fieldext: (string*typ list) Symtab.table (* maps field to its extension *) |
|
256 }; |
|
257 |
|
258 fun make_record_data |
|
259 records sel_upd equalities extinjects extsplit splits extfields fieldext = |
|
260 {records = records, sel_upd = sel_upd, |
|
261 equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits, |
|
262 extfields = extfields, fieldext = fieldext }: record_data; |
|
263 |
|
264 structure RecordsData = TheoryDataFun |
|
265 ( |
|
266 type T = record_data; |
|
267 val empty = |
|
268 make_record_data Symtab.empty |
|
269 {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss} |
|
270 Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty; |
|
271 |
|
272 val copy = I; |
|
273 val extend = I; |
|
274 fun merge _ |
|
275 ({records = recs1, |
|
276 sel_upd = {selectors = sels1, updates = upds1, simpset = ss1}, |
|
277 equalities = equalities1, |
|
278 extinjects = extinjects1, |
|
279 extsplit = extsplit1, |
|
280 splits = splits1, |
|
281 extfields = extfields1, |
|
282 fieldext = fieldext1}, |
|
283 {records = recs2, |
|
284 sel_upd = {selectors = sels2, updates = upds2, simpset = ss2}, |
|
285 equalities = equalities2, |
|
286 extinjects = extinjects2, |
|
287 extsplit = extsplit2, |
|
288 splits = splits2, |
|
289 extfields = extfields2, |
|
290 fieldext = fieldext2}) = |
|
291 make_record_data |
|
292 (Symtab.merge (K true) (recs1, recs2)) |
|
293 {selectors = Symtab.merge (K true) (sels1, sels2), |
|
294 updates = Symtab.merge (K true) (upds1, upds2), |
|
295 simpset = Simplifier.merge_ss (ss1, ss2)} |
|
296 (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2)) |
|
297 (Library.merge Thm.eq_thm_prop (extinjects1, extinjects2)) |
|
298 (Symtab.merge Thm.eq_thm_prop (extsplit1,extsplit2)) |
|
299 (Symtab.merge (fn ((a,b,c,d),(w,x,y,z)) |
|
300 => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso |
|
301 Thm.eq_thm (c,y) andalso Thm.eq_thm (d,z)) |
|
302 (splits1, splits2)) |
|
303 (Symtab.merge (K true) (extfields1,extfields2)) |
|
304 (Symtab.merge (K true) (fieldext1,fieldext2)); |
|
305 ); |
|
306 |
|
307 fun print_records thy = |
|
308 let |
|
309 val {records = recs, ...} = RecordsData.get thy; |
|
310 val prt_typ = Syntax.pretty_typ_global thy; |
|
311 |
|
312 fun pretty_parent NONE = [] |
|
313 | pretty_parent (SOME (Ts, name)) = |
|
314 [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]]; |
|
315 |
|
316 fun pretty_field (c, T) = Pretty.block |
|
317 [Pretty.str (Sign.extern_const thy c), Pretty.str " ::", |
|
318 Pretty.brk 1, Pretty.quote (prt_typ T)]; |
|
319 |
|
320 fun pretty_record (name, {args, parent, fields, ...}: record_info) = |
|
321 Pretty.block (Pretty.fbreaks (Pretty.block |
|
322 [prt_typ (Type (name, map TFree args)), Pretty.str " = "] :: |
|
323 pretty_parent parent @ map pretty_field fields)); |
|
324 in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end; |
|
325 |
|
326 |
|
327 (* access 'records' *) |
|
328 |
|
329 val get_record = Symtab.lookup o #records o RecordsData.get; |
|
330 |
|
331 fun put_record name info thy = |
|
332 let |
|
333 val {records, sel_upd, equalities, extinjects,extsplit,splits,extfields,fieldext} = |
|
334 RecordsData.get thy; |
|
335 val data = make_record_data (Symtab.update (name, info) records) |
|
336 sel_upd equalities extinjects extsplit splits extfields fieldext; |
|
337 in RecordsData.put data thy end; |
|
338 |
|
339 |
|
340 (* access 'sel_upd' *) |
|
341 |
|
342 val get_sel_upd = #sel_upd o RecordsData.get; |
|
343 |
|
344 val is_selector = Symtab.defined o #selectors o get_sel_upd; |
|
345 val get_updates = Symtab.lookup o #updates o get_sel_upd; |
|
346 fun get_simpset thy = Simplifier.theory_context thy (#simpset (get_sel_upd thy)); |
|
347 |
|
348 fun put_sel_upd names simps = RecordsData.map (fn {records, |
|
349 sel_upd = {selectors, updates, simpset}, |
|
350 equalities, extinjects, extsplit, splits, extfields, fieldext} => |
|
351 make_record_data records |
|
352 {selectors = fold (fn name => Symtab.update (name, ())) names selectors, |
|
353 updates = fold (fn name => Symtab.update ((suffix updateN) name, name)) names updates, |
|
354 simpset = Simplifier.addsimps (simpset, simps)} |
|
355 equalities extinjects extsplit splits extfields fieldext); |
|
356 |
|
357 |
|
358 (* access 'equalities' *) |
|
359 |
|
360 fun add_record_equalities name thm thy = |
|
361 let |
|
362 val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = |
|
363 RecordsData.get thy; |
|
364 val data = make_record_data records sel_upd |
|
365 (Symtab.update_new (name, thm) equalities) extinjects extsplit |
|
366 splits extfields fieldext; |
|
367 in RecordsData.put data thy end; |
|
368 |
|
369 val get_equalities =Symtab.lookup o #equalities o RecordsData.get; |
|
370 |
|
371 |
|
372 (* access 'extinjects' *) |
|
373 |
|
374 fun add_extinjects thm thy = |
|
375 let |
|
376 val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = |
|
377 RecordsData.get thy; |
|
378 val data = |
|
379 make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) extsplit |
|
380 splits extfields fieldext; |
|
381 in RecordsData.put data thy end; |
|
382 |
|
383 val get_extinjects = rev o #extinjects o RecordsData.get; |
|
384 |
|
385 |
|
386 (* access 'extsplit' *) |
|
387 |
|
388 fun add_extsplit name thm thy = |
|
389 let |
|
390 val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = |
|
391 RecordsData.get thy; |
|
392 val data = make_record_data records sel_upd |
|
393 equalities extinjects (Symtab.update_new (name, thm) extsplit) splits |
|
394 extfields fieldext; |
|
395 in RecordsData.put data thy end; |
|
396 |
|
397 val get_extsplit = Symtab.lookup o #extsplit o RecordsData.get; |
|
398 |
|
399 |
|
400 (* access 'splits' *) |
|
401 |
|
402 fun add_record_splits name thmP thy = |
|
403 let |
|
404 val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = |
|
405 RecordsData.get thy; |
|
406 val data = make_record_data records sel_upd |
|
407 equalities extinjects extsplit (Symtab.update_new (name, thmP) splits) |
|
408 extfields fieldext; |
|
409 in RecordsData.put data thy end; |
|
410 |
|
411 val get_splits = Symtab.lookup o #splits o RecordsData.get; |
|
412 |
|
413 |
|
414 (* parent/extension of named record *) |
|
415 |
|
416 val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o RecordsData.get); |
|
417 val get_extension = Option.map #extension oo (Symtab.lookup o #records o RecordsData.get); |
|
418 |
|
419 |
|
420 (* access 'extfields' *) |
|
421 |
|
422 fun add_extfields name fields thy = |
|
423 let |
|
424 val {records, sel_upd, equalities, extinjects, extsplit,splits, extfields, fieldext} = |
|
425 RecordsData.get thy; |
|
426 val data = make_record_data records sel_upd |
|
427 equalities extinjects extsplit splits |
|
428 (Symtab.update_new (name, fields) extfields) fieldext; |
|
429 in RecordsData.put data thy end; |
|
430 |
|
431 val get_extfields = Symtab.lookup o #extfields o RecordsData.get; |
|
432 |
|
433 fun get_extT_fields thy T = |
|
434 let |
|
435 val ((name,Ts),moreT) = dest_recT T; |
|
436 val recname = let val (nm::recn::rst) = rev (Long_Name.explode name) |
|
437 in Long_Name.implode (rev (nm::rst)) end; |
|
438 val midx = maxidx_of_typs (moreT::Ts); |
|
439 val varifyT = varifyT midx; |
|
440 val {records,extfields,...} = RecordsData.get thy; |
|
441 val (flds,(more,_)) = split_last (Symtab.lookup_list extfields name); |
|
442 val args = map varifyT (snd (#extension (the (Symtab.lookup records recname)))); |
|
443 |
|
444 val subst = fold (Sign.typ_match thy) (but_last args ~~ but_last Ts) (Vartab.empty); |
|
445 val flds' = map (apsnd ((Envir.norm_type subst) o varifyT)) flds; |
|
446 in (flds',(more,moreT)) end; |
|
447 |
|
448 fun get_recT_fields thy T = |
|
449 let |
|
450 val (root_flds,(root_more,root_moreT)) = get_extT_fields thy T; |
|
451 val (rest_flds,rest_more) = |
|
452 if is_recT root_moreT then get_recT_fields thy root_moreT |
|
453 else ([],(root_more,root_moreT)); |
|
454 in (root_flds@rest_flds,rest_more) end; |
|
455 |
|
456 |
|
457 (* access 'fieldext' *) |
|
458 |
|
459 fun add_fieldext extname_types fields thy = |
|
460 let |
|
461 val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = |
|
462 RecordsData.get thy; |
|
463 val fieldext' = |
|
464 fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext; |
|
465 val data=make_record_data records sel_upd equalities extinjects extsplit |
|
466 splits extfields fieldext'; |
|
467 in RecordsData.put data thy end; |
|
468 |
|
469 |
|
470 val get_fieldext = Symtab.lookup o #fieldext o RecordsData.get; |
|
471 |
|
472 |
|
473 (* parent records *) |
|
474 |
|
475 fun add_parents thy NONE parents = parents |
|
476 | add_parents thy (SOME (types, name)) parents = |
|
477 let |
|
478 fun err msg = error (msg ^ " parent record " ^ quote name); |
|
479 |
|
480 val {args, parent, fields, extension, induct} = |
|
481 (case get_record thy name of SOME info => info | NONE => err "Unknown"); |
|
482 val _ = if length types <> length args then err "Bad number of arguments for" else (); |
|
483 |
|
484 fun bad_inst ((x, S), T) = |
|
485 if Sign.of_sort thy (T, S) then NONE else SOME x |
|
486 val bads = List.mapPartial bad_inst (args ~~ types); |
|
487 val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in"); |
|
488 |
|
489 val inst = map fst args ~~ types; |
|
490 val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst); |
|
491 val parent' = Option.map (apfst (map subst)) parent; |
|
492 val fields' = map (apsnd subst) fields; |
|
493 val extension' = apsnd (map subst) extension; |
|
494 in |
|
495 add_parents thy parent' |
|
496 (make_parent_info name fields' extension' induct :: parents) |
|
497 end; |
|
498 |
|
499 |
|
500 |
|
501 (** concrete syntax for records **) |
|
502 |
|
503 (* decode type *) |
|
504 |
|
505 fun decode_type thy t = |
|
506 let |
|
507 fun get_sort xs n = AList.lookup (op =) xs (n: indexname) |> the_default (Sign.defaultS thy); |
|
508 val map_sort = Sign.intern_sort thy; |
|
509 in |
|
510 Syntax.typ_of_term (get_sort (Syntax.term_sorts map_sort t)) map_sort t |
|
511 |> Sign.intern_tycons thy |
|
512 end; |
|
513 |
|
514 |
|
515 (* parse translations *) |
|
516 |
|
517 fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) = |
|
518 if c = mark then Syntax.const (suffix sfx name) $ (Abs ("_",dummyT, arg)) |
|
519 else raise TERM ("gen_field_tr: " ^ mark, [t]) |
|
520 | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]); |
|
521 |
|
522 fun gen_fields_tr sep mark sfx (tm as Const (c, _) $ t $ u) = |
|
523 if c = sep then gen_field_tr mark sfx t :: gen_fields_tr sep mark sfx u |
|
524 else [gen_field_tr mark sfx tm] |
|
525 | gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm]; |
|
526 |
|
527 |
|
528 fun record_update_tr [t, u] = |
|
529 Library.foldr (op $) (rev (gen_fields_tr "_updates" "_update" updateN u), t) |
|
530 | record_update_tr ts = raise TERM ("record_update_tr", ts); |
|
531 |
|
532 fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts |
|
533 | update_name_tr (Const (x, T) :: ts) = Const (suffix updateN x, T) $$ ts |
|
534 | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) = |
|
535 (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy")) $$ ts |
|
536 | update_name_tr ts = raise TERM ("update_name_tr", ts); |
|
537 |
|
538 fun dest_ext_field mark (t as (Const (c,_) $ Const (name,_) $ arg)) = |
|
539 if c = mark then (name,arg) else raise TERM ("dest_ext_field: " ^ mark, [t]) |
|
540 | dest_ext_field _ t = raise TERM ("dest_ext_field", [t]) |
|
541 |
|
542 fun dest_ext_fields sep mark (trm as (Const (c,_) $ t $ u)) = |
|
543 if c = sep then dest_ext_field mark t::dest_ext_fields sep mark u |
|
544 else [dest_ext_field mark trm] |
|
545 | dest_ext_fields _ mark t = [dest_ext_field mark t] |
|
546 |
|
547 fun gen_ext_fields_tr sep mark sfx more ctxt t = |
|
548 let |
|
549 val thy = ProofContext.theory_of ctxt; |
|
550 val msg = "error in record input: "; |
|
551 val fieldargs = dest_ext_fields sep mark t; |
|
552 fun splitargs (field::fields) ((name,arg)::fargs) = |
|
553 if can (unsuffix name) field |
|
554 then let val (args,rest) = splitargs fields fargs |
|
555 in (arg::args,rest) end |
|
556 else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t]) |
|
557 | splitargs [] (fargs as (_::_)) = ([],fargs) |
|
558 | splitargs (_::_) [] = raise TERM (msg ^ "expecting more fields", [t]) |
|
559 | splitargs _ _ = ([],[]); |
|
560 |
|
561 fun mk_ext (fargs as (name,arg)::_) = |
|
562 (case get_fieldext thy (Sign.intern_const thy name) of |
|
563 SOME (ext,_) => (case get_extfields thy ext of |
|
564 SOME flds |
|
565 => let val (args,rest) = |
|
566 splitargs (map fst (but_last flds)) fargs; |
|
567 val more' = mk_ext rest; |
|
568 in list_comb (Syntax.const (suffix sfx ext),args@[more']) |
|
569 end |
|
570 | NONE => raise TERM(msg ^ "no fields defined for " |
|
571 ^ ext,[t])) |
|
572 | NONE => raise TERM (msg ^ name ^" is no proper field",[t])) |
|
573 | mk_ext [] = more |
|
574 |
|
575 in mk_ext fieldargs end; |
|
576 |
|
577 fun gen_ext_type_tr sep mark sfx more ctxt t = |
|
578 let |
|
579 val thy = ProofContext.theory_of ctxt; |
|
580 val msg = "error in record-type input: "; |
|
581 val fieldargs = dest_ext_fields sep mark t; |
|
582 fun splitargs (field::fields) ((name,arg)::fargs) = |
|
583 if can (unsuffix name) field |
|
584 then let val (args,rest) = splitargs fields fargs |
|
585 in (arg::args,rest) end |
|
586 else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t]) |
|
587 | splitargs [] (fargs as (_::_)) = ([],fargs) |
|
588 | splitargs (_::_) [] = raise TERM (msg ^ "expecting more fields", [t]) |
|
589 | splitargs _ _ = ([],[]); |
|
590 |
|
591 fun mk_ext (fargs as (name,arg)::_) = |
|
592 (case get_fieldext thy (Sign.intern_const thy name) of |
|
593 SOME (ext,alphas) => |
|
594 (case get_extfields thy ext of |
|
595 SOME flds |
|
596 => (let |
|
597 val flds' = but_last flds; |
|
598 val types = map snd flds'; |
|
599 val (args,rest) = splitargs (map fst flds') fargs; |
|
600 val argtypes = map (Sign.certify_typ thy o decode_type thy) args; |
|
601 val midx = fold (fn T => fn i => Int.max (maxidx_of_typ T, i)) |
|
602 argtypes 0; |
|
603 val varifyT = varifyT midx; |
|
604 val vartypes = map varifyT types; |
|
605 |
|
606 val subst = fold (Sign.typ_match thy) (vartypes ~~ argtypes) |
|
607 Vartab.empty; |
|
608 val alphas' = map ((Syntax.term_of_typ (! Syntax.show_sorts)) o |
|
609 Envir.norm_type subst o varifyT) |
|
610 (but_last alphas); |
|
611 |
|
612 val more' = mk_ext rest; |
|
613 in list_comb (Syntax.const (suffix sfx ext),alphas'@[more']) |
|
614 end handle TYPE_MATCH => raise |
|
615 TERM (msg ^ "type is no proper record (extension)", [t])) |
|
616 | NONE => raise TERM (msg ^ "no fields defined for " ^ ext,[t])) |
|
617 | NONE => raise TERM (msg ^ name ^" is no proper field",[t])) |
|
618 | mk_ext [] = more |
|
619 |
|
620 in mk_ext fieldargs end; |
|
621 |
|
622 fun gen_adv_record_tr sep mark sfx unit ctxt [t] = |
|
623 gen_ext_fields_tr sep mark sfx unit ctxt t |
|
624 | gen_adv_record_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts); |
|
625 |
|
626 fun gen_adv_record_scheme_tr sep mark sfx ctxt [t, more] = |
|
627 gen_ext_fields_tr sep mark sfx more ctxt t |
|
628 | gen_adv_record_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts); |
|
629 |
|
630 fun gen_adv_record_type_tr sep mark sfx unit ctxt [t] = |
|
631 gen_ext_type_tr sep mark sfx unit ctxt t |
|
632 | gen_adv_record_type_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts); |
|
633 |
|
634 fun gen_adv_record_type_scheme_tr sep mark sfx ctxt [t, more] = |
|
635 gen_ext_type_tr sep mark sfx more ctxt t |
|
636 | gen_adv_record_type_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts); |
|
637 |
|
638 val adv_record_tr = gen_adv_record_tr "_fields" "_field" extN HOLogic.unit; |
|
639 val adv_record_scheme_tr = gen_adv_record_scheme_tr "_fields" "_field" extN; |
|
640 |
|
641 val adv_record_type_tr = |
|
642 gen_adv_record_type_tr "_field_types" "_field_type" ext_typeN |
|
643 (Syntax.term_of_typ false (HOLogic.unitT)); |
|
644 val adv_record_type_scheme_tr = |
|
645 gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN; |
|
646 |
|
647 |
|
648 val parse_translation = |
|
649 [("_record_update", record_update_tr), |
|
650 ("_update_name", update_name_tr)]; |
|
651 |
|
652 |
|
653 val adv_parse_translation = |
|
654 [("_record",adv_record_tr), |
|
655 ("_record_scheme",adv_record_scheme_tr), |
|
656 ("_record_type",adv_record_type_tr), |
|
657 ("_record_type_scheme",adv_record_type_scheme_tr)]; |
|
658 |
|
659 |
|
660 (* print translations *) |
|
661 |
|
662 val print_record_type_abbr = ref true; |
|
663 val print_record_type_as_fields = ref true; |
|
664 |
|
665 fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ k $ u) = |
|
666 let val t = (case k of (Abs (_,_,(Abs (_,_,t)$Bound 0))) |
|
667 => if null (loose_bnos t) then t else raise Match |
|
668 | Abs (x,_,t) => if null (loose_bnos t) then t else raise Match |
|
669 | _ => raise Match) |
|
670 |
|
671 (* (case k of (Const ("K_record",_)$t) => t |
|
672 | Abs (x,_,Const ("K_record",_)$t$Bound 0) => t |
|
673 | _ => raise Match)*) |
|
674 in |
|
675 (case try (unsuffix sfx) name_field of |
|
676 SOME name => |
|
677 apfst (cons (Syntax.const mark $ Syntax.free name $ t)) (gen_field_upds_tr' mark sfx u) |
|
678 | NONE => ([], tm)) |
|
679 end |
|
680 | gen_field_upds_tr' _ _ tm = ([], tm); |
|
681 |
|
682 fun record_update_tr' tm = |
|
683 let val (ts, u) = gen_field_upds_tr' "_update" updateN tm in |
|
684 if null ts then raise Match |
|
685 else Syntax.const "_record_update" $ u $ |
|
686 foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts) |
|
687 end; |
|
688 |
|
689 fun gen_field_tr' sfx tr' name = |
|
690 let val name_sfx = suffix sfx name |
|
691 in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end; |
|
692 |
|
693 fun record_tr' sep mark record record_scheme unit ctxt t = |
|
694 let |
|
695 val thy = ProofContext.theory_of ctxt; |
|
696 fun field_lst t = |
|
697 (case strip_comb t of |
|
698 (Const (ext,_),args as (_::_)) |
|
699 => (case try (unsuffix extN) (Sign.intern_const thy ext) of |
|
700 SOME ext' |
|
701 => (case get_extfields thy ext' of |
|
702 SOME flds |
|
703 => (let |
|
704 val (f::fs) = but_last (map fst flds); |
|
705 val flds' = Sign.extern_const thy f :: map Long_Name.base_name fs; |
|
706 val (args',more) = split_last args; |
|
707 in (flds'~~args')@field_lst more end |
|
708 handle Library.UnequalLengths => [("",t)]) |
|
709 | NONE => [("",t)]) |
|
710 | NONE => [("",t)]) |
|
711 | _ => [("",t)]) |
|
712 |
|
713 val (flds,(_,more)) = split_last (field_lst t); |
|
714 val _ = if null flds then raise Match else (); |
|
715 val flds' = map (fn (n,t)=>Syntax.const mark$Syntax.const n$t) flds; |
|
716 val flds'' = foldr1 (fn (x,y) => Syntax.const sep$x$y) flds'; |
|
717 |
|
718 in if unit more |
|
719 then Syntax.const record$flds'' |
|
720 else Syntax.const record_scheme$flds''$more |
|
721 end |
|
722 |
|
723 fun gen_record_tr' name = |
|
724 let val name_sfx = suffix extN name; |
|
725 val unit = (fn Const (@{const_syntax "Product_Type.Unity"},_) => true | _ => false); |
|
726 fun tr' ctxt ts = record_tr' "_fields" "_field" "_record" "_record_scheme" unit ctxt |
|
727 (list_comb (Syntax.const name_sfx,ts)) |
|
728 in (name_sfx,tr') |
|
729 end |
|
730 |
|
731 fun print_translation names = |
|
732 map (gen_field_tr' updateN record_update_tr') names; |
|
733 |
|
734 |
|
735 (* record_type_abbr_tr' tries to reconstruct the record name type abbreviation from *) |
|
736 (* the (nested) extension types. *) |
|
737 fun record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt tm = |
|
738 let |
|
739 val thy = ProofContext.theory_of ctxt; |
|
740 (* tm is term representation of a (nested) field type. We first reconstruct the *) |
|
741 (* type from tm so that we can continue on the type level rather then the term level.*) |
|
742 |
|
743 (* WORKAROUND: |
|
744 * If a record type occurs in an error message of type inference there |
|
745 * may be some internal frees donoted by ??: |
|
746 * (Const "_tfree",_)$Free ("??'a",_). |
|
747 |
|
748 * This will unfortunately be translated to Type ("??'a",[]) instead of |
|
749 * TFree ("??'a",_) by typ_of_term, which will confuse unify below. |
|
750 * fixT works around. |
|
751 *) |
|
752 fun fixT (T as Type (x,[])) = |
|
753 if String.isPrefix "??'" x then TFree (x,Sign.defaultS thy) else T |
|
754 | fixT (Type (x,xs)) = Type (x,map fixT xs) |
|
755 | fixT T = T; |
|
756 |
|
757 val T = fixT (decode_type thy tm); |
|
758 val midx = maxidx_of_typ T; |
|
759 val varifyT = varifyT midx; |
|
760 |
|
761 fun mk_type_abbr subst name alphas = |
|
762 let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas); |
|
763 in Syntax.term_of_typ (! Syntax.show_sorts) |
|
764 (Sign.extern_typ thy (Envir.norm_type subst abbrT)) end; |
|
765 |
|
766 fun match rT T = (Sign.typ_match thy (varifyT rT,T) |
|
767 Vartab.empty); |
|
768 |
|
769 in if !print_record_type_abbr |
|
770 then (case last_extT T of |
|
771 SOME (name,_) |
|
772 => if name = lastExt |
|
773 then |
|
774 (let |
|
775 val subst = match schemeT T |
|
776 in |
|
777 if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree(zeta,Sign.defaultS thy)))) |
|
778 then mk_type_abbr subst abbr alphas |
|
779 else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta]) |
|
780 end handle TYPE_MATCH => default_tr' ctxt tm) |
|
781 else raise Match (* give print translation of specialised record a chance *) |
|
782 | _ => raise Match) |
|
783 else default_tr' ctxt tm |
|
784 end |
|
785 |
|
786 fun record_type_tr' sep mark record record_scheme ctxt t = |
|
787 let |
|
788 val thy = ProofContext.theory_of ctxt; |
|
789 |
|
790 val T = decode_type thy t; |
|
791 val varifyT = varifyT (Term.maxidx_of_typ T); |
|
792 |
|
793 fun term_of_type T = Syntax.term_of_typ (!Syntax.show_sorts) (Sign.extern_typ thy T); |
|
794 |
|
795 fun field_lst T = |
|
796 (case T of |
|
797 Type (ext, args) |
|
798 => (case try (unsuffix ext_typeN) ext of |
|
799 SOME ext' |
|
800 => (case get_extfields thy ext' of |
|
801 SOME flds |
|
802 => (case get_fieldext thy (fst (hd flds)) of |
|
803 SOME (_, alphas) |
|
804 => (let |
|
805 val (f :: fs) = but_last flds; |
|
806 val flds' = apfst (Sign.extern_const thy) f |
|
807 :: map (apfst Long_Name.base_name) fs; |
|
808 val (args', more) = split_last args; |
|
809 val alphavars = map varifyT (but_last alphas); |
|
810 val subst = fold2 (curry (Sign.typ_match thy)) |
|
811 alphavars args' Vartab.empty; |
|
812 val flds'' = (map o apsnd) |
|
813 (Envir.norm_type subst o varifyT) flds'; |
|
814 in flds'' @ field_lst more end |
|
815 handle TYPE_MATCH => [("", T)] |
|
816 | Library.UnequalLengths => [("", T)]) |
|
817 | NONE => [("", T)]) |
|
818 | NONE => [("", T)]) |
|
819 | NONE => [("", T)]) |
|
820 | _ => [("", T)]) |
|
821 |
|
822 val (flds, (_, moreT)) = split_last (field_lst T); |
|
823 val flds' = map (fn (n, T) => Syntax.const mark $ Syntax.const n $ term_of_type T) flds; |
|
824 val flds'' = foldr1 (fn (x, y) => Syntax.const sep $ x $ y) flds' handle Empty => raise Match; |
|
825 |
|
826 in if not (!print_record_type_as_fields) orelse null flds then raise Match |
|
827 else if moreT = HOLogic.unitT |
|
828 then Syntax.const record$flds'' |
|
829 else Syntax.const record_scheme$flds''$term_of_type moreT |
|
830 end |
|
831 |
|
832 |
|
833 fun gen_record_type_tr' name = |
|
834 let val name_sfx = suffix ext_typeN name; |
|
835 fun tr' ctxt ts = record_type_tr' "_field_types" "_field_type" |
|
836 "_record_type" "_record_type_scheme" ctxt |
|
837 (list_comb (Syntax.const name_sfx,ts)) |
|
838 in (name_sfx,tr') |
|
839 end |
|
840 |
|
841 |
|
842 fun gen_record_type_abbr_tr' abbr alphas zeta lastExt schemeT name = |
|
843 let val name_sfx = suffix ext_typeN name; |
|
844 val default_tr' = record_type_tr' "_field_types" "_field_type" |
|
845 "_record_type" "_record_type_scheme" |
|
846 fun tr' ctxt ts = |
|
847 record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt |
|
848 (list_comb (Syntax.const name_sfx,ts)) |
|
849 in (name_sfx, tr') end; |
|
850 |
|
851 (** record simprocs **) |
|
852 |
|
853 val record_quick_and_dirty_sensitive = ref false; |
|
854 |
|
855 |
|
856 fun quick_and_dirty_prove stndrd thy asms prop tac = |
|
857 if !record_quick_and_dirty_sensitive andalso !quick_and_dirty |
|
858 then Goal.prove (ProofContext.init thy) [] [] |
|
859 (Logic.list_implies (map Logic.varify asms,Logic.varify prop)) |
|
860 (K (SkipProof.cheat_tac @{theory HOL})) |
|
861 (* standard can take quite a while for large records, thats why |
|
862 * we varify the proposition manually here.*) |
|
863 else let val prf = Goal.prove (ProofContext.init thy) [] asms prop tac; |
|
864 in if stndrd then standard prf else prf end; |
|
865 |
|
866 fun quick_and_dirty_prf noopt opt () = |
|
867 if !record_quick_and_dirty_sensitive andalso !quick_and_dirty |
|
868 then noopt () |
|
869 else opt (); |
|
870 |
|
871 local |
|
872 fun abstract_over_fun_app (Abs (f,fT,t)) = |
|
873 let |
|
874 val (f',t') = Term.dest_abs (f,fT,t); |
|
875 val T = domain_type fT; |
|
876 val (x,T') = hd (Term.variant_frees t' [("x",T)]); |
|
877 val f_x = Free (f',fT)$(Free (x,T')); |
|
878 fun is_constr (Const (c,_)$_) = can (unsuffix extN) c |
|
879 | is_constr _ = false; |
|
880 fun subst (t as u$w) = if Free (f',fT)=u |
|
881 then if is_constr w then f_x |
|
882 else raise TERM ("abstract_over_fun_app",[t]) |
|
883 else subst u$subst w |
|
884 | subst (Abs (x,T,t)) = (Abs (x,T,subst t)) |
|
885 | subst t = t |
|
886 val t'' = abstract_over (f_x,subst t'); |
|
887 val vars = strip_qnt_vars "all" t''; |
|
888 val bdy = strip_qnt_body "all" t''; |
|
889 |
|
890 in list_abs ((x,T')::vars,bdy) end |
|
891 | abstract_over_fun_app t = raise TERM ("abstract_over_fun_app",[t]); |
|
892 (* Generates a theorem of the kind: |
|
893 * !!f x*. PROP P (f ( r x* ) x* == !!r x*. PROP P r x* |
|
894 *) |
|
895 fun mk_fun_apply_eq (Abs (f, fT, t)) thy = |
|
896 let |
|
897 val rT = domain_type fT; |
|
898 val vars = Term.strip_qnt_vars "all" t; |
|
899 val Ts = map snd vars; |
|
900 val n = length vars; |
|
901 fun app_bounds 0 t = t$Bound 0 |
|
902 | app_bounds n t = if n > 0 then app_bounds (n-1) (t$Bound n) else t |
|
903 |
|
904 |
|
905 val [P,r] = Term.variant_frees t [("P",rT::Ts--->Term.propT),("r",Ts--->rT)]; |
|
906 val prop = Logic.mk_equals |
|
907 (list_all ((f,fT)::vars, |
|
908 app_bounds (n - 1) ((Free P)$(Bound n$app_bounds (n-1) (Free r)))), |
|
909 list_all ((fst r,rT)::vars, |
|
910 app_bounds (n - 1) ((Free P)$Bound n))); |
|
911 val prove_standard = quick_and_dirty_prove true thy; |
|
912 val thm = prove_standard [] prop (fn _ => |
|
913 EVERY [rtac equal_intr_rule 1, |
|
914 Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1, |
|
915 Goal.norm_hhf_tac 1,REPEAT (etac meta_allE 1), atac 1]); |
|
916 in thm end |
|
917 | mk_fun_apply_eq t thy = raise TERM ("mk_fun_apply_eq",[t]); |
|
918 |
|
919 in |
|
920 (* During proof of theorems produced by record_simproc you can end up in |
|
921 * situations like "!!f ... . ... f r ..." where f is an extension update function. |
|
922 * In order to split "f r" we transform this to "!!r ... . ... r ..." so that the |
|
923 * usual split rules for extensions can apply. |
|
924 *) |
|
925 val record_split_f_more_simproc = |
|
926 Simplifier.simproc @{theory HOL} "record_split_f_more_simp" ["x"] |
|
927 (fn thy => fn _ => fn t => |
|
928 (case t of (Const ("all", Type (_, [Type (_, [Type("fun",[T,T']), _]), _])))$ |
|
929 (trm as Abs _) => |
|
930 (case rec_id (~1) T of |
|
931 "" => NONE |
|
932 | n => if T=T' |
|
933 then (let |
|
934 val P=cterm_of thy (abstract_over_fun_app trm); |
|
935 val thm = mk_fun_apply_eq trm thy; |
|
936 val PV = cterm_of thy (hd (OldTerm.term_vars (prop_of thm))); |
|
937 val thm' = cterm_instantiate [(PV,P)] thm; |
|
938 in SOME thm' end handle TERM _ => NONE) |
|
939 else NONE) |
|
940 | _ => NONE)) |
|
941 end |
|
942 |
|
943 fun prove_split_simp thy ss T prop = |
|
944 let |
|
945 val {sel_upd={simpset,...},extsplit,...} = RecordsData.get thy; |
|
946 val extsplits = |
|
947 Library.foldl (fn (thms,(n,_)) => the_list (Symtab.lookup extsplit n) @ thms) |
|
948 ([],dest_recTs T); |
|
949 val thms = (case get_splits thy (rec_id (~1) T) of |
|
950 SOME (all_thm,_,_,_) => |
|
951 all_thm::(case extsplits of [thm] => [] | _ => extsplits) |
|
952 (* [thm] is the same as all_thm *) |
|
953 | NONE => extsplits) |
|
954 val thms'=K_comp_convs@thms; |
|
955 val ss' = (Simplifier.inherit_context ss simpset |
|
956 addsimps thms' |
|
957 addsimprocs [record_split_f_more_simproc]); |
|
958 in |
|
959 quick_and_dirty_prove true thy [] prop (fn _ => simp_tac ss' 1) |
|
960 end; |
|
961 |
|
962 |
|
963 local |
|
964 fun eq (s1:string) (s2:string) = (s1 = s2); |
|
965 fun has_field extfields f T = |
|
966 exists (fn (eN,_) => exists (eq f o fst) (Symtab.lookup_list extfields eN)) |
|
967 (dest_recTs T); |
|
968 |
|
969 fun K_skeleton n (T as Type (_,[_,kT])) (b as Bound i) (Abs (x,xT,t)) = |
|
970 if null (loose_bnos t) then ((n,kT),(Abs (x,xT,Bound (i+1)))) else ((n,T),b) |
|
971 | K_skeleton n T b _ = ((n,T),b); |
|
972 |
|
973 (* |
|
974 fun K_skeleton n _ b ((K_rec as Const ("Record.K_record",Type (_,[kT,_])))$_) = |
|
975 ((n,kT),K_rec$b) |
|
976 | K_skeleton n _ (Bound i) |
|
977 (Abs (x,T,(K_rec as Const ("Record.K_record",Type (_,[kT,_])))$_$Bound 0)) = |
|
978 ((n,kT),Abs (x,T,(K_rec$Bound (i+1)$Bound 0))) |
|
979 | K_skeleton n T b _ = ((n,T),b); |
|
980 *) |
|
981 |
|
982 fun normalize_rhs thm = |
|
983 let |
|
984 val ss = HOL_basic_ss addsimps K_comp_convs; |
|
985 val rhs = thm |> Thm.cprop_of |> Thm.dest_comb |> snd; |
|
986 val rhs' = (Simplifier.rewrite ss rhs); |
|
987 in Thm.transitive thm rhs' end; |
|
988 in |
|
989 (* record_simproc *) |
|
990 (* Simplifies selections of an record update: |
|
991 * (1) S (S_update k r) = k (S r) |
|
992 * (2) S (X_update k r) = S r |
|
993 * The simproc skips multiple updates at once, eg: |
|
994 * S (X_update x (Y_update y (S_update k r))) = k (S r) |
|
995 * But be careful in (2) because of the extendibility of records. |
|
996 * - If S is a more-selector we have to make sure that the update on component |
|
997 * X does not affect the selected subrecord. |
|
998 * - If X is a more-selector we have to make sure that S is not in the updated |
|
999 * subrecord. |
|
1000 *) |
|
1001 val record_simproc = |
|
1002 Simplifier.simproc @{theory HOL} "record_simp" ["x"] |
|
1003 (fn thy => fn ss => fn t => |
|
1004 (case t of (sel as Const (s, Type (_,[domS,rangeS])))$ |
|
1005 ((upd as Const (u,Type(_,[_,Type (_,[rT,_])]))) $ k $ r)=> |
|
1006 if is_selector thy s then |
|
1007 (case get_updates thy u of SOME u_name => |
|
1008 let |
|
1009 val {sel_upd={updates,...},extfields,...} = RecordsData.get thy; |
|
1010 |
|
1011 fun mk_eq_terms ((upd as Const (u,Type(_,[kT,_]))) $ k $ r) = |
|
1012 (case Symtab.lookup updates u of |
|
1013 NONE => NONE |
|
1014 | SOME u_name |
|
1015 => if u_name = s |
|
1016 then (case mk_eq_terms r of |
|
1017 NONE => |
|
1018 let |
|
1019 val rv = ("r",rT) |
|
1020 val rb = Bound 0 |
|
1021 val (kv,kb) = K_skeleton "k" kT (Bound 1) k; |
|
1022 in SOME (upd$kb$rb,kb$(sel$rb),[kv,rv]) end |
|
1023 | SOME (trm,trm',vars) => |
|
1024 let |
|
1025 val (kv,kb) = K_skeleton "k" kT (Bound (length vars)) k; |
|
1026 in SOME (upd$kb$trm,kb$trm',kv::vars) end) |
|
1027 else if has_field extfields u_name rangeS |
|
1028 orelse has_field extfields s (domain_type kT) |
|
1029 then NONE |
|
1030 else (case mk_eq_terms r of |
|
1031 SOME (trm,trm',vars) |
|
1032 => let |
|
1033 val (kv,kb) = |
|
1034 K_skeleton "k" kT (Bound (length vars)) k; |
|
1035 in SOME (upd$kb$trm,trm',kv::vars) end |
|
1036 | NONE |
|
1037 => let |
|
1038 val rv = ("r",rT) |
|
1039 val rb = Bound 0 |
|
1040 val (kv,kb) = K_skeleton "k" kT (Bound 1) k; |
|
1041 in SOME (upd$kb$rb,sel$rb,[kv,rv]) end)) |
|
1042 | mk_eq_terms r = NONE |
|
1043 in |
|
1044 (case mk_eq_terms (upd$k$r) of |
|
1045 SOME (trm,trm',vars) |
|
1046 => SOME (prove_split_simp thy ss domS |
|
1047 (list_all(vars, Logic.mk_equals (sel $ trm, trm')))) |
|
1048 | NONE => NONE) |
|
1049 end |
|
1050 | NONE => NONE) |
|
1051 else NONE |
|
1052 | _ => NONE)); |
|
1053 |
|
1054 (* record_upd_simproc *) |
|
1055 (* simplify multiple updates: |
|
1056 * (1) "N_update y (M_update g (N_update x (M_update f r))) = |
|
1057 (N_update (y o x) (M_update (g o f) r))" |
|
1058 * (2) "r(|M:= M r|) = r" |
|
1059 * For (2) special care of "more" updates has to be taken: |
|
1060 * r(|more := m; A := A r|) |
|
1061 * If A is contained in the fields of m we cannot remove the update A := A r! |
|
1062 * (But r(|more := r; A := A (r(|more := r|))|) = r(|more := r|) |
|
1063 *) |
|
1064 val record_upd_simproc = |
|
1065 Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"] |
|
1066 (fn thy => fn ss => fn t => |
|
1067 (case t of ((upd as Const (u, Type(_,[_,Type(_,[rT,_])]))) $ k $ r) => |
|
1068 let datatype ('a,'b) calc = Init of 'b | Inter of 'a |
|
1069 val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get thy; |
|
1070 |
|
1071 (*fun mk_abs_var x t = (x, fastype_of t);*) |
|
1072 fun sel_name u = Long_Name.base_name (unsuffix updateN u); |
|
1073 |
|
1074 fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) = |
|
1075 if has_field extfields s (domain_type' mT) then upd else seed s r |
|
1076 | seed _ r = r; |
|
1077 |
|
1078 fun grow u uT k kT vars (sprout,skeleton) = |
|
1079 if sel_name u = moreN |
|
1080 then let val (kv,kb) = K_skeleton "k" kT (Bound (length vars)) k; |
|
1081 in ((Const (u,uT)$k$sprout,Const (u,uT)$kb$skeleton),kv::vars) end |
|
1082 else ((sprout,skeleton),vars); |
|
1083 |
|
1084 |
|
1085 fun dest_k (Abs (x,T,((sel as Const (s,_))$r))) = |
|
1086 if null (loose_bnos r) then SOME (x,T,sel,s,r) else NONE |
|
1087 | dest_k (Abs (_,_,(Abs (x,T,((sel as Const (s,_))$r)))$Bound 0)) = |
|
1088 (* eta expanded variant *) |
|
1089 if null (loose_bnos r) then SOME (x,T,sel,s,r) else NONE |
|
1090 | dest_k _ = NONE; |
|
1091 |
|
1092 fun is_upd_same (sprout,skeleton) u k = |
|
1093 (case dest_k k of SOME (x,T,sel,s,r) => |
|
1094 if (unsuffix updateN u) = s andalso (seed s sprout) = r |
|
1095 then SOME (fn t => Abs (x,T,incr_boundvars 1 t),sel,seed s skeleton) |
|
1096 else NONE |
|
1097 | NONE => NONE); |
|
1098 |
|
1099 fun init_seed r = ((r,Bound 0), [("r", rT)]); |
|
1100 |
|
1101 fun add (n:string) f fmaps = |
|
1102 (case AList.lookup (op =) fmaps n of |
|
1103 NONE => AList.update (op =) (n,[f]) fmaps |
|
1104 | SOME fs => AList.update (op =) (n,f::fs) fmaps) |
|
1105 |
|
1106 fun comps (n:string) T fmaps = |
|
1107 (case AList.lookup (op =) fmaps n of |
|
1108 SOME fs => |
|
1109 foldr1 (fn (f,g) => Const ("Fun.comp",(T-->T)-->(T-->T)-->(T-->T))$f$g) fs |
|
1110 | NONE => error ("record_upd_simproc.comps")) |
|
1111 |
|
1112 (* mk_updterm returns either |
|
1113 * - Init (orig-term, orig-term-skeleton, vars) if no optimisation can be made, |
|
1114 * where vars are the bound variables in the skeleton |
|
1115 * - Inter (orig-term-skeleton,simplified-term-skeleton, |
|
1116 * vars, (term-sprout, skeleton-sprout)) |
|
1117 * where "All vars. orig-term-skeleton = simplified-term-skeleton" is |
|
1118 * the desired simplification rule, |
|
1119 * the sprouts accumulate the "more-updates" on the way from the seed |
|
1120 * to the outermost update. It is only relevant to calculate the |
|
1121 * possible simplification for (2) |
|
1122 * The algorithm first walks down the updates to the seed-record while |
|
1123 * memorising the updates in the already-table. While walking up the |
|
1124 * updates again, the optimised term is constructed. |
|
1125 *) |
|
1126 fun mk_updterm upds already |
|
1127 (t as ((upd as Const (u,uT as (Type (_,[kT,_])))) $ k $ r)) = |
|
1128 if Symtab.defined upds u |
|
1129 then let |
|
1130 fun rest already = mk_updterm upds already |
|
1131 in if u mem_string already |
|
1132 then (case (rest already r) of |
|
1133 Init ((sprout,skel),vars) => |
|
1134 let |
|
1135 val n = sel_name u; |
|
1136 val (kv,kb) = K_skeleton n kT (Bound (length vars)) k; |
|
1137 val (sprout',vars')= grow u uT k kT (kv::vars) (sprout,skel); |
|
1138 in Inter (upd$kb$skel,skel,vars',add n kb [],sprout') end |
|
1139 | Inter (trm,trm',vars,fmaps,sprout) => |
|
1140 let |
|
1141 val n = sel_name u; |
|
1142 val (kv,kb) = K_skeleton n kT (Bound (length vars)) k; |
|
1143 val (sprout',vars') = grow u uT k kT (kv::vars) sprout; |
|
1144 in Inter(upd$kb$trm,trm',kv::vars',add n kb fmaps,sprout') |
|
1145 end) |
|
1146 else |
|
1147 (case rest (u::already) r of |
|
1148 Init ((sprout,skel),vars) => |
|
1149 (case is_upd_same (sprout,skel) u k of |
|
1150 SOME (K_rec,sel,skel') => |
|
1151 let |
|
1152 val (sprout',vars') = grow u uT k kT vars (sprout,skel); |
|
1153 in Inter(upd$(K_rec (sel$skel'))$skel,skel,vars',[],sprout') |
|
1154 end |
|
1155 | NONE => |
|
1156 let |
|
1157 val n = sel_name u; |
|
1158 val (kv,kb) = K_skeleton n kT (Bound (length vars)) k; |
|
1159 in Init ((upd$k$sprout,upd$kb$skel),kv::vars) end) |
|
1160 | Inter (trm,trm',vars,fmaps,sprout) => |
|
1161 (case is_upd_same sprout u k of |
|
1162 SOME (K_rec,sel,skel) => |
|
1163 let |
|
1164 val (sprout',vars') = grow u uT k kT vars sprout |
|
1165 in Inter(upd$(K_rec (sel$skel))$trm,trm',vars',fmaps,sprout') |
|
1166 end |
|
1167 | NONE => |
|
1168 let |
|
1169 val n = sel_name u |
|
1170 val T = domain_type kT |
|
1171 val (kv,kb) = K_skeleton n kT (Bound (length vars)) k; |
|
1172 val (sprout',vars') = grow u uT k kT (kv::vars) sprout |
|
1173 val fmaps' = add n kb fmaps |
|
1174 in Inter (upd$kb$trm,upd$comps n T fmaps'$trm' |
|
1175 ,vars',fmaps',sprout') end)) |
|
1176 end |
|
1177 else Init (init_seed t) |
|
1178 | mk_updterm _ _ t = Init (init_seed t); |
|
1179 |
|
1180 in (case mk_updterm updates [] t of |
|
1181 Inter (trm,trm',vars,_,_) |
|
1182 => SOME (normalize_rhs |
|
1183 (prove_split_simp thy ss rT |
|
1184 (list_all(vars, Logic.mk_equals (trm, trm'))))) |
|
1185 | _ => NONE) |
|
1186 end |
|
1187 | _ => NONE)) |
|
1188 end |
|
1189 |
|
1190 (* record_eq_simproc *) |
|
1191 (* looks up the most specific record-equality. |
|
1192 * Note on efficiency: |
|
1193 * Testing equality of records boils down to the test of equality of all components. |
|
1194 * Therefore the complexity is: #components * complexity for single component. |
|
1195 * Especially if a record has a lot of components it may be better to split up |
|
1196 * the record first and do simplification on that (record_split_simp_tac). |
|
1197 * e.g. r(|lots of updates|) = x |
|
1198 * |
|
1199 * record_eq_simproc record_split_simp_tac |
|
1200 * Complexity: #components * #updates #updates |
|
1201 * |
|
1202 *) |
|
1203 val record_eq_simproc = |
|
1204 Simplifier.simproc @{theory HOL} "record_eq_simp" ["r = s"] |
|
1205 (fn thy => fn _ => fn t => |
|
1206 (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ => |
|
1207 (case rec_id (~1) T of |
|
1208 "" => NONE |
|
1209 | name => (case get_equalities thy name of |
|
1210 NONE => NONE |
|
1211 | SOME thm => SOME (thm RS Eq_TrueI))) |
|
1212 | _ => NONE)); |
|
1213 |
|
1214 (* record_split_simproc *) |
|
1215 (* splits quantified occurrences of records, for which P holds. P can peek on the |
|
1216 * subterm starting at the quantified occurrence of the record (including the quantifier) |
|
1217 * P t = 0: do not split |
|
1218 * P t = ~1: completely split |
|
1219 * P t > 0: split up to given bound of record extensions |
|
1220 *) |
|
1221 fun record_split_simproc P = |
|
1222 Simplifier.simproc @{theory HOL} "record_split_simp" ["x"] |
|
1223 (fn thy => fn _ => fn t => |
|
1224 (case t of (Const (quantifier, Type (_, [Type (_, [T, _]), _])))$trm => |
|
1225 if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex" |
|
1226 then (case rec_id (~1) T of |
|
1227 "" => NONE |
|
1228 | name |
|
1229 => let val split = P t |
|
1230 in if split <> 0 then |
|
1231 (case get_splits thy (rec_id split T) of |
|
1232 NONE => NONE |
|
1233 | SOME (all_thm, All_thm, Ex_thm,_) |
|
1234 => SOME (case quantifier of |
|
1235 "all" => all_thm |
|
1236 | "All" => All_thm RS eq_reflection |
|
1237 | "Ex" => Ex_thm RS eq_reflection |
|
1238 | _ => error "record_split_simproc")) |
|
1239 else NONE |
|
1240 end) |
|
1241 else NONE |
|
1242 | _ => NONE)) |
|
1243 |
|
1244 val record_ex_sel_eq_simproc = |
|
1245 Simplifier.simproc @{theory HOL} "record_ex_sel_eq_simproc" ["Ex t"] |
|
1246 (fn thy => fn ss => fn t => |
|
1247 let |
|
1248 fun prove prop = |
|
1249 quick_and_dirty_prove true thy [] prop |
|
1250 (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy) |
|
1251 addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1); |
|
1252 |
|
1253 fun mkeq (lr,Teq,(sel,Tsel),x) i = |
|
1254 if is_selector thy sel then |
|
1255 let val x' = if not (loose_bvar1 (x,0)) |
|
1256 then Free ("x" ^ string_of_int i, range_type Tsel) |
|
1257 else raise TERM ("",[x]); |
|
1258 val sel' = Const (sel,Tsel)$Bound 0; |
|
1259 val (l,r) = if lr then (sel',x') else (x',sel'); |
|
1260 in Const ("op =",Teq)$l$r end |
|
1261 else raise TERM ("",[Const (sel,Tsel)]); |
|
1262 |
|
1263 fun dest_sel_eq (Const ("op =",Teq)$(Const (sel,Tsel)$Bound 0)$X) = |
|
1264 (true,Teq,(sel,Tsel),X) |
|
1265 | dest_sel_eq (Const ("op =",Teq)$X$(Const (sel,Tsel)$Bound 0)) = |
|
1266 (false,Teq,(sel,Tsel),X) |
|
1267 | dest_sel_eq _ = raise TERM ("",[]); |
|
1268 |
|
1269 in |
|
1270 (case t of |
|
1271 (Const ("Ex",Tex)$Abs(s,T,t)) => |
|
1272 (let val eq = mkeq (dest_sel_eq t) 0; |
|
1273 val prop = list_all ([("r",T)], |
|
1274 Logic.mk_equals (Const ("Ex",Tex)$Abs(s,T,eq), |
|
1275 HOLogic.true_const)); |
|
1276 in SOME (prove prop) end |
|
1277 handle TERM _ => NONE) |
|
1278 | _ => NONE) |
|
1279 end) |
|
1280 |
|
1281 |
|
1282 |
|
1283 |
|
1284 local |
|
1285 val inductive_atomize = thms "induct_atomize"; |
|
1286 val inductive_rulify = thms "induct_rulify"; |
|
1287 in |
|
1288 (* record_split_simp_tac *) |
|
1289 (* splits (and simplifies) all records in the goal for which P holds. |
|
1290 * For quantified occurrences of a record |
|
1291 * P can peek on the whole subterm (including the quantifier); for free variables P |
|
1292 * can only peek on the variable itself. |
|
1293 * P t = 0: do not split |
|
1294 * P t = ~1: completely split |
|
1295 * P t > 0: split up to given bound of record extensions |
|
1296 *) |
|
1297 fun record_split_simp_tac thms P i st = |
|
1298 let |
|
1299 val thy = Thm.theory_of_thm st; |
|
1300 |
|
1301 val has_rec = exists_Const |
|
1302 (fn (s, Type (_, [Type (_, [T, _]), _])) => |
|
1303 (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T |
|
1304 | _ => false); |
|
1305 |
|
1306 val goal = nth (Thm.prems_of st) (i - 1); |
|
1307 val frees = List.filter (is_recT o type_of) (OldTerm.term_frees goal); |
|
1308 |
|
1309 fun mk_split_free_tac free induct_thm i = |
|
1310 let val cfree = cterm_of thy free; |
|
1311 val (_$(_$r)) = concl_of induct_thm; |
|
1312 val crec = cterm_of thy r; |
|
1313 val thm = cterm_instantiate [(crec,cfree)] induct_thm; |
|
1314 in EVERY [simp_tac (HOL_basic_ss addsimps inductive_atomize) i, |
|
1315 rtac thm i, |
|
1316 simp_tac (HOL_basic_ss addsimps inductive_rulify) i] |
|
1317 end; |
|
1318 |
|
1319 fun split_free_tac P i (free as Free (n,T)) = |
|
1320 (case rec_id (~1) T of |
|
1321 "" => NONE |
|
1322 | name => let val split = P free |
|
1323 in if split <> 0 then |
|
1324 (case get_splits thy (rec_id split T) of |
|
1325 NONE => NONE |
|
1326 | SOME (_,_,_,induct_thm) |
|
1327 => SOME (mk_split_free_tac free induct_thm i)) |
|
1328 else NONE |
|
1329 end) |
|
1330 | split_free_tac _ _ _ = NONE; |
|
1331 |
|
1332 val split_frees_tacs = List.mapPartial (split_free_tac P i) frees; |
|
1333 |
|
1334 val simprocs = if has_rec goal then [record_split_simproc P] else []; |
|
1335 val thms' = K_comp_convs@thms |
|
1336 in st |> ((EVERY split_frees_tacs) |
|
1337 THEN (Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i)) |
|
1338 end handle Empty => Seq.empty; |
|
1339 end; |
|
1340 |
|
1341 |
|
1342 (* record_split_tac *) |
|
1343 (* splits all records in the goal, which are quantified by ! or !!. *) |
|
1344 fun record_split_tac i st = |
|
1345 let |
|
1346 val thy = Thm.theory_of_thm st; |
|
1347 |
|
1348 val has_rec = exists_Const |
|
1349 (fn (s, Type (_, [Type (_, [T, _]), _])) => |
|
1350 (s = "all" orelse s = "All") andalso is_recT T |
|
1351 | _ => false); |
|
1352 |
|
1353 val goal = nth (Thm.prems_of st) (i - 1); |
|
1354 |
|
1355 fun is_all t = |
|
1356 (case t of (Const (quantifier, _)$_) => |
|
1357 if quantifier = "All" orelse quantifier = "all" then ~1 else 0 |
|
1358 | _ => 0); |
|
1359 |
|
1360 in if has_rec goal |
|
1361 then Simplifier.full_simp_tac |
|
1362 (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i st |
|
1363 else Seq.empty |
|
1364 end handle Subscript => Seq.empty; |
|
1365 |
|
1366 (* wrapper *) |
|
1367 |
|
1368 val record_split_name = "record_split_tac"; |
|
1369 val record_split_wrapper = (record_split_name, fn tac => record_split_tac ORELSE' tac); |
|
1370 |
|
1371 |
|
1372 |
|
1373 (** theory extender interface **) |
|
1374 |
|
1375 (* prepare arguments *) |
|
1376 |
|
1377 fun read_raw_parent ctxt raw_T = |
|
1378 (case ProofContext.read_typ_abbrev ctxt raw_T of |
|
1379 Type (name, Ts) => (Ts, name) |
|
1380 | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T)); |
|
1381 |
|
1382 fun read_typ ctxt raw_T env = |
|
1383 let |
|
1384 val ctxt' = fold (Variable.declare_typ o TFree) env ctxt; |
|
1385 val T = Syntax.read_typ ctxt' raw_T; |
|
1386 val env' = OldTerm.add_typ_tfrees (T, env); |
|
1387 in (T, env') end; |
|
1388 |
|
1389 fun cert_typ ctxt raw_T env = |
|
1390 let |
|
1391 val thy = ProofContext.theory_of ctxt; |
|
1392 val T = Type.no_tvars (Sign.certify_typ thy raw_T) handle TYPE (msg, _, _) => error msg; |
|
1393 val env' = OldTerm.add_typ_tfrees (T, env); |
|
1394 in (T, env') end; |
|
1395 |
|
1396 |
|
1397 (* attributes *) |
|
1398 |
|
1399 fun case_names_fields x = RuleCases.case_names ["fields"] x; |
|
1400 fun induct_type_global name = [case_names_fields, Induct.induct_type name]; |
|
1401 fun cases_type_global name = [case_names_fields, Induct.cases_type name]; |
|
1402 |
|
1403 (* tactics *) |
|
1404 |
|
1405 fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps)); |
|
1406 |
|
1407 (* do case analysis / induction according to rule on last parameter of ith subgoal |
|
1408 * (or on s if there are no parameters); |
|
1409 * Instatiation of record variable (and predicate) in rule is calculated to |
|
1410 * avoid problems with higher order unification. |
|
1411 *) |
|
1412 |
|
1413 fun try_param_tac s rule i st = |
|
1414 let |
|
1415 val cert = cterm_of (Thm.theory_of_thm st); |
|
1416 val g = nth (prems_of st) (i - 1); |
|
1417 val params = Logic.strip_params g; |
|
1418 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g); |
|
1419 val rule' = Thm.lift_rule (Thm.cprem_of st i) rule; |
|
1420 val (P, ys) = strip_comb (HOLogic.dest_Trueprop |
|
1421 (Logic.strip_assums_concl (prop_of rule'))); |
|
1422 (* ca indicates if rule is a case analysis or induction rule *) |
|
1423 val (x, ca) = (case rev (Library.drop (length params, ys)) of |
|
1424 [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop |
|
1425 (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true) |
|
1426 | [x] => (head_of x, false)); |
|
1427 val rule'' = cterm_instantiate (map (pairself cert) (case (rev params) of |
|
1428 [] => (case AList.lookup (op =) (map dest_Free (OldTerm.term_frees (prop_of st))) s of |
|
1429 NONE => sys_error "try_param_tac: no such variable" |
|
1430 | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), |
|
1431 (x, Free (s, T))]) |
|
1432 | (_, T) :: _ => [(P, list_abs (params, if ca then concl |
|
1433 else incr_boundvars 1 (Abs (s, T, concl)))), |
|
1434 (x, list_abs (params, Bound 0))])) rule' |
|
1435 in compose_tac (false, rule'', nprems_of rule) i st end; |
|
1436 |
|
1437 |
|
1438 (* !!x1 ... xn. ... ==> EX x1 ... xn. P x1 ... xn; |
|
1439 instantiates x1 ... xn with parameters x1 ... xn *) |
|
1440 fun ex_inst_tac i st = |
|
1441 let |
|
1442 val thy = Thm.theory_of_thm st; |
|
1443 val g = nth (prems_of st) (i - 1); |
|
1444 val params = Logic.strip_params g; |
|
1445 val exI' = Thm.lift_rule (Thm.cprem_of st i) exI; |
|
1446 val (_$(_$x)) = Logic.strip_assums_concl (hd (prems_of exI')); |
|
1447 val cx = cterm_of thy (fst (strip_comb x)); |
|
1448 |
|
1449 in Seq.single (Library.foldl (fn (st,v) => |
|
1450 Seq.hd |
|
1451 (compose_tac (false, cterm_instantiate |
|
1452 [(cx,cterm_of thy (list_abs (params,Bound v)))] exI',1) |
|
1453 i st)) (st,((length params) - 1) downto 0)) |
|
1454 end; |
|
1455 |
|
1456 fun extension_typedef name repT alphas thy = |
|
1457 let |
|
1458 fun get_thms thy name = |
|
1459 let |
|
1460 val SOME { Abs_induct = abs_induct, |
|
1461 Abs_inject=abs_inject, Abs_inverse = abs_inverse, ...} = TypedefPackage.get_info thy name; |
|
1462 val rewrite_rule = MetaSimplifier.rewrite_rule [rec_UNIV_I, rec_True_simp]; |
|
1463 in map rewrite_rule [abs_inject, abs_inverse, abs_induct] end; |
|
1464 val tname = Binding.name (Long_Name.base_name name); |
|
1465 in |
|
1466 thy |
|
1467 |> TypecopyPackage.typecopy (Binding.suffix_name ext_typeN tname, alphas) repT NONE |
|
1468 |-> (fn (name, _) => `(fn thy => get_thms thy name)) |
|
1469 end; |
|
1470 |
|
1471 fun mixit convs refls = |
|
1472 let fun f ((res,lhs,rhs),refl) = ((refl,List.revAppend (lhs,refl::tl rhs))::res,hd rhs::lhs,tl rhs); |
|
1473 in #1 (Library.foldl f (([],[],convs),refls)) end; |
|
1474 |
|
1475 |
|
1476 fun extension_definition full name fields names alphas zeta moreT more vars thy = |
|
1477 let |
|
1478 val base = Long_Name.base_name; |
|
1479 val fieldTs = (map snd fields); |
|
1480 val alphas_zeta = alphas@[zeta]; |
|
1481 val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta; |
|
1482 val vT = TFree (Name.variant alphas_zeta "'v", HOLogic.typeS); |
|
1483 val extT_name = suffix ext_typeN name |
|
1484 val extT = Type (extT_name, alphas_zetaTs); |
|
1485 val repT = foldr1 HOLogic.mk_prodT (fieldTs@[moreT]); |
|
1486 val fields_more = fields@[(full moreN,moreT)]; |
|
1487 val fields_moreTs = fieldTs@[moreT]; |
|
1488 val bfields_more = map (apfst base) fields_more; |
|
1489 val r = Free (rN,extT) |
|
1490 val len = length fields; |
|
1491 val idxms = 0 upto len; |
|
1492 |
|
1493 (* prepare declarations and definitions *) |
|
1494 |
|
1495 (*fields constructor*) |
|
1496 val ext_decl = (mk_extC (name,extT) fields_moreTs); |
|
1497 (* |
|
1498 val ext_spec = Const ext_decl :== |
|
1499 (foldr (uncurry lambda) |
|
1500 (mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more]))) (vars@[more])) |
|
1501 *) |
|
1502 val ext_spec = list_comb (Const ext_decl,vars@[more]) :== |
|
1503 (mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more]))); |
|
1504 |
|
1505 fun mk_ext args = list_comb (Const ext_decl, args); |
|
1506 |
|
1507 (*destructors*) |
|
1508 val _ = timing_msg "record extension preparing definitions"; |
|
1509 val dest_decls = map (mk_selC extT o (apfst (suffix ext_dest))) bfields_more; |
|
1510 |
|
1511 fun mk_dest_spec (i, (c,T)) = |
|
1512 let val snds = (funpow i HOLogic.mk_snd (mk_Rep name repT extT $ r)) |
|
1513 in Const (mk_selC extT (suffix ext_dest c,T)) |
|
1514 :== (lambda r (if i=len then snds else HOLogic.mk_fst snds)) |
|
1515 end; |
|
1516 val dest_specs = |
|
1517 ListPair.map mk_dest_spec (idxms, fields_more); |
|
1518 |
|
1519 (*updates*) |
|
1520 val upd_decls = map (mk_updC updN extT) bfields_more; |
|
1521 fun mk_upd_spec (c,T) = |
|
1522 let |
|
1523 val args = map (fn (n,nT) => if n=c then Free (base c,T --> T)$ |
|
1524 (mk_sel r (suffix ext_dest n,nT)) |
|
1525 else (mk_sel r (suffix ext_dest n,nT))) |
|
1526 fields_more; |
|
1527 in Const (mk_updC updN extT (c,T))$(Free (base c,T --> T))$r |
|
1528 :== mk_ext args |
|
1529 end; |
|
1530 val upd_specs = map mk_upd_spec fields_more; |
|
1531 |
|
1532 (* 1st stage: defs_thy *) |
|
1533 fun mk_defs () = |
|
1534 thy |
|
1535 |> extension_typedef name repT (alphas @ [zeta]) |
|
1536 ||> Sign.add_consts_i |
|
1537 (map (Syntax.no_syn o apfst Binding.name) (apfst base ext_decl :: dest_decls @ upd_decls)) |
|
1538 ||>> PureThy.add_defs false |
|
1539 (map (Thm.no_attributes o apfst Binding.name) (ext_spec :: dest_specs)) |
|
1540 ||>> PureThy.add_defs false |
|
1541 (map (Thm.no_attributes o apfst Binding.name) upd_specs) |
|
1542 |-> (fn args as ((_, dest_defs), upd_defs) => |
|
1543 fold Code.add_default_eqn dest_defs |
|
1544 #> fold Code.add_default_eqn upd_defs |
|
1545 #> pair args); |
|
1546 val ((([abs_inject, abs_inverse, abs_induct], ext_def :: dest_defs), upd_defs), defs_thy) = |
|
1547 timeit_msg "record extension type/selector/update defs:" mk_defs; |
|
1548 |
|
1549 (* prepare propositions *) |
|
1550 val _ = timing_msg "record extension preparing propositions"; |
|
1551 val vars_more = vars@[more]; |
|
1552 val named_vars_more = (names@[full moreN])~~vars_more; |
|
1553 val variants = map (fn (Free (x,_))=>x) vars_more; |
|
1554 val ext = mk_ext vars_more; |
|
1555 val s = Free (rN, extT); |
|
1556 val w = Free (wN, extT); |
|
1557 val P = Free (Name.variant variants "P", extT-->HOLogic.boolT); |
|
1558 val C = Free (Name.variant variants "C", HOLogic.boolT); |
|
1559 |
|
1560 val inject_prop = |
|
1561 let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more; |
|
1562 in All (map dest_Free (vars_more@vars_more')) |
|
1563 ((HOLogic.eq_const extT $ |
|
1564 mk_ext vars_more$mk_ext vars_more') |
|
1565 === |
|
1566 foldr1 HOLogic.mk_conj (map HOLogic.mk_eq (vars_more ~~ vars_more'))) |
|
1567 end; |
|
1568 |
|
1569 val induct_prop = |
|
1570 (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s)); |
|
1571 |
|
1572 val cases_prop = |
|
1573 (All (map dest_Free vars_more) |
|
1574 (Trueprop (HOLogic.mk_eq (s,ext)) ==> Trueprop C)) |
|
1575 ==> Trueprop C; |
|
1576 |
|
1577 (*destructors*) |
|
1578 val dest_conv_props = |
|
1579 map (fn (c, x as Free (_,T)) => mk_sel ext (suffix ext_dest c,T) === x) named_vars_more; |
|
1580 |
|
1581 (*updates*) |
|
1582 fun mk_upd_prop (i,(c,T)) = |
|
1583 let val x' = Free (Name.variant variants (base c ^ "'"),T --> T) |
|
1584 val args' = nth_map i (K (x'$nth vars_more i)) vars_more |
|
1585 in mk_upd updN c x' ext === mk_ext args' end; |
|
1586 val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more); |
|
1587 |
|
1588 val surjective_prop = |
|
1589 let val args = |
|
1590 map (fn (c, Free (_,T)) => mk_sel s (suffix ext_dest c,T)) named_vars_more; |
|
1591 in s === mk_ext args end; |
|
1592 |
|
1593 val split_meta_prop = |
|
1594 let val P = Free (Name.variant variants "P", extT-->Term.propT) in |
|
1595 Logic.mk_equals |
|
1596 (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext)) |
|
1597 end; |
|
1598 |
|
1599 fun prove stndrd = quick_and_dirty_prove stndrd defs_thy; |
|
1600 val prove_standard = quick_and_dirty_prove true defs_thy; |
|
1601 fun prove_simp stndrd simps = |
|
1602 let val tac = simp_all_tac HOL_ss simps |
|
1603 in fn prop => prove stndrd [] prop (K tac) end; |
|
1604 |
|
1605 fun inject_prf () = (prove_simp true [ext_def,abs_inject,Pair_eq] inject_prop); |
|
1606 val inject = timeit_msg "record extension inject proof:" inject_prf; |
|
1607 |
|
1608 fun induct_prf () = |
|
1609 let val (assm, concl) = induct_prop |
|
1610 in prove_standard [assm] concl (fn {prems, ...} => |
|
1611 EVERY [try_param_tac rN abs_induct 1, |
|
1612 simp_tac (HOL_ss addsimps [split_paired_all]) 1, |
|
1613 resolve_tac (map (rewrite_rule [ext_def]) prems) 1]) |
|
1614 end; |
|
1615 val induct = timeit_msg "record extension induct proof:" induct_prf; |
|
1616 |
|
1617 fun cases_prf_opt () = |
|
1618 let |
|
1619 val (_$(Pvar$_)) = concl_of induct; |
|
1620 val ind = cterm_instantiate |
|
1621 [(cterm_of defs_thy Pvar, cterm_of defs_thy |
|
1622 (lambda w (HOLogic.imp$HOLogic.mk_eq(r,w)$C)))] |
|
1623 induct; |
|
1624 in standard (ObjectLogic.rulify (mp OF [ind, refl])) end; |
|
1625 |
|
1626 fun cases_prf_noopt () = |
|
1627 prove_standard [] cases_prop (fn _ => |
|
1628 EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1, |
|
1629 try_param_tac rN induct 1, |
|
1630 rtac impI 1, |
|
1631 REPEAT (etac allE 1), |
|
1632 etac mp 1, |
|
1633 rtac refl 1]) |
|
1634 |
|
1635 val cases_prf = quick_and_dirty_prf cases_prf_noopt cases_prf_opt; |
|
1636 val cases = timeit_msg "record extension cases proof:" cases_prf; |
|
1637 |
|
1638 fun dest_convs_prf () = map (prove_simp false |
|
1639 ([ext_def,abs_inverse]@Pair_sel_convs@dest_defs)) dest_conv_props; |
|
1640 val dest_convs = timeit_msg "record extension dest_convs proof:" dest_convs_prf; |
|
1641 fun dest_convs_standard_prf () = map standard dest_convs; |
|
1642 |
|
1643 val dest_convs_standard = |
|
1644 timeit_msg "record extension dest_convs_standard proof:" dest_convs_standard_prf; |
|
1645 |
|
1646 fun upd_convs_prf_noopt () = map (prove_simp true (dest_convs_standard@upd_defs)) |
|
1647 upd_conv_props; |
|
1648 fun upd_convs_prf_opt () = |
|
1649 let |
|
1650 |
|
1651 fun mkrefl (c,T) = Thm.reflexive |
|
1652 (cterm_of defs_thy (Free (Name.variant variants (base c ^ "'"),T-->T))); |
|
1653 val refls = map mkrefl fields_more; |
|
1654 val dest_convs' = map mk_meta_eq dest_convs; |
|
1655 val map_eqs = map (uncurry Thm.combination) (refls ~~ dest_convs'); |
|
1656 |
|
1657 val constr_refl = Thm.reflexive (cterm_of defs_thy (head_of ext)); |
|
1658 |
|
1659 fun mkthm (udef,(fld_refl,thms)) = |
|
1660 let val bdyeq = Library.foldl (uncurry Thm.combination) (constr_refl,thms); |
|
1661 (* (|N=N (|N=N,M=M,K=K,more=more|) |
|
1662 M=M (|N=N,M=M,K=K,more=more|) |
|
1663 K=K' |
|
1664 more = more (|N=N,M=M,K=K,more=more|) = |
|
1665 (|N=N,M=M,K=K',more=more|) |
|
1666 *) |
|
1667 val (_$(_$v$r)$_) = prop_of udef; |
|
1668 val (_$(v'$_)$_) = prop_of fld_refl; |
|
1669 val udef' = cterm_instantiate |
|
1670 [(cterm_of defs_thy v,cterm_of defs_thy v'), |
|
1671 (cterm_of defs_thy r,cterm_of defs_thy ext)] udef; |
|
1672 in standard (Thm.transitive udef' bdyeq) end; |
|
1673 in map mkthm (rev upd_defs ~~ (mixit dest_convs' map_eqs)) end; |
|
1674 |
|
1675 val upd_convs_prf = quick_and_dirty_prf upd_convs_prf_noopt upd_convs_prf_opt; |
|
1676 |
|
1677 val upd_convs = |
|
1678 timeit_msg "record extension upd_convs proof:" upd_convs_prf; |
|
1679 |
|
1680 fun surjective_prf () = |
|
1681 prove_standard [] surjective_prop (fn _ => |
|
1682 (EVERY [try_param_tac rN induct 1, |
|
1683 simp_tac (HOL_basic_ss addsimps dest_convs_standard) 1])); |
|
1684 val surjective = timeit_msg "record extension surjective proof:" surjective_prf; |
|
1685 |
|
1686 fun split_meta_prf () = |
|
1687 prove_standard [] split_meta_prop (fn _ => |
|
1688 EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1, |
|
1689 etac meta_allE 1, atac 1, |
|
1690 rtac (prop_subst OF [surjective]) 1, |
|
1691 REPEAT (etac meta_allE 1), atac 1]); |
|
1692 val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf; |
|
1693 |
|
1694 |
|
1695 val (([inject',induct',cases',surjective',split_meta'], |
|
1696 [dest_convs',upd_convs']), |
|
1697 thm_thy) = |
|
1698 defs_thy |
|
1699 |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name)) |
|
1700 [("ext_inject", inject), |
|
1701 ("ext_induct", induct), |
|
1702 ("ext_cases", cases), |
|
1703 ("ext_surjective", surjective), |
|
1704 ("ext_split", split_meta)] |
|
1705 ||>> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name)) |
|
1706 [("dest_convs", dest_convs_standard), ("upd_convs", upd_convs)] |
|
1707 |
|
1708 in (thm_thy,extT,induct',inject',dest_convs',split_meta',upd_convs') |
|
1709 end; |
|
1710 |
|
1711 fun chunks [] [] = [] |
|
1712 | chunks [] xs = [xs] |
|
1713 | chunks (l::ls) xs = Library.take (l,xs)::chunks ls (Library.drop (l,xs)); |
|
1714 |
|
1715 fun chop_last [] = error "last: list should not be empty" |
|
1716 | chop_last [x] = ([],x) |
|
1717 | chop_last (x::xs) = let val (tl,l) = chop_last xs in (x::tl,l) end; |
|
1718 |
|
1719 fun subst_last s [] = error "subst_last: list should not be empty" |
|
1720 | subst_last s ([x]) = [s] |
|
1721 | subst_last s (x::xs) = (x::subst_last s xs); |
|
1722 |
|
1723 (* mk_recordT builds up the record type from the current extension tpye extT and a list |
|
1724 * of parent extensions, starting with the root of the record hierarchy |
|
1725 *) |
|
1726 fun mk_recordT extT = |
|
1727 fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT; |
|
1728 |
|
1729 |
|
1730 |
|
1731 fun obj_to_meta_all thm = |
|
1732 let |
|
1733 fun E thm = case (SOME (spec OF [thm]) handle THM _ => NONE) of |
|
1734 SOME thm' => E thm' |
|
1735 | NONE => thm; |
|
1736 val th1 = E thm; |
|
1737 val th2 = Drule.forall_intr_vars th1; |
|
1738 in th2 end; |
|
1739 |
|
1740 fun meta_to_obj_all thm = |
|
1741 let |
|
1742 val thy = Thm.theory_of_thm thm; |
|
1743 val prop = Thm.prop_of thm; |
|
1744 val params = Logic.strip_params prop; |
|
1745 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop); |
|
1746 val ct = cterm_of thy |
|
1747 (HOLogic.mk_Trueprop (HOLogic.list_all (params, concl))); |
|
1748 val thm' = Seq.hd (REPEAT (rtac allI 1) (Thm.trivial ct)); |
|
1749 in |
|
1750 Thm.implies_elim thm' thm |
|
1751 end; |
|
1752 |
|
1753 |
|
1754 |
|
1755 (* record_definition *) |
|
1756 |
|
1757 fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy = |
|
1758 let |
|
1759 val external_names = NameSpace.external_names (Sign.naming_of thy); |
|
1760 |
|
1761 val alphas = map fst args; |
|
1762 val name = Sign.full_bname thy bname; |
|
1763 val full = Sign.full_bname_path thy bname; |
|
1764 val base = Long_Name.base_name; |
|
1765 |
|
1766 val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields); |
|
1767 |
|
1768 val parent_fields = List.concat (map #fields parents); |
|
1769 val parent_chunks = map (length o #fields) parents; |
|
1770 val parent_names = map fst parent_fields; |
|
1771 val parent_types = map snd parent_fields; |
|
1772 val parent_fields_len = length parent_fields; |
|
1773 val parent_variants = Name.variant_list [moreN, rN, rN ^ "'", wN] (map base parent_names); |
|
1774 val parent_vars = ListPair.map Free (parent_variants, parent_types); |
|
1775 val parent_len = length parents; |
|
1776 val parents_idx = (map #name parents) ~~ (0 upto (parent_len - 1)); |
|
1777 |
|
1778 val fields = map (apfst full) bfields; |
|
1779 val names = map fst fields; |
|
1780 val extN = full bname; |
|
1781 val types = map snd fields; |
|
1782 val alphas_fields = List.foldr OldTerm.add_typ_tfree_names [] types; |
|
1783 val alphas_ext = alphas inter alphas_fields; |
|
1784 val len = length fields; |
|
1785 val variants = |
|
1786 Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants) (map fst bfields); |
|
1787 val vars = ListPair.map Free (variants, types); |
|
1788 val named_vars = names ~~ vars; |
|
1789 val idxs = 0 upto (len - 1); |
|
1790 val idxms = 0 upto len; |
|
1791 |
|
1792 val all_fields = parent_fields @ fields; |
|
1793 val all_names = parent_names @ names; |
|
1794 val all_types = parent_types @ types; |
|
1795 val all_len = parent_fields_len + len; |
|
1796 val all_variants = parent_variants @ variants; |
|
1797 val all_vars = parent_vars @ vars; |
|
1798 val all_named_vars = (parent_names ~~ parent_vars) @ named_vars; |
|
1799 |
|
1800 |
|
1801 val zeta = Name.variant alphas "'z"; |
|
1802 val moreT = TFree (zeta, HOLogic.typeS); |
|
1803 val more = Free (moreN, moreT); |
|
1804 val full_moreN = full moreN; |
|
1805 val bfields_more = bfields @ [(moreN,moreT)]; |
|
1806 val fields_more = fields @ [(full_moreN,moreT)]; |
|
1807 val vars_more = vars @ [more]; |
|
1808 val named_vars_more = named_vars @[(full_moreN,more)]; |
|
1809 val all_vars_more = all_vars @ [more]; |
|
1810 val all_named_vars_more = all_named_vars @ [(full_moreN,more)]; |
|
1811 |
|
1812 (* 1st stage: extension_thy *) |
|
1813 val (extension_thy,extT,ext_induct,ext_inject,ext_dest_convs,ext_split,u_convs) = |
|
1814 thy |
|
1815 |> Sign.add_path bname |
|
1816 |> extension_definition full extN fields names alphas_ext zeta moreT more vars; |
|
1817 |
|
1818 val _ = timing_msg "record preparing definitions"; |
|
1819 val Type extension_scheme = extT; |
|
1820 val extension_name = unsuffix ext_typeN (fst extension_scheme); |
|
1821 val extension = let val (n,Ts) = extension_scheme in (n,subst_last HOLogic.unitT Ts) end; |
|
1822 val extension_names = |
|
1823 (map ((unsuffix ext_typeN) o fst o #extension) parents) @ [extN]; |
|
1824 val extension_id = Library.foldl (op ^) ("",extension_names); |
|
1825 |
|
1826 |
|
1827 fun rec_schemeT n = mk_recordT (map #extension (prune n parents)) extT; |
|
1828 val rec_schemeT0 = rec_schemeT 0; |
|
1829 |
|
1830 fun recT n = |
|
1831 let val (c,Ts) = extension |
|
1832 in mk_recordT (map #extension (prune n parents)) (Type (c,subst_last HOLogic.unitT Ts)) |
|
1833 end; |
|
1834 val recT0 = recT 0; |
|
1835 |
|
1836 fun mk_rec args n = |
|
1837 let val (args',more) = chop_last args; |
|
1838 fun mk_ext' (((name,T),args),more) = mk_ext (name,T) (args@[more]); |
|
1839 fun build Ts = |
|
1840 List.foldr mk_ext' more (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args'))) |
|
1841 in |
|
1842 if more = HOLogic.unit |
|
1843 then build (map recT (0 upto parent_len)) |
|
1844 else build (map rec_schemeT (0 upto parent_len)) |
|
1845 end; |
|
1846 |
|
1847 val r_rec0 = mk_rec all_vars_more 0; |
|
1848 val r_rec_unit0 = mk_rec (all_vars@[HOLogic.unit]) 0; |
|
1849 |
|
1850 fun r n = Free (rN, rec_schemeT n) |
|
1851 val r0 = r 0; |
|
1852 fun r_unit n = Free (rN, recT n) |
|
1853 val r_unit0 = r_unit 0; |
|
1854 val w = Free (wN, rec_schemeT 0) |
|
1855 |
|
1856 (* prepare print translation functions *) |
|
1857 val field_tr's = |
|
1858 print_translation (distinct (op =) (maps external_names (full_moreN :: names))); |
|
1859 |
|
1860 val adv_ext_tr's = |
|
1861 let |
|
1862 val trnames = external_names extN; |
|
1863 in map (gen_record_tr') trnames end; |
|
1864 |
|
1865 val adv_record_type_abbr_tr's = |
|
1866 let val trnames = external_names (hd extension_names); |
|
1867 val lastExt = unsuffix ext_typeN (fst extension); |
|
1868 in map (gen_record_type_abbr_tr' name alphas zeta lastExt rec_schemeT0) trnames |
|
1869 end; |
|
1870 |
|
1871 val adv_record_type_tr's = |
|
1872 let val trnames = if parent_len > 0 then external_names extN else []; |
|
1873 (* avoid conflict with adv_record_type_abbr_tr's *) |
|
1874 in map (gen_record_type_tr') trnames |
|
1875 end; |
|
1876 |
|
1877 |
|
1878 (* prepare declarations *) |
|
1879 |
|
1880 val sel_decls = map (mk_selC rec_schemeT0) bfields_more; |
|
1881 val upd_decls = map (mk_updC updateN rec_schemeT0) bfields_more; |
|
1882 val make_decl = (makeN, all_types ---> recT0); |
|
1883 val fields_decl = (fields_selN, types ---> Type extension); |
|
1884 val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0); |
|
1885 val truncate_decl = (truncateN, rec_schemeT0 --> recT0); |
|
1886 |
|
1887 (* prepare definitions *) |
|
1888 |
|
1889 fun parent_more s = |
|
1890 if null parents then s |
|
1891 else mk_sel s (Long_Name.qualify (#name (List.last parents)) moreN, extT); |
|
1892 |
|
1893 fun parent_more_upd v s = |
|
1894 if null parents then v$s |
|
1895 else let val mp = Long_Name.qualify (#name (List.last parents)) moreN; |
|
1896 in mk_upd updateN mp v s end; |
|
1897 |
|
1898 (*record (scheme) type abbreviation*) |
|
1899 val recordT_specs = |
|
1900 [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn), |
|
1901 (Binding.name bname, alphas, recT0, Syntax.NoSyn)]; |
|
1902 |
|
1903 (*selectors*) |
|
1904 fun mk_sel_spec (c,T) = |
|
1905 Const (mk_selC rec_schemeT0 (c,T)) |
|
1906 :== (lambda r0 (Const (mk_selC extT (suffix ext_dest c,T))$parent_more r0)); |
|
1907 val sel_specs = map mk_sel_spec fields_more; |
|
1908 |
|
1909 (*updates*) |
|
1910 |
|
1911 fun mk_upd_spec (c,T) = |
|
1912 let |
|
1913 val new = mk_upd' updN c (Free (base c,T-->T)) extT(*(parent_more r0)*); |
|
1914 in Const (mk_updC updateN rec_schemeT0 (c,T))$(Free (base c,T-->T))$r0 |
|
1915 :== (parent_more_upd new r0) |
|
1916 end; |
|
1917 val upd_specs = map mk_upd_spec fields_more; |
|
1918 |
|
1919 (*derived operations*) |
|
1920 val make_spec = Const (full makeN, all_types ---> recT0) $$ all_vars :== |
|
1921 mk_rec (all_vars @ [HOLogic.unit]) 0; |
|
1922 val fields_spec = Const (full fields_selN, types ---> Type extension) $$ vars :== |
|
1923 mk_rec (all_vars @ [HOLogic.unit]) parent_len; |
|
1924 val extend_spec = |
|
1925 Const (full extendN, recT0-->moreT-->rec_schemeT0) $ r_unit0 $ more :== |
|
1926 mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0; |
|
1927 val truncate_spec = Const (full truncateN, rec_schemeT0 --> recT0) $ r0 :== |
|
1928 mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0; |
|
1929 |
|
1930 (* 2st stage: defs_thy *) |
|
1931 |
|
1932 fun mk_defs () = |
|
1933 extension_thy |
|
1934 |> Sign.add_trfuns |
|
1935 ([],[],field_tr's, []) |
|
1936 |> Sign.add_advanced_trfuns |
|
1937 ([],[],adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's,[]) |
|
1938 |> Sign.parent_path |
|
1939 |> Sign.add_tyabbrs_i recordT_specs |
|
1940 |> Sign.add_path bname |
|
1941 |> Sign.add_consts_i |
|
1942 (map2 (fn (x, T) => fn mx => (Binding.name x, T, mx)) |
|
1943 sel_decls (field_syntax @ [Syntax.NoSyn])) |
|
1944 |> (Sign.add_consts_i o map (fn (x, T) => (Binding.name x, T, Syntax.NoSyn))) |
|
1945 (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl]) |
|
1946 |> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) sel_specs) |
|
1947 ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) upd_specs) |
|
1948 ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) |
|
1949 [make_spec, fields_spec, extend_spec, truncate_spec]) |
|
1950 |-> (fn defs as ((sel_defs, upd_defs), derived_defs) => |
|
1951 fold Code.add_default_eqn sel_defs |
|
1952 #> fold Code.add_default_eqn upd_defs |
|
1953 #> fold Code.add_default_eqn derived_defs |
|
1954 #> pair defs) |
|
1955 val (((sel_defs, upd_defs), derived_defs), defs_thy) = |
|
1956 timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:" |
|
1957 mk_defs; |
|
1958 |
|
1959 |
|
1960 (* prepare propositions *) |
|
1961 val _ = timing_msg "record preparing propositions"; |
|
1962 val P = Free (Name.variant all_variants "P", rec_schemeT0-->HOLogic.boolT); |
|
1963 val C = Free (Name.variant all_variants "C", HOLogic.boolT); |
|
1964 val P_unit = Free (Name.variant all_variants "P", recT0-->HOLogic.boolT); |
|
1965 |
|
1966 (*selectors*) |
|
1967 val sel_conv_props = |
|
1968 map (fn (c, x as Free (_,T)) => mk_sel r_rec0 (c,T) === x) named_vars_more; |
|
1969 |
|
1970 (*updates*) |
|
1971 fun mk_upd_prop (i,(c,T)) = |
|
1972 let val x' = Free (Name.variant all_variants (base c ^ "'"),T-->T); |
|
1973 val n = parent_fields_len + i; |
|
1974 val args' = nth_map n (K (x'$nth all_vars_more n)) all_vars_more |
|
1975 in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end; |
|
1976 val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more); |
|
1977 |
|
1978 (*induct*) |
|
1979 val induct_scheme_prop = |
|
1980 All (map dest_Free all_vars_more) (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0); |
|
1981 val induct_prop = |
|
1982 (All (map dest_Free all_vars) (Trueprop (P_unit $ r_rec_unit0)), |
|
1983 Trueprop (P_unit $ r_unit0)); |
|
1984 |
|
1985 (*surjective*) |
|
1986 val surjective_prop = |
|
1987 let val args = map (fn (c,Free (_,T)) => mk_sel r0 (c,T)) all_named_vars_more |
|
1988 in r0 === mk_rec args 0 end; |
|
1989 |
|
1990 (*cases*) |
|
1991 val cases_scheme_prop = |
|
1992 (All (map dest_Free all_vars_more) |
|
1993 (Trueprop (HOLogic.mk_eq (r0,r_rec0)) ==> Trueprop C)) |
|
1994 ==> Trueprop C; |
|
1995 |
|
1996 val cases_prop = |
|
1997 (All (map dest_Free all_vars) |
|
1998 (Trueprop (HOLogic.mk_eq (r_unit0,r_rec_unit0)) ==> Trueprop C)) |
|
1999 ==> Trueprop C; |
|
2000 |
|
2001 (*split*) |
|
2002 val split_meta_prop = |
|
2003 let val P = Free (Name.variant all_variants "P", rec_schemeT0-->Term.propT) in |
|
2004 Logic.mk_equals |
|
2005 (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0)) |
|
2006 end; |
|
2007 |
|
2008 val split_object_prop = |
|
2009 let fun ALL vs t = List.foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) t vs |
|
2010 in (ALL [dest_Free r0] (P $ r0)) === (ALL (map dest_Free all_vars_more) (P $ r_rec0)) |
|
2011 end; |
|
2012 |
|
2013 |
|
2014 val split_ex_prop = |
|
2015 let fun EX vs t = List.foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) t vs |
|
2016 in (EX [dest_Free r0] (P $ r0)) === (EX (map dest_Free all_vars_more) (P $ r_rec0)) |
|
2017 end; |
|
2018 |
|
2019 (*equality*) |
|
2020 val equality_prop = |
|
2021 let |
|
2022 val s' = Free (rN ^ "'", rec_schemeT0) |
|
2023 fun mk_sel_eq (c,Free (_,T)) = mk_sel r0 (c,T) === mk_sel s' (c,T) |
|
2024 val seleqs = map mk_sel_eq all_named_vars_more |
|
2025 in All (map dest_Free [r0,s']) (Logic.list_implies (seleqs,r0 === s')) end; |
|
2026 |
|
2027 (* 3rd stage: thms_thy *) |
|
2028 |
|
2029 fun prove stndrd = quick_and_dirty_prove stndrd defs_thy; |
|
2030 val prove_standard = quick_and_dirty_prove true defs_thy; |
|
2031 |
|
2032 fun prove_simp stndrd ss simps = |
|
2033 let val tac = simp_all_tac ss simps |
|
2034 in fn prop => prove stndrd [] prop (K tac) end; |
|
2035 |
|
2036 val ss = get_simpset defs_thy; |
|
2037 |
|
2038 fun sel_convs_prf () = map (prove_simp false ss |
|
2039 (sel_defs@ext_dest_convs)) sel_conv_props; |
|
2040 val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf; |
|
2041 fun sel_convs_standard_prf () = map standard sel_convs |
|
2042 val sel_convs_standard = |
|
2043 timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf; |
|
2044 |
|
2045 fun upd_convs_prf () = |
|
2046 map (prove_simp true ss (upd_defs@u_convs)) upd_conv_props; |
|
2047 |
|
2048 val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf; |
|
2049 |
|
2050 val parent_induct = if null parents then [] else [#induct (hd (rev parents))]; |
|
2051 |
|
2052 fun induct_scheme_prf () = prove_standard [] induct_scheme_prop (fn _ => |
|
2053 (EVERY [if null parent_induct |
|
2054 then all_tac else try_param_tac rN (hd parent_induct) 1, |
|
2055 try_param_tac rN ext_induct 1, |
|
2056 asm_simp_tac HOL_basic_ss 1])); |
|
2057 val induct_scheme = timeit_msg "record induct_scheme proof:" induct_scheme_prf; |
|
2058 |
|
2059 fun induct_prf () = |
|
2060 let val (assm, concl) = induct_prop; |
|
2061 in |
|
2062 prove_standard [assm] concl (fn {prems, ...} => |
|
2063 try_param_tac rN induct_scheme 1 |
|
2064 THEN try_param_tac "more" @{thm unit.induct} 1 |
|
2065 THEN resolve_tac prems 1) |
|
2066 end; |
|
2067 val induct = timeit_msg "record induct proof:" induct_prf; |
|
2068 |
|
2069 fun surjective_prf () = |
|
2070 prove_standard [] surjective_prop (fn prems => |
|
2071 (EVERY [try_param_tac rN induct_scheme 1, |
|
2072 simp_tac (ss addsimps sel_convs_standard) 1])) |
|
2073 val surjective = timeit_msg "record surjective proof:" surjective_prf; |
|
2074 |
|
2075 fun cases_scheme_prf_opt () = |
|
2076 let |
|
2077 val (_$(Pvar$_)) = concl_of induct_scheme; |
|
2078 val ind = cterm_instantiate |
|
2079 [(cterm_of defs_thy Pvar, cterm_of defs_thy |
|
2080 (lambda w (HOLogic.imp$HOLogic.mk_eq(r0,w)$C)))] |
|
2081 induct_scheme; |
|
2082 in standard (ObjectLogic.rulify (mp OF [ind, refl])) end; |
|
2083 |
|
2084 fun cases_scheme_prf_noopt () = |
|
2085 prove_standard [] cases_scheme_prop (fn _ => |
|
2086 EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1, |
|
2087 try_param_tac rN induct_scheme 1, |
|
2088 rtac impI 1, |
|
2089 REPEAT (etac allE 1), |
|
2090 etac mp 1, |
|
2091 rtac refl 1]) |
|
2092 val cases_scheme_prf = quick_and_dirty_prf cases_scheme_prf_noopt cases_scheme_prf_opt; |
|
2093 val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf; |
|
2094 |
|
2095 fun cases_prf () = |
|
2096 prove_standard [] cases_prop (fn _ => |
|
2097 try_param_tac rN cases_scheme 1 |
|
2098 THEN simp_all_tac HOL_basic_ss [unit_all_eq1]); |
|
2099 val cases = timeit_msg "record cases proof:" cases_prf; |
|
2100 |
|
2101 fun split_meta_prf () = |
|
2102 prove false [] split_meta_prop (fn _ => |
|
2103 EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1, |
|
2104 etac meta_allE 1, atac 1, |
|
2105 rtac (prop_subst OF [surjective]) 1, |
|
2106 REPEAT (etac meta_allE 1), atac 1]); |
|
2107 val split_meta = timeit_msg "record split_meta proof:" split_meta_prf; |
|
2108 val split_meta_standard = standard split_meta; |
|
2109 |
|
2110 fun split_object_prf_opt () = |
|
2111 let |
|
2112 val cPI= cterm_of defs_thy (lambda r0 (Trueprop (P$r0))); |
|
2113 val (_$Abs(_,_,P$_)) = fst (Logic.dest_equals (concl_of split_meta_standard)); |
|
2114 val cP = cterm_of defs_thy P; |
|
2115 val split_meta' = cterm_instantiate [(cP,cPI)] split_meta_standard; |
|
2116 val (l,r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop); |
|
2117 val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l); |
|
2118 val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r); |
|
2119 val thl = assume cl (*All r. P r*) (* 1 *) |
|
2120 |> obj_to_meta_all (*!!r. P r*) |
|
2121 |> equal_elim split_meta' (*!!n m more. P (ext n m more)*) |
|
2122 |> meta_to_obj_all (*All n m more. P (ext n m more)*) (* 2*) |
|
2123 |> implies_intr cl (* 1 ==> 2 *) |
|
2124 val thr = assume cr (*All n m more. P (ext n m more)*) |
|
2125 |> obj_to_meta_all (*!!n m more. P (ext n m more)*) |
|
2126 |> equal_elim (symmetric split_meta') (*!!r. P r*) |
|
2127 |> meta_to_obj_all (*All r. P r*) |
|
2128 |> implies_intr cr (* 2 ==> 1 *) |
|
2129 in standard (thr COMP (thl COMP iffI)) end; |
|
2130 |
|
2131 fun split_object_prf_noopt () = |
|
2132 prove_standard [] split_object_prop (fn _ => |
|
2133 EVERY [rtac iffI 1, |
|
2134 REPEAT (rtac allI 1), etac allE 1, atac 1, |
|
2135 rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]); |
|
2136 |
|
2137 val split_object_prf = quick_and_dirty_prf split_object_prf_noopt split_object_prf_opt; |
|
2138 val split_object = timeit_msg "record split_object proof:" split_object_prf; |
|
2139 |
|
2140 |
|
2141 fun split_ex_prf () = |
|
2142 prove_standard [] split_ex_prop (fn _ => |
|
2143 EVERY [rtac iffI 1, |
|
2144 etac exE 1, |
|
2145 simp_tac (HOL_basic_ss addsimps [split_meta_standard]) 1, |
|
2146 ex_inst_tac 1, |
|
2147 (*REPEAT (rtac exI 1),*) |
|
2148 atac 1, |
|
2149 REPEAT (etac exE 1), |
|
2150 rtac exI 1, |
|
2151 atac 1]); |
|
2152 val split_ex = timeit_msg "record split_ex proof:" split_ex_prf; |
|
2153 |
|
2154 fun equality_tac thms = |
|
2155 let val (s'::s::eqs) = rev thms; |
|
2156 val ss' = ss addsimps (s'::s::sel_convs_standard); |
|
2157 val eqs' = map (simplify ss') eqs; |
|
2158 in simp_tac (HOL_basic_ss addsimps (s'::s::eqs')) 1 end; |
|
2159 |
|
2160 fun equality_prf () = prove_standard [] equality_prop (fn {context, ...} => |
|
2161 fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in |
|
2162 st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1 |
|
2163 THEN res_inst_tac context [((rN, 0), s')] cases_scheme 1 |
|
2164 THEN (METAHYPS equality_tac 1)) |
|
2165 (* simp_all_tac ss (sel_convs) would also work but is less efficient *) |
|
2166 end); |
|
2167 val equality = timeit_msg "record equality proof:" equality_prf; |
|
2168 |
|
2169 val ((([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],derived_defs'], |
|
2170 [surjective',equality']),[induct_scheme',induct',cases_scheme',cases']), thms_thy) = |
|
2171 defs_thy |
|
2172 |> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name)) |
|
2173 [("select_convs", sel_convs_standard), |
|
2174 ("update_convs", upd_convs), |
|
2175 ("select_defs", sel_defs), |
|
2176 ("update_defs", upd_defs), |
|
2177 ("splits", [split_meta_standard,split_object,split_ex]), |
|
2178 ("defs", derived_defs)] |
|
2179 ||>> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name)) |
|
2180 [("surjective", surjective), |
|
2181 ("equality", equality)] |
|
2182 ||>> (PureThy.add_thms o (map o apfst o apfst) Binding.name) |
|
2183 [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)), |
|
2184 (("induct", induct), induct_type_global name), |
|
2185 (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)), |
|
2186 (("cases", cases), cases_type_global name)]; |
|
2187 |
|
2188 |
|
2189 val sel_upd_simps = sel_convs' @ upd_convs'; |
|
2190 val iffs = [ext_inject] |
|
2191 val final_thy = |
|
2192 thms_thy |
|
2193 |> (snd oo PureThy.add_thmss) |
|
2194 [((Binding.name "simps", sel_upd_simps), |
|
2195 [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]), |
|
2196 ((Binding.name "iffs", iffs), [iff_add])] |
|
2197 |> put_record name (make_record_info args parent fields extension induct_scheme') |
|
2198 |> put_sel_upd (names @ [full_moreN]) sel_upd_simps |
|
2199 |> add_record_equalities extension_id equality' |
|
2200 |> add_extinjects ext_inject |
|
2201 |> add_extsplit extension_name ext_split |
|
2202 |> add_record_splits extension_id (split_meta',split_object',split_ex',induct_scheme') |
|
2203 |> add_extfields extension_name (fields @ [(full_moreN,moreT)]) |
|
2204 |> add_fieldext (extension_name,snd extension) (names @ [full_moreN]) |
|
2205 |> Sign.parent_path; |
|
2206 |
|
2207 in final_thy |
|
2208 end; |
|
2209 |
|
2210 |
|
2211 (* add_record *) |
|
2212 |
|
2213 (*we do all preparations and error checks here, deferring the real |
|
2214 work to record_definition*) |
|
2215 fun gen_add_record prep_typ prep_raw_parent quiet_mode (params, bname) raw_parent raw_fields thy = |
|
2216 let |
|
2217 val _ = Theory.requires thy "Record" "record definitions"; |
|
2218 val _ = if quiet_mode then () else writeln ("Defining record " ^ quote bname ^ " ..."); |
|
2219 |
|
2220 val ctxt = ProofContext.init thy; |
|
2221 |
|
2222 |
|
2223 (* parents *) |
|
2224 |
|
2225 fun prep_inst T = fst (cert_typ ctxt T []); |
|
2226 |
|
2227 val parent = Option.map (apfst (map prep_inst) o prep_raw_parent ctxt) raw_parent |
|
2228 handle ERROR msg => cat_error msg ("The error(s) above in parent record specification"); |
|
2229 val parents = add_parents thy parent []; |
|
2230 |
|
2231 val init_env = |
|
2232 (case parent of |
|
2233 NONE => [] |
|
2234 | SOME (types, _) => List.foldr OldTerm.add_typ_tfrees [] types); |
|
2235 |
|
2236 |
|
2237 (* fields *) |
|
2238 |
|
2239 fun prep_field (c, raw_T, mx) env = |
|
2240 let val (T, env') = prep_typ ctxt raw_T env handle ERROR msg => |
|
2241 cat_error msg ("The error(s) above occured in record field " ^ quote c) |
|
2242 in ((c, T, mx), env') end; |
|
2243 |
|
2244 val (bfields, envir) = fold_map prep_field raw_fields init_env; |
|
2245 val envir_names = map fst envir; |
|
2246 |
|
2247 |
|
2248 (* args *) |
|
2249 |
|
2250 val defaultS = Sign.defaultS thy; |
|
2251 val args = map (fn x => (x, AList.lookup (op =) envir x |> the_default defaultS)) params; |
|
2252 |
|
2253 |
|
2254 (* errors *) |
|
2255 |
|
2256 val name = Sign.full_bname thy bname; |
|
2257 val err_dup_record = |
|
2258 if is_none (get_record thy name) then [] |
|
2259 else ["Duplicate definition of record " ^ quote name]; |
|
2260 |
|
2261 val err_dup_parms = |
|
2262 (case duplicates (op =) params of |
|
2263 [] => [] |
|
2264 | dups => ["Duplicate parameter(s) " ^ commas dups]); |
|
2265 |
|
2266 val err_extra_frees = |
|
2267 (case subtract (op =) params envir_names of |
|
2268 [] => [] |
|
2269 | extras => ["Extra free type variable(s) " ^ commas extras]); |
|
2270 |
|
2271 val err_no_fields = if null bfields then ["No fields present"] else []; |
|
2272 |
|
2273 val err_dup_fields = |
|
2274 (case duplicates (op =) (map #1 bfields) of |
|
2275 [] => [] |
|
2276 | dups => ["Duplicate field(s) " ^ commas_quote dups]); |
|
2277 |
|
2278 val err_bad_fields = |
|
2279 if forall (not_equal moreN o #1) bfields then [] |
|
2280 else ["Illegal field name " ^ quote moreN]; |
|
2281 |
|
2282 val err_dup_sorts = |
|
2283 (case duplicates (op =) envir_names of |
|
2284 [] => [] |
|
2285 | dups => ["Inconsistent sort constraints for " ^ commas dups]); |
|
2286 |
|
2287 val errs = |
|
2288 err_dup_record @ err_dup_parms @ err_extra_frees @ err_no_fields @ |
|
2289 err_dup_fields @ err_bad_fields @ err_dup_sorts; |
|
2290 in |
|
2291 if null errs then () else error (cat_lines errs) ; |
|
2292 thy |> record_definition (args, bname) parent parents bfields |
|
2293 end |
|
2294 handle ERROR msg => cat_error msg ("Failed to define record " ^ quote bname); |
|
2295 |
|
2296 val add_record = gen_add_record read_typ read_raw_parent; |
|
2297 val add_record_i = gen_add_record cert_typ (K I); |
|
2298 |
|
2299 (* setup theory *) |
|
2300 |
|
2301 val setup = |
|
2302 Sign.add_trfuns ([], parse_translation, [], []) #> |
|
2303 Sign.add_advanced_trfuns ([], adv_parse_translation, [], []) #> |
|
2304 Simplifier.map_simpset (fn ss => |
|
2305 ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]); |
|
2306 |
|
2307 (* outer syntax *) |
|
2308 |
|
2309 local structure P = OuterParse and K = OuterKeyword in |
|
2310 |
|
2311 val record_decl = |
|
2312 P.type_args -- P.name -- |
|
2313 (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const); |
|
2314 |
|
2315 val _ = |
|
2316 OuterSyntax.command "record" "define extensible record" K.thy_decl |
|
2317 (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record false x y z))); |
|
2318 |
|
2319 end; |
|
2320 |
|
2321 end; |
|
2322 |
|
2323 |
|
2324 structure BasicRecordPackage: BASIC_RECORD_PACKAGE = RecordPackage; |
|
2325 open BasicRecordPackage; |
|