# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1473972065 -7200
# Node ID a6cd18af8bf941cae81c622a9f3e8e2f5fe6b1dc
# Parent  d588f684ccaf1e5a93175b31cd8e5b11f3644419
new type for finite maps; use it in HOL-Probability

diff -r d588f684ccaf -r a6cd18af8bf9 src/HOL/Library/Finite_Map.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Finite_Map.thy	Thu Sep 15 22:41:05 2016 +0200
@@ -0,0 +1,837 @@
+(*  Title:      HOL/Library/Finite_Map.thy
+    Author:     Lars Hupel, TU München
+*)
+
+section \<open>Type of finite maps defined as a subtype of maps\<close>
+
+theory Finite_Map
+  imports FSet AList
+begin
+
+subsection \<open>Auxiliary constants and lemmas over @{type map}\<close>
+
+context includes lifting_syntax begin
+
+abbreviation rel_map :: "('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c) \<Rightarrow> bool" where
+"rel_map f \<equiv> op = ===> rel_option f"
+
+lemma map_empty_transfer[transfer_rule]: "rel_map A Map.empty Map.empty"
+by transfer_prover
+
+lemma ran_transfer[transfer_rule]: "(rel_map A ===> rel_set A) ran ran"
+proof
+  fix m n
+  assume "rel_map A m n"
+  show "rel_set A (ran m) (ran n)"
+    proof (rule rel_setI)
+      fix x
+      assume "x \<in> ran m"
+      then obtain a where "m a = Some x"
+        unfolding ran_def by auto
+
+      have "rel_option A (m a) (n a)"
+        using \<open>rel_map A m n\<close>
+        by (auto dest: rel_funD)
+      then obtain y where "n a = Some y" "A x y"
+        unfolding \<open>m a = _\<close>
+        by cases auto
+      thus "\<exists>y \<in> ran n. A x y"
+        unfolding ran_def by blast
+    next
+      fix y
+      assume "y \<in> ran n"
+      then obtain a where "n a = Some y"
+        unfolding ran_def by auto
+
+      have "rel_option A (m a) (n a)"
+        using \<open>rel_map A m n\<close>
+        by (auto dest: rel_funD)
+      then obtain x where "m a = Some x" "A x y"
+        unfolding \<open>n a = _\<close>
+        by cases auto
+      thus "\<exists>x \<in> ran m. A x y"
+        unfolding ran_def by blast
+    qed
+qed
+
+lemma ran_alt_def: "ran m = (the \<circ> m) ` dom m"
+unfolding ran_def dom_def by force
+
+lemma dom_transfer[transfer_rule]: "(rel_map A ===> op =) dom dom"
+proof
+  fix m n
+  assume "rel_map A m n"
+  have "m a \<noteq> None \<longleftrightarrow> n a \<noteq> None" for a
+    proof -
+      from \<open>rel_map A m n\<close> have "rel_option A (m a) (n a)"
+        unfolding rel_fun_def by auto
+      thus ?thesis
+        by cases auto
+    qed
+  thus "dom m = dom n"
+    by auto
+qed
+
+definition map_upd :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
+"map_upd k v m = m(k \<mapsto> v)"
+
+lemma map_upd_transfer[transfer_rule]:
+  "(op = ===> A ===> rel_map A ===> rel_map A) map_upd map_upd"
+unfolding map_upd_def[abs_def]
+by transfer_prover
+
+definition map_filter :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
+"map_filter P m = (\<lambda>x. if P x then m x else None)"
+
+lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of [(k, _) \<leftarrow> m. P k]"
+proof
+  fix x
+  show "map_filter P (map_of m) x = map_of [(k, _) \<leftarrow> m. P k] x"
+    by (induct m) (auto simp: map_filter_def)
+qed
+
+lemma map_filter_transfer[transfer_rule]:
+  "(op = ===> rel_map A ===> rel_map A) map_filter map_filter"
+unfolding map_filter_def[abs_def]
+by transfer_prover
+
+lemma map_filter_finite[intro]:
+  assumes "finite (dom m)"
+  shows "finite (dom (map_filter P m))"
+proof -
+  have "dom (map_filter P m) = Set.filter P (dom m)"
+    unfolding map_filter_def Set.filter_def dom_def
+    by auto
+  thus ?thesis
+    using assms
+    by (simp add: Set.filter_def)
+qed
+
+definition map_drop :: "'a \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
+"map_drop a = map_filter (\<lambda>a'. a' \<noteq> a)"
+
+lemma map_drop_transfer[transfer_rule]:
+  "(op = ===> rel_map A ===> rel_map A) map_drop map_drop"
+unfolding map_drop_def[abs_def]
+by transfer_prover
+
+definition map_drop_set :: "'a set \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
+"map_drop_set A = map_filter (\<lambda>a. a \<notin> A)"
+
+lemma map_drop_set_transfer[transfer_rule]:
+  "(op = ===> rel_map A ===> rel_map A) map_drop_set map_drop_set"
+unfolding map_drop_set_def[abs_def]
+by transfer_prover
+
+definition map_restrict_set :: "'a set \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
+"map_restrict_set A = map_filter (\<lambda>a. a \<in> A)"
+
+lemma map_restrict_set_transfer[transfer_rule]:
+  "(op = ===> rel_map A ===> rel_map A) map_restrict_set map_restrict_set"
+unfolding map_restrict_set_def[abs_def]
+by transfer_prover
+
+lemma map_add_transfer[transfer_rule]:
+  "(rel_map A ===> rel_map A ===> rel_map A) op ++ op ++"
+unfolding map_add_def[abs_def]
+by transfer_prover
+
+definition map_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" where
+"map_pred P m \<longleftrightarrow> (\<forall>x. case m x of None \<Rightarrow> True | Some y \<Rightarrow> P x y)"
+
+lemma map_pred_transfer[transfer_rule]:
+  "((op = ===> A ===> op =) ===> rel_map A ===> op =) map_pred map_pred"
+unfolding map_pred_def[abs_def]
+by transfer_prover
+
+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
+
+
+subsection \<open>Abstract characterisation\<close>
+
+typedef ('a, 'b) fmap = "{m. finite (dom m)} :: ('a \<rightharpoonup> 'b) set"
+  morphisms fmlookup Abs_fmap
+proof
+  show "Map.empty \<in> {m. finite (dom m)}"
+    by auto
+qed
+
+setup_lifting type_definition_fmap
+
+lemma fmlookup_finite[intro, simp]: "finite (dom (fmlookup m))"
+using fmap.fmlookup by auto
+
+lemma fmap_ext:
+  assumes "\<And>x. fmlookup m x = fmlookup n x"
+  shows "m = n"
+using assms
+by transfer' auto
+
+
+subsection \<open>Operations\<close>
+
+context
+  includes fset.lifting
+begin
+
+lift_definition fmran :: "('a, 'b) fmap \<Rightarrow> 'b fset"
+  is ran
+  parametric ran_transfer
+unfolding ran_alt_def by auto
+
+lemma fmranI: "fmlookup m x = Some y \<Longrightarrow> y |\<in>| fmran m" by transfer' (auto simp: ran_def)
+
+lift_definition fmdom :: "('a, 'b) fmap \<Rightarrow> 'a fset"
+  is dom
+  parametric dom_transfer
+.
+
+lemma fmdom_notI: "fmlookup m x = None \<Longrightarrow> x |\<notin>| fmdom m" by transfer' auto
+lemma fmdomI: "fmlookup m x = Some y \<Longrightarrow> x |\<in>| fmdom m" by transfer' auto
+
+lift_definition fmdom' :: "('a, 'b) fmap \<Rightarrow> 'a set"
+  is dom
+  parametric dom_transfer
+.
+
+lemma fmdom'_notI: "fmlookup m x = None \<Longrightarrow> x \<notin> fmdom' m" by transfer' auto
+lemma fmdom'I: "fmlookup m x = Some y \<Longrightarrow> x \<in> fmdom' m" by transfer' auto
+
+lemma fmdom'_alt_def: "fmdom' = fset \<circ> fmdom"
+by transfer' force
+
+lemma fmlookup_dom_iff: "x |\<in>| fmdom m \<longleftrightarrow> (\<exists>a. fmlookup m x = Some a)"
+by transfer' auto
+
+lift_definition fmempty :: "('a, 'b) fmap"
+  is Map.empty
+  parametric map_empty_transfer
+by simp
+
+lemma fmempty_lookup[simp]: "fmlookup fmempty x = None"
+by transfer' simp
+
+lemma fmdom_empty[simp]: "fmdom fmempty = {||}" by transfer' simp
+lemma fmdom'_empty[simp]: "fmdom' fmempty = {}" by transfer' simp
+
+lift_definition fmupd :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
+  is map_upd
+  parametric map_upd_transfer
+unfolding map_upd_def[abs_def]
+by simp
+
+lemma fmupd_lookup[simp]: "fmlookup (fmupd a b m) a' = (if a = a' then Some b else fmlookup m a')"
+by transfer' (auto simp: map_upd_def)
+
+lemma fmdom_fmupd[simp]: "fmdom (fmupd a b m) = finsert a (fmdom m)" by transfer (simp add: map_upd_def)
+lemma fmdom'_fmupd[simp]: "fmdom' (fmupd a b m) = insert a (fmdom' m)" by transfer (simp add: map_upd_def)
+
+lift_definition fmfilter :: "('a \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
+  is map_filter
+  parametric map_filter_transfer
+by auto
+
+lemma fmdom_filter[simp]: "fmdom (fmfilter P m) = ffilter P (fmdom m)"
+by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits)
+
+lemma fmdom'_filter[simp]: "fmdom' (fmfilter P m) = Set.filter P (fmdom' m)"
+by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits)
+
+lemma fmlookup_filter[simp]: "fmlookup (fmfilter P m) x = (if P x then fmlookup m x else None)"
+by transfer' (auto simp: map_filter_def)
+
+lemma fmfilter_empty[simp]: "fmfilter P fmempty = fmempty"
+by transfer' (auto simp: map_filter_def)
+
+lemma fmfilter_true[simp]: "(\<And>x. x |\<in>| fmdom m \<Longrightarrow> P x) \<Longrightarrow> fmfilter P m = m"
+apply transfer'
+apply (rule ext)
+apply (auto simp: map_filter_def)
+apply (case_tac "m x")
+apply simp
+apply simp
+apply (drule_tac m = m in domI)
+apply auto
+done
+
+lemma fmfilter_false[simp]: "(\<And>x. x |\<in>| fmdom m \<Longrightarrow> \<not> P x) \<Longrightarrow> fmfilter P m = fmempty"
+apply transfer'
+apply (rule ext)
+apply (auto simp: map_filter_def)
+done
+
+lemma fmfilter_comp[simp]: "fmfilter P (fmfilter Q m) = fmfilter (\<lambda>x. P x \<and> Q x) m"
+by transfer' (auto simp: map_filter_def)
+
+lemma fmfilter_comm: "fmfilter P (fmfilter Q m) = fmfilter Q (fmfilter P m)"
+unfolding fmfilter_comp by meson
+
+lemma fmfilter_cong[cong]:
+  assumes "\<And>x. x |\<in>| fmdom m \<Longrightarrow> P x = Q x"
+  shows "fmfilter P m = fmfilter Q m"
+using assms
+apply transfer'
+apply (rule ext)
+apply (auto simp: map_filter_def split: if_splits)
+apply (case_tac "m x")
+apply simp
+apply simp
+apply (drule_tac m = m in domI)
+apply auto
+done
+
+lemma fmfilter_cong'[fundef_cong]:
+  assumes "\<And>x. x \<in> fmdom' m \<Longrightarrow> P x = Q x"
+  shows "fmfilter P m = fmfilter Q m"
+apply (rule fmfilter_cong)
+using assms
+unfolding fmdom'_alt_def fmember.rep_eq
+by auto
+
+lemma fmfilter_upd[simp]: "fmfilter P (fmupd x y m) = (if P x then fmupd x y (fmfilter P m) else fmfilter P m)"
+by transfer' (auto simp: map_upd_def map_filter_def)
+
+lift_definition fmdrop :: "'a \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
+  is map_drop
+  parametric map_drop_transfer
+unfolding map_drop_def by auto
+
+lemma fmdrop_lookup[simp]: "fmlookup (fmdrop a m) a = None"
+by transfer' (auto simp: map_drop_def map_filter_def)
+
+lift_definition fmdrop_set :: "'a set \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
+  is map_drop_set
+  parametric map_drop_set_transfer
+unfolding map_drop_set_def by auto
+
+lift_definition fmdrop_fset :: "'a fset \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
+  is map_drop_set
+  parametric map_drop_set_transfer
+unfolding map_drop_set_def by auto
+
+lift_definition fmrestrict_set :: "'a set \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
+  is map_restrict_set
+  parametric map_restrict_set_transfer
+unfolding map_restrict_set_def by auto
+
+lemma fmrestrict_set_dom[simp]: "fmrestrict_set (fmdom' m) m = m"
+apply transfer'
+apply (auto simp: map_restrict_set_def map_filter_def)
+apply (rule ext)
+apply (auto split: if_splits)
+by (metis option.collapse)
+
+lift_definition fmrestrict_fset :: "'a fset \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap"
+  is map_restrict_set
+  parametric map_restrict_set_transfer
+unfolding map_restrict_set_def by auto
+
+lemma fmrestrict_fset_dom[simp]: "fmrestrict_fset (fmdom m) m = m"
+apply transfer'
+apply (auto simp: map_restrict_set_def map_filter_def)
+apply (rule ext)
+apply (auto split: if_splits)
+by (metis option.collapse)
+
+lemma fmfilter_alt_defs:
+  "fmdrop a = fmfilter (\<lambda>a'. a' \<noteq> a)"
+  "fmdrop_set A = fmfilter (\<lambda>a. a \<notin> A)"
+  "fmdrop_fset B = fmfilter (\<lambda>a. a |\<notin>| B)"
+  "fmrestrict_set A = fmfilter (\<lambda>a. a \<in> A)"
+  "fmrestrict_fset B = fmfilter (\<lambda>a. a |\<in>| B)"
+by (transfer'; simp add: map_drop_def map_drop_set_def map_restrict_set_def)+
+
+lemma fmdom_drop[simp]: "fmdom (fmdrop a m) = fmdom m - {|a|}" unfolding fmfilter_alt_defs by auto
+lemma fmdom'_drop[simp]: "fmdom' (fmdrop a m) = fmdom' m - {a}" unfolding fmfilter_alt_defs by auto
+lemma fmdom'_drop_set[simp]: "fmdom' (fmdrop_set A m) = fmdom' m - A" unfolding fmfilter_alt_defs by auto
+lemma fmdom_drop_fset[simp]: "fmdom (fmdrop_fset A m) = fmdom m - A" unfolding fmfilter_alt_defs by auto
+lemma fmdom'_restrict_set: "fmdom' (fmrestrict_set A m) \<subseteq> A" unfolding fmfilter_alt_defs by auto
+lemma fmdom_restrict_fset: "fmdom (fmrestrict_fset A m) |\<subseteq>| A" unfolding fmfilter_alt_defs by auto
+
+lemma fmdom'_drop_fset[simp]: "fmdom' (fmdrop_fset A m) = fmdom' m - fset A"
+unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def split: if_splits)
+
+lemma fmdom'_restrict_fset: "fmdom' (fmrestrict_fset A m) \<subseteq> fset A"
+unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def)
+
+lemma fmlookup_drop[simp]:
+  "fmlookup (fmdrop a m) x = (if x \<noteq> a then fmlookup m x else None)"
+unfolding fmfilter_alt_defs by simp
+
+lemma fmlookup_drop_set[simp]:
+  "fmlookup (fmdrop_set A m) x = (if x \<notin> A then fmlookup m x else None)"
+unfolding fmfilter_alt_defs by simp
+
+lemma fmlookup_drop_fset[simp]:
+  "fmlookup (fmdrop_fset A m) x = (if x |\<notin>| A then fmlookup m x else None)"
+unfolding fmfilter_alt_defs by simp
+
+lemma fmlookup_restrict_set[simp]:
+  "fmlookup (fmrestrict_set A m) x = (if x \<in> A then fmlookup m x else None)"
+unfolding fmfilter_alt_defs by simp
+
+lemma fmlookup_restrict_fset[simp]:
+  "fmlookup (fmrestrict_fset A m) x = (if x |\<in>| A then fmlookup m x else None)"
+unfolding fmfilter_alt_defs by simp
+
+lemma fmdrop_empty[simp]: "fmdrop a fmempty = fmempty"
+  unfolding fmfilter_alt_defs by simp
+
+lemma fmdrop_set_empty[simp]: "fmdrop_set A fmempty = fmempty"
+  unfolding fmfilter_alt_defs by simp
+
+lemma fmdrop_fset_empty[simp]: "fmdrop_fset A fmempty = fmempty"
+  unfolding fmfilter_alt_defs by simp
+
+lemma fmrestrict_set_empty[simp]: "fmrestrict_set A fmempty = fmempty"
+  unfolding fmfilter_alt_defs by simp
+
+lemma fmrestrict_fset_empty[simp]: "fmrestrict_fset A fmempty = fmempty"
+  unfolding fmfilter_alt_defs by simp
+
+lemma fmdrop_set_single[simp]: "fmdrop_set {a} m = fmdrop a m"
+  unfolding fmfilter_alt_defs by simp
+
+lemma fmdrop_fset_single[simp]: "fmdrop_fset {|a|} m = fmdrop a m"
+  unfolding fmfilter_alt_defs by simp
+
+lemma fmrestrict_set_null[simp]: "fmrestrict_set {} m = fmempty"
+  unfolding fmfilter_alt_defs by simp
+
+lemma fmrestrict_fset_null[simp]: "fmrestrict_fset {||} m = fmempty"
+  unfolding fmfilter_alt_defs by simp
+
+lemma fmdrop_comm: "fmdrop a (fmdrop b m) = fmdrop b (fmdrop a m)"
+unfolding fmfilter_alt_defs by (rule fmfilter_comm)
+
+lemma fmdrop_fmupd[simp]: "fmdrop x (fmupd x y m) = m"
+oops
+
+lift_definition fmadd :: "('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap" (infixl "++\<^sub>f" 100)
+  is map_add
+  parametric map_add_transfer
+by simp
+
+lemma fmdom_add[simp]: "fmdom (m ++\<^sub>f n) = fmdom m |\<union>| fmdom n" by transfer' auto
+lemma fmdom'_add[simp]: "fmdom' (m ++\<^sub>f n) = fmdom' m \<union> fmdom' n" by transfer' auto
+
+lemma fmadd_drop_left_dom: "fmdrop_fset (fmdom n) m ++\<^sub>f n = m ++\<^sub>f n"
+apply transfer'
+unfolding map_add_def dom_def map_drop_set_def map_filter_def
+by (rule ext) auto
+
+lemma fmadd_restrict_right_dom: "fmrestrict_fset (fmdom n) (m ++\<^sub>f n) = n"
+apply transfer'
+unfolding map_add_def dom_def map_restrict_set_def map_filter_def
+by (rule ext) auto
+
+lemma fmfilter_add_distrib[simp]: "fmfilter P (m ++\<^sub>f n) = fmfilter P m ++\<^sub>f fmfilter P n"
+by transfer' (auto simp: map_filter_def map_add_def)
+
+lemma fmdrop_add_distrib[simp]: "fmdrop a (m ++\<^sub>f n) = fmdrop a m ++\<^sub>f fmdrop a n"
+  unfolding fmfilter_alt_defs by simp
+
+lemma fmdrop_set_add_distrib[simp]: "fmdrop_set A (m ++\<^sub>f n) = fmdrop_set A m ++\<^sub>f fmdrop_set A n"
+  unfolding fmfilter_alt_defs by simp
+
+lemma fmdrop_fset_add_distrib[simp]: "fmdrop_fset A (m ++\<^sub>f n) = fmdrop_fset A m ++\<^sub>f fmdrop_fset A n"
+  unfolding fmfilter_alt_defs by simp
+
+lemma fmrestrict_set_add_distrib[simp]:
+  "fmrestrict_set A (m ++\<^sub>f n) = fmrestrict_set A m ++\<^sub>f fmrestrict_set A n"
+  unfolding fmfilter_alt_defs by simp
+
+lemma fmrestrict_fset_add_distrib[simp]:
+  "fmrestrict_fset A (m ++\<^sub>f n) = fmrestrict_fset A m ++\<^sub>f fmrestrict_fset A n"
+  unfolding fmfilter_alt_defs by simp
+
+lemma fmadd_empty[simp]: "fmempty ++\<^sub>f m = m" "m ++\<^sub>f fmempty = m"
+by (transfer'; auto)+
+
+lemma fmadd_idempotent[simp]: "m ++\<^sub>f m = m"
+by transfer' (auto simp: map_add_def split: option.splits)
+
+lemma fmadd_assoc[simp]: "m ++\<^sub>f (n ++\<^sub>f p) = m ++\<^sub>f n ++\<^sub>f p"
+by transfer' simp
+
+lemma fmlookup_add[simp]:
+  "fmlookup (m ++\<^sub>f n) x = (if x |\<in>| fmdom n then fmlookup n x else fmlookup m x)"
+  by transfer' (auto simp: map_add_def split: option.splits)
+
+lift_definition fmpred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> bool"
+  is map_pred
+  parametric map_pred_transfer
+.
+
+lemma fmpredI[intro]:
+  assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x y"
+  shows "fmpred P m"
+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" 
+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)"
+by auto
+
+lemma fmpred_alt_def: "fmpred P m \<longleftrightarrow> fBall (fmdom m) (\<lambda>x. P x (the (fmlookup m x)))"
+unfolding fmpred_iff
+apply auto
+apply (subst (asm) fmlookup_dom_iff)
+apply simp
+apply (erule_tac x = x in fBallE)
+apply simp
+by (simp add: fmlookup_dom_iff)
+
+lemma fmpred_empty[intro!, simp]: "fmpred P fmempty"
+by auto
+
+lemma fmpred_upd[intro]: "fmpred P m \<Longrightarrow> P x y \<Longrightarrow> fmpred P (fmupd x y m)"
+by transfer' (auto simp: map_pred_def map_upd_def)
+
+lemma fmpred_updD[dest]: "fmpred P (fmupd x y m) \<Longrightarrow> P x y"
+by auto
+
+lemma fmpred_add[intro]: "fmpred P m \<Longrightarrow> fmpred P n \<Longrightarrow> fmpred P (m ++\<^sub>f n)"
+by transfer' (auto simp: map_pred_def map_add_def split: option.splits)
+
+lemma fmpred_filter[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmfilter Q m)"
+by transfer' (auto simp: map_pred_def map_filter_def)
+
+lemma fmpred_drop[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop a m)"
+  by (auto simp: fmfilter_alt_defs)
+
+lemma fmpred_drop_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_set A m)"
+  by (auto simp: fmfilter_alt_defs)
+
+lemma fmpred_drop_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_fset A m)"
+  by (auto simp: fmfilter_alt_defs)
+
+lemma fmpred_restrict_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_set A m)"
+  by (auto simp: fmfilter_alt_defs)
+
+lemma fmpred_restrict_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_fset A m)"
+  by (auto simp: fmfilter_alt_defs)
+
+lemma fmpred_cases[consumes 1]:
+  assumes "fmpred P m"
+  obtains (none) "fmlookup m x = None" | (some) y where "fmlookup m x = Some y" "P x y"
+using assms by auto
+
+lift_definition fmsubset :: "('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> bool" (infix "\<subseteq>\<^sub>f" 50)
+  is map_le
+.
+
+lemma fmsubset_alt_def: "m \<subseteq>\<^sub>f n \<longleftrightarrow> fmpred (\<lambda>k v. fmlookup n k = Some v) m"
+by transfer' (auto simp: map_pred_def map_le_def dom_def split: option.splits)
+
+lemma fmsubset_pred: "fmpred P m \<Longrightarrow> n \<subseteq>\<^sub>f m \<Longrightarrow> fmpred P n"
+unfolding fmsubset_alt_def fmpred_iff
+by auto
+
+lemma fmsubset_filter_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmfilter P m \<subseteq>\<^sub>f fmfilter P n"
+unfolding fmsubset_alt_def fmpred_iff
+by auto
+
+lemma fmsubset_drop_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmdrop a m \<subseteq>\<^sub>f fmdrop a n"
+unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
+
+lemma fmsubset_drop_set_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmdrop_set A m \<subseteq>\<^sub>f fmdrop_set A n"
+unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
+
+lemma fmsubset_drop_fset_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmdrop_fset A m \<subseteq>\<^sub>f fmdrop_fset A n"
+unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
+
+lemma fmsubset_restrict_set_mono: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmrestrict_set A m \<subseteq>\<^sub>f fmrestrict_set A n"
+unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono)
+
+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 fmap_of_list :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) fmap"
+  is map_of
+  parametric map_of_transfer
+by (rule finite_dom_map_of)
+
+lemma fmap_of_list_simps[simp]:
+  "fmap_of_list [] = fmempty"
+  "fmap_of_list ((k, v) # kvs) = fmupd k v (fmap_of_list kvs)"
+by (transfer, simp add: map_upd_def)+
+
+lemma fmap_of_list_app[simp]: "fmap_of_list (xs @ ys) = fmap_of_list ys ++\<^sub>f fmap_of_list xs"
+by transfer' simp
+
+lemma fmupd_alt_def: "fmupd k v m = m ++\<^sub>f fmap_of_list [(k, v)]"
+by transfer' (auto simp: map_upd_def)
+
+lemma fmpred_of_list[intro]:
+  assumes "\<And>k v. (k, v) \<in> set xs \<Longrightarrow> P k v"
+  shows "fmpred P (fmap_of_list xs)"
+using assms
+by (induction xs) (transfer'; auto simp: map_pred_def)+
+
+lemma fmap_of_list_SomeD: "fmlookup (fmap_of_list xs) k = Some v \<Longrightarrow> (k, v) \<in> set xs"
+by transfer' (auto dest: map_of_SomeD)
+
+lift_definition fmrel_on_set :: "'a set \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap \<Rightarrow> bool"
+  is rel_map_on_set
+.
+
+lift_definition fmrel_on_fset :: "'a fset \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap \<Rightarrow> bool"
+  is rel_map_on_set
+.
+
+lemma fmrel_on_fset_alt_def: "fmrel_on_fset S P m n \<longleftrightarrow> fBall S (\<lambda>x. rel_option P (fmlookup m x) (fmlookup n x))"
+by transfer' (auto simp: rel_map_on_set_def eq_onp_def rel_fun_def)
+
+lemma rel_map_on_fsetI[intro]:
+  assumes "\<And>x. x |\<in>| S \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
+  shows "fmrel_on_fset S P m n"
+using assms
+unfolding fmrel_on_fset_alt_def by auto
+
+lemma fmrel_on_fset_mono[mono]: "R \<le> Q \<Longrightarrow> fmrel_on_fset S R \<le> fmrel_on_fset S Q"
+unfolding fmrel_on_fset_alt_def[abs_def]
+apply (intro le_funI fBall_mono)
+using option.rel_mono by auto
+
+lemma fmrel_on_fsetD: "x |\<in>| S \<Longrightarrow> fmrel_on_fset S P m n \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
+unfolding fmrel_on_fset_alt_def
+by auto
+
+lemma fmrel_on_fsubset: "fmrel_on_fset S R m n \<Longrightarrow> T |\<subseteq>| S \<Longrightarrow> fmrel_on_fset T R m n"
+unfolding fmrel_on_fset_alt_def
+by auto
+
+end
+
+
+subsection \<open>BNF setup\<close>
+
+lift_bnf ('a, fmran': 'b) fmap [wits: Map.empty]
+  for map: fmmap
+      rel: fmrel
+  by auto
+
+context includes lifting_syntax begin
+
+lemma fmmap_transfer[transfer_rule]:
+  "(op = ===> pcr_fmap op = op = ===> pcr_fmap op = op =) (\<lambda>f. op \<circ> (map_option f)) fmmap"
+apply (tactic \<open>Local_Defs.unfold_tac @{context} [BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.map_def_of_bnf]\<close>)
+apply (rule rel_funI ext)+
+apply (auto simp: fmap.Abs_fmap_inverse fmap.pcr_cr_eq cr_fmap_def)
+done
+
+lemma fmran'_transfer[transfer_rule]:
+  "(pcr_fmap op = op = ===> op =) (\<lambda>x. UNION (range x) set_option) fmran'"
+apply (tactic \<open>Local_Defs.unfold_tac @{context} (BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.set_defs_of_bnf)\<close>)
+unfolding fmap.pcr_cr_eq cr_fmap_def
+by fastforce
+
+lemma fmrel_transfer[transfer_rule]:
+  "(op = ===> pcr_fmap op = op = ===> pcr_fmap op = op = ===> op =) rel_map fmrel"
+apply (tactic \<open>Local_Defs.unfold_tac @{context} [BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.rel_def_of_bnf]\<close>)
+unfolding fmap.pcr_cr_eq cr_fmap_def vimage2p_def
+  by fastforce
+
+end
+
+
+lemma fmran'_alt_def: "fmran' = fset \<circ> fmran"
+including fset.lifting
+by transfer' (auto simp: ran_def fun_eq_iff)
+
+lemma fmran'I: "fmlookup m x = Some y \<Longrightarrow> y \<in> fmran' m"
+by transfer' auto
+
+lemma fmrel_iff: "fmrel R m n \<longleftrightarrow> (\<forall>x. rel_option R (fmlookup m x) (fmlookup n x))"
+by transfer' (auto simp: rel_fun_def)
+
+lemma fmrelI[intro]:
+  assumes "\<And>x. rel_option R (fmlookup m x) (fmlookup n x)"
+  shows "fmrel R m n"
+using assms
+by transfer' auto
+
+lemma fmempty_transfer[simp, intro, transfer_rule]: "fmrel P fmempty fmempty"
+by transfer auto
+
+lemma fmrel_upd[intro]: "fmrel P m n \<Longrightarrow> P x y \<Longrightarrow> fmrel P (fmupd k x m) (fmupd k y n)"
+by transfer' (auto simp: map_upd_def rel_fun_def)
+
+lemma fmrelD[dest]: "fmrel P m n \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
+by transfer' (auto simp: rel_fun_def)
+
+lemma fmrel_addI[intro]:
+  assumes "fmrel P m n" "fmrel P a b"
+  shows "fmrel P (m ++\<^sub>f a) (n ++\<^sub>f b)"
+using assms
+apply transfer'
+apply (auto simp: rel_fun_def map_add_def)
+by (metis option.case_eq_if option.collapse option.rel_sel)
+
+lemma fmrel_cases[consumes 1]:
+  assumes "fmrel P m n"
+  obtains (none) "fmlookup m x = None" "fmlookup n x = None"
+        | (some) a b where "fmlookup m x = Some a" "fmlookup n x = Some b" "P a b"
+proof -
+  from assms have "rel_option P (fmlookup m x) (fmlookup n x)"
+    by auto
+  thus thesis
+    using none some
+    by (cases rule: option.rel_cases) auto
+qed
+
+lemma fmrel_filter[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmfilter Q m) (fmfilter Q n)"
+unfolding fmrel_iff by auto
+
+lemma fmrel_drop[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop a m) (fmdrop a n)"
+  unfolding fmfilter_alt_defs by blast
+
+lemma fmrel_drop_set[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop_set A m) (fmdrop_set A n)"
+  unfolding fmfilter_alt_defs by blast
+
+lemma fmrel_drop_fset[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmdrop_fset A m) (fmdrop_fset A n)"
+  unfolding fmfilter_alt_defs by blast
+
+lemma fmrel_restrict_set[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmrestrict_set A m) (fmrestrict_set A n)"
+  unfolding fmfilter_alt_defs by blast
+
+lemma fmrel_restrict_fset[intro]: "fmrel P m n \<Longrightarrow> fmrel P (fmrestrict_fset A m) (fmrestrict_fset A n)"
+  unfolding fmfilter_alt_defs by blast
+
+lemma pred_fmap_fmpred[simp]: "pred_fmap P = fmpred (\<lambda>_. P)"
+unfolding fmap.pred_set fmran'_alt_def
+including fset.lifting
+apply transfer'
+apply (rule ext)
+apply (auto simp: map_pred_def ran_def split: option.splits dest: )
+done
+
+lemma pred_fmap_id[simp]: "pred_fmap id (fmmap f m) \<longleftrightarrow> pred_fmap f m"
+unfolding fmap.pred_set fmap.set_map
+by simp
+
+lemma fmlookup_map[simp]: "fmlookup (fmmap f m) x = map_option f (fmlookup m x)"
+apply (tactic \<open>Local_Defs.unfold_tac @{context} [BNF_Def.bnf_of @{context} @{type_name fmap} |> the |> BNF_Def.map_def_of_bnf]\<close>)
+apply (auto simp: fmap.Abs_fmap_inverse)
+done
+
+lemma fmpred_map[simp]: "fmpred P (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>k v. P k (f v)) m"
+unfolding fmpred_iff pred_fmap_def fmap.set_map
+by auto
+
+lemma fmpred_id[simp]: "fmpred (\<lambda>_. id) (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>_. f) m"
+by simp
+
+lemma fmmap_add[simp]: "fmmap f (m ++\<^sub>f n) = fmmap f m ++\<^sub>f fmmap f n"
+by transfer' (auto simp: map_add_def fun_eq_iff split: option.splits)
+
+lemma fmmap_empty[simp]: "fmmap f fmempty = fmempty"
+by transfer auto
+
+lemma fmdom_map[simp]: "fmdom (fmmap f m) = fmdom m"
+including fset.lifting
+by transfer' simp
+
+lemma fmdom'_map[simp]: "fmdom' (fmmap f m) = fmdom' m"
+by transfer' simp
+
+lemma fmfilter_fmmap[simp]: "fmfilter P (fmmap f m) = fmmap f (fmfilter P m)"
+by transfer' (auto simp: map_filter_def)
+
+lemma fmdrop_fmmap[simp]: "fmdrop a (fmmap f m) = fmmap f (fmdrop a m)" unfolding fmfilter_alt_defs by simp
+lemma fmdrop_set_fmmap[simp]: "fmdrop_set A (fmmap f m) = fmmap f (fmdrop_set A m)" unfolding fmfilter_alt_defs by simp
+lemma fmdrop_fset_fmmap[simp]: "fmdrop_fset A (fmmap f m) = fmmap f (fmdrop_fset A m)" unfolding fmfilter_alt_defs by simp
+lemma fmrestrict_set_fmmap[simp]: "fmrestrict_set A (fmmap f m) = fmmap f (fmrestrict_set A m)" unfolding fmfilter_alt_defs by simp
+lemma fmrestrict_fset_fmmap[simp]: "fmrestrict_fset A (fmmap f m) = fmmap f (fmrestrict_fset A m)" unfolding fmfilter_alt_defs by simp
+
+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)
+
+
+subsection \<open>Code setup\<close>
+
+instantiation fmap :: (type, equal) equal begin
+
+definition "equal_fmap \<equiv> fmrel HOL.equal"
+
+instance proof
+  fix m n :: "('a, 'b) fmap"
+  have "fmrel op = m n \<longleftrightarrow> (m = n)"
+    by transfer' (simp add: option.rel_eq rel_fun_eq)
+  thus "equal_class.equal m n \<longleftrightarrow> (m = n)"
+    unfolding equal_fmap_def
+    by (simp add: equal_eq[abs_def])
+qed
+
+end
+
+lemma fBall_alt_def: "fBall S P \<longleftrightarrow> (\<forall>x. x |\<in>| S \<longrightarrow> P x)"
+by force
+
+lemma fmrel_code:
+  "fmrel R m n \<longleftrightarrow>
+    fBall (fmdom m) (\<lambda>x. rel_option R (fmlookup m x) (fmlookup n x)) \<and>
+    fBall (fmdom n) (\<lambda>x. rel_option R (fmlookup m x) (fmlookup n x))"
+unfolding fmrel_iff fmlookup_dom_iff fBall_alt_def
+by (metis option.collapse option.rel_sel)
+
+lemmas fmap_generic_code =
+  fmrel_code
+  fmran'_alt_def
+  fmdom'_alt_def
+  fmfilter_alt_defs
+  pred_fmap_fmpred
+  fmsubset_alt_def
+  fmupd_alt_def
+  fmrel_on_fset_alt_def
+  fmpred_alt_def
+
+
+code_datatype fmap_of_list
+quickcheck_generator fmap constructors: fmap_of_list
+
+context includes fset.lifting begin
+
+lemma [code]: "fmlookup (fmap_of_list m) = map_of m"
+by transfer simp
+
+lemma [code]: "fmempty = fmap_of_list []"
+by transfer simp
+
+lemma [code]: "fmran (fmap_of_list m) = snd |`| fset_of_list (AList.clearjunk m)"
+by transfer (auto simp: ran_map_of)
+
+lemma [code]: "fmdom (fmap_of_list m) = fst |`| fset_of_list m"
+by transfer (auto simp: dom_map_of_conv_image_fst)
+
+lemma [code]: "fmfilter P (fmap_of_list m) = fmap_of_list (filter (\<lambda>(k, _). P k) m)"
+by transfer' auto
+
+lemma [code]: "fmap_of_list m ++\<^sub>f fmap_of_list n = fmap_of_list (AList.merge m n)"
+by transfer (simp add: merge_conv')
+
+lemma [code]: "fmmap f (fmap_of_list m) = fmap_of_list (map (apsnd f) m)"
+apply transfer
+apply (subst map_of_map[symmetric])
+apply (auto simp: apsnd_def map_prod_def)
+done
+
+end
+
+declare fmap_generic_code[code]
+
+lifting_update fmap.lifting
+lifting_forget fmap.lifting
+
+end
\ No newline at end of file
diff -r d588f684ccaf -r a6cd18af8bf9 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Thu Sep 15 19:31:17 2016 +0200
+++ b/src/HOL/Library/Library.thy	Thu Sep 15 22:41:05 2016 +0200
@@ -26,6 +26,7 @@
   Extended_Nonnegative_Real
   Extended_Real
   FinFun
+  Finite_Map
   Float
   Formal_Power_Series
   Fraction_Field
diff -r d588f684ccaf -r a6cd18af8bf9 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Thu Sep 15 19:31:17 2016 +0200
+++ b/src/HOL/Probability/Fin_Map.thy	Thu Sep 15 22:41:05 2016 +0200
@@ -5,29 +5,27 @@
 section \<open>Finite Maps\<close>
 
 theory Fin_Map
-imports Finite_Product_Measure
+  imports Finite_Product_Measure "~~/src/HOL/Library/Finite_Map"
 begin
 
-text \<open>Auxiliary type that is instantiated to @{class polish_space}, needed for the proof of
+text \<open>The @{type fmap} type can be instantiated to @{class polish_space}, needed for the proof of
   projective limit. @{const extensional} functions are used for the representation in order to
   stay close to the developments of (finite) products @{const Pi\<^sub>E} and their sigma-algebra
   @{const Pi\<^sub>M}.\<close>
 
-typedef ('i, 'a) finmap ("(_ \<Rightarrow>\<^sub>F /_)" [22, 21] 21) =
-  "{f::'i \<Rightarrow> 'a option. finite (dom f)}"
-  by (auto intro!: exI[where x="\<lambda>_. None"])
+type_notation fmap ("(_ \<Rightarrow>\<^sub>F /_)" [22, 21] 21)
 
-setup_lifting type_definition_finmap
+unbundle fmap.lifting
 
 
 subsection \<open>Domain and Application\<close>
 
-lift_definition domain::"('i, 'a) finmap \<Rightarrow> 'i set" is dom .
+lift_definition domain::"('i \<Rightarrow>\<^sub>F 'a) \<Rightarrow> 'i set" is dom .
 
 lemma finite_domain[simp, intro]: "finite (domain P)"
   by transfer simp
 
-lift_definition proj :: "('i, 'a) finmap \<Rightarrow> 'i \<Rightarrow> 'a" ("'((_)')\<^sub>F" [0] 1000) is
+lift_definition proj :: "('i \<Rightarrow>\<^sub>F 'a) \<Rightarrow> 'i \<Rightarrow> 'a" ("'((_)')\<^sub>F" [0] 1000) is
   "\<lambda>f x. if x \<in> dom f then the (f x) else undefined" .
 
 declare [[coercion proj]]
@@ -48,7 +46,7 @@
 
 subsection \<open>Countable Finite Maps\<close>
 
-instance finmap :: (countable, countable) countable
+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])
@@ -68,7 +66,7 @@
 
 subsection \<open>Constructor of Finite Maps\<close>
 
