--- a/NEWS Fri Nov 26 09:15:49 2010 +0100
+++ b/NEWS Fri Nov 26 10:04:04 2010 +0100
@@ -291,9 +291,10 @@
derive instantiated and simplified equations for inductive predicates,
similar to inductive_cases.
-* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". surj_on is a
-generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV".
-The theorems bij_def and surj_def are unchanged.
+* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". "surj f" is now an
+abbreviation of "range f = UIV". The theorems bij_def and surj_def are
+unchanged.
+INCOMPATIBILITY.
* Function package: .psimps rules are no longer implicitly declared [simp].
INCOMPATIBILITY.
--- a/src/HOL/Finite_Set.thy Fri Nov 26 09:15:49 2010 +0100
+++ b/src/HOL/Finite_Set.thy Fri Nov 26 10:04:04 2010 +0100
@@ -2179,6 +2179,11 @@
finite A; finite B |] ==> card A = card B"
by (auto intro: le_antisym card_inj_on_le)
+lemma bij_betw_finite:
+ assumes "bij_betw f A B"
+ shows "finite A \<longleftrightarrow> finite B"
+using assms unfolding bij_betw_def
+using finite_imageD[of f A] by auto
subsubsection {* Pigeonhole Principles *}
@@ -2286,7 +2291,7 @@
lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
-by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
+by (blast intro: finite_surj_inj subset_UNIV)
lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
--- a/src/HOL/Fun.thy Fri Nov 26 09:15:49 2010 +0100
+++ b/src/HOL/Fun.thy Fri Nov 26 10:04:04 2010 +0100
@@ -130,24 +130,22 @@
by (simp_all add: fun_eq_iff)
-subsection {* Injectivity, Surjectivity and Bijectivity *}
+subsection {* Injectivity and Bijectivity *}
definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" where -- "injective"
"inj_on f A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y)"
-definition surj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> bool" where -- "surjective"
- "surj_on f B \<longleftrightarrow> B \<subseteq> range f"
-
definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" where -- "bijective"
"bij_betw f A B \<longleftrightarrow> inj_on f A \<and> f ` A = B"
-text{*A common special case: functions injective over the entire domain type.*}
+text{*A common special case: functions injective, surjective or bijective over
+the entire domain type.*}
abbreviation
"inj f \<equiv> inj_on f UNIV"
-abbreviation
- "surj f \<equiv> surj_on f UNIV"
+abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" where -- "surjective"
+ "surj f \<equiv> (range f = UNIV)"
abbreviation
"bij f \<equiv> bij_betw f UNIV UNIV"
@@ -171,6 +169,14 @@
lemma inj_on_eq_iff: "inj_on f A ==> x:A ==> y:A ==> (f(x) = f(y)) = (x=y)"
by (force simp add: inj_on_def)
+lemma inj_on_cong:
+ "(\<And> a. a : A \<Longrightarrow> f a = g a) \<Longrightarrow> inj_on f A = inj_on g A"
+unfolding inj_on_def by auto
+
+lemma inj_on_strict_subset:
+ "\<lbrakk> inj_on f B; A < B \<rbrakk> \<Longrightarrow> f`A < f`B"
+unfolding inj_on_def unfolding image_def by blast
+
lemma inj_comp:
"inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
by (simp add: inj_on_def)
@@ -187,8 +193,44 @@
lemma inj_on_id2[simp]: "inj_on (%x. x) A"
by (simp add: inj_on_def)
-lemma surj_id[simp]: "surj_on id A"
-by (simp add: surj_on_def)
+lemma inj_on_Int: "\<lbrakk>inj_on f A; inj_on f B\<rbrakk> \<Longrightarrow> inj_on f (A \<inter> B)"
+unfolding inj_on_def by blast
+
+lemma inj_on_INTER:
+ "\<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)"
+unfolding inj_on_def by blast
+
+lemma inj_on_Inter:
+ "\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> inj_on f A\<rbrakk> \<Longrightarrow> inj_on f (Inter S)"
+unfolding inj_on_def by blast
+
+lemma inj_on_UNION_chain:
+ 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
+ INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
+ shows "inj_on f (\<Union> i \<in> I. A i)"
+proof(unfold inj_on_def UNION_def, auto)
+ fix i j x y
+ assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
+ and ***: "f x = f y"
+ show "x = y"
+ proof-
+ {assume "A i \<le> A j"
+ with ** have "x \<in> A j" by auto
+ with INJ * ** *** have ?thesis
+ by(auto simp add: inj_on_def)
+ }
+ moreover
+ {assume "A j \<le> A i"
+ with ** have "y \<in> A i" by auto
+ with INJ * ** *** have ?thesis
+ by(auto simp add: inj_on_def)
+ }
+ ultimately show ?thesis using CH * by blast
+ qed
+qed
+
+lemma surj_id: "surj id"
+by simp
lemma bij_id[simp]: "bij id"
by (simp add: bij_betw_def)
@@ -251,20 +293,19 @@
apply (blast)
done
-lemma surj_onI: "(\<And>x. x \<in> B \<Longrightarrow> g (f x) = x) \<Longrightarrow> surj_on g B"
- by (simp add: surj_on_def) (blast intro: sym)
+lemma comp_inj_on_iff:
+ "inj_on f A \<Longrightarrow> inj_on f' (f ` A) \<longleftrightarrow> inj_on (f' o f) A"
+by(auto simp add: comp_inj_on inj_on_def)
-lemma surj_onD: "surj_on f B \<Longrightarrow> y \<in> B \<Longrightarrow> \<exists>x. y = f x"
- by (auto simp: surj_on_def)
-
-lemma surj_on_range_iff: "surj_on f B \<longleftrightarrow> (\<exists>A. f ` A = B)"
- unfolding surj_on_def by (auto intro!: exI[of _ "f -` B"])
+lemma inj_on_imageI2:
+ "inj_on (f' o f) A \<Longrightarrow> inj_on f A"
+by(auto simp add: comp_inj_on inj_on_def)
lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
- by (simp add: surj_on_def subset_eq image_iff)
+ by auto
-lemma surjI: "(\<And> x. g (f x) = x) \<Longrightarrow> surj g"
- by (blast intro: surj_onI)
+lemma surjI: assumes *: "\<And> x. g (f x) = x" shows "surj g"
+ using *[symmetric] by auto
lemma surjD: "surj f \<Longrightarrow> \<exists>x. y = f x"
by (simp add: surj_def)
@@ -278,17 +319,25 @@
apply (drule_tac x = x in spec, blast)
done
-lemma surj_range: "surj f \<Longrightarrow> range f = UNIV"
- by (auto simp add: surj_on_def)
+lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
+ unfolding bij_betw_def by auto
+
+lemma bij_betw_empty1:
+ assumes "bij_betw f {} A"
+ shows "A = {}"
+using assms unfolding bij_betw_def by blast
-lemma surj_range_iff: "surj f \<longleftrightarrow> range f = UNIV"
- unfolding surj_on_def by auto
+lemma bij_betw_empty2:
+ assumes "bij_betw f A {}"
+ shows "A = {}"
+using assms unfolding bij_betw_def by blast
-lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
- unfolding bij_betw_def surj_range_iff by auto
+lemma inj_on_imp_bij_betw:
+ "inj_on f A \<Longrightarrow> bij_betw f A (f ` A)"
+unfolding bij_betw_def by simp
lemma bij_def: "bij f \<longleftrightarrow> inj f \<and> surj f"
- unfolding surj_range_iff bij_betw_def ..
+ unfolding bij_betw_def ..
lemma bijI: "[| inj f; surj f |] ==> bij f"
by (simp add: bij_def)
@@ -302,16 +351,39 @@
lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
by (simp add: bij_betw_def)
-lemma bij_betw_imp_surj_on: "bij_betw f A B \<Longrightarrow> surj_on f B"
-by (auto simp: bij_betw_def surj_on_range_iff)
-
-lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
-by(fastsimp intro: comp_inj_on comp_surj simp: bij_def surj_range)
-
lemma bij_betw_trans:
"bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g o f) A C"
by(auto simp add:bij_betw_def comp_inj_on)
+lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
+ by (rule bij_betw_trans)
+
+lemma bij_betw_comp_iff:
+ "bij_betw f A A' \<Longrightarrow> bij_betw f' A' A'' \<longleftrightarrow> bij_betw (f' o f) A A''"
+by(auto simp add: bij_betw_def inj_on_def)
+
+lemma bij_betw_comp_iff2:
+ assumes BIJ: "bij_betw f' A' A''" and IM: "f ` A \<le> A'"
+ shows "bij_betw f A A' \<longleftrightarrow> bij_betw (f' o f) A A''"
+using assms
+proof(auto simp add: bij_betw_comp_iff)
+ assume *: "bij_betw (f' \<circ> f) A A''"
+ thus "bij_betw f A A'"
+ using IM
+ proof(auto simp add: bij_betw_def)
+ assume "inj_on (f' \<circ> f) A"
+ thus "inj_on f A" using inj_on_imageI2 by blast
+ next
+ fix a' assume **: "a' \<in> A'"
+ hence "f' a' \<in> A''" using BIJ unfolding bij_betw_def by auto
+ then obtain a where 1: "a \<in> A \<and> f'(f a) = f' a'" using *
+ unfolding bij_betw_def by force
+ hence "f a \<in> A'" using IM by auto
+ hence "f a = a'" using BIJ ** 1 unfolding bij_betw_def inj_on_def by auto
+ thus "a' \<in> f ` A" using 1 by auto
+ qed
+qed
+
lemma bij_betw_inv: assumes "bij_betw f A B" shows "EX g. bij_betw g B A"
proof -
have i: "inj_on f A" and s: "f ` A = B"
@@ -343,21 +415,81 @@
ultimately show ?thesis by(auto simp:bij_betw_def)
qed
+lemma bij_betw_cong:
+ "(\<And> a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> bij_betw f A A' = bij_betw g A A'"
+unfolding bij_betw_def inj_on_def by force
+
+lemma bij_betw_id[intro, simp]:
+ "bij_betw id A A"
+unfolding bij_betw_def id_def by auto
+
+lemma bij_betw_id_iff:
+ "bij_betw id A B \<longleftrightarrow> A = B"
+by(auto simp add: bij_betw_def)
+
lemma bij_betw_combine:
assumes "bij_betw f A B" "bij_betw f C D" "B \<inter> D = {}"
shows "bij_betw f (A \<union> C) (B \<union> D)"
using assms unfolding bij_betw_def inj_on_Un image_Un by auto
+lemma bij_betw_UNION_chain:
+ 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
+ BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
+ shows "bij_betw f (\<Union> i \<in> I. A i) (\<Union> i \<in> I. A' i)"
+proof(unfold bij_betw_def, auto simp add: image_def)
+ have "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
+ using BIJ bij_betw_def[of f] by auto
+ thus "inj_on f (\<Union> i \<in> I. A i)"
+ using CH inj_on_UNION_chain[of I A f] by auto
+next
+ fix i x
+ assume *: "i \<in> I" "x \<in> A i"
+ hence "f x \<in> A' i" using BIJ bij_betw_def[of f] by auto
+ thus "\<exists>j \<in> I. f x \<in> A' j" using * by blast
+next
+ fix i x'
+ assume *: "i \<in> I" "x' \<in> A' i"
+ hence "\<exists>x \<in> A i. x' = f x" using BIJ bij_betw_def[of f] by blast
+ thus "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
+ using * by blast
+qed
+
+lemma bij_betw_Disj_Un:
+ assumes DISJ: "A \<inter> B = {}" and DISJ': "A' \<inter> B' = {}" and
+ B1: "bij_betw f A A'" and B2: "bij_betw f B B'"
+ shows "bij_betw f (A \<union> B) (A' \<union> B')"
+proof-
+ have 1: "inj_on f A \<and> inj_on f B"
+ using B1 B2 by (auto simp add: bij_betw_def)
+ have 2: "f`A = A' \<and> f`B = B'"
+ using B1 B2 by (auto simp add: bij_betw_def)
+ hence "f`(A - B) \<inter> f`(B - A) = {}"
+ using DISJ DISJ' by blast
+ hence "inj_on f (A \<union> B)"
+ using 1 by (auto simp add: inj_on_Un)
+ (* *)
+ moreover
+ have "f`(A \<union> B) = A' \<union> B'"
+ using 2 by auto
+ ultimately show ?thesis
+ unfolding bij_betw_def by auto
+qed
+
+lemma bij_betw_subset:
+ assumes BIJ: "bij_betw f A A'" and
+ SUB: "B \<le> A" and IM: "f ` B = B'"
+ shows "bij_betw f B B'"
+using assms
+by(unfold bij_betw_def inj_on_def, auto simp add: inj_on_def)
+
lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
-by (simp add: surj_range)
+by simp
lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
by (simp add: inj_on_def, blast)
lemma vimage_subsetD: "surj f ==> f -` B <= A ==> B <= f ` A"
-apply (unfold surj_def)
-apply (blast intro: sym)
-done
+by (blast intro: sym)
lemma vimage_subsetI: "inj f ==> B <= f ` A ==> f -` B <= A"
by (unfold inj_on_def, blast)
@@ -410,7 +542,7 @@
done
lemma surj_Compl_image_subset: "surj f ==> -(f`A) <= f`(-A)"
-by (auto simp add: surj_def)
+by auto
lemma inj_image_Compl_subset: "inj f ==> f`(-A) <= -(f`A)"
by (auto simp add: inj_on_def)
@@ -559,10 +691,10 @@
qed
lemma surj_imp_surj_swap: "surj f \<Longrightarrow> surj (swap a b f)"
- unfolding surj_range_iff by simp
+ by simp
lemma surj_swap_iff [simp]: "surj (swap a b f) \<longleftrightarrow> surj f"
- unfolding surj_range_iff by simp
+ by simp
lemma bij_betw_swap_iff [simp]:
"\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> bij_betw (swap x y f) A B \<longleftrightarrow> bij_betw f A B"
@@ -635,6 +767,17 @@
shows "the_inv f (f x) = x" using assms UNIV_I
by (rule the_inv_into_f_f)
+subsection {* Cantor's Paradox *}
+
+lemma Cantors_paradox:
+ "\<not>(\<exists>f. f ` A = Pow A)"
+proof clarify
+ fix f assume "f ` A = Pow A" hence *: "Pow A \<le> f ` A" by blast
+ let ?X = "{a \<in> A. a \<notin> f a}"
+ have "?X \<in> Pow A" unfolding Pow_def by auto
+ with * obtain x where "x \<in> A \<and> f x = ?X" by blast
+ thus False by best
+qed
subsection {* Proof tool setup *}
--- a/src/HOL/Hilbert_Choice.thy Fri Nov 26 09:15:49 2010 +0100
+++ b/src/HOL/Hilbert_Choice.thy Fri Nov 26 10:04:04 2010 +0100
@@ -151,10 +151,10 @@
by(fastsimp simp: image_def)
lemma inj_imp_surj_inv: "inj f ==> surj (inv f)"
-by (blast intro: surjI inv_into_f_f)
+by (blast intro!: surjI inv_into_f_f)
lemma surj_f_inv_f: "surj f ==> f(inv f y) = y"
-by (simp add: f_inv_into_f surj_range)
+by (simp add: f_inv_into_f)
lemma inv_into_injective:
assumes eq: "inv_into A f x = inv_into A f y"
@@ -173,12 +173,13 @@
by (auto simp add: bij_betw_def inj_on_inv_into)
lemma surj_imp_inj_inv: "surj f ==> inj (inv f)"
-by (simp add: inj_on_inv_into surj_range)
+by (simp add: inj_on_inv_into)
lemma surj_iff: "(surj f) = (f o inv f = id)"
-apply (simp add: o_def fun_eq_iff)
-apply (blast intro: surjI surj_f_inv_f)
-done
+by (auto intro!: surjI simp: surj_f_inv_f fun_eq_iff[where 'b='a])
+
+lemma surj_iff_all: "surj f \<longleftrightarrow> (\<forall>x. f (inv f x) = x)"
+ unfolding surj_iff by (simp add: o_def fun_eq_iff)
lemma surj_imp_inv_eq: "[| surj f; \<forall>x. g(f x) = x |] ==> inv f = g"
apply (rule ext)
@@ -260,6 +261,208 @@
ultimately show "finite (UNIV :: 'a set)" by simp
qed
+lemma image_inv_into_cancel:
+ assumes SURJ: "f`A=A'" and SUB: "B' \<le> A'"
+ shows "f `((inv_into A f)`B') = B'"
+ using assms
+proof (auto simp add: f_inv_into_f)
+ let ?f' = "(inv_into A f)"
+ fix a' assume *: "a' \<in> B'"
+ then have "a' \<in> A'" using SUB by auto
+ then have "a' = f (?f' a')"
+ using SURJ by (auto simp add: f_inv_into_f)
+ then show "a' \<in> f ` (?f' ` B')" using * by blast
+qed
+
+lemma inv_into_inv_into_eq:
+ assumes "bij_betw f A A'" "a \<in> A"
+ shows "inv_into A' (inv_into A f) a = f a"
+proof -
+ let ?f' = "inv_into A f" let ?f'' = "inv_into A' ?f'"
+ have 1: "bij_betw ?f' A' A" using assms
+ by (auto simp add: bij_betw_inv_into)
+ obtain a' where 2: "a' \<in> A'" and 3: "?f' a' = a"
+ using 1 `a \<in> A` unfolding bij_betw_def by force
+ hence "?f'' a = a'"
+ using `a \<in> A` 1 3 by (auto simp add: f_inv_into_f bij_betw_def)
+ moreover have "f a = a'" using assms 2 3
+ by (auto simp add: inv_into_f_f bij_betw_def)
+ ultimately show "?f'' a = f a" by simp
+qed
+
+lemma inj_on_iff_surj:
+ assumes "A \<noteq> {}"
+ shows "(\<exists>f. inj_on f A \<and> f ` A \<le> A') \<longleftrightarrow> (\<exists>g. g ` A' = A)"
+proof safe
+ fix f assume INJ: "inj_on f A" and INCL: "f ` A \<le> A'"
+ let ?phi = "\<lambda>a' a. a \<in> A \<and> f a = a'" let ?csi = "\<lambda>a. a \<in> A"
+ let ?g = "\<lambda>a'. if a' \<in> f ` A then (SOME a. ?phi a' a) else (SOME a. ?csi a)"
+ have "?g ` A' = A"
+ proof
+ show "?g ` A' \<le> A"
+ proof clarify
+ fix a' assume *: "a' \<in> A'"
+ show "?g a' \<in> A"
+ proof cases
+ assume Case1: "a' \<in> f ` A"
+ then obtain a where "?phi a' a" by blast
+ hence "?phi a' (SOME a. ?phi a' a)" using someI[of "?phi a'" a] by blast
+ with Case1 show ?thesis by auto
+ next
+ assume Case2: "a' \<notin> f ` A"
+ hence "?csi (SOME a. ?csi a)" using assms someI_ex[of ?csi] by blast
+ with Case2 show ?thesis by auto
+ qed
+ qed
+ next
+ show "A \<le> ?g ` A'"
+ proof-
+ {fix a assume *: "a \<in> A"
+ let ?b = "SOME aa. ?phi (f a) aa"
+ have "?phi (f a) a" using * by auto
+ hence 1: "?phi (f a) ?b" using someI[of "?phi(f a)" a] by blast
+ hence "?g(f a) = ?b" using * by auto
+ moreover have "a = ?b" using 1 INJ * by (auto simp add: inj_on_def)
+ ultimately have "?g(f a) = a" by simp
+ with INCL * have "?g(f a) = a \<and> f a \<in> A'" by auto
+ }
+ thus ?thesis by force
+ qed
+ qed
+ thus "\<exists>g. g ` A' = A" by blast
+next
+ fix g let ?f = "inv_into A' g"
+ have "inj_on ?f (g ` A')"
+ by (auto simp add: inj_on_inv_into)
+ moreover
+ {fix a' assume *: "a' \<in> A'"
+ let ?phi = "\<lambda> b'. b' \<in> A' \<and> g b' = g a'"
+ have "?phi a'" using * by auto
+ hence "?phi(SOME b'. ?phi b')" using someI[of ?phi] by blast
+ hence "?f(g a') \<in> A'" unfolding inv_into_def by auto
+ }
+ ultimately show "\<exists>f. inj_on f (g ` A') \<and> f ` g ` A' \<subseteq> A'" by auto
+qed
+
+lemma Ex_inj_on_UNION_Sigma:
+ "\<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))"
+proof
+ let ?phi = "\<lambda> a i. i \<in> I \<and> a \<in> A i"
+ let ?sm = "\<lambda> a. SOME i. ?phi a i"
+ let ?f = "\<lambda>a. (?sm a, a)"
+ have "inj_on ?f (\<Union> i \<in> I. A i)" unfolding inj_on_def by auto
+ moreover
+ { { fix i a assume "i \<in> I" and "a \<in> A i"
+ hence "?sm a \<in> I \<and> a \<in> A(?sm a)" using someI[of "?phi a" i] by auto
+ }
+ hence "?f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i)" by auto
+ }
+ ultimately
+ show "inj_on ?f (\<Union> i \<in> I. A i) \<and> ?f ` (\<Union> i \<in> I. A i) \<le> (SIGMA i : I. A i)"
+ by auto
+qed
+
+subsection {* The Cantor-Bernstein Theorem *}
+
+lemma Cantor_Bernstein_aux:
+ shows "\<exists>A' h. A' \<le> A \<and>
+ (\<forall>a \<in> A'. a \<notin> g`(B - f ` A')) \<and>
+ (\<forall>a \<in> A'. h a = f a) \<and>
+ (\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g(h a))"
+proof-
+ obtain H where H_def: "H = (\<lambda> A'. A - (g`(B - (f ` A'))))" by blast
+ have 0: "mono H" unfolding mono_def H_def by blast
+ then obtain A' where 1: "H A' = A'" using lfp_unfold by blast
+ hence 2: "A' = A - (g`(B - (f ` A')))" unfolding H_def by simp
+ hence 3: "A' \<le> A" by blast
+ have 4: "\<forall>a \<in> A'. a \<notin> g`(B - f ` A')"
+ using 2 by blast
+ have 5: "\<forall>a \<in> A - A'. \<exists>b \<in> B - (f ` A'). a = g b"
+ using 2 by blast
+ (* *)
+ obtain h where h_def:
+ "h = (\<lambda> a. if a \<in> A' then f a else (SOME b. b \<in> B - (f ` A') \<and> a = g b))" by blast
+ hence "\<forall>a \<in> A'. h a = f a" by auto
+ moreover
+ have "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g(h a)"
+ proof
+ fix a assume *: "a \<in> A - A'"
+ let ?phi = "\<lambda> b. b \<in> B - (f ` A') \<and> a = g b"
+ have "h a = (SOME b. ?phi b)" using h_def * by auto
+ moreover have "\<exists>b. ?phi b" using 5 * by auto
+ ultimately show "?phi (h a)" using someI_ex[of ?phi] by auto
+ qed
+ ultimately show ?thesis using 3 4 by blast
+qed
+
+theorem Cantor_Bernstein:
+ assumes INJ1: "inj_on f A" and SUB1: "f ` A \<le> B" and
+ INJ2: "inj_on g B" and SUB2: "g ` B \<le> A"
+ shows "\<exists>h. bij_betw h A B"
+proof-
+ obtain A' and h where 0: "A' \<le> A" and
+ 1: "\<forall>a \<in> A'. a \<notin> g`(B - f ` A')" and
+ 2: "\<forall>a \<in> A'. h a = f a" and
+ 3: "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g(h a)"
+ using Cantor_Bernstein_aux[of A g B f] by blast
+ have "inj_on h A"
+ proof (intro inj_onI)
+ fix a1 a2
+ assume 4: "a1 \<in> A" and 5: "a2 \<in> A" and 6: "h a1 = h a2"
+ show "a1 = a2"
+ proof(cases "a1 \<in> A'")
+ assume Case1: "a1 \<in> A'"
+ show ?thesis
+ proof(cases "a2 \<in> A'")
+ assume Case11: "a2 \<in> A'"
+ hence "f a1 = f a2" using Case1 2 6 by auto
+ thus ?thesis using INJ1 Case1 Case11 0
+ unfolding inj_on_def by blast
+ next
+ assume Case12: "a2 \<notin> A'"
+ hence False using 3 5 2 6 Case1 by force
+ thus ?thesis by simp
+ qed
+ next
+ assume Case2: "a1 \<notin> A'"
+ show ?thesis
+ proof(cases "a2 \<in> A'")
+ assume Case21: "a2 \<in> A'"
+ hence False using 3 4 2 6 Case2 by auto
+ thus ?thesis by simp
+ next
+ assume Case22: "a2 \<notin> A'"
+ hence "a1 = g(h a1) \<and> a2 = g(h a2)" using Case2 4 5 3 by auto
+ thus ?thesis using 6 by simp
+ qed
+ qed
+ qed
+ (* *)
+ moreover
+ have "h ` A = B"
+ proof safe
+ fix a assume "a \<in> A"
+ thus "h a \<in> B" using SUB1 2 3 by (case_tac "a \<in> A'", auto)
+ next
+ fix b assume *: "b \<in> B"
+ show "b \<in> h ` A"
+ proof(cases "b \<in> f ` A'")
+ assume Case1: "b \<in> f ` A'"
+ then obtain a where "a \<in> A' \<and> b = f a" by blast
+ thus ?thesis using 2 0 by force
+ next
+ assume Case2: "b \<notin> f ` A'"
+ hence "g b \<notin> A'" using 1 * by auto
+ hence 4: "g b \<in> A - A'" using * SUB2 by auto
+ hence "h(g b) \<in> B \<and> g(h(g b)) = g b"
+ using 3 by auto
+ hence "h(g b) = b" using * INJ2 unfolding inj_on_def by auto
+ thus ?thesis using 4 by force
+ qed
+ qed
+ (* *)
+ ultimately show ?thesis unfolding bij_betw_def by auto
+qed
subsection {*Other Consequences of Hilbert's Epsilon*}
--- a/src/HOL/Lattice/Orders.thy Fri Nov 26 09:15:49 2010 +0100
+++ b/src/HOL/Lattice/Orders.thy Fri Nov 26 10:04:04 2010 +0100
@@ -118,8 +118,8 @@
qed
qed
-lemma range_dual [simp]: "dual ` UNIV = UNIV"
-proof (rule surj_range)
+lemma range_dual [simp]: "surj dual"
+proof -
have "\<And>x'. dual (undual x') = x'" by simp
thus "surj dual" by (rule surjI)
qed
--- a/src/HOL/Library/ContNotDenum.thy Fri Nov 26 09:15:49 2010 +0100
+++ b/src/HOL/Library/ContNotDenum.thy Fri Nov 26 10:04:04 2010 +0100
@@ -565,8 +565,7 @@
shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
proof -- "by contradiction"
assume "\<exists>f::nat\<Rightarrow>real. surj f"
- then obtain f::"nat\<Rightarrow>real" where "surj f" by auto
- hence rangeF: "range f = UNIV" by (rule surj_range)
+ then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto
-- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
--- a/src/HOL/Library/Countable.thy Fri Nov 26 09:15:49 2010 +0100
+++ b/src/HOL/Library/Countable.thy Fri Nov 26 10:04:04 2010 +0100
@@ -165,7 +165,7 @@
qed
lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj"
-by (simp add: Rats_def surj_nat_to_rat_surj surj_range)
+by (simp add: Rats_def surj_nat_to_rat_surj)
context field_char_0
begin
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri Nov 26 09:15:49 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Nov 26 10:04:04 2010 +0100
@@ -948,14 +948,12 @@
assumes lf: "linear f" and gf: "f o g = id"
shows "linear g"
proof-
- from gf have fi: "surj f" apply (auto simp add: surj_def o_def id_def fun_eq_iff)
- by metis
+ from gf have fi: "surj f" by (auto simp add: surj_def o_def id_def) metis
from linear_surjective_isomorphism[OF lf fi]
obtain h:: "'a => 'a" where
h: "linear h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x" by blast
have "h = g" apply (rule ext) using gf h(2,3)
- apply (simp add: o_def id_def fun_eq_iff)
- by metis
+ by (simp add: o_def id_def fun_eq_iff) metis
with h(1) show ?thesis by blast
qed
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Nov 26 09:15:49 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Nov 26 10:04:04 2010 +0100
@@ -2843,7 +2843,7 @@
h: "linear h" "\<forall> x\<in> basis ` {..<DIM('b)}. h x = inv f x" by blast
from h(2)
have th: "\<forall>i<DIM('b). (f o h) (basis i) = id (basis i)"
- using sf by(auto simp add: surj_iff o_def fun_eq_iff)
+ using sf by(auto simp add: surj_iff_all)
from linear_eq_stdbasis[OF linear_compose[OF h(1) lf] linear_id th]
have "f o h = id" .
then show ?thesis using h(1) by blast
@@ -2995,7 +2995,7 @@
{fix f f':: "'a => 'a"
assume lf: "linear f" "linear f'" and f: "f o f' = id"
from f have sf: "surj f"
- apply (auto simp add: o_def fun_eq_iff id_def surj_def)
+ apply (auto simp add: o_def id_def surj_def)
by metis
from linear_surjective_isomorphism[OF lf(1) sf] lf f
have "f' o f = id" unfolding fun_eq_iff o_def id_def
--- a/src/HOL/Nominal/Examples/Support.thy Fri Nov 26 09:15:49 2010 +0100
+++ b/src/HOL/Nominal/Examples/Support.thy Fri Nov 26 10:04:04 2010 +0100
@@ -47,7 +47,7 @@
also have "\<dots> = (\<lambda>n. atom n) ` ({n. \<exists>i. n = 2*i \<or> n = 2*i+1})" by auto
also have "\<dots> = (\<lambda>n. atom n) ` (UNIV::nat set)" using even_or_odd by auto
also have "\<dots> = (UNIV::atom set)" using atom.exhaust
- by (rule_tac surj_range) (auto simp add: surj_def)
+ by (auto simp add: surj_def)
finally show "EVEN \<union> ODD = UNIV" by simp
qed
--- a/src/HOL/Probability/Sigma_Algebra.thy Fri Nov 26 09:15:49 2010 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Fri Nov 26 10:04:04 2010 +0100
@@ -132,7 +132,7 @@
by (auto intro!: exI[of _ "from_nat i"])
qed
have **: "range ?A' = range A"
- using surj_range[OF surj_from_nat]
+ using surj_from_nat
by (auto simp: image_compose intro!: imageI)
show ?thesis unfolding * ** ..
qed
--- a/src/HOL/Product_Type.thy Fri Nov 26 09:15:49 2010 +0100
+++ b/src/HOL/Product_Type.thy Fri Nov 26 10:04:04 2010 +0100
@@ -1135,6 +1135,7 @@
qed
lemma map_pair_surj:
+ fixes f :: "'a \<Rightarrow> 'b" and g :: "'c \<Rightarrow> 'd"
assumes "surj f" and "surj g"
shows "surj (map_pair f g)"
unfolding surj_def
--- a/src/HOL/Set.thy Fri Nov 26 09:15:49 2010 +0100
+++ b/src/HOL/Set.thy Fri Nov 26 10:04:04 2010 +0100
@@ -622,6 +622,8 @@
lemma Pow_top: "A \<in> Pow A"
by simp
+lemma Pow_not_empty: "Pow A \<noteq> {}"
+ using Pow_top by blast
subsubsection {* Set complement *}
@@ -972,6 +974,21 @@
lemmas [symmetric, rulify] = atomize_ball
and [symmetric, defn] = atomize_ball
+lemma image_Pow_mono:
+ assumes "f ` A \<le> B"
+ shows "(image f) ` (Pow A) \<le> Pow B"
+using assms by blast
+
+lemma image_Pow_surj:
+ assumes "f ` A = B"
+ shows "(image f) ` (Pow A) = Pow B"
+using assms unfolding Pow_def proof(auto)
+ fix Y assume *: "Y \<le> f ` A"
+ obtain X where X_def: "X = {x \<in> A. f x \<in> Y}" by blast
+ have "f ` X = Y \<and> X \<le> A" unfolding X_def using * by auto
+ thus "Y \<in> (image f) ` {X. X \<le> A}" by blast
+qed
+
subsubsection {* Derived rules involving subsets. *}
text {* @{text insert}. *}
--- a/src/HOL/SetInterval.thy Fri Nov 26 09:15:49 2010 +0100
+++ b/src/HOL/SetInterval.thy Fri Nov 26 10:04:04 2010 +0100
@@ -159,6 +159,10 @@
apply simp_all
done
+lemma lessThan_strict_subset_iff:
+ fixes m n :: "'a::linorder"
+ shows "{..<m} < {..<n} \<longleftrightarrow> m < n"
+ by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq)
subsection {*Two-sided intervals*}
@@ -262,6 +266,18 @@
apply (simp add: less_imp_le)
done
+lemma atLeastLessThan_inj:
+ fixes a b c d :: "'a::linorder"
+ assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d"
+ shows "a = c" "b = d"
+using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le linorder_antisym_conv2 subset_refl)+
+
+lemma atLeastLessThan_eq_iff:
+ fixes a b c d :: "'a::linorder"
+ assumes "a < b" "c < d"
+ shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d"
+ using atLeastLessThan_inj assms by auto
+
subsubsection {* Intersection *}
context linorder
@@ -705,6 +721,39 @@
"finite M \<Longrightarrow> \<exists>h. bij_betw h {1 .. card M} M"
by (rule finite_same_card_bij) auto
+lemma bij_betw_iff_card:
+ assumes FIN: "finite A" and FIN': "finite B"
+ shows BIJ: "(\<exists>f. bij_betw f A B) \<longleftrightarrow> (card A = card B)"
+using assms
+proof(auto simp add: bij_betw_same_card)
+ assume *: "card A = card B"
+ obtain f where "bij_betw f A {0 ..< card A}"
+ using FIN ex_bij_betw_finite_nat by blast
+ moreover obtain g where "bij_betw g {0 ..< card B} B"
+ using FIN' ex_bij_betw_nat_finite by blast
+ ultimately have "bij_betw (g o f) A B"
+ using * by (auto simp add: bij_betw_trans)
+ thus "(\<exists>f. bij_betw f A B)" by blast
+qed
+
+lemma inj_on_iff_card_le:
+ assumes FIN: "finite A" and FIN': "finite B"
+ shows "(\<exists>f. inj_on f A \<and> f ` A \<le> B) = (card A \<le> card B)"
+proof (safe intro!: card_inj_on_le)
+ assume *: "card A \<le> card B"
+ obtain f where 1: "inj_on f A" and 2: "f ` A = {0 ..< card A}"
+ using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force
+ moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g ` {0 ..< card B} = B"
+ using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force
+ ultimately have "inj_on g (f ` A)" using subset_inj_on[of g _ "f ` A"] * by force
+ hence "inj_on (g o f) A" using 1 comp_inj_on by blast
+ moreover
+ {have "{0 ..< card A} \<le> {0 ..< card B}" using * by force
+ with 2 have "f ` A \<le> {0 ..< card B}" by blast
+ hence "(g o f) ` A \<le> B" unfolding comp_def using 3 by force
+ }
+ ultimately show "(\<exists>f. inj_on f A \<and> f ` A \<le> B)" by blast
+qed (insert assms, auto)
subsection {* Intervals of integers *}
--- a/src/HOL/UNITY/Comp/Alloc.thy Fri Nov 26 09:15:49 2010 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy Fri Nov 26 10:04:04 2010 +0100
@@ -358,7 +358,7 @@
done
lemma surj_sysOfAlloc [iff]: "surj sysOfAlloc"
- apply (simp add: surj_iff fun_eq_iff o_apply)
+ apply (simp add: surj_iff_all)
apply record_auto
done
@@ -386,7 +386,7 @@
done
lemma surj_sysOfClient [iff]: "surj sysOfClient"
- apply (simp add: surj_iff fun_eq_iff o_apply)
+ apply (simp add: surj_iff_all)
apply record_auto
done
@@ -410,7 +410,7 @@
done
lemma surj_client_map [iff]: "surj client_map"
- apply (simp add: surj_iff fun_eq_iff o_apply)
+ apply (simp add: surj_iff_all)
apply record_auto
done
@@ -682,7 +682,7 @@
lemma fst_lift_map_eq_fst [simp]: "fst (lift_map i x) i = fst x"
apply (insert fst_o_lift_map [of i])
apply (drule fun_cong [where x=x])
-apply (simp add: o_def);
+apply (simp add: o_def)
done
lemma fst_o_lift_map' [simp]:
@@ -702,7 +702,7 @@
RS guarantees_PLam_I
RS (bij_sysOfClient RS rename_rename_guarantees_eq RS iffD2)
|> simplify (simpset() addsimps [lift_image_eq_rename, o_def, split_def,
- surj_rename RS surj_range])
+ surj_rename])
However, the "preserves" property remains to be discharged, and the unfolding
of "o" and "sub" complicates subsequent reasoning.
@@ -723,7 +723,7 @@
asm_simp_tac
(ss addsimps [@{thm lift_guarantees_eq_lift_inv},
@{thm rename_guarantees_eq_rename_inv},
- @{thm bij_imp_bij_inv}, @{thm surj_rename} RS @{thm surj_range},
+ @{thm bij_imp_bij_inv}, @{thm surj_rename},
@{thm inv_inv_eq}]) 1,
asm_simp_tac
(@{simpset} addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1]
@@ -798,9 +798,9 @@
lemmas rename_Alloc_Increasing =
Alloc_Increasing
[THEN rename_guarantees_sysOfAlloc_I,
- simplified surj_rename [THEN surj_range] o_def sub_apply
+ simplified surj_rename o_def sub_apply
rename_image_Increasing bij_sysOfAlloc
- allocGiv_o_inv_sysOfAlloc_eq'];
+ allocGiv_o_inv_sysOfAlloc_eq']
lemma System_Increasing_allocGiv:
"i < Nclients ==> System : Increasing (sub i o allocGiv)"
@@ -879,7 +879,7 @@
\<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel) s)}"
apply (simp add: o_apply)
apply (insert Alloc_Safety [THEN rename_guarantees_sysOfAlloc_I])
- apply (simp add: o_def);
+ apply (simp add: o_def)
apply (erule component_guaranteesD)
apply (auto simp add: System_Increasing_allocRel [simplified sub_apply o_def])
done
--- a/src/HOL/UNITY/Extend.thy Fri Nov 26 09:15:49 2010 +0100
+++ b/src/HOL/UNITY/Extend.thy Fri Nov 26 10:04:04 2010 +0100
@@ -127,7 +127,7 @@
assumes surj_h: "surj h"
and prem: "!! x y. g (h(x,y)) = x"
shows "fst (inv h z) = g z"
-by (metis UNIV_I f_inv_into_f pair_collapse prem surj_h surj_range)
+by (metis UNIV_I f_inv_into_f pair_collapse prem surj_h)
subsection{*Trivial properties of f, g, h*}
--- a/src/HOL/UNITY/Rename.thy Fri Nov 26 09:15:49 2010 +0100
+++ b/src/HOL/UNITY/Rename.thy Fri Nov 26 10:04:04 2010 +0100
@@ -60,7 +60,8 @@
lemma bij_extend_act: "bij h ==> bij (extend_act (%(x,u::'c). h x))"
apply (rule bijI)
apply (rule Extend.inj_extend_act)
-apply (auto simp add: bij_extend_act_eq_project_act)
+apply simp
+apply (simp add: bij_extend_act_eq_project_act)
apply (rule surjI)
apply (rule Extend.extend_act_inverse)
apply (blast intro: bij_imp_bij_inv good_map_bij)
@@ -75,7 +76,7 @@
project_act (%(x,u::'c). h x)"
apply (simp (no_asm_simp) add: bij_extend_act_eq_project_act [symmetric])
apply (rule surj_imp_inv_eq)
-apply (blast intro: bij_extend_act bij_is_surj)
+apply (blast intro!: bij_extend_act bij_is_surj)
apply (simp (no_asm_simp) add: Extend.extend_act_inverse)
done