author  wenzelm 
Sat, 25 May 2013 17:40:44 +0200  
changeset 52147  9943f8067f11 
parent 51798  ad3a241def73 
child 58957  c9e744ea8a38 
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 = 

51798  19 
sig 
20 
val best_tac: Proof.context > int > tactic 

21 
val best_dup_tac: Proof.context > int > tactic 

22 
val fast_tac: Proof.context > int > tactic 

0  23 
val inst_step_tac: int > tactic 
51798  24 
val safe_step_tac: Proof.context > int > tactic 
0  25 
val safe_brls: (bool * thm) list 
51798  26 
val safe_tac: Proof.context > tactic 
27 
val step_tac: Proof.context > int > tactic 

28 
val step_dup_tac: Proof.context > int > tactic 

0  29 
val haz_brls: (bool * thm) list 
5203  30 
val haz_dup_brls: (bool * thm) list 
51798  31 
end; 
0  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*) 

51798  65 
fun safe_step_tac ctxt = 
66 
FIRST' [ 

67 
eq_assume_tac, 

68 
eq_mp_tac, 

69 
bimatch_tac safe0_brls, 

70 
hyp_subst_tac ctxt, 

71 
bimatch_tac safep_brls]; 

0  72 

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

51798  74 
fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt); 
0  75 

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

77 
val inst_step_tac = 

78 
assume_tac APPEND' mp_tac APPEND' 

79 
biresolve_tac (safe0_brls @ safep_brls); 

80 

81 
(*One safe or unsafe step. *) 

51798  82 
fun step_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_brls i]; 
0  83 

51798  84 
fun step_dup_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_dup_brls i]; 
5203  85 

0  86 
(*Dumb but fast*) 
51798  87 
fun fast_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); 
0  88 

89 
(*Slower but smarter than fast_tac*) 

51798  90 
fun best_tac ctxt = 
91 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1)); 

0  92 

5203  93 
(*Uses all_dupE: allows multiple use of universal assumptions. VERY slow.*) 
51798  94 
fun best_dup_tac ctxt = 
95 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac ctxt 1)); 

5203  96 

97 

0  98 
end; 
99 