14 |
14 |
15 The approach was developed independently by Roy Dyckhoff and L C Paulson. |
15 The approach was developed independently by Roy Dyckhoff and L C Paulson. |
16 *) |
16 *) |
17 |
17 |
18 signature INT_PROVER = |
18 signature INT_PROVER = |
19 sig |
19 sig |
20 val best_tac: int -> tactic |
20 val best_tac: Proof.context -> int -> tactic |
21 val best_dup_tac: int -> tactic |
21 val best_dup_tac: Proof.context -> int -> tactic |
22 val fast_tac: int -> tactic |
22 val fast_tac: Proof.context -> int -> tactic |
23 val inst_step_tac: int -> tactic |
23 val inst_step_tac: int -> tactic |
24 val safe_step_tac: int -> tactic |
24 val safe_step_tac: Proof.context -> int -> tactic |
25 val safe_brls: (bool * thm) list |
25 val safe_brls: (bool * thm) list |
26 val safe_tac: tactic |
26 val safe_tac: Proof.context -> tactic |
27 val step_tac: int -> tactic |
27 val step_tac: Proof.context -> int -> tactic |
28 val step_dup_tac: int -> tactic |
28 val step_dup_tac: Proof.context -> int -> tactic |
29 val haz_brls: (bool * thm) list |
29 val haz_brls: (bool * thm) list |
30 val haz_dup_brls: (bool * thm) list |
30 val haz_dup_brls: (bool * thm) list |
31 end; |
31 end; |
32 |
32 |
33 |
33 |
34 structure IntPr : INT_PROVER = |
34 structure IntPr : INT_PROVER = |
35 struct |
35 struct |
36 |
36 |
60 (*0 subgoals vs 1 or more: the p in safep is for positive*) |
60 (*0 subgoals vs 1 or more: the p in safep is for positive*) |
61 val (safe0_brls, safep_brls) = |
61 val (safe0_brls, safep_brls) = |
62 List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls; |
62 List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls; |
63 |
63 |
64 (*Attack subgoals using safe inferences -- matching, not resolution*) |
64 (*Attack subgoals using safe inferences -- matching, not resolution*) |
65 val safe_step_tac = FIRST' [eq_assume_tac, |
65 fun safe_step_tac ctxt = |
66 eq_mp_tac, |
66 FIRST' [ |
67 bimatch_tac safe0_brls, |
67 eq_assume_tac, |
68 hyp_subst_tac, |
68 eq_mp_tac, |
69 bimatch_tac safep_brls] ; |
69 bimatch_tac safe0_brls, |
|
70 hyp_subst_tac ctxt, |
|
71 bimatch_tac safep_brls]; |
70 |
72 |
71 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) |
73 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) |
72 val safe_tac = REPEAT_DETERM_FIRST safe_step_tac; |
74 fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt); |
73 |
75 |
74 (*These steps could instantiate variables and are therefore unsafe.*) |
76 (*These steps could instantiate variables and are therefore unsafe.*) |
75 val inst_step_tac = |
77 val inst_step_tac = |
76 assume_tac APPEND' mp_tac APPEND' |
78 assume_tac APPEND' mp_tac APPEND' |
77 biresolve_tac (safe0_brls @ safep_brls); |
79 biresolve_tac (safe0_brls @ safep_brls); |
78 |
80 |
79 (*One safe or unsafe step. *) |
81 (*One safe or unsafe step. *) |
80 fun step_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_brls i]; |
82 fun step_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_brls i]; |
81 |
83 |
82 fun step_dup_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_dup_brls i]; |
84 fun step_dup_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_dup_brls i]; |
83 |
85 |
84 (*Dumb but fast*) |
86 (*Dumb but fast*) |
85 val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1)); |
87 fun fast_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); |
86 |
88 |
87 (*Slower but smarter than fast_tac*) |
89 (*Slower but smarter than fast_tac*) |
88 val best_tac = |
90 fun best_tac ctxt = |
89 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 ctxt 1)); |
90 |
92 |
91 (*Uses all_dupE: allows multiple use of universal assumptions. VERY slow.*) |
93 (*Uses all_dupE: allows multiple use of universal assumptions. VERY slow.*) |
92 val best_dup_tac = |
94 fun best_dup_tac ctxt = |
93 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac 1)); |
95 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac ctxt 1)); |
94 |
96 |
95 |
97 |
96 end; |
98 end; |
97 |
99 |