# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1500241641 -7200
# Node ID e5ba49a72ab9c8725aa42c266e9527de8e59363a
# Parent  6ad54b84ca5ddd529fc3430cf54bc7913ed56e3a
fmap is finite

diff -r 6ad54b84ca5d -r e5ba49a72ab9 src/HOL/Library/Finite_Map.thy
--- a/src/HOL/Library/Finite_Map.thy	Sat Jul 15 21:40:24 2017 +0100
+++ b/src/HOL/Library/Finite_Map.thy	Sun Jul 16 23:47:21 2017 +0200
@@ -152,6 +152,28 @@
   shows "(list_all2 (rel_prod op = A) ===> rel_map A) map_of map_of"
 unfolding map_of_def by transfer_prover
 
+definition set_of_map :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<times> 'b) set" where
+"set_of_map m = {(k, v)|k v. m k = Some v}"
+
+lemma set_of_map_alt_def: "set_of_map m = (\<lambda>k. (k, the (m k))) ` dom m"
+unfolding set_of_map_def dom_def
+by auto
+
+lemma set_of_map_finite: "finite (dom m) \<Longrightarrow> finite (set_of_map m)"
+unfolding set_of_map_alt_def
+by auto
+
+lemma set_of_map_inj: "inj set_of_map"
+proof
+  fix x y
+  assume "set_of_map x = set_of_map y"
+  hence "(x a = Some b) = (y a = Some b)" for a b
+    unfolding set_of_map_def by auto
+  hence "x k = y k" for k
+    by (metis not_None_eq)
+  thus "x = y" ..
+qed
+
 end
 
 
@@ -575,6 +597,14 @@
 lemma fmsubset_restrict_fset_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmrestrict_fset A m \<subseteq>\<^sub>f fmrestrict_fset A n"
 unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
 
+lift_definition fset_of_fmap :: "('a, 'b) fmap \<Rightarrow> ('a \<times> 'b) fset" is set_of_map
+by (rule set_of_map_finite)
+
+lemma fset_of_fmap_inj[intro, simp]: "inj fset_of_fmap"
+apply rule
+apply transfer'
+using set_of_map_inj unfolding inj_def by auto
+
 lift_definition fmap_of_list :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) fmap"
   is map_of
   parametric map_of_transfer
@@ -1141,6 +1171,12 @@
     by auto
 qed
 
+instance fmap :: (finite, finite) finite
+proof
+  show "finite (UNIV :: ('a, 'b) fmap set)"
+    by (rule finite_imageD) auto
+qed
+
 lifting_update fmap.lifting
 lifting_forget fmap.lifting