# HG changeset patch
# User paulson
# Date 1097156550 -7200
# Node ID ec91a90c604ed6f197adca3cf4694e633d470641
# Parent  c55a121629441adb758ffeba0138d5e5756e3a7b
simplification tweaks for better arithmetic reasoning

diff -r c55a12162944 -r ec91a90c604e src/HOL/Complex/CLim.thy
--- a/src/HOL/Complex/CLim.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Complex/CLim.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -1014,16 +1014,11 @@
       \<exists>g. (\<forall>z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l"
 by (simp add: NSCDERIV_CDERIV_iff isNSContc_isContc_iff CARAT_CDERIV)
 
-(* FIXME tidy! How about a NS proof? *)
 lemma CARAT_CDERIVD:
      "(\<forall>z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l
       ==> NSCDERIV f x :> l"
-apply (simp only: NSCDERIV_iff2) 
-apply (tactic {*(auto_tac (claset(), 
-              simpset() delsimprocs field_cancel_factor
-                        addsimps [thm"NSCDERIV_iff2"])) *})
-apply (simp add: isNSContc_def)
-done
+by (auto simp add: NSCDERIV_iff2 isNSContc_def cstarfun_if_eq); 
+
 
 ML
 {*
diff -r c55a12162944 -r ec91a90c604e src/HOL/Complex/CStar.thy
--- a/src/HOL/Complex/CStar.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Complex/CStar.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -218,6 +218,13 @@
 apply (auto iff add: hcomplexrel_iff, ultra)
 done
 
+lemma cstarfun_if_eq:
+     "w \<noteq> hcomplex_of_complex x
+       ==> ( *fc* (\<lambda>z. if z = x then a else g z)) w = ( *fc* g) w" 
+apply (cases w) 
+apply (simp add: hcomplex_of_complex_def starfunC, ultra)
+done
+
 lemma starfunRC:
       "( *fRc* f) (Abs_hypreal(hyprel``{%n. X n})) =
        Abs_hcomplex(hcomplexrel `` {%n. f (X n)})"
diff -r c55a12162944 -r ec91a90c604e src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Complex/Complex.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -212,10 +212,10 @@
 lemma complex_mult_inv_left: "z \<noteq> (0::complex) ==> inverse(z) * z = 1"
 apply (induct z)
 apply (rename_tac x y)
-apply (auto simp add: complex_mult complex_inverse complex_one_def
-      complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac)
-apply (drule_tac y = y in real_sum_squares_not_zero)
-apply (drule_tac [2] x = x in real_sum_squares_not_zero2, auto)
+apply (auto simp add: times_divide_eq complex_mult complex_inverse 
+             complex_one_def complex_zero_def add_divide_distrib [symmetric] 
+             power2_eq_square mult_ac)
+apply (simp_all add: real_sum_squares_not_zero real_sum_squares_not_zero2) 
 done
 
 
diff -r c55a12162944 -r ec91a90c604e src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -1297,7 +1297,7 @@
   apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
   apply (erule ssubst)
   apply (subst times_divide_eq_right [THEN sym])
-  apply (auto simp add: mult_ac divide_self)
+  apply (auto simp add: mult_ac times_divide_eq_right divide_self)
   done
 
 lemma setprod_inversef: "finite A ==>
diff -r c55a12162944 -r ec91a90c604e src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -386,14 +386,12 @@
 lemma starfun_ln_not_eq_zero [simp]: "[| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
 apply (cases x)
 apply (auto simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
-apply (auto dest: ln_not_eq_zero) 
 done
 
 lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* ln) x \<in> HFinite"
 apply (rule HFinite_bounded)
-apply (rule_tac [2] order_less_imp_le)
-apply (rule_tac [2] starfun_ln_less_self)
-apply (rule_tac [2] order_less_le_trans, auto)
+apply assumption 
+apply (simp_all add: starfun_ln_less_self order_less_imp_le)
 done
 
 lemma starfun_ln_inverse: "0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
@@ -453,7 +451,6 @@
 lemma starfun_ln_less_zero: "[| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
 apply (cases x)
 apply (simp add: hypreal_zero_num hypreal_one_num hypreal_less starfun, ultra)
-apply (auto intro: ln_less_zero) 
 done
 
 lemma starfun_ln_Infinitesimal_less_zero:
diff -r c55a12162944 -r ec91a90c604e src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -506,9 +506,7 @@
 qed
 
 lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)"
-apply auto
-apply (rule OrderedGroup.add_right_cancel [of _ "-y", THEN iffD1], auto)
-done
+by auto
 
 lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
 by auto
diff -r c55a12162944 -r ec91a90c604e src/HOL/Hyperreal/Integration.thy
--- a/src/HOL/Hyperreal/Integration.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/Integration.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -432,7 +432,7 @@
 apply (rule_tac y = "(e/2) * \<bar>v - x\<bar>" in order_trans)
  prefer 2 apply simp
 apply (erule_tac [!] V= "\<forall>x'. x' ~= x & \<bar>x' + - x\<bar> < s --> ?P x'" in thin_rl)
-apply (drule_tac x = v in spec, simp)
+apply (drule_tac x = v in spec, simp add: times_divide_eq)
 apply (drule_tac x = u in spec, auto, arith)
 apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
 apply (rule order_trans)
diff -r c55a12162944 -r ec91a90c604e src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -277,7 +277,7 @@
 apply (rule ccontr, simp)
 apply (simp add: linorder_not_less)
 apply (drule lemma_skolemize_LIM2, safe)
-apply (drule_tac x = "Abs_hypreal (hyprel``{X}) " in spec)
+apply (drule_tac x = "Abs_hypreal (hyprel``{X})" in spec)
 apply (auto simp add: starfun hypreal_minus hypreal_of_real_def hypreal_add)
 apply (drule lemma_simp [THEN real_seq_to_hypreal_Infinitesimal])
 apply (simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_of_real_def hypreal_minus hypreal_add, blast)
@@ -603,10 +603,12 @@
                \<bar>z + -y\<bar> < inverse(real(Suc n)) &
                r \<le> \<bar>f z + -f y\<bar>"
 apply clarify
-apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
+apply (cut_tac n1 = n 
+       in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
 done
 
-lemma lemma_skolemize_LIM2u: "\<forall>s. 0 < s --> (\<exists>z y. \<bar>z + - y\<bar> < s  & r \<le> \<bar>f z + -f y\<bar>)
+lemma lemma_skolemize_LIM2u:
+     "\<forall>s. 0 < s --> (\<exists>z y. \<bar>z + - y\<bar> < s  & r \<le> \<bar>f z + -f y\<bar>)
       ==> \<exists>X Y. \<forall>n::nat.
                abs(X n + -(Y n)) < inverse(real(Suc n)) &
                r \<le> abs(f (X n) + -f (Y n))"
@@ -627,8 +629,8 @@
 apply (rule ccontr, simp)
 apply (simp add: linorder_not_less)
 apply (drule lemma_skolemize_LIM2u, safe)
-apply (drule_tac x = "Abs_hypreal (hyprel``{X}) " in spec)
-apply (drule_tac x = "Abs_hypreal (hyprel``{Y}) " in spec)
+apply (drule_tac x = "Abs_hypreal (hyprel``{X})" in spec)
+apply (drule_tac x = "Abs_hypreal (hyprel``{Y})" in spec)
 apply (simp add: starfun hypreal_minus hypreal_add, auto)
 apply (drule lemma_simpu [THEN real_seq_to_hypreal_Infinitesimal2])
 apply (simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_minus hypreal_add, blast)
@@ -778,7 +780,7 @@
 apply (drule_tac c = "u - hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1)
 apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1])
 apply (subgoal_tac [2] "( *f* (%z. z-x)) u \<noteq> (0::hypreal) ")
-apply (auto simp add: diff_minus
+apply (auto simp add: times_divide_eq_left diff_minus
 	       approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
 		     Infinitesimal_subset_HFinite [THEN subsetD])
 done
@@ -794,7 +796,7 @@
 apply (drule_tac x = h in bspec)
 apply (drule_tac [2] c = h in approx_mult1)
 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
-            simp add: diff_minus)
+            simp add: times_divide_eq_left diff_minus)
 done
 
 lemma NSDERIVD3:
@@ -806,7 +808,7 @@
 apply (rule ccontr, drule_tac x = h in bspec)
 apply (drule_tac [2] c = h in approx_mult1)
 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
-            simp add: mult_assoc diff_minus)
+            simp add: mult_assoc times_divide_eq_left diff_minus)
 done
 
 text{*Now equivalence between NSDERIV and DERIV*}
