src/HOL/OrderedGroup.thy
author nipkow
Sun Feb 08 11:59:26 2009 +0100 (2009-02-08)
changeset 29833 409138c4de12
parent 29670 cbe35f4f04f8
child 29886 b8a6b9c56fdd
permissions -rw-r--r--
added noatps
     1 (*  Title:   HOL/OrderedGroup.thy
     2     Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, Markus Wenzel, Jeremy Avigad
     3 *)
     4 
     5 header {* Ordered Groups *}
     6 
     7 theory OrderedGroup
     8 imports Lattices
     9 uses "~~/src/Provers/Arith/abel_cancel.ML"
    10 begin
    11 
    12 text {*
    13   The theory of partially ordered groups is taken from the books:
    14   \begin{itemize}
    15   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
    16   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963
    17   \end{itemize}
    18   Most of the used notions can also be looked up in 
    19   \begin{itemize}
    20   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
    21   \item \emph{Algebra I} by van der Waerden, Springer.
    22   \end{itemize}
    23 *}
    24 
    25 ML{*
    26 structure AlgebraSimps =
    27   NamedThmsFun(val name = "algebra_simps"
    28                val description = "algebra simplification rules");
    29 *}
    30 
    31 setup AlgebraSimps.setup
    32 
    33 text{* The rewrites accumulated in @{text algebra_simps} deal with the
    34 classical algebraic structures of groups, rings and family. They simplify
    35 terms by multiplying everything out (in case of a ring) and bringing sums and
    36 products into a canonical form (by ordered rewriting). As a result it decides
    37 group and ring equalities but also helps with inequalities.
    38 
    39 Of course it also works for fields, but it knows nothing about multiplicative
    40 inverses or division. This is catered for by @{text field_simps}. *}
    41 
    42 subsection {* Semigroups and Monoids *}
    43 
    44 class semigroup_add = plus +
    45   assumes add_assoc[algebra_simps]: "(a + b) + c = a + (b + c)"
    46 
    47 class ab_semigroup_add = semigroup_add +
    48   assumes add_commute[algebra_simps]: "a + b = b + a"
    49 begin
    50 
    51 lemma add_left_commute[algebra_simps]: "a + (b + c) = b + (a + c)"
    52 by (rule mk_left_commute [of "plus", OF add_assoc add_commute])
    53 
    54 theorems add_ac = add_assoc add_commute add_left_commute
    55 
    56 end
    57 
    58 theorems add_ac = add_assoc add_commute add_left_commute
    59 
    60 class semigroup_mult = times +
    61   assumes mult_assoc[algebra_simps]: "(a * b) * c = a * (b * c)"
    62 
    63 class ab_semigroup_mult = semigroup_mult +
    64   assumes mult_commute[algebra_simps]: "a * b = b * a"
    65 begin
    66 
    67 lemma mult_left_commute[algebra_simps]: "a * (b * c) = b * (a * c)"
    68 by (rule mk_left_commute [of "times", OF mult_assoc mult_commute])
    69 
    70 theorems mult_ac = mult_assoc mult_commute mult_left_commute
    71 
    72 end
    73 
    74 theorems mult_ac = mult_assoc mult_commute mult_left_commute
    75 
    76 class ab_semigroup_idem_mult = ab_semigroup_mult +
    77   assumes mult_idem[simp]: "x * x = x"
    78 begin
    79 
    80 lemma mult_left_idem[simp]: "x * (x * y) = x * y"
    81   unfolding mult_assoc [symmetric, of x] mult_idem ..
    82 
    83 end
    84 
    85 class monoid_add = zero + semigroup_add +
    86   assumes add_0_left [simp]: "0 + a = a"
    87     and add_0_right [simp]: "a + 0 = a"
    88 
    89 lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
    90 by (rule eq_commute)
    91 
    92 class comm_monoid_add = zero + ab_semigroup_add +
    93   assumes add_0: "0 + a = a"
    94 begin
    95 
    96 subclass monoid_add
    97   proof qed (insert add_0, simp_all add: add_commute)
    98 
    99 end
   100 
   101 class monoid_mult = one + semigroup_mult +
   102   assumes mult_1_left [simp]: "1 * a  = a"
   103   assumes mult_1_right [simp]: "a * 1 = a"
   104 
   105 lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
   106 by (rule eq_commute)
   107 
   108 class comm_monoid_mult = one + ab_semigroup_mult +
   109   assumes mult_1: "1 * a = a"
   110 begin
   111 
   112 subclass monoid_mult
   113   proof qed (insert mult_1, simp_all add: mult_commute)
   114 
   115 end
   116 
   117 class cancel_semigroup_add = semigroup_add +
   118   assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
   119   assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
   120 begin
   121 
   122 lemma add_left_cancel [simp]:
   123   "a + b = a + c \<longleftrightarrow> b = c"
   124 by (blast dest: add_left_imp_eq)
   125 
   126 lemma add_right_cancel [simp]:
   127   "b + a = c + a \<longleftrightarrow> b = c"
   128 by (blast dest: add_right_imp_eq)
   129 
   130 end
   131 
   132 class cancel_ab_semigroup_add = ab_semigroup_add +
   133   assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
   134 begin
   135 
   136 subclass cancel_semigroup_add
   137 proof
   138   fix a b c :: 'a
   139   assume "a + b = a + c" 
   140   then show "b = c" by (rule add_imp_eq)
   141 next
   142   fix a b c :: 'a
   143   assume "b + a = c + a"
   144   then have "a + b = a + c" by (simp only: add_commute)
   145   then show "b = c" by (rule add_imp_eq)
   146 qed
   147 
   148 end
   149 
   150 subsection {* Groups *}
   151 
   152 class group_add = minus + uminus + monoid_add +
   153   assumes left_minus [simp]: "- a + a = 0"
   154   assumes diff_minus: "a - b = a + (- b)"
   155 begin
   156 
   157 lemma minus_add_cancel: "- a + (a + b) = b"
   158 by (simp add: add_assoc[symmetric])
   159 
   160 lemma minus_zero [simp]: "- 0 = 0"
   161 proof -
   162   have "- 0 = - 0 + (0 + 0)" by (simp only: add_0_right)
   163   also have "\<dots> = 0" by (rule minus_add_cancel)
   164   finally show ?thesis .
   165 qed
   166 
   167 lemma minus_minus [simp]: "- (- a) = a"
   168 proof -
   169   have "- (- a) = - (- a) + (- a + a)" by simp
   170   also have "\<dots> = a" by (rule minus_add_cancel)
   171   finally show ?thesis .
   172 qed
   173 
   174 lemma right_minus [simp]: "a + - a = 0"
   175 proof -
   176   have "a + - a = - (- a) + - a" by simp
   177   also have "\<dots> = 0" by (rule left_minus)
   178   finally show ?thesis .
   179 qed
   180 
   181 lemma right_minus_eq: "a - b = 0 \<longleftrightarrow> a = b"
   182 proof
   183   assume "a - b = 0"
   184   have "a = (a - b) + b" by (simp add:diff_minus add_assoc)
   185   also have "\<dots> = b" using `a - b = 0` by simp
   186   finally show "a = b" .
   187 next
   188   assume "a = b" thus "a - b = 0" by (simp add: diff_minus)
   189 qed
   190 
   191 lemma equals_zero_I:
   192   assumes "a + b = 0" shows "- a = b"
   193 proof -
   194   have "- a = - a + (a + b)" using assms by simp
   195   also have "\<dots> = b" by (simp add: add_assoc[symmetric])
   196   finally show ?thesis .
   197 qed
   198 
   199 lemma diff_self [simp]: "a - a = 0"
   200 by (simp add: diff_minus)
   201 
   202 lemma diff_0 [simp]: "0 - a = - a"
   203 by (simp add: diff_minus)
   204 
   205 lemma diff_0_right [simp]: "a - 0 = a" 
   206 by (simp add: diff_minus)
   207 
   208 lemma diff_minus_eq_add [simp]: "a - - b = a + b"
   209 by (simp add: diff_minus)
   210 
   211 lemma neg_equal_iff_equal [simp]:
   212   "- a = - b \<longleftrightarrow> a = b" 
   213 proof 
   214   assume "- a = - b"
   215   hence "- (- a) = - (- b)" by simp
   216   thus "a = b" by simp
   217 next
   218   assume "a = b"
   219   thus "- a = - b" by simp
   220 qed
   221 
   222 lemma neg_equal_0_iff_equal [simp]:
   223   "- a = 0 \<longleftrightarrow> a = 0"
   224 by (subst neg_equal_iff_equal [symmetric], simp)
   225 
   226 lemma neg_0_equal_iff_equal [simp]:
   227   "0 = - a \<longleftrightarrow> 0 = a"
   228 by (subst neg_equal_iff_equal [symmetric], simp)
   229 
   230 text{*The next two equations can make the simplifier loop!*}
   231 
   232 lemma equation_minus_iff:
   233   "a = - b \<longleftrightarrow> b = - a"
   234 proof -
   235   have "- (- a) = - b \<longleftrightarrow> - a = b" by (rule neg_equal_iff_equal)
   236   thus ?thesis by (simp add: eq_commute)
   237 qed
   238 
   239 lemma minus_equation_iff:
   240   "- a = b \<longleftrightarrow> - b = a"
   241 proof -
   242   have "- a = - (- b) \<longleftrightarrow> a = -b" by (rule neg_equal_iff_equal)
   243   thus ?thesis by (simp add: eq_commute)
   244 qed
   245 
   246 lemma diff_add_cancel: "a - b + b = a"
   247 by (simp add: diff_minus add_assoc)
   248 
   249 lemma add_diff_cancel: "a + b - b = a"
   250 by (simp add: diff_minus add_assoc)
   251 
   252 declare diff_minus[symmetric, algebra_simps]
   253 
   254 end
   255 
   256 class ab_group_add = minus + uminus + comm_monoid_add +
   257   assumes ab_left_minus: "- a + a = 0"
   258   assumes ab_diff_minus: "a - b = a + (- b)"
   259 begin
   260 
   261 subclass group_add
   262   proof qed (simp_all add: ab_left_minus ab_diff_minus)
   263 
   264 subclass cancel_ab_semigroup_add
   265 proof
   266   fix a b c :: 'a
   267   assume "a + b = a + c"
   268   then have "- a + a + b = - a + a + c"
   269     unfolding add_assoc by simp
   270   then show "b = c" by simp
   271 qed
   272 
   273 lemma uminus_add_conv_diff[algebra_simps]:
   274   "- a + b = b - a"
   275 by (simp add:diff_minus add_commute)
   276 
   277 lemma minus_add_distrib [simp]:
   278   "- (a + b) = - a + - b"
   279 by (rule equals_zero_I) (simp add: add_ac)
   280 
   281 lemma minus_diff_eq [simp]:
   282   "- (a - b) = b - a"
   283 by (simp add: diff_minus add_commute)
   284 
   285 lemma add_diff_eq[algebra_simps]: "a + (b - c) = (a + b) - c"
   286 by (simp add: diff_minus add_ac)
   287 
   288 lemma diff_add_eq[algebra_simps]: "(a - b) + c = (a + c) - b"
   289 by (simp add: diff_minus add_ac)
   290 
   291 lemma diff_eq_eq[algebra_simps]: "a - b = c \<longleftrightarrow> a = c + b"
   292 by (auto simp add: diff_minus add_assoc)
   293 
   294 lemma eq_diff_eq[algebra_simps]: "a = c - b \<longleftrightarrow> a + b = c"
   295 by (auto simp add: diff_minus add_assoc)
   296 
   297 lemma diff_diff_eq[algebra_simps]: "(a - b) - c = a - (b + c)"
   298 by (simp add: diff_minus add_ac)
   299 
   300 lemma diff_diff_eq2[algebra_simps]: "a - (b - c) = (a + c) - b"
   301 by (simp add: diff_minus add_ac)
   302 
   303 lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
   304 by (simp add: algebra_simps)
   305 
   306 end
   307 
   308 subsection {* (Partially) Ordered Groups *} 
   309 
   310 class pordered_ab_semigroup_add = order + ab_semigroup_add +
   311   assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
   312 begin
   313 
   314 lemma add_right_mono:
   315   "a \<le> b \<Longrightarrow> a + c \<le> b + c"
   316 by (simp add: add_commute [of _ c] add_left_mono)
   317 
   318 text {* non-strict, in both arguments *}
   319 lemma add_mono:
   320   "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d"
   321   apply (erule add_right_mono [THEN order_trans])
   322   apply (simp add: add_commute add_left_mono)
   323   done
   324 
   325 end
   326 
   327 class pordered_cancel_ab_semigroup_add =
   328   pordered_ab_semigroup_add + cancel_ab_semigroup_add
   329 begin
   330 
   331 lemma add_strict_left_mono:
   332   "a < b \<Longrightarrow> c + a < c + b"
   333 by (auto simp add: less_le add_left_mono)
   334 
   335 lemma add_strict_right_mono:
   336   "a < b \<Longrightarrow> a + c < b + c"
   337 by (simp add: add_commute [of _ c] add_strict_left_mono)
   338 
   339 text{*Strict monotonicity in both arguments*}
   340 lemma add_strict_mono:
   341   "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   342 apply (erule add_strict_right_mono [THEN less_trans])
   343 apply (erule add_strict_left_mono)
   344 done
   345 
   346 lemma add_less_le_mono:
   347   "a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d"
   348 apply (erule add_strict_right_mono [THEN less_le_trans])
   349 apply (erule add_left_mono)
   350 done
   351 
   352 lemma add_le_less_mono:
   353   "a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
   354 apply (erule add_right_mono [THEN le_less_trans])
   355 apply (erule add_strict_left_mono) 
   356 done
   357 
   358 end
   359 
   360 class pordered_ab_semigroup_add_imp_le =
   361   pordered_cancel_ab_semigroup_add +
   362   assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
   363 begin
   364 
   365 lemma add_less_imp_less_left:
   366   assumes less: "c + a < c + b" shows "a < b"
   367 proof -
   368   from less have le: "c + a <= c + b" by (simp add: order_le_less)
   369   have "a <= b" 
   370     apply (insert le)
   371     apply (drule add_le_imp_le_left)
   372     by (insert le, drule add_le_imp_le_left, assumption)
   373   moreover have "a \<noteq> b"
   374   proof (rule ccontr)
   375     assume "~(a \<noteq> b)"
   376     then have "a = b" by simp
   377     then have "c + a = c + b" by simp
   378     with less show "False"by simp
   379   qed
   380   ultimately show "a < b" by (simp add: order_le_less)
   381 qed
   382 
   383 lemma add_less_imp_less_right:
   384   "a + c < b + c \<Longrightarrow> a < b"
   385 apply (rule add_less_imp_less_left [of c])
   386 apply (simp add: add_commute)  
   387 done
   388 
   389 lemma add_less_cancel_left [simp]:
   390   "c + a < c + b \<longleftrightarrow> a < b"
   391 by (blast intro: add_less_imp_less_left add_strict_left_mono) 
   392 
   393 lemma add_less_cancel_right [simp]:
   394   "a + c < b + c \<longleftrightarrow> a < b"
   395 by (blast intro: add_less_imp_less_right add_strict_right_mono)
   396 
   397 lemma add_le_cancel_left [simp]:
   398   "c + a \<le> c + b \<longleftrightarrow> a \<le> b"
   399 by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
   400 
   401 lemma add_le_cancel_right [simp]:
   402   "a + c \<le> b + c \<longleftrightarrow> a \<le> b"
   403 by (simp add: add_commute [of a c] add_commute [of b c])
   404 
   405 lemma add_le_imp_le_right:
   406   "a + c \<le> b + c \<Longrightarrow> a \<le> b"
   407 by simp
   408 
   409 lemma max_add_distrib_left:
   410   "max x y + z = max (x + z) (y + z)"
   411   unfolding max_def by auto
   412 
   413 lemma min_add_distrib_left:
   414   "min x y + z = min (x + z) (y + z)"
   415   unfolding min_def by auto
   416 
   417 end
   418 
   419 subsection {* Support for reasoning about signs *}
   420 
   421 class pordered_comm_monoid_add =
   422   pordered_cancel_ab_semigroup_add + comm_monoid_add
   423 begin
   424 
   425 lemma add_pos_nonneg:
   426   assumes "0 < a" and "0 \<le> b" shows "0 < a + b"
   427 proof -
   428   have "0 + 0 < a + b" 
   429     using assms by (rule add_less_le_mono)
   430   then show ?thesis by simp
   431 qed
   432 
   433 lemma add_pos_pos:
   434   assumes "0 < a" and "0 < b" shows "0 < a + b"
   435 by (rule add_pos_nonneg) (insert assms, auto)
   436 
   437 lemma add_nonneg_pos:
   438   assumes "0 \<le> a" and "0 < b" shows "0 < a + b"
   439 proof -
   440   have "0 + 0 < a + b" 
   441     using assms by (rule add_le_less_mono)
   442   then show ?thesis by simp
   443 qed
   444 
   445 lemma add_nonneg_nonneg:
   446   assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
   447 proof -
   448   have "0 + 0 \<le> a + b" 
   449     using assms by (rule add_mono)
   450   then show ?thesis by simp
   451 qed
   452 
   453 lemma add_neg_nonpos: 
   454   assumes "a < 0" and "b \<le> 0" shows "a + b < 0"
   455 proof -
   456   have "a + b < 0 + 0"
   457     using assms by (rule add_less_le_mono)
   458   then show ?thesis by simp
   459 qed
   460 
   461 lemma add_neg_neg: 
   462   assumes "a < 0" and "b < 0" shows "a + b < 0"
   463 by (rule add_neg_nonpos) (insert assms, auto)
   464 
   465 lemma add_nonpos_neg:
   466   assumes "a \<le> 0" and "b < 0" shows "a + b < 0"
   467 proof -
   468   have "a + b < 0 + 0"
   469     using assms by (rule add_le_less_mono)
   470   then show ?thesis by simp
   471 qed
   472 
   473 lemma add_nonpos_nonpos:
   474   assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
   475 proof -
   476   have "a + b \<le> 0 + 0"
   477     using assms by (rule add_mono)
   478   then show ?thesis by simp
   479 qed
   480 
   481 end
   482 
   483 class pordered_ab_group_add =
   484   ab_group_add + pordered_ab_semigroup_add
   485 begin
   486 
   487 subclass pordered_cancel_ab_semigroup_add ..
   488 
   489 subclass pordered_ab_semigroup_add_imp_le
   490 proof
   491   fix a b c :: 'a
   492   assume "c + a \<le> c + b"
   493   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
   494   hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)
   495   thus "a \<le> b" by simp
   496 qed
   497 
   498 subclass pordered_comm_monoid_add ..
   499 
   500 lemma max_diff_distrib_left:
   501   shows "max x y - z = max (x - z) (y - z)"
   502 by (simp add: diff_minus, rule max_add_distrib_left) 
   503 
   504 lemma min_diff_distrib_left:
   505   shows "min x y - z = min (x - z) (y - z)"
   506 by (simp add: diff_minus, rule min_add_distrib_left) 
   507 
   508 lemma le_imp_neg_le:
   509   assumes "a \<le> b" shows "-b \<le> -a"
   510 proof -
   511   have "-a+a \<le> -a+b" using `a \<le> b` by (rule add_left_mono) 
   512   hence "0 \<le> -a+b" by simp
   513   hence "0 + (-b) \<le> (-a + b) + (-b)" by (rule add_right_mono) 
   514   thus ?thesis by (simp add: add_assoc)
   515 qed
   516 
   517 lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
   518 proof 
   519   assume "- b \<le> - a"
   520   hence "- (- a) \<le> - (- b)" by (rule le_imp_neg_le)
   521   thus "a\<le>b" by simp
   522 next
   523   assume "a\<le>b"
   524   thus "-b \<le> -a" by (rule le_imp_neg_le)
   525 qed
   526 
   527 lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
   528 by (subst neg_le_iff_le [symmetric], simp)
   529 
   530 lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
   531 by (subst neg_le_iff_le [symmetric], simp)
   532 
   533 lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
   534 by (force simp add: less_le) 
   535 
   536 lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
   537 by (subst neg_less_iff_less [symmetric], simp)
   538 
   539 lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
   540 by (subst neg_less_iff_less [symmetric], simp)
   541 
   542 text{*The next several equations can make the simplifier loop!*}
   543 
   544 lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
   545 proof -
   546   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
   547   thus ?thesis by simp
   548 qed
   549 
   550 lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
   551 proof -
   552   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
   553   thus ?thesis by simp
   554 qed
   555 
   556 lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
   557 proof -
   558   have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
   559   have "(- (- a) <= -b) = (b <= - a)" 
   560     apply (auto simp only: le_less)
   561     apply (drule mm)
   562     apply (simp_all)
   563     apply (drule mm[simplified], assumption)
   564     done
   565   then show ?thesis by simp
   566 qed
   567 
   568 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
   569 by (auto simp add: le_less minus_less_iff)
   570 
   571 lemma less_iff_diff_less_0: "a < b \<longleftrightarrow> a - b < 0"
   572 proof -
   573   have  "(a < b) = (a + (- b) < b + (-b))"  
   574     by (simp only: add_less_cancel_right)
   575   also have "... =  (a - b < 0)" by (simp add: diff_minus)
   576   finally show ?thesis .
   577 qed
   578 
   579 lemma diff_less_eq[algebra_simps]: "a - b < c \<longleftrightarrow> a < c + b"
   580 apply (subst less_iff_diff_less_0 [of a])
   581 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
   582 apply (simp add: diff_minus add_ac)
   583 done
   584 
   585 lemma less_diff_eq[algebra_simps]: "a < c - b \<longleftrightarrow> a + b < c"
   586 apply (subst less_iff_diff_less_0 [of "plus a b"])
   587 apply (subst less_iff_diff_less_0 [of a])
   588 apply (simp add: diff_minus add_ac)
   589 done
   590 
   591 lemma diff_le_eq[algebra_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
   592 by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel)
   593 
   594 lemma le_diff_eq[algebra_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
   595 by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
   596 
   597 lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"
   598 by (simp add: algebra_simps)
   599 
   600 text{*Legacy - use @{text algebra_simps} *}
   601 lemmas group_simps[noatp] = algebra_simps
   602 
   603 end
   604 
   605 text{*Legacy - use @{text algebra_simps} *}
   606 lemmas group_simps[noatp] = algebra_simps
   607 
   608 class ordered_ab_semigroup_add =
   609   linorder + pordered_ab_semigroup_add
   610 
   611 class ordered_cancel_ab_semigroup_add =
   612   linorder + pordered_cancel_ab_semigroup_add
   613 begin
   614 
   615 subclass ordered_ab_semigroup_add ..
   616 
   617 subclass pordered_ab_semigroup_add_imp_le
   618 proof
   619   fix a b c :: 'a
   620   assume le: "c + a <= c + b"  
   621   show "a <= b"
   622   proof (rule ccontr)
   623     assume w: "~ a \<le> b"
   624     hence "b <= a" by (simp add: linorder_not_le)
   625     hence le2: "c + b <= c + a" by (rule add_left_mono)
   626     have "a = b" 
   627       apply (insert le)
   628       apply (insert le2)
   629       apply (drule antisym, simp_all)
   630       done
   631     with w show False 
   632       by (simp add: linorder_not_le [symmetric])
   633   qed
   634 qed
   635 
   636 end
   637 
   638 class ordered_ab_group_add =
   639   linorder + pordered_ab_group_add
   640 begin
   641 
   642 subclass ordered_cancel_ab_semigroup_add ..
   643 
   644 lemma neg_less_eq_nonneg:
   645   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
   646 proof
   647   assume A: "- a \<le> a" show "0 \<le> a"
   648   proof (rule classical)
   649     assume "\<not> 0 \<le> a"
   650     then have "a < 0" by auto
   651     with A have "- a < 0" by (rule le_less_trans)
   652     then show ?thesis by auto
   653   qed
   654 next
   655   assume A: "0 \<le> a" show "- a \<le> a"
   656   proof (rule order_trans)
   657     show "- a \<le> 0" using A by (simp add: minus_le_iff)
   658   next
   659     show "0 \<le> a" using A .
   660   qed
   661 qed
   662   
   663 lemma less_eq_neg_nonpos:
   664   "a \<le> - a \<longleftrightarrow> a \<le> 0"
   665 proof
   666   assume A: "a \<le> - a" show "a \<le> 0"
   667   proof (rule classical)
   668     assume "\<not> a \<le> 0"
   669     then have "0 < a" by auto
   670     then have "0 < - a" using A by (rule less_le_trans)
   671     then show ?thesis by auto
   672   qed
   673 next
   674   assume A: "a \<le> 0" show "a \<le> - a"
   675   proof (rule order_trans)
   676     show "0 \<le> - a" using A by (simp add: minus_le_iff)
   677   next
   678     show "a \<le> 0" using A .
   679   qed
   680 qed
   681 
   682 lemma equal_neg_zero:
   683   "a = - a \<longleftrightarrow> a = 0"
   684 proof
   685   assume "a = 0" then show "a = - a" by simp
   686 next
   687   assume A: "a = - a" show "a = 0"
   688   proof (cases "0 \<le> a")
   689     case True with A have "0 \<le> - a" by auto
   690     with le_minus_iff have "a \<le> 0" by simp
   691     with True show ?thesis by (auto intro: order_trans)
   692   next
   693     case False then have B: "a \<le> 0" by auto
   694     with A have "- a \<le> 0" by auto
   695     with B show ?thesis by (auto intro: order_trans)
   696   qed
   697 qed
   698 
   699 lemma neg_equal_zero:
   700   "- a = a \<longleftrightarrow> a = 0"
   701   unfolding equal_neg_zero [symmetric] by auto
   702 
   703 end
   704 
   705 -- {* FIXME localize the following *}
   706 
   707 lemma add_increasing:
   708   fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
   709   shows  "[|0\<le>a; b\<le>c|] ==> b \<le> a + c"
   710 by (insert add_mono [of 0 a b c], simp)
   711 
   712 lemma add_increasing2:
   713   fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
   714   shows  "[|0\<le>c; b\<le>a|] ==> b \<le> a + c"
   715 by (simp add:add_increasing add_commute[of a])
   716 
   717 lemma add_strict_increasing:
   718   fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
   719   shows "[|0<a; b\<le>c|] ==> b < a + c"
   720 by (insert add_less_le_mono [of 0 a b c], simp)
   721 
   722 lemma add_strict_increasing2:
   723   fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
   724   shows "[|0\<le>a; b<c|] ==> b < a + c"
   725 by (insert add_le_less_mono [of 0 a b c], simp)
   726 
   727 
   728 class pordered_ab_group_add_abs = pordered_ab_group_add + abs +
   729   assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
   730     and abs_ge_self: "a \<le> \<bar>a\<bar>"
   731     and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
   732     and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
   733     and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   734 begin
   735 
   736 lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
   737   unfolding neg_le_0_iff_le by simp
   738 
   739 lemma abs_of_nonneg [simp]:
   740   assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a"
   741 proof (rule antisym)
   742   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
   743   from this nonneg have "- a \<le> a" by (rule order_trans)
   744   then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
   745 qed (rule abs_ge_self)
   746 
   747 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
   748 by (rule antisym)
   749    (auto intro!: abs_ge_self abs_leI order_trans [of "uminus (abs a)" zero "abs a"])
   750 
   751 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
   752 proof -
   753   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
   754   proof (rule antisym)
   755     assume zero: "\<bar>a\<bar> = 0"
   756     with abs_ge_self show "a \<le> 0" by auto
   757     from zero have "\<bar>-a\<bar> = 0" by simp
   758     with abs_ge_self [of "uminus a"] have "- a \<le> 0" by auto
   759     with neg_le_0_iff_le show "0 \<le> a" by auto
   760   qed
   761   then show ?thesis by auto
   762 qed
   763 
   764 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
   765 by simp
   766 
   767 lemma abs_0_eq [simp, noatp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
   768 proof -
   769   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
   770   thus ?thesis by simp
   771 qed
   772 
   773 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
   774 proof
   775   assume "\<bar>a\<bar> \<le> 0"
   776   then have "\<bar>a\<bar> = 0" by (rule antisym) simp
   777   thus "a = 0" by simp
   778 next
   779   assume "a = 0"
   780   thus "\<bar>a\<bar> \<le> 0" by simp
   781 qed
   782 
   783 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
   784 by (simp add: less_le)
   785 
   786 lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0"
   787 proof -
   788   have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto
   789   show ?thesis by (simp add: a)
   790 qed
   791 
   792 lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
   793 proof -
   794   have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
   795   then show ?thesis by simp
   796 qed
   797 
   798 lemma abs_minus_commute: 
   799   "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
   800 proof -
   801   have "\<bar>a - b\<bar> = \<bar>- (a - b)\<bar>" by (simp only: abs_minus_cancel)
   802   also have "... = \<bar>b - a\<bar>" by simp
   803   finally show ?thesis .
   804 qed
   805 
   806 lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
   807 by (rule abs_of_nonneg, rule less_imp_le)
   808 
   809 lemma abs_of_nonpos [simp]:
   810   assumes "a \<le> 0" shows "\<bar>a\<bar> = - a"
   811 proof -
   812   let ?b = "- a"
   813   have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
   814   unfolding abs_minus_cancel [of "?b"]
   815   unfolding neg_le_0_iff_le [of "?b"]
   816   unfolding minus_minus by (erule abs_of_nonneg)
   817   then show ?thesis using assms by auto
   818 qed
   819   
   820 lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
   821 by (rule abs_of_nonpos, rule less_imp_le)
   822 
   823 lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
   824 by (insert abs_ge_self, blast intro: order_trans)
   825 
   826 lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
   827 by (insert abs_le_D1 [of "uminus a"], simp)
   828 
   829 lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
   830 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
   831 
   832 lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
   833   apply (simp add: algebra_simps)
   834   apply (subgoal_tac "abs a = abs (plus b (minus a b))")
   835   apply (erule ssubst)
   836   apply (rule abs_triangle_ineq)
   837   apply (rule arg_cong[of _ _ abs])
   838   apply (simp add: algebra_simps)
   839 done
   840 
   841 lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
   842   apply (subst abs_le_iff)
   843   apply auto
   844   apply (rule abs_triangle_ineq2)
   845   apply (subst abs_minus_commute)
   846   apply (rule abs_triangle_ineq2)
   847 done
   848 
   849 lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   850 proof -
   851   have "abs(a - b) = abs(a + - b)" by (subst diff_minus, rule refl)
   852   also have "... <= abs a + abs (- b)" by (rule abs_triangle_ineq)
   853   finally show ?thesis by simp
   854 qed
   855 
   856 lemma abs_diff_triangle_ineq: "\<bar>a + b - (c + d)\<bar> \<le> \<bar>a - c\<bar> + \<bar>b - d\<bar>"
   857 proof -
   858   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)
   859   also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)
   860   finally show ?thesis .
   861 qed
   862 
   863 lemma abs_add_abs [simp]:
   864   "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
   865 proof (rule antisym)
   866   show "?L \<ge> ?R" by(rule abs_ge_self)
   867 next
   868   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
   869   also have "\<dots> = ?R" by simp
   870   finally show "?L \<le> ?R" .
   871 qed
   872 
   873 end
   874 
   875 
   876 subsection {* Lattice Ordered (Abelian) Groups *}
   877 
   878 class lordered_ab_group_add_meet = pordered_ab_group_add + lower_semilattice
   879 begin
   880 
   881 lemma add_inf_distrib_left:
   882   "a + inf b c = inf (a + b) (a + c)"
   883 apply (rule antisym)
   884 apply (simp_all add: le_infI)
   885 apply (rule add_le_imp_le_left [of "uminus a"])
   886 apply (simp only: add_assoc [symmetric], simp)
   887 apply rule
   888 apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+
   889 done
   890 
   891 lemma add_inf_distrib_right:
   892   "inf a b + c = inf (a + c) (b + c)"
   893 proof -
   894   have "c + inf a b = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)
   895   thus ?thesis by (simp add: add_commute)
   896 qed
   897 
   898 end
   899 
   900 class lordered_ab_group_add_join = pordered_ab_group_add + upper_semilattice
   901 begin
   902 
   903 lemma add_sup_distrib_left:
   904   "a + sup b c = sup (a + b) (a + c)" 
   905 apply (rule antisym)
   906 apply (rule add_le_imp_le_left [of "uminus a"])
   907 apply (simp only: add_assoc[symmetric], simp)
   908 apply rule
   909 apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+
   910 apply (rule le_supI)
   911 apply (simp_all)
   912 done
   913 
   914 lemma add_sup_distrib_right:
   915   "sup a b + c = sup (a+c) (b+c)"
   916 proof -
   917   have "c + sup a b = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
   918   thus ?thesis by (simp add: add_commute)
   919 qed
   920 
   921 end
   922 
   923 class lordered_ab_group_add = pordered_ab_group_add + lattice
   924 begin
   925 
   926 subclass lordered_ab_group_add_meet ..
   927 subclass lordered_ab_group_add_join ..
   928 
   929 lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
   930 
   931 lemma inf_eq_neg_sup: "inf a b = - sup (-a) (-b)"
   932 proof (rule inf_unique)
   933   fix a b :: 'a
   934   show "- sup (-a) (-b) \<le> a"
   935     by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"])
   936       (simp, simp add: add_sup_distrib_left)
   937 next
   938   fix a b :: 'a
   939   show "- sup (-a) (-b) \<le> b"
   940     by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"])
   941       (simp, simp add: add_sup_distrib_left)
   942 next
   943   fix a b c :: 'a
   944   assume "a \<le> b" "a \<le> c"
   945   then show "a \<le> - sup (-b) (-c)" by (subst neg_le_iff_le [symmetric])
   946     (simp add: le_supI)
   947 qed
   948   
   949 lemma sup_eq_neg_inf: "sup a b = - inf (-a) (-b)"
   950 proof (rule sup_unique)
   951   fix a b :: 'a
   952   show "a \<le> - inf (-a) (-b)"
   953     by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"])
   954       (simp, simp add: add_inf_distrib_left)
   955 next
   956   fix a b :: 'a
   957   show "b \<le> - inf (-a) (-b)"
   958     by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"])
   959       (simp, simp add: add_inf_distrib_left)
   960 next
   961   fix a b c :: 'a
   962   assume "a \<le> c" "b \<le> c"
   963   then show "- inf (-a) (-b) \<le> c" by (subst neg_le_iff_le [symmetric])
   964     (simp add: le_infI)
   965 qed
   966 
   967 lemma neg_inf_eq_sup: "- inf a b = sup (-a) (-b)"
   968 by (simp add: inf_eq_neg_sup)
   969 
   970 lemma neg_sup_eq_inf: "- sup a b = inf (-a) (-b)"
   971 by (simp add: sup_eq_neg_inf)
   972 
   973 lemma add_eq_inf_sup: "a + b = sup a b + inf a b"
   974 proof -
   975   have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute)
   976   hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup)
   977   hence "0 = (-a + sup a b) + (inf a b + (-b))"
   978     by (simp add: add_sup_distrib_left add_inf_distrib_right)
   979        (simp add: algebra_simps)
   980   thus ?thesis by (simp add: algebra_simps)
   981 qed
   982 
   983 subsection {* Positive Part, Negative Part, Absolute Value *}
   984 
   985 definition
   986   nprt :: "'a \<Rightarrow> 'a" where
   987   "nprt x = inf x 0"
   988 
   989 definition
   990   pprt :: "'a \<Rightarrow> 'a" where
   991   "pprt x = sup x 0"
   992 
   993 lemma pprt_neg: "pprt (- x) = - nprt x"
   994 proof -
   995   have "sup (- x) 0 = sup (- x) (- 0)" unfolding minus_zero ..
   996   also have "\<dots> = - inf x 0" unfolding neg_inf_eq_sup ..
   997   finally have "sup (- x) 0 = - inf x 0" .
   998   then show ?thesis unfolding pprt_def nprt_def .
   999 qed
  1000 
  1001 lemma nprt_neg: "nprt (- x) = - pprt x"
  1002 proof -
  1003   from pprt_neg have "pprt (- (- x)) = - nprt (- x)" .
  1004   then have "pprt x = - nprt (- x)" by simp
  1005   then show ?thesis by simp
  1006 qed
  1007 
  1008 lemma prts: "a = pprt a + nprt a"
  1009 by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric])
  1010 
  1011 lemma zero_le_pprt[simp]: "0 \<le> pprt a"
  1012 by (simp add: pprt_def)
  1013 
  1014 lemma nprt_le_zero[simp]: "nprt a \<le> 0"
  1015 by (simp add: nprt_def)
  1016 
  1017 lemma le_eq_neg: "a \<le> - b \<longleftrightarrow> a + b \<le> 0" (is "?l = ?r")
  1018 proof -
  1019   have a: "?l \<longrightarrow> ?r"
  1020     apply (auto)
  1021     apply (rule add_le_imp_le_right[of _ "uminus b" _])
  1022     apply (simp add: add_assoc)
  1023     done
  1024   have b: "?r \<longrightarrow> ?l"
  1025     apply (auto)
  1026     apply (rule add_le_imp_le_right[of _ "b" _])
  1027     apply (simp)
  1028     done
  1029   from a b show ?thesis by blast
  1030 qed
  1031 
  1032 lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def)
  1033 lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
  1034 
  1035 lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
  1036 by (simp add: pprt_def le_iff_sup sup_ACI)
  1037 
  1038 lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
  1039 by (simp add: nprt_def le_iff_inf inf_ACI)
  1040 
  1041 lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
  1042 by (simp add: pprt_def le_iff_sup sup_ACI)
  1043 
  1044 lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
  1045 by (simp add: nprt_def le_iff_inf inf_ACI)
  1046 
  1047 lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
  1048 proof -
  1049   {
  1050     fix a::'a
  1051     assume hyp: "sup a (-a) = 0"
  1052     hence "sup a (-a) + a = a" by (simp)
  1053     hence "sup (a+a) 0 = a" by (simp add: add_sup_distrib_right) 
  1054     hence "sup (a+a) 0 <= a" by (simp)
  1055     hence "0 <= a" by (blast intro: order_trans inf_sup_ord)
  1056   }
  1057   note p = this
  1058   assume hyp:"sup a (-a) = 0"
  1059   hence hyp2:"sup (-a) (-(-a)) = 0" by (simp add: sup_commute)
  1060   from p[OF hyp] p[OF hyp2] show "a = 0" by simp
  1061 qed
  1062 
  1063 lemma inf_0_imp_0: "inf a (-a) = 0 \<Longrightarrow> a = 0"
  1064 apply (simp add: inf_eq_neg_sup)
  1065 apply (simp add: sup_commute)
  1066 apply (erule sup_0_imp_0)
  1067 done
  1068 
  1069 lemma inf_0_eq_0 [simp, noatp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
  1070 by (rule, erule inf_0_imp_0) simp
  1071 
  1072 lemma sup_0_eq_0 [simp, noatp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
  1073 by (rule, erule sup_0_imp_0) simp
  1074 
  1075 lemma zero_le_double_add_iff_zero_le_single_add [simp]:
  1076   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
  1077 proof
  1078   assume "0 <= a + a"
  1079   hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute)
  1080   have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
  1081     by (simp add: add_sup_inf_distribs inf_ACI)
  1082   hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
  1083   hence "inf a 0 = 0" by (simp only: add_right_cancel)
  1084   then show "0 <= a" by (simp add: le_iff_inf inf_commute)    
  1085 next  
  1086   assume a: "0 <= a"
  1087   show "0 <= a + a" by (simp add: add_mono[OF a a, simplified])
  1088 qed
  1089 
  1090 lemma double_zero: "a + a = 0 \<longleftrightarrow> a = 0"
  1091 proof
  1092   assume assm: "a + a = 0"
  1093   then have "a + a + - a = - a" by simp
  1094   then have "a + (a + - a) = - a" by (simp only: add_assoc)
  1095   then have a: "- a = a" by simp (*FIXME tune proof*)
  1096   show "a = 0" apply (rule antisym)
  1097   apply (unfold neg_le_iff_le [symmetric, of a])
  1098   unfolding a apply simp
  1099   unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a]
  1100   unfolding assm unfolding le_less apply simp_all done
  1101 next
  1102   assume "a = 0" then show "a + a = 0" by simp
  1103 qed
  1104 
  1105 lemma zero_less_double_add_iff_zero_less_single_add:
  1106   "0 < a + a \<longleftrightarrow> 0 < a"
  1107 proof (cases "a = 0")
  1108   case True then show ?thesis by auto
  1109 next
  1110   case False then show ?thesis (*FIXME tune proof*)
  1111   unfolding less_le apply simp apply rule
  1112   apply clarify
  1113   apply rule
  1114   apply assumption
  1115   apply (rule notI)
  1116   unfolding double_zero [symmetric, of a] apply simp
  1117   done
  1118 qed
  1119 
  1120 lemma double_add_le_zero_iff_single_add_le_zero [simp]:
  1121   "a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
  1122 proof -
  1123   have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)" by (subst le_minus_iff, simp)
  1124   moreover have "\<dots> \<longleftrightarrow> a \<le> 0" by (simp add: zero_le_double_add_iff_zero_le_single_add)
  1125   ultimately show ?thesis by blast
  1126 qed
  1127 
  1128 lemma double_add_less_zero_iff_single_less_zero [simp]:
  1129   "a + a < 0 \<longleftrightarrow> a < 0"
  1130 proof -
  1131   have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)" by (subst less_minus_iff, simp)
  1132   moreover have "\<dots> \<longleftrightarrow> a < 0" by (simp add: zero_less_double_add_iff_zero_less_single_add)
  1133   ultimately show ?thesis by blast
  1134 qed
  1135 
  1136 declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp]
  1137 
  1138 lemma le_minus_self_iff: "a \<le> - a \<longleftrightarrow> a \<le> 0"
  1139 proof -
  1140   from add_le_cancel_left [of "uminus a" "plus a a" zero]
  1141   have "(a <= -a) = (a+a <= 0)" 
  1142     by (simp add: add_assoc[symmetric])
  1143   thus ?thesis by simp
  1144 qed
  1145 
  1146 lemma minus_le_self_iff: "- a \<le> a \<longleftrightarrow> 0 \<le> a"
  1147 proof -
  1148   from add_le_cancel_left [of "uminus a" zero "plus a a"]
  1149   have "(-a <= a) = (0 <= a+a)" 
  1150     by (simp add: add_assoc[symmetric])
  1151   thus ?thesis by simp
  1152 qed
  1153 
  1154 lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0"
  1155 by (simp add: le_iff_inf nprt_def inf_commute)
  1156 
  1157 lemma le_zero_iff_zero_pprt: "a \<le> 0 \<longleftrightarrow> pprt a = 0"
  1158 by (simp add: le_iff_sup pprt_def sup_commute)
  1159 
  1160 lemma le_zero_iff_pprt_id: "0 \<le> a \<longleftrightarrow> pprt a = a"
  1161 by (simp add: le_iff_sup pprt_def sup_commute)
  1162 
  1163 lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a"
  1164 by (simp add: le_iff_inf nprt_def inf_commute)
  1165 
  1166 lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
  1167 by (simp add: le_iff_sup pprt_def sup_ACI sup_assoc [symmetric, of a])
  1168 
  1169 lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
  1170 by (simp add: le_iff_inf nprt_def inf_ACI inf_assoc [symmetric, of a])
  1171 
  1172 end
  1173 
  1174 lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
  1175 
  1176 
  1177 class lordered_ab_group_add_abs = lordered_ab_group_add + abs +
  1178   assumes abs_lattice: "\<bar>a\<bar> = sup a (- a)"
  1179 begin
  1180 
  1181 lemma abs_prts: "\<bar>a\<bar> = pprt a - nprt a"
  1182 proof -
  1183   have "0 \<le> \<bar>a\<bar>"
  1184   proof -
  1185     have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice)
  1186     show ?thesis by (rule add_mono [OF a b, simplified])
  1187   qed
  1188   then have "0 \<le> sup a (- a)" unfolding abs_lattice .
  1189   then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
  1190   then show ?thesis
  1191     by (simp add: add_sup_inf_distribs sup_ACI
  1192       pprt_def nprt_def diff_minus abs_lattice)
  1193 qed
  1194 
  1195 subclass pordered_ab_group_add_abs
  1196 proof
  1197   have abs_ge_zero [simp]: "\<And>a. 0 \<le> \<bar>a\<bar>"
  1198   proof -
  1199     fix a b
  1200     have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice)
  1201     show "0 \<le> \<bar>a\<bar>" by (rule add_mono [OF a b, simplified])
  1202   qed
  1203   have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
  1204     by (simp add: abs_lattice le_supI)
  1205   fix a b
  1206   show "0 \<le> \<bar>a\<bar>" by simp
  1207   show "a \<le> \<bar>a\<bar>"
  1208     by (auto simp add: abs_lattice)
  1209   show "\<bar>-a\<bar> = \<bar>a\<bar>"
  1210     by (simp add: abs_lattice sup_commute)
  1211   show "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" by (fact abs_leI)
  1212   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
  1213   proof -
  1214     have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
  1215       by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus)
  1216     have a:"a+b <= sup ?m ?n" by (simp)
  1217     have b:"-a-b <= ?n" by (simp) 
  1218     have c:"?n <= sup ?m ?n" by (simp)
  1219     from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans)
  1220     have e:"-a-b = -(a+b)" by (simp add: diff_minus)
  1221     from a d e have "abs(a+b) <= sup ?m ?n" 
  1222       by (drule_tac abs_leI, auto)
  1223     with g[symmetric] show ?thesis by simp
  1224   qed
  1225 qed
  1226 
  1227 end
  1228 
  1229 lemma sup_eq_if:
  1230   fixes a :: "'a\<Colon>{lordered_ab_group_add, linorder}"
  1231   shows "sup a (- a) = (if a < 0 then - a else a)"
  1232 proof -
  1233   note add_le_cancel_right [of a a "- a", symmetric, simplified]
  1234   moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
  1235   then show ?thesis by (auto simp: sup_max max_def)
  1236 qed
  1237 
  1238 lemma abs_if_lattice:
  1239   fixes a :: "'a\<Colon>{lordered_ab_group_add_abs, linorder}"
  1240   shows "\<bar>a\<bar> = (if a < 0 then - a else a)"
  1241 by auto
  1242 
  1243 
  1244 text {* Needed for abelian cancellation simprocs: *}
  1245 
  1246 lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)"
  1247 apply (subst add_left_commute)
  1248 apply (subst add_left_cancel)
  1249 apply simp
  1250 done
  1251 
  1252 lemma add_cancel_end: "(x + (y + z) = y) = (x = - (z::'a::ab_group_add))"
  1253 apply (subst add_cancel_21[of _ _ _ 0, simplified])
  1254 apply (simp add: add_right_cancel[symmetric, of "x" "-z" "z", simplified])
  1255 done
  1256 
  1257 lemma less_eqI: "(x::'a::pordered_ab_group_add) - y = x' - y' \<Longrightarrow> (x < y) = (x' < y')"
  1258 by (simp add: less_iff_diff_less_0[of x y] less_iff_diff_less_0[of x' y'])
  1259 
  1260 lemma le_eqI: "(x::'a::pordered_ab_group_add) - y = x' - y' \<Longrightarrow> (y <= x) = (y' <= x')"
  1261 apply (simp add: le_iff_diff_le_0[of y x] le_iff_diff_le_0[of  y' x'])
  1262 apply (simp add: neg_le_iff_le[symmetric, of "y-x" 0] neg_le_iff_le[symmetric, of "y'-x'" 0])
  1263 done
  1264 
  1265 lemma eq_eqI: "(x::'a::ab_group_add) - y = x' - y' \<Longrightarrow> (x = y) = (x' = y')"
  1266 by (simp add: eq_iff_diff_eq_0[of x y] eq_iff_diff_eq_0[of x' y'])
  1267 
  1268 lemma diff_def: "(x::'a::ab_group_add) - y == x + (-y)"
  1269 by (simp add: diff_minus)
  1270 
  1271 lemma add_minus_cancel: "(a::'a::ab_group_add) + (-a + b) = b"
  1272 by (simp add: add_assoc[symmetric])
  1273 
  1274 lemma le_add_right_mono: 
  1275   assumes 
  1276   "a <= b + (c::'a::pordered_ab_group_add)"
  1277   "c <= d"    
  1278   shows "a <= b + d"
  1279   apply (rule_tac order_trans[where y = "b+c"])
  1280   apply (simp_all add: prems)
  1281   done
  1282 
  1283 lemma estimate_by_abs:
  1284   "a + b <= (c::'a::lordered_ab_group_add_abs) \<Longrightarrow> a <= c + abs b" 
  1285 proof -
  1286   assume "a+b <= c"
  1287   hence 2: "a <= c+(-b)" by (simp add: algebra_simps)
  1288   have 3: "(-b) <= abs b" by (rule abs_ge_minus_self)
  1289   show ?thesis by (rule le_add_right_mono[OF 2 3])
  1290 qed
  1291 
  1292 subsection {* Tools setup *}
  1293 
  1294 lemma add_mono_thms_ordered_semiring [noatp]:
  1295   fixes i j k :: "'a\<Colon>pordered_ab_semigroup_add"
  1296   shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1297     and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
  1298     and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
  1299     and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
  1300 by (rule add_mono, clarify+)+
  1301 
  1302 lemma add_mono_thms_ordered_field [noatp]:
  1303   fixes i j k :: "'a\<Colon>pordered_cancel_ab_semigroup_add"
  1304   shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
  1305     and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
  1306     and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
  1307     and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
  1308     and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"
  1309 by (auto intro: add_strict_right_mono add_strict_left_mono
  1310   add_less_le_mono add_le_less_mono add_strict_mono)
  1311 
  1312 text{*Simplification of @{term "x-y < 0"}, etc.*}
  1313 lemmas diff_less_0_iff_less [simp, noatp] = less_iff_diff_less_0 [symmetric]
  1314 lemmas diff_eq_0_iff_eq [simp, noatp] = eq_iff_diff_eq_0 [symmetric]
  1315 lemmas diff_le_0_iff_le [simp, noatp] = le_iff_diff_le_0 [symmetric]
  1316 
  1317 ML {*
  1318 structure ab_group_add_cancel = Abel_Cancel
  1319 (
  1320 
  1321 (* term order for abelian groups *)
  1322 
  1323 fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
  1324       [@{const_name HOL.zero}, @{const_name HOL.plus},
  1325         @{const_name HOL.uminus}, @{const_name HOL.minus}]
  1326   | agrp_ord _ = ~1;
  1327 
  1328 fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS);
  1329 
  1330 local
  1331   val ac1 = mk_meta_eq @{thm add_assoc};
  1332   val ac2 = mk_meta_eq @{thm add_commute};
  1333   val ac3 = mk_meta_eq @{thm add_left_commute};
  1334   fun solve_add_ac thy _ (_ $ (Const (@{const_name HOL.plus},_) $ _ $ _) $ _) =
  1335         SOME ac1
  1336     | solve_add_ac thy _ (_ $ x $ (Const (@{const_name HOL.plus},_) $ y $ z)) =
  1337         if termless_agrp (y, x) then SOME ac3 else NONE
  1338     | solve_add_ac thy _ (_ $ x $ y) =
  1339         if termless_agrp (y, x) then SOME ac2 else NONE
  1340     | solve_add_ac thy _ _ = NONE
  1341 in
  1342   val add_ac_proc = Simplifier.simproc (the_context ())
  1343     "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;
  1344 end;
  1345 
  1346 val eq_reflection = @{thm eq_reflection};
  1347   
  1348 val T = @{typ "'a::ab_group_add"};
  1349 
  1350 val cancel_ss = HOL_basic_ss settermless termless_agrp
  1351   addsimprocs [add_ac_proc] addsimps
  1352   [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_def},
  1353    @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},
  1354    @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},
  1355    @{thm minus_add_cancel}];
  1356 
  1357 val sum_pats = [@{cterm "x + y::'a::ab_group_add"}, @{cterm "x - y::'a::ab_group_add"}];
  1358   
  1359 val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];
  1360 
  1361 val dest_eqI = 
  1362   fst o HOLogic.dest_bin "op =" HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
  1363 
  1364 );
  1365 *}
  1366 
  1367 ML {*
  1368   Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];
  1369 *}
  1370 
  1371 end