1 (* Title : HOL/Hyperreal/HyperDef.thy |
|
2 ID : $Id$ |
|
3 Author : Jacques D. Fleuriot |
|
4 Copyright : 1998 University of Cambridge |
|
5 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
|
6 *) |
|
7 |
|
8 header{*Construction of Hyperreals Using Ultrafilters*} |
|
9 |
|
10 theory HyperDef |
|
11 imports HyperNat "../Real/Real" |
|
12 uses ("hypreal_arith.ML") |
|
13 begin |
|
14 |
|
15 types hypreal = "real star" |
|
16 |
|
17 abbreviation |
|
18 hypreal_of_real :: "real => real star" where |
|
19 "hypreal_of_real == star_of" |
|
20 |
|
21 abbreviation |
|
22 hypreal_of_hypnat :: "hypnat \<Rightarrow> hypreal" where |
|
23 "hypreal_of_hypnat \<equiv> of_hypnat" |
|
24 |
|
25 definition |
|
26 omega :: hypreal where |
|
27 -- {*an infinite number @{text "= [<1,2,3,...>]"} *} |
|
28 "omega = star_n (\<lambda>n. real (Suc n))" |
|
29 |
|
30 definition |
|
31 epsilon :: hypreal where |
|
32 -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *} |
|
33 "epsilon = star_n (\<lambda>n. inverse (real (Suc n)))" |
|
34 |
|
35 notation (xsymbols) |
|
36 omega ("\<omega>") and |
|
37 epsilon ("\<epsilon>") |
|
38 |
|
39 notation (HTML output) |
|
40 omega ("\<omega>") and |
|
41 epsilon ("\<epsilon>") |
|
42 |
|
43 |
|
44 subsection {* Real vector class instances *} |
|
45 |
|
46 instantiation star :: (scaleR) scaleR |
|
47 begin |
|
48 |
|
49 definition |
|
50 star_scaleR_def [transfer_unfold, code func del]: "scaleR r \<equiv> *f* (scaleR r)" |
|
51 |
|
52 instance .. |
|
53 |
|
54 end |
|
55 |
|
56 lemma Standard_scaleR [simp]: "x \<in> Standard \<Longrightarrow> scaleR r x \<in> Standard" |
|
57 by (simp add: star_scaleR_def) |
|
58 |
|
59 lemma star_of_scaleR [simp]: "star_of (scaleR r x) = scaleR r (star_of x)" |
|
60 by transfer (rule refl) |
|
61 |
|
62 instance star :: (real_vector) real_vector |
|
63 proof |
|
64 fix a b :: real |
|
65 show "\<And>x y::'a star. scaleR a (x + y) = scaleR a x + scaleR a y" |
|
66 by transfer (rule scaleR_right_distrib) |
|
67 show "\<And>x::'a star. scaleR (a + b) x = scaleR a x + scaleR b x" |
|
68 by transfer (rule scaleR_left_distrib) |
|
69 show "\<And>x::'a star. scaleR a (scaleR b x) = scaleR (a * b) x" |
|
70 by transfer (rule scaleR_scaleR) |
|
71 show "\<And>x::'a star. scaleR 1 x = x" |
|
72 by transfer (rule scaleR_one) |
|
73 qed |
|
74 |
|
75 instance star :: (real_algebra) real_algebra |
|
76 proof |
|
77 fix a :: real |
|
78 show "\<And>x y::'a star. scaleR a x * y = scaleR a (x * y)" |
|
79 by transfer (rule mult_scaleR_left) |
|
80 show "\<And>x y::'a star. x * scaleR a y = scaleR a (x * y)" |
|
81 by transfer (rule mult_scaleR_right) |
|
82 qed |
|
83 |
|
84 instance star :: (real_algebra_1) real_algebra_1 .. |
|
85 |
|
86 instance star :: (real_div_algebra) real_div_algebra .. |
|
87 |
|
88 instance star :: (real_field) real_field .. |
|
89 |
|
90 lemma star_of_real_def [transfer_unfold]: "of_real r = star_of (of_real r)" |
|
91 by (unfold of_real_def, transfer, rule refl) |
|
92 |
|
93 lemma Standard_of_real [simp]: "of_real r \<in> Standard" |
|
94 by (simp add: star_of_real_def) |
|
95 |
|
96 lemma star_of_of_real [simp]: "star_of (of_real r) = of_real r" |
|
97 by transfer (rule refl) |
|
98 |
|
99 lemma of_real_eq_star_of [simp]: "of_real = star_of" |
|
100 proof |
|
101 fix r :: real |
|
102 show "of_real r = star_of r" |
|
103 by transfer simp |
|
104 qed |
|
105 |
|
106 lemma Reals_eq_Standard: "(Reals :: hypreal set) = Standard" |
|
107 by (simp add: Reals_def Standard_def) |
|
108 |
|
109 |
|
110 subsection {* Injection from @{typ hypreal} *} |
|
111 |
|
112 definition |
|
113 of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where |
|
114 [transfer_unfold, code func del]: "of_hypreal = *f* of_real" |
|
115 |
|
116 lemma Standard_of_hypreal [simp]: |
|
117 "r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard" |
|
118 by (simp add: of_hypreal_def) |
|
119 |
|
120 lemma of_hypreal_0 [simp]: "of_hypreal 0 = 0" |
|
121 by transfer (rule of_real_0) |
|
122 |
|
123 lemma of_hypreal_1 [simp]: "of_hypreal 1 = 1" |
|
124 by transfer (rule of_real_1) |
|
125 |
|
126 lemma of_hypreal_add [simp]: |
|
127 "\<And>x y. of_hypreal (x + y) = of_hypreal x + of_hypreal y" |
|
128 by transfer (rule of_real_add) |
|
129 |
|
130 lemma of_hypreal_minus [simp]: "\<And>x. of_hypreal (- x) = - of_hypreal x" |
|
131 by transfer (rule of_real_minus) |
|
132 |
|
133 lemma of_hypreal_diff [simp]: |
|
134 "\<And>x y. of_hypreal (x - y) = of_hypreal x - of_hypreal y" |
|
135 by transfer (rule of_real_diff) |
|
136 |
|
137 lemma of_hypreal_mult [simp]: |
|
138 "\<And>x y. of_hypreal (x * y) = of_hypreal x * of_hypreal y" |
|
139 by transfer (rule of_real_mult) |
|
140 |
|
141 lemma of_hypreal_inverse [simp]: |
|
142 "\<And>x. of_hypreal (inverse x) = |
|
143 inverse (of_hypreal x :: 'a::{real_div_algebra,division_by_zero} star)" |
|
144 by transfer (rule of_real_inverse) |
|
145 |
|
146 lemma of_hypreal_divide [simp]: |
|
147 "\<And>x y. of_hypreal (x / y) = |
|
148 (of_hypreal x / of_hypreal y :: 'a::{real_field,division_by_zero} star)" |
|
149 by transfer (rule of_real_divide) |
|
150 |
|
151 lemma of_hypreal_eq_iff [simp]: |
|
152 "\<And>x y. (of_hypreal x = of_hypreal y) = (x = y)" |
|
153 by transfer (rule of_real_eq_iff) |
|
154 |
|
155 lemma of_hypreal_eq_0_iff [simp]: |
|
156 "\<And>x. (of_hypreal x = 0) = (x = 0)" |
|
157 by transfer (rule of_real_eq_0_iff) |
|
158 |
|
159 |
|
160 subsection{*Properties of @{term starrel}*} |
|
161 |
|
162 lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}" |
|
163 by (simp add: starrel_def) |
|
164 |
|
165 lemma starrel_in_hypreal [simp]: "starrel``{x}:star" |
|
166 by (simp add: star_def starrel_def quotient_def, blast) |
|
167 |
|
168 declare Abs_star_inject [simp] Abs_star_inverse [simp] |
|
169 declare equiv_starrel [THEN eq_equiv_class_iff, simp] |
|
170 |
|
171 subsection{*@{term hypreal_of_real}: |
|
172 the Injection from @{typ real} to @{typ hypreal}*} |
|
173 |
|
174 lemma inj_star_of: "inj star_of" |
|
175 by (rule inj_onI, simp) |
|
176 |
|
177 lemma mem_Rep_star_iff: "(X \<in> Rep_star x) = (x = star_n X)" |
|
178 by (cases x, simp add: star_n_def) |
|
179 |
|
180 lemma Rep_star_star_n_iff [simp]: |
|
181 "(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)" |
|
182 by (simp add: star_n_def) |
|
183 |
|
184 lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)" |
|
185 by simp |
|
186 |
|
187 subsection{* Properties of @{term star_n} *} |
|
188 |
|
189 lemma star_n_add: |
|
190 "star_n X + star_n Y = star_n (%n. X n + Y n)" |
|
191 by (simp only: star_add_def starfun2_star_n) |
|
192 |
|
193 lemma star_n_minus: |
|
194 "- star_n X = star_n (%n. -(X n))" |
|
195 by (simp only: star_minus_def starfun_star_n) |
|
196 |
|
197 lemma star_n_diff: |
|
198 "star_n X - star_n Y = star_n (%n. X n - Y n)" |
|
199 by (simp only: star_diff_def starfun2_star_n) |
|
200 |
|
201 lemma star_n_mult: |
|
202 "star_n X * star_n Y = star_n (%n. X n * Y n)" |
|
203 by (simp only: star_mult_def starfun2_star_n) |
|
204 |
|
205 lemma star_n_inverse: |
|
206 "inverse (star_n X) = star_n (%n. inverse(X n))" |
|
207 by (simp only: star_inverse_def starfun_star_n) |
|
208 |
|
209 lemma star_n_le: |
|
210 "star_n X \<le> star_n Y = |
|
211 ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)" |
|
212 by (simp only: star_le_def starP2_star_n) |
|
213 |
|
214 lemma star_n_less: |
|
215 "star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)" |
|
216 by (simp only: star_less_def starP2_star_n) |
|
217 |
|
218 lemma star_n_zero_num: "0 = star_n (%n. 0)" |
|
219 by (simp only: star_zero_def star_of_def) |
|
220 |
|
221 lemma star_n_one_num: "1 = star_n (%n. 1)" |
|
222 by (simp only: star_one_def star_of_def) |
|
223 |
|
224 lemma star_n_abs: |
|
225 "abs (star_n X) = star_n (%n. abs (X n))" |
|
226 by (simp only: star_abs_def starfun_star_n) |
|
227 |
|
228 subsection{*Misc Others*} |
|
229 |
|
230 lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y" |
|
231 by (auto) |
|
232 |
|
233 lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)" |
|
234 by auto |
|
235 |
|
236 lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)" |
|
237 by auto |
|
238 |
|
239 lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)" |
|
240 by auto |
|
241 |
|
242 lemma hypreal_omega_gt_zero [simp]: "0 < omega" |
|
243 by (simp add: omega_def star_n_zero_num star_n_less) |
|
244 |
|
245 subsection{*Existence of Infinite Hyperreal Number*} |
|
246 |
|
247 text{*Existence of infinite number not corresponding to any real number. |
|
248 Use assumption that member @{term FreeUltrafilterNat} is not finite.*} |
|
249 |
|
250 |
|
251 text{*A few lemmas first*} |
|
252 |
|
253 lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} | |
|
254 (\<exists>y. {n::nat. x = real n} = {y})" |
|
255 by force |
|
256 |
|
257 lemma lemma_finite_omega_set: "finite {n::nat. x = real n}" |
|
258 by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto) |
|
259 |
|
260 lemma not_ex_hypreal_of_real_eq_omega: |
|
261 "~ (\<exists>x. hypreal_of_real x = omega)" |
|
262 apply (simp add: omega_def) |
|
263 apply (simp add: star_of_def star_n_eq_iff) |
|
264 apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] |
|
265 lemma_finite_omega_set [THEN FreeUltrafilterNat.finite]) |
|
266 done |
|
267 |
|
268 lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> omega" |
|
269 by (insert not_ex_hypreal_of_real_eq_omega, auto) |
|
270 |
|
271 text{*Existence of infinitesimal number also not corresponding to any |
|
272 real number*} |
|
273 |
|
274 lemma lemma_epsilon_empty_singleton_disj: |
|
275 "{n::nat. x = inverse(real(Suc n))} = {} | |
|
276 (\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})" |
|
277 by auto |
|
278 |
|
279 lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}" |
|
280 by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto) |
|
281 |
|
282 lemma not_ex_hypreal_of_real_eq_epsilon: "~ (\<exists>x. hypreal_of_real x = epsilon)" |
|
283 by (auto simp add: epsilon_def star_of_def star_n_eq_iff |
|
284 lemma_finite_epsilon_set [THEN FreeUltrafilterNat.finite]) |
|
285 |
|
286 lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> epsilon" |
|
287 by (insert not_ex_hypreal_of_real_eq_epsilon, auto) |
|
288 |
|
289 lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0" |
|
290 by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff |
|
291 del: star_of_zero) |
|
292 |
|
293 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)" |
|
294 by (simp add: epsilon_def omega_def star_n_inverse) |
|
295 |
|
296 lemma hypreal_epsilon_gt_zero: "0 < epsilon" |
|
297 by (simp add: hypreal_epsilon_inverse_omega) |
|
298 |
|
299 subsection{*Absolute Value Function for the Hyperreals*} |
|
300 |
|
301 lemma hrabs_add_less: |
|
302 "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)" |
|
303 by (simp add: abs_if split: split_if_asm) |
|
304 |
|
305 lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r" |
|
306 by (blast intro!: order_le_less_trans abs_ge_zero) |
|
307 |
|
308 lemma hrabs_disj: "abs x = (x::'a::abs_if) | abs x = -x" |
|
309 by (simp add: abs_if) |
|
310 |
|
311 lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y" |
|
312 by (simp add: abs_if split add: split_if_asm) |
|
313 |
|
314 |
|
315 subsection{*Embedding the Naturals into the Hyperreals*} |
|
316 |
|
317 abbreviation |
|
318 hypreal_of_nat :: "nat => hypreal" where |
|
319 "hypreal_of_nat == of_nat" |
|
320 |
|
321 lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}" |
|
322 by (simp add: Nats_def image_def) |
|
323 |
|
324 (*------------------------------------------------------------*) |
|
325 (* naturals embedded in hyperreals *) |
|
326 (* is a hyperreal c.f. NS extension *) |
|
327 (*------------------------------------------------------------*) |
|
328 |
|
329 lemma hypreal_of_nat_eq: |
|
330 "hypreal_of_nat (n::nat) = hypreal_of_real (real n)" |
|
331 by (simp add: real_of_nat_def) |
|
332 |
|
333 lemma hypreal_of_nat: |
|
334 "hypreal_of_nat m = star_n (%n. real m)" |
|
335 apply (fold star_of_def) |
|
336 apply (simp add: real_of_nat_def) |
|
337 done |
|
338 |
|
339 (* |
|
340 FIXME: we should declare this, as for type int, but many proofs would break. |
|
341 It replaces x+-y by x-y. |
|
342 Addsimps [symmetric hypreal_diff_def] |
|
343 *) |
|
344 |
|
345 use "hypreal_arith.ML" |
|
346 declaration {* K hypreal_arith_setup *} |
|
347 |
|
348 |
|
349 subsection {* Exponentials on the Hyperreals *} |
|
350 |
|
351 lemma hpowr_0 [simp]: "r ^ 0 = (1::hypreal)" |
|
352 by (rule power_0) |
|
353 |
|
354 lemma hpowr_Suc [simp]: "r ^ (Suc n) = (r::hypreal) * (r ^ n)" |
|
355 by (rule power_Suc) |
|
356 |
|
357 lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r" |
|
358 by simp |
|
359 |
|
360 lemma hrealpow_two_le [simp]: "(0::hypreal) \<le> r ^ Suc (Suc 0)" |
|
361 by (auto simp add: zero_le_mult_iff) |
|
362 |
|
363 lemma hrealpow_two_le_add_order [simp]: |
|
364 "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)" |
|
365 by (simp only: hrealpow_two_le add_nonneg_nonneg) |
|
366 |
|
367 lemma hrealpow_two_le_add_order2 [simp]: |
|
368 "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)" |
|
369 by (simp only: hrealpow_two_le add_nonneg_nonneg) |
|
370 |
|
371 lemma hypreal_add_nonneg_eq_0_iff: |
|
372 "[| 0 \<le> x; 0 \<le> y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))" |
|
373 by arith |
|
374 |
|
375 |
|
376 text{*FIXME: DELETE THESE*} |
|
377 lemma hypreal_three_squares_add_zero_iff: |
|
378 "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))" |
|
379 apply (simp only: zero_le_square add_nonneg_nonneg hypreal_add_nonneg_eq_0_iff, auto) |
|
380 done |
|
381 |
|
382 lemma hrealpow_three_squares_add_zero_iff [simp]: |
|
383 "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = |
|
384 (x = 0 & y = 0 & z = 0)" |
|
385 by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two) |
|
386 |
|
387 (*FIXME: This and RealPow.abs_realpow_two should be replaced by an abstract |
|
388 result proved in Ring_and_Field*) |
|
389 lemma hrabs_hrealpow_two [simp]: |
|
390 "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)" |
|
391 by (simp add: abs_mult) |
|
392 |
|
393 lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n" |
|
394 by (insert power_increasing [of 0 n "2::hypreal"], simp) |
|
395 |
|
396 lemma two_hrealpow_gt [simp]: "hypreal_of_nat n < 2 ^ n" |
|
397 apply (induct n) |
|
398 apply (auto simp add: left_distrib) |
|
399 apply (cut_tac n = n in two_hrealpow_ge_one, arith) |
|
400 done |
|
401 |
|
402 lemma hrealpow: |
|
403 "star_n X ^ m = star_n (%n. (X n::real) ^ m)" |
|
404 apply (induct_tac "m") |
|
405 apply (auto simp add: star_n_one_num star_n_mult power_0) |
|
406 done |
|
407 |
|
408 lemma hrealpow_sum_square_expand: |
|
409 "(x + (y::hypreal)) ^ Suc (Suc 0) = |
|
410 x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y" |
|
411 by (simp add: right_distrib left_distrib) |
|
412 |
|
413 lemma power_hypreal_of_real_number_of: |
|
414 "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)" |
|
415 by simp |
|
416 declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp] |
|
417 (* |
|
418 lemma hrealpow_HFinite: |
|
419 fixes x :: "'a::{real_normed_algebra,recpower} star" |
|
420 shows "x \<in> HFinite ==> x ^ n \<in> HFinite" |
|
421 apply (induct_tac "n") |
|
422 apply (auto simp add: power_Suc intro: HFinite_mult) |
|
423 done |
|
424 *) |
|
425 |
|
426 subsection{*Powers with Hypernatural Exponents*} |
|
427 |
|
428 definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where |
|
429 hyperpow_def [transfer_unfold, code func del]: "R pow N = ( *f2* op ^) R N" |
|
430 (* hypernatural powers of hyperreals *) |
|
431 |
|
432 lemma Standard_hyperpow [simp]: |
|
433 "\<lbrakk>r \<in> Standard; n \<in> Standard\<rbrakk> \<Longrightarrow> r pow n \<in> Standard" |
|
434 unfolding hyperpow_def by simp |
|
435 |
|
436 lemma hyperpow: "star_n X pow star_n Y = star_n (%n. X n ^ Y n)" |
|
437 by (simp add: hyperpow_def starfun2_star_n) |
|
438 |
|
439 lemma hyperpow_zero [simp]: |
|
440 "\<And>n. (0::'a::{recpower,semiring_0} star) pow (n + (1::hypnat)) = 0" |
|
441 by transfer simp |
|
442 |
|
443 lemma hyperpow_not_zero: |
|
444 "\<And>r n. r \<noteq> (0::'a::{recpower,field} star) ==> r pow n \<noteq> 0" |
|
445 by transfer (rule field_power_not_zero) |
|
446 |
|
447 lemma hyperpow_inverse: |
|
448 "\<And>r n. r \<noteq> (0::'a::{recpower,division_by_zero,field} star) |
|
449 \<Longrightarrow> inverse (r pow n) = (inverse r) pow n" |
|
450 by transfer (rule power_inverse) |
|
451 |
|
452 lemma hyperpow_hrabs: |
|
453 "\<And>r n. abs (r::'a::{recpower,ordered_idom} star) pow n = abs (r pow n)" |
|
454 by transfer (rule power_abs [symmetric]) |
|
455 |
|
456 lemma hyperpow_add: |
|
457 "\<And>r n m. (r::'a::recpower star) pow (n + m) = (r pow n) * (r pow m)" |
|
458 by transfer (rule power_add) |
|
459 |
|
460 lemma hyperpow_one [simp]: |
|
461 "\<And>r. (r::'a::recpower star) pow (1::hypnat) = r" |
|
462 by transfer (rule power_one_right) |
|
463 |
|
464 lemma hyperpow_two: |
|
465 "\<And>r. (r::'a::recpower star) pow ((1::hypnat) + (1::hypnat)) = r * r" |
|
466 by transfer (simp add: power_Suc) |
|
467 |
|
468 lemma hyperpow_gt_zero: |
|
469 "\<And>r n. (0::'a::{recpower,ordered_semidom} star) < r \<Longrightarrow> 0 < r pow n" |
|
470 by transfer (rule zero_less_power) |
|
471 |
|
472 lemma hyperpow_ge_zero: |
|
473 "\<And>r n. (0::'a::{recpower,ordered_semidom} star) \<le> r \<Longrightarrow> 0 \<le> r pow n" |
|
474 by transfer (rule zero_le_power) |
|
475 |
|
476 lemma hyperpow_le: |
|
477 "\<And>x y n. \<lbrakk>(0::'a::{recpower,ordered_semidom} star) < x; x \<le> y\<rbrakk> |
|
478 \<Longrightarrow> x pow n \<le> y pow n" |
|
479 by transfer (rule power_mono [OF _ order_less_imp_le]) |
|
480 |
|
481 lemma hyperpow_eq_one [simp]: |
|
482 "\<And>n. 1 pow n = (1::'a::recpower star)" |
|
483 by transfer (rule power_one) |
|
484 |
|
485 lemma hrabs_hyperpow_minus_one [simp]: |
|
486 "\<And>n. abs(-1 pow n) = (1::'a::{number_ring,recpower,ordered_idom} star)" |
|
487 by transfer (rule abs_power_minus_one) |
|
488 |
|
489 lemma hyperpow_mult: |
|
490 "\<And>r s n. (r * s::'a::{comm_monoid_mult,recpower} star) pow n |
|
491 = (r pow n) * (s pow n)" |
|
492 by transfer (rule power_mult_distrib) |
|
493 |
|
494 lemma hyperpow_two_le [simp]: |
|
495 "(0::'a::{recpower,ordered_ring_strict} star) \<le> r pow (1 + 1)" |
|
496 by (auto simp add: hyperpow_two zero_le_mult_iff) |
|
497 |
|
498 lemma hrabs_hyperpow_two [simp]: |
|
499 "abs(x pow (1 + 1)) = |
|
500 (x::'a::{recpower,ordered_ring_strict} star) pow (1 + 1)" |
|
501 by (simp only: abs_of_nonneg hyperpow_two_le) |
|
502 |
|
503 lemma hyperpow_two_hrabs [simp]: |
|
504 "abs(x::'a::{recpower,ordered_idom} star) pow (1 + 1) = x pow (1 + 1)" |
|
505 by (simp add: hyperpow_hrabs) |
|
506 |
|
507 text{*The precondition could be weakened to @{term "0\<le>x"}*} |
|
508 lemma hypreal_mult_less_mono: |
|
509 "[| u<v; x<y; (0::hypreal) < v; 0 < x |] ==> u*x < v* y" |
|
510 by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le) |
|
511 |
|
512 lemma hyperpow_two_gt_one: |
|
513 "\<And>r::'a::{recpower,ordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow (1 + 1)" |
|
514 by transfer (simp add: power_gt1) |
|
515 |
|
516 lemma hyperpow_two_ge_one: |
|
517 "\<And>r::'a::{recpower,ordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow (1 + 1)" |
|
518 by transfer (simp add: one_le_power) |
|
519 |
|
520 lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n" |
|
521 apply (rule_tac y = "1 pow n" in order_trans) |
|
522 apply (rule_tac [2] hyperpow_le, auto) |
|
523 done |
|
524 |
|
525 lemma hyperpow_minus_one2 [simp]: |
|
526 "!!n. -1 pow ((1 + 1)*n) = (1::hypreal)" |
|
527 by transfer (subst power_mult, simp) |
|
528 |
|
529 lemma hyperpow_less_le: |
|
530 "!!r n N. [|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n" |
|
531 by transfer (rule power_decreasing [OF order_less_imp_le]) |
|
532 |
|
533 lemma hyperpow_SHNat_le: |
|
534 "[| 0 \<le> r; r \<le> (1::hypreal); N \<in> HNatInfinite |] |
|
535 ==> ALL n: Nats. r pow N \<le> r pow n" |
|
536 by (auto intro!: hyperpow_less_le simp add: HNatInfinite_iff) |
|
537 |
|
538 lemma hyperpow_realpow: |
|
539 "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)" |
|
540 by transfer (rule refl) |
|
541 |
|
542 lemma hyperpow_SReal [simp]: |
|
543 "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals" |
|
544 by (simp add: Reals_eq_Standard) |
|
545 |
|
546 lemma hyperpow_zero_HNatInfinite [simp]: |
|
547 "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0" |
|
548 by (drule HNatInfinite_is_Suc, auto) |
|
549 |
|
550 lemma hyperpow_le_le: |
|
551 "[| (0::hypreal) \<le> r; r \<le> 1; n \<le> N |] ==> r pow N \<le> r pow n" |
|
552 apply (drule order_le_less [of n, THEN iffD1]) |
|
553 apply (auto intro: hyperpow_less_le) |
|
554 done |
|
555 |
|
556 lemma hyperpow_Suc_le_self2: |
|
557 "[| (0::hypreal) \<le> r; r < 1 |] ==> r pow (n + (1::hypnat)) \<le> r" |
|
558 apply (drule_tac n = " (1::hypnat) " in hyperpow_le_le) |
|
559 apply auto |
|
560 done |
|
561 |
|
562 lemma hyperpow_hypnat_of_nat: "\<And>x. x pow hypnat_of_nat n = x ^ n" |
|
563 by transfer (rule refl) |
|
564 |
|
565 lemma of_hypreal_hyperpow: |
|
566 "\<And>x n. of_hypreal (x pow n) = |
|
567 (of_hypreal x::'a::{real_algebra_1,recpower} star) pow n" |
|
568 by transfer (rule of_real_power) |
|
569 |
|
570 end |
|