src/HOL/Tools/record.ML
changeset 38012 3ca193a6ae5a
parent 37781 2fbbf0a48cef
child 38252 175a5b4b2c94
equal deleted inserted replaced
37974:d9549f9da779 38012:3ca193a6ae5a
     5     Author:     Thomas Sewell, NICTA
     5     Author:     Thomas Sewell, NICTA
     6 
     6 
     7 Extensible records with structural subtyping.
     7 Extensible records with structural subtyping.
     8 *)
     8 *)
     9 
     9 
    10 signature BASIC_RECORD =
    10 signature RECORD =
    11 sig
    11 sig
    12   type record_info =
    12   val print_type_abbr: bool Unsynchronized.ref
       
    13   val print_type_as_fields: bool Unsynchronized.ref
       
    14   val timing: bool Unsynchronized.ref
       
    15 
       
    16   type info =
    13    {args: (string * sort) list,
    17    {args: (string * sort) list,
    14     parent: (typ list * string) option,
    18     parent: (typ list * string) option,
    15     fields: (string * typ) list,
    19     fields: (string * typ) list,
    16     extension: (string * typ list),
    20     extension: (string * typ list),
    17     ext_induct: thm, ext_inject: thm, ext_surjective: thm, ext_split: thm, ext_def: thm,
    21     ext_induct: thm, ext_inject: thm, ext_surjective: thm, ext_split: thm, ext_def: thm,
    18     select_convs: thm list, update_convs: thm list, select_defs: thm list, update_defs: thm list,
    22     select_convs: thm list, update_convs: thm list, select_defs: thm list, update_defs: thm list,
    19     fold_congs: thm list, unfold_congs: thm list, splits: thm list, defs: thm list,
    23     fold_congs: thm list, unfold_congs: thm list, splits: thm list, defs: thm list,
    20     surjective: thm, equality: thm, induct_scheme: thm, induct: thm, cases_scheme: thm,
    24     surjective: thm, equality: thm, induct_scheme: thm, induct: thm, cases_scheme: thm,
    21     cases: thm, simps: thm list, iffs: thm list}
    25     cases: thm, simps: thm list, iffs: thm list}
    22   val get_record: theory -> string -> record_info option
    26   val get_info: theory -> string -> info option
    23   val the_record: theory -> string -> record_info
    27   val the_info: theory -> string -> info
    24   val record_simproc: simproc
    28   val add_record: bool -> (string * sort) list * binding -> (typ list * string) option ->
    25   val record_eq_simproc: simproc
    29     (binding * typ * mixfix) list -> theory -> theory
    26   val record_upd_simproc: simproc
    30 
    27   val record_split_simproc: (term -> int) -> simproc
       
    28   val record_ex_sel_eq_simproc: simproc
       
    29   val record_split_tac: int -> tactic
       
    30   val record_split_simp_tac: thm list -> (term -> int) -> int -> tactic
       
    31   val record_split_name: string
       
    32   val record_split_wrapper: string * wrapper
       
    33   val print_record_type_abbr: bool Unsynchronized.ref
       
    34   val print_record_type_as_fields: bool Unsynchronized.ref
       
    35 end;
       
    36 
       
    37 signature RECORD =
       
    38 sig
       
    39   include BASIC_RECORD
       
    40   val timing: bool Unsynchronized.ref
       
    41   val updateN: string
       
    42   val ext_typeN: string
       
    43   val extN: string
       
    44   val makeN: string
       
    45   val moreN: string
       
    46   val last_extT: typ -> (string * typ list) option
    31   val last_extT: typ -> (string * typ list) option
    47   val dest_recTs: typ -> (string * typ list) list
    32   val dest_recTs: typ -> (string * typ list) list
    48   val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ)
    33   val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ)
    49   val get_recT_fields: theory -> typ -> (string * typ) list * (string * typ)
    34   val get_recT_fields: theory -> typ -> (string * typ) list * (string * typ)
    50   val get_parent: theory -> string -> (typ list * string) option
    35   val get_parent: theory -> string -> (typ list * string) option
    51   val get_extension: theory -> string -> (string * typ list) option
    36   val get_extension: theory -> string -> (string * typ list) option
    52   val get_extinjects: theory -> thm list
    37   val get_extinjects: theory -> thm list
    53   val get_simpset: theory -> simpset
    38   val get_simpset: theory -> simpset
    54   val print_records: theory -> unit
    39   val simproc: simproc
       
    40   val eq_simproc: simproc
       
    41   val upd_simproc: simproc
       
    42   val split_simproc: (term -> int) -> simproc
       
    43   val ex_sel_eq_simproc: simproc
       
    44   val split_tac: int -> tactic
       
    45   val split_simp_tac: thm list -> (term -> int) -> int -> tactic
       
    46   val split_wrapper: string * wrapper
       
    47 
       
    48   val updateN: string
       
    49   val ext_typeN: string
       
    50   val extN: string
    55   val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list
    51   val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list
    56   val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list
    52   val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list
    57   val add_record: bool -> (string * sort) list * binding -> (typ list * string) option ->
       
    58     (binding * typ * mixfix) list -> theory -> theory
       
    59   val add_record_cmd: bool -> (string * string option) list * binding -> string option ->
       
    60     (binding * string * mixfix) list -> theory -> theory
       
    61   val setup: theory -> theory
    53   val setup: theory -> theory
    62 end;
    54 end;
    63 
    55 
    64 
    56 
    65 signature ISO_TUPLE_SUPPORT =
    57 signature ISO_TUPLE_SUPPORT =
   337 
   329 
   338 (*** extend theory by record definition ***)
   330 (*** extend theory by record definition ***)
   339 
   331 
   340 (** record info **)
   332 (** record info **)
   341 
   333 
   342 (* type record_info and parent_info *)
   334 (* type info and parent_info *)
   343 
   335 
   344 type record_info =
   336 type info =
   345  {args: (string * sort) list,
   337  {args: (string * sort) list,
   346   parent: (typ list * string) option,
   338   parent: (typ list * string) option,
   347   fields: (string * typ) list,
   339   fields: (string * typ) list,
   348   extension: (string * typ list),
   340   extension: (string * typ list),
   349 
   341 
   370   cases: thm,
   362   cases: thm,
   371 
   363 
   372   simps: thm list,
   364   simps: thm list,
   373   iffs: thm list};
   365   iffs: thm list};
   374 
   366 
   375 fun make_record_info args parent fields extension
   367 fun make_info args parent fields extension
   376     ext_induct ext_inject ext_surjective ext_split ext_def
   368     ext_induct ext_inject ext_surjective ext_split ext_def
   377     select_convs update_convs select_defs update_defs fold_congs unfold_congs splits defs
   369     select_convs update_convs select_defs update_defs fold_congs unfold_congs splits defs
   378     surjective equality induct_scheme induct cases_scheme cases
   370     surjective equality induct_scheme induct cases_scheme cases
   379     simps iffs : record_info =
   371     simps iffs : info =
   380  {args = args, parent = parent, fields = fields, extension = extension,
   372  {args = args, parent = parent, fields = fields, extension = extension,
   381   ext_induct = ext_induct, ext_inject = ext_inject, ext_surjective = ext_surjective,
   373   ext_induct = ext_induct, ext_inject = ext_inject, ext_surjective = ext_surjective,
   382   ext_split = ext_split, ext_def = ext_def, select_convs = select_convs,
   374   ext_split = ext_split, ext_def = ext_def, select_convs = select_convs,
   383   update_convs = update_convs, select_defs = select_defs, update_defs = update_defs,
   375   update_convs = update_convs, select_defs = select_defs, update_defs = update_defs,
   384   fold_congs = fold_congs, unfold_congs = unfold_congs, splits = splits, defs = defs,
   376   fold_congs = fold_congs, unfold_congs = unfold_congs, splits = splits, defs = defs,
   397   ext_def = ext_def, induct_scheme = induct_scheme};
   389   ext_def = ext_def, induct_scheme = induct_scheme};
   398 
   390 
   399 
   391 
   400 (* theory data *)
   392 (* theory data *)
   401 
   393 
   402 type record_data =
   394 type data =
   403  {records: record_info Symtab.table,
   395  {records: info Symtab.table,
   404   sel_upd:
   396   sel_upd:
   405    {selectors: (int * bool) Symtab.table,
   397    {selectors: (int * bool) Symtab.table,
   406     updates: string Symtab.table,
   398     updates: string Symtab.table,
   407     simpset: Simplifier.simpset,
   399     simpset: Simplifier.simpset,
   408     defset: Simplifier.simpset,
   400     defset: Simplifier.simpset,
   413   extsplit: thm Symtab.table,  (*maps extension name to split rule*)
   405   extsplit: thm Symtab.table,  (*maps extension name to split rule*)
   414   splits: (thm * thm * thm * thm) Symtab.table,  (*!!, ALL, EX - split-equalities, induct rule*)
   406   splits: (thm * thm * thm * thm) Symtab.table,  (*!!, ALL, EX - split-equalities, induct rule*)
   415   extfields: (string * typ) list Symtab.table,  (*maps extension to its fields*)
   407   extfields: (string * typ) list Symtab.table,  (*maps extension to its fields*)
   416   fieldext: (string * typ list) Symtab.table};  (*maps field to its extension*)
   408   fieldext: (string * typ list) Symtab.table};  (*maps field to its extension*)
   417 
   409 
   418 fun make_record_data
   410 fun make_data
   419     records sel_upd equalities extinjects extsplit splits extfields fieldext =
   411     records sel_upd equalities extinjects extsplit splits extfields fieldext =
   420  {records = records, sel_upd = sel_upd,
   412  {records = records, sel_upd = sel_upd,
   421   equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
   413   equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
   422   extfields = extfields, fieldext = fieldext }: record_data;
   414   extfields = extfields, fieldext = fieldext }: data;
   423 
   415 
   424 structure Records_Data = Theory_Data
   416 structure Records_Data = Theory_Data
   425 (
   417 (
   426   type T = record_data;
   418   type T = data;
   427   val empty =
   419   val empty =
   428     make_record_data Symtab.empty
   420     make_data Symtab.empty
   429       {selectors = Symtab.empty, updates = Symtab.empty,
   421       {selectors = Symtab.empty, updates = Symtab.empty,
   430           simpset = HOL_basic_ss, defset = HOL_basic_ss,
   422           simpset = HOL_basic_ss, defset = HOL_basic_ss,
   431           foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
   423           foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
   432        Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
   424        Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
   433   val extend = I;
   425   val extend = I;
   452      extinjects = extinjects2,
   444      extinjects = extinjects2,
   453      extsplit = extsplit2,
   445      extsplit = extsplit2,
   454      splits = splits2,
   446      splits = splits2,
   455      extfields = extfields2,
   447      extfields = extfields2,
   456      fieldext = fieldext2}) =
   448      fieldext = fieldext2}) =
   457     make_record_data
   449     make_data
   458       (Symtab.merge (K true) (recs1, recs2))
   450       (Symtab.merge (K true) (recs1, recs2))
   459       {selectors = Symtab.merge (K true) (sels1, sels2),
   451       {selectors = Symtab.merge (K true) (sels1, sels2),
   460         updates = Symtab.merge (K true) (upds1, upds2),
   452         updates = Symtab.merge (K true) (upds1, upds2),
   461         simpset = Simplifier.merge_ss (ss1, ss2),
   453         simpset = Simplifier.merge_ss (ss1, ss2),
   462         defset = Simplifier.merge_ss (ds1, ds2),
   454         defset = Simplifier.merge_ss (ds1, ds2),
   470           Thm.eq_thm (c, y) andalso Thm.eq_thm (d, z)) (splits1, splits2))
   462           Thm.eq_thm (c, y) andalso Thm.eq_thm (d, z)) (splits1, splits2))
   471       (Symtab.merge (K true) (extfields1, extfields2))
   463       (Symtab.merge (K true) (extfields1, extfields2))
   472       (Symtab.merge (K true) (fieldext1, fieldext2));
   464       (Symtab.merge (K true) (fieldext1, fieldext2));
   473 );
   465 );
   474 
   466 
   475 fun print_records thy =
       
   476   let
       
   477     val {records = recs, ...} = Records_Data.get thy;
       
   478     val prt_typ = Syntax.pretty_typ_global thy;
       
   479 
       
   480     fun pretty_parent NONE = []
       
   481       | pretty_parent (SOME (Ts, name)) =
       
   482           [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
       
   483 
       
   484     fun pretty_field (c, T) = Pretty.block
       
   485       [Pretty.str (Sign.extern_const thy c), Pretty.str " ::",
       
   486         Pretty.brk 1, Pretty.quote (prt_typ T)];
       
   487 
       
   488     fun pretty_record (name, {args, parent, fields, ...}: record_info) =
       
   489       Pretty.block (Pretty.fbreaks (Pretty.block
       
   490         [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
       
   491         pretty_parent parent @ map pretty_field fields));
       
   492   in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
       
   493 
       
   494 
   467 
   495 (* access 'records' *)
   468 (* access 'records' *)
   496 
   469 
   497 val get_record = Symtab.lookup o #records o Records_Data.get;
   470 val get_info = Symtab.lookup o #records o Records_Data.get;
   498 
   471 
   499 fun the_record thy name =
   472 fun the_info thy name =
   500   (case get_record thy name of
   473   (case get_info thy name of
   501     SOME info => info
   474     SOME info => info
   502   | NONE => error ("Unknown record type " ^ quote name));
   475   | NONE => error ("Unknown record type " ^ quote name));
   503 
   476 
   504 fun put_record name info thy =
   477 fun put_record name info thy =
   505   let
   478   let
   506     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   479     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   507       Records_Data.get thy;
   480       Records_Data.get thy;
   508     val data = make_record_data (Symtab.update (name, info) records)
   481     val data = make_data (Symtab.update (name, info) records)
   509       sel_upd equalities extinjects extsplit splits extfields fieldext;
   482       sel_upd equalities extinjects extsplit splits extfields fieldext;
   510   in Records_Data.put data thy end;
   483   in Records_Data.put data thy end;
   511 
   484 
   512 
   485 
   513 (* access 'sel_upd' *)
   486 (* access 'sel_upd' *)
   536     val sels = map (rpair (depth, false)) names @ [(more, (depth, true))];
   509     val sels = map (rpair (depth, false)) names @ [(more, (depth, true))];
   537     val upds = map (suffix updateN) all ~~ all;
   510     val upds = map (suffix updateN) all ~~ all;
   538 
   511 
   539     val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong},
   512     val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong},
   540       equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy;
   513       equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy;
   541     val data = make_record_data records
   514     val data = make_data records
   542       {selectors = fold Symtab.update_new sels selectors,
   515       {selectors = fold Symtab.update_new sels selectors,
   543         updates = fold Symtab.update_new upds updates,
   516         updates = fold Symtab.update_new upds updates,
   544         simpset = Simplifier.addsimps (simpset, simps),
   517         simpset = Simplifier.addsimps (simpset, simps),
   545         defset = Simplifier.addsimps (defset, defs),
   518         defset = Simplifier.addsimps (defset, defs),
   546         foldcong = foldcong addcongs folds,
   519         foldcong = foldcong addcongs folds,
   549   in Records_Data.put data thy end;
   522   in Records_Data.put data thy end;
   550 
   523 
   551 
   524 
   552 (* access 'equalities' *)
   525 (* access 'equalities' *)
   553 
   526 
   554 fun add_record_equalities name thm thy =
   527 fun add_equalities name thm thy =
   555   let
   528   let
   556     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   529     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   557       Records_Data.get thy;
   530       Records_Data.get thy;
   558     val data = make_record_data records sel_upd
   531     val data = make_data records sel_upd
   559       (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext;
   532       (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext;
   560   in Records_Data.put data thy end;
   533   in Records_Data.put data thy end;
   561 
   534 
   562 val get_equalities = Symtab.lookup o #equalities o Records_Data.get;
   535 val get_equalities = Symtab.lookup o #equalities o Records_Data.get;
   563 
   536 
   567 fun add_extinjects thm thy =
   540 fun add_extinjects thm thy =
   568   let
   541   let
   569     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   542     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   570       Records_Data.get thy;
   543       Records_Data.get thy;
   571     val data =
   544     val data =
   572       make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
   545       make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
   573         extsplit splits extfields fieldext;
   546         extsplit splits extfields fieldext;
   574   in Records_Data.put data thy end;
   547   in Records_Data.put data thy end;
   575 
   548 
   576 val get_extinjects = rev o #extinjects o Records_Data.get;
   549 val get_extinjects = rev o #extinjects o Records_Data.get;
   577 
   550 
   581 fun add_extsplit name thm thy =
   554 fun add_extsplit name thm thy =
   582   let
   555   let
   583     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   556     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   584       Records_Data.get thy;
   557       Records_Data.get thy;
   585     val data =
   558     val data =
   586       make_record_data records sel_upd equalities extinjects
   559       make_data records sel_upd equalities extinjects
   587         (Symtab.update_new (name, thm) extsplit) splits extfields fieldext;
   560         (Symtab.update_new (name, thm) extsplit) splits extfields fieldext;
   588   in Records_Data.put data thy end;
   561   in Records_Data.put data thy end;
   589 
   562 
   590 
   563 
   591 (* access 'splits' *)
   564 (* access 'splits' *)
   592 
   565 
   593 fun add_record_splits name thmP thy =
   566 fun add_splits name thmP thy =
   594   let
   567   let
   595     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   568     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   596       Records_Data.get thy;
   569       Records_Data.get thy;
   597     val data =
   570     val data =
   598       make_record_data records sel_upd equalities extinjects extsplit
   571       make_data records sel_upd equalities extinjects extsplit
   599         (Symtab.update_new (name, thmP) splits) extfields fieldext;
   572         (Symtab.update_new (name, thmP) splits) extfields fieldext;
   600   in Records_Data.put data thy end;
   573   in Records_Data.put data thy end;
   601 
   574 
   602 val get_splits = Symtab.lookup o #splits o Records_Data.get;
   575 val get_splits = Symtab.lookup o #splits o Records_Data.get;
   603 
   576 
   613 fun add_extfields name fields thy =
   586 fun add_extfields name fields thy =
   614   let
   587   let
   615     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   588     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   616       Records_Data.get thy;
   589       Records_Data.get thy;
   617     val data =
   590     val data =
   618       make_record_data records sel_upd equalities extinjects extsplit splits
   591       make_data records sel_upd equalities extinjects extsplit splits
   619         (Symtab.update_new (name, fields) extfields) fieldext;
   592         (Symtab.update_new (name, fields) extfields) fieldext;
   620   in Records_Data.put data thy end;
   593   in Records_Data.put data thy end;
   621 
   594 
   622 val get_extfields = Symtab.lookup o #extfields o Records_Data.get;
   595 val get_extfields = Symtab.lookup o #extfields o Records_Data.get;
   623 
   596 
   653     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   626     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   654       Records_Data.get thy;
   627       Records_Data.get thy;
   655     val fieldext' =
   628     val fieldext' =
   656       fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
   629       fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
   657     val data =
   630     val data =
   658       make_record_data records sel_upd equalities extinjects
   631       make_data records sel_upd equalities extinjects
   659         extsplit splits extfields fieldext';
   632         extsplit splits extfields fieldext';
   660   in Records_Data.put data thy end;
   633   in Records_Data.put data thy end;
   661 
   634 
   662 val get_fieldext = Symtab.lookup o #fieldext o Records_Data.get;
   635 val get_fieldext = Symtab.lookup o #fieldext o Records_Data.get;
   663 
   636 
   668   | add_parents thy (SOME (types, name)) parents =
   641   | add_parents thy (SOME (types, name)) parents =
   669       let
   642       let
   670         fun err msg = error (msg ^ " parent record " ^ quote name);
   643         fun err msg = error (msg ^ " parent record " ^ quote name);
   671 
   644 
   672         val {args, parent, fields, extension, induct_scheme, ext_def, ...} =
   645         val {args, parent, fields, extension, induct_scheme, ext_def, ...} =
   673           (case get_record thy name of SOME info => info | NONE => err "Unknown");
   646           (case get_info thy name of SOME info => info | NONE => err "Unknown");
   674         val _ = if length types <> length args then err "Bad number of arguments for" else ();
   647         val _ = if length types <> length args then err "Bad number of arguments for" else ();
   675 
   648 
   676         fun bad_inst ((x, S), T) =
   649         fun bad_inst ((x, S), T) =
   677           if Sign.of_sort thy (T, S) then NONE else SOME x
   650           if Sign.of_sort thy (T, S) then NONE else SOME x
   678         val bads = map_filter bad_inst (args ~~ types);
   651         val bads = map_filter bad_inst (args ~~ types);
   835 end;
   808 end;
   836 
   809 
   837 
   810 
   838 (* print translations *)
   811 (* print translations *)
   839 
   812 
   840 val print_record_type_abbr = Unsynchronized.ref true;
   813 val print_type_abbr = Unsynchronized.ref true;
   841 val print_record_type_as_fields = Unsynchronized.ref true;
   814 val print_type_as_fields = Unsynchronized.ref true;
   842 
   815 
   843 
   816 
   844 local
   817 local
   845 
   818 
   846 (* FIXME early extern (!??) *)
   819 (* FIXME early extern (!??) *)
   884 
   857 
   885     val (fields, (_, moreT)) = split_last (strip_fields T);
   858     val (fields, (_, moreT)) = split_last (strip_fields T);
   886     val _ = null fields andalso raise Match;
   859     val _ = null fields andalso raise Match;
   887     val u = foldr1 field_types_tr' (map (field_type_tr' o apsnd term_of_type) fields);
   860     val u = foldr1 field_types_tr' (map (field_type_tr' o apsnd term_of_type) fields);
   888   in
   861   in
   889     if not (! print_record_type_as_fields) orelse null fields then raise Match
   862     if not (! print_type_as_fields) orelse null fields then raise Match
   890     else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
   863     else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
   891     else Syntax.const @{syntax_const "_record_type_scheme"} $ u $ term_of_type moreT
   864     else Syntax.const @{syntax_const "_record_type_scheme"} $ u $ term_of_type moreT
   892   end;
   865   end;
   893 
   866 
   894 (*try to reconstruct the record name type abbreviation from
   867 (*try to reconstruct the record name type abbreviation from
   904       let val abbrT = Type (name, map (varifyT o TFree) args)
   877       let val abbrT = Type (name, map (varifyT o TFree) args)
   905       in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;
   878       in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;
   906 
   879 
   907     fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
   880     fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
   908   in
   881   in
   909     if ! print_record_type_abbr then
   882     if ! print_type_abbr then
   910       (case last_extT T of
   883       (case last_extT T of
   911         SOME (name, _) =>
   884         SOME (name, _) =>
   912           if name = last_ext then
   885           if name = last_ext then
   913             let val subst = match schemeT T in
   886             let val subst = match schemeT T in
   914               if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree zeta)))
   887               if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree zeta)))
  1173       if null (loose_bnos t) then ((n, kT), (Abs (x, xT, Bound (i + 1)))) else ((n, T), b)
  1146       if null (loose_bnos t) then ((n, kT), (Abs (x, xT, Bound (i + 1)))) else ((n, T), b)
  1174   | K_skeleton n T b _ = ((n, T), b);
  1147   | K_skeleton n T b _ = ((n, T), b);
  1175 
  1148 
  1176 in
  1149 in
  1177 
  1150 
  1178 (* record_simproc *)
  1151 (* simproc *)
  1179 
  1152 
  1180 (*
  1153 (*
  1181   Simplify selections of an record update:
  1154   Simplify selections of an record update:
  1182     (1)  S (S_update k r) = k (S r)
  1155     (1)  S (S_update k r) = k (S r)
  1183     (2)  S (X_update k r) = S r
  1156     (2)  S (X_update k r) = S r
  1189   - If S is a more-selector we have to make sure that the update on component
  1162   - If S is a more-selector we have to make sure that the update on component
  1190     X does not affect the selected subrecord.
  1163     X does not affect the selected subrecord.
  1191   - If X is a more-selector we have to make sure that S is not in the updated
  1164   - If X is a more-selector we have to make sure that S is not in the updated
  1192     subrecord.
  1165     subrecord.
  1193 *)
  1166 *)
  1194 val record_simproc =
  1167 val simproc =
  1195   Simplifier.simproc @{theory HOL} "record_simp" ["x"]
  1168   Simplifier.simproc @{theory HOL} "record_simp" ["x"]
  1196     (fn thy => fn _ => fn t =>
  1169     (fn thy => fn _ => fn t =>
  1197       (case t of
  1170       (case t of
  1198         (sel as Const (s, Type (_, [_, rangeS]))) $
  1171         (sel as Const (s, Type (_, [_, rangeS]))) $
  1199             ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
  1172             ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
  1253         REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
  1226         REPEAT_DETERM (Iso_Tuple_Support.iso_tuple_intros_tac 1) THEN
  1254         TRY (resolve_tac [updacc_cong_idI] 1))
  1227         TRY (resolve_tac [updacc_cong_idI] 1))
  1255   end;
  1228   end;
  1256 
  1229 
  1257 
  1230 
  1258 (* record_upd_simproc *)
  1231 (* upd_simproc *)
  1259 
  1232 
  1260 (*Simplify multiple updates:
  1233 (*Simplify multiple updates:
  1261     (1) "N_update y (M_update g (N_update x (M_update f r))) =
  1234     (1) "N_update y (M_update g (N_update x (M_update f r))) =
  1262           (N_update (y o x) (M_update (g o f) r))"
  1235           (N_update (y o x) (M_update (g o f) r))"
  1263     (2)  "r(|M:= M r|) = r"
  1236     (2)  "r(|M:= M r|) = r"
  1264 
  1237 
  1265   In both cases "more" updates complicate matters: for this reason
  1238   In both cases "more" updates complicate matters: for this reason
  1266   we omit considering further updates if doing so would introduce
  1239   we omit considering further updates if doing so would introduce
  1267   both a more update and an update to a field within it.*)
  1240   both a more update and an update to a field within it.*)
  1268 val record_upd_simproc =
  1241 val upd_simproc =
  1269   Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"]
  1242   Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"]
  1270     (fn thy => fn _ => fn t =>
  1243     (fn thy => fn _ => fn t =>
  1271       let
  1244       let
  1272         (*We can use more-updators with other updators as long
  1245         (*We can use more-updators with other updators as long
  1273           as none of the other updators go deeper than any more
  1246           as none of the other updators go deeper than any more
  1361         val (lhs, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
  1334         val (lhs, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
  1362         val noops' = maps snd (Symtab.dest noops);
  1335         val noops' = maps snd (Symtab.dest noops);
  1363       in
  1336       in
  1364         if simp then
  1337         if simp then
  1365           SOME
  1338           SOME
  1366             (prove_unfold_defs thy noops' [record_simproc]
  1339             (prove_unfold_defs thy noops' [simproc]
  1367               (list_all (vars, Logic.mk_equals (lhs, rhs))))
  1340               (list_all (vars, Logic.mk_equals (lhs, rhs))))
  1368         else NONE
  1341         else NONE
  1369       end);
  1342       end);
  1370 
  1343 
  1371 end;
  1344 end;
  1372 
  1345 
  1373 
  1346 
  1374 (* record_eq_simproc *)
  1347 (* eq_simproc *)
  1375 
  1348 
  1376 (*Look up the most specific record-equality.
  1349 (*Look up the most specific record-equality.
  1377 
  1350 
  1378  Note on efficiency:
  1351  Note on efficiency:
  1379  Testing equality of records boils down to the test of equality of all components.
  1352  Testing equality of records boils down to the test of equality of all components.
  1380  Therefore the complexity is: #components * complexity for single component.
  1353  Therefore the complexity is: #components * complexity for single component.
  1381  Especially if a record has a lot of components it may be better to split up
  1354  Especially if a record has a lot of components it may be better to split up
  1382  the record first and do simplification on that (record_split_simp_tac).
  1355  the record first and do simplification on that (split_simp_tac).
  1383  e.g. r(|lots of updates|) = x
  1356  e.g. r(|lots of updates|) = x
  1384 
  1357 
  1385              record_eq_simproc          record_split_simp_tac
  1358              eq_simproc          split_simp_tac
  1386  Complexity: #components * #updates     #updates
  1359  Complexity: #components * #updates     #updates
  1387 *)
  1360 *)
  1388 val record_eq_simproc =
  1361 val eq_simproc =
  1389   Simplifier.simproc @{theory HOL} "record_eq_simp" ["r = s"]
  1362   Simplifier.simproc @{theory HOL} "record_eq_simp" ["r = s"]
  1390     (fn thy => fn _ => fn t =>
  1363     (fn thy => fn _ => fn t =>
  1391       (case t of Const (@{const_name "op ="}, Type (_, [T, _])) $ _ $ _ =>
  1364       (case t of Const (@{const_name "op ="}, Type (_, [T, _])) $ _ $ _ =>
  1392         (case rec_id ~1 T of
  1365         (case rec_id ~1 T of
  1393           "" => NONE
  1366           "" => NONE
  1396               NONE => NONE
  1369               NONE => NONE
  1397             | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
  1370             | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
  1398       | _ => NONE));
  1371       | _ => NONE));
  1399 
  1372 
  1400 
  1373 
  1401 (* record_split_simproc *)
  1374 (* split_simproc *)
  1402 
  1375 
  1403 (*Split quantified occurrences of records, for which P holds.  P can peek on the
  1376 (*Split quantified occurrences of records, for which P holds.  P can peek on the
  1404   subterm starting at the quantified occurrence of the record (including the quantifier):
  1377   subterm starting at the quantified occurrence of the record (including the quantifier):
  1405     P t = 0: do not split
  1378     P t = 0: do not split
  1406     P t = ~1: completely split
  1379     P t = ~1: completely split
  1407     P t > 0: split up to given bound of record extensions.*)
  1380     P t > 0: split up to given bound of record extensions.*)
  1408 fun record_split_simproc P =
  1381 fun split_simproc P =
  1409   Simplifier.simproc @{theory HOL} "record_split_simp" ["x"]
  1382   Simplifier.simproc @{theory HOL} "record_split_simp" ["x"]
  1410     (fn thy => fn _ => fn t =>
  1383     (fn thy => fn _ => fn t =>
  1411       (case t of
  1384       (case t of
  1412         Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
  1385         Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
  1413           if quantifier = @{const_name all} orelse
  1386           if quantifier = @{const_name all} orelse
  1425                         SOME
  1398                         SOME
  1426                           (case quantifier of
  1399                           (case quantifier of
  1427                             @{const_name all} => all_thm
  1400                             @{const_name all} => all_thm
  1428                           | @{const_name All} => All_thm RS eq_reflection
  1401                           | @{const_name All} => All_thm RS eq_reflection
  1429                           | @{const_name Ex} => Ex_thm RS eq_reflection
  1402                           | @{const_name Ex} => Ex_thm RS eq_reflection
  1430                           | _ => error "record_split_simproc"))
  1403                           | _ => error "split_simproc"))
  1431                   else NONE
  1404                   else NONE
  1432                 end)
  1405                 end)
  1433           else NONE
  1406           else NONE
  1434       | _ => NONE));
  1407       | _ => NONE));
  1435 
  1408 
  1436 val record_ex_sel_eq_simproc =
  1409 val ex_sel_eq_simproc =
  1437   Simplifier.simproc @{theory HOL} "record_ex_sel_eq_simproc" ["Ex t"]
  1410   Simplifier.simproc @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
  1438     (fn thy => fn ss => fn t =>
  1411     (fn thy => fn ss => fn t =>
  1439       let
  1412       let
  1440         fun prove prop =
  1413         fun prove prop =
  1441           prove_global true thy [] prop
  1414           prove_global true thy [] prop
  1442             (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
  1415             (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
  1443                 addsimps @{thms simp_thms} addsimprocs [record_split_simproc (K ~1)]) 1);
  1416                 addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1);
  1444 
  1417 
  1445         fun mkeq (lr, Teq, (sel, Tsel), x) i =
  1418         fun mkeq (lr, Teq, (sel, Tsel), x) i =
  1446           if is_selector thy sel then
  1419           if is_selector thy sel then
  1447             let
  1420             let
  1448               val x' =
  1421               val x' =
  1472             handle TERM _ => NONE)
  1445             handle TERM _ => NONE)
  1473         | _ => NONE)
  1446         | _ => NONE)
  1474       end);
  1447       end);
  1475 
  1448 
  1476 
  1449 
  1477 (* record_split_simp_tac *)
  1450 (* split_simp_tac *)
  1478 
  1451 
  1479 (*Split (and simplify) all records in the goal for which P holds.
  1452 (*Split (and simplify) all records in the goal for which P holds.
  1480   For quantified occurrences of a record
  1453   For quantified occurrences of a record
  1481   P can peek on the whole subterm (including the quantifier); for free variables P
  1454   P can peek on the whole subterm (including the quantifier); for free variables P
  1482   can only peek on the variable itself.
  1455   can only peek on the variable itself.
  1483   P t = 0: do not split
  1456   P t = 0: do not split
  1484   P t = ~1: completely split
  1457   P t = ~1: completely split
  1485   P t > 0: split up to given bound of record extensions.*)
  1458   P t > 0: split up to given bound of record extensions.*)
  1486 fun record_split_simp_tac thms P = CSUBGOAL (fn (cgoal, i) =>
  1459 fun split_simp_tac thms P = CSUBGOAL (fn (cgoal, i) =>
  1487   let
  1460   let
  1488     val thy = Thm.theory_of_cterm cgoal;
  1461     val thy = Thm.theory_of_cterm cgoal;
  1489 
  1462 
  1490     val goal = term_of cgoal;
  1463     val goal = term_of cgoal;
  1491     val frees = filter (is_recT o #2) (Term.add_frees goal []);
  1464     val frees = filter (is_recT o #2) (Term.add_frees goal []);
  1523                 | SOME (_, _, _, induct_thm) =>
  1496                 | SOME (_, _, _, induct_thm) =>
  1524                     SOME (mk_split_free_tac free induct_thm i))
  1497                     SOME (mk_split_free_tac free induct_thm i))
  1525               else NONE
  1498               else NONE
  1526             end));
  1499             end));
  1527 
  1500 
  1528     val simprocs = if has_rec goal then [record_split_simproc P] else [];
  1501     val simprocs = if has_rec goal then [split_simproc P] else [];
  1529     val thms' = K_comp_convs @ thms;
  1502     val thms' = K_comp_convs @ thms;
  1530   in
  1503   in
  1531     EVERY split_frees_tacs THEN
  1504     EVERY split_frees_tacs THEN
  1532     Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i
  1505     Simplifier.full_simp_tac (get_simpset thy addsimps thms' addsimprocs simprocs) i
  1533   end);
  1506   end);
  1534 
  1507 
  1535 
  1508 
  1536 (* record_split_tac *)
  1509 (* split_tac *)
  1537 
  1510 
  1538 (*Split all records in the goal, which are quantified by !! or ALL.*)
  1511 (*Split all records in the goal, which are quantified by !! or ALL.*)
  1539 val record_split_tac = CSUBGOAL (fn (cgoal, i) =>
  1512 val split_tac = CSUBGOAL (fn (cgoal, i) =>
  1540   let
  1513   let
  1541     val goal = term_of cgoal;
  1514     val goal = term_of cgoal;
  1542 
  1515 
  1543     val has_rec = exists_Const
  1516     val has_rec = exists_Const
  1544       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
  1517       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
  1548     fun is_all (Const (@{const_name all}, _) $ _) = ~1
  1521     fun is_all (Const (@{const_name all}, _) $ _) = ~1
  1549       | is_all (Const (@{const_name All}, _) $ _) = ~1
  1522       | is_all (Const (@{const_name All}, _) $ _) = ~1
  1550       | is_all _ = 0;
  1523       | is_all _ = 0;
  1551   in
  1524   in
  1552     if has_rec goal then
  1525     if has_rec goal then
  1553       Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i
  1526       Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [split_simproc is_all]) i
  1554     else no_tac
  1527     else no_tac
  1555   end);
  1528   end);
  1556 
  1529 
  1557 
  1530 
  1558 (* wrapper *)
  1531 (* wrapper *)
  1559 
  1532 
  1560 val record_split_name = "record_split_tac";
  1533 val split_name = "record_split_tac";
  1561 val record_split_wrapper = (record_split_name, fn tac => record_split_tac ORELSE' tac);
  1534 val split_wrapper = (split_name, fn tac => split_tac ORELSE' tac);
  1562 
  1535 
  1563 
  1536 
  1564 
  1537 
  1565 (** theory extender interface **)
  1538 (** theory extender interface **)
  1566 
  1539 
  1840     val ct = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.list_all (params, concl)));
  1813     val ct = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.list_all (params, concl)));
  1841     val thm' = Seq.hd (REPEAT (rtac allI 1) (Thm.trivial ct));
  1814     val thm' = Seq.hd (REPEAT (rtac allI 1) (Thm.trivial ct));
  1842   in Thm.implies_elim thm' thm end;
  1815   in Thm.implies_elim thm' thm end;
  1843 
  1816 
  1844 
  1817 
  1845 (* record_definition *)
  1818 (* definition *)
  1846 
  1819 
  1847 fun record_definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
  1820 fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
  1848   let
  1821   let
  1849     val prefix = Binding.name_of binding;
  1822     val prefix = Binding.name_of binding;
  1850     val name = Sign.full_name thy binding;
  1823     val name = Sign.full_name thy binding;
  1851     val full = Sign.full_name_path thy prefix;
  1824     val full = Sign.full_name_path thy prefix;
  1852 
  1825 
  2340       |> PureThy.add_thmss
  2313       |> PureThy.add_thmss
  2341           [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
  2314           [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
  2342            ((Binding.name "iffs", iffs), [iff_add])];
  2315            ((Binding.name "iffs", iffs), [iff_add])];
  2343 
  2316 
  2344     val info =
  2317     val info =
  2345       make_record_info alphas parent fields extension
  2318       make_info alphas parent fields extension
  2346         ext_induct ext_inject ext_surjective ext_split ext_def
  2319         ext_induct ext_inject ext_surjective ext_split ext_def
  2347         sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs'
  2320         sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs'
  2348         surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs';
  2321         surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs';
  2349 
  2322 
  2350     val final_thy =
  2323     val final_thy =
  2351       thms_thy'
  2324       thms_thy'
  2352       |> put_record name info
  2325       |> put_record name info
  2353       |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs')
  2326       |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs')
  2354       |> add_record_equalities extension_id equality'
  2327       |> add_equalities extension_id equality'
  2355       |> add_extinjects ext_inject
  2328       |> add_extinjects ext_inject
  2356       |> add_extsplit extension_name ext_split
  2329       |> add_extsplit extension_name ext_split
  2357       |> add_record_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
  2330       |> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
  2358       |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
  2331       |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
  2359       |> add_fieldext (extension_name, snd extension) (names @ [full_moreN])
  2332       |> add_fieldext (extension_name, snd extension) (names @ [full_moreN])
  2360       |> Sign.restore_naming thy;
  2333       |> Sign.restore_naming thy;
  2361 
  2334 
  2362   in final_thy end;
  2335   in final_thy end;
  2406 
  2379 
  2407     (* errors *)
  2380     (* errors *)
  2408 
  2381 
  2409     val name = Sign.full_name thy binding;
  2382     val name = Sign.full_name thy binding;
  2410     val err_dup_record =
  2383     val err_dup_record =
  2411       if is_none (get_record thy name) then []
  2384       if is_none (get_info thy name) then []
  2412       else ["Duplicate definition of record " ^ quote name];
  2385       else ["Duplicate definition of record " ^ quote name];
  2413 
  2386 
  2414     val spec_frees = fold Term.add_tfreesT (parent_args @ map #2 bfields) [];
  2387     val spec_frees = fold Term.add_tfreesT (parent_args @ map #2 bfields) [];
  2415     val err_extra_frees =
  2388     val err_extra_frees =
  2416       (case subtract (op =) params spec_frees of
  2389       (case subtract (op =) params spec_frees of
  2431 
  2404 
  2432     val errs =
  2405     val errs =
  2433       err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields;
  2406       err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields;
  2434     val _ = if null errs then () else error (cat_lines errs);
  2407     val _ = if null errs then () else error (cat_lines errs);
  2435   in
  2408   in
  2436     thy |> record_definition (params, binding) parent parents bfields
  2409     thy |> definition (params, binding) parent parents bfields
  2437   end
  2410   end
  2438   handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of binding));
  2411   handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of binding));
  2439 
  2412 
  2440 fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy =
  2413 fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy =
  2441   let
  2414   let
  2454 
  2427 
  2455 val setup =
  2428 val setup =
  2456   Sign.add_trfuns ([], parse_translation, [], []) #>
  2429   Sign.add_trfuns ([], parse_translation, [], []) #>
  2457   Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #>
  2430   Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #>
  2458   Simplifier.map_simpset (fn ss =>
  2431   Simplifier.map_simpset (fn ss =>
  2459     ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]);
  2432     ss addsimprocs [simproc, upd_simproc, eq_simproc]);
  2460 
  2433 
  2461 
  2434 
  2462 (* outer syntax *)
  2435 (* outer syntax *)
  2463 
  2436 
  2464 val _ =
  2437 val _ =
  2467       (Parse.$$$ "=" |-- Scan.option (Parse.typ --| Parse.$$$ "+") --
  2440       (Parse.$$$ "=" |-- Scan.option (Parse.typ --| Parse.$$$ "+") --
  2468         Scan.repeat1 Parse.const_binding)
  2441         Scan.repeat1 Parse.const_binding)
  2469     >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z)));
  2442     >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z)));
  2470 
  2443 
  2471 end;
  2444 end;
  2472 
       
  2473 structure Basic_Record: BASIC_RECORD = Record;
       
  2474 open Basic_Record;