src/HOL/Groups.thy
 author wenzelm Tue Sep 01 22:32:58 2015 +0200 (2015-09-01) changeset 61076 bdc1e2f0a86a parent 60762 bf0c76ccee8d child 61169 4de9ff3ea29a permissions -rw-r--r--
eliminated \<Colon>;
     1 (*  Title:   HOL/Groups.thy

     2     Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, Markus Wenzel, Jeremy Avigad

     3 *)

     4

     5 section \<open>Groups, also combined with orderings\<close>

     6

     7 theory Groups

     8 imports Orderings

     9 begin

    10

    11 subsection \<open>Dynamic facts\<close>

    12

    13 named_theorems ac_simps "associativity and commutativity simplification rules"

    14

    15

    16 text\<open>The rewrites accumulated in @{text algebra_simps} deal with the

    17 classical algebraic structures of groups, rings and family. They simplify

    18 terms by multiplying everything out (in case of a ring) and bringing sums and

    19 products into a canonical form (by ordered rewriting). As a result it decides

    20 group and ring equalities but also helps with inequalities.

    21

    22 Of course it also works for fields, but it knows nothing about multiplicative

    23 inverses or division. This is catered for by @{text field_simps}.\<close>

    24

    25 named_theorems algebra_simps "algebra simplification rules"

    26

    27

    28 text\<open>Lemmas @{text field_simps} multiply with denominators in (in)equations

    29 if they can be proved to be non-zero (for equations) or positive/negative

    30 (for inequations). Can be too aggressive and is therefore separate from the

    31 more benign @{text algebra_simps}.\<close>

    32

    33 named_theorems field_simps "algebra simplification rules for fields"

    34

    35

    36 subsection \<open>Abstract structures\<close>

    37

    38 text \<open>

    39   These locales provide basic structures for interpretation into

    40   bigger structures;  extensions require careful thinking, otherwise

    41   undesired effects may occur due to interpretation.

    42 \<close>

    43

    44 locale semigroup =

    45   fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)

    46   assumes assoc [ac_simps]: "a * b * c = a * (b * c)"

    47

    48 locale abel_semigroup = semigroup +

    49   assumes commute [ac_simps]: "a * b = b * a"

    50 begin

    51

    52 lemma left_commute [ac_simps]:

    53   "b * (a * c) = a * (b * c)"

    54 proof -

    55   have "(b * a) * c = (a * b) * c"

    56     by (simp only: commute)

    57   then show ?thesis

    58     by (simp only: assoc)

    59 qed

    60

    61 end

    62

    63 locale monoid = semigroup +

    64   fixes z :: 'a ("1")

    65   assumes left_neutral [simp]: "1 * a = a"

    66   assumes right_neutral [simp]: "a * 1 = a"

    67

    68 locale comm_monoid = abel_semigroup +

    69   fixes z :: 'a ("1")

    70   assumes comm_neutral: "a * 1 = a"

    71 begin

    72

    73 sublocale monoid

    74   by default (simp_all add: commute comm_neutral)

    75

    76 end

    77

    78

    79 subsection \<open>Generic operations\<close>

    80

    81 class zero =

    82   fixes zero :: 'a  ("0")

    83

    84 class one =

    85   fixes one  :: 'a  ("1")

    86

    87 hide_const (open) zero one

    88

    89 lemma Let_0 [simp]: "Let 0 f = f 0"

    90   unfolding Let_def ..

    91

    92 lemma Let_1 [simp]: "Let 1 f = f 1"

    93   unfolding Let_def ..

    94

    95 setup \<open>

    96   Reorient_Proc.add

    97     (fn Const(@{const_name Groups.zero}, _) => true

    98       | Const(@{const_name Groups.one}, _) => true

    99       | _ => false)

   100 \<close>

   101

   102 simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc

   103 simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc

   104

   105 typed_print_translation \<open>

   106   let

   107     fun tr' c = (c, fn ctxt => fn T => fn ts =>

   108       if null ts andalso Printer.type_emphasis ctxt T then

   109         Syntax.const @{syntax_const "_constrain"} $Syntax.const c$

   110           Syntax_Phases.term_of_typ ctxt T

   111       else raise Match);

   112   in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;

   113 \<close> -- \<open>show types that are presumably too general\<close>

   114

   115 class plus =

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

   117

   118 class minus =

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

   120

   121 class uminus =

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

   123

   124 class times =

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

   126

   127

   128 subsection \<open>Semigroups and Monoids\<close>

   129

   130 class semigroup_add = plus +

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

   132 begin

   133

   134 sublocale add!: semigroup plus

   135   by default (fact add_assoc)

   136

   137 end

   138

   139 hide_fact add_assoc

   140

   141 class ab_semigroup_add = semigroup_add +

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

   143 begin

   144

   145 sublocale add!: abel_semigroup plus

   146   by default (fact add_commute)

   147

   148 declare add.left_commute [algebra_simps, field_simps]

   149

   150 theorems add_ac = add.assoc add.commute add.left_commute

   151

   152 end

   153

   154 hide_fact add_commute

   155

   156 theorems add_ac = add.assoc add.commute add.left_commute

   157

   158 class semigroup_mult = times +

   159   assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"

   160 begin

   161

   162 sublocale mult!: semigroup times

   163   by default (fact mult_assoc)

   164

   165 end

   166

   167 hide_fact mult_assoc

   168

   169 class ab_semigroup_mult = semigroup_mult +

   170   assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"

   171 begin

   172

   173 sublocale mult!: abel_semigroup times

   174   by default (fact mult_commute)

   175

   176 declare mult.left_commute [algebra_simps, field_simps]

   177

   178 theorems mult_ac = mult.assoc mult.commute mult.left_commute

   179

   180 end

   181

   182 hide_fact mult_commute

   183

   184 theorems mult_ac = mult.assoc mult.commute mult.left_commute

   185

   186 class monoid_add = zero + semigroup_add +

   187   assumes add_0_left: "0 + a = a"

   188     and add_0_right: "a + 0 = a"

   189 begin

   190

   191 sublocale add!: monoid plus 0

   192   by default (fact add_0_left add_0_right)+

   193

   194 end

   195

   196 lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"

   197   by (fact eq_commute)

   198

   199 class comm_monoid_add = zero + ab_semigroup_add +

   200   assumes add_0: "0 + a = a"

   201 begin

   202

   203 subclass monoid_add

   204   by default (simp_all add: add_0 add.commute [of _ 0])

   205

   206 sublocale add!: comm_monoid plus 0

   207   by default (simp add: ac_simps)

   208

   209 end

   210

   211 class monoid_mult = one + semigroup_mult +

   212   assumes mult_1_left: "1 * a  = a"

   213     and mult_1_right: "a * 1 = a"

   214 begin

   215

   216 sublocale mult!: monoid times 1

   217   by default (fact mult_1_left mult_1_right)+

   218

   219 end

   220

   221 lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"

   222   by (fact eq_commute)

   223

   224 class comm_monoid_mult = one + ab_semigroup_mult +

   225   assumes mult_1: "1 * a = a"

   226 begin

   227

   228 subclass monoid_mult

   229   by default (simp_all add: mult_1 mult.commute [of _ 1])

   230

   231 sublocale mult!: comm_monoid times 1

   232   by default (simp add: ac_simps)

   233

   234 end

   235

   236 class cancel_semigroup_add = semigroup_add +

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

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

   239 begin

   240

   241 lemma add_left_cancel [simp]:

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

   243 by (blast dest: add_left_imp_eq)

   244

   245 lemma add_right_cancel [simp]:

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

   247 by (blast dest: add_right_imp_eq)

   248

   249 end

   250

   251 class cancel_ab_semigroup_add = ab_semigroup_add + minus +

   252   assumes add_diff_cancel_left' [simp]: "(a + b) - a = b"

   253   assumes diff_diff_add [algebra_simps, field_simps]: "a - b - c = a - (b + c)"

   254 begin

   255

   256 lemma add_diff_cancel_right' [simp]:

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

   258   using add_diff_cancel_left' [of b a] by (simp add: ac_simps)

   259

   260 subclass cancel_semigroup_add

   261 proof

   262   fix a b c :: 'a

   263   assume "a + b = a + c"

   264   then have "a + b - a = a + c - a"

   265     by simp

   266   then show "b = c"

   267     by simp

   268 next

   269   fix a b c :: 'a

   270   assume "b + a = c + a"

   271   then have "b + a - a = c + a - a"

   272     by simp

   273   then show "b = c"

   274     by simp

   275 qed

   276

   277 lemma add_diff_cancel_left [simp]:

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

   279   unfolding diff_diff_add [symmetric] by simp

   280

   281 lemma add_diff_cancel_right [simp]:

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

   283   using add_diff_cancel_left [symmetric] by (simp add: ac_simps)

   284

   285 lemma diff_right_commute:

   286   "a - c - b = a - b - c"

   287   by (simp add: diff_diff_add add.commute)

   288

   289 end

   290

   291 class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add

   292 begin

   293

   294 lemma diff_zero [simp]:

   295   "a - 0 = a"

   296   using add_diff_cancel_right' [of a 0] by simp

   297

   298 lemma diff_cancel [simp]:

   299   "a - a = 0"

   300 proof -

   301   have "(a + 0) - (a + 0) = 0" by (simp only: add_diff_cancel_left diff_zero)

   302   then show ?thesis by simp

   303 qed

   304

   305 lemma add_implies_diff:

   306   assumes "c + b = a"

   307   shows "c = a - b"

   308 proof -

   309   from assms have "(b + c) - (b + 0) = a - b" by (simp add: add.commute)

   310   then show "c = a - b" by simp

   311 qed

   312

   313 end

   314

   315 class comm_monoid_diff = cancel_comm_monoid_add +

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

   317 begin

   318

   319 lemma diff_add_zero [simp]:

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

   321 proof -

   322   have "a - (a + b) = (a + 0) - (a + b)" by simp

   323   also have "\<dots> = 0" by (simp only: add_diff_cancel_left zero_diff)

   324   finally show ?thesis .

   325 qed

   326

   327 end

   328

   329

   330 subsection \<open>Groups\<close>

   331

   332 class group_add = minus + uminus + monoid_add +

   333   assumes left_minus [simp]: "- a + a = 0"

   334   assumes add_uminus_conv_diff [simp]: "a + (- b) = a - b"

   335 begin

   336

   337 lemma diff_conv_add_uminus:

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

   339   by simp

   340

   341 lemma minus_unique:

   342   assumes "a + b = 0" shows "- a = b"

   343 proof -

   344   have "- a = - a + (a + b)" using assms by simp

   345   also have "\<dots> = b" by (simp add: add.assoc [symmetric])

   346   finally show ?thesis .

   347 qed

   348

   349 lemma minus_zero [simp]: "- 0 = 0"

   350 proof -

   351   have "0 + 0 = 0" by (rule add_0_right)

   352   thus "- 0 = 0" by (rule minus_unique)

   353 qed

   354

   355 lemma minus_minus [simp]: "- (- a) = a"

   356 proof -

   357   have "- a + a = 0" by (rule left_minus)

   358   thus "- (- a) = a" by (rule minus_unique)

   359 qed

   360

   361 lemma right_minus: "a + - a = 0"

   362 proof -

   363   have "a + - a = - (- a) + - a" by simp

   364   also have "\<dots> = 0" by (rule left_minus)

   365   finally show ?thesis .

   366 qed

   367

   368 lemma diff_self [simp]:

   369   "a - a = 0"

   370   using right_minus [of a] by simp

   371

   372 subclass cancel_semigroup_add

   373 proof

   374   fix a b c :: 'a

   375   assume "a + b = a + c"

   376   then have "- a + a + b = - a + a + c"

   377     unfolding add.assoc by simp

   378   then show "b = c" by simp

   379 next

   380   fix a b c :: 'a

   381   assume "b + a = c + a"

   382   then have "b + a + - a = c + a  + - a" by simp

   383   then show "b = c" unfolding add.assoc by simp

   384 qed

   385

   386 lemma minus_add_cancel [simp]:

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

   388   by (simp add: add.assoc [symmetric])

   389

   390 lemma add_minus_cancel [simp]:

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

   392   by (simp add: add.assoc [symmetric])

   393

   394 lemma diff_add_cancel [simp]:

   395   "a - b + b = a"

   396   by (simp only: diff_conv_add_uminus add.assoc) simp

   397

   398 lemma add_diff_cancel [simp]:

   399   "a + b - b = a"

   400   by (simp only: diff_conv_add_uminus add.assoc) simp

   401

   402 lemma minus_add:

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

   404 proof -

   405   have "(a + b) + (- b + - a) = 0"

   406     by (simp only: add.assoc add_minus_cancel) simp

   407   then show "- (a + b) = - b + - a"

   408     by (rule minus_unique)

   409 qed

   410

   411 lemma right_minus_eq [simp]:

   412   "a - b = 0 \<longleftrightarrow> a = b"

   413 proof

   414   assume "a - b = 0"

   415   have "a = (a - b) + b" by (simp add: add.assoc)

   416   also have "\<dots> = b" using \<open>a - b = 0\<close> by simp

   417   finally show "a = b" .

   418 next

   419   assume "a = b" thus "a - b = 0" by simp

   420 qed

   421

   422 lemma eq_iff_diff_eq_0:

   423   "a = b \<longleftrightarrow> a - b = 0"

   424   by (fact right_minus_eq [symmetric])

   425

   426 lemma diff_0 [simp]:

   427   "0 - a = - a"

   428   by (simp only: diff_conv_add_uminus add_0_left)

   429

   430 lemma diff_0_right [simp]:

   431   "a - 0 = a"

   432   by (simp only: diff_conv_add_uminus minus_zero add_0_right)

   433

   434 lemma diff_minus_eq_add [simp]:

   435   "a - - b = a + b"

   436   by (simp only: diff_conv_add_uminus minus_minus)

   437

   438 lemma neg_equal_iff_equal [simp]:

   439   "- a = - b \<longleftrightarrow> a = b"

   440 proof

   441   assume "- a = - b"

   442   hence "- (- a) = - (- b)" by simp

   443   thus "a = b" by simp

   444 next

   445   assume "a = b"

   446   thus "- a = - b" by simp

   447 qed

   448

   449 lemma neg_equal_0_iff_equal [simp]:

   450   "- a = 0 \<longleftrightarrow> a = 0"

   451   by (subst neg_equal_iff_equal [symmetric]) simp

   452

   453 lemma neg_0_equal_iff_equal [simp]:

   454   "0 = - a \<longleftrightarrow> 0 = a"

   455   by (subst neg_equal_iff_equal [symmetric]) simp

   456

   457 text\<open>The next two equations can make the simplifier loop!\<close>

   458

   459 lemma equation_minus_iff:

   460   "a = - b \<longleftrightarrow> b = - a"

   461 proof -

   462   have "- (- a) = - b \<longleftrightarrow> - a = b" by (rule neg_equal_iff_equal)

   463   thus ?thesis by (simp add: eq_commute)

   464 qed

   465

   466 lemma minus_equation_iff:

   467   "- a = b \<longleftrightarrow> - b = a"

   468 proof -

   469   have "- a = - (- b) \<longleftrightarrow> a = -b" by (rule neg_equal_iff_equal)

   470   thus ?thesis by (simp add: eq_commute)

   471 qed

   472

   473 lemma eq_neg_iff_add_eq_0:

   474   "a = - b \<longleftrightarrow> a + b = 0"

   475 proof

   476   assume "a = - b" then show "a + b = 0" by simp

   477 next

   478   assume "a + b = 0"

   479   moreover have "a + (b + - b) = (a + b) + - b"

   480     by (simp only: add.assoc)

   481   ultimately show "a = - b" by simp

   482 qed

   483

   484 lemma add_eq_0_iff2:

   485   "a + b = 0 \<longleftrightarrow> a = - b"

   486   by (fact eq_neg_iff_add_eq_0 [symmetric])

   487

   488 lemma neg_eq_iff_add_eq_0:

   489   "- a = b \<longleftrightarrow> a + b = 0"

   490   by (auto simp add: add_eq_0_iff2)

   491

   492 lemma add_eq_0_iff:

   493   "a + b = 0 \<longleftrightarrow> b = - a"

   494   by (auto simp add: neg_eq_iff_add_eq_0 [symmetric])

   495

   496 lemma minus_diff_eq [simp]:

   497   "- (a - b) = b - a"

   498   by (simp only: neg_eq_iff_add_eq_0 diff_conv_add_uminus add.assoc minus_add_cancel) simp

   499

   500 lemma add_diff_eq [algebra_simps, field_simps]:

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

   502   by (simp only: diff_conv_add_uminus add.assoc)

   503

   504 lemma diff_add_eq_diff_diff_swap:

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

   506   by (simp only: diff_conv_add_uminus add.assoc minus_add)

   507

   508 lemma diff_eq_eq [algebra_simps, field_simps]:

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

   510   by auto

   511

   512 lemma eq_diff_eq [algebra_simps, field_simps]:

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

   514   by auto

   515

   516 lemma diff_diff_eq2 [algebra_simps, field_simps]:

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

   518   by (simp only: diff_conv_add_uminus add.assoc) simp

   519

   520 lemma diff_eq_diff_eq:

   521   "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"

   522   by (simp only: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])

   523

   524 end

   525

   526 class ab_group_add = minus + uminus + comm_monoid_add +

   527   assumes ab_left_minus: "- a + a = 0"

   528   assumes ab_diff_conv_add_uminus: "a - b = a + (- b)"

   529 begin

   530

   531 subclass group_add

   532   proof qed (simp_all add: ab_left_minus ab_diff_conv_add_uminus)

   533

   534 subclass cancel_comm_monoid_add

   535 proof

   536   fix a b c :: 'a

   537   have "b + a - a = b"

   538     by simp

   539   then show "a + b - a = b"

   540     by (simp add: ac_simps)

   541   show "a - b - c = a - (b + c)"

   542     by (simp add: algebra_simps)

   543 qed

   544

   545 lemma uminus_add_conv_diff [simp]:

   546   "- a + b = b - a"

   547   by (simp add: add.commute)

   548

   549 lemma minus_add_distrib [simp]:

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

   551   by (simp add: algebra_simps)

   552

   553 lemma diff_add_eq [algebra_simps, field_simps]:

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

   555   by (simp add: algebra_simps)

   556

   557 end

   558

   559

   560 subsection \<open>(Partially) Ordered Groups\<close>

   561

   562 text \<open>

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

   564   \begin{itemize}

   565   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979

   566   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963

   567   \end{itemize}

   568   Most of the used notions can also be looked up in

   569   \begin{itemize}

   570   \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.

   571   \item \emph{Algebra I} by van der Waerden, Springer.

   572   \end{itemize}

   573 \<close>

   574

   575 class ordered_ab_semigroup_add = order + ab_semigroup_add +

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

   577 begin

   578

   579 lemma add_right_mono:

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

   581 by (simp add: add.commute [of _ c] add_left_mono)

   582

   583 text \<open>non-strict, in both arguments\<close>

   584 lemma add_mono:

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

   586   apply (erule add_right_mono [THEN order_trans])

   587   apply (simp add: add.commute add_left_mono)

   588   done

   589

   590 end

   591

   592 class ordered_cancel_ab_semigroup_add =

   593   ordered_ab_semigroup_add + cancel_ab_semigroup_add

   594 begin

   595

   596 lemma add_strict_left_mono:

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

   598 by (auto simp add: less_le add_left_mono)

   599

   600 lemma add_strict_right_mono:

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

   602 by (simp add: add.commute [of _ c] add_strict_left_mono)

   603

   604 text\<open>Strict monotonicity in both arguments\<close>

   605 lemma add_strict_mono:

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

   607 apply (erule add_strict_right_mono [THEN less_trans])

   608 apply (erule add_strict_left_mono)

   609 done

   610

   611 lemma add_less_le_mono:

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

   613 apply (erule add_strict_right_mono [THEN less_le_trans])

   614 apply (erule add_left_mono)

   615 done

   616

   617 lemma add_le_less_mono:

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

   619 apply (erule add_right_mono [THEN le_less_trans])

   620 apply (erule add_strict_left_mono)

   621 done

   622

   623 end

   624

   625 class ordered_ab_semigroup_add_imp_le =

   626   ordered_cancel_ab_semigroup_add +

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

   628 begin

   629

   630 lemma add_less_imp_less_left:

   631   assumes less: "c + a < c + b" shows "a < b"

   632 proof -

   633   from less have le: "c + a <= c + b" by (simp add: order_le_less)

   634   have "a <= b"

   635     apply (insert le)

   636     apply (drule add_le_imp_le_left)

   637     by (insert le, drule add_le_imp_le_left, assumption)

   638   moreover have "a \<noteq> b"

   639   proof (rule ccontr)

   640     assume "~(a \<noteq> b)"

   641     then have "a = b" by simp

   642     then have "c + a = c + b" by simp

   643     with less show "False"by simp

   644   qed

   645   ultimately show "a < b" by (simp add: order_le_less)

   646 qed

   647

   648 lemma add_less_imp_less_right:

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

   650 apply (rule add_less_imp_less_left [of c])

   651 apply (simp add: add.commute)

   652 done

   653

   654 lemma add_less_cancel_left [simp]:

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

   656   by (blast intro: add_less_imp_less_left add_strict_left_mono)

   657

   658 lemma add_less_cancel_right [simp]:

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

   660   by (blast intro: add_less_imp_less_right add_strict_right_mono)

   661

   662 lemma add_le_cancel_left [simp]:

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

   664   by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono)

   665

   666 lemma add_le_cancel_right [simp]:

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

   668   by (simp add: add.commute [of a c] add.commute [of b c])

   669

   670 lemma add_le_imp_le_right:

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

   672 by simp

   673

   674 lemma max_add_distrib_left:

   675   "max x y + z = max (x + z) (y + z)"

   676   unfolding max_def by auto

   677

   678 lemma min_add_distrib_left:

   679   "min x y + z = min (x + z) (y + z)"

   680   unfolding min_def by auto

   681

   682 lemma max_add_distrib_right:

   683   "x + max y z = max (x + y) (x + z)"

   684   unfolding max_def by auto

   685

   686 lemma min_add_distrib_right:

   687   "x + min y z = min (x + y) (x + z)"

   688   unfolding min_def by auto

   689

   690 end

   691

   692 class ordered_cancel_comm_monoid_diff = comm_monoid_diff + ordered_ab_semigroup_add_imp_le +

   693   assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"

   694 begin

   695

   696 context

   697   fixes a b

   698   assumes "a \<le> b"

   699 begin

   700

   701 lemma add_diff_inverse:

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

   703   using \<open>a \<le> b\<close> by (auto simp add: le_iff_add)

   704

   705 lemma add_diff_assoc:

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

   707   using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.left_commute [of c])

   708

   709 lemma add_diff_assoc2:

   710   "b - a + c = b + c - a"

   711   using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.assoc)

   712

   713 lemma diff_add_assoc:

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

   715   using \<open>a \<le> b\<close> by (simp add: add.commute add_diff_assoc)

   716

   717 lemma diff_add_assoc2:

   718   "b + c - a = b - a + c"

   719   using \<open>a \<le> b\<close>by (simp add: add.commute add_diff_assoc)

   720

   721 lemma diff_diff_right:

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

   723   by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add.commute)

   724

   725 lemma diff_add:

   726   "b - a + a = b"

   727   by (simp add: add.commute add_diff_inverse)

   728

   729 lemma le_add_diff:

   730   "c \<le> b + c - a"

   731   by (auto simp add: add.commute diff_add_assoc2 le_iff_add)

   732

   733 lemma le_imp_diff_is_add:

   734   "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"

   735   by (auto simp add: add.commute add_diff_inverse)

   736

   737 lemma le_diff_conv2:

   738   "c \<le> b - a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q")

   739 proof

   740   assume ?P

   741   then have "c + a \<le> b - a + a" by (rule add_right_mono)

   742   then show ?Q by (simp add: add_diff_inverse add.commute)

   743 next

   744   assume ?Q

   745   then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add.commute)

   746   then show ?P by simp

   747 qed

   748

   749 end

   750

   751 end

   752

   753

   754 subsection \<open>Support for reasoning about signs\<close>

   755

   756 class ordered_comm_monoid_add =

   757   ordered_cancel_ab_semigroup_add + comm_monoid_add

   758 begin

   759

   760 lemma add_pos_nonneg:

   761   assumes "0 < a" and "0 \<le> b" shows "0 < a + b"

   762 proof -

   763   have "0 + 0 < a + b"

   764     using assms by (rule add_less_le_mono)

   765   then show ?thesis by simp

   766 qed

   767

   768 lemma add_pos_pos:

   769   assumes "0 < a" and "0 < b" shows "0 < a + b"

   770 by (rule add_pos_nonneg) (insert assms, auto)

   771

   772 lemma add_nonneg_pos:

   773   assumes "0 \<le> a" and "0 < b" shows "0 < a + b"

   774 proof -

   775   have "0 + 0 < a + b"

   776     using assms by (rule add_le_less_mono)

   777   then show ?thesis by simp

   778 qed

   779

   780 lemma add_nonneg_nonneg [simp]:

   781   assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"

   782 proof -

   783   have "0 + 0 \<le> a + b"

   784     using assms by (rule add_mono)

   785   then show ?thesis by simp

   786 qed

   787

   788 lemma add_neg_nonpos:

   789   assumes "a < 0" and "b \<le> 0" shows "a + b < 0"

   790 proof -

   791   have "a + b < 0 + 0"

   792     using assms by (rule add_less_le_mono)

   793   then show ?thesis by simp

   794 qed

   795

   796 lemma add_neg_neg:

   797   assumes "a < 0" and "b < 0" shows "a + b < 0"

   798 by (rule add_neg_nonpos) (insert assms, auto)

   799

   800 lemma add_nonpos_neg:

   801   assumes "a \<le> 0" and "b < 0" shows "a + b < 0"

   802 proof -

   803   have "a + b < 0 + 0"

   804     using assms by (rule add_le_less_mono)

   805   then show ?thesis by simp

   806 qed

   807

   808 lemma add_nonpos_nonpos:

   809   assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"

   810 proof -

   811   have "a + b \<le> 0 + 0"

   812     using assms by (rule add_mono)

   813   then show ?thesis by simp

   814 qed

   815

   816 lemmas add_sign_intros =

   817   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg

   818   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos

   819

   820 lemma add_nonneg_eq_0_iff:

   821   assumes x: "0 \<le> x" and y: "0 \<le> y"

   822   shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"

   823 proof (intro iffI conjI)

   824   have "x = x + 0" by simp

   825   also have "x + 0 \<le> x + y" using y by (rule add_left_mono)

   826   also assume "x + y = 0"

   827   also have "0 \<le> x" using x .

   828   finally show "x = 0" .

   829 next

   830   have "y = 0 + y" by simp

   831   also have "0 + y \<le> x + y" using x by (rule add_right_mono)

   832   also assume "x + y = 0"

   833   also have "0 \<le> y" using y .

   834   finally show "y = 0" .

   835 next

   836   assume "x = 0 \<and> y = 0"

   837   then show "x + y = 0" by simp

   838 qed

   839

   840 lemma add_increasing:

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

   842   by (insert add_mono [of 0 a b c], simp)

   843

   844 lemma add_increasing2:

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

   846   by (simp add: add_increasing add.commute [of a])

   847

   848 lemma add_strict_increasing:

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

   850   by (insert add_less_le_mono [of 0 a b c], simp)

   851

   852 lemma add_strict_increasing2:

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

   854   by (insert add_le_less_mono [of 0 a b c], simp)

   855

   856 end

   857

   858 class ordered_ab_group_add =

   859   ab_group_add + ordered_ab_semigroup_add

   860 begin

   861

   862 subclass ordered_cancel_ab_semigroup_add ..

   863

   864 subclass ordered_ab_semigroup_add_imp_le

   865 proof

   866   fix a b c :: 'a

   867   assume "c + a \<le> c + b"

   868   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)

   869   hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add.assoc)

   870   thus "a \<le> b" by simp

   871 qed

   872

   873 subclass ordered_comm_monoid_add ..

   874

   875 lemma add_less_same_cancel1 [simp]:

   876   "b + a < b \<longleftrightarrow> a < 0"

   877   using add_less_cancel_left [of _ _ 0] by simp

   878

   879 lemma add_less_same_cancel2 [simp]:

   880   "a + b < b \<longleftrightarrow> a < 0"

   881   using add_less_cancel_right [of _ _ 0] by simp

   882

   883 lemma less_add_same_cancel1 [simp]:

   884   "a < a + b \<longleftrightarrow> 0 < b"

   885   using add_less_cancel_left [of _ 0] by simp

   886

   887 lemma less_add_same_cancel2 [simp]:

   888   "a < b + a \<longleftrightarrow> 0 < b"

   889   using add_less_cancel_right [of 0] by simp

   890

   891 lemma add_le_same_cancel1 [simp]:

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

   893   using add_le_cancel_left [of _ _ 0] by simp

   894

   895 lemma add_le_same_cancel2 [simp]:

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

   897   using add_le_cancel_right [of _ _ 0] by simp

   898

   899 lemma le_add_same_cancel1 [simp]:

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

   901   using add_le_cancel_left [of _ 0] by simp

   902

   903 lemma le_add_same_cancel2 [simp]:

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

   905   using add_le_cancel_right [of 0] by simp

   906

   907 lemma max_diff_distrib_left:

   908   shows "max x y - z = max (x - z) (y - z)"

   909   using max_add_distrib_left [of x y "- z"] by simp

   910

   911 lemma min_diff_distrib_left:

   912   shows "min x y - z = min (x - z) (y - z)"

   913   using min_add_distrib_left [of x y "- z"] by simp

   914

   915 lemma le_imp_neg_le:

   916   assumes "a \<le> b" shows "-b \<le> -a"

   917 proof -

   918   have "-a+a \<le> -a+b" using \<open>a \<le> b\<close> by (rule add_left_mono)

   919   then have "0 \<le> -a+b" by simp

   920   then have "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono)

   921   then show ?thesis by (simp add: algebra_simps)

   922 qed

   923

   924 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"

   925 proof

   926   assume "- b \<le> - a"

   927   hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)

   928   thus "a\<le>b" by simp

   929 next

   930   assume "a\<le>b"

   931   thus "-b \<le> -a" by (rule le_imp_neg_le)

   932 qed

   933

   934 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"

   935 by (subst neg_le_iff_le [symmetric], simp)

   936

   937 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"

   938 by (subst neg_le_iff_le [symmetric], simp)

   939

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

   941 by (force simp add: less_le)

   942

   943 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"

   944 by (subst neg_less_iff_less [symmetric], simp)

   945

   946 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"

   947 by (subst neg_less_iff_less [symmetric], simp)

   948

   949 text\<open>The next several equations can make the simplifier loop!\<close>

   950

   951 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"

   952 proof -

   953   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)

   954   thus ?thesis by simp

   955 qed

   956

   957 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"

   958 proof -

   959   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)

   960   thus ?thesis by simp

   961 qed

   962

   963 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"

   964 proof -

   965   have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)

   966   have "(- (- a) <= -b) = (b <= - a)"

   967     apply (auto simp only: le_less)

   968     apply (drule mm)

   969     apply (simp_all)

   970     apply (drule mm[simplified], assumption)

   971     done

   972   then show ?thesis by simp

   973 qed

   974

   975 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"

   976 by (auto simp add: le_less minus_less_iff)

   977

   978 lemma diff_less_0_iff_less [simp]:

   979   "a - b < 0 \<longleftrightarrow> a < b"

   980 proof -

   981   have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by simp

   982   also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)

   983   finally show ?thesis .

   984 qed

   985

   986 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]

   987

   988 lemma diff_less_eq [algebra_simps, field_simps]:

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

   990 apply (subst less_iff_diff_less_0 [of a])

   991 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])

   992 apply (simp add: algebra_simps)

   993 done

   994

   995 lemma less_diff_eq[algebra_simps, field_simps]:

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

   997 apply (subst less_iff_diff_less_0 [of "a + b"])

   998 apply (subst less_iff_diff_less_0 [of a])

   999 apply (simp add: algebra_simps)

  1000 done

  1001

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

  1003 by (auto simp add: le_less diff_less_eq )

  1004

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

  1006 by (auto simp add: le_less less_diff_eq)

  1007

  1008 lemma diff_le_0_iff_le [simp]:

  1009   "a - b \<le> 0 \<longleftrightarrow> a \<le> b"

  1010   by (simp add: algebra_simps)

  1011

  1012 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]

  1013

  1014 lemma diff_eq_diff_less:

  1015   "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"

  1016   by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])

  1017

  1018 lemma diff_eq_diff_less_eq:

  1019   "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"

  1020   by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])

  1021

  1022 lemma diff_mono: "a \<le> b \<Longrightarrow> d \<le> c \<Longrightarrow> a - c \<le> b - d"

  1023   by (simp add: field_simps add_mono)

  1024

  1025 lemma diff_left_mono: "b \<le> a \<Longrightarrow> c - a \<le> c - b"

  1026   by (simp add: field_simps)

  1027

  1028 lemma diff_right_mono: "a \<le> b \<Longrightarrow> a - c \<le> b - c"

  1029   by (simp add: field_simps)

  1030

  1031 lemma diff_strict_mono: "a < b \<Longrightarrow> d < c \<Longrightarrow> a - c < b - d"

  1032   by (simp add: field_simps add_strict_mono)

  1033

  1034 lemma diff_strict_left_mono: "b < a \<Longrightarrow> c - a < c - b"

  1035   by (simp add: field_simps)

  1036

  1037 lemma diff_strict_right_mono: "a < b \<Longrightarrow> a - c < b - c"

  1038   by (simp add: field_simps)

  1039

  1040 end

  1041

  1042 ML_file "Tools/group_cancel.ML"

  1043

  1044 simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =

  1045   \<open>fn phi => fn ss => try Group_Cancel.cancel_add_conv\<close>

  1046

  1047 simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") =

  1048   \<open>fn phi => fn ss => try Group_Cancel.cancel_diff_conv\<close>

  1049

  1050 simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") =

  1051   \<open>fn phi => fn ss => try Group_Cancel.cancel_eq_conv\<close>

  1052

  1053 simproc_setup group_cancel_le ("a \<le> (b::'a::ordered_ab_group_add)") =

  1054   \<open>fn phi => fn ss => try Group_Cancel.cancel_le_conv\<close>

  1055

  1056 simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") =

  1057   \<open>fn phi => fn ss => try Group_Cancel.cancel_less_conv\<close>

  1058

  1059 class linordered_ab_semigroup_add =

  1060   linorder + ordered_ab_semigroup_add

  1061

  1062 class linordered_cancel_ab_semigroup_add =

  1063   linorder + ordered_cancel_ab_semigroup_add

  1064 begin

  1065

  1066 subclass linordered_ab_semigroup_add ..

  1067

  1068 subclass ordered_ab_semigroup_add_imp_le

  1069 proof

  1070   fix a b c :: 'a

  1071   assume le: "c + a <= c + b"

  1072   show "a <= b"

  1073   proof (rule ccontr)

  1074     assume w: "~ a \<le> b"

  1075     hence "b <= a" by (simp add: linorder_not_le)

  1076     hence le2: "c + b <= c + a" by (rule add_left_mono)

  1077     have "a = b"

  1078       apply (insert le)

  1079       apply (insert le2)

  1080       apply (drule antisym, simp_all)

  1081       done

  1082     with w show False

  1083       by (simp add: linorder_not_le [symmetric])

  1084   qed

  1085 qed

  1086

  1087 end

  1088

  1089 class linordered_ab_group_add = linorder + ordered_ab_group_add

  1090 begin

  1091

  1092 subclass linordered_cancel_ab_semigroup_add ..

  1093

  1094 lemma equal_neg_zero [simp]:

  1095   "a = - a \<longleftrightarrow> a = 0"

  1096 proof

  1097   assume "a = 0" then show "a = - a" by simp

  1098 next

  1099   assume A: "a = - a" show "a = 0"

  1100   proof (cases "0 \<le> a")

  1101     case True with A have "0 \<le> - a" by auto

  1102     with le_minus_iff have "a \<le> 0" by simp

  1103     with True show ?thesis by (auto intro: order_trans)

  1104   next

  1105     case False then have B: "a \<le> 0" by auto

  1106     with A have "- a \<le> 0" by auto

  1107     with B show ?thesis by (auto intro: order_trans)

  1108   qed

  1109 qed

  1110

  1111 lemma neg_equal_zero [simp]:

  1112   "- a = a \<longleftrightarrow> a = 0"

  1113   by (auto dest: sym)

  1114

  1115 lemma neg_less_eq_nonneg [simp]:

  1116   "- a \<le> a \<longleftrightarrow> 0 \<le> a"

  1117 proof

  1118   assume A: "- a \<le> a" show "0 \<le> a"

  1119   proof (rule classical)

  1120     assume "\<not> 0 \<le> a"

  1121     then have "a < 0" by auto

  1122     with A have "- a < 0" by (rule le_less_trans)

  1123     then show ?thesis by auto

  1124   qed

  1125 next

  1126   assume A: "0 \<le> a" show "- a \<le> a"

  1127   proof (rule order_trans)

  1128     show "- a \<le> 0" using A by (simp add: minus_le_iff)

  1129   next

  1130     show "0 \<le> a" using A .

  1131   qed

  1132 qed

  1133

  1134 lemma neg_less_pos [simp]:

  1135   "- a < a \<longleftrightarrow> 0 < a"

  1136   by (auto simp add: less_le)

  1137

  1138 lemma less_eq_neg_nonpos [simp]:

  1139   "a \<le> - a \<longleftrightarrow> a \<le> 0"

  1140   using neg_less_eq_nonneg [of "- a"] by simp

  1141

  1142 lemma less_neg_neg [simp]:

  1143   "a < - a \<longleftrightarrow> a < 0"

  1144   using neg_less_pos [of "- a"] by simp

  1145

  1146 lemma double_zero [simp]:

  1147   "a + a = 0 \<longleftrightarrow> a = 0"

  1148 proof

  1149   assume assm: "a + a = 0"

  1150   then have a: "- a = a" by (rule minus_unique)

  1151   then show "a = 0" by (simp only: neg_equal_zero)

  1152 qed simp

  1153

  1154 lemma double_zero_sym [simp]:

  1155   "0 = a + a \<longleftrightarrow> a = 0"

  1156   by (rule, drule sym) simp_all

  1157

  1158 lemma zero_less_double_add_iff_zero_less_single_add [simp]:

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

  1160 proof

  1161   assume "0 < a + a"

  1162   then have "0 - a < a" by (simp only: diff_less_eq)

  1163   then have "- a < a" by simp

  1164   then show "0 < a" by simp

  1165 next

  1166   assume "0 < a"

  1167   with this have "0 + 0 < a + a"

  1168     by (rule add_strict_mono)

  1169   then show "0 < a + a" by simp

  1170 qed

  1171

  1172 lemma zero_le_double_add_iff_zero_le_single_add [simp]:

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

  1174   by (auto simp add: le_less)

  1175

  1176 lemma double_add_less_zero_iff_single_add_less_zero [simp]:

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

  1178 proof -

  1179   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"

  1180     by (simp add: not_less)

  1181   then show ?thesis by simp

  1182 qed

  1183

  1184 lemma double_add_le_zero_iff_single_add_le_zero [simp]:

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

  1186 proof -

  1187   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"

  1188     by (simp add: not_le)

  1189   then show ?thesis by simp

  1190 qed

  1191

  1192 lemma minus_max_eq_min:

  1193   "- max x y = min (-x) (-y)"

  1194   by (auto simp add: max_def min_def)

  1195

  1196 lemma minus_min_eq_max:

  1197   "- min x y = max (-x) (-y)"

  1198   by (auto simp add: max_def min_def)

  1199

  1200 end

  1201

  1202 class abs =

  1203   fixes abs :: "'a \<Rightarrow> 'a"

  1204 begin

  1205

  1206 notation (xsymbols)

  1207   abs  ("\<bar>_\<bar>")

  1208

  1209 notation (HTML output)

  1210   abs  ("\<bar>_\<bar>")

  1211

  1212 end

  1213

  1214 class sgn =

  1215   fixes sgn :: "'a \<Rightarrow> 'a"

  1216

  1217 class abs_if = minus + uminus + ord + zero + abs +

  1218   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"

  1219

  1220 class sgn_if = minus + uminus + zero + one + ord + sgn +

  1221   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"

  1222 begin

  1223

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

  1225   by (simp add:sgn_if)

  1226

  1227 end

  1228

  1229 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +

  1230   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"

  1231     and abs_ge_self: "a \<le> \<bar>a\<bar>"

  1232     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"

  1233     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"

  1234     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"

  1235 begin

  1236

  1237 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"

  1238   unfolding neg_le_0_iff_le by simp

  1239

  1240 lemma abs_of_nonneg [simp]:

  1241   assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"

  1242 proof (rule antisym)

  1243   from nonneg le_imp_neg_le have "- a \<le> 0" by simp

  1244   from this nonneg have "- a \<le> a" by (rule order_trans)

  1245   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)

  1246 qed (rule abs_ge_self)

  1247

  1248 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"

  1249 by (rule antisym)

  1250    (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])

  1251

  1252 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"

  1253 proof -

  1254   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"

  1255   proof (rule antisym)

  1256     assume zero: "\<bar>a\<bar> = 0"

  1257     with abs_ge_self show "a \<le> 0" by auto

  1258     from zero have "\<bar>-a\<bar> = 0" by simp

  1259     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto

  1260     with neg_le_0_iff_le show "0 \<le> a" by auto

  1261   qed

  1262   then show ?thesis by auto

  1263 qed

  1264

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

  1266 by simp

  1267

  1268 lemma abs_0_eq [simp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"

  1269 proof -

  1270   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)

  1271   thus ?thesis by simp

  1272 qed

  1273

  1274 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"

  1275 proof

  1276   assume "\<bar>a\<bar> \<le> 0"

  1277   then have "\<bar>a\<bar> = 0" by (rule antisym) simp

  1278   thus "a = 0" by simp

  1279 next

  1280   assume "a = 0"

  1281   thus "\<bar>a\<bar> \<le> 0" by simp

  1282 qed

  1283

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

  1285 by (simp add: less_le)

  1286

  1287 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"

  1288 proof -

  1289   have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto

  1290   show ?thesis by (simp add: a)

  1291 qed

  1292

  1293 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"

  1294 proof -

  1295   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)

  1296   then show ?thesis by simp

  1297 qed

  1298

  1299 lemma abs_minus_commute:

  1300   "\<bar>a - b\<bar> = \<bar>b - a\<bar>"

  1301 proof -

  1302   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)

  1303   also have "... = \<bar>b - a\<bar>" by simp

  1304   finally show ?thesis .

  1305 qed

  1306

  1307 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"

  1308 by (rule abs_of_nonneg, rule less_imp_le)

  1309

  1310 lemma abs_of_nonpos [simp]:

  1311   assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"

  1312 proof -

  1313   let ?b = "- a"

  1314   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"

  1315   unfolding abs_minus_cancel [of "?b"]

  1316   unfolding neg_le_0_iff_le [of "?b"]

  1317   unfolding minus_minus by (erule abs_of_nonneg)

  1318   then show ?thesis using assms by auto

  1319 qed

  1320

  1321 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"

  1322 by (rule abs_of_nonpos, rule less_imp_le)

  1323

  1324 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"

  1325 by (insert abs_ge_self, blast intro: order_trans)

  1326

  1327 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"

  1328 by (insert abs_le_D1 [of "- a"], simp)

  1329

  1330 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"

  1331 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)

  1332

  1333 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"

  1334 proof -

  1335   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"

  1336     by (simp add: algebra_simps)

  1337   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"

  1338     by (simp add: abs_triangle_ineq)

  1339   then show ?thesis

  1340     by (simp add: algebra_simps)

  1341 qed

  1342

  1343 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"

  1344   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)

  1345

  1346 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"

  1347   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)

  1348

  1349 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"

  1350 proof -

  1351   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (simp add: algebra_simps)

  1352   also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)

  1353   finally show ?thesis by simp

  1354 qed

  1355

  1356 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"

  1357 proof -

  1358   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: algebra_simps)

  1359   also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)

  1360   finally show ?thesis .

  1361 qed

  1362

  1363 lemma abs_add_abs [simp]:

  1364   "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")

  1365 proof (rule antisym)

  1366   show "?L \<ge> ?R" by(rule abs_ge_self)

  1367 next

  1368   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)

  1369   also have "\<dots> = ?R" by simp

  1370   finally show "?L \<le> ?R" .

  1371 qed

  1372

  1373 end

  1374

  1375 lemma dense_eq0_I:

  1376   fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"

  1377   shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) ==> x = 0"

  1378   apply (cases "abs x=0", simp)

  1379   apply (simp only: zero_less_abs_iff [symmetric])

  1380   apply (drule dense)

  1381   apply (auto simp add: not_less [symmetric])

  1382   done

  1383

  1384 hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus

  1385

  1386 lemmas add_0 = add_0_left -- \<open>FIXME duplicate\<close>

  1387 lemmas mult_1 = mult_1_left -- \<open>FIXME duplicate\<close>

  1388 lemmas ab_left_minus = left_minus -- \<open>FIXME duplicate\<close>

  1389 lemmas diff_diff_eq = diff_diff_add -- \<open>FIXME duplicate\<close>

  1390

  1391

  1392 subsection \<open>Tools setup\<close>

  1393

  1394 lemma add_mono_thms_linordered_semiring:

  1395   fixes i j k :: "'a::ordered_ab_semigroup_add"

  1396   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"

  1397     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"

  1398     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"

  1399     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"

  1400 by (rule add_mono, clarify+)+

  1401

  1402 lemma add_mono_thms_linordered_field:

  1403   fixes i j k :: "'a::ordered_cancel_ab_semigroup_add"

  1404   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"

  1405     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"

  1406     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"

  1407     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"

  1408     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"

  1409 by (auto intro: add_strict_right_mono add_strict_left_mono

  1410   add_less_le_mono add_le_less_mono add_strict_mono)

  1411

  1412 code_identifier

  1413   code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith

  1414

  1415 end

  1416