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