# HG changeset patch
# User nipkow
# Date 912079131 -3600
# Node ID cd19eaa90f4584735e6f2aeae8ecc02af15d4d2f
# Parent  6acf3ff0f4865fac7525b58358d51e1a527a4489
Added a general refutation tactic which works by putting things into nnf first.

diff -r 6acf3ff0f486 -r cd19eaa90f45 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Nov 26 12:18:08 1998 +0100
+++ b/src/HOL/simpdata.ML	Thu Nov 26 12:18:51 1998 +0100
@@ -90,10 +90,11 @@
     handle THM _ =>
     error("Premises and conclusion of congruence rules must be =-equalities");
 
+val not_not = prover "(~ ~ P) = P";
 
-val simp_thms = map prover
+val simp_thms = [not_not] @ map prover
  [ "(x=x) = True",
-   "(~True) = False", "(~False) = True", "(~ ~ P) = P",
+   "(~True) = False", "(~False) = True",
    "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
    "(True=P) = P", "(P=True) = P", "(False=P) = (~P)", "(P=False) = (~P)",
    "(True --> P) = P", "(False --> P) = True", 
@@ -203,6 +204,10 @@
 prove "not_iff" "(P~=Q) = (P = (~Q))";
 prove "disj_not1" "(~P | Q) = (P --> Q)";
 prove "disj_not2" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *)
+prove "imp_conv_disj" "(P --> Q) = ((~P) | Q)";
+
+prove "iff_conv_conj_imp" "(P = Q) = ((P --> Q) & (Q --> P))";
+
 
 (*Avoids duplication of subgoals after split_if, when the true and false 
   cases boil down to the same thing.*) 
@@ -463,3 +468,43 @@
 open Clasimp;
 
 val HOL_css = (HOL_cs, HOL_ss);
+
+
+(*** A general refutation procedure ***)
+ 
+(* Parameters:
+
+   test: term -> bool
+   tests if a term is at all relevant to the refutation proof;
+   if not, then it can be discarded. Can improve performance,
+   esp. if disjunctions can be discarded (no case distinction needed!).
+
+   prep_tac: int -> tactic
+   A preparation tactic to be applied to the goal once all relevant premises
+   have been moved to the conclusion.
+
+   ref_tac: int -> tactic
+   the actual refutation tactic. Should be able to deal with goals
+   [| A1; ...; An |] ==> False
+   where the Ai are atomic, i.e. no top-level &, | or ?
+*)
+
+fun refute_tac test prep_tac ref_tac =
+  let val nnf_simps =
+        [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj,
+         not_all,not_ex,not_not];
+      val nnf_simpset =
+        empty_ss setmkeqTrue mk_eq_True
+                 setmksimps (mksimps mksimps_pairs)
+                 addsimps nnf_simps;
+      val prem_nnf_tac = full_simp_tac nnf_simpset;
+
+      val refute_prems_tac =
+        REPEAT(eresolve_tac [conjE, exE] 1 ORELSE
+               filter_prems_tac test 1 ORELSE
+               eresolve_tac [disjE] 1) THEN
+        ref_tac 1;
+  in EVERY'[TRY o filter_prems_tac test,
+            REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
+            SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
+  end;