# HG changeset patch
# User bulwahn
# Date 1350234995 -7200
# Node ID caaa1956f0da506ab1368100d190f5631257536e
# Parent  4d33963962fa86de2fc048b3002e5620d069f6f5
refined tactic in set_comprehension_pointfree simproc

diff -r 4d33963962fa -r caaa1956f0da src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Oct 14 19:16:33 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Oct 14 19:16:35 2012 +0200
@@ -130,6 +130,8 @@
   | mk_formula (@{const HOL.disj} $ t1 $ t2) = merge Un (mk_formula t1) (mk_formula t2)
   | mk_formula t = apfst single (mk_atom t)
 
+fun strip_Int (Int (fm1, fm2)) = fm1 :: (strip_Int fm2) 
+  | strip_Int fm = [fm]
 
 (* term construction *)
 
@@ -208,12 +210,6 @@
   THEN' (TRY o REPEAT_DETERM1 o Splitter.split_asm_tac @{thms prod.split_asm})
   THEN' hyp_subst_tac
 
-val intro_Collect_tac = rtac @{thm iffD2[OF mem_Collect_eq]}
-  THEN' REPEAT_DETERM1 o resolve_tac @{thms exI}
-  THEN' (TRY o (rtac @{thm conjI}))
-  THEN' (TRY o hyp_subst_tac)
-  THEN' rtac @{thm refl};
-
 fun tac1_of_formula (Int (fm1, fm2)) =
     TRY o etac @{thm conjE}
     THEN' rtac @{thm IntI}
@@ -255,8 +251,12 @@
       THEN' (tac1_of_formula fm)
     val subset_tac2 = rtac @{thm subsetI}
       THEN' elim_image_tac
-      THEN' intro_Collect_tac
-      THEN' tac2_of_formula fm
+      THEN' rtac @{thm iffD2[OF mem_Collect_eq]}
+      THEN' REPEAT_DETERM1 o resolve_tac @{thms exI}
+      THEN' (TRY o REPEAT_ALL_NEW (rtac @{thm conjI}))
+      THEN' (K (SOMEGOAL ((TRY o hyp_subst_tac) THEN' rtac @{thm refl})))
+      THEN' (fn i => EVERY (rev (map_index (fn (j, f) =>
+        REPEAT_DETERM (etac @{thm IntE} (i + j)) THEN tac2_of_formula f (i + j)) (strip_Int fm))))
   in
     rtac @{thm subset_antisym} THEN' subset_tac1 THEN' subset_tac2
   end;