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