src/HOL/ex/BinEx.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 20807 bd3b60f9a343
child 28952 15a4b2cf8c34
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
paulson@5545
     1
(*  Title:      HOL/ex/BinEx.thy
paulson@5545
     2
    ID:         $Id$
paulson@5545
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5545
     4
    Copyright   1998  University of Cambridge
paulson@5545
     5
*)
paulson@5545
     6
wenzelm@11024
     7
header {* Binary arithmetic examples *}
wenzelm@11024
     8
haftmann@16417
     9
theory BinEx imports Main begin
wenzelm@11024
    10
paulson@14113
    11
subsection {* Regression Testing for Cancellation Simprocs *}
paulson@14113
    12
paulson@14113
    13
lemma "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
paulson@14113
    14
apply simp  oops
paulson@14113
    15
paulson@14113
    16
lemma "2*u = (u::int)"
paulson@14113
    17
apply simp  oops
paulson@14113
    18
paulson@14113
    19
lemma "(i + j + 12 + (k::int)) - 15 = y"
paulson@14113
    20
apply simp  oops
paulson@14113
    21
paulson@14113
    22
lemma "(i + j + 12 + (k::int)) - 5 = y"
paulson@14113
    23
apply simp  oops
paulson@14113
    24
paulson@14113
    25
lemma "y - b < (b::int)"
paulson@14113
    26
apply simp  oops
paulson@14113
    27
paulson@14113
    28
lemma "y - (3*b + c) < (b::int) - 2*c"
paulson@14113
    29
apply simp  oops
paulson@14113
    30
paulson@14113
    31
lemma "(2*x - (u*v) + y) - v*3*u = (w::int)"
paulson@14113
    32
apply simp  oops
paulson@14113
    33
paulson@14113
    34
lemma "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"
paulson@14113
    35
apply simp  oops
paulson@14113
    36
paulson@14113
    37
lemma "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"
paulson@14113
    38
apply simp  oops
paulson@14113
    39
paulson@14113
    40
lemma "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"
paulson@14113
    41
apply simp  oops
paulson@14113
    42
paulson@14113
    43
lemma "(i + j + 12 + (k::int)) = u + 15 + y"
paulson@14113
    44
apply simp  oops
paulson@14113
    45
paulson@14113
    46
lemma "(i + j*2 + 12 + (k::int)) = j + 5 + y"
paulson@14113
    47
apply simp  oops
paulson@14113
    48
paulson@14113
    49
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
    50
apply simp  oops
paulson@14113
    51
paulson@14113
    52
lemma "a + -(b+c) + b = (d::int)"
paulson@14113
    53
apply simp  oops
paulson@14113
    54
paulson@14113
    55
lemma "a + -(b+c) - b = (d::int)"
paulson@14113
    56
apply simp  oops
paulson@14113
    57
paulson@14113
    58
(*negative numerals*)
paulson@14113
    59
lemma "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"
paulson@14113
    60
apply simp  oops
paulson@14113
    61
paulson@14113
    62
lemma "(i + j + -3 + (k::int)) < u + 5 + y"
paulson@14113
    63
apply simp  oops
paulson@14113
    64
paulson@14113
    65
lemma "(i + j + 3 + (k::int)) < u + -6 + y"
paulson@14113
    66
apply simp  oops
paulson@14113
    67
paulson@14113
    68
lemma "(i + j + -12 + (k::int)) - 15 = y"
paulson@14113
    69
apply simp  oops
paulson@14113
    70
paulson@14113
    71
lemma "(i + j + 12 + (k::int)) - -15 = y"
paulson@14113
    72
apply simp  oops
paulson@14113
    73
paulson@14113
    74
lemma "(i + j + -12 + (k::int)) - -15 = y"
paulson@14113
    75
apply simp  oops
paulson@14113
    76
paulson@14124
    77
lemma "- (2*i) + 3  + (2*i + 4) = (0::int)"
paulson@14124
    78
apply simp  oops
paulson@14124
    79
paulson@14124
    80
paulson@14113
    81
paulson@14113
    82
subsection {* Arithmetic Method Tests *}
paulson@14113
    83
paulson@14113
    84
paulson@14113
    85
lemma "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"
paulson@14113
    86
by arith
paulson@14113
    87
paulson@14113
    88
lemma "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)"
paulson@14113
    89
by arith
paulson@14113
    90
paulson@14113
    91
lemma "!!a::int. [| a < b; c < d |] ==> a+c+ 1 < b+d"
paulson@14113
    92
by arith
paulson@14113
    93
paulson@14113
    94
lemma "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"
paulson@14113
    95
