src/HOL/Groups.thy
 changeset 59815 cce82e360c2f parent 59559 35da1bbf234e child 60758 d8d85a8172b5
```     1.1 --- a/src/HOL/Groups.thy	Mon Mar 23 19:05:14 2015 +0100
1.2 +++ b/src/HOL/Groups.thy	Mon Mar 23 19:05:14 2015 +0100
1.3 @@ -248,55 +248,52 @@
1.4
1.5  end
1.6
1.8 -  assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
1.10 +  assumes add_diff_cancel_left' [simp]: "(a + b) - a = b"
1.11 +  assumes diff_diff_add [algebra_simps, field_simps]: "a - b - c = a - (b + c)"
1.12  begin
1.13
1.15 +  "(a + b) - b = a"
1.17 +
1.19  proof
1.20    fix a b c :: 'a
1.21 -  assume "a + b = a + c"
1.22 -  then show "b = c" by (rule add_imp_eq)
1.23 +  assume "a + b = a + c"
1.24 +  then have "a + b - a = a + c - a"
1.25 +    by simp
1.26 +  then show "b = c"
1.27 +    by simp
1.28  next
1.29    fix a b c :: 'a
1.30    assume "b + a = c + a"
1.31 -  then have "a + b = a + c" by (simp only: add.commute)
1.32 -  then show "b = c" by (rule add_imp_eq)
1.33 +  then have "b + a - a = c + a - a"
1.34 +    by simp
1.35 +  then show "b = c"
1.36 +    by simp
1.37  qed
1.38
1.40 +  "(c + a) - (c + b) = a - b"
1.41 +  unfolding diff_diff_add [symmetric] by simp
1.42 +
1.44 +  "(a + c) - (b + c) = a - b"
1.46 +
1.47 +lemma diff_right_commute:
1.48 +  "a - c - b = a - b - c"
1.50 +
1.51  end
1.52
1.54 -
1.55 -class comm_monoid_diff = comm_monoid_add + minus +
1.56 -  assumes diff_zero [simp]: "a - 0 = a"
1.57 -    and zero_diff [simp]: "0 - a = 0"
1.58 -    and add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b"
1.59 -    and diff_diff_add: "a - b - c = a - (b + c)"
1.60  begin
1.61
1.63 -  "(a + c) - (b + c) = a - b"
1.65 -
1.67 -  "(b + a) - b = a"
1.68 -proof -
1.69 -  have "(b + a) - (b + 0) = a" by (simp only: add_diff_cancel_left diff_zero)
1.70 -  then show ?thesis by simp
1.71 -qed
1.72 -
1.74 -  "(a + b) - b = a"
1.76 -
1.78 -  "a - (a + b) = 0"
1.79 -proof -
1.80 -  have "a - (a + b) = (a + 0) - (a + b)" by simp
1.81 -  also have "\<dots> = 0" by (simp only: add_diff_cancel_left zero_diff)
1.82 -  finally show ?thesis .
1.83 -qed
1.84 +lemma diff_zero [simp]:
1.85 +  "a - 0 = a"
1.86 +  using add_diff_cancel_right' [of a 0] by simp
1.87
1.88  lemma diff_cancel [simp]:
1.89    "a - a = 0"
1.90 @@ -305,10 +302,6 @@
1.91    then show ?thesis by simp
1.92  qed
1.93
1.94 -lemma diff_right_commute:
1.95 -  "a - c - b = a - b - c"
1.97 -
1.99    assumes "c + b = a"
1.100    shows "c = a - b"
1.101 @@ -317,6 +310,20 @@
1.102    then show "c = a - b" by simp
1.103  qed
1.104
1.105 +end
1.106 +
1.107 +class comm_monoid_diff = cancel_comm_monoid_add +
1.108 +  assumes zero_diff [simp]: "0 - a = 0"
1.109 +begin
1.110 +
1.112 +  "a - (a + b) = 0"
1.113 +proof -
1.114 +  have "a - (a + b) = (a + 0) - (a + b)" by simp
1.115 +  also have "\<dots> = 0" by (simp only: add_diff_cancel_left zero_diff)
1.116 +  finally show ?thesis .
1.117 +qed
1.118 +
1.119  end
1.120
1.121
1.122 @@ -527,10 +534,12 @@
1.124  proof
1.125    fix a b c :: 'a
1.126 -  assume "a + b = a + c"
1.127 -  then have "- a + a + b = - a + a + c"
1.128 -    by (simp only: add.assoc)
1.129 -  then show "b = c" by simp
1.130 +  have "b + a - a = b"
1.131 +    by simp
1.132 +  then show "a + b - a = b"
1.133 +    by (simp add: ac_simps)
1.134 +  show "a - b - c = a - (b + c)"
1.135 +    by (simp add: algebra_simps)
1.136  qed
1.137
1.139 @@ -545,18 +554,6 @@
1.140    "(a - b) + c = (a + c) - b"
1.142
1.143 -lemma diff_diff_eq [algebra_simps, field_simps]:
1.144 -  "(a - b) - c = a - (b + c)"
1.145 -  by (simp add: algebra_simps)
1.146 -
1.148 -  "a - (b + c) = a - b - c"
1.150 -
1.152 -  "(c + a) - (c + b) = a - b"
1.153 -  by (simp add: algebra_simps)
1.154 -
1.155  end
1.156
1.157
1.158 @@ -1375,7 +1372,13 @@
1.159
1.160  end
1.161