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