by arith
paulson@14113
    96
paulson@14113
    97
lemma "!!a::int. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"
paulson@14113
    98
by arith
paulson@14113
    99
paulson@14113
   100
lemma "!!a::int. [| a+b < i+j; a<b; i<j |] ==> a+a - - -1 < j+j - 3"
paulson@14113
   101
by arith
paulson@14113
   102
paulson@14113
   103
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
   104
by arith
paulson@14113
   105
paulson@14113
   106
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
   107
      ==> a <= l"
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+a+a+a <= l+l+l+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+a <= l+l+l+l+i"
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+a <= l+l+l+l+i+l"
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
      ==> 6*a <= 5*l+i"
paulson@14113
   124
by arith
paulson@14113
   125
paulson@14113
   126
paulson@14113
   127
wenzelm@11024
   128
subsection {* The Integers *}
wenzelm@11024
   129
wenzelm@11024
   130
text {* Addition *}
wenzelm@11024
   131
wenzelm@11704
   132
lemma "(13::int) + 19 = 32"
wenzelm@11024
   133
  by simp
wenzelm@11024
   134
wenzelm@11704
   135
lemma "(1234::int) + 5678 = 6912"
wenzelm@11024
   136
  by simp
wenzelm@11024
   137
wenzelm@11704
   138
lemma "(1359::int) + -2468 = -1109"
wenzelm@11024
   139
  by simp
wenzelm@11024
   140
wenzelm@11704
   141
lemma "(93746::int) + -46375 = 47371"
wenzelm@11024
   142
  by simp
wenzelm@11024
   143
wenzelm@11024
   144
wenzelm@11024
   145
text {* \medskip Negation *}
wenzelm@11024
   146
wenzelm@11704
   147
lemma "- (65745::int) = -65745"
wenzelm@11024
   148
  by simp
wenzelm@11024
   149
wenzelm@11704
   150
lemma "- (-54321::int) = 54321"
wenzelm@11024
   151
  by simp
wenzelm@11024
   152
wenzelm@11024
   153
wenzelm@11024
   154
text {* \medskip Multiplication *}
wenzelm@11024
   155
wenzelm@11704
   156
lemma "(13::int) * 19 = 247"
wenzelm@11024
   157
  by simp
wenzelm@11024
   158
wenzelm@11704
   159
lemma "(-84::int) * 51 = -4284"
wenzelm@11024
   160
  by simp
wenzelm@11024
   161
wenzelm@11704
   162
lemma "(255::int) * 255 = 65025"
wenzelm@11024
   163
  by simp
wenzelm@11024
   164
wenzelm@11704
   165
lemma "(1359::int) * -2468 = -3354012"
wenzelm@11024
   166
  by simp
wenzelm@11024
   167
wenzelm@11704
   168
lemma "(89::int) * 10 \<noteq> 889"
wenzelm@11024
   169
  by simp
wenzelm@11024
   170
wenzelm@11704
   171
lemma "(13::int) < 18 - 4"
wenzelm@11024
   172
  by simp
wenzelm@11024
   173
wenzelm@11704
   174
lemma "(-345::int) < -242 + -100"
wenzelm@11024
   175
  by simp
wenzelm@11024
   176
wenzelm@11704
   177
lemma "(13557456::int) < 18678654"
wenzelm@11024
   178
  by simp
wenzelm@11024
   179
paulson@11868
   180
lemma "(999999::int) \<le> (1000001 + 1) - 2"
wenzelm@11024
   181
  by simp
wenzelm@11024
   182
wenzelm@11704
   183
lemma "(1234567::int) \<le> 1234567"
wenzelm@11024
   184
  by simp
wenzelm@11024
   185
paulson@15965
   186
text{*No integer overflow!*}
paulson@15965
   187
lemma "1234567 * (1234567::int) < 1234567*1234567*1234567"
paulson@15965
   188
  by simp
paulson@15965
   189
wenzelm@11024
   190
wenzelm@11024
   191
text {* \medskip Quotient and Remainder *}
wenzelm@11024
   192
wenzelm@11704
   193
lemma "(10::int) div 3 = 3"
wenzelm@11024
   194
  by simp
wenzelm@11024
   195
paulson@11868
   196
lemma "(10::int) mod 3 = 1"
wenzelm@11024
   197
  by simp
wenzelm@11024
   198
wenzelm@11024
   199
text {* A negative divisor *}
wenzelm@11024
   200
wenzelm@11704
   201
lemma "(10::int) div -3 = -4"
wenzelm@11024
   202
  by simp
wenzelm@11024
   203
wenzelm@11704
   204
