# HG changeset patch
# User bulwahn
# Date 1350716973 -7200
# Node ID 28cd3c9ca27838e07d326067c6575e0ee7394ae1
# Parent  6a26fed717550ee16a78ee7116d6845f93fba518
tuned tactic in set_comprehension_pointfree simproc to handle composition of negation and vimage

diff -r 6a26fed71755 -r 28cd3c9ca278 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sat Oct 20 09:09:32 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Sat Oct 20 09:09:33 2012 +0200
@@ -235,6 +235,10 @@
     Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
   | _ => raise CTERM ("eq_conv", [ct]))
 
+val vimageI2' = @{lemma "f a \<notin> A ==> a \<notin> f -` A" by simp}
+val vimageE' =
+  @{lemma "a \<notin> f -` B ==> (\<And> x. f a = x ==> x \<notin> B ==> P) ==> P" by simp}
+
 val elim_Collect_tac = dtac @{thm iffD1[OF mem_Collect_eq]}
   THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE}))
   THEN' TRY o etac @{thm conjE}
@@ -264,7 +268,7 @@
     THEN' tac1_of_formula fm2
   | tac1_of_formula (Atom _) =
     REPEAT_DETERM1 o (rtac @{thm SigmaI}
-      ORELSE' (rtac @{thm vimageI2} THEN'
+      ORELSE' ((rtac @{thm vimageI2} ORELSE' rtac 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]}
@@ -284,10 +288,10 @@
     TRY o REPEAT_DETERM1 o
       (dtac @{thm iffD1[OF mem_Sigma_iff]}
        ORELSE' etac @{thm conjE}
-       ORELSE' (etac @{thm vimageE}
+       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' etac @{thm ComplE}
        ORELSE' atac)
 
 fun tac ctxt fm =