src/HOL/ex/BinEx.thy
 author paulson Wed Apr 01 15:47:55 2015 +0100 (2015-04-01) changeset 59871 e1a49ac9c537 parent 58889 5b7a9633cfa8 child 61343 5b5656a63bd6 permissions -rw-r--r--
John Harrison's example: a 32-bit approximation to pi. SLOW
     1 (*  Title:      HOL/ex/BinEx.thy

     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     3     Copyright   1998  University of Cambridge

     4 *)

     5

     6 section {* Binary arithmetic examples *}

     7

     8 theory BinEx

     9 imports Complex_Main

    10 begin

    11

    12 subsection {* Regression Testing for Cancellation Simprocs *}

    13

    14 lemma "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"

    15 apply simp  oops

    16

    17 lemma "2*u = (u::int)"

    18 apply simp  oops

    19

    20 lemma "(i + j + 12 + (k::int)) - 15 = y"

    21 apply simp  oops

    22

    23 lemma "(i + j + 12 + (k::int)) - 5 = y"

    24 apply simp  oops

    25

    26 lemma "y - b < (b::int)"

    27 apply simp  oops

    28

    29 lemma "y - (3*b + c) < (b::int) - 2*c"

    30 apply simp  oops

    31

    32 lemma "(2*x - (u*v) + y) - v*3*u = (w::int)"

    33 apply simp  oops

    34

    35 lemma "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"

    36 apply simp  oops

    37

    38 lemma "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"

    39 apply simp  oops

    40

    41 lemma "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"

    42 apply simp  oops

    43

    44 lemma "(i + j + 12 + (k::int)) = u + 15 + y"

    45 apply simp  oops

    46

    47 lemma "(i + j*2 + 12 + (k::int)) = j + 5 + y"

    48 apply simp  oops

    49

    50 lemma "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)"

    51 apply simp  oops

    52

    53 lemma "a + -(b+c) + b = (d::int)"

    54 apply simp  oops

    55

    56 lemma "a + -(b+c) - b = (d::int)"

    57 apply simp  oops

    58

    59 (*negative numerals*)

    60 lemma "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"

    61 apply simp  oops

    62

    63 lemma "(i + j + -3 + (k::int)) < u + 5 + y"

    64 apply simp  oops

    65

    66 lemma "(i + j + 3 + (k::int)) < u + -6 + y"

    67 apply simp  oops

    68

    69 lemma "(i + j + -12 + (k::int)) - 15 = y"

    70 apply simp  oops

    71

    72 lemma "(i + j + 12 + (k::int)) - -15 = y"

    73 apply simp  oops

    74

    75 lemma "(i + j + -12 + (k::int)) - -15 = y"

    76 apply simp  oops

    77

    78 lemma "- (2*i) + 3  + (2*i + 4) = (0::int)"

    79 apply simp  oops

    80

    81 (*Tobias's example dated 2015-03-02*)

    82 lemma "(pi * (real u * 2) = pi * (real (xa v) * - 2))"

    83 apply simp oops

    84

    85

    86 subsection {* Arithmetic Method Tests *}

    87

    88

    89 lemma "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"

    90 by arith

    91

    92 lemma "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)"

    93 by arith

    94

    95 lemma "!!a::int. [| a < b; c < d |] ==> a+c+ 1 < b+d"

    96 by arith

    97

    98 lemma "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"

    99 by arith

   100

   101 lemma "!!a::int. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"

   102 by arith

   103

   104 lemma "!!a::int. [| a+b < i+j; a<b; i<j |] ==> a+a - - (- 1) < j+j - 3"

   105 by arith

   106

   107 lemma "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"

   108 by arith

   109

   110 lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]

   111       ==> a <= l"

   112 by arith

   113

   114 lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]

   115       ==> a+a+a+a <= l+l+l+l"

   116 by arith

   117

   118 lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]

   119       ==> a+a+a+a+a <= l+l+l+l+i"

   120 by arith

   121

   122 lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]

   123       ==> a+a+a+a+a+a <= l+l+l+l+i+l"

   124 by arith

   125

   126 lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]

   127       ==> 6*a <= 5*l+i"

   128 by arith

   129

   130

   131

   132 subsection {* The Integers *}

   133

   134 text {* Addition *}

   135

   136 lemma "(13::int) + 19 = 32"

   137   by simp

   138

   139 lemma "(1234::int) + 5678 = 6912"

   140   by simp

   141

   142 lemma "(1359::int) + -2468 = -1109"

   143   by simp

   144

   145 lemma "(93746::int) + -46375 = 47371"

   146   by simp

   147

   148

   149 text {* \medskip Negation *}

   150

   151 lemma "- (65745::int) = -65745"

   152   by simp

   153

   154 lemma "- (-54321::int) = 54321"

   155   by simp

   156

   157

   158 text {* \medskip Multiplication *}

   159

   160 lemma "(13::int) * 19 = 247"

   161   by simp

   162

   163 lemma "(-84::int) * 51 = -4284"

   164   by simp

   165

   166 lemma "(255::int) * 255 = 65025"

   167   by simp

   168

   169 lemma "(1359::int) * -2468 = -3354012"

   170   by simp

   171

   172 lemma "(89::int) * 10 \<noteq> 889"

   173   by simp

   174

   175 lemma "(13::int) < 18 - 4"

   176   by simp

   177

   178 lemma "(-345::int) < -242 + -100"

   179   by simp

   180

   181 lemma "(13557456::int) < 18678654"

   182   by simp

   183

   184 lemma "(999999::int) \<le> (1000001 + 1) - 2"

   185   by simp

   186

   187 lemma "(1234567::int) \<le> 1234567"

   188   by simp

   189

   190 text{*No integer overflow!*}

   191 lemma "1234567 * (1234567::int) < 1234567*1234567*1234567"

   192   by simp

   193

   194

   195 text {* \medskip Quotient and Remainder *}

   196

   197 lemma "(10::int) div 3 = 3"

   198   by simp

   199

   200 lemma "(10::int) mod 3 = 1"

   201   by simp

   202

   203 text {* A negative divisor *}

   204

   205 lemma "(10::int) div -3 = -4"

   206   by simp

   207

   208 lemma "(10::int) mod -3 = -2"

   209   by simp

   210

   211 text {*

   212   A negative dividend\footnote{The definition agrees with mathematical

   213   convention and with ML, but not with the hardware of most computers}

   214 *}

   215

   216 lemma "(-10::int) div 3 = -4"

   217   by simp

   218

   219 lemma "(-10::int) mod 3 = 2"

   220   by simp

   221

   222 text {* A negative dividend \emph{and} divisor *}

   223

   224 lemma "(-10::int) div -3 = 3"

   225   by simp

   226

   227 lemma "(-10::int) mod -3 = -1"

   228   by simp

   229

   230 text {* A few bigger examples *}

   231

   232 lemma "(8452::int) mod 3 = 1"

   233   by simp

   234

   235 lemma "(59485::int) div 434 = 137"

   236   by simp

   237

   238 lemma "(1000006::int) mod 10 = 6"

   239   by simp

   240

   241

   242 text {* \medskip Division by shifting *}

   243

   244 lemma "10000000 div 2 = (5000000::int)"

   245   by simp

   246

   247 lemma "10000001 mod 2 = (1::int)"

   248   by simp

   249

   250 lemma "10000055 div 32 = (312501::int)"

   251   by simp

   252

   253 lemma "10000055 mod 32 = (23::int)"

   254   by simp

   255

   256 lemma "100094 div 144 = (695::int)"

   257   by simp

   258

   259 lemma "100094 mod 144 = (14::int)"

   260   by simp

   261

   262

   263 text {* \medskip Powers *}

   264

   265 lemma "2 ^ 10 = (1024::int)"

   266   by simp

   267

   268 lemma "(- 3) ^ 7 = (-2187::int)"

   269   by simp

   270

   271 lemma "13 ^ 7 = (62748517::int)"

   272   by simp

   273

   274 lemma "3 ^ 15 = (14348907::int)"

   275   by simp

   276

   277 lemma "(- 5) ^ 11 = (-48828125::int)"

   278   by simp

   279

   280

   281 subsection {* The Natural Numbers *}

   282

   283 text {* Successor *}

   284

   285 lemma "Suc 99999 = 100000"

   286   by simp

   287

   288

   289 text {* \medskip Addition *}

   290

   291 lemma "(13::nat) + 19 = 32"

   292   by simp

   293

   294 lemma "(1234::nat) + 5678 = 6912"

   295   by simp

   296

   297 lemma "(973646::nat) + 6475 = 980121"

   298   by simp

   299

   300

   301 text {* \medskip Subtraction *}

   302

   303 lemma "(32::nat) - 14 = 18"

   304   by simp

   305

   306 lemma "(14::nat) - 15 = 0"

   307   by simp

   308

   309 lemma "(14::nat) - 1576644 = 0"

   310   by simp

   311

   312 lemma "(48273776::nat) - 3873737 = 44400039"

   313   by simp

   314

   315

   316 text {* \medskip Multiplication *}

   317

   318 lemma "(12::nat) * 11 = 132"

   319   by simp

   320

   321 lemma "(647::nat) * 3643 = 2357021"

   322   by simp

   323

   324

   325 text {* \medskip Quotient and Remainder *}

   326

   327 lemma "(10::nat) div 3 = 3"

   328   by simp

   329

   330 lemma "(10::nat) mod 3 = 1"

   331   by simp

   332

   333 lemma "(10000::nat) div 9 = 1111"

   334   by simp

   335

   336 lemma "(10000::nat) mod 9 = 1"

   337   by simp

   338

   339 lemma "(10000::nat) div 16 = 625"

   340   by simp

   341

   342 lemma "(10000::nat) mod 16 = 0"

   343   by simp

   344

   345

   346 text {* \medskip Powers *}

   347

   348 lemma "2 ^ 12 = (4096::nat)"

   349   by simp

   350

   351 lemma "3 ^ 10 = (59049::nat)"

   352   by simp

   353

   354 lemma "12 ^ 7 = (35831808::nat)"

   355   by simp

   356

   357 lemma "3 ^ 14 = (4782969::nat)"

   358   by simp

   359

   360 lemma "5 ^ 11 = (48828125::nat)"

   361   by simp

   362

   363

   364 text {* \medskip Testing the cancellation of complementary terms *}

   365

   366 lemma "y + (x + -x) = (0::int) + y"

   367   by simp

   368

   369 lemma "y + (-x + (- y + x)) = (0::int)"

   370   by simp

   371

   372 lemma "-x + (y + (- y + x)) = (0::int)"

   373   by simp

   374

   375 lemma "x + (x + (- x + (- x + (- y + - z)))) = (0::int) - y - z"

   376   by simp

   377

   378 lemma "x + x - x - x - y - z = (0::int) - y - z"

   379   by simp

   380

   381 lemma "x + y + z - (x + z) = y - (0::int)"

   382   by simp

   383

   384 lemma "x + (y + (y + (y + (-x + -x)))) = (0::int) + y - x + y + y"

   385   by simp

   386

   387 lemma "x + (y + (y + (y + (-y + -x)))) = y + (0::int) + y"

   388   by simp

   389

   390 lemma "x + y - x + z - x - y - z + x < (1::int)"

   391   by simp

   392

   393

   394 subsection{*Real Arithmetic*}

   395

   396 subsubsection {*Addition *}

   397

   398 lemma "(1359::real) + -2468 = -1109"

   399 by simp

   400

   401 lemma "(93746::real) + -46375 = 47371"

   402 by simp

   403

   404

   405 subsubsection {*Negation *}

   406

   407 lemma "- (65745::real) = -65745"

   408 by simp

   409

   410 lemma "- (-54321::real) = 54321"

   411 by simp

   412

   413

   414 subsubsection {*Multiplication *}

   415

   416 lemma "(-84::real) * 51 = -4284"

   417 by simp

   418

   419 lemma "(255::real) * 255 = 65025"

   420 by simp

   421

   422 lemma "(1359::real) * -2468 = -3354012"

   423 by simp

   424

   425

   426 subsubsection {*Inequalities *}

   427

   428 lemma "(89::real) * 10 \<noteq> 889"

   429 by simp

   430

   431 lemma "(13::real) < 18 - 4"

   432 by simp

   433

   434 lemma "(-345::real) < -242 + -100"

   435 by simp

   436

   437 lemma "(13557456::real) < 18678654"

   438 by simp

   439

   440 lemma "(999999::real) \<le> (1000001 + 1) - 2"

   441 by simp

   442

   443 lemma "(1234567::real) \<le> 1234567"

   444 by simp

   445

   446

   447 subsubsection {*Powers *}

   448

   449 lemma "2 ^ 15 = (32768::real)"

   450 by simp

   451

   452 lemma "(- 3) ^ 7 = (-2187::real)"

   453 by simp

   454

   455 lemma "13 ^ 7 = (62748517::real)"

   456 by simp

   457

   458 lemma "3 ^ 15 = (14348907::real)"

   459 by simp

   460

   461 lemma "(- 5) ^ 11 = (-48828125::real)"

   462 by simp

   463

   464

   465 subsubsection {*Tests *}

   466

   467 lemma "(x + y = x) = (y = (0::real))"

   468 by arith

   469

   470 lemma "(x + y = y) = (x = (0::real))"

   471 by arith

   472

   473 lemma "(x + y = (0::real)) = (x = -y)"

   474 by arith

   475

   476 lemma "(x + y = (0::real)) = (y = -x)"

   477 by arith

   478

   479 lemma "((x + y) < (x + z)) = (y < (z::real))"

   480 by arith

   481

   482 lemma "((x + z) < (y + z)) = (x < (y::real))"

   483 by arith

   484

   485 lemma "(\<not> x < y) = (y \<le> (x::real))"

   486 by arith

   487

   488 lemma "\<not> (x < y \<and> y < (x::real))"

   489 by arith

   490

   491 lemma "(x::real) < y ==> \<not> y < x"

   492 by arith

   493

   494 lemma "((x::real) \<noteq> y) = (x < y \<or> y < x)"

   495 by arith

   496

   497 lemma "(\<not> x \<le> y) = (y < (x::real))"

   498 by arith

   499

   500 lemma "x \<le> y \<or> y \<le> (x::real)"

   501 by arith

   502

   503 lemma "x \<le> y \<or> y < (x::real)"

   504 by arith

   505

   506 lemma "x < y \<or> y \<le> (x::real)"

   507 by arith

   508

   509 lemma "x \<le> (x::real)"

   510 by arith

   511

   512 lemma "((x::real) \<le> y) = (x < y \<or> x = y)"

   513 by arith

   514

   515 lemma "((x::real) \<le> y \<and> y \<le> x) = (x = y)"

   516 by arith

   517

   518 lemma "\<not>(x < y \<and> y \<le> (x::real))"

   519 by arith

   520

   521 lemma "\<not>(x \<le> y \<and> y < (x::real))"

   522 by arith

   523

   524 lemma "(-x < (0::real)) = (0 < x)"

   525 by arith

   526

   527 lemma "((0::real) < -x) = (x < 0)"

   528 by arith

   529

   530 lemma "(-x \<le> (0::real)) = (0 \<le> x)"

   531 by arith

   532

   533 lemma "((0::real) \<le> -x) = (x \<le> 0)"

   534 by arith

   535

   536 lemma "(x::real) = y \<or> x < y \<or> y < x"

   537 by arith

   538

   539 lemma "(x::real) = 0 \<or> 0 < x \<or> 0 < -x"

   540 by arith

   541

   542 lemma "(0::real) \<le> x \<or> 0 \<le> -x"

   543 by arith

   544

   545 lemma "((x::real) + y \<le> x + z) = (y \<le> z)"

   546 by arith

   547

   548 lemma "((x::real) + z \<le> y + z) = (x \<le> y)"

   549 by arith

   550

   551 lemma "(w::real) < x \<and> y < z ==> w + y < x + z"

   552 by arith

   553

   554 lemma "(w::real) \<le> x \<and> y \<le> z ==> w + y \<le> x + z"

   555 by arith

   556

   557 lemma "(0::real) \<le> x \<and> 0 \<le> y ==> 0 \<le> x + y"

   558 by arith

   559

   560 lemma "(0::real) < x \<and> 0 < y ==> 0 < x + y"

   561 by arith

   562

   563 lemma "(-x < y) = (0 < x + (y::real))"

   564 by arith

   565

   566 lemma "(x < -y) = (x + y < (0::real))"

   567 by arith

   568

   569 lemma "(y < x + -z) = (y + z < (x::real))"

   570 by arith

   571

   572 lemma "(x + -y < z) = (x < z + (y::real))"

   573 by arith

   574

   575 lemma "x \<le> y ==> x < y + (1::real)"

   576 by arith

   577

   578 lemma "(x - y) + y = (x::real)"

   579 by arith

   580

   581 lemma "y + (x - y) = (x::real)"

   582 by arith

   583

   584 lemma "x - x = (0::real)"

   585 by arith

   586

   587 lemma "(x - y = 0) = (x = (y::real))"

   588 by arith

   589

   590 lemma "((0::real) \<le> x + x) = (0 \<le> x)"

   591 by arith

   592

   593 lemma "(-x \<le> x) = ((0::real) \<le> x)"

   594 by arith

   595

   596 lemma "(x \<le> -x) = (x \<le> (0::real))"

   597 by arith

   598

   599 lemma "(-x = (0::real)) = (x = 0)"

   600 by arith

   601

   602 lemma "-(x - y) = y - (x::real)"

   603 by arith

   604

   605 lemma "((0::real) < x - y) = (y < x)"

   606 by arith

   607

   608 lemma "((0::real) \<le> x - y) = (y \<le> x)"

   609 by arith

   610

   611 lemma "(x + y) - x = (y::real)"

   612 by arith

   613

   614 lemma "(-x = y) = (x = (-y::real))"

   615 by arith

   616

   617 lemma "x < (y::real) ==> \<not>(x = y)"

   618 by arith

   619

   620 lemma "(x \<le> x + y) = ((0::real) \<le> y)"

   621 by arith

   622

   623 lemma "(y \<le> x + y) = ((0::real) \<le> x)"

   624 by arith

   625

   626 lemma "(x < x + y) = ((0::real) < y)"

   627 by arith

   628

   629 lemma "(y < x + y) = ((0::real) < x)"

   630 by arith

   631

   632 lemma "(x - y) - x = (-y::real)"

   633 by arith

   634

   635 lemma "(x + y < z) = (x < z - (y::real))"

   636 by arith

   637

   638 lemma "(x - y < z) = (x < z + (y::real))"

   639 by arith

   640

   641 lemma "(x < y - z) = (x + z < (y::real))"

   642 by arith

   643

   644 lemma "(x \<le> y - z) = (x + z \<le> (y::real))"

   645 by arith

   646

   647 lemma "(x - y \<le> z) = (x \<le> z + (y::real))"

   648 by arith

   649

   650 lemma "(-x < -y) = (y < (x::real))"

   651 by arith

   652

   653 lemma "(-x \<le> -y) = (y \<le> (x::real))"

   654 by arith

   655

   656 lemma "(a + b) - (c + d) = (a - c) + (b - (d::real))"

   657 by arith

   658

   659 lemma "(0::real) - x = -x"

   660 by arith

   661

   662 lemma "x - (0::real) = x"

   663 by arith

   664

   665 lemma "w \<le> x \<and> y < z ==> w + y < x + (z::real)"

   666 by arith

   667

   668 lemma "w < x \<and> y \<le> z ==> w + y < x + (z::real)"

   669 by arith

   670

   671 lemma "(0::real) \<le> x \<and> 0 < y ==> 0 < x + (y::real)"

   672 by arith

   673

   674 lemma "(0::real) < x \<and> 0 \<le> y ==> 0 < x + y"

   675 by arith

   676

   677 lemma "-x - y = -(x + (y::real))"

   678 by arith

   679

   680 lemma "x - (-y) = x + (y::real)"

   681 by arith

   682

   683 lemma "-x - -y = y - (x::real)"

   684 by arith

   685

   686 lemma "(a - b) + (b - c) = a - (c::real)"

   687 by arith

   688

   689 lemma "(x = y - z) = (x + z = (y::real))"

   690 by arith

   691

   692 lemma "(x - y = z) = (x = z + (y::real))"

   693 by arith

   694

   695 lemma "x - (x - y) = (y::real)"

   696 by arith

   697

   698 lemma "x - (x + y) = -(y::real)"

   699 by arith

   700

   701 lemma "x = y ==> x \<le> (y::real)"

   702 by arith

   703

   704 lemma "(0::real) < x ==> \<not>(x = 0)"

   705 by arith

   706

   707 lemma "(x + y) * (x - y) = (x * x) - (y * y)"

   708   oops

   709

   710 lemma "(-x = -y) = (x = (y::real))"

   711 by arith

   712

   713 lemma "(-x < -y) = (y < (x::real))"

   714 by arith

   715

   716 lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d"

   717 by linarith

   718

   719 lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)"

   720 by linarith

   721

   722 lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c"

   723 by linarith

   724

   725 lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j"

   726 by linarith

   727

   728 lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j"

   729 by linarith

   730

   731 lemma "!!a::real. a + b + c \<le> i + j + k \<and> a \<le> b \<and> b \<le> c \<and> i \<le> j \<and> j \<le> k --> a + a + a \<le> k + k + k"

   732 by arith

   733

   734 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c

   735     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l"

   736 by linarith

   737

   738 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c

   739     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l"

   740 by linarith

   741

   742 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c

   743     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i"

   744 by linarith

   745

   746 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c

   747     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a + a \<le> l + l + l + l + i + l"

   748 by linarith

   749

   750

   751 subsection{*Complex Arithmetic*}

   752

   753 lemma "(1359 + 93746*ii) - (2468 + 46375*ii) = -1109 + 47371*ii"

   754 by simp

   755

   756 lemma "- (65745 + -47371*ii) = -65745 + 47371*ii"

   757 by simp

   758

   759 text{*Multiplication requires distributive laws.  Perhaps versions instantiated

   760 to literal constants should be added to the simpset.*}

   761

   762 lemma "(1 + ii) * (1 - ii) = 2"

   763 by (simp add: ring_distribs)

   764

   765 lemma "(1 + 2*ii) * (1 + 3*ii) = -5 + 5*ii"

   766 by (simp add: ring_distribs)

   767

   768 lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii"

   769 by (simp add: ring_distribs)

   770

   771 text{*No inequalities or linear arithmetic: the complex numbers are unordered!*}

   772

   773 text{*No powers (not supported yet)*}

   774

   775 end