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