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