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