"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
by the new simproc defColl_regroup. More precisely, the simproc pulls an
equation x=t (or t=x) out of a nest of conjunctions to the front where the
simp rule singleton_conj_conv(2) converts to "if".

--- a/src/HOL/Bali/Example.thy	Fri May 15 10:01:57 2009 +0200
+++ b/src/HOL/Bali/Example.thy	Sat May 16 11:28:02 2009 +0200
@@ -1075,10 +1075,7 @@
 lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \<lparr>name=foo,parTs=[NT]\<rparr> = 
   {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
    , [Class Base])}"
-apply (unfold max_spec_def)
-apply (simp (no_asm) add: appl_methds_Base_foo)
-apply auto
-done
+by (simp (no_asm) add: max_spec_def appl_methds_Base_foo)
 
 section "well-typedness"
 

--- a/src/HOL/HOL.thy	Fri May 15 10:01:57 2009 +0200
+++ b/src/HOL/HOL.thy	Sat May 16 11:28:02 2009 +0200
@@ -1050,8 +1050,7 @@
     "(P | False) = P"  "(False | P) = P"
     "(P | P) = P"  "(P | (P | Q)) = (P | Q)" and
     "(ALL x. P) = P"  "(EX x. P) = P"  "EX x. x=t"  "EX x. t=x"
-    -- {* needed for the one-point-rule quantifier simplification procs *}
-    -- {* essential for termination!! *} and
+  and
     "!!P. (EX x. x=t & P(x)) = P(t)"
     "!!P. (EX x. t=x & P(x)) = P(t)"
     "!!P. (ALL x. x=t --> P(x)) = P(t)"

--- a/src/HOL/Library/Binomial.thy	Fri May 15 10:01:57 2009 +0200
+++ b/src/HOL/Library/Binomial.thy	Sat May 16 11:28:02 2009 +0200
@@ -88,9 +88,7 @@
 
 lemma card_s_0_eq_empty:
     "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
-  apply (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
-  apply (simp cong add: rev_conj_cong)
-  done
+by (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
 
 lemma choose_deconstruct: "finite M ==> x \<notin> M
   ==> {s. s <= insert x M & card(s) = Suc k}

--- a/src/HOL/MicroJava/BV/BVExample.thy	Fri May 15 10:01:57 2009 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Sat May 16 11:28:02 2009 +0200
@@ -69,10 +69,11 @@
 lemma subcls1:
   "subcls1 E = (\<lambda>C D. (C, D) \<in> {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
                 (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)})"
-  apply (simp add: subcls1_def2)
-  apply (simp add: name_defs class_defs system_defs E_def class_def)
-  apply (auto simp: expand_fun_eq split: split_if_asm)
-  done
+apply (simp add: subcls1_def2)
+apply (simp add: name_defs class_defs system_defs E_def class_def)
+apply (auto simp: expand_fun_eq name_defs[symmetric] class_defs split:split_if_asm)
+apply(simp add:name_defs)+
+done
 
 text {* The subclass relation is acyclic; hence its converse is well founded: *}
 lemma notin_rtrancl:

--- a/src/HOL/NanoJava/TypeRel.thy	Fri May 15 10:01:57 2009 +0200
+++ b/src/HOL/NanoJava/TypeRel.thy	Sat May 16 11:28:02 2009 +0200
@@ -56,7 +56,7 @@
   "subcls1 = 
     (SIGMA C: {C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})"
 apply (unfold subcls1_def is_class_def)
-apply auto
+apply (auto split:split_if_asm)
 done
 
 lemma finite_subcls1: "finite subcls1"

--- a/src/HOL/Set.thy	Fri May 15 10:01:57 2009 +0200
+++ b/src/HOL/Set.thy	Sat May 16 11:28:02 2009 +0200
@@ -1034,6 +1034,29 @@
 
 subsubsection {* Set reasoning tools *}
 
+text{* Elimination of @{text"{x. \<dots> & x=t & \<dots>}"}. *}
+
+lemma singleton_conj_conv[simp]: "{x. x=a & P x} = (if P a then {a} else {})"
+by auto
+
+lemma singleton_conj_conv2[simp]: "{x. a=x & P x} = (if P a then {a} else {})"
+by auto
+
+ML{*
+  local
+    val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN
+    ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}),
+                    DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])])
+  in
+    val defColl_regroup = Simplifier.simproc (the_context ())
+      "defined Collect" ["{x. P x & Q x}"]
+      (Quantifier1.rearrange_Coll Coll_perm_tac)
+  end;
+
+  Addsimprocs [defColl_regroup];
+
+*}
+
 text {*
   Rewrite rules for boolean case-splitting: faster than @{text
   "split_if [split]"}.

--- a/src/Provers/quantifier1.ML	Fri May 15 10:01:57 2009 +0200
+++ b/src/Provers/quantifier1.ML	Sat May 16 11:28:02 2009 +0200
@@ -21,11 +21,21 @@
         "!x. x=t --> P(x)" is covered by the congreunce rule for -->;
         "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
         As must be "? x. t=x & P(x)".
-
         
      And similarly for the bounded quantifiers.
 
 Gries etc call this the "1 point rules"
+
+The above also works for !x1..xn. and ?x1..xn by moving the defined
+qunatifier inside first, but not for nested bounded quantifiers.
+
+For set comprehensions the basic permutations
+      ... & x = t & ...  ->  x = t & (... & ...)
+      ... & t = x & ...  ->  t = x & (... & ...)
+are also exported.
+
+To avoid looping, NONE is returned if the term cannot be rearranged,
+esp if x=t/t=x sits at the front already.
 *)
 
 signature QUANTIFIER1_DATA =
