fine-tuned elimination of comprehensions involving x=t.

--- a/src/HOL/Bali/Example.thy	Mon May 18 09:48:06 2009 +0200
+++ b/src/HOL/Bali/Example.thy	Mon May 18 23:15:38 2009 +0200
@@ -1075,7 +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])}"
-by (simp (no_asm) add: max_spec_def appl_methds_Base_foo)
+by (simp add: max_spec_def appl_methds_Base_foo Collect_conv_if)
 
 section "well-typedness"
 

--- a/src/HOL/Library/Pocklington.thy	Mon May 18 09:48:06 2009 +0200
+++ b/src/HOL/Library/Pocklington.thy	Mon May 18 23:15:38 2009 +0200
@@ -382,8 +382,9 @@
 (* Euler totient function.                                                   *)
 
 definition phi_def: "\<phi> n = card { m. 0 < m \<and> m <= n \<and> coprime m n }"
+
 lemma phi_0[simp]: "\<phi> 0 = 0"
-  unfolding phi_def by (auto simp add: card_eq_0_iff)
+  unfolding phi_def by auto
 
 lemma phi_finite[simp]: "finite ({ m. 0 < m \<and> m <= n \<and> coprime m n })"
 proof-

--- a/src/HOL/MicroJava/BV/BVExample.thy	Mon May 18 09:48:06 2009 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon May 18 23:15:38 2009 +0200
@@ -69,9 +69,9 @@
 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 del:singleton_conj_conv2)
+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)
+apply (auto simp: expand_fun_eq)
 done
 
 text {* The subclass relation is acyclic; hence its converse is well founded: *}

--- a/src/HOL/Set.thy	Mon May 18 09:48:06 2009 +0200
+++ b/src/HOL/Set.thy	Mon May 18 23:15:38 2009 +0200
@@ -1036,11 +1036,16 @@
 
 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 {})"
+lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})"
+by auto
+
+lemma Collect_conv_if2: "{x. a=x & 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
+text {*
+Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
+to the front (and similarly for @{text "t=x"}):
+*}
 
 ML{*
   local
@@ -1054,7 +1059,6 @@
   end;
 
   Addsimprocs [defColl_regroup];
-
 *}
 
 text {*

--- a/src/Provers/quantifier1.ML	Mon May 18 09:48:06 2009 +0200
+++ b/src/Provers/quantifier1.ML	Mon May 18 23:15:38 2009 +0200
@@ -90,7 +90,7 @@
 
 fun extract_conj fst xs t = case dest_conj t of NONE => NONE
     | SOME(conj,P,Q) =>
-        (if not fst andalso def xs P then SOME(xs,P,Q) else
+        (if def xs P then (if fst then NONE else SOME(xs,P,Q)) else
          if def xs Q then SOME(xs,Q,P) else
          (case extract_conj false xs P of
             SOME(xs,eq,P') => SOME(xs,eq, conj $ P' $ Q)
@@ -99,7 +99,7 @@
                      | NONE => NONE)));
 
 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)
+    | SOME(imp,P,Q) => if def xs P then (if fst then NONE else 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 false xs Q of