--- 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;