src/HOL/Tools/record_package.ML
author schirmer
Wed Jun 30 14:04:58 2004 +0200 (2004-06-30)
changeset 15012 28fa57b57209
parent 14981 e73f8140af78
child 15015 c5768e8c4da4
permissions -rw-r--r--
Added reference record_definition_quick_and_dirty_sensitive, to
skip proofs triggered by a record definition, if quick_and_dirty
is enabled.
     1 (*  Title:      HOL/Tools/record_package.ML
     2     ID:         $Id$
     3     Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
     4 
     5 Extensible records with structural subtyping in HOL.
     6 *)
     7 
     8 signature BASIC_RECORD_PACKAGE =
     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 -> bool) -> simproc
    14   val record_ex_sel_eq_simproc: simproc
    15   val record_split_tac: int -> tactic
    16   val record_split_simp_tac: (term -> bool) -> 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_PACKAGE =
    24 sig
    25   include BASIC_RECORD_PACKAGE
    26   val quiet_mode: bool ref
    27   val record_definition_quick_and_dirty_sensitive: bool ref
    28   val updateN: string
    29   val ext_typeN: string
    30   val last_extT: typ -> (string * typ list) option
    31   val dest_recTs : typ -> (string * typ list) list
    32   val get_extension: Sign.sg -> Symtab.key -> (string * typ list) option
    33   val print_records: theory -> unit
    34   val add_record: string list * string -> string option -> (string * string * mixfix) list 
    35                   -> theory -> theory
    36   val add_record_i: string list * string -> (typ list * string) option 
    37                     -> (string * typ * mixfix) list -> theory -> theory
    38   val setup: (theory -> theory) list
    39 end;
    40 
    41 
    42 structure RecordPackage :RECORD_PACKAGE =     
    43 struct
    44 
    45 val rec_UNIV_I = thm "rec_UNIV_I";
    46 val rec_True_simp = thm "rec_True_simp";
    47 val Pair_eq = thm "Product_Type.Pair_eq";
    48 val atomize_all = thm "HOL.atomize_all";
    49 val atomize_imp = thm "HOL.atomize_imp";
    50 val triv_goal   = thm "triv_goal";
    51 val prop_subst  = thm "prop_subst";
    52 val Pair_sel_convs = [fst_conv,snd_conv];
    53 
    54 
    55 
    56 (** name components **)
    57 
    58 val rN = "r";
    59 val moreN = "more";
    60 val schemeN = "_scheme";
    61 val ext_typeN = "_ext_type"; 
    62 val extN ="_ext";
    63 val ext_dest = "_sel";
    64 val updateN = "_update";
    65 val schemeN = "_scheme";
    66 val makeN = "make";
    67 val fields_selN = "fields";
    68 val extendN = "extend";
    69 val truncateN = "truncate";
    70 
    71 (*see typedef_package.ML*)
    72 val RepN = "Rep_";
    73 val AbsN = "Abs_";
    74 
    75 (*** utilities ***)
    76 
    77 fun but_last xs = fst (split_last xs);
    78 
    79 (* messages *)
    80 
    81 val quiet_mode = ref false;
    82 fun message s = if ! quiet_mode then () else writeln s;
    83 
    84 (* timing *)
    85 
    86 fun timeit_msg s x = if !timing then (warning s; timeit x) else x ();
    87  
    88 (* syntax *)
    89 
    90 fun prune n xs = Library.drop (n, xs);
    91 fun prefix_base s = NameSpace.map_base (fn bname => s ^ bname);
    92 
    93 val Trueprop = HOLogic.mk_Trueprop;
    94 fun All xs t = Term.list_all_free (xs, t);
    95 
    96 infix 9 $$;
    97 infix 0 :== ===;
    98 infixr 0 ==>;
    99 
   100 val (op $$) = Term.list_comb;
   101 val (op :==) = Logic.mk_defpair;
   102 val (op ===) = Trueprop o HOLogic.mk_eq;
   103 val (op ==>) = Logic.mk_implies;
   104 
   105 (* morphisms *)
   106 
   107 fun mk_RepN name = suffix ext_typeN (prefix_base RepN name);
   108 fun mk_AbsN name = suffix ext_typeN (prefix_base AbsN name);
   109 
   110 fun mk_Rep name repT absT  =
   111   Const (suffix ext_typeN (prefix_base RepN name),absT --> repT);
   112 
   113 fun mk_Abs name repT absT =
   114   Const (mk_AbsN name,repT --> absT);
   115 
   116 (* constructor *)
   117 
   118 fun mk_extC (name,T) Ts  = (suffix extN name, Ts ---> T);
   119 
   120 fun mk_ext (name,T) ts =
   121   let val Ts = map fastype_of ts
   122   in list_comb (Const (mk_extC (name,T) Ts),ts) end;
   123 
   124 (* selector *)
   125 
   126 fun mk_selC sT (c,T) = (c,sT --> T);
   127 
   128 fun mk_sel s (c,T) =
   129   let val sT = fastype_of s
   130   in Const (mk_selC sT (c,T)) $ s end;
   131 
   132 (* updates *)
   133 
   134 fun mk_updC sT (c,T) = (suffix updateN c, T --> sT --> sT);
   135 
   136 fun mk_upd c v s =
   137   let val sT = fastype_of s;
   138       val vT = fastype_of v;
   139   in Const (mk_updC sT (c, vT)) $ v $ s end;
   140 
   141 (* types *)
   142 
   143 fun dest_recT (typ as Type (c_ext_type, Ts as (T::_))) =
   144       (case try (unsuffix ext_typeN) c_ext_type of
   145         None => raise TYPE ("RecordPackage.dest_recT", [typ], [])
   146       | Some c => ((c, Ts), last_elem Ts))
   147   | dest_recT typ = raise TYPE ("RecordPackage.dest_recT", [typ], []);
   148 
   149 fun is_recT T =
   150   (case try dest_recT T of None => false | Some _ => true); 
   151 
   152 fun dest_recTs T =
   153   let val ((c, Ts), U) = dest_recT T
   154   in (c, Ts) :: dest_recTs U
   155   end handle TYPE _ => [];
   156 
   157 fun last_extT T =
   158   let val ((c, Ts), U) = dest_recT T
   159   in (case last_extT U of
   160         None => Some (c,Ts)
   161       | Some l => Some l)
   162   end handle TYPE _ => None
   163 
   164 fun rec_id T = foldl (fn (s,(c,T)) => s ^ c) ("",dest_recTs T);
   165 
   166 (*** extend theory by record definition ***)
   167 
   168 (** record info **)
   169 
   170 (* type record_info and parent_info  *)
   171 
   172 type record_info =
   173  {args: (string * sort) list,
   174   parent: (typ list * string) option,
   175   fields: (string * typ) list,
   176   extension: (string * typ list),
   177   induct: thm
   178  };
   179 
   180 fun make_record_info args parent fields extension induct =
   181  {args = args, parent = parent, fields = fields, extension = extension, 
   182   induct = induct}: record_info;
   183 
   184 
   185 type parent_info =
   186  {name: string,
   187   fields: (string * typ) list,
   188   extension: (string * typ list),
   189   induct: thm
   190 };
   191 
   192 fun make_parent_info name fields extension induct =
   193  {name = name, fields = fields, extension = extension, induct = induct}: parent_info;
   194 
   195 (* data kind 'HOL/record' *)
   196 
   197 type record_data =
   198  {records: record_info Symtab.table,
   199   sel_upd:
   200    {selectors: unit Symtab.table,
   201     updates: string Symtab.table,
   202     simpset: Simplifier.simpset},
   203   equalities: thm Symtab.table,
   204   splits: (thm*thm*thm*thm) Symtab.table,    (* !!,!,EX - split-equalities,induct rule *) 
   205   extfields: (string*typ) list Symtab.table, (* maps extension to its fields *)
   206   fieldext: (string*typ list) Symtab.table   (* maps field to its extension *)
   207 };
   208 
   209 fun make_record_data records sel_upd equalities splits extfields fieldext =
   210  {records = records, sel_upd = sel_upd, 
   211   equalities = equalities, splits = splits, 
   212   extfields = extfields, fieldext = fieldext }: record_data;
   213 
   214 structure RecordsArgs =
   215 struct
   216   val name = "HOL/records";     
   217   type T = record_data;
   218 
   219   val empty =
   220     make_record_data Symtab.empty
   221       {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss}
   222       Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
   223 
   224   val copy = I;
   225   val prep_ext = I;
   226   fun merge
   227    ({records = recs1,
   228      sel_upd = {selectors = sels1, updates = upds1, simpset = ss1},
   229      equalities = equalities1,
   230      splits = splits1,
   231      extfields = extfields1,
   232      fieldext = fieldext1},
   233     {records = recs2,
   234      sel_upd = {selectors = sels2, updates = upds2, simpset = ss2},
   235      equalities = equalities2, 
   236      splits = splits2,
   237      extfields = extfields2,
   238      fieldext = fieldext2}) =
   239     make_record_data  
   240       (Symtab.merge (K true) (recs1, recs2))
   241       {selectors = Symtab.merge (K true) (sels1, sels2),
   242         updates = Symtab.merge (K true) (upds1, upds2),
   243         simpset = Simplifier.merge_ss (ss1, ss2)}
   244       (Symtab.merge Thm.eq_thm (equalities1, equalities2))
   245       (Symtab.merge (fn ((a,b,c,d),(w,x,y,z)) 
   246                      => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso 
   247                         Thm.eq_thm (c,y) andalso Thm.eq_thm (d,z)) 
   248                     (splits1, splits2))
   249       (Symtab.merge (K true) (extfields1,extfields2))
   250       (Symtab.merge (K true) (fieldext1,fieldext2));
   251 
   252   fun print sg ({records = recs, ...}: record_data) =
   253     let
   254       val prt_typ = Sign.pretty_typ sg;
   255 
   256       fun pretty_parent None = []
   257         | pretty_parent (Some (Ts, name)) =
   258             [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
   259 
   260       fun pretty_field (c, T) = Pretty.block
   261         [Pretty.str (Sign.cond_extern sg Sign.constK c), Pretty.str " ::",
   262           Pretty.brk 1, Pretty.quote (prt_typ T)];
   263 
   264       fun pretty_record (name, {args, parent, fields, ...}: record_info) =
   265         Pretty.block (Pretty.fbreaks (Pretty.block
   266           [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
   267           pretty_parent parent @ map pretty_field fields));
   268     in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
   269 end;
   270 
   271 structure RecordsData = TheoryDataFun(RecordsArgs);
   272 val print_records = RecordsData.print;
   273 
   274 (* access 'records' *)
   275 
   276 fun get_record thy name = Symtab.lookup (#records (RecordsData.get thy), name);
   277 
   278 fun put_record name info thy =
   279   let
   280     val {records, sel_upd, equalities, splits,extfields,fieldext} = RecordsData.get thy;
   281     val data = make_record_data (Symtab.update ((name, info), records))
   282       sel_upd equalities splits extfields fieldext;
   283   in RecordsData.put data thy end;
   284 
   285 (* access 'sel_upd' *)
   286 
   287 fun get_sel_upd sg = #sel_upd (RecordsData.get_sg sg);
   288 
   289 fun get_selectors sg name = Symtab.lookup (#selectors (get_sel_upd sg), name);
   290 fun is_selector sg name = 
   291   case get_selectors sg (Sign.intern_const sg name) of 
   292      None => false
   293    | Some _ => true
   294 
   295                              
   296 fun get_updates sg name = Symtab.lookup (#updates (get_sel_upd sg), name);
   297 fun get_simpset sg = #simpset (get_sel_upd sg);
   298 
   299 fun put_sel_upd names simps thy =
   300   let
   301     val sels = map (rpair ()) names;
   302     val upds = map (suffix updateN) names ~~ names;
   303 
   304     val {records, sel_upd = {selectors, updates, simpset}, 
   305       equalities, splits, extfields,fieldext} = RecordsData.get thy;
   306     val data = make_record_data records
   307       {selectors = Symtab.extend (selectors, sels),
   308         updates = Symtab.extend (updates, upds),
   309         simpset = Simplifier.addsimps (simpset, simps)}
   310        equalities splits extfields fieldext;
   311   in RecordsData.put data thy end;
   312 
   313 (* access 'equalities' *)
   314 
   315 fun add_record_equalities name thm thy =
   316   let
   317     val {records, sel_upd, equalities, splits, extfields,fieldext} = RecordsData.get thy;
   318     val data = make_record_data records sel_upd 
   319       (Symtab.update_new ((name, thm), equalities)) splits extfields fieldext;
   320   in RecordsData.put data thy end;
   321 
   322 fun get_equalities sg name =
   323   Symtab.lookup (#equalities (RecordsData.get_sg sg), name);
   324 
   325 (* access 'splits' *)
   326 
   327 fun add_record_splits name thmP thy =
   328   let
   329     val {records, sel_upd, equalities, splits, extfields,fieldext} = RecordsData.get thy;
   330     val data = make_record_data records sel_upd 
   331       equalities (Symtab.update_new ((name, thmP), splits)) extfields fieldext;
   332   in RecordsData.put data thy end;
   333 
   334 fun get_splits sg name =
   335   Symtab.lookup (#splits (RecordsData.get_sg sg), name);
   336 
   337 (* extension of a record name *)
   338 fun get_extension sg name =
   339  case Symtab.lookup (#records (RecordsData.get_sg sg),name) of
   340         Some s => Some (#extension s)
   341       | None => None;
   342 
   343 (* access 'extfields' *)
   344 
   345 fun add_extfields name fields thy =
   346   let
   347     val {records, sel_upd, equalities, splits, extfields, fieldext} = RecordsData.get thy;
   348     val data = make_record_data records sel_upd 
   349          equalities splits (Symtab.update_new ((name, fields), extfields)) fieldext;
   350   in RecordsData.put data thy end;
   351 
   352 fun get_extfields sg name =
   353   Symtab.lookup (#extfields (RecordsData.get_sg sg), name);
   354 
   355 (* access 'fieldext' *)
   356 
   357 fun add_fieldext extname_types fields thy =
   358   let
   359     val {records, sel_upd, equalities, splits, extfields, fieldext} = RecordsData.get thy;
   360     val fieldext' = foldl (fn (table,field) => Symtab.update_new ((field,extname_types),table))  
   361                           (fieldext,fields);
   362     val data = make_record_data records sel_upd equalities splits extfields fieldext';
   363   in RecordsData.put data thy end;
   364 
   365 
   366 fun get_fieldext sg name =
   367   Symtab.lookup (#fieldext (RecordsData.get_sg sg), name);
   368 
   369 (* parent records *)
   370 
   371 fun add_parents thy None parents = parents
   372   | add_parents thy (Some (types, name)) parents =
   373       let
   374         val sign = Theory.sign_of thy;
   375         fun err msg = error (msg ^ " parent record " ^ quote name);
   376 
   377         val {args, parent, fields, extension, induct} =
   378           (case get_record thy name of Some info => info | None => err "Unknown");
   379         val _ = if length types <> length args then err "Bad number of arguments for" else ();
   380 
   381         fun bad_inst ((x, S), T) =
   382           if Sign.of_sort sign (T, S) then None else Some x
   383         val bads = mapfilter bad_inst (args ~~ types);
   384 
   385         val inst = map fst args ~~ types;
   386         val subst = Term.map_type_tfree (fn (x, _) => the (assoc (inst, x)));
   387         val parent' = apsome (apfst (map subst)) parent;
   388         val fields' = map (apsnd subst) fields;
   389         val extension' = apsnd (map subst) extension;
   390       in
   391         conditional (not (null bads)) (fn () =>
   392           err ("Ill-sorted instantiation of " ^ commas bads ^ " in"));
   393         add_parents thy parent'
   394           (make_parent_info name fields' extension' induct::parents)
   395       end;
   396 
   397 
   398 (** concrete syntax for records **)
   399 
   400 (* parse translations *)
   401 
   402 fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) =
   403       if c = mark then Syntax.const (suffix sfx name) $ arg
   404       else raise TERM ("gen_field_tr: " ^ mark, [t])
   405   | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]);
   406 
   407 fun gen_fields_tr sep mark sfx (tm as Const (c, _) $ t $ u) =
   408       if c = sep then gen_field_tr mark sfx t :: gen_fields_tr sep mark sfx u
   409       else [gen_field_tr mark sfx tm]
   410   | gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm];
   411 
   412 
   413 fun record_update_tr [t, u] =
   414       foldr (op $) (rev (gen_fields_tr "_updates" "_update" updateN u), t)
   415   | record_update_tr ts = raise TERM ("record_update_tr", ts);
   416 
   417 fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts
   418   | update_name_tr (Const (x, T) :: ts) = Const (suffix updateN x, T) $$ ts
   419   | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
   420       (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy")) $$ ts
   421   | update_name_tr ts = raise TERM ("update_name_tr", ts);
   422 
   423 fun dest_ext_field mark (t as (Const (c,_) $ Const (name,_) $ arg)) =
   424      if c = mark then (name,arg) else raise TERM ("dest_ext_field: " ^ mark, [t])
   425   | dest_ext_field _ t = raise TERM ("dest_ext_field", [t])
   426 
   427 fun dest_ext_fields sep mark (trm as (Const (c,_) $ t $ u)) =
   428      if c = sep then dest_ext_field mark t::dest_ext_fields sep mark u
   429      else [dest_ext_field mark trm]
   430   | dest_ext_fields _ mark t = [dest_ext_field mark t]
   431 
   432 fun gen_ext_fields_tr sep mark sfx more sg t =
   433   let 
   434     val msg = "error in record input: ";
   435     val fieldargs = dest_ext_fields sep mark t; 
   436     fun splitargs (field::fields) ((name,arg)::fargs) =
   437           if can (unsuffix name) field
   438           then let val (args,rest) = splitargs fields fargs
   439                in (arg::args,rest) end
   440           else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t])
   441       | splitargs [] (fargs as (_::_)) = ([],fargs)
   442       | splitargs (_::_) [] = raise TERM (msg ^ "expecting more fields", [t])
   443       | splitargs _ _ = ([],[]);
   444 
   445     fun mk_ext (fargs as (name,arg)::_) =
   446          (case get_fieldext sg (Sign.intern_const sg name) of
   447             Some (ext,_) => (case get_extfields sg ext of
   448                                Some flds 
   449                                  => let val (args,rest) = 
   450                                                splitargs (map fst (but_last flds)) fargs;
   451                                         val more' = mk_ext rest;  
   452                                     in list_comb (Syntax.const (suffix sfx ext),args@[more'])
   453                                     end
   454                              | None => raise TERM(msg ^ "no fields defined for "
   455                                                    ^ ext,[t]))
   456           | None => raise TERM (msg ^ name ^" is no proper field",[t]))
   457       | mk_ext [] = more
   458 
   459   in mk_ext fieldargs end;   
   460 
   461 fun gen_ext_type_tr sep mark sfx more sg t =
   462   let 
   463     val msg = "error in record-type input: ";
   464     val fieldargs = dest_ext_fields sep mark t; 
   465     fun splitargs (field::fields) ((name,arg)::fargs) =
   466           if can (unsuffix name) field
   467           then let val (args,rest) = splitargs fields fargs
   468                in (arg::args,rest) end
   469           else raise TERM (msg ^ "expecting field " ^ field ^ " but got " ^ name, [t])
   470       | splitargs [] (fargs as (_::_)) = ([],fargs)
   471       | splitargs (_::_) [] = raise TERM (msg ^ "expecting more fields", [t])
   472       | splitargs _ _ = ([],[]);
   473 
   474     fun get_sort xs n = (case assoc (xs,n) of 
   475                                 Some s => s 
   476                               | None => Sign.defaultS sg);
   477     fun to_type t = Sign.intern_typ sg 
   478                       (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t);
   479  
   480     val tsig = Sign.tsig_of sg;
   481     fun unify (t,env) = Type.unify tsig env t; 
   482     
   483     fun mk_ext (fargs as (name,arg)::_) =
   484          (case get_fieldext sg (Sign.intern_const sg name) of
   485             Some (ext,alphas) => 
   486               (case get_extfields sg ext of
   487                  Some flds 
   488                   => (let
   489                        val flds' = but_last flds;
   490                        val types = map snd flds'; 
   491                        val (args,rest) = splitargs (map fst flds') fargs;
   492                        val vartypes = map Type.varifyT types;
   493                        val argtypes = map to_type args;
   494                        val (subst,_) = foldr unify (vartypes ~~ argtypes,(Vartab.empty,0));
   495                        val alphas' = map ((Syntax.term_of_typ (! Syntax.show_sorts)) o 
   496                                           (Envir.norm_type subst) o Type.varifyT) 
   497                                          (but_last alphas);
   498  
   499                        val more' = mk_ext rest;   
   500                      in list_comb (Syntax.const (suffix sfx ext),alphas'@[more']) 
   501                      end handle TUNIFY => raise 
   502                            TERM (msg ^ "type is no proper record (extension)", [t]))
   503                | None => raise TERM (msg ^ "no fields defined for " ^ ext,[t]))
   504           | None => raise TERM (msg ^ name ^" is no proper field",[t]))
   505       | mk_ext [] = more
   506 
   507   in mk_ext fieldargs end;   
   508 
   509 fun gen_adv_record_tr sep mark sfx unit sg [t] = 
   510       gen_ext_fields_tr sep mark sfx unit sg t
   511   | gen_adv_record_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
   512 
   513 fun gen_adv_record_scheme_tr sep mark sfx sg [t, more] = 
   514       gen_ext_fields_tr sep mark sfx more sg t 
   515   | gen_adv_record_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
   516 
   517 fun gen_adv_record_type_tr sep mark sfx unit sg [t] = 
   518       gen_ext_type_tr sep mark sfx unit sg t
   519   | gen_adv_record_type_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
   520 
   521 fun gen_adv_record_type_scheme_tr sep mark sfx sg [t, more] = 
   522       gen_ext_type_tr sep mark sfx more sg t 
   523   | gen_adv_record_type_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
   524 
   525 val adv_record_tr = gen_adv_record_tr "_fields" "_field" extN HOLogic.unit;
   526 val adv_record_scheme_tr = gen_adv_record_scheme_tr "_fields" "_field" extN;
   527 
   528 val adv_record_type_tr = 
   529       gen_adv_record_type_tr "_field_types" "_field_type" ext_typeN 
   530         (Syntax.term_of_typ false (HOLogic.unitT));
   531 val adv_record_type_scheme_tr = 
   532       gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN;
   533 
   534 val parse_translation =
   535  [("_record_update", record_update_tr),
   536   ("_update_name", update_name_tr)];
   537 
   538 val adv_parse_translation = 
   539  [("_record",adv_record_tr),
   540   ("_record_scheme",adv_record_scheme_tr),
   541   ("_record_type",adv_record_type_tr),
   542   ("_record_type_scheme",adv_record_type_scheme_tr)];
   543 
   544 
   545 (* print translations *)
   546 
   547 val print_record_type_abbr = ref true;
   548 val print_record_type_as_fields = ref true;
   549 
   550 fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ t $ u) =
   551     (case try (unsuffix sfx) name_field of
   552       Some name =>
   553         apfst (cons (Syntax.const mark $ Syntax.free name $ t)) (gen_field_upds_tr' mark sfx u)
   554      | None => ([], tm))
   555   | gen_field_upds_tr' _ _ tm = ([], tm);
   556 
   557 fun record_update_tr' tm =
   558   let val (ts, u) = gen_field_upds_tr' "_update" updateN tm in
   559     Syntax.const "_record_update" $ u $
   560       foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts)
   561   end;
   562 
   563 fun gen_field_tr' sfx tr' name =
   564   let val name_sfx = suffix sfx name
   565   in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
   566 
   567 fun record_tr' sep mark record record_scheme unit sg t =
   568   let 
   569     fun field_lst t =
   570       (case strip_comb t of
   571         (Const (ext,_),args) 
   572          => (case try (unsuffix extN) (Sign.intern_const sg ext) of
   573                Some ext' 
   574                => (case get_extfields sg ext' of
   575                      Some flds 
   576                      => (let
   577                           val (f::fs) = but_last (map fst flds);
   578                           val flds' = Sign.extern sg Sign.constK f::map NameSpace.base fs; 
   579                           val (args',more) = split_last args; 
   580                          in (flds'~~args')@field_lst more end
   581                          handle LIST _ => [("",t)]) 
   582                    | None => [("",t)])
   583              | None => [("",t)])
   584        | _ => [("",t)])
   585 
   586     val (flds,(_,more)) = split_last (field_lst t);
   587     val flds' = map (fn (n,t)=>Syntax.const mark$Syntax.const n$t) flds;
   588     val flds'' = foldr1 (fn (x,y) => Syntax.const sep$x$y) flds';
   589 
   590   in if null flds then raise Match
   591      else if unit more  
   592           then Syntax.const record$flds'' 
   593           else Syntax.const record_scheme$flds''$more
   594   end
   595 
   596 fun gen_record_tr' name = 
   597   let val name_sfx = suffix extN name;
   598       val unit = (fn Const ("Unity",_) => true | _ => false);
   599       fun tr' sg ts = record_tr' "_fields" "_field" "_record" "_record_scheme" unit sg 
   600                        (list_comb (Syntax.const name_sfx,ts))
   601   in (name_sfx,tr')
   602   end
   603 
   604 fun print_translation names =
   605   map (gen_field_tr' updateN record_update_tr') names;
   606 
   607 (* record_type_abbr_tr' tries to reconstruct the record name type abbreviation from *)
   608 (* the (nested) extension types.                                                    *)
   609 fun record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT sg tm =
   610   let
   611       (* tm is term representation of a (nested) field type. We first reconstruct the      *)
   612       (* type from tm so that we can continue on the type level rather then the term level.*)
   613 
   614       fun get_sort xs n = (case assoc (xs,n) of 
   615                              Some s => s 
   616                            | None => Sign.defaultS sg);
   617 
   618       val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm) 
   619       val tsig = Sign.tsig_of sg
   620 
   621       fun mk_type_abbr subst name alphas = 
   622           let val abbrT = Type (name, map (fn a => TVar ((a, 0), [])) alphas);
   623           in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;    
   624 
   625       fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T))
   626 
   627    in if !print_record_type_abbr
   628       then (case last_extT T of
   629              Some (name,_) 
   630               => if name = lastExt 
   631                  then
   632 		  (let val subst = unify schemeT T 
   633                    in 
   634                     if HOLogic.is_unitT (Envir.norm_type subst (TVar((zeta,0),Sign.defaultS sg)))
   635                     then mk_type_abbr subst abbr alphas
   636                     else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta])
   637 		   end handle TUNIFY => default_tr' sg tm)
   638                  else raise Match (* give print translation of specialised record a chance *)
   639             | _ => raise Match)
   640        else default_tr' sg tm
   641   end
   642 
   643 fun record_type_tr' sep mark record record_scheme sg t =
   644   let
   645     fun get_sort xs n = (case assoc (xs,n) of 
   646                              Some s => s 
   647                            | None => Sign.defaultS sg);
   648 
   649     val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t)
   650 
   651     val tsig = Sign.tsig_of sg
   652     fun unify (t,v) = Type.unify tsig v t;
   653 
   654     fun term_of_type T = Syntax.term_of_typ (!Syntax.show_sorts) (Sign.extern_typ sg T);
   655  
   656     fun field_lst T =
   657       (case T of
   658         Type (ext,args) 
   659          => (case try (unsuffix ext_typeN) ext of
   660                Some ext' 
   661                => (case get_extfields sg ext' of
   662                      Some flds 
   663                      => (case get_fieldext sg (fst (hd flds)) of
   664                            Some (_,alphas) 
   665                            => (let
   666                                 val (f::fs) = but_last flds;
   667                                 val flds' = apfst (Sign.extern sg Sign.constK) f
   668                                             ::map (apfst NameSpace.base) fs; 
   669                                 val (args',more) = split_last args; 
   670                                 val alphavars = map Type.varifyT (but_last alphas); 
   671                                 val (subst,_)= foldr unify (alphavars~~args',(Vartab.empty,0));
   672                                 val flds'' =map (apsnd ((Envir.norm_type subst)o(Type.varifyT)))
   673                                                 flds';
   674                               in flds''@field_lst more end
   675                               handle TUNIFY => [("",T)] 
   676                                    | LIST _=> [("",T)])
   677                          | None => [("",T)])
   678                    | None => [("",T)])
   679              | None => [("",T)]) 
   680         | _ => [("",T)])
   681 
   682     val (flds,(_,moreT)) = split_last (field_lst T);
   683     val flds' = map (fn (n,T)=>Syntax.const mark$Syntax.const n$term_of_type T) flds;
   684     val flds'' = foldr1 (fn (x,y) => Syntax.const sep$x$y) flds';
   685 
   686   in if not (!print_record_type_as_fields) orelse null flds then raise Match
   687      else if moreT = HOLogic.unitT 
   688           then Syntax.const record$flds'' 
   689           else Syntax.const record_scheme$flds''$term_of_type moreT
   690   end
   691     
   692 
   693 fun gen_record_type_tr' name = 
   694   let val name_sfx = suffix ext_typeN name;
   695       fun tr' sg ts = record_type_tr' "_field_types" "_field_type" 
   696                        "_record_type" "_record_type_scheme" sg 
   697                        (list_comb (Syntax.const name_sfx,ts))
   698   in (name_sfx,tr')
   699   end
   700 
   701      
   702 fun gen_record_type_abbr_tr' abbr alphas zeta lastExt schemeT name =
   703   let val name_sfx = suffix ext_typeN name;
   704       val default_tr' = record_type_tr' "_field_types" "_field_type" 
   705                                "_record_type" "_record_type_scheme" 
   706       fun tr' sg ts = record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT sg
   707                          (list_comb (Syntax.const name_sfx,ts))
   708   in (name_sfx, tr') end;
   709 
   710 
   711 (** record simprocs **)
   712 fun quick_and_dirty_prove sg xs asms prop tac =
   713 Tactic.prove_standard sg xs asms prop
   714     (if !quick_and_dirty then (K (SkipProof.cheat_tac HOL.thy)) else tac);
   715 
   716 
   717 fun prove_split_simp sg T prop =
   718   (case get_splits sg (rec_id T) of
   719      Some (all_thm,_,_,_) 
   720      => let val {sel_upd={simpset,...},...} = RecordsData.get_sg sg;
   721         in (quick_and_dirty_prove sg [] [] prop 
   722            (K (simp_tac (simpset addsimps [all_thm]) 1)))
   723         end
   724    | _ => error "RecordPackage.prove_split_simp:code should never been reached")
   725 
   726 (* record_simproc *)
   727 (* Simplifies selections of an record update:
   728  *  (1)  S (r(|S:=k|)) = k respectively
   729  *  (2)  S (r(|X:=k|)) = S r
   730  * The simproc skips multiple updates at once, eg:
   731  *  S (r (|S:=k,X:=2,Y:=3|)) = k
   732  * But be careful in (2) because of the extendibility of records.
   733  * - If S is a more-selector we have to make sure that the update on component
   734  *   X does not affect the selected subrecord.
   735  * - If X is a more-selector we have to make sure that S is not in the updated
   736  *   subrecord. 
   737  *)
   738 val record_simproc =
   739   Simplifier.simproc (Theory.sign_of HOL.thy) "record_simp" ["s (u k r)"]
   740     (fn sg => fn _ => fn t =>
   741       (case t of (sel as Const (s, Type (_,[domS,rangeS]))) $ ((upd as Const (u, _)) $ k $ r) =>
   742         (case get_selectors sg s of Some () =>
   743           (case get_updates sg u of Some u_name =>
   744             let
   745               fun mk_abs_var x t = (x, fastype_of t);
   746               val {sel_upd={updates,...},extfields,...} = RecordsData.get_sg sg;
   747               fun flds T = 
   748                    foldl (fn (xs,(eN,_))=>xs@(map fst (Symtab.lookup_multi (extfields,eN))))
   749                          ([],(dest_recTs T));
   750               fun mk_eq_terms ((upd as Const (u,Type(_,[updT,_]))) $ k $ r) =
   751 		  (case (Symtab.lookup (updates,u)) of
   752                      None => None
   753                    | Some u_name 
   754                      => if u_name = s
   755                         then let 
   756                                val rv = mk_abs_var "r" r
   757                                val rb = Bound 0
   758                                val kv = mk_abs_var "k" k
   759                                val kb = Bound 1 
   760                              in Some (upd$kb$rb,kb,[kv,rv],true) end
   761                         else if u_name mem (flds rangeS)
   762                              orelse s mem (flds updT)
   763                              then None
   764 			     else (case mk_eq_terms r of 
   765                                      Some (trm,trm',vars,update_s) 
   766                                      => let   
   767 					  val kv = mk_abs_var "k" k
   768                                           val kb = Bound (length vars)
   769 		                        in Some (upd$kb$trm,trm',kv::vars,update_s) end
   770                                    | None
   771                                      => let 
   772 					  val rv = mk_abs_var "r" r
   773                                           val rb = Bound 0
   774                                           val kv = mk_abs_var "k" k
   775                                           val kb = Bound 1 
   776                                         in Some (upd$kb$rb,rb,[kv,rv],false) end))
   777                 | mk_eq_terms r = None     
   778             in
   779 	      (case mk_eq_terms (upd$k$r) of
   780                  Some (trm,trm',vars,update_s) 
   781                  => if update_s 
   782 		    then Some (prove_split_simp sg domS 
   783                                  (list_all(vars,(Logic.mk_equals (sel$trm,trm')))))
   784                     else Some (prove_split_simp sg domS 
   785                                  (list_all(vars,(Logic.mk_equals (sel$trm,sel$trm')))))
   786                | None => None)
   787             end
   788           | None => None)
   789         | None => None)
   790       | _ => None));
   791 
   792 (* record_eq_simproc *)
   793 (* looks up the most specific record-equality.
   794  * Note on efficiency:
   795  * Testing equality of records boils down to the test of equality of all components.
   796  * Therefore the complexity is: #components * complexity for single component.
   797  * Especially if a record has a lot of components it may be better to split up
   798  * the record first and do simplification on that (record_split_simp_tac).
   799  * e.g. r(|lots of updates|) = x
   800  *
   801  *               record_eq_simproc       record_split_simp_tac
   802  * Complexity: #components * #updates     #updates   
   803  *           
   804  *)
   805 val record_eq_simproc =
   806   Simplifier.simproc (Theory.sign_of HOL.thy) "record_eq_simp" ["r = s"]
   807     (fn sg => fn _ => fn t =>
   808       (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ =>
   809         (case rec_id T of
   810            "" => None
   811          | name => (case get_equalities sg name of
   812                                 None => None
   813                               | Some thm => Some (thm RS Eq_TrueI)))
   814        | _ => None));
   815 
   816 
   817 (* record_upd_simproc *)
   818 (* simplify multiple updates; for example: "r(|M:=3,N:=1,M:=2,N:=4|) == r(|M:=2,N:=4|)" *)
   819 val record_upd_simproc =
   820   Simplifier.simproc (Theory.sign_of HOL.thy) "record_upd_simp" ["(u1 k1 (u2 k2 r))"]
   821     (fn sg => fn _ => fn t =>
   822       (case t of ((upd as Const (u, Type(_,[_,Type(_,[T,_])]))) $ k $ r) =>
   823  	 let val {sel_upd={updates,...},...} = RecordsData.get_sg sg;
   824 	     fun mk_abs_var x t = (x, fastype_of t);
   825 
   826              fun mk_updterm upds already ((upd as Const (u,_)) $ k $ r) =
   827 		 if is_some (Symtab.lookup (upds,u))
   828 		 then let 
   829 			 fun rest already = mk_updterm upds already
   830 		      in if is_some (Symtab.lookup (already,u)) 
   831 			 then (case (rest already r) of
   832 				 None => let 
   833 				           val rv = mk_abs_var "r" r
   834                                            val rb = Bound 0
   835 					   val kv = mk_abs_var "k" k
   836                                            val kb = Bound 1	      
   837                                          in Some (upd$kb$rb,rb,[kv,rv]) end
   838                                | Some (trm,trm',vars) 
   839 				 => let 
   840 				     val kv = mk_abs_var "k" k
   841                                      val kb = Bound (length vars)
   842                                     in Some (upd$kb$trm,trm',kv::vars) end)
   843 	                 else (case rest (Symtab.update ((u,()),already)) r of 
   844 				 None => None
   845 		               | Some (trm,trm',vars) 
   846                                   => let
   847 				      val kv = mk_abs_var "k" k
   848                                       val kb = Bound (length vars)
   849                                      in Some (upd$kb$trm,upd$kb$trm',kv::vars) end)
   850 		     end
   851 		 else None
   852 	       | mk_updterm _ _ _ = None;
   853 
   854 	 in (case mk_updterm updates Symtab.empty t of
   855 	       Some (trm,trm',vars)
   856                 => Some (prove_split_simp sg T  
   857                           (list_all(vars,(Logic.mk_equals (trm,trm')))))
   858              | None => None)
   859 	 end
   860        | _ => None));
   861 
   862 (* record_split_simproc *)
   863 (* splits quantified occurrences of records, for which P holds. P can peek on the 
   864  * subterm starting at the quantified occurrence of the record (including the quantifier)
   865  *)
   866 fun record_split_simproc P =
   867   Simplifier.simproc (Theory.sign_of HOL.thy) "record_split_simp" ["(a t)"]
   868     (fn sg => fn _ => fn t =>
   869       (case t of (Const (quantifier, Type (_, [Type (_, [T, _]), _])))$trm =>
   870          if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex"
   871          then (case rec_id T of
   872                  "" => None
   873                | name
   874                   => if P t 
   875                      then (case get_splits sg name of
   876                              None => None
   877                            | Some (all_thm, All_thm, Ex_thm,_) 
   878                               => Some (case quantifier of
   879                                          "all" => all_thm
   880                                        | "All" => All_thm RS HOL.eq_reflection
   881                                        | "Ex"  => Ex_thm RS HOL.eq_reflection
   882                                        | _     => error "record_split_simproc"))
   883                      else None)
   884          else None
   885        | _ => None))
   886 
   887 val record_ex_sel_eq_simproc =
   888   Simplifier.simproc (Theory.sign_of HOL.thy) "record_ex_sel_eq_simproc" ["Ex t"]
   889     (fn sg => fn _ => fn t =>
   890        let 
   891          fun prove prop = (quick_and_dirty_prove sg [] [] prop 
   892                              (fn _ => (simp_tac ((get_simpset sg) addsimps simp_thms
   893                                         addsimprocs [record_split_simproc (K true)]) 1)));
   894 
   895          fun mkeq (lr,Teq,(sel,Tsel),x) i =
   896               (case get_selectors sg sel of Some () =>
   897                  let val x' = if not (loose_bvar1 (x,0)) 
   898                               then Free ("x" ^ string_of_int i, range_type Tsel) 
   899                               else raise TERM ("",[x]);
   900                      val sel' = Const (sel,Tsel)$Bound 0;
   901                      val (l,r) = if lr then (sel',x') else (x',sel');
   902                   in Const ("op =",Teq)$l$r end
   903                | None => raise TERM ("",[Const (sel,Tsel)]));
   904 
   905          fun dest_sel_eq (Const ("op =",Teq)$(Const (sel,Tsel)$Bound 0)$X) = 
   906                            (true,Teq,(sel,Tsel),X)
   907            | dest_sel_eq (Const ("op =",Teq)$X$(Const (sel,Tsel)$Bound 0)) =
   908                            (false,Teq,(sel,Tsel),X)
   909            | dest_sel_eq _ = raise TERM ("",[]);
   910 
   911        in         
   912          (case t of 
   913            (Const ("Ex",Tex)$Abs(s,T,t)) =>
   914              let val eq = mkeq (dest_sel_eq t) 0;
   915                  val prop = list_all ([("r",T)],
   916                               Logic.mk_equals (Const ("Ex",Tex)$Abs(s,T,eq),
   917                                                HOLogic.true_const));
   918              in Some (prove prop) end
   919              handle TERM _ => None
   920           | _ => None)                      
   921          end)
   922 
   923 
   924     
   925 
   926 local
   927 val inductive_atomize = thms "induct_atomize";
   928 val inductive_rulify1 = thms "induct_rulify1";
   929 in
   930 (* record_split_simp_tac *)
   931 (* splits (and simplifies) all records in the goal for which P holds. 
   932  * For quantified occurrences of a record
   933  * P can peek on the whole subterm (including the quantifier); for free variables P
   934  * can only peek on the variable itself. 
   935  *)
   936 fun record_split_simp_tac P i st =
   937   let
   938     val sg = Thm.sign_of_thm st;
   939     val {sel_upd={simpset,...},...} 
   940             = RecordsData.get_sg sg;
   941 
   942     val has_rec = exists_Const
   943       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   944           (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T 
   945         | _ => false);
   946 
   947     val goal = Library.nth_elem (i - 1, Thm.prems_of st);
   948     val frees = filter (is_recT o type_of) (term_frees goal);
   949 
   950     fun mk_split_free_tac free induct_thm i = 
   951 	let val cfree = cterm_of sg free;
   952             val (_$(_$r)) = concl_of induct_thm;
   953             val crec = cterm_of sg r;
   954             val thm  = cterm_instantiate [(crec,cfree)] induct_thm;
   955         in EVERY [simp_tac (HOL_basic_ss addsimps inductive_atomize) i,
   956                   rtac thm i,
   957                   simp_tac (HOL_basic_ss addsimps inductive_rulify1) i]
   958 	end;
   959 
   960     fun split_free_tac P i (free as Free (n,T)) = 
   961 	(case rec_id T of
   962            "" => None
   963          | name => if P free 
   964                    then (case get_splits sg name of
   965                            None => None
   966                          | Some (_,_,_,induct_thm)
   967                              => Some (mk_split_free_tac free induct_thm i))
   968                    else None)
   969      | split_free_tac _ _ _ = None;
   970 
   971     val split_frees_tacs = mapfilter (split_free_tac P i) frees;
   972    
   973     val simprocs = if has_rec goal then [record_split_simproc P] else [];
   974    
   975   in st |> (EVERY split_frees_tacs) 
   976            THEN (Simplifier.full_simp_tac (simpset addsimprocs simprocs) i)
   977   end handle Library.LIST _ => Seq.empty;
   978 end;
   979 
   980 
   981 (* record_split_tac *)
   982 (* splits all records in the goal, which are quantified by ! or !!. *)
   983 fun record_split_tac i st =
   984   let
   985     val sg = Thm.sign_of_thm st;
   986 
   987     val has_rec = exists_Const
   988       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   989           (s = "all" orelse s = "All") andalso is_recT T 
   990         | _ => false);
   991  
   992     val goal = Library.nth_elem (i - 1, Thm.prems_of st);   
   993 
   994     fun is_all t =
   995       (case t of (Const (quantifier, _)$_) =>
   996          quantifier = "All" orelse quantifier = "all"
   997        | _ => false);
   998  
   999   in if has_rec goal 
  1000      then Simplifier.full_simp_tac 
  1001            (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i st 
  1002      else Seq.empty
  1003   end handle Library.LIST _ => Seq.empty;
  1004 
  1005 (* wrapper *)
  1006 
  1007 val record_split_name = "record_split_tac";
  1008 val record_split_wrapper = (record_split_name, fn tac => record_split_tac ORELSE' tac);
  1009 
  1010 (** theory extender interface **)
  1011 
  1012 (* prepare arguments *)
  1013 
  1014 (*note: read_raw_typ avoids expanding type abbreviations*)
  1015 fun read_raw_parent sign s =
  1016   (case Sign.read_raw_typ (sign, K None) s handle TYPE (msg, _, _) => error msg of
  1017     Type (name, Ts) => (Ts, name)
  1018   | _ => error ("Bad parent record specification: " ^ quote s));
  1019 
  1020 fun read_typ sign (env, s) =
  1021   let
  1022     fun def_sort (x, ~1) = assoc (env, x)
  1023       | def_sort _ = None;
  1024     val T = Type.no_tvars (Sign.read_typ (sign, def_sort) s) handle TYPE (msg, _, _) => error msg;
  1025   in (Term.add_typ_tfrees (T, env), T) end;
  1026 
  1027 fun cert_typ sign (env, raw_T) =
  1028   let val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle TYPE (msg, _, _) => error msg
  1029   in (Term.add_typ_tfrees (T, env), T) end;
  1030 
  1031 (* attributes *)
  1032 
  1033 fun case_names_fields x = RuleCases.case_names ["fields"] x;
  1034 fun induct_type_global name = [case_names_fields, InductAttrib.induct_type_global name];
  1035 fun cases_type_global name = [case_names_fields, InductAttrib.cases_type_global name];
  1036 
  1037 (* tactics *)
  1038 
  1039 fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));
  1040 
  1041 (* do case analysis / induction according to rule on last parameter of ith subgoal 
  1042  * (or on s if there are no parameters); 
  1043  * Instatiation of record variable (and predicate) in rule is calculated to
  1044  * avoid problems with higher order unification. 
  1045  *)
  1046 
  1047 fun try_param_tac s rule i st =
  1048   let
  1049     val cert = cterm_of (Thm.sign_of_thm st);
  1050     val g = nth_elem (i - 1, prems_of st);
  1051     val params = Logic.strip_params g;
  1052     val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
  1053     val rule' = Thm.lift_rule (st, i) rule;
  1054     val (P, ys) = strip_comb (HOLogic.dest_Trueprop
  1055       (Logic.strip_assums_concl (prop_of rule')));
  1056     (* ca indicates if rule is a case analysis or induction rule *)
  1057     val (x, ca) = (case rev (drop (length params, ys)) of
  1058         [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
  1059           (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
  1060       | [x] => (head_of x, false));
  1061     val rule'' = cterm_instantiate (map (pairself cert) (case (rev params) of
  1062         [] => (case assoc (map dest_Free (term_frees (prop_of st)), s) of
  1063           None => sys_error "try_param_tac: no such variable"
  1064         | Some T => [(P, if ca then concl else lambda (Free (s, T)) concl),
  1065             (x, Free (s, T))])
  1066       | (_, T) :: _ => [(P, list_abs (params, if ca then concl
  1067           else incr_boundvars 1 (Abs (s, T, concl)))),
  1068         (x, list_abs (params, Bound 0))])) rule'
  1069   in compose_tac (false, rule'', nprems_of rule) i st end;
  1070 
  1071 
  1072 val record_definition_quick_and_dirty_sensitive = ref false;
  1073 
  1074 (* fun is crucial here; val would evaluate only once! *)
  1075 fun definition_prove_standard sg = 
  1076   if !record_definition_quick_and_dirty_sensitive
  1077   then quick_and_dirty_prove sg 
  1078   else Tactic.prove_standard sg;
  1079 
  1080 
  1081 fun extension_typedef name repT alphas thy =
  1082   let
  1083     val UNIV = HOLogic.mk_UNIV repT;
  1084 
  1085     val (thy',{set_def=Some def, Abs_induct = abs_induct, 
  1086                Abs_inject=abs_inject, Abs_inverse = abs_inverse,...}) =
  1087         thy |> setmp TypedefPackage.quiet_mode true
  1088            (TypedefPackage.add_typedef_i true None
  1089              (suffix ext_typeN (Sign.base_name name), alphas, Syntax.NoSyn) UNIV None
  1090              (Tactic.rtac UNIV_witness 1))
  1091     val rewrite_rule = Tactic.rewrite_rule [def, rec_UNIV_I, rec_True_simp];
  1092   in (thy',map rewrite_rule [abs_inject, abs_inverse, abs_induct])
  1093   end;
  1094 
  1095 fun extension_definition full name fields names alphas zeta moreT more vars thy = 
  1096   let  
  1097     val base = Sign.base_name;
  1098 
  1099     val fieldTs = (map snd fields);
  1100     val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) (alphas@[zeta]);
  1101     val extT_name = suffix ext_typeN name
  1102     val extT = Type (extT_name, alphas_zetaTs);
  1103     val repT = foldr1 HOLogic.mk_prodT (fieldTs@[moreT]);
  1104     val fields_more = fields@[(full moreN,moreT)];
  1105     val bfields_more = map (apfst base) fields_more;
  1106     val r = Free (rN,extT)
  1107     val len = length fields;
  1108     val idxms = 0 upto len;
  1109 
  1110     (* prepare declarations and definitions *)
  1111     
  1112     (*fields constructor*)
  1113     val ext_decl = (mk_extC (name,extT) (fieldTs@[moreT]));     
  1114     val ext_spec = Const ext_decl :== 
  1115          (foldr (uncurry lambda) 
  1116             (vars@[more],(mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more]))))) 
  1117     
  1118     (*destructors*) 
  1119     val dest_decls = map (mk_selC extT o (apfst (suffix ext_dest))) bfields_more;
  1120 
  1121     fun mk_dest_spec (i, (c,T)) =
  1122       let val snds = (funpow i HOLogic.mk_snd (mk_Rep name repT extT $ r))
  1123       in Const (mk_selC extT (suffix ext_dest c,T))
  1124          :== (lambda r (if i=len then snds else HOLogic.mk_fst snds))
  1125       end;
  1126     val dest_specs =
  1127       ListPair.map mk_dest_spec (idxms, fields_more);
  1128 
  1129     (* code generator data *)
  1130         (* Representation as nested pairs is revealed for codegeneration *)
  1131     val [rep_code,abs_code] = map (Codegen.parse_mixfix (K (Bound 0))) ["(_)","(_)"];
  1132     val ext_type_code = Codegen.parse_mixfix (K dummyT) "(_)";
  1133     
  1134     (* 1st stage: defs_thy *)
  1135     val (defs_thy, ([abs_inject, abs_inverse, abs_induct],ext_def::dest_defs)) =
  1136         thy 
  1137         |> extension_typedef name repT (alphas@[zeta])
  1138         |>> Codegen.assoc_consts_i 
  1139                [(mk_AbsN name,None,abs_code),
  1140                 (mk_RepN name,None,rep_code)]
  1141         |>> Codegen.assoc_types [(extT_name,ext_type_code)]
  1142         |>> Theory.add_consts_i (map Syntax.no_syn ((apfst base ext_decl)::dest_decls))
  1143         |>>> PureThy.add_defs_i false (map Thm.no_attributes (ext_spec::dest_specs))
  1144 
  1145     
  1146     (* prepare propositions *)
  1147 
  1148     val vars_more = vars@[more];
  1149     val named_vars_more = (names@[full moreN])~~vars_more;
  1150     val ext = list_comb (Const ext_decl,vars_more);
  1151     val s     = Free (rN, extT);
  1152     val P = Free (variant (map (fn (Free (x,_))=>x) vars_more) "P", extT-->HOLogic.boolT);
  1153     val C = Free (variant (map (fn (Free (x,_))=>x) vars_more) "C", HOLogic.boolT);
  1154 
  1155     val inject_prop =
  1156       let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more;
  1157       in All (map dest_Free (vars_more@vars_more')) 
  1158           ((HOLogic.eq_const extT $ 
  1159             list_comb (Const ext_decl,vars_more)$list_comb (Const ext_decl,vars_more')) 
  1160            ===
  1161            foldr1 HOLogic.mk_conj (map HOLogic.mk_eq (vars_more ~~ vars_more')))
  1162       end;
  1163     
  1164     val induct_prop =
  1165       (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s));
  1166 
  1167 
  1168     val cases_prop =
  1169       (All (map dest_Free vars_more) 
  1170         (Trueprop (HOLogic.mk_eq (s,ext)) ==> Trueprop C)) 
  1171       ==> Trueprop C;
  1172 
  1173     (*destructors*) 
  1174     val dest_conv_props =
  1175        map (fn (c, x as Free (_,T)) => mk_sel ext (suffix ext_dest c,T) === x) named_vars_more;
  1176 
  1177     val prove_standard = definition_prove_standard (Theory.sign_of defs_thy);
  1178     fun prove_simp simps =
  1179       let val tac = simp_all_tac HOL_ss simps
  1180       in fn prop => prove_standard [] [] prop (K tac) end;
  1181     
  1182     (* prove propositions *)
  1183 
  1184     fun inject_prf () = (prove_simp [ext_def,abs_inject,Pair_eq] inject_prop);
  1185     val inject = timeit_msg "record extension inject proof:" inject_prf;
  1186 
  1187     fun induct_prf () =
  1188       let val (assm, concl) = induct_prop
  1189       in prove_standard [] [assm] concl (fn prems =>
  1190            EVERY [try_param_tac rN abs_induct 1, 
  1191                   simp_tac (HOL_ss addsimps [split_paired_all]) 1,
  1192                   resolve_tac (map (rewrite_rule [ext_def]) prems) 1])
  1193       end;
  1194     val induct = timeit_msg "record extension induct proof:" induct_prf;
  1195 
  1196     fun cases_prf () =
  1197         prove_standard [] [] cases_prop (fn prems =>
  1198          EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
  1199                 try_param_tac rN induct 1,
  1200                 rtac impI 1,
  1201                 REPEAT (etac allE 1),
  1202                 etac mp 1,
  1203                 rtac refl 1])
  1204     val cases = timeit_msg "record extension cases proof:" cases_prf;
  1205 	
  1206     fun dest_convs_prf () = map (prove_simp 
  1207                            ([ext_def,abs_inverse]@Pair_sel_convs@dest_defs)) dest_conv_props;
  1208     val dest_convs = timeit_msg "record extension dest_convs proof:" dest_convs_prf;
  1209 
  1210     val (thm_thy,([inject',induct',cases'],[dest_convs'])) =
  1211       defs_thy 
  1212       |> (PureThy.add_thms o map Thm.no_attributes) 
  1213            [("ext_inject", inject),
  1214             ("ext_induct", induct),
  1215             ("ext_cases", cases)]
  1216       |>>> (PureThy.add_thmss o map Thm.no_attributes)
  1217               [("dest_convs",dest_convs)] 
  1218 
  1219   in (thm_thy,extT,induct',inject',dest_convs')
  1220   end;
  1221    
  1222 fun chunks []      []   = []
  1223   | chunks []      xs   = [xs]
  1224   | chunks (l::ls) xs  = take (l,xs)::chunks ls (drop (l,xs));
  1225  
  1226 fun chop_last [] = error "last: list should not be empty"
  1227   | chop_last [x] = ([],x)
  1228   | chop_last (x::xs) = let val (tl,l) = chop_last xs in (x::tl,l) end;
  1229      	
  1230 fun subst_last s []      = error "subst_last: list should not be empty"
  1231   | subst_last s ([x])   = [s]
  1232   | subst_last s (x::xs) = (x::subst_last s xs);
  1233 
  1234 (* mk_recordT builds up the record type from the current extension tpye extT and a list
  1235  * of parent extensions, starting with the root of the record hierarchy 
  1236 *) 
  1237 fun mk_recordT extT parent_exts = 
  1238     foldr (fn ((parent,Ts),T) => Type (parent, subst_last T Ts)) (parent_exts,extT);
  1239 
  1240 (* record_definition *)
  1241 fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy = 
  1242   (* smlnj needs type annotation of parents *)
  1243   let
  1244     val sign = Theory.sign_of thy;
  1245 
  1246     val alphas = map fst args;
  1247     val name = Sign.full_name sign bname;
  1248     val full = Sign.full_name_path sign bname;
  1249     val base = Sign.base_name;
  1250 
  1251     val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
  1252 
  1253     val parent_fields = flat (map #fields parents);
  1254     val parent_chunks = map (length o #fields) parents;
  1255     val parent_names = map fst parent_fields;
  1256     val parent_types = map snd parent_fields;
  1257     val parent_fields_len = length parent_fields;
  1258     val parent_variants = variantlist (map base parent_names, [moreN, rN, rN ^ "'"]);
  1259     val parent_vars = ListPair.map Free (parent_variants, parent_types);
  1260     val parent_len = length parents;
  1261     val parents_idx = (map #name parents) ~~ (0 upto (parent_len - 1));
  1262 
  1263     val fields = map (apfst full) bfields;
  1264     val names = map fst fields;
  1265     val extN = full bname;
  1266     val types = map snd fields;
  1267     val alphas_fields = foldr add_typ_tfree_names (types,[]);
  1268     val alphas_ext = alphas inter alphas_fields; 
  1269     val len = length fields;
  1270     val variants = variantlist (map fst bfields, moreN::rN::rN ^ "'"::parent_variants);
  1271     val vars = ListPair.map Free (variants, types);
  1272     val named_vars = names ~~ vars;
  1273     val idxs = 0 upto (len - 1);
  1274     val idxms = 0 upto len;
  1275 
  1276     val all_fields = parent_fields @ fields;
  1277     val all_names = parent_names @ names;
  1278     val all_types = parent_types @ types;
  1279     val all_len = parent_fields_len + len;
  1280     val all_variants = parent_variants @ variants;
  1281     val all_vars = parent_vars @ vars;
  1282     val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
  1283 
  1284 
  1285     val zeta = variant alphas "'z";
  1286     val moreT = TFree (zeta, HOLogic.typeS);
  1287     val more = Free (moreN, moreT);
  1288     val full_moreN = full moreN;
  1289     val bfields_more = bfields @ [(moreN,moreT)];
  1290     val fields_more = fields @ [(full_moreN,moreT)];
  1291     val vars_more = vars @ [more];
  1292     val named_vars_more = named_vars @[(full_moreN,more)];
  1293     val all_vars_more = all_vars @ [more];
  1294     val all_named_vars_more = all_named_vars @ [(full_moreN,more)];
  1295    
  1296     (* 1st stage: extension_thy *)
  1297 	
  1298     val (extension_thy,extT,ext_induct,ext_inject,ext_dest_convs) =
  1299       thy
  1300       |> Theory.add_path bname
  1301       |> extension_definition full extN fields names alphas_ext zeta moreT more vars;
  1302 
  1303    
  1304     val Type extension_scheme = extT;
  1305     val extension_name = unsuffix ext_typeN (fst extension_scheme);
  1306     val extension = let val (n,Ts) = extension_scheme in (n,subst_last HOLogic.unitT Ts) end; 
  1307     val extension_names = 
  1308          (map ((unsuffix ext_typeN) o fst o #extension) parents) @ [extN];
  1309     val extension_id = foldl (op ^) ("",extension_names);
  1310 
  1311  
  1312     fun rec_schemeT n = mk_recordT extT (map #extension (prune n parents));
  1313     val rec_schemeT0 = rec_schemeT 0;
  1314 
  1315     fun recT n = 
  1316       let val (c,Ts) = extension
  1317       in mk_recordT (Type (c,subst_last HOLogic.unitT Ts))(map #extension (prune n parents))
  1318       end;
  1319     val recT0 = recT 0;
  1320     
  1321     fun mk_rec args n =
  1322       let val (args',more) = chop_last args;
  1323 	  fun mk_ext' (((name,T),args),more) = mk_ext (name,T) (args@[more]);
  1324           fun build Ts = 
  1325            foldr mk_ext' (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args')),more) 
  1326       in 
  1327         if more = HOLogic.unit 
  1328         then build (map recT (0 upto parent_len)) 
  1329         else build (map rec_schemeT (0 upto parent_len))
  1330       end;
  1331    
  1332     val r_rec0 = mk_rec all_vars_more 0;
  1333     val r_rec_unit0 = mk_rec (all_vars@[HOLogic.unit]) 0;
  1334 
  1335     fun r n = Free (rN, rec_schemeT n)
  1336     val r0 = r 0;
  1337     fun r_unit n = Free (rN, recT n)
  1338     val r_unit0 = r_unit 0;
  1339 
  1340     (* prepare print translation functions *)
  1341     val field_tr's =
  1342       print_translation (distinct (flat (map NameSpace.accesses' (full_moreN :: names))));
  1343 
  1344     val adv_ext_tr's =
  1345     let
  1346       val trnames = NameSpace.accesses' extN;
  1347     in map (gen_record_tr') trnames end;
  1348 
  1349     val adv_record_type_abbr_tr's =
  1350       let val trnames = NameSpace.accesses' (hd extension_names);
  1351           val lastExt = (unsuffix ext_typeN (fst extension));
  1352       in map (gen_record_type_abbr_tr' bname alphas zeta lastExt rec_schemeT0) trnames
  1353       end;
  1354 
  1355     val adv_record_type_tr's =
  1356       let val trnames = if parent_len > 0 then NameSpace.accesses' extN else [];
  1357                         (* avoid conflict with adv_record_type_abbr_tr's *)
  1358       in map (gen_record_type_tr') trnames
  1359       end;
  1360 
  1361     
  1362     (* prepare declarations *)
  1363 
  1364     val sel_decls = map (mk_selC rec_schemeT0) bfields_more;
  1365     val upd_decls = map (mk_updC rec_schemeT0) bfields_more;
  1366     val make_decl = (makeN, all_types ---> recT0);
  1367     val fields_decl = (fields_selN, types ---> Type extension); 
  1368     val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0);
  1369     val truncate_decl = (truncateN, rec_schemeT0 --> recT0);
  1370 
  1371     (* prepare definitions *)
  1372     
  1373     fun parent_more s = 
  1374          if null parents then s 
  1375          else mk_sel s (NameSpace.append (#name (hd (rev parents))) moreN, extT);
  1376 
  1377     fun parent_more_upd v s =
  1378       if null parents then v 
  1379       else let val mp = (NameSpace.append (#name (hd (rev parents))) moreN);
  1380            in mk_upd mp v s end;
  1381    
  1382     (*record (scheme) type abbreviation*)
  1383     val recordT_specs =
  1384       [(suffix schemeN bname, alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
  1385         (bname, alphas, recT0, Syntax.NoSyn)];	
  1386 
  1387     (*selectors*) 
  1388     fun mk_sel_spec (c,T) = 
  1389 	 Const (mk_selC rec_schemeT0 (c,T)) 
  1390           :== (lambda r0 (Const (mk_selC extT (suffix ext_dest c,T))$parent_more r0));
  1391     val sel_specs = map mk_sel_spec fields_more;
  1392 
  1393     (*updates*)
  1394     fun mk_upd_spec (c,T) =
  1395       let 
  1396         val args = map (fn (n,nT) => if n=c then Free (base c,T) else (mk_sel r0 (n,nT))) 
  1397                        fields_more;
  1398         val new = mk_ext (extN,extT) args; 
  1399       in Const (mk_updC rec_schemeT0 (c,T))
  1400           :== (lambda (Free (base c,T)) (lambda r0 (parent_more_upd new r0)))
  1401       end;
  1402     val upd_specs = map mk_upd_spec fields_more;
  1403 
  1404     (*derived operations*)
  1405     val make_spec = Const (full makeN, all_types ---> recT0) $$ all_vars :==
  1406       mk_rec (all_vars @ [HOLogic.unit]) 0;
  1407     val fields_spec = Const (full fields_selN, types ---> Type extension) $$ vars :==
  1408       mk_rec (all_vars @ [HOLogic.unit]) parent_len;
  1409     val extend_spec = 
  1410       Const (full extendN, recT0-->moreT-->rec_schemeT0) $ r_unit0 $ more :==
  1411       mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
  1412     val truncate_spec = Const (full truncateN, rec_schemeT0 --> recT0) $ r0 :==
  1413       mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
  1414 
  1415     (* 2st stage: defs_thy *)
  1416  
  1417     val (defs_thy,((sel_defs,upd_defs),derived_defs)) = 
  1418         extension_thy
  1419         |> Theory.add_trfuns 
  1420             ([],[],field_tr's, [])
  1421         |> Theory.add_advanced_trfuns 
  1422             ([],[],adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's,[])
  1423 
  1424         |> Theory.parent_path
  1425         |> Theory.add_tyabbrs_i recordT_specs
  1426         |> Theory.add_path bname
  1427         |> Theory.add_consts_i
  1428             (map2 (fn ((x, T), mx) => (x, T, mx)) (sel_decls, field_syntax @ [Syntax.NoSyn]))
  1429         |> (Theory.add_consts_i o map Syntax.no_syn) 
  1430             (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
  1431         |> (PureThy.add_defs_i false o map Thm.no_attributes) sel_specs
  1432         |>>> (PureThy.add_defs_i false o map Thm.no_attributes) upd_specs
  1433 	|>>> (PureThy.add_defs_i false o map Thm.no_attributes)
  1434                [make_spec, fields_spec, extend_spec, truncate_spec];
  1435         
  1436 
  1437     (* prepare propositions *)
  1438     val P = Free (variant all_variants "P", rec_schemeT0-->HOLogic.boolT);
  1439     val C = Free (variant all_variants "C", HOLogic.boolT);    
  1440     val P_unit = Free (variant all_variants "P", recT0-->HOLogic.boolT);
  1441 
  1442     (*selectors*) 
  1443     val sel_conv_props =
  1444        map (fn (c, x as Free (_,T)) => mk_sel r_rec0 (c,T) === x) named_vars_more;
  1445 
  1446     (*updates*) 
  1447     fun mk_upd_prop (i,(c,T)) =
  1448       let val x' = Free (variant all_variants (base c ^ "'"),T) 
  1449           val args' = nth_update x' (parent_fields_len + i, all_vars_more)
  1450       in mk_upd c x' r_rec0 === mk_rec args' 0  end;
  1451     val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
  1452 
  1453     (*induct*)
  1454     val induct_scheme_prop =
  1455       All (map dest_Free all_vars_more) (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0);
  1456     val induct_prop =  
  1457       (All (map dest_Free all_vars) (Trueprop (P_unit $ r_rec_unit0)),
  1458        Trueprop (P_unit $ r_unit0));
  1459 
  1460     (*surjective*)
  1461     val surjective_prop =
  1462       let val args = map (fn (c,Free (_,T)) => mk_sel r0 (c,T)) all_named_vars_more
  1463       in r0 === mk_rec args 0 end;
  1464 
  1465     (*cases*)
  1466     val cases_scheme_prop =
  1467       (All (map dest_Free all_vars_more) 
  1468         (Trueprop (HOLogic.mk_eq (r0,r_rec0)) ==> Trueprop C)) 
  1469       ==> Trueprop C;
  1470 
  1471     val cases_prop =
  1472       (All (map dest_Free all_vars) 
  1473         (Trueprop (HOLogic.mk_eq (r_unit0,r_rec_unit0)) ==> Trueprop C)) 
  1474        ==> Trueprop C;
  1475 
  1476     (*split*)
  1477     val split_meta_prop =
  1478       let val P = Free (variant all_variants "P", rec_schemeT0-->Term.propT) in
  1479         Logic.mk_equals 
  1480          (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
  1481       end; 
  1482 
  1483     val split_object_prop =
  1484       let fun ALL vs t = foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) (vs,t)
  1485       in (ALL [dest_Free r0] (P $ r0)) === (ALL (map dest_Free all_vars_more) (P $ r_rec0))
  1486       end;
  1487 
  1488 
  1489     val split_ex_prop =
  1490       let fun EX vs t = foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) (vs,t)
  1491       in (EX [dest_Free r0] (P $ r0)) === (EX (map dest_Free all_vars_more) (P $ r_rec0))
  1492       end;
  1493 
  1494     (*equality*)
  1495     val equality_prop =
  1496       let 
  1497 	val s' = Free (rN ^ "'", rec_schemeT0)
  1498         fun mk_sel_eq (c,Free (_,T)) =  mk_sel r0 (c,T) === mk_sel s' (c,T) 
  1499         val seleqs = map mk_sel_eq all_named_vars_more
  1500       in All (map dest_Free [r0,s']) (Logic.list_implies (seleqs,r0 === s')) end;
  1501 
  1502     (* 3rd stage: thms_thy *)
  1503 
  1504     val prove_standard = definition_prove_standard (Theory.sign_of defs_thy);
  1505     fun prove_simp ss simps =
  1506       let val tac = simp_all_tac ss simps
  1507       in fn prop => prove_standard [] [] prop (K tac) end;
  1508 
  1509     val ss = get_simpset (sign_of defs_thy);
  1510 
  1511     fun sel_convs_prf () = map (prove_simp ss 
  1512                            (sel_defs@ext_dest_convs)) sel_conv_props;
  1513     val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
  1514 
  1515     fun upd_convs_prf () = map (prove_simp ss (sel_convs@upd_defs)) 
  1516                              upd_conv_props;
  1517     val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
  1518 
  1519     val parent_induct = if null parents then [] else [#induct (hd (rev parents))];
  1520 
  1521     fun induct_scheme_prf () = prove_standard [] [] induct_scheme_prop (fn prems =>
  1522           (EVERY [if null parent_induct 
  1523                   then all_tac else try_param_tac rN (hd parent_induct) 1,
  1524                   try_param_tac rN ext_induct 1,
  1525                   asm_simp_tac HOL_basic_ss 1]));
  1526     val induct_scheme = timeit_msg "record induct_scheme proof:" induct_scheme_prf;
  1527 
  1528     fun induct_prf () =
  1529       let val (assm, concl) = induct_prop;
  1530       in
  1531         prove_standard [] [assm] concl (fn prems =>
  1532           try_param_tac rN induct_scheme 1
  1533           THEN try_param_tac "more" unit_induct 1
  1534           THEN resolve_tac prems 1)
  1535       end;
  1536     val induct = timeit_msg "record induct proof:" induct_prf;
  1537 
  1538     fun surjective_prf () = 
  1539       prove_standard [] [] surjective_prop (fn prems =>
  1540           (EVERY [try_param_tac rN induct_scheme 1,
  1541                   simp_tac (ss addsimps sel_convs) 1]))
  1542     val surjective = timeit_msg "record surjective proof:" surjective_prf;
  1543 
  1544     fun cases_scheme_prf () =
  1545         prove_standard [] [] cases_scheme_prop (fn prems =>
  1546          EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
  1547                try_param_tac rN induct_scheme 1,
  1548                rtac impI 1,
  1549                REPEAT (etac allE 1),
  1550                etac mp 1,
  1551                rtac refl 1])
  1552     val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
  1553 
  1554     fun cases_prf () =
  1555       prove_standard [] [] cases_prop  (fn _ =>
  1556         try_param_tac rN cases_scheme 1
  1557         THEN simp_all_tac HOL_basic_ss [unit_all_eq1]);
  1558     val cases = timeit_msg "record cases proof:" cases_prf;
  1559 
  1560     fun split_meta_prf () =
  1561         prove_standard [] [] split_meta_prop (fn prems =>
  1562          EVERY [rtac equal_intr_rule 1,
  1563                   rtac meta_allE 1, etac triv_goal 1, atac 1,
  1564                 rtac (prop_subst OF [surjective]) 1,
  1565                 REPEAT (EVERY [rtac meta_allE 1, etac triv_goal 1, etac thin_rl 1]),
  1566                 atac 1]);
  1567     val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
  1568 
  1569     fun split_object_prf () =
  1570         prove_standard [] [] split_object_prop (fn prems =>
  1571          EVERY [rtac iffI 1, 
  1572                 REPEAT (rtac allI 1), etac allE 1, atac 1,
  1573                 rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]);
  1574     val split_object = timeit_msg "record split_object proof:" split_object_prf;
  1575 
  1576 
  1577     fun split_ex_prf () = 
  1578         prove_standard [] [] split_ex_prop (fn prems =>
  1579           EVERY [rtac iffI 1,
  1580                    etac exE 1,
  1581                    simp_tac (HOL_basic_ss addsimps [split_meta]) 1,
  1582                    REPEAT (rtac exI 1),
  1583                    atac 1,
  1584                  REPEAT (etac exE 1),
  1585                  rtac exI 1,
  1586                  atac 1]);
  1587     val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
  1588 
  1589     fun equality_tac thms = 
  1590       let val (s'::s::eqs) = rev thms;
  1591           val ss' = ss addsimps (s'::s::sel_convs);
  1592           val eqs' = map (simplify ss') eqs;
  1593       in simp_tac (HOL_basic_ss addsimps (s'::s::eqs')) 1 end;
  1594  
  1595    fun equality_prf () = prove_standard [] [] equality_prop (fn _ =>
  1596       fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
  1597         st |> (res_inst_tac [(rN, s)] cases_scheme 1
  1598         THEN res_inst_tac [(rN, s')] cases_scheme 1
  1599         THEN (METAHYPS equality_tac 1)) 
  1600              (* simp_all_tac ss (sel_convs) would also work but is less efficient *)
  1601       end);                              
  1602      val equality = timeit_msg "record equality proof':" equality_prf;
  1603 
  1604     val (thms_thy,(([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'],
  1605                     derived_defs'],
  1606                    [surjective',equality']),[induct_scheme',induct',cases_scheme',cases'])) =
  1607       defs_thy
  1608       |> (PureThy.add_thmss o map Thm.no_attributes)
  1609          [("select_convs", sel_convs),
  1610           ("update_convs", upd_convs),
  1611           ("select_defs", sel_defs),
  1612           ("update_defs", upd_defs),
  1613           ("splits", [split_meta,split_object,split_ex]),
  1614           ("defs", derived_defs)]
  1615       |>>> (PureThy.add_thms o map Thm.no_attributes)
  1616           [("surjective", surjective),
  1617            ("equality", equality)]
  1618       |>>> PureThy.add_thms 
  1619         [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
  1620          (("induct", induct), induct_type_global name),
  1621          (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
  1622          (("cases", cases), cases_type_global name)];
  1623 
  1624 
  1625     val sel_upd_simps = sel_convs' @ upd_convs';
  1626     val iffs = [ext_inject]
  1627     val final_thy =
  1628       thms_thy
  1629       |> (#1 oo PureThy.add_thmss)
  1630           [(("simps", sel_upd_simps), [Simplifier.simp_add_global]),
  1631            (("iffs",iffs), [iff_add_global])]
  1632       |> put_record name (make_record_info args parent fields extension induct_scheme') 
  1633       |> put_sel_upd (names @ [full_moreN]) sel_upd_simps
  1634       |> add_record_equalities extension_id equality'
  1635       |> add_record_splits extension_id (split_meta',split_object',split_ex',induct_scheme')
  1636       |> add_extfields extension_name (fields @ [(full_moreN,moreT)]) 
  1637       |> add_fieldext (extension_name,snd extension) (names @ [full_moreN]) 
  1638       |> Theory.parent_path;
  1639 
  1640   in final_thy
  1641   end;
  1642 
  1643 (* add_record *)
  1644 
  1645 (*we do all preparations and error checks here, deferring the real
  1646   work to record_definition*)
  1647 fun gen_add_record prep_typ prep_raw_parent (params, bname) raw_parent raw_fields thy =
  1648   let
  1649     val _ = Theory.requires thy "Record" "record definitions"; 
  1650     val sign = Theory.sign_of thy;
  1651     val _ = message ("Defining record " ^ quote bname ^ " ...");
  1652 
  1653 
  1654     (* parents *)
  1655 
  1656     fun prep_inst T = snd (cert_typ sign ([], T));
  1657 
  1658     val parent = apsome (apfst (map prep_inst) o prep_raw_parent sign) raw_parent
  1659       handle ERROR => error ("The error(s) above in parent record specification");
  1660     val parents = add_parents thy parent [];
  1661 
  1662     val init_env =
  1663       (case parent of
  1664         None => []
  1665       | Some (types, _) => foldr Term.add_typ_tfrees (types, []));
  1666 
  1667 
  1668     (* fields *)
  1669 
  1670     fun prep_field (env, (c, raw_T, mx)) =
  1671       let val (env', T) = prep_typ sign (env, raw_T) handle ERROR =>
  1672         error ("The error(s) above occured in field " ^ quote c)
  1673       in (env', (c, T, mx)) end;
  1674 
  1675     val (envir, bfields) = foldl_map prep_field (init_env, raw_fields);
  1676     val envir_names = map fst envir;
  1677 
  1678 
  1679     (* args *)
  1680 
  1681     val defaultS = Sign.defaultS sign;
  1682     val args = map (fn x => (x, if_none (assoc (envir, x)) defaultS)) params;
  1683 
  1684 
  1685     (* errors *)
  1686 
  1687     val name = Sign.full_name sign bname;
  1688     val err_dup_record =  
  1689       if is_none (get_record thy name) then []
  1690       else ["Duplicate definition of record " ^ quote name];
  1691 
  1692     val err_dup_parms =
  1693       (case duplicates params of
  1694         [] => []
  1695       | dups => ["Duplicate parameter(s) " ^ commas dups]);
  1696 
  1697     val err_extra_frees =
  1698       (case gen_rems (op =) (envir_names, params) of
  1699         [] => []
  1700       | extras => ["Extra free type variable(s) " ^ commas extras]);
  1701 
  1702     val err_no_fields = if null bfields then ["No fields present"] else [];
  1703 
  1704     val err_dup_fields =
  1705       (case duplicates (map #1 bfields) of
  1706         [] => []
  1707       | dups => ["Duplicate field(s) " ^ commas_quote dups]);
  1708 
  1709     val err_bad_fields =
  1710       if forall (not_equal moreN o #1) bfields then []
  1711       else ["Illegal field name " ^ quote moreN];
  1712 
  1713     val err_dup_sorts =
  1714       (case duplicates envir_names of
  1715         [] => []
  1716       | dups => ["Inconsistent sort constraints for " ^ commas dups]);
  1717 
  1718     val errs =
  1719       err_dup_record @ err_dup_parms @ err_extra_frees @ err_no_fields @
  1720       err_dup_fields @ err_bad_fields @ err_dup_sorts;
  1721   in
  1722     if null errs then () else error (cat_lines errs)  ;
  1723     thy |> record_definition (args, bname) parent parents bfields
  1724   end
  1725   handle ERROR => error ("Failed to define record " ^ quote bname);
  1726 
  1727 val add_record = gen_add_record read_typ read_raw_parent;
  1728 val add_record_i = gen_add_record cert_typ (K I);
  1729 
  1730 (* setup theory *)
  1731 
  1732 val setup =
  1733  [RecordsData.init,
  1734   Theory.add_trfuns ([], parse_translation, [], []),
  1735   Theory.add_advanced_trfuns ([], adv_parse_translation, [], []),   
  1736   Simplifier.change_simpset_of Simplifier.addsimprocs
  1737     [record_simproc, record_upd_simproc, record_eq_simproc]];
  1738 
  1739 (* outer syntax *)
  1740 
  1741 local structure P = OuterParse and K = OuterSyntax.Keyword in
  1742 
  1743 val record_decl =
  1744   P.type_args -- P.name --
  1745     (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
  1746 
  1747 val recordP =
  1748   OuterSyntax.command "record" "define extensible record" K.thy_decl  
  1749     (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z)));  
  1750 
  1751 val _ = OuterSyntax.add_parsers [recordP];
  1752 
  1753 end;
  1754 
  1755 end;
  1756 
  1757 structure BasicRecordPackage: BASIC_RECORD_PACKAGE = RecordPackage;
  1758 open BasicRecordPackage;