src/HOL/Groups.thy
author haftmann
Sat Jun 11 16:22:42 2016 +0200 (2016-06-11)
changeset 63290 9ac558ab0906
parent 63145 703edebd1d92
child 63325 1086d56cde86
permissions -rw-r--r--
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
     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 \<open>algebra_simps\<close> 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 \<open>field_simps\<close>.\<close>
    24 
    25 named_theorems algebra_simps "algebra simplification rules"
    26 
    27 
    28 text\<open>Lemmas \<open>field_simps\<close> 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 \<open>algebra_simps\<close>.\<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 "\<^bold>*" 70)
    46   assumes assoc [ac_simps]: "a \<^bold>* b \<^bold>* c = a \<^bold>* (b \<^bold>* c)"
    47 
    48 locale abel_semigroup = semigroup +
    49   assumes commute [ac_simps]: "a \<^bold>* b = b \<^bold>* a"
    50 begin
    51 
    52 lemma left_commute [ac_simps]:
    53   "b \<^bold>* (a \<^bold>* c) = a \<^bold>* (b \<^bold>* c)"
    54 proof -
    55   have "(b \<^bold>* a) \<^bold>* c = (a \<^bold>* b) \<^bold>* 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 ("\<^bold>1")
    65   assumes left_neutral [simp]: "\<^bold>1 \<^bold>* a = a"
    66   assumes right_neutral [simp]: "a \<^bold>* \<^bold>1 = a"
    67 
    68 locale comm_monoid = abel_semigroup +
    69   fixes z :: 'a ("\<^bold>1")
    70   assumes comm_neutral: "a \<^bold>* \<^bold>1 = a"
    71 begin
    72 
    73 sublocale monoid
    74   by standard (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> \<comment> \<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 standard (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 standard (fact add_commute)
   147 
   148 declare add.left_commute [algebra_simps, field_simps]
   149 
   150 lemmas add_ac = add.assoc add.commute add.left_commute
   151 
   152 end
   153 
   154 hide_fact add_commute
   155 
   156 lemmas 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 standard (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 standard (fact mult_commute)
   175 
   176 declare mult.left_commute [algebra_simps, field_simps]
   177 
   178 lemmas mult_ac = mult.assoc mult.commute mult.left_commute
   179 
   180 end
   181 
   182 hide_fact mult_commute
   183 
   184 lemmas 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 standard (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 standard (simp_all add: add_0 add.commute [of _ 0])
   205 
   206 sublocale add: comm_monoid plus 0
   207   by standard (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 standard (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 standard (simp_all add: mult_1 mult.commute [of _ 1])
   230 
   231 sublocale mult: comm_monoid times 1
   232   by standard (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 lemma add_cancel_right_right [simp]:
   314   "a = a + b \<longleftrightarrow> b = 0" (is "?P \<longleftrightarrow> ?Q")
   315 proof
   316   assume ?Q then show ?P by simp
   317 next
   318   assume ?P then have "a - a = a + b - a" by simp
   319   then show ?Q by simp
   320 qed
   321 
   322 lemma add_cancel_right_left [simp]:
   323   "a = b + a \<longleftrightarrow> b = 0"
   324   using add_cancel_right_right [of a b] by (simp add: ac_simps)
   325 
   326 lemma add_cancel_left_right [simp]:
   327   "a + b = a \<longleftrightarrow> b = 0"
   328   by (auto dest: sym)
   329 
   330 lemma add_cancel_left_left [simp]:
   331   "b + a = a \<longleftrightarrow> b = 0"
   332   by (auto dest: sym)
   333 
   334 end
   335 
   336 class comm_monoid_diff = cancel_comm_monoid_add +
   337   assumes zero_diff [simp]: "0 - a = 0"
   338 begin
   339 
   340 lemma diff_add_zero [simp]:
   341   "a - (a + b) = 0"
   342 proof -
   343   have "a - (a + b) = (a + 0) - (a + b)" by simp
   344   also have "\<dots> = 0" by (simp only: add_diff_cancel_left zero_diff)
   345   finally show ?thesis .
   346 qed
   347 
   348 end
   349 
   350 
   351 subsection \<open>Groups\<close>
   352 
   353 class group_add = minus + uminus + monoid_add +
   354   assumes left_minus [simp]: "- a + a = 0"
   355   assumes add_uminus_conv_diff [simp]: "a + (- b) = a - b"
   356 begin
   357 
   358 lemma diff_conv_add_uminus:
   359   "a - b = a + (- b)"
   360   by simp
   361 
   362 lemma minus_unique:
   363   assumes "a + b = 0" shows "- a = b"
   364 proof -
   365   have "- a = - a + (a + b)" using assms by simp
   366   also have "\<dots> = b" by (simp add: add.assoc [symmetric])
   367   finally show ?thesis .
   368 qed
   369 
   370 lemma minus_zero [simp]: "- 0 = 0"
   371 proof -
   372   have "0 + 0 = 0" by (rule add_0_right)
   373   thus "- 0 = 0" by (rule minus_unique)
   374 qed
   375 
   376 lemma minus_minus [simp]: "- (- a) = a"
   377 proof -
   378   have "- a + a = 0" by (rule left_minus)
   379   thus "- (- a) = a" by (rule minus_unique)
   380 qed
   381 
   382 lemma right_minus: "a + - a = 0"
   383 proof -
   384   have "a + - a = - (- a) + - a" by simp
   385   also have "\<dots> = 0" by (rule left_minus)
   386   finally show ?thesis .
   387 qed
   388 
   389 lemma diff_self [simp]:
   390   "a - a = 0"
   391   using right_minus [of a] by simp
   392 
   393 subclass cancel_semigroup_add
   394 proof
   395   fix a b c :: 'a
   396   assume "a + b = a + c"
   397   then have "- a + a + b = - a + a + c"
   398     unfolding add.assoc by simp
   399   then show "b = c" by simp
   400 next
   401   fix a b c :: 'a
   402   assume "b + a = c + a"
   403   then have "b + a + - a = c + a  + - a" by simp
   404   then show "b = c" unfolding add.assoc by simp
   405 qed
   406 
   407 lemma minus_add_cancel [simp]:
   408   "- a + (a + b) = b"
   409   by (simp add: add.assoc [symmetric])
   410 
   411 lemma add_minus_cancel [simp]:
   412   "a + (- a + b) = b"
   413   by (simp add: add.assoc [symmetric])
   414 
   415 lemma diff_add_cancel [simp]:
   416   "a - b + b = a"
   417   by (simp only: diff_conv_add_uminus add.assoc) simp
   418 
   419 lemma add_diff_cancel [simp]:
   420   "a + b - b = a"
   421   by (simp only: diff_conv_add_uminus add.assoc) simp
   422 
   423 lemma minus_add:
   424   "- (a + b) = - b + - a"
   425 proof -
   426   have "(a + b) + (- b + - a) = 0"
   427     by (simp only: add.assoc add_minus_cancel) simp
   428   then show "- (a + b) = - b + - a"
   429     by (rule minus_unique)
   430 qed
   431 
   432 lemma right_minus_eq [simp]:
   433   "a - b = 0 \<longleftrightarrow> a = b"
   434 proof
   435   assume "a - b = 0"
   436   have "a = (a - b) + b" by (simp add: add.assoc)
   437   also have "\<dots> = b" using \<open>a - b = 0\<close> by simp
   438   finally show "a = b" .
   439 next
   440   assume "a = b" thus "a - b = 0" by simp
   441 qed
   442 
   443 lemma eq_iff_diff_eq_0:
   444   "a = b \<longleftrightarrow> a - b = 0"
   445   by (fact right_minus_eq [symmetric])
   446 
   447 lemma diff_0 [simp]:
   448   "0 - a = - a"
   449   by (simp only: diff_conv_add_uminus add_0_left)
   450 
   451 lemma diff_0_right [simp]:
   452   "a - 0 = a"
   453   by (simp only: diff_conv_add_uminus minus_zero add_0_right)
   454 
   455 lemma diff_minus_eq_add [simp]:
   456   "a - - b = a + b"
   457   by (simp only: diff_conv_add_uminus minus_minus)
   458 
   459 lemma neg_equal_iff_equal [simp]:
   460   "- a = - b \<longleftrightarrow> a = b"
   461 proof
   462   assume "- a = - b"
   463   hence "- (- a) = - (- b)" by simp
   464   thus "a = b" by simp
   465 next
   466   assume "a = b"
   467   thus "- a = - b" by simp
   468 qed
   469 
   470 lemma neg_equal_0_iff_equal [simp]:
   471   "- a = 0 \<longleftrightarrow> a = 0"
   472   by (subst neg_equal_iff_equal [symmetric]) simp
   473 
   474 lemma neg_0_equal_iff_equal [simp]:
   475   "0 = - a \<longleftrightarrow> 0 = a"
   476   by (subst neg_equal_iff_equal [symmetric]) simp
   477 
   478 text\<open>The next two equations can make the simplifier loop!\<close>
   479 
   480 lemma equation_minus_iff:
   481   "a = - b \<longleftrightarrow> b = - a"
   482 proof -
   483   have "- (- a) = - b \<longleftrightarrow> - a = b" by (rule neg_equal_iff_equal)
   484   thus ?thesis by (simp add: eq_commute)
   485 qed
   486 
   487 lemma minus_equation_iff:
   488   "- a = b \<longleftrightarrow> - b = a"
   489 proof -
   490   have "- a = - (- b) \<longleftrightarrow> a = -b" by (rule neg_equal_iff_equal)
   491   thus ?thesis by (simp add: eq_commute)
   492 qed
   493 
   494 lemma eq_neg_iff_add_eq_0:
   495   "a = - b \<longleftrightarrow> a + b = 0"
   496 proof
   497   assume "a = - b" then show "a + b = 0" by simp
   498 next
   499   assume "a + b = 0"
   500   moreover have "a + (b + - b) = (a + b) + - b"
   501     by (simp only: add.assoc)
   502   ultimately show "a = - b" by simp
   503 qed
   504 
   505 lemma add_eq_0_iff2:
   506   "a + b = 0 \<longleftrightarrow> a = - b"
   507   by (fact eq_neg_iff_add_eq_0 [symmetric])
   508 
   509 lemma neg_eq_iff_add_eq_0:
   510   "- a = b \<longleftrightarrow> a + b = 0"
   511   by (auto simp add: add_eq_0_iff2)
   512 
   513 lemma add_eq_0_iff:
   514   "a + b = 0 \<longleftrightarrow> b = - a"
   515   by (auto simp add: neg_eq_iff_add_eq_0 [symmetric])
   516 
   517 lemma minus_diff_eq [simp]:
   518   "- (a - b) = b - a"
   519   by (simp only: neg_eq_iff_add_eq_0 diff_conv_add_uminus add.assoc minus_add_cancel) simp
   520 
   521 lemma add_diff_eq [algebra_simps, field_simps]:
   522   "a + (b - c) = (a + b) - c"
   523   by (simp only: diff_conv_add_uminus add.assoc)
   524 
   525 lemma diff_add_eq_diff_diff_swap:
   526   "a - (b + c) = a - c - b"
   527   by (simp only: diff_conv_add_uminus add.assoc minus_add)
   528 
   529 lemma diff_eq_eq [algebra_simps, field_simps]:
   530   "a - b = c \<longleftrightarrow> a = c + b"
   531   by auto
   532 
   533 lemma eq_diff_eq [algebra_simps, field_simps]:
   534   "a = c - b \<longleftrightarrow> a + b = c"
   535   by auto
   536 
   537 lemma diff_diff_eq2 [algebra_simps, field_simps]:
   538   "a - (b - c) = (a + c) - b"
   539   by (simp only: diff_conv_add_uminus add.assoc) simp
   540 
   541 lemma diff_eq_diff_eq:
   542   "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
   543   by (simp only: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])
   544 
   545 end
   546 
   547 class ab_group_add = minus + uminus + comm_monoid_add +
   548   assumes ab_left_minus: "- a + a = 0"
   549   assumes ab_diff_conv_add_uminus: "a - b = a + (- b)"
   550 begin
   551 
   552 subclass group_add
   553   proof qed (simp_all add: ab_left_minus ab_diff_conv_add_uminus)
   554 
   555 subclass cancel_comm_monoid_add
   556 proof
   557   fix a b c :: 'a
   558   have "b + a - a = b"
   559     by simp
   560   then show "a + b - a = b"
   561     by (simp add: ac_simps)
   562   show "a - b - c = a - (b + c)"
   563     by (simp add: algebra_simps)
   564 qed
   565 
   566 lemma uminus_add_conv_diff [simp]:
   567   "- a + b = b - a"
   568   by (simp add: add.commute)
   569 
   570 lemma minus_add_distrib [simp]:
   571   "- (a + b) = - a + - b"
   572   by (simp add: algebra_simps)
   573 
   574 lemma diff_add_eq [algebra_simps, field_simps]:
   575   "(a - b) + c = (a + c) - b"
   576   by (simp add: algebra_simps)
   577 
   578 end
   579 
   580 
   581 subsection \<open>(Partially) Ordered Groups\<close>
   582 
   583 text \<open>
   584   The theory of partially ordered groups is taken from the books:
   585   \begin{itemize}
   586   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979
   587   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
   588   \end{itemize}
   589   Most of the used notions can also be looked up in
   590   \begin{itemize}
   591   \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
   592   \item \emph{Algebra I} by van der Waerden, Springer.
   593   \end{itemize}
   594 \<close>
   595 
   596 class ordered_ab_semigroup_add = order + ab_semigroup_add +
   597   assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
   598 begin
   599 
   600 lemma add_right_mono:
   601   "a \<le> b \<Longrightarrow> a + c \<le> b + c"
   602 by (simp add: add.commute [of _ c] add_left_mono)
   603 
   604 text \<open>non-strict, in both arguments\<close>
   605 lemma add_mono:
   606   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
   607   apply (erule add_right_mono [THEN order_trans])
   608   apply (simp add: add.commute add_left_mono)
   609   done
   610 
   611 end
   612 
   613 text\<open>Strict monotonicity in both arguments\<close>
   614 class strict_ordered_ab_semigroup_add = ordered_ab_semigroup_add +
   615   assumes add_strict_mono: "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   616 
   617 class ordered_cancel_ab_semigroup_add =
   618   ordered_ab_semigroup_add + cancel_ab_semigroup_add
   619 begin
   620 
   621 lemma add_strict_left_mono:
   622   "a < b \<Longrightarrow> c + a < c + b"
   623 by (auto simp add: less_le add_left_mono)
   624 
   625 lemma add_strict_right_mono:
   626   "a < b \<Longrightarrow> a + c < b + c"
   627 by (simp add: add.commute [of _ c] add_strict_left_mono)
   628 
   629 subclass strict_ordered_ab_semigroup_add
   630   apply standard
   631   apply (erule add_strict_right_mono [THEN less_trans])
   632   apply (erule add_strict_left_mono)
   633   done
   634 
   635 lemma add_less_le_mono:
   636   "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
   637 apply (erule add_strict_right_mono [THEN less_le_trans])
   638 apply (erule add_left_mono)
   639 done
   640 
   641 lemma add_le_less_mono:
   642   "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   643 apply (erule add_right_mono [THEN le_less_trans])
   644 apply (erule add_strict_left_mono)
   645 done
   646 
   647 end
   648 
   649 class ordered_ab_semigroup_add_imp_le = ordered_cancel_ab_semigroup_add +
   650   assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
   651 begin
   652 
   653 lemma add_less_imp_less_left:
   654   assumes less: "c + a < c + b" shows "a < b"
   655 proof -
   656   from less have le: "c + a <= c + b" by (simp add: order_le_less)
   657   have "a <= b"
   658     apply (insert le)
   659     apply (drule add_le_imp_le_left)
   660     by (insert le, drule add_le_imp_le_left, assumption)
   661   moreover have "a \<noteq> b"
   662   proof (rule ccontr)
   663     assume "~(a \<noteq> b)"
   664     then have "a = b" by simp
   665     then have "c + a = c + b" by simp
   666     with less show "False"by simp
   667   qed
   668   ultimately show "a < b" by (simp add: order_le_less)
   669 qed
   670 
   671 lemma add_less_imp_less_right:
   672   "a + c < b + c \<Longrightarrow> a < b"
   673 apply (rule add_less_imp_less_left [of c])
   674 apply (simp add: add.commute)
   675 done
   676 
   677 lemma add_less_cancel_left [simp]:
   678   "c + a < c + b \<longleftrightarrow> a < b"
   679   by (blast intro: add_less_imp_less_left add_strict_left_mono)
   680 
   681 lemma add_less_cancel_right [simp]:
   682   "a + c < b + c \<longleftrightarrow> a < b"
   683   by (blast intro: add_less_imp_less_right add_strict_right_mono)
   684 
   685 lemma add_le_cancel_left [simp]:
   686   "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
   687   by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono)
   688 
   689 lemma add_le_cancel_right [simp]:
   690   "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
   691   by (simp add: add.commute [of a c] add.commute [of b c])
   692 
   693 lemma add_le_imp_le_right:
   694   "a + c \<le> b + c \<Longrightarrow> a \<le> b"
   695 by simp
   696 
   697 lemma max_add_distrib_left:
   698   "max x y + z = max (x + z) (y + z)"
   699   unfolding max_def by auto
   700 
   701 lemma min_add_distrib_left:
   702   "min x y + z = min (x + z) (y + z)"
   703   unfolding min_def by auto
   704 
   705 lemma max_add_distrib_right:
   706   "x + max y z = max (x + y) (x + z)"
   707   unfolding max_def by auto
   708 
   709 lemma min_add_distrib_right:
   710   "x + min y z = min (x + y) (x + z)"
   711   unfolding min_def by auto
   712 
   713 end
   714 
   715 subsection \<open>Support for reasoning about signs\<close>
   716 
   717 class ordered_comm_monoid_add = comm_monoid_add + ordered_ab_semigroup_add
   718 begin
   719 
   720 lemma add_nonneg_nonneg [simp]:
   721   "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
   722   using add_mono[of 0 a 0 b] by simp
   723 
   724 lemma add_nonpos_nonpos:
   725   "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> a + b \<le> 0"
   726   using add_mono[of a 0 b 0] by simp
   727 
   728 lemma add_nonneg_eq_0_iff:
   729   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   730   using add_left_mono[of 0 y x] add_right_mono[of 0 x y] by auto
   731 
   732 lemma add_nonpos_eq_0_iff:
   733   "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   734   using add_left_mono[of y 0 x] add_right_mono[of x 0 y] by auto
   735 
   736 lemma add_increasing:
   737   "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
   738   by (insert add_mono [of 0 a b c], simp)
   739 
   740 lemma add_increasing2:
   741   "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
   742   by (simp add: add_increasing add.commute [of a])
   743 
   744 lemma add_decreasing:
   745   "a \<le> 0 \<Longrightarrow> c \<le> b \<Longrightarrow> a + c \<le> b"
   746   using add_mono[of a 0 c b] by simp
   747 
   748 lemma add_decreasing2:
   749   "c \<le> 0 \<Longrightarrow> a \<le> b \<Longrightarrow> a + c \<le> b"
   750   using add_mono[of a b c 0] by simp
   751 
   752 lemma add_pos_nonneg: "0 < a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < a + b"
   753   using less_le_trans[of 0 a "a + b"] by (simp add: add_increasing2)
   754 
   755 lemma add_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a + b"
   756   by (intro add_pos_nonneg less_imp_le)
   757 
   758 lemma add_nonneg_pos: "0 \<le> a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a + b"
   759   using add_pos_nonneg[of b a] by (simp add: add_commute)
   760 
   761 lemma add_neg_nonpos: "a < 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> a + b < 0"
   762   using le_less_trans[of "a + b" a 0] by (simp add: add_decreasing2)
   763 
   764 lemma add_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> a + b < 0"
   765   by (intro add_neg_nonpos less_imp_le)
   766 
   767 lemma add_nonpos_neg: "a \<le> 0 \<Longrightarrow> b < 0 \<Longrightarrow> a + b < 0"
   768   using add_neg_nonpos[of b a] by (simp add: add_commute)
   769 
   770 lemmas add_sign_intros =
   771   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
   772   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
   773 
   774 end
   775 
   776 class strict_ordered_comm_monoid_add = comm_monoid_add + strict_ordered_ab_semigroup_add
   777 begin
   778 
   779 lemma pos_add_strict:
   780   shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   781   using add_strict_mono [of 0 a b c] by simp
   782 
   783 end
   784 
   785 class ordered_cancel_comm_monoid_add = ordered_comm_monoid_add + cancel_ab_semigroup_add
   786 begin
   787 
   788 subclass ordered_cancel_ab_semigroup_add ..
   789 subclass strict_ordered_comm_monoid_add ..
   790 
   791 lemma add_strict_increasing:
   792   "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
   793   by (insert add_less_le_mono [of 0 a b c], simp)
   794 
   795 lemma add_strict_increasing2:
   796   "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   797   by (insert add_le_less_mono [of 0 a b c], simp)
   798 
   799 end
   800 
   801 class ordered_ab_group_add = ab_group_add + ordered_ab_semigroup_add
   802 begin
   803 
   804 subclass ordered_cancel_ab_semigroup_add ..
   805 
   806 subclass ordered_ab_semigroup_add_imp_le
   807 proof
   808   fix a b c :: 'a
   809   assume "c + a \<le> c + b"
   810   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
   811   hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add.assoc)
   812   thus "a \<le> b" by simp
   813 qed
   814 
   815 subclass ordered_cancel_comm_monoid_add ..
   816 
   817 lemma add_less_same_cancel1 [simp]:
   818   "b + a < b \<longleftrightarrow> a < 0"
   819   using add_less_cancel_left [of _ _ 0] by simp
   820 
   821 lemma add_less_same_cancel2 [simp]:
   822   "a + b < b \<longleftrightarrow> a < 0"
   823   using add_less_cancel_right [of _ _ 0] by simp
   824 
   825 lemma less_add_same_cancel1 [simp]:
   826   "a < a + b \<longleftrightarrow> 0 < b"
   827   using add_less_cancel_left [of _ 0] by simp
   828 
   829 lemma less_add_same_cancel2 [simp]:
   830   "a < b + a \<longleftrightarrow> 0 < b"
   831   using add_less_cancel_right [of 0] by simp
   832 
   833 lemma add_le_same_cancel1 [simp]:
   834   "b + a \<le> b \<longleftrightarrow> a \<le> 0"
   835   using add_le_cancel_left [of _ _ 0] by simp
   836 
   837 lemma add_le_same_cancel2 [simp]:
   838   "a + b \<le> b \<longleftrightarrow> a \<le> 0"
   839   using add_le_cancel_right [of _ _ 0] by simp
   840 
   841 lemma le_add_same_cancel1 [simp]:
   842   "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
   843   using add_le_cancel_left [of _ 0] by simp
   844 
   845 lemma le_add_same_cancel2 [simp]:
   846   "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
   847   using add_le_cancel_right [of 0] by simp
   848 
   849 lemma max_diff_distrib_left:
   850   shows "max x y - z = max (x - z) (y - z)"
   851   using max_add_distrib_left [of x y "- z"] by simp
   852 
   853 lemma min_diff_distrib_left:
   854   shows "min x y - z = min (x - z) (y - z)"
   855   using min_add_distrib_left [of x y "- z"] by simp
   856 
   857 lemma le_imp_neg_le:
   858   assumes "a \<le> b" shows "-b \<le> -a"
   859 proof -
   860   have "-a+a \<le> -a+b" using \<open>a \<le> b\<close> by (rule add_left_mono)
   861   then have "0 \<le> -a+b" by simp
   862   then have "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono)
   863   then show ?thesis by (simp add: algebra_simps)
   864 qed
   865 
   866 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
   867 proof
   868   assume "- b \<le> - a"
   869   hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
   870   thus "a\<le>b" by simp
   871 next
   872   assume "a\<le>b"
   873   thus "-b \<le> -a" by (rule le_imp_neg_le)
   874 qed
   875 
   876 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   877 by (subst neg_le_iff_le [symmetric], simp)
   878 
   879 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
   880 by (subst neg_le_iff_le [symmetric], simp)
   881 
   882 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
   883 by (force simp add: less_le)
   884 
   885 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
   886 by (subst neg_less_iff_less [symmetric], simp)
   887 
   888 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
   889 by (subst neg_less_iff_less [symmetric], simp)
   890 
   891 text\<open>The next several equations can make the simplifier loop!\<close>
   892 
   893 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
   894 proof -
   895   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
   896   thus ?thesis by simp
   897 qed
   898 
   899 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
   900 proof -
   901   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
   902   thus ?thesis by simp
   903 qed
   904 
   905 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
   906 proof -
   907   have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
   908   have "(- (- a) <= -b) = (b <= - a)"
   909     apply (auto simp only: le_less)
   910     apply (drule mm)
   911     apply (simp_all)
   912     apply (drule mm[simplified], assumption)
   913     done
   914   then show ?thesis by simp
   915 qed
   916 
   917 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
   918 by (auto simp add: le_less minus_less_iff)
   919 
   920 lemma diff_less_0_iff_less [simp]:
   921   "a - b < 0 \<longleftrightarrow> a < b"
   922 proof -
   923   have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by simp
   924   also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
   925   finally show ?thesis .
   926 qed
   927 
   928 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
   929 
   930 lemma diff_less_eq [algebra_simps, field_simps]:
   931   "a - b < c \<longleftrightarrow> a < c + b"
   932 apply (subst less_iff_diff_less_0 [of a])
   933 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
   934 apply (simp add: algebra_simps)
   935 done
   936 
   937 lemma less_diff_eq[algebra_simps, field_simps]:
   938   "a < c - b \<longleftrightarrow> a + b < c"
   939 apply (subst less_iff_diff_less_0 [of "a + b"])
   940 apply (subst less_iff_diff_less_0 [of a])
   941 apply (simp add: algebra_simps)
   942 done
   943 
   944 lemma diff_gt_0_iff_gt [simp]:
   945   "a - b > 0 \<longleftrightarrow> a > b"
   946   by (simp add: less_diff_eq)
   947 
   948 lemma diff_le_eq [algebra_simps, field_simps]:
   949   "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
   950   by (auto simp add: le_less diff_less_eq )
   951 
   952 lemma le_diff_eq [algebra_simps, field_simps]:
   953   "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
   954   by (auto simp add: le_less less_diff_eq)
   955 
   956 lemma diff_le_0_iff_le [simp]:
   957   "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
   958   by (simp add: algebra_simps)
   959 
   960 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
   961 
   962 lemma diff_ge_0_iff_ge [simp]:
   963   "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
   964   by (simp add: le_diff_eq)
   965 
   966 lemma diff_eq_diff_less:
   967   "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
   968   by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
   969 
   970 lemma diff_eq_diff_less_eq:
   971   "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
   972   by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
   973 
   974 lemma diff_mono: "a \<le> b \<Longrightarrow> d \<le> c \<Longrightarrow> a - c \<le> b - d"
   975   by (simp add: field_simps add_mono)
   976 
   977 lemma diff_left_mono: "b \<le> a \<Longrightarrow> c - a \<le> c - b"
   978   by (simp add: field_simps)
   979 
   980 lemma diff_right_mono: "a \<le> b \<Longrightarrow> a - c \<le> b - c"
   981   by (simp add: field_simps)
   982 
   983 lemma diff_strict_mono: "a < b \<Longrightarrow> d < c \<Longrightarrow> a - c < b - d"
   984   by (simp add: field_simps add_strict_mono)
   985 
   986 lemma diff_strict_left_mono: "b < a \<Longrightarrow> c - a < c - b"
   987   by (simp add: field_simps)
   988 
   989 lemma diff_strict_right_mono: "a < b \<Longrightarrow> a - c < b - c"
   990   by (simp add: field_simps)
   991 
   992 end
   993 
   994 ML_file "Tools/group_cancel.ML"
   995 
   996 simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =
   997   \<open>fn phi => fn ss => try Group_Cancel.cancel_add_conv\<close>
   998 
   999 simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") =
  1000   \<open>fn phi => fn ss => try Group_Cancel.cancel_diff_conv\<close>
  1001 
  1002 simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") =
  1003   \<open>fn phi => fn ss => try Group_Cancel.cancel_eq_conv\<close>
  1004 
  1005 simproc_setup group_cancel_le ("a \<le> (b::'a::ordered_ab_group_add)") =
  1006   \<open>fn phi => fn ss => try Group_Cancel.cancel_le_conv\<close>
  1007 
  1008 simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") =
  1009   \<open>fn phi => fn ss => try Group_Cancel.cancel_less_conv\<close>
  1010 
  1011 class linordered_ab_semigroup_add =
  1012   linorder + ordered_ab_semigroup_add
  1013 
  1014 class linordered_cancel_ab_semigroup_add =
  1015   linorder + ordered_cancel_ab_semigroup_add
  1016 begin
  1017 
  1018 subclass linordered_ab_semigroup_add ..
  1019 
  1020 subclass ordered_ab_semigroup_add_imp_le
  1021 proof
  1022   fix a b c :: 'a
  1023   assume le: "c + a <= c + b"
  1024   show "a <= b"
  1025   proof (rule ccontr)
  1026     assume w: "~ a \<le> b"
  1027     hence "b <= a" by (simp add: linorder_not_le)
  1028     hence le2: "c + b <= c + a" by (rule add_left_mono)
  1029     have "a = b"
  1030       apply (insert le)
  1031       apply (insert le2)
  1032       apply (drule antisym, simp_all)
  1033       done
  1034     with w show False
  1035       by (simp add: linorder_not_le [symmetric])
  1036   qed
  1037 qed
  1038 
  1039 end
  1040 
  1041 class linordered_ab_group_add = linorder + ordered_ab_group_add
  1042 begin
  1043 
  1044 subclass linordered_cancel_ab_semigroup_add ..
  1045 
  1046 lemma equal_neg_zero [simp]:
  1047   "a = - a \<longleftrightarrow> a = 0"
  1048 proof
  1049   assume "a = 0" then show "a = - a" by simp
  1050 next
  1051   assume A: "a = - a" show "a = 0"
  1052   proof (cases "0 \<le> a")
  1053     case True with A have "0 \<le> - a" by auto
  1054     with le_minus_iff have "a \<le> 0" by simp
  1055     with True show ?thesis by (auto intro: order_trans)
  1056   next
  1057     case False then have B: "a \<le> 0" by auto
  1058     with A have "- a \<le> 0" by auto
  1059     with B show ?thesis by (auto intro: order_trans)
  1060   qed
  1061 qed
  1062 
  1063 lemma neg_equal_zero [simp]:
  1064   "- a = a \<longleftrightarrow> a = 0"
  1065   by (auto dest: sym)
  1066 
  1067 lemma neg_less_eq_nonneg [simp]:
  1068   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
  1069 proof
  1070   assume A: "- a \<le> a" show "0 \<le> a"
  1071   proof (rule classical)
  1072     assume "\<not> 0 \<le> a"
  1073     then have "a < 0" by auto
  1074     with A have "- a < 0" by (rule le_less_trans)
  1075     then show ?thesis by auto
  1076   qed
  1077 next
  1078   assume A: "0 \<le> a" show "- a \<le> a"
  1079   proof (rule order_trans)
  1080     show "- a \<le> 0" using A by (simp add: minus_le_iff)
  1081   next
  1082     show "0 \<le> a" using A .
  1083   qed
  1084 qed
  1085 
  1086 lemma neg_less_pos [simp]:
  1087   "- a < a \<longleftrightarrow> 0 < a"
  1088   by (auto simp add: less_le)
  1089 
  1090 lemma less_eq_neg_nonpos [simp]:
  1091   "a \<le> - a \<longleftrightarrow> a \<le> 0"
  1092   using neg_less_eq_nonneg [of "- a"] by simp
  1093 
  1094 lemma less_neg_neg [simp]:
  1095   "a < - a \<longleftrightarrow> a < 0"
  1096   using neg_less_pos [of "- a"] by simp
  1097 
  1098 lemma double_zero [simp]:
  1099   "a + a = 0 \<longleftrightarrow> a = 0"
  1100 proof
  1101   assume assm: "a + a = 0"
  1102   then have a: "- a = a" by (rule minus_unique)
  1103   then show "a = 0" by (simp only: neg_equal_zero)
  1104 qed simp
  1105 
  1106 lemma double_zero_sym [simp]:
  1107   "0 = a + a \<longleftrightarrow> a = 0"
  1108   by (rule, drule sym) simp_all
  1109 
  1110 lemma zero_less_double_add_iff_zero_less_single_add [simp]:
  1111   "0 < a + a \<longleftrightarrow> 0 < a"
  1112 proof
  1113   assume "0 < a + a"
  1114   then have "0 - a < a" by (simp only: diff_less_eq)
  1115   then have "- a < a" by simp
  1116   then show "0 < a" by simp
  1117 next
  1118   assume "0 < a"
  1119   with this have "0 + 0 < a + a"
  1120     by (rule add_strict_mono)
  1121   then show "0 < a + a" by simp
  1122 qed
  1123 
  1124 lemma zero_le_double_add_iff_zero_le_single_add [simp]:
  1125   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
  1126   by (auto simp add: le_less)
  1127 
  1128 lemma double_add_less_zero_iff_single_add_less_zero [simp]:
  1129   "a + a < 0 \<longleftrightarrow> a < 0"
  1130 proof -
  1131   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
  1132     by (simp add: not_less)
  1133   then show ?thesis by simp
  1134 qed
  1135 
  1136 lemma double_add_le_zero_iff_single_add_le_zero [simp]:
  1137   "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
  1138 proof -
  1139   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
  1140     by (simp add: not_le)
  1141   then show ?thesis by simp
  1142 qed
  1143 
  1144 lemma minus_max_eq_min:
  1145   "- max x y = min (-x) (-y)"
  1146   by (auto simp add: max_def min_def)
  1147 
  1148 lemma minus_min_eq_max:
  1149   "- min x y = max (-x) (-y)"
  1150   by (auto simp add: max_def min_def)
  1151 
  1152 end
  1153 
  1154 class abs =
  1155   fixes abs :: "'a \<Rightarrow> 'a"  ("\<bar>_\<bar>")
  1156 
  1157 class sgn =
  1158   fixes sgn :: "'a \<Rightarrow> 'a"
  1159 
  1160 class abs_if = minus + uminus + ord + zero + abs +
  1161   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
  1162 
  1163 class sgn_if = minus + uminus + zero + one + ord + sgn +
  1164   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  1165 begin
  1166 
  1167 lemma sgn0 [simp]: "sgn 0 = 0"
  1168   by (simp add:sgn_if)
  1169 
  1170 end
  1171 
  1172 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
  1173   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
  1174     and abs_ge_self: "a \<le> \<bar>a\<bar>"
  1175     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
  1176     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
  1177     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1178 begin
  1179 
  1180 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
  1181   unfolding neg_le_0_iff_le by simp
  1182 
  1183 lemma abs_of_nonneg [simp]:
  1184   assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
  1185 proof (rule antisym)
  1186   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
  1187   from this nonneg have "- a \<le> a" by (rule order_trans)
  1188   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
  1189 qed (rule abs_ge_self)
  1190 
  1191 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
  1192 by (rule antisym)
  1193    (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
  1194 
  1195 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
  1196 proof -
  1197   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
  1198   proof (rule antisym)
  1199     assume zero: "\<bar>a\<bar> = 0"
  1200     with abs_ge_self show "a \<le> 0" by auto
  1201     from zero have "\<bar>-a\<bar> = 0" by simp
  1202     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
  1203     with neg_le_0_iff_le show "0 \<le> a" by auto
  1204   qed
  1205   then show ?thesis by auto
  1206 qed
  1207 
  1208 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
  1209 by simp
  1210 
  1211 lemma abs_0_eq [simp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
  1212 proof -
  1213   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
  1214   thus ?thesis by simp
  1215 qed
  1216 
  1217 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"
  1218 proof
  1219   assume "\<bar>a\<bar> \<le> 0"
  1220   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
  1221   thus "a = 0" by simp
  1222 next
  1223   assume "a = 0"
  1224   thus "\<bar>a\<bar> \<le> 0" by simp
  1225 qed
  1226 
  1227 lemma abs_le_self_iff [simp]: "\<bar>a\<bar> \<le> a \<longleftrightarrow> 0 \<le> a"
  1228 proof -
  1229   have "\<forall>a. (0::'a) \<le> \<bar>a\<bar>"
  1230     using abs_ge_zero by blast
  1231   then have "\<bar>a\<bar> \<le> a \<Longrightarrow> 0 \<le> a"
  1232     using order.trans by blast
  1233   then show ?thesis
  1234     using abs_of_nonneg eq_refl by blast
  1235 qed
  1236 
  1237 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
  1238 by (simp add: less_le)
  1239 
  1240 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
  1241 proof -
  1242   have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
  1243   show ?thesis by (simp add: a)
  1244 qed
  1245 
  1246 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
  1247 proof -
  1248   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
  1249   then show ?thesis by simp
  1250 qed
  1251 
  1252 lemma abs_minus_commute:
  1253   "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
  1254 proof -
  1255   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
  1256   also have "... = \<bar>b - a\<bar>" by simp
  1257   finally show ?thesis .
  1258 qed
  1259 
  1260 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
  1261 by (rule abs_of_nonneg, rule less_imp_le)
  1262 
  1263 lemma abs_of_nonpos [simp]:
  1264   assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
  1265 proof -
  1266   let ?b = "- a"
  1267   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
  1268   unfolding abs_minus_cancel [of "?b"]
  1269   unfolding neg_le_0_iff_le [of "?b"]
  1270   unfolding minus_minus by (erule abs_of_nonneg)
  1271   then show ?thesis using assms by auto
  1272 qed
  1273 
  1274 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
  1275 by (rule abs_of_nonpos, rule less_imp_le)
  1276 
  1277 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
  1278 by (insert abs_ge_self, blast intro: order_trans)
  1279 
  1280 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
  1281 by (insert abs_le_D1 [of "- a"], simp)
  1282 
  1283 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
  1284 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
  1285 
  1286 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
  1287 proof -
  1288   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
  1289     by (simp add: algebra_simps)
  1290   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
  1291     by (simp add: abs_triangle_ineq)
  1292   then show ?thesis
  1293     by (simp add: algebra_simps)
  1294 qed
  1295 
  1296 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
  1297   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
  1298 
  1299 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
  1300   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
  1301 
  1302 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1303 proof -
  1304   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (simp add: algebra_simps)
  1305   also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
  1306   finally show ?thesis by simp
  1307 qed
  1308 
  1309 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
  1310 proof -
  1311   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: algebra_simps)
  1312   also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
  1313   finally show ?thesis .
  1314 qed
  1315 
  1316 lemma abs_add_abs [simp]:
  1317   "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
  1318 proof (rule antisym)
  1319   show "?L \<ge> ?R" by(rule abs_ge_self)
  1320 next
  1321   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
  1322   also have "\<dots> = ?R" by simp
  1323   finally show "?L \<le> ?R" .
  1324 qed
  1325 
  1326 end
  1327 
  1328 lemma dense_eq0_I:
  1329   fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
  1330   shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) ==> x = 0"
  1331   apply (cases "\<bar>x\<bar> = 0", simp)
  1332   apply (simp only: zero_less_abs_iff [symmetric])
  1333   apply (drule dense)
  1334   apply (auto simp add: not_less [symmetric])
  1335   done
  1336 
  1337 hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus
  1338 
  1339 lemmas add_0 = add_0_left \<comment> \<open>FIXME duplicate\<close>
  1340 lemmas mult_1 = mult_1_left \<comment> \<open>FIXME duplicate\<close>
  1341 lemmas ab_left_minus = left_minus \<comment> \<open>FIXME duplicate\<close>
  1342 lemmas diff_diff_eq = diff_diff_add \<comment> \<open>FIXME duplicate\<close>
  1343 
  1344 subsection \<open>Canonically ordered monoids\<close>
  1345 
  1346 text \<open>Canonically ordered monoids are never groups.\<close>
  1347 
  1348 class canonically_ordered_monoid_add = comm_monoid_add + order +
  1349   assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
  1350 begin
  1351 
  1352 lemma zero_le[simp]: "0 \<le> x"
  1353   by (auto simp: le_iff_add)
  1354 
  1355 lemma le_zero_eq[simp]: "n \<le> 0 \<longleftrightarrow> n = 0"
  1356   by (auto intro: antisym)
  1357 
  1358 lemma not_less_zero[simp]: "\<not> n < 0"
  1359   by (auto simp: less_le)
  1360 
  1361 lemma zero_less_iff_neq_zero: "(0 < n) \<longleftrightarrow> (n \<noteq> 0)"
  1362   by (auto simp: less_le)
  1363 
  1364 text \<open>This theorem is useful with \<open>blast\<close>\<close>
  1365 lemma gr_zeroI: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n"
  1366   by (rule zero_less_iff_neq_zero[THEN iffD2]) iprover
  1367 
  1368 lemma not_gr_zero[simp]: "(\<not> (0 < n)) \<longleftrightarrow> (n = 0)"
  1369   by (simp add: zero_less_iff_neq_zero)
  1370 
  1371 subclass ordered_comm_monoid_add
  1372   proof qed (auto simp: le_iff_add add_ac)
  1373 
  1374 lemma add_eq_0_iff_both_eq_0: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
  1375   by (intro add_nonneg_eq_0_iff zero_le)
  1376 
  1377 lemma gr_implies_not_zero: "m < n \<Longrightarrow> n \<noteq> 0"
  1378   using add_eq_0_iff_both_eq_0[of m] by (auto simp: le_iff_add less_le)
  1379 
  1380 lemmas zero_order = zero_le le_zero_eq not_less_zero zero_less_iff_neq_zero not_gr_zero
  1381   \<comment> \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close>
  1382 
  1383 end
  1384 
  1385 class ordered_cancel_comm_monoid_diff =
  1386   canonically_ordered_monoid_add + comm_monoid_diff + ordered_ab_semigroup_add_imp_le
  1387 begin
  1388 
  1389 context
  1390   fixes a b
  1391   assumes "a \<le> b"
  1392 begin
  1393 
  1394 lemma add_diff_inverse:
  1395   "a + (b - a) = b"
  1396   using \<open>a \<le> b\<close> by (auto simp add: le_iff_add)
  1397 
  1398 lemma add_diff_assoc:
  1399   "c + (b - a) = c + b - a"
  1400   using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.left_commute [of c])
  1401 
  1402 lemma add_diff_assoc2:
  1403   "b - a + c = b + c - a"
  1404   using \<open>a \<le> b\<close> by (auto simp add: le_iff_add add.assoc)
  1405 
  1406 lemma diff_add_assoc:
  1407   "c + b - a = c + (b - a)"
  1408   using \<open>a \<le> b\<close> by (simp add: add.commute add_diff_assoc)
  1409 
  1410 lemma diff_add_assoc2:
  1411   "b + c - a = b - a + c"
  1412   using \<open>a \<le> b\<close>by (simp add: add.commute add_diff_assoc)
  1413 
  1414 lemma diff_diff_right:
  1415   "c - (b - a) = c + a - b"
  1416   by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add.commute)
  1417 
  1418 lemma diff_add:
  1419   "b - a + a = b"
  1420   by (simp add: add.commute add_diff_inverse)
  1421 
  1422 lemma le_add_diff:
  1423   "c \<le> b + c - a"
  1424   by (auto simp add: add.commute diff_add_assoc2 le_iff_add)
  1425 
  1426 lemma le_imp_diff_is_add:
  1427   "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
  1428   by (auto simp add: add.commute add_diff_inverse)
  1429 
  1430 lemma le_diff_conv2:
  1431   "c \<le> b - a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q")
  1432 proof
  1433   assume ?P
  1434   then have "c + a \<le> b - a + a" by (rule add_right_mono)
  1435   then show ?Q by (simp add: add_diff_inverse add.commute)
  1436 next
  1437   assume ?Q
  1438   then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add.commute)
  1439   then show ?P by simp
  1440 qed
  1441 
  1442 end
  1443 
  1444 end
  1445 
  1446 subsection \<open>Tools setup\<close>
  1447 
  1448 lemma add_mono_thms_linordered_semiring:
  1449   fixes i j k :: "'a::ordered_ab_semigroup_add"
  1450   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1451     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1452     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
  1453     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
  1454 by (rule add_mono, clarify+)+
  1455 
  1456 lemma add_mono_thms_linordered_field:
  1457   fixes i j k :: "'a::ordered_cancel_ab_semigroup_add"
  1458   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
  1459     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
  1460     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
  1461     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
  1462     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
  1463 by (auto intro: add_strict_right_mono add_strict_left_mono
  1464   add_less_le_mono add_le_less_mono add_strict_mono)
  1465 
  1466 code_identifier
  1467   code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1468 
  1469 end