move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
authorhuffman
Thu Sep 04 17:18:44 2008 +0200 (2008-09-04)
changeset 2813032b4185bfdc7
parent 28129 8f647d24b49f
child 28131 3130d7b3149d
move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
src/HOL/OrderedGroup.thy
     1.1 --- a/src/HOL/OrderedGroup.thy	Thu Sep 04 16:43:51 2008 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Thu Sep 04 17:18:44 2008 +0200
     1.3 @@ -234,6 +234,12 @@
     1.4    thus ?thesis by (simp add: eq_commute)
     1.5  qed
     1.6  
     1.7 +lemma diff_add_cancel: "a - b + b = a"
     1.8 +  by (simp add: diff_minus add_assoc)
     1.9 +
    1.10 +lemma add_diff_cancel: "a + b - b = a"
    1.11 +  by (simp add: diff_minus add_assoc)
    1.12 +
    1.13  end
    1.14  
    1.15  class ab_group_add = minus + uminus + comm_monoid_add +
    1.16 @@ -283,12 +289,6 @@
    1.17  lemma diff_diff_eq2: "a - (b - c) = (a + c) - b"
    1.18    by (simp add: diff_minus add_ac)
    1.19  
    1.20 -lemma diff_add_cancel: "a - b + b = a"
    1.21 -  by (simp add: diff_minus add_ac)
    1.22 -
    1.23 -lemma add_diff_cancel: "a + b - b = a"
    1.24 -  by (simp add: diff_minus add_ac)
    1.25 -
    1.26  lemmas compare_rls =
    1.27         diff_minus [symmetric]
    1.28         add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2