# HG changeset patch
# User oheimb
# Date 833562720 -7200
# Node ID d7e77cb8ce5c2fe369dfbfd5f40aeca61ad416c3
# Parent  3f5382e95e1e83465575a65b7e2fe25a2cda339c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
as there have been unnecessary proofs of anonymous thms, which could not be
removed (by name) from the !simpset where necessary. All these thms except
singleton_iff were already proved in Set.ML.
therefore in Set.ML: New version of singletonE, proof of new thm singleton_iff

diff -r 3f5382e95e1e -r d7e77cb8ce5c src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Thu May 30 13:31:29 1996 +0200
+++ b/src/HOL/Fun.ML	Fri May 31 19:12:00 1996 +0200
@@ -190,20 +190,3 @@
             subsetD, subsetCE];
 
 fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac set_cs;
-
-
-fun prover s = prove_goal Fun.thy s (fn _=>[fast_tac set_cs 1]);
-
-val mem_simps = map prover
- [ "(a : A Un B)   =  (a:A | a:B)",	(* Un_iff *)
-   "(a : A Int B)  =  (a:A & a:B)",	(* Int_iff *)
-   "(a : Compl(B)) =  (~a:B)",		(* Compl_iff *)
-   "(a : A-B)      =  (a:A & ~a:B)",	(* Diff_iff *)
-   "(a : {b})      =  (a=b)",
-   "(a : {x.P(x)}) =  P(a)" ];
-
-val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
-
-simpset := !simpset addsimps mem_simps
-                    addcongs [ball_cong,bex_cong]
-                    setmksimps (mksimps mksimps_pairs);
diff -r 3f5382e95e1e -r d7e77cb8ce5c src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu May 30 13:31:29 1996 +0200
+++ b/src/HOL/Set.ML	Fri May 31 19:12:00 1996 +0200
@@ -319,16 +319,17 @@
 qed_goal "singletonI" Set.thy "a : {a}"
  (fn _=> [ (rtac insertI1 1) ]);
 
-qed_goal "singletonE" Set.thy "[| a: {b};  a=b ==> P |] ==> P"
- (fn major::prems=>
-  [ (rtac (major RS insertE) 1),
-    (REPEAT (eresolve_tac (prems @ [emptyE]) 1)) ]);
-
 goalw Set.thy [insert_def] "!!a. b : {a} ==> b=a";
 by (fast_tac (!claset addSEs [emptyE,CollectE,UnE]) 1);
 qed "singletonD";
 
-val singletonE = make_elim singletonD;
+bind_thm ("singletonE", make_elim singletonD);
+
+qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" (fn _ => [
+	rtac iffI 1,
+	etac singletonD 1,
+	hyp_subst_tac 1,
+	rtac singletonI 1]);
 
 val [major] = goal Set.thy "{a}={b} ==> a=b";
 by (rtac (major RS equalityD1 RS subsetD RS singletonD) 1);
@@ -467,3 +468,17 @@
 
 val Pow_bottom = empty_subsetI RS PowI;        (* {}: Pow(B) *)
 val Pow_top = subset_refl RS PowI;             (* A : Pow(A) *)
+
+
+
+(*** Set reasoning tools ***)
+
+
+val mem_simps = [ Un_iff, Int_iff, Compl_iff, Diff_iff, singleton_iff,
+		  mem_Collect_eq];
+
+val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
+
+simpset := !simpset addsimps mem_simps
+                    addcongs [ball_cong,bex_cong]
+                    setmksimps (mksimps mksimps_pairs);