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