author  ballarin 
Wed, 19 Jul 2006 19:25:58 +0200  
changeset 20168  ed7bced29e1b 
parent 17496  26535df536ae 
child 21539  c5cf9243ad62 
permissions  rwrr 
1459  1 
(* Title: FOL/intprover 
0  2 
ID: $Id$ 
1459  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 

6 
A naive prover for intuitionistic logic 

7 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2572
diff
changeset

8 
BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS  use IntPr.fast_tac ... 
0  9 

10 
Completeness (for propositional logic) is proved in 

11 

12 
Roy Dyckhoff. 

13 
ContractionFree Sequent Calculi for Intuitionistic Logic. 

1005  14 
J. Symbolic Logic 57(3), 1992, pages 795807. 
15 

16 
The approach was developed independently by Roy Dyckhoff and L C Paulson. 

0  17 
*) 
18 

19 
signature INT_PROVER = 

20 
sig 

21 
val best_tac: int > tactic 

5203  22 
val best_dup_tac: int > tactic 
0  23 
val fast_tac: int > tactic 
24 
val inst_step_tac: int > tactic 

25 
val safe_step_tac: int > tactic 

26 
val safe_brls: (bool * thm) list 

27 
val safe_tac: tactic 

28 
val step_tac: int > tactic 

5203  29 
val step_dup_tac: int > tactic 
0  30 
val haz_brls: (bool * thm) list 
5203  31 
val haz_dup_brls: (bool * thm) list 
0  32 
end; 
33 

34 

2601
b301958c465d
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2572
diff
changeset

35 
structure IntPr : INT_PROVER = 
0  36 
struct 
37 

38 
(*Negation is treated as a primitive symbol, with rules notI (introduction), 

39 
not_to_imp (converts the assumption ~P to P>False), and not_impE 

40 
(handles double negations). Could instead rewrite by not_def as the first 

41 
step of an intuitionistic proof. 

42 
*) 

4440  43 
val safe_brls = sort (make_ord lessb) 
0  44 
[ (true,FalseE), (false,TrueI), (false,refl), 
45 
(false,impI), (false,notI), (false,allI), 

46 
(true,conjE), (true,exE), 

47 
(false,conjI), (true,conj_impE), 

2572  48 
(true,disj_impE), (true,disjE), 
49 
(false,iffI), (true,iffE), (true,not_to_imp) ]; 

0  50 

51 
val haz_brls = 

52 
[ (false,disjI1), (false,disjI2), (false,exI), 

53 
(true,allE), (true,not_impE), (true,imp_impE), (true,iff_impE), 

2572  54 
(true,all_impE), (true,ex_impE), (true,impE) ]; 
0  55 

5203  56 
val haz_dup_brls = 
57 
[ (false,disjI1), (false,disjI2), (false,exI), 

58 
(true,all_dupE), (true,not_impE), (true,imp_impE), (true,iff_impE), 

59 
(true,all_impE), (true,ex_impE), (true,impE) ]; 

60 

0  61 
(*0 subgoals vs 1 or more: the p in safep is for positive*) 
62 
val (safe0_brls, safep_brls) = 

17496  63 
List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls; 
0  64 

65 
(*Attack subgoals using safe inferences  matching, not resolution*) 

66 
val safe_step_tac = FIRST' [eq_assume_tac, 

1459  67 
eq_mp_tac, 
68 
bimatch_tac safe0_brls, 

69 
hyp_subst_tac, 

70 
bimatch_tac safep_brls] ; 

0  71 

72 
(*Repeatedly attack subgoals using safe inferences  it's deterministic!*) 

702
98fc1a8e832a
FOL/intprover/safe_tac: now uses REPEAT_DETERM_FIRST instead of REPEAT_DETERM
lcp
parents:
0
diff
changeset

73 
val safe_tac = REPEAT_DETERM_FIRST safe_step_tac; 
0  74 

75 
(*These steps could instantiate variables and are therefore unsafe.*) 

76 
val inst_step_tac = 

77 
assume_tac APPEND' mp_tac APPEND' 

78 
biresolve_tac (safe0_brls @ safep_brls); 

79 

80 
(*One safe or unsafe step. *) 

81 
fun step_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_brls i]; 

82 

5203  83 
fun step_dup_tac i = FIRST [safe_tac, inst_step_tac i, 
84 
biresolve_tac haz_dup_brls i]; 

85 

0  86 
(*Dumb but fast*) 
87 
val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1)); 

88 

89 
(*Slower but smarter than fast_tac*) 

90 
val best_tac = 

91 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac 1)); 

92 

5203  93 
(*Uses all_dupE: allows multiple use of universal assumptions. VERY slow.*) 
94 
val best_dup_tac = 

95 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac 1)); 

96 

97 

0  98 
end; 
99 