author | haftmann |
Sat, 19 Oct 2019 09:15:37 +0000 | |
changeset 70902 | cb161182ce7f |
parent 59529 | d881f5288d5a |
permissions | -rw-r--r-- |
31974 | 1 |
(* Title: FOL/intprover.ML |
1459 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 3 |
Copyright 1992 University of Cambridge |
4 |
||
5 |
A naive prover for intuitionistic logic |
|
6 |
||
2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2572
diff
changeset
|
7 |
BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use IntPr.fast_tac ... |
0 | 8 |
|
59529 | 9 |
Completeness (for propositional logic) is proved in |
0 | 10 |
|
11 |
Roy Dyckhoff. |
|
12 |
Contraction-Free Sequent Calculi for Intuitionistic Logic. |
|
1005 | 13 |
J. Symbolic Logic 57(3), 1992, pages 795-807. |
14 |
||
15 |
The approach was developed independently by Roy Dyckhoff and L C Paulson. |
|
0 | 16 |
*) |
17 |
||
59529 | 18 |
signature INT_PROVER = |
51798 | 19 |
sig |
20 |
val best_tac: Proof.context -> int -> tactic |
|
21 |
val best_dup_tac: Proof.context -> int -> tactic |
|
22 |
val fast_tac: Proof.context -> int -> tactic |
|
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
23 |
val inst_step_tac: Proof.context -> int -> tactic |
51798 | 24 |
val safe_step_tac: Proof.context -> int -> tactic |
0 | 25 |
val safe_brls: (bool * thm) list |
51798 | 26 |
val safe_tac: Proof.context -> tactic |
27 |
val step_tac: Proof.context -> int -> tactic |
|
28 |
val step_dup_tac: Proof.context -> int -> tactic |
|
0 | 29 |
val haz_brls: (bool * thm) list |
5203 | 30 |
val haz_dup_brls: (bool * thm) list |
51798 | 31 |
end; |
0 | 32 |
|
33 |
||
59529 | 34 |
structure IntPr : INT_PROVER = |
0 | 35 |
struct |
36 |
||
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 |
|
39 |
(handles double negations). Could instead rewrite by not_def as the first |
|
40 |
step of an intuitionistic proof. |
|
41 |
*) |
|
4440 | 42 |
val safe_brls = sort (make_ord lessb) |
38500 | 43 |
[ (true, @{thm FalseE}), (false, @{thm TrueI}), (false, @{thm refl}), |
44 |
(false, @{thm impI}), (false, @{thm notI}), (false, @{thm allI}), |
|
45 |
(true, @{thm conjE}), (true, @{thm exE}), |
|
46 |
(false, @{thm conjI}), (true, @{thm conj_impE}), |
|
59529 | 47 |
(true, @{thm disj_impE}), (true, @{thm disjE}), |
38500 | 48 |
(false, @{thm iffI}), (true, @{thm iffE}), (true, @{thm not_to_imp}) ]; |
0 | 49 |
|
50 |
val haz_brls = |
|
59529 | 51 |
[ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}), |
38500 | 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}) ]; |
|
0 | 54 |
|
5203 | 55 |
val haz_dup_brls = |
38500 | 56 |
[ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}), |
57 |
(true, @{thm all_dupE}), (true, @{thm not_impE}), (true, @{thm imp_impE}), (true, @{thm iff_impE}), |
|
58 |
(true, @{thm all_impE}), (true, @{thm ex_impE}), (true, @{thm impE}) ]; |
|
5203 | 59 |
|
0 | 60 |
(*0 subgoals vs 1 or more: the p in safep is for positive*) |
61 |
val (safe0_brls, safep_brls) = |
|
17496 | 62 |
List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls; |
0 | 63 |
|
64 |
(*Attack subgoals using safe inferences -- matching, not resolution*) |
|
51798 | 65 |
fun safe_step_tac ctxt = |
66 |
FIRST' [ |
|
67 |
eq_assume_tac, |
|
59529 | 68 |
eq_mp_tac ctxt, |
58957 | 69 |
bimatch_tac ctxt safe0_brls, |
51798 | 70 |
hyp_subst_tac ctxt, |
58957 | 71 |
bimatch_tac ctxt safep_brls]; |
0 | 72 |
|
73 |
(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) |
|
51798 | 74 |
fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt); |
0 | 75 |
|
76 |
(*These steps could instantiate variables and are therefore unsafe.*) |
|
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
77 |
fun inst_step_tac ctxt = |
59529 | 78 |
assume_tac ctxt APPEND' mp_tac ctxt APPEND' |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
79 |
biresolve_tac ctxt (safe0_brls @ safep_brls); |
0 | 80 |
|
81 |
(*One safe or unsafe step. *) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
82 |
fun step_tac ctxt i = |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
83 |
FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac ctxt haz_brls i]; |
0 | 84 |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
85 |
fun step_dup_tac ctxt i = |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
86 |
FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac ctxt haz_dup_brls i]; |
5203 | 87 |
|
0 | 88 |
(*Dumb but fast*) |
51798 | 89 |
fun fast_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); |
0 | 90 |
|
91 |
(*Slower but smarter than fast_tac*) |
|
51798 | 92 |
fun best_tac ctxt = |
93 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1)); |
|
0 | 94 |
|
5203 | 95 |
(*Uses all_dupE: allows multiple use of universal assumptions. VERY slow.*) |
51798 | 96 |
fun best_dup_tac ctxt = |
97 |
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac ctxt 1)); |
|
5203 | 98 |
|
99 |
||
0 | 100 |
end; |
101 |