--- a/src/HOL/Library/Countable_Set.thy Thu Jun 12 08:48:59 2014 +0200
+++ b/src/HOL/Library/Countable_Set.thy Wed Jun 11 13:39:38 2014 +0200
@@ -296,4 +296,23 @@
qed
qed
+subsection {* Uncountable *}
+
+abbreviation uncountable where
+ "uncountable A \<equiv> \<not> countable A"
+
+lemma uncountable_def: "uncountable A \<longleftrightarrow> A \<noteq> {} \<and> \<not> (\<exists>f::(nat \<Rightarrow> 'a). range f = A)"
+ by (auto intro: inj_on_inv_into simp: countable_def)
+ (metis all_not_in_conv inj_on_iff_surj subset_UNIV)
+
+lemma uncountable_bij_betw: "bij_betw f A B \<Longrightarrow> uncountable B \<Longrightarrow> uncountable A"
+ unfolding bij_betw_def by (metis countable_image)
+
+lemma uncountable_infinite: "uncountable A \<Longrightarrow> infinite A"
+ by (metis countable_finite)
+
+lemma uncountable_minus_countable:
+ "uncountable A \<Longrightarrow> countable B \<Longrightarrow> uncountable (A - B)"
+ using countable_Un[of B "A - B"] assms by auto
+
end