# HG changeset patch
# User bulwahn
# Date 1350386293 -7200
# Node ID 0adcb5cd4eba59c8bb5d5a9d790d186c99272e54
# Parent  72b6d5fb407f9a920d5f0edd92b1b6ebe1d115d3
tactic of set_comprehension_pointfree simproc handles f x y : S patterns with Set.vimage

diff -r 72b6d5fb407f -r 0adcb5cd4eba src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Tue Oct 16 13:18:12 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Tue Oct 16 13:18:13 2012 +0200
@@ -246,10 +246,12 @@
     THEN' rtac @{thm UnI2}
     THEN' tac1_of_formula fm2
   | tac1_of_formula (Atom _) =
-    (REPEAT_DETERM1 o (rtac @{thm SigmaI}
+    REPEAT_DETERM1 o (rtac @{thm SigmaI}
+      ORELSE' (rtac @{thm vimageI2} THEN'
+        TRY o Simplifier.simp_tac (HOL_basic_ss addsimps [@{thm prod.cases}])) 
       ORELSE' rtac @{thm UNIV_I}
       ORELSE' rtac @{thm iffD2[OF Compl_iff]}
-      ORELSE' atac))
+      ORELSE' atac)
 
 fun tac2_of_formula (Int (fm1, fm2)) =
     TRY o etac @{thm IntE}
@@ -265,6 +267,9 @@
     TRY o REPEAT_DETERM1 o
       (dtac @{thm iffD1[OF mem_Sigma_iff]}
        ORELSE' etac @{thm conjE}
+       ORELSE' (etac @{thm vimageE}
+        THEN' TRY o Simplifier.full_simp_tac (HOL_basic_ss addsimps [@{thm prod.cases}])
+        THEN' TRY o hyp_subst_tac)
        ORELSE' etac @{thm ComplE}
        ORELSE' atac)