Added a general refutation tactic which works by putting things into nnf first.
authornipkow
Thu Nov 26 12:18:51 1998 +0100 (1998-11-26)
changeset 5975cd19eaa90f45
parent 5974 6acf3ff0f486
child 5976 44290b71a85f
Added a general refutation tactic which works by putting things into nnf first.
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/simpdata.ML	Thu Nov 26 12:18:08 1998 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Thu Nov 26 12:18:51 1998 +0100
     1.3 @@ -90,10 +90,11 @@
     1.4      handle THM _ =>
     1.5      error("Premises and conclusion of congruence rules must be =-equalities");
     1.6  
     1.7 +val not_not = prover "(~ ~ P) = P";
     1.8  
     1.9 -val simp_thms = map prover
    1.10 +val simp_thms = [not_not] @ map prover
    1.11   [ "(x=x) = True",
    1.12 -   "(~True) = False", "(~False) = True", "(~ ~ P) = P",
    1.13 +   "(~True) = False", "(~False) = True",
    1.14     "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
    1.15     "(True=P) = P", "(P=True) = P", "(False=P) = (~P)", "(P=False) = (~P)",
    1.16     "(True --> P) = P", "(False --> P) = True", 
    1.17 @@ -203,6 +204,10 @@
    1.18  prove "not_iff" "(P~=Q) = (P = (~Q))";
    1.19  prove "disj_not1" "(~P | Q) = (P --> Q)";
    1.20  prove "disj_not2" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *)
    1.21 +prove "imp_conv_disj" "(P --> Q) = ((~P) | Q)";
    1.22 +
    1.23 +prove "iff_conv_conj_imp" "(P = Q) = ((P --> Q) & (Q --> P))";
    1.24 +
    1.25  
    1.26  (*Avoids duplication of subgoals after split_if, when the true and false 
    1.27    cases boil down to the same thing.*) 
    1.28 @@ -463,3 +468,43 @@
    1.29  open Clasimp;
    1.30  
    1.31  val HOL_css = (HOL_cs, HOL_ss);
    1.32 +
    1.33 +
    1.34 +(*** A general refutation procedure ***)
    1.35 + 
    1.36 +(* Parameters:
    1.37 +
    1.38 +   test: term -> bool
    1.39 +   tests if a term is at all relevant to the refutation proof;
    1.40 +   if not, then it can be discarded. Can improve performance,
    1.41 +   esp. if disjunctions can be discarded (no case distinction needed!).
    1.42 +
    1.43 +   prep_tac: int -> tactic
    1.44 +   A preparation tactic to be applied to the goal once all relevant premises
    1.45 +   have been moved to the conclusion.
    1.46 +
    1.47 +   ref_tac: int -> tactic
    1.48 +   the actual refutation tactic. Should be able to deal with goals
    1.49 +   [| A1; ...; An |] ==> False
    1.50 +   where the Ai are atomic, i.e. no top-level &, | or ?
    1.51 +*)
    1.52 +
    1.53 +fun refute_tac test prep_tac ref_tac =
    1.54 +  let val nnf_simps =
    1.55 +        [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj,
    1.56 +         not_all,not_ex,not_not];
    1.57 +      val nnf_simpset =
    1.58 +        empty_ss setmkeqTrue mk_eq_True
    1.59 +                 setmksimps (mksimps mksimps_pairs)
    1.60 +                 addsimps nnf_simps;
    1.61 +      val prem_nnf_tac = full_simp_tac nnf_simpset;
    1.62 +
    1.63 +      val refute_prems_tac =
    1.64 +        REPEAT(eresolve_tac [conjE, exE] 1 ORELSE
    1.65 +               filter_prems_tac test 1 ORELSE
    1.66 +               eresolve_tac [disjE] 1) THEN
    1.67 +        ref_tac 1;
    1.68 +  in EVERY'[TRY o filter_prems_tac test,
    1.69 +            REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
    1.70 +            SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
    1.71 +  end;