lemma "(10::int) mod -3 = -2"
wenzelm@11024
   205
  by simp
paulson@5545
   206
wenzelm@11024
   207
text {*
wenzelm@11024
   208
  A negative dividend\footnote{The definition agrees with mathematical
paulson@15965
   209
  convention and with ML, but not with the hardware of most computers}
wenzelm@11024
   210
*}
wenzelm@11024
   211
wenzelm@11704
   212
lemma "(-10::int) div 3 = -4"
wenzelm@11024
   213
  by simp
wenzelm@11024
   214
wenzelm@11704
   215
lemma "(-10::int) mod 3 = 2"
wenzelm@11024
   216
  by simp
wenzelm@11024
   217
wenzelm@11024
   218
text {* A negative dividend \emph{and} divisor *}
wenzelm@11024
   219
wenzelm@11704
   220
lemma "(-10::int) div -3 = 3"
wenzelm@11024
   221
  by simp
wenzelm@11024
   222
wenzelm@11704
   223
lemma "(-10::int) mod -3 = -1"
wenzelm@11024
   224
  by simp
wenzelm@11024
   225
wenzelm@11024
   226
text {* A few bigger examples *}
wenzelm@11024
   227
paulson@11868
   228
lemma "(8452::int) mod 3 = 1"
wenzelm@11024
   229
  by simp
wenzelm@11024
   230
wenzelm@11704
   231
lemma "(59485::int) div 434 = 137"
wenzelm@11024
   232
  by simp
wenzelm@11024
   233
wenzelm@11704
   234
lemma "(1000006::int) mod 10 = 6"
wenzelm@11024
   235
  by simp
wenzelm@11024
   236
wenzelm@11024
   237
wenzelm@11024
   238
text {* \medskip Division by shifting *}
wenzelm@11024
   239
wenzelm@11704
   240
lemma "10000000 div 2 = (5000000::int)"
wenzelm@11024
   241
  by simp
wenzelm@11024
   242
paulson@11868
   243
lemma "10000001 mod 2 = (1::int)"
wenzelm@11024
   244
  by simp
wenzelm@11024
   245
wenzelm@11704
   246
lemma "10000055 div 32 = (312501::int)"
wenzelm@11024
   247
  by simp
wenzelm@11024
   248
wenzelm@11704
   249
lemma "10000055 mod 32 = (23::int)"
wenzelm@11024
   250
  by simp
wenzelm@11024
   251
wenzelm@11704
   252
lemma "100094 div 144 = (695::int)"
wenzelm@11024
   253
  by simp
wenzelm@11024
   254
wenzelm@11704
   255
lemma "100094 mod 144 = (14::int)"
wenzelm@11024
   256
  by simp
wenzelm@11024
   257
wenzelm@11024
   258
paulson@12613
   259
text {* \medskip Powers *}
paulson@12613
   260
paulson@12613
   261
lemma "2 ^ 10 = (1024::int)"
paulson@12613
   262
  by simp
paulson@12613
   263
paulson@12613
   264
lemma "-3 ^ 7 = (-2187::int)"
paulson@12613
   265
  by simp
paulson@12613
   266
paulson@12613
   267
lemma "13 ^ 7 = (62748517::int)"
paulson@12613
   268
  by simp
paulson@12613
   269
paulson@12613
   270
lemma "3 ^ 15 = (14348907::int)"
paulson@12613
   271
  by simp
paulson@12613
   272
paulson@12613
   273
lemma "-5 ^ 11 = (-48828125::int)"
paulson@12613
   274
  by simp
paulson@12613
   275
paulson@12613
   276
wenzelm@11024
   277
subsection {* The Natural Numbers *}
wenzelm@11024
   278
wenzelm@11024
   279
text {* Successor *}
wenzelm@11024
   280
wenzelm@11704
   281
lemma "Suc 99999 = 100000"
wenzelm@11024
   282
  by (simp add: Suc_nat_number_of)
wenzelm@20807
   283
    -- {* not a default rewrite since sometimes we want to have @{text "Suc nnn"} *}
wenzelm@11024
   284
wenzelm@11024
   285
wenzelm@11024
   286
text {* \medskip Addition *}
wenzelm@11024
   287
wenzelm@11704
   288
lemma "(13::nat) + 19 = 32"
wenzelm@11024
   289
  by simp
wenzelm@11024
   290
wenzelm@11704
   291
lemma "(1234::nat) + 5678 = 6912"
wenzelm@11024
   292
  by simp
wenzelm@11024
   293
wenzelm@11704
   294
lemma "(973646::nat) + 6475 = 980121"
wenzelm@11024
   295
  by simp
