# HG changeset patch
# User nipkow
# Date 1182711341 -7200
# Node ID 2f4be6844f7ca326eb8e812f18d8253ec84fe25d
# Parent  93dca7620d0d4e332999545294116ac36bafde99
tuned and used field_simps

diff -r 93dca7620d0d -r 2f4be6844f7c src/HOL/Hyperreal/Ln.thy
--- a/src/HOL/Hyperreal/Ln.thy	Sun Jun 24 20:47:05 2007 +0200
+++ b/src/HOL/Hyperreal/Ln.thy	Sun Jun 24 20:55:41 2007 +0200
@@ -36,12 +36,7 @@
 proof (induct n)
   show "inverse (real (fact (0 + 2))) * x ^ (0 + 2) <= 
       x ^ 2 / 2 * (1 / 2) ^ 0"
-    apply (simp add: power2_eq_square)
-    apply (subgoal_tac "real (Suc (Suc 0)) = 2")
-    apply (erule ssubst)
-    apply simp
-    apply simp
-    done
+    by (simp add: real_of_nat_Suc power2_eq_square)
 next
   fix n
   assume c: "inverse (real (fact (n + 2))) * x ^ (n + 2)
@@ -147,12 +142,6 @@
     by auto
 qed
 
-lemma aux3: "(0::real) <= x ==> (1 + x + x^2)/(1 + x^2) <= 1 + x"
-  apply (subst pos_divide_le_eq)
-  apply (simp add: zero_compare_simps)
-  apply (simp add: ring_simps zero_compare_simps)
-done
-
 lemma aux4: "0 <= (x::real) ==> x <= 1 ==> exp (x - x^2) <= 1 + x" 
 proof -
   assume a: "0 <= x" and b: "x <= 1"
@@ -175,7 +164,7 @@
     apply auto
     done
   also from a have "... <= 1 + x"
-    by (rule aux3)
+    by(simp add:field_simps zero_compare_simps)
   finally show ?thesis .
 qed
 
@@ -245,18 +234,7 @@
       by (insert a, auto)
     finally show ?thesis .
   qed
-  also have " 1 / (1 - x) = 1 + x / (1 - x)"
-  proof -
-    have "1 / (1 - x) = (1 - x + x) / (1 - x)"
-      by auto
-    also have "... = (1 - x) / (1 - x) + x / (1 - x)"
-      by (rule add_divide_distrib)
-    also have "... = 1 + x / (1-x)"
-      apply (subst add_right_cancel)
-      apply (insert a, simp)
-      done
-    finally show ?thesis .
-  qed
+  also have " 1 / (1 - x) = 1 + x / (1 - x)" using a by(simp add:field_simps)
   finally show ?thesis .
 qed
 
@@ -280,13 +258,10 @@
   also have "- (x / (1 - x)) = -x / (1 - x)"
     by auto
   finally have d: "- x / (1 - x) <= ln (1 - x)" .
-  have e: "-x - 2 * x^2 <= - x / (1 - x)"
-    apply (rule mult_imp_le_div_pos)
-    apply (insert prems, force)
-    apply (auto simp add: ring_simps power2_eq_square)
-    apply(insert mult_right_le_one_le[of "x*x" "2*x"])
-    apply (simp)
-    done
+  have "0 < 1 - x" using prems by simp
+  hence e: "-x - 2 * x^2 <= - x / (1 - x)"
+    using mult_right_le_one_le[of "x*x" "2*x"] prems
+    by(simp add:field_simps power2_eq_square)
   from e d show "- x - 2 * x^2 <= ln (1 - x)"
     by (rule order_trans)
 qed
@@ -427,21 +402,15 @@
     done
   also have "y / x = (x + (y - x)) / x"
     by simp
-  also have "... = 1 + (y - x) / x"
-    apply (simp only: add_divide_distrib)
-    apply (simp add: prems)
-    apply (insert a, arith)
-    done
+  also have "... = 1 + (y - x) / x" using a prems by(simp add:field_simps)
   also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
     apply (rule mult_left_mono)
     apply (rule ln_add_one_self_le_self)
     apply (rule divide_nonneg_pos)
     apply (insert prems a, simp_all) 
     done
