Introduced new classes monoid_add and group_add
authornipkow
Thu May 24 07:27:44 2007 +0200 (2007-05-24)
changeset 23085fd30d75a6614
parent 23084 bc000fc64fce
child 23086 12320f6e2523
Introduced new classes monoid_add and group_add
src/HOL/Integ/NatBin.thy
src/HOL/OrderedGroup.thy
src/HOL/arith_data.ML
     1.1 --- a/src/HOL/Integ/NatBin.thy	Wed May 23 19:23:22 2007 +0200
     1.2 +++ b/src/HOL/Integ/NatBin.thy	Thu May 24 07:27:44 2007 +0200
     1.3 @@ -526,8 +526,8 @@
     1.4       "((number_of (v BIT x) ::int) = number_of (w BIT y)) =  
     1.5        (x=y & (((number_of v) ::int) = number_of w))"
     1.6  apply (simp only: number_of_BIT lemma1 lemma2 eq_commute
     1.7 -               OrderedGroup.add_left_cancel add_assoc OrderedGroup.add_0
     1.8 -            split add: bit.split) 
     1.9 +               OrderedGroup.add_left_cancel add_assoc OrderedGroup.add_0_left
    1.10 +            split add: bit.split)
    1.11  apply simp
    1.12  done
    1.13  
     2.1 --- a/src/HOL/OrderedGroup.thy	Wed May 23 19:23:22 2007 +0200
     2.2 +++ b/src/HOL/OrderedGroup.thy	Thu May 24 07:27:44 2007 +0200
     2.3 @@ -24,7 +24,7 @@
     2.4    \end{itemize}
     2.5  *}
     2.6  
     2.7 -subsection {* Semigroups, Groups *}
     2.8 +subsection {* Semigroups and Monoids *}
     2.9  
    2.10  class semigroup_add = plus +
    2.11    assumes add_assoc: "(a \<^loc>+ b) \<^loc>+ c = a \<^loc>+ (b \<^loc>+ c)"
    2.12 @@ -48,8 +48,14 @@
    2.13  
    2.14  theorems mult_ac = mult_assoc mult_commute mult_left_commute
    2.15  
    2.16 +class monoid_add = zero + semigroup_add +
    2.17 +  assumes add_0_left [simp]: "\<^loc>0 \<^loc>+ a = a" and add_0_right [simp]: "a \<^loc>+ \<^loc>0 = a"
    2.18 +
    2.19  class comm_monoid_add = zero + ab_semigroup_add +
    2.20 -  assumes add_0 [simp]: "\<^loc>0 \<^loc>+ a = a"
    2.21 +  assumes add_0: "\<^loc>0 \<^loc>+ a = a"
    2.22 +
    2.23 +instance comm_monoid_add < monoid_add
    2.24 +by intro_classes (insert comm_monoid_add_class.zero_plus.add_0, simp_all add: add_commute, auto)
    2.25  
    2.26  class monoid_mult = one + semigroup_mult +
    2.27    assumes mult_1_left [simp]: "\<^loc>1 \<^loc>* a  = a"
    2.28 @@ -80,80 +86,89 @@
    2.29    then show "b = c" by (rule add_imp_eq)
    2.30  qed
    2.31  
    2.32 +lemma add_left_cancel [simp]:
    2.33 +  "a + b = a + c \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
    2.34 +  by (blast dest: add_left_imp_eq)
    2.35 +
    2.36 +lemma add_right_cancel [simp]:
    2.37 +  "b + a = c + a \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
    2.38 +  by (blast dest: add_right_imp_eq)
    2.39 +
    2.40 +subsection {* Groups *}
    2.41 +
    2.42  class ab_group_add = minus + comm_monoid_add +
    2.43 +  assumes ab_left_minus: "uminus a \<^loc>+ a = \<^loc>0"
    2.44 +  assumes ab_diff_minus: "a \<^loc>- b = a \<^loc>+ (uminus b)"
    2.45 +
    2.46 +class group_add = minus + monoid_add +
    2.47    assumes left_minus [simp]: "uminus a \<^loc>+ a = \<^loc>0"
    2.48    assumes diff_minus: "a \<^loc>- b = a \<^loc>+ (uminus b)"
    2.49  
    2.50 +instance ab_group_add < group_add
    2.51 +by intro_classes (simp_all add: ab_left_minus ab_diff_minus)
    2.52 +
    2.53  instance ab_group_add \<subseteq> cancel_ab_semigroup_add
    2.54  proof intro_classes
    2.55    fix a b c :: 'a
    2.56    assume "a + b = a + c"
    2.57    then have "uminus a + a + b = uminus a + a + c" unfolding add_assoc by simp
    2.58 -  then show "b = c" by simp 
    2.59 +  then show "b = c" by simp
    2.60  qed
    2.61  
    2.62 -lemma add_0_right [simp]: "a + 0 = (a::'a::comm_monoid_add)"
    2.63 +lemma minus_add_cancel: "-(a::'a::group_add) + (a+b) = b"
    2.64 +by(simp add:add_assoc[symmetric])
    2.65 +
    2.66 +lemma minus_zero[simp]: "-(0::'a::group_add) = 0"
    2.67  proof -
    2.68 -  have "a + 0 = 0 + a" by (simp only: add_commute)
    2.69 -  also have "... = a" by simp
    2.70 +  have "-(0::'a::group_add) = - 0 + (0+0)" by(simp only: add_0_right)
    2.71 +  also have "\<dots> = 0" by(rule minus_add_cancel)
    2.72    finally show ?thesis .
    2.73  qed
    2.74  
    2.75 -lemmas add_zero_left = add_0
    2.76 -  and add_zero_right = add_0_right
    2.77 -
    2.78 -lemma add_left_cancel [simp]:
    2.79 -  "a + b = a + c \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
    2.80 -  by (blast dest: add_left_imp_eq) 
    2.81 +lemma minus_minus[simp]: "- (-(a::'a::group_add)) = a"
    2.82 +proof -
    2.83 +  have "-(-a) = -(-a) + (-a + a)" by simp
    2.84 +  also have "\<dots> = a" by(rule minus_add_cancel)
    2.85 +  finally show ?thesis .
    2.86 +qed
    2.87  
    2.88 -lemma add_right_cancel [simp]:
    2.89 -  "b + a = c + a \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
    2.90 -  by (blast dest: add_right_imp_eq)
    2.91 -
    2.92 -lemma right_minus [simp]: "a + -(a::'a::ab_group_add) = 0"
    2.93 +lemma right_minus[simp]: "a + - a = (0::'a::group_add)"
    2.94  proof -
    2.95 -  have "a + -a = -a + a" by (simp add: add_ac)
    2.96 -  also have "... = 0" by simp
    2.97 +  have "a + -a = -(-a) + -a" by simp
    2.98 +  also have "\<dots> = 0" thm group_add.left_minus by(rule left_minus)
    2.99    finally show ?thesis .
   2.100  qed
   2.101  
   2.102 -lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::ab_group_add))"
   2.103 +lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::group_add))"
   2.104  proof
   2.105 -  have "a = a - b + b" by (simp add: diff_minus add_ac)
   2.106 -  also assume "a - b = 0"
   2.107 -  finally show "a = b" by simp
   2.108 +  assume "a - b = 0"
   2.109 +  have "a = (a - b) + b" by (simp add:diff_minus add_assoc)
   2.110 +  also have "\<dots> = b" using `a - b = 0` by simp
   2.111 +  finally show "a = b" .
   2.112  next
   2.113 -  assume "a = b"
   2.114 -  thus "a - b = 0" by (simp add: diff_minus)
   2.115 -qed
   2.116 -
   2.117 -lemma minus_minus [simp]: "- (- (a::'a::ab_group_add)) = a"
   2.118 -proof (rule add_left_cancel [of "-a", THEN iffD1])
   2.119 -  show "(-a + -(-a) = -a + a)"
   2.120 -  by simp
   2.121 +  assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
   2.122  qed
   2.123  
   2.124 -lemma equals_zero_I: "a+b = 0 ==> -a = (b::'a::ab_group_add)"
   2.125 -apply (rule right_minus_eq [THEN iffD1, symmetric])
   2.126 -apply (simp add: diff_minus add_commute) 
   2.127 -done
   2.128 +lemma equals_zero_I: assumes "a+b = 0" shows "-a = (b::'a::group_add)"
   2.129 +proof -
   2.130 +  have "- a = -a + (a+b)" using assms by simp
   2.131 +  also have "\<dots> = b" by(simp add:add_assoc[symmetric])
   2.132 +  finally show ?thesis .
   2.133 +qed
   2.134  
   2.135 -lemma minus_zero [simp]: "- 0 = (0::'a::ab_group_add)"
   2.136 -by (simp add: equals_zero_I)
   2.137 +lemma diff_self[simp]: "(a::'a::group_add) - a = 0"
   2.138 +by(simp add: diff_minus)
   2.139  
   2.140 -lemma diff_self [simp]: "a - (a::'a::ab_group_add) = 0"
   2.141 -  by (simp add: diff_minus)
   2.142 -
   2.143 -lemma diff_0 [simp]: "(0::'a::ab_group_add) - a = -a"
   2.144 +lemma diff_0 [simp]: "(0::'a::group_add) - a = -a"
   2.145  by (simp add: diff_minus)
   2.146  
   2.147 -lemma diff_0_right [simp]: "a - (0::'a::ab_group_add) = a" 
   2.148 +lemma diff_0_right [simp]: "a - (0::'a::group_add) = a" 
   2.149  by (simp add: diff_minus)
   2.150  
   2.151 -lemma diff_minus_eq_add [simp]: "a - - b = a + (b::'a::ab_group_add)"
   2.152 +lemma diff_minus_eq_add [simp]: "a - - b = a + (b::'a::group_add)"
   2.153  by (simp add: diff_minus)
   2.154  
   2.155 -lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ab_group_add))" 
   2.156 +lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::group_add))" 
   2.157  proof 
   2.158    assume "- a = - b"
   2.159    hence "- (- a) = - (- b)"
   2.160 @@ -164,21 +179,21 @@
   2.161    thus "-a = -b" by simp
   2.162  qed
   2.163  
   2.164 -lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::ab_group_add))"
   2.165 +lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::group_add))"
   2.166  by (subst neg_equal_iff_equal [symmetric], simp)
   2.167  
   2.168 -lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::ab_group_add))"
   2.169 +lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::group_add))"
   2.170  by (subst neg_equal_iff_equal [symmetric], simp)
   2.171  
   2.172  text{*The next two equations can make the simplifier loop!*}
   2.173  
   2.174 -lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::ab_group_add))"
   2.175 +lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::group_add))"
   2.176  proof -
   2.177    have "(- (-a) = - b) = (- a = b)" by (rule neg_equal_iff_equal)
   2.178    thus ?thesis by (simp add: eq_commute)
   2.179  qed
   2.180  
   2.181 -lemma minus_equation_iff: "(- a = b) = (- (b::'a::ab_group_add) = a)"
   2.182 +lemma minus_equation_iff: "(- a = b) = (- (b::'a::group_add) = a)"
   2.183  proof -
   2.184    have "(- a = - (-b)) = (a = -b)" by (rule neg_equal_iff_equal)
   2.185    thus ?thesis by (simp add: eq_commute)
   2.186 @@ -186,7 +201,7 @@
   2.187  
   2.188  lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ab_group_add)"
   2.189  apply (rule equals_zero_I)
   2.190 -apply (simp add: add_ac) 
   2.191 +apply (simp add: add_ac)
   2.192  done
   2.193  
   2.194  lemma minus_diff_eq [simp]: "- (a - b) = b - (a::'a::ab_group_add)"
   2.195 @@ -1009,9 +1024,6 @@
   2.196  lemma add_minus_cancel: "(a::'a::ab_group_add) + (-a + b) = b"
   2.197  by (simp add: add_assoc[symmetric])
   2.198  
   2.199 -lemma minus_add_cancel: "-(a::'a::ab_group_add) + (a + b) = b"
   2.200 -by (simp add: add_assoc[symmetric])
   2.201 -
   2.202  lemma  le_add_right_mono: 
   2.203    assumes 
   2.204    "a <= b + (c::'a::pordered_ab_group_add)"
   2.205 @@ -1082,7 +1094,7 @@
   2.206  
   2.207  val cancel_ss = HOL_basic_ss settermless termless_agrp
   2.208    addsimprocs [add_ac_proc] addsimps
   2.209 -  [@{thm add_0}, @{thm add_0_right}, @{thm diff_def},
   2.210 +  [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_def},
   2.211     @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
   2.212     @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
   2.213     @{thm minus_add_cancel}];
     3.1 --- a/src/HOL/arith_data.ML	Wed May 23 19:23:22 2007 +0200
     3.2 +++ b/src/HOL/arith_data.ML	Thu May 24 07:27:44 2007 +0200
     3.3 @@ -928,7 +928,7 @@
     3.4      lessD = lessD @ [thm "Suc_leI"],
     3.5      neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_ordered_idom}],
     3.6      simpset = HOL_basic_ss
     3.7 -      addsimps [@{thm "add_zero_left"}, @{thm "add_zero_right"},
     3.8 +      addsimps [@{thm "monoid_add_class.zero_plus.add_0_left"}, @{thm "monoid_add_class.zero_plus.add_0_right"},
     3.9          @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"},
    3.10          @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
    3.11          @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},