1.1 --- a/src/HOL/Finite_Set.thy	Mon Nov 22 10:34:33 2010 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Nov 23 14:14:17 2010 +0100
     1.3 @@ -2179,6 +2179,11 @@
     1.4       finite A; finite B |] ==> card A = card B"
     1.5  by (auto intro: le_antisym card_inj_on_le)
     1.6  
     1.7 +lemma bij_betw_finite:
     1.8 +  assumes "bij_betw f A B"
     1.9 +  shows "finite A \<longleftrightarrow> finite B"
    1.10 +using assms unfolding bij_betw_def
    1.11 +using finite_imageD[of f A] by auto
    1.12  
    1.13  subsubsection {* Pigeonhole Principles *}
    1.14  

     2.1 --- a/src/HOL/Fun.thy	Mon Nov 22 10:34:33 2010 +0100
     2.2 +++ b/src/HOL/Fun.thy	Tue Nov 23 14:14:17 2010 +0100
     2.3 @@ -169,6 +169,14 @@
     2.4  lemma inj_on_eq_iff: "inj_on f A ==> x:A ==> y:A ==> (f(x) = f(y)) = (x=y)"
     2.5  by (force simp add: inj_on_def)
     2.6  
     2.7 +lemma inj_on_cong:
     2.8 +  "(\<And> a. a : A \<Longrightarrow> f a = g a) \<Longrightarrow> inj_on f A = inj_on g A"
     2.9 +unfolding inj_on_def by auto
    2.10 +
    2.11 +lemma inj_on_strict_subset:
    2.12 +  "\<lbrakk> inj_on f B; A < B \<rbrakk> \<Longrightarrow> f`A < f`B"
    2.13 +unfolding inj_on_def unfolding image_def by blast
    2.14 +
    2.15  lemma inj_comp:
    2.16    "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
    2.17    by (simp add: inj_on_def)
    2.18 @@ -185,6 +193,42 @@
    2.19  lemma inj_on_id2[simp]: "inj_on (%x. x) A"
    2.20  by (simp add: inj_on_def)
    2.21  
    2.22 +lemma inj_on_Int: "\<lbrakk>inj_on f A; inj_on f B\<rbrakk> \<Longrightarrow> inj_on f (A \<inter> B)"
    2.23 +unfolding inj_on_def by blast
    2.24 +
    2.25 +lemma inj_on_INTER:
    2.26 +  "\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)\<rbrakk> \<Longrightarrow> inj_on f (\<Inter> i \<in> I. A i)"
    2.27 +unfolding inj_on_def by blast
    2.28 +
    2.29 +lemma inj_on_Inter:
    2.30 +  "\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> inj_on f A\<rbrakk> \<Longrightarrow> inj_on f (Inter S)"
    2.31 +unfolding inj_on_def by blast
    2.32 +
    2.33 +lemma inj_on_UNION_chain:
    2.34 +  assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
    2.35 +         INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
    2.36 +  shows "inj_on f (\<Union> i \<in> I. A i)"
    2.37 +proof(unfold inj_on_def UNION_def, auto)
    2.38 +  fix i j x y
    2.39 +  assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
    2.40 +         and ***: "f x = f y"
    2.41 +  show "x = y"
    2.42 +  proof-
    2.43 +    {assume "A i \<le> A j"
    2.44 +     with ** have "x \<in> A j" by auto
    2.45 +     with INJ * ** *** have ?thesis
    2.46 +     by(auto simp add: inj_on_def)
    2.47 +    }
    2.48 +    moreover
    2.49 +    {assume "A j \<le> A i"
    2.50 +     with ** have "y \<in> A i" by auto
    2.51 +     with INJ * ** *** have ?thesis
    2.52 +     by(auto simp add: inj_on_def)
    2.53 +    }
    2.54 +    ultimately show ?thesis using  CH * by blast
    2.55 +  qed
    2.56 +qed
    2.57 +
    2.58  lemma surj_id: "surj id"
    2.59  by simp
    2.60  
    2.61 @@ -249,6 +293,14 @@
    2.62  apply (blast)
    2.63  done
    2.64  
    2.65 +lemma comp_inj_on_iff:
    2.66 +  "inj_on f A \<Longrightarrow> inj_on f' (f ` A) \<longleftrightarrow> inj_on (f' o f) A"
    2.67 +by(auto simp add: comp_inj_on inj_on_def)
    2.68 +
    2.69 +lemma inj_on_imageI2:
    2.70 +  "inj_on (f' o f) A \<Longrightarrow> inj_on f A"
    2.71 +by(auto simp add: comp_inj_on inj_on_def)
    2.72 +
    2.73  lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
    2.74    by auto
    2.75  
    2.76 @@ -270,6 +322,20 @@
    2.77  lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
    2.78    unfolding bij_betw_def by auto
    2.79  
    2.80 +lemma bij_betw_empty1:
    2.81 +  assumes "bij_betw f {} A"
    2.82 +  shows "A = {}"
    2.83 +using assms unfolding bij_betw_def by blast
    2.84 +
    2.85 +lemma bij_betw_empty2:
    2.86 +  assumes "bij_betw f A {}"
    2.87 +  shows "A = {}"
    2.88 +using assms unfolding bij_betw_def by blast
    2.89 +
    2.90 +lemma inj_on_imp_bij_betw:
    2.91 +  "inj_on f A \<Longrightarrow> bij_betw f A (f ` A)"
    2.92 +unfolding bij_betw_def by simp
    2.93 +
    2.94  lemma bij_def: "bij f \<longleftrightarrow> inj f \<and> surj f"
    2.95    unfolding bij_betw_def ..
    2.96  
    2.97 @@ -292,6 +358,32 @@
    2.98  lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
    2.99    by (rule bij_betw_trans)
   2.100  
   2.101 +lemma bij_betw_comp_iff:
   2.102 +  "bij_betw f A A' \<Longrightarrow> bij_betw f' A' A'' \<longleftrightarrow> bij_betw (f' o f) A A''"
   2.103 +by(auto simp add: bij_betw_def inj_on_def)
   2.104 +
   2.105 +lemma bij_betw_comp_iff2:
   2.106 +  assumes BIJ: "bij_betw f' A' A''" and IM: "f ` A \<le> A'"
   2.107 +  shows "bij_betw f A A' \<longleftrightarrow> bij_betw (f' o f) A A''"
   2.108 +using assms
   2.109 +proof(auto simp add: bij_betw_comp_iff)
   2.110 +  assume *: "bij_betw (f' \<circ> f) A A''"
   2.111 +  thus "bij_betw f A A'"
   2.112 +  using IM
   2.113 +  proof(auto simp add: bij_betw_def)
   2.114 +    assume "inj_on (f' \<circ> f) A"
   2.115 +    thus "inj_on f A" using inj_on_imageI2 by blast
   2.116 +  next
   2.117 +    fix a' assume **: "a' \<in> A'"
   2.118 +    hence "f' a' \<in> A''" using BIJ unfolding bij_betw_def by auto
   2.119 +    then obtain a where 1: "a \<in> A \<and> f'(f a) = f' a'" using *
   2.120 +    unfolding bij_betw_def by force
   2.121 +    hence "f a \<in> A'" using IM by auto
   2.122 +    hence "f a = a'" using BIJ ** 1 unfolding bij_betw_def inj_on_def by auto
   2.123 +    thus "a' \<in> f ` A" using 1 by auto
   2.124 +  qed
   2.125 +qed
   2.126 +
   2.127  lemma bij_betw_inv: assumes "bij_betw f A B" shows "EX g. bij_betw g B A"
   2.128  proof -
   2.129    have i: "inj_on f A" and s: "f ` A = B"
   2.130 @@ -323,11 +415,73 @@
   2.131    ultimately show ?thesis by(auto simp:bij_betw_def)
   2.132  qed
   2.133  
   2.134 +lemma bij_betw_cong:
   2.135 +  "(\<And> a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> bij_betw f A A' = bij_betw g A A'"
   2.136 +unfolding bij_betw_def inj_on_def by force
   2.137 +
   2.138 +lemma bij_betw_id[intro, simp]:
   2.139 +  "bij_betw id A A"
   2.140 +unfolding bij_betw_def id_def by auto
   2.141 +
   2.142 +lemma bij_betw_id_iff:
   2.143 +  "bij_betw id A B \<longleftrightarrow> A = B"
   2.144 +by(auto simp add: bij_betw_def)
   2.145 +
   2.146  lemma bij_betw_combine:
   2.147    assumes "bij_betw f A B" "bij_betw f C D" "B \<inter> D = {}"
   2.148    shows "bij_betw f (A \<union> C) (B \<union> D)"
   2.149    using assms unfolding bij_betw_def inj_on_Un image_Un by auto
   2.150  
   2.151 +lemma bij_betw_UNION_chain:
   2.152 +  assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
   2.153 +         BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
   2.154 +  shows "bij_betw f (\<Union> i \<in> I. A i) (\<Union> i \<in> I. A' i)"
   2.155 +proof(unfold bij_betw_def, auto simp add: image_def)
   2.156 +  have "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
   2.157 +  using BIJ bij_betw_def[of f] by auto
   2.158 +  thus "inj_on f (\<Union> i \<in> I. A i)"
   2.159 +  using CH inj_on_UNION_chain[of I A f] by auto
   2.160 +next
   2.161 +  fix i x
   2.162 +  assume *: "i \<in> I" "x \<in> A i"
   2.163 +  hence "f x \<in> A' i" using BIJ bij_betw_def[of f] by auto
   2.164 +  thus "\<exists>j \<in> I. f x \<in> A' j" using * by blast
   2.165 +next
   2.166 +  fix i x'
   2.167 +  assume *: "i \<in> I" "x' \<in> A' i"
   2.168 +  hence "\<exists>x \<in> A i. x' = f x" using BIJ bij_betw_def[of f] by blast
   2.169 +  thus "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
   2.170 +  using * by blast
   2.171 +qed
   2.172 +
   2.173 +lemma bij_betw_Disj_Un:
   2.174 +  assumes DISJ: "A \<inter> B = {}" and DISJ': "A' \<inter> B' = {}" and
   2.175 +          B1: "bij_betw f A A'" and B2: "bij_betw f B B'"
   2.176 +  shows "bij_betw f (A \<union> B) (A' \<union> B')"
   2.177 +proof-
   2.178 +  have 1: "inj_on f A \<and> inj_on f B"
   2.179 +  using B1 B2 by (auto simp add: bij_betw_def)
   2.180 +  have 2: "f`A = A' \<and> f`B = B'"
   2.181 +  using B1 B2 by (auto simp add: bij_betw_def)
   2.182 +  hence "f`(A - B) \<inter> f`(B - A) = {}"
   2.183 +  using DISJ DISJ' by blast
   2.184 +  hence "inj_on f (A \<union> B)"
   2.185 +  using 1 by (auto simp add: inj_on_Un)
   2.186 +  (*  *)
   2.187 +  moreover
   2.188 +  have "f`(A \<union> B) = A' \<union> B'"
   2.189 +  using 2 by auto
   2.190 +  ultimately show ?thesis
   2.191 +  unfolding bij_betw_def by auto
   2.192 +qed
   2.193 +
   2.194 +lemma bij_betw_subset:
   2.195 +  assumes BIJ: "bij_betw f A A'" and
   2.196 +          SUB: "B \<le> A" and IM: "f ` B = B'"
   2.197 +  shows "bij_betw f B B'"
   2.198 +using assms
   2.199 +by(unfold bij_betw_def inj_on_def, auto simp add: inj_on_def)
   2.200 +
   2.201  lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
   2.202  by simp
   2.203  
   2.204 @@ -613,6 +767,17 @@
   2.205    shows "the_inv f (f x) = x" using assms UNIV_I
   2.206    by (rule the_inv_into_f_f)
   2.207  
   2.208 +subsection {* Cantor's Paradox *}
   2.209 +
   2.210 +lemma Cantors_paradox:
   2.211 +  "\<not>(\<exists>f. f ` A = Pow A)"
   2.212 +proof clarify
   2.213 +  fix f assume "f ` A = Pow A" hence *: "Pow A \<le> f ` A" by blast
   2.214 +  let ?X = "{a \<in> A. a \<notin> f a}"
   2.215 +  have "?X \<in> Pow A" unfolding Pow_def by auto
   2.216 +  with * obtain x where "x \<in> A \<and> f x = ?X" by blast
   2.217 +  thus False by best
   2.218 +qed
   2.219  
   2.220  subsection {* Proof tool setup *} 
   2.221  

     3.1 --- a/src/HOL/Hilbert_Choice.thy	Mon Nov 22 10:34:33 2010 +0100
     3.2 +++ b/src/HOL/Hilbert_Choice.thy	Tue Nov 23 14:14:17 2010 +0100
     3.3 @@ -261,6 +261,208 @@
     3.4    ultimately show "finite (UNIV :: 'a set)" by simp
     3.5  qed
     3.6  
     3.7 +lemma image_inv_into_cancel:
     3.8 +  assumes SURJ: "f`A=A'" and SUB: "B' \<le> A'"
     3.9 +  shows "f `((inv_into A f)`B') = B'"
    3.10 +  using assms
    3.11 +proof (auto simp add: f_inv_into_f)
    3.12 +  let ?f' = "(inv_into A f)"
    3.13 +  fix a' assume *: "a' \<in> B'"
    3.14 +  then have "a' \<in> A'" using SUB by auto
    3.15 +  then have "a' = f (?f' a')"
    3.16 +    using SURJ by (auto simp add: f_inv_into_f)
    3.17 +  then show "a' \<in> f ` (?f' ` B')" using * by blast
    3.18 +qed
    3.19 +
    3.20 +lemma inv_into_inv_into_eq:
    3.21 +  assumes "bij_betw f A A'" "a \<in> A"
    3.22 +  shows "inv_into A' (inv_into A f) a = f a"
    3.23 +proof -
    3.24 +  let ?f' = "inv_into A f"   let ?f'' = "inv_into A' ?f'"
    3.25 +  have 1: "bij_betw ?f' A' A" using assms
    3.26 +  by (auto simp add: bij_betw_inv_into)
    3.27 +  obtain a' where 2: "a' \<in> A'" and 3: "?f' a' = a"
    3.28 +    using 1 `a \<in> A` unfolding bij_betw_def by force
    3.29 +  hence "?f'' a = a'"
    3.30 +    using `a \<in> A` 1 3 by (auto simp add: f_inv_into_f bij_betw_def)
    3.31 +  moreover have "f a = a'" using assms 2 3
    3.32 +    by (auto simp add: inv_into_f_f bij_betw_def)
    3.33 +  ultimately show "?f'' a = f a" by simp
    3.34 +qed
    3.35 +
    3.36 +lemma inj_on_iff_surj:
    3.37 +  assumes "A \<noteq> {}"
    3.38 +  shows "(\<exists>f. inj_on f A \<and> f ` A \<le> A') \<longleftrightarrow> (\<exists>g. g ` A' = A)"
    3.39 +proof safe
    3.40 +  fix f assume INJ: "inj_on f A" and INCL: "f ` A \<le> A'"
    3.41 +  let ?phi = "\<lambda>a' a. a \<in> A \<and> f a = a'"  let ?csi = "\<lambda>a. a \<in> A"
    3.42 +  let ?g = "\<lambda>a'. if a' \<in> f ` A then (SOME a. ?phi a' a) else (SOME a. ?csi a)"
    3.43 +  have "?g ` A' = A"
    3.44 +  proof
    3.45 +    show "?g ` A' \<le> A"
    3.46 +    proof clarify
    3.47 +      fix a' assume *: "a' \<in> A'"
    3.48 +      show "?g a' \<in> A"
    3.49 +      proof cases
    3.50 +        assume Case1: "a' \<in> f ` A"
    3.51 +        then obtain a where "?phi a' a" by blast
    3.52 +        hence "?phi a' (SOME a. ?phi a' a)" using someI[of "?phi a'" a] by blast
    3.53 +        with Case1 show ?thesis by auto
    3.54 +      next
    3.55 +        assume Case2: "a' \<notin> f ` A"
    3.56 +        hence "?csi (SOME a. ?csi a)" using assms someI_ex[of ?csi] by blast
    3.57 +        with Case2 show ?thesis by auto
    3.58 +      qed
    3.59 +    qed
    3.60 +  next
    3.61 +    show "A \<le> ?g ` A'"
    3.62 +    proof-
    3.63 +      {fix a assume *: "a \<in> A"
    3.64 +       let ?b = "SOME aa. ?phi (f a) aa"
    3.65 +       have "?phi (f a) a" using * by auto
    3.66 +       hence 1: "?phi (f a) ?b" using someI[of "?phi(f a)" a] by blast
    3.67 +       hence "?g(f a) = ?b" using * by auto
    3.68 +       moreover have "a = ?b" using 1 INJ * by (auto simp add: inj_on_def)
    3.69 +       ultimately have "?g(f a) = a" by simp
    3.70 +       with INCL * have "?g(f a) = a \<and> f a \<in> A'" by auto
    3.71 +      }
    3.72 +      thus ?thesis by force
    3.73 +    qed
    3.74 +  qed
    3.75 +  thus "\<exists>g. g ` A' = A" by blast
    3.76 +next
    3.77 +  fix g  let ?f = "inv_into A' g"
    3.78 +  have "inj_on ?f (g ` A')"
    3.79 +    by (auto simp add: inj_on_inv_into)
    3.80 +  moreover
    3.81 +  {fix a' assume *: "a' \<in> A'"
    3.82 +   let ?phi = "\<lambda> b'. b' \<in> A' \<and> g b' = g a'"
    3.83 +   have "?phi a'" using * by auto
    3.84 +   hence "?phi(SOME b'. ?phi b')" using someI[of ?phi] by blast
    3.85 +   hence "?f(g a') \<in> A'" unfolding inv_into_def by auto
    3.86 +  }
    3.87 +  ultimately show "\<exists>f. inj_on f (g ` A') \<and> f ` g ` A' \<subseteq> A'" by auto
    3.88 +qed
    3.89 +
    3.90 +lemma Ex_inj_on_UNION_Sigma:
    3.91 +  "\<exists>f. (inj_on f (\<Union> i \<in> I. A i) \<and> f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i))"
    3.92 +proof
    3.93 +  let ?phi = "\<lambda> a i. i \<in> I \<and> a \<in> A i"
    3.94 +  let ?sm = "\<lambda> a. SOME i. ?phi a i"
    3.95 +  let ?f = "\<lambda>a. (?sm a, a)"
    3.96 +  have "inj_on ?f (\<Union> i \<in> I. A i)" unfolding inj_on_def by auto
    3.97 +  moreover
    3.98 +  { { fix i a assume "i \<in> I" and "a \<in> A i"
    3.99 +      hence "?sm a \<in> I \<and> a \<in> A(?sm a)" using someI[of "?phi a" i] by auto
   3.100 +    }
   3.101 +    hence "?f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i)" by auto
   3.102 +  }
   3.103 +  ultimately
   3.104 +  show "inj_on ?f (\<Union> i \<in> I. A i) \<and> ?f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i)"
   3.105 +  by auto
   3.106 +qed
   3.107 +
   3.108 +subsection {* The Cantor-Bernstein Theorem *}
   3.109 +
   3.110 +lemma Cantor_Bernstein_aux:
   3.111 +  shows "\<exists>A' h. A' \<le> A \<and>
   3.112 +                (\<forall>a \<in> A'. a \<notin> g`(B - f ` A')) \<and>
   3.113 +                (\<forall>a \<in> A'. h a = f a) \<and>
   3.114 +                (\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g(h a))"
   3.115 +proof-
   3.116 +  obtain H where H_def: "H = (\<lambda> A'. A - (g`(B - (f ` A'))))" by blast
   3.117 +  have 0: "mono H" unfolding mono_def H_def by blast
   3.118 +  then obtain A' where 1: "H A' = A'" using lfp_unfold by blast
   3.119 +  hence 2: "A' = A - (g`(B - (f ` A')))" unfolding H_def by simp
   3.120 +  hence 3: "A' \<le> A" by blast
   3.121 +  have 4: "\<forall>a \<in> A'.  a \<notin> g`(B - f ` A')"
   3.122 +  using 2 by blast
   3.123 +  have 5: "\<forall>a \<in> A - A'. \<exists>b \<in> B - (f ` A'). a = g b"
   3.124 +  using 2 by blast
   3.125 +  (*  *)
   3.126 +  obtain h where h_def:
   3.127 +  "h = (\<lambda> a. if a \<in> A' then f a else (SOME b. b \<in> B - (f ` A') \<and> a = g b))" by blast
   3.128 +  hence "\<forall>a \<in> A'. h a = f a" by auto
   3.129 +  moreover
   3.130 +  have "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g(h a)"
   3.131 +  proof
   3.132 +    fix a assume *: "a \<in> A - A'"
   3.133 +    let ?phi = "\<lambda> b. b \<in> B - (f ` A') \<and> a = g b"
   3.134 +    have "h a = (SOME b. ?phi b)" using h_def * by auto
   3.135 +    moreover have "\<exists>b. ?phi b" using 5 *  by auto
   3.136 +    ultimately show  "?phi (h a)" using someI_ex[of ?phi] by auto
   3.137 +  qed
   3.138 +  ultimately show ?thesis using 3 4 by blast
   3.139 +qed
   3.140 +
   3.141 +theorem Cantor_Bernstein:
   3.142 +  assumes INJ1: "inj_on f A" and SUB1: "f ` A \<le> B" and
   3.143 +          INJ2: "inj_on g B" and SUB2: "g ` B \<le> A"
   3.144 +  shows "\<exists>h. bij_betw h A B"
   3.145 +proof-
   3.146 +  obtain A' and h where 0: "A' \<le> A" and
   3.147 +  1: "\<forall>a \<in> A'. a \<notin> g`(B - f ` A')" and
   3.148 +  2: "\<forall>a \<in> A'. h a = f a" and
   3.149 +  3: "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g(h a)"
   3.150 +  using Cantor_Bernstein_aux[of A g B f] by blast
   3.151 +  have "inj_on h A"
   3.152 +  proof (intro inj_onI)
   3.153 +    fix a1 a2
   3.154 +    assume 4: "a1 \<in> A" and 5: "a2 \<in> A" and 6: "h a1 = h a2"
   3.155 +    show "a1 = a2"
   3.156 +    proof(cases "a1 \<in> A'")
   3.157 +      assume Case1: "a1 \<in> A'"
   3.158 +      show ?thesis
   3.159 +      proof(cases "a2 \<in> A'")
   3.160 +        assume Case11: "a2 \<in> A'"
   3.161 +        hence "f a1 = f a2" using Case1 2 6 by auto
   3.162 +        thus ?thesis using INJ1 Case1 Case11 0
   3.163 +        unfolding inj_on_def by blast
   3.164 +      next
   3.165 +        assume Case12: "a2 \<notin> A'"
   3.166 +        hence False using 3 5 2 6 Case1 by force
   3.167 +        thus ?thesis by simp
   3.168 +      qed
   3.169 +    next
   3.170 +    assume Case2: "a1 \<notin> A'"
   3.171 +      show ?thesis
   3.172 +      proof(cases "a2 \<in> A'")
   3.173 +        assume Case21: "a2 \<in> A'"
   3.174 +        hence False using 3 4 2 6 Case2 by auto
   3.175 +        thus ?thesis by simp
   3.176 +      next
   3.177 +        assume Case22: "a2 \<notin> A'"
   3.178 +        hence "a1 = g(h a1) \<and> a2 = g(h a2)" using Case2 4 5 3 by auto
   3.179 +        thus ?thesis using 6 by simp
   3.180 +      qed
   3.181 +    qed
   3.182 +  qed
   3.183 +  (*  *)
   3.184 +  moreover
   3.185 +  have "h ` A = B"
   3.186 +  proof safe
   3.187 +    fix a assume "a \<in> A"
   3.188 +    thus "h a \<in> B" using SUB1 2 3 by (case_tac "a \<in> A'", auto)
   3.189 +  next
   3.190 +    fix b assume *: "b \<in> B"
   3.191 +    show "b \<in> h ` A"
   3.192 +    proof(cases "b \<in> f ` A'")
   3.193 +      assume Case1: "b \<in> f ` A'"
   3.194 +      then obtain a where "a \<in> A' \<and> b = f a" by blast
   3.195 +      thus ?thesis using 2 0 by force
   3.196 +    next
   3.197 +      assume Case2: "b \<notin> f ` A'"
   3.198 +      hence "g b \<notin> A'" using 1 * by auto
   3.199 +      hence 4: "g b \<in> A - A'" using * SUB2 by auto
   3.200 +      hence "h(g b) \<in> B \<and> g(h(g b)) = g b"
   3.201 +      using 3 by auto
   3.202 +      hence "h(g b) = b" using * INJ2 unfolding inj_on_def by auto
   3.203 +      thus ?thesis using 4 by force
   3.204 +    qed
   3.205 +  qed
   3.206 +  (*  *)
   3.207 +  ultimately show ?thesis unfolding bij_betw_def by auto
   3.208 +qed
   3.209  
   3.210  subsection {*Other Consequences of Hilbert's Epsilon*}
   3.211  

     4.1 --- a/src/HOL/Set.thy	Mon Nov 22 10:34:33 2010 +0100
     4.2 +++ b/src/HOL/Set.thy	Tue Nov 23 14:14:17 2010 +0100
     4.3 @@ -622,6 +622,8 @@
     4.4  lemma Pow_top: "A \<in> Pow A"
     4.5    by simp
     4.6  
     4.7 +lemma Pow_not_empty: "Pow A \<noteq> {}"
     4.8 +  using Pow_top by blast
     4.9  
    4.10  subsubsection {* Set complement *}
    4.11  
    4.12 @@ -972,6 +974,21 @@
    4.13  lemmas [symmetric, rulify] = atomize_ball
    4.14    and [symmetric, defn] = atomize_ball
    4.15  
    4.16 +lemma image_Pow_mono:
    4.17 +  assumes "f ` A \<le> B"
    4.18 +  shows "(image f) ` (Pow A) \<le> Pow B"
    4.19 +using assms by blast
    4.20 +
    4.21 +lemma image_Pow_surj:
    4.22 +  assumes "f ` A = B"
    4.23 +  shows "(image f) ` (Pow A) = Pow B"
    4.24 +using assms unfolding Pow_def proof(auto)
    4.25 +  fix Y assume *: "Y \<le> f ` A"
    4.26 +  obtain X where X_def: "X = {x \<in> A. f x \<in> Y}" by blast
    4.27 +  have "f ` X = Y \<and> X \<le> A" unfolding X_def using * by auto
    4.28 +  thus "Y \<in> (image f) ` {X. X \<le> A}" by blast
    4.29 +qed
    4.30 +
    4.31  subsubsection {* Derived rules involving subsets. *}
    4.32  
    4.33  text {* @{text insert}. *}

     5.1 --- a/src/HOL/SetInterval.thy	Mon Nov 22 10:34:33 2010 +0100
     5.2 +++ b/src/HOL/SetInterval.thy	Tue Nov 23 14:14:17 2010 +0100
     5.3 @@ -159,6 +159,10 @@
     5.4   apply simp_all
     5.5  done
     5.6  
     5.7 +lemma lessThan_strict_subset_iff:
     5.8 +  fixes m n :: "'a::linorder"
     5.9 +  shows "{..<m} < {..<n} \<longleftrightarrow> m < n"
    5.10 +  by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq)
    5.11  
    5.12  subsection {*Two-sided intervals*}
    5.13  
    5.14 @@ -262,6 +266,18 @@
    5.15  apply (simp add: less_imp_le)
    5.16  done
    5.17  
    5.18 +lemma atLeastLessThan_inj:
    5.19 +  fixes a b c d :: "'a::linorder"
    5.20 +  assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d"
    5.21 +  shows "a = c" "b = d"
    5.22 +using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le linorder_antisym_conv2 subset_refl)+
    5.23 +
    5.24 +lemma atLeastLessThan_eq_iff:
    5.25 +  fixes a b c d :: "'a::linorder"
    5.26 +  assumes "a < b" "c < d"
    5.27 +  shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d"
    5.28 +  using atLeastLessThan_inj assms by auto
    5.29 +
    5.30  subsubsection {* Intersection *}
    5.31  
    5.32  context linorder
    5.33 @@ -705,6 +721,39 @@
    5.34    "finite M \<Longrightarrow> \<exists>h. bij_betw h {1 .. card M} M"
    5.35  by (rule finite_same_card_bij) auto
    5.36  
    5.37 +lemma bij_betw_iff_card:
    5.38 +  assumes FIN: "finite A" and FIN': "finite B"
    5.39 +  shows BIJ: "(\<exists>f. bij_betw f A B) \<longleftrightarrow> (card A = card B)"
    5.40 +using assms
    5.41 +proof(auto simp add: bij_betw_same_card)
    5.42 +  assume *: "card A = card B"
    5.43 +  obtain f where "bij_betw f A {0 ..< card A}"
    5.44 +  using FIN ex_bij_betw_finite_nat by blast
    5.45 +  moreover obtain g where "bij_betw g {0 ..< card B} B"
    5.46 +  using FIN' ex_bij_betw_nat_finite by blast
    5.47 +  ultimately have "bij_betw (g o f) A B"
    5.48 +  using * by (auto simp add: bij_betw_trans)
    5.49 +  thus "(\<exists>f. bij_betw f A B)" by blast
    5.50 +qed
    5.51 +
    5.52 +lemma inj_on_iff_card_le:
    5.53 +  assumes FIN: "finite A" and FIN': "finite B"
    5.54 +  shows "(\<exists>f. inj_on f A \<and> f ` A \<le> B) = (card A \<le> card B)"
    5.55 +proof (safe intro!: card_inj_on_le)
    5.56 +  assume *: "card A \<le> card B"
    5.57 +  obtain f where 1: "inj_on f A" and 2: "f ` A = {0 ..< card A}"
    5.58 +  using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force
    5.59 +  moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g ` {0 ..< card B} = B"
    5.60 +  using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force
    5.61 +  ultimately have "inj_on g (f ` A)" using subset_inj_on[of g _ "f ` A"] * by force
    5.62 +  hence "inj_on (g o f) A" using 1 comp_inj_on by blast
    5.63 +  moreover
    5.64 +  {have "{0 ..< card A} \<le> {0 ..< card B}" using * by force
    5.65 +   with 2 have "f ` A  \<le> {0 ..< card B}" by blast
    5.66 +   hence "(g o f) ` A \<le> B" unfolding comp_def using 3 by force
    5.67 +  }
    5.68 +  ultimately show "(\<exists>f. inj_on f A \<and> f ` A \<le> B)" by blast
    5.69 +qed (insert assms, auto)
    5.70  
    5.71  subsection {* Intervals of integers *}
    5.72