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 = |
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, |
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 |
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 |
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); |
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, _]), _])) => |
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; |