tuned lemmas: more general class
authornipkow
Sun Apr 06 21:01:33 2014 +0200 (2014-04-06)
changeset 5644582ce19612fe8
parent 56442 681717041f55
child 56446 70a13de8a154
tuned lemmas: more general class
src/HOL/Fields.thy
src/HOL/Multivariate_Analysis/Derivative.thy
     1.1 --- a/src/HOL/Fields.thy	Sun Apr 06 17:19:08 2014 +0200
     1.2 +++ b/src/HOL/Fields.thy	Sun Apr 06 21:01:33 2014 +0200
     1.3 @@ -188,6 +188,22 @@
     1.4  lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
     1.5    by (drule sym) (simp add: divide_inverse mult_assoc)
     1.6  
     1.7 +lemma add_divide_eq_iff [field_simps]:
     1.8 +  "z \<noteq> 0 \<Longrightarrow> x + y / z = (x * z + y) / z"
     1.9 +  by (simp add: add_divide_distrib nonzero_eq_divide_eq)
    1.10 +
    1.11 +lemma divide_add_eq_iff [field_simps]:
    1.12 +  "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + y * z) / z"
    1.13 +  by (simp add: add_divide_distrib nonzero_eq_divide_eq)
    1.14 +
    1.15 +lemma diff_divide_eq_iff [field_simps]:
    1.16 +  "z \<noteq> 0 \<Longrightarrow> x - y / z = (x * z - y) / z"
    1.17 +  by (simp add: diff_divide_distrib nonzero_eq_divide_eq eq_diff_eq)
    1.18 +
    1.19 +lemma divide_diff_eq_iff [field_simps]:
    1.20 +  "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - y * z) / z"
    1.21 +  by (simp add: field_simps)
    1.22 +
    1.23  end
    1.24  
    1.25  class division_ring_inverse_zero = division_ring +
    1.26 @@ -323,22 +339,6 @@
    1.27    "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
    1.28  using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
    1.29  
    1.30 -lemma add_divide_eq_iff [field_simps]:
    1.31 -  "z \<noteq> 0 \<Longrightarrow> x + y / z = (z * x + y) / z"
    1.32 -  by (simp add: add_divide_distrib)
    1.33 -
    1.34 -lemma divide_add_eq_iff [field_simps]:
    1.35 -  "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + z * y) / z"
    1.36 -  by (simp add: add_divide_distrib)
    1.37 -
    1.38 -lemma diff_divide_eq_iff [field_simps]:
    1.39 -  "z \<noteq> 0 \<Longrightarrow> x - y / z = (z * x - y) / z"
    1.40 -  by (simp add: diff_divide_distrib)
    1.41 -
    1.42 -lemma divide_diff_eq_iff [field_simps]:
    1.43 -  "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - z * y) / z"
    1.44 -  by (simp add: diff_divide_distrib)
    1.45 -
    1.46  lemma diff_frac_eq:
    1.47    "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
    1.48    by (simp add: field_simps)
     2.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Apr 06 17:19:08 2014 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Apr 06 21:01:33 2014 +0200
     2.3 @@ -127,7 +127,7 @@
     2.4    "(f has_field_derivative D) (at a within s) \<longleftrightarrow> ((\<lambda>z. (f z - f a) / (z - a)) ---> D) (at a within s)"
     2.5  proof -
     2.6    have 1: "\<And>w y. ~(w = a) ==> y / (w - a) - D = (y - (w - a)*D)/(w - a)"
     2.7 -    by (metis divide_diff_eq_iff eq_iff_diff_eq_0)
     2.8 +    by (metis divide_diff_eq_iff eq_iff_diff_eq_0 mult_commute)
     2.9    show ?thesis
    2.10      apply (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right)
    2.11      apply (simp add: LIM_zero_iff [where l = D, symmetric])