moved lemmas to OrderedGroup.thy
authorhaftmann
Thu Oct 18 09:20:58 2007 +0200 (2007-10-18)
changeset 25078a1ddc5206cb1
parent 25077 c2ec5e589d78
child 25079 db5fdc34f3af
moved lemmas to OrderedGroup.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Ring_and_Field.thy	Thu Oct 18 09:20:57 2007 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Thu Oct 18 09:20:58 2007 +0200
     1.3 @@ -1977,8 +1977,8 @@
     1.4        apply (insert prems)
     1.5        apply (auto simp add: 
     1.6  	ring_simps 
     1.7 -	iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]
     1.8 -	iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id])
     1.9 +	iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
    1.10 +	iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
    1.11  	apply(drule (1) mult_nonneg_nonpos[of a b], simp)
    1.12  	apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
    1.13        done
    1.14 @@ -2127,25 +2127,4 @@
    1.15    then show ?thesis by simp
    1.16  qed
    1.17  
    1.18 -
    1.19 -subsection {* Theorems for proof tools *}
    1.20 -
    1.21 -lemma add_mono_thms_ordered_semiring [noatp]:
    1.22 -  fixes i j k :: "'a\<Colon>pordered_ab_semigroup_add"
    1.23 -  shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
    1.24 -    and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
    1.25 -    and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
    1.26 -    and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
    1.27 -by (rule add_mono, clarify+)+
    1.28 -
    1.29 -lemma add_mono_thms_ordered_field [noatp]:
    1.30 -  fixes i j k :: "'a\<Colon>pordered_cancel_ab_semigroup_add"
    1.31 -  shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
    1.32 -    and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
    1.33 -    and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
    1.34 -    and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
    1.35 -    and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
    1.36 -by (auto intro: add_strict_right_mono add_strict_left_mono
    1.37 -  add_less_le_mono add_le_less_mono add_strict_mono)
    1.38 -
    1.39  end