--- 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,