src/HOL/simpdata.ML
changeset 26110 06eacfd8dd9f
parent 24035 74c032aea9ed
child 26711 3a478bfa1650
--- 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;