src/HOL/Complex/ex/BinEx.thy
author paulson
Tue Feb 03 11:06:36 2004 +0100 (2004-02-03)
changeset 14373 67a628beb981
parent 14051 4b61bbb0dcab
child 15149 c5c4884634b7
permissions -rw-r--r--
tidying of the complex numbers
paulson@14051
     1
(*  Title:      HOL/Complex/ex/BinEx.thy
paulson@13966
     2
    ID:         $Id$
paulson@13966
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@13966
     4
    Copyright   1999  University of Cambridge
paulson@13966
     5
*)
paulson@13966
     6
paulson@13966
     7
header {* Binary arithmetic examples *}
paulson@13966
     8
paulson@14051
     9
theory BinEx = Complex_Main:
paulson@13966
    10
paulson@13966
    11
text {*
paulson@14051
    12
  Examples of performing binary arithmetic by simplification.  This time
paulson@13966
    13
  we use the reals, though the representation is just of integers.
paulson@13966
    14
*}
paulson@13966
    15
paulson@14051
    16
subsection{*Real Arithmetic*}
paulson@14051
    17
paulson@14051
    18
subsubsection {*Addition *}
paulson@13966
    19
paulson@13966
    20
lemma "(1359::real) + -2468 = -1109"
paulson@13966
    21
  by simp
paulson@13966
    22
paulson@13966
    23
lemma "(93746::real) + -46375 = 47371"
paulson@13966
    24
  by simp
paulson@13966
    25
paulson@13966
    26
paulson@14051
    27
subsubsection {*Negation *}
paulson@13966
    28
paulson@13966
    29
lemma "- (65745::real) = -65745"
paulson@13966
    30
  by simp
paulson@13966
    31
paulson@13966
    32
lemma "- (-54321::real) = 54321"
paulson@13966
    33
  by simp
paulson@13966
    34
paulson@13966
    35
paulson@14051
    36
subsubsection {*Multiplication *}
paulson@13966
    37
paulson@13966
    38
lemma "(-84::real) * 51 = -4284"
paulson@13966
    39
  by simp
paulson@13966
    40
paulson@13966
    41
lemma "(255::real) * 255 = 65025"
paulson@13966
    42
  by simp
paulson@13966
    43
paulson@13966
    44
lemma "(1359::real) * -2468 = -3354012"
paulson@13966
    45
  by simp
paulson@13966
    46
paulson@13966
    47
paulson@14051
    48
subsubsection {*Inequalities *}
paulson@13966
    49
paulson@13966
    50
lemma "(89::real) * 10 \<noteq> 889"
paulson@13966
    51
  by simp
paulson@13966
    52
paulson@13966
    53
lemma "(13::real) < 18 - 4"
paulson@13966
    54
  by simp
paulson@13966
    55
paulson@13966
    56
lemma "(-345::real) < -242 + -100"
paulson@13966
    57
  by simp
paulson@13966
    58
paulson@13966
    59
lemma "(13557456::real) < 18678654"
paulson@13966
    60
  by simp
paulson@13966
    61
paulson@13966
    62
lemma "(999999::real) \<le> (1000001 + 1) - 2"
paulson@13966
    63
  by simp
paulson@13966
    64
paulson@13966
    65
lemma "(1234567::real) \<le> 1234567"
paulson@13966
    66
  by simp
paulson@13966
    67
paulson@13966
    68
paulson@14051
    69
subsubsection {*Powers *}
paulson@13966
    70
paulson@13966
    71
lemma "2 ^ 15 = (32768::real)"
paulson@13966
    72
  by simp
paulson@13966
    73
paulson@13966
    74
lemma "-3 ^ 7 = (-2187::real)"
paulson@13966
    75
  by simp
paulson@13966
    76
paulson@13966
    77
lemma "13 ^ 7 = (62748517::real)"
paulson@13966
    78
  by simp
paulson@13966
    79
paulson@13966
    80
lemma "3 ^ 15 = (14348907::real)"
paulson@13966
    81
  by simp
