1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/FOLP/intprover.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,79 @@
     1.4 +(*  Title: 	FOL/int-prover
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +A naive prover for intuitionistic logic
    1.10 +
    1.11 +BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use Int.fast_tac ...
    1.12 +
    1.13 +Completeness (for propositional logic) is proved in 
    1.14 +
    1.15 +Roy Dyckhoff.
    1.16 +Contraction-Free Sequent Calculi for Intuitionistic Logic.
    1.17 +J. Symbolic Logic (in press)
    1.18 +*)
    1.19 +
    1.20 +signature INT_PROVER = 
    1.21 +  sig
    1.22 +  val best_tac: int -> tactic
    1.23 +  val fast_tac: int -> tactic
    1.24 +  val inst_step_tac: int -> tactic
    1.25 +  val safe_step_tac: int -> tactic
    1.26 +  val safe_brls: (bool * thm) list
    1.27 +  val safe_tac: tactic
    1.28 +  val step_tac: int -> tactic
    1.29 +  val haz_brls: (bool * thm) list
    1.30 +  end;
    1.31 +
    1.32 +
    1.33 +structure Int : INT_PROVER   = 
    1.34 +struct
    1.35 +
    1.36 +(*Negation is treated as a primitive symbol, with rules notI (introduction),
    1.37 +  not_to_imp (converts the assumption ~P to P-->False), and not_impE
    1.38 +  (handles double negations).  Could instead rewrite by not_def as the first
    1.39 +  step of an intuitionistic proof.
    1.40 +*)
    1.41 +val safe_brls = sort lessb 
    1.42 +    [ (true,FalseE), (false,TrueI), (false,refl),
    1.43 +      (false,impI), (false,notI), (false,allI),
    1.44 +      (true,conjE), (true,exE),
    1.45 +      (false,conjI), (true,conj_impE),
    1.46 +      (true,disj_impE), (true,ex_impE),
    1.47 +      (true,disjE), (false,iffI), (true,iffE), (true,not_to_imp) ];
    1.48 +
    1.49 +val haz_brls =
    1.50 +    [ (false,disjI1), (false,disjI2), (false,exI), 
    1.51 +      (true,allE), (true,not_impE), (true,imp_impE), (true,iff_impE),
    1.52 +      (true,all_impE), (true,impE) ];
    1.53 +
    1.54 +(*0 subgoals vs 1 or more: the p in safep is for positive*)
    1.55 +val (safe0_brls, safep_brls) =
    1.56 +    partition (apl(0,op=) o subgoals_of_brl) safe_brls;
    1.57 +
    1.58 +(*Attack subgoals using safe inferences*)
    1.59 +val safe_step_tac = FIRST' [uniq_assume_tac,
    1.60 +			    IFOLP_Lemmas.uniq_mp_tac,
    1.61 +			    biresolve_tac safe0_brls,
    1.62 +			    hyp_subst_tac,
    1.63 +			    biresolve_tac safep_brls] ;
    1.64 +
    1.65 +(*Repeatedly attack subgoals using safe inferences*)
    1.66 +val safe_tac = DETERM (REPEAT_FIRST safe_step_tac);
    1.67 +
    1.68 +(*These steps could instantiate variables and are therefore unsafe.*)
    1.69 +val inst_step_tac = assume_tac APPEND' mp_tac;
    1.70 +
    1.71 +(*One safe or unsafe step. *)
    1.72 +fun step_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_brls i];
    1.73 +
    1.74 +(*Dumb but fast*)
    1.75 +val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1));
    1.76 +
    1.77 +(*Slower but smarter than fast_tac*)
    1.78 +val best_tac = 
    1.79 +  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac 1));
    1.80 +
    1.81 +end;
    1.82 +