tuned order
authorhaftmann
Thu Jan 08 18:23:29 2015 +0100 (2015-01-08)
changeset 593228ccecf1415b0
parent 59321 2b40fb12b09d
child 59323 468bd3aedfa1
tuned order
src/HOL/Groups.thy
     1.1 --- a/src/HOL/Groups.thy	Thu Jan 08 18:23:27 2015 +0100
     1.2 +++ b/src/HOL/Groups.thy	Thu Jan 08 18:23:29 2015 +0100
     1.3 @@ -208,57 +208,6 @@
     1.4  
     1.5  end
     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 @@ -319,6 +268,57 @@
    1.62  
    1.63  class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add
    1.64  
    1.65 +class comm_monoid_diff = comm_monoid_add + minus +
    1.66 +  assumes diff_zero [simp]: "a - 0 = a"
    1.67 +    and zero_diff [simp]: "0 - a = 0"
    1.68 +    and add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b"
    1.69 +    and diff_diff_add: "a - b - c = a - (b + c)"
    1.70 +begin
    1.71 +
    1.72 +lemma add_diff_cancel_right [simp]:
    1.73 +  "(a + c) - (b + c) = a - b"
    1.74 +  using add_diff_cancel_left [symmetric] by (simp add: add.commute)
    1.75 +
    1.76 +lemma add_diff_cancel_left' [simp]:
    1.77 +  "(b + a) - b = a"
    1.78 +proof -
    1.79 +  have "(b + a) - (b + 0) = a" by (simp only: add_diff_cancel_left diff_zero)
    1.80 +  then show ?thesis by simp
    1.81 +qed
    1.82 +
    1.83 +lemma add_diff_cancel_right' [simp]:
    1.84 +  "(a + b) - b = a"
    1.85 +  using add_diff_cancel_left' [symmetric] by (simp add: add.commute)
    1.86 +
    1.87 +lemma diff_add_zero [simp]:
    1.88 +  "a - (a + b) = 0"
    1.89 +proof -
    1.90 +  have "a - (a + b) = (a + 0) - (a + b)" by simp
    1.91 +  also have "\<dots> = 0" by (simp only: add_diff_cancel_left zero_diff)
    1.92 +  finally show ?thesis .
    1.93 +qed
    1.94 +
    1.95 +lemma diff_cancel [simp]:
    1.96 +  "a - a = 0"
    1.97 +proof -
    1.98 +  have "(a + 0) - (a + 0) = 0" by (simp only: add_diff_cancel_left diff_zero)
    1.99 +  then show ?thesis by simp
   1.100 +qed
   1.101 +
   1.102 +lemma diff_right_commute:
   1.103 +  "a - c - b = a - b - c"
   1.104 +  by (simp add: diff_diff_add add.commute)
   1.105 +
   1.106 +lemma add_implies_diff:
   1.107 +  assumes "c + b = a"
   1.108 +  shows "c = a - b"
   1.109 +proof -
   1.110 +  from assms have "(b + c) - (b + 0) = a - b" by (simp add: add.commute)
   1.111 +  then show "c = a - b" by simp
   1.112 +qed
   1.113 +
   1.114 +end
   1.115 +
   1.116  
   1.117  subsection {* Groups *}
   1.118