src/HOL/Groups.thy
 changeset 49388 1ffd5a055acf parent 48891 c0eafbd55de3 child 49690 a6814de45b69
```     1.1 --- a/src/HOL/Groups.thy	Sat Sep 15 20:13:25 2012 +0200
1.2 +++ b/src/HOL/Groups.thy	Sat Sep 15 20:14:29 2012 +0200
1.3 @@ -213,6 +213,57 @@
1.6
1.7 +class comm_monoid_diff = comm_monoid_add + minus +
1.8 +  assumes diff_zero [simp]: "a - 0 = a"
1.9 +    and zero_diff [simp]: "0 - a = 0"
1.10 +    and add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b"
1.11 +    and diff_diff_add: "a - b - c = a - (b + c)"
1.12 +begin
1.13 +
1.15 +  "(a + c) - (b + c) = a - b"
1.17 +
1.19 +  "(b + a) - b = a"
1.20 +proof -
1.21 +  have "(b + a) - (b + 0) = a" by (simp only: add_diff_cancel_left diff_zero)
1.22 +  then show ?thesis by simp
1.23 +qed
1.24 +
1.26 +  "(a + b) - b = a"
1.28 +
1.30 +  "a - (a + b) = 0"
1.31 +proof -
1.32 +  have "a - (a + b) = (a + 0) - (a + b)" by simp
1.33 +  also have "\<dots> = 0" by (simp only: add_diff_cancel_left zero_diff)
1.34 +  finally show ?thesis .
1.35 +qed
1.36 +
1.37 +lemma diff_cancel [simp]:
1.38 +  "a - a = 0"
1.39 +proof -
1.40 +  have "(a + 0) - (a + 0) = 0" by (simp only: add_diff_cancel_left diff_zero)
1.41 +  then show ?thesis by simp
1.42 +qed
1.43 +
1.44 +lemma diff_right_commute:
1.45 +  "a - c - b = a - b - c"
1.47 +
1.49 +  assumes "c + b = a"
1.50 +  shows "c = a - b"
1.51 +proof -
1.52 +  from assms have "(b + c) - (b + 0) = a - b" by (simp add: add.commute)
1.53 +  then show "c = a - b" by simp
1.54 +qed
1.55 +
1.56 +end
1.57 +
1.58  class monoid_mult = one + semigroup_mult +
1.59    assumes mult_1_left: "1 * a  = a"
1.60      and mult_1_right: "a * 1 = a"
1.61 @@ -1263,3 +1314,4 @@
1.62  lemmas diff_def = diff_minus
1.63
1.64  end
1.65 +
```