moving some division theorems to Ring_and_Field

--- a/src/HOL/Hyperreal/Lim.ML	Fri Dec 12 03:41:47 2003 +0100
+++ b/src/HOL/Hyperreal/Lim.ML	Fri Dec 12 15:05:18 2003 +0100
@@ -1074,11 +1074,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 (subgoal_tac "(\\<lambda>h. (- f (x + h) + - (- f x)) / h) = (\\<lambda>h. - ((f (x + h) + - f x) / h))" 1);
+by (dtac NSLIM_minus 1);
+by (subgoal_tac "ALL a::real. ALL b. - a + b = - (a + - b)" 1);
+by (asm_full_simp_tac (HOL_ss addsimps [thm"minus_divide_left" RS sym]) 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/Hyperreal/Series.ML	Fri Dec 12 03:41:47 2003 +0100
+++ b/src/HOL/Hyperreal/Series.ML	Fri Dec 12 15:05:18 2003 +0100
@@ -430,9 +430,8 @@
 by (auto_tac (claset() addSDs [LIMSEQ_rabs_realpow_zero2],
              simpset() addsimps [sumr_geometric ,sums_def,
                                  real_diff_def, real_add_divide_distrib]));
-by (subgoal_tac "1 / (1 + -x) = 0/(x - 1) + - 1/(x - 1)" 1);
-by (asm_full_simp_tac (simpset() addsimps [
-                      real_divide_minus_eq RS sym, real_diff_def]) 2); 
+by (subgoal_tac "1 / (1 + -x) = 0/(x - 1) + - 1/(x - 1)" 1); 
+by (asm_full_simp_tac (simpset() addsimps [thm"minus_divide_right"]) 2); 
 by (etac ssubst 1); 
 by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_divide 1);
 by (auto_tac (claset() addIs [LIMSEQ_const], 

--- a/src/HOL/Real/RealArith.thy	Fri Dec 12 03:41:47 2003 +0100
+++ b/src/HOL/Real/RealArith.thy	Fri Dec 12 15:05:18 2003 +0100
@@ -63,14 +63,16 @@
 
 (*** Density of the Reals ***)
 
+text{*Similar results are proved in @{text Ring_and_Field}*}
 lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)"
-by auto
+  by auto
 
 lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y"
-by auto
+  by auto
 
 lemma real_dense: "x < y ==> \<exists>r::real. x < r & r < y"
-by (blast intro!: real_less_half_sum real_gt_half_sum)
+  by (rule Ring_and_Field.dense)
+
 
 subsection{*Absolute Value Function for the Reals*}
 

--- a/src/HOL/Real/RealOrd.thy	Fri Dec 12 03:41:47 2003 +0100
+++ b/src/HOL/Real/RealOrd.thy	Fri Dec 12 15:05:18 2003 +0100
@@ -16,17 +16,11 @@
 subsection{*Properties of Less-Than Or Equals*}
 
 lemma real_leI: "~(w < z) ==> z \<le> (w::real)"
-apply (unfold real_le_def, assumption)
-done
+by (unfold real_le_def, assumption)
 
 lemma real_leD: "z\<le>w ==> ~(w<(z::real))"
 by (unfold real_le_def, assumption)
 
-lemmas real_leE = real_leD [elim_format]
-
-lemma real_less_le_iff: "(~(w < z)) = (z \<le> (w::real))"
-by (blast intro!: real_leI real_leD)
-
 lemma not_real_leE: "~ z \<le> w ==> w<(z::real)"
 by (unfold real_le_def, blast)
 
@@ -106,9 +100,7 @@
 by (blast intro!: real_less_all_preal real_leI)
 
 lemma real_of_preal_le_iff: "(real_of_preal m1 \<le> real_of_preal m2) = (m1 \<le> m2)"
-apply (auto intro!: preal_leI simp add: real_less_le_iff [symmetric])
-apply (drule order_le_less_trans, assumption)
-apply (erule preal_less_irrefl)
+apply (auto intro!: preal_leI simp add: linorder_not_less [symmetric])
 done
 
 
@@ -195,8 +187,8 @@
 
 lemma real_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::real)"
 apply (rule real_le_eqI [THEN iffD1]) 
- prefer 2 apply assumption; 
-apply (simp add: real_diff_def real_add_ac);
+ prefer 2 apply assumption
+apply (simp add: real_diff_def real_add_ac)
 done
 
 
@@ -295,26 +287,8 @@
 lemma real_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::real)"
   by (rule Ring_and_Field.inverse_mult_distrib)
 
