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 \<open>Binary arithmetic examples\<close>
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 \<open>Regression Testing for Cancellation Simprocs\<close>
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 \<open>Arithmetic Method Tests\<close>
paulson@14113
    87
paulson@14113
    88
paulson@14113
    89
lemma "!!a::int. [| a <= b; c <= d; x+y<z |] ==> 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<b; i<j |] ==> 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 \<open>The Integers\<close>
wenzelm@11024
   133
wenzelm@61343
   134
text \<open>Addition\<close>
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 \<open>\medskip Negation\<close>
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 \<open>\medskip Multiplication\<close>
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 \<noteq> 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) \<le> (1000001 + 1) - 2"
wenzelm@11024
   185
  by simp
wenzelm@11024
   186
wenzelm@11704
   187
lemma "(1234567::int) \<le> 1234567"
wenzelm@11024
   188
  by simp
wenzelm@11024
   189
wenzelm@61343
   190
text\<open>No integer overflow!\<close>
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 \<open>\medskip Quotient and Remainder\<close>
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 \<open>A negative divisor\<close>
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 \<open>
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
\<close>
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 \<open>A negative dividend \emph{and} divisor\<close>
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 \<open>A few bigger examples\<close>
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 \<open>\medskip Division by shifting\<close>
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 \<open>\medskip Powers\<close>
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 \<open>The Natural Numbers\<close>
wenzelm@11024
   282
wenzelm@61343
   283
text \<open>Successor\<close>
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 \<open>\medskip Addition\<close>
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 \<open>\medskip Subtraction\<close>
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 \<open>\medskip Multiplication\<close>
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 \<open>\medskip Quotient and Remainder\<close>
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 \<open>\medskip Powers\<close>
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 \<open>\medskip Testing the cancellation of complementary terms\<close>
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\<open>Real Arithmetic\<close>
haftmann@28952
   395
wenzelm@61343
   396
subsubsection \<open>Addition\<close>
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 \<open>Negation\<close>
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 \<open>Multiplication\<close>
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 \<open>Inequalities\<close>
haftmann@28952
   427
haftmann@28952
   428
lemma "(89::real) * 10 \<noteq> 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) \<le> (1000001 + 1) - 2"
haftmann@28952
   441
by simp
haftmann@28952
   442
haftmann@28952
   443
lemma "(1234567::real) \<le> 1234567"
haftmann@28952
   444
by simp
haftmann@28952
   445
haftmann@28952
   446
wenzelm@61343
   447
subsubsection \<open>Powers\<close>
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 \<open>Tests\<close>
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 "(\<not> x < y) = (y \<le> (x::real))"
haftmann@28952
   486
by arith
haftmann@28952
   487
haftmann@28952
   488
lemma "\<not> (x < y \<and> y < (x::real))"
haftmann@28952
   489
by arith
haftmann@28952
   490
haftmann@28952
   491
lemma "(x::real) < y ==> \<not> y < x"
haftmann@28952
   492
by arith
haftmann@28952
   493
haftmann@28952
   494
lemma "((x::real) \<noteq> y) = (x < y \<or> y < x)"
haftmann@28952
   495
by arith
haftmann@28952
   496
haftmann@28952
   497
lemma "(\<not> x \<le> y) = (y < (x::real))"
haftmann@28952
   498
by arith
haftmann@28952
   499
haftmann@28952
   500
lemma "x \<le> y \<or> y \<le> (x::real)"
haftmann@28952
   501
by arith
haftmann@28952
   502
haftmann@28952
   503
lemma "x \<le> y \<or> y < (x::real)"
haftmann@28952
   504
by arith
haftmann@28952
   505
haftmann@28952
   506
lemma "x < y \<or> y \<le> (x::real)"
haftmann@28952
   507
by arith
haftmann@28952
   508
haftmann@28952
   509
lemma "x \<le> (x::real)"
haftmann@28952
   510
by arith
haftmann@28952
   511
haftmann@28952
   512
lemma "((x::real) \<le> y) = (x < y \<or> x = y)"
haftmann@28952
   513
by arith
haftmann@28952
   514
haftmann@28952
   515
lemma "((x::real) \<le> y \<and> y \<le> x) = (x = y)"
haftmann@28952
   516
by arith
haftmann@28952
   517
haftmann@28952
   518
lemma "\<not>(x < y \<and> y \<le> (x::real))"
haftmann@28952
   519
by arith
haftmann@28952
   520
haftmann@28952
   521
lemma "\<not>(x \<le> y \<and> 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 \<le> (0::real)) = (0 \<le> x)"
haftmann@28952
   531
by arith
haftmann@28952
   532
haftmann@28952
   533
lemma "((0::real) \<le> -x) = (x \<le> 0)"
haftmann@28952
   534
by arith
haftmann@28952
   535
