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 setup: theory -> theory
56 signature ISO_TUPLE_SUPPORT =
58 val add_iso_tuple_type: binding * (string * sort) list ->
59 typ * typ -> theory -> (term * term) * theory
60 val mk_cons_tuple: term * term -> term
61 val dest_cons_tuple: term -> term * term
62 val iso_tuple_intros_tac: int -> tactic
63 val named_cterm_instantiate: (string * cterm) list -> thm -> thm
66 structure Iso_Tuple_Support: ISO_TUPLE_SUPPORT =
69 val isoN = "_Tuple_Iso";
71 val iso_tuple_intro = @{thm isomorphic_tuple_intro};
72 val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};
74 val tuple_iso_tuple = (@{const_name Record.tuple_iso_tuple}, @{thm tuple_iso_tuple});
76 fun named_cterm_instantiate values thm = (* FIXME eliminate *)
78 fun match name ((name', _), _) = name = name';
80 (case find_first (match name) (Term.add_vars (prop_of thm) []) of
81 SOME var => cterm_of (theory_of_thm thm) (Var var)
82 | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm]));
84 cterm_instantiate (map (apfst getvar) values) thm
87 structure Iso_Tuple_Thms = Theory_Data
89 type T = thm Symtab.table;
90 val empty = Symtab.make [tuple_iso_tuple];
92 fun merge data = Symtab.merge Thm.eq_thm_prop data; (* FIXME handle Symtab.DUP ?? *)
95 fun get_typedef_info tyco vs
96 (({rep_type, Abs_name, ...}, {Rep_inject, Abs_inverse, ... }) : Typedef.info) thy =
100 |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] [];
101 val proj_constr = Abs_inverse OF [exists_thm];
102 val absT = Type (tyco, map TFree vs);
105 |> pair (tyco, ((Rep_inject, proj_constr), Const (Abs_name, rep_type --> absT), absT))
108 fun do_typedef raw_tyco repT raw_vs thy =
110 val ctxt = Proof_Context.init_global thy |> Variable.declare_typ repT;
111 val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
114 |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
115 (HOLogic.mk_UNIV repT) NONE (rtac UNIV_witness 1)
116 |-> (fn (tyco, info) => get_typedef_info tyco vs info)
119 fun mk_cons_tuple (left, right) =
121 val (leftT, rightT) = (fastype_of left, fastype_of right);
122 val prodT = HOLogic.mk_prodT (leftT, rightT);
123 val isomT = Type (@{type_name tuple_isomorphism}, [prodT, leftT, rightT]);
125 Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $
126 Const (fst tuple_iso_tuple, isomT) $ left $ right
129 fun dest_cons_tuple (Const (@{const_name Record.iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
130 | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
132 fun add_iso_tuple_type (b, alphas) (leftT, rightT) thy =
134 val repT = HOLogic.mk_prodT (leftT, rightT);
136 val ((_, ((rep_inject, abs_inverse), absC, absT)), typ_thy) =
138 |> do_typedef b repT alphas
139 ||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*)
141 (*construct a type and body for the isomorphism constant by
142 instantiating the theorem to which the definition will be applied*)
144 rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] iso_tuple_intro;
145 val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
146 val isomT = fastype_of body;
147 val isom_binding = Binding.suffix_name isoN b;
148 val isom_name = Sign.full_name typ_thy isom_binding;
149 val isom = Const (isom_name, isomT);
151 val ([isom_def], cdef_thy) =
153 |> Sign.declare_const_global ((isom_binding, isomT), NoSyn) |> snd
154 |> Global_Theory.add_defs false
155 [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
157 val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
158 val cons = Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
162 |> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple))
163 |> Sign.restore_naming thy
165 ((isom, cons $ isom), thm_thy)
168 val iso_tuple_intros_tac =
169 resolve_from_net_tac iso_tuple_intros THEN'
170 CSUBGOAL (fn (cgoal, i) =>
172 val thy = Thm.theory_of_cterm cgoal;
173 val goal = Thm.term_of cgoal;
175 val isthms = Iso_Tuple_Thms.get thy;
176 fun err s t = raise TERM ("iso_tuple_intros_tac: " ^ s, [t]);
178 val goal' = Envir.beta_eta_contract goal;
181 Const (@{const_name Trueprop}, _) $
182 (Const (@{const_name isomorphic_tuple}, _) $ Const is) => is
183 | _ => err "unexpected goal format" goal');
185 (case Symtab.lookup isthms (#1 is) of
187 | NONE => err "no thm found for constant" (Const is));
188 in rtac isthm i end);
193 structure Record: RECORD =
196 val surject_assistI = @{thm iso_tuple_surjective_proof_assistI};
197 val surject_assist_idE = @{thm iso_tuple_surjective_proof_assist_idE};
199 val updacc_accessor_eqE = @{thm update_accessor_accessor_eqE};
200 val updacc_updator_eqE = @{thm update_accessor_updator_eqE};
201 val updacc_eq_idI = @{thm iso_tuple_update_accessor_eq_assist_idI};
202 val updacc_eq_triv = @{thm iso_tuple_update_accessor_eq_assist_triv};
204 val updacc_foldE = @{thm update_accessor_congruence_foldE};
205 val updacc_unfoldE = @{thm update_accessor_congruence_unfoldE};
206 val updacc_noopE = @{thm update_accessor_noopE};
207 val updacc_noop_compE = @{thm update_accessor_noop_compE};
208 val updacc_cong_idI = @{thm update_accessor_cong_assist_idI};
209 val updacc_cong_triv = @{thm update_accessor_cong_assist_triv};
210 val updacc_cong_from_eq = @{thm iso_tuple_update_accessor_cong_from_eq};
214 (** name components **)
219 val schemeN = "_scheme";
220 val ext_typeN = "_ext";
221 val inner_typeN = "_inner";
223 val updateN = "_update";
225 val fields_selN = "fields";
226 val extendN = "extend";
227 val truncateN = "truncate";
233 fun varifyT idx = map_type_tfree (fn (a, S) => TVar ((a, idx), S));
238 val timing = Attrib.setup_config_bool @{binding record_timing} (K false);
239 fun timeit_msg ctxt s x = if Config.get ctxt timing then (warning s; timeit x) else x ();
240 fun timing_msg ctxt s = if Config.get ctxt timing then warning s else ();
245 val Trueprop = HOLogic.mk_Trueprop;
250 val op :== = Misc_Legacy.mk_defpair;
251 val op === = Trueprop o HOLogic.mk_eq;
252 val op ==> = Logic.mk_implies;
257 fun mk_ext (name, T) ts =
258 let val Ts = map fastype_of ts
259 in list_comb (Const (suffix extN name, Ts ---> T), ts) end;
264 fun mk_selC sT (c, T) = (c, sT --> T);
266 fun mk_sel s (c, T) =
267 let val sT = fastype_of s
268 in Const (mk_selC sT (c, T)) $ s end;
273 fun mk_updC sfx sT (c, T) = (suffix sfx c, (T --> T) --> sT --> sT);
275 fun mk_upd' sfx c v sT =
276 let val vT = domain_type (fastype_of v);
277 in Const (mk_updC sfx sT (c, vT)) $ v end;
279 fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s;
284 fun dest_recT (typ as Type (c_ext_type, Ts as (_ :: _))) =
285 (case try (unsuffix ext_typeN) c_ext_type of
286 NONE => raise TYPE ("Record.dest_recT", [typ], [])
287 | SOME c => ((c, Ts), List.last Ts))
288 | dest_recT typ = raise TYPE ("Record.dest_recT", [typ], []);
290 val is_recT = can dest_recT;
293 let val ((c, Ts), U) = dest_recT T
294 in (c, Ts) :: dest_recTs U
295 end handle TYPE _ => [];
298 let val ((c, Ts), U) = dest_recT T in
302 end handle TYPE _ => NONE;
306 val rTs = dest_recTs T;
307 val rTs' = if i < 0 then rTs else take i rTs;
308 in implode (map #1 rTs') end;
312 (*** extend theory by record definition ***)
316 (* type info and parent_info *)
319 {args: (string * sort) list,
320 parent: (typ list * string) option,
321 fields: (string * typ) list,
322 extension: (string * typ list),
330 select_convs: thm list,
331 update_convs: thm list,
332 select_defs: thm list,
333 update_defs: thm list,
334 fold_congs: thm list, (* FIXME unused!? *)
335 unfold_congs: thm list, (* FIXME unused!? *)
349 fun make_info args parent fields extension
350 ext_induct ext_inject ext_surjective ext_split ext_def
351 select_convs update_convs select_defs update_defs fold_congs unfold_congs splits defs
352 surjective equality induct_scheme induct cases_scheme cases
354 {args = args, parent = parent, fields = fields, extension = extension,
355 ext_induct = ext_induct, ext_inject = ext_inject, ext_surjective = ext_surjective,
356 ext_split = ext_split, ext_def = ext_def, select_convs = select_convs,
357 update_convs = update_convs, select_defs = select_defs, update_defs = update_defs,
358 fold_congs = fold_congs, unfold_congs = unfold_congs, splits = splits, defs = defs,
359 surjective = surjective, equality = equality, induct_scheme = induct_scheme,
360 induct = induct, cases_scheme = cases_scheme, cases = cases, simps = simps, iffs = iffs};
364 fields: (string * typ) list,
365 extension: (string * typ list),
369 fun make_parent_info name fields extension ext_def induct_scheme : parent_info =
370 {name = name, fields = fields, extension = extension,
371 ext_def = ext_def, induct_scheme = induct_scheme};
377 {records: info Symtab.table,
379 {selectors: (int * bool) Symtab.table,
380 updates: string Symtab.table,
383 equalities: thm Symtab.table,
384 extinjects: thm list,
385 extsplit: thm Symtab.table, (*maps extension name to split rule*)
386 splits: (thm * thm * thm * thm) Symtab.table, (*!!, ALL, EX - split-equalities, induct rule*)
387 extfields: (string * typ) list Symtab.table, (*maps extension to its fields*)
388 fieldext: (string * typ list) Symtab.table}; (*maps field to its extension*)
391 records sel_upd equalities extinjects extsplit splits extfields fieldext =
392 {records = records, sel_upd = sel_upd,
393 equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
394 extfields = extfields, fieldext = fieldext }: data;
396 structure Data = Theory_Data
400 make_data Symtab.empty
401 {selectors = Symtab.empty, updates = Symtab.empty,
402 simpset = HOL_basic_ss, defset = HOL_basic_ss}
403 Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
407 sel_upd = {selectors = sels1, updates = upds1, simpset = ss1, defset = ds1},
408 equalities = equalities1,
409 extinjects = extinjects1,
410 extsplit = extsplit1,
412 extfields = extfields1,
413 fieldext = fieldext1},
415 sel_upd = {selectors = sels2, updates = upds2, simpset = ss2, defset = ds2},
416 equalities = equalities2,
417 extinjects = extinjects2,
418 extsplit = extsplit2,
420 extfields = extfields2,
421 fieldext = fieldext2}) =
423 (Symtab.merge (K true) (recs1, recs2))
424 {selectors = Symtab.merge (K true) (sels1, sels2),
425 updates = Symtab.merge (K true) (upds1, upds2),
426 simpset = Simplifier.merge_ss (ss1, ss2),
427 defset = Simplifier.merge_ss (ds1, ds2)}
428 (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
429 (Thm.merge_thms (extinjects1, extinjects2))
430 (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
431 (Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
432 Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
433 Thm.eq_thm (c, y) andalso Thm.eq_thm (d, z)) (splits1, splits2))
434 (Symtab.merge (K true) (extfields1, extfields2))
435 (Symtab.merge (K true) (fieldext1, fieldext2));
439 (* access 'records' *)
441 val get_info = Symtab.lookup o #records o Data.get;
443 fun the_info thy name =
444 (case get_info thy name of
446 | NONE => error ("Unknown record type " ^ quote name));
448 fun put_record name info =
449 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
450 make_data (Symtab.update (name, info) records)
451 sel_upd equalities extinjects extsplit splits extfields fieldext);
454 (* access 'sel_upd' *)
456 val get_sel_upd = #sel_upd o Data.get;
458 val is_selector = Symtab.defined o #selectors o get_sel_upd;
459 val get_updates = Symtab.lookup o #updates o get_sel_upd;
460 fun get_ss_with_context getss thy = Simplifier.global_context thy (getss (get_sel_upd thy));
462 val get_simpset = get_ss_with_context #simpset;
463 val get_sel_upd_defs = get_ss_with_context #defset;
465 fun get_update_details u thy =
466 let val sel_upd = get_sel_upd thy in
467 (case Symtab.lookup (#updates sel_upd) u of
469 let val SOME (dep, ismore) = Symtab.lookup (#selectors sel_upd) s
470 in SOME (s, dep, ismore) end
474 fun put_sel_upd names more depth simps defs thy =
476 val all = names @ [more];
477 val sels = map (rpair (depth, false)) names @ [(more, (depth, true))];
478 val upds = map (suffix updateN) all ~~ all;
480 val {records, sel_upd = {selectors, updates, simpset, defset},
481 equalities, extinjects, extsplit, splits, extfields, fieldext} = Data.get thy;
484 {selectors = fold Symtab.update_new sels selectors,
485 updates = fold Symtab.update_new upds updates,
486 simpset = simpset addsimps simps,
487 defset = defset addsimps defs}
488 equalities extinjects extsplit splits extfields fieldext;
489 in Data.put data thy end;
492 (* access 'equalities' *)
494 fun add_equalities name thm =
495 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
496 make_data records sel_upd
497 (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext);
499 val get_equalities = Symtab.lookup o #equalities o Data.get;
502 (* access 'extinjects' *)
504 fun add_extinjects thm =
505 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
506 make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
507 extsplit splits extfields fieldext);
509 val get_extinjects = rev o #extinjects o Data.get;
512 (* access 'extsplit' *)
514 fun add_extsplit name thm =
515 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
516 make_data records sel_upd equalities extinjects
517 (Symtab.update_new (name, thm) extsplit) splits extfields fieldext);
520 (* access 'splits' *)
522 fun add_splits name thmP =
523 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
524 make_data records sel_upd equalities extinjects extsplit
525 (Symtab.update_new (name, thmP) splits) extfields fieldext);
527 val get_splits = Symtab.lookup o #splits o Data.get;
530 (* parent/extension of named record *)
532 val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o Data.get);
533 val get_extension = Option.map #extension oo (Symtab.lookup o #records o Data.get);
536 (* access 'extfields' *)
538 fun add_extfields name fields =
539 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
540 make_data records sel_upd equalities extinjects extsplit splits
541 (Symtab.update_new (name, fields) extfields) fieldext);
543 val get_extfields = Symtab.lookup o #extfields o Data.get;
545 fun get_extT_fields thy T =
547 val ((name, Ts), moreT) = dest_recT T;
549 let val (nm :: _ :: rst) = rev (Long_Name.explode name) (* FIXME !? *)
550 in Long_Name.implode (rev (nm :: rst)) end;
551 val varifyT = varifyT (maxidx_of_typs (moreT :: Ts) + 1);
552 val {records, extfields, ...} = Data.get thy;
553 val (fields, (more, _)) = split_last (Symtab.lookup_list extfields name);
554 val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
556 val subst = fold (Sign.typ_match thy) (#1 (split_last args) ~~ #1 (split_last Ts)) Vartab.empty;
557 val fields' = map (apsnd (Envir.norm_type subst o varifyT)) fields;
558 in (fields', (more, moreT)) end;
560 fun get_recT_fields thy T =
562 val (root_fields, (root_more, root_moreT)) = get_extT_fields thy T;
563 val (rest_fields, rest_more) =
564 if is_recT root_moreT then get_recT_fields thy root_moreT
565 else ([], (root_more, root_moreT));
566 in (root_fields @ rest_fields, rest_more) end;
569 (* access 'fieldext' *)
571 fun add_fieldext extname_types fields =
572 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
575 fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
576 in make_data records sel_upd equalities extinjects extsplit splits extfields fieldext' end);
578 val get_fieldext = Symtab.lookup o #fieldext o Data.get;
585 fun add_parents _ NONE = I
586 | add_parents thy (SOME (types, name)) =
588 fun err msg = error (msg ^ " parent record " ^ quote name);
590 val {args, parent, ...} =
591 (case get_info thy name of SOME info => info | NONE => err "Unknown");
592 val _ = if length types <> length args then err "Bad number of arguments for" else ();
594 fun bad_inst ((x, S), T) =
595 if Sign.of_sort thy (T, S) then NONE else SOME x
596 val bads = map_filter bad_inst (args ~~ types);
597 val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");
599 val inst = args ~~ types;
600 val subst = Term.map_type_tfree (the o AList.lookup (op =) inst);
601 val parent' = Option.map (apfst (map subst)) parent;
602 in cons (name, inst) #> add_parents thy parent' end;
606 fun get_hierarchy thy (name, types) = add_parents thy (SOME (types, name)) [];
608 fun get_parent_info thy parent =
609 add_parents thy parent [] |> map (fn (name, inst) =>
611 val subst = Term.map_type_tfree (the o AList.lookup (op =) inst);
612 val {fields, extension, induct_scheme, ext_def, ...} = the_info thy name;
613 val fields' = map (apsnd subst) fields;
614 val extension' = apsnd (map subst) extension;
615 in make_parent_info name fields' extension' ext_def induct_scheme end);
621 (** concrete syntax for records **)
623 (* parse translations *)
627 fun split_args (field :: fields) ((name, arg) :: fargs) =
628 if can (unsuffix name) field then
629 let val (args, rest) = split_args fields fargs
630 in (arg :: args, rest) end
631 else raise Fail ("expecting field " ^ quote field ^ " but got " ^ quote name)
632 | split_args [] (fargs as (_ :: _)) = ([], fargs)
633 | split_args (_ :: _) [] = raise Fail "expecting more fields"
634 | split_args _ _ = ([], []);
636 fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) =
638 | field_type_tr t = raise TERM ("field_type_tr", [t]);
640 fun field_types_tr (Const (@{syntax_const "_field_types"}, _) $ t $ u) =
641 field_type_tr t :: field_types_tr u
642 | field_types_tr t = [field_type_tr t];
644 fun record_field_types_tr more ctxt t =
646 val thy = Proof_Context.theory_of ctxt;
647 fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]);
649 fun mk_ext (fargs as (name, _) :: _) =
650 (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
651 SOME (ext, alphas) =>
652 (case get_extfields thy ext of
655 val (fields', _) = split_last fields;
656 val types = map snd fields';
657 val (args, rest) = split_args (map fst fields') fargs
658 handle Fail msg => err msg;
659 val argtypes = Syntax.check_typs ctxt (map Syntax_Phases.decode_typ args);
660 val varifyT = varifyT (fold Term.maxidx_typ argtypes ~1 + 1);
661 val vartypes = map varifyT types;
663 val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
664 handle Type.TYPE_MATCH => err "type is no proper record (extension)";
666 map (Syntax_Phases.term_of_typ ctxt o Envir.norm_type subst o varifyT)
667 (#1 (split_last alphas));
669 val more' = mk_ext rest;
672 (Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
674 | NONE => err ("no fields defined for " ^ quote ext))
675 | NONE => err (quote name ^ " is no proper field"))
678 mk_ext (field_types_tr t)
681 fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const @{type_syntax unit}) ctxt t
682 | record_type_tr _ ts = raise TERM ("record_type_tr", ts);
684 fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t
685 | record_type_scheme_tr _ ts = raise TERM ("record_type_scheme_tr", ts);
688 fun field_tr ((Const (@{syntax_const "_field"}, _) $ Const (name, _) $ arg)) = (name, arg)
689 | field_tr t = raise TERM ("field_tr", [t]);
691 fun fields_tr (Const (@{syntax_const "_fields"}, _) $ t $ u) = field_tr t :: fields_tr u
692 | fields_tr t = [field_tr t];
694 fun record_fields_tr more ctxt t =
696 val thy = Proof_Context.theory_of ctxt;
697 fun err msg = raise TERM ("Error in record input: " ^ msg, [t]);
699 fun mk_ext (fargs as (name, _) :: _) =
700 (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
702 (case get_extfields thy ext of
705 val (args, rest) = split_args (map fst (fst (split_last fields))) fargs
706 handle Fail msg => err msg;
707 val more' = mk_ext rest;
708 in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end
709 | NONE => err ("no fields defined for " ^ quote ext))
710 | NONE => err (quote name ^ " is no proper field"))
712 in mk_ext (fields_tr t) end;
714 fun record_tr ctxt [t] = record_fields_tr (Syntax.const @{const_syntax Unity}) ctxt t
715 | record_tr _ ts = raise TERM ("record_tr", ts);
717 fun record_scheme_tr ctxt [t, more] = record_fields_tr more ctxt t
718 | record_scheme_tr _ ts = raise TERM ("record_scheme_tr", ts);
721 fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) =
722 Syntax.const (suffix updateN name) $ Abs (Name.uu_, dummyT, arg)
723 | field_update_tr t = raise TERM ("field_update_tr", [t]);
725 fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) =
726 field_update_tr t :: field_updates_tr u
727 | field_updates_tr t = [field_update_tr t];
729 fun record_update_tr [t, u] = fold (curry op $) (field_updates_tr u) t
730 | record_update_tr ts = raise TERM ("record_update_tr", ts);
734 val parse_translation =
735 [(@{syntax_const "_record_update"}, record_update_tr)];
737 val advanced_parse_translation =
738 [(@{syntax_const "_record"}, record_tr),
739 (@{syntax_const "_record_scheme"}, record_scheme_tr),
740 (@{syntax_const "_record_type"}, record_type_tr),
741 (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)];
746 (* print translations *)
748 val type_abbr = Attrib.setup_config_bool @{binding record_type_abbr} (K true);
749 val type_as_fields = Attrib.setup_config_bool @{binding record_type_as_fields} (K true);
754 (* FIXME early extern (!??) *)
755 (* FIXME Syntax.free (??) *)
756 fun field_type_tr' (c, t) = Syntax.const @{syntax_const "_field_type"} $ Syntax.const c $ t;
758 fun field_types_tr' (t, u) = Syntax.const @{syntax_const "_field_types"} $ t $ u;
760 fun record_type_tr' ctxt t =
762 val thy = Proof_Context.theory_of ctxt;
764 val T = Syntax_Phases.decode_typ t;
765 val varifyT = varifyT (Term.maxidx_of_typ T + 1);
769 Type (ext, args as _ :: _) =>
770 (case try (unsuffix ext_typeN) ext of
772 (case get_extfields thy ext' of
773 SOME (fields as (x, _) :: _) =>
774 (case get_fieldext thy x of
777 val (f :: fs, _) = split_last fields;
779 apfst (Proof_Context.extern_const ctxt) f ::
780 map (apfst Long_Name.base_name) fs;
781 val (args', more) = split_last args;
782 val alphavars = map varifyT (#1 (split_last alphas));
783 val subst = Type.raw_matches (alphavars, args') Vartab.empty;
784 val fields'' = (map o apsnd) (Envir.norm_type subst o varifyT) fields';
785 in fields'' @ strip_fields more end
786 handle Type.TYPE_MATCH => [("", T)])
792 val (fields, (_, moreT)) = split_last (strip_fields T);
793 val _ = null fields andalso raise Match;
795 foldr1 field_types_tr'
796 (map (field_type_tr' o apsnd (Syntax_Phases.term_of_typ ctxt)) fields);
798 if not (Config.get ctxt type_as_fields) orelse null fields then raise Match
799 else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
801 Syntax.const @{syntax_const "_record_type_scheme"} $ u $
802 Syntax_Phases.term_of_typ ctxt moreT
805 (*try to reconstruct the record name type abbreviation from
806 the (nested) extension types*)
807 fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm =
809 val T = Syntax_Phases.decode_typ tm;
810 val varifyT = varifyT (maxidx_of_typ T + 1);
812 fun mk_type_abbr subst name args =
813 let val abbrT = Type (name, map (varifyT o TFree) args)
814 in Syntax_Phases.term_of_typ ctxt (Envir.norm_type subst abbrT) end;
816 fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
818 if Config.get ctxt type_abbr then
821 if name = last_ext then
822 let val subst = match schemeT T in
823 if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree zeta)))
824 then mk_type_abbr subst abbr alphas
825 else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
826 end handle Type.TYPE_MATCH => record_type_tr' ctxt tm
827 else raise Match (*give print translation of specialised record a chance*)
829 else record_type_tr' ctxt tm
834 fun record_ext_type_tr' name =
836 val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);
838 record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts));
839 in (ext_type_name, tr') end;
841 fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
843 val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);
845 record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt
846 (list_comb (Syntax.const ext_type_name, ts));
847 in (ext_type_name, tr') end;
854 (* FIXME Syntax.free (??) *)
855 fun field_tr' (c, t) = Syntax.const @{syntax_const "_field"} $ Syntax.const c $ t;
856 fun fields_tr' (t, u) = Syntax.const @{syntax_const "_fields"} $ t $ u;
858 fun record_tr' ctxt t =
860 val thy = Proof_Context.theory_of ctxt;
863 (case strip_comb t of
864 (Const (ext, _), args as (_ :: _)) =>
865 (case try (Lexicon.unmark_const o unsuffix extN) ext of
867 (case get_extfields thy ext' of
870 val (f :: fs, _) = split_last (map fst fields);
871 val fields' = Proof_Context.extern_const ctxt f :: map Long_Name.base_name fs;
872 val (args', more) = split_last args;
873 in (fields' ~~ args') @ strip_fields more end
874 handle ListPair.UnequalLengths => [("", t)])
879 val (fields, (_, more)) = split_last (strip_fields t);
880 val _ = null fields andalso raise Match;
881 val u = foldr1 fields_tr' (map field_tr' fields);
884 Const (@{const_syntax Unity}, _) => Syntax.const @{syntax_const "_record"} $ u
885 | _ => Syntax.const @{syntax_const "_record_scheme"} $ u $ more)
890 fun record_ext_tr' name =
892 val ext_name = Lexicon.mark_const (name ^ extN);
893 fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));
894 in (ext_name, tr') end;
901 fun dest_update ctxt c =
902 (case try Lexicon.unmark_const c of
903 SOME d => try (unsuffix updateN) (Proof_Context.extern_const ctxt d)
906 fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
907 (case dest_update ctxt c of
909 (case try Syntax_Trans.const_abs_tr' k of
911 apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
912 (field_updates_tr' ctxt u)
915 | field_updates_tr' _ tm = ([], tm);
917 fun record_update_tr' ctxt tm =
918 (case field_updates_tr' ctxt tm of
919 ([], _) => raise Match
921 Syntax.const @{syntax_const "_record_update"} $ u $
922 foldr1 (fn (v, w) => Syntax.const @{syntax_const "_field_updates"} $ v $ w) (rev ts));
926 fun field_update_tr' name =
928 val update_name = Lexicon.mark_const (name ^ updateN);
929 fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u)
930 | tr' _ _ = raise Match;
931 in (update_name, tr') end;
937 (** record simprocs **)
939 fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) =
940 (case get_updates thy u of
941 SOME u_name => u_name = s
942 | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));
945 let val T = range_type (fastype_of f)
946 in HOLogic.mk_comp (Const (@{const_name Fun.id}, T --> T), f) end;
948 fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
949 | get_upd_funs _ = [];
951 fun get_accupd_simps thy term defset =
953 val (acc, [body]) = strip_comb term;
954 val upd_funs = sort_distinct Term_Ord.fast_term_ord (get_upd_funs body);
957 (* FIXME fresh "f" (!?) *)
958 val T = domain_type (fastype_of upd);
959 val lhs = HOLogic.mk_comp (acc, upd $ Free ("f", T));
961 if is_sel_upd_pair thy acc upd
962 then HOLogic.mk_comp (Free ("f", T), acc)
964 val prop = lhs === rhs;
966 Goal.prove (Proof_Context.init_global thy) [] [] prop
968 simp_tac defset 1 THEN
969 REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
970 TRY (simp_tac (HOL_ss addsimps @{thms id_apply id_o o_id}) 1));
972 if is_sel_upd_pair thy acc upd
973 then @{thm o_eq_dest}
974 else @{thm o_eq_id_dest};
975 in Drule.export_without_context (othm RS dest) end;
976 in map get_simp upd_funs end;
978 fun get_updupd_simp thy defset u u' comp =
980 (* FIXME fresh "f" (!?) *)
981 val f = Free ("f", domain_type (fastype_of u));
982 val f' = Free ("f'", domain_type (fastype_of u'));
983 val lhs = HOLogic.mk_comp (u $ f, u' $ f');
986 then u $ HOLogic.mk_comp (f, f')
987 else HOLogic.mk_comp (u' $ f', u $ f);
988 val prop = lhs === rhs;
990 Goal.prove (Proof_Context.init_global thy) [] [] prop
992 simp_tac defset 1 THEN
993 REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
994 TRY (simp_tac (HOL_ss addsimps @{thms id_apply}) 1));
995 val dest = if comp then @{thm o_eq_dest_lhs} else @{thm o_eq_dest};
996 in Drule.export_without_context (othm RS dest) end;
998 fun get_updupd_simps thy term defset =
1000 val upd_funs = get_upd_funs term;
1001 val cname = fst o dest_Const;
1002 fun getswap u u' = get_updupd_simp thy defset u u' (cname u = cname u');
1003 fun build_swaps_to_eq _ [] swaps = swaps
1004 | build_swaps_to_eq upd (u :: us) swaps =
1006 val key = (cname u, cname upd);
1008 if Symreltab.defined swaps key then swaps
1009 else Symreltab.insert (K true) (key, getswap u upd) swaps;
1011 if cname u = cname upd then newswaps
1012 else build_swaps_to_eq upd us newswaps
1014 fun swaps_needed [] _ _ swaps = map snd (Symreltab.dest swaps)
1015 | swaps_needed (u :: us) prev seen swaps =
1016 if Symtab.defined seen (cname u)
1017 then swaps_needed us prev seen (build_swaps_to_eq u prev swaps)
1018 else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps;
1019 in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end;
1021 val named_cterm_instantiate = Iso_Tuple_Support.named_cterm_instantiate;
1023 fun prove_unfold_defs thy ex_simps ex_simprs prop =
1025 val defset = get_sel_upd_defs thy;
1026 val prop' = Envir.beta_eta_contract prop;
1027 val (lhs, _) = Logic.dest_equals (Logic.strip_assums_concl prop');
1028 val (_, args) = strip_comb lhs;
1029 val simps = (if length args = 1 then get_accupd_simps else get_updupd_simps) thy lhs defset;
1031 Goal.prove (Proof_Context.init_global thy) [] [] prop'
1033 simp_tac (HOL_basic_ss addsimps (simps @ @{thms K_record_comp})) 1 THEN
1034 TRY (simp_tac (HOL_basic_ss addsimps ex_simps addsimprocs ex_simprs) 1))
1040 fun eq (s1: string) (s2: string) = (s1 = s2);
1042 fun has_field extfields f T =
1043 exists (fn (eN, _) => exists (eq f o fst) (Symtab.lookup_list extfields eN)) (dest_recTs T);
1045 fun K_skeleton n (T as Type (_, [_, kT])) (b as Bound i) (Abs (x, xT, t)) =
1046 if null (loose_bnos t) then ((n, kT), (Abs (x, xT, Bound (i + 1)))) else ((n, T), b)
1047 | K_skeleton n T b _ = ((n, T), b);
1054 Simplify selections of an record update:
1055 (1) S (S_update k r) = k (S r)
1056 (2) S (X_update k r) = S r
1058 The simproc skips multiple updates at once, eg:
1059 S (X_update x (Y_update y (S_update k r))) = k (S r)
1061 But be careful in (2) because of the extensibility of records.
1062 - If S is a more-selector we have to make sure that the update on component
1063 X does not affect the selected subrecord.
1064 - If X is a more-selector we have to make sure that S is not in the updated
1068 Simplifier.simproc_global @{theory HOL} "record_simp" ["x"]
1069 (fn thy => fn _ => fn t =>
1071 (sel as Const (s, Type (_, [_, rangeS]))) $
1072 ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
1073 if is_selector thy s andalso is_some (get_updates thy u) then
1075 val {sel_upd = {updates, ...}, extfields, ...} = Data.get thy;
1077 fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
1078 (case Symtab.lookup updates u of
1082 (case mk_eq_terms r of
1087 val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
1088 in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end
1089 | SOME (trm, trm', vars) =>
1091 val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k;
1092 in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end)
1093 else if has_field extfields u_name rangeS orelse
1094 has_field extfields s (domain_type kT) then NONE
1096 (case mk_eq_terms r of
1097 SOME (trm, trm', vars) =>
1098 let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k
1099 in SOME (upd $ kb $ trm, trm', kv :: vars) end
1104 val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
1105 in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end))
1106 | mk_eq_terms _ = NONE;
1108 (case mk_eq_terms (upd $ k $ r) of
1109 SOME (trm, trm', vars) =>
1111 (prove_unfold_defs thy [] []
1112 (Logic.list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
1118 fun get_upd_acc_cong_thm upd acc thy simpset =
1120 val insts = [("upd", cterm_of thy upd), ("ac", cterm_of thy acc)];
1121 val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv);
1123 Goal.prove (Proof_Context.init_global thy) [] [] prop
1125 simp_tac simpset 1 THEN
1126 REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
1127 TRY (resolve_tac [updacc_cong_idI] 1))
1133 (*Simplify multiple updates:
1134 (1) "N_update y (M_update g (N_update x (M_update f r))) =
1135 (N_update (y o x) (M_update (g o f) r))"
1136 (2) "r(|M:= M r|) = r"
1138 In both cases "more" updates complicate matters: for this reason
1139 we omit considering further updates if doing so would introduce
1140 both a more update and an update to a field within it.*)
1142 Simplifier.simproc_global @{theory HOL} "record_upd_simp" ["x"]
1143 (fn thy => fn _ => fn t =>
1145 (*We can use more-updators with other updators as long
1146 as none of the other updators go deeper than any more
1147 updator. min here is the depth of the deepest other
1148 updator, max the depth of the shallowest more updator.*)
1149 fun include_depth (dep, true) (min, max) =
1151 then SOME (min, if dep <= max orelse max = ~1 then dep else max)
1153 | include_depth (dep, false) (min, max) =
1154 if dep <= max orelse max = ~1
1155 then SOME (if min <= dep then dep else min, max)
1158 fun getupdseq (term as (upd as Const (u, _)) $ f $ tm) min max =
1159 (case get_update_details u thy of
1160 SOME (s, dep, ismore) =>
1161 (case include_depth (dep, ismore) (min, max) of
1162 SOME (min', max') =>
1163 let val (us, bs, _) = getupdseq tm min' max'
1164 in ((upd, s, f) :: us, bs, fastype_of term) end
1165 | NONE => ([], term, HOLogic.unitT))
1166 | NONE => ([], term, HOLogic.unitT))
1167 | getupdseq term _ _ = ([], term, HOLogic.unitT);
1169 val (upds, base, baseT) = getupdseq t 0 ~1;
1171 fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm =
1172 if s = s' andalso null (loose_bnos tm')
1173 andalso subst_bound (HOLogic.unit, tm') = tm
1174 then (true, Abs (n, T, Const (s', T') $ Bound 1))
1175 else (false, HOLogic.unit)
1176 | is_upd_noop _ _ _ = (false, HOLogic.unit);
1178 fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) =
1180 val ss = get_sel_upd_defs thy;
1181 val uathm = get_upd_acc_cong_thm upd acc thy ss;
1183 [Drule.export_without_context (uathm RS updacc_noopE),
1184 Drule.export_without_context (uathm RS updacc_noop_compE)]
1187 (*If f is constant then (f o g) = f. We know that K_skeleton
1188 only returns constant abstractions thus when we see an
1189 abstraction we can discard inner updates.*)
1190 fun add_upd (f as Abs _) fs = [f]
1191 | add_upd f fs = (f :: fs);
1193 (*mk_updterm returns
1194 (orig-term-skeleton, simplified-skeleton,
1195 variables, duplicate-updates, simp-flag, noop-simps)
1197 where duplicate-updates is a table used to pass upward
1198 the list of update functions which can be composed
1199 into an update above them, simp-flag indicates whether
1200 any simplification was achieved, and noop-simps are
1201 used for eliminating case (2) defined above*)
1202 fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term =
1204 val (lhs, rhs, vars, dups, simp, noops) =
1205 mk_updterm upds (Symtab.update (u, ()) above) term;
1207 K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f;
1208 val (isnoop, skelf') = is_upd_noop s f term;
1209 val funT = domain_type T;
1210 fun mk_comp_local (f, f') =
1211 Const (@{const_name Fun.comp}, funT --> funT --> funT) $ f $ f';
1214 (upd $ skelf' $ lhs, rhs, vars,
1215 Symtab.update (u, []) dups, true,
1216 if Symtab.defined noops u then noops
1217 else Symtab.update (u, get_noop_simps upd skelf') noops)
1218 else if Symtab.defined above u then
1219 (upd $ skelf $ lhs, rhs, fvar :: vars,
1220 Symtab.map_default (u, []) (add_upd skelf) dups,
1223 (case Symtab.lookup dups u of
1226 upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs,
1227 fvar :: vars, dups, true, noops)
1228 | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops))
1230 | mk_updterm [] _ _ =
1231 (Bound 0, Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty)
1232 | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _) => x) us);
1234 val (lhs, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
1235 val noops' = maps snd (Symtab.dest noops);
1239 (prove_unfold_defs thy noops' [simproc]
1240 (Logic.list_all (vars, Logic.mk_equals (lhs, rhs))))
1249 (*Look up the most specific record-equality.
1252 Testing equality of records boils down to the test of equality of all components.
1253 Therefore the complexity is: #components * complexity for single component.
1254 Especially if a record has a lot of components it may be better to split up
1255 the record first and do simplification on that (split_simp_tac).
1256 e.g. r(|lots of updates|) = x
1258 eq_simproc split_simp_tac
1259 Complexity: #components * #updates #updates
1262 Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
1263 (fn thy => fn _ => fn t =>
1264 (case t of Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ =>
1265 (case rec_id ~1 T of
1268 (case get_equalities thy name of
1270 | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
1276 (*Split quantified occurrences of records, for which P holds. P can peek on the
1277 subterm starting at the quantified occurrence of the record (including the quantifier):
1278 P t = 0: do not split
1279 P t = ~1: completely split
1280 P t > 0: split up to given bound of record extensions.*)
1281 fun split_simproc P =
1282 Simplifier.simproc_global @{theory HOL} "record_split_simp" ["x"]
1283 (fn thy => fn _ => fn t =>
1285 Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
1286 if quantifier = @{const_name all} orelse
1287 quantifier = @{const_name All} orelse
1288 quantifier = @{const_name Ex}
1290 (case rec_id ~1 T of
1293 let val split = P t in
1295 (case get_splits thy (rec_id split T) of
1297 | SOME (all_thm, All_thm, Ex_thm, _) =>
1300 @{const_name all} => all_thm
1301 | @{const_name All} => All_thm RS @{thm eq_reflection}
1302 | @{const_name Ex} => Ex_thm RS @{thm eq_reflection}
1303 | _ => raise Fail "split_simproc"))
1309 val ex_sel_eq_simproc =
1310 Simplifier.simproc_global @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
1311 (fn thy => fn ss => fn t =>
1313 fun mkeq (lr, Teq, (sel, Tsel), x) i =
1314 if is_selector thy sel then
1317 if not (Term.is_dependent x)
1318 then Free ("x" ^ string_of_int i, range_type Tsel)
1319 else raise TERM ("", [x]);
1320 val sel' = Const (sel, Tsel) $ Bound 0;
1321 val (l, r) = if lr then (sel', x') else (x', sel');
1322 in Const (@{const_name HOL.eq}, Teq) $ l $ r end
1323 else raise TERM ("", [Const (sel, Tsel)]);
1325 fun dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
1326 (true, Teq, (sel, Tsel), X)
1327 | dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
1328 (false, Teq, (sel, Tsel), X)
1329 | dest_sel_eq _ = raise TERM ("", []);
1332 Const (@{const_name Ex}, Tex) $ Abs (s, T, t) =>
1334 val eq = mkeq (dest_sel_eq t) 0;
1336 Logic.list_all ([("r", T)],
1338 (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
1340 SOME (Skip_Proof.prove_global thy [] [] prop
1341 (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
1342 addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))
1343 end handle TERM _ => NONE)
1348 (* split_simp_tac *)
1350 (*Split (and simplify) all records in the goal for which P holds.
1351 For quantified occurrences of a record
1352 P can peek on the whole subterm (including the quantifier); for free variables P
1353 can only peek on the variable itself.
1354 P t = 0: do not split
1355 P t = ~1: completely split
1356 P t > 0: split up to given bound of record extensions.*)
1357 fun split_simp_tac thms P = CSUBGOAL (fn (cgoal, i) =>
1359 val thy = Thm.theory_of_cterm cgoal;
1361 val goal = term_of cgoal;
1362 val frees = filter (is_recT o #2) (Term.add_frees goal []);
1364 val has_rec = exists_Const
1365 (fn (s, Type (_, [Type (_, [T, _]), _])) =>
1366 (s = @{const_name all} orelse s = @{const_name All} orelse s = @{const_name Ex}) andalso
1370 fun mk_split_free_tac free induct_thm i =
1372 val cfree = cterm_of thy free;
1373 val _$ (_ $ r) = concl_of induct_thm;
1374 val crec = cterm_of thy r;
1375 val thm = cterm_instantiate [(crec, cfree)] induct_thm;
1377 simp_tac (HOL_basic_ss addsimps @{thms induct_atomize}) i THEN
1379 simp_tac (HOL_basic_ss addsimps @{thms induct_rulify}) i
1382 val split_frees_tacs =
1383 frees |> map_filter (fn (x, T) =>
1384 (case rec_id ~1 T of
1388 val free = Free (x, T);
1392 (case get_splits thy (rec_id split T) of
1394 | SOME (_, _, _, induct_thm) =>
1395 SOME (mk_split_free_tac free induct_thm i))
1399 val simprocs = if has_rec goal then [split_simproc P] else [];
1400 val thms' = @{thms o_apply K_record_comp} @ thms;
1402 EVERY split_frees_tacs THEN
1403 full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i
1409 (*Split all records in the goal, which are quantified by !! or ALL.*)
1410 val split_tac = CSUBGOAL (fn (cgoal, i) =>
1412 val goal = term_of cgoal;
1414 val has_rec = exists_Const
1415 (fn (s, Type (_, [Type (_, [T, _]), _])) =>
1416 (s = @{const_name all} orelse s = @{const_name All}) andalso is_recT T
1419 fun is_all (Const (@{const_name all}, _) $ _) = ~1
1420 | is_all (Const (@{const_name All}, _) $ _) = ~1
1423 if has_rec goal then
1424 full_simp_tac (HOL_basic_ss addsimprocs [split_simproc is_all]) i
1431 val split_name = "record_split_tac";
1432 val split_wrapper = (split_name, fn _ => fn tac => split_tac ORELSE' tac);
1436 (** theory extender interface **)
1440 fun case_names_fields x = Rule_Cases.case_names ["fields"] x;
1441 fun induct_type_global name = [case_names_fields, Induct.induct_type name];
1442 fun cases_type_global name = [case_names_fields, Induct.cases_type name];
1447 (*Do case analysis / induction according to rule on last parameter of ith subgoal
1448 (or on s if there are no parameters).
1449 Instatiation of record variable (and predicate) in rule is calculated to
1450 avoid problems with higher order unification.*)
1451 fun try_param_tac s rule = CSUBGOAL (fn (cgoal, i) =>
1453 val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
1455 val g = Thm.term_of cgoal;
1456 val params = Logic.strip_params g;
1457 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
1458 val rule' = Thm.lift_rule cgoal rule;
1459 val (P, ys) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_assums_concl (prop_of rule')));
1460 (*ca indicates if rule is a case analysis or induction rule*)
1462 (case rev (drop (length params) ys) of
1463 [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
1464 (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
1465 | [x] => (head_of x, false));
1468 (map (pairself cert)
1471 (case AList.lookup (op =) (Term.add_frees g []) s of
1472 NONE => error "try_param_tac: no such variable"
1473 | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
1475 [(P, fold_rev Term.abs params (if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
1476 (x, fold_rev Term.abs params (Bound 0))])) rule';
1477 in compose_tac (false, rule'', nprems_of rule) i end);
1480 fun extension_definition name fields alphas zeta moreT more vars thy =
1482 val ctxt = Proof_Context.init_global thy;
1484 val base_name = Long_Name.base_name name;
1486 val fieldTs = map snd fields;
1487 val fields_moreTs = fieldTs @ [moreT];
1489 val alphas_zeta = alphas @ [zeta];
1491 val ext_binding = Binding.name (suffix extN base_name);
1492 val ext_name = suffix extN name;
1493 val ext_tyco = suffix ext_typeN name
1494 val extT = Type (ext_tyco, map TFree alphas_zeta);
1495 val ext_type = fields_moreTs ---> extT;
1498 (* the tree of new types that will back the record extension *)
1500 val mktreeV = Balanced_Tree.make Iso_Tuple_Support.mk_cons_tuple;
1502 fun mk_iso_tuple (left, right) (thy, i) =
1504 val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
1505 val ((_, cons), thy') = thy
1506 |> Iso_Tuple_Support.add_iso_tuple_type
1507 (Binding.suffix_name suff (Binding.name base_name), alphas_zeta)
1508 (fastype_of left, fastype_of right);
1510 (cons $ left $ right, (thy', i + 1))
1513 (*trying to create a 1-element iso_tuple will fail, and is pointless anyway*)
1514 fun mk_even_iso_tuple [arg] = pair arg
1515 | mk_even_iso_tuple args = mk_iso_tuple (Iso_Tuple_Support.dest_cons_tuple (mktreeV args));
1517 fun build_meta_tree_type i thy vars more =
1518 let val len = length vars in
1519 if len < 1 then raise TYPE ("meta_tree_type args too short", [], vars)
1520 else if len > 16 then
1523 | group16 xs = take 16 xs :: group16 (drop 16 xs);
1524 val vars' = group16 vars;
1525 val (composites, (thy', i')) = fold_map mk_even_iso_tuple vars' (thy, i);
1527 build_meta_tree_type i' thy' composites more
1530 let val (term, (thy', _)) = mk_iso_tuple (mktreeV vars, more) (thy, 0)
1534 val _ = timing_msg ctxt "record extension preparing definitions";
1537 (* 1st stage part 1: introduce the tree of new types *)
1539 val (ext_body, typ_thy) = timeit_msg ctxt "record extension nested type def:" (fn () =>
1540 build_meta_tree_type 1 thy vars more);
1543 (* prepare declarations and definitions *)
1545 (* 1st stage part 2: define the ext constant *)
1547 fun mk_ext args = list_comb (Const (ext_name, ext_type), args);
1548 val ext_spec = Logic.mk_equals (mk_ext (vars @ [more]), ext_body);
1550 val ([ext_def], defs_thy) = timeit_msg ctxt "record extension constructor def:" (fn () =>
1552 |> Sign.declare_const_global ((ext_binding, ext_type), NoSyn) |> snd
1553 |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]
1554 ||> Theory.checkpoint);
1557 (* prepare propositions *)
1559 val _ = timing_msg ctxt "record extension preparing propositions";
1560 val vars_more = vars @ [more];
1561 val variants = map (fn Free (x, _) => x) vars_more;
1562 val ext = mk_ext vars_more;
1563 val s = Free (rN, extT);
1564 val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT);
1566 val inject_prop = (* FIXME local x x' *)
1567 let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
1568 HOLogic.mk_conj (HOLogic.eq_const extT $
1569 mk_ext vars_more $ mk_ext vars_more', @{term True})
1571 foldr1 HOLogic.mk_conj
1572 (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [@{term True}])
1575 val induct_prop = (fold_rev Logic.all vars_more (Trueprop (P $ ext)), Trueprop (P $ s));
1577 val split_meta_prop = (* FIXME local P *)
1578 let val P = Free (singleton (Name.variant_list variants) "P", extT --> propT)
1579 in Logic.mk_equals (Logic.all s (P $ s), fold_rev Logic.all vars_more (P $ ext)) end;
1581 val inject = timeit_msg ctxt "record extension inject proof:" (fn () =>
1583 (Skip_Proof.prove_global defs_thy [] [] inject_prop
1585 simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
1587 (rtac @{thm refl_conj_eq} 1 ORELSE
1588 Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
1592 (*We need a surjection property r = (| f = f r, g = g r ... |)
1593 to prove other theorems. We haven't given names to the accessors
1594 f, g etc yet however, so we generate an ext structure with
1595 free variables as all arguments and allow the introduction tactic to
1596 operate on it as far as it can. We then use Drule.export_without_context
1597 to convert the free variables into unifiable variables and unify them with
1598 (roughly) the definition of the accessor.*)
1599 val surject = timeit_msg ctxt "record extension surjective proof:" (fn () =>
1601 val cterm_ext = cterm_of defs_thy ext;
1602 val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
1604 simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
1605 REPEAT_ALL_NEW Iso_Tuple_Support.iso_tuple_intros_tac 1;
1606 val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
1607 val [halfway] = Seq.list_of (tactic1 start);
1608 val [surject] = Seq.list_of (tactic2 (Drule.export_without_context halfway));
1613 val split_meta = timeit_msg ctxt "record extension split_meta proof:" (fn () =>
1614 Skip_Proof.prove_global defs_thy [] [] split_meta_prop
1617 [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
1618 etac @{thm meta_allE}, atac,
1619 rtac (@{thm prop_subst} OF [surject]),
1620 REPEAT o etac @{thm meta_allE}, atac]));
1622 val induct = timeit_msg ctxt "record extension induct proof:" (fn () =>
1623 let val (assm, concl) = induct_prop in
1624 Skip_Proof.prove_global defs_thy [] [assm] concl
1626 cut_tac (split_meta RS Drule.equal_elim_rule2) 1 THEN
1627 resolve_tac prems 2 THEN
1628 asm_simp_tac HOL_ss 1)
1631 val ([(_, [induct']), (_, [inject']), (_, [surjective']), (_, [split_meta'])], thm_thy) =
1633 |> Global_Theory.note_thmss ""
1634 [((Binding.name "ext_induct", []), [([induct], [])]),
1635 ((Binding.name "ext_inject", []), [([inject], [])]),
1636 ((Binding.name "ext_surjective", []), [([surject], [])]),
1637 ((Binding.name "ext_split", []), [([split_meta], [])])];
1639 (((ext_name, ext_type), (ext_tyco, alphas_zeta),
1640 extT, induct', inject', surjective', split_meta', ext_def), thm_thy)
1643 fun chunks [] [] = []
1644 | chunks [] xs = [xs]
1645 | chunks (l :: ls) xs = take l xs :: chunks ls (drop l xs);
1647 fun chop_last [] = error "chop_last: list should not be empty"
1648 | chop_last [x] = ([], x)
1649 | chop_last (x :: xs) = let val (tl, l) = chop_last xs in (x :: tl, l) end;
1651 fun subst_last _ [] = error "subst_last: list should not be empty"
1652 | subst_last s [_] = [s]
1653 | subst_last s (x :: xs) = x :: subst_last s xs;
1658 (*build up the record type from the current extension tpye extT and a list
1659 of parent extensions, starting with the root of the record hierarchy*)
1660 fun mk_recordT extT =
1661 fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT;
1664 (* code generation *)
1666 fun mk_random_eq tyco vs extN Ts =
1668 (* FIXME local i etc. *)
1669 val size = @{term "i::code_numeral"};
1670 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
1671 val T = Type (tyco, map TFree vs);
1672 val Tm = termifyT T;
1673 val params = Name.invent_names Name.context "x" Ts;
1674 val lhs = HOLogic.mk_random T size;
1675 val tc = HOLogic.mk_return Tm @{typ Random.seed}
1676 (HOLogic.mk_valtermify_app extN params T);
1680 ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params)
1681 tc @{typ Random.seed} (SOME Tm, @{typ Random.seed});
1686 fun mk_full_exhaustive_eq tyco vs extN Ts =
1688 (* FIXME local i etc. *)
1689 val size = @{term "i::code_numeral"};
1690 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
1691 val T = Type (tyco, map TFree vs);
1692 val test_function = Free ("f", termifyT T --> @{typ "(bool * term list) option"});
1693 val params = Name.invent_names Name.context "x" Ts;
1694 fun full_exhaustiveT T =
1695 (termifyT T --> @{typ "(bool * Code_Evaluation.term list) option"}) -->
1696 @{typ code_numeral} --> @{typ "(bool * Code_Evaluation.term list) option"};
1697 fun mk_full_exhaustive T =
1698 Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
1699 full_exhaustiveT T);
1700 val lhs = mk_full_exhaustive T $ test_function $ size;
1701 val tc = test_function $ (HOLogic.mk_valtermify_app extN params T);
1702 val rhs = fold_rev (fn (v, T) => fn cont =>
1703 mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc;
1708 fun instantiate_sort_record (sort, mk_eq) tyco vs extN Ts thy =
1710 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_eq tyco vs extN Ts));
1713 |> Class.instantiation ([tyco], vs, sort)
1714 |> `(fn lthy => Syntax.check_term lthy eq)
1715 |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
1717 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
1720 fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy =
1722 val algebra = Sign.classes_of thy;
1723 val has_inst = can (Sorts.mg_domain algebra ext_tyco) sort;
1725 if has_inst then thy
1727 (case Quickcheck_Common.perhaps_constrain thy (map (rpair sort) Ts) vs of
1729 instantiate_sort_record (sort, mk_eq) ext_tyco (map constrain vs) extN
1730 ((map o map_atyps) (fn TFree v => TFree (constrain v)) Ts) thy
1734 fun add_code ext_tyco vs extT ext simps inject thy =
1737 HOLogic.mk_Trueprop (HOLogic.mk_eq
1738 (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
1739 Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT)));
1741 Class.intro_classes_tac []
1742 THEN rewrite_goals_tac [Simpdata.mk_eq eq_def]
1743 THEN ALLGOALS (rtac @{thm refl});
1744 fun mk_eq thy eq_def =
1745 Simplifier.rewrite_rule
1746 [AxClass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
1747 fun mk_eq_refl thy =
1750 ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
1751 |> AxClass.unoverload thy;
1752 val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
1753 val ensure_exhaustive_record =
1754 ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
1757 |> Code.add_datatype [ext]
1758 |> fold Code.add_default_eqn simps
1759 |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
1760 |> `(fn lthy => Syntax.check_term lthy eq)
1761 |-> (fn eq => Specification.definition
1762 (NONE, (Attrib.empty_binding, eq)))
1763 |-> (fn (_, (_, eq_def)) =>
1764 Class.prove_instantiation_exit_result Morphism.thm
1765 (fn _ => fn eq_def => tac eq_def) eq_def)
1766 |-> (fn eq_def => fn thy =>
1767 thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
1768 |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
1769 |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
1770 |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
1776 fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
1778 val ctxt = Proof_Context.init_global thy;
1780 val prefix = Binding.name_of binding;
1781 val name = Sign.full_name thy binding;
1782 val full = Sign.full_name_path thy prefix;
1784 val bfields = map (fn (x, T, _) => (x, T)) raw_fields;
1785 val field_syntax = map #3 raw_fields;
1787 val parent_fields = maps #fields parents;
1788 val parent_chunks = map (length o #fields) parents;
1789 val parent_names = map fst parent_fields;
1790 val parent_types = map snd parent_fields;
1791 val parent_fields_len = length parent_fields;
1792 val parent_variants =
1793 Name.variant_list [moreN, rN, rN ^ "'", wN] (map Long_Name.base_name parent_names);
1794 val parent_vars = map2 (curry Free) parent_variants parent_types;
1795 val parent_len = length parents;
1797 val fields = map (apfst full) bfields;
1798 val names = map fst fields;
1799 val types = map snd fields;
1800 val alphas_fields = fold Term.add_tfreesT types [];
1801 val alphas_ext = inter (op =) alphas_fields alphas;
1802 val len = length fields;
1804 Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
1805 (map (Binding.name_of o fst) bfields);
1806 val vars = map2 (curry Free) variants types;
1807 val named_vars = names ~~ vars;
1808 val idxms = 0 upto len;
1810 val all_fields = parent_fields @ fields;
1811 val all_types = parent_types @ types;
1812 val all_variants = parent_variants @ variants;
1813 val all_vars = parent_vars @ vars;
1814 val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
1816 val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", HOLogic.typeS);
1817 val moreT = TFree zeta;
1818 val more = Free (moreN, moreT);
1819 val full_moreN = full (Binding.name moreN);
1820 val bfields_more = bfields @ [(Binding.name moreN, moreT)];
1821 val fields_more = fields @ [(full_moreN, moreT)];
1822 val named_vars_more = named_vars @ [(full_moreN, more)];
1823 val all_vars_more = all_vars @ [more];
1824 val all_named_vars_more = all_named_vars @ [(full_moreN, more)];
1827 (* 1st stage: ext_thy *)
1829 val extension_name = full binding;
1831 val ((ext, (ext_tyco, vs),
1832 extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
1834 |> Sign.qualified_path false binding
1835 |> extension_definition extension_name fields alphas_ext zeta moreT more vars;
1837 val _ = timing_msg ctxt "record preparing definitions";
1838 val Type extension_scheme = extT;
1839 val extension_name = unsuffix ext_typeN (fst extension_scheme);
1840 val extension = let val (n, Ts) = extension_scheme in (n, subst_last HOLogic.unitT Ts) end;
1841 val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extension_name];
1842 val extension_id = implode extension_names;
1844 fun rec_schemeT n = mk_recordT (map #extension (drop n parents)) extT;
1845 val rec_schemeT0 = rec_schemeT 0;
1848 let val (c, Ts) = extension in
1849 mk_recordT (map #extension (drop n parents))
1850 (Type (c, subst_last HOLogic.unitT Ts))
1856 val (args', more) = chop_last args;
1857 fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]);
1859 fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args')) more;
1861 if more = HOLogic.unit
1862 then build (map_range recT (parent_len + 1))
1863 else build (map_range rec_schemeT (parent_len + 1))
1866 val r_rec0 = mk_rec all_vars_more 0;
1867 val r_rec_unit0 = mk_rec (all_vars @ [HOLogic.unit]) 0;
1869 fun r n = Free (rN, rec_schemeT n);
1871 fun r_unit n = Free (rN, recT n);
1872 val r_unit0 = r_unit 0;
1873 val w = Free (wN, rec_schemeT 0);
1876 (* print translations *)
1878 val record_ext_type_abbr_tr's =
1880 val trname = hd extension_names;
1881 val last_ext = unsuffix ext_typeN (fst extension);
1882 in [record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0 trname] end;
1884 val record_ext_type_tr's =
1886 (*avoid conflict with record_type_abbr_tr's*)
1887 val trnames = if parent_len > 0 then [extension_name] else [];
1888 in map record_ext_type_tr' trnames end;
1890 val advanced_print_translation =
1891 map field_update_tr' (full_moreN :: names) @ [record_ext_tr' extension_name] @
1892 record_ext_type_tr's @ record_ext_type_abbr_tr's;
1895 (* prepare declarations *)
1897 val sel_decls = map (mk_selC rec_schemeT0 o apfst Binding.name_of) bfields_more;
1898 val upd_decls = map (mk_updC updateN rec_schemeT0 o apfst Binding.name_of) bfields_more;
1899 val make_decl = (makeN, all_types ---> recT0);
1900 val fields_decl = (fields_selN, types ---> Type extension);
1901 val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0);
1902 val truncate_decl = (truncateN, rec_schemeT0 --> recT0);
1905 (* prepare definitions *)
1907 val ext_defs = ext_def :: map #ext_def parents;
1909 (*Theorems from the iso_tuple intros.
1910 By unfolding ext_defs from r_rec0 we create a tree of constructor
1911 calls (many of them Pair, but others as well). The introduction
1912 rules for update_accessor_eq_assist can unify two different ways
1913 on these constructors. If we take the complete result sequence of
1914 running a the introduction tactic, we get one theorem for each upd/acc
1915 pair, from which we can derive the bodies of our selector and
1916 updator and their convs.*)
1917 val (accessor_thms, updator_thms, upd_acc_cong_assists) =
1918 timeit_msg ctxt "record getting tree access/updates:" (fn () =>
1922 (*pick variable indices of 1 to avoid possible variable
1923 collisions with existing variables in updacc_eq_triv*)
1924 fun to_Var (Free (c, T)) = Var ((c, 1), T);
1925 in mk_rec (map to_Var all_vars_more) 0 end;
1927 val cterm_rec = cterm_of ext_thy r_rec0;
1928 val cterm_vrs = cterm_of ext_thy r_rec0_Vars;
1929 val insts = [("v", cterm_rec), ("v'", cterm_vrs)];
1930 val init_thm = named_cterm_instantiate insts updacc_eq_triv;
1931 val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
1933 simp_tac (HOL_basic_ss addsimps ext_defs) 1 THEN
1934 REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE terminal);
1935 val updaccs = Seq.list_of (tactic init_thm);
1937 (updaccs RL [updacc_accessor_eqE],
1938 updaccs RL [updacc_updator_eqE],
1939 updaccs RL [updacc_cong_from_eq])
1942 fun lastN xs = drop parent_fields_len xs;
1945 fun mk_sel_spec ((c, T), thm) =
1947 val (acc $ arg, _) =
1948 HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (Thm.concl_of thm)));
1950 if arg aconv r_rec0 then ()
1951 else raise TERM ("mk_sel_spec: different arg", [arg]);
1953 Const (mk_selC rec_schemeT0 (c, T)) :== acc
1955 val sel_specs = map mk_sel_spec (fields_more ~~ lastN accessor_thms);
1958 fun mk_upd_spec ((c, T), thm) =
1960 val (upd $ _ $ arg, _) =
1961 HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (Thm.concl_of thm)));
1963 if arg aconv r_rec0 then ()
1964 else raise TERM ("mk_sel_spec: different arg", [arg]);
1965 in Const (mk_updC updateN rec_schemeT0 (c, T)) :== upd end;
1966 val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms);
1968 (*derived operations*)
1970 list_comb (Const (full (Binding.name makeN), all_types ---> recT0), all_vars) :==
1971 mk_rec (all_vars @ [HOLogic.unit]) 0;
1973 list_comb (Const (full (Binding.name fields_selN), types ---> Type extension), vars) :==
1974 mk_rec (all_vars @ [HOLogic.unit]) parent_len;
1976 Const (full (Binding.name extendN), recT0 --> moreT --> rec_schemeT0) $ r_unit0 $ more :==
1977 mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
1979 Const (full (Binding.name truncateN), rec_schemeT0 --> recT0) $ r0 :==
1980 mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
1983 (* 2st stage: defs_thy *)
1985 val (((sel_defs, upd_defs), derived_defs), defs_thy) =
1986 timeit_msg ctxt "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
1989 |> Sign.add_advanced_trfuns ([], [], advanced_print_translation, [])
1990 |> Sign.restore_naming thy
1991 |> Typedecl.abbrev_global (binding, map #1 alphas, NoSyn) recT0 |> snd
1992 |> Typedecl.abbrev_global
1993 (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0
1995 |> Sign.qualified_path false binding
1996 |> fold (fn ((x, T), mx) => snd o Sign.declare_const_global ((Binding.name x, T), mx))
1997 (sel_decls ~~ (field_syntax @ [NoSyn]))
1998 |> fold (fn (x, T) => snd o Sign.declare_const_global ((Binding.name x, T), NoSyn))
1999 (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
2000 |> (Global_Theory.add_defs false o
2001 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) sel_specs
2002 ||>> (Global_Theory.add_defs false o
2003 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) upd_specs
2004 ||>> (Global_Theory.add_defs false o
2005 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
2006 [make_spec, fields_spec, extend_spec, truncate_spec]
2007 ||> Theory.checkpoint);
2009 (* prepare propositions *)
2010 val _ = timing_msg ctxt "record preparing propositions";
2011 val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> HOLogic.boolT);
2012 val C = Free (singleton (Name.variant_list all_variants) "C", HOLogic.boolT);
2013 val P_unit = Free (singleton (Name.variant_list all_variants) "P", recT0 --> HOLogic.boolT);
2016 val sel_conv_props =
2017 map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more;
2020 fun mk_upd_prop i (c, T) =
2023 Free (singleton (Name.variant_list all_variants) (Long_Name.base_name c ^ "'"), T --> T);
2024 val n = parent_fields_len + i;
2025 val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more;
2026 in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
2027 val upd_conv_props = map2 mk_upd_prop idxms fields_more;
2030 val induct_scheme_prop =
2031 fold_rev Logic.all all_vars_more (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0);
2033 (fold_rev Logic.all all_vars (Trueprop (P_unit $ r_rec_unit0)), Trueprop (P_unit $ r_unit0));
2036 val surjective_prop =
2037 let val args = map (fn (c, Free (_, T)) => mk_sel r0 (c, T)) all_named_vars_more
2038 in r0 === mk_rec args 0 end;
2041 val cases_scheme_prop =
2042 (fold_rev Logic.all all_vars_more ((r0 === r_rec0) ==> Trueprop C), Trueprop C);
2045 fold_rev Logic.all all_vars ((r_unit0 === r_rec_unit0) ==> Trueprop C) ==> Trueprop C;
2048 val split_meta_prop =
2050 val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> propT);
2052 Logic.mk_equals (Logic.all r0 (P $ r0), fold_rev Logic.all all_vars_more (P $ r_rec0))
2055 val split_object_prop =
2056 let val ALL = fold_rev (fn (v, T) => fn t => HOLogic.mk_all (v, T, t))
2057 in ALL [dest_Free r0] (P $ r0) === ALL (map dest_Free all_vars_more) (P $ r_rec0) end;
2060 let val EX = fold_rev (fn (v, T) => fn t => HOLogic.mk_exists (v, T, t))
2061 in EX [dest_Free r0] (P $ r0) === EX (map dest_Free all_vars_more) (P $ r_rec0) end;
2066 val s' = Free (rN ^ "'", rec_schemeT0);
2067 fun mk_sel_eq (c, Free (_, T)) = mk_sel r0 (c, T) === mk_sel s' (c, T);
2068 val seleqs = map mk_sel_eq all_named_vars_more;
2069 in Logic.all r0 (Logic.all s' (Logic.list_implies (seleqs, r0 === s'))) end;
2072 (* 3rd stage: thms_thy *)
2074 val record_ss = get_simpset defs_thy;
2075 val sel_upd_ss = record_ss addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms);
2077 val (sel_convs, upd_convs) =
2078 timeit_msg ctxt "record sel_convs/upd_convs proof:" (fn () =>
2079 grouped 10 Par_List.map (fn prop =>
2080 Skip_Proof.prove_global defs_thy [] [] prop
2081 (K (ALLGOALS (asm_full_simp_tac sel_upd_ss)))) (sel_conv_props @ upd_conv_props))
2082 |> chop (length sel_conv_props);
2084 val (fold_congs, unfold_congs) = timeit_msg ctxt "record upd fold/unfold congs:" (fn () =>
2086 val symdefs = map Thm.symmetric (sel_defs @ upd_defs);
2087 val fold_ss = HOL_basic_ss addsimps symdefs;
2088 val ua_congs = map (Drule.export_without_context o simplify fold_ss) upd_acc_cong_assists;
2089 in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end);
2091 val parent_induct = Option.map #induct_scheme (try List.last parents);
2093 val induct_scheme = timeit_msg ctxt "record induct_scheme proof:" (fn () =>
2094 Skip_Proof.prove_global defs_thy [] [] induct_scheme_prop
2097 [case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
2098 try_param_tac rN ext_induct 1,
2099 asm_simp_tac HOL_basic_ss 1]));
2101 val induct = timeit_msg ctxt "record induct proof:" (fn () =>
2102 Skip_Proof.prove_global defs_thy [] [#1 induct_prop] (#2 induct_prop) (fn {prems, ...} =>
2103 try_param_tac rN induct_scheme 1
2104 THEN try_param_tac "more" @{thm unit.induct} 1
2105 THEN resolve_tac prems 1));
2107 val surjective = timeit_msg ctxt "record surjective proof:" (fn () =>
2110 get_sel_upd_defs defs_thy addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id});
2111 val init_ss = HOL_basic_ss addsimps ext_defs;
2113 Skip_Proof.prove_global defs_thy [] [] surjective_prop
2116 [rtac surject_assist_idE 1,
2119 (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
2120 (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
2123 val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" (fn () =>
2124 Skip_Proof.prove_global defs_thy [] [#1 cases_scheme_prop] (#2 cases_scheme_prop)
2126 resolve_tac prems 1 THEN
2127 rtac surjective 1));
2129 val cases = timeit_msg ctxt "record cases proof:" (fn () =>
2130 Skip_Proof.prove_global defs_thy [] [] cases_prop
2132 try_param_tac rN cases_scheme 1 THEN
2133 ALLGOALS (asm_full_simp_tac (HOL_basic_ss addsimps @{thms unit_all_eq1}))));
2135 val split_meta = timeit_msg ctxt "record split_meta proof:" (fn () =>
2136 Skip_Proof.prove_global defs_thy [] [] split_meta_prop
2139 [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
2140 etac @{thm meta_allE}, atac,
2141 rtac (@{thm prop_subst} OF [surjective]),
2142 REPEAT o etac @{thm meta_allE}, atac]));
2144 val split_object = timeit_msg ctxt "record split_object proof:" (fn () =>
2145 Skip_Proof.prove_global defs_thy [] [] split_object_prop
2147 rtac @{lemma "Trueprop A == Trueprop B ==> A = B" by (rule iffI) unfold} 1 THEN
2148 rewrite_goals_tac @{thms atomize_all [symmetric]} THEN
2149 rtac split_meta 1));
2151 val split_ex = timeit_msg ctxt "record split_ex proof:" (fn () =>
2152 Skip_Proof.prove_global defs_thy [] [] split_ex_prop
2155 (HOL_basic_ss addsimps
2156 (@{lemma "EX x. P x == ~ (ALL x. ~ P x)" by simp} ::
2157 @{thms not_not Not_eq_iff})) 1 THEN
2158 rtac split_object 1));
2160 val equality = timeit_msg ctxt "record equality proof:" (fn () =>
2161 Skip_Proof.prove_global defs_thy [] [] equality_prop
2162 (fn _ => asm_full_simp_tac (record_ss addsimps (split_meta :: sel_convs)) 1));
2164 val ([(_, sel_convs'), (_, upd_convs'), (_, sel_defs'), (_, upd_defs'),
2165 (_, fold_congs'), (_, unfold_congs'),
2166 (_, splits' as [split_meta', split_object', split_ex']), (_, derived_defs'),
2167 (_, [surjective']), (_, [equality']), (_, [induct_scheme']), (_, [induct']),
2168 (_, [cases_scheme']), (_, [cases'])], thms_thy) = defs_thy
2169 |> Global_Theory.note_thmss ""
2170 [((Binding.name "select_convs", []), [(sel_convs, [])]),
2171 ((Binding.name "update_convs", []), [(upd_convs, [])]),
2172 ((Binding.name "select_defs", []), [(sel_defs, [])]),
2173 ((Binding.name "update_defs", []), [(upd_defs, [])]),
2174 ((Binding.name "fold_congs", []), [(fold_congs, [])]),
2175 ((Binding.name "unfold_congs", []), [(unfold_congs, [])]),
2176 ((Binding.name "splits", []), [([split_meta, split_object, split_ex], [])]),
2177 ((Binding.name "defs", []), [(derived_defs, [])]),
2178 ((Binding.name "surjective", []), [([surjective], [])]),
2179 ((Binding.name "equality", []), [([equality], [])]),
2180 ((Binding.name "induct_scheme", induct_type_global (suffix schemeN name)),
2181 [([induct_scheme], [])]),
2182 ((Binding.name "induct", induct_type_global name), [([induct], [])]),
2183 ((Binding.name "cases_scheme", cases_type_global (suffix schemeN name)),
2184 [([cases_scheme], [])]),
2185 ((Binding.name "cases", cases_type_global name), [([cases], [])])];
2187 val sel_upd_simps = sel_convs' @ upd_convs';
2188 val sel_upd_defs = sel_defs' @ upd_defs';
2189 val depth = parent_len + 1;
2191 val ([(_, simps'), (_, iffs')], thms_thy') = thms_thy
2192 |> Global_Theory.note_thmss ""
2193 [((Binding.name "simps", [Simplifier.simp_add]), [(sel_upd_simps, [])]),
2194 ((Binding.name "iffs", [iff_add]), [([ext_inject], [])])];
2197 make_info alphas parent fields extension
2198 ext_induct ext_inject ext_surjective ext_split ext_def
2199 sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs'
2200 surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs';
2204 |> put_record name info
2205 |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs
2206 |> add_equalities extension_id equality'
2207 |> add_extinjects ext_inject
2208 |> add_extsplit extension_name ext_split
2209 |> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
2210 |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
2211 |> add_fieldext (extension_name, snd extension) names
2212 |> add_code ext_tyco vs extT ext simps' ext_inject
2213 |> Sign.restore_naming thy;
2222 fun read_parent NONE ctxt = (NONE, ctxt)
2223 | read_parent (SOME raw_T) ctxt =
2224 (case Proof_Context.read_typ_abbrev ctxt raw_T of
2225 Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt)
2226 | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));
2228 fun read_fields raw_fields ctxt =
2230 val Ts = Syntax.read_typs ctxt (map (fn (_, raw_T, _) => raw_T) raw_fields);
2231 val fields = map2 (fn (x, _, mx) => fn T => (x, T, mx)) raw_fields Ts;
2232 val ctxt' = fold Variable.declare_typ Ts ctxt;
2233 in (fields, ctxt') end;
2237 fun add_record (params, binding) raw_parent raw_fields thy =
2239 val _ = Theory.requires thy "Record" "record definitions";
2241 val ctxt = Proof_Context.init_global thy;
2242 fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T)
2243 handle TYPE (msg, _, _) => error msg;
2248 val parent = Option.map (apfst (map cert_typ)) raw_parent
2250 cat_error msg ("The error(s) above occurred in parent record specification");
2251 val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []);
2252 val parents = get_parent_info thy parent;
2255 raw_fields |> map (fn (x, raw_T, mx) => (x, cert_typ raw_T, mx)
2257 cat_error msg ("The error(s) above occurred in record field " ^ Binding.print x));
2262 val name = Sign.full_name thy binding;
2263 val err_dup_record =
2264 if is_none (get_info thy name) then []
2265 else ["Duplicate definition of record " ^ quote name];
2267 val spec_frees = fold Term.add_tfreesT (parent_args @ map #2 bfields) [];
2268 val err_extra_frees =
2269 (case subtract (op =) params spec_frees of
2271 | extras => ["Extra free type variable(s) " ^
2272 commas (map (Syntax.string_of_typ ctxt o TFree) extras)]);
2274 val err_no_fields = if null bfields then ["No fields present"] else [];
2276 val err_dup_fields =
2277 (case duplicates Binding.eq_name (map #1 bfields) of
2279 | dups => ["Duplicate field(s) " ^ commas (map Binding.print dups)]);
2281 val err_bad_fields =
2282 if forall (not_equal moreN o Binding.name_of o #1) bfields then []
2283 else ["Illegal field name " ^ quote moreN];
2286 err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields;
2287 val _ = if null errs then () else error (cat_lines errs);
2289 thy |> definition (params, binding) parent parents bfields
2291 handle ERROR msg => cat_error msg ("Failed to define record " ^ Binding.print binding);
2293 fun add_record_cmd (raw_params, binding) raw_parent raw_fields thy =
2295 val ctxt = Proof_Context.init_global thy;
2296 val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
2297 val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
2298 val (parent, ctxt2) = read_parent raw_parent ctxt1;
2299 val (fields, ctxt3) = read_fields raw_fields ctxt2;
2300 val params' = map (Proof_Context.check_tfree ctxt3) params;
2301 in thy |> add_record (params', binding) parent fields end;
2309 Sign.add_trfuns ([], parse_translation, [], []) #>
2310 Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #>
2311 Simplifier.map_simpset_global (fn ss => ss addsimprocs [simproc, upd_simproc, eq_simproc]);
2317 Outer_Syntax.command @{command_spec "record"} "define extensible record"
2318 (Parse.type_args_constrained -- Parse.binding --
2319 (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
2320 Scan.repeat1 Parse.const_binding)
2321 >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd x y z)));