author  wenzelm 
Fri, 08 Jan 2021 22:30:32 +0100  
changeset 73110  c87ca43ebd3b 
parent 60754  02924903a6fd 
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. 

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

15 

16 
signature INT_PROVER = 

17 
sig 

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

18 
val best_tac: Proof.context > int > tactic 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
52457
diff
changeset

19 
val fast_tac: Proof.context > int > tactic 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
52457
diff
changeset

20 
val inst_step_tac: Proof.context > int > tactic 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
52457
diff
changeset

21 
val safe_step_tac: Proof.context > int > tactic 
0  22 
val safe_brls: (bool * thm) list 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
52457
diff
changeset

23 
val safe_tac: Proof.context > tactic 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
52457
diff
changeset

24 
val step_tac: Proof.context > int > tactic 
0  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*) 

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

55 
fun safe_step_tac ctxt = FIRST' [uniq_assume_tac ctxt, 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
52457
diff
changeset

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

57 
biresolve_tac ctxt safe0_brls, 
60754  58 
hyp_subst_tac ctxt, 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

59 
biresolve_tac ctxt safep_brls] ; 
0  60 

61 
(*Repeatedly attack subgoals using safe inferences*) 

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

62 
fun safe_tac ctxt = DETERM (REPEAT_FIRST (safe_step_tac ctxt)); 
0  63 

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

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

65 
fun inst_step_tac ctxt = assume_tac ctxt APPEND' mp_tac ctxt; 
0  66 

67 
(*One safe or unsafe step. *) 

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

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

70 
(*Dumb but fast*) 

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

71 
fun fast_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); 
0  72 

73 
(*Slower but smarter than fast_tac*) 

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

74 
fun best_tac ctxt = 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
52457
diff
changeset

75 
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1)); 
0  76 

77 
end; 