4 |
4 |
5 A naive prover for intuitionistic logic |
5 A naive prover for intuitionistic logic |
6 |
6 |
7 BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use IntPr.fast_tac ... |
7 BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use IntPr.fast_tac ... |
8 |
8 |
9 Completeness (for propositional logic) is proved in |
9 Completeness (for propositional logic) is proved in |
10 |
10 |
11 Roy Dyckhoff. |
11 Roy Dyckhoff. |
12 Contraction-Free Sequent Calculi for Intuitionistic Logic. |
12 Contraction-Free Sequent Calculi for Intuitionistic Logic. |
13 J. Symbolic Logic 57(3), 1992, pages 795-807. |
13 J. Symbolic Logic 57(3), 1992, pages 795-807. |
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: Proof.context -> int -> tactic |
20 val best_tac: Proof.context -> int -> tactic |
21 val best_dup_tac: Proof.context -> int -> tactic |
21 val best_dup_tac: Proof.context -> int -> tactic |
22 val fast_tac: Proof.context -> int -> tactic |
22 val fast_tac: Proof.context -> int -> tactic |
23 val inst_step_tac: Proof.context -> int -> tactic |
23 val inst_step_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 |
37 (*Negation is treated as a primitive symbol, with rules notI (introduction), |
37 (*Negation is treated as a primitive symbol, with rules notI (introduction), |
38 not_to_imp (converts the assumption ~P to P-->False), and not_impE |
38 not_to_imp (converts the assumption ~P to P-->False), and not_impE |
39 (handles double negations). Could instead rewrite by not_def as the first |
39 (handles double negations). Could instead rewrite by not_def as the first |
42 val safe_brls = sort (make_ord lessb) |
42 val safe_brls = sort (make_ord lessb) |
43 [ (true, @{thm FalseE}), (false, @{thm TrueI}), (false, @{thm refl}), |
43 [ (true, @{thm FalseE}), (false, @{thm TrueI}), (false, @{thm refl}), |
44 (false, @{thm impI}), (false, @{thm notI}), (false, @{thm allI}), |
44 (false, @{thm impI}), (false, @{thm notI}), (false, @{thm allI}), |
45 (true, @{thm conjE}), (true, @{thm exE}), |
45 (true, @{thm conjE}), (true, @{thm exE}), |
46 (false, @{thm conjI}), (true, @{thm conj_impE}), |
46 (false, @{thm conjI}), (true, @{thm conj_impE}), |
47 (true, @{thm disj_impE}), (true, @{thm disjE}), |
47 (true, @{thm disj_impE}), (true, @{thm disjE}), |
48 (false, @{thm iffI}), (true, @{thm iffE}), (true, @{thm not_to_imp}) ]; |
48 (false, @{thm iffI}), (true, @{thm iffE}), (true, @{thm not_to_imp}) ]; |
49 |
49 |
50 val haz_brls = |
50 val haz_brls = |
51 [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}), |
51 [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}), |
52 (true, @{thm allE}), (true, @{thm not_impE}), (true, @{thm imp_impE}), (true, @{thm iff_impE}), |
52 (true, @{thm allE}), (true, @{thm not_impE}), (true, @{thm imp_impE}), (true, @{thm iff_impE}), |
53 (true, @{thm all_impE}), (true, @{thm ex_impE}), (true, @{thm impE}) ]; |
53 (true, @{thm all_impE}), (true, @{thm ex_impE}), (true, @{thm impE}) ]; |
54 |
54 |
55 val haz_dup_brls = |
55 val haz_dup_brls = |
56 [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}), |
56 [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}), |
63 |
63 |
64 (*Attack subgoals using safe inferences -- matching, not resolution*) |
64 (*Attack subgoals using safe inferences -- matching, not resolution*) |
65 fun safe_step_tac ctxt = |
65 fun safe_step_tac ctxt = |
66 FIRST' [ |
66 FIRST' [ |
67 eq_assume_tac, |
67 eq_assume_tac, |
68 eq_mp_tac, |
68 eq_mp_tac ctxt, |
69 bimatch_tac ctxt safe0_brls, |
69 bimatch_tac ctxt safe0_brls, |
70 hyp_subst_tac ctxt, |
70 hyp_subst_tac ctxt, |
71 bimatch_tac ctxt safep_brls]; |
71 bimatch_tac ctxt safep_brls]; |
72 |
72 |
73 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) |
73 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) |
74 fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt); |
74 fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt); |
75 |
75 |
76 (*These steps could instantiate variables and are therefore unsafe.*) |
76 (*These steps could instantiate variables and are therefore unsafe.*) |
77 fun inst_step_tac ctxt = |
77 fun inst_step_tac ctxt = |
78 assume_tac ctxt APPEND' mp_tac APPEND' |
78 assume_tac ctxt APPEND' mp_tac ctxt APPEND' |
79 biresolve_tac ctxt (safe0_brls @ safep_brls); |
79 biresolve_tac ctxt (safe0_brls @ safep_brls); |
80 |
80 |
81 (*One safe or unsafe step. *) |
81 (*One safe or unsafe step. *) |
82 fun step_tac ctxt i = |
82 fun step_tac ctxt i = |
83 FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac ctxt haz_brls i]; |
83 FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac ctxt haz_brls i]; |