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