1(*  Title:      FOL/intprover.ML
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1992  University of Cambridge
4
5A naive prover for intuitionistic logic
6
7BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use IntPr.fast_tac ...
8
9Completeness (for propositional logic) is proved in
10
11Roy Dyckhoff.
12Contraction-Free Sequent Calculi for Intuitionistic Logic.
13J. Symbolic Logic  57(3), 1992, pages 795-807.
14
15The approach was developed independently by Roy Dyckhoff and L C Paulson.
16*)
17
18signature INT_PROVER =
19sig
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
23  val inst_step_tac: Proof.context -> int -> tactic
24  val safe_step_tac: Proof.context -> int -> tactic
25  val safe_brls: (bool * thm) list
26  val safe_tac: Proof.context -> tactic
27  val step_tac: Proof.context -> int -> tactic
28  val step_dup_tac: Proof.context -> int -> tactic
29  val haz_brls: (bool * thm) list
30  val haz_dup_brls: (bool * thm) list
31end;
32
33
34structure IntPr : INT_PROVER   =
35struct
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*)
42val safe_brls = sort (make_ord lessb)
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}) ];
49
50val haz_brls =
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}) ];
54
55val haz_dup_brls =
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}) ];
59
60(*0 subgoals vs 1 or more: the p in safep is for positive*)
61val (safe0_brls, safep_brls) =
62    List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
63
64(*Attack subgoals using safe inferences -- matching, not resolution*)
65fun safe_step_tac ctxt =
66  FIRST' [
67    eq_assume_tac,
68    eq_mp_tac ctxt,
69    bimatch_tac ctxt safe0_brls,
70    hyp_subst_tac ctxt,
71    bimatch_tac ctxt safep_brls];
72
73(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
74fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt);
75
76(*These steps could instantiate variables and are therefore unsafe.*)
77fun inst_step_tac ctxt =
78  assume_tac ctxt APPEND' mp_tac ctxt APPEND'
79  biresolve_tac ctxt (safe0_brls @ safep_brls);
80
81(*One safe or unsafe step. *)
82fun step_tac ctxt i =
83  FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac ctxt haz_brls i];
84
85fun step_dup_tac ctxt i =
86  FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac ctxt haz_dup_brls i];
87
88(*Dumb but fast*)
89fun fast_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
90
91(*Slower but smarter than fast_tac*)
92fun best_tac ctxt =
93  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1));
94
95(*Uses all_dupE: allows multiple use of universal assumptions.  VERY slow.*)
96fun best_dup_tac ctxt =
97  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac ctxt 1));
98
99
100end;
101
102