96 "[| (h O g O f): inj(A,A); \ |
96 "[| (h O g O f): inj(A,A); \ |
97 \ (f O h O g): surj(B,B); \ |
97 \ (f O h O g): surj(B,B); \ |
98 \ (g O f O h): surj(C,C); \ |
98 \ (g O f O h): surj(C,C); \ |
99 \ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)"; |
99 \ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)"; |
100 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); |
100 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); |
101 val pastre1 = result(); |
101 qed "pastre1"; |
102 |
102 |
103 val prems = goalw Perm.thy [bij_def] |
103 val prems = goalw Perm.thy [bij_def] |
104 "[| (h O g O f): surj(A,A); \ |
104 "[| (h O g O f): surj(A,A); \ |
105 \ (f O h O g): inj(B,B); \ |
105 \ (f O h O g): inj(B,B); \ |
106 \ (g O f O h): surj(C,C); \ |
106 \ (g O f O h): surj(C,C); \ |
107 \ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)"; |
107 \ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)"; |
108 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); |
108 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); |
109 val pastre2 = result(); |
109 qed "pastre2"; |
110 |
110 |
111 val prems = goalw Perm.thy [bij_def] |
111 val prems = goalw Perm.thy [bij_def] |
112 "[| (h O g O f): surj(A,A); \ |
112 "[| (h O g O f): surj(A,A); \ |
113 \ (f O h O g): surj(B,B); \ |
113 \ (f O h O g): surj(B,B); \ |
114 \ (g O f O h): inj(C,C); \ |
114 \ (g O f O h): inj(C,C); \ |
115 \ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)"; |
115 \ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)"; |
116 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); |
116 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); |
117 val pastre3 = result(); |
117 qed "pastre3"; |
118 |
118 |
119 val prems = goalw Perm.thy [bij_def] |
119 val prems = goalw Perm.thy [bij_def] |
120 "[| (h O g O f): surj(A,A); \ |
120 "[| (h O g O f): surj(A,A); \ |
121 \ (f O h O g): inj(B,B); \ |
121 \ (f O h O g): inj(B,B); \ |
122 \ (g O f O h): inj(C,C); \ |
122 \ (g O f O h): inj(C,C); \ |
123 \ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)"; |
123 \ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)"; |
124 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); |
124 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); |
125 val pastre4 = result(); |
125 qed "pastre4"; |
126 |
126 |
127 val prems = goalw Perm.thy [bij_def] |
127 val prems = goalw Perm.thy [bij_def] |
128 "[| (h O g O f): inj(A,A); \ |
128 "[| (h O g O f): inj(A,A); \ |
129 \ (f O h O g): surj(B,B); \ |
129 \ (f O h O g): surj(B,B); \ |
130 \ (g O f O h): inj(C,C); \ |
130 \ (g O f O h): inj(C,C); \ |
131 \ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)"; |
131 \ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)"; |
132 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); |
132 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); |
133 val pastre5 = result(); |
133 qed "pastre5"; |
134 |
134 |
135 val prems = goalw Perm.thy [bij_def] |
135 val prems = goalw Perm.thy [bij_def] |
136 "[| (h O g O f): inj(A,A); \ |
136 "[| (h O g O f): inj(A,A); \ |
137 \ (f O h O g): inj(B,B); \ |
137 \ (f O h O g): inj(B,B); \ |
138 \ (g O f O h): surj(C,C); \ |
138 \ (g O f O h): surj(C,C); \ |
139 \ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)"; |
139 \ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)"; |
140 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); |
140 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); |
141 val pastre6 = result(); |
141 qed "pastre6"; |
142 |
142 |
143 (** Yet another example... **) |
143 (** Yet another example... **) |
144 |
144 |
145 goal (merge_theories(Sum.thy,Perm.thy)) |
145 goal (merge_theories(Sum.thy,Perm.thy)) |
146 "(lam Z:Pow(A+B). <{x:A. Inl(x):Z}, {y:B. Inr(y):Z}>) \ |
146 "(lam Z:Pow(A+B). <{x:A. Inl(x):Z}, {y:B. Inr(y):Z}>) \ |