src/HOL/Rings.thy
changeset 54489 03ff4d1e6784
parent 54250 7d2544dd3988
child 54703 499f92dc6e45
     1.1 --- a/src/HOL/Rings.thy	Tue Nov 19 01:30:14 2013 +0100
     1.2 +++ b/src/HOL/Rings.thy	Tue Nov 19 10:05:53 2013 +0100
     1.3 @@ -1058,6 +1058,34 @@
     1.4    "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
     1.5  by(subst abs_dvd_iff[symmetric]) simp
     1.6  
     1.7 +text {* The following lemmas can be proven in more generale structures, but
     1.8 +are dangerous as simp rules in absence of @{thm neg_equal_zero}, 
     1.9 +@{thm neg_less_pos}, @{thm neg_less_eq_nonneg}. *}
    1.10 +
    1.11 +lemma equation_minus_iff_1 [simp, no_atp]:
    1.12 +  "1 = - a \<longleftrightarrow> a = - 1"
    1.13 +  by (fact equation_minus_iff)
    1.14 +
    1.15 +lemma minus_equation_iff_1 [simp, no_atp]:
    1.16 +  "- a = 1 \<longleftrightarrow> a = - 1"
    1.17 +  by (subst minus_equation_iff, auto)
    1.18 +
    1.19 +lemma le_minus_iff_1 [simp, no_atp]:
    1.20 +  "1 \<le> - b \<longleftrightarrow> b \<le> - 1"
    1.21 +  by (fact le_minus_iff)
    1.22 +
    1.23 +lemma minus_le_iff_1 [simp, no_atp]:
    1.24 +  "- a \<le> 1 \<longleftrightarrow> - 1 \<le> a"
    1.25 +  by (fact minus_le_iff)
    1.26 +
    1.27 +lemma less_minus_iff_1 [simp, no_atp]:
    1.28 +  "1 < - b \<longleftrightarrow> b < - 1"
    1.29 +  by (fact less_minus_iff)
    1.30 +
    1.31 +lemma minus_less_iff_1 [simp, no_atp]:
    1.32 +  "- a < 1 \<longleftrightarrow> - 1 < a"
    1.33 +  by (fact minus_less_iff)
    1.34 +
    1.35  end
    1.36  
    1.37  text {* Simprules for comparisons where common factors can be cancelled. *}