src/HOL/Tools/record.ML
author Thomas Sewell <tsewell@nicta.com.au>
Thu Sep 10 16:38:18 2009 +1000 (2009-09-10)
changeset 32745 192d58483fdf
parent 32744 50406c4951d9
child 32748 887c68b70f7d
permissions -rw-r--r--
Simplification of various aspects of the IsTuple component
of the new record package. Extensive documentation added in
IsTuple.thy - it should now be possible to figure out what's
going on from the sources supplied.
     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             ("ext_def", ext_def)]
  1726 
  1727   in (thm_thy,extT,induct',inject',split_meta',ext_def')
  1728   end;
  1729 
  1730 fun chunks []      []   = []
  1731   | chunks []      xs   = [xs]
  1732   | chunks (l::ls) xs  = Library.take (l,xs)::chunks ls (Library.drop (l,xs));
  1733 
  1734 fun chop_last [] = error "last: list should not be empty"
  1735   | chop_last [x] = ([],x)
  1736   | chop_last (x::xs) = let val (tl,l) = chop_last xs in (x::tl,l) end;
  1737 
  1738 fun subst_last s []      = error "subst_last: list should not be empty"
  1739   | subst_last s ([x])   = [s]
  1740   | subst_last s (x::xs) = (x::subst_last s xs);
  1741 
  1742 (* mk_recordT builds up the record type from the current extension tpye extT and a list
  1743  * of parent extensions, starting with the root of the record hierarchy
  1744 *)
  1745 fun mk_recordT extT =
  1746     fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT;
  1747 
  1748 
  1749 
  1750 fun obj_to_meta_all thm =
  1751   let
  1752     fun E thm = case (SOME (spec OF [thm]) handle THM _ => NONE) of
  1753                   SOME thm' => E thm'
  1754                 | NONE => thm;
  1755     val th1 = E thm;
  1756     val th2 = Drule.forall_intr_vars th1;
  1757   in th2 end;
  1758 
  1759 fun meta_to_obj_all thm =
  1760   let
  1761     val thy = Thm.theory_of_thm thm;
  1762     val prop = Thm.prop_of thm;
  1763     val params = Logic.strip_params prop;
  1764     val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop);
  1765     val ct = cterm_of thy
  1766       (HOLogic.mk_Trueprop (HOLogic.list_all (params, concl)));
  1767     val thm' = Seq.hd (REPEAT (rtac allI 1) (Thm.trivial ct));
  1768   in
  1769     Thm.implies_elim thm' thm
  1770   end;
  1771 
  1772 
  1773 
  1774 (* record_definition *)
  1775 
  1776 fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy =
  1777   let
  1778     val external_names = NameSpace.external_names (Sign.naming_of thy);
  1779 
  1780     val alphas = map fst args;
  1781     val name = Sign.full_bname thy bname;
  1782     val full = Sign.full_bname_path thy bname;
  1783     val base = Long_Name.base_name;
  1784 
  1785     val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
  1786 
  1787     val parent_fields = List.concat (map #fields parents);
  1788     val parent_chunks = map (length o #fields) parents;
  1789     val parent_names = map fst parent_fields;
  1790     val parent_types = map snd parent_fields;
  1791     val parent_fields_len = length parent_fields;
  1792     val parent_variants = Name.variant_list [moreN, rN, rN ^ "'", wN] (map base parent_names);
  1793     val parent_vars = ListPair.map Free (parent_variants, parent_types);
  1794     val parent_len = length parents;
  1795     val parents_idx = (map #name parents) ~~ (0 upto (parent_len - 1));
  1796 
  1797     val fields = map (apfst full) bfields;
  1798     val names = map fst fields;
  1799     val extN = full bname;
  1800     val types = map snd fields;
  1801     val alphas_fields = List.foldr OldTerm.add_typ_tfree_names [] types;
  1802     val alphas_ext = alphas inter alphas_fields;
  1803     val len = length fields;
  1804     val variants =
  1805       Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants) (map fst bfields);
  1806     val vars = ListPair.map Free (variants, types);
  1807     val named_vars = names ~~ vars;
  1808     val idxs = 0 upto (len - 1);
  1809     val idxms = 0 upto len;
  1810 
  1811     val all_fields = parent_fields @ fields;
  1812     val all_names = parent_names @ names;
  1813     val all_types = parent_types @ types;
  1814     val all_len = parent_fields_len + len;
  1815     val all_variants = parent_variants @ variants;
  1816     val all_vars = parent_vars @ vars;
  1817     val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
  1818 
  1819 
  1820     val zeta = Name.variant alphas "'z";
  1821     val moreT = TFree (zeta, HOLogic.typeS);
  1822     val more = Free (moreN, moreT);
  1823     val full_moreN = full moreN;
  1824     val bfields_more = bfields @ [(moreN,moreT)];
  1825     val fields_more = fields @ [(full_moreN,moreT)];
  1826     val vars_more = vars @ [more];
  1827     val named_vars_more = named_vars @[(full_moreN,more)];
  1828     val all_vars_more = all_vars @ [more];
  1829     val all_named_vars_more = all_named_vars @ [(full_moreN,more)];
  1830 
  1831     (* 1st stage: extension_thy *)
  1832     val (extension_thy,extT,ext_induct,ext_inject,ext_split,ext_def) =
  1833       thy
  1834       |> Sign.add_path bname
  1835       |> extension_definition full extN fields names alphas_ext zeta moreT more vars;
  1836 
  1837     val _ = timing_msg "record preparing definitions";
  1838     val Type extension_scheme = extT;
  1839     val extension_name = unsuffix ext_typeN (fst extension_scheme);
  1840     val extension = let val (n,Ts) = extension_scheme in (n,subst_last HOLogic.unitT Ts) end;
  1841     val extension_names =
  1842          (map ((unsuffix ext_typeN) o fst o #extension) parents) @ [extN];
  1843     val extension_id = Library.foldl (op ^) ("",extension_names);
  1844 
  1845 
  1846     fun rec_schemeT n = mk_recordT (map #extension (prune n parents)) extT;
  1847     val rec_schemeT0 = rec_schemeT 0;
  1848 
  1849     fun recT n =
  1850       let val (c,Ts) = extension
  1851       in mk_recordT (map #extension (prune n parents)) (Type (c,subst_last HOLogic.unitT Ts))
  1852       end;
  1853     val recT0 = recT 0;
  1854 
  1855     fun mk_rec args n =
  1856       let val (args',more) = chop_last args;
  1857           fun mk_ext' (((name,T),args),more) = mk_ext (name,T) (args@[more]);
  1858           fun build Ts =
  1859            List.foldr mk_ext' more (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args')))
  1860       in
  1861         if more = HOLogic.unit
  1862         then build (map recT (0 upto parent_len))
  1863         else build (map rec_schemeT (0 upto parent_len))
  1864       end;
  1865 
  1866     val r_rec0 = mk_rec all_vars_more 0;
  1867     val r_rec_unit0 = mk_rec (all_vars@[HOLogic.unit]) 0;
  1868     val r_rec0_Vars = let
  1869         fun to_Var (Free (c, T)) = Var ((c, 0), T);
  1870       in mk_rec (map to_Var all_vars_more) 0 end;
  1871 
  1872     fun r n = Free (rN, rec_schemeT n)
  1873     val r0 = r 0;
  1874     fun r_unit n = Free (rN, recT n)
  1875     val r_unit0 = r_unit 0;
  1876     val w = Free (wN, rec_schemeT 0)
  1877 
  1878     (* prepare print translation functions *)
  1879     val field_tr's =
  1880       print_translation (distinct (op =) (maps external_names (full_moreN :: names)));
  1881 
  1882     val adv_ext_tr's =
  1883     let
  1884       val trnames = external_names extN;
  1885     in map (gen_record_tr') trnames end;
  1886 
  1887     val adv_record_type_abbr_tr's =
  1888       let val trnames = external_names (hd extension_names);
  1889           val lastExt = unsuffix ext_typeN (fst extension);
  1890       in map (gen_record_type_abbr_tr' name alphas zeta lastExt rec_schemeT0) trnames
  1891       end;
  1892 
  1893     val adv_record_type_tr's =
  1894       let val trnames = if parent_len > 0 then external_names extN else [];
  1895                         (* avoid conflict with adv_record_type_abbr_tr's *)
  1896       in map (gen_record_type_tr') trnames
  1897       end;
  1898 
  1899 
  1900     (* prepare declarations *)
  1901 
  1902     val sel_decls = map (mk_selC rec_schemeT0) bfields_more;
  1903     val upd_decls = map (mk_updC updateN rec_schemeT0) bfields_more;
  1904     val make_decl = (makeN, all_types ---> recT0);
  1905     val fields_decl = (fields_selN, types ---> Type extension);
  1906     val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0);
  1907     val truncate_decl = (truncateN, rec_schemeT0 --> recT0);
  1908 
  1909     (* prepare definitions *)
  1910 
  1911     fun parent_more s =
  1912          if null parents then s
  1913          else mk_sel s (Long_Name.qualify (#name (List.last parents)) moreN, extT);
  1914 
  1915     fun parent_more_upd v s =
  1916       if null parents then v$s
  1917       else let val mp = Long_Name.qualify (#name (List.last parents)) moreN;
  1918            in mk_upd updateN mp v s end;
  1919 
  1920     (*record (scheme) type abbreviation*)
  1921     val recordT_specs =
  1922       [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
  1923         (Binding.name bname, alphas, recT0, Syntax.NoSyn)];
  1924 
  1925     val ext_defs = ext_def :: map #extdef parents;
  1926     val intros_tac = IsTupleSupport.istuple_intros_tac extension_thy;
  1927 
  1928     (* Theorems from the istuple intros.
  1929        This is complex enough to deserve a full comment.
  1930        By unfolding ext_defs from r_rec0 we create a tree of constructor
  1931        calls (many of them Pair, but others as well). The introduction
  1932        rules for update_accessor_eq_assist can unify two different ways
  1933        on these constructors. If we take the complete result sequence of
  1934        running a the introduction tactic, we get one theorem for each upd/acc
  1935        pair, from which we can derive the bodies of our selector and
  1936        updator and their convs. *)
  1937     fun get_access_update_thms () = let
  1938         val cterm_rec = cterm_of extension_thy r_rec0;
  1939         val cterm_vrs = cterm_of extension_thy r_rec0_Vars;
  1940         val insts     = [("v", cterm_rec), ("v'", cterm_vrs)];
  1941         val init_thm  = named_cterm_instantiate insts updacc_eq_triv;
  1942         val terminal  = rtac updacc_eq_idI 1 THEN rtac refl 1;
  1943         val tactic    = simp_tac (HOL_basic_ss addsimps ext_defs) 1
  1944                         THEN REPEAT (intros_tac 1 ORELSE terminal);
  1945         val updaccs   = Seq.list_of (tactic init_thm);
  1946       in
  1947         (updaccs RL [updacc_accessor_eqE],
  1948          updaccs RL [updacc_updator_eqE],
  1949          updaccs RL [updacc_cong_from_eq])
  1950       end;
  1951     val (accessor_thms, updator_thms, upd_acc_cong_assists) =
  1952        timeit_msg "record getting tree access/updates:" get_access_update_thms;
  1953 
  1954     fun lastN xs = List.drop (xs, parent_fields_len);
  1955 
  1956     (*selectors*)
  1957     fun mk_sel_spec ((c,T), thm) =
  1958       let
  1959         val (acc $ arg) = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop
  1960                                o Envir.beta_eta_contract o concl_of) thm;
  1961         val _ = if (arg aconv r_rec0) then ()
  1962                 else raise TERM ("mk_sel_spec: different arg", [arg]);
  1963       in
  1964         Const (mk_selC rec_schemeT0 (c,T))
  1965           :== acc
  1966       end;
  1967     val sel_specs = map mk_sel_spec (fields_more ~~ lastN accessor_thms);
  1968 
  1969     (*updates*)
  1970 
  1971     fun mk_upd_spec ((c,T), thm) =
  1972       let
  1973         val (upd $ _ $ arg) = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop
  1974                                    o Envir.beta_eta_contract o concl_of) thm;
  1975         val _ = if (arg aconv r_rec0) then ()
  1976                 else raise TERM ("mk_sel_spec: different arg", [arg]);
  1977       in Const (mk_updC updateN rec_schemeT0 (c,T))
  1978           :== upd
  1979       end;
  1980     val upd_specs = map mk_upd_spec (fields_more ~~ lastN updator_thms);
  1981 
  1982     (*derived operations*)
  1983     val make_spec = Const (full makeN, all_types ---> recT0) $$ all_vars :==
  1984       mk_rec (all_vars @ [HOLogic.unit]) 0;
  1985     val fields_spec = Const (full fields_selN, types ---> Type extension) $$ vars :==
  1986       mk_rec (all_vars @ [HOLogic.unit]) parent_len;
  1987     val extend_spec =
  1988       Const (full extendN, recT0-->moreT-->rec_schemeT0) $ r_unit0 $ more :==
  1989       mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0;
  1990     val truncate_spec = Const (full truncateN, rec_schemeT0 --> recT0) $ r0 :==
  1991       mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0;
  1992 
  1993     (* 2st stage: defs_thy *)
  1994 
  1995     fun mk_defs () =
  1996       extension_thy
  1997       |> Sign.add_trfuns
  1998           ([],[],field_tr's, [])
  1999       |> Sign.add_advanced_trfuns
  2000           ([],[],adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's,[])
  2001       |> Sign.parent_path
  2002       |> Sign.add_tyabbrs_i recordT_specs
  2003       |> Sign.add_path bname
  2004       |> Sign.add_consts_i
  2005           (map2 (fn (x, T) => fn mx => (Binding.name x, T, mx))
  2006             sel_decls (field_syntax @ [Syntax.NoSyn]))
  2007       |> (Sign.add_consts_i o map (fn (x, T) => (Binding.name x, T, Syntax.NoSyn)))
  2008           (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
  2009       |> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) sel_specs)
  2010       ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) upd_specs)
  2011       ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name))
  2012              [make_spec, fields_spec, extend_spec, truncate_spec])
  2013       |-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
  2014           fold Code.add_default_eqn sel_defs
  2015           #> fold Code.add_default_eqn upd_defs
  2016           #> fold Code.add_default_eqn derived_defs
  2017           #> pair defs)
  2018     val (((sel_defs, upd_defs), derived_defs), defs_thy) =
  2019       timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
  2020         mk_defs;
  2021 
  2022 
  2023     (* prepare propositions *)
  2024     val _ = timing_msg "record preparing propositions";
  2025     val P = Free (Name.variant all_variants "P", rec_schemeT0-->HOLogic.boolT);
  2026     val C = Free (Name.variant all_variants "C", HOLogic.boolT);
  2027     val P_unit = Free (Name.variant all_variants "P", recT0-->HOLogic.boolT);
  2028 
  2029     (*selectors*)
  2030     val sel_conv_props =
  2031        map (fn (c, x as Free (_,T)) => mk_sel r_rec0 (c,T) === x) named_vars_more;
  2032 
  2033     (*updates*)
  2034     fun mk_upd_prop (i,(c,T)) =
  2035       let val x' = Free (Name.variant all_variants (base c ^ "'"),T-->T);
  2036           val n = parent_fields_len + i;
  2037           val args' = nth_map n (K (x'$nth all_vars_more n)) all_vars_more
  2038       in mk_upd updateN c x' r_rec0 === mk_rec args' 0  end;
  2039     val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
  2040 
  2041     (*induct*)
  2042     val induct_scheme_prop =
  2043       All (map dest_Free all_vars_more) (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0);
  2044     val induct_prop =
  2045       (All (map dest_Free all_vars) (Trueprop (P_unit $ r_rec_unit0)),
  2046        Trueprop (P_unit $ r_unit0));
  2047 
  2048     (*surjective*)
  2049     val surjective_prop =
  2050       let val args = map (fn (c,Free (_,T)) => mk_sel r0 (c,T)) all_named_vars_more
  2051       in r0 === mk_rec args 0 end;
  2052 
  2053     (*cases*)
  2054     val cases_scheme_prop =
  2055       (All (map dest_Free all_vars_more)
  2056         (Trueprop (HOLogic.mk_eq (r0,r_rec0)) ==> Trueprop C))
  2057       ==> Trueprop C;
  2058 
  2059     val cases_prop =
  2060       (All (map dest_Free all_vars)
  2061         (Trueprop (HOLogic.mk_eq (r_unit0,r_rec_unit0)) ==> Trueprop C))
  2062        ==> Trueprop C;
  2063 
  2064     (*split*)
  2065     val split_meta_prop =
  2066       let val P = Free (Name.variant all_variants "P", rec_schemeT0-->Term.propT) in
  2067         Logic.mk_equals
  2068          (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
  2069       end;
  2070 
  2071     val split_object_prop =
  2072       let fun ALL vs t = List.foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) t vs
  2073       in (ALL [dest_Free r0] (P $ r0)) === (ALL (map dest_Free all_vars_more) (P $ r_rec0))
  2074       end;
  2075 
  2076 
  2077     val split_ex_prop =
  2078       let fun EX vs t = List.foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) t vs
  2079       in (EX [dest_Free r0] (P $ r0)) === (EX (map dest_Free all_vars_more) (P $ r_rec0))
  2080       end;
  2081 
  2082     (*equality*)
  2083     val equality_prop =
  2084       let
  2085         val s' = Free (rN ^ "'", rec_schemeT0)
  2086         fun mk_sel_eq (c,Free (_,T)) =  mk_sel r0 (c,T) === mk_sel s' (c,T)
  2087         val seleqs = map mk_sel_eq all_named_vars_more
  2088       in All (map dest_Free [r0,s']) (Logic.list_implies (seleqs,r0 === s')) end;
  2089 
  2090     (* 3rd stage: thms_thy *)
  2091 
  2092     fun prove stndrd = quick_and_dirty_prove stndrd defs_thy;
  2093     val prove_standard = quick_and_dirty_prove true defs_thy;
  2094 
  2095     fun prove_simp stndrd ss simps =
  2096       let val tac = simp_all_tac ss simps
  2097       in fn prop => prove stndrd [] prop (K tac) end;
  2098 
  2099     val ss = get_simpset defs_thy;
  2100 
  2101     fun sel_convs_prf () = map (prove_simp false ss
  2102                            (sel_defs@accessor_thms)) sel_conv_props;
  2103     val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf;
  2104     fun sel_convs_standard_prf () = map standard sel_convs
  2105     val sel_convs_standard =
  2106           timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf;
  2107 
  2108     fun upd_convs_prf () = map (prove_simp false ss
  2109                            (upd_defs@updator_thms)) upd_conv_props;
  2110     val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf;
  2111     fun upd_convs_standard_prf () = map standard upd_convs
  2112     val upd_convs_standard =
  2113           timeit_msg "record upd_convs_standard proof:" upd_convs_standard_prf;
  2114 
  2115     fun get_upd_acc_congs () = let
  2116         val symdefs  = map symmetric (sel_defs @ upd_defs);
  2117         val fold_ss  = HOL_basic_ss addsimps symdefs;
  2118         val ua_congs = map (standard o simplify fold_ss) upd_acc_cong_assists;
  2119       in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end;
  2120     val (fold_congs, unfold_congs) =
  2121           timeit_msg "record upd fold/unfold congs:" get_upd_acc_congs;
  2122 
  2123     val parent_induct = if null parents then [] else [#induct (hd (rev parents))];
  2124 
  2125     fun induct_scheme_prf () = prove_standard [] induct_scheme_prop (fn _ =>
  2126           (EVERY [if null parent_induct
  2127                   then all_tac else try_param_tac rN (hd parent_induct) 1,
  2128                   try_param_tac rN ext_induct 1,
  2129                   asm_simp_tac HOL_basic_ss 1]));
  2130     val induct_scheme = timeit_msg "record induct_scheme proof:" induct_scheme_prf;
  2131 
  2132     fun induct_prf () =
  2133       let val (assm, concl) = induct_prop;
  2134       in
  2135         prove_standard [assm] concl (fn {prems, ...} =>
  2136           try_param_tac rN induct_scheme 1
  2137           THEN try_param_tac "more" @{thm unit.induct} 1
  2138           THEN resolve_tac prems 1)
  2139       end;
  2140     val induct = timeit_msg "record induct proof:" induct_prf;
  2141 
  2142     fun cases_scheme_prf_opt () =
  2143       let
  2144         val (_$(Pvar$_)) = concl_of induct_scheme;
  2145         val ind = cterm_instantiate
  2146                     [(cterm_of defs_thy Pvar, cterm_of defs_thy
  2147                             (lambda w (HOLogic.imp$HOLogic.mk_eq(r0,w)$C)))]
  2148                     induct_scheme;
  2149         in standard (ObjectLogic.rulify (mp OF [ind, refl])) end;
  2150 
  2151     fun cases_scheme_prf_noopt () =
  2152         prove_standard [] cases_scheme_prop (fn _ =>
  2153          EVERY [asm_full_simp_tac (HOL_basic_ss addsimps [atomize_all, atomize_imp]) 1,
  2154                try_param_tac rN induct_scheme 1,
  2155                rtac impI 1,
  2156                REPEAT (etac allE 1),
  2157                etac mp 1,
  2158                rtac refl 1])
  2159     val cases_scheme_prf = quick_and_dirty_prf cases_scheme_prf_noopt cases_scheme_prf_opt;
  2160     val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
  2161 
  2162     fun cases_prf () =
  2163       prove_standard [] cases_prop  (fn _ =>
  2164         try_param_tac rN cases_scheme 1
  2165         THEN simp_all_tac HOL_basic_ss [unit_all_eq1]);
  2166     val cases = timeit_msg "record cases proof:" cases_prf;
  2167 
  2168     fun surjective_prf () = let
  2169         val leaf_ss   = get_sel_upd_defs defs_thy
  2170                                 addsimps (sel_defs @ (o_assoc :: id_o_apps));
  2171         val init_ss   = HOL_basic_ss addsimps ext_defs;
  2172       in
  2173         prove_standard [] surjective_prop (fn prems =>
  2174             (EVERY [rtac surject_assist_idE 1,
  2175                     simp_tac init_ss 1,
  2176                     REPEAT (intros_tac 1 ORELSE
  2177                             (rtac surject_assistI 1 THEN
  2178                              simp_tac leaf_ss 1))]))
  2179       end;
  2180     val surjective = timeit_msg "record surjective proof:" surjective_prf;
  2181 
  2182     fun split_meta_prf () =
  2183         prove false [] split_meta_prop (fn prems =>
  2184          EVERY [rtac equal_intr_rule 1, Goal.norm_hhf_tac 1,
  2185                 etac meta_allE 1, atac 1,
  2186                 rtac (prop_subst OF [surjective]) 1,
  2187                 REPEAT (etac meta_allE 1), atac 1]);
  2188     val split_meta = timeit_msg "record split_meta proof:" split_meta_prf;
  2189     fun split_meta_standardise () = standard split_meta;
  2190     val split_meta_standard = timeit_msg "record split_meta standard:"
  2191         split_meta_standardise;
  2192 
  2193     fun split_object_prf_opt () =
  2194       let
  2195         val cPI= cterm_of defs_thy (lambda r0 (Trueprop (P$r0)));
  2196         val (_$Abs(_,_,P$_)) = fst (Logic.dest_equals (concl_of split_meta_standard));
  2197         val cP = cterm_of defs_thy P;
  2198         val split_meta' = cterm_instantiate [(cP,cPI)] split_meta_standard;
  2199         val (l,r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop);
  2200         val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l);
  2201         val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r);
  2202         val thl = assume cl                 (*All r. P r*) (* 1 *)
  2203                 |> obj_to_meta_all          (*!!r. P r*)
  2204                 |> equal_elim split_meta'   (*!!n m more. P (ext n m more)*)
  2205                 |> meta_to_obj_all          (*All n m more. P (ext n m more)*) (* 2*)
  2206                 |> implies_intr cl          (* 1 ==> 2 *)
  2207         val thr = assume cr                           (*All n m more. P (ext n m more)*)
  2208                 |> obj_to_meta_all                    (*!!n m more. P (ext n m more)*)
  2209                 |> equal_elim (symmetric split_meta') (*!!r. P r*)
  2210                 |> meta_to_obj_all                    (*All r. P r*)
  2211                 |> implies_intr cr                    (* 2 ==> 1 *)
  2212      in standard (thr COMP (thl COMP iffI)) end;
  2213 
  2214     fun split_object_prf_noopt () =
  2215         prove_standard [] split_object_prop (fn _ =>
  2216          EVERY [rtac iffI 1,
  2217                 REPEAT (rtac allI 1), etac allE 1, atac 1,
  2218                 rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]);
  2219 
  2220     val split_object_prf = quick_and_dirty_prf split_object_prf_noopt split_object_prf_opt;
  2221     val split_object = timeit_msg "record split_object proof:" split_object_prf;
  2222 
  2223 
  2224     fun split_ex_prf () =
  2225       let
  2226         val ss   = HOL_basic_ss addsimps [not_ex RS sym, nth simp_thms 1];
  2227         val [Pv] = OldTerm.term_vars (prop_of split_object);
  2228         val cPv  = cterm_of defs_thy Pv;
  2229         val cP   = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0)));
  2230         val so3  = cterm_instantiate ([(cPv, cP)]) split_object;
  2231         val so4  = simplify ss so3;
  2232       in
  2233         prove_standard [] split_ex_prop (fn prems => resolve_tac [so4] 1)
  2234       end;
  2235     val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;
  2236 
  2237     fun equality_tac thms =
  2238       let val (s'::s::eqs) = rev thms;
  2239           val ss' = ss addsimps (s'::s::sel_convs_standard);
  2240           val eqs' = map (simplify ss') eqs;
  2241       in simp_tac (HOL_basic_ss addsimps (s'::s::eqs')) 1 end;
  2242 
  2243    fun equality_prf () = prove_standard [] equality_prop (fn {context, ...} =>
  2244       fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in
  2245         st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1
  2246         THEN res_inst_tac context [((rN, 0), s')] cases_scheme 1
  2247         THEN (Subgoal.FOCUS (fn {prems, ...} => equality_tac prems) context 1))
  2248              (* simp_all_tac ss (sel_convs) would also work but is less efficient *)
  2249       end);
  2250      val equality = timeit_msg "record equality proof:" equality_prf;
  2251 
  2252     val ((([sel_convs', upd_convs', sel_defs', upd_defs',
  2253             fold_congs', unfold_congs',
  2254           [split_meta', split_object', split_ex'], derived_defs'],
  2255           [surjective', equality']),
  2256           [induct_scheme', induct', cases_scheme', cases']), thms_thy) =
  2257       defs_thy
  2258       |> (PureThy.add_thmss o map (Thm.no_attributes o apfst Binding.name))
  2259          [("select_convs", sel_convs_standard),
  2260           ("update_convs", upd_convs_standard),
  2261           ("select_defs", sel_defs),
  2262           ("update_defs", upd_defs),
  2263           ("fold_congs", fold_congs),
  2264           ("unfold_congs", unfold_congs),
  2265           ("splits", [split_meta_standard,split_object,split_ex]),
  2266           ("defs", derived_defs)]
  2267       ||>> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
  2268           [("surjective", surjective),
  2269            ("equality", equality)]
  2270       ||>> (PureThy.add_thms o (map o apfst o apfst) Binding.name)
  2271         [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)),
  2272          (("induct", induct), induct_type_global name),
  2273          (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)),
  2274          (("cases", cases), cases_type_global name)];
  2275 
  2276 
  2277     val sel_upd_simps = sel_convs' @ upd_convs';
  2278     val sel_upd_defs = sel_defs' @ upd_defs';
  2279     val iffs = [ext_inject]
  2280     val depth = parent_len + 1;
  2281     val final_thy =
  2282       thms_thy
  2283       |> (snd oo PureThy.add_thmss)
  2284           [((Binding.name "simps", sel_upd_simps),
  2285             [Simplifier.simp_add, Nitpick_Const_Simps.add]),
  2286            ((Binding.name "iffs", iffs), [iff_add])]
  2287       |> put_record name (make_record_info args parent fields extension induct_scheme' ext_def)
  2288       |> put_sel_upd names full_moreN depth sel_upd_simps
  2289                            sel_upd_defs (fold_congs', unfold_congs')
  2290       |> add_record_equalities extension_id equality'
  2291       |> add_extinjects ext_inject
  2292       |> add_extsplit extension_name ext_split
  2293       |> add_record_splits extension_id (split_meta',split_object',split_ex',induct_scheme')
  2294       |> add_extfields extension_name (fields @ [(full_moreN,moreT)])
  2295       |> add_fieldext (extension_name,snd extension) (names @ [full_moreN])
  2296       |> Sign.parent_path;
  2297 
  2298   in final_thy
  2299   end;
  2300 
  2301 
  2302 (* add_record *)
  2303 
  2304 (*we do all preparations and error checks here, deferring the real
  2305   work to record_definition*)
  2306 fun gen_add_record prep_typ prep_raw_parent quiet_mode (params, bname) raw_parent raw_fields thy =
  2307   let
  2308     val _ = Theory.requires thy "Record" "record definitions";
  2309     val _ = if quiet_mode then () else writeln ("Defining record " ^ quote bname ^ " ...");
  2310 
  2311     val ctxt = ProofContext.init thy;
  2312 
  2313 
  2314     (* parents *)
  2315 
  2316     fun prep_inst T = fst (cert_typ ctxt T []);
  2317 
  2318     val parent = Option.map (apfst (map prep_inst) o prep_raw_parent ctxt) raw_parent
  2319       handle ERROR msg => cat_error msg ("The error(s) above in parent record specification");
  2320     val parents = add_parents thy parent [];
  2321 
  2322     val init_env =
  2323       (case parent of
  2324         NONE => []
  2325       | SOME (types, _) => List.foldr OldTerm.add_typ_tfrees [] types);
  2326 
  2327 
  2328     (* fields *)
  2329 
  2330     fun prep_field (c, raw_T, mx) env =
  2331       let val (T, env') = prep_typ ctxt raw_T env handle ERROR msg =>
  2332         cat_error msg ("The error(s) above occured in record field " ^ quote c)
  2333       in ((c, T, mx), env') end;
  2334 
  2335     val (bfields, envir) = fold_map prep_field raw_fields init_env;
  2336     val envir_names = map fst envir;
  2337 
  2338 
  2339     (* args *)
  2340 
  2341     val defaultS = Sign.defaultS thy;
  2342     val args = map (fn x => (x, AList.lookup (op =) envir x |> the_default defaultS)) params;
  2343 
  2344 
  2345     (* errors *)
  2346 
  2347     val name = Sign.full_bname thy bname;
  2348     val err_dup_record =
  2349       if is_none (get_record thy name) then []
  2350       else ["Duplicate definition of record " ^ quote name];
  2351 
  2352     val err_dup_parms =
  2353       (case duplicates (op =) params of
  2354         [] => []
  2355       | dups => ["Duplicate parameter(s) " ^ commas dups]);
  2356 
  2357     val err_extra_frees =
  2358       (case subtract (op =) params envir_names of
  2359         [] => []
  2360       | extras => ["Extra free type variable(s) " ^ commas extras]);
  2361 
  2362     val err_no_fields = if null bfields then ["No fields present"] else [];
  2363 
  2364     val err_dup_fields =
  2365       (case duplicates (op =) (map #1 bfields) of
  2366         [] => []
  2367       | dups => ["Duplicate field(s) " ^ commas_quote dups]);
  2368 
  2369     val err_bad_fields =
  2370       if forall (not_equal moreN o #1) bfields then []
  2371       else ["Illegal field name " ^ quote moreN];
  2372 
  2373     val err_dup_sorts =
  2374       (case duplicates (op =) envir_names of
  2375         [] => []
  2376       | dups => ["Inconsistent sort constraints for " ^ commas dups]);
  2377 
  2378     val errs =
  2379       err_dup_record @ err_dup_parms @ err_extra_frees @ err_no_fields @
  2380       err_dup_fields @ err_bad_fields @ err_dup_sorts;
  2381   in
  2382     if null errs then () else error (cat_lines errs)  ;
  2383     thy |> record_definition (args, bname) parent parents bfields
  2384   end
  2385   handle ERROR msg => cat_error msg ("Failed to define record " ^ quote bname);
  2386 
  2387 val add_record = gen_add_record read_typ read_raw_parent;
  2388 val add_record_i = gen_add_record cert_typ (K I);
  2389 
  2390 
  2391 (* setup theory *)
  2392 
  2393 val setup =
  2394   Sign.add_trfuns ([], parse_translation, [], []) #>
  2395   Sign.add_advanced_trfuns ([], adv_parse_translation, [], []) #>
  2396   Simplifier.map_simpset (fn ss =>
  2397     ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]);
  2398 
  2399 
  2400 (* outer syntax *)
  2401 
  2402 local structure P = OuterParse and K = OuterKeyword in
  2403 
  2404 val record_decl =
  2405   P.type_args -- P.name --
  2406     (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
  2407 
  2408 val _ =
  2409   OuterSyntax.command "record" "define extensible record" K.thy_decl
  2410     (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record false x y z)));
  2411 
  2412 end;
  2413 
  2414 end;
  2415 
  2416 structure Basic_Record: BASIC_RECORD = Record;
  2417 open Basic_Record;