src/HOL/Groups.thy
 author wenzelm Sat, 07 Apr 2012 16:41:59 +0200 changeset 47389 e8552cba702d parent 45548 3e2722d66169 child 48556 62a3fbf9d35b permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;

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

header {* Groups, also combined with orderings *}

theory Groups
imports Orderings
uses ("Tools/abel_cancel.ML")
begin

subsection {* Fact collections *}

ML {*
structure Ac_Simps = Named_Thms
(
val name = @{binding ac_simps}
val description = "associativity and commutativity simplification rules"
)
*}

setup Ac_Simps.setup

text{* The rewrites accumulated in @{text 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 @{text field_simps}. *}

ML {*
structure Algebra_Simps = Named_Thms
(
val name = @{binding algebra_simps}
val description = "algebra simplification rules"
)
*}

setup Algebra_Simps.setup

text{* Lemmas @{text field_simps} multiply with denominators in (in)equations
if they can be proved to be non-zero (for equations) or positive/negative
(for inequations). Can be too aggressive and is therefore separate from the
more benign @{text algebra_simps}. *}

ML {*
structure Field_Simps = Named_Thms
(
val name = @{binding field_simps}
val description = "algebra simplification rules for fields"
)
*}

setup Field_Simps.setup

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 \<Rightarrow> 'a \<Rightarrow> '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"

sublocale comm_monoid < monoid proof

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

let
fun tr' c = (c, fn ctxt => fn T => fn ts =>
if not (null ts) orelse T = dummyT
orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
then raise Match
else
Syntax.const @{syntax_const "_constrain"} $Syntax.const c$
Syntax_Phases.term_of_typ ctxt T);
in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
*} -- {* show types that are presumably too general *}

class plus =
fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)

class minus =
fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)

class uminus =
fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)

class times =
fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)

subsection {* Semigroups and Monoids *}

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

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

begin

end

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

sublocale semigroup_mult < mult!: semigroup times proof
qed (fact mult_assoc)

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

sublocale ab_semigroup_mult < mult!: abel_semigroup times proof
qed (fact mult_commute)

context ab_semigroup_mult
begin

lemmas mult_left_commute [algebra_simps, field_simps] = mult.left_commute

theorems mult_ac = mult_assoc mult_commute mult_left_commute

end

theorems mult_ac = mult_assoc mult_commute mult_left_commute

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

lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
by (rule eq_commute)

assumes add_0: "0 + a = a"

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

sublocale monoid_mult < mult!: monoid times 1 proof
qed (fact mult_1_left mult_1_right)+

lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
by (rule eq_commute)

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

sublocale comm_monoid_mult < mult!: comm_monoid times 1 proof
qed (insert mult_1, simp add: ac_simps)

subclass (in comm_monoid_mult) monoid_mult proof
qed (fact mult.left_neutral mult.right_neutral)+

assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
begin

"a + b = a + c \<longleftrightarrow> b = c"

"b + a = c + a \<longleftrightarrow> b = c"

end

assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
begin

proof
fix a b c :: 'a
assume "a + b = a + c"
then show "b = c" by (rule add_imp_eq)
next
fix a b c :: 'a
assume "b + a = c + a"
then have "a + b = a + c" by (simp only: add_commute)
then show "b = c" by (rule add_imp_eq)
qed

end

subsection {* Groups *}

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

lemma minus_unique:
assumes "a + b = 0" shows "- a = b"
proof -
have "- a = - a + (a + b)" using assms by simp
finally show ?thesis .
qed

lemmas equals_zero_I = minus_unique (* legacy name *)

lemma minus_zero [simp]: "- 0 = 0"
proof -
have "0 + 0 = 0" by (rule add_0_right)
thus "- 0 = 0" by (rule minus_unique)
qed

lemma minus_minus [simp]: "- (- a) = a"
proof -
have "- a + a = 0" by (rule left_minus)
thus "- (- a) = a" by (rule minus_unique)
qed

lemma right_minus [simp]: "a + - a = 0"
proof -
have "a + - a = - (- a) + - a" by simp
also have "\<dots> = 0" by (rule left_minus)
finally show ?thesis .
qed

proof
fix a b c :: 'a
assume "a + b = a + c"
then have "- a + a + b = - a + a + c"
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" unfolding add_assoc by simp
qed

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

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

lemma minus_add: "- (a + b) = - b + - a"
proof -
have "(a + b) + (- b + - a) = 0"
thus "- (a + b) = - b + - a"
by (rule minus_unique)
qed

