--- a/src/HOL/Finite_Set.thy Thu Jul 17 20:09:42 2025 +0100
+++ b/src/HOL/Finite_Set.thy Thu Jul 17 21:06:22 2025 +0100
@@ -2239,6 +2239,11 @@
then show "\<exists>B. finite B \<and> card B = Suc n \<and> B \<subseteq> A" ..
qed
+corollary finite_arbitrarily_large_disj:
+ "\<lbrakk> \<not> finite(UNIV::'a set); finite (A::'a set) \<rbrakk> \<Longrightarrow> \<exists>B. finite B \<and> card B = n \<and> A \<inter> B = {}"
+using infinite_arbitrarily_large[of "UNIV - A"]
+by fastforce
+
text \<open>Sometimes, to prove that a set is finite, it is convenient to work with finite subsets
and to show that their cardinalities are uniformly bounded. This possibility is formalized in
the next criterion.\<close>
@@ -2969,11 +2974,6 @@
with \<open>infinite S\<close> show False by simp
qed
-corollary finite_arbitrarily_large_disj:
- "\<lbrakk> infinite(UNIV::'a set); finite (A::'a set) \<rbrakk> \<Longrightarrow> \<exists>B. finite B \<and> card B = n \<and> A \<inter> B = {}"
-using infinite_arbitrarily_large[of "UNIV - A"]
-by fastforce
-
proposition infinite_coinduct [consumes 1, case_names infinite]:
assumes "X A"
and step: "\<And>A. X A \<Longrightarrow> \<exists>x\<in>A. X (A - {x}) \<or> infinite (A - {x})"