equal
deleted
inserted
replaced
21 |
21 |
22 (*** inj(f): f is a one-to-one function ***) |
22 (*** inj(f): f is a one-to-one function ***) |
23 |
23 |
24 val prems = goalw Fun.thy [inj_def] |
24 val prems = goalw Fun.thy [inj_def] |
25 "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)"; |
25 "[| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)"; |
26 by (fast_tac (!claset addIs prems) 1); |
26 by (blast_tac (!claset addIs prems) 1); |
27 qed "injI"; |
27 qed "injI"; |
28 |
28 |
29 val [major] = goal Fun.thy "(!!x. g(f(x)) = x) ==> inj(f)"; |
29 val [major] = goal Fun.thy "(!!x. g(f(x)) = x) ==> inj(f)"; |
30 by (rtac injI 1); |
30 by (rtac injI 1); |
31 by (etac (arg_cong RS box_equals) 1); |
31 by (etac (arg_cong RS box_equals) 1); |
67 |
67 |
68 (*** inj_onto f A: f is one-to-one over A ***) |
68 (*** inj_onto f A: f is one-to-one over A ***) |
69 |
69 |
70 val prems = goalw Fun.thy [inj_onto_def] |
70 val prems = goalw Fun.thy [inj_onto_def] |
71 "(!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_onto f A"; |
71 "(!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_onto f A"; |
72 by (fast_tac (!claset addIs prems) 1); |
72 by (blast_tac (!claset addIs prems) 1); |
73 qed "inj_ontoI"; |
73 qed "inj_ontoI"; |
74 |
74 |
75 val [major] = goal Fun.thy |
75 val [major] = goal Fun.thy |
76 "(!!x. x:A ==> g(f(x)) = x) ==> inj_onto f A"; |
76 "(!!x. x:A ==> g(f(x)) = x) ==> inj_onto f A"; |
77 by (rtac inj_ontoI 1); |
77 by (rtac inj_ontoI 1); |
84 by (rtac (major RS bspec RS bspec RS mp) 1); |
84 by (rtac (major RS bspec RS bspec RS mp) 1); |
85 by (REPEAT (resolve_tac prems 1)); |
85 by (REPEAT (resolve_tac prems 1)); |
86 qed "inj_ontoD"; |
86 qed "inj_ontoD"; |
87 |
87 |
88 goal Fun.thy "!!x y.[| inj_onto f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)"; |
88 goal Fun.thy "!!x y.[| inj_onto f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)"; |
89 by (fast_tac (!claset addSEs [inj_ontoD]) 1); |
89 by (blast_tac (!claset addSDs [inj_ontoD]) 1); |
90 qed "inj_onto_iff"; |
90 qed "inj_onto_iff"; |
91 |
91 |
92 val major::prems = goal Fun.thy |
92 val major::prems = goal Fun.thy |
93 "[| inj_onto f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)"; |
93 "[| inj_onto f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)"; |
94 by (rtac contrapos 1); |
94 by (rtac contrapos 1); |
103 "!!f g. [| inj(f); inj_onto g (range f) |] ==> inj(g o f)"; |
103 "!!f g. [| inj(f); inj_onto g (range f) |] ==> inj(g o f)"; |
104 by (fast_tac (!claset addIs [injI] addEs [injD, inj_ontoD]) 1); |
104 by (fast_tac (!claset addIs [injI] addEs [injD, inj_ontoD]) 1); |
105 qed "comp_inj"; |
105 qed "comp_inj"; |
106 |
106 |
107 val [prem] = goal Fun.thy "inj(f) ==> inj_onto f A"; |
107 val [prem] = goal Fun.thy "inj(f) ==> inj_onto f A"; |
108 by (fast_tac (!claset addIs [prem RS injD, inj_ontoI]) 1); |
108 by (blast_tac (!claset addIs [prem RS injD, inj_ontoI]) 1); |
109 qed "inj_imp"; |
109 qed "inj_imp"; |
110 |
110 |
111 val [prem] = goalw Fun.thy [inv_def] "y : range(f) ==> f(inv f y) = y"; |
111 val [prem] = goalw Fun.thy [inv_def] "y : range(f) ==> f(inv f y) = y"; |
112 by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]); |
112 by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]); |
113 qed "f_inv_f"; |
113 qed "f_inv_f"; |
116 "[| inv f x=inv f y; x: range(f); y: range(f) |] ==> x=y"; |
116 "[| inv f x=inv f y; x: range(f); y: range(f) |] ==> x=y"; |
117 by (rtac (arg_cong RS box_equals) 1); |
117 by (rtac (arg_cong RS box_equals) 1); |
118 by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1)); |
118 by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1)); |
119 qed "inv_injective"; |
119 qed "inv_injective"; |
120 |
120 |
121 val prems = goal Fun.thy |
121 goal Fun.thy "!!f. [| inj(f); A<=range(f) |] ==> inj_onto (inv f) A"; |
122 "[| inj(f); A<=range(f) |] ==> inj_onto (inv f) A"; |
|
123 by (cut_facts_tac prems 1); |
|
124 by (fast_tac (!claset addIs [inj_ontoI] |
122 by (fast_tac (!claset addIs [inj_ontoI] |
125 addEs [inv_injective,injD]) 1); |
123 addEs [inv_injective,injD]) 1); |
126 qed "inj_onto_inv"; |
124 qed "inj_onto_inv"; |
127 |
125 |
128 |
126 |