split_all_tac now fails if there is nothing to split
split_all_tac has moved within claset() from usafe wrappers to safe wrappers

--- a/src/HOL/IMP/Transition.ML	Thu Apr 02 13:49:04 1998 +0200
+++ b/src/HOL/IMP/Transition.ML	Thu Apr 02 17:19:02 1998 +0200
@@ -33,12 +33,8 @@
   "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
 \              (c;d, s) -*-> (SKIP, u)";
 by (nat_ind_tac "n" 1);
- (* case n = 0 *)
  by (fast_tac (claset() addIs [rtrancl_into_rtrancl2])1);
-(* induction step *)
-by (safe_tac (claset() addSDs [rel_pow_Suc_D2]));
-by (split_all_tac 1);
-by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
+by (fast_tac  (claset() addIs [rtrancl_into_rtrancl2]addSDs [rel_pow_Suc_D2])1);
 qed_spec_mp "lemma1";
 
 

--- a/src/HOL/IOA/IOA.ML	Thu Apr 02 13:49:04 1998 +0200
+++ b/src/HOL/IOA/IOA.ML	Thu Apr 02 17:19:02 1998 +0200
@@ -56,18 +56,19 @@
 "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t";
   by (asm_full_simp_tac (simpset() delsimps bex_simps) 1);
   by Safe_tac;