@@ -821,14 +823,14 @@
 apply (drule hypreal_not_eq_minus_iff [THEN iffD1])
 apply (drule_tac x = "-hypreal_of_real x + xa" in bspec)
  prefer 2 apply (simp add: add_assoc [symmetric])
-apply (auto simp add: mem_infmal_iff [symmetric] hypreal_add_commute)
+apply (auto simp add: mem_infmal_iff [symmetric] add_commute)
 apply (drule_tac c = "xa + -hypreal_of_real x" in approx_mult1)
 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
             simp add: mult_assoc)
 apply (drule_tac x3=D in
            HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult,
              THEN mem_infmal_iff [THEN iffD1]])
-apply (auto simp add: mult_commute
+apply (auto simp add: times_divide_eq_right mult_commute
             intro: approx_trans approx_minus_iff [THEN iffD2])
 done
 
@@ -877,9 +879,9 @@
          z \<in> Infinitesimal; yb \<in> Infinitesimal |]
       ==> x + y \<approx> 0"
 apply (frule_tac c1 = z in hypreal_mult_right_cancel [THEN iffD2], assumption)
-apply (erule_tac V = " (x + y) / z = hypreal_of_real D + yb" in thin_rl)
+apply (erule_tac V = "(x + y) / z = hypreal_of_real D + yb" in thin_rl)
 apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add
-            simp add: hypreal_mult_assoc mem_infmal_iff [symmetric])
+            simp add: times_divide_eq_left mult_assoc mem_infmal_iff [symmetric])
 apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
 done
 
@@ -891,7 +893,8 @@
 	    simp add: starfun_lambda_cancel lemma_nsderiv1)
 apply (simp (no_asm) add: add_divide_distrib)
 apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
-apply (auto simp del: times_divide_eq_right simp add: times_divide_eq_right [symmetric])
+apply (auto simp add: times_divide_eq_right [symmetric]
+            simp del: times_divide_eq)
 apply (drule_tac D = Db in lemma_nsderiv2)
 apply (drule_tac [4]
      approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]])
@@ -989,7 +992,7 @@
         in hypreal_mult_right_cancel [THEN iffD2])
 apply (erule_tac [2] V = "(( *f* f) (hypreal_of_real (x) + h) + - hypreal_of_real (f x)) / h = hypreal_of_real (D) + y" in thin_rl)
 apply assumption
-apply (simp add: times_divide_eq_right [symmetric] del: times_divide_eq_right)
+apply (simp add: times_divide_eq_left times_divide_eq_right [symmetric])
 apply (auto simp add: left_distrib)
 done
 
@@ -1116,7 +1119,7 @@
 apply (auto simp add: real_of_nat_Suc left_distrib)
 apply (case_tac "0 < n")
 apply (drule_tac x = x in realpow_minus_mult)
-apply (auto simp add: real_mult_assoc real_add_commute)
+apply (auto simp add: mult_assoc add_commute)
 done
 
 (* NS version *)
@@ -1140,7 +1143,7 @@
                  minus_mult_left [symmetric] minus_mult_right [symmetric])
 apply (simp (no_asm_simp) add: mult_assoc [symmetric] right_distrib
             del: minus_mult_left [symmetric] minus_mult_right [symmetric])
-apply (rule_tac y = " inverse (- hypreal_of_real x * hypreal_of_real x) " in approx_trans)
+apply (rule_tac y = "inverse (- hypreal_of_real x * hypreal_of_real x)" in approx_trans)
 apply (rule inverse_add_Infinitesimal_approx2)
 apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal
             simp add: inverse_minus_eq [symmetric] HFinite_minus_iff)
@@ -1194,7 +1197,7 @@
   show "\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) \<and> isCont g x \<and> g x = l"
   proof (intro exI conjI)
     let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
-    show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
+    show "\<forall>z. f z - f x = ?g z * (z-x)" by (simp add: times_divide_eq)
     show "isCont ?g x" using der
       by (simp add: isCont_iff DERIV_iff diff_minus
                cong: LIM_equal [rule_format])
@@ -1231,10 +1234,8 @@
     by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong)
 qed
 
-(*--------------------------------------------------------------------------*)
-(* Lemmas about nested intervals and proof by bisection (cf.Harrison)       *)
-(* All considerably tidied by lcp                                           *)
-(*--------------------------------------------------------------------------*)
+text{*Lemmas about nested intervals and proof by bisection (cf.Harrison).
+     All considerably tidied by lcp.*}
 
 lemma lemma_f_mono_add [rule_format (no_asm)]: "(\<forall>n. (f::nat=>real) n \<le> f (Suc n)) --> f m \<le> f(m + no)"
 apply (induct_tac "no")
@@ -1248,7 +1249,7 @@
 apply (rule_tac k = "f 0" and K = "g 0" in BseqI2, rule allI)
 apply (induct_tac "n")
 apply (auto intro: order_trans)
-apply (rule_tac y = "g (Suc na) " in order_trans)
+apply (rule_tac y = "g (Suc na)" in order_trans)
 apply (induct_tac [2] "na")
 apply (auto intro: order_trans)
 done
@@ -1258,7 +1259,7 @@
          \<forall>n. f(n) \<le> g(n) |]
       ==> Bseq g"
 apply (subst Bseq_minus_iff [symmetric])
-apply (rule_tac g = "%x. - (f x) " in f_inc_g_dec_Beq_f)
+apply (rule_tac g = "%x. - (f x)" in f_inc_g_dec_Beq_f)
 apply auto
 done
 
@@ -1282,7 +1283,7 @@
 
 lemma g_dec_imp_lim_le: "[| \<forall>n. g(Suc n) \<le> g(n);  convergent g |] ==> lim g \<le> g n"
 apply (subgoal_tac "- (g n) \<le> - (lim g) ")
-apply (cut_tac [2] f = "%x. - (g x) " in f_inc_imp_le_lim)
+apply (cut_tac [2] f = "%x. - (g x)" in f_inc_imp_le_lim)
 apply (auto simp add: lim_uminus convergent_minus_iff [symmetric])
 done
 
@@ -1335,13 +1336,13 @@
    \<forall>n. snd(Bolzano_bisect P a b (Suc n)) \<le> snd (Bolzano_bisect P a b n)"
 apply (rule allI)
 apply (induct_tac "n")
-apply (auto simp add: Bolzano_bisect_le Let_def split_def)
+apply (auto simp add: Bolzano_bisect_le Let_def split_def times_divide_eq)
 done
 
-lemma eq_divide_2_times_iff: "((x::real) = y / (2 * z)) = (2 * x = y/z)"
-apply auto
+lemma eq_divide_2_times_iff: "((x::real) = y / (2 * z)) = (2 * x = y/z)" 
+apply (auto simp add: times_divide_eq) 
 apply (drule_tac f = "%u. (1/2) *u" in arg_cong)
-apply auto
+apply (simp add: times_divide_eq) 
 done
 
 lemma Bolzano_bisect_diff:
@@ -1403,7 +1404,7 @@
 apply (drule_tac x = "snd (Bolzano_bisect P a b (no + noa))" in spec)
 apply safe
 apply (simp_all (no_asm_simp))
-apply (rule_tac y = "abs (fst (Bolzano_bisect P a b (no + noa)) - l) + abs (snd (Bolzano_bisect P a b (no + noa)) - l) " in order_le_less_trans)
+apply (rule_tac y = "abs (fst (Bolzano_bisect P a b (no + noa)) - l) + abs (snd (Bolzano_bisect P a b (no + noa)) - l)" in order_le_less_trans)
 apply (simp (no_asm_simp) add: abs_if)
 apply (rule real_sum_of_halves [THEN subst])
 apply (rule add_strict_mono)
@@ -1438,7 +1439,7 @@
  apply (drule_tac P = "%d. 0<d --> ?P d" and x = 1 in spec, arith)
 apply (drule_tac x = x in spec)+
 apply simp
-apply (drule_tac P = "%r. ?P r --> (\<exists>s. 0<s & ?Q r s) " and x = "\<bar>y - f x\<bar> " in spec)
+apply (drule_tac P = "%r. ?P r --> (\<exists>s. 0<s & ?Q r s) " and x = "\<bar>y - f x\<bar>" in spec)
 apply safe
 apply simp
 apply (drule_tac x = s in spec, clarify)
@@ -1471,15 +1472,12 @@
 apply (blast intro: IVT2)
 done
 
