# HG changeset patch
# User haftmann
# Date 1178480969 -7200
# Node ID 6d2fd4e0f9844a5af4d1c8368189de7c54fe5454
# Parent  83b9f2d3fb3c760a5b5dbbd6520721c18527dfbc
added auxiliary lemmas for proof tools

diff -r 83b9f2d3fb3c -r 6d2fd4e0f984 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Sun May 06 21:49:27 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Sun May 06 21:49:29 2007 +0200
@@ -2067,4 +2067,24 @@
   then show ?thesis by simp
 qed
 
+subsection {* Theorems for proof tools *}
+
+lemma add_mono_thms_ordered_semiring:
+  fixes i j k :: "'a\<Colon>pordered_ab_semigroup_add"
+  shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
+    and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
+    and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
+    and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
+by (rule add_mono, clarify+)+
+
+lemma add_mono_thms_ordered_field:
+  fixes i j k :: "'a\<Colon>pordered_cancel_ab_semigroup_add"
+  shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
+    and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
+    and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
+    and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
+    and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
+by (auto intro: add_strict_right_mono add_strict_left_mono
+  add_less_le_mono add_le_less_mono add_strict_mono)
+
 end