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