finite sets are countable

--- a/src/HOL/Library/FSet.thy	Mon Jul 10 16:38:42 2017 +0200
+++ b/src/HOL/Library/FSet.thy	Mon Jul 10 18:53:38 2017 +0200
@@ -7,7 +7,7 @@
 section \<open>Type of finite sets defined as a subtype of sets\<close>
 
 theory FSet
-imports Main
+imports Main Countable
 begin
 
 subsection \<open>Definition of the type\<close>
@@ -1115,6 +1115,33 @@
 qed
 
 
+subsubsection \<open>Countability\<close>
+
+lemma exists_fset_of_list: "\<exists>xs. fset_of_list xs = S"
+including fset.lifting
+by transfer (rule finite_list)
+
+lemma fset_of_list_surj[simp, intro]: "surj fset_of_list"
+proof -
+  have "x \<in> range fset_of_list" for x :: "'a fset"
+    unfolding image_iff
+    using exists_fset_of_list by fastforce
+  thus ?thesis by auto
+qed
+
+instance fset :: (countable) countable
+proof
+  obtain to_nat :: "'a list \<Rightarrow> nat" where "inj to_nat"
+    by (metis ex_inj)
+  moreover have "inj (inv fset_of_list)"
+    using fset_of_list_surj by (rule surj_imp_inj_inv)
+  ultimately have "inj (to_nat \<circ> inv fset_of_list)"
+    by (rule inj_comp)
+  thus "\<exists>to_nat::'a fset \<Rightarrow> nat. inj to_nat"
+    by auto
+qed
+
+
 subsection \<open>Quickcheck setup\<close>
 
 text \<open>Setup adapted from sets.\<close>

--- a/src/HOL/Probability/Fin_Map.thy	Mon Jul 10 16:38:42 2017 +0200
+++ b/src/HOL/Probability/Fin_Map.thy	Mon Jul 10 18:53:38 2017 +0200
@@ -1352,4 +1352,4 @@
 
 end
 
-end
+end
\ No newline at end of file