# HG changeset patch
# User bulwahn
# Date 1350476037 -7200
# Node ID a39deedd5c3f5bb05184c161e594fdc3c259e83c
# Parent  b0d6d2e7a52269232331eb1dbccbedccdb5c2704
employing a preprocessing conversion that rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} in set_comprehension_pointfree simproc

diff -r b0d6d2e7a522 -r a39deedd5c3f src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Oct 17 00:16:31 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Oct 17 14:13:57 2012 +0200
@@ -292,6 +292,43 @@
   end;
 
 
+(* preprocessing conversion:
+  rewrites {(x1, ..., xn). P x1 ... xn} to {(x1, ..., xn) | x1 ... xn. P x1 ... xn} *)
+
+fun comprehension_conv ctxt ct =
+let
+  fun dest_Collect (Const (@{const_name Collect}, T) $ t) = (HOLogic.dest_setT (body_type T), t)
+    | dest_Collect t = raise TERM ("dest_Collect", [t])
+  fun list_ex Ts t = fold_rev (fn T => fn t => HOLogic.exists_const T $ absdummy T t) Ts t
+  fun mk_term t =
+    let
+      val (T, t') = dest_Collect t
+      val (t'', Ts, fp) = HOLogic.strip_psplits t'
+      val eq = HOLogic.eq_const T $ Bound (length Ts) $
+        (HOLogic.mk_ptuple fp (HOLogic.mk_ptupleT fp Ts) (rev (map_index (fn (i, _) => Bound i) Ts)))
+    in
+      HOLogic.Collect_const T $ absdummy T (list_ex Ts (HOLogic.mk_conj (eq, t'')))
+    end;
+  val tac = 
+    rtac @{thm set_eqI}
+    THEN' Simplifier.simp_tac
+      (HOL_basic_ss addsimps [@{thm split_paired_all}, @{thm mem_Collect_eq}, @{thm prod.cases}])
+    THEN' rtac @{thm iffI}
+    THEN' REPEAT_DETERM o rtac @{thm exI}
+    THEN' rtac @{thm conjI} THEN' rtac @{thm refl} THEN' atac
+    THEN' REPEAT_DETERM o etac @{thm exE}
+    THEN' etac @{thm conjE}
+    THEN' REPEAT_DETERM o etac @{thm Pair_inject}
+    THEN' hyp_subst_tac THEN' atac
+in
+  case try mk_term (term_of ct) of
+    NONE => Thm.reflexive ct
+  | SOME t' =>
+     Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (term_of ct, t'))) (K (tac 1))
+       RS @{thm eq_reflection}
+end
+
+
 (* main simprocs *)
 
 val prep_thms = map mk_meta_eq [@{thm Bex_def}, @{thm Pow_iff[symmetric]}]
@@ -304,7 +341,7 @@
 fun conv ctxt t =
   let
     val ct = cterm_of (Proof_Context.theory_of ctxt) t
-    val prep_eq = Raw_Simplifier.rewrite true prep_thms ct 
+    val prep_eq = (comprehension_conv ctxt then_conv 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)