src/HOL/Library/Finite_Map.thy

 apply auto
 apply (rename_tac x y)
 apply (erule_tac x = x in fBallE)
 apply simp
 by (simp add: fmlookup_dom_iff)
+
+lemma fmpred_mono_strong:
+  assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x y \<Longrightarrow> Q x y"
+  shows "fmpred P m \<Longrightarrow> fmpred Q m"
+using assms unfolding fmpred_iff by auto
+
+lemma fmpred_mono[mono]: "P \<le> Q \<Longrightarrow> fmpred P \<le> fmpred Q"
+apply rule
+apply (rule fmpred_mono_strong[where P = P and Q = Q])
+apply auto
+done
 
 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)"