src/HOL/Tools/record.ML
author wenzelm
Fri Oct 12 21:22:35 2012 +0200 (2012-10-12)
changeset 49835 31f32ec4d766
parent 49833 1d80798e8d8a
child 51143 0a2371e7ced3
permissions -rw-r--r--
discontinued typedef with alternative name;
     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 RECORD =
    11 sig
    12   val type_abbr: bool Config.T
    13   val type_as_fields: bool Config.T
    14   val timing: bool Config.T
    15 
    16   type info =
    17    {args: (string * sort) list,
    18     parent: (typ list * string) option,
    19     fields: (string * typ) list,
    20     extension: (string * typ list),
    21     ext_induct: thm, ext_inject: thm, ext_surjective: thm, ext_split: thm, ext_def: thm,
    22     select_convs: thm list, update_convs: thm list, select_defs: thm list, update_defs: thm list,
    23     fold_congs: thm list, unfold_congs: thm list, splits: thm list, defs: thm list,
    24     surjective: thm, equality: thm, induct_scheme: thm, induct: thm, cases_scheme: thm,
    25     cases: thm, simps: thm list, iffs: thm list}
    26   val get_info: theory -> string -> info option
    27   val the_info: theory -> string -> info
    28   val get_hierarchy: theory -> (string * typ list) -> (string * ((string * sort) * typ) list) list
    29   val add_record: (string * sort) list * binding -> (typ list * string) option ->
    30     (binding * typ * mixfix) list -> theory -> theory
    31 
    32   val last_extT: typ -> (string * typ list) option
    33   val dest_recTs: typ -> (string * typ list) list
    34   val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ)
    35   val get_recT_fields: theory -> typ -> (string * typ) list * (string * typ)
    36   val get_parent: theory -> string -> (typ list * string) option
    37   val get_extension: theory -> string -> (string * typ list) option
    38   val get_extinjects: theory -> thm list
    39   val get_simpset: theory -> simpset
    40   val simproc: simproc
    41   val eq_simproc: simproc
    42   val upd_simproc: simproc
    43   val split_simproc: (term -> int) -> simproc
    44   val ex_sel_eq_simproc: simproc
    45   val split_tac: int -> tactic
    46   val split_simp_tac: thm list -> (term -> int) -> int -> tactic
    47   val split_wrapper: string * (Proof.context -> wrapper)
    48 
    49   val codegen: bool Config.T
    50   val updateN: string
    51   val ext_typeN: string
    52   val extN: string
    53   val setup: theory -> theory
    54 end;
    55 
    56 
    57 signature ISO_TUPLE_SUPPORT =
    58 sig
    59   val add_iso_tuple_type: binding * (string * sort) list ->
    60     typ * typ -> theory -> (term * term) * theory
    61   val mk_cons_tuple: term * term -> term
    62   val dest_cons_tuple: term -> term * term
    63   val iso_tuple_intros_tac: int -> tactic
    64   val named_cterm_instantiate: (string * cterm) list -> thm -> thm
    65 end;
    66 
    67 structure Iso_Tuple_Support: ISO_TUPLE_SUPPORT =
    68 struct
    69 
    70 val isoN = "_Tuple_Iso";
    71 
    72 val iso_tuple_intro = @{thm isomorphic_tuple_intro};
    73 val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};
    74 
    75 val tuple_iso_tuple = (@{const_name Record.tuple_iso_tuple}, @{thm tuple_iso_tuple});
    76 
    77 fun named_cterm_instantiate values thm =  (* FIXME eliminate *)
    78   let
    79     fun match name ((name', _), _) = name = name';
    80     fun getvar name =
    81       (case find_first (match name) (Term.add_vars (prop_of thm) []) of
    82         SOME var => cterm_of (theory_of_thm thm) (Var var)
    83       | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm]));
    84   in
    85     cterm_instantiate (map (apfst getvar) values) thm
    86   end;
    87 
    88 structure Iso_Tuple_Thms = Theory_Data
    89 (
    90   type T = thm Symtab.table;
    91   val empty = Symtab.make [tuple_iso_tuple];
    92   val extend = I;
    93   fun merge data = Symtab.merge Thm.eq_thm_prop data;   (* FIXME handle Symtab.DUP ?? *)
    94 );
    95 
    96 fun get_typedef_info tyco vs
    97     (({rep_type, Abs_name, ...}, {Rep_inject, Abs_inverse, ... }) : Typedef.info) thy =
    98   let
    99     val exists_thm =
   100       UNIV_I
   101       |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] [];
   102     val proj_constr = Abs_inverse OF [exists_thm];
   103     val absT = Type (tyco, map TFree vs);
   104   in
   105     thy
   106     |> pair (tyco, ((Rep_inject, proj_constr), Const (Abs_name, rep_type --> absT), absT))
   107   end
   108 
   109 fun do_typedef raw_tyco repT raw_vs thy =
   110   let
   111     val ctxt = Proof_Context.init_global thy |> Variable.declare_typ repT;
   112     val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
   113   in
   114     thy
   115     |> Typedef.add_typedef_global (raw_tyco, vs, NoSyn)
   116         (HOLogic.mk_UNIV repT) NONE (rtac UNIV_witness 1)
   117     |-> (fn (tyco, info) => get_typedef_info tyco vs info)
   118   end;
   119 
   120 fun mk_cons_tuple (left, right) =
   121   let
   122     val (leftT, rightT) = (fastype_of left, fastype_of right);
   123     val prodT = HOLogic.mk_prodT (leftT, rightT);
   124     val isomT = Type (@{type_name tuple_isomorphism}, [prodT, leftT, rightT]);
   125   in
   126     Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $
   127       Const (fst tuple_iso_tuple, isomT) $ left $ right
   128   end;
   129 
   130 fun dest_cons_tuple (Const (@{const_name Record.iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
   131   | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
   132 
   133 fun add_iso_tuple_type (b, alphas) (leftT, rightT) thy =
   134   let
   135     val repT = HOLogic.mk_prodT (leftT, rightT);
   136 
   137     val ((_, ((rep_inject, abs_inverse), absC, absT)), typ_thy) =
   138       thy
   139       |> do_typedef b repT alphas
   140       ||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*)
   141 
   142     (*construct a type and body for the isomorphism constant by
   143       instantiating the theorem to which the definition will be applied*)
   144     val intro_inst =
   145       rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] iso_tuple_intro;
   146     val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
   147     val isomT = fastype_of body;
   148     val isom_binding = Binding.suffix_name isoN b;
   149     val isom_name = Sign.full_name typ_thy isom_binding;
   150     val isom = Const (isom_name, isomT);
   151 
   152     val ([isom_def], cdef_thy) =
   153       typ_thy
   154       |> Sign.declare_const_global ((isom_binding, isomT), NoSyn) |> snd
   155       |> Global_Theory.add_defs false
   156         [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
   157 
   158     val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
   159     val cons = Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
   160 
   161     val thm_thy =
   162       cdef_thy
   163       |> Iso_Tuple_Thms.map (Symtab.insert Thm.eq_thm_prop (isom_name, iso_tuple))
   164       |> Sign.restore_naming thy
   165   in
   166     ((isom, cons $ isom), thm_thy)
   167   end;
   168 
   169 val iso_tuple_intros_tac =
   170   resolve_from_net_tac iso_tuple_intros THEN'
   171   CSUBGOAL (fn (cgoal, i) =>
   172     let
   173       val thy = Thm.theory_of_cterm cgoal;
   174       val goal = Thm.term_of cgoal;
   175 
   176       val isthms = Iso_Tuple_Thms.get thy;
   177       fun err s t = raise TERM ("iso_tuple_intros_tac: " ^ s, [t]);
   178 
   179       val goal' = Envir.beta_eta_contract goal;
   180       val is =
   181         (case goal' of
   182           Const (@{const_name Trueprop}, _) $
   183             (Const (@{const_name isomorphic_tuple}, _) $ Const is) => is
   184         | _ => err "unexpected goal format" goal');
   185       val isthm =
   186         (case Symtab.lookup isthms (#1 is) of
   187           SOME isthm => isthm
   188         | NONE => err "no thm found for constant" (Const is));
   189     in rtac isthm i end);
   190 
   191 end;
   192 
   193 
   194 structure Record: RECORD =
   195 struct
   196 
   197 val surject_assistI = @{thm iso_tuple_surjective_proof_assistI};
   198 val surject_assist_idE = @{thm iso_tuple_surjective_proof_assist_idE};
   199 
   200 val updacc_accessor_eqE = @{thm update_accessor_accessor_eqE};
   201 val updacc_updator_eqE = @{thm update_accessor_updator_eqE};
   202 val updacc_eq_idI = @{thm iso_tuple_update_accessor_eq_assist_idI};
   203 val updacc_eq_triv = @{thm iso_tuple_update_accessor_eq_assist_triv};
   204 
   205 val updacc_foldE = @{thm update_accessor_congruence_foldE};
   206 val updacc_unfoldE = @{thm update_accessor_congruence_unfoldE};
   207 val updacc_noopE = @{thm update_accessor_noopE};
   208 val updacc_noop_compE = @{thm update_accessor_noop_compE};
   209 val updacc_cong_idI = @{thm update_accessor_cong_assist_idI};
   210 val updacc_cong_triv = @{thm update_accessor_cong_assist_triv};
   211 val updacc_cong_from_eq = @{thm iso_tuple_update_accessor_cong_from_eq};
   212 
   213 val codegen = Attrib.setup_config_bool @{binding record_codegen} (K true);
   214 
   215 
   216 (** name components **)
   217 
   218 val rN = "r";
   219 val wN = "w";
   220 val moreN = "more";
   221 val schemeN = "_scheme";
   222 val ext_typeN = "_ext";
   223 val inner_typeN = "_inner";
   224 val extN ="_ext";
   225 val updateN = "_update";
   226 val makeN = "make";
   227 val fields_selN = "fields";
   228 val extendN = "extend";
   229 val truncateN = "truncate";
   230 
   231 
   232 
   233 (*** utilities ***)
   234 
   235 fun varifyT idx = map_type_tfree (fn (a, S) => TVar ((a, idx), S));
   236 
   237 
   238 (* timing *)
   239 
   240 val timing = Attrib.setup_config_bool @{binding record_timing} (K false);
   241 fun timeit_msg ctxt s x = if Config.get ctxt timing then (warning s; timeit x) else x ();
   242 fun timing_msg ctxt s = if Config.get ctxt timing then warning s else ();
   243 
   244 
   245 (* syntax *)
   246 
   247 val Trueprop = HOLogic.mk_Trueprop;
   248 
   249 infix 0 :== ===;
   250 infixr 0 ==>;
   251 
   252 val op :== = Misc_Legacy.mk_defpair;
   253 val op === = Trueprop o HOLogic.mk_eq;
   254 val op ==> = Logic.mk_implies;
   255 
   256 
   257 (* constructor *)
   258 
   259 fun mk_ext (name, T) ts =
   260   let val Ts = map fastype_of ts
   261   in list_comb (Const (suffix extN name, Ts ---> T), ts) end;
   262 
   263 
   264 (* selector *)
   265 
   266 fun mk_selC sT (c, T) = (c, sT --> T);
   267 
   268 fun mk_sel s (c, T) =
   269   let val sT = fastype_of s
   270   in Const (mk_selC sT (c, T)) $ s end;
   271 
   272 
   273 (* updates *)
   274 
   275 fun mk_updC sfx sT (c, T) = (suffix sfx c, (T --> T) --> sT --> sT);
   276 
   277 fun mk_upd' sfx c v sT =
   278   let val vT = domain_type (fastype_of v);
   279   in Const (mk_updC sfx sT (c, vT)) $ v end;
   280 
   281 fun mk_upd sfx c v s = mk_upd' sfx c v (fastype_of s) $ s;
   282 
   283 
   284 (* types *)
   285 
   286 fun dest_recT (typ as Type (c_ext_type, Ts as (_ :: _))) =
   287       (case try (unsuffix ext_typeN) c_ext_type of
   288         NONE => raise TYPE ("Record.dest_recT", [typ], [])
   289       | SOME c => ((c, Ts), List.last Ts))
   290   | dest_recT typ = raise TYPE ("Record.dest_recT", [typ], []);
   291 
   292 val is_recT = can dest_recT;
   293 
   294 fun dest_recTs T =
   295   let val ((c, Ts), U) = dest_recT T
   296   in (c, Ts) :: dest_recTs U
   297   end handle TYPE _ => [];
   298 
   299 fun last_extT T =
   300   let val ((c, Ts), U) = dest_recT T in
   301     (case last_extT U of
   302       NONE => SOME (c, Ts)
   303     | SOME l => SOME l)
   304   end handle TYPE _ => NONE;
   305 
   306 fun rec_id i T =
   307   let
   308     val rTs = dest_recTs T;
   309     val rTs' = if i < 0 then rTs else take i rTs;
   310   in implode (map #1 rTs') end;
   311 
   312 
   313 
   314 (*** extend theory by record definition ***)
   315 
   316 (** record info **)
   317 
   318 (* type info and parent_info *)
   319 
   320 type info =
   321  {args: (string * sort) list,
   322   parent: (typ list * string) option,
   323   fields: (string * typ) list,
   324   extension: (string * typ list),
   325 
   326   ext_induct: thm,
   327   ext_inject: thm,
   328   ext_surjective: thm,
   329   ext_split: thm,
   330   ext_def: thm,
   331 
   332   select_convs: thm list,
   333   update_convs: thm list,
   334   select_defs: thm list,
   335   update_defs: thm list,
   336   fold_congs: thm list,  (* potentially used in L4.verified *)
   337   unfold_congs: thm list,  (* potentially used in L4.verified *)
   338   splits: thm list,
   339   defs: thm list,
   340 
   341   surjective: thm,
   342   equality: thm,
   343   induct_scheme: thm,
   344   induct: thm,
   345   cases_scheme: thm,
   346   cases: thm,
   347 
   348   simps: thm list,
   349   iffs: thm list};
   350 
   351 fun make_info args parent fields extension
   352     ext_induct ext_inject ext_surjective ext_split ext_def
   353     select_convs update_convs select_defs update_defs fold_congs unfold_congs splits defs
   354     surjective equality induct_scheme induct cases_scheme cases
   355     simps iffs : info =
   356  {args = args, parent = parent, fields = fields, extension = extension,
   357   ext_induct = ext_induct, ext_inject = ext_inject, ext_surjective = ext_surjective,
   358   ext_split = ext_split, ext_def = ext_def, select_convs = select_convs,
   359   update_convs = update_convs, select_defs = select_defs, update_defs = update_defs,
   360   fold_congs = fold_congs, unfold_congs = unfold_congs, splits = splits, defs = defs,
   361   surjective = surjective, equality = equality, induct_scheme = induct_scheme,
   362   induct = induct, cases_scheme = cases_scheme, cases = cases, simps = simps, iffs = iffs};
   363 
   364 type parent_info =
   365  {name: string,
   366   fields: (string * typ) list,
   367   extension: (string * typ list),
   368   induct_scheme: thm,
   369   ext_def: thm};
   370 
   371 fun make_parent_info name fields extension ext_def induct_scheme : parent_info =
   372  {name = name, fields = fields, extension = extension,
   373   ext_def = ext_def, induct_scheme = induct_scheme};
   374 
   375 
   376 (* theory data *)
   377 
   378 type data =
   379  {records: info Symtab.table,
   380   sel_upd:
   381    {selectors: (int * bool) Symtab.table,
   382     updates: string Symtab.table,
   383     simpset: simpset,
   384     defset: simpset},
   385   equalities: thm Symtab.table,
   386   extinjects: thm list,
   387   extsplit: thm Symtab.table,  (*maps extension name to split rule*)
   388   splits: (thm * thm * thm * thm) Symtab.table,  (*!!, ALL, EX - split-equalities, induct rule*)
   389   extfields: (string * typ) list Symtab.table,  (*maps extension to its fields*)
   390   fieldext: (string * typ list) Symtab.table};  (*maps field to its extension*)
   391 
   392 fun make_data
   393     records sel_upd equalities extinjects extsplit splits extfields fieldext =
   394  {records = records, sel_upd = sel_upd,
   395   equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
   396   extfields = extfields, fieldext = fieldext }: data;
   397 
   398 structure Data = Theory_Data
   399 (
   400   type T = data;
   401   val empty =
   402     make_data Symtab.empty
   403       {selectors = Symtab.empty, updates = Symtab.empty,
   404         simpset = HOL_basic_ss, defset = HOL_basic_ss}
   405        Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
   406   val extend = I;
   407   fun merge
   408    ({records = recs1,
   409      sel_upd = {selectors = sels1, updates = upds1, simpset = ss1, defset = ds1},
   410      equalities = equalities1,
   411      extinjects = extinjects1,
   412      extsplit = extsplit1,
   413      splits = splits1,
   414      extfields = extfields1,
   415      fieldext = fieldext1},
   416     {records = recs2,
   417      sel_upd = {selectors = sels2, updates = upds2, simpset = ss2, defset = ds2},
   418      equalities = equalities2,
   419      extinjects = extinjects2,
   420      extsplit = extsplit2,
   421      splits = splits2,
   422      extfields = extfields2,
   423      fieldext = fieldext2}) =
   424     make_data
   425       (Symtab.merge (K true) (recs1, recs2))
   426       {selectors = Symtab.merge (K true) (sels1, sels2),
   427         updates = Symtab.merge (K true) (upds1, upds2),
   428         simpset = Simplifier.merge_ss (ss1, ss2),
   429         defset = Simplifier.merge_ss (ds1, ds2)}
   430       (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
   431       (Thm.merge_thms (extinjects1, extinjects2))
   432       (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
   433       (Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
   434           Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
   435           Thm.eq_thm (c, y) andalso Thm.eq_thm (d, z)) (splits1, splits2))
   436       (Symtab.merge (K true) (extfields1, extfields2))
   437       (Symtab.merge (K true) (fieldext1, fieldext2));
   438 );
   439 
   440 
   441 (* access 'records' *)
   442 
   443 val get_info = Symtab.lookup o #records o Data.get;
   444 
   445 fun the_info thy name =
   446   (case get_info thy name of
   447     SOME info => info
   448   | NONE => error ("Unknown record type " ^ quote name));
   449 
   450 fun put_record name info =
   451   Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
   452     make_data (Symtab.update (name, info) records)
   453       sel_upd equalities extinjects extsplit splits extfields fieldext);
   454 
   455 
   456 (* access 'sel_upd' *)
   457 
   458 val get_sel_upd = #sel_upd o Data.get;
   459 
   460 val is_selector = Symtab.defined o #selectors o get_sel_upd;
   461 val get_updates = Symtab.lookup o #updates o get_sel_upd;
   462 fun get_ss_with_context getss thy = Simplifier.global_context thy (getss (get_sel_upd thy));
   463 
   464 val get_simpset = get_ss_with_context #simpset;
   465 val get_sel_upd_defs = get_ss_with_context #defset;
   466 
   467 fun get_update_details u thy =
   468   let val sel_upd = get_sel_upd thy in
   469     (case Symtab.lookup (#updates sel_upd) u of
   470       SOME s =>
   471         let val SOME (dep, ismore) = Symtab.lookup (#selectors sel_upd) s
   472         in SOME (s, dep, ismore) end
   473     | NONE => NONE)
   474   end;
   475 
   476 fun put_sel_upd names more depth simps defs thy =
   477   let
   478     val all = names @ [more];
   479     val sels = map (rpair (depth, false)) names @ [(more, (depth, true))];
   480     val upds = map (suffix updateN) all ~~ all;
   481 
   482     val {records, sel_upd = {selectors, updates, simpset, defset},
   483       equalities, extinjects, extsplit, splits, extfields, fieldext} = Data.get thy;
   484     val data =
   485       make_data records
   486         {selectors = fold Symtab.update_new sels selectors,
   487           updates = fold Symtab.update_new upds updates,
   488           simpset = simpset addsimps simps,
   489           defset = defset addsimps defs}
   490          equalities extinjects extsplit splits extfields fieldext;
   491   in Data.put data thy end;
   492 
   493 
   494 (* access 'equalities' *)
   495 
   496 fun add_equalities name thm =
   497   Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
   498     make_data records sel_upd
   499       (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext);
   500 
   501 val get_equalities = Symtab.lookup o #equalities o Data.get;
   502 
   503 
   504 (* access 'extinjects' *)
   505 
   506 fun add_extinjects thm =
   507   Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
   508     make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
   509       extsplit splits extfields fieldext);
   510 
   511 val get_extinjects = rev o #extinjects o Data.get;
   512 
   513 
   514 (* access 'extsplit' *)
   515 
   516 fun add_extsplit name thm =
   517   Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
   518     make_data records sel_upd equalities extinjects
   519       (Symtab.update_new (name, thm) extsplit) splits extfields fieldext);
   520 
   521 
   522 (* access 'splits' *)
   523 
   524 fun add_splits name thmP =
   525   Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
   526     make_data records sel_upd equalities extinjects extsplit
   527       (Symtab.update_new (name, thmP) splits) extfields fieldext);
   528 
   529 val get_splits = Symtab.lookup o #splits o Data.get;
   530 
   531 
   532 (* parent/extension of named record *)
   533 
   534 val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o Data.get);
   535 val get_extension = Option.map #extension oo (Symtab.lookup o #records o Data.get);
   536 
   537 
   538 (* access 'extfields' *)
   539 
   540 fun add_extfields name fields =
   541   Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
   542     make_data records sel_upd equalities extinjects extsplit splits
   543       (Symtab.update_new (name, fields) extfields) fieldext);
   544 
   545 val get_extfields = Symtab.lookup o #extfields o Data.get;
   546 
   547 fun get_extT_fields thy T =
   548   let
   549     val ((name, Ts), moreT) = dest_recT T;
   550     val recname =
   551       let val (nm :: _ :: rst) = rev (Long_Name.explode name)   (* FIXME !? *)
   552       in Long_Name.implode (rev (nm :: rst)) end;
   553     val varifyT = varifyT (maxidx_of_typs (moreT :: Ts) + 1);
   554     val {records, extfields, ...} = Data.get thy;
   555     val (fields, (more, _)) = split_last (Symtab.lookup_list extfields name);
   556     val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
   557 
   558     val subst = fold (Sign.typ_match thy) (#1 (split_last args) ~~ #1 (split_last Ts)) Vartab.empty;
   559     val fields' = map (apsnd (Envir.norm_type subst o varifyT)) fields;
   560   in (fields', (more, moreT)) end;
   561 
   562 fun get_recT_fields thy T =
   563   let
   564     val (root_fields, (root_more, root_moreT)) = get_extT_fields thy T;
   565     val (rest_fields, rest_more) =
   566       if is_recT root_moreT then get_recT_fields thy root_moreT
   567       else ([], (root_more, root_moreT));
   568   in (root_fields @ rest_fields, rest_more) end;
   569 
   570 
   571 (* access 'fieldext' *)
   572 
   573 fun add_fieldext extname_types fields =
   574   Data.map (fn {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =>
   575     let
   576       val fieldext' =
   577         fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
   578     in make_data records sel_upd equalities extinjects extsplit splits extfields fieldext' end);
   579 
   580 val get_fieldext = Symtab.lookup o #fieldext o Data.get;
   581 
   582 
   583 (* parent records *)
   584 
   585 local
   586 
   587 fun add_parents _ NONE = I
   588   | add_parents thy (SOME (types, name)) =
   589       let
   590         fun err msg = error (msg ^ " parent record " ^ quote name);
   591 
   592         val {args, parent, ...} =
   593           (case get_info thy name of SOME info => info | NONE => err "Unknown");
   594         val _ = if length types <> length args then err "Bad number of arguments for" else ();
   595 
   596         fun bad_inst ((x, S), T) =
   597           if Sign.of_sort thy (T, S) then NONE else SOME x
   598         val bads = map_filter bad_inst (args ~~ types);
   599         val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");
   600 
   601         val inst = args ~~ types;
   602         val subst = Term.map_type_tfree (the o AList.lookup (op =) inst);
   603         val parent' = Option.map (apfst (map subst)) parent;
   604       in cons (name, inst) #> add_parents thy parent' end;
   605 
   606 in
   607 
   608 fun get_hierarchy thy (name, types) = add_parents thy (SOME (types, name)) [];
   609 
   610 fun get_parent_info thy parent =
   611   add_parents thy parent [] |> map (fn (name, inst) =>
   612     let
   613       val subst = Term.map_type_tfree (the o AList.lookup (op =) inst);
   614       val {fields, extension, induct_scheme, ext_def, ...} = the_info thy name;
   615       val fields' = map (apsnd subst) fields;
   616       val extension' = apsnd (map subst) extension;
   617     in make_parent_info name fields' extension' ext_def induct_scheme end);
   618 
   619 end;
   620 
   621 
   622 
   623 (** concrete syntax for records **)
   624 
   625 (* parse translations *)
   626 
   627 local
   628 
   629 fun split_args (field :: fields) ((name, arg) :: fargs) =
   630       if can (unsuffix name) field then
   631         let val (args, rest) = split_args fields fargs
   632         in (arg :: args, rest) end
   633       else raise Fail ("expecting field " ^ quote field ^ " but got " ^ quote name)
   634   | split_args [] (fargs as (_ :: _)) = ([], fargs)
   635   | split_args (_ :: _) [] = raise Fail "expecting more fields"
   636   | split_args _ _ = ([], []);
   637 
   638 fun field_type_tr ((Const (@{syntax_const "_field_type"}, _) $ Const (name, _) $ arg)) =
   639       (name, arg)
   640   | field_type_tr t = raise TERM ("field_type_tr", [t]);
   641 
   642 fun field_types_tr (Const (@{syntax_const "_field_types"}, _) $ t $ u) =
   643       field_type_tr t :: field_types_tr u
   644   | field_types_tr t = [field_type_tr t];
   645 
   646 fun record_field_types_tr more ctxt t =
   647   let
   648     val thy = Proof_Context.theory_of ctxt;
   649     fun err msg = raise TERM ("Error in record-type input: " ^ msg, [t]);
   650 
   651     fun mk_ext (fargs as (name, _) :: _) =
   652           (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
   653             SOME (ext, alphas) =>
   654               (case get_extfields thy ext of
   655                 SOME fields =>
   656                   let
   657                     val (fields', _) = split_last fields;
   658                     val types = map snd fields';
   659                     val (args, rest) = split_args (map fst fields') fargs
   660                       handle Fail msg => err msg;
   661                     val argtypes = Syntax.check_typs ctxt (map Syntax_Phases.decode_typ args);
   662                     val varifyT = varifyT (fold Term.maxidx_typ argtypes ~1 + 1);
   663                     val vartypes = map varifyT types;
   664 
   665                     val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
   666                       handle Type.TYPE_MATCH => err "type is no proper record (extension)";
   667                     val alphas' =
   668                       map (Syntax_Phases.term_of_typ ctxt o Envir.norm_type subst o varifyT)
   669                         (#1 (split_last alphas));
   670 
   671                     val more' = mk_ext rest;
   672                   in
   673                     list_comb
   674                       (Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
   675                   end
   676               | NONE => err ("no fields defined for " ^ quote ext))
   677           | NONE => err (quote name ^ " is no proper field"))
   678       | mk_ext [] = more;
   679   in
   680     mk_ext (field_types_tr t)
   681   end;
   682 
   683 fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const @{type_syntax unit}) ctxt t
   684   | record_type_tr _ ts = raise TERM ("record_type_tr", ts);
   685 
   686 fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t
   687   | record_type_scheme_tr _ ts = raise TERM ("record_type_scheme_tr", ts);
   688 
   689 
   690 fun field_tr ((Const (@{syntax_const "_field"}, _) $ Const (name, _) $ arg)) = (name, arg)
   691   | field_tr t = raise TERM ("field_tr", [t]);
   692 
   693 fun fields_tr (Const (@{syntax_const "_fields"}, _) $ t $ u) = field_tr t :: fields_tr u
   694   | fields_tr t = [field_tr t];
   695 
   696 fun record_fields_tr more ctxt t =
   697   let
   698     val thy = Proof_Context.theory_of ctxt;
   699     fun err msg = raise TERM ("Error in record input: " ^ msg, [t]);
   700 
   701     fun mk_ext (fargs as (name, _) :: _) =
   702           (case get_fieldext thy (Proof_Context.intern_const ctxt name) of
   703             SOME (ext, _) =>
   704               (case get_extfields thy ext of
   705                 SOME fields =>
   706                   let
   707                     val (args, rest) = split_args (map fst (fst (split_last fields))) fargs
   708                       handle Fail msg => err msg;
   709                     val more' = mk_ext rest;
   710                   in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end
   711               | NONE => err ("no fields defined for " ^ quote ext))
   712           | NONE => err (quote name ^ " is no proper field"))
   713       | mk_ext [] = more;
   714   in mk_ext (fields_tr t) end;
   715 
   716 fun record_tr ctxt [t] = record_fields_tr (Syntax.const @{const_syntax Unity}) ctxt t
   717   | record_tr _ ts = raise TERM ("record_tr", ts);
   718 
   719 fun record_scheme_tr ctxt [t, more] = record_fields_tr more ctxt t
   720   | record_scheme_tr _ ts = raise TERM ("record_scheme_tr", ts);
   721 
   722 
   723 fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) =
   724       Syntax.const (suffix updateN name) $ Abs (Name.uu_, dummyT, arg)
   725   | field_update_tr t = raise TERM ("field_update_tr", [t]);
   726 
   727 fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) =
   728       field_update_tr t :: field_updates_tr u
   729   | field_updates_tr t = [field_update_tr t];
   730 
   731 fun record_update_tr [t, u] = fold (curry op $) (field_updates_tr u) t
   732   | record_update_tr ts = raise TERM ("record_update_tr", ts);
   733 
   734 in
   735 
   736 val parse_translation =
   737  [(@{syntax_const "_record_update"}, record_update_tr)];
   738 
   739 val advanced_parse_translation =
   740  [(@{syntax_const "_record"}, record_tr),
   741   (@{syntax_const "_record_scheme"}, record_scheme_tr),
   742   (@{syntax_const "_record_type"}, record_type_tr),
   743   (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)];
   744 
   745 end;
   746 
   747 
   748 (* print translations *)
   749 
   750 val type_abbr = Attrib.setup_config_bool @{binding record_type_abbr} (K true);
   751 val type_as_fields = Attrib.setup_config_bool @{binding record_type_as_fields} (K true);
   752 
   753 
   754 local
   755 
   756 (* FIXME early extern (!??) *)
   757 (* FIXME Syntax.free (??) *)
   758 fun field_type_tr' (c, t) = Syntax.const @{syntax_const "_field_type"} $ Syntax.const c $ t;
   759 
   760 fun field_types_tr' (t, u) = Syntax.const @{syntax_const "_field_types"} $ t $ u;
   761 
   762 fun record_type_tr' ctxt t =
   763   let
   764     val thy = Proof_Context.theory_of ctxt;
   765 
   766     val T = Syntax_Phases.decode_typ t;
   767     val varifyT = varifyT (Term.maxidx_of_typ T + 1);
   768 
   769     fun strip_fields T =
   770       (case T of
   771         Type (ext, args as _ :: _) =>
   772           (case try (unsuffix ext_typeN) ext of
   773             SOME ext' =>
   774               (case get_extfields thy ext' of
   775                 SOME (fields as (x, _) :: _) =>
   776                   (case get_fieldext thy x of
   777                     SOME (_, alphas) =>
   778                      (let
   779                         val (f :: fs, _) = split_last fields;
   780                         val fields' =
   781                           apfst (Proof_Context.extern_const ctxt) f ::
   782                             map (apfst Long_Name.base_name) fs;
   783                         val (args', more) = split_last args;
   784                         val alphavars = map varifyT (#1 (split_last alphas));
   785                         val subst = Type.raw_matches (alphavars, args') Vartab.empty;
   786                         val fields'' = (map o apsnd) (Envir.norm_type subst o varifyT) fields';
   787                       in fields'' @ strip_fields more end
   788                       handle Type.TYPE_MATCH => [("", T)])
   789                   | _ => [("", T)])
   790               | _ => [("", T)])
   791           | _ => [("", T)])
   792       | _ => [("", T)]);
   793 
   794     val (fields, (_, moreT)) = split_last (strip_fields T);
   795     val _ = null fields andalso raise Match;
   796     val u =
   797       foldr1 field_types_tr'
   798         (map (field_type_tr' o apsnd (Syntax_Phases.term_of_typ ctxt)) fields);
   799   in
   800     if not (Config.get ctxt type_as_fields) orelse null fields then raise Match
   801     else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
   802     else
   803       Syntax.const @{syntax_const "_record_type_scheme"} $ u $
   804         Syntax_Phases.term_of_typ ctxt moreT
   805   end;
   806 
   807 (*try to reconstruct the record name type abbreviation from
   808   the (nested) extension types*)
   809 fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm =
   810   let
   811     val T = Syntax_Phases.decode_typ tm;
   812     val varifyT = varifyT (maxidx_of_typ T + 1);
   813 
   814     fun mk_type_abbr subst name args =
   815       let val abbrT = Type (name, map (varifyT o TFree) args)
   816       in Syntax_Phases.term_of_typ ctxt (Envir.norm_type subst abbrT) end;
   817 
   818     fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
   819   in
   820     if Config.get ctxt type_abbr then
   821       (case last_extT T of
   822         SOME (name, _) =>
   823           if name = last_ext then
   824             let val subst = match schemeT T in
   825               if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree zeta)))
   826               then mk_type_abbr subst abbr alphas
   827               else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
   828             end handle Type.TYPE_MATCH => record_type_tr' ctxt tm
   829           else raise Match (*give print translation of specialised record a chance*)
   830       | _ => raise Match)
   831     else record_type_tr' ctxt tm
   832   end;
   833 
   834 in
   835 
   836 fun record_ext_type_tr' name =
   837   let
   838     val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);
   839     fun tr' ctxt ts =
   840       record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts));
   841   in (ext_type_name, tr') end;
   842 
   843 fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
   844   let
   845     val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);
   846     fun tr' ctxt ts =
   847       record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt
   848         (list_comb (Syntax.const ext_type_name, ts));
   849   in (ext_type_name, tr') end;
   850 
   851 end;
   852 
   853 
   854 local
   855 
   856 (* FIXME Syntax.free (??) *)
   857 fun field_tr' (c, t) = Syntax.const @{syntax_const "_field"} $ Syntax.const c $ t;
   858 fun fields_tr' (t, u) = Syntax.const @{syntax_const "_fields"} $ t $ u;
   859 
   860 fun record_tr' ctxt t =
   861   let
   862     val thy = Proof_Context.theory_of ctxt;
   863 
   864     fun strip_fields t =
   865       (case strip_comb t of
   866         (Const (ext, _), args as (_ :: _)) =>
   867           (case try (Lexicon.unmark_const o unsuffix extN) ext of
   868             SOME ext' =>
   869               (case get_extfields thy ext' of
   870                 SOME fields =>
   871                  (let
   872                     val (f :: fs, _) = split_last (map fst fields);
   873                     val fields' = Proof_Context.extern_const ctxt f :: map Long_Name.base_name fs;
   874                     val (args', more) = split_last args;
   875                   in (fields' ~~ args') @ strip_fields more end
   876                   handle ListPair.UnequalLengths => [("", t)])
   877               | NONE => [("", t)])
   878           | NONE => [("", t)])
   879        | _ => [("", t)]);
   880 
   881     val (fields, (_, more)) = split_last (strip_fields t);
   882     val _ = null fields andalso raise Match;
   883     val u = foldr1 fields_tr' (map field_tr' fields);
   884   in
   885     (case more of
   886       Const (@{const_syntax Unity}, _) => Syntax.const @{syntax_const "_record"} $ u
   887     | _ => Syntax.const @{syntax_const "_record_scheme"} $ u $ more)
   888   end;
   889 
   890 in
   891 
   892 fun record_ext_tr' name =
   893   let
   894     val ext_name = Lexicon.mark_const (name ^ extN);
   895     fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));
   896   in (ext_name, tr') end;
   897 
   898 end;
   899 
   900 
   901 local
   902 
   903 fun dest_update ctxt c =
   904   (case try Lexicon.unmark_const c of
   905     SOME d => try (unsuffix updateN) (Proof_Context.extern_const ctxt d)
   906   | NONE => NONE);
   907 
   908 fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
   909       (case dest_update ctxt c of
   910         SOME name =>
   911           (case try Syntax_Trans.const_abs_tr' k of
   912             SOME t =>
   913               apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
   914                 (field_updates_tr' ctxt u)
   915           | NONE => ([], tm))
   916       | NONE => ([], tm))
   917   | field_updates_tr' _ tm = ([], tm);
   918 
   919 fun record_update_tr' ctxt tm =
   920   (case field_updates_tr' ctxt tm of
   921     ([], _) => raise Match
   922   | (ts, u) =>
   923       Syntax.const @{syntax_const "_record_update"} $ u $
   924         foldr1 (fn (v, w) => Syntax.const @{syntax_const "_field_updates"} $ v $ w) (rev ts));
   925 
   926 in
   927 
   928 fun field_update_tr' name =
   929   let
   930     val update_name = Lexicon.mark_const (name ^ updateN);
   931     fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u)
   932       | tr' _ _ = raise Match;
   933   in (update_name, tr') end;
   934 
   935 end;
   936 
   937 
   938 
   939 (** record simprocs **)
   940 
   941 fun is_sel_upd_pair thy (Const (s, _)) (Const (u, t')) =
   942   (case get_updates thy u of
   943     SOME u_name => u_name = s
   944   | NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));
   945 
   946 fun mk_comp_id f =
   947   let val T = range_type (fastype_of f)
   948   in HOLogic.mk_comp (Const (@{const_name Fun.id}, T --> T), f) end;
   949 
   950 fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
   951   | get_upd_funs _ = [];
   952 
   953 fun get_accupd_simps thy term defset =
   954   let
   955     val (acc, [body]) = strip_comb term;
   956     val upd_funs = sort_distinct Term_Ord.fast_term_ord (get_upd_funs body);
   957     fun get_simp upd =
   958       let
   959         (* FIXME fresh "f" (!?) *)
   960         val T = domain_type (fastype_of upd);
   961         val lhs = HOLogic.mk_comp (acc, upd $ Free ("f", T));
   962         val rhs =
   963           if is_sel_upd_pair thy acc upd
   964           then HOLogic.mk_comp (Free ("f", T), acc)
   965           else mk_comp_id acc;
   966         val prop = lhs === rhs;
   967         val othm =
   968           Goal.prove (Proof_Context.init_global thy) [] [] prop
   969             (fn _ =>
   970               simp_tac defset 1 THEN
   971               REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
   972               TRY (simp_tac (HOL_ss addsimps @{thms id_apply id_o o_id}) 1));
   973         val dest =
   974           if is_sel_upd_pair thy acc upd
   975           then @{thm o_eq_dest}
   976           else @{thm o_eq_id_dest};
   977       in Drule.export_without_context (othm RS dest) end;
   978   in map get_simp upd_funs end;
   979 
   980 fun get_updupd_simp thy defset u u' comp =
   981   let
   982     (* FIXME fresh "f" (!?) *)
   983     val f = Free ("f", domain_type (fastype_of u));
   984     val f' = Free ("f'", domain_type (fastype_of u'));
   985     val lhs = HOLogic.mk_comp (u $ f, u' $ f');
   986     val rhs =
   987       if comp
   988       then u $ HOLogic.mk_comp (f, f')
   989       else HOLogic.mk_comp (u' $ f', u $ f);
   990     val prop = lhs === rhs;
   991     val othm =
   992       Goal.prove (Proof_Context.init_global thy) [] [] prop
   993         (fn _ =>
   994           simp_tac defset 1 THEN
   995           REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
   996           TRY (simp_tac (HOL_ss addsimps @{thms id_apply}) 1));
   997     val dest = if comp then @{thm o_eq_dest_lhs} else @{thm o_eq_dest};
   998   in Drule.export_without_context (othm RS dest) end;
   999 
  1000 fun get_updupd_simps thy term defset =
  1001   let
  1002     val upd_funs = get_upd_funs term;
  1003     val cname = fst o dest_Const;
  1004     fun getswap u u' = get_updupd_simp thy defset u u' (cname u = cname u');
  1005     fun build_swaps_to_eq _ [] swaps = swaps
  1006       | build_swaps_to_eq upd (u :: us) swaps =
  1007           let
  1008             val key = (cname u, cname upd);
  1009             val newswaps =
  1010               if Symreltab.defined swaps key then swaps
  1011               else Symreltab.insert (K true) (key, getswap u upd) swaps;
  1012           in
  1013             if cname u = cname upd then newswaps
  1014             else build_swaps_to_eq upd us newswaps
  1015           end;
  1016     fun swaps_needed [] _ _ swaps = map snd (Symreltab.dest swaps)
  1017       | swaps_needed (u :: us) prev seen swaps =
  1018           if Symtab.defined seen (cname u)
  1019           then swaps_needed us prev seen (build_swaps_to_eq u prev swaps)
  1020           else swaps_needed us (u :: prev) (Symtab.insert (K true) (cname u, ()) seen) swaps;
  1021   in swaps_needed upd_funs [] Symtab.empty Symreltab.empty end;
  1022 
  1023 val named_cterm_instantiate = Iso_Tuple_Support.named_cterm_instantiate;
  1024 
  1025 fun prove_unfold_defs thy ex_simps ex_simprs prop =
  1026   let
  1027     val defset = get_sel_upd_defs thy;
  1028     val prop' = Envir.beta_eta_contract prop;
  1029     val (lhs, _) = Logic.dest_equals (Logic.strip_assums_concl prop');
  1030     val (_, args) = strip_comb lhs;
  1031     val simps = (if length args = 1 then get_accupd_simps else get_updupd_simps) thy lhs defset;
  1032   in
  1033     Goal.prove (Proof_Context.init_global thy) [] [] prop'
  1034       (fn _ =>
  1035         simp_tac (HOL_basic_ss addsimps (simps @ @{thms K_record_comp})) 1 THEN
  1036         TRY (simp_tac (HOL_basic_ss addsimps ex_simps addsimprocs ex_simprs) 1))
  1037   end;
  1038 
  1039 
  1040 local
  1041 
  1042 fun eq (s1: string) (s2: string) = (s1 = s2);
  1043 
  1044 fun has_field extfields f T =
  1045   exists (fn (eN, _) => exists (eq f o fst) (Symtab.lookup_list extfields eN)) (dest_recTs T);
  1046 
  1047 fun K_skeleton n (T as Type (_, [_, kT])) (b as Bound i) (Abs (x, xT, t)) =
  1048       if null (loose_bnos t) then ((n, kT), (Abs (x, xT, Bound (i + 1)))) else ((n, T), b)
  1049   | K_skeleton n T b _ = ((n, T), b);
  1050 
  1051 in
  1052 
  1053 (* simproc *)
  1054 
  1055 (*
  1056   Simplify selections of an record update:
  1057     (1)  S (S_update k r) = k (S r)
  1058     (2)  S (X_update k r) = S r
  1059 
  1060   The simproc skips multiple updates at once, eg:
  1061    S (X_update x (Y_update y (S_update k r))) = k (S r)
  1062 
  1063   But be careful in (2) because of the extensibility of records.
  1064   - If S is a more-selector we have to make sure that the update on component
  1065     X does not affect the selected subrecord.
  1066   - If X is a more-selector we have to make sure that S is not in the updated
  1067     subrecord.
  1068 *)
  1069 val simproc =
  1070   Simplifier.simproc_global @{theory HOL} "record_simp" ["x"]
  1071     (fn thy => fn _ => fn t =>
  1072       (case t of
  1073         (sel as Const (s, Type (_, [_, rangeS]))) $
  1074             ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
  1075           if is_selector thy s andalso is_some (get_updates thy u) then
  1076             let
  1077               val {sel_upd = {updates, ...}, extfields, ...} = Data.get thy;
  1078 
  1079               fun mk_eq_terms ((upd as Const (u, Type(_, [kT, _]))) $ k $ r) =
  1080                     (case Symtab.lookup updates u of
  1081                       NONE => NONE
  1082                     | SOME u_name =>
  1083                         if u_name = s then
  1084                           (case mk_eq_terms r of
  1085                             NONE =>
  1086                               let
  1087                                 val rv = ("r", rT);
  1088                                 val rb = Bound 0;
  1089                                 val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
  1090                               in SOME (upd $ kb $ rb, kb $ (sel $ rb), [kv, rv]) end
  1091                           | SOME (trm, trm', vars) =>
  1092                               let
  1093                                 val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k;
  1094                               in SOME (upd $ kb $ trm, kb $ trm', kv :: vars) end)
  1095                         else if has_field extfields u_name rangeS orelse
  1096                           has_field extfields s (domain_type kT) then NONE
  1097                         else
  1098                           (case mk_eq_terms r of
  1099                             SOME (trm, trm', vars) =>
  1100                               let val (kv, kb) = K_skeleton "k" kT (Bound (length vars)) k
  1101                               in SOME (upd $ kb $ trm, trm', kv :: vars) end
  1102                           | NONE =>
  1103                               let
  1104                                 val rv = ("r", rT);
  1105                                 val rb = Bound 0;
  1106                                 val (kv, kb) = K_skeleton "k" kT (Bound 1) k;
  1107                               in SOME (upd $ kb $ rb, sel $ rb, [kv, rv]) end))
  1108                 | mk_eq_terms _ = NONE;
  1109             in
  1110               (case mk_eq_terms (upd $ k $ r) of
  1111                 SOME (trm, trm', vars) =>
  1112                   SOME
  1113                     (prove_unfold_defs thy [] []
  1114                       (Logic.list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
  1115               | NONE => NONE)
  1116             end
  1117           else NONE
  1118       | _ => NONE));
  1119 
  1120 fun get_upd_acc_cong_thm upd acc thy simpset =
  1121   let
  1122     val insts = [("upd", cterm_of thy upd), ("ac", cterm_of thy acc)];
  1123     val prop = Thm.concl_of (named_cterm_instantiate insts updacc_cong_triv);
  1124   in
  1125     Goal.prove (Proof_Context.init_global thy) [] [] prop
  1126       (fn _ =>
  1127         simp_tac simpset 1 THEN
  1128         REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
  1129         TRY (resolve_tac [updacc_cong_idI] 1))
  1130   end;
  1131 
  1132 
  1133 (* upd_simproc *)
  1134 
  1135 (*Simplify multiple updates:
  1136     (1) "N_update y (M_update g (N_update x (M_update f r))) =
  1137           (N_update (y o x) (M_update (g o f) r))"
  1138     (2)  "r(|M:= M r|) = r"
  1139 
  1140   In both cases "more" updates complicate matters: for this reason
  1141   we omit considering further updates if doing so would introduce
  1142   both a more update and an update to a field within it.*)
  1143 val upd_simproc =
  1144   Simplifier.simproc_global @{theory HOL} "record_upd_simp" ["x"]
  1145     (fn thy => fn _ => fn t =>
  1146       let
  1147         (*We can use more-updators with other updators as long
  1148           as none of the other updators go deeper than any more
  1149           updator. min here is the depth of the deepest other
  1150           updator, max the depth of the shallowest more updator.*)
  1151         fun include_depth (dep, true) (min, max) =
  1152               if min <= dep
  1153               then SOME (min, if dep <= max orelse max = ~1 then dep else max)
  1154               else NONE
  1155           | include_depth (dep, false) (min, max) =
  1156               if dep <= max orelse max = ~1
  1157               then SOME (if min <= dep then dep else min, max)
  1158               else NONE;
  1159 
  1160         fun getupdseq (term as (upd as Const (u, _)) $ f $ tm) min max =
  1161               (case get_update_details u thy of
  1162                 SOME (s, dep, ismore) =>
  1163                   (case include_depth (dep, ismore) (min, max) of
  1164                     SOME (min', max') =>
  1165                       let val (us, bs, _) = getupdseq tm min' max'
  1166                       in ((upd, s, f) :: us, bs, fastype_of term) end
  1167                   | NONE => ([], term, HOLogic.unitT))
  1168               | NONE => ([], term, HOLogic.unitT))
  1169           | getupdseq term _ _ = ([], term, HOLogic.unitT);
  1170 
  1171         val (upds, base, baseT) = getupdseq t 0 ~1;
  1172 
  1173         fun is_upd_noop s (Abs (n, T, Const (s', T') $ tm')) tm =
  1174               if s = s' andalso null (loose_bnos tm')
  1175                 andalso subst_bound (HOLogic.unit, tm') = tm
  1176               then (true, Abs (n, T, Const (s', T') $ Bound 1))
  1177               else (false, HOLogic.unit)
  1178           | is_upd_noop _ _ _ = (false, HOLogic.unit);
  1179 
  1180         fun get_noop_simps (upd as Const _) (Abs (_, _, (acc as Const _) $ _)) =
  1181           let
  1182             val ss = get_sel_upd_defs thy;
  1183             val uathm = get_upd_acc_cong_thm upd acc thy ss;
  1184           in
  1185            [Drule.export_without_context (uathm RS updacc_noopE),
  1186             Drule.export_without_context (uathm RS updacc_noop_compE)]
  1187           end;
  1188 
  1189         (*If f is constant then (f o g) = f.  We know that K_skeleton
  1190           only returns constant abstractions thus when we see an
  1191           abstraction we can discard inner updates.*)
  1192         fun add_upd (f as Abs _) fs = [f]
  1193           | add_upd f fs = (f :: fs);
  1194 
  1195         (*mk_updterm returns
  1196           (orig-term-skeleton, simplified-skeleton,
  1197             variables, duplicate-updates, simp-flag, noop-simps)
  1198 
  1199           where duplicate-updates is a table used to pass upward
  1200           the list of update functions which can be composed
  1201           into an update above them, simp-flag indicates whether
  1202           any simplification was achieved, and noop-simps are
  1203           used for eliminating case (2) defined above*)
  1204         fun mk_updterm ((upd as Const (u, T), s, f) :: upds) above term =
  1205               let
  1206                 val (lhs, rhs, vars, dups, simp, noops) =
  1207                   mk_updterm upds (Symtab.update (u, ()) above) term;
  1208                 val (fvar, skelf) =
  1209                   K_skeleton (Long_Name.base_name s) (domain_type T) (Bound (length vars)) f;
  1210                 val (isnoop, skelf') = is_upd_noop s f term;
  1211                 val funT = domain_type T;
  1212                 fun mk_comp_local (f, f') =
  1213                   Const (@{const_name Fun.comp}, funT --> funT --> funT) $ f $ f';
  1214               in
  1215                 if isnoop then
  1216                   (upd $ skelf' $ lhs, rhs, vars,
  1217                     Symtab.update (u, []) dups, true,
  1218                     if Symtab.defined noops u then noops
  1219                     else Symtab.update (u, get_noop_simps upd skelf') noops)
  1220                 else if Symtab.defined above u then
  1221                   (upd $ skelf $ lhs, rhs, fvar :: vars,
  1222                     Symtab.map_default (u, []) (add_upd skelf) dups,
  1223                     true, noops)
  1224                 else
  1225                   (case Symtab.lookup dups u of
  1226                     SOME fs =>
  1227                      (upd $ skelf $ lhs,
  1228                       upd $ foldr1 mk_comp_local (add_upd skelf fs) $ rhs,
  1229                       fvar :: vars, dups, true, noops)
  1230                   | NONE => (upd $ skelf $ lhs, upd $ skelf $ rhs, fvar :: vars, dups, simp, noops))
  1231               end
  1232           | mk_updterm [] _ _ =
  1233               (Bound 0, Bound 0, [("r", baseT)], Symtab.empty, false, Symtab.empty)
  1234           | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _) => x) us);
  1235 
  1236         val (lhs, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
  1237         val noops' = maps snd (Symtab.dest noops);
  1238       in
  1239         if simp then
  1240           SOME
  1241             (prove_unfold_defs thy noops' [simproc]
  1242               (Logic.list_all (vars, Logic.mk_equals (lhs, rhs))))
  1243         else NONE
  1244       end);
  1245 
  1246 end;
  1247 
  1248 
  1249 (* eq_simproc *)
  1250 
  1251 (*Look up the most specific record-equality.
  1252 
  1253  Note on efficiency:
  1254  Testing equality of records boils down to the test of equality of all components.
  1255  Therefore the complexity is: #components * complexity for single component.
  1256  Especially if a record has a lot of components it may be better to split up
  1257  the record first and do simplification on that (split_simp_tac).
  1258  e.g. r(|lots of updates|) = x
  1259 
  1260              eq_simproc          split_simp_tac
  1261  Complexity: #components * #updates     #updates
  1262 *)
  1263 val eq_simproc =
  1264   Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
  1265     (fn thy => fn _ => fn t =>
  1266       (case t of Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ =>
  1267         (case rec_id ~1 T of
  1268           "" => NONE
  1269         | name =>
  1270             (case get_equalities thy name of
  1271               NONE => NONE
  1272             | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
  1273       | _ => NONE));
  1274 
  1275 
  1276 (* split_simproc *)
  1277 
  1278 (*Split quantified occurrences of records, for which P holds.  P can peek on the
  1279   subterm starting at the quantified occurrence of the record (including the quantifier):
  1280     P t = 0: do not split
  1281     P t = ~1: completely split
  1282     P t > 0: split up to given bound of record extensions.*)
  1283 fun split_simproc P =
  1284   Simplifier.simproc_global @{theory HOL} "record_split_simp" ["x"]
  1285     (fn thy => fn _ => fn t =>
  1286       (case t of
  1287         Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
  1288           if quantifier = @{const_name all} orelse
  1289             quantifier = @{const_name All} orelse
  1290             quantifier = @{const_name Ex}
  1291           then
  1292             (case rec_id ~1 T of
  1293               "" => NONE
  1294             | _ =>
  1295                 let val split = P t in
  1296                   if split <> 0 then
  1297                     (case get_splits thy (rec_id split T) of
  1298                       NONE => NONE
  1299                     | SOME (all_thm, All_thm, Ex_thm, _) =>
  1300                         SOME
  1301                           (case quantifier of
  1302                             @{const_name all} => all_thm
  1303                           | @{const_name All} => All_thm RS @{thm eq_reflection}
  1304                           | @{const_name Ex} => Ex_thm RS @{thm eq_reflection}
  1305                           | _ => raise Fail "split_simproc"))
  1306                   else NONE
  1307                 end)
  1308           else NONE
  1309       | _ => NONE));
  1310 
  1311 val ex_sel_eq_simproc =
  1312   Simplifier.simproc_global @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
  1313     (fn thy => fn ss => fn t =>
  1314       let
  1315         fun mkeq (lr, Teq, (sel, Tsel), x) i =
  1316           if is_selector thy sel then
  1317             let
  1318               val x' =
  1319                 if not (Term.is_dependent x)
  1320                 then Free ("x" ^ string_of_int i, range_type Tsel)
  1321                 else raise TERM ("", [x]);
  1322               val sel' = Const (sel, Tsel) $ Bound 0;
  1323               val (l, r) = if lr then (sel', x') else (x', sel');
  1324             in Const (@{const_name HOL.eq}, Teq) $ l $ r end
  1325           else raise TERM ("", [Const (sel, Tsel)]);
  1326 
  1327         fun dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
  1328               (true, Teq, (sel, Tsel), X)
  1329           | dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
  1330               (false, Teq, (sel, Tsel), X)
  1331           | dest_sel_eq _ = raise TERM ("", []);
  1332       in
  1333         (case t of
  1334           Const (@{const_name Ex}, Tex) $ Abs (s, T, t) =>
  1335            (let
  1336              val eq = mkeq (dest_sel_eq t) 0;
  1337              val prop =
  1338                Logic.list_all ([("r", T)],
  1339                  Logic.mk_equals
  1340                   (Const (@{const_name Ex}, Tex) $ Abs (s, T, eq), @{term True}));
  1341             in
  1342               SOME (Skip_Proof.prove_global thy [] [] prop
  1343                 (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
  1344                     addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))
  1345             end handle TERM _ => NONE)
  1346         | _ => NONE)
  1347       end);
  1348 
  1349 
  1350 (* split_simp_tac *)
  1351 
  1352 (*Split (and simplify) all records in the goal for which P holds.
  1353   For quantified occurrences of a record
  1354   P can peek on the whole subterm (including the quantifier); for free variables P
  1355   can only peek on the variable itself.
  1356   P t = 0: do not split
  1357   P t = ~1: completely split
  1358   P t > 0: split up to given bound of record extensions.*)
  1359 fun split_simp_tac thms P = CSUBGOAL (fn (cgoal, i) =>
  1360   let
  1361     val thy = Thm.theory_of_cterm cgoal;
  1362 
  1363     val goal = term_of cgoal;
  1364     val frees = filter (is_recT o #2) (Term.add_frees goal []);
  1365 
  1366     val has_rec = exists_Const
  1367       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
  1368           (s = @{const_name all} orelse s = @{const_name All} orelse s = @{const_name Ex}) andalso
  1369           is_recT T
  1370         | _ => false);
  1371 
  1372     fun mk_split_free_tac free induct_thm i =
  1373       let
  1374         val cfree = cterm_of thy free;
  1375         val _$ (_ $ r) = concl_of induct_thm;
  1376         val crec = cterm_of thy r;
  1377         val thm = cterm_instantiate [(crec, cfree)] induct_thm;
  1378       in
  1379         simp_tac (HOL_basic_ss addsimps @{thms induct_atomize}) i THEN
  1380         rtac thm i THEN
  1381         simp_tac (HOL_basic_ss addsimps @{thms induct_rulify}) i
  1382       end;
  1383 
  1384     val split_frees_tacs =
  1385       frees |> map_filter (fn (x, T) =>
  1386         (case rec_id ~1 T of
  1387           "" => NONE
  1388         | _ =>
  1389             let
  1390               val free = Free (x, T);
  1391               val split = P free;
  1392             in
  1393               if split <> 0 then
  1394                 (case get_splits thy (rec_id split T) of
  1395                   NONE => NONE
  1396                 | SOME (_, _, _, induct_thm) =>
  1397                     SOME (mk_split_free_tac free induct_thm i))
  1398               else NONE
  1399             end));
  1400 
  1401     val simprocs = if has_rec goal then [split_simproc P] else [];
  1402     val thms' = @{thms o_apply K_record_comp} @ thms;
  1403   in
  1404     EVERY split_frees_tacs THEN
  1405     full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i
  1406   end);
  1407 
  1408 
  1409 (* split_tac *)
  1410 
  1411 (*Split all records in the goal, which are quantified by !! or ALL.*)
  1412 val split_tac = CSUBGOAL (fn (cgoal, i) =>
  1413   let
  1414     val goal = term_of cgoal;
  1415 
  1416     val has_rec = exists_Const
  1417       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
  1418           (s = @{const_name all} orelse s = @{const_name All}) andalso is_recT T
  1419         | _ => false);
  1420 
  1421     fun is_all (Const (@{const_name all}, _) $ _) = ~1
  1422       | is_all (Const (@{const_name All}, _) $ _) = ~1
  1423       | is_all _ = 0;
  1424   in
  1425     if has_rec goal then
  1426       full_simp_tac (HOL_basic_ss addsimprocs [split_simproc is_all]) i
  1427     else no_tac
  1428   end);
  1429 
  1430 
  1431 (* wrapper *)
  1432 
  1433 val split_name = "record_split_tac";
  1434 val split_wrapper = (split_name, fn _ => fn tac => split_tac ORELSE' tac);
  1435 
  1436 
  1437 
  1438 (** theory extender interface **)
  1439 
  1440 (* attributes *)
  1441 
  1442 fun case_names_fields x = Rule_Cases.case_names ["fields"] x;
  1443 fun induct_type_global name = [case_names_fields, Induct.induct_type name];
  1444 fun cases_type_global name = [case_names_fields, Induct.cases_type name];
  1445 
  1446 
  1447 (* tactics *)
  1448 
  1449 (*Do case analysis / induction according to rule on last parameter of ith subgoal
  1450   (or on s if there are no parameters).
  1451   Instatiation of record variable (and predicate) in rule is calculated to
  1452   avoid problems with higher order unification.*)
  1453 fun try_param_tac s rule = CSUBGOAL (fn (cgoal, i) =>
  1454   let
  1455     val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
  1456 
  1457     val g = Thm.term_of cgoal;
  1458     val params = Logic.strip_params g;
  1459     val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
  1460     val rule' = Thm.lift_rule cgoal rule;
  1461     val (P, ys) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_assums_concl (prop_of rule')));
  1462     (*ca indicates if rule is a case analysis or induction rule*)
  1463     val (x, ca) =
  1464       (case rev (drop (length params) ys) of
  1465         [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
  1466           (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
  1467       | [x] => (head_of x, false));
  1468     val rule'' =
  1469       cterm_instantiate
  1470         (map (pairself cert)
  1471           (case rev params of
  1472             [] =>
  1473               (case AList.lookup (op =) (Term.add_frees g []) s of
  1474                 NONE => error "try_param_tac: no such variable"
  1475               | SOME T => [(P, if ca then concl else lambda (Free (s, T)) concl), (x, Free (s, T))])
  1476           | (_, T) :: _ =>
  1477               [(P, fold_rev Term.abs params (if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
  1478                 (x, fold_rev Term.abs params (Bound 0))])) rule';
  1479   in compose_tac (false, rule'', nprems_of rule) i end);
  1480 
  1481 
  1482 fun extension_definition name fields alphas zeta moreT more vars thy =
  1483   let
  1484     val ctxt = Proof_Context.init_global thy;
  1485 
  1486     val base_name = Long_Name.base_name name;
  1487 
  1488     val fieldTs = map snd fields;
  1489     val fields_moreTs = fieldTs @ [moreT];
  1490 
  1491     val alphas_zeta = alphas @ [zeta];
  1492 
  1493     val ext_binding = Binding.name (suffix extN base_name);
  1494     val ext_name = suffix extN name;
  1495     val ext_tyco = suffix ext_typeN name
  1496     val extT = Type (ext_tyco, map TFree alphas_zeta);
  1497     val ext_type = fields_moreTs ---> extT;
  1498 
  1499 
  1500     (* the tree of new types that will back the record extension *)
  1501 
  1502     val mktreeV = Balanced_Tree.make Iso_Tuple_Support.mk_cons_tuple;
  1503 
  1504     fun mk_iso_tuple (left, right) (thy, i) =
  1505       let
  1506         val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
  1507         val ((_, cons), thy') = thy
  1508           |> Iso_Tuple_Support.add_iso_tuple_type
  1509             (Binding.suffix_name suff (Binding.name base_name), alphas_zeta)
  1510               (fastype_of left, fastype_of right);
  1511       in
  1512         (cons $ left $ right, (thy', i + 1))
  1513       end;
  1514 
  1515     (*trying to create a 1-element iso_tuple will fail, and is pointless anyway*)
  1516     fun mk_even_iso_tuple [arg] = pair arg
  1517       | mk_even_iso_tuple args = mk_iso_tuple (Iso_Tuple_Support.dest_cons_tuple (mktreeV args));
  1518 
  1519     fun build_meta_tree_type i thy vars more =
  1520       let val len = length vars in
  1521         if len < 1 then raise TYPE ("meta_tree_type args too short", [], vars)
  1522         else if len > 16 then
  1523           let
  1524             fun group16 [] = []
  1525               | group16 xs = take 16 xs :: group16 (drop 16 xs);
  1526             val vars' = group16 vars;
  1527             val (composites, (thy', i')) = fold_map mk_even_iso_tuple vars' (thy, i);
  1528           in
  1529             build_meta_tree_type i' thy' composites more
  1530           end
  1531         else
  1532           let val (term, (thy', _)) = mk_iso_tuple (mktreeV vars, more) (thy, 0)
  1533           in (term, thy') end
  1534       end;
  1535 
  1536     val _ = timing_msg ctxt "record extension preparing definitions";
  1537 
  1538 
  1539     (* 1st stage part 1: introduce the tree of new types *)
  1540 
  1541     val (ext_body, typ_thy) = timeit_msg ctxt "record extension nested type def:" (fn () =>
  1542       build_meta_tree_type 1 thy vars more);
  1543 
  1544 
  1545     (* prepare declarations and definitions *)
  1546 
  1547     (* 1st stage part 2: define the ext constant *)
  1548 
  1549     fun mk_ext args = list_comb (Const (ext_name, ext_type), args);
  1550     val ext_spec = Logic.mk_equals (mk_ext (vars @ [more]), ext_body);
  1551 
  1552     val ([ext_def], defs_thy) = timeit_msg ctxt "record extension constructor def:" (fn () =>
  1553       typ_thy
  1554       |> Sign.declare_const_global ((ext_binding, ext_type), NoSyn) |> snd
  1555       |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]
  1556       ||> Theory.checkpoint);
  1557 
  1558 
  1559     (* prepare propositions *)
  1560 
  1561     val _ = timing_msg ctxt "record extension preparing propositions";
  1562     val vars_more = vars @ [more];
  1563     val variants = map (fn Free (x, _) => x) vars_more;
  1564     val ext = mk_ext vars_more;
  1565     val s = Free (rN, extT);
  1566     val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT);
  1567 
  1568     val inject_prop =  (* FIXME local x x' *)
  1569       let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in
  1570         HOLogic.mk_conj (HOLogic.eq_const extT $
  1571           mk_ext vars_more $ mk_ext vars_more', @{term True})
  1572         ===
  1573         foldr1 HOLogic.mk_conj
  1574           (map HOLogic.mk_eq (vars_more ~~ vars_more') @ [@{term True}])
  1575       end;
  1576 
  1577     val induct_prop = (fold_rev Logic.all vars_more (Trueprop (P $ ext)), Trueprop (P $ s));
  1578 
  1579     val split_meta_prop =  (* FIXME local P *)
  1580       let val P = Free (singleton (Name.variant_list variants) "P", extT --> propT)
  1581       in Logic.mk_equals (Logic.all s (P $ s), fold_rev Logic.all vars_more (P $ ext)) end;
  1582 
  1583     val inject = timeit_msg ctxt "record extension inject proof:" (fn () =>
  1584       simplify HOL_ss
  1585         (Skip_Proof.prove_global defs_thy [] [] inject_prop
  1586           (fn _ =>
  1587             simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
  1588             REPEAT_DETERM
  1589               (rtac @{thm refl_conj_eq} 1 ORELSE
  1590                 Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
  1591                 rtac refl 1))));
  1592 
  1593 
  1594     (*We need a surjection property r = (| f = f r, g = g r ... |)
  1595       to prove other theorems. We haven't given names to the accessors
  1596       f, g etc yet however, so we generate an ext structure with
  1597       free variables as all arguments and allow the introduction tactic to
  1598       operate on it as far as it can. We then use Drule.export_without_context
  1599       to convert the free variables into unifiable variables and unify them with
  1600       (roughly) the definition of the accessor.*)
  1601     val surject = timeit_msg ctxt "record extension surjective proof:" (fn () =>
  1602       let
  1603         val cterm_ext = cterm_of defs_thy ext;
  1604         val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
  1605         val tactic1 =
  1606           simp_tac (HOL_basic_ss addsimps [ext_def]) 1 THEN
  1607           REPEAT_ALL_NEW Iso_Tuple_Support.iso_tuple_intros_tac 1;
  1608         val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
  1609         val [halfway] = Seq.list_of (tactic1 start);
  1610         val [surject] = Seq.list_of (tactic2 (Drule.export_without_context halfway));
  1611       in
  1612         surject
  1613       end);
  1614 
  1615     val split_meta = timeit_msg ctxt "record extension split_meta proof:" (fn () =>
  1616       Skip_Proof.prove_global defs_thy [] [] split_meta_prop
  1617         (fn _ =>
  1618           EVERY1
  1619            [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
  1620             etac @{thm meta_allE}, atac,
  1621             rtac (@{thm prop_subst} OF [surject]),
  1622             REPEAT o etac @{thm meta_allE}, atac]));
  1623 
  1624     val induct = timeit_msg ctxt "record extension induct proof:" (fn () =>
  1625       let val (assm, concl) = induct_prop in
  1626         Skip_Proof.prove_global defs_thy [] [assm] concl
  1627           (fn {prems, ...} =>
  1628             cut_tac (split_meta RS Drule.equal_elim_rule2) 1 THEN
  1629             resolve_tac prems 2 THEN
  1630             asm_simp_tac HOL_ss 1)
  1631       end);
  1632 
  1633     val ([(_, [induct']), (_, [inject']), (_, [surjective']), (_, [split_meta'])], thm_thy) =
  1634       defs_thy
  1635       |> Global_Theory.note_thmss ""
  1636           [((Binding.name "ext_induct", []), [([induct], [])]),
  1637            ((Binding.name "ext_inject", []), [([inject], [])]),
  1638            ((Binding.name "ext_surjective", []), [([surject], [])]),
  1639            ((Binding.name "ext_split", []), [([split_meta], [])])];
  1640   in
  1641     (((ext_name, ext_type), (ext_tyco, alphas_zeta),
  1642       extT, induct', inject', surjective', split_meta', ext_def), thm_thy)
  1643   end;
  1644 
  1645 fun chunks [] [] = []
  1646   | chunks [] xs = [xs]
  1647   | chunks (l :: ls) xs = take l xs :: chunks ls (drop l xs);
  1648 
  1649 fun chop_last [] = error "chop_last: list should not be empty"
  1650   | chop_last [x] = ([], x)
  1651   | chop_last (x :: xs) = let val (tl, l) = chop_last xs in (x :: tl, l) end;
  1652 
  1653 fun subst_last _ [] = error "subst_last: list should not be empty"
  1654   | subst_last s [_] = [s]
  1655   | subst_last s (x :: xs) = x :: subst_last s xs;
  1656 
  1657 
  1658 (* mk_recordT *)
  1659 
  1660 (*build up the record type from the current extension tpye extT and a list
  1661   of parent extensions, starting with the root of the record hierarchy*)
  1662 fun mk_recordT extT =
  1663   fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT;
  1664 
  1665 
  1666 (* code generation *)
  1667 
  1668 fun mk_random_eq tyco vs extN Ts =
  1669   let
  1670     (* FIXME local i etc. *)
  1671     val size = @{term "i::code_numeral"};
  1672     fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
  1673     val T = Type (tyco, map TFree vs);
  1674     val Tm = termifyT T;
  1675     val params = Name.invent_names Name.context "x" Ts;
  1676     val lhs = HOLogic.mk_random T size;
  1677     val tc = HOLogic.mk_return Tm @{typ Random.seed}
  1678       (HOLogic.mk_valtermify_app extN params T);
  1679     val rhs =
  1680       HOLogic.mk_ST
  1681         (map (fn (v, T') =>
  1682           ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params)
  1683         tc @{typ Random.seed} (SOME Tm, @{typ Random.seed});
  1684   in
  1685     (lhs, rhs)
  1686   end
  1687 
  1688 fun mk_full_exhaustive_eq tyco vs extN Ts =
  1689   let
  1690     (* FIXME local i etc. *)
  1691     val size = @{term "i::code_numeral"};
  1692     fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"});
  1693     val T = Type (tyco, map TFree vs);
  1694     val test_function = Free ("f", termifyT T --> @{typ "(bool * term list) option"});
  1695     val params = Name.invent_names Name.context "x" Ts;
  1696     fun full_exhaustiveT T =
  1697       (termifyT T --> @{typ "(bool * Code_Evaluation.term list) option"}) -->
  1698         @{typ code_numeral} --> @{typ "(bool * Code_Evaluation.term list) option"};
  1699     fun mk_full_exhaustive T =
  1700       Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
  1701         full_exhaustiveT T);
  1702     val lhs = mk_full_exhaustive T $ test_function $ size;
  1703     val tc = test_function $ (HOLogic.mk_valtermify_app extN params T);
  1704     val rhs = fold_rev (fn (v, T) => fn cont =>
  1705         mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc;
  1706   in
  1707     (lhs, rhs)
  1708   end;
  1709 
  1710 fun instantiate_sort_record (sort, mk_eq) tyco vs extN Ts thy =
  1711   let
  1712     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_eq tyco vs extN Ts));
  1713   in
  1714     thy
  1715     |> Class.instantiation ([tyco], vs, sort)
  1716     |> `(fn lthy => Syntax.check_term lthy eq)
  1717     |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
  1718     |> snd
  1719     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
  1720   end;
  1721 
  1722 fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy =
  1723   let
  1724     val algebra = Sign.classes_of thy;
  1725     val has_inst = Sorts.has_instance algebra ext_tyco sort;
  1726   in
  1727     if has_inst then thy
  1728     else
  1729       (case Quickcheck_Common.perhaps_constrain thy (map (rpair sort) Ts) vs of
  1730         SOME constrain =>
  1731           instantiate_sort_record (sort, mk_eq) ext_tyco (map constrain vs) extN
  1732             ((map o map_atyps) (fn TFree v => TFree (constrain v)) Ts) thy
  1733       | NONE => thy)
  1734   end;
  1735 
  1736 fun add_code ext_tyco vs extT ext simps inject thy =
  1737   if Config.get_global thy codegen then
  1738     let
  1739       val eq =
  1740         HOLogic.mk_Trueprop (HOLogic.mk_eq
  1741           (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
  1742            Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT)));
  1743       fun tac eq_def =
  1744         Class.intro_classes_tac []
  1745         THEN rewrite_goals_tac [Simpdata.mk_eq eq_def]
  1746         THEN ALLGOALS (rtac @{thm refl});
  1747       fun mk_eq thy eq_def =
  1748         Simplifier.rewrite_rule
  1749           [AxClass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
  1750       fun mk_eq_refl thy =
  1751         @{thm equal_refl}
  1752         |> Thm.instantiate
  1753           ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
  1754         |> AxClass.unoverload thy;
  1755       val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
  1756       val ensure_exhaustive_record =
  1757         ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
  1758     in
  1759       thy
  1760       |> Code.add_datatype [ext]
  1761       |> fold Code.add_default_eqn simps
  1762       |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
  1763       |> `(fn lthy => Syntax.check_term lthy eq)
  1764       |-> (fn eq => Specification.definition
  1765             (NONE, (Attrib.empty_binding, eq)))
  1766       |-> (fn (_, (_, eq_def)) =>
  1767          Class.prove_instantiation_exit_result Morphism.thm
  1768             (fn _ => fn eq_def => tac eq_def) eq_def)
  1769       |-> (fn eq_def => fn thy =>
  1770             thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
  1771       |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
  1772       |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
  1773       |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
  1774     end
  1775   else thy;
  1776 
  1777 
  1778 (* definition *)
  1779 
  1780 fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
  1781   let
  1782     val ctxt = Proof_Context.init_global thy;
  1783 
  1784     val prefix = Binding.name_of binding;
  1785     val name = Sign.full_name thy binding;
  1786     val full = Sign.full_name_path thy prefix;
  1787 
  1788     val bfields = map (fn (x, T, _) => (x, T)) raw_fields;
  1789     val field_syntax = map #3 raw_fields;
  1790 
  1791     val parent_fields = maps #fields parents;
  1792     val parent_chunks = map (length o #fields) parents;
  1793     val parent_names = map fst parent_fields;
  1794     val parent_types = map snd parent_fields;
  1795     val parent_fields_len = length parent_fields;
  1796     val parent_variants =
  1797       Name.variant_list [moreN, rN, rN ^ "'", wN] (map Long_Name.base_name parent_names);
  1798     val parent_vars = map2 (curry Free) parent_variants parent_types;
  1799     val parent_len = length parents;
  1800 
  1801     val fields = map (apfst full) bfields;
  1802     val names = map fst fields;
  1803     val types = map snd fields;
  1804     val alphas_fields = fold Term.add_tfreesT types [];
  1805     val alphas_ext = inter (op =) alphas_fields alphas;
  1806     val len = length fields;
  1807     val variants =
  1808       Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
  1809         (map (Binding.name_of o fst) bfields);
  1810     val vars = map2 (curry Free) variants types;
  1811     val named_vars = names ~~ vars;
  1812     val idxms = 0 upto len;
  1813 
  1814     val all_fields = parent_fields @ fields;
  1815     val all_types = parent_types @ types;
  1816     val all_variants = parent_variants @ variants;
  1817     val all_vars = parent_vars @ vars;
  1818     val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
  1819 
  1820     val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", HOLogic.typeS);
  1821     val moreT = TFree zeta;
  1822     val more = Free (moreN, moreT);
  1823     val full_moreN = full (Binding.name moreN);
  1824     val bfields_more = bfields @ [(Binding.name moreN, moreT)];
  1825     val fields_more = fields @ [(full_moreN, moreT)];
  1826     val named_vars_more = named_vars @ [(full_moreN, more)];
  1827     val all_vars_more = all_vars @ [more];
  1828     val all_named_vars_more = all_named_vars @ [(full_moreN, more)];
  1829 
  1830 
  1831     (* 1st stage: ext_thy *)
  1832 
  1833     val extension_name = full binding;
  1834 
  1835     val ((ext, (ext_tyco, vs),
  1836         extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
  1837       thy
  1838       |> Sign.qualified_path false binding
  1839       |> extension_definition extension_name fields alphas_ext zeta moreT more vars;
  1840 
  1841     val _ = timing_msg ctxt "record preparing definitions";
  1842     val Type extension_scheme = extT;
  1843     val extension_name = unsuffix ext_typeN (fst extension_scheme);
  1844     val extension = let val (n, Ts) = extension_scheme in (n, subst_last HOLogic.unitT Ts) end;
  1845     val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extension_name];
  1846     val extension_id = implode extension_names;
  1847 
  1848     fun rec_schemeT n = mk_recordT (map #extension (drop n parents)) extT;
  1849     val rec_schemeT0 = rec_schemeT 0;
  1850 
  1851     fun recT n =
  1852       let val (c, Ts) = extension in
  1853         mk_recordT (map #extension (drop n parents))
  1854           (Type (c, subst_last HOLogic.unitT Ts))
  1855       end;
  1856     val recT0 = recT 0;
  1857 
  1858     fun mk_rec args n =
  1859       let
  1860         val (args', more) = chop_last args;
  1861         fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]);
  1862         fun build Ts =
  1863           fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args')) more;
  1864       in
  1865         if more = HOLogic.unit
  1866         then build (map_range recT (parent_len + 1))
  1867         else build (map_range rec_schemeT (parent_len + 1))
  1868       end;
  1869 
  1870     val r_rec0 = mk_rec all_vars_more 0;
  1871     val r_rec_unit0 = mk_rec (all_vars @ [HOLogic.unit]) 0;
  1872 
  1873     fun r n = Free (rN, rec_schemeT n);
  1874     val r0 = r 0;
  1875     fun r_unit n = Free (rN, recT n);
  1876     val r_unit0 = r_unit 0;
  1877     val w = Free (wN, rec_schemeT 0);
  1878 
  1879 
  1880     (* print translations *)
  1881 
  1882     val record_ext_type_abbr_tr's =
  1883       let
  1884         val trname = hd extension_names;
  1885         val last_ext = unsuffix ext_typeN (fst extension);
  1886       in [record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0 trname] end;
  1887 
  1888     val record_ext_type_tr's =
  1889       let
  1890         (*avoid conflict with record_type_abbr_tr's*)
  1891         val trnames = if parent_len > 0 then [extension_name] else [];
  1892       in map record_ext_type_tr' trnames end;
  1893 
  1894     val advanced_print_translation =
  1895       map field_update_tr' (full_moreN :: names) @ [record_ext_tr' extension_name] @
  1896       record_ext_type_tr's @ record_ext_type_abbr_tr's;
  1897 
  1898 
  1899     (* prepare declarations *)
  1900 
  1901     val sel_decls = map (mk_selC rec_schemeT0 o apfst Binding.name_of) bfields_more;
  1902     val upd_decls = map (mk_updC updateN rec_schemeT0 o apfst Binding.name_of) bfields_more;
  1903     val make_decl = (makeN, all_types ---> recT0);
  1904     val fields_decl = (fields_selN, types ---> Type extension);
  1905     val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0);
  1906     val truncate_decl = (truncateN, rec_schemeT0 --> recT0);
  1907 
  1908 
  1909     (* prepare definitions *)
  1910 
  1911     val ext_defs = ext_def :: map #ext_def parents;
  1912 
  1913     (*Theorems from the iso_tuple intros.
  1914       By unfolding ext_defs from r_rec0 we create a tree of constructor
  1915       calls (many of them Pair, but others as well). The introduction
  1916       rules for update_accessor_eq_assist can unify two different ways
  1917       on these constructors. If we take the complete result sequence of
  1918       running a the introduction tactic, we get one theorem for each upd/acc
  1919       pair, from which we can derive the bodies of our selector and
  1920       updator and their convs.*)
  1921     val (accessor_thms, updator_thms, upd_acc_cong_assists) =
  1922       timeit_msg ctxt "record getting tree access/updates:" (fn () =>
  1923         let
  1924           val r_rec0_Vars =
  1925             let
  1926               (*pick variable indices of 1 to avoid possible variable
  1927                 collisions with existing variables in updacc_eq_triv*)
  1928               fun to_Var (Free (c, T)) = Var ((c, 1), T);
  1929             in mk_rec (map to_Var all_vars_more) 0 end;
  1930 
  1931           val cterm_rec = cterm_of ext_thy r_rec0;
  1932           val cterm_vrs = cterm_of ext_thy r_rec0_Vars;
  1933           val insts = [("v", cterm_rec), ("v'", cterm_vrs)];
  1934           val init_thm = named_cterm_instantiate insts updacc_eq_triv;
  1935           val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
  1936           val tactic =
  1937             simp_tac (HOL_basic_ss addsimps ext_defs) 1 THEN
  1938             REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE terminal);
  1939           val updaccs = Seq.list_of (tactic init_thm);
  1940         in
  1941           (updaccs RL [updacc_accessor_eqE],
  1942            updaccs RL [updacc_updator_eqE],
  1943            updaccs RL [updacc_cong_from_eq])
  1944         end);
  1945 
  1946     fun lastN xs = drop parent_fields_len xs;
  1947 
  1948     (*selectors*)
  1949     fun mk_sel_spec ((c, T), thm) =
  1950       let
  1951         val (acc $ arg, _) =
  1952           HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (Thm.concl_of thm)));
  1953         val _ =
  1954           if arg aconv r_rec0 then ()
  1955           else raise TERM ("mk_sel_spec: different arg", [arg]);
  1956       in
  1957         Const (mk_selC rec_schemeT0 (c, T)) :== acc
  1958       end;
  1959     val sel_specs = map mk_sel_spec (fields_more ~~ lastN accessor_thms);
  1960 
  1961     (*updates*)
  1962     fun mk_upd_spec ((c, T), thm) =
  1963       let
  1964         val (upd $ _ $ arg, _) =
  1965           HOLogic.dest_eq (HOLogic.dest_Trueprop (Envir.beta_eta_contract (Thm.concl_of thm)));
  1966         val _ =
  1967           if arg aconv r_rec0 then ()
  1968           else raise TERM ("mk_sel_spec: different arg", [arg]);
  1969       in Const (mk_updC updateN rec_schemeT0 (c, T)) :== upd end;
  1970     val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms);
  1971 
  1972     (*derived operations*)
  1973     val make_spec =
  1974       list_comb (Const (full (Binding.name makeN), all_types ---> recT0), all_vars) :==
  1975         mk_rec (all_vars @ [HOLogic.unit]) 0;
  1976     val fields_spec =
  1977       list_comb (Const (full (Binding.name fields_selN), types ---> Type extension), vars) :==
  1978         mk_rec (all_vars @ [HOLogic.unit]) parent_len;
  1979     val extend_spec =
  1980       Const (full (Binding.name extendN), recT0 --> moreT --> rec_schemeT0) $ r_unit0 $ more :==
  1981         mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
  1982     val truncate_spec =
  1983       Const (full (Binding.name truncateN), rec_schemeT0 --> recT0) $ r0 :==
  1984         mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
  1985 
  1986 
  1987     (* 2st stage: defs_thy *)
  1988 
  1989     val (((sel_defs, upd_defs), derived_defs), defs_thy) =
  1990       timeit_msg ctxt "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
  1991         (fn () =>
  1992           ext_thy
  1993           |> Sign.add_advanced_trfuns ([], [], advanced_print_translation, [])
  1994           |> Sign.restore_naming thy
  1995           |> Typedecl.abbrev_global (binding, map #1 alphas, NoSyn) recT0 |> snd
  1996           |> Typedecl.abbrev_global
  1997             (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0
  1998           |> snd
  1999           |> Sign.qualified_path false binding
  2000           |> fold (fn ((x, T), mx) => snd o Sign.declare_const_global ((Binding.name x, T), mx))
  2001             (sel_decls ~~ (field_syntax @ [NoSyn]))
  2002           |> fold (fn (x, T) => snd o Sign.declare_const_global ((Binding.name x, T), NoSyn))
  2003             (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
  2004           |> (Global_Theory.add_defs false o
  2005                 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) sel_specs
  2006           ||>> (Global_Theory.add_defs false o
  2007                 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) upd_specs
  2008           ||>> (Global_Theory.add_defs false o
  2009                 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
  2010             [make_spec, fields_spec, extend_spec, truncate_spec]
  2011           ||> Theory.checkpoint);
  2012 
  2013     (* prepare propositions *)
  2014     val _ = timing_msg ctxt "record preparing propositions";
  2015     val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> HOLogic.boolT);
  2016     val C = Free (singleton (Name.variant_list all_variants) "C", HOLogic.boolT);
  2017     val P_unit = Free (singleton (Name.variant_list all_variants) "P", recT0 --> HOLogic.boolT);
  2018 
  2019     (*selectors*)
  2020     val sel_conv_props =
  2021        map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more;
  2022 
  2023     (*updates*)
  2024     fun mk_upd_prop i (c, T) =
  2025       let
  2026         val x' =
  2027           Free (singleton (Name.variant_list all_variants) (Long_Name.base_name c ^ "'"), T --> T);
  2028         val n = parent_fields_len + i;
  2029         val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more;
  2030       in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
  2031     val upd_conv_props = map2 mk_upd_prop idxms fields_more;
  2032 
  2033     (*induct*)
  2034     val induct_scheme_prop =
  2035       fold_rev Logic.all all_vars_more (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0);
  2036     val induct_prop =
  2037       (fold_rev Logic.all all_vars (Trueprop (P_unit $ r_rec_unit0)), Trueprop (P_unit $ r_unit0));
  2038 
  2039     (*surjective*)
  2040     val surjective_prop =
  2041       let val args = map (fn (c, Free (_, T)) => mk_sel r0 (c, T)) all_named_vars_more
  2042       in r0 === mk_rec args 0 end;
  2043 
  2044     (*cases*)
  2045     val cases_scheme_prop =
  2046       (fold_rev Logic.all all_vars_more ((r0 === r_rec0) ==> Trueprop C), Trueprop C);
  2047 
  2048     val cases_prop =
  2049       fold_rev Logic.all all_vars ((r_unit0 === r_rec_unit0) ==> Trueprop C) ==> Trueprop C;
  2050 
  2051     (*split*)
  2052     val split_meta_prop =
  2053       let
  2054         val P = Free (singleton (Name.variant_list all_variants) "P", rec_schemeT0 --> propT);
  2055       in
  2056         Logic.mk_equals (Logic.all r0 (P $ r0), fold_rev Logic.all all_vars_more (P $ r_rec0))
  2057       end;
  2058 
  2059     val split_object_prop =
  2060       let val ALL = fold_rev (fn (v, T) => fn t => HOLogic.mk_all (v, T, t))
  2061       in ALL [dest_Free r0] (P $ r0) === ALL (map dest_Free all_vars_more) (P $ r_rec0) end;
  2062 
  2063     val split_ex_prop =
  2064       let val EX = fold_rev (fn (v, T) => fn t => HOLogic.mk_exists (v, T, t))
  2065       in EX [dest_Free r0] (P $ r0) === EX (map dest_Free all_vars_more) (P $ r_rec0) end;
  2066 
  2067     (*equality*)
  2068     val equality_prop =
  2069       let
  2070         val s' = Free (rN ^ "'", rec_schemeT0);
  2071         fun mk_sel_eq (c, Free (_, T)) = mk_sel r0 (c, T) === mk_sel s' (c, T);
  2072         val seleqs = map mk_sel_eq all_named_vars_more;
  2073       in Logic.all r0 (Logic.all s' (Logic.list_implies (seleqs, r0 === s'))) end;
  2074 
  2075 
  2076     (* 3rd stage: thms_thy *)
  2077 
  2078     val record_ss = get_simpset defs_thy;
  2079     val sel_upd_ss = record_ss addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms);
  2080 
  2081     val (sel_convs, upd_convs) =
  2082       timeit_msg ctxt "record sel_convs/upd_convs proof:" (fn () =>
  2083         grouped 10 Par_List.map (fn prop =>
  2084           Skip_Proof.prove_global defs_thy [] [] prop
  2085             (K (ALLGOALS (asm_full_simp_tac sel_upd_ss)))) (sel_conv_props @ upd_conv_props))
  2086       |> chop (length sel_conv_props);
  2087 
  2088     val (fold_congs, unfold_congs) = timeit_msg ctxt "record upd fold/unfold congs:" (fn () =>
  2089       let
  2090         val symdefs = map Thm.symmetric (sel_defs @ upd_defs);
  2091         val fold_ss = HOL_basic_ss addsimps symdefs;
  2092         val ua_congs = map (Drule.export_without_context o simplify fold_ss) upd_acc_cong_assists;
  2093       in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end);
  2094 
  2095     val parent_induct = Option.map #induct_scheme (try List.last parents);
  2096 
  2097     val induct_scheme = timeit_msg ctxt "record induct_scheme proof:" (fn () =>
  2098       Skip_Proof.prove_global defs_thy [] [] induct_scheme_prop
  2099         (fn _ =>
  2100           EVERY
  2101            [case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
  2102             try_param_tac rN ext_induct 1,
  2103             asm_simp_tac HOL_basic_ss 1]));
  2104 
  2105     val induct = timeit_msg ctxt "record induct proof:" (fn () =>
  2106       Skip_Proof.prove_global defs_thy [] [#1 induct_prop] (#2 induct_prop) (fn {prems, ...} =>
  2107         try_param_tac rN induct_scheme 1
  2108         THEN try_param_tac "more" @{thm unit.induct} 1
  2109         THEN resolve_tac prems 1));
  2110 
  2111     val surjective = timeit_msg ctxt "record surjective proof:" (fn () =>
  2112       let
  2113         val leaf_ss =
  2114           get_sel_upd_defs defs_thy addsimps (sel_defs @ @{thms o_assoc id_apply id_o o_id});
  2115         val init_ss = HOL_basic_ss addsimps ext_defs;
  2116       in
  2117         Skip_Proof.prove_global defs_thy [] [] surjective_prop
  2118           (fn _ =>
  2119             EVERY
  2120              [rtac surject_assist_idE 1,
  2121               simp_tac init_ss 1,
  2122               REPEAT
  2123                 (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE
  2124                   (rtac surject_assistI 1 THEN simp_tac leaf_ss 1))])
  2125       end);
  2126 
  2127     val cases_scheme = timeit_msg ctxt "record cases_scheme proof:" (fn () =>
  2128       Skip_Proof.prove_global defs_thy [] [#1 cases_scheme_prop] (#2 cases_scheme_prop)
  2129         (fn {prems, ...} =>
  2130           resolve_tac prems 1 THEN
  2131           rtac surjective 1));
  2132 
  2133     val cases = timeit_msg ctxt "record cases proof:" (fn () =>
  2134       Skip_Proof.prove_global defs_thy [] [] cases_prop
  2135         (fn _ =>
  2136           try_param_tac rN cases_scheme 1 THEN
  2137           ALLGOALS (asm_full_simp_tac (HOL_basic_ss addsimps @{thms unit_all_eq1}))));
  2138 
  2139     val split_meta = timeit_msg ctxt "record split_meta proof:" (fn () =>
  2140       Skip_Proof.prove_global defs_thy [] [] split_meta_prop
  2141         (fn _ =>
  2142           EVERY1
  2143            [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac,
  2144             etac @{thm meta_allE}, atac,
  2145             rtac (@{thm prop_subst} OF [surjective]),
  2146             REPEAT o etac @{thm meta_allE}, atac]));
  2147 
  2148     val split_object = timeit_msg ctxt "record split_object proof:" (fn () =>
  2149       Skip_Proof.prove_global defs_thy [] [] split_object_prop
  2150         (fn _ =>
  2151           rtac @{lemma "Trueprop A == Trueprop B ==> A = B" by (rule iffI) unfold} 1 THEN
  2152           rewrite_goals_tac @{thms atomize_all [symmetric]} THEN
  2153           rtac split_meta 1));
  2154 
  2155     val split_ex = timeit_msg ctxt "record split_ex proof:" (fn () =>
  2156       Skip_Proof.prove_global defs_thy [] [] split_ex_prop
  2157         (fn _ =>
  2158           simp_tac
  2159             (HOL_basic_ss addsimps
  2160               (@{lemma "EX x. P x == ~ (ALL x. ~ P x)" by simp} ::
  2161                 @{thms not_not Not_eq_iff})) 1 THEN
  2162           rtac split_object 1));
  2163 
  2164     val equality = timeit_msg ctxt "record equality proof:" (fn () =>
  2165       Skip_Proof.prove_global defs_thy [] [] equality_prop
  2166         (fn _ => asm_full_simp_tac (record_ss addsimps (split_meta :: sel_convs)) 1));
  2167 
  2168     val ([(_, sel_convs'), (_, upd_convs'), (_, sel_defs'), (_, upd_defs'),
  2169           (_, fold_congs'), (_, unfold_congs'),
  2170           (_, splits' as [split_meta', split_object', split_ex']), (_, derived_defs'),
  2171           (_, [surjective']), (_, [equality']), (_, [induct_scheme']), (_, [induct']),
  2172           (_, [cases_scheme']), (_, [cases'])], thms_thy) = defs_thy
  2173       |> Global_Theory.note_thmss ""
  2174        [((Binding.name "select_convs", []), [(sel_convs, [])]),
  2175         ((Binding.name "update_convs", []), [(upd_convs, [])]),
  2176         ((Binding.name "select_defs", []), [(sel_defs, [])]),
  2177         ((Binding.name "update_defs", []), [(upd_defs, [])]),
  2178         ((Binding.name "fold_congs", []), [(fold_congs, [])]),
  2179         ((Binding.name "unfold_congs", []), [(unfold_congs, [])]),
  2180         ((Binding.name "splits", []), [([split_meta, split_object, split_ex], [])]),
  2181         ((Binding.name "defs", []), [(derived_defs, [])]),
  2182         ((Binding.name "surjective", []), [([surjective], [])]),
  2183         ((Binding.name "equality", []), [([equality], [])]),
  2184         ((Binding.name "induct_scheme", induct_type_global (suffix schemeN name)),
  2185           [([induct_scheme], [])]),
  2186         ((Binding.name "induct", induct_type_global name), [([induct], [])]),
  2187         ((Binding.name "cases_scheme", cases_type_global (suffix schemeN name)),
  2188           [([cases_scheme], [])]),
  2189         ((Binding.name "cases", cases_type_global name), [([cases], [])])];
  2190 
  2191     val sel_upd_simps = sel_convs' @ upd_convs';
  2192     val sel_upd_defs = sel_defs' @ upd_defs';
  2193     val depth = parent_len + 1;
  2194 
  2195     val ([(_, simps'), (_, iffs')], thms_thy') = thms_thy
  2196       |> Global_Theory.note_thmss ""
  2197           [((Binding.name "simps", [Simplifier.simp_add]), [(sel_upd_simps, [])]),
  2198            ((Binding.name "iffs", [iff_add]), [([ext_inject], [])])];
  2199 
  2200     val info =
  2201       make_info alphas parent fields extension
  2202         ext_induct ext_inject ext_surjective ext_split ext_def
  2203         sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs'
  2204         surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs';
  2205 
  2206     val final_thy =
  2207       thms_thy'
  2208       |> put_record name info
  2209       |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs
  2210       |> add_equalities extension_id equality'
  2211       |> add_extinjects ext_inject
  2212       |> add_extsplit extension_name ext_split
  2213       |> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
  2214       |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
  2215       |> add_fieldext (extension_name, snd extension) names
  2216       |> add_code ext_tyco vs extT ext simps' ext_inject
  2217       |> Sign.restore_naming thy;
  2218 
  2219   in final_thy end;
  2220 
  2221 
  2222 (* add_record *)
  2223 
  2224 local
  2225 
  2226 fun read_parent NONE ctxt = (NONE, ctxt)
  2227   | read_parent (SOME raw_T) ctxt =
  2228       (case Proof_Context.read_typ_abbrev ctxt raw_T of
  2229         Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt)
  2230       | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));
  2231 
  2232 fun read_fields raw_fields ctxt =
  2233   let
  2234     val Ts = Syntax.read_typs ctxt (map (fn (_, raw_T, _) => raw_T) raw_fields);
  2235     val fields = map2 (fn (x, _, mx) => fn T => (x, T, mx)) raw_fields Ts;
  2236     val ctxt' = fold Variable.declare_typ Ts ctxt;
  2237   in (fields, ctxt') end;
  2238 
  2239 in
  2240 
  2241 fun add_record (params, binding) raw_parent raw_fields thy =
  2242   let
  2243     val _ = Theory.requires thy "Record" "record definitions";
  2244 
  2245     val ctxt = Proof_Context.init_global thy;
  2246     fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T)
  2247       handle TYPE (msg, _, _) => error msg;
  2248 
  2249 
  2250     (* specification *)
  2251 
  2252     val parent = Option.map (apfst (map cert_typ)) raw_parent
  2253       handle ERROR msg =>
  2254         cat_error msg ("The error(s) above occurred in parent record specification");
  2255     val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []);
  2256     val parents = get_parent_info thy parent;
  2257 
  2258     val bfields =
  2259       raw_fields |> map (fn (x, raw_T, mx) => (x, cert_typ raw_T, mx)
  2260         handle ERROR msg =>
  2261           cat_error msg ("The error(s) above occurred in record field " ^ Binding.print x));
  2262 
  2263 
  2264     (* errors *)
  2265 
  2266     val name = Sign.full_name thy binding;
  2267     val err_dup_record =
  2268       if is_none (get_info thy name) then []
  2269       else ["Duplicate definition of record " ^ quote name];
  2270 
  2271     val spec_frees = fold Term.add_tfreesT (parent_args @ map #2 bfields) [];
  2272     val err_extra_frees =
  2273       (case subtract (op =) params spec_frees of
  2274         [] => []
  2275       | extras => ["Extra free type variable(s) " ^
  2276           commas (map (Syntax.string_of_typ ctxt o TFree) extras)]);
  2277 
  2278     val err_no_fields = if null bfields then ["No fields present"] else [];
  2279 
  2280     val err_dup_fields =
  2281       (case duplicates Binding.eq_name (map #1 bfields) of
  2282         [] => []
  2283       | dups => ["Duplicate field(s) " ^ commas (map Binding.print dups)]);
  2284 
  2285     val err_bad_fields =
  2286       if forall (not_equal moreN o Binding.name_of o #1) bfields then []
  2287       else ["Illegal field name " ^ quote moreN];
  2288 
  2289     val errs =
  2290       err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields;
  2291     val _ = if null errs then () else error (cat_lines errs);
  2292   in
  2293     thy |> definition (params, binding) parent parents bfields
  2294   end
  2295   handle ERROR msg => cat_error msg ("Failed to define record " ^ Binding.print binding);
  2296 
  2297 fun add_record_cmd (raw_params, binding) raw_parent raw_fields thy =
  2298   let
  2299     val ctxt = Proof_Context.init_global thy;
  2300     val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
  2301     val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
  2302     val (parent, ctxt2) = read_parent raw_parent ctxt1;
  2303     val (fields, ctxt3) = read_fields raw_fields ctxt2;
  2304     val params' = map (Proof_Context.check_tfree ctxt3) params;
  2305   in thy |> add_record (params', binding) parent fields end;
  2306 
  2307 end;
  2308 
  2309 
  2310 (* setup theory *)
  2311 
  2312 val setup =
  2313   Sign.add_trfuns ([], parse_translation, [], []) #>
  2314   Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #>
  2315   Simplifier.map_simpset_global (fn ss => ss addsimprocs [simproc, upd_simproc, eq_simproc]);
  2316 
  2317 
  2318 (* outer syntax *)
  2319 
  2320 val _ =
  2321   Outer_Syntax.command @{command_spec "record"} "define extensible record"
  2322     (Parse.type_args_constrained -- Parse.binding --
  2323       (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
  2324         Scan.repeat1 Parse.const_binding)
  2325     >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd x y z)));
  2326 
  2327 end;