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