40 syntax (HTML output) |
32 syntax (HTML output) |
41 omega :: hypreal ("\<omega>") |
33 omega :: hypreal ("\<omega>") |
42 epsilon :: hypreal ("\<epsilon>") |
34 epsilon :: hypreal ("\<epsilon>") |
43 |
35 |
44 |
36 |
45 subsection{*The Set of Naturals is not Finite*} |
|
46 |
|
47 (*** based on James' proof that the set of naturals is not finite ***) |
|
48 lemma finite_exhausts [rule_format]: |
|
49 "finite (A::nat set) --> (\<exists>n. \<forall>m. Suc (n + m) \<notin> A)" |
|
50 apply (rule impI) |
|
51 apply (erule_tac F = A in finite_induct) |
|
52 apply (blast, erule exE) |
|
53 apply (rule_tac x = "n + x" in exI) |
|
54 apply (rule allI, erule_tac x = "x + m" in allE) |
|
55 apply (auto simp add: add_ac) |
|
56 done |
|
57 |
|
58 lemma finite_not_covers [rule_format (no_asm)]: |
|
59 "finite (A :: nat set) --> (\<exists>n. n \<notin>A)" |
|
60 by (rule impI, drule finite_exhausts, blast) |
|
61 |
|
62 lemma not_finite_nat: "~ finite(UNIV:: nat set)" |
|
63 by (fast dest!: finite_exhausts) |
|
64 |
|
65 |
|
66 subsection{*Existence of Free Ultrafilter over the Naturals*} |
37 subsection{*Existence of Free Ultrafilter over the Naturals*} |
67 |
38 |
68 text{*Also, proof of various properties of @{term FreeUltrafilterNat}: |
39 text{*Also, proof of various properties of @{term FreeUltrafilterNat}: |
69 an arbitrary free ultrafilter*} |
40 an arbitrary free ultrafilter*} |
70 |
41 |
71 lemma FreeUltrafilterNat_Ex: "\<exists>U::nat set set. freeultrafilter U" |
42 lemma FreeUltrafilterNat_Ex: "\<exists>U::nat set set. freeultrafilter U" |
72 by (rule not_finite_nat [THEN freeultrafilter_Ex]) |
43 by (rule nat_infinite [THEN freeultrafilter_Ex]) |
73 |
44 |
74 lemma FreeUltrafilterNat_mem: "freeultrafilter FreeUltrafilterNat" |
45 lemma FreeUltrafilterNat_mem: "freeultrafilter FreeUltrafilterNat" |
75 apply (unfold FreeUltrafilterNat_def) |
46 apply (unfold FreeUltrafilterNat_def) |
76 apply (rule someI_ex) |
47 apply (rule someI_ex) |
77 apply (rule FreeUltrafilterNat_Ex) |
48 apply (rule FreeUltrafilterNat_Ex) |
181 lemma starrel_trans: |
152 lemma starrel_trans: |
182 "[|(x,y) \<in> starrel; (y,z) \<in> starrel|] ==> (x,z) \<in> starrel" |
153 "[|(x,y) \<in> starrel; (y,z) \<in> starrel|] ==> (x,z) \<in> starrel" |
183 by (simp add: starrel_def, ultra) |
154 by (simp add: starrel_def, ultra) |
184 |
155 |
185 lemma equiv_starrel: "equiv UNIV starrel" |
156 lemma equiv_starrel: "equiv UNIV starrel" |
186 by (rule StarType.equiv_starrel) |
157 by (rule StarDef.equiv_starrel) |
187 |
158 |
188 (* (starrel `` {x} = starrel `` {y}) = ((x,y) \<in> starrel) *) |
159 (* (starrel `` {x} = starrel `` {y}) = ((x,y) \<in> starrel) *) |
189 lemmas equiv_starrel_iff = |
160 lemmas equiv_starrel_iff = |
190 eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I, simp] |
161 eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I, simp] |
191 |
162 |
192 lemma starrel_in_hypreal [simp]: "starrel``{x}:star" |
163 lemma starrel_in_hypreal [simp]: "starrel``{x}:star" |
193 by (simp add: star_def starrel_def quotient_def, blast) |
164 by (simp add: star_def starrel_def quotient_def, blast) |
194 |
165 |
195 declare Abs_star_inject [simp] Abs_star_inverse [simp] |
166 declare Abs_star_inject [simp] Abs_star_inverse [simp] |
196 declare equiv_starrel [THEN eq_equiv_class_iff, simp] |
167 declare equiv_starrel [THEN eq_equiv_class_iff, simp] |
197 declare starrel_iff [iff] |
|
198 |
168 |
199 lemmas eq_starrelD = eq_equiv_class [OF _ equiv_starrel] |
169 lemmas eq_starrelD = eq_equiv_class [OF _ equiv_starrel] |
200 |
170 |
201 lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}" |
171 lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}" |
202 by (simp add: starrel_def) |
172 by (simp add: starrel_def) |
213 the Injection from @{typ real} to @{typ hypreal}*} |
183 the Injection from @{typ real} to @{typ hypreal}*} |
214 |
184 |
215 lemma inj_hypreal_of_real: "inj(hypreal_of_real)" |
185 lemma inj_hypreal_of_real: "inj(hypreal_of_real)" |
216 by (rule inj_onI, simp) |
186 by (rule inj_onI, simp) |
217 |
187 |
218 lemma eq_Abs_star: |
|
219 "(!!x. z = Abs_star(starrel``{x}) ==> P) ==> P" |
|
220 by (fold star_n_def, auto intro: star_cases) |
|
221 |
|
222 lemma Rep_star_star_n_iff [simp]: |
188 lemma Rep_star_star_n_iff [simp]: |
223 "(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)" |
189 "(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)" |
224 by (simp add: star_n_def) |
190 by (simp add: star_n_def) |
225 |
191 |
226 lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)" |
192 lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)" |
227 by simp |
193 by simp |
228 |
194 |
229 subsection{*Hyperreal Addition*} |
195 subsection{* Properties of @{term star_n} *} |
230 |
196 |
231 lemma star_n_add: |
197 lemma star_n_add: |
232 "star_n X + star_n Y = star_n (%n. X n + Y n)" |
198 "star_n X + star_n Y = star_n (%n. X n + Y n)" |
233 by (simp add: star_add_def Ifun2_of_def star_of_def Ifun_star_n) |
199 by (simp only: star_add_def starfun2_star_n) |
234 |
|
235 subsection{*Additive inverse on @{typ hypreal}*} |
|
236 |
200 |
237 lemma star_n_minus: |
201 lemma star_n_minus: |
238 "- star_n X = star_n (%n. -(X n))" |
202 "- star_n X = star_n (%n. -(X n))" |
239 by (simp add: star_minus_def Ifun_of_def star_of_def Ifun_star_n) |
203 by (simp only: star_minus_def starfun_star_n) |
240 |
204 |
241 lemma star_n_diff: |
205 lemma star_n_diff: |
242 "star_n X - star_n Y = star_n (%n. X n - Y n)" |
206 "star_n X - star_n Y = star_n (%n. X n - Y n)" |
243 by (simp add: star_diff_def Ifun2_of_def star_of_def Ifun_star_n) |
207 by (simp only: star_diff_def starfun2_star_n) |
244 |
|
245 |
|
246 subsection{*Hyperreal Multiplication*} |
|
247 |
208 |
248 lemma star_n_mult: |
209 lemma star_n_mult: |
249 "star_n X * star_n Y = star_n (%n. X n * Y n)" |
210 "star_n X * star_n Y = star_n (%n. X n * Y n)" |
250 by (simp add: star_mult_def Ifun2_of_def star_of_def Ifun_star_n) |
211 by (simp only: star_mult_def starfun2_star_n) |
251 |
|
252 |
|
253 subsection{*Multiplicative Inverse on @{typ hypreal} *} |
|
254 |
212 |
255 lemma star_n_inverse: |
213 lemma star_n_inverse: |
256 "inverse (star_n X) = star_n (%n. if X n = (0::real) then 0 else inverse(X n))" |
|
257 apply (simp add: star_inverse_def Ifun_of_def star_of_def Ifun_star_n) |
|
258 apply (rule_tac f=star_n in arg_cong) |
|
259 apply (rule ext) |
|
260 apply simp |
|
261 done |
|
262 |
|
263 lemma star_n_inverse2: |
|
264 "inverse (star_n X) = star_n (%n. inverse(X n))" |
214 "inverse (star_n X) = star_n (%n. inverse(X n))" |
265 by (simp add: star_inverse_def Ifun_of_def star_of_def Ifun_star_n) |
215 by (simp only: star_inverse_def starfun_star_n) |
266 |
|
267 |
|
268 subsection{*Properties of The @{text "\<le>"} Relation*} |
|
269 |
216 |
270 lemma star_n_le: |
217 lemma star_n_le: |
271 "star_n X \<le> star_n Y = |
218 "star_n X \<le> star_n Y = |
272 ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)" |
219 ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)" |
273 by (simp add: star_le_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n) |
220 by (simp only: star_le_def starP2_star_n) |
|
221 |
|
222 lemma star_n_less: |
|
223 "star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)" |
|
224 by (simp only: star_less_def starP2_star_n) |
|
225 |
|
226 lemma star_n_zero_num: "0 = star_n (%n. 0)" |
|
227 by (simp only: star_zero_def star_of_def) |
|
228 |
|
229 lemma star_n_one_num: "1 = star_n (%n. 1)" |
|
230 by (simp only: star_one_def star_of_def) |
|
231 |
|
232 lemma star_n_abs: |
|
233 "abs (star_n X) = star_n (%n. abs (X n))" |
|
234 by (simp only: star_abs_def starfun_star_n) |
|
235 |
|
236 subsection{*Misc Others*} |
274 |
237 |
275 lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y" |
238 lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y" |
276 by (auto) |
239 by (auto) |
277 |
|
278 subsection{*The Hyperreals Form an Ordered Field*} |
|
279 |
240 |
280 lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)" |
241 lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)" |
281 by auto |
242 by auto |
282 |
243 |
283 lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)" |
244 lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)" |
284 by auto |
245 by auto |
285 |
246 |
286 lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)" |
247 lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)" |
287 by auto |
248 by auto |
288 |
249 |
289 |
|
290 subsection{*Misc Others*} |
|
291 |
|
292 lemma star_n_less: |
|
293 "star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)" |
|
294 by (simp add: star_less_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n) |
|
295 |
|
296 lemma star_n_zero_num: "0 = star_n (%n. 0)" |
|
297 by (simp add: star_zero_def star_of_def) |
|
298 |
|
299 lemma star_n_one_num: "1 = star_n (%n. 1)" |
|
300 by (simp add: star_one_def star_of_def) |
|
301 |
|
302 lemma hypreal_omega_gt_zero [simp]: "0 < omega" |
250 lemma hypreal_omega_gt_zero [simp]: "0 < omega" |
303 apply (simp only: omega_def star_zero_def star_less_def star_of_def) |
251 by (simp add: omega_def star_n_zero_num star_n_less) |
304 apply (simp add: Ipred2_of_def star_of_def Ifun_star_n unstar_star_n) |
|
305 done |
|
306 |
|
307 lemma star_n_abs: |
|
308 "abs (star_n X) = star_n (%n. abs (X n))" |
|
309 by (simp add: star_abs_def Ifun_of_def star_of_def Ifun_star_n) |
|
310 |
252 |
311 subsection{*Existence of Infinite Hyperreal Number*} |
253 subsection{*Existence of Infinite Hyperreal Number*} |
312 |
254 |
313 text{*Existence of infinite number not corresponding to any real number. |
255 text{*Existence of infinite number not corresponding to any real number. |
314 Use assumption that member @{term FreeUltrafilterNat} is not finite.*} |
256 Use assumption that member @{term FreeUltrafilterNat} is not finite.*} |
355 lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0" |
297 lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0" |
356 by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff |
298 by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff |
357 del: star_of_zero) |
299 del: star_of_zero) |
358 |
300 |
359 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)" |
301 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)" |
360 apply (simp add: epsilon_def omega_def star_inverse_def) |
302 by (simp add: epsilon_def omega_def star_n_inverse) |
361 apply (simp add: Ifun_of_def star_of_def Ifun_star_n) |
|
362 done |
|
363 |
303 |
364 |
304 |
365 ML |
305 ML |
366 {* |
306 {* |
367 val omega_def = thm "omega_def"; |
307 val omega_def = thm "omega_def"; |
368 val epsilon_def = thm "epsilon_def"; |
308 val epsilon_def = thm "epsilon_def"; |
369 |
309 |
370 val finite_exhausts = thm "finite_exhausts"; |
|
371 val finite_not_covers = thm "finite_not_covers"; |
|
372 val not_finite_nat = thm "not_finite_nat"; |
|
373 val FreeUltrafilterNat_Ex = thm "FreeUltrafilterNat_Ex"; |
310 val FreeUltrafilterNat_Ex = thm "FreeUltrafilterNat_Ex"; |
374 val FreeUltrafilterNat_mem = thm "FreeUltrafilterNat_mem"; |
311 val FreeUltrafilterNat_mem = thm "FreeUltrafilterNat_mem"; |
375 val FreeUltrafilterNat_finite = thm "FreeUltrafilterNat_finite"; |
312 val FreeUltrafilterNat_finite = thm "FreeUltrafilterNat_finite"; |
376 val FreeUltrafilterNat_not_finite = thm "FreeUltrafilterNat_not_finite"; |
313 val FreeUltrafilterNat_not_finite = thm "FreeUltrafilterNat_not_finite"; |
377 val FreeUltrafilterNat_empty = thm "FreeUltrafilterNat_empty"; |
314 val FreeUltrafilterNat_empty = thm "FreeUltrafilterNat_empty"; |
392 val Abs_star_inverse = thm "Abs_star_inverse"; |
329 val Abs_star_inverse = thm "Abs_star_inverse"; |
393 val lemma_starrel_refl = thm "lemma_starrel_refl"; |
330 val lemma_starrel_refl = thm "lemma_starrel_refl"; |
394 val hypreal_empty_not_mem = thm "hypreal_empty_not_mem"; |
331 val hypreal_empty_not_mem = thm "hypreal_empty_not_mem"; |
395 val Rep_hypreal_nonempty = thm "Rep_hypreal_nonempty"; |
332 val Rep_hypreal_nonempty = thm "Rep_hypreal_nonempty"; |
396 val inj_hypreal_of_real = thm "inj_hypreal_of_real"; |
333 val inj_hypreal_of_real = thm "inj_hypreal_of_real"; |
397 val eq_Abs_star = thm "eq_Abs_star"; |
334 (* val eq_Abs_star = thm "eq_Abs_star"; *) |
398 val star_n_minus = thm "star_n_minus"; |
335 val star_n_minus = thm "star_n_minus"; |
399 val star_n_add = thm "star_n_add"; |
336 val star_n_add = thm "star_n_add"; |
400 val star_n_diff = thm "star_n_diff"; |
337 val star_n_diff = thm "star_n_diff"; |
401 val star_n_mult = thm "star_n_mult"; |
338 val star_n_mult = thm "star_n_mult"; |
402 val star_n_inverse = thm "star_n_inverse"; |
339 val star_n_inverse = thm "star_n_inverse"; |