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.48  by (simp add: diff_minus add_divide_distrib) 
    1.49  
    1.50 +lemma add_divide_eq_iff:
    1.51 +  "(z::'a::field) \<noteq> 0 \<Longrightarrow> x + y/z = (z*x + y)/z"
    1.52 +by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)
    1.53 +
    1.54 +lemma divide_add_eq_iff:
    1.55 +  "(z::'a::field) \<noteq> 0 \<Longrightarrow> x/z + y = (x + z*y)/z"
    1.56 +by(simp add:add_divide_distrib nonzero_mult_divide_cancel_left)
    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.60 +by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)
    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.64 +by(simp add:diff_divide_distrib nonzero_mult_divide_cancel_left)
    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.88 +by (simp add: nonzero_eq_divide_eq) 
    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.105 +  add_divide_eq_iff divide_add_eq_iff
   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.109 +(* is added later:
   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.117 + apply(simp add:field_eq_simps)
   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.126 -apply (subst add_frac_eq)
   1.127 -apply simp_all
   1.128 -done
   1.129 +by (simp add:field_eq_simps times_divide_eq)
   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.133 +by (simp add:field_eq_simps times_divide_eq)
   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.247      by (simp add: linorder_not_less)
   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.335 -	      add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
   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.340 +            add: order_less_imp_not_eq nonzero_inverse_minus_eq)
   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.412 -by (simp add: nonzero_eq_divide_eq) 
   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.464 +apply(simp add:field_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.475 +by (simp add: divide_inverse)
   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.485 +by(simp add:field_simps)
   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.496 +by(simp add:field_simps)
   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.505 +by(simp add:field_simps)
   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.515 +by(simp add:field_simps)
   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.524 +by(simp add:field_simps)
   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.534 +by(simp add:field_simps)
   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.543 +by(simp add:field_simps)
   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.553 +by(simp add:field_simps)
   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.580 -apply (simp add: right_inverse_eq) 
   1.581 +apply (cases "b=0", simp)
   1.582 +apply (simp add: right_inverse_eq)
   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.684 +by(simp add:field_simps)
   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.689 +by(simp add:field_simps)
   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.694 +by(simp add:field_simps)
   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)