src/HOL/Groups.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (19 months ago)
changeset 67022 49309fe530fd
parent 64290 fb5c74a58796
child 69216 1a52baa70aed
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     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>\<open>http://www.mathworld.com\<close> 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 ordered_ab_group_add_abs = ordered_ab_group_add + abs +
  1152   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
  1153     and abs_ge_self: "a \<le> \<bar>a\<bar>"
  1154     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
  1155     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
  1156     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1157 begin
  1158 
  1159 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
  1160   unfolding neg_le_0_iff_le by simp
  1161 
  1162 lemma abs_of_nonneg [simp]:
  1163   assumes nonneg: "0 \<le> a"
  1164   shows "\<bar>a\<bar> = a"
  1165 proof (rule antisym)
  1166   show "a \<le> \<bar>a\<bar>" by (rule abs_ge_self)
  1167   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
  1168   from this nonneg have "- a \<le> a" by (rule order_trans)
  1169   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
  1170 qed
  1171 
  1172 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
  1173   by (rule antisym) (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
  1174 
  1175 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
  1176 proof -
  1177   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
  1178   proof (rule antisym)
  1179     assume zero: "\<bar>a\<bar> = 0"
  1180     with abs_ge_self show "a \<le> 0" by auto
  1181     from zero have "\<bar>-a\<bar> = 0" by simp
  1182     with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
  1183     with neg_le_0_iff_le show "0 \<le> a" by auto
  1184   qed
  1185   then show ?thesis by auto
  1186 qed
  1187 
  1188 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
  1189   by simp
  1190 
  1191 lemma abs_0_eq [simp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
  1192 proof -
  1193   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
  1194   then show ?thesis by simp
  1195 qed
  1196 
  1197 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"
  1198 proof
  1199   assume "\<bar>a\<bar> \<le> 0"
  1200   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
  1201   then show "a = 0" by simp
  1202 next
  1203   assume "a = 0"
  1204   then show "\<bar>a\<bar> \<le> 0" by simp
  1205 qed
  1206 
  1207 lemma abs_le_self_iff [simp]: "\<bar>a\<bar> \<le> a \<longleftrightarrow> 0 \<le> a"
  1208 proof -
  1209   have "0 \<le> \<bar>a\<bar>"
  1210     using abs_ge_zero by blast
  1211   then have "\<bar>a\<bar> \<le> a \<Longrightarrow> 0 \<le> a"
  1212     using order.trans by blast
  1213   then show ?thesis
  1214     using abs_of_nonneg eq_refl by blast
  1215 qed
  1216 
  1217 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
  1218   by (simp add: less_le)
  1219 
  1220 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
  1221 proof -
  1222   have "x \<le> y \<Longrightarrow> \<not> y < x" for x y by auto
  1223   then show ?thesis by simp
  1224 qed
  1225 
  1226 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
  1227 proof -
  1228   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
  1229   then show ?thesis by simp
  1230 qed
  1231 
  1232 lemma abs_minus_commute: "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
  1233 proof -
  1234   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>"
  1235     by (simp only: abs_minus_cancel)
  1236   also have "\<dots> = \<bar>b - a\<bar>" by simp
  1237   finally show ?thesis .
  1238 qed
  1239 
  1240 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
  1241   by (rule abs_of_nonneg) (rule less_imp_le)
  1242 
  1243 lemma abs_of_nonpos [simp]:
  1244   assumes "a \<le> 0"
  1245   shows "\<bar>a\<bar> = - a"
  1246 proof -
  1247   let ?b = "- a"
  1248   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
  1249     unfolding abs_minus_cancel [of ?b]
  1250     unfolding neg_le_0_iff_le [of ?b]
  1251     unfolding minus_minus by (erule abs_of_nonneg)
  1252   then show ?thesis using assms by auto
  1253 qed
  1254 
  1255 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
  1256   by (rule abs_of_nonpos) (rule less_imp_le)
  1257 
  1258 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
  1259   using abs_ge_self by (blast intro: order_trans)
  1260 
  1261 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
  1262   using abs_le_D1 [of "- a"] by simp
  1263 
  1264 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
  1265   by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
  1266 
  1267 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
  1268 proof -
  1269   have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
  1270     by (simp add: algebra_simps)
  1271   then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
  1272     by (simp add: abs_triangle_ineq)
  1273   then show ?thesis
  1274     by (simp add: algebra_simps)
  1275 qed
  1276 
  1277 lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
  1278   by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
  1279 
  1280 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
  1281   by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
  1282 
  1283 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1284 proof -
  1285   have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>"
  1286     by (simp add: algebra_simps)
  1287   also have "\<dots> \<le> \<bar>a\<bar> + \<bar>- b\<bar>"
  1288     by (rule abs_triangle_ineq)
  1289   finally show ?thesis by simp
  1290 qed
  1291 
  1292 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
  1293 proof -
  1294   have "\<bar>a + b - (c + d)\<bar> = \<bar>(a - c) + (b - d)\<bar>"
  1295     by (simp add: algebra_simps)
  1296   also have "\<dots> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
  1297     by (rule abs_triangle_ineq)
  1298   finally show ?thesis .
  1299 qed
  1300 
  1301 lemma abs_add_abs [simp]: "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>"
  1302   (is "?L = ?R")
  1303 proof (rule antisym)
  1304   show "?L \<ge> ?R" by (rule abs_ge_self)
  1305   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by (rule abs_triangle_ineq)
  1306   also have "\<dots> = ?R" by simp
  1307   finally show "?L \<le> ?R" .
  1308 qed
  1309 
  1310 end
  1311 
  1312 lemma dense_eq0_I:
  1313   fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
  1314   shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) \<Longrightarrow> x = 0"
  1315   apply (cases "\<bar>x\<bar> = 0")
  1316    apply simp
  1317   apply (simp only: zero_less_abs_iff [symmetric])
  1318   apply (drule dense)
  1319   apply (auto simp add: not_less [symmetric])
  1320   done
  1321 
  1322 hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus
  1323 
  1324 lemmas add_0 = add_0_left (* FIXME duplicate *)
  1325 lemmas mult_1 = mult_1_left (* FIXME duplicate *)
  1326 lemmas ab_left_minus = left_minus (* FIXME duplicate *)
  1327 lemmas diff_diff_eq = diff_diff_add (* FIXME duplicate *)
  1328 
  1329 
  1330 subsection \<open>Canonically ordered monoids\<close>
  1331 
  1332 text \<open>Canonically ordered monoids are never groups.\<close>
  1333 
  1334 class canonically_ordered_monoid_add = comm_monoid_add + order +
  1335   assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
  1336 begin
  1337 
  1338 lemma zero_le[simp]: "0 \<le> x"
  1339   by (auto simp: le_iff_add)
  1340 
  1341 lemma le_zero_eq[simp]: "n \<le> 0 \<longleftrightarrow> n = 0"
  1342   by (auto intro: antisym)
  1343 
  1344 lemma not_less_zero[simp]: "\<not> n < 0"
  1345   by (auto simp: less_le)
  1346 
  1347 lemma zero_less_iff_neq_zero: "0 < n \<longleftrightarrow> n \<noteq> 0"
  1348   by (auto simp: less_le)
  1349 
  1350 text \<open>This theorem is useful with \<open>blast\<close>\<close>
  1351 lemma gr_zeroI: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n"
  1352   by (rule zero_less_iff_neq_zero[THEN iffD2]) iprover
  1353 
  1354 lemma not_gr_zero[simp]: "\<not> 0 < n \<longleftrightarrow> n = 0"
  1355   by (simp add: zero_less_iff_neq_zero)
  1356 
  1357 subclass ordered_comm_monoid_add
  1358   proof qed (auto simp: le_iff_add add_ac)
  1359 
  1360 lemma gr_implies_not_zero: "m < n \<Longrightarrow> n \<noteq> 0"
  1361   by auto
  1362 
  1363 lemma add_eq_0_iff_both_eq_0[simp]: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
  1364   by (intro add_nonneg_eq_0_iff zero_le)
  1365 
  1366 lemma zero_eq_add_iff_both_eq_0[simp]: "0 = x + y \<longleftrightarrow> x = 0 \<and> y = 0"
  1367   using add_eq_0_iff_both_eq_0[of x y] unfolding eq_commute[of 0] .
  1368 
  1369 lemmas zero_order = zero_le le_zero_eq not_less_zero zero_less_iff_neq_zero not_gr_zero
  1370   \<comment> \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close>
  1371 
  1372 end
  1373 
  1374 class ordered_cancel_comm_monoid_diff =
  1375   canonically_ordered_monoid_add + comm_monoid_diff + ordered_ab_semigroup_add_imp_le
  1376 begin
  1377 
  1378 context
  1379   fixes a b :: 'a
  1380   assumes le: "a \<le> b"
  1381 begin
  1382 
  1383 lemma add_diff_inverse: "a + (b - a) = b"
  1384   using le by (auto simp add: le_iff_add)
  1385 
  1386 lemma add_diff_assoc: "c + (b - a) = c + b - a"
  1387   using le by (auto simp add: le_iff_add add.left_commute [of c])
  1388 
  1389 lemma add_diff_assoc2: "b - a + c = b + c - a"
  1390   using le by (auto simp add: le_iff_add add.assoc)
  1391 
  1392 lemma diff_add_assoc: "c + b - a = c + (b - a)"
  1393   using le by (simp add: add.commute add_diff_assoc)
  1394 
  1395 lemma diff_add_assoc2: "b + c - a = b - a + c"
  1396   using le by (simp add: add.commute add_diff_assoc)
  1397 
  1398 lemma diff_diff_right: "c - (b - a) = c + a - b"
  1399   by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add.commute)
  1400 
  1401 lemma diff_add: "b - a + a = b"
  1402   by (simp add: add.commute add_diff_inverse)
  1403 
  1404 lemma le_add_diff: "c \<le> b + c - a"
  1405   by (auto simp add: add.commute diff_add_assoc2 le_iff_add)
  1406 
  1407 lemma le_imp_diff_is_add: "a \<le> b \<Longrightarrow> b - a = c \<longleftrightarrow> b = c + a"
  1408   by (auto simp add: add.commute add_diff_inverse)
  1409 
  1410 lemma le_diff_conv2: "c \<le> b - a \<longleftrightarrow> c + a \<le> b"
  1411   (is "?P \<longleftrightarrow> ?Q")
  1412 proof
  1413   assume ?P
  1414   then have "c + a \<le> b - a + a"
  1415     by (rule add_right_mono)
  1416   then show ?Q
  1417     by (simp add: add_diff_inverse add.commute)
  1418 next
  1419   assume ?Q
  1420   then have "a + c \<le> a + (b - a)"
  1421     by (simp add: add_diff_inverse add.commute)
  1422   then show ?P by simp
  1423 qed
  1424 
  1425 end
  1426 
  1427 end
  1428 
  1429 
  1430 subsection \<open>Tools setup\<close>
  1431 
  1432 lemma add_mono_thms_linordered_semiring:
  1433   fixes i j k :: "'a::ordered_ab_semigroup_add"
  1434   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1435     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1436     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
  1437     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
  1438   by (rule add_mono, clarify+)+
  1439 
  1440 lemma add_mono_thms_linordered_field:
  1441   fixes i j k :: "'a::ordered_cancel_ab_semigroup_add"
  1442   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
  1443     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
  1444     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
  1445     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
  1446     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
  1447   by (auto intro: add_strict_right_mono add_strict_left_mono
  1448       add_less_le_mono add_le_less_mono add_strict_mono)
  1449 
  1450 code_identifier
  1451   code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
  1452 
  1453 end