author  paulson 
Fri, 31 Jan 1997 17:13:19 +0100  
changeset 2572  8a47f85e7a03 
parent 1459  d12da312eff4 
child 2601  b301958c465d 
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 

8 
BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS  use Int.fast_tac ... 

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 

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 

28 
val haz_brls: (bool * thm) list 

29 
end; 

30 

31 

32 
structure Int : INT_PROVER = 

33 
struct 

34 

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

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

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

38 
step of an intuitionistic proof. 

39 
*) 

40 
val safe_brls = sort lessb 

41 
[ (true,FalseE), (false,TrueI), (false,refl), 

42 
(false,impI), (false,notI), (false,allI), 

43 
(true,conjE), (true,exE), 

44 
(false,conjI), (true,conj_impE), 

2572  45 
(true,disj_impE), (true,disjE), 
46 
(false,iffI), (true,iffE), (true,not_to_imp) ]; 

0  47 

48 
val haz_brls = 

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

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

2572  51 
(true,all_impE), (true,ex_impE), (true,impE) ]; 
0  52 

53 
(*0 subgoals vs 1 or more: the p in safep is for positive*) 

54 
val (safe0_brls, safep_brls) = 

55 
partition (apl(0,op=) o subgoals_of_brl) safe_brls; 

56 

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

58 
val safe_step_tac = FIRST' [eq_assume_tac, 

1459  59 
eq_mp_tac, 
60 
bimatch_tac safe0_brls, 

61 
hyp_subst_tac, 

62 
bimatch_tac safep_brls] ; 

0  63 

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

65 
val safe_tac = REPEAT_DETERM_FIRST safe_step_tac; 
0  66 

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

68 
val inst_step_tac = 

69 
assume_tac APPEND' mp_tac APPEND' 

70 
biresolve_tac (safe0_brls @ safep_brls); 

71 

72 
(*One safe or unsafe step. *) 

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

74 

75 
(*Dumb but fast*) 

76 
val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1)); 

77 

78 
(*Slower but smarter than fast_tac*) 

79 
val best_tac = 

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

81 

82 
end; 

83 