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