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