clarified record syntax: fieldext excludes the "more" pseudo-field (unlike 2f885b7e5ba7), so that errors like (| x = a, more = b |) are reported less confusingly;
1 (* Title: HOL/Tools/record.ML
2 Author: Wolfgang Naraschewski, TU Muenchen
3 Author: Markus Wenzel, TU Muenchen
4 Author: Norbert Schirmer, TU Muenchen
5 Author: Thomas Sewell, NICTA
7 Extensible records with structural subtyping.
12 val type_abbr: bool Config.T
13 val type_as_fields: bool Config.T
14 val timing: bool Config.T
17 {args: (string * sort) list,
18 parent: (typ list * string) option,
19 fields: (string * typ) list,
20 extension: (string * typ list),
21 ext_induct: thm, ext_inject: thm, ext_surjective: thm, ext_split: thm, ext_def: thm,
22 select_convs: thm list, update_convs: thm list, select_defs: thm list, update_defs: thm list,
23 fold_congs: thm list, unfold_congs: thm list, splits: thm list, defs: thm list,
24 surjective: thm, equality: thm, induct_scheme: thm, induct: thm, cases_scheme: thm,
25 cases: thm, simps: thm list, iffs: thm list}
26 val get_info: theory -> string -> info option
27 val the_info: theory -> string -> info
28 val get_hierarchy: theory -> (string * typ list) -> (string * ((string * sort) * typ) list) list
29 val add_record: bool -> (string * sort) list * binding -> (typ list * string) option ->
30 (binding * typ * mixfix) list -> theory -> theory
32 val last_extT: typ -> (string * typ list) option
33 val dest_recTs: typ -> (string * typ list) list
34 val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ)
35 val get_recT_fields: theory -> typ -> (string * typ) list * (string * typ)
36 val get_parent: theory -> string -> (typ list * string) option
37 val get_extension: theory -> string -> (string * typ list) option
38 val get_extinjects: theory -> thm list
39 val get_simpset: theory -> simpset
41 val eq_simproc: simproc
42 val upd_simproc: simproc
43 val split_simproc: (term -> int) -> simproc
44 val ex_sel_eq_simproc: simproc
45 val split_tac: int -> tactic
46 val split_simp_tac: thm list -> (term -> int) -> int -> tactic
47 val split_wrapper: string * (Proof.context -> wrapper)
52 val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list
53 val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list
54 val setup: theory -> theory
58 signature ISO_TUPLE_SUPPORT =
60 val add_iso_tuple_type: binding * (string * sort) list ->
61 typ * typ -> theory -> (term * term) * theory
62 val mk_cons_tuple: term * term -> term
63 val dest_cons_tuple: term -> term * term
64 val iso_tuple_intros_tac: int -> tactic
65 val named_cterm_instantiate: (string * cterm) list -> thm -> thm
68 structure Iso_Tuple_Support: ISO_TUPLE_SUPPORT =
71 val isoN = "_Tuple_Iso";
73 val iso_tuple_intro = @{thm isomorphic_tuple_intro};
74 val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};
76 val tuple_iso_tuple = (@{const_name Record.tuple_iso_tuple}, @{thm tuple_iso_tuple});
78 fun named_cterm_instantiate values thm = (* FIXME eliminate *)
80 fun match name ((name', _), _) = name = name';
82 (case find_first (match name) (Term.add_vars (prop_of thm) []) of
83 SOME var => cterm_of (theory_of_thm thm) (Var var)
84 | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm]));
86 cterm_instantiate (map (apfst getvar) values) thm
89 structure Iso_Tuple_Thms = Theory_Data
91 type T = thm Symtab.table;
92 val empty = Symtab.make [tuple_iso_tuple];
94 fun merge data = Symtab.merge Thm.eq_thm_prop data; (* FIXME handle Symtab.DUP ?? *)
97 fun get_typedef_info tyco vs
98 (({rep_type, Abs_name, ...}, {Rep_inject, Abs_inverse, ... }) : Typedef.info) thy =
102 |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] [];
103 val proj_constr = Abs_inverse OF [exists_thm];
104 val absT = Type (tyco, map TFree vs);
107 |> pair (tyco, ((Rep_inject, proj_constr), Const (Abs_name, rep_type --> absT), absT))
110 fun do_typedef raw_tyco repT raw_vs thy =
112 val ctxt = Proof_Context.init_global thy |> Variable.declare_typ repT;
113 val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
114 val tac = Tactic.rtac UNIV_witness 1;
117 |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
118 (HOLogic.mk_UNIV repT) NONE tac
119 |-> (fn (tyco, info) => get_typedef_info tyco vs info)
122 fun mk_cons_tuple (left, right) =
124 val (leftT, rightT) = (fastype_of left, fastype_of right);
125 val prodT = HOLogic.mk_prodT (leftT, rightT);
126 val isomT = Type (@{type_name tuple_isomorphism}, [prodT, leftT, rightT]);
128 Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $
129 Const (fst tuple_iso_tuple, isomT) $ left $ right
132 fun dest_cons_tuple (Const (@{const_name Record.iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
133 | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
135 fun add_iso_tuple_type (b, alphas) (leftT, rightT) thy =
137 val repT = HOLogic.mk_prodT (leftT, rightT);
139 val ((_, ((rep_inject, abs_inverse), absC, absT)), typ_thy) =
141 |> do_typedef b repT alphas
142 ||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*)
144 (*construct a type and body for the isomorphism constant by
145 instantiating the theorem to which the definition will be applied*)
147 rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] iso_tuple_intro;
148 val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
149 val isomT = fastype_of body;
150 val isom_binding = Binding.suffix_name isoN b;
151 val isom_name = Sign.full_name typ_thy isom_binding;
152 val isom = Const (isom_name, isomT);
154 val ([isom_def], cdef_thy) =
156 |> Sign.declare_const_global ((isom_binding, isomT), NoSyn) |> snd
157 |> Global_Theory.add_defs false
158 [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
160 val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
161 val cons = Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
165 |> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple))
166 |> Sign.restore_naming thy
168 ((isom, cons $ isom), thm_thy)
171 val iso_tuple_intros_tac =
172 resolve_from_net_tac iso_tuple_intros THEN'
173 CSUBGOAL (fn (cgoal, i) =>
175 val thy = Thm.theory_of_cterm cgoal;
176 val goal = Thm.term_of cgoal;
178 val isthms = Iso_Tuple_Thms.get thy;
179 fun err s t = raise TERM ("iso_tuple_intros_tac: " ^ s, [t]);
181 val goal' = Envir.beta_eta_contract goal;
184 Const (@{const_name Trueprop}, _) $
185 (Const (@{const_name isomorphic_tuple}, _) $ Const is) => is
186 | _ => err "unexpected goal format" goal');
188 (case Symtab.lookup isthms (#1 is) of
190 | NONE => err "no thm found for constant" (Const is));
191 in rtac isthm i end);
196 structure Record: RECORD =
199 val eq_reflection = @{thm eq_reflection};
200 val meta_allE = @{thm Pure.meta_allE};
201 val prop_subst = @{thm prop_subst};
202 val K_record_comp = @{thm K_record_comp};
203 val K_comp_convs = [@{thm o_apply}, K_record_comp];
204 val o_assoc = @{thm o_assoc};
205 val id_apply = @{thm id_apply};
206 val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}];
207 val Not_eq_iff = @{thm Not_eq_iff};
209 val refl_conj_eq = @{thm refl_conj_eq};
211 val surject_assistI = @{thm iso_tuple_surjective_proof_assistI};
212 val surject_assist_idE = @{thm iso_tuple_surjective_proof_assist_idE};
214 val updacc_accessor_eqE = @{thm update_accessor_accessor_eqE};
215 val updacc_updator_eqE = @{thm update_accessor_updator_eqE};
216 val updacc_eq_idI = @{thm iso_tuple_update_accessor_eq_assist_idI};
217 val updacc_eq_triv = @{thm iso_tuple_update_accessor_eq_assist_triv};
219 val updacc_foldE = @{thm update_accessor_congruence_foldE};
220 val updacc_unfoldE = @{thm update_accessor_congruence_unfoldE};
221 val updacc_noopE = @{thm update_accessor_noopE};
222 val updacc_noop_compE = @{thm update_accessor_noop_compE};
223 val updacc_cong_idI = @{thm update_accessor_cong_assist_idI};
224 val updacc_cong_triv = @{thm update_accessor_cong_assist_triv};
225 val updacc_cong_from_eq = @{thm iso_tuple_update_accessor_cong_from_eq};
227 val o_eq_dest = @{thm o_eq_dest};
228 val o_eq_id_dest = @{thm o_eq_id_dest};
229 val o_eq_dest_lhs = @{thm o_eq_dest_lhs};
233 (** name components **)
238 val schemeN = "_scheme";
239 val ext_typeN = "_ext";
240 val inner_typeN = "_inner";
242 val updateN = "_update";
244 val fields_selN = "fields";
245 val extendN = "extend";
246 val truncateN = "truncate";
253 let fun varify (a, S) = TVar ((a, midx + 1), S);
254 in map_type_tfree varify end;
259 val timing = Attrib.setup_config_bool @{binding record_timing} (K false);
260 fun timeit_msg ctxt s x = if Config.get ctxt timing then (warning s; timeit x) else x ();
261 fun timing_msg ctxt s = if Config.get ctxt timing then warning s else ();
266 val Trueprop = HOLogic.mk_Trueprop;
267 fun All xs t = Term.list_all_free (xs, t);
272 val op :== = Misc_Legacy.mk_defpair;
273 val op === = Trueprop o HOLogic.mk_eq;
274 val op ==> = Logic.mk_implies;
279 fun mk_ext (name, T) ts =
280 let val Ts = map fastype_of ts
281 in list_comb (Const (suffix extN name, Ts ---> T), ts) end;
286 fun mk_selC sT (c, T) = (c, sT --> T);
288 fun mk_sel s (c, T) =
289 let val sT = fastype_of s
290 in Const (mk_selC sT (c, T)) $ s end;
295 fun mk_updC sfx sT (c, T) = (suffix sfx c, (T --> T) --> sT --> sT);
297 fun mk_upd' sfx c v sT =
298 let val vT = domain_type (fastype_of v);
299 in Const (mk_updC sfx sT (c, vT)) $ v end;
301 fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s;
306 fun dest_recT (typ as Type (c_ext_type, Ts as (_ :: _))) =
307 (case try (unsuffix ext_typeN) c_ext_type of
308 NONE => raise TYPE ("Record.dest_recT", [typ], [])
309 | SOME c => ((c, Ts), List.last Ts))
310 | dest_recT typ = raise TYPE ("Record.dest_recT", [typ], []);
312 val is_recT = can dest_recT;
315 let val ((c, Ts), U) = dest_recT T
316 in (c, Ts) :: dest_recTs U
317 end handle TYPE _ => [];
320 let val ((c, Ts), U) = dest_recT T in
324 end handle TYPE _ => NONE;
328 val rTs = dest_recTs T;
329 val rTs' = if i < 0 then rTs else take i rTs;
330 in implode (map #1 rTs') end;
334 (*** extend theory by record definition ***)
338 (* type info and parent_info *)
341 {args: (string * sort) list,
342 parent: (typ list * string) option,
343 fields: (string * typ) list,
344 extension: (string * typ list),
352 select_convs: thm list,
353 update_convs: thm list,
354 select_defs: thm list,
355 update_defs: thm list,
356 fold_congs: thm list,
357 unfold_congs: thm list,
371 fun make_info args parent fields extension
372 ext_induct ext_inject ext_surjective ext_split ext_def
373 select_convs update_convs select_defs update_defs fold_congs unfold_congs splits defs
374 surjective equality induct_scheme induct cases_scheme cases
376 {args = args, parent = parent, fields = fields, extension = extension,
377 ext_induct = ext_induct, ext_inject = ext_inject, ext_surjective = ext_surjective,
378 ext_split = ext_split, ext_def = ext_def, select_convs = select_convs,
379 update_convs = update_convs, select_defs = select_defs, update_defs = update_defs,
380 fold_congs = fold_congs, unfold_congs = unfold_congs, splits = splits, defs = defs,
381 surjective = surjective, equality = equality, induct_scheme = induct_scheme,
382 induct = induct, cases_scheme = cases_scheme, cases = cases, simps = simps, iffs = iffs};
386 fields: (string * typ) list,
387 extension: (string * typ list),
391 fun make_parent_info name fields extension ext_def induct_scheme : parent_info =
392 {name = name, fields = fields, extension = extension,
393 ext_def = ext_def, induct_scheme = induct_scheme};
399 {records: info Symtab.table,
401 {selectors: (int * bool) Symtab.table,
402 updates: string Symtab.table,
403 simpset: Simplifier.simpset,
404 defset: Simplifier.simpset,
405 foldcong: Simplifier.simpset,
406 unfoldcong: Simplifier.simpset},
407 equalities: thm Symtab.table,
408 extinjects: thm list,
409 extsplit: thm Symtab.table, (*maps extension name to split rule*)
410 splits: (thm * thm * thm * thm) Symtab.table, (*!!, ALL, EX - split-equalities, induct rule*)
411 extfields: (string * typ) list Symtab.table, (*maps extension to its fields*)
412 fieldext: (string * typ list) Symtab.table}; (*maps field to its extension*)
415 records sel_upd equalities extinjects extsplit splits extfields fieldext =
416 {records = records, sel_upd = sel_upd,
417 equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
418 extfields = extfields, fieldext = fieldext }: data;
420 structure Data = Theory_Data
424 make_data Symtab.empty
425 {selectors = Symtab.empty, updates = Symtab.empty,
426 simpset = HOL_basic_ss, defset = HOL_basic_ss,
427 foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
428 Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
433 {selectors = sels1, updates = upds1,
434 simpset = ss1, defset = ds1,
435 foldcong = fc1, unfoldcong = uc1},
436 equalities = equalities1,
437 extinjects = extinjects1,
438 extsplit = extsplit1,
440 extfields = extfields1,
441 fieldext = fieldext1},
444 {selectors = sels2, updates = upds2,
445 simpset = ss2, defset = ds2,
446 foldcong = fc2, unfoldcong = uc2},
447 equalities = equalities2,
448 extinjects = extinjects2,
449 extsplit = extsplit2,
451 extfields = extfields2,
452 fieldext = fieldext2}) =
454 (Symtab.merge (K true) (recs1, recs2))
455 {selectors = Symtab.merge (K true) (sels1, sels2),
456 updates = Symtab.merge (K true) (upds1, upds2),
457 simpset = Simplifier.merge_ss (ss1, ss2),
458 defset = Simplifier.merge_ss (ds1, ds2),
459 foldcong = Simplifier.merge_ss (fc1, fc2),
460 unfoldcong = Simplifier.merge_ss (uc1, uc2)}
461 (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
462 (Thm.merge_thms (extinjects1, extinjects2))
463 (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
464 (Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
465 Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
466 Thm.eq_thm (c, y) andalso Thm.eq_thm (d, z)) (splits1, splits2))
467 (Symtab.merge (K true) (extfields1, extfields2))
468 (Symtab.merge (K true) (fieldext1, fieldext2));
472 (* access 'records' *)
474 val get_info = Symtab.lookup o #records o Data.get;
476 fun the_info thy name =
477 (case get_info thy name of
479 | NONE => error ("Unknown record type " ^ quote name));
481 fun put_record name info =
482 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
483 make_data (Symtab.update (name, info) records)
484 sel_upd equalities extinjects extsplit splits extfields fieldext);
487 (* access 'sel_upd' *)
489 val get_sel_upd = #sel_upd o Data.get;
491 val is_selector = Symtab.defined o #selectors o get_sel_upd;
492 val get_updates = Symtab.lookup o #updates o get_sel_upd;
493 fun get_ss_with_context getss thy = Simplifier.global_context thy (getss (get_sel_upd thy));
495 val get_simpset = get_ss_with_context #simpset;
496 val get_sel_upd_defs = get_ss_with_context #defset;
498 fun get_update_details u thy =
499 let val sel_upd = get_sel_upd thy in
500 (case Symtab.lookup (#updates sel_upd) u of
502 let val SOME (dep, ismore) = Symtab.lookup (#selectors sel_upd) s
503 in SOME (s, dep, ismore) end
507 fun put_sel_upd names more depth simps defs (folds, unfolds) thy =
509 val all = names @ [more];
510 val sels = map (rpair (depth, false)) names @ [(more, (depth, true))];
511 val upds = map (suffix updateN) all ~~ all;
513 val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong},
514 equalities, extinjects, extsplit, splits, extfields, fieldext} = Data.get thy;
515 val data = make_data records
516 {selectors = fold Symtab.update_new sels selectors,
517 updates = fold Symtab.update_new upds updates,
518 simpset = Simplifier.addsimps (simpset, simps),
519 defset = Simplifier.addsimps (defset, defs),
520 foldcong = foldcong addcongs folds,
521 unfoldcong = unfoldcong addcongs unfolds}
522 equalities extinjects extsplit splits extfields fieldext;
523 in Data.put data thy end;
526 (* access 'equalities' *)
528 fun add_equalities name thm =
529 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
530 make_data records sel_upd
531 (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext);
533 val get_equalities = Symtab.lookup o #equalities o Data.get;
536 (* access 'extinjects' *)
538 fun add_extinjects thm =
539 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
540 make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
541 extsplit splits extfields fieldext);
543 val get_extinjects = rev o #extinjects o Data.get;
546 (* access 'extsplit' *)
548 fun add_extsplit name thm =
549 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
550 make_data records sel_upd equalities extinjects
551 (Symtab.update_new (name, thm) extsplit) splits extfields fieldext);
554 (* access 'splits' *)
556 fun add_splits name thmP =
557 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
558 make_data records sel_upd equalities extinjects extsplit
559 (Symtab.update_new (name, thmP) splits) extfields fieldext);
561 val get_splits = Symtab.lookup o #splits o Data.get;
564 (* parent/extension of named record *)
566 val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o Data.get);
567 val get_extension = Option.map #extension oo (Symtab.lookup o #records o Data.get);
570 (* access 'extfields' *)
572 fun add_extfields name fields =
573 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
574 make_data records sel_upd equalities extinjects extsplit splits
575 (Symtab.update_new (name, fields) extfields) fieldext);
577 val get_extfields = Symtab.lookup o #extfields o Data.get;
579 fun get_extT_fields thy T =
581 val ((name, Ts), moreT) = dest_recT T;
583 let val (nm :: _ :: rst) = rev (Long_Name.explode name) (* FIXME !? *)
584 in Long_Name.implode (rev (nm :: rst)) end;
585 val midx = maxidx_of_typs (moreT :: Ts);
586 val varifyT = varifyT midx;
587 val {records, extfields, ...} = Data.get thy;
588 val (fields, (more, _)) = split_last (Symtab.lookup_list extfields name);
589 val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
591 val subst = fold (Sign.typ_match thy) (#1 (split_last args) ~~ #1 (split_last Ts)) Vartab.empty;
592 val fields' = map (apsnd (Envir.norm_type subst o varifyT)) fields;
593 in (fields', (more, moreT)) end;
595 fun get_recT_fields thy T =
597 val (root_fields, (root_more, root_moreT)) = get_extT_fields thy T;
598 val (rest_fields, rest_more) =
599 if is_recT root_moreT then get_recT_fields thy root_moreT
600 else ([], (root_more, root_moreT));
601 in (root_fields @ rest_fields, rest_more) end;
604 (* access 'fieldext' *)
606 fun add_fieldext extname_types fields =
607 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
610 fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
611 in make_data records sel_upd equalities extinjects extsplit splits extfields fieldext' end);
613 val get_fieldext = Symtab.lookup o #fieldext o Data.get;
620 fun add_parents _ NONE = I
621 | add_parents thy (SOME (types, name)) =
623 fun err msg = error (msg ^ " parent record " ^ quote name);
625 val {args, parent, ...} =
626 (case get_info thy name of SOME info => info | NONE => err "Unknown");
627 val _ = if length types <> length args then err "Bad number of arguments for" else ();
629 fun bad_inst ((x, S), T) =
630 if Sign.of_sort thy (T, S) then NONE else SOME x
631 val bads = map_filter bad_inst (args ~~ types);
632 val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");
634 val inst = args ~~ types;
635 val subst = Term.map_type_tfree (the o AList.lookup (op =) inst);
636 val parent' = Option.map (apfst (map subst)) parent;
637 in cons (name, inst) #> add_parents thy parent' end;
641 fun get_hierarchy thy (name, types) = add_parents thy (SOME (types, name)) [];
643 fun get_parent_info thy parent =
644 add_parents thy parent [] |> map (fn (name, inst) =>
646 val subst = Term.map_type_tfree (the o AList.lookup (op =) inst);
647 val {fields, extension, induct_scheme, ext_def, ...} = the_info thy name;
648 val fields' = map (apsnd subst) fields;
649 val extension' = apsnd (map subst) extension;
650 in make_parent_info name fields' extension' ext_def induct_scheme end);
656 (** concrete syntax for records **)
660 fun decode_type thy t =
662 fun get_sort env xi =
663 the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname));
665 Syntax_Phases.typ_of_term (get_sort (Syntax_Phases.term_sorts t)) t
669 (* parse translations *)
673 fun split_args (field :: fields) ((name, arg) :: fargs) =
674 if can (unsuffix name) field then
675 let val (args, rest) = split_args fields fargs
676 in (arg :: args, rest) end
677 else raise Fail ("expecting field " ^ quote field ^ " but got " ^ quote name)
678 | split_args [] (fargs as (_ :: _)) = ([], fargs)
679 | split_args (_ :: _) [] = raise Fail "expecting more fields"
680 | split_args _ _ = ([], []);
682 fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) =
684 | field_type_tr t = raise TERM ("field_type_tr", [t]);
686 fun field_types_tr (Const (@{syntax_const "_field_types"}, _) $ t $ u) =
687 field_type_tr t :: field_types_tr u
688 | field_types_tr t = [field_type_tr t];
690 fun record_field_types_tr more ctxt t =
692 val thy = Proof_Context.theory_of ctxt;
693 fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]);
695 fun mk_ext (fargs as (name, _) :: _) =
696 (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
697 SOME (ext, alphas) =>
698 (case get_extfields thy ext of
701 val (fields', _) = split_last fields;
702 val types = map snd fields';
703 val (args, rest) = split_args (map fst fields') fargs
704 handle Fail msg => err msg;
705 val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
706 val midx = fold Term.maxidx_typ argtypes 0;
707 val varifyT = varifyT midx;
708 val vartypes = map varifyT types;
710 val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
711 handle Type.TYPE_MATCH => err "type is no proper record (extension)";
713 map (Syntax_Phases.term_of_typ ctxt o Envir.norm_type subst o varifyT)
714 (#1 (split_last alphas));
716 val more' = mk_ext rest;
719 (Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
721 | NONE => err ("no fields defined for " ^ quote ext))
722 | NONE => err (quote name ^ " is no proper field"))
725 mk_ext (field_types_tr t)
728 fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const @{type_syntax unit}) ctxt t
729 | record_type_tr _ ts = raise TERM ("record_type_tr", ts);
731 fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t
732 | record_type_scheme_tr _ ts = raise TERM ("record_type_scheme_tr", ts);
735 fun field_tr ((Const (@{syntax_const "_field"}, _) $ Const (name, _) $ arg)) = (name, arg)
736 | field_tr t = raise TERM ("field_tr", [t]);
738 fun fields_tr (Const (@{syntax_const "_fields"}, _) $ t $ u) = field_tr t :: fields_tr u
739 | fields_tr t = [field_tr t];
741 fun record_fields_tr more ctxt t =
743 val thy = Proof_Context.theory_of ctxt;
744 fun err msg = raise TERM ("Error in record input: " ^ msg, [t]);
746 fun mk_ext (fargs as (name, _) :: _) =
747 (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
749 (case get_extfields thy ext of
752 val (args, rest) = split_args (map fst (fst (split_last fields))) fargs
753 handle Fail msg => err msg;
754 val more' = mk_ext rest;
755 in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end
756 | NONE => err ("no fields defined for " ^ quote ext))
757 | NONE => err (quote name ^ " is no proper field"))
759 in mk_ext (fields_tr t) end;
761 fun record_tr ctxt [t] = record_fields_tr (Syntax.const @{const_syntax Unity}) ctxt t
762 | record_tr _ ts = raise TERM ("record_tr", ts);
764 fun record_scheme_tr ctxt [t, more] = record_fields_tr more ctxt t
765 | record_scheme_tr _ ts = raise TERM ("record_scheme_tr", ts);
768 fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) =
769 Syntax.const (suffix updateN name) $ Abs (Name.uu_, dummyT, arg)
770 | field_update_tr t = raise TERM ("field_update_tr", [t]);
772 fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) =
773 field_update_tr t :: field_updates_tr u
774 | field_updates_tr t = [field_update_tr t];
776 fun record_update_tr [t, u] = fold (curry op $) (field_updates_tr u) t
777 | record_update_tr ts = raise TERM ("record_update_tr", ts);
781 val parse_translation =
782 [(@{syntax_const "_record_update"}, record_update_tr)];
784 val advanced_parse_translation =
785 [(@{syntax_const "_record"}, record_tr),
786 (@{syntax_const "_record_scheme"}, record_scheme_tr),
787 (@{syntax_const "_record_type"}, record_type_tr),
788 (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)];
793 (* print translations *)
795 val type_abbr = Attrib.setup_config_bool @{binding record_type_abbr} (K true);
796 val type_as_fields = Attrib.setup_config_bool @{binding record_type_as_fields} (K true);
801 (* FIXME early extern (!??) *)
802 (* FIXME Syntax.free (??) *)
803 fun field_type_tr' (c, t) = Syntax.const @{syntax_const "_field_type"} $ Syntax.const c $ t;
805 fun field_types_tr' (t, u) = Syntax.const @{syntax_const "_field_types"} $ t $ u;
807 fun record_type_tr' ctxt t =
809 val thy = Proof_Context.theory_of ctxt;
811 val T = decode_type thy t;
812 val varifyT = varifyT (Term.maxidx_of_typ T);
816 Type (ext, args as _ :: _) =>
817 (case try (unsuffix ext_typeN) ext of
819 (case get_extfields thy ext' of
820 SOME (fields as (x, _) :: _) =>
821 (case get_fieldext thy x of
824 val (f :: fs, _) = split_last fields;
826 apfst (Proof_Context.extern_const ctxt) f ::
827 map (apfst Long_Name.base_name) fs;
828 val (args', more) = split_last args;
829 val alphavars = map varifyT (#1 (split_last alphas));
830 val subst = Type.raw_matches (alphavars, args') Vartab.empty;
831 val fields'' = (map o apsnd) (Envir.norm_type subst o varifyT) fields';
832 in fields'' @ strip_fields more end
833 handle Type.TYPE_MATCH => [("", T)])
839 val (fields, (_, moreT)) = split_last (strip_fields T);
840 val _ = null fields andalso raise Match;
842 foldr1 field_types_tr'
843 (map (field_type_tr' o apsnd (Syntax_Phases.term_of_typ ctxt)) fields);
845 if not (Config.get ctxt type_as_fields) orelse null fields then raise Match
846 else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
848 Syntax.const @{syntax_const "_record_type_scheme"} $ u $
849 Syntax_Phases.term_of_typ ctxt moreT
852 (*try to reconstruct the record name type abbreviation from
853 the (nested) extension types*)
854 fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm =
856 val thy = Proof_Context.theory_of ctxt;
857 val T = decode_type thy tm;
858 val midx = maxidx_of_typ T;
859 val varifyT = varifyT midx;
861 fun mk_type_abbr subst name args =
862 let val abbrT = Type (name, map (varifyT o TFree) args)
863 in Syntax_Phases.term_of_typ ctxt (Envir.norm_type subst abbrT) end;
865 fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
867 if Config.get ctxt type_abbr then
870 if name = last_ext then
871 let val subst = match schemeT T in
872 if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree zeta)))
873 then mk_type_abbr subst abbr alphas
874 else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
875 end handle Type.TYPE_MATCH => record_type_tr' ctxt tm
876 else raise Match (*give print translation of specialised record a chance*)
878 else record_type_tr' ctxt tm
883 fun record_ext_type_tr' name =
885 val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);
887 record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts));
888 in (ext_type_name, tr') end;
890 fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
892 val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);
894 record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt
895 (list_comb (Syntax.const ext_type_name, ts));
896 in (ext_type_name, tr') end;
903 (* FIXME Syntax.free (??) *)
904 fun field_tr' (c, t) = Syntax.const @{syntax_const "_field"} $ Syntax.const c $ t;
905 fun fields_tr' (t, u) = Syntax.const @{syntax_const "_fields"} $ t $ u;
907 fun record_tr' ctxt t =
909 val thy = Proof_Context.theory_of ctxt;
912 (case strip_comb t of
913 (Const (ext, _), args as (_ :: _)) =>
914 (case try (Lexicon.unmark_const o unsuffix extN) ext of
916 (case get_extfields thy ext' of
919 val (f :: fs, _) = split_last (map fst fields);
920 val fields' = Proof_Context.extern_const ctxt f :: map Long_Name.base_name fs;
921 val (args', more) = split_last args;
922 in (fields' ~~ args') @ strip_fields more end
923 handle ListPair.UnequalLengths => [("", t)])
928 val (fields, (_, more)) = split_last (strip_fields t);
929 val _ = null fields andalso raise Match;
930 val u = foldr1 fields_tr' (map field_tr' fields);
933 Const (@{const_syntax Unity}, _) => Syntax.const @{syntax_const "_record"} $ u
934 | _ => Syntax.const @{syntax_const "_record_scheme"} $ u $ more
939 fun record_ext_tr' name =
941 val ext_name = Lexicon.mark_const (name ^ extN);
942 fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));
943 in (ext_name, tr') end;
950 fun dest_update ctxt c =
951 (case try Lexicon.unmark_const c of
952 SOME d => try (unsuffix updateN) (Proof_Context.extern_const ctxt d)
955 fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
956 (case dest_update ctxt c of
958 (case try Syntax_Trans.const_abs_tr' k of
960 apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
961 (field_updates_tr' ctxt u)
964 | field_updates_tr' _ tm = ([], tm);
966 fun record_update_tr' ctxt tm =
967 (case field_updates_tr' ctxt tm of
968 ([], _) => raise Match
970 Syntax.const @{syntax_const "_record_update"} $ u $
971 foldr1 (fn (v, w) => Syntax.const @{syntax_const "_field_updates"} $ v $ w) (rev ts));
975 fun field_update_tr' name =
977 val update_name = Lexicon.mark_const (name ^ updateN);
978 fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u)
979 | tr' _ _ = raise Match;
980 in (update_name, tr') end;
986 (** record simprocs **)
988 fun future_forward_prf_standard thy prf prop () =
990 if ! quick_and_dirty then Skip_Proof.make_thm thy prop
991 else if Goal.future_enabled () then
992 Goal.future_result (Proof_Context.init_global thy) (Goal.fork prf) prop
994 in Drule.export_without_context thm end;
996 fun prove_common immediate stndrd thy asms prop tac =
999 if ! quick_and_dirty then Skip_Proof.prove
1000 else if immediate orelse not (Goal.future_enabled ()) then Goal.prove
1001 else Goal.prove_future;
1002 val prf = prv (Proof_Context.init_global thy) [] asms prop tac;
1003 in if stndrd then Drule.export_without_context prf else prf end;
1005 val prove_future_global = prove_common false;
1006 val prove_global = prove_common true;
1008 fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) =
1009 (case get_updates thy u of
1010 SOME u_name => u_name = s
1011 | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));
1014 let val T = range_type (fastype_of f)
1015 in HOLogic.mk_comp (Const (@{const_name Fun.id}, T --> T), f) end;
1017 fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
1018 | get_upd_funs _ = [];
1020 fun get_accupd_simps thy term defset =
1022 val (acc, [body]) = strip_comb term;
1023 val upd_funs = sort_distinct Term_Ord.fast_term_ord (get_upd_funs body);
1026 (* FIXME fresh "f" (!?) *)
1027 val T = domain_type (fastype_of upd);
1028 val lhs = HOLogic.mk_comp (acc, upd $ Free ("f", T));
1030 if is_sel_upd_pair thy acc upd
1031 then HOLogic.mk_comp (Free ("f", T), acc)
1032 else mk_comp_id acc;
1033 val prop = lhs === rhs;
1035 Goal.prove (Proof_Context.init_global thy) [] [] prop
1037 simp_tac defset 1 THEN
1038 REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
1039 TRY (simp_tac (HOL_ss addsimps id_o_apps) 1));
1041 if is_sel_upd_pair thy acc upd
1044 in Drule.export_without_context (othm RS dest) end;
1045 in map get_simp upd_funs end;
1047 fun get_updupd_simp thy defset u u' comp =
1049 (* FIXME fresh "f" (!?) *)
1050 val f = Free ("f", domain_type (fastype_of u));
1051 val f' = Free ("f'", domain_type (fastype_of u'));
1052 val lhs = HOLogic.mk_comp (u $ f, u' $ f');
1055 then u $ HOLogic.mk_comp (f, f')
1056 else HOLogic.mk_comp (u' $ f', u $ f);
1057 val prop = lhs === rhs;
1059 Goal.prove (Proof_Context.init_global thy) [] [] prop
1061 simp_tac defset 1 THEN
1062 REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
1063 TRY (simp_tac (HOL_ss addsimps [id_apply]) 1));
1064 val dest = if comp then o_eq_dest_lhs else o_eq_dest;
1065 in Drule.export_without_context (othm RS dest) end;
1067 fun get_updupd_simps thy term defset =
1069 val upd_funs = get_upd_funs term;
1070 val cname = fst o dest_Const;
1071 fun getswap u u' = get_updupd_simp thy defset u u' (cname u = cname u');
1072 fun build_swaps_to_eq _ [] swaps = swaps
1073 | build_swaps_to_eq upd (u :: us) swaps =
1075 val key = (cname u, cname upd);
1077 if Symreltab.defined swaps key then swaps
1078 else Symreltab.insert (K true) (key, getswap u upd) swaps;
1080 if cname u = cname upd then newswaps
1081 else build_swaps_to_eq upd us newswaps
1083 fun swaps_needed [] _ _ swaps = map snd (Symreltab.dest swaps)
1084 | swaps_needed (u :: us) prev seen swaps =
1085 if Symtab.defined seen (cname u)
1086 then swaps_needed us prev seen (build_swaps_to_eq u prev swaps)
1087 else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps;
1088 in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end;
1090 val named_cterm_instantiate = Iso_Tuple_Support.named_cterm_instantiate;
1092 fun prove_unfold_defs thy ex_simps ex_simprs prop =
1094 val defset = get_sel_upd_defs thy;
1095 val prop' = Envir.beta_eta_contract prop;
1096 val (lhs, _) = Logic.dest_equals (Logic.strip_assums_concl prop');
1097 val (_, args) = strip_comb lhs;
1098 val simps = (if length args = 1 then get_accupd_simps else get_updupd_simps) thy lhs defset;
1100 Goal.prove (Proof_Context.init_global thy) [] [] prop'
1102 simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1 THEN
1103 TRY (simp_tac (HOL_basic_ss addsimps ex_simps addsimprocs ex_simprs) 1))
1109 fun eq (s1: string) (s2: string) = (s1 = s2);
1111 fun has_field extfields f T =
1112 exists (fn (eN, _) => exists (eq f o fst) (Symtab.lookup_list extfields eN)) (dest_recTs T);
1114 fun K_skeleton n (T as Type (_, [_, kT])) (b as Bound i) (Abs (x, xT, t)) =
1115 if null (loose_bnos t) then ((n, kT), (Abs (x, xT, Bound (i + 1)))) else ((n, T), b)
1116 | K_skeleton n T b _ = ((n, T), b);
1123 Simplify selections of an record update:
1124 (1) S (S_update k r) = k (S r)
1125 (2) S (X_update k r) = S r
1127 The simproc skips multiple updates at once, eg:
1128 S (X_update x (Y_update y (S_update k r))) = k (S r)
1130 But be careful in (2) because of the extensibility of records.
1131 - If S is a more-selector we have to make sure that the update on component
1132 X does not affect the selected subrecord.
1133 - If X is a more-selector we have to make sure that S is not in the updated
1137 Simplifier.simproc_global @{theory HOL} "record_simp" ["x"]
1138 (fn thy => fn _ => fn t =>
1140 (sel as Const (s, Type (_, [_, rangeS]))) $
1141 ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
1142 if is_selector thy s andalso is_some (get_updates thy u) then
1144 val {sel_upd = {updates, ...}, extfields, ...} = Data.get thy;
1146 fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
1147 (case Symtab.lookup updates u of
1151 (case mk_eq_terms r of
1156 val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
1157 in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end
1158 | SOME (trm, trm', vars) =>
1160 val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k;
1161 in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end)
1162 else if has_field extfields u_name rangeS orelse
1163 has_field extfields s (domain_type kT) then NONE
1165 (case mk_eq_terms r of
1166 SOME (trm, trm', vars) =>
1167 let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k
1168 in SOME (upd $ kb $ trm, trm', kv :: vars) end
1173 val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
1174 in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end))
1175 | mk_eq_terms _ = NONE;
1177 (case mk_eq_terms (upd $ k $ r) of
1178 SOME (trm, trm', vars) =>
1180 (prove_unfold_defs thy [] []
1181 (list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
1187 fun get_upd_acc_cong_thm upd acc thy simpset =
1189 val insts = [("upd", cterm_of thy upd), ("ac", cterm_of thy acc)];
1190 val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv);
1192 Goal.prove (Proof_Context.init_global thy) [] [] prop
1194 simp_tac simpset 1 THEN
1195 REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
1196 TRY (resolve_tac [updacc_cong_idI] 1))
1202 (*Simplify multiple updates:
1203 (1) "N_update y (M_update g (N_update x (M_update f r))) =
1204 (N_update (y o x) (M_update (g o f) r))"
1205 (2) "r(|M:= M r|) = r"
1207 In both cases "more" updates complicate matters: for this reason
1208 we omit considering further updates if doing so would introduce
1209 both a more update and an update to a field within it.*)
1211 Simplifier.simproc_global @{theory HOL} "record_upd_simp" ["x"]
1212 (fn thy => fn _ => fn t =>
1214 (*We can use more-updators with other updators as long
1215 as none of the other updators go deeper than any more
1216 updator. min here is the depth of the deepest other
1217 updator, max the depth of the shallowest more updator.*)
1218 fun include_depth (dep, true) (min, max) =
1220 then SOME (min, if dep <= max orelse max = ~1 then dep else max)
1222 | include_depth (dep, false) (min, max) =
1223 if dep <= max orelse max = ~1
1224 then SOME (if min <= dep then dep else min, max)
1227 fun getupdseq (term as (upd as Const (u, _)) $ f $ tm) min max =
1228 (case get_update_details u thy of
1229 SOME (s, dep, ismore) =>
1230 (case include_depth (dep, ismore) (min, max) of
1231 SOME (min', max') =>
1232 let val (us, bs, _) = getupdseq tm min' max'
1233 in ((upd, s, f) :: us, bs, fastype_of term) end
1234 | NONE => ([], term, HOLogic.unitT))
1235 | NONE => ([], term, HOLogic.unitT))
1236 | getupdseq term _ _ = ([], term, HOLogic.unitT);
1238 val (upds, base, baseT) = getupdseq t 0 ~1;
1240 fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm =
1241 if s = s' andalso null (loose_bnos tm')
1242 andalso subst_bound (HOLogic.unit, tm') = tm
1243 then (true, Abs (n, T, Const (s', T') $ Bound 1))
1244 else (false, HOLogic.unit)
1245 | is_upd_noop _ _ _ = (false, HOLogic.unit);
1247 fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) =
1249 val ss = get_sel_upd_defs thy;
1250 val uathm = get_upd_acc_cong_thm upd acc thy ss;
1252 [Drule.export_without_context (uathm RS updacc_noopE),
1253 Drule.export_without_context (uathm RS updacc_noop_compE)]
1256 (*If f is constant then (f o g) = f. We know that K_skeleton
1257 only returns constant abstractions thus when we see an
1258 abstraction we can discard inner updates.*)
1259 fun add_upd (f as Abs _) fs = [f]
1260 | add_upd f fs = (f :: fs);
1262 (*mk_updterm returns
1263 (orig-term-skeleton, simplified-skeleton,
1264 variables, duplicate-updates, simp-flag, noop-simps)
1266 where duplicate-updates is a table used to pass upward
1267 the list of update functions which can be composed
1268 into an update above them, simp-flag indicates whether
1269 any simplification was achieved, and noop-simps are
1270 used for eliminating case (2) defined above*)
1271 fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term =
1273 val (lhs, rhs, vars, dups, simp, noops) =
1274 mk_updterm upds (Symtab.update (u, ()) above) term;
1276 K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f;
1277 val (isnoop, skelf') = is_upd_noop s f term;
1278 val funT = domain_type T;
1279 fun mk_comp_local (f, f') =
1280 Const (@{const_name Fun.comp}, funT --> funT --> funT) $ f $ f';
1283 (upd $ skelf' $ lhs, rhs, vars,
1284 Symtab.update (u, []) dups, true,
1285 if Symtab.defined noops u then noops
1286 else Symtab.update (u, get_noop_simps upd skelf') noops)
1287 else if Symtab.defined above u then
1288 (upd $ skelf $ lhs, rhs, fvar :: vars,
1289 Symtab.map_default (u, []) (add_upd skelf) dups,
1292 (case Symtab.lookup dups u of
1295 upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs,
1296 fvar :: vars, dups, true, noops)
1297 | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops))
1299 | mk_updterm [] _ _ =
1300 (Bound 0, Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty)
1301 | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _) => x) us);
1303 val (lhs, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
1304 val noops' = maps snd (Symtab.dest noops);
1308 (prove_unfold_defs thy noops' [simproc]
1309 (list_all (vars, Logic.mk_equals (lhs, rhs))))
1318 (*Look up the most specific record-equality.
1321 Testing equality of records boils down to the test of equality of all components.
1322 Therefore the complexity is: #components * complexity for single component.
1323 Especially if a record has a lot of components it may be better to split up
1324 the record first and do simplification on that (split_simp_tac).
1325 e.g. r(|lots of updates|) = x
1327 eq_simproc split_simp_tac
1328 Complexity: #components * #updates #updates
1331 Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
1332 (fn thy => fn _ => fn t =>
1333 (case t of Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ =>
1334 (case rec_id ~1 T of
1337 (case get_equalities thy name of
1339 | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
1345 (*Split quantified occurrences of records, for which P holds. P can peek on the
1346 subterm starting at the quantified occurrence of the record (including the quantifier):
1347 P t = 0: do not split
1348 P t = ~1: completely split
1349 P t > 0: split up to given bound of record extensions.*)
1350 fun split_simproc P =
1351 Simplifier.simproc_global @{theory HOL} "record_split_simp" ["x"]
1352 (fn thy => fn _ => fn t =>
1354 Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
1355 if quantifier = @{const_name all} orelse
1356 quantifier = @{const_name All} orelse
1357 quantifier = @{const_name Ex}
1359 (case rec_id ~1 T of
1362 let val split = P t in
1364 (case get_splits thy (rec_id split T) of
1366 | SOME (all_thm, All_thm, Ex_thm, _) =>
1369 @{const_name all} => all_thm
1370 | @{const_name All} => All_thm RS eq_reflection
1371 | @{const_name Ex} => Ex_thm RS eq_reflection
1372 | _ => raise Fail "split_simproc"))
1378 val ex_sel_eq_simproc =
1379 Simplifier.simproc_global @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
1380 (fn thy => fn ss => fn t =>
1383 prove_global true thy [] prop
1384 (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
1385 addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1);
1387 fun mkeq (lr, Teq, (sel, Tsel), x) i =
1388 if is_selector thy sel then
1391 if not (loose_bvar1 (x, 0))
1392 then Free ("x" ^ string_of_int i, range_type Tsel)
1393 else raise TERM ("", [x]);
1394 val sel' = Const (sel, Tsel) $ Bound 0;
1395 val (l, r) = if lr then (sel', x') else (x', sel');
1396 in Const (@{const_name HOL.eq}, Teq) $ l $ r end
1397 else raise TERM ("", [Const (sel, Tsel)]);
1399 fun dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
1400 (true, Teq, (sel, Tsel), X)
1401 | dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
1402 (false, Teq, (sel, Tsel), X)
1403 | dest_sel_eq _ = raise TERM ("", []);
1406 Const (@{const_name Ex}, Tex) $ Abs (s, T, t) =>
1408 val eq = mkeq (dest_sel_eq t) 0;
1410 list_all ([("r", T)],
1412 (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), HOLogic.true_const));
1413 in SOME (prove prop) end
1414 handle TERM _ => NONE)
1419 (* split_simp_tac *)
1421 (*Split (and simplify) all records in the goal for which P holds.
1422 For quantified occurrences of a record
1423 P can peek on the whole subterm (including the quantifier); for free variables P
1424 can only peek on the variable itself.
1425 P t = 0: do not split
1426 P t = ~1: completely split
1427 P t > 0: split up to given bound of record extensions.*)
1428 fun split_simp_tac thms P = CSUBGOAL (fn (cgoal, i) =>
1430 val thy = Thm.theory_of_cterm cgoal;
1432 val goal = term_of cgoal;
1433 val frees = filter (is_recT o #2) (Term.add_frees goal []);
1435 val has_rec = exists_Const
1436 (fn (s, Type (_, [Type (_, [T, _]), _])) =>
1437 (s = @{const_name all} orelse s = @{const_name All} orelse s = @{const_name Ex}) andalso
1441 fun mk_split_free_tac free induct_thm i =
1443 val cfree = cterm_of thy free;
1444 val _$ (_ $ r) = concl_of induct_thm;
1445 val crec = cterm_of thy r;
1446 val thm = cterm_instantiate [(crec, cfree)] induct_thm;
1448 simp_tac (HOL_basic_ss addsimps @{thms induct_atomize}) i THEN
1450 simp_tac (HOL_basic_ss addsimps @{thms induct_rulify}) i
1453 val split_frees_tacs =
1454 frees |> map_filter (fn (x, T) =>
1455 (case rec_id ~1 T of
1459 val free = Free (x, T);
1463 (case get_splits thy (rec_id split T) of
1465 | SOME (_, _, _, induct_thm) =>
1466 SOME (mk_split_free_tac free induct_thm i))
1470 val simprocs = if has_rec goal then [split_simproc P] else [];
1471 val thms' = K_comp_convs @ thms;
1473 EVERY split_frees_tacs THEN
1474 Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i
1480 (*Split all records in the goal, which are quantified by !! or ALL.*)
1481 val split_tac = CSUBGOAL (fn (cgoal, i) =>
1483 val goal = term_of cgoal;
1485 val has_rec = exists_Const
1486 (fn (s, Type (_, [Type (_, [T, _]), _])) =>
1487 (s = @{const_name all} orelse s = @{const_name All}) andalso is_recT T
1490 fun is_all (Const (@{const_name all}, _) $ _) = ~1
1491 | is_all (Const (@{const_name All}, _) $ _) = ~1
1494 if has_rec goal then
1495 Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [split_simproc is_all]) i
1502 val split_name = "record_split_tac";
1503 val split_wrapper = (split_name, fn _ => fn tac => split_tac ORELSE' tac);
1507 (** theory extender interface **)
1509 (* prepare arguments *)
1511 fun read_typ ctxt raw_T env =
1513 val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
1514 val T = Syntax.read_typ ctxt' raw_T;
1515 val env' = OldTerm.add_typ_tfrees (T, env);
1518 fun cert_typ ctxt raw_T env =
1520 val thy = Proof_Context.theory_of ctxt;
1521 val T = Type.no_tvars (Sign.certify_typ thy raw_T)
1522 handle TYPE (msg, _, _) => error msg;
1523 val env' = OldTerm.add_typ_tfrees (T, env);
1529 fun case_names_fields x = Rule_Cases.case_names ["fields"] x;
1530 fun induct_type_global name = [case_names_fields, Induct.induct_type name];
1531 fun cases_type_global name = [case_names_fields, Induct.cases_type name];
1536 fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));
1538 (*Do case analysis / induction according to rule on last parameter of ith subgoal
1539 (or on s if there are no parameters).
1540 Instatiation of record variable (and predicate) in rule is calculated to
1541 avoid problems with higher order unification.*)
1542 fun try_param_tac s rule = CSUBGOAL (fn (cgoal, i) =>
1544 val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
1546 val g = Thm.term_of cgoal;
1547 val params = Logic.strip_params g;
1548 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
1549 val rule' = Thm.lift_rule cgoal rule;
1550 val (P, ys) = strip_comb (HOLogic.dest_Trueprop
1551 (Logic.strip_assums_concl (prop_of rule')));
1552 (*ca indicates if rule is a case analysis or induction rule*)
1554 (case rev (drop (length params) ys) of
1555 [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
1556 (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
1557 | [x] => (head_of x, false));
1560 (map (pairself cert)
1563 (case AList.lookup (op =) (Term.add_frees g []) s of
1564 NONE => error "try_param_tac: no such variable"
1565 | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
1567 [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
1568 (x, list_abs (params, Bound 0))])) rule';
1569 in compose_tac (false, rule'', nprems_of rule) i end);
1572 fun extension_definition name fields alphas zeta moreT more vars thy =
1574 val ctxt = Proof_Context.init_global thy;
1576 val base_name = Long_Name.base_name name;
1578 val fieldTs = map snd fields;
1579 val fields_moreTs = fieldTs @ [moreT];
1581 val alphas_zeta = alphas @ [zeta];
1583 val ext_binding = Binding.name (suffix extN base_name);
1584 val ext_name = suffix extN name;
1585 val ext_tyco = suffix ext_typeN name
1586 val extT = Type (ext_tyco, map TFree alphas_zeta);
1587 val ext_type = fields_moreTs ---> extT;
1590 (* the tree of new types that will back the record extension *)
1592 val mktreeV = Balanced_Tree.make Iso_Tuple_Support.mk_cons_tuple;
1594 fun mk_iso_tuple (left, right) (thy, i) =
1596 val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
1597 val ((_, cons), thy') = thy
1598 |> Iso_Tuple_Support.add_iso_tuple_type
1599 (Binding.suffix_name suff (Binding.name base_name), alphas_zeta)
1600 (fastype_of left, fastype_of right);
1602 (cons $ left $ right, (thy', i + 1))
1605 (*trying to create a 1-element iso_tuple will fail, and is pointless anyway*)
1606 fun mk_even_iso_tuple [arg] = pair arg
1607 | mk_even_iso_tuple args = mk_iso_tuple (Iso_Tuple_Support.dest_cons_tuple (mktreeV args));
1609 fun build_meta_tree_type i thy vars more =
1610 let val len = length vars in
1611 if len < 1 then raise TYPE ("meta_tree_type args too short", [], vars)
1612 else if len > 16 then
1615 | group16 xs = take 16 xs :: group16 (drop 16 xs);
1616 val vars' = group16 vars;
1617 val (composites, (thy', i')) = fold_map mk_even_iso_tuple vars' (thy, i);
1619 build_meta_tree_type i' thy' composites more
1622 let val (term, (thy', _)) = mk_iso_tuple (mktreeV vars, more) (thy, 0)
1626 val _ = timing_msg ctxt "record extension preparing definitions";
1629 (* 1st stage part 1: introduce the tree of new types *)
1631 fun get_meta_tree () = build_meta_tree_type 1 thy vars more;
1632 val (ext_body, typ_thy) =
1633 timeit_msg ctxt "record extension nested type def:" get_meta_tree;
1636 (* prepare declarations and definitions *)
1638 (* 1st stage part 2: define the ext constant *)
1640 fun mk_ext args = list_comb (Const (ext_name, ext_type), args);
1641 val ext_spec = Logic.mk_equals (mk_ext (vars @ [more]), ext_body);
1645 |> Sign.declare_const_global ((ext_binding, ext_type), NoSyn) |> snd
1646 |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]
1647 ||> Theory.checkpoint
1648 val ([ext_def], defs_thy) =
1649 timeit_msg ctxt "record extension constructor def:" mk_defs;
1652 (* prepare propositions *)
1654 val _ = timing_msg ctxt "record extension preparing propositions";
1655 val vars_more = vars @ [more];
1656 val variants = map (fn Free (x, _) => x) vars_more;
1657 val ext = mk_ext vars_more;
1658 val s = Free (rN, extT);
1659 val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT);
1661 val inject_prop = (* FIXME local x x' *)
1662 let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
1663 HOLogic.mk_conj (HOLogic.eq_const extT $
1664 mk_ext vars_more $ mk_ext vars_more', HOLogic.true_const)
1666 foldr1 HOLogic.mk_conj
1667 (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [HOLogic.true_const])
1671 (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
1673 val split_meta_prop = (* FIXME local P *)
1674 let val P = Free (singleton (Name.variant_list variants) "P", extT --> Term.propT) in
1676 (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
1679 val prove_standard = prove_future_global true defs_thy;
1683 (prove_standard [] inject_prop
1685 simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
1687 (rtac refl_conj_eq 1 ORELSE
1688 Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
1691 val inject = timeit_msg ctxt "record extension inject proof:" inject_prf;
1693 (*We need a surjection property r = (| f = f r, g = g r ... |)
1694 to prove other theorems. We haven't given names to the accessors
1695 f, g etc yet however, so we generate an ext structure with
1696 free variables as all arguments and allow the introduction tactic to
1697 operate on it as far as it can. We then use Drule.export_without_context
1698 to convert the free variables into unifiable variables and unify them with
1699 (roughly) the definition of the accessor.*)
1700 fun surject_prf () =
1702 val cterm_ext = cterm_of defs_thy ext;
1703 val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
1705 simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
1706 REPEAT_ALL_NEW Iso_Tuple_Support.iso_tuple_intros_tac 1;
1707 val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
1708 val [halfway] = Seq.list_of (tactic1 start);
1709 val [surject] = Seq.list_of (tactic2 (Drule.export_without_context halfway));
1713 val surject = timeit_msg ctxt "record extension surjective proof:" surject_prf;
1715 fun split_meta_prf () =
1716 prove_standard [] split_meta_prop
1719 [rtac equal_intr_rule, Goal.norm_hhf_tac,
1720 etac meta_allE, atac,
1721 rtac (prop_subst OF [surject]),
1722 REPEAT o etac meta_allE, atac]);
1723 val split_meta = timeit_msg ctxt "record extension split_meta proof:" split_meta_prf;
1726 let val (assm, concl) = induct_prop in
1727 prove_standard [assm] concl
1729 cut_rules_tac [split_meta RS Drule.equal_elim_rule2] 1 THEN
1730 resolve_tac prems 2 THEN
1731 asm_simp_tac HOL_ss 1)
1733 val induct = timeit_msg ctxt "record extension induct proof:" induct_prf;
1735 val ([induct', inject', surjective', split_meta'], thm_thy) =
1737 |> Global_Theory.add_thms (map (Thm.no_attributes o apfst Binding.name)
1738 [("ext_induct", induct),
1739 ("ext_inject", inject),
1740 ("ext_surjective", surject),
1741 ("ext_split", split_meta)]);
1744 (((ext_name, ext_type), (ext_tyco, alphas_zeta),
1745 extT, induct', inject', surjective', split_meta', ext_def), thm_thy)
1748 fun chunks [] [] = []
1749 | chunks [] xs = [xs]
1750 | chunks (l :: ls) xs = take l xs :: chunks ls (drop l xs);
1752 fun chop_last [] = error "chop_last: list should not be empty"
1753 | chop_last [x] = ([], x)
1754 | chop_last (x :: xs) = let val (tl, l) = chop_last xs in (x :: tl, l) end;
1756 fun subst_last _ [] = error "subst_last: list should not be empty"
1757 | subst_last s [_] = [s]
1758 | subst_last s (x :: xs) = x :: subst_last s xs;
1763 (*build up the record type from the current extension tpye extT and a list
1764 of parent extensions, starting with the root of the record hierarchy*)
1765 fun mk_recordT extT =
1766 fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT;
1769 fun obj_to_meta_all thm =
1771 fun E thm = (* FIXME proper name *)
1772 (case SOME (spec OF [thm]) handle THM _ => NONE of
1776 val th2 = Drule.forall_intr_vars th1;
1779 fun meta_to_obj_all thm =
1781 val thy = Thm.theory_of_thm thm;
1782 val prop = Thm.prop_of thm;
1783 val params = Logic.strip_params prop;
1784 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop);
1785 val ct = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.list_all (params, concl)));
1786 val thm' = Seq.hd (REPEAT (rtac allI 1) (Thm.trivial ct));
1787 in Thm.implies_elim thm' thm end;
1790 (* code generation *)
1792 fun mk_random_eq tyco vs extN Ts =
1794 (* FIXME local i etc. *)
1795 val size = @{term "i::code_numeral"};
1796 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
1797 val T = Type (tyco, map TFree vs);
1798 val Tm = termifyT T;
1799 val params = Name.invent_names Name.context "x" Ts;
1800 val lhs = HOLogic.mk_random T size;
1801 val tc = HOLogic.mk_return Tm @{typ Random.seed}
1802 (HOLogic.mk_valtermify_app extN params T);
1806 ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params)
1807 tc @{typ Random.seed} (SOME Tm, @{typ Random.seed});
1812 fun mk_full_exhaustive_eq tyco vs extN Ts =
1814 (* FIXME local i etc. *)
1815 val size = @{term "i::code_numeral"};
1816 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
1817 val T = Type (tyco, map TFree vs);
1818 val test_function = Free ("f", termifyT T --> @{typ "term list option"});
1819 val params = Name.invent_names Name.context "x" Ts;
1820 fun full_exhaustiveT T =
1821 (termifyT T --> @{typ "Code_Evaluation.term list option"}) -->
1822 @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"};
1823 fun mk_full_exhaustive T =
1824 Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
1825 full_exhaustiveT T);
1826 val lhs = mk_full_exhaustive T $ test_function $ size;
1827 val tc = test_function $ (HOLogic.mk_valtermify_app extN params T);
1828 val rhs = fold_rev (fn (v, T) => fn cont =>
1829 mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc;
1834 fun instantiate_sort_record (sort, mk_eq) tyco vs extN Ts thy =
1836 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_eq tyco vs extN Ts));
1839 |> Class.instantiation ([tyco], vs, sort)
1840 |> `(fn lthy => Syntax.check_term lthy eq)
1841 |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
1843 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
1846 fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy =
1848 val algebra = Sign.classes_of thy;
1849 val has_inst = can (Sorts.mg_domain algebra ext_tyco) sort;
1851 if has_inst then thy
1853 (case Quickcheck_Common.perhaps_constrain thy (map (rpair sort) Ts) vs of
1855 instantiate_sort_record (sort, mk_eq) ext_tyco (map constrain vs) extN
1856 ((map o map_atyps) (fn TFree v => TFree (constrain v)) Ts) thy
1860 fun add_code ext_tyco vs extT ext simps inject thy =
1863 (HOLogic.mk_Trueprop o HOLogic.mk_eq)
1864 (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
1865 Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT));
1867 Class.intro_classes_tac []
1868 THEN (Simplifier.rewrite_goals_tac [Simpdata.mk_eq eq_def])
1869 THEN ALLGOALS (rtac @{thm refl});
1870 fun mk_eq thy eq_def = Simplifier.rewrite_rule
1871 [(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject;
1872 fun mk_eq_refl thy =
1875 ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
1876 |> AxClass.unoverload thy;
1877 val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
1878 val ensure_exhaustive_record =
1879 ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
1882 |> Code.add_datatype [ext]
1883 |> fold Code.add_default_eqn simps
1884 |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
1885 |> `(fn lthy => Syntax.check_term lthy eq)
1886 |-> (fn eq => Specification.definition
1887 (NONE, (Attrib.empty_binding, eq)))
1888 |-> (fn (_, (_, eq_def)) =>
1889 Class.prove_instantiation_exit_result Morphism.thm
1890 (fn _ => fn eq_def => tac eq_def) eq_def)
1891 |-> (fn eq_def => fn thy =>
1892 thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
1893 |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
1894 |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
1895 |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
1901 fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
1903 val ctxt = Proof_Context.init_global thy;
1905 val prefix = Binding.name_of binding;
1906 val name = Sign.full_name thy binding;
1907 val full = Sign.full_name_path thy prefix;
1909 val bfields = map (fn (x, T, _) => (x, T)) raw_fields;
1910 val field_syntax = map #3 raw_fields;
1912 val parent_fields = maps #fields parents;
1913 val parent_chunks = map (length o #fields) parents;
1914 val parent_names = map fst parent_fields;
1915 val parent_types = map snd parent_fields;
1916 val parent_fields_len = length parent_fields;
1917 val parent_variants =
1918 Name.variant_list [moreN, rN, rN ^ "'", wN] (map Long_Name.base_name parent_names);
1919 val parent_vars = map2 (curry Free) parent_variants parent_types;
1920 val parent_len = length parents;
1922 val fields = map (apfst full) bfields;
1923 val names = map fst fields;
1924 val types = map snd fields;
1925 val alphas_fields = fold Term.add_tfreesT types [];
1926 val alphas_ext = inter (op =) alphas_fields alphas;
1927 val len = length fields;
1929 Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
1930 (map (Binding.name_of o fst) bfields);
1931 val vars = map2 (curry Free) variants types;
1932 val named_vars = names ~~ vars;
1933 val idxms = 0 upto len;
1935 val all_fields = parent_fields @ fields;
1936 val all_types = parent_types @ types;
1937 val all_variants = parent_variants @ variants;
1938 val all_vars = parent_vars @ vars;
1939 val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
1941 val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", HOLogic.typeS);
1942 val moreT = TFree zeta;
1943 val more = Free (moreN, moreT);
1944 val full_moreN = full (Binding.name moreN);
1945 val bfields_more = bfields @ [(Binding.name moreN, moreT)];
1946 val fields_more = fields @ [(full_moreN, moreT)];
1947 val named_vars_more = named_vars @ [(full_moreN, more)];
1948 val all_vars_more = all_vars @ [more];
1949 val all_named_vars_more = all_named_vars @ [(full_moreN, more)];
1952 (* 1st stage: ext_thy *)
1954 val extension_name = full binding;
1956 val ((ext, (ext_tyco, vs),
1957 extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
1959 |> Sign.qualified_path false binding
1960 |> extension_definition extension_name fields alphas_ext zeta moreT more vars;
1962 val _ = timing_msg ctxt "record preparing definitions";
1963 val Type extension_scheme = extT;
1964 val extension_name = unsuffix ext_typeN (fst extension_scheme);
1965 val extension = let val (n, Ts) = extension_scheme in (n, subst_last HOLogic.unitT Ts) end;
1966 val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extension_name];
1967 val extension_id = implode extension_names;
1969 fun rec_schemeT n = mk_recordT (map #extension (drop n parents)) extT;
1970 val rec_schemeT0 = rec_schemeT 0;
1973 let val (c, Ts) = extension in
1974 mk_recordT (map #extension (drop n parents))
1975 (Type (c, subst_last HOLogic.unitT Ts))
1981 val (args', more) = chop_last args;
1982 fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]);
1984 fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args')) more;
1986 if more = HOLogic.unit
1987 then build (map_range recT (parent_len + 1))
1988 else build (map_range rec_schemeT (parent_len + 1))
1991 val r_rec0 = mk_rec all_vars_more 0;
1992 val r_rec_unit0 = mk_rec (all_vars @ [HOLogic.unit]) 0;
1994 fun r n = Free (rN, rec_schemeT n);
1996 fun r_unit n = Free (rN, recT n);
1997 val r_unit0 = r_unit 0;
1998 val w = Free (wN, rec_schemeT 0);
2001 (* print translations *)
2003 val record_ext_type_abbr_tr's =
2005 val trname = hd extension_names;
2006 val last_ext = unsuffix ext_typeN (fst extension);
2007 in [record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0 trname] end;
2009 val record_ext_type_tr's =
2011 (*avoid conflict with record_type_abbr_tr's*)
2012 val trnames = if parent_len > 0 then [extension_name] else [];
2013 in map record_ext_type_tr' trnames end;
2015 val advanced_print_translation =
2016 map field_update_tr' (full_moreN :: names) @ [record_ext_tr' extension_name] @
2017 record_ext_type_tr's @ record_ext_type_abbr_tr's;
2020 (* prepare declarations *)
2022 val sel_decls = map (mk_selC rec_schemeT0 o apfst Binding.name_of) bfields_more;
2023 val upd_decls = map (mk_updC updateN rec_schemeT0 o apfst Binding.name_of) bfields_more;
2024 val make_decl = (makeN, all_types ---> recT0);
2025 val fields_decl = (fields_selN, types ---> Type extension);
2026 val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0);
2027 val truncate_decl = (truncateN, rec_schemeT0 --> recT0);
2030 (* prepare definitions *)
2032 val ext_defs = ext_def :: map #ext_def parents;
2034 (*Theorems from the iso_tuple intros.
2035 By unfolding ext_defs from r_rec0 we create a tree of constructor
2036 calls (many of them Pair, but others as well). The introduction
2037 rules for update_accessor_eq_assist can unify two different ways
2038 on these constructors. If we take the complete result sequence of
2039 running a the introduction tactic, we get one theorem for each upd/acc
2040 pair, from which we can derive the bodies of our selector and
2041 updator and their convs.*)
2042 fun get_access_update_thms () =
2046 (*pick variable indices of 1 to avoid possible variable
2047 collisions with existing variables in updacc_eq_triv*)
2048 fun to_Var (Free (c, T)) = Var ((c, 1), T);
2049 in mk_rec (map to_Var all_vars_more) 0 end;
2051 val cterm_rec = cterm_of ext_thy r_rec0;
2052 val cterm_vrs = cterm_of ext_thy r_rec0_Vars;
2053 val insts = [("v", cterm_rec), ("v'", cterm_vrs)];
2054 val init_thm = named_cterm_instantiate insts updacc_eq_triv;
2055 val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
2057 simp_tac (HOL_basic_ss addsimps ext_defs) 1 THEN
2058 REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE terminal);
2059 val updaccs = Seq.list_of (tactic init_thm);
2061 (updaccs RL [updacc_accessor_eqE],
2062 updaccs RL [updacc_updator_eqE],
2063 updaccs RL [updacc_cong_from_eq])
2065 val (accessor_thms, updator_thms, upd_acc_cong_assists) =
2066 timeit_msg ctxt "record getting tree access/updates:" get_access_update_thms;
2068 fun lastN xs = drop parent_fields_len xs;
2071 fun mk_sel_spec ((c, T), thm) =
2073 val (acc $ arg, _) =
2074 HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (Thm.concl_of thm)));
2076 if arg aconv r_rec0 then ()
2077 else raise TERM ("mk_sel_spec: different arg", [arg]);
2079 Const (mk_selC rec_schemeT0 (c, T)) :== acc
2081 val sel_specs = map mk_sel_spec (fields_more ~~ lastN accessor_thms);
2084 fun mk_upd_spec ((c, T), thm) =
2086 val (upd $ _ $ arg, _) =
2087 HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (Thm.concl_of thm)));
2089 if arg aconv r_rec0 then ()
2090 else raise TERM ("mk_sel_spec: different arg", [arg]);
2091 in Const (mk_updC updateN rec_schemeT0 (c, T)) :== upd end;
2092 val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms);
2094 (*derived operations*)
2096 list_comb (Const (full (Binding.name makeN), all_types ---> recT0), all_vars) :==
2097 mk_rec (all_vars @ [HOLogic.unit]) 0;
2099 list_comb (Const (full (Binding.name fields_selN), types ---> Type extension), vars) :==
2100 mk_rec (all_vars @ [HOLogic.unit]) parent_len;
2102 Const (full (Binding.name extendN), recT0 --> moreT --> rec_schemeT0) $ r_unit0 $ more :==
2103 mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
2105 Const (full (Binding.name truncateN), rec_schemeT0 --> recT0) $ r0 :==
2106 mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
2109 (* 2st stage: defs_thy *)
2113 |> Sign.add_advanced_trfuns ([], [], advanced_print_translation, [])
2114 |> Sign.restore_naming thy
2115 |> Typedecl.abbrev_global (binding, map #1 alphas, NoSyn) recT0 |> snd
2116 |> Typedecl.abbrev_global
2117 (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0 |> snd
2118 |> Sign.qualified_path false binding
2119 |> fold (fn ((x, T), mx) => snd o Sign.declare_const_global ((Binding.name x, T), mx))
2120 (sel_decls ~~ (field_syntax @ [NoSyn]))
2121 |> fold (fn (x, T) => snd o Sign.declare_const_global ((Binding.name x, T), NoSyn))
2122 (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
2123 |> (Global_Theory.add_defs false o
2124 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) sel_specs
2125 ||>> (Global_Theory.add_defs false o
2126 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) upd_specs
2127 ||>> (Global_Theory.add_defs false o
2128 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
2129 [make_spec, fields_spec, extend_spec, truncate_spec]
2130 ||> Theory.checkpoint
2131 val (((sel_defs, upd_defs), derived_defs), defs_thy) =
2132 timeit_msg ctxt "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
2135 (* prepare propositions *)
2136 val _ = timing_msg ctxt "record preparing propositions";
2137 val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> HOLogic.boolT);
2138 val C = Free (singleton (Name.variant_list all_variants) "C", HOLogic.boolT);
2139 val P_unit = Free (singleton (Name.variant_list all_variants) "P", recT0 --> HOLogic.boolT);
2142 val sel_conv_props =
2143 map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more;
2146 fun mk_upd_prop i (c, T) =
2149 Free (singleton (Name.variant_list all_variants) (Long_Name.base_name c ^ "'"), T --> T);
2150 val n = parent_fields_len + i;
2151 val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more;
2152 in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
2153 val upd_conv_props = map2 mk_upd_prop idxms fields_more;
2156 val induct_scheme_prop =
2157 All (map dest_Free all_vars_more) (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0);
2159 (All (map dest_Free all_vars) (Trueprop (P_unit $ r_rec_unit0)),
2160 Trueprop (P_unit $ r_unit0));
2163 val surjective_prop =
2164 let val args = map (fn (c, Free (_, T)) => mk_sel r0 (c, T)) all_named_vars_more
2165 in r0 === mk_rec args 0 end;
2168 val cases_scheme_prop =
2169 (All (map dest_Free all_vars_more) ((r0 === r_rec0) ==> Trueprop C))
2173 (All (map dest_Free all_vars) ((r_unit0 === r_rec_unit0) ==> Trueprop C))
2177 val split_meta_prop =
2179 val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0-->Term.propT);
2182 (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
2185 val split_object_prop =
2186 let val ALL = fold_rev (fn (v, T) => fn t => HOLogic.mk_all (v, T, t))
2187 in ALL [dest_Free r0] (P $ r0) === ALL (map dest_Free all_vars_more) (P $ r_rec0) end;
2190 let val EX = fold_rev (fn (v, T) => fn t => HOLogic.mk_exists (v, T, t))
2191 in EX [dest_Free r0] (P $ r0) === EX (map dest_Free all_vars_more) (P $ r_rec0) end;
2196 val s' = Free (rN ^ "'", rec_schemeT0);
2197 fun mk_sel_eq (c, Free (_, T)) = mk_sel r0 (c, T) === mk_sel s' (c, T);
2198 val seleqs = map mk_sel_eq all_named_vars_more;
2199 in All (map dest_Free [r0, s']) (Logic.list_implies (seleqs, r0 === s')) end;
2202 (* 3rd stage: thms_thy *)
2204 fun prove stndrd = prove_future_global stndrd defs_thy;
2205 val prove_standard = prove_future_global true defs_thy;
2206 val future_forward_prf = future_forward_prf_standard defs_thy;
2208 fun prove_simp stndrd ss simps =
2209 let val tac = simp_all_tac ss simps
2210 in fn prop => prove stndrd [] prop (K tac) end;
2212 val ss = get_simpset defs_thy;
2214 fun sel_convs_prf () =
2215 map (prove_simp false ss (sel_defs @ accessor_thms)) sel_conv_props;
2216 val sel_convs = timeit_msg ctxt "record sel_convs proof:" sel_convs_prf;
2217 fun sel_convs_standard_prf () = map Drule.export_without_context sel_convs;
2218 val sel_convs_standard =
2219 timeit_msg ctxt "record sel_convs_standard proof:" sel_convs_standard_prf;
2221 fun upd_convs_prf () =
2222 map (prove_simp false ss (upd_defs @ updator_thms)) upd_conv_props;
2223 val upd_convs = timeit_msg ctxt "record upd_convs proof:" upd_convs_prf;
2224 fun upd_convs_standard_prf () = map Drule.export_without_context upd_convs;
2225 val upd_convs_standard =
2226 timeit_msg ctxt "record upd_convs_standard proof:" upd_convs_standard_prf;
2228 fun get_upd_acc_congs () =
2230 val symdefs = map Thm.symmetric (sel_defs @ upd_defs);
2231 val fold_ss = HOL_basic_ss addsimps symdefs;
2232 val ua_congs = map (Drule.export_without_context o simplify fold_ss) upd_acc_cong_assists;
2233 in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
2234 val (fold_congs, unfold_congs) =
2235 timeit_msg ctxt "record upd fold/unfold congs:" get_upd_acc_congs;
2237 val parent_induct = Option.map #induct_scheme (try List.last parents);
2239 fun induct_scheme_prf () =
2240 prove_standard [] induct_scheme_prop
2243 [case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
2244 try_param_tac rN ext_induct 1,
2245 asm_simp_tac HOL_basic_ss 1]);
2246 val induct_scheme = timeit_msg ctxt "record induct_scheme proof:" induct_scheme_prf;
2249 let val (assm, concl) = induct_prop in
2250 prove_standard [assm] concl (fn {prems, ...} =>
2251 try_param_tac rN induct_scheme 1
2252 THEN try_param_tac "more" @{thm unit.induct} 1
2253 THEN resolve_tac prems 1)
2255 val induct = timeit_msg ctxt "record induct proof:" induct_prf;
2257 fun cases_scheme_prf () =
2259 val _ $ (Pvar $ _) = concl_of induct_scheme;
2262 [(cterm_of defs_thy Pvar, cterm_of defs_thy
2263 (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
2265 in Object_Logic.rulify (mp OF [ind, refl]) end;
2267 val cases_scheme_prf = future_forward_prf cases_scheme_prf cases_scheme_prop;
2268 val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" cases_scheme_prf;
2271 prove_standard [] cases_prop
2273 try_param_tac rN cases_scheme 1 THEN
2274 simp_all_tac HOL_basic_ss [@{thm unit_all_eq1}]);
2275 val cases = timeit_msg ctxt "record cases proof:" cases_prf;
2277 fun surjective_prf () =
2279 val leaf_ss = get_sel_upd_defs defs_thy addsimps (sel_defs @ (o_assoc :: id_o_apps));
2280 val init_ss = HOL_basic_ss addsimps ext_defs;
2282 prove_standard [] surjective_prop
2285 [rtac surject_assist_idE 1,
2288 (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
2289 (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
2291 val surjective = timeit_msg ctxt "record surjective proof:" surjective_prf;
2293 fun split_meta_prf () =
2294 prove false [] split_meta_prop
2297 [rtac equal_intr_rule, Goal.norm_hhf_tac,
2298 etac meta_allE, atac,
2299 rtac (prop_subst OF [surjective]),
2300 REPEAT o etac meta_allE, atac]);
2301 val split_meta = timeit_msg ctxt "record split_meta proof:" split_meta_prf;
2302 fun split_meta_standardise () = Drule.export_without_context split_meta;
2303 val split_meta_standard =
2304 timeit_msg ctxt "record split_meta standard:" split_meta_standardise;
2306 fun split_object_prf () =
2308 val cPI= cterm_of defs_thy (lambda r0 (Trueprop (P $ r0)));
2309 val _ $ Abs (_, _, P $ _) = fst (Logic.dest_equals (concl_of split_meta_standard));
2310 val cP = cterm_of defs_thy P;
2311 val split_meta' = cterm_instantiate [(cP, cPI)] split_meta_standard;
2312 val (l, r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop);
2313 val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l);
2314 val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r);
2316 Thm.assume cl (*All r. P r*) (* 1 *)
2317 |> obj_to_meta_all (*!!r. P r*)
2318 |> Thm.equal_elim split_meta' (*!!n m more. P (ext n m more)*)
2319 |> meta_to_obj_all (*All n m more. P (ext n m more)*) (* 2*)
2320 |> Thm.implies_intr cl (* 1 ==> 2 *)
2322 Thm.assume cr (*All n m more. P (ext n m more)*)
2323 |> obj_to_meta_all (*!!n m more. P (ext n m more)*)
2324 |> Thm.equal_elim (Thm.symmetric split_meta') (*!!r. P r*)
2325 |> meta_to_obj_all (*All r. P r*)
2326 |> Thm.implies_intr cr (* 2 ==> 1 *)
2327 in thr COMP (thl COMP iffI) end;
2330 val split_object_prf = future_forward_prf split_object_prf split_object_prop;
2331 val split_object = timeit_msg ctxt "record split_object proof:" split_object_prf;
2334 fun split_ex_prf () =
2336 val ss = HOL_basic_ss addsimps [not_ex RS sym, Not_eq_iff];
2337 val P_nm = fst (dest_Free P);
2338 val not_P = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
2339 val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object;
2340 val so'' = simplify ss so';
2342 prove_standard [] split_ex_prop (fn _ => resolve_tac [so''] 1)
2344 val split_ex = timeit_msg ctxt "record split_ex proof:" split_ex_prf;
2346 fun equality_tac thms =
2348 val s' :: s :: eqs = rev thms;
2349 val ss' = ss addsimps (s' :: s :: sel_convs_standard);
2350 val eqs' = map (simplify ss') eqs;
2351 in simp_tac (HOL_basic_ss addsimps (s' :: s :: eqs')) 1 end;
2353 fun equality_prf () =
2354 prove_standard [] equality_prop (fn {context, ...} =>
2356 let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
2357 st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1 THEN
2358 res_inst_tac context [((rN, 0), s')] cases_scheme 1 THEN
2359 Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1)
2360 (*simp_all_tac ss (sel_convs) would also work but is less efficient*)
2362 val equality = timeit_msg ctxt "record equality proof:" equality_prf;
2364 val ((([sel_convs', upd_convs', sel_defs', upd_defs',
2365 fold_congs', unfold_congs',
2366 splits' as [split_meta', split_object', split_ex'], derived_defs'],
2367 [surjective', equality']),
2368 [induct_scheme', induct', cases_scheme', cases']), thms_thy) =
2370 |> (Global_Theory.add_thmss o map (Thm.no_attributes o apfst Binding.name))
2371 [("select_convs", sel_convs_standard),
2372 ("update_convs", upd_convs_standard),
2373 ("select_defs", sel_defs),
2374 ("update_defs", upd_defs),
2375 ("fold_congs", fold_congs),
2376 ("unfold_congs", unfold_congs),
2377 ("splits", [split_meta_standard, split_object, split_ex]),
2378 ("defs", derived_defs)]
2379 ||>> (Global_Theory.add_thms o map (Thm.no_attributes o apfst Binding.name))
2380 [("surjective", surjective),
2381 ("equality", equality)]
2382 ||>> (Global_Theory.add_thms o (map o apfst o apfst) Binding.name)
2383 [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
2384 (("induct", induct), induct_type_global name),
2385 (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
2386 (("cases", cases), cases_type_global name)];
2388 val sel_upd_simps = sel_convs' @ upd_convs';
2389 val sel_upd_defs = sel_defs' @ upd_defs';
2390 val iffs = [ext_inject]
2391 val depth = parent_len + 1;
2393 val ([simps', iffs'], thms_thy') =
2395 |> Global_Theory.add_thmss
2396 [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
2397 ((Binding.name "iffs", iffs), [iff_add])];
2400 make_info alphas parent fields extension
2401 ext_induct ext_inject ext_surjective ext_split ext_def
2402 sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs'
2403 surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs';
2407 |> put_record name info
2408 |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs')
2409 |> add_equalities extension_id equality'
2410 |> add_extinjects ext_inject
2411 |> add_extsplit extension_name ext_split
2412 |> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
2413 |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
2414 |> add_fieldext (extension_name, snd extension) names
2415 |> add_code ext_tyco vs extT ext simps' ext_inject
2416 |> Sign.restore_naming thy;
2425 fun read_parent NONE ctxt = (NONE, ctxt)
2426 | read_parent (SOME raw_T) ctxt =
2427 (case Proof_Context.read_typ_abbrev ctxt raw_T of
2428 Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt)
2429 | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));
2431 fun prep_field prep (x, T, mx) = (x, prep T, mx)
2433 cat_error msg ("The error(s) above occurred in record field " ^ Binding.print x);
2435 fun read_field raw_field ctxt =
2436 let val field as (_, T, _) = prep_field (Syntax.read_typ ctxt) raw_field
2437 in (field, Variable.declare_typ T ctxt) end;
2441 fun add_record quiet_mode (params, binding) raw_parent raw_fields thy =
2443 val _ = Theory.requires thy "Record" "record definitions";
2445 if quiet_mode then ()
2446 else writeln ("Defining record " ^ Binding.print binding ^ " ...");
2448 val ctxt = Proof_Context.init_global thy;
2449 fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T)
2450 handle TYPE (msg, _, _) => error msg;
2455 val parent = Option.map (apfst (map cert_typ)) raw_parent
2457 cat_error msg ("The error(s) above occurred in parent record specification");
2458 val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []);
2459 val parents = get_parent_info thy parent;
2461 val bfields = map (prep_field cert_typ) raw_fields;
2465 val name = Sign.full_name thy binding;
2466 val err_dup_record =
2467 if is_none (get_info thy name) then []
2468 else ["Duplicate definition of record " ^ quote name];
2470 val spec_frees = fold Term.add_tfreesT (parent_args @ map #2 bfields) [];
2471 val err_extra_frees =
2472 (case subtract (op =) params spec_frees of
2474 | extras => ["Extra free type variable(s) " ^
2475 commas (map (Syntax.string_of_typ ctxt o TFree) extras)]);
2477 val err_no_fields = if null bfields then ["No fields present"] else [];
2479 val err_dup_fields =
2480 (case duplicates Binding.eq_name (map #1 bfields) of
2482 | dups => ["Duplicate field(s) " ^ commas (map Binding.print dups)]);
2484 val err_bad_fields =
2485 if forall (not_equal moreN o Binding.name_of o #1) bfields then []
2486 else ["Illegal field name " ^ quote moreN];
2489 err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields;
2490 val _ = if null errs then () else error (cat_lines errs);
2492 thy |> definition (params, binding) parent parents bfields
2494 handle ERROR msg => cat_error msg ("Failed to define record " ^ Binding.print binding);
2496 fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy =
2498 val ctxt = Proof_Context.init_global thy;
2499 val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
2500 val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
2501 val (parent, ctxt2) = read_parent raw_parent ctxt1;
2502 val (fields, ctxt3) = fold_map read_field raw_fields ctxt2;
2503 val params' = map (Proof_Context.check_tfree ctxt3) params;
2504 in thy |> add_record quiet_mode (params', binding) parent fields end;
2512 Sign.add_trfuns ([], parse_translation, [], []) #>
2513 Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #>
2514 Simplifier.map_simpset_global (fn ss => ss addsimprocs [simproc, upd_simproc, eq_simproc]);
2520 Outer_Syntax.command "record" "define extensible record" Keyword.thy_decl
2521 (Parse.type_args_constrained -- Parse.binding --
2522 (Parse.$$$ "=" |-- Scan.option (Parse.typ --| Parse.$$$ "+") --
2523 Scan.repeat1 Parse.const_binding)
2524 >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z)));