-lift_definition finmap_of::"'i set \<Rightarrow> ('i \<Rightarrow> 'a) \<Rightarrow> ('i, 'a) finmap" is
+lift_definition finmap_of::"'i set \<Rightarrow> ('i \<Rightarrow> 'a) \<Rightarrow> ('i \<Rightarrow>\<^sub>F 'a)" is
   "\<lambda>I f x. if x \<in> I \<and> finite I then Some (f x) else None"
   by (simp add: dom_def)
 
@@ -156,17 +154,17 @@
 
 subsection \<open>Topological Space of Finite Maps\<close>
 
-instantiation finmap :: (type, topological_space) topological_space
+instantiation fmap :: (type, topological_space) topological_space
 begin
 
-definition open_finmap :: "('a \<Rightarrow>\<^sub>F 'b) set \<Rightarrow> bool" where
-   [code del]: "open_finmap = generate_topology {Pi' a b|a b. \<forall>i\<in>a. open (b i)}"
+definition open_fmap :: "('a \<Rightarrow>\<^sub>F 'b) set \<Rightarrow> bool" where
+   [code del]: "open_fmap = generate_topology {Pi' a b|a b. \<forall>i\<in>a. open (b i)}"
 
 lemma open_Pi'I: "(\<And>i. i \<in> I \<Longrightarrow> open (A i)) \<Longrightarrow> open (Pi' I A)"