-(** As with multiplication, pull minus signs OUT of the / operator **)
-
-lemma real_minus_divide_eq: "(-x) / (y::real) = - (x/y)"
-by (simp add: real_divide_def)
-declare real_minus_divide_eq [simp]
-
-lemma real_divide_minus_eq: "(x / -(y::real)) = - (x/y)"
-by (simp add: real_divide_def real_minus_inverse)
-declare real_divide_minus_eq [simp]
-
 lemma real_add_divide_distrib: "(x+y)/(z::real) = x/z + y/z"
-by (simp add: real_divide_def real_add_mult_distrib)
-
-(*The following would e.g. convert (x+y)/2 to x/2 + y/2.  Sometimes that
-  leads to cancellations in x or y, but is also prevents "multiplying out"
-  the 2 in e.g. (x+y)/2 = 5.
-
-Addsimps [inst "z" "number_of ?w" real_add_divide_distrib]
-**)
-
+  by (rule Ring_and_Field.add_divide_distrib)
 
 
 subsection{*More Lemmas*}
@@ -395,34 +369,6 @@
   by (rule Ring_and_Field.mult_divide_cancel_eq_if) 
 
 
-subsection{*For the @{text abel_cancel} Simproc (DELETE)*}
-
-lemma real_eq_eqI: "(x::real) - y = x' - y' ==> (x=y) = (x'=y')"
-apply safe
-apply (simp_all add: eq_diff_eq diff_eq_eq)
-done
-
-lemma real_add_minus_cancel: "z + ((- z) + w) = (w::real)"
-by (simp add: real_add_assoc [symmetric])
-
-lemma real_minus_add_cancel: "(-z) + (z + w) = (w::real)"
-by (simp add: real_add_assoc [symmetric])
-
-(*Deletion of other terms in the formula, seeking the -x at the front of z*)
-lemma real_add_cancel_21: "((x::real) + (y + z) = y + u) = ((x + z) = u)"
-apply (subst real_add_left_commute)
-apply (rule real_add_left_cancel)
-done
-
-(*A further rule to deal with the case that
-  everything gets cancelled on the right.*)
-lemma real_add_cancel_end: "((x::real) + (y + z) = y) = (x = -z)"
-apply (subst real_add_left_commute)
-apply (rule_tac t = y in real_add_zero_right [THEN subst], subst real_add_left_cancel)
-apply (simp add: real_diff_def eq_diff_eq [symmetric])
-done
-
-
 subsection{*Inverse and Division*}
 
 lemma real_inverse_gt_0: "0 < x ==> 0 < inverse (x::real)"
@@ -606,8 +552,7 @@
 
 lemma real_of_nat_diff [rule_format]:
      "n \<le> m --> real (m - n) = real (m::nat) - real n"
-apply (induct_tac "m")
-apply (simp add: );
+apply (induct_tac "m", simp)
 apply (simp add: real_diff_def Suc_diff_le le_Suc_eq real_of_nat_Suc add_ac)
 apply (simp add: add_left_commute [of _ "- 1"]) 
 done
@@ -649,11 +594,10 @@
 
 lemma real_of_posnat_ge_one: "1 <= real_of_posnat n"
 apply (simp (no_asm) add: real_of_posnat_one [symmetric])
-apply (induct_tac "n")
-apply (simp add: ); 
+apply (induct_tac "n", simp) 
 apply (simp add: real_of_posnat_Suc real_of_posnat_one order_less_imp_le)
 apply (rule add_le_cancel_right [THEN iffD1, of _ "- 1"]) 
-apply (simp add: add_assoc); 
+apply (simp add: add_assoc) 
 done
 declare real_of_posnat_ge_one [simp]
 
@@ -780,8 +724,7 @@
 declare real_of_nat_ge_zero_cancel_iff [simp]
 
 lemma real_of_nat_num_if: "real n = (if n=0 then 0 else 1 + real ((n::nat) - 1))"
-apply (case_tac "n")
-apply (simp add: ); 
+apply (case_tac "n", simp) 
 apply (simp add: real_of_nat_Suc add_commute)
 done
 
@@ -860,8 +803,6 @@
 val real_linear_less2 = thm"real_linear_less2";
 val real_leI = thm"real_leI";
 val real_leD = thm"real_leD";
-val real_leE = thm"real_leE";
-val real_less_le_iff = thm"real_less_le_iff";
 val not_real_leE = thm"not_real_leE";
 val real_le_imp_less_or_eq = thm"real_le_imp_less_or_eq";
 val real_less_or_eq_imp_le = thm"real_less_or_eq_imp_le";
