src/HOL/Groups.thy
changeset 62608 19f87fa0cfcb
parent 62379 340738057c8c
child 63145 703edebd1d92
     1.1 --- a/src/HOL/Groups.thy	Sun Mar 13 09:06:50 2016 +0100
     1.2 +++ b/src/HOL/Groups.thy	Sun Mar 13 10:22:46 2016 +0100
     1.3 @@ -310,6 +310,27 @@
     1.4    then show "c = a - b" by simp
     1.5  qed
     1.6  
     1.7 +lemma add_cancel_right_right [simp]:
     1.8 +  "a = a + b \<longleftrightarrow> b = 0" (is "?P \<longleftrightarrow> ?Q")
     1.9 +proof
    1.10 +  assume ?Q then show ?P by simp
    1.11 +next
    1.12 +  assume ?P then have "a - a = a + b - a" by simp
    1.13 +  then show ?Q by simp
    1.14 +qed
    1.15 +
    1.16 +lemma add_cancel_right_left [simp]:
    1.17 +  "a = b + a \<longleftrightarrow> b = 0"
    1.18 +  using add_cancel_right_right [of a b] by (simp add: ac_simps)
    1.19 +
    1.20 +lemma add_cancel_left_right [simp]:
    1.21 +  "a + b = a \<longleftrightarrow> b = 0"
    1.22 +  by (auto dest: sym)
    1.23 +
    1.24 +lemma add_cancel_left_left [simp]:
    1.25 +  "b + a = a \<longleftrightarrow> b = 0"
    1.26 +  by (auto dest: sym)
    1.27 +
    1.28  end
    1.29  
    1.30  class comm_monoid_diff = cancel_comm_monoid_add +