src/HOL/Groups.thy
author wenzelm
Tue Aug 02 21:05:34 2016 +0200 (2016-08-02)
changeset 63588 d0e2bad67bd4
parent 63456 3365c8ec67bd
child 63680 6e1e8b5abbfa
permissions -rw-r--r--
misc tuning and modernization;
     1 (*  Title:      HOL/Groups.thy
     2     Author:     Gertrud Bauer
     3     Author:     Steven Obua
     4     Author:     Lawrence C Paulson
     5     Author:     Markus Wenzel
     6     Author:     Jeremy Avigad
     7 *)
     8 
     9 section \<open>Groups, also combined with orderings\<close>
    10 
    11 theory Groups
    12   imports Orderings
    13 begin
    14 
    15 subsection \<open>Dynamic facts\<close>
    16 
    17 named_theorems ac_simps "associativity and commutativity simplification rules"
    18   and algebra_simps "algebra simplification rules"
    19   and field_simps "algebra simplification rules for fields"
    20 
    21 text \<open>
    22   The rewrites accumulated in \<open>algebra_simps\<close> deal with the classical
    23   algebraic structures of groups, rings and family. They simplify terms by
    24   multiplying everything out (in case of a ring) and bringing sums and
    25   products into a canonical form (by ordered rewriting). As a result it
    26   decides group and ring equalities but also helps with inequalities.
    27 
    28   Of course it also works for fields, but it knows nothing about
    29   multiplicative inverses or division. This is catered for by \<open>field_simps\<close>.
    30 
    31   Facts in \<open>field_simps\<close> multiply with denominators in (in)equations if they
    32   can be proved to be non-zero (for equations) or positive/negative (for
    33   inequalities). Can be too aggressive and is therefore separate from the more
    34   benign \<open>algebra_simps\<close>.
    35 \<close>
    36 
    37 
    38 subsection \<open>Abstract structures\<close>
    39 
    40 text \<open>
    41   These locales provide basic structures for interpretation into bigger
    42   structures; extensions require careful thinking, otherwise undesired effects
    43   may occur due to interpretation.
    44 \<close>
    45 
    46 locale semigroup =
    47   fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^bold>*" 70)
    48   assumes assoc [ac_simps]: "a \<^bold>* b \<^bold>* c = a \<^bold>* (b \<^bold>* c)"
    49 
    50 locale abel_semigroup = semigroup +
    51   assumes commute [ac_simps]: "a \<^bold>* b = b \<^bold>* a"
    52 begin
    53 
    54 lemma left_commute [ac_simps]: "b \<^bold>* (a \<^bold>* c) = a \<^bold>* (b \<^bold>* c)"
    55 proof -
    56   have "(b \<^bold>* a) \<^bold>* c = (a \<^bold>* b) \<^bold>* c"
    57     by (simp only: commute)
    58   then show ?thesis
    59     by (simp only: assoc)
    60 qed
    61 
    62 end
    63 
    64 locale monoid = semigroup +
    65   fixes z :: 'a ("\<^bold>1")
    66   assumes left_neutral [simp]: "\<^bold>1 \<^bold>* a = a"
    67   assumes right_neutral [simp]: "a \<^bold>* \<^bold>1 = a"
    68 
    69 locale comm_monoid = abel_semigroup +
    70   fixes z :: 'a ("\<^bold>1")
    71   assumes comm_neutral: "a \<^bold>* \<^bold>1 = a"
    72 begin
    73 
    74 sublocale monoid
    75   by standard (simp_all add: commute comm_neutral)
    76 
    77 end
    78 
    79 locale group = semigroup +
    80   fixes z :: 'a ("\<^bold>1")
    81   fixes inverse :: "'a \<Rightarrow> 'a"
    82   assumes group_left_neutral: "\<^bold>1 \<^bold>* a = a"
    83   assumes left_inverse [simp]:  "inverse a \<^bold>* a = \<^bold>1"
    84 begin
    85 
    86 lemma left_cancel: "a \<^bold>* b = a \<^bold>* c \<longleftrightarrow> b = c"
    87 proof
    88   assume "a \<^bold>* b = a \<^bold>* c"
    89   then have "inverse a \<^bold>* (a \<^bold>* b) = inverse a \<^bold>* (a \<^bold>* c)" by simp
    90   then have "(inverse a \<^bold>* a) \<^bold>* b = (inverse a \<^bold>* a) \<^bold>* c"
    91     by (simp only: assoc)
    92   then show "b = c" by (simp add: group_left_neutral)
    93 qed simp
    94 
    95 sublocale monoid
    96 proof
    97   fix a
    98   have "inverse a \<^bold>* a = \<^bold>1" by simp
    99   then have "inverse a \<^bold>* (a \<^bold>* \<^bold>1) = inverse a \<^bold>* a"
   100     by (simp add: group_left_neutral assoc [symmetric])
   101   with left_cancel show "a \<^bold>* \<^bold>1 = a"
   102     by (simp only: left_cancel)
   103 qed (fact group_left_neutral)
   104 
   105 lemma inverse_unique:
   106   assumes "a \<^bold>* b = \<^bold>1"
   107   shows "inverse a = b"
   108 proof -
   109   from assms have "inverse a \<^bold>* (a \<^bold>* b) = inverse a"
   110     by simp
   111   then show ?thesis
   112     by (simp add: assoc [symmetric])
   113 qed
   114 
   115 lemma inverse_neutral [simp]: "inverse \<^bold>1 = \<^bold>1"
   116   by (rule inverse_unique) simp
   117 
   118 lemma inverse_inverse [simp]: "inverse (inverse a) = a"
   119   by (rule inverse_unique) simp
   120 
   121 lemma right_inverse [simp]: "a \<^bold>* inverse a = \<^bold>1"
   122 proof -
   123   have "a \<^bold>* inverse a = inverse (inverse a) \<^bold>* inverse a"
   124     by simp
   125   also have "\<dots> = \<^bold>1"
   126     by (rule left_inverse)
   127   then show ?thesis by simp
   128 qed
   129 
   130 lemma inverse_distrib_swap: "inverse (a \<^bold>* b) = inverse b \<^bold>* inverse a"
   131 proof (rule inverse_unique)
   132   have "a \<^bold>* b \<^bold>* (inverse b \<^bold>* inverse a) =
   133     a \<^bold>* (b \<^bold>* inverse b) \<^bold>* inverse a"
   134     by (simp only: assoc)
   135   also have "\<dots> = \<^bold>1"
   136     by simp
   137   finally show "a \<^bold>* b \<^bold>* (inverse b \<^bold>* inverse a) = \<^bold>1" .
   138 qed
   139 
   140 lemma right_cancel: "b \<^bold>* a = c \<^bold>* a \<longleftrightarrow> b = c"
   141 proof
   142   assume "b \<^bold>* a = c \<^bold>* a"
   143   then have "b \<^bold>* a \<^bold>* inverse a= c \<^bold>* a \<^bold>* inverse a"
   144     by simp
   145   then show "b = c"
   146     by (simp add: assoc)
   147 qed simp
   148 
   149 end
   150 
   151 
   152 subsection \<open>Generic operations\<close>
   153 
   154 class zero =
   155   fixes zero :: 'a  ("0")
   156 
   157 class one =
   158   fixes one  :: 'a  ("1")
   159 
   160 hide_const (open) zero one
   161 
   162 lemma Let_0 [simp]: "Let 0 f = f 0"
   163   unfolding Let_def ..
   164 
   165 lemma Let_1 [simp]: "Let 1 f = f 1"
   166   unfolding Let_def ..
   167 
   168 setup \<open>
   169   Reorient_Proc.add
   170     (fn Const(@{const_name Groups.zero}, _) => true
   171       | Const(@{const_name Groups.one}, _) => true
   172       | _ => false)
   173 \<close>
   174 
   175 simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
   176 simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
   177 
   178 typed_print_translation \<open>
   179   let
   180     fun tr' c = (c, fn ctxt => fn T => fn ts =>
   181       if null ts andalso Printer.type_emphasis ctxt T then
   182         Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $
   183           Syntax_Phases.term_of_typ ctxt T
   184       else raise Match);
   185   in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
   186 \<close> \<comment> \<open>show types that are presumably too general\<close>
   187 
   188 class plus =
   189   fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
   190 
   191 class minus =
   192   fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
   193 
   194 class uminus =
   195   fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
   196 
   197 class times =
   198   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
   199 
   200 
   201 subsection \<open>Semigroups and Monoids\<close>
   202 
   203 class semigroup_add = plus +
   204   assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"
   205 begin
   206 
   207 sublocale add: semigroup plus
   208   by standard (fact add_assoc)
   209 
   210 end
   211 
   212 hide_fact add_assoc
   213 
   214 class ab_semigroup_add = semigroup_add +
   215   assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
   216 begin
   217 
   218 sublocale add: abel_semigroup plus
   219   by standard (fact add_commute)
   220 
   221 declare add.left_commute [algebra_simps, field_simps]
   222 
   223 lemmas add_ac = add.assoc add.commute add.left_commute
   224 
   225 end
   226 
   227 hide_fact add_commute
   228 
   229 lemmas add_ac = add.assoc add.commute add.left_commute
   230 
   231 class semigroup_mult = times +
   232   assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
   233 begin
   234 
   235 sublocale mult: semigroup times
   236   by standard (fact mult_assoc)
   237 
   238 end
   239 
   240 hide_fact mult_assoc
   241 
   242 class ab_semigroup_mult = semigroup_mult +
   243   assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
   244 begin
   245 
   246 sublocale mult: abel_semigroup times
   247   by standard (fact mult_commute)
   248 
   249 declare mult.left_commute [algebra_simps, field_simps]
   250 
   251 lemmas mult_ac = mult.assoc mult.commute mult.left_commute
   252 
   253 end
   254 
   255 hide_fact mult_commute
   256 
   257 lemmas mult_ac = mult.assoc mult.commute mult.left_commute
   258 
   259 class monoid_add = zero + semigroup_add +
   260   assumes add_0_left: "0 + a = a"
   261     and add_0_right: "a + 0 = a"
   262 begin
   263 
   264 sublocale add: monoid plus 0
   265   by standard (fact add_0_left add_0_right)+
   266 
   267 end
   268 
   269 lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
   270   by (fact eq_commute)
   271 
   272 class comm_monoid_add = zero + ab_semigroup_add +
   273   assumes add_0: "0 + a = a"
   274 begin
   275 
   276 subclass monoid_add
   277   by standard (simp_all add: add_0 add.commute [of _ 0])
   278 
   279 sublocale add: comm_monoid plus 0
   280   by standard (simp add: ac_simps)
   281 
   282 end
   283 
   284 class monoid_mult = one + semigroup_mult +
   285   assumes mult_1_left: "1 * a  = a"
   286     and mult_1_right: "a * 1 = a"
   287 begin
   288 
   289 sublocale mult: monoid times 1
   290   by standard (fact mult_1_left mult_1_right)+
   291 
   292 end
   293 
   294 lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
   295   by (fact eq_commute)
   296 
   297 class comm_monoid_mult = one + ab_semigroup_mult +
   298   assumes mult_1: "1 * a = a"
   299 begin
   300 
   301 subclass monoid_mult
   302   by standard (simp_all add: mult_1 mult.commute [of _ 1])
   303 
   304 sublocale mult: comm_monoid times 1
   305   by standard (simp add: ac_simps)
   306 
   307 end
   308 
   309 class cancel_semigroup_add = semigroup_add +
   310   assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
   311   assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
   312 begin
   313 
   314 lemma add_left_cancel [simp]: "a + b = a + c \<longleftrightarrow> b = c"
   315   by (blast dest: add_left_imp_eq)
   316 
   317 lemma add_right_cancel [simp]: "b + a = c + a \<longleftrightarrow> b = c"
   318   by (blast dest: add_right_imp_eq)
   319 
   320 end
   321 
   322 class cancel_ab_semigroup_add = ab_semigroup_add + minus +
   323   assumes add_diff_cancel_left' [simp]: "(a + b) - a = b"
   324   assumes diff_diff_add [algebra_simps, field_simps]: "a - b - c = a - (b + c)"
   325 begin
   326 
   327 lemma add_diff_cancel_right' [simp]: "(a + b) - b = a"
   328   using add_diff_cancel_left' [of b a] by (simp add: ac_simps)
   329 
   330 subclass cancel_semigroup_add
   331 proof
   332   fix a b c :: 'a
   333   assume "a + b = a + c"
   334   then have "a + b - a = a + c - a"
   335     by simp
   336   then show "b = c"
   337     by simp
   338 next
   339   fix a b c :: 'a
   340   assume "b + a = c + a"
   341   then have "b + a - a = c + a - a"
   342     by simp
   343   then show "b = c"
   344     by simp
   345 qed
   346 
   347 lemma add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b"
   348   unfolding diff_diff_add [symmetric] by simp
   349 
   350 lemma add_diff_cancel_right [simp]: "(a + c) - (b + c) = a - b"
   351   using add_diff_cancel_left [symmetric] by (simp add: ac_simps)
   352 
   353 lemma diff_right_commute: "a - c - b = a - b - c"
   354   by (simp add: diff_diff_add add.commute)
   355 
   356 end
   357 
   358 class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add
   359 begin
   360 
   361 lemma diff_zero [simp]: "a - 0 = a"
   362   using add_diff_cancel_right' [of a 0] by simp
   363 
   364 lemma diff_cancel [simp]: "a - a = 0"
   365 proof -
   366   have "(a + 0) - (a + 0) = 0"
   367     by (simp only: add_diff_cancel_left diff_zero)
   368   then show ?thesis by simp
   369 qed
   370 
   371 lemma add_implies_diff:
   372   assumes "c + b = a"
   373   shows "c = a - b"
   374 proof -
   375   from assms have "(b + c) - (b + 0) = a - b"
   376     by (simp add: add.commute)
   377   then show "c = a - b" by simp
   378 qed
   379 
   380 lemma add_cancel_right_right [simp]: "a = a + b \<longleftrightarrow> b = 0"
   381   (is "?P \<longleftrightarrow> ?Q")
   382 proof
   383   assume ?Q
   384   then show ?P by simp
   385 next
   386   assume ?P
   387   then have "a - a = a + b - a" by simp
   388   then show ?Q by simp
   389 qed
   390 
   391 lemma add_cancel_right_left [simp]: "a = b + a \<longleftrightarrow> b = 0"
   392   using add_cancel_right_right [of a b] by (simp add: ac_simps)
   393 
   394 lemma add_cancel_left_right [simp]: "a + b = a \<longleftrightarrow> b = 0"
   395   by (auto dest: sym)
   396 
   397 lemma add_cancel_left_left [simp]: "b + a = a \<longleftrightarrow> b = 0"
   398   by (auto dest: sym)
   399 
   400 end
   401 
   402 class comm_monoid_diff = cancel_comm_monoid_add +
   403   assumes zero_diff [simp]: "0 - a = 0"
   404 begin
   405 
   406 lemma diff_add_zero [simp]: "a - (a + b) = 0"
   407 proof -
   408   have "a - (a + b) = (a + 0) - (a + b)"
   409     by simp
   410   also have "\<dots> = 0"
   411     by (simp only: add_diff_cancel_left zero_diff)
   412   finally show ?thesis .
   413 qed
   414 
   415 end
   416 
   417 
   418 subsection \<open>Groups\<close>
   419 
   420 class group_add = minus + uminus + monoid_add +
   421   assumes left_minus: "- a + a = 0"
   422   assumes add_uminus_conv_diff [simp]: "a + (- b) = a - b"
   423 begin
   424 
   425 lemma diff_conv_add_uminus: "a - b = a + (- b)"
   426   by simp
   427 
   428 sublocale add: group plus 0 uminus
   429   by standard (simp_all add: left_minus)
   430 
   431 lemma minus_unique: "a + b = 0 \<Longrightarrow> - a = b"
   432   by (fact add.inverse_unique)
   433 
   434 lemma minus_zero: "- 0 = 0"
   435   by (fact add.inverse_neutral)
   436 
   437 lemma minus_minus: "- (- a) = a"
   438   by (fact add.inverse_inverse)
   439 
   440 lemma right_minus: "a + - a = 0"
   441   by (fact add.right_inverse)
   442 
   443 lemma diff_self [simp]: "a - a = 0"
   444   using right_minus [of a] by simp
   445 
   446 subclass cancel_semigroup_add
   447   by standard (simp_all add: add.left_cancel add.right_cancel)
   448 
   449 lemma minus_add_cancel [simp]: "- a + (a + b) = b"
   450   by (simp add: add.assoc [symmetric])
   451 
   452 lemma add_minus_cancel [simp]: "a + (- a + b) = b"
   453   by (simp add: add.assoc [symmetric])
   454 
   455 lemma diff_add_cancel [simp]: "a - b + b = a"
   456   by (simp only: diff_conv_add_uminus add.assoc) simp
   457 
   458 lemma add_diff_cancel [simp]: "a + b - b = a"
   459   by (simp only: diff_conv_add_uminus add.assoc) simp
   460 
   461 lemma minus_add: "- (a + b) = - b + - a"
   462   by (fact add.inverse_distrib_swap)
   463 
   464 lemma right_minus_eq [simp]: "a - b = 0 \<longleftrightarrow> a = b"
   465 proof
   466   assume "a - b = 0"
   467   have "a = (a - b) + b" by (simp add: add.assoc)
   468   also have "\<dots> = b" using \<open>a - b = 0\<close> by simp
   469   finally show "a = b" .
   470 next
   471   assume "a = b"
   472   then show "a - b = 0" by simp
   473 qed
   474 
   475 lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
   476   by (fact right_minus_eq [symmetric])
   477 
   478 lemma diff_0 [simp]: "0 - a = - a"
   479   by (simp only: diff_conv_add_uminus add_0_left)
   480 
   481 lemma diff_0_right [simp]: "a - 0 = a"
   482   by (simp only: diff_conv_add_uminus minus_zero add_0_right)
   483 
   484 lemma diff_minus_eq_add [simp]: "a - - b = a + b"
   485   by (simp only: diff_conv_add_uminus minus_minus)
   486 
   487 lemma neg_equal_iff_equal [simp]: "- a = - b \<longleftrightarrow> a = b"
   488 proof
   489   assume "- a = - b"
   490   then have "- (- a) = - (- b)" by simp
   491   then show "a = b" by simp
   492 next
   493   assume "a = b"
   494   then show "- a = - b" by simp
   495 qed
   496 
   497 lemma neg_equal_0_iff_equal [simp]: "- a = 0 \<longleftrightarrow> a = 0"
   498   by (subst neg_equal_iff_equal [symmetric]) simp
   499 
   500 lemma neg_0_equal_iff_equal [simp]: "0 = - a \<longleftrightarrow> 0 = a"
   501   by (subst neg_equal_iff_equal [symmetric]) simp
   502 
   503 text \<open>The next two equations can make the simplifier loop!\<close>
   504 
   505 lemma equation_minus_iff: "a = - b \<longleftrightarrow> b = - a"
   506 proof -
   507   have "- (- a) = - b \<longleftrightarrow> - a = b"
   508     by (rule neg_equal_iff_equal)
   509   then show ?thesis
   510     by (simp add: eq_commute)
   511 qed
   512 
   513 lemma minus_equation_iff: "- a = b \<longleftrightarrow> - b = a"
   514 proof -
   515   have "- a = - (- b) \<longleftrightarrow> a = -b"
   516     by (rule neg_equal_iff_equal)
   517   then show ?thesis
   518     by (simp add: eq_commute)
   519 qed
   520 
   521 lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0"
   522 proof
   523   assume "a = - b"
   524   then show "a + b = 0" by simp
   525 next
   526   assume "a + b = 0"
   527   moreover have "a + (b + - b) = (a + b) + - b"
   528     by (simp only: add.assoc)
   529   ultimately show "a = - b"
   530     by simp
   531 qed
   532 
   533 lemma add_eq_0_iff2: "a + b = 0 \<longleftrightarrow> a = - b"
   534   by (fact eq_neg_iff_add_eq_0 [symmetric])
   535 
   536 lemma neg_eq_iff_add_eq_0: "- a = b \<longleftrightarrow> a + b = 0"
   537   by (auto simp add: add_eq_0_iff2)
   538 
   539 lemma add_eq_0_iff: "a + b = 0 \<longleftrightarrow> b = - a"
   540   by (auto simp add: neg_eq_iff_add_eq_0 [symmetric])
   541 
   542 lemma minus_diff_eq [simp]: "- (a - b) = b - a"
   543   by (simp only: neg_eq_iff_add_eq_0 diff_conv_add_uminus add.assoc minus_add_cancel) simp
   544 
   545 lemma add_diff_eq [algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
   546   by (simp only: diff_conv_add_uminus add.assoc)
   547 
   548 lemma diff_add_eq_diff_diff_swap: "a - (b + c) = a - c - b"
   549   by (simp only: diff_conv_add_uminus add.assoc minus_add)
   550 
   551 lemma diff_eq_eq [algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
   552   by auto
   553 
   554 lemma eq_diff_eq [algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
   555   by auto
   556 
   557 lemma diff_diff_eq2 [algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"
   558   by (simp only: diff_conv_add_uminus add.assoc) simp
   559 
   560 lemma diff_eq_diff_eq: "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
   561   by (simp only: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])
   562 
   563 end
   564 
   565 class ab_group_add = minus + uminus + comm_monoid_add +
   566   assumes ab_left_minus: "- a + a = 0"
   567   assumes ab_diff_conv_add_uminus: "a - b = a + (- b)"
   568 begin
   569 
   570 subclass group_add
   571   by standard (simp_all add: ab_left_minus ab_diff_conv_add_uminus)
   572 
   573 subclass cancel_comm_monoid_add
   574 proof
   575   fix a b c :: 'a
   576   have "b + a - a = b"
   577     by simp
   578   then show "a + b - a = b"
   579     by (simp add: ac_simps)
   580   show "a - b - c = a - (b + c)"
   581     by (simp add: algebra_simps)
   582 qed
   583 
   584 lemma uminus_add_conv_diff [simp]: "- a + b = b - a"
   585   by (simp add: add.commute)
   586 
   587 lemma minus_add_distrib [simp]: "- (a + b) = - a + - b"
   588   by (simp add: algebra_simps)
   589 
   590 lemma diff_add_eq [algebra_simps, field_simps]: "(a - b) + c = (a + c) - b"
   591   by (simp add: algebra_simps)
   592 
   593 end
   594 
   595 
   596 subsection \<open>(Partially) Ordered Groups\<close>
   597 
   598 text \<open>
   599   The theory of partially ordered groups is taken from the books:
   600 
   601     \<^item> \<^emph>\<open>Lattice Theory\<close> by Garret Birkhoff, American Mathematical Society, 1979
   602     \<^item> \<^emph>\<open>Partially Ordered Algebraic Systems\<close>, Pergamon Press, 1963
   603 
   604   Most of the used notions can also be looked up in
   605     \<^item> @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
   606     \<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer
   607 \<close>
   608 
   609 class ordered_ab_semigroup_add = order + ab_semigroup_add +
   610   assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
   611 begin
   612 
   613 lemma add_right_mono: "a \<le> b \<Longrightarrow> a + c \<le> b + c"
   614   by (simp add: add.commute [of _ c] add_left_mono)
   615 
   616 text \<open>non-strict, in both arguments\<close>
   617 lemma add_mono: "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
   618   apply (erule add_right_mono [THEN order_trans])
   619   apply (simp add: add.commute add_left_mono)
   620   done
   621 
   622 end
   623 
   624 text \<open>Strict monotonicity in both arguments\<close>
   625 class strict_ordered_ab_semigroup_add = ordered_ab_semigroup_add +
   626   assumes add_strict_mono: "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   627 
   628 class ordered_cancel_ab_semigroup_add =
   629   ordered_ab_semigroup_add + cancel_ab_semigroup_add
   630 begin
   631 
   632 lemma add_strict_left_mono: "a < b \<Longrightarrow> c + a < c + b"
   633   by (auto simp add: less_le add_left_mono)
   634 
   635 lemma add_strict_right_mono: "a < b \<Longrightarrow> a + c < b + c"
   636   by (simp add: add.commute [of _ c] add_strict_left_mono)
   637 
   638 subclass strict_ordered_ab_semigroup_add
   639   apply standard
   640   apply (erule add_strict_right_mono [THEN less_trans])
   641   apply (erule add_strict_left_mono)
   642   done
   643 
   644 lemma add_less_le_mono: "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
   645   apply (erule add_strict_right_mono [THEN less_le_trans])
   646   apply (erule add_left_mono)
   647   done
   648 
   649 lemma add_le_less_mono: "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   650   apply (erule add_right_mono [THEN le_less_trans])
   651   apply (erule add_strict_left_mono)
   652   done
   653 
   654 end
   655 
   656 class ordered_ab_semigroup_add_imp_le = ordered_cancel_ab_semigroup_add +
   657   assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
   658 begin
   659 
   660 lemma add_less_imp_less_left:
   661   assumes less: "c + a < c + b"
   662   shows "a < b"
   663 proof -
   664   from less have le: "c + a \<le> c + b"
   665     by (simp add: order_le_less)
   666   have "a \<le> b"
   667     apply (insert le)
   668     apply (drule add_le_imp_le_left)
   669     apply (insert le)
   670     apply (drule add_le_imp_le_left)
   671     apply assumption
   672     done
   673   moreover have "a \<noteq> b"
   674   proof (rule ccontr)
   675     assume "\<not> ?thesis"
   676     then have "a = b" by simp
   677     then have "c + a = c + b" by simp
   678     with less show "False" by simp
   679   qed
   680   ultimately show "a < b"
   681     by (simp add: order_le_less)
   682 qed
   683 
   684 lemma add_less_imp_less_right: "a + c < b + c \<Longrightarrow> a < b"
   685   by (rule add_less_imp_less_left [of c]) (simp add: add.commute)
   686 
   687 lemma add_less_cancel_left [simp]: "c + a < c + b \<longleftrightarrow> a < b"
   688   by (blast intro: add_less_imp_less_left add_strict_left_mono)
   689 
   690 lemma add_less_cancel_right [simp]: "a + c < b + c \<longleftrightarrow> a < b"
   691   by (blast intro: add_less_imp_less_right add_strict_right_mono)
   692 
   693 lemma add_le_cancel_left [simp]: "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
   694   apply auto
   695    apply (drule add_le_imp_le_left)
   696    apply (simp_all add: add_left_mono)
   697   done
   698 
   699 lemma add_le_cancel_right [simp]: "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
   700   by (simp add: add.commute [of a c] add.commute [of b c])
   701 
   702 lemma add_le_imp_le_right: "a + c \<le> b + c \<Longrightarrow> a \<le> b"
   703   by simp
   704 
   705 lemma max_add_distrib_left: "max x y + z = max (x + z) (y + z)"
   706   unfolding max_def by auto
   707 
   708 lemma min_add_distrib_left: "min x y + z = min (x + z) (y + z)"
   709   unfolding min_def by auto
   710 
   711 lemma max_add_distrib_right: "x + max y z = max (x + y) (x + z)"
   712   unfolding max_def by auto
   713 
   714 lemma min_add_distrib_right: "x + min y z = min (x + y) (x + z)"
   715   unfolding min_def by auto
   716 
   717 end
   718 
   719 subsection \<open>Support for reasoning about signs\<close>
   720 
   721 class ordered_comm_monoid_add = comm_monoid_add + ordered_ab_semigroup_add
   722 begin
   723 
   724 lemma add_nonneg_nonneg [simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
   725   using add_mono[of 0 a 0 b] by simp
   726 
   727 lemma add_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> a + b \<le> 0"
   728   using add_mono[of a 0 b 0] by simp
   729 
   730 lemma add_nonneg_eq_0_iff: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   731   using add_left_mono[of 0 y x] add_right_mono[of 0 x y] by auto
   732 
   733 lemma add_nonpos_eq_0_iff: "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
   734   using add_left_mono[of y 0 x] add_right_mono[of x 0 y] by auto
   735 
   736 lemma add_increasing: "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
   737   using add_mono [of 0 a b c] by simp
   738 
   739 lemma add_increasing2: "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
   740   by (simp add: add_increasing add.commute [of a])
   741 
   742 lemma add_decreasing: "a \<le> 0 \<Longrightarrow> c \<le> b \<Longrightarrow> a + c \<le> b"
   743   using add_mono [of a 0 c b] by simp
   744 
   745 lemma add_decreasing2: "c \<le> 0 \<Longrightarrow> a \<le> b \<Longrightarrow> a + c \<le> b"
   746   using add_mono[of a b c 0] by simp
   747 
   748 lemma add_pos_nonneg: "0 < a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < a + b"
   749   using less_le_trans[of 0 a "a + b"] by (simp add: add_increasing2)
   750 
   751 lemma add_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a + b"
   752   by (intro add_pos_nonneg less_imp_le)
   753 
   754 lemma add_nonneg_pos: "0 \<le> a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a + b"
   755   using add_pos_nonneg[of b a] by (simp add: add_commute)
   756 
   757 lemma add_neg_nonpos: "a < 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> a + b < 0"
   758   using le_less_trans[of "a + b" a 0] by (simp add: add_decreasing2)
   759 
   760 lemma add_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> a + b < 0"
   761   by (intro add_neg_nonpos less_imp_le)
   762 
   763 lemma add_nonpos_neg: "a \<le> 0 \<Longrightarrow> b < 0 \<Longrightarrow> a + b < 0"
   764   using add_neg_nonpos[of b a] by (simp add: add_commute)
   765 
   766 lemmas add_sign_intros =
   767   add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg
   768   add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos
   769 
   770 end
   771 
   772 class strict_ordered_comm_monoid_add = comm_monoid_add + strict_ordered_ab_semigroup_add
   773 begin
   774 
   775 lemma pos_add_strict: "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   776   using add_strict_mono [of 0 a b c] by simp
   777 
   778 end
   779 
   780 class ordered_cancel_comm_monoid_add = ordered_comm_monoid_add + cancel_ab_semigroup_add
   781 begin
   782 
   783 subclass ordered_cancel_ab_semigroup_add ..
   784 subclass strict_ordered_comm_monoid_add ..
   785 
   786 lemma add_strict_increasing: "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
   787   using add_less_le_mono [of 0 a b c] by simp
   788 
   789 lemma add_strict_increasing2: "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
   790   using add_le_less_mono [of 0 a b c] by simp
   791 
   792 end
   793 
   794 class ordered_ab_semigroup_monoid_add_imp_le = monoid_add + ordered_ab_semigroup_add_imp_le
   795 begin
   796 
   797 lemma add_less_same_cancel1 [simp]: "b + a < b \<longleftrightarrow> a < 0"
   798   using add_less_cancel_left [of _ _ 0] by simp
   799 
   800 lemma add_less_same_cancel2 [simp]: "a + b < b \<longleftrightarrow> a < 0"
   801   using add_less_cancel_right [of _ _ 0] by simp
   802 
   803 lemma less_add_same_cancel1 [simp]: "a < a + b \<longleftrightarrow> 0 < b"
   804   using add_less_cancel_left [of _ 0] by simp
   805 
   806 lemma less_add_same_cancel2 [simp]: "a < b + a \<longleftrightarrow> 0 < b"
   807   using add_less_cancel_right [of 0] by simp
   808 
   809 lemma add_le_same_cancel1 [simp]: "b + a \<le> b \<longleftrightarrow> a \<le> 0"
   810   using add_le_cancel_left [of _ _ 0] by simp
   811 
   812 lemma add_le_same_cancel2 [simp]: "a + b \<le> b \<longleftrightarrow> a \<le> 0"
   813   using add_le_cancel_right [of _ _ 0] by simp
   814 
   815 lemma le_add_same_cancel1 [simp]: "a \<le> a + b \<longleftrightarrow> 0 \<le> b"
   816   using add_le_cancel_left [of _ 0] by simp
   817 
   818 lemma le_add_same_cancel2 [simp]: "a \<le> b + a \<longleftrightarrow> 0 \<le> b"
   819   using add_le_cancel_right [of 0] by simp
   820 
   821 subclass cancel_comm_monoid_add
   822   by standard auto
   823 
   824 subclass ordered_cancel_comm_monoid_add
   825   by standard
   826 
   827 end
   828 
   829 class ordered_ab_group_add = ab_group_add + ordered_ab_semigroup_add
   830 begin
   831 
   832 subclass ordered_cancel_ab_semigroup_add ..
   833 
   834 subclass ordered_ab_semigroup_monoid_add_imp_le
   835 proof
   836   fix a b c :: 'a
   837   assume "c + a \<le> c + b"
   838   then have "(-c) + (c + a) \<le> (-c) + (c + b)"
   839     by (rule add_left_mono)
   840   then have "((-c) + c) + a \<le> ((-c) + c) + b"
   841     by (simp only: add.assoc)
   842   then show "a \<le> b" by simp
   843 qed
   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 "c + b \<le> c + a" by (rule add_left_mono)
  1026     with le1 have "a = b"
  1027       apply -
  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 :: 'a
  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