author Lars Hupel Sun, 16 Jul 2017 23:47:21 +0200 changeset 66282 e5ba49a72ab9 parent 66281 6ad54b84ca5d child 66283 adf3155c57e2 child 66284 378895354604
fmap is finite
```--- 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
```