moved ordered_ab_semigroup_add to OrderedGroup.thy
authorhaftmann
Tue Aug 21 13:30:36 2007 +0200 (2007-08-21)
changeset 24380c215e256beca
parent 24379 823ffe1fdf67
child 24381 560e8ecdf633
moved ordered_ab_semigroup_add to OrderedGroup.thy
src/HOL/Finite_Set.thy
src/HOL/OrderedGroup.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Aug 21 09:07:04 2007 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Aug 21 13:30:36 2007 +0200
     1.3 @@ -2653,7 +2653,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -class linordered_ab_semigroup_add = linorder + pordered_ab_semigroup_add
     1.8 +context ordered_ab_semigroup_add
     1.9  begin
    1.10  
    1.11  lemma add_Min_commute:
     2.1 --- a/src/HOL/OrderedGroup.thy	Tue Aug 21 09:07:04 2007 +0200
     2.2 +++ b/src/HOL/OrderedGroup.thy	Tue Aug 21 13:30:36 2007 +0200
     2.3 @@ -235,7 +235,13 @@
     2.4    thus "a \<le> b" by simp
     2.5  qed
     2.6  
     2.7 -class ordered_cancel_ab_semigroup_add = pordered_cancel_ab_semigroup_add + linorder
     2.8 +class ordered_ab_semigroup_add =
     2.9 +  linorder + pordered_ab_semigroup_add
    2.10 +
    2.11 +class ordered_cancel_ab_semigroup_add =
    2.12 +  linorder + pordered_cancel_ab_semigroup_add
    2.13 +
    2.14 +instance ordered_cancel_ab_semigroup_add \<subseteq> ordered_ab_semigroup_add ..
    2.15  
    2.16  instance ordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add_imp_le
    2.17  proof
    2.18 @@ -1049,7 +1055,7 @@
    2.19    diff_less_eq less_diff_eq diff_le_eq le_diff_eq
    2.20  
    2.21  lemma estimate_by_abs:
    2.22 -"a + b <= (c::'a::lordered_ab_group_abs) \<Longrightarrow> a <= c + abs b" 
    2.23 +  "a + b <= (c::'a::lordered_ab_group_abs) \<Longrightarrow> a <= c + abs b" 
    2.24  proof -
    2.25    assume "a+b <= c"
    2.26    hence 2: "a <= c+(-b)" by (simp add: group_simps)
    2.27 @@ -1061,12 +1067,9 @@
    2.28  subsection {* Tools setup *}
    2.29  
    2.30  text{*Simplification of @{term "x-y < 0"}, etc.*}
    2.31 -lemmas diff_less_0_iff_less = less_iff_diff_less_0 [symmetric]
    2.32 -lemmas diff_eq_0_iff_eq = eq_iff_diff_eq_0 [symmetric]
    2.33 -lemmas diff_le_0_iff_le = le_iff_diff_le_0 [symmetric]
    2.34 -declare diff_less_0_iff_less [simp]
    2.35 -declare diff_eq_0_iff_eq [simp,noatp]
    2.36 -declare diff_le_0_iff_le [simp]
    2.37 +lemmas diff_less_0_iff_less [simp] = less_iff_diff_less_0 [symmetric]
    2.38 +lemmas diff_eq_0_iff_eq [simp, noatp] = eq_iff_diff_eq_0 [symmetric]
    2.39 +lemmas diff_le_0_iff_le [simp] = le_iff_diff_le_0 [symmetric]
    2.40  
    2.41  ML {*
    2.42  structure ab_group_add_cancel = Abel_Cancel(