src/HOL/ex/BinEx.thy
 author wenzelm Sun Oct 01 18:29:23 2006 +0200 (2006-10-01) changeset 20807 bd3b60f9a343 parent 16417 9bc16273c2d4 child 28952 15a4b2cf8c34 permissions -rw-r--r--
tuned;
     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