-(*---------------------------------------------------------------------------*)
-(* By bisection, function continuous on closed interval is bounded above     *)
-(*---------------------------------------------------------------------------*)
-
+subsection{*By bisection, function continuous on closed interval is bounded above*}
 
 lemma isCont_bounded:
      "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
       ==> \<exists>M. \<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M"
-apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> (\<exists>M. \<forall>x. u \<le> x & x \<le> v --> f x \<le> M) " in lemma_BOLZANO2)
+apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> (\<exists>M. \<forall>x. u \<le> x & x \<le> v --> f x \<le> M)" in lemma_BOLZANO2)
 apply safe
 apply simp_all
 apply (rename_tac x xa ya M Ma)
@@ -1501,19 +1499,17 @@
 apply (auto simp add: abs_ge_self, arith+)
 done
 
-(*----------------------------------------------------------------------------*)
-(* Refine the above to existence of least upper bound                         *)
-(*----------------------------------------------------------------------------*)
+text{*Refine the above to existence of least upper bound*}
 
 lemma lemma_reals_complete: "((\<exists>x. x \<in> S) & (\<exists>y. isUb UNIV S (y::real))) -->
       (\<exists>t. isLub UNIV S t)"
-apply (blast intro: reals_complete)
-done
+by (blast intro: reals_complete)
 
 lemma isCont_has_Ub: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
          ==> \<exists>M. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
                    (\<forall>N. N < M --> (\<exists>x. a \<le> x & x \<le> b & N < f(x)))"
-apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x) " in lemma_reals_complete)
+apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x)" 
+        in lemma_reals_complete)
 apply auto
 apply (drule isCont_bounded, assumption)
 apply (auto simp add: isUb_def leastP_def isLub_def setge_def setle_def)
@@ -1521,9 +1517,7 @@
 apply (auto dest!: spec simp add: linorder_not_less)
 done
 
-(*----------------------------------------------------------------------------*)
-(* Now show that it attains its upper bound                                   *)
-(*----------------------------------------------------------------------------*)
+text{*Now show that it attains its upper bound*}
 
 lemma isCont_eq_Ub:
   assumes le: "a \<le> b"
@@ -1565,25 +1559,20 @@
 qed
 
 
-
-(*----------------------------------------------------------------------------*)
-(* Same theorem for lower bound                                               *)
-(*----------------------------------------------------------------------------*)
+text{*Same theorem for lower bound*}
 
 lemma isCont_eq_Lb: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
          ==> \<exists>M. (\<forall>x. a \<le> x & x \<le> b --> M \<le> f(x)) &
                    (\<exists>x. a \<le> x & x \<le> b & f(x) = M)"
 apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. - (f x)) x")
 prefer 2 apply (blast intro: isCont_minus)
-apply (drule_tac f = " (%x. - (f x))" in isCont_eq_Ub)
+apply (drule_tac f = "(%x. - (f x))" in isCont_eq_Ub)
 apply safe
 apply auto
 done
 
 
-(* ------------------------------------------------------------------------- *)
-(* Another version.                                                          *)
-(* ------------------------------------------------------------------------- *)
+text{*Another version.*}
 
 lemma isCont_Lb_Ub: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
       ==> \<exists>L M. (\<forall>x. a \<le> x & x \<le> b --> L \<le> f(x) & f(x) \<le> M) &
@@ -1821,7 +1810,8 @@
   hence ba: "b-a \<noteq> 0" by arith
   show ?thesis
     by (rule real_mult_left_cancel [OF ba, THEN iffD1],
-        simp add: right_diff_distrib, simp add: left_diff_distrib)
+        simp add: times_divide_eq right_diff_distrib, 
+        simp add: left_diff_distrib)
 qed
 
 theorem MVT:
@@ -1856,7 +1846,8 @@
   proof (intro exI conjI)
     show "a < z" .
     show "z < b" .
-    show "f b - f a = (b - a) * ((f b - f a)/(b-a))" by simp
+    show "f b - f a = (b - a) * ((f b - f a)/(b-a))" 
+      by (simp add: times_divide_eq)
     show "DERIV f z :> ((f b - f a)/(b-a))"  using derF by simp
   qed
 qed
@@ -1906,14 +1897,14 @@
 lemma DERIV_const_ratio_const2:
      "[|a \<noteq> b; \<forall>x. DERIV f x :> k |] ==> (f(b) - f(a))/(b-a) = k"
 apply (rule_tac c1 = "b-a" in real_mult_right_cancel [THEN iffD1])
-apply (auto dest!: DERIV_const_ratio_const simp add: real_mult_assoc)
+apply (auto dest!: DERIV_const_ratio_const simp add: mult_assoc times_divide_eq)
 done
 
 lemma real_average_minus_first [simp]: "((a + b) /2 - a) = (b-a)/(2::real)"
-by auto
+by (simp add: times_divide_eq) 
 
 lemma real_average_minus_second [simp]: "((b + a)/2 - a) = (b-a)/(2::real)"
-by auto
+by (simp add: times_divide_eq) 
 
 text{*Gallileo's "trick": average velocity = av. of end velocities*}
 
diff -r c55a12162944 -r ec91a90c604e src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -38,10 +38,11 @@
     "0 < h ==>
      \<exists>B. f h = sumr 0 n (%m. (j m / real (fact m)) * (h^m)) +
                (B * ((h^n) / real(fact n)))"
-by (rule_tac x = "(f h - sumr 0 n (%m. (j m / real (fact m)) * h^m)) *
+apply (rule_tac x = "(f h - sumr 0 n (%m. (j m / real (fact m)) * h^m)) *
                  real(fact n) / (h^n)"
-       in exI, auto)
-
+       in exI)
+apply (simp add: times_divide_eq) 
+done
 
 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
 by arith
@@ -159,12 +160,12 @@
  prefer 2 apply simp
 apply (frule Maclaurin_lemma2, assumption+)
 apply (subgoal_tac "\<forall>ma. ma < n --> (\<exists>t. 0 < t & t < h & difg (Suc ma) t = 0) ")
-apply (drule_tac x = m and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
-apply (erule impE)
-apply (simp (no_asm_simp))
-apply (erule exE)
-apply (rule_tac x = t in exI)
-apply (simp del: realpow_Suc fact_Suc)
+ apply (drule_tac x = m and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
+ apply (erule impE)
+  apply (simp (no_asm_simp))
+ apply (erule exE)
+ apply (rule_tac x = t in exI)
+ apply (simp add: times_divide_eq del: realpow_Suc fact_Suc)
 apply (subgoal_tac "\<forall>m. m < n --> difg m 0 = 0")
  prefer 2
  apply clarify
@@ -254,7 +255,7 @@
 apply (cut_tac f = "%x. f (-x)"
         and diff = "%n x. ((- 1) ^ n) * diff n (-x)"
         and h = "-h" and n = n in Maclaurin_objl)
-apply simp
+apply (simp add: times_divide_eq) 
 apply safe
 apply (subst minus_mult_right)
 apply (rule DERIV_cmult)
@@ -303,7 +304,7 @@
 apply (case_tac "n = 0", force)
 apply (case_tac "x = 0")
 apply (rule_tac x = 0 in exI)
-apply (force simp add: Maclaurin_bi_le_lemma)
+apply (force simp add: Maclaurin_bi_le_lemma times_divide_eq)
 apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
 txt{*Case 1, where @{term "x < 0"}*}
 apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
@@ -414,27 +415,8 @@
       "0 < n --> Suc (2 * n - 1) = 2*n"
 by (induct_tac "n", auto)
 
-lemma Maclaurin_sin_expansion:
-     "\<exists>t. sin x =
-       (sumr 0 n (%m. (if even m then 0
-                       else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
-                       x ^ m))
-      + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
-apply (cut_tac f = sin and n = n and x = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
-apply safe
-apply (simp (no_asm))
-apply (simp (no_asm))
-apply (case_tac "n", clarify, simp)
-apply (drule_tac x = 0 in spec, simp, simp)
-apply (rule ccontr, simp)
-apply (drule_tac x = x in spec, simp)
-apply (erule ssubst)
-apply (rule_tac x = t in exI, simp)
-apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc)
-(*Could sin_zero_iff help?*)
-done
+
+text{*It is unclear why so many variant results are needed.*}
 
 lemma Maclaurin_sin_expansion2:
      "\<exists>t. abs t \<le> abs x &
@@ -447,17 +429,28 @@
         and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
 apply safe
 apply (simp (no_asm))
-apply (simp (no_asm))
+apply (simp (no_asm) add: times_divide_eq)
 apply (case_tac "n", clarify, simp, simp)
 apply (rule ccontr, simp)
 apply (drule_tac x = x in spec, simp)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc)
+apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
 done
 
+lemma Maclaurin_sin_expansion:
+     "\<exists>t. sin x =
+       (sumr 0 n (%m. (if even m then 0
+                       else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
+                       x ^ m))
+      + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
+apply (insert Maclaurin_sin_expansion2 [of x n]) 
+apply (blast intro: elim:); 
+done
+
+
+
 lemma Maclaurin_sin_expansion3:
      "[| 0 < n; 0 < x |] ==>
        \<exists>t. 0 < t & t < x &
@@ -469,12 +462,11 @@
 apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl)
 apply safe
 apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: times_divide_eq)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc)
+apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
 done
 
 lemma Maclaurin_sin_expansion4:
@@ -488,12 +480,11 @@
 apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl)
 apply safe
 apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: times_divide_eq)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex simp del: fact_Suc realpow_Suc)
+apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
 done
 
 
@@ -518,7 +509,7 @@
 apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
 apply safe
 apply (simp (no_asm))
-apply (simp (no_asm))
+apply (simp (no_asm) add: times_divide_eq)
 apply (case_tac "n", simp)
 apply (simp del: sumr_Suc)
 apply (rule ccontr, simp)
@@ -526,9 +517,7 @@
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex left_distrib cos_add simp del: fact_Suc realpow_Suc)
-apply (simp add: mult_commute [of _ pi])
+apply (auto simp add: cos_zero_iff even_mult_two_ex)
 done
 
 lemma Maclaurin_cos_expansion2:
@@ -543,16 +532,15 @@
 apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl)
 apply safe
 apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: times_divide_eq)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex left_distrib cos_add simp del: fact_Suc realpow_Suc)
-apply (simp add: mult_commute [of _ pi])
+apply (auto simp add: cos_zero_iff even_mult_two_ex)
 done
 
-lemma Maclaurin_minus_cos_expansion: "[| x < 0; 0 < n |] ==>
+lemma Maclaurin_minus_cos_expansion:
+     "[| x < 0; 0 < n |] ==>
        \<exists>t. x < t & t < 0 &
        cos x =
        (sumr 0 n (%m. (if even m
@@ -563,13 +551,11 @@
 apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl)
 apply safe
 apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: times_divide_eq)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule sumr_fun_eq)
-apply (auto simp add: odd_Suc_mult_two_ex)
-apply (auto simp add: even_mult_two_ex left_distrib cos_add simp del: fact_Suc realpow_Suc)
-apply (simp add: mult_commute [of _ pi])
+apply (auto simp add: cos_zero_iff even_mult_two_ex)
 done
 
 (* ------------------------------------------------------------------------- *)
diff -r c55a12162944 -r ec91a90c604e src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -324,10 +324,8 @@
 apply (frule hrabs_less_gt_zero)
 apply (drule_tac x = "r/t" in bspec)
 apply (blast intro: SReal_divide)
-apply (simp add: zero_less_divide_iff)
-apply (case_tac "x=0 | y=0")
-apply (cut_tac [2] a = "abs x" and b = "r/t" and c = "abs y" in mult_strict_mono)
-apply (auto simp add: zero_less_divide_iff)
+apply (cut_tac a = "abs x" and b = "r/t" and c = "abs y" in mult_strict_mono)
+apply (auto simp add: times_divide_eq_left zero_less_divide_iff)
 done
 
 lemma Infinitesimal_HFinite_mult2:
diff -r c55a12162944 -r ec91a90c604e src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -259,11 +259,12 @@
 
 
 lemma sumr_pos_lt_pair:
-     "[|summable f; \<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|]  
+     "[|summable f; 
+        \<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|]  
       ==> sumr 0 n f < suminf f"
 apply (drule summable_sums)
 apply (auto simp add: sums_def LIMSEQ_def)
-apply (drule_tac x = "f (n) + f (n + 1) " in spec)
+apply (drule_tac x = "f (n) + f (n + 1)" in spec)
 apply (auto iff: real_0_less_add_iff)
    --{*legacy proof: not necessarily better!*}
 apply (rule_tac [2] ccontr, drule_tac [2] linorder_not_less [THEN iffD1])
@@ -312,17 +313,18 @@
 lemma sumr_geometric: "x ~= 1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - 1) / (x - 1)"
 apply (induct_tac "n", auto)
 apply (rule_tac c1 = "x - 1" in real_mult_right_cancel [THEN iffD1])
-apply (auto simp add: real_mult_assoc left_distrib)
-apply (simp add: right_distrib real_diff_def real_mult_commute)
+apply (auto simp add: mult_assoc left_distrib  times_divide_eq)
+apply (simp add: right_distrib diff_minus mult_commute)
 done
 
 lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))"
 apply (case_tac "x = 1")
-apply (auto dest!: LIMSEQ_rabs_realpow_zero2 simp add: sumr_geometric sums_def real_diff_def add_divide_distrib)
+apply (auto dest!: LIMSEQ_rabs_realpow_zero2 
+        simp add: sumr_geometric sums_def diff_minus add_divide_distrib)
 apply (subgoal_tac "1 / (1 + -x) = 0/ (x - 1) + - 1/ (x - 1) ")
 apply (erule ssubst)
 apply (rule LIMSEQ_add, rule LIMSEQ_divide)
-apply (auto intro: LIMSEQ_const simp add: real_diff_def minus_divide_right LIMSEQ_rabs_realpow_zero2)
+apply (auto intro: LIMSEQ_const simp add: diff_minus minus_divide_right LIMSEQ_rabs_realpow_zero2)
 done
 
 text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
@@ -433,18 +435,19 @@
      "[| c < 1; \<forall>n. N \<le> n --> abs(f(Suc n)) \<le> c*abs(f n) |]  
       ==> summable f"
 apply (frule ratio_test_lemma2, auto)
-apply (rule_tac g = "%n. (abs (f N) / (c ^ N))*c ^ n" in summable_comparison_test)
+apply (rule_tac g = "%n. (abs (f N) / (c ^ N))*c ^ n" 
+       in summable_comparison_test)
 apply (rule_tac x = N in exI, safe)
 apply (drule le_Suc_ex_iff [THEN iffD1])
 apply (auto simp add: power_add realpow_not_zero)
-apply (induct_tac "na", auto)
+apply (induct_tac "na", auto simp add: times_divide_eq)
 apply (rule_tac y = "c*abs (f (N + n))" in order_trans)
 apply (auto intro: mult_right_mono simp add: summable_def)
 apply (simp add: mult_ac)
-apply (rule_tac x = "abs (f N) * (1/ (1 - c)) / (c ^ N) " in exI)
-apply (rule sums_divide)
-apply (rule sums_mult)
-apply (auto intro!: sums_mult geometric_sums simp add: abs_if)
+apply (rule_tac x = "abs (f N) * (1/ (1 - c)) / (c ^ N)" in exI)
+apply (rule sums_divide) 
+apply (rule sums_mult) 
+apply (auto intro!: geometric_sums)
 done
 
 
diff -r c55a12162944 -r ec91a90c604e src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -424,9 +424,8 @@
 apply (subgoal_tac "x \<noteq> 0")
 apply (subgoal_tac [3] "x \<noteq> 0")
 apply (auto simp del: abs_inverse abs_mult simp add: abs_inverse [symmetric] realpow_not_zero abs_mult [symmetric] power_inverse power_mult_distrib [symmetric])
-apply (auto intro!: geometric_sums simp add: power_abs inverse_eq_divide)
-apply (rule_tac c="\<bar>x\<bar>" in mult_right_less_imp_less) 
-apply (auto simp add: abs_mult [symmetric] mult_assoc)
+apply (auto intro!: geometric_sums 
+            simp add: power_abs inverse_eq_divide times_divide_eq)
 done
 
 lemma powser_inside:
@@ -912,7 +911,7 @@
   hence "exp x * inverse (exp x) < exp y * inverse (exp x)"
     by (auto simp add: exp_add exp_minus)
   thus ?thesis
