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