|
1 (* Title: FOL/int-prover |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 A naive prover for intuitionistic logic |
|
7 |
|
8 BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use Int.fast_tac ... |
|
9 |
|
10 Completeness (for propositional logic) is proved in |
|
11 |
|
12 Roy Dyckhoff. |
|
13 Contraction-Free Sequent Calculi for Intuitionistic Logic. |
|
14 J. Symbolic Logic (in press) |
|
15 *) |
|
16 |
|
17 signature INT_PROVER = |
|
18 sig |
|
19 val best_tac: int -> tactic |
|
20 val fast_tac: int -> tactic |
|
21 val inst_step_tac: int -> tactic |
|
22 val safe_step_tac: int -> tactic |
|
23 val safe_brls: (bool * thm) list |
|
24 val safe_tac: tactic |
|
25 val step_tac: int -> tactic |
|
26 val haz_brls: (bool * thm) list |
|
27 end; |
|
28 |
|
29 |
|
30 structure Int : INT_PROVER = |
|
31 struct |
|
32 |
|
33 (*Negation is treated as a primitive symbol, with rules notI (introduction), |
|
34 not_to_imp (converts the assumption ~P to P-->False), and not_impE |
|
35 (handles double negations). Could instead rewrite by not_def as the first |
|
36 step of an intuitionistic proof. |
|
37 *) |
|
38 val safe_brls = sort lessb |
|
39 [ (true,FalseE), (false,TrueI), (false,refl), |
|
40 (false,impI), (false,notI), (false,allI), |
|
41 (true,conjE), (true,exE), |
|
42 (false,conjI), (true,conj_impE), |
|
43 (true,disj_impE), (true,ex_impE), |
|
44 (true,disjE), (false,iffI), (true,iffE), (true,not_to_imp) ]; |
|
45 |
|
46 val haz_brls = |
|
47 [ (false,disjI1), (false,disjI2), (false,exI), |
|
48 (true,allE), (true,not_impE), (true,imp_impE), (true,iff_impE), |
|
49 (true,all_impE), (true,impE) ]; |
|
50 |
|
51 (*0 subgoals vs 1 or more: the p in safep is for positive*) |
|
52 val (safe0_brls, safep_brls) = |
|
53 partition (apl(0,op=) o subgoals_of_brl) safe_brls; |
|
54 |
|
55 (*Attack subgoals using safe inferences -- matching, not resolution*) |
|
56 val safe_step_tac = FIRST' [eq_assume_tac, |
|
57 eq_mp_tac, |
|
58 bimatch_tac safe0_brls, |
|
59 hyp_subst_tac, |
|
60 bimatch_tac safep_brls] ; |
|
61 |
|
62 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) |
|
63 val safe_tac = DETERM (REPEAT_FIRST safe_step_tac); |
|
64 |
|
65 (*These steps could instantiate variables and are therefore unsafe.*) |
|
66 val inst_step_tac = |
|
67 assume_tac APPEND' mp_tac APPEND' |
|
68 biresolve_tac (safe0_brls @ safep_brls); |
|
69 |
|
70 (*One safe or unsafe step. *) |
|
71 fun step_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_brls i]; |
|
72 |
|
73 (*Dumb but fast*) |
|
74 val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1)); |
|
75 |
|
76 (*Slower but smarter than fast_tac*) |
|
77 val best_tac = |
|
78 SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac 1)); |
|
79 |
|
80 end; |
|
81 |