# HG changeset patch
# User wenzelm
# Date 950186092 -3600
# Node ID 8283e416b680a1310a8da44b6fad5691707df26f
# Parent  d67db92897df5196ad0cdefbcb255cddcddf6789
added easy_setup;

diff -r d67db92897df -r 8283e416b680 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Thu Feb 10 13:34:38 2000 +0100
+++ b/src/Provers/simplifier.ML	Thu Feb 10 13:34:52 2000 +0100
@@ -94,6 +94,7 @@
   val change_simpset_of: (simpset * 'a -> simpset) -> 'a -> theory -> theory
   val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   val setup: (theory -> theory) list
+  val easy_setup: thm -> thm list -> (theory -> theory) list
 end;
 
 structure Simplifier: SIMPLIFIER =
@@ -514,6 +515,29 @@
 
 val setup = [GlobalSimpset.init, LocalSimpset.init, setup_attrs, setup_methods];
 
+fun easy_setup reflect trivs =
+  let
+    val trivialities = Drule.reflexive_thm :: trivs;
+
+    fun unsafe_solver_tac prems = FIRST' [resolve_tac (trivialities @ prems), assume_tac];
+    val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
+
+    (*no premature instantiation of variables during simplification*)
+    fun safe_solver_tac prems = FIRST' [match_tac (trivialities @ prems), eq_assume_tac];
+    val safe_solver = mk_solver "easy safe" safe_solver_tac;
+
+    fun mksimps thm =
+      if Logic.is_equals (Thm.concl_of thm) then [thm]
+      else [thm RS reflect] handle THM _ => [];
+
+    fun init_ss thy =
+      (simpset_ref_of thy :=
+        empty_ss setsubgoaler asm_simp_tac
+        setSSolver safe_solver
+        setSolver unsafe_solver
+        setmksimps mksimps; thy);
+  in setup @ [init_ss] end;
+
 
 end;