src/ZF/ex/misc.ML
 changeset 4595 fa8cee619732 parent 4477 b3e5857d8d99 child 5068 fb28eaa07e01
equal inserted replaced
4594:f8d4387b40d9 4595:fa8cee619732
`   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.";`