wenzelm@11024
   296
wenzelm@11024
   297
wenzelm@11024
   298
text {* \medskip Subtraction *}
wenzelm@11024
   299
wenzelm@11704
   300
lemma "(32::nat) - 14 = 18"
wenzelm@11024
   301
  by simp
wenzelm@11024
   302
paulson@11868
   303
lemma "(14::nat) - 15 = 0"
wenzelm@11024
   304
  by simp
paulson@5545
   305
paulson@11868
   306
lemma "(14::nat) - 1576644 = 0"
wenzelm@11024
   307
  by simp
wenzelm@11024
   308
wenzelm@11704
   309
lemma "(48273776::nat) - 3873737 = 44400039"
wenzelm@11024
   310
  by simp
wenzelm@11024
   311
wenzelm@11024
   312
wenzelm@11024
   313
text {* \medskip Multiplication *}
wenzelm@11024
   314
wenzelm@11704
   315
lemma "(12::nat) * 11 = 132"
wenzelm@11024
   316
  by simp
wenzelm@11024
   317
wenzelm@11704
   318
lemma "(647::nat) * 3643 = 2357021"
wenzelm@11024
   319
  by simp
wenzelm@11024
   320
wenzelm@11024
   321
wenzelm@11024
   322
text {* \medskip Quotient and Remainder *}
wenzelm@11024
   323
wenzelm@11704
   324
lemma "(10::nat) div 3 = 3"
wenzelm@11024
   325
  by simp
wenzelm@11024
   326
paulson@11868
   327
lemma "(10::nat) mod 3 = 1"
wenzelm@11024
   328
  by simp
wenzelm@11024
   329
wenzelm@11704
   330
lemma "(10000::nat) div 9 = 1111"
wenzelm@11024
   331
  by simp
wenzelm@11024
   332
paulson@11868
   333
lemma "(10000::nat) mod 9 = 1"
wenzelm@11024
   334
  by simp
wenzelm@11024
   335
wenzelm@11704
   336
lemma "(10000::nat) div 16 = 625"
wenzelm@11024
   337
  by simp
wenzelm@11024
   338
paulson@11868
   339
lemma "(10000::nat) mod 16 = 0"
wenzelm@11024
   340
  by simp
wenzelm@11024
   341
paulson@5545
   342
paulson@12613
   343
text {* \medskip Powers *}
paulson@12613
   344
paulson@12613
   345
lemma "2 ^ 12 = (4096::nat)"
paulson@12613
   346
  by simp
paulson@12613
   347
paulson@12613
   348
lemma "3 ^ 10 = (59049::nat)"
paulson@12613
   349
  by simp
paulson@12613
   350
paulson@12613
   351
lemma "12 ^ 7 = (35831808::nat)"
paulson@12613
   352
  by simp
paulson@12613
   353
paulson@12613
   354
lemma "3 ^ 14 = (4782969::nat)"
paulson@12613
   355
  by simp
paulson@12613
   356
paulson@12613
   357
lemma "5 ^ 11 = (48828125::nat)"
paulson@12613
   358
  by simp
paulson@12613
   359
paulson@12613
   360
wenzelm@11024
   361
text {* \medskip Testing the cancellation of complementary terms *}
wenzelm@11024
   362
paulson@11868
   363
lemma "y + (x + -x) = (0::int) + y"
wenzelm@11024
   364
  by simp
wenzelm@11024
   365
paulson@11868
   366
lemma "y + (-x + (- y + x)) = (0::int)"
wenzelm@11024
   367
  by simp
wenzelm@11024
   368
paulson@11868
   369
lemma "-x + (y + (- y + x)) = (0::int)"
wenzelm@11024
   370
  by simp
wenzelm@11024
   371
paulson@11868
   372
lemma "x + (x + (- x + (- x + (- y + - z)))) = (0::int) - y - z"
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 + y + z - (x + z) = y - (0::int)"
wenzelm@11024
   379
  by simp
wenzelm@11024
   380
paulson@11868
   381
lemma "x + (y + (y + (y + (-x + -x)))) = (0::int) + y - x + y + y"
wenzelm@11024
   382
  by simp
wenzelm@11024
   383
paulson@11868
   384
lemma "x + (y + (y + (y + (-y + -x)))) = y + (0::int) + y"
wenzelm@11024
   385
  by simp
wenzelm@11024
   386
paulson@11868
   387
lemma "x + y - x + z - x - y - z + x < (1::int)"
wenzelm@11024
   388
  by simp
wenzelm@11024
   389
paulson@5545
   390
end