@@ -61,6 +71,7 @@
   val rearrange_ex:  theory -> simpset -> term -> thm option
   val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option
   val rearrange_bex:  (simpset -> tactic) -> theory -> simpset -> term -> thm option
+  val rearrange_Coll: tactic -> theory -> simpset -> term -> thm option
 end;
 
 functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
@@ -70,29 +81,28 @@
 
 (* FIXME: only test! *)
 fun def xs eq =
-  let val n = length xs
-  in case dest_eq eq of
-      SOME(c,s,t) =>
-        s = Bound n andalso not(loose_bvar1(t,n)) orelse
-        t = Bound n andalso not(loose_bvar1(s,n))
-    | NONE => false
-  end;
+  (case dest_eq eq of
+     SOME(c,s,t) =>
+       let val n = length xs
+       in s = Bound n andalso not(loose_bvar1(t,n)) orelse
+          t = Bound n andalso not(loose_bvar1(s,n)) end
+   | NONE => false);
 
-fun extract_conj xs t = case dest_conj t of NONE => NONE
+fun extract_conj fst xs t = case dest_conj t of NONE => NONE
     | SOME(conj,P,Q) =>
-        (if def xs P then SOME(xs,P,Q) else
+        (if not fst andalso def xs P then SOME(xs,P,Q) else
          if def xs Q then SOME(xs,Q,P) else
-         (case extract_conj xs P of
+         (case extract_conj false xs P of
             SOME(xs,eq,P') => SOME(xs,eq, conj $ P' $ Q)
-          | NONE => (case extract_conj xs Q of
+          | NONE => (case extract_conj false xs Q of
                        SOME(xs,eq,Q') => SOME(xs,eq,conj $ P $ Q')
                      | NONE => NONE)));
 
-fun extract_imp xs t = case dest_imp t of NONE => NONE
-    | SOME(imp,P,Q) => if def xs P then SOME(xs,P,Q)
-                       else (case extract_conj xs P of
+fun extract_imp fst xs t = case dest_imp t of NONE => NONE
+    | SOME(imp,P,Q) => if not fst andalso def xs P then SOME(xs,P,Q)
+                       else (case extract_conj false xs P of
                                SOME(xs,eq,P') => SOME(xs, eq, imp $ P' $ Q)
-                             | NONE => (case extract_imp xs Q of
+                             | NONE => (case extract_imp false xs Q of
                                           NONE => NONE
                                         | SOME(xs,eq,Q') =>
                                             SOME(xs,eq,imp$P$Q')));
@@ -100,8 +110,8 @@
 fun extract_quant extract q =
   let fun exqu xs ((qC as Const(qa,_)) $ Abs(x,T,Q)) =
             if qa = q then exqu ((qC,x,T)::xs) Q else NONE
-        | exqu xs P = extract xs P
-  in exqu end;
+        | exqu xs P = extract (null xs) xs P
+  in exqu [] end;
 
 fun prove_conv tac thy tu =
   Goal.prove (ProofContext.init thy) [] [] (Logic.mk_equals tu)
@@ -147,7 +157,7 @@
   in quant xs (qC $ Abs(x,T,Q)) end;
 
 fun rearrange_all thy _ (F as (all as Const(q,_)) $ Abs(x,T, P)) =
-     (case extract_quant extract_imp q [] P of
+     (case extract_quant extract_imp q P of
         NONE => NONE
       | SOME(xs,eq,Q) =>
           let val R = quantify all x T xs (imp $ eq $ Q)
@@ -155,7 +165,7 @@
   | rearrange_all _ _ _ = NONE;
 
 fun rearrange_ball tac thy ss (F as Ball $ A $ Abs(x,T,P)) =
-     (case extract_imp [] P of
+     (case extract_imp true [] P of
         NONE => NONE
       | SOME(xs,eq,Q) => if not(null xs) then NONE else
           let val R = imp $ eq $ Q
@@ -163,7 +173,7 @@
   | rearrange_ball _ _ _ _ = NONE;
 
 fun rearrange_ex thy _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
-     (case extract_quant extract_conj q [] P of
+     (case extract_quant extract_conj q P of
         NONE => NONE
       | SOME(xs,eq,Q) =>
           let val R = quantify ex x T xs (conj $ eq $ Q)
@@ -171,10 +181,17 @@
   | rearrange_ex _ _ _ = NONE;
 
 fun rearrange_bex tac thy ss (F as Bex $ A $ Abs(x,T,P)) =
-     (case extract_conj [] P of
+     (case extract_conj true [] P of
         NONE => NONE
       | SOME(xs,eq,Q) => if not(null xs) then NONE else
           SOME(prove_conv (tac ss) thy (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
   | rearrange_bex _ _ _ _ = NONE;
 
+fun rearrange_Coll tac thy _ (F as Coll $ Abs(x,T,P)) =
+     (case extract_conj true [] P of
+        NONE => NONE
+      | SOME(_,eq,Q) =>
+          let val R = Coll $ Abs(x,T, conj $ eq $ Q)
+          in SOME(prove_conv tac thy (F,R)) end);
+
 end;