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