src/HOL/Groups.thy
author hoelzl
Tue May 13 11:35:51 2014 +0200 (2014-05-13)
changeset 56950 c49edf06f8e4
parent 54868 bab6cade3cc5
child 57512 cc97b347b301
permissions -rw-r--r--
add mono rules for diff
     1 (*  Title:   HOL/Groups.thy
     2     Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, Markus Wenzel, Jeremy Avigad
     3 *)
     4 
     5 header {* Groups, also combined with orderings *}
     6 
     7 theory Groups
     8 imports Orderings
     9 begin
    10 
    11 subsection {* Fact collections *}
    12 
    13 ML {*
    14 structure Ac_Simps = Named_Thms
    15 (
    16   val name = @{binding ac_simps}
    17   val description = "associativity and commutativity simplification rules"
    18 )
    19 *}
    20 
    21 setup Ac_Simps.setup
    22 
    23 text{* The rewrites accumulated in @{text algebra_simps} deal with the
    24 classical algebraic structures of groups, rings and family. They simplify
    25 terms by multiplying everything out (in case of a ring) and bringing sums and
    26 products into a canonical form (by ordered rewriting). As a result it decides
    27 group and ring equalities but also helps with inequalities.
    28 
    29 Of course it also works for fields, but it knows nothing about multiplicative
    30 inverses or division. This is catered for by @{text field_simps}. *}
    31 
    32 ML {*
    33 structure Algebra_Simps = Named_Thms
    34 (
    35   val name = @{binding algebra_simps}
    36   val description = "algebra simplification rules"
    37 )
    38 *}
    39 
    40 setup Algebra_Simps.setup
    41 
    42 text{* Lemmas @{text field_simps} multiply with denominators in (in)equations
    43 if they can be proved to be non-zero (for equations) or positive/negative
    44 (for inequations). Can be too aggressive and is therefore separate from the
    45 more benign @{text algebra_simps}. *}
    46 
    47 ML {*
    48 structure Field_Simps = Named_Thms
    49 (
    50   val name = @{binding field_simps}
    51   val description = "algebra simplification rules for fields"
    52 )
    53 *}
    54 
    55 setup Field_Simps.setup
    56 
    57 
    58 subsection {* Abstract structures *}
    59 
    60 text {*
    61   These locales provide basic structures for interpretation into
    62   bigger structures;  extensions require careful thinking, otherwise
    63   undesired effects may occur due to interpretation.
    64 *}
    65 
    66 locale semigroup =
    67   fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
    68   assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
    69 
    70 locale abel_semigroup = semigroup +
    71   assumes commute [ac_simps]: "a * b = b * a"
    72 begin
    73 
    74 lemma left_commute [ac_simps]:
    75   "b * (a * c) = a * (b * c)"
    76 proof -
    77   have "(b * a) * c = (a * b) * c"
    78     by (simp only: commute)
    79   then show ?thesis
    80     by (simp only: assoc)
    81 qed
    82 
    83 end
    84 
    85 locale monoid = semigroup +
    86   fixes z :: 'a ("1")
    87   assumes left_neutral [simp]: "1 * a = a"
    88   assumes right_neutral [simp]: "a * 1 = a"
    89 
    90 locale comm_monoid = abel_semigroup +
    91   fixes z :: 'a ("1")
    92   assumes comm_neutral: "a * 1 = a"
    93 begin
    94 
    95 sublocale monoid
    96   by default (simp_all add: commute comm_neutral)
    97 
    98 end
    99 
   100 
   101 subsection {* Generic operations *}
   102 
   103 class zero = 
   104   fixes zero :: 'a  ("0")
   105 
   106 class one =
   107   fixes one  :: 'a  ("1")
   108 
   109 hide_const (open) zero one
   110 
   111 lemma Let_0 [simp]: "Let 0 f = f 0"
   112   unfolding Let_def ..
   113 
   114 lemma Let_1 [simp]: "Let 1 f = f 1"
   115   unfolding Let_def ..
   116 
   117 setup {*
   118   Reorient_Proc.add
   119     (fn Const(@{const_name Groups.zero}, _) => true
   120       | Const(@{const_name Groups.one}, _) => true
   121       | _ => false)
   122 *}
   123 
   124 simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
   125 simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
   126 
   127 typed_print_translation {*
   128   let
   129     fun tr' c = (c, fn ctxt => fn T => fn ts =>
   130       if null ts andalso Printer.type_emphasis ctxt T then
   131         Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $
   132           Syntax_Phases.term_of_typ ctxt T
   133       else raise Match);
   134   in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
   135 *} -- {* show types that are presumably too general *}
   136 
   137 class plus =
   138   fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
   139 
   140 class minus =
   141   fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
   142 
   143 class uminus =
   144   fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
   145 
   146 class times =
   147   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
   148 
   149 
   150 subsection {* Semigroups and Monoids *}
   151 
   152 class semigroup_add = plus +
   153   assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"
   154 begin
   155 
   156 sublocale add!: semigroup plus
   157   by default (fact add_assoc)
   158 
   159 end
   160 
   161 class ab_semigroup_add = semigroup_add +
   162   assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
   163 begin
   164 
   165 sublocale add!: abel_semigroup plus
   166   by default (fact add_commute)
   167 
   168 lemmas add_left_commute [algebra_simps, field_simps] = add.left_commute
   169 
   170 theorems add_ac = add_assoc add_commute add_left_commute
   171 
   172 end
   173 
   174 theorems add_ac = add_assoc add_commute add_left_commute
   175 
   176 class semigroup_mult = times +
   177   assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
   178 begin
   179 
   180 sublocale mult!: semigroup times
   181   by default (fact mult_assoc)
   182 
   183 end
   184 
   185 class ab_semigroup_mult = semigroup_mult +
   186   assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
   187 begin
   188 
   189 sublocale mult!: abel_semigroup times
   190   by default (fact mult_commute)
   191 
   192 lemmas mult_left_commute [algebra_simps, field_simps] = mult.left_commute
   193 
   194 theorems mult_ac = mult_assoc mult_commute mult_left_commute
   195 
   196 end
   197 
   198 theorems mult_ac = mult_assoc mult_commute mult_left_commute
   199 
   200 class monoid_add = zero + semigroup_add +
   201   assumes add_0_left: "0 + a = a"
   202     and add_0_right: "a + 0 = a"
   203 begin
   204 
   205 sublocale add!: monoid plus 0
   206   by default (fact add_0_left add_0_right)+
   207 
   208 end
   209 
   210 lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
   211   by (fact eq_commute)
   212 
   213 class comm_monoid_add = zero + ab_semigroup_add +
   214   assumes add_0: "0 + a = a"
   215 begin
   216 
   217 sublocale add!: comm_monoid plus 0
   218   by default (insert add_0, simp add: ac_simps)
   219 
   220 subclass monoid_add
   221   by default (fact add.left_neutral add.right_neutral)+
   222 
   223 end
   224 
   225 class comm_monoid_diff = comm_monoid_add + minus +
   226   assumes diff_zero [simp]: "a - 0 = a"
   227     and zero_diff [simp]: "0 - a = 0"
   228     and add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b"
   229     and diff_diff_add: "a - b - c = a - (b + c)"
   230 begin
   231 
   232 lemma add_diff_cancel_right [simp]:
   233   "(a + c) - (b + c) = a - b"
   234   using add_diff_cancel_left [symmetric] by (simp add: add.commute)
   235 
   236 lemma add_diff_cancel_left' [simp]:
   237   "(b + a) - b = a"
   238 proof -
   239   have "(b + a) - (b + 0) = a" by (simp only: add_diff_cancel_left diff_zero)
   240   then show ?thesis by simp
   241 qed
   242 
   243 lemma add_diff_cancel_right' [simp]:
   244   "(a + b) - b = a"
   245   using add_diff_cancel_left' [symmetric] by (simp add: add.commute)
   246 
   247 lemma diff_add_zero [simp]:
   248   "a - (a + b) = 0"
   249 proof -
   250   have "a - (a + b) = (a + 0) - (a + b)" by simp
   251   also have "\<dots> = 0" by (simp only: add_diff_cancel_left zero_diff)
   252   finally show ?thesis .
   253 qed
   254 
   255 lemma diff_cancel [simp]:
   256   "a - a = 0"
   257 proof -
   258   have "(a + 0) - (a + 0) = 0" by (simp only: add_diff_cancel_left diff_zero)
   259   then show ?thesis by simp
   260 qed
   261 
   262 lemma diff_right_commute:
   263   "a - c - b = a - b - c"
   264   by (simp add: diff_diff_add add.commute)
   265 
   266 lemma add_implies_diff:
   267   assumes "c + b = a"
   268   shows "c = a - b"
   269 proof -
   270   from assms have "(b + c) - (b + 0) = a - b" by (simp add: add.commute)
   271   then show "c = a - b" by simp
   272 qed
   273 
   274 end
   275 
   276 class monoid_mult = one + semigroup_mult +
   277   assumes mult_1_left: "1 * a  = a"
   278     and mult_1_right: "a * 1 = a"
   279 begin
   280 
   281 sublocale mult!: monoid times 1
   282   by default (fact mult_1_left mult_1_right)+
   283 
   284 end
   285 
   286 lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
   287   by (fact eq_commute)
   288 
   289 class comm_monoid_mult = one + ab_semigroup_mult +
   290   assumes mult_1: "1 * a = a"
   291 begin
   292 
   293 sublocale mult!: comm_monoid times 1
   294   by default (insert mult_1, simp add: ac_simps)
   295 
   296 subclass monoid_mult
   297   by default (fact mult.left_neutral mult.right_neutral)+
   298 
   299 end
   300 
   301 class cancel_semigroup_add = semigroup_add +
   302   assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
   303   assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
   304 begin
   305 
   306 lemma add_left_cancel [simp]:
   307   "a + b = a + c \<longleftrightarrow> b = c"
   308 by (blast dest: add_left_imp_eq)
   309 
   310 lemma add_right_cancel [simp]:
   311   "b + a = c + a \<longleftrightarrow> b = c"
   312 by (blast dest: add_right_imp_eq)
   313 
   314 end
   315 
   316 class cancel_ab_semigroup_add = ab_semigroup_add +
   317   assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
   318 begin
   319 
   320 subclass cancel_semigroup_add
   321 proof
   322   fix a b c :: 'a
   323   assume "a + b = a + c" 
   324   then show "b = c" by (rule add_imp_eq)
   325 next
   326   fix a b c :: 'a
   327   assume "b + a = c + a"
   328   then have "a + b = a + c" by (simp only: add_commute)
   329   then show "b = c" by (rule add_imp_eq)
   330 qed
   331 
   332 end
   333 
   334 class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add
   335 
   336 
   337 subsection {* Groups *}
   338 
   339 class group_add = minus + uminus + monoid_add +
   340   assumes left_minus [simp]: "- a + a = 0"
   341   assumes add_uminus_conv_diff [simp]: "a + (- b) = a - b"
   342 begin
   343 
   344 lemma diff_conv_add_uminus:
   345   "a - b = a + (- b)"
   346   by simp
   347 
   348 lemma minus_unique:
   349   assumes "a + b = 0" shows "- a = b"
   350 proof -
   351   have "- a = - a + (a + b)" using assms by simp
   352   also have "\<dots> = b" by (simp add: add_assoc [symmetric])
   353   finally show ?thesis .
   354 qed
   355 
   356 lemma minus_zero [simp]: "- 0 = 0"
   357 proof -
   358   have "0 + 0 = 0" by (rule add_0_right)
   359   thus "- 0 = 0" by (rule minus_unique)
   360 qed
   361 
   362 lemma minus_minus [simp]: "- (- a) = a"
   363 proof -
   364   have "- a + a = 0" by (rule left_minus)
   365   thus "- (- a) = a" by (rule minus_unique)
   366 qed
   367 
   368 lemma right_minus: "a + - a = 0"
   369 proof -
   370   have "a + - a = - (- a) + - a" by simp
   371   also have "\<dots> = 0" by (rule left_minus)
   372   finally show ?thesis .
   373 qed
   374 
   375 lemma diff_self [simp]:
   376   "a - a = 0"
   377   using right_minus [of a] by simp
   378 
   379 subclass cancel_semigroup_add
   380 proof
   381   fix a b c :: 'a
   382   assume "a + b = a + c"
   383   then have "- a + a + b = - a + a + c"
   384     unfolding add_assoc by simp
   385   then show "b = c" by simp
   386 next
   387   fix a b c :: 'a
   388   assume "b + a = c + a"
   389   then have "b + a + - a = c + a  + - a" by simp
   390   then show "b = c" unfolding add_assoc by simp
   391 qed
   392 
   393 lemma minus_add_cancel [simp]:
   394   "- a + (a + b) = b"
   395   by (simp add: add_assoc [symmetric])
   396 
   397 lemma add_minus_cancel [simp]:
   398   "a + (- a + b) = b"
   399   by (simp add: add_assoc [symmetric])
   400 
   401 lemma diff_add_cancel [simp]:
   402   "a - b + b = a"
   403   by (simp only: diff_conv_add_uminus add_assoc) simp
   404 
   405 lemma add_diff_cancel [simp]:
   406   "a + b - b = a"
   407   by (simp only: diff_conv_add_uminus add_assoc) simp
   408 
   409 lemma minus_add:
   410   "- (a + b) = - b + - a"
   411 proof -
   412   have "(a + b) + (- b + - a) = 0"
   413     by (simp only: add_assoc add_minus_cancel) simp
   414   then show "- (a + b) = - b + - a"
   415     by (rule minus_unique)
   416 qed
   417 
   418 lemma right_minus_eq [simp]:
   419   "a - b = 0 \<longleftrightarrow> a = b"
   420 proof
   421   assume "a - b = 0"
   422   have "a = (a - b) + b" by (simp add: add_assoc)
   423   also have "\<dots> = b" using `a - b = 0` by simp
   424   finally show "a = b" .
   425 next
   426   assume "a = b" thus "a - b = 0" by simp
   427 qed
   428 
   429 lemma eq_iff_diff_eq_0:
   430   "a = b \<longleftrightarrow> a - b = 0"
   431   by (fact right_minus_eq [symmetric])
   432 
   433 lemma diff_0 [simp]:
   434   "0 - a = - a"
   435   by (simp only: diff_conv_add_uminus add_0_left)
   436 
   437 lemma diff_0_right [simp]:
   438   "a - 0 = a" 
   439   by (simp only: diff_conv_add_uminus minus_zero add_0_right)
   440 
   441 lemma diff_minus_eq_add [simp]:
   442   "a - - b = a + b"
   443   by (simp only: diff_conv_add_uminus minus_minus)
   444 
   445 lemma neg_equal_iff_equal [simp]:
   446   "- a = - b \<longleftrightarrow> a = b" 
   447 proof 
   448   assume "- a = - b"
   449   hence "- (- a) = - (- b)" by simp
   450   thus "a = b" by simp
   451 next
   452   assume "a = b"
   453   thus "- a = - b" by simp
   454 qed
   455 
   456 lemma neg_equal_0_iff_equal [simp]:
   457   "- a = 0 \<longleftrightarrow> a = 0"
   458   by (subst neg_equal_iff_equal [symmetric]) simp
   459 
   460 lemma neg_0_equal_iff_equal [simp]:
   461   "0 = - a \<longleftrightarrow> 0 = a"
   462   by (subst neg_equal_iff_equal [symmetric]) simp
   463 
   464 text{*The next two equations can make the simplifier loop!*}
   465 
   466 lemma equation_minus_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 minus_equation_iff:
   474   "- a = b \<longleftrightarrow> - b = a"
   475 proof -
   476   have "- a = - (- b) \<longleftrightarrow> a = -b" by (rule neg_equal_iff_equal)
   477   thus ?thesis by (simp add: eq_commute)
   478 qed
   479 
   480 lemma eq_neg_iff_add_eq_0:
   481   "a = - b \<longleftrightarrow> a + b = 0"
   482 proof
   483   assume "a = - b" then show "a + b = 0" by simp
   484 next
   485   assume "a + b = 0"
   486   moreover have "a + (b + - b) = (a + b) + - b"
   487     by (simp only: add_assoc)
   488   ultimately show "a = - b" by simp
   489 qed
   490 
   491 lemma add_eq_0_iff2:
   492   "a + b = 0 \<longleftrightarrow> a = - b"
   493   by (fact eq_neg_iff_add_eq_0 [symmetric])
   494 
   495 lemma neg_eq_iff_add_eq_0:
   496   "- a = b \<longleftrightarrow> a + b = 0"
   497   by (auto simp add: add_eq_0_iff2)
   498 
   499 lemma add_eq_0_iff:
   500   "a + b = 0 \<longleftrightarrow> b = - a"
   501   by (auto simp add: neg_eq_iff_add_eq_0 [symmetric])
   502 
   503 lemma minus_diff_eq [simp]:
   504   "- (a - b) = b - a"
   505   by (simp only: neg_eq_iff_add_eq_0 diff_conv_add_uminus add_assoc minus_add_cancel) simp
   506 
   507 lemma add_diff_eq [algebra_simps, field_simps]:
   508   "a + (b - c) = (a + b) - c"
   509   by (simp only: diff_conv_add_uminus add_assoc)
   510 
   511 lemma diff_add_eq_diff_diff_swap:
   512   "a - (b + c) = a - c - b"
   513   by (simp only: diff_conv_add_uminus add_assoc minus_add)
   514 
   515 lemma diff_eq_eq [algebra_simps, field_simps]:
   516   "a - b = c \<longleftrightarrow> a = c + b"
   517   by auto
   518 
   519 lemma eq_diff_eq [algebra_simps, field_simps]:
   520   "a = c - b \<longleftrightarrow> a + b = c"
   521   by auto
   522 
   523 lemma diff_diff_eq2 [algebra_simps, field_simps]:
   524   "a - (b - c) = (a + c) - b"
   525   by (simp only: diff_conv_add_uminus add_assoc) simp
   526 
   527 lemma diff_eq_diff_eq:
   528   "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
   529   by (simp only: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])
   530 
   531 end
   532 
   533 class ab_group_add = minus + uminus + comm_monoid_add +
   534   assumes ab_left_minus: "- a + a = 0"
   535   assumes ab_add_uminus_conv_diff: "a - b = a + (- b)"
   536 begin
   537 
   538 subclass group_add
   539   proof qed (simp_all add: ab_left_minus ab_add_uminus_conv_diff)
   540 
   541 subclass cancel_comm_monoid_add
   542 proof
   543   fix a b c :: 'a
   544   assume "a + b = a + c"
   545   then have "- a + a + b = - a + a + c"
   546     by (simp only: add_assoc)
   547   then show "b = c" by simp
   548 qed
   549 
   550 lemma uminus_add_conv_diff [simp]:
   551   "- a + b = b - a"
   552   by (simp add: add_commute)
   553 
   554 lemma minus_add_distrib [simp]:
   555   "- (a + b) = - a + - b"
   556   by (simp add: algebra_simps)
   557 
   558 lemma diff_add_eq [algebra_simps, field_simps]:
   559   "(a - b) + c = (a + c) - b"
   560   by (simp add: algebra_simps)
   561 
   562 lemma diff_diff_eq [algebra_simps, field_simps]:
   563   "(a - b) - c = a - (b + c)"
   564   by (simp add: algebra_simps)
   565 
   566 lemma diff_add_eq_diff_diff:
   567   "a - (b + c) = a - b - c"
   568   using diff_add_eq_diff_diff_swap [of a c b] by (simp add: add.commute)
   569 
   570 lemma add_diff_cancel_left [simp]:
   571   "(c + a) - (c + b) = a - b"
   572   by (simp add: algebra_simps)
   573 
   574 end
   575 
   576 
   577 subsection {* (Partially) Ordered Groups *} 
   578 
   579 text {*
   580   The theory of partially ordered groups is taken from the books:
   581   \begin{itemize}
   582   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
   583   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
   584   \end{itemize}
   585   Most of the used notions can also be looked up in 
   586   \begin{itemize}
   587   \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
   588   \item \emph{Algebra I} by van der Waerden, Springer.
   589   \end{itemize}
   590 *}
   591 
   592 class ordered_ab_semigroup_add = order + ab_semigroup_add +
   593   assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
   594 begin
   595 
   596 lemma add_right_mono:
   597   "a \<le> b \<Longrightarrow> a + c \<le> b + c"
   598 by (simp add: add_commute [of _ c] add_left_mono)
   599 
   600 text {* non-strict, in both arguments *}
   601 lemma add_mono:
   602   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
   603   apply (erule add_right_mono [THEN order_trans])
   604   apply (simp add: add_commute add_left_mono)
   605   done
   606 
   607 end
   608 
   609 class ordered_cancel_ab_semigroup_add =
   610   ordered_ab_semigroup_add + cancel_ab_semigroup_add
   611 begin
   612 
   613 lemma add_strict_left_mono:
   614   "a < b \<Longrightarrow> c + a < c + b"
   615 by (auto simp add: less_le add_left_mono)
   616 
   617 lemma add_strict_right_mono:
   618   "a < b \<Longrightarrow> a + c < b + c"
   619 by (simp add: add_commute [of _ c] add_strict_left_mono)
   620 
   621 text{*Strict monotonicity in both arguments*}
   622 lemma add_strict_mono:
   623   "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   624 apply (erule add_strict_right_mono [THEN less_trans])
   625 apply (erule add_strict_left_mono)
   626 done
   627 
   628 lemma add_less_le_mono:
   629   "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
   630 apply (erule add_strict_right_mono [THEN less_le_trans])
   631 apply (erule add_left_mono)
   632 done
   633 
   634 lemma add_le_less_mono:
   635   "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   636 apply (erule add_right_mono [THEN le_less_trans])
   637 apply (erule add_strict_left_mono) 
   638 done
   639 
   640 end
   641 
   642 class ordered_ab_semigroup_add_imp_le =
   643   ordered_cancel_ab_semigroup_add +
   644   assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
   645 begin
   646 
   647 lemma add_less_imp_less_left:
   648   assumes less: "c + a < c + b" shows "a < b"
   649 proof -
   650   from less have le: "c + a <= c + b" by (simp add: order_le_less)
   651   have "a <= b" 
   652     apply (insert le)
   653     apply (drule add_le_imp_le_left)
   654     by (insert le, drule add_le_imp_le_left, assumption)
   655   moreover have "a \<noteq> b"
   656   proof (rule ccontr)
   657     assume "~(a \<noteq> b)"
   658     then have "a = b" by simp
   659     then have "c + a = c + b" by simp
   660     with less show "False"by simp
   661   qed
   662   ultimately show "a < b" by (simp add: order_le_less)
   663 qed
   664 
   665 lemma add_less_imp_less_right:
   666   "a + c < b + c \<Longrightarrow> a < b"
   667 apply (rule add_less_imp_less_left [of c])
   668 apply (simp add: add_commute)  
   669 done
   670 
   671 lemma add_less_cancel_left [simp]:
   672   "c + a < c + b \<longleftrightarrow> a < b"
   673   by (blast intro: add_less_imp_less_left add_strict_left_mono) 
   674 
   675 lemma add_less_cancel_right [simp]:
   676   "a + c < b + c \<longleftrightarrow> a < b"
   677   by (blast intro: add_less_imp_less_right add_strict_right_mono)
   678 
   679 lemma add_le_cancel_left [simp]:
   680   "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
   681   by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
   682 
   683 lemma add_le_cancel_right [simp]:
   684   "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
   685   by (simp add: add_commute [of a c] add_commute [of b c])
   686 
   687 lemma add_le_imp_le_right:
   688   "a + c \<le> b + c \<Longrightarrow> a \<le> b"
   689 by simp
   690 
   691 lemma max_add_distrib_left:
   692   "max x y + z = max (x + z) (y + z)"
   693   unfolding max_def by auto
   694 
   695 lemma min_add_distrib_left:
   696   "min x y + z = min (x + z) (y + z)"
   697   unfolding min_def by auto
   698 
   699 lemma max_add_distrib_right:
   700   "x + max y z = max (x + y) (x + z)"
   701   unfolding max_def by auto
   702 
   703 lemma min_add_distrib_right:
   704   "x + min y z = min (x + y) (x + z)"
   705   unfolding min_def by auto
   706 
   707 end
   708 
   709 class ordered_cancel_comm_monoid_diff = comm_monoid_diff + ordered_ab_semigroup_add_imp_le +
   710   assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
   711 begin
   712 
   713 context
   714   fixes a b
   715   assumes "a \<le> b"
   716 begin
   717 
   718 lemma add_diff_inverse:
   719   "a + (b - a) = b"
   720   using `a \<le> b` by (auto simp add: le_iff_add)
   721 
   722 lemma add_diff_assoc:
   723   "c + (b - a) = c + b - a"
   724   using `a \<le> b` by (auto simp add: le_iff_add add_left_commute [of c])
   725 
   726 lemma add_diff_assoc2:
   727   "b - a + c = b + c - a"
   728   using `a \<le> b` by (auto simp add: le_iff_add add_assoc)
   729 
   730 lemma diff_add_assoc:
   731   "c + b - a = c + (b - a)"
   732   using `a \<le> b` by (simp add: add_commute add_diff_assoc)
   733 
   734 lemma diff_add_assoc2:
   735   "b + c - a = b - a + c"
   736   using `a \<le> b`by (simp add: add_commute add_diff_assoc)
   737 
   738 lemma diff_diff_right:
   739   "c - (b - a) = c + a - b"
   740   by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add_commute)
   741 
   742 lemma diff_add:
   743   "b - a + a = b"
   744   by (simp add: add_commute add_diff_inverse)
   745 
   746 lemma le_add_diff:
   747   "c \<le> b + c - a"
   748   by (auto simp add: add_commute diff_add_assoc2 le_iff_add)
   749 
   750 lemma le_imp_diff_is_add:
   751   "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
   752   by (auto simp add: add_commute add_diff_inverse)
   753 
   754 lemma le_diff_conv2:
   755   "c \<le> b - a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q")
   756 proof
   757   assume ?P
   758   then have "c + a \<le> b - a + a" by (rule add_right_mono)
   759   then show ?Q by (simp add: add_diff_inverse add_commute)
   760 next
   761   assume ?Q
   762   then have "a + c \<le> a + (b - a)" by (simp add: add_diff_inverse add_commute)
   763   then show ?P by simp
   764 qed
   765 
   766 end
   767 
   768 end
   769 
   770 
   771 subsection {* Support for reasoning about signs *}
   772 
   773 class ordered_comm_monoid_add =
   774   ordered_cancel_ab_semigroup_add + comm_monoid_add
   775 begin
   776 
   777 lemma add_pos_nonneg:
   778   assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
   779 proof -
   780   have "0 + 0 < a + b" 
   781     using assms by (rule add_less_le_mono)
   782   then show ?thesis by simp
   783 qed
   784 
   785 lemma add_pos_pos:
   786   assumes "0 < a" and "0 < b" shows "0 < a + b"
   787 by (rule add_pos_nonneg) (insert assms, auto)
   788 
   789 lemma add_nonneg_pos:
   790   assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
   791 proof -
   792   have "0 + 0 < a + b" 
   793     using assms by (rule add_le_less_mono)
   794   then show ?thesis by simp
   795 qed
   796 
   797 lemma add_nonneg_nonneg [simp]:
   798   assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
   799 proof -
   800   have "0 + 0 \<le> a + b" 
   801     using assms by (rule add_mono)
   802   then show ?thesis by simp
   803 qed
   804 
   805 lemma add_neg_nonpos:
   806   assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
   807 proof -
   808   have "a + b < 0 + 0"
   809     using assms by (rule add_less_le_mono)
   810   then show ?thesis by simp
   811 qed
   812 
   813 lemma add_neg_neg: 
   814   assumes "a < 0" and "b < 0" shows "a + b < 0"
   815 by (rule add_neg_nonpos) (insert assms, auto)
   816 
   817 lemma add_nonpos_neg:
   818   assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
   819 proof -
   820   have "a + b < 0 + 0"
   821     using assms by (rule add_le_less_mono)
   822   then show ?thesis by simp
   823 qed
   824 
   825 lemma add_nonpos_nonpos:
   826   assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
   827 proof -
   828   have "a + b \<le> 0 + 0"
   829     using assms by (rule add_mono)
   830   then show ?thesis by simp
   831 qed
   832 
   833 lemmas add_sign_intros =
   834   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
   835   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
   836 
   837 lemma add_nonneg_eq_0_iff:
   838   assumes x: "0 \<le> x" and y: "0 \<le> y"
   839   shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   840 proof (intro iffI conjI)
   841   have "x = x + 0" by simp
   842   also have "x + 0 \<le> x + y" using y by (rule add_left_mono)
   843   also assume "x + y = 0"
   844   also have "0 \<le> x" using x .
   845   finally show "x = 0" .
   846 next
   847   have "y = 0 + y" by simp
   848   also have "0 + y \<le> x + y" using x by (rule add_right_mono)
   849   also assume "x + y = 0"
   850   also have "0 \<le> y" using y .
   851   finally show "y = 0" .
   852 next
   853   assume "x = 0 \<and> y = 0"
   854   then show "x + y = 0" by simp
   855 qed
   856 
   857 lemma add_increasing:
   858   "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
   859   by (insert add_mono [of 0 a b c], simp)
   860 
   861 lemma add_increasing2:
   862   "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
   863   by (simp add: add_increasing add_commute [of a])
   864 
   865 lemma add_strict_increasing:
   866   "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
   867   by (insert add_less_le_mono [of 0 a b c], simp)
   868 
   869 lemma add_strict_increasing2:
   870   "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   871   by (insert add_le_less_mono [of 0 a b c], simp)
   872 
   873 end
   874 
   875 class ordered_ab_group_add =
   876   ab_group_add + ordered_ab_semigroup_add
   877 begin
   878 
   879 subclass ordered_cancel_ab_semigroup_add ..
   880 
   881 subclass ordered_ab_semigroup_add_imp_le
   882 proof
   883   fix a b c :: 'a
   884   assume "c + a \<le> c + b"
   885   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
   886   hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
   887   thus "a \<le> b" by simp
   888 qed
   889 
   890 subclass ordered_comm_monoid_add ..
   891 
   892 lemma add_less_same_cancel1 [simp]:
   893   "b + a < b \<longleftrightarrow> a < 0"
   894   using add_less_cancel_left [of _ _ 0] by simp
   895 
   896 lemma add_less_same_cancel2 [simp]:
   897   "a + b < b \<longleftrightarrow> a < 0"
   898   using add_less_cancel_right [of _ _ 0] by simp
   899 
   900 lemma less_add_same_cancel1 [simp]:
   901   "a < a + b \<longleftrightarrow> 0 < b"
   902   using add_less_cancel_left [of _ 0] by simp
   903 
   904 lemma less_add_same_cancel2 [simp]:
   905   "a < b + a \<longleftrightarrow> 0 < b"
   906   using add_less_cancel_right [of 0] by simp
   907 
   908 lemma add_le_same_cancel1 [simp]:
   909   "b + a \<le> b \<longleftrightarrow> a \<le> 0"
   910   using add_le_cancel_left [of _ _ 0] by simp
   911 
   912 lemma add_le_same_cancel2 [simp]:
   913   "a + b \<le> b \<longleftrightarrow> a \<le> 0"
   914   using add_le_cancel_right [of _ _ 0] by simp
   915 
   916 lemma le_add_same_cancel1 [simp]:
   917   "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
   918   using add_le_cancel_left [of _ 0] by simp
   919 
   920 lemma le_add_same_cancel2 [simp]:
   921   "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
   922   using add_le_cancel_right [of 0] by simp
   923 
   924 lemma max_diff_distrib_left:
   925   shows "max x y - z = max (x - z) (y - z)"
   926   using max_add_distrib_left [of x y "- z"] by simp
   927 
   928 lemma min_diff_distrib_left:
   929   shows "min x y - z = min (x - z) (y - z)"
   930   using min_add_distrib_left [of x y "- z"] by simp
   931 
   932 lemma le_imp_neg_le:
   933   assumes "a \<le> b" shows "-b \<le> -a"
   934 proof -
   935   have "-a+a \<le> -a+b" using `a \<le> b` by (rule add_left_mono) 
   936   then have "0 \<le> -a+b" by simp
   937   then have "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono) 
   938   then show ?thesis by (simp add: algebra_simps)
   939 qed
   940 
   941 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
   942 proof 
   943   assume "- b \<le> - a"
   944   hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
   945   thus "a\<le>b" by simp
   946 next
   947   assume "a\<le>b"
   948   thus "-b \<le> -a" by (rule le_imp_neg_le)
   949 qed
   950 
   951 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   952 by (subst neg_le_iff_le [symmetric], simp)
   953 
   954 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
   955 by (subst neg_le_iff_le [symmetric], simp)
   956 
   957 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
   958 by (force simp add: less_le) 
   959 
   960 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
   961 by (subst neg_less_iff_less [symmetric], simp)
   962 
   963 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
   964 by (subst neg_less_iff_less [symmetric], simp)
   965 
   966 text{*The next several equations can make the simplifier loop!*}
   967 
   968 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
   969 proof -
   970   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
   971   thus ?thesis by simp
   972 qed
   973 
   974 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
   975 proof -
   976   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
   977   thus ?thesis by simp
   978 qed
   979 
   980 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
   981 proof -
   982   have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
   983   have "(- (- a) <= -b) = (b <= - a)" 
   984     apply (auto simp only: le_less)
   985     apply (drule mm)
   986     apply (simp_all)
   987     apply (drule mm[simplified], assumption)
   988     done
   989   then show ?thesis by simp
   990 qed
   991 
   992 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
   993 by (auto simp add: le_less minus_less_iff)
   994 
   995 lemma diff_less_0_iff_less [simp]:
   996   "a - b < 0 \<longleftrightarrow> a < b"
   997 proof -
   998   have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by simp
   999   also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right)
  1000   finally show ?thesis .
  1001 qed
  1002 
  1003 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
  1004 
  1005 lemma diff_less_eq [algebra_simps, field_simps]:
  1006   "a - b < c \<longleftrightarrow> a < c + b"
  1007 apply (subst less_iff_diff_less_0 [of a])
  1008 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
  1009 apply (simp add: algebra_simps)
  1010 done
  1011 
  1012 lemma less_diff_eq[algebra_simps, field_simps]:
  1013   "a < c - b \<longleftrightarrow> a + b < c"
  1014 apply (subst less_iff_diff_less_0 [of "a + b"])
  1015 apply (subst less_iff_diff_less_0 [of a])
  1016 apply (simp add: algebra_simps)
  1017 done
  1018 
  1019 lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
  1020 by (auto simp add: le_less diff_less_eq )
  1021 
  1022 lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
  1023 by (auto simp add: le_less less_diff_eq)
  1024 
  1025 lemma diff_le_0_iff_le [simp]:
  1026   "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
  1027   by (simp add: algebra_simps)
  1028 
  1029 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
  1030 
  1031 lemma diff_eq_diff_less:
  1032   "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
  1033   by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
  1034 
  1035 lemma diff_eq_diff_less_eq:
  1036   "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
  1037   by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
  1038 
  1039 lemma diff_mono: "a \<le> b \<Longrightarrow> d \<le> c \<Longrightarrow> a - c \<le> b - d"
  1040   by (simp add: field_simps add_mono)
  1041 
  1042 lemma diff_left_mono: "b \<le> a \<Longrightarrow> c - a \<le> c - b"
  1043   by (simp add: field_simps)
  1044 
  1045 lemma diff_right_mono: "a \<le> b \<Longrightarrow> a - c \<le> b - c"
  1046   by (simp add: field_simps)
  1047 
  1048 lemma diff_strict_mono: "a < b \<Longrightarrow> d < c \<Longrightarrow> a - c < b - d"
  1049   by (simp add: field_simps add_strict_mono)
  1050 
  1051 lemma diff_strict_left_mono: "b < a \<Longrightarrow> c - a < c - b"
  1052   by (simp add: field_simps)
  1053 
  1054 lemma diff_strict_right_mono: "a < b \<Longrightarrow> a - c < b - c"
  1055   by (simp add: field_simps)
  1056 
  1057 end
  1058 
  1059 ML_file "Tools/group_cancel.ML"
  1060 
  1061 simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =
  1062   {* fn phi => fn ss => try Group_Cancel.cancel_add_conv *}
  1063 
  1064 simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") =
  1065   {* fn phi => fn ss => try Group_Cancel.cancel_diff_conv *}
  1066 
  1067 simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") =
  1068   {* fn phi => fn ss => try Group_Cancel.cancel_eq_conv *}
  1069 
  1070 simproc_setup group_cancel_le ("a \<le> (b::'a::ordered_ab_group_add)") =
  1071   {* fn phi => fn ss => try Group_Cancel.cancel_le_conv *}
  1072 
  1073 simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") =
  1074   {* fn phi => fn ss => try Group_Cancel.cancel_less_conv *}
  1075 
  1076 class linordered_ab_semigroup_add =
  1077   linorder + ordered_ab_semigroup_add
  1078 
  1079 class linordered_cancel_ab_semigroup_add =
  1080   linorder + ordered_cancel_ab_semigroup_add
  1081 begin
  1082 
  1083 subclass linordered_ab_semigroup_add ..
  1084 
  1085 subclass ordered_ab_semigroup_add_imp_le
  1086 proof
  1087   fix a b c :: 'a
  1088   assume le: "c + a <= c + b"  
  1089   show "a <= b"
  1090   proof (rule ccontr)
  1091     assume w: "~ a \<le> b"
  1092     hence "b <= a" by (simp add: linorder_not_le)
  1093     hence le2: "c + b <= c + a" by (rule add_left_mono)
  1094     have "a = b" 
  1095       apply (insert le)
  1096       apply (insert le2)
  1097       apply (drule antisym, simp_all)
  1098       done
  1099     with w show False 
  1100       by (simp add: linorder_not_le [symmetric])
  1101   qed
  1102 qed
  1103 
  1104 end
  1105 
  1106 class linordered_ab_group_add = linorder + ordered_ab_group_add
  1107 begin
  1108 
  1109 subclass linordered_cancel_ab_semigroup_add ..
  1110 
  1111 lemma equal_neg_zero [simp]:
  1112   "a = - a \<longleftrightarrow> a = 0"
  1113 proof
  1114   assume "a = 0" then show "a = - a" by simp
  1115 next
  1116   assume A: "a = - a" show "a = 0"
  1117   proof (cases "0 \<le> a")
  1118     case True with A have "0 \<le> - a" by auto
  1119     with le_minus_iff have "a \<le> 0" by simp
  1120     with True show ?thesis by (auto intro: order_trans)
  1121   next
  1122     case False then have B: "a \<le> 0" by auto
  1123     with A have "- a \<le> 0" by auto
  1124     with B show ?thesis by (auto intro: order_trans)
  1125   qed
  1126 qed
  1127 
  1128 lemma neg_equal_zero [simp]:
  1129   "- a = a \<longleftrightarrow> a = 0"
  1130   by (auto dest: sym)
  1131 
  1132 lemma neg_less_eq_nonneg [simp]:
  1133   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
  1134 proof
  1135   assume A: "- a \<le> a" show "0 \<le> a"
  1136   proof (rule classical)
  1137     assume "\<not> 0 \<le> a"
  1138     then have "a < 0" by auto
  1139     with A have "- a < 0" by (rule le_less_trans)
  1140     then show ?thesis by auto
  1141   qed
  1142 next
  1143   assume A: "0 \<le> a" show "- a \<le> a"
  1144   proof (rule order_trans)
  1145     show "- a \<le> 0" using A by (simp add: minus_le_iff)
  1146   next
  1147     show "0 \<le> a" using A .
  1148   qed
  1149 qed
  1150 
  1151 lemma neg_less_pos [simp]:
  1152   "- a < a \<longleftrightarrow> 0 < a"
  1153   by (auto simp add: less_le)
  1154 
  1155 lemma less_eq_neg_nonpos [simp]:
  1156   "a \<le> - a \<longleftrightarrow> a \<le> 0"
  1157   using neg_less_eq_nonneg [of "- a"] by simp
  1158 
  1159 lemma less_neg_neg [simp]:
  1160   "a < - a \<longleftrightarrow> a < 0"
  1161   using neg_less_pos [of "- a"] by simp
  1162 
  1163 lemma double_zero [simp]:
  1164   "a + a = 0 \<longleftrightarrow> a = 0"
  1165 proof
  1166   assume assm: "a + a = 0"
  1167   then have a: "- a = a" by (rule minus_unique)
  1168   then show "a = 0" by (simp only: neg_equal_zero)
  1169 qed simp
  1170 
  1171 lemma double_zero_sym [simp]:
  1172   "0 = a + a \<longleftrightarrow> a = 0"
  1173   by (rule, drule sym) simp_all
  1174 
  1175 lemma zero_less_double_add_iff_zero_less_single_add [simp]:
  1176   "0 < a + a \<longleftrightarrow> 0 < a"
  1177 proof
  1178   assume "0 < a + a"
  1179   then have "0 - a < a" by (simp only: diff_less_eq)
  1180   then have "- a < a" by simp
  1181   then show "0 < a" by simp
  1182 next
  1183   assume "0 < a"
  1184   with this have "0 + 0 < a + a"
  1185     by (rule add_strict_mono)
  1186   then show "0 < a + a" by simp
  1187 qed
  1188 
  1189 lemma zero_le_double_add_iff_zero_le_single_add [simp]:
  1190   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
  1191   by (auto simp add: le_less)
  1192 
  1193 lemma double_add_less_zero_iff_single_add_less_zero [simp]:
  1194   "a + a < 0 \<longleftrightarrow> a < 0"
  1195 proof -
  1196   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
  1197     by (simp add: not_less)
  1198   then show ?thesis by simp
  1199 qed
  1200 
  1201 lemma double_add_le_zero_iff_single_add_le_zero [simp]:
  1202   "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
  1203 proof -
  1204   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
  1205     by (simp add: not_le)
  1206   then show ?thesis by simp
  1207 qed
  1208 
  1209 lemma minus_max_eq_min:
  1210   "- max x y = min (-x) (-y)"
  1211   by (auto simp add: max_def min_def)
  1212 
  1213 lemma minus_min_eq_max:
  1214   "- min x y = max (-x) (-y)"
  1215   by (auto simp add: max_def min_def)
  1216 
  1217 end
  1218 
  1219 class abs =
  1220   fixes abs :: "'a \<Rightarrow> 'a"
  1221 begin
  1222 
  1223 notation (xsymbols)
  1224   abs  ("\<bar>_\<bar>")
  1225 
  1226 notation (HTML output)
  1227   abs  ("\<bar>_\<bar>")
  1228 
  1229 end
  1230 
  1231 class sgn =
  1232   fixes sgn :: "'a \<Rightarrow> 'a"
  1233 
  1234 class abs_if = minus + uminus + ord + zero + abs +
  1235   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
  1236 
  1237 class sgn_if = minus + uminus + zero + one + ord + sgn +
  1238   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  1239 begin
  1240 
  1241 lemma sgn0 [simp]: "sgn 0 = 0"
  1242   by (simp add:sgn_if)
  1243 
  1244 end
  1245 
  1246 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
  1247   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
  1248     and abs_ge_self: "a \<le> \<bar>a\<bar>"
  1249     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
  1250     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
  1251     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1252 begin
  1253 
  1254 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
  1255   unfolding neg_le_0_iff_le by simp
  1256 
  1257 lemma abs_of_nonneg [simp]:
  1258   assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
  1259 proof (rule antisym)
  1260   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
  1261   from this nonneg have "- a \<le> a" by (rule order_trans)
  1262   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
  1263 qed (rule abs_ge_self)
  1264 
  1265 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
  1266 by (rule antisym)
  1267    (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
  1268 
  1269 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
  1270 proof -
  1271   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
  1272   proof (rule antisym)
  1273     assume zero: "\<bar>a\<bar> = 0"
  1274     with abs_ge_self show "a \<le> 0" by auto
  1275     from zero have "\<bar>-a\<bar> = 0" by simp
  1276     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
  1277     with neg_le_0_iff_le show "0 \<le> a" by auto
  1278   qed
  1279   then show ?thesis by auto
  1280 qed
  1281 
  1282 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
  1283 by simp
  1284 
  1285 lemma abs_0_eq [simp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
  1286 proof -
  1287   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
  1288   thus ?thesis by simp
  1289 qed
  1290 
  1291 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
  1292 proof
  1293   assume "\<bar>a\<bar> \<le> 0"
  1294   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
  1295   thus "a = 0" by simp
  1296 next
  1297   assume "a = 0"
  1298   thus "\<bar>a\<bar> \<le> 0" by simp
  1299 qed
  1300 
  1301 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
  1302 by (simp add: less_le)
  1303 
  1304 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
  1305 proof -
  1306   have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
  1307   show ?thesis by (simp add: a)
  1308 qed
  1309 
  1310 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
  1311 proof -
  1312   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
  1313   then show ?thesis by simp
  1314 qed
  1315 
  1316 lemma abs_minus_commute: 
  1317   "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
  1318 proof -
  1319   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
  1320   also have "... = \<bar>b - a\<bar>" by simp
  1321   finally show ?thesis .
  1322 qed
  1323 
  1324 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
  1325 by (rule abs_of_nonneg, rule less_imp_le)
  1326 
  1327 lemma abs_of_nonpos [simp]:
  1328   assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
  1329 proof -
  1330   let ?b = "- a"
  1331   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
  1332   unfolding abs_minus_cancel [of "?b"]
  1333   unfolding neg_le_0_iff_le [of "?b"]
  1334   unfolding minus_minus by (erule abs_of_nonneg)
  1335   then show ?thesis using assms by auto
  1336 qed
  1337   
  1338 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
  1339 by (rule abs_of_nonpos, rule less_imp_le)
  1340 
  1341 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
  1342 by (insert abs_ge_self, blast intro: order_trans)
  1343 
  1344 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
  1345 by (insert abs_le_D1 [of "- a"], simp)
  1346 
  1347 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
  1348 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
  1349 
  1350 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
  1351 proof -
  1352   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
  1353     by (simp add: algebra_simps)
  1354   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
  1355     by (simp add: abs_triangle_ineq)
  1356   then show ?thesis
  1357     by (simp add: algebra_simps)
  1358 qed
  1359 
  1360 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
  1361   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
  1362 
  1363 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
  1364   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
  1365 
  1366 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1367 proof -
  1368   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (simp add: algebra_simps)
  1369   also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
  1370   finally show ?thesis by simp
  1371 qed
  1372 
  1373 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
  1374 proof -
  1375   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: algebra_simps)
  1376   also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
  1377   finally show ?thesis .
  1378 qed
  1379 
  1380 lemma abs_add_abs [simp]:
  1381   "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
  1382 proof (rule antisym)
  1383   show "?L \<ge> ?R" by(rule abs_ge_self)
  1384 next
  1385   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
  1386   also have "\<dots> = ?R" by simp
  1387   finally show "?L \<le> ?R" .
  1388 qed
  1389 
  1390 end
  1391 
  1392 
  1393 subsection {* Tools setup *}
  1394 
  1395 lemma add_mono_thms_linordered_semiring:
  1396   fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"
  1397   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1398     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1399     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
  1400     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
  1401 by (rule add_mono, clarify+)+
  1402 
  1403 lemma add_mono_thms_linordered_field:
  1404   fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add"
  1405   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
  1406     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
  1407     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
  1408     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
  1409     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
  1410 by (auto intro: add_strict_right_mono add_strict_left_mono
  1411   add_less_le_mono add_le_less_mono add_strict_mono)
  1412 
  1413 code_identifier
  1414   code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1415 
  1416 end
  1417