src/FOLP/intprover.ML
 author blanchet Mon May 19 23:43:53 2014 +0200 (2014-05-19) changeset 57009 8cb6a5f1ae84 parent 52457 c3b4b74a54fd child 58963 26bf09b95dda permissions -rw-r--r--
```     1 (*  Title:      FOLP/intprover.ML
```
```     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     3     Copyright   1992  University of Cambridge
```
```     4
```
```     5 A naive prover for intuitionistic logic
```
```     6
```
```     7 BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use IntPr.fast_tac ...
```
```     8
```
```     9 Completeness (for propositional logic) is proved in
```
```    10
```
```    11 Roy Dyckhoff.
```
```    12 Contraction-Free Sequent Calculi for Intuitionistic Logic.
```
```    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
```
```    29 structure IntPr : INT_PROVER   =
```
```    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 *)
```
```    37 val safe_brls = sort (make_ord lessb)
```
```    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}) ];
```
```    44
```
```    45 val haz_brls =
```
```    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}) ];
```
```    49
```
```    50 (*0 subgoals vs 1 or more: the p in safep is for positive*)
```
```    51 val (safe0_brls, safep_brls) =
```
```    52     List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
```
```    53
```
```    54 (*Attack subgoals using safe inferences*)
```
```    55 val safe_step_tac = FIRST' [uniq_assume_tac,
```
```    56                             int_uniq_mp_tac,
```
```    57                             biresolve_tac safe0_brls,
```
```    58                             hyp_subst_tac,
```
```    59                             biresolve_tac safep_brls] ;
```
```    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;
```