--- a/src/Provers/clasimp.ML Thu Feb 26 15:41:46 1998 +0100
+++ b/src/Provers/clasimp.ML Thu Feb 26 15:45:33 1998 +0100
@@ -6,12 +6,12 @@
to be used after installing both of them
*)
+type clasimpset = claset * simpset;
+
infix 4 addSIs2 addSEs2 addSDs2 addIs2 addEs2 addDs2
addsimps2 delsimps2 addcongs2 delcongs2;
infix 4 addSss addss;
-type clasimpset = claset * simpset;
-
signature CLASIMP =
sig
val addSIs2 : clasimpset * thm list -> clasimpset
@@ -28,11 +28,17 @@
val auto_tac : clasimpset -> tactic
val Auto_tac : tactic
val auto : unit -> unit
+ val smart_tac : clasimpset -> int -> tactic
+ val Smart_tac : int -> tactic
+ val smart : int -> unit
end;
structure Clasimp: CLASIMP =
struct
+(* this interface for updating a clasimpset is rudimentary and just for
+ convenience for the most common cases.
+ In other cases a clasimpset may be dealt with componentwise. *)
local
fun pair_upd1 f ((a,b),x) = (f(a,x), b);
fun pair_upd2 f ((a,b),x) = (a, f(b,x));
@@ -107,4 +113,12 @@
fun auto () = by Auto_tac;
+(* aimed to solve the given subgoal totally, using whatever tools possible *)
+fun smart_tac (cs,ss) = let val cs' = cs addss ss in SELECT_GOAL (EVERY [
+ clarify_tac cs' 1,
+ IF_UNSOLVED (asm_full_simp_tac ss 1),
+ IF_UNSOLVED (fast_tac cs' 1)]) end;
+fun Smart_tac i = smart_tac (claset(), simpset()) i;
+fun smart i = by (Smart_tac i);
+
end;