# HG changeset patch
# User bulwahn
# Date 1352372389 -3600
# Node ID d05f859558a00448498b31e7cba4c0a7f1ea18ed
# Parent  7747a9f4c3587cdfd12e1ff8bd2b5e68fc3a55c9
improving the extension of sets in case of more than one bound variable; rearranging the tactic to prefer simpler steps before more involved ones

diff -r 7747a9f4c358 -r d05f859558a0 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Nov 08 11:59:48 2012 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Nov 08 11:59:49 2012 +0100
@@ -214,7 +214,7 @@
   | map_atoms f (Un (fm1, fm2)) = Un (pairself (map_atoms f) (fm1, fm2))
   | map_atoms f (Int (fm1, fm2)) = Int (pairself (map_atoms f) (fm1, fm2))
 
-fun extend Ts bs t = fold (fn b => fn t => mk_sigma (t, HOLogic.mk_UNIV (nth Ts b))) bs t
+fun extend Ts bs t = foldr1 mk_sigma (t :: map (fn b => HOLogic.mk_UNIV (nth Ts b)) bs)
 
 fun rearrange vs (pat, pat') t =
   let
@@ -345,8 +345,10 @@
         (Trueprop_conv (eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq prod_case_distrib)))))) ctxt)))
 
 val elim_image_tac = etac @{thm imageE}
-  THEN' (TRY o REPEAT_DETERM1 o Splitter.split_asm_tac @{thms prod.split_asm})
-  THEN' hyp_subst_tac
+  THEN' REPEAT_DETERM o CHANGED o
+    (TRY o Simplifier.full_simp_tac (HOL_basic_ss addsimps @{thms split_paired_all prod.cases})
+    THEN' REPEAT_DETERM o etac @{thm Pair_inject}
+    THEN' TRY o hyp_subst_tac)
 
 fun tac1_of_formula (Int (fm1, fm2)) =
     TRY o etac @{thm conjE}
@@ -359,7 +361,8 @@
     THEN' rtac @{thm UnI2}
     THEN' tac1_of_formula fm2
   | tac1_of_formula (Atom _) =
-    REPEAT_DETERM1 o (rtac @{thm SigmaI}
+    REPEAT_DETERM1 o (atac
+      ORELSE' rtac @{thm SigmaI}
       ORELSE' ((rtac @{thm CollectI} ORELSE' rtac collectI') THEN' TRY o Simplifier.simp_tac (HOL_basic_ss addsimps [@{thm prod.cases}]))
       ORELSE' ((rtac @{thm vimageI2} ORELSE' rtac vimageI2') THEN'
         TRY o Simplifier.simp_tac (HOL_basic_ss addsimps [@{thm prod.cases}])) 
@@ -383,21 +386,21 @@
     THEN' tac2_of_formula fm2
   | tac2_of_formula (Atom _) =
     REPEAT_DETERM o
-      (dtac @{thm iffD1[OF mem_Sigma_iff]}
+      (atac
+       ORELSE' dtac @{thm iffD1[OF mem_Sigma_iff]}
+       ORELSE' etac @{thm conjE}
        ORELSE' ((etac @{thm CollectE} ORELSE' etac collectE') THEN'
          TRY o Simplifier.full_simp_tac (HOL_basic_ss addsimps [@{thm prod.cases}]) THEN'
          REPEAT_DETERM o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac THEN' TRY o rtac @{thm refl})
-       ORELSE' (REPEAT_DETERM1 o etac @{thm imageE}
-         THEN' (TRY o REPEAT_DETERM1 o Splitter.split_asm_tac @{thms prod.split_asm})
+       ORELSE' (etac @{thm imageE}
+         THEN' (REPEAT_DETERM o CHANGED o
+         (TRY o Simplifier.full_simp_tac (HOL_basic_ss addsimps @{thms split_paired_all prod.cases})
          THEN' REPEAT_DETERM o etac @{thm Pair_inject}
-         THEN' TRY o hyp_subst_tac)
-       ORELSE' etac @{thm conjE}
+         THEN' TRY o hyp_subst_tac THEN' TRY o rtac @{thm refl})))
        ORELSE' etac @{thm ComplE}
        ORELSE' ((etac @{thm vimageE} ORELSE' etac vimageE')
         THEN' TRY o Simplifier.full_simp_tac (HOL_basic_ss addsimps [@{thm prod.cases}])
-        THEN' TRY o hyp_subst_tac)
-       ORELSE' (REPEAT_DETERM1 o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac)
-       ORELSE' atac)
+        THEN' TRY o hyp_subst_tac THEN' TRY o rtac @{thm refl}))
 
 fun tac ctxt fm =
   let