-  also have "... = y - x"
-    by (insert a, simp)
-  also have "... = (y - x) * ln (exp 1)"
-    by simp
+  also have "... = y - x" using a by simp
+  also have "... = (y - x) * ln (exp 1)" by simp
   also have "... <= (y - x) * ln x"
     apply (rule mult_left_mono)
     apply (subst ln_le_cancel_iff)
@@ -454,18 +423,9 @@
     by (rule left_diff_distrib)
   finally have "x * ln y <= y * ln x"
     by arith
-  then have "ln y <= (y * ln x) / x"
-    apply (subst pos_le_divide_eq)
-    apply (rule a)
-    apply (simp add: mult_ac)
-    done
-  also have "... = y * (ln x / x)"
-    by simp
-  finally show ?thesis 
-    apply (subst pos_divide_le_eq)
-    apply (rule b)
-    apply (simp add: mult_ac)
-    done
+  then have "ln y <= (y * ln x) / x" using a by(simp add:field_simps)
+  also have "... = y * (ln x / x)"  by simp
+  finally show ?thesis using b by(simp add:field_simps)
 qed
 
 end
diff -r 93dca7620d0d -r 2f4be6844f7c src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Sun Jun 24 20:47:05 2007 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Sun Jun 24 20:55:41 2007 +0200
@@ -904,8 +904,7 @@
     have "norm (X m - X n) = norm ((X m - a) - (X n - a))" by simp
     also have "\<dots> \<le> norm (X m - a) + norm (X n - a)"
       by (rule norm_triangle_ineq4)
-    also from m n have "\<dots> < e/2 + e/2" by (rule add_strict_mono)
-    also have "e/2 + e/2 = e" by simp
+    also from m n have "\<dots> < e" by(simp add:field_simps)
     finally show "norm (X m - X n) < e" .
   qed
 qed
@@ -988,22 +987,17 @@
 
   from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast
   hence "X N - r/2 \<in> S" by (rule mem_S)
-  hence "X N - r/2 \<le> x" using x isLub_isUb isUbD by fast
-  hence 1: "X N + r/2 \<le> x + r" by simp
+  hence 1: "X N - r/2 \<le> x" using x isLub_isUb isUbD by fast
 
   from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast
   hence "isUb UNIV S (X N + r/2)" by (rule bound_isUb)
-  hence "x \<le> X N + r/2" using x isLub_le_isUb by fast
-  hence 2: "x - r \<le> X N - r/2" by simp
+  hence 2: "x \<le> X N + r/2" using x isLub_le_isUb by fast
 
   show "\<exists>N. \<forall>n\<ge>N. norm (X n - x) < r"
   proof (intro exI allI impI)
     fix n assume n: "N \<le> n"
-    from N n have 3: "X n < X N + r/2" by simp
-    from N n have 4: "X N - r/2 < X n" by simp
-    show "norm (X n - x) < r"
-      using order_less_le_trans [OF 3 1]
-            order_le_less_trans [OF 2 4]
+    from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+
+    thus "norm (X n - x) < r" using 1 2
       by (simp add: real_abs_diff_less_iff)
   qed
 qed
diff -r 93dca7620d0d -r 2f4be6844f7c src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Sun Jun 24 20:47:05 2007 +0200
+++ b/src/HOL/Real/RealDef.thy	Sun Jun 24 20:55:41 2007 +0200
@@ -526,10 +526,6 @@
 lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
 by(simp add:mult_commute)
 
-(* FIXME: redundant, but used by Integration/Integral.thy in AFP *)
-lemma real_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::real) \<le> x + y"
-by (rule add_nonneg_nonneg)
-
 lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x"
 by (simp add: one_less_inverse_iff) (* TODO: generalize/move *)
 