@@ -937,8 +878,6 @@
 val real_inverse_1 = thm"real_inverse_1";
 val real_minus_inverse = thm"real_minus_inverse";
 val real_inverse_distrib = thm"real_inverse_distrib";
-val real_minus_divide_eq = thm"real_minus_divide_eq";
-val real_divide_minus_eq = thm"real_divide_minus_eq";
 val real_add_divide_distrib = thm"real_add_divide_distrib";
 
 val real_of_posnat_one = thm "real_of_posnat_one";
@@ -990,8 +929,6 @@
 
 val real_minus_add_distrib = thm"real_minus_add_distrib";
 val real_add_left_cancel = thm"real_add_left_cancel";
-val real_add_minus_cancel = thm"real_add_minus_cancel";
-val real_minus_add_cancel = thm"real_minus_add_cancel";
 *}
 
 end

--- a/src/HOL/Real/real_arith.ML	Fri Dec 12 03:41:47 2003 +0100
+++ b/src/HOL/Real/real_arith.ML	Fri Dec 12 15:05:18 2003 +0100
@@ -20,6 +20,16 @@
 
 (****Common factor cancellation****)
 
+(*To quote from Provers/Arith/cancel_numeral_factor.ML:
+
+This simproc Cancels common coefficients in balanced expressions:
+
+     u*#m ~~ u'*#m'  ==  #n*u ~~ #n'*u'
+
+where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
+and d = gcd(m,m') and n=m/d and n'=m'/d.
+*)
+
 val real_inverse_eq_divide = thm"real_inverse_eq_divide";
 val real_mult_less_cancel2 = thm"real_mult_less_cancel2";
 val real_mult_le_cancel2 = thm"real_mult_le_cancel2";
@@ -234,7 +244,8 @@
              inst "w" "number_of ?v" real_add_mult_distrib2,
              divide_1,times_divide_eq_right,times_divide_eq_left];
 
-val simprocs = [real_cancel_numeral_factors_divide];
+val simprocs = [real_cancel_numeral_factors_divide,
+                real_cancel_numeral_factors_divide];
 
 fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
 

--- a/src/HOL/Ring_and_Field.thy	Fri Dec 12 03:41:47 2003 +0100
+++ b/src/HOL/Ring_and_Field.thy	Fri Dec 12 15:05:18 2003 +0100
@@ -640,30 +640,6 @@
 by (simp add: mult_commute [of c] mult_cancel_right)
 
 
-subsection {* Absolute Value *}
-
-text{*But is it really better than just rewriting with @{text abs_if}?*}
-lemma abs_split:
-     "P(abs(a::'a::ordered_ring)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
-by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
-
-lemma abs_zero [simp]: "abs 0 = (0::'a::ordered_ring)"
-by (simp add: abs_if)
-
-lemma abs_mult: "abs (x * y) = abs x * abs (y::'a::ordered_ring)" 
-apply (case_tac "x=0 | y=0", force) 
-apply (auto elim: order_less_asym
-            simp add: abs_if mult_less_0_iff linorder_neq_iff
-                  minus_mult_left [symmetric] minus_mult_right [symmetric])  
-done
-
-lemma abs_eq_0 [simp]: "(abs x = 0) = (x = (0::'a::ordered_ring))"
-by (simp add: abs_if)
-
-lemma zero_less_abs_iff [simp]: "(0 < abs x) = (x ~= (0::'a::ordered_ring))"
-by (simp add: abs_if linorder_neq_iff)
-
-
 subsection {* Fields *}
 
 lemma right_inverse [simp]:
@@ -704,6 +680,14 @@
 lemma inverse_eq_divide: "inverse (a::'a::{field,division_by_zero}) = 1/a"
 by (simp add: divide_inverse_zero)
 
+lemma nonzero_add_divide_distrib: "c \<noteq> 0 ==> (a+b)/(c::'a::field) = a/c + b/c"
+by (simp add: divide_inverse left_distrib) 
+
+lemma add_divide_distrib: "(a+b)/(c::'a::{field,division_by_zero}) = a/c + b/c"
+apply (case_tac "c=0", simp) 
+apply (simp add: nonzero_add_divide_distrib) 
+done
+
 text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
       of an ordering.*}
 lemma field_mult_eq_0_iff: "(a*b = (0::'a::field)) = (a = 0 | b = 0)"
@@ -924,6 +908,37 @@
 by (simp add: divide_inverse_zero mult_assoc)
 
 
