merged
authorhoelzl
Fri Nov 26 10:04:04 2010 +0100 (2010-11-26)
changeset 40704407c6122956f
parent 40701 e7aa34600c36
parent 40703 d1fc454d6735
child 40708 739dc2c2ba24
merged
     1.1 --- a/NEWS	Fri Nov 26 09:15:49 2010 +0100
     1.2 +++ b/NEWS	Fri Nov 26 10:04:04 2010 +0100
     1.3 @@ -291,9 +291,10 @@
     1.4  derive instantiated and simplified equations for inductive predicates,
     1.5  similar to inductive_cases.
     1.6  
     1.7 -* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". surj_on is a
     1.8 -generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV".
     1.9 -The theorems bij_def and surj_def are unchanged.
    1.10 +* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". "surj f" is now an
    1.11 +abbreviation of "range f = UIV". The theorems bij_def and surj_def are
    1.12 +unchanged.
    1.13 +INCOMPATIBILITY.
    1.14  
    1.15  * Function package: .psimps rules are no longer implicitly declared [simp].
    1.16  INCOMPATIBILITY.
     2.1 --- a/src/HOL/Finite_Set.thy	Fri Nov 26 09:15:49 2010 +0100
     2.2 +++ b/src/HOL/Finite_Set.thy	Fri Nov 26 10:04:04 2010 +0100
     2.3 @@ -2179,6 +2179,11 @@
     2.4       finite A; finite B |] ==> card A = card B"
     2.5  by (auto intro: le_antisym card_inj_on_le)
     2.6  
     2.7 +lemma bij_betw_finite:
     2.8 +  assumes "bij_betw f A B"
     2.9 +  shows "finite A \<longleftrightarrow> finite B"
    2.10 +using assms unfolding bij_betw_def
    2.11 +using finite_imageD[of f A] by auto
    2.12  
    2.13  subsubsection {* Pigeonhole Principles *}
    2.14  
    2.15 @@ -2286,7 +2291,7 @@
    2.16  
    2.17  lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
    2.18  shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
    2.19 -by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
    2.20 +by (blast intro: finite_surj_inj subset_UNIV)
    2.21  
    2.22  lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
    2.23  shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
     3.1 --- a/src/HOL/Fun.thy	Fri Nov 26 09:15:49 2010 +0100
     3.2 +++ b/src/HOL/Fun.thy	Fri Nov 26 10:04:04 2010 +0100
     3.3 @@ -130,24 +130,22 @@
     3.4    by (simp_all add: fun_eq_iff)
     3.5  
     3.6  
     3.7 -subsection {* Injectivity, Surjectivity and Bijectivity *}
     3.8 +subsection {* Injectivity and Bijectivity *}
     3.9  
    3.10  definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" where -- "injective"
    3.11    "inj_on f A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y)"
    3.12  
    3.13 -definition surj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> bool" where -- "surjective"
    3.14 -  "surj_on f B \<longleftrightarrow> B \<subseteq> range f"
    3.15 -
    3.16  definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" where -- "bijective"
    3.17    "bij_betw f A B \<longleftrightarrow> inj_on f A \<and> f ` A = B"
    3.18  
    3.19 -text{*A common special case: functions injective over the entire domain type.*}
    3.20 +text{*A common special case: functions injective, surjective or bijective over
    3.21 +the entire domain type.*}
    3.22  
    3.23  abbreviation
    3.24    "inj f \<equiv> inj_on f UNIV"
    3.25  
    3.26 -abbreviation
    3.27 -  "surj f \<equiv> surj_on f UNIV"
    3.28 +abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" where -- "surjective"
    3.29 +  "surj f \<equiv> (range f = UNIV)"
    3.30  
    3.31  abbreviation
    3.32    "bij f \<equiv> bij_betw f UNIV UNIV"
    3.33 @@ -171,6 +169,14 @@
    3.34  lemma inj_on_eq_iff: "inj_on f A ==> x:A ==> y:A ==> (f(x) = f(y)) = (x=y)"
    3.35  by (force simp add: inj_on_def)
    3.36  
    3.37 +lemma inj_on_cong:
    3.38 +  "(\<And> a. a : A \<Longrightarrow> f a = g a) \<Longrightarrow> inj_on f A = inj_on g A"
    3.39 +unfolding inj_on_def by auto
    3.40 +
    3.41 +lemma inj_on_strict_subset:
    3.42 +  "\<lbrakk> inj_on f B; A < B \<rbrakk> \<Longrightarrow> f`A < f`B"
    3.43 +unfolding inj_on_def unfolding image_def by blast
    3.44 +
    3.45  lemma inj_comp:
    3.46    "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
    3.47    by (simp add: inj_on_def)
    3.48 @@ -187,8 +193,44 @@
    3.49  lemma inj_on_id2[simp]: "inj_on (%x. x) A"
    3.50  by (simp add: inj_on_def)
    3.51  
    3.52 -lemma surj_id[simp]: "surj_on id A"
    3.53 -by (simp add: surj_on_def)
    3.54 +lemma inj_on_Int: "\<lbrakk>inj_on f A; inj_on f B\<rbrakk> \<Longrightarrow> inj_on f (A \<inter> B)"
    3.55 +unfolding inj_on_def by blast
    3.56 +
    3.57 +lemma inj_on_INTER:
    3.58 +  "\<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)"
    3.59 +unfolding inj_on_def by blast
    3.60 +
    3.61 +lemma inj_on_Inter:
    3.62 +  "\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> inj_on f A\<rbrakk> \<Longrightarrow> inj_on f (Inter S)"
    3.63 +unfolding inj_on_def by blast
    3.64 +
    3.65 +lemma inj_on_UNION_chain:
    3.66 +  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
    3.67 +         INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
    3.68 +  shows "inj_on f (\<Union> i \<in> I. A i)"
    3.69 +proof(unfold inj_on_def UNION_def, auto)
    3.70 +  fix i j x y
    3.71 +  assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
    3.72 +         and ***: "f x = f y"
    3.73 +  show "x = y"
    3.74 +  proof-
    3.75 +    {assume "A i \<le> A j"
    3.76 +     with ** have "x \<in> A j" by auto
    3.77 +     with INJ * ** *** have ?thesis
    3.78 +     by(auto simp add: inj_on_def)
    3.79 +    }
    3.80 +    moreover
    3.81 +    {assume "A j \<le> A i"
    3.82 +     with ** have "y \<in> A i" by auto
    3.83 +     with INJ * ** *** have ?thesis
    3.84 +     by(auto simp add: inj_on_def)
    3.85 +    }
    3.86 +    ultimately show ?thesis using  CH * by blast
    3.87 +  qed
    3.88 +qed
    3.89 +
    3.90 +lemma surj_id: "surj id"
    3.91 +by simp
    3.92  
    3.93  lemma bij_id[simp]: "bij id"
    3.94  by (simp add: bij_betw_def)
    3.95 @@ -251,20 +293,19 @@
    3.96  apply (blast)
    3.97  done
    3.98  
    3.99 -lemma surj_onI: "(\<And>x. x \<in> B \<Longrightarrow> g (f x) = x) \<Longrightarrow> surj_on g B"
   3.100 -  by (simp add: surj_on_def) (blast intro: sym)
   3.101 +lemma comp_inj_on_iff:
   3.102 +  "inj_on f A \<Longrightarrow> inj_on f' (f ` A) \<longleftrightarrow> inj_on (f' o f) A"
   3.103 +by(auto simp add: comp_inj_on inj_on_def)
   3.104  
   3.105 -lemma surj_onD: "surj_on f B \<Longrightarrow> y \<in> B \<Longrightarrow> \<exists>x. y = f x"
   3.106 -  by (auto simp: surj_on_def)
   3.107 -
   3.108 -lemma surj_on_range_iff: "surj_on f B \<longleftrightarrow> (\<exists>A. f ` A = B)"
   3.109 -  unfolding surj_on_def by (auto intro!: exI[of _ "f -` B"])
   3.110 +lemma inj_on_imageI2:
   3.111 +  "inj_on (f' o f) A \<Longrightarrow> inj_on f A"
   3.112 +by(auto simp add: comp_inj_on inj_on_def)
   3.113  
   3.114  lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
   3.115 -  by (simp add: surj_on_def subset_eq image_iff)
   3.116 +  by auto
   3.117  
   3.118 -lemma surjI: "(\<And> x. g (f x) = x) \<Longrightarrow> surj g"
   3.119 -  by (blast intro: surj_onI)
   3.120 +lemma surjI: assumes *: "\<And> x. g (f x) = x" shows "surj g"
   3.121 +  using *[symmetric] by auto
   3.122  
   3.123  lemma surjD: "surj f \<Longrightarrow> \<exists>x. y = f x"
   3.124    by (simp add: surj_def)
   3.125 @@ -278,17 +319,25 @@
   3.126  apply (drule_tac x = x in spec, blast)
   3.127  done
   3.128  
   3.129 -lemma surj_range: "surj f \<Longrightarrow> range f = UNIV"
   3.130 -  by (auto simp add: surj_on_def)
   3.131 +lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
   3.132 +  unfolding bij_betw_def by auto
   3.133 +
   3.134 +lemma bij_betw_empty1:
   3.135 +  assumes "bij_betw f {} A"
   3.136 +  shows "A = {}"
   3.137 +using assms unfolding bij_betw_def by blast
   3.138  
   3.139 -lemma surj_range_iff: "surj f \<longleftrightarrow> range f = UNIV"
   3.140 -  unfolding surj_on_def by auto
   3.141 +lemma bij_betw_empty2:
   3.142 +  assumes "bij_betw f A {}"
   3.143 +  shows "A = {}"
   3.144 +using assms unfolding bij_betw_def by blast
   3.145  
   3.146 -lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
   3.147 -  unfolding bij_betw_def surj_range_iff by auto
   3.148 +lemma inj_on_imp_bij_betw:
   3.149 +  "inj_on f A \<Longrightarrow> bij_betw f A (f ` A)"
   3.150 +unfolding bij_betw_def by simp
   3.151  
   3.152  lemma bij_def: "bij f \<longleftrightarrow> inj f \<and> surj f"
   3.153 -  unfolding surj_range_iff bij_betw_def ..
   3.154 +  unfolding bij_betw_def ..
   3.155  
   3.156  lemma bijI: "[| inj f; surj f |] ==> bij f"
   3.157  by (simp add: bij_def)
   3.158 @@ -302,16 +351,39 @@
   3.159  lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
   3.160  by (simp add: bij_betw_def)
   3.161  
   3.162 -lemma bij_betw_imp_surj_on: "bij_betw f A B \<Longrightarrow> surj_on f B"
   3.163 -by (auto simp: bij_betw_def surj_on_range_iff)
   3.164 -
   3.165 -lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
   3.166 -by(fastsimp intro: comp_inj_on comp_surj simp: bij_def surj_range)
   3.167 -
   3.168  lemma bij_betw_trans:
   3.169    "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g o f) A C"
   3.170  by(auto simp add:bij_betw_def comp_inj_on)
   3.171  
   3.172 +lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
   3.173 +  by (rule bij_betw_trans)
   3.174 +
   3.175 +lemma bij_betw_comp_iff:
   3.176 +  "bij_betw f A A' \<Longrightarrow> bij_betw f' A' A'' \<longleftrightarrow> bij_betw (f' o f) A A''"
   3.177 +by(auto simp add: bij_betw_def inj_on_def)
   3.178 +
   3.179 +lemma bij_betw_comp_iff2:
   3.180 +  assumes BIJ: "bij_betw f' A' A''" and IM: "f ` A \<le> A'"
   3.181 +  shows "bij_betw f A A' \<longleftrightarrow> bij_betw (f' o f) A A''"
   3.182 +using assms
   3.183 +proof(auto simp add: bij_betw_comp_iff)
   3.184 +  assume *: "bij_betw (f' \<circ> f) A A''"
   3.185 +  thus "bij_betw f A A'"
   3.186 +  using IM
   3.187 +  proof(auto simp add: bij_betw_def)
   3.188 +    assume "inj_on (f' \<circ> f) A"
   3.189 +    thus "inj_on f A" using inj_on_imageI2 by blast
   3.190 +  next
   3.191 +    fix a' assume **: "a' \<in> A'"
   3.192 +    hence "f' a' \<in> A''" using BIJ unfolding bij_betw_def by auto
   3.193 +    then obtain a where 1: "a \<in> A \<and> f'(f a) = f' a'" using *
   3.194 +    unfolding bij_betw_def by force
   3.195 +    hence "f a \<in> A'" using IM by auto
   3.196 +    hence "f a = a'" using BIJ ** 1 unfolding bij_betw_def inj_on_def by auto
   3.197 +    thus "a' \<in> f ` A" using 1 by auto
   3.198 +  qed
   3.199 +qed
   3.200 +
   3.201  lemma bij_betw_inv: assumes "bij_betw f A B" shows "EX g. bij_betw g B A"
   3.202  proof -
   3.203    have i: "inj_on f A" and s: "f ` A = B"
   3.204 @@ -343,21 +415,81 @@
   3.205    ultimately show ?thesis by(auto simp:bij_betw_def)
   3.206  qed
   3.207  
   3.208 +lemma bij_betw_cong:
   3.209 +  "(\<And> a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> bij_betw f A A' = bij_betw g A A'"
   3.210 +unfolding bij_betw_def inj_on_def by force
   3.211 +
   3.212 +lemma bij_betw_id[intro, simp]:
   3.213 +  "bij_betw id A A"
   3.214 +unfolding bij_betw_def id_def by auto
   3.215 +
   3.216 +lemma bij_betw_id_iff:
   3.217 +  "bij_betw id A B \<longleftrightarrow> A = B"
   3.218 +by(auto simp add: bij_betw_def)
   3.219 +
   3.220  lemma bij_betw_combine:
   3.221    assumes "bij_betw f A B" "bij_betw f C D" "B \<inter> D = {}"
   3.222    shows "bij_betw f (A \<union> C) (B \<union> D)"
   3.223    using assms unfolding bij_betw_def inj_on_Un image_Un by auto
   3.224  
   3.225 +lemma bij_betw_UNION_chain:
   3.226 +  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
   3.227 +         BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
   3.228 +  shows "bij_betw f (\<Union> i \<in> I. A i) (\<Union> i \<in> I. A' i)"
   3.229 +proof(unfold bij_betw_def, auto simp add: image_def)
   3.230 +  have "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
   3.231 +  using BIJ bij_betw_def[of f] by auto
   3.232 +  thus "inj_on f (\<Union> i \<in> I. A i)"
   3.233 +  using CH inj_on_UNION_chain[of I A f] by auto
   3.234 +next
   3.235 +  fix i x
   3.236 +  assume *: "i \<in> I" "x \<in> A i"
   3.237 +  hence "f x \<in> A' i" using BIJ bij_betw_def[of f] by auto
   3.238 +  thus "\<exists>j \<in> I. f x \<in> A' j" using * by blast
   3.239 +next
   3.240 +  fix i x'
   3.241 +  assume *: "i \<in> I" "x' \<in> A' i"
   3.242 +  hence "\<exists>x \<in> A i. x' = f x" using BIJ bij_betw_def[of f] by blast
   3.243 +  thus "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
   3.244 +  using * by blast
   3.245 +qed
   3.246 +
   3.247 +lemma bij_betw_Disj_Un:
   3.248 +  assumes DISJ: "A \<inter> B = {}" and DISJ': "A' \<inter> B' = {}" and
   3.249 +          B1: "bij_betw f A A'" and B2: "bij_betw f B B'"
   3.250 +  shows "bij_betw f (A \<union> B) (A' \<union> B')"
   3.251 +proof-
   3.252 +  have 1: "inj_on f A \<and> inj_on f B"
   3.253 +  using B1 B2 by (auto simp add: bij_betw_def)
   3.254 +  have 2: "f`A = A' \<and> f`B = B'"
   3.255 +  using B1 B2 by (auto simp add: bij_betw_def)
   3.256 +  hence "f`(A - B) \<inter> f`(B - A) = {}"
   3.257 +  using DISJ DISJ' by blast
   3.258 +  hence "inj_on f (A \<union> B)"
   3.259 +  using 1 by (auto simp add: inj_on_Un)
   3.260 +  (*  *)
   3.261 +  moreover
   3.262 +  have "f`(A \<union> B) = A' \<union> B'"
   3.263 +  using 2 by auto
   3.264 +  ultimately show ?thesis
   3.265 +  unfolding bij_betw_def by auto
   3.266 +qed
   3.267 +
   3.268 +lemma bij_betw_subset:
   3.269 +  assumes BIJ: "bij_betw f A A'" and
   3.270 +          SUB: "B \<le> A" and IM: "f ` B = B'"
   3.271 +  shows "bij_betw f B B'"
   3.272 +using assms
   3.273 +by(unfold bij_betw_def inj_on_def, auto simp add: inj_on_def)
   3.274 +
   3.275  lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
   3.276 -by (simp add: surj_range)
   3.277 +by simp
   3.278  
   3.279  lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
   3.280  by (simp add: inj_on_def, blast)
   3.281  
   3.282  lemma vimage_subsetD: "surj f ==> f -` B <= A ==> B <= f ` A"
   3.283 -apply (unfold surj_def)
   3.284 -apply (blast intro: sym)
   3.285 -done
   3.286 +by (blast intro: sym)
   3.287  
   3.288  lemma vimage_subsetI: "inj f ==> B <= f ` A ==> f -` B <= A"
   3.289  by (unfold inj_on_def, blast)
   3.290 @@ -410,7 +542,7 @@
   3.291  done
   3.292  
   3.293  lemma surj_Compl_image_subset: "surj f ==> -(f`A) <= f`(-A)"
   3.294 -by (auto simp add: surj_def)
   3.295 +by auto
   3.296  
   3.297  lemma inj_image_Compl_subset: "inj f ==> f`(-A) <= -(f`A)"
   3.298  by (auto simp add: inj_on_def)
   3.299 @@ -559,10 +691,10 @@
   3.300  qed
   3.301  
   3.302  lemma surj_imp_surj_swap: "surj f \<Longrightarrow> surj (swap a b f)"
   3.303 -  unfolding surj_range_iff by simp
   3.304 +  by simp
   3.305  
   3.306  lemma surj_swap_iff [simp]: "surj (swap a b f) \<longleftrightarrow> surj f"
   3.307 -  unfolding surj_range_iff by simp
   3.308 +  by simp
   3.309  
   3.310  lemma bij_betw_swap_iff [simp]:
   3.311    "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> bij_betw (swap x y f) A B \<longleftrightarrow> bij_betw f A B"
   3.312 @@ -635,6 +767,17 @@
   3.313    shows "the_inv f (f x) = x" using assms UNIV_I
   3.314    by (rule the_inv_into_f_f)
   3.315  
   3.316 +subsection {* Cantor's Paradox *}
   3.317 +
   3.318 +lemma Cantors_paradox:
   3.319 +  "\<not>(\<exists>f. f ` A = Pow A)"
   3.320 +proof clarify
   3.321 +  fix f assume "f ` A = Pow A" hence *: "Pow A \<le> f ` A" by blast
   3.322 +  let ?X = "{a \<in> A. a \<notin> f a}"
   3.323 +  have "?X \<in> Pow A" unfolding Pow_def by auto
   3.324 +  with * obtain x where "x \<in> A \<and> f x = ?X" by blast
   3.325 +  thus False by best
   3.326 +qed
   3.327  
   3.328  subsection {* Proof tool setup *} 
   3.329  
     4.1 --- a/src/HOL/Hilbert_Choice.thy	Fri Nov 26 09:15:49 2010 +0100
     4.2 +++ b/src/HOL/Hilbert_Choice.thy	Fri Nov 26 10:04:04 2010 +0100
     4.3 @@ -151,10 +151,10 @@
     4.4  by(fastsimp simp: image_def)
     4.5  
     4.6  lemma inj_imp_surj_inv: "inj f ==> surj (inv f)"
     4.7 -by (blast intro: surjI inv_into_f_f)
     4.8 +by (blast intro!: surjI inv_into_f_f)
     4.9  
    4.10  lemma surj_f_inv_f: "surj f ==> f(inv f y) = y"
    4.11 -by (simp add: f_inv_into_f surj_range)
    4.12 +by (simp add: f_inv_into_f)
    4.13  
    4.14  lemma inv_into_injective:
    4.15    assumes eq: "inv_into A f x = inv_into A f y"
    4.16 @@ -173,12 +173,13 @@
    4.17  by (auto simp add: bij_betw_def inj_on_inv_into)
    4.18  
    4.19  lemma surj_imp_inj_inv: "surj f ==> inj (inv f)"
    4.20 -by (simp add: inj_on_inv_into surj_range)
    4.21 +by (simp add: inj_on_inv_into)
    4.22  
    4.23  lemma surj_iff: "(surj f) = (f o inv f = id)"
    4.24 -apply (simp add: o_def fun_eq_iff)
    4.25 -apply (blast intro: surjI surj_f_inv_f)
    4.26 -done
    4.27 +by (auto intro!: surjI simp: surj_f_inv_f fun_eq_iff[where 'b='a])
    4.28 +
    4.29 +lemma surj_iff_all: "surj f \<longleftrightarrow> (\<forall>x. f (inv f x) = x)"
    4.30 +  unfolding surj_iff by (simp add: o_def fun_eq_iff)
    4.31  
    4.32  lemma surj_imp_inv_eq: "[| surj f; \<forall>x. g(f x) = x |] ==> inv f = g"
    4.33  apply (rule ext)
    4.34 @@ -260,6 +261,208 @@
    4.35    ultimately show "finite (UNIV :: 'a set)" by simp
    4.36  qed
    4.37  
    4.38 +lemma image_inv_into_cancel:
    4.39 +  assumes SURJ: "f`A=A'" and SUB: "B' \<le> A'"
    4.40 +  shows "f `((inv_into A f)`B') = B'"
    4.41 +  using assms
    4.42 +proof (auto simp add: f_inv_into_f)
    4.43 +  let ?f' = "(inv_into A f)"
    4.44 +  fix a' assume *: "a' \<in> B'"
    4.45 +  then have "a' \<in> A'" using SUB by auto
    4.46 +  then have "a' = f (?f' a')"
    4.47 +    using SURJ by (auto simp add: f_inv_into_f)
    4.48 +  then show "a' \<in> f ` (?f' ` B')" using * by blast
    4.49 +qed
    4.50 +
    4.51 +lemma inv_into_inv_into_eq:
    4.52 +  assumes "bij_betw f A A'" "a \<in> A"
    4.53 +  shows "inv_into A' (inv_into A f) a = f a"
    4.54 +proof -
    4.55 +  let ?f' = "inv_into A f"   let ?f'' = "inv_into A' ?f'"
    4.56 +  have 1: "bij_betw ?f' A' A" using assms
    4.57 +  by (auto simp add: bij_betw_inv_into)
    4.58 +  obtain a' where 2: "a' \<in> A'" and 3: "?f' a' = a"
    4.59 +    using 1 `a \<in> A` unfolding bij_betw_def by force
    4.60 +  hence "?f'' a = a'"
    4.61 +    using `a \<in> A` 1 3 by (auto simp add: f_inv_into_f bij_betw_def)
    4.62 +  moreover have "f a = a'" using assms 2 3
    4.63 +    by (auto simp add: inv_into_f_f bij_betw_def)
    4.64 +  ultimately show "?f'' a = f a" by simp
    4.65 +qed
    4.66 +
    4.67 +lemma inj_on_iff_surj:
    4.68 +  assumes "A \<noteq> {}"
    4.69 +  shows "(\<exists>f. inj_on f A \<and> f ` A \<le> A') \<longleftrightarrow> (\<exists>g. g ` A' = A)"
    4.70 +proof safe
    4.71 +  fix f assume INJ: "inj_on f A" and INCL: "f ` A \<le> A'"
    4.72 +  let ?phi = "\<lambda>a' a. a \<in> A \<and> f a = a'"  let ?csi = "\<lambda>a. a \<in> A"
    4.73 +  let ?g = "\<lambda>a'. if a' \<in> f ` A then (SOME a. ?phi a' a) else (SOME a. ?csi a)"
    4.74 +  have "?g ` A' = A"
    4.75 +  proof
    4.76 +    show "?g ` A' \<le> A"
    4.77 +    proof clarify
    4.78 +      fix a' assume *: "a' \<in> A'"
    4.79 +      show "?g a' \<in> A"
    4.80 +      proof cases
    4.81 +        assume Case1: "a' \<in> f ` A"
    4.82 +        then obtain a where "?phi a' a" by blast
    4.83 +        hence "?phi a' (SOME a. ?phi a' a)" using someI[of "?phi a'" a] by blast
    4.84 +        with Case1 show ?thesis by auto
    4.85 +      next
    4.86 +        assume Case2: "a' \<notin> f ` A"
    4.87 +        hence "?csi (SOME a. ?csi a)" using assms someI_ex[of ?csi] by blast
    4.88 +        with Case2 show ?thesis by auto
    4.89 +      qed
    4.90 +    qed
    4.91 +  next
    4.92 +    show "A \<le> ?g ` A'"
    4.93 +    proof-
    4.94 +      {fix a assume *: "a \<in> A"
    4.95 +       let ?b = "SOME aa. ?phi (f a) aa"
    4.96 +       have "?phi (f a) a" using * by auto
    4.97 +       hence 1: "?phi (f a) ?b" using someI[of "?phi(f a)" a] by blast
    4.98 +       hence "?g(f a) = ?b" using * by auto
    4.99 +       moreover have "a = ?b" using 1 INJ * by (auto simp add: inj_on_def)
   4.100 +       ultimately have "?g(f a) = a" by simp
   4.101 +       with INCL * have "?g(f a) = a \<and> f a \<in> A'" by auto
   4.102 +      }
   4.103 +      thus ?thesis by force
   4.104 +    qed
   4.105 +  qed
   4.106 +  thus "\<exists>g. g ` A' = A" by blast
   4.107 +next
   4.108 +  fix g  let ?f = "inv_into A' g"
   4.109 +  have "inj_on ?f (g ` A')"
   4.110 +    by (auto simp add: inj_on_inv_into)
   4.111 +  moreover
   4.112 +  {fix a' assume *: "a' \<in> A'"
   4.113 +   let ?phi = "\<lambda> b'. b' \<in> A' \<and> g b' = g a'"
   4.114 +   have "?phi a'" using * by auto
   4.115 +   hence "?phi(SOME b'. ?phi b')" using someI[of ?phi] by blast
   4.116 +   hence "?f(g a') \<in> A'" unfolding inv_into_def by auto
   4.117 +  }
   4.118 +  ultimately show "\<exists>f. inj_on f (g ` A') \<and> f ` g ` A' \<subseteq> A'" by auto
   4.119 +qed
   4.120 +
   4.121 +lemma Ex_inj_on_UNION_Sigma:
   4.122 +  "\<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))"
   4.123 +proof
   4.124 +  let ?phi = "\<lambda> a i. i \<in> I \<and> a \<in> A i"
   4.125 +  let ?sm = "\<lambda> a. SOME i. ?phi a i"
   4.126 +  let ?f = "\<lambda>a. (?sm a, a)"
   4.127 +  have "inj_on ?f (\<Union> i \<in> I. A i)" unfolding inj_on_def by auto
   4.128 +  moreover
   4.129 +  { { fix i a assume "i \<in> I" and "a \<in> A i"
   4.130 +      hence "?sm a \<in> I \<and> a \<in> A(?sm a)" using someI[of "?phi a" i] by auto
   4.131 +    }
   4.132 +    hence "?f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i)" by auto
   4.133 +  }
   4.134 +  ultimately
   4.135 +  show "inj_on ?f (\<Union> i \<in> I. A i) \<and> ?f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i)"
   4.136 +  by auto
   4.137 +qed
   4.138 +
   4.139 +subsection {* The Cantor-Bernstein Theorem *}
   4.140 +
   4.141 +lemma Cantor_Bernstein_aux:
   4.142 +  shows "\<exists>A' h. A' \<le> A \<and>
   4.143 +                (\<forall>a \<in> A'. a \<notin> g`(B - f ` A')) \<and>
   4.144 +                (\<forall>a \<in> A'. h a = f a) \<and>
   4.145 +                (\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g(h a))"
   4.146 +proof-
   4.147 +  obtain H where H_def: "H = (\<lambda> A'. A - (g`(B - (f ` A'))))" by blast
   4.148 +  have 0: "mono H" unfolding mono_def H_def by blast
   4.149 +  then obtain A' where 1: "H A' = A'" using lfp_unfold by blast
   4.150 +  hence 2: "A' = A - (g`(B - (f ` A')))" unfolding H_def by simp
   4.151 +  hence 3: "A' \<le> A" by blast
   4.152 +  have 4: "\<forall>a \<in> A'.  a \<notin> g`(B - f ` A')"
   4.153 +  using 2 by blast
   4.154 +  have 5: "\<forall>a \<in> A - A'. \<exists>b \<in> B - (f ` A'). a = g b"
   4.155 +  using 2 by blast
   4.156 +  (*  *)
   4.157 +  obtain h where h_def:
   4.158 +  "h = (\<lambda> a. if a \<in> A' then f a else (SOME b. b \<in> B - (f ` A') \<and> a = g b))" by blast
   4.159 +  hence "\<forall>a \<in> A'. h a = f a" by auto
   4.160 +  moreover
   4.161 +  have "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g(h a)"
   4.162 +  proof
   4.163 +    fix a assume *: "a \<in> A - A'"
   4.164 +    let ?phi = "\<lambda> b. b \<in> B - (f ` A') \<and> a = g b"
   4.165 +    have "h a = (SOME b. ?phi b)" using h_def * by auto
   4.166 +    moreover have "\<exists>b. ?phi b" using 5 *  by auto
   4.167 +    ultimately show  "?phi (h a)" using someI_ex[of ?phi] by auto
   4.168 +  qed
   4.169 +  ultimately show ?thesis using 3 4 by blast
   4.170 +qed
   4.171 +
   4.172 +theorem Cantor_Bernstein:
   4.173 +  assumes INJ1: "inj_on f A" and SUB1: "f ` A \<le> B" and
   4.174 +          INJ2: "inj_on g B" and SUB2: "g ` B \<le> A"
   4.175 +  shows "\<exists>h. bij_betw h A B"
   4.176 +proof-
   4.177 +  obtain A' and h where 0: "A' \<le> A" and
   4.178 +  1: "\<forall>a \<in> A'. a \<notin> g`(B - f ` A')" and
   4.179 +  2: "\<forall>a \<in> A'. h a = f a" and
   4.180 +  3: "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g(h a)"
   4.181 +  using Cantor_Bernstein_aux[of A g B f] by blast
   4.182 +  have "inj_on h A"
   4.183 +  proof (intro inj_onI)
   4.184 +    fix a1 a2
   4.185 +    assume 4: "a1 \<in> A" and 5: "a2 \<in> A" and 6: "h a1 = h a2"
   4.186 +    show "a1 = a2"
   4.187 +    proof(cases "a1 \<in> A'")
   4.188 +      assume Case1: "a1 \<in> A'"
   4.189 +      show ?thesis
   4.190 +      proof(cases "a2 \<in> A'")
   4.191 +        assume Case11: "a2 \<in> A'"
   4.192 +        hence "f a1 = f a2" using Case1 2 6 by auto
   4.193 +        thus ?thesis using INJ1 Case1 Case11 0
   4.194 +        unfolding inj_on_def by blast
   4.195 +      next
   4.196 +        assume Case12: "a2 \<notin> A'"
   4.197 +        hence False using 3 5 2 6 Case1 by force
   4.198 +        thus ?thesis by simp
   4.199 +      qed
   4.200 +    next
   4.201 +    assume Case2: "a1 \<notin> A'"
   4.202 +      show ?thesis
   4.203 +      proof(cases "a2 \<in> A'")
   4.204 +        assume Case21: "a2 \<in> A'"
   4.205 +        hence False using 3 4 2 6 Case2 by auto
   4.206 +        thus ?thesis by simp
   4.207 +      next
   4.208 +        assume Case22: "a2 \<notin> A'"
   4.209 +        hence "a1 = g(h a1) \<and> a2 = g(h a2)" using Case2 4 5 3 by auto
   4.210 +        thus ?thesis using 6 by simp
   4.211 +      qed
   4.212 +    qed
   4.213 +  qed
   4.214 +  (*  *)
   4.215 +  moreover
   4.216 +  have "h ` A = B"
   4.217 +  proof safe
   4.218 +    fix a assume "a \<in> A"
   4.219 +    thus "h a \<in> B" using SUB1 2 3 by (case_tac "a \<in> A'", auto)
   4.220 +  next
   4.221 +    fix b assume *: "b \<in> B"
   4.222 +    show "b \<in> h ` A"
   4.223 +    proof(cases "b \<in> f ` A'")
   4.224 +      assume Case1: "b \<in> f ` A'"
   4.225 +      then obtain a where "a \<in> A' \<and> b = f a" by blast
   4.226 +      thus ?thesis using 2 0 by force
   4.227 +    next
   4.228 +      assume Case2: "b \<notin> f ` A'"
   4.229 +      hence "g b \<notin> A'" using 1 * by auto
   4.230 +      hence 4: "g b \<in> A - A'" using * SUB2 by auto
   4.231 +      hence "h(g b) \<in> B \<and> g(h(g b)) = g b"
   4.232 +      using 3 by auto
   4.233 +      hence "h(g b) = b" using * INJ2 unfolding inj_on_def by auto
   4.234 +      thus ?thesis using 4 by force
   4.235 +    qed
   4.236 +  qed
   4.237 +  (*  *)
   4.238 +  ultimately show ?thesis unfolding bij_betw_def by auto
   4.239 +qed
   4.240  
   4.241  subsection {*Other Consequences of Hilbert's Epsilon*}
   4.242  
     5.1 --- a/src/HOL/Lattice/Orders.thy	Fri Nov 26 09:15:49 2010 +0100
     5.2 +++ b/src/HOL/Lattice/Orders.thy	Fri Nov 26 10:04:04 2010 +0100
     5.3 @@ -118,8 +118,8 @@
     5.4    qed
     5.5  qed
     5.6  
     5.7 -lemma range_dual [simp]: "dual ` UNIV = UNIV"
     5.8 -proof (rule surj_range)
     5.9 +lemma range_dual [simp]: "surj dual"
    5.10 +proof -
    5.11    have "\<And>x'. dual (undual x') = x'" by simp
    5.12    thus "surj dual" by (rule surjI)
    5.13  qed
     6.1 --- a/src/HOL/Library/ContNotDenum.thy	Fri Nov 26 09:15:49 2010 +0100
     6.2 +++ b/src/HOL/Library/ContNotDenum.thy	Fri Nov 26 10:04:04 2010 +0100
     6.3 @@ -565,8 +565,7 @@
     6.4    shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
     6.5  proof -- "by contradiction"
     6.6    assume "\<exists>f::nat\<Rightarrow>real. surj f"
     6.7 -  then obtain f::"nat\<Rightarrow>real" where "surj f" by auto
     6.8 -  hence rangeF: "range f = UNIV" by (rule surj_range)
     6.9 +  then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto
    6.10    -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
    6.11    have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
    6.12    moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
     7.1 --- a/src/HOL/Library/Countable.thy	Fri Nov 26 09:15:49 2010 +0100
     7.2 +++ b/src/HOL/Library/Countable.thy	Fri Nov 26 10:04:04 2010 +0100
     7.3 @@ -165,7 +165,7 @@
     7.4  qed
     7.5  
     7.6  lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj"
     7.7 -by (simp add: Rats_def surj_nat_to_rat_surj surj_range)
     7.8 +by (simp add: Rats_def surj_nat_to_rat_surj)
     7.9  
    7.10  context field_char_0
    7.11  begin
     8.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Nov 26 09:15:49 2010 +0100
     8.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Nov 26 10:04:04 2010 +0100
     8.3 @@ -948,14 +948,12 @@
     8.4     assumes lf: "linear f" and gf: "f o g = id"
     8.5     shows "linear g"
     8.6   proof-
     8.7 -   from gf have fi: "surj f" apply (auto simp add: surj_def o_def id_def fun_eq_iff)
     8.8 -     by metis 
     8.9 +   from gf have fi: "surj f" by (auto simp add: surj_def o_def id_def) metis
    8.10     from linear_surjective_isomorphism[OF lf fi]
    8.11     obtain h:: "'a => 'a" where
    8.12       h: "linear h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x" by blast
    8.13     have "h = g" apply (rule ext) using gf h(2,3)
    8.14 -     apply (simp add: o_def id_def fun_eq_iff)
    8.15 -     by metis
    8.16 +     by (simp add: o_def id_def fun_eq_iff) metis
    8.17     with h(1) show ?thesis by blast
    8.18   qed
    8.19   
     9.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Fri Nov 26 09:15:49 2010 +0100
     9.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Fri Nov 26 10:04:04 2010 +0100
     9.3 @@ -2843,7 +2843,7 @@
     9.4      h: "linear h" "\<forall> x\<in> basis ` {..<DIM('b)}. h x = inv f x" by blast
     9.5    from h(2)
     9.6    have th: "\<forall>i<DIM('b). (f o h) (basis i) = id (basis i)"
     9.7 -    using sf by(auto simp add: surj_iff o_def fun_eq_iff)
     9.8 +    using sf by(auto simp add: surj_iff_all)
     9.9    from linear_eq_stdbasis[OF linear_compose[OF h(1) lf] linear_id th]
    9.10    have "f o h = id" .
    9.11    then show ?thesis using h(1) by blast
    9.12 @@ -2995,7 +2995,7 @@
    9.13    {fix f f':: "'a => 'a"
    9.14      assume lf: "linear f" "linear f'" and f: "f o f' = id"
    9.15      from f have sf: "surj f"
    9.16 -      apply (auto simp add: o_def fun_eq_iff id_def surj_def)
    9.17 +      apply (auto simp add: o_def id_def surj_def)
    9.18        by metis
    9.19      from linear_surjective_isomorphism[OF lf(1) sf] lf f
    9.20      have "f' o f = id" unfolding fun_eq_iff o_def id_def
    10.1 --- a/src/HOL/Nominal/Examples/Support.thy	Fri Nov 26 09:15:49 2010 +0100
    10.2 +++ b/src/HOL/Nominal/Examples/Support.thy	Fri Nov 26 10:04:04 2010 +0100
    10.3 @@ -47,7 +47,7 @@
    10.4    also have "\<dots> = (\<lambda>n. atom n) ` ({n. \<exists>i. n = 2*i \<or> n = 2*i+1})" by auto
    10.5    also have "\<dots> = (\<lambda>n. atom n) ` (UNIV::nat set)" using even_or_odd by auto
    10.6    also have "\<dots> = (UNIV::atom set)" using atom.exhaust
    10.7 -    by (rule_tac  surj_range) (auto simp add: surj_def)
    10.8 +    by (auto simp add: surj_def)
    10.9    finally show "EVEN \<union> ODD = UNIV" by simp
   10.10  qed
   10.11  
    11.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Fri Nov 26 09:15:49 2010 +0100
    11.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri Nov 26 10:04:04 2010 +0100
    11.3 @@ -132,7 +132,7 @@
    11.4        by (auto intro!: exI[of _ "from_nat i"])
    11.5    qed
    11.6    have **: "range ?A' = range A"
    11.7 -    using surj_range[OF surj_from_nat]
    11.8 +    using surj_from_nat
    11.9      by (auto simp: image_compose intro!: imageI)
   11.10    show ?thesis unfolding * ** ..
   11.11  qed
    12.1 --- a/src/HOL/Product_Type.thy	Fri Nov 26 09:15:49 2010 +0100
    12.2 +++ b/src/HOL/Product_Type.thy	Fri Nov 26 10:04:04 2010 +0100
    12.3 @@ -1135,6 +1135,7 @@
    12.4  qed
    12.5  
    12.6  lemma map_pair_surj:
    12.7 +  fixes f :: "'a \<Rightarrow> 'b" and g :: "'c \<Rightarrow> 'd"
    12.8    assumes "surj f" and "surj g"
    12.9    shows "surj (map_pair f g)"
   12.10  unfolding surj_def
    13.1 --- a/src/HOL/Set.thy	Fri Nov 26 09:15:49 2010 +0100
    13.2 +++ b/src/HOL/Set.thy	Fri Nov 26 10:04:04 2010 +0100
    13.3 @@ -622,6 +622,8 @@
    13.4  lemma Pow_top: "A \<in> Pow A"
    13.5    by simp
    13.6  
    13.7 +lemma Pow_not_empty: "Pow A \<noteq> {}"
    13.8 +  using Pow_top by blast
    13.9  
   13.10  subsubsection {* Set complement *}
   13.11  
   13.12 @@ -972,6 +974,21 @@
   13.13  lemmas [symmetric, rulify] = atomize_ball
   13.14    and [symmetric, defn] = atomize_ball
   13.15  
   13.16 +lemma image_Pow_mono:
   13.17 +  assumes "f ` A \<le> B"
   13.18 +  shows "(image f) ` (Pow A) \<le> Pow B"
   13.19 +using assms by blast
   13.20 +
   13.21 +lemma image_Pow_surj:
   13.22 +  assumes "f ` A = B"
   13.23 +  shows "(image f) ` (Pow A) = Pow B"
   13.24 +using assms unfolding Pow_def proof(auto)
   13.25 +  fix Y assume *: "Y \<le> f ` A"
   13.26 +  obtain X where X_def: "X = {x \<in> A. f x \<in> Y}" by blast
   13.27 +  have "f ` X = Y \<and> X \<le> A" unfolding X_def using * by auto
   13.28 +  thus "Y \<in> (image f) ` {X. X \<le> A}" by blast
   13.29 +qed
   13.30 +
   13.31  subsubsection {* Derived rules involving subsets. *}
   13.32  
   13.33  text {* @{text insert}. *}
    14.1 --- a/src/HOL/SetInterval.thy	Fri Nov 26 09:15:49 2010 +0100
    14.2 +++ b/src/HOL/SetInterval.thy	Fri Nov 26 10:04:04 2010 +0100
    14.3 @@ -159,6 +159,10 @@
    14.4   apply simp_all
    14.5  done
    14.6  
    14.7 +lemma lessThan_strict_subset_iff:
    14.8 +  fixes m n :: "'a::linorder"
    14.9 +  shows "{..<m} < {..<n} \<longleftrightarrow> m < n"
   14.10 +  by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq)
   14.11  
   14.12  subsection {*Two-sided intervals*}
   14.13  
   14.14 @@ -262,6 +266,18 @@
   14.15  apply (simp add: less_imp_le)
   14.16  done
   14.17  
   14.18 +lemma atLeastLessThan_inj:
   14.19 +  fixes a b c d :: "'a::linorder"
   14.20 +  assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d"
   14.21 +  shows "a = c" "b = d"
   14.22 +using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le linorder_antisym_conv2 subset_refl)+
   14.23 +
   14.24 +lemma atLeastLessThan_eq_iff:
   14.25 +  fixes a b c d :: "'a::linorder"
   14.26 +  assumes "a < b" "c < d"
   14.27 +  shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d"
   14.28 +  using atLeastLessThan_inj assms by auto
   14.29 +
   14.30  subsubsection {* Intersection *}
   14.31  
   14.32  context linorder
   14.33 @@ -705,6 +721,39 @@
   14.34    "finite M \<Longrightarrow> \<exists>h. bij_betw h {1 .. card M} M"
   14.35  by (rule finite_same_card_bij) auto
   14.36  
   14.37 +lemma bij_betw_iff_card:
   14.38 +  assumes FIN: "finite A" and FIN': "finite B"
   14.39 +  shows BIJ: "(\<exists>f. bij_betw f A B) \<longleftrightarrow> (card A = card B)"
   14.40 +using assms
   14.41 +proof(auto simp add: bij_betw_same_card)
   14.42 +  assume *: "card A = card B"
   14.43 +  obtain f where "bij_betw f A {0 ..< card A}"
   14.44 +  using FIN ex_bij_betw_finite_nat by blast
   14.45 +  moreover obtain g where "bij_betw g {0 ..< card B} B"
   14.46 +  using FIN' ex_bij_betw_nat_finite by blast
   14.47 +  ultimately have "bij_betw (g o f) A B"
   14.48 +  using * by (auto simp add: bij_betw_trans)
   14.49 +  thus "(\<exists>f. bij_betw f A B)" by blast
   14.50 +qed
   14.51 +
   14.52 +lemma inj_on_iff_card_le:
   14.53 +  assumes FIN: "finite A" and FIN': "finite B"
   14.54 +  shows "(\<exists>f. inj_on f A \<and> f ` A \<le> B) = (card A \<le> card B)"
   14.55 +proof (safe intro!: card_inj_on_le)
   14.56 +  assume *: "card A \<le> card B"
   14.57 +  obtain f where 1: "inj_on f A" and 2: "f ` A = {0 ..< card A}"
   14.58 +  using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force
   14.59 +  moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g ` {0 ..< card B} = B"
   14.60 +  using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force
   14.61 +  ultimately have "inj_on g (f ` A)" using subset_inj_on[of g _ "f ` A"] * by force
   14.62 +  hence "inj_on (g o f) A" using 1 comp_inj_on by blast
   14.63 +  moreover
   14.64 +  {have "{0 ..< card A} \<le> {0 ..< card B}" using * by force
   14.65 +   with 2 have "f ` A  \<le> {0 ..< card B}" by blast
   14.66 +   hence "(g o f) ` A \<le> B" unfolding comp_def using 3 by force
   14.67 +  }
   14.68 +  ultimately show "(\<exists>f. inj_on f A \<and> f ` A \<le> B)" by blast
   14.69 +qed (insert assms, auto)
   14.70  
   14.71  subsection {* Intervals of integers *}
   14.72  
    15.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Fri Nov 26 09:15:49 2010 +0100
    15.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Fri Nov 26 10:04:04 2010 +0100
    15.3 @@ -358,7 +358,7 @@
    15.4    done
    15.5  
    15.6  lemma surj_sysOfAlloc [iff]: "surj sysOfAlloc"
    15.7 -  apply (simp add: surj_iff fun_eq_iff o_apply)
    15.8 +  apply (simp add: surj_iff_all)
    15.9    apply record_auto
   15.10    done
   15.11  
   15.12 @@ -386,7 +386,7 @@
   15.13    done
   15.14  
   15.15  lemma surj_sysOfClient [iff]: "surj sysOfClient"
   15.16 -  apply (simp add: surj_iff fun_eq_iff o_apply)
   15.17 +  apply (simp add: surj_iff_all)
   15.18    apply record_auto
   15.19    done
   15.20  
   15.21 @@ -410,7 +410,7 @@
   15.22    done
   15.23  
   15.24  lemma surj_client_map [iff]: "surj client_map"
   15.25 -  apply (simp add: surj_iff fun_eq_iff o_apply)
   15.26 +  apply (simp add: surj_iff_all)
   15.27    apply record_auto
   15.28    done
   15.29  
   15.30 @@ -682,7 +682,7 @@
   15.31  lemma fst_lift_map_eq_fst [simp]: "fst (lift_map i x) i = fst x"
   15.32  apply (insert fst_o_lift_map [of i])
   15.33  apply (drule fun_cong [where x=x])
   15.34 -apply (simp add: o_def);
   15.35 +apply (simp add: o_def)
   15.36  done
   15.37  
   15.38  lemma fst_o_lift_map' [simp]:
   15.39 @@ -702,7 +702,7 @@
   15.40    RS guarantees_PLam_I
   15.41    RS (bij_sysOfClient RS rename_rename_guarantees_eq RS iffD2)
   15.42    |> simplify (simpset() addsimps [lift_image_eq_rename, o_def, split_def,
   15.43 -                                   surj_rename RS surj_range])
   15.44 +                                   surj_rename])
   15.45  
   15.46  However, the "preserves" property remains to be discharged, and the unfolding
   15.47  of "o" and "sub" complicates subsequent reasoning.
   15.48 @@ -723,7 +723,7 @@
   15.49      asm_simp_tac
   15.50          (ss addsimps [@{thm lift_guarantees_eq_lift_inv},
   15.51                        @{thm rename_guarantees_eq_rename_inv},
   15.52 -                      @{thm bij_imp_bij_inv}, @{thm surj_rename} RS @{thm surj_range},
   15.53 +                      @{thm bij_imp_bij_inv}, @{thm surj_rename},
   15.54                        @{thm inv_inv_eq}]) 1,
   15.55      asm_simp_tac
   15.56          (@{simpset} addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1]
   15.57 @@ -798,9 +798,9 @@
   15.58  lemmas rename_Alloc_Increasing =
   15.59    Alloc_Increasing
   15.60      [THEN rename_guarantees_sysOfAlloc_I,
   15.61 -     simplified surj_rename [THEN surj_range] o_def sub_apply
   15.62 +     simplified surj_rename o_def sub_apply
   15.63                  rename_image_Increasing bij_sysOfAlloc
   15.64 -                allocGiv_o_inv_sysOfAlloc_eq'];
   15.65 +                allocGiv_o_inv_sysOfAlloc_eq']
   15.66  
   15.67  lemma System_Increasing_allocGiv:
   15.68       "i < Nclients ==> System : Increasing (sub i o allocGiv)"
   15.69 @@ -879,7 +879,7 @@
   15.70              \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel) s)}"
   15.71    apply (simp add: o_apply)
   15.72    apply (insert Alloc_Safety [THEN rename_guarantees_sysOfAlloc_I])
   15.73 -  apply (simp add: o_def);
   15.74 +  apply (simp add: o_def)
   15.75    apply (erule component_guaranteesD)
   15.76    apply (auto simp add: System_Increasing_allocRel [simplified sub_apply o_def])
   15.77    done
    16.1 --- a/src/HOL/UNITY/Extend.thy	Fri Nov 26 09:15:49 2010 +0100
    16.2 +++ b/src/HOL/UNITY/Extend.thy	Fri Nov 26 10:04:04 2010 +0100
    16.3 @@ -127,7 +127,7 @@
    16.4       assumes surj_h: "surj h"
    16.5           and prem:   "!! x y. g (h(x,y)) = x"
    16.6       shows "fst (inv h z) = g z"
    16.7 -by (metis UNIV_I f_inv_into_f pair_collapse prem surj_h surj_range)
    16.8 +by (metis UNIV_I f_inv_into_f pair_collapse prem surj_h)
    16.9  
   16.10  
   16.11  subsection{*Trivial properties of f, g, h*}
    17.1 --- a/src/HOL/UNITY/Rename.thy	Fri Nov 26 09:15:49 2010 +0100
    17.2 +++ b/src/HOL/UNITY/Rename.thy	Fri Nov 26 10:04:04 2010 +0100
    17.3 @@ -60,7 +60,8 @@
    17.4  lemma bij_extend_act: "bij h ==> bij (extend_act (%(x,u::'c). h x))"
    17.5  apply (rule bijI)
    17.6  apply (rule Extend.inj_extend_act)
    17.7 -apply (auto simp add: bij_extend_act_eq_project_act)
    17.8 +apply simp
    17.9 +apply (simp add: bij_extend_act_eq_project_act)
   17.10  apply (rule surjI)
   17.11  apply (rule Extend.extend_act_inverse)
   17.12  apply (blast intro: bij_imp_bij_inv good_map_bij)
   17.13 @@ -75,7 +76,7 @@
   17.14                  project_act (%(x,u::'c). h x)"
   17.15  apply (simp (no_asm_simp) add: bij_extend_act_eq_project_act [symmetric])
   17.16  apply (rule surj_imp_inv_eq)
   17.17 -apply (blast intro: bij_extend_act bij_is_surj)
   17.18 +apply (blast intro!: bij_extend_act bij_is_surj)
   17.19  apply (simp (no_asm_simp) add: Extend.extend_act_inverse)
   17.20  done
   17.21