src/HOL/OrderedGroup.thy
changeset 23085 fd30d75a6614
parent 22997 d4f3b015b50b
child 23181 f52b555f8141
     1.1 --- a/src/HOL/OrderedGroup.thy	Wed May 23 19:23:22 2007 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Thu May 24 07:27:44 2007 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4    \end{itemize}
     1.5  *}
     1.6  
     1.7 -subsection {* Semigroups, Groups *}
     1.8 +subsection {* Semigroups and Monoids *}
     1.9  
    1.10  class semigroup_add = plus +
    1.11    assumes add_assoc: "(a \<^loc>+ b) \<^loc>+ c = a \<^loc>+ (b \<^loc>+ c)"
    1.12 @@ -48,8 +48,14 @@
    1.13  
    1.14  theorems mult_ac = mult_assoc mult_commute mult_left_commute
    1.15  
    1.16 +class monoid_add = zero + semigroup_add +
    1.17 +  assumes add_0_left [simp]: "\<^loc>0 \<^loc>+ a = a" and add_0_right [simp]: "a \<^loc>+ \<^loc>0 = a"
    1.18 +
    1.19  class comm_monoid_add = zero + ab_semigroup_add +
    1.20 -  assumes add_0 [simp]: "\<^loc>0 \<^loc>+ a = a"
    1.21 +  assumes add_0: "\<^loc>0 \<^loc>+ a = a"
    1.22 +
    1.23 +instance comm_monoid_add < monoid_add
    1.24 +by intro_classes (insert comm_monoid_add_class.zero_plus.add_0, simp_all add: add_commute, auto)
    1.25  
    1.26  class monoid_mult = one + semigroup_mult +
    1.27    assumes mult_1_left [simp]: "\<^loc>1 \<^loc>* a  = a"
    1.28 @@ -80,80 +86,89 @@
    1.29    then show "b = c" by (rule add_imp_eq)
    1.30  qed
    1.31  
    1.32 +lemma add_left_cancel [simp]:
    1.33 +  "a + b = a + c \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
    1.34 +  by (blast dest: add_left_imp_eq)
    1.35 +
    1.36 +lemma add_right_cancel [simp]:
    1.37 +  "b + a = c + a \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
    1.38 +  by (blast dest: add_right_imp_eq)
    1.39 +
    1.40 +subsection {* Groups *}
    1.41 +
    1.42  class ab_group_add = minus + comm_monoid_add +
    1.43 +  assumes ab_left_minus: "uminus a \<^loc>+ a = \<^loc>0"
    1.44 +  assumes ab_diff_minus: "a \<^loc>- b = a \<^loc>+ (uminus b)"
    1.45 +
    1.46 +class group_add = minus + monoid_add +
    1.47    assumes left_minus [simp]: "uminus a \<^loc>+ a = \<^loc>0"
    1.48    assumes diff_minus: "a \<^loc>- b = a \<^loc>+ (uminus b)"
    1.49  
    1.50 +instance ab_group_add < group_add
    1.51 +by intro_classes (simp_all add: ab_left_minus ab_diff_minus)
    1.52 +
    1.53  instance ab_group_add \<subseteq> cancel_ab_semigroup_add
    1.54  proof intro_classes
    1.55    fix a b c :: 'a
    1.56    assume "a + b = a + c"
    1.57    then have "uminus a + a + b = uminus a + a + c" unfolding add_assoc by simp
    1.58 -  then show "b = c" by simp 
    1.59 +  then show "b = c" by simp
    1.60  qed
    1.61  
    1.62 -lemma add_0_right [simp]: "a + 0 = (a::'a::comm_monoid_add)"
    1.63 +lemma minus_add_cancel: "-(a::'a::group_add) + (a+b) = b"
    1.64 +by(simp add:add_assoc[symmetric])
    1.65 +
    1.66 +lemma minus_zero[simp]: "-(0::'a::group_add) = 0"
    1.67  proof -
    1.68 -  have "a + 0 = 0 + a" by (simp only: add_commute)
    1.69 -  also have "... = a" by simp
    1.70 +  have "-(0::'a::group_add) = - 0 + (0+0)" by(simp only: add_0_right)
    1.71 +  also have "\<dots> = 0" by(rule minus_add_cancel)
    1.72    finally show ?thesis .
    1.73  qed
    1.74  
    1.75 -lemmas add_zero_left = add_0
    1.76 -  and add_zero_right = add_0_right
    1.77 -
    1.78 -lemma add_left_cancel [simp]:
    1.79 -  "a + b = a + c \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
    1.80 -  by (blast dest: add_left_imp_eq) 
    1.81 +lemma minus_minus[simp]: "- (-(a::'a::group_add)) = a"
    1.82 +proof -
    1.83 +  have "-(-a) = -(-a) + (-a + a)" by simp
    1.84 +  also have "\<dots> = a" by(rule minus_add_cancel)
    1.85 +  finally show ?thesis .
    1.86 +qed
    1.87  
    1.88 -lemma add_right_cancel [simp]:
    1.89 -  "b + a = c + a \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
    1.90 -  by (blast dest: add_right_imp_eq)
    1.91 -
    1.92 -lemma right_minus [simp]: "a + -(a::'a::ab_group_add) = 0"
    1.93 +lemma right_minus[simp]: "a + - a = (0::'a::group_add)"
    1.94  proof -
    1.95 -  have "a + -a = -a + a" by (simp add: add_ac)
    1.96 -  also have "... = 0" by simp
    1.97 +  have "a + -a = -(-a) + -a" by simp
    1.98 +  also have "\<dots> = 0" thm group_add.left_minus by(rule left_minus)
    1.99    finally show ?thesis .
   1.100  qed
   1.101  
   1.102 -lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::ab_group_add))"
   1.103 +lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::group_add))"
   1.104  proof
   1.105 -  have "a = a - b + b" by (simp add: diff_minus add_ac)
   1.106 -  also assume "a - b = 0"
   1.107 -  finally show "a = b" by simp
   1.108 +  assume "a - b = 0"
   1.109 +  have "a = (a - b) + b" by (simp add:diff_minus add_assoc)
   1.110 +  also have "\<dots> = b" using `a - b = 0` by simp
   1.111 +  finally show "a = b" .
   1.112  next
   1.113 -  assume "a = b"
   1.114 -  thus "a - b = 0" by (simp add: diff_minus)
   1.115 -qed
   1.116 -
   1.117 -lemma minus_minus [simp]: "- (- (a::'a::ab_group_add)) = a"
   1.118 -proof (rule add_left_cancel [of "-a", THEN iffD1])
   1.119 -  show "(-a + -(-a) = -a + a)"
   1.120 -  by simp
   1.121 +  assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
   1.122  qed
   1.123  
   1.124 -lemma equals_zero_I: "a+b = 0 ==> -a = (b::'a::ab_group_add)"
   1.125 -apply (rule right_minus_eq [THEN iffD1, symmetric])
   1.126 -apply (simp add: diff_minus add_commute) 
   1.127 -done
   1.128 +lemma equals_zero_I: assumes "a+b = 0" shows "-a = (b::'a::group_add)"
   1.129 +proof -
   1.130 +  have "- a = -a + (a+b)" using assms by simp
   1.131 +  also have "\<dots> = b" by(simp add:add_assoc[symmetric])
   1.132 +  finally show ?thesis .
   1.133 +qed
   1.134  
   1.135 -lemma minus_zero [simp]: "- 0 = (0::'a::ab_group_add)"
   1.136 -by (simp add: equals_zero_I)
   1.137 +lemma diff_self[simp]: "(a::'a::group_add) - a = 0"
   1.138 +by(simp add: diff_minus)
   1.139  
   1.140 -lemma diff_self [simp]: "a - (a::'a::ab_group_add) = 0"
   1.141 -  by (simp add: diff_minus)
   1.142 -
   1.143 -lemma diff_0 [simp]: "(0::'a::ab_group_add) - a = -a"
   1.144 +lemma diff_0 [simp]: "(0::'a::group_add) - a = -a"
   1.145  by (simp add: diff_minus)
   1.146  
   1.147 -lemma diff_0_right [simp]: "a - (0::'a::ab_group_add) = a" 
   1.148 +lemma diff_0_right [simp]: "a - (0::'a::group_add) = a" 
   1.149  by (simp add: diff_minus)
   1.150  
   1.151 -lemma diff_minus_eq_add [simp]: "a - - b = a + (b::'a::ab_group_add)"
   1.152 +lemma diff_minus_eq_add [simp]: "a - - b = a + (b::'a::group_add)"
   1.153  by (simp add: diff_minus)
   1.154  
   1.155 -lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ab_group_add))" 
   1.156 +lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::group_add))" 
   1.157  proof 
   1.158    assume "- a = - b"
   1.159    hence "- (- a) = - (- b)"
   1.160 @@ -164,21 +179,21 @@
   1.161    thus "-a = -b" by simp
   1.162  qed
   1.163  
   1.164 -lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::ab_group_add))"
   1.165 +lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::group_add))"
   1.166  by (subst neg_equal_iff_equal [symmetric], simp)
   1.167  
   1.168 -lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::ab_group_add))"
   1.169 +lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::group_add))"
   1.170  by (subst neg_equal_iff_equal [symmetric], simp)
   1.171  
   1.172  text{*The next two equations can make the simplifier loop!*}
   1.173  
   1.174 -lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::ab_group_add))"
   1.175 +lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::group_add))"
   1.176  proof -
   1.177    have "(- (-a) = - b) = (- a = b)" by (rule neg_equal_iff_equal)
   1.178    thus ?thesis by (simp add: eq_commute)
   1.179  qed
   1.180  
   1.181 -lemma minus_equation_iff: "(- a = b) = (- (b::'a::ab_group_add) = a)"
   1.182 +lemma minus_equation_iff: "(- a = b) = (- (b::'a::group_add) = a)"
   1.183  proof -
   1.184    have "(- a = - (-b)) = (a = -b)" by (rule neg_equal_iff_equal)
   1.185    thus ?thesis by (simp add: eq_commute)
   1.186 @@ -186,7 +201,7 @@
   1.187  
   1.188  lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ab_group_add)"
   1.189  apply (rule equals_zero_I)
   1.190 -apply (simp add: add_ac) 
   1.191 +apply (simp add: add_ac)
   1.192  done
   1.193  
   1.194  lemma minus_diff_eq [simp]: "- (a - b) = b - (a::'a::ab_group_add)"
   1.195 @@ -1009,9 +1024,6 @@
   1.196  lemma add_minus_cancel: "(a::'a::ab_group_add) + (-a + b) = b"
   1.197  by (simp add: add_assoc[symmetric])
   1.198  
   1.199 -lemma minus_add_cancel: "-(a::'a::ab_group_add) + (a + b) = b"
   1.200 -by (simp add: add_assoc[symmetric])
   1.201 -
   1.202  lemma  le_add_right_mono: 
   1.203    assumes 
   1.204    "a <= b + (c::'a::pordered_ab_group_add)"
   1.205 @@ -1082,7 +1094,7 @@
   1.206  
   1.207  val cancel_ss = HOL_basic_ss settermless termless_agrp
   1.208    addsimprocs [add_ac_proc] addsimps
   1.209 -  [@{thm add_0}, @{thm add_0_right}, @{thm diff_def},
   1.210 +  [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_def},
   1.211     @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
   1.212     @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
   1.213     @{thm minus_add_cancel}];