-    by (simp add: divide_inverse [symmetric] pos_less_divide_eq 
+    by (simp add: divide_inverse [symmetric] pos_less_divide_eq times_divide_eq
              del: divide_self_if)
 qed
 
@@ -1008,7 +1007,7 @@
 apply (rule ln_less_cancel_iff [THEN iffD2], auto)
 done
 
-lemma ln_ge_zero:
+lemma ln_ge_zero [simp]:
   assumes x: "1 \<le> x" shows "0 \<le> ln x"
 proof -
   have "0 < x" using x by arith
@@ -1029,6 +1028,9 @@
 lemma ln_ge_zero_iff [simp]: "0 < x ==> (0 \<le> ln x) = (1 \<le> x)"
 by (blast intro: ln_ge_zero ln_ge_zero_imp_ge_one)
 
+lemma ln_less_zero_iff [simp]: "0 < x ==> (ln x < 0) = (x < 1)"
+by (insert ln_ge_zero_iff [of x], arith)
+
 lemma ln_gt_zero:
   assumes x: "1 < x" shows "0 < ln x"
 proof -
@@ -1050,16 +1052,11 @@
 lemma ln_gt_zero_iff [simp]: "0 < x ==> (0 < ln x) = (1 < x)"
 by (blast intro: ln_gt_zero ln_gt_zero_imp_gt_one)
 
-lemma ln_not_eq_zero [simp]: "[| 0 < x; x \<noteq> 1 |] ==> ln x \<noteq> 0"
-apply safe
-apply (drule exp_inj_iff [THEN iffD2])
-apply (drule exp_ln_iff [THEN iffD2], auto)
-done
+lemma ln_eq_zero_iff [simp]: "0 < x ==> (ln x = 0) = (x = 1)"
+by (insert ln_less_zero_iff [of x] ln_gt_zero_iff [of x], arith)
 
 lemma ln_less_zero: "[| 0 < x; x < 1 |] ==> ln x < 0"
-apply (rule exp_less_cancel_iff [THEN iffD1])
-apply (auto simp add: exp_ln_iff [symmetric] simp del: exp_ln_iff)
-done
+by simp
 
 lemma exp_ln_eq: "exp u = x ==> ln x = u"
 by auto
@@ -1364,9 +1361,10 @@
 apply (erule sums_summable)
 apply (case_tac "m=0")
 apply (simp (no_asm_simp))
-apply (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x")
-apply (simp only: mult_less_cancel_left, simp)
-apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
+apply (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x") 
+apply (simp only: mult_less_cancel_left, simp add: times_divide_eq)  
+apply (simp (no_asm_simp) add: times_divide_eq 
+               numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
 apply (subgoal_tac "x*x < 2*3", simp) 
 apply (rule mult_strict_mono)
 apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
@@ -1425,10 +1423,10 @@
 apply (cut_tac x = 2 in cos_paired)
 apply (drule sums_minus)
 apply (rule neg_less_iff_less [THEN iffD1]) 
-apply (frule sums_unique, auto)
+apply (frule sums_unique, auto simp add: times_divide_eq)
 apply (rule_tac y = "sumr 0 (Suc (Suc (Suc 0))) (%n. - ((- 1) ^ n / (real (fact (2 * n))) * 2 ^ (2 * n)))" in order_less_trans)
 apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)
-apply (simp (no_asm) add: mult_assoc del: sumr_Suc)
+apply (simp (no_asm) add: mult_assoc times_divide_eq del: sumr_Suc)
 apply (rule sumr_pos_lt_pair)
 apply (erule sums_summable, safe)
 apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] 
@@ -1522,10 +1520,10 @@
 done
 
 lemma cos_pi [simp]: "cos pi = -1"
-by (cut_tac x = "pi/2" and y = "pi/2" in cos_add, simp)
+by (cut_tac x = "pi/2" and y = "pi/2" in cos_add, simp add: times_divide_eq)
 
 lemma sin_pi [simp]: "sin pi = 0"
-by (cut_tac x = "pi/2" and y = "pi/2" in sin_add, simp)
+by (cut_tac x = "pi/2" and y = "pi/2" in sin_add, simp add: times_divide_eq)
 
 lemma sin_cos_eq: "sin x = cos (pi/2 - x)"
 by (simp add: diff_minus cos_add)
@@ -1703,7 +1701,7 @@
 apply (cut_tac x="-x" in cos_zero_lemma, simp, simp) 
 apply (force simp add: minus_equation_iff [of x]) 
 apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib) 
-apply (auto simp add: cos_add)
+apply (auto simp add: cos_add times_divide_eq)
 done
 
 (* ditto: but to a lesser extent *)
@@ -1716,7 +1714,7 @@
 apply (drule sin_zero_lemma, assumption+)
 apply (cut_tac x="-x" in sin_zero_lemma, simp, simp, safe)
 apply (force simp add: minus_equation_iff [of x]) 
-apply (auto simp add: even_mult_two_ex)
+apply (auto simp add: even_mult_two_ex times_divide_eq)
 done
 
 
@@ -1746,7 +1744,7 @@
 apply (rule_tac c1 = "cos x * cos y" in real_mult_right_cancel [THEN subst])
 apply (auto simp del: inverse_mult_distrib 
             simp add: mult_assoc left_diff_distrib cos_add)
-done
+done  
 
 lemma add_tan_eq: 
       "[| cos x \<noteq> 0; cos y \<noteq> 0 |]  
@@ -1754,7 +1752,7 @@
 apply (simp add: tan_def)
 apply (rule_tac c1 = "cos x * cos y" in real_mult_right_cancel [THEN subst])
 apply (auto simp add: mult_assoc left_distrib)
-apply (simp (no_asm) add: sin_add)
+apply (simp add: sin_add times_divide_eq)
 done
 
 lemma tan_add:
@@ -2065,7 +2063,7 @@
 by (rule DERIV_exp [THEN DERIV_isCont])
 
 lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
-by (auto simp add: sin_zero_iff even_mult_two_ex)
+by (auto simp add: sin_zero_iff even_mult_two_ex times_divide_eq)
 
 lemma exp_eq_one_iff [simp]: "(exp x = 1) = (x = 0)"
 apply auto
@@ -2130,13 +2128,17 @@
      "[| 0 \<le> x; 0 \<le> y |] 
       ==> root(Suc n) (x * y) = root(Suc n) x * root(Suc n) y"
 apply (rule real_root_pos_unique)
-apply (auto intro!: real_root_pos_pos_le simp add: power_mult_distrib zero_le_mult_iff real_root_pow_pos2 simp del: realpow_Suc)
+apply (auto intro!: real_root_pos_pos_le 
+            simp add: power_mult_distrib zero_le_mult_iff real_root_pow_pos2 
+            simp del: realpow_Suc)
 done
 
 lemma real_root_inverse:
      "0 \<le> x ==> (root(Suc n) (inverse x) = inverse(root(Suc n) x))"
 apply (rule real_root_pos_unique)
-apply (auto intro: real_root_pos_pos_le simp add: power_inverse [symmetric] real_root_pow_pos2 simp del: realpow_Suc)
+apply (auto intro: real_root_pos_pos_le 
+            simp add: power_inverse [symmetric] real_root_pow_pos2 
+            simp del: realpow_Suc)
 done
 
 lemma real_root_divide: 
@@ -2449,11 +2451,11 @@
 apply (rule order_less_le_trans [of _ "7/5"], simp) 
 apply (rule_tac n = 1 in realpow_increasing)
   prefer 3 apply (simp add: numeral_2_eq_2 [symmetric] del: realpow_Suc)
-apply (simp_all add: numeral_2_eq_2)
+apply (simp_all add: numeral_2_eq_2 times_divide_eq)
 done
 
 lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u"
-by (rule_tac z1 = "inverse u" in real_mult_less_iff1 [THEN iffD1], auto)
+by (simp add: divide_less_eq mult_compare_simps) 
 
 lemma four_x_squared: 
   fixes x::real
@@ -2690,7 +2692,6 @@
 val ln_less_self = thm "ln_less_self";
 val ln_ge_zero = thm "ln_ge_zero";
 val ln_gt_zero = thm "ln_gt_zero";
-val ln_not_eq_zero = thm "ln_not_eq_zero";
 val ln_less_zero = thm "ln_less_zero";
 val exp_ln_eq = thm "exp_ln_eq";
 val sin_zero = thm "sin_zero";
diff -r c55a12162944 -r ec91a90c604e src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Integ/IntArith.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -326,38 +326,36 @@
 
 subsection{*Products and 1, by T. M. Rasmussen*}
 
-lemma zmult_eq_self_iff: "(m = m*(n::int)) = (n = 1 | m = 0)"
-apply auto
-apply (subgoal_tac "m*1 = m*n")
-apply (drule mult_cancel_left [THEN iffD1], auto)
+lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
+by arith
+
+lemma abs_zmult_eq_1: "(\<bar>m * n\<bar> = 1) ==> \<bar>m\<bar> = (1::int)"
+apply (case_tac "\<bar>n\<bar>=1") 
+apply (simp add: abs_mult) 
+apply (rule ccontr) 
+apply (auto simp add: linorder_neq_iff abs_mult) 
+apply (subgoal_tac "2 \<le> \<bar>m\<bar> & 2 \<le> \<bar>n\<bar>")
+ prefer 2 apply arith 
+apply (subgoal_tac "2*2 \<le> \<bar>m\<bar> * \<bar>n\<bar>", simp) 
+apply (rule mult_mono, auto) 
 done
 
-text{*FIXME: tidy*}
+lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1"
+by (insert abs_zmult_eq_1 [of m n], arith)
+
 lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
-apply auto
-apply (case_tac "m=1")
-apply (case_tac [2] "n=1")
-apply (case_tac [4] "m=1")
-apply (case_tac [5] "n=1", auto)
-apply (tactic"distinct_subgoals_tac")
-apply (subgoal_tac "1<m*n", simp)
-apply (rule less_1_mult, arith)
-apply (subgoal_tac "0<n", arith)
-apply (subgoal_tac "0<m*n")
-apply (drule zero_less_mult_iff [THEN iffD1], auto)
+apply (auto dest: pos_zmult_eq_1_iff_lemma) 
+apply (simp add: mult_commute [of m]) 
+apply (frule pos_zmult_eq_1_iff_lemma, auto) 
 done
 
 lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
-apply (case_tac "0<m")
-apply (simp add: pos_zmult_eq_1_iff)
-apply (case_tac "m=0")
-apply (simp del: number_of_reorient)
-apply (subgoal_tac "0 < -m")
-apply (drule_tac n = "-n" in pos_zmult_eq_1_iff, auto)
+apply (rule iffI) 
+ apply (frule pos_zmult_eq_1_iff_lemma)
+ apply (simp add: mult_commute [of m]) 
+ apply (frule pos_zmult_eq_1_iff_lemma, auto) 
 done
 
-
-
 ML
 {*
 val zle_diff1_eq = thm "zle_diff1_eq";
@@ -376,7 +374,6 @@
 val nat_le_eq_zle = thm "nat_le_eq_zle";
 
 val nat_intermed_int_val = thm "nat_intermed_int_val";
-val zmult_eq_self_iff = thm "zmult_eq_self_iff";
 val pos_zmult_eq_1_iff = thm "pos_zmult_eq_1_iff";
 val zmult_eq_1_iff = thm "zmult_eq_1_iff";
 val nat_add_distrib = thm "nat_add_distrib";
diff -r c55a12162944 -r ec91a90c604e src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Integ/IntDiv.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -241,7 +241,7 @@
 by(simp add: zmod_zdiv_equality[symmetric])
 
 lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k"
-by(simp add: zmult_commute zmod_zdiv_equality[symmetric])
+by(simp add: mult_commute zmod_zdiv_equality[symmetric])
 
 use "IntDiv_setup.ML"
 
@@ -606,7 +606,7 @@
 apply (rule trans)
 apply (rule_tac s = "b*a mod c" in trans)
 apply (rule_tac [2] zmod_zmult1_eq)
-apply (simp_all add: zmult_commute)
+apply (simp_all add: mult_commute)
 done
 
 lemma zmod_zmult_distrib: "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c"
@@ -618,13 +618,13 @@
 by (simp add: zdiv_zmult1_eq)
 
 lemma zdiv_zmult_self2 [simp]: "b \<noteq> (0::int) ==> (b*a) div b = a"
-by (subst zmult_commute, erule zdiv_zmult_self1)
+by (subst mult_commute, erule zdiv_zmult_self1)
 
 lemma zmod_zmult_self1 [simp]: "(a*b) mod b = (0::int)"
 by (simp add: zmod_zmult1_eq)
 
 lemma zmod_zmult_self2 [simp]: "(b*a) mod b = (0::int)"
-by (simp add: zmult_commute zmod_zmult1_eq)
+by (simp add: mult_commute zmod_zmult1_eq)
 
 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"
 proof
@@ -773,7 +773,7 @@
 
 lemma zdiv_zmult_zmult2: "c \<noteq> (0::int) ==> (a*c) div (b*c) = a div b"
 apply (drule zdiv_zmult_zmult1)
-apply (auto simp add: zmult_commute)
+apply (auto simp add: mult_commute)
 done
 
 
@@ -798,7 +798,7 @@
 
 lemma zmod_zmult_zmult2: "(a*c) mod (b*c) = (a mod b) * (c::int)"
 apply (cut_tac c = c in zmod_zmult_zmult1)
-apply (auto simp add: zmult_commute)
+apply (auto simp add: mult_commute)
 done
 
 
@@ -922,7 +922,7 @@
  prefer 2 apply arith
 apply (subgoal_tac "2* (1 + b mod a) \<le> 2*a")
  apply (rule_tac [2] mult_left_mono)
-apply (auto simp add: add_commute [of 1] zmult_commute add1_zle_eq 
+apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq 
                       pos_mod_bound)
 apply (subst zmod_zadd1_eq)
 apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
@@ -1009,7 +1009,7 @@
 by (auto simp add: dvd_def intro: zmult_1_right [symmetric])
 
 lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
-by (auto simp add: dvd_def intro: zmult_assoc)
+by (auto simp add: dvd_def intro: mult_assoc)
 
 lemma zdvd_zminus_iff: "(m dvd -n) = (m dvd (n::int))"
   apply (simp add: dvd_def, auto)
@@ -1024,7 +1024,7 @@
 lemma zdvd_anti_sym:
     "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
   apply (simp add: dvd_def, auto)
-  apply (simp add: zmult_assoc zmult_eq_self_iff zero_less_mult_iff zmult_eq_1_iff)
+  apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)
   done
 
 lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)"
