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