70 by (assume_tac 1); |
70 by (assume_tac 1); |
71 |
71 |
72 choplev 0; |
72 choplev 0; |
73 by (best_tac (claset() addSEs [equalityCE]) 1); |
73 by (best_tac (claset() addSEs [equalityCE]) 1); |
74 |
74 |
|
75 |
75 (*** The Schroder-Berstein Theorem ***) |
76 (*** The Schroder-Berstein Theorem ***) |
76 |
77 |
77 Goalw [image_def] "inj(f) ==> inv(f)``(f``X) = X"; |
78 Goal "[| -(f``X) = g``(-X); f(a)=g(b); a:X |] ==> b:X"; |
78 by (rtac equalityI 1); |
79 by (blast_tac (claset() addEs [equalityE]) 1); |
79 by (fast_tac (claset() addEs [inv_f_f RS ssubst]) 1); |
|
80 by (fast_tac (claset() addEs [inv_f_f RS ssubst]) 1); |
|
81 qed "inv_image_comp"; |
|
82 |
|
83 Goal "f(a) ~: (f``X) ==> a~:X"; |
|
84 by (Blast_tac 1); |
|
85 qed "contra_imageI"; |
|
86 |
|
87 Goal "(a ~: -(X)) = (a:X)"; |
|
88 by (Blast_tac 1); |
|
89 qed "not_Compl"; |
|
90 |
|
91 (*Lots of backtracking in this proof...*) |
|
92 val [compl,fg,Xa] = goal Lfp.thy |
|
93 "[| -(f``X) = g``(-X); f(a)=g(b); a:X |] ==> b:X"; |
|
94 by (EVERY1 [rtac (not_Compl RS subst), rtac contra_imageI, |
|
95 rtac (compl RS subst), rtac (fg RS subst), stac not_Compl, |
|
96 rtac imageI, rtac Xa]); |
|
97 qed "disj_lemma"; |
80 qed "disj_lemma"; |
98 |
81 |
99 Goalw [image_def] |
|
100 "range(%z. if z:X then f(z) else g(z)) = f``X Un g``(-X)"; |
|
101 by (Simp_tac 1); |
|
102 by (Blast_tac 1); |
|
103 qed "range_if_then_else"; |
|
104 |
|
105 Goalw [surj_def] "surj(f) = (!a. a : range(f))"; |
|
106 by (fast_tac (claset() addEs [ssubst]) 1); |
|
107 qed "surj_iff_full_range"; |
|
108 |
|
109 Goal "-(f``X) = g``(-X) ==> surj(%z. if z:X then f(z) else g(z))"; |
82 Goal "-(f``X) = g``(-X) ==> surj(%z. if z:X then f(z) else g(z))"; |
110 by (EVERY1[stac surj_iff_full_range, stac range_if_then_else, |
83 by (asm_simp_tac (simpset() addsimps [surj_def]) 1); |
111 etac subst]); |
84 by (blast_tac (claset() addEs [equalityE]) 1); |
112 by (Blast_tac 1); |
|
113 qed "surj_if_then_else"; |
85 qed "surj_if_then_else"; |
114 |
86 |
115 Goalw [inj_on_def] |
87 Goalw [inj_on_def] |
116 "[| inj_on f X; inj_on g (-X); -(f``X) = g``(-X); \ |
88 "[| inj_on f X; inj_on g (-X); -(f``X) = g``(-X); \ |
117 \ bij = (%z. if z:X then f(z) else g(z)) |] \ |
89 \ bij = (%z. if z:X then f(z) else g(z)) |] \ |
132 \ ? h:: 'a=>'b. inj(h) & surj(h)"; |
104 \ ? h:: 'a=>'b. inj(h) & surj(h)"; |
133 by (rtac (decomposition RS exE) 1); |
105 by (rtac (decomposition RS exE) 1); |
134 by (rtac exI 1); |
106 by (rtac exI 1); |
135 by (rtac bij_if_then_else 1); |
107 by (rtac bij_if_then_else 1); |
136 by (rtac refl 4); |
108 by (rtac refl 4); |
137 by (EVERY [rtac ([subset_UNIV,injf] MRS subset_inj_on) 1, |
109 by (rtac inj_on_inv 2); |
138 rtac (injg RS inj_on_inv) 1]); |
110 by (rtac ([subset_UNIV, injf] MRS subset_inj_on) 1); |
|
111 (**tricky variable instantiations!**) |
139 by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI, |
112 by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI, |
140 etac imageE, etac ssubst, rtac rangeI]); |
113 etac imageE, etac ssubst, rtac rangeI]); |
141 by (EVERY1 [etac ssubst, stac double_complement, |
114 by (EVERY1 [etac ssubst, stac double_complement, |
142 rtac (injg RS inv_image_comp RS sym)]); |
115 rtac (injg RS inv_image_comp RS sym)]); |
143 qed "schroeder_bernstein"; |
116 qed "schroeder_bernstein"; |