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