equal
deleted
inserted
replaced
127 by (fast_tac (claset() addEs [inj_onD, sym RS f_eq_gE]) 1); |
127 by (fast_tac (claset() addEs [inj_onD, sym RS f_eq_gE]) 1); |
128 by (stac split_if 1); |
128 by (stac split_if 1); |
129 by (fast_tac (claset() addEs [inj_onD, f_eq_gE]) 1); |
129 by (fast_tac (claset() addEs [inj_onD, f_eq_gE]) 1); |
130 qed "bij_if_then_else"; |
130 qed "bij_if_then_else"; |
131 |
131 |
132 Goal "!!f:: 'a=>'b. ? X. X = - (g``(- f``X))"; |
132 Goal "? X. X = - (g``(- (f``X)))"; |
133 by (rtac exI 1); |
133 by (rtac exI 1); |
134 by (rtac lfp_Tarski 1); |
134 by (rtac lfp_Tarski 1); |
135 by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1)); |
135 by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1)); |
136 qed "decomposition"; |
136 qed "decomposition"; |
137 |
137 |