src/FOL/intprover.ML
changeset 2601 b301958c465d
parent 2572 8a47f85e7a03
child 4440 9ed4098074bc
equal deleted inserted replaced
2600:be48eff459e9 2601:b301958c465d
     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 IntPr.fast_tac ...
     9 
     9 
    10 Completeness (for propositional logic) is proved in 
    10 Completeness (for propositional logic) is proved in 
    11 
    11 
    12 Roy Dyckhoff.
    12 Roy Dyckhoff.
    13 Contraction-Free Sequent Calculi for Intuitionistic Logic.
    13 Contraction-Free Sequent Calculi for Intuitionistic Logic.
    27   val step_tac: int -> tactic
    27   val step_tac: int -> tactic
    28   val haz_brls: (bool * thm) list
    28   val haz_brls: (bool * thm) list
    29   end;
    29   end;
    30 
    30 
    31 
    31 
    32 structure Int : INT_PROVER   = 
    32 structure IntPr : INT_PROVER   = 
    33 struct
    33 struct
    34 
    34 
    35 (*Negation is treated as a primitive symbol, with rules notI (introduction),
    35 (*Negation is treated as a primitive symbol, with rules notI (introduction),
    36   not_to_imp (converts the assumption ~P to P-->False), and not_impE
    36   not_to_imp (converts the assumption ~P to P-->False), and not_impE
    37   (handles double negations).  Could instead rewrite by not_def as the first
    37   (handles double negations).  Could instead rewrite by not_def as the first