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.4  subclass (in comm_monoid_add) monoid_add proof
     1.5  qed (fact add.left_neutral add.right_neutral)+
     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.14 +lemma add_diff_cancel_right [simp]:
    1.15 +  "(a + c) - (b + c) = a - b"
    1.16 +  using add_diff_cancel_left [symmetric] by (simp add: add.commute)
    1.17 +
    1.18 +lemma add_diff_cancel_left' [simp]:
    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.25 +lemma add_diff_cancel_right' [simp]:
    1.26 +  "(a + b) - b = a"
    1.27 +  using add_diff_cancel_left' [symmetric] by (simp add: add.commute)
    1.28 +
    1.29 +lemma diff_add_zero [simp]:
    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.46 +  by (simp add: diff_diff_add add.commute)
    1.47 +
    1.48 +lemma add_implies_diff:
    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 +