@@ -1049,7 +1049,7 @@
   done
 
 lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"
-  apply (subst zmult_commute)
+  apply (subst mult_commute)
   apply (erule zdvd_zmult)
   done
 
@@ -1065,12 +1065,12 @@
 
 lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)"
   apply (simp add: dvd_def)
-  apply (simp add: zmult_assoc, blast)
+  apply (simp add: mult_assoc, blast)
   done
 
 lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)"
   apply (rule zdvd_zmultD2)
-  apply (subst zmult_commute, assumption)
+  apply (subst mult_commute, assumption)
   done
 
 lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
diff -r c55a12162944 -r ec91a90c604e src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Integ/NatBin.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -252,7 +252,7 @@
 lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2
 
 
-subsection{*General Theorems About Powers Involving Binary Numerals*}
+subsection{*Powers with Numeric Exponents*}
 
 text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}.
 We cannot prove general results about the numeral @{term "-1"}, so we have to
@@ -277,6 +277,11 @@
      "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,recpower}))"
   by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
 
+lemma power2_less_0 [simp]:
+  fixes a :: "'a::{ordered_idom,recpower}"
+  shows "~ (a\<twosuperior> < 0)"
+by (force simp add: power2_eq_square mult_less_0_iff) 
+
 lemma zero_eq_power2 [simp]:
      "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,recpower}))"
   by (force simp add: power2_eq_square mult_eq_0_iff)
@@ -340,6 +345,14 @@
 apply (force simp add: linorder_not_less [symmetric]) 
 done
 
+text{*Simprules for comparisons where common factors can be cancelled.*}
+lemmas zero_compare_simps =
+    add_strict_increasing add_strict_increasing2 add_increasing
+    zero_le_mult_iff zero_le_divide_iff 
+    zero_less_mult_iff zero_less_divide_iff 
+    mult_le_0_iff divide_le_0_iff 
+    mult_less_0_iff divide_less_0_iff 
+    zero_le_power2 power2_less_0
 
 subsubsection{*Nat *}
 
diff -r c55a12162944 -r ec91a90c604e src/HOL/Integ/NatSimprocs.thy
--- a/src/HOL/Integ/NatSimprocs.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Integ/NatSimprocs.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -174,6 +174,23 @@
 declare zero_le_divide_iff [of "number_of w", standard, simp]
 declare divide_le_0_iff [of "number_of w", standard, simp]
 
