# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1502463289 -7200
# Node ID 4d2ce596f5050686df014a4c7a7d6d5d24742fea
# Parent  32084d7e6b598414e500e03f89ed6dbad450c3dd
fmap :: size

diff -r 32084d7e6b59 -r 4d2ce596f505 src/HOL/Library/Finite_Map.thy
--- a/src/HOL/Library/Finite_Map.thy	Fri Aug 11 14:29:30 2017 +0200
+++ b/src/HOL/Library/Finite_Map.thy	Fri Aug 11 16:54:49 2017 +0200
@@ -605,6 +605,13 @@
 apply transfer'
 using set_of_map_inj unfolding inj_def by auto
 
+lemma fset_of_fmap_iff[simp]: "(a, b) |\<in>| fset_of_fmap m \<longleftrightarrow> fmlookup m a = Some b"
+by transfer' (auto simp: set_of_map_def)
+
+lemma fset_of_fmap_iff'[simp]: "(a, b) \<in> fset (fset_of_fmap m) \<longleftrightarrow> fmlookup m a = Some b"
+by transfer' (auto simp: set_of_map_def)
+
+
 lift_definition fmap_of_list :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) fmap"
   is map_of
   parametric map_of_transfer
@@ -900,6 +907,47 @@
 lemma fmmap_subset[intro]: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmmap f m \<subseteq>\<^sub>f fmmap f n"
 by transfer' (auto simp: map_le_def)
 
+lemma fmmap_fset_of_fmap: "fset_of_fmap (fmmap f m) = (\<lambda>(k, v). (k, f v)) |`| fset_of_fmap m"
+including fset.lifting
+by transfer' (auto simp: set_of_map_def)
+
+
+subsection \<open>@{const size} setup\<close>
+
+definition size_fmap :: "('a \<Rightarrow> nat) \<Rightarrow> ('b \<Rightarrow> nat) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> nat" where
+[simp]: "size_fmap f g m = size_fset (\<lambda>(a, b). f a + g b) (fset_of_fmap m)"
+
+instantiation fmap :: (type, type) size begin
+
+definition size_fmap where
+size_fmap_overloaded_def: "size_fmap = Finite_Map.size_fmap (\<lambda>_. 0) (\<lambda>_. 0)"
+
+instance ..
+
+end
+
+lemma size_fmap_overloaded_simps[simp]: "size x = size (fset_of_fmap x)"
+unfolding size_fmap_overloaded_def
+by simp
+
+lemma fmap_size_o_map: "inj h \<Longrightarrow> size_fmap f g \<circ> fmmap h = size_fmap f (g \<circ> h)"
+  unfolding size_fmap_def
+  apply (auto simp: fun_eq_iff fmmap_fset_of_fmap)
+  apply (subst sum.reindex)
+  subgoal for m
+    using prod.inj_map[unfolded map_prod_def, of "\<lambda>x. x" h]
+    unfolding inj_on_def
+    by auto
+  subgoal
+    by (rule sum.cong) (auto split: prod.splits)
+  done
+
+setup \<open>
+BNF_LFP_Size.register_size_global @{type_name fmap} @{const_name size_fmap}
+  @{thm size_fmap_overloaded_def} @{thms size_fmap_def size_fmap_overloaded_simps}
+  @{thms fmap_size_o_map}
+\<close>
+
 
 subsection \<open>Additional operations\<close>