tuned and used field_simps
authornipkow
Sun Jun 24 20:55:41 2007 +0200 (2007-06-24)
changeset 234822f4be6844f7c
parent 23481 93dca7620d0d
child 23483 a9356b40fbd3
tuned and used field_simps
src/HOL/Hyperreal/Ln.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Real/RealDef.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Hyperreal/Ln.thy	Sun Jun 24 20:47:05 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/Ln.thy	Sun Jun 24 20:55:41 2007 +0200
     1.3 @@ -36,12 +36,7 @@
     1.4  proof (induct n)
     1.5    show "inverse (real (fact (0 + 2))) * x ^ (0 + 2) <= 
     1.6        x ^ 2 / 2 * (1 / 2) ^ 0"
     1.7 -    apply (simp add: power2_eq_square)
     1.8 -    apply (subgoal_tac "real (Suc (Suc 0)) = 2")
     1.9 -    apply (erule ssubst)
    1.10 -    apply simp
    1.11 -    apply simp
    1.12 -    done
    1.13 +    by (simp add: real_of_nat_Suc power2_eq_square)
    1.14  next
    1.15    fix n
    1.16    assume c: "inverse (real (fact (n + 2))) * x ^ (n + 2)
    1.17 @@ -147,12 +142,6 @@
    1.18      by auto
    1.19  qed
    1.20  
    1.21 -lemma aux3: "(0::real) <= x ==> (1 + x + x^2)/(1 + x^2) <= 1 + x"
    1.22 -  apply (subst pos_divide_le_eq)
    1.23 -  apply (simp add: zero_compare_simps)
    1.24 -  apply (simp add: ring_simps zero_compare_simps)
    1.25 -done
    1.26 -
    1.27  lemma aux4: "0 <= (x::real) ==> x <= 1 ==> exp (x - x^2) <= 1 + x" 
    1.28  proof -
    1.29    assume a: "0 <= x" and b: "x <= 1"
    1.30 @@ -175,7 +164,7 @@
    1.31      apply auto
    1.32      done
    1.33    also from a have "... <= 1 + x"
    1.34 -    by (rule aux3)
    1.35 +    by(simp add:field_simps zero_compare_simps)
    1.36    finally show ?thesis .
    1.37  qed
    1.38  
    1.39 @@ -245,18 +234,7 @@
    1.40        by (insert a, auto)
    1.41      finally show ?thesis .
    1.42    qed
    1.43 -  also have " 1 / (1 - x) = 1 + x / (1 - x)"
    1.44 -  proof -
    1.45 -    have "1 / (1 - x) = (1 - x + x) / (1 - x)"
    1.46 -      by auto
    1.47 -    also have "... = (1 - x) / (1 - x) + x / (1 - x)"
    1.48 -      by (rule add_divide_distrib)
    1.49 -    also have "... = 1 + x / (1-x)"
    1.50 -      apply (subst add_right_cancel)
    1.51 -      apply (insert a, simp)
    1.52 -      done
    1.53 -    finally show ?thesis .
    1.54 -  qed
    1.55 +  also have " 1 / (1 - x) = 1 + x / (1 - x)" using a by(simp add:field_simps)
    1.56    finally show ?thesis .
    1.57  qed
    1.58  
    1.59 @@ -280,13 +258,10 @@
    1.60    also have "- (x / (1 - x)) = -x / (1 - x)"
    1.61      by auto
    1.62    finally have d: "- x / (1 - x) <= ln (1 - x)" .
    1.63 -  have e: "-x - 2 * x^2 <= - x / (1 - x)"
    1.64 -    apply (rule mult_imp_le_div_pos)
    1.65 -    apply (insert prems, force)
    1.66 -    apply (auto simp add: ring_simps power2_eq_square)
    1.67 -    apply(insert mult_right_le_one_le[of "x*x" "2*x"])
    1.68 -    apply (simp)
    1.69 -    done
    1.70 +  have "0 < 1 - x" using prems by simp
    1.71 +  hence e: "-x - 2 * x^2 <= - x / (1 - x)"
    1.72 +    using mult_right_le_one_le[of "x*x" "2*x"] prems
    1.73 +    by(simp add:field_simps power2_eq_square)
    1.74    from e d show "- x - 2 * x^2 <= ln (1 - x)"
    1.75      by (rule order_trans)
    1.76  qed
    1.77 @@ -427,21 +402,15 @@
    1.78      done
    1.79    also have "y / x = (x + (y - x)) / x"
    1.80      by simp
    1.81 -  also have "... = 1 + (y - x) / x"
    1.82 -    apply (simp only: add_divide_distrib)
    1.83 -    apply (simp add: prems)
    1.84 -    apply (insert a, arith)
    1.85 -    done
    1.86 +  also have "... = 1 + (y - x) / x" using a prems by(simp add:field_simps)
    1.87    also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
    1.88      apply (rule mult_left_mono)
    1.89      apply (rule ln_add_one_self_le_self)
    1.90      apply (rule divide_nonneg_pos)
    1.91      apply (insert prems a, simp_all) 
    1.92      done
    1.93 -  also have "... = y - x"
    1.94 -    by (insert a, simp)
    1.95 -  also have "... = (y - x) * ln (exp 1)"
    1.96 -    by simp
    1.97 +  also have "... = y - x" using a by simp
    1.98 +  also have "... = (y - x) * ln (exp 1)" by simp
    1.99    also have "... <= (y - x) * ln x"
   1.100      apply (rule mult_left_mono)
   1.101      apply (subst ln_le_cancel_iff)
   1.102 @@ -454,18 +423,9 @@
   1.103      by (rule left_diff_distrib)
   1.104    finally have "x * ln y <= y * ln x"
   1.105      by arith
   1.106 -  then have "ln y <= (y * ln x) / x"
   1.107 -    apply (subst pos_le_divide_eq)
   1.108 -    apply (rule a)
   1.109 -    apply (simp add: mult_ac)
   1.110 -    done
   1.111 -  also have "... = y * (ln x / x)"
   1.112 -    by simp
   1.113 -  finally show ?thesis 
   1.114 -    apply (subst pos_divide_le_eq)
   1.115 -    apply (rule b)
   1.116 -    apply (simp add: mult_ac)
   1.117 -    done
   1.118 +  then have "ln y <= (y * ln x) / x" using a by(simp add:field_simps)
   1.119 +  also have "... = y * (ln x / x)"  by simp
   1.120 +  finally show ?thesis using b by(simp add:field_simps)
   1.121  qed
   1.122  
   1.123  end
     2.1 --- a/src/HOL/Hyperreal/SEQ.thy	Sun Jun 24 20:47:05 2007 +0200
     2.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Sun Jun 24 20:55:41 2007 +0200
     2.3 @@ -904,8 +904,7 @@
     2.4      have "norm (X m - X n) = norm ((X m - a) - (X n - a))" by simp
     2.5      also have "\<dots> \<le> norm (X m - a) + norm (X n - a)"
     2.6        by (rule norm_triangle_ineq4)
     2.7 -    also from m n have "\<dots> < e/2 + e/2" by (rule add_strict_mono)
     2.8 -    also have "e/2 + e/2 = e" by simp
     2.9 +    also from m n have "\<dots> < e" by(simp add:field_simps)
    2.10      finally show "norm (X m - X n) < e" .
    2.11    qed
    2.12  qed
    2.13 @@ -988,22 +987,17 @@
    2.14  
    2.15    from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast
    2.16    hence "X N - r/2 \<in> S" by (rule mem_S)
    2.17 -  hence "X N - r/2 \<le> x" using x isLub_isUb isUbD by fast
    2.18 -  hence 1: "X N + r/2 \<le> x + r" by simp
    2.19 +  hence 1: "X N - r/2 \<le> x" using x isLub_isUb isUbD by fast
    2.20  
    2.21    from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast
    2.22    hence "isUb UNIV S (X N + r/2)" by (rule bound_isUb)
    2.23 -  hence "x \<le> X N + r/2" using x isLub_le_isUb by fast
    2.24 -  hence 2: "x - r \<le> X N - r/2" by simp
    2.25 +  hence 2: "x \<le> X N + r/2" using x isLub_le_isUb by fast
    2.26  
    2.27    show "\<exists>N. \<forall>n\<ge>N. norm (X n - x) < r"
    2.28    proof (intro exI allI impI)
    2.29      fix n assume n: "N \<le> n"
    2.30 -    from N n have 3: "X n < X N + r/2" by simp
    2.31 -    from N n have 4: "X N - r/2 < X n" by simp
    2.32 -    show "norm (X n - x) < r"
    2.33 -      using order_less_le_trans [OF 3 1]
    2.34 -            order_le_less_trans [OF 2 4]
    2.35 +    from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+
    2.36 +    thus "norm (X n - x) < r" using 1 2
    2.37        by (simp add: real_abs_diff_less_iff)
    2.38    qed
    2.39  qed
     3.1 --- a/src/HOL/Real/RealDef.thy	Sun Jun 24 20:47:05 2007 +0200
     3.2 +++ b/src/HOL/Real/RealDef.thy	Sun Jun 24 20:55:41 2007 +0200
     3.3 @@ -526,10 +526,6 @@
     3.4  lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
     3.5  by(simp add:mult_commute)
     3.6  
     3.7 -(* FIXME: redundant, but used by Integration/Integral.thy in AFP *)
     3.8 -lemma real_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::real) \<le> x + y"
     3.9 -by (rule add_nonneg_nonneg)
    3.10 -
    3.11  lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x"
    3.12  by (simp add: one_less_inverse_iff) (* TODO: generalize/move *)
    3.13  
     4.1 --- a/src/HOL/Ring_and_Field.thy	Sun Jun 24 20:47:05 2007 +0200
     4.2 +++ b/src/HOL/Ring_and_Field.thy	Sun Jun 24 20:55:41 2007 +0200
     4.3 @@ -773,12 +773,13 @@
     4.4  lemma add_divide_distrib: "(a+b)/(c::'a::field) = a/c + b/c"
     4.5  by (simp add: divide_inverse ring_distribs) 
     4.6  
     4.7 -
     4.8 +(* what ordering?? this is a straight instance of mult_eq_0_iff
     4.9  text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
    4.10        of an ordering.*}
    4.11  lemma field_mult_eq_0_iff [simp]:
    4.12    "(a*b = (0::'a::division_ring)) = (a = 0 | b = 0)"
    4.13  by simp
    4.14 +*)
    4.15  
    4.16  text{*Cancellation of equalities with a common factor*}
    4.17  lemma field_mult_cancel_right_lemma:
    4.18 @@ -915,7 +916,7 @@
    4.19        shows "inverse(a*b) = inverse(b) * inverse(a::'a::division_ring)"
    4.20    proof -
    4.21    have "inverse(a*b) * (a * b) * inverse(b) = inverse(b)" 
    4.22 -    by (simp add: field_mult_eq_0_iff anz bnz)
    4.23 +    by (simp add: anz bnz)
    4.24    hence "inverse(a*b) * a = inverse(b)" 
    4.25      by (simp add: mult_assoc bnz)
    4.26    hence "inverse(a*b) * a * inverse(a) = inverse(b) * inverse(a)" 
    4.27 @@ -969,8 +970,7 @@
    4.28  assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/(b::'a::field)"
    4.29  proof -
    4.30    have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
    4.31 -    by (simp add: field_mult_eq_0_iff divide_inverse 
    4.32 -                  nonzero_inverse_mult_distrib)
    4.33 +    by (simp add: divide_inverse nonzero_inverse_mult_distrib)
    4.34    also have "... =  a * inverse b * (inverse c * c)"
    4.35      by (simp only: mult_ac)
    4.36    also have "... =  a * inverse b"
    4.37 @@ -1004,6 +1004,8 @@
    4.38  lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
    4.39  by (simp add: divide_inverse mult_ac)
    4.40  
    4.41 +lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
    4.42 +
    4.43  lemma divide_divide_eq_right [simp]:
    4.44    "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
    4.45  by (simp add: divide_inverse mult_ac)
    4.46 @@ -1098,53 +1100,120 @@
    4.47  lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c"
    4.48  by (simp add: diff_minus add_divide_distrib) 
    4.49  
    4.50 +lemma add_divide_eq_iff:
    4.51 +  "(z::'a::field) \<noteq> 0 \<Longrightarrow> x + y/z = (z*x + y)/z"
    4.52 +by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)
    4.53 +
    4.54 +lemma divide_add_eq_iff:
    4.55 +  "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z + y = (x + z*y)/z"
    4.56 +by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)
    4.57 +
    4.58 +lemma diff_divide_eq_iff:
    4.59 +  "(z::'a::field) \<noteq> 0 \<Longrightarrow> x - y/z = (z*x - y)/z"
    4.60 +by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)
    4.61 +
    4.62 +lemma divide_diff_eq_iff:
    4.63 +  "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z - y = (x - z*y)/z"
    4.64 +by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)
    4.65 +
    4.66 +lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"
    4.67 +proof -
    4.68 +  assume [simp]: "c\<noteq>0"
    4.69 +  have "(a = b/c) = (a*c = (b/c)*c)"
    4.70 +    by (simp add: field_mult_cancel_right)
    4.71 +  also have "... = (a*c = b)"
    4.72 +    by (simp add: divide_inverse mult_assoc)
    4.73 +  finally show ?thesis .
    4.74 +qed
    4.75 +
    4.76 +lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"
    4.77 +proof -
    4.78 +  assume [simp]: "c\<noteq>0"
    4.79 +  have "(b/c = a) = ((b/c)*c = a*c)"
    4.80 +    by (simp add: field_mult_cancel_right)
    4.81 +  also have "... = (b = a*c)"
    4.82 +    by (simp add: divide_inverse mult_assoc) 
    4.83 +  finally show ?thesis .
    4.84 +qed
    4.85 +
    4.86 +lemma eq_divide_eq:
    4.87 +  "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
    4.88 +by (simp add: nonzero_eq_divide_eq) 
    4.89 +
    4.90 +lemma divide_eq_eq:
    4.91 +  "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
    4.92 +by (force simp add: nonzero_divide_eq_eq) 
    4.93 +
    4.94 +lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
    4.95 +    b = a * c ==> b / c = a"
    4.96 +  by (subst divide_eq_eq, simp)
    4.97 +
    4.98 +lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
    4.99 +    a * c = b ==> a = b / c"
   4.100 +  by (subst eq_divide_eq, simp)
   4.101 +
   4.102 +
   4.103 +lemmas field_eq_simps = ring_simps
   4.104 +  (* pull / out*)
   4.105 +  add_divide_eq_iff divide_add_eq_iff
   4.106 +  diff_divide_eq_iff divide_diff_eq_iff
   4.107 +  (* multiply eqn *)
   4.108 +  nonzero_eq_divide_eq nonzero_divide_eq_eq
   4.109 +(* is added later:
   4.110 +  times_divide_eq_left times_divide_eq_right
   4.111 +*)
   4.112 +
   4.113 +text{*An example:*}
   4.114 +lemma fixes a b c d e f :: "'a::field"
   4.115 +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"
   4.116 +apply(subgoal_tac "(c-d)*(e-f)*(a-b) \<noteq> 0")
   4.117 + apply(simp add:field_eq_simps)
   4.118 +apply(simp)
   4.119 +done
   4.120 +
   4.121 +
   4.122  lemma diff_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
   4.123      x / y - w / z = (x * z - w * y) / (y * z)"
   4.124 -apply (subst diff_def)+
   4.125 -apply (subst minus_divide_left)
   4.126 -apply (subst add_frac_eq)
   4.127 -apply simp_all
   4.128 -done
   4.129 +by (simp add:field_eq_simps times_divide_eq)
   4.130 +
   4.131 +lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
   4.132 +    (x / y = w / z) = (x * z = w * y)"
   4.133 +by (simp add:field_eq_simps times_divide_eq)
   4.134  
   4.135  
   4.136  subsection {* Ordered Fields *}
   4.137  
   4.138  lemma positive_imp_inverse_positive: 
   4.139 -      assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::ordered_field)"
   4.140 -  proof -
   4.141 +assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::ordered_field)"
   4.142 +proof -
   4.143    have "0 < a * inverse a" 
   4.144      by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
   4.145    thus "0 < inverse a" 
   4.146      by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
   4.147 -  qed
   4.148 +qed
   4.149  
   4.150  lemma negative_imp_inverse_negative:
   4.151 -     "a < 0 ==> inverse a < (0::'a::ordered_field)"
   4.152 -  by (insert positive_imp_inverse_positive [of "-a"], 
   4.153 -      simp add: nonzero_inverse_minus_eq order_less_imp_not_eq) 
   4.154 +  "a < 0 ==> inverse a < (0::'a::ordered_field)"
   4.155 +by (insert positive_imp_inverse_positive [of "-a"], 
   4.156 +    simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)
   4.157  
   4.158  lemma inverse_le_imp_le:
   4.159 -      assumes invle: "inverse a \<le> inverse b"
   4.160 -	  and apos:  "0 < a"
   4.161 -	 shows "b \<le> (a::'a::ordered_field)"
   4.162 -  proof (rule classical)
   4.163 +assumes invle: "inverse a \<le> inverse b" and apos:  "0 < a"
   4.164 +shows "b \<le> (a::'a::ordered_field)"
   4.165 +proof (rule classical)
   4.166    assume "~ b \<le> a"
   4.167 -  hence "a < b"
   4.168 -    by (simp add: linorder_not_le)
   4.169 -  hence bpos: "0 < b"
   4.170 -    by (blast intro: apos order_less_trans)
   4.171 +  hence "a < b"  by (simp add: linorder_not_le)
   4.172 +  hence bpos: "0 < b"  by (blast intro: apos order_less_trans)
   4.173    hence "a * inverse a \<le> a * inverse b"
   4.174      by (simp add: apos invle order_less_imp_le mult_left_mono)
   4.175    hence "(a * inverse a) * b \<le> (a * inverse b) * b"
   4.176      by (simp add: bpos order_less_imp_le mult_right_mono)
   4.177 -  thus "b \<le> a"
   4.178 -    by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
   4.179 -  qed
   4.180 +  thus "b \<le> a"  by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
   4.181 +qed
   4.182  
   4.183  lemma inverse_positive_imp_positive:
   4.184 -  assumes inv_gt_0: "0 < inverse a"
   4.185 -    and nz: "a \<noteq> 0"
   4.186 -  shows "0 < (a::'a::ordered_field)"
   4.187 +assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
   4.188 +shows "0 < (a::'a::ordered_field)"
   4.189  proof -
   4.190    have "0 < inverse (inverse a)"
   4.191      using inv_gt_0 by (rule positive_imp_inverse_positive)
   4.192 @@ -1153,34 +1222,32 @@
   4.193  qed
   4.194  
   4.195  lemma inverse_positive_iff_positive [simp]:
   4.196 -      "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
   4.197 +  "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
   4.198  apply (cases "a = 0", simp)
   4.199  apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
   4.200  done
   4.201  
   4.202  lemma inverse_negative_imp_negative:
   4.203 -  assumes inv_less_0: "inverse a < 0"
   4.204 -    and nz:  "a \<noteq> 0"
   4.205 -  shows "a < (0::'a::ordered_field)"
   4.206 +assumes inv_less_0: "inverse a < 0" and nz:  "a \<noteq> 0"
   4.207 +shows "a < (0::'a::ordered_field)"
   4.208  proof -
   4.209    have "inverse (inverse a) < 0"
   4.210      using inv_less_0 by (rule negative_imp_inverse_negative)
   4.211 -  thus "a < 0"
   4.212 -    using nz by (simp add: nonzero_inverse_inverse_eq)
   4.213 +  thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
   4.214  qed
   4.215  
   4.216  lemma inverse_negative_iff_negative [simp]:
   4.217 -      "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
   4.218 +  "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
   4.219  apply (cases "a = 0", simp)
   4.220  apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
   4.221  done
   4.222  
   4.223  lemma inverse_nonnegative_iff_nonnegative [simp]:
   4.224 -      "(0 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"
   4.225 +  "(0 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"
   4.226  by (simp add: linorder_not_less [symmetric])
   4.227  
   4.228  lemma inverse_nonpositive_iff_nonpositive [simp]:
   4.229 -      "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"
   4.230 +  "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"
   4.231  by (simp add: linorder_not_less [symmetric])
   4.232  
   4.233  lemma ordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::ordered_field)"
   4.234 @@ -1204,10 +1271,9 @@
   4.235  subsection{*Anti-Monotonicity of @{term inverse}*}
   4.236  
   4.237  lemma less_imp_inverse_less:
   4.238 -      assumes less: "a < b"
   4.239 -	  and apos:  "0 < a"
   4.240 -	shows "inverse b < inverse (a::'a::ordered_field)"
   4.241 -  proof (rule ccontr)
   4.242 +assumes less: "a < b" and apos:  "0 < a"
   4.243 +shows "inverse b < inverse (a::'a::ordered_field)"
   4.244 +proof (rule ccontr)
   4.245    assume "~ inverse b < inverse a"
   4.246    hence "inverse a \<le> inverse b"
   4.247      by (simp add: linorder_not_less)
   4.248 @@ -1215,81 +1281,78 @@
   4.249      by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])
   4.250    thus False
   4.251      by (rule notE [OF _ less])
   4.252 -  qed
   4.253 +qed
   4.254  
   4.255  lemma inverse_less_imp_less:
   4.256 -   "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"
   4.257 +  "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"
   4.258  apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])
   4.259  apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) 
   4.260  done
   4.261  
   4.262  text{*Both premises are essential. Consider -1 and 1.*}
   4.263  lemma inverse_less_iff_less [simp]:
   4.264 -     "[|0 < a; 0 < b|] 
   4.265 -      ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
   4.266 +  "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
   4.267  by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
   4.268  
   4.269  lemma le_imp_inverse_le:
   4.270 -   "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
   4.271 -  by (force simp add: order_le_less less_imp_inverse_less)
   4.272 +  "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
   4.273 +by (force simp add: order_le_less less_imp_inverse_less)
   4.274  
   4.275  lemma inverse_le_iff_le [simp]:
   4.276 -     "[|0 < a; 0 < b|] 
   4.277 -      ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
   4.278 + "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
   4.279  by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
   4.280  
   4.281  
   4.282  text{*These results refer to both operands being negative.  The opposite-sign
   4.283  case is trivial, since inverse preserves signs.*}
   4.284  lemma inverse_le_imp_le_neg:
   4.285 -   "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"
   4.286 -  apply (rule classical) 
   4.287 -  apply (subgoal_tac "a < 0") 
   4.288 -   prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans) 
   4.289 -  apply (insert inverse_le_imp_le [of "-b" "-a"])
   4.290 -  apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
   4.291 -  done
   4.292 +  "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"
   4.293 +apply (rule classical) 
   4.294 +apply (subgoal_tac "a < 0") 
   4.295 + prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans) 
   4.296 +apply (insert inverse_le_imp_le [of "-b" "-a"])
   4.297 +apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
   4.298 +done
   4.299  
   4.300  lemma less_imp_inverse_less_neg:
   4.301     "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::ordered_field)"
   4.302 -  apply (subgoal_tac "a < 0") 
   4.303 -   prefer 2 apply (blast intro: order_less_trans) 
   4.304 -  apply (insert less_imp_inverse_less [of "-b" "-a"])
   4.305 -  apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
   4.306 -  done
   4.307 +apply (subgoal_tac "a < 0") 
   4.308 + prefer 2 apply (blast intro: order_less_trans) 
   4.309 +apply (insert less_imp_inverse_less [of "-b" "-a"])
   4.310 +apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
   4.311 +done
   4.312  
   4.313  lemma inverse_less_imp_less_neg:
   4.314     "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::ordered_field)"
   4.315 -  apply (rule classical) 
   4.316 -  apply (subgoal_tac "a < 0") 
   4.317 -   prefer 2
   4.318 -   apply (force simp add: linorder_not_less intro: order_le_less_trans) 
   4.319 -  apply (insert inverse_less_imp_less [of "-b" "-a"])
   4.320 -  apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
   4.321 -  done
   4.322 +apply (rule classical) 
   4.323 +apply (subgoal_tac "a < 0") 
   4.324 + prefer 2
   4.325 + apply (force simp add: linorder_not_less intro: order_le_less_trans) 
   4.326 +apply (insert inverse_less_imp_less [of "-b" "-a"])
   4.327 +apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
   4.328 +done
   4.329  
   4.330  lemma inverse_less_iff_less_neg [simp]:
   4.331 -     "[|a < 0; b < 0|] 
   4.332 -      ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
   4.333 -  apply (insert inverse_less_iff_less [of "-b" "-a"])
   4.334 -  apply (simp del: inverse_less_iff_less 
   4.335 -	      add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
   4.336 -  done
   4.337 +  "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
   4.338 +apply (insert inverse_less_iff_less [of "-b" "-a"])
   4.339 +apply (simp del: inverse_less_iff_less 
   4.340 +            add: order_less_imp_not_eq nonzero_inverse_minus_eq)
   4.341 +done
   4.342  
   4.343  lemma le_imp_inverse_le_neg:
   4.344 -   "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
   4.345 -  by (force simp add: order_le_less less_imp_inverse_less_neg)
   4.346 +  "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
   4.347 +by (force simp add: order_le_less less_imp_inverse_less_neg)
   4.348  
   4.349  lemma inverse_le_iff_le_neg [simp]:
   4.350 -     "[|a < 0; b < 0|] 
   4.351 -      ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
   4.352 + "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
   4.353  by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
   4.354  
   4.355  
   4.356  subsection{*Inverses and the Number One*}
   4.357  
   4.358  lemma one_less_inverse_iff:
   4.359 -    "(1 < inverse x) = (0 < x & x < (1::'a::{ordered_field,division_by_zero}))"proof cases
   4.360 +  "(1 < inverse x) = (0 < x & x < (1::'a::{ordered_field,division_by_zero}))"
   4.361 +proof cases
   4.362    assume "0 < x"
   4.363      with inverse_less_iff_less [OF zero_less_one, of x]
   4.364      show ?thesis by simp
   4.365 @@ -1306,20 +1369,20 @@
   4.366  qed
   4.367  
   4.368  lemma inverse_eq_1_iff [simp]:
   4.369 -    "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
   4.370 +  "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
   4.371  by (insert inverse_eq_iff_eq [of x 1], simp) 
   4.372  
   4.373  lemma one_le_inverse_iff:
   4.374 -   "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{ordered_field,division_by_zero}))"
   4.375 +  "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{ordered_field,division_by_zero}))"
   4.376  by (force simp add: order_le_less one_less_inverse_iff zero_less_one 
   4.377                      eq_commute [of 1]) 
   4.378  
   4.379  lemma inverse_less_1_iff:
   4.380 -   "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{ordered_field,division_by_zero}))"
   4.381 +  "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{ordered_field,division_by_zero}))"
   4.382  by (simp add: linorder_not_le [symmetric] one_le_inverse_iff) 
   4.383  
   4.384  lemma inverse_le_1_iff:
   4.385 -   "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
   4.386 +  "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
   4.387  by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) 
   4.388  
   4.389  
   4.390 @@ -1445,49 +1508,41 @@
   4.391  apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff) 
   4.392  done
   4.393  
   4.394 -lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"
   4.395 -proof -
   4.396 -  assume [simp]: "c\<noteq>0"
   4.397 -  have "(a = b/c) = (a*c = (b/c)*c)"
   4.398 -    by (simp add: field_mult_cancel_right)
   4.399 -  also have "... = (a*c = b)"
   4.400 -    by (simp add: divide_inverse mult_assoc) 
   4.401 -  finally show ?thesis .
   4.402 -qed
   4.403 +
   4.404 +subsection{*Field simplification*}
   4.405 +
   4.406 +text{* Lemmas @{text field_simps} multiply with denominators in
   4.407 +in(equations) if they can be proved to be non-zero (for equations) or
   4.408 +positive/negative (for inequations). *}
   4.409  
   4.410 -lemma eq_divide_eq:
   4.411 -  "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
   4.412 -by (simp add: nonzero_eq_divide_eq) 
   4.413 +lemmas field_simps = field_eq_simps
   4.414 +  (* multiply ineqn *)
   4.415 +  pos_divide_less_eq neg_divide_less_eq
   4.416 +  pos_less_divide_eq neg_less_divide_eq
   4.417 +  pos_divide_le_eq neg_divide_le_eq
   4.418 +  pos_le_divide_eq neg_le_divide_eq
   4.419  
   4.420 -lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"
   4.421 -proof -
   4.422 -  assume [simp]: "c\<noteq>0"
   4.423 -  have "(b/c = a) = ((b/c)*c = a*c)"
   4.424 -    by (simp add: field_mult_cancel_right)
   4.425 -  also have "... = (b = a*c)"
   4.426 -    by (simp add: divide_inverse mult_assoc) 
   4.427 -  finally show ?thesis .
   4.428 -qed
   4.429 +text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
   4.430 +of positivity/negativity needed for field_simps. Have not added @{text
   4.431 +sign_simps} to @{text field_simps} because the former can lead to case
   4.432 +explosions. *}
   4.433  
   4.434 -lemma divide_eq_eq:
   4.435 -  "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
   4.436 -by (force simp add: nonzero_divide_eq_eq) 
   4.437 +lemmas sign_simps = group_simps
   4.438 +  zero_less_mult_iff  mult_less_0_iff
   4.439  
   4.440 -lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
   4.441 -    b = a * c ==> b / c = a"
   4.442 -  by (subst divide_eq_eq, simp)
   4.443 -
   4.444 -lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
   4.445 -    a * c = b ==> a = b / c"
   4.446 -  by (subst eq_divide_eq, simp)
   4.447 -
   4.448 -lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
   4.449 -    (x / y = w / z) = (x * z = w * y)"
   4.450 -  apply (subst nonzero_eq_divide_eq)
   4.451 -  apply assumption
   4.452 -  apply (subst times_divide_eq_left)
   4.453 -  apply (erule nonzero_divide_eq_eq) 
   4.454 +(* Only works once linear arithmetic is installed:
   4.455 +text{*An example:*}
   4.456 +lemma fixes a b c d e f :: "'a::ordered_field"
   4.457 +shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
   4.458 + ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
   4.459 + ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
   4.460 +apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
   4.461 + prefer 2 apply(simp add:sign_simps)
   4.462 +apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
   4.463 + prefer 2 apply(simp add:sign_simps)
   4.464 +apply(simp add:field_simps)
   4.465  done
   4.466 +*)
   4.467  
   4.468  
   4.469  subsection{*Division and Signs*}
   4.470 @@ -1513,74 +1568,54 @@
   4.471  
   4.472  lemma divide_eq_0_iff [simp]:
   4.473       "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
   4.474 -by (simp add: divide_inverse field_mult_eq_0_iff)
   4.475 +by (simp add: divide_inverse)
   4.476  
   4.477 -lemma divide_pos_pos: "0 < (x::'a::ordered_field) ==> 
   4.478 -    0 < y ==> 0 < x / y"
   4.479 -  apply (subst pos_less_divide_eq)
   4.480 -  apply assumption
   4.481 -  apply simp
   4.482 -done
   4.483 +lemma divide_pos_pos:
   4.484 +  "0 < (x::'a::ordered_field) ==> 0 < y ==> 0 < x / y"
   4.485 +by(simp add:field_simps)
   4.486 +
   4.487  
   4.488 -lemma divide_nonneg_pos: "0 <= (x::'a::ordered_field) ==> 0 < y ==> 
   4.489 -    0 <= x / y"
   4.490 -  apply (subst pos_le_divide_eq)
   4.491 -  apply assumption
   4.492 -  apply simp
   4.493 -done
   4.494 +lemma divide_nonneg_pos:
   4.495 +  "0 <= (x::'a::ordered_field) ==> 0 < y ==> 0 <= x / y"
   4.496 +by(simp add:field_simps)
   4.497  
   4.498 -lemma divide_neg_pos: "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0"
   4.499 -  apply (subst pos_divide_less_eq)
   4.500 -  apply assumption
   4.501 -  apply simp
   4.502 -done
   4.503 +lemma divide_neg_pos:
   4.504 +  "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0"
   4.505 +by(simp add:field_simps)
   4.506  
   4.507 -lemma divide_nonpos_pos: "(x::'a::ordered_field) <= 0 ==> 
   4.508 -    0 < y ==> x / y <= 0"
   4.509 -  apply (subst pos_divide_le_eq)
   4.510 -  apply assumption
   4.511 -  apply simp
   4.512 -done
   4.513 +lemma divide_nonpos_pos:
   4.514 +  "(x::'a::ordered_field) <= 0 ==> 0 < y ==> x / y <= 0"
   4.515 +by(simp add:field_simps)
   4.516  
   4.517 -lemma divide_pos_neg: "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0"
   4.518 -  apply (subst neg_divide_less_eq)
   4.519 -  apply assumption
   4.520 -  apply simp
   4.521 -done
   4.522 +lemma divide_pos_neg:
   4.523 +  "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0"
   4.524 +by(simp add:field_simps)
   4.525  
   4.526 -lemma divide_nonneg_neg: "0 <= (x::'a::ordered_field) ==> 
   4.527 -    y < 0 ==> x / y <= 0"
   4.528 -  apply (subst neg_divide_le_eq)
   4.529 -  apply assumption
   4.530 -  apply simp
   4.531 -done
   4.532 +lemma divide_nonneg_neg:
   4.533 +  "0 <= (x::'a::ordered_field) ==> y < 0 ==> x / y <= 0" 
   4.534 +by(simp add:field_simps)
   4.535  
   4.536 -lemma divide_neg_neg: "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y"
   4.537 -  apply (subst neg_less_divide_eq)
   4.538 -  apply assumption
   4.539 -  apply simp
   4.540 -done
   4.541 +lemma divide_neg_neg:
   4.542 +  "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y"
   4.543 +by(simp add:field_simps)
   4.544  
   4.545 -lemma divide_nonpos_neg: "(x::'a::ordered_field) <= 0 ==> y < 0 ==> 
   4.546 -    0 <= x / y"
   4.547 -  apply (subst neg_le_divide_eq)
   4.548 -  apply assumption
   4.549 -  apply simp
   4.550 -done
   4.551 +lemma divide_nonpos_neg:
   4.552 +  "(x::'a::ordered_field) <= 0 ==> y < 0 ==> 0 <= x / y"
   4.553 +by(simp add:field_simps)
   4.554  
   4.555  
   4.556  subsection{*Cancellation Laws for Division*}
   4.557  
   4.558  lemma divide_cancel_right [simp]:
   4.559       "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
   4.560 -apply (cases "c=0", simp) 
   4.561 -apply (simp add: divide_inverse field_mult_cancel_right) 
   4.562 +apply (cases "c=0", simp)
   4.563 +apply (simp add: divide_inverse field_mult_cancel_right)
   4.564  done
   4.565  
   4.566  lemma divide_cancel_left [simp]:
   4.567       "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
   4.568 -apply (cases "c=0", simp) 
   4.569 -apply (simp add: divide_inverse field_mult_cancel_left) 
   4.570 +apply (cases "c=0", simp)
   4.571 +apply (simp add: divide_inverse field_mult_cancel_left)
   4.572  done
   4.573  
   4.574  
   4.575 @@ -1589,25 +1624,25 @@
   4.576  text{*Simplify expressions equated with 1*}
   4.577  lemma divide_eq_1_iff [simp]:
   4.578       "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
   4.579 -apply (cases "b=0", simp) 
   4.580 -apply (simp add: right_inverse_eq) 
   4.581 +apply (cases "b=0", simp)
   4.582 +apply (simp add: right_inverse_eq)
   4.583  done
   4.584  
   4.585  lemma one_eq_divide_iff [simp]:
   4.586       "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
   4.587 -by (simp add: eq_commute [of 1])  
   4.588 +by (simp add: eq_commute [of 1])
   4.589  
   4.590  lemma zero_eq_1_divide_iff [simp]:
   4.591       "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)"
   4.592 -apply (cases "a=0", simp) 
   4.593 -apply (auto simp add: nonzero_eq_divide_eq) 
   4.594 +apply (cases "a=0", simp)
   4.595 +apply (auto simp add: nonzero_eq_divide_eq)
   4.596  done
   4.597  
   4.598  lemma one_divide_eq_0_iff [simp]:
   4.599       "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"
   4.600 -apply (cases "a=0", simp) 
   4.601 -apply (insert zero_neq_one [THEN not_sym]) 
   4.602 -apply (auto simp add: nonzero_divide_eq_eq) 
   4.603 +apply (cases "a=0", simp)
   4.604 +apply (insert zero_neq_one [THEN not_sym])
   4.605 +apply (auto simp add: nonzero_divide_eq_eq)
   4.606  done
   4.607  
   4.608  text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
   4.609 @@ -1627,40 +1662,33 @@
   4.610  lemma divide_strict_right_mono:
   4.611       "[|a < b; 0 < c|] ==> a / c < b / (c::'a::ordered_field)"
   4.612  by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono 
   4.613 -              positive_imp_inverse_positive) 
   4.614 +              positive_imp_inverse_positive)
   4.615  
   4.616  lemma divide_right_mono:
   4.617       "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{ordered_field,division_by_zero})"
   4.618 -  by (force simp add: divide_strict_right_mono order_le_less) 
   4.619 +by (force simp add: divide_strict_right_mono order_le_less)
   4.620  
   4.621  lemma divide_right_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b 
   4.622      ==> c <= 0 ==> b / c <= a / c"
   4.623 -  apply (drule divide_right_mono [of _ _ "- c"])
   4.624 -  apply auto
   4.625 +apply (drule divide_right_mono [of _ _ "- c"])
   4.626 +apply auto
   4.627  done
   4.628  
   4.629  lemma divide_strict_right_mono_neg:
   4.630       "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)"
   4.631 -apply (drule divide_strict_right_mono [of _ _ "-c"], simp) 
   4.632 -apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric]) 
   4.633 +apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
   4.634 +apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric])
   4.635  done
   4.636  
   4.637  text{*The last premise ensures that @{term a} and @{term b} 
   4.638        have the same sign*}
   4.639  lemma divide_strict_left_mono:
   4.640 -       "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
   4.641 -by (force simp add: zero_less_mult_iff divide_inverse mult_strict_left_mono 
   4.642 -      order_less_imp_not_eq order_less_imp_not_eq2  
   4.643 -      less_imp_inverse_less less_imp_inverse_less_neg) 
   4.644 +  "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
   4.645 +by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
   4.646  
   4.647  lemma divide_left_mono:
   4.648 -     "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::ordered_field)"
   4.649 -  apply (subgoal_tac "a \<noteq> 0 & b \<noteq> 0") 
   4.650 -   prefer 2 
   4.651 -   apply (force simp add: zero_less_mult_iff order_less_imp_not_eq) 
   4.652 -  apply (cases "c=0", simp add: divide_inverse)
   4.653 -  apply (force simp add: divide_strict_left_mono order_le_less) 
   4.654 -  done
   4.655 +  "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::ordered_field)"
   4.656 +by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
   4.657  
   4.658  lemma divide_left_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b 
   4.659      ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
   4.660 @@ -1669,13 +1697,9 @@
   4.661  done
   4.662  
   4.663  lemma divide_strict_left_mono_neg:
   4.664 -     "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
   4.665 -  apply (subgoal_tac "a \<noteq> 0 & b \<noteq> 0") 
   4.666 -   prefer 2 
   4.667 -   apply (force simp add: zero_less_mult_iff order_less_imp_not_eq) 
   4.668 -  apply (drule divide_strict_left_mono [of _ _ "-c"]) 
   4.669 -   apply (simp_all add: mult_commute nonzero_minus_divide_left [symmetric]) 
   4.670 -  done
   4.671 +  "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
   4.672 +by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
   4.673 +
   4.674  
   4.675  text{*Simplify quotients that are compared with the value 1.*}
   4.676  
   4.677 @@ -1768,16 +1792,16 @@
   4.678    by (subst pos_divide_le_eq, assumption+);
   4.679  
   4.680  lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>
   4.681 -    z <= x / y";
   4.682 -  by (subst pos_le_divide_eq, assumption+)
   4.683 +    z <= x / y"
   4.684 +by(simp add:field_simps)
   4.685  
   4.686  lemma mult_imp_div_pos_less: "0 < (y::'a::ordered_field) ==> x < z * y ==>
   4.687      x / y < z"
   4.688 -  by (subst pos_divide_less_eq, assumption+)
   4.689 +by(simp add:field_simps)
   4.690  
   4.691  lemma mult_imp_less_div_pos: "0 < (y::'a::ordered_field) ==> z * y < x ==>
   4.692      z < x / y"
   4.693 -  by (subst pos_less_divide_eq, assumption+)
   4.694 +by(simp add:field_simps)
   4.695  
   4.696  lemma frac_le: "(0::'a::ordered_field) <= x ==> 
   4.697      x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
   4.698 @@ -1809,8 +1833,6 @@
   4.699    apply simp_all
   4.700  done
   4.701  
   4.702 -lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
   4.703 -
   4.704  text{*It's not obvious whether these should be simprules or not. 
   4.705    Their effect is to gather terms into one big fraction, like
   4.706    a*b*c / x*y*z. The rationale for that is unclear, but many proofs 
   4.707 @@ -1824,18 +1846,18 @@
   4.708  lemma less_add_one: "a < (a+1::'a::ordered_semidom)"
   4.709  proof -
   4.710    have "a+0 < (a+1::'a::ordered_semidom)"
   4.711 -    by (blast intro: zero_less_one add_strict_left_mono) 
   4.712 +    by (blast intro: zero_less_one add_strict_left_mono)
   4.713    thus ?thesis by simp
   4.714  qed
   4.715  
   4.716  lemma zero_less_two: "0 < (1+1::'a::ordered_semidom)"
   4.717 -  by (blast intro: order_less_trans zero_less_one less_add_one) 
   4.718 +by (blast intro: order_less_trans zero_less_one less_add_one)
   4.719  
   4.720  lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"
   4.721 -by (simp add: zero_less_two pos_less_divide_eq ring_distribs) 
   4.722 +by (simp add: field_simps zero_less_two)
   4.723  
   4.724  lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"
   4.725 -by (simp add: zero_less_two pos_divide_less_eq ring_distribs) 
   4.726 +by (simp add: field_simps zero_less_two)
   4.727  
   4.728  lemma dense: "a < b ==> \<exists>r::'a::ordered_field. a < r & r < b"
   4.729  by (blast intro!: less_half_sum gt_half_sum)