lemma right_minus_eq: "a - b = 0 \<longleftrightarrow> a = b"
proof
assume "a - b = 0"
have "a = (a - b) + b" by (simp add:diff_minus add_assoc)
also have "\<dots> = b" using a - b = 0 by simp
finally show "a = b" .
next
assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
qed

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

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 \<longleftrightarrow> a = b"
proof
assume "- a = - b"
hence "- (- a) = - (- b)" by simp
thus "a = b" by simp
next
assume "a = b"
thus "- a = - b" by simp
qed

lemma neg_equal_0_iff_equal [simp]:
"- a = 0 \<longleftrightarrow> a = 0"
by (subst neg_equal_iff_equal [symmetric], simp)

lemma neg_0_equal_iff_equal [simp]:
"0 = - a \<longleftrightarrow> 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 \<longleftrightarrow> b = - a"
proof -
have "- (- a) = - b \<longleftrightarrow> - a = b" by (rule neg_equal_iff_equal)
thus ?thesis by (simp add: eq_commute)
qed

lemma minus_equation_iff:
"- a = b \<longleftrightarrow> - b = a"
proof -
have "- a = - (- b) \<longleftrightarrow> a = -b" by (rule neg_equal_iff_equal)
thus ?thesis by (simp add: eq_commute)
qed

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

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

declare diff_minus[symmetric, algebra_simps, field_simps]

lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> 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_iff: "x + y = 0 \<longleftrightarrow> y = - x"
by (rule equation_minus_iff)

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

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

lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"

lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"

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

lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
by (fact right_minus_eq [symmetric])

lemma diff_eq_diff_eq:
"a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
by (simp add: 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_minus: "a - b = a + (- b)"
begin

proof qed (simp_all add: ab_left_minus ab_diff_minus)

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

"- a + b = b - a"

"- (a + b) = - a + - b"

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

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

(* FIXME: duplicates right_minus_eq from class group_add *)
(* but only this one is declared as a simp rule. *)
lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
by (rule right_minus_eq)

end

subsection {* (Partially) Ordered Groups *}

text {*
The theory of partially ordered groups is taken from the books:
\begin{itemize}
\item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
\item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
\end{itemize}
Most of the used notions can also be looked up in
\begin{itemize}
\item \url{http://www.mathworld.com} by Eric Weisstein et. al.
\item \emph{Algebra I} by van der Waerden, Springer.
\end{itemize}
*}

assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
begin

"a \<le> b \<Longrightarrow> a + c \<le> b + c"

text {* non-strict, in both arguments *}
"a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
done

end

begin

"a < b \<Longrightarrow> c + a < c + b"

"a < b \<Longrightarrow> a + c < b + c"

text{*Strict monotonicity in both arguments*}
"a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
done

"a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
done

"a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
done

end

assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
begin

assumes less: "c + a < c + b" shows "a < b"
proof -
from less have le: "c + a <= c + b" by (simp add: order_le_less)
have "a <= b"
apply (insert le)
by (insert le, drule add_le_imp_le_left, assumption)
moreover have "a \<noteq> b"
proof (rule ccontr)
assume "~(a \<noteq> b)"
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" by (simp add: order_le_less)
qed

"a + c < b + c \<Longrightarrow> a < b"
done

"c + a < c + b \<longleftrightarrow> a < b"

"a + c < b + c \<longleftrightarrow> a < b"

"c + a \<le> c + b \<longleftrightarrow> a \<le> b"

"a + c \<le> b + c \<longleftrightarrow> a \<le> b"

"a + c \<le> b + c \<Longrightarrow> a \<le> b"
by simp

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

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

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

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

end

subsection {* Support for reasoning about signs *}

begin

assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
proof -
have "0 + 0 < a + b"
then show ?thesis by simp
qed

assumes "0 < a" and "0 < b" shows "0 < a + b"
by (rule add_pos_nonneg) (insert assms, auto)

assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
proof -
have "0 + 0 < a + b"
then show ?thesis by simp
qed

assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
proof -
have "0 + 0 \<le> a + b"
then show ?thesis by simp
qed

assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
proof -
have "a + b < 0 + 0"
then show ?thesis by simp
qed

assumes "a < 0" and "b < 0" shows "a + b < 0"
by (rule add_neg_nonpos) (insert assms, auto)

assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
proof -
have "a + b < 0 + 0"
then show ?thesis by simp
qed

assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
proof -
have "a + b \<le> 0 + 0"
then show ?thesis by simp
qed

assumes x: "0 \<le> x" and y: "0 \<le> y"
shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
proof (intro iffI conjI)
have "x = x + 0" by simp
also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
also assume "x + y = 0"
also have "0 \<le> x" using x .
finally show "x = 0" .
next
have "y = 0 + y" by simp
also have "0 + y \<le> x + y" using x by (rule add_right_mono)
also assume "x + y = 0"
also have "0 \<le> y" using y .
finally show "y = 0" .
next
assume "x = 0 \<and> y = 0"
then show "x + y = 0" by simp
qed

end

begin

proof
fix a b c :: 'a
assume "c + a \<le> c + b"
hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
thus "a \<le> b" by simp
qed

lemma max_diff_distrib_left:
shows "max x y - z = max (x - z) (y - z)"

lemma min_diff_distrib_left:
shows "min x y - z = min (x - z) (y - z)"

lemma le_imp_neg_le:
assumes "a \<le> b" shows "-b \<le> -a"
proof -
have "-a+a \<le> -a+b" using a \<le> b by (rule add_left_mono)
hence "0 \<le> -a+b" by simp
hence "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono)
qed

lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
proof
assume "- b \<le> - a"
hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
thus "a\<le>b" by simp
next
assume "a\<le>b"
thus "-b \<le> -a" by (rule le_imp_neg_le)
qed

lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
by (subst neg_le_iff_le [symmetric], simp)

lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
by (subst neg_le_iff_le [symmetric], simp)

lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"

lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
by (subst neg_less_iff_less [symmetric], simp)

lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> 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 \<longleftrightarrow> b < - a"
proof -
have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
thus ?thesis by simp
qed

lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
proof -
have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
thus ?thesis by simp
qed

lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
proof -
have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
have "(- (- a) <= -b) = (b <= - a)"
apply (auto simp only: le_less)
apply (drule mm)
apply (simp_all)
apply (drule mm[simplified], assumption)
done
then show ?thesis by simp
qed

lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
by (auto simp add: le_less minus_less_iff)

lemma diff_less_0_iff_less [simp, no_atp]:
"a - b < 0 \<longleftrightarrow> a < b"
proof -
have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)
also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
finally show ?thesis .
qed

lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]

