82 val haz_step_tac : claset -> int -> tactic |
82 val haz_step_tac : claset -> int -> tactic |
83 val joinrules : thm list * thm list -> (bool * thm) list |
83 val joinrules : thm list * thm list -> (bool * thm) list |
84 val mp_tac : int -> tactic |
84 val mp_tac : int -> tactic |
85 val safe_tac : claset -> tactic |
85 val safe_tac : claset -> tactic |
86 val safe_step_tac : claset -> int -> tactic |
86 val safe_step_tac : claset -> int -> tactic |
|
87 val clarify_tac : claset -> int -> tactic |
|
88 val clarify_step_tac : claset -> int -> tactic |
87 val step_tac : claset -> int -> tactic |
89 val step_tac : claset -> int -> tactic |
88 val slow_step_tac : claset -> int -> tactic |
90 val slow_step_tac : claset -> int -> tactic |
89 val swap : thm (* ~P ==> (~Q ==> P) ==> Q *) |
91 val swap : thm (* ~P ==> (~Q ==> P) ==> Q *) |
90 val swapify : thm list -> thm list |
92 val swapify : thm list -> thm list |
91 val swap_res_tac : thm list -> int -> tactic |
93 val swap_res_tac : thm list -> int -> tactic |
100 val AddSDs : thm list -> unit |
102 val AddSDs : thm list -> unit |
101 val AddSEs : thm list -> unit |
103 val AddSEs : thm list -> unit |
102 val AddSIs : thm list -> unit |
104 val AddSIs : thm list -> unit |
103 val Delrules : thm list -> unit |
105 val Delrules : thm list -> unit |
104 val Safe_step_tac : int -> tactic |
106 val Safe_step_tac : int -> tactic |
|
107 val Clarify_tac : int -> tactic |
|
108 val Clarify_step_tac : int -> tactic |
105 val Step_tac : int -> tactic |
109 val Step_tac : int -> tactic |
106 val Fast_tac : int -> tactic |
110 val Fast_tac : int -> tactic |
107 val Best_tac : int -> tactic |
111 val Best_tac : int -> tactic |
108 val Slow_tac : int -> tactic |
112 val Slow_tac : int -> tactic |
109 val Slow_best_tac : int -> tactic |
113 val Slow_best_tac : int -> tactic |
529 |
533 |
530 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) |
534 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) |
531 fun safe_tac cs = REPEAT_DETERM_FIRST |
535 fun safe_tac cs = REPEAT_DETERM_FIRST |
532 (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i)); |
536 (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i)); |
533 |
537 |
|
538 |
|
539 (*** Clarify_tac: do safe steps without causing branching ***) |
|
540 |
|
541 fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n); |
|
542 |
|
543 (*version of bimatch_from_nets_tac that only applies rules that |
|
544 create precisely n subgoals.*) |
|
545 fun n_bimatch_from_nets_tac n = |
|
546 biresolution_from_nets_tac (orderlist o filter (nsubgoalsP n)) true; |
|
547 |
|
548 fun eq_contr_tac i = ematch_tac [not_elim] i THEN eq_assume_tac i; |
|
549 val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac; |
|
550 |
|
551 (*Two-way branching is allowed only if one of the branches immediately closes*) |
|
552 fun bimatch2_tac netpair i = |
|
553 n_bimatch_from_nets_tac 2 netpair i THEN |
|
554 (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i+1)); |
|
555 |
|
556 (*Attack subgoals using safe inferences -- matching, not resolution*) |
|
557 fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = |
|
558 getSWrapper cs (FIRST' [ |
|
559 eq_assume_contr_tac, |
|
560 bimatch_from_nets_tac safe0_netpair, |
|
561 FIRST' hyp_subst_tacs, |
|
562 n_bimatch_from_nets_tac 1 safep_netpair, |
|
563 bimatch2_tac safep_netpair]); |
|
564 |
|
565 fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1)); |
|
566 |
|
567 |
|
568 (*** Unsafe steps instantiate variables or lose information ***) |
|
569 |
534 (*But these unsafe steps at least solve a subgoal!*) |
570 (*But these unsafe steps at least solve a subgoal!*) |
535 fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = |
571 fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = |
536 assume_tac APPEND' |
572 assume_tac APPEND' |
537 contr_tac APPEND' |
573 contr_tac APPEND' |
538 biresolve_from_nets_tac safe0_netpair; |
574 biresolve_from_nets_tac safe0_netpair; |
642 |
678 |
643 (*Cannot have Safe_tac, as it takes no arguments; must delay dereferencing!*) |
679 (*Cannot have Safe_tac, as it takes no arguments; must delay dereferencing!*) |
644 |
680 |
645 fun Safe_step_tac i = safe_step_tac (!claset) i; |
681 fun Safe_step_tac i = safe_step_tac (!claset) i; |
646 |
682 |
|
683 fun Clarify_step_tac i = clarify_step_tac (!claset) i; |
|
684 |
|
685 fun Clarify_tac i = clarify_tac (!claset) i; |
|
686 |
647 fun Step_tac i = step_tac (!claset) i; |
687 fun Step_tac i = step_tac (!claset) i; |
648 |
688 |
649 fun Fast_tac i = fast_tac (!claset) i; |
689 fun Fast_tac i = fast_tac (!claset) i; |
650 |
690 |
651 fun Best_tac i = best_tac (!claset) i; |
691 fun Best_tac i = best_tac (!claset) i; |