author Lars Hupel Mon, 10 Jul 2017 18:53:38 +0200 changeset 66259 4a2c9d32e7aa parent 66258 fb6efe575c6d child 66260 466d8e7ed170
finite sets are countable
 src/HOL/Library/FSet.thy file | annotate | diff | comparison | revisions src/HOL/Probability/Fin_Map.thy file | annotate | diff | comparison | revisions
```--- 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>

```--- a/src/HOL/Probability/Fin_Map.thy	Mon Jul 10 16:38:42 2017 +0200