src/FOLP/intprover.ML
changeset 1459 d12da312eff4
parent 0 a5a9c433f639
child 1463 49ca5e875691
equal deleted inserted replaced
1458:fd510875fb71 1459:d12da312eff4
     1 (*  Title: 	FOL/int-prover
     1 (*  Title:      FOL/int-prover
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
     5 
     6 A naive prover for intuitionistic logic
     6 A naive prover for intuitionistic logic
     7 
     7 
     8 BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use Int.fast_tac ...
     8 BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use Int.fast_tac ...
    52 val (safe0_brls, safep_brls) =
    52 val (safe0_brls, safep_brls) =
    53     partition (apl(0,op=) o subgoals_of_brl) safe_brls;
    53     partition (apl(0,op=) o subgoals_of_brl) safe_brls;
    54 
    54 
    55 (*Attack subgoals using safe inferences*)
    55 (*Attack subgoals using safe inferences*)
    56 val safe_step_tac = FIRST' [uniq_assume_tac,
    56 val safe_step_tac = FIRST' [uniq_assume_tac,
    57 			    IFOLP_Lemmas.uniq_mp_tac,
    57                             IFOLP_Lemmas.uniq_mp_tac,
    58 			    biresolve_tac safe0_brls,
    58                             biresolve_tac safe0_brls,
    59 			    hyp_subst_tac,
    59                             hyp_subst_tac,
    60 			    biresolve_tac safep_brls] ;
    60                             biresolve_tac safep_brls] ;
    61 
    61 
    62 (*Repeatedly attack subgoals using safe inferences*)
    62 (*Repeatedly attack subgoals using safe inferences*)
    63 val safe_tac = DETERM (REPEAT_FIRST safe_step_tac);
    63 val safe_tac = DETERM (REPEAT_FIRST safe_step_tac);
    64 
    64 
    65 (*These steps could instantiate variables and are therefore unsafe.*)
    65 (*These steps could instantiate variables and are therefore unsafe.*)