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