sharing simp rules between ordered monoids and rings
authorfleury <Mathias.Fleury@mpi-inf.mpg.de>
Tue Jul 12 13:55:35 2016 +0200 (2016-07-12)
changeset 634563365c8ec67bd
parent 63455 019856db2bb6
child 63463 b6a1047bc164
sharing simp rules between ordered monoids and rings
NEWS
src/HOL/Groups.thy
src/HOL/Nonstandard_Analysis/StarDef.thy
src/HOL/Rings.thy
     1.1 --- a/NEWS	Tue Jul 12 11:51:05 2016 +0200
     1.2 +++ b/NEWS	Tue Jul 12 13:55:35 2016 +0200
     1.3 @@ -254,6 +254,29 @@
     1.4  * Removed obsolete theorem nat_less_cases. INCOMPATIBILITY, use
     1.5  linorder_cases instead.
     1.6  
     1.7 +* Some theorems about groups and orders have been generalised from
     1.8 +  groups to semi-groups that are also monoids:
     1.9 +    le_add_same_cancel1
    1.10 +    le_add_same_cancel2
    1.11 +    less_add_same_cancel1
    1.12 +    less_add_same_cancel2
    1.13 +    add_le_same_cancel1
    1.14 +    add_le_same_cancel2
    1.15 +    add_less_same_cancel1
    1.16 +    add_less_same_cancel2
    1.17 +
    1.18 +* Some simplifications theorems about rings have been removed, since
    1.19 +  superseeded by a more general version:
    1.20 +    less_add_cancel_left_greater_zero ~> less_add_same_cancel1
    1.21 +    less_add_cancel_right_greater_zero ~> less_add_same_cancel2
    1.22 +    less_eq_add_cancel_left_greater_eq_zero ~> le_add_same_cancel1
    1.23 +    less_eq_add_cancel_right_greater_eq_zero ~> le_add_same_cancel2
    1.24 +    less_eq_add_cancel_left_less_eq_zero ~> add_le_same_cancel1
    1.25 +    less_eq_add_cancel_right_less_eq_zero ~> add_le_same_cancel2
    1.26 +    less_add_cancel_left_less_zero ~> add_less_same_cancel1
    1.27 +    less_add_cancel_right_less_zero ~> add_less_same_cancel2
    1.28 +INCOMPATIBILITY.
    1.29 +
    1.30  * Renamed split_if -> if_split and split_if_asm -> if_split_asm to
    1.31  resemble the f.split naming convention, INCOMPATIBILITY.
    1.32  
    1.33 @@ -398,6 +421,12 @@
    1.34  
    1.35  * Introduced the type classes canonically_ordered_comm_monoid_add and dioid.
    1.36  
    1.37 +* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When
    1.38 +instantiating linordered_semiring_strict and ordered_ab_group_add, an explicit
    1.39 +instantiation of ordered_ab_semigroup_monoid_add_imp_le might be
    1.40 +required.
    1.41 +INCOMPATIBILITY.
    1.42 +
    1.43  * Added topological_monoid
    1.44  
    1.45  * Library/Complete_Partial_Order2.thy provides reasoning support for
     2.1 --- a/src/HOL/Groups.thy	Tue Jul 12 11:51:05 2016 +0200
     2.2 +++ b/src/HOL/Groups.thy	Tue Jul 12 13:55:35 2016 +0200
     2.3 @@ -800,12 +800,55 @@
     2.4  
     2.5  end
     2.6  
     2.7 +class ordered_ab_semigroup_monoid_add_imp_le = monoid_add + ordered_ab_semigroup_add_imp_le
     2.8 +begin
     2.9 +
    2.10 +lemma add_less_same_cancel1 [simp]:
    2.11 +  "b + a < b \<longleftrightarrow> a < 0"
    2.12 +  using add_less_cancel_left [of _ _ 0] by simp
    2.13 +
    2.14 +lemma add_less_same_cancel2 [simp]:
    2.15 +  "a + b < b \<longleftrightarrow> a < 0"
    2.16 +  using add_less_cancel_right [of _ _ 0] by simp
    2.17 +
    2.18 +lemma less_add_same_cancel1 [simp]:
    2.19 +  "a < a + b \<longleftrightarrow> 0 < b"
    2.20 +  using add_less_cancel_left [of _ 0] by simp
    2.21 +
    2.22 +lemma less_add_same_cancel2 [simp]:
    2.23 +  "a < b + a \<longleftrightarrow> 0 < b"
    2.24 +  using add_less_cancel_right [of 0] by simp
    2.25 +
    2.26 +lemma add_le_same_cancel1 [simp]:
    2.27 +  "b + a \<le> b \<longleftrightarrow> a \<le> 0"
    2.28 +  using add_le_cancel_left [of _ _ 0] by simp
    2.29 +
    2.30 +lemma add_le_same_cancel2 [simp]:
    2.31 +  "a + b \<le> b \<longleftrightarrow> a \<le> 0"
    2.32 +  using add_le_cancel_right [of _ _ 0] by simp
    2.33 +
    2.34 +lemma le_add_same_cancel1 [simp]:
    2.35 +  "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
    2.36 +  using add_le_cancel_left [of _ 0] by simp
    2.37 +
    2.38 +lemma le_add_same_cancel2 [simp]:
    2.39 +  "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
    2.40 +  using add_le_cancel_right [of 0] by simp
    2.41 +
    2.42 +subclass cancel_comm_monoid_add
    2.43 +  by standard auto
    2.44 +
    2.45 +subclass ordered_cancel_comm_monoid_add
    2.46 +  by standard
    2.47 +
    2.48 +end
    2.49 +
    2.50  class ordered_ab_group_add = ab_group_add + ordered_ab_semigroup_add
    2.51  begin
    2.52  
    2.53  subclass ordered_cancel_ab_semigroup_add ..
    2.54  
    2.55 -subclass ordered_ab_semigroup_add_imp_le
    2.56 +subclass ordered_ab_semigroup_monoid_add_imp_le
    2.57  proof
    2.58    fix a b c :: 'a
    2.59    assume "c + a \<le> c + b"
    2.60 @@ -816,32 +859,6 @@
    2.61    then show "a \<le> b" by simp
    2.62  qed
    2.63  
    2.64 -subclass ordered_cancel_comm_monoid_add ..
    2.65 -
    2.66 -lemma add_less_same_cancel1 [simp]: "b + a < b \<longleftrightarrow> a < 0"
    2.67 -  using add_less_cancel_left [of _ _ 0] by simp
    2.68 -
    2.69 -lemma add_less_same_cancel2 [simp]: "a + b < b \<longleftrightarrow> a < 0"
    2.70 -  using add_less_cancel_right [of _ _ 0] by simp
    2.71 -
    2.72 -lemma less_add_same_cancel1 [simp]: "a < a + b \<longleftrightarrow> 0 < b"
    2.73 -  using add_less_cancel_left [of _ 0] by simp
    2.74 -
    2.75 -lemma less_add_same_cancel2 [simp]: "a < b + a \<longleftrightarrow> 0 < b"
    2.76 -  using add_less_cancel_right [of 0] by simp
    2.77 -
    2.78 -lemma add_le_same_cancel1 [simp]: "b + a \<le> b \<longleftrightarrow> a \<le> 0"
    2.79 -  using add_le_cancel_left [of _ _ 0] by simp
    2.80 -
    2.81 -lemma add_le_same_cancel2 [simp]: "a + b \<le> b \<longleftrightarrow> a \<le> 0"
    2.82 -  using add_le_cancel_right [of _ _ 0] by simp
    2.83 -
    2.84 -lemma le_add_same_cancel1 [simp]: "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
    2.85 -  using add_le_cancel_left [of _ 0] by simp
    2.86 -
    2.87 -lemma le_add_same_cancel2 [simp]: "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
    2.88 -  using add_le_cancel_right [of 0] by simp
    2.89 -
    2.90  lemma max_diff_distrib_left: "max x y - z = max (x - z) (y - z)"
    2.91    using max_add_distrib_left [of x y "- z"] by simp
    2.92  
     3.1 --- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Tue Jul 12 11:51:05 2016 +0200
     3.2 +++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Tue Jul 12 13:55:35 2016 +0200
     3.3 @@ -806,6 +806,7 @@
     3.4  by (intro_classes, transfer, rule add_le_imp_le_left)
     3.5  
     3.6  instance star :: (ordered_comm_monoid_add) ordered_comm_monoid_add ..
     3.7 +instance star :: (ordered_ab_semigroup_monoid_add_imp_le) ordered_ab_semigroup_monoid_add_imp_le ..
     3.8  instance star :: (ordered_cancel_comm_monoid_add) ordered_cancel_comm_monoid_add ..
     3.9  instance star :: (ordered_ab_group_add) ordered_ab_group_add ..
    3.10  
     4.1 --- a/src/HOL/Rings.thy	Tue Jul 12 11:51:05 2016 +0200
     4.2 +++ b/src/HOL/Rings.thy	Tue Jul 12 13:55:35 2016 +0200
     4.3 @@ -1292,36 +1292,14 @@
     4.4  
     4.5  subclass ordered_cancel_comm_monoid_add ..
     4.6  
     4.7 +subclass ordered_ab_semigroup_monoid_add_imp_le ..
     4.8 +
     4.9  lemma mult_left_less_imp_less: "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
    4.10    by (force simp add: mult_left_mono not_le [symmetric])
    4.11  
    4.12  lemma mult_right_less_imp_less: "a * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
    4.13    by (force simp add: mult_right_mono not_le [symmetric])
    4.14  
    4.15 -lemma less_eq_add_cancel_left_greater_eq_zero [simp]: "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
    4.16 -  using add_le_cancel_left [of a 0 b] by simp
    4.17 -
    4.18 -lemma less_eq_add_cancel_left_less_eq_zero [simp]: "a + b \<le> a \<longleftrightarrow> b \<le> 0"
    4.19 -  using add_le_cancel_left [of a b 0] by simp
    4.20 -
    4.21 -lemma less_eq_add_cancel_right_greater_eq_zero [simp]: "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
    4.22 -  using add_le_cancel_right [of 0 a b] by simp
    4.23 -
    4.24 -lemma less_eq_add_cancel_right_less_eq_zero [simp]: "b + a \<le> a \<longleftrightarrow> b \<le> 0"
    4.25 -  using add_le_cancel_right [of b a 0] by simp
    4.26 -
    4.27 -lemma less_add_cancel_left_greater_zero [simp]: "a < a + b \<longleftrightarrow> 0 < b"
    4.28 -  using add_less_cancel_left [of a 0 b] by simp
    4.29 -
    4.30 -lemma less_add_cancel_left_less_zero [simp]: "a + b < a \<longleftrightarrow> b < 0"
    4.31 -  using add_less_cancel_left [of a b 0] by simp
    4.32 -
    4.33 -lemma less_add_cancel_right_greater_zero [simp]: "a < b + a \<longleftrightarrow> 0 < b"
    4.34 -  using add_less_cancel_right [of 0 a b] by simp
    4.35 -
    4.36 -lemma less_add_cancel_right_less_zero [simp]: "b + a < a \<longleftrightarrow> b < 0"
    4.37 -  using add_less_cancel_right [of b a 0] by simp
    4.38 -
    4.39  end
    4.40  
    4.41  class linordered_semiring_1 = linordered_semiring + semiring_1