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