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