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