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: (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";
252 fun varifyT idx = map_type_tfree (fn (a, S) => TVar ((a, idx), S));
257 val timing = Attrib.setup_config_bool @{binding record_timing} (K false);
258 fun timeit_msg ctxt s x = if Config.get ctxt timing then (warning s; timeit x) else x ();
259 fun timing_msg ctxt s = if Config.get ctxt timing then warning s else ();
264 val Trueprop = HOLogic.mk_Trueprop;
265 fun All xs t = Term.list_all_free (xs, t);
270 val op :== = Misc_Legacy.mk_defpair;
271 val op === = Trueprop o HOLogic.mk_eq;
272 val op ==> = Logic.mk_implies;
277 fun mk_ext (name, T) ts =
278 let val Ts = map fastype_of ts
279 in list_comb (Const (suffix extN name, Ts ---> T), ts) end;
284 fun mk_selC sT (c, T) = (c, sT --> T);
286 fun mk_sel s (c, T) =
287 let val sT = fastype_of s
288 in Const (mk_selC sT (c, T)) $ s end;
293 fun mk_updC sfx sT (c, T) = (suffix sfx c, (T --> T) --> sT --> sT);
295 fun mk_upd' sfx c v sT =
296 let val vT = domain_type (fastype_of v);
297 in Const (mk_updC sfx sT (c, vT)) $ v end;
299 fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s;
304 fun dest_recT (typ as Type (c_ext_type, Ts as (_ :: _))) =
305 (case try (unsuffix ext_typeN) c_ext_type of
306 NONE => raise TYPE ("Record.dest_recT", [typ], [])
307 | SOME c => ((c, Ts), List.last Ts))
308 | dest_recT typ = raise TYPE ("Record.dest_recT", [typ], []);
310 val is_recT = can dest_recT;
313 let val ((c, Ts), U) = dest_recT T
314 in (c, Ts) :: dest_recTs U
315 end handle TYPE _ => [];
318 let val ((c, Ts), U) = dest_recT T in
322 end handle TYPE _ => NONE;
326 val rTs = dest_recTs T;
327 val rTs' = if i < 0 then rTs else take i rTs;
328 in implode (map #1 rTs') end;
332 (*** extend theory by record definition ***)
336 (* type info and parent_info *)
339 {args: (string * sort) list,
340 parent: (typ list * string) option,
341 fields: (string * typ) list,
342 extension: (string * typ list),
350 select_convs: thm list,
351 update_convs: thm list,
352 select_defs: thm list,
353 update_defs: thm list,
354 fold_congs: thm list,
355 unfold_congs: thm list,
369 fun make_info args parent fields extension
370 ext_induct ext_inject ext_surjective ext_split ext_def
371 select_convs update_convs select_defs update_defs fold_congs unfold_congs splits defs
372 surjective equality induct_scheme induct cases_scheme cases
374 {args = args, parent = parent, fields = fields, extension = extension,
375 ext_induct = ext_induct, ext_inject = ext_inject, ext_surjective = ext_surjective,
376 ext_split = ext_split, ext_def = ext_def, select_convs = select_convs,
377 update_convs = update_convs, select_defs = select_defs, update_defs = update_defs,
378 fold_congs = fold_congs, unfold_congs = unfold_congs, splits = splits, defs = defs,
379 surjective = surjective, equality = equality, induct_scheme = induct_scheme,
380 induct = induct, cases_scheme = cases_scheme, cases = cases, simps = simps, iffs = iffs};
384 fields: (string * typ) list,
385 extension: (string * typ list),
389 fun make_parent_info name fields extension ext_def induct_scheme : parent_info =
390 {name = name, fields = fields, extension = extension,
391 ext_def = ext_def, induct_scheme = induct_scheme};
397 {records: info Symtab.table,
399 {selectors: (int * bool) Symtab.table,
400 updates: string Symtab.table,
401 simpset: Simplifier.simpset,
402 defset: Simplifier.simpset,
403 foldcong: Simplifier.simpset,
404 unfoldcong: Simplifier.simpset},
405 equalities: thm Symtab.table,
406 extinjects: thm list,
407 extsplit: thm Symtab.table, (*maps extension name to split rule*)
408 splits: (thm * thm * thm * thm) Symtab.table, (*!!, ALL, EX - split-equalities, induct rule*)
409 extfields: (string * typ) list Symtab.table, (*maps extension to its fields*)
410 fieldext: (string * typ list) Symtab.table}; (*maps field to its extension*)
413 records sel_upd equalities extinjects extsplit splits extfields fieldext =
414 {records = records, sel_upd = sel_upd,
415 equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
416 extfields = extfields, fieldext = fieldext }: data;
418 structure Data = Theory_Data
422 make_data Symtab.empty
423 {selectors = Symtab.empty, updates = Symtab.empty,
424 simpset = HOL_basic_ss, defset = HOL_basic_ss,
425 foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
426 Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
431 {selectors = sels1, updates = upds1,
432 simpset = ss1, defset = ds1,
433 foldcong = fc1, unfoldcong = uc1},
434 equalities = equalities1,
435 extinjects = extinjects1,
436 extsplit = extsplit1,
438 extfields = extfields1,
439 fieldext = fieldext1},
442 {selectors = sels2, updates = upds2,
443 simpset = ss2, defset = ds2,
444 foldcong = fc2, unfoldcong = uc2},
445 equalities = equalities2,
446 extinjects = extinjects2,
447 extsplit = extsplit2,
449 extfields = extfields2,
450 fieldext = fieldext2}) =
452 (Symtab.merge (K true) (recs1, recs2))
453 {selectors = Symtab.merge (K true) (sels1, sels2),
454 updates = Symtab.merge (K true) (upds1, upds2),
455 simpset = Simplifier.merge_ss (ss1, ss2),
456 defset = Simplifier.merge_ss (ds1, ds2),
457 foldcong = Simplifier.merge_ss (fc1, fc2),
458 unfoldcong = Simplifier.merge_ss (uc1, uc2)}
459 (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
460 (Thm.merge_thms (extinjects1, extinjects2))
461 (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
462 (Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
463 Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
464 Thm.eq_thm (c, y) andalso Thm.eq_thm (d, z)) (splits1, splits2))
465 (Symtab.merge (K true) (extfields1, extfields2))
466 (Symtab.merge (K true) (fieldext1, fieldext2));
470 (* access 'records' *)
472 val get_info = Symtab.lookup o #records o Data.get;
474 fun the_info thy name =
475 (case get_info thy name of
477 | NONE => error ("Unknown record type " ^ quote name));
479 fun put_record name info =
480 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
481 make_data (Symtab.update (name, info) records)
482 sel_upd equalities extinjects extsplit splits extfields fieldext);
485 (* access 'sel_upd' *)
487 val get_sel_upd = #sel_upd o Data.get;
489 val is_selector = Symtab.defined o #selectors o get_sel_upd;
490 val get_updates = Symtab.lookup o #updates o get_sel_upd;
491 fun get_ss_with_context getss thy = Simplifier.global_context thy (getss (get_sel_upd thy));
493 val get_simpset = get_ss_with_context #simpset;
494 val get_sel_upd_defs = get_ss_with_context #defset;
496 fun get_update_details u thy =
497 let val sel_upd = get_sel_upd thy in
498 (case Symtab.lookup (#updates sel_upd) u of
500 let val SOME (dep, ismore) = Symtab.lookup (#selectors sel_upd) s
501 in SOME (s, dep, ismore) end
505 fun put_sel_upd names more depth simps defs (folds, unfolds) thy =
507 val all = names @ [more];
508 val sels = map (rpair (depth, false)) names @ [(more, (depth, true))];
509 val upds = map (suffix updateN) all ~~ all;
511 val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong},
512 equalities, extinjects, extsplit, splits, extfields, fieldext} = Data.get thy;
513 val data = make_data records
514 {selectors = fold Symtab.update_new sels selectors,
515 updates = fold Symtab.update_new upds updates,
516 simpset = Simplifier.addsimps (simpset, simps),
517 defset = Simplifier.addsimps (defset, defs),
518 foldcong = foldcong addcongs folds,
519 unfoldcong = unfoldcong addcongs unfolds}
520 equalities extinjects extsplit splits extfields fieldext;
521 in Data.put data thy end;
524 (* access 'equalities' *)
526 fun add_equalities name thm =
527 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
528 make_data records sel_upd
529 (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext);
531 val get_equalities = Symtab.lookup o #equalities o Data.get;
534 (* access 'extinjects' *)
536 fun add_extinjects thm =
537 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
538 make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
539 extsplit splits extfields fieldext);
541 val get_extinjects = rev o #extinjects o Data.get;
544 (* access 'extsplit' *)
546 fun add_extsplit name thm =
547 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
548 make_data records sel_upd equalities extinjects
549 (Symtab.update_new (name, thm) extsplit) splits extfields fieldext);
552 (* access 'splits' *)
554 fun add_splits name thmP =
555 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
556 make_data records sel_upd equalities extinjects extsplit
557 (Symtab.update_new (name, thmP) splits) extfields fieldext);
559 val get_splits = Symtab.lookup o #splits o Data.get;
562 (* parent/extension of named record *)
564 val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o Data.get);
565 val get_extension = Option.map #extension oo (Symtab.lookup o #records o Data.get);
568 (* access 'extfields' *)
570 fun add_extfields name fields =
571 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
572 make_data records sel_upd equalities extinjects extsplit splits
573 (Symtab.update_new (name, fields) extfields) fieldext);
575 val get_extfields = Symtab.lookup o #extfields o Data.get;
577 fun get_extT_fields thy T =
579 val ((name, Ts), moreT) = dest_recT T;
581 let val (nm :: _ :: rst) = rev (Long_Name.explode name) (* FIXME !? *)
582 in Long_Name.implode (rev (nm :: rst)) end;
583 val varifyT = varifyT (maxidx_of_typs (moreT :: Ts) + 1);
584 val {records, extfields, ...} = Data.get thy;
585 val (fields, (more, _)) = split_last (Symtab.lookup_list extfields name);
586 val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
588 val subst = fold (Sign.typ_match thy) (#1 (split_last args) ~~ #1 (split_last Ts)) Vartab.empty;
589 val fields' = map (apsnd (Envir.norm_type subst o varifyT)) fields;
590 in (fields', (more, moreT)) end;
592 fun get_recT_fields thy T =
594 val (root_fields, (root_more, root_moreT)) = get_extT_fields thy T;
595 val (rest_fields, rest_more) =
596 if is_recT root_moreT then get_recT_fields thy root_moreT
597 else ([], (root_more, root_moreT));
598 in (root_fields @ rest_fields, rest_more) end;
601 (* access 'fieldext' *)
603 fun add_fieldext extname_types fields =
604 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
607 fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
608 in make_data records sel_upd equalities extinjects extsplit splits extfields fieldext' end);
610 val get_fieldext = Symtab.lookup o #fieldext o Data.get;
617 fun add_parents _ NONE = I
618 | add_parents thy (SOME (types, name)) =
620 fun err msg = error (msg ^ " parent record " ^ quote name);
622 val {args, parent, ...} =
623 (case get_info thy name of SOME info => info | NONE => err "Unknown");
624 val _ = if length types <> length args then err "Bad number of arguments for" else ();
626 fun bad_inst ((x, S), T) =
627 if Sign.of_sort thy (T, S) then NONE else SOME x
628 val bads = map_filter bad_inst (args ~~ types);
629 val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");
631 val inst = args ~~ types;
632 val subst = Term.map_type_tfree (the o AList.lookup (op =) inst);
633 val parent' = Option.map (apfst (map subst)) parent;
634 in cons (name, inst) #> add_parents thy parent' end;
638 fun get_hierarchy thy (name, types) = add_parents thy (SOME (types, name)) [];
640 fun get_parent_info thy parent =
641 add_parents thy parent [] |> map (fn (name, inst) =>
643 val subst = Term.map_type_tfree (the o AList.lookup (op =) inst);
644 val {fields, extension, induct_scheme, ext_def, ...} = the_info thy name;
645 val fields' = map (apsnd subst) fields;
646 val extension' = apsnd (map subst) extension;
647 in make_parent_info name fields' extension' ext_def induct_scheme end);
653 (** concrete syntax for records **)
655 (* parse translations *)
659 fun split_args (field :: fields) ((name, arg) :: fargs) =
660 if can (unsuffix name) field then
661 let val (args, rest) = split_args fields fargs
662 in (arg :: args, rest) end
663 else raise Fail ("expecting field " ^ quote field ^ " but got " ^ quote name)
664 | split_args [] (fargs as (_ :: _)) = ([], fargs)
665 | split_args (_ :: _) [] = raise Fail "expecting more fields"
666 | split_args _ _ = ([], []);
668 fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) =
670 | field_type_tr t = raise TERM ("field_type_tr", [t]);
672 fun field_types_tr (Const (@{syntax_const "_field_types"}, _) $ t $ u) =
673 field_type_tr t :: field_types_tr u
674 | field_types_tr t = [field_type_tr t];
676 fun record_field_types_tr more ctxt t =
678 val thy = Proof_Context.theory_of ctxt;
679 fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]);
681 fun mk_ext (fargs as (name, _) :: _) =
682 (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
683 SOME (ext, alphas) =>
684 (case get_extfields thy ext of
687 val (fields', _) = split_last fields;
688 val types = map snd fields';
689 val (args, rest) = split_args (map fst fields') fargs
690 handle Fail msg => err msg;
691 val argtypes = Syntax.check_typs ctxt (map Syntax_Phases.decode_typ args);
692 val varifyT = varifyT (fold Term.maxidx_typ argtypes ~1 + 1);
693 val vartypes = map varifyT types;
695 val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
696 handle Type.TYPE_MATCH => err "type is no proper record (extension)";
698 map (Syntax_Phases.term_of_typ ctxt o Envir.norm_type subst o varifyT)
699 (#1 (split_last alphas));
701 val more' = mk_ext rest;
704 (Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
706 | NONE => err ("no fields defined for " ^ quote ext))
707 | NONE => err (quote name ^ " is no proper field"))
710 mk_ext (field_types_tr t)
713 fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const @{type_syntax unit}) ctxt t
714 | record_type_tr _ ts = raise TERM ("record_type_tr", ts);
716 fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t
717 | record_type_scheme_tr _ ts = raise TERM ("record_type_scheme_tr", ts);
720 fun field_tr ((Const (@{syntax_const "_field"}, _) $ Const (name, _) $ arg)) = (name, arg)
721 | field_tr t = raise TERM ("field_tr", [t]);
723 fun fields_tr (Const (@{syntax_const "_fields"}, _) $ t $ u) = field_tr t :: fields_tr u
724 | fields_tr t = [field_tr t];
726 fun record_fields_tr more ctxt t =
728 val thy = Proof_Context.theory_of ctxt;
729 fun err msg = raise TERM ("Error in record input: " ^ msg, [t]);
731 fun mk_ext (fargs as (name, _) :: _) =
732 (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
734 (case get_extfields thy ext of
737 val (args, rest) = split_args (map fst (fst (split_last fields))) fargs
738 handle Fail msg => err msg;
739 val more' = mk_ext rest;
740 in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end
741 | NONE => err ("no fields defined for " ^ quote ext))
742 | NONE => err (quote name ^ " is no proper field"))
744 in mk_ext (fields_tr t) end;
746 fun record_tr ctxt [t] = record_fields_tr (Syntax.const @{const_syntax Unity}) ctxt t
747 | record_tr _ ts = raise TERM ("record_tr", ts);
749 fun record_scheme_tr ctxt [t, more] = record_fields_tr more ctxt t
750 | record_scheme_tr _ ts = raise TERM ("record_scheme_tr", ts);
753 fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) =
754 Syntax.const (suffix updateN name) $ Abs (Name.uu_, dummyT, arg)
755 | field_update_tr t = raise TERM ("field_update_tr", [t]);
757 fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) =
758 field_update_tr t :: field_updates_tr u
759 | field_updates_tr t = [field_update_tr t];
761 fun record_update_tr [t, u] = fold (curry op $) (field_updates_tr u) t
762 | record_update_tr ts = raise TERM ("record_update_tr", ts);
766 val parse_translation =
767 [(@{syntax_const "_record_update"}, record_update_tr)];
769 val advanced_parse_translation =
770 [(@{syntax_const "_record"}, record_tr),
771 (@{syntax_const "_record_scheme"}, record_scheme_tr),
772 (@{syntax_const "_record_type"}, record_type_tr),
773 (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)];
778 (* print translations *)
780 val type_abbr = Attrib.setup_config_bool @{binding record_type_abbr} (K true);
781 val type_as_fields = Attrib.setup_config_bool @{binding record_type_as_fields} (K true);
786 (* FIXME early extern (!??) *)
787 (* FIXME Syntax.free (??) *)
788 fun field_type_tr' (c, t) = Syntax.const @{syntax_const "_field_type"} $ Syntax.const c $ t;
790 fun field_types_tr' (t, u) = Syntax.const @{syntax_const "_field_types"} $ t $ u;
792 fun record_type_tr' ctxt t =
794 val thy = Proof_Context.theory_of ctxt;
796 val T = Syntax_Phases.decode_typ t;
797 val varifyT = varifyT (Term.maxidx_of_typ T + 1);
801 Type (ext, args as _ :: _) =>
802 (case try (unsuffix ext_typeN) ext of
804 (case get_extfields thy ext' of
805 SOME (fields as (x, _) :: _) =>
806 (case get_fieldext thy x of
809 val (f :: fs, _) = split_last fields;
811 apfst (Proof_Context.extern_const ctxt) f ::
812 map (apfst Long_Name.base_name) fs;
813 val (args', more) = split_last args;
814 val alphavars = map varifyT (#1 (split_last alphas));
815 val subst = Type.raw_matches (alphavars, args') Vartab.empty;
816 val fields'' = (map o apsnd) (Envir.norm_type subst o varifyT) fields';
817 in fields'' @ strip_fields more end
818 handle Type.TYPE_MATCH => [("", T)])
824 val (fields, (_, moreT)) = split_last (strip_fields T);
825 val _ = null fields andalso raise Match;
827 foldr1 field_types_tr'
828 (map (field_type_tr' o apsnd (Syntax_Phases.term_of_typ ctxt)) fields);
830 if not (Config.get ctxt type_as_fields) orelse null fields then raise Match
831 else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
833 Syntax.const @{syntax_const "_record_type_scheme"} $ u $
834 Syntax_Phases.term_of_typ ctxt moreT
837 (*try to reconstruct the record name type abbreviation from
838 the (nested) extension types*)
839 fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm =
841 val T = Syntax_Phases.decode_typ tm;
842 val varifyT = varifyT (maxidx_of_typ T + 1);
844 fun mk_type_abbr subst name args =
845 let val abbrT = Type (name, map (varifyT o TFree) args)
846 in Syntax_Phases.term_of_typ ctxt (Envir.norm_type subst abbrT) end;
848 fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
850 if Config.get ctxt type_abbr then
853 if name = last_ext then
854 let val subst = match schemeT T in
855 if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree zeta)))
856 then mk_type_abbr subst abbr alphas
857 else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
858 end handle Type.TYPE_MATCH => record_type_tr' ctxt tm
859 else raise Match (*give print translation of specialised record a chance*)
861 else record_type_tr' ctxt tm
866 fun record_ext_type_tr' name =
868 val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);
870 record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts));
871 in (ext_type_name, tr') end;
873 fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
875 val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);
877 record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt
878 (list_comb (Syntax.const ext_type_name, ts));
879 in (ext_type_name, tr') end;
886 (* FIXME Syntax.free (??) *)
887 fun field_tr' (c, t) = Syntax.const @{syntax_const "_field"} $ Syntax.const c $ t;
888 fun fields_tr' (t, u) = Syntax.const @{syntax_const "_fields"} $ t $ u;
890 fun record_tr' ctxt t =
892 val thy = Proof_Context.theory_of ctxt;
895 (case strip_comb t of
896 (Const (ext, _), args as (_ :: _)) =>
897 (case try (Lexicon.unmark_const o unsuffix extN) ext of
899 (case get_extfields thy ext' of
902 val (f :: fs, _) = split_last (map fst fields);
903 val fields' = Proof_Context.extern_const ctxt f :: map Long_Name.base_name fs;
904 val (args', more) = split_last args;
905 in (fields' ~~ args') @ strip_fields more end
906 handle ListPair.UnequalLengths => [("", t)])
911 val (fields, (_, more)) = split_last (strip_fields t);
912 val _ = null fields andalso raise Match;
913 val u = foldr1 fields_tr' (map field_tr' fields);
916 Const (@{const_syntax Unity}, _) => Syntax.const @{syntax_const "_record"} $ u
917 | _ => Syntax.const @{syntax_const "_record_scheme"} $ u $ more
922 fun record_ext_tr' name =
924 val ext_name = Lexicon.mark_const (name ^ extN);
925 fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));
926 in (ext_name, tr') end;
933 fun dest_update ctxt c =
934 (case try Lexicon.unmark_const c of
935 SOME d => try (unsuffix updateN) (Proof_Context.extern_const ctxt d)
938 fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
939 (case dest_update ctxt c of
941 (case try Syntax_Trans.const_abs_tr' k of
943 apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
944 (field_updates_tr' ctxt u)
947 | field_updates_tr' _ tm = ([], tm);
949 fun record_update_tr' ctxt tm =
950 (case field_updates_tr' ctxt tm of
951 ([], _) => raise Match
953 Syntax.const @{syntax_const "_record_update"} $ u $
954 foldr1 (fn (v, w) => Syntax.const @{syntax_const "_field_updates"} $ v $ w) (rev ts));
958 fun field_update_tr' name =
960 val update_name = Lexicon.mark_const (name ^ updateN);
961 fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u)
962 | tr' _ _ = raise Match;
963 in (update_name, tr') end;
969 (** record simprocs **)
971 fun future_forward_prf_standard thy prf prop () =
973 if ! quick_and_dirty then Skip_Proof.make_thm thy prop
974 else if Goal.future_enabled () then
975 Goal.future_result (Proof_Context.init_global thy) (Goal.fork prf) prop
977 in Drule.export_without_context thm end;
979 fun prove_common immediate stndrd thy asms prop tac =
982 if ! quick_and_dirty then Skip_Proof.prove
983 else if immediate orelse not (Goal.future_enabled ()) then Goal.prove
984 else Goal.prove_future;
985 val prf = prv (Proof_Context.init_global thy) [] asms prop tac;
986 in if stndrd then Drule.export_without_context prf else prf end;
988 val prove_future_global = prove_common false;
989 val prove_global = prove_common true;
991 fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) =
992 (case get_updates thy u of
993 SOME u_name => u_name = s
994 | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));
997 let val T = range_type (fastype_of f)
998 in HOLogic.mk_comp (Const (@{const_name Fun.id}, T --> T), f) end;
1000 fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
1001 | get_upd_funs _ = [];
1003 fun get_accupd_simps thy term defset =
1005 val (acc, [body]) = strip_comb term;
1006 val upd_funs = sort_distinct Term_Ord.fast_term_ord (get_upd_funs body);
1009 (* FIXME fresh "f" (!?) *)
1010 val T = domain_type (fastype_of upd);
1011 val lhs = HOLogic.mk_comp (acc, upd $ Free ("f", T));
1013 if is_sel_upd_pair thy acc upd
1014 then HOLogic.mk_comp (Free ("f", T), acc)
1015 else mk_comp_id acc;
1016 val prop = lhs === rhs;
1018 Goal.prove (Proof_Context.init_global thy) [] [] prop
1020 simp_tac defset 1 THEN
1021 REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
1022 TRY (simp_tac (HOL_ss addsimps id_o_apps) 1));
1024 if is_sel_upd_pair thy acc upd
1027 in Drule.export_without_context (othm RS dest) end;
1028 in map get_simp upd_funs end;
1030 fun get_updupd_simp thy defset u u' comp =
1032 (* FIXME fresh "f" (!?) *)
1033 val f = Free ("f", domain_type (fastype_of u));
1034 val f' = Free ("f'", domain_type (fastype_of u'));
1035 val lhs = HOLogic.mk_comp (u $ f, u' $ f');
1038 then u $ HOLogic.mk_comp (f, f')
1039 else HOLogic.mk_comp (u' $ f', u $ f);
1040 val prop = lhs === rhs;
1042 Goal.prove (Proof_Context.init_global thy) [] [] prop
1044 simp_tac defset 1 THEN
1045 REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
1046 TRY (simp_tac (HOL_ss addsimps [id_apply]) 1));
1047 val dest = if comp then o_eq_dest_lhs else o_eq_dest;
1048 in Drule.export_without_context (othm RS dest) end;
1050 fun get_updupd_simps thy term defset =
1052 val upd_funs = get_upd_funs term;
1053 val cname = fst o dest_Const;
1054 fun getswap u u' = get_updupd_simp thy defset u u' (cname u = cname u');
1055 fun build_swaps_to_eq _ [] swaps = swaps
1056 | build_swaps_to_eq upd (u :: us) swaps =
1058 val key = (cname u, cname upd);
1060 if Symreltab.defined swaps key then swaps
1061 else Symreltab.insert (K true) (key, getswap u upd) swaps;
1063 if cname u = cname upd then newswaps
1064 else build_swaps_to_eq upd us newswaps
1066 fun swaps_needed [] _ _ swaps = map snd (Symreltab.dest swaps)
1067 | swaps_needed (u :: us) prev seen swaps =
1068 if Symtab.defined seen (cname u)
1069 then swaps_needed us prev seen (build_swaps_to_eq u prev swaps)
1070 else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps;
1071 in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end;
1073 val named_cterm_instantiate = Iso_Tuple_Support.named_cterm_instantiate;
1075 fun prove_unfold_defs thy ex_simps ex_simprs prop =
1077 val defset = get_sel_upd_defs thy;
1078 val prop' = Envir.beta_eta_contract prop;
1079 val (lhs, _) = Logic.dest_equals (Logic.strip_assums_concl prop');
1080 val (_, args) = strip_comb lhs;
1081 val simps = (if length args = 1 then get_accupd_simps else get_updupd_simps) thy lhs defset;
1083 Goal.prove (Proof_Context.init_global thy) [] [] prop'
1085 simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1 THEN
1086 TRY (simp_tac (HOL_basic_ss addsimps ex_simps addsimprocs ex_simprs) 1))
1092 fun eq (s1: string) (s2: string) = (s1 = s2);
1094 fun has_field extfields f T =
1095 exists (fn (eN, _) => exists (eq f o fst) (Symtab.lookup_list extfields eN)) (dest_recTs T);
1097 fun K_skeleton n (T as Type (_, [_, kT])) (b as Bound i) (Abs (x, xT, t)) =
1098 if null (loose_bnos t) then ((n, kT), (Abs (x, xT, Bound (i + 1)))) else ((n, T), b)
1099 | K_skeleton n T b _ = ((n, T), b);
1106 Simplify selections of an record update:
1107 (1) S (S_update k r) = k (S r)
1108 (2) S (X_update k r) = S r
1110 The simproc skips multiple updates at once, eg:
1111 S (X_update x (Y_update y (S_update k r))) = k (S r)
1113 But be careful in (2) because of the extensibility of records.
1114 - If S is a more-selector we have to make sure that the update on component
1115 X does not affect the selected subrecord.
1116 - If X is a more-selector we have to make sure that S is not in the updated
1120 Simplifier.simproc_global @{theory HOL} "record_simp" ["x"]
1121 (fn thy => fn _ => fn t =>
1123 (sel as Const (s, Type (_, [_, rangeS]))) $
1124 ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
1125 if is_selector thy s andalso is_some (get_updates thy u) then
1127 val {sel_upd = {updates, ...}, extfields, ...} = Data.get thy;
1129 fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
1130 (case Symtab.lookup updates u of
1134 (case mk_eq_terms r of
1139 val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
1140 in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end
1141 | SOME (trm, trm', vars) =>
1143 val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k;
1144 in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end)
1145 else if has_field extfields u_name rangeS orelse
1146 has_field extfields s (domain_type kT) then NONE
1148 (case mk_eq_terms r of
1149 SOME (trm, trm', vars) =>
1150 let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k
1151 in SOME (upd $ kb $ trm, trm', kv :: vars) end
1156 val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
1157 in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end))
1158 | mk_eq_terms _ = NONE;
1160 (case mk_eq_terms (upd $ k $ r) of
1161 SOME (trm, trm', vars) =>
1163 (prove_unfold_defs thy [] []
1164 (list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
1170 fun get_upd_acc_cong_thm upd acc thy simpset =
1172 val insts = [("upd", cterm_of thy upd), ("ac", cterm_of thy acc)];
1173 val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv);
1175 Goal.prove (Proof_Context.init_global thy) [] [] prop
1177 simp_tac simpset 1 THEN
1178 REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
1179 TRY (resolve_tac [updacc_cong_idI] 1))
1185 (*Simplify multiple updates:
1186 (1) "N_update y (M_update g (N_update x (M_update f r))) =
1187 (N_update (y o x) (M_update (g o f) r))"
1188 (2) "r(|M:= M r|) = r"
1190 In both cases "more" updates complicate matters: for this reason
1191 we omit considering further updates if doing so would introduce
1192 both a more update and an update to a field within it.*)
1194 Simplifier.simproc_global @{theory HOL} "record_upd_simp" ["x"]
1195 (fn thy => fn _ => fn t =>
1197 (*We can use more-updators with other updators as long
1198 as none of the other updators go deeper than any more
1199 updator. min here is the depth of the deepest other
1200 updator, max the depth of the shallowest more updator.*)
1201 fun include_depth (dep, true) (min, max) =
1203 then SOME (min, if dep <= max orelse max = ~1 then dep else max)
1205 | include_depth (dep, false) (min, max) =
1206 if dep <= max orelse max = ~1
1207 then SOME (if min <= dep then dep else min, max)
1210 fun getupdseq (term as (upd as Const (u, _)) $ f $ tm) min max =
1211 (case get_update_details u thy of
1212 SOME (s, dep, ismore) =>
1213 (case include_depth (dep, ismore) (min, max) of
1214 SOME (min', max') =>
1215 let val (us, bs, _) = getupdseq tm min' max'
1216 in ((upd, s, f) :: us, bs, fastype_of term) end
1217 | NONE => ([], term, HOLogic.unitT))
1218 | NONE => ([], term, HOLogic.unitT))
1219 | getupdseq term _ _ = ([], term, HOLogic.unitT);
1221 val (upds, base, baseT) = getupdseq t 0 ~1;
1223 fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm =
1224 if s = s' andalso null (loose_bnos tm')
1225 andalso subst_bound (HOLogic.unit, tm') = tm
1226 then (true, Abs (n, T, Const (s', T') $ Bound 1))
1227 else (false, HOLogic.unit)
1228 | is_upd_noop _ _ _ = (false, HOLogic.unit);
1230 fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) =
1232 val ss = get_sel_upd_defs thy;
1233 val uathm = get_upd_acc_cong_thm upd acc thy ss;
1235 [Drule.export_without_context (uathm RS updacc_noopE),
1236 Drule.export_without_context (uathm RS updacc_noop_compE)]
1239 (*If f is constant then (f o g) = f. We know that K_skeleton
1240 only returns constant abstractions thus when we see an
1241 abstraction we can discard inner updates.*)
1242 fun add_upd (f as Abs _) fs = [f]
1243 | add_upd f fs = (f :: fs);
1245 (*mk_updterm returns
1246 (orig-term-skeleton, simplified-skeleton,
1247 variables, duplicate-updates, simp-flag, noop-simps)
1249 where duplicate-updates is a table used to pass upward
1250 the list of update functions which can be composed
1251 into an update above them, simp-flag indicates whether
1252 any simplification was achieved, and noop-simps are
1253 used for eliminating case (2) defined above*)
1254 fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term =
1256 val (lhs, rhs, vars, dups, simp, noops) =
1257 mk_updterm upds (Symtab.update (u, ()) above) term;
1259 K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f;
1260 val (isnoop, skelf') = is_upd_noop s f term;
1261 val funT = domain_type T;
1262 fun mk_comp_local (f, f') =
1263 Const (@{const_name Fun.comp}, funT --> funT --> funT) $ f $ f';
1266 (upd $ skelf' $ lhs, rhs, vars,
1267 Symtab.update (u, []) dups, true,
1268 if Symtab.defined noops u then noops
1269 else Symtab.update (u, get_noop_simps upd skelf') noops)
1270 else if Symtab.defined above u then
1271 (upd $ skelf $ lhs, rhs, fvar :: vars,
1272 Symtab.map_default (u, []) (add_upd skelf) dups,
1275 (case Symtab.lookup dups u of
1278 upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs,
1279 fvar :: vars, dups, true, noops)
1280 | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops))
1282 | mk_updterm [] _ _ =
1283 (Bound 0, Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty)
1284 | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _) => x) us);
1286 val (lhs, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
1287 val noops' = maps snd (Symtab.dest noops);
1291 (prove_unfold_defs thy noops' [simproc]
1292 (list_all (vars, Logic.mk_equals (lhs, rhs))))
1301 (*Look up the most specific record-equality.
1304 Testing equality of records boils down to the test of equality of all components.
1305 Therefore the complexity is: #components * complexity for single component.
1306 Especially if a record has a lot of components it may be better to split up
1307 the record first and do simplification on that (split_simp_tac).
1308 e.g. r(|lots of updates|) = x
1310 eq_simproc split_simp_tac
1311 Complexity: #components * #updates #updates
1314 Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
1315 (fn thy => fn _ => fn t =>
1316 (case t of Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ =>
1317 (case rec_id ~1 T of
1320 (case get_equalities thy name of
1322 | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
1328 (*Split quantified occurrences of records, for which P holds. P can peek on the
1329 subterm starting at the quantified occurrence of the record (including the quantifier):
1330 P t = 0: do not split
1331 P t = ~1: completely split
1332 P t > 0: split up to given bound of record extensions.*)
1333 fun split_simproc P =
1334 Simplifier.simproc_global @{theory HOL} "record_split_simp" ["x"]
1335 (fn thy => fn _ => fn t =>
1337 Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
1338 if quantifier = @{const_name all} orelse
1339 quantifier = @{const_name All} orelse
1340 quantifier = @{const_name Ex}
1342 (case rec_id ~1 T of
1345 let val split = P t in
1347 (case get_splits thy (rec_id split T) of
1349 | SOME (all_thm, All_thm, Ex_thm, _) =>
1352 @{const_name all} => all_thm
1353 | @{const_name All} => All_thm RS eq_reflection
1354 | @{const_name Ex} => Ex_thm RS eq_reflection
1355 | _ => raise Fail "split_simproc"))
1361 val ex_sel_eq_simproc =
1362 Simplifier.simproc_global @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
1363 (fn thy => fn ss => fn t =>
1366 prove_global true thy [] prop
1367 (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
1368 addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1);
1370 fun mkeq (lr, Teq, (sel, Tsel), x) i =
1371 if is_selector thy sel then
1374 if not (loose_bvar1 (x, 0))
1375 then Free ("x" ^ string_of_int i, range_type Tsel)
1376 else raise TERM ("", [x]);
1377 val sel' = Const (sel, Tsel) $ Bound 0;
1378 val (l, r) = if lr then (sel', x') else (x', sel');
1379 in Const (@{const_name HOL.eq}, Teq) $ l $ r end
1380 else raise TERM ("", [Const (sel, Tsel)]);
1382 fun dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
1383 (true, Teq, (sel, Tsel), X)
1384 | dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
1385 (false, Teq, (sel, Tsel), X)
1386 | dest_sel_eq _ = raise TERM ("", []);
1389 Const (@{const_name Ex}, Tex) $ Abs (s, T, t) =>
1391 val eq = mkeq (dest_sel_eq t) 0;
1393 list_all ([("r", T)],
1395 (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), HOLogic.true_const));
1396 in SOME (prove prop) end
1397 handle TERM _ => NONE)
1402 (* split_simp_tac *)
1404 (*Split (and simplify) all records in the goal for which P holds.
1405 For quantified occurrences of a record
1406 P can peek on the whole subterm (including the quantifier); for free variables P
1407 can only peek on the variable itself.
1408 P t = 0: do not split
1409 P t = ~1: completely split
1410 P t > 0: split up to given bound of record extensions.*)
1411 fun split_simp_tac thms P = CSUBGOAL (fn (cgoal, i) =>
1413 val thy = Thm.theory_of_cterm cgoal;
1415 val goal = term_of cgoal;
1416 val frees = filter (is_recT o #2) (Term.add_frees goal []);
1418 val has_rec = exists_Const
1419 (fn (s, Type (_, [Type (_, [T, _]), _])) =>
1420 (s = @{const_name all} orelse s = @{const_name All} orelse s = @{const_name Ex}) andalso
1424 fun mk_split_free_tac free induct_thm i =
1426 val cfree = cterm_of thy free;
1427 val _$ (_ $ r) = concl_of induct_thm;
1428 val crec = cterm_of thy r;
1429 val thm = cterm_instantiate [(crec, cfree)] induct_thm;
1431 simp_tac (HOL_basic_ss addsimps @{thms induct_atomize}) i THEN
1433 simp_tac (HOL_basic_ss addsimps @{thms induct_rulify}) i
1436 val split_frees_tacs =
1437 frees |> map_filter (fn (x, T) =>
1438 (case rec_id ~1 T of
1442 val free = Free (x, T);
1446 (case get_splits thy (rec_id split T) of
1448 | SOME (_, _, _, induct_thm) =>
1449 SOME (mk_split_free_tac free induct_thm i))
1453 val simprocs = if has_rec goal then [split_simproc P] else [];
1454 val thms' = K_comp_convs @ thms;
1456 EVERY split_frees_tacs THEN
1457 Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i
1463 (*Split all records in the goal, which are quantified by !! or ALL.*)
1464 val split_tac = CSUBGOAL (fn (cgoal, i) =>
1466 val goal = term_of cgoal;
1468 val has_rec = exists_Const
1469 (fn (s, Type (_, [Type (_, [T, _]), _])) =>
1470 (s = @{const_name all} orelse s = @{const_name All}) andalso is_recT T
1473 fun is_all (Const (@{const_name all}, _) $ _) = ~1
1474 | is_all (Const (@{const_name All}, _) $ _) = ~1
1477 if has_rec goal then
1478 Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [split_simproc is_all]) i
1485 val split_name = "record_split_tac";
1486 val split_wrapper = (split_name, fn _ => fn tac => split_tac ORELSE' tac);
1490 (** theory extender interface **)
1492 (* prepare arguments *)
1494 fun read_typ ctxt raw_T env =
1496 val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
1497 val T = Syntax.read_typ ctxt' raw_T;
1498 val env' = Misc_Legacy.add_typ_tfrees (T, env);
1501 fun cert_typ ctxt raw_T env =
1503 val thy = Proof_Context.theory_of ctxt;
1504 val T = Type.no_tvars (Sign.certify_typ thy raw_T)
1505 handle TYPE (msg, _, _) => error msg;
1506 val env' = Misc_Legacy.add_typ_tfrees (T, env);
1512 fun case_names_fields x = Rule_Cases.case_names ["fields"] x;
1513 fun induct_type_global name = [case_names_fields, Induct.induct_type name];
1514 fun cases_type_global name = [case_names_fields, Induct.cases_type name];
1519 fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));
1521 (*Do case analysis / induction according to rule on last parameter of ith subgoal
1522 (or on s if there are no parameters).
1523 Instatiation of record variable (and predicate) in rule is calculated to
1524 avoid problems with higher order unification.*)
1525 fun try_param_tac s rule = CSUBGOAL (fn (cgoal, i) =>
1527 val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
1529 val g = Thm.term_of cgoal;
1530 val params = Logic.strip_params g;
1531 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
1532 val rule' = Thm.lift_rule cgoal rule;
1533 val (P, ys) = strip_comb (HOLogic.dest_Trueprop
1534 (Logic.strip_assums_concl (prop_of rule')));
1535 (*ca indicates if rule is a case analysis or induction rule*)
1537 (case rev (drop (length params) ys) of
1538 [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
1539 (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
1540 | [x] => (head_of x, false));
1543 (map (pairself cert)
1546 (case AList.lookup (op =) (Term.add_frees g []) s of
1547 NONE => error "try_param_tac: no such variable"
1548 | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
1550 [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
1551 (x, list_abs (params, Bound 0))])) rule';
1552 in compose_tac (false, rule'', nprems_of rule) i end);
1555 fun extension_definition name fields alphas zeta moreT more vars thy =
1557 val ctxt = Proof_Context.init_global thy;
1559 val base_name = Long_Name.base_name name;
1561 val fieldTs = map snd fields;
1562 val fields_moreTs = fieldTs @ [moreT];
1564 val alphas_zeta = alphas @ [zeta];
1566 val ext_binding = Binding.name (suffix extN base_name);
1567 val ext_name = suffix extN name;
1568 val ext_tyco = suffix ext_typeN name
1569 val extT = Type (ext_tyco, map TFree alphas_zeta);
1570 val ext_type = fields_moreTs ---> extT;
1573 (* the tree of new types that will back the record extension *)
1575 val mktreeV = Balanced_Tree.make Iso_Tuple_Support.mk_cons_tuple;
1577 fun mk_iso_tuple (left, right) (thy, i) =
1579 val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
1580 val ((_, cons), thy') = thy
1581 |> Iso_Tuple_Support.add_iso_tuple_type
1582 (Binding.suffix_name suff (Binding.name base_name), alphas_zeta)
1583 (fastype_of left, fastype_of right);
1585 (cons $ left $ right, (thy', i + 1))
1588 (*trying to create a 1-element iso_tuple will fail, and is pointless anyway*)
1589 fun mk_even_iso_tuple [arg] = pair arg
1590 | mk_even_iso_tuple args = mk_iso_tuple (Iso_Tuple_Support.dest_cons_tuple (mktreeV args));
1592 fun build_meta_tree_type i thy vars more =
1593 let val len = length vars in
1594 if len < 1 then raise TYPE ("meta_tree_type args too short", [], vars)
1595 else if len > 16 then
1598 | group16 xs = take 16 xs :: group16 (drop 16 xs);
1599 val vars' = group16 vars;
1600 val (composites, (thy', i')) = fold_map mk_even_iso_tuple vars' (thy, i);
1602 build_meta_tree_type i' thy' composites more
1605 let val (term, (thy', _)) = mk_iso_tuple (mktreeV vars, more) (thy, 0)
1609 val _ = timing_msg ctxt "record extension preparing definitions";
1612 (* 1st stage part 1: introduce the tree of new types *)
1614 fun get_meta_tree () = build_meta_tree_type 1 thy vars more;
1615 val (ext_body, typ_thy) =
1616 timeit_msg ctxt "record extension nested type def:" get_meta_tree;
1619 (* prepare declarations and definitions *)
1621 (* 1st stage part 2: define the ext constant *)
1623 fun mk_ext args = list_comb (Const (ext_name, ext_type), args);
1624 val ext_spec = Logic.mk_equals (mk_ext (vars @ [more]), ext_body);
1628 |> Sign.declare_const_global ((ext_binding, ext_type), NoSyn) |> snd
1629 |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]
1630 ||> Theory.checkpoint
1631 val ([ext_def], defs_thy) =
1632 timeit_msg ctxt "record extension constructor def:" mk_defs;
1635 (* prepare propositions *)
1637 val _ = timing_msg ctxt "record extension preparing propositions";
1638 val vars_more = vars @ [more];
1639 val variants = map (fn Free (x, _) => x) vars_more;
1640 val ext = mk_ext vars_more;
1641 val s = Free (rN, extT);
1642 val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT);
1644 val inject_prop = (* FIXME local x x' *)
1645 let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
1646 HOLogic.mk_conj (HOLogic.eq_const extT $
1647 mk_ext vars_more $ mk_ext vars_more', HOLogic.true_const)
1649 foldr1 HOLogic.mk_conj
1650 (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [HOLogic.true_const])
1654 (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
1656 val split_meta_prop = (* FIXME local P *)
1657 let val P = Free (singleton (Name.variant_list variants) "P", extT --> Term.propT) in
1659 (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
1662 val prove_standard = prove_future_global true defs_thy;
1666 (prove_standard [] inject_prop
1668 simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
1670 (rtac refl_conj_eq 1 ORELSE
1671 Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
1674 val inject = timeit_msg ctxt "record extension inject proof:" inject_prf;
1676 (*We need a surjection property r = (| f = f r, g = g r ... |)
1677 to prove other theorems. We haven't given names to the accessors
1678 f, g etc yet however, so we generate an ext structure with
1679 free variables as all arguments and allow the introduction tactic to
1680 operate on it as far as it can. We then use Drule.export_without_context
1681 to convert the free variables into unifiable variables and unify them with
1682 (roughly) the definition of the accessor.*)
1683 fun surject_prf () =
1685 val cterm_ext = cterm_of defs_thy ext;
1686 val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
1688 simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
1689 REPEAT_ALL_NEW Iso_Tuple_Support.iso_tuple_intros_tac 1;
1690 val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
1691 val [halfway] = Seq.list_of (tactic1 start);
1692 val [surject] = Seq.list_of (tactic2 (Drule.export_without_context halfway));
1696 val surject = timeit_msg ctxt "record extension surjective proof:" surject_prf;
1698 fun split_meta_prf () =
1699 prove_standard [] split_meta_prop
1702 [rtac equal_intr_rule, Goal.norm_hhf_tac,
1703 etac meta_allE, atac,
1704 rtac (prop_subst OF [surject]),
1705 REPEAT o etac meta_allE, atac]);
1706 val split_meta = timeit_msg ctxt "record extension split_meta proof:" split_meta_prf;
1709 let val (assm, concl) = induct_prop in
1710 prove_standard [assm] concl
1712 cut_rules_tac [split_meta RS Drule.equal_elim_rule2] 1 THEN
1713 resolve_tac prems 2 THEN
1714 asm_simp_tac HOL_ss 1)
1716 val induct = timeit_msg ctxt "record extension induct proof:" induct_prf;
1718 val ([induct', inject', surjective', split_meta'], thm_thy) =
1720 |> Global_Theory.add_thms (map (Thm.no_attributes o apfst Binding.name)
1721 [("ext_induct", induct),
1722 ("ext_inject", inject),
1723 ("ext_surjective", surject),
1724 ("ext_split", split_meta)]);
1727 (((ext_name, ext_type), (ext_tyco, alphas_zeta),
1728 extT, induct', inject', surjective', split_meta', ext_def), thm_thy)
1731 fun chunks [] [] = []
1732 | chunks [] xs = [xs]
1733 | chunks (l :: ls) xs = take l xs :: chunks ls (drop l xs);
1735 fun chop_last [] = error "chop_last: list should not be empty"
1736 | chop_last [x] = ([], x)
1737 | chop_last (x :: xs) = let val (tl, l) = chop_last xs in (x :: tl, l) end;
1739 fun subst_last _ [] = error "subst_last: list should not be empty"
1740 | subst_last s [_] = [s]
1741 | subst_last s (x :: xs) = x :: subst_last s xs;
1746 (*build up the record type from the current extension tpye extT and a list
1747 of parent extensions, starting with the root of the record hierarchy*)
1748 fun mk_recordT extT =
1749 fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT;
1752 fun obj_to_meta_all thm =
1754 fun E thm = (* FIXME proper name *)
1755 (case SOME (spec OF [thm]) handle THM _ => NONE of
1759 val th2 = Drule.forall_intr_vars th1;
1762 fun meta_to_obj_all thm =
1764 val thy = Thm.theory_of_thm thm;
1765 val prop = Thm.prop_of thm;
1766 val params = Logic.strip_params prop;
1767 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop);
1768 val ct = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.list_all (params, concl)));
1769 val thm' = Seq.hd (REPEAT (rtac allI 1) (Thm.trivial ct));
1770 in Thm.implies_elim thm' thm end;
1773 (* code generation *)
1775 fun mk_random_eq tyco vs extN Ts =
1777 (* FIXME local i etc. *)
1778 val size = @{term "i::code_numeral"};
1779 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
1780 val T = Type (tyco, map TFree vs);
1781 val Tm = termifyT T;
1782 val params = Name.invent_names Name.context "x" Ts;
1783 val lhs = HOLogic.mk_random T size;
1784 val tc = HOLogic.mk_return Tm @{typ Random.seed}
1785 (HOLogic.mk_valtermify_app extN params T);
1789 ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params)
1790 tc @{typ Random.seed} (SOME Tm, @{typ Random.seed});
1795 fun mk_full_exhaustive_eq tyco vs extN Ts =
1797 (* FIXME local i etc. *)
1798 val size = @{term "i::code_numeral"};
1799 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
1800 val T = Type (tyco, map TFree vs);
1801 val test_function = Free ("f", termifyT T --> @{typ "term list option"});
1802 val params = Name.invent_names Name.context "x" Ts;
1803 fun full_exhaustiveT T =
1804 (termifyT T --> @{typ "Code_Evaluation.term list option"}) -->
1805 @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"};
1806 fun mk_full_exhaustive T =
1807 Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
1808 full_exhaustiveT T);
1809 val lhs = mk_full_exhaustive T $ test_function $ size;
1810 val tc = test_function $ (HOLogic.mk_valtermify_app extN params T);
1811 val rhs = fold_rev (fn (v, T) => fn cont =>
1812 mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc;
1817 fun instantiate_sort_record (sort, mk_eq) tyco vs extN Ts thy =
1819 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_eq tyco vs extN Ts));
1822 |> Class.instantiation ([tyco], vs, sort)
1823 |> `(fn lthy => Syntax.check_term lthy eq)
1824 |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
1826 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
1829 fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy =
1831 val algebra = Sign.classes_of thy;
1832 val has_inst = can (Sorts.mg_domain algebra ext_tyco) sort;
1834 if has_inst then thy
1836 (case Quickcheck_Common.perhaps_constrain thy (map (rpair sort) Ts) vs of
1838 instantiate_sort_record (sort, mk_eq) ext_tyco (map constrain vs) extN
1839 ((map o map_atyps) (fn TFree v => TFree (constrain v)) Ts) thy
1843 fun add_code ext_tyco vs extT ext simps inject thy =
1846 (HOLogic.mk_Trueprop o HOLogic.mk_eq)
1847 (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
1848 Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT));
1850 Class.intro_classes_tac []
1851 THEN (Simplifier.rewrite_goals_tac [Simpdata.mk_eq eq_def])
1852 THEN ALLGOALS (rtac @{thm refl});
1853 fun mk_eq thy eq_def = Simplifier.rewrite_rule
1854 [(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject;
1855 fun mk_eq_refl thy =
1858 ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
1859 |> AxClass.unoverload thy;
1860 val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
1861 val ensure_exhaustive_record =
1862 ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
1865 |> Code.add_datatype [ext]
1866 |> fold Code.add_default_eqn simps
1867 |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
1868 |> `(fn lthy => Syntax.check_term lthy eq)
1869 |-> (fn eq => Specification.definition
1870 (NONE, (Attrib.empty_binding, eq)))
1871 |-> (fn (_, (_, eq_def)) =>
1872 Class.prove_instantiation_exit_result Morphism.thm
1873 (fn _ => fn eq_def => tac eq_def) eq_def)
1874 |-> (fn eq_def => fn thy =>
1875 thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
1876 |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
1877 |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
1878 |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
1884 fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
1886 val ctxt = Proof_Context.init_global thy;
1888 val prefix = Binding.name_of binding;
1889 val name = Sign.full_name thy binding;
1890 val full = Sign.full_name_path thy prefix;
1892 val bfields = map (fn (x, T, _) => (x, T)) raw_fields;
1893 val field_syntax = map #3 raw_fields;
1895 val parent_fields = maps #fields parents;
1896 val parent_chunks = map (length o #fields) parents;
1897 val parent_names = map fst parent_fields;
1898 val parent_types = map snd parent_fields;
1899 val parent_fields_len = length parent_fields;
1900 val parent_variants =
1901 Name.variant_list [moreN, rN, rN ^ "'", wN] (map Long_Name.base_name parent_names);
1902 val parent_vars = map2 (curry Free) parent_variants parent_types;
1903 val parent_len = length parents;
1905 val fields = map (apfst full) bfields;
1906 val names = map fst fields;
1907 val types = map snd fields;
1908 val alphas_fields = fold Term.add_tfreesT types [];
1909 val alphas_ext = inter (op =) alphas_fields alphas;
1910 val len = length fields;
1912 Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
1913 (map (Binding.name_of o fst) bfields);
1914 val vars = map2 (curry Free) variants types;
1915 val named_vars = names ~~ vars;
1916 val idxms = 0 upto len;
1918 val all_fields = parent_fields @ fields;
1919 val all_types = parent_types @ types;
1920 val all_variants = parent_variants @ variants;
1921 val all_vars = parent_vars @ vars;
1922 val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
1924 val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", HOLogic.typeS);
1925 val moreT = TFree zeta;
1926 val more = Free (moreN, moreT);
1927 val full_moreN = full (Binding.name moreN);
1928 val bfields_more = bfields @ [(Binding.name moreN, moreT)];
1929 val fields_more = fields @ [(full_moreN, moreT)];
1930 val named_vars_more = named_vars @ [(full_moreN, more)];
1931 val all_vars_more = all_vars @ [more];
1932 val all_named_vars_more = all_named_vars @ [(full_moreN, more)];
1935 (* 1st stage: ext_thy *)
1937 val extension_name = full binding;
1939 val ((ext, (ext_tyco, vs),
1940 extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
1942 |> Sign.qualified_path false binding
1943 |> extension_definition extension_name fields alphas_ext zeta moreT more vars;
1945 val _ = timing_msg ctxt "record preparing definitions";
1946 val Type extension_scheme = extT;
1947 val extension_name = unsuffix ext_typeN (fst extension_scheme);
1948 val extension = let val (n, Ts) = extension_scheme in (n, subst_last HOLogic.unitT Ts) end;
1949 val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extension_name];
1950 val extension_id = implode extension_names;
1952 fun rec_schemeT n = mk_recordT (map #extension (drop n parents)) extT;
1953 val rec_schemeT0 = rec_schemeT 0;
1956 let val (c, Ts) = extension in
1957 mk_recordT (map #extension (drop n parents))
1958 (Type (c, subst_last HOLogic.unitT Ts))
1964 val (args', more) = chop_last args;
1965 fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]);
1967 fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args')) more;
1969 if more = HOLogic.unit
1970 then build (map_range recT (parent_len + 1))
1971 else build (map_range rec_schemeT (parent_len + 1))
1974 val r_rec0 = mk_rec all_vars_more 0;
1975 val r_rec_unit0 = mk_rec (all_vars @ [HOLogic.unit]) 0;
1977 fun r n = Free (rN, rec_schemeT n);
1979 fun r_unit n = Free (rN, recT n);
1980 val r_unit0 = r_unit 0;
1981 val w = Free (wN, rec_schemeT 0);
1984 (* print translations *)
1986 val record_ext_type_abbr_tr's =
1988 val trname = hd extension_names;
1989 val last_ext = unsuffix ext_typeN (fst extension);
1990 in [record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0 trname] end;
1992 val record_ext_type_tr's =
1994 (*avoid conflict with record_type_abbr_tr's*)
1995 val trnames = if parent_len > 0 then [extension_name] else [];
1996 in map record_ext_type_tr' trnames end;
1998 val advanced_print_translation =
1999 map field_update_tr' (full_moreN :: names) @ [record_ext_tr' extension_name] @
2000 record_ext_type_tr's @ record_ext_type_abbr_tr's;
2003 (* prepare declarations *)
2005 val sel_decls = map (mk_selC rec_schemeT0 o apfst Binding.name_of) bfields_more;
2006 val upd_decls = map (mk_updC updateN rec_schemeT0 o apfst Binding.name_of) bfields_more;
2007 val make_decl = (makeN, all_types ---> recT0);
2008 val fields_decl = (fields_selN, types ---> Type extension);
2009 val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0);
2010 val truncate_decl = (truncateN, rec_schemeT0 --> recT0);
2013 (* prepare definitions *)
2015 val ext_defs = ext_def :: map #ext_def parents;
2017 (*Theorems from the iso_tuple intros.
2018 By unfolding ext_defs from r_rec0 we create a tree of constructor
2019 calls (many of them Pair, but others as well). The introduction
2020 rules for update_accessor_eq_assist can unify two different ways
2021 on these constructors. If we take the complete result sequence of
2022 running a the introduction tactic, we get one theorem for each upd/acc
2023 pair, from which we can derive the bodies of our selector and
2024 updator and their convs.*)
2025 fun get_access_update_thms () =
2029 (*pick variable indices of 1 to avoid possible variable
2030 collisions with existing variables in updacc_eq_triv*)
2031 fun to_Var (Free (c, T)) = Var ((c, 1), T);
2032 in mk_rec (map to_Var all_vars_more) 0 end;
2034 val cterm_rec = cterm_of ext_thy r_rec0;
2035 val cterm_vrs = cterm_of ext_thy r_rec0_Vars;
2036 val insts = [("v", cterm_rec), ("v'", cterm_vrs)];
2037 val init_thm = named_cterm_instantiate insts updacc_eq_triv;
2038 val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
2040 simp_tac (HOL_basic_ss addsimps ext_defs) 1 THEN
2041 REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE terminal);
2042 val updaccs = Seq.list_of (tactic init_thm);
2044 (updaccs RL [updacc_accessor_eqE],
2045 updaccs RL [updacc_updator_eqE],
2046 updaccs RL [updacc_cong_from_eq])
2048 val (accessor_thms, updator_thms, upd_acc_cong_assists) =
2049 timeit_msg ctxt "record getting tree access/updates:" get_access_update_thms;
2051 fun lastN xs = drop parent_fields_len xs;
2054 fun mk_sel_spec ((c, T), thm) =
2056 val (acc $ arg, _) =
2057 HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (Thm.concl_of thm)));
2059 if arg aconv r_rec0 then ()
2060 else raise TERM ("mk_sel_spec: different arg", [arg]);
2062 Const (mk_selC rec_schemeT0 (c, T)) :== acc
2064 val sel_specs = map mk_sel_spec (fields_more ~~ lastN accessor_thms);
2067 fun mk_upd_spec ((c, T), thm) =
2069 val (upd $ _ $ arg, _) =
2070 HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (Thm.concl_of thm)));
2072 if arg aconv r_rec0 then ()
2073 else raise TERM ("mk_sel_spec: different arg", [arg]);
2074 in Const (mk_updC updateN rec_schemeT0 (c, T)) :== upd end;
2075 val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms);
2077 (*derived operations*)
2079 list_comb (Const (full (Binding.name makeN), all_types ---> recT0), all_vars) :==
2080 mk_rec (all_vars @ [HOLogic.unit]) 0;
2082 list_comb (Const (full (Binding.name fields_selN), types ---> Type extension), vars) :==
2083 mk_rec (all_vars @ [HOLogic.unit]) parent_len;
2085 Const (full (Binding.name extendN), recT0 --> moreT --> rec_schemeT0) $ r_unit0 $ more :==
2086 mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
2088 Const (full (Binding.name truncateN), rec_schemeT0 --> recT0) $ r0 :==
2089 mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
2092 (* 2st stage: defs_thy *)
2096 |> Sign.add_advanced_trfuns ([], [], advanced_print_translation, [])
2097 |> Sign.restore_naming thy
2098 |> Typedecl.abbrev_global (binding, map #1 alphas, NoSyn) recT0 |> snd
2099 |> Typedecl.abbrev_global
2100 (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0 |> snd
2101 |> Sign.qualified_path false binding
2102 |> fold (fn ((x, T), mx) => snd o Sign.declare_const_global ((Binding.name x, T), mx))
2103 (sel_decls ~~ (field_syntax @ [NoSyn]))
2104 |> fold (fn (x, T) => snd o Sign.declare_const_global ((Binding.name x, T), NoSyn))
2105 (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
2106 |> (Global_Theory.add_defs false o
2107 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) sel_specs
2108 ||>> (Global_Theory.add_defs false o
2109 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) upd_specs
2110 ||>> (Global_Theory.add_defs false o
2111 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
2112 [make_spec, fields_spec, extend_spec, truncate_spec]
2113 ||> Theory.checkpoint
2114 val (((sel_defs, upd_defs), derived_defs), defs_thy) =
2115 timeit_msg ctxt "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
2118 (* prepare propositions *)
2119 val _ = timing_msg ctxt "record preparing propositions";
2120 val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> HOLogic.boolT);
2121 val C = Free (singleton (Name.variant_list all_variants) "C", HOLogic.boolT);
2122 val P_unit = Free (singleton (Name.variant_list all_variants) "P", recT0 --> HOLogic.boolT);
2125 val sel_conv_props =
2126 map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more;
2129 fun mk_upd_prop i (c, T) =
2132 Free (singleton (Name.variant_list all_variants) (Long_Name.base_name c ^ "'"), T --> T);
2133 val n = parent_fields_len + i;
2134 val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more;
2135 in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
2136 val upd_conv_props = map2 mk_upd_prop idxms fields_more;
2139 val induct_scheme_prop =
2140 All (map dest_Free all_vars_more) (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0);
2142 (All (map dest_Free all_vars) (Trueprop (P_unit $ r_rec_unit0)),
2143 Trueprop (P_unit $ r_unit0));
2146 val surjective_prop =
2147 let val args = map (fn (c, Free (_, T)) => mk_sel r0 (c, T)) all_named_vars_more
2148 in r0 === mk_rec args 0 end;
2151 val cases_scheme_prop =
2152 (All (map dest_Free all_vars_more) ((r0 === r_rec0) ==> Trueprop C))
2156 (All (map dest_Free all_vars) ((r_unit0 === r_rec_unit0) ==> Trueprop C))
2160 val split_meta_prop =
2162 val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0-->Term.propT);
2165 (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
2168 val split_object_prop =
2169 let val ALL = fold_rev (fn (v, T) => fn t => HOLogic.mk_all (v, T, t))
2170 in ALL [dest_Free r0] (P $ r0) === ALL (map dest_Free all_vars_more) (P $ r_rec0) end;
2173 let val EX = fold_rev (fn (v, T) => fn t => HOLogic.mk_exists (v, T, t))
2174 in EX [dest_Free r0] (P $ r0) === EX (map dest_Free all_vars_more) (P $ r_rec0) end;
2179 val s' = Free (rN ^ "'", rec_schemeT0);
2180 fun mk_sel_eq (c, Free (_, T)) = mk_sel r0 (c, T) === mk_sel s' (c, T);
2181 val seleqs = map mk_sel_eq all_named_vars_more;
2182 in All (map dest_Free [r0, s']) (Logic.list_implies (seleqs, r0 === s')) end;
2185 (* 3rd stage: thms_thy *)
2187 fun prove stndrd = prove_future_global stndrd defs_thy;
2188 val prove_standard = prove_future_global true defs_thy;
2189 val future_forward_prf = future_forward_prf_standard defs_thy;
2191 fun prove_simp stndrd ss simps =
2192 let val tac = simp_all_tac ss simps
2193 in fn prop => prove stndrd [] prop (K tac) end;
2195 val ss = get_simpset defs_thy;
2197 fun sel_convs_prf () =
2198 map (prove_simp false ss (sel_defs @ accessor_thms)) sel_conv_props;
2199 val sel_convs = timeit_msg ctxt "record sel_convs proof:" sel_convs_prf;
2200 fun sel_convs_standard_prf () = map Drule.export_without_context sel_convs;
2201 val sel_convs_standard =
2202 timeit_msg ctxt "record sel_convs_standard proof:" sel_convs_standard_prf;
2204 fun upd_convs_prf () =
2205 map (prove_simp false ss (upd_defs @ updator_thms)) upd_conv_props;
2206 val upd_convs = timeit_msg ctxt "record upd_convs proof:" upd_convs_prf;
2207 fun upd_convs_standard_prf () = map Drule.export_without_context upd_convs;
2208 val upd_convs_standard =
2209 timeit_msg ctxt "record upd_convs_standard proof:" upd_convs_standard_prf;
2211 fun get_upd_acc_congs () =
2213 val symdefs = map Thm.symmetric (sel_defs @ upd_defs);
2214 val fold_ss = HOL_basic_ss addsimps symdefs;
2215 val ua_congs = map (Drule.export_without_context o simplify fold_ss) upd_acc_cong_assists;
2216 in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
2217 val (fold_congs, unfold_congs) =
2218 timeit_msg ctxt "record upd fold/unfold congs:" get_upd_acc_congs;
2220 val parent_induct = Option.map #induct_scheme (try List.last parents);
2222 fun induct_scheme_prf () =
2223 prove_standard [] induct_scheme_prop
2226 [case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
2227 try_param_tac rN ext_induct 1,
2228 asm_simp_tac HOL_basic_ss 1]);
2229 val induct_scheme = timeit_msg ctxt "record induct_scheme proof:" induct_scheme_prf;
2232 let val (assm, concl) = induct_prop in
2233 prove_standard [assm] concl (fn {prems, ...} =>
2234 try_param_tac rN induct_scheme 1
2235 THEN try_param_tac "more" @{thm unit.induct} 1
2236 THEN resolve_tac prems 1)
2238 val induct = timeit_msg ctxt "record induct proof:" induct_prf;
2240 fun cases_scheme_prf () =
2242 val _ $ (Pvar $ _) = concl_of induct_scheme;
2245 [(cterm_of defs_thy Pvar, cterm_of defs_thy
2246 (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
2248 in Object_Logic.rulify (mp OF [ind, refl]) end;
2250 val cases_scheme_prf = future_forward_prf cases_scheme_prf cases_scheme_prop;
2251 val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" cases_scheme_prf;
2254 prove_standard [] cases_prop
2256 try_param_tac rN cases_scheme 1 THEN
2257 simp_all_tac HOL_basic_ss [@{thm unit_all_eq1}]);
2258 val cases = timeit_msg ctxt "record cases proof:" cases_prf;
2260 fun surjective_prf () =
2262 val leaf_ss = get_sel_upd_defs defs_thy addsimps (sel_defs @ (o_assoc :: id_o_apps));
2263 val init_ss = HOL_basic_ss addsimps ext_defs;
2265 prove_standard [] surjective_prop
2268 [rtac surject_assist_idE 1,
2271 (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
2272 (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
2274 val surjective = timeit_msg ctxt "record surjective proof:" surjective_prf;
2276 fun split_meta_prf () =
2277 prove false [] split_meta_prop
2280 [rtac equal_intr_rule, Goal.norm_hhf_tac,
2281 etac meta_allE, atac,
2282 rtac (prop_subst OF [surjective]),
2283 REPEAT o etac meta_allE, atac]);
2284 val split_meta = timeit_msg ctxt "record split_meta proof:" split_meta_prf;
2285 fun split_meta_standardise () = Drule.export_without_context split_meta;
2286 val split_meta_standard =
2287 timeit_msg ctxt "record split_meta standard:" split_meta_standardise;
2289 fun split_object_prf () =
2291 val cPI= cterm_of defs_thy (lambda r0 (Trueprop (P $ r0)));
2292 val _ $ Abs (_, _, P $ _) = fst (Logic.dest_equals (concl_of split_meta_standard));
2293 val cP = cterm_of defs_thy P;
2294 val split_meta' = cterm_instantiate [(cP, cPI)] split_meta_standard;
2295 val (l, r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop);
2296 val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l);
2297 val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r);
2299 Thm.assume cl (*All r. P r*) (* 1 *)
2300 |> obj_to_meta_all (*!!r. P r*)
2301 |> Thm.equal_elim split_meta' (*!!n m more. P (ext n m more)*)
2302 |> meta_to_obj_all (*All n m more. P (ext n m more)*) (* 2*)
2303 |> Thm.implies_intr cl (* 1 ==> 2 *)
2305 Thm.assume cr (*All n m more. P (ext n m more)*)
2306 |> obj_to_meta_all (*!!n m more. P (ext n m more)*)
2307 |> Thm.equal_elim (Thm.symmetric split_meta') (*!!r. P r*)
2308 |> meta_to_obj_all (*All r. P r*)
2309 |> Thm.implies_intr cr (* 2 ==> 1 *)
2310 in thr COMP (thl COMP iffI) end;
2313 val split_object_prf = future_forward_prf split_object_prf split_object_prop;
2314 val split_object = timeit_msg ctxt "record split_object proof:" split_object_prf;
2317 fun split_ex_prf () =
2319 val ss = HOL_basic_ss addsimps [not_ex RS sym, Not_eq_iff];
2320 val P_nm = fst (dest_Free P);
2321 val not_P = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
2322 val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object;
2323 val so'' = simplify ss so';
2325 prove_standard [] split_ex_prop (fn _ => resolve_tac [so''] 1)
2327 val split_ex = timeit_msg ctxt "record split_ex proof:" split_ex_prf;
2329 fun equality_tac thms =
2331 val s' :: s :: eqs = rev thms;
2332 val ss' = ss addsimps (s' :: s :: sel_convs_standard);
2333 val eqs' = map (simplify ss') eqs;
2334 in simp_tac (HOL_basic_ss addsimps (s' :: s :: eqs')) 1 end;
2336 fun equality_prf () =
2337 prove_standard [] equality_prop (fn {context, ...} =>
2339 let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
2340 st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1 THEN
2341 res_inst_tac context [((rN, 0), s')] cases_scheme 1 THEN
2342 Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1)
2343 (*simp_all_tac ss (sel_convs) would also work but is less efficient*)
2345 val equality = timeit_msg ctxt "record equality proof:" equality_prf;
2347 val ((([sel_convs', upd_convs', sel_defs', upd_defs',
2348 fold_congs', unfold_congs',
2349 splits' as [split_meta', split_object', split_ex'], derived_defs'],
2350 [surjective', equality']),
2351 [induct_scheme', induct', cases_scheme', cases']), thms_thy) =
2353 |> (Global_Theory.add_thmss o map (Thm.no_attributes o apfst Binding.name))
2354 [("select_convs", sel_convs_standard),
2355 ("update_convs", upd_convs_standard),
2356 ("select_defs", sel_defs),
2357 ("update_defs", upd_defs),
2358 ("fold_congs", fold_congs),
2359 ("unfold_congs", unfold_congs),
2360 ("splits", [split_meta_standard, split_object, split_ex]),
2361 ("defs", derived_defs)]
2362 ||>> (Global_Theory.add_thms o map (Thm.no_attributes o apfst Binding.name))
2363 [("surjective", surjective),
2364 ("equality", equality)]
2365 ||>> (Global_Theory.add_thms o (map o apfst o apfst) Binding.name)
2366 [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
2367 (("induct", induct), induct_type_global name),
2368 (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
2369 (("cases", cases), cases_type_global name)];
2371 val sel_upd_simps = sel_convs' @ upd_convs';
2372 val sel_upd_defs = sel_defs' @ upd_defs';
2373 val iffs = [ext_inject]
2374 val depth = parent_len + 1;
2376 val ([simps', iffs'], thms_thy') =
2378 |> Global_Theory.add_thmss
2379 [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
2380 ((Binding.name "iffs", iffs), [iff_add])];
2383 make_info alphas parent fields extension
2384 ext_induct ext_inject ext_surjective ext_split ext_def
2385 sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs'
2386 surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs';
2390 |> put_record name info
2391 |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs')
2392 |> add_equalities extension_id equality'
2393 |> add_extinjects ext_inject
2394 |> add_extsplit extension_name ext_split
2395 |> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
2396 |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
2397 |> add_fieldext (extension_name, snd extension) names
2398 |> add_code ext_tyco vs extT ext simps' ext_inject
2399 |> Sign.restore_naming thy;
2408 fun read_parent NONE ctxt = (NONE, ctxt)
2409 | read_parent (SOME raw_T) ctxt =
2410 (case Proof_Context.read_typ_abbrev ctxt raw_T of
2411 Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt)
2412 | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));
2414 fun prep_field prep (x, T, mx) = (x, prep T, mx)
2416 cat_error msg ("The error(s) above occurred in record field " ^ Binding.print x);
2418 fun read_field raw_field ctxt =
2419 let val field as (_, T, _) = prep_field (Syntax.read_typ ctxt) raw_field
2420 in (field, Variable.declare_typ T ctxt) end;
2424 fun add_record (params, binding) raw_parent raw_fields thy =
2426 val _ = Theory.requires thy "Record" "record definitions";
2428 val ctxt = Proof_Context.init_global thy;
2429 fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T)
2430 handle TYPE (msg, _, _) => error msg;
2435 val parent = Option.map (apfst (map cert_typ)) raw_parent
2437 cat_error msg ("The error(s) above occurred in parent record specification");
2438 val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []);
2439 val parents = get_parent_info thy parent;
2441 val bfields = map (prep_field cert_typ) raw_fields;
2445 val name = Sign.full_name thy binding;
2446 val err_dup_record =
2447 if is_none (get_info thy name) then []
2448 else ["Duplicate definition of record " ^ quote name];
2450 val spec_frees = fold Term.add_tfreesT (parent_args @ map #2 bfields) [];
2451 val err_extra_frees =
2452 (case subtract (op =) params spec_frees of
2454 | extras => ["Extra free type variable(s) " ^
2455 commas (map (Syntax.string_of_typ ctxt o TFree) extras)]);
2457 val err_no_fields = if null bfields then ["No fields present"] else [];
2459 val err_dup_fields =
2460 (case duplicates Binding.eq_name (map #1 bfields) of
2462 | dups => ["Duplicate field(s) " ^ commas (map Binding.print dups)]);
2464 val err_bad_fields =
2465 if forall (not_equal moreN o Binding.name_of o #1) bfields then []
2466 else ["Illegal field name " ^ quote moreN];
2469 err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields;
2470 val _ = if null errs then () else error (cat_lines errs);
2472 thy |> definition (params, binding) parent parents bfields
2474 handle ERROR msg => cat_error msg ("Failed to define record " ^ Binding.print binding);
2476 fun add_record_cmd (raw_params, binding) raw_parent raw_fields thy =
2478 val ctxt = Proof_Context.init_global thy;
2479 val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
2480 val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
2481 val (parent, ctxt2) = read_parent raw_parent ctxt1;
2482 val (fields, ctxt3) = fold_map read_field raw_fields ctxt2;
2483 val params' = map (Proof_Context.check_tfree ctxt3) params;
2484 in thy |> add_record (params', binding) parent fields end;
2492 Sign.add_trfuns ([], parse_translation, [], []) #>
2493 Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #>
2494 Simplifier.map_simpset_global (fn ss => ss addsimprocs [simproc, upd_simproc, eq_simproc]);
2500 Outer_Syntax.command "record" "define extensible record" Keyword.thy_decl
2501 (Parse.type_args_constrained -- Parse.binding --
2502 (Parse.$$$ "=" |-- Scan.option (Parse.typ --| Parse.$$$ "+") --
2503 Scan.repeat1 Parse.const_binding)
2504 >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd x y z)));