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