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