diff -r 93dca7620d0d -r 2f4be6844f7c src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Sun Jun 24 20:47:05 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Sun Jun 24 20:55:41 2007 +0200
@@ -773,12 +773,13 @@
 lemma add_divide_distrib: "(a+b)/(c::'a::field) = a/c + b/c"
 by (simp add: divide_inverse ring_distribs) 
 
-
+(* what ordering?? this is a straight instance of mult_eq_0_iff
 text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
       of an ordering.*}
 lemma field_mult_eq_0_iff [simp]:
   "(a*b = (0::'a::division_ring)) = (a = 0 | b = 0)"
 by simp
+*)
 
 text{*Cancellation of equalities with a common factor*}
 lemma field_mult_cancel_right_lemma:
@@ -915,7 +916,7 @@
       shows "inverse(a*b) = inverse(b) * inverse(a::'a::division_ring)"
   proof -
   have "inverse(a*b) * (a * b) * inverse(b) = inverse(b)" 
-    by (simp add: field_mult_eq_0_iff anz bnz)
+    by (simp add: anz bnz)
   hence "inverse(a*b) * a = inverse(b)" 
     by (simp add: mult_assoc bnz)
   hence "inverse(a*b) * a * inverse(a) = inverse(b) * inverse(a)" 
@@ -969,8 +970,7 @@
 assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/(b::'a::field)"
 proof -
   have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
-    by (simp add: field_mult_eq_0_iff divide_inverse 
-                  nonzero_inverse_mult_distrib)
+    by (simp add: divide_inverse nonzero_inverse_mult_distrib)
   also have "... =  a * inverse b * (inverse c * c)"
     by (simp only: mult_ac)
   also have "... =  a * inverse b"
@@ -1004,6 +1004,8 @@
 lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
 by (simp add: divide_inverse mult_ac)
 
+lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
+
 lemma divide_divide_eq_right [simp]:
   "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
 by (simp add: divide_inverse mult_ac)
@@ -1098,53 +1100,120 @@
 lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c"
 by (simp add: diff_minus add_divide_distrib) 
 
+lemma add_divide_eq_iff:
+  "(z::'a::field) \<noteq> 0 \<Longrightarrow> x + y/z = (z*x + y)/z"
+by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)
+
+lemma divide_add_eq_iff:
+  "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z + y = (x + z*y)/z"
+by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)
+
+lemma diff_divide_eq_iff:
+  "(z::'a::field) \<noteq> 0 \<Longrightarrow> x - y/z = (z*x - y)/z"
+by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)
+
+lemma divide_diff_eq_iff:
+  "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z - y = (x - z*y)/z"
+by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)
+
+lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"
+proof -
+  assume [simp]: "c\<noteq>0"
+  have "(a = b/c) = (a*c = (b/c)*c)"
+    by (simp add: field_mult_cancel_right)
+  also have "... = (a*c = b)"
+    by (simp add: divide_inverse mult_assoc)
+  finally show ?thesis .
+qed
+
+lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"
+proof -
+  assume [simp]: "c\<noteq>0"
+  have "(b/c = a) = ((b/c)*c = a*c)"
+    by (simp add: field_mult_cancel_right)
+  also have "... = (b = a*c)"
+    by (simp add: divide_inverse mult_assoc) 
+  finally show ?thesis .
+qed
+
+lemma eq_divide_eq:
+  "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
+by (simp add: nonzero_eq_divide_eq) 
+
+lemma divide_eq_eq:
+  "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
+by (force simp add: nonzero_divide_eq_eq) 
+
+lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
+    b = a * c ==> b / c = a"
+  by (subst divide_eq_eq, simp)
+
+lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
+    a * c = b ==> a = b / c"
+  by (subst eq_divide_eq, simp)
+
+
+lemmas field_eq_simps = ring_simps
+  (* pull / out*)
+  add_divide_eq_iff divide_add_eq_iff
+  diff_divide_eq_iff divide_diff_eq_iff
+  (* multiply eqn *)
+  nonzero_eq_divide_eq nonzero_divide_eq_eq
+(* is added later:
+  times_divide_eq_left times_divide_eq_right
+*)
+
+text{*An example:*}
+lemma fixes a b c d e f :: "'a::field"
+shows "\<lbrakk>a\<noteq>b; c\<noteq>d; e\<noteq>f \<rbrakk> \<Longrightarrow> ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1"
+apply(subgoal_tac "(c-d)*(e-f)*(a-b) \<noteq> 0")
+ apply(simp add:field_eq_simps)
+apply(simp)
+done
+
+
 lemma diff_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
     x / y - w / z = (x * z - w * y) / (y * z)"
