dropped redundancy
authorhaftmann
Thu Oct 25 19:27:52 2007 +0200 (2007-10-25)
changeset 2519437a1743f0fc3
parent 25193 e2e1a4b00de3
child 25195 62638dcafe38
dropped redundancy
src/HOL/OrderedGroup.thy
     1.1 --- a/src/HOL/OrderedGroup.thy	Thu Oct 25 19:27:50 2007 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Thu Oct 25 19:27:52 2007 +0200
     1.3 @@ -90,9 +90,8 @@
     1.4  
     1.5  class cancel_ab_semigroup_add = ab_semigroup_add +
     1.6    assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
     1.7 -begin
     1.8  
     1.9 -subclass cancel_semigroup_add
    1.10 +subclass (in cancel_ab_semigroup_add) cancel_semigroup_add
    1.11  proof unfold_locales
    1.12    fix a b c :: 'a
    1.13    assume "a + b = a + c" 
    1.14 @@ -104,7 +103,8 @@
    1.15    then show "b = c" by (rule add_imp_eq)
    1.16  qed
    1.17  
    1.18 -end context cancel_ab_semigroup_add begin
    1.19 +context cancel_ab_semigroup_add
    1.20 +begin
    1.21  
    1.22  lemma add_left_cancel [simp]:
    1.23    "a + b = a + c \<longleftrightarrow> b = c"
    1.24 @@ -223,21 +223,6 @@
    1.25  subclass (in ab_group_add) group_add
    1.26    by unfold_locales (simp_all add: ab_left_minus ab_diff_minus)
    1.27  
    1.28 -subclass (in ab_group_add) cancel_semigroup_add
    1.29 -proof unfold_locales
    1.30 -  fix a b c :: 'a
    1.31 -  assume "a + b = a + c"
    1.32 -  then have "- a + a + b = - a + a + c"
    1.33 -    unfolding add_assoc by simp
    1.34 -  then show "b = c" by simp
    1.35 -next
    1.36 -  fix a b c :: 'a
    1.37 -  assume "b + a = c + a"
    1.38 -  then have "b + (a + - a) = c + (a + - a)"
    1.39 -    unfolding add_assoc [symmetric] by simp
    1.40 -  then show "b = c" by simp
    1.41 -qed
    1.42 -
    1.43  subclass (in ab_group_add) cancel_ab_semigroup_add
    1.44  proof unfold_locales
    1.45    fix a b c :: 'a