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
     1 (*  Title:      HOL/ex/BinEx.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 *)
     6 
     7 header {* Binary arithmetic examples *}
     8 
     9 theory BinEx imports Main begin
    10 
    11 subsection {* Regression Testing for Cancellation Simprocs *}
    12 
    13 lemma "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
    14 apply simp  oops
    15 
    16 lemma "2*u = (u::int)"
    17 apply simp  oops
    18 
    19 lemma "(i + j + 12 + (k::int)) - 15 = y"
    20 apply simp  oops
    21 
    22 lemma "(i + j + 12 + (k::int)) - 5 = y"
    23 apply simp  oops
    24 
    25 lemma "y - b < (b::int)"
    26 apply simp  oops
    27 
    28 lemma "y - (3*b + c) < (b::int) - 2*c"
    29 apply simp  oops
    30 
    31 lemma "(2*x - (u*v) + y) - v*3*u = (w::int)"
    32 apply simp  oops
    33 
    34 lemma "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"
    35 apply simp  oops
    36 
    37 lemma "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"
    38 apply simp  oops
    39 
    40 lemma "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"
    41 apply simp  oops
    42 
    43 lemma "(i + j + 12 + (k::int)) = u + 15 + y"
    44 apply simp  oops
    45 
    46 lemma "(i + j*2 + 12 + (k::int)) = j + 5 + y"
    47 apply simp  oops
    48 
    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)"
    50 apply simp  oops
    51 
    52 lemma "a + -(b+c) + b = (d::int)"
    53 apply simp  oops
    54 
    55 lemma "a + -(b+c) - b = (d::int)"
    56 apply simp  oops
    57 
    58 (*negative numerals*)
    59 lemma "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"
    60 apply simp  oops
    61 
    62 lemma "(i + j + -3 + (k::int)) < u + 5 + y"
    63 apply simp  oops
    64 
    65 lemma "(i + j + 3 + (k::int)) < u + -6 + y"
    66 apply simp  oops
    67 
    68 lemma "(i + j + -12 + (k::int)) - 15 = y"
    69 apply simp  oops
    70 
    71 lemma "(i + j + 12 + (k::int)) - -15 = y"
    72 apply simp  oops
    73 
    74 lemma "(i + j + -12 + (k::int)) - -15 = y"
    75 apply simp  oops
    76 
    77 lemma "- (2*i) + 3  + (2*i + 4) = (0::int)"
    78 apply simp  oops
    79 
    80 
    81 
    82 subsection {* Arithmetic Method Tests *}
    83 
    84 
    85 lemma "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"
    86 by arith
    87 
    88 lemma "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)"
    89 by arith
    90 
    91 lemma "!!a::int. [| a < b; c < d |] ==> a+c+ 1 < b+d"
    92 by arith
    93 
    94 lemma "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"
    95 by arith
    96 
    97 lemma "!!a::int. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"
    98 by arith
    99 
   100 lemma "!!a::int. [| a+b < i+j; a<b; i<j |] ==> a+a - - -1 < j+j - 3"
   101 by arith
   102 
   103 lemma "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"
   104 by arith
   105 
   106 lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
   107       ==> a <= l"
   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+a+a+a <= l+l+l+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+a <= l+l+l+l+i"
   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+a <= l+l+l+l+i+l"
   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       ==> 6*a <= 5*l+i"
   124 by arith
   125 
   126 
   127 
   128 subsection {* The Integers *}
   129 
   130 text {* Addition *}
   131 
   132 lemma "(13::int) + 19 = 32"
   133   by simp
   134 
   135 lemma "(1234::int) + 5678 = 6912"
   136   by simp
   137 
   138 lemma "(1359::int) + -2468 = -1109"
   139   by simp
   140 
   141 lemma "(93746::int) + -46375 = 47371"
   142   by simp
   143 
   144 
   145 text {* \medskip Negation *}
   146 
   147 lemma "- (65745::int) = -65745"
   148   by simp
   149 
   150 lemma "- (-54321::int) = 54321"
   151   by simp
   152 
   153 
   154 text {* \medskip Multiplication *}
   155 
   156 lemma "(13::int) * 19 = 247"
   157   by simp
   158 
   159 lemma "(-84::int) * 51 = -4284"
   160   by simp
   161 
   162 lemma "(255::int) * 255 = 65025"
   163   by simp
   164 
   165 lemma "(1359::int) * -2468 = -3354012"
   166   by simp
   167 
   168 lemma "(89::int) * 10 \<noteq> 889"
   169   by simp
   170 
   171 lemma "(13::int) < 18 - 4"
   172   by simp
   173 
   174 lemma "(-345::int) < -242 + -100"
   175   by simp
   176 
   177 lemma "(13557456::int) < 18678654"
   178   by simp
   179 
   180 lemma "(999999::int) \<le> (1000001 + 1) - 2"
   181   by simp
   182 
   183 lemma "(1234567::int) \<le> 1234567"
   184   by simp
   185 
   186 text{*No integer overflow!*}
   187 lemma "1234567 * (1234567::int) < 1234567*1234567*1234567"
   188   by simp
   189 
   190 
   191 text {* \medskip Quotient and Remainder *}
   192 
   193 lemma "(10::int) div 3 = 3"
   194   by simp
   195 
   196 lemma "(10::int) mod 3 = 1"
   197   by simp
   198 
   199 text {* A negative divisor *}
   200 
   201 lemma "(10::int) div -3 = -4"
   202   by simp
   203 
   204 lemma "(10::int) mod -3 = -2"
   205   by simp
   206 
   207 text {*
   208   A negative dividend\footnote{The definition agrees with mathematical
   209   convention and with ML, but not with the hardware of most computers}
   210 *}
   211 
   212 lemma "(-10::int) div 3 = -4"
   213   by simp
   214 
   215 lemma "(-10::int) mod 3 = 2"
   216   by simp
   217 
   218 text {* A negative dividend \emph{and} divisor *}
   219 
   220 lemma "(-10::int) div -3 = 3"
   221   by simp
   222 
   223 lemma "(-10::int) mod -3 = -1"
   224   by simp
   225 
   226 text {* A few bigger examples *}
   227 
   228 lemma "(8452::int) mod 3 = 1"
   229   by simp
   230 
   231 lemma "(59485::int) div 434 = 137"
   232   by simp
   233 
   234 lemma "(1000006::int) mod 10 = 6"
   235   by simp
   236 
   237 
   238 text {* \medskip Division by shifting *}
   239 
   240 lemma "10000000 div 2 = (5000000::int)"
   241   by simp
   242 
   243 lemma "10000001 mod 2 = (1::int)"
   244   by simp
   245 
   246 lemma "10000055 div 32 = (312501::int)"
   247   by simp
   248 
   249 lemma "10000055 mod 32 = (23::int)"
   250   by simp
   251 
   252 lemma "100094 div 144 = (695::int)"
   253   by simp
   254 
   255 lemma "100094 mod 144 = (14::int)"
   256   by simp
   257 
   258 
   259 text {* \medskip Powers *}
   260 
   261 lemma "2 ^ 10 = (1024::int)"
   262   by simp
   263 
   264 lemma "-3 ^ 7 = (-2187::int)"
   265   by simp
   266 
   267 lemma "13 ^ 7 = (62748517::int)"
   268   by simp
   269 
   270 lemma "3 ^ 15 = (14348907::int)"
   271   by simp
   272 
   273 lemma "-5 ^ 11 = (-48828125::int)"
   274   by simp
   275 
   276 
   277 subsection {* The Natural Numbers *}
   278 
   279 text {* Successor *}
   280 
   281 lemma "Suc 99999 = 100000"
   282   by (simp add: Suc_nat_number_of)
   283     -- {* not a default rewrite since sometimes we want to have @{text "Suc nnn"} *}
   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 end