17 *) |
17 *) |
18 |
18 |
19 signature INT_PROVER = |
19 signature INT_PROVER = |
20 sig |
20 sig |
21 val best_tac: int -> tactic |
21 val best_tac: int -> tactic |
|
22 val best_dup_tac: int -> tactic |
22 val fast_tac: int -> tactic |
23 val fast_tac: int -> tactic |
23 val inst_step_tac: int -> tactic |
24 val inst_step_tac: int -> tactic |
24 val safe_step_tac: int -> tactic |
25 val safe_step_tac: int -> tactic |
25 val safe_brls: (bool * thm) list |
26 val safe_brls: (bool * thm) list |
26 val safe_tac: tactic |
27 val safe_tac: tactic |
27 val step_tac: int -> tactic |
28 val step_tac: int -> tactic |
|
29 val step_dup_tac: int -> tactic |
28 val haz_brls: (bool * thm) list |
30 val haz_brls: (bool * thm) list |
|
31 val haz_dup_brls: (bool * thm) list |
29 end; |
32 end; |
30 |
33 |
31 |
34 |
32 structure IntPr : INT_PROVER = |
35 structure IntPr : INT_PROVER = |
33 struct |
36 struct |
48 val haz_brls = |
51 val haz_brls = |
49 [ (false,disjI1), (false,disjI2), (false,exI), |
52 [ (false,disjI1), (false,disjI2), (false,exI), |
50 (true,allE), (true,not_impE), (true,imp_impE), (true,iff_impE), |
53 (true,allE), (true,not_impE), (true,imp_impE), (true,iff_impE), |
51 (true,all_impE), (true,ex_impE), (true,impE) ]; |
54 (true,all_impE), (true,ex_impE), (true,impE) ]; |
52 |
55 |
|
56 val haz_dup_brls = |
|
57 [ (false,disjI1), (false,disjI2), (false,exI), |
|
58 (true,all_dupE), (true,not_impE), (true,imp_impE), (true,iff_impE), |
|
59 (true,all_impE), (true,ex_impE), (true,impE) ]; |
|
60 |
53 (*0 subgoals vs 1 or more: the p in safep is for positive*) |
61 (*0 subgoals vs 1 or more: the p in safep is for positive*) |
54 val (safe0_brls, safep_brls) = |
62 val (safe0_brls, safep_brls) = |
55 partition (apl(0,op=) o subgoals_of_brl) safe_brls; |
63 partition (apl(0,op=) o subgoals_of_brl) safe_brls; |
56 |
64 |
57 (*Attack subgoals using safe inferences -- matching, not resolution*) |
65 (*Attack subgoals using safe inferences -- matching, not resolution*) |
70 biresolve_tac (safe0_brls @ safep_brls); |
78 biresolve_tac (safe0_brls @ safep_brls); |
71 |
79 |
72 (*One safe or unsafe step. *) |
80 (*One safe or unsafe step. *) |
73 fun step_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_brls i]; |
81 fun step_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_brls i]; |
74 |
82 |
|
83 fun step_dup_tac i = FIRST [safe_tac, inst_step_tac i, |
|
84 biresolve_tac haz_dup_brls i]; |
|
85 |
75 (*Dumb but fast*) |
86 (*Dumb but fast*) |
76 val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1)); |
87 val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1)); |
77 |
88 |
78 (*Slower but smarter than fast_tac*) |
89 (*Slower but smarter than fast_tac*) |
79 val best_tac = |
90 val best_tac = |
80 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac 1)); |
91 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac 1)); |
81 |
92 |
|
93 (*Uses all_dupE: allows multiple use of universal assumptions. VERY slow.*) |
|
94 val best_dup_tac = |
|
95 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac 1)); |
|
96 |
|
97 |
82 end; |
98 end; |
83 |
99 |