-  by (res_inst_tac [("x","(%i. if i<n then fst ex i                    \
+  by (rename_tac "n ex1 ex2 a1 a4 a5 a2 a3" 1);
+  by (res_inst_tac [("x","(%i. if i<n then ex1 i                    \
 \                            else (if i=n then Some a else None),    \
-\                         %i. if i<Suc n then snd ex i else t)")] bexI 1);
-  by (res_inst_tac [("x","Suc(n)")] exI 1);
-  by (Simp_tac 1);
-  by (Asm_simp_tac 1);
+\                         %i. if i<Suc n then ex2 i else t)")] bexI 1);
+   by (res_inst_tac [("x","Suc(n)")] exI 1);
+   by (Simp_tac 1);
+  by (Asm_full_simp_tac 1);
   by (REPEAT(rtac allI 1));
   by (res_inst_tac [("m","na"),("n","n")] (make_elim less_linear) 1);
   by (etac disjE 1);
-  by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
+   by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
   by (etac disjE 1);
-  by (Asm_simp_tac 1);
+   by (Asm_simp_tac 1);
   by (forward_tac [less_not_sym] 1);
   by (asm_simp_tac (simpset() addsimps [less_not_refl2,less_Suc_eq]) 1);
 qed "reachable_n";
@@ -78,14 +79,16 @@
 \  ==> invariant A P";
   by (rewrite_goals_tac(reachable_def::Let_def::exec_rws));
   by Safe_tac;
-  by (res_inst_tac [("Q","reachable A (snd ex n)")] conjunct1 1);
+  by (rename_tac "n ex1 ex2" 1);
+  by (res_inst_tac [("Q","reachable A (ex2 n)")] conjunct1 1);
+  by (Asm_full_simp_tac 1);
   by (nat_ind_tac "n" 1);
-  by (fast_tac (claset() addIs [p1,reachable_0]) 1);
-  by (eres_inst_tac[("x","n")]allE 1);
-  by (exhaust_tac "fst ex n" 1 THEN ALLGOALS Asm_full_simp_tac);
+   by (fast_tac (claset() addIs [p1,reachable_0]) 1);
+  by (eres_inst_tac[("x","n")] allE 1);
+  by (exhaust_tac "ex1 n" 1 THEN ALLGOALS Asm_full_simp_tac);
   by Safe_tac;
-  by (etac (p2 RS mp) 1);
-  by (ALLGOALS(fast_tac(claset() addDs [reachable_n])));
+   by (etac (p2 RS mp) 1);
+    by (ALLGOALS(fast_tac(claset() addDs [reachable_n])));
 qed "invariantI";
 
 val [p1,p2] = goal IOA.thy

--- a/src/HOL/IOA/Solve.ML	Thu Apr 02 13:49:04 1998 +0200
+++ b/src/HOL/IOA/Solve.ML	Thu Apr 02 17:19:02 1998 +0200
@@ -16,16 +16,17 @@
 
   by (simp_tac(simpset() addsimps [has_trace_def])1);
   by Safe_tac;
+  by (rename_tac "f ex1 ex2" 1);
 
   (* choose same trace, therefore same NF *)
-  by (res_inst_tac[("x","mk_trace  C (fst ex)")] exI 1);
+  by (res_inst_tac[("x","mk_trace  C ex1")] exI 1);
   by (Asm_full_simp_tac 1);
 
   (* give execution of abstract automata *)
-  by (res_inst_tac[("x","(mk_trace A (fst ex),%i. f(snd ex i))")] bexI 1);
+  by (res_inst_tac[("x","(mk_trace A ex1,%i. f (ex2 i))")] bexI 1);
 
   (* Traces coincide *)
-  by (asm_simp_tac (simpset() addsimps [mk_trace_def,filter_oseq_idemp])1);
+   by (asm_simp_tac (simpset() addsimps [mk_trace_def,filter_oseq_idemp])1);
 
   (* Use lemma *)
   by (forward_tac [states_of_exec_reachable] 1);
@@ -42,8 +43,8 @@
   by (asm_full_simp_tac (simpset() addsimps [is_execution_fragment_def])1);
   by Safe_tac;
 
-  by (eres_inst_tac [("x","snd ex n")] allE 1);
-  by (eres_inst_tac [("x","snd ex (Suc n)")] allE 1);
+  by (eres_inst_tac [("x","ex2 n")] allE 1);
+  by (eres_inst_tac [("x","ex2 (Suc n)")] allE 1);
   by (eres_inst_tac [("x","a")] allE 1);
   by (Asm_full_simp_tac 1);
 qed "trace_inclusion";
@@ -73,7 +74,7 @@
 \    %i. fst (snd ex i))")]  bexI 1);
 (* fst(s) is in projected execution *)
  by (Simp_tac 1);
- by (fast_tac (claset() delWrapper "split_all_tac") 1);
+ by (fast_tac (claset() delSWrapper "split_all_tac") 1);
 (* projected execution is indeed an execution *)
 by (asm_full_simp_tac
       (simpset() addsimps [executions_def,is_execution_fragment_def,
@@ -93,7 +94,7 @@
 \    %i. snd (snd ex i))")]  bexI 1);
 (* fst(s) is in projected execution *)
  by (Simp_tac 1);
- by (fast_tac (claset() delWrapper "split_all_tac") 1);
+ by (fast_tac (claset() delSWrapper "split_all_tac") 1);
 (* projected execution is indeed an execution *)
 by (asm_full_simp_tac
       (simpset() addsimps [executions_def,is_execution_fragment_def,

--- a/src/HOL/Integ/Integ.ML	Thu Apr 02 13:49:04 1998 +0200
+++ b/src/HOL/Integ/Integ.ML	Thu Apr 02 17:19:02 1998 +0200
@@ -321,9 +321,10 @@
 \               split (%x1 y1. split (%x2 y2.   \
 \                   intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
 by (rtac (equiv_intrel RS congruent2_commuteI) 1);
-by Safe_tac;
-by (rewtac split_def);
-by (simp_tac (simpset() addsimps add_ac@mult_ac) 1);
+ by Safe_tac;
+ by (rewtac split_def);
+ by (simp_tac (simpset() addsimps add_ac@mult_ac) 1);
+by (rename_tac "x1 y1 x2 y2 z1 z2" 1);
 by (asm_simp_tac (simpset() delsimps [equiv_intrel_iff]
                            addsimps add_ac@mult_ac) 1);
 by (rtac (intrelI RS(equiv_intrel RS equiv_class_eq)) 1);

--- a/src/HOL/Prod.ML	Thu Apr 02 13:49:04 1998 +0200
+++ b/src/HOL/Prod.ML	Thu Apr 02 17:19:02 1998 +0200
@@ -72,7 +72,7 @@
 
 in
 
-val split_all_tac = REPEAT o SUBGOAL (fn (prem,i) =>
+val split_all_tac = REPEAT1 o SUBGOAL (fn (prem,i) =>
   case find_pair_param prem of
     None => no_tac
   | Some x => EVERY[res_inst_tac[("p",x)] PairE i,
@@ -80,8 +80,7 @@
 
 end;
 
-(* consider addSbefore ?? *)
-claset_ref() := claset() addbefore ("split_all_tac",split_all_tac);
+claset_ref() := claset() addSaltern ("split_all_tac", split_all_tac);
 
 (*** lemmas for splitting paired `!!'
 Does not work with simplifier because it also affects premises in
@@ -446,7 +445,7 @@
 
 (*Attempts to remove occurrences of split, and pair-valued parameters*)
 val remove_split = rewrite_rule [split RS eq_reflection]  o  
-                   rule_by_tactic (ALLGOALS split_all_tac);
+                   rule_by_tactic (TRYALL split_all_tac);
 
 (*Uncurries any Var of function type in the rule*)
 fun split_rule_var (t as Var(v, Type("fun",[T1,T2])), rl) =

--- a/src/HOL/Trancl.ML	Thu Apr 02 13:49:04 1998 +0200
+++ b/src/HOL/Trancl.ML	Thu Apr 02 17:19:02 1998 +0200
@@ -153,10 +153,7 @@
 qed "rtrancl_converseI";
 
 goal Trancl.thy "(r^-1)^* = (r^*)^-1";
-by (safe_tac (claset() addSIs [rtrancl_converseI]));
-by (res_inst_tac [("p","x")] PairE 1);
-by (hyp_subst_tac 1);
-by (etac rtrancl_converseD 1);
+by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]));
 qed "rtrancl_converse";
 
 val major::prems = goal Trancl.thy
@@ -336,9 +333,8 @@
 goal Trancl.thy "(r^+)^= = r^*";
 by Safe_tac;
 by  (etac trancl_into_rtrancl 1);
-by (split_all_tac 1);
 by (etac rtranclE 1);
-auto();
+by  (Auto_tac );
 by (etac rtrancl_into_trancl1 1);
 ba 1;
 qed "reflcl_trancl";
@@ -348,7 +344,6 @@
 by Safe_tac;
 by  (dtac trancl_into_rtrancl 1);
 by  (Asm_full_simp_tac 1);
-by (split_all_tac 1);
 by (etac rtranclE 1);
 by  Safe_tac;
 by  (rtac r_into_trancl 1);