src/HOL/Groups.thy
 author paulson Mon Feb 22 14:37:56 2016 +0000 (2016-02-22) changeset 62379 340738057c8c parent 62378 85ed00c1fe7c child 62608 19f87fa0cfcb permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
 haftmann@35050  1 (* Title: HOL/Groups.thy  wenzelm@29269  2  Author: Gertrud Bauer, Steven Obua, Lawrence C Paulson, Markus Wenzel, Jeremy Avigad  obua@14738  3 *)  obua@14738  4 wenzelm@60758  5 section \Groups, also combined with orderings\  obua@14738  6 haftmann@35050  7 theory Groups  haftmann@35092  8 imports Orderings  nipkow@15131  9 begin  obua@14738  10 wenzelm@60758  11 subsection \Dynamic facts\  haftmann@35301  12 wenzelm@57950  13 named_theorems ac_simps "associativity and commutativity simplification rules"  haftmann@36343  14 haftmann@36343  15 wenzelm@61799  16 text\The rewrites accumulated in \algebra_simps\ deal with the  haftmann@36348  17 classical algebraic structures of groups, rings and family. They simplify  haftmann@36348  18 terms by multiplying everything out (in case of a ring) and bringing sums and  haftmann@36348  19 products into a canonical form (by ordered rewriting). As a result it decides  haftmann@36348  20 group and ring equalities but also helps with inequalities.  haftmann@36348  21 haftmann@36348  22 Of course it also works for fields, but it knows nothing about multiplicative  wenzelm@61799  23 inverses or division. This is catered for by \field_simps\.\  haftmann@36348  24 wenzelm@57950  25 named_theorems algebra_simps "algebra simplification rules"  haftmann@35301  26 haftmann@35301  27 wenzelm@61799  28 text\Lemmas \field_simps\ multiply with denominators in (in)equations  haftmann@36348  29 if they can be proved to be non-zero (for equations) or positive/negative  haftmann@36348  30 (for inequations). Can be too aggressive and is therefore separate from the  wenzelm@61799  31 more benign \algebra_simps\.\  haftmann@35301  32 wenzelm@57950  33 named_theorems field_simps "algebra simplification rules for fields"  haftmann@35301  34 haftmann@35301  35 wenzelm@60758  36 subsection \Abstract structures\  haftmann@35301  37 wenzelm@60758  38 text \  haftmann@35301  39  These locales provide basic structures for interpretation into  haftmann@35301  40  bigger structures; extensions require careful thinking, otherwise  haftmann@35301  41  undesired effects may occur due to interpretation.  wenzelm@60758  42 \  haftmann@35301  43 haftmann@35301  44 locale semigroup =  haftmann@35301  45  fixes f :: "'a \ 'a \ 'a" (infixl "*" 70)  haftmann@35301  46  assumes assoc [ac_simps]: "a * b * c = a * (b * c)"  haftmann@35301  47 haftmann@35301  48 locale abel_semigroup = semigroup +  haftmann@35301  49  assumes commute [ac_simps]: "a * b = b * a"  haftmann@35301  50 begin  haftmann@35301  51 haftmann@35301  52 lemma left_commute [ac_simps]:  haftmann@35301  53  "b * (a * c) = a * (b * c)"  haftmann@35301  54 proof -  haftmann@35301  55  have "(b * a) * c = (a * b) * c"  haftmann@35301  56  by (simp only: commute)  haftmann@35301  57  then show ?thesis  haftmann@35301  58  by (simp only: assoc)  haftmann@35301  59 qed  haftmann@35301  60 haftmann@35301  61 end  haftmann@35301  62 haftmann@35720  63 locale monoid = semigroup +  haftmann@35723  64  fixes z :: 'a ("1")  haftmann@35723  65  assumes left_neutral [simp]: "1 * a = a"  haftmann@35723  66  assumes right_neutral [simp]: "a * 1 = a"  haftmann@35720  67 haftmann@35720  68 locale comm_monoid = abel_semigroup +  haftmann@35723  69  fixes z :: 'a ("1")  haftmann@35723  70  assumes comm_neutral: "a * 1 = a"  haftmann@54868  71 begin  haftmann@35720  72 haftmann@54868  73 sublocale monoid  wenzelm@61169  74  by standard (simp_all add: commute comm_neutral)  haftmann@35720  75 haftmann@54868  76 end  haftmann@54868  77 haftmann@35301  78 wenzelm@60758  79 subsection \Generic operations\  haftmann@35267  80 hoelzl@62376  81 class zero =  haftmann@35267  82  fixes zero :: 'a ("0")  haftmann@35267  83 haftmann@35267  84 class one =  haftmann@35267  85  fixes one :: 'a ("1")  haftmann@35267  86 wenzelm@36176  87 hide_const (open) zero one  haftmann@35267  88 haftmann@35267  89 lemma Let_0 [simp]: "Let 0 f = f 0"  haftmann@35267  90  unfolding Let_def ..  haftmann@35267  91 haftmann@35267  92 lemma Let_1 [simp]: "Let 1 f = f 1"  haftmann@35267  93  unfolding Let_def ..  haftmann@35267  94 wenzelm@60758  95 setup \  haftmann@35267  96  Reorient_Proc.add  haftmann@35267  97  (fn Const(@{const_name Groups.zero}, _) => true  haftmann@35267  98  | Const(@{const_name Groups.one}, _) => true  haftmann@35267  99  | _ => false)  wenzelm@60758  100 \  haftmann@35267  101 haftmann@35267  102 simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc  haftmann@35267  103 simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc  haftmann@35267  104 wenzelm@60758  105 typed_print_translation \  wenzelm@42247  106  let  wenzelm@42247  107  fun tr' c = (c, fn ctxt => fn T => fn ts =>  wenzelm@52210  108  if null ts andalso Printer.type_emphasis ctxt T then  wenzelm@42248  109  Syntax.const @{syntax_const "_constrain"} $Syntax.const c$  wenzelm@52210  110  Syntax_Phases.term_of_typ ctxt T  wenzelm@52210  111  else raise Match);  wenzelm@42247  112  in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;  wenzelm@61799  113 \ \ \show types that are presumably too general\  haftmann@35267  114 haftmann@35267  115 class plus =  haftmann@35267  116  fixes plus :: "'a \ 'a \ 'a" (infixl "+" 65)  haftmann@35267  117 haftmann@35267  118 class minus =  haftmann@35267  119  fixes minus :: "'a \ 'a \ 'a" (infixl "-" 65)  haftmann@35267  120 haftmann@35267  121 class uminus =  haftmann@35267  122  fixes uminus :: "'a \ 'a" ("- _" [81] 80)  haftmann@35267  123 haftmann@35267  124 class times =  haftmann@35267  125  fixes times :: "'a \ 'a \ 'a" (infixl "*" 70)  haftmann@35267  126 haftmann@35092  127 wenzelm@60758  128 subsection \Semigroups and Monoids\  obua@14738  129 haftmann@22390  130 class semigroup_add = plus +  haftmann@36348  131  assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"  haftmann@54868  132 begin  haftmann@34973  133 wenzelm@61605  134 sublocale add: semigroup plus  wenzelm@61169  135  by standard (fact add_assoc)  haftmann@22390  136 haftmann@54868  137 end  haftmann@54868  138 haftmann@57512  139 hide_fact add_assoc  haftmann@57512  140 haftmann@22390  141 class ab_semigroup_add = semigroup_add +  haftmann@36348  142  assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"  haftmann@54868  143 begin  haftmann@34973  144 wenzelm@61605  145 sublocale add: abel_semigroup plus  wenzelm@61169  146  by standard (fact add_commute)  haftmann@34973  147 haftmann@57512  148 declare add.left_commute [algebra_simps, field_simps]  haftmann@25062  149 wenzelm@61337  150 lemmas add_ac = add.assoc add.commute add.left_commute  nipkow@57571  151 haftmann@25062  152 end  obua@14738  153 haftmann@57512  154 hide_fact add_commute  haftmann@57512  155 wenzelm@61337  156 lemmas add_ac = add.assoc add.commute add.left_commute  nipkow@57571  157 haftmann@22390  158 class semigroup_mult = times +  haftmann@36348  159  assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"  haftmann@54868  160 begin  haftmann@34973  161 wenzelm@61605  162 sublocale mult: semigroup times  wenzelm@61169  163  by standard (fact mult_assoc)  obua@14738  164 haftmann@54868  165 end  haftmann@54868  166 haftmann@57512  167 hide_fact mult_assoc  haftmann@57512  168 haftmann@22390  169 class ab_semigroup_mult = semigroup_mult +  haftmann@36348  170  assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"  haftmann@54868  171 begin  haftmann@34973  172 wenzelm@61605  173 sublocale mult: abel_semigroup times  wenzelm@61169  174  by standard (fact mult_commute)  haftmann@34973  175 haftmann@57512  176 declare mult.left_commute [algebra_simps, field_simps]  haftmann@25062  177 wenzelm@61337  178 lemmas mult_ac = mult.assoc mult.commute mult.left_commute  nipkow@57571  179 haftmann@23181  180 end  obua@14738  181 haftmann@57512  182 hide_fact mult_commute  haftmann@57512  183 wenzelm@61337  184 lemmas mult_ac = mult.assoc mult.commute mult.left_commute  nipkow@57571  185 nipkow@23085  186 class monoid_add = zero + semigroup_add +  haftmann@35720  187  assumes add_0_left: "0 + a = a"  haftmann@35720  188  and add_0_right: "a + 0 = a"  haftmann@54868  189 begin  haftmann@35720  190 wenzelm@61605  191 sublocale add: monoid plus 0  wenzelm@61169  192  by standard (fact add_0_left add_0_right)+  nipkow@23085  193 haftmann@54868  194 end  haftmann@54868  195 haftmann@26071  196 lemma zero_reorient: "0 = x \ x = 0"  haftmann@54868  197  by (fact eq_commute)  haftmann@26071  198 haftmann@22390  199 class comm_monoid_add = zero + ab_semigroup_add +  haftmann@25062  200  assumes add_0: "0 + a = a"  haftmann@54868  201 begin  nipkow@23085  202 haftmann@59559  203 subclass monoid_add  wenzelm@61169  204  by standard (simp_all add: add_0 add.commute [of _ 0])  haftmann@25062  205 wenzelm@61605  206 sublocale add: comm_monoid plus 0  wenzelm@61169  207  by standard (simp add: ac_simps)  obua@14738  208 haftmann@54868  209 end  haftmann@54868  210 haftmann@22390  211 class monoid_mult = one + semigroup_mult +  haftmann@35720  212  assumes mult_1_left: "1 * a = a"  haftmann@35720  213  and mult_1_right: "a * 1 = a"  haftmann@54868  214 begin  haftmann@35720  215 wenzelm@61605  216 sublocale mult: monoid times 1  wenzelm@61169  217  by standard (fact mult_1_left mult_1_right)+  obua@14738  218 haftmann@54868  219 end  haftmann@54868  220 haftmann@26071  221 lemma one_reorient: "1 = x \ x = 1"  haftmann@54868  222  by (fact eq_commute)  haftmann@26071  223 haftmann@22390  224 class comm_monoid_mult = one + ab_semigroup_mult +  haftmann@25062  225  assumes mult_1: "1 * a = a"  haftmann@54868  226 begin  obua@14738  227 haftmann@59559  228 subclass monoid_mult  wenzelm@61169  229  by standard (simp_all add: mult_1 mult.commute [of _ 1])  haftmann@25062  230 wenzelm@61605  231 sublocale mult: comm_monoid times 1  wenzelm@61169  232  by standard (simp add: ac_simps)  obua@14738  233 haftmann@54868  234 end  haftmann@54868  235 haftmann@22390  236 class cancel_semigroup_add = semigroup_add +  haftmann@25062  237  assumes add_left_imp_eq: "a + b = a + c \ b = c"  haftmann@25062  238  assumes add_right_imp_eq: "b + a = c + a \ b = c"  huffman@27474  239 begin  huffman@27474  240 huffman@27474  241 lemma add_left_cancel [simp]:  huffman@27474  242  "a + b = a + c \ b = c"  nipkow@29667  243 by (blast dest: add_left_imp_eq)  huffman@27474  244 huffman@27474  245 lemma add_right_cancel [simp]:  huffman@27474  246  "b + a = c + a \ b = c"  nipkow@29667  247 by (blast dest: add_right_imp_eq)  huffman@27474  248 huffman@27474  249 end  obua@14738  250 haftmann@59815  251 class cancel_ab_semigroup_add = ab_semigroup_add + minus +  haftmann@59815  252  assumes add_diff_cancel_left' [simp]: "(a + b) - a = b"  haftmann@59815  253  assumes diff_diff_add [algebra_simps, field_simps]: "a - b - c = a - (b + c)"  haftmann@25267  254 begin  obua@14738  255 haftmann@59815  256 lemma add_diff_cancel_right' [simp]:  haftmann@59815  257  "(a + b) - b = a"  haftmann@59815  258  using add_diff_cancel_left' [of b a] by (simp add: ac_simps)  haftmann@59815  259 haftmann@25267  260 subclass cancel_semigroup_add  haftmann@28823  261 proof  haftmann@22390  262  fix a b c :: 'a  haftmann@59815  263  assume "a + b = a + c"  haftmann@59815  264  then have "a + b - a = a + c - a"  haftmann@59815  265  by simp  haftmann@59815  266  then show "b = c"  haftmann@59815  267  by simp  haftmann@22390  268 next  obua@14738  269  fix a b c :: 'a  obua@14738  270  assume "b + a = c + a"  haftmann@59815  271  then have "b + a - a = c + a - a"  haftmann@59815  272  by simp  haftmann@59815  273  then show "b = c"  haftmann@59815  274  by simp  obua@14738  275 qed  obua@14738  276 haftmann@59815  277 lemma add_diff_cancel_left [simp]:  haftmann@59815  278  "(c + a) - (c + b) = a - b"  haftmann@59815  279  unfolding diff_diff_add [symmetric] by simp  haftmann@59815  280 haftmann@59815  281 lemma add_diff_cancel_right [simp]:  haftmann@59815  282  "(a + c) - (b + c) = a - b"  haftmann@59815  283  using add_diff_cancel_left [symmetric] by (simp add: ac_simps)  haftmann@59815  284 haftmann@59815  285 lemma diff_right_commute:  haftmann@59815  286  "a - c - b = a - b - c"  haftmann@59815  287  by (simp add: diff_diff_add add.commute)  haftmann@59815  288 haftmann@25267  289 end  haftmann@25267  290 huffman@29904  291 class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add  haftmann@59322  292 begin  haftmann@59322  293 haftmann@59815  294 lemma diff_zero [simp]:  haftmann@59815  295  "a - 0 = a"  haftmann@59815  296  using add_diff_cancel_right' [of a 0] by simp  haftmann@59322  297 haftmann@59322  298 lemma diff_cancel [simp]:  haftmann@59322  299  "a - a = 0"  haftmann@59322  300 proof -  haftmann@59322  301  have "(a + 0) - (a + 0) = 0" by (simp only: add_diff_cancel_left diff_zero)  haftmann@59322  302  then show ?thesis by simp  haftmann@59322  303 qed  haftmann@59322  304 haftmann@59322  305 lemma add_implies_diff:  haftmann@59322  306  assumes "c + b = a"  haftmann@59322  307  shows "c = a - b"  haftmann@59322  308 proof -  haftmann@59322  309  from assms have "(b + c) - (b + 0) = a - b" by (simp add: add.commute)  haftmann@59322  310  then show "c = a - b" by simp  haftmann@59322  311 qed  haftmann@59322  312 hoelzl@62376  313 end  haftmann@59815  314 haftmann@59815  315 class comm_monoid_diff = cancel_comm_monoid_add +  haftmann@59815  316  assumes zero_diff [simp]: "0 - a = 0"  haftmann@59815  317 begin  haftmann@59815  318 haftmann@59815  319 lemma diff_add_zero [simp]:  haftmann@59815  320  "a - (a + b) = 0"  haftmann@59815  321 proof -  haftmann@59815  322  have "a - (a + b) = (a + 0) - (a + b)" by simp  haftmann@59815  323  also have "\ = 0" by (simp only: add_diff_cancel_left zero_diff)  haftmann@59815  324  finally show ?thesis .  haftmann@59815  325 qed  haftmann@59815  326 haftmann@59322  327 end  haftmann@59322  328 huffman@29904  329 wenzelm@60758  330 subsection \Groups\  nipkow@23085  331 haftmann@25762  332 class group_add = minus + uminus + monoid_add +  haftmann@25062  333  assumes left_minus [simp]: "- a + a = 0"  haftmann@54230  334  assumes add_uminus_conv_diff [simp]: "a + (- b) = a - b"  haftmann@25062  335 begin  nipkow@23085  336 haftmann@54230  337 lemma diff_conv_add_uminus:  haftmann@54230  338  "a - b = a + (- b)"  haftmann@54230  339  by simp  haftmann@54230  340 huffman@34147  341 lemma minus_unique:  huffman@34147  342  assumes "a + b = 0" shows "- a = b"  huffman@34147  343 proof -  huffman@34147  344  have "- a = - a + (a + b)" using assms by simp  haftmann@57512  345  also have "\ = b" by (simp add: add.assoc [symmetric])  huffman@34147  346  finally show ?thesis .  huffman@34147  347 qed  huffman@34147  348 haftmann@25062  349 lemma minus_zero [simp]: "- 0 = 0"  obua@14738  350 proof -  huffman@34147  351  have "0 + 0 = 0" by (rule add_0_right)  huffman@34147  352  thus "- 0 = 0" by (rule minus_unique)  obua@14738  353 qed  obua@14738  354 haftmann@25062  355 lemma minus_minus [simp]: "- (- a) = a"  nipkow@23085  356 proof -  huffman@34147  357  have "- a + a = 0" by (rule left_minus)  huffman@34147  358  thus "- (- a) = a" by (rule minus_unique)  nipkow@23085  359 qed  obua@14738  360 haftmann@54230  361 lemma right_minus: "a + - a = 0"  obua@14738  362 proof -  haftmann@25062  363  have "a + - a = - (- a) + - a" by simp  haftmann@25062  364  also have "\ = 0" by (rule left_minus)  obua@14738  365  finally show ?thesis .  obua@14738  366 qed  obua@14738  367 haftmann@54230  368 lemma diff_self [simp]:  haftmann@54230  369  "a - a = 0"  haftmann@54230  370  using right_minus [of a] by simp  haftmann@54230  371 haftmann@40368  372 subclass cancel_semigroup_add  haftmann@40368  373 proof  haftmann@40368  374  fix a b c :: 'a  haftmann@40368  375  assume "a + b = a + c"  haftmann@40368  376  then have "- a + a + b = - a + a + c"  haftmann@57512  377  unfolding add.assoc by simp  haftmann@40368  378  then show "b = c" by simp  haftmann@40368  379 next  haftmann@40368  380  fix a b c :: 'a  haftmann@40368  381  assume "b + a = c + a"  haftmann@40368  382  then have "b + a + - a = c + a + - a" by simp  haftmann@57512  383  then show "b = c" unfolding add.assoc by simp  haftmann@40368  384 qed  haftmann@40368  385 haftmann@54230  386 lemma minus_add_cancel [simp]:  haftmann@54230  387  "- a + (a + b) = b"  haftmann@57512  388  by (simp add: add.assoc [symmetric])  haftmann@54230  389 haftmann@54230  390 lemma add_minus_cancel [simp]:  haftmann@54230  391  "a + (- a + b) = b"  haftmann@57512  392  by (simp add: add.assoc [symmetric])  huffman@34147  393 haftmann@54230  394 lemma diff_add_cancel [simp]:  haftmann@54230  395  "a - b + b = a"  haftmann@57512  396  by (simp only: diff_conv_add_uminus add.assoc) simp  huffman@34147  397 haftmann@54230  398 lemma add_diff_cancel [simp]:  haftmann@54230  399  "a + b - b = a"  haftmann@57512  400  by (simp only: diff_conv_add_uminus add.assoc) simp  haftmann@54230  401 haftmann@54230  402 lemma minus_add:  haftmann@54230  403  "- (a + b) = - b + - a"  huffman@34147  404 proof -  huffman@34147  405  have "(a + b) + (- b + - a) = 0"  haftmann@57512  406  by (simp only: add.assoc add_minus_cancel) simp  haftmann@54230  407  then show "- (a + b) = - b + - a"  huffman@34147  408  by (rule minus_unique)  huffman@34147  409 qed  huffman@34147  410 haftmann@54230  411 lemma right_minus_eq [simp]:  haftmann@54230  412  "a - b = 0 \ a = b"  obua@14738  413 proof  nipkow@23085  414  assume "a - b = 0"  haftmann@57512  415  have "a = (a - b) + b" by (simp add: add.assoc)  wenzelm@60758  416  also have "\ = b" using \a - b = 0\ by simp  nipkow@23085  417  finally show "a = b" .  obua@14738  418 next  haftmann@54230  419  assume "a = b" thus "a - b = 0" by simp  obua@14738  420 qed  obua@14738  421 haftmann@54230  422 lemma eq_iff_diff_eq_0:  haftmann@54230  423  "a = b \ a - b = 0"  haftmann@54230  424  by (fact right_minus_eq [symmetric])  obua@14738  425 haftmann@54230  426 lemma diff_0 [simp]:  haftmann@54230  427  "0 - a = - a"  haftmann@54230  428  by (simp only: diff_conv_add_uminus add_0_left)  obua@14738  429 haftmann@54230  430 lemma diff_0_right [simp]:  hoelzl@62376  431  "a - 0 = a"  haftmann@54230  432  by (simp only: diff_conv_add_uminus minus_zero add_0_right)  obua@14738  433 haftmann@54230  434 lemma diff_minus_eq_add [simp]:  haftmann@54230  435  "a - - b = a + b"  haftmann@54230  436  by (simp only: diff_conv_add_uminus minus_minus)  obua@14738  437 haftmann@25062  438 lemma neg_equal_iff_equal [simp]:  hoelzl@62376  439  "- a = - b \ a = b"  hoelzl@62376  440 proof  obua@14738  441  assume "- a = - b"  nipkow@29667  442  hence "- (- a) = - (- b)" by simp  haftmann@25062  443  thus "a = b" by simp  obua@14738  444 next  haftmann@25062  445  assume "a = b"  haftmann@25062  446  thus "- a = - b" by simp  obua@14738  447 qed  obua@14738  448 haftmann@25062  449 lemma neg_equal_0_iff_equal [simp]:  haftmann@25062  450  "- a = 0 \ a = 0"  haftmann@54230  451  by (subst neg_equal_iff_equal [symmetric]) simp  obua@14738  452 haftmann@25062  453 lemma neg_0_equal_iff_equal [simp]:  haftmann@25062  454  "0 = - a \ 0 = a"  haftmann@54230  455  by (subst neg_equal_iff_equal [symmetric]) simp  obua@14738  456 wenzelm@60758  457 text\The next two equations can make the simplifier loop!\  obua@14738  458 haftmann@25062  459 lemma equation_minus_iff:  haftmann@25062  460  "a = - b \ b = - a"  obua@14738  461 proof -  haftmann@25062  462  have "- (- a) = - b \ - a = b" by (rule neg_equal_iff_equal)  haftmann@25062  463  thus ?thesis by (simp add: eq_commute)  haftmann@25062  464 qed  haftmann@25062  465 haftmann@25062  466 lemma minus_equation_iff:  haftmann@25062  467  "- a = b \ - b = a"  haftmann@25062  468 proof -  haftmann@25062  469  have "- a = - (- b) \ a = -b" by (rule neg_equal_iff_equal)  obua@14738  470  thus ?thesis by (simp add: eq_commute)  obua@14738  471 qed  obua@14738  472 haftmann@54230  473 lemma eq_neg_iff_add_eq_0:  haftmann@54230  474  "a = - b \ a + b = 0"  huffman@29914  475 proof  huffman@29914  476  assume "a = - b" then show "a + b = 0" by simp  huffman@29914  477 next  huffman@29914  478  assume "a + b = 0"  huffman@29914  479  moreover have "a + (b + - b) = (a + b) + - b"  haftmann@57512  480  by (simp only: add.assoc)  huffman@29914  481  ultimately show "a = - b" by simp  huffman@29914  482 qed  huffman@29914  483 haftmann@54230  484 lemma add_eq_0_iff2:  haftmann@54230  485  "a + b = 0 \ a = - b"  haftmann@54230  486  by (fact eq_neg_iff_add_eq_0 [symmetric])  haftmann@54230  487 haftmann@54230  488 lemma neg_eq_iff_add_eq_0:  haftmann@54230  489  "- a = b \ a + b = 0"  haftmann@54230  490  by (auto simp add: add_eq_0_iff2)  huffman@44348  491 haftmann@54230  492 lemma add_eq_0_iff:  haftmann@54230  493  "a + b = 0 \ b = - a"  haftmann@54230  494  by (auto simp add: neg_eq_iff_add_eq_0 [symmetric])  huffman@45548  495 haftmann@54230  496 lemma minus_diff_eq [simp]:  haftmann@54230  497  "- (a - b) = b - a"  haftmann@57512  498  by (simp only: neg_eq_iff_add_eq_0 diff_conv_add_uminus add.assoc minus_add_cancel) simp  huffman@45548  499 haftmann@54230  500 lemma add_diff_eq [algebra_simps, field_simps]:  haftmann@54230  501  "a + (b - c) = (a + b) - c"  haftmann@57512  502  by (simp only: diff_conv_add_uminus add.assoc)  huffman@45548  503 haftmann@54230  504 lemma diff_add_eq_diff_diff_swap:  haftmann@54230  505  "a - (b + c) = a - c - b"  haftmann@57512  506  by (simp only: diff_conv_add_uminus add.assoc minus_add)  huffman@45548  507 haftmann@54230  508 lemma diff_eq_eq [algebra_simps, field_simps]:  haftmann@54230  509  "a - b = c \ a = c + b"  haftmann@54230  510  by auto  huffman@45548  511 haftmann@54230  512 lemma eq_diff_eq [algebra_simps, field_simps]:  haftmann@54230  513  "a = c - b \ a + b = c"  haftmann@54230  514  by auto  haftmann@54230  515 haftmann@54230  516 lemma diff_diff_eq2 [algebra_simps, field_simps]:  haftmann@54230  517  "a - (b - c) = (a + c) - b"  haftmann@57512  518  by (simp only: diff_conv_add_uminus add.assoc) simp  huffman@45548  519 huffman@45548  520 lemma diff_eq_diff_eq:  huffman@45548  521  "a - b = c - d \ a = b \ c = d"  haftmann@54230  522  by (simp only: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])  huffman@45548  523 haftmann@25062  524 end  haftmann@25062  525 haftmann@25762  526 class ab_group_add = minus + uminus + comm_monoid_add +  haftmann@25062  527  assumes ab_left_minus: "- a + a = 0"  haftmann@59557  528  assumes ab_diff_conv_add_uminus: "a - b = a + (- b)"  haftmann@25267  529 begin  haftmann@25062  530 haftmann@25267  531 subclass group_add  haftmann@59557  532  proof qed (simp_all add: ab_left_minus ab_diff_conv_add_uminus)  haftmann@25062  533 huffman@29904  534 subclass cancel_comm_monoid_add  haftmann@28823  535 proof  haftmann@25062  536  fix a b c :: 'a  haftmann@59815  537  have "b + a - a = b"  haftmann@59815  538  by simp  haftmann@59815  539  then show "a + b - a = b"  haftmann@59815  540  by (simp add: ac_simps)  haftmann@59815  541  show "a - b - c = a - (b + c)"  haftmann@59815  542  by (simp add: algebra_simps)  haftmann@25062  543 qed  haftmann@25062  544 haftmann@54230  545 lemma uminus_add_conv_diff [simp]:  haftmann@25062  546  "- a + b = b - a"  haftmann@57512  547  by (simp add: add.commute)  haftmann@25062  548 haftmann@25062  549 lemma minus_add_distrib [simp]:  haftmann@25062  550  "- (a + b) = - a + - b"  haftmann@54230  551  by (simp add: algebra_simps)  haftmann@25062  552 haftmann@54230  553 lemma diff_add_eq [algebra_simps, field_simps]:  haftmann@54230  554  "(a - b) + c = (a + c) - b"  haftmann@54230  555  by (simp add: algebra_simps)  haftmann@25077  556 haftmann@25062  557 end  obua@14738  558 haftmann@37884  559 hoelzl@62376  560 subsection \(Partially) Ordered Groups\  obua@14738  561 wenzelm@60758  562 text \  haftmann@35301  563  The theory of partially ordered groups is taken from the books:  haftmann@35301  564  \begin{itemize}  hoelzl@62376  565  \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979  haftmann@35301  566  \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963  haftmann@35301  567  \end{itemize}  hoelzl@62376  568  Most of the used notions can also be looked up in  haftmann@35301  569  \begin{itemize}  wenzelm@54703  570  \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.  haftmann@35301  571  \item \emph{Algebra I} by van der Waerden, Springer.  haftmann@35301  572  \end{itemize}  wenzelm@60758  573 \  haftmann@35301  574 haftmann@35028  575 class ordered_ab_semigroup_add = order + ab_semigroup_add +  haftmann@25062  576  assumes add_left_mono: "a \ b \ c + a \ c + b"  haftmann@25062  577 begin  haftmann@24380  578 haftmann@25062  579 lemma add_right_mono:  haftmann@25062  580  "a \ b \ a + c \ b + c"  haftmann@57512  581 by (simp add: add.commute [of _ c] add_left_mono)  obua@14738  582 wenzelm@60758  583 text \non-strict, in both arguments\  obua@14738  584 lemma add_mono:  haftmann@25062  585  "a \ b \ c \ d \ a + c \ b + d"  obua@14738  586  apply (erule add_right_mono [THEN order_trans])  haftmann@57512  587  apply (simp add: add.commute add_left_mono)  obua@14738  588  done  obua@14738  589 haftmann@25062  590 end  haftmann@25062  591 hoelzl@62377  592 text\Strict monotonicity in both arguments\  hoelzl@62377  593 class strict_ordered_ab_semigroup_add = ordered_ab_semigroup_add +  hoelzl@62377  594  assumes add_strict_mono: "a < b \ c < d \ a + c < b + d"  hoelzl@62377  595 haftmann@35028  596 class ordered_cancel_ab_semigroup_add =  haftmann@35028  597  ordered_ab_semigroup_add + cancel_ab_semigroup_add  haftmann@25062  598 begin  haftmann@25062  599 obua@14738  600 lemma add_strict_left_mono:  haftmann@25062  601  "a < b \ c + a < c + b"  nipkow@29667  602 by (auto simp add: less_le add_left_mono)  obua@14738  603 obua@14738  604 lemma add_strict_right_mono:  haftmann@25062  605  "a < b \ a + c < b + c"  haftmann@57512  606 by (simp add: add.commute [of _ c] add_strict_left_mono)  obua@14738  607 hoelzl@62377  608 subclass strict_ordered_ab_semigroup_add  hoelzl@62377  609  apply standard  hoelzl@62377  610  apply (erule add_strict_right_mono [THEN less_trans])  hoelzl@62377  611  apply (erule add_strict_left_mono)  hoelzl@62377  612  done  obua@14738  613 obua@14738  614 lemma add_less_le_mono:  haftmann@25062  615  "a < b \ c \ d \ a + c < b + d"  haftmann@25062  616 apply (erule add_strict_right_mono [THEN less_le_trans])  haftmann@25062  617 apply (erule add_left_mono)  obua@14738  618 done  obua@14738  619 obua@14738  620 lemma add_le_less_mono:  haftmann@25062  621  "a \ b \ c < d \ a + c < b + d"  haftmann@25062  622 apply (erule add_right_mono [THEN le_less_trans])  hoelzl@62376  623 apply (erule add_strict_left_mono)  obua@14738  624 done  obua@14738  625 haftmann@25062  626 end  haftmann@25062  627 hoelzl@62377  628 class ordered_ab_semigroup_add_imp_le = ordered_cancel_ab_semigroup_add +  haftmann@25062  629  assumes add_le_imp_le_left: "c + a \ c + b \ a \ b"  haftmann@25062  630 begin  haftmann@25062  631 obua@14738  632 lemma add_less_imp_less_left:  nipkow@29667  633  assumes less: "c + a < c + b" shows "a < b"  obua@14738  634 proof -  obua@14738  635  from less have le: "c + a <= c + b" by (simp add: order_le_less)  hoelzl@62376  636  have "a <= b"  obua@14738  637  apply (insert le)  obua@14738  638  apply (drule add_le_imp_le_left)  obua@14738  639  by (insert le, drule add_le_imp_le_left, assumption)  obua@14738  640  moreover have "a \ b"  obua@14738  641  proof (rule ccontr)  obua@14738  642  assume "~(a \ b)"  obua@14738  643  then have "a = b" by simp  obua@14738  644  then have "c + a = c + b" by simp  obua@14738  645  with less show "False"by simp  obua@14738  646  qed  obua@14738  647  ultimately show "a < b" by (simp add: order_le_less)  obua@14738  648 qed  obua@14738  649 obua@14738  650 lemma add_less_imp_less_right:  haftmann@25062  651  "a + c < b + c \ a < b"  obua@14738  652 apply (rule add_less_imp_less_left [of c])  hoelzl@62376  653 apply (simp add: add.commute)  obua@14738  654 done  obua@14738  655 obua@14738  656 lemma add_less_cancel_left [simp]:  haftmann@25062  657  "c + a < c + b \ a < b"  hoelzl@62376  658  by (blast intro: add_less_imp_less_left add_strict_left_mono)  obua@14738  659 obua@14738  660 lemma add_less_cancel_right [simp]:  haftmann@25062  661  "a + c < b + c \ a < b"  haftmann@54230  662  by (blast intro: add_less_imp_less_right add_strict_right_mono)  obua@14738  663 obua@14738  664 lemma add_le_cancel_left [simp]:  haftmann@25062  665  "c + a \ c + b \ a \ b"  hoelzl@62376  666  by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono)  obua@14738  667 obua@14738  668 lemma add_le_cancel_right [simp]:  haftmann@25062  669  "a + c \ b + c \ a \ b"  haftmann@57512  670  by (simp add: add.commute [of a c] add.commute [of b c])  obua@14738  671 obua@14738  672 lemma add_le_imp_le_right:  haftmann@25062  673  "a + c \ b + c \ a \ b"  nipkow@29667  674 by simp  haftmann@25062  675 haftmann@25077  676 lemma max_add_distrib_left:  haftmann@25077  677  "max x y + z = max (x + z) (y + z)"  haftmann@25077  678  unfolding max_def by auto  haftmann@25077  679 haftmann@25077  680 lemma min_add_distrib_left:  haftmann@25077  681  "min x y + z = min (x + z) (y + z)"  haftmann@25077  682  unfolding min_def by auto  haftmann@25077  683 huffman@44848  684 lemma max_add_distrib_right:  huffman@44848  685  "x + max y z = max (x + y) (x + z)"  huffman@44848  686  unfolding max_def by auto  huffman@44848  687 huffman@44848  688 lemma min_add_distrib_right:  huffman@44848  689  "x + min y z = min (x + y) (x + z)"  huffman@44848  690  unfolding min_def by auto  huffman@44848  691 haftmann@25062  692 end  haftmann@25062  693 hoelzl@62376  694 subsection \Support for reasoning about signs\  hoelzl@62376  695 hoelzl@62376  696 class ordered_comm_monoid_add = comm_monoid_add + ordered_ab_semigroup_add  hoelzl@62376  697 begin  hoelzl@62376  698 hoelzl@62376  699 lemma add_nonneg_nonneg [simp]:  hoelzl@62377  700  "0 \ a \ 0 \ b \ 0 \ a + b"  hoelzl@62377  701  using add_mono[of 0 a 0 b] by simp  hoelzl@62376  702 hoelzl@62376  703 lemma add_nonpos_nonpos:  hoelzl@62377  704  "a \ 0 \ b \ 0 \ a + b \ 0"  hoelzl@62377  705  using add_mono[of a 0 b 0] by simp  hoelzl@62376  706 hoelzl@62376  707 lemma add_nonneg_eq_0_iff:  hoelzl@62377  708  "0 \ x \ 0 \ y \ x + y = 0 \ x = 0 \ y = 0"  hoelzl@62377  709  using add_left_mono[of 0 y x] add_right_mono[of 0 x y] by auto  hoelzl@62377  710 hoelzl@62377  711 lemma add_nonpos_eq_0_iff:  hoelzl@62377  712  "x \ 0 \ y \ 0 \ x + y = 0 \ x = 0 \ y = 0"  hoelzl@62377  713  using add_left_mono[of y 0 x] add_right_mono[of x 0 y] by auto  hoelzl@62376  714 hoelzl@62376  715 lemma add_increasing:  hoelzl@62376  716  "0 \ a \ b \ c \ b \ a + c"  hoelzl@62376  717  by (insert add_mono [of 0 a b c], simp)  hoelzl@62376  718 hoelzl@62376  719 lemma add_increasing2:  hoelzl@62376  720  "0 \ c \ b \ a \ b \ a + c"  hoelzl@62376  721  by (simp add: add_increasing add.commute [of a])  hoelzl@62376  722 hoelzl@62377  723 lemma add_decreasing:  hoelzl@62377  724  "a \ 0 \ c \ b \ a + c \ b"  hoelzl@62377  725  using add_mono[of a 0 c b] by simp  haftmann@52289  726 hoelzl@62377  727 lemma add_decreasing2:  hoelzl@62377  728  "c \ 0 \ a \ b \ a + c \ b"  hoelzl@62377  729  using add_mono[of a b c 0] by simp  haftmann@52289  730 hoelzl@62377  731 lemma add_pos_nonneg: "0 < a \ 0 \ b \ 0 < a + b"  hoelzl@62377  732  using less_le_trans[of 0 a "a + b"] by (simp add: add_increasing2)  haftmann@52289  733 hoelzl@62377  734 lemma add_pos_pos: "0 < a \ 0 < b \ 0 < a + b"  hoelzl@62377  735  by (intro add_pos_nonneg less_imp_le)  haftmann@52289  736 hoelzl@62377  737 lemma add_nonneg_pos: "0 \ a \ 0 < b \ 0 < a + b"  hoelzl@62377  738  using add_pos_nonneg[of b a] by (simp add: add_commute)  hoelzl@62376  739 hoelzl@62377  740 lemma add_neg_nonpos: "a < 0 \ b \ 0 \ a + b < 0"  hoelzl@62377  741  using le_less_trans[of "a + b" a 0] by (simp add: add_decreasing2)  haftmann@25303  742 hoelzl@62377  743 lemma add_neg_neg: "a < 0 \ b < 0 \ a + b < 0"  hoelzl@62377  744  by (intro add_neg_nonpos less_imp_le)  haftmann@25303  745 hoelzl@62377  746 lemma add_nonpos_neg: "a \ 0 \ b < 0 \ a + b < 0"  hoelzl@62377  747  using add_neg_nonpos[of b a] by (simp add: add_commute)  haftmann@25303  748 huffman@30691  749 lemmas add_sign_intros =  huffman@30691  750  add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg  huffman@30691  751  add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos  huffman@30691  752 hoelzl@62377  753 end  hoelzl@62377  754 hoelzl@62377  755 class strict_ordered_comm_monoid_add = comm_monoid_add + strict_ordered_ab_semigroup_add  hoelzl@62378  756 begin  hoelzl@62378  757 hoelzl@62378  758 lemma pos_add_strict:  hoelzl@62378  759  shows "0 < a \ b < c \ b < a + c"  hoelzl@62378  760  using add_strict_mono [of 0 a b c] by simp  hoelzl@62378  761 hoelzl@62378  762 end  hoelzl@62377  763 hoelzl@62377  764 class ordered_cancel_comm_monoid_add = ordered_comm_monoid_add + cancel_ab_semigroup_add  hoelzl@62377  765 begin  hoelzl@62377  766 hoelzl@62377  767 subclass ordered_cancel_ab_semigroup_add ..  hoelzl@62377  768 subclass strict_ordered_comm_monoid_add ..  hoelzl@62377  769 haftmann@54230  770 lemma add_strict_increasing:  haftmann@54230  771  "0 < a \ b \ c \ b < a + c"  haftmann@54230  772  by (insert add_less_le_mono [of 0 a b c], simp)  haftmann@54230  773 haftmann@54230  774 lemma add_strict_increasing2:  haftmann@54230  775  "0 \ a \ b < c \ b < a + c"  haftmann@54230  776  by (insert add_le_less_mono [of 0 a b c], simp)  haftmann@54230  777 haftmann@25303  778 end  haftmann@25303  779 hoelzl@62376  780 class ordered_ab_group_add = ab_group_add + ordered_ab_semigroup_add  haftmann@25062  781 begin  haftmann@25062  782 haftmann@35028  783 subclass ordered_cancel_ab_semigroup_add ..  haftmann@25062  784 haftmann@35028  785 subclass ordered_ab_semigroup_add_imp_le  haftmann@28823  786 proof  haftmann@25062  787  fix a b c :: 'a  haftmann@25062  788  assume "c + a \ c + b"  haftmann@25062  789  hence "(-c) + (c + a) \ (-c) + (c + b)" by (rule add_left_mono)  haftmann@57512  790  hence "((-c) + c) + a \ ((-c) + c) + b" by (simp only: add.assoc)  haftmann@25062  791  thus "a \ b" by simp  haftmann@25062  792 qed  haftmann@25062  793 hoelzl@62376  794 subclass ordered_cancel_comm_monoid_add ..  haftmann@25303  795 haftmann@54230  796 lemma add_less_same_cancel1 [simp]:  haftmann@54230  797  "b + a < b \ a < 0"  haftmann@54230  798  using add_less_cancel_left [of _ _ 0] by simp  haftmann@54230  799 haftmann@54230  800 lemma add_less_same_cancel2 [simp]:  haftmann@54230  801  "a + b < b \ a < 0"  haftmann@54230  802  using add_less_cancel_right [of _ _ 0] by simp  haftmann@54230  803 haftmann@54230  804 lemma less_add_same_cancel1 [simp]:  haftmann@54230  805  "a < a + b \ 0 < b"  haftmann@54230  806  using add_less_cancel_left [of _ 0] by simp  haftmann@54230  807 haftmann@54230  808 lemma less_add_same_cancel2 [simp]:  haftmann@54230  809  "a < b + a \ 0 < b"  haftmann@54230  810  using add_less_cancel_right [of 0] by simp  haftmann@54230  811 haftmann@54230  812 lemma add_le_same_cancel1 [simp]:  haftmann@54230  813  "b + a \ b \ a \ 0"  haftmann@54230  814  using add_le_cancel_left [of _ _ 0] by simp  haftmann@54230  815 haftmann@54230  816 lemma add_le_same_cancel2 [simp]:  haftmann@54230  817  "a + b \ b \ a \ 0"  haftmann@54230  818  using add_le_cancel_right [of _ _ 0] by simp  haftmann@54230  819 haftmann@54230  820 lemma le_add_same_cancel1 [simp]:  haftmann@54230  821  "a \ a + b \ 0 \ b"  haftmann@54230  822  using add_le_cancel_left [of _ 0] by simp  haftmann@54230  823 haftmann@54230  824 lemma le_add_same_cancel2 [simp]:  haftmann@54230  825  "a \ b + a \ 0 \ b"  haftmann@54230  826  using add_le_cancel_right [of 0] by simp  haftmann@54230  827 haftmann@25077  828 lemma max_diff_distrib_left:  haftmann@25077  829  shows "max x y - z = max (x - z) (y - z)"  haftmann@54230  830  using max_add_distrib_left [of x y "- z"] by simp  haftmann@25077  831 haftmann@25077  832 lemma min_diff_distrib_left:  haftmann@25077  833  shows "min x y - z = min (x - z) (y - z)"  haftmann@54230  834  using min_add_distrib_left [of x y "- z"] by simp  haftmann@25077  835 haftmann@25077  836 lemma le_imp_neg_le:  nipkow@29667  837  assumes "a \ b" shows "-b \ -a"  haftmann@25077  838 proof -  hoelzl@62376  839  have "-a+a \ -a+b" using \a \ b\ by (rule add_left_mono)  haftmann@54230  840  then have "0 \ -a+b" by simp  hoelzl@62376  841  then have "0 + (-b) \ (-a + b) + (-b)" by (rule add_right_mono)  haftmann@54230  842  then show ?thesis by (simp add: algebra_simps)  haftmann@25077  843 qed  haftmann@25077  844 haftmann@25077  845 lemma neg_le_iff_le [simp]: "- b \ - a \ a \ b"  hoelzl@62376  846 proof  haftmann@25077  847  assume "- b \ - a"  nipkow@29667  848  hence "- (- a) \ - (- b)" by (rule le_imp_neg_le)  haftmann@25077  849  thus "a\b" by simp  haftmann@25077  850 next  haftmann@25077  851  assume "a\b"  haftmann@25077  852  thus "-b \ -a" by (rule le_imp_neg_le)  haftmann@25077  853 qed  haftmann@25077  854 haftmann@25077  855 lemma neg_le_0_iff_le [simp]: "- a \ 0 \ 0 \ a"  nipkow@29667  856 by (subst neg_le_iff_le [symmetric], simp)  haftmann@25077  857 haftmann@25077  858 lemma neg_0_le_iff_le [simp]: "0 \ - a \ a \ 0"  nipkow@29667  859 by (subst neg_le_iff_le [symmetric], simp)  haftmann@25077  860 haftmann@25077  861 lemma neg_less_iff_less [simp]: "- b < - a \ a < b"  hoelzl@62376  862 by (force simp add: less_le)  haftmann@25077  863 haftmann@25077  864 lemma neg_less_0_iff_less [simp]: "- a < 0 \ 0 < a"  nipkow@29667  865 by (subst neg_less_iff_less [symmetric], simp)  haftmann@25077  866 haftmann@25077  867 lemma neg_0_less_iff_less [simp]: "0 < - a \ a < 0"  nipkow@29667  868 by (subst neg_less_iff_less [symmetric], simp)  haftmann@25077  869 wenzelm@60758  870 text\The next several equations can make the simplifier loop!\  haftmann@25077  871 haftmann@25077  872 lemma less_minus_iff: "a < - b \ b < - a"  haftmann@25077  873 proof -  haftmann@25077  874  have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)  haftmann@25077  875  thus ?thesis by simp  haftmann@25077  876 qed  haftmann@25077  877 haftmann@25077  878 lemma minus_less_iff: "- a < b \ - b < a"  haftmann@25077  879 proof -  haftmann@25077  880  have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)  haftmann@25077  881  thus ?thesis by simp  haftmann@25077  882 qed  haftmann@25077  883 haftmann@25077  884 lemma le_minus_iff: "a \ - b \ b \ - a"  haftmann@25077  885 proof -  haftmann@25077  886  have mm: "!! a (b::'a). (-(-a)) < -b \ -(-b) < -a" by (simp only: minus_less_iff)  hoelzl@62376  887  have "(- (- a) <= -b) = (b <= - a)"  haftmann@25077  888  apply (auto simp only: le_less)  haftmann@25077  889  apply (drule mm)  haftmann@25077  890  apply (simp_all)  haftmann@25077  891  apply (drule mm[simplified], assumption)  haftmann@25077  892  done  haftmann@25077  893  then show ?thesis by simp  haftmann@25077  894 qed  haftmann@25077  895 haftmann@25077  896 lemma minus_le_iff: "- a \ b \ - b \ a"  nipkow@29667  897 by (auto simp add: le_less minus_less_iff)  haftmann@25077  898 blanchet@54148  899 lemma diff_less_0_iff_less [simp]:  haftmann@37884  900  "a - b < 0 \ a < b"  haftmann@25077  901 proof -  haftmann@54230  902  have "a - b < 0 \ a + (- b) < b + (- b)" by simp  haftmann@37884  903  also have "... \ a < b" by (simp only: add_less_cancel_right)  haftmann@25077  904  finally show ?thesis .  haftmann@25077  905 qed  haftmann@25077  906 haftmann@37884  907 lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric]  haftmann@37884  908 haftmann@54230  909 lemma diff_less_eq [algebra_simps, field_simps]:  haftmann@54230  910  "a - b < c \ a < c + b"  haftmann@25077  911 apply (subst less_iff_diff_less_0 [of a])  haftmann@25077  912 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])  haftmann@54230  913 apply (simp add: algebra_simps)  haftmann@25077  914 done  haftmann@25077  915 haftmann@54230  916 lemma less_diff_eq[algebra_simps, field_simps]:  haftmann@54230  917  "a < c - b \ a + b < c"  haftmann@36302  918 apply (subst less_iff_diff_less_0 [of "a + b"])  haftmann@25077  919 apply (subst less_iff_diff_less_0 [of a])  haftmann@54230  920 apply (simp add: algebra_simps)  haftmann@25077  921 done  haftmann@25077  922 haftmann@62348  923 lemma diff_gt_0_iff_gt [simp]:  haftmann@62348  924  "a - b > 0 \ a > b"  haftmann@62348  925  by (simp add: less_diff_eq)  lp15@61762  926 haftmann@62348  927 lemma diff_le_eq [algebra_simps, field_simps]:  haftmann@62348  928  "a - b \ c \ a \ c + b"  haftmann@62348  929  by (auto simp add: le_less diff_less_eq )  haftmann@25077  930 haftmann@62348  931 lemma le_diff_eq [algebra_simps, field_simps]:  haftmann@62348  932  "a \ c - b \ a + b \ c"  haftmann@62348  933  by (auto simp add: le_less less_diff_eq)  haftmann@25077  934 blanchet@54148  935 lemma diff_le_0_iff_le [simp]:  haftmann@37884  936  "a - b \ 0 \ a \ b"  haftmann@37884  937  by (simp add: algebra_simps)  haftmann@37884  938 haftmann@37884  939 lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric]  haftmann@37884  940 haftmann@62348  941 lemma diff_ge_0_iff_ge [simp]:  haftmann@62348  942  "a - b \ 0 \ a \ b"  haftmann@62348  943  by (simp add: le_diff_eq)  haftmann@62348  944 haftmann@37884  945 lemma diff_eq_diff_less:  haftmann@37884  946  "a - b = c - d \ a < b \ c < d"  haftmann@37884  947  by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d])  haftmann@37884  948 haftmann@37889  949 lemma diff_eq_diff_less_eq:  haftmann@37889  950  "a - b = c - d \ a \ b \ c \ d"  haftmann@37889  951  by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d])  haftmann@25077  952 hoelzl@56950  953 lemma diff_mono: "a \ b \ d \ c \ a - c \ b - d"  hoelzl@56950  954  by (simp add: field_simps add_mono)  hoelzl@56950  955 hoelzl@56950  956 lemma diff_left_mono: "b \ a \ c - a \ c - b"  hoelzl@56950  957  by (simp add: field_simps)  hoelzl@56950  958 hoelzl@56950  959 lemma diff_right_mono: "a \ b \ a - c \ b - c"  hoelzl@56950  960  by (simp add: field_simps)  hoelzl@56950  961 hoelzl@56950  962 lemma diff_strict_mono: "a < b \ d < c \ a - c < b - d"  hoelzl@56950  963  by (simp add: field_simps add_strict_mono)  hoelzl@56950  964 hoelzl@56950  965 lemma diff_strict_left_mono: "b < a \ c - a < c - b"  hoelzl@56950  966  by (simp add: field_simps)  hoelzl@56950  967 hoelzl@56950  968 lemma diff_strict_right_mono: "a < b \ a - c < b - c"  hoelzl@56950  969  by (simp add: field_simps)  hoelzl@56950  970 haftmann@25077  971 end  haftmann@25077  972 wenzelm@48891  973 ML_file "Tools/group_cancel.ML"  huffman@48556  974 huffman@48556  975 simproc_setup group_cancel_add ("a + b::'a::ab_group_add") =  wenzelm@60758  976  \fn phi => fn ss => try Group_Cancel.cancel_add_conv\  huffman@48556  977 huffman@48556  978 simproc_setup group_cancel_diff ("a - b::'a::ab_group_add") =  wenzelm@60758  979  \fn phi => fn ss => try Group_Cancel.cancel_diff_conv\  haftmann@37884  980 huffman@48556  981 simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") =  wenzelm@60758  982  \fn phi => fn ss => try Group_Cancel.cancel_eq_conv\  haftmann@37889  983 huffman@48556  984 simproc_setup group_cancel_le ("a \ (b::'a::ordered_ab_group_add)") =  wenzelm@60758  985  \fn phi => fn ss => try Group_Cancel.cancel_le_conv\  huffman@48556  986 huffman@48556  987 simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") =  wenzelm@60758  988  \fn phi => fn ss => try Group_Cancel.cancel_less_conv\  haftmann@37884  989 haftmann@35028  990 class linordered_ab_semigroup_add =  haftmann@35028  991  linorder + ordered_ab_semigroup_add  haftmann@25062  992 haftmann@35028  993 class linordered_cancel_ab_semigroup_add =  haftmann@35028  994  linorder + ordered_cancel_ab_semigroup_add  haftmann@25267  995 begin  haftmann@25062  996 haftmann@35028  997 subclass linordered_ab_semigroup_add ..  haftmann@25062  998 haftmann@35028  999 subclass ordered_ab_semigroup_add_imp_le  haftmann@28823  1000 proof  haftmann@25062  1001  fix a b c :: 'a  hoelzl@62376  1002  assume le: "c + a <= c + b"  haftmann@25062  1003  show "a <= b"  haftmann@25062  1004  proof (rule ccontr)  haftmann@25062  1005  assume w: "~ a \ b"  haftmann@25062  1006  hence "b <= a" by (simp add: linorder_not_le)  haftmann@25062  1007  hence le2: "c + b <= c + a" by (rule add_left_mono)  hoelzl@62376  1008  have "a = b"  haftmann@25062  1009  apply (insert le)  haftmann@25062  1010  apply (insert le2)  haftmann@25062  1011  apply (drule antisym, simp_all)  haftmann@25062  1012  done  hoelzl@62376  1013  with w show False  haftmann@25062  1014  by (simp add: linorder_not_le [symmetric])  haftmann@25062  1015  qed  haftmann@25062  1016 qed  haftmann@25062  1017 haftmann@25267  1018 end  haftmann@25267  1019 haftmann@35028  1020 class linordered_ab_group_add = linorder + ordered_ab_group_add  haftmann@25267  1021 begin  haftmann@25230  1022 haftmann@35028  1023 subclass linordered_cancel_ab_semigroup_add ..  haftmann@25230  1024 haftmann@35036  1025 lemma equal_neg_zero [simp]:  haftmann@25303  1026  "a = - a \ a = 0"  haftmann@25303  1027 proof  haftmann@25303  1028  assume "a = 0" then show "a = - a" by simp  haftmann@25303  1029 next  haftmann@25303  1030  assume A: "a = - a" show "a = 0"  haftmann@25303  1031  proof (cases "0 \ a")  haftmann@25303  1032  case True with A have "0 \ - a" by auto  haftmann@25303  1033  with le_minus_iff have "a \ 0" by simp  haftmann@25303  1034  with True show ?thesis by (auto intro: order_trans)  haftmann@25303  1035  next  haftmann@25303  1036  case False then have B: "a \ 0" by auto  haftmann@25303  1037  with A have "- a \ 0" by auto  haftmann@25303  1038  with B show ?thesis by (auto intro: order_trans)  haftmann@25303  1039  qed  haftmann@25303  1040 qed  haftmann@25303  1041 haftmann@35036  1042 lemma neg_equal_zero [simp]:  haftmann@25303  1043  "- a = a \ a = 0"  haftmann@35036  1044  by (auto dest: sym)  haftmann@35036  1045 haftmann@54250  1046 lemma neg_less_eq_nonneg [simp]:  haftmann@54250  1047  "- a \ a \ 0 \ a"  haftmann@54250  1048 proof  haftmann@54250  1049  assume A: "- a \ a" show "0 \ a"  haftmann@54250  1050  proof (rule classical)  haftmann@54250  1051  assume "\ 0 \ a"  haftmann@54250  1052  then have "a < 0" by auto  haftmann@54250  1053  with A have "- a < 0" by (rule le_less_trans)  haftmann@54250  1054  then show ?thesis by auto  haftmann@54250  1055  qed  haftmann@54250  1056 next  haftmann@54250  1057  assume A: "0 \ a" show "- a \ a"  haftmann@54250  1058  proof (rule order_trans)  haftmann@54250  1059  show "- a \ 0" using A by (simp add: minus_le_iff)  haftmann@54250  1060  next  haftmann@54250  1061  show "0 \ a" using A .  haftmann@54250  1062  qed  haftmann@54250  1063 qed  haftmann@54250  1064 haftmann@54250  1065 lemma neg_less_pos [simp]:  haftmann@54250  1066  "- a < a \ 0 < a"  haftmann@54250  1067  by (auto simp add: less_le)  haftmann@54250  1068 haftmann@54250  1069 lemma less_eq_neg_nonpos [simp]:  haftmann@54250  1070  "a \ - a \ a \ 0"  haftmann@54250  1071  using neg_less_eq_nonneg [of "- a"] by simp  haftmann@54250  1072 haftmann@54250  1073 lemma less_neg_neg [simp]:  haftmann@54250  1074  "a < - a \ a < 0"  haftmann@54250  1075  using neg_less_pos [of "- a"] by simp  haftmann@54250  1076 haftmann@35036  1077 lemma double_zero [simp]:  haftmann@35036  1078  "a + a = 0 \ a = 0"  haftmann@35036  1079 proof  haftmann@35036  1080  assume assm: "a + a = 0"  haftmann@35036  1081  then have a: "- a = a" by (rule minus_unique)  huffman@35216  1082  then show "a = 0" by (simp only: neg_equal_zero)  haftmann@35036  1083 qed simp  haftmann@35036  1084 haftmann@35036  1085 lemma double_zero_sym [simp]:  haftmann@35036  1086  "0 = a + a \ a = 0"  haftmann@35036  1087  by (rule, drule sym) simp_all  haftmann@35036  1088 haftmann@35036  1089 lemma zero_less_double_add_iff_zero_less_single_add [simp]:  haftmann@35036  1090  "0 < a + a \ 0 < a"  haftmann@35036  1091 proof  haftmann@35036  1092  assume "0 < a + a"  haftmann@35036  1093  then have "0 - a < a" by (simp only: diff_less_eq)  haftmann@35036  1094  then have "- a < a" by simp  haftmann@54250  1095  then show "0 < a" by simp  haftmann@35036  1096 next  haftmann@35036  1097  assume "0 < a"  haftmann@35036  1098  with this have "0 + 0 < a + a"  haftmann@35036  1099  by (rule add_strict_mono)  haftmann@35036  1100  then show "0 < a + a" by simp  haftmann@35036  1101 qed  haftmann@35036  1102 haftmann@35036  1103 lemma zero_le_double_add_iff_zero_le_single_add [simp]:  haftmann@35036  1104  "0 \ a + a \ 0 \ a"  haftmann@35036  1105  by (auto simp add: le_less)  haftmann@35036  1106 haftmann@35036  1107 lemma double_add_less_zero_iff_single_add_less_zero [simp]:  haftmann@35036  1108  "a + a < 0 \ a < 0"  haftmann@35036  1109 proof -  haftmann@35036  1110  have "\ a + a < 0 \ \ a < 0"  haftmann@35036  1111  by (simp add: not_less)  haftmann@35036  1112  then show ?thesis by simp  haftmann@35036  1113 qed  haftmann@35036  1114 haftmann@35036  1115 lemma double_add_le_zero_iff_single_add_le_zero [simp]:  hoelzl@62376  1116  "a + a \ 0 \ a \ 0"  haftmann@35036  1117 proof -  haftmann@35036  1118  have "\ a + a \ 0 \ \ a \ 0"  haftmann@35036  1119  by (simp add: not_le)  haftmann@35036  1120  then show ?thesis by simp  haftmann@35036  1121 qed  haftmann@35036  1122 haftmann@35036  1123 lemma minus_max_eq_min:  haftmann@35036  1124  "- max x y = min (-x) (-y)"  haftmann@35036  1125  by (auto simp add: max_def min_def)  haftmann@35036  1126 haftmann@35036  1127 lemma minus_min_eq_max:  haftmann@35036  1128  "- min x y = max (-x) (-y)"  haftmann@35036  1129  by (auto simp add: max_def min_def)  haftmann@25303  1130 haftmann@25267  1131 end  haftmann@25267  1132 haftmann@35092  1133 class abs =  wenzelm@61944  1134  fixes abs :: "'a \ 'a" ("\_\")  haftmann@35092  1135 haftmann@35092  1136 class sgn =  haftmann@35092  1137  fixes sgn :: "'a \ 'a"  haftmann@35092  1138 haftmann@35092  1139 class abs_if = minus + uminus + ord + zero + abs +  haftmann@35092  1140  assumes abs_if: "\a\ = (if a < 0 then - a else a)"  haftmann@35092  1141 haftmann@35092  1142 class sgn_if = minus + uminus + zero + one + ord + sgn +  haftmann@35092  1143  assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"  haftmann@35092  1144 begin  haftmann@35092  1145 haftmann@35092  1146 lemma sgn0 [simp]: "sgn 0 = 0"  haftmann@35092  1147  by (simp add:sgn_if)  haftmann@35092  1148 haftmann@35092  1149 end  obua@14738  1150 haftmann@35028  1151 class ordered_ab_group_add_abs = ordered_ab_group_add + abs +  haftmann@25303  1152  assumes abs_ge_zero [simp]: "\a\ \ 0"  haftmann@25303  1153  and abs_ge_self: "a \ \a\"  haftmann@25303  1154  and abs_leI: "a \ b \ - a \ b \ \a\ \ b"  haftmann@25303  1155  and abs_minus_cancel [simp]: "\-a\ = \a\"  haftmann@25303  1156  and abs_triangle_ineq: "\a + b\ \ \a\ + \b\"  haftmann@25303  1157 begin  haftmann@25303  1158 haftmann@25307  1159 lemma abs_minus_le_zero: "- \a\ \ 0"  haftmann@25307  1160  unfolding neg_le_0_iff_le by simp  haftmann@25307  1161 haftmann@25307  1162 lemma abs_of_nonneg [simp]:  nipkow@29667  1163  assumes nonneg: "0 \ a" shows "\a\ = a"  haftmann@25307  1164 proof (rule antisym)  haftmann@25307  1165  from nonneg le_imp_neg_le have "- a \ 0" by simp  haftmann@25307  1166  from this nonneg have "- a \ a" by (rule order_trans)  haftmann@25307  1167  then show "\a\ \ a" by (auto intro: abs_leI)  haftmann@25307  1168 qed (rule abs_ge_self)  haftmann@25307  1169 haftmann@25307  1170 lemma abs_idempotent [simp]: "\\a\\ = \a\"  nipkow@29667  1171 by (rule antisym)  haftmann@36302  1172  (auto intro!: abs_ge_self abs_leI order_trans [of "- \a\" 0 "\a\"])  haftmann@25307  1173 haftmann@25307  1174 lemma abs_eq_0 [simp]: "\a\ = 0 \ a = 0"  haftmann@25307  1175 proof -  haftmann@25307  1176  have "\a\ = 0 \ a = 0"  haftmann@25307  1177  proof (rule antisym)  haftmann@25307  1178  assume zero: "\a\ = 0"  haftmann@25307  1179  with abs_ge_self show "a \ 0" by auto  haftmann@25307  1180  from zero have "\-a\ = 0" by simp  haftmann@36302  1181  with abs_ge_self [of "- a"] have "- a \ 0" by auto  haftmann@25307  1182  with neg_le_0_iff_le show "0 \ a" by auto  haftmann@25307  1183  qed  haftmann@25307  1184  then show ?thesis by auto  haftmann@25307  1185 qed  haftmann@25307  1186 haftmann@25303  1187 lemma abs_zero [simp]: "\0\ = 0"  nipkow@29667  1188 by simp  avigad@16775  1189 blanchet@54148  1190 lemma abs_0_eq [simp]: "0 = \a\ \ a = 0"  haftmann@25303  1191 proof -  haftmann@25303  1192  have "0 = \a\ \ \a\ = 0" by (simp only: eq_ac)  haftmann@25303  1193  thus ?thesis by simp  haftmann@25303  1194 qed  haftmann@25303  1195 hoelzl@62376  1196 lemma abs_le_zero_iff [simp]: "\a\ \ 0 \ a = 0"  haftmann@25303  1197 proof  haftmann@25303  1198  assume "\a\ \ 0"  haftmann@25303  1199  then have "\a\ = 0" by (rule antisym) simp  haftmann@25303  1200  thus "a = 0" by simp  haftmann@25303  1201 next  haftmann@25303  1202  assume "a = 0"  haftmann@25303  1203  thus "\a\ \ 0" by simp  haftmann@25303  1204 qed  haftmann@25303  1205 lp15@62379  1206 lemma abs_le_self_iff [simp]: "\a\ \ a \ 0 \ a"  lp15@62379  1207 proof -  lp15@62379  1208  have "\a. (0::'a) \ \a\"  lp15@62379  1209  using abs_ge_zero by blast  lp15@62379  1210  then have "\a\ \ a \ 0 \ a"  lp15@62379  1211  using order.trans by blast  lp15@62379  1212  then show ?thesis  lp15@62379  1213  using abs_of_nonneg eq_refl by blast  lp15@62379  1214 qed  lp15@62379  1215 haftmann@25303  1216 lemma zero_less_abs_iff [simp]: "0 < \a\ \ a \ 0"  nipkow@29667  1217 by (simp add: less_le)  haftmann@25303  1218 haftmann@25303  1219 lemma abs_not_less_zero [simp]: "\ \a\ < 0"  haftmann@25303  1220 proof -  haftmann@25303  1221  have a: "\x y. x \ y \ \ y < x" by auto  haftmann@25303  1222  show ?thesis by (simp add: a)  haftmann@25303  1223 qed  avigad@16775  1224 haftmann@25303  1225 lemma abs_ge_minus_self: "- a \ \a\"  haftmann@25303  1226 proof -  haftmann@25303  1227  have "- a \ \-a\" by (rule abs_ge_self)  haftmann@25303  1228  then show ?thesis by simp  haftmann@25303  1229 qed  haftmann@25303  1230 hoelzl@62376  1231 lemma abs_minus_commute:  haftmann@25303  1232  "\a - b\ = \b - a\"  haftmann@25303  1233 proof -  haftmann@25303  1234  have "\a - b\ = \- (a - b)\" by (simp only: abs_minus_cancel)  haftmann@25303  1235  also have "... = \b - a\" by simp  haftmann@25303  1236  finally show ?thesis .  haftmann@25303  1237 qed  haftmann@25303  1238 haftmann@25303  1239 lemma abs_of_pos: "0 < a \ \a\ = a"  nipkow@29667  1240 by (rule abs_of_nonneg, rule less_imp_le)  avigad@16775  1241 haftmann@25303  1242 lemma abs_of_nonpos [simp]:  nipkow@29667  1243  assumes "a \ 0" shows "\a\ = - a"  haftmann@25303  1244 proof -  haftmann@25303  1245  let ?b = "- a"  haftmann@25303  1246  have "- ?b \ 0 \ \- ?b\ = - (- ?b)"  haftmann@25303  1247  unfolding abs_minus_cancel [of "?b"]  haftmann@25303  1248  unfolding neg_le_0_iff_le [of "?b"]  haftmann@25303  1249  unfolding minus_minus by (erule abs_of_nonneg)  haftmann@25303  1250  then show ?thesis using assms by auto  haftmann@25303  1251 qed  hoelzl@62376  1252 haftmann@25303  1253 lemma abs_of_neg: "a < 0 \ \a\ = - a"  nipkow@29667  1254 by (rule abs_of_nonpos, rule less_imp_le)  haftmann@25303  1255 haftmann@25303  1256 lemma abs_le_D1: "\a\ \ b \ a \ b"  nipkow@29667  1257 by (insert abs_ge_self, blast intro: order_trans)  haftmann@25303  1258 haftmann@25303  1259 lemma abs_le_D2: "\a\ \ b \ - a \ b"  haftmann@36302  1260 by (insert abs_le_D1 [of "- a"], simp)  haftmann@25303  1261 haftmann@25303  1262 lemma abs_le_iff: "\a\ \ b \ a \ b \ - a \ b"  nipkow@29667  1263 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)  haftmann@25303  1264 haftmann@25303  1265 lemma abs_triangle_ineq2: "\a\ - \b\ \ \a - b\"  haftmann@36302  1266 proof -  haftmann@36302  1267  have "\a\ = \b + (a - b)\"  haftmann@54230  1268  by (simp add: algebra_simps)  haftmann@36302  1269  then have "\a\ \ \b\ + \a - b\"  haftmann@36302  1270  by (simp add: abs_triangle_ineq)  haftmann@36302  1271  then show ?thesis  haftmann@36302  1272  by (simp add: algebra_simps)  haftmann@36302  1273 qed  haftmann@36302  1274 haftmann@36302  1275 lemma abs_triangle_ineq2_sym: "\a\ - \b\ \ \b - a\"  haftmann@36302  1276  by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)  avigad@16775  1277 haftmann@25303  1278 lemma abs_triangle_ineq3: "\\a\ - \b\\ \ \a - b\"  haftmann@36302  1279  by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)  avigad@16775  1280 haftmann@25303  1281 lemma abs_triangle_ineq4: "\a - b\ \ \a\ + \b\"  haftmann@25303  1282 proof -  haftmann@54230  1283  have "\a - b\ = \a + - b\" by (simp add: algebra_simps)  haftmann@36302  1284  also have "... \ \a\ + \- b\" by (rule abs_triangle_ineq)  nipkow@29667  1285  finally show ?thesis by simp  haftmann@25303  1286 qed  avigad@16775  1287 haftmann@25303  1288 lemma abs_diff_triangle_ineq: "\a + b - (c + d)\ \ \a - c\ + \b - d\"  haftmann@25303  1289 proof -  haftmann@54230  1290  have "\a + b - (c+d)\ = \(a-c) + (b-d)\" by (simp add: algebra_simps)  haftmann@25303  1291  also have "... \ \a-c\ + \b-d\" by (rule abs_triangle_ineq)  haftmann@25303  1292  finally show ?thesis .  haftmann@25303  1293 qed  avigad@16775  1294 haftmann@25303  1295 lemma abs_add_abs [simp]:  haftmann@25303  1296  "\\a\ + \b\\ = \a\ + \b\" (is "?L = ?R")  haftmann@25303  1297 proof (rule antisym)  haftmann@25303  1298  show "?L \ ?R" by(rule abs_ge_self)  haftmann@25303  1299 next  haftmann@25303  1300  have "?L \ \\a\\ + \\b\\" by(rule abs_triangle_ineq)  haftmann@25303  1301  also have "\ = ?R" by simp  haftmann@25303  1302  finally show "?L \ ?R" .  haftmann@25303  1303 qed  haftmann@25303  1304 haftmann@25303  1305 end  obua@14738  1306 paulson@60762  1307 lemma dense_eq0_I:  paulson@60762  1308  fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"  paulson@60762  1309  shows "(\e. 0 < e \ \x\ \ e) ==> x = 0"  wenzelm@61944  1310  apply (cases "\x\ = 0", simp)  paulson@60762  1311  apply (simp only: zero_less_abs_iff [symmetric])  paulson@60762  1312  apply (drule dense)  paulson@60762  1313  apply (auto simp add: not_less [symmetric])  paulson@60762  1314  done  paulson@60762  1315 haftmann@59815  1316 hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus  haftmann@59815  1317 wenzelm@61799  1318 lemmas add_0 = add_0_left \ \FIXME duplicate\  wenzelm@61799  1319 lemmas mult_1 = mult_1_left \ \FIXME duplicate\  wenzelm@61799  1320 lemmas ab_left_minus = left_minus \ \FIXME duplicate\  wenzelm@61799  1321 lemmas diff_diff_eq = diff_diff_add \ \FIXME duplicate\  haftmann@59815  1322 hoelzl@62377  1323 subsection \Canonically ordered monoids\  hoelzl@62377  1324 hoelzl@62377  1325 text \Canonically ordered monoids are never groups.\  hoelzl@62377  1326 hoelzl@62377  1327 class canonically_ordered_monoid_add = comm_monoid_add + order +  hoelzl@62377  1328  assumes le_iff_add: "a \ b \ (\c. b = a + c)"  hoelzl@62377  1329 begin  hoelzl@62377  1330 hoelzl@62378  1331 lemma zero_le[simp]: "0 \ x"  hoelzl@62377  1332  by (auto simp: le_iff_add)  hoelzl@62377  1333 hoelzl@62378  1334 lemma le_zero_eq[simp]: "n \ 0 \ n = 0"  hoelzl@62378  1335  by (auto intro: antisym)  hoelzl@62378  1336 hoelzl@62378  1337 lemma not_less_zero[simp]: "\ n < 0"  hoelzl@62378  1338  by (auto simp: less_le)  hoelzl@62378  1339 hoelzl@62378  1340 lemma zero_less_iff_neq_zero: "(0 < n) \ (n \ 0)"  hoelzl@62378  1341  by (auto simp: less_le)  hoelzl@62378  1342 hoelzl@62378  1343 text \This theorem is useful with \blast\\  hoelzl@62378  1344 lemma gr_zeroI: "(n = 0 \ False) \ 0 < n"  hoelzl@62378  1345  by (rule zero_less_iff_neq_zero[THEN iffD2]) iprover  hoelzl@62378  1346 hoelzl@62378  1347 lemma not_gr_zero[simp]: "(\ (0 < n)) \ (n = 0)"  hoelzl@62378  1348  by (simp add: zero_less_iff_neq_zero)  hoelzl@62378  1349 hoelzl@62377  1350 subclass ordered_comm_monoid_add  hoelzl@62377  1351  proof qed (auto simp: le_iff_add add_ac)  hoelzl@62377  1352 hoelzl@62377  1353 lemma add_eq_0_iff_both_eq_0: "x + y = 0 \ x = 0 \ y = 0"  hoelzl@62377  1354  by (intro add_nonneg_eq_0_iff zero_le)  hoelzl@62377  1355 hoelzl@62378  1356 lemma gr_implies_not_zero: "m < n \ n \ 0"  hoelzl@62378  1357  using add_eq_0_iff_both_eq_0[of m] by (auto simp: le_iff_add less_le)  hoelzl@62378  1358 hoelzl@62378  1359 lemmas zero_order = zero_le le_zero_eq not_less_zero zero_less_iff_neq_zero not_gr_zero  hoelzl@62378  1360  -- \This should be attributed with \[iff]\, but then \blast\ fails in \Set\.\  hoelzl@62378  1361 hoelzl@62377  1362 end  hoelzl@62377  1363 hoelzl@62377  1364 class ordered_cancel_comm_monoid_diff =  hoelzl@62377  1365  canonically_ordered_monoid_add + comm_monoid_diff + ordered_ab_semigroup_add_imp_le  hoelzl@62377  1366 begin  hoelzl@62377  1367 hoelzl@62377  1368 context  hoelzl@62377  1369  fixes a b  hoelzl@62377  1370  assumes "a \ b"  hoelzl@62377  1371 begin  hoelzl@62377  1372 hoelzl@62377  1373 lemma add_diff_inverse:  hoelzl@62377  1374  "a + (b - a) = b"  hoelzl@62377  1375  using \a \ b\ by (auto simp add: le_iff_add)  hoelzl@62377  1376 hoelzl@62377  1377 lemma add_diff_assoc:  hoelzl@62377  1378  "c + (b - a) = c + b - a"  hoelzl@62377  1379  using \a \ b\ by (auto simp add: le_iff_add add.left_commute [of c])  hoelzl@62377  1380 hoelzl@62377  1381 lemma add_diff_assoc2:  hoelzl@62377  1382  "b - a + c = b + c - a"  hoelzl@62377  1383  using \a \ b\ by (auto simp add: le_iff_add add.assoc)  hoelzl@62377  1384 hoelzl@62377  1385 lemma diff_add_assoc:  hoelzl@62377  1386  "c + b - a = c + (b - a)"  hoelzl@62377  1387  using \a \ b\ by (simp add: add.commute add_diff_assoc)  hoelzl@62377  1388 hoelzl@62377  1389 lemma diff_add_assoc2:  hoelzl@62377  1390  "b + c - a = b - a + c"  hoelzl@62377  1391  using \a \ b\by (simp add: add.commute add_diff_assoc)  hoelzl@62377  1392 hoelzl@62377  1393 lemma diff_diff_right:  hoelzl@62377  1394  "c - (b - a) = c + a - b"  hoelzl@62377  1395  by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add.commute)  hoelzl@62377  1396 hoelzl@62377  1397 lemma diff_add:  hoelzl@62377  1398  "b - a + a = b"  hoelzl@62377  1399  by (simp add: add.commute add_diff_inverse)  hoelzl@62377  1400 hoelzl@62377  1401 lemma le_add_diff:  hoelzl@62377  1402  "c \ b + c - a"  hoelzl@62377  1403  by (auto simp add: add.commute diff_add_assoc2 le_iff_add)  hoelzl@62377  1404 hoelzl@62377  1405 lemma le_imp_diff_is_add:  hoelzl@62377  1406  "a \ b \ b - a = c \ b = c + a"  hoelzl@62377  1407  by (auto simp add: add.commute add_diff_inverse)  hoelzl@62377  1408 hoelzl@62377  1409 lemma le_diff_conv2:  hoelzl@62377  1410  "c \ b - a \ c + a \ b" (is "?P \ ?Q")  hoelzl@62377  1411 proof  hoelzl@62377  1412  assume ?P  hoelzl@62377  1413  then have "c + a \ b - a + a" by (rule add_right_mono)  hoelzl@62377  1414  then show ?Q by (simp add: add_diff_inverse add.commute)  hoelzl@62377  1415 next  hoelzl@62377  1416  assume ?Q  hoelzl@62377  1417  then have "a + c \ a + (b - a)" by (simp add: add_diff_inverse add.commute)  hoelzl@62377  1418  then show ?P by simp  hoelzl@62377  1419 qed  hoelzl@62377  1420 hoelzl@62377  1421 end  hoelzl@62377  1422 hoelzl@62377  1423 end  hoelzl@62377  1424 wenzelm@60758  1425 subsection \Tools setup\  haftmann@25090  1426 blanchet@54147  1427 lemma add_mono_thms_linordered_semiring:  wenzelm@61076  1428  fixes i j k :: "'a::ordered_ab_semigroup_add"  haftmann@25077  1429  shows "i \ j \ k \ l \ i + k \ j + l"  haftmann@25077  1430  and "i = j \ k \ l \ i + k \ j + l"  haftmann@25077  1431  and "i \ j \ k = l \ i + k \ j + l"  haftmann@25077  1432  and "i = j \ k = l \ i + k = j + l"  haftmann@25077  1433 by (rule add_mono, clarify+)+  haftmann@25077  1434 blanchet@54147  1435 lemma add_mono_thms_linordered_field:  wenzelm@61076  1436  fixes i j k :: "'a::ordered_cancel_ab_semigroup_add"  haftmann@25077  1437  shows "i < j \ k = l \ i + k < j + l"  haftmann@25077  1438  and "i = j \ k < l \ i + k < j + l"  haftmann@25077  1439  and "i < j \ k \ l \ i + k < j + l"  haftmann@25077  1440  and "i \ j \ k < l \ i + k < j + l"  haftmann@25077  1441  and "i < j \ k < l \ i + k < j + l"  haftmann@25077  1442 by (auto intro: add_strict_right_mono add_strict_left_mono  haftmann@25077  1443  add_less_le_mono add_le_less_mono add_strict_mono)  haftmann@25077  1444 haftmann@52435  1445 code_identifier  haftmann@52435  1446  code_module Groups \ (SML) Arith and (OCaml) Arith and (Haskell) Arith  haftmann@33364  1447 obua@14738  1448 end