# HG changeset patch
# User haftmann
# Date 1203678112 -3600
# Node ID 06eacfd8dd9f4b693246c77d842ccfdfbf4e3c52
# Parent  c69c3559355b5401b962e6f9a5210df8e54e5a23
moved refute_tac to linarith.ML

diff -r c69c3559355b -r 06eacfd8dd9f src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Thu Feb 21 21:31:52 2008 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Fri Feb 22 12:01:52 2008 +0100
@@ -826,6 +826,49 @@
 solver all the time rather than add the additional check. *)
 
 
+(* generic 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 EX
+*)
+
+local
+  val nnf_simpset =
+    empty_ss setmkeqTrue mk_eq_True
+    setmksimps (mksimps mksimps_pairs)
+    addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
+      @{thm de_Morgan_conj}, @{thm not_all}, @{thm not_ex}, @{thm not_not}];
+  fun prem_nnf_tac i st =
+    full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st;
+in
+fun refute_tac test prep_tac ref_tac =
+  let val refute_prems_tac =
+        REPEAT_DETERM
+              (eresolve_tac [@{thm conjE}, @{thm exE}] 1 ORELSE
+               filter_prems_tac test 1 ORELSE
+               etac @{thm disjE} 1) THEN
+        (DETERM (etac @{thm notE} 1 THEN eq_assume_tac 1) ORELSE
+         ref_tac 1);
+  in EVERY'[TRY o filter_prems_tac test,
+            REPEAT_DETERM o etac @{thm rev_mp}, prep_tac, rtac @{thm ccontr}, prem_nnf_tac,
+            SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
+  end;
+end;
+
+
 (* arith proof method *)
 
 local
diff -r c69c3559355b -r 06eacfd8dd9f src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Feb 21 21:31:52 2008 +0100
+++ b/src/HOL/simpdata.ML	Fri Feb 22 12:01:52 2008 +0100
@@ -183,50 +183,6 @@
   let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths
   in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
 
-
-
-(** generic 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 EX
-*)
-
-local
-  val nnf_simpset =
-    empty_ss setmkeqTrue mk_eq_True
-    setmksimps (mksimps mksimps_pairs)
-    addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
-      @{thm de_Morgan_conj}, @{thm not_all}, @{thm not_ex}, @{thm not_not}];
-  fun prem_nnf_tac i st =
-    full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st;
-in
-fun refute_tac test prep_tac ref_tac =
-  let val refute_prems_tac =
-        REPEAT_DETERM
-              (eresolve_tac [@{thm conjE}, @{thm exE}] 1 ORELSE
-               filter_prems_tac test 1 ORELSE
-               etac @{thm disjE} 1) THEN
-        (DETERM (etac @{thm notE} 1 THEN eq_assume_tac 1) ORELSE
-         ref_tac 1);
-  in EVERY'[TRY o filter_prems_tac test,
-            REPEAT_DETERM o etac @{thm rev_mp}, prep_tac, rtac @{thm ccontr}, prem_nnf_tac,
-            SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
-  end;
-end;
-
 val defALL_regroup =
   Simplifier.simproc @{theory}
     "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;