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