author nipkow Sun, 06 Apr 2014 21:01:33 +0200 changeset 56445 82ce19612fe8 parent 56442 681717041f55 child 56446 70a13de8a154
tuned lemmas: more general class
 src/HOL/Fields.thy file | annotate | diff | comparison | revisions src/HOL/Multivariate_Analysis/Derivative.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Fields.thy	Sun Apr 06 17:19:08 2014 +0200
+++ b/src/HOL/Fields.thy	Sun Apr 06 21:01:33 2014 +0200
@@ -188,6 +188,22 @@
lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
by (drule sym) (simp add: divide_inverse mult_assoc)

+  "z \<noteq> 0 \<Longrightarrow> x + y / z = (x * z + y) / z"
+
+  "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + y * z) / z"
+
+lemma diff_divide_eq_iff [field_simps]:
+  "z \<noteq> 0 \<Longrightarrow> x - y / z = (x * z - y) / z"
+  by (simp add: diff_divide_distrib nonzero_eq_divide_eq eq_diff_eq)
+
+lemma divide_diff_eq_iff [field_simps]:
+  "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - y * z) / z"
+
end

class division_ring_inverse_zero = division_ring +
@@ -323,22 +339,6 @@
"\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)

-  "z \<noteq> 0 \<Longrightarrow> x + y / z = (z * x + y) / z"
-
-  "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + z * y) / z"
-
-lemma diff_divide_eq_iff [field_simps]:
-  "z \<noteq> 0 \<Longrightarrow> x - y / z = (z * x - y) / z"
-
-lemma divide_diff_eq_iff [field_simps]:
-  "z \<noteq> 0 \<Longrightarrow> x / z - y = (x - z * y) / z"
-
lemma diff_frac_eq:
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
```--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Apr 06 17:19:08 2014 +0200