src/HOL/Groups.thy
author fleury <Mathias.Fleury@mpi-inf.mpg.de>
Tue Jul 12 13:55:35 2016 +0200 (2016-07-12)
changeset 63456 3365c8ec67bd
parent 63364 4fa441c2f20c
child 63588 d0e2bad67bd4
permissions -rw-r--r--
sharing simp rules between ordered monoids and rings
     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_semigroup_monoid_add_imp_le = monoid_add + ordered_ab_semigroup_add_imp_le
   804 begin
   805 
   806 lemma add_less_same_cancel1 [simp]:
   807   "b + a < b \<longleftrightarrow> a < 0"
   808   using add_less_cancel_left [of _ _ 0] by simp
   809 
   810 lemma add_less_same_cancel2 [simp]:
   811   "a + b < b \<longleftrightarrow> a < 0"
   812   using add_less_cancel_right [of _ _ 0] by simp
   813 
   814 lemma less_add_same_cancel1 [simp]:
   815   "a < a + b \<longleftrightarrow> 0 < b"
   816   using add_less_cancel_left [of _ 0] by simp
   817 
   818 lemma less_add_same_cancel2 [simp]:
   819   "a < b + a \<longleftrightarrow> 0 < b"
   820   using add_less_cancel_right [of 0] by simp
   821 
   822 lemma add_le_same_cancel1 [simp]:
   823   "b + a \<le> b \<longleftrightarrow> a \<le> 0"
   824   using add_le_cancel_left [of _ _ 0] by simp
   825 
   826 lemma add_le_same_cancel2 [simp]:
   827   "a + b \<le> b \<longleftrightarrow> a \<le> 0"
   828   using add_le_cancel_right [of _ _ 0] by simp
   829 
   830 lemma le_add_same_cancel1 [simp]:
   831   "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
   832   using add_le_cancel_left [of _ 0] by simp
   833 
   834 lemma le_add_same_cancel2 [simp]:
   835   "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
   836   using add_le_cancel_right [of 0] by simp
   837 
   838 subclass cancel_comm_monoid_add
   839   by standard auto
   840 
   841 subclass ordered_cancel_comm_monoid_add
   842   by standard
   843 
   844 end
   845 
   846 class ordered_ab_group_add = ab_group_add + ordered_ab_semigroup_add
   847 begin
   848 
   849 subclass ordered_cancel_ab_semigroup_add ..
   850 
   851 subclass ordered_ab_semigroup_monoid_add_imp_le
   852 proof
   853   fix a b c :: 'a
   854   assume "c + a \<le> c + b"
   855   then have "(-c) + (c + a) \<le> (-c) + (c + b)"
   856     by (rule add_left_mono)
   857   then have "((-c) + c) + a \<le> ((-c) + c) + b"
   858     by (simp only: add.assoc)
   859   then show "a \<le> b" by simp
   860 qed
   861 
   862 lemma max_diff_distrib_left: "max x y - z = max (x - z) (y - z)"
   863   using max_add_distrib_left [of x y "- z"] by simp
   864 
   865 lemma min_diff_distrib_left: "min x y - z = min (x - z) (y - z)"
   866   using min_add_distrib_left [of x y "- z"] by simp
   867 
   868 lemma le_imp_neg_le:
   869   assumes "a \<le> b"
   870   shows "- b \<le> - a"
   871 proof -
   872   from assms have "- a + a \<le> - a + b"
   873     by (rule add_left_mono)
   874   then have "0 \<le> - a + b"
   875     by simp
   876   then have "0 + (- b) \<le> (- a + b) + (- b)"
   877     by (rule add_right_mono)
   878   then show ?thesis
   879     by (simp add: algebra_simps)
   880 qed
   881 
   882 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
   883 proof
   884   assume "- b \<le> - a"
   885   then have "- (- a) \<le> - (- b)"
   886     by (rule le_imp_neg_le)
   887   then show "a \<le> b"
   888     by simp
   889 next
   890   assume "a \<le> b"
   891   then show "- b \<le> - a"
   892     by (rule le_imp_neg_le)
   893 qed
   894 
   895 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   896   by (subst neg_le_iff_le [symmetric]) simp
   897 
   898 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
   899   by (subst neg_le_iff_le [symmetric]) simp
   900 
   901 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
   902   by (auto simp add: less_le)
   903 
   904 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
   905   by (subst neg_less_iff_less [symmetric]) simp
   906 
   907 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
   908   by (subst neg_less_iff_less [symmetric]) simp
   909 
   910 text \<open>The next several equations can make the simplifier loop!\<close>
   911 
   912 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
   913 proof -
   914   have "- (-a) < - b \<longleftrightarrow> b < - a"
   915     by (rule neg_less_iff_less)
   916   then show ?thesis by simp
   917 qed
   918 
   919 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
   920 proof -
   921   have "- a < - (- b) \<longleftrightarrow> - b < a"
   922     by (rule neg_less_iff_less)
   923   then show ?thesis by simp
   924 qed
   925 
   926 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
   927 proof -
   928   have mm: "- (- a) < -b \<Longrightarrow> - (- b) < -a" for a b :: 'a
   929     by (simp only: minus_less_iff)
   930   have "- (- a) \<le> -b \<longleftrightarrow> b \<le> - a"
   931     apply (auto simp only: le_less)
   932     apply (drule mm)
   933     apply (simp_all)
   934     apply (drule mm[simplified], assumption)
   935     done
   936   then show ?thesis by simp
   937 qed
   938 
   939 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
   940   by (auto simp add: le_less minus_less_iff)
   941 
   942 lemma diff_less_0_iff_less [simp]: "a - b < 0 \<longleftrightarrow> a < b"
   943 proof -
   944   have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)"
   945     by simp
   946   also have "\<dots> \<longleftrightarrow> a < b"
   947     by (simp only: add_less_cancel_right)
   948   finally show ?thesis .
   949 qed
   950 
   951 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]
   952 
   953 lemma diff_less_eq [algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b"
   954   apply (subst less_iff_diff_less_0 [of a])
   955   apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
   956   apply (simp add: algebra_simps)
   957   done
   958 
   959 lemma less_diff_eq[algebra_simps, field_simps]: "a < c - b \<longleftrightarrow> a + b < c"
   960   apply (subst less_iff_diff_less_0 [of "a + b"])
   961   apply (subst less_iff_diff_less_0 [of a])
   962   apply (simp add: algebra_simps)
   963   done
   964 
   965 lemma diff_gt_0_iff_gt [simp]: "a - b > 0 \<longleftrightarrow> a > b"
   966   by (simp add: less_diff_eq)
   967 
   968 lemma diff_le_eq [algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
   969   by (auto simp add: le_less diff_less_eq )
   970 
   971 lemma le_diff_eq [algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
   972   by (auto simp add: le_less less_diff_eq)
   973 
   974 lemma diff_le_0_iff_le [simp]: "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
   975   by (simp add: algebra_simps)
   976 
   977 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]
   978 
   979 lemma diff_ge_0_iff_ge [simp]: "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
   980   by (simp add: le_diff_eq)
   981 
   982 lemma diff_eq_diff_less: "a - b = c - d \<Longrightarrow> a < b \<longleftrightarrow> c < d"
   983   by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])
   984 
   985 lemma diff_eq_diff_less_eq: "a - b = c - d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d"
   986   by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])
   987 
   988 lemma diff_mono: "a \<le> b \<Longrightarrow> d \<le> c \<Longrightarrow> a - c \<le> b - d"
   989   by (simp add: field_simps add_mono)
   990 
   991 lemma diff_left_mono: "b \<le> a \<Longrightarrow> c - a \<le> c - b"
   992   by (simp add: field_simps)
   993 
   994 lemma diff_right_mono: "a \<le> b \<Longrightarrow> a - c \<le> b - c"
   995   by (simp add: field_simps)
   996 
   997 lemma diff_strict_mono: "a < b \<Longrightarrow> d < c \<Longrightarrow> a - c < b - d"
   998   by (simp add: field_simps add_strict_mono)
   999 
  1000 lemma diff_strict_left_mono: "b < a \<Longrightarrow> c - a < c - b"
  1001   by (simp add: field_simps)
  1002 
  1003 lemma diff_strict_right_mono: "a < b \<Longrightarrow> a - c < b - c"
  1004   by (simp add: field_simps)
  1005 
  1006 end
  1007 
  1008 ML_file "Tools/group_cancel.ML"
  1009 
  1010 simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =
  1011   \<open>fn phi => fn ss => try Group_Cancel.cancel_add_conv\<close>
  1012 
  1013 simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") =
  1014   \<open>fn phi => fn ss => try Group_Cancel.cancel_diff_conv\<close>
  1015 
  1016 simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") =
  1017   \<open>fn phi => fn ss => try Group_Cancel.cancel_eq_conv\<close>
  1018 
  1019 simproc_setup group_cancel_le ("a \<le> (b::'a::ordered_ab_group_add)") =
  1020   \<open>fn phi => fn ss => try Group_Cancel.cancel_le_conv\<close>
  1021 
  1022 simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") =
  1023   \<open>fn phi => fn ss => try Group_Cancel.cancel_less_conv\<close>
  1024 
  1025 class linordered_ab_semigroup_add =
  1026   linorder + ordered_ab_semigroup_add
  1027 
  1028 class linordered_cancel_ab_semigroup_add =
  1029   linorder + ordered_cancel_ab_semigroup_add
  1030 begin
  1031 
  1032 subclass linordered_ab_semigroup_add ..
  1033 
  1034 subclass ordered_ab_semigroup_add_imp_le
  1035 proof
  1036   fix a b c :: 'a
  1037   assume le1: "c + a \<le> c + b"
  1038   show "a \<le> b"
  1039   proof (rule ccontr)
  1040     assume *: "\<not> ?thesis"
  1041     then have "b \<le> a" by (simp add: linorder_not_le)
  1042     then have le2: "c + b \<le> c + a" by (rule add_left_mono)
  1043     have "a = b"
  1044       apply (insert le1 le2)
  1045       apply (drule antisym)
  1046       apply simp_all
  1047       done
  1048     with * show False
  1049       by (simp add: linorder_not_le [symmetric])
  1050   qed
  1051 qed
  1052 
  1053 end
  1054 
  1055 class linordered_ab_group_add = linorder + ordered_ab_group_add
  1056 begin
  1057 
  1058 subclass linordered_cancel_ab_semigroup_add ..
  1059 
  1060 lemma equal_neg_zero [simp]: "a = - a \<longleftrightarrow> a = 0"
  1061 proof
  1062   assume "a = 0"
  1063   then show "a = - a" by simp
  1064 next
  1065   assume A: "a = - a"
  1066   show "a = 0"
  1067   proof (cases "0 \<le> a")
  1068     case True
  1069     with A have "0 \<le> - a" by auto
  1070     with le_minus_iff have "a \<le> 0" by simp
  1071     with True show ?thesis by (auto intro: order_trans)
  1072   next
  1073     case False
  1074     then have B: "a \<le> 0" by auto
  1075     with A have "- a \<le> 0" by auto
  1076     with B show ?thesis by (auto intro: order_trans)
  1077   qed
  1078 qed
  1079 
  1080 lemma neg_equal_zero [simp]: "- a = a \<longleftrightarrow> a = 0"
  1081   by (auto dest: sym)
  1082 
  1083 lemma neg_less_eq_nonneg [simp]: "- a \<le> a \<longleftrightarrow> 0 \<le> a"
  1084 proof
  1085   assume *: "- a \<le> a"
  1086   show "0 \<le> a"
  1087   proof (rule classical)
  1088     assume "\<not> ?thesis"
  1089     then have "a < 0" by auto
  1090     with * have "- a < 0" by (rule le_less_trans)
  1091     then show ?thesis by auto
  1092   qed
  1093 next
  1094   assume *: "0 \<le> a"
  1095   then have "- a \<le> 0" by (simp add: minus_le_iff)
  1096   from this * show "- a \<le> a" by (rule order_trans)
  1097 qed
  1098 
  1099 lemma neg_less_pos [simp]: "- a < a \<longleftrightarrow> 0 < a"
  1100   by (auto simp add: less_le)
  1101 
  1102 lemma less_eq_neg_nonpos [simp]: "a \<le> - a \<longleftrightarrow> a \<le> 0"
  1103   using neg_less_eq_nonneg [of "- a"] by simp
  1104 
  1105 lemma less_neg_neg [simp]: "a < - a \<longleftrightarrow> a < 0"
  1106   using neg_less_pos [of "- a"] by simp
  1107 
  1108 lemma double_zero [simp]: "a + a = 0 \<longleftrightarrow> a = 0"
  1109 proof
  1110   assume "a + a = 0"
  1111   then have a: "- a = a" by (rule minus_unique)
  1112   then show "a = 0" by (simp only: neg_equal_zero)
  1113 next
  1114   assume "a = 0"
  1115   then show "a + a = 0" by simp
  1116 qed
  1117 
  1118 lemma double_zero_sym [simp]: "0 = a + a \<longleftrightarrow> a = 0"
  1119   apply (rule iffI)
  1120   apply (drule sym)
  1121   apply simp_all
  1122   done
  1123 
  1124 lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \<longleftrightarrow> 0 < a"
  1125 proof
  1126   assume "0 < a + a"
  1127   then have "0 - a < a" by (simp only: diff_less_eq)
  1128   then have "- a < a" by simp
  1129   then show "0 < a" by simp
  1130 next
  1131   assume "0 < a"
  1132   with this have "0 + 0 < a + a"
  1133     by (rule add_strict_mono)
  1134   then show "0 < a + a" by simp
  1135 qed
  1136 
  1137 lemma zero_le_double_add_iff_zero_le_single_add [simp]: "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
  1138   by (auto simp add: le_less)
  1139 
  1140 lemma double_add_less_zero_iff_single_add_less_zero [simp]: "a + a < 0 \<longleftrightarrow> a < 0"
  1141 proof -
  1142   have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0"
  1143     by (simp add: not_less)
  1144   then show ?thesis by simp
  1145 qed
  1146 
  1147 lemma double_add_le_zero_iff_single_add_le_zero [simp]: "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
  1148 proof -
  1149   have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0"
  1150     by (simp add: not_le)
  1151   then show ?thesis by simp
  1152 qed
  1153 
  1154 lemma minus_max_eq_min: "- max x y = min (- x) (- y)"
  1155   by (auto simp add: max_def min_def)
  1156 
  1157 lemma minus_min_eq_max: "- min x y = max (- x) (- y)"
  1158   by (auto simp add: max_def min_def)
  1159 
  1160 end
  1161 
  1162 class abs =
  1163   fixes abs :: "'a \<Rightarrow> 'a"  ("\<bar>_\<bar>")
  1164 
  1165 class sgn =
  1166   fixes sgn :: "'a \<Rightarrow> 'a"
  1167 
  1168 class abs_if = minus + uminus + ord + zero + abs +
  1169   assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
  1170 
  1171 class sgn_if = minus + uminus + zero + one + ord + sgn +
  1172   assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  1173 begin
  1174 
  1175 lemma sgn0 [simp]: "sgn 0 = 0"
  1176   by (simp add:sgn_if)
  1177 
  1178 end
  1179 
  1180 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
  1181   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
  1182     and abs_ge_self: "a \<le> \<bar>a\<bar>"
  1183     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
  1184     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
  1185     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1186 begin
  1187 
  1188 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
  1189   unfolding neg_le_0_iff_le by simp
  1190 
  1191 lemma abs_of_nonneg [simp]:
  1192   assumes nonneg: "0 \<le> a"
  1193   shows "\<bar>a\<bar> = a"
  1194 proof (rule antisym)
  1195   show "a \<le> \<bar>a\<bar>" by (rule abs_ge_self)
  1196   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
  1197   from this nonneg have "- a \<le> a" by (rule order_trans)
  1198   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
  1199 qed
  1200 
  1201 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
  1202   by (rule antisym) (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
  1203 
  1204 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
  1205 proof -
  1206   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
  1207   proof (rule antisym)
  1208     assume zero: "\<bar>a\<bar> = 0"
  1209     with abs_ge_self show "a \<le> 0" by auto
  1210     from zero have "\<bar>-a\<bar> = 0" by simp
  1211     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
  1212     with neg_le_0_iff_le show "0 \<le> a" by auto
  1213   qed
  1214   then show ?thesis by auto
  1215 qed
  1216 
  1217 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
  1218   by simp
  1219 
  1220 lemma abs_0_eq [simp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
  1221 proof -
  1222   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
  1223   then show ?thesis by simp
  1224 qed
  1225 
  1226 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"
  1227 proof
  1228   assume "\<bar>a\<bar> \<le> 0"
  1229   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
  1230   then show "a = 0" by simp
  1231 next
  1232   assume "a = 0"
  1233   then show "\<bar>a\<bar> \<le> 0" by simp
  1234 qed
  1235 
  1236 lemma abs_le_self_iff [simp]: "\<bar>a\<bar> \<le> a \<longleftrightarrow> 0 \<le> a"
  1237 proof -
  1238   have "0 \<le> \<bar>a\<bar>"
  1239     using abs_ge_zero by blast
  1240   then have "\<bar>a\<bar> \<le> a \<Longrightarrow> 0 \<le> a"
  1241     using order.trans by blast
  1242   then show ?thesis
  1243     using abs_of_nonneg eq_refl by blast
  1244 qed
  1245 
  1246 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
  1247   by (simp add: less_le)
  1248 
  1249 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
  1250 proof -
  1251   have "x \<le> y \<Longrightarrow> \<not> y < x" for x y by auto
  1252   then show ?thesis by simp
  1253 qed
  1254 
  1255 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
  1256 proof -
  1257   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
  1258   then show ?thesis by simp
  1259 qed
  1260 
  1261 lemma abs_minus_commute: "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
  1262 proof -
  1263   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>"
  1264     by (simp only: abs_minus_cancel)
  1265   also have "\<dots> = \<bar>b - a\<bar>" by simp
  1266   finally show ?thesis .
  1267 qed
  1268 
  1269 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
  1270   by (rule abs_of_nonneg) (rule less_imp_le)
  1271 
  1272 lemma abs_of_nonpos [simp]:
  1273   assumes "a \<le> 0"
  1274   shows "\<bar>a\<bar> = - a"
  1275 proof -
  1276   let ?b = "- a"
  1277   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
  1278     unfolding abs_minus_cancel [of ?b]
  1279     unfolding neg_le_0_iff_le [of ?b]
  1280     unfolding minus_minus by (erule abs_of_nonneg)
  1281   then show ?thesis using assms by auto
  1282 qed
  1283 
  1284 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
  1285   by (rule abs_of_nonpos) (rule less_imp_le)
  1286 
  1287 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
  1288   using abs_ge_self by (blast intro: order_trans)
  1289 
  1290 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
  1291   using abs_le_D1 [of "- a"] by simp
  1292 
  1293 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
  1294   by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
  1295 
  1296 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
  1297 proof -
  1298   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
  1299     by (simp add: algebra_simps)
  1300   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
  1301     by (simp add: abs_triangle_ineq)
  1302   then show ?thesis
  1303     by (simp add: algebra_simps)
  1304 qed
  1305 
  1306 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
  1307   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
  1308 
  1309 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
  1310   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
  1311 
  1312 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1313 proof -
  1314   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>"
  1315     by (simp add: algebra_simps)
  1316   also have "\<dots> \<le> \<bar>a\<bar> + \<bar>- b\<bar>"
  1317     by (rule abs_triangle_ineq)
  1318   finally show ?thesis by simp
  1319 qed
  1320 
  1321 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
  1322 proof -
  1323   have "\<bar>a + b - (c + d)\<bar> = \<bar>(a - c) + (b - d)\<bar>"
  1324     by (simp add: algebra_simps)
  1325   also have "\<dots> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
  1326     by (rule abs_triangle_ineq)
  1327   finally show ?thesis .
  1328 qed
  1329 
  1330 lemma abs_add_abs [simp]: "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>"
  1331   (is "?L = ?R")
  1332 proof (rule antisym)
  1333   show "?L \<ge> ?R" by (rule abs_ge_self)
  1334   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by (rule abs_triangle_ineq)
  1335   also have "\<dots> = ?R" by simp
  1336   finally show "?L \<le> ?R" .
  1337 qed
  1338 
  1339 end
  1340 
  1341 lemma dense_eq0_I:
  1342   fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
  1343   shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) \<Longrightarrow> x = 0"
  1344   apply (cases "\<bar>x\<bar> = 0")
  1345   apply simp
  1346   apply (simp only: zero_less_abs_iff [symmetric])
  1347   apply (drule dense)
  1348   apply (auto simp add: not_less [symmetric])
  1349   done
  1350 
  1351 hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus
  1352 
  1353 lemmas add_0 = add_0_left (* FIXME duplicate *)
  1354 lemmas mult_1 = mult_1_left (* FIXME duplicate *)
  1355 lemmas ab_left_minus = left_minus (* FIXME duplicate *)
  1356 lemmas diff_diff_eq = diff_diff_add (* FIXME duplicate *)
  1357 
  1358 
  1359 subsection \<open>Canonically ordered monoids\<close>
  1360 
  1361 text \<open>Canonically ordered monoids are never groups.\<close>
  1362 
  1363 class canonically_ordered_monoid_add = comm_monoid_add + order +
  1364   assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
  1365 begin
  1366 
  1367 lemma zero_le[simp]: "0 \<le> x"
  1368   by (auto simp: le_iff_add)
  1369 
  1370 lemma le_zero_eq[simp]: "n \<le> 0 \<longleftrightarrow> n = 0"
  1371   by (auto intro: antisym)
  1372 
  1373 lemma not_less_zero[simp]: "\<not> n < 0"
  1374   by (auto simp: less_le)
  1375 
  1376 lemma zero_less_iff_neq_zero: "0 < n \<longleftrightarrow> n \<noteq> 0"
  1377   by (auto simp: less_le)
  1378 
  1379 text \<open>This theorem is useful with \<open>blast\<close>\<close>
  1380 lemma gr_zeroI: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n"
  1381   by (rule zero_less_iff_neq_zero[THEN iffD2]) iprover
  1382 
  1383 lemma not_gr_zero[simp]: "\<not> 0 < n \<longleftrightarrow> n = 0"
  1384   by (simp add: zero_less_iff_neq_zero)
  1385 
  1386 subclass ordered_comm_monoid_add
  1387   proof qed (auto simp: le_iff_add add_ac)
  1388 
  1389 lemma add_eq_0_iff_both_eq_0: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
  1390   by (intro add_nonneg_eq_0_iff zero_le)
  1391 
  1392 lemma gr_implies_not_zero: "m < n \<Longrightarrow> n \<noteq> 0"
  1393   using add_eq_0_iff_both_eq_0[of m] by (auto simp: le_iff_add less_le)
  1394 
  1395 lemmas zero_order = zero_le le_zero_eq not_less_zero zero_less_iff_neq_zero not_gr_zero
  1396   \<comment> \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close>
  1397 
  1398 end
  1399 
  1400 class ordered_cancel_comm_monoid_diff =
  1401   canonically_ordered_monoid_add + comm_monoid_diff + ordered_ab_semigroup_add_imp_le
  1402 begin
  1403 
  1404 context
  1405   fixes a b
  1406   assumes le: "a \<le> b"
  1407 begin
  1408 
  1409 lemma add_diff_inverse: "a + (b - a) = b"
  1410   using le by (auto simp add: le_iff_add)
  1411 
  1412 lemma add_diff_assoc: "c + (b - a) = c + b - a"
  1413   using le by (auto simp add: le_iff_add add.left_commute [of c])
  1414 
  1415 lemma add_diff_assoc2: "b - a + c = b + c - a"
  1416   using le by (auto simp add: le_iff_add add.assoc)
  1417 
  1418 lemma diff_add_assoc: "c + b - a = c + (b - a)"
  1419   using le by (simp add: add.commute add_diff_assoc)
  1420 
  1421 lemma diff_add_assoc2: "b + c - a = b - a + c"
  1422   using le by (simp add: add.commute add_diff_assoc)
  1423 
  1424 lemma diff_diff_right: "c - (b - a) = c + a - b"
  1425   by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add.commute)
  1426 
  1427 lemma diff_add: "b - a + a = b"
  1428   by (simp add: add.commute add_diff_inverse)
  1429 
  1430 lemma le_add_diff: "c \<le> b + c - a"
  1431   by (auto simp add: add.commute diff_add_assoc2 le_iff_add)
  1432 
  1433 lemma le_imp_diff_is_add: "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
  1434   by (auto simp add: add.commute add_diff_inverse)
  1435 
  1436 lemma le_diff_conv2: "c \<le> b - a \<longleftrightarrow> c + a \<le> b"
  1437   (is "?P \<longleftrightarrow> ?Q")
  1438 proof
  1439   assume ?P
  1440   then have "c + a \<le> b - a + a"
  1441     by (rule add_right_mono)
  1442   then show ?Q
  1443     by (simp add: add_diff_inverse add.commute)
  1444 next
  1445   assume ?Q
  1446   then have "a + c \<le> a + (b - a)"
  1447     by (simp add: add_diff_inverse add.commute)
  1448   then show ?P by simp
  1449 qed
  1450 
  1451 end
  1452 
  1453 end
  1454 
  1455 
  1456 subsection \<open>Tools setup\<close>
  1457 
  1458 lemma add_mono_thms_linordered_semiring:
  1459   fixes i j k :: "'a::ordered_ab_semigroup_add"
  1460   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1461     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1462     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
  1463     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
  1464   by (rule add_mono, clarify+)+
  1465 
  1466 lemma add_mono_thms_linordered_field:
  1467   fixes i j k :: "'a::ordered_cancel_ab_semigroup_add"
  1468   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
  1469     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
  1470     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
  1471     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
  1472     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
  1473   by (auto intro: add_strict_right_mono add_strict_left_mono
  1474       add_less_le_mono add_le_less_mono add_strict_mono)
  1475 
  1476 code_identifier
  1477   code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1478 
  1479 end