additions to Ring_and_Field

--- a/src/HOL/Hyperreal/Lim.ML	Tue Nov 18 11:03:56 2003 +0100
+++ b/src/HOL/Hyperreal/Lim.ML	Wed Nov 19 14:29:06 2003 +0100
@@ -50,8 +50,9 @@
 qed "LIM_add";
 
 Goalw [LIM_def] "f -- a --> L ==> (%x. -f(x)) -- a --> -L";
-by (full_simp_tac (simpset() addsimps [real_minus_add_distrib RS sym] 
-                    delsimps [real_minus_add_distrib, real_minus_minus]) 1);
+by (subgoal_tac "ALL x. abs(- f x + L) = abs(f x + - L)" 1);
+by (Asm_full_simp_tac 1); 
+by (asm_full_simp_tac (simpset() addsimps [real_abs_def]) 1); 
 qed "LIM_minus";
 
 (*----------------------------------------------
@@ -1072,10 +1073,10 @@
 Goal "NSDERIV f x :> D ==> NSDERIV (%x. -(f x)) x :> -D";
 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff]) 1);
 by (res_inst_tac [("t","f x")] (real_minus_minus RS subst) 1);
-by (asm_simp_tac (simpset() addsimps [real_minus_add_distrib RS sym,
-                                      real_mult_minus_eq1] 
-                   delsimps [real_minus_add_distrib, real_minus_minus]) 1);
+by (subgoal_tac "(\\<lambda>h. (- f (x + h) + - (- f x)) / h) = (\\<lambda>h. - ((f (x + h) + - f x) / h))" 1);
+by (Asm_full_simp_tac 1); 
 by (etac NSLIM_minus 1);
+by (asm_full_simp_tac (simpset() addsimps [real_minus_divide_eq RS sym]) 1); 
 qed "NSDERIV_minus";
 
 Goal "DERIV f x :> D \

--- a/src/HOL/Library/Ring_and_Field.thy	Tue Nov 18 11:03:56 2003 +0100
+++ b/src/HOL/Library/Ring_and_Field.thy	Wed Nov 19 14:29:06 2003 +0100
@@ -85,7 +85,7 @@
   assume eq: "a + b = a + c"
   then have "(-a + a) + b = (-a + a) + c"
     by (simp only: eq add_assoc)
-  then show "b = c" by (simp add: )
+  then show "b = c" by simp
 next
   assume eq: "b = c"
   then show "a + b = a + c" by simp
@@ -95,6 +95,39 @@
      "(b + a = c + a) = (b = (c::'a::ring))"
   by (simp add: add_commute)
 
+lemma minus_minus [simp]: "- (- (a::'a::ring)) = a"
+  proof (rule add_left_cancel [of "-a", THEN iffD1])
+    show "(-a + -(-a) = -a + a)"
+    by simp
+  qed
+
+lemma equals_zero_I: "a+b = 0 ==> -a = (b::'a::ring)"
+apply (rule right_minus_eq [THEN iffD1, symmetric])
+apply (simp add: diff_minus add_commute) 
+done
+
+lemma minus_zero [simp]: "- 0 = (0::'a::ring)"
+by (simp add: equals_zero_I)
+
+lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ring))" 
+  proof 
+    assume "- a = - b"
+    then have "- (- a) = - (- b)"
+      by simp
+    then show "a=b"
+      by simp
+  next
+    assume "a=b"
+    then show "-a = -b"
+      by simp
+  qed
+
+lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::ring))"
+by (subst neg_equal_iff_equal [symmetric], simp)
+
+lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::ring))"
+by (subst neg_equal_iff_equal [symmetric], simp)
+
 
 subsubsection {* Derived rules for multiplication *}
 
@@ -159,4 +192,89 @@
 
 theorems ring_distrib = right_distrib left_distrib
 
+lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ring)"
+apply (rule equals_zero_I)
+apply (simp add: ring_add_ac) 
+done
+
+lemma minus_mult_left: "- (a * b) = (-a) * (b::'a::ring)"
+apply (rule equals_zero_I)
+apply (simp add: left_distrib [symmetric]) 
+done
+
+lemma minus_mult_right: "- (a * b) = a * -(b::'a::ring)"
+apply (rule equals_zero_I)
+apply (simp add: right_distrib [symmetric]) 
+done
+
+lemma right_diff_distrib: "a * (b - c) = a * b - a * (c::'a::ring)"
+by (simp add: right_distrib diff_minus 
+              minus_mult_left [symmetric] minus_mult_right [symmetric]) 
+
+
+subsubsection {* Ordering rules *}
+
+lemma add_right_mono: "a \<le> (b::'a::ordered_ring) ==> a + c \<le> b + c"
+by (simp add: add_commute [of _ c] add_left_mono)
+
+lemma le_imp_neg_le: "a \<le> (b::'a::ordered_ring) ==> -b \<le> -a"
+  proof -
+  assume "a\<le>b"
+  then have "-a+a \<le> -a+b"
+    by (rule add_left_mono) 
+  then have "0 \<le> -a+b"
+    by simp
+  then have "0 + (-b) \<le> (-a + b) + (-b)"
+    by (rule add_right_mono) 
+  then show ?thesis
+    by (simp add: add_assoc)
+  qed
+
+lemma neg_le_iff_le [simp]: "(-b \<le> -a) = (a \<le> (b::'a::ordered_ring))"
+  proof 
+    assume "- b \<le> - a"
+    then have "- (- a) \<le> - (- b)"
+      by (rule le_imp_neg_le)
+    then show "a\<le>b"
+      by simp
+  next
+    assume "a\<le>b"
+    then show "-b \<le> -a"
+      by (rule le_imp_neg_le)
+  qed
+
+lemma neg_le_0_iff_le [simp]: "(-a \<le> 0) = (0 \<le> (a::'a::ordered_ring))"
+by (subst neg_le_iff_le [symmetric], simp)
+
+lemma neg_0_le_iff_le [simp]: "(0 \<le> -a) = (a \<le> (0::'a::ordered_ring))"
+by (subst neg_le_iff_le [symmetric], simp)
+
+lemma neg_less_iff_less [simp]: "(-b < -a) = (a < (b::'a::ordered_ring))"
+by (force simp add: order_less_le) 
+
+lemma neg_less_0_iff_less [simp]: "(-a < 0) = (0 < (a::'a::ordered_ring))"
+by (subst neg_less_iff_less [symmetric], simp)
+
+lemma neg_0_less_iff_less [simp]: "(0 < -a) = (a < (0::'a::ordered_ring))"
+by (subst neg_less_iff_less [symmetric], simp)
+
+lemma mult_strict_right_mono:
+     "[|a < b; 0 < c|] ==> a * c < b * (c::'a::ordered_ring)"
+by (simp add: mult_commute [of _ c] mult_strict_left_mono)
+
+lemma mult_neg_left_mono:
+     "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring)"
+ apply (drule mult_strict_left_mono [of _ _ "-c"])
+apply (simp_all add: minus_mult_left [symmetric]) 
+done
+
+
+subsubsection{* Products of Signs *}
+
+lemma mult_pos: "[| (0::'a::ordered_ring) < a; 0 < b |] ==> 0 < a*b"
+by (drule mult_strict_left_mono [of 0 b], auto)
+
+lemma mult_pos_neg: "[| (0::'a::ordered_ring) < a; b < 0 |] ==> a*b < 0"
+by (drule mult_strict_left_mono [of b 0], auto)
+
 end