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