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.12    unfolding eq_neg_iff_add_eq_0 [symmetric]
    1.13    by (rule equation_minus_iff)
    1.14  
    1.15 +lemma minus_diff_eq [simp]: "- (a - b) = b - a"
    1.16 +  by (simp add: diff_minus minus_add)
    1.17 +
    1.18 +lemma add_diff_eq[algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
    1.19 +  by (simp add: diff_minus add_assoc)
    1.20 +
    1.21 +lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
    1.22 +  by (auto simp add: diff_minus add_assoc)
    1.23 +
    1.24 +lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
    1.25 +  by (auto simp add: diff_minus add_assoc)
    1.26 +
    1.27 +lemma diff_diff_eq2[algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"
    1.28 +  by (simp add: diff_minus minus_add add_assoc)
    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.39  class ab_group_add = minus + uminus + comm_monoid_add +
    1.40 @@ -440,40 +461,17 @@
    1.41    "- (a + b) = - a + - b"
    1.42  by (rule minus_unique) (simp add: add_ac)
    1.43  
    1.44 -lemma minus_diff_eq [simp]:
    1.45 -  "- (a - b) = b - a"
    1.46 -by (simp add: diff_minus add_commute)
    1.47 -
    1.48 -lemma add_diff_eq[algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
    1.49 -by (simp add: diff_minus add_ac)
    1.50 -
    1.51  lemma diff_add_eq[algebra_simps, field_simps]: "(a - b) + c = (a + c) - b"
    1.52  by (simp add: diff_minus add_ac)
    1.53  
    1.54 -lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
    1.55 -by (auto simp add: diff_minus add_assoc)
    1.56 -
    1.57 -lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
    1.58 -by (auto simp add: diff_minus add_assoc)
    1.59 -
    1.60  lemma diff_diff_eq[algebra_simps, field_simps]: "(a - b) - c = a - (b + c)"
    1.61  by (simp add: diff_minus add_ac)
    1.62  
    1.63 -lemma diff_diff_eq2[algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"
    1.64 -by (simp add: diff_minus add_ac)
    1.65 -
    1.66 -lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
    1.67 -by (simp add: algebra_simps)
    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