author  wenzelm 
Wed, 03 Nov 2010 21:53:56 +0100  
changeset 40335  3e4bb6e7c3ca 
parent 38500  d5477ee35820 
child 51798  ad3a241def73 
permissions  rwrr 
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 

9 
Completeness (for propositional logic) is proved in 

10 

11 
Roy Dyckhoff. 

12 
ContractionFree Sequent Calculi for Intuitionistic Logic. 

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

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

0  16 
*) 
17 

18 
signature INT_PROVER = 

19 
sig 

20 
val best_tac: int > tactic 

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

24 
val safe_step_tac: int > tactic 

25 
val safe_brls: (bool * thm) list 

26 
val safe_tac: tactic 

27 
val step_tac: int > tactic 

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

33 

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

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}), 

47 
(true, @{thm disj_impE}), (true, @{thm disjE}), 

48 
(false, @{thm iffI}), (true, @{thm iffE}), (true, @{thm not_to_imp}) ]; 

0  49 

50 
val haz_brls = 

38500  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}), 

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*) 

65 
val safe_step_tac = FIRST' [eq_assume_tac, 

1459  66 
eq_mp_tac, 
67 
bimatch_tac safe0_brls, 

68 
hyp_subst_tac, 

69 
bimatch_tac safep_brls] ; 

0  70 

71 
(*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

72 
val safe_tac = REPEAT_DETERM_FIRST safe_step_tac; 
0  73 

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

75 
val inst_step_tac = 

76 
assume_tac APPEND' mp_tac APPEND' 

77 
biresolve_tac (safe0_brls @ safep_brls); 

78 

79 
(*One safe or unsafe step. *) 

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

81 

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

0  84 
(*Dumb but fast*) 
85 
val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1)); 

86 

87 
(*Slower but smarter than fast_tac*) 

88 
val best_tac = 

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

90 

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

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

94 

95 

0  96 
end; 
97 