-  by (auto intro: generate_topology.Basis simp: open_finmap_def)
+  by (auto intro: generate_topology.Basis simp: open_fmap_def)
 
 instance using topological_space_generate_topology
-  by intro_classes (auto simp: open_finmap_def class.topological_space_def)
+  by intro_classes (auto simp: open_fmap_def class.topological_space_def)
 
 end
 
@@ -211,7 +209,7 @@
   shows "continuous_on s (\<lambda>x. (x)\<^sub>F i)"
   unfolding continuous_on_def by (safe intro!: tendsto_proj tendsto_ident_at)
 
-instance finmap :: (type, first_countable_topology) first_countable_topology
+instance fmap :: (type, first_countable_topology) first_countable_topology
 proof
   fix x::"'a\<Rightarrow>\<^sub>F'b"
   have "\<forall>i. \<exists>A. countable A \<and> (\<forall>a\<in>A. x i \<in> a) \<and> (\<forall>a\<in>A. open a) \<and>
@@ -229,7 +227,7 @@
     show "countable ?A" using A by (simp add: countable_PiE)
   next
     fix S::"('a \<Rightarrow>\<^sub>F 'b) set" assume "open S" "x \<in> S"
-    thus "\<exists>a\<in>?A. a \<subseteq> S" unfolding open_finmap_def
+    thus "\<exists>a\<in>?A. a \<subseteq> S" unfolding open_fmap_def
     proof (induct rule: generate_topology.induct)
       case UNIV thus ?case by (auto simp add: ex_in_conv PiE_eq_empty_iff A_notempty)
     next
