# HG changeset patch
# User Andreas Lochbihler
# Date 1423659011 -3600
# Node ID 6949c8837e90426ec451cfd7d9d12390d6052d6d
# Parent  9bf568cc71a48f7356ba254c737c680715669e98
add monotonicity lemmas for rel_fun

diff -r 9bf568cc71a4 -r 6949c8837e90 src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Wed Feb 11 13:47:48 2015 +0100
+++ b/src/HOL/BNF_Def.thy	Wed Feb 11 13:50:11 2015 +0100
@@ -41,6 +41,14 @@
   shows "B (f x) (g y)"
   using assms by (simp add: rel_fun_def)
 
+lemma rel_fun_mono:
+  "\<lbrakk> rel_fun X A f g; \<And>x y. Y x y \<longrightarrow> X x y; \<And>x y. A x y \<Longrightarrow> B x y \<rbrakk> \<Longrightarrow> rel_fun Y B f g"
+by(simp add: rel_fun_def)
+
+lemma rel_fun_mono' [mono]:
+  "\<lbrakk> \<And>x y. Y x y \<longrightarrow> X x y; \<And>x y. A x y \<longrightarrow> B x y \<rbrakk> \<Longrightarrow> rel_fun X A f g \<longrightarrow> rel_fun Y B f g"
+by(simp add: rel_fun_def)
+
 definition rel_set :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"
   where "rel_set R = (\<lambda>A B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y))"