src/HOL/Library/Infinite_Set.thy

 
 subsection \<open>The set of integers is also infinite\<close>
 
 lemma infinite_int_iff_infinite_nat_abs: "infinite S \<longleftrightarrow> infinite ((nat \<circ> abs) ` S)"
   for S :: "int set"
-  by (auto simp: transfer_nat_int_set_relations o_def image_comp dest: finite_image_absD)
+proof -
+  have "inj_on nat (abs ` A)" for A
+    by (rule inj_onI) auto
+  then show ?thesis
+    by (auto simp add: image_comp [symmetric] dest: finite_image_absD finite_imageD)
+qed
 
 proposition infinite_int_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> \<ge> m \<and> n \<in> S)"
   for S :: "int set"
   by (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded_le o_def image_def)
     (metis abs_ge_zero nat_le_eq_zle le_nat_iff)

 lemma MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
   and MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
   by (simp_all add: MOST_Suc_iff)
 
 lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
-  by (simp add: cofinite_eq_sequentially eventually_ge_at_top)
+  by (simp add: cofinite_eq_sequentially)
 
 (* legacy names *)
 lemma Inf_many_def: "Inf_many P \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
 lemma Alm_all_def: "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)" by simp
 lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)