equal
deleted
inserted
replaced
159 qed "surj_range"; |
159 qed "surj_range"; |
160 |
160 |
161 Goalw [surj_def] "surj f ==> EX x. y = f x"; |
161 Goalw [surj_def] "surj f ==> EX x. y = f x"; |
162 by (Blast_tac 1); |
162 by (Blast_tac 1); |
163 qed "surjD"; |
163 qed "surjD"; |
|
164 |
|
165 val [p1, p2] = Goal "surj f ==> (!!x. y = f x ==> C) ==> C"; |
|
166 by (cut_facts_tac [p1 RS surjD] 1); |
|
167 by (etac exE 1); |
|
168 by (rtac p2 1); |
|
169 by (atac 1); |
|
170 qed "surjE"; |
164 |
171 |
165 Goalw [o_def, surj_def] "[| surj f; surj g |] ==> surj (g o f)"; |
172 Goalw [o_def, surj_def] "[| surj f; surj g |] ==> surj (g o f)"; |
166 by (Clarify_tac 1); |
173 by (Clarify_tac 1); |
167 by (dres_inst_tac [("x","y")] spec 1); |
174 by (dres_inst_tac [("x","y")] spec 1); |
168 by (Clarify_tac 1); |
175 by (Clarify_tac 1); |