author | wenzelm |
Thu, 30 May 2013 20:38:50 +0200 | |
changeset 52252 | 81fcc11d8c65 |
parent 45615 | c05e8209a3aa |
child 58410 | 6d46ad54a2ab |
permissions | -rw-r--r-- |
5545 | 1 |
(* Title: HOL/ex/BinEx.thy |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 |
Copyright 1998 University of Cambridge |
|
4 |
*) |
|
5 |
||
11024 | 6 |
header {* Binary arithmetic examples *} |
7 |
||
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
8 |
theory BinEx |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
9 |
imports Complex_Main |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
10 |
begin |
11024 | 11 |
|
14113 | 12 |
subsection {* Regression Testing for Cancellation Simprocs *} |
13 |
||
14 |
lemma "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)" |
|
15 |
apply simp oops |
|
16 |
||
17 |
lemma "2*u = (u::int)" |
|
18 |
apply simp oops |
|
19 |
||
20 |
lemma "(i + j + 12 + (k::int)) - 15 = y" |
|
21 |
apply simp oops |
|
22 |
||
23 |
lemma "(i + j + 12 + (k::int)) - 5 = y" |
|
24 |
apply simp oops |
|
25 |
||
26 |
lemma "y - b < (b::int)" |
|
27 |
apply simp oops |
|
28 |
||
29 |
lemma "y - (3*b + c) < (b::int) - 2*c" |
|
30 |
apply simp oops |
|
31 |
||
32 |
lemma "(2*x - (u*v) + y) - v*3*u = (w::int)" |
|
33 |
apply simp oops |
|
34 |
||
35 |
lemma "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)" |
|
36 |
apply simp oops |
|
37 |
||
38 |
lemma "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)" |
|
39 |
apply simp oops |
|
40 |
||
41 |
lemma "u*v - (x*u*v + (u*v)*4 + y) = (w::int)" |
|
42 |
apply simp oops |
|
43 |
||
44 |
lemma "(i + j + 12 + (k::int)) = u + 15 + y" |
|
45 |
apply simp oops |
|
46 |
||
47 |
lemma "(i + j*2 + 12 + (k::int)) = j + 5 + y" |
|
48 |
apply simp oops |
|
49 |
||
50 |
lemma "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)" |
|
51 |
apply simp oops |
|
52 |
||
53 |
lemma "a + -(b+c) + b = (d::int)" |
|
54 |
apply simp oops |
|
55 |
||
56 |
lemma "a + -(b+c) - b = (d::int)" |
|
57 |
apply simp oops |
|
58 |
||
59 |
(*negative numerals*) |
|
60 |
lemma "(i + j + -2 + (k::int)) - (u + 5 + y) = zz" |
|
61 |
apply simp oops |
|
62 |
||
63 |
lemma "(i + j + -3 + (k::int)) < u + 5 + y" |
|
64 |
apply simp oops |
|
65 |
||
66 |
lemma "(i + j + 3 + (k::int)) < u + -6 + y" |
|
67 |
apply simp oops |
|
68 |
||
69 |
lemma "(i + j + -12 + (k::int)) - 15 = y" |
|
70 |
apply simp oops |
|
71 |
||
72 |
lemma "(i + j + 12 + (k::int)) - -15 = y" |
|
73 |
apply simp oops |
|
74 |
||
75 |
lemma "(i + j + -12 + (k::int)) - -15 = y" |
|
76 |
apply simp oops |
|
77 |
||
14124 | 78 |
lemma "- (2*i) + 3 + (2*i + 4) = (0::int)" |
79 |
apply simp oops |
|
80 |
||
81 |
||
14113 | 82 |
|
83 |
subsection {* Arithmetic Method Tests *} |
|
84 |
||
85 |
||
86 |
lemma "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d" |
|
87 |
by arith |
|
88 |
||
89 |
lemma "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)" |
|
90 |
by arith |
|
91 |
||
92 |
lemma "!!a::int. [| a < b; c < d |] ==> a+c+ 1 < b+d" |
|
93 |
by arith |
|
94 |
||
95 |
lemma "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c" |
|
96 |
by arith |
|
97 |
||
98 |
lemma "!!a::int. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j" |
|
99 |
by arith |
|
100 |
||
101 |
lemma "!!a::int. [| a+b < i+j; a<b; i<j |] ==> a+a - - -1 < j+j - 3" |
|
102 |
by arith |
|
103 |
||
104 |
lemma "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k" |
|
105 |
by arith |
|
106 |
||
107 |
lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] |
|
108 |
==> a <= l" |
|
109 |
by arith |
|
110 |
||
111 |
lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] |
|
112 |
==> a+a+a+a <= l+l+l+l" |
|
113 |
by arith |
|
114 |
||
115 |
lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] |
|
116 |
==> a+a+a+a+a <= l+l+l+l+i" |
|
117 |
by arith |
|
118 |
||
119 |
lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] |
|
120 |
==> a+a+a+a+a+a <= l+l+l+l+i+l" |
|
121 |
by arith |
|
122 |
||
123 |
lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] |
|
124 |
==> 6*a <= 5*l+i" |
|
125 |
by arith |
|
126 |
||
127 |
||
128 |
||
11024 | 129 |
subsection {* The Integers *} |
130 |
||
131 |
text {* Addition *} |
|
132 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
133 |
lemma "(13::int) + 19 = 32" |
11024 | 134 |
by simp |
135 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
136 |
lemma "(1234::int) + 5678 = 6912" |
11024 | 137 |
by simp |
138 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
139 |
lemma "(1359::int) + -2468 = -1109" |
11024 | 140 |
by simp |
141 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
142 |
lemma "(93746::int) + -46375 = 47371" |
11024 | 143 |
by simp |
144 |
||
145 |
||
146 |
text {* \medskip Negation *} |
|
147 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
148 |
lemma "- (65745::int) = -65745" |
11024 | 149 |
by simp |
150 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
151 |
lemma "- (-54321::int) = 54321" |
11024 | 152 |
by simp |
153 |
||
154 |
||
155 |
text {* \medskip Multiplication *} |
|
156 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
157 |
lemma "(13::int) * 19 = 247" |
11024 | 158 |
by simp |
159 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
160 |
lemma "(-84::int) * 51 = -4284" |
11024 | 161 |
by simp |
162 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
163 |
lemma "(255::int) * 255 = 65025" |
11024 | 164 |
by simp |
165 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
166 |
lemma "(1359::int) * -2468 = -3354012" |
11024 | 167 |
by simp |
168 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
169 |
lemma "(89::int) * 10 \<noteq> 889" |
11024 | 170 |
by simp |
171 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
172 |
lemma "(13::int) < 18 - 4" |
11024 | 173 |
by simp |
174 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
175 |
lemma "(-345::int) < -242 + -100" |
11024 | 176 |
by simp |
177 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
178 |
lemma "(13557456::int) < 18678654" |
11024 | 179 |
by simp |
180 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
181 |
lemma "(999999::int) \<le> (1000001 + 1) - 2" |
11024 | 182 |
by simp |
183 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
184 |
lemma "(1234567::int) \<le> 1234567" |
11024 | 185 |
by simp |
186 |
||
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15013
diff
changeset
|
187 |
text{*No integer overflow!*} |
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15013
diff
changeset
|
188 |
lemma "1234567 * (1234567::int) < 1234567*1234567*1234567" |
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15013
diff
changeset
|
189 |
by simp |
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15013
diff
changeset
|
190 |
|
11024 | 191 |
|
192 |
text {* \medskip Quotient and Remainder *} |
|
193 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
194 |
lemma "(10::int) div 3 = 3" |
11024 | 195 |
by simp |
196 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
197 |
lemma "(10::int) mod 3 = 1" |
11024 | 198 |
by simp |
199 |
||
200 |
text {* A negative divisor *} |
|
201 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
202 |
lemma "(10::int) div -3 = -4" |
11024 | 203 |
by simp |
204 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
205 |
lemma "(10::int) mod -3 = -2" |
11024 | 206 |
by simp |
5545 | 207 |
|
11024 | 208 |
text {* |
209 |
A negative dividend\footnote{The definition agrees with mathematical |
|
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15013
diff
changeset
|
210 |
convention and with ML, but not with the hardware of most computers} |
11024 | 211 |
*} |
212 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
213 |
lemma "(-10::int) div 3 = -4" |
11024 | 214 |
by simp |
215 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
216 |
lemma "(-10::int) mod 3 = 2" |
11024 | 217 |
by simp |
218 |
||
219 |
text {* A negative dividend \emph{and} divisor *} |
|
220 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
221 |
lemma "(-10::int) div -3 = 3" |
11024 | 222 |
by simp |
223 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
224 |
lemma "(-10::int) mod -3 = -1" |
11024 | 225 |
by simp |
226 |
||
227 |
text {* A few bigger examples *} |
|
228 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
229 |
lemma "(8452::int) mod 3 = 1" |
11024 | 230 |
by simp |
231 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
232 |
lemma "(59485::int) div 434 = 137" |
11024 | 233 |
by simp |
234 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
235 |
lemma "(1000006::int) mod 10 = 6" |
11024 | 236 |
by simp |
237 |
||
238 |
||
239 |
text {* \medskip Division by shifting *} |
|
240 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
241 |
lemma "10000000 div 2 = (5000000::int)" |
11024 | 242 |
by simp |
243 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
244 |
lemma "10000001 mod 2 = (1::int)" |
11024 | 245 |
by simp |
246 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
247 |
lemma "10000055 div 32 = (312501::int)" |
11024 | 248 |
by simp |
249 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
250 |
lemma "10000055 mod 32 = (23::int)" |
11024 | 251 |
by simp |
252 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
253 |
lemma "100094 div 144 = (695::int)" |
11024 | 254 |
by simp |
255 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
256 |
lemma "100094 mod 144 = (14::int)" |
11024 | 257 |
by simp |
258 |
||
259 |
||
12613
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
260 |
text {* \medskip Powers *} |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
261 |
|
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
262 |
lemma "2 ^ 10 = (1024::int)" |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
263 |
by simp |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
264 |
|
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
265 |
lemma "-3 ^ 7 = (-2187::int)" |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
266 |
by simp |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
267 |
|
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
268 |
lemma "13 ^ 7 = (62748517::int)" |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
269 |
by simp |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
270 |
|
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
271 |
lemma "3 ^ 15 = (14348907::int)" |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
272 |
by simp |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
273 |
|
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
274 |
lemma "-5 ^ 11 = (-48828125::int)" |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
275 |
by simp |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
276 |
|
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
277 |
|
11024 | 278 |
subsection {* The Natural Numbers *} |
279 |
||
280 |
text {* Successor *} |
|
281 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
282 |
lemma "Suc 99999 = 100000" |
45615 | 283 |
by simp |
11024 | 284 |
|
285 |
||
286 |
text {* \medskip Addition *} |
|
287 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
288 |
lemma "(13::nat) + 19 = 32" |
11024 | 289 |
by simp |
290 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
291 |
lemma "(1234::nat) + 5678 = 6912" |
11024 | 292 |
by simp |
293 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
294 |
lemma "(973646::nat) + 6475 = 980121" |
11024 | 295 |
by simp |
296 |
||
297 |
||
298 |
text {* \medskip Subtraction *} |
|
299 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
300 |
lemma "(32::nat) - 14 = 18" |
11024 | 301 |
by simp |
302 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
303 |
lemma "(14::nat) - 15 = 0" |
11024 | 304 |
by simp |
5545 | 305 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
306 |
lemma "(14::nat) - 1576644 = 0" |
11024 | 307 |
by simp |
308 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
309 |
lemma "(48273776::nat) - 3873737 = 44400039" |
11024 | 310 |
by simp |
311 |
||
312 |
||
313 |
text {* \medskip Multiplication *} |
|
314 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
315 |
lemma "(12::nat) * 11 = 132" |
11024 | 316 |
by simp |
317 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
318 |
lemma "(647::nat) * 3643 = 2357021" |
11024 | 319 |
by simp |
320 |
||
321 |
||
322 |
text {* \medskip Quotient and Remainder *} |
|
323 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
324 |
lemma "(10::nat) div 3 = 3" |
11024 | 325 |
by simp |
326 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
327 |
lemma "(10::nat) mod 3 = 1" |
11024 | 328 |
by simp |
329 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
330 |
lemma "(10000::nat) div 9 = 1111" |
11024 | 331 |
by simp |
332 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
333 |
lemma "(10000::nat) mod 9 = 1" |
11024 | 334 |
by simp |
335 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
336 |
lemma "(10000::nat) div 16 = 625" |
11024 | 337 |
by simp |
338 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
339 |
lemma "(10000::nat) mod 16 = 0" |
11024 | 340 |
by simp |
341 |
||
5545 | 342 |
|
12613
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
343 |
text {* \medskip Powers *} |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
344 |
|
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
345 |
lemma "2 ^ 12 = (4096::nat)" |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
346 |
by simp |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
347 |
|
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
348 |
lemma "3 ^ 10 = (59049::nat)" |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
349 |
by simp |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
350 |
|
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
351 |
lemma "12 ^ 7 = (35831808::nat)" |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
352 |
by simp |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
353 |
|
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
354 |
lemma "3 ^ 14 = (4782969::nat)" |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
355 |
by simp |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
356 |
|
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
357 |
lemma "5 ^ 11 = (48828125::nat)" |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
358 |
by simp |
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
359 |
|
279facb4253a
Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents:
11868
diff
changeset
|
360 |
|
11024 | 361 |
text {* \medskip Testing the cancellation of complementary terms *} |
362 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
363 |
lemma "y + (x + -x) = (0::int) + y" |
11024 | 364 |
by simp |
365 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
366 |
lemma "y + (-x + (- y + x)) = (0::int)" |
11024 | 367 |
by simp |
368 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
369 |
lemma "-x + (y + (- y + x)) = (0::int)" |
11024 | 370 |
by simp |
371 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
372 |
lemma "x + (x + (- x + (- x + (- y + - z)))) = (0::int) - y - z" |
11024 | 373 |
by simp |
374 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
375 |
lemma "x + x - x - x - y - z = (0::int) - y - z" |
11024 | 376 |
by simp |
377 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
378 |
lemma "x + y + z - (x + z) = y - (0::int)" |
11024 | 379 |
by simp |
380 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
381 |
lemma "x + (y + (y + (y + (-x + -x)))) = (0::int) + y - x + y + y" |
11024 | 382 |
by simp |
383 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
384 |
lemma "x + (y + (y + (y + (-y + -x)))) = y + (0::int) + y" |
11024 | 385 |
by simp |
386 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11704
diff
changeset
|
387 |
lemma "x + y - x + z - x - y - z + x < (1::int)" |
11024 | 388 |
by simp |
389 |
||
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
390 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
391 |
subsection{*Real Arithmetic*} |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
392 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
393 |
subsubsection {*Addition *} |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
394 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
395 |
lemma "(1359::real) + -2468 = -1109" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
396 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
397 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
398 |
lemma "(93746::real) + -46375 = 47371" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
399 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
400 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
401 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
402 |
subsubsection {*Negation *} |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
403 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
404 |
lemma "- (65745::real) = -65745" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
405 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
406 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
407 |
lemma "- (-54321::real) = 54321" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
408 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
409 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
410 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
411 |
subsubsection {*Multiplication *} |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
412 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
413 |
lemma "(-84::real) * 51 = -4284" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
414 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
415 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
416 |
lemma "(255::real) * 255 = 65025" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
417 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
418 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
419 |
lemma "(1359::real) * -2468 = -3354012" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
420 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
421 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
422 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
423 |
subsubsection {*Inequalities *} |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
424 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
425 |
lemma "(89::real) * 10 \<noteq> 889" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
426 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
427 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
428 |
lemma "(13::real) < 18 - 4" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
429 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
430 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
431 |
lemma "(-345::real) < -242 + -100" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
432 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
433 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
434 |
lemma "(13557456::real) < 18678654" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
435 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
436 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
437 |
lemma "(999999::real) \<le> (1000001 + 1) - 2" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
438 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
439 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
440 |
lemma "(1234567::real) \<le> 1234567" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
441 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
442 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
443 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
444 |
subsubsection {*Powers *} |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
445 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
446 |
lemma "2 ^ 15 = (32768::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
447 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
448 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
449 |
lemma "-3 ^ 7 = (-2187::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
450 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
451 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
452 |
lemma "13 ^ 7 = (62748517::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
453 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
454 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
455 |
lemma "3 ^ 15 = (14348907::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
456 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
457 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
458 |
lemma "-5 ^ 11 = (-48828125::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
459 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
460 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
461 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
462 |
subsubsection {*Tests *} |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
463 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
464 |
lemma "(x + y = x) = (y = (0::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
465 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
466 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
467 |
lemma "(x + y = y) = (x = (0::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
468 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
469 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
470 |
lemma "(x + y = (0::real)) = (x = -y)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
471 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
472 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
473 |
lemma "(x + y = (0::real)) = (y = -x)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
474 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
475 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
476 |
lemma "((x + y) < (x + z)) = (y < (z::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
477 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
478 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
479 |
lemma "((x + z) < (y + z)) = (x < (y::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
480 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
481 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
482 |
lemma "(\<not> x < y) = (y \<le> (x::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
483 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
484 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
485 |
lemma "\<not> (x < y \<and> y < (x::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
486 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
487 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
488 |
lemma "(x::real) < y ==> \<not> y < x" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
489 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
490 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
491 |
lemma "((x::real) \<noteq> y) = (x < y \<or> y < x)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
492 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
493 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
494 |
lemma "(\<not> x \<le> y) = (y < (x::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
495 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
496 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
497 |
lemma "x \<le> y \<or> y \<le> (x::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
498 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
499 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
500 |
lemma "x \<le> y \<or> y < (x::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
501 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
502 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
503 |
lemma "x < y \<or> y \<le> (x::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
504 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
505 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
506 |
lemma "x \<le> (x::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
507 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
508 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
509 |
lemma "((x::real) \<le> y) = (x < y \<or> x = y)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
510 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
511 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
512 |
lemma "((x::real) \<le> y \<and> y \<le> x) = (x = y)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
513 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
514 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
515 |
lemma "\<not>(x < y \<and> y \<le> (x::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
516 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
517 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
518 |
lemma "\<not>(x \<le> y \<and> y < (x::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
519 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
520 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
521 |
lemma "(-x < (0::real)) = (0 < x)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
522 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
523 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
524 |
lemma "((0::real) < -x) = (x < 0)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
525 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
526 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
527 |
lemma "(-x \<le> (0::real)) = (0 \<le> x)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
528 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
529 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
530 |
lemma "((0::real) \<le> -x) = (x \<le> 0)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
531 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
532 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
533 |
lemma "(x::real) = y \<or> x < y \<or> y < x" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
534 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
535 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
536 |
lemma "(x::real) = 0 \<or> 0 < x \<or> 0 < -x" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
537 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
538 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
539 |
lemma "(0::real) \<le> x \<or> 0 \<le> -x" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
540 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
541 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
542 |
lemma "((x::real) + y \<le> x + z) = (y \<le> z)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
543 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
544 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
545 |
lemma "((x::real) + z \<le> y + z) = (x \<le> y)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
546 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
547 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
548 |
lemma "(w::real) < x \<and> y < z ==> w + y < x + z" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
549 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
550 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
551 |
lemma "(w::real) \<le> x \<and> y \<le> z ==> w + y \<le> x + z" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
552 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
553 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
554 |
lemma "(0::real) \<le> x \<and> 0 \<le> y ==> 0 \<le> x + y" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
555 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
556 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
557 |
lemma "(0::real) < x \<and> 0 < y ==> 0 < x + y" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
558 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
559 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
560 |
lemma "(-x < y) = (0 < x + (y::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
561 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
562 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
563 |
lemma "(x < -y) = (x + y < (0::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
564 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
565 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
566 |
lemma "(y < x + -z) = (y + z < (x::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
567 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
568 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
569 |
lemma "(x + -y < z) = (x < z + (y::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
570 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
571 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
572 |
lemma "x \<le> y ==> x < y + (1::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
573 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
574 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
575 |
lemma "(x - y) + y = (x::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
576 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
577 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
578 |
lemma "y + (x - y) = (x::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
579 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
580 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
581 |
lemma "x - x = (0::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
582 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
583 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
584 |
lemma "(x - y = 0) = (x = (y::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
585 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
586 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
587 |
lemma "((0::real) \<le> x + x) = (0 \<le> x)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
588 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
589 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
590 |
lemma "(-x \<le> x) = ((0::real) \<le> x)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
591 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
592 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
593 |
lemma "(x \<le> -x) = (x \<le> (0::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
594 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
595 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
596 |
lemma "(-x = (0::real)) = (x = 0)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
597 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
598 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
599 |
lemma "-(x - y) = y - (x::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
600 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
601 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
602 |
lemma "((0::real) < x - y) = (y < x)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
603 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
604 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
605 |
lemma "((0::real) \<le> x - y) = (y \<le> x)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
606 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
607 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
608 |
lemma "(x + y) - x = (y::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
609 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
610 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
611 |
lemma "(-x = y) = (x = (-y::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
612 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
613 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
614 |
lemma "x < (y::real) ==> \<not>(x = y)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
615 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
616 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
617 |
lemma "(x \<le> x + y) = ((0::real) \<le> y)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
618 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
619 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
620 |
lemma "(y \<le> x + y) = ((0::real) \<le> x)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
621 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
622 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
623 |
lemma "(x < x + y) = ((0::real) < y)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
624 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
625 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
626 |
lemma "(y < x + y) = ((0::real) < x)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
627 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
628 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
629 |
lemma "(x - y) - x = (-y::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
630 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
631 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
632 |
lemma "(x + y < z) = (x < z - (y::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
633 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
634 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
635 |
lemma "(x - y < z) = (x < z + (y::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
636 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
637 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
638 |
lemma "(x < y - z) = (x + z < (y::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
639 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
640 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
641 |
lemma "(x \<le> y - z) = (x + z \<le> (y::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
642 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
643 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
644 |
lemma "(x - y \<le> z) = (x \<le> z + (y::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
645 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
646 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
647 |
lemma "(-x < -y) = (y < (x::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
648 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
649 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
650 |
lemma "(-x \<le> -y) = (y \<le> (x::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
651 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
652 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
653 |
lemma "(a + b) - (c + d) = (a - c) + (b - (d::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
654 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
655 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
656 |
lemma "(0::real) - x = -x" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
657 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
658 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
659 |
lemma "x - (0::real) = x" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
660 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
661 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
662 |
lemma "w \<le> x \<and> y < z ==> w + y < x + (z::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
663 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
664 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
665 |
lemma "w < x \<and> y \<le> z ==> w + y < x + (z::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
666 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
667 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
668 |
lemma "(0::real) \<le> x \<and> 0 < y ==> 0 < x + (y::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
669 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
670 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
671 |
lemma "(0::real) < x \<and> 0 \<le> y ==> 0 < x + y" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
672 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
673 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
674 |
lemma "-x - y = -(x + (y::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
675 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
676 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
677 |
lemma "x - (-y) = x + (y::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
678 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
679 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
680 |
lemma "-x - -y = y - (x::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
681 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
682 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
683 |
lemma "(a - b) + (b - c) = a - (c::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
684 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
685 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
686 |
lemma "(x = y - z) = (x + z = (y::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
687 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
688 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
689 |
lemma "(x - y = z) = (x = z + (y::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
690 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
691 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
692 |
lemma "x - (x - y) = (y::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
693 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
694 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
695 |
lemma "x - (x + y) = -(y::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
696 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
697 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
698 |
lemma "x = y ==> x \<le> (y::real)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
699 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
700 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
701 |
lemma "(0::real) < x ==> \<not>(x = 0)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
702 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
703 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
704 |
lemma "(x + y) * (x - y) = (x * x) - (y * y)" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
705 |
oops |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
706 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
707 |
lemma "(-x = -y) = (x = (y::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
708 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
709 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
710 |
lemma "(-x < -y) = (y < (x::real))" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
711 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
712 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
713 |
lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d" |
31066 | 714 |
by linarith |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
715 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
716 |
lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)" |
31066 | 717 |
by linarith |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
718 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
719 |
lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c" |
31066 | 720 |
by linarith |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
721 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
722 |
lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j" |
31066 | 723 |
by linarith |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
724 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
725 |
lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j" |
31066 | 726 |
by linarith |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
727 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
728 |
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" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
729 |
by arith |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
730 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
731 |
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
732 |
==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l" |
31066 | 733 |
by linarith |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
734 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
735 |
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
736 |
==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l" |
31066 | 737 |
by linarith |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
738 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
739 |
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
740 |
==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i" |
31066 | 741 |
by linarith |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
742 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
743 |
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
744 |
==> 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" |
31066 | 745 |
by linarith |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
746 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
747 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
748 |
subsection{*Complex Arithmetic*} |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
749 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
750 |
lemma "(1359 + 93746*ii) - (2468 + 46375*ii) = -1109 + 47371*ii" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
751 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
752 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
753 |
lemma "- (65745 + -47371*ii) = -65745 + 47371*ii" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
754 |
by simp |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
755 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
756 |
text{*Multiplication requires distributive laws. Perhaps versions instantiated |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
757 |
to literal constants should be added to the simpset.*} |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
758 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
759 |
lemma "(1 + ii) * (1 - ii) = 2" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
760 |
by (simp add: ring_distribs) |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
761 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
762 |
lemma "(1 + 2*ii) * (1 + 3*ii) = -5 + 5*ii" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
763 |
by (simp add: ring_distribs) |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
764 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
765 |
lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii" |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
766 |
by (simp add: ring_distribs) |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
767 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
768 |
text{*No inequalities or linear arithmetic: the complex numbers are unordered!*} |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
769 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
770 |
text{*No powers (not supported yet)*} |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
20807
diff
changeset
|
771 |
|
5545 | 772 |
end |