584 |
580 |
585 fun cs delrules ths = fold delrule ths cs; |
581 fun cs delrules ths = fold delrule ths cs; |
586 |
582 |
587 |
583 |
588 (*** Modifying the wrapper tacticals ***) |
584 (*** Modifying the wrapper tacticals ***) |
589 fun update_swrappers |
585 fun map_swrappers f |
590 (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
586 (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
591 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f = |
587 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
592 CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, |
588 CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, |
593 swrappers = f swrappers, uwrappers = uwrappers, |
589 swrappers = f swrappers, uwrappers = uwrappers, |
594 safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, |
590 safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, |
595 haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; |
591 haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; |
596 |
592 |
597 fun update_uwrappers |
593 fun map_uwrappers f |
598 (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
594 (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, |
599 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) f = |
595 safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = |
600 CS{safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, |
596 CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, |
601 swrappers = swrappers, uwrappers = f uwrappers, |
597 swrappers = swrappers, uwrappers = f uwrappers, |
602 safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, |
598 safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, |
603 haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; |
599 haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; |
604 |
600 |
605 fun overwrite_warn msg (p as (key : string, v)) xs = |
601 fun update_warn msg (p as (key : string, _)) xs = |
606 let |
602 (if AList.defined (op =) xs key then warning msg else (); |
607 fun over ((q as (keyi, _)) :: xs) = |
603 AList.update (op =) p xs); |
608 if keyi = key then p :: xs else q :: over xs |
604 |
609 | over [] = [p]; |
605 fun delete_warn msg (key : string) xs = |
610 in ( |
606 if AList.defined (op =) xs key then AList.delete (op =) key xs |
611 if AList.defined (op =) xs key then warning msg else (); |
607 else (warning msg; xs); |
612 over xs |
|
613 ) end; |
|
614 |
608 |
615 (*Add/replace a safe wrapper*) |
609 (*Add/replace a safe wrapper*) |
616 fun cs addSWrapper new_swrapper = update_swrappers cs |
610 fun cs addSWrapper new_swrapper = map_swrappers |
617 (overwrite_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper); |
611 (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs; |
618 |
612 |
619 (*Add/replace an unsafe wrapper*) |
613 (*Add/replace an unsafe wrapper*) |
620 fun cs addWrapper new_uwrapper = update_uwrappers cs |
614 fun cs addWrapper new_uwrapper = map_uwrappers |
621 (overwrite_warn ("Overwriting unsafe wrapper "^fst new_uwrapper) new_uwrapper); |
615 (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs; |
622 |
616 |
623 (*Remove a safe wrapper*) |
617 (*Remove a safe wrapper*) |
624 fun cs delSWrapper name = update_swrappers cs (fn swrappers => |
618 fun cs delSWrapper name = map_swrappers |
625 let val swrappers' = filter_out (equal name o fst) swrappers in |
619 (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs; |
626 if length swrappers <> length swrappers' then swrappers' |
|
627 else (warning ("No such safe wrapper in claset: "^ name); swrappers) |
|
628 end); |
|
629 |
620 |
630 (*Remove an unsafe wrapper*) |
621 (*Remove an unsafe wrapper*) |
631 fun cs delWrapper name = update_uwrappers cs (fn uwrappers => |
622 fun cs delWrapper name = map_uwrappers |
632 let val uwrappers' = filter_out (equal name o fst) uwrappers in |
623 (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs; |
633 if length uwrappers <> length uwrappers' then uwrappers' |
|
634 else (warning ("No such unsafe wrapper in claset: " ^ name); uwrappers) |
|
635 end); |
|
636 |
624 |
637 (* compose a safe tactic alternatively before/after safe_step_tac *) |
625 (* compose a safe tactic alternatively before/after safe_step_tac *) |
638 fun cs addSbefore (name, tac1) = |
626 fun cs addSbefore (name, tac1) = |
639 cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2); |
627 cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2); |
640 fun cs addSafter (name, tac2) = |
628 fun cs addSafter (name, tac2) = |
656 cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac); |
644 cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac); |
657 |
645 |
658 (*Merge works by adding all new rules of the 2nd claset into the 1st claset. |
646 (*Merge works by adding all new rules of the 2nd claset into the 1st claset. |
659 Merging the term nets may look more efficient, but the rather delicate |
647 Merging the term nets may look more efficient, but the rather delicate |
660 treatment of priority might get muddled up.*) |
648 treatment of priority might get muddled up.*) |
661 fun merge_cs (cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, |
649 fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}, |
662 CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, swrappers, uwrappers, ...}) = |
650 CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2, |
663 let val safeIs' = fold rem_thm safeIs safeIs2 |
651 swrappers, uwrappers, ...}) = |
664 val safeEs' = fold rem_thm safeEs safeEs2 |
652 let |
665 val hazIs' = fold rem_thm hazIs hazIs2 |
653 val safeIs' = fold rem_thm safeIs safeIs2; |
666 val hazEs' = fold rem_thm hazEs hazEs2 |
654 val safeEs' = fold rem_thm safeEs safeEs2; |
667 val cs1 = cs addSIs safeIs' |
655 val hazIs' = fold rem_thm hazIs hazIs2; |
668 addSEs safeEs' |
656 val hazEs' = fold rem_thm hazEs hazEs2; |
669 addIs hazIs' |
657 val cs1 = cs addSIs safeIs' |
670 addEs hazEs' |
658 addSEs safeEs' |
671 val cs2 = update_swrappers cs1 (fn ws => merge_alists ws swrappers); |
659 addIs hazIs' |
672 val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers); |
660 addEs hazEs'; |
673 in cs3 |
661 val cs2 = map_swrappers |
674 end; |
662 (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1; |
|
663 val cs3 = map_uwrappers |
|
664 (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2; |
|
665 in cs3 end; |
675 |
666 |
676 |
667 |
677 (**** Simple tactics for theorem proving ****) |
668 (**** Simple tactics for theorem proving ****) |
678 |
669 |
679 (*Attack subgoals using safe inferences -- matching, not resolution*) |
670 (*Attack subgoals using safe inferences -- matching, not resolution*) |