paulson@13966
    82
paulson@13966
    83
lemma "-5 ^ 11 = (-48828125::real)"
paulson@13966
    84
  by simp
paulson@13966
    85
paulson@13966
    86
paulson@14051
    87
subsubsection {*Tests *}
paulson@13966
    88
paulson@13966
    89
lemma "(x + y = x) = (y = (0::real))"
paulson@13966
    90
  by arith
paulson@13966
    91
paulson@13966
    92
lemma "(x + y = y) = (x = (0::real))"
paulson@13966
    93
  by arith
paulson@13966
    94
paulson@13966
    95
lemma "(x + y = (0::real)) = (x = -y)"
paulson@13966
    96
  by arith
paulson@13966
    97
paulson@13966
    98
lemma "(x + y = (0::real)) = (y = -x)"
paulson@13966
    99
  by arith
paulson@13966
   100
paulson@13966
   101
lemma "((x + y) < (x + z)) = (y < (z::real))"
paulson@13966
   102
  by arith
paulson@13966
   103
paulson@13966
   104
lemma "((x + z) < (y + z)) = (x < (y::real))"
paulson@13966
   105
  by arith
paulson@13966
   106
paulson@13966
   107
lemma "(\<not> x < y) = (y \<le> (x::real))"
paulson@13966
   108
  by arith
paulson@13966
   109
paulson@13966
   110
lemma "\<not> (x < y \<and> y < (x::real))"
paulson@13966
   111
  by arith
paulson@13966
   112
paulson@13966
   113
lemma "(x::real) < y ==> \<not> y < x"
paulson@13966
   114
  by arith
paulson@13966
   115
paulson@13966
   116
lemma "((x::real) \<noteq> y) = (x < y \<or> y < x)"
paulson@13966
   117
  by arith
paulson@13966
   118
paulson@13966
   119
lemma "(\<not> x \<le> y) = (y < (x::real))"
paulson@13966
   120
  by arith
paulson@13966
   121
paulson@13966
   122
lemma "x \<le> y \<or> y \<le> (x::real)"
paulson@13966
   123
  by arith
paulson@13966
   124
paulson@13966
   125
lemma "x \<le> y \<or> y < (x::real)"
paulson@13966
   126
  by arith
paulson@13966
   127
paulson@13966
   128
lemma "x < y \<or> y \<le> (x::real)"
paulson@13966
   129
  by arith
paulson@13966
   130
paulson@13966
   131
lemma "x \<le> (x::real)"
paulson@13966
   132
  by arith
paulson@13966
   133
paulson@13966
   134
lemma "((x::real) \<le> y) = (x < y \<or> x = y)"
paulson@13966
   135
  by arith
paulson@13966
   136
paulson@13966
   137
lemma "((x::real) \<le> y \<and> y \<le> x) = (x = y)"
paulson@13966
   138
  by arith
paulson@13966
   139
paulson@13966
   140
lemma "\<not>(x < y \<and> y \<le> (x::real))"
paulson@13966
   141
  by arith
paulson@13966
   142
paulson@13966
   143
lemma "\<not>(x \<le> y \<and> y < (x::real))"
paulson@13966
   144
  by arith
paulson@13966
   145
paulson@13966
   146
lemma "(-x < (0::real)) = (0 < x)"
paulson@13966
   147
  by arith
paulson@13966
   148
paulson@13966
   149
lemma "((0::real) < -x) = (x < 0)"
paulson@13966
   150
  by arith
paulson@13966
   151
paulson@13966
   152
lemma "(-x \<le> (0::real)) = (0 \<le> x)"
paulson@13966
   153
  by arith
paulson@13966
   154
paulson@13966
   155
lemma "((0::real) \<le> -x) = (x \<le> 0)"
paulson@13966
   156
  by arith
paulson@13966
   157
paulson@13966
   158
lemma "(x::real) = y \<or> x < y \<or> y < x"
paulson@13966
   159
  by arith
paulson@13966
   160
paulson@13966
   161
