author | haftmann |
Sat, 12 Mar 2016 22:04:52 +0100 | |
changeset 62597 | b3f2b8c906a6 |
parent 62479 | 716336f19aa9 |
child 63648 | f9f3006a5579 |
permissions | -rw-r--r-- |
62479 | 1 |
(* Title: HOL/Nonstandard_Analysis/HyperDef.thy |
2 |
Author: Jacques D. Fleuriot |
|
3 |
Copyright: 1998 University of Cambridge |
|
27468 | 4 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
5 |
*) |
|
6 |
||
61975 | 7 |
section\<open>Construction of Hyperreals Using Ultrafilters\<close> |
27468 | 8 |
|
9 |
theory HyperDef |
|
51525 | 10 |
imports Complex_Main HyperNat |
27468 | 11 |
begin |
12 |
||
42463 | 13 |
type_synonym hypreal = "real star" |
27468 | 14 |
|
15 |
abbreviation |
|
16 |
hypreal_of_real :: "real => real star" where |
|
17 |
"hypreal_of_real == star_of" |
|
18 |
||
19 |
abbreviation |
|
20 |
hypreal_of_hypnat :: "hypnat \<Rightarrow> hypreal" where |
|
21 |
"hypreal_of_hypnat \<equiv> of_hypnat" |
|
22 |
||
23 |
definition |
|
61981 | 24 |
omega :: hypreal ("\<omega>") where |
61975 | 25 |
\<comment> \<open>an infinite number \<open>= [<1,2,3,...>]\<close>\<close> |
61981 | 26 |
"\<omega> = star_n (\<lambda>n. real (Suc n))" |
27468 | 27 |
|
28 |
definition |
|
61981 | 29 |
epsilon :: hypreal ("\<epsilon>") where |
61975 | 30 |
\<comment> \<open>an infinitesimal number \<open>= [<1,1/2,1/3,...>]\<close>\<close> |
61981 | 31 |
"\<epsilon> = star_n (\<lambda>n. inverse (real (Suc n)))" |
27468 | 32 |
|
33 |
||
61975 | 34 |
subsection \<open>Real vector class instances\<close> |
27468 | 35 |
|
36 |
instantiation star :: (scaleR) scaleR |
|
37 |
begin |
|
38 |
||
39 |
definition |
|
37765 | 40 |
star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)" |
27468 | 41 |
|
42 |
instance .. |
|
43 |
||
44 |
end |
|
45 |
||
46 |
lemma Standard_scaleR [simp]: "x \<in> Standard \<Longrightarrow> scaleR r x \<in> Standard" |
|
47 |
by (simp add: star_scaleR_def) |
|
48 |
||
49 |
lemma star_of_scaleR [simp]: "star_of (scaleR r x) = scaleR r (star_of x)" |
|
50 |
by transfer (rule refl) |
|
51 |
||
52 |
instance star :: (real_vector) real_vector |
|
53 |
proof |
|
54 |
fix a b :: real |
|
55 |
show "\<And>x y::'a star. scaleR a (x + y) = scaleR a x + scaleR a y" |
|
56 |
by transfer (rule scaleR_right_distrib) |
|
57 |
show "\<And>x::'a star. scaleR (a + b) x = scaleR a x + scaleR b x" |
|
58 |
by transfer (rule scaleR_left_distrib) |
|
59 |
show "\<And>x::'a star. scaleR a (scaleR b x) = scaleR (a * b) x" |
|
60 |
by transfer (rule scaleR_scaleR) |
|
61 |
show "\<And>x::'a star. scaleR 1 x = x" |
|
62 |
by transfer (rule scaleR_one) |
|
63 |
qed |
|
64 |
||
65 |
instance star :: (real_algebra) real_algebra |
|
66 |
proof |
|
67 |
fix a :: real |
|
68 |
show "\<And>x y::'a star. scaleR a x * y = scaleR a (x * y)" |
|
69 |
by transfer (rule mult_scaleR_left) |
|
70 |
show "\<And>x y::'a star. x * scaleR a y = scaleR a (x * y)" |
|
71 |
by transfer (rule mult_scaleR_right) |
|
72 |
qed |
|
73 |
||
74 |
instance star :: (real_algebra_1) real_algebra_1 .. |
|
75 |
||
76 |
instance star :: (real_div_algebra) real_div_algebra .. |
|
77 |
||
27553 | 78 |
instance star :: (field_char_0) field_char_0 .. |
79 |
||
27468 | 80 |
instance star :: (real_field) real_field .. |
81 |
||
82 |
lemma star_of_real_def [transfer_unfold]: "of_real r = star_of (of_real r)" |
|
83 |
by (unfold of_real_def, transfer, rule refl) |
|
84 |
||
85 |
lemma Standard_of_real [simp]: "of_real r \<in> Standard" |
|
86 |
by (simp add: star_of_real_def) |
|
87 |
||
88 |
lemma star_of_of_real [simp]: "star_of (of_real r) = of_real r" |
|
89 |
by transfer (rule refl) |
|
90 |
||
91 |
lemma of_real_eq_star_of [simp]: "of_real = star_of" |
|
92 |
proof |
|
93 |
fix r :: real |
|
94 |
show "of_real r = star_of r" |
|
95 |
by transfer simp |
|
96 |
qed |
|
97 |
||
61070 | 98 |
lemma Reals_eq_Standard: "(\<real> :: hypreal set) = Standard" |
27468 | 99 |
by (simp add: Reals_def Standard_def) |
100 |
||
101 |
||
61975 | 102 |
subsection \<open>Injection from @{typ hypreal}\<close> |
27468 | 103 |
|
104 |
definition |
|
105 |
of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where |
|
37765 | 106 |
[transfer_unfold]: "of_hypreal = *f* of_real" |
27468 | 107 |
|
108 |
lemma Standard_of_hypreal [simp]: |
|
109 |
"r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard" |
|
110 |
by (simp add: of_hypreal_def) |
|
111 |
||
112 |
lemma of_hypreal_0 [simp]: "of_hypreal 0 = 0" |
|
113 |
by transfer (rule of_real_0) |
|
114 |
||
115 |
lemma of_hypreal_1 [simp]: "of_hypreal 1 = 1" |
|
116 |
by transfer (rule of_real_1) |
|
117 |
||
118 |
lemma of_hypreal_add [simp]: |
|
119 |
"\<And>x y. of_hypreal (x + y) = of_hypreal x + of_hypreal y" |
|
120 |
by transfer (rule of_real_add) |
|
121 |
||
122 |
lemma of_hypreal_minus [simp]: "\<And>x. of_hypreal (- x) = - of_hypreal x" |
|
123 |
by transfer (rule of_real_minus) |
|
124 |
||
125 |
lemma of_hypreal_diff [simp]: |
|
126 |
"\<And>x y. of_hypreal (x - y) = of_hypreal x - of_hypreal y" |
|
127 |
by transfer (rule of_real_diff) |
|
128 |
||
129 |
lemma of_hypreal_mult [simp]: |
|
130 |
"\<And>x y. of_hypreal (x * y) = of_hypreal x * of_hypreal y" |
|
131 |
by transfer (rule of_real_mult) |
|
132 |
||
133 |
lemma of_hypreal_inverse [simp]: |
|
134 |
"\<And>x. of_hypreal (inverse x) = |
|
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59582
diff
changeset
|
135 |
inverse (of_hypreal x :: 'a::{real_div_algebra, division_ring} star)" |
27468 | 136 |
by transfer (rule of_real_inverse) |
137 |
||
138 |
lemma of_hypreal_divide [simp]: |
|
139 |
"\<And>x y. of_hypreal (x / y) = |
|
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59582
diff
changeset
|
140 |
(of_hypreal x / of_hypreal y :: 'a::{real_field, field} star)" |
27468 | 141 |
by transfer (rule of_real_divide) |
142 |
||
143 |
lemma of_hypreal_eq_iff [simp]: |
|
144 |
"\<And>x y. (of_hypreal x = of_hypreal y) = (x = y)" |
|
145 |
by transfer (rule of_real_eq_iff) |
|
146 |
||
147 |
lemma of_hypreal_eq_0_iff [simp]: |
|
148 |
"\<And>x. (of_hypreal x = 0) = (x = 0)" |
|
149 |
by transfer (rule of_real_eq_0_iff) |
|
150 |
||
151 |
||
61975 | 152 |
subsection\<open>Properties of @{term starrel}\<close> |
27468 | 153 |
|
154 |
lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}" |
|
155 |
by (simp add: starrel_def) |
|
156 |
||
157 |
lemma starrel_in_hypreal [simp]: "starrel``{x}:star" |
|
158 |
by (simp add: star_def starrel_def quotient_def, blast) |
|
159 |
||
160 |
declare Abs_star_inject [simp] Abs_star_inverse [simp] |
|
161 |
declare equiv_starrel [THEN eq_equiv_class_iff, simp] |
|
162 |
||
61975 | 163 |
subsection\<open>@{term hypreal_of_real}: |
164 |
the Injection from @{typ real} to @{typ hypreal}\<close> |
|
27468 | 165 |
|
166 |
lemma inj_star_of: "inj star_of" |
|
167 |
by (rule inj_onI, simp) |
|
168 |
||
169 |
lemma mem_Rep_star_iff: "(X \<in> Rep_star x) = (x = star_n X)" |
|
170 |
by (cases x, simp add: star_n_def) |
|
171 |
||
172 |
lemma Rep_star_star_n_iff [simp]: |
|
60041 | 173 |
"(X \<in> Rep_star (star_n Y)) = (eventually (\<lambda>n. Y n = X n) \<U>)" |
27468 | 174 |
by (simp add: star_n_def) |
175 |
||
176 |
lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)" |
|
177 |
by simp |
|
178 |
||
61975 | 179 |
subsection\<open>Properties of @{term star_n}\<close> |
27468 | 180 |
|
181 |
lemma star_n_add: |
|
182 |
"star_n X + star_n Y = star_n (%n. X n + Y n)" |
|
183 |
by (simp only: star_add_def starfun2_star_n) |
|
184 |
||
185 |
lemma star_n_minus: |
|
186 |
"- star_n X = star_n (%n. -(X n))" |
|
187 |
by (simp only: star_minus_def starfun_star_n) |
|
188 |
||
189 |
lemma star_n_diff: |
|
190 |
"star_n X - star_n Y = star_n (%n. X n - Y n)" |
|
191 |
by (simp only: star_diff_def starfun2_star_n) |
|
192 |
||
193 |
lemma star_n_mult: |
|
194 |
"star_n X * star_n Y = star_n (%n. X n * Y n)" |
|
195 |
by (simp only: star_mult_def starfun2_star_n) |
|
196 |
||
197 |
lemma star_n_inverse: |
|
198 |
"inverse (star_n X) = star_n (%n. inverse(X n))" |
|
199 |
by (simp only: star_inverse_def starfun_star_n) |
|
200 |
||
201 |
lemma star_n_le: |
|
60041 | 202 |
"star_n X \<le> star_n Y = (eventually (\<lambda>n. X n \<le> Y n) FreeUltrafilterNat)" |
27468 | 203 |
by (simp only: star_le_def starP2_star_n) |
204 |
||
205 |
lemma star_n_less: |
|
60041 | 206 |
"star_n X < star_n Y = (eventually (\<lambda>n. X n < Y n) FreeUltrafilterNat)" |
27468 | 207 |
by (simp only: star_less_def starP2_star_n) |
208 |
||
209 |
lemma star_n_zero_num: "0 = star_n (%n. 0)" |
|
210 |
by (simp only: star_zero_def star_of_def) |
|
211 |
||
212 |
lemma star_n_one_num: "1 = star_n (%n. 1)" |
|
213 |
by (simp only: star_one_def star_of_def) |
|
214 |
||
61945 | 215 |
lemma star_n_abs: "\<bar>star_n X\<bar> = star_n (%n. \<bar>X n\<bar>)" |
27468 | 216 |
by (simp only: star_abs_def starfun_star_n) |
217 |
||
61981 | 218 |
lemma hypreal_omega_gt_zero [simp]: "0 < \<omega>" |
27468 | 219 |
by (simp add: omega_def star_n_zero_num star_n_less) |
220 |
||
61975 | 221 |
subsection\<open>Existence of Infinite Hyperreal Number\<close> |
27468 | 222 |
|
61975 | 223 |
text\<open>Existence of infinite number not corresponding to any real number. |
224 |
Use assumption that member @{term FreeUltrafilterNat} is not finite.\<close> |
|
27468 | 225 |
|
226 |
||
61975 | 227 |
text\<open>A few lemmas first\<close> |
27468 | 228 |
|
61806
d2e62ae01cd8
Cauchy's integral formula for circles. Starting to fix eventually_mono.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset
|
229 |
lemma lemma_omega_empty_singleton_disj: |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61378
diff
changeset
|
230 |
"{n::nat. x = real n} = {} \<or> (\<exists>y. {n::nat. x = real n} = {y})" |
27468 | 231 |
by force |
232 |
||
233 |
lemma lemma_finite_omega_set: "finite {n::nat. x = real n}" |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61378
diff
changeset
|
234 |
using lemma_omega_empty_singleton_disj [of x] by auto |
27468 | 235 |
|
56217
dc429a5b13c4
Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents:
55911
diff
changeset
|
236 |
lemma not_ex_hypreal_of_real_eq_omega: |
61981 | 237 |
"~ (\<exists>x. hypreal_of_real x = \<omega>)" |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61378
diff
changeset
|
238 |
apply (simp add: omega_def star_of_def star_n_eq_iff) |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61378
diff
changeset
|
239 |
apply clarify |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61378
diff
changeset
|
240 |
apply (rule_tac x2="x-1" in lemma_finite_omega_set [THEN FreeUltrafilterNat.finite, THEN notE]) |
61810 | 241 |
apply (erule eventually_mono) |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61378
diff
changeset
|
242 |
apply auto |
27468 | 243 |
done |
244 |
||
61981 | 245 |
lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> \<omega>" |
27468 | 246 |
by (insert not_ex_hypreal_of_real_eq_omega, auto) |
247 |
||
61975 | 248 |
text\<open>Existence of infinitesimal number also not corresponding to any |
249 |
real number\<close> |
|
27468 | 250 |
|
251 |
lemma lemma_epsilon_empty_singleton_disj: |
|
56217
dc429a5b13c4
Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents:
55911
diff
changeset
|
252 |
"{n::nat. x = inverse(real(Suc n))} = {} | |
27468 | 253 |
(\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})" |
254 |
by auto |
|
255 |
||
256 |
lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}" |
|
257 |
by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto) |
|
258 |
||
61981 | 259 |
lemma not_ex_hypreal_of_real_eq_epsilon: "~ (\<exists>x. hypreal_of_real x = \<epsilon>)" |
27468 | 260 |
by (auto simp add: epsilon_def star_of_def star_n_eq_iff |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61378
diff
changeset
|
261 |
lemma_finite_epsilon_set [THEN FreeUltrafilterNat.finite] simp del: of_nat_Suc) |
27468 | 262 |
|
61981 | 263 |
lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> \<epsilon>" |
27468 | 264 |
by (insert not_ex_hypreal_of_real_eq_epsilon, auto) |
265 |
||
61981 | 266 |
lemma hypreal_epsilon_not_zero: "\<epsilon> \<noteq> 0" |
60041 | 267 |
by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff FreeUltrafilterNat.proper |
27468 | 268 |
del: star_of_zero) |
269 |
||
61981 | 270 |
lemma hypreal_epsilon_inverse_omega: "\<epsilon> = inverse \<omega>" |
27468 | 271 |
by (simp add: epsilon_def omega_def star_n_inverse) |
272 |
||
61981 | 273 |
lemma hypreal_epsilon_gt_zero: "0 < \<epsilon>" |
27468 | 274 |
by (simp add: hypreal_epsilon_inverse_omega) |
275 |
||
61975 | 276 |
subsection\<open>Absolute Value Function for the Hyperreals\<close> |
27468 | 277 |
|
61945 | 278 |
lemma hrabs_add_less: "[| \<bar>x\<bar> < r; \<bar>y\<bar> < s |] ==> \<bar>x + y\<bar> < r + (s::hypreal)" |
62390 | 279 |
by (simp add: abs_if split: if_split_asm) |
27468 | 280 |
|
61945 | 281 |
lemma hrabs_less_gt_zero: "\<bar>x\<bar> < r ==> (0::hypreal) < r" |
27468 | 282 |
by (blast intro!: order_le_less_trans abs_ge_zero) |
283 |
||
61945 | 284 |
lemma hrabs_disj: "\<bar>x\<bar> = (x::'a::abs_if) \<or> \<bar>x\<bar> = -x" |
27468 | 285 |
by (simp add: abs_if) |
286 |
||
61945 | 287 |
lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = \<bar>x + - z\<bar> ==> y = z | x = y" |
62390 | 288 |
by (simp add: abs_if split add: if_split_asm) |
27468 | 289 |
|
290 |
||
61975 | 291 |
subsection\<open>Embedding the Naturals into the Hyperreals\<close> |
27468 | 292 |
|
293 |
abbreviation |
|
294 |
hypreal_of_nat :: "nat => hypreal" where |
|
295 |
"hypreal_of_nat == of_nat" |
|
296 |
||
297 |
lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}" |
|
298 |
by (simp add: Nats_def image_def) |
|
299 |
||
300 |
(*------------------------------------------------------------*) |
|
301 |
(* naturals embedded in hyperreals *) |
|
302 |
(* is a hyperreal c.f. NS extension *) |
|
303 |
(*------------------------------------------------------------*) |
|
304 |
||
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61378
diff
changeset
|
305 |
lemma hypreal_of_nat: "hypreal_of_nat m = star_n (%n. real m)" |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61378
diff
changeset
|
306 |
by (simp add: star_of_def [symmetric]) |
27468 | 307 |
|
61975 | 308 |
declaration \<open> |
31100 | 309 |
K (Lin_Arith.add_inj_thms [@{thm star_of_le} RS iffD2, |
310 |
@{thm star_of_less} RS iffD2, @{thm star_of_eq} RS iffD2] |
|
311 |
#> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one}, |
|
55911
d00023bd3554
remove simp rules made redundant by the replacement of neg_numeral with negated numerals
huffman
parents:
54489
diff
changeset
|
312 |
@{thm star_of_numeral}, @{thm star_of_add}, |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45605
diff
changeset
|
313 |
@{thm star_of_minus}, @{thm star_of_diff}, @{thm star_of_mult}] |
43595 | 314 |
#> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"})) |
61975 | 315 |
\<close> |
27468 | 316 |
|
43595 | 317 |
simproc_setup fast_arith_hypreal ("(m::hypreal) < n" | "(m::hypreal) <= n" | "(m::hypreal) = n") = |
61975 | 318 |
\<open>K Lin_Arith.simproc\<close> |
43595 | 319 |
|
27468 | 320 |
|
61975 | 321 |
subsection \<open>Exponentials on the Hyperreals\<close> |
27468 | 322 |
|
323 |
lemma hpowr_0 [simp]: "r ^ 0 = (1::hypreal)" |
|
324 |
by (rule power_0) |
|
325 |
||
326 |
lemma hpowr_Suc [simp]: "r ^ (Suc n) = (r::hypreal) * (r ^ n)" |
|
327 |
by (rule power_Suc) |
|
328 |
||
329 |
lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r" |
|
330 |
by simp |
|
331 |
||
332 |
lemma hrealpow_two_le [simp]: "(0::hypreal) \<le> r ^ Suc (Suc 0)" |
|
333 |
by (auto simp add: zero_le_mult_iff) |
|
334 |
||
335 |
lemma hrealpow_two_le_add_order [simp]: |
|
336 |
"(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)" |
|
337 |
by (simp only: hrealpow_two_le add_nonneg_nonneg) |
|
338 |
||
339 |
lemma hrealpow_two_le_add_order2 [simp]: |
|
340 |
"(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)" |
|
341 |
by (simp only: hrealpow_two_le add_nonneg_nonneg) |
|
342 |
||
343 |
lemma hypreal_add_nonneg_eq_0_iff: |
|
344 |
"[| 0 \<le> x; 0 \<le> y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))" |
|
345 |
by arith |
|
346 |
||
347 |
||
61975 | 348 |
text\<open>FIXME: DELETE THESE\<close> |
27468 | 349 |
lemma hypreal_three_squares_add_zero_iff: |
350 |
"(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))" |
|
351 |
apply (simp only: zero_le_square add_nonneg_nonneg hypreal_add_nonneg_eq_0_iff, auto) |
|
352 |
done |
|
353 |
||
354 |
lemma hrealpow_three_squares_add_zero_iff [simp]: |
|
56217
dc429a5b13c4
Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents:
55911
diff
changeset
|
355 |
"(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = |
27468 | 356 |
(x = 0 & y = 0 & z = 0)" |
357 |
by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two) |
|
358 |
||
359 |
(*FIXME: This and RealPow.abs_realpow_two should be replaced by an abstract |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset
|
360 |
result proved in Rings or Fields*) |
61945 | 361 |
lemma hrabs_hrealpow_two [simp]: "\<bar>x ^ Suc (Suc 0)\<bar> = (x::hypreal) ^ Suc (Suc 0)" |
27468 | 362 |
by (simp add: abs_mult) |
363 |
||
364 |
lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n" |
|
365 |
by (insert power_increasing [of 0 n "2::hypreal"], simp) |
|
366 |
||
367 |
lemma hrealpow: |
|
368 |
"star_n X ^ m = star_n (%n. (X n::real) ^ m)" |
|
369 |
apply (induct_tac "m") |
|
370 |
apply (auto simp add: star_n_one_num star_n_mult power_0) |
|
371 |
done |
|
372 |
||
373 |
lemma hrealpow_sum_square_expand: |
|
374 |
"(x + (y::hypreal)) ^ Suc (Suc 0) = |
|
375 |
x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y" |
|
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
47195
diff
changeset
|
376 |
by (simp add: distrib_left distrib_right) |
27468 | 377 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45605
diff
changeset
|
378 |
lemma power_hypreal_of_real_numeral: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45605
diff
changeset
|
379 |
"(numeral v :: hypreal) ^ n = hypreal_of_real ((numeral v) ^ n)" |
27468 | 380 |
by simp |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45605
diff
changeset
|
381 |
declare power_hypreal_of_real_numeral [of _ "numeral w", simp] for w |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45605
diff
changeset
|
382 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45605
diff
changeset
|
383 |
lemma power_hypreal_of_real_neg_numeral: |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
51525
diff
changeset
|
384 |
"(- numeral v :: hypreal) ^ n = hypreal_of_real ((- numeral v) ^ n)" |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45605
diff
changeset
|
385 |
by simp |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45605
diff
changeset
|
386 |
declare power_hypreal_of_real_neg_numeral [of _ "numeral w", simp] for w |
27468 | 387 |
(* |
388 |
lemma hrealpow_HFinite: |
|
31017 | 389 |
fixes x :: "'a::{real_normed_algebra,power} star" |
27468 | 390 |
shows "x \<in> HFinite ==> x ^ n \<in> HFinite" |
391 |
apply (induct_tac "n") |
|
392 |
apply (auto simp add: power_Suc intro: HFinite_mult) |
|
393 |
done |
|
394 |
*) |
|
395 |
||
61975 | 396 |
subsection\<open>Powers with Hypernatural Exponents\<close> |
27468 | 397 |
|
31001 | 398 |
definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where |
37765 | 399 |
hyperpow_def [transfer_unfold]: "R pow N = ( *f2* op ^) R N" |
27468 | 400 |
(* hypernatural powers of hyperreals *) |
401 |
||
402 |
lemma Standard_hyperpow [simp]: |
|
403 |
"\<lbrakk>r \<in> Standard; n \<in> Standard\<rbrakk> \<Longrightarrow> r pow n \<in> Standard" |
|
404 |
unfolding hyperpow_def by simp |
|
405 |
||
406 |
lemma hyperpow: "star_n X pow star_n Y = star_n (%n. X n ^ Y n)" |
|
407 |
by (simp add: hyperpow_def starfun2_star_n) |
|
408 |
||
409 |
lemma hyperpow_zero [simp]: |
|
31017 | 410 |
"\<And>n. (0::'a::{power,semiring_0} star) pow (n + (1::hypnat)) = 0" |
27468 | 411 |
by transfer simp |
412 |
||
413 |
lemma hyperpow_not_zero: |
|
31017 | 414 |
"\<And>r n. r \<noteq> (0::'a::{field} star) ==> r pow n \<noteq> 0" |
60867 | 415 |
by transfer (rule power_not_zero) |
27468 | 416 |
|
417 |
lemma hyperpow_inverse: |
|
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59582
diff
changeset
|
418 |
"\<And>r n. r \<noteq> (0::'a::field star) |
27468 | 419 |
\<Longrightarrow> inverse (r pow n) = (inverse r) pow n" |
60867 | 420 |
by transfer (rule power_inverse [symmetric]) |
56217
dc429a5b13c4
Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents:
55911
diff
changeset
|
421 |
|
27468 | 422 |
lemma hyperpow_hrabs: |
61945 | 423 |
"\<And>r n. \<bar>r::'a::{linordered_idom} star\<bar> pow n = \<bar>r pow n\<bar>" |
27468 | 424 |
by transfer (rule power_abs [symmetric]) |
425 |
||
426 |
lemma hyperpow_add: |
|
31017 | 427 |
"\<And>r n m. (r::'a::monoid_mult star) pow (n + m) = (r pow n) * (r pow m)" |
27468 | 428 |
by transfer (rule power_add) |
429 |
||
430 |
lemma hyperpow_one [simp]: |
|
31001 | 431 |
"\<And>r. (r::'a::monoid_mult star) pow (1::hypnat) = r" |
27468 | 432 |
by transfer (rule power_one_right) |
433 |
||
434 |
lemma hyperpow_two: |
|
45542
4849dbe6e310
HOL-NSA: add number_semiring instance, reformulate several lemmas using '2' instead of '1+1'
huffman
parents:
43595
diff
changeset
|
435 |
"\<And>r. (r::'a::monoid_mult star) pow (2::hypnat) = r * r" |
4849dbe6e310
HOL-NSA: add number_semiring instance, reformulate several lemmas using '2' instead of '1+1'
huffman
parents:
43595
diff
changeset
|
436 |
by transfer (rule power2_eq_square) |
27468 | 437 |
|
438 |
lemma hyperpow_gt_zero: |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
31101
diff
changeset
|
439 |
"\<And>r n. (0::'a::{linordered_semidom} star) < r \<Longrightarrow> 0 < r pow n" |
27468 | 440 |
by transfer (rule zero_less_power) |
441 |
||
442 |
lemma hyperpow_ge_zero: |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
31101
diff
changeset
|
443 |
"\<And>r n. (0::'a::{linordered_semidom} star) \<le> r \<Longrightarrow> 0 \<le> r pow n" |
27468 | 444 |
by transfer (rule zero_le_power) |
445 |
||
446 |
lemma hyperpow_le: |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
31101
diff
changeset
|
447 |
"\<And>x y n. \<lbrakk>(0::'a::{linordered_semidom} star) < x; x \<le> y\<rbrakk> |
27468 | 448 |
\<Longrightarrow> x pow n \<le> y pow n" |
449 |
by transfer (rule power_mono [OF _ order_less_imp_le]) |
|
450 |
||
451 |
lemma hyperpow_eq_one [simp]: |
|
31017 | 452 |
"\<And>n. 1 pow n = (1::'a::monoid_mult star)" |
27468 | 453 |
by transfer (rule power_one) |
454 |
||
55911
d00023bd3554
remove simp rules made redundant by the replacement of neg_numeral with negated numerals
huffman
parents:
54489
diff
changeset
|
455 |
lemma hrabs_hyperpow_minus [simp]: |
61945 | 456 |
"\<And>(a::'a::{linordered_idom} star) n. \<bar>(-a) pow n\<bar> = \<bar>a pow n\<bar>" |
55911
d00023bd3554
remove simp rules made redundant by the replacement of neg_numeral with negated numerals
huffman
parents:
54489
diff
changeset
|
457 |
by transfer (rule abs_power_minus) |
27468 | 458 |
|
459 |
lemma hyperpow_mult: |
|
31017 | 460 |
"\<And>r s n. (r * s::'a::{comm_monoid_mult} star) pow n |
27468 | 461 |
= (r pow n) * (s pow n)" |
462 |
by transfer (rule power_mult_distrib) |
|
463 |
||
464 |
lemma hyperpow_two_le [simp]: |
|
45542
4849dbe6e310
HOL-NSA: add number_semiring instance, reformulate several lemmas using '2' instead of '1+1'
huffman
parents:
43595
diff
changeset
|
465 |
"\<And>r. (0::'a::{monoid_mult,linordered_ring_strict} star) \<le> r pow 2" |
27468 | 466 |
by (auto simp add: hyperpow_two zero_le_mult_iff) |
467 |
||
468 |
lemma hrabs_hyperpow_two [simp]: |
|
61945 | 469 |
"\<bar>x pow 2\<bar> = |
45542
4849dbe6e310
HOL-NSA: add number_semiring instance, reformulate several lemmas using '2' instead of '1+1'
huffman
parents:
43595
diff
changeset
|
470 |
(x::'a::{monoid_mult,linordered_ring_strict} star) pow 2" |
27468 | 471 |
by (simp only: abs_of_nonneg hyperpow_two_le) |
472 |
||
473 |
lemma hyperpow_two_hrabs [simp]: |
|
61945 | 474 |
"\<bar>x::'a::{linordered_idom} star\<bar> pow 2 = x pow 2" |
27468 | 475 |
by (simp add: hyperpow_hrabs) |
476 |
||
61975 | 477 |
text\<open>The precondition could be weakened to @{term "0\<le>x"}\<close> |
27468 | 478 |
lemma hypreal_mult_less_mono: |
479 |
"[| u<v; x<y; (0::hypreal) < v; 0 < x |] ==> u*x < v* y" |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset
|
480 |
by (simp add: mult_strict_mono order_less_imp_le) |
27468 | 481 |
|
482 |
lemma hyperpow_two_gt_one: |
|
45542
4849dbe6e310
HOL-NSA: add number_semiring instance, reformulate several lemmas using '2' instead of '1+1'
huffman
parents:
43595
diff
changeset
|
483 |
"\<And>r::'a::{linordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow 2" |
4849dbe6e310
HOL-NSA: add number_semiring instance, reformulate several lemmas using '2' instead of '1+1'
huffman
parents:
43595
diff
changeset
|
484 |
by transfer simp |
27468 | 485 |
|
486 |
lemma hyperpow_two_ge_one: |
|
45542
4849dbe6e310
HOL-NSA: add number_semiring instance, reformulate several lemmas using '2' instead of '1+1'
huffman
parents:
43595
diff
changeset
|
487 |
"\<And>r::'a::{linordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow 2" |
4849dbe6e310
HOL-NSA: add number_semiring instance, reformulate several lemmas using '2' instead of '1+1'
huffman
parents:
43595
diff
changeset
|
488 |
by transfer (rule one_le_power) |
27468 | 489 |
|
490 |
lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n" |
|
491 |
apply (rule_tac y = "1 pow n" in order_trans) |
|
492 |
apply (rule_tac [2] hyperpow_le, auto) |
|
493 |
done |
|
494 |
||
495 |
lemma hyperpow_minus_one2 [simp]: |
|
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
56225
diff
changeset
|
496 |
"\<And>n. (- 1) pow (2*n) = (1::hypreal)" |
47195
836bf25fb70f
remove duplicate lemmas power_m1_{even,odd} in favor of power_minus1_{even,odd}
huffman
parents:
47108
diff
changeset
|
497 |
by transfer (rule power_minus1_even) |
27468 | 498 |
|
499 |
lemma hyperpow_less_le: |
|
500 |
"!!r n N. [|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n" |
|
501 |
by transfer (rule power_decreasing [OF order_less_imp_le]) |
|
502 |
||
503 |
lemma hyperpow_SHNat_le: |
|
504 |
"[| 0 \<le> r; r \<le> (1::hypreal); N \<in> HNatInfinite |] |
|
505 |
==> ALL n: Nats. r pow N \<le> r pow n" |
|
506 |
by (auto intro!: hyperpow_less_le simp add: HNatInfinite_iff) |
|
507 |
||
508 |
lemma hyperpow_realpow: |
|
509 |
"(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)" |
|
510 |
by transfer (rule refl) |
|
511 |
||
512 |
lemma hyperpow_SReal [simp]: |
|
61070 | 513 |
"(hypreal_of_real r) pow (hypnat_of_nat n) \<in> \<real>" |
27468 | 514 |
by (simp add: Reals_eq_Standard) |
515 |
||
516 |
lemma hyperpow_zero_HNatInfinite [simp]: |
|
517 |
"N \<in> HNatInfinite ==> (0::hypreal) pow N = 0" |
|
518 |
by (drule HNatInfinite_is_Suc, auto) |
|
519 |
||
520 |
lemma hyperpow_le_le: |
|
521 |
"[| (0::hypreal) \<le> r; r \<le> 1; n \<le> N |] ==> r pow N \<le> r pow n" |
|
522 |
apply (drule order_le_less [of n, THEN iffD1]) |
|
523 |
apply (auto intro: hyperpow_less_le) |
|
524 |
done |
|
525 |
||
526 |
lemma hyperpow_Suc_le_self2: |
|
527 |
"[| (0::hypreal) \<le> r; r < 1 |] ==> r pow (n + (1::hypnat)) \<le> r" |
|
528 |
apply (drule_tac n = " (1::hypnat) " in hyperpow_le_le) |
|
529 |
apply auto |
|
530 |
done |
|
531 |
||
532 |
lemma hyperpow_hypnat_of_nat: "\<And>x. x pow hypnat_of_nat n = x ^ n" |
|
533 |
by transfer (rule refl) |
|
534 |
||
535 |
lemma of_hypreal_hyperpow: |
|
536 |
"\<And>x n. of_hypreal (x pow n) = |
|
31017 | 537 |
(of_hypreal x::'a::{real_algebra_1} star) pow n" |
27468 | 538 |
by transfer (rule of_real_power) |
539 |
||
540 |
end |