strengthened force_tac by using new first_best_tac

--- a/NEWS	Fri Jul 21 17:46:38 2000 +0200
+++ b/NEWS	Fri Jul 21 17:46:43 2000 +0200
@@ -46,6 +46,8 @@
 
 * Isar: changed syntax of local blocks from {{ }} to { };
 
+* Provers: strengthened force_tac by using new first_best_tac
+
 * Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g.
   [| inj ?f;          ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
 use instead the strong form,
@@ -53,6 +55,10 @@
 In HOL, FOL and ZF the function cla_make_elim will create such rules
 from destruct-rules;
 
+* Provers: safe_asm_full_simp_tac is no longer in the simplifier signature. Use
+  val safe_asm_full_simp_tac = generic_simp_tac true (true,true,true);
+  if required.
+
 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
 timing flag supersedes proof_timing and Toplevel.trace;
 

--- a/src/Provers/clasimp.ML	Fri Jul 21 17:46:38 2000 +0200
+++ b/src/Provers/clasimp.ML	Fri Jul 21 17:46:43 2000 +0200
@@ -77,10 +77,13 @@
 fun op addsimps2 arg = pair_upd2 Simplifier.addsimps arg;
 fun op delsimps2 arg = pair_upd2 Simplifier.delsimps arg;
 
+(*not totally safe: may instantiate unknowns that appear also in other subgoals*)
+val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true,true,true);
+
 (*Add a simpset to a classical set!*)
 (*Caution: only one simpset added can be added by each of addSss and addss*)
 fun cs addSss ss = Classical.addSaltern (cs, ("safe_asm_full_simp_tac",
-			    CHANGED o Simplifier.safe_asm_full_simp_tac ss));
+			    CHANGED o safe_asm_full_simp_tac ss));
 fun cs addss  ss = Classical.addbefore  (cs, ("asm_full_simp_tac", 
 			    CHANGED o Simplifier.asm_full_simp_tac ss));
 
@@ -93,7 +96,7 @@
   Classical.CLASET (fn cs => Simplifier.SIMPSET (fn ss => tacf (cs, ss) i)) state;
 
 
-fun clarsimp_tac (cs, ss) = Simplifier.safe_asm_full_simp_tac ss THEN_ALL_NEW
+fun clarsimp_tac (cs, ss) = safe_asm_full_simp_tac ss THEN_ALL_NEW
 			    Classical.clarify_tac (cs addSss ss);
 fun Clarsimp_tac i = clarsimp_tac (Classical.claset(), Simplifier.simpset()) i;
 
@@ -117,7 +120,7 @@
         )) i state;
 end;
 
-(*Designed to be idempotent, except if best_tac instantiates variables
+(*Designed to be idempotent, except if blast_depth_tac instantiates variables
   in some of the subgoals*)
 fun mk_auto_tac (cs, ss) m n =
     let val cs' = cs addss ss
@@ -138,14 +141,13 @@
 
 fun auto () = by Auto_tac;
 
-
 (* force_tac *)
 
 (* aimed to solve the given subgoal totally, using whatever tools possible *)
 fun force_tac (cs,ss) = let val cs' = cs addss ss in SELECT_GOAL (EVERY [
 	Classical.clarify_tac cs' 1,
 	IF_UNSOLVED (Simplifier.asm_full_simp_tac ss 1),
-	ALLGOALS (Classical.best_tac cs')]) end;
+	ALLGOALS (Classical.first_best_tac cs')]) end;
 fun Force_tac i = force_tac (Classical.claset(), Simplifier.simpset()) i;
 fun force i = by (Force_tac i);
 

--- a/src/Provers/classical.ML	Fri Jul 21 17:46:38 2000 +0200
+++ b/src/Provers/classical.ML	Fri Jul 21 17:46:43 2000 +0200
@@ -88,6 +88,7 @@
   val astar_tac		: claset -> int -> tactic
   val slow_astar_tac 	: claset -> int -> tactic
   val best_tac 		: claset -> int -> tactic
+  val first_best_tac	: claset -> int -> tactic
   val slow_best_tac 	: claset -> int -> tactic
   val depth_tac		: claset -> int -> int -> tactic
   val deepen_tac	: claset -> int -> int -> tactic
@@ -835,6 +836,10 @@
 fun best_tac cs = 
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
 
+(*even a bit smarter than best_tac*)
+fun first_best_tac cs = 
+  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
+
 fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
 
 fun slow_best_tac cs = 

--- a/src/ZF/AC/DC.ML	Fri Jul 21 17:46:38 2000 +0200
+++ b/src/ZF/AC/DC.ML	Fri Jul 21 17:46:43 2000 +0200
@@ -84,10 +84,10 @@
 by (asm_full_simp_tac (simpset() addsimps [XX_def]) 1);
 by Safe_tac;
 by (rtac bexI 1 THEN (assume_tac 2));
-by (force_tac (claset() addIs [ltD]
+by (best_tac (claset() addIs [ltD]
                         addSEs [nat_0_le RS leE]
-			addEs [sym RS trans RS succ_neq_0, domain_of_fun], 
-	       simpset() addsimps [RR_def]) 1);
+			addEs [sym RS trans RS succ_neq_0, domain_of_fun]
+	       addss (simpset() addsimps [RR_def])) 1);
 (** LEVEL 7, other subgoal **)
 by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1));
 by (subgoal_tac "f ` succ(succ(x)) : succ(k)->X" 1);