# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1712590031 -3600
# Node ID f7b9179b5029198b6b57ad7ab009d0f9227add1f
# Parent  5afbf04418ec4b481cd533e5c2a17808a930e1e1
A bit of new material about type class "infinite", from Eval_FO

diff -r 5afbf04418ec -r f7b9179b5029 src/HOL/Library/Infinite_Typeclass.thy
--- a/src/HOL/Library/Infinite_Typeclass.thy	Fri Apr 05 21:21:02 2024 +0200
+++ b/src/HOL/Library/Infinite_Typeclass.thy	Mon Apr 08 16:27:11 2024 +0100
@@ -11,6 +11,28 @@
 class infinite =
   assumes infinite_UNIV: "infinite (UNIV::'a set)"
 
+begin
+
+lemma arb_element: "finite Y \<Longrightarrow> \<exists>x :: 'a. x \<notin> Y"
+  using ex_new_if_finite infinite_UNIV
+  by blast
+
+lemma arb_finite_subset: "finite Y \<Longrightarrow> \<exists>X :: 'a set. Y \<inter> X = {} \<and> finite X \<and> n \<le> card X"
+proof -
+  assume fin: "finite Y"
+  then obtain X where "X \<subseteq> UNIV - Y" "finite X" "n \<le> card X"
+    using infinite_UNIV
+    by (metis Compl_eq_Diff_UNIV finite_compl infinite_arbitrarily_large order_refl)
+  then show ?thesis
+    by auto
+qed
+
+lemma arb_countable_map: "finite Y \<Longrightarrow> \<exists>f :: (nat \<Rightarrow> 'a). inj f \<and> range f \<subseteq> UNIV - Y"
+  using infinite_UNIV
+  by (auto simp: infinite_countable_subset)
+
+end
+
 instance nat :: infinite
   by (intro_classes) simp