wenzelm@31974: (* Title: FOL/intprover.ML clasohm@1459: Author: Lawrence C Paulson, Cambridge University Computer Laboratory clasohm@0: Copyright 1992 University of Cambridge clasohm@0: clasohm@0: A naive prover for intuitionistic logic clasohm@0: paulson@2601: BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use IntPr.fast_tac ... clasohm@0: clasohm@0: Completeness (for propositional logic) is proved in clasohm@0: clasohm@0: Roy Dyckhoff. clasohm@0: Contraction-Free Sequent Calculi for Intuitionistic Logic. lcp@1005: J. Symbolic Logic 57(3), 1992, pages 795-807. lcp@1005: lcp@1005: The approach was developed independently by Roy Dyckhoff and L C Paulson. clasohm@0: *) clasohm@0: clasohm@0: signature INT_PROVER = wenzelm@51798: sig wenzelm@51798: val best_tac: Proof.context -> int -> tactic wenzelm@51798: val best_dup_tac: Proof.context -> int -> tactic wenzelm@51798: val fast_tac: Proof.context -> int -> tactic clasohm@0: val inst_step_tac: int -> tactic wenzelm@51798: val safe_step_tac: Proof.context -> int -> tactic clasohm@0: val safe_brls: (bool * thm) list wenzelm@51798: val safe_tac: Proof.context -> tactic wenzelm@51798: val step_tac: Proof.context -> int -> tactic wenzelm@51798: val step_dup_tac: Proof.context -> int -> tactic clasohm@0: val haz_brls: (bool * thm) list paulson@5203: val haz_dup_brls: (bool * thm) list wenzelm@51798: end; clasohm@0: clasohm@0: paulson@2601: structure IntPr : INT_PROVER = clasohm@0: struct clasohm@0: clasohm@0: (*Negation is treated as a primitive symbol, with rules notI (introduction), clasohm@0: not_to_imp (converts the assumption ~P to P-->False), and not_impE clasohm@0: (handles double negations). Could instead rewrite by not_def as the first clasohm@0: step of an intuitionistic proof. clasohm@0: *) wenzelm@4440: val safe_brls = sort (make_ord lessb) haftmann@38500: [ (true, @{thm FalseE}), (false, @{thm TrueI}), (false, @{thm refl}), haftmann@38500: (false, @{thm impI}), (false, @{thm notI}), (false, @{thm allI}), haftmann@38500: (true, @{thm conjE}), (true, @{thm exE}), haftmann@38500: (false, @{thm conjI}), (true, @{thm conj_impE}), haftmann@38500: (true, @{thm disj_impE}), (true, @{thm disjE}), haftmann@38500: (false, @{thm iffI}), (true, @{thm iffE}), (true, @{thm not_to_imp}) ]; clasohm@0: clasohm@0: val haz_brls = haftmann@38500: [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}), haftmann@38500: (true, @{thm allE}), (true, @{thm not_impE}), (true, @{thm imp_impE}), (true, @{thm iff_impE}), haftmann@38500: (true, @{thm all_impE}), (true, @{thm ex_impE}), (true, @{thm impE}) ]; clasohm@0: paulson@5203: val haz_dup_brls = haftmann@38500: [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}), haftmann@38500: (true, @{thm all_dupE}), (true, @{thm not_impE}), (true, @{thm imp_impE}), (true, @{thm iff_impE}), haftmann@38500: (true, @{thm all_impE}), (true, @{thm ex_impE}), (true, @{thm impE}) ]; paulson@5203: clasohm@0: (*0 subgoals vs 1 or more: the p in safep is for positive*) clasohm@0: val (safe0_brls, safep_brls) = haftmann@17496: List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls; clasohm@0: clasohm@0: (*Attack subgoals using safe inferences -- matching, not resolution*) wenzelm@51798: fun safe_step_tac ctxt = wenzelm@51798: FIRST' [ wenzelm@51798: eq_assume_tac, wenzelm@51798: eq_mp_tac, wenzelm@51798: bimatch_tac safe0_brls, wenzelm@51798: hyp_subst_tac ctxt, wenzelm@51798: bimatch_tac safep_brls]; clasohm@0: clasohm@0: (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) wenzelm@51798: fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt); clasohm@0: clasohm@0: (*These steps could instantiate variables and are therefore unsafe.*) clasohm@0: val inst_step_tac = clasohm@0: assume_tac APPEND' mp_tac APPEND' clasohm@0: biresolve_tac (safe0_brls @ safep_brls); clasohm@0: clasohm@0: (*One safe or unsafe step. *) wenzelm@51798: fun step_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_brls i]; clasohm@0: wenzelm@51798: fun step_dup_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_dup_brls i]; paulson@5203: clasohm@0: (*Dumb but fast*) wenzelm@51798: fun fast_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1)); clasohm@0: clasohm@0: (*Slower but smarter than fast_tac*) wenzelm@51798: fun best_tac ctxt = wenzelm@51798: SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1)); clasohm@0: paulson@5203: (*Uses all_dupE: allows multiple use of universal assumptions. VERY slow.*) wenzelm@51798: fun best_dup_tac ctxt = wenzelm@51798: SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac ctxt 1)); paulson@5203: paulson@5203: clasohm@0: end; clasohm@0: