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