Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.

--- a/src/HOL/Finite_Set.thy	Mon Nov 22 10:34:33 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Nov 23 14:14:17 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 *}
 

--- a/src/HOL/Fun.thy	Mon Nov 22 10:34:33 2010 +0100
+++ b/src/HOL/Fun.thy	Tue Nov 23 14:14:17 2010 +0100
@@ -169,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)
@@ -185,6 +193,42 @@
 lemma inj_on_id2[simp]: "inj_on (%x. x) A"
 by (simp add: inj_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
 
@@ -249,6 +293,14 @@
 apply (blast)
 done
 
+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 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 auto
 
@@ -270,6 +322,20 @@
 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 bij_betw_empty2:
+  assumes "bij_betw f A {}"
+  shows "A = {}"
+using assms unfolding bij_betw_def by blast
+
+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 bij_betw_def ..
 
@@ -292,6 +358,32 @@
 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"
@@ -323,11 +415,73 @@
   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
 
@@ -613,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	Mon Nov 22 10:34:33 2010 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Tue Nov 23 14:14:17 2010 +0100
@@ -261,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/Set.thy	Mon Nov 22 10:34:33 2010 +0100
+++ b/src/HOL/Set.thy	Tue Nov 23 14:14:17 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	Mon Nov 22 10:34:33 2010 +0100
+++ b/src/HOL/SetInterval.thy	Tue Nov 23 14:14:17 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 *}