110 by (EVERY1[stac surj_iff_full_range, stac range_if_then_else, |
110 by (EVERY1[stac surj_iff_full_range, stac range_if_then_else, |
111 etac subst]); |
111 etac subst]); |
112 by (Blast_tac 1); |
112 by (Blast_tac 1); |
113 qed "surj_if_then_else"; |
113 qed "surj_if_then_else"; |
114 |
114 |
115 val [injf,injg,compl,bij] = |
115 Goalw [inj_on_def] |
116 goal Lfp.thy |
116 "[| inj_on f X; inj_on g (-X); -(f``X) = g``(-X); \ |
117 "[| inj_on f X; inj_on g (-X); -(f``X) = g``(-X); \ |
117 \ bij = (%z. if z:X then f(z) else g(z)) |] \ |
118 \ bij = (%z. if z:X then f(z) else g(z)) |] ==> \ |
118 \ ==> inj(bij) & surj(bij)"; |
119 \ inj(bij) & surj(bij)"; |
119 by (asm_simp_tac (simpset() addsimps [surj_if_then_else]) 1); |
120 val f_eq_gE = make_elim (compl RS disj_lemma); |
120 (*PROOF FAILED if inj_onD*) |
121 by (stac bij 1); |
121 by (blast_tac (claset() addDs [disj_lemma, sym RSN (2,disj_lemma)]) 1); |
122 by (rtac conjI 1); |
|
123 by (rtac (compl RS surj_if_then_else) 2); |
|
124 by (rewtac inj_def); |
|
125 by (cut_facts_tac [injf,injg] 1); |
|
126 by (EVERY1 [rtac allI, rtac allI, stac split_if, rtac conjI, stac split_if]); |
|
127 by (fast_tac (claset() addEs [inj_onD, sym RS f_eq_gE]) 1); |
|
128 by (stac split_if 1); |
|
129 by (fast_tac (claset() addEs [inj_onD, f_eq_gE]) 1); |
|
130 qed "bij_if_then_else"; |
122 qed "bij_if_then_else"; |
131 |
123 |
132 Goal "? X. X = - (g``(- (f``X)))"; |
124 Goal "? X. X = - (g``(- (f``X)))"; |
133 by (rtac exI 1); |
125 by (rtac exI 1); |
134 by (rtac lfp_Tarski 1); |
126 by (rtac lfp_Tarski 1); |
135 by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1)); |
127 by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1)); |
136 qed "decomposition"; |
128 qed "decomposition"; |
137 |
129 |
138 val [injf,injg] = goal Lfp.thy |
130 val [injf,injg] = goal Lfp.thy |
139 "[| inj(f:: 'a=>'b); inj(g:: 'b=>'a) |] ==> \ |
131 "[| inj (f:: 'a=>'b); inj (g:: 'b=>'a) |] ==> \ |
140 \ ? h:: 'a=>'b. inj(h) & surj(h)"; |
132 \ ? h:: 'a=>'b. inj(h) & surj(h)"; |
141 by (rtac (decomposition RS exE) 1); |
133 by (rtac (decomposition RS exE) 1); |
142 by (rtac exI 1); |
134 by (rtac exI 1); |
143 by (rtac bij_if_then_else 1); |
135 by (rtac bij_if_then_else 1); |
144 by (EVERY [rtac refl 4, rtac (injf RS inj_imp) 1, |
136 by (rtac refl 4); |
|
137 by (EVERY [rtac ([subset_UNIV,injf] MRS subset_inj_on) 1, |
145 rtac (injg RS inj_on_inv) 1]); |
138 rtac (injg RS inj_on_inv) 1]); |
146 by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI, |
139 by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI, |
147 etac imageE, etac ssubst, rtac rangeI]); |
140 etac imageE, etac ssubst, rtac rangeI]); |
148 by (EVERY1 [etac ssubst, stac double_complement, |
141 by (EVERY1 [etac ssubst, stac double_complement, |
149 rtac (injg RS inv_image_comp RS sym)]); |
142 rtac (injg RS inv_image_comp RS sym)]); |