src/HOL/ex/BinEx.thy
 author huffman Fri Aug 19 14:17:28 2011 -0700 (2011-08-19) changeset 44311 42c5cbf68052 parent 31066 972c870da225 child 45615 c05e8209a3aa 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@11024  6 header {* 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 paulson@14113  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 paulson@12613  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 paulson@12613  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"  wenzelm@11024  283  by (simp add: Suc_nat_number_of)  wenzelm@20807  284  -- {* not a default rewrite since sometimes we want to have @{text "Suc nnn"} *}  wenzelm@11024  285 wenzelm@11024  286 wenzelm@11024  287 text {* \medskip Addition *}  wenzelm@11024  288 wenzelm@11704  289 lemma "(13::nat) + 19 = 32"  wenzelm@11024  290  by simp  wenzelm@11024  291 wenzelm@11704  292 lemma "(1234::nat) + 5678 = 6912"  wenzelm@11024  293  by simp  wenzelm@11024  294 wenzelm@11704  295 lemma "(973646::nat) + 6475 = 980121"  wenzelm@11024  296  by simp  wenzelm@11024  297 wenzelm@11024  298 wenzelm@11024  299 text {* \medskip Subtraction *}  wenzelm@11024  300 wenzelm@11704  301 lemma "(32::nat) - 14 = 18"  wenzelm@11024  302  by simp  wenzelm@11024  303 paulson@11868  304 lemma "(14::nat) - 15 = 0"  wenzelm@11024  305  by simp  paulson@5545  306 paulson@11868  307 lemma "(14::nat) - 1576644 = 0"  wenzelm@11024  308  by simp  wenzelm@11024  309 wenzelm@11704  310 lemma "(48273776::nat) - 3873737 = 44400039"  wenzelm@11024  311  by simp  wenzelm@11024  312 wenzelm@11024  313 wenzelm@11024  314 text {* \medskip Multiplication *}  wenzelm@11024  315 wenzelm@11704  316 lemma "(12::nat) * 11 = 132"  wenzelm@11024  317  by simp  wenzelm@11024  318 wenzelm@11704  319 lemma "(647::nat) * 3643 = 2357021"  wenzelm@11024  320  by simp  wenzelm@11024  321 wenzelm@11024  322 wenzelm@11024  323 text {* \medskip Quotient and Remainder *}  wenzelm@11024  324 wenzelm@11704  325 lemma "(10::nat) div 3 = 3"  wenzelm@11024  326  by simp  wenzelm@11024  327 paulson@11868  328 lemma "(10::nat) mod 3 = 1"  wenzelm@11024  329  by simp  wenzelm@11024  330 wenzelm@11704  331 lemma "(10000::nat) div 9 = 1111"  wenzelm@11024  332  by simp  wenzelm@11024  333 paulson@11868  334 lemma "(10000::nat) mod 9 = 1"  wenzelm@11024  335  by simp  wenzelm@11024  336 wenzelm@11704  337 lemma "(10000::nat) div 16 = 625"  wenzelm@11024  338  by simp  wenzelm@11024  339 paulson@11868  340 lemma "(10000::nat) mod 16 = 0"  wenzelm@11024  341  by simp  wenzelm@11024  342 paulson@5545  343 paulson@12613  344 text {* \medskip Powers *}  paulson@12613  345 paulson@12613  346 lemma "2 ^ 12 = (4096::nat)"  paulson@12613  347  by simp  paulson@12613  348 paulson@12613  349 lemma "3 ^ 10 = (59049::nat)"  paulson@12613  350  by simp  paulson@12613  351 paulson@12613  352 lemma "12 ^ 7 = (35831808::nat)"  paulson@12613  353  by simp  paulson@12613  354 paulson@12613  355 lemma "3 ^ 14 = (4782969::nat)"  paulson@12613  356  by simp  paulson@12613  357 paulson@12613  358 lemma "5 ^ 11 = (48828125::nat)"  paulson@12613  359  by simp  paulson@12613  360 paulson@12613  361 wenzelm@11024  362 text {* \medskip Testing the cancellation of complementary terms *}  wenzelm@11024  363 paulson@11868  364 lemma "y + (x + -x) = (0::int) + y"  wenzelm@11024  365  by simp  wenzelm@11024  366 paulson@11868  367 lemma "y + (-x + (- y + x)) = (0::int)"  wenzelm@11024  368  by simp  wenzelm@11024  369 paulson@11868  370 lemma "-x + (y + (- y + x)) = (0::int)"  wenzelm@11024  371  by simp  wenzelm@11024  372 paulson@11868  373 lemma "x + (x + (- x + (- x + (- y + - z)))) = (0::int) - y - z"  wenzelm@11024  374  by simp  wenzelm@11024  375 paulson@11868  376 lemma "x + x - x - x - y - z = (0::int) - y - z"  wenzelm@11024  377  by simp  wenzelm@11024  378 paulson@11868  379 lemma "x + y + z - (x + z) = y - (0::int)"  wenzelm@11024  380  by simp  wenzelm@11024  381 paulson@11868  382 lemma "x + (y + (y + (y + (-x + -x)))) = (0::int) + y - x + y + y"  wenzelm@11024  383  by simp  wenzelm@11024  384 paulson@11868  385 lemma "x + (y + (y + (y + (-y + -x)))) = y + (0::int) + y"  wenzelm@11024  386  by simp  wenzelm@11024  387 paulson@11868  388 lemma "x + y - x + z - x - y - z + x < (1::int)"  wenzelm@11024  389  by simp  wenzelm@11024  390 haftmann@28952  391 haftmann@28952  392 subsection{*Real Arithmetic*}  haftmann@28952  393 haftmann@28952  394 subsubsection {*Addition *}  haftmann@28952  395 haftmann@28952  396 lemma "(1359::real) + -2468 = -1109"  haftmann@28952  397 by simp  haftmann@28952  398 haftmann@28952  399 lemma "(93746::real) + -46375 = 47371"  haftmann@28952  400 by simp  haftmann@28952  401 haftmann@28952  402 haftmann@28952  403 subsubsection {*Negation *}  haftmann@28952  404 haftmann@28952  405 lemma "- (65745::real) = -65745"  haftmann@28952  406 by simp  haftmann@28952  407 haftmann@28952  408 lemma "- (-54321::real) = 54321"  haftmann@28952  409 by simp  haftmann@28952  410 haftmann@28952  411 haftmann@28952  412 subsubsection {*Multiplication *}  haftmann@28952  413 haftmann@28952  414 lemma "(-84::real) * 51 = -4284"  haftmann@28952  415 by simp  haftmann@28952  416 haftmann@28952  417 lemma "(255::real) * 255 = 65025"  haftmann@28952  418 by simp  haftmann@28952  419 haftmann@28952  420 lemma "(1359::real) * -2468 = -3354012"  haftmann@28952  421 by simp  haftmann@28952  422 haftmann@28952  423 haftmann@28952  424 subsubsection {*Inequalities *}  haftmann@28952  425 haftmann@28952  426 lemma "(89::real) * 10 \ 889"  haftmann@28952  427 by simp  haftmann@28952  428 haftmann@28952  429 lemma "(13::real) < 18 - 4"  haftmann@28952  430 by simp  haftmann@28952  431 haftmann@28952  432 lemma "(-345::real) < -242 + -100"  haftmann@28952  433 by simp  haftmann@28952  434 haftmann@28952  435 lemma "(13557456::real) < 18678654"  haftmann@28952  436 by simp  haftmann@28952  437 haftmann@28952  438 lemma "(999999::real) \ (1000001 + 1) - 2"  haftmann@28952  439 by simp  haftmann@28952  440 haftmann@28952  441 lemma "(1234567::real) \ 1234567"  haftmann@28952  442 by simp  haftmann@28952  443 haftmann@28952  444 haftmann@28952  445 subsubsection {*Powers *}  haftmann@28952  446 haftmann@28952  447 lemma "2 ^ 15 = (32768::real)"  haftmann@28952  448 by simp  haftmann@28952  449 haftmann@28952  450 lemma "-3 ^ 7 = (-2187::real)"  haftmann@28952  451 by simp  haftmann@28952  452 haftmann@28952  453 lemma "13 ^ 7 = (62748517::real)"  haftmann@28952  454 by simp  haftmann@28952  455 haftmann@28952  456 lemma "3 ^ 15 = (14348907::real)"  haftmann@28952  457 by simp  haftmann@28952  458 haftmann@28952  459 lemma "-5 ^ 11 = (-48828125::real)"  haftmann@28952  460 by simp  haftmann@28952  461 haftmann@28952  462 haftmann@28952  463 subsubsection {*Tests *}  haftmann@28952  464 haftmann@28952  465 lemma "(x + y = x) = (y = (0::real))"  haftmann@28952  466 by arith  haftmann@28952  467 haftmann@28952  468 lemma "(x + y = y) = (x = (0::real))"  haftmann@28952  469 by arith  haftmann@28952  470 haftmann@28952  471 lemma "(x + y = (0::real)) = (x = -y)"  haftmann@28952  472 by arith  haftmann@28952  473 haftmann@28952  474 lemma "(x + y = (0::real)) = (y = -x)"  haftmann@28952  475 by arith  haftmann@28952  476 haftmann@28952  477 lemma "((x + y) < (x + z)) = (y < (z::real))"  haftmann@28952  478 by arith  haftmann@28952  479 haftmann@28952  480 lemma "((x + z) < (y + z)) = (x < (y::real))"  haftmann@28952  481 by arith  haftmann@28952  482 haftmann@28952  483 lemma "(\ x < y) = (y \ (x::real))"  haftmann@28952  484 by arith  haftmann@28952  485 haftmann@28952  486 lemma "\ (x < y \ y < (x::real))"  haftmann@28952  487 by arith  haftmann@28952  488 haftmann@28952  489 lemma "(x::real) < y ==> \ y < x"  haftmann@28952  490 by arith  haftmann@28952  491 haftmann@28952  492 lemma "((x::real) \ y) = (x < y \ y < x)"  haftmann@28952  493 by arith  haftmann@28952  494 haftmann@28952  495 lemma "(\ x \ y) = (y < (x::real))"  haftmann@28952  496 by arith  haftmann@28952  497 haftmann@28952  498 lemma "x \ y \ y \ (x::real)"  haftmann@28952  499 by arith  haftmann@28952  500 haftmann@28952  501 lemma "x \ y \ y < (x::real)"  haftmann@28952  502 by arith  haftmann@28952  503 haftmann@28952  504 lemma "x < y \ y \ (x::real)"  haftmann@28952  505 by arith  haftmann@28952  506 haftmann@28952  507 lemma "x \ (x::real)"  haftmann@28952  508 by arith  haftmann@28952  509 haftmann@28952  510 lemma "((x::real) \ y) = (x < y \ x = y)"  haftmann@28952  511 by arith  haftmann@28952  512 haftmann@28952  513 lemma "((x::real) \ y \ y \ x) = (x = y)"  haftmann@28952  514 by arith  haftmann@28952  515 haftmann@28952  516 lemma "\(x < y \ y \ (x::real))"  haftmann@28952  517 by arith  haftmann@28952  518 haftmann@28952  519 lemma "\(x \ y \ y < (x::real))"  haftmann@28952  520 by arith  haftmann@28952  521 haftmann@28952  522 lemma "(-x < (0::real)) = (0 < x)"  haftmann@28952  523 by arith  haftmann@28952  524 haftmann@28952  525 lemma "((0::real) < -x) = (x < 0)"  haftmann@28952  526 by arith  haftmann@28952  527 haftmann@28952  528 lemma "(-x \ (0::real)) = (0 \ x)"  haftmann@28952  529 by arith  haftmann@28952  530 haftmann@28952  531 lemma "((0::real) \ -x) = (x \ 0)"  haftmann@28952  532 by arith  haftmann@28952  533 haftmann@28952  534 lemma "(x::real) = y \ x < y \ y < x"  haftmann@28952  535 by arith  haftmann@28952  536 haftmann@28952  537 lemma "(x::real) = 0 \ 0 < x \ 0 < -x"  haftmann@28952  538 by arith  haftmann@28952  539 haftmann@28952  540 lemma "(0::real) \ x \ 0 \ -x"  haftmann@28952  541 by arith  haftmann@28952  542 haftmann@28952  543 lemma "((x::real) + y \ x + z) = (y \ z)"  haftmann@28952  544 by arith  haftmann@28952  545 haftmann@28952  546 lemma "((x::real) + z \ y + z) = (x \ y)"  haftmann@28952  547 by arith  haftmann@28952  548 haftmann@28952  549 lemma "(w::real) < x \ y < z ==> w + y < x + z"  haftmann@28952  550 by arith  haftmann@28952  551 haftmann@28952  552 lemma "(w::real) \ x \ y \ z ==> w + y \ x + z"  haftmann@28952  553 by arith  haftmann@28952  554 haftmann@28952  555 lemma "(0::real) \ x \ 0 \ y ==> 0 \ x + y"  haftmann@28952  556 by arith  haftmann@28952  557 haftmann@28952  558 lemma "(0::real) < x \ 0 < y ==> 0 < x + y"  haftmann@28952  559 by arith  haftmann@28952  560 haftmann@28952  561 lemma "(-x < y) = (0 < x + (y::real))"  haftmann@28952  562 by arith  haftmann@28952  563 haftmann@28952  564 lemma "(x < -y) = (x + y < (0::real))"  haftmann@28952  565 by arith  haftmann@28952  566 haftmann@28952  567 lemma "(y < x + -z) = (y + z < (x::real))"  haftmann@28952  568 by arith  haftmann@28952  569 haftmann@28952  570 lemma "(x + -y < z) = (x < z + (y::real))"  haftmann@28952  571 by arith  haftmann@28952  572 haftmann@28952  573 lemma "x \ y ==> x < y + (1::real)"  haftmann@28952  574 by arith  haftmann@28952  575 haftmann@28952  576 lemma "(x - y) + y = (x::real)"  haftmann@28952  577 by arith  haftmann@28952  578 haftmann@28952  579 lemma "y + (x - y) = (x::real)"  haftmann@28952  580 by arith  haftmann@28952  581 haftmann@28952  582 lemma "x - x = (0::real)"  haftmann@28952  583 by arith  haftmann@28952  584 haftmann@28952  585 lemma "(x - y = 0) = (x = (y::real))"  haftmann@28952  586 by arith  haftmann@28952  587 haftmann@28952  588 lemma "((0::real) \ x + x) = (0 \ x)"  haftmann@28952  589 by arith  haftmann@28952  590 haftmann@28952  591 lemma "(-x \ x) = ((0::real) \ x)"  haftmann@28952  592 by arith  haftmann@28952  593 haftmann@28952  594 lemma "(x \ -x) = (x \ (0::real))"  haftmann@28952  595 by arith  haftmann@28952  596 haftmann@28952  597 lemma "(-x = (0::real)) = (x = 0)"  haftmann@28952  598 by arith  haftmann@28952  599 haftmann@28952  600 lemma "-(x - y) = y - (x::real)"  haftmann@28952  601 by arith  haftmann@28952  602 haftmann@28952  603 lemma "((0::real) < x - y) = (y < x)"  haftmann@28952  604 by arith  haftmann@28952  605 haftmann@28952  606 lemma "((0::real) \ x - y) = (y \ x)"  haftmann@28952  607 by arith  haftmann@28952  608 haftmann@28952  609 lemma "(x + y) - x = (y::real)"  haftmann@28952  610 by arith  haftmann@28952  611 haftmann@28952  612 lemma "(-x = y) = (x = (-y::real))"  haftmann@28952  613 by arith  haftmann@28952  614 haftmann@28952  615 lemma "x < (y::real) ==> \(x = y)"  haftmann@28952  616 by arith  haftmann@28952  617 haftmann@28952  618 lemma "(x \ x + y) = ((0::real) \ y)"  haftmann@28952  619 by arith  haftmann@28952  620 haftmann@28952  621 lemma "(y \ x + y) = ((0::real) \ x)"  haftmann@28952  622 by arith  haftmann@28952  623 haftmann@28952  624 lemma "(x < x + y) = ((0::real) < y)"  haftmann@28952  625 by arith  haftmann@28952  626 haftmann@28952  627 lemma "(y < x + y) = ((0::real) < x)"  haftmann@28952  628 by arith  haftmann@28952  629 haftmann@28952  630 lemma "(x - y) - x = (-y::real)"  haftmann@28952  631 by arith  haftmann@28952  632 haftmann@28952  633 lemma "(x + y < z) = (x < z - (y::real))"  haftmann@28952  634 by arith  haftmann@28952  635 haftmann@28952  636 lemma "(x - y < z) = (x < z + (y::real))"  haftmann@28952  637 by arith  haftmann@28952  638 haftmann@28952  639 lemma "(x < y - z) = (x + z < (y::real))"  haftmann@28952  640 by arith  haftmann@28952  641 haftmann@28952  642 lemma "(x \ y - z) = (x + z \ (y::real))"  haftmann@28952  643 by arith  haftmann@28952  644 haftmann@28952  645 lemma "(x - y \ z) = (x \ z + (y::real))"  haftmann@28952  646 by arith  haftmann@28952  647 haftmann@28952  648 lemma "(-x < -y) = (y < (x::real))"  haftmann@28952  649 by arith  haftmann@28952  650 haftmann@28952  651 lemma "(-x \ -y) = (y \ (x::real))"  haftmann@28952  652 by arith  haftmann@28952  653 haftmann@28952  654 lemma "(a + b) - (c + d) = (a - c) + (b - (d::real))"  haftmann@28952  655 by arith  haftmann@28952  656 haftmann@28952  657 lemma "(0::real) - x = -x"  haftmann@28952  658 by arith  haftmann@28952  659 haftmann@28952  660 lemma "x - (0::real) = x"  haftmann@28952  661 by arith  haftmann@28952  662 haftmann@28952  663 lemma "w \ x \ y < z ==> w + y < x + (z::real)"  haftmann@28952  664 by arith  haftmann@28952  665 haftmann@28952  666 lemma "w < x \ y \ z ==> w + y < x + (z::real)"  haftmann@28952  667 by arith  haftmann@28952  668 haftmann@28952  669 lemma "(0::real) \ x \ 0 < y ==> 0 < x + (y::real)"  haftmann@28952  670 by arith  haftmann@28952  671 haftmann@28952  672 lemma "(0::real) < x \ 0 \ y ==> 0 < x + y"  haftmann@28952  673 by arith  haftmann@28952  674 haftmann@28952  675 lemma "-x - y = -(x + (y::real))"  haftmann@28952  676 by arith  haftmann@28952  677 haftmann@28952  678 lemma "x - (-y) = x + (y::real)"  haftmann@28952  679 by arith  haftmann@28952  680 haftmann@28952  681 lemma "-x - -y = y - (x::real)"  haftmann@28952  682 by arith  haftmann@28952  683 haftmann@28952  684 lemma "(a - b) + (b - c) = a - (c::real)"  haftmann@28952  685 by arith  haftmann@28952  686 haftmann@28952  687 lemma "(x = y - z) = (x + z = (y::real))"  haftmann@28952  688 by arith  haftmann@28952  689 haftmann@28952  690 lemma "(x - y = z) = (x = z + (y::real))"  haftmann@28952  691 by arith  haftmann@28952  692 haftmann@28952  693 lemma "x - (x - y) = (y::real)"  haftmann@28952  694 by arith  haftmann@28952  695 haftmann@28952  696 lemma "x - (x + y) = -(y::real)"  haftmann@28952  697 by arith  haftmann@28952  698 haftmann@28952  699 lemma "x = y ==> x \ (y::real)"  haftmann@28952  700 by arith  haftmann@28952  701 haftmann@28952  702 lemma "(0::real) < x ==> \(x = 0)"  haftmann@28952  703 by arith  haftmann@28952  704 haftmann@28952  705 lemma "(x + y) * (x - y) = (x * x) - (y * y)"  haftmann@28952  706  oops  haftmann@28952  707 haftmann@28952  708 lemma "(-x = -y) = (x = (y::real))"  haftmann@28952  709 by arith  haftmann@28952  710 haftmann@28952  711 lemma "(-x < -y) = (y < (x::real))"  haftmann@28952  712 by arith  haftmann@28952  713 haftmann@28952  714 lemma "!!a::real. a \ b ==> c \ d ==> x + y < z ==> a + c \ b + d"  haftmann@31066  715 by linarith  haftmann@28952  716 haftmann@28952  717 lemma "!!a::real. a < b ==> c < d ==> a - d \ b + (-c)"  haftmann@31066  718 by linarith  haftmann@28952  719 haftmann@28952  720 lemma "!!a::real. a \ b ==> b + b \ c ==> a + a \ c"  haftmann@31066  721 by linarith  haftmann@28952  722 haftmann@28952  723 lemma "!!a::real. a + b \ i + j ==> a \ b ==> i \ j ==> a + a \ j + j"  haftmann@31066  724 by linarith  haftmann@28952  725 haftmann@28952  726 lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j"  haftmann@31066  727 by linarith  haftmann@28952  728 haftmann@28952  729 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  730 by arith  haftmann@28952  731 haftmann@28952  732 lemma "!!a::real. a + b + c + d \ i + j + k + l ==> a \ b ==> b \ c  haftmann@28952  733  ==> c \ d ==> i \ j ==> j \ k ==> k \ l ==> a \ l"  haftmann@31066  734 by linarith  haftmann@28952  735 haftmann@28952  736 lemma "!!a::real. a + b + c + d \ i + j + k + l ==> a \ b ==> b \ c  haftmann@28952  737  ==> c \ d ==> i \ j ==> j \ k ==> k \ l ==> a + a + a + a \ l + l + l + l"  haftmann@31066  738 by linarith  haftmann@28952  739 haftmann@28952  740 lemma "!!a::real. a + b + c + d \ i + j + k + l ==> a \ b ==> b \ c  haftmann@28952  741  ==> c \ d ==> i \ j ==> j \ k ==> k \ l ==> a + a + a + a + a \ l + l + l + l + i"  haftmann@31066  742 by linarith  haftmann@28952  743 haftmann@28952  744 lemma "!!a::real. a + b + c + d \ i + j + k + l ==> a \ b ==> b \ c  haftmann@28952  745  ==> c \ d ==> i \ j ==> j \ k ==> k \ l ==> a + a + a + a + a + a \ l + l + l + l + i + l"  haftmann@31066  746 by linarith  haftmann@28952  747 haftmann@28952  748 haftmann@28952  749 subsection{*Complex Arithmetic*}  haftmann@28952  750 haftmann@28952  751 lemma "(1359 + 93746*ii) - (2468 + 46375*ii) = -1109 + 47371*ii"  haftmann@28952  752 by simp  haftmann@28952  753 haftmann@28952  754 lemma "- (65745 + -47371*ii) = -65745 + 47371*ii"  haftmann@28952  755 by simp  haftmann@28952  756 haftmann@28952  757 text{*Multiplication requires distributive laws. Perhaps versions instantiated  haftmann@28952  758 to literal constants should be added to the simpset.*}  haftmann@28952  759 haftmann@28952  760 lemma "(1 + ii) * (1 - ii) = 2"  haftmann@28952  761 by (simp add: ring_distribs)  haftmann@28952  762 haftmann@28952  763 lemma "(1 + 2*ii) * (1 + 3*ii) = -5 + 5*ii"  haftmann@28952  764 by (simp add: ring_distribs)  haftmann@28952  765 haftmann@28952  766 lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii"  haftmann@28952  767 by (simp add: ring_distribs)  haftmann@28952  768 haftmann@28952  769 text{*No inequalities or linear arithmetic: the complex numbers are unordered!*}  haftmann@28952  770 haftmann@28952  771 text{*No powers (not supported yet)*}  haftmann@28952  772 paulson@5545  773 end