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