src/HOL/Tools/record.ML
author wenzelm
Tue Sep 29 21:34:59 2009 +0200 (2009-09-29)
changeset 32761 54fee94b2b29
parent 32760 ea6672bff5dd
child 32763 ebfaf9e3c03a
permissions -rw-r--r--
tuned whitespace -- recover basic Isabelle conventions;
     1 (*  Title:      HOL/Tools/record.ML
     2     Authors:    Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
     3                 Thomas Sewell, NICTA
     4 
     5 Extensible records with structural subtyping in HOL.
     6 *)
     7 
     8 signature BASIC_RECORD =
     9 sig
    10   val record_simproc: simproc
    11   val record_eq_simproc: simproc
    12   val record_upd_simproc: simproc
    13   val record_split_simproc: (term -> int) -> simproc
    14   val record_ex_sel_eq_simproc: simproc
    15   val record_split_tac: int -> tactic
    16   val record_split_simp_tac: thm list -> (term -> int) -> int -> tactic
    17   val record_split_name: string
    18   val record_split_wrapper: string * wrapper
    19   val print_record_type_abbr: bool Unsynchronized.ref
    20   val print_record_type_as_fields: bool Unsynchronized.ref
    21 end;
    22 
    23 signature RECORD =
    24 sig
    25   include BASIC_RECORD
    26   val timing: bool Unsynchronized.ref
    27   val record_quick_and_dirty_sensitive: bool Unsynchronized.ref
    28   val updateN: string
    29   val updN: string
    30   val ext_typeN: string
    31   val extN: string
    32   val makeN: string
    33   val moreN: string
    34   val ext_dest: string
    35 
    36   val last_extT: typ -> (string * typ list) option
    37   val dest_recTs : typ -> (string * typ list) list
    38   val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ)
    39   val get_recT_fields: theory -> typ -> (string * typ) list * (string * typ)
    40   val get_parent: theory -> string -> (typ list * string) option
    41   val get_extension: theory -> string -> (string * typ list) option
    42   val get_extinjects: theory -> thm list
    43   val get_simpset: theory -> simpset
    44   val print_records: theory -> unit
    45   val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list
    46   val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list
    47   val add_record: bool -> string list * string -> string option -> (string * string * mixfix) list
    48     -> theory -> theory
    49   val add_record_i: bool -> string list * string -> (typ list * string) option
    50     -> (string * typ * mixfix) list -> theory -> theory
    51   val setup: theory -> theory
    52 end;
    53 
    54 
    55 signature ISTUPLE_SUPPORT =
    56 sig
    57   val add_istuple_type: bstring * string list -> (typ * typ) -> theory -> term * term * theory
    58 
    59   val mk_cons_tuple: term * term -> term
    60   val dest_cons_tuple: term -> term * term
    61 
    62   val istuple_intros_tac: theory -> int -> tactic
    63 
    64   val named_cterm_instantiate: (string * cterm) list -> thm -> thm
    65 end;
    66 
    67 structure IsTupleSupport: ISTUPLE_SUPPORT =
    68 struct
    69 
    70 val isomN = "_TupleIsom";
    71 val defN = "_def";
    72 
    73 val istuple_UNIV_I = @{thm "istuple_UNIV_I"};
    74 val istuple_True_simp = @{thm "istuple_True_simp"};
    75 
    76 val istuple_intro = @{thm "isomorphic_tuple_intro"};
    77 val istuple_intros = build_net (@{thms "isomorphic_tuple.intros"});
    78 
    79 val constname = fst o dest_Const;
    80 val tuple_istuple = (constname @{term tuple_istuple}, @{thm tuple_istuple});
    81 
    82 val istuple_constN = constname @{term isomorphic_tuple};
    83 val istuple_consN = constname @{term istuple_cons};
    84 
    85 val tup_isom_typeN = fst (dest_Type @{typ "('a, 'b, 'c) tuple_isomorphism"});
    86 
    87 fun named_cterm_instantiate values thm =
    88   let
    89     fun match name ((name', _), _) = name = name'
    90       | match name _ = false;
    91     fun getvar name =
    92       (case find_first (match name) (Term.add_vars (prop_of thm) []) of
    93         SOME var => cterm_of (theory_of_thm thm) (Var var)
    94       | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm]));
    95   in
    96     cterm_instantiate (map (apfst getvar) values) thm
    97   end;
    98 
    99 structure IsTupleThms = TheoryDataFun
   100 (
   101   type T = thm Symtab.table;
   102   val empty = Symtab.make [tuple_istuple];
   103   val copy = I;
   104   val extend = I;
   105   val merge = K (Symtab.merge Thm.eq_thm_prop);
   106 );
   107 
   108 fun do_typedef name repT alphas thy =
   109   let
   110     fun get_thms thy name =
   111       let
   112         val SOME { Rep_inject=rep_inject, Abs_name=absN, abs_type=absT,
   113           Abs_inverse=abs_inverse, ...} = Typedef.get_info thy name;
   114         val rewrite_rule = MetaSimplifier.rewrite_rule [istuple_UNIV_I, istuple_True_simp];
   115       in (map rewrite_rule [rep_inject, abs_inverse],
   116             Const (absN, repT --> absT), absT) end;
   117   in
   118     thy
   119     |> Typecopy.typecopy (Binding.name name, alphas) repT NONE
   120     |-> (fn (name, _) => `(fn thy => get_thms thy name))
   121   end;
   122 
   123 fun mk_cons_tuple (left, right) =
   124   let
   125     val (leftT, rightT) = (fastype_of left, fastype_of right);
   126     val prodT = HOLogic.mk_prodT (leftT, rightT);
   127     val isomT = Type (tup_isom_typeN, [prodT, leftT, rightT]);
   128   in
   129     Const (istuple_consN, isomT --> leftT --> rightT --> prodT) $
   130       Const (fst tuple_istuple, isomT) $ left $ right
   131   end;
   132 
   133 fun dest_cons_tuple (v as Const (ic, _) $ Const _ $ left $ right) =
   134       if ic = istuple_consN then (left, right)
   135       else raise TERM ("dest_cons_tuple", [v])
   136   | dest_cons_tuple v = raise TERM ("dest_cons_tuple", [v]);
   137 
   138 fun add_istuple_type (name, alphas) (leftT, rightT) thy =
   139   let
   140     val repT = HOLogic.mk_prodT (leftT, rightT);
   141 
   142     val (([rep_inject, abs_inverse], absC, absT), typ_thy) =
   143       thy
   144       |> do_typedef name repT alphas
   145       ||> Sign.add_path name;
   146 
   147     (*construct a type and body for the isomorphism constant by
   148       instantiating the theorem to which the definition will be applied*)
   149     val intro_inst =
   150       rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] istuple_intro;
   151     val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
   152     val isomT = fastype_of body;
   153     val isom_bind = Binding.name (name ^ isomN);
   154     val isom = Const (Sign.full_name typ_thy isom_bind, isomT);
   155     val isom_spec = (name ^ isomN ^ defN, Logic.mk_equals (isom, body));
   156 
   157     val ([isom_def], cdef_thy) =
   158       typ_thy
   159       |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)]
   160       |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)];
   161 
   162     val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro));
   163     val cons = Const (istuple_consN, isomT --> leftT --> rightT --> absT);
   164 
   165     val thm_thy =
   166       cdef_thy
   167       |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop (constname isom, istuple))
   168       |> Sign.parent_path;
   169   in
   170     (isom, cons $ isom, thm_thy)
   171   end;
   172 
   173 fun istuple_intros_tac thy =
   174   let
   175     val isthms = IsTupleThms.get thy;
   176     fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]);
   177     val use_istuple_thm_tac = SUBGOAL (fn (goal, n) =>
   178       let
   179         val goal' = Envir.beta_eta_contract goal;
   180         val isom =
   181           (case goal' of
   182             Const tp $ (Const pr $ Const is) =>
   183               if fst tp = "Trueprop" andalso fst pr = istuple_constN
   184               then Const is
   185               else err "unexpected goal predicate" goal'
   186           | _ => err "unexpected goal format" goal');
   187         val isthm =
   188           (case Symtab.lookup isthms (constname isom) of
   189             SOME isthm => isthm
   190           | NONE => err "no thm found for constant" isom);
   191       in rtac isthm n end);
   192   in
   193     fn n => resolve_from_net_tac istuple_intros n THEN use_istuple_thm_tac n
   194   end;
   195 
   196 end;
   197 
   198 
   199 structure Record: RECORD =
   200 struct
   201 
   202 val eq_reflection = thm "eq_reflection";
   203 val Pair_eq = thm "Product_Type.prod.inject";
   204 val atomize_all = thm "HOL.atomize_all";
   205 val atomize_imp = thm "HOL.atomize_imp";
   206 val meta_allE = thm "Pure.meta_allE";
   207 val prop_subst = thm "prop_subst";
   208 val Pair_sel_convs = [fst_conv, snd_conv];
   209 val K_record_comp = @{thm "K_record_comp"};
   210 val K_comp_convs = [@{thm o_apply}, K_record_comp]
   211 val transitive_thm = thm "transitive";
   212 val o_assoc = @{thm "o_assoc"};
   213 val id_apply = @{thm id_apply};
   214 val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}];
   215 val Not_eq_iff = @{thm Not_eq_iff};
   216 
   217 val refl_conj_eq = thm "refl_conj_eq";
   218 val meta_all_sameI = thm "meta_all_sameI";
   219 val meta_iffD2 = thm "meta_iffD2";
   220 
   221 val surject_assistI = @{thm "istuple_surjective_proof_assistI"};
   222 val surject_assist_idE = @{thm "istuple_surjective_proof_assist_idE"};
   223 
   224 val updacc_accessor_eqE = @{thm "update_accessor_accessor_eqE"};
   225 val updacc_updator_eqE = @{thm "update_accessor_updator_eqE"};
   226 val updacc_eq_idI = @{thm "istuple_update_accessor_eq_assist_idI"};
   227 val updacc_eq_triv = @{thm "istuple_update_accessor_eq_assist_triv"};
   228 
   229 val updacc_foldE = @{thm "update_accessor_congruence_foldE"};
   230 val updacc_unfoldE = @{thm "update_accessor_congruence_unfoldE"};
   231 val updacc_noopE = @{thm "update_accessor_noopE"};
   232 val updacc_noop_compE = @{thm "update_accessor_noop_compE"};
   233 val updacc_cong_idI = @{thm "update_accessor_cong_assist_idI"};
   234 val updacc_cong_triv = @{thm "update_accessor_cong_assist_triv"};
   235 val updacc_cong_from_eq = @{thm "istuple_update_accessor_cong_from_eq"};
   236 
   237 val o_eq_dest = thm "o_eq_dest";
   238 val o_eq_id_dest = thm "o_eq_id_dest";
   239 val o_eq_dest_lhs = thm "o_eq_dest_lhs";
   240 
   241 
   242 
   243 (** name components **)
   244 
   245 val rN = "r";
   246 val wN = "w";
   247 val moreN = "more";
   248 val schemeN = "_scheme";
   249 val ext_typeN = "_ext_type";
   250 val inner_typeN = "_inner_type";
   251 val extN ="_ext";
   252 val casesN = "_cases";
   253 val ext_dest = "_sel";
   254 val updateN = "_update";
   255 val updN = "_upd";
   256 val makeN = "make";
   257 val fields_selN = "fields";
   258 val extendN = "extend";
   259 val truncateN = "truncate";
   260 
   261 (*see typedef.ML*)
   262 val RepN = "Rep_";
   263 val AbsN = "Abs_";
   264 
   265 
   266 
   267 (*** utilities ***)
   268 
   269 fun but_last xs = fst (split_last xs);
   270 
   271 fun varifyT midx =
   272   let fun varify (a, S) = TVar ((a, midx + 1), S);
   273   in map_type_tfree varify end;
   274 
   275 fun domain_type' T =
   276   domain_type T handle Match => T;
   277 
   278 fun range_type' T =
   279   range_type T handle Match => T;
   280 
   281 
   282 (* messages *)  (* FIXME proper context *)
   283 
   284 fun trace_thm str thm =
   285   tracing (str ^ Pretty.string_of (Display.pretty_thm_without_context thm));
   286 
   287 fun trace_thms str thms =
   288   (tracing str; map (trace_thm "") thms);
   289 
   290 fun trace_term str t =
   291   tracing (str ^ Syntax.string_of_term_global Pure.thy t);
   292 
   293 
   294 (* timing *)
   295 
   296 val timing = Unsynchronized.ref false;
   297 fun timeit_msg s x = if ! timing then (warning s; timeit x) else x ();
   298 fun timing_msg s = if ! timing then warning s else ();
   299 
   300 
   301 (* syntax *)
   302 
   303 fun prune n xs = Library.drop (n, xs);
   304 fun prefix_base s = Long_Name.map_base_name (fn bname => s ^ bname);
   305 
   306 val Trueprop = HOLogic.mk_Trueprop;
   307 fun All xs t = Term.list_all_free (xs, t);
   308 
   309 infix 9 $$;
   310 infix 0 :== ===;
   311 infixr 0 ==>;
   312 
   313 val (op $$) = Term.list_comb;
   314 val (op :==) = PrimitiveDefs.mk_defpair;
   315 val (op ===) = Trueprop o HOLogic.mk_eq;
   316 val (op ==>) = Logic.mk_implies;
   317 
   318 
   319 (* morphisms *)
   320 
   321 fun mk_RepN name = suffix ext_typeN (prefix_base RepN name);
   322 fun mk_AbsN name = suffix ext_typeN (prefix_base AbsN name);
   323 
   324 fun mk_Rep name repT absT =
   325   Const (suffix ext_typeN (prefix_base RepN name), absT --> repT);
   326 
   327 fun mk_Abs name repT absT =
   328   Const (mk_AbsN name, repT --> absT);
   329 
   330 
   331 (* constructor *)
   332 
   333 fun mk_extC (name, T) Ts = (suffix extN name, Ts ---> T);
   334 
   335 fun mk_ext (name, T) ts =
   336   let val Ts = map fastype_of ts
   337   in list_comb (Const (mk_extC (name, T) Ts), ts) end;
   338 
   339 
   340 (* cases *)
   341 
   342 fun mk_casesC (name, T, vT) Ts = (suffix casesN name, (Ts ---> vT) --> T --> vT);
   343 
   344 fun mk_cases (name, T, vT) f =
   345   let val Ts = binder_types (fastype_of f)
   346   in Const (mk_casesC (name, T, vT) Ts) $ f end;
   347 
   348 
   349 (* selector *)
   350 
   351 fun mk_selC sT (c, T) = (c, sT --> T);
   352 
   353 fun mk_sel s (c, T) =
   354   let val sT = fastype_of s
   355   in Const (mk_selC sT (c, T)) $ s end;
   356 
   357 
   358 (* updates *)
   359 
   360 fun mk_updC sfx sT (c, T) = (suffix sfx c, (T --> T) --> sT --> sT);
   361 
   362 fun mk_upd' sfx c v sT =
   363   let val vT = domain_type (fastype_of v);
   364   in Const (mk_updC sfx sT (c, vT)) $ v end;
   365 
   366 fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s;
   367 
   368 
   369 (* types *)
   370 
   371 fun dest_recT (typ as Type (c_ext_type, Ts as (T :: _))) =
   372       (case try (unsuffix ext_typeN) c_ext_type of
   373         NONE => raise TYPE ("Record.dest_recT", [typ], [])
   374       | SOME c => ((c, Ts), List.last Ts))
   375   | dest_recT typ = raise TYPE ("Record.dest_recT", [typ], []);
   376 
   377 fun is_recT T =
   378   (case try dest_recT T of NONE => false | SOME _ => true);
   379 
   380 fun dest_recTs T =
   381   let val ((c, Ts), U) = dest_recT T
   382   in (c, Ts) :: dest_recTs U
   383   end handle TYPE _ => [];
   384 
   385 fun last_extT T =
   386   let val ((c, Ts), U) = dest_recT T in
   387     (case last_extT U of
   388       NONE => SOME (c, Ts)
   389     | SOME l => SOME l)
   390   end handle TYPE _ => NONE;
   391 
   392 fun rec_id i T =
   393   let
   394     val rTs = dest_recTs T;
   395     val rTs' = if i < 0 then rTs else Library.take (i, rTs);
   396   in Library.foldl (fn (s, (c, T)) => s ^ c) ("", rTs') end;   (* FIXME ? *)
   397 
   398 
   399 
   400 (*** extend theory by record definition ***)
   401 
   402 (** record info **)
   403 
   404 (* type record_info and parent_info *)
   405 
   406 type record_info =
   407  {args: (string * sort) list,
   408   parent: (typ list * string) option,
   409   fields: (string * typ) list,
   410   extension: (string * typ list),
   411   induct: thm,
   412   extdef: thm};
   413 
   414 fun make_record_info args parent fields extension induct extdef =
   415  {args = args, parent = parent, fields = fields, extension = extension,
   416   induct = induct, extdef = extdef}: record_info;
   417 
   418 
   419 type parent_info =
   420  {name: string,
   421   fields: (string * typ) list,
   422   extension: (string * typ list),
   423   induct: thm,
   424   extdef: thm};
   425 
   426 fun make_parent_info name fields extension induct extdef =
   427  {name = name, fields = fields, extension = extension,
   428   induct = induct, extdef = extdef}: parent_info;
   429 
   430 
   431 (* theory data *)
   432 
   433 type record_data =
   434  {records: record_info Symtab.table,
   435   sel_upd:
   436    {selectors: (int * bool) Symtab.table,
   437     updates: string Symtab.table,
   438     simpset: Simplifier.simpset,
   439     defset: Simplifier.simpset,
   440     foldcong: Simplifier.simpset,
   441     unfoldcong: Simplifier.simpset},
   442   equalities: thm Symtab.table,
   443   extinjects: thm list,
   444   extsplit: thm Symtab.table,  (* maps extension name to split rule *)
   445   splits: (thm*thm*thm*thm) Symtab.table,  (* !!, !, EX - split-equalities, induct rule *)
   446   extfields: (string*typ) list Symtab.table,  (* maps extension to its fields *)
   447   fieldext: (string*typ list) Symtab.table};  (* maps field to its extension *)
   448 
   449 fun make_record_data
   450     records sel_upd equalities extinjects extsplit splits extfields fieldext =
   451  {records = records, sel_upd = sel_upd,
   452   equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
   453   extfields = extfields, fieldext = fieldext }: record_data;
   454 
   455 structure RecordsData = TheoryDataFun
   456 (
   457   type T = record_data;
   458   val empty =
   459     make_record_data Symtab.empty
   460       {selectors = Symtab.empty, updates = Symtab.empty,
   461           simpset = HOL_basic_ss, defset = HOL_basic_ss,
   462           foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
   463        Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
   464 
   465   val copy = I;
   466   val extend = I;
   467   fun merge _
   468    ({records = recs1,
   469      sel_upd =
   470       {selectors = sels1, updates = upds1,
   471        simpset = ss1, defset = ds1,
   472        foldcong = fc1, unfoldcong = uc1},
   473      equalities = equalities1,
   474      extinjects = extinjects1,
   475      extsplit = extsplit1,
   476      splits = splits1,
   477      extfields = extfields1,
   478      fieldext = fieldext1},
   479     {records = recs2,
   480      sel_upd =
   481       {selectors = sels2, updates = upds2,
   482        simpset = ss2, defset = ds2,
   483        foldcong = fc2, unfoldcong = uc2},
   484      equalities = equalities2,
   485      extinjects = extinjects2,
   486      extsplit = extsplit2,
   487      splits = splits2,
   488      extfields = extfields2,
   489      fieldext = fieldext2}) =
   490     make_record_data
   491       (Symtab.merge (K true) (recs1, recs2))
   492       {selectors = Symtab.merge (K true) (sels1, sels2),
   493         updates = Symtab.merge (K true) (upds1, upds2),
   494         simpset = Simplifier.merge_ss (ss1, ss2),
   495         defset = Simplifier.merge_ss (ds1, ds2),
   496         foldcong = Simplifier.merge_ss (fc1, fc2),
   497         unfoldcong = Simplifier.merge_ss (uc1, uc2)}
   498       (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
   499       (Library.merge Thm.eq_thm_prop (extinjects1, extinjects2))
   500       (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
   501       (Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
   502           Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
   503           Thm.eq_thm (c, y) andalso Thm.eq_thm (d, z)) (splits1, splits2))
   504       (Symtab.merge (K true) (extfields1, extfields2))
   505       (Symtab.merge (K true) (fieldext1, fieldext2));
   506 );
   507 
   508 fun print_records thy =
   509   let
   510     val {records = recs, ...} = RecordsData.get thy;
   511     val prt_typ = Syntax.pretty_typ_global thy;
   512 
   513     fun pretty_parent NONE = []
   514       | pretty_parent (SOME (Ts, name)) =
   515           [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
   516 
   517     fun pretty_field (c, T) = Pretty.block
   518       [Pretty.str (Sign.extern_const thy c), Pretty.str " ::",
   519         Pretty.brk 1, Pretty.quote (prt_typ T)];
   520 
   521     fun pretty_record (name, {args, parent, fields, ...}: record_info) =
   522       Pretty.block (Pretty.fbreaks (Pretty.block
   523         [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
   524         pretty_parent parent @ map pretty_field fields));
   525   in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
   526 
   527 
   528 (* access 'records' *)
   529 
   530 val get_record = Symtab.lookup o #records o RecordsData.get;
   531 
   532 fun put_record name info thy =
   533   let
   534     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   535       RecordsData.get thy;
   536     val data = make_record_data (Symtab.update (name, info) records)
   537       sel_upd equalities extinjects extsplit splits extfields fieldext;
   538   in RecordsData.put data thy end;
   539 
   540 
   541 (* access 'sel_upd' *)
   542 
   543 val get_sel_upd = #sel_upd o RecordsData.get;
   544 
   545 val is_selector = Symtab.defined o #selectors o get_sel_upd;
   546 val get_updates = Symtab.lookup o #updates o get_sel_upd;
   547 fun get_ss_with_context getss thy =
   548     Simplifier.theory_context thy (getss (get_sel_upd thy));
   549 
   550 val get_simpset = get_ss_with_context (#simpset);
   551 val get_sel_upd_defs = get_ss_with_context (#defset);
   552 val get_foldcong_ss = get_ss_with_context (#foldcong);
   553 val get_unfoldcong_ss = get_ss_with_context (#unfoldcong);
   554 
   555 fun get_update_details u thy =
   556   let val sel_upd = get_sel_upd thy in
   557     (case Symtab.lookup (#updates sel_upd) u of
   558       SOME s =>
   559         let val SOME (dep, ismore) = Symtab.lookup (#selectors sel_upd) s
   560         in SOME (s, dep, ismore) end
   561     | NONE => NONE)
   562   end;
   563 
   564 fun put_sel_upd names more depth simps defs (folds, unfolds) thy =
   565   let
   566     val all = names @ [more];
   567     val sels = map (rpair (depth, false)) names @ [(more, (depth, true))];
   568     val upds = map (suffix updateN) all ~~ all;
   569 
   570     val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong},
   571       equalities, extinjects, extsplit, splits, extfields, fieldext} = RecordsData.get thy;
   572     val data = make_record_data records
   573       {selectors = fold Symtab.update_new sels selectors,
   574         updates = fold Symtab.update_new upds updates,
   575         simpset = Simplifier.addsimps (simpset, simps),
   576         defset = Simplifier.addsimps (defset, defs),
   577         foldcong = foldcong addcongs folds,
   578         unfoldcong = unfoldcong addcongs unfolds}
   579        equalities extinjects extsplit splits extfields fieldext;
   580   in RecordsData.put data thy end;
   581 
   582 
   583 (* access 'equalities' *)
   584 
   585 fun add_record_equalities name thm thy =
   586   let
   587     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   588       RecordsData.get thy;
   589     val data = make_record_data records sel_upd
   590       (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext;
   591   in RecordsData.put data thy end;
   592 
   593 val get_equalities = Symtab.lookup o #equalities o RecordsData.get;
   594 
   595 
   596 (* access 'extinjects' *)
   597 
   598 fun add_extinjects thm thy =
   599   let
   600     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   601       RecordsData.get thy;
   602     val data =
   603       make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
   604         extsplit splits extfields fieldext;
   605   in RecordsData.put data thy end;
   606 
   607 val get_extinjects = rev o #extinjects o RecordsData.get;
   608 
   609 
   610 (* access 'extsplit' *)
   611 
   612 fun add_extsplit name thm thy =
   613   let
   614     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   615       RecordsData.get thy;
   616     val data = make_record_data records sel_upd
   617       equalities extinjects (Symtab.update_new (name, thm) extsplit) splits
   618       extfields fieldext;
   619   in RecordsData.put data thy end;
   620 
   621 val get_extsplit = Symtab.lookup o #extsplit o RecordsData.get;
   622 
   623 
   624 (* access 'splits' *)
   625 
   626 fun add_record_splits name thmP thy =
   627   let
   628     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   629       RecordsData.get thy;
   630     val data = make_record_data records sel_upd
   631       equalities extinjects extsplit (Symtab.update_new (name, thmP) splits)
   632       extfields fieldext;
   633   in RecordsData.put data thy end;
   634 
   635 val get_splits = Symtab.lookup o #splits o RecordsData.get;
   636 
   637 
   638 (* parent/extension of named record *)
   639 
   640 val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o RecordsData.get);
   641 val get_extension = Option.map #extension oo (Symtab.lookup o #records o RecordsData.get);
   642 
   643 
   644 (* access 'extfields' *)
   645 
   646 fun add_extfields name fields thy =
   647   let
   648     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   649       RecordsData.get thy;
   650     val data =
   651       make_record_data records sel_upd
   652         equalities extinjects extsplit splits
   653         (Symtab.update_new (name, fields) extfields) fieldext;
   654   in RecordsData.put data thy end;
   655 
   656 val get_extfields = Symtab.lookup o #extfields o RecordsData.get;
   657 
   658 fun get_extT_fields thy T =
   659   let
   660     val ((name, Ts), moreT) = dest_recT T;
   661     val recname =
   662       let val (nm :: recn :: rst) = rev (Long_Name.explode name)
   663       in Long_Name.implode (rev (nm :: rst)) end;
   664     val midx = maxidx_of_typs (moreT :: Ts);
   665     val varifyT = varifyT midx;
   666     val {records, extfields, ...} = RecordsData.get thy;
   667     val (flds, (more, _)) = split_last (Symtab.lookup_list extfields name);
   668     val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
   669 
   670     val subst = fold (Sign.typ_match thy) (but_last args ~~ but_last Ts) (Vartab.empty);
   671     val flds' = map (apsnd ((Envir.norm_type subst) o varifyT)) flds;
   672   in (flds', (more, moreT)) end;
   673 
   674 fun get_recT_fields thy T =
   675   let
   676     val (root_flds, (root_more, root_moreT)) = get_extT_fields thy T;
   677     val (rest_flds, rest_more) =
   678       if is_recT root_moreT then get_recT_fields thy root_moreT
   679       else ([], (root_more, root_moreT));
   680   in (root_flds @ rest_flds, rest_more) end;
   681 
   682 
   683 (* access 'fieldext' *)
   684 
   685 fun add_fieldext extname_types fields thy =
   686   let
   687     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   688       RecordsData.get thy;
   689     val fieldext' =
   690       fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
   691     val data =
   692       make_record_data records sel_upd equalities extinjects
   693         extsplit splits extfields fieldext';
   694   in RecordsData.put data thy end;
   695 
   696 val get_fieldext = Symtab.lookup o #fieldext o RecordsData.get;
   697 
   698 
   699 (* parent records *)
   700 
   701 fun add_parents thy NONE parents = parents
   702   | add_parents thy (SOME (types, name)) parents =
   703       let
   704         fun err msg = error (msg ^ " parent record " ^ quote name);
   705 
   706         val {args, parent, fields, extension, induct, extdef} =
   707           (case get_record thy name of SOME info => info | NONE => err "Unknown");
   708         val _ = if length types <> length args then err "Bad number of arguments for" else ();
   709 
   710         fun bad_inst ((x, S), T) =
   711           if Sign.of_sort thy (T, S) then NONE else SOME x
   712         val bads = List.mapPartial bad_inst (args ~~ types);
   713         val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");
   714 
   715         val inst = map fst args ~~ types;
   716         val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
   717         val parent' = Option.map (apfst (map subst)) parent;
   718         val fields' = map (apsnd subst) fields;
   719         val extension' = apsnd (map subst) extension;
   720       in
   721         add_parents thy parent'
   722           (make_parent_info name fields' extension' induct extdef :: parents)
   723       end;
   724 
   725 
   726 
   727 (** concrete syntax for records **)
   728 
   729 (* decode type *)
   730 
   731 fun decode_type thy t =
   732   let
   733     fun get_sort xs n = AList.lookup (op =) xs (n: indexname) |> the_default (Sign.defaultS thy);
   734     val map_sort = Sign.intern_sort thy;
   735   in
   736     Syntax.typ_of_term (get_sort (Syntax.term_sorts map_sort t)) map_sort t
   737     |> Sign.intern_tycons thy
   738   end;
   739 
   740 
   741 (* parse translations *)
   742 
   743 fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) =
   744       if c = mark then Syntax.const (suffix sfx name) $ Abs ("_", dummyT, arg)
   745       else raise TERM ("gen_field_tr: " ^ mark, [t])
   746   | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]);
   747 
   748 fun gen_fields_tr sep mark sfx (tm as Const (c, _) $ t $ u) =
   749       if c = sep then gen_field_tr mark sfx t :: gen_fields_tr sep mark sfx u
   750       else [gen_field_tr mark sfx tm]
   751   | gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm];
   752 
   753 
   754 fun record_update_tr [t, u] =
   755       Library.foldr (op $) (rev (gen_fields_tr "_updates" "_update" updateN u), t)
   756   | record_update_tr ts = raise TERM ("record_update_tr", ts);
   757 
   758 fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts
   759   | update_name_tr (Const (x, T) :: ts) = Const (suffix updateN x, T) $$ ts
   760   | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
   761       (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy")) $$ ts
   762   | update_name_tr ts = raise TERM ("update_name_tr", ts);
   763 
   764 fun dest_ext_field mark (t as (Const (c, _) $ Const (name, _) $ arg)) =
   765       if c = mark then (name, arg)
   766       else raise TERM ("dest_ext_field: " ^ mark, [t])
   767   | dest_ext_field _ t = raise TERM ("dest_ext_field", [t]);
   768 
   769 fun dest_ext_fields sep mark (trm as (Const (c, _) $ t $ u)) =
   770       if c = sep then dest_ext_field mark t :: dest_ext_fields sep mark u
   771       else [dest_ext_field mark trm]
   772   | dest_ext_fields _ mark t = [dest_ext_field mark t];
   773 
   774 fun gen_ext_fields_tr sep mark sfx more ctxt t =
   775   let
   776     val thy = ProofContext.theory_of ctxt;
   777     val msg = "error in record input: ";
   778 
   779     val fieldargs = dest_ext_fields sep mark t;
   780     fun splitargs (field :: fields) ((name, arg) :: fargs) =
   781           if can (unsuffix name) field
   782           then
   783             let val (args, rest) = splitargs fields fargs
   784             in (arg :: args, rest) end
   785           else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t])
   786       | splitargs [] (fargs as (_ :: _)) = ([], fargs)
   787       | splitargs (_ :: _) [] = raise TERM (msg ^ "expecting more fields", [t])
   788       | splitargs _ _ = ([], []);
   789 
   790     fun mk_ext (fargs as (name, arg) :: _) =
   791           (case get_fieldext thy (Sign.intern_const thy name) of
   792             SOME (ext, _) =>
   793               (case get_extfields thy ext of
   794                 SOME flds =>
   795                   let
   796                     val (args, rest) = splitargs (map fst (but_last flds)) fargs;
   797                     val more' = mk_ext rest;
   798                   in list_comb (Syntax.const (suffix sfx ext), args @ [more']) end
   799               | NONE => raise TERM (msg ^ "no fields defined for " ^ ext, [t]))
   800           | NONE => raise TERM (msg ^ name ^" is no proper field", [t]))
   801       | mk_ext [] = more;
   802   in mk_ext fieldargs end;
   803 
   804 fun gen_ext_type_tr sep mark sfx more ctxt t =
   805   let
   806     val thy = ProofContext.theory_of ctxt;
   807     val msg = "error in record-type input: ";
   808 
   809     val fieldargs = dest_ext_fields sep mark t;
   810     fun splitargs (field :: fields) ((name, arg) :: fargs) =
   811           if can (unsuffix name) field then
   812             let val (args, rest) = splitargs fields fargs
   813             in (arg :: args, rest) end
   814           else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t])
   815       | splitargs [] (fargs as (_ :: _)) = ([], fargs)
   816       | splitargs (_ :: _) [] = raise TERM (msg ^ "expecting more fields", [t])
   817       | splitargs _ _ = ([], []);
   818 
   819     fun mk_ext (fargs as (name, arg) :: _) =
   820           (case get_fieldext thy (Sign.intern_const thy name) of
   821             SOME (ext, alphas) =>
   822               (case get_extfields thy ext of
   823                 SOME flds =>
   824                  (let
   825                     val flds' = but_last flds;
   826                     val types = map snd flds';
   827                     val (args, rest) = splitargs (map fst flds') fargs;
   828                     val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
   829                     val midx = fold (fn T => fn i => Int.max (maxidx_of_typ T, i)) argtypes 0;
   830                     val varifyT = varifyT midx;
   831                     val vartypes = map varifyT types;
   832 
   833                     val subst = fold (Sign.typ_match thy) (vartypes ~~ argtypes) Vartab.empty;
   834                     val alphas' =
   835                       map (Syntax.term_of_typ (! Syntax.show_sorts) o Envir.norm_type subst o varifyT)
   836                         (but_last alphas);
   837 
   838                     val more' = mk_ext rest;
   839                   in
   840                     list_comb (Syntax.const (suffix sfx ext), alphas' @ [more'])
   841                   end handle TYPE_MATCH =>
   842                     raise TERM (msg ^ "type is no proper record (extension)", [t]))
   843               | NONE => raise TERM (msg ^ "no fields defined for " ^ ext, [t]))
   844           | NONE => raise TERM (msg ^ name ^" is no proper field", [t]))
   845       | mk_ext [] = more;
   846 
   847   in mk_ext fieldargs end;
   848 
   849 fun gen_adv_record_tr sep mark sfx unit ctxt [t] =
   850       gen_ext_fields_tr sep mark sfx unit ctxt t
   851   | gen_adv_record_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
   852 
   853 fun gen_adv_record_scheme_tr sep mark sfx ctxt [t, more] =
   854       gen_ext_fields_tr sep mark sfx more ctxt t
   855   | gen_adv_record_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
   856 
   857 fun gen_adv_record_type_tr sep mark sfx unit ctxt [t] =
   858       gen_ext_type_tr sep mark sfx unit ctxt t
   859   | gen_adv_record_type_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
   860 
   861 fun gen_adv_record_type_scheme_tr sep mark sfx ctxt [t, more] =
   862       gen_ext_type_tr sep mark sfx more ctxt t
   863   | gen_adv_record_type_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
   864 
   865 val adv_record_tr = gen_adv_record_tr "_fields" "_field" extN HOLogic.unit;
   866 
   867 val adv_record_scheme_tr = gen_adv_record_scheme_tr "_fields" "_field" extN;
   868 
   869 val adv_record_type_tr =
   870   gen_adv_record_type_tr "_field_types" "_field_type" ext_typeN
   871     (Syntax.term_of_typ false (HOLogic.unitT));
   872 
   873 val adv_record_type_scheme_tr =
   874   gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN;
   875 
   876 
   877 val parse_translation =
   878  [("_record_update", record_update_tr),
   879   ("_update_name", update_name_tr)];
   880 
   881 val adv_parse_translation =
   882  [("_record", adv_record_tr),
   883   ("_record_scheme", adv_record_scheme_tr),
   884   ("_record_type", adv_record_type_tr),
   885   ("_record_type_scheme", adv_record_type_scheme_tr)];
   886 
   887 
   888 (* print translations *)
   889 
   890 val print_record_type_abbr = Unsynchronized.ref true;
   891 val print_record_type_as_fields = Unsynchronized.ref true;
   892 
   893 fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ k $ u) =
   894       let
   895         val t =
   896           (case k of
   897             Abs (_, _, Abs (_, _, t) $ Bound 0) =>
   898               if null (loose_bnos t) then t else raise Match
   899           | Abs (x, _, t) =>
   900               if null (loose_bnos t) then t else raise Match
   901           | _ => raise Match);
   902 
   903           (* FIXME ? *)
   904           (* (case k of (Const ("K_record", _) $ t) => t
   905                    | Abs (x, _, Const ("K_record", _) $ t $ Bound 0) => t
   906                    | _ => raise Match)*)
   907       in
   908         (case try (unsuffix sfx) name_field of
   909           SOME name =>
   910             apfst (cons (Syntax.const mark $ Syntax.free name $ t)) (gen_field_upds_tr' mark sfx u)
   911         | NONE => ([], tm))
   912       end
   913   | gen_field_upds_tr' _ _ tm = ([], tm);
   914 
   915 fun record_update_tr' tm =
   916   let val (ts, u) = gen_field_upds_tr' "_update" updateN tm in
   917     if null ts then raise Match
   918     else
   919       Syntax.const "_record_update" $ u $
   920         foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts)
   921   end;
   922 
   923 fun gen_field_tr' sfx tr' name =
   924   let val name_sfx = suffix sfx name
   925   in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
   926 
   927 fun record_tr' sep mark record record_scheme unit ctxt t =
   928   let
   929     val thy = ProofContext.theory_of ctxt;
   930 
   931     fun field_lst t =
   932       (case strip_comb t of
   933         (Const (ext, _), args as (_ :: _)) =>
   934           (case try (unsuffix extN) (Sign.intern_const thy ext) of
   935             SOME ext' =>
   936               (case get_extfields thy ext' of
   937                 SOME flds =>
   938                  (let
   939                     val f :: fs = but_last (map fst flds);
   940                     val flds' = Sign.extern_const thy f :: map Long_Name.base_name fs;
   941                     val (args', more) = split_last args;
   942                   in (flds' ~~ args') @ field_lst more end
   943                   handle Library.UnequalLengths => [("", t)])
   944               | NONE => [("", t)])
   945           | NONE => [("", t)])
   946        | _ => [("", t)]);
   947 
   948     val (flds, (_, more)) = split_last (field_lst t);
   949     val _ = if null flds then raise Match else ();
   950     val flds' = map (fn (n, t) => Syntax.const mark $ Syntax.const n $ t) flds;
   951     val flds'' = foldr1 (fn (x, y) => Syntax.const sep $ x $ y) flds';
   952   in
   953     if unit more
   954     then Syntax.const record $ flds''
   955     else Syntax.const record_scheme $ flds'' $ more
   956   end;
   957 
   958 fun gen_record_tr' name =
   959   let
   960     val name_sfx = suffix extN name;
   961     val unit = (fn Const (@{const_syntax "Product_Type.Unity"}, _) => true | _ => false);
   962     fun tr' ctxt ts =
   963       record_tr' "_fields" "_field" "_record" "_record_scheme" unit ctxt
   964         (list_comb (Syntax.const name_sfx, ts));
   965   in (name_sfx, tr') end;
   966 
   967 fun print_translation names =
   968   map (gen_field_tr' updateN record_update_tr') names;
   969 
   970 
   971 (* record_type_abbr_tr' *)
   972 
   973 (*try to reconstruct the record name type abbreviation from
   974   the (nested) extension types*)
   975 fun record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt tm =
   976   let
   977     val thy = ProofContext.theory_of ctxt;
   978 
   979     (*tm is term representation of a (nested) field type. We first reconstruct the
   980       type from tm so that we can continue on the type level rather then the term level*)
   981 
   982     (*WORKAROUND:
   983       If a record type occurs in an error message of type inference there
   984       may be some internal frees donoted by ??:
   985       (Const "_tfree",_) $ Free ("??'a", _).
   986 
   987       This will unfortunately be translated to Type ("??'a", []) instead of
   988       TFree ("??'a", _) by typ_of_term, which will confuse unify below.
   989       fixT works around.*)
   990     fun fixT (T as Type (x, [])) =
   991           if String.isPrefix "??'" x then TFree (x, Sign.defaultS thy) else T
   992       | fixT (Type (x, xs)) = Type (x, map fixT xs)
   993       | fixT T = T;
   994 
   995     val T = fixT (decode_type thy tm);
   996     val midx = maxidx_of_typ T;
   997     val varifyT = varifyT midx;
   998 
   999     fun mk_type_abbr subst name alphas =
  1000       let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas) in
  1001         Syntax.term_of_typ (! Syntax.show_sorts)
  1002           (Sign.extern_typ thy (Envir.norm_type subst abbrT))
  1003       end;
  1004 
  1005     fun match rT T = Sign.typ_match thy (varifyT rT, T) Vartab.empty;
  1006   in
  1007     if ! print_record_type_abbr then
  1008       (case last_extT T of
  1009         SOME (name, _) =>
  1010           if name = lastExt then
  1011            (let val subst = match schemeT T in
  1012               if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, Sign.defaultS thy))))
  1013               then mk_type_abbr subst abbr alphas
  1014               else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
  1015             end handle TYPE_MATCH => default_tr' ctxt tm)
  1016           else raise Match (*give print translation of specialised record a chance*)
  1017       | _ => raise Match)
  1018     else default_tr' ctxt tm
  1019   end;
  1020 
  1021 fun record_type_tr' sep mark record record_scheme ctxt t =
  1022   let
  1023     val thy = ProofContext.theory_of ctxt;
  1024 
  1025     val T = decode_type thy t;
  1026     val varifyT = varifyT (Term.maxidx_of_typ T);
  1027 
  1028     fun term_of_type T = Syntax.term_of_typ (! Syntax.show_sorts) (Sign.extern_typ thy T);
  1029 
  1030     fun field_lst T =
  1031       (case T of
  1032         Type (ext, args) =>
  1033           (case try (unsuffix ext_typeN) ext of
  1034             SOME ext' =>
  1035               (case get_extfields thy ext' of
  1036                 SOME flds =>
  1037                   (case get_fieldext thy (fst (hd flds)) of
  1038                     SOME (_, alphas) =>
  1039                      (let
  1040                         val f :: fs = but_last flds;
  1041                         val flds' = apfst (Sign.extern_const thy) f ::
  1042                           map (apfst Long_Name.base_name) fs;
  1043                         val (args', more) = split_last args;
  1044                         val alphavars = map varifyT (but_last alphas);
  1045                         val subst = fold2 (curry (Sign.typ_match thy)) alphavars args' Vartab.empty;
  1046                         val flds'' = (map o apsnd) (Envir.norm_type subst o varifyT) flds';
  1047                       in flds'' @ field_lst more end
  1048                       handle TYPE_MATCH => [("", T)]
  1049                         | Library.UnequalLengths => [("", T)])
  1050                   | NONE => [("", T)])
  1051               | NONE => [("", T)])
  1052           | NONE => [("", T)])
  1053       | _ => [("", T)]);
  1054 
  1055     val (flds, (_, moreT)) = split_last (field_lst T);
  1056     val flds' = map (fn (n, T) => Syntax.const mark $ Syntax.const n $ term_of_type T) flds;
  1057     val flds'' =
  1058       foldr1 (fn (x, y) => Syntax.const sep $ x $ y) flds'
  1059         handle Empty => raise Match;
  1060   in
  1061     if not (! print_record_type_as_fields) orelse null flds then raise Match
  1062     else if moreT = HOLogic.unitT then Syntax.const record $ flds''
  1063     else Syntax.const record_scheme $ flds'' $ term_of_type moreT
  1064   end;
  1065 
  1066 
  1067 fun gen_record_type_tr' name =
  1068   let
  1069     val name_sfx = suffix ext_typeN name;
  1070     fun tr' ctxt ts =
  1071       record_type_tr' "_field_types" "_field_type" "_record_type" "_record_type_scheme"
  1072         ctxt (list_comb (Syntax.const name_sfx, ts))
  1073   in (name_sfx, tr') end;
  1074 
  1075 
  1076 fun gen_record_type_abbr_tr' abbr alphas zeta lastExt schemeT name =
  1077   let
  1078     val name_sfx = suffix ext_typeN name;
  1079     val default_tr' =
  1080       record_type_tr' "_field_types" "_field_type" "_record_type" "_record_type_scheme";
  1081     fun tr' ctxt ts =
  1082       record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt
  1083         (list_comb (Syntax.const name_sfx, ts));
  1084   in (name_sfx, tr') end;
  1085 
  1086 
  1087 
  1088 (** record simprocs **)
  1089 
  1090 val record_quick_and_dirty_sensitive = Unsynchronized.ref false;
  1091 
  1092 
  1093 fun quick_and_dirty_prove stndrd thy asms prop tac =
  1094   if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty then
  1095     Goal.prove (ProofContext.init thy) [] []
  1096       (Logic.list_implies (map Logic.varify asms, Logic.varify prop))
  1097       (K (SkipProof.cheat_tac @{theory HOL}))
  1098       (*Drule.standard can take quite a while for large records, thats why
  1099         we varify the proposition manually here.*)
  1100   else
  1101     let val prf = Goal.prove (ProofContext.init thy) [] asms prop tac
  1102     in if stndrd then standard prf else prf end;
  1103 
  1104 fun quick_and_dirty_prf noopt opt () =
  1105   if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty
  1106   then noopt ()
  1107   else opt ();
  1108 
  1109 fun is_sel_upd_pair thy (Const (s, t)) (Const (u, t')) =
  1110   (case get_updates thy u of
  1111     SOME u_name => u_name = s
  1112   | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));
  1113 
  1114 fun mk_comp f g =
  1115   let
  1116     val x = fastype_of g;
  1117     val a = domain_type x;
  1118     val b = range_type x;
  1119     val c = range_type (fastype_of f);
  1120     val T = (b --> c) --> ((a --> b) --> (a --> c))
  1121   in Const ("Fun.comp", T) $ f $ g end;
  1122 
  1123 fun mk_comp_id f =
  1124   let val T = range_type (fastype_of f)
  1125   in mk_comp (Const ("Fun.id", T --> T)) f end;
  1126 
  1127 fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
  1128   | get_upd_funs _ = [];
  1129 
  1130 fun get_accupd_simps thy term defset intros_tac =
  1131   let
  1132     val (acc, [body]) = strip_comb term;
  1133     val recT = domain_type (fastype_of acc);
  1134     val upd_funs = sort_distinct TermOrd.fast_term_ord (get_upd_funs body);
  1135     fun get_simp upd =
  1136       let
  1137         val T = domain_type (fastype_of upd);
  1138         val lhs = mk_comp acc (upd $ Free ("f", T));
  1139         val rhs =
  1140           if is_sel_upd_pair thy acc upd
  1141           then mk_comp (Free ("f", T)) acc
  1142           else mk_comp_id acc;
  1143         val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
  1144         val othm =
  1145           Goal.prove (ProofContext.init thy) [] [] prop
  1146             (fn prems =>
  1147               EVERY
  1148                [simp_tac defset 1,
  1149                 REPEAT_DETERM (intros_tac 1),
  1150                 TRY (simp_tac (HOL_ss addsimps id_o_apps) 1)]);
  1151         val dest =
  1152           if is_sel_upd_pair thy acc upd
  1153           then o_eq_dest
  1154           else o_eq_id_dest;
  1155       in standard (othm RS dest) end;
  1156   in map get_simp upd_funs end;
  1157 
  1158 (* FIXME dup? *)
  1159 structure SymSymTab =
  1160   Table(type key = string * string val ord = prod_ord fast_string_ord fast_string_ord);
  1161 
  1162 fun get_updupd_simp thy defset intros_tac u u' comp =
  1163   let
  1164     val f = Free ("f", domain_type (fastype_of u));
  1165     val f' = Free ("f'", domain_type (fastype_of u'));
  1166     val lhs = mk_comp (u $ f) (u' $ f');
  1167     val rhs =
  1168       if comp
  1169       then u $ mk_comp f f'
  1170       else mk_comp (u' $ f') (u $ f);
  1171     val prop = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
  1172     val othm =
  1173       Goal.prove (ProofContext.init thy) [] [] prop
  1174         (fn prems =>
  1175           EVERY
  1176            [simp_tac defset 1,
  1177             REPEAT_DETERM (intros_tac 1),
  1178             TRY (simp_tac (HOL_ss addsimps [id_apply]) 1)]);
  1179     val dest = if comp then o_eq_dest_lhs else o_eq_dest;
  1180   in standard (othm RS dest) end;
  1181 
  1182 fun get_updupd_simps thy term defset intros_tac =
  1183   let
  1184     val recT = fastype_of term;
  1185     val upd_funs = get_upd_funs term;
  1186     val cname = fst o dest_Const;
  1187     fun getswap u u' = get_updupd_simp thy defset intros_tac u u' (cname u = cname u');
  1188     fun build_swaps_to_eq upd [] swaps = swaps
  1189       | build_swaps_to_eq upd (u :: us) swaps =
  1190           let
  1191             val key = (cname u, cname upd);
  1192             val newswaps =
  1193               if SymSymTab.defined swaps key then swaps
  1194               else SymSymTab.insert (K true) (key, getswap u upd) swaps;
  1195           in
  1196             if cname u = cname upd then newswaps
  1197             else build_swaps_to_eq upd us newswaps
  1198           end;
  1199     fun swaps_needed [] prev seen swaps = map snd (SymSymTab.dest swaps)
  1200       | swaps_needed (u :: us) prev seen swaps =
  1201           if Symtab.defined seen (cname u)
  1202           then swaps_needed us prev seen (build_swaps_to_eq u prev swaps)
  1203           else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps;
  1204   in swaps_needed upd_funs [] Symtab.empty SymSymTab.empty end;
  1205 
  1206 val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate;
  1207 
  1208 fun prove_unfold_defs thy ss T ex_simps ex_simprs prop =
  1209   let
  1210     val defset = get_sel_upd_defs thy;
  1211     val in_tac = IsTupleSupport.istuple_intros_tac thy;
  1212     val prop' = Envir.beta_eta_contract prop;
  1213     val (lhs, rhs) = Logic.dest_equals (Logic.strip_assums_concl prop');
  1214     val (head, args) = strip_comb lhs;
  1215     val simps =
  1216       if length args = 1
  1217       then get_accupd_simps thy lhs defset in_tac
  1218       else get_updupd_simps thy lhs defset in_tac;
  1219   in
  1220     Goal.prove (ProofContext.init thy) [] [] prop'
  1221       (fn prems =>
  1222         simp_tac (HOL_basic_ss addsimps (simps @ [K_record_comp])) 1 THEN
  1223         TRY (simp_tac (HOL_basic_ss addsimps ex_simps addsimprocs ex_simprs) 1))
  1224   end;
  1225 
  1226 
  1227 local
  1228 
  1229 fun eq (s1: string) (s2: string) = (s1 = s2);
  1230 
  1231 fun has_field extfields f T =
  1232   exists (fn (eN, _) => exists (eq f o fst) (Symtab.lookup_list extfields eN)) (dest_recTs T);
  1233 
  1234 fun K_skeleton n (T as Type (_, [_, kT])) (b as Bound i) (Abs (x, xT, t)) =
  1235       if null (loose_bnos t) then ((n, kT), (Abs (x, xT, Bound (i + 1)))) else ((n, T), b)
  1236   | K_skeleton n T b _ = ((n, T), b);
  1237 
  1238 in
  1239 
  1240 (* record_simproc *)
  1241 
  1242 (*
  1243   Simplify selections of an record update:
  1244     (1)  S (S_update k r) = k (S r)
  1245     (2)  S (X_update k r) = S r
  1246 
  1247   The simproc skips multiple updates at once, eg:
  1248    S (X_update x (Y_update y (S_update k r))) = k (S r)
  1249 
  1250   But be careful in (2) because of the extensibility of records.
  1251   - If S is a more-selector we have to make sure that the update on component
  1252     X does not affect the selected subrecord.
  1253   - If X is a more-selector we have to make sure that S is not in the updated
  1254     subrecord.
  1255 *)
  1256 val record_simproc =
  1257   Simplifier.simproc @{theory HOL} "record_simp" ["x"]
  1258     (fn thy => fn ss => fn t =>
  1259       (case t of
  1260         (sel as Const (s, Type (_, [domS, rangeS]))) $
  1261             ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
  1262           if is_selector thy s then
  1263             (case get_updates thy u of
  1264               SOME u_name =>
  1265                 let
  1266                   val {sel_upd = {updates, ...}, extfields, ...} = RecordsData.get thy;
  1267 
  1268                   fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
  1269                         (case Symtab.lookup updates u of
  1270                           NONE => NONE
  1271                         | SOME u_name =>
  1272                             if u_name = s then
  1273                               (case mk_eq_terms r of
  1274                                 NONE =>
  1275                                   let
  1276                                     val rv = ("r", rT);
  1277                                     val rb = Bound 0;
  1278                                     val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
  1279                                   in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end
  1280                               | SOME (trm, trm', vars) =>
  1281                                   let
  1282                                     val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k;
  1283                                   in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end)
  1284                             else if has_field extfields u_name rangeS orelse
  1285                               has_field extfields s (domain_type kT) then NONE
  1286                             else
  1287                               (case mk_eq_terms r of
  1288                                 SOME (trm, trm', vars) =>
  1289                                   let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k
  1290                                   in SOME (upd $ kb $ trm, trm', kv :: vars) end
  1291                               | NONE =>
  1292                                   let
  1293                                     val rv = ("r", rT);
  1294                                     val rb = Bound 0;
  1295                                     val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
  1296                                   in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end))
  1297                     | mk_eq_terms r = NONE;
  1298                 in
  1299                   (case mk_eq_terms (upd $ k $ r) of
  1300                     SOME (trm, trm', vars) =>
  1301                       SOME
  1302                         (prove_unfold_defs thy ss domS [] []
  1303                           (list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
  1304                   | NONE => NONE)
  1305                 end
  1306             | NONE => NONE)
  1307           else NONE
  1308       | _ => NONE));
  1309 
  1310 fun get_upd_acc_cong_thm upd acc thy simpset =
  1311   let
  1312     val in_tac = IsTupleSupport.istuple_intros_tac thy;
  1313 
  1314     val insts = [("upd", cterm_of thy upd), ("acc", cterm_of thy acc)]
  1315     val prop = concl_of (named_cterm_instantiate insts updacc_cong_triv);
  1316   in
  1317     Goal.prove (ProofContext.init thy) [] [] prop
  1318       (fn prems =>
  1319         EVERY
  1320          [simp_tac simpset 1,
  1321           REPEAT_DETERM (in_tac 1),
  1322           TRY (resolve_tac [updacc_cong_idI] 1)])
  1323   end;
  1324 
  1325 
  1326 (* record_upd_simproc *)
  1327 
  1328 (*Simplify multiple updates:
  1329     (1) "N_update y (M_update g (N_update x (M_update f r))) =
  1330           (N_update (y o x) (M_update (g o f) r))"
  1331     (2)  "r(|M:= M r|) = r"
  1332 
  1333   In both cases "more" updates complicate matters: for this reason
  1334   we omit considering further updates if doing so would introduce
  1335   both a more update and an update to a field within it.*)
  1336 val record_upd_simproc =
  1337   Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"]
  1338     (fn thy => fn ss => fn t =>
  1339       let
  1340         (*We can use more-updators with other updators as long
  1341           as none of the other updators go deeper than any more
  1342           updator. min here is the depth of the deepest other
  1343           updator, max the depth of the shallowest more updator.*)
  1344         fun include_depth (dep, true) (min, max) =
  1345               if min <= dep
  1346               then SOME (min, if dep <= max orelse max = ~1 then dep else max)
  1347               else NONE
  1348           | include_depth (dep, false) (min, max) =
  1349               if dep <= max orelse max = ~1
  1350               then SOME (if min <= dep then dep else min, max)
  1351               else NONE;
  1352 
  1353         fun getupdseq (term as (upd as Const (u, T)) $ f $ tm) min max =
  1354               (case get_update_details u thy of
  1355                 SOME (s, dep, ismore) =>
  1356                   (case include_depth (dep, ismore) (min, max) of
  1357                     SOME (min', max') =>
  1358                       let val (us, bs, _) = getupdseq tm min' max'
  1359                       in ((upd, s, f) :: us, bs, fastype_of term) end
  1360                   | NONE => ([], term, HOLogic.unitT))
  1361               | NONE => ([], term, HOLogic.unitT))
  1362           | getupdseq term _ _ = ([], term, HOLogic.unitT);
  1363 
  1364         val (upds, base, baseT) = getupdseq t 0 ~1;
  1365 
  1366         fun is_upd_noop s (f as Abs (n, T, Const (s', T') $ tm')) tm =
  1367               if s = s' andalso null (loose_bnos tm')
  1368                 andalso subst_bound (HOLogic.unit, tm') = tm
  1369               then (true, Abs (n, T, Const (s', T') $ Bound 1))
  1370               else (false, HOLogic.unit)
  1371           | is_upd_noop s f tm = (false, HOLogic.unit);
  1372 
  1373         fun get_noop_simps (upd as Const (u, T))
  1374             (f as Abs (n, T', (acc as Const (s, T'')) $ _)) =
  1375           let
  1376             val ss = get_sel_upd_defs thy;
  1377             val uathm = get_upd_acc_cong_thm upd acc thy ss;
  1378           in
  1379             [standard (uathm RS updacc_noopE), standard (uathm RS updacc_noop_compE)]
  1380           end;
  1381 
  1382         (*If f is constant then (f o g) = f. we know that K_skeleton
  1383           only returns constant abstractions thus when we see an
  1384           abstraction we can discard inner updates.*)
  1385         fun add_upd (f as Abs _) fs = [f]
  1386           | add_upd f fs = (f :: fs);
  1387 
  1388         (*mk_updterm returns
  1389           (orig-term-skeleton, simplified-skeleton,
  1390             variables, duplicate-updates, simp-flag, noop-simps)
  1391 
  1392           where duplicate-updates is a table used to pass upward
  1393           the list of update functions which can be composed
  1394           into an update above them, simp-flag indicates whether
  1395           any simplification was achieved, and noop-simps are
  1396           used for eliminating case (2) defined above*)
  1397         fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term =
  1398               let
  1399                 val (lhs, rhs, vars, dups, simp, noops) =
  1400                   mk_updterm upds (Symtab.update (u, ()) above) term;
  1401                 val (fvar, skelf) =
  1402                   K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f;
  1403                 val (isnoop, skelf') = is_upd_noop s f term;
  1404                 val funT = domain_type T;
  1405                 fun mk_comp_local (f, f') = Const ("Fun.comp", funT --> funT --> funT) $ f $ f';
  1406               in
  1407                 if isnoop then
  1408                   (upd $ skelf' $ lhs, rhs, vars,
  1409                     Symtab.update (u, []) dups, true,
  1410                     if Symtab.defined noops u then noops
  1411                     else Symtab.update (u, get_noop_simps upd skelf') noops)
  1412                 else if Symtab.defined above u then
  1413                   (upd $ skelf $ lhs, rhs, fvar :: vars,
  1414                     Symtab.map_default (u, []) (add_upd skelf) dups,
  1415                     true, noops)
  1416                 else
  1417                   (case Symtab.lookup dups u of
  1418                     SOME fs =>
  1419                      (upd $ skelf $ lhs,
  1420                       upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs,
  1421                       fvar :: vars, dups, true, noops)
  1422                   | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops))
  1423               end
  1424           | mk_updterm [] above term =
  1425               (Bound 0, Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty)
  1426           | mk_updterm us above term =
  1427               raise TERM ("mk_updterm match", map (fn (x, y, z) => x) us);
  1428 
  1429         val (lhs, rhs, vars, dups, simp, noops) = mk_updterm upds Symtab.empty base;
  1430         val noops' = flat (map snd (Symtab.dest noops));
  1431       in
  1432         if simp then
  1433           SOME
  1434             (prove_unfold_defs thy ss baseT noops' [record_simproc]
  1435               (list_all (vars, Logic.mk_equals (lhs, rhs))))
  1436         else NONE
  1437       end);
  1438 
  1439 end;
  1440 
  1441 
  1442 (* record_eq_simproc *)
  1443 
  1444 (*Looks up the most specific record-equality.
  1445 
  1446  Note on efficiency:
  1447  Testing equality of records boils down to the test of equality of all components.
  1448  Therefore the complexity is: #components * complexity for single component.
  1449  Especially if a record has a lot of components it may be better to split up
  1450  the record first and do simplification on that (record_split_simp_tac).
  1451  e.g. r(|lots of updates|) = x
  1452 
  1453              record_eq_simproc          record_split_simp_tac
  1454  Complexity: #components * #updates     #updates
  1455 *)
  1456 val record_eq_simproc =
  1457   Simplifier.simproc @{theory HOL} "record_eq_simp" ["r = s"]
  1458     (fn thy => fn _ => fn t =>
  1459       (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ =>
  1460         (case rec_id ~1 T of
  1461           "" => NONE
  1462         | name =>
  1463             (case get_equalities thy name of
  1464               NONE => NONE
  1465             | SOME thm => SOME (thm RS Eq_TrueI)))
  1466       | _ => NONE));
  1467 
  1468 
  1469 (* record_split_simproc *)
  1470 
  1471 (*Split quantified occurrences of records, for which P holds.  P can peek on the
  1472   subterm starting at the quantified occurrence of the record (including the quantifier):
  1473     P t = 0: do not split
  1474     P t = ~1: completely split
  1475     P t > 0: split up to given bound of record extensions.*)
  1476 fun record_split_simproc P =
  1477   Simplifier.simproc @{theory HOL} "record_split_simp" ["x"]
  1478     (fn thy => fn _ => fn t =>
  1479       (case t of
  1480         Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ trm =>
  1481           if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex" then
  1482             (case rec_id ~1 T of
  1483               "" => NONE
  1484             | name =>
  1485                 let val split = P t in
  1486                   if split <> 0 then
  1487                     (case get_splits thy (rec_id split T) of
  1488                       NONE => NONE
  1489                     | SOME (all_thm, All_thm, Ex_thm, _) =>
  1490                         SOME
  1491                           (case quantifier of
  1492                             "all" => all_thm
  1493                           | "All" => All_thm RS eq_reflection
  1494                           | "Ex" => Ex_thm RS eq_reflection
  1495                           | _ => error "record_split_simproc"))
  1496                   else NONE
  1497                 end)
  1498           else NONE
  1499       | _ => NONE));
  1500 
  1501 val record_ex_sel_eq_simproc =
  1502   Simplifier.simproc @{theory HOL} "record_ex_sel_eq_simproc" ["Ex t"]
  1503     (fn thy => fn ss => fn t =>
  1504       let
  1505         fun prove prop =
  1506           quick_and_dirty_prove true thy [] prop
  1507             (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
  1508                 addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1);
  1509 
  1510         fun mkeq (lr, Teq, (sel, Tsel), x) i =
  1511           if is_selector thy sel then
  1512             let
  1513               val x' =
  1514                 if not (loose_bvar1 (x, 0))
  1515                 then Free ("x" ^ string_of_int i, range_type Tsel)
  1516                 else raise TERM ("", [x]);
  1517               val sel' = Const (sel, Tsel) $ Bound 0;
  1518               val (l, r) = if lr then (sel', x') else (x', sel');
  1519             in Const ("op =", Teq) $ l $ r end
  1520           else raise TERM ("", [Const (sel, Tsel)]);
  1521 
  1522         fun dest_sel_eq (Const ("op =", Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
  1523               (true, Teq, (sel, Tsel), X)
  1524           | dest_sel_eq (Const ("op =", Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
  1525               (false, Teq, (sel, Tsel), X)
  1526           | dest_sel_eq _ = raise TERM ("", []);
  1527       in
  1528         (case t of
  1529           Const ("Ex", Tex) $ Abs (s, T, t) =>
  1530            (let
  1531               val eq = mkeq (dest_sel_eq t) 0;
  1532               val prop =
  1533                 list_all ([("r", T)],
  1534                   Logic.mk_equals (Const ("Ex", Tex) $ Abs (s, T, eq), HOLogic.true_const));
  1535             in SOME (prove prop) end
  1536             handle TERM _ => NONE)
  1537         | _ => NONE)
  1538       end);
  1539 
  1540 
  1541 local
  1542 
  1543 val inductive_atomize = thms "induct_atomize";
  1544 val inductive_rulify = thms "induct_rulify";
  1545 
  1546 in
  1547 
  1548 (* record_split_simp_tac *)
  1549 
  1550 (*Split (and simplify) all records in the goal for which P holds.
  1551   For quantified occurrences of a record
  1552   P can peek on the whole subterm (including the quantifier); for free variables P
  1553   can only peek on the variable itself.
  1554   P t = 0: do not split
  1555   P t = ~1: completely split
  1556   P t > 0: split up to given bound of record extensions.*)
  1557 fun record_split_simp_tac thms P i st =
  1558   let
  1559     val thy = Thm.theory_of_thm st;
  1560 
  1561     val has_rec = exists_Const
  1562       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
  1563           (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T
  1564         | _ => false);
  1565 
  1566     val goal = nth (Thm.prems_of st) (i - 1);
  1567     val frees = List.filter (is_recT o type_of) (OldTerm.term_frees goal);
  1568 
  1569     fun mk_split_free_tac free induct_thm i =
  1570       let
  1571         val cfree = cterm_of thy free;
  1572         val _$ (_ $ r) = concl_of induct_thm;
  1573         val crec = cterm_of thy r;
  1574         val thm = cterm_instantiate [(crec, cfree)] induct_thm;
  1575       in
  1576         EVERY
  1577          [simp_tac (HOL_basic_ss addsimps inductive_atomize) i,
  1578           rtac thm i,
  1579           simp_tac (HOL_basic_ss addsimps inductive_rulify) i]
  1580       end;
  1581 
  1582     fun split_free_tac P i (free as Free (n, T)) =
  1583           (case rec_id ~1 T of
  1584             "" => NONE
  1585           | name =>
  1586               let val split = P free in
  1587                 if split <> 0 then
  1588                   (case get_splits thy (rec_id split T) of
  1589                     NONE => NONE
  1590                   | SOME (_, _, _, induct_thm) =>
  1591                       SOME (mk_split_free_tac free induct_thm i))
  1592                 else NONE
  1593               end)
  1594       | split_free_tac _ _ _ = NONE;
  1595 
  1596     val split_frees_tacs = List.mapPartial (split_free_tac P i) frees;
  1597 
  1598     val simprocs = if has_rec goal then [record_split_simproc P] else [];
  1599     val thms' = K_comp_convs @ thms;
  1600   in
  1601     st |>
  1602       (EVERY split_frees_tacs THEN
  1603         Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i)
  1604   end handle Empty => Seq.empty;
  1605 end;
  1606 
  1607 
  1608 (* record_split_tac *)
  1609 
  1610 (*Split all records in the goal, which are quantified by ! or !!.*)
  1611 fun record_split_tac i st =
  1612   let
  1613     val thy = Thm.theory_of_thm st;
  1614 
  1615     val has_rec = exists_Const
  1616       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
  1617           (s = "all" orelse s = "All") andalso is_recT T
  1618         | _ => false);
  1619 
  1620     val goal = nth (Thm.prems_of st) (i - 1);  (* FIXME SUBGOAL *)
  1621 
  1622     fun is_all t =
  1623       (case t of
  1624         Const (quantifier, _) $ _ =>
  1625           if quantifier = "All" orelse quantifier = "all" then ~1 else 0
  1626       | _ => 0);
  1627 
  1628   in
  1629     if has_rec goal then
  1630       Simplifier.full_simp_tac
  1631         (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i st
  1632     else Seq.empty
  1633   end handle Subscript => Seq.empty;     (* FIXME SUBGOAL *)
  1634 
  1635 
  1636 (* wrapper *)
  1637 
  1638 val record_split_name = "record_split_tac";
  1639 val record_split_wrapper = (record_split_name, fn tac => record_split_tac ORELSE' tac);
  1640 
  1641 
  1642 
  1643 (** theory extender interface **)
  1644 
  1645 (* prepare arguments *)
  1646 
  1647 fun read_raw_parent ctxt raw_T =
  1648   (case ProofContext.read_typ_abbrev ctxt raw_T of
  1649     Type (name, Ts) => (Ts, name)
  1650   | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));
  1651 
  1652 fun read_typ ctxt raw_T env =
  1653   let
  1654     val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
  1655     val T = Syntax.read_typ ctxt' raw_T;
  1656     val env' = OldTerm.add_typ_tfrees (T, env);
  1657   in (T, env') end;
  1658 
  1659 fun cert_typ ctxt raw_T env =
  1660   let
  1661     val thy = ProofContext.theory_of ctxt;
  1662     val T = Type.no_tvars (Sign.certify_typ thy raw_T)
  1663       handle TYPE (msg, _, _) => error msg;
  1664     val env' = OldTerm.add_typ_tfrees (T, env);
  1665   in (T, env') end;
  1666 
  1667 
  1668 (* attributes *)
  1669 
  1670 fun case_names_fields x = RuleCases.case_names ["fields"] x;
  1671 fun induct_type_global name = [case_names_fields, Induct.induct_type name];
  1672 fun cases_type_global name = [case_names_fields, Induct.cases_type name];
  1673 
  1674 
  1675 (* tactics *)
  1676 
  1677 fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));
  1678 
  1679 (*Do case analysis / induction according to rule on last parameter of ith subgoal
  1680   (or on s if there are no parameters).
  1681   Instatiation of record variable (and predicate) in rule is calculated to
  1682   avoid problems with higher order unification.*)
  1683 fun try_param_tac s rule i st =
  1684   let
  1685     val cert = cterm_of (Thm.theory_of_thm st);
  1686     val g = nth (prems_of st) (i - 1);   (* FIXME SUBGOAL *)
  1687     val params = Logic.strip_params g;
  1688     val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
  1689     val rule' = Thm.lift_rule (Thm.cprem_of st i) rule;
  1690     val (P, ys) = strip_comb (HOLogic.dest_Trueprop
  1691       (Logic.strip_assums_concl (prop_of rule')));
  1692     (*ca indicates if rule is a case analysis or induction rule*)
  1693     val (x, ca) =
  1694       (case rev (Library.drop (length params, ys)) of
  1695         [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
  1696           (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
  1697       | [x] => (head_of x, false));
  1698     val rule'' = cterm_instantiate (map (pairself cert)
  1699       (case (rev params) of
  1700         [] =>
  1701           (case AList.lookup (op =) (map dest_Free (OldTerm.term_frees (prop_of st))) s of
  1702             NONE => sys_error "try_param_tac: no such variable"
  1703           | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
  1704       | (_, T) :: _ =>
  1705           [(P, list_abs (params, if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
  1706             (x, list_abs (params, Bound 0))])) rule';
  1707   in compose_tac (false, rule'', nprems_of rule) i st end;
  1708 
  1709 
  1710 (*!!x1 ... xn. ... ==> EX x1 ... xn. P x1 ... xn;
  1711   instantiates x1 ... xn with parameters x1 ... xn*)
  1712 fun ex_inst_tac i st =
  1713   let
  1714     val thy = Thm.theory_of_thm st;
  1715     val g = nth (prems_of st) (i - 1);   (* FIXME SUBGOAL *)
  1716     val params = Logic.strip_params g;
  1717     val exI' = Thm.lift_rule (Thm.cprem_of st i) exI;
  1718     val _ $ (_ $ x) = Logic.strip_assums_concl (hd (prems_of exI'));
  1719     val cx = cterm_of thy (fst (strip_comb x));
  1720   in
  1721     Seq.single (Library.foldl (fn (st, v) =>
  1722       Seq.hd
  1723         (compose_tac
  1724           (false,
  1725             cterm_instantiate [(cx, cterm_of thy (list_abs (params, Bound v)))] exI', 1) i st))
  1726         (st, (length params - 1) downto 0))
  1727   end;
  1728 
  1729 fun extension_definition full name fields names alphas zeta moreT more vars thy =
  1730   let
  1731     val base = Long_Name.base_name;
  1732     val fieldTs = (map snd fields);
  1733     val alphas_zeta = alphas @ [zeta];
  1734     val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta;
  1735     val vT = TFree (Name.variant alphas_zeta "'v", HOLogic.typeS);
  1736     val extT_name = suffix ext_typeN name
  1737     val extT = Type (extT_name, alphas_zetaTs);
  1738     val fields_more = fields @ [(full moreN, moreT)];
  1739     val fields_moreTs = fieldTs @ [moreT];
  1740     val bfields_more = map (apfst base) fields_more;
  1741     val r = Free (rN, extT);
  1742     val len = length fields;
  1743     val idxms = 0 upto len;
  1744 
  1745     (*before doing anything else, create the tree of new types
  1746       that will back the record extension*)
  1747 
  1748     fun mktreeT [] = raise TYPE ("mktreeT: empty list", [], [])
  1749       | mktreeT [T] = T
  1750       | mktreeT xs =
  1751           let
  1752             val len = length xs;
  1753             val half = len div 2;
  1754             val left = List.take (xs, half);
  1755             val right = List.drop (xs, half);
  1756           in
  1757             HOLogic.mk_prodT (mktreeT left, mktreeT right)
  1758           end;
  1759 
  1760     fun mktreeV [] = raise TYPE ("mktreeV: empty list", [], [])
  1761       | mktreeV [T] = T
  1762       | mktreeV xs =
  1763           let
  1764             val len = length xs;
  1765             val half = len div 2;
  1766             val left = List.take (xs, half);
  1767             val right = List.drop (xs, half);
  1768           in
  1769             IsTupleSupport.mk_cons_tuple (mktreeV left, mktreeV right)
  1770           end;
  1771 
  1772     fun mk_istuple ((thy, i), (left, rght)) =
  1773       let
  1774         val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
  1775         val nm = suffix suff (Long_Name.base_name name);
  1776         val (isom, cons, thy') =
  1777           IsTupleSupport.add_istuple_type
  1778             (nm, alphas_zeta) (fastype_of left, fastype_of rght) thy;
  1779       in
  1780         ((thy', i + 1), cons $ left $ rght)
  1781       end;
  1782 
  1783     (*trying to create a 1-element istuple will fail, and
  1784       is pointless anyway*)
  1785     fun mk_even_istuple ((thy, i), [arg]) = ((thy, i), arg)
  1786       | mk_even_istuple ((thy, i), args) =
  1787           mk_istuple ((thy, i), IsTupleSupport.dest_cons_tuple (mktreeV args));
  1788 
  1789     fun build_meta_tree_type i thy vars more =
  1790       let val len = length vars in
  1791         if len < 1 then raise (TYPE ("meta_tree_type args too short", [], vars))
  1792         else if len > 16 then
  1793           let
  1794             fun group16 [] = []
  1795               | group16 xs = Library.take (16, xs) :: group16 (Library.drop (16, xs));
  1796             val vars' = group16 vars;
  1797             val ((thy', i'), composites) =
  1798               Library.foldl_map mk_even_istuple ((thy, i), vars');   (* FIXME fold_map !? *)
  1799           in
  1800             build_meta_tree_type i' thy' composites more
  1801           end
  1802         else
  1803           let val ((thy', i'), term) = mk_istuple ((thy, 0), (mktreeV vars, more))
  1804           in (term, thy') end
  1805       end;
  1806 
  1807     val _ = timing_msg "record extension preparing definitions";
  1808 
  1809 
  1810     (* 1st stage part 1: introduce the tree of new types *)
  1811 
  1812     fun get_meta_tree () = build_meta_tree_type 1 thy vars more;
  1813     val (ext_body, typ_thy) =
  1814       timeit_msg "record extension nested type def:" get_meta_tree;
  1815 
  1816 
  1817     (* prepare declarations and definitions *)
  1818 
  1819     (*fields constructor*)
  1820     val ext_decl = mk_extC (name, extT) fields_moreTs;
  1821     val ext_spec = list_comb (Const ext_decl, vars @ [more]) :== ext_body;
  1822 
  1823     fun mk_ext args = list_comb (Const ext_decl, args);
  1824 
  1825 
  1826     (* 1st stage part 2: define the ext constant *)
  1827 
  1828     fun mk_defs () =
  1829       typ_thy
  1830       |> Sign.add_consts_i [Syntax.no_syn (apfst (Binding.name o base) ext_decl)]
  1831       |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name ext_spec)]
  1832     val ([ext_def], defs_thy) =
  1833       timeit_msg "record extension constructor def:" mk_defs;
  1834 
  1835     (* prepare propositions *)
  1836     val _ = timing_msg "record extension preparing propositions";
  1837     val vars_more = vars @ [more];
  1838     val named_vars_more = (names @ [full moreN]) ~~ vars_more;
  1839     val variants = map (fn Free (x, _) => x) vars_more;
  1840     val ext = mk_ext vars_more;
  1841     val s = Free (rN, extT);
  1842     val w = Free (wN, extT);
  1843     val P = Free (Name.variant variants "P", extT-->HOLogic.boolT);
  1844     val C = Free (Name.variant variants "C", HOLogic.boolT);
  1845     val intros_tac = IsTupleSupport.istuple_intros_tac defs_thy;
  1846 
  1847     val inject_prop =
  1848       let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
  1849         HOLogic.mk_conj (HOLogic.eq_const extT $
  1850           mk_ext vars_more $ mk_ext vars_more', HOLogic.true_const)
  1851         ===
  1852         foldr1 HOLogic.mk_conj
  1853           (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [HOLogic.true_const])
  1854       end;
  1855 
  1856     val induct_prop =
  1857       (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
  1858 
  1859     val cases_prop =
  1860       All (map dest_Free vars_more)
  1861         (Trueprop (HOLogic.mk_eq (s, ext)) ==> Trueprop C)
  1862       ==> Trueprop C;
  1863 
  1864     val split_meta_prop =
  1865       let val P = Free (Name.variant variants "P", extT-->Term.propT) in
  1866         Logic.mk_equals
  1867          (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
  1868       end;
  1869 
  1870     fun prove stndrd = quick_and_dirty_prove stndrd defs_thy;
  1871     val prove_standard = quick_and_dirty_prove true defs_thy;
  1872     fun prove_simp stndrd simps =
  1873       let val tac = simp_all_tac HOL_ss simps
  1874       in fn prop => prove stndrd [] prop (K tac) end;
  1875 
  1876     fun inject_prf () =
  1877       simplify HOL_ss
  1878         (prove_standard [] inject_prop
  1879           (fn prems =>
  1880             EVERY
  1881              [simp_tac (HOL_basic_ss addsimps [ext_def]) 1,
  1882               REPEAT_DETERM (resolve_tac [refl_conj_eq] 1 ORELSE
  1883                 intros_tac 1 ORELSE
  1884                 resolve_tac [refl] 1)]));
  1885 
  1886     val inject = timeit_msg "record extension inject proof:" inject_prf;
  1887 
  1888     (*We need a surjection property r = (| f = f r, g = g r ... |)
  1889       to prove other theorems. We haven't given names to the accessors
  1890       f, g etc yet however, so we generate an ext structure with
  1891       free variables as all arguments and allow the introduction tactic to
  1892       operate on it as far as it can. We then use standard to convert
  1893       the free variables into unifiable variables and unify them with
  1894       (roughly) the definition of the accessor.*)
  1895     fun surject_prf () =
  1896       let
  1897         val cterm_ext = cterm_of defs_thy ext;
  1898         val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
  1899         val tactic1 =
  1900           simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
  1901           REPEAT_ALL_NEW intros_tac 1;
  1902         val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
  1903         val [halfway] = Seq.list_of (tactic1 start);    (* FIXME Seq.lift_of ?? *)
  1904         val [surject] = Seq.list_of (tactic2 (standard halfway));    (* FIXME Seq.lift_of ?? *)
  1905       in
  1906         surject
  1907       end;
  1908     val surject = timeit_msg "record extension surjective proof:" surject_prf;
  1909 
  1910     fun split_meta_prf () =
  1911       prove_standard [] split_meta_prop
  1912         (fn prems =>
  1913           EVERY
  1914            [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
  1915             etac meta_allE 1, atac 1,
  1916             rtac (prop_subst OF [surject]) 1,
  1917             REPEAT (etac meta_allE 1), atac 1]);
  1918     val split_meta = timeit_msg "record extension split_meta proof:" split_meta_prf;
  1919 
  1920     fun induct_prf () =
  1921       let val (assm, concl) = induct_prop in
  1922         prove_standard [assm] concl
  1923           (fn {prems, ...} =>
  1924             EVERY
  1925              [cut_rules_tac [split_meta RS meta_iffD2] 1,
  1926               resolve_tac prems 2,
  1927               asm_simp_tac HOL_ss 1])
  1928       end;
  1929     val induct = timeit_msg "record extension induct proof:" induct_prf;
  1930 
  1931     val ([inject', induct', surjective', split_meta'], thm_thy) =
  1932       defs_thy
  1933       |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
  1934            [("ext_inject", inject),
  1935             ("ext_induct", induct),
  1936             ("ext_surjective", surject),
  1937             ("ext_split", split_meta)];
  1938 
  1939   in (thm_thy, extT, induct', inject', split_meta', ext_def) end;
  1940 
  1941 fun chunks [] [] = []
  1942   | chunks [] xs = [xs]
  1943   | chunks (l :: ls) xs = Library.take (l, xs) :: chunks ls (Library.drop (l, xs));
  1944 
  1945 fun chop_last [] = error "last: list should not be empty"
  1946   | chop_last [x] = ([], x)
  1947   | chop_last (x :: xs) = let val (tl, l) = chop_last xs in (x :: tl, l) end;
  1948 
  1949 fun subst_last s [] = error "subst_last: list should not be empty"
  1950   | subst_last s [x] = [s]
  1951   | subst_last s (x :: xs) = x :: subst_last s xs;
  1952 
  1953 
  1954 (* mk_recordT *)
  1955 
  1956 (*builds up the record type from the current extension tpye extT and a list
  1957   of parent extensions, starting with the root of the record hierarchy*)
  1958 fun mk_recordT extT =
  1959   fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT;
  1960 
  1961 
  1962 fun obj_to_meta_all thm =
  1963   let
  1964     fun E thm =  (* FIXME proper name *)
  1965       (case (SOME (spec OF [thm]) handle THM _ => NONE) of
  1966         SOME thm' => E thm'
  1967       | NONE => thm);
  1968     val th1 = E thm;
  1969     val th2 = Drule.forall_intr_vars th1;
  1970   in th2 end;
  1971 
  1972 fun meta_to_obj_all thm =
  1973   let
  1974     val thy = Thm.theory_of_thm thm;
  1975     val prop = Thm.prop_of thm;
  1976     val params = Logic.strip_params prop;
  1977     val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop);
  1978     val ct = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.list_all (params, concl)));
  1979     val thm' = Seq.hd (REPEAT (rtac allI 1) (Thm.trivial ct));
  1980   in Thm.implies_elim thm' thm end;
  1981 
  1982 
  1983 (* record_definition *)
  1984 
  1985 fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy =
  1986   let
  1987     val external_names = NameSpace.external_names (Sign.naming_of thy);
  1988 
  1989     val alphas = map fst args;
  1990     val name = Sign.full_bname thy bname;
  1991     val full = Sign.full_bname_path thy bname;
  1992     val base = Long_Name.base_name;
  1993 
  1994     val (bfields, field_syntax) =
  1995       split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
  1996 
  1997     val parent_fields = List.concat (map #fields parents);
  1998     val parent_chunks = map (length o #fields) parents;
  1999     val parent_names = map fst parent_fields;
  2000     val parent_types = map snd parent_fields;
  2001     val parent_fields_len = length parent_fields;
  2002     val parent_variants = Name.variant_list [moreN, rN, rN ^ "'", wN] (map base parent_names);
  2003     val parent_vars = ListPair.map Free (parent_variants, parent_types);
  2004     val parent_len = length parents;
  2005     val parents_idx = (map #name parents) ~~ (0 upto (parent_len - 1));
  2006 
  2007     val fields = map (apfst full) bfields;
  2008     val names = map fst fields;
  2009     val extN = full bname;
  2010     val types = map snd fields;
  2011     val alphas_fields = List.foldr OldTerm.add_typ_tfree_names [] types;
  2012     val alphas_ext = alphas inter alphas_fields;
  2013     val len = length fields;
  2014     val variants =
  2015       Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants) (map fst bfields);
  2016     val vars = ListPair.map Free (variants, types);
  2017     val named_vars = names ~~ vars;
  2018     val idxs = 0 upto (len - 1);
  2019     val idxms = 0 upto len;
  2020 
  2021     val all_fields = parent_fields @ fields;
  2022     val all_names = parent_names @ names;
  2023     val all_types = parent_types @ types;
  2024     val all_len = parent_fields_len + len;
  2025     val all_variants = parent_variants @ variants;
  2026     val all_vars = parent_vars @ vars;
  2027     val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
  2028 
  2029 
  2030     val zeta = Name.variant alphas "'z";
  2031     val moreT = TFree (zeta, HOLogic.typeS);
  2032     val more = Free (moreN, moreT);
  2033     val full_moreN = full moreN;
  2034     val bfields_more = bfields @ [(moreN, moreT)];
  2035     val fields_more = fields @ [(full_moreN, moreT)];
  2036     val vars_more = vars @ [more];
  2037     val named_vars_more = named_vars @ [(full_moreN, more)];
  2038     val all_vars_more = all_vars @ [more];
  2039     val all_named_vars_more = all_named_vars @ [(full_moreN, more)];
  2040 
  2041 
  2042     (* 1st stage: extension_thy *)
  2043 
  2044     val (extension_thy, extT, ext_induct, ext_inject, ext_split, ext_def) =
  2045       thy
  2046       |> Sign.add_path bname
  2047       |> extension_definition full extN fields names alphas_ext zeta moreT more vars;
  2048 
  2049     val _ = timing_msg "record preparing definitions";
  2050     val Type extension_scheme = extT;
  2051     val extension_name = unsuffix ext_typeN (fst extension_scheme);
  2052     val extension = let val (n, Ts) = extension_scheme in (n, subst_last HOLogic.unitT Ts) end;
  2053     val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extN];
  2054     val extension_id = Library.foldl (op ^) ("", extension_names);  (* FIXME implode!? *)
  2055 
  2056 
  2057     fun rec_schemeT n = mk_recordT (map #extension (prune n parents)) extT;
  2058     val rec_schemeT0 = rec_schemeT 0;
  2059 
  2060     fun recT n =
  2061       let val (c, Ts) = extension
  2062       in mk_recordT (map #extension (prune n parents)) (Type (c, subst_last HOLogic.unitT Ts)) end;
  2063     val recT0 = recT 0;
  2064 
  2065     fun mk_rec args n =
  2066       let
  2067         val (args', more) = chop_last args;
  2068         fun mk_ext' (((name, T), args), more) = mk_ext (name, T) (args @ [more]);
  2069         fun build Ts =
  2070           List.foldr mk_ext' more (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args')));
  2071       in
  2072         if more = HOLogic.unit
  2073         then build (map recT (0 upto parent_len))
  2074         else build (map rec_schemeT (0 upto parent_len))
  2075       end;
  2076 
  2077     val r_rec0 = mk_rec all_vars_more 0;
  2078     val r_rec_unit0 = mk_rec (all_vars @ [HOLogic.unit]) 0;
  2079 
  2080     fun r n = Free (rN, rec_schemeT n)
  2081     val r0 = r 0;
  2082     fun r_unit n = Free (rN, recT n)
  2083     val r_unit0 = r_unit 0;
  2084     val w = Free (wN, rec_schemeT 0)
  2085 
  2086 
  2087     (* prepare print translation functions *)
  2088 
  2089     val field_tr's =
  2090       print_translation (distinct (op =) (maps external_names (full_moreN :: names)));
  2091 
  2092     val adv_ext_tr's =
  2093       let val trnames = external_names extN
  2094       in map (gen_record_tr') trnames end;
  2095 
  2096     val adv_record_type_abbr_tr's =
  2097       let
  2098         val trnames = external_names (hd extension_names);
  2099         val lastExt = unsuffix ext_typeN (fst extension);
  2100       in map (gen_record_type_abbr_tr' name alphas zeta lastExt rec_schemeT0) trnames end;
  2101 
  2102     val adv_record_type_tr's =
  2103       let
  2104         val trnames = if parent_len > 0 then external_names extN else [];
  2105         (*avoid conflict with adv_record_type_abbr_tr's*)
  2106       in map (gen_record_type_tr') trnames end;
  2107 
  2108 
  2109     (* prepare declarations *)
  2110 
  2111     val sel_decls = map (mk_selC rec_schemeT0) bfields_more;
  2112     val upd_decls = map (mk_updC updateN rec_schemeT0) bfields_more;
  2113     val make_decl = (makeN, all_types ---> recT0);
  2114     val fields_decl = (fields_selN, types ---> Type extension);
  2115     val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0);
  2116     val truncate_decl = (truncateN, rec_schemeT0 --> recT0);
  2117 
  2118     (* prepare definitions *)
  2119 
  2120     fun parent_more s =
  2121       if null parents then s
  2122       else mk_sel s (Long_Name.qualify (#name (List.last parents)) moreN, extT);
  2123 
  2124     fun parent_more_upd v s =
  2125       if null parents then v $ s
  2126       else
  2127         let val mp = Long_Name.qualify (#name (List.last parents)) moreN;
  2128         in mk_upd updateN mp v s end;
  2129 
  2130     (*record (scheme) type abbreviation*)
  2131     val recordT_specs =
  2132       [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
  2133         (Binding.name bname, alphas, recT0, Syntax.NoSyn)];
  2134 
  2135     val ext_defs = ext_def :: map #extdef parents;
  2136     val intros_tac = IsTupleSupport.istuple_intros_tac extension_thy;
  2137 
  2138     (*Theorems from the istuple intros.
  2139       This is complex enough to deserve a full comment.
  2140       By unfolding ext_defs from r_rec0 we create a tree of constructor
  2141       calls (many of them Pair, but others as well). The introduction
  2142       rules for update_accessor_eq_assist can unify two different ways
  2143       on these constructors. If we take the complete result sequence of
  2144       running a the introduction tactic, we get one theorem for each upd/acc
  2145       pair, from which we can derive the bodies of our selector and
  2146       updator and their convs.*)
  2147     fun get_access_update_thms () =
  2148       let
  2149         val r_rec0_Vars =
  2150           let
  2151             (*pick variable indices of 1 to avoid possible variable
  2152               collisions with existing variables in updacc_eq_triv*)
  2153             fun to_Var (Free (c, T)) = Var ((c, 1), T);
  2154           in mk_rec (map to_Var all_vars_more) 0 end;
  2155 
  2156         val cterm_rec = cterm_of extension_thy r_rec0;
  2157         val cterm_vrs = cterm_of extension_thy r_rec0_Vars;
  2158         val insts = [("v", cterm_rec), ("v'", cterm_vrs)];
  2159         val init_thm = named_cterm_instantiate insts updacc_eq_triv;
  2160         val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
  2161         val tactic =
  2162           simp_tac (HOL_basic_ss addsimps ext_defs) 1 THEN
  2163           REPEAT (intros_tac 1 ORELSE terminal);
  2164         val updaccs = Seq.list_of (tactic init_thm);  (* FIXME Seq.lift_of *)
  2165       in
  2166         (updaccs RL [updacc_accessor_eqE],
  2167          updaccs RL [updacc_updator_eqE],
  2168          updaccs RL [updacc_cong_from_eq])
  2169       end;
  2170     val (accessor_thms, updator_thms, upd_acc_cong_assists) =
  2171       timeit_msg "record getting tree access/updates:" get_access_update_thms;
  2172 
  2173     fun lastN xs = List.drop (xs, parent_fields_len);
  2174 
  2175     (*selectors*)
  2176     fun mk_sel_spec ((c, T), thm) =
  2177       let
  2178         val acc $ arg =
  2179           (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Envir.beta_eta_contract o concl_of) thm;
  2180         val _ =
  2181           if (arg aconv r_rec0) then ()
  2182           else raise TERM ("mk_sel_spec: different arg", [arg]);
  2183       in
  2184         Const (mk_selC rec_schemeT0 (c, T)) :== acc
  2185       end;
  2186     val sel_specs = map mk_sel_spec (fields_more ~~ lastN accessor_thms);
  2187 
  2188 
  2189     (*updates*)
  2190     fun mk_upd_spec ((c, T), thm) =
  2191       let
  2192         val (upd $ _ $ arg) =
  2193           (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Envir.beta_eta_contract o concl_of) thm;
  2194         val _ =
  2195           if (arg aconv r_rec0) then ()
  2196           else raise TERM ("mk_sel_spec: different arg", [arg]);
  2197       in Const (mk_updC updateN rec_schemeT0 (c, T)) :== upd end;
  2198     val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms);
  2199 
  2200     (*derived operations*)
  2201     val make_spec = Const (full makeN, all_types ---> recT0) $$ all_vars :==
  2202       mk_rec (all_vars @ [HOLogic.unit]) 0;
  2203     val fields_spec = Const (full fields_selN, types ---> Type extension) $$ vars :==
  2204       mk_rec (all_vars @ [HOLogic.unit]) parent_len;
  2205     val extend_spec =
  2206       Const (full extendN, recT0-->moreT-->rec_schemeT0) $ r_unit0 $ more :==
  2207       mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
  2208     val truncate_spec = Const (full truncateN, rec_schemeT0 --> recT0) $ r0 :==
  2209       mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
  2210 
  2211 
  2212     (* 2st stage: defs_thy *)
  2213 
  2214     fun mk_defs () =
  2215       extension_thy
  2216       |> Sign.add_trfuns ([], [], field_tr's, [])
  2217       |> Sign.add_advanced_trfuns
  2218           ([], [], adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's, [])
  2219       |> Sign.parent_path
  2220       |> Sign.add_tyabbrs_i recordT_specs
  2221       |> Sign.add_path bname
  2222       |> Sign.add_consts_i
  2223           (map2 (fn (x, T) => fn mx => (Binding.name x, T, mx))
  2224             sel_decls (field_syntax @ [Syntax.NoSyn]))
  2225       |> (Sign.add_consts_i o map (fn (x, T) => (Binding.name x, T, Syntax.NoSyn)))
  2226           (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
  2227       |> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) sel_specs)
  2228       ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) upd_specs)
  2229       ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name))
  2230              [make_spec, fields_spec, extend_spec, truncate_spec])
  2231       |->
  2232         (fn defs as ((sel_defs, upd_defs), derived_defs) =>
  2233           fold Code.add_default_eqn sel_defs
  2234           #> fold Code.add_default_eqn upd_defs
  2235           #> fold Code.add_default_eqn derived_defs
  2236           #> pair defs)
  2237     val (((sel_defs, upd_defs), derived_defs), defs_thy) =
  2238       timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
  2239         mk_defs;
  2240 
  2241     (* prepare propositions *)
  2242     val _ = timing_msg "record preparing propositions";
  2243     val P = Free (Name.variant all_variants "P", rec_schemeT0 --> HOLogic.boolT);
  2244     val C = Free (Name.variant all_variants "C", HOLogic.boolT);
  2245     val P_unit = Free (Name.variant all_variants "P", recT0 --> HOLogic.boolT);
  2246 
  2247     (*selectors*)
  2248     val sel_conv_props =
  2249        map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more;
  2250 
  2251     (*updates*)
  2252     fun mk_upd_prop (i, (c, T)) =
  2253       let
  2254         val x' = Free (Name.variant all_variants (base c ^ "'"), T --> T);
  2255         val n = parent_fields_len + i;
  2256         val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more
  2257       in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
  2258     val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
  2259 
  2260     (*induct*)
  2261     val induct_scheme_prop =
  2262       All (map dest_Free all_vars_more) (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0);
  2263     val induct_prop =
  2264       (All (map dest_Free all_vars) (Trueprop (P_unit $ r_rec_unit0)),
  2265         Trueprop (P_unit $ r_unit0));
  2266 
  2267     (*surjective*)
  2268     val surjective_prop =
  2269       let val args = map (fn (c, Free (_, T)) => mk_sel r0 (c, T)) all_named_vars_more
  2270       in r0 === mk_rec args 0 end;
  2271 
  2272     (*cases*)
  2273     val cases_scheme_prop =
  2274       (All (map dest_Free all_vars_more)
  2275         (Trueprop (HOLogic.mk_eq (r0, r_rec0)) ==> Trueprop C))
  2276       ==> Trueprop C;
  2277 
  2278     val cases_prop =
  2279       (All (map dest_Free all_vars)
  2280         (Trueprop (HOLogic.mk_eq (r_unit0, r_rec_unit0)) ==> Trueprop C))
  2281        ==> Trueprop C;
  2282 
  2283     (*split*)
  2284     val split_meta_prop =
  2285       let val P = Free (Name.variant all_variants "P", rec_schemeT0-->Term.propT) in
  2286         Logic.mk_equals
  2287          (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
  2288       end;
  2289 
  2290     (* FIXME eliminate old List.foldr *)
  2291 
  2292     val split_object_prop =
  2293       let fun ALL vs t = List.foldr (fn ((v, T), t) => HOLogic.mk_all (v, T, t)) t vs
  2294       in (ALL [dest_Free r0] (P $ r0)) === (ALL (map dest_Free all_vars_more) (P $ r_rec0)) end;
  2295 
  2296     val split_ex_prop =
  2297       let fun EX vs t = List.foldr (fn ((v, T), t) => HOLogic.mk_exists (v, T, t)) t vs
  2298       in (EX [dest_Free r0] (P $ r0)) === (EX (map dest_Free all_vars_more) (P $ r_rec0)) end;
  2299 
  2300     (*equality*)
  2301     val equality_prop =
  2302       let
  2303         val s' = Free (rN ^ "'", rec_schemeT0);
  2304         fun mk_sel_eq (c, Free (_, T)) = mk_sel r0 (c, T) === mk_sel s' (c, T);
  2305         val seleqs = map mk_sel_eq all_named_vars_more;
  2306       in All (map dest_Free [r0, s']) (Logic.list_implies (seleqs, r0 === s')) end;
  2307 
  2308 
  2309     (* 3rd stage: thms_thy *)
  2310 
  2311     fun prove stndrd = quick_and_dirty_prove stndrd defs_thy;
  2312     val prove_standard = quick_and_dirty_prove true defs_thy;
  2313 
  2314     fun prove_simp stndrd ss simps =
  2315       let val tac = simp_all_tac ss simps
  2316       in fn prop => prove stndrd [] prop (K tac) end;
  2317 
  2318     val ss = get_simpset defs_thy;
  2319 
  2320     fun sel_convs_prf () =
  2321       map (prove_simp false ss (sel_defs @ accessor_thms)) sel_conv_props;
  2322     val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
  2323     fun sel_convs_standard_prf () = map standard sel_convs
  2324     val sel_convs_standard =
  2325       timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf;
  2326 
  2327     fun upd_convs_prf () =
  2328       map (prove_simp false ss (upd_defs @ updator_thms)) upd_conv_props;
  2329     val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
  2330     fun upd_convs_standard_prf () = map standard upd_convs
  2331     val upd_convs_standard =
  2332       timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf;
  2333 
  2334     fun get_upd_acc_congs () =
  2335       let
  2336         val symdefs = map symmetric (sel_defs @ upd_defs);
  2337         val fold_ss = HOL_basic_ss addsimps symdefs;
  2338         val ua_congs = map (standard o simplify fold_ss) upd_acc_cong_assists;
  2339       in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
  2340     val (fold_congs, unfold_congs) =
  2341       timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
  2342 
  2343     val parent_induct = if null parents then [] else [#induct (hd (rev parents))];
  2344 
  2345     fun induct_scheme_prf () =
  2346       prove_standard [] induct_scheme_prop
  2347         (fn _ =>
  2348           EVERY
  2349            [if null parent_induct
  2350             then all_tac else try_param_tac rN (hd parent_induct) 1,
  2351             try_param_tac rN ext_induct 1,
  2352             asm_simp_tac HOL_basic_ss 1]);
  2353     val induct_scheme = timeit_msg "record induct_scheme proof:" induct_scheme_prf;
  2354 
  2355     fun induct_prf () =
  2356       let val (assm, concl) = induct_prop in
  2357         prove_standard [assm] concl (fn {prems, ...} =>
  2358           try_param_tac rN induct_scheme 1
  2359           THEN try_param_tac "more" @{thm unit.induct} 1
  2360           THEN resolve_tac prems 1)
  2361       end;
  2362     val induct = timeit_msg "record induct proof:" induct_prf;
  2363 
  2364     fun cases_scheme_prf_opt () =
  2365       let
  2366         val _ $ (Pvar $ _) = concl_of induct_scheme;
  2367         val ind =
  2368           cterm_instantiate
  2369             [(cterm_of defs_thy Pvar, cterm_of defs_thy
  2370               (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
  2371             induct_scheme;
  2372         in standard (ObjectLogic.rulify (mp OF [ind, refl])) end;
  2373 
  2374     fun cases_scheme_prf_noopt () =
  2375       prove_standard [] cases_scheme_prop
  2376         (fn _ =>
  2377           EVERY
  2378            [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
  2379             try_param_tac rN induct_scheme 1,
  2380             rtac impI 1,
  2381             REPEAT (etac allE 1),
  2382             etac mp 1,
  2383             rtac refl 1]);
  2384     val cases_scheme_prf = quick_and_dirty_prf cases_scheme_prf_noopt cases_scheme_prf_opt;
  2385     val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
  2386 
  2387     fun cases_prf () =
  2388       prove_standard [] cases_prop
  2389         (fn _ =>
  2390           try_param_tac rN cases_scheme 1 THEN
  2391           simp_all_tac HOL_basic_ss [unit_all_eq1]);
  2392     val cases = timeit_msg "record cases proof:" cases_prf;
  2393 
  2394     fun surjective_prf () =
  2395       let
  2396         val leaf_ss = get_sel_upd_defs defs_thy addsimps (sel_defs @ (o_assoc :: id_o_apps));
  2397         val init_ss = HOL_basic_ss addsimps ext_defs;
  2398       in
  2399         prove_standard [] surjective_prop
  2400           (fn prems =>
  2401             EVERY
  2402              [rtac surject_assist_idE 1,
  2403               simp_tac init_ss 1,
  2404               REPEAT (intros_tac 1 ORELSE (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
  2405       end;
  2406     val surjective = timeit_msg "record surjective proof:" surjective_prf;
  2407 
  2408     fun split_meta_prf () =
  2409       prove false [] split_meta_prop
  2410         (fn prems =>
  2411           EVERY
  2412            [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
  2413             etac meta_allE 1, atac 1,
  2414             rtac (prop_subst OF [surjective]) 1,
  2415             REPEAT (etac meta_allE 1), atac 1]);
  2416     val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
  2417     fun split_meta_standardise () = standard split_meta;
  2418     val split_meta_standard =
  2419       timeit_msg "record split_meta standard:" split_meta_standardise;
  2420 
  2421     fun split_object_prf_opt () =
  2422       let
  2423         val cPI= cterm_of defs_thy (lambda r0 (Trueprop (P $ r0)));
  2424         val _ $ Abs (_, _, P $ _) = fst (Logic.dest_equals (concl_of split_meta_standard));
  2425         val cP = cterm_of defs_thy P;
  2426         val split_meta' = cterm_instantiate [(cP, cPI)] split_meta_standard;
  2427         val (l, r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop);
  2428         val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l);
  2429         val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r);
  2430         val thl =
  2431           assume cl                   (*All r. P r*) (* 1 *)
  2432           |> obj_to_meta_all          (*!!r. P r*)
  2433           |> equal_elim split_meta'   (*!!n m more. P (ext n m more)*)
  2434           |> meta_to_obj_all          (*All n m more. P (ext n m more)*) (* 2*)
  2435           |> implies_intr cl          (* 1 ==> 2 *)
  2436         val thr =
  2437           assume cr                             (*All n m more. P (ext n m more)*)
  2438           |> obj_to_meta_all                    (*!!n m more. P (ext n m more)*)
  2439           |> equal_elim (symmetric split_meta') (*!!r. P r*)
  2440           |> meta_to_obj_all                    (*All r. P r*)
  2441           |> implies_intr cr                    (* 2 ==> 1 *)
  2442      in standard (thr COMP (thl COMP iffI)) end;
  2443 
  2444     fun split_object_prf_noopt () =
  2445       prove_standard [] split_object_prop
  2446         (fn _ =>
  2447           EVERY
  2448            [rtac iffI 1,
  2449             REPEAT (rtac allI 1), etac allE 1, atac 1,
  2450             rtac allI 1, rtac induct_scheme 1, REPEAT (etac allE 1), atac 1]);
  2451 
  2452     val split_object_prf = quick_and_dirty_prf split_object_prf_noopt split_object_prf_opt;
  2453     val split_object = timeit_msg "record split_object proof:" split_object_prf;
  2454 
  2455 
  2456     fun split_ex_prf () =
  2457       let
  2458         val ss = HOL_basic_ss addsimps [not_ex RS sym, Not_eq_iff];
  2459         val P_nm = fst (dest_Free P);
  2460         val not_P = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
  2461         val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object;
  2462         val so'' = simplify ss so';
  2463       in
  2464         prove_standard [] split_ex_prop (fn prems => resolve_tac [so''] 1)
  2465       end;
  2466     val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
  2467 
  2468     fun equality_tac thms =
  2469       let
  2470         val s' :: s :: eqs = rev thms;
  2471         val ss' = ss addsimps (s' :: s :: sel_convs_standard);
  2472         val eqs' = map (simplify ss') eqs;
  2473       in simp_tac (HOL_basic_ss addsimps (s' :: s :: eqs')) 1 end;
  2474 
  2475     fun equality_prf () =
  2476       prove_standard [] equality_prop (fn {context, ...} =>
  2477         fn st =>
  2478           let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
  2479             st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1 THEN
  2480               res_inst_tac context [((rN, 0), s')] cases_scheme 1 THEN
  2481               Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1)
  2482              (*simp_all_tac ss (sel_convs) would also work but is less efficient*)
  2483           end);
  2484     val equality = timeit_msg "record equality proof:" equality_prf;
  2485 
  2486     val ((([sel_convs', upd_convs', sel_defs', upd_defs',
  2487             fold_congs', unfold_congs',
  2488           [split_meta', split_object', split_ex'], derived_defs'],
  2489           [surjective', equality']),
  2490           [induct_scheme', induct', cases_scheme', cases']), thms_thy) =
  2491       defs_thy
  2492       |> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
  2493          [("select_convs", sel_convs_standard),
  2494           ("update_convs", upd_convs_standard),
  2495           ("select_defs", sel_defs),
  2496           ("update_defs", upd_defs),
  2497           ("fold_congs", fold_congs),
  2498           ("unfold_congs", unfold_congs),
  2499           ("splits", [split_meta_standard, split_object, split_ex]),
  2500           ("defs", derived_defs)]
  2501       ||>> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
  2502           [("surjective", surjective),
  2503            ("equality", equality)]
  2504       ||>> (PureThy.add_thms o (map o apfst o apfst) Binding.name)
  2505         [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
  2506          (("induct", induct), induct_type_global name),
  2507          (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
  2508          (("cases", cases), cases_type_global name)];
  2509 
  2510     val sel_upd_simps = sel_convs' @ upd_convs';
  2511     val sel_upd_defs = sel_defs' @ upd_defs';
  2512     val iffs = [ext_inject]
  2513     val depth = parent_len + 1;
  2514     val final_thy =
  2515       thms_thy
  2516       |> (snd oo PureThy.add_thmss)
  2517           [((Binding.name "simps", sel_upd_simps),
  2518             [Simplifier.simp_add, Nitpick_Const_Simps.add]),
  2519            ((Binding.name "iffs", iffs), [iff_add])]
  2520       |> put_record name (make_record_info args parent fields extension induct_scheme' ext_def)
  2521       |> put_sel_upd names full_moreN depth sel_upd_simps
  2522                            sel_upd_defs (fold_congs', unfold_congs')
  2523       |> add_record_equalities extension_id equality'
  2524       |> add_extinjects ext_inject
  2525       |> add_extsplit extension_name ext_split
  2526       |> add_record_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
  2527       |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
  2528       |> add_fieldext (extension_name, snd extension) (names @ [full_moreN])
  2529       |> Sign.parent_path;
  2530 
  2531   in final_thy end;
  2532 
  2533 
  2534 (* add_record *)
  2535 
  2536 (*We do all preparations and error checks here, deferring the real
  2537   work to record_definition.*)
  2538 fun gen_add_record prep_typ prep_raw_parent quiet_mode (params, bname) raw_parent raw_fields thy =
  2539   let
  2540     val _ = Theory.requires thy "Record" "record definitions";
  2541     val _ = if quiet_mode then () else writeln ("Defining record " ^ quote bname ^ " ...");
  2542 
  2543     val ctxt = ProofContext.init thy;
  2544 
  2545 
  2546     (* parents *)
  2547 
  2548     fun prep_inst T = fst (cert_typ ctxt T []);
  2549 
  2550     val parent = Option.map (apfst (map prep_inst) o prep_raw_parent ctxt) raw_parent
  2551       handle ERROR msg => cat_error msg ("The error(s) above in parent record specification");
  2552     val parents = add_parents thy parent [];
  2553 
  2554     val init_env =
  2555       (case parent of
  2556         NONE => []
  2557       | SOME (types, _) => List.foldr OldTerm.add_typ_tfrees [] types);
  2558 
  2559 
  2560     (* fields *)
  2561 
  2562     fun prep_field (c, raw_T, mx) env =
  2563       let val (T, env') = prep_typ ctxt raw_T env handle ERROR msg =>
  2564         cat_error msg ("The error(s) above occured in record field " ^ quote c)
  2565       in ((c, T, mx), env') end;
  2566 
  2567     val (bfields, envir) = fold_map prep_field raw_fields init_env;
  2568     val envir_names = map fst envir;
  2569 
  2570 
  2571     (* args *)
  2572 
  2573     val defaultS = Sign.defaultS thy;
  2574     val args = map (fn x => (x, AList.lookup (op =) envir x |> the_default defaultS)) params;
  2575 
  2576 
  2577     (* errors *)
  2578 
  2579     val name = Sign.full_bname thy bname;
  2580     val err_dup_record =
  2581       if is_none (get_record thy name) then []
  2582       else ["Duplicate definition of record " ^ quote name];
  2583 
  2584     val err_dup_parms =
  2585       (case duplicates (op =) params of
  2586         [] => []
  2587       | dups => ["Duplicate parameter(s) " ^ commas dups]);
  2588 
  2589     val err_extra_frees =
  2590       (case subtract (op =) params envir_names of
  2591         [] => []
  2592       | extras => ["Extra free type variable(s) " ^ commas extras]);
  2593 
  2594     val err_no_fields = if null bfields then ["No fields present"] else [];
  2595 
  2596     val err_dup_fields =
  2597       (case duplicates (op =) (map #1 bfields) of
  2598         [] => []
  2599       | dups => ["Duplicate field(s) " ^ commas_quote dups]);
  2600 
  2601     val err_bad_fields =
  2602       if forall (not_equal moreN o #1) bfields then []
  2603       else ["Illegal field name " ^ quote moreN];
  2604 
  2605     val err_dup_sorts =
  2606       (case duplicates (op =) envir_names of
  2607         [] => []
  2608       | dups => ["Inconsistent sort constraints for " ^ commas dups]);
  2609 
  2610     val errs =
  2611       err_dup_record @ err_dup_parms @ err_extra_frees @ err_no_fields @
  2612       err_dup_fields @ err_bad_fields @ err_dup_sorts;
  2613 
  2614     val _ = if null errs then () else error (cat_lines errs);
  2615   in
  2616     thy |> record_definition (args, bname) parent parents bfields
  2617   end
  2618   handle ERROR msg => cat_error msg ("Failed to define record " ^ quote bname);
  2619 
  2620 val add_record = gen_add_record read_typ read_raw_parent;
  2621 val add_record_i = gen_add_record cert_typ (K I);
  2622 
  2623 
  2624 (* setup theory *)
  2625 
  2626 val setup =
  2627   Sign.add_trfuns ([], parse_translation, [], []) #>
  2628   Sign.add_advanced_trfuns ([], adv_parse_translation, [], []) #>
  2629   Simplifier.map_simpset (fn ss =>
  2630     ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]);
  2631 
  2632 
  2633 (* outer syntax *)
  2634 
  2635 local structure P = OuterParse and K = OuterKeyword in
  2636 
  2637 val record_decl =
  2638   P.type_args -- P.name --
  2639     (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
  2640 
  2641 val _ =
  2642   OuterSyntax.command "record" "define extensible record" K.thy_decl
  2643     (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record false x y z)));
  2644 
  2645 end;
  2646 
  2647 end;
  2648 
  2649 structure Basic_Record: BASIC_RECORD = Record;
  2650 open Basic_Record;