--- a/src/HOL/Library/Ring_and_Field.thy Tue Nov 18 11:01:52 2003 +0100
+++ b/src/HOL/Library/Ring_and_Field.thy Tue Nov 18 11:03:33 2003 +0100
@@ -79,6 +79,22 @@
lemma diff_self [simp]: "a - (a::'a::ring) = 0"
by (simp add: diff_minus)
+lemma add_left_cancel [simp]:
+ "(a + b = a + c) = (b = (c::'a::ring))"
+proof
+ assume eq: "a + b = a + c"
+ then have "(-a + a) + b = (-a + a) + c"
+ by (simp only: eq add_assoc)
+ then show "b = c" by (simp add: )
+next
+ assume eq: "b = c"
+ then show "a + b = a + c" by simp
+qed
+
+lemma add_right_cancel [simp]:
+ "(b + a = c + a) = (b = (c::'a::ring))"
+ by (simp add: add_commute)
+
subsubsection {* Derived rules for multiplication *}
@@ -118,6 +134,18 @@
lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
by (simp add: divide_inverse)
+lemma mult_left_zero [simp]:
+ "0 * a = (0::'a::ring)"
+proof -
+ have "0*a + 0*a = 0*a + 0"
+ by (simp add: left_distrib [symmetric])
+ then show ?thesis by (simp only: add_left_cancel)
+qed
+
+lemma mult_right_zero [simp]:
+ "a * 0 = (0::'a::ring)"
+ by (simp add: mult_commute)
+
subsubsection {* Distribution rules *}