-apply (subst diff_def)+
-apply (subst minus_divide_left)
-apply (subst add_frac_eq)
-apply simp_all
-done
+by (simp add:field_eq_simps times_divide_eq)
+
+lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
+    (x / y = w / z) = (x * z = w * y)"
+by (simp add:field_eq_simps times_divide_eq)
 
 
 subsection {* Ordered Fields *}
 
 lemma positive_imp_inverse_positive: 
-      assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::ordered_field)"
-  proof -
+assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::ordered_field)"
+proof -
   have "0 < a * inverse a" 
     by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
   thus "0 < inverse a" 
     by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
-  qed
+qed
 
 lemma negative_imp_inverse_negative:
-     "a < 0 ==> inverse a < (0::'a::ordered_field)"
-  by (insert positive_imp_inverse_positive [of "-a"], 
-      simp add: nonzero_inverse_minus_eq order_less_imp_not_eq) 
+  "a < 0 ==> inverse a < (0::'a::ordered_field)"
+by (insert positive_imp_inverse_positive [of "-a"], 
+    simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)
 
 lemma inverse_le_imp_le:
-      assumes invle: "inverse a \<le> inverse b"
-	  and apos:  "0 < a"
-	 shows "b \<le> (a::'a::ordered_field)"
-  proof (rule classical)
+assumes invle: "inverse a \<le> inverse b" and apos:  "0 < a"
+shows "b \<le> (a::'a::ordered_field)"
+proof (rule classical)
   assume "~ b \<le> a"
-  hence "a < b"
-    by (simp add: linorder_not_le)
-  hence bpos: "0 < b"
-    by (blast intro: apos order_less_trans)
+  hence "a < b"  by (simp add: linorder_not_le)
+  hence bpos: "0 < b"  by (blast intro: apos order_less_trans)
   hence "a * inverse a \<le> a * inverse b"
     by (simp add: apos invle order_less_imp_le mult_left_mono)
   hence "(a * inverse a) * b \<le> (a * inverse b) * b"
     by (simp add: bpos order_less_imp_le mult_right_mono)
-  thus "b \<le> a"
-    by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
-  qed
+  thus "b \<le> a"  by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
+qed
 
 lemma inverse_positive_imp_positive:
-  assumes inv_gt_0: "0 < inverse a"
-    and nz: "a \<noteq> 0"
-  shows "0 < (a::'a::ordered_field)"
+assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
+shows "0 < (a::'a::ordered_field)"
 proof -
   have "0 < inverse (inverse a)"
     using inv_gt_0 by (rule positive_imp_inverse_positive)
@@ -1153,34 +1222,32 @@
 qed
 
 lemma inverse_positive_iff_positive [simp]:
-      "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
+  "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
 apply (cases "a = 0", simp)
 apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
 done
 
 lemma inverse_negative_imp_negative:
-  assumes inv_less_0: "inverse a < 0"
-    and nz:  "a \<noteq> 0"
-  shows "a < (0::'a::ordered_field)"
+assumes inv_less_0: "inverse a < 0" and nz:  "a \<noteq> 0"
+shows "a < (0::'a::ordered_field)"
 proof -
   have "inverse (inverse a) < 0"
     using inv_less_0 by (rule negative_imp_inverse_negative)
-  thus "a < 0"
-    using nz by (simp add: nonzero_inverse_inverse_eq)
+  thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
 qed
 
 lemma inverse_negative_iff_negative [simp]:
