author nipkow Thu, 26 Nov 1998 12:18:51 +0100 changeset 5975 cd19eaa90f45 parent 5974 6acf3ff0f486 child 5976 44290b71a85f
Added a general refutation tactic which works by putting things into nnf first.
 src/HOL/simpdata.ML file | annotate | diff | comparison | revisions
```--- 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)