31 "[| f: A->B; !!y. y:B ==> d(y): A; !!y. y:B ==> f`d(y) = y \ |
31 "[| f: A->B; !!y. y:B ==> d(y): A; !!y. y:B ==> f`d(y) = y \ |
32 \ |] ==> f: surj(A,B)"; |
32 \ |] ==> f: surj(A,B)"; |
33 by (blast_tac (claset() addIs prems) 1); |
33 by (blast_tac (claset() addIs prems) 1); |
34 qed "f_imp_surjective"; |
34 qed "f_imp_surjective"; |
35 |
35 |
36 val prems = goal Perm.thy |
36 val prems = Goal |
37 "[| !!x. x:A ==> c(x): B; \ |
37 "[| !!x. x:A ==> c(x): B; \ |
38 \ !!y. y:B ==> d(y): A; \ |
38 \ !!y. y:B ==> d(y): A; \ |
39 \ !!y. y:B ==> c(d(y)) = y \ |
39 \ !!y. y:B ==> c(d(y)) = y \ |
40 \ |] ==> (lam x:A. c(x)) : surj(A,B)"; |
40 \ |] ==> (lam x:A. c(x)) : surj(A,B)"; |
41 by (res_inst_tac [("d", "d")] f_imp_surjective 1); |
41 by (res_inst_tac [("d", "d")] f_imp_surjective 1); |
72 Goal "[| f: A->B; ALL x:A. d(f`x)=x |] ==> f: inj(A,B)"; |
72 Goal "[| f: A->B; ALL x:A. d(f`x)=x |] ==> f: inj(A,B)"; |
73 by (asm_simp_tac (simpset() addsimps [inj_def]) 1); |
73 by (asm_simp_tac (simpset() addsimps [inj_def]) 1); |
74 by (deepen_tac (claset() addEs [subst_context RS box_equals]) 0 1); |
74 by (deepen_tac (claset() addEs [subst_context RS box_equals]) 0 1); |
75 bind_thm ("f_imp_injective", ballI RSN (2,result())); |
75 bind_thm ("f_imp_injective", ballI RSN (2,result())); |
76 |
76 |
77 val prems = goal Perm.thy |
77 val prems = Goal |
78 "[| !!x. x:A ==> c(x): B; \ |
78 "[| !!x. x:A ==> c(x): B; \ |
79 \ !!x. x:A ==> d(c(x)) = x \ |
79 \ !!x. x:A ==> d(c(x)) = x \ |
80 \ |] ==> (lam x:A. c(x)) : inj(A,B)"; |
80 \ |] ==> (lam x:A. c(x)) : inj(A,B)"; |
81 by (res_inst_tac [("d", "d")] f_imp_injective 1); |
81 by (res_inst_tac [("d", "d")] f_imp_injective 1); |
82 by (ALLGOALS (asm_simp_tac (simpset() addsimps ([lam_type]@prems)) )); |
82 by (ALLGOALS (asm_simp_tac (simpset() addsimps ([lam_type]@prems)) )); |
183 inj_is_fun]) 1); |
183 inj_is_fun]) 1); |
184 qed "left_inverse"; |
184 qed "left_inverse"; |
185 |
185 |
186 val left_inverse_bij = bij_is_inj RS left_inverse; |
186 val left_inverse_bij = bij_is_inj RS left_inverse; |
187 |
187 |
188 val prems = goal Perm.thy |
188 Goal "[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b"; |
189 "[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b"; |
|
190 by (rtac (apply_Pair RS (converseD RS apply_equality)) 1); |
189 by (rtac (apply_Pair RS (converseD RS apply_equality)) 1); |
191 by (REPEAT (resolve_tac prems 1)); |
190 by (REPEAT (assume_tac 1)); |
192 qed "right_inverse_lemma"; |
191 qed "right_inverse_lemma"; |
193 |
192 |
194 (*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse? |
193 (*Should the premises be f:surj(A,B), b:B for symmetry with left_inverse? |
195 No: they would not imply that converse(f) was a function! *) |
194 No: they would not imply that converse(f) was a function! *) |
196 Goal "[| f: inj(A,B); b: range(f) |] ==> f`(converse(f)`b) = b"; |
195 Goal "[| f: inj(A,B); b: range(f) |] ==> f`(converse(f)`b) = b"; |
335 qed "comp_fun_apply"; |
334 qed "comp_fun_apply"; |
336 |
335 |
337 Addsimps [comp_fun_apply]; |
336 Addsimps [comp_fun_apply]; |
338 |
337 |
339 (*Simplifies compositions of lambda-abstractions*) |
338 (*Simplifies compositions of lambda-abstractions*) |
340 val [prem] = goal Perm.thy |
339 val [prem] = Goal |
341 "[| !!x. x:A ==> b(x): B \ |
340 "[| !!x. x:A ==> b(x): B \ |
342 \ |] ==> (lam y:B. c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))"; |
341 \ |] ==> (lam y:B. c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))"; |
343 by (rtac fun_extension 1); |
342 by (rtac fun_extension 1); |
344 by (rtac comp_fun 1); |
343 by (rtac comp_fun 1); |
345 by (rtac lam_funtype 2); |
344 by (rtac lam_funtype 2); |
511 by (safe_tac (claset() addSEs [restrict_type2])); |
510 by (safe_tac (claset() addSEs [restrict_type2])); |
512 by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp, subsetD, |
511 by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp, subsetD, |
513 box_equals, restrict] 1)); |
512 box_equals, restrict] 1)); |
514 qed "restrict_inj"; |
513 qed "restrict_inj"; |
515 |
514 |
516 val prems = goal Perm.thy |
515 Goal "[| f: Pi(A,B); C<=A |] ==> restrict(f,C): surj(C, f``C)"; |
517 "[| f: Pi(A,B); C<=A |] ==> restrict(f,C): surj(C, f``C)"; |
|
518 by (rtac (restrict_image RS subst) 1); |
516 by (rtac (restrict_image RS subst) 1); |
519 by (rtac (restrict_type2 RS surj_image) 3); |
517 by (rtac (restrict_type2 RS surj_image) 3); |
520 by (REPEAT (resolve_tac prems 1)); |
518 by (REPEAT (assume_tac 1)); |
521 qed "restrict_surj"; |
519 qed "restrict_surj"; |
522 |
520 |
523 Goalw [inj_def,bij_def] |
521 Goalw [inj_def,bij_def] |
524 "[| f: inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C)"; |
522 "[| f: inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C)"; |
525 by (blast_tac (claset() addSIs [restrict, restrict_surj] |
523 by (blast_tac (claset() addSIs [restrict, restrict_surj] |