-      "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
+  "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
 apply (cases "a = 0", simp)
 apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
 done
 
 lemma inverse_nonnegative_iff_nonnegative [simp]:
-      "(0 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"
+  "(0 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"
 by (simp add: linorder_not_less [symmetric])
 
 lemma inverse_nonpositive_iff_nonpositive [simp]:
-      "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"
+  "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"
 by (simp add: linorder_not_less [symmetric])
 
 lemma ordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::ordered_field)"
@@ -1204,10 +1271,9 @@
 subsection{*Anti-Monotonicity of @{term inverse}*}
 
 lemma less_imp_inverse_less:
-      assumes less: "a < b"
-	  and apos:  "0 < a"
-	shows "inverse b < inverse (a::'a::ordered_field)"
-  proof (rule ccontr)
+assumes less: "a < b" and apos:  "0 < a"
+shows "inverse b < inverse (a::'a::ordered_field)"
+proof (rule ccontr)
   assume "~ inverse b < inverse a"
   hence "inverse a \<le> inverse b"
     by (simp add: linorder_not_less)
@@ -1215,81 +1281,78 @@
     by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])
   thus False
     by (rule notE [OF _ less])
-  qed
+qed
 
 lemma inverse_less_imp_less:
-   "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"
+  "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"
 apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])
 apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) 
 done
 
 text{*Both premises are essential. Consider -1 and 1.*}
 lemma inverse_less_iff_less [simp]:
-     "[|0 < a; 0 < b|] 
-      ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
+  "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
 
 lemma le_imp_inverse_le:
-   "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
-  by (force simp add: order_le_less less_imp_inverse_less)
+  "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
+by (force simp add: order_le_less less_imp_inverse_less)
 
 lemma inverse_le_iff_le [simp]:
-     "[|0 < a; 0 < b|] 
-      ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
+ "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
 
 
 text{*These results refer to both operands being negative.  The opposite-sign
 case is trivial, since inverse preserves signs.*}
 lemma inverse_le_imp_le_neg:
-   "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"
-  apply (rule classical) 
-  apply (subgoal_tac "a < 0") 
-   prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans) 
-  apply (insert inverse_le_imp_le [of "-b" "-a"])
-  apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
-  done
+  "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"
+apply (rule classical) 
+apply (subgoal_tac "a < 0") 
+ prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans) 
+apply (insert inverse_le_imp_le [of "-b" "-a"])
+apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
+done
 
 lemma less_imp_inverse_less_neg:
    "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::ordered_field)"
-  apply (subgoal_tac "a < 0") 
-   prefer 2 apply (blast intro: order_less_trans) 
-  apply (insert less_imp_inverse_less [of "-b" "-a"])
-  apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
-  done
+apply (subgoal_tac "a < 0") 
+ prefer 2 apply (blast intro: order_less_trans) 
+apply (insert less_imp_inverse_less [of "-b" "-a"])
+apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
+done
 
 lemma inverse_less_imp_less_neg:
    "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::ordered_field)"
-  apply (rule classical) 
-  apply (subgoal_tac "a < 0") 
-   prefer 2
-   apply (force simp add: linorder_not_less intro: order_le_less_trans) 
-  apply (insert inverse_less_imp_less [of "-b" "-a"])
-  apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
-  done
+apply (rule classical) 
+apply (subgoal_tac "a < 0") 
+ prefer 2
+ apply (force simp add: linorder_not_less intro: order_le_less_trans) 
+apply (insert inverse_less_imp_less [of "-b" "-a"])
+apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
+done
 
 lemma inverse_less_iff_less_neg [simp]:
