# HG changeset patch
# User paulson
# Date 1079689702 -3600
# Node ID aa973ba84f69b363a7e651bc037d57a51fd5e024
# Parent  00292f6f8d13be7ee45913bf96219bc4d52f589c
new thms

diff -r 00292f6f8d13 -r aa973ba84f69 src/HOL/Integ/NatSimprocs.thy
--- 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]
+
 
 
 
diff -r 00292f6f8d13 -r aa973ba84f69 src/HOL/Ring_and_Field.thy
--- 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 -