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