src/HOL/Tools/record_package.ML
author wenzelm
Wed Oct 21 13:31:30 1998 +0200 (1998-10-21)
changeset 5707 b0e631634b5a
parent 5698 2b5d9bdec5af
child 5713 27d4fcf5fe5f
permissions -rw-r--r--
field_injects [iffs];
     1 (*  Title:      HOL/Tools/record_package.ML
     2     ID:         $Id$
     3     Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     4 
     5 Extensible records with structural subtyping in HOL.
     6 *)
     7 
     8 signature BASIC_RECORD_PACKAGE =
     9 sig
    10   val record_split_tac: int -> tactic
    11   val record_split_wrapper: string * wrapper
    12   val record_split_name: string
    13 end;
    14 
    15 signature RECORD_PACKAGE =
    16 sig
    17   include BASIC_RECORD_PACKAGE
    18   val quiet_mode: bool ref
    19   val moreS: sort
    20   val mk_fieldT: (string * typ) * typ -> typ
    21   val dest_fieldT: typ -> (string * typ) * typ
    22   val mk_field: (string * term) * term -> term
    23   val mk_fst: term -> term
    24   val mk_snd: term -> term
    25   val mk_recordT: (string * typ) list * typ -> typ
    26   val dest_recordT: typ -> (string * typ) list * typ
    27   val mk_record: (string * term) list * term -> term
    28   val mk_sel: term -> string -> term
    29   val mk_update: term -> string * term -> term
    30   val print_records: theory -> unit
    31   val add_record: (string list * bstring) -> string option
    32     -> (bstring * string) list -> theory -> theory
    33   val add_record_i: (string list * bstring) -> (typ list * string) option
    34     -> (bstring * typ) list -> theory -> theory
    35   val setup: (theory -> theory) list
    36 end;
    37 
    38 structure RecordPackage: RECORD_PACKAGE =
    39 struct
    40 
    41 
    42 (*** utilities ***)
    43 
    44 (* messages *)
    45 
    46 val quiet_mode = ref false;
    47 fun message s = if ! quiet_mode then () else writeln s;
    48 
    49 
    50 (* attributes etc. *)        (* FIXME move to Provers *)
    51 
    52 fun add_iffs_global (thy, th) =
    53   let
    54     val ss = Simplifier.simpset_ref_of thy;
    55     val cs = Classical.claset_ref_of thy;
    56     val (cs', ss') = (! cs, ! ss) addIffs [Attribute.thm_of th];
    57   in ss := ss'; cs := cs'; (thy, th) end;
    58 
    59 fun add_wrapper wrapper thy =
    60   let val r = claset_ref_of thy
    61   in r := ! r addSWrapper wrapper; thy end;
    62 
    63 
    64 (* definitions and equations *)
    65 
    66 infix 0 :== ===;
    67 
    68 val (op :==) = Logic.mk_defpair;
    69 val (op ===) = HOLogic.mk_Trueprop o HOLogic.mk_eq;
    70 
    71 fun get_defs thy specs = map (PureThy.get_tthm thy o fst) specs;
    72 
    73 
    74 (* proof by simplification *)
    75 
    76 fun prove_simp thy tacs simps =
    77   let
    78     val sign = Theory.sign_of thy;
    79     val ss = Simplifier.addsimps (HOL_basic_ss, map Attribute.thm_of simps);
    80 
    81     fun prove goal =
    82       Attribute.tthm_of
    83         (Goals.prove_goalw_cterm [] (Thm.cterm_of sign goal)
    84           (K (tacs @ [ALLGOALS (Simplifier.simp_tac ss)]))
    85         handle ERROR => error ("The error(s) above occurred while trying to prove "
    86           ^ quote (Sign.string_of_term sign goal)));
    87   in prove end;
    88 
    89 fun simp simps =
    90   let val ss = Simplifier.addsimps (HOL_basic_ss, map Attribute.thm_of simps)
    91   in apfst (Simplifier.full_simplify ss) end;
    92 
    93 
    94 
    95 (*** syntax operations ***)
    96 
    97 (** name components **)
    98 
    99 val moreN = "more";
   100 val schemeN = "_scheme";
   101 val fieldN = "_field";
   102 val raw_fieldN = "_raw_field";
   103 val field_typeN = "_field_type";
   104 val fstN = "_val";
   105 val sndN = "_more";
   106 val updateN = "_update";
   107 val makeN = "make";
   108 val make_schemeN = "make_scheme";
   109 
   110 (*see datatype package*)
   111 val caseN = "_case";
   112 
   113 
   114 
   115 (** generic operations **)
   116 
   117 fun fst_fn T U = Abs ("x", T, Abs ("y", U, Bound 1));
   118 fun snd_fn T U = Abs ("x", T, Abs ("y", U, Bound 0));
   119 
   120 fun mk_prod_case name f p =
   121   let
   122     val fT as Type ("fun", [A, Type ("fun", [B, C])]) = fastype_of f;
   123     val pT = fastype_of p;
   124   in Const (suffix caseN name, fT --> pT --> C) $ f $ p end;
   125 
   126 
   127 
   128 (** tuple operations **)
   129 
   130 (* more type class *)
   131 
   132 val moreS = ["Record.more"];
   133 
   134 
   135 (* types *)
   136 
   137 fun mk_fieldT ((c, T), U) = Type (suffix field_typeN c, [T, U]);
   138 
   139 fun dest_fieldT (typ as Type (c_field_type, [T, U])) =
   140       (case try (unsuffix field_typeN) c_field_type of
   141         None => raise TYPE ("dest_fieldT", [typ], [])
   142       | Some c => ((c, T), U))
   143   | dest_fieldT typ = raise TYPE ("dest_fieldT", [typ], []);
   144 
   145 
   146 (* constructors *)
   147 
   148 fun mk_fieldC U (c, T) = (suffix fieldN c, T --> U --> mk_fieldT ((c, T), U));
   149 
   150 fun gen_mk_field sfx ((c, t), u) =
   151   let val T = fastype_of t and U = fastype_of u
   152   in Const (suffix sfx c, [T, U] ---> mk_fieldT ((c, T), U)) $ t $ u end;
   153 
   154 val mk_field = gen_mk_field fieldN;
   155 val mk_raw_field = gen_mk_field raw_fieldN;
   156 
   157 
   158 (* destructors *)
   159 
   160 fun mk_fstC U (c, T) = (suffix fstN c, mk_fieldT ((c, T), U) --> T);
   161 fun mk_sndC U (c, T) = (suffix sndN c, mk_fieldT ((c, T), U) --> U);
   162 
   163 fun dest_field fst_or_snd p =
   164   let
   165     val pT = fastype_of p;
   166     val ((c, T), U) = dest_fieldT pT;
   167     val (destN, destT) = if fst_or_snd then (fstN, T) else (sndN, U);
   168   in Const (suffix destN c, pT --> destT) $ p end;
   169 
   170 val mk_fst = dest_field true;
   171 val mk_snd = dest_field false;
   172 
   173 
   174 
   175 (** record operations **)
   176 
   177 (* types *)
   178 
   179 val mk_recordT = foldr mk_fieldT;
   180 
   181 fun dest_recordT T =
   182   (case try dest_fieldT T of
   183     None => ([], T)
   184   | Some (c_T, U) => apfst (cons c_T) (dest_recordT U));
   185 
   186 fun find_fieldT c rT =
   187   (case assoc (fst (dest_recordT rT), c) of
   188     None => raise TYPE ("find_field: " ^ c, [rT], [])
   189   | Some T => T);
   190 
   191 
   192 (* constructors *)
   193 
   194 val mk_record = foldr mk_field;
   195 
   196 
   197 (* selectors *)
   198 
   199 fun mk_selC rT (c, T) = (c, rT --> T);
   200 
   201 fun mk_sel r c =
   202   let val rT = fastype_of r
   203   in Const (mk_selC rT (c, find_fieldT c rT)) $ r end;
   204 
   205 val mk_moreC = mk_selC;
   206 
   207 fun mk_more r c =
   208   let val rT = fastype_of r
   209   in Const (mk_moreC rT (c, snd (dest_recordT rT))) $ r end;
   210 
   211 
   212 (* updates *)
   213 
   214 fun mk_updateC rT (c, T) = (suffix updateN c, T --> rT --> rT);
   215 
   216 fun mk_update r (c, x) =
   217   let val rT = fastype_of r
   218   in Const (mk_updateC rT (c, find_fieldT c rT)) $ x $ r end;
   219 
   220 val mk_more_updateC = mk_updateC;
   221 
   222 fun mk_more_update r (c, x) =
   223   let val rT = fastype_of r
   224   in Const (mk_more_updateC rT (c, snd (dest_recordT rT))) $ x $ r end;
   225 
   226 
   227 (* make *)
   228 
   229 fun mk_makeC rT (c, Ts) = (c, Ts ---> rT);
   230 
   231 
   232 
   233 (** concrete syntax for records **)
   234 
   235 (* parse translations *)
   236 
   237 fun gen_field_tr mark sfx (t as Const (c, _) $ Free (name, _) $ arg) =
   238       if c = mark then Syntax.const (suffix sfx name) $ arg
   239       else raise TERM ("gen_field_tr: " ^ mark, [t])
   240   | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]);
   241 
   242 fun gen_fields_tr sep mark sfx (tm as Const (c, _) $ t $ u) =
   243       if c = sep then gen_field_tr mark sfx t :: gen_fields_tr sep mark sfx u
   244       else [gen_field_tr mark sfx tm]
   245   | gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm];
   246 
   247 fun gen_record_tr sep mark sfx unit [t] = foldr (op $) (gen_fields_tr sep mark sfx t, unit)
   248   | gen_record_tr _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
   249 
   250 fun gen_record_scheme_tr sep mark sfx [t, more] = foldr (op $) (gen_fields_tr sep mark sfx t, more)
   251   | gen_record_scheme_tr _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
   252 
   253 
   254 val record_type_tr = gen_record_tr "_field_types" "_field_type" field_typeN (Syntax.const "unit");
   255 val record_type_scheme_tr = gen_record_scheme_tr "_field_types" "_field_type" field_typeN;
   256 
   257 val record_tr = gen_record_tr "_fields" "_field" fieldN HOLogic.unit;
   258 val record_scheme_tr = gen_record_scheme_tr "_fields" "_field" fieldN;
   259 
   260 fun record_update_tr [t, u] =
   261       foldr (op $) (rev (gen_fields_tr "_updates" "_update" updateN u), t)
   262   | record_update_tr ts = raise TERM ("record_update_tr", ts);
   263 
   264 
   265 val parse_translation =
   266  [("_record_type", record_type_tr),
   267   ("_record_type_scheme", record_type_scheme_tr),
   268   ("_record", record_tr),
   269   ("_record_scheme", record_scheme_tr),
   270   ("_record_update", record_update_tr)];
   271 
   272 
   273 (* print translations *)
   274 
   275 fun gen_fields_tr' mark sfx (tm as Const (name_field, _) $ t $ u) =
   276       (case try (unsuffix sfx) name_field of
   277         Some name =>
   278           apfst (cons (Syntax.const mark $ Syntax.free name $ t)) (gen_fields_tr' mark sfx u)
   279       | None => ([], tm))
   280   | gen_fields_tr' _ _ tm = ([], tm);
   281 
   282 fun gen_record_tr' sep mark sfx is_unit record record_scheme tm =
   283   let
   284     val (ts, u) = gen_fields_tr' mark sfx tm;
   285     val t' = foldr1 (fn (v, w) => Syntax.const sep $ v $ w) ts;
   286   in
   287     if is_unit u then Syntax.const record $ t'
   288     else Syntax.const record_scheme $ t' $ u
   289   end;
   290 
   291 
   292 val record_type_tr' =
   293   gen_record_tr' "_field_types" "_field_type" field_typeN
   294     (fn Const ("unit", _) => true | _ => false) "_record_type" "_record_type_scheme";
   295 
   296 val record_tr' =
   297   gen_record_tr' "_fields" "_field" fieldN HOLogic.is_unit "_record" "_record_scheme";
   298 
   299 fun record_update_tr' tm =
   300   let val (ts, u) = gen_fields_tr' "_update" updateN tm in
   301     Syntax.const "_record_update" $ u $
   302       foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts)
   303   end;
   304 
   305 
   306 fun gen_field_tr' sfx tr' name =
   307   let val name_sfx = suffix sfx name
   308   in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
   309 
   310 fun print_translation names =
   311   map (gen_field_tr' field_typeN record_type_tr') names @
   312   map (gen_field_tr' fieldN record_tr') names @
   313   map (gen_field_tr' updateN record_update_tr') names;
   314 
   315 
   316 
   317 (*** extend theory by record definition ***)
   318 
   319 (** record info **)
   320 
   321 (* type record_info and parent_info *)
   322 
   323 type record_info =
   324  {args: (string * sort) list,
   325   parent: (typ list * string) option,
   326   fields: (string * typ) list,
   327   simps: tthm list};
   328 
   329 type parent_info =
   330  {name: string,
   331   fields: (string * typ) list,
   332   simps: tthm list};
   333 
   334 
   335 (* data kind 'HOL/records' *)
   336 
   337 structure RecordsArgs =
   338 struct
   339   val name = "HOL/records";
   340   type T =
   341     record_info Symtab.table *                          (*records*)
   342       (thm Symtab.table * Simplifier.simpset);          (*field split rules*)
   343 
   344   val empty = (Symtab.empty, (Symtab.empty, HOL_basic_ss));
   345   val prep_ext = I;
   346   fun merge ((recs1, (sps1, ss1)), (recs2, (sps2, ss2))) =
   347     (Symtab.merge (K true) (recs1, recs2),
   348       (Symtab.merge (K true) (sps1, sps2), Simplifier.merge_ss (ss1, ss2)));
   349 
   350   fun print sg (recs, _) =
   351     let
   352       val prt_typ = Sign.pretty_typ sg;
   353       val ext_const = Sign.cond_extern sg Sign.constK;
   354 
   355       fun pretty_parent None = []
   356         | pretty_parent (Some (Ts, name)) =
   357             [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
   358 
   359       fun pretty_field (c, T) = Pretty.block
   360         [Pretty.str (ext_const c), Pretty.str " ::", Pretty.brk 1, Pretty.quote (prt_typ T)];
   361 
   362       fun pretty_record (name, {args, parent, fields, simps = _}) = Pretty.block (Pretty.fbreaks
   363         (Pretty.block [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
   364           pretty_parent parent @ map pretty_field fields));
   365     in
   366       seq (Pretty.writeln o pretty_record) (Symtab.dest recs)
   367     end;
   368 end;
   369 
   370 structure RecordsData = TheoryDataFun(RecordsArgs);
   371 val print_records = RecordsData.print;
   372 
   373 
   374 (* get and put data *)
   375 
   376 fun get_record thy name = Symtab.lookup (#1 (RecordsData.get thy), name);
   377 
   378 fun put_record name info thy =
   379   let val (tab, sp) = RecordsData.get thy
   380   in RecordsData.put (Symtab.update ((name, info), tab), sp) thy end;
   381 
   382 fun add_record_splits splits thy =
   383   let
   384     val (tab, (sps, ss)) = RecordsData.get thy;
   385     val simps = map #2 splits;
   386   in RecordsData.put (tab, (Symtab.extend (sps, splits), Simplifier.addsimps (ss, simps))) thy end;
   387 
   388 
   389 (* parent records *)
   390 
   391 fun inst_record thy (types, name) =
   392   let
   393     val sign = Theory.sign_of thy;
   394     fun err msg = error (msg ^ " parent record " ^ quote name);
   395 
   396     val {args, parent, fields, simps} =
   397       (case get_record thy name of Some info => info | None => err "Unknown");
   398     val _ = if length types <> length args then err "Bad number of arguments for" else ();
   399 
   400     fun bad_inst ((x, S), T) =
   401       if Sign.of_sort sign (T, S) then None else Some x
   402     val bads = mapfilter bad_inst (args ~~ types);
   403 
   404     val inst = map fst args ~~ types;
   405     val subst = Term.map_type_tfree (fn (x, _) => the (assoc (inst, x)));
   406   in
   407     if not (null bads) then
   408       err ("Ill-sorted instantiation of " ^ commas bads ^ " in")
   409     else (apsome (apfst (map subst)) parent, map (apsnd subst) fields, simps)
   410   end;
   411 
   412 fun add_parents thy (None, parents) = parents
   413   | add_parents thy (Some (types, name), parents) =
   414       let val (pparent, pfields, psimps) = inst_record thy (types, name)
   415       in add_parents thy (pparent, {name = name, fields = pfields, simps = psimps} :: parents) end;
   416 
   417 
   418 
   419 (** record field splitting **)
   420 
   421 fun record_split_tac i st =
   422   let
   423     val (_, (sps, ss)) = RecordsData.get_sg (Thm.sign_of_thm st);
   424 
   425     fun is_fieldT (_, Type (a, [_, _])) = is_some (Symtab.lookup (sps, a))
   426       | is_fieldT _ = false;
   427     val params = Logic.strip_params (Library.nth_elem (i - 1, Thm.prems_of st));
   428   in
   429     if exists is_fieldT params then Simplifier.full_simp_tac ss i st
   430     else Seq.empty
   431   end handle Library.LIST _ => Seq.empty;
   432 
   433 val record_split_name = "record_split_tac";
   434 val record_split_wrapper = (record_split_name, fn tac => record_split_tac ORELSE' tac);
   435 
   436 
   437 
   438 (** internal theory extenders **)
   439 
   440 (* field_type_defs *)
   441 
   442 fun field_type_def ((thy, simps, injects), (name, tname, vs, T, U)) =
   443   let
   444     val full = Sign.full_name (sign_of thy);
   445     val (thy', {simps = simps', inject, ...}) =
   446       thy
   447       |> setmp DatatypePackage.quiet_mode true
   448         (DatatypePackage.add_datatype_i true [tname]
   449           [(vs, tname, Syntax.NoSyn, [(name, [T, U], Syntax.NoSyn)])]);
   450     val thy'' =
   451       thy'
   452       |> setmp AxClass.quiet_mode true
   453         (AxClass.add_inst_arity_i (full tname, [HOLogic.termS, moreS], moreS) [] [] None);
   454   in (thy'', simps' @ simps, flat inject @ injects) end;
   455 
   456 fun field_type_defs args thy = foldl field_type_def ((thy, [], []), args);
   457 
   458 
   459 (* field_definitions *)
   460 
   461 fun field_definitions fields names zeta moreT more vars named_vars thy =
   462   let
   463     val sign = Theory.sign_of thy;
   464     val base = Sign.base_name;
   465     val full_path = Sign.full_name_path sign;
   466 
   467 
   468     (* prepare declarations and definitions *)
   469 
   470     (*field types*)
   471     fun mk_fieldT_spec c =
   472       (suffix raw_fieldN c, suffix field_typeN c,
   473         ["'a", zeta], TFree ("'a", HOLogic.termS), moreT);
   474     val fieldT_specs = map (mk_fieldT_spec o base) names;
   475 
   476     (*field constructors*)
   477     val field_decls = map (mk_fieldC moreT) fields;
   478 
   479     fun mk_field_spec (c, v) =
   480       mk_field ((c, v), more) :== mk_raw_field ((c, v), more);
   481     val field_specs = map mk_field_spec named_vars;
   482 
   483     (*field destructors*)
   484     val dest_decls = map (mk_fstC moreT) fields @ map (mk_sndC moreT) fields;
   485 
   486     fun mk_dest_spec dest f (c, T) =
   487       let val p = Free ("p", mk_fieldT ((c, T), moreT));
   488       in dest p :== mk_prod_case (suffix field_typeN c) (f T moreT) p end;
   489     val dest_specs =
   490       map (mk_dest_spec mk_fst fst_fn) fields @
   491       map (mk_dest_spec mk_snd snd_fn) fields;
   492 
   493 
   494     (* prepare theorems *)
   495 
   496     (*destructor conversions*)
   497     fun mk_dest_prop dest dest' (c, v) =
   498       dest (mk_field ((c, v), more)) === dest' (v, more);
   499     val dest_props =
   500       map (mk_dest_prop mk_fst fst) named_vars @
   501       map (mk_dest_prop mk_snd snd) named_vars;
   502 
   503     (*surjective pairing*)
   504     fun mk_surj_prop (c, T) =
   505       let val p = Free ("p", mk_fieldT ((c, T), moreT));
   506       in p === mk_field ((c, mk_fst p), mk_snd p) end;
   507     val surj_props = map mk_surj_prop fields;
   508 
   509 
   510     (* 1st stage: types_thy *)
   511 
   512     val (types_thy, simps, raw_injects) =
   513       thy
   514       |> field_type_defs fieldT_specs;
   515 
   516     val datatype_simps = map Attribute.tthm_of simps;
   517 
   518 
   519     (* 2nd stage: defs_thy *)
   520 
   521     val defs_thy =
   522       types_thy
   523        |> (Theory.add_consts_i o map (Syntax.no_syn o apfst base))
   524          (field_decls @ dest_decls)
   525        |> (PureThy.add_defs_i o map (fn x => (x, [Attribute.tag_internal])))
   526          (field_specs @ dest_specs);
   527 
   528     val field_defs = get_defs defs_thy field_specs;
   529     val dest_defs = get_defs defs_thy dest_specs;
   530 
   531     val injects = map (simp (map (apfst Thm.symmetric) field_defs))
   532       (map Attribute.tthm_of raw_injects);
   533 
   534 
   535     (* 3rd stage: thms_thy *)
   536 
   537     val prove = prove_simp defs_thy;
   538 
   539     val dest_convs = map (prove [] (field_defs @ dest_defs @ datatype_simps)) dest_props;
   540     val surj_pairs = map (prove [DatatypePackage.induct_tac "p" 1]
   541       (map (apfst Thm.symmetric) field_defs @ dest_convs)) surj_props;
   542 
   543     fun mk_split th = SplitPairedAll.rule (th RS eq_reflection);
   544     val splits = map (fn (th, _) => Attribute.tthm_of (mk_split th)) surj_pairs;
   545 
   546     val thms_thy =
   547       defs_thy
   548       |> (PureThy.add_tthmss o map Attribute.none)
   549         [("field_defs", field_defs),
   550           ("dest_defs", dest_defs),
   551           ("dest_convs", dest_convs),
   552           ("surj_pairs", surj_pairs),
   553           ("splits", splits)];
   554 
   555   in (thms_thy, dest_convs, injects, splits) end;
   556 
   557 
   558 (* record_definition *)
   559 
   560 fun record_definition (args, bname) parent (parents: parent_info list) bfields thy =
   561   let
   562     val sign = Theory.sign_of thy;
   563     val full = Sign.full_name_path sign bname;
   564     val base = Sign.base_name;
   565 
   566 
   567     (* basic components *)
   568 
   569     val alphas = map fst args;
   570     val name = Sign.full_name sign bname;       (*not made part of record name space!*)
   571 
   572     val parent_fields = flat (map #fields parents);
   573     val parent_names = map fst parent_fields;
   574     val parent_types = map snd parent_fields;
   575     val parent_len = length parent_fields;
   576     val parent_xs = variantlist (map (base o fst) parent_fields, [moreN]);
   577     val parent_vars = ListPair.map Free (parent_xs, parent_types);
   578     val parent_named_vars = parent_names ~~ parent_vars;
   579 
   580     val fields = map (apfst full) bfields;
   581     val names = map fst fields;
   582     val types = map snd fields;
   583     val len = length fields;
   584     val xs = variantlist (map fst bfields, moreN :: parent_xs);
   585     val vars = ListPair.map Free (xs, types);
   586     val named_vars = names ~~ vars;
   587 
   588     val all_fields = parent_fields @ fields;
   589     val all_names = parent_names @ names;
   590     val all_types = parent_types @ types;
   591     val all_len = parent_len + len;
   592     val all_xs = parent_xs @ xs;
   593     val all_vars = parent_vars @ vars;
   594     val all_named_vars = parent_named_vars @ named_vars;
   595 
   596     val zeta = variant alphas "'z";
   597     val moreT = TFree (zeta, moreS);
   598     val more = Free (moreN, moreT);
   599     val full_moreN = full moreN;
   600     fun more_part t = mk_more t full_moreN;
   601     fun more_part_update t x = mk_more_update t (full_moreN, x);
   602 
   603     val parent_more = funpow parent_len mk_snd;
   604     val idxs = 0 upto (len - 1);
   605 
   606     val rec_schemeT = mk_recordT (all_fields, moreT);
   607     val rec_scheme = mk_record (all_named_vars, more);
   608     val r = Free ("r", rec_schemeT);
   609     val recT = mk_recordT (all_fields, HOLogic.unitT);
   610 
   611 
   612     (* prepare print translation functions *)
   613 
   614     val field_tr's =
   615       print_translation (distinct (flat (map NameSpace.accesses (full_moreN :: names))));
   616 
   617 
   618     (* prepare declarations *)
   619 
   620     val sel_decls = map (mk_selC rec_schemeT) bfields @
   621       [mk_moreC rec_schemeT (moreN, moreT)];
   622     val update_decls = map (mk_updateC rec_schemeT) bfields @
   623       [mk_more_updateC rec_schemeT (moreN, moreT)];
   624     val make_decls =
   625       [(mk_makeC rec_schemeT (make_schemeN, all_types @ [moreT])),
   626        (mk_makeC recT (makeN, all_types))];
   627 
   628 
   629     (* prepare definitions *)
   630 
   631     (*record (scheme) type abbreviation*)
   632     val recordT_specs =
   633       [(suffix schemeN bname, alphas @ [zeta], rec_schemeT, Syntax.NoSyn),
   634         (bname, alphas, recT, Syntax.NoSyn)];
   635 
   636     (*selectors*)
   637     fun mk_sel_spec (i, c) =
   638       mk_sel r c :== mk_fst (funpow i mk_snd (parent_more r));
   639     val sel_specs =
   640       ListPair.map mk_sel_spec (idxs, names) @
   641         [more_part r :== funpow len mk_snd (parent_more r)];
   642 
   643     (*updates*)
   644     val all_sels = all_names ~~ map (mk_sel r) all_names;
   645     fun mk_upd_spec (i, (c, x)) =
   646       mk_update r (c, x) :==
   647         mk_record (nth_update (c, x) (parent_len + i, all_sels), more_part r)
   648     val update_specs =
   649       ListPair.map mk_upd_spec (idxs, named_vars) @
   650         [more_part_update r more :== mk_record (all_sels, more)];
   651 
   652     (*makes*)
   653     val make_scheme = Const (mk_makeC rec_schemeT (full make_schemeN, all_types @ [moreT]));
   654     val make = Const (mk_makeC recT (full makeN, all_types));
   655     val make_specs =
   656       [list_comb (make_scheme, all_vars) $ more :== rec_scheme,
   657         list_comb (make, all_vars) :== mk_record (all_named_vars, HOLogic.unit)];
   658 
   659 
   660     (* prepare propositions *)
   661 
   662     (*selectors*)
   663     val sel_props =
   664       map (fn (c, x) => mk_sel rec_scheme c === x) named_vars @
   665         [more_part rec_scheme === more];
   666 
   667     (*updates*)
   668     fun mk_upd_prop (i, (c, T)) =
   669       let val x' = Free (variant all_xs (base c ^ "'"), T) in
   670         mk_update rec_scheme (c, x') ===
   671           mk_record (nth_update (c, x') (parent_len + i, all_named_vars), more)
   672       end;
   673     val update_props =
   674       ListPair.map mk_upd_prop (idxs, fields) @
   675         let val more' = Free (variant all_xs (moreN ^ "'"), moreT)
   676         in [more_part_update rec_scheme more' === mk_record (all_named_vars, more')] end;
   677 
   678 
   679     (* 1st stage: fields_thy *)
   680 
   681     val (fields_thy, field_simps, field_injects, splits) =
   682       thy
   683       |> Theory.add_path bname
   684       |> field_definitions fields names zeta moreT more vars named_vars;
   685 
   686     val field_splits = map2 (fn (c, (th, _)) => (suffix field_typeN c, th)) (names, splits);
   687 
   688 
   689     (* 2nd stage: defs_thy *)
   690 
   691     val defs_thy =
   692       fields_thy
   693       |> Theory.parent_path
   694       |> Theory.add_tyabbrs_i recordT_specs     (*not made part of record name space!*)
   695       |> Theory.add_path bname
   696       |> Theory.add_trfuns ([], [], field_tr's, [])
   697       |> (Theory.add_consts_i o map Syntax.no_syn)
   698         (sel_decls @ update_decls @ make_decls)
   699       |> (PureThy.add_defs_i o map (fn x => (x, [Attribute.tag_internal])))
   700         (sel_specs @ update_specs)
   701       |> (PureThy.add_defs_i o map Attribute.none) make_specs;
   702 
   703     val sel_defs = get_defs defs_thy sel_specs;
   704     val update_defs = get_defs defs_thy update_specs;
   705     val make_defs = get_defs defs_thy make_specs;
   706 
   707 
   708     (* 3rd stage: thms_thy *)
   709 
   710     val parent_simps = flat (map #simps parents);
   711     val prove = prove_simp defs_thy [];
   712 
   713     val sel_convs = map (prove (parent_simps @ sel_defs @ field_simps)) sel_props;
   714     val update_convs = map (prove (parent_simps @ update_defs @ sel_convs)) update_props;
   715 
   716     val simps = field_simps @ sel_convs @ update_convs @ make_defs;
   717 
   718     val thms_thy =
   719       defs_thy
   720       |> (PureThy.add_tthmss o map Attribute.none)
   721         [("select_defs", sel_defs),
   722           ("update_defs", update_defs),
   723           ("make_defs", make_defs),
   724           ("select_convs", sel_convs),
   725           ("update_convs", update_convs)]
   726       |> PureThy.add_tthmss
   727         [(("simps", simps), [Simplifier.simp_add_global]),
   728          (("injects", field_injects), [add_iffs_global])];
   729 
   730 
   731     (* 4th stage: final_thy *)
   732 
   733     val final_thy =
   734       thms_thy
   735       |> put_record name {args = args, parent = parent, fields = fields, simps = simps}
   736       |> add_record_splits field_splits
   737       |> Theory.parent_path;
   738 
   739   in final_thy end;
   740 
   741 
   742 
   743 (** theory extender interface **)
   744 
   745 (* prepare arguments *)
   746 
   747 (*note: read_raw_typ avoids expanding type abbreviations*)
   748 fun read_raw_parent sign s =
   749   (case Sign.read_raw_typ (sign, K None) s handle TYPE (msg, _, _) => error msg of
   750     Type (name, Ts) => (Ts, name)
   751   | _ => error ("Bad parent record specification: " ^ quote s));
   752 
   753 fun read_typ sign (env, s) =
   754   let
   755     fun def_sort (x, ~1) = assoc (env, x)
   756       | def_sort _ = None;
   757     val T = Type.no_tvars (Sign.read_typ (sign, def_sort) s) handle TYPE (msg, _, _) => error msg;
   758   in (Term.add_typ_tfrees (T, env), T) end;
   759 
   760 fun cert_typ sign (env, raw_T) =
   761   let val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle TYPE (msg, _, _) => error msg
   762   in (Term.add_typ_tfrees (T, env), T) end;
   763 
   764 
   765 (* add_record *)
   766 
   767 (*we do all preparations and error checks here, deferring the real
   768   work to record_definition*)
   769 
   770 fun gen_add_record prep_typ prep_raw_parent (params, bname) raw_parent raw_fields thy =
   771   let
   772     val _ = Theory.requires thy "Record" "record definitions";
   773     val sign = Theory.sign_of thy;
   774     val _ = message ("Defining record " ^ quote bname ^ " ...");
   775 
   776 
   777     (* parents *)
   778 
   779     fun prep_inst T = snd (cert_typ sign ([], T));
   780 
   781     val parent = apsome (apfst (map prep_inst) o prep_raw_parent sign) raw_parent
   782       handle ERROR => error ("The error(s) above in parent record specification");
   783     val parents = add_parents thy (parent, []);
   784 
   785     val init_env =
   786       (case parent of
   787         None => []
   788       | Some (types, _) => foldr Term.add_typ_tfrees (types, []));
   789 
   790 
   791     (* fields *)
   792 
   793     fun prep_field (env, (c, raw_T)) =
   794       let val (env', T) = prep_typ sign (env, raw_T) handle ERROR =>
   795         error ("The error(s) above occured in field " ^ quote c)
   796       in (env', (c, T)) end;
   797 
   798     val (envir, bfields) = foldl_map prep_field (init_env, raw_fields);
   799     val envir_names = map fst envir;
   800 
   801 
   802     (* args *)
   803 
   804     val defaultS = Sign.defaultS sign;
   805     val args = map (fn x => (x, if_none (assoc (envir, x)) defaultS)) params;
   806 
   807 
   808     (* errors *)
   809 
   810     val name = Sign.full_name sign bname;
   811     val err_dup_record =
   812       if is_none (get_record thy name) then []
   813       else ["Duplicate definition of record " ^ quote name];
   814 
   815     val err_dup_parms =
   816       (case duplicates params of
   817         [] => []
   818       | dups => ["Duplicate parameter(s) " ^ commas dups]);
   819 
   820     val err_extra_frees =
   821       (case gen_rems (op =) (envir_names, params) of
   822         [] => []
   823       | extras => ["Extra free type variable(s) " ^ commas extras]);
   824 
   825     val err_no_fields = if null bfields then ["No fields present"] else [];
   826 
   827     val err_dup_fields =
   828       (case duplicates (map fst bfields) of
   829         [] => []
   830       | dups => ["Duplicate field(s) " ^ commas_quote dups]);
   831 
   832     val err_bad_fields =
   833       if forall (not_equal moreN o fst) bfields then []
   834       else ["Illegal field name " ^ quote moreN];
   835 
   836     val err_dup_sorts =
   837       (case duplicates envir_names of
   838         [] => []
   839       | dups => ["Inconsistent sort constraints for " ^ commas dups]);
   840 
   841     val errs =
   842       err_dup_record @ err_dup_parms @ err_extra_frees @ err_no_fields @
   843       err_dup_fields @ err_bad_fields @ err_dup_sorts;
   844   in
   845     if null errs then () else error (cat_lines errs);
   846     thy |> record_definition (args, bname) parent parents bfields
   847   end
   848   handle ERROR => error ("Failed to define record " ^ quote bname);
   849 
   850 val add_record = gen_add_record read_typ read_raw_parent;
   851 val add_record_i = gen_add_record cert_typ (K I);
   852 
   853 
   854 
   855 (** setup theory **)
   856 
   857 val setup =
   858  [RecordsData.init,
   859   Theory.add_trfuns ([], parse_translation, [], []),
   860   add_wrapper record_split_wrapper];
   861 
   862 
   863 end;
   864 
   865 
   866 structure BasicRecordPackage: BASIC_RECORD_PACKAGE = RecordPackage;
   867 open BasicRecordPackage;