src/HOL/Fields.thy
 changeset 56445 82ce19612fe8 parent 56441 49e95c9ebb59 child 56479 91958d4b30f7
```     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.8 +  "z \<noteq> 0 \<Longrightarrow> x + y / z = (x * z + y) / z"
1.10 +
1.12 +  "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + y * z) / z"
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.31 -  "z \<noteq> 0 \<Longrightarrow> x + y / z = (z * x + y) / z"
1.33 -
1.35 -  "z \<noteq> 0 \<Longrightarrow> x / z + y = (x + z * y) / z"