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