# HG changeset patch
# User lcp
# Date 781960194 -3600
# Node ID 9e4d4f3eb812c090e6772cee35642f5cd288491b
# Parent  f9a3f77f71e84aebb4d78260c00896e1785df25e
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
solve the goal fully before proceeding

{HOL,ZF}/indrule/mutual_ind_tac: ensures that calls to "prem" cannot loop;
calls DEPTH_SOLVE_1 instead of REPEAT to solve the goal fully

diff -r f9a3f77f71e8 -r 9e4d4f3eb812 src/ZF/indrule.ML
--- a/src/ZF/indrule.ML	Wed Oct 12 11:09:11 1994 +0100
+++ b/src/ZF/indrule.ML	Wed Oct 12 12:09:54 1994 +0100
@@ -59,10 +59,12 @@
   in list_all_free (quantfrees, list_implies (iprems,concl)) end
   handle Bind => error"Recursion term not found in conclusion";
 
-(*Avoids backtracking by delivering the correct premise to each goal*)
+(*Reduces backtracking by delivering the correct premise to each goal.
+  Intro rules with extra Vars in premises still cause some backtracking *)
 fun ind_tac [] 0 = all_tac
-  | ind_tac(prem::prems) i = REPEAT (ares_tac [Part_eqI, prem, refl] i) THEN
-			     ind_tac prems (i-1);
+  | ind_tac(prem::prems) i = 
+    	DEPTH_SOLVE_1 (ares_tac [Part_eqI, prem, refl] i) THEN
+	ind_tac prems (i-1);
 
 val pred = Free(pred_name, iT-->oT);
 
@@ -136,15 +138,22 @@
 (*Avoids backtracking by delivering the correct premise to each goal*)
 fun mutual_ind_tac [] 0 = all_tac
   | mutual_ind_tac(prem::prems) i = 
-      SELECT_GOAL 
-	((*unpackage and use "prem" in the corresponding place*)
-	 REPEAT (FIRSTGOAL
-		    (eresolve_tac ([conjE,mp]@cmonos) ORELSE'
-		     ares_tac [prem,impI,conjI]))
-	 (*prove remaining goals by contradiction*)
-	 THEN rewrite_goals_tac (con_defs@part_rec_defs)
-	 THEN REPEAT (eresolve_tac (PartE :: sumprod_free_SEs) 1))
-	i  THEN mutual_ind_tac prems (i-1);
+      DETERM
+       (SELECT_GOAL 
+	  ((*unpackage and use "prem" in the corresponding place*)
+	   REPEAT (FIRSTGOAL
+		   (etac conjE ORELSE' eq_mp_tac ORELSE' 
+		    ares_tac [impI, conjI]))
+	   (*prem is not allowed in the REPEAT, lest it loop!*)
+	   THEN TRYALL (rtac prem)
+	   THEN REPEAT
+		  (FIRSTGOAL (ares_tac [impI] ORELSE' 
+			      eresolve_tac (mp::cmonos)))
+	   (*prove remaining goals by contradiction*)
+	   THEN rewrite_goals_tac (con_defs@part_rec_defs)
+	   THEN DEPTH_SOLVE (eresolve_tac (PartE :: sumprod_free_SEs) 1))
+	  i)
+       THEN mutual_ind_tac prems (i-1);
 
 val mutual_induct_fsplit = 
     prove_goalw_cterm []