src/HOL/Tools/record_package.ML
author schirmer
Thu Nov 06 20:45:02 2003 +0100 (2003-11-06)
changeset 14255 e6e3e3f0deed
parent 14079 1c22e5499eeb
child 14358 233c5bd5b539
permissions -rw-r--r--
Records:
- Record types are now by default printed with their type abbreviation
instead of the list of all field types. This can be configured via
the reference "print_record_type_abbr".
- Simproc "record_upd_simproc" for simplification of multiple updates
added (not enabled by default).
- Tactic "record_split_simp_tac" to split and simplify records added.
- Bug-fix and optimisation of "record_simproc".
- "record_simproc" and "record_upd_simproc" are now sensitive to
quick_and_dirty flag.
     1 (*  Title:      HOL/Tools/record_package.ML
     2     ID:         $Id$
     3     Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Extensible records with structural subtyping in HOL.
     7 *)
     8 
     9 signature BASIC_RECORD_PACKAGE =
    10 sig
    11   val record_simproc: simproc
    12   val record_eq_simproc: simproc
    13   val record_split_tac: int -> tactic
    14   val record_split_name: string
    15   val record_split_wrapper: string * wrapper
    16   val print_record_type_abbr: bool ref 
    17 end;
    18 
    19 signature RECORD_PACKAGE =
    20 sig
    21   include BASIC_RECORD_PACKAGE
    22   val quiet_mode: bool ref
    23   val updateN: string
    24   val mk_fieldT: (string * typ) * typ -> typ
    25   val dest_fieldT: typ -> (string * typ) * typ
    26   val dest_fieldTs: typ -> (string * typ) list
    27   val last_fieldT: typ -> (string * typ) option
    28   val mk_field: (string * term) * term -> term
    29   val mk_fst: term -> term
    30   val mk_snd: term -> term
    31   val mk_recordT: (string * typ) list * typ -> typ
    32   val dest_recordT: typ -> (string * typ) list * typ
    33   val mk_record: (string * term) list * term -> term
    34   val mk_sel: term -> string -> term
    35   val mk_update: term -> string * term -> term
    36   val print_records: theory -> unit
    37   val add_record: (string list * bstring) -> string option
    38     -> (bstring * string * mixfix) list -> theory -> theory * {simps: thm list, iffs: thm list}
    39   val add_record_i: (string list * bstring) -> (typ list * string) option
    40     -> (bstring * typ * mixfix) list -> theory -> theory * {simps: thm list, iffs: thm list}
    41   val setup: (theory -> theory) list
    42   val record_upd_simproc: simproc
    43   val record_split_simproc: (term -> bool) -> simproc
    44   val record_split_simp_tac: (term -> bool) -> int -> tactic
    45 end;
    46 
    47 structure RecordPackage :RECORD_PACKAGE =
    48 struct
    49 
    50 
    51 (*** theory context references ***)
    52 
    53 val product_typeN = "Record.product_type";
    54 
    55 val product_type_intro = thm "product_type.intro";
    56 val product_type_inject = thm "product_type.inject";
    57 val product_type_conv1 = thm "product_type.conv1";
    58 val product_type_conv2 = thm "product_type.conv2";
    59 val product_type_induct = thm "product_type.induct";
    60 val product_type_cases = thm "product_type.cases";
    61 val product_type_split_paired_all = thm "product_type.split_paired_all";
    62 val product_type_split_paired_All = thm "product_type.split_paired_All";
    63 
    64 
    65 
    66 (*** utilities ***)
    67 
    68 (* messages *)
    69 
    70 val quiet_mode = ref false;
    71 fun message s = if ! quiet_mode then () else writeln s;
    72 
    73 
    74 (* syntax *)
    75 
    76 fun prune n xs = Library.drop (n, xs);
    77 fun prefix_base s = NameSpace.map_base (fn bname => s ^ bname);
    78 
    79 val Trueprop = HOLogic.mk_Trueprop;
    80 fun All xs t = Term.list_all_free (xs, t);
    81 
    82 infix 9 $$;
    83 infix 0 :== ===;
    84 infixr 0 ==>;
    85 
    86 val (op $$) = Term.list_comb;
    87 val (op :==) = Logic.mk_defpair;
    88 val (op ===) = Trueprop o HOLogic.mk_eq;
    89 val (op ==>) = Logic.mk_implies;
    90 
    91 
    92 (* attributes *)
    93 
    94 fun case_names_fields x = RuleCases.case_names ["fields"] x;
    95 fun induct_type_global name = [case_names_fields, InductAttrib.induct_type_global name];
    96 fun cases_type_global name = [case_names_fields, InductAttrib.cases_type_global name];
    97 
    98 
    99 (* tactics *)
   100 
   101 fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps));
   102 
   103 (* do case analysis / induction on last parameter of ith subgoal (or s) *)
   104 
   105 fun try_param_tac s rule i st =
   106   let
   107     val cert = cterm_of (#sign (rep_thm st));
   108     val g = nth_elem (i - 1, prems_of st);
   109     val params = Logic.strip_params g;
   110     val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
   111     val rule' = Thm.lift_rule (st, i) rule;
   112     val (P, ys) = strip_comb (HOLogic.dest_Trueprop
   113       (Logic.strip_assums_concl (prop_of rule')));
   114     val (x, ca) = (case rev (drop (length params, ys)) of
   115         [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
   116           (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
   117       | [x] => (head_of x, false));
   118     val rule'' = cterm_instantiate (map (pairself cert) (case (rev params) of
   119         [] => (case assoc (map dest_Free (term_frees (prop_of st)), s) of
   120           None => sys_error "try_param_tac: no such variable"
   121         | Some T => [(P, if ca then concl else lambda (Free (s, T)) concl),
   122             (x, Free (s, T))])
   123       | (_, T) :: _ => [(P, list_abs (params, if ca then concl
   124           else incr_boundvars 1 (Abs (s, T, concl)))),
   125         (x, list_abs (params, Bound 0))])) rule'
   126   in compose_tac (false, rule'', nprems_of rule) i st end;
   127 
   128 
   129 
   130 (*** code generator data ***)
   131 
   132 val [prod_code, fst_code, snd_code] =
   133   map (Codegen.parse_mixfix (K (Bound 0))) ["(_,/ _)", "fst", "snd"];
   134 val prodT_code = Codegen.parse_mixfix (K dummyT) "(_ */ _)";
   135 
   136 
   137 
   138 (*** syntax operations ***)
   139 
   140 (** name components **)
   141 
   142 val rN = "r";
   143 val moreN = "more";
   144 val schemeN = "_scheme";
   145 val field_typeN = "_field_type";
   146 val fieldN = "_field";
   147 val fstN = "_val";
   148 val sndN = "_more";
   149 val updateN = "_update";
   150 val makeN = "make";
   151 val fieldsN = "fields";
   152 val extendN = "extend";
   153 val truncateN = "truncate";
   154 
   155 
   156 (*see typedef_package.ML*)
   157 val RepN = "Rep_";
   158 val AbsN = "Abs_";
   159 
   160 
   161 
   162 (** tuple operations **)
   163 
   164 (* types *)
   165 
   166 fun mk_fieldT ((c, T), U) = Type (suffix field_typeN c, [T, U]);
   167 
   168 fun dest_fieldT (typ as Type (c_field_type, [T, U])) =
   169       (case try (unsuffix field_typeN) c_field_type of
   170         None => raise TYPE ("dest_fieldT", [typ], [])
   171       | Some c => ((c, T), U))
   172   | dest_fieldT typ = raise TYPE ("dest_fieldT", [typ], []);
   173 
   174 fun dest_fieldTs T =
   175   let val ((c, T), U) = dest_fieldT T
   176   in (c, T) :: dest_fieldTs U
   177   end handle TYPE _ => [];
   178 
   179 fun last_fieldT T =
   180   let val ((c, T), U) = dest_fieldT T
   181   in (case last_fieldT U of
   182         None => Some (c,T)
   183       | Some l => Some l)
   184   end handle TYPE _ => None
   185 
   186 (* morphisms *)
   187 
   188 fun mk_Rep U (c, T) =
   189   Const (suffix field_typeN (prefix_base RepN c),
   190     mk_fieldT ((c, T), U) --> HOLogic.mk_prodT (T, U));
   191 
   192 fun mk_Abs U (c, T) =
   193   Const (suffix field_typeN (prefix_base AbsN c),
   194     HOLogic.mk_prodT (T, U) --> mk_fieldT ((c, T), U));
   195 
   196 
   197 (* constructors *)
   198 
   199 fun mk_fieldC U (c, T) = (suffix fieldN c, T --> U --> mk_fieldT ((c, T), U));
   200 
   201 fun mk_field ((c, t), u) =
   202   let val T = fastype_of t and U = fastype_of u
   203   in Const (suffix fieldN c, [T, U] ---> mk_fieldT ((c, T), U)) $ t $ u end;
   204 
   205 
   206 (* destructors *)
   207 
   208 fun mk_fstC U (c, T) = (suffix fstN c, mk_fieldT ((c, T), U) --> T);
   209 fun mk_sndC U (c, T) = (suffix sndN c, mk_fieldT ((c, T), U) --> U);
   210 
   211 fun dest_field fst_or_snd p =
   212   let
   213     val pT = fastype_of p;
   214     val ((c, T), U) = dest_fieldT pT;
   215     val (destN, destT) = if fst_or_snd then (fstN, T) else (sndN, U);
   216   in Const (suffix destN c, pT --> destT) $ p end;
   217 
   218 val mk_fst = dest_field true;
   219 val mk_snd = dest_field false;
   220 
   221 
   222 
   223 (** record operations **)
   224 
   225 (* types *)
   226 
   227 val mk_recordT = foldr mk_fieldT;
   228 
   229 fun dest_recordT T =
   230   (case try dest_fieldT T of
   231     None => ([], T)
   232   | Some (c_T, U) => apfst (cons c_T) (dest_recordT U));
   233 
   234 fun find_fieldT c rT =
   235   (case assoc (fst (dest_recordT rT), c) of
   236     None => raise TYPE ("find_field: " ^ c, [rT], [])
   237   | Some T => T);
   238 
   239 
   240 (* constructors *)
   241 
   242 val mk_record = foldr mk_field;
   243 
   244 
   245 (* selectors *)
   246 
   247 fun mk_selC rT (c, T) = (c, rT --> T);
   248 
   249 fun mk_sel r c =
   250   let val rT = fastype_of r
   251   in Const (mk_selC rT (c, find_fieldT c rT)) $ r end;
   252 
   253 fun mk_named_sels names r = names ~~ map (mk_sel r) names;
   254 
   255 val mk_moreC = mk_selC;
   256 
   257 fun mk_more r c =
   258   let val rT = fastype_of r
   259   in Const (mk_moreC rT (c, snd (dest_recordT rT))) $ r end;
   260 
   261 
   262 (* updates *)
   263 
   264 fun mk_updateC rT (c, T) = (suffix updateN c, T --> rT --> rT);
   265 
   266 fun mk_update r (c, x) =
   267   let val rT = fastype_of r
   268   in Const (mk_updateC rT (c, find_fieldT c rT)) $ x $ r end;
   269 
   270 val mk_more_updateC = mk_updateC;
   271 
   272 fun mk_more_update r (c, x) =
   273   let val rT = fastype_of r
   274   in Const (mk_more_updateC rT (c, snd (dest_recordT rT))) $ x $ r end;
   275 
   276 
   277 
   278 (** concrete syntax for records **)
   279 
   280 (* parse translations *)
   281 
   282 fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) =
   283       if c = mark then Syntax.const (suffix sfx name) $ arg
   284       else raise TERM ("gen_field_tr: " ^ mark, [t])
   285   | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]);
   286 
   287 fun gen_fields_tr sep mark sfx (tm as Const (c, _) $ t $ u) =
   288       if c = sep then gen_field_tr mark sfx t :: gen_fields_tr sep mark sfx u
   289       else [gen_field_tr mark sfx tm]
   290   | gen_fields_tr _ mark sfx tm = [gen_field_tr mark sfx tm];
   291 
   292 fun gen_record_tr sep mark sfx unit [t] = foldr (op $) (gen_fields_tr sep mark sfx t, unit)
   293   | gen_record_tr _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
   294 
   295 fun gen_record_scheme_tr sep mark sfx [t, more] = foldr (op $) (gen_fields_tr sep mark sfx t, more)
   296   | gen_record_scheme_tr _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
   297 
   298 
   299 val record_type_tr = gen_record_tr "_field_types" "_field_type" field_typeN (Syntax.const "unit");
   300 val record_type_scheme_tr = gen_record_scheme_tr "_field_types" "_field_type" field_typeN;
   301 
   302 val record_tr = gen_record_tr "_fields" "_field" fieldN HOLogic.unit;
   303 val record_scheme_tr = gen_record_scheme_tr "_fields" "_field" fieldN;
   304 
   305 fun record_update_tr [t, u] =
   306       foldr (op $) (rev (gen_fields_tr "_updates" "_update" updateN u), t)
   307   | record_update_tr ts = raise TERM ("record_update_tr", ts);
   308 
   309 
   310 fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts
   311   | update_name_tr (Const (x, T) :: ts) = Const (suffix updateN x, T) $$ ts
   312   | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
   313       (c $ update_name_tr [t] $ (Syntax.const "fun" $ ty $ Syntax.const "dummy")) $$ ts
   314   | update_name_tr ts = raise TERM ("update_name_tr", ts);
   315 
   316 
   317 val parse_translation =
   318  [("_record_type", record_type_tr),
   319   ("_record_type_scheme", record_type_scheme_tr),
   320   ("_record", record_tr),
   321   ("_record_scheme", record_scheme_tr),
   322   ("_record_update", record_update_tr),
   323   ("_update_name", update_name_tr)];
   324 
   325 
   326 (* print translations *)
   327 
   328 
   329 val print_record_type_abbr = ref true;
   330 
   331 fun gen_fields_tr' mark sfx (tm as Const (name_field, _) $ t $ u) =
   332       (case try (unsuffix sfx) name_field of
   333         Some name =>
   334           apfst (cons (Syntax.const mark $ Syntax.free name $ t)) (gen_fields_tr' mark sfx u)
   335       | None => ([], tm))
   336   | gen_fields_tr' _ _ tm = ([], tm);
   337 
   338 fun gen_record_tr' sep mark sfx is_unit record record_scheme tm =
   339   let
   340     val (ts, u) = gen_fields_tr' mark sfx tm;
   341     val t' = foldr1 (fn (v, w) => Syntax.const sep $ v $ w) ts;
   342   in
   343     if is_unit u then Syntax.const record $ t'
   344     else Syntax.const record_scheme $ t' $ u
   345   end;
   346 
   347 
   348 val record_type_tr' =
   349   gen_record_tr' "_field_types" "_field_type" field_typeN
   350     (fn Const ("unit", _) => true | _ => false) "_record_type" "_record_type_scheme";
   351 
   352 
   353 (* record_type_abbr_tr' tries to reconstruct the record name type abbreviation from *)
   354 (* the (nested) field types.                                                        *)
   355 fun record_type_abbr_tr' sg abbr alphas zeta lastF recT rec_schemeT tm =
   356   let
   357       (* tm is term representation of a (nested) field type. We first reconstruct the      *)
   358       (* type from tm so that we can continue on the type level rather then the term level.*)
   359  
   360       fun get_sort xs n = (case assoc (xs,n) of 
   361                              Some s => s 
   362                            | None => Sign.defaultS sg);
   363 
   364       val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm) 
   365       val {tsig,...} = Sign.rep_sg sg
   366 
   367       fun mk_type_abbr subst name alphas = 
   368           let val abbrT = Type (name, map (fn a => TVar ((a,0),logicS)) alphas);
   369           in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;    
   370 
   371       fun unify rT T = fst (Type.unify tsig (Vartab.empty,0) (Type.varifyT rT,T))
   372 
   373    in if !print_record_type_abbr
   374       then (case last_fieldT T of
   375              Some (name,_) 
   376               => if name = lastF 
   377                  then
   378 		   let val subst = unify rec_schemeT T 
   379                    in 
   380                     if HOLogic.is_unitT (Envir.norm_type subst (TVar((zeta,0),Sign.defaultS sg)))
   381                     then mk_type_abbr subst abbr alphas
   382                     else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta])
   383 		   end handle TUNIFY => record_type_tr' tm
   384                  else raise Match (* give print translation of specialised record a chance *)
   385             | _ => record_type_tr' tm)
   386        else record_type_tr' tm
   387   end
   388 
   389      
   390 fun gen_record_type_abbr_tr' sg abbr alphas zeta lastF recT rec_schemeT name =
   391   let val name_sfx = suffix field_typeN name
   392       val tr' = record_type_abbr_tr' sg abbr alphas zeta lastF recT rec_schemeT 
   393   in (name_sfx, fn [t,u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
   394       
   395 val record_tr' =
   396   gen_record_tr' "_fields" "_field" fieldN
   397     (fn Const ("Unity", _) => true | _ => false) "_record" "_record_scheme";
   398 
   399 fun record_update_tr' tm =
   400   let val (ts, u) = gen_fields_tr' "_update" updateN tm in
   401     Syntax.const "_record_update" $ u $
   402       foldr1 (fn (v, w) => Syntax.const "_updates" $ v $ w) (rev ts)
   403   end;
   404 
   405 fun gen_field_tr' sfx tr' name =
   406   let val name_sfx = suffix sfx name
   407   in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
   408 
   409 fun print_translation names =
   410   map (gen_field_tr' fieldN record_tr') names @
   411   map (gen_field_tr' updateN record_update_tr') names;
   412 
   413 fun print_translation_field_types names =
   414   map (gen_field_tr' field_typeN record_type_tr') names
   415 
   416 
   417 
   418 (*** extend theory by record definition ***)
   419 
   420 (** record info **)
   421 
   422 (* type record_info and parent_info  *)
   423 
   424 type record_info =
   425  {args: (string * sort) list,
   426   parent: (typ list * string) option,
   427   fields: (string * typ) list,
   428   field_inducts: thm list,
   429   field_cases: thm list,
   430   field_splits: thm list,
   431   simps: thm list};
   432 
   433 fun make_record_info args parent fields field_inducts field_cases field_splits simps =
   434  {args = args, parent = parent, fields = fields, field_inducts = field_inducts,
   435   field_cases = field_cases, field_splits = field_splits, simps = simps}: record_info;
   436 
   437 type parent_info =
   438  {name: string,
   439   fields: (string * typ) list,
   440   field_inducts: thm list,
   441   field_cases: thm list,
   442   field_splits: thm list,
   443   simps: thm list};
   444 
   445 fun make_parent_info name fields field_inducts field_cases field_splits simps =
   446  {name = name, fields = fields, field_inducts = field_inducts,
   447   field_cases = field_cases, field_splits = field_splits, simps = simps}: parent_info;
   448 
   449 
   450 (* data kind 'HOL/records' *)
   451 
   452 type record_data =
   453  {records: record_info Symtab.table,
   454   sel_upd:
   455    {selectors: unit Symtab.table,
   456     updates: string Symtab.table,
   457     simpset: Simplifier.simpset},
   458   field_splits:
   459    {fields: unit Symtab.table,
   460     simpset: Simplifier.simpset},
   461   equalities: thm Symtab.table,
   462   splits: (thm*thm*thm*thm) Symtab.table (* !!,!,EX - split-equalities,induct rule *) 
   463 };
   464 
   465 fun make_record_data records sel_upd field_splits equalities splits =
   466  {records = records, sel_upd = sel_upd, field_splits = field_splits,
   467   equalities = equalities, splits = splits}: record_data;
   468 
   469 structure RecordsArgs =
   470 struct
   471   val name = "HOL/records";
   472   type T = record_data;
   473 
   474   val empty =
   475     make_record_data Symtab.empty
   476       {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss}
   477       {fields = Symtab.empty, simpset = HOL_basic_ss} Symtab.empty Symtab.empty;
   478 
   479   val copy = I;
   480   val prep_ext = I;
   481   fun merge
   482    ({records = recs1,
   483      sel_upd = {selectors = sels1, updates = upds1, simpset = ss1},
   484      field_splits = {fields = flds1, simpset = fld_ss1},
   485      equalities = equalities1,
   486      splits = splits1},
   487     {records = recs2,
   488      sel_upd = {selectors = sels2, updates = upds2, simpset = ss2},
   489      field_splits = {fields = flds2, simpset = fld_ss2},
   490      equalities = equalities2, 
   491      splits = splits2}) =
   492     make_record_data  
   493       (Symtab.merge (K true) (recs1, recs2))
   494       {selectors = Symtab.merge (K true) (sels1, sels2),
   495         updates = Symtab.merge (K true) (upds1, upds2),
   496         simpset = Simplifier.merge_ss (ss1, ss2)}
   497       {fields = Symtab.merge (K true) (flds1, flds2),
   498         simpset = Simplifier.merge_ss (fld_ss1, fld_ss2)}
   499       (Symtab.merge Thm.eq_thm (equalities1, equalities2))
   500       (Symtab.merge (fn ((a,b,c,d),(w,x,y,z)) 
   501                      => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso 
   502                         Thm.eq_thm (c,y) andalso Thm.eq_thm (d,z)) 
   503                     (splits1, splits2));
   504 
   505   fun print sg ({records = recs, ...}: record_data) =
   506     let
   507       val prt_typ = Sign.pretty_typ sg;
   508 
   509       fun pretty_parent None = []
   510         | pretty_parent (Some (Ts, name)) =
   511             [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
   512 
   513       fun pretty_field (c, T) = Pretty.block
   514         [Pretty.str (Sign.cond_extern sg Sign.constK c), Pretty.str " ::",
   515           Pretty.brk 1, Pretty.quote (prt_typ T)];
   516 
   517       fun pretty_record (name, {args, parent, fields, ...}: record_info) =
   518         Pretty.block (Pretty.fbreaks (Pretty.block
   519           [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
   520           pretty_parent parent @ map pretty_field fields));
   521     in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
   522 end;
   523 
   524 structure RecordsData = TheoryDataFun(RecordsArgs);
   525 val print_records = RecordsData.print;
   526 
   527 
   528 (* access 'records' *)
   529 
   530 fun get_record thy name = Symtab.lookup (#records (RecordsData.get thy), name);
   531 
   532 fun put_record name info thy =
   533   let
   534     val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy;
   535     val data = make_record_data (Symtab.update ((name, info), records))
   536       sel_upd field_splits equalities splits;
   537   in RecordsData.put data thy end;
   538 
   539 
   540 (* access 'sel_upd' *)
   541 
   542 fun get_sel_upd sg = #sel_upd (RecordsData.get_sg sg);
   543 
   544 fun get_selectors sg name = Symtab.lookup (#selectors (get_sel_upd sg), name);
   545 fun get_updates sg name = Symtab.lookup (#updates (get_sel_upd sg), name);
   546 fun get_simpset sg = #simpset (get_sel_upd sg);
   547 
   548 fun put_sel_upd names simps thy =
   549   let
   550     val sels = map (rpair ()) names;
   551     val upds = map (suffix updateN) names ~~ names;
   552 
   553     val {records, sel_upd = {selectors, updates, simpset}, field_splits,
   554       equalities, splits} = RecordsData.get thy;
   555     val data = make_record_data records
   556       {selectors = Symtab.extend (selectors, sels),
   557         updates = Symtab.extend (updates, upds),
   558         simpset = Simplifier.addsimps (simpset, simps)}
   559       field_splits equalities splits;
   560   in RecordsData.put data thy end;
   561 
   562 
   563 (* access 'field_splits' *)
   564 
   565 fun add_field_splits names simps thy =
   566   let
   567     val {records, sel_upd, field_splits = {fields, simpset},
   568       equalities, splits} = RecordsData.get thy;
   569     val flds = map (rpair ()) names;
   570     val data = make_record_data records sel_upd
   571       {fields = Symtab.extend (fields, flds),
   572        simpset = Simplifier.addsimps (simpset, simps)} equalities splits;
   573   in RecordsData.put data thy end;
   574 
   575 
   576 (* access 'equalities' *)
   577 
   578 fun add_record_equalities name thm thy =
   579   let
   580     val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy;
   581     val data = make_record_data records sel_upd field_splits
   582       (Symtab.update_new ((name, thm), equalities)) splits;
   583   in RecordsData.put data thy end;
   584 
   585 fun get_equalities sg name =
   586   Symtab.lookup (#equalities (RecordsData.get_sg sg), name);
   587 
   588 (* access 'splits' *)
   589 
   590 fun add_record_splits name thmP thy =
   591   let
   592     val {records, sel_upd, field_splits, equalities, splits} = RecordsData.get thy;
   593     val data = make_record_data records sel_upd field_splits
   594       equalities (Symtab.update_new ((name, thmP), splits));
   595   in RecordsData.put data thy end;
   596 
   597 fun get_splits sg name =
   598   Symtab.lookup (#splits (RecordsData.get_sg sg), name);
   599 
   600 
   601 (* parent records *)
   602 
   603 fun add_parents thy None parents = parents
   604   | add_parents thy (Some (types, name)) parents =
   605       let
   606         val sign = Theory.sign_of thy;
   607         fun err msg = error (msg ^ " parent record " ^ quote name);
   608 
   609         val {args, parent, fields, field_inducts, field_cases, field_splits, simps} =
   610           (case get_record thy name of Some info => info | None => err "Unknown");
   611         val _ = if length types <> length args then err "Bad number of arguments for" else ();
   612 
   613         fun bad_inst ((x, S), T) =
   614           if Sign.of_sort sign (T, S) then None else Some x
   615         val bads = mapfilter bad_inst (args ~~ types);
   616 
   617         val inst = map fst args ~~ types;
   618         val subst = Term.map_type_tfree (fn (x, _) => the (assoc (inst, x)));
   619         val parent' = apsome (apfst (map subst)) parent;
   620         val fields' = map (apsnd subst) fields;
   621       in
   622         conditional (not (null bads)) (fn () =>
   623           err ("Ill-sorted instantiation of " ^ commas bads ^ " in"));
   624         add_parents thy parent'
   625           (make_parent_info name fields' field_inducts field_cases field_splits simps::parents)
   626       end;
   627 
   628 
   629 (** record simprocs **)
   630  
   631 fun quick_and_dirty_prove sg xs asms prop tac =
   632 Tactic.prove sg xs asms prop
   633     (if ! quick_and_dirty then (K (SkipProof.cheat_tac HOL.thy)) else tac);
   634 
   635 
   636 fun prove_split_simp sg T prop =
   637     (case last_fieldT T of
   638       Some (name,_) => (case get_splits sg name of
   639                          Some (all_thm,_,_,_) 
   640                           => let val {sel_upd={simpset,...},...} = RecordsData.get_sg sg;
   641                              in (quick_and_dirty_prove sg [] [] prop 
   642                                   (K (simp_tac (simpset addsimps [all_thm]) 1)))
   643                              end
   644                       | _ => error "RecordPackage.prove_split_simp: code should never been reached")
   645      | _ => error "RecordPackage.prove_split_simp: code should never been reached")
   646 
   647 
   648 (* record_simproc *)
   649 (* Simplifies selections of an record update:
   650  *  (1)  S (r(|S:=k|)) = k respectively
   651  *  (2)  S (r(|X:=k|)) = S r
   652  * The simproc skips multiple updates at once, eg:
   653  *  S (r (|S:=k,X:=2,Y:=3|)) = k
   654  * But be careful in (2) because of the extendibility of records.
   655  * - If S is a more-selector we have to make sure that the update on component
   656  *   X does not affect the selected subrecord.
   657  * - If X is a more-selector we have to make sure that S is not in the updated
   658  *   subrecord. 
   659  *)
   660 val record_simproc =
   661   Simplifier.simproc (Theory.sign_of HOL.thy) "record_simp" ["s (u k r)"]
   662     (fn sg => fn _ => fn t =>
   663       (case t of (sel as Const (s, Type (_,[domS,rangeS]))) $ ((upd as Const (u, _)) $ k $ r) =>
   664         (case get_selectors sg s of Some () =>
   665           (case get_updates sg u of Some u_name =>
   666             let
   667               fun mk_abs_var x t = (x, fastype_of t);
   668               val {sel_upd={updates,...},...} = RecordsData.get_sg sg;
   669 
   670               fun mk_eq_terms ((upd as Const (u,Type(_,[updT,_]))) $ k $ r) =
   671 		  (case (Symtab.lookup (updates,u)) of
   672                      None => None
   673                    | Some u_name 
   674                      => if u_name = s
   675                         then let 
   676                                val rv = mk_abs_var "r" r
   677                                val rb = Bound 0
   678                                val kv = mk_abs_var "k" k
   679                                val kb = Bound 1 
   680                              in Some (upd$kb$rb,kb,[kv,rv],true) end
   681                         else if u_name mem (map fst (dest_fieldTs rangeS))
   682                              orelse s mem (map fst (dest_fieldTs updT))
   683                              then None
   684 			     else (case mk_eq_terms r of 
   685                                      Some (trm,trm',vars,update_s) 
   686                                      => let   
   687 					  val kv = mk_abs_var "k" k
   688                                           val kb = Bound (length vars)
   689 		                        in Some (upd$kb$trm,trm',kv::vars,update_s) end
   690                                    | None
   691                                      => let 
   692 					  val rv = mk_abs_var "r" r
   693                                           val rb = Bound 0
   694                                           val kv = mk_abs_var "k" k
   695                                           val kb = Bound 1 
   696                                         in Some (upd$kb$rb,rb,[kv,rv],false) end))
   697                 | mk_eq_terms r = None     
   698             in
   699 	      (case mk_eq_terms (upd$k$r) of
   700                  Some (trm,trm',vars,update_s) 
   701                  => if update_s 
   702 		    then Some (prove_split_simp sg domS 
   703                                  (list_all(vars,(Logic.mk_equals (sel$trm,trm')))))
   704                     else Some (prove_split_simp sg domS 
   705                                  (list_all(vars,(Logic.mk_equals (sel$trm,sel$trm')))))
   706                | None => None)
   707             end
   708           | None => None)
   709         | None => None)
   710       | _ => None));
   711 
   712 (* record_eq_simproc *)
   713 (* looks up the most specific record-equality.
   714  * Note on efficiency:
   715  * Testing equality of records boils down to the test of equality of all components.
   716  * Therefore the complexity is: #components * complexity for single component.
   717  * Especially if a record has a lot of components it may be better to split up
   718  * the record first and do simplification on that (record_split_simp_tac).
   719  * e.g. r(|lots of updates|) = x
   720  *
   721  *               record_eq_simproc           record_split_simp_tac
   722  * Complexity: #components * #updates     #updates   
   723  *           
   724  *)
   725 val record_eq_simproc =
   726   Simplifier.simproc (Theory.sign_of HOL.thy) "record_eq_simp" ["r = s"]
   727     (fn sg => fn _ => fn t =>
   728       (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ =>
   729         (case last_fieldT T of
   730            None => None
   731          | Some (name, _) => (case get_equalities sg name of
   732                                 None => None
   733                               | Some thm => Some (thm RS Eq_TrueI)))
   734        | _ => None));
   735 
   736 
   737 (* record_upd_simproc *)
   738 (* simplify multiple updates; for example: "r(|M:=3,N:=1,M:=2,N:=4|) == r(|M:=2,N:=4|)" *)
   739 val record_upd_simproc =
   740   Simplifier.simproc (Theory.sign_of HOL.thy) "record_upd_simp" ["(u1 k1 (u2 k2 r))"]
   741     (fn sg => fn _ => fn t =>
   742       (case t of ((upd as Const (u, Type(_,[_,Type(_,[T,_])]))) $ k $ r) =>
   743  	 let val {sel_upd={updates,...},...} = RecordsData.get_sg sg;
   744 	     fun mk_abs_var x t = (x, fastype_of t);
   745 
   746              fun mk_updterm upds already ((upd as Const (u,_)) $ k $ r) =
   747 		 if is_some (Symtab.lookup (upds,u))
   748 		 then let 
   749 			 fun rest already = mk_updterm upds already
   750 		      in if is_some (Symtab.lookup (already,u)) 
   751 			 then (case (rest already r) of
   752 				 None => let 
   753 				           val rv = mk_abs_var "r" r
   754                                            val rb = Bound 0
   755 					   val kv = mk_abs_var "k" k
   756                                            val kb = Bound 1	      
   757                                          in Some (upd$kb$rb,rb,[kv,rv]) end
   758                                | Some (trm,trm',vars) 
   759 				 => let 
   760 				     val kv = mk_abs_var "k" k
   761                                      val kb = Bound (length vars)
   762                                     in Some (upd$kb$trm,trm',kv::vars) end)
   763 	                 else (case rest (Symtab.update ((u,()),already)) r of 
   764 				 None => None
   765 		               | Some (trm,trm',vars) 
   766                                   => let
   767 				      val kv = mk_abs_var "k" k
   768                                       val kb = Bound (length vars)
   769                                      in Some (upd$kb$trm,upd$kb$trm',kv::vars) end)
   770 		     end
   771 		 else None
   772 	       | mk_updterm _ _ _ = None;
   773 
   774 	 in (case mk_updterm updates Symtab.empty t of
   775 	       Some (trm,trm',vars)
   776                 => Some (prove_split_simp sg T (list_all(vars,(Logic.mk_equals (trm,trm')))))
   777              | None => None)
   778 	 end
   779        | _ => None));
   780 
   781 (* record_split_simproc *)
   782 (* splits quantified occurrences of records, for which P holds. P can peek on the 
   783  * subterm starting at the quantified occurrence of the record (including the quantifier)
   784  *)
   785 fun record_split_simproc P =
   786   Simplifier.simproc (Theory.sign_of HOL.thy) "record_split_simp" ["(a t)"]
   787     (fn sg => fn _ => fn t =>
   788       (case t of (Const (quantifier, Type (_, [Type (_, [T, _]), _])))$trm =>
   789          if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex"
   790          then (case last_fieldT T of
   791                  None => None
   792                | Some (name, _)
   793                   => if P t 
   794                      then (case get_splits sg name of
   795                              None => None
   796                            | Some (all_thm, All_thm, Ex_thm,_) 
   797                               => Some (case quantifier of
   798                                          "all" => all_thm
   799                                        | "All" => All_thm RS HOL.eq_reflection
   800                                        | "Ex"  => Ex_thm RS HOL.eq_reflection
   801                                        | _     => error "record_split_simproc"))
   802                      else None)
   803          else None
   804        | _ => None))
   805 
   806 (** record field splitting **)
   807 
   808 (* tactic *)
   809 
   810 fun is_fieldT fields (Type (a, [_, _])) = is_some (Symtab.lookup (fields, a))
   811   | is_fieldT _ _ = false;
   812 
   813 fun record_split_tac i st =
   814   let
   815     val {field_splits = {fields, simpset}, ...} = RecordsData.get_sg (Thm.sign_of_thm st);
   816 
   817     val has_field = exists_Const
   818       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   819           (s = "all" orelse s = "All") andalso is_fieldT fields T
   820         | _ => false);
   821 
   822     val goal = Library.nth_elem (i - 1, Thm.prems_of st);
   823   in
   824     if has_field goal then Simplifier.full_simp_tac simpset i st
   825     else Seq.empty
   826   end handle Library.LIST _ => Seq.empty;
   827 
   828 
   829 local
   830 val inductive_atomize = thms "induct_atomize";
   831 val inductive_rulify1 = thms "induct_rulify1";
   832 in
   833 (* record_split_simp_tac *)
   834 (* splits (and simplifies) all records in the goal for which P holds. 
   835  * For quantified occurrences of a record
   836  * P can peek on the whole subterm (including the quantifier); for free variables P
   837  * can only peek on the variable itself. 
   838  *)
   839 fun record_split_simp_tac P i st =
   840   let
   841     val sg = Thm.sign_of_thm st;
   842     val {sel_upd={simpset,...},field_splits={fields,...},...} 
   843             = RecordsData.get_sg sg;
   844 
   845     val has_field = exists_Const
   846       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
   847           (s = "all" orelse s = "All" orelse s = "Ex") andalso is_fieldT fields T
   848         | _ => false);
   849 
   850     val goal = Library.nth_elem (i - 1, Thm.prems_of st);
   851     val frees = filter (is_fieldT fields o type_of) (term_frees goal);
   852 
   853     fun mk_split_free_tac free induct_thm i = 
   854 	let val cfree = cterm_of sg free;
   855             val (_$(_$r)) = concl_of induct_thm;
   856             val crec = cterm_of sg r;
   857             val thm  = cterm_instantiate [(crec,cfree)] induct_thm;
   858         in EVERY [simp_tac (HOL_basic_ss addsimps inductive_atomize) i,
   859                   rtac thm i,
   860                   simp_tac (HOL_basic_ss addsimps inductive_rulify1) i]
   861 	end;
   862 
   863     fun split_free_tac P i (free as Free (n,T)) = 
   864 	(case last_fieldT T of
   865            None => None
   866          | Some(name,_)=> if P free 
   867                           then (case get_splits sg name of
   868                                   None => None
   869                                 | Some (_,_,_,induct_thm)
   870                                    => Some (mk_split_free_tac free induct_thm i))
   871                           else None)
   872      | split_free_tac _ _ _ = None;
   873 
   874     val split_frees_tacs = mapfilter (split_free_tac P i) frees;
   875    
   876     val simprocs = if has_field goal then [record_split_simproc P] else [];
   877    
   878   in st |> (EVERY split_frees_tacs) 
   879            THEN (Simplifier.full_simp_tac (simpset addsimprocs simprocs) i)
   880   end handle Library.LIST _ => Seq.empty;
   881 end;
   882 
   883 (* wrapper *)
   884 
   885 val record_split_name = "record_split_tac";
   886 val record_split_wrapper = (record_split_name, fn tac => record_split_tac ORELSE' tac);
   887 
   888 
   889 (* method *)
   890 
   891 val record_split_method =
   892   ("record_split", Method.no_args (Method.SIMPLE_METHOD' HEADGOAL record_split_tac),
   893     "split record fields");
   894 
   895 
   896 
   897 (** internal theory extenders **)
   898 
   899 (* field_typedefs *)
   900 
   901 fun field_typedefs zeta moreT names theory =
   902   let
   903     val alpha = "'a";
   904     val aT = TFree (alpha, HOLogic.typeS);
   905     val UNIV = HOLogic.mk_UNIV (HOLogic.mk_prodT (aT, moreT));
   906 
   907     fun type_def (thy, name) =
   908       let val (thy', {type_definition, set_def = Some def, ...}) =
   909         thy |> setmp TypedefPackage.quiet_mode true
   910           (TypedefPackage.add_typedef_i true None
   911             (suffix field_typeN (Sign.base_name name), [alpha, zeta], Syntax.NoSyn) UNIV None
   912           (Tactic.rtac UNIV_witness 1))
   913       in (thy', Tactic.rewrite_rule [def] type_definition) end
   914   in foldl_map type_def (theory, names) end;
   915 
   916 
   917 (* field_definitions *)
   918 
   919 fun field_definitions fields names xs alphas zeta moreT more vars named_vars thy =
   920   let
   921     val sign = Theory.sign_of thy;
   922     val base = Sign.base_name;
   923 
   924     val xT = TFree (variant alphas "'x", HOLogic.typeS);
   925 
   926 
   927     (* prepare declarations and definitions *)
   928 
   929     (*field constructors*)
   930     val field_decls = map (mk_fieldC moreT) fields;
   931 
   932     fun mk_field_spec ((c, T), v) =
   933       Term.head_of (mk_field ((c, v), more)) :==
   934         lambda v (lambda more (mk_Abs moreT (c, T) $ (HOLogic.mk_prod (v, more))));
   935     val field_specs = map mk_field_spec (fields ~~ vars);
   936 
   937     (*field destructors*)
   938     val dest_decls = map (mk_fstC moreT) fields @ map (mk_sndC moreT) fields;
   939 
   940     fun mk_dest_spec dest sel (c, T) =
   941       let val p = Free ("p", mk_fieldT ((c, T), moreT));
   942       in Term.head_of (dest p) :== lambda p (sel (mk_Rep moreT (c, T) $ p)) end;
   943     val dest_specs1 = map (mk_dest_spec mk_fst HOLogic.mk_fst) fields;
   944     val dest_specs2 = map (mk_dest_spec mk_snd HOLogic.mk_snd) fields;
   945 
   946 
   947     (* 1st stage: defs_thy *)
   948 
   949     val (defs_thy, (((typedefs, field_defs), dest_defs1), dest_defs2)) =
   950       thy
   951       |> field_typedefs zeta moreT names
   952       |>> (Theory.add_consts_i o map (Syntax.no_syn o apfst base)) (field_decls @ dest_decls)
   953       |>>> (PureThy.add_defs_i false o map Thm.no_attributes) field_specs
   954       |>>> (PureThy.add_defs_i false o map Thm.no_attributes) dest_specs1
   955       |>>> (PureThy.add_defs_i false o map Thm.no_attributes) dest_specs2;
   956 
   957     val prod_types = map (fn (((a, b), c), d) => product_type_intro OF [a, b, c, d])
   958       (typedefs ~~ field_defs ~~ dest_defs1 ~~ dest_defs2);
   959 
   960 
   961     (* 2nd stage: thms_thy *)
   962 
   963     fun make ren th = map (fn (prod_type, field) => Drule.standard
   964       (Drule.rename_bvars (ren ~~ [base (fst field), moreN] handle LIST _ => [])
   965         (th OF [prod_type]))) (prod_types ~~ fields);
   966 
   967     val dest_convs = make [] product_type_conv1 @ make [] product_type_conv2;
   968     val field_injects = make [] product_type_inject;
   969     val field_inducts = make ["x", "y"] product_type_induct;
   970     val field_cases = make ["x", "y"] product_type_cases;
   971     val field_splits = make ["a", "b"] product_type_split_paired_all @
   972       make ["a", "b"] product_type_split_paired_All;
   973 
   974     val (thms_thy, [field_defs', dest_defs', dest_convs', field_injects',
   975         field_splits', field_inducts', field_cases']) = defs_thy
   976       |> Codegen.assoc_consts_i (flat (map (fn (s, _) =>
   977            [(suffix fieldN s, None, prod_code),
   978             (suffix fstN s, None, fst_code),
   979             (suffix sndN s, None, snd_code)]) fields))
   980       |> Codegen.assoc_types (map (fn (s, _) =>
   981            (suffix field_typeN s, prodT_code)) fields)
   982       |> (PureThy.add_thmss o map Thm.no_attributes)
   983        [("field_defs", field_defs),
   984         ("dest_defs", dest_defs1 @ dest_defs2),
   985         ("dest_convs", dest_convs),
   986         ("field_injects", field_injects),
   987         ("field_splits", field_splits),
   988         ("field_inducts", field_inducts),
   989         ("field_cases", field_cases)];
   990 
   991   in (thms_thy, dest_convs', field_injects', field_splits', field_inducts', field_cases') end;
   992 
   993 
   994 (* record_definition *)
   995 
   996 fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy =
   997   let
   998     val sign = Theory.sign_of thy;
   999 
  1000     val alphas = map fst args;
  1001     val name = Sign.full_name sign bname;
  1002     val full = Sign.full_name_path sign bname;
  1003     val base = Sign.base_name;
  1004 
  1005     val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
  1006 
  1007 
  1008     (* basic components *)
  1009 
  1010     val ancestry = map (length o flat o map #fields) (Library.prefixes1 parents);
  1011 
  1012     val parent_fields = flat (map #fields parents);
  1013     val parent_names = map fst parent_fields;
  1014     val parent_types = map snd parent_fields;
  1015     val parent_len = length parent_fields;
  1016     val parent_xs = variantlist (map (base o fst) parent_fields, [moreN, rN]);
  1017     val parent_vars = ListPair.map Free (parent_xs, parent_types);
  1018     val parent_named_vars = parent_names ~~ parent_vars;
  1019 
  1020     val fields = map (apfst full) bfields;
  1021     val names = map fst fields;
  1022     val types = map snd fields;
  1023     val len = length fields;
  1024     val xs = variantlist (map fst bfields, moreN :: rN :: parent_xs);
  1025     val vars = ListPair.map Free (xs, types);
  1026     val named_vars = names ~~ vars;
  1027 
  1028     val all_fields = parent_fields @ fields;
  1029     val all_names = parent_names @ names;
  1030     val all_types = parent_types @ types;
  1031     val all_len = parent_len + len;
  1032     val all_xs = parent_xs @ xs;
  1033     val all_vars = parent_vars @ vars;
  1034     val all_named_vars = parent_named_vars @ named_vars;
  1035 
  1036     val zeta = variant alphas "'z";
  1037     val moreT = TFree (zeta, HOLogic.typeS);
  1038     val more = Free (moreN, moreT);
  1039     val full_moreN = full moreN;
  1040     fun more_part t = mk_more t full_moreN;
  1041     fun more_part_update t x = mk_more_update t (full_moreN, x);
  1042     val all_types_more = all_types @ [moreT];
  1043     val all_xs_more = all_xs @ [moreN];
  1044 
  1045     val parent_more = funpow parent_len mk_snd;
  1046     val idxs = 0 upto (len - 1);
  1047 
  1048     val fieldsT = mk_recordT (fields, HOLogic.unitT);
  1049     fun rec_schemeT n = mk_recordT (prune n all_fields, moreT);
  1050     fun rec_scheme n = mk_record (prune n all_named_vars, more);
  1051     fun recT n = mk_recordT (prune n all_fields, HOLogic.unitT);
  1052     fun rec_ n = mk_record (prune n all_named_vars, HOLogic.unit);
  1053     fun r_scheme n = Free (rN, rec_schemeT n);
  1054     fun r n = Free (rN, recT n);
  1055 
  1056     
  1057 
  1058     (* prepare print translation functions *)
  1059     val field_tr's =
  1060       print_translation (distinct (flat (map NameSpace.accesses' (full_moreN :: names))));
  1061 
  1062     val field_type_tr's = 
  1063 	let val fldnames = if parent_len = 0 then (tl names) else names;
  1064         in print_translation_field_types (distinct (flat (map NameSpace.accesses' fldnames))) 
  1065         end;
  1066                           
  1067     fun record_type_abbr_tr's thy =
  1068 	let val trnames = (distinct (flat (map NameSpace.accesses' [hd all_names])))
  1069             val sg = Theory.sign_of thy
  1070 	in map (gen_record_type_abbr_tr' 
  1071                  sg bname alphas zeta (hd (rev names)) (recT 0) (rec_schemeT 0)) trnames end;   
  1072 
  1073     (* prepare declarations *)
  1074 
  1075     val sel_decls = map (mk_selC (rec_schemeT 0)) bfields @
  1076       [mk_moreC (rec_schemeT 0) (moreN, moreT)];
  1077     val update_decls = map (mk_updateC (rec_schemeT 0)) bfields @
  1078       [mk_more_updateC (rec_schemeT 0) (moreN, moreT)];
  1079     val make_decl = (makeN, all_types ---> recT 0);
  1080     val fields_decl = (fieldsN, types ---> fieldsT);
  1081     val extend_decl = (extendN, recT 0 --> moreT --> rec_schemeT 0);
  1082     val truncate_decl = (truncateN, rec_schemeT 0 --> recT 0);
  1083 
  1084 
  1085     (* prepare definitions *)
  1086 
  1087     (*record (scheme) type abbreviation*)
  1088     val recordT_specs =
  1089       [(suffix schemeN bname, alphas @ [zeta], rec_schemeT 0, Syntax.NoSyn),
  1090         (bname, alphas, recT 0, Syntax.NoSyn)];
  1091 
  1092     (*selectors*)
  1093     fun mk_sel_spec (i, c) =
  1094       mk_sel (r_scheme 0) c :== mk_fst (funpow i mk_snd (parent_more (r_scheme 0)));
  1095     val sel_specs =
  1096       ListPair.map mk_sel_spec (idxs, names) @
  1097         [more_part (r_scheme 0) :== funpow len mk_snd (parent_more (r_scheme 0))];
  1098 
  1099     (*updates*)
  1100     val all_sels = mk_named_sels all_names (r_scheme 0);
  1101     fun mk_upd_spec (i, (c, x)) =
  1102       mk_update (r_scheme 0) (c, x) :==
  1103         mk_record (nth_update (c, x) (parent_len + i, all_sels), more_part (r_scheme 0))
  1104     val update_specs =
  1105       ListPair.map mk_upd_spec (idxs, named_vars) @
  1106         [more_part_update (r_scheme 0) more :== mk_record (all_sels, more)];
  1107 
  1108     (*derived operations*)
  1109     val make_spec = Const (full makeN, all_types ---> recT 0) $$ all_vars :==
  1110       mk_record (all_named_vars, HOLogic.unit);
  1111     val fields_spec = Const (full fieldsN, types ---> fieldsT) $$ vars :==
  1112       mk_record (named_vars, HOLogic.unit);
  1113     val extend_spec = Const (full extendN, recT 0 --> moreT --> rec_schemeT 0) $ r 0 $ more :==
  1114       mk_record (mk_named_sels all_names (r 0), more);
  1115     val truncate_spec = Const (full truncateN, rec_schemeT 0 --> recT 0) $ r_scheme 0 :==
  1116       mk_record (all_sels, HOLogic.unit);
  1117 
  1118 
  1119     (* prepare propositions *)
  1120 
  1121     (*selectors*)
  1122     val sel_props =
  1123       map (fn (c, x) => mk_sel (rec_scheme 0) c === x) named_vars @
  1124         [more_part (rec_scheme 0) === more];
  1125 
  1126     (*updates*)
  1127     fun mk_upd_prop (i, (c, T)) =
  1128       let val x' = Free (variant all_xs (base c ^ "'"), T) in
  1129         mk_update (rec_scheme 0) (c, x') ===
  1130           mk_record (nth_update (c, x') (parent_len + i, all_named_vars), more)
  1131       end;
  1132     val update_props =
  1133       ListPair.map mk_upd_prop (idxs, fields) @
  1134         let val more' = Free (variant all_xs (moreN ^ "'"), moreT)
  1135         in [more_part_update (rec_scheme 0) more' === mk_record (all_named_vars, more')] end;
  1136 
  1137     (*equality*)
  1138     fun mk_sel_eq (t, T) =
  1139       let val t' = Term.abstract_over (r_scheme 0, t)
  1140       in Trueprop (HOLogic.eq_const T $ Term.incr_boundvars 1 t' $ t') end;
  1141     val sel_eqs = map2 mk_sel_eq
  1142       (map (mk_sel (r_scheme 0)) all_names @ [more_part (r_scheme 0)], all_types @ [moreT]);
  1143     val equality_prop =
  1144       Term.all (rec_schemeT 0) $ (Abs ("r", rec_schemeT 0,
  1145         Term.all (rec_schemeT 0) $ (Abs ("r'", rec_schemeT 0,
  1146           Logic.list_implies (sel_eqs,
  1147             Trueprop (HOLogic.eq_const (rec_schemeT 0) $ Bound 1 $ Bound 0))))));
  1148 
  1149     (*induct*)
  1150     fun induct_scheme_prop n =
  1151       let val P = Free ("P", rec_schemeT n --> HOLogic.boolT) in
  1152         (All (prune n all_xs_more ~~ prune n all_types_more)
  1153           (Trueprop (P $ rec_scheme n)), Trueprop (P $ r_scheme n))
  1154       end;
  1155     fun induct_prop n =
  1156       let val P = Free ("P", recT n --> HOLogic.boolT) in
  1157         (All (prune n all_xs ~~ prune n all_types) (Trueprop (P $ rec_ n)), Trueprop (P $ r n))
  1158       end;
  1159 
  1160     (*cases*)
  1161     val C = Trueprop (Free (variant all_xs_more "C", HOLogic.boolT));
  1162     fun cases_scheme_prop n =
  1163       All (prune n all_xs_more ~~ prune n all_types_more)
  1164         ((r_scheme n === rec_scheme n) ==> C) ==> C;
  1165     fun cases_prop n = All (prune n all_xs ~~ prune n all_types) ((r n === rec_ n) ==> C) ==> C;
  1166 
  1167     (*split*)
  1168     fun split_scheme_meta_prop n =
  1169       let val P = Free ("P", rec_schemeT n --> Term.propT) in
  1170        equals (Term.propT) $
  1171         (Term.list_all_free ([(rN,rec_schemeT n)],(P $ r_scheme n)))$
  1172         (All (prune n all_xs_more ~~ prune n all_types_more) (P $ rec_scheme n))
  1173       end;
  1174 
  1175     fun split_scheme_object_prop n =
  1176       let val P = Free ("P", rec_schemeT n --> HOLogic.boolT) 
  1177           val ALL = foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) 
  1178       in
  1179 	Trueprop (
  1180            HOLogic.eq_const (HOLogic.boolT) $
  1181             (HOLogic.mk_all ((rN,rec_schemeT n,P $ r_scheme n)))$
  1182             (ALL (prune n all_xs_more ~~ prune n all_types_more,P $ rec_scheme n)))
  1183       end;
  1184 
  1185       fun split_scheme_object_ex_prop n =
  1186       let val P = Free ("P", rec_schemeT n --> HOLogic.boolT) 
  1187           val EX = foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) 
  1188       in
  1189 	Trueprop (
  1190            HOLogic.eq_const (HOLogic.boolT) $
  1191             (HOLogic.mk_exists ((rN,rec_schemeT n,P $ r_scheme n)))$
  1192             (EX (prune n all_xs_more ~~ prune n all_types_more,P $ rec_scheme n)))
  1193       end;
  1194     (* 1st stage: fields_thy *)
  1195 
  1196     val (fields_thy, field_simps, field_injects, field_splits, field_inducts, field_cases) =
  1197       thy
  1198       |> Theory.add_path bname
  1199       |> field_definitions fields names xs alphas zeta moreT more vars named_vars;
  1200 
  1201     val all_field_inducts = flat (map #field_inducts parents) @ field_inducts;
  1202     val all_field_cases = flat (map #field_cases parents) @ field_cases;
  1203     val all_field_splits = flat (map #field_splits parents) @ field_splits
  1204 
  1205     
  1206     (* 2nd stage: defs_thy *)
  1207 
  1208         
  1209    
  1210 
  1211     val (defs_thy, (((sel_defs, update_defs), derived_defs))) =
  1212       fields_thy
  1213       |> Theory.add_trfuns 
  1214            ([],[],record_type_abbr_tr's fields_thy @ field_type_tr's @ field_tr's, [])
  1215       |> add_field_splits (map (suffix field_typeN) names) field_splits
  1216       |> Theory.parent_path
  1217       |> Theory.add_tyabbrs_i recordT_specs
  1218       |> Theory.add_path bname
  1219       |> Theory.add_consts_i
  1220         (map2 (fn ((x, T), mx) => (x, T, mx)) (sel_decls, field_syntax @ [Syntax.NoSyn]))
  1221       |> (Theory.add_consts_i o map Syntax.no_syn)
  1222         (update_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
  1223       |> (PureThy.add_defs_i false o map Thm.no_attributes) sel_specs
  1224       |>>> (PureThy.add_defs_i false o map Thm.no_attributes) update_specs
  1225       |>>> (PureThy.add_defs_i false o map Thm.no_attributes)
  1226         [make_spec, fields_spec, extend_spec, truncate_spec]
  1227       |>> Theory.hide_consts false [full makeN, full fieldsN, full extendN, full truncateN,
  1228         full moreN, full (suffix updateN moreN)];
  1229 
  1230 
  1231     (* 3rd stage: thms_thy *)
  1232 
  1233     val prove_standard = Tactic.prove_standard (Theory.sign_of defs_thy);
  1234     fun prove_simp simps =
  1235       let val tac = simp_all_tac HOL_basic_ss simps
  1236       in fn prop => prove_standard [] [] prop (K tac) end;
  1237 
  1238     val parent_simps = flat (map #simps parents);
  1239     val sel_convs = map (prove_simp (parent_simps @ sel_defs @ field_simps)) sel_props;
  1240     val update_convs = map (prove_simp (parent_simps @ update_defs @ sel_convs)) update_props;
  1241 
  1242     fun induct_scheme n =
  1243       let val (assm, concl) = induct_scheme_prop n in
  1244         prove_standard [] [assm] concl (fn prems =>
  1245           EVERY (map (fn rule => try_param_tac rN rule 1) (prune n all_field_inducts))
  1246           THEN resolve_tac prems 1)
  1247       end;
  1248 
  1249     fun cases_scheme n =
  1250       prove_standard [] [] (cases_scheme_prop n) (fn _ =>
  1251         EVERY (map (fn rule => try_param_tac rN rule 1) (prune n all_field_cases))
  1252         THEN simp_all_tac HOL_basic_ss []);
  1253 
  1254     fun split_scheme_meta n =
  1255       prove_standard [] [] (split_scheme_meta_prop n) (fn _ =>
  1256         Simplifier.full_simp_tac (HOL_basic_ss addsimps all_field_splits) 1);
  1257 
  1258     fun split_scheme_object induct_scheme n =
  1259       prove_standard [] [] (split_scheme_object_prop n) (fn _ =>
  1260          EVERY [rtac iffI 1, 
  1261                 REPEAT (rtac allI 1), etac allE 1, atac 1,
  1262                 rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]);
  1263 
  1264     fun split_scheme_object_ex split_scheme_meta n =
  1265       prove_standard [] [] (split_scheme_object_ex_prop n) (fn _ =>
  1266         fast_simp_tac (claset_of HOL.thy,
  1267                        HOL_basic_ss addsimps [split_scheme_meta]) 1);
  1268        
  1269     val induct_scheme0 = induct_scheme 0;
  1270     val cases_scheme0 = cases_scheme 0;
  1271     val split_scheme_meta0 = split_scheme_meta 0;
  1272     val split_scheme_object0 = split_scheme_object induct_scheme0 0;
  1273     val split_scheme_object_ex0 = split_scheme_object_ex split_scheme_meta0 0;
  1274     val more_induct_scheme = map induct_scheme ancestry;
  1275     val more_cases_scheme = map cases_scheme ancestry;
  1276 
  1277     val (thms_thy, (([sel_convs', update_convs', sel_defs', update_defs', _, 
  1278                       [split_scheme_meta',split_scheme_object',
  1279                        split_scheme_object_ex',split_scheme_free']],
  1280         [induct_scheme', cases_scheme']), [more_induct_scheme', more_cases_scheme'])) =
  1281       defs_thy
  1282       |> (PureThy.add_thmss o map Thm.no_attributes)
  1283        [("select_convs", sel_convs),
  1284         ("update_convs", update_convs),
  1285         ("select_defs", sel_defs),
  1286         ("update_defs", update_defs),
  1287         ("defs", derived_defs),
  1288         ("splits",[split_scheme_meta0,split_scheme_object0,
  1289                    split_scheme_object_ex0,induct_scheme0])]
  1290       |>>> PureThy.add_thms
  1291        [(("induct_scheme", induct_scheme0), induct_type_global (suffix schemeN name)),
  1292         (("cases_scheme", cases_scheme0), cases_type_global (suffix schemeN name))]
  1293       |>>> PureThy.add_thmss
  1294         [(("more_induct_scheme", more_induct_scheme), induct_type_global ""),
  1295          (("more_cases_scheme", more_cases_scheme), cases_type_global "")];
  1296 
  1297 
  1298     (* 4th stage: more_thms_thy *)
  1299 
  1300     val prove_standard = Tactic.prove_standard (Theory.sign_of thms_thy);
  1301 
  1302     fun induct (n, scheme) =
  1303       let val (assm, concl) = induct_prop n in
  1304         prove_standard [] [assm] concl (fn prems =>
  1305           res_inst_tac [(rN, rN)] scheme 1
  1306           THEN try_param_tac "more" unit_induct 1
  1307           THEN resolve_tac prems 1)
  1308       end;
  1309 
  1310     fun cases (n, scheme) =
  1311       prove_standard [] [] (cases_prop n) (fn _ =>
  1312         res_inst_tac [(rN, rN)] scheme 1
  1313         THEN simp_all_tac HOL_basic_ss [unit_all_eq1]);
  1314 
  1315     val induct0 = induct (0, induct_scheme');
  1316     val cases0 = cases (0, cases_scheme');
  1317     val more_induct = map induct (ancestry ~~ more_induct_scheme');
  1318     val more_cases = map cases (ancestry ~~ more_cases_scheme');
  1319 
  1320     val equality = prove_standard [] [] equality_prop (fn _ =>
  1321       fn st => let val [r, r'] = map #1 (rev (Tactic.innermost_params 1 st)) in
  1322         st |> (res_inst_tac [(rN, r)] cases_scheme' 1
  1323         THEN res_inst_tac [(rN, r')] cases_scheme' 1
  1324         THEN simp_all_tac HOL_basic_ss (parent_simps @ sel_convs))
  1325       end);
  1326 
  1327     val (more_thms_thy, [_, _, equality']) =
  1328       thms_thy |> PureThy.add_thms
  1329        [(("induct", induct0), induct_type_global name),
  1330         (("cases", cases0), cases_type_global name),
  1331         (("equality", equality), [ContextRules.intro_bang_global None])]
  1332       |>> (#1 oo PureThy.add_thmss)
  1333         [(("more_induct", more_induct), induct_type_global ""),
  1334          (("more_cases", more_cases), cases_type_global "")];
  1335 
  1336     val simps = sel_convs' @ update_convs';
  1337     val iffs = field_injects;
  1338 
  1339     val more_thms_thy' =
  1340       more_thms_thy |> (#1 oo PureThy.add_thmss)
  1341         [(("simps", simps), [Simplifier.simp_add_global]),
  1342          (("iffs", iffs), [iff_add_global])];
  1343 
  1344 
  1345     (* 5th stage: final_thy *)
  1346 
  1347     val final_thy =
  1348       more_thms_thy'
  1349       |> put_record name (make_record_info args parent fields field_inducts field_cases
  1350           field_splits (field_simps @ simps))
  1351       |> put_sel_upd (names @ [full_moreN]) simps
  1352       |> add_record_equalities (snd (split_last names)) equality'
  1353       |> add_record_splits (snd (split_last names)) 
  1354                            (split_scheme_meta',split_scheme_object',
  1355                             split_scheme_object_ex',split_scheme_free')
  1356       |> Theory.parent_path;
  1357 
  1358   in (final_thy, {simps = simps, iffs = iffs}) end;
  1359 
  1360 
  1361 
  1362 (** theory extender interface **)
  1363 
  1364 (* prepare arguments *)
  1365 
  1366 (*note: read_raw_typ avoids expanding type abbreviations*)
  1367 fun read_raw_parent sign s =
  1368   (case Sign.read_raw_typ (sign, K None) s handle TYPE (msg, _, _) => error msg of
  1369     Type (name, Ts) => (Ts, name)
  1370   | _ => error ("Bad parent record specification: " ^ quote s));
  1371 
  1372 fun read_typ sign (env, s) =
  1373   let
  1374     fun def_sort (x, ~1) = assoc (env, x)
  1375       | def_sort _ = None;
  1376     val T = Type.no_tvars (Sign.read_typ (sign, def_sort) s) handle TYPE (msg, _, _) => error msg;
  1377   in (Term.add_typ_tfrees (T, env), T) end;
  1378 
  1379 fun cert_typ sign (env, raw_T) =
  1380   let val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle TYPE (msg, _, _) => error msg
  1381   in (Term.add_typ_tfrees (T, env), T) end;
  1382 
  1383 
  1384 (* add_record *)
  1385 
  1386 (*we do all preparations and error checks here, deferring the real
  1387   work to record_definition*)
  1388 
  1389 fun gen_add_record prep_typ prep_raw_parent (params, bname) raw_parent raw_fields thy =
  1390   let
  1391     val _ = Theory.requires thy "Record" "record definitions";
  1392     val sign = Theory.sign_of thy;
  1393     val _ = message ("Defining record " ^ quote bname ^ " ...");
  1394 
  1395 
  1396     (* parents *)
  1397 
  1398     fun prep_inst T = snd (cert_typ sign ([], T));
  1399 
  1400     val parent = apsome (apfst (map prep_inst) o prep_raw_parent sign) raw_parent
  1401       handle ERROR => error ("The error(s) above in parent record specification");
  1402     val parents = add_parents thy parent [];
  1403 
  1404     val init_env =
  1405       (case parent of
  1406         None => []
  1407       | Some (types, _) => foldr Term.add_typ_tfrees (types, []));
  1408 
  1409 
  1410     (* fields *)
  1411 
  1412     fun prep_field (env, (c, raw_T, mx)) =
  1413       let val (env', T) = prep_typ sign (env, raw_T) handle ERROR =>
  1414         error ("The error(s) above occured in field " ^ quote c)
  1415       in (env', (c, T, mx)) end;
  1416 
  1417     val (envir, bfields) = foldl_map prep_field (init_env, raw_fields);
  1418     val envir_names = map fst envir;
  1419 
  1420 
  1421     (* args *)
  1422 
  1423     val defaultS = Sign.defaultS sign;
  1424     val args = map (fn x => (x, if_none (assoc (envir, x)) defaultS)) params;
  1425 
  1426 
  1427     (* errors *)
  1428 
  1429     val name = Sign.full_name sign bname;
  1430     val err_dup_record =
  1431       if is_none (get_record thy name) then []
  1432       else ["Duplicate definition of record " ^ quote name];
  1433 
  1434     val err_dup_parms =
  1435       (case duplicates params of
  1436         [] => []
  1437       | dups => ["Duplicate parameter(s) " ^ commas dups]);
  1438 
  1439     val err_extra_frees =
  1440       (case gen_rems (op =) (envir_names, params) of
  1441         [] => []
  1442       | extras => ["Extra free type variable(s) " ^ commas extras]);
  1443 
  1444     val err_no_fields = if null bfields then ["No fields present"] else [];
  1445 
  1446     val err_dup_fields =
  1447       (case duplicates (map #1 bfields) of
  1448         [] => []
  1449       | dups => ["Duplicate field(s) " ^ commas_quote dups]);
  1450 
  1451     val err_bad_fields =
  1452       if forall (not_equal moreN o #1) bfields then []
  1453       else ["Illegal field name " ^ quote moreN];
  1454 
  1455     val err_dup_sorts =
  1456       (case duplicates envir_names of
  1457         [] => []
  1458       | dups => ["Inconsistent sort constraints for " ^ commas dups]);
  1459 
  1460     val errs =
  1461       err_dup_record @ err_dup_parms @ err_extra_frees @ err_no_fields @
  1462       err_dup_fields @ err_bad_fields @ err_dup_sorts;
  1463   in
  1464     if null errs then () else error (cat_lines errs);
  1465     thy |> record_definition (args, bname) parent parents bfields
  1466   end
  1467   handle ERROR => error ("Failed to define record " ^ quote bname);
  1468 
  1469 val add_record = gen_add_record read_typ read_raw_parent;
  1470 val add_record_i = gen_add_record cert_typ (K I);
  1471 
  1472 
  1473 (** package setup **)
  1474 
  1475 (* setup theory *)
  1476 
  1477 val setup =
  1478  [RecordsData.init,
  1479   Theory.add_trfuns ([], parse_translation, [], []),
  1480   Method.add_methods [record_split_method],
  1481   Simplifier.change_simpset_of Simplifier.addsimprocs
  1482     [record_simproc, record_eq_simproc]];
  1483 
  1484 
  1485 (* outer syntax *)
  1486 
  1487 local structure P = OuterParse and K = OuterSyntax.Keyword in
  1488 
  1489 val record_decl =
  1490   P.type_args -- P.name --
  1491     (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const);
  1492 
  1493 val recordP =
  1494   OuterSyntax.command "record" "define extensible record" K.thy_decl
  1495     (record_decl >> (fn (x, (y, z)) => Toplevel.theory (#1 o add_record x y z)));
  1496 
  1497 val _ = OuterSyntax.add_parsers [recordP];
  1498 
  1499 end;
  1500 
  1501 end;
  1502 
  1503 structure BasicRecordPackage: BASIC_RECORD_PACKAGE = RecordPackage;
  1504 open BasicRecordPackage;