diff -r 8fcbfce2a2a9 -r 596a499318ab src/HOL/Library/Countable_Set.thy
--- 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 \ \ countable A"
+
+lemma uncountable_def: "uncountable A \ A \ {} \ \ (\f::(nat \ '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 \ uncountable B \ uncountable A"
+ unfolding bij_betw_def by (metis countable_image)
+
+lemma uncountable_infinite: "uncountable A \ infinite A"
+ by (metis countable_finite)
+
+lemma uncountable_minus_countable:
+ "uncountable A \ countable B \ uncountable (A - B)"
+ using countable_Un[of B "A - B"] assms by auto
+
end