# HG changeset patch
# User hoelzl
# Date 1399973751 -7200
# Node ID c49edf06f8e4f822cc4feb73d2b2b90fcf9f46b7
# Parent  d1a937cbf8582063ef46dce9093409b3abc50ec0
add mono rules for diff

diff -r d1a937cbf858 -r c49edf06f8e4 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Tue May 13 11:35:47 2014 +0200
+++ b/src/HOL/Groups.thy	Tue May 13 11:35:51 2014 +0200
@@ -1036,6 +1036,24 @@
   "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
   by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
 
+lemma diff_mono: "a \<le> b \<Longrightarrow> d \<le> c \<Longrightarrow> a - c \<le> b - d"
+  by (simp add: field_simps add_mono)
+
+lemma diff_left_mono: "b \<le> a \<Longrightarrow> c - a \<le> c - b"
+  by (simp add: field_simps)
+
+lemma diff_right_mono: "a \<le> b \<Longrightarrow> a - c \<le> b - c"
+  by (simp add: field_simps)
+
+lemma diff_strict_mono: "a < b \<Longrightarrow> d < c \<Longrightarrow> a - c < b - d"
+  by (simp add: field_simps add_strict_mono)
+
+lemma diff_strict_left_mono: "b < a \<Longrightarrow> c - a < c - b"
+  by (simp add: field_simps)
+
+lemma diff_strict_right_mono: "a < b \<Longrightarrow> a - c < b - c"
+  by (simp add: field_simps)
+
 end
 
 ML_file "Tools/group_cancel.ML"