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