+subsection {* Division and Unary Minus *}
+
+lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"
+by (simp add: divide_inverse minus_mult_left)
+
+lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a/b) = a / -(b::'a::field)"
+by (simp add: divide_inverse nonzero_inverse_minus_eq minus_mult_right)
+
+lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a)/(-b) = a / (b::'a::field)"
+by (simp add: divide_inverse nonzero_inverse_minus_eq)
+
+lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::{field,division_by_zero})"
+apply (case_tac "b=0", simp) 
+apply (simp add: nonzero_minus_divide_left) 
+done
+
+lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
+apply (case_tac "b=0", simp) 
+by (rule nonzero_minus_divide_right) 
+
+text{*The effect is to extract signs from divisions*}
+declare minus_divide_left  [symmetric, simp]
+declare minus_divide_right [symmetric, simp]
+
+lemma minus_divide_divide [simp]:
+     "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
+apply (case_tac "b=0", simp) 
+apply (simp add: nonzero_minus_divide_divide) 
+done
+
+
 subsection {* Ordered Fields *}
 
 lemma positive_imp_inverse_positive: 
@@ -1279,4 +1294,92 @@
 done
 
 
+subsection {* Ordering Rules for Division *}
+
+lemma divide_strict_right_mono:
+     "[|a < b; 0 < c|] ==> a / c < b / (c::'a::ordered_field)"
+by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono 
+              positive_imp_inverse_positive) 
+
+lemma divide_right_mono:
+     "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{ordered_field,division_by_zero})"
+  by (force simp add: divide_strict_right_mono order_le_less) 
+
+
+text{*The last premise ensures that @{term a} and @{term b} 
+      have the same sign*}
+lemma divide_strict_left_mono:
+       "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
+by (force simp add: zero_less_mult_iff divide_inverse mult_strict_left_mono 
+      order_less_imp_not_eq order_less_imp_not_eq2  
+      less_imp_inverse_less less_imp_inverse_less_neg) 
+
+lemma divide_left_mono:
+     "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::ordered_field)"
+  apply (subgoal_tac "a \<noteq> 0 & b \<noteq> 0") 
+   prefer 2 
+   apply (force simp add: zero_less_mult_iff order_less_imp_not_eq) 
+  apply (case_tac "c=0", simp add: divide_inverse)
+  apply (force simp add: divide_strict_left_mono order_le_less) 
+  done
+
+lemma divide_strict_left_mono_neg:
+     "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
+  apply (subgoal_tac "a \<noteq> 0 & b \<noteq> 0") 
+   prefer 2 
+   apply (force simp add: zero_less_mult_iff order_less_imp_not_eq) 
+  apply (drule divide_strict_left_mono [of _ _ "-c"]) 
+   apply (simp_all add: mult_commute nonzero_minus_divide_left [symmetric]) 
+  done
+
+lemma divide_strict_right_mono_neg:
+     "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)"
+apply (drule divide_strict_right_mono [of _ _ "-c"], simp) 
+apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric]) 
+done
+
+
+subsection {* Ordered Fields are Dense *}
+
+lemma zero_less_two: "0 < (1+1::'a::ordered_field)"
+proof -
+  have "0 + 0 <  (1+1::'a::ordered_field)"
+    by (blast intro: zero_less_one add_strict_mono) 
+  thus ?thesis by simp
+qed
+
+lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"
+by (simp add: zero_less_two pos_less_divide_eq right_distrib) 
+
+lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"
+by (simp add: zero_less_two pos_divide_less_eq right_distrib) 
+
+lemma dense: "a < b ==> \<exists>r::'a::ordered_field. a < r & r < b"
+by (blast intro!: less_half_sum gt_half_sum)
+
+
+subsection {* Absolute Value *}
+
+text{*But is it really better than just rewriting with @{text abs_if}?*}
+lemma abs_split:
+     "P(abs(a::'a::ordered_ring)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
+by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
+
+lemma abs_zero [simp]: "abs 0 = (0::'a::ordered_ring)"
+by (simp add: abs_if)
+
+lemma abs_mult: "abs (x * y) = abs x * abs (y::'a::ordered_ring)" 
+apply (case_tac "x=0 | y=0", force) 
+apply (auto elim: order_less_asym
+            simp add: abs_if mult_less_0_iff linorder_neq_iff
+                  minus_mult_left [symmetric] minus_mult_right [symmetric])  
+done
+
+lemma abs_eq_0 [simp]: "(abs x = 0) = (x = (0::'a::ordered_ring))"
+by (simp add: abs_if)
+
+lemma zero_less_abs_iff [simp]: "(0 < abs x) = (x ~= (0::'a::ordered_ring))"
+by (simp add: abs_if linorder_neq_iff)
+
+
 end