eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
--- a/src/HOL/BNF/Basic_BNFs.thy Mon Nov 25 08:22:29 2013 +0100
+++ b/src/HOL/BNF/Basic_BNFs.thy Mon Nov 25 10:14:29 2013 +0100
@@ -16,7 +16,7 @@
lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
lemma natLeq_cinfinite: "cinfinite natLeq"
-unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
+unfolding cinfinite_def Field_natLeq by (metis infinite_UNIV_nat)
lemma wpull_Grp_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Grp B1 f1 OO (Grp B2 f2)\<inverse>\<inverse> \<le> (Grp A p1)\<inverse>\<inverse> OO Grp A p2"
unfolding wpull_def Grp_def by auto
--- a/src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy Mon Nov 25 08:22:29 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic_FP.thy Mon Nov 25 10:14:29 2013 +0100
@@ -121,7 +121,7 @@
subsection {* (In)finite cardinals *}
definition cinfinite where
- "cinfinite r = infinite (Field r)"
+ "cinfinite r = (\<not> finite (Field r))"
abbreviation Cinfinite where
"Cinfinite r \<equiv> cinfinite r \<and> Card_order r"
@@ -140,7 +140,7 @@
assumes inf: "Cinfinite r"
shows "natLeq \<le>o r"
proof -
- from inf have "natLeq \<le>o |Field r|" by (simp add: cinfinite_def infinite_iff_natLeq_ordLeq)
+ from inf have "natLeq \<le>o |Field r|" by (metis cinfinite_def infinite_iff_natLeq_ordLeq)
also from inf have "|Field r| =o r" by (simp add: card_of_unique ordIso_symmetric)
finally show ?thesis .
qed
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy Mon Nov 25 08:22:29 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Mon Nov 25 10:14:29 2013 +0100
@@ -308,18 +308,17 @@
corollary Card_order_Times3:
"Card_order r \<Longrightarrow> |Field r| \<le>o |(Field r) \<times> (Field r)|"
-using card_of_Times3 card_of_Field_ordIso
- ordIso_ordLeq_trans ordIso_symmetric by blast
+ by (rule card_of_Times3)
lemma card_of_Times_cong1[simp]:
assumes "|A| =o |B|"
shows "|A \<times> C| =o |B \<times> C|"
-using assms by (simp add: ordIso_iff_ordLeq card_of_Times_mono1)
+using assms by (simp add: ordIso_iff_ordLeq)
lemma card_of_Times_cong2[simp]:
assumes "|A| =o |B|"
shows "|C \<times> A| =o |C \<times> B|"
-using assms by (simp add: ordIso_iff_ordLeq card_of_Times_mono2)
+using assms by (simp add: ordIso_iff_ordLeq)
lemma card_of_Times_mono[simp]:
assumes "|A| \<le>o |B|" and "|C| \<le>o |D|"
@@ -473,18 +472,18 @@
by auto
corollary Times_same_infinite_bij_betw:
-assumes "infinite A"
+assumes "\<not>finite A"
shows "\<exists>f. bij_betw f (A \<times> A) A"
using assms by (auto simp add: card_of_ordIso)
corollary Times_same_infinite_bij_betw_types:
-assumes INF: "infinite(UNIV::'a set)"
+assumes INF: "\<not>finite(UNIV::'a set)"
shows "\<exists>(f::('a * 'a) => 'a). bij f"
using assms Times_same_infinite_bij_betw[of "UNIV::'a set"]
by auto
corollary Times_infinite_bij_betw:
-assumes INF: "infinite A" and NE: "B \<noteq> {}" and INJ: "inj_on g B \<and> g ` B \<le> A"
+assumes INF: "\<not>finite A" and NE: "B \<noteq> {}" and INJ: "inj_on g B \<and> g ` B \<le> A"
shows "(\<exists>f. bij_betw f (A \<times> B) A) \<and> (\<exists>h. bij_betw h (B \<times> A) A)"
proof-
have "|B| \<le>o |A|" using INJ card_of_ordLeq by blast
@@ -493,19 +492,19 @@
qed
corollary Times_infinite_bij_betw_types:
-assumes INF: "infinite(UNIV::'a set)" and
+assumes INF: "\<not>finite(UNIV::'a set)" and
BIJ: "inj(g::'b \<Rightarrow> 'a)"
shows "(\<exists>(f::('b * 'a) => 'a). bij f) \<and> (\<exists>(h::('a * 'b) => 'a). bij h)"
using assms Times_infinite_bij_betw[of "UNIV::'a set" "UNIV::'b set" g]
by auto
lemma card_of_Times_ordLeq_infinite:
-"\<lbrakk>infinite C; |A| \<le>o |C|; |B| \<le>o |C|\<rbrakk>
+"\<lbrakk>\<not>finite C; |A| \<le>o |C|; |B| \<le>o |C|\<rbrakk>
\<Longrightarrow> |A <*> B| \<le>o |C|"
by(simp add: card_of_Sigma_ordLeq_infinite)
corollary Plus_infinite_bij_betw:
-assumes INF: "infinite A" and INJ: "inj_on g B \<and> g ` B \<le> A"
+assumes INF: "\<not>finite A" and INJ: "inj_on g B \<and> g ` B \<le> A"
shows "(\<exists>f. bij_betw f (A <+> B) A) \<and> (\<exists>h. bij_betw h (B <+> A) A)"
proof-
have "|B| \<le>o |A|" using INJ card_of_ordLeq by blast
@@ -514,14 +513,14 @@
qed
corollary Plus_infinite_bij_betw_types:
-assumes INF: "infinite(UNIV::'a set)" and
+assumes INF: "\<not>finite(UNIV::'a set)" and
BIJ: "inj(g::'b \<Rightarrow> 'a)"
shows "(\<exists>(f::('b + 'a) => 'a). bij f) \<and> (\<exists>(h::('a + 'b) => 'a). bij h)"
using assms Plus_infinite_bij_betw[of "UNIV::'a set" g "UNIV::'b set"]
by auto
lemma card_of_Un_infinite:
-assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
+assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
shows "|A \<union> B| =o |A| \<and> |B \<union> A| =o |A|"
proof-
have "|A \<union> B| \<le>o |A <+> B|" by (rule card_of_Un_Plus_ordLeq)
@@ -533,12 +532,12 @@
qed
lemma card_of_Un_infinite_simps[simp]:
-"\<lbrakk>infinite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |A \<union> B| =o |A|"
-"\<lbrakk>infinite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |B \<union> A| =o |A|"
+"\<lbrakk>\<not>finite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |A \<union> B| =o |A|"
+"\<lbrakk>\<not>finite A; |B| \<le>o |A| \<rbrakk> \<Longrightarrow> |B \<union> A| =o |A|"
using card_of_Un_infinite by auto
lemma card_of_Un_diff_infinite:
-assumes INF: "infinite A" and LESS: "|B| <o |A|"
+assumes INF: "\<not>finite A" and LESS: "|B| <o |A|"
shows "|A - B| =o |A|"
proof-
obtain C where C_def: "C = A - B" by blast
@@ -554,7 +553,7 @@
using card_of_ordLeq_finite * by blast
hence False using ** INF card_of_ordIso_finite 1 by blast
}
- hence "infinite B" by auto
+ hence "\<not>finite B" by auto
ultimately have False
using card_of_Un_infinite 1 ordIso_equivalence(1,3) LESS not_ordLess_ordIso by metis
}
@@ -563,14 +562,14 @@
hence "finite B" using card_of_ordLeq_finite 2 by blast
hence False using * INF card_of_ordIso_finite 1 by blast
}
- hence "infinite C" by auto
+ hence "\<not>finite C" by auto
hence "|C| =o |A|"
using card_of_Un_infinite 1 2 ordIso_equivalence(1,3) by metis
thus ?thesis unfolding C_def .
qed
corollary Card_order_Un_infinite:
-assumes INF: "infinite(Field r)" and CARD: "Card_order r" and
+assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
LEQ: "p \<le>o r"
shows "| (Field r) \<union> (Field p) | =o r \<and> | (Field p) \<union> (Field r) | =o r"
proof-
@@ -584,12 +583,12 @@
qed
corollary subset_ordLeq_diff_infinite:
-assumes INF: "infinite B" and SUB: "A \<le> B" and LESS: "|A| <o |B|"
-shows "infinite (B - A)"
+assumes INF: "\<not>finite B" and SUB: "A \<le> B" and LESS: "|A| <o |B|"
+shows "\<not>finite (B - A)"
using assms card_of_Un_diff_infinite card_of_ordIso_finite by blast
lemma card_of_Times_ordLess_infinite[simp]:
-assumes INF: "infinite C" and
+assumes INF: "\<not>finite C" and
LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
shows "|A \<times> B| <o |C|"
proof(cases "A = {} \<or> B = {}")
@@ -601,17 +600,17 @@
next
assume Case2: "\<not>(A = {} \<or> B = {})"
{assume *: "|C| \<le>o |A \<times> B|"
- hence "infinite (A \<times> B)" using INF card_of_ordLeq_finite by blast
- hence 1: "infinite A \<or> infinite B" using finite_cartesian_product by blast
+ hence "\<not>finite (A \<times> B)" using INF card_of_ordLeq_finite by blast
+ hence 1: "\<not>finite A \<or> \<not>finite B" using finite_cartesian_product by blast
{assume Case21: "|A| \<le>o |B|"
- hence "infinite B" using 1 card_of_ordLeq_finite by blast
+ hence "\<not>finite B" using 1 card_of_ordLeq_finite by blast
hence "|A \<times> B| =o |B|" using Case2 Case21
by (auto simp add: card_of_Times_infinite)
hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
}
moreover
{assume Case22: "|B| \<le>o |A|"
- hence "infinite A" using 1 card_of_ordLeq_finite by blast
+ hence "\<not>finite A" using 1 card_of_ordLeq_finite by blast
hence "|A \<times> B| =o |A|" using Case2 Case22
by (auto simp add: card_of_Times_infinite)
hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
@@ -624,7 +623,7 @@
qed
lemma card_of_Times_ordLess_infinite_Field[simp]:
-assumes INF: "infinite (Field r)" and r: "Card_order r" and
+assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
LESS1: "|A| <o r" and LESS2: "|B| <o r"
shows "|A \<times> B| <o r"
proof-
@@ -639,14 +638,14 @@
qed
lemma card_of_Un_ordLess_infinite[simp]:
-assumes INF: "infinite C" and
+assumes INF: "\<not>finite C" and
LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
shows "|A \<union> B| <o |C|"
using assms card_of_Plus_ordLess_infinite card_of_Un_Plus_ordLeq
ordLeq_ordLess_trans by blast
lemma card_of_Un_ordLess_infinite_Field[simp]:
-assumes INF: "infinite (Field r)" and r: "Card_order r" and
+assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
LESS1: "|A| <o r" and LESS2: "|B| <o r"
shows "|A Un B| <o r"
proof-
@@ -667,10 +666,10 @@
"finite A = ( |A| <o |UNIV :: nat set| )"
using infinite_iff_card_of_nat[of A]
not_ordLeq_iff_ordLess[of "|A|" "|UNIV :: nat set|"]
-by (fastforce simp: card_of_Well_order)
+by fastforce
lemma finite_ordLess_infinite2[simp]:
-assumes "finite A" and "infinite B"
+assumes "finite A" and "\<not>finite B"
shows "|A| <o |B|"
using assms
finite_ordLess_infinite[of "|A|" "|B|"]
@@ -678,7 +677,7 @@
Field_card_of[of A] Field_card_of[of B] by auto
lemma infinite_card_of_insert:
-assumes "infinite A"
+assumes "\<not>finite A"
shows "|insert a A| =o |A|"
proof-
have iA: "insert a A = A \<union> {a}" by simp
@@ -688,7 +687,7 @@
qed
lemma card_of_Un_singl_ordLess_infinite1:
-assumes "infinite B" and "|A| <o |B|"
+assumes "\<not>finite B" and "|A| <o |B|"
shows "|{a} Un A| <o |B|"
proof-
have "|{a}| <o |B|" using assms by auto
@@ -696,7 +695,7 @@
qed
lemma card_of_Un_singl_ordLess_infinite:
-assumes "infinite B"
+assumes "\<not>finite B"
shows "( |A| <o |B| ) = ( |{a} Un A| <o |B| )"
using assms card_of_Un_singl_ordLess_infinite1[of B A]
proof(auto)
@@ -766,11 +765,11 @@
qed
lemma card_of_nlists_infinite:
-assumes "infinite A"
+assumes "\<not>finite A"
shows "|nlists A n| \<le>o |A|"
proof(induct n)
have "A \<noteq> {}" using assms by auto
- thus "|nlists A 0| \<le>o |A|" by (simp add: nlists_0 card_of_singl_ordLeq)
+ thus "|nlists A 0| \<le>o |A|" by (simp add: nlists_0)
next
fix n assume IH: "|nlists A n| \<le>o |A|"
have "|nlists A (Suc n)| =o |A \<times> (nlists A n)|"
@@ -857,18 +856,17 @@
qed
lemma card_of_lists_infinite[simp]:
-assumes "infinite A"
+assumes "\<not>finite A"
shows "|lists A| =o |A|"
proof-
- have "|lists A| \<le>o |A|"
- using assms
- by (auto simp add: lists_UNION_nlists card_of_UNION_ordLeq_infinite
- infinite_iff_card_of_nat card_of_nlists_infinite)
+ have "|lists A| \<le>o |A|" unfolding lists_UNION_nlists
+ by (rule card_of_UNION_ordLeq_infinite[OF assms _ ballI[OF card_of_nlists_infinite[OF assms]]])
+ (metis infinite_iff_card_of_nat assms)
thus ?thesis using card_of_lists ordIso_iff_ordLeq by blast
qed
lemma Card_order_lists_infinite:
-assumes "Card_order r" and "infinite(Field r)"
+assumes "Card_order r" and "\<not>finite(Field r)"
shows "|lists(Field r)| =o r"
using assms card_of_lists_infinite card_of_Field_ordIso ordIso_transitive by blast
@@ -878,12 +876,12 @@
using assms card_of_cong card_of_lists_cong by blast
corollary lists_infinite_bij_betw:
-assumes "infinite A"
+assumes "\<not>finite A"
shows "\<exists>f. bij_betw f (lists A) A"
using assms card_of_lists_infinite card_of_ordIso by blast
corollary lists_infinite_bij_betw_types:
-assumes "infinite(UNIV :: 'a set)"
+assumes "\<not>finite(UNIV :: 'a set)"
shows "\<exists>(f::'a list \<Rightarrow> 'a). bij f"
using assms assms lists_infinite_bij_betw[of "UNIV::'a set"]
using lists_UNIV by auto
@@ -991,13 +989,13 @@
qed
lemma card_of_Fpow_infinite[simp]:
-assumes "infinite A"
+assumes "\<not>finite A"
shows "|Fpow A| =o |A|"
using assms card_of_Fpow_lists card_of_lists_infinite card_of_Fpow
ordLeq_ordIso_trans ordIso_iff_ordLeq by blast
corollary Fpow_infinite_bij_betw:
-assumes "infinite A"
+assumes "\<not>finite A"
shows "\<exists>f. bij_betw f (Fpow A) A"
using assms card_of_Fpow_infinite card_of_ordIso by blast
@@ -1052,7 +1050,7 @@
simp add: Field_natLeq_on, unfold rel.under_def, auto)
lemma natLeq_on_ordLess_natLeq: "natLeq_on n <o natLeq"
-using Field_natLeq Field_natLeq_on[of n] nat_infinite
+using Field_natLeq Field_natLeq_on[of n]
finite_ordLess_infinite[of "natLeq_on n" natLeq]
natLeq_Well_order natLeq_on_Well_order[of n] by auto
@@ -1074,11 +1072,11 @@
subsubsection {* Then as cardinals *}
lemma ordIso_natLeq_infinite1:
-"|A| =o natLeq \<Longrightarrow> infinite A"
+"|A| =o natLeq \<Longrightarrow> \<not>finite A"
using ordIso_symmetric ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast
lemma ordIso_natLeq_infinite2:
-"natLeq =o |A| \<Longrightarrow> infinite A"
+"natLeq =o |A| \<Longrightarrow> \<not>finite A"
using ordIso_imp_ordLeq infinite_iff_natLeq_ordLeq by blast
lemma ordLeq_natLeq_on_imp_finite:
@@ -1148,11 +1146,11 @@
qed
lemma card_of_Plus_ordLeq_infinite[simp]:
-assumes C: "infinite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
+assumes C: "\<not>finite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
shows "|A <+> B| \<le>o |C|"
proof-
let ?r = "cardSuc |C|"
- have "Card_order ?r \<and> infinite (Field ?r)" using assms by simp
+ have "Card_order ?r \<and> \<not>finite (Field ?r)" using assms by simp
moreover have "|A| <o ?r" and "|B| <o ?r" using A B by auto
ultimately have "|A <+> B| <o ?r"
using card_of_Plus_ordLess_infinite_Field by blast
@@ -1160,7 +1158,7 @@
qed
lemma card_of_Un_ordLeq_infinite[simp]:
-assumes C: "infinite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
+assumes C: "\<not>finite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
shows "|A Un B| \<le>o |C|"
using assms card_of_Plus_ordLeq_infinite card_of_Un_Plus_ordLeq
ordLeq_transitive by metis
@@ -1185,12 +1183,12 @@
using assms unfolding relChain_def by auto
lemma card_of_infinite_diff_finite:
-assumes "infinite A" and "finite B"
+assumes "\<not>finite A" and "finite B"
shows "|A - B| =o |A|"
by (metis assms card_of_Un_diff_infinite finite_ordLess_infinite2)
lemma infinite_card_of_diff_singl:
-assumes "infinite A"
+assumes "\<not>finite A"
shows "|A - {a}| =o |A|"
by (metis assms card_of_infinite_diff_finite finite.emptyI finite_insert)
@@ -1235,8 +1233,8 @@
lemma infinite_Bpow:
assumes rc: "Card_order r" and r: "Field r \<noteq> {}"
-and A: "infinite A"
-shows "infinite (Bpow r A)"
+and A: "\<not>finite A"
+shows "\<not>finite (Bpow r A)"
using ordLeq_card_Bpow[OF rc r]
by (metis A card_of_ordLeq_infinite)
@@ -1350,7 +1348,7 @@
qed
lemma Bpow_ordLeq_Func_Field:
-assumes rc: "Card_order r" and r: "Field r \<noteq> {}" and A: "infinite A"
+assumes rc: "Card_order r" and r: "Field r \<noteq> {}" and A: "\<not>finite A"
shows "|Bpow r A| \<le>o |Func (Field r) A|"
proof-
let ?F = "\<lambda> f. {x | x a. f a = x \<and> a \<in> Field r}"
@@ -1368,10 +1366,9 @@
hence "|Bpow r A - {{}}| \<le>o |Func (Field r) A|"
by (rule surj_imp_ordLeq)
moreover
- {have 2: "infinite (Bpow r A)" using infinite_Bpow[OF rc r A] .
+ {have 2: "\<not>finite (Bpow r A)" using infinite_Bpow[OF rc r A] .
have "|Bpow r A| =o |Bpow r A - {{}}|"
- using card_of_infinite_diff_finite
- by (metis Pow_empty 2 finite_Pow_iff infinite_imp_nonempty ordIso_symmetric)
+ by (metis 2 infinite_card_of_diff_singl ordIso_symmetric)
}
ultimately show ?thesis by (metis ordIso_ordLeq_trans)
qed
@@ -1408,8 +1405,8 @@
qed
lemma infinite_Func:
-assumes A: "infinite A" and B: "{b1,b2} \<subseteq> B" "b1 \<noteq> b2"
-shows "infinite (Func A B)"
+assumes A: "\<not>finite A" and B: "{b1,b2} \<subseteq> B" "b1 \<noteq> b2"
+shows "\<not>finite (Func A B)"
using ordLeq_Func[OF B] by (metis A card_of_ordLeq_finite)
end
--- a/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy Mon Nov 25 08:22:29 2013 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation_FP.thy Mon Nov 25 10:14:29 2013 +0100
@@ -487,8 +487,8 @@
lemma infinite_Pow:
-assumes "infinite A"
-shows "infinite (Pow A)"
+assumes "\<not> finite A"
+shows "\<not> finite (Pow A)"
proof-
have "|A| \<le>o |Pow A|" by (metis card_of_Pow ordLess_imp_ordLeq)
thus ?thesis by (metis assms finite_Pow_iff)
@@ -908,8 +908,8 @@
lemma card_of_ordLeq_infinite:
-assumes "|A| \<le>o |B|" and "infinite A"
-shows "infinite B"
+assumes "|A| \<le>o |B|" and "\<not> finite A"
+shows "\<not> finite B"
using assms card_of_ordLeq_finite by auto
@@ -938,15 +938,14 @@
lemma infinite_iff_card_of_nat:
-"infinite A = ( |UNIV::nat set| \<le>o |A| )"
-by (auto simp add: infinite_iff_countable_subset card_of_ordLeq)
-
+"\<not> finite A \<longleftrightarrow> ( |UNIV::nat set| \<le>o |A| )"
+unfolding infinite_iff_countable_subset card_of_ordLeq ..
text{* The next two results correspond to the ZF fact that all infinite cardinals are
limit ordinals: *}
lemma Card_order_infinite_not_under:
-assumes CARD: "Card_order r" and INF: "infinite (Field r)"
+assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)"
shows "\<not> (\<exists>a. Field r = rel.under r a)"
proof(auto)
have 0: "Well_order r \<and> wo_rel r \<and> Refl r"
@@ -983,7 +982,7 @@
lemma infinite_Card_order_limit:
-assumes r: "Card_order r" and "infinite (Field r)"
+assumes r: "Card_order r" and "\<not>finite (Field r)"
and a: "a : Field r"
shows "EX b : Field r. a \<noteq> b \<and> (a,b) : r"
proof-
@@ -1005,11 +1004,11 @@
theorem Card_order_Times_same_infinite:
-assumes CO: "Card_order r" and INF: "infinite(Field r)"
+assumes CO: "Card_order r" and INF: "\<not>finite(Field r)"
shows "|Field r \<times> Field r| \<le>o r"
proof-
obtain phi where phi_def:
- "phi = (\<lambda>r::'a rel. Card_order r \<and> infinite(Field r) \<and>
+ "phi = (\<lambda>r::'a rel. Card_order r \<and> \<not>finite(Field r) \<and>
\<not> |Field r \<times> Field r| \<le>o r )" by blast
have temp1: "\<forall>r. phi r \<longrightarrow> Well_order r"
unfolding phi_def card_order_on_def by auto
@@ -1060,15 +1059,15 @@
}
ultimately have 11: "|A1| <o r" using ordLeq_ordLess_trans by blast
(* *)
- have "infinite (Field r)" using 1 unfolding phi_def by simp
- hence "infinite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast
- hence "infinite A1" using 9 infinite_super finite_cartesian_product by blast
+ have "\<not> finite (Field r)" using 1 unfolding phi_def by simp
+ hence "\<not> finite ?B" using 8 3 card_of_ordIso_finite_Field[of r ?B] by blast
+ hence "\<not> finite A1" using 9 finite_cartesian_product finite_subset by metis
moreover have temp4: "Field |A1| = A1 \<and> Well_order |A1| \<and> Card_order |A1|"
using card_of_Card_order[of A1] card_of_Well_order[of A1]
by (simp add: Field_card_of)
moreover have "\<not> r \<le>o | A1 |"
using temp4 11 3 using not_ordLeq_iff_ordLess by blast
- ultimately have "infinite(Field |A1| ) \<and> Card_order |A1| \<and> \<not> r \<le>o | A1 |"
+ ultimately have "\<not> finite(Field |A1| ) \<and> Card_order |A1| \<and> \<not> r \<le>o | A1 |"
by (simp add: card_of_card_order_on)
hence "|Field |A1| \<times> Field |A1| | \<le>o |A1|"
using 2 unfolding phi_def by blast
@@ -1081,7 +1080,7 @@
corollary card_of_Times_same_infinite:
-assumes "infinite A"
+assumes "\<not>finite A"
shows "|A \<times> A| =o |A|"
proof-
let ?r = "|A|"
@@ -1094,7 +1093,7 @@
lemma card_of_Times_infinite:
-assumes INF: "infinite A" and NE: "B \<noteq> {}" and LEQ: "|B| \<le>o |A|"
+assumes INF: "\<not>finite A" and NE: "B \<noteq> {}" and LEQ: "|B| \<le>o |A|"
shows "|A \<times> B| =o |A| \<and> |B \<times> A| =o |A|"
proof-
have "|A| \<le>o |A \<times> B| \<and> |A| \<le>o |B \<times> A|"
@@ -1111,7 +1110,7 @@
corollary Card_order_Times_infinite:
-assumes INF: "infinite(Field r)" and CARD: "Card_order r" and
+assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
NE: "Field p \<noteq> {}" and LEQ: "p \<le>o r"
shows "| (Field r) \<times> (Field p) | =o r \<and> | (Field p) \<times> (Field r) | =o r"
proof-
@@ -1125,7 +1124,7 @@
lemma card_of_Sigma_ordLeq_infinite:
-assumes INF: "infinite B" and
+assumes INF: "\<not>finite B" and
LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
shows "|SIGMA i : I. A i| \<le>o |B|"
proof(cases "I = {}", simp add: card_of_empty)
@@ -1139,7 +1138,7 @@
lemma card_of_Sigma_ordLeq_infinite_Field:
-assumes INF: "infinite (Field r)" and r: "Card_order r" and
+assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
shows "|SIGMA i : I. A i| \<le>o r"
proof-
@@ -1155,21 +1154,21 @@
lemma card_of_Times_ordLeq_infinite_Field:
-"\<lbrakk>infinite (Field r); |A| \<le>o r; |B| \<le>o r; Card_order r\<rbrakk>
+"\<lbrakk>\<not>finite (Field r); |A| \<le>o r; |B| \<le>o r; Card_order r\<rbrakk>
\<Longrightarrow> |A <*> B| \<le>o r"
by(simp add: card_of_Sigma_ordLeq_infinite_Field)
lemma card_of_Times_infinite_simps:
-"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A \<times> B| =o |A|"
-"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |A \<times> B|"
-"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |B \<times> A| =o |A|"
-"\<lbrakk>infinite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |B \<times> A|"
+"\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A \<times> B| =o |A|"
+"\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |A \<times> B|"
+"\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |B \<times> A| =o |A|"
+"\<lbrakk>\<not>finite A; B \<noteq> {}; |B| \<le>o |A|\<rbrakk> \<Longrightarrow> |A| =o |B \<times> A|"
by (auto simp add: card_of_Times_infinite ordIso_symmetric)
lemma card_of_UNION_ordLeq_infinite:
-assumes INF: "infinite B" and
+assumes INF: "\<not>finite B" and
LEQ_I: "|I| \<le>o |B|" and LEQ: "\<forall>i \<in> I. |A i| \<le>o |B|"
shows "|\<Union> i \<in> I. A i| \<le>o |B|"
proof(cases "I = {}", simp add: card_of_empty)
@@ -1183,7 +1182,7 @@
corollary card_of_UNION_ordLeq_infinite_Field:
-assumes INF: "infinite (Field r)" and r: "Card_order r" and
+assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
LEQ_I: "|I| \<le>o r" and LEQ: "\<forall>i \<in> I. |A i| \<le>o r"
shows "|\<Union> i \<in> I. A i| \<le>o r"
proof-
@@ -1199,7 +1198,7 @@
lemma card_of_Plus_infinite1:
-assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
+assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
shows "|A <+> B| =o |A|"
proof(cases "B = {}", simp add: card_of_Plus_empty1 card_of_Plus_empty2 ordIso_symmetric)
let ?Inl = "Inl::'a \<Rightarrow> 'a + 'b" let ?Inr = "Inr::'b \<Rightarrow> 'a + 'b"
@@ -1210,7 +1209,7 @@
assume Case1: "B = {b1}"
have 2: "bij_betw ?Inl A ((?Inl ` A))"
unfolding bij_betw_def inj_on_def by auto
- hence 3: "infinite (?Inl ` A)"
+ hence 3: "\<not>finite (?Inl ` A)"
using INF bij_betw_finite[of ?Inl A] by blast
let ?A' = "?Inl ` A \<union> {?Inr b1}"
obtain g where "bij_betw g (?Inl ` A) ?A'"
@@ -1238,20 +1237,20 @@
lemma card_of_Plus_infinite2:
-assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
+assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
shows "|B <+> A| =o |A|"
using assms card_of_Plus_commute card_of_Plus_infinite1
ordIso_equivalence by blast
lemma card_of_Plus_infinite:
-assumes INF: "infinite A" and LEQ: "|B| \<le>o |A|"
+assumes INF: "\<not>finite A" and LEQ: "|B| \<le>o |A|"
shows "|A <+> B| =o |A| \<and> |B <+> A| =o |A|"
using assms by (auto simp: card_of_Plus_infinite1 card_of_Plus_infinite2)
corollary Card_order_Plus_infinite:
-assumes INF: "infinite(Field r)" and CARD: "Card_order r" and
+assumes INF: "\<not>finite(Field r)" and CARD: "Card_order r" and
LEQ: "p \<le>o r"
shows "| (Field r) <+> (Field p) | =o r \<and> | (Field p) <+> (Field r) | =o r"
proof-
@@ -1281,8 +1280,8 @@
where "natLeq_on n \<equiv> {(x,y). x < n \<and> y < n \<and> x \<le> y}"
lemma infinite_cartesian_product:
-assumes "infinite A" "infinite B"
-shows "infinite (A \<times> B)"
+assumes "\<not>finite A" "\<not>finite B"
+shows "\<not>finite (A \<times> B)"
proof
assume "finite (A \<times> B)"
from assms(1) have "A \<noteq> {}" by auto
@@ -1421,7 +1420,7 @@
Card_order_iff_Restr_underS Restr_natLeq2, simp add: Field_natLeq)
fix n have "finite(Field (natLeq_on n))"
unfolding Field_natLeq_on by auto
- moreover have "infinite(UNIV::nat set)" by auto
+ moreover have "\<not>finite(UNIV::nat set)" by auto
ultimately show "natLeq_on n <o |UNIV::nat set|"
using finite_ordLess_infinite[of "natLeq_on n" "|UNIV::nat set|"]
Field_card_of[of "UNIV::nat set"]
@@ -1441,7 +1440,7 @@
corollary infinite_iff_natLeq_ordLeq:
-"infinite A = ( natLeq \<le>o |A| )"
+"\<not>finite A = ( natLeq \<le>o |A| )"
using infinite_iff_card_of_nat[of A] card_of_nat
ordIso_ordLeq_trans ordLeq_ordIso_trans ordIso_symmetric by blast
@@ -1769,7 +1768,7 @@
lemma card_of_Plus_ordLess_infinite:
-assumes INF: "infinite C" and
+assumes INF: "\<not>finite C" and
LESS1: "|A| <o |C|" and LESS2: "|B| <o |C|"
shows "|A <+> B| <o |C|"
proof(cases "A = {} \<or> B = {}")
@@ -1784,17 +1783,17 @@
next
assume Case2: "\<not>(A = {} \<or> B = {})"
{assume *: "|C| \<le>o |A <+> B|"
- hence "infinite (A <+> B)" using INF card_of_ordLeq_finite by blast
- hence 1: "infinite A \<or> infinite B" using finite_Plus by blast
+ hence "\<not>finite (A <+> B)" using INF card_of_ordLeq_finite by blast
+ hence 1: "\<not>finite A \<or> \<not>finite B" using finite_Plus by blast
{assume Case21: "|A| \<le>o |B|"
- hence "infinite B" using 1 card_of_ordLeq_finite by blast
+ hence "\<not>finite B" using 1 card_of_ordLeq_finite by blast
hence "|A <+> B| =o |B|" using Case2 Case21
by (auto simp add: card_of_Plus_infinite)
hence False using LESS2 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
}
moreover
{assume Case22: "|B| \<le>o |A|"
- hence "infinite A" using 1 card_of_ordLeq_finite by blast
+ hence "\<not>finite A" using 1 card_of_ordLeq_finite by blast
hence "|A <+> B| =o |A|" using Case2 Case22
by (auto simp add: card_of_Plus_infinite)
hence False using LESS1 not_ordLess_ordLeq * ordLeq_ordIso_trans by blast
@@ -1808,7 +1807,7 @@
lemma card_of_Plus_ordLess_infinite_Field:
-assumes INF: "infinite (Field r)" and r: "Card_order r" and
+assumes INF: "\<not>finite (Field r)" and r: "Card_order r" and
LESS1: "|A| <o r" and LESS2: "|B| <o r"
shows "|A <+> B| <o r"
proof-
@@ -1824,12 +1823,12 @@
lemma card_of_Plus_ordLeq_infinite_Field:
-assumes r: "infinite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
+assumes r: "\<not>finite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
and c: "Card_order r"
shows "|A <+> B| \<le>o r"
proof-
let ?r' = "cardSuc r"
- have "Card_order ?r' \<and> infinite (Field ?r')" using assms
+ have "Card_order ?r' \<and> \<not>finite (Field ?r')" using assms
by (simp add: cardSuc_Card_order cardSuc_finite)
moreover have "|A| <o ?r'" and "|B| <o ?r'" using A B c
by (auto simp: card_of_card_order_on Field_card_of cardSuc_ordLeq_ordLess)
@@ -1841,7 +1840,7 @@
lemma card_of_Un_ordLeq_infinite_Field:
-assumes C: "infinite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
+assumes C: "\<not>finite (Field r)" and A: "|A| \<le>o r" and B: "|B| \<le>o r"
and "Card_order r"
shows "|A Un B| \<le>o r"
using assms card_of_Plus_ordLeq_infinite_Field card_of_Un_Plus_ordLeq
@@ -1904,7 +1903,7 @@
lemma infinite_cardSuc_regular:
-assumes r_inf: "infinite (Field r)" and r_card: "Card_order r"
+assumes r_inf: "\<not>finite (Field r)" and r_card: "Card_order r"
shows "regular (cardSuc r)"
proof-
let ?r' = "cardSuc r"
@@ -1955,7 +1954,7 @@
qed
lemma cardSuc_UNION:
-assumes r: "Card_order r" and "infinite (Field r)"
+assumes r: "Card_order r" and "\<not>finite (Field r)"
and As: "relChain (cardSuc r) As"
and Bsub: "B \<le> (UN i : Field (cardSuc r). As i)"
and cardB: "|B| <=o r"
--- a/src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy Mon Nov 25 08:22:29 2013 +0100
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders_FP.thy Mon Nov 25 10:14:29 2013 +0100
@@ -861,7 +861,7 @@
lemma finite_ordLess_infinite:
assumes WELL: "Well_order r" and WELL': "Well_order r'" and
- FIN: "finite(Field r)" and INF: "infinite(Field r')"
+ FIN: "finite(Field r)" and INF: "\<not>finite(Field r')"
shows "r <o r'"
proof-
{assume "r' \<le>o r"
--- a/src/HOL/Cardinals/Fun_More_FP.thy Mon Nov 25 08:22:29 2013 +0100
+++ b/src/HOL/Cardinals/Fun_More_FP.thy Mon Nov 25 10:14:29 2013 +0100
@@ -8,12 +8,12 @@
header {* More on Injections, Bijections and Inverses (FP) *}
theory Fun_More_FP
-imports "~~/src/HOL/Library/Infinite_Set"
+imports Main
begin
text {* This section proves more facts (additional to those in @{text "Fun.thy"},
-@{text "Hilbert_Choice.thy"}, @{text "Finite_Set.thy"} and @{text "Infinite_Set.thy"}),
+@{text "Hilbert_Choice.thy"}, and @{text "Finite_Set.thy"}),
mainly concerning injections, bijections, inverses and (numeric) cardinals of
finite sets. *}
@@ -97,18 +97,19 @@
(*3*)lemma inj_on_finite:
assumes "inj_on f A" "f ` A \<le> B" "finite B"
shows "finite A"
-using assms infinite_super by (fast dest: finite_imageD)
+using assms by (metis finite_imageD finite_subset)
(*3*)lemma infinite_imp_bij_betw:
-assumes INF: "infinite A"
+assumes INF: "\<not> finite A"
shows "\<exists>h. bij_betw h A (A - {a})"
proof(cases "a \<in> A")
assume Case1: "a \<notin> A" hence "A - {a} = A" by blast
thus ?thesis using bij_betw_id[of A] by auto
next
assume Case2: "a \<in> A"
- have "infinite (A - {a})" using INF infinite_remove by auto
+find_theorems "\<not> finite _"
+ have "\<not> finite (A - {a})" using INF by auto
with infinite_iff_countable_subset[of "A - {a}"] obtain f::"nat \<Rightarrow> 'a"
where 1: "inj f" and 2: "f ` UNIV \<le> A - {a}" by blast
obtain g where g_def: "g = (\<lambda> n. if n = 0 then a else f (Suc n))" by blast
@@ -179,7 +180,7 @@
(*3*)lemma infinite_imp_bij_betw2:
-assumes INF: "infinite A"
+assumes INF: "\<not> finite A"
shows "\<exists>h. bij_betw h A (A \<union> {a})"
proof(cases "a \<in> A")
assume Case1: "a \<in> A" hence "A \<union> {a} = A" by blast
@@ -187,7 +188,7 @@
next
let ?A' = "A \<union> {a}"
assume Case2: "a \<notin> A" hence "A = ?A' - {a}" by blast
- moreover have "infinite ?A'" using INF by auto
+ moreover have "\<not> finite ?A'" using INF by auto
ultimately obtain f where "bij_betw f ?A' A"
using infinite_imp_bij_betw[of ?A' a] by auto
hence "bij_betw(inv_into ?A' f) A ?A'" using bij_betw_inv_into by blast
--- a/src/HOL/Fun.thy Mon Nov 25 08:22:29 2013 +0100
+++ b/src/HOL/Fun.thy Mon Nov 25 10:14:29 2013 +0100
@@ -308,6 +308,16 @@
show ?thesis ..
qed
+lemma linorder_injI:
+ assumes hyp: "\<And>x y. x < (y::'a::linorder) \<Longrightarrow> f x \<noteq> f y"
+ shows "inj f"
+ -- {* Courtesy of Stephan Merz *}
+proof (rule inj_onI)
+ fix x y
+ assume f_eq: "f x = f y"
+ show "x = y" by (rule linorder_cases) (auto dest: hyp simp: f_eq)
+qed
+
lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
by auto
--- a/src/HOL/Hilbert_Choice.thy Mon Nov 25 08:22:29 2013 +0100
+++ b/src/HOL/Hilbert_Choice.thy Mon Nov 25 10:14:29 2013 +0100
@@ -272,6 +272,41 @@
ultimately show "finite (UNIV :: 'a set)" by simp
qed
+text {*
+ Every infinite set contains a countable subset. More precisely we
+ show that a set @{text S} is infinite if and only if there exists an
+ injective function from the naturals into @{text S}.
+
+ The ``only if'' direction is harder because it requires the
+ construction of a sequence of pairwise different elements of an
+ infinite set @{text S}. The idea is to construct a sequence of
+ non-empty and infinite subsets of @{text S} obtained by successively
+ removing elements of @{text S}.
+*}
+
+lemma infinite_countable_subset:
+ assumes inf: "\<not> finite (S::'a set)"
+ shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
+ -- {* Courtesy of Stephan Merz *}
+proof -
+ def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
+ def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
+ { fix n have "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" by (induct n) (auto simp add: Sseq_def inf) }
+ moreover then have *: "\<And>n. pick n \<in> Sseq n" by (metis someI_ex pick_def ex_in_conv finite.simps)
+ ultimately have "range pick \<subseteq> S" by auto
+ moreover
+ { fix n m
+ have "pick n \<notin> Sseq (n + Suc m)" by (induct m) (auto simp add: Sseq_def pick_def)
+ hence "pick n \<noteq> pick (n + Suc m)" by (metis *)
+ }
+ then have "inj pick" by (intro linorder_injI) (auto simp add: less_iff_Suc_add)
+ ultimately show ?thesis by blast
+qed
+
+lemma infinite_iff_countable_subset: "\<not> finite S \<longleftrightarrow> (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
+ -- {* Courtesy of Stephan Merz *}
+ by (metis finite_imageD finite_subset infinite_UNIV_char_0 infinite_countable_subset)
+
lemma image_inv_into_cancel:
assumes SURJ: "f`A=A'" and SUB: "B' \<le> A'"
shows "f `((inv_into A f)`B') = B'"
--- a/src/HOL/Library/Infinite_Set.thy Mon Nov 25 08:22:29 2013 +0100
+++ b/src/HOL/Library/Infinite_Set.thy Mon Nov 25 10:14:29 2013 +0100
@@ -200,12 +200,6 @@
lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
by simp
-text {*
- Every infinite set contains a countable subset. More precisely we
- show that a set @{text S} is infinite if and only if there exists an
- injective function from the naturals into @{text S}.
-*}
-
lemma range_inj_infinite:
"inj (f::nat \<Rightarrow> 'a) \<Longrightarrow> infinite (range f)"
proof
@@ -215,6 +209,7 @@
then show False by simp
qed
+(* duplicates Int.infinite_UNIV_int *)
lemma int_infinite [simp]: "infinite (UNIV::int set)"
proof -
from inj_int have "infinite (range int)"
@@ -226,108 +221,6 @@
qed
text {*
- The ``only if'' direction is harder because it requires the
- construction of a sequence of pairwise different elements of an
- infinite set @{text S}. The idea is to construct a sequence of
- non-empty and infinite subsets of @{text S} obtained by successively
- removing elements of @{text S}.
-*}
-
-lemma linorder_injI:
- assumes hyp: "\<And>x y. x < (y::'a::linorder) \<Longrightarrow> f x \<noteq> f y"
- shows "inj f"
-proof (rule inj_onI)
- fix x y
- assume f_eq: "f x = f y"
- show "x = y"
- proof (rule linorder_cases)
- assume "x < y"
- with hyp have "f x \<noteq> f y" by blast
- with f_eq show ?thesis by simp
- next
- assume "x = y"
- then show ?thesis .
- next
- assume "y < x"
- with hyp have "f y \<noteq> f x" by blast
- with f_eq show ?thesis by simp
- qed
-qed
-
-lemma infinite_countable_subset:
- assumes inf: "infinite (S::'a set)"
- shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
-proof -
- def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
- def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
- have Sseq_inf: "\<And>n. infinite (Sseq n)"
- proof -
- fix n
- show "infinite (Sseq n)"
- proof (induct n)
- from inf show "infinite (Sseq 0)"
- by (simp add: Sseq_def)
- next
- fix n
- assume "infinite (Sseq n)" then show "infinite (Sseq (Suc n))"
- by (simp add: Sseq_def infinite_remove)
- qed
- qed
- have Sseq_S: "\<And>n. Sseq n \<subseteq> S"
- proof -
- fix n
- show "Sseq n \<subseteq> S"
- by (induct n) (auto simp add: Sseq_def)
- qed
- have Sseq_pick: "\<And>n. pick n \<in> Sseq n"
- proof -
- fix n
- show "pick n \<in> Sseq n"
- unfolding pick_def
- proof (rule someI_ex)
- from Sseq_inf have "infinite (Sseq n)" .
- then have "Sseq n \<noteq> {}" by auto
- then show "\<exists>x. x \<in> Sseq n" by auto
- qed
- qed
- with Sseq_S have rng: "range pick \<subseteq> S"
- by auto
- have pick_Sseq_gt: "\<And>n m. pick n \<notin> Sseq (n + Suc m)"
- proof -
- fix n m
- show "pick n \<notin> Sseq (n + Suc m)"
- by (induct m) (auto simp add: Sseq_def pick_def)
- qed
- have pick_pick: "\<And>n m. pick n \<noteq> pick (n + Suc m)"
- proof -
- fix n m
- from Sseq_pick have "pick (n + Suc m) \<in> Sseq (n + Suc m)" .
- moreover from pick_Sseq_gt
- have "pick n \<notin> Sseq (n + Suc m)" .
- ultimately show "pick n \<noteq> pick (n + Suc m)"
- by auto
- qed
- have inj: "inj pick"
- proof (rule linorder_injI)
- fix i j :: nat
- assume "i < j"
- show "pick i \<noteq> pick j"
- proof
- assume eq: "pick i = pick j"
- from `i < j` obtain k where "j = i + Suc k"
- by (auto simp add: less_iff_Suc_add)
- with pick_pick have "pick i \<noteq> pick j" by simp
- with eq show False by simp
- qed
- qed
- from rng inj show ?thesis by auto
-qed
-
-lemma infinite_iff_countable_subset:
- "infinite S \<longleftrightarrow> (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)"
- by (auto simp add: infinite_countable_subset range_inj_infinite infinite_super)
-
-text {*
For any function with infinite domain and finite range there is some
element that is the image of infinitely many domain elements. In
particular, any infinite sequence of elements from a finite set