lemma "(x::real) = 0 \<or> 0 < x \<or> 0 < -x"
paulson@13966
   162
  by arith
paulson@13966
   163
paulson@13966
   164
lemma "(0::real) \<le> x \<or> 0 \<le> -x"
paulson@13966
   165
  by arith
paulson@13966
   166
paulson@13966
   167
lemma "((x::real) + y \<le> x + z) = (y \<le> z)"
paulson@13966
   168
  by arith
paulson@13966
   169
paulson@13966
   170
lemma "((x::real) + z \<le> y + z) = (x \<le> y)"
paulson@13966
   171
  by arith
paulson@13966
   172
paulson@13966
   173
lemma "(w::real) < x \<and> y < z ==> w + y < x + z"
paulson@13966
   174
  by arith
paulson@13966
   175
paulson@13966
   176
lemma "(w::real) \<le> x \<and> y \<le> z ==> w + y \<le> x + z"
paulson@13966
   177
  by arith
paulson@13966
   178
paulson@13966
   179
lemma "(0::real) \<le> x \<and> 0 \<le> y ==> 0 \<le> x + y"
paulson@13966
   180
  by arith
paulson@13966
   181
paulson@13966
   182
lemma "(0::real) < x \<and> 0 < y ==> 0 < x + y"
paulson@13966
   183
  by arith
paulson@13966
   184
paulson@13966
   185
lemma "(-x < y) = (0 < x + (y::real))"
paulson@13966
   186
  by arith
paulson@13966
   187
paulson@13966
   188
lemma "(x < -y) = (x + y < (0::real))"
paulson@13966
   189
  by arith
paulson@13966
   190
paulson@13966
   191
lemma "(y < x + -z) = (y + z < (x::real))"
paulson@13966
   192
  by arith
paulson@13966
   193
paulson@13966
   194
lemma "(x + -y < z) = (x < z + (y::real))"
paulson@13966
   195
  by arith
paulson@13966
   196
paulson@13966
   197
lemma "x \<le> y ==> x < y + (1::real)"
paulson@13966
   198
  by arith
paulson@13966
   199
paulson@13966
   200
lemma "(x - y) + y = (x::real)"
paulson@13966
   201
  by arith
paulson@13966
   202
paulson@13966
   203
lemma "y + (x - y) = (x::real)"
paulson@13966
   204
  by arith
paulson@13966
   205
paulson@13966
   206
lemma "x - x = (0::real)"
paulson@13966
   207
  by arith
paulson@13966
   208
paulson@13966
   209
lemma "(x - y = 0) = (x = (y::real))"
paulson@13966
   210
  by arith
paulson@13966
   211
paulson@13966
   212
lemma "((0::real) \<le> x + x) = (0 \<le> x)"
paulson@13966
   213
  by arith
paulson@13966
   214
paulson@13966
   215
lemma "(-x \<le> x) = ((0::real) \<le> x)"
paulson@13966
   216
  by arith
paulson@13966
   217
paulson@13966
   218
lemma "(x \<le> -x) = (x \<le> (0::real))"
paulson@13966
   219
  by arith
paulson@13966
   220
paulson@13966
   221
lemma "(-x = (0::real)) = (x = 0)"
paulson@13966
   222
  by arith
paulson@13966
   223
paulson@13966
   224
lemma "-(x - y) = y - (x::real)"
paulson@13966
   225
  by arith
paulson@13966
   226
paulson@13966
   227
lemma "((0::real) < x - y) = (y < x)"
paulson@13966
   228
  by arith
paulson@13966
   229
paulson@13966
   230
lemma "((0::real) \<le> x - y) = (y \<le> x)"
paulson@13966
   231
  by arith
paulson@13966
   232
paulson@13966
   233
lemma "(x + y) - x = (y::real)"
paulson@13966
   234
  by arith
paulson@13966
   235
paulson@13966
   236
lemma "(-x = y) = (x = (-y::real))"
paulson@13966
   237
  by arith
paulson@13966
   238
