src/HOL/Groups.thy
 changeset 45548 3e2722d66169 parent 45294 3c5d3d286055 child 48556 62a3fbf9d35b
```     1.1 --- a/src/HOL/Groups.thy	Thu Nov 17 15:07:46 2011 +0100
1.2 +++ b/src/HOL/Groups.thy	Thu Nov 17 18:31:00 2011 +0100
1.3 @@ -284,7 +284,6 @@
1.4    finally show ?thesis .
1.5  qed
1.6
1.7 -
1.8  lemmas equals_zero_I = minus_unique (* legacy name *)
1.9
1.10  lemma minus_zero [simp]: "- 0 = 0"
1.11 @@ -413,6 +412,28 @@
1.13    by (rule equation_minus_iff)
1.14
1.15 +lemma minus_diff_eq [simp]: "- (a - b) = b - a"
1.17 +
1.18 +lemma add_diff_eq[algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
1.20 +
1.21 +lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
1.23 +
1.24 +lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
1.26 +
1.27 +lemma diff_diff_eq2[algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"
1.29 +
1.30 +lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
1.31 +  by (fact right_minus_eq [symmetric])
1.32 +
1.33 +lemma diff_eq_diff_eq:
1.34 +  "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
1.35 +  by (simp add: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])
1.36 +
1.37  end
1.38
1.40 @@ -440,40 +461,17 @@
1.41    "- (a + b) = - a + - b"
1.43
1.44 -lemma minus_diff_eq [simp]:
1.45 -  "- (a - b) = b - a"
1.47 -
1.48 -lemma add_diff_eq[algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
1.50 -
1.51  lemma diff_add_eq[algebra_simps, field_simps]: "(a - b) + c = (a + c) - b"
1.53
1.54 -lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
1.56 -
1.57 -lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
1.59 -
1.60  lemma diff_diff_eq[algebra_simps, field_simps]: "(a - b) - c = a - (b + c)"
1.62
1.63 -lemma diff_diff_eq2[algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"
1.65 -
1.66 -lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
1.68 -
1.69  (* FIXME: duplicates right_minus_eq from class group_add *)
1.70  (* but only this one is declared as a simp rule. *)
1.71  lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
1.72    by (rule right_minus_eq)
1.73
1.74 -lemma diff_eq_diff_eq:
1.75 -  "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
1.76 -  by (auto simp add: algebra_simps)
1.77 -
1.78  end
1.79
1.80
```