src/HOL/Complex/ex/BinEx.thy
author paulson
Thu Jul 01 12:29:53 2004 +0200 (2004-07-01)
changeset 15013 34264f5e4691
parent 14373 67a628beb981
child 15149 c5c4884634b7
permissions -rw-r--r--
new treatment of binary numerals
     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 = left_distrib right_distrib left_diff_distrib right_diff_distrib
   385 
   386 lemma "(1 + ii) * (1 - ii) = 2"
   387 by (simp add: distrib)
   388 
   389 lemma "(1 + 2*ii) * (1 + 3*ii) = -5 + 5*ii"
   390 by (simp add: distrib)
   391 
   392 lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii"
   393 by (simp add: distrib)
   394 
   395 text{*No inequalities or linear arithmetic: the complex numbers are unordered!*}
   396 
   397 text{*No powers (not supported yet)*}
   398 
   399 end