author  wenzelm 
Wed, 03 Nov 2010 21:53:56 +0100  
changeset 40335  3e4bb6e7c3ca 
parent 35762  af3ff2ba4c54 
child 52457  c3b4b74a54fd 
permissions  rwrr 
24584  1 
(* Title: FOLP/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 

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

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

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

15 

16 
signature INT_PROVER = 

17 
sig 

18 
val best_tac: int > tactic 

19 
val fast_tac: int > tactic 

20 
val inst_step_tac: int > tactic 

21 
val safe_step_tac: int > tactic 

22 
val safe_brls: (bool * thm) list 

23 
val safe_tac: tactic 

24 
val step_tac: int > tactic 

25 
val haz_brls: (bool * thm) list 

26 
end; 

27 

28 

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

29 
structure IntPr : INT_PROVER = 
0  30 
struct 
31 

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

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

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

35 
step of an intuitionistic proof. 

36 
*) 

4440  37 
val safe_brls = sort (make_ord lessb) 
26322  38 
[ (true, @{thm FalseE}), (false, @{thm TrueI}), (false, @{thm refl}), 
39 
(false, @{thm impI}), (false, @{thm notI}), (false, @{thm allI}), 

40 
(true, @{thm conjE}), (true, @{thm exE}), 

41 
(false, @{thm conjI}), (true, @{thm conj_impE}), 

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

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

0  44 

45 
val haz_brls = 

26322  46 
[ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}), 
47 
(true, @{thm allE}), (true, @{thm not_impE}), (true, @{thm imp_impE}), (true, @{thm iff_impE}), 

48 
(true, @{thm all_impE}), (true, @{thm ex_impE}), (true, @{thm impE}) ]; 

0  49 

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

51 
val (safe0_brls, safep_brls) = 

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

54 
(*Attack subgoals using safe inferences*) 

55 
val safe_step_tac = FIRST' [uniq_assume_tac, 

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

59 
biresolve_tac safep_brls] ; 

0  60 

61 
(*Repeatedly attack subgoals using safe inferences*) 

62 
val safe_tac = DETERM (REPEAT_FIRST safe_step_tac); 

63 

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

65 
val inst_step_tac = assume_tac APPEND' mp_tac; 

66 

67 
(*One safe or unsafe step. *) 

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

69 

70 
(*Dumb but fast*) 

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

72 

73 
(*Slower but smarter than fast_tac*) 

74 
val best_tac = 

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

76 

77 
end; 