# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1499780075 -7200
# Node ID 04b626416eae10a043e81c8d72d83bee891c6beb
# Parent  130dea8500cb709aca5d4a1680820ce0db535052
fmaps are countable

diff -r 130dea8500cb -r 04b626416eae src/HOL/Library/Finite_Map.thy
--- a/src/HOL/Library/Finite_Map.thy	Tue Jul 11 12:24:27 2017 +0200
+++ b/src/HOL/Library/Finite_Map.thy	Tue Jul 11 15:34:35 2017 +0200
@@ -146,12 +146,12 @@
 
 definition rel_map_on_set :: "'a set \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c) \<Rightarrow> bool" where
 "rel_map_on_set S P = eq_onp (\<lambda>x. x \<in> S) ===> rel_option P"
-  
+
 lemma map_of_transfer[transfer_rule]:
   includes lifting_syntax
   shows "(list_all2 (rel_prod op = A) ===> rel_map A) map_of map_of"
 unfolding map_of_def by transfer_prover
-  
+
 end
 
 
@@ -465,7 +465,7 @@
 using assms
 by transfer' (auto simp: map_pred_def split: option.splits)
 
-lemma fmpredD[dest]: "fmpred P m \<Longrightarrow> fmlookup m x = Some y \<Longrightarrow> P x y" 
+lemma fmpredD[dest]: "fmpred P m \<Longrightarrow> fmlookup m x = Some y \<Longrightarrow> P x y"
 by transfer' (auto simp: map_pred_def split: option.split_asm)
 
 lemma fmpred_iff: "fmpred P m \<longleftrightarrow> (\<forall>x y. fmlookup m x = Some y \<longrightarrow> P x y)"
@@ -828,7 +828,62 @@
 
 declare fmap_generic_code[code]
 
+
+subsection \<open>Instances\<close>
+
+lemma exists_map_of:
+  assumes "finite (dom m)" shows "\<exists>xs. map_of xs = m"
+  using assms
+proof (induction "dom m" arbitrary: m)
+  case empty
+  hence "m = Map.empty"
+    by auto
+  moreover have "map_of [] = Map.empty"
+    by simp
+  ultimately show ?case
+    by blast
+next
+  case (insert x F)
+  hence "F = dom (map_drop x m)"
+    unfolding map_drop_def map_filter_def dom_def by auto
+  with insert have "\<exists>xs'. map_of xs' = map_drop x m"
+    by auto
+  then obtain xs' where "map_of xs' = map_drop x m"
+    ..
+  moreover obtain y where "m x = Some y"
+    using insert unfolding dom_def by blast
+  ultimately have "map_of ((x, y) # xs') = m"
+    using \<open>insert x F = dom m\<close>
+    unfolding map_drop_def map_filter_def
+    by auto
+  thus ?case
+    ..
+qed
+
+lemma exists_fmap_of_list: "\<exists>xs. fmap_of_list xs = m"
+by transfer (rule exists_map_of)
+
+lemma fmap_of_list_surj[simp, intro]: "surj fmap_of_list"
+proof -
+  have "x \<in> range fmap_of_list" for x :: "('a, 'b) fmap"
+    unfolding image_iff
+    using exists_fmap_of_list by (metis UNIV_I)
+  thus ?thesis by auto
+qed
+
+instance fmap :: (countable, countable) countable
+proof
+  obtain to_nat :: "('a \<times> 'b) list \<Rightarrow> nat" where "inj to_nat"
+    by (metis ex_inj)
+  moreover have "inj (inv fmap_of_list)"
+    using fmap_of_list_surj by (rule surj_imp_inj_inv)
+  ultimately have "inj (to_nat \<circ> inv fmap_of_list)"
+    by (rule inj_comp)
+  thus "\<exists>to_nat::('a, 'b) fmap \<Rightarrow> nat. inj to_nat"
+    by auto
+qed
+
 lifting_update fmap.lifting
 lifting_forget fmap.lifting
 
-end
+end
\ No newline at end of file
diff -r 130dea8500cb -r 04b626416eae src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Tue Jul 11 12:24:27 2017 +0200
+++ b/src/HOL/Probability/Fin_Map.thy	Tue Jul 11 15:34:35 2017 +0200
@@ -44,26 +44,6 @@
   done
 
 
-subsection \<open>Countable Finite Maps\<close>
-
-instance fmap :: (countable, countable) countable
-proof
-  obtain mapper where mapper: "\<And>fm :: 'a \<Rightarrow>\<^sub>F 'b. set (mapper fm) = domain fm"
-    by (metis finite_list[OF finite_domain])
-  have "inj (\<lambda>fm. map (\<lambda>i. (i, (fm)\<^sub>F i)) (mapper fm))" (is "inj ?F")
-  proof (rule inj_onI)
-    fix f1 f2 assume "?F f1 = ?F f2"
-    then have "map fst (?F f1) = map fst (?F f2)" by simp
-    then have "mapper f1 = mapper f2" by (simp add: comp_def)
-    then have "domain f1 = domain f2" by (simp add: mapper[symmetric])
-    with \<open>?F f1 = ?F f2\<close> show "f1 = f2"
-      unfolding \<open>mapper f1 = mapper f2\<close> map_eq_conv mapper
-      by (simp add: finmap_eq_iff)
-  qed
-  then show "\<exists>to_nat :: 'a \<Rightarrow>\<^sub>F 'b \<Rightarrow> nat. inj to_nat"
-    by (intro exI[of _ "to_nat \<circ> ?F"] inj_comp) auto
-qed
-
 subsection \<open>Constructor of Finite Maps\<close>
 
 lift_definition finmap_of::"'i set \<Rightarrow> ('i \<Rightarrow> 'a) \<Rightarrow> ('i \<Rightarrow>\<^sub>F 'a)" is