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