src/HOL/simpdata.ML
changeset 20973 0b8e436ed071
parent 20944 34b2c1bb7178
child 21045 66d6d1b0ddfa
     1.1 --- a/src/HOL/simpdata.ML	Wed Oct 11 10:49:36 2006 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Wed Oct 11 14:51:24 2006 +0200
     1.3 @@ -6,40 +6,16 @@
     1.4  Instantiation of the generic simplifier for HOL.
     1.5  *)
     1.6  
     1.7 -(* legacy ML bindings - FIXME get rid of this *)
     1.8 -
     1.9 -val Eq_FalseI = thm "Eq_FalseI";
    1.10 -val Eq_TrueI = thm "Eq_TrueI";
    1.11 -val de_Morgan_conj = thm "de_Morgan_conj";
    1.12 -val de_Morgan_disj = thm "de_Morgan_disj";
    1.13 -val iff_conv_conj_imp = thm "iff_conv_conj_imp";
    1.14 -val imp_cong = thm "imp_cong";
    1.15 -val imp_conv_disj = thm "imp_conv_disj";
    1.16 -val imp_disj1 = thm "imp_disj1";
    1.17 -val imp_disj2 = thm "imp_disj2";
    1.18 -val imp_disjL = thm "imp_disjL";
    1.19 -val simp_impliesI = thm "simp_impliesI";
    1.20 -val simp_implies_cong = thm "simp_implies_cong";
    1.21 -val simp_implies_def = thm "simp_implies_def";
    1.22 -
    1.23 -local
    1.24 -  val uncurry = thm "uncurry"
    1.25 -  val iff_allI = thm "iff_allI"
    1.26 -  val iff_exI = thm "iff_exI"
    1.27 -  val all_comm = thm "all_comm"
    1.28 -  val ex_comm = thm "ex_comm"
    1.29 -in
    1.30 -
    1.31 -(*** make simplification procedures for quantifier elimination ***)
    1.32 +(** tools setup **)
    1.33  
    1.34  structure Quantifier1 = Quantifier1Fun
    1.35  (struct
    1.36    (*abstract syntax*)
    1.37 -  fun dest_eq((c as Const("op =",_)) $ s $ t) = SOME(c,s,t)
    1.38 +  fun dest_eq ((c as Const("op =",_)) $ s $ t) = SOME (c, s, t)
    1.39      | dest_eq _ = NONE;
    1.40 -  fun dest_conj((c as Const("op &",_)) $ s $ t) = SOME(c,s,t)
    1.41 +  fun dest_conj ((c as Const("op &",_)) $ s $ t) = SOME (c, s, t)
    1.42      | dest_conj _ = NONE;
    1.43 -  fun dest_imp((c as Const("op -->",_)) $ s $ t) = SOME(c,s,t)
    1.44 +  fun dest_imp ((c as Const("op -->",_)) $ s $ t) = SOME (c, s, t)
    1.45      | dest_imp _ = NONE;
    1.46    val conj = HOLogic.conj
    1.47    val imp  = HOLogic.imp
    1.48 @@ -51,32 +27,162 @@
    1.49    val conjE= HOL.conjE
    1.50    val impI = HOL.impI
    1.51    val mp   = HOL.mp
    1.52 -  val uncurry = uncurry
    1.53 +  val uncurry = thm "uncurry"
    1.54    val exI  = HOL.exI
    1.55    val exE  = HOL.exE
    1.56 -  val iff_allI = iff_allI
    1.57 -  val iff_exI = iff_exI
    1.58 -  val all_comm = all_comm
    1.59 -  val ex_comm = ex_comm
    1.60 +  val iff_allI = thm "iff_allI"
    1.61 +  val iff_exI = thm "iff_exI"
    1.62 +  val all_comm = thm "all_comm"
    1.63 +  val ex_comm = thm "ex_comm"
    1.64  end);
    1.65  
    1.66 +structure HOL =
    1.67 +struct
    1.68 +
    1.69 +open HOL;
    1.70 +
    1.71 +val Eq_FalseI = thm "Eq_FalseI";
    1.72 +val Eq_TrueI = thm "Eq_TrueI";
    1.73 +val simp_implies_def = thm "simp_implies_def";
    1.74 +val simp_impliesI = thm "simp_impliesI";
    1.75 +
    1.76 +fun mk_meta_eq r = r RS eq_reflection;
    1.77 +fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
    1.78 +
    1.79 +fun mk_eq thm = case concl_of thm
    1.80 +  (*expects Trueprop if not == *)
    1.81 +  of Const ("==",_) $ _ $ _ => thm
    1.82 +   | _ $ (Const ("op =", _) $ _ $ _) => mk_meta_eq thm
    1.83 +   | _ $ (Const ("Not", _) $ _) => thm RS Eq_FalseI
    1.84 +   | _ => thm RS Eq_TrueI;
    1.85 +
    1.86 +fun mk_eq_True r =
    1.87 +  SOME (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE;
    1.88 +
    1.89 +(* Produce theorems of the form
    1.90 +  (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y)
    1.91 +*)
    1.92 +fun lift_meta_eq_to_obj_eq i st =
    1.93 +  let
    1.94 +    fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q
    1.95 +      | count_imp _ = 0;
    1.96 +    val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1)))
    1.97 +  in if j = 0 then meta_eq_to_obj_eq
    1.98 +    else
    1.99 +      let
   1.100 +        val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
   1.101 +        fun mk_simp_implies Q = foldr (fn (R, S) =>
   1.102 +          Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps
   1.103 +        val aT = TFree ("'a", HOLogic.typeS);
   1.104 +        val x = Free ("x", aT);
   1.105 +        val y = Free ("y", aT)
   1.106 +      in Goal.prove_global (Thm.theory_of_thm st) []
   1.107 +        [mk_simp_implies (Logic.mk_equals (x, y))]
   1.108 +        (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))
   1.109 +        (fn prems => EVERY
   1.110 +         [rewrite_goals_tac [simp_implies_def],
   1.111 +          REPEAT (ares_tac (meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)])
   1.112 +      end
   1.113 +  end;
   1.114 +
   1.115 +(*Congruence rules for = (instead of ==)*)
   1.116 +fun mk_meta_cong rl = zero_var_indexes
   1.117 +  (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
   1.118 +     rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
   1.119 +   in mk_meta_eq rl' handle THM _ =>
   1.120 +     if can Logic.dest_equals (concl_of rl') then rl'
   1.121 +     else error "Conclusion of congruence rules must be =-equality"
   1.122 +   end);
   1.123 +
   1.124 +(*
   1.125 +val mk_atomize:      (string * thm list) list -> thm -> thm list
   1.126 +looks too specific to move it somewhere else
   1.127 +*)
   1.128 +fun mk_atomize pairs =
   1.129 +  let
   1.130 +    fun atoms thm = case concl_of thm
   1.131 +     of Const("Trueprop", _) $ p => (case head_of p
   1.132 +        of Const(a, _) => (case AList.lookup (op =) pairs a
   1.133 +           of SOME rls => maps atoms ([thm] RL rls)
   1.134 +            | NONE => [thm])
   1.135 +         | _ => [thm])
   1.136 +      | _ => [thm]
   1.137 +  in atoms end;
   1.138 +
   1.139 +fun mksimps pairs =
   1.140 +  (map_filter (try mk_eq) o mk_atomize pairs o gen_all);
   1.141 +
   1.142 +fun unsafe_solver_tac prems =
   1.143 +  (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
   1.144 +  FIRST'[resolve_tac(reflexive_thm :: TrueI :: refl :: prems), atac, etac FalseE];
   1.145 +val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
   1.146 +
   1.147 +(*No premature instantiation of variables during simplification*)
   1.148 +fun safe_solver_tac prems =
   1.149 +  (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
   1.150 +  FIRST'[match_tac(reflexive_thm :: TrueI :: refl :: prems),
   1.151 +         eq_assume_tac, ematch_tac [FalseE]];
   1.152 +val safe_solver = mk_solver "HOL safe" safe_solver_tac;
   1.153 +
   1.154  end;
   1.155  
   1.156 -val defEX_regroup =
   1.157 -  Simplifier.simproc (the_context ())
   1.158 -    "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
   1.159 +structure SplitterData =
   1.160 +struct
   1.161 +  structure Simplifier = Simplifier
   1.162 +  val mk_eq           = HOL.mk_eq
   1.163 +  val meta_eq_to_iff  = HOL.meta_eq_to_obj_eq
   1.164 +  val iffD            = HOL.iffD2
   1.165 +  val disjE           = HOL.disjE
   1.166 +  val conjE           = HOL.conjE
   1.167 +  val exE             = HOL.exE
   1.168 +  val contrapos       = HOL.contrapos_nn
   1.169 +  val contrapos2      = HOL.contrapos_pp
   1.170 +  val notnotD         = HOL.notnotD
   1.171 +end;
   1.172 +
   1.173 +structure Splitter = SplitterFun(SplitterData);
   1.174 +
   1.175 +(* integration of simplifier with classical reasoner *)
   1.176 +
   1.177 +structure Clasimp = ClasimpFun
   1.178 + (structure Simplifier = Simplifier and Splitter = Splitter
   1.179 +  and Classical  = Classical and Blast = Blast
   1.180 +  val iffD1 = HOL.iffD1 val iffD2 = HOL.iffD2 val notE = HOL.notE);
   1.181  
   1.182 -val defALL_regroup =
   1.183 -  Simplifier.simproc (the_context ())
   1.184 -    "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
   1.185 +structure HOL =
   1.186 +struct
   1.187 +
   1.188 +open HOL;
   1.189 +
   1.190 +val mksimps_pairs =
   1.191 +  [("op -->", [mp]), ("op &", [thm "conjunct1", thm "conjunct2"]),
   1.192 +   ("All", [spec]), ("True", []), ("False", []),
   1.193 +   ("HOL.If", [thm "if_bool_eq_conj" RS iffD1])];
   1.194  
   1.195 +val simpset_basic =
   1.196 +  Simplifier.theory_context (the_context ()) empty_ss
   1.197 +    setsubgoaler asm_simp_tac
   1.198 +    setSSolver safe_solver
   1.199 +    setSolver unsafe_solver
   1.200 +    setmksimps (mksimps mksimps_pairs)
   1.201 +    setmkeqTrue mk_eq_True
   1.202 +    setmkcong mk_meta_cong;
   1.203 +
   1.204 +fun simplify rews = Simplifier.full_simplify (simpset_basic addsimps rews);
   1.205 +
   1.206 +fun unfold_tac ths =
   1.207 +  let val ss0 = Simplifier.clear_ss simpset_basic addsimps ths
   1.208 +  in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
   1.209 +
   1.210 +(** simprocs **)
   1.211  
   1.212  (* simproc for proving "(y = x) == False" from premise "~(x = y)" *)
   1.213  
   1.214  val use_neq_simproc = ref true;
   1.215  
   1.216  local
   1.217 -  val neq_to_EQ_False = thm "not_sym" RS Eq_FalseI;
   1.218 +  val thy = the_context ();
   1.219 +  val neq_to_EQ_False = thm "not_sym" RS HOL.Eq_FalseI;
   1.220    fun neq_prover sg ss (eq $ lhs $ rhs) =
   1.221      let
   1.222        fun test thm = (case #prop (rep_thm thm) of
   1.223 @@ -91,10 +197,9 @@
   1.224      end
   1.225  in
   1.226  
   1.227 -val neq_simproc = Simplifier.simproc (the_context ())
   1.228 -  "neq_simproc" ["x = y"] neq_prover;
   1.229 +val neq_simproc = Simplifier.simproc thy "neq_simproc" ["x = y"] neq_prover;
   1.230  
   1.231 -end;
   1.232 +end; (*local*)
   1.233  
   1.234  
   1.235  (* Simproc for Let *)
   1.236 @@ -102,23 +207,24 @@
   1.237  val use_let_simproc = ref true;
   1.238  
   1.239  local
   1.240 +  val thy = the_context ();
   1.241    val Let_folded = thm "Let_folded";
   1.242    val Let_unfold = thm "Let_unfold";
   1.243 -  val (f_Let_unfold,x_Let_unfold) =
   1.244 +  val (f_Let_unfold, x_Let_unfold) =
   1.245        let val [(_$(f$x)$_)] = prems_of Let_unfold
   1.246 -      in (cterm_of (the_context ()) f,cterm_of (the_context ()) x) end
   1.247 -  val (f_Let_folded,x_Let_folded) =
   1.248 +      in (cterm_of thy f, cterm_of thy x) end
   1.249 +  val (f_Let_folded, x_Let_folded) =
   1.250        let val [(_$(f$x)$_)] = prems_of Let_folded
   1.251 -      in (cterm_of (the_context ()) f, cterm_of (the_context ()) x) end;
   1.252 +      in (cterm_of thy f, cterm_of thy x) end;
   1.253    val g_Let_folded =
   1.254 -      let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of (the_context ()) g end;
   1.255 +      let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of thy g end;
   1.256  in
   1.257  
   1.258  val let_simproc =
   1.259 -  Simplifier.simproc (the_context ()) "let_simp" ["Let x f"]
   1.260 +  Simplifier.simproc thy "let_simp" ["Let x f"]
   1.261     (fn sg => fn ss => fn t =>
   1.262       let val ctxt = Simplifier.the_context ss;
   1.263 -         val ([t'],ctxt') = Variable.import_terms false [t] ctxt;
   1.264 +         val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
   1.265       in Option.map (hd o Variable.export ctxt' ctxt o single)
   1.266        (case t' of (Const ("Let",_)$x$f) => (* x and f are already in normal form *)
   1.267           if not (!use_let_simproc) then NONE
   1.268 @@ -153,192 +259,9 @@
   1.269          | _ => NONE)
   1.270       end)
   1.271  
   1.272 -end
   1.273 -
   1.274 -(*** Case splitting ***)
   1.275 -
   1.276 -(*Make meta-equalities.  The operator below is Trueprop*)
   1.277 -
   1.278 -fun mk_meta_eq r = r RS HOL.eq_reflection;
   1.279 -fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
   1.280 -
   1.281 -fun mk_eq th = case concl_of th of
   1.282 -        Const("==",_)$_$_       => th
   1.283 -    |   _$(Const("op =",_)$_$_) => mk_meta_eq th
   1.284 -    |   _$(Const("Not",_)$_)    => th RS Eq_FalseI
   1.285 -    |   _                       => th RS Eq_TrueI;
   1.286 -(* Expects Trueprop(.) if not == *)
   1.287 -
   1.288 -fun mk_eq_True r =
   1.289 -  SOME (r RS HOL.meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE;
   1.290 -
   1.291 -(* Produce theorems of the form
   1.292 -  (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y)
   1.293 -*)
   1.294 -fun lift_meta_eq_to_obj_eq i st =
   1.295 -  let
   1.296 -    val {sign, ...} = rep_thm st;
   1.297 -    fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q
   1.298 -      | count_imp _ = 0;
   1.299 -    val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1)))
   1.300 -  in if j = 0 then HOL.meta_eq_to_obj_eq
   1.301 -    else
   1.302 -      let
   1.303 -        val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
   1.304 -        fun mk_simp_implies Q = foldr (fn (R, S) =>
   1.305 -          Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps
   1.306 -        val aT = TFree ("'a", HOLogic.typeS);
   1.307 -        val x = Free ("x", aT);
   1.308 -        val y = Free ("y", aT)
   1.309 -      in Goal.prove_global (Thm.theory_of_thm st) []
   1.310 -        [mk_simp_implies (Logic.mk_equals (x, y))]
   1.311 -        (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))
   1.312 -        (fn prems => EVERY
   1.313 -         [rewrite_goals_tac [simp_implies_def],
   1.314 -          REPEAT (ares_tac (HOL.meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)])
   1.315 -      end
   1.316 -  end;
   1.317 -
   1.318 -(*Congruence rules for = (instead of ==)*)
   1.319 -fun mk_meta_cong rl = zero_var_indexes
   1.320 -  (let val rl' = Seq.hd (TRYALL (fn i => fn st =>
   1.321 -     rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
   1.322 -   in mk_meta_eq rl' handle THM _ =>
   1.323 -     if can Logic.dest_equals (concl_of rl') then rl'
   1.324 -     else error "Conclusion of congruence rules must be =-equality"
   1.325 -   end);
   1.326 -
   1.327 -structure SplitterData =
   1.328 -struct
   1.329 -  structure Simplifier = Simplifier
   1.330 -  val mk_eq          = mk_eq
   1.331 -  val meta_eq_to_iff = HOL.meta_eq_to_obj_eq
   1.332 -  val iffD           = HOL.iffD2
   1.333 -  val disjE          = HOL.disjE
   1.334 -  val conjE          = HOL.conjE
   1.335 -  val exE            = HOL.exE
   1.336 -  val contrapos      = HOL.contrapos_nn
   1.337 -  val contrapos2     = HOL.contrapos_pp
   1.338 -  val notnotD        = HOL.notnotD
   1.339 -end;
   1.340 -
   1.341 -structure Splitter = SplitterFun(SplitterData);
   1.342 -
   1.343 -val split_tac        = Splitter.split_tac;
   1.344 -val split_inside_tac = Splitter.split_inside_tac;
   1.345 -val split_asm_tac    = Splitter.split_asm_tac;
   1.346 -val op addsplits     = Splitter.addsplits;
   1.347 -val op delsplits     = Splitter.delsplits;
   1.348 -val Addsplits        = Splitter.Addsplits;
   1.349 -val Delsplits        = Splitter.Delsplits;
   1.350 -
   1.351 -val mksimps_pairs =
   1.352 -  [("op -->", [HOL.mp]), ("op &", [thm "conjunct1", thm "conjunct2"]),
   1.353 -   ("All", [HOL.spec]), ("True", []), ("False", []),
   1.354 -   ("HOL.If", [thm "if_bool_eq_conj" RS HOL.iffD1])];
   1.355 +end; (*local*)
   1.356  
   1.357 -(*
   1.358 -val mk_atomize:      (string * thm list) list -> thm -> thm list
   1.359 -looks too specific to move it somewhere else
   1.360 -*)
   1.361 -fun mk_atomize pairs =
   1.362 -  let fun atoms th =
   1.363 -        (case concl_of th of
   1.364 -           Const("Trueprop",_) $ p =>
   1.365 -             (case head_of p of
   1.366 -                Const(a,_) =>
   1.367 -                  (case AList.lookup (op =) pairs a of
   1.368 -                     SOME(rls) => List.concat (map atoms ([th] RL rls))
   1.369 -                   | NONE => [th])
   1.370 -              | _ => [th])
   1.371 -         | _ => [th])
   1.372 -  in atoms end;
   1.373 -
   1.374 -fun mksimps pairs =
   1.375 -  (List.mapPartial (try mk_eq) o mk_atomize pairs o gen_all);
   1.376 -
   1.377 -fun unsafe_solver_tac prems =
   1.378 -  (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
   1.379 -  FIRST'[resolve_tac(reflexive_thm :: HOL.TrueI :: HOL.refl :: prems), atac, etac HOL.FalseE];
   1.380 -val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
   1.381 -
   1.382 -(*No premature instantiation of variables during simplification*)
   1.383 -fun safe_solver_tac prems =
   1.384 -  (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
   1.385 -  FIRST'[match_tac(reflexive_thm :: HOL.TrueI :: HOL.refl :: prems),
   1.386 -         eq_assume_tac, ematch_tac [HOL.FalseE]];
   1.387 -val safe_solver = mk_solver "HOL safe" safe_solver_tac;
   1.388 -
   1.389 -val HOL_basic_ss =
   1.390 -  Simplifier.theory_context (the_context ()) empty_ss
   1.391 -    setsubgoaler asm_simp_tac
   1.392 -    setSSolver safe_solver
   1.393 -    setSolver unsafe_solver
   1.394 -    setmksimps (mksimps mksimps_pairs)
   1.395 -    setmkeqTrue mk_eq_True
   1.396 -    setmkcong mk_meta_cong;
   1.397 -
   1.398 -fun unfold_tac ths =
   1.399 -  let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths
   1.400 -  in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
   1.401 -
   1.402 -(*In general it seems wrong to add distributive laws by default: they
   1.403 -  might cause exponential blow-up.  But imp_disjL has been in for a while
   1.404 -  and cannot be removed without affecting existing proofs.  Moreover,
   1.405 -  rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
   1.406 -  grounds that it allows simplification of R in the two cases.*)
   1.407 -
   1.408 -local
   1.409 -  val ex_simps = thms "ex_simps";
   1.410 -  val all_simps = thms "all_simps";
   1.411 -  val simp_thms = thms "simp_thms";
   1.412 -  val cases_simp = thm "cases_simp";
   1.413 -  val conj_assoc = thm "conj_assoc";
   1.414 -  val if_False = thm "if_False";
   1.415 -  val if_True = thm "if_True";
   1.416 -  val disj_assoc = thm "disj_assoc";
   1.417 -  val disj_not1 = thm "disj_not1";
   1.418 -  val if_cancel = thm "if_cancel";
   1.419 -  val if_eq_cancel = thm "if_eq_cancel";
   1.420 -  val True_implies_equals = thm "True_implies_equals";
   1.421 -in
   1.422 -
   1.423 -val HOL_ss =
   1.424 -    HOL_basic_ss addsimps
   1.425 -     ([triv_forall_equality, (* prunes params *)
   1.426 -       True_implies_equals, (* prune asms `True' *)
   1.427 -       if_True, if_False, if_cancel, if_eq_cancel,
   1.428 -       imp_disjL, conj_assoc, disj_assoc,
   1.429 -       de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, thm "not_imp",
   1.430 -       disj_not1, thm "not_all", thm "not_ex", cases_simp,
   1.431 -       thm "the_eq_trivial", HOL.the_sym_eq_trivial]
   1.432 -     @ ex_simps @ all_simps @ simp_thms)
   1.433 -     addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc]
   1.434 -     addcongs [imp_cong, simp_implies_cong]
   1.435 -     addsplits [thm "split_if"];
   1.436 -
   1.437 -end;
   1.438 -
   1.439 -fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
   1.440 -
   1.441 -(* default simpset *)
   1.442 -val simpsetup =
   1.443 -  (fn thy => (change_simpset_of thy (fn _ => HOL_ss); thy));
   1.444 -
   1.445 -
   1.446 -(*** integration of simplifier with classical reasoner ***)
   1.447 -
   1.448 -structure Clasimp = ClasimpFun
   1.449 - (structure Simplifier = Simplifier and Splitter = Splitter
   1.450 -  and Classical  = Classical and Blast = Blast
   1.451 -  val iffD1 = HOL.iffD1 val iffD2 = HOL.iffD2 val notE = HOL.notE);
   1.452 -open Clasimp;
   1.453 -
   1.454 -val HOL_css = (HOL_cs, HOL_ss);
   1.455 -
   1.456 -
   1.457 -
   1.458 -(*** A general refutation procedure ***)
   1.459 +(* A general refutation procedure *)
   1.460  
   1.461  (* Parameters:
   1.462  
   1.463 @@ -361,7 +284,7 @@
   1.464    val nnf_simpset =
   1.465      empty_ss setmkeqTrue mk_eq_True
   1.466      setmksimps (mksimps mksimps_pairs)
   1.467 -    addsimps [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj,
   1.468 +    addsimps [thm "imp_conv_disj", thm "iff_conv_conj_imp", thm "de_Morgan_disj", thm "de_Morgan_conj",
   1.469        thm "not_all", thm "not_ex", thm "not_not"];
   1.470    fun prem_nnf_tac i st =
   1.471      full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st;
   1.472 @@ -369,13 +292,27 @@
   1.473  fun refute_tac test prep_tac ref_tac =
   1.474    let val refute_prems_tac =
   1.475          REPEAT_DETERM
   1.476 -              (eresolve_tac [HOL.conjE, HOL.exE] 1 ORELSE
   1.477 +              (eresolve_tac [conjE, exE] 1 ORELSE
   1.478                 filter_prems_tac test 1 ORELSE
   1.479 -               etac HOL.disjE 1) THEN
   1.480 -        ((etac HOL.notE 1 THEN eq_assume_tac 1) ORELSE
   1.481 +               etac disjE 1) THEN
   1.482 +        ((etac notE 1 THEN eq_assume_tac 1) ORELSE
   1.483           ref_tac 1);
   1.484    in EVERY'[TRY o filter_prems_tac test,
   1.485 -            REPEAT_DETERM o etac HOL.rev_mp, prep_tac, rtac HOL.ccontr, prem_nnf_tac,
   1.486 +            REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
   1.487              SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
   1.488    end;
   1.489 -end;
   1.490 +end; (*local*)
   1.491 +
   1.492 +val defALL_regroup =
   1.493 +  Simplifier.simproc (the_context ())
   1.494 +    "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
   1.495 +
   1.496 +val defEX_regroup =
   1.497 +  Simplifier.simproc (the_context ())
   1.498 +    "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
   1.499 +
   1.500 +
   1.501 +val simpset_simprocs = simpset_basic
   1.502 +  addsimprocs [defALL_regroup, defEX_regroup, neq_simproc, let_simproc]
   1.503 +
   1.504 +end; (*struct*)
   1.505 \ No newline at end of file