author | haftmann |
Tue, 15 Jan 2008 16:19:23 +0100 | |
changeset 25919 | 8b1c0d434824 |
parent 20485 | 3078fd2eec7b |
child 26086 | 3c243098b64a |
permissions | -rw-r--r-- |
15647 | 1 |
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *) |
2 |
||
17566 | 3 |
theory HOL4Real imports HOL4Base begin |
14516 | 4 |
|
5 |
;setup_theory realax |
|
6 |
||
17644 | 7 |
lemma HREAL_RDISTRIB: "ALL (x::hreal) (y::hreal) z::hreal. |
14516 | 8 |
hreal_mul (hreal_add x y) z = hreal_add (hreal_mul x z) (hreal_mul y z)" |
9 |
by (import realax HREAL_RDISTRIB) |
|
10 |
||
17644 | 11 |
lemma HREAL_EQ_ADDL: "ALL (x::hreal) y::hreal. x ~= hreal_add x y" |
14516 | 12 |
by (import realax HREAL_EQ_ADDL) |
13 |
||
17644 | 14 |
lemma HREAL_EQ_LADD: "ALL (x::hreal) (y::hreal) z::hreal. |
15 |
(hreal_add x y = hreal_add x z) = (y = z)" |
|
14516 | 16 |
by (import realax HREAL_EQ_LADD) |
17 |
||
17644 | 18 |
lemma HREAL_LT_REFL: "ALL x::hreal. ~ hreal_lt x x" |
14516 | 19 |
by (import realax HREAL_LT_REFL) |
20 |
||
17644 | 21 |
lemma HREAL_LT_ADDL: "ALL (x::hreal) y::hreal. hreal_lt x (hreal_add x y)" |
14516 | 22 |
by (import realax HREAL_LT_ADDL) |
23 |
||
17644 | 24 |
lemma HREAL_LT_NE: "ALL (x::hreal) y::hreal. hreal_lt x y --> x ~= y" |
14516 | 25 |
by (import realax HREAL_LT_NE) |
26 |
||
17644 | 27 |
lemma HREAL_LT_ADDR: "ALL (x::hreal) y::hreal. ~ hreal_lt (hreal_add x y) x" |
14516 | 28 |
by (import realax HREAL_LT_ADDR) |
29 |
||
17644 | 30 |
lemma HREAL_LT_GT: "ALL (x::hreal) y::hreal. hreal_lt x y --> ~ hreal_lt y x" |
14516 | 31 |
by (import realax HREAL_LT_GT) |
32 |
||
17644 | 33 |
lemma HREAL_LT_ADD2: "ALL (x1::hreal) (x2::hreal) (y1::hreal) y2::hreal. |
14516 | 34 |
hreal_lt x1 y1 & hreal_lt x2 y2 --> |
35 |
hreal_lt (hreal_add x1 x2) (hreal_add y1 y2)" |
|
36 |
by (import realax HREAL_LT_ADD2) |
|
37 |
||
17644 | 38 |
lemma HREAL_LT_LADD: "ALL (x::hreal) (y::hreal) z::hreal. |
39 |
hreal_lt (hreal_add x y) (hreal_add x z) = hreal_lt y z" |
|
14516 | 40 |
by (import realax HREAL_LT_LADD) |
41 |
||
42 |
constdefs |
|
43 |
treal_0 :: "hreal * hreal" |
|
44 |
"treal_0 == (hreal_1, hreal_1)" |
|
45 |
||
46 |
lemma treal_0: "treal_0 = (hreal_1, hreal_1)" |
|
47 |
by (import realax treal_0) |
|
48 |
||
49 |
constdefs |
|
50 |
treal_1 :: "hreal * hreal" |
|
51 |
"treal_1 == (hreal_add hreal_1 hreal_1, hreal_1)" |
|
52 |
||
53 |
lemma treal_1: "treal_1 = (hreal_add hreal_1 hreal_1, hreal_1)" |
|
54 |
by (import realax treal_1) |
|
55 |
||
56 |
constdefs |
|
57 |
treal_neg :: "hreal * hreal => hreal * hreal" |
|
17644 | 58 |
"treal_neg == %(x::hreal, y::hreal). (y, x)" |
59 |
||
60 |
lemma treal_neg: "ALL (x::hreal) y::hreal. treal_neg (x, y) = (y, x)" |
|
14516 | 61 |
by (import realax treal_neg) |
62 |
||
63 |
constdefs |
|
64 |
treal_add :: "hreal * hreal => hreal * hreal => hreal * hreal" |
|
17644 | 65 |
"treal_add == |
66 |
%(x1::hreal, y1::hreal) (x2::hreal, y2::hreal). |
|
67 |
(hreal_add x1 x2, hreal_add y1 y2)" |
|
68 |
||
69 |
lemma treal_add: "ALL (x1::hreal) (y1::hreal) (x2::hreal) y2::hreal. |
|
14516 | 70 |
treal_add (x1, y1) (x2, y2) = (hreal_add x1 x2, hreal_add y1 y2)" |
71 |
by (import realax treal_add) |
|
72 |
||
73 |
constdefs |
|
74 |
treal_mul :: "hreal * hreal => hreal * hreal => hreal * hreal" |
|
75 |
"treal_mul == |
|
17644 | 76 |
%(x1::hreal, y1::hreal) (x2::hreal, y2::hreal). |
14516 | 77 |
(hreal_add (hreal_mul x1 x2) (hreal_mul y1 y2), |
78 |
hreal_add (hreal_mul x1 y2) (hreal_mul y1 x2))" |
|
79 |
||
17644 | 80 |
lemma treal_mul: "ALL (x1::hreal) (y1::hreal) (x2::hreal) y2::hreal. |
14516 | 81 |
treal_mul (x1, y1) (x2, y2) = |
82 |
(hreal_add (hreal_mul x1 x2) (hreal_mul y1 y2), |
|
83 |
hreal_add (hreal_mul x1 y2) (hreal_mul y1 x2))" |
|
84 |
by (import realax treal_mul) |
|
85 |
||
86 |
constdefs |
|
87 |
treal_lt :: "hreal * hreal => hreal * hreal => bool" |
|
17644 | 88 |
"treal_lt == |
89 |
%(x1::hreal, y1::hreal) (x2::hreal, y2::hreal). |
|
90 |
hreal_lt (hreal_add x1 y2) (hreal_add x2 y1)" |
|
91 |
||
92 |
lemma treal_lt: "ALL (x1::hreal) (y1::hreal) (x2::hreal) y2::hreal. |
|
14516 | 93 |
treal_lt (x1, y1) (x2, y2) = hreal_lt (hreal_add x1 y2) (hreal_add x2 y1)" |
94 |
by (import realax treal_lt) |
|
95 |
||
96 |
constdefs |
|
97 |
treal_inv :: "hreal * hreal => hreal * hreal" |
|
98 |
"treal_inv == |
|
17644 | 99 |
%(x::hreal, y::hreal). |
14516 | 100 |
if x = y then treal_0 |
101 |
else if hreal_lt y x |
|
102 |
then (hreal_add (hreal_inv (hreal_sub x y)) hreal_1, hreal_1) |
|
103 |
else (hreal_1, hreal_add (hreal_inv (hreal_sub y x)) hreal_1)" |
|
104 |
||
17644 | 105 |
lemma treal_inv: "ALL (x::hreal) y::hreal. |
14516 | 106 |
treal_inv (x, y) = |
107 |
(if x = y then treal_0 |
|
108 |
else if hreal_lt y x |
|
109 |
then (hreal_add (hreal_inv (hreal_sub x y)) hreal_1, hreal_1) |
|
110 |
else (hreal_1, hreal_add (hreal_inv (hreal_sub y x)) hreal_1))" |
|
111 |
by (import realax treal_inv) |
|
112 |
||
113 |
constdefs |
|
114 |
treal_eq :: "hreal * hreal => hreal * hreal => bool" |
|
17644 | 115 |
"treal_eq == |
116 |
%(x1::hreal, y1::hreal) (x2::hreal, y2::hreal). |
|
117 |
hreal_add x1 y2 = hreal_add x2 y1" |
|
118 |
||
119 |
lemma treal_eq: "ALL (x1::hreal) (y1::hreal) (x2::hreal) y2::hreal. |
|
14516 | 120 |
treal_eq (x1, y1) (x2, y2) = (hreal_add x1 y2 = hreal_add x2 y1)" |
121 |
by (import realax treal_eq) |
|
122 |
||
17644 | 123 |
lemma TREAL_EQ_REFL: "ALL x::hreal * hreal. treal_eq x x" |
14516 | 124 |
by (import realax TREAL_EQ_REFL) |
125 |
||
17644 | 126 |
lemma TREAL_EQ_SYM: "ALL (x::hreal * hreal) y::hreal * hreal. treal_eq x y = treal_eq y x" |
14516 | 127 |
by (import realax TREAL_EQ_SYM) |
128 |
||
17644 | 129 |
lemma TREAL_EQ_TRANS: "ALL (x::hreal * hreal) (y::hreal * hreal) z::hreal * hreal. |
130 |
treal_eq x y & treal_eq y z --> treal_eq x z" |
|
14516 | 131 |
by (import realax TREAL_EQ_TRANS) |
132 |
||
17644 | 133 |
lemma TREAL_EQ_EQUIV: "ALL (p::hreal * hreal) q::hreal * hreal. |
134 |
treal_eq p q = (treal_eq p = treal_eq q)" |
|
14516 | 135 |
by (import realax TREAL_EQ_EQUIV) |
136 |
||
17644 | 137 |
lemma TREAL_EQ_AP: "ALL (p::hreal * hreal) q::hreal * hreal. p = q --> treal_eq p q" |
14516 | 138 |
by (import realax TREAL_EQ_AP) |
139 |
||
140 |
lemma TREAL_10: "~ treal_eq treal_1 treal_0" |
|
141 |
by (import realax TREAL_10) |
|
142 |
||
17644 | 143 |
lemma TREAL_ADD_SYM: "ALL (x::hreal * hreal) y::hreal * hreal. treal_add x y = treal_add y x" |
14516 | 144 |
by (import realax TREAL_ADD_SYM) |
145 |
||
17644 | 146 |
lemma TREAL_MUL_SYM: "ALL (x::hreal * hreal) y::hreal * hreal. treal_mul x y = treal_mul y x" |
14516 | 147 |
by (import realax TREAL_MUL_SYM) |
148 |
||
17644 | 149 |
lemma TREAL_ADD_ASSOC: "ALL (x::hreal * hreal) (y::hreal * hreal) z::hreal * hreal. |
150 |
treal_add x (treal_add y z) = treal_add (treal_add x y) z" |
|
14516 | 151 |
by (import realax TREAL_ADD_ASSOC) |
152 |
||
17644 | 153 |
lemma TREAL_MUL_ASSOC: "ALL (x::hreal * hreal) (y::hreal * hreal) z::hreal * hreal. |
154 |
treal_mul x (treal_mul y z) = treal_mul (treal_mul x y) z" |
|
14516 | 155 |
by (import realax TREAL_MUL_ASSOC) |
156 |
||
17644 | 157 |
lemma TREAL_LDISTRIB: "ALL (x::hreal * hreal) (y::hreal * hreal) z::hreal * hreal. |
14516 | 158 |
treal_mul x (treal_add y z) = treal_add (treal_mul x y) (treal_mul x z)" |
159 |
by (import realax TREAL_LDISTRIB) |
|
160 |
||
17644 | 161 |
lemma TREAL_ADD_LID: "ALL x::hreal * hreal. treal_eq (treal_add treal_0 x) x" |
14516 | 162 |
by (import realax TREAL_ADD_LID) |
163 |
||
17644 | 164 |
lemma TREAL_MUL_LID: "ALL x::hreal * hreal. treal_eq (treal_mul treal_1 x) x" |
14516 | 165 |
by (import realax TREAL_MUL_LID) |
166 |
||
17644 | 167 |
lemma TREAL_ADD_LINV: "ALL x::hreal * hreal. treal_eq (treal_add (treal_neg x) x) treal_0" |
14516 | 168 |
by (import realax TREAL_ADD_LINV) |
169 |
||
170 |
lemma TREAL_INV_0: "treal_eq (treal_inv treal_0) treal_0" |
|
171 |
by (import realax TREAL_INV_0) |
|
172 |
||
17644 | 173 |
lemma TREAL_MUL_LINV: "ALL x::hreal * hreal. |
174 |
~ treal_eq x treal_0 --> treal_eq (treal_mul (treal_inv x) x) treal_1" |
|
14516 | 175 |
by (import realax TREAL_MUL_LINV) |
176 |
||
17644 | 177 |
lemma TREAL_LT_TOTAL: "ALL (x::hreal * hreal) y::hreal * hreal. |
178 |
treal_eq x y | treal_lt x y | treal_lt y x" |
|
14516 | 179 |
by (import realax TREAL_LT_TOTAL) |
180 |
||
17644 | 181 |
lemma TREAL_LT_REFL: "ALL x::hreal * hreal. ~ treal_lt x x" |
14516 | 182 |
by (import realax TREAL_LT_REFL) |
183 |
||
17644 | 184 |
lemma TREAL_LT_TRANS: "ALL (x::hreal * hreal) (y::hreal * hreal) z::hreal * hreal. |
185 |
treal_lt x y & treal_lt y z --> treal_lt x z" |
|
14516 | 186 |
by (import realax TREAL_LT_TRANS) |
187 |
||
17644 | 188 |
lemma TREAL_LT_ADD: "ALL (x::hreal * hreal) (y::hreal * hreal) z::hreal * hreal. |
189 |
treal_lt y z --> treal_lt (treal_add x y) (treal_add x z)" |
|
14516 | 190 |
by (import realax TREAL_LT_ADD) |
191 |
||
17644 | 192 |
lemma TREAL_LT_MUL: "ALL (x::hreal * hreal) y::hreal * hreal. |
14516 | 193 |
treal_lt treal_0 x & treal_lt treal_0 y --> |
194 |
treal_lt treal_0 (treal_mul x y)" |
|
195 |
by (import realax TREAL_LT_MUL) |
|
196 |
||
197 |
constdefs |
|
198 |
treal_of_hreal :: "hreal => hreal * hreal" |
|
17644 | 199 |
"treal_of_hreal == %x::hreal. (hreal_add x hreal_1, hreal_1)" |
200 |
||
201 |
lemma treal_of_hreal: "ALL x::hreal. treal_of_hreal x = (hreal_add x hreal_1, hreal_1)" |
|
14516 | 202 |
by (import realax treal_of_hreal) |
203 |
||
204 |
constdefs |
|
205 |
hreal_of_treal :: "hreal * hreal => hreal" |
|
17644 | 206 |
"hreal_of_treal == %(x::hreal, y::hreal). SOME d::hreal. x = hreal_add y d" |
207 |
||
208 |
lemma hreal_of_treal: "ALL (x::hreal) y::hreal. |
|
209 |
hreal_of_treal (x, y) = (SOME d::hreal. x = hreal_add y d)" |
|
14516 | 210 |
by (import realax hreal_of_treal) |
211 |
||
17644 | 212 |
lemma TREAL_BIJ: "(ALL h::hreal. hreal_of_treal (treal_of_hreal h) = h) & |
213 |
(ALL r::hreal * hreal. |
|
214 |
treal_lt treal_0 r = treal_eq (treal_of_hreal (hreal_of_treal r)) r)" |
|
14516 | 215 |
by (import realax TREAL_BIJ) |
216 |
||
17644 | 217 |
lemma TREAL_ISO: "ALL (h::hreal) i::hreal. |
218 |
hreal_lt h i --> treal_lt (treal_of_hreal h) (treal_of_hreal i)" |
|
14516 | 219 |
by (import realax TREAL_ISO) |
220 |
||
17644 | 221 |
lemma TREAL_BIJ_WELLDEF: "ALL (h::hreal * hreal) i::hreal * hreal. |
222 |
treal_eq h i --> hreal_of_treal h = hreal_of_treal i" |
|
14516 | 223 |
by (import realax TREAL_BIJ_WELLDEF) |
224 |
||
17644 | 225 |
lemma TREAL_NEG_WELLDEF: "ALL (x1::hreal * hreal) x2::hreal * hreal. |
226 |
treal_eq x1 x2 --> treal_eq (treal_neg x1) (treal_neg x2)" |
|
14516 | 227 |
by (import realax TREAL_NEG_WELLDEF) |
228 |
||
17644 | 229 |
lemma TREAL_ADD_WELLDEFR: "ALL (x1::hreal * hreal) (x2::hreal * hreal) y::hreal * hreal. |
230 |
treal_eq x1 x2 --> treal_eq (treal_add x1 y) (treal_add x2 y)" |
|
14516 | 231 |
by (import realax TREAL_ADD_WELLDEFR) |
232 |
||
17644 | 233 |
lemma TREAL_ADD_WELLDEF: "ALL (x1::hreal * hreal) (x2::hreal * hreal) (y1::hreal * hreal) |
234 |
y2::hreal * hreal. |
|
14516 | 235 |
treal_eq x1 x2 & treal_eq y1 y2 --> |
236 |
treal_eq (treal_add x1 y1) (treal_add x2 y2)" |
|
237 |
by (import realax TREAL_ADD_WELLDEF) |
|
238 |
||
17644 | 239 |
lemma TREAL_MUL_WELLDEFR: "ALL (x1::hreal * hreal) (x2::hreal * hreal) y::hreal * hreal. |
240 |
treal_eq x1 x2 --> treal_eq (treal_mul x1 y) (treal_mul x2 y)" |
|
14516 | 241 |
by (import realax TREAL_MUL_WELLDEFR) |
242 |
||
17644 | 243 |
lemma TREAL_MUL_WELLDEF: "ALL (x1::hreal * hreal) (x2::hreal * hreal) (y1::hreal * hreal) |
244 |
y2::hreal * hreal. |
|
14516 | 245 |
treal_eq x1 x2 & treal_eq y1 y2 --> |
246 |
treal_eq (treal_mul x1 y1) (treal_mul x2 y2)" |
|
247 |
by (import realax TREAL_MUL_WELLDEF) |
|
248 |
||
17644 | 249 |
lemma TREAL_LT_WELLDEFR: "ALL (x1::hreal * hreal) (x2::hreal * hreal) y::hreal * hreal. |
250 |
treal_eq x1 x2 --> treal_lt x1 y = treal_lt x2 y" |
|
14516 | 251 |
by (import realax TREAL_LT_WELLDEFR) |
252 |
||
17644 | 253 |
lemma TREAL_LT_WELLDEFL: "ALL (x::hreal * hreal) (y1::hreal * hreal) y2::hreal * hreal. |
254 |
treal_eq y1 y2 --> treal_lt x y1 = treal_lt x y2" |
|
14516 | 255 |
by (import realax TREAL_LT_WELLDEFL) |
256 |
||
17644 | 257 |
lemma TREAL_LT_WELLDEF: "ALL (x1::hreal * hreal) (x2::hreal * hreal) (y1::hreal * hreal) |
258 |
y2::hreal * hreal. |
|
14516 | 259 |
treal_eq x1 x2 & treal_eq y1 y2 --> treal_lt x1 y1 = treal_lt x2 y2" |
260 |
by (import realax TREAL_LT_WELLDEF) |
|
261 |
||
17644 | 262 |
lemma TREAL_INV_WELLDEF: "ALL (x1::hreal * hreal) x2::hreal * hreal. |
263 |
treal_eq x1 x2 --> treal_eq (treal_inv x1) (treal_inv x2)" |
|
14516 | 264 |
by (import realax TREAL_INV_WELLDEF) |
265 |
||
266 |
;end_setup |
|
267 |
||
268 |
;setup_theory real |
|
269 |
||
17652 | 270 |
lemma REAL_0: "(op =::real => real => bool) (0::real) (0::real)" |
14516 | 271 |
by (import real REAL_0) |
272 |
||
17652 | 273 |
lemma REAL_1: "(op =::real => real => bool) (1::real) (1::real)" |
14516 | 274 |
by (import real REAL_1) |
275 |
||
17652 | 276 |
lemma REAL_ADD_LID_UNIQ: "ALL (x::real) y::real. (x + y = y) = (x = 0)" |
14516 | 277 |
by (import real REAL_ADD_LID_UNIQ) |
278 |
||
17652 | 279 |
lemma REAL_ADD_RID_UNIQ: "ALL (x::real) y::real. (x + y = x) = (y = 0)" |
14516 | 280 |
by (import real REAL_ADD_RID_UNIQ) |
281 |
||
17652 | 282 |
lemma REAL_LNEG_UNIQ: "ALL (x::real) y::real. (x + y = 0) = (x = - y)" |
14516 | 283 |
by (import real REAL_LNEG_UNIQ) |
284 |
||
285 |
lemma REAL_LT_ANTISYM: "ALL (x::real) y::real. ~ (x < y & y < x)" |
|
286 |
by (import real REAL_LT_ANTISYM) |
|
287 |
||
288 |
lemma REAL_LTE_TOTAL: "ALL (x::real) y::real. x < y | y <= x" |
|
289 |
by (import real REAL_LTE_TOTAL) |
|
290 |
||
291 |
lemma REAL_LET_ANTISYM: "ALL (x::real) y::real. ~ (x < y & y <= x)" |
|
292 |
by (import real REAL_LET_ANTISYM) |
|
293 |
||
294 |
lemma REAL_LTE_ANTSYM: "ALL (x::real) y::real. ~ (x <= y & y < x)" |
|
295 |
by (import real REAL_LTE_ANTSYM) |
|
296 |
||
17652 | 297 |
lemma REAL_LT_NEGTOTAL: "ALL x::real. x = 0 | 0 < x | 0 < - x" |
14516 | 298 |
by (import real REAL_LT_NEGTOTAL) |
299 |
||
17652 | 300 |
lemma REAL_LE_NEGTOTAL: "ALL x::real. 0 <= x | 0 <= - x" |
14516 | 301 |
by (import real REAL_LE_NEGTOTAL) |
302 |
||
303 |
lemma REAL_LT_ADDNEG: "ALL (x::real) (y::real) z::real. (y < x + - z) = (y + z < x)" |
|
304 |
by (import real REAL_LT_ADDNEG) |
|
305 |
||
306 |
lemma REAL_LT_ADDNEG2: "ALL (x::real) (y::real) z::real. (x + - y < z) = (x < z + y)" |
|
307 |
by (import real REAL_LT_ADDNEG2) |
|
308 |
||
17652 | 309 |
lemma REAL_LT_ADD1: "ALL (x::real) y::real. x <= y --> x < y + 1" |
14516 | 310 |
by (import real REAL_LT_ADD1) |
311 |
||
14796 | 312 |
lemma REAL_SUB_ADD2: "ALL (x::real) y::real. y + (x - y) = x" |
313 |
by (import real REAL_SUB_ADD2) |
|
314 |
||
17652 | 315 |
lemma REAL_SUB_LT: "ALL (x::real) y::real. (0 < x - y) = (y < x)" |
15647 | 316 |
by (import real REAL_SUB_LT) |
317 |
||
17652 | 318 |
lemma REAL_SUB_LE: "ALL (x::real) y::real. (0 <= x - y) = (y <= x)" |
15647 | 319 |
by (import real REAL_SUB_LE) |
320 |
||
14796 | 321 |
lemma REAL_ADD_SUB: "ALL (x::real) y::real. x + y - x = y" |
322 |
by (import real REAL_ADD_SUB) |
|
14516 | 323 |
|
324 |
lemma REAL_NEG_EQ: "ALL (x::real) y::real. (- x = y) = (x = - y)" |
|
325 |
by (import real REAL_NEG_EQ) |
|
326 |
||
17652 | 327 |
lemma REAL_NEG_MINUS1: "ALL x::real. - x = - 1 * x" |
14516 | 328 |
by (import real REAL_NEG_MINUS1) |
329 |
||
17652 | 330 |
lemma REAL_LT_LMUL_0: "ALL (x::real) y::real. 0 < x --> (0 < x * y) = (0 < y)" |
14516 | 331 |
by (import real REAL_LT_LMUL_0) |
332 |
||
17652 | 333 |
lemma REAL_LT_RMUL_0: "ALL (x::real) y::real. 0 < y --> (0 < x * y) = (0 < x)" |
14516 | 334 |
by (import real REAL_LT_RMUL_0) |
335 |
||
17652 | 336 |
lemma REAL_LT_LMUL: "ALL (x::real) (y::real) z::real. 0 < x --> (x * y < x * z) = (y < z)" |
14516 | 337 |
by (import real REAL_LT_LMUL) |
338 |
||
17652 | 339 |
lemma REAL_LINV_UNIQ: "ALL (x::real) y::real. x * y = 1 --> x = inverse y" |
14516 | 340 |
by (import real REAL_LINV_UNIQ) |
341 |
||
17652 | 342 |
lemma REAL_LE_INV: "(All::(real => bool) => bool) |
343 |
(%x::real. |
|
344 |
(op -->::bool => bool => bool) |
|
345 |
((op <=::real => real => bool) (0::real) x) |
|
346 |
((op <=::real => real => bool) (0::real) ((inverse::real => real) x)))" |
|
14516 | 347 |
by (import real REAL_LE_INV) |
348 |
||
17652 | 349 |
lemma REAL_LE_ADDR: "ALL (x::real) y::real. (x <= x + y) = (0 <= y)" |
14516 | 350 |
by (import real REAL_LE_ADDR) |
351 |
||
17652 | 352 |
lemma REAL_LE_ADDL: "ALL (x::real) y::real. (y <= x + y) = (0 <= x)" |
14516 | 353 |
by (import real REAL_LE_ADDL) |
354 |
||
17652 | 355 |
lemma REAL_LT_ADDR: "ALL (x::real) y::real. (x < x + y) = (0 < y)" |
14516 | 356 |
by (import real REAL_LT_ADDR) |
357 |
||
17652 | 358 |
lemma REAL_LT_ADDL: "ALL (x::real) y::real. (y < x + y) = (0 < x)" |
14516 | 359 |
by (import real REAL_LT_ADDL) |
360 |
||
17652 | 361 |
lemma REAL_LT_NZ: "ALL n::nat. (real n ~= 0) = (0 < real n)" |
14516 | 362 |
by (import real REAL_LT_NZ) |
363 |
||
17652 | 364 |
lemma REAL_NZ_IMP_LT: "ALL n::nat. n ~= 0 --> 0 < real n" |
14516 | 365 |
by (import real REAL_NZ_IMP_LT) |
366 |
||
17652 | 367 |
lemma REAL_LT_RDIV_0: "ALL (y::real) z::real. 0 < z --> (0 < y / z) = (0 < y)" |
14516 | 368 |
by (import real REAL_LT_RDIV_0) |
369 |
||
17652 | 370 |
lemma REAL_LT_RDIV: "ALL (x::real) (y::real) z::real. 0 < z --> (x / z < y / z) = (x < y)" |
14516 | 371 |
by (import real REAL_LT_RDIV) |
372 |
||
17652 | 373 |
lemma REAL_LT_FRACTION_0: "ALL (n::nat) d::real. n ~= 0 --> (0 < d / real n) = (0 < d)" |
14516 | 374 |
by (import real REAL_LT_FRACTION_0) |
375 |
||
17652 | 376 |
lemma REAL_LT_MULTIPLE: "ALL (x::nat) xa::real. 1 < x --> (xa < real x * xa) = (0 < xa)" |
14516 | 377 |
by (import real REAL_LT_MULTIPLE) |
378 |
||
17652 | 379 |
lemma REAL_LT_FRACTION: "ALL (n::nat) d::real. 1 < n --> (d / real n < d) = (0 < d)" |
14516 | 380 |
by (import real REAL_LT_FRACTION) |
381 |
||
17652 | 382 |
lemma REAL_LT_HALF2: "ALL d::real. (d / 2 < d) = (0 < d)" |
14516 | 383 |
by (import real REAL_LT_HALF2) |
384 |
||
17652 | 385 |
lemma REAL_DIV_LMUL: "ALL (x::real) y::real. y ~= 0 --> y * (x / y) = x" |
14516 | 386 |
by (import real REAL_DIV_LMUL) |
387 |
||
17652 | 388 |
lemma REAL_DIV_RMUL: "ALL (x::real) y::real. y ~= 0 --> x / y * y = x" |
14516 | 389 |
by (import real REAL_DIV_RMUL) |
390 |
||
17652 | 391 |
lemma REAL_DOWN: "(All::(real => bool) => bool) |
392 |
(%x::real. |
|
393 |
(op -->::bool => bool => bool) |
|
394 |
((op <::real => real => bool) (0::real) x) |
|
395 |
((Ex::(real => bool) => bool) |
|
396 |
(%xa::real. |
|
397 |
(op &::bool => bool => bool) |
|
398 |
((op <::real => real => bool) (0::real) xa) |
|
399 |
((op <::real => real => bool) xa x))))" |
|
14516 | 400 |
by (import real REAL_DOWN) |
401 |
||
402 |
lemma REAL_SUB_SUB: "ALL (x::real) y::real. x - y - x = - y" |
|
403 |
by (import real REAL_SUB_SUB) |
|
404 |
||
405 |
lemma REAL_ADD2_SUB2: "ALL (a::real) (b::real) (c::real) d::real. a + b - (c + d) = a - c + (b - d)" |
|
406 |
by (import real REAL_ADD2_SUB2) |
|
407 |
||
408 |
lemma REAL_SUB_LNEG: "ALL (x::real) y::real. - x - y = - (x + y)" |
|
409 |
by (import real REAL_SUB_LNEG) |
|
410 |
||
411 |
lemma REAL_SUB_NEG2: "ALL (x::real) y::real. - x - - y = y - x" |
|
412 |
by (import real REAL_SUB_NEG2) |
|
413 |
||
414 |
lemma REAL_SUB_TRIANGLE: "ALL (a::real) (b::real) c::real. a - b + (b - c) = a - c" |
|
415 |
by (import real REAL_SUB_TRIANGLE) |
|
416 |
||
417 |
lemma REAL_INV_MUL: "ALL (x::real) y::real. |
|
17652 | 418 |
x ~= 0 & y ~= 0 --> inverse (x * y) = inverse x * inverse y" |
14516 | 419 |
by (import real REAL_INV_MUL) |
420 |
||
421 |
lemma REAL_SUB_INV2: "ALL (x::real) y::real. |
|
17652 | 422 |
x ~= 0 & y ~= 0 --> inverse x - inverse y = (y - x) / (x * y)" |
14516 | 423 |
by (import real REAL_SUB_INV2) |
424 |
||
425 |
lemma REAL_SUB_SUB2: "ALL (x::real) y::real. x - (x - y) = y" |
|
426 |
by (import real REAL_SUB_SUB2) |
|
427 |
||
428 |
lemma REAL_ADD_SUB2: "ALL (x::real) y::real. x - (x + y) = - y" |
|
429 |
by (import real REAL_ADD_SUB2) |
|
430 |
||
431 |
lemma REAL_LE_MUL2: "ALL (x1::real) (x2::real) (y1::real) y2::real. |
|
17652 | 432 |
0 <= x1 & 0 <= y1 & x1 <= x2 & y1 <= y2 --> x1 * y1 <= x2 * y2" |
14516 | 433 |
by (import real REAL_LE_MUL2) |
434 |
||
17652 | 435 |
lemma REAL_LE_DIV: "ALL (x::real) xa::real. 0 <= x & 0 <= xa --> 0 <= x / xa" |
14516 | 436 |
by (import real REAL_LE_DIV) |
437 |
||
17652 | 438 |
lemma REAL_LT_1: "ALL (x::real) y::real. 0 <= x & x < y --> x / y < 1" |
14516 | 439 |
by (import real REAL_LT_1) |
440 |
||
17652 | 441 |
lemma REAL_POS_NZ: "(All::(real => bool) => bool) |
442 |
(%x::real. |
|
443 |
(op -->::bool => bool => bool) |
|
444 |
((op <::real => real => bool) (0::real) x) |
|
445 |
((Not::bool => bool) ((op =::real => real => bool) x (0::real))))" |
|
14516 | 446 |
by (import real REAL_POS_NZ) |
447 |
||
17652 | 448 |
lemma REAL_EQ_LMUL_IMP: "ALL (x::real) (xa::real) xb::real. x ~= 0 & x * xa = x * xb --> xa = xb" |
14516 | 449 |
by (import real REAL_EQ_LMUL_IMP) |
450 |
||
17652 | 451 |
lemma REAL_FACT_NZ: "ALL n::nat. real (FACT n) ~= 0" |
14516 | 452 |
by (import real REAL_FACT_NZ) |
453 |
||
454 |
lemma REAL_DIFFSQ: "ALL (x::real) y::real. (x + y) * (x - y) = x * x - y * y" |
|
455 |
by (import real REAL_DIFFSQ) |
|
456 |
||
17652 | 457 |
lemma REAL_POASQ: "ALL x::real. (0 < x * x) = (x ~= 0)" |
14516 | 458 |
by (import real REAL_POASQ) |
459 |
||
17652 | 460 |
lemma REAL_SUMSQ: "ALL (x::real) y::real. (x * x + y * y = 0) = (x = 0 & y = 0)" |
14516 | 461 |
by (import real REAL_SUMSQ) |
462 |
||
17188 | 463 |
lemma REAL_DIV_MUL2: "ALL (x::real) z::real. |
17652 | 464 |
x ~= 0 & z ~= 0 --> (ALL y::real. y / z = x * y / (x * z))" |
17188 | 465 |
by (import real REAL_DIV_MUL2) |
466 |
||
17652 | 467 |
lemma REAL_MIDDLE1: "ALL (a::real) b::real. a <= b --> a <= (a + b) / 2" |
14516 | 468 |
by (import real REAL_MIDDLE1) |
469 |
||
17652 | 470 |
lemma REAL_MIDDLE2: "ALL (a::real) b::real. a <= b --> (a + b) / 2 <= b" |
14516 | 471 |
by (import real REAL_MIDDLE2) |
472 |
||
473 |
lemma ABS_LT_MUL2: "ALL (w::real) (x::real) (y::real) z::real. |
|
474 |
abs w < y & abs x < z --> abs (w * x) < y * z" |
|
475 |
by (import real ABS_LT_MUL2) |
|
476 |
||
17652 | 477 |
lemma ABS_REFL: "ALL x::real. (abs x = x) = (0 <= x)" |
14516 | 478 |
by (import real ABS_REFL) |
479 |
||
480 |
lemma ABS_BETWEEN: "ALL (x::real) (y::real) d::real. |
|
17652 | 481 |
(0 < d & x - d < y & y < x + d) = (abs (y - x) < d)" |
14516 | 482 |
by (import real ABS_BETWEEN) |
483 |
||
484 |
lemma ABS_BOUND: "ALL (x::real) (y::real) d::real. abs (x - y) < d --> y < x + d" |
|
485 |
by (import real ABS_BOUND) |
|
486 |
||
17652 | 487 |
lemma ABS_STILLNZ: "ALL (x::real) y::real. abs (x - y) < abs y --> x ~= 0" |
14516 | 488 |
by (import real ABS_STILLNZ) |
489 |
||
17652 | 490 |
lemma ABS_CASES: "ALL x::real. x = 0 | 0 < abs x" |
14516 | 491 |
by (import real ABS_CASES) |
492 |
||
493 |
lemma ABS_BETWEEN1: "ALL (x::real) (y::real) z::real. x < z & abs (y - x) < z - x --> y < z" |
|
494 |
by (import real ABS_BETWEEN1) |
|
495 |
||
17652 | 496 |
lemma ABS_SIGN: "ALL (x::real) y::real. abs (x - y) < y --> 0 < x" |
14516 | 497 |
by (import real ABS_SIGN) |
498 |
||
17652 | 499 |
lemma ABS_SIGN2: "ALL (x::real) y::real. abs (x - y) < - y --> x < 0" |
14516 | 500 |
by (import real ABS_SIGN2) |
501 |
||
502 |
lemma ABS_CIRCLE: "ALL (x::real) (y::real) h::real. |
|
503 |
abs h < abs y - abs x --> abs (x + h) < abs y" |
|
504 |
by (import real ABS_CIRCLE) |
|
505 |
||
506 |
lemma ABS_BETWEEN2: "ALL (x0::real) (x::real) (y0::real) y::real. |
|
17652 | 507 |
x0 < y0 & abs (x - x0) < (y0 - x0) / 2 & abs (y - y0) < (y0 - x0) / 2 --> |
14516 | 508 |
x < y" |
509 |
by (import real ABS_BETWEEN2) |
|
510 |
||
17652 | 511 |
lemma POW_PLUS1: "ALL e>0. ALL n::nat. 1 + real n * e <= (1 + e) ^ n" |
14516 | 512 |
by (import real POW_PLUS1) |
513 |
||
17652 | 514 |
lemma POW_M1: "(All::(nat => bool) => bool) |
515 |
(%n::nat. |
|
516 |
(op =::real => real => bool) |
|
517 |
((abs::real => real) |
|
518 |
((op ^::real => nat => real) ((uminus::real => real) (1::real)) n)) |
|
519 |
(1::real))" |
|
14516 | 520 |
by (import real POW_M1) |
521 |
||
17652 | 522 |
lemma REAL_LE1_POW2: "(All::(real => bool) => bool) |
523 |
(%x::real. |
|
524 |
(op -->::bool => bool => bool) |
|
525 |
((op <=::real => real => bool) (1::real) x) |
|
526 |
((op <=::real => real => bool) (1::real) |
|
527 |
((op ^::real => nat => real) x |
|
20485 | 528 |
((number_of \<Colon> int => nat) |
529 |
((op BIT \<Colon> int => bit => int) |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
20485
diff
changeset
|
530 |
((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
17652 | 531 |
(bit.B0::bit))))))" |
14516 | 532 |
by (import real REAL_LE1_POW2) |
533 |
||
17652 | 534 |
lemma REAL_LT1_POW2: "(All::(real => bool) => bool) |
535 |
(%x::real. |
|
536 |
(op -->::bool => bool => bool) |
|
537 |
((op <::real => real => bool) (1::real) x) |
|
538 |
((op <::real => real => bool) (1::real) |
|
539 |
((op ^::real => nat => real) x |
|
20485 | 540 |
((number_of \<Colon> int => nat) |
541 |
((op BIT \<Colon> int => bit => int) |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
20485
diff
changeset
|
542 |
((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
17652 | 543 |
(bit.B0::bit))))))" |
14516 | 544 |
by (import real REAL_LT1_POW2) |
545 |
||
17652 | 546 |
lemma POW_POS_LT: "ALL (x::real) n::nat. 0 < x --> 0 < x ^ Suc n" |
14516 | 547 |
by (import real POW_POS_LT) |
548 |
||
17652 | 549 |
lemma POW_LT: "ALL (n::nat) (x::real) y::real. 0 <= x & x < y --> x ^ Suc n < y ^ Suc n" |
14516 | 550 |
by (import real POW_LT) |
551 |
||
17652 | 552 |
lemma POW_ZERO_EQ: "ALL (n::nat) x::real. (x ^ Suc n = 0) = (x = 0)" |
14516 | 553 |
by (import real POW_ZERO_EQ) |
554 |
||
17652 | 555 |
lemma REAL_POW_LT2: "ALL (n::nat) (x::real) y::real. n ~= 0 & 0 <= x & x < y --> x ^ n < y ^ n" |
14516 | 556 |
by (import real REAL_POW_LT2) |
557 |
||
17652 | 558 |
lemma REAL_POW_MONO_LT: "ALL (m::nat) (n::nat) x::real. 1 < x & m < n --> x ^ m < x ^ n" |
17188 | 559 |
by (import real REAL_POW_MONO_LT) |
560 |
||
14516 | 561 |
lemma REAL_SUP_SOMEPOS: "ALL P::real => bool. |
17652 | 562 |
(EX x::real. P x & 0 < x) & (EX z::real. ALL x::real. P x --> x < z) --> |
14516 | 563 |
(EX s::real. ALL y::real. (EX x::real. P x & y < x) = (y < s))" |
564 |
by (import real REAL_SUP_SOMEPOS) |
|
565 |
||
566 |
lemma SUP_LEMMA1: "ALL (P::real => bool) (s::real) d::real. |
|
567 |
(ALL y::real. (EX x::real. P (x + d) & y < x) = (y < s)) --> |
|
568 |
(ALL y::real. (EX x::real. P x & y < x) = (y < s + d))" |
|
569 |
by (import real SUP_LEMMA1) |
|
570 |
||
17652 | 571 |
lemma SUP_LEMMA2: "ALL P::real => bool. Ex P --> (EX (d::real) x::real. P (x + d) & 0 < x)" |
14516 | 572 |
by (import real SUP_LEMMA2) |
573 |
||
574 |
lemma SUP_LEMMA3: "ALL d::real. |
|
575 |
(EX z::real. ALL x::real. (P::real => bool) x --> x < z) --> |
|
576 |
(EX x::real. ALL xa::real. P (xa + d) --> xa < x)" |
|
577 |
by (import real SUP_LEMMA3) |
|
578 |
||
579 |
lemma REAL_SUP_EXISTS: "ALL P::real => bool. |
|
580 |
Ex P & (EX z::real. ALL x::real. P x --> x < z) --> |
|
581 |
(EX x::real. ALL y::real. (EX x::real. P x & y < x) = (y < x))" |
|
582 |
by (import real REAL_SUP_EXISTS) |
|
583 |
||
584 |
constdefs |
|
585 |
sup :: "(real => bool) => real" |
|
17644 | 586 |
"sup == |
587 |
%P::real => bool. |
|
588 |
SOME s::real. ALL y::real. (EX x::real. P x & y < x) = (y < s)" |
|
589 |
||
590 |
lemma sup: "ALL P::real => bool. |
|
591 |
sup P = (SOME s::real. ALL y::real. (EX x::real. P x & y < x) = (y < s))" |
|
14516 | 592 |
by (import real sup) |
593 |
||
17644 | 594 |
lemma REAL_SUP: "ALL P::real => bool. |
595 |
Ex P & (EX z::real. ALL x::real. P x --> x < z) --> |
|
596 |
(ALL y::real. (EX x::real. P x & y < x) = (y < sup P))" |
|
14516 | 597 |
by (import real REAL_SUP) |
598 |
||
17644 | 599 |
lemma REAL_SUP_UBOUND: "ALL P::real => bool. |
600 |
Ex P & (EX z::real. ALL x::real. P x --> x < z) --> |
|
601 |
(ALL y::real. P y --> y <= sup P)" |
|
14516 | 602 |
by (import real REAL_SUP_UBOUND) |
603 |
||
604 |
lemma SETOK_LE_LT: "ALL P::real => bool. |
|
605 |
(Ex P & (EX z::real. ALL x::real. P x --> x <= z)) = |
|
606 |
(Ex P & (EX z::real. ALL x::real. P x --> x < z))" |
|
607 |
by (import real SETOK_LE_LT) |
|
608 |
||
17644 | 609 |
lemma REAL_SUP_LE: "ALL P::real => bool. |
610 |
Ex P & (EX z::real. ALL x::real. P x --> x <= z) --> |
|
611 |
(ALL y::real. (EX x::real. P x & y < x) = (y < sup P))" |
|
14516 | 612 |
by (import real REAL_SUP_LE) |
613 |
||
17644 | 614 |
lemma REAL_SUP_UBOUND_LE: "ALL P::real => bool. |
615 |
Ex P & (EX z::real. ALL x::real. P x --> x <= z) --> |
|
616 |
(ALL y::real. P y --> y <= sup P)" |
|
14516 | 617 |
by (import real REAL_SUP_UBOUND_LE) |
618 |
||
17652 | 619 |
lemma REAL_ARCH_LEAST: "ALL y>0. ALL x>=0. EX n::nat. real n * y <= x & x < real (Suc n) * y" |
14516 | 620 |
by (import real REAL_ARCH_LEAST) |
621 |
||
622 |
consts |
|
623 |
sumc :: "nat => nat => (nat => real) => real" |
|
624 |
||
17652 | 625 |
specification (sumc) sumc: "(ALL (n::nat) f::nat => real. sumc n 0 f = 0) & |
17644 | 626 |
(ALL (n::nat) (m::nat) f::nat => real. |
627 |
sumc n (Suc m) f = sumc n m f + f (n + m))" |
|
14516 | 628 |
by (import real sumc) |
629 |
||
14694 | 630 |
consts |
14516 | 631 |
sum :: "nat * nat => (nat => real) => real" |
14694 | 632 |
|
633 |
defs |
|
15647 | 634 |
sum_def: "(op ==::(nat * nat => (nat => real) => real) |
635 |
=> (nat * nat => (nat => real) => real) => prop) |
|
636 |
(real.sum::nat * nat => (nat => real) => real) |
|
637 |
((split::(nat => nat => (nat => real) => real) |
|
638 |
=> nat * nat => (nat => real) => real) |
|
639 |
(sumc::nat => nat => (nat => real) => real))" |
|
14516 | 640 |
|
17644 | 641 |
lemma SUM_DEF: "ALL (m::nat) (n::nat) f::nat => real. real.sum (m, n) f = sumc m n f" |
14516 | 642 |
by (import real SUM_DEF) |
643 |
||
17644 | 644 |
lemma sum: "ALL (x::nat => real) (xa::nat) xb::nat. |
17652 | 645 |
real.sum (xa, 0) x = 0 & |
14516 | 646 |
real.sum (xa, Suc xb) x = real.sum (xa, xb) x + x (xa + xb)" |
647 |
by (import real sum) |
|
648 |
||
17644 | 649 |
lemma SUM_TWO: "ALL (f::nat => real) (n::nat) p::nat. |
17652 | 650 |
real.sum (0, n) f + real.sum (n, p) f = real.sum (0, n + p) f" |
14516 | 651 |
by (import real SUM_TWO) |
652 |
||
17644 | 653 |
lemma SUM_DIFF: "ALL (f::nat => real) (m::nat) n::nat. |
17652 | 654 |
real.sum (m, n) f = real.sum (0, m + n) f - real.sum (0, m) f" |
14516 | 655 |
by (import real SUM_DIFF) |
656 |
||
17644 | 657 |
lemma ABS_SUM: "ALL (f::nat => real) (m::nat) n::nat. |
658 |
abs (real.sum (m, n) f) <= real.sum (m, n) (%n::nat. abs (f n))" |
|
14516 | 659 |
by (import real ABS_SUM) |
660 |
||
17644 | 661 |
lemma SUM_LE: "ALL (f::nat => real) (g::nat => real) (m::nat) n::nat. |
662 |
(ALL r::nat. m <= r & r < n + m --> f r <= g r) --> |
|
14516 | 663 |
real.sum (m, n) f <= real.sum (m, n) g" |
664 |
by (import real SUM_LE) |
|
665 |
||
17644 | 666 |
lemma SUM_EQ: "ALL (f::nat => real) (g::nat => real) (m::nat) n::nat. |
667 |
(ALL r::nat. m <= r & r < n + m --> f r = g r) --> |
|
14516 | 668 |
real.sum (m, n) f = real.sum (m, n) g" |
669 |
by (import real SUM_EQ) |
|
670 |
||
17644 | 671 |
lemma SUM_POS: "ALL f::nat => real. |
17652 | 672 |
(ALL n::nat. 0 <= f n) --> (ALL (m::nat) n::nat. 0 <= real.sum (m, n) f)" |
14516 | 673 |
by (import real SUM_POS) |
674 |
||
17644 | 675 |
lemma SUM_POS_GEN: "ALL (f::nat => real) m::nat. |
17652 | 676 |
(ALL n::nat. m <= n --> 0 <= f n) --> |
677 |
(ALL n::nat. 0 <= real.sum (m, n) f)" |
|
14516 | 678 |
by (import real SUM_POS_GEN) |
679 |
||
17644 | 680 |
lemma SUM_ABS: "ALL (f::nat => real) (m::nat) x::nat. |
681 |
abs (real.sum (m, x) (%m::nat. abs (f m))) = |
|
682 |
real.sum (m, x) (%m::nat. abs (f m))" |
|
14516 | 683 |
by (import real SUM_ABS) |
684 |
||
17644 | 685 |
lemma SUM_ABS_LE: "ALL (f::nat => real) (m::nat) n::nat. |
686 |
abs (real.sum (m, n) f) <= real.sum (m, n) (%n::nat. abs (f n))" |
|
14516 | 687 |
by (import real SUM_ABS_LE) |
688 |
||
17644 | 689 |
lemma SUM_ZERO: "ALL (f::nat => real) N::nat. |
17652 | 690 |
(ALL n::nat. N <= n --> f n = 0) --> |
691 |
(ALL (m::nat) n::nat. N <= m --> real.sum (m, n) f = 0)" |
|
14516 | 692 |
by (import real SUM_ZERO) |
693 |
||
17644 | 694 |
lemma SUM_ADD: "ALL (f::nat => real) (g::nat => real) (m::nat) n::nat. |
695 |
real.sum (m, n) (%n::nat. f n + g n) = |
|
696 |
real.sum (m, n) f + real.sum (m, n) g" |
|
14516 | 697 |
by (import real SUM_ADD) |
698 |
||
17644 | 699 |
lemma SUM_CMUL: "ALL (f::nat => real) (c::real) (m::nat) n::nat. |
700 |
real.sum (m, n) (%n::nat. c * f n) = c * real.sum (m, n) f" |
|
14516 | 701 |
by (import real SUM_CMUL) |
702 |
||
17644 | 703 |
lemma SUM_NEG: "ALL (f::nat => real) (n::nat) d::nat. |
704 |
real.sum (n, d) (%n::nat. - f n) = - real.sum (n, d) f" |
|
14516 | 705 |
by (import real SUM_NEG) |
706 |
||
17644 | 707 |
lemma SUM_SUB: "ALL (f::nat => real) (g::nat => real) (m::nat) n::nat. |
708 |
real.sum (m, n) (%x::nat. f x - g x) = |
|
709 |
real.sum (m, n) f - real.sum (m, n) g" |
|
14516 | 710 |
by (import real SUM_SUB) |
711 |
||
17644 | 712 |
lemma SUM_SUBST: "ALL (f::nat => real) (g::nat => real) (m::nat) n::nat. |
713 |
(ALL p::nat. m <= p & p < m + n --> f p = g p) --> |
|
14516 | 714 |
real.sum (m, n) f = real.sum (m, n) g" |
715 |
by (import real SUM_SUBST) |
|
716 |
||
17644 | 717 |
lemma SUM_NSUB: "ALL (n::nat) (f::nat => real) c::real. |
17652 | 718 |
real.sum (0, n) f - real n * c = real.sum (0, n) (%p::nat. f p - c)" |
14516 | 719 |
by (import real SUM_NSUB) |
720 |
||
17644 | 721 |
lemma SUM_BOUND: "ALL (f::nat => real) (k::real) (m::nat) n::nat. |
722 |
(ALL p::nat. m <= p & p < m + n --> f p <= k) --> |
|
14516 | 723 |
real.sum (m, n) f <= real n * k" |
724 |
by (import real SUM_BOUND) |
|
725 |
||
17644 | 726 |
lemma SUM_GROUP: "ALL (n::nat) (k::nat) f::nat => real. |
17652 | 727 |
real.sum (0, n) (%m::nat. real.sum (m * k, k) f) = real.sum (0, n * k) f" |
14516 | 728 |
by (import real SUM_GROUP) |
729 |
||
17652 | 730 |
lemma SUM_1: "ALL (f::nat => real) n::nat. real.sum (n, 1) f = f n" |
14516 | 731 |
by (import real SUM_1) |
732 |
||
17652 | 733 |
lemma SUM_2: "ALL (f::nat => real) n::nat. real.sum (n, 2) f = f n + f (n + 1)" |
14516 | 734 |
by (import real SUM_2) |
735 |
||
17644 | 736 |
lemma SUM_OFFSET: "ALL (f::nat => real) (n::nat) k::nat. |
17652 | 737 |
real.sum (0, n) (%m::nat. f (m + k)) = |
738 |
real.sum (0, n + k) f - real.sum (0, k) f" |
|
14516 | 739 |
by (import real SUM_OFFSET) |
740 |
||
17644 | 741 |
lemma SUM_REINDEX: "ALL (f::nat => real) (m::nat) (k::nat) n::nat. |
742 |
real.sum (m + k, n) f = real.sum (m, n) (%r::nat. f (r + k))" |
|
14516 | 743 |
by (import real SUM_REINDEX) |
744 |
||
17652 | 745 |
lemma SUM_0: "ALL (m::nat) n::nat. real.sum (m, n) (%r::nat. 0) = 0" |
14516 | 746 |
by (import real SUM_0) |
747 |
||
14847 | 748 |
lemma SUM_PERMUTE_0: "(All::(nat => bool) => bool) |
749 |
(%n::nat. |
|
750 |
(All::((nat => nat) => bool) => bool) |
|
751 |
(%p::nat => nat. |
|
752 |
(op -->::bool => bool => bool) |
|
753 |
((All::(nat => bool) => bool) |
|
754 |
(%y::nat. |
|
755 |
(op -->::bool => bool => bool) |
|
756 |
((op <::nat => nat => bool) y n) |
|
757 |
((Ex1::(nat => bool) => bool) |
|
758 |
(%x::nat. |
|
759 |
(op &::bool => bool => bool) |
|
760 |
((op <::nat => nat => bool) x n) |
|
761 |
((op =::nat => nat => bool) (p x) y))))) |
|
762 |
((All::((nat => real) => bool) => bool) |
|
763 |
(%f::nat => real. |
|
764 |
(op =::real => real => bool) |
|
765 |
((real.sum::nat * nat => (nat => real) => real) |
|
766 |
((Pair::nat => nat => nat * nat) (0::nat) n) |
|
767 |
(%n::nat. f (p n))) |
|
768 |
((real.sum::nat * nat => (nat => real) => real) |
|
769 |
((Pair::nat => nat => nat * nat) (0::nat) n) f)))))" |
|
14516 | 770 |
by (import real SUM_PERMUTE_0) |
771 |
||
17644 | 772 |
lemma SUM_CANCEL: "ALL (f::nat => real) (n::nat) d::nat. |
773 |
real.sum (n, d) (%n::nat. f (Suc n) - f n) = f (n + d) - f n" |
|
14516 | 774 |
by (import real SUM_CANCEL) |
775 |
||
17652 | 776 |
lemma REAL_EQ_RDIV_EQ: "ALL (x::real) (xa::real) xb::real. 0 < xb --> (x = xa / xb) = (x * xb = xa)" |
14516 | 777 |
by (import real REAL_EQ_RDIV_EQ) |
778 |
||
17652 | 779 |
lemma REAL_EQ_LDIV_EQ: "ALL (x::real) (xa::real) xb::real. 0 < xb --> (x / xb = xa) = (x = xa * xb)" |
14516 | 780 |
by (import real REAL_EQ_LDIV_EQ) |
781 |
||
782 |
;end_setup |
|
783 |
||
784 |
;setup_theory topology |
|
785 |
||
786 |
constdefs |
|
17652 | 787 |
re_Union :: "(('a => bool) => bool) => 'a => bool" |
17644 | 788 |
"re_Union == |
789 |
%(P::('a::type => bool) => bool) x::'a::type. |
|
790 |
EX s::'a::type => bool. P s & s x" |
|
791 |
||
792 |
lemma re_Union: "ALL P::('a::type => bool) => bool. |
|
793 |
re_Union P = (%x::'a::type. EX s::'a::type => bool. P s & s x)" |
|
14516 | 794 |
by (import topology re_Union) |
795 |
||
796 |
constdefs |
|
17652 | 797 |
re_union :: "('a => bool) => ('a => bool) => 'a => bool" |
17644 | 798 |
"re_union == |
799 |
%(P::'a::type => bool) (Q::'a::type => bool) x::'a::type. P x | Q x" |
|
800 |
||
801 |
lemma re_union: "ALL (P::'a::type => bool) Q::'a::type => bool. |
|
802 |
re_union P Q = (%x::'a::type. P x | Q x)" |
|
14516 | 803 |
by (import topology re_union) |
804 |
||
805 |
constdefs |
|
17652 | 806 |
re_intersect :: "('a => bool) => ('a => bool) => 'a => bool" |
17644 | 807 |
"re_intersect == |
808 |
%(P::'a::type => bool) (Q::'a::type => bool) x::'a::type. P x & Q x" |
|
809 |
||
810 |
lemma re_intersect: "ALL (P::'a::type => bool) Q::'a::type => bool. |
|
811 |
re_intersect P Q = (%x::'a::type. P x & Q x)" |
|
14516 | 812 |
by (import topology re_intersect) |
813 |
||
814 |
constdefs |
|
17652 | 815 |
re_null :: "'a => bool" |
17644 | 816 |
"re_null == %x::'a::type. False" |
817 |
||
818 |
lemma re_null: "re_null = (%x::'a::type. False)" |
|
14516 | 819 |
by (import topology re_null) |
820 |
||
821 |
constdefs |
|
17652 | 822 |
re_universe :: "'a => bool" |
17644 | 823 |
"re_universe == %x::'a::type. True" |
824 |
||
825 |
lemma re_universe: "re_universe = (%x::'a::type. True)" |
|
14516 | 826 |
by (import topology re_universe) |
827 |
||
828 |
constdefs |
|
17652 | 829 |
re_subset :: "('a => bool) => ('a => bool) => bool" |
17644 | 830 |
"re_subset == |
831 |
%(P::'a::type => bool) Q::'a::type => bool. ALL x::'a::type. P x --> Q x" |
|
832 |
||
833 |
lemma re_subset: "ALL (P::'a::type => bool) Q::'a::type => bool. |
|
834 |
re_subset P Q = (ALL x::'a::type. P x --> Q x)" |
|
14516 | 835 |
by (import topology re_subset) |
836 |
||
837 |
constdefs |
|
17652 | 838 |
re_compl :: "('a => bool) => 'a => bool" |
17644 | 839 |
"re_compl == %(P::'a::type => bool) x::'a::type. ~ P x" |
840 |
||
841 |
lemma re_compl: "ALL P::'a::type => bool. re_compl P = (%x::'a::type. ~ P x)" |
|
14516 | 842 |
by (import topology re_compl) |
843 |
||
17644 | 844 |
lemma SUBSET_REFL: "ALL P::'a::type => bool. re_subset P P" |
14516 | 845 |
by (import topology SUBSET_REFL) |
846 |
||
17644 | 847 |
lemma COMPL_MEM: "ALL (P::'a::type => bool) x::'a::type. P x = (~ re_compl P x)" |
14516 | 848 |
by (import topology COMPL_MEM) |
849 |
||
17644 | 850 |
lemma SUBSET_ANTISYM: "ALL (P::'a::type => bool) Q::'a::type => bool. |
851 |
(re_subset P Q & re_subset Q P) = (P = Q)" |
|
14516 | 852 |
by (import topology SUBSET_ANTISYM) |
853 |
||
17644 | 854 |
lemma SUBSET_TRANS: "ALL (P::'a::type => bool) (Q::'a::type => bool) R::'a::type => bool. |
855 |
re_subset P Q & re_subset Q R --> re_subset P R" |
|
14516 | 856 |
by (import topology SUBSET_TRANS) |
857 |
||
858 |
constdefs |
|
17652 | 859 |
istopology :: "(('a => bool) => bool) => bool" |
14516 | 860 |
"istopology == |
17644 | 861 |
%L::('a::type => bool) => bool. |
862 |
L re_null & |
|
863 |
L re_universe & |
|
864 |
(ALL (a::'a::type => bool) b::'a::type => bool. |
|
865 |
L a & L b --> L (re_intersect a b)) & |
|
866 |
(ALL P::('a::type => bool) => bool. re_subset P L --> L (re_Union P))" |
|
867 |
||
868 |
lemma istopology: "ALL L::('a::type => bool) => bool. |
|
14516 | 869 |
istopology L = |
870 |
(L re_null & |
|
871 |
L re_universe & |
|
17644 | 872 |
(ALL (a::'a::type => bool) b::'a::type => bool. |
873 |
L a & L b --> L (re_intersect a b)) & |
|
874 |
(ALL P::('a::type => bool) => bool. re_subset P L --> L (re_Union P)))" |
|
14516 | 875 |
by (import topology istopology) |
876 |
||
17644 | 877 |
typedef (open) ('a) topology = "(Collect::((('a::type => bool) => bool) => bool) |
878 |
=> (('a::type => bool) => bool) set) |
|
879 |
(istopology::(('a::type => bool) => bool) => bool)" |
|
14516 | 880 |
by (rule typedef_helper,import topology topology_TY_DEF) |
881 |
||
882 |
lemmas topology_TY_DEF = typedef_hol2hol4 [OF type_definition_topology] |
|
883 |
||
884 |
consts |
|
17652 | 885 |
topology :: "(('a => bool) => bool) => 'a topology" |
886 |
"open" :: "'a topology => ('a => bool) => bool" |
|
17644 | 887 |
|
888 |
specification ("open" topology) topology_tybij: "(ALL a::'a::type topology. topology (open a) = a) & |
|
889 |
(ALL r::('a::type => bool) => bool. istopology r = (open (topology r) = r))" |
|
14516 | 890 |
by (import topology topology_tybij) |
891 |
||
17644 | 892 |
lemma TOPOLOGY: "ALL L::'a::type topology. |
14516 | 893 |
open L re_null & |
894 |
open L re_universe & |
|
17644 | 895 |
(ALL (a::'a::type => bool) b::'a::type => bool. |
896 |
open L a & open L b --> open L (re_intersect a b)) & |
|
897 |
(ALL P::('a::type => bool) => bool. |
|
898 |
re_subset P (open L) --> open L (re_Union P))" |
|
14516 | 899 |
by (import topology TOPOLOGY) |
900 |
||
17644 | 901 |
lemma TOPOLOGY_UNION: "ALL (x::'a::type topology) xa::('a::type => bool) => bool. |
902 |
re_subset xa (open x) --> open x (re_Union xa)" |
|
14516 | 903 |
by (import topology TOPOLOGY_UNION) |
904 |
||
905 |
constdefs |
|
17652 | 906 |
neigh :: "'a topology => ('a => bool) * 'a => bool" |
17644 | 907 |
"neigh == |
908 |
%(top::'a::type topology) (N::'a::type => bool, x::'a::type). |
|
909 |
EX P::'a::type => bool. open top P & re_subset P N & P x" |
|
910 |
||
911 |
lemma neigh: "ALL (top::'a::type topology) (N::'a::type => bool) x::'a::type. |
|
912 |
neigh top (N, x) = |
|
913 |
(EX P::'a::type => bool. open top P & re_subset P N & P x)" |
|
14516 | 914 |
by (import topology neigh) |
915 |
||
17644 | 916 |
lemma OPEN_OWN_NEIGH: "ALL (S'::'a::type => bool) (top::'a::type topology) x::'a::type. |
917 |
open top S' & S' x --> neigh top (S', x)" |
|
14516 | 918 |
by (import topology OPEN_OWN_NEIGH) |
919 |
||
17644 | 920 |
lemma OPEN_UNOPEN: "ALL (S'::'a::type => bool) top::'a::type topology. |
921 |
open top S' = |
|
922 |
(re_Union (%P::'a::type => bool. open top P & re_subset P S') = S')" |
|
14516 | 923 |
by (import topology OPEN_UNOPEN) |
924 |
||
17644 | 925 |
lemma OPEN_SUBOPEN: "ALL (S'::'a::type => bool) top::'a::type topology. |
926 |
open top S' = |
|
927 |
(ALL x::'a::type. |
|
928 |
S' x --> (EX P::'a::type => bool. P x & open top P & re_subset P S'))" |
|
14516 | 929 |
by (import topology OPEN_SUBOPEN) |
930 |
||
17644 | 931 |
lemma OPEN_NEIGH: "ALL (S'::'a::type => bool) top::'a::type topology. |
932 |
open top S' = |
|
933 |
(ALL x::'a::type. |
|
934 |
S' x --> (EX N::'a::type => bool. neigh top (N, x) & re_subset N S'))" |
|
14516 | 935 |
by (import topology OPEN_NEIGH) |
936 |
||
937 |
constdefs |
|
17652 | 938 |
closed :: "'a topology => ('a => bool) => bool" |
17644 | 939 |
"closed == %(L::'a::type topology) S'::'a::type => bool. open L (re_compl S')" |
940 |
||
941 |
lemma closed: "ALL (L::'a::type topology) S'::'a::type => bool. |
|
942 |
closed L S' = open L (re_compl S')" |
|
14516 | 943 |
by (import topology closed) |
944 |
||
945 |
constdefs |
|
17652 | 946 |
limpt :: "'a topology => 'a => ('a => bool) => bool" |
17644 | 947 |
"limpt == |
948 |
%(top::'a::type topology) (x::'a::type) S'::'a::type => bool. |
|
949 |
ALL N::'a::type => bool. |
|
950 |
neigh top (N, x) --> (EX y::'a::type. x ~= y & S' y & N y)" |
|
951 |
||
952 |
lemma limpt: "ALL (top::'a::type topology) (x::'a::type) S'::'a::type => bool. |
|
14516 | 953 |
limpt top x S' = |
17644 | 954 |
(ALL N::'a::type => bool. |
955 |
neigh top (N, x) --> (EX y::'a::type. x ~= y & S' y & N y))" |
|
14516 | 956 |
by (import topology limpt) |
957 |
||
17644 | 958 |
lemma CLOSED_LIMPT: "ALL (top::'a::type topology) S'::'a::type => bool. |
959 |
closed top S' = (ALL x::'a::type. limpt top x S' --> S' x)" |
|
14516 | 960 |
by (import topology CLOSED_LIMPT) |
961 |
||
962 |
constdefs |
|
17652 | 963 |
ismet :: "('a * 'a => real) => bool" |
14516 | 964 |
"ismet == |
17644 | 965 |
%m::'a::type * 'a::type => real. |
17652 | 966 |
(ALL (x::'a::type) y::'a::type. (m (x, y) = 0) = (x = y)) & |
17644 | 967 |
(ALL (x::'a::type) (y::'a::type) z::'a::type. |
968 |
m (y, z) <= m (x, y) + m (x, z))" |
|
969 |
||
970 |
lemma ismet: "ALL m::'a::type * 'a::type => real. |
|
14516 | 971 |
ismet m = |
17652 | 972 |
((ALL (x::'a::type) y::'a::type. (m (x, y) = 0) = (x = y)) & |
17644 | 973 |
(ALL (x::'a::type) (y::'a::type) z::'a::type. |
974 |
m (y, z) <= m (x, y) + m (x, z)))" |
|
14516 | 975 |
by (import topology ismet) |
976 |
||
17644 | 977 |
typedef (open) ('a) metric = "(Collect::(('a::type * 'a::type => real) => bool) |
978 |
=> ('a::type * 'a::type => real) set) |
|
979 |
(ismet::('a::type * 'a::type => real) => bool)" |
|
14516 | 980 |
by (rule typedef_helper,import topology metric_TY_DEF) |
981 |
||
982 |
lemmas metric_TY_DEF = typedef_hol2hol4 [OF type_definition_metric] |
|
983 |
||
984 |
consts |
|
17652 | 985 |
metric :: "('a * 'a => real) => 'a metric" |
986 |
dist :: "'a metric => 'a * 'a => real" |
|
17644 | 987 |
|
988 |
specification (dist metric) metric_tybij: "(ALL a::'a::type metric. metric (dist a) = a) & |
|
989 |
(ALL r::'a::type * 'a::type => real. ismet r = (dist (metric r) = r))" |
|
14516 | 990 |
by (import topology metric_tybij) |
991 |
||
17644 | 992 |
lemma METRIC_ISMET: "ALL m::'a::type metric. ismet (dist m)" |
14516 | 993 |
by (import topology METRIC_ISMET) |
994 |
||
17644 | 995 |
lemma METRIC_ZERO: "ALL (m::'a::type metric) (x::'a::type) y::'a::type. |
17652 | 996 |
(dist m (x, y) = 0) = (x = y)" |
14516 | 997 |
by (import topology METRIC_ZERO) |
998 |
||
17652 | 999 |
lemma METRIC_SAME: "ALL (m::'a::type metric) x::'a::type. dist m (x, x) = 0" |
14516 | 1000 |
by (import topology METRIC_SAME) |
1001 |
||
17652 | 1002 |
lemma METRIC_POS: "ALL (m::'a::type metric) (x::'a::type) y::'a::type. 0 <= dist m (x, y)" |
14516 | 1003 |
by (import topology METRIC_POS) |
1004 |
||
17644 | 1005 |
lemma METRIC_SYM: "ALL (m::'a::type metric) (x::'a::type) y::'a::type. |
1006 |
dist m (x, y) = dist m (y, x)" |
|
14516 | 1007 |
by (import topology METRIC_SYM) |
1008 |
||
17644 | 1009 |
lemma METRIC_TRIANGLE: "ALL (m::'a::type metric) (x::'a::type) (y::'a::type) z::'a::type. |
1010 |
dist m (x, z) <= dist m (x, y) + dist m (y, z)" |
|
14516 | 1011 |
by (import topology METRIC_TRIANGLE) |
1012 |
||
17644 | 1013 |
lemma METRIC_NZ: "ALL (m::'a::type metric) (x::'a::type) y::'a::type. |
17652 | 1014 |
x ~= y --> 0 < dist m (x, y)" |
14516 | 1015 |
by (import topology METRIC_NZ) |
1016 |
||
1017 |
constdefs |
|
17652 | 1018 |
mtop :: "'a metric => 'a topology" |
14516 | 1019 |
"mtop == |
17644 | 1020 |
%m::'a::type metric. |
1021 |
topology |
|
1022 |
(%S'::'a::type => bool. |
|
1023 |
ALL x::'a::type. |
|
17652 | 1024 |
S' x --> (EX e>0. ALL y::'a::type. dist m (x, y) < e --> S' y))" |
17644 | 1025 |
|
1026 |
lemma mtop: "ALL m::'a::type metric. |
|
14516 | 1027 |
mtop m = |
1028 |
topology |
|
17644 | 1029 |
(%S'::'a::type => bool. |
1030 |
ALL x::'a::type. |
|
17652 | 1031 |
S' x --> (EX e>0. ALL y::'a::type. dist m (x, y) < e --> S' y))" |
14516 | 1032 |
by (import topology mtop) |
1033 |
||
17644 | 1034 |
lemma mtop_istopology: "ALL m::'a::type metric. |
14516 | 1035 |
istopology |
17644 | 1036 |
(%S'::'a::type => bool. |
1037 |
ALL x::'a::type. |
|
17652 | 1038 |
S' x --> (EX e>0. ALL y::'a::type. dist m (x, y) < e --> S' y))" |
14516 | 1039 |
by (import topology mtop_istopology) |
1040 |
||
17644 | 1041 |
lemma MTOP_OPEN: "ALL (S'::'a::type => bool) x::'a::type metric. |
14516 | 1042 |
open (mtop x) S' = |
17644 | 1043 |
(ALL xa::'a::type. |
17652 | 1044 |
S' xa --> (EX e>0. ALL y::'a::type. dist x (xa, y) < e --> S' y))" |
14516 | 1045 |
by (import topology MTOP_OPEN) |
1046 |
||
1047 |
constdefs |
|
17652 | 1048 |
B :: "'a metric => 'a * real => 'a => bool" |
17644 | 1049 |
"B == |
1050 |
%(m::'a::type metric) (x::'a::type, e::real) y::'a::type. dist m (x, y) < e" |
|
1051 |
||
1052 |
lemma ball: "ALL (m::'a::type metric) (x::'a::type) e::real. |
|
1053 |
B m (x, e) = (%y::'a::type. dist m (x, y) < e)" |
|
14516 | 1054 |
by (import topology ball) |
1055 |
||
17644 | 1056 |
lemma BALL_OPEN: "ALL (m::'a::type metric) (x::'a::type) e::real. |
17652 | 1057 |
0 < e --> open (mtop m) (B m (x, e))" |
14516 | 1058 |
by (import topology BALL_OPEN) |
1059 |
||
17644 | 1060 |
lemma BALL_NEIGH: "ALL (m::'a::type metric) (x::'a::type) e::real. |
17652 | 1061 |
0 < e --> neigh (mtop m) (B m (x, e), x)" |
14516 | 1062 |
by (import topology BALL_NEIGH) |
1063 |
||
17644 | 1064 |
lemma MTOP_LIMPT: "ALL (m::'a::type metric) (x::'a::type) S'::'a::type => bool. |
1065 |
limpt (mtop m) x S' = |
|
17652 | 1066 |
(ALL e>0. EX y::'a::type. x ~= y & S' y & dist m (x, y) < e)" |
14516 | 1067 |
by (import topology MTOP_LIMPT) |
1068 |
||
17644 | 1069 |
lemma ISMET_R1: "ismet (%(x::real, y::real). abs (y - x))" |
14516 | 1070 |
by (import topology ISMET_R1) |
1071 |
||
1072 |
constdefs |
|
1073 |
mr1 :: "real metric" |
|
17644 | 1074 |
"mr1 == metric (%(x::real, y::real). abs (y - x))" |
1075 |
||
1076 |
lemma mr1: "mr1 = metric (%(x::real, y::real). abs (y - x))" |
|
14516 | 1077 |
by (import topology mr1) |
1078 |
||
17644 | 1079 |
lemma MR1_DEF: "ALL (x::real) y::real. dist mr1 (x, y) = abs (y - x)" |
14516 | 1080 |
by (import topology MR1_DEF) |
1081 |
||
17644 | 1082 |
lemma MR1_ADD: "ALL (x::real) d::real. dist mr1 (x, x + d) = abs d" |
14516 | 1083 |
by (import topology MR1_ADD) |
1084 |
||
17644 | 1085 |
lemma MR1_SUB: "ALL (x::real) d::real. dist mr1 (x, x - d) = abs d" |
14516 | 1086 |
by (import topology MR1_SUB) |
1087 |
||
17652 | 1088 |
lemma MR1_ADD_POS: "ALL (x::real) d::real. 0 <= d --> dist mr1 (x, x + d) = d" |
14516 | 1089 |
by (import topology MR1_ADD_POS) |
1090 |
||
17652 | 1091 |
lemma MR1_SUB_LE: "ALL (x::real) d::real. 0 <= d --> dist mr1 (x, x - d) = d" |
14516 | 1092 |
by (import topology MR1_SUB_LE) |
1093 |
||
17652 | 1094 |
lemma MR1_ADD_LT: "ALL (x::real) d::real. 0 < d --> dist mr1 (x, x + d) = d" |
14516 | 1095 |
by (import topology MR1_ADD_LT) |
1096 |
||
17652 | 1097 |
lemma MR1_SUB_LT: "ALL (x::real) d::real. 0 < d --> dist mr1 (x, x - d) = d" |
14516 | 1098 |
by (import topology MR1_SUB_LT) |
1099 |
||
17644 | 1100 |
lemma MR1_BETWEEN1: "ALL (x::real) (y::real) z::real. x < z & dist mr1 (x, y) < z - x --> y < z" |
14516 | 1101 |
by (import topology MR1_BETWEEN1) |
1102 |
||
17644 | 1103 |
lemma MR1_LIMPT: "ALL x::real. limpt (mtop mr1) x re_universe" |
14516 | 1104 |
by (import topology MR1_LIMPT) |
1105 |
||
1106 |
;end_setup |
|
1107 |
||
1108 |
;setup_theory nets |
|
1109 |
||
1110 |
constdefs |
|
17652 | 1111 |
dorder :: "('a => 'a => bool) => bool" |
14516 | 1112 |
"dorder == |
17644 | 1113 |
%g::'a::type => 'a::type => bool. |
1114 |
ALL (x::'a::type) y::'a::type. |
|
1115 |
g x x & g y y --> |
|
1116 |
(EX z::'a::type. g z z & (ALL w::'a::type. g w z --> g w x & g w y))" |
|
1117 |
||
1118 |
lemma dorder: "ALL g::'a::type => 'a::type => bool. |
|
14516 | 1119 |
dorder g = |
17644 | 1120 |
(ALL (x::'a::type) y::'a::type. |
1121 |
g x x & g y y --> |
|
1122 |
(EX z::'a::type. g z z & (ALL w::'a::type. g w z --> g w x & g w y)))" |
|
14516 | 1123 |
by (import nets dorder) |
1124 |
||
1125 |
constdefs |
|
17652 | 1126 |
tends :: "('b => 'a) => 'a => 'a topology * ('b => 'b => bool) => bool" |
14516 | 1127 |
"tends == |
17644 | 1128 |
%(s::'b::type => 'a::type) (l::'a::type) (top::'a::type topology, |
1129 |
g::'b::type => 'b::type => bool). |
|
1130 |
ALL N::'a::type => bool. |
|
14516 | 1131 |
neigh top (N, l) --> |
17644 | 1132 |
(EX n::'b::type. g n n & (ALL m::'b::type. g m n --> N (s m)))" |
1133 |
||
1134 |
lemma tends: "ALL (s::'b::type => 'a::type) (l::'a::type) (top::'a::type topology) |
|
1135 |
g::'b::type => 'b::type => bool. |
|
14516 | 1136 |
tends s l (top, g) = |
17644 | 1137 |
(ALL N::'a::type => bool. |
14516 | 1138 |
neigh top (N, l) --> |
17644 | 1139 |
(EX n::'b::type. g n n & (ALL m::'b::type. g m n --> N (s m))))" |
14516 | 1140 |
by (import nets tends) |
1141 |
||
1142 |
constdefs |
|
17652 | 1143 |
bounded :: "'a metric * ('b => 'b => bool) => ('b => 'a) => bool" |
14516 | 1144 |
"bounded == |
17644 | 1145 |
%(m::'a::type metric, g::'b::type => 'b::type => bool) |
1146 |
f::'b::type => 'a::type. |
|
1147 |
EX (k::real) (x::'a::type) N::'b::type. |
|
1148 |
g N N & (ALL n::'b::type. g n N --> dist m (f n, x) < k)" |
|
1149 |
||
1150 |
lemma bounded: "ALL (m::'a::type metric) (g::'b::type => 'b::type => bool) |
|
1151 |
f::'b::type => 'a::type. |
|
14516 | 1152 |
bounded (m, g) f = |
17644 | 1153 |
(EX (k::real) (x::'a::type) N::'b::type. |
1154 |
g N N & (ALL n::'b::type. g n N --> dist m (f n, x) < k))" |
|
14516 | 1155 |
by (import nets bounded) |
1156 |
||
1157 |
constdefs |
|
17652 | 1158 |
tendsto :: "'a metric * 'a => 'a => 'a => bool" |
17644 | 1159 |
"tendsto == |
1160 |
%(m::'a::type metric, x::'a::type) (y::'a::type) z::'a::type. |
|
17652 | 1161 |
0 < dist m (x, y) & dist m (x, y) <= dist m (x, z)" |
17644 | 1162 |
|
1163 |
lemma tendsto: "ALL (m::'a::type metric) (x::'a::type) (y::'a::type) z::'a::type. |
|
17652 | 1164 |
tendsto (m, x) y z = (0 < dist m (x, y) & dist m (x, y) <= dist m (x, z))" |
14516 | 1165 |
by (import nets tendsto) |
1166 |
||
17644 | 1167 |
lemma DORDER_LEMMA: "ALL g::'a::type => 'a::type => bool. |
14516 | 1168 |
dorder g --> |
17644 | 1169 |
(ALL (P::'a::type => bool) Q::'a::type => bool. |
1170 |
(EX n::'a::type. g n n & (ALL m::'a::type. g m n --> P m)) & |
|
1171 |
(EX n::'a::type. g n n & (ALL m::'a::type. g m n --> Q m)) --> |
|
1172 |
(EX n::'a::type. g n n & (ALL m::'a::type. g m n --> P m & Q m)))" |
|
14516 | 1173 |
by (import nets DORDER_LEMMA) |
1174 |
||
1175 |
lemma DORDER_NGE: "dorder nat_ge" |
|
1176 |
by (import nets DORDER_NGE) |
|
1177 |
||
17644 | 1178 |
lemma DORDER_TENDSTO: "ALL (m::'a::type metric) x::'a::type. dorder (tendsto (m, x))" |
14516 | 1179 |
by (import nets DORDER_TENDSTO) |
1180 |
||
17644 | 1181 |
lemma MTOP_TENDS: "ALL (d::'a::type metric) (g::'b::type => 'b::type => bool) |
1182 |
(x::'b::type => 'a::type) x0::'a::type. |
|
14516 | 1183 |
tends x x0 (mtop d, g) = |
17652 | 1184 |
(ALL e>0. |
17644 | 1185 |
EX n::'b::type. |
1186 |
g n n & (ALL m::'b::type. g m n --> dist d (x m, x0) < e))" |
|
14516 | 1187 |
by (import nets MTOP_TENDS) |
1188 |
||
17644 | 1189 |
lemma MTOP_TENDS_UNIQ: "ALL (g::'b::type => 'b::type => bool) d::'a::type metric. |
14516 | 1190 |
dorder g --> |
17644 | 1191 |
tends (x::'b::type => 'a::type) (x0::'a::type) (mtop d, g) & |
1192 |
tends x (x1::'a::type) (mtop d, g) --> |
|
14516 | 1193 |
x0 = x1" |
1194 |
by (import nets MTOP_TENDS_UNIQ) |
|
1195 |
||
17644 | 1196 |
lemma SEQ_TENDS: "ALL (d::'a::type metric) (x::nat => 'a::type) x0::'a::type. |
14516 | 1197 |
tends x x0 (mtop d, nat_ge) = |
17652 | 1198 |
(ALL xa>0. EX xb::nat. ALL xc::nat. xb <= xc --> dist d (x xc, x0) < xa)" |
14516 | 1199 |
by (import nets SEQ_TENDS) |
1200 |
||
17644 | 1201 |
lemma LIM_TENDS: "ALL (m1::'a::type metric) (m2::'b::type metric) (f::'a::type => 'b::type) |
1202 |
(x0::'a::type) y0::'b::type. |
|
14516 | 1203 |
limpt (mtop m1) x0 re_universe --> |
1204 |
tends f y0 (mtop m2, tendsto (m1, x0)) = |
|
17652 | 1205 |
(ALL e>0. |
1206 |
EX d>0. |
|
17644 | 1207 |
ALL x::'a::type. |
17652 | 1208 |
0 < dist m1 (x, x0) & dist m1 (x, x0) <= d --> |
15647 | 1209 |
dist m2 (f x, y0) < e)" |
14516 | 1210 |
by (import nets LIM_TENDS) |
1211 |
||
17644 | 1212 |
lemma LIM_TENDS2: "ALL (m1::'a::type metric) (m2::'b::type metric) (f::'a::type => 'b::type) |
1213 |
(x0::'a::type) y0::'b::type. |
|
14516 | 1214 |
limpt (mtop m1) x0 re_universe --> |
1215 |
tends f y0 (mtop m2, tendsto (m1, x0)) = |
|
17652 | 1216 |
(ALL e>0. |
1217 |
EX d>0. |
|
17644 | 1218 |
ALL x::'a::type. |
17652 | 1219 |
0 < dist m1 (x, x0) & dist m1 (x, x0) < d --> |
15647 | 1220 |
dist m2 (f x, y0) < e)" |
14516 | 1221 |
by (import nets LIM_TENDS2) |
1222 |
||
17644 | 1223 |
lemma MR1_BOUNDED: "ALL (g::'a::type => 'a::type => bool) f::'a::type => real. |
1224 |
bounded (mr1, g) f = |
|
1225 |
(EX (k::real) N::'a::type. |
|
1226 |
g N N & (ALL n::'a::type. g n N --> abs (f n) < k))" |
|
14516 | 1227 |
by (import nets MR1_BOUNDED) |
1228 |
||
17644 | 1229 |
lemma NET_NULL: "ALL (g::'a::type => 'a::type => bool) (x::'a::type => real) x0::real. |
17652 | 1230 |
tends x x0 (mtop mr1, g) = tends (%n::'a::type. x n - x0) 0 (mtop mr1, g)" |
14516 | 1231 |
by (import nets NET_NULL) |
1232 |
||
17644 | 1233 |
lemma NET_CONV_BOUNDED: "ALL (g::'a::type => 'a::type => bool) (x::'a::type => real) x0::real. |
1234 |
tends x x0 (mtop mr1, g) --> bounded (mr1, g) x" |
|
14516 | 1235 |
by (import nets NET_CONV_BOUNDED) |
1236 |
||
17644 | 1237 |
lemma NET_CONV_NZ: "ALL (g::'a::type => 'a::type => bool) (x::'a::type => real) x0::real. |
17652 | 1238 |
tends x x0 (mtop mr1, g) & x0 ~= 0 --> |
1239 |
(EX N::'a::type. g N N & (ALL n::'a::type. g n N --> x n ~= 0))" |
|
14516 | 1240 |
by (import nets NET_CONV_NZ) |
1241 |
||
17644 | 1242 |
lemma NET_CONV_IBOUNDED: "ALL (g::'a::type => 'a::type => bool) (x::'a::type => real) x0::real. |
17652 | 1243 |
tends x x0 (mtop mr1, g) & x0 ~= 0 --> |
17644 | 1244 |
bounded (mr1, g) (%n::'a::type. inverse (x n))" |
14516 | 1245 |
by (import nets NET_CONV_IBOUNDED) |
1246 |
||
17644 | 1247 |
lemma NET_NULL_ADD: "ALL g::'a::type => 'a::type => bool. |
14516 | 1248 |
dorder g --> |
17644 | 1249 |
(ALL (x::'a::type => real) y::'a::type => real. |
17652 | 1250 |
tends x 0 (mtop mr1, g) & tends y 0 (mtop mr1, g) --> |
1251 |
tends (%n::'a::type. x n + y n) 0 (mtop mr1, g))" |
|
14516 | 1252 |
by (import nets NET_NULL_ADD) |
1253 |
||
17644 | 1254 |
lemma NET_NULL_MUL: "ALL g::'a::type => 'a::type => bool. |
14516 | 1255 |
dorder g --> |
17644 | 1256 |
(ALL (x::'a::type => real) y::'a::type => real. |
17652 | 1257 |
bounded (mr1, g) x & tends y 0 (mtop mr1, g) --> |
1258 |
tends (%n::'a::type. x n * y n) 0 (mtop mr1, g))" |
|
14516 | 1259 |
by (import nets NET_NULL_MUL) |
1260 |
||
17644 | 1261 |
lemma NET_NULL_CMUL: "ALL (g::'a::type => 'a::type => bool) (k::real) x::'a::type => real. |
17652 | 1262 |
tends x 0 (mtop mr1, g) --> tends (%n::'a::type. k * x n) 0 (mtop mr1, g)" |
14516 | 1263 |
by (import nets NET_NULL_CMUL) |
1264 |
||
17644 | 1265 |
lemma NET_ADD: "ALL g::'a::type => 'a::type => bool. |
14516 | 1266 |
dorder g --> |
17644 | 1267 |
(ALL (x::'a::type => real) (x0::real) (y::'a::type => real) y0::real. |
14516 | 1268 |
tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) --> |
17644 | 1269 |
tends (%n::'a::type. x n + y n) (x0 + y0) (mtop mr1, g))" |
14516 | 1270 |
by (import nets NET_ADD) |
1271 |
||
17644 | 1272 |
lemma NET_NEG: "ALL g::'a::type => 'a::type => bool. |
14516 | 1273 |
dorder g --> |
17644 | 1274 |
(ALL (x::'a::type => real) x0::real. |
1275 |
tends x x0 (mtop mr1, g) = |
|
1276 |
tends (%n::'a::type. - x n) (- x0) (mtop mr1, g))" |
|
14516 | 1277 |
by (import nets NET_NEG) |
1278 |
||
17644 | 1279 |
lemma NET_SUB: "ALL g::'a::type => 'a::type => bool. |
14516 | 1280 |
dorder g --> |
17644 | 1281 |
(ALL (x::'a::type => real) (x0::real) (y::'a::type => real) y0::real. |
14516 | 1282 |
tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) --> |
17644 | 1283 |
tends (%xa::'a::type. x xa - y xa) (x0 - y0) (mtop mr1, g))" |
14516 | 1284 |
by (import nets NET_SUB) |
1285 |
||
17644 | 1286 |
lemma NET_MUL: "ALL g::'a::type => 'a::type => bool. |
14516 | 1287 |
dorder g --> |
17644 | 1288 |
(ALL (x::'a::type => real) (y::'a::type => real) (x0::real) y0::real. |
14516 | 1289 |
tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) --> |
17644 | 1290 |
tends (%n::'a::type. x n * y n) (x0 * y0) (mtop mr1, g))" |
14516 | 1291 |
by (import nets NET_MUL) |
1292 |
||
17644 | 1293 |
lemma NET_INV: "ALL g::'a::type => 'a::type => bool. |
14516 | 1294 |
dorder g --> |
17644 | 1295 |
(ALL (x::'a::type => real) x0::real. |
17652 | 1296 |
tends x x0 (mtop mr1, g) & x0 ~= 0 --> |
17644 | 1297 |
tends (%n::'a::type. inverse (x n)) (inverse x0) (mtop mr1, g))" |
14516 | 1298 |
by (import nets NET_INV) |
1299 |
||
17644 | 1300 |
lemma NET_DIV: "ALL g::'a::type => 'a::type => bool. |
14516 | 1301 |
dorder g --> |
17644 | 1302 |
(ALL (x::'a::type => real) (x0::real) (y::'a::type => real) y0::real. |
17652 | 1303 |
tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) & y0 ~= 0 --> |
17644 | 1304 |
tends (%xa::'a::type. x xa / y xa) (x0 / y0) (mtop mr1, g))" |
14516 | 1305 |
by (import nets NET_DIV) |
1306 |
||
17644 | 1307 |
lemma NET_ABS: "ALL (g::'a::type => 'a::type => bool) (x::'a::type => real) x0::real. |
1308 |
tends x x0 (mtop mr1, g) --> |
|
1309 |
tends (%n::'a::type. abs (x n)) (abs x0) (mtop mr1, g)" |
|
14516 | 1310 |
by (import nets NET_ABS) |
1311 |
||
17644 | 1312 |
lemma NET_LE: "ALL g::'a::type => 'a::type => bool. |
14516 | 1313 |
dorder g --> |
17644 | 1314 |
(ALL (x::'a::type => real) (x0::real) (y::'a::type => real) y0::real. |
14516 | 1315 |
tends x x0 (mtop mr1, g) & |
1316 |
tends y y0 (mtop mr1, g) & |
|
17644 | 1317 |
(EX N::'a::type. g N N & (ALL n::'a::type. g n N --> x n <= y n)) --> |
14516 | 1318 |
x0 <= y0)" |
1319 |
by (import nets NET_LE) |
|
1320 |
||
1321 |
;end_setup |
|
1322 |
||
1323 |
;setup_theory seq |
|
1324 |
||
14694 | 1325 |
consts |
17694 | 1326 |
"hol4-->" :: "(nat => real) => real => bool" ("hol4-->") |
14694 | 1327 |
|
1328 |
defs |
|
17694 | 1329 |
"hol4-->_def": "hol4--> == %(x::nat => real) x0::real. tends x x0 (mtop mr1, nat_ge)" |
1330 |
||
1331 |
lemma tends_num_real: "ALL (x::nat => real) x0::real. hol4--> x x0 = tends x x0 (mtop mr1, nat_ge)" |
|
14516 | 1332 |
by (import seq tends_num_real) |
1333 |
||
17694 | 1334 |
lemma SEQ: "ALL (x::nat => real) x0::real. |
1335 |
hol4--> x x0 = |
|
1336 |
(ALL e>0. EX N::nat. ALL n::nat. N <= n --> abs (x n - x0) < e)" |
|
14516 | 1337 |
by (import seq SEQ) |
1338 |
||
17694 | 1339 |
lemma SEQ_CONST: "ALL k::real. hol4--> (%x::nat. k) k" |
14516 | 1340 |
by (import seq SEQ_CONST) |
1341 |
||
17694 | 1342 |
lemma SEQ_ADD: "ALL (x::nat => real) (x0::real) (y::nat => real) y0::real. |
1343 |
hol4--> x x0 & hol4--> y y0 --> hol4--> (%n::nat. x n + y n) (x0 + y0)" |
|
14516 | 1344 |
by (import seq SEQ_ADD) |
1345 |
||
17694 | 1346 |
lemma SEQ_MUL: "ALL (x::nat => real) (x0::real) (y::nat => real) y0::real. |
1347 |
hol4--> x x0 & hol4--> y y0 --> hol4--> (%n::nat. x n * y n) (x0 * y0)" |
|
14516 | 1348 |
by (import seq SEQ_MUL) |
1349 |
||
17694 | 1350 |
lemma SEQ_NEG: "ALL (x::nat => real) x0::real. |
1351 |
hol4--> x x0 = hol4--> (%n::nat. - x n) (- x0)" |
|
14516 | 1352 |
by (import seq SEQ_NEG) |
1353 |
||
17694 | 1354 |
lemma SEQ_INV: "ALL (x::nat => real) x0::real. |
1355 |
hol4--> x x0 & x0 ~= 0 --> hol4--> (%n::nat. inverse (x n)) (inverse x0)" |
|
14516 | 1356 |
by (import seq SEQ_INV) |
1357 |
||
17694 | 1358 |
lemma SEQ_SUB: "ALL (x::nat => real) (x0::real) (y::nat => real) y0::real. |
1359 |
hol4--> x x0 & hol4--> y y0 --> hol4--> (%n::nat. x n - y n) (x0 - y0)" |
|
14516 | 1360 |
by (import seq SEQ_SUB) |
1361 |
||
17694 | 1362 |
lemma SEQ_DIV: "ALL (x::nat => real) (x0::real) (y::nat => real) y0::real. |
1363 |
hol4--> x x0 & hol4--> y y0 & y0 ~= 0 --> |
|
1364 |
hol4--> (%n::nat. x n / y n) (x0 / y0)" |
|
14516 | 1365 |
by (import seq SEQ_DIV) |
1366 |
||
17694 | 1367 |
lemma SEQ_UNIQ: "ALL (x::nat => real) (x1::real) x2::real. |
1368 |
hol4--> x x1 & hol4--> x x2 --> x1 = x2" |
|
14516 | 1369 |
by (import seq SEQ_UNIQ) |
1370 |
||
1371 |
constdefs |
|
1372 |
convergent :: "(nat => real) => bool" |
|
17694 | 1373 |
"convergent == %f::nat => real. Ex (hol4--> f)" |
1374 |
||
1375 |
lemma convergent: "ALL f::nat => real. convergent f = Ex (hol4--> f)" |
|
14516 | 1376 |
by (import seq convergent) |
1377 |
||
1378 |
constdefs |
|
1379 |
cauchy :: "(nat => real) => bool" |
|
17694 | 1380 |
"cauchy == |
1381 |
%f::nat => real. |
|
1382 |
ALL e>0. |
|
1383 |
EX N::nat. |
|
1384 |
ALL (m::nat) n::nat. N <= m & N <= n --> abs (f m - f n) < e" |
|
1385 |
||
1386 |
lemma cauchy: "ALL f::nat => real. |
|
1387 |
cauchy f = |
|
1388 |
(ALL e>0. |
|
1389 |
EX N::nat. |
|
1390 |
ALL (m::nat) n::nat. N <= m & N <= n --> abs (f m - f n) < e)" |
|
14516 | 1391 |
by (import seq cauchy) |
1392 |
||
1393 |
constdefs |
|
1394 |
lim :: "(nat => real) => real" |
|
17694 | 1395 |
"lim == %f::nat => real. Eps (hol4--> f)" |
1396 |
||
1397 |
lemma lim: "ALL f::nat => real. lim f = Eps (hol4--> f)" |
|
14516 | 1398 |
by (import seq lim) |
1399 |
||
17694 | 1400 |
lemma SEQ_LIM: "ALL f::nat => real. convergent f = hol4--> f (lim f)" |
14516 | 1401 |
by (import seq SEQ_LIM) |
1402 |
||
1403 |
constdefs |
|
1404 |
subseq :: "(nat => nat) => bool" |
|
17694 | 1405 |
"subseq == %f::nat => nat. ALL (m::nat) n::nat. m < n --> f m < f n" |
1406 |
||
1407 |
lemma subseq: "ALL f::nat => nat. subseq f = (ALL (m::nat) n::nat. m < n --> f m < f n)" |
|
14516 | 1408 |
by (import seq subseq) |
1409 |
||
17644 | 1410 |
lemma SUBSEQ_SUC: "ALL f::nat => nat. subseq f = (ALL n::nat. f n < f (Suc n))" |
14516 | 1411 |
by (import seq SUBSEQ_SUC) |
1412 |
||
14694 | 1413 |
consts |
14516 | 1414 |
mono :: "(nat => real) => bool" |
14694 | 1415 |
|
1416 |
defs |
|
17694 | 1417 |
mono_def: "seq.mono == |
1418 |
%f::nat => real. |
|
1419 |
(ALL (m::nat) n::nat. m <= n --> f m <= f n) | |
|
1420 |
(ALL (m::nat) n::nat. m <= n --> f n <= f m)" |
|
1421 |
||
1422 |
lemma mono: "ALL f::nat => real. |
|
1423 |
seq.mono f = |
|
1424 |
((ALL (m::nat) n::nat. m <= n --> f m <= f n) | |
|
1425 |
(ALL (m::nat) n::nat. m <= n --> f n <= f m))" |
|
14516 | 1426 |
by (import seq mono) |
1427 |
||
17644 | 1428 |
lemma MONO_SUC: "ALL f::nat => real. |
1429 |
seq.mono f = |
|
1430 |
((ALL x::nat. f x <= f (Suc x)) | (ALL n::nat. f (Suc n) <= f n))" |
|
14516 | 1431 |
by (import seq MONO_SUC) |
1432 |
||
14847 | 1433 |
lemma MAX_LEMMA: "(All::((nat => real) => bool) => bool) |
1434 |
(%s::nat => real. |
|
1435 |
(All::(nat => bool) => bool) |
|
1436 |
(%N::nat. |
|
1437 |
(Ex::(real => bool) => bool) |
|
1438 |
(%k::real. |
|
1439 |
(All::(nat => bool) => bool) |
|
1440 |
(%n::nat. |
|
1441 |
(op -->::bool => bool => bool) |
|
1442 |
((op <::nat => nat => bool) n N) |
|
1443 |
((op <::real => real => bool) |
|
1444 |
((abs::real => real) (s n)) k)))))" |
|
14516 | 1445 |
by (import seq MAX_LEMMA) |
1446 |
||
17644 | 1447 |
lemma SEQ_BOUNDED: "ALL s::nat => real. |
1448 |
bounded (mr1, nat_ge) s = (EX k::real. ALL n::nat. abs (s n) < k)" |
|
14516 | 1449 |
by (import seq SEQ_BOUNDED) |
1450 |
||
17694 | 1451 |
lemma SEQ_BOUNDED_2: "ALL (f::nat => real) (k::real) k'::real. |
1452 |
(ALL n::nat. k <= f n & f n <= k') --> bounded (mr1, nat_ge) f" |
|
14516 | 1453 |
by (import seq SEQ_BOUNDED_2) |
1454 |
||
17694 | 1455 |
lemma SEQ_CBOUNDED: "ALL f::nat => real. cauchy f --> bounded (mr1, nat_ge) f" |
14516 | 1456 |
by (import seq SEQ_CBOUNDED) |
1457 |
||
17694 | 1458 |
lemma SEQ_ICONV: "ALL f::nat => real. |
1459 |
bounded (mr1, nat_ge) f & |
|
1460 |
(ALL (m::nat) n::nat. n <= m --> f n <= f m) --> |
|
1461 |
convergent f" |
|
14516 | 1462 |
by (import seq SEQ_ICONV) |
1463 |
||
17644 | 1464 |
lemma SEQ_NEG_CONV: "ALL f::nat => real. convergent f = convergent (%n::nat. - f n)" |
14516 | 1465 |
by (import seq SEQ_NEG_CONV) |
1466 |
||
17644 | 1467 |
lemma SEQ_NEG_BOUNDED: "ALL f::nat => real. |
1468 |
bounded (mr1, nat_ge) (%n::nat. - f n) = bounded (mr1, nat_ge) f" |
|
14516 | 1469 |
by (import seq SEQ_NEG_BOUNDED) |
1470 |
||
17694 | 1471 |
lemma SEQ_BCONV: "ALL f::nat => real. bounded (mr1, nat_ge) f & seq.mono f --> convergent f" |
14516 | 1472 |
by (import seq SEQ_BCONV) |
1473 |
||
17644 | 1474 |
lemma SEQ_MONOSUB: "ALL s::nat => real. EX f::nat => nat. subseq f & seq.mono (%n::nat. s (f n))" |
14516 | 1475 |
by (import seq SEQ_MONOSUB) |
1476 |
||
17694 | 1477 |
lemma SEQ_SBOUNDED: "ALL (s::nat => real) f::nat => nat. |
1478 |
bounded (mr1, nat_ge) s --> bounded (mr1, nat_ge) (%n::nat. s (f n))" |
|
14516 | 1479 |
by (import seq SEQ_SBOUNDED) |
1480 |
||
17694 | 1481 |
lemma SEQ_SUBLE: "ALL f::nat => nat. subseq f --> (ALL n::nat. n <= f n)" |
14516 | 1482 |
by (import seq SEQ_SUBLE) |
1483 |
||
17694 | 1484 |
lemma SEQ_DIRECT: "ALL f::nat => nat. |
1485 |
subseq f --> (ALL (N1::nat) N2::nat. EX x::nat. N1 <= x & N2 <= f x)" |
|
14516 | 1486 |
by (import seq SEQ_DIRECT) |
1487 |
||
17644 | 1488 |
lemma SEQ_CAUCHY: "ALL f::nat => real. cauchy f = convergent f" |
14516 | 1489 |
by (import seq SEQ_CAUCHY) |
1490 |
||
17694 | 1491 |
lemma SEQ_LE: "ALL (f::nat => real) (g::nat => real) (l::real) m::real. |
1492 |
hol4--> f l & |
|
1493 |
hol4--> g m & (EX x::nat. ALL xa::nat. x <= xa --> f xa <= g xa) --> |
|
1494 |
l <= m" |
|
14516 | 1495 |
by (import seq SEQ_LE) |
1496 |
||
17694 | 1497 |
lemma SEQ_SUC: "ALL (f::nat => real) l::real. hol4--> f l = hol4--> (%n::nat. f (Suc n)) l" |
14516 | 1498 |
by (import seq SEQ_SUC) |
1499 |
||
17694 | 1500 |
lemma SEQ_ABS: "ALL f::nat => real. hol4--> (%n::nat. abs (f n)) 0 = hol4--> f 0" |
14516 | 1501 |
by (import seq SEQ_ABS) |
1502 |
||
17694 | 1503 |
lemma SEQ_ABS_IMP: "ALL (f::nat => real) l::real. |
1504 |
hol4--> f l --> hol4--> (%n::nat. abs (f n)) (abs l)" |
|
14516 | 1505 |
by (import seq SEQ_ABS_IMP) |
1506 |
||
17694 | 1507 |
lemma SEQ_INV0: "ALL f::nat => real. |
1508 |
(ALL y::real. EX N::nat. ALL n::nat. N <= n --> y < f n) --> |
|
1509 |
hol4--> (%n::nat. inverse (f n)) 0" |
|
14516 | 1510 |
by (import seq SEQ_INV0) |
1511 |
||
17694 | 1512 |
lemma SEQ_POWER_ABS: "ALL c::real. abs c < 1 --> hol4--> (op ^ (abs c)) 0" |
14516 | 1513 |
by (import seq SEQ_POWER_ABS) |
1514 |
||
17694 | 1515 |
lemma SEQ_POWER: "ALL c::real. abs c < 1 --> hol4--> (op ^ c) 0" |
14516 | 1516 |
by (import seq SEQ_POWER) |
1517 |
||
17694 | 1518 |
lemma NEST_LEMMA: "ALL (f::nat => real) g::nat => real. |
1519 |
(ALL n::nat. f n <= f (Suc n)) & |
|
1520 |
(ALL n::nat. g (Suc n) <= g n) & (ALL n::nat. f n <= g n) --> |
|
1521 |
(EX (l::real) m::real. |
|
1522 |
l <= m & |
|
1523 |
((ALL n::nat. f n <= l) & hol4--> f l) & |
|
1524 |
(ALL n::nat. m <= g n) & hol4--> g m)" |
|
14516 | 1525 |
by (import seq NEST_LEMMA) |
1526 |
||
17694 | 1527 |
lemma NEST_LEMMA_UNIQ: "ALL (f::nat => real) g::nat => real. |
1528 |
(ALL n::nat. f n <= f (Suc n)) & |
|
1529 |
(ALL n::nat. g (Suc n) <= g n) & |
|
1530 |
(ALL n::nat. f n <= g n) & hol4--> (%n::nat. f n - g n) 0 --> |
|
1531 |
(EX x::real. |
|
1532 |
((ALL n::nat. f n <= x) & hol4--> f x) & |
|
1533 |
(ALL n::nat. x <= g n) & hol4--> g x)" |
|
14516 | 1534 |
by (import seq NEST_LEMMA_UNIQ) |
1535 |
||
17694 | 1536 |
lemma BOLZANO_LEMMA: "ALL P::real * real => bool. |
1537 |
(ALL (a::real) (b::real) c::real. |
|
1538 |
a <= b & b <= c & P (a, b) & P (b, c) --> P (a, c)) & |
|
1539 |
(ALL x::real. |
|
1540 |
EX d>0. |
|
1541 |
ALL (a::real) b::real. |
|
1542 |
a <= x & x <= b & b - a < d --> P (a, b)) --> |
|
1543 |
(ALL (a::real) b::real. a <= b --> P (a, b))" |
|
14516 | 1544 |
by (import seq BOLZANO_LEMMA) |
1545 |
||
1546 |
constdefs |
|
1547 |
sums :: "(nat => real) => real => bool" |
|
17694 | 1548 |
"sums == %f::nat => real. hol4--> (%n::nat. real.sum (0, n) f)" |
1549 |
||
1550 |
lemma sums: "ALL (f::nat => real) s::real. |
|
1551 |
sums f s = hol4--> (%n::nat. real.sum (0, n) f) s" |
|
14516 | 1552 |
by (import seq sums) |
1553 |
||
1554 |
constdefs |
|
1555 |
summable :: "(nat => real) => bool" |
|
17644 | 1556 |
"summable == %f::nat => real. Ex (sums f)" |
1557 |
||
1558 |
lemma summable: "ALL f::nat => real. summable f = Ex (sums f)" |
|
14516 | 1559 |
by (import seq summable) |
1560 |
||
1561 |
constdefs |
|
1562 |
suminf :: "(nat => real) => real" |
|
17644 | 1563 |
"suminf == %f::nat => real. Eps (sums f)" |
1564 |
||
1565 |
lemma suminf: "ALL f::nat => real. suminf f = Eps (sums f)" |
|
14516 | 1566 |
by (import seq suminf) |
1567 |
||
17694 | 1568 |
lemma SUM_SUMMABLE: "ALL (f::nat => real) l::real. sums f l --> summable f" |
14516 | 1569 |
by (import seq SUM_SUMMABLE) |
1570 |
||
17694 | 1571 |
lemma SUMMABLE_SUM: "ALL f::nat => real. summable f --> sums f (suminf f)" |
14516 | 1572 |
by (import seq SUMMABLE_SUM) |
1573 |
||
17694 | 1574 |
lemma SUM_UNIQ: "ALL (f::nat => real) x::real. sums f x --> x = suminf f" |
14516 | 1575 |
by (import seq SUM_UNIQ) |
1576 |
||
17694 | 1577 |
lemma SER_0: "ALL (f::nat => real) n::nat. |
1578 |
(ALL m::nat. n <= m --> f m = 0) --> sums f (real.sum (0, n) f)" |
|
14516 | 1579 |
by (import seq SER_0) |
1580 |
||
17694 | 1581 |
lemma SER_POS_LE: "ALL (f::nat => real) n::nat. |
1582 |
summable f & (ALL m::nat. n <= m --> 0 <= f m) --> |
|
1583 |
real.sum (0, n) f <= suminf f" |
|
14516 | 1584 |
by (import seq SER_POS_LE) |
1585 |
||
17694 | 1586 |
lemma SER_POS_LT: "ALL (f::nat => real) n::nat. |
1587 |
summable f & (ALL m::nat. n <= m --> 0 < f m) --> |
|
1588 |
real.sum (0, n) f < suminf f" |
|
14516 | 1589 |
by (import seq SER_POS_LT) |
1590 |
||
17694 | 1591 |
lemma SER_GROUP: "ALL (f::nat => real) k::nat. |
1592 |
summable f & 0 < k --> sums (%n::nat. real.sum (n * k, k) f) (suminf f)" |
|
14516 | 1593 |
by (import seq SER_GROUP) |
1594 |
||
17694 | 1595 |
lemma SER_PAIR: "ALL f::nat => real. |
1596 |
summable f --> sums (%n::nat. real.sum (2 * n, 2) f) (suminf f)" |
|
14516 | 1597 |
by (import seq SER_PAIR) |
1598 |
||
17694 | 1599 |
lemma SER_OFFSET: "ALL f::nat => real. |
1600 |
summable f --> |
|
1601 |
(ALL k::nat. sums (%n::nat. f (n + k)) (suminf f - real.sum (0, k) f))" |
|
14516 | 1602 |
by (import seq SER_OFFSET) |
1603 |
||
17694 | 1604 |
lemma SER_POS_LT_PAIR: "ALL (f::nat => real) n::nat. |
1605 |
summable f & (ALL d::nat. 0 < f (n + 2 * d) + f (n + (2 * d + 1))) --> |
|
1606 |
real.sum (0, n) f < suminf f" |
|
14516 | 1607 |
by (import seq SER_POS_LT_PAIR) |
1608 |
||
17694 | 1609 |
lemma SER_ADD: "ALL (x::nat => real) (x0::real) (y::nat => real) y0::real. |
1610 |
sums x x0 & sums y y0 --> sums (%n::nat. x n + y n) (x0 + y0)" |
|
14516 | 1611 |
by (import seq SER_ADD) |
1612 |
||
17694 | 1613 |
lemma SER_CMUL: "ALL (x::nat => real) (x0::real) c::real. |
1614 |
sums x x0 --> sums (%n::nat. c * x n) (c * x0)" |
|
14516 | 1615 |
by (import seq SER_CMUL) |
1616 |
||
17694 | 1617 |
lemma SER_NEG: "ALL (x::nat => real) x0::real. sums x x0 --> sums (%xa::nat. - x xa) (- x0)" |
14516 | 1618 |
by (import seq SER_NEG) |
1619 |
||
17694 | 1620 |
lemma SER_SUB: "ALL (x::nat => real) (x0::real) (y::nat => real) y0::real. |
1621 |
sums x x0 & sums y y0 --> sums (%xa::nat. x xa - y xa) (x0 - y0)" |
|
14516 | 1622 |
by (import seq SER_SUB) |
1623 |
||
17694 | 1624 |
lemma SER_CDIV: "ALL (x::nat => real) (x0::real) c::real. |
1625 |
sums x x0 --> sums (%xa::nat. x xa / c) (x0 / c)" |
|
14516 | 1626 |
by (import seq SER_CDIV) |
1627 |
||
17694 | 1628 |
lemma SER_CAUCHY: "ALL f::nat => real. |
1629 |
summable f = |
|
1630 |
(ALL e>0. |
|
1631 |
EX N::nat. |
|
1632 |
ALL (m::nat) n::nat. N <= m --> abs (real.sum (m, n) f) < e)" |
|
14516 | 1633 |
by (import seq SER_CAUCHY) |
1634 |
||
17694 | 1635 |
lemma SER_ZERO: "ALL f::nat => real. summable f --> hol4--> f 0" |
14516 | 1636 |
by (import seq SER_ZERO) |
1637 |
||
17694 | 1638 |
lemma SER_COMPAR: "ALL (f::nat => real) g::nat => real. |
1639 |
(EX x::nat. ALL xa::nat. x <= xa --> abs (f xa) <= g xa) & summable g --> |
|
1640 |
summable f" |
|
14516 | 1641 |
by (import seq SER_COMPAR) |
1642 |
||
17694 | 1643 |
lemma SER_COMPARA: "ALL (f::nat => real) g::nat => real. |
1644 |
(EX x::nat. ALL xa::nat. x <= xa --> abs (f xa) <= g xa) & summable g --> |
|
1645 |
summable (%k::nat. abs (f k))" |
|
14516 | 1646 |
by (import seq SER_COMPARA) |
1647 |
||
17694 | 1648 |
lemma SER_LE: "ALL (f::nat => real) g::nat => real. |
1649 |
(ALL n::nat. f n <= g n) & summable f & summable g --> |
|
1650 |
suminf f <= suminf g" |
|
14516 | 1651 |
by (import seq SER_LE) |
1652 |
||
17694 | 1653 |
lemma SER_LE2: "ALL (f::nat => real) g::nat => real. |
1654 |
(ALL n::nat. abs (f n) <= g n) & summable g --> |
|
1655 |
summable f & suminf f <= suminf g" |
|
14516 | 1656 |
by (import seq SER_LE2) |
1657 |
||
17694 | 1658 |
lemma SER_ACONV: "ALL f::nat => real. summable (%n::nat. abs (f n)) --> summable f" |
14516 | 1659 |
by (import seq SER_ACONV) |
1660 |
||
17694 | 1661 |
lemma SER_ABS: "ALL f::nat => real. |
1662 |
summable (%n::nat. abs (f n)) --> |
|
1663 |
abs (suminf f) <= suminf (%n::nat. abs (f n))" |
|
14516 | 1664 |
by (import seq SER_ABS) |
1665 |
||
17694 | 1666 |
lemma GP_FINITE: "ALL x::real. |
1667 |
x ~= 1 --> (ALL n::nat. real.sum (0, n) (op ^ x) = (x ^ n - 1) / (x - 1))" |
|
14516 | 1668 |
by (import seq GP_FINITE) |
1669 |
||
17694 | 1670 |
lemma GP: "ALL x::real. abs x < 1 --> sums (op ^ x) (inverse (1 - x))" |
14516 | 1671 |
by (import seq GP) |
1672 |
||
1673 |
lemma ABS_NEG_LEMMA: "(All::(real => bool) => bool) |
|
1674 |
(%c::real. |
|
1675 |
(op -->::bool => bool => bool) |
|
1676 |
((op <=::real => real => bool) c (0::real)) |
|
1677 |
((All::(real => bool) => bool) |
|
1678 |
(%x::real. |
|
1679 |
(All::(real => bool) => bool) |
|
1680 |
(%y::real. |
|
1681 |
(op -->::bool => bool => bool) |
|
1682 |
((op <=::real => real => bool) ((abs::real => real) x) |
|
1683 |
((op *::real => real => real) c |
|
1684 |
((abs::real => real) y))) |
|
1685 |
((op =::real => real => bool) x (0::real))))))" |
|
1686 |
by (import seq ABS_NEG_LEMMA) |
|
1687 |
||
17694 | 1688 |
lemma SER_RATIO: "ALL (f::nat => real) (c::real) N::nat. |
1689 |
c < 1 & (ALL n::nat. N <= n --> abs (f (Suc n)) <= c * abs (f n)) --> |
|
1690 |
summable f" |
|
14516 | 1691 |
by (import seq SER_RATIO) |
1692 |
||
1693 |
;end_setup |
|
1694 |
||
1695 |
;setup_theory lim |
|
1696 |
||
1697 |
constdefs |
|
1698 |
tends_real_real :: "(real => real) => real => real => bool" |
|
17644 | 1699 |
"tends_real_real == |
1700 |
%(f::real => real) (l::real) x0::real. |
|
1701 |
tends f l (mtop mr1, tendsto (mr1, x0))" |
|
1702 |
||
1703 |
lemma tends_real_real: "ALL (f::real => real) (l::real) x0::real. |
|
1704 |
tends_real_real f l x0 = tends f l (mtop mr1, tendsto (mr1, x0))" |
|
14516 | 1705 |
by (import lim tends_real_real) |
1706 |
||
17694 | 1707 |
lemma LIM: "ALL (f::real => real) (y0::real) x0::real. |
1708 |
tends_real_real f y0 x0 = |
|
1709 |
(ALL e>0. |
|
1710 |
EX d>0. |
|
1711 |
ALL x::real. |
|
1712 |
0 < abs (x - x0) & abs (x - x0) < d --> abs (f x - y0) < e)" |
|
14516 | 1713 |
by (import lim LIM) |
1714 |
||
17644 | 1715 |
lemma LIM_CONST: "ALL k::real. All (tends_real_real (%x::real. k) k)" |
14516 | 1716 |
by (import lim LIM_CONST) |
1717 |
||
17694 | 1718 |
lemma LIM_ADD: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real. |
1719 |
tends_real_real f l x & tends_real_real g m x --> |
|
1720 |
tends_real_real (%x::real. f x + g x) (l + m) x" |
|
14516 | 1721 |
by (import lim LIM_ADD) |
1722 |
||
17694 | 1723 |
lemma LIM_MUL: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real. |
1724 |
tends_real_real f l x & tends_real_real g m x --> |
|
1725 |
tends_real_real (%x::real. f x * g x) (l * m) x" |
|
14516 | 1726 |
by (import lim LIM_MUL) |
1727 |
||
17644 | 1728 |
lemma LIM_NEG: "ALL (f::real => real) (l::real) x::real. |
1729 |
tends_real_real f l x = tends_real_real (%x::real. - f x) (- l) x" |
|
14516 | 1730 |
by (import lim LIM_NEG) |
1731 |
||
17694 | 1732 |
lemma LIM_INV: "ALL (f::real => real) (l::real) x::real. |
1733 |
tends_real_real f l x & l ~= 0 --> |
|
1734 |
tends_real_real (%x::real. inverse (f x)) (inverse l) x" |
|
14516 | 1735 |
by (import lim LIM_INV) |
1736 |
||
17694 | 1737 |
lemma LIM_SUB: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real. |
1738 |
tends_real_real f l x & tends_real_real g m x --> |
|
1739 |
tends_real_real (%x::real. f x - g x) (l - m) x" |
|
14516 | 1740 |
by (import lim LIM_SUB) |
1741 |
||
17694 | 1742 |
lemma LIM_DIV: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real. |
1743 |
tends_real_real f l x & tends_real_real g m x & m ~= 0 --> |
|
1744 |
tends_real_real (%x::real. f x / g x) (l / m) x" |
|
14516 | 1745 |
by (import lim LIM_DIV) |
1746 |
||
17644 | 1747 |
lemma LIM_NULL: "ALL (f::real => real) (l::real) x::real. |
17652 | 1748 |
tends_real_real f l x = tends_real_real (%x::real. f x - l) 0 x" |
14516 | 1749 |
by (import lim LIM_NULL) |
1750 |
||
17644 | 1751 |
lemma LIM_X: "ALL x0::real. tends_real_real (%x::real. x) x0 x0" |
14516 | 1752 |
by (import lim LIM_X) |
1753 |
||
17694 | 1754 |
lemma LIM_UNIQ: "ALL (f::real => real) (l::real) (m::real) x::real. |
1755 |
tends_real_real f l x & tends_real_real f m x --> l = m" |
|
14516 | 1756 |
by (import lim LIM_UNIQ) |
1757 |
||
17694 | 1758 |
lemma LIM_EQUAL: "ALL (f::real => real) (g::real => real) (l::real) x0::real. |
1759 |
(ALL x::real. x ~= x0 --> f x = g x) --> |
|
1760 |
tends_real_real f l x0 = tends_real_real g l x0" |
|
14516 | 1761 |
by (import lim LIM_EQUAL) |
1762 |
||
17694 | 1763 |
lemma LIM_TRANSFORM: "ALL (f::real => real) (g::real => real) (x0::real) l::real. |
1764 |
tends_real_real (%x::real. f x - g x) 0 x0 & tends_real_real g l x0 --> |
|
1765 |
tends_real_real f l x0" |
|
14516 | 1766 |
by (import lim LIM_TRANSFORM) |
1767 |
||
1768 |
constdefs |
|
1769 |
diffl :: "(real => real) => real => real => bool" |
|
17644 | 1770 |
"diffl == |
1771 |
%(f::real => real) (l::real) x::real. |
|
17652 | 1772 |
tends_real_real (%h::real. (f (x + h) - f x) / h) l 0" |
17644 | 1773 |
|
1774 |
lemma diffl: "ALL (f::real => real) (l::real) x::real. |
|
17652 | 1775 |
diffl f l x = tends_real_real (%h::real. (f (x + h) - f x) / h) l 0" |
14516 | 1776 |
by (import lim diffl) |
1777 |
||
1778 |
constdefs |
|
1779 |
contl :: "(real => real) => real => bool" |
|
17644 | 1780 |
"contl == |
17652 | 1781 |
%(f::real => real) x::real. tends_real_real (%h::real. f (x + h)) (f x) 0" |
17644 | 1782 |
|
1783 |
lemma contl: "ALL (f::real => real) x::real. |
|
17652 | 1784 |
contl f x = tends_real_real (%h::real. f (x + h)) (f x) 0" |
14516 | 1785 |
by (import lim contl) |
1786 |
||
1787 |
constdefs |
|
1788 |
differentiable :: "(real => real) => real => bool" |
|
17644 | 1789 |
"differentiable == %(f::real => real) x::real. EX l::real. diffl f l x" |
1790 |
||
1791 |
lemma differentiable: "ALL (f::real => real) x::real. |
|
1792 |
differentiable f x = (EX l::real. diffl f l x)" |
|
14516 | 1793 |
by (import lim differentiable) |
1794 |
||
17694 | 1795 |
lemma DIFF_UNIQ: "ALL (f::real => real) (l::real) (m::real) x::real. |
1796 |
diffl f l x & diffl f m x --> l = m" |
|
14516 | 1797 |
by (import lim DIFF_UNIQ) |
1798 |
||
17694 | 1799 |
lemma DIFF_CONT: "ALL (f::real => real) (l::real) x::real. diffl f l x --> contl f x" |
14516 | 1800 |
by (import lim DIFF_CONT) |
1801 |
||
17644 | 1802 |
lemma CONTL_LIM: "ALL (f::real => real) x::real. contl f x = tends_real_real f (f x) x" |
14516 | 1803 |
by (import lim CONTL_LIM) |
1804 |
||
17644 | 1805 |
lemma DIFF_CARAT: "ALL (f::real => real) (l::real) x::real. |
14516 | 1806 |
diffl f l x = |
17644 | 1807 |
(EX g::real => real. |
1808 |
(ALL z::real. f z - f x = g z * (z - x)) & contl g x & g x = l)" |
|
14516 | 1809 |
by (import lim DIFF_CARAT) |
1810 |
||
17644 | 1811 |
lemma CONT_CONST: "ALL k::real. All (contl (%x::real. k))" |
14516 | 1812 |
by (import lim CONT_CONST) |
1813 |
||
17694 | 1814 |
lemma CONT_ADD: "ALL (f::real => real) (g::real => real) x::real. |
1815 |
contl f x & contl g x --> contl (%x::real. f x + g x) x" |
|
14516 | 1816 |
by (import lim CONT_ADD) |
1817 |
||
17694 | 1818 |
lemma CONT_MUL: "ALL (f::real => real) (g::real => real) x::real. |
1819 |
contl f x & contl g x --> contl (%x::real. f x * g x) x" |
|
14516 | 1820 |
by (import lim CONT_MUL) |
1821 |
||
17694 | 1822 |
lemma CONT_NEG: "ALL (f::real => real) x::real. contl f x --> contl (%x::real. - f x) x" |
14516 | 1823 |
by (import lim CONT_NEG) |
1824 |
||
17694 | 1825 |
lemma CONT_INV: "ALL (f::real => real) x::real. |
1826 |
contl f x & f x ~= 0 --> contl (%x::real. inverse (f x)) x" |
|
14516 | 1827 |
by (import lim CONT_INV) |
1828 |
||
17694 | 1829 |
lemma CONT_SUB: "ALL (f::real => real) (g::real => real) x::real. |
1830 |
contl f x & contl g x --> contl (%x::real. f x - g x) x" |
|
14516 | 1831 |
by (import lim CONT_SUB) |
1832 |
||
17694 | 1833 |
lemma CONT_DIV: "ALL (f::real => real) (g::real => real) x::real. |
1834 |
contl f x & contl g x & g x ~= 0 --> contl (%x::real. f x / g x) x" |
|
14516 | 1835 |
by (import lim CONT_DIV) |
1836 |
||
17694 | 1837 |
lemma CONT_COMPOSE: "ALL (f::real => real) (g::real => real) x::real. |
1838 |
contl f x & contl g (f x) --> contl (%x::real. g (f x)) x" |
|
14516 | 1839 |
by (import lim CONT_COMPOSE) |
1840 |
||
17694 | 1841 |
lemma IVT: "ALL (f::real => real) (a::real) (b::real) y::real. |
1842 |
a <= b & |
|
1843 |
(f a <= y & y <= f b) & (ALL x::real. a <= x & x <= b --> contl f x) --> |
|
1844 |
(EX x::real. a <= x & x <= b & f x = y)" |
|
14516 | 1845 |
by (import lim IVT) |
1846 |
||
17694 | 1847 |
lemma IVT2: "ALL (f::real => real) (a::real) (b::real) y::real. |
1848 |
a <= b & |
|
1849 |
(f b <= y & y <= f a) & (ALL x::real. a <= x & x <= b --> contl f x) --> |
|
1850 |
(EX x::real. a <= x & x <= b & f x = y)" |
|
14516 | 1851 |
by (import lim IVT2) |
1852 |
||
17652 | 1853 |
lemma DIFF_CONST: "ALL k::real. All (diffl (%x::real. k) 0)" |
14516 | 1854 |
by (import lim DIFF_CONST) |
1855 |
||
17694 | 1856 |
lemma DIFF_ADD: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real. |
1857 |
diffl f l x & diffl g m x --> diffl (%x::real. f x + g x) (l + m) x" |
|
14516 | 1858 |
by (import lim DIFF_ADD) |
1859 |
||
17694 | 1860 |
lemma DIFF_MUL: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real. |
1861 |
diffl f l x & diffl g m x --> |
|
1862 |
diffl (%x::real. f x * g x) (l * g x + m * f x) x" |
|
14516 | 1863 |
by (import lim DIFF_MUL) |
1864 |
||
17694 | 1865 |
lemma DIFF_CMUL: "ALL (f::real => real) (c::real) (l::real) x::real. |
1866 |
diffl f l x --> diffl (%x::real. c * f x) (c * l) x" |
|
14516 | 1867 |
by (import lim DIFF_CMUL) |
1868 |
||
17694 | 1869 |
lemma DIFF_NEG: "ALL (f::real => real) (l::real) x::real. |
1870 |
diffl f l x --> diffl (%x::real. - f x) (- l) x" |
|
14516 | 1871 |
by (import lim DIFF_NEG) |
1872 |
||
17694 | 1873 |
lemma DIFF_SUB: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real. |
1874 |
diffl f l x & diffl g m x --> diffl (%x::real. f x - g x) (l - m) x" |
|
14516 | 1875 |
by (import lim DIFF_SUB) |
1876 |
||
17694 | 1877 |
lemma DIFF_CHAIN: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real. |
1878 |
diffl f l (g x) & diffl g m x --> diffl (%x::real. f (g x)) (l * m) x" |
|
14516 | 1879 |
by (import lim DIFF_CHAIN) |
1880 |
||
17652 | 1881 |
lemma DIFF_X: "All (diffl (%x::real. x) 1)" |
14516 | 1882 |
by (import lim DIFF_X) |
1883 |
||
17652 | 1884 |
lemma DIFF_POW: "ALL (n::nat) x::real. diffl (%x::real. x ^ n) (real n * x ^ (n - 1)) x" |
14516 | 1885 |
by (import lim DIFF_POW) |
1886 |
||
17694 | 1887 |
lemma DIFF_XM1: "ALL x::real. x ~= 0 --> diffl inverse (- (inverse x ^ 2)) x" |
14516 | 1888 |
by (import lim DIFF_XM1) |
1889 |
||
17694 | 1890 |
lemma DIFF_INV: "ALL (f::real => real) (l::real) x::real. |
1891 |
diffl f l x & f x ~= 0 --> |
|
1892 |
diffl (%x::real. inverse (f x)) (- (l / f x ^ 2)) x" |
|
14516 | 1893 |
by (import lim DIFF_INV) |
1894 |
||
17694 | 1895 |
lemma DIFF_DIV: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real. |
1896 |
diffl f l x & diffl g m x & g x ~= 0 --> |
|
1897 |
diffl (%x::real. f x / g x) ((l * g x - m * f x) / g x ^ 2) x" |
|
14516 | 1898 |
by (import lim DIFF_DIV) |
1899 |
||
17694 | 1900 |
lemma DIFF_SUM: "ALL (f::nat => real => real) (f'::nat => real => real) (m::nat) (n::nat) |
1901 |
x::real. |
|
1902 |
(ALL r::nat. m <= r & r < m + n --> diffl (f r) (f' r x) x) --> |
|
1903 |
diffl (%x::real. real.sum (m, n) (%n::nat. f n x)) |
|
1904 |
(real.sum (m, n) (%r::nat. f' r x)) x" |
|
14516 | 1905 |
by (import lim DIFF_SUM) |
1906 |
||
17694 | 1907 |
lemma CONT_BOUNDED: "ALL (f::real => real) (a::real) b::real. |
1908 |
a <= b & (ALL x::real. a <= x & x <= b --> contl f x) --> |
|
1909 |
(EX M::real. ALL x::real. a <= x & x <= b --> f x <= M)" |
|
14516 | 1910 |
by (import lim CONT_BOUNDED) |
1911 |
||
1912 |
lemma CONT_HASSUP: "(All::((real => real) => bool) => bool) |
|
1913 |
(%f::real => real. |
|
1914 |
(All::(real => bool) => bool) |
|
1915 |
(%a::real. |
|
1916 |
(All::(real => bool) => bool) |
|
1917 |
(%b::real. |
|
1918 |
(op -->::bool => bool => bool) |
|
1919 |
((op &::bool => bool => bool) |
|
1920 |
((op <=::real => real => bool) a b) |
|
1921 |
((All::(real => bool) => bool) |
|
1922 |
(%x::real. |
|
1923 |
(op -->::bool => bool => bool) |
|
1924 |
((op &::bool => bool => bool) |
|
1925 |
((op <=::real => real => bool) a x) |
|
1926 |
((op <=::real => real => bool) x b)) |
|
1927 |
((contl::(real => real) => real => bool) f x)))) |
|
1928 |
((Ex::(real => bool) => bool) |
|
1929 |
(%M::real. |
|
1930 |
(op &::bool => bool => bool) |
|
1931 |
((All::(real => bool) => bool) |
|
1932 |
(%x::real. |
|
1933 |
(op -->::bool => bool => bool) |
|
1934 |
((op &::bool => bool => bool) |
|
1935 |
((op <=::real => real => bool) a x) |
|
1936 |
((op <=::real => real => bool) x b)) |
|
1937 |
((op <=::real => real => bool) (f x) M))) |
|
1938 |
((All::(real => bool) => bool) |
|
1939 |
(%N::real. |
|
1940 |
(op -->::bool => bool => bool) |
|
1941 |
((op <::real => real => bool) N M) |
|
1942 |
((Ex::(real => bool) => bool) |
|
1943 |
(%x::real. |
|
1944 |
(op &::bool => bool => bool) |
|
1945 |
((op <=::real => real => bool) a x) |
|
1946 |
((op &::bool => bool => bool) |
|
1947 |
((op <=::real => real => bool) x b) |
|
1948 |
((op <::real => real => bool) N (f x))))))))))))" |
|
1949 |
by (import lim CONT_HASSUP) |
|
1950 |
||
17694 | 1951 |
lemma CONT_ATTAINS: "ALL (f::real => real) (a::real) b::real. |
1952 |
a <= b & (ALL x::real. a <= x & x <= b --> contl f x) --> |
|
1953 |
(EX x::real. |
|
1954 |
(ALL xa::real. a <= xa & xa <= b --> f xa <= x) & |
|
1955 |
(EX xa::real. a <= xa & xa <= b & f xa = x))" |
|
14516 | 1956 |
by (import lim CONT_ATTAINS) |
1957 |
||
17694 | 1958 |
lemma CONT_ATTAINS2: "ALL (f::real => real) (a::real) b::real. |
1959 |
a <= b & (ALL x::real. a <= x & x <= b --> contl f x) --> |
|
1960 |
(EX x::real. |
|
1961 |
(ALL xa::real. a <= xa & xa <= b --> x <= f xa) & |
|
1962 |
(EX xa::real. a <= xa & xa <= b & f xa = x))" |
|
14516 | 1963 |
by (import lim CONT_ATTAINS2) |
1964 |
||
17694 | 1965 |
lemma CONT_ATTAINS_ALL: "ALL (f::real => real) (a::real) b::real. |
1966 |
a <= b & (ALL x::real. a <= x & x <= b --> contl f x) --> |
|
1967 |
(EX (x::real) M::real. |
|
1968 |
x <= M & |
|
1969 |
(ALL y::real. |
|
1970 |
x <= y & y <= M --> (EX x::real. a <= x & x <= b & f x = y)) & |
|
1971 |
(ALL xa::real. a <= xa & xa <= b --> x <= f xa & f xa <= M))" |
|
14516 | 1972 |
by (import lim CONT_ATTAINS_ALL) |
1973 |
||
17694 | 1974 |
lemma DIFF_LINC: "ALL (f::real => real) (x::real) l::real. |
1975 |
diffl f l x & 0 < l --> |
|
1976 |
(EX d>0. ALL h::real. 0 < h & h < d --> f x < f (x + h))" |
|
14516 | 1977 |
by (import lim DIFF_LINC) |
1978 |
||
17694 | 1979 |
lemma DIFF_LDEC: "ALL (f::real => real) (x::real) l::real. |
1980 |
diffl f l x & l < 0 --> |
|
1981 |
(EX d>0. ALL h::real. 0 < h & h < d --> f x < f (x - h))" |
|
14516 | 1982 |
by (import lim DIFF_LDEC) |
1983 |
||
17694 | 1984 |
lemma DIFF_LMAX: "ALL (f::real => real) (x::real) l::real. |
1985 |
diffl f l x & (EX d>0. ALL y::real. abs (x - y) < d --> f y <= f x) --> |
|
1986 |
l = 0" |
|
14516 | 1987 |
by (import lim DIFF_LMAX) |
1988 |
||
17694 | 1989 |
lemma DIFF_LMIN: "ALL (f::real => real) (x::real) l::real. |
1990 |
diffl f l x & (EX d>0. ALL y::real. abs (x - y) < d --> f x <= f y) --> |
|
1991 |
l = 0" |
|
14516 | 1992 |
by (import lim DIFF_LMIN) |
1993 |
||
17694 | 1994 |
lemma DIFF_LCONST: "ALL (f::real => real) (x::real) l::real. |
1995 |
diffl f l x & (EX d>0. ALL y::real. abs (x - y) < d --> f y = f x) --> |
|
1996 |
l = 0" |
|
14516 | 1997 |
by (import lim DIFF_LCONST) |
1998 |
||
17694 | 1999 |
lemma INTERVAL_LEMMA: "ALL (a::real) (b::real) x::real. |
2000 |
a < x & x < b --> |
|
2001 |
(EX d>0. ALL y::real. abs (x - y) < d --> a <= y & y <= b)" |
|
14516 | 2002 |
by (import lim INTERVAL_LEMMA) |
2003 |
||
17694 | 2004 |
lemma ROLLE: "ALL (f::real => real) (a::real) b::real. |
2005 |
a < b & |
|
2006 |
f a = f b & |
|
2007 |
(ALL x::real. a <= x & x <= b --> contl f x) & |
|
2008 |
(ALL x::real. a < x & x < b --> differentiable f x) --> |
|
2009 |
(EX z::real. a < z & z < b & diffl f 0 z)" |
|
14516 | 2010 |
by (import lim ROLLE) |
2011 |
||
2012 |
lemma MVT_LEMMA: "ALL (f::real => real) (a::real) b::real. |
|
2013 |
f a - (f b - f a) / (b - a) * a = f b - (f b - f a) / (b - a) * b" |
|
2014 |
by (import lim MVT_LEMMA) |
|
2015 |
||
17694 | 2016 |
lemma MVT: "ALL (f::real => real) (a::real) b::real. |
2017 |
a < b & |
|
2018 |
(ALL x::real. a <= x & x <= b --> contl f x) & |
|
2019 |
(ALL x::real. a < x & x < b --> differentiable f x) --> |
|
2020 |
(EX (l::real) z::real. |
|
2021 |
a < z & z < b & diffl f l z & f b - f a = (b - a) * l)" |
|
14516 | 2022 |
by (import lim MVT) |
2023 |
||
17694 | 2024 |
lemma DIFF_ISCONST_END: "ALL (f::real => real) (a::real) b::real. |
2025 |
a < b & |
|
2026 |
(ALL x::real. a <= x & x <= b --> contl f x) & |
|
2027 |
(ALL x::real. a < x & x < b --> diffl f 0 x) --> |
|
2028 |
f b = f a" |
|
14516 | 2029 |
by (import lim DIFF_ISCONST_END) |
2030 |
||
17694 | 2031 |
lemma DIFF_ISCONST: "ALL (f::real => real) (a::real) b::real. |
2032 |
a < b & |
|
2033 |
(ALL x::real. a <= x & x <= b --> contl f x) & |
|
2034 |
(ALL x::real. a < x & x < b --> diffl f 0 x) --> |
|
2035 |
(ALL x::real. a <= x & x <= b --> f x = f a)" |
|
14516 | 2036 |
by (import lim DIFF_ISCONST) |
2037 |
||
17694 | 2038 |
lemma DIFF_ISCONST_ALL: "ALL f::real => real. All (diffl f 0) --> (ALL (x::real) y::real. f x = f y)" |
14516 | 2039 |
by (import lim DIFF_ISCONST_ALL) |
2040 |
||
2041 |
lemma INTERVAL_ABS: "ALL (x::real) (z::real) d::real. |
|
2042 |
(x - d <= z & z <= x + d) = (abs (z - x) <= d)" |
|
2043 |
by (import lim INTERVAL_ABS) |
|
2044 |
||
17694 | 2045 |
lemma CONT_INJ_LEMMA: "ALL (f::real => real) (g::real => real) (x::real) d::real. |
2046 |
0 < d & |
|
2047 |
(ALL z::real. abs (z - x) <= d --> g (f z) = z) & |
|
2048 |
(ALL z::real. abs (z - x) <= d --> contl f z) --> |
|
2049 |
~ (ALL z::real. abs (z - x) <= d --> f z <= f x)" |
|
14516 | 2050 |
by (import lim CONT_INJ_LEMMA) |
2051 |
||
17694 | 2052 |
lemma CONT_INJ_LEMMA2: "ALL (f::real => real) (g::real => real) (x::real) d::real. |
2053 |
0 < d & |
|
2054 |
(ALL z::real. abs (z - x) <= d --> g (f z) = z) & |
|
2055 |
(ALL z::real. abs (z - x) <= d --> contl f z) --> |
|
2056 |
~ (ALL z::real. abs (z - x) <= d --> f x <= f z)" |
|
14516 | 2057 |
by (import lim CONT_INJ_LEMMA2) |
2058 |
||
17694 | 2059 |
lemma CONT_INJ_RANGE: "ALL (f::real => real) (g::real => real) (x::real) d::real. |
2060 |
0 < d & |
|
2061 |
(ALL z::real. abs (z - x) <= d --> g (f z) = z) & |
|
2062 |
(ALL z::real. abs (z - x) <= d --> contl f z) --> |
|
2063 |
(EX e>0. |
|
2064 |
ALL y::real. |
|
2065 |
abs (y - f x) <= e --> (EX z::real. abs (z - x) <= d & f z = y))" |
|
14516 | 2066 |
by (import lim CONT_INJ_RANGE) |
2067 |
||
17694 | 2068 |
lemma CONT_INVERSE: "ALL (f::real => real) (g::real => real) (x::real) d::real. |
2069 |
0 < d & |
|
2070 |
(ALL z::real. abs (z - x) <= d --> g (f z) = z) & |
|
2071 |
(ALL z::real. abs (z - x) <= d --> contl f z) --> |
|
2072 |
contl g (f x)" |
|
14516 | 2073 |
by (import lim CONT_INVERSE) |
2074 |
||
17694 | 2075 |
lemma DIFF_INVERSE: "ALL (f::real => real) (g::real => real) (l::real) (x::real) d::real. |
2076 |
0 < d & |
|
2077 |
(ALL z::real. abs (z - x) <= d --> g (f z) = z) & |
|
2078 |
(ALL z::real. abs (z - x) <= d --> contl f z) & diffl f l x & l ~= 0 --> |
|
2079 |
diffl g (inverse l) (f x)" |
|
14516 | 2080 |
by (import lim DIFF_INVERSE) |
2081 |
||
17694 | 2082 |
lemma DIFF_INVERSE_LT: "ALL (f::real => real) (g::real => real) (l::real) (x::real) d::real. |
2083 |
0 < d & |
|
2084 |
(ALL z::real. abs (z - x) < d --> g (f z) = z) & |
|
2085 |
(ALL z::real. abs (z - x) < d --> contl f z) & diffl f l x & l ~= 0 --> |
|
2086 |
diffl g (inverse l) (f x)" |
|
14516 | 2087 |
by (import lim DIFF_INVERSE_LT) |
2088 |
||
17694 | 2089 |
lemma INTERVAL_CLEMMA: "ALL (a::real) (b::real) x::real. |
2090 |
a < x & x < b --> |
|
2091 |
(EX d>0. ALL y::real. abs (y - x) <= d --> a < y & y < b)" |
|
14516 | 2092 |
by (import lim INTERVAL_CLEMMA) |
2093 |
||
17694 | 2094 |
lemma DIFF_INVERSE_OPEN: "ALL (f::real => real) (g::real => real) (l::real) (a::real) (x::real) |
2095 |
b::real. |
|
2096 |
a < x & |
|
2097 |
x < b & |
|
2098 |
(ALL z::real. a < z & z < b --> g (f z) = z & contl f z) & |
|
2099 |
diffl f l x & l ~= 0 --> |
|
2100 |
diffl g (inverse l) (f x)" |
|
14516 | 2101 |
by (import lim DIFF_INVERSE_OPEN) |
2102 |
||
2103 |
;end_setup |
|
2104 |
||
2105 |
;setup_theory powser |
|
2106 |
||
17644 | 2107 |
lemma POWDIFF_LEMMA: "ALL (n::nat) (x::real) y::real. |
17652 | 2108 |
real.sum (0, Suc n) (%p::nat. x ^ p * y ^ (Suc n - p)) = |
2109 |
y * real.sum (0, Suc n) (%p::nat. x ^ p * y ^ (n - p))" |
|
14516 | 2110 |
by (import powser POWDIFF_LEMMA) |
2111 |
||
17644 | 2112 |
lemma POWDIFF: "ALL (n::nat) (x::real) y::real. |
14516 | 2113 |
x ^ Suc n - y ^ Suc n = |
17652 | 2114 |
(x - y) * real.sum (0, Suc n) (%p::nat. x ^ p * y ^ (n - p))" |
14516 | 2115 |
by (import powser POWDIFF) |
2116 |
||
17644 | 2117 |
lemma POWREV: "ALL (n::nat) (x::real) y::real. |
17652 | 2118 |
real.sum (0, Suc n) (%xa::nat. x ^ xa * y ^ (n - xa)) = |
2119 |
real.sum (0, Suc n) (%xa::nat. x ^ (n - xa) * y ^ xa)" |
|
14516 | 2120 |
by (import powser POWREV) |
2121 |
||
17694 | 2122 |
lemma POWSER_INSIDEA: "ALL (f::nat => real) (x::real) z::real. |
2123 |
summable (%n::nat. f n * x ^ n) & abs z < abs x --> |
|
2124 |
summable (%n::nat. abs (f n) * z ^ n)" |
|
14516 | 2125 |
by (import powser POWSER_INSIDEA) |
2126 |
||
17694 | 2127 |
lemma POWSER_INSIDE: "ALL (f::nat => real) (x::real) z::real. |
2128 |
summable (%n::nat. f n * x ^ n) & abs z < abs x --> |
|
2129 |
summable (%n::nat. f n * z ^ n)" |
|
14516 | 2130 |
by (import powser POWSER_INSIDE) |
2131 |
||
2132 |
constdefs |
|
2133 |
diffs :: "(nat => real) => nat => real" |
|
17644 | 2134 |
"diffs == %(c::nat => real) n::nat. real (Suc n) * c (Suc n)" |
2135 |
||
2136 |
lemma diffs: "ALL c::nat => real. diffs c = (%n::nat. real (Suc n) * c (Suc n))" |
|
14516 | 2137 |
by (import powser diffs) |
2138 |
||
17644 | 2139 |
lemma DIFFS_NEG: "ALL c::nat => real. diffs (%n::nat. - c n) = (%x::nat. - diffs c x)" |
14516 | 2140 |
by (import powser DIFFS_NEG) |
2141 |
||
17644 | 2142 |
lemma DIFFS_LEMMA: "ALL (n::nat) (c::nat => real) x::real. |
17652 | 2143 |
real.sum (0, n) (%n::nat. diffs c n * x ^ n) = |
2144 |
real.sum (0, n) (%n::nat. real n * (c n * x ^ (n - 1))) + |
|
2145 |
real n * (c n * x ^ (n - 1))" |
|
14516 | 2146 |
by (import powser DIFFS_LEMMA) |
2147 |
||
17644 | 2148 |
lemma DIFFS_LEMMA2: "ALL (n::nat) (c::nat => real) x::real. |
17652 | 2149 |
real.sum (0, n) (%n::nat. real n * (c n * x ^ (n - 1))) = |
2150 |
real.sum (0, n) (%n::nat. diffs c n * x ^ n) - |
|
2151 |
real n * (c n * x ^ (n - 1))" |
|
14516 | 2152 |
by (import powser DIFFS_LEMMA2) |
2153 |
||
17694 | 2154 |
lemma DIFFS_EQUIV: "ALL (c::nat => real) x::real. |
2155 |
summable (%n::nat. diffs c n * x ^ n) --> |
|
2156 |
sums (%n::nat. real n * (c n * x ^ (n - 1))) |
|
2157 |
(suminf (%n::nat. diffs c n * x ^ n))" |
|
14516 | 2158 |
by (import powser DIFFS_EQUIV) |
2159 |
||
17644 | 2160 |
lemma TERMDIFF_LEMMA1: "ALL (m::nat) (z::real) h::real. |
17652 | 2161 |
real.sum (0, m) (%p::nat. (z + h) ^ (m - p) * z ^ p - z ^ m) = |
2162 |
real.sum (0, m) (%p::nat. z ^ p * ((z + h) ^ (m - p) - z ^ (m - p)))" |
|
14516 | 2163 |
by (import powser TERMDIFF_LEMMA1) |
2164 |
||
17694 | 2165 |
lemma TERMDIFF_LEMMA2: "ALL (z::real) (h::real) n::nat. |
2166 |
h ~= 0 --> |
|
2167 |
((z + h) ^ n - z ^ n) / h - real n * z ^ (n - 1) = |
|
2168 |
h * |
|
2169 |
real.sum (0, n - 1) |
|
2170 |
(%p::nat. |
|
2171 |
z ^ p * |
|
2172 |
real.sum (0, n - 1 - p) |
|
2173 |
(%q::nat. (z + h) ^ q * z ^ (n - 2 - p - q)))" |
|
14516 | 2174 |
by (import powser TERMDIFF_LEMMA2) |
2175 |
||
17694 | 2176 |
lemma TERMDIFF_LEMMA3: "ALL (z::real) (h::real) (n::nat) k'::real. |
2177 |
h ~= 0 & abs z <= k' & abs (z + h) <= k' --> |
|
2178 |
abs (((z + h) ^ n - z ^ n) / h - real n * z ^ (n - 1)) |
|
2179 |
<= real n * (real (n - 1) * (k' ^ (n - 2) * abs h))" |
|
14516 | 2180 |
by (import powser TERMDIFF_LEMMA3) |
2181 |
||
17694 | 2182 |
lemma TERMDIFF_LEMMA4: "ALL (f::real => real) (k'::real) k::real. |
2183 |
0 < k & |
|
2184 |
(ALL h::real. 0 < abs h & abs h < k --> abs (f h) <= k' * abs h) --> |
|
2185 |
tends_real_real f 0 0" |
|
14516 | 2186 |
by (import powser TERMDIFF_LEMMA4) |
2187 |
||
17694 | 2188 |
lemma TERMDIFF_LEMMA5: "ALL (f::nat => real) (g::real => nat => real) k::real. |
2189 |
0 < k & |
|
2190 |
summable f & |
|
2191 |
(ALL h::real. |
|
2192 |
0 < abs h & abs h < k --> |
|
2193 |
(ALL n::nat. abs (g h n) <= f n * abs h)) --> |
|
2194 |
tends_real_real (%h::real. suminf (g h)) 0 0" |
|
14516 | 2195 |
by (import powser TERMDIFF_LEMMA5) |
2196 |
||
17694 | 2197 |
lemma TERMDIFF: "ALL (c::nat => real) (k'::real) x::real. |
2198 |
summable (%n::nat. c n * k' ^ n) & |
|
2199 |
summable (%n::nat. diffs c n * k' ^ n) & |
|
2200 |
summable (%n::nat. diffs (diffs c) n * k' ^ n) & abs x < abs k' --> |
|
2201 |
diffl (%x::real. suminf (%n::nat. c n * x ^ n)) |
|
2202 |
(suminf (%n::nat. diffs c n * x ^ n)) x" |
|
14516 | 2203 |
by (import powser TERMDIFF) |
2204 |
||
2205 |
;end_setup |
|
2206 |
||
2207 |
;setup_theory transc |
|
2208 |
||
2209 |
constdefs |
|
2210 |
exp :: "real => real" |
|
17644 | 2211 |
"exp == %x::real. suminf (%n::nat. inverse (real (FACT n)) * x ^ n)" |
2212 |
||
2213 |
lemma exp: "ALL x::real. exp x = suminf (%n::nat. inverse (real (FACT n)) * x ^ n)" |
|
14516 | 2214 |
by (import transc exp) |
2215 |
||
2216 |
constdefs |
|
2217 |
cos :: "real => real" |
|
17652 | 2218 |
"cos == |
2219 |
%x::real. |
|
2220 |
suminf |
|
2221 |
(%n::nat. |
|
2222 |
(if EVEN n then (- 1) ^ (n div 2) / real (FACT n) else 0) * x ^ n)" |
|
2223 |
||
2224 |
lemma cos: "ALL x::real. |
|
2225 |
cos x = |
|
2226 |
suminf |
|
2227 |
(%n::nat. |
|
2228 |
(if EVEN n then (- 1) ^ (n div 2) / real (FACT n) else 0) * x ^ n)" |
|
14516 | 2229 |
by (import transc cos) |
2230 |
||
2231 |
constdefs |
|
2232 |
sin :: "real => real" |
|
2233 |
"sin == |
|
17644 | 2234 |
%x::real. |
2235 |
suminf |
|
2236 |
(%n::nat. |
|
17652 | 2237 |
(if EVEN n then 0 else (- 1) ^ ((n - 1) div 2) / real (FACT n)) * |
17644 | 2238 |
x ^ n)" |
2239 |
||
2240 |
lemma sin: "ALL x::real. |
|
14516 | 2241 |
sin x = |
2242 |
suminf |
|
17644 | 2243 |
(%n::nat. |
17652 | 2244 |
(if EVEN n then 0 else (- 1) ^ ((n - 1) div 2) / real (FACT n)) * |
17644 | 2245 |
x ^ n)" |
14516 | 2246 |
by (import transc sin) |
2247 |
||
17644 | 2248 |
lemma EXP_CONVERGES: "ALL x::real. sums (%n::nat. inverse (real (FACT n)) * x ^ n) (exp x)" |
14516 | 2249 |
by (import transc EXP_CONVERGES) |
2250 |
||
17644 | 2251 |
lemma SIN_CONVERGES: "ALL x::real. |
14516 | 2252 |
sums |
17644 | 2253 |
(%n::nat. |
17652 | 2254 |
(if EVEN n then 0 else (- 1) ^ ((n - 1) div 2) / real (FACT n)) * |
17644 | 2255 |
x ^ n) |
14516 | 2256 |
(sin x)" |
2257 |
by (import transc SIN_CONVERGES) |
|
2258 |
||
17652 | 2259 |
lemma COS_CONVERGES: "ALL x::real. |
2260 |
sums |
|
2261 |
(%n::nat. |
|
2262 |
(if EVEN n then (- 1) ^ (n div 2) / real (FACT n) else 0) * x ^ n) |
|
2263 |
(cos x)" |
|
14516 | 2264 |
by (import transc COS_CONVERGES) |
2265 |
||
17644 | 2266 |
lemma EXP_FDIFF: "diffs (%n::nat. inverse (real (FACT n))) = |
2267 |
(%n::nat. inverse (real (FACT n)))" |
|
14516 | 2268 |
by (import transc EXP_FDIFF) |
2269 |
||
17652 | 2270 |
lemma SIN_FDIFF: "diffs |
2271 |
(%n::nat. if EVEN n then 0 else (- 1) ^ ((n - 1) div 2) / real (FACT n)) = |
|
2272 |
(%n::nat. if EVEN n then (- 1) ^ (n div 2) / real (FACT n) else 0)" |
|
14516 | 2273 |
by (import transc SIN_FDIFF) |
2274 |
||
17652 | 2275 |
lemma COS_FDIFF: "diffs (%n::nat. if EVEN n then (- 1) ^ (n div 2) / real (FACT n) else 0) = |
2276 |
(%n::nat. - (if EVEN n then 0 else (- 1) ^ ((n - 1) div 2) / real (FACT n)))" |
|
14516 | 2277 |
by (import transc COS_FDIFF) |
2278 |
||
17644 | 2279 |
lemma SIN_NEGLEMMA: "ALL x::real. |
14516 | 2280 |
- sin x = |
2281 |
suminf |
|
17644 | 2282 |
(%n::nat. |
17652 | 2283 |
- ((if EVEN n then 0 else (- 1) ^ ((n - 1) div 2) / real (FACT n)) * |
17644 | 2284 |
x ^ n))" |
14516 | 2285 |
by (import transc SIN_NEGLEMMA) |
2286 |
||
17644 | 2287 |
lemma DIFF_EXP: "ALL x::real. diffl exp (exp x) x" |
14516 | 2288 |
by (import transc DIFF_EXP) |
2289 |
||
17644 | 2290 |
lemma DIFF_SIN: "ALL x::real. diffl sin (cos x) x" |
14516 | 2291 |
by (import transc DIFF_SIN) |
2292 |
||
17644 | 2293 |
lemma DIFF_COS: "ALL x::real. diffl cos (- sin x) x" |
14516 | 2294 |
by (import transc DIFF_COS) |
2295 |
||
17694 | 2296 |
lemma DIFF_COMPOSITE: "(diffl (f::real => real) (l::real) (x::real) & f x ~= 0 --> |
2297 |
diffl (%x::real. inverse (f x)) (- (l / f x ^ 2)) x) & |
|
2298 |
(diffl f l x & diffl (g::real => real) (m::real) x & g x ~= 0 --> |
|
2299 |
diffl (%x::real. f x / g x) ((l * g x - m * f x) / g x ^ 2) x) & |
|
2300 |
(diffl f l x & diffl g m x --> diffl (%x::real. f x + g x) (l + m) x) & |
|
2301 |
(diffl f l x & diffl g m x --> |
|
2302 |
diffl (%x::real. f x * g x) (l * g x + m * f x) x) & |
|
2303 |
(diffl f l x & diffl g m x --> diffl (%x::real. f x - g x) (l - m) x) & |
|
2304 |
(diffl f l x --> diffl (%x::real. - f x) (- l) x) & |
|
2305 |
(diffl g m x --> |
|
2306 |
diffl (%x::real. g x ^ (n::nat)) (real n * g x ^ (n - 1) * m) x) & |
|
2307 |
(diffl g m x --> diffl (%x::real. exp (g x)) (exp (g x) * m) x) & |
|
2308 |
(diffl g m x --> diffl (%x::real. sin (g x)) (cos (g x) * m) x) & |
|
2309 |
(diffl g m x --> diffl (%x::real. cos (g x)) (- sin (g x) * m) x)" |
|
14516 | 2310 |
by (import transc DIFF_COMPOSITE) |
2311 |
||
17652 | 2312 |
lemma EXP_0: "exp 0 = 1" |
14516 | 2313 |
by (import transc EXP_0) |
2314 |
||
17652 | 2315 |
lemma EXP_LE_X: "ALL x>=0. 1 + x <= exp x" |
14516 | 2316 |
by (import transc EXP_LE_X) |
2317 |
||
17652 | 2318 |
lemma EXP_LT_1: "ALL x>0. 1 < exp x" |
14516 | 2319 |
by (import transc EXP_LT_1) |
2320 |
||
17644 | 2321 |
lemma EXP_ADD_MUL: "ALL (x::real) y::real. exp (x + y) * exp (- x) = exp y" |
14516 | 2322 |
by (import transc EXP_ADD_MUL) |
2323 |
||
17652 | 2324 |
lemma EXP_NEG_MUL: "ALL x::real. exp x * exp (- x) = 1" |
14516 | 2325 |
by (import transc EXP_NEG_MUL) |
2326 |
||
17652 | 2327 |
lemma EXP_NEG_MUL2: "ALL x::real. exp (- x) * exp x = 1" |
14516 | 2328 |
by (import transc EXP_NEG_MUL2) |
2329 |
||
17644 | 2330 |
lemma EXP_NEG: "ALL x::real. exp (- x) = inverse (exp x)" |
14516 | 2331 |
by (import transc EXP_NEG) |
2332 |
||
17644 | 2333 |
lemma EXP_ADD: "ALL (x::real) y::real. exp (x + y) = exp x * exp y" |
14516 | 2334 |
by (import transc EXP_ADD) |
2335 |
||
17652 | 2336 |
lemma EXP_POS_LE: "ALL x::real. 0 <= exp x" |
14516 | 2337 |
by (import transc EXP_POS_LE) |
2338 |
||
17652 | 2339 |
lemma EXP_NZ: "ALL x::real. exp x ~= 0" |
14516 | 2340 |
by (import transc EXP_NZ) |
2341 |
||
17652 | 2342 |
lemma EXP_POS_LT: "ALL x::real. 0 < exp x" |
14516 | 2343 |
by (import transc EXP_POS_LT) |
2344 |
||
17644 | 2345 |
lemma EXP_N: "ALL (n::nat) x::real. exp (real n * x) = exp x ^ n" |
14516 | 2346 |
by (import transc EXP_N) |
2347 |
||
17644 | 2348 |
lemma EXP_SUB: "ALL (x::real) y::real. exp (x - y) = exp x / exp y" |
14516 | 2349 |
by (import transc EXP_SUB) |
2350 |
||
17694 | 2351 |
lemma EXP_MONO_IMP: "ALL (x::real) y::real. x < y --> exp x < exp y" |
14516 | 2352 |
by (import transc EXP_MONO_IMP) |
2353 |
||
17644 | 2354 |
lemma EXP_MONO_LT: "ALL (x::real) y::real. (exp x < exp y) = (x < y)" |
14516 | 2355 |
by (import transc EXP_MONO_LT) |
2356 |
||
17644 | 2357 |
lemma EXP_MONO_LE: "ALL (x::real) y::real. (exp x <= exp y) = (x <= y)" |
14516 | 2358 |
by (import transc EXP_MONO_LE) |
2359 |
||
17644 | 2360 |
lemma EXP_INJ: "ALL (x::real) y::real. (exp x = exp y) = (x = y)" |
14516 | 2361 |
by (import transc EXP_INJ) |
2362 |
||
17652 | 2363 |
lemma EXP_TOTAL_LEMMA: "ALL y>=1. EX x>=0. x <= y - 1 & exp x = y" |
14516 | 2364 |
by (import transc EXP_TOTAL_LEMMA) |
2365 |
||
17652 | 2366 |
lemma EXP_TOTAL: "ALL y>0. EX x::real. exp x = y" |
14516 | 2367 |
by (import transc EXP_TOTAL) |
2368 |
||
2369 |
constdefs |
|
2370 |
ln :: "real => real" |
|
17644 | 2371 |
"ln == %x::real. SOME u::real. exp u = x" |
2372 |
||
2373 |
lemma ln: "ALL x::real. ln x = (SOME u::real. exp u = x)" |
|
14516 | 2374 |
by (import transc ln) |
2375 |
||
17644 | 2376 |
lemma LN_EXP: "ALL x::real. ln (exp x) = x" |
14516 | 2377 |
by (import transc LN_EXP) |
2378 |
||
17652 | 2379 |
lemma EXP_LN: "ALL x::real. (exp (ln x) = x) = (0 < x)" |
14516 | 2380 |
by (import transc EXP_LN) |
2381 |
||
17694 | 2382 |
lemma LN_MUL: "ALL (x::real) y::real. 0 < x & 0 < y --> ln (x * y) = ln x + ln y" |
14516 | 2383 |
by (import transc LN_MUL) |
2384 |
||
17694 | 2385 |
lemma LN_INJ: "ALL (x::real) y::real. 0 < x & 0 < y --> (ln x = ln y) = (x = y)" |
14516 | 2386 |
by (import transc LN_INJ) |
2387 |
||
17652 | 2388 |
lemma LN_1: "ln 1 = 0" |
14516 | 2389 |
by (import transc LN_1) |
2390 |
||
17652 | 2391 |
lemma LN_INV: "ALL x>0. ln (inverse x) = - ln x" |
14516 | 2392 |
by (import transc LN_INV) |
2393 |
||
17694 | 2394 |
lemma LN_DIV: "ALL (x::real) y::real. 0 < x & 0 < y --> ln (x / y) = ln x - ln y" |
14516 | 2395 |
by (import transc LN_DIV) |
2396 |
||
17694 | 2397 |
lemma LN_MONO_LT: "ALL (x::real) y::real. 0 < x & 0 < y --> (ln x < ln y) = (x < y)" |
14516 | 2398 |
by (import transc LN_MONO_LT) |
2399 |
||
17694 | 2400 |
lemma LN_MONO_LE: "ALL (x::real) y::real. 0 < x & 0 < y --> (ln x <= ln y) = (x <= y)" |
14516 | 2401 |
by (import transc LN_MONO_LE) |
2402 |
||
17694 | 2403 |
lemma LN_POW: "ALL (n::nat) x::real. 0 < x --> ln (x ^ n) = real n * ln x" |
14516 | 2404 |
by (import transc LN_POW) |
2405 |
||
17652 | 2406 |
lemma LN_LE: "ALL x>=0. ln (1 + x) <= x" |
14516 | 2407 |
by (import transc LN_LE) |
2408 |
||
17652 | 2409 |
lemma LN_LT_X: "ALL x>0. ln x < x" |
14516 | 2410 |
by (import transc LN_LT_X) |
2411 |
||
17652 | 2412 |
lemma LN_POS: "ALL x>=1. 0 <= ln x" |
14516 | 2413 |
by (import transc LN_POS) |
2414 |
||
2415 |
constdefs |
|
2416 |
root :: "nat => real => real" |
|
17694 | 2417 |
"root == %(n::nat) x::real. SOME u::real. (0 < x --> 0 < u) & u ^ n = x" |
2418 |
||
2419 |
lemma root: "ALL (n::nat) x::real. |
|
2420 |
root n x = (SOME u::real. (0 < x --> 0 < u) & u ^ n = x)" |
|
14516 | 2421 |
by (import transc root) |
2422 |
||
2423 |
constdefs |
|
2424 |
sqrt :: "real => real" |
|
17652 | 2425 |
"sqrt == root 2" |
2426 |
||
2427 |
lemma sqrt: "ALL x::real. sqrt x = root 2 x" |
|
14516 | 2428 |
by (import transc sqrt) |
2429 |
||
17694 | 2430 |
lemma ROOT_LT_LEMMA: "ALL (n::nat) x::real. 0 < x --> exp (ln x / real (Suc n)) ^ Suc n = x" |
14516 | 2431 |
by (import transc ROOT_LT_LEMMA) |
2432 |
||
17694 | 2433 |
lemma ROOT_LN: "ALL (n::nat) x::real. 0 < x --> root (Suc n) x = exp (ln x / real (Suc n))" |
14516 | 2434 |
by (import transc ROOT_LN) |
2435 |
||
17652 | 2436 |
lemma ROOT_0: "ALL n::nat. root (Suc n) 0 = 0" |
14516 | 2437 |
by (import transc ROOT_0) |
2438 |
||
17652 | 2439 |
lemma ROOT_1: "ALL n::nat. root (Suc n) 1 = 1" |
14516 | 2440 |
by (import transc ROOT_1) |
2441 |
||
17694 | 2442 |
lemma ROOT_POS_LT: "ALL (n::nat) x::real. 0 < x --> 0 < root (Suc n) x" |
14516 | 2443 |
by (import transc ROOT_POS_LT) |
2444 |
||
17694 | 2445 |
lemma ROOT_POW_POS: "ALL (n::nat) x::real. 0 <= x --> root (Suc n) x ^ Suc n = x" |
14516 | 2446 |
by (import transc ROOT_POW_POS) |
2447 |
||
17694 | 2448 |
lemma POW_ROOT_POS: "ALL (n::nat) x::real. 0 <= x --> root (Suc n) (x ^ Suc n) = x" |
14516 | 2449 |
by (import transc POW_ROOT_POS) |
2450 |
||
17694 | 2451 |
lemma ROOT_POS: "ALL (n::nat) x::real. 0 <= x --> 0 <= root (Suc n) x" |
14516 | 2452 |
by (import transc ROOT_POS) |
2453 |
||
17694 | 2454 |
lemma ROOT_POS_UNIQ: "ALL (n::nat) (x::real) y::real. |
2455 |
0 <= x & 0 <= y & y ^ Suc n = x --> root (Suc n) x = y" |
|
14516 | 2456 |
by (import transc ROOT_POS_UNIQ) |
2457 |
||
17694 | 2458 |
lemma ROOT_MUL: "ALL (n::nat) (x::real) y::real. |
2459 |
0 <= x & 0 <= y --> |
|
2460 |
root (Suc n) (x * y) = root (Suc n) x * root (Suc n) y" |
|
14516 | 2461 |
by (import transc ROOT_MUL) |
2462 |
||
17694 | 2463 |
lemma ROOT_INV: "ALL (n::nat) x::real. |
2464 |
0 <= x --> root (Suc n) (inverse x) = inverse (root (Suc n) x)" |
|
14516 | 2465 |
by (import transc ROOT_INV) |
2466 |
||
17694 | 2467 |
lemma ROOT_DIV: "ALL (x::nat) (xa::real) xb::real. |
2468 |
0 <= xa & 0 <= xb --> |
|
2469 |
root (Suc x) (xa / xb) = root (Suc x) xa / root (Suc x) xb" |
|
14516 | 2470 |
by (import transc ROOT_DIV) |
2471 |
||
17694 | 2472 |
lemma ROOT_MONO_LE: "ALL (x::real) y::real. |
2473 |
0 <= x & x <= y --> root (Suc (n::nat)) x <= root (Suc n) y" |
|
14516 | 2474 |
by (import transc ROOT_MONO_LE) |
2475 |
||
17652 | 2476 |
lemma SQRT_0: "sqrt 0 = 0" |
14516 | 2477 |
by (import transc SQRT_0) |
2478 |
||
17652 | 2479 |
lemma SQRT_1: "sqrt 1 = 1" |
14516 | 2480 |
by (import transc SQRT_1) |
2481 |
||
17652 | 2482 |
lemma SQRT_POS_LT: "ALL x>0. 0 < sqrt x" |
14516 | 2483 |
by (import transc SQRT_POS_LT) |
2484 |
||
17652 | 2485 |
lemma SQRT_POS_LE: "ALL x>=0. 0 <= sqrt x" |
14516 | 2486 |
by (import transc SQRT_POS_LE) |
2487 |
||
17652 | 2488 |
lemma SQRT_POW2: "ALL x::real. (sqrt x ^ 2 = x) = (0 <= x)" |
14516 | 2489 |
by (import transc SQRT_POW2) |
2490 |
||
17652 | 2491 |
lemma SQRT_POW_2: "ALL x>=0. sqrt x ^ 2 = x" |
14516 | 2492 |
by (import transc SQRT_POW_2) |
2493 |
||
17694 | 2494 |
lemma POW_2_SQRT: "0 <= (x::real) --> sqrt (x ^ 2) = x" |
14516 | 2495 |
by (import transc POW_2_SQRT) |
2496 |
||
17694 | 2497 |
lemma SQRT_POS_UNIQ: "ALL (x::real) xa::real. 0 <= x & 0 <= xa & xa ^ 2 = x --> sqrt x = xa" |
14516 | 2498 |
by (import transc SQRT_POS_UNIQ) |
2499 |
||
17694 | 2500 |
lemma SQRT_MUL: "ALL (x::real) xa::real. |
2501 |
0 <= x & 0 <= xa --> sqrt (x * xa) = sqrt x * sqrt xa" |
|
14516 | 2502 |
by (import transc SQRT_MUL) |
2503 |
||
17652 | 2504 |
lemma SQRT_INV: "ALL x>=0. sqrt (inverse x) = inverse (sqrt x)" |
14516 | 2505 |
by (import transc SQRT_INV) |
2506 |
||
17694 | 2507 |
lemma SQRT_DIV: "ALL (x::real) xa::real. |
2508 |
0 <= x & 0 <= xa --> sqrt (x / xa) = sqrt x / sqrt xa" |
|
14516 | 2509 |
by (import transc SQRT_DIV) |
2510 |
||
17694 | 2511 |
lemma SQRT_MONO_LE: "ALL (x::real) xa::real. 0 <= x & x <= xa --> sqrt x <= sqrt xa" |
14516 | 2512 |
by (import transc SQRT_MONO_LE) |
2513 |
||
17694 | 2514 |
lemma SQRT_EVEN_POW2: "ALL n::nat. EVEN n --> sqrt (2 ^ n) = 2 ^ (n div 2)" |
14516 | 2515 |
by (import transc SQRT_EVEN_POW2) |
2516 |
||
17652 | 2517 |
lemma REAL_DIV_SQRT: "ALL x>=0. x / sqrt x = sqrt x" |
14516 | 2518 |
by (import transc REAL_DIV_SQRT) |
2519 |
||
17694 | 2520 |
lemma SQRT_EQ: "ALL (x::real) y::real. x ^ 2 = y & 0 <= x --> x = sqrt y" |
14516 | 2521 |
by (import transc SQRT_EQ) |
2522 |
||
17652 | 2523 |
lemma SIN_0: "sin 0 = 0" |
14516 | 2524 |
by (import transc SIN_0) |
2525 |
||
17652 | 2526 |
lemma COS_0: "cos 0 = 1" |
14516 | 2527 |
by (import transc COS_0) |
2528 |
||
17652 | 2529 |
lemma SIN_CIRCLE: "ALL x::real. sin x ^ 2 + cos x ^ 2 = 1" |
14516 | 2530 |
by (import transc SIN_CIRCLE) |
2531 |
||
17652 | 2532 |
lemma SIN_BOUND: "ALL x::real. abs (sin x) <= 1" |
14516 | 2533 |
by (import transc SIN_BOUND) |
2534 |
||
17652 | 2535 |
lemma SIN_BOUNDS: "ALL x::real. - 1 <= sin x & sin x <= 1" |
14516 | 2536 |
by (import transc SIN_BOUNDS) |
2537 |
||
17652 | 2538 |
lemma COS_BOUND: "ALL x::real. abs (cos x) <= 1" |
14516 | 2539 |
by (import transc COS_BOUND) |
2540 |
||
17652 | 2541 |
lemma COS_BOUNDS: "ALL x::real. - 1 <= cos x & cos x <= 1" |
14516 | 2542 |
by (import transc COS_BOUNDS) |
2543 |
||
17644 | 2544 |
lemma SIN_COS_ADD: "ALL (x::real) y::real. |
14516 | 2545 |
(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 + |
2546 |
(cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2 = |
|
17652 | 2547 |
0" |
14516 | 2548 |
by (import transc SIN_COS_ADD) |
2549 |
||
17652 | 2550 |
lemma SIN_COS_NEG: "ALL x::real. (sin (- x) + sin x) ^ 2 + (cos (- x) - cos x) ^ 2 = 0" |
14516 | 2551 |
by (import transc SIN_COS_NEG) |
2552 |
||
17644 | 2553 |
lemma SIN_ADD: "ALL (x::real) y::real. sin (x + y) = sin x * cos y + cos x * sin y" |
14516 | 2554 |
by (import transc SIN_ADD) |
2555 |
||
17644 | 2556 |
lemma COS_ADD: "ALL (x::real) y::real. cos (x + y) = cos x * cos y - sin x * sin y" |
14516 | 2557 |
by (import transc COS_ADD) |
2558 |
||
17644 | 2559 |
lemma SIN_NEG: "ALL x::real. sin (- x) = - sin x" |
14516 | 2560 |
by (import transc SIN_NEG) |
2561 |
||
17644 | 2562 |
lemma COS_NEG: "ALL x::real. cos (- x) = cos x" |
14516 | 2563 |
by (import transc COS_NEG) |
2564 |
||
17652 | 2565 |
lemma SIN_DOUBLE: "ALL x::real. sin (2 * x) = 2 * (sin x * cos x)" |
14516 | 2566 |
by (import transc SIN_DOUBLE) |
2567 |
||
17652 | 2568 |
lemma COS_DOUBLE: "ALL x::real. cos (2 * x) = cos x ^ 2 - sin x ^ 2" |
14516 | 2569 |
by (import transc COS_DOUBLE) |
2570 |
||
17644 | 2571 |
lemma SIN_PAIRED: "ALL x::real. |
17652 | 2572 |
sums (%n::nat. (- 1) ^ n / real (FACT (2 * n + 1)) * x ^ (2 * n + 1)) |
17644 | 2573 |
(sin x)" |
14516 | 2574 |
by (import transc SIN_PAIRED) |
2575 |
||
17694 | 2576 |
lemma SIN_POS: "ALL x::real. 0 < x & x < 2 --> 0 < sin x" |
14516 | 2577 |
by (import transc SIN_POS) |
2578 |
||
17644 | 2579 |
lemma COS_PAIRED: "ALL x::real. |
17652 | 2580 |
sums (%n::nat. (- 1) ^ n / real (FACT (2 * n)) * x ^ (2 * n)) (cos x)" |
14516 | 2581 |
by (import transc COS_PAIRED) |
2582 |
||
17652 | 2583 |
lemma COS_2: "cos 2 < 0" |
14516 | 2584 |
by (import transc COS_2) |
2585 |
||
17652 | 2586 |
lemma COS_ISZERO: "EX! x::real. 0 <= x & x <= 2 & cos x = 0" |
14516 | 2587 |
by (import transc COS_ISZERO) |
2588 |
||
2589 |
constdefs |
|
2590 |
pi :: "real" |
|
17652 | 2591 |
"pi == 2 * (SOME x::real. 0 <= x & x <= 2 & cos x = 0)" |
2592 |
||
2593 |
lemma pi: "pi = 2 * (SOME x::real. 0 <= x & x <= 2 & cos x = 0)" |
|
14516 | 2594 |
by (import transc pi) |
2595 |
||
17652 | 2596 |
lemma PI2: "pi / 2 = (SOME x::real. 0 <= x & x <= 2 & cos x = 0)" |
14516 | 2597 |
by (import transc PI2) |
2598 |
||
17652 | 2599 |
lemma COS_PI2: "cos (pi / 2) = 0" |
14516 | 2600 |
by (import transc COS_PI2) |
2601 |
||
17652 | 2602 |
lemma PI2_BOUNDS: "0 < pi / 2 & pi / 2 < 2" |
14516 | 2603 |
by (import transc PI2_BOUNDS) |
2604 |
||
17652 | 2605 |
lemma PI_POS: "0 < pi" |
14516 | 2606 |
by (import transc PI_POS) |
2607 |
||
17652 | 2608 |
lemma SIN_PI2: "sin (pi / 2) = 1" |
14516 | 2609 |
by (import transc SIN_PI2) |
2610 |
||
17652 | 2611 |
lemma COS_PI: "cos pi = - 1" |
14516 | 2612 |
by (import transc COS_PI) |
2613 |
||
17652 | 2614 |
lemma SIN_PI: "sin pi = 0" |
14516 | 2615 |
by (import transc SIN_PI) |
2616 |
||
17652 | 2617 |
lemma SIN_COS: "ALL x::real. sin x = cos (pi / 2 - x)" |
14516 | 2618 |
by (import transc SIN_COS) |
2619 |
||
17652 | 2620 |
lemma COS_SIN: "ALL x::real. cos x = sin (pi / 2 - x)" |
14516 | 2621 |
by (import transc COS_SIN) |
2622 |
||
17644 | 2623 |
lemma SIN_PERIODIC_PI: "ALL x::real. sin (x + pi) = - sin x" |
14516 | 2624 |
by (import transc SIN_PERIODIC_PI) |
2625 |
||
17644 | 2626 |
lemma COS_PERIODIC_PI: "ALL x::real. cos (x + pi) = - cos x" |
14516 | 2627 |
by (import transc COS_PERIODIC_PI) |
2628 |
||
17652 | 2629 |
lemma SIN_PERIODIC: "ALL x::real. sin (x + 2 * pi) = sin x" |
14516 | 2630 |
by (import transc SIN_PERIODIC) |
2631 |
||
17652 | 2632 |
lemma COS_PERIODIC: "ALL x::real. cos (x + 2 * pi) = cos x" |
14516 | 2633 |
by (import transc COS_PERIODIC) |
2634 |
||
17652 | 2635 |
lemma COS_NPI: "ALL n::nat. cos (real n * pi) = (- 1) ^ n" |
14516 | 2636 |
by (import transc COS_NPI) |
2637 |
||
17652 | 2638 |
lemma SIN_NPI: "ALL n::nat. sin (real n * pi) = 0" |
14516 | 2639 |
by (import transc SIN_NPI) |
2640 |
||
17694 | 2641 |
lemma SIN_POS_PI2: "ALL x::real. 0 < x & x < pi / 2 --> 0 < sin x" |
14516 | 2642 |
by (import transc SIN_POS_PI2) |
2643 |
||
17694 | 2644 |
lemma COS_POS_PI2: "ALL x::real. 0 < x & x < pi / 2 --> 0 < cos x" |
14516 | 2645 |
by (import transc COS_POS_PI2) |
2646 |
||
17694 | 2647 |
lemma COS_POS_PI: "ALL x::real. - (pi / 2) < x & x < pi / 2 --> 0 < cos x" |
14516 | 2648 |
by (import transc COS_POS_PI) |
2649 |
||
17694 | 2650 |
lemma SIN_POS_PI: "ALL x::real. 0 < x & x < pi --> 0 < sin x" |
14516 | 2651 |
by (import transc SIN_POS_PI) |
2652 |
||
17694 | 2653 |
lemma COS_POS_PI2_LE: "ALL x::real. 0 <= x & x <= pi / 2 --> 0 <= cos x" |
14516 | 2654 |
by (import transc COS_POS_PI2_LE) |
2655 |
||
17694 | 2656 |
lemma COS_POS_PI_LE: "ALL x::real. - (pi / 2) <= x & x <= pi / 2 --> 0 <= cos x" |
14516 | 2657 |
by (import transc COS_POS_PI_LE) |
2658 |
||
17694 | 2659 |
lemma SIN_POS_PI2_LE: "ALL x::real. 0 <= x & x <= pi / 2 --> 0 <= sin x" |
14516 | 2660 |
by (import transc SIN_POS_PI2_LE) |
2661 |
||
17694 | 2662 |
lemma SIN_POS_PI_LE: "ALL x::real. 0 <= x & x <= pi --> 0 <= sin x" |
14516 | 2663 |
by (import transc SIN_POS_PI_LE) |
2664 |
||
17694 | 2665 |
lemma COS_TOTAL: "ALL y::real. |
2666 |
- 1 <= y & y <= 1 --> (EX! x::real. 0 <= x & x <= pi & cos x = y)" |
|
14516 | 2667 |
by (import transc COS_TOTAL) |
2668 |
||
17694 | 2669 |
lemma SIN_TOTAL: "ALL y::real. |
2670 |
- 1 <= y & y <= 1 --> |
|
2671 |
(EX! x::real. - (pi / 2) <= x & x <= pi / 2 & sin x = y)" |
|
14516 | 2672 |
by (import transc SIN_TOTAL) |
2673 |
||
17694 | 2674 |
lemma COS_ZERO_LEMMA: "ALL x::real. |
2675 |
0 <= x & cos x = 0 --> (EX n::nat. ~ EVEN n & x = real n * (pi / 2))" |
|
14516 | 2676 |
by (import transc COS_ZERO_LEMMA) |
2677 |
||
17694 | 2678 |
lemma SIN_ZERO_LEMMA: "ALL x::real. |
2679 |
0 <= x & sin x = 0 --> (EX n::nat. EVEN n & x = real n * (pi / 2))" |
|
14516 | 2680 |
by (import transc SIN_ZERO_LEMMA) |
2681 |
||
17644 | 2682 |
lemma COS_ZERO: "ALL x::real. |
17652 | 2683 |
(cos x = 0) = |
2684 |
((EX n::nat. ~ EVEN n & x = real n * (pi / 2)) | |
|
2685 |
(EX n::nat. ~ EVEN n & x = - (real n * (pi / 2))))" |
|
14516 | 2686 |
by (import transc COS_ZERO) |
2687 |
||
17644 | 2688 |
lemma SIN_ZERO: "ALL x::real. |
17652 | 2689 |
(sin x = 0) = |
2690 |
((EX n::nat. EVEN n & x = real n * (pi / 2)) | |
|
2691 |
(EX n::nat. EVEN n & x = - (real n * (pi / 2))))" |
|
14516 | 2692 |
by (import transc SIN_ZERO) |
2693 |
||
2694 |
constdefs |
|
2695 |
tan :: "real => real" |
|
17644 | 2696 |
"tan == %x::real. sin x / cos x" |
2697 |
||
2698 |
lemma tan: "ALL x::real. tan x = sin x / cos x" |
|
14516 | 2699 |
by (import transc tan) |
2700 |
||
17652 | 2701 |
lemma TAN_0: "tan 0 = 0" |
14516 | 2702 |
by (import transc TAN_0) |
2703 |
||
17652 | 2704 |
lemma TAN_PI: "tan pi = 0" |
14516 | 2705 |
by (import transc TAN_PI) |
2706 |
||
17652 | 2707 |
lemma TAN_NPI: "ALL n::nat. tan (real n * pi) = 0" |
14516 | 2708 |
by (import transc TAN_NPI) |
2709 |
||
17644 | 2710 |
lemma TAN_NEG: "ALL x::real. tan (- x) = - tan x" |
14516 | 2711 |
by (import transc TAN_NEG) |
2712 |
||
17652 | 2713 |
lemma TAN_PERIODIC: "ALL x::real. tan (x + 2 * pi) = tan x" |
14516 | 2714 |
by (import transc TAN_PERIODIC) |
2715 |
||
17694 | 2716 |
lemma TAN_ADD: "ALL (x::real) y::real. |
2717 |
cos x ~= 0 & cos y ~= 0 & cos (x + y) ~= 0 --> |
|
2718 |
tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)" |
|
14516 | 2719 |
by (import transc TAN_ADD) |
2720 |
||
17694 | 2721 |
lemma TAN_DOUBLE: "ALL x::real. |
2722 |
cos x ~= 0 & cos (2 * x) ~= 0 --> |
|
2723 |
tan (2 * x) = 2 * tan x / (1 - tan x ^ 2)" |
|
14516 | 2724 |
by (import transc TAN_DOUBLE) |
2725 |
||
17694 | 2726 |
lemma TAN_POS_PI2: "ALL x::real. 0 < x & x < pi / 2 --> 0 < tan x" |
14516 | 2727 |
by (import transc TAN_POS_PI2) |
2728 |
||
17694 | 2729 |
lemma DIFF_TAN: "ALL x::real. cos x ~= 0 --> diffl tan (inverse (cos x ^ 2)) x" |
14516 | 2730 |
by (import transc DIFF_TAN) |
2731 |
||
17652 | 2732 |
lemma TAN_TOTAL_LEMMA: "ALL y>0. EX x>0. x < pi / 2 & y < tan x" |
14516 | 2733 |
by (import transc TAN_TOTAL_LEMMA) |
2734 |
||
17652 | 2735 |
lemma TAN_TOTAL_POS: "ALL y>=0. EX x>=0. x < pi / 2 & tan x = y" |
14516 | 2736 |
by (import transc TAN_TOTAL_POS) |
2737 |
||
17652 | 2738 |
lemma TAN_TOTAL: "ALL y::real. EX! x::real. - (pi / 2) < x & x < pi / 2 & tan x = y" |
14516 | 2739 |
by (import transc TAN_TOTAL) |
2740 |
||
2741 |
constdefs |
|
2742 |
asn :: "real => real" |
|
17652 | 2743 |
"asn == %y::real. SOME x::real. - (pi / 2) <= x & x <= pi / 2 & sin x = y" |
17644 | 2744 |
|
2745 |
lemma asn: "ALL y::real. |
|
17652 | 2746 |
asn y = (SOME x::real. - (pi / 2) <= x & x <= pi / 2 & sin x = y)" |
14516 | 2747 |
by (import transc asn) |
2748 |
||
2749 |
constdefs |
|
2750 |
acs :: "real => real" |
|
17652 | 2751 |
"acs == %y::real. SOME x::real. 0 <= x & x <= pi & cos x = y" |
2752 |
||
2753 |
lemma acs: "ALL y::real. acs y = (SOME x::real. 0 <= x & x <= pi & cos x = y)" |
|
14516 | 2754 |
by (import transc acs) |
2755 |
||
2756 |
constdefs |
|
2757 |
atn :: "real => real" |
|
17652 | 2758 |
"atn == %y::real. SOME x::real. - (pi / 2) < x & x < pi / 2 & tan x = y" |
2759 |
||
2760 |
lemma atn: "ALL y::real. atn y = (SOME x::real. - (pi / 2) < x & x < pi / 2 & tan x = y)" |
|
14516 | 2761 |
by (import transc atn) |
2762 |
||
17694 | 2763 |
lemma ASN: "ALL y::real. |
2764 |
- 1 <= y & y <= 1 --> |
|
2765 |
- (pi / 2) <= asn y & asn y <= pi / 2 & sin (asn y) = y" |
|
14516 | 2766 |
by (import transc ASN) |
2767 |
||
17694 | 2768 |
lemma ASN_SIN: "ALL y::real. - 1 <= y & y <= 1 --> sin (asn y) = y" |
14516 | 2769 |
by (import transc ASN_SIN) |
2770 |
||
17694 | 2771 |
lemma ASN_BOUNDS: "ALL y::real. - 1 <= y & y <= 1 --> - (pi / 2) <= asn y & asn y <= pi / 2" |
14516 | 2772 |
by (import transc ASN_BOUNDS) |
2773 |
||
17694 | 2774 |
lemma ASN_BOUNDS_LT: "ALL y::real. - 1 < y & y < 1 --> - (pi / 2) < asn y & asn y < pi / 2" |
14516 | 2775 |
by (import transc ASN_BOUNDS_LT) |
2776 |
||
17694 | 2777 |
lemma SIN_ASN: "ALL x::real. - (pi / 2) <= x & x <= pi / 2 --> asn (sin x) = x" |
14516 | 2778 |
by (import transc SIN_ASN) |
2779 |
||
17694 | 2780 |
lemma ACS: "ALL y::real. |
2781 |
- 1 <= y & y <= 1 --> 0 <= acs y & acs y <= pi & cos (acs y) = y" |
|
14516 | 2782 |
by (import transc ACS) |
2783 |
||
17694 | 2784 |
lemma ACS_COS: "ALL y::real. - 1 <= y & y <= 1 --> cos (acs y) = y" |
14516 | 2785 |
by (import transc ACS_COS) |
2786 |
||
17694 | 2787 |
lemma ACS_BOUNDS: "ALL y::real. - 1 <= y & y <= 1 --> 0 <= acs y & acs y <= pi" |
14516 | 2788 |
by (import transc ACS_BOUNDS) |
2789 |
||
17694 | 2790 |
lemma ACS_BOUNDS_LT: "ALL y::real. - 1 < y & y < 1 --> 0 < acs y & acs y < pi" |
14516 | 2791 |
by (import transc ACS_BOUNDS_LT) |
2792 |
||
17694 | 2793 |
lemma COS_ACS: "ALL x::real. 0 <= x & x <= pi --> acs (cos x) = x" |
14516 | 2794 |
by (import transc COS_ACS) |
2795 |
||
17652 | 2796 |
lemma ATN: "ALL y::real. - (pi / 2) < atn y & atn y < pi / 2 & tan (atn y) = y" |
14516 | 2797 |
by (import transc ATN) |
2798 |
||
17644 | 2799 |
lemma ATN_TAN: "ALL x::real. tan (atn x) = x" |
14516 | 2800 |
by (import transc ATN_TAN) |
2801 |
||
17652 | 2802 |
lemma ATN_BOUNDS: "ALL x::real. - (pi / 2) < atn x & atn x < pi / 2" |
14516 | 2803 |
by (import transc ATN_BOUNDS) |
2804 |
||
17694 | 2805 |
lemma TAN_ATN: "ALL x::real. - (pi / 2) < x & x < pi / 2 --> atn (tan x) = x" |
14516 | 2806 |
by (import transc TAN_ATN) |
2807 |
||
17694 | 2808 |
lemma TAN_SEC: "ALL x::real. cos x ~= 0 --> 1 + tan x ^ 2 = inverse (cos x) ^ 2" |
14516 | 2809 |
by (import transc TAN_SEC) |
2810 |
||
17694 | 2811 |
lemma SIN_COS_SQ: "ALL x::real. 0 <= x & x <= pi --> sin x = sqrt (1 - cos x ^ 2)" |
14516 | 2812 |
by (import transc SIN_COS_SQ) |
2813 |
||
17694 | 2814 |
lemma COS_SIN_SQ: "ALL x::real. - (pi / 2) <= x & x <= pi / 2 --> cos x = sqrt (1 - sin x ^ 2)" |
14516 | 2815 |
by (import transc COS_SIN_SQ) |
2816 |
||
17652 | 2817 |
lemma COS_ATN_NZ: "ALL x::real. cos (atn x) ~= 0" |
14516 | 2818 |
by (import transc COS_ATN_NZ) |
2819 |
||
17694 | 2820 |
lemma COS_ASN_NZ: "ALL x::real. - 1 < x & x < 1 --> cos (asn x) ~= 0" |
14516 | 2821 |
by (import transc COS_ASN_NZ) |
2822 |
||
17694 | 2823 |
lemma SIN_ACS_NZ: "ALL x::real. - 1 < x & x < 1 --> sin (acs x) ~= 0" |
14516 | 2824 |
by (import transc SIN_ACS_NZ) |
2825 |
||
17694 | 2826 |
lemma COS_SIN_SQRT: "ALL x::real. 0 <= cos x --> cos x = sqrt (1 - sin x ^ 2)" |
14516 | 2827 |
by (import transc COS_SIN_SQRT) |
2828 |
||
17694 | 2829 |
lemma SIN_COS_SQRT: "ALL x::real. 0 <= sin x --> sin x = sqrt (1 - cos x ^ 2)" |
14516 | 2830 |
by (import transc SIN_COS_SQRT) |
2831 |
||
17652 | 2832 |
lemma DIFF_LN: "ALL x>0. diffl ln (inverse x) x" |
14516 | 2833 |
by (import transc DIFF_LN) |
2834 |
||
17694 | 2835 |
lemma DIFF_ASN_LEMMA: "ALL x::real. - 1 < x & x < 1 --> diffl asn (inverse (cos (asn x))) x" |
14516 | 2836 |
by (import transc DIFF_ASN_LEMMA) |
2837 |
||
17694 | 2838 |
lemma DIFF_ASN: "ALL x::real. - 1 < x & x < 1 --> diffl asn (inverse (sqrt (1 - x ^ 2))) x" |
14516 | 2839 |
by (import transc DIFF_ASN) |
2840 |
||
17694 | 2841 |
lemma DIFF_ACS_LEMMA: "ALL x::real. - 1 < x & x < 1 --> diffl acs (inverse (- sin (acs x))) x" |
14516 | 2842 |
by (import transc DIFF_ACS_LEMMA) |
2843 |
||
17694 | 2844 |
lemma DIFF_ACS: "ALL x::real. - 1 < x & x < 1 --> diffl acs (- inverse (sqrt (1 - x ^ 2))) x" |
14516 | 2845 |
by (import transc DIFF_ACS) |
2846 |
||
17652 | 2847 |
lemma DIFF_ATN: "ALL x::real. diffl atn (inverse (1 + x ^ 2)) x" |
14516 | 2848 |
by (import transc DIFF_ATN) |
2849 |
||
2850 |
constdefs |
|
2851 |
division :: "real * real => (nat => real) => bool" |
|
2852 |
"(op ==::(real * real => (nat => real) => bool) |
|
2853 |
=> (real * real => (nat => real) => bool) => prop) |
|
2854 |
(division::real * real => (nat => real) => bool) |
|
2855 |
((split::(real => real => (nat => real) => bool) |
|
2856 |
=> real * real => (nat => real) => bool) |
|
2857 |
(%(a::real) (b::real) D::nat => real. |
|
2858 |
(op &::bool => bool => bool) |
|
2859 |
((op =::real => real => bool) (D (0::nat)) a) |
|
2860 |
((Ex::(nat => bool) => bool) |
|
2861 |
(%N::nat. |
|
2862 |
(op &::bool => bool => bool) |
|
2863 |
((All::(nat => bool) => bool) |
|
2864 |
(%n::nat. |
|
2865 |
(op -->::bool => bool => bool) |
|
2866 |
((op <::nat => nat => bool) n N) |
|
2867 |
((op <::real => real => bool) (D n) |
|
2868 |
(D ((Suc::nat => nat) n))))) |
|
2869 |
((All::(nat => bool) => bool) |
|
2870 |
(%n::nat. |
|
2871 |
(op -->::bool => bool => bool) |
|
2872 |
((op <=::nat => nat => bool) N n) |
|
2873 |
((op =::real => real => bool) (D n) b)))))))" |
|
2874 |
||
2875 |
lemma division: "(All::(real => bool) => bool) |
|
2876 |
(%a::real. |
|
2877 |
(All::(real => bool) => bool) |
|
2878 |
(%b::real. |
|
2879 |
(All::((nat => real) => bool) => bool) |
|
2880 |
(%D::nat => real. |
|
2881 |
(op =::bool => bool => bool) |
|
2882 |
((division::real * real => (nat => real) => bool) |
|
2883 |
((Pair::real => real => real * real) a b) D) |
|
2884 |
((op &::bool => bool => bool) |
|
2885 |
((op =::real => real => bool) (D (0::nat)) a) |
|
2886 |
((Ex::(nat => bool) => bool) |
|
2887 |
(%N::nat. |
|
2888 |
(op &::bool => bool => bool) |
|
2889 |
((All::(nat => bool) => bool) |
|
2890 |
(%n::nat. |
|
2891 |
(op -->::bool => bool => bool) |
|
2892 |
((op <::nat => nat => bool) n N) |
|
2893 |
((op <::real => real => bool) (D n) |
|
2894 |
(D ((Suc::nat => nat) n))))) |
|
2895 |
((All::(nat => bool) => bool) |
|
2896 |
(%n::nat. |
|
2897 |
(op -->::bool => bool => bool) |
|
2898 |
((op <=::nat => nat => bool) N n) |
|
2899 |
((op =::real => real => bool) (D n) |
|
2900 |
b)))))))))" |
|
2901 |
by (import transc division) |
|
2902 |
||
2903 |
constdefs |
|
2904 |
dsize :: "(nat => real) => nat" |
|
2905 |
"(op ==::((nat => real) => nat) => ((nat => real) => nat) => prop) |
|
2906 |
(dsize::(nat => real) => nat) |
|
2907 |
(%D::nat => real. |
|
2908 |
(Eps::(nat => bool) => nat) |
|
2909 |
(%N::nat. |
|
2910 |
(op &::bool => bool => bool) |
|
2911 |
((All::(nat => bool) => bool) |
|
2912 |
(%n::nat. |
|
2913 |
(op -->::bool => bool => bool) |
|
2914 |
((op <::nat => nat => bool) n N) |
|
2915 |
((op <::real => real => bool) (D n) |
|
2916 |
(D ((Suc::nat => nat) n))))) |
|
2917 |
((All::(nat => bool) => bool) |
|
2918 |
(%n::nat. |
|
2919 |
(op -->::bool => bool => bool) |
|
2920 |
((op <=::nat => nat => bool) N n) |
|
2921 |
((op =::real => real => bool) (D n) (D N))))))" |
|
2922 |
||
2923 |
lemma dsize: "(All::((nat => real) => bool) => bool) |
|
2924 |
(%D::nat => real. |
|
2925 |
(op =::nat => nat => bool) ((dsize::(nat => real) => nat) D) |
|
2926 |
((Eps::(nat => bool) => nat) |
|
2927 |
(%N::nat. |
|
2928 |
(op &::bool => bool => bool) |
|
2929 |
((All::(nat => bool) => bool) |
|
2930 |
(%n::nat. |
|
2931 |
(op -->::bool => bool => bool) |
|
2932 |
((op <::nat => nat => bool) n N) |
|
2933 |
((op <::real => real => bool) (D n) |
|
2934 |
(D ((Suc::nat => nat) n))))) |
|
2935 |
((All::(nat => bool) => bool) |
|
2936 |
(%n::nat. |
|
2937 |
(op -->::bool => bool => bool) |
|
2938 |
((op <=::nat => nat => bool) N n) |
|
2939 |
((op =::real => real => bool) (D n) (D N)))))))" |
|
2940 |
by (import transc dsize) |
|
2941 |
||
2942 |
constdefs |
|
2943 |
tdiv :: "real * real => (nat => real) * (nat => real) => bool" |
|
2944 |
"tdiv == |
|
17644 | 2945 |
%(a::real, b::real) (D::nat => real, p::nat => real). |
2946 |
division (a, b) D & (ALL n::nat. D n <= p n & p n <= D (Suc n))" |
|
2947 |
||
2948 |
lemma tdiv: "ALL (a::real) (b::real) (D::nat => real) p::nat => real. |
|
14516 | 2949 |
tdiv (a, b) (D, p) = |
17644 | 2950 |
(division (a, b) D & (ALL n::nat. D n <= p n & p n <= D (Suc n)))" |
14516 | 2951 |
by (import transc tdiv) |
2952 |
||
2953 |
constdefs |
|
2954 |
gauge :: "(real => bool) => (real => real) => bool" |
|
17694 | 2955 |
"gauge == %(E::real => bool) g::real => real. ALL x::real. E x --> 0 < g x" |
2956 |
||
2957 |
lemma gauge: "ALL (E::real => bool) g::real => real. |
|
2958 |
gauge E g = (ALL x::real. E x --> 0 < g x)" |
|
14516 | 2959 |
by (import transc gauge) |
2960 |
||
2961 |
constdefs |
|
2962 |
fine :: "(real => real) => (nat => real) * (nat => real) => bool" |
|
14847 | 2963 |
"(op ==::((real => real) => (nat => real) * (nat => real) => bool) |
2964 |
=> ((real => real) => (nat => real) * (nat => real) => bool) |
|
2965 |
=> prop) |
|
2966 |
(fine::(real => real) => (nat => real) * (nat => real) => bool) |
|
2967 |
(%g::real => real. |
|
2968 |
(split::((nat => real) => (nat => real) => bool) |
|
2969 |
=> (nat => real) * (nat => real) => bool) |
|
2970 |
(%(D::nat => real) p::nat => real. |
|
2971 |
(All::(nat => bool) => bool) |
|
2972 |
(%n::nat. |
|
2973 |
(op -->::bool => bool => bool) |
|
2974 |
((op <::nat => nat => bool) n |
|
2975 |
((dsize::(nat => real) => nat) D)) |
|
2976 |
((op <::real => real => bool) |
|
2977 |
((op -::real => real => real) (D ((Suc::nat => nat) n)) |
|
2978 |
(D n)) |
|
2979 |
(g (p n))))))" |
|
2980 |
||
2981 |
lemma fine: "(All::((real => real) => bool) => bool) |
|
2982 |
(%g::real => real. |
|
2983 |
(All::((nat => real) => bool) => bool) |
|
2984 |
(%D::nat => real. |
|
2985 |
(All::((nat => real) => bool) => bool) |
|
2986 |
(%p::nat => real. |
|
2987 |
(op =::bool => bool => bool) |
|
2988 |
((fine::(real => real) |
|
2989 |
=> (nat => real) * (nat => real) => bool) |
|
2990 |
g ((Pair::(nat => real) |
|
2991 |
=> (nat => real) |
|
2992 |
=> (nat => real) * (nat => real)) |
|
2993 |
D p)) |
|
2994 |
((All::(nat => bool) => bool) |
|
2995 |
(%n::nat. |
|
2996 |
(op -->::bool => bool => bool) |
|
2997 |
((op <::nat => nat => bool) n |
|
2998 |
((dsize::(nat => real) => nat) D)) |
|
2999 |
((op <::real => real => bool) |
|
3000 |
((op -::real => real => real) |
|
3001 |
(D ((Suc::nat => nat) n)) (D n)) |
|
3002 |
(g (p n))))))))" |
|
14516 | 3003 |
by (import transc fine) |
3004 |
||
3005 |
constdefs |
|
3006 |
rsum :: "(nat => real) * (nat => real) => (real => real) => real" |
|
17644 | 3007 |
"rsum == |
3008 |
%(D::nat => real, p::nat => real) f::real => real. |
|
17652 | 3009 |
real.sum (0, dsize D) (%n::nat. f (p n) * (D (Suc n) - D n))" |
17644 | 3010 |
|
3011 |
lemma rsum: "ALL (D::nat => real) (p::nat => real) f::real => real. |
|
3012 |
rsum (D, p) f = |
|
17652 | 3013 |
real.sum (0, dsize D) (%n::nat. f (p n) * (D (Suc n) - D n))" |
14516 | 3014 |
by (import transc rsum) |
3015 |
||
3016 |
constdefs |
|
3017 |
Dint :: "real * real => (real => real) => real => bool" |
|
17694 | 3018 |
"Dint == |
3019 |
%(a::real, b::real) (f::real => real) k::real. |
|
3020 |
ALL e>0. |
|
3021 |
EX g::real => real. |
|
3022 |
gauge (%x::real. a <= x & x <= b) g & |
|
3023 |
(ALL (D::nat => real) p::nat => real. |
|
3024 |
tdiv (a, b) (D, p) & fine g (D, p) --> |
|
3025 |
abs (rsum (D, p) f - k) < e)" |
|
3026 |
||
3027 |
lemma Dint: "ALL (a::real) (b::real) (f::real => real) k::real. |
|
3028 |
Dint (a, b) f k = |
|
3029 |
(ALL e>0. |
|
3030 |
EX g::real => real. |
|
3031 |
gauge (%x::real. a <= x & x <= b) g & |
|
3032 |
(ALL (D::nat => real) p::nat => real. |
|
3033 |
tdiv (a, b) (D, p) & fine g (D, p) --> |
|
3034 |
abs (rsum (D, p) f - k) < e))" |
|
14516 | 3035 |
by (import transc Dint) |
3036 |
||
17694 | 3037 |
lemma DIVISION_0: "ALL (a::real) b::real. a = b --> dsize (%n::nat. if n = 0 then a else b) = 0" |
14516 | 3038 |
by (import transc DIVISION_0) |
3039 |
||
17694 | 3040 |
lemma DIVISION_1: "ALL (a::real) b::real. a < b --> dsize (%n::nat. if n = 0 then a else b) = 1" |
14516 | 3041 |
by (import transc DIVISION_1) |
3042 |
||
17694 | 3043 |
lemma DIVISION_SINGLE: "ALL (a::real) b::real. |
3044 |
a <= b --> division (a, b) (%n::nat. if n = 0 then a else b)" |
|
14516 | 3045 |
by (import transc DIVISION_SINGLE) |
3046 |
||
17694 | 3047 |
lemma DIVISION_LHS: "ALL (D::nat => real) (a::real) b::real. division (a, b) D --> D 0 = a" |
14516 | 3048 |
by (import transc DIVISION_LHS) |
3049 |
||
3050 |
lemma DIVISION_THM: "(All::((nat => real) => bool) => bool) |
|
3051 |
(%D::nat => real. |
|
3052 |
(All::(real => bool) => bool) |
|
3053 |
(%a::real. |
|
3054 |
(All::(real => bool) => bool) |
|
3055 |
(%b::real. |
|
3056 |
(op =::bool => bool => bool) |
|
3057 |
((division::real * real => (nat => real) => bool) |
|
3058 |
((Pair::real => real => real * real) a b) D) |
|
3059 |
((op &::bool => bool => bool) |
|
3060 |
((op =::real => real => bool) (D (0::nat)) a) |
|
3061 |
((op &::bool => bool => bool) |
|
3062 |
((All::(nat => bool) => bool) |
|
3063 |
(%n::nat. |
|
3064 |
(op -->::bool => bool => bool) |
|
3065 |
((op <::nat => nat => bool) n |
|
3066 |
((dsize::(nat => real) => nat) D)) |
|
3067 |
((op <::real => real => bool) (D n) |
|
3068 |
(D ((Suc::nat => nat) n))))) |
|
3069 |
((All::(nat => bool) => bool) |
|
3070 |
(%n::nat. |
|
3071 |
(op -->::bool => bool => bool) |
|
3072 |
((op <=::nat => nat => bool) |
|
3073 |
((dsize::(nat => real) => nat) D) n) |
|
3074 |
((op =::real => real => bool) (D n) b))))))))" |
|
3075 |
by (import transc DIVISION_THM) |
|
3076 |
||
17694 | 3077 |
lemma DIVISION_RHS: "ALL (D::nat => real) (a::real) b::real. |
3078 |
division (a, b) D --> D (dsize D) = b" |
|
14516 | 3079 |
by (import transc DIVISION_RHS) |
3080 |
||
17694 | 3081 |
lemma DIVISION_LT_GEN: "ALL (D::nat => real) (a::real) (b::real) (m::nat) n::nat. |
3082 |
division (a, b) D & m < n & n <= dsize D --> D m < D n" |
|
14516 | 3083 |
by (import transc DIVISION_LT_GEN) |
3084 |
||
3085 |
lemma DIVISION_LT: "(All::((nat => real) => bool) => bool) |
|
3086 |
(%D::nat => real. |
|
3087 |
(All::(real => bool) => bool) |
|
3088 |
(%a::real. |
|
3089 |
(All::(real => bool) => bool) |
|
3090 |
(%b::real. |
|
3091 |
(op -->::bool => bool => bool) |
|
3092 |
((division::real * real => (nat => real) => bool) |
|
3093 |
((Pair::real => real => real * real) a b) D) |
|
3094 |
((All::(nat => bool) => bool) |
|
3095 |
(%n::nat. |
|
3096 |
(op -->::bool => bool => bool) |
|
3097 |
((op <::nat => nat => bool) n |
|
3098 |
((dsize::(nat => real) => nat) D)) |
|
3099 |
((op <::real => real => bool) (D (0::nat)) |
|
3100 |
(D ((Suc::nat => nat) n))))))))" |
|
3101 |
by (import transc DIVISION_LT) |
|
3102 |
||
17694 | 3103 |
lemma DIVISION_LE: "ALL (D::nat => real) (a::real) b::real. division (a, b) D --> a <= b" |
14516 | 3104 |
by (import transc DIVISION_LE) |
3105 |
||
3106 |
lemma DIVISION_GT: "(All::((nat => real) => bool) => bool) |
|
3107 |
(%D::nat => real. |
|
3108 |
(All::(real => bool) => bool) |
|
3109 |
(%a::real. |
|
3110 |
(All::(real => bool) => bool) |
|
3111 |
(%b::real. |
|
3112 |
(op -->::bool => bool => bool) |
|
3113 |
((division::real * real => (nat => real) => bool) |
|
3114 |
((Pair::real => real => real * real) a b) D) |
|
3115 |
((All::(nat => bool) => bool) |
|
3116 |
(%n::nat. |
|
3117 |
(op -->::bool => bool => bool) |
|
3118 |
((op <::nat => nat => bool) n |
|
3119 |
((dsize::(nat => real) => nat) D)) |
|
3120 |
((op <::real => real => bool) (D n) |
|
3121 |
(D ((dsize::(nat => real) => nat) D))))))))" |
|
3122 |
by (import transc DIVISION_GT) |
|
3123 |
||
17694 | 3124 |
lemma DIVISION_EQ: "ALL (D::nat => real) (a::real) b::real. |
3125 |
division (a, b) D --> (a = b) = (dsize D = 0)" |
|
14516 | 3126 |
by (import transc DIVISION_EQ) |
3127 |
||
17694 | 3128 |
lemma DIVISION_LBOUND: "ALL (D::nat => real) (a::real) b::real. |
3129 |
division (a, b) D --> (ALL r::nat. a <= D r)" |
|
14516 | 3130 |
by (import transc DIVISION_LBOUND) |
3131 |
||
17694 | 3132 |
lemma DIVISION_LBOUND_LT: "ALL (D::nat => real) (a::real) b::real. |
3133 |
division (a, b) D & dsize D ~= 0 --> (ALL n::nat. a < D (Suc n))" |
|
14516 | 3134 |
by (import transc DIVISION_LBOUND_LT) |
3135 |
||
17694 | 3136 |
lemma DIVISION_UBOUND: "ALL (D::nat => real) (a::real) b::real. |
3137 |
division (a, b) D --> (ALL r::nat. D r <= b)" |
|
14516 | 3138 |
by (import transc DIVISION_UBOUND) |
3139 |
||
17694 | 3140 |
lemma DIVISION_UBOUND_LT: "ALL (D::nat => real) (a::real) (b::real) n::nat. |
3141 |
division (a, b) D & n < dsize D --> D n < b" |
|
14516 | 3142 |
by (import transc DIVISION_UBOUND_LT) |
3143 |
||
17694 | 3144 |
lemma DIVISION_APPEND: "ALL (a::real) (b::real) c::real. |
3145 |
(EX (D1::nat => real) p1::nat => real. |
|
3146 |
tdiv (a, b) (D1, p1) & fine (g::real => real) (D1, p1)) & |
|
3147 |
(EX (D2::nat => real) p2::nat => real. |
|
3148 |
tdiv (b, c) (D2, p2) & fine g (D2, p2)) --> |
|
3149 |
(EX (x::nat => real) p::nat => real. tdiv (a, c) (x, p) & fine g (x, p))" |
|
14516 | 3150 |
by (import transc DIVISION_APPEND) |
3151 |
||
17694 | 3152 |
lemma DIVISION_EXISTS: "ALL (a::real) (b::real) g::real => real. |
3153 |
a <= b & gauge (%x::real. a <= x & x <= b) g --> |
|
3154 |
(EX (D::nat => real) p::nat => real. tdiv (a, b) (D, p) & fine g (D, p))" |
|
14516 | 3155 |
by (import transc DIVISION_EXISTS) |
3156 |
||
17694 | 3157 |
lemma GAUGE_MIN: "ALL (E::real => bool) (g1::real => real) g2::real => real. |
3158 |
gauge E g1 & gauge E g2 --> |
|
3159 |
gauge E (%x::real. if g1 x < g2 x then g1 x else g2 x)" |
|
14516 | 3160 |
by (import transc GAUGE_MIN) |
3161 |
||
17694 | 3162 |
lemma FINE_MIN: "ALL (g1::real => real) (g2::real => real) (D::nat => real) p::nat => real. |
3163 |
fine (%x::real. if g1 x < g2 x then g1 x else g2 x) (D, p) --> |
|
3164 |
fine g1 (D, p) & fine g2 (D, p)" |
|
14516 | 3165 |
by (import transc FINE_MIN) |
3166 |
||
17694 | 3167 |
lemma DINT_UNIQ: "ALL (a::real) (b::real) (f::real => real) (k1::real) k2::real. |
3168 |
a <= b & Dint (a, b) f k1 & Dint (a, b) f k2 --> k1 = k2" |
|
14516 | 3169 |
by (import transc DINT_UNIQ) |
3170 |
||
17652 | 3171 |
lemma INTEGRAL_NULL: "ALL (f::real => real) a::real. Dint (a, a) f 0" |
14516 | 3172 |
by (import transc INTEGRAL_NULL) |
3173 |
||
17694 | 3174 |
lemma FTC1: "ALL (f::real => real) (f'::real => real) (a::real) b::real. |
3175 |
a <= b & (ALL x::real. a <= x & x <= b --> diffl f (f' x) x) --> |
|
3176 |
Dint (a, b) f' (f b - f a)" |
|
14516 | 3177 |
by (import transc FTC1) |
3178 |
||
17694 | 3179 |
lemma MCLAURIN: "ALL (f::real => real) (diff::nat => real => real) (h::real) n::nat. |
3180 |
0 < h & |
|
3181 |
0 < n & |
|
3182 |
diff 0 = f & |
|
3183 |
(ALL (m::nat) t::real. |
|
3184 |
m < n & 0 <= t & t <= h --> diffl (diff m) (diff (Suc m) t) t) --> |
|
3185 |
(EX t>0. |
|
3186 |
t < h & |
|
3187 |
f h = |
|
3188 |
real.sum (0, n) (%m::nat. diff m 0 / real (FACT m) * h ^ m) + |
|
3189 |
diff n t / real (FACT n) * h ^ n)" |
|
14516 | 3190 |
by (import transc MCLAURIN) |
3191 |
||
17694 | 3192 |
lemma MCLAURIN_NEG: "ALL (f::real => real) (diff::nat => real => real) (h::real) n::nat. |
3193 |
h < 0 & |
|
3194 |
0 < n & |
|
3195 |
diff 0 = f & |
|
3196 |
(ALL (m::nat) t::real. |
|
3197 |
m < n & h <= t & t <= 0 --> diffl (diff m) (diff (Suc m) t) t) --> |
|
3198 |
(EX t::real. |
|
3199 |
h < t & |
|
3200 |
t < 0 & |
|
3201 |
f h = |
|
3202 |
real.sum (0, n) (%m::nat. diff m 0 / real (FACT m) * h ^ m) + |
|
3203 |
diff n t / real (FACT n) * h ^ n)" |
|
14516 | 3204 |
by (import transc MCLAURIN_NEG) |
3205 |
||
17694 | 3206 |
lemma MCLAURIN_ALL_LT: "ALL (f::real => real) diff::nat => real => real. |
3207 |
diff 0 = f & |
|
3208 |
(ALL (m::nat) x::real. diffl (diff m) (diff (Suc m) x) x) --> |
|
3209 |
(ALL (x::real) n::nat. |
|
3210 |
x ~= 0 & 0 < n --> |
|
3211 |
(EX t::real. |
|
3212 |
0 < abs t & |
|
3213 |
abs t < abs x & |
|
3214 |
f x = |
|
3215 |
real.sum (0, n) (%m::nat. diff m 0 / real (FACT m) * x ^ m) + |
|
3216 |
diff n t / real (FACT n) * x ^ n))" |
|
14516 | 3217 |
by (import transc MCLAURIN_ALL_LT) |
3218 |
||
17694 | 3219 |
lemma MCLAURIN_ZERO: "ALL (diff::nat => real => real) (n::nat) x::real. |
3220 |
x = 0 & 0 < n --> |
|
3221 |
real.sum (0, n) (%m::nat. diff m 0 / real (FACT m) * x ^ m) = diff 0 0" |
|
14516 | 3222 |
by (import transc MCLAURIN_ZERO) |
3223 |
||
17694 | 3224 |
lemma MCLAURIN_ALL_LE: "ALL (f::real => real) diff::nat => real => real. |
3225 |
diff 0 = f & |
|
3226 |
(ALL (m::nat) x::real. diffl (diff m) (diff (Suc m) x) x) --> |
|
3227 |
(ALL (x::real) n::nat. |
|
3228 |
EX t::real. |
|
3229 |
abs t <= abs x & |
|
3230 |
f x = |
|
3231 |
real.sum (0, n) (%m::nat. diff m 0 / real (FACT m) * x ^ m) + |
|
3232 |
diff n t / real (FACT n) * x ^ n)" |
|
14516 | 3233 |
by (import transc MCLAURIN_ALL_LE) |
3234 |
||
17694 | 3235 |
lemma MCLAURIN_EXP_LT: "ALL (x::real) n::nat. |
3236 |
x ~= 0 & 0 < n --> |
|
3237 |
(EX xa::real. |
|
3238 |
0 < abs xa & |
|
3239 |
abs xa < abs x & |
|
3240 |
exp x = |
|
3241 |
real.sum (0, n) (%m::nat. x ^ m / real (FACT m)) + |
|
3242 |
exp xa / real (FACT n) * x ^ n)" |
|
14516 | 3243 |
by (import transc MCLAURIN_EXP_LT) |
3244 |
||
17644 | 3245 |
lemma MCLAURIN_EXP_LE: "ALL (x::real) n::nat. |
3246 |
EX xa::real. |
|
14516 | 3247 |
abs xa <= abs x & |
3248 |
exp x = |
|
17652 | 3249 |
real.sum (0, n) (%m::nat. x ^ m / real (FACT m)) + |
14516 | 3250 |
exp xa / real (FACT n) * x ^ n" |
3251 |
by (import transc MCLAURIN_EXP_LE) |
|
3252 |
||
17694 | 3253 |
lemma DIFF_LN_COMPOSITE: "ALL (g::real => real) (m::real) x::real. |
3254 |
diffl g m x & 0 < g x --> |
|
3255 |
diffl (%x::real. ln (g x)) (inverse (g x) * m) x" |
|
14516 | 3256 |
by (import transc DIFF_LN_COMPOSITE) |
3257 |
||
3258 |
;end_setup |
|
3259 |
||
3260 |
;setup_theory poly |
|
3261 |
||
3262 |
consts |
|
3263 |
poly :: "real list => real => real" |
|
3264 |
||
17652 | 3265 |
specification (poly_primdef: poly) poly_def: "(ALL x::real. poly [] x = 0) & |
17644 | 3266 |
(ALL (h::real) (t::real list) x::real. poly (h # t) x = h + x * poly t x)" |
14516 | 3267 |
by (import poly poly_def) |
3268 |
||
3269 |
consts |
|
3270 |
poly_add :: "real list => real list => real list" |
|
3271 |
||
17644 | 3272 |
specification (poly_add_primdef: poly_add) poly_add_def: "(ALL l2::real list. poly_add [] l2 = l2) & |
3273 |
(ALL (h::real) (t::real list) l2::real list. |
|
14516 | 3274 |
poly_add (h # t) l2 = |
3275 |
(if l2 = [] then h # t else (h + hd l2) # poly_add t (tl l2)))" |
|
3276 |
by (import poly poly_add_def) |
|
3277 |
||
3278 |
consts |
|
3279 |
"##" :: "real => real list => real list" ("##") |
|
3280 |
||
17644 | 3281 |
specification ("##") poly_cmul_def: "(ALL c::real. ## c [] = []) & |
3282 |
(ALL (c::real) (h::real) t::real list. ## c (h # t) = c * h # ## c t)" |
|
14516 | 3283 |
by (import poly poly_cmul_def) |
3284 |
||
3285 |
consts |
|
3286 |
poly_neg :: "real list => real list" |
|
3287 |
||
3288 |
defs |
|
17652 | 3289 |
poly_neg_primdef: "poly_neg == ## (- 1)" |
3290 |
||
3291 |
lemma poly_neg_def: "poly_neg = ## (- 1)" |
|
14516 | 3292 |
by (import poly poly_neg_def) |
3293 |
||
3294 |
consts |
|
3295 |
poly_mul :: "real list => real list => real list" |
|
3296 |
||
17644 | 3297 |
specification (poly_mul_primdef: poly_mul) poly_mul_def: "(ALL l2::real list. poly_mul [] l2 = []) & |
3298 |
(ALL (h::real) (t::real list) l2::real list. |
|
14516 | 3299 |
poly_mul (h # t) l2 = |
17652 | 3300 |
(if t = [] then ## h l2 else poly_add (## h l2) (0 # poly_mul t l2)))" |
14516 | 3301 |
by (import poly poly_mul_def) |
3302 |
||
3303 |
consts |
|
3304 |
poly_exp :: "real list => nat => real list" |
|
3305 |
||
17652 | 3306 |
specification (poly_exp_primdef: poly_exp) poly_exp_def: "(ALL p::real list. poly_exp p 0 = [1]) & |
17644 | 3307 |
(ALL (p::real list) n::nat. poly_exp p (Suc n) = poly_mul p (poly_exp p n))" |
14516 | 3308 |
by (import poly poly_exp_def) |
3309 |
||
3310 |
consts |
|
3311 |
poly_diff_aux :: "nat => real list => real list" |
|
3312 |
||
17644 | 3313 |
specification (poly_diff_aux_primdef: poly_diff_aux) poly_diff_aux_def: "(ALL n::nat. poly_diff_aux n [] = []) & |
3314 |
(ALL (n::nat) (h::real) t::real list. |
|
3315 |
poly_diff_aux n (h # t) = real n * h # poly_diff_aux (Suc n) t)" |
|
14516 | 3316 |
by (import poly poly_diff_aux_def) |
3317 |
||
3318 |
constdefs |
|
3319 |
diff :: "real list => real list" |
|
17652 | 3320 |
"diff == %l::real list. if l = [] then [] else poly_diff_aux 1 (tl l)" |
3321 |
||
3322 |
lemma poly_diff_def: "ALL l::real list. diff l = (if l = [] then [] else poly_diff_aux 1 (tl l))" |
|
14516 | 3323 |
by (import poly poly_diff_def) |
3324 |
||
17644 | 3325 |
lemma POLY_ADD_CLAUSES: "poly_add [] (p2::real list) = p2 & |
3326 |
poly_add (p1::real list) [] = p1 & |
|
3327 |
poly_add ((h1::real) # (t1::real list)) ((h2::real) # (t2::real list)) = |
|
3328 |
(h1 + h2) # poly_add t1 t2" |
|
14516 | 3329 |
by (import poly POLY_ADD_CLAUSES) |
3330 |
||
17644 | 3331 |
lemma POLY_CMUL_CLAUSES: "## (c::real) [] = [] & ## c ((h::real) # (t::real list)) = c * h # ## c t" |
14516 | 3332 |
by (import poly POLY_CMUL_CLAUSES) |
3333 |
||
17644 | 3334 |
lemma POLY_NEG_CLAUSES: "poly_neg [] = [] & poly_neg ((h::real) # (t::real list)) = - h # poly_neg t" |
14516 | 3335 |
by (import poly POLY_NEG_CLAUSES) |
3336 |
||
17644 | 3337 |
lemma POLY_MUL_CLAUSES: "poly_mul [] (p2::real list) = [] & |
3338 |
poly_mul [h1::real] p2 = ## h1 p2 & |
|
3339 |
poly_mul (h1 # (k1::real) # (t1::real list)) p2 = |
|
17652 | 3340 |
poly_add (## h1 p2) (0 # poly_mul (k1 # t1) p2)" |
14516 | 3341 |
by (import poly POLY_MUL_CLAUSES) |
3342 |
||
17644 | 3343 |
lemma POLY_DIFF_CLAUSES: "diff [] = [] & |
17652 | 3344 |
diff [c::real] = [] & diff ((h::real) # (t::real list)) = poly_diff_aux 1 t" |
14516 | 3345 |
by (import poly POLY_DIFF_CLAUSES) |
3346 |
||
17644 | 3347 |
lemma POLY_ADD: "ALL (t::real list) (p2::real list) x::real. |
3348 |
poly (poly_add t p2) x = poly t x + poly p2 x" |
|
14516 | 3349 |
by (import poly POLY_ADD) |
3350 |
||
17644 | 3351 |
lemma POLY_CMUL: "ALL (t::real list) (c::real) x::real. poly (## c t) x = c * poly t x" |
14516 | 3352 |
by (import poly POLY_CMUL) |
3353 |
||
17644 | 3354 |
lemma POLY_NEG: "ALL (x::real list) xa::real. poly (poly_neg x) xa = - poly x xa" |
14516 | 3355 |
by (import poly POLY_NEG) |
3356 |
||
17644 | 3357 |
lemma POLY_MUL: "ALL (x::real) (t::real list) p2::real list. |
3358 |
poly (poly_mul t p2) x = poly t x * poly p2 x" |
|
14516 | 3359 |
by (import poly POLY_MUL) |
3360 |
||
17644 | 3361 |
lemma POLY_EXP: "ALL (p::real list) (n::nat) x::real. poly (poly_exp p n) x = poly p x ^ n" |
14516 | 3362 |
by (import poly POLY_EXP) |
3363 |
||
17644 | 3364 |
lemma POLY_DIFF_LEMMA: "ALL (t::real list) (n::nat) x::real. |
3365 |
diffl (%x::real. x ^ Suc n * poly t x) |
|
14516 | 3366 |
(x ^ n * poly (poly_diff_aux (Suc n) t) x) x" |
3367 |
by (import poly POLY_DIFF_LEMMA) |
|
3368 |
||
17644 | 3369 |
lemma POLY_DIFF: "ALL (t::real list) x::real. diffl (poly t) (poly (diff t) x) x" |
14516 | 3370 |
by (import poly POLY_DIFF) |
3371 |
||
17644 | 3372 |
lemma POLY_DIFFERENTIABLE: "ALL l::real list. All (differentiable (poly l))" |
14516 | 3373 |
by (import poly POLY_DIFFERENTIABLE) |
3374 |
||
17644 | 3375 |
lemma POLY_CONT: "ALL l::real list. All (contl (poly l))" |
14516 | 3376 |
by (import poly POLY_CONT) |
3377 |
||
17694 | 3378 |
lemma POLY_IVT_POS: "ALL (x::real list) (xa::real) xb::real. |
3379 |
xa < xb & poly x xa < 0 & 0 < poly x xb --> |
|
3380 |
(EX xc::real. xa < xc & xc < xb & poly x xc = 0)" |
|
14516 | 3381 |
by (import poly POLY_IVT_POS) |
3382 |
||
17694 | 3383 |
lemma POLY_IVT_NEG: "ALL (p::real list) (a::real) b::real. |
3384 |
a < b & 0 < poly p a & poly p b < 0 --> |
|
3385 |
(EX x::real. a < x & x < b & poly p x = 0)" |
|
14516 | 3386 |
by (import poly POLY_IVT_NEG) |
3387 |
||
17694 | 3388 |
lemma POLY_MVT: "ALL (p::real list) (a::real) b::real. |
3389 |
a < b --> |
|
3390 |
(EX x::real. |
|
3391 |
a < x & x < b & poly p b - poly p a = (b - a) * poly (diff p) x)" |
|
14516 | 3392 |
by (import poly POLY_MVT) |
3393 |
||
17644 | 3394 |
lemma POLY_ADD_RZERO: "ALL x::real list. poly (poly_add x []) = poly x" |
14516 | 3395 |
by (import poly POLY_ADD_RZERO) |
3396 |
||
17644 | 3397 |
lemma POLY_MUL_ASSOC: "ALL (x::real list) (xa::real list) xb::real list. |
14516 | 3398 |
poly (poly_mul x (poly_mul xa xb)) = poly (poly_mul (poly_mul x xa) xb)" |
3399 |
by (import poly POLY_MUL_ASSOC) |
|
3400 |
||
17644 | 3401 |
lemma POLY_EXP_ADD: "ALL (x::nat) (xa::nat) xb::real list. |
14516 | 3402 |
poly (poly_exp xb (xa + x)) = |
3403 |
poly (poly_mul (poly_exp xb xa) (poly_exp xb x))" |
|
3404 |
by (import poly POLY_EXP_ADD) |
|
3405 |
||
17644 | 3406 |
lemma POLY_DIFF_AUX_ADD: "ALL (t::real list) (p2::real list) n::nat. |
14516 | 3407 |
poly (poly_diff_aux n (poly_add t p2)) = |
3408 |
poly (poly_add (poly_diff_aux n t) (poly_diff_aux n p2))" |
|
3409 |
by (import poly POLY_DIFF_AUX_ADD) |
|
3410 |
||
17644 | 3411 |
lemma POLY_DIFF_AUX_CMUL: "ALL (t::real list) (c::real) n::nat. |
3412 |
poly (poly_diff_aux n (## c t)) = poly (## c (poly_diff_aux n t))" |
|
14516 | 3413 |
by (import poly POLY_DIFF_AUX_CMUL) |
3414 |
||
17644 | 3415 |
lemma POLY_DIFF_AUX_NEG: "ALL (x::real list) xa::nat. |
14516 | 3416 |
poly (poly_diff_aux xa (poly_neg x)) = |
3417 |
poly (poly_neg (poly_diff_aux xa x))" |
|
3418 |
by (import poly POLY_DIFF_AUX_NEG) |
|
3419 |
||
17644 | 3420 |
lemma POLY_DIFF_AUX_MUL_LEMMA: "ALL (t::real list) n::nat. |
14516 | 3421 |
poly (poly_diff_aux (Suc n) t) = poly (poly_add (poly_diff_aux n t) t)" |
3422 |
by (import poly POLY_DIFF_AUX_MUL_LEMMA) |
|
3423 |
||
17644 | 3424 |
lemma POLY_DIFF_ADD: "ALL (t::real list) p2::real list. |
3425 |
poly (diff (poly_add t p2)) = poly (poly_add (diff t) (diff p2))" |
|
14516 | 3426 |
by (import poly POLY_DIFF_ADD) |
3427 |
||
17644 | 3428 |
lemma POLY_DIFF_CMUL: "ALL (t::real list) c::real. poly (diff (## c t)) = poly (## c (diff t))" |
14516 | 3429 |
by (import poly POLY_DIFF_CMUL) |
3430 |
||
17644 | 3431 |
lemma POLY_DIFF_NEG: "ALL x::real list. poly (diff (poly_neg x)) = poly (poly_neg (diff x))" |
14516 | 3432 |
by (import poly POLY_DIFF_NEG) |
3433 |
||
17644 | 3434 |
lemma POLY_DIFF_MUL_LEMMA: "ALL (x::real list) xa::real. |
17652 | 3435 |
poly (diff (xa # x)) = poly (poly_add (0 # diff x) x)" |
14516 | 3436 |
by (import poly POLY_DIFF_MUL_LEMMA) |
3437 |
||
17644 | 3438 |
lemma POLY_DIFF_MUL: "ALL (t::real list) p2::real list. |
14516 | 3439 |
poly (diff (poly_mul t p2)) = |
3440 |
poly (poly_add (poly_mul t (diff p2)) (poly_mul (diff t) p2))" |
|
3441 |
by (import poly POLY_DIFF_MUL) |
|
3442 |
||
17644 | 3443 |
lemma POLY_DIFF_EXP: "ALL (p::real list) n::nat. |
14516 | 3444 |
poly (diff (poly_exp p (Suc n))) = |
3445 |
poly (poly_mul (## (real (Suc n)) (poly_exp p n)) (diff p))" |
|
3446 |
by (import poly POLY_DIFF_EXP) |
|
3447 |
||
17644 | 3448 |
lemma POLY_DIFF_EXP_PRIME: "ALL (n::nat) a::real. |
17652 | 3449 |
poly (diff (poly_exp [- a, 1] (Suc n))) = |
3450 |
poly (## (real (Suc n)) (poly_exp [- a, 1] n))" |
|
14516 | 3451 |
by (import poly POLY_DIFF_EXP_PRIME) |
3452 |
||
17644 | 3453 |
lemma POLY_LINEAR_REM: "ALL (t::real list) h::real. |
3454 |
EX (q::real list) r::real. |
|
17652 | 3455 |
h # t = poly_add [r] (poly_mul [- (a::real), 1] q)" |
14516 | 3456 |
by (import poly POLY_LINEAR_REM) |
3457 |
||
17644 | 3458 |
lemma POLY_LINEAR_DIVIDES: "ALL (a::real) t::real list. |
17652 | 3459 |
(poly t a = 0) = (t = [] | (EX q::real list. t = poly_mul [- a, 1] q))" |
14516 | 3460 |
by (import poly POLY_LINEAR_DIVIDES) |
3461 |
||
17652 | 3462 |
lemma POLY_LENGTH_MUL: "ALL x::real list. length (poly_mul [- (a::real), 1] x) = Suc (length x)" |
14516 | 3463 |
by (import poly POLY_LENGTH_MUL) |
3464 |
||
3465 |
lemma POLY_ROOTS_INDEX_LEMMA: "(All::(nat => bool) => bool) |
|
3466 |
(%n::nat. |
|
3467 |
(All::(real list => bool) => bool) |
|
3468 |
(%p::real list. |
|
3469 |
(op -->::bool => bool => bool) |
|
3470 |
((op &::bool => bool => bool) |
|
3471 |
((Not::bool => bool) |
|
3472 |
((op =::(real => real) => (real => real) => bool) |
|
3473 |
((poly::real list => real => real) p) |
|
3474 |
((poly::real list => real => real) ([]::real list)))) |
|
3475 |
((op =::nat => nat => bool) ((size::real list => nat) p) n)) |
|
3476 |
((Ex::((nat => real) => bool) => bool) |
|
3477 |
(%i::nat => real. |
|
3478 |
(All::(real => bool) => bool) |
|
3479 |
(%x::real. |
|
3480 |
(op -->::bool => bool => bool) |
|
3481 |
((op =::real => real => bool) |
|
3482 |
((poly::real list => real => real) p x) (0::real)) |
|
3483 |
((Ex::(nat => bool) => bool) |
|
3484 |
(%m::nat. |
|
3485 |
(op &::bool => bool => bool) |
|
3486 |
((op <=::nat => nat => bool) m n) |
|
3487 |
((op =::real => real => bool) x (i m)))))))))" |
|
3488 |
by (import poly POLY_ROOTS_INDEX_LEMMA) |
|
3489 |
||
3490 |
lemma POLY_ROOTS_INDEX_LENGTH: "(All::(real list => bool) => bool) |
|
3491 |
(%p::real list. |
|
3492 |
(op -->::bool => bool => bool) |
|
3493 |
((Not::bool => bool) |
|
3494 |
((op =::(real => real) => (real => real) => bool) |
|
3495 |
((poly::real list => real => real) p) |
|
3496 |
((poly::real list => real => real) ([]::real list)))) |
|
3497 |
((Ex::((nat => real) => bool) => bool) |
|
3498 |
(%i::nat => real. |
|
3499 |
(All::(real => bool) => bool) |
|
3500 |
(%x::real. |
|
3501 |
(op -->::bool => bool => bool) |
|
3502 |
((op =::real => real => bool) |
|
3503 |
((poly::real list => real => real) p x) (0::real)) |
|
3504 |
((Ex::(nat => bool) => bool) |
|
3505 |
(%n::nat. |
|
3506 |
(op &::bool => bool => bool) |
|
3507 |
((op <=::nat => nat => bool) n |
|
3508 |
((size::real list => nat) p)) |
|
3509 |
((op =::real => real => bool) x (i n))))))))" |
|
3510 |
by (import poly POLY_ROOTS_INDEX_LENGTH) |
|
3511 |
||
3512 |
lemma POLY_ROOTS_FINITE_LEMMA: "(All::(real list => bool) => bool) |
|
3513 |
(%p::real list. |
|
3514 |
(op -->::bool => bool => bool) |
|
3515 |
((Not::bool => bool) |
|
3516 |
((op =::(real => real) => (real => real) => bool) |
|
3517 |
((poly::real list => real => real) p) |
|
3518 |
((poly::real list => real => real) ([]::real list)))) |
|
3519 |
((Ex::(nat => bool) => bool) |
|
3520 |
(%N::nat. |
|
3521 |
(Ex::((nat => real) => bool) => bool) |
|
3522 |
(%i::nat => real. |
|
3523 |
(All::(real => bool) => bool) |
|
3524 |
(%x::real. |
|
3525 |
(op -->::bool => bool => bool) |
|
3526 |
((op =::real => real => bool) |
|
3527 |
((poly::real list => real => real) p x) (0::real)) |
|
3528 |
((Ex::(nat => bool) => bool) |
|
3529 |
(%n::nat. |
|
3530 |
(op &::bool => bool => bool) |
|
3531 |
((op <::nat => nat => bool) n N) |
|
3532 |
((op =::real => real => bool) x (i n)))))))))" |
|
3533 |
by (import poly POLY_ROOTS_FINITE_LEMMA) |
|
3534 |
||
3535 |
lemma FINITE_LEMMA: "(All::((nat => real) => bool) => bool) |
|
3536 |
(%i::nat => real. |
|
3537 |
(All::(nat => bool) => bool) |
|
3538 |
(%x::nat. |
|
3539 |
(All::((real => bool) => bool) => bool) |
|
3540 |
(%xa::real => bool. |
|
3541 |
(op -->::bool => bool => bool) |
|
3542 |
((All::(real => bool) => bool) |
|
3543 |
(%xb::real. |
|
3544 |
(op -->::bool => bool => bool) (xa xb) |
|
3545 |
((Ex::(nat => bool) => bool) |
|
3546 |
(%n::nat. |
|
3547 |
(op &::bool => bool => bool) |
|
3548 |
((op <::nat => nat => bool) n x) |
|
3549 |
((op =::real => real => bool) xb (i n)))))) |
|
3550 |
((Ex::(real => bool) => bool) |
|
3551 |
(%a::real. |
|
3552 |
(All::(real => bool) => bool) |
|
3553 |
(%x::real. |
|
3554 |
(op -->::bool => bool => bool) (xa x) |
|
3555 |
((op <::real => real => bool) x a)))))))" |
|
3556 |
by (import poly FINITE_LEMMA) |
|
3557 |
||
3558 |
lemma POLY_ROOTS_FINITE: "(All::(real list => bool) => bool) |
|
3559 |
(%p::real list. |
|
3560 |
(op =::bool => bool => bool) |
|
3561 |
((Not::bool => bool) |
|
3562 |
((op =::(real => real) => (real => real) => bool) |
|
3563 |
((poly::real list => real => real) p) |
|
3564 |
((poly::real list => real => real) ([]::real list)))) |
|
3565 |
((Ex::(nat => bool) => bool) |
|
3566 |
(%N::nat. |
|
3567 |
(Ex::((nat => real) => bool) => bool) |
|
3568 |
(%i::nat => real. |
|
3569 |
(All::(real => bool) => bool) |
|
3570 |
(%x::real. |
|
3571 |
(op -->::bool => bool => bool) |
|
3572 |
((op =::real => real => bool) |
|
3573 |
((poly::real list => real => real) p x) (0::real)) |
|
3574 |
((Ex::(nat => bool) => bool) |
|
3575 |
(%n::nat. |
|
3576 |
(op &::bool => bool => bool) |
|
3577 |
((op <::nat => nat => bool) n N) |
|
3578 |
((op =::real => real => bool) x (i n)))))))))" |
|
3579 |
by (import poly POLY_ROOTS_FINITE) |
|
3580 |
||
17694 | 3581 |
lemma POLY_ENTIRE_LEMMA: "ALL (p::real list) q::real list. |
3582 |
poly p ~= poly [] & poly q ~= poly [] --> poly (poly_mul p q) ~= poly []" |
|
14516 | 3583 |
by (import poly POLY_ENTIRE_LEMMA) |
3584 |
||
17644 | 3585 |
lemma POLY_ENTIRE: "ALL (p::real list) q::real list. |
14516 | 3586 |
(poly (poly_mul p q) = poly []) = (poly p = poly [] | poly q = poly [])" |
3587 |
by (import poly POLY_ENTIRE) |
|
3588 |
||
17644 | 3589 |
lemma POLY_MUL_LCANCEL: "ALL (x::real list) (xa::real list) xb::real list. |
14516 | 3590 |
(poly (poly_mul x xa) = poly (poly_mul x xb)) = |
3591 |
(poly x = poly [] | poly xa = poly xb)" |
|
3592 |
by (import poly POLY_MUL_LCANCEL) |
|
3593 |
||
17644 | 3594 |
lemma POLY_EXP_EQ_0: "ALL (p::real list) n::nat. |
17652 | 3595 |
(poly (poly_exp p n) = poly []) = (poly p = poly [] & n ~= 0)" |
14516 | 3596 |
by (import poly POLY_EXP_EQ_0) |
3597 |
||
17652 | 3598 |
lemma POLY_PRIME_EQ_0: "ALL a::real. poly [a, 1] ~= poly []" |
14516 | 3599 |
by (import poly POLY_PRIME_EQ_0) |
3600 |
||
17652 | 3601 |
lemma POLY_EXP_PRIME_EQ_0: "ALL (a::real) n::nat. poly (poly_exp [a, 1] n) ~= poly []" |
14516 | 3602 |
by (import poly POLY_EXP_PRIME_EQ_0) |
3603 |
||
17694 | 3604 |
lemma POLY_ZERO_LEMMA: "ALL (h::real) t::real list. |
3605 |
poly (h # t) = poly [] --> h = 0 & poly t = poly []" |
|
14516 | 3606 |
by (import poly POLY_ZERO_LEMMA) |
3607 |
||
17652 | 3608 |
lemma POLY_ZERO: "ALL t::real list. (poly t = poly []) = list_all (%c::real. c = 0) t" |
14516 | 3609 |
by (import poly POLY_ZERO) |
3610 |
||
17644 | 3611 |
lemma POLY_DIFF_AUX_ISZERO: "ALL (t::real list) n::nat. |
17652 | 3612 |
list_all (%c::real. c = 0) (poly_diff_aux (Suc n) t) = |
3613 |
list_all (%c::real. c = 0) t" |
|
14516 | 3614 |
by (import poly POLY_DIFF_AUX_ISZERO) |
3615 |
||
17694 | 3616 |
lemma POLY_DIFF_ISZERO: "ALL x::real list. |
3617 |
poly (diff x) = poly [] --> (EX h::real. poly x = poly [h])" |
|
14516 | 3618 |
by (import poly POLY_DIFF_ISZERO) |
3619 |
||
17694 | 3620 |
lemma POLY_DIFF_ZERO: "ALL x::real list. poly x = poly [] --> poly (diff x) = poly []" |
14516 | 3621 |
by (import poly POLY_DIFF_ZERO) |
3622 |
||
17694 | 3623 |
lemma POLY_DIFF_WELLDEF: "ALL (p::real list) q::real list. |
3624 |
poly p = poly q --> poly (diff p) = poly (diff q)" |
|
14516 | 3625 |
by (import poly POLY_DIFF_WELLDEF) |
3626 |
||
3627 |
constdefs |
|
3628 |
poly_divides :: "real list => real list => bool" |
|
17644 | 3629 |
"poly_divides == |
3630 |
%(p1::real list) p2::real list. |
|
3631 |
EX q::real list. poly p2 = poly (poly_mul p1 q)" |
|
3632 |
||
3633 |
lemma poly_divides: "ALL (p1::real list) p2::real list. |
|
3634 |
poly_divides p1 p2 = (EX q::real list. poly p2 = poly (poly_mul p1 q))" |
|
14516 | 3635 |
by (import poly poly_divides) |
3636 |
||
17644 | 3637 |
lemma POLY_PRIMES: "ALL (a::real) (p::real list) q::real list. |
17652 | 3638 |
poly_divides [a, 1] (poly_mul p q) = |
3639 |
(poly_divides [a, 1] p | poly_divides [a, 1] q)" |
|
14516 | 3640 |
by (import poly POLY_PRIMES) |
3641 |
||
17644 | 3642 |
lemma POLY_DIVIDES_REFL: "ALL p::real list. poly_divides p p" |
14516 | 3643 |
by (import poly POLY_DIVIDES_REFL) |
3644 |
||
17694 | 3645 |
lemma POLY_DIVIDES_TRANS: "ALL (p::real list) (q::real list) r::real list. |
3646 |
poly_divides p q & poly_divides q r --> poly_divides p r" |
|
14516 | 3647 |
by (import poly POLY_DIVIDES_TRANS) |
3648 |
||
17694 | 3649 |
lemma POLY_DIVIDES_EXP: "ALL (p::real list) (m::nat) n::nat. |
3650 |
m <= n --> poly_divides (poly_exp p m) (poly_exp p n)" |
|
14516 | 3651 |
by (import poly POLY_DIVIDES_EXP) |
3652 |
||
17694 | 3653 |
lemma POLY_EXP_DIVIDES: "ALL (p::real list) (q::real list) (m::nat) n::nat. |
3654 |
poly_divides (poly_exp p n) q & m <= n --> poly_divides (poly_exp p m) q" |
|
14516 | 3655 |
by (import poly POLY_EXP_DIVIDES) |
3656 |
||
17694 | 3657 |
lemma POLY_DIVIDES_ADD: "ALL (p::real list) (q::real list) r::real list. |
3658 |
poly_divides p q & poly_divides p r --> poly_divides p (poly_add q r)" |
|
14516 | 3659 |
by (import poly POLY_DIVIDES_ADD) |
3660 |
||
17694 | 3661 |
lemma POLY_DIVIDES_SUB: "ALL (p::real list) (q::real list) r::real list. |
3662 |
poly_divides p q & poly_divides p (poly_add q r) --> poly_divides p r" |
|
14516 | 3663 |
by (import poly POLY_DIVIDES_SUB) |
3664 |
||
17694 | 3665 |
lemma POLY_DIVIDES_SUB2: "ALL (p::real list) (q::real list) r::real list. |
3666 |
poly_divides p r & poly_divides p (poly_add q r) --> poly_divides p q" |
|
14516 | 3667 |
by (import poly POLY_DIVIDES_SUB2) |
3668 |
||
17694 | 3669 |
lemma POLY_DIVIDES_ZERO: "ALL (p::real list) q::real list. poly p = poly [] --> poly_divides q p" |
14516 | 3670 |
by (import poly POLY_DIVIDES_ZERO) |
3671 |
||
17694 | 3672 |
lemma POLY_ORDER_EXISTS: "ALL (a::real) (d::nat) p::real list. |
3673 |
length p = d & poly p ~= poly [] --> |
|
3674 |
(EX x::nat. |
|
3675 |
poly_divides (poly_exp [- a, 1] x) p & |
|
3676 |
~ poly_divides (poly_exp [- a, 1] (Suc x)) p)" |
|
14516 | 3677 |
by (import poly POLY_ORDER_EXISTS) |
3678 |
||
17694 | 3679 |
lemma POLY_ORDER: "ALL (p::real list) a::real. |
3680 |
poly p ~= poly [] --> |
|
3681 |
(EX! n::nat. |
|
3682 |
poly_divides (poly_exp [- a, 1] n) p & |
|
3683 |
~ poly_divides (poly_exp [- a, 1] (Suc n)) p)" |
|
14516 | 3684 |
by (import poly POLY_ORDER) |
3685 |
||
3686 |
constdefs |
|
3687 |
poly_order :: "real => real list => nat" |
|
3688 |
"poly_order == |
|
17644 | 3689 |
%(a::real) p::real list. |
3690 |
SOME n::nat. |
|
17652 | 3691 |
poly_divides (poly_exp [- a, 1] n) p & |
3692 |
~ poly_divides (poly_exp [- a, 1] (Suc n)) p" |
|
17644 | 3693 |
|
3694 |
lemma poly_order: "ALL (a::real) p::real list. |
|
14516 | 3695 |
poly_order a p = |
17644 | 3696 |
(SOME n::nat. |
17652 | 3697 |
poly_divides (poly_exp [- a, 1] n) p & |
3698 |
~ poly_divides (poly_exp [- a, 1] (Suc n)) p)" |
|
14516 | 3699 |
by (import poly poly_order) |
3700 |
||
17644 | 3701 |
lemma ORDER: "ALL (p::real list) (a::real) n::nat. |
17652 | 3702 |
(poly_divides (poly_exp [- a, 1] n) p & |
3703 |
~ poly_divides (poly_exp [- a, 1] (Suc n)) p) = |
|
14516 | 3704 |
(n = poly_order a p & poly p ~= poly [])" |
3705 |
by (import poly ORDER) |
|
3706 |
||
17694 | 3707 |
lemma ORDER_THM: "ALL (p::real list) a::real. |
3708 |
poly p ~= poly [] --> |
|
3709 |
poly_divides (poly_exp [- a, 1] (poly_order a p)) p & |
|
3710 |
~ poly_divides (poly_exp [- a, 1] (Suc (poly_order a p))) p" |
|
14516 | 3711 |
by (import poly ORDER_THM) |
3712 |
||
17694 | 3713 |
lemma ORDER_UNIQUE: "ALL (p::real list) (a::real) n::nat. |
3714 |
poly p ~= poly [] & |
|
3715 |
poly_divides (poly_exp [- a, 1] n) p & |
|
3716 |
~ poly_divides (poly_exp [- a, 1] (Suc n)) p --> |
|
3717 |
n = poly_order a p" |
|
14516 | 3718 |
by (import poly ORDER_UNIQUE) |
3719 |
||
17694 | 3720 |
lemma ORDER_POLY: "ALL (p::real list) (q::real list) a::real. |
3721 |
poly p = poly q --> poly_order a p = poly_order a q" |
|
14516 | 3722 |
by (import poly ORDER_POLY) |
3723 |
||
17644 | 3724 |
lemma ORDER_ROOT: "ALL (p::real list) a::real. |
17652 | 3725 |
(poly p a = 0) = (poly p = poly [] | poly_order a p ~= 0)" |
14516 | 3726 |
by (import poly ORDER_ROOT) |
3727 |
||
17644 | 3728 |
lemma ORDER_DIVIDES: "ALL (p::real list) (a::real) n::nat. |
17652 | 3729 |
poly_divides (poly_exp [- a, 1] n) p = |
14516 | 3730 |
(poly p = poly [] | n <= poly_order a p)" |
3731 |
by (import poly ORDER_DIVIDES) |
|
3732 |
||
17694 | 3733 |
lemma ORDER_DECOMP: "ALL (p::real list) a::real. |
3734 |
poly p ~= poly [] --> |
|
3735 |
(EX x::real list. |
|
3736 |
poly p = poly (poly_mul (poly_exp [- a, 1] (poly_order a p)) x) & |
|
3737 |
~ poly_divides [- a, 1] x)" |
|
14516 | 3738 |
by (import poly ORDER_DECOMP) |
3739 |
||
17694 | 3740 |
lemma ORDER_MUL: "ALL (a::real) (p::real list) q::real list. |
3741 |
poly (poly_mul p q) ~= poly [] --> |
|
3742 |
poly_order a (poly_mul p q) = poly_order a p + poly_order a q" |
|
14516 | 3743 |
by (import poly ORDER_MUL) |
3744 |
||
17694 | 3745 |
lemma ORDER_DIFF: "ALL (p::real list) a::real. |
3746 |
poly (diff p) ~= poly [] & poly_order a p ~= 0 --> |
|
3747 |
poly_order a p = Suc (poly_order a (diff p))" |
|
14516 | 3748 |
by (import poly ORDER_DIFF) |
3749 |
||
17694 | 3750 |
lemma POLY_SQUAREFREE_DECOMP_ORDER: "ALL (p::real list) (q::real list) (d::real list) (e::real list) |
3751 |
(r::real list) s::real list. |
|
3752 |
poly (diff p) ~= poly [] & |
|
3753 |
poly p = poly (poly_mul q d) & |
|
3754 |
poly (diff p) = poly (poly_mul e d) & |
|
3755 |
poly d = poly (poly_add (poly_mul r p) (poly_mul s (diff p))) --> |
|
3756 |
(ALL a::real. poly_order a q = (if poly_order a p = 0 then 0 else 1))" |
|
14516 | 3757 |
by (import poly POLY_SQUAREFREE_DECOMP_ORDER) |
3758 |
||
3759 |
constdefs |
|
3760 |
rsquarefree :: "real list => bool" |
|
3761 |
"rsquarefree == |
|
17644 | 3762 |
%p::real list. |
3763 |
poly p ~= poly [] & |
|
17652 | 3764 |
(ALL a::real. poly_order a p = 0 | poly_order a p = 1)" |
17644 | 3765 |
|
3766 |
lemma rsquarefree: "ALL p::real list. |
|
14516 | 3767 |
rsquarefree p = |
17644 | 3768 |
(poly p ~= poly [] & |
17652 | 3769 |
(ALL a::real. poly_order a p = 0 | poly_order a p = 1))" |
14516 | 3770 |
by (import poly rsquarefree) |
3771 |
||
17644 | 3772 |
lemma RSQUAREFREE_ROOTS: "ALL p::real list. |
17652 | 3773 |
rsquarefree p = (ALL a::real. ~ (poly p a = 0 & poly (diff p) a = 0))" |
14516 | 3774 |
by (import poly RSQUAREFREE_ROOTS) |
3775 |
||
17694 | 3776 |
lemma RSQUAREFREE_DECOMP: "ALL (p::real list) a::real. |
3777 |
rsquarefree p & poly p a = 0 --> |
|
3778 |
(EX q::real list. poly p = poly (poly_mul [- a, 1] q) & poly q a ~= 0)" |
|
14516 | 3779 |
by (import poly RSQUAREFREE_DECOMP) |
3780 |
||
17694 | 3781 |
lemma POLY_SQUAREFREE_DECOMP: "ALL (p::real list) (q::real list) (d::real list) (e::real list) |
3782 |
(r::real list) s::real list. |
|
3783 |
poly (diff p) ~= poly [] & |
|
3784 |
poly p = poly (poly_mul q d) & |
|
3785 |
poly (diff p) = poly (poly_mul e d) & |
|
3786 |
poly d = poly (poly_add (poly_mul r p) (poly_mul s (diff p))) --> |
|
3787 |
rsquarefree q & (ALL x::real. (poly q x = 0) = (poly p x = 0))" |
|
14516 | 3788 |
by (import poly POLY_SQUAREFREE_DECOMP) |
3789 |
||
3790 |
consts |
|
3791 |
normalize :: "real list => real list" |
|
3792 |
||
3793 |
specification (normalize) normalize: "normalize [] = [] & |
|
17644 | 3794 |
(ALL (h::real) t::real list. |
14516 | 3795 |
normalize (h # t) = |
17652 | 3796 |
(if normalize t = [] then if h = 0 then [] else [h] |
14516 | 3797 |
else h # normalize t))" |
3798 |
by (import poly normalize) |
|
3799 |
||
17644 | 3800 |
lemma POLY_NORMALIZE: "ALL t::real list. poly (normalize t) = poly t" |
14516 | 3801 |
by (import poly POLY_NORMALIZE) |
3802 |
||
3803 |
constdefs |
|
3804 |
degree :: "real list => nat" |
|
17644 | 3805 |
"degree == %p::real list. PRE (length (normalize p))" |
3806 |
||
3807 |
lemma degree: "ALL p::real list. degree p = PRE (length (normalize p))" |
|
14516 | 3808 |
by (import poly degree) |
3809 |
||
17694 | 3810 |
lemma DEGREE_ZERO: "ALL p::real list. poly p = poly [] --> degree p = 0" |
14516 | 3811 |
by (import poly DEGREE_ZERO) |
3812 |
||
17694 | 3813 |
lemma POLY_ROOTS_FINITE_SET: "ALL p::real list. |
3814 |
poly p ~= poly [] --> FINITE (GSPEC (%x::real. (x, poly p x = 0)))" |
|
14516 | 3815 |
by (import poly POLY_ROOTS_FINITE_SET) |
3816 |
||
17694 | 3817 |
lemma POLY_MONO: "ALL (x::real) (k::real) xa::real list. |
3818 |
abs x <= k --> abs (poly xa x) <= poly (map abs xa) k" |
|
14516 | 3819 |
by (import poly POLY_MONO) |
3820 |
||
3821 |
;end_setup |
|
3822 |
||
3823 |
end |
|
3824 |