# HG changeset patch
# User haftmann
# Date 1162560157 -3600
# Node ID 25bd46916c1220b46478ca42043e61a880465719
# Parent  405ebd7ba8816bf87dc3efa83a5c8add199abf49
simplified reasoning tools setup

diff -r 405ebd7ba881 -r 25bd46916c12 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Nov 03 14:22:36 2006 +0100
+++ b/src/HOL/HOL.thy	Fri Nov 03 14:22:37 2006 +0100
@@ -7,7 +7,7 @@
 
 theory HOL
 imports CPure
-uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML") "Tools/res_atpset.ML"
+uses ("simpdata.ML") "Tools/res_atpset.ML"
 begin
 
 subsection {* Primitive logic *}
@@ -861,8 +861,34 @@
 lemma thin_refl:
   "\<And>X. \<lbrakk> x=x; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
 
-use "cladata.ML"
-setup Hypsubst.hypsubst_setup
+ML {*
+structure Hypsubst = HypsubstFun(
+struct
+  structure Simplifier = Simplifier
+  val dest_eq = HOLogic.dest_eq_typ
+  val dest_Trueprop = HOLogic.dest_Trueprop
+  val dest_imp = HOLogic.dest_imp
+  val eq_reflection = HOL.eq_reflection
+  val rev_eq_reflection = HOL.def_imp_eq
+  val imp_intr = HOL.impI
+  val rev_mp = HOL.rev_mp
+  val subst = HOL.subst
+  val sym = HOL.sym
+  val thin_refl = thm "thin_refl";
+end);
+
+structure Classical = ClassicalFun(
+struct
+  val mp = HOL.mp
+  val not_elim = HOL.notE
+  val classical = HOL.classical
+  val sizef = Drule.size_of_thm
+  val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
+end);
+
+structure BasicClassical: BASIC_CLASSICAL = Classical; 
+*}
+
 setup {*
 let
   (*prevent substitution on bool*)
@@ -870,11 +896,12 @@
     Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("bool", []) | _ => false)
       (nth (Thm.prems_of thm) (i - 1)) then Hypsubst.hyp_subst_tac i thm else no_tac thm;
 in
-  ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
+  Hypsubst.hypsubst_setup
+  #> ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
+  #> Classical.setup
+  #> ResAtpset.setup
 end
 *}
-setup Classical.setup
-setup ResAtpset.setup
 
 declare iffI [intro!]
   and notI [intro!]
@@ -891,17 +918,6 @@
   and conjE [elim!]
   and conjE [elim!]
 
-ML {*
-structure HOL =
-struct
-
-open HOL;
-
-val claset_prop = Classical.claset_of (the_context ());
-
-end;
-*}
-
 declare ex_ex1I [intro!]
   and allI [intro!]
   and the_equality [intro]
@@ -943,15 +959,31 @@
 apply (tactic "etac (Classical.dup_elim HOL.allE) 1")
 by iprover
 
