src/HOL/Complex/ex/BinEx.thy
author paulson
Tue May 06 17:45:54 2003 +0200 (2003-05-06)
changeset 13966 2160abf7cfe7
child 14051 4b61bbb0dcab
permissions -rw-r--r--
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
     1 (*  Title:      HOL/Real/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 = Real:
    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 text {* \medskip Addition *}
    17 
    18 lemma "(1359::real) + -2468 = -1109"
    19   by simp
    20 
    21 lemma "(93746::real) + -46375 = 47371"
    22   by simp
    23 
    24 
    25 text {* \medskip Negation *}
    26 
    27 lemma "- (65745::real) = -65745"
    28   by simp
    29 
    30 lemma "- (-54321::real) = 54321"
    31   by simp
    32 
    33 
    34 text {* \medskip Multiplication *}
    35 
    36 lemma "(-84::real) * 51 = -4284"
    37   by simp
    38 
    39 lemma "(255::real) * 255 = 65025"
    40   by simp
    41 
    42 lemma "(1359::real) * -2468 = -3354012"
    43   by simp
    44 
    45 
    46 text {* \medskip Inequalities *}
    47 
    48 lemma "(89::real) * 10 \<noteq> 889"
    49   by simp
    50 
    51 lemma "(13::real) < 18 - 4"
    52   by simp
    53 
    54 lemma "(-345::real) < -242 + -100"
    55   by simp
    56 
    57 lemma "(13557456::real) < 18678654"
    58   by simp
    59 
    60 lemma "(999999::real) \<le> (1000001 + 1) - 2"
    61   by simp
    62 
    63 lemma "(1234567::real) \<le> 1234567"
    64   by simp
    65 
    66 
    67 text {* \medskip Powers *}
    68 
    69 lemma "2 ^ 15 = (32768::real)"
    70   by simp
    71 
    72 lemma "-3 ^ 7 = (-2187::real)"
    73   by simp
    74 
    75 lemma "13 ^ 7 = (62748517::real)"
    76   by simp
    77 
    78 lemma "3 ^ 15 = (14348907::real)"
    79   by simp
    80 
    81 lemma "-5 ^ 11 = (-48828125::real)"
    82   by simp
    83 
    84 
    85 text {* \medskip Tests *}
    86 
    87 lemma "(x + y = x) = (y = (0::real))"
    88   by arith
    89 
    90 lemma "(x + y = y) = (x = (0::real))"
    91   by arith
    92 
    93 lemma "(x + y = (0::real)) = (x = -y)"
    94   by arith
    95 
    96 lemma "(x + y = (0::real)) = (y = -x)"
    97   by arith
    98 
    99 lemma "((x + y) < (x + z)) = (y < (z::real))"
   100   by arith
   101 
   102 lemma "((x + z) < (y + z)) = (x < (y::real))"
   103   by arith
   104 
   105 lemma "(\<not> x < y) = (y \<le> (x::real))"
   106   by arith
   107 
   108 lemma "\<not> (x < y \<and> y < (x::real))"
   109   by arith
   110 
   111 lemma "(x::real) < y ==> \<not> y < x"
   112   by arith
   113 
   114 lemma "((x::real) \<noteq> y) = (x < y \<or> y < x)"
   115   by arith
   116 
   117 lemma "(\<not> x \<le> y) = (y < (x::real))"
   118   by arith
   119 
   120 lemma "x \<le> y \<or> y \<le> (x::real)"
   121   by arith
   122 
   123 lemma "x \<le> y \<or> y < (x::real)"
   124   by arith
   125 
   126 lemma "x < y \<or> y \<le> (x::real)"
   127   by arith
   128 
   129 lemma "x \<le> (x::real)"
   130   by arith
   131 
   132 lemma "((x::real) \<le> y) = (x < y \<or> x = y)"
   133   by arith
   134 
   135 lemma "((x::real) \<le> y \<and> y \<le> x) = (x = y)"
   136   by arith
   137 
   138 lemma "\<not>(x < y \<and> y \<le> (x::real))"
   139   by arith
   140 
   141 lemma "\<not>(x \<le> y \<and> y < (x::real))"
   142   by arith
   143 
   144 lemma "(-x < (0::real)) = (0 < x)"
   145   by arith
   146 
   147 lemma "((0::real) < -x) = (x < 0)"
   148   by arith
   149 
   150 lemma "(-x \<le> (0::real)) = (0 \<le> x)"
   151   by arith
   152 
   153 lemma "((0::real) \<le> -x) = (x \<le> 0)"
   154   by arith
   155 
   156 lemma "(x::real) = y \<or> x < y \<or> y < x"
   157   by arith
   158 
   159 lemma "(x::real) = 0 \<or> 0 < x \<or> 0 < -x"
   160   by arith
   161 
   162 lemma "(0::real) \<le> x \<or> 0 \<le> -x"
   163   by arith
   164 
   165 lemma "((x::real) + y \<le> x + z) = (y \<le> z)"
   166   by arith
   167 
   168 lemma "((x::real) + z \<le> y + z) = (x \<le> y)"
   169   by arith
   170 
   171 lemma "(w::real) < x \<and> y < z ==> w + y < x + z"
   172   by arith
   173 
   174 lemma "(w::real) \<le> x \<and> y \<le> z ==> w + y \<le> x + z"
   175   by arith
   176 
   177 lemma "(0::real) \<le> x \<and> 0 \<le> y ==> 0 \<le> x + y"
   178   by arith
   179 
   180 lemma "(0::real) < x \<and> 0 < y ==> 0 < x + y"
   181   by arith
   182 
   183 lemma "(-x < y) = (0 < x + (y::real))"
   184   by arith
   185 
   186 lemma "(x < -y) = (x + y < (0::real))"
   187   by arith
   188 
   189 lemma "(y < x + -z) = (y + z < (x::real))"
   190   by arith
   191 
   192 lemma "(x + -y < z) = (x < z + (y::real))"
   193   by arith
   194 
   195 lemma "x \<le> y ==> x < y + (1::real)"
   196   by arith
   197 
   198 lemma "(x - y) + y = (x::real)"
   199   by arith
   200 
   201 lemma "y + (x - y) = (x::real)"
   202   by arith
   203 
   204 lemma "x - x = (0::real)"
   205   by arith
   206 
   207 lemma "(x - y = 0) = (x = (y::real))"
   208   by arith
   209 
   210 lemma "((0::real) \<le> x + x) = (0 \<le> x)"
   211   by arith
   212 
   213 lemma "(-x \<le> x) = ((0::real) \<le> x)"
   214   by arith
   215 
   216 lemma "(x \<le> -x) = (x \<le> (0::real))"
   217   by arith
   218 
   219 lemma "(-x = (0::real)) = (x = 0)"
   220   by arith
   221 
   222 lemma "-(x - y) = y - (x::real)"
   223   by arith
   224 
   225 lemma "((0::real) < x - y) = (y < x)"
   226   by arith
   227 
   228 lemma "((0::real) \<le> x - y) = (y \<le> x)"
   229   by arith
   230 
   231 lemma "(x + y) - x = (y::real)"
   232   by arith
   233 
   234 lemma "(-x = y) = (x = (-y::real))"
   235   by arith
   236 
   237 lemma "x < (y::real) ==> \<not>(x = y)"
   238   by arith
   239 
   240 lemma "(x \<le> x + y) = ((0::real) \<le> y)"
   241   by arith
   242 
   243 lemma "(y \<le> x + y) = ((0::real) \<le> x)"
   244   by arith
   245 
   246 lemma "(x < x + y) = ((0::real) < y)"
   247   by arith
   248 
   249 lemma "(y < x + y) = ((0::real) < x)"
   250   by arith
   251 
   252 lemma "(x - y) - x = (-y::real)"
   253   by arith
   254 
   255 lemma "(x + y < z) = (x < z - (y::real))"
   256   by arith
   257 
   258 lemma "(x - y < z) = (x < z + (y::real))"
   259   by arith
   260 
   261 lemma "(x < y - z) = (x + z < (y::real))"
   262   by arith
   263 
   264 lemma "(x \<le> y - z) = (x + z \<le> (y::real))"
   265   by arith
   266 
   267 lemma "(x - y \<le> z) = (x \<le> z + (y::real))"
   268   by arith
   269 
   270 lemma "(-x < -y) = (y < (x::real))"
   271   by arith
   272 
   273 lemma "(-x \<le> -y) = (y \<le> (x::real))"
   274   by arith
   275 
   276 lemma "(a + b) - (c + d) = (a - c) + (b - (d::real))"
   277   by arith
   278 
   279 lemma "(0::real) - x = -x"
   280   by arith
   281 
   282 lemma "x - (0::real) = x"
   283   by arith
   284 
   285 lemma "w \<le> x \<and> y < z ==> w + y < x + (z::real)"
   286   by arith
   287 
   288 lemma "w < x \<and> y \<le> z ==> w + y < x + (z::real)"
   289   by arith
   290 
   291 lemma "(0::real) \<le> x \<and> 0 < y ==> 0 < x + (y::real)"
   292   by arith
   293 
   294 lemma "(0::real) < x \<and> 0 \<le> y ==> 0 < x + y"
   295   by arith
   296 
   297 lemma "-x - y = -(x + (y::real))"
   298   by arith
   299 
   300 lemma "x - (-y) = x + (y::real)"
   301   by arith
   302 
   303 lemma "-x - -y = y - (x::real)"
   304   by arith
   305 
   306 lemma "(a - b) + (b - c) = a - (c::real)"
   307   by arith
   308 
   309 lemma "(x = y - z) = (x + z = (y::real))"
   310   by arith
   311 
   312 lemma "(x - y = z) = (x = z + (y::real))"
   313   by arith
   314 
   315 lemma "x - (x - y) = (y::real)"
   316   by arith
   317 
   318 lemma "x - (x + y) = -(y::real)"
   319   by arith
   320 
   321 lemma "x = y ==> x \<le> (y::real)"
   322   by arith
   323 
   324 lemma "(0::real) < x ==> \<not>(x = 0)"
   325   by arith
   326 
   327 lemma "(x + y) * (x - y) = (x * x) - (y * y)"
   328   oops
   329 
   330 lemma "(-x = -y) = (x = (y::real))"
   331   by arith
   332 
   333 lemma "(-x < -y) = (y < (x::real))"
   334   by arith
   335 
   336 lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d"
   337   by (tactic "fast_arith_tac 1")
   338 
   339 lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)"
   340   by (tactic "fast_arith_tac 1")
   341 
   342 lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c"
   343   by (tactic "fast_arith_tac 1")
   344 
   345 lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j"
   346   by (tactic "fast_arith_tac 1")
   347 
   348 lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j"
   349   by (tactic "fast_arith_tac 1")
   350 
   351 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"
   352   by arith
   353 
   354 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
   355     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l"
   356   by (tactic "fast_arith_tac 1")
   357 
   358 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
   359     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l"
   360   by (tactic "fast_arith_tac 1")
   361 
   362 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
   363     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i"
   364   by (tactic "fast_arith_tac 1")
   365 
   366 lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
   367     ==> 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"
   368   by (tactic "fast_arith_tac 1")
   369 
   370 end