+(****
+IF times_divide_eq_right and times_divide_eq_left are removed as simprules,
+then these special-case declarations may be useful.
+
+text{*These simprules move numerals into numerators and denominators.*}
+lemma times_recip_eq_right [simp]: "a * (1/c) = a / (c::'a::field)"
+by (simp add: times_divide_eq)
+
+lemma times_recip_eq_left [simp]: "(1/c) * a = a / (c::'a::field)"
+by (simp add: times_divide_eq)
+
+declare times_divide_eq_right [of "number_of w", standard, simp]
+declare times_divide_eq_right [of _ _ "number_of w", standard, simp]
+declare times_divide_eq_left [of _ "number_of w", standard, simp]
+declare times_divide_eq_left [of _ _ "number_of w", standard, simp]
+****)
+
 text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
   strange, but then other simprocs simplify the quotient.*}
 
diff -r c55a12162944 -r ec91a90c604e src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/OrderedGroup.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -314,9 +314,22 @@
       "a + c \<le> b + c ==> a \<le> (b::'a::pordered_ab_semigroup_add_imp_le)"
 by simp
 
-lemma add_increasing: "[|0\<le>a; b\<le>c|] ==> b \<le> a + (c::'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add})"
+lemma add_increasing:
+  fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
+  shows  "[|0\<le>a; b\<le>c|] ==> b \<le> a + c"
 by (insert add_mono [of 0 a b c], simp)
 
+lemma add_strict_increasing:
+  fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
+  shows "[|0<a; b\<le>c|] ==> b < a + c"
+by (insert add_less_le_mono [of 0 a b c], simp)
+
+lemma add_strict_increasing2:
+  fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
+  shows "[|0\<le>a; b<c|] ==> b < a + c"
+by (insert add_le_less_mono [of 0 a b c], simp)
+
+
 subsection {* Ordering Rules for Unary Minus *}
 
 lemma le_imp_neg_le:
diff -r c55a12162944 -r ec91a90c604e src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Real/PReal.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -808,7 +808,7 @@
       also with ypos have "... = (r/y) * (y + ?d)"
 	by (simp only: right_distrib divide_inverse mult_ac, simp)
       also have "... = r*x" using ypos
-	by simp
+	by (simp add: times_divide_eq_left) 
       finally show "r + ?d < r*x" .
     qed
     with r notin rdpos
diff -r c55a12162944 -r ec91a90c604e src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Real/RComplete.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -153,7 +153,7 @@
 apply (rule lemma_real_complete2b)
 apply (erule_tac [2] order_less_imp_le)
 apply (blast intro!: isLubD2, blast) 
-apply (simp (no_asm_use) add: real_add_assoc)
+apply (simp (no_asm_use) add: add_assoc)
 apply (blast dest: isUbD intro!: setleI [THEN isUbI] intro: add_right_mono)
 apply (blast dest: isUbD intro!: setleI [THEN isUbI] intro: add_right_mono, auto)
 done
@@ -169,7 +169,7 @@
 apply (drule_tac x = n in spec)
 apply (drule_tac c = "real (Suc n)"  in mult_right_mono)
 apply (rule real_of_nat_ge_zero)
-apply (simp add: real_of_nat_Suc_gt_zero [THEN real_not_refl2, THEN not_sym] real_mult_commute)
+apply (simp add: times_divide_eq_right real_of_nat_Suc_gt_zero [THEN real_not_refl2, THEN not_sym] mult_commute)
 apply (subgoal_tac "isUb (UNIV::real set) {z. \<exists>n. z = x* (real (Suc n))} 1")
 apply (subgoal_tac "\<exists>X. X \<in> {z. \<exists>n. z = x* (real (Suc n))}")
 apply (drule reals_complete)
diff -r c55a12162944 -r ec91a90c604e src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/Ring_and_Field.thy	Thu Oct 07 15:42:30 2004 +0200
@@ -472,7 +472,10 @@
 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
    also with the relations @{text "\<le>"} and equality.*}
 
-lemma mult_less_cancel_right:
+text{*These ``disjunction'' versions produce two cases when the comparison is
+ an assumption, but effectively four when the comparison is a goal.*}
+
+lemma mult_less_cancel_right_disj:
     "(a*c < b*c) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring_strict)))"
 apply (case_tac "c = 0")
 apply (auto simp add: linorder_neq_iff mult_strict_right_mono 
@@ -485,7 +488,7 @@
                       mult_right_mono_neg)
 done
 
-lemma mult_less_cancel_left:
+lemma mult_less_cancel_left_disj:
     "(c*a < c*b) = ((0 < c & a < b) | (c < 0 & b < (a::'a::ordered_ring_strict)))"
 apply (case_tac "c = 0")
 apply (auto simp add: linorder_neq_iff mult_strict_left_mono 
@@ -498,13 +501,27 @@
                       mult_left_mono_neg)
 done
 
+
+text{*The ``conjunction of implication'' lemmas produce two cases when the
+comparison is a goal, but give four when the comparison is an assumption.*}
+
+lemma mult_less_cancel_right:
+  fixes c :: "'a :: ordered_ring_strict"
+  shows      "(a*c < b*c) = ((0 \<le> c --> a < b) & (c \<le> 0 --> b < a))"
+by (insert mult_less_cancel_right_disj [of a c b], auto)
+
+lemma mult_less_cancel_left:
+  fixes c :: "'a :: ordered_ring_strict"
+  shows      "(c*a < c*b) = ((0 \<le> c --> a < b) & (c \<le> 0 --> b < a))"
+by (insert mult_less_cancel_left_disj [of c a b], auto)
+
 lemma mult_le_cancel_right:
      "(a*c \<le> b*c) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring_strict)))"
-by (simp add: linorder_not_less [symmetric] mult_less_cancel_right)
+by (simp add: linorder_not_less [symmetric] mult_less_cancel_right_disj)
 
 lemma mult_le_cancel_left:
      "(c*a \<le> c*b) = ((0<c --> a\<le>b) & (c<0 --> b \<le> (a::'a::ordered_ring_strict)))"
-by (simp add: linorder_not_less [symmetric] mult_less_cancel_left)
+by (simp add: linorder_not_less [symmetric] mult_less_cancel_left_disj)
 
 lemma mult_less_imp_less_left:
       assumes less: "c*a < c*b" and nonneg: "0 \<le> c"
@@ -545,6 +562,85 @@
              simp add: linorder_neq_iff)
 done
 
+
+subsubsection{*Special Cancellation Simprules for Multiplication*}
+
+text{*These also produce two cases when the comparison is a goal.*}
+
+lemma mult_le_cancel_right1:
+  fixes c :: "'a :: ordered_idom"
+  shows "(c \<le> b*c) = ((0<c --> 1\<le>b) & (c<0 --> b \<le> 1))"
+by (insert mult_le_cancel_right [of 1 c b], simp)
+
+lemma mult_le_cancel_right2:
+  fixes c :: "'a :: ordered_idom"
+  shows "(a*c \<le> c) = ((0<c --> a\<le>1) & (c<0 --> 1 \<le> a))"
+by (insert mult_le_cancel_right [of a c 1], simp)
+
+lemma mult_le_cancel_left1:
+  fixes c :: "'a :: ordered_idom"
+  shows "(c \<le> c*b) = ((0<c --> 1\<le>b) & (c<0 --> b \<le> 1))"
+by (insert mult_le_cancel_left [of c 1 b], simp)
+
+lemma mult_le_cancel_left2:
+  fixes c :: "'a :: ordered_idom"
+  shows "(c*a \<le> c) = ((0<c --> a\<le>1) & (c<0 --> 1 \<le> a))"
+by (insert mult_le_cancel_left [of c a 1], simp)
+
+lemma mult_less_cancel_right1:
+  fixes c :: "'a :: ordered_idom"
+  shows "(c < b*c) = ((0 \<le> c --> 1<b) & (c \<le> 0 --> b < 1))"
+by (insert mult_less_cancel_right [of 1 c b], simp)
+
+lemma mult_less_cancel_right2:
+  fixes c :: "'a :: ordered_idom"
+  shows "(a*c < c) = ((0 \<le> c --> a<1) & (c \<le> 0 --> 1 < a))"
+by (insert mult_less_cancel_right [of a c 1], simp)
+
+lemma mult_less_cancel_left1:
+  fixes c :: "'a :: ordered_idom"
+  shows "(c < c*b) = ((0 \<le> c --> 1<b) & (c \<le> 0 --> b < 1))"
+by (insert mult_less_cancel_left [of c 1 b], simp)
+
+lemma mult_less_cancel_left2:
+  fixes c :: "'a :: ordered_idom"
+  shows "(c*a < c) = ((0 \<le> c --> a<1) & (c \<le> 0 --> 1 < a))"
+by (insert mult_less_cancel_left [of c a 1], simp)
+
+lemma mult_cancel_right1 [simp]:
+fixes c :: "'a :: ordered_idom"
+  shows "(c = b*c) = (c = 0 | b=1)"
+by (insert mult_cancel_right [of 1 c b], force)
+
+lemma mult_cancel_right2 [simp]:
+fixes c :: "'a :: ordered_idom"
+  shows "(a*c = c) = (c = 0 | a=1)"
+by (insert mult_cancel_right [of a c 1], simp)
+ 
+lemma mult_cancel_left1 [simp]:
+fixes c :: "'a :: ordered_idom"
+  shows "(c = c*b) = (c = 0 | b=1)"
+by (insert mult_cancel_left [of c 1 b], force)
+
+lemma mult_cancel_left2 [simp]:
+fixes c :: "'a :: ordered_idom"
+  shows "(c*a = c) = (c = 0 | a=1)"
+by (insert mult_cancel_left [of c a 1], simp)
+
+
+text{*Simprules for comparisons where common factors can be cancelled.*}
+lemmas mult_compare_simps =
+    mult_le_cancel_right mult_le_cancel_left
+    mult_le_cancel_right1 mult_le_cancel_right2
+    mult_le_cancel_left1 mult_le_cancel_left2
+    mult_less_cancel_right mult_less_cancel_left
+    mult_less_cancel_right1 mult_less_cancel_right2
+    mult_less_cancel_left1 mult_less_cancel_left2
+    mult_cancel_right mult_cancel_left
+    mult_cancel_right1 mult_cancel_right2
+    mult_cancel_left1 mult_cancel_left2
+
+
 text{*This list of rewrites decides ring equalities by ordered rewriting.*}
 lemmas ring_eq_simps =  
 (*  mult_ac*)
