src/FOL/intprover.ML
 changeset 2601 b301958c465d parent 2572 8a47f85e7a03 child 4440 9ed4098074bc
equal 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`