@@ -266,29 +264,29 @@
 
 (* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
 
-instantiation finmap :: (type, metric_space) dist
+instantiation fmap :: (type, metric_space) dist
 begin
 
-definition dist_finmap where
+definition dist_fmap where
   "dist P Q = Max (range (\<lambda>i. dist ((P)\<^sub>F i) ((Q)\<^sub>F i))) + (if domain P = domain Q then 0 else 1)"
 
 instance ..
 end
 
-instantiation finmap :: (type, metric_space) uniformity_dist
+instantiation fmap :: (type, metric_space) uniformity_dist
 begin
 
 definition [code del]:
-  "(uniformity :: (('a, 'b) finmap \<times> ('a, 'b) finmap) filter) =
+  "(uniformity :: (('a, 'b) fmap \<times> ('a \<Rightarrow>\<^sub>F 'b)) filter) =
     (INF e:{0 <..}. principal {(x, y). dist x y < e})"
 
 instance
-  by standard (rule uniformity_finmap_def)
+  by standard (rule uniformity_fmap_def)
 end
 
-declare uniformity_Abort[where 'a="('a, 'b::metric_space) finmap", code]
+declare uniformity_Abort[where 'a="('a \<Rightarrow>\<^sub>F 'b::metric_space)", code]
 
-instantiation finmap :: (type, metric_space) metric_space
+instantiation fmap :: (type, metric_space) metric_space
 begin
 
 lemma finite_proj_image': "x \<notin> domain P \<Longrightarrow> finite ((P)\<^sub>F ` S)"
@@ -308,14 +306,14 @@
 
 lemma dist_le_1_imp_domain_eq:
   shows "dist P Q < 1 \<Longrightarrow> domain P = domain Q"
-  by (simp add: dist_finmap_def finite_proj_diag split: if_split_asm)
+  by (simp add: dist_fmap_def finite_proj_diag split: if_split_asm)
 
 lemma dist_proj:
   shows "dist ((x)\<^sub>F i) ((y)\<^sub>F i) \<le> dist x y"
 proof -
   have "dist (x i) (y i) \<le> Max (range (\<lambda>i. dist (x i) (y i)))"
     by (simp add: Max_ge_iff finite_proj_diag)
-  also have "\<dots> \<le> dist x y" by (simp add: dist_finmap_def)
+  also have "\<dots> \<le> dist x y" by (simp add: dist_fmap_def)
   finally show ?thesis .
 qed
 
@@ -326,7 +324,7 @@
   shows "dist P Q < e"
 proof -
   have "dist P Q = Max (range (\<lambda>i. dist (P i) (Q i)))"
-    using assms by (simp add: dist_finmap_def finite_proj_diag)
+    using assms by (simp add: dist_fmap_def finite_proj_diag)
   also have "\<dots> < e"
   proof (subst Max_less_iff, safe)
     fix i
@@ -343,7 +341,7 @@
   proof
     assume "open S"
     thus ?od
-      unfolding open_finmap_def
+      unfolding open_fmap_def
     proof (induct rule: generate_topology.induct)
       case UNIV thus ?case by (auto intro: zero_less_one)
     next
@@ -383,7 +381,7 @@
             show "domain y = a" using d s \<open>a \<noteq> {}\<close> by (auto simp: dist_le_1_imp_domain_eq a_dom)
             fix i assume i: "i \<in> a"
             hence "dist ((y)\<^sub>F i) ((x)\<^sub>F i) < es i" using d
-              by (auto simp: dist_finmap_def \<open>a \<noteq> {}\<close> intro!: le_less_trans[OF dist_proj])
+              by (auto simp: dist_fmap_def \<open>a \<noteq> {}\<close> intro!: le_less_trans[OF dist_proj])
             with i show "y i \<in> b i" by (rule in_b)
           qed
         next
@@ -410,23 +408,23 @@
       moreover
       assume "x \<in> (\<Pi>' i\<in>domain y. ball (y i) (e y))"
       hence "dist x y < e y" using e_pos \<open>y \<in> S\<close>
-        by (auto simp: dist_finmap_def Pi'_iff finite_proj_diag dist_commute)
+        by (auto simp: dist_fmap_def Pi'_iff finite_proj_diag dist_commute)
       ultimately show "x \<in> S" by (rule e_in)
     qed
     also have "open \<dots>"
-      unfolding open_finmap_def
+      unfolding open_fmap_def
       by (intro generate_topology.UN) (auto intro: generate_topology.Basis)
     finally show "open S" .
   qed
   show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
     unfolding * eventually_uniformity_metric
-    by (simp del: split_paired_All add: dist_finmap_def dist_commute eq_commute)
+    by (simp del: split_paired_All add: dist_fmap_def dist_commute eq_commute)
 next
   fix P Q::"'a \<Rightarrow>\<^sub>F 'b"
   have Max_eq_iff: "\<And>A m. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (Max A = m) = (m \<in> A \<and> (\<forall>a\<in>A. a \<le> m))"
     by (auto intro: Max_in Max_eqI)
   show "dist P Q = 0 \<longleftrightarrow> P = Q"
-    by (auto simp: finmap_eq_iff dist_finmap_def Max_ge_iff finite_proj_diag Max_eq_iff
+    by (auto simp: finmap_eq_iff dist_fmap_def Max_ge_iff finite_proj_diag Max_eq_iff
         add_nonneg_eq_0_iff
       intro!: Max_eqI image_eqI[where x=undefined])
 next
@@ -435,14 +433,14 @@
   let ?dpq = "?dists P Q" and ?dpr = "?dists P R" and ?dqr = "?dists Q R"
   let ?dom = "\<lambda>P Q. (if domain P = domain Q then 0 else 1::real)"
   have "dist P Q = Max (range ?dpq) + ?dom P Q"
-    by (simp add: dist_finmap_def)
+    by (simp add: dist_fmap_def)
   also obtain t where "t \<in> range ?dpq" "t = Max (range ?dpq)" by (simp add: finite_proj_diag)
   then obtain i where "Max (range ?dpq) = ?dpq i" by auto
   also have "?dpq i \<le> ?dpr i + ?dqr i" by (rule dist_triangle2)
   also have "?dpr i \<le> Max (range ?dpr)" by (simp add: finite_proj_diag)
   also have "?dqr i \<le> Max (range ?dqr)" by (simp add: finite_proj_diag)
   also have "?dom P Q \<le> ?dom P R + ?dom Q R" by simp
-  finally show "dist P Q \<le> dist P R + dist Q R" by (simp add: dist_finmap_def ac_simps)
+  finally show "dist P Q \<le> dist P R + dist Q R" by (simp add: dist_fmap_def ac_simps)
 qed
 
 end
@@ -468,10 +466,10 @@
     ultimately show ?case by eventually_elim auto
   qed simp
   thus "eventually (\<lambda>x. dist (f x) g < e) sequentially"
-    by eventually_elim (auto simp add: dist_finmap_def finite_proj_diag ind_f \<open>0 < e\<close>)
+    by eventually_elim (auto simp add: dist_fmap_def finite_proj_diag ind_f \<open>0 < e\<close>)
 qed
 
-instance finmap :: (type, complete_space) complete_space
+instance fmap :: (type, complete_space) complete_space
 proof
   fix P::"nat \<Rightarrow> 'a \<Rightarrow>\<^sub>F 'b"
   assume "Cauchy P"
@@ -483,7 +481,7 @@
   define p where "p i n = P n i" for i n
   define q where "q i = lim (p i)" for i
   define Q where "Q = finmap_of d q"
-  have q: "\<And>i. i \<in> d \<Longrightarrow> q i = Q i" by (auto simp add: Q_def Abs_finmap_inverse)
+  have q: "\<And>i. i \<in> d \<Longrightarrow> q i = Q i" by (auto simp add: Q_def Abs_fmap_inverse)
   {
     fix i assume "i \<in> d"
     have "Cauchy (p i)" unfolding cauchy p_def
@@ -520,7 +518,7 @@
     proof (safe intro!: exI[where x="N"])
       fix n assume "N \<le> n"
       hence dom: "domain (P n) = d" "domain Q = d" "domain (P n) = domain Q"
-        using dim by (simp_all add: N_def Q_def dim_def Abs_finmap_inverse)
+        using dim by (simp_all add: N_def Q_def dim_def Abs_fmap_inverse)
       show "dist (P n) Q < e"
       proof (rule dist_finmap_lessI[OF dom(3) \<open>0 < e\<close>])
         fix i
@@ -537,7 +535,7 @@
 
 subsection \<open>Second Countable Space of Finite Maps\<close>
 
-instantiation finmap :: (countable, second_countable_topology) second_countable_topology
+instantiation fmap :: (countable, second_countable_topology) second_countable_topology
 begin
 
 definition basis_proj::"'b set set"
@@ -590,7 +588,7 @@
   assume O': "open O'" "x \<in> O'"
   then obtain a where a:
     "x \<in> Pi' (domain x) a" "Pi' (domain x) a \<subseteq> O'" "\<And>i. i\<in>domain x \<Longrightarrow> open (a i)"
-    unfolding open_finmap_def
+    unfolding open_fmap_def
   proof (atomize_elim, induct rule: generate_topology.induct)
     case (Int a b)
     let ?p="\<lambda>a f. x \<in> Pi' (domain x) f \<and> Pi' (domain x) f \<subseteq> a \<and> (\<forall>i. i \<in> domain x \<longrightarrow> open (f i))"
@@ -630,7 +628,7 @@
 
 subsection \<open>Polish Space of Finite Maps\<close>
 
-instance finmap :: (countable, polish_space) polish_space proof qed
+instance fmap :: (countable, polish_space) polish_space proof qed
 
 
 subsection \<open>Product Measurable Space of Finite Maps\<close>
diff -r d588f684ccaf -r a6cd18af8bf9 src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Thu Sep 15 19:31:17 2016 +0200
+++ b/src/HOL/Probability/Projective_Limit.thy	Thu Sep 15 22:41:05 2016 +0200
@@ -455,8 +455,6 @@
 hide_const (open) PiF
 hide_const (open) Pi\<^sub>F
 hide_const (open) Pi'
-hide_const (open) Abs_finmap
-hide_const (open) Rep_finmap
 hide_const (open) finmap_of
 hide_const (open) proj
 hide_const (open) domain
@@ -477,7 +475,7 @@
   product_prob_space "\<lambda>_. borel::('a::polish_space) measure" I for I::"'i set"
 
 sublocale polish_product_prob_space \<subseteq> P: polish_projective I "\<lambda>J. PiM J (\<lambda>_. borel::('a) measure)"
-proof qed
+  ..
 
 lemma (in polish_product_prob_space) limP_eq_PiM: "lim = PiM I (\<lambda>_. borel)"
   by (rule PiM_eq) (auto simp: emeasure_PiM emeasure_lim_emb)
diff -r d588f684ccaf -r a6cd18af8bf9 src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Sep 15 19:31:17 2016 +0200
+++ b/src/HOL/ROOT	Thu Sep 15 22:41:05 2016 +0200
@@ -739,6 +739,7 @@
     "~~/src/HOL/Library/Permutation"
     "~~/src/HOL/Library/Order_Continuity"
     "~~/src/HOL/Library/Diagonal_Subsequence"
+    "~~/src/HOL/Library/Finite_Map"
   theories
     Probability
   document_files "root.tex"