diff -r 8dea233d4bae -r 8d1bf38c6fe6 src/HOL/Library/Finite_Map.thy
--- a/src/HOL/Library/Finite_Map.thy	Mon Jun 18 07:27:12 2018 +0200
+++ b/src/HOL/Library/Finite_Map.thy	Mon Jun 18 10:50:24 2018 +0200
@@ -5,20 +5,20 @@
 section \<open>Type of finite maps defined as a subtype of maps\<close>
 
 theory Finite_Map
-  imports FSet AList
+  imports FSet AList Conditional_Parametricity
   abbrevs "(=" = "\<subseteq>\<^sub>f"
 begin
 
 subsection \<open>Auxiliary constants and lemmas over @{type map}\<close>
 
+parametric_constant map_add_transfer[transfer_rule]: map_add_def
+parametric_constant map_of_transfer[transfer_rule]: map_of_def
+
 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> (=) ===> 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
@@ -58,32 +58,18 @@
 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 ===> (=)) 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
-      then show ?thesis
-        by cases auto
-    qed
-  then show "dom m = dom n"
-    by auto
-qed
+parametric_constant dom_transfer[transfer_rule]: dom_def
 
 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]:
-  "((=) ===> A ===> rel_map A ===> rel_map A) map_upd map_upd"
-unfolding map_upd_def[abs_def]
-by transfer_prover
+parametric_constant map_upd_transfer[transfer_rule]: map_upd_def
 
 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)"
 
+parametric_constant map_filter_transfer[transfer_rule]: map_filter_def
+
 lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of [(k, _) \<leftarrow> m. P k]"
 proof
   fix x
@@ -91,11 +77,6 @@
     by (induct m) (auto simp: map_filter_def)
 qed
 
-lemma map_filter_transfer[transfer_rule]:
-  "((=) ===> 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))"
@@ -111,48 +92,26 @@
 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]:
-  "((=) ===> rel_map A ===> rel_map A) map_drop map_drop"
-unfolding map_drop_def[abs_def]
-by transfer_prover
+parametric_constant map_drop_transfer[transfer_rule]: map_drop_def
 
 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]:
-  "((=) ===> rel_map A ===> rel_map A) map_drop_set map_drop_set"
-unfolding map_drop_set_def[abs_def]
-by transfer_prover
+parametric_constant map_drop_set_transfer[transfer_rule]: map_drop_set_def
 
 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]:
-  "((=) ===> 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) (++) (++)"
-unfolding map_add_def[abs_def]
-by transfer_prover
+parametric_constant map_restrict_set_transfer[transfer_rule]: map_restrict_set_def
 
 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]:
-  "(((=) ===> A ===> (=)) ===> rel_map A ===> (=)) map_pred map_pred"
-unfolding map_pred_def[abs_def]
-by transfer_prover
+parametric_constant map_pred_transfer[transfer_rule]: map_pred_def
 
 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 (=) 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}"
 
@@ -208,7 +167,7 @@
 lift_definition fmran :: "('a, 'b) fmap \<Rightarrow> 'b fset"
   is ran
   parametric ran_transfer
-unfolding ran_alt_def by auto
+by (rule finite_ran)
 
 lemma fmlookup_ran_iff: "y |\<in>| fmran m \<longleftrightarrow> (\<exists>x. fmlookup m x = Some y)"
 by transfer' (auto simp: ran_def)
@@ -259,7 +218,6 @@
 
 lift_definition fmempty :: "('a, 'b) fmap"
   is Map.empty
-  parametric map_empty_transfer
 by simp
 
 lemma fmempty_lookup[simp]: "fmlookup fmempty x = None"