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