lemma diff_less_eq[algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"
apply (subst less_iff_diff_less_0 [of a])
apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
done

lemma less_diff_eq[algebra_simps, field_simps]: "a < c - b \<longleftrightarrow> a + b < c"
apply (subst less_iff_diff_less_0 [of "a + b"])
apply (subst less_iff_diff_less_0 [of a])
done

lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"

lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"

lemma diff_le_0_iff_le [simp, no_atp]:
"a - b \<le> 0 \<longleftrightarrow> a \<le> b"

lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]

lemma diff_eq_diff_less:
"a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> 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 \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])

end

use "Tools/abel_cancel.ML"

simproc_setup abel_cancel_sum
{* fn phi => Abel_Cancel.sum_proc *}

simproc_setup abel_cancel_relation
{* fn phi => Abel_Cancel.rel_proc *}

begin

proof
fix a b c :: 'a
assume le: "c + a <= c + b"
show "a <= b"
proof (rule ccontr)
assume w: "~ a \<le> b"
hence "b <= a" by (simp add: linorder_not_le)
hence le2: "c + b <= c + a" by (rule add_left_mono)
have "a = b"
apply (insert le)
apply (insert le2)
apply (drule antisym, simp_all)
done
with w show False
qed
qed

end

begin

lemma neg_less_eq_nonneg [simp]:
"- a \<le> a \<longleftrightarrow> 0 \<le> a"
proof
assume A: "- a \<le> a" show "0 \<le> a"
proof (rule classical)
assume "\<not> 0 \<le> a"
then have "a < 0" by auto
with A have "- a < 0" by (rule le_less_trans)
then show ?thesis by auto
qed
next
assume A: "0 \<le> a" show "- a \<le> a"
proof (rule order_trans)
show "- a \<le> 0" using A by (simp add: minus_le_iff)
next
show "0 \<le> a" using A .
qed
qed

lemma neg_less_nonneg [simp]:
"- a < a \<longleftrightarrow> 0 < a"
proof
assume A: "- a < a" show "0 < a"
proof (rule classical)
assume "\<not> 0 < a"
then have "a \<le> 0" by auto
with A have "- a < 0" by (rule less_le_trans)
then show ?thesis by auto
qed
next
assume A: "0 < a" show "- a < a"
proof (rule less_trans)
show "- a < 0" using A by (simp add: minus_le_iff)
next
show "0 < a" using A .
qed
qed

lemma less_eq_neg_nonpos [simp]:
"a \<le> - a \<longleftrightarrow> a \<le> 0"
proof
assume A: "a \<le> - a" show "a \<le> 0"
proof (rule classical)
assume "\<not> a \<le> 0"
then have "0 < a" by auto
then have "0 < - a" using A by (rule less_le_trans)
then show ?thesis by auto
qed
next
assume A: "a \<le> 0" show "a \<le> - a"
proof (rule order_trans)
show "0 \<le> - a" using A by (simp add: minus_le_iff)
next
show "a \<le> 0" using A .
qed
qed

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

lemma neg_equal_zero [simp]:
"- a = a \<longleftrightarrow> a = 0"
by (auto dest: sym)