paulson@13966
   239
lemma "x < (y::real) ==> \<not>(x = y)"
paulson@13966
   240
  by arith
paulson@13966
   241
paulson@13966
   242
lemma "(x \<le> x + y) = ((0::real) \<le> y)"
paulson@13966
   243
  by arith
paulson@13966
   244
paulson@13966
   245
lemma "(y \<le> x + y) = ((0::real) \<le> x)"
paulson@13966
   246
  by arith
paulson@13966
   247
paulson@13966
   248
lemma "(x < x + y) = ((0::real) < y)"
paulson@13966
   249
  by arith
paulson@13966
   250
paulson@13966
   251
lemma "(y < x + y) = ((0::real) < x)"
paulson@13966
   252
  by arith
paulson@13966
   253
paulson@13966
   254
lemma "(x - y) - x = (-y::real)"
paulson@13966
   255
  by arith
paulson@13966
   256
paulson@13966
   257
lemma "(x + y < z) = (x < z - (y::real))"
paulson@13966
   258
  by arith
paulson@13966
   259
paulson@13966
   260
lemma "(x - y < z) = (x < z + (y::real))"
paulson@13966
   261
  by arith
paulson@13966
   262
paulson@13966
   263
lemma "(x < y - z) = (x + z < (y::real))"
paulson@13966
   264
  by arith
paulson@13966
   265
paulson@13966
   266
lemma "(x \<le> y - z) = (x + z \<le> (y::real))"
paulson@13966
   267
  by arith
paulson@13966
   268
paulson@13966
   269
lemma "(x - y \<le> z) = (x \<le> z + (y::real))"
paulson@13966
   270
  by arith
paulson@13966
   271
paulson@13966
   272
lemma "(-x < -y) = (y < (x::real))"
paulson@13966
   273
  by arith
paulson@13966
   274
paulson@13966
   275
lemma "(-x \<le> -y) = (y \<le> (x::real))"
paulson@13966
   276
  by arith
paulson@13966
   277
paulson@13966
   278
lemma "(a + b) - (c + d) = (a - c) + (b - (d::real))"
paulson@13966
   279
  by arith
paulson@13966
   280
paulson@13966
   281
lemma "(0::real) - x = -x"
paulson@13966
   282
  by arith
paulson@13966
   283
paulson@13966
   284
lemma "x - (0::real) = x"
paulson@13966
   285
  by arith
paulson@13966
   286
paulson@13966
   287
lemma "w \<le> x \<and> y < z ==> w + y < x + (z::real)"
paulson@13966
   288
  by arith
paulson@13966
   289
paulson@13966
   290
lemma "w < x \<and> y \<le> z ==> w + y < x + (z::real)"
paulson@13966
   291
  by arith
paulson@13966
   292
paulson@13966
   293
lemma "(0::real) \<le> x \<and> 0 < y ==> 0 < x + (y::real)"
paulson@13966
   294
  by arith
paulson@13966
   295
paulson@13966
   296
lemma "(0::real) < x \<and> 0 \<le> y ==> 0 < x + y"
paulson@13966
   297
  by arith
paulson@13966
   298
paulson@13966
   299
lemma "-x - y = -(x + (y::real))"
paulson@13966
   300
  by arith
paulson@13966
   301
paulson@13966
   302
lemma "x - (-y) = x + (y::real)"
paulson@13966
   303
  by arith
paulson@13966
   304
paulson@13966
   305
lemma "-x - -y = y - (x::real)"
paulson@13966
   306
  by arith
paulson@13966
   307
paulson@13966
   308
lemma "(a - b) + (b - c) = a - (c::real)"
paulson@13966
   309
  by arith
paulson@13966
   310
paulson@13966
   311
lemma "(x = y - z) = (x + z = (y::real))"
paulson@13966
   312
  by arith
paulson@13966
   313
paulson@13966
   314
lemma "(x - y = z) = (x = z + (y::real))"
paulson@13966
   315
  by arith
paulson@13966
   316
paulson@13966
   317
