author  haftmann 
Tue, 10 Jul 2007 17:30:50 +0200  
changeset 23709  fd31da8f752a 
parent 17496  26535df536ae 
child 24584  01e83ffa6c54 
permissions  rwrr 
1463  1 
(* Title: FOLP/intprover.ML 
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 

2603
4988dda71c0b
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. 

2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2572
diff
changeset

13 
ContractionFree Sequent Calculi for IntPruitionistic Logic. 
0  14 
J. Symbolic Logic (in press) 
15 
*) 

16 

17 
signature INT_PROVER = 

18 
sig 

19 
val best_tac: int > tactic 

20 
val fast_tac: int > tactic 

21 
val inst_step_tac: int > tactic 

22 
val safe_step_tac: int > tactic 

23 
val safe_brls: (bool * thm) list 

24 
val safe_tac: tactic 

25 
val step_tac: int > tactic 

26 
val haz_brls: (bool * thm) list 

27 
end; 

28 

29 

2603
4988dda71c0b
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
paulson
parents:
2572
diff
changeset

30 
structure IntPr : INT_PROVER = 
0  31 
struct 
32 

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

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

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

36 
step of an intuitionistic proof. 

37 
*) 

4440  38 
val safe_brls = sort (make_ord lessb) 
0  39 
[ (true,FalseE), (false,TrueI), (false,refl), 
40 
(false,impI), (false,notI), (false,allI), 

41 
(true,conjE), (true,exE), 

42 
(false,conjI), (true,conj_impE), 

2572  43 
(true,disj_impE), (true,disjE), 
44 
(false,iffI), (true,iffE), (true,not_to_imp) ]; 

0  45 

46 
val haz_brls = 

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

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

2572  49 
(true,all_impE), (true,ex_impE), (true,impE) ]; 
0  50 

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

52 
val (safe0_brls, safep_brls) = 

17496  53 
List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls; 
0  54 

55 
(*Attack subgoals using safe inferences*) 

56 
val safe_step_tac = FIRST' [uniq_assume_tac, 

9263  57 
int_uniq_mp_tac, 
1459  58 
biresolve_tac safe0_brls, 
59 
hyp_subst_tac, 

60 
biresolve_tac safep_brls] ; 

0  61 

62 
(*Repeatedly attack subgoals using safe inferences*) 

63 
val safe_tac = DETERM (REPEAT_FIRST safe_step_tac); 

64 

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

66 
val inst_step_tac = assume_tac APPEND' mp_tac; 

67 

68 
(*One safe or unsafe step. *) 

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

70 

71 
(*Dumb but fast*) 

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

73 

74 
(*Slower but smarter than fast_tac*) 

75 
val best_tac = 

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

77 

78 
end; 

79 