src/HOL/ex/BinEx.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 28952 15a4b2cf8c34
child 31066 972c870da225
permissions -rw-r--r--
added lemmas
     1 (*  Title:      HOL/ex/BinEx.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1998  University of Cambridge
     4 *)
     5 
     6 header {* Binary arithmetic examples *}
     7 
     8 theory BinEx
     9 imports Complex_Main
    10 begin
    11 
    12 subsection {* Regression Testing for Cancellation Simprocs *}
    13 
    14 lemma "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
    15 apply simp  oops
    16 
    17 lemma "2*u = (u::int)"
    18 apply simp  oops
    19 
    20 lemma "(i + j + 12 + (k::int)) - 15 = y"
    21 apply simp  oops
    22 
    23 lemma "(i + j + 12 + (k::int)) - 5 = y"
    24 apply simp  oops
    25 
    26 lemma "y - b < (b::int)"
    27 apply simp  oops
    28 
    29 lemma "y - (3*b + c) < (b::int) - 2*c"
    30 apply simp  oops
    31 
    32 lemma "(2*x - (u*v) + y) - v*3*u = (w::int)"
    33 apply simp  oops
    34 
    35 lemma "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"
    36 apply simp  oops
    37 
    38 lemma "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"
    39 apply simp  oops
    40 
    41 lemma "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"
    42 apply simp  oops
    43 
    44 lemma "(i + j + 12 + (k::int)) = u + 15 + y"
    45 apply simp  oops
    46 
    47 lemma "(i + j*2 + 12 + (k::int)) = j + 5 + y"
    48 apply simp  oops
    49 
    50 lemma "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)"
    51 apply simp  oops
    52 
    53 lemma "a + -(b+c) + b = (d::int)"
    54 apply simp  oops
    55 
    56 lemma "a + -(b+c) - b = (d::int)"
    57 apply simp  oops
    58 
    59 (*negative numerals*)
    60 lemma "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"
    61 apply simp  oops
    62 
    63 lemma "(i + j + -3 + (k::int)) < u + 5 + y"
    64 apply simp  oops
    65 
    66 lemma "(i + j + 3 + (k::int)) < u + -6 + y"
    67 apply simp  oops
    68 
    69 lemma "(i + j + -12 + (k::int)) - 15 = y"
    70 apply simp  oops
    71 
    72 lemma "(i + j + 12 + (k::int)) - -15 = y"
    73 apply simp  oops
    74 
    75 lemma "(i + j + -12 + (k::int)) - -15 = y"
    76 apply simp  oops
    77 
    78 lemma "- (2*i) + 3  + (2*i + 4) = (0::int)"
    79 apply simp  oops
    80 
    81 
    82 
    83 subsection {* Arithmetic Method Tests *}
    84 
    85 
    86 lemma "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"
    87 by arith
    88 
    89 lemma "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)"
    90 by arith
    91 
    92 lemma "!!a::int. [| a < b; c < d |] ==> a+c+ 1 < b+d"
    93 by arith
    94 
    95 lemma "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"
    96 by arith
    97 
    98 lemma "!!a::int. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"
    99 by arith
   100 
   101 lemma "!!a::int. [| a+b < i+j; a<b; i<j |] ==> a+a - - -1 < j+j - 3"
   102 by arith
   103 
   104 lemma "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"
   105 by arith
   106 
   107 lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
   108       ==> a <= l"
   109 by arith
   110 
   111 lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
   112       ==> a+a+a+a <= l+l+l+l"
   113 by arith
   114 
   115 lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
   116       ==> a+a+a+a+a <= l+l+l+l+i"
   117 by arith
   118 
   119 lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
   120       ==> a+a+a+a+a+a <= l+l+l+l+i+l"
   121 by arith
   122 
   123 lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
   124       ==> 6*a <= 5*l+i"
   125 by arith
   126 
   127 
   128 
   129 subsection {* The Integers *}
   130 
   131 text {* Addition *}
   132 
   133 lemma "(13::int) + 19 = 32"
   134   by simp
   135 
   136 lemma "(1234::int) + 5678 = 6912"
   137   by simp
   138 
   139 lemma "(1359::int) + -2468 = -1109"
   140   by simp
   141 
   142 lemma "(93746::int) + -46375 = 47371"
   143   by simp
   144 
   145 
   146 text {* \medskip Negation *}
   147 
   148 lemma "- (65745::int) = -65745"
   149   by simp
   150 
   151 lemma "- (-54321::int) = 54321"
   152   by simp
   153 
   154 
   155 text {* \medskip Multiplication *}
   156 
   157 lemma "(13::int) * 19 = 247"
   158   by simp
   159 
   160 lemma "(-84::int) * 51 = -4284"
   161   by simp
   162 
   163 lemma "(255::int) * 255 = 65025"
   164   by simp
   165 
   166 lemma "(1359::int) * -2468 = -3354012"
   167   by simp
   168 
   169 lemma "(89::int) * 10 \<noteq> 889"
   170   by simp
   171 
   172 lemma "(13::int) < 18 - 4"
   173   by simp
   174 
   175 lemma "(-345::int) < -242 + -100"
   176   by simp
   177 
   178 lemma "(13557456::int) < 18678654"
   179   by simp
   180 
   181 lemma "(999999::int) \<le> (1000001 + 1) - 2"
   182   by simp
   183 
   184 lemma "(1234567::int) \<le> 1234567"
   185   by simp
   186 
   187 text{*No integer overflow!*}
   188 lemma "1234567 * (1234567::int) < 1234567*1234567*1234567"
   189   by simp
   190 
   191 
   192 text {* \medskip Quotient and Remainder *}
   193 
   194 lemma "(10::int) div 3 = 3"
   195   by simp
   196 
   197 lemma "(10::int) mod 3 = 1"
   198   by simp
   199 
   200 text {* A negative divisor *}
   201 
   202 lemma "(10::int) div -3 = -4"
   203   by simp
   204 
   205 lemma "(10::int) mod -3 = -2"
   206   by simp
   207 
   208 text {*
   209   A negative dividend\footnote{The definition agrees with mathematical
   210   convention and with ML, but not with the hardware of most computers}
   211 *}
   212 
   213 lemma "(-10::int) div 3 = -4"
   214   by simp
   215 
   216 lemma "(-10::int) mod 3 = 2"
   217   by simp
   218 
   219 text {* A negative dividend \emph{and} divisor *}
   220 
   221 lemma "(-10::int) div -3 = 3"
   222   by simp
   223 
   224 lemma "(-10::int) mod -3 = -1"
   225   by simp
   226 
   227 text {* A few bigger examples *}
   228 
   229 lemma "(8452::int) mod 3 = 1"
   230   by simp
   231 
   232 lemma "(59485::int) div 434 = 137"
   233   by simp
   234 
   235 lemma "(1000006::int) mod 10 = 6"
   236   by simp
   237 
   238 
   239 text {* \medskip Division by shifting *}
   240 
   241 lemma "10000000 div 2 = (5000000::int)"
   242   by simp
   243 
   244 lemma "10000001 mod 2 = (1::int)"
   245   by simp
   246 
   247 lemma "10000055 div 32 = (312501::int)"
   248   by simp
   249 
   250 lemma "10000055 mod 32 = (23::int)"
   251   by simp
   252 
   253 lemma "100094 div 144 = (695::int)"
   254   by simp
   255 
   256 lemma "100094 mod 144 = (14::int)"
   257   by simp
   258 
   259 
   260 text {* \medskip Powers *}
   261 
   262 lemma "2 ^ 10 = (1024::int)"
   263   by simp
   264 
   265 lemma "-3 ^ 7 = (-2187::int)"
   266   by simp
   267 
   268 lemma "13 ^ 7 = (62748517::int)"
   269   by simp
   270 
   271 lemma "3 ^ 15 = (14348907::int)"
   272   by simp
   273 
   274 lemma "-5 ^ 11 = (-48828125::int)"
   275   by simp
   276 
   277 
   278 subsection {* The Natural Numbers *}
   279 
   280 text {* Successor *}
   281 
   282 lemma "Suc 99999 = 100000"
   283   by (simp add: Suc_nat_number_of)
   284     -- {* not a default rewrite since sometimes we want to have @{text "Suc nnn"} *}
   285 
   286 
   287 text {* \medskip Addition *}
   288 
   289 lemma "(13::nat) + 19 = 32"
   290   by simp
   291 
   292 lemma "(1234::nat) + 5678 = 6912"
   293   by simp
   294 
   295 lemma "(973646::nat) + 6475 = 980121"
   296   by simp
   297 
   298 
   299 text {* \medskip Subtraction *}
   300 
   301 lemma "(32::nat) - 14 = 18"
   302   by simp
   303 
   304 lemma "(14::nat) - 15 = 0"
   305   by simp
   306 
   307 lemma "(14::nat) - 1576644 = 0"
   308   by simp
   309 
   310 lemma "(48273776::nat) - 3873737 = 44400039"
   311   by simp
   312 
   313 
   314 text {* \medskip Multiplication *}
   315 
   316 lemma "(12::nat) * 11 = 132"
   317   by simp
   318 
   319 lemma "(647::nat) * 3643 = 2357021"
   320   by simp
   321 
   322 
   323 text {* \medskip Quotient and Remainder *}
   324 
   325 lemma "(10::nat) div 3 = 3"
   326   by simp
   327 
   328 lemma "(10::nat) mod 3 = 1"
   329   by simp
   330 
   331 lemma "(10000::nat) div 9 = 1111"
   332   by simp
   333 
   334 lemma "(10000::nat) mod 9 = 1"
   335   by simp
   336 
   337 lemma "(10000::nat) div 16 = 625"
   338   by simp
   339 
   340 lemma "(10000::nat) mod 16 = 0"
   341   by simp
   342 
   343 
   344 text {* \medskip Powers *}
   345 
   346 lemma "2 ^ 12 = (4096::nat)"
   347   by simp
   348 
   349 lemma "3 ^ 10 = (59049::nat)"
   350   by simp
   351 
   352 lemma "12 ^ 7 = (35831808::nat)"
   353   by simp
   354 
   355 lemma "3 ^ 14 = (4782969::nat)"
   356   by simp
   357 
   358 lemma "5 ^ 11 = (48828125::nat)"
   359   by simp
   360 
   361 
   362 text {* \medskip Testing the cancellation of complementary terms *}
   363 
   364 lemma "y + (x + -x) = (0::int) + y"
   365   by simp
   366 
   367 lemma "y + (-x + (- y + x)) = (0::int)"
   368   by simp
   369 
   370 lemma "-x + (y + (- y + x)) = (0::int)"
   371   by simp
   372 
   373 lemma "x + (x + (- x + (- x + (- y + - z)))) = (0::int) - y - z"
   374   by simp
   375 
   376 lemma "x + x - x - x - y - z = (0::int) - y - z"
   377   by simp
   378 
   379 lemma "x + y + z - (x + z) = y - (0::int)"
   380   by simp
   381 
   382 lemma "x + (y + (y + (y + (-x + -x)))) = (0::int) + y - x + y + y"
   383   by simp
   384 
   385 lemma "x + (y + (y + (y + (-y + -x)))) = y + (0::int) + y"
   386   by simp
   387 
   388 lemma "x + y - x + z - x - y - z + x < (1::int)"
   389   by simp
   390 
   391 
   392 subsection{*Real Arithmetic*}
   393 
   394 subsubsection {*Addition *}
   395 
   396 lemma "(1359::real) + -2468 = -1109"
   397 by simp
   398 
   399 lemma "(93746::real) + -46375 = 47371"
   400 by simp
   401 
   402 
   403 subsubsection {*Negation *}
   404 
   405 lemma "- (65745::real) = -65745"
   406 by simp
   407 
   408 lemma "- (-54321::real) = 54321"
   409 by simp
   410 
   411 
   412 subsubsection {*Multiplication *}
   413 
   414 lemma "(-84::real) * 51 = -4284"
   415 by simp
   416 
   417 lemma "(255::real) * 255 = 65025"
   418 by simp
   419 
   420 lemma "(1359::real) * -2468 = -3354012"
   421 by simp
   422 
   423 
   424 subsubsection {*Inequalities *}
   425 
   426 lemma "(89::real) * 10 \<noteq> 889"
   427 by simp
   428 
   429 lemma "(13::real) < 18 - 4"
   430 by simp
   431 
   432 lemma "(-345::real) < -242 + -100"
   433 by simp
   434 
   435 lemma "(13557456::real) < 18678654"
   436 by simp
   437 
   438 lemma "(999999::real) \<le> (1000001 + 1) - 2"
   439 by simp
   440 
   441 lemma "(1234567::real) \<le> 1234567"
   442 by simp
   443 
   444 
   445 subsubsection {*Powers *}
   446 
   447 lemma "2 ^ 15 = (32768::real)"
   448 by simp
   449 
   450 lemma "-3 ^ 7 = (-2187::real)"
   451 by simp
   452 
   453 lemma "13 ^ 7 = (62748517::real)"
   454 by simp
   455 
   456 lemma "3 ^ 15 = (14348907::real)"
   457 by simp
   458 
   459 lemma "-5 ^ 11 = (-48828125::real)"
   460 by simp
   461 
   462 
   463 subsubsection {*Tests *}
   464 
   465 lemma "(x + y = x) = (y = (0::real))"
   466 by arith
   467 
   468 lemma "(x + y = y) = (x = (0::real))"
   469 by arith
   470 
   471 lemma "(x + y = (0::real)) = (x = -y)"
   472 by arith
   473 
   474 lemma "(x + y = (0::real)) = (y = -x)"
   475 by arith
   476 
   477 lemma "((x + y) < (x + z)) = (y < (z::real))"
   478 by arith
   479 
   480 lemma "((x + z) < (y + z)) = (x < (y::real))"
   481 by arith
   482 
   483 lemma "(\<not> x < y) = (y \<le> (x::real))"
   484 by arith
   485 
   486 lemma "\<not> (x < y \<and> y < (x::real))"
   487 by arith
   488 
   489 lemma "(x::real) < y ==> \<not> y < x"
   490 by arith
   491 
   492 lemma "((x::real) \<noteq> y) = (x < y \<or> y < x)"
   493 by arith
   494 
   495 lemma "(\<not> x \<le> y) = (y < (x::real))"
   496 by arith
   497 
   498 lemma "x \<le> y \<or> y \<le> (x::real)"
   499 by arith
   500 
   501 lemma "x \<le> y \<or> y < (x::real)"
   502 by arith
   503 
   504 lemma "x < y \<or> y \<le> (x::real)"
   505 by arith
   506 
   507 lemma "x \<le> (x::real)"
   508 by arith
   509 
   510 lemma "((x::real) \<le> y) = (x < y \<or> x = y)"
   511 by arith
   512 
   513 lemma "((x::real) \<le> y \<and> y \<le> x) = (x = y)"
   514 by arith
   515 
   516 lemma "\<not>(x < y \<and> y \<le> (x::real))"
   517 by arith
   518 
   519 lemma "\<not>(x \<le> y \<and> y < (x::real))"
   520 by arith
   521 
   522 lemma "(-x < (0::real)) = (0 < x)"
   523 by arith
   524 
   525 lemma "((0::real) < -x) = (x < 0)"
   526 by arith
   527 
   528 lemma "(-x \<le> (0::real)) = (0 \<le> x)"
   529 by arith
   530 
   531 lemma "((0::real) \<le> -x) = (x \<le> 0)"
   532 by arith
   533 
   534 lemma "(x::real) = y \<or> x < y \<or> y < x"
   535 by arith
   536 
   537 lemma "(x::real) = 0 \<or> 0 < x \<or> 0 < -x"
   538 by arith
   539 
   540 lemma "(0::real) \<le> x \<or> 0 \<le> -x"
   541 by arith
   542 
   543 lemma "((x::real) + y \<le> x + z) = (y \<le> z)"
   544 by arith
   545 
   546 lemma "((x::real) + z \<le> y + z) = (x \<le> y)"
   547 by arith
   548 
   549 lemma "(w::real) < x \<and> y < z ==> w + y < x + z"
   550 by arith
   551 
   552 lemma "(w::real) \<le> x \<and> y \<le> z ==> w + y \<le> x + z"
   553 by arith
   554 
   555 lemma "(0::real) \<le> x \<and> 0 \<le> y ==> 0 \<le> x + y"
   556 by arith
   557 
   558 lemma "(0::real) < x \<and> 0 < y ==> 0 < x + y"
   559 by arith
   560 
   561 lemma "(-x < y) = (0 < x + (y::real))"
   562 by arith
   563 
   564 lemma "(x < -y) = (x + y < (0::real))"
   565 by arith
   566 
   567 lemma "(y < x + -z) = (y + z < (x::real))"
   568 by arith
   569 
   570 lemma "(x + -y < z) = (x < z + (y::real))"
   571 by arith
   572 
   573 lemma "x \<le> y ==> x < y + (1::real)"
   574 by arith
   575 
   576 lemma "(x - y) + y = (x::real)"
   577 by arith
   578 
   579 lemma "y + (x - y) = (x::real)"
   580 by arith
   581 
   582 lemma "x - x = (0::real)"
   583 by arith
   584 
   585 lemma "(x - y = 0) = (x = (y::real))"
   586 by arith
   587 
   588 lemma "((0::real) \<le> x + x) = (0 \<le> x)"
   589 by arith
   590 
   591 lemma "(-x \<le> x) = ((0::real) \<le> x)"
   592 by arith
   593 
   594 lemma "(x \<le> -x) = (x \<le> (0::real))"
   595 by arith
   596 
   597 lemma "(-x = (0::real)) = (x = 0)"
   598 by arith
   599 
   600 lemma "-(x - y) = y - (x::real)"
   601 by arith
   602 
   603 lemma "((0::real) < x - y) = (y < x)"
   604 by arith
   605 
   606 lemma "((0::real) \<le> x - y) = (y \<le> x)"
   607 by arith
   608 
   609 lemma "(x + y) - x = (y::real)"
   610 by arith
   611 
   612 lemma "(-x = y) = (x = (-y::real))"
   613 by arith
   614 
   615 lemma "x < (y::real) ==> \<not>(x = y)"
   616 by arith
   617 
   618 lemma "(x \<le> x + y) = ((0::real) \<le> y)"
   619 by arith
   620 
   621 lemma "(y \<le> x + y) = ((0::real) \<le> x)"
   622 by arith
   623 
   624 lemma "(x < x + y) = ((0::real) < y)"
   625 by arith
   626 
   627 lemma "(y < x + y) = ((0::real) < x)"
   628 by arith
   629 
   630 lemma "(x - y) - x = (-y::real)"
   631 by arith
   632 
   633 lemma "(x + y < z) = (x < z - (y::real))"
   634 by arith
   635 
   636 lemma "(x - y < z) = (x < z + (y::real))"
   637 by arith
   638 
   639 lemma "(x < y - z) = (x + z < (y::real))"
   640 by arith
   641 
   642 lemma "(x \<le> y - z) = (x + z \<le> (y::real))"
   643 by arith
   644 
   645 lemma "(x - y \<le> z) = (x \<le> z + (y::real))"
   646 by arith
   647 
   648 lemma "(-x < -y) = (y < (x::real))"
   649 by arith
   650 
   651 lemma "(-x \<le> -y) = (y \<le> (x::real))"
   652 by arith
   653 
   654 lemma "(a + b) - (c + d) = (a - c) + (b - (d::real))"
   655 by arith
   656 
   657 lemma "(0::real) - x = -x"
   658 by arith
   659 
   660 lemma "x - (0::real) = x"
   661 by arith
   662 
   663 lemma "w \<le> x \<and> y < z ==> w + y < x + (z::real)"
   664 by arith
   665 
   666 lemma "w < x \<and> y \<le> z ==> w + y < x + (z::real)"
   667 by arith
   668 
   669 lemma "(0::real) \<le> x \<and> 0 < y ==> 0 < x + (y::real)"
   670 by arith
   671 
   672 lemma "(0::real) < x \<and> 0 \<le> y ==> 0 < x + y"
   673 by arith
   674 
   675 lemma "-x - y = -(x + (y::real))"
   676 by arith
   677 
   678 lemma "x - (-y) = x + (y::real)"
   679 by arith
   680 
   681 lemma "-x - -y = y - (x::real)"
   682 by arith
   683 
   684 lemma "(a - b) + (b - c) = a - (c::real)"
   685 by arith
   686 
   687 lemma "(x = y - z) = (x + z = (y::real))"
   688 by arith
   689 
   690 lemma "(x - y = z) = (x = z + (y::real))"
   691 by arith
   692 
   693 lemma "x - (x - y) = (y::real)"
   694 by arith
   695 
   696 lemma "x - (x + y) = -(y::real)"
   697 by arith
   698 
   699 lemma "x = y ==> x \<le> (y::real)"
   700 by arith
   701 
   702 lemma "(0::real) < x ==> \<not>(x = 0)"
   703 by arith
   704 
   705 lemma "(x + y) * (x - y) = (x * x) - (y * y)"
   706   oops
   707 
   708 lemma "(-x = -y) = (x = (y::real))"
   709 by arith
   710 
   711 lemma "(-x < -y) = (y < (x::real))"
   712 by arith
   713 
   714 lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d"
   715 by (tactic "fast_arith_tac @{context} 1")
   716 
   717 lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)"
   718 by (tactic "fast_arith_tac @{context} 1")
   719 
   720 lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c"
   721 by (tactic "fast_arith_tac @{context} 1")
   722 
   723 lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j"
   724 by (tactic "fast_arith_tac @{context} 1")
   725 
   726 lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j"
   727 by (tactic "fast_arith_tac @{context} 1")
   728 
   729 lemma "!!a::real. a + b + c \<le> i + j + k \<and> a \<le> b \<and> b \<le> c \<and> i \<le> j \<and> j \<le> k --> a + a + a \<le> k + k + k"
   730 by arith
   731 
   732 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
   733     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l"
   734 by (tactic "fast_arith_tac @{context} 1")
   735 
   736 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
   737     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l"
   738 by (tactic "fast_arith_tac @{context} 1")
   739 
   740 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
   741     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i"
   742 by (tactic "fast_arith_tac @{context} 1")
   743 
   744 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
   745     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a + a \<le> l + l + l + l + i + l"
   746 by (tactic "fast_arith_tac @{context} 1")
   747 
   748 
   749 subsection{*Complex Arithmetic*}
   750 
   751 lemma "(1359 + 93746*ii) - (2468 + 46375*ii) = -1109 + 47371*ii"
   752 by simp
   753 
   754 lemma "- (65745 + -47371*ii) = -65745 + 47371*ii"
   755 by simp
   756 
   757 text{*Multiplication requires distributive laws.  Perhaps versions instantiated
   758 to literal constants should be added to the simpset.*}
   759 
   760 lemma "(1 + ii) * (1 - ii) = 2"
   761 by (simp add: ring_distribs)
   762 
   763 lemma "(1 + 2*ii) * (1 + 3*ii) = -5 + 5*ii"
   764 by (simp add: ring_distribs)
   765 
   766 lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii"
   767 by (simp add: ring_distribs)
   768 
   769 text{*No inequalities or linear arithmetic: the complex numbers are unordered!*}
   770 
   771 text{*No powers (not supported yet)*}
   772 
   773 end