# Theory Groups

```(*  Title:      HOL/Groups.thy
Author:     Gertrud Bauer
Author:     Steven Obua
Author:     Lawrence C Paulson
Author:     Markus Wenzel
*)

section ‹Groups, also combined with orderings›

theory Groups
imports Orderings
begin

subsection ‹Dynamic facts›

named_theorems ac_simps "associativity and commutativity simplification rules"
and algebra_simps "algebra simplification rules for rings"
and algebra_split_simps "algebra simplification rules for rings, with potential goal splitting"
and field_simps "algebra simplification rules for fields"
and field_split_simps "algebra simplification rules for fields, with potential goal splitting"

text ‹
The rewrites accumulated in ‹algebra_simps› deal with the classical
algebraic structures of groups, rings and family. They simplify terms by
multiplying everything out (in case of a ring) and bringing sums and
products into a canonical form (by ordered rewriting). As a result it
decides group and ring equalities but also helps with inequalities.

Of course it also works for fields, but it knows nothing about
multiplicative inverses or division. This is catered for by ‹field_simps›.

Facts in ‹field_simps› multiply with denominators in (in)equations if they
can be proved to be non-zero (for equations) or positive/negative (for
inequalities). Can be too aggressive and is therefore separate from the more
benign ‹algebra_simps›.

Collections ‹algebra_split_simps› and ‹field_split_simps›
correspond to ‹algebra_simps› and ‹field_simps›
but contain more aggresive rules that may lead to goal splitting.
›

subsection ‹Abstract structures›

text ‹
These locales provide basic structures for interpretation into bigger
structures; extensions require careful thinking, otherwise undesired effects
may occur due to interpretation.
›

locale semigroup =
fixes f :: "'a ⇒ 'a ⇒ 'a"  (infixl "❙*" 70)
assumes assoc [ac_simps]: "a ❙* b ❙* c = a ❙* (b ❙* c)"

locale abel_semigroup = semigroup +
assumes commute [ac_simps]: "a ❙* b = b ❙* a"
begin

lemma left_commute [ac_simps]: "b ❙* (a ❙* c) = a ❙* (b ❙* c)"
proof -
have "(b ❙* a) ❙* c = (a ❙* b) ❙* c"
by (simp only: commute)
then show ?thesis
by (simp only: assoc)
qed

end

locale monoid = semigroup +
fixes z :: 'a ("❙1")
assumes left_neutral [simp]: "❙1 ❙* a = a"
assumes right_neutral [simp]: "a ❙* ❙1 = a"

locale comm_monoid = abel_semigroup +
fixes z :: 'a ("❙1")
assumes comm_neutral: "a ❙* ❙1 = a"
begin

sublocale monoid
by standard (simp_all add: commute comm_neutral)

end

locale group = semigroup +
fixes z :: 'a ("❙1")
fixes inverse :: "'a ⇒ 'a"
assumes group_left_neutral: "❙1 ❙* a = a"
assumes left_inverse [simp]:  "inverse a ❙* a = ❙1"
begin

lemma left_cancel: "a ❙* b = a ❙* c ⟷ b = c"
proof
assume "a ❙* b = a ❙* c"
then have "inverse a ❙* (a ❙* b) = inverse a ❙* (a ❙* c)" by simp
then have "(inverse a ❙* a) ❙* b = (inverse a ❙* a) ❙* c"
by (simp only: assoc)
then show "b = c" by (simp add: group_left_neutral)
qed simp

sublocale monoid
proof
fix a
have "inverse a ❙* a = ❙1" by simp
then have "inverse a ❙* (a ❙* ❙1) = inverse a ❙* a"
by (simp add: group_left_neutral assoc [symmetric])
with left_cancel show "a ❙* ❙1 = a"
by (simp only: left_cancel)
qed (fact group_left_neutral)

lemma inverse_unique:
assumes "a ❙* b = ❙1"
shows "inverse a = b"
proof -
from assms have "inverse a ❙* (a ❙* b) = inverse a"
by simp
then show ?thesis
qed

lemma inverse_neutral [simp]: "inverse ❙1 = ❙1"
by (rule inverse_unique) simp

lemma inverse_inverse [simp]: "inverse (inverse a) = a"
by (rule inverse_unique) simp

lemma right_inverse [simp]: "a ❙* inverse a = ❙1"
proof -
have "a ❙* inverse a = inverse (inverse a) ❙* inverse a"
by simp
also have "… = ❙1"
by (rule left_inverse)
then show ?thesis by simp
qed

lemma inverse_distrib_swap: "inverse (a ❙* b) = inverse b ❙* inverse a"
proof (rule inverse_unique)
have "a ❙* b ❙* (inverse b ❙* inverse a) =
a ❙* (b ❙* inverse b) ❙* inverse a"
by (simp only: assoc)
also have "… = ❙1"
by simp
finally show "a ❙* b ❙* (inverse b ❙* inverse a) = ❙1" .
qed

lemma right_cancel: "b ❙* a = c ❙* a ⟷ b = c"
proof
assume "b ❙* a = c ❙* a"
then have "b ❙* a ❙* inverse a= c ❙* a ❙* inverse a"
by simp
then show "b = c"
qed simp

end

subsection ‹Generic operations›

class zero =
fixes zero :: 'a  ("0")

class one =
fixes one  :: 'a  ("1")

hide_const (open) zero one

lemma Let_0 [simp]: "Let 0 f = f 0"
unfolding Let_def ..

lemma Let_1 [simp]: "Let 1 f = f 1"
unfolding Let_def ..

setup ‹
(fn Const(\<^const_name>‹Groups.zero›, _) => true
| Const(\<^const_name>‹Groups.one›, _) => true
| _ => false)
›

simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc

typed_print_translation ‹
let
fun tr' c = (c, fn ctxt => fn T => fn ts =>
if null ts andalso Printer.type_emphasis ctxt T then
Syntax.const \<^syntax_const>‹_constrain› \$ Syntax.const c \$
Syntax_Phases.term_of_typ ctxt T
else raise Match);
in map tr' [\<^const_syntax>‹Groups.one›, \<^const_syntax>‹Groups.zero›] end
› ― ‹show types that are presumably too general›

class plus =
fixes plus :: "'a ⇒ 'a ⇒ 'a"  (infixl "+" 65)

class minus =
fixes minus :: "'a ⇒ 'a ⇒ 'a"  (infixl "-" 65)

class uminus =
fixes uminus :: "'a ⇒ 'a"  ("- _" [81] 80)

class times =
fixes times :: "'a ⇒ 'a ⇒ 'a"  (infixl "*" 70)

subsection ‹Semigroups and Monoids›

assumes add_assoc [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
"(a + b) + c = a + (b + c)"
begin

end

assumes add_commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
"a + b = b + a"
begin

declare add.left_commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps]

end

class semigroup_mult = times +
assumes mult_assoc [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
"(a * b) * c = a * (b * c)"
begin

sublocale mult: semigroup times
by standard (fact mult_assoc)

end

hide_fact mult_assoc

class ab_semigroup_mult = semigroup_mult +
assumes mult_commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
"a * b = b * a"
begin

sublocale mult: abel_semigroup times
by standard (fact mult_commute)

declare mult.left_commute [algebra_simps, algebra_split_simps, field_simps, field_split_simps]

lemmas mult_ac = mult.assoc mult.commute mult.left_commute

end

hide_fact mult_commute

lemmas mult_ac = mult.assoc mult.commute mult.left_commute

assumes add_0_left: "0 + a = a"
and add_0_right: "a + 0 = a"
begin

end

lemma zero_reorient: "0 = x ⟷ x = 0"
by (fact eq_commute)

assumes add_0: "0 + a = a"
begin

end

class monoid_mult = one + semigroup_mult +
assumes mult_1_left: "1 * a  = a"
and mult_1_right: "a * 1 = a"
begin

sublocale mult: monoid times 1
by standard (fact mult_1_left mult_1_right)+

end

lemma one_reorient: "1 = x ⟷ x = 1"
by (fact eq_commute)

class comm_monoid_mult = one + ab_semigroup_mult +
assumes mult_1: "1 * a = a"
begin

subclass monoid_mult
by standard (simp_all add: mult_1 mult.commute [of _ 1])

sublocale mult: comm_monoid times 1

end

assumes add_left_imp_eq: "a + b = a + c ⟹ b = c"
assumes add_right_imp_eq: "b + a = c + a ⟹ b = c"
begin

lemma add_left_cancel [simp]: "a + b = a + c ⟷ b = c"

lemma add_right_cancel [simp]: "b + a = c + a ⟷ b = c"

end

assumes add_diff_cancel_left' [simp]: "(a + b) - a = b"
assumes diff_diff_add [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
"a - b - c = a - (b + c)"
begin

lemma add_diff_cancel_right' [simp]: "(a + b) - b = a"

proof
fix a b c :: 'a
assume "a + b = a + c"
then have "a + b - a = a + c - a"
by simp
then show "b = c"
by simp
next
fix a b c :: 'a
assume "b + a = c + a"
then have "b + a - a = c + a - a"
by simp
then show "b = c"
by simp
qed

lemma add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b"

lemma add_diff_cancel_right [simp]: "(a + c) - (b + c) = a - b"

lemma diff_right_commute: "a - c - b = a - b - c"

end

begin

lemma diff_zero [simp]: "a - 0 = a"
using add_diff_cancel_right' [of a 0] by simp

lemma diff_cancel [simp]: "a - a = 0"
proof -
have "(a + 0) - (a + 0) = 0"
then show ?thesis by simp
qed

assumes "c + b = a"
shows "c = a - b"
proof -
from assms have "(b + c) - (b + 0) = a - b"
then show "c = a - b" by simp
qed

lemma add_cancel_right_right [simp]: "a = a + b ⟷ b = 0"
(is "?P ⟷ ?Q")
proof
assume ?Q
then show ?P by simp
next
assume ?P
then have "a - a = a + b - a" by simp
then show ?Q by simp
qed

lemma add_cancel_right_left [simp]: "a = b + a ⟷ b = 0"

lemma add_cancel_left_right [simp]: "a + b = a ⟷ b = 0"
by (auto dest: sym)

lemma add_cancel_left_left [simp]: "b + a = a ⟷ b = 0"
by (auto dest: sym)

end

assumes zero_diff [simp]: "0 - a = 0"
begin

lemma diff_add_zero [simp]: "a - (a + b) = 0"
proof -
have "a - (a + b) = (a + 0) - (a + b)"
by simp
also have "… = 0"
finally show ?thesis .
qed

end

subsection ‹Groups›

assumes left_minus: "- a + a = 0"
assumes add_uminus_conv_diff [simp]: "a + (- b) = a - b"
begin

lemma diff_conv_add_uminus: "a - b = a + (- b)"
by simp

sublocale add: group plus 0 uminus

lemma minus_unique: "a + b = 0 ⟹ - a = b"

lemma minus_zero: "- 0 = 0"

lemma minus_minus: "- (- a) = a"

lemma right_minus: "a + - a = 0"

lemma diff_self [simp]: "a - a = 0"
using right_minus [of a] by simp

lemma minus_add_cancel [simp]: "- a + (a + b) = b"

lemma add_minus_cancel [simp]: "a + (- a + b) = b"

lemma diff_add_cancel [simp]: "a - b + b = a"

lemma add_diff_cancel [simp]: "a + b - b = a"

lemma minus_add: "- (a + b) = - b + - a"

lemma right_minus_eq [simp]: "a - b = 0 ⟷ a = b"
proof
assume "a - b = 0"
have "a = (a - b) + b" by (simp add: add.assoc)
also have "… = b" using ‹a - b = 0› by simp
finally show "a = b" .
next
assume "a = b"
then show "a - b = 0" by simp
qed

lemma eq_iff_diff_eq_0: "a = b ⟷ a - b = 0"
by (fact right_minus_eq [symmetric])

lemma diff_0 [simp]: "0 - a = - a"

lemma diff_0_right [simp]: "a - 0 = a"

lemma diff_minus_eq_add [simp]: "a - - b = a + b"

lemma neg_equal_iff_equal [simp]: "- a = - b ⟷ a = b"
proof
assume "- a = - b"
then have "- (- a) = - (- b)" by simp
then show "a = b" by simp
next
assume "a = b"
then show "- a = - b" by simp
qed

lemma neg_equal_0_iff_equal [simp]: "- a = 0 ⟷ a = 0"
by (subst neg_equal_iff_equal [symmetric]) simp

lemma neg_0_equal_iff_equal [simp]: "0 = - a ⟷ 0 = a"
by (subst neg_equal_iff_equal [symmetric]) simp

text ‹The next two equations can make the simplifier loop!›

lemma equation_minus_iff: "a = - b ⟷ b = - a"
proof -
have "- (- a) = - b ⟷ - a = b"
by (rule neg_equal_iff_equal)
then show ?thesis
qed

lemma minus_equation_iff: "- a = b ⟷ - b = a"
proof -
have "- a = - (- b) ⟷ a = -b"
by (rule neg_equal_iff_equal)
then show ?thesis
qed

lemma eq_neg_iff_add_eq_0: "a = - b ⟷ a + b = 0"
proof
assume "a = - b"
then show "a + b = 0" by simp
next
assume "a + b = 0"
moreover have "a + (b + - b) = (a + b) + - b"
ultimately show "a = - b"
by simp
qed

lemma add_eq_0_iff2: "a + b = 0 ⟷ a = - b"

lemma neg_eq_iff_add_eq_0: "- a = b ⟷ a + b = 0"

lemma add_eq_0_iff: "a + b = 0 ⟷ b = - a"

lemma minus_diff_eq [simp]: "- (a - b) = b - a"

lemma add_diff_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
"a + (b - c) = (a + b) - c"

lemma diff_add_eq_diff_diff_swap: "a - (b + c) = a - c - b"

lemma diff_eq_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
"a - b = c ⟷ a = c + b"
by auto

lemma eq_diff_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
"a = c - b ⟷ a + b = c"
by auto

lemma diff_diff_eq2 [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
"a - (b - c) = (a + c) - b"

lemma diff_eq_diff_eq: "a - b = c - d ⟹ a = b ⟷ c = d"
by (simp only: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])

end

assumes ab_left_minus: "- a + a = 0"
assumes ab_diff_conv_add_uminus: "a - b = a + (- b)"
begin

proof
fix a b c :: 'a
have "b + a - a = b"
by simp
then show "a + b - a = b"
show "a - b - c = a - (b + c)"
qed

lemma uminus_add_conv_diff [simp]: "- a + b = b - a"

lemma minus_add_distrib [simp]: "- (a + b) = - a + - b"

lemma diff_add_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
"(a - b) + c = (a + c) - b"

lemma minus_diff_commute:
"- b - a = - a - b"

end

subsection ‹(Partially) Ordered Groups›

text ‹
The theory of partially ordered groups is taken from the books:

▪ ∗‹Lattice Theory› by Garret Birkhoff, American Mathematical Society, 1979
▪ ∗‹Partially Ordered Algebraic Systems›, Pergamon Press, 1963

Most of the used notions can also be looked up in
▪ 🌐‹http://www.mathworld.com› by Eric Weisstein et. al.
▪ ∗‹Algebra I› by van der Waerden, Springer
›

assumes add_left_mono: "a ≤ b ⟹ c + a ≤ c + b"
begin

lemma add_right_mono: "a ≤ b ⟹ a + c ≤ b + c"

text ‹non-strict, in both arguments›
lemma add_mono: "a ≤ b ⟹ c ≤ d ⟹ a + c ≤ b + d"

end

shows "mono ((+) a)"

text ‹Strict monotonicity in both arguments›
assumes add_strict_mono: "a < b ⟹ c < d ⟹ a + c < b + d"

begin

lemma add_strict_left_mono: "a < b ⟹ c + a < c + b"

lemma add_strict_right_mono: "a < b ⟹ a + c < b + c"

proof
show "⋀a b c d. ⟦a < b; c < d⟧ ⟹ a + c < b + d"
qed

lemma add_less_le_mono: "a < b ⟹ c ≤ d ⟹ a + c < b + d"

lemma add_le_less_mono: "a ≤ b ⟹ c < d ⟹ a + c < b + d"

end

assumes add_le_imp_le_left: "c + a ≤ c + b ⟹ a ≤ b"
begin

assumes less: "c + a < c + b"
shows "a < b"
proof -
from less have le: "c + a ≤ c + b"
have "a ≤ b"
moreover have "a ≠ b"
proof (rule ccontr)
assume "¬ ?thesis"
then have "a = b" by simp
then have "c + a = c + b" by simp
with less show "False" by simp
qed
ultimately show "a < b"
qed

lemma add_less_imp_less_right: "a + c < b + c ⟹ a < b"

lemma add_less_cancel_left [simp]: "c + a < c + b ⟷ a < b"

lemma add_less_cancel_right [simp]: "a + c < b + c ⟷ a < b"

lemma add_le_cancel_left [simp]: "c + a ≤ c + b ⟷ a ≤ b"

lemma add_le_cancel_right [simp]: "a + c ≤ b + c ⟷ a ≤ b"

lemma add_le_imp_le_right: "a + c ≤ b + c ⟹ a ≤ b"
by simp

lemma max_add_distrib_left: "max x y + z = max (x + z) (y + z)"
unfolding max_def by auto

lemma min_add_distrib_left: "min x y + z = min (x + z) (y + z)"
unfolding min_def by auto

lemma max_add_distrib_right: "x + max y z = max (x + y) (x + z)"
unfolding max_def by auto

lemma min_add_distrib_right: "x + min y z = min (x + y) (x + z)"
unfolding min_def by auto

end

subsection ‹Support for reasoning about signs›

begin

lemma add_nonneg_nonneg [simp]: "0 ≤ a ⟹ 0 ≤ b ⟹ 0 ≤ a + b"
using add_mono[of 0 a 0 b] by simp

lemma add_nonpos_nonpos: "a ≤ 0 ⟹ b ≤ 0 ⟹ a + b ≤ 0"
using add_mono[of a 0 b 0] by simp

lemma add_nonneg_eq_0_iff: "0 ≤ x ⟹ 0 ≤ y ⟹ x + y = 0 ⟷ x = 0 ∧ y = 0"

lemma add_nonpos_eq_0_iff: "x ≤ 0 ⟹ y ≤ 0 ⟹ x + y = 0 ⟷ x = 0 ∧ y = 0"

lemma add_increasing: "0 ≤ a ⟹ b ≤ c ⟹ b ≤ a + c"
using add_mono [of 0 a b c] by simp

lemma add_increasing2: "0 ≤ c ⟹ b ≤ a ⟹ b ≤ a + c"

lemma add_decreasing: "a ≤ 0 ⟹ c ≤ b ⟹ a + c ≤ b"
using add_mono [of a 0 c b] by simp

lemma add_decreasing2: "c ≤ 0 ⟹ a ≤ b ⟹ a + c ≤ b"
using add_mono[of a b c 0] by simp

lemma add_pos_nonneg: "0 < a ⟹ 0 ≤ b ⟹ 0 < a + b"

lemma add_pos_pos: "0 < a ⟹ 0 < b ⟹ 0 < a + b"

lemma add_nonneg_pos: "0 ≤ a ⟹ 0 < b ⟹ 0 < a + b"

lemma add_neg_nonpos: "a < 0 ⟹ b ≤ 0 ⟹ a + b < 0"

lemma add_neg_neg: "a < 0 ⟹ b < 0 ⟹ a + b < 0"

lemma add_nonpos_neg: "a ≤ 0 ⟹ b < 0 ⟹ a + b < 0"

end

begin

lemma pos_add_strict: "0 < a ⟹ b < c ⟹ b < a + c"
using add_strict_mono [of 0 a b c] by simp

end

begin

lemma add_strict_increasing: "0 < a ⟹ b ≤ c ⟹ b < a + c"
using add_less_le_mono [of 0 a b c] by simp

lemma add_strict_increasing2: "0 ≤ a ⟹ b < c ⟹ b < a + c"
using add_le_less_mono [of 0 a b c] by simp

end

begin

lemma add_less_same_cancel1 [simp]: "b + a < b ⟷ a < 0"
using add_less_cancel_left [of _ _ 0] by simp

lemma add_less_same_cancel2 [simp]: "a + b < b ⟷ a < 0"
using add_less_cancel_right [of _ _ 0] by simp

lemma less_add_same_cancel1 [simp]: "a < a + b ⟷ 0 < b"
using add_less_cancel_left [of _ 0] by simp

lemma less_add_same_cancel2 [simp]: "a < b + a ⟷ 0 < b"
using add_less_cancel_right [of 0] by simp

lemma add_le_same_cancel1 [simp]: "b + a ≤ b ⟷ a ≤ 0"
using add_le_cancel_left [of _ _ 0] by simp

lemma add_le_same_cancel2 [simp]: "a + b ≤ b ⟷ a ≤ 0"
using add_le_cancel_right [of _ _ 0] by simp

lemma le_add_same_cancel1 [simp]: "a ≤ a + b ⟷ 0 ≤ b"
using add_le_cancel_left [of _ 0] by simp

lemma le_add_same_cancel2 [simp]: "a ≤ b + a ⟷ 0 ≤ b"
using add_le_cancel_right [of 0] by simp

by standard auto

by standard

end

begin

proof
fix a b c :: 'a
assume "c + a ≤ c + b"
then have "(-c) + (c + a) ≤ (-c) + (c + b)"
then have "((-c) + c) + a ≤ ((-c) + c) + b"
then show "a ≤ b" by simp
qed

lemma max_diff_distrib_left: "max x y - z = max (x - z) (y - z)"
using max_add_distrib_left [of x y "- z"] by simp

lemma min_diff_distrib_left: "min x y - z = min (x - z) (y - z)"
using min_add_distrib_left [of x y "- z"] by simp

lemma le_imp_neg_le:
assumes "a ≤ b"
shows "- b ≤ - a"
proof -
from assms have "- a + a ≤ - a + b"
then have "0 ≤ - a + b"
by simp
then have "0 + (- b) ≤ (- a + b) + (- b)"
then show ?thesis
qed

lemma neg_le_iff_le [simp]: "- b ≤ - a ⟷ a ≤ b"
proof
assume "- b ≤ - a"
then have "- (- a) ≤ - (- b)"
by (rule le_imp_neg_le)
then show "a ≤ b"
by simp
next
assume "a ≤ b"
then show "- b ≤ - a"
by (rule le_imp_neg_le)
qed

lemma neg_le_0_iff_le [simp]: "- a ≤ 0 ⟷ 0 ≤ a"
by (subst neg_le_iff_le [symmetric]) simp

lemma neg_0_le_iff_le [simp]: "0 ≤ - a ⟷ a ≤ 0"
by (subst neg_le_iff_le [symmetric]) simp

lemma neg_less_iff_less [simp]: "- b < - a ⟷ a < b"

lemma neg_less_0_iff_less [simp]: "- a < 0 ⟷ 0 < a"
by (subst neg_less_iff_less [symmetric]) simp

lemma neg_0_less_iff_less [simp]: "0 < - a ⟷ a < 0"
by (subst neg_less_iff_less [symmetric]) simp

text ‹The next several equations can make the simplifier loop!›

lemma less_minus_iff: "a < - b ⟷ b < - a"
proof -
have "- (- a) < - b ⟷ b < - a"
by (rule neg_less_iff_less)
then show ?thesis by simp
qed

lemma minus_less_iff: "- a < b ⟷ - b < a"
proof -
have "- a < - (- b) ⟷ - b < a"
by (rule neg_less_iff_less)
then show ?thesis by simp
qed

lemma le_minus_iff: "a ≤ - b ⟷ b ≤ - a"
by (auto simp: order.order_iff_strict less_minus_iff)

lemma minus_le_iff: "- a ≤ b ⟷ - b ≤ a"
by (auto simp add: le_less minus_less_iff)

lemma diff_less_0_iff_less [simp]: "a - b < 0 ⟷ a < b"
proof -
have "a - b < 0 ⟷ a + (- b) < b + (- b)"
by simp
also have "… ⟷ a < b"
finally show ?thesis .
qed

lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]

lemma diff_less_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
"a - b < c ⟷ a < c + b"
proof (subst less_iff_diff_less_0 [of a])
show "(a - b < c) = (a - (c + b) < 0)"
by (simp add: algebra_simps less_iff_diff_less_0 [of _ c])
qed

lemma less_diff_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
"a < c - b ⟷ a + b < c"
proof (subst less_iff_diff_less_0 [of "a + b"])
show "(a < c - b) = (a + b - c < 0)"
by (simp add: algebra_simps less_iff_diff_less_0 [of a])
qed

lemma diff_gt_0_iff_gt [simp]: "a - b > 0 ⟷ a > b"

lemma diff_le_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
"a - b ≤ c ⟷ a ≤ c + b"
by (auto simp add: le_less diff_less_eq )

lemma le_diff_eq [algebra_simps, algebra_split_simps, field_simps, field_split_simps]:
"a ≤ c - b ⟷ a + b ≤ c"
by (auto simp add: le_less less_diff_eq)

lemma diff_le_0_iff_le [simp]: "a - b ≤ 0 ⟷ a ≤ b"

lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]

lemma diff_ge_0_iff_ge [simp]: "a - b ≥ 0 ⟷ a ≥ b"

lemma diff_eq_diff_less: "a - b = c - d ⟹ a < b ⟷ c < d"
by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])

lemma diff_eq_diff_less_eq: "a - b = c - d ⟹ a ≤ b ⟷ c ≤ d"
by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])

lemma diff_mono: "a ≤ b ⟹ d ≤ c ⟹ a - c ≤ b - d"

lemma diff_left_mono: "b ≤ a ⟹ c - a ≤ c - b"

lemma diff_right_mono: "a ≤ b ⟹ a - c ≤ b - c"

lemma diff_strict_mono: "a < b ⟹ d < c ⟹ a - c < b - d"

lemma diff_strict_left_mono: "b < a ⟹ c - a < c - b"

lemma diff_strict_right_mono: "a < b ⟹ a - c < b - c"

end

locale group_cancel
begin

lemma add1: "(A::'a::comm_monoid_add) ≡ k + a ⟹ A + b ≡ k + (a + b)"
by (simp only: ac_simps)

lemma add2: "(B::'a::comm_monoid_add) ≡ k + b ⟹ a + B ≡ k + (a + b)"
by (simp only: ac_simps)

lemma sub1: "(A::'a::ab_group_add) ≡ k + a ⟹ A - b ≡ k + (a - b)"

lemma sub2: "(B::'a::ab_group_add) ≡ k + b ⟹ a - B ≡ - k + (a - b)"

lemma neg1: "(A::'a::ab_group_add) ≡ k + a ⟹ - A ≡ - k + - a"

lemma rule0: "(a::'a::comm_monoid_add) ≡ a + 0"

end

ML_file ‹Tools/group_cancel.ML›

‹fn phi => fn ss => try Group_Cancel.cancel_add_conv›

simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") =
‹fn phi => fn ss => try Group_Cancel.cancel_diff_conv›

simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") =
‹fn phi => fn ss => try Group_Cancel.cancel_eq_conv›

simproc_setup group_cancel_le ("a ≤ (b::'a::ordered_ab_group_add)") =
‹fn phi => fn ss => try Group_Cancel.cancel_le_conv›

simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") =
‹fn phi => fn ss => try Group_Cancel.cancel_less_conv›

begin

proof
fix a b c :: 'a
assume le1: "c + a ≤ c + b"
show "a ≤ b"
proof (rule ccontr)
assume *: "¬ ?thesis"
then have "b ≤ a" by (simp add: linorder_not_le)
then have "c + b ≤ c + a" by (rule add_left_mono)
then have "c + a = c + b"
using le1 by (iprover intro: order.antisym)
then have "a = b"
by simp
with * show False
qed
qed

end

begin

lemma equal_neg_zero [simp]: "a = - a ⟷ a = 0"
proof
assume "a = 0"
then show "a = - a" by simp
next
assume A: "a = - a"
show "a = 0"
proof (cases "0 ≤ a")
case True
with A have "0 ≤ - a" by auto
with le_minus_iff have "a ≤ 0" by simp
with True show ?thesis by (auto intro: order_trans)
next
case False
then have B: "a ≤ 0" by auto
with A have "- a ≤ 0" by auto
with B show ?thesis by (auto intro: order_trans)
qed
qed

lemma neg_equal_zero [simp]: "- a = a ⟷ a = 0"
by (auto dest: sym)

lemma neg_less_eq_nonneg [simp]: "- a ≤ a ⟷ 0 ≤ a"
proof
assume *: "- a ≤ a"
show "0 ≤ a"
proof (rule classical)
assume "¬ ?thesis"
then have "a < 0" by auto
with * have "- a < 0" by (rule le_less_trans)
then show ?thesis by auto
qed
next
assume *: "0 ≤ a"
then have "- a ≤ 0" by (simp add: minus_le_iff)
from this * show "- a ≤ a" by (rule order_trans)
qed

lemma neg_less_pos [simp]: "- a < a ⟷ 0 < a"

lemma less_eq_neg_nonpos [simp]: "a ≤ - a ⟷ a ≤ 0"
using neg_less_eq_nonneg [of "- a"] by simp

lemma less_neg_neg [simp]: "a < - a ⟷ a < 0"
using neg_less_pos [of "- a"] by simp

lemma double_zero [simp]: "a + a = 0 ⟷ a = 0"
proof
assume "a + a = 0"
then have a: "- a = a" by (rule minus_unique)
then show "a = 0" by (simp only: neg_equal_zero)
next
assume "a = 0"
then show "a + a = 0" by simp
qed

lemma double_zero_sym [simp]: "0 = a + a ⟷ a = 0"
using double_zero [of a] by (simp only: eq_commute)

lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a ⟷ 0 < a"
proof
assume "0 < a + a"
then have "0 - a < a" by (simp only: diff_less_eq)
then have "- a < a" by simp
then show "0 < a" by simp
next
assume "0 < a"
with this have "0 + 0 < a + a"
then show "0 < a + a" by simp
qed

lemma zero_le_double_add_iff_zero_le_single_add [simp]: "0 ≤ a + a ⟷ 0 ≤ a"

lemma double_add_less_zero_iff_single_add_less_zero [simp]: "a + a < 0 ⟷ a < 0"
proof -
have "¬ a + a < 0 ⟷ ¬ a < 0"
then show ?thesis by simp
qed

lemma double_add_le_zero_iff_single_add_le_zero [simp]: "a + a ≤ 0 ⟷ a ≤ 0"
proof -
have "¬ a + a ≤ 0 ⟷ ¬ a ≤ 0"
then show ?thesis by simp
qed

lemma minus_max_eq_min: "- max x y = min (- x) (- y)"
by (auto simp add: max_def min_def)

lemma minus_min_eq_max: "- min x y = max (- x) (- y)"
by (auto simp add: max_def min_def)

end

class abs =
fixes abs :: "'a ⇒ 'a"  ("¦_¦")

class sgn =
fixes sgn :: "'a ⇒ 'a"

assumes abs_ge_zero [simp]: "¦a¦ ≥ 0"
and abs_ge_self: "a ≤ ¦a¦"
and abs_leI: "a ≤ b ⟹ - a ≤ b ⟹ ¦a¦ ≤ b"
and abs_minus_cancel [simp]: "¦-a¦ = ¦a¦"
and abs_triangle_ineq: "¦a + b¦ ≤ ¦a¦ + ¦b¦"
begin

lemma abs_minus_le_zero: "- ¦a¦ ≤ 0"
unfolding neg_le_0_iff_le by simp

lemma abs_of_nonneg [simp]:
assumes nonneg: "0 ≤ a"
shows "¦a¦ = a"
proof (rule order.antisym)
show "a ≤ ¦a¦" by (rule abs_ge_self)
from nonneg le_imp_neg_le have "- a ≤ 0" by simp
from this nonneg have "- a ≤ a" by (rule order_trans)
then show "¦a¦ ≤ a" by (auto intro: abs_leI)
qed

lemma abs_idempotent [simp]: "¦¦a¦¦ = ¦a¦"
by (rule order.antisym) (auto intro!: abs_ge_self abs_leI order_trans [of "- ¦a¦" 0 "¦a¦"])

lemma abs_eq_0 [simp]: "¦a¦ = 0 ⟷ a = 0"
proof -
have "¦a¦ = 0 ⟹ a = 0"
proof (rule order.antisym)
assume zero: "¦a¦ = 0"
with abs_ge_self show "a ≤ 0" by auto
from zero have "¦-a¦ = 0" by simp
with abs_ge_self [of "- a"] have "- a ≤ 0" by auto
with neg_le_0_iff_le show "0 ≤ a" by auto
qed
then show ?thesis by auto
qed

lemma abs_zero [simp]: "¦0¦ = 0"
by simp

lemma abs_0_eq [simp]: "0 = ¦a¦ ⟷ a = 0"
proof -
have "0 = ¦a¦ ⟷ ¦a¦ = 0" by (simp only: eq_ac)
then show ?thesis by simp
qed

lemma abs_le_zero_iff [simp]: "¦a¦ ≤ 0 ⟷ a = 0"
proof
assume "¦a¦ ≤ 0"
then have "¦a¦ = 0" by (rule order.antisym) simp
then show "a = 0" by simp
next
assume "a = 0"
then show "¦a¦ ≤ 0" by simp
qed

lemma abs_le_self_iff [simp]: "¦a¦ ≤ a ⟷ 0 ≤ a"
proof -
have "0 ≤ ¦a¦"
using abs_ge_zero by blast
then have "¦a¦ ≤ a ⟹ 0 ≤ a"
using order.trans by blast
then show ?thesis
using abs_of_nonneg eq_refl by blast
qed

lemma zero_less_abs_iff [simp]: "0 < ¦a¦ ⟷ a ≠ 0"

lemma abs_not_less_zero [simp]: "¬ ¦a¦ < 0"
proof -
have "x ≤ y ⟹ ¬ y < x" for x y by auto
then show ?thesis by simp
qed

lemma abs_ge_minus_self: "- a ≤ ¦a¦"
proof -
have "- a ≤ ¦-a¦" by (rule abs_ge_self)
then show ?thesis by simp
qed

lemma abs_minus_commute: "¦a - b¦ = ¦b - a¦"
proof -
have "¦a - b¦ = ¦- (a - b)¦"
by (simp only: abs_minus_cancel)
also have "… = ¦b - a¦" by simp
finally show ?thesis .
qed

lemma abs_of_pos: "0 < a ⟹ ¦a¦ = a"
by (rule abs_of_nonneg) (rule less_imp_le)

lemma abs_of_nonpos [simp]:
assumes "a ≤ 0"
shows "¦a¦ = - a"
proof -
let ?b = "- a"
have "- ?b ≤ 0 ⟹ ¦- ?b¦ = - (- ?b)"
unfolding abs_minus_cancel [of ?b]
unfolding neg_le_0_iff_le [of ?b]
unfolding minus_minus by (erule abs_of_nonneg)
then show ?thesis using assms by auto
qed

lemma abs_of_neg: "a < 0 ⟹ ¦a¦ = - a"
by (rule abs_of_nonpos) (rule less_imp_le)

lemma abs_le_D1: "¦a¦ ≤ b ⟹ a ≤ b"
using abs_ge_self by (blast intro: order_trans)

lemma abs_le_D2: "¦a¦ ≤ b ⟹ - a ≤ b"
using abs_le_D1 [of "- a"] by simp

lemma abs_le_iff: "¦a¦ ≤ b ⟷ a ≤ b ∧ - a ≤ b"
by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)

lemma abs_triangle_ineq2: "¦a¦ - ¦b¦ ≤ ¦a - b¦"
proof -
have "¦a¦ = ¦b + (a - b)¦"
then have "¦a¦ ≤ ¦b¦ + ¦a - b¦"
then show ?thesis
qed

lemma abs_triangle_ineq2_sym: "¦a¦ - ¦b¦ ≤ ¦b - a¦"
by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)

lemma abs_triangle_ineq3: "¦¦a¦ - ¦b¦¦ ≤ ¦a - b¦"
by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)

lemma abs_triangle_ineq4: "¦a - b¦ ≤ ¦a¦ + ¦b¦"
proof -
have "¦a - b¦ = ¦a + - b¦"
also have "… ≤ ¦a¦ + ¦- b¦"
by (rule abs_triangle_ineq)
finally show ?thesis by simp
qed

lemma abs_diff_triangle_ineq: "¦a + b - (c + d)¦ ≤ ¦a - c¦ + ¦b - d¦"
proof -
have "¦a + b - (c + d)¦ = ¦(a - c) + (b - d)¦"
also have "… ≤ ¦a - c¦ + ¦b - d¦"
by (rule abs_triangle_ineq)
finally show ?thesis .
qed

lemma abs_add_abs [simp]: "¦¦a¦ + ¦b¦¦ = ¦a¦ + ¦b¦"
(is "?L = ?R")
proof (rule order.antisym)
show "?L ≥ ?R" by (rule abs_ge_self)
have "?L ≤ ¦¦a¦¦ + ¦¦b¦¦" by (rule abs_triangle_ineq)
also have "… = ?R" by simp
finally show "?L ≤ ?R" .
qed

end

lemma dense_eq0_I:
assumes "⋀e. 0 < e ⟹ ¦x¦ ≤ e"
shows "x = 0"
proof (cases "¦x¦ = 0")
case False
then have "¦x¦ > 0"
by simp
then obtain z where "0 < z" "z < ¦x¦"
using dense by force
then show ?thesis
using assms by (simp flip: not_less)
qed auto

lemmas mult_1 = mult_1_left (* FIXME duplicate *)
lemmas ab_left_minus = left_minus (* FIXME duplicate *)
lemmas diff_diff_eq = diff_diff_add (* FIXME duplicate *)

subsection ‹Canonically ordered monoids›

text ‹Canonically ordered monoids are never groups.›

assumes le_iff_add: "a ≤ b ⟷ (∃c. b = a + c)"
begin

lemma zero_le[simp]: "0 ≤ x"

lemma le_zero_eq[simp]: "n ≤ 0 ⟷ n = 0"
by (auto intro: order.antisym)

lemma not_less_zero[simp]: "¬ n < 0"
by (auto simp: less_le)

lemma zero_less_iff_neq_zero: "0 < n ⟷ n ≠ 0"
by (auto simp: less_le)

text ‹This theorem is useful with ‹blast››
lemma gr_zeroI: "(n = 0 ⟹ False) ⟹ 0 < n"
by (rule zero_less_iff_neq_zero[THEN iffD2]) iprover

lemma not_gr_zero[simp]: "¬ 0 < n ⟷ n = 0"

lemma gr_implies_not_zero: "m < n ⟹ n ≠ 0"
by auto

lemma add_eq_0_iff_both_eq_0[simp]: "x + y = 0 ⟷ x = 0 ∧ y = 0"

lemma zero_eq_add_iff_both_eq_0[simp]: "0 = x + y ⟷ x = 0 ∧ y = 0"
using add_eq_0_iff_both_eq_0[of x y] unfolding eq_commute[of 0] .

lemma less_eqE:
assumes ‹a ≤ b›
obtains c where ‹b = a + c›

lemma lessE:
assumes ‹a < b›
obtains c where ‹b = a + c› and ‹c ≠ 0›
proof -
from assms have ‹a ≤ b› ‹a ≠ b›
by simp_all
from ‹a ≤ b› obtain c where ‹b = a + c›
by (rule less_eqE)
moreover have ‹c ≠ 0› using ‹a ≠ b› ‹b = a + c›
by auto
ultimately show ?thesis
by (rule that)
qed

lemmas zero_order = zero_le le_zero_eq not_less_zero zero_less_iff_neq_zero not_gr_zero
― ‹This should be attributed with ‹[iff]›, but then ‹blast› fails in ‹Set›.›

end

class ordered_cancel_comm_monoid_diff =
begin

context
fixes a b :: 'a
assumes le: "a ≤ b"
begin

lemma add_diff_inverse: "a + (b - a) = b"

lemma add_diff_assoc: "c + (b - a) = c + b - a"

lemma add_diff_assoc2: "b - a + c = b + c - a"

lemma diff_add_assoc: "c + b - a = c + (b - a)"

lemma diff_add_assoc2: "b + c - a = b - a + c"

lemma diff_diff_right: "c - (b - a) = c + a - b"

lemma diff_add: "b - a + a = b"

lemma le_add_diff: "c ≤ b + c - a"

lemma le_imp_diff_is_add: "a ≤ b ⟹ b - a = c ⟷ b = c + a"

lemma le_diff_conv2: "c ≤ b - a ⟷ c + a ≤ b"
(is "?P ⟷ ?Q")
proof
assume ?P
then have "c + a ≤ b - a + a"
then show ?Q
next
assume ?Q
then have "a + c ≤ a + (b - a)"
then show ?P by simp
qed

end

end

subsection ‹Tools setup›

fixes i j k :: "'a::ordered_ab_semigroup_add"
shows "i ≤ j ∧ k ≤ l ⟹ i + k ≤ j + l"
and "i = j ∧ k ≤ l ⟹ i + k ≤ j + l"
and "i ≤ j ∧ k = l ⟹ i + k ≤ j + l"
and "i = j ∧ k = l ⟹ i + k = j + l"

fixes i j k :: "'a::ordered_cancel_ab_semigroup_add"
shows "i < j ∧ k = l ⟹ i + k < j + l"
and "i = j ∧ k < l ⟹ i + k < j + l"
and "i < j ∧ k ≤ l ⟹ i + k < j + l"
and "i ≤ j ∧ k < l ⟹ i + k < j + l"
and "i < j ∧ k < l ⟹ i + k < j + l"