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.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.37  text {* Simprules for comparisons where common factors can be cancelled. *}