haftmann@28952
   536
lemma "(x::real) = y \<or> x < y \<or> y < x"
haftmann@28952
   537
by arith
haftmann@28952
   538
haftmann@28952
   539
lemma "(x::real) = 0 \<or> 0 < x \<or> 0 < -x"
haftmann@28952
   540
by arith
haftmann@28952
   541
haftmann@28952
   542
lemma "(0::real) \<le> x \<or> 0 \<le> -x"
haftmann@28952
   543
by arith
haftmann@28952
   544
haftmann@28952
   545
lemma "((x::real) + y \<le> x + z) = (y \<le> z)"
haftmann@28952
   546
by arith
haftmann@28952
   547
haftmann@28952
   548
lemma "((x::real) + z \<le> y + z) = (x \<le> y)"
haftmann@28952
   549
by arith
haftmann@28952
   550
haftmann@28952
   551
lemma "(w::real) < x \<and> y < z ==> w + y < x + z"
haftmann@28952
   552
by arith
haftmann@28952
   553
haftmann@28952
   554
lemma "(w::real) \<le> x \<and> y \<le> z ==> w + y \<le> x + z"
haftmann@28952
   555
by arith
haftmann@28952
   556
haftmann@28952
   557
lemma "(0::real) \<le> x \<and> 0 \<le> y ==> 0 \<le> x + y"
haftmann@28952
   558
by arith
haftmann@28952
   559
haftmann@28952
   560
lemma "(0::real) < x \<and> 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 \<le> 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) \<le> x + x) = (0 \<le> x)"
haftmann@28952
   591
by arith
haftmann@28952
   592
haftmann@28952
   593
lemma "(-x \<le> x) = ((0::real) \<le> x)"
haftmann@28952
   594
by arith
haftmann@28952
   595
haftmann@28952
   596
lemma "(x \<le> -x) = (x \<le> (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) \<le> x - y) = (y \<le> 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) ==> \<not>(x = y)"
haftmann@28952
   618
by arith
haftmann@28952
   619
haftmann@28952
   620
lemma "(x \<le> x + y) = ((0::real) \<le> y)"
haftmann@28952
   621
by arith
haftmann@28952
   622
haftmann@28952
   623
lemma "(y \<le> x + y) = ((0::real) \<le> 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 \<le> y - z) = (x + z \<le> (y::real))"
haftmann@28952
   645
by arith
haftmann@28952
   646
haftmann@28952
   647
lemma "(x - y \<le> z) = (x \<le> 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 \<le> -y) = (y \<le> (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 \<le> x \<and> y < z ==> w + y < x + (z::real)"
haftmann@28952
   666
by arith
haftmann@28952
   667
haftmann@28952
   668
lemma "w < x \<and> y \<le> z ==> w + y < x + (z::real)"
haftmann@28952
   669
by arith
haftmann@28952
   670
haftmann@28952
   671
lemma "(0::real) \<le> x \<and> 0 < y ==> 0 < x + (y::real)"
haftmann@28952
   672
by arith
haftmann@28952
   673
haftmann@28952
   674
lemma "(0::real) < x \<and> 0 \<le> 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 \<le> (y::real)"
haftmann@28952
   702
by arith
haftmann@28952
   703
haftmann@28952
   704
lemma "(0::real) < x ==> \<not>(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 \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d"
haftmann@31066
   717
by linarith
haftmann@28952
   718
haftmann@28952
   719
lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)"
haftmann@31066
   720
by linarith
haftmann@28952
   721
haftmann@28952
   722
lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c"
haftmann@31066
   723
by linarith
haftmann@28952
   724
haftmann@28952
   725
lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> 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 \<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"
haftmann@28952
   732
by arith
haftmann@28952
   733
haftmann@28952
   734
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
haftmann@28952
   735
    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l"
haftmann@31066
   736
by linarith
haftmann@28952
   737
haftmann@28952
   738
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
haftmann@28952
   739
    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l"
haftmann@31066
   740
by linarith
haftmann@28952
   741
haftmann@28952
   742
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
haftmann@28952
   743
    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i"
haftmann@31066
   744
by linarith
haftmann@28952
   745
haftmann@28952
   746
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
haftmann@28952
   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"
haftmann@31066
   748
by linarith
haftmann@28952
   749
haftmann@28952
   750
wenzelm@61343
   751
subsection\<open>Complex Arithmetic\<close>
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\<open>Multiplication requires distributive laws.  Perhaps versions instantiated
wenzelm@61343
   760
to literal constants should be added to the simpset.\<close>
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\<open>No inequalities or linear arithmetic: the complex numbers are unordered!\<close>
haftmann@28952
   772
wenzelm@61343
   773
text\<open>No powers (not supported yet)\<close>
haftmann@28952
   774
paulson@5545
   775
end