--- a/src/HOL/Integ/NatSimprocs.thy Fri Mar 19 10:46:25 2004 +0100
+++ b/src/HOL/Integ/NatSimprocs.thy Fri Mar 19 10:48:22 2004 +0100
@@ -223,6 +223,12 @@
"-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
by (simp add: divide_inverse inverse_minus_eq)
+lemma half_gt_zero_iff:
+ "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))"
+by auto
+
+lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, simp]
+
--- a/src/HOL/Ring_and_Field.thy Fri Mar 19 10:46:25 2004 +0100
+++ b/src/HOL/Ring_and_Field.thy Fri Mar 19 10:48:22 2004 +0100
@@ -1648,6 +1648,14 @@
lemma abs_triangle_ineq: "abs (a+b) \<le> abs a + abs (b::'a::ordered_ring)"
by (force simp add: abs_le_iff abs_ge_self abs_ge_minus_self add_mono)
+lemma abs_diff_triangle_ineq:
+ "\<bar>(a::'a::ordered_ring) + b - (c+d)\<bar> \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>"
+proof -
+ have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
+ also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
+ finally show ?thesis .
+qed
+
lemma abs_mult_less:
"[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::ordered_ring)"
proof -