lemma "x - (x - y) = (y::real)"
paulson@13966
   318
  by arith
paulson@13966
   319
paulson@13966
   320
lemma "x - (x + y) = -(y::real)"
paulson@13966
   321
  by arith
paulson@13966
   322
paulson@13966
   323
lemma "x = y ==> x \<le> (y::real)"
paulson@13966
   324
  by arith
paulson@13966
   325
paulson@13966
   326
lemma "(0::real) < x ==> \<not>(x = 0)"
paulson@13966
   327
  by arith
paulson@13966
   328
paulson@13966
   329
lemma "(x + y) * (x - y) = (x * x) - (y * y)"
paulson@13966
   330
  oops
paulson@13966
   331
paulson@13966
   332
lemma "(-x = -y) = (x = (y::real))"
paulson@13966
   333
  by arith
paulson@13966
   334
paulson@13966
   335
lemma "(-x < -y) = (y < (x::real))"
paulson@13966
   336
  by arith
paulson@13966
   337
paulson@13966
   338
lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d"
paulson@13966
   339
  by (tactic "fast_arith_tac 1")
paulson@13966
   340
paulson@13966
   341
lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)"
paulson@13966
   342
  by (tactic "fast_arith_tac 1")
paulson@13966
   343
paulson@13966
   344
lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c"
paulson@13966
   345
  by (tactic "fast_arith_tac 1")
paulson@13966
   346
paulson@13966
   347
lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j"
paulson@13966
   348
  by (tactic "fast_arith_tac 1")
paulson@13966
   349
paulson@13966
   350
lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j"
paulson@13966
   351
  by (tactic "fast_arith_tac 1")
paulson@13966
   352
paulson@13966
   353
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"
paulson@13966
   354
  by arith
paulson@13966
   355
paulson@13966
   356
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
paulson@13966
   357
    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l"
paulson@13966
   358
  by (tactic "fast_arith_tac 1")
paulson@13966
   359
paulson@13966
   360
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
paulson@13966
   361
    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l"
paulson@13966
   362
  by (tactic "fast_arith_tac 1")
paulson@13966
   363
paulson@13966
   364
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
paulson@13966
   365
    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i"
paulson@13966
   366
  by (tactic "fast_arith_tac 1")
paulson@13966
   367
paulson@13966
   368
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
paulson@13966
   369
    ==> 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"
paulson@13966
   370
  by (tactic "fast_arith_tac 1")
paulson@13966
   371
paulson@14051
   372
paulson@14051
   373
subsection{*Complex Arithmetic*}
paulson@14051
   374
paulson@14051
   375
lemma "(1359 + 93746*ii) - (2468 + 46375*ii) = -1109 + 47371*ii"
paulson@14051
   376
  by simp
paulson@14051
   377
paulson@14051
   378
lemma "- (65745 + -47371*ii) = -65745 + 47371*ii"
paulson@14051
   379
  by simp
paulson@14051
   380
paulson@14051
   381
text{*Multiplication requires distributive laws.  Perhaps versions instantiated
paulson@14051
   382
to literal constants should be added to the simpset.*}
paulson@14051
   383
paulson@14373
   384
lemmas distrib = left_distrib right_distrib left_diff_distrib right_diff_distrib
paulson@14051
   385
paulson@14051
   386
lemma "(1 + ii) * (1 - ii) = 2"
paulson@14051
   387
by (simp add: distrib)
paulson@14051
   388
paulson@14051
   389
lemma "(1 + 2*ii) * (1 + 3*ii) = -5 + 5*ii"
paulson@14051
   390
by (simp add: distrib)
paulson@14051
   391
paulson@14051
   392
lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii"
paulson@14051
   393
by (simp add: distrib)
paulson@14051
   394
paulson@14373
   395
text{*No inequalities or linear arithmetic: the complex numbers are unordered!*}
paulson@14051
   396
paulson@14051
   397
text{*No powers (not supported yet)*}
paulson@14051
   398
paulson@13966
   399
end