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