-     "[|a < 0; b < 0|] 
-      ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
-  apply (insert inverse_less_iff_less [of "-b" "-a"])
-  apply (simp del: inverse_less_iff_less 
-	      add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
-  done
+  "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
+apply (insert inverse_less_iff_less [of "-b" "-a"])
+apply (simp del: inverse_less_iff_less 
+            add: order_less_imp_not_eq nonzero_inverse_minus_eq)
+done
 
 lemma le_imp_inverse_le_neg:
-   "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
-  by (force simp add: order_le_less less_imp_inverse_less_neg)
+  "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
+by (force simp add: order_le_less less_imp_inverse_less_neg)
 
 lemma inverse_le_iff_le_neg [simp]:
-     "[|a < 0; b < 0|] 
-      ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
+ "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
 
 
 subsection{*Inverses and the Number One*}
 
 lemma one_less_inverse_iff:
-    "(1 < inverse x) = (0 < x & x < (1::'a::{ordered_field,division_by_zero}))"proof cases
+  "(1 < inverse x) = (0 < x & x < (1::'a::{ordered_field,division_by_zero}))"
+proof cases
   assume "0 < x"
     with inverse_less_iff_less [OF zero_less_one, of x]
     show ?thesis by simp
@@ -1306,20 +1369,20 @@
 qed
 
 lemma inverse_eq_1_iff [simp]:
-    "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
+  "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
 by (insert inverse_eq_iff_eq [of x 1], simp) 
 
 lemma one_le_inverse_iff:
-   "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{ordered_field,division_by_zero}))"
+  "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{ordered_field,division_by_zero}))"
 by (force simp add: order_le_less one_less_inverse_iff zero_less_one 
                     eq_commute [of 1]) 
 
 lemma inverse_less_1_iff:
-   "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{ordered_field,division_by_zero}))"
+  "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{ordered_field,division_by_zero}))"
 by (simp add: linorder_not_le [symmetric] one_le_inverse_iff) 
 
 lemma inverse_le_1_iff:
-   "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
+  "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
 by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) 
 
 
@@ -1445,49 +1508,41 @@
 apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff) 
 done
 
-lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"
-proof -
-  assume [simp]: "c\<noteq>0"
-  have "(a = b/c) = (a*c = (b/c)*c)"
-    by (simp add: field_mult_cancel_right)
-  also have "... = (a*c = b)"
-    by (simp add: divide_inverse mult_assoc) 
-  finally show ?thesis .
-qed
+
+subsection{*Field simplification*}
+
+text{* Lemmas @{text field_simps} multiply with denominators in
+in(equations) if they can be proved to be non-zero (for equations) or
+positive/negative (for inequations). *}
 
-lemma eq_divide_eq:
-  "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
-by (simp add: nonzero_eq_divide_eq) 
+lemmas field_simps = field_eq_simps
+  (* multiply ineqn *)
+  pos_divide_less_eq neg_divide_less_eq
+  pos_less_divide_eq neg_less_divide_eq
+  pos_divide_le_eq neg_divide_le_eq
+  pos_le_divide_eq neg_le_divide_eq
 
-lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"
-proof -
-  assume [simp]: "c\<noteq>0"
-  have "(b/c = a) = ((b/c)*c = a*c)"
-    by (simp add: field_mult_cancel_right)
-  also have "... = (b = a*c)"
-    by (simp add: divide_inverse mult_assoc) 
-  finally show ?thesis .
-qed
+text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
+of positivity/negativity needed for field_simps. Have not added @{text
+sign_simps} to @{text field_simps} because the former can lead to case
+explosions. *}
 
-lemma divide_eq_eq:
-  "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
-by (force simp add: nonzero_divide_eq_eq) 
+lemmas sign_simps = group_simps
+  zero_less_mult_iff  mult_less_0_iff
 
-lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
-    b = a * c ==> b / c = a"
-  by (subst divide_eq_eq, simp)
-
-lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
-    a * c = b ==> a = b / c"
-  by (subst eq_divide_eq, simp)
-
-lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
-    (x / y = w / z) = (x * z = w * y)"
-  apply (subst nonzero_eq_divide_eq)
-  apply assumption
-  apply (subst times_divide_eq_left)
-  apply (erule nonzero_divide_eq_eq) 
+(* Only works once linear arithmetic is installed:
+text{*An example:*}
+lemma fixes a b c d e f :: "'a::ordered_field"
+shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
+ ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
+ ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
+apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
+ prefer 2 apply(simp add:sign_simps)
+apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
+ prefer 2 apply(simp add:sign_simps)
+apply(simp add:field_simps)
 done
+*)
 
 
 subsection{*Division and Signs*}
