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