# HG changeset patch
# User haftmann
# Date 1192692058 -7200
# Node ID a1ddc5206cb1d9aa1428f403bee9322be67e5603
# Parent  c2ec5e589d78659014180e8145065020ca5420d5
moved lemmas to OrderedGroup.thy

diff -r c2ec5e589d78 -r a1ddc5206cb1 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Thu Oct 18 09:20:57 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Thu Oct 18 09:20:58 2007 +0200
@@ -1977,8 +1977,8 @@
       apply (insert prems)
       apply (auto simp add: 
 	ring_simps 
-	iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]
-	iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id])
+	iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
+	iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
 	apply(drule (1) mult_nonneg_nonpos[of a b], simp)
 	apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
       done
@@ -2127,25 +2127,4 @@
   then show ?thesis by simp
 qed
 
-
-subsection {* Theorems for proof tools *}
-
-lemma add_mono_thms_ordered_semiring [noatp]:
-  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 [noatp]:
-  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