src/HOL/ex/BinEx.thy
 author haftmann Sun Sep 21 16:56:11 2014 +0200 (2014-09-21) changeset 58410 6d46ad54a2ab parent 45615 c05e8209a3aa child 58889 5b7a9633cfa8 permissions -rw-r--r--
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
     1 (*  Title:      HOL/ex/BinEx.thy

     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     3     Copyright   1998  University of Cambridge

     4 *)

     5

     6 header {* 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

    82

    83 subsection {* Arithmetic Method Tests *}

    84

    85

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

    87 by arith

    88

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

    90 by arith

    91

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

    93 by arith

    94

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

    96 by arith

    97

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

    99 by arith

   100

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

   102 by arith

   103

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

   105 by arith

   106

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

   108       ==> a <= l"

   109 by arith

   110

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

   112       ==> a+a+a+a <= l+l+l+l"

   113 by arith

   114

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

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

   117 by arith

   118

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

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

   121 by arith

   122

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

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

   125 by arith

   126

   127

   128

   129 subsection {* The Integers *}

   130

   131 text {* Addition *}

   132

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

   134   by simp

   135

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

   137   by simp

   138

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

   140   by simp

   141

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

   143   by simp

   144

   145

   146 text {* \medskip Negation *}

   147

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

   149   by simp

   150

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

   152   by simp

   153

   154

   155 text {* \medskip Multiplication *}

   156

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

   158   by simp

   159

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

   161   by simp

   162

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

   164   by simp

   165

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

   167   by simp

   168

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

   170   by simp

   171

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

   173   by simp

   174

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

   176   by simp

   177

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

   179   by simp

   180

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

   182   by simp

   183

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

   185   by simp

   186

   187 text{*No integer overflow!*}

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

   189   by simp

   190

   191

   192 text {* \medskip Quotient and Remainder *}

   193

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

   195   by simp

   196

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

   198   by simp

   199

   200 text {* A negative divisor *}

   201

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

   203   by simp

   204

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

   206   by simp

   207

   208 text {*

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

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

   211 *}

   212

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

   214   by simp

   215

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

   217   by simp

   218

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

   220

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

   222   by simp

   223

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

   225   by simp

   226

   227 text {* A few bigger examples *}

   228

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

   230   by simp

   231

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

   233   by simp

   234

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

   236   by simp

   237

   238

   239 text {* \medskip Division by shifting *}

   240

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

   242   by simp

   243

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

   245   by simp

   246

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

   248   by simp

   249

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

   251   by simp

   252

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

   254   by simp

   255

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

   257   by simp

   258

   259

   260 text {* \medskip Powers *}

   261

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

   263   by simp

   264

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

   266   by simp

   267

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

   269   by simp

   270

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

   272   by simp

   273

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

   275   by simp

   276

   277

   278 subsection {* The Natural Numbers *}

   279

   280 text {* Successor *}

   281

   282 lemma "Suc 99999 = 100000"

   283   by simp

   284

   285

   286 text {* \medskip Addition *}

   287

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

   289   by simp

   290

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

   292   by simp

   293

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

   295   by simp

   296

   297

   298 text {* \medskip Subtraction *}

   299

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

   301   by simp

   302

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

   304   by simp

   305

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

   307   by simp

   308

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

   310   by simp

   311

   312

   313 text {* \medskip Multiplication *}

   314

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

   316   by simp

   317

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

   319   by simp

   320

   321

   322 text {* \medskip Quotient and Remainder *}

   323

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

   325   by simp

   326

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

   328   by simp

   329

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

   331   by simp

   332

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

   334   by simp

   335

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

   337   by simp

   338

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

   340   by simp

   341

   342

   343 text {* \medskip Powers *}

   344

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

   346   by simp

   347

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

   349   by simp

   350

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

   352   by simp

   353

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

   355   by simp

   356

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

   358   by simp

   359

   360

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

   362

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

   364   by simp

   365

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

   367   by simp

   368

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

   370   by simp

   371

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

   373   by simp

   374

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

   376   by simp

   377

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

   379   by simp

   380

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

   382   by simp

   383

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

   385   by simp

   386

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

   388   by simp

   389

   390

   391 subsection{*Real Arithmetic*}

   392

   393 subsubsection {*Addition *}

   394

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

   396 by simp

   397

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

   399 by simp

   400

   401

   402 subsubsection {*Negation *}

   403

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

   405 by simp

   406

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

   408 by simp

   409

   410

   411 subsubsection {*Multiplication *}

   412

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

   414 by simp

   415

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

   417 by simp

   418

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

   420 by simp

   421

   422

   423 subsubsection {*Inequalities *}

   424

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

   426 by simp

   427

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

   429 by simp

   430

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

   432 by simp

   433

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

   435 by simp

   436

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

   438 by simp

   439

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

   441 by simp

   442

   443

   444 subsubsection {*Powers *}

   445

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

   447 by simp

   448

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

   450 by simp

   451

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

   453 by simp

   454

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

   456 by simp

   457

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

   459 by simp

   460

   461

   462 subsubsection {*Tests *}

   463

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

   465 by arith

   466

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

   468 by arith

   469

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

   471 by arith

   472

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

   474 by arith

   475

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

   477 by arith

   478

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

   480 by arith

   481

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

   483 by arith

   484

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

   486 by arith

   487

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

   489 by arith

   490

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

   492 by arith

   493

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

   495 by arith

   496

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

   498 by arith

   499

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

   501 by arith

   502

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

   504 by arith

   505

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

   507 by arith

   508

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

   510 by arith

   511

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

   513 by arith

   514

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

   516 by arith

   517

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

   519 by arith

   520

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

   522 by arith

   523

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

   525 by arith

   526

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

   528 by arith

   529

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

   531 by arith

   532

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

   534 by arith

   535

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

   537 by arith

   538

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

   540 by arith

   541

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

   543 by arith

   544

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

   546 by arith

   547

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

   549 by arith

   550

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

   552 by arith

   553

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

   555 by arith

   556

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

   558 by arith

   559

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

   561 by arith

   562

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

   564 by arith

   565

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

   567 by arith

   568

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

   570 by arith

   571

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

   573 by arith

   574

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

   576 by arith

   577

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

   579 by arith

   580

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

   582 by arith

   583

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

   585 by arith

   586

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

   588 by arith

   589

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

   591 by arith

   592

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

   594 by arith

   595

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

   597 by arith

   598

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

   600 by arith

   601

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

   603 by arith

   604

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

   606 by arith

   607

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

   609 by arith

   610

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

   612 by arith

   613

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

   615 by arith

   616

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

   618 by arith

   619

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

   621 by arith

   622

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

   624 by arith

   625

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

   627 by arith

   628

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

   630 by arith

   631

   632 lemma "(x + y < z) = (x < z - (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 \<le> y - z) = (x + z \<le> (y::real))"

   642 by arith

   643

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

   645 by arith

   646

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

   648 by arith

   649

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

   651 by arith

   652

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

   654 by arith

   655

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

   657 by arith

   658

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

   660 by arith

   661

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

   663 by arith

   664

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

   666 by arith

   667

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

   669 by arith

   670

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

   672 by arith

   673

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

   675 by arith

   676

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

   678 by arith

   679

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

   681 by arith

   682

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

   684 by arith

   685

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

   687 by arith

   688

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

   690 by arith

   691

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

   693 by arith

   694

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

   696 by arith

   697

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

   699 by arith

   700

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

   702 by arith

   703

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

   705   oops

   706

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

   708 by arith

   709

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

   711 by arith

   712

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

   714 by linarith

   715

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

   717 by linarith

   718

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

   720 by linarith

   721

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

   723 by linarith

   724

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

   726 by linarith

   727

   728 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"

   729 by arith

   730

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

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

   733 by linarith

   734

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

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

   737 by linarith

   738

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

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

   741 by linarith

   742

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

   744     ==> 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"

   745 by linarith

   746

   747

   748 subsection{*Complex Arithmetic*}

   749

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

   751 by simp

   752

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

   754 by simp

   755

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

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

   758

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

   760 by (simp add: ring_distribs)

   761

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

   763 by (simp add: ring_distribs)

   764

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

   766 by (simp add: ring_distribs)

   767

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

   769

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

   771

   772 end