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