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.7 -class cancel_ab_semigroup_add = ab_semigroup_add +
     1.8 -  assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
     1.9 +class cancel_ab_semigroup_add = ab_semigroup_add + minus +
    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.14 +lemma add_diff_cancel_right' [simp]:
    1.15 +  "(a + b) - b = a"
    1.16 +  using add_diff_cancel_left' [of b a] by (simp add: ac_simps)
    1.17 +
    1.18  subclass cancel_semigroup_add
    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.39 +lemma add_diff_cancel_left [simp]:
    1.40 +  "(c + a) - (c + b) = a - b"
    1.41 +  unfolding diff_diff_add [symmetric] by simp
    1.42 +
    1.43 +lemma add_diff_cancel_right [simp]:
    1.44 +  "(a + c) - (b + c) = a - b"
    1.45 +  using add_diff_cancel_left [symmetric] by (simp add: ac_simps)
    1.46 +
    1.47 +lemma diff_right_commute:
    1.48 +  "a - c - b = a - b - c"
    1.49 +  by (simp add: diff_diff_add add.commute)
    1.50 +
    1.51  end
    1.52  
    1.53  class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add
    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.62 -lemma add_diff_cancel_right [simp]:
    1.63 -  "(a + c) - (b + c) = a - b"
    1.64 -  using add_diff_cancel_left [symmetric] by (simp add: add.commute)
    1.65 -
    1.66 -lemma add_diff_cancel_left' [simp]:
    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.73 -lemma add_diff_cancel_right' [simp]:
    1.74 -  "(a + b) - b = a"
    1.75 -  using add_diff_cancel_left' [symmetric] by (simp add: add.commute)
    1.76 -
    1.77 -lemma diff_add_zero [simp]:
    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.96 -  by (simp add: diff_diff_add add.commute)
    1.97 -
    1.98  lemma add_implies_diff:
    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.111 +lemma diff_add_zero [simp]:
   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.123  subclass cancel_comm_monoid_add
   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.138  lemma uminus_add_conv_diff [simp]:
   1.139 @@ -545,18 +554,6 @@
   1.140    "(a - b) + c = (a + c) - b"
   1.141    by (simp add: algebra_simps)
   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.147 -lemma diff_add_eq_diff_diff:
   1.148 -  "a - (b + c) = a - b - c"
   1.149 -  using diff_add_eq_diff_diff_swap [of a c b] by (simp add: add.commute)
   1.150 -
   1.151 -lemma add_diff_cancel_left [simp]:
   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  
   1.162 -hide_fact (open) ab_diff_conv_add_uminus add_imp_eq
   1.163 +hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus
   1.164 +
   1.165 +lemmas add_0 = add_0_left -- \<open>FIXME duplicate\<close>
   1.166 +lemmas mult_1 = mult_1_left -- \<open>FIXME duplicate\<close>
   1.167 +lemmas ab_left_minus = left_minus -- \<open>FIXME duplicate\<close>
   1.168 +lemmas diff_diff_eq = diff_diff_add -- \<open>FIXME duplicate\<close>
   1.169 +
   1.170  
   1.171  subsection {* Tools setup *}
   1.172