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;
246 fun All xs t = Term.list_all_free (xs, t);
251 val op :== = Misc_Legacy.mk_defpair;
252 val op === = Trueprop o HOLogic.mk_eq;
253 val op ==> = Logic.mk_implies;
258 fun mk_ext (name, T) ts =
259 let val Ts = map fastype_of ts
260 in list_comb (Const (suffix extN name, Ts ---> T), ts) end;
265 fun mk_selC sT (c, T) = (c, sT --> T);
267 fun mk_sel s (c, T) =
268 let val sT = fastype_of s
269 in Const (mk_selC sT (c, T)) $ s end;
274 fun mk_updC sfx sT (c, T) = (suffix sfx c, (T --> T) --> sT --> sT);
276 fun mk_upd' sfx c v sT =
277 let val vT = domain_type (fastype_of v);
278 in Const (mk_updC sfx sT (c, vT)) $ v end;
280 fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s;
285 fun dest_recT (typ as Type (c_ext_type, Ts as (_ :: _))) =
286 (case try (unsuffix ext_typeN) c_ext_type of
287 NONE => raise TYPE ("Record.dest_recT", [typ], [])
288 | SOME c => ((c, Ts), List.last Ts))
289 | dest_recT typ = raise TYPE ("Record.dest_recT", [typ], []);
291 val is_recT = can dest_recT;
294 let val ((c, Ts), U) = dest_recT T
295 in (c, Ts) :: dest_recTs U
296 end handle TYPE _ => [];
299 let val ((c, Ts), U) = dest_recT T in
303 end handle TYPE _ => NONE;
307 val rTs = dest_recTs T;
308 val rTs' = if i < 0 then rTs else take i rTs;
309 in implode (map #1 rTs') end;
313 (*** extend theory by record definition ***)
317 (* type info and parent_info *)
320 {args: (string * sort) list,
321 parent: (typ list * string) option,
322 fields: (string * typ) list,
323 extension: (string * typ list),
331 select_convs: thm list,
332 update_convs: thm list,
333 select_defs: thm list,
334 update_defs: thm list,
335 fold_congs: thm list,
336 unfold_congs: thm list,
350 fun make_info args parent fields extension
351 ext_induct ext_inject ext_surjective ext_split ext_def
352 select_convs update_convs select_defs update_defs fold_congs unfold_congs splits defs
353 surjective equality induct_scheme induct cases_scheme cases
355 {args = args, parent = parent, fields = fields, extension = extension,
356 ext_induct = ext_induct, ext_inject = ext_inject, ext_surjective = ext_surjective,
357 ext_split = ext_split, ext_def = ext_def, select_convs = select_convs,
358 update_convs = update_convs, select_defs = select_defs, update_defs = update_defs,
359 fold_congs = fold_congs, unfold_congs = unfold_congs, splits = splits, defs = defs,
360 surjective = surjective, equality = equality, induct_scheme = induct_scheme,
361 induct = induct, cases_scheme = cases_scheme, cases = cases, simps = simps, iffs = iffs};
365 fields: (string * typ) list,
366 extension: (string * typ list),
370 fun make_parent_info name fields extension ext_def induct_scheme : parent_info =
371 {name = name, fields = fields, extension = extension,
372 ext_def = ext_def, induct_scheme = induct_scheme};
378 {records: info Symtab.table,
380 {selectors: (int * bool) Symtab.table,
381 updates: string Symtab.table,
382 simpset: Simplifier.simpset,
383 defset: Simplifier.simpset,
384 foldcong: Simplifier.simpset,
385 unfoldcong: Simplifier.simpset},
386 equalities: thm Symtab.table,
387 extinjects: thm list,
388 extsplit: thm Symtab.table, (*maps extension name to split rule*)
389 splits: (thm * thm * thm * thm) Symtab.table, (*!!, ALL, EX - split-equalities, induct rule*)
390 extfields: (string * typ) list Symtab.table, (*maps extension to its fields*)
391 fieldext: (string * typ list) Symtab.table}; (*maps field to its extension*)
394 records sel_upd equalities extinjects extsplit splits extfields fieldext =
395 {records = records, sel_upd = sel_upd,
396 equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
397 extfields = extfields, fieldext = fieldext }: data;
399 structure Data = Theory_Data
403 make_data Symtab.empty
404 {selectors = Symtab.empty, updates = Symtab.empty,
405 simpset = HOL_basic_ss, defset = HOL_basic_ss,
406 foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
407 Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
412 {selectors = sels1, updates = upds1,
413 simpset = ss1, defset = ds1,
414 foldcong = fc1, unfoldcong = uc1},
415 equalities = equalities1,
416 extinjects = extinjects1,
417 extsplit = extsplit1,
419 extfields = extfields1,
420 fieldext = fieldext1},
423 {selectors = sels2, updates = upds2,
424 simpset = ss2, defset = ds2,
425 foldcong = fc2, unfoldcong = uc2},
426 equalities = equalities2,
427 extinjects = extinjects2,
428 extsplit = extsplit2,
430 extfields = extfields2,
431 fieldext = fieldext2}) =
433 (Symtab.merge (K true) (recs1, recs2))
434 {selectors = Symtab.merge (K true) (sels1, sels2),
435 updates = Symtab.merge (K true) (upds1, upds2),
436 simpset = Simplifier.merge_ss (ss1, ss2),
437 defset = Simplifier.merge_ss (ds1, ds2),
438 foldcong = Simplifier.merge_ss (fc1, fc2),
439 unfoldcong = Simplifier.merge_ss (uc1, uc2)}
440 (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
441 (Thm.merge_thms (extinjects1, extinjects2))
442 (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
443 (Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
444 Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
445 Thm.eq_thm (c, y) andalso Thm.eq_thm (d, z)) (splits1, splits2))
446 (Symtab.merge (K true) (extfields1, extfields2))
447 (Symtab.merge (K true) (fieldext1, fieldext2));
451 (* access 'records' *)
453 val get_info = Symtab.lookup o #records o Data.get;
455 fun the_info thy name =
456 (case get_info thy name of
458 | NONE => error ("Unknown record type " ^ quote name));
460 fun put_record name info =
461 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
462 make_data (Symtab.update (name, info) records)
463 sel_upd equalities extinjects extsplit splits extfields fieldext);
466 (* access 'sel_upd' *)
468 val get_sel_upd = #sel_upd o Data.get;
470 val is_selector = Symtab.defined o #selectors o get_sel_upd;
471 val get_updates = Symtab.lookup o #updates o get_sel_upd;
472 fun get_ss_with_context getss thy = Simplifier.global_context thy (getss (get_sel_upd thy));
474 val get_simpset = get_ss_with_context #simpset;
475 val get_sel_upd_defs = get_ss_with_context #defset;
477 fun get_update_details u thy =
478 let val sel_upd = get_sel_upd thy in
479 (case Symtab.lookup (#updates sel_upd) u of
481 let val SOME (dep, ismore) = Symtab.lookup (#selectors sel_upd) s
482 in SOME (s, dep, ismore) end
486 fun put_sel_upd names more depth simps defs (folds, unfolds) thy =
488 val all = names @ [more];
489 val sels = map (rpair (depth, false)) names @ [(more, (depth, true))];
490 val upds = map (suffix updateN) all ~~ all;
492 val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong},
493 equalities, extinjects, extsplit, splits, extfields, fieldext} = Data.get thy;
494 val data = make_data records
495 {selectors = fold Symtab.update_new sels selectors,
496 updates = fold Symtab.update_new upds updates,
497 simpset = Simplifier.addsimps (simpset, simps),
498 defset = Simplifier.addsimps (defset, defs),
499 foldcong = foldcong |> fold Simplifier.add_cong folds,
500 unfoldcong = unfoldcong |> fold Simplifier.add_cong unfolds}
501 equalities extinjects extsplit splits extfields fieldext;
502 in Data.put data thy end;
505 (* access 'equalities' *)
507 fun add_equalities name thm =
508 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
509 make_data records sel_upd
510 (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext);
512 val get_equalities = Symtab.lookup o #equalities o Data.get;
515 (* access 'extinjects' *)
517 fun add_extinjects thm =
518 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
519 make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
520 extsplit splits extfields fieldext);
522 val get_extinjects = rev o #extinjects o Data.get;
525 (* access 'extsplit' *)
527 fun add_extsplit name thm =
528 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
529 make_data records sel_upd equalities extinjects
530 (Symtab.update_new (name, thm) extsplit) splits extfields fieldext);
533 (* access 'splits' *)
535 fun add_splits name thmP =
536 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
537 make_data records sel_upd equalities extinjects extsplit
538 (Symtab.update_new (name, thmP) splits) extfields fieldext);
540 val get_splits = Symtab.lookup o #splits o Data.get;
543 (* parent/extension of named record *)
545 val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o Data.get);
546 val get_extension = Option.map #extension oo (Symtab.lookup o #records o Data.get);
549 (* access 'extfields' *)
551 fun add_extfields name fields =
552 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
553 make_data records sel_upd equalities extinjects extsplit splits
554 (Symtab.update_new (name, fields) extfields) fieldext);
556 val get_extfields = Symtab.lookup o #extfields o Data.get;
558 fun get_extT_fields thy T =
560 val ((name, Ts), moreT) = dest_recT T;
562 let val (nm :: _ :: rst) = rev (Long_Name.explode name) (* FIXME !? *)
563 in Long_Name.implode (rev (nm :: rst)) end;
564 val varifyT = varifyT (maxidx_of_typs (moreT :: Ts) + 1);
565 val {records, extfields, ...} = Data.get thy;
566 val (fields, (more, _)) = split_last (Symtab.lookup_list extfields name);
567 val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
569 val subst = fold (Sign.typ_match thy) (#1 (split_last args) ~~ #1 (split_last Ts)) Vartab.empty;
570 val fields' = map (apsnd (Envir.norm_type subst o varifyT)) fields;
571 in (fields', (more, moreT)) end;
573 fun get_recT_fields thy T =
575 val (root_fields, (root_more, root_moreT)) = get_extT_fields thy T;
576 val (rest_fields, rest_more) =
577 if is_recT root_moreT then get_recT_fields thy root_moreT
578 else ([], (root_more, root_moreT));
579 in (root_fields @ rest_fields, rest_more) end;
582 (* access 'fieldext' *)
584 fun add_fieldext extname_types fields =
585 Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
588 fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
589 in make_data records sel_upd equalities extinjects extsplit splits extfields fieldext' end);
591 val get_fieldext = Symtab.lookup o #fieldext o Data.get;
598 fun add_parents _ NONE = I
599 | add_parents thy (SOME (types, name)) =
601 fun err msg = error (msg ^ " parent record " ^ quote name);
603 val {args, parent, ...} =
604 (case get_info thy name of SOME info => info | NONE => err "Unknown");
605 val _ = if length types <> length args then err "Bad number of arguments for" else ();
607 fun bad_inst ((x, S), T) =
608 if Sign.of_sort thy (T, S) then NONE else SOME x
609 val bads = map_filter bad_inst (args ~~ types);
610 val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");
612 val inst = args ~~ types;
613 val subst = Term.map_type_tfree (the o AList.lookup (op =) inst);
614 val parent' = Option.map (apfst (map subst)) parent;
615 in cons (name, inst) #> add_parents thy parent' end;
619 fun get_hierarchy thy (name, types) = add_parents thy (SOME (types, name)) [];
621 fun get_parent_info thy parent =
622 add_parents thy parent [] |> map (fn (name, inst) =>
624 val subst = Term.map_type_tfree (the o AList.lookup (op =) inst);
625 val {fields, extension, induct_scheme, ext_def, ...} = the_info thy name;
626 val fields' = map (apsnd subst) fields;
627 val extension' = apsnd (map subst) extension;
628 in make_parent_info name fields' extension' ext_def induct_scheme end);
634 (** concrete syntax for records **)
636 (* parse translations *)
640 fun split_args (field :: fields) ((name, arg) :: fargs) =
641 if can (unsuffix name) field then
642 let val (args, rest) = split_args fields fargs
643 in (arg :: args, rest) end
644 else raise Fail ("expecting field " ^ quote field ^ " but got " ^ quote name)
645 | split_args [] (fargs as (_ :: _)) = ([], fargs)
646 | split_args (_ :: _) [] = raise Fail "expecting more fields"
647 | split_args _ _ = ([], []);
649 fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) =
651 | field_type_tr t = raise TERM ("field_type_tr", [t]);
653 fun field_types_tr (Const (@{syntax_const "_field_types"}, _) $ t $ u) =
654 field_type_tr t :: field_types_tr u
655 | field_types_tr t = [field_type_tr t];
657 fun record_field_types_tr more ctxt t =
659 val thy = Proof_Context.theory_of ctxt;
660 fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]);
662 fun mk_ext (fargs as (name, _) :: _) =
663 (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
664 SOME (ext, alphas) =>
665 (case get_extfields thy ext of
668 val (fields', _) = split_last fields;
669 val types = map snd fields';
670 val (args, rest) = split_args (map fst fields') fargs
671 handle Fail msg => err msg;
672 val argtypes = Syntax.check_typs ctxt (map Syntax_Phases.decode_typ args);
673 val varifyT = varifyT (fold Term.maxidx_typ argtypes ~1 + 1);
674 val vartypes = map varifyT types;
676 val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
677 handle Type.TYPE_MATCH => err "type is no proper record (extension)";
679 map (Syntax_Phases.term_of_typ ctxt o Envir.norm_type subst o varifyT)
680 (#1 (split_last alphas));
682 val more' = mk_ext rest;
685 (Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
687 | NONE => err ("no fields defined for " ^ quote ext))
688 | NONE => err (quote name ^ " is no proper field"))
691 mk_ext (field_types_tr t)
694 fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const @{type_syntax unit}) ctxt t
695 | record_type_tr _ ts = raise TERM ("record_type_tr", ts);
697 fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t
698 | record_type_scheme_tr _ ts = raise TERM ("record_type_scheme_tr", ts);
701 fun field_tr ((Const (@{syntax_const "_field"}, _) $ Const (name, _) $ arg)) = (name, arg)
702 | field_tr t = raise TERM ("field_tr", [t]);
704 fun fields_tr (Const (@{syntax_const "_fields"}, _) $ t $ u) = field_tr t :: fields_tr u
705 | fields_tr t = [field_tr t];
707 fun record_fields_tr more ctxt t =
709 val thy = Proof_Context.theory_of ctxt;
710 fun err msg = raise TERM ("Error in record input: " ^ msg, [t]);
712 fun mk_ext (fargs as (name, _) :: _) =
713 (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
715 (case get_extfields thy ext of
718 val (args, rest) = split_args (map fst (fst (split_last fields))) fargs
719 handle Fail msg => err msg;
720 val more' = mk_ext rest;
721 in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end
722 | NONE => err ("no fields defined for " ^ quote ext))
723 | NONE => err (quote name ^ " is no proper field"))
725 in mk_ext (fields_tr t) end;
727 fun record_tr ctxt [t] = record_fields_tr (Syntax.const @{const_syntax Unity}) ctxt t
728 | record_tr _ ts = raise TERM ("record_tr", ts);
730 fun record_scheme_tr ctxt [t, more] = record_fields_tr more ctxt t
731 | record_scheme_tr _ ts = raise TERM ("record_scheme_tr", ts);
734 fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) =
735 Syntax.const (suffix updateN name) $ Abs (Name.uu_, dummyT, arg)
736 | field_update_tr t = raise TERM ("field_update_tr", [t]);
738 fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) =
739 field_update_tr t :: field_updates_tr u
740 | field_updates_tr t = [field_update_tr t];
742 fun record_update_tr [t, u] = fold (curry op $) (field_updates_tr u) t
743 | record_update_tr ts = raise TERM ("record_update_tr", ts);
747 val parse_translation =
748 [(@{syntax_const "_record_update"}, record_update_tr)];
750 val advanced_parse_translation =
751 [(@{syntax_const "_record"}, record_tr),
752 (@{syntax_const "_record_scheme"}, record_scheme_tr),
753 (@{syntax_const "_record_type"}, record_type_tr),
754 (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)];
759 (* print translations *)
761 val type_abbr = Attrib.setup_config_bool @{binding record_type_abbr} (K true);
762 val type_as_fields = Attrib.setup_config_bool @{binding record_type_as_fields} (K true);
767 (* FIXME early extern (!??) *)
768 (* FIXME Syntax.free (??) *)
769 fun field_type_tr' (c, t) = Syntax.const @{syntax_const "_field_type"} $ Syntax.const c $ t;
771 fun field_types_tr' (t, u) = Syntax.const @{syntax_const "_field_types"} $ t $ u;
773 fun record_type_tr' ctxt t =
775 val thy = Proof_Context.theory_of ctxt;
777 val T = Syntax_Phases.decode_typ t;
778 val varifyT = varifyT (Term.maxidx_of_typ T + 1);
782 Type (ext, args as _ :: _) =>
783 (case try (unsuffix ext_typeN) ext of
785 (case get_extfields thy ext' of
786 SOME (fields as (x, _) :: _) =>
787 (case get_fieldext thy x of
790 val (f :: fs, _) = split_last fields;
792 apfst (Proof_Context.extern_const ctxt) f ::
793 map (apfst Long_Name.base_name) fs;
794 val (args', more) = split_last args;
795 val alphavars = map varifyT (#1 (split_last alphas));
796 val subst = Type.raw_matches (alphavars, args') Vartab.empty;
797 val fields'' = (map o apsnd) (Envir.norm_type subst o varifyT) fields';
798 in fields'' @ strip_fields more end
799 handle Type.TYPE_MATCH => [("", T)])
805 val (fields, (_, moreT)) = split_last (strip_fields T);
806 val _ = null fields andalso raise Match;
808 foldr1 field_types_tr'
809 (map (field_type_tr' o apsnd (Syntax_Phases.term_of_typ ctxt)) fields);
811 if not (Config.get ctxt type_as_fields) orelse null fields then raise Match
812 else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
814 Syntax.const @{syntax_const "_record_type_scheme"} $ u $
815 Syntax_Phases.term_of_typ ctxt moreT
818 (*try to reconstruct the record name type abbreviation from
819 the (nested) extension types*)
820 fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm =
822 val T = Syntax_Phases.decode_typ tm;
823 val varifyT = varifyT (maxidx_of_typ T + 1);
825 fun mk_type_abbr subst name args =
826 let val abbrT = Type (name, map (varifyT o TFree) args)
827 in Syntax_Phases.term_of_typ ctxt (Envir.norm_type subst abbrT) end;
829 fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
831 if Config.get ctxt type_abbr then
834 if name = last_ext then
835 let val subst = match schemeT T in
836 if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree zeta)))
837 then mk_type_abbr subst abbr alphas
838 else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
839 end handle Type.TYPE_MATCH => record_type_tr' ctxt tm
840 else raise Match (*give print translation of specialised record a chance*)
842 else record_type_tr' ctxt tm
847 fun record_ext_type_tr' name =
849 val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);
851 record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts));
852 in (ext_type_name, tr') end;
854 fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
856 val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);
858 record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt
859 (list_comb (Syntax.const ext_type_name, ts));
860 in (ext_type_name, tr') end;
867 (* FIXME Syntax.free (??) *)
868 fun field_tr' (c, t) = Syntax.const @{syntax_const "_field"} $ Syntax.const c $ t;
869 fun fields_tr' (t, u) = Syntax.const @{syntax_const "_fields"} $ t $ u;
871 fun record_tr' ctxt t =
873 val thy = Proof_Context.theory_of ctxt;
876 (case strip_comb t of
877 (Const (ext, _), args as (_ :: _)) =>
878 (case try (Lexicon.unmark_const o unsuffix extN) ext of
880 (case get_extfields thy ext' of
883 val (f :: fs, _) = split_last (map fst fields);
884 val fields' = Proof_Context.extern_const ctxt f :: map Long_Name.base_name fs;
885 val (args', more) = split_last args;
886 in (fields' ~~ args') @ strip_fields more end
887 handle ListPair.UnequalLengths => [("", t)])
892 val (fields, (_, more)) = split_last (strip_fields t);
893 val _ = null fields andalso raise Match;
894 val u = foldr1 fields_tr' (map field_tr' fields);
897 Const (@{const_syntax Unity}, _) => Syntax.const @{syntax_const "_record"} $ u
898 | _ => Syntax.const @{syntax_const "_record_scheme"} $ u $ more
903 fun record_ext_tr' name =
905 val ext_name = Lexicon.mark_const (name ^ extN);
906 fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));
907 in (ext_name, tr') end;
914 fun dest_update ctxt c =
915 (case try Lexicon.unmark_const c of
916 SOME d => try (unsuffix updateN) (Proof_Context.extern_const ctxt d)
919 fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
920 (case dest_update ctxt c of
922 (case try Syntax_Trans.const_abs_tr' k of
924 apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
925 (field_updates_tr' ctxt u)
928 | field_updates_tr' _ tm = ([], tm);
930 fun record_update_tr' ctxt tm =
931 (case field_updates_tr' ctxt tm of
932 ([], _) => raise Match
934 Syntax.const @{syntax_const "_record_update"} $ u $
935 foldr1 (fn (v, w) => Syntax.const @{syntax_const "_field_updates"} $ v $ w) (rev ts));
939 fun field_update_tr' name =
941 val update_name = Lexicon.mark_const (name ^ updateN);
942 fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u)
943 | tr' _ _ = raise Match;
944 in (update_name, tr') end;
950 (** record simprocs **)
952 fun future_forward_prf_standard thy prf prop () =
954 if ! quick_and_dirty then Skip_Proof.make_thm thy prop
955 else if Goal.future_enabled () then
956 Goal.future_result (Proof_Context.init_global thy) (Goal.fork prf) prop
958 in Drule.export_without_context thm end;
960 fun prove_common immediate stndrd thy asms prop tac =
963 if ! quick_and_dirty then Skip_Proof.prove
964 else if immediate orelse not (Goal.future_enabled ()) then Goal.prove
965 else Goal.prove_future;
966 val prf = prv (Proof_Context.init_global thy) [] asms prop tac;
967 in if stndrd then Drule.export_without_context prf else prf end;
969 val prove_future_global = prove_common false;
970 val prove_global = prove_common true;
972 fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) =
973 (case get_updates thy u of
974 SOME u_name => u_name = s
975 | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));
978 let val T = range_type (fastype_of f)
979 in HOLogic.mk_comp (Const (@{const_name Fun.id}, T --> T), f) end;
981 fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
982 | get_upd_funs _ = [];
984 fun get_accupd_simps thy term defset =
986 val (acc, [body]) = strip_comb term;
987 val upd_funs = sort_distinct Term_Ord.fast_term_ord (get_upd_funs body);
990 (* FIXME fresh "f" (!?) *)
991 val T = domain_type (fastype_of upd);
992 val lhs = HOLogic.mk_comp (acc, upd $ Free ("f", T));
994 if is_sel_upd_pair thy acc upd
995 then HOLogic.mk_comp (Free ("f", T), acc)
997 val prop = lhs === rhs;
999 Goal.prove (Proof_Context.init_global thy) [] [] prop
1001 simp_tac defset 1 THEN
1002 REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
1003 TRY (simp_tac (HOL_ss addsimps @{thms id_apply id_o o_id}) 1));
1005 if is_sel_upd_pair thy acc upd
1006 then @{thm o_eq_dest}
1007 else @{thm o_eq_id_dest};
1008 in Drule.export_without_context (othm RS dest) end;
1009 in map get_simp upd_funs end;
1011 fun get_updupd_simp thy defset u u' comp =
1013 (* FIXME fresh "f" (!?) *)
1014 val f = Free ("f", domain_type (fastype_of u));
1015 val f' = Free ("f'", domain_type (fastype_of u'));
1016 val lhs = HOLogic.mk_comp (u $ f, u' $ f');
1019 then u $ HOLogic.mk_comp (f, f')
1020 else HOLogic.mk_comp (u' $ f', u $ f);
1021 val prop = lhs === rhs;
1023 Goal.prove (Proof_Context.init_global thy) [] [] prop
1025 simp_tac defset 1 THEN
1026 REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
1027 TRY (simp_tac (HOL_ss addsimps @{thms id_apply}) 1));
1028 val dest = if comp then @{thm o_eq_dest_lhs} else @{thm o_eq_dest};
1029 in Drule.export_without_context (othm RS dest) end;
1031 fun get_updupd_simps thy term defset =
1033 val upd_funs = get_upd_funs term;
1034 val cname = fst o dest_Const;
1035 fun getswap u u' = get_updupd_simp thy defset u u' (cname u = cname u');
1036 fun build_swaps_to_eq _ [] swaps = swaps
1037 | build_swaps_to_eq upd (u :: us) swaps =
1039 val key = (cname u, cname upd);
1041 if Symreltab.defined swaps key then swaps
1042 else Symreltab.insert (K true) (key, getswap u upd) swaps;
1044 if cname u = cname upd then newswaps
1045 else build_swaps_to_eq upd us newswaps
1047 fun swaps_needed [] _ _ swaps = map snd (Symreltab.dest swaps)
1048 | swaps_needed (u :: us) prev seen swaps =
1049 if Symtab.defined seen (cname u)
1050 then swaps_needed us prev seen (build_swaps_to_eq u prev swaps)
1051 else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps;
1052 in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end;
1054 val named_cterm_instantiate = Iso_Tuple_Support.named_cterm_instantiate;
1056 fun prove_unfold_defs thy ex_simps ex_simprs prop =
1058 val defset = get_sel_upd_defs thy;
1059 val prop' = Envir.beta_eta_contract prop;
1060 val (lhs, _) = Logic.dest_equals (Logic.strip_assums_concl prop');
1061 val (_, args) = strip_comb lhs;
1062 val simps = (if length args = 1 then get_accupd_simps else get_updupd_simps) thy lhs defset;
1064 Goal.prove (Proof_Context.init_global thy) [] [] prop'
1066 simp_tac (HOL_basic_ss addsimps (simps @ @{thms K_record_comp})) 1 THEN
1067 TRY (simp_tac (HOL_basic_ss addsimps ex_simps addsimprocs ex_simprs) 1))
1073 fun eq (s1: string) (s2: string) = (s1 = s2);
1075 fun has_field extfields f T =
1076 exists (fn (eN, _) => exists (eq f o fst) (Symtab.lookup_list extfields eN)) (dest_recTs T);
1078 fun K_skeleton n (T as Type (_, [_, kT])) (b as Bound i) (Abs (x, xT, t)) =
1079 if null (loose_bnos t) then ((n, kT), (Abs (x, xT, Bound (i + 1)))) else ((n, T), b)
1080 | K_skeleton n T b _ = ((n, T), b);
1087 Simplify selections of an record update:
1088 (1) S (S_update k r) = k (S r)
1089 (2) S (X_update k r) = S r
1091 The simproc skips multiple updates at once, eg:
1092 S (X_update x (Y_update y (S_update k r))) = k (S r)
1094 But be careful in (2) because of the extensibility of records.
1095 - If S is a more-selector we have to make sure that the update on component
1096 X does not affect the selected subrecord.
1097 - If X is a more-selector we have to make sure that S is not in the updated
1101 Simplifier.simproc_global @{theory HOL} "record_simp" ["x"]
1102 (fn thy => fn _ => fn t =>
1104 (sel as Const (s, Type (_, [_, rangeS]))) $
1105 ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
1106 if is_selector thy s andalso is_some (get_updates thy u) then
1108 val {sel_upd = {updates, ...}, extfields, ...} = Data.get thy;
1110 fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
1111 (case Symtab.lookup updates u of
1115 (case mk_eq_terms r of
1120 val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
1121 in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end
1122 | SOME (trm, trm', vars) =>
1124 val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k;
1125 in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end)
1126 else if has_field extfields u_name rangeS orelse
1127 has_field extfields s (domain_type kT) then NONE
1129 (case mk_eq_terms r of
1130 SOME (trm, trm', vars) =>
1131 let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k
1132 in SOME (upd $ kb $ trm, trm', kv :: vars) end
1137 val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
1138 in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end))
1139 | mk_eq_terms _ = NONE;
1141 (case mk_eq_terms (upd $ k $ r) of
1142 SOME (trm, trm', vars) =>
1144 (prove_unfold_defs thy [] []
1145 (list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
1151 fun get_upd_acc_cong_thm upd acc thy simpset =
1153 val insts = [("upd", cterm_of thy upd), ("ac", cterm_of thy acc)];
1154 val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv);
1156 Goal.prove (Proof_Context.init_global thy) [] [] prop
1158 simp_tac simpset 1 THEN
1159 REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
1160 TRY (resolve_tac [updacc_cong_idI] 1))
1166 (*Simplify multiple updates:
1167 (1) "N_update y (M_update g (N_update x (M_update f r))) =
1168 (N_update (y o x) (M_update (g o f) r))"
1169 (2) "r(|M:= M r|) = r"
1171 In both cases "more" updates complicate matters: for this reason
1172 we omit considering further updates if doing so would introduce
1173 both a more update and an update to a field within it.*)
1175 Simplifier.simproc_global @{theory HOL} "record_upd_simp" ["x"]
1176 (fn thy => fn _ => fn t =>
1178 (*We can use more-updators with other updators as long
1179 as none of the other updators go deeper than any more
1180 updator. min here is the depth of the deepest other
1181 updator, max the depth of the shallowest more updator.*)
1182 fun include_depth (dep, true) (min, max) =
1184 then SOME (min, if dep <= max orelse max = ~1 then dep else max)
1186 | include_depth (dep, false) (min, max) =
1187 if dep <= max orelse max = ~1
1188 then SOME (if min <= dep then dep else min, max)
1191 fun getupdseq (term as (upd as Const (u, _)) $ f $ tm) min max =
1192 (case get_update_details u thy of
1193 SOME (s, dep, ismore) =>
1194 (case include_depth (dep, ismore) (min, max) of
1195 SOME (min', max') =>
1196 let val (us, bs, _) = getupdseq tm min' max'
1197 in ((upd, s, f) :: us, bs, fastype_of term) end
1198 | NONE => ([], term, HOLogic.unitT))
1199 | NONE => ([], term, HOLogic.unitT))
1200 | getupdseq term _ _ = ([], term, HOLogic.unitT);
1202 val (upds, base, baseT) = getupdseq t 0 ~1;
1204 fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm =
1205 if s = s' andalso null (loose_bnos tm')
1206 andalso subst_bound (HOLogic.unit, tm') = tm
1207 then (true, Abs (n, T, Const (s', T') $ Bound 1))
1208 else (false, HOLogic.unit)
1209 | is_upd_noop _ _ _ = (false, HOLogic.unit);
1211 fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) =
1213 val ss = get_sel_upd_defs thy;
1214 val uathm = get_upd_acc_cong_thm upd acc thy ss;
1216 [Drule.export_without_context (uathm RS updacc_noopE),
1217 Drule.export_without_context (uathm RS updacc_noop_compE)]
1220 (*If f is constant then (f o g) = f. We know that K_skeleton
1221 only returns constant abstractions thus when we see an
1222 abstraction we can discard inner updates.*)
1223 fun add_upd (f as Abs _) fs = [f]
1224 | add_upd f fs = (f :: fs);
1226 (*mk_updterm returns
1227 (orig-term-skeleton, simplified-skeleton,
1228 variables, duplicate-updates, simp-flag, noop-simps)
1230 where duplicate-updates is a table used to pass upward
1231 the list of update functions which can be composed
1232 into an update above them, simp-flag indicates whether
1233 any simplification was achieved, and noop-simps are
1234 used for eliminating case (2) defined above*)
1235 fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term =
1237 val (lhs, rhs, vars, dups, simp, noops) =
1238 mk_updterm upds (Symtab.update (u, ()) above) term;
1240 K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f;
1241 val (isnoop, skelf') = is_upd_noop s f term;
1242 val funT = domain_type T;
1243 fun mk_comp_local (f, f') =
1244 Const (@{const_name Fun.comp}, funT --> funT --> funT) $ f $ f';
1247 (upd $ skelf' $ lhs, rhs, vars,
1248 Symtab.update (u, []) dups, true,
1249 if Symtab.defined noops u then noops
1250 else Symtab.update (u, get_noop_simps upd skelf') noops)
1251 else if Symtab.defined above u then
1252 (upd $ skelf $ lhs, rhs, fvar :: vars,
1253 Symtab.map_default (u, []) (add_upd skelf) dups,
1256 (case Symtab.lookup dups u of
1259 upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs,
1260 fvar :: vars, dups, true, noops)
1261 | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops))
1263 | mk_updterm [] _ _ =
1264 (Bound 0, Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty)
1265 | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _) => x) us);
1267 val (lhs, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
1268 val noops' = maps snd (Symtab.dest noops);
1272 (prove_unfold_defs thy noops' [simproc]
1273 (list_all (vars, Logic.mk_equals (lhs, rhs))))
1282 (*Look up the most specific record-equality.
1285 Testing equality of records boils down to the test of equality of all components.
1286 Therefore the complexity is: #components * complexity for single component.
1287 Especially if a record has a lot of components it may be better to split up
1288 the record first and do simplification on that (split_simp_tac).
1289 e.g. r(|lots of updates|) = x
1291 eq_simproc split_simp_tac
1292 Complexity: #components * #updates #updates
1295 Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
1296 (fn thy => fn _ => fn t =>
1297 (case t of Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ =>
1298 (case rec_id ~1 T of
1301 (case get_equalities thy name of
1303 | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
1309 (*Split quantified occurrences of records, for which P holds. P can peek on the
1310 subterm starting at the quantified occurrence of the record (including the quantifier):
1311 P t = 0: do not split
1312 P t = ~1: completely split
1313 P t > 0: split up to given bound of record extensions.*)
1314 fun split_simproc P =
1315 Simplifier.simproc_global @{theory HOL} "record_split_simp" ["x"]
1316 (fn thy => fn _ => fn t =>
1318 Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
1319 if quantifier = @{const_name all} orelse
1320 quantifier = @{const_name All} orelse
1321 quantifier = @{const_name Ex}
1323 (case rec_id ~1 T of
1326 let val split = P t in
1328 (case get_splits thy (rec_id split T) of
1330 | SOME (all_thm, All_thm, Ex_thm, _) =>
1333 @{const_name all} => all_thm
1334 | @{const_name All} => All_thm RS @{thm eq_reflection}
1335 | @{const_name Ex} => Ex_thm RS @{thm eq_reflection}
1336 | _ => raise Fail "split_simproc"))
1342 val ex_sel_eq_simproc =
1343 Simplifier.simproc_global @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
1344 (fn thy => fn ss => fn t =>
1347 prove_global true thy [] prop
1348 (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
1349 addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1);
1351 fun mkeq (lr, Teq, (sel, Tsel), x) i =
1352 if is_selector thy sel then
1355 if not (loose_bvar1 (x, 0))
1356 then Free ("x" ^ string_of_int i, range_type Tsel)
1357 else raise TERM ("", [x]);
1358 val sel' = Const (sel, Tsel) $ Bound 0;
1359 val (l, r) = if lr then (sel', x') else (x', sel');
1360 in Const (@{const_name HOL.eq}, Teq) $ l $ r end
1361 else raise TERM ("", [Const (sel, Tsel)]);
1363 fun dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
1364 (true, Teq, (sel, Tsel), X)
1365 | dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
1366 (false, Teq, (sel, Tsel), X)
1367 | dest_sel_eq _ = raise TERM ("", []);
1370 Const (@{const_name Ex}, Tex) $ Abs (s, T, t) =>
1372 val eq = mkeq (dest_sel_eq t) 0;
1374 list_all ([("r", T)],
1376 (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
1377 in SOME (prove prop) end
1378 handle TERM _ => NONE)
1383 (* split_simp_tac *)
1385 (*Split (and simplify) all records in the goal for which P holds.
1386 For quantified occurrences of a record
1387 P can peek on the whole subterm (including the quantifier); for free variables P
1388 can only peek on the variable itself.
1389 P t = 0: do not split
1390 P t = ~1: completely split
1391 P t > 0: split up to given bound of record extensions.*)
1392 fun split_simp_tac thms P = CSUBGOAL (fn (cgoal, i) =>
1394 val thy = Thm.theory_of_cterm cgoal;
1396 val goal = term_of cgoal;
1397 val frees = filter (is_recT o #2) (Term.add_frees goal []);
1399 val has_rec = exists_Const
1400 (fn (s, Type (_, [Type (_, [T, _]), _])) =>
1401 (s = @{const_name all} orelse s = @{const_name All} orelse s = @{const_name Ex}) andalso
1405 fun mk_split_free_tac free induct_thm i =
1407 val cfree = cterm_of thy free;
1408 val _$ (_ $ r) = concl_of induct_thm;
1409 val crec = cterm_of thy r;
1410 val thm = cterm_instantiate [(crec, cfree)] induct_thm;
1412 simp_tac (HOL_basic_ss addsimps @{thms induct_atomize}) i THEN
1414 simp_tac (HOL_basic_ss addsimps @{thms induct_rulify}) i
1417 val split_frees_tacs =
1418 frees |> map_filter (fn (x, T) =>
1419 (case rec_id ~1 T of
1423 val free = Free (x, T);
1427 (case get_splits thy (rec_id split T) of
1429 | SOME (_, _, _, induct_thm) =>
1430 SOME (mk_split_free_tac free induct_thm i))
1434 val simprocs = if has_rec goal then [split_simproc P] else [];
1435 val thms' = @{thms o_apply K_record_comp} @ thms;
1437 EVERY split_frees_tacs THEN
1438 Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i
1444 (*Split all records in the goal, which are quantified by !! or ALL.*)
1445 val split_tac = CSUBGOAL (fn (cgoal, i) =>
1447 val goal = term_of cgoal;
1449 val has_rec = exists_Const
1450 (fn (s, Type (_, [Type (_, [T, _]), _])) =>
1451 (s = @{const_name all} orelse s = @{const_name All}) andalso is_recT T
1454 fun is_all (Const (@{const_name all}, _) $ _) = ~1
1455 | is_all (Const (@{const_name All}, _) $ _) = ~1
1458 if has_rec goal then
1459 Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [split_simproc is_all]) i
1466 val split_name = "record_split_tac";
1467 val split_wrapper = (split_name, fn _ => fn tac => split_tac ORELSE' tac);
1471 (** theory extender interface **)
1475 fun case_names_fields x = Rule_Cases.case_names ["fields"] x;
1476 fun induct_type_global name = [case_names_fields, Induct.induct_type name];
1477 fun cases_type_global name = [case_names_fields, Induct.cases_type name];
1482 fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));
1484 (*Do case analysis / induction according to rule on last parameter of ith subgoal
1485 (or on s if there are no parameters).
1486 Instatiation of record variable (and predicate) in rule is calculated to
1487 avoid problems with higher order unification.*)
1488 fun try_param_tac s rule = CSUBGOAL (fn (cgoal, i) =>
1490 val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
1492 val g = Thm.term_of cgoal;
1493 val params = Logic.strip_params g;
1494 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
1495 val rule' = Thm.lift_rule cgoal rule;
1496 val (P, ys) = strip_comb (HOLogic.dest_Trueprop
1497 (Logic.strip_assums_concl (prop_of rule')));
1498 (*ca indicates if rule is a case analysis or induction rule*)
1500 (case rev (drop (length params) ys) of
1501 [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
1502 (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
1503 | [x] => (head_of x, false));
1506 (map (pairself cert)
1509 (case AList.lookup (op =) (Term.add_frees g []) s of
1510 NONE => error "try_param_tac: no such variable"
1511 | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
1513 [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
1514 (x, list_abs (params, Bound 0))])) rule';
1515 in compose_tac (false, rule'', nprems_of rule) i end);
1518 fun extension_definition name fields alphas zeta moreT more vars thy =
1520 val ctxt = Proof_Context.init_global thy;
1522 val base_name = Long_Name.base_name name;
1524 val fieldTs = map snd fields;
1525 val fields_moreTs = fieldTs @ [moreT];
1527 val alphas_zeta = alphas @ [zeta];
1529 val ext_binding = Binding.name (suffix extN base_name);
1530 val ext_name = suffix extN name;
1531 val ext_tyco = suffix ext_typeN name
1532 val extT = Type (ext_tyco, map TFree alphas_zeta);
1533 val ext_type = fields_moreTs ---> extT;
1536 (* the tree of new types that will back the record extension *)
1538 val mktreeV = Balanced_Tree.make Iso_Tuple_Support.mk_cons_tuple;
1540 fun mk_iso_tuple (left, right) (thy, i) =
1542 val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
1543 val ((_, cons), thy') = thy
1544 |> Iso_Tuple_Support.add_iso_tuple_type
1545 (Binding.suffix_name suff (Binding.name base_name), alphas_zeta)
1546 (fastype_of left, fastype_of right);
1548 (cons $ left $ right, (thy', i + 1))
1551 (*trying to create a 1-element iso_tuple will fail, and is pointless anyway*)
1552 fun mk_even_iso_tuple [arg] = pair arg
1553 | mk_even_iso_tuple args = mk_iso_tuple (Iso_Tuple_Support.dest_cons_tuple (mktreeV args));
1555 fun build_meta_tree_type i thy vars more =
1556 let val len = length vars in
1557 if len < 1 then raise TYPE ("meta_tree_type args too short", [], vars)
1558 else if len > 16 then
1561 | group16 xs = take 16 xs :: group16 (drop 16 xs);
1562 val vars' = group16 vars;
1563 val (composites, (thy', i')) = fold_map mk_even_iso_tuple vars' (thy, i);
1565 build_meta_tree_type i' thy' composites more
1568 let val (term, (thy', _)) = mk_iso_tuple (mktreeV vars, more) (thy, 0)
1572 val _ = timing_msg ctxt "record extension preparing definitions";
1575 (* 1st stage part 1: introduce the tree of new types *)
1577 fun get_meta_tree () = build_meta_tree_type 1 thy vars more;
1578 val (ext_body, typ_thy) =
1579 timeit_msg ctxt "record extension nested type def:" get_meta_tree;
1582 (* prepare declarations and definitions *)
1584 (* 1st stage part 2: define the ext constant *)
1586 fun mk_ext args = list_comb (Const (ext_name, ext_type), args);
1587 val ext_spec = Logic.mk_equals (mk_ext (vars @ [more]), ext_body);
1591 |> Sign.declare_const_global ((ext_binding, ext_type), NoSyn) |> snd
1592 |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]
1593 ||> Theory.checkpoint
1594 val ([ext_def], defs_thy) =
1595 timeit_msg ctxt "record extension constructor def:" mk_defs;
1598 (* prepare propositions *)
1600 val _ = timing_msg ctxt "record extension preparing propositions";
1601 val vars_more = vars @ [more];
1602 val variants = map (fn Free (x, _) => x) vars_more;
1603 val ext = mk_ext vars_more;
1604 val s = Free (rN, extT);
1605 val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT);
1607 val inject_prop = (* FIXME local x x' *)
1608 let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
1609 HOLogic.mk_conj (HOLogic.eq_const extT $
1610 mk_ext vars_more $ mk_ext vars_more', @{term True})
1612 foldr1 HOLogic.mk_conj
1613 (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [@{term True}])
1617 (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
1619 val split_meta_prop = (* FIXME local P *)
1620 let val P = Free (singleton (Name.variant_list variants) "P", extT --> Term.propT) in
1622 (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
1625 val prove_standard = prove_future_global true defs_thy;
1629 (prove_standard [] inject_prop
1631 simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
1633 (rtac @{thm refl_conj_eq} 1 ORELSE
1634 Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
1637 val inject = timeit_msg ctxt "record extension inject proof:" inject_prf;
1639 (*We need a surjection property r = (| f = f r, g = g r ... |)
1640 to prove other theorems. We haven't given names to the accessors
1641 f, g etc yet however, so we generate an ext structure with
1642 free variables as all arguments and allow the introduction tactic to
1643 operate on it as far as it can. We then use Drule.export_without_context
1644 to convert the free variables into unifiable variables and unify them with
1645 (roughly) the definition of the accessor.*)
1646 fun surject_prf () =
1648 val cterm_ext = cterm_of defs_thy ext;
1649 val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
1651 simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
1652 REPEAT_ALL_NEW Iso_Tuple_Support.iso_tuple_intros_tac 1;
1653 val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
1654 val [halfway] = Seq.list_of (tactic1 start);
1655 val [surject] = Seq.list_of (tactic2 (Drule.export_without_context halfway));
1659 val surject = timeit_msg ctxt "record extension surjective proof:" surject_prf;
1661 fun split_meta_prf () =
1662 prove_standard [] split_meta_prop
1665 [rtac equal_intr_rule, Goal.norm_hhf_tac,
1666 etac @{thm meta_allE}, atac,
1667 rtac (@{thm prop_subst} OF [surject]),
1668 REPEAT o etac @{thm meta_allE}, atac]);
1669 val split_meta = timeit_msg ctxt "record extension split_meta proof:" split_meta_prf;
1672 let val (assm, concl) = induct_prop in
1673 prove_standard [assm] concl
1675 cut_rules_tac [split_meta RS Drule.equal_elim_rule2] 1 THEN
1676 resolve_tac prems 2 THEN
1677 asm_simp_tac HOL_ss 1)
1679 val induct = timeit_msg ctxt "record extension induct proof:" induct_prf;
1681 val ([induct', inject', surjective', split_meta'], thm_thy) =
1683 |> Global_Theory.add_thms (map (Thm.no_attributes o apfst Binding.name)
1684 [("ext_induct", induct),
1685 ("ext_inject", inject),
1686 ("ext_surjective", surject),
1687 ("ext_split", split_meta)]);
1690 (((ext_name, ext_type), (ext_tyco, alphas_zeta),
1691 extT, induct', inject', surjective', split_meta', ext_def), thm_thy)
1694 fun chunks [] [] = []
1695 | chunks [] xs = [xs]
1696 | chunks (l :: ls) xs = take l xs :: chunks ls (drop l xs);
1698 fun chop_last [] = error "chop_last: list should not be empty"
1699 | chop_last [x] = ([], x)
1700 | chop_last (x :: xs) = let val (tl, l) = chop_last xs in (x :: tl, l) end;
1702 fun subst_last _ [] = error "subst_last: list should not be empty"
1703 | subst_last s [_] = [s]
1704 | subst_last s (x :: xs) = x :: subst_last s xs;
1709 (*build up the record type from the current extension tpye extT and a list
1710 of parent extensions, starting with the root of the record hierarchy*)
1711 fun mk_recordT extT =
1712 fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT;
1715 fun obj_to_meta_all thm =
1717 fun E thm = (* FIXME proper name *)
1718 (case SOME (spec OF [thm]) handle THM _ => NONE of
1722 val th2 = Drule.forall_intr_vars th1;
1725 fun meta_to_obj_all thm =
1727 val thy = Thm.theory_of_thm thm;
1728 val prop = Thm.prop_of thm;
1729 val params = Logic.strip_params prop;
1730 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop);
1731 val ct = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.list_all (params, concl)));
1732 val thm' = Seq.hd (REPEAT (rtac allI 1) (Thm.trivial ct));
1733 in Thm.implies_elim thm' thm end;
1736 (* code generation *)
1738 fun mk_random_eq tyco vs extN Ts =
1740 (* FIXME local i etc. *)
1741 val size = @{term "i::code_numeral"};
1742 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
1743 val T = Type (tyco, map TFree vs);
1744 val Tm = termifyT T;
1745 val params = Name.invent_names Name.context "x" Ts;
1746 val lhs = HOLogic.mk_random T size;
1747 val tc = HOLogic.mk_return Tm @{typ Random.seed}
1748 (HOLogic.mk_valtermify_app extN params T);
1752 ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params)
1753 tc @{typ Random.seed} (SOME Tm, @{typ Random.seed});
1758 fun mk_full_exhaustive_eq tyco vs extN Ts =
1760 (* FIXME local i etc. *)
1761 val size = @{term "i::code_numeral"};
1762 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
1763 val T = Type (tyco, map TFree vs);
1764 val test_function = Free ("f", termifyT T --> @{typ "(bool * term list) option"});
1765 val params = Name.invent_names Name.context "x" Ts;
1766 fun full_exhaustiveT T =
1767 (termifyT T --> @{typ "(bool * Code_Evaluation.term list) option"}) -->
1768 @{typ code_numeral} --> @{typ "(bool * Code_Evaluation.term list) option"};
1769 fun mk_full_exhaustive T =
1770 Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
1771 full_exhaustiveT T);
1772 val lhs = mk_full_exhaustive T $ test_function $ size;
1773 val tc = test_function $ (HOLogic.mk_valtermify_app extN params T);
1774 val rhs = fold_rev (fn (v, T) => fn cont =>
1775 mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc;
1780 fun instantiate_sort_record (sort, mk_eq) tyco vs extN Ts thy =
1782 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_eq tyco vs extN Ts));
1785 |> Class.instantiation ([tyco], vs, sort)
1786 |> `(fn lthy => Syntax.check_term lthy eq)
1787 |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
1789 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
1792 fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy =
1794 val algebra = Sign.classes_of thy;
1795 val has_inst = can (Sorts.mg_domain algebra ext_tyco) sort;
1797 if has_inst then thy
1799 (case Quickcheck_Common.perhaps_constrain thy (map (rpair sort) Ts) vs of
1801 instantiate_sort_record (sort, mk_eq) ext_tyco (map constrain vs) extN
1802 ((map o map_atyps) (fn TFree v => TFree (constrain v)) Ts) thy
1806 fun add_code ext_tyco vs extT ext simps inject thy =
1809 (HOLogic.mk_Trueprop o HOLogic.mk_eq)
1810 (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
1811 Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT));
1813 Class.intro_classes_tac []
1814 THEN (Simplifier.rewrite_goals_tac [Simpdata.mk_eq eq_def])
1815 THEN ALLGOALS (rtac @{thm refl});
1816 fun mk_eq thy eq_def = Simplifier.rewrite_rule
1817 [(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject;
1818 fun mk_eq_refl thy =
1821 ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
1822 |> AxClass.unoverload thy;
1823 val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
1824 val ensure_exhaustive_record =
1825 ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
1828 |> Code.add_datatype [ext]
1829 |> fold Code.add_default_eqn simps
1830 |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
1831 |> `(fn lthy => Syntax.check_term lthy eq)
1832 |-> (fn eq => Specification.definition
1833 (NONE, (Attrib.empty_binding, eq)))
1834 |-> (fn (_, (_, eq_def)) =>
1835 Class.prove_instantiation_exit_result Morphism.thm
1836 (fn _ => fn eq_def => tac eq_def) eq_def)
1837 |-> (fn eq_def => fn thy =>
1838 thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
1839 |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
1840 |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
1841 |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
1847 fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
1849 val ctxt = Proof_Context.init_global thy;
1851 val prefix = Binding.name_of binding;
1852 val name = Sign.full_name thy binding;
1853 val full = Sign.full_name_path thy prefix;
1855 val bfields = map (fn (x, T, _) => (x, T)) raw_fields;
1856 val field_syntax = map #3 raw_fields;
1858 val parent_fields = maps #fields parents;
1859 val parent_chunks = map (length o #fields) parents;
1860 val parent_names = map fst parent_fields;
1861 val parent_types = map snd parent_fields;
1862 val parent_fields_len = length parent_fields;
1863 val parent_variants =
1864 Name.variant_list [moreN, rN, rN ^ "'", wN] (map Long_Name.base_name parent_names);
1865 val parent_vars = map2 (curry Free) parent_variants parent_types;
1866 val parent_len = length parents;
1868 val fields = map (apfst full) bfields;
1869 val names = map fst fields;
1870 val types = map snd fields;
1871 val alphas_fields = fold Term.add_tfreesT types [];
1872 val alphas_ext = inter (op =) alphas_fields alphas;
1873 val len = length fields;
1875 Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
1876 (map (Binding.name_of o fst) bfields);
1877 val vars = map2 (curry Free) variants types;
1878 val named_vars = names ~~ vars;
1879 val idxms = 0 upto len;
1881 val all_fields = parent_fields @ fields;
1882 val all_types = parent_types @ types;
1883 val all_variants = parent_variants @ variants;
1884 val all_vars = parent_vars @ vars;
1885 val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
1887 val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", HOLogic.typeS);
1888 val moreT = TFree zeta;
1889 val more = Free (moreN, moreT);
1890 val full_moreN = full (Binding.name moreN);
1891 val bfields_more = bfields @ [(Binding.name moreN, moreT)];
1892 val fields_more = fields @ [(full_moreN, moreT)];
1893 val named_vars_more = named_vars @ [(full_moreN, more)];
1894 val all_vars_more = all_vars @ [more];
1895 val all_named_vars_more = all_named_vars @ [(full_moreN, more)];
1898 (* 1st stage: ext_thy *)
1900 val extension_name = full binding;
1902 val ((ext, (ext_tyco, vs),
1903 extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
1905 |> Sign.qualified_path false binding
1906 |> extension_definition extension_name fields alphas_ext zeta moreT more vars;
1908 val _ = timing_msg ctxt "record preparing definitions";
1909 val Type extension_scheme = extT;
1910 val extension_name = unsuffix ext_typeN (fst extension_scheme);
1911 val extension = let val (n, Ts) = extension_scheme in (n, subst_last HOLogic.unitT Ts) end;
1912 val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extension_name];
1913 val extension_id = implode extension_names;
1915 fun rec_schemeT n = mk_recordT (map #extension (drop n parents)) extT;
1916 val rec_schemeT0 = rec_schemeT 0;
1919 let val (c, Ts) = extension in
1920 mk_recordT (map #extension (drop n parents))
1921 (Type (c, subst_last HOLogic.unitT Ts))
1927 val (args', more) = chop_last args;
1928 fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]);
1930 fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args')) more;
1932 if more = HOLogic.unit
1933 then build (map_range recT (parent_len + 1))
1934 else build (map_range rec_schemeT (parent_len + 1))
1937 val r_rec0 = mk_rec all_vars_more 0;
1938 val r_rec_unit0 = mk_rec (all_vars @ [HOLogic.unit]) 0;
1940 fun r n = Free (rN, rec_schemeT n);
1942 fun r_unit n = Free (rN, recT n);
1943 val r_unit0 = r_unit 0;
1944 val w = Free (wN, rec_schemeT 0);
1947 (* print translations *)
1949 val record_ext_type_abbr_tr's =
1951 val trname = hd extension_names;
1952 val last_ext = unsuffix ext_typeN (fst extension);
1953 in [record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0 trname] end;
1955 val record_ext_type_tr's =
1957 (*avoid conflict with record_type_abbr_tr's*)
1958 val trnames = if parent_len > 0 then [extension_name] else [];
1959 in map record_ext_type_tr' trnames end;
1961 val advanced_print_translation =
1962 map field_update_tr' (full_moreN :: names) @ [record_ext_tr' extension_name] @
1963 record_ext_type_tr's @ record_ext_type_abbr_tr's;
1966 (* prepare declarations *)
1968 val sel_decls = map (mk_selC rec_schemeT0 o apfst Binding.name_of) bfields_more;
1969 val upd_decls = map (mk_updC updateN rec_schemeT0 o apfst Binding.name_of) bfields_more;
1970 val make_decl = (makeN, all_types ---> recT0);
1971 val fields_decl = (fields_selN, types ---> Type extension);
1972 val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0);
1973 val truncate_decl = (truncateN, rec_schemeT0 --> recT0);
1976 (* prepare definitions *)
1978 val ext_defs = ext_def :: map #ext_def parents;
1980 (*Theorems from the iso_tuple intros.
1981 By unfolding ext_defs from r_rec0 we create a tree of constructor
1982 calls (many of them Pair, but others as well). The introduction
1983 rules for update_accessor_eq_assist can unify two different ways
1984 on these constructors. If we take the complete result sequence of
1985 running a the introduction tactic, we get one theorem for each upd/acc
1986 pair, from which we can derive the bodies of our selector and
1987 updator and their convs.*)
1988 fun get_access_update_thms () =
1992 (*pick variable indices of 1 to avoid possible variable
1993 collisions with existing variables in updacc_eq_triv*)
1994 fun to_Var (Free (c, T)) = Var ((c, 1), T);
1995 in mk_rec (map to_Var all_vars_more) 0 end;
1997 val cterm_rec = cterm_of ext_thy r_rec0;
1998 val cterm_vrs = cterm_of ext_thy r_rec0_Vars;
1999 val insts = [("v", cterm_rec), ("v'", cterm_vrs)];
2000 val init_thm = named_cterm_instantiate insts updacc_eq_triv;
2001 val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
2003 simp_tac (HOL_basic_ss addsimps ext_defs) 1 THEN
2004 REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE terminal);
2005 val updaccs = Seq.list_of (tactic init_thm);
2007 (updaccs RL [updacc_accessor_eqE],
2008 updaccs RL [updacc_updator_eqE],
2009 updaccs RL [updacc_cong_from_eq])
2011 val (accessor_thms, updator_thms, upd_acc_cong_assists) =
2012 timeit_msg ctxt "record getting tree access/updates:" get_access_update_thms;
2014 fun lastN xs = drop parent_fields_len xs;
2017 fun mk_sel_spec ((c, T), thm) =
2019 val (acc $ arg, _) =
2020 HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (Thm.concl_of thm)));
2022 if arg aconv r_rec0 then ()
2023 else raise TERM ("mk_sel_spec: different arg", [arg]);
2025 Const (mk_selC rec_schemeT0 (c, T)) :== acc
2027 val sel_specs = map mk_sel_spec (fields_more ~~ lastN accessor_thms);
2030 fun mk_upd_spec ((c, T), thm) =
2032 val (upd $ _ $ arg, _) =
2033 HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (Thm.concl_of thm)));
2035 if arg aconv r_rec0 then ()
2036 else raise TERM ("mk_sel_spec: different arg", [arg]);
2037 in Const (mk_updC updateN rec_schemeT0 (c, T)) :== upd end;
2038 val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms);
2040 (*derived operations*)
2042 list_comb (Const (full (Binding.name makeN), all_types ---> recT0), all_vars) :==
2043 mk_rec (all_vars @ [HOLogic.unit]) 0;
2045 list_comb (Const (full (Binding.name fields_selN), types ---> Type extension), vars) :==
2046 mk_rec (all_vars @ [HOLogic.unit]) parent_len;
2048 Const (full (Binding.name extendN), recT0 --> moreT --> rec_schemeT0) $ r_unit0 $ more :==
2049 mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
2051 Const (full (Binding.name truncateN), rec_schemeT0 --> recT0) $ r0 :==
2052 mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
2055 (* 2st stage: defs_thy *)
2059 |> Sign.add_advanced_trfuns ([], [], advanced_print_translation, [])
2060 |> Sign.restore_naming thy
2061 |> Typedecl.abbrev_global (binding, map #1 alphas, NoSyn) recT0 |> snd
2062 |> Typedecl.abbrev_global
2063 (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0 |> snd
2064 |> Sign.qualified_path false binding
2065 |> fold (fn ((x, T), mx) => snd o Sign.declare_const_global ((Binding.name x, T), mx))
2066 (sel_decls ~~ (field_syntax @ [NoSyn]))
2067 |> fold (fn (x, T) => snd o Sign.declare_const_global ((Binding.name x, T), NoSyn))
2068 (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
2069 |> (Global_Theory.add_defs false o
2070 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) sel_specs
2071 ||>> (Global_Theory.add_defs false o
2072 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) upd_specs
2073 ||>> (Global_Theory.add_defs false o
2074 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
2075 [make_spec, fields_spec, extend_spec, truncate_spec]
2076 ||> Theory.checkpoint
2077 val (((sel_defs, upd_defs), derived_defs), defs_thy) =
2078 timeit_msg ctxt "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
2081 (* prepare propositions *)
2082 val _ = timing_msg ctxt "record preparing propositions";
2083 val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> HOLogic.boolT);
2084 val C = Free (singleton (Name.variant_list all_variants) "C", HOLogic.boolT);
2085 val P_unit = Free (singleton (Name.variant_list all_variants) "P", recT0 --> HOLogic.boolT);
2088 val sel_conv_props =
2089 map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more;
2092 fun mk_upd_prop i (c, T) =
2095 Free (singleton (Name.variant_list all_variants) (Long_Name.base_name c ^ "'"), T --> T);
2096 val n = parent_fields_len + i;
2097 val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more;
2098 in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
2099 val upd_conv_props = map2 mk_upd_prop idxms fields_more;
2102 val induct_scheme_prop =
2103 All (map dest_Free all_vars_more) (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0);
2105 (All (map dest_Free all_vars) (Trueprop (P_unit $ r_rec_unit0)),
2106 Trueprop (P_unit $ r_unit0));
2109 val surjective_prop =
2110 let val args = map (fn (c, Free (_, T)) => mk_sel r0 (c, T)) all_named_vars_more
2111 in r0 === mk_rec args 0 end;
2114 val cases_scheme_prop =
2115 (All (map dest_Free all_vars_more) ((r0 === r_rec0) ==> Trueprop C))
2119 (All (map dest_Free all_vars) ((r_unit0 === r_rec_unit0) ==> Trueprop C))
2123 val split_meta_prop =
2125 val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0-->Term.propT);
2128 (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
2131 val split_object_prop =
2132 let val ALL = fold_rev (fn (v, T) => fn t => HOLogic.mk_all (v, T, t))
2133 in ALL [dest_Free r0] (P $ r0) === ALL (map dest_Free all_vars_more) (P $ r_rec0) end;
2136 let val EX = fold_rev (fn (v, T) => fn t => HOLogic.mk_exists (v, T, t))
2137 in EX [dest_Free r0] (P $ r0) === EX (map dest_Free all_vars_more) (P $ r_rec0) end;
2142 val s' = Free (rN ^ "'", rec_schemeT0);
2143 fun mk_sel_eq (c, Free (_, T)) = mk_sel r0 (c, T) === mk_sel s' (c, T);
2144 val seleqs = map mk_sel_eq all_named_vars_more;
2145 in All (map dest_Free [r0, s']) (Logic.list_implies (seleqs, r0 === s')) end;
2148 (* 3rd stage: thms_thy *)
2150 fun prove stndrd = prove_future_global stndrd defs_thy;
2151 val prove_standard = prove_future_global true defs_thy;
2152 val future_forward_prf = future_forward_prf_standard defs_thy;
2154 fun prove_simp stndrd ss simps =
2155 let val tac = simp_all_tac ss simps
2156 in fn prop => prove stndrd [] prop (K tac) end;
2158 val ss = get_simpset defs_thy;
2160 fun sel_convs_prf () =
2161 map (prove_simp false ss (sel_defs @ accessor_thms)) sel_conv_props;
2162 val sel_convs = timeit_msg ctxt "record sel_convs proof:" sel_convs_prf;
2163 fun sel_convs_standard_prf () = map Drule.export_without_context sel_convs;
2164 val sel_convs_standard =
2165 timeit_msg ctxt "record sel_convs_standard proof:" sel_convs_standard_prf;
2167 fun upd_convs_prf () =
2168 map (prove_simp false ss (upd_defs @ updator_thms)) upd_conv_props;
2169 val upd_convs = timeit_msg ctxt "record upd_convs proof:" upd_convs_prf;
2170 fun upd_convs_standard_prf () = map Drule.export_without_context upd_convs;
2171 val upd_convs_standard =
2172 timeit_msg ctxt "record upd_convs_standard proof:" upd_convs_standard_prf;
2174 fun get_upd_acc_congs () =
2176 val symdefs = map Thm.symmetric (sel_defs @ upd_defs);
2177 val fold_ss = HOL_basic_ss addsimps symdefs;
2178 val ua_congs = map (Drule.export_without_context o simplify fold_ss) upd_acc_cong_assists;
2179 in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
2180 val (fold_congs, unfold_congs) =
2181 timeit_msg ctxt "record upd fold/unfold congs:" get_upd_acc_congs;
2183 val parent_induct = Option.map #induct_scheme (try List.last parents);
2185 fun induct_scheme_prf () =
2186 prove_standard [] induct_scheme_prop
2189 [case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
2190 try_param_tac rN ext_induct 1,
2191 asm_simp_tac HOL_basic_ss 1]);
2192 val induct_scheme = timeit_msg ctxt "record induct_scheme proof:" induct_scheme_prf;
2195 let val (assm, concl) = induct_prop in
2196 prove_standard [assm] concl (fn {prems, ...} =>
2197 try_param_tac rN induct_scheme 1
2198 THEN try_param_tac "more" @{thm unit.induct} 1
2199 THEN resolve_tac prems 1)
2201 val induct = timeit_msg ctxt "record induct proof:" induct_prf;
2203 fun cases_scheme_prf () =
2205 val _ $ (Pvar $ _) = concl_of induct_scheme;
2208 [(cterm_of defs_thy Pvar, cterm_of defs_thy
2209 (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
2211 in Object_Logic.rulify (mp OF [ind, refl]) end;
2213 val cases_scheme_prf = future_forward_prf cases_scheme_prf cases_scheme_prop;
2214 val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" cases_scheme_prf;
2217 prove_standard [] cases_prop
2219 try_param_tac rN cases_scheme 1 THEN
2220 simp_all_tac HOL_basic_ss [@{thm unit_all_eq1}]);
2221 val cases = timeit_msg ctxt "record cases proof:" cases_prf;
2223 fun surjective_prf () =
2226 get_sel_upd_defs defs_thy addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id});
2227 val init_ss = HOL_basic_ss addsimps ext_defs;
2229 prove_standard [] surjective_prop
2232 [rtac surject_assist_idE 1,
2235 (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
2236 (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
2238 val surjective = timeit_msg ctxt "record surjective proof:" surjective_prf;
2240 fun split_meta_prf () =
2241 prove false [] split_meta_prop
2244 [rtac equal_intr_rule, Goal.norm_hhf_tac,
2245 etac @{thm meta_allE}, atac,
2246 rtac (@{thm prop_subst} OF [surjective]),
2247 REPEAT o etac @{thm meta_allE}, atac]);
2248 val split_meta = timeit_msg ctxt "record split_meta proof:" split_meta_prf;
2249 fun split_meta_standardise () = Drule.export_without_context split_meta;
2250 val split_meta_standard =
2251 timeit_msg ctxt "record split_meta standard:" split_meta_standardise;
2253 fun split_object_prf () =
2255 val cPI= cterm_of defs_thy (lambda r0 (Trueprop (P $ r0)));
2256 val _ $ Abs (_, _, P $ _) = fst (Logic.dest_equals (concl_of split_meta_standard));
2257 val cP = cterm_of defs_thy P;
2258 val split_meta' = cterm_instantiate [(cP, cPI)] split_meta_standard;
2259 val (l, r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop);
2260 val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l);
2261 val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r);
2263 Thm.assume cl (*All r. P r*) (* 1 *)
2264 |> obj_to_meta_all (*!!r. P r*)
2265 |> Thm.equal_elim split_meta' (*!!n m more. P (ext n m more)*)
2266 |> meta_to_obj_all (*All n m more. P (ext n m more)*) (* 2*)
2267 |> Thm.implies_intr cl (* 1 ==> 2 *)
2269 Thm.assume cr (*All n m more. P (ext n m more)*)
2270 |> obj_to_meta_all (*!!n m more. P (ext n m more)*)
2271 |> Thm.equal_elim (Thm.symmetric split_meta') (*!!r. P r*)
2272 |> meta_to_obj_all (*All r. P r*)
2273 |> Thm.implies_intr cr (* 2 ==> 1 *)
2274 in thr COMP (thl COMP iffI) end;
2277 val split_object_prf = future_forward_prf split_object_prf split_object_prop;
2278 val split_object = timeit_msg ctxt "record split_object proof:" split_object_prf;
2281 fun split_ex_prf () =
2283 val ss = HOL_basic_ss addsimps @{thms not_ex [symmetric] Not_eq_iff};
2284 val P_nm = fst (dest_Free P);
2285 val not_P = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
2286 val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object;
2287 val so'' = simplify ss so';
2289 prove_standard [] split_ex_prop (fn _ => resolve_tac [so''] 1)
2291 val split_ex = timeit_msg ctxt "record split_ex proof:" split_ex_prf;
2293 fun equality_tac thms =
2295 val s' :: s :: eqs = rev thms;
2296 val ss' = ss addsimps (s' :: s :: sel_convs_standard);
2297 val eqs' = map (simplify ss') eqs;
2298 in simp_tac (HOL_basic_ss addsimps (s' :: s :: eqs')) 1 end;
2300 fun equality_prf () =
2301 prove_standard [] equality_prop (fn {context, ...} =>
2303 let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
2304 st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1 THEN
2305 res_inst_tac context [((rN, 0), s')] cases_scheme 1 THEN
2306 Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1)
2307 (*simp_all_tac ss (sel_convs) would also work but is less efficient*)
2309 val equality = timeit_msg ctxt "record equality proof:" equality_prf;
2311 val ((([sel_convs', upd_convs', sel_defs', upd_defs',
2312 fold_congs', unfold_congs',
2313 splits' as [split_meta', split_object', split_ex'], derived_defs'],
2314 [surjective', equality']),
2315 [induct_scheme', induct', cases_scheme', cases']), thms_thy) =
2317 |> (Global_Theory.add_thmss o map (Thm.no_attributes o apfst Binding.name))
2318 [("select_convs", sel_convs_standard),
2319 ("update_convs", upd_convs_standard),
2320 ("select_defs", sel_defs),
2321 ("update_defs", upd_defs),
2322 ("fold_congs", fold_congs),
2323 ("unfold_congs", unfold_congs),
2324 ("splits", [split_meta_standard, split_object, split_ex]),
2325 ("defs", derived_defs)]
2326 ||>> (Global_Theory.add_thms o map (Thm.no_attributes o apfst Binding.name))
2327 [("surjective", surjective),
2328 ("equality", equality)]
2329 ||>> (Global_Theory.add_thms o (map o apfst o apfst) Binding.name)
2330 [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
2331 (("induct", induct), induct_type_global name),
2332 (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
2333 (("cases", cases), cases_type_global name)];
2335 val sel_upd_simps = sel_convs' @ upd_convs';
2336 val sel_upd_defs = sel_defs' @ upd_defs';
2337 val iffs = [ext_inject]
2338 val depth = parent_len + 1;
2340 val ([simps', iffs'], thms_thy') =
2342 |> Global_Theory.add_thmss
2343 [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
2344 ((Binding.name "iffs", iffs), [iff_add])];
2347 make_info alphas parent fields extension
2348 ext_induct ext_inject ext_surjective ext_split ext_def
2349 sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs'
2350 surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs';
2354 |> put_record name info
2355 |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs')
2356 |> add_equalities extension_id equality'
2357 |> add_extinjects ext_inject
2358 |> add_extsplit extension_name ext_split
2359 |> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
2360 |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
2361 |> add_fieldext (extension_name, snd extension) names
2362 |> add_code ext_tyco vs extT ext simps' ext_inject
2363 |> Sign.restore_naming thy;
2372 fun read_parent NONE ctxt = (NONE, ctxt)
2373 | read_parent (SOME raw_T) ctxt =
2374 (case Proof_Context.read_typ_abbrev ctxt raw_T of
2375 Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt)
2376 | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));
2378 fun prep_field prep (x, T, mx) = (x, prep T, mx)
2380 cat_error msg ("The error(s) above occurred in record field " ^ Binding.print x);
2382 fun read_field raw_field ctxt =
2383 let val field as (_, T, _) = prep_field (Syntax.read_typ ctxt) raw_field
2384 in (field, Variable.declare_typ T ctxt) end;
2388 fun add_record (params, binding) raw_parent raw_fields thy =
2390 val _ = Theory.requires thy "Record" "record definitions";
2392 val ctxt = Proof_Context.init_global thy;
2393 fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T)
2394 handle TYPE (msg, _, _) => error msg;
2399 val parent = Option.map (apfst (map cert_typ)) raw_parent
2401 cat_error msg ("The error(s) above occurred in parent record specification");
2402 val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []);
2403 val parents = get_parent_info thy parent;
2405 val bfields = map (prep_field cert_typ) raw_fields;
2409 val name = Sign.full_name thy binding;
2410 val err_dup_record =
2411 if is_none (get_info thy name) then []
2412 else ["Duplicate definition of record " ^ quote name];
2414 val spec_frees = fold Term.add_tfreesT (parent_args @ map #2 bfields) [];
2415 val err_extra_frees =
2416 (case subtract (op =) params spec_frees of
2418 | extras => ["Extra free type variable(s) " ^
2419 commas (map (Syntax.string_of_typ ctxt o TFree) extras)]);
2421 val err_no_fields = if null bfields then ["No fields present"] else [];
2423 val err_dup_fields =
2424 (case duplicates Binding.eq_name (map #1 bfields) of
2426 | dups => ["Duplicate field(s) " ^ commas (map Binding.print dups)]);
2428 val err_bad_fields =
2429 if forall (not_equal moreN o Binding.name_of o #1) bfields then []
2430 else ["Illegal field name " ^ quote moreN];
2433 err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields;
2434 val _ = if null errs then () else error (cat_lines errs);
2436 thy |> definition (params, binding) parent parents bfields
2438 handle ERROR msg => cat_error msg ("Failed to define record " ^ Binding.print binding);
2440 fun add_record_cmd (raw_params, binding) raw_parent raw_fields thy =
2442 val ctxt = Proof_Context.init_global thy;
2443 val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
2444 val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
2445 val (parent, ctxt2) = read_parent raw_parent ctxt1;
2446 val (fields, ctxt3) = fold_map read_field raw_fields ctxt2;
2447 val params' = map (Proof_Context.check_tfree ctxt3) params;
2448 in thy |> add_record (params', binding) parent fields end;
2456 Sign.add_trfuns ([], parse_translation, [], []) #>
2457 Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #>
2458 Simplifier.map_simpset_global (fn ss => ss addsimprocs [simproc, upd_simproc, eq_simproc]);
2464 Outer_Syntax.command "record" "define extensible record" Keyword.thy_decl
2465 (Parse.type_args_constrained -- Parse.binding --
2466 (Parse.$$$ "=" |-- Scan.option (Parse.typ --| Parse.$$$ "+") --
2467 Scan.repeat1 Parse.const_binding)
2468 >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd x y z)));