author  wenzelm 
Sat, 04 Nov 2017 12:39:25 +0100  
changeset 67001  b34fbf33a7ea 
parent 59529  d881f5288d5a 
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 

59529  9 
Completeness (for propositional logic) is proved in 
0  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 

59529  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 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

23 
val inst_step_tac: Proof.context > 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 

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

59529  47 
(true, @{thm disj_impE}), (true, @{thm disjE}), 
38500  48 
(false, @{thm iffI}), (true, @{thm iffE}), (true, @{thm not_to_imp}) ]; 
0  49 

50 
val haz_brls = 

59529  51 
[ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}), 
38500  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, 

59529  68 
eq_mp_tac ctxt, 
58957  69 
bimatch_tac ctxt safe0_brls, 
51798  70 
hyp_subst_tac ctxt, 
58957  71 
bimatch_tac ctxt 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.*) 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

77 
fun inst_step_tac ctxt = 
59529  78 
assume_tac ctxt APPEND' mp_tac ctxt APPEND' 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

79 
biresolve_tac ctxt (safe0_brls @ safep_brls); 
0  80 

81 
(*One safe or unsafe step. *) 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

82 
fun step_tac ctxt i = 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

83 
FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac ctxt haz_brls i]; 
0  84 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

85 
fun step_dup_tac ctxt i = 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

86 
FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac ctxt haz_dup_brls i]; 
5203  87 

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

91 
(*Slower but smarter than fast_tac*) 

51798  92 
fun best_tac ctxt = 
93 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1)); 

0  94 

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

5203  98 

99 

0  100 
end; 
101 