equal
deleted
inserted
replaced
155 \ : bij(Pow(A+B), Pow(A)*Pow(B))"; |
155 \ : bij(Pow(A+B), Pow(A)*Pow(B))"; |
156 by (res_inst_tac [("d", "%<X,Y>.{Inl(x).x:X} Un {Inr(y).y:Y}")] |
156 by (res_inst_tac [("d", "%<X,Y>.{Inl(x).x:X} Un {Inr(y).y:Y}")] |
157 lam_bijective 1); |
157 lam_bijective 1); |
158 (*Auto_tac no longer proves it*) |
158 (*Auto_tac no longer proves it*) |
159 by (REPEAT (fast_tac (claset() addss (simpset())) 1)); |
159 by (REPEAT (fast_tac (claset() addss (simpset())) 1)); |
160 qed "Pow_bij"; |
160 qed "Pow_sum_bij"; |
|
161 |
|
162 (*As a special case, we have bij(Pow(A*B), A -> Pow B) *) |
|
163 goal Perm.thy |
|
164 "(lam r:Pow(Sigma(A,B)). lam x:A. r``{x}) \ |
|
165 \ : bij(Pow(Sigma(A,B)), PROD x:A. Pow(B(x)))"; |
|
166 by (res_inst_tac [("d", "%f. UN x:A. UN y:f`x. {<x,y>}")] lam_bijective 1); |
|
167 by (blast_tac (claset() addDs [apply_type]) 2); |
|
168 by (blast_tac (claset() addIs [lam_type]) 1); |
|
169 by (ALLGOALS Asm_simp_tac); |
|
170 by (Fast_tac 1); |
|
171 by (rtac fun_extension 1); |
|
172 by (assume_tac 2); |
|
173 by (rtac (singletonI RS lam_type) 1); |
|
174 by (Asm_simp_tac 1); |
|
175 by (Blast_tac 1); |
|
176 qed "Pow_Sigma_bij"; |
161 |
177 |
162 writeln"Reached end of file."; |
178 writeln"Reached end of file."; |