@@ -824,7 +920,7 @@
 lemma divide_1 [simp]: "a/1 = (a::'a::field)"
   by (simp add: divide_inverse)
 
-lemma times_divide_eq_right [simp]: "a * (b/c) = (a*b) / (c::'a::field)"
+lemma times_divide_eq_right: "a * (b/c) = (a*b) / (c::'a::field)"
 by (simp add: divide_inverse mult_assoc)
 
 lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
@@ -839,6 +935,59 @@
 by (simp add: divide_inverse mult_assoc)
 
 
+subsubsection{*Special Cancellation Simprules for Division*}
+
+lemma mult_divide_cancel_left_if [simp]:
+  fixes c :: "'a :: {field,division_by_zero}"
+  shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
+by (simp add: mult_divide_cancel_left)
+
+lemma mult_divide_cancel_right_if [simp]:
+  fixes c :: "'a :: {field,division_by_zero}"
+  shows "(a*c) / (b*c) = (if c=0 then 0 else a/b)"
+by (simp add: mult_divide_cancel_right)
+
+lemma mult_divide_cancel_left_if1 [simp]:
+  fixes c :: "'a :: {field,division_by_zero}"
+  shows "c / (c*b) = (if c=0 then 0 else 1/b)"
+apply (insert mult_divide_cancel_left_if [of c 1 b]) 
+apply (simp del: mult_divide_cancel_left_if)
+done
+
+lemma mult_divide_cancel_left_if2 [simp]:
+  fixes c :: "'a :: {field,division_by_zero}"
+  shows "(c*a) / c = (if c=0 then 0 else a)" 
+apply (insert mult_divide_cancel_left_if [of c a 1]) 
+apply (simp del: mult_divide_cancel_left_if)
+done
+
+lemma mult_divide_cancel_right_if1 [simp]:
+  fixes c :: "'a :: {field,division_by_zero}"
+  shows "c / (b*c) = (if c=0 then 0 else 1/b)"
+apply (insert mult_divide_cancel_right_if [of 1 c b]) 
+apply (simp del: mult_divide_cancel_right_if)
+done
+
+lemma mult_divide_cancel_right_if2 [simp]:
+  fixes c :: "'a :: {field,division_by_zero}"
+  shows "(a*c) / c = (if c=0 then 0 else a)" 
+apply (insert mult_divide_cancel_right_if [of a c 1]) 
+apply (simp del: mult_divide_cancel_right_if)
+done
+
+text{*Two lemmas for cancelling the denominator*}
+
+lemma times_divide_self_right [simp]: 
+  fixes a :: "'a :: {field,division_by_zero}"
+  shows "a * (b/a) = (if a=0 then 0 else b)"
+by (simp add: times_divide_eq_right)
+
+lemma times_divide_self_left [simp]: 
+  fixes a :: "'a :: {field,division_by_zero}"
+  shows "(b/a) * a = (if a=0 then 0 else b)"
+by (simp add: times_divide_eq_left)
+
+
 subsection {* Division and Unary Minus *}
 
 lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"
@@ -1167,7 +1316,7 @@
 proof -
   assume less: "0<c"
   hence "(a < b/c) = (a*c < (b/c)*c)"
-    by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
+    by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
   also have "... = (a*c < b)"
     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
   finally show ?thesis .
@@ -1178,7 +1327,7 @@
 proof -
   assume less: "c<0"
   hence "(a < b/c) = ((b/c)*c < a*c)"
-    by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
+    by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
   also have "... = (b < a*c)"
     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
   finally show ?thesis .
@@ -1198,7 +1347,7 @@
 proof -
   assume less: "0<c"
   hence "(b/c < a) = ((b/c)*c < a*c)"
-    by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
+    by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
   also have "... = (b < a*c)"
     by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc) 
   finally show ?thesis .
@@ -1209,7 +1358,7 @@
 proof -
   assume less: "c<0"
   hence "(b/c < a) = (a*c < (b/c)*c)"
-    by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
+    by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
   also have "... = (a*c < b)"
     by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc) 
   finally show ?thesis .
@@ -1252,6 +1401,7 @@
   "(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) 
 
+
 subsection{*Cancellation Laws for Division*}
 
 lemma divide_cancel_right [simp]:
@@ -1366,6 +1516,17 @@
 lemma dense: "a < b ==> \<exists>r::'a::ordered_field. a < r & r < b"
 by (blast intro!: less_half_sum gt_half_sum)
 
+
+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 
+  seem to need them.*}
+
+declare times_divide_eq [simp]
+
+
 subsection {* Absolute Value *}
 
 lemma abs_one [simp]: "abs 1 = (1::'a::ordered_idom)"
@@ -1486,7 +1647,7 @@
      "b \<noteq> 0 ==> abs (a / (b::'a::ordered_field)) = abs a / abs b"
 by (simp add: divide_inverse abs_mult nonzero_abs_inverse) 
 
-lemma abs_divide:
+lemma abs_divide [simp]:
      "abs (a / (b::'a::{ordered_field,division_by_zero})) = abs a / abs b"
 apply (case_tac "b=0", simp) 
 apply (simp add: nonzero_abs_divide) 
@@ -1513,9 +1674,6 @@
 apply (simp add: le_minus_self_iff linorder_neq_iff) 
 done
 
-text{*Moving this up spoils many proofs using @{text mult_le_cancel_right}*}
-declare times_divide_eq_left [simp]
-
 lemma linprog_dual_estimate:
   assumes
   "A * x \<le> (b::'a::lordered_ring)"
@@ -1670,6 +1828,8 @@
 val mult_strict_mono' = thm "mult_strict_mono'";
 val mult_mono = thm "mult_mono";
 val less_1_mult = thm "less_1_mult";
+val mult_less_cancel_right_disj = thm "mult_less_cancel_right_disj";
+val mult_less_cancel_left_disj = thm "mult_less_cancel_left_disj";
 val mult_less_cancel_right = thm "mult_less_cancel_right";
 val mult_less_cancel_left = thm "mult_less_cancel_left";
 val mult_le_cancel_right = thm "mult_le_cancel_right";
diff -r c55a12162944 -r ec91a90c604e src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Wed Oct 06 13:59:33 2004 +0200
+++ b/src/HOL/arith_data.ML	Thu Oct 07 15:42:30 2004 +0200
@@ -424,7 +424,11 @@
     mult_mono_thms = mult_mono_thms,
     inj_thms = inj_thms,
     lessD = lessD @ [Suc_leI],
-    simpset = HOL_basic_ss addsimps add_rules addsimprocs nat_cancel_sums_add}),
+    simpset = HOL_basic_ss addsimps add_rules
+                   addsimprocs [ab_group_add_cancel.sum_conv, 
+                                ab_group_add_cancel.rel_conv]
+                   (*abel_cancel helps it work in abstract algebraic domains*)
+                   addsimprocs nat_cancel_sums_add}),
   ArithTheoryData.init, arith_discrete "nat"];
 
 end;