src/HOL/OrderedGroup.thy
changeset 27474 a89d755b029d
parent 27250 7eef2b183032
child 27516 9a5d4a8d4aac
     1.1 --- a/src/HOL/OrderedGroup.thy	Thu Jul 03 18:03:10 2008 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Thu Jul 03 18:15:39 2008 +0200
     1.3 @@ -106,6 +106,17 @@
     1.4  class cancel_semigroup_add = semigroup_add +
     1.5    assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
     1.6    assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
     1.7 +begin
     1.8 +
     1.9 +lemma add_left_cancel [simp]:
    1.10 +  "a + b = a + c \<longleftrightarrow> b = c"
    1.11 +  by (blast dest: add_left_imp_eq)
    1.12 +
    1.13 +lemma add_right_cancel [simp]:
    1.14 +  "b + a = c + a \<longleftrightarrow> b = c"
    1.15 +  by (blast dest: add_right_imp_eq)
    1.16 +
    1.17 +end
    1.18  
    1.19  class cancel_ab_semigroup_add = ab_semigroup_add +
    1.20    assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
    1.21 @@ -125,19 +136,6 @@
    1.22  
    1.23  end
    1.24  
    1.25 -context cancel_ab_semigroup_add
    1.26 -begin
    1.27 -
    1.28 -lemma add_left_cancel [simp]:
    1.29 -  "a + b = a + c \<longleftrightarrow> b = c"
    1.30 -  by (blast dest: add_left_imp_eq)
    1.31 -
    1.32 -lemma add_right_cancel [simp]:
    1.33 -  "b + a = c + a \<longleftrightarrow> b = c"
    1.34 -  by (blast dest: add_right_imp_eq)
    1.35 -
    1.36 -end
    1.37 -
    1.38  subsection {* Groups *}
    1.39  
    1.40  class group_add = minus + uminus + monoid_add +