# HG changeset patch
# User oheimb
# Date 893172319 -7200
# Node ID ef2e8e2a10e13a2d994d2e265d3dea469cc2ec64
# Parent  90dab9f7d81eab0d97d9e65de4b2cc757de21aad
improved pair_tac to call prune_params_tac afterwards
improved the (bad) efficiency of split_all_tac by about 50%
split_all_tac is now added to claset() _before_ other safe tactics

diff -r 90dab9f7d81e -r ef2e8e2a10e1 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Tue Apr 21 17:23:24 1998 +0200
+++ b/src/HOL/Prod.ML	Tue Apr 21 17:25:19 1998 +0200
@@ -54,34 +54,34 @@
 by (REPEAT (eresolve_tac [prem,exE] 1));
 qed "PairE";
 
-fun pair_tac s = res_inst_tac [("p",s)] PairE THEN' hyp_subst_tac;
+fun pair_tac s = EVERY' [res_inst_tac [("p",s)] PairE, hyp_subst_tac,
+			 K prune_params_tac];
 
 (* replace parameters of product type by individual component parameters *)
 local
-fun is_pair (_,Type("*",_)) = true
-  | is_pair _ = false;
-
-fun find_pair_param prem =
-  let val params = Logic.strip_params prem
-  in if exists is_pair params
-     then let val params = rev(rename_wrt_term prem params)
-                           (*as they are printed*)
-          in apsome fst (find_first is_pair params) end
-     else None
-  end;
-
+  fun is_pair (_,Type("*",_)) = true
+    | is_pair  _              = false;
+  fun ptac x = res_inst_tac [("p",x)] PairE;
+  fun find_pair_params prem =
+    let val params = Logic.strip_params prem
+    in if exists is_pair params
+       then let val params = rev(rename_wrt_term prem params)
+                             (*as they are printed*)
+            in filter is_pair params end
+       else []
+   end;
 in
-
-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,
-                    REPEAT(hyp_subst_tac i), prune_params_tac]);
-
+val split_all_tac = REPEAT1 o SUBGOAL (fn (prem,i) => 
+  let val params = find_pair_params prem in
+  if params = [] then no_tac 
+  	         else EVERY'[EVERY' (map (ptac o fst) params),
+			     REPEAT o hyp_subst_tac,
+			     K prune_params_tac] i end)
 end;
 
-(* claset_ref() := claset() addbefore  ("split_all_tac", TRY o split_all_tac);*)
-   claset_ref() := claset() addSaltern ("split_all_tac",       split_all_tac);
+(*claset_ref() := claset()  addbefore  ("split_all_tac", TRY o split_all_tac);*)
+  claset_ref() := claset() addSWrapper ("split_all_tac", 
+					fn tac2 => split_all_tac ORELSE' tac2);
 
 (*** lemmas for splitting paired `!!'
 Does not work with simplifier because it also affects premises in
@@ -163,7 +163,7 @@
 qed_goal "split_eta" Prod.thy "(%(x,y). f(x,y)) = f"
   (K [rtac ext 1, split_all_tac 1, rtac split 1]);
 
-val split_beta = prove_goal Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)"
+qed_goal "split_beta" Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)"
 	(K [stac surjective_pairing 1, stac split 1, rtac refl 1]);
 
 (*For use with split_tac and the simplifier*)