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