-use "blastdata.ML"
-setup Blast.setup
+ML {*
+structure Blast = BlastFun(
+struct
+  type claset = Classical.claset
+  val equality_name = "op ="
+  val not_name = "Not"
+  val notE = HOL.notE
+  val ccontr = HOL.ccontr
+  val contr_tac = Classical.contr_tac
+  val dup_intr = Classical.dup_intr
+  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
+  val claset	= Classical.claset
+  val rep_cs = Classical.rep_cs
+  val cla_modifiers = Classical.cla_modifiers
+  val cla_meth' = Classical.cla_meth'
+end);
 
-ML {*
 structure HOL =
 struct
 
 open HOL;
 
+val Blast_tac = Blast.Blast_tac;
+val blast_tac = Blast.blast_tac;
+
 fun case_tac a = res_inst_tac [("P", a)] case_split;
 
 (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
@@ -967,9 +999,6 @@
 
 fun strip_tac i = REPEAT (resolve_tac [impI, allI] i);
 
-val Blast_tac = Blast.Blast_tac;
-val blast_tac = Blast.blast_tac;
-
 fun Trueprop_conv conv ct = (case term_of ct of
     Const ("Trueprop", _) $ _ =>
       let val (ct1, ct2) = Thm.dest_comb ct
@@ -1002,6 +1031,8 @@
 end;
 *}
 
+setup Blast.setup
+
 
 subsubsection {* Simplifier *}
 
@@ -1042,29 +1073,6 @@
     "!!P. (ALL x. t=x --> P(x)) = P(t)"
   by (blast, blast, blast, blast, blast, iprover+)
 
-lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
-  by iprover
-
-lemma ex_simps:
-  "!!P Q. (EX x. P x & Q)   = ((EX x. P x) & Q)"
-  "!!P Q. (EX x. P & Q x)   = (P & (EX x. Q x))"
-  "!!P Q. (EX x. P x | Q)   = ((EX x. P x) | Q)"
-  "!!P Q. (EX x. P | Q x)   = (P | (EX x. Q x))"
-  "!!P Q. (EX x. P x --> Q) = ((ALL x. P x) --> Q)"
-  "!!P Q. (EX x. P --> Q x) = (P --> (EX x. Q x))"
-  -- {* Miniscoping: pushing in existential quantifiers. *}
-  by (iprover | blast)+
-
-lemma all_simps:
-  "!!P Q. (ALL x. P x & Q)   = ((ALL x. P x) & Q)"
-  "!!P Q. (ALL x. P & Q x)   = (P & (ALL x. Q x))"
-  "!!P Q. (ALL x. P x | Q)   = ((ALL x. P x) | Q)"
-  "!!P Q. (ALL x. P | Q x)   = (P | (ALL x. Q x))"
-  "!!P Q. (ALL x. P x --> Q) = ((EX x. P x) --> Q)"
-  "!!P Q. (ALL x. P --> Q x) = (P --> (ALL x. Q x))"
-  -- {* Miniscoping: pushing in universal quantifiers. *}
-  by (iprover | blast)+
-
 lemma disj_absorb: "(A | A) = A"
   by blast
 
@@ -1114,6 +1122,9 @@
 lemma imp_disj1: "((P-->Q)|R) = (P--> Q|R)" by blast
 lemma imp_disj2: "(Q|(P-->R)) = (P--> Q|R)" by blast
 
+lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
+  by iprover
+
 lemma de_Morgan_disj: "(~(P | Q)) = (~P & ~Q)" by iprover
 lemma de_Morgan_conj: "(~(P & Q)) = (~P | ~Q)" by blast
 lemma not_imp: "(~(P --> Q)) = (P & ~Q)" by blast
@@ -1257,18 +1268,6 @@
     by (rule equal_elim_rule1)
 qed
 
-
-text {* \medskip Actual Installation of the Simplifier. *}
-
-lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
-proof
-  assume prem: "True \<Longrightarrow> PROP P"
-  from prem [OF TrueI] show "PROP P" . 
-next
-  assume "PROP P"
-  show "PROP P" .
-qed
-
 lemma uncurry:
   assumes "P \<longrightarrow> Q \<longrightarrow> R"
   shows "P \<and> Q \<longrightarrow> R"
@@ -1293,11 +1292,42 @@
   by blast
 
 use "simpdata.ML"
-setup "Simplifier.method_setup Splitter.split_modifiers"
-setup "(fn thy => (change_simpset_of thy (fn _ => HOL.simpset_simprocs); thy))"
-setup Splitter.setup
-setup Clasimp.setup
-setup EqSubst.setup
+setup {*
+  Simplifier.method_setup Splitter.split_modifiers
+  #> (fn thy => (change_simpset_of thy (fn _ => HOL.simpset_simprocs); thy))
+  #> Splitter.setup
+  #> Clasimp.setup
+  #> EqSubst.setup
+*}
+
+lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
+proof
+  assume prem: "True \<Longrightarrow> PROP P"
+  from prem [OF TrueI] show "PROP P" . 
+next
+  assume "PROP P"
+  show "PROP P" .
+qed
+
+lemma ex_simps:
+  "!!P Q. (EX x. P x & Q)   = ((EX x. P x) & Q)"
+  "!!P Q. (EX x. P & Q x)   = (P & (EX x. Q x))"
+  "!!P Q. (EX x. P x | Q)   = ((EX x. P x) | Q)"
+  "!!P Q. (EX x. P | Q x)   = (P | (EX x. Q x))"
+  "!!P Q. (EX x. P x --> Q) = ((ALL x. P x) --> Q)"
+  "!!P Q. (EX x. P --> Q x) = (P --> (EX x. Q x))"
+  -- {* Miniscoping: pushing in existential quantifiers. *}
+  by (iprover | blast)+
+
+lemma all_simps:
+  "!!P Q. (ALL x. P x & Q)   = ((ALL x. P x) & Q)"
+  "!!P Q. (ALL x. P & Q x)   = (P & (ALL x. Q x))"
+  "!!P Q. (ALL x. P x | Q)   = ((ALL x. P x) | Q)"
+  "!!P Q. (ALL x. P | Q x)   = (P | (ALL x. Q x))"
+  "!!P Q. (ALL x. P x --> Q) = ((EX x. P x) --> Q)"
+  "!!P Q. (ALL x. P --> Q x) = (P --> (ALL x. Q x))"
+  -- {* Miniscoping: pushing in universal quantifiers. *}
+  by (iprover | blast)+
 
 declare triv_forall_equality [simp] (*prunes params*)
   and True_implies_equals [simp] (*prune asms `True'*)
diff -r 405ebd7ba881 -r 25bd46916c12 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Nov 03 14:22:36 2006 +0100
+++ b/src/HOL/IsaMakefile	Fri Nov 03 14:22:37 2006 +0100
@@ -119,7 +119,7 @@
   Tools/typedef_package.ML Tools/typedef_codegen.ML	\
   Transitive_Closure.ML Transitive_Closure.thy		\
   Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy		\
-  arith_data.ML blastdata.ML cladata.ML			\
+  arith_data.ML			\
   document/root.tex hologic.ML simpdata.ML ResAtpMethods.thy 			\
   Tools/res_atp_provers.ML Tools/res_atp_methods.ML	\
   Tools/res_hol_clause.ML	\
diff -r 405ebd7ba881 -r 25bd46916c12 src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Fri Nov 03 14:22:36 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(*  Title:      HOL/cladata.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1996  University of Cambridge
-
-Setting up the classical reasoner.
-*)
-
-structure Hypsubst_Data =
-struct
-  structure Simplifier = Simplifier
-  val dest_eq = HOLogic.dest_eq_typ
-  val dest_Trueprop = HOLogic.dest_Trueprop
-  val dest_imp = HOLogic.dest_imp
-  val eq_reflection = HOL.eq_reflection
-  val rev_eq_reflection = HOL.def_imp_eq
-  val imp_intr = HOL.impI
-  val rev_mp = HOL.rev_mp
-  val subst = HOL.subst
-  val sym = HOL.sym
-  val thin_refl = thm "thin_refl";
-end;
-
-structure Hypsubst = HypsubstFun(Hypsubst_Data);
-
-structure Classical_Data = 
-struct
-  val mp = HOL.mp
-  val not_elim = HOL.notE
-  val classical = HOL.classical
-  val sizef = Drule.size_of_thm
-  val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
-end;
-
-structure Classical = ClassicalFun(Classical_Data);
-structure BasicClassical: BASIC_CLASSICAL = Classical; 
diff -r 405ebd7ba881 -r 25bd46916c12 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Nov 03 14:22:36 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,318 +0,0 @@
-(*  Title:      HOL/simpdata.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1991  University of Cambridge
-
-Instantiation of the generic simplifier for HOL.
-*)
-
-(** tools setup **)
-
-structure Quantifier1 = Quantifier1Fun
-(struct
-  (*abstract syntax*)
-  fun dest_eq ((c as Const("op =",_)) $ s $ t) = SOME (c, s, t)
-    | dest_eq _ = NONE;
-  fun dest_conj ((c as Const("op &",_)) $ s $ t) = SOME (c, s, t)
-    | dest_conj _ = NONE;
-  fun dest_imp ((c as Const("op -->",_)) $ s $ t) = SOME (c, s, t)
-    | dest_imp _ = NONE;
-  val conj = HOLogic.conj
-  val imp  = HOLogic.imp
-  (*rules*)
-  val iff_reflection = HOL.eq_reflection
-  val iffI = HOL.iffI
-  val iff_trans = HOL.trans
-  val conjI= HOL.conjI
-  val conjE= HOL.conjE
-  val impI = HOL.impI
-  val mp   = HOL.mp
-  val uncurry = thm "uncurry"
-  val exI  = HOL.exI
-  val exE  = HOL.exE
-  val iff_allI = thm "iff_allI"
-  val iff_exI = thm "iff_exI"
-  val all_comm = thm "all_comm"
-  val ex_comm = thm "ex_comm"
-end);
-
-structure HOL =
-struct
-
-open HOL;
-
-val Eq_FalseI = thm "Eq_FalseI";
-val Eq_TrueI = thm "Eq_TrueI";
-val simp_implies_def = thm "simp_implies_def";
-val simp_impliesI = thm "simp_impliesI";
-
-fun mk_meta_eq r = r RS eq_reflection;
-fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
-
-fun mk_eq thm = case concl_of thm
-  (*expects Trueprop if not == *)
-  of Const ("==",_) $ _ $ _ => thm
-   | _ $ (Const ("op =", _) $ _ $ _) => mk_meta_eq thm
-   | _ $ (Const ("Not", _) $ _) => thm RS Eq_FalseI
-   | _ => thm RS Eq_TrueI;
-
-fun mk_eq_True r =
-  SOME (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE;
-
-(* Produce theorems of the form
-  (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y)
-*)
-fun lift_meta_eq_to_obj_eq i st =
-  let
-    fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q
-      | count_imp _ = 0;
-    val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1)))
-  in if j = 0 then meta_eq_to_obj_eq
-    else
-      let
-        val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
-        fun mk_simp_implies Q = foldr (fn (R, S) =>
-          Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps
-        val aT = TFree ("'a", HOLogic.typeS);
-        val x = Free ("x", aT);
-        val y = Free ("y", aT)
-      in Goal.prove_global (Thm.theory_of_thm st) []
-        [mk_simp_implies (Logic.mk_equals (x, y))]
-        (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))
-        (fn prems => EVERY
-         [rewrite_goals_tac [simp_implies_def],
-          REPEAT (ares_tac (meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)])
-      end
-  end;
-
-(*Congruence rules for = (instead of ==)*)
-fun mk_meta_cong rl = zero_var_indexes
-  (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
-     rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
-   in mk_meta_eq rl' handle THM _ =>
-     if can Logic.dest_equals (concl_of rl') then rl'
-     else error "Conclusion of congruence rules must be =-equality"
-   end);
-
-(*
-val mk_atomize:      (string * thm list) list -> thm -> thm list
-looks too specific to move it somewhere else
-*)
-fun mk_atomize pairs =
-  let
-    fun atoms thm = case concl_of thm
-     of Const("Trueprop", _) $ p => (case head_of p
-        of Const(a, _) => (case AList.lookup (op =) pairs a
-           of SOME rls => maps atoms ([thm] RL rls)
-            | NONE => [thm])
-         | _ => [thm])
-      | _ => [thm]
-  in atoms end;
-
-fun mksimps pairs =
-  (map_filter (try mk_eq) o mk_atomize pairs o gen_all);
-
-fun unsafe_solver_tac prems =
-  (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
-  FIRST'[resolve_tac(reflexive_thm :: TrueI :: refl :: prems), atac, etac FalseE];
-val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
-
-(*No premature instantiation of variables during simplification*)
-fun safe_solver_tac prems =
-  (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
-  FIRST'[match_tac(reflexive_thm :: TrueI :: refl :: prems),
-         eq_assume_tac, ematch_tac [FalseE]];
-val safe_solver = mk_solver "HOL safe" safe_solver_tac;
-
-end;
-
-structure SplitterData =
-struct
-  structure Simplifier = Simplifier
-  val mk_eq           = HOL.mk_eq
-  val meta_eq_to_iff  = HOL.meta_eq_to_obj_eq
-  val iffD            = HOL.iffD2
-  val disjE           = HOL.disjE
-  val conjE           = HOL.conjE
-  val exE             = HOL.exE
-  val contrapos       = HOL.contrapos_nn
-  val contrapos2      = HOL.contrapos_pp
-  val notnotD         = HOL.notnotD
-end;
-
-structure Splitter = SplitterFun(SplitterData);
-
-(* integration of simplifier with classical reasoner *)
-
-structure Clasimp = ClasimpFun
- (structure Simplifier = Simplifier and Splitter = Splitter
-  and Classical  = Classical and Blast = Blast
-  val iffD1 = HOL.iffD1 val iffD2 = HOL.iffD2 val notE = HOL.notE);
-
-structure HOL =
-struct
-
-open HOL;
-
-val mksimps_pairs =
-  [("op -->", [mp]), ("op &", [thm "conjunct1", thm "conjunct2"]),
-   ("All", [spec]), ("True", []), ("False", []),
-   ("HOL.If", [thm "if_bool_eq_conj" RS iffD1])];
-
-val simpset_basic =
-  Simplifier.theory_context (the_context ()) empty_ss
-    setsubgoaler asm_simp_tac
-    setSSolver safe_solver
-    setSolver unsafe_solver
-    setmksimps (mksimps mksimps_pairs)
-    setmkeqTrue mk_eq_True
-    setmkcong mk_meta_cong;
-
-fun simplify rews = Simplifier.full_simplify (simpset_basic addsimps rews);
-
-fun unfold_tac ths =
-  let val ss0 = Simplifier.clear_ss simpset_basic addsimps ths
-  in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
-
-(** simprocs **)
-
-(* simproc for proving "(y = x) == False" from premise "~(x = y)" *)
-
-val use_neq_simproc = ref true;
-
-local
-  val thy = the_context ();
-  val neq_to_EQ_False = thm "not_sym" RS HOL.Eq_FalseI;
-  fun neq_prover sg ss (eq $ lhs $ rhs) =
-    let
-      fun test thm = (case #prop (rep_thm thm) of
-                    _ $ (Not $ (eq' $ l' $ r')) =>
-                      Not = HOLogic.Not andalso eq' = eq andalso
-                      r' aconv lhs andalso l' aconv rhs
-                  | _ => false)
-    in if !use_neq_simproc then case find_first test (prems_of_ss ss)
-     of NONE => NONE
-      | SOME thm => SOME (thm RS neq_to_EQ_False)
-     else NONE
-    end
-in
-
-val neq_simproc = Simplifier.simproc thy "neq_simproc" ["x = y"] neq_prover;
-
-end; (*local*)
-
-
-(* simproc for Let *)
-
-val use_let_simproc = ref true;
-
-local
-  val thy = the_context ();
-  val Let_folded = thm "Let_folded";
-  val Let_unfold = thm "Let_unfold";
-  val (f_Let_unfold, x_Let_unfold) =
-      let val [(_$(f$x)$_)] = prems_of Let_unfold
-      in (cterm_of thy f, cterm_of thy x) end
-  val (f_Let_folded, x_Let_folded) =
-      let val [(_$(f$x)$_)] = prems_of Let_folded
-      in (cterm_of thy f, cterm_of thy x) end;
-  val g_Let_folded =
-      let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of thy g end;
-in
-
-val let_simproc =
-  Simplifier.simproc thy "let_simp" ["Let x f"]
-   (fn sg => fn ss => fn t =>
-     let val ctxt = Simplifier.the_context ss;
-         val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
-     in Option.map (hd o Variable.export ctxt' ctxt o single)
-      (case t' of (Const ("Let",_)$x$f) => (* x and f are already in normal form *)
-         if not (!use_let_simproc) then NONE
-         else if is_Free x orelse is_Bound x orelse is_Const x
-         then SOME (thm "Let_def")
-         else
-          let
-             val n = case f of (Abs (x,_,_)) => x | _ => "x";
-             val cx = cterm_of sg x;
-             val {T=xT,...} = rep_cterm cx;
-             val cf = cterm_of sg f;
-             val fx_g = Simplifier.rewrite ss (Thm.capply cf cx);
-             val (_$_$g) = prop_of fx_g;
-             val g' = abstract_over (x,g);
-           in (if (g aconv g')
-               then
-                  let
-                    val rl = cterm_instantiate [(f_Let_unfold,cf),(x_Let_unfold,cx)] Let_unfold;
-                  in SOME (rl OF [fx_g]) end
-               else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*)
-               else let
-                     val abs_g'= Abs (n,xT,g');
-                     val g'x = abs_g'$x;
-                     val g_g'x = symmetric (beta_conversion false (cterm_of sg g'x));
-                     val rl = cterm_instantiate
-                               [(f_Let_folded,cterm_of sg f),(x_Let_folded,cx),
-                                (g_Let_folded,cterm_of sg abs_g')]
-                               Let_folded;
-                   in SOME (rl OF [transitive fx_g g_g'x])
-                   end)
-           end
-        | _ => NONE)
-     end)
-
-end; (*local*)
-
-(* 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 [conjE, exE] 1 ORELSE
-               filter_prems_tac test 1 ORELSE
-               etac disjE 1) THEN
-        ((etac notE 1 THEN eq_assume_tac 1) ORELSE
-         ref_tac 1);
-  in EVERY'[TRY o filter_prems_tac test,
-            REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
-            SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
-  end;
-end; (*local*)
-
-val defALL_regroup =
-  Simplifier.simproc (the_context ())
-    "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
-
-val defEX_regroup =
-  Simplifier.simproc (the_context ())
-    "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
-
-
-val simpset_simprocs = simpset_basic
-  addsimprocs [defALL_regroup, defEX_regroup, neq_simproc, let_simproc]
-
-end; (*struct*)
\ No newline at end of file