@@ -1513,74 +1568,54 @@
 
 lemma divide_eq_0_iff [simp]:
      "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
-by (simp add: divide_inverse field_mult_eq_0_iff)
+by (simp add: divide_inverse)
 
-lemma divide_pos_pos: "0 < (x::'a::ordered_field) ==> 
-    0 < y ==> 0 < x / y"
-  apply (subst pos_less_divide_eq)
-  apply assumption
-  apply simp
-done
+lemma divide_pos_pos:
+  "0 < (x::'a::ordered_field) ==> 0 < y ==> 0 < x / y"
+by(simp add:field_simps)
+
 
-lemma divide_nonneg_pos: "0 <= (x::'a::ordered_field) ==> 0 < y ==> 
-    0 <= x / y"
-  apply (subst pos_le_divide_eq)
-  apply assumption
-  apply simp
-done
+lemma divide_nonneg_pos:
+  "0 <= (x::'a::ordered_field) ==> 0 < y ==> 0 <= x / y"
+by(simp add:field_simps)
 
-lemma divide_neg_pos: "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0"
-  apply (subst pos_divide_less_eq)
-  apply assumption
-  apply simp
-done
+lemma divide_neg_pos:
+  "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0"
+by(simp add:field_simps)
 
-lemma divide_nonpos_pos: "(x::'a::ordered_field) <= 0 ==> 
-    0 < y ==> x / y <= 0"
-  apply (subst pos_divide_le_eq)
-  apply assumption
-  apply simp
-done
+lemma divide_nonpos_pos:
+  "(x::'a::ordered_field) <= 0 ==> 0 < y ==> x / y <= 0"
+by(simp add:field_simps)
 
-lemma divide_pos_neg: "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0"
-  apply (subst neg_divide_less_eq)
-  apply assumption
-  apply simp
-done
+lemma divide_pos_neg:
+  "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0"
+by(simp add:field_simps)
 
-lemma divide_nonneg_neg: "0 <= (x::'a::ordered_field) ==> 
-    y < 0 ==> x / y <= 0"
-  apply (subst neg_divide_le_eq)
-  apply assumption
-  apply simp
-done
+lemma divide_nonneg_neg:
+  "0 <= (x::'a::ordered_field) ==> y < 0 ==> x / y <= 0" 
+by(simp add:field_simps)
 
-lemma divide_neg_neg: "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y"
-  apply (subst neg_less_divide_eq)
-  apply assumption
-  apply simp
-done
+lemma divide_neg_neg:
+  "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y"
+by(simp add:field_simps)
 
-lemma divide_nonpos_neg: "(x::'a::ordered_field) <= 0 ==> y < 0 ==> 
-    0 <= x / y"
-  apply (subst neg_le_divide_eq)
-  apply assumption
-  apply simp
-done
+lemma divide_nonpos_neg:
+  "(x::'a::ordered_field) <= 0 ==> y < 0 ==> 0 <= x / y"
+by(simp add:field_simps)
 
 
 subsection{*Cancellation Laws for Division*}
 
 lemma divide_cancel_right [simp]:
      "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
-apply (cases "c=0", simp) 
-apply (simp add: divide_inverse field_mult_cancel_right) 
+apply (cases "c=0", simp)
+apply (simp add: divide_inverse field_mult_cancel_right)
 done
 
 lemma divide_cancel_left [simp]:
      "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
-apply (cases "c=0", simp) 
-apply (simp add: divide_inverse field_mult_cancel_left) 
+apply (cases "c=0", simp)
+apply (simp add: divide_inverse field_mult_cancel_left)
 done
 
 
@@ -1589,25 +1624,25 @@
 text{*Simplify expressions equated with 1*}
 lemma divide_eq_1_iff [simp]:
      "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
