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