src/HOL/Ring_and_Field.thy
 changeset 23482 2f4be6844f7c parent 23477 f4b83f03cac9 child 23483 a9356b40fbd3
```     1.1 --- a/src/HOL/Ring_and_Field.thy	Sun Jun 24 20:47:05 2007 +0200
1.2 +++ b/src/HOL/Ring_and_Field.thy	Sun Jun 24 20:55:41 2007 +0200
1.3 @@ -773,12 +773,13 @@
1.4  lemma add_divide_distrib: "(a+b)/(c::'a::field) = a/c + b/c"
1.5  by (simp add: divide_inverse ring_distribs)
1.6
1.7 -
1.8 +(* what ordering?? this is a straight instance of mult_eq_0_iff
1.9  text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
1.10        of an ordering.*}
1.11  lemma field_mult_eq_0_iff [simp]:
1.12    "(a*b = (0::'a::division_ring)) = (a = 0 | b = 0)"
1.13  by simp
1.14 +*)
1.15
1.16  text{*Cancellation of equalities with a common factor*}
1.17  lemma field_mult_cancel_right_lemma:
1.18 @@ -915,7 +916,7 @@
1.19        shows "inverse(a*b) = inverse(b) * inverse(a::'a::division_ring)"
1.20    proof -
1.21    have "inverse(a*b) * (a * b) * inverse(b) = inverse(b)"
1.22 -    by (simp add: field_mult_eq_0_iff anz bnz)
1.23 +    by (simp add: anz bnz)
1.24    hence "inverse(a*b) * a = inverse(b)"
1.25      by (simp add: mult_assoc bnz)
1.26    hence "inverse(a*b) * a * inverse(a) = inverse(b) * inverse(a)"
1.27 @@ -969,8 +970,7 @@
1.28  assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/(b::'a::field)"
1.29  proof -
1.30    have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
1.31 -    by (simp add: field_mult_eq_0_iff divide_inverse
1.32 -                  nonzero_inverse_mult_distrib)
1.33 +    by (simp add: divide_inverse nonzero_inverse_mult_distrib)
1.34    also have "... =  a * inverse b * (inverse c * c)"
1.35      by (simp only: mult_ac)
1.36    also have "... =  a * inverse b"
1.37 @@ -1004,6 +1004,8 @@
1.38  lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
1.39  by (simp add: divide_inverse mult_ac)
1.40
1.41 +lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
1.42 +
1.43  lemma divide_divide_eq_right [simp]:
1.44    "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
1.45  by (simp add: divide_inverse mult_ac)
1.46 @@ -1098,53 +1100,120 @@
1.47  lemma diff_divide_distrib: "(a-b)/(c::'a::field) = a/c - b/c"
1.49
1.51 +  "(z::'a::field) \<noteq> 0 \<Longrightarrow> x + y/z = (z*x + y)/z"
1.53 +
1.55 +  "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z + y = (x + z*y)/z"
1.57 +
1.58 +lemma diff_divide_eq_iff:
1.59 +  "(z::'a::field) \<noteq> 0 \<Longrightarrow> x - y/z = (z*x - y)/z"
1.61 +
1.62 +lemma divide_diff_eq_iff:
1.63 +  "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z - y = (x - z*y)/z"
1.65 +
1.66 +lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"
1.67 +proof -
1.68 +  assume [simp]: "c\<noteq>0"
1.69 +  have "(a = b/c) = (a*c = (b/c)*c)"
1.70 +    by (simp add: field_mult_cancel_right)
1.71 +  also have "... = (a*c = b)"
1.72 +    by (simp add: divide_inverse mult_assoc)
1.73 +  finally show ?thesis .
1.74 +qed
1.75 +
1.76 +lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"
1.77 +proof -
1.78 +  assume [simp]: "c\<noteq>0"
1.79 +  have "(b/c = a) = ((b/c)*c = a*c)"
1.80 +    by (simp add: field_mult_cancel_right)
1.81 +  also have "... = (b = a*c)"
1.82 +    by (simp add: divide_inverse mult_assoc)
1.83 +  finally show ?thesis .
1.84 +qed
1.85 +
1.86 +lemma eq_divide_eq:
1.87 +  "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
1.89 +
1.90 +lemma divide_eq_eq:
1.91 +  "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
1.92 +by (force simp add: nonzero_divide_eq_eq)
1.93 +
1.94 +lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
1.95 +    b = a * c ==> b / c = a"
1.96 +  by (subst divide_eq_eq, simp)
1.97 +
1.98 +lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
1.99 +    a * c = b ==> a = b / c"
1.100 +  by (subst eq_divide_eq, simp)
1.101 +
1.102 +
1.103 +lemmas field_eq_simps = ring_simps
1.104 +  (* pull / out*)
1.106 +  diff_divide_eq_iff divide_diff_eq_iff
1.107 +  (* multiply eqn *)
1.108 +  nonzero_eq_divide_eq nonzero_divide_eq_eq
1.110 +  times_divide_eq_left times_divide_eq_right
1.111 +*)
1.112 +
1.113 +text{*An example:*}
1.114 +lemma fixes a b c d e f :: "'a::field"
1.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"
1.116 +apply(subgoal_tac "(c-d)*(e-f)*(a-b) \<noteq> 0")
1.118 +apply(simp)
1.119 +done
1.120 +
1.121 +
1.122  lemma diff_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
1.123      x / y - w / z = (x * z - w * y) / (y * z)"
1.124 -apply (subst diff_def)+
1.125 -apply (subst minus_divide_left)
1.127 -apply simp_all
1.128 -done
1.130 +
1.131 +lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
1.132 +    (x / y = w / z) = (x * z = w * y)"
1.134
1.135
1.136  subsection {* Ordered Fields *}
1.137
1.138  lemma positive_imp_inverse_positive:
1.139 -      assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::ordered_field)"
1.140 -  proof -
1.141 +assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::ordered_field)"
1.142 +proof -
1.143    have "0 < a * inverse a"
1.144      by (simp add: a_gt_0 [THEN order_less_imp_not_eq2] zero_less_one)
1.145    thus "0 < inverse a"
1.146      by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
1.147 -  qed
1.148 +qed
1.149
1.150  lemma negative_imp_inverse_negative:
1.151 -     "a < 0 ==> inverse a < (0::'a::ordered_field)"
1.152 -  by (insert positive_imp_inverse_positive [of "-a"],
1.153 -      simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)
1.154 +  "a < 0 ==> inverse a < (0::'a::ordered_field)"
1.155 +by (insert positive_imp_inverse_positive [of "-a"],
1.156 +    simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)
1.157
1.158  lemma inverse_le_imp_le:
1.159 -      assumes invle: "inverse a \<le> inverse b"
1.160 -	  and apos:  "0 < a"
1.161 -	 shows "b \<le> (a::'a::ordered_field)"
1.162 -  proof (rule classical)
1.163 +assumes invle: "inverse a \<le> inverse b" and apos:  "0 < a"
1.164 +shows "b \<le> (a::'a::ordered_field)"
1.165 +proof (rule classical)
1.166    assume "~ b \<le> a"
1.167 -  hence "a < b"
1.168 -    by (simp add: linorder_not_le)
1.169 -  hence bpos: "0 < b"
1.170 -    by (blast intro: apos order_less_trans)
1.171 +  hence "a < b"  by (simp add: linorder_not_le)
1.172 +  hence bpos: "0 < b"  by (blast intro: apos order_less_trans)
1.173    hence "a * inverse a \<le> a * inverse b"
1.174      by (simp add: apos invle order_less_imp_le mult_left_mono)
1.175    hence "(a * inverse a) * b \<le> (a * inverse b) * b"
1.176      by (simp add: bpos order_less_imp_le mult_right_mono)
1.177 -  thus "b \<le> a"
1.178 -    by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
1.179 -  qed
1.180 +  thus "b \<le> a"  by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
1.181 +qed
1.182
1.183  lemma inverse_positive_imp_positive:
1.184 -  assumes inv_gt_0: "0 < inverse a"
1.185 -    and nz: "a \<noteq> 0"
1.186 -  shows "0 < (a::'a::ordered_field)"
1.187 +assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
1.188 +shows "0 < (a::'a::ordered_field)"
1.189  proof -
1.190    have "0 < inverse (inverse a)"
1.191      using inv_gt_0 by (rule positive_imp_inverse_positive)
1.192 @@ -1153,34 +1222,32 @@
1.193  qed
1.194
1.195  lemma inverse_positive_iff_positive [simp]:
1.196 -      "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
1.197 +  "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
1.198  apply (cases "a = 0", simp)
1.199  apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
1.200  done
1.201
1.202  lemma inverse_negative_imp_negative:
1.203 -  assumes inv_less_0: "inverse a < 0"
1.204 -    and nz:  "a \<noteq> 0"
1.205 -  shows "a < (0::'a::ordered_field)"
1.206 +assumes inv_less_0: "inverse a < 0" and nz:  "a \<noteq> 0"
1.207 +shows "a < (0::'a::ordered_field)"
1.208  proof -
1.209    have "inverse (inverse a) < 0"
1.210      using inv_less_0 by (rule negative_imp_inverse_negative)
1.211 -  thus "a < 0"
1.212 -    using nz by (simp add: nonzero_inverse_inverse_eq)
1.213 +  thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
1.214  qed
1.215
1.216  lemma inverse_negative_iff_negative [simp]:
1.217 -      "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
1.218 +  "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
1.219  apply (cases "a = 0", simp)
1.220  apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
1.221  done
1.222
1.223  lemma inverse_nonnegative_iff_nonnegative [simp]:
1.224 -      "(0 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"
1.225 +  "(0 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"
1.226  by (simp add: linorder_not_less [symmetric])
1.227
1.228  lemma inverse_nonpositive_iff_nonpositive [simp]:
1.229 -      "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"
1.230 +  "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"
1.231  by (simp add: linorder_not_less [symmetric])
1.232
1.233  lemma ordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::ordered_field)"
1.234 @@ -1204,10 +1271,9 @@
1.235  subsection{*Anti-Monotonicity of @{term inverse}*}
1.236
1.237  lemma less_imp_inverse_less:
1.238 -      assumes less: "a < b"
1.239 -	  and apos:  "0 < a"
1.240 -	shows "inverse b < inverse (a::'a::ordered_field)"
1.241 -  proof (rule ccontr)
1.242 +assumes less: "a < b" and apos:  "0 < a"
1.243 +shows "inverse b < inverse (a::'a::ordered_field)"
1.244 +proof (rule ccontr)
1.245    assume "~ inverse b < inverse a"
1.246    hence "inverse a \<le> inverse b"
1.248 @@ -1215,81 +1281,78 @@
1.249      by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])
1.250    thus False
1.251      by (rule notE [OF _ less])
1.252 -  qed
1.253 +qed
1.254
1.255  lemma inverse_less_imp_less:
1.256 -   "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"
1.257 +  "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::ordered_field)"
1.258  apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])
1.259  apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)
1.260  done
1.261
1.262  text{*Both premises are essential. Consider -1 and 1.*}
1.263  lemma inverse_less_iff_less [simp]:
1.264 -     "[|0 < a; 0 < b|]
1.265 -      ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
1.266 +  "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
1.267  by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)
1.268
1.269  lemma le_imp_inverse_le:
1.270 -   "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
1.271 -  by (force simp add: order_le_less less_imp_inverse_less)
1.272 +  "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
1.273 +by (force simp add: order_le_less less_imp_inverse_less)
1.274
1.275  lemma inverse_le_iff_le [simp]:
1.276 -     "[|0 < a; 0 < b|]
1.277 -      ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
1.278 + "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
1.279  by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)
1.280
1.281
1.282  text{*These results refer to both operands being negative.  The opposite-sign
1.283  case is trivial, since inverse preserves signs.*}
1.284  lemma inverse_le_imp_le_neg:
1.285 -   "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"
1.286 -  apply (rule classical)
1.287 -  apply (subgoal_tac "a < 0")
1.288 -   prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans)
1.289 -  apply (insert inverse_le_imp_le [of "-b" "-a"])
1.290 -  apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
1.291 -  done
1.292 +  "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::ordered_field)"
1.293 +apply (rule classical)
1.294 +apply (subgoal_tac "a < 0")
1.295 + prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans)
1.296 +apply (insert inverse_le_imp_le [of "-b" "-a"])
1.297 +apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
1.298 +done
1.299
1.300  lemma less_imp_inverse_less_neg:
1.301     "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::ordered_field)"
1.302 -  apply (subgoal_tac "a < 0")
1.303 -   prefer 2 apply (blast intro: order_less_trans)
1.304 -  apply (insert less_imp_inverse_less [of "-b" "-a"])
1.305 -  apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
1.306 -  done
1.307 +apply (subgoal_tac "a < 0")
1.308 + prefer 2 apply (blast intro: order_less_trans)
1.309 +apply (insert less_imp_inverse_less [of "-b" "-a"])
1.310 +apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
1.311 +done
1.312
1.313  lemma inverse_less_imp_less_neg:
1.314     "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::ordered_field)"
1.315 -  apply (rule classical)
1.316 -  apply (subgoal_tac "a < 0")
1.317 -   prefer 2
1.318 -   apply (force simp add: linorder_not_less intro: order_le_less_trans)
1.319 -  apply (insert inverse_less_imp_less [of "-b" "-a"])
1.320 -  apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
1.321 -  done
1.322 +apply (rule classical)
1.323 +apply (subgoal_tac "a < 0")
1.324 + prefer 2
1.325 + apply (force simp add: linorder_not_less intro: order_le_less_trans)
1.326 +apply (insert inverse_less_imp_less [of "-b" "-a"])
1.327 +apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
1.328 +done
1.329
1.330  lemma inverse_less_iff_less_neg [simp]:
1.331 -     "[|a < 0; b < 0|]
1.332 -      ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
1.333 -  apply (insert inverse_less_iff_less [of "-b" "-a"])
1.334 -  apply (simp del: inverse_less_iff_less
1.336 -  done
1.337 +  "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
1.338 +apply (insert inverse_less_iff_less [of "-b" "-a"])
1.339 +apply (simp del: inverse_less_iff_less
1.341 +done
1.342
1.343  lemma le_imp_inverse_le_neg:
1.344 -   "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
1.345 -  by (force simp add: order_le_less less_imp_inverse_less_neg)
1.346 +  "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
1.347 +by (force simp add: order_le_less less_imp_inverse_less_neg)
1.348
1.349  lemma inverse_le_iff_le_neg [simp]:
1.350 -     "[|a < 0; b < 0|]
1.351 -      ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
1.352 + "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
1.353  by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)
1.354
1.355
1.356  subsection{*Inverses and the Number One*}
1.357
1.358  lemma one_less_inverse_iff:
1.359 -    "(1 < inverse x) = (0 < x & x < (1::'a::{ordered_field,division_by_zero}))"proof cases
1.360 +  "(1 < inverse x) = (0 < x & x < (1::'a::{ordered_field,division_by_zero}))"
1.361 +proof cases
1.362    assume "0 < x"
1.363      with inverse_less_iff_less [OF zero_less_one, of x]
1.364      show ?thesis by simp
1.365 @@ -1306,20 +1369,20 @@
1.366  qed
1.367
1.368  lemma inverse_eq_1_iff [simp]:
1.369 -    "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
1.370 +  "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
1.371  by (insert inverse_eq_iff_eq [of x 1], simp)
1.372
1.373  lemma one_le_inverse_iff:
1.374 -   "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{ordered_field,division_by_zero}))"
1.375 +  "(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{ordered_field,division_by_zero}))"
1.376  by (force simp add: order_le_less one_less_inverse_iff zero_less_one
1.377                      eq_commute [of 1])
1.378
1.379  lemma inverse_less_1_iff:
1.380 -   "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{ordered_field,division_by_zero}))"
1.381 +  "(inverse x < 1) = (x \<le> 0 | 1 < (x::'a::{ordered_field,division_by_zero}))"
1.382  by (simp add: linorder_not_le [symmetric] one_le_inverse_iff)
1.383
1.384  lemma inverse_le_1_iff:
1.385 -   "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
1.386 +  "(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{ordered_field,division_by_zero}))"
1.387  by (simp add: linorder_not_less [symmetric] one_less_inverse_iff)
1.388
1.389
1.390 @@ -1445,49 +1508,41 @@
1.391  apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)
1.392  done
1.393
1.394 -lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"
1.395 -proof -
1.396 -  assume [simp]: "c\<noteq>0"
1.397 -  have "(a = b/c) = (a*c = (b/c)*c)"
1.398 -    by (simp add: field_mult_cancel_right)
1.399 -  also have "... = (a*c = b)"
1.400 -    by (simp add: divide_inverse mult_assoc)
1.401 -  finally show ?thesis .
1.402 -qed
1.403 +
1.404 +subsection{*Field simplification*}
1.405 +
1.406 +text{* Lemmas @{text field_simps} multiply with denominators in
1.407 +in(equations) if they can be proved to be non-zero (for equations) or
1.408 +positive/negative (for inequations). *}
1.409
1.410 -lemma eq_divide_eq:
1.411 -  "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
1.413 +lemmas field_simps = field_eq_simps
1.414 +  (* multiply ineqn *)
1.415 +  pos_divide_less_eq neg_divide_less_eq
1.416 +  pos_less_divide_eq neg_less_divide_eq
1.417 +  pos_divide_le_eq neg_divide_le_eq
1.418 +  pos_le_divide_eq neg_le_divide_eq
1.419
1.420 -lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"
1.421 -proof -
1.422 -  assume [simp]: "c\<noteq>0"
1.423 -  have "(b/c = a) = ((b/c)*c = a*c)"
1.424 -    by (simp add: field_mult_cancel_right)
1.425 -  also have "... = (b = a*c)"
1.426 -    by (simp add: divide_inverse mult_assoc)
1.427 -  finally show ?thesis .
1.428 -qed
1.429 +text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
1.430 +of positivity/negativity needed for field_simps. Have not added @{text
1.431 +sign_simps} to @{text field_simps} because the former can lead to case
1.432 +explosions. *}
1.433
1.434 -lemma divide_eq_eq:
1.435 -  "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
1.436 -by (force simp add: nonzero_divide_eq_eq)
1.437 +lemmas sign_simps = group_simps
1.438 +  zero_less_mult_iff  mult_less_0_iff
1.439
1.440 -lemma divide_eq_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
1.441 -    b = a * c ==> b / c = a"
1.442 -  by (subst divide_eq_eq, simp)
1.443 -
1.444 -lemma eq_divide_imp: "(c::'a::{division_by_zero,field}) ~= 0 ==>
1.445 -    a * c = b ==> a = b / c"
1.446 -  by (subst eq_divide_eq, simp)
1.447 -
1.448 -lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
1.449 -    (x / y = w / z) = (x * z = w * y)"
1.450 -  apply (subst nonzero_eq_divide_eq)
1.451 -  apply assumption
1.452 -  apply (subst times_divide_eq_left)
1.453 -  apply (erule nonzero_divide_eq_eq)
1.454 +(* Only works once linear arithmetic is installed:
1.455 +text{*An example:*}
1.456 +lemma fixes a b c d e f :: "'a::ordered_field"
1.457 +shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
1.458 + ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
1.459 + ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
1.460 +apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
1.461 + prefer 2 apply(simp add:sign_simps)
1.462 +apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
1.463 + prefer 2 apply(simp add:sign_simps)
1.465  done
1.466 +*)
1.467
1.468
1.469  subsection{*Division and Signs*}
1.470 @@ -1513,74 +1568,54 @@
1.471
1.472  lemma divide_eq_0_iff [simp]:
1.473       "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
1.474 -by (simp add: divide_inverse field_mult_eq_0_iff)
1.476
1.477 -lemma divide_pos_pos: "0 < (x::'a::ordered_field) ==>
1.478 -    0 < y ==> 0 < x / y"
1.479 -  apply (subst pos_less_divide_eq)
1.480 -  apply assumption
1.481 -  apply simp
1.482 -done
1.483 +lemma divide_pos_pos:
1.484 +  "0 < (x::'a::ordered_field) ==> 0 < y ==> 0 < x / y"
1.486 +
1.487
1.488 -lemma divide_nonneg_pos: "0 <= (x::'a::ordered_field) ==> 0 < y ==>
1.489 -    0 <= x / y"
1.490 -  apply (subst pos_le_divide_eq)
1.491 -  apply assumption
1.492 -  apply simp
1.493 -done
1.494 +lemma divide_nonneg_pos:
1.495 +  "0 <= (x::'a::ordered_field) ==> 0 < y ==> 0 <= x / y"
1.497
1.498 -lemma divide_neg_pos: "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0"
1.499 -  apply (subst pos_divide_less_eq)
1.500 -  apply assumption
1.501 -  apply simp
1.502 -done
1.503 +lemma divide_neg_pos:
1.504 +  "(x::'a::ordered_field) < 0 ==> 0 < y ==> x / y < 0"
1.506
1.507 -lemma divide_nonpos_pos: "(x::'a::ordered_field) <= 0 ==>
1.508 -    0 < y ==> x / y <= 0"
1.509 -  apply (subst pos_divide_le_eq)
1.510 -  apply assumption
1.511 -  apply simp
1.512 -done
1.513 +lemma divide_nonpos_pos:
1.514 +  "(x::'a::ordered_field) <= 0 ==> 0 < y ==> x / y <= 0"
1.516
1.517 -lemma divide_pos_neg: "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0"
1.518 -  apply (subst neg_divide_less_eq)
1.519 -  apply assumption
1.520 -  apply simp
1.521 -done
1.522 +lemma divide_pos_neg:
1.523 +  "0 < (x::'a::ordered_field) ==> y < 0 ==> x / y < 0"
1.525
1.526 -lemma divide_nonneg_neg: "0 <= (x::'a::ordered_field) ==>
1.527 -    y < 0 ==> x / y <= 0"
1.528 -  apply (subst neg_divide_le_eq)
1.529 -  apply assumption
1.530 -  apply simp
1.531 -done
1.532 +lemma divide_nonneg_neg:
1.533 +  "0 <= (x::'a::ordered_field) ==> y < 0 ==> x / y <= 0"
1.535
1.536 -lemma divide_neg_neg: "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y"
1.537 -  apply (subst neg_less_divide_eq)
1.538 -  apply assumption
1.539 -  apply simp
1.540 -done
1.541 +lemma divide_neg_neg:
1.542 +  "(x::'a::ordered_field) < 0 ==> y < 0 ==> 0 < x / y"
1.544
1.545 -lemma divide_nonpos_neg: "(x::'a::ordered_field) <= 0 ==> y < 0 ==>
1.546 -    0 <= x / y"
1.547 -  apply (subst neg_le_divide_eq)
1.548 -  apply assumption
1.549 -  apply simp
1.550 -done
1.551 +lemma divide_nonpos_neg:
1.552 +  "(x::'a::ordered_field) <= 0 ==> y < 0 ==> 0 <= x / y"
1.554
1.555
1.556  subsection{*Cancellation Laws for Division*}
1.557
1.558  lemma divide_cancel_right [simp]:
1.559       "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
1.560 -apply (cases "c=0", simp)
1.561 -apply (simp add: divide_inverse field_mult_cancel_right)
1.562 +apply (cases "c=0", simp)
1.563 +apply (simp add: divide_inverse field_mult_cancel_right)
1.564  done
1.565
1.566  lemma divide_cancel_left [simp]:
1.567       "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
1.568 -apply (cases "c=0", simp)
1.569 -apply (simp add: divide_inverse field_mult_cancel_left)
1.570 +apply (cases "c=0", simp)
1.571 +apply (simp add: divide_inverse field_mult_cancel_left)
1.572  done
1.573
1.574
1.575 @@ -1589,25 +1624,25 @@
1.576  text{*Simplify expressions equated with 1*}
1.577  lemma divide_eq_1_iff [simp]:
1.578       "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
1.579 -apply (cases "b=0", simp)
1.581 +apply (cases "b=0", simp)
1.583  done
1.584
1.585  lemma one_eq_divide_iff [simp]:
1.586       "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
1.587 -by (simp add: eq_commute [of 1])
1.588 +by (simp add: eq_commute [of 1])
1.589
1.590  lemma zero_eq_1_divide_iff [simp]:
1.591       "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)"
1.592 -apply (cases "a=0", simp)
1.593 -apply (auto simp add: nonzero_eq_divide_eq)
1.594 +apply (cases "a=0", simp)
1.595 +apply (auto simp add: nonzero_eq_divide_eq)
1.596  done
1.597
1.598  lemma one_divide_eq_0_iff [simp]:
1.599       "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"
1.600 -apply (cases "a=0", simp)
1.601 -apply (insert zero_neq_one [THEN not_sym])
1.602 -apply (auto simp add: nonzero_divide_eq_eq)
1.603 +apply (cases "a=0", simp)
1.604 +apply (insert zero_neq_one [THEN not_sym])
1.605 +apply (auto simp add: nonzero_divide_eq_eq)
1.606  done
1.607
1.608  text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
1.609 @@ -1627,40 +1662,33 @@
1.610  lemma divide_strict_right_mono:
1.611       "[|a < b; 0 < c|] ==> a / c < b / (c::'a::ordered_field)"
1.612  by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono
1.613 -              positive_imp_inverse_positive)
1.614 +              positive_imp_inverse_positive)
1.615
1.616  lemma divide_right_mono:
1.617       "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{ordered_field,division_by_zero})"
1.618 -  by (force simp add: divide_strict_right_mono order_le_less)
1.619 +by (force simp add: divide_strict_right_mono order_le_less)
1.620
1.621  lemma divide_right_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b
1.622      ==> c <= 0 ==> b / c <= a / c"
1.623 -  apply (drule divide_right_mono [of _ _ "- c"])
1.624 -  apply auto
1.625 +apply (drule divide_right_mono [of _ _ "- c"])
1.626 +apply auto
1.627  done
1.628
1.629  lemma divide_strict_right_mono_neg:
1.630       "[|b < a; c < 0|] ==> a / c < b / (c::'a::ordered_field)"
1.631 -apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
1.632 -apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric])
1.633 +apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
1.634 +apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric])
1.635  done
1.636
1.637  text{*The last premise ensures that @{term a} and @{term b}
1.638        have the same sign*}
1.639  lemma divide_strict_left_mono:
1.640 -       "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
1.641 -by (force simp add: zero_less_mult_iff divide_inverse mult_strict_left_mono
1.642 -      order_less_imp_not_eq order_less_imp_not_eq2
1.643 -      less_imp_inverse_less less_imp_inverse_less_neg)
1.644 +  "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
1.645 +by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
1.646
1.647  lemma divide_left_mono:
1.648 -     "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::ordered_field)"
1.649 -  apply (subgoal_tac "a \<noteq> 0 & b \<noteq> 0")
1.650 -   prefer 2
1.651 -   apply (force simp add: zero_less_mult_iff order_less_imp_not_eq)
1.652 -  apply (cases "c=0", simp add: divide_inverse)
1.653 -  apply (force simp add: divide_strict_left_mono order_le_less)
1.654 -  done
1.655 +  "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::ordered_field)"
1.656 +by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
1.657
1.658  lemma divide_left_mono_neg: "(a::'a::{division_by_zero,ordered_field}) <= b
1.659      ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
1.660 @@ -1669,13 +1697,9 @@
1.661  done
1.662
1.663  lemma divide_strict_left_mono_neg:
1.664 -     "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
1.665 -  apply (subgoal_tac "a \<noteq> 0 & b \<noteq> 0")
1.666 -   prefer 2
1.667 -   apply (force simp add: zero_less_mult_iff order_less_imp_not_eq)
1.668 -  apply (drule divide_strict_left_mono [of _ _ "-c"])
1.669 -   apply (simp_all add: mult_commute nonzero_minus_divide_left [symmetric])
1.670 -  done
1.671 +  "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::ordered_field)"
1.672 +by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
1.673 +
1.674
1.675  text{*Simplify quotients that are compared with the value 1.*}
1.676
1.677 @@ -1768,16 +1792,16 @@
1.678    by (subst pos_divide_le_eq, assumption+);
1.679
1.680  lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>
1.681 -    z <= x / y";
1.682 -  by (subst pos_le_divide_eq, assumption+)
1.683 +    z <= x / y"
1.685
1.686  lemma mult_imp_div_pos_less: "0 < (y::'a::ordered_field) ==> x < z * y ==>
1.687      x / y < z"
1.688 -  by (subst pos_divide_less_eq, assumption+)
1.690
1.691  lemma mult_imp_less_div_pos: "0 < (y::'a::ordered_field) ==> z * y < x ==>
1.692      z < x / y"
1.693 -  by (subst pos_less_divide_eq, assumption+)
1.695
1.696  lemma frac_le: "(0::'a::ordered_field) <= x ==>
1.697      x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
1.698 @@ -1809,8 +1833,6 @@
1.699    apply simp_all
1.700  done
1.701
1.702 -lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
1.703 -
1.704  text{*It's not obvious whether these should be simprules or not.
1.705    Their effect is to gather terms into one big fraction, like
1.706    a*b*c / x*y*z. The rationale for that is unclear, but many proofs
1.707 @@ -1824,18 +1846,18 @@
1.708  lemma less_add_one: "a < (a+1::'a::ordered_semidom)"
1.709  proof -
1.710    have "a+0 < (a+1::'a::ordered_semidom)"
1.711 -    by (blast intro: zero_less_one add_strict_left_mono)
1.712 +    by (blast intro: zero_less_one add_strict_left_mono)
1.713    thus ?thesis by simp
1.714  qed
1.715
1.716  lemma zero_less_two: "0 < (1+1::'a::ordered_semidom)"
1.717 -  by (blast intro: order_less_trans zero_less_one less_add_one)
1.718 +by (blast intro: order_less_trans zero_less_one less_add_one)
1.719
1.720  lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::ordered_field)"
1.721 -by (simp add: zero_less_two pos_less_divide_eq ring_distribs)
1.722 +by (simp add: field_simps zero_less_two)
1.723
1.724  lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"
1.725 -by (simp add: zero_less_two pos_divide_less_eq ring_distribs)
1.726 +by (simp add: field_simps zero_less_two)
1.727
1.728  lemma dense: "a < b ==> \<exists>r::'a::ordered_field. a < r & r < b"
1.729  by (blast intro!: less_half_sum gt_half_sum)
```