-apply (cases "b=0", simp) 
-apply (simp add: right_inverse_eq) 
+apply (cases "b=0", simp)
+apply (simp add: right_inverse_eq)
 done
 
 lemma one_eq_divide_iff [simp]:
      "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
-by (simp add: eq_commute [of 1])  
+by (simp add: eq_commute [of 1])
 
 lemma zero_eq_1_divide_iff [simp]:
      "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)"
-apply (cases "a=0", simp) 
-apply (auto simp add: nonzero_eq_divide_eq) 
+apply (cases "a=0", simp)
+apply (auto simp add: nonzero_eq_divide_eq)
 done
 
 lemma one_divide_eq_0_iff [simp]:
      "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"
-apply (cases "a=0", simp) 
-apply (insert zero_neq_one [THEN not_sym]) 
-apply (auto simp add: nonzero_divide_eq_eq) 
+apply (cases "a=0", simp)
+apply (insert zero_neq_one [THEN not_sym])
+apply (auto simp add: nonzero_divide_eq_eq)
 done
 
 text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
@@ -1627,40 +1662,33 @@
 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) 
+              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) 
+by (force simp add: divide_strict_right_mono order_le_less)
 
 lemma divide_right_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b 
     ==> c <= 0 ==> b / c <= a / c"
-  apply (drule divide_right_mono [of _ _ "- c"])
-  apply auto
+apply (drule divide_right_mono [of _ _ "- c"])
+apply auto
 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]) 
+apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
+apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric])
 done
 
 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) 
+  "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
+by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
 
 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 (cases "c=0", simp add: divide_inverse)
-  apply (force simp add: divide_strict_left_mono order_le_less) 
-  done
+  "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::ordered_field)"
+by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
 
 lemma divide_left_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b 
     ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
@@ -1669,13 +1697,9 @@
 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
+  "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
+by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
+
 
 text{*Simplify quotients that are compared with the value 1.*}
 
@@ -1768,16 +1792,16 @@
   by (subst pos_divide_le_eq, assumption+);
 
 lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>
-    z <= x / y";
-  by (subst pos_le_divide_eq, assumption+)
+    z <= x / y"
+by(simp add:field_simps)
 
 lemma mult_imp_div_pos_less: "0 < (y::'a::ordered_field) ==> x < z * y ==>
     x / y < z"
-  by (subst pos_divide_less_eq, assumption+)
+by(simp add:field_simps)
 
 lemma mult_imp_less_div_pos: "0 < (y::'a::ordered_field) ==> z * y < x ==>
     z < x / y"
-  by (subst pos_less_divide_eq, assumption+)
+by(simp add:field_simps)
 
 lemma frac_le: "(0::'a::ordered_field) <= x ==> 
     x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
@@ -1809,8 +1833,6 @@
   apply simp_all
 done
 
-lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
-
 text{*It's not obvious whether these should be simprules or not. 
   Their effect is to gather terms into one big fraction, like
   a*b*c / x*y*z. The rationale for that is unclear, but many proofs 
@@ -1824,18 +1846,18 @@
 lemma less_add_one: "a < (a+1::'a::ordered_semidom)"
 proof -
   have "a+0 < (a+1::'a::ordered_semidom)"
-    by (blast intro: zero_less_one add_strict_left_mono) 
+    by (blast intro: zero_less_one add_strict_left_mono)
   thus ?thesis by simp
 qed
 
 lemma zero_less_two: "0 < (1+1::'a::ordered_semidom)"
-  by (blast intro: order_less_trans zero_less_one less_add_one) 
+by (blast intro: order_less_trans zero_less_one less_add_one)
 
 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"
-by (simp add: zero_less_two pos_less_divide_eq ring_distribs) 
+by (simp add: field_simps zero_less_two)
 
 lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"
-by (simp add: zero_less_two pos_divide_less_eq ring_distribs) 
+by (simp add: field_simps zero_less_two)
 
 lemma dense: "a < b ==> \<exists>r::'a::ordered_field. a < r & r < b"
 by (blast intro!: less_half_sum gt_half_sum)