# HG changeset patch
# User bulwahn
# Date 1350386290 -7200
# Node ID 4b7c2e4991fcf98fb2d4886b8e0372bb2267f2de
# Parent  c6a686c9be2aa3b5f481f1802e65d85b817fbcf0
extending preprocessing of simproc to rewrite subset inequality into membership of powerset

diff -r c6a686c9be2a -r 4b7c2e4991fc src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Tue Oct 16 13:15:58 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Tue Oct 16 13:18:10 2012 +0200
@@ -265,6 +265,8 @@
 
 (* main simprocs *)
 
+val prep_thms = map mk_meta_eq [@{thm Bex_def}, @{thm Pow_iff[symmetric]}]
+
 val post_thms =
   map mk_meta_eq [@{thm Times_Un_distrib1[symmetric]},
   @{lemma "A \<times> B \<union> A \<times> C = A \<times> (B \<union> C)" by auto},
@@ -273,12 +275,11 @@
 fun conv ctxt t =
   let
     val ct = cterm_of (Proof_Context.theory_of ctxt) t
-    val Bex_def = mk_meta_eq @{thm Bex_def}
-    val unfold_eq = Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv Bex_def))) ctxt ct
-    val t' = term_of (Thm.rhs_of unfold_eq)
+    val prep_eq = Raw_Simplifier.rewrite true prep_thms ct 
+    val t' = term_of (Thm.rhs_of prep_eq)
     fun mk_thm (fm, t'') = Goal.prove ctxt [] []
       (HOLogic.mk_Trueprop (HOLogic.mk_eq (t', t''))) (fn {context, ...} => tac context fm 1)
-    fun unfold th = th RS ((unfold_eq RS meta_eq_to_obj_eq) RS @{thm trans})
+    fun unfold th = th RS ((prep_eq RS meta_eq_to_obj_eq) RS @{thm trans})
     fun post th = Conv.fconv_rule (Trueprop_conv (eq_conv Conv.all_conv
       (Raw_Simplifier.rewrite true post_thms))) th
   in