src/HOL/ex/BinEx.thy
 author nipkow Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) changeset 30313 b2441b0c8d38 parent 28952 15a4b2cf8c34 child 31066 972c870da225 permissions -rw-r--r--
     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 add: Suc_nat_number_of)

   284     -- {* not a default rewrite since sometimes we want to have @{text "Suc nnn"} *}

   285

   286

   287 text {* \medskip Addition *}

   288

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

   290   by simp

   291

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

   293   by simp

   294

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

   296   by simp

   297

   298

   299 text {* \medskip Subtraction *}

   300

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

   302   by simp

   303

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

   305   by simp

   306

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

   308   by simp

   309

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

   311   by simp

   312

   313

   314 text {* \medskip Multiplication *}

   315

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

   317   by simp

   318

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

   320   by simp

   321

   322

   323 text {* \medskip Quotient and Remainder *}

   324

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

   326   by simp

   327

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

   329   by simp

   330

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

   332   by simp

   333

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

   335   by simp

   336

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

   338   by simp

   339

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

   341   by simp

   342

   343

   344 text {* \medskip Powers *}

   345

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

   347   by simp

   348

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

   350   by simp

   351

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

   353   by simp

   354

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

   356   by simp

   357

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

   359   by simp

   360

   361

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

   363

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

   365   by simp

   366

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

   368   by simp

   369

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

   371   by simp

   372

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

   374   by simp

   375

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

   377   by simp

   378

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

   380   by simp

   381

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

   383   by simp

   384

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

   386   by simp

   387

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

   389   by simp

   390

   391

   392 subsection{*Real Arithmetic*}

   393

   394 subsubsection {*Addition *}

   395

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

   397 by simp

   398

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

   400 by simp

   401

   402

   403 subsubsection {*Negation *}

   404

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

   406 by simp

   407

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

   409 by simp

   410

   411

   412 subsubsection {*Multiplication *}

   413

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

   415 by simp

   416

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

   418 by simp

   419

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

   421 by simp

   422

   423

   424 subsubsection {*Inequalities *}

   425

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

   427 by simp

   428

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

   430 by simp

   431

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

   433 by simp

   434

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

   436 by simp

   437

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

   439 by simp

   440

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

   442 by simp

   443

   444

   445 subsubsection {*Powers *}

   446

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

   448 by simp

   449

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

   451 by simp

   452

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

   454 by simp

   455

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

   457 by simp

   458

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

   460 by simp

   461

   462

   463 subsubsection {*Tests *}

   464

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

   466 by arith

   467

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

   469 by arith

   470

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

   472 by arith

   473

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

   475 by arith

   476

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

   478 by arith

   479

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

   481 by arith

   482

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

   484 by arith

   485

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

   487 by arith

   488

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

   490 by arith

   491

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

   493 by arith

   494

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

   496 by arith

   497

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

   499 by arith

   500

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

   502 by arith

   503

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

   505 by arith

   506

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

   508 by arith

   509

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

   511 by arith

   512

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

   514 by arith

   515

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

   517 by arith

   518

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

   520 by arith

   521

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

   523 by arith

   524

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

   526 by arith

   527

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

   529 by arith

   530

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

   532 by arith

   533

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

   535 by arith

   536

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

   538 by arith

   539

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

   541 by arith

   542

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

   544 by arith

   545

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

   547 by arith

   548

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

   550 by arith

   551

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

   553 by arith

   554

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

   556 by arith

   557

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

   559 by arith

   560

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

   562 by arith

   563

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

   565 by arith

   566

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

   568 by arith

   569

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

   571 by arith

   572

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

   574 by arith

   575

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

   577 by arith

   578

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

   580 by arith

   581

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

   583 by arith

   584

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

   586 by arith

   587

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

   589 by arith

   590

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

   592 by arith

   593

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

   595 by arith

   596

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

   598 by arith

   599

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

   601 by arith

   602

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

   604 by arith

   605

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

   607 by arith

   608

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

   610 by arith

   611

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

   613 by arith

   614

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

   616 by arith

   617

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

   619 by arith

   620

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

   622 by arith

   623

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

   625 by arith

   626

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

   628 by arith

   629

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

   631 by arith

   632

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

   634 by arith

   635

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

   637 by arith

   638

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

   640 by arith

   641

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

   643 by arith

   644

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

   646 by arith

   647

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

   649 by arith

   650

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

   652 by arith

   653

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

   655 by arith

   656

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

   658 by arith

   659

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

   661 by arith

   662

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

   664 by arith

   665

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

   667 by arith

   668

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

   670 by arith

   671

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

   673 by arith

   674

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

   676 by arith

   677

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

   679 by arith

   680

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

   682 by arith

   683

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

   685 by arith

   686

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

   688 by arith

   689

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

   691 by arith

   692

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

   694 by arith

   695

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

   697 by arith

   698

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

   700 by arith

   701

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

   703 by arith

   704

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

   706   oops

   707

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

   709 by arith

   710

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

   712 by arith

   713

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

   715 by (tactic "fast_arith_tac @{context} 1")

   716

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

   718 by (tactic "fast_arith_tac @{context} 1")

   719

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

   721 by (tactic "fast_arith_tac @{context} 1")

   722

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

   724 by (tactic "fast_arith_tac @{context} 1")

   725

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

   727 by (tactic "fast_arith_tac @{context} 1")

   728

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

   730 by arith

   731

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

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

   734 by (tactic "fast_arith_tac @{context} 1")

   735

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

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

   738 by (tactic "fast_arith_tac @{context} 1")

   739

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

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

   742 by (tactic "fast_arith_tac @{context} 1")

   743

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

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

   746 by (tactic "fast_arith_tac @{context} 1")

   747

   748

   749 subsection{*Complex Arithmetic*}

   750

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

   752 by simp

   753

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

   755 by simp

   756

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

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

   759

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

   761 by (simp add: ring_distribs)

   762

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

   764 by (simp add: ring_distribs)

   765

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

   767 by (simp add: ring_distribs)

   768

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

   770

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

   772

   773 end