lemma double_zero [simp]:
"a + a = 0 \<longleftrightarrow> a = 0"
proof
assume assm: "a + a = 0"
then have a: "- a = a" by (rule minus_unique)
then show "a = 0" by (simp only: neg_equal_zero)
qed simp

lemma double_zero_sym [simp]:
"0 = a + a \<longleftrightarrow> a = 0"
by (rule, drule sym) simp_all

"0 < a + a \<longleftrightarrow> 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 only: neg_less_nonneg)
next
assume "0 < a"
with this have "0 + 0 < a + a"
then show "0 < a + a" by simp
qed

"0 \<le> a + a \<longleftrightarrow> 0 \<le> a"

"a + a < 0 \<longleftrightarrow> a < 0"
proof -
have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
then show ?thesis by simp
qed

"a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
proof -
have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
then show ?thesis by simp
qed

lemma le_minus_self_iff:
"a \<le> - a \<longleftrightarrow> a \<le> 0"
proof -
from add_le_cancel_left [of "- a" "a + a" 0]
have "a \<le> - a \<longleftrightarrow> a + a \<le> 0"
thus ?thesis by simp
qed

lemma minus_le_self_iff:
"- a \<le> a \<longleftrightarrow> 0 \<le> a"
proof -
from add_le_cancel_left [of "- a" 0 "a + a"]
have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a"
thus ?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

begin

"0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
by (insert add_mono [of 0 a b c], simp)

"0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"

"0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
by (insert add_less_le_mono [of 0 a b c], simp)

"0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
by (insert add_le_less_mono [of 0 a b c], simp)

end

class abs =
fixes abs :: "'a \<Rightarrow> 'a"
begin

notation (xsymbols)
abs  ("\<bar>_\<bar>")

notation (HTML output)
abs  ("\<bar>_\<bar>")

end

class sgn =
fixes sgn :: "'a \<Rightarrow> 'a"

class abs_if = minus + uminus + ord + zero + abs +
assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"

class sgn_if = minus + uminus + zero + one + ord + sgn +
assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
begin

lemma sgn0 [simp]: "sgn 0 = 0"

end

assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
and abs_ge_self: "a \<le> \<bar>a\<bar>"
and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
begin

lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
unfolding neg_le_0_iff_le by simp

lemma abs_of_nonneg [simp]:
assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
proof (rule antisym)
from nonneg le_imp_neg_le have "- a \<le> 0" by simp
from this nonneg have "- a \<le> a" by (rule order_trans)
then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
qed (rule abs_ge_self)

lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
by (rule antisym)
(auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])

lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
proof -
have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
proof (rule antisym)
assume zero: "\<bar>a\<bar> = 0"
with abs_ge_self show "a \<le> 0" by auto
from zero have "\<bar>-a\<bar> = 0" by simp
with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
with neg_le_0_iff_le show "0 \<le> a" by auto
qed
then show ?thesis by auto
qed

lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
by simp

lemma abs_0_eq [simp, no_atp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
proof -
have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
thus ?thesis by simp
qed

lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"
proof
assume "\<bar>a\<bar> \<le> 0"
then have "\<bar>a\<bar> = 0" by (rule antisym) simp
thus "a = 0" by simp
next
assume "a = 0"
thus "\<bar>a\<bar> \<le> 0" by simp
qed

lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"

lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
proof -
have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
show ?thesis by (simp add: a)
qed

lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
proof -
have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
then show ?thesis by simp
qed

lemma abs_minus_commute:
"\<bar>a - b\<bar> = \<bar>b - a\<bar>"
proof -
have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
also have "... = \<bar>b - a\<bar>" by simp
finally show ?thesis .
qed

lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
by (rule abs_of_nonneg, rule less_imp_le)

lemma abs_of_nonpos [simp]:
assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
proof -
let ?b = "- a"
have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?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 \<Longrightarrow> \<bar>a\<bar> = - a"
by (rule abs_of_nonpos, rule less_imp_le)

lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
by (insert abs_ge_self, blast intro: order_trans)

lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
by (insert abs_le_D1 [of "- a"], simp)

lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)

lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
proof -
have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
then show ?thesis
qed

lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)

lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)

lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
proof -
have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (subst diff_minus, rule refl)
also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
finally show ?thesis by simp
qed

lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
proof -
have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
finally show ?thesis .
qed

"\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
proof (rule antisym)
show "?L \<ge> ?R" by(rule abs_ge_self)
next
have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
also have "\<dots> = ?R" by simp
finally show "?L \<le> ?R" .
qed

end

subsection {* Tools setup *}

fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"
shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"

fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add"
shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"

code_modulename SML
Groups Arith

code_modulename OCaml
Groups Arith