# HG changeset patch
# User paulson
# Date 918232302 -3600
# Node ID 958f4fc3e8b8bc54d219bb6d6b50f8c867978e70
# Parent  c8a69ecafb99000a200e204feef53562e8e9c0fb
tidied Schroeder-Bernstein proof

diff -r c8a69ecafb99 -r 958f4fc3e8b8 src/HOL/ex/set.ML
--- a/src/HOL/ex/set.ML	Fri Feb 05 17:31:04 1999 +0100
+++ b/src/HOL/ex/set.ML	Fri Feb 05 17:31:42 1999 +0100
@@ -72,44 +72,16 @@
 choplev 0;
 by (best_tac (claset() addSEs [equalityCE]) 1);
 
+
 (*** The Schroder-Berstein Theorem ***)
 
-Goalw [image_def] "inj(f) ==> inv(f)``(f``X) = X";
-by (rtac equalityI 1);
-by (fast_tac (claset() addEs [inv_f_f RS ssubst]) 1);
-by (fast_tac (claset() addEs [inv_f_f RS ssubst]) 1);
-qed "inv_image_comp";
-
-Goal "f(a) ~: (f``X) ==> a~:X";
-by (Blast_tac 1);
-qed "contra_imageI";
-
-Goal "(a ~: -(X)) = (a:X)";
-by (Blast_tac 1);
-qed "not_Compl";
-
-(*Lots of backtracking in this proof...*)
-val [compl,fg,Xa] = goal Lfp.thy
-    "[| -(f``X) = g``(-X);  f(a)=g(b);  a:X |] ==> b:X";
-by (EVERY1 [rtac (not_Compl RS subst), rtac contra_imageI,
-            rtac (compl RS subst), rtac (fg RS subst), stac not_Compl,
-            rtac imageI, rtac Xa]);
+Goal "[| -(f``X) = g``(-X);  f(a)=g(b);  a:X |] ==> b:X";
+by (blast_tac (claset() addEs [equalityE]) 1);
 qed "disj_lemma";
 
-Goalw [image_def]
-     "range(%z. if z:X then f(z) else g(z)) = f``X Un g``(-X)";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "range_if_then_else";
-
-Goalw [surj_def] "surj(f) = (!a. a : range(f))";
-by (fast_tac (claset() addEs [ssubst]) 1);
-qed "surj_iff_full_range";
-
 Goal "-(f``X) = g``(-X) ==> surj(%z. if z:X then f(z) else g(z))";
-by (EVERY1[stac surj_iff_full_range, stac range_if_then_else,
-           etac subst]);
-by (Blast_tac 1);
+by (asm_simp_tac (simpset() addsimps [surj_def]) 1);
+by (blast_tac (claset() addEs [equalityE]) 1);
 qed "surj_if_then_else";
 
 Goalw [inj_on_def]
@@ -134,8 +106,9 @@
 by (rtac exI 1);
 by (rtac bij_if_then_else 1);
 by (rtac refl 4);
-by (EVERY [rtac ([subset_UNIV,injf] MRS subset_inj_on) 1,
-           rtac (injg RS inj_on_inv) 1]);
+by (rtac inj_on_inv 2);
+by (rtac ([subset_UNIV, injf] MRS subset_inj_on) 1);
+  (**tricky variable instantiations!**)
 by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI,
             etac imageE, etac ssubst, rtac rangeI]);
 by (EVERY1 [etac ssubst, stac double_complement,