# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1534534496 -7200
# Node ID e7e3776385ba52db7d94d75b58349907adaf179a
# Parent  7066e83dfe46a3acef19c4669505578bdc7f7df5
Finite_Map: monotonicity

diff -r 7066e83dfe46 -r e7e3776385ba src/HOL/Library/Finite_Map.thy
--- a/src/HOL/Library/Finite_Map.thy	Fri Aug 17 21:34:12 2018 +0200
+++ b/src/HOL/Library/Finite_Map.thy	Fri Aug 17 21:34:56 2018 +0200
@@ -491,6 +491,17 @@
 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