src/ZF/OrderArith.thy
changeset 14120 3a73850c6c7d
parent 13823 d49ffd9f9662
child 14171 0cab06e3bbd0
     1.1 --- a/src/ZF/OrderArith.thy	Mon Jul 21 10:58:16 2003 +0200
     1.2 +++ b/src/ZF/OrderArith.thy	Mon Jul 21 13:02:07 2003 +0200
     1.3 @@ -543,6 +543,27 @@
     1.4  apply (frule ok, assumption+, blast) 
     1.5  done
     1.6  
     1.7 +subsubsection{*Bijections involving Powersets*}
     1.8 +
     1.9 +lemma Pow_sum_bij:
    1.10 +    "(\<lambda>Z \<in> Pow(A+B). <{x \<in> A. Inl(x) \<in> Z}, {y \<in> B. Inr(y) \<in> Z}>)  
    1.11 +     \<in> bij(Pow(A+B), Pow(A)*Pow(B))"
    1.12 +apply (rule_tac d = "%<X,Y>. {Inl (x). x \<in> X} Un {Inr (y). y \<in> Y}" 
    1.13 +       in lam_bijective)
    1.14 +apply force+
    1.15 +done
    1.16 +
    1.17 +text{*As a special case, we have @{term "bij(Pow(A*B), A -> Pow(B))"} *}
    1.18 +lemma Pow_Sigma_bij:
    1.19 +    "(\<lambda>r \<in> Pow(Sigma(A,B)). \<lambda>x \<in> A. r``{x})  
    1.20 +     \<in> bij(Pow(Sigma(A,B)), \<Pi>x \<in> A. Pow(B(x)))"
    1.21 +apply (rule_tac d = "%f. \<Union>x \<in> A. \<Union>y \<in> f`x. {<x,y>}" in lam_bijective)
    1.22 +apply (blast intro: lam_type)
    1.23 +apply (blast dest: apply_type, simp_all)
    1.24 +apply fast (*strange, but blast can't do it*)
    1.25 +apply (rule fun_extension, auto)
    1.26 +by blast
    1.27 +
    1.28  
    1.29  ML {*
    1.30  val measure_def = thm "measure_def";