8 |
8 |
9 theory Star |
9 theory Star |
10 imports NSA |
10 imports NSA |
11 begin |
11 begin |
12 |
12 |
13 constdefs |
13 definition |
14 (* internal sets *) |
14 (* internal sets *) |
15 starset_n :: "(nat => 'a set) => 'a star set" ("*sn* _" [80] 80) |
15 starset_n :: "(nat => 'a set) => 'a star set" ("*sn* _" [80] 80) |
16 "*sn* As == Iset (star_n As)" |
16 "*sn* As = Iset (star_n As)" |
17 |
17 |
18 InternalSets :: "'a star set set" |
18 InternalSets :: "'a star set set" |
19 "InternalSets == {X. \<exists>As. X = *sn* As}" |
19 "InternalSets = {X. \<exists>As. X = *sn* As}" |
20 |
20 |
21 (* nonstandard extension of function *) |
21 (* nonstandard extension of function *) |
22 is_starext :: "['a star => 'a star, 'a => 'a] => bool" |
22 is_starext :: "['a star => 'a star, 'a => 'a] => bool" |
23 "is_starext F f == (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y). |
23 "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y). |
24 ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))" |
24 ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))" |
25 (* internal functions *) |
25 (* internal functions *) |
26 starfun_n :: "(nat => ('a => 'b)) => 'a star => 'b star" |
26 starfun_n :: "(nat => ('a => 'b)) => 'a star => 'b star" ("*fn* _" [80] 80) |
27 ("*fn* _" [80] 80) |
27 "*fn* F = Ifun (star_n F)" |
28 "*fn* F == Ifun (star_n F)" |
28 |
29 |
29 InternalFuns :: "('a star => 'b star) set" |
30 InternalFuns :: "('a star => 'b star) set" |
30 "InternalFuns = {X. \<exists>F. X = *fn* F}" |
31 "InternalFuns == {X. \<exists>F. X = *fn* F}" |
|
32 |
|
33 |
31 |
34 |
32 |
35 (*-------------------------------------------------------- |
33 (*-------------------------------------------------------- |
36 Preamble - Pulling "EX" over "ALL" |
34 Preamble - Pulling "EX" over "ALL" |
37 ---------------------------------------------------------*) |
35 ---------------------------------------------------------*) |
351 apply (rule ext, rule ccontr) |
349 apply (rule ext, rule ccontr) |
352 apply (drule_tac x = "star_n (%n. xa)" in fun_cong) |
350 apply (drule_tac x = "star_n (%n. xa)" in fun_cong) |
353 apply (auto simp add: starfun star_n_eq_iff) |
351 apply (auto simp add: starfun star_n_eq_iff) |
354 done |
352 done |
355 |
353 |
356 ML |
|
357 {* |
|
358 val starset_n_def = thm"starset_n_def"; |
|
359 val InternalSets_def = thm"InternalSets_def"; |
|
360 val is_starext_def = thm"is_starext_def"; |
|
361 val starfun_n_def = thm"starfun_n_def"; |
|
362 val InternalFuns_def = thm"InternalFuns_def"; |
|
363 |
|
364 val no_choice = thm "no_choice"; |
|
365 val STAR_UNIV_set = thm "STAR_UNIV_set"; |
|
366 val STAR_empty_set = thm "STAR_empty_set"; |
|
367 val STAR_Un = thm "STAR_Un"; |
|
368 val STAR_Int = thm "STAR_Int"; |
|
369 val STAR_Compl = thm "STAR_Compl"; |
|
370 val STAR_mem_Compl = thm "STAR_mem_Compl"; |
|
371 val STAR_diff = thm "STAR_diff"; |
|
372 val STAR_subset = thm "STAR_subset"; |
|
373 val STAR_mem = thm "STAR_mem"; |
|
374 val STAR_star_of_image_subset = thm "STAR_star_of_image_subset"; |
|
375 val STAR_hypreal_of_real_Int = thm "STAR_hypreal_of_real_Int"; |
|
376 val STAR_real_seq_to_hypreal = thm "STAR_real_seq_to_hypreal"; |
|
377 val STAR_singleton = thm "STAR_singleton"; |
|
378 val STAR_not_mem = thm "STAR_not_mem"; |
|
379 val STAR_subset_closed = thm "STAR_subset_closed"; |
|
380 val starset_n_starset = thm "starset_n_starset"; |
|
381 val starfun_n_starfun = thm "starfun_n_starfun"; |
|
382 val hrabs_is_starext_rabs = thm "hrabs_is_starext_rabs"; |
|
383 val Rep_star_FreeUltrafilterNat = thm "Rep_star_FreeUltrafilterNat"; |
|
384 val starfun = thm "starfun"; |
|
385 val starfun_mult = thm "starfun_mult"; |
|
386 val starfun_add = thm "starfun_add"; |
|
387 val starfun_minus = thm "starfun_minus"; |
|
388 val starfun_add_minus = thm "starfun_add_minus"; |
|
389 val starfun_diff = thm "starfun_diff"; |
|
390 val starfun_o2 = thm "starfun_o2"; |
|
391 val starfun_o = thm "starfun_o"; |
|
392 val starfun_const_fun = thm "starfun_const_fun"; |
|
393 val starfun_Idfun_approx = thm "starfun_Idfun_approx"; |
|
394 val starfun_Id = thm "starfun_Id"; |
|
395 val is_starext_starfun = thm "is_starext_starfun"; |
|
396 val is_starfun_starext = thm "is_starfun_starext"; |
|
397 val is_starext_starfun_iff = thm "is_starext_starfun_iff"; |
|
398 val starfun_eq = thm "starfun_eq"; |
|
399 val starfun_approx = thm "starfun_approx"; |
|
400 val starfun_lambda_cancel = thm "starfun_lambda_cancel"; |
|
401 val starfun_lambda_cancel2 = thm "starfun_lambda_cancel2"; |
|
402 val starfun_mult_HFinite_approx = thm "starfun_mult_HFinite_approx"; |
|
403 val starfun_add_approx = thm "starfun_add_approx"; |
|
404 val starfun_rabs_hrabs = thm "starfun_rabs_hrabs"; |
|
405 val starfun_inverse_inverse = thm "starfun_inverse_inverse"; |
|
406 val starfun_inverse = thm "starfun_inverse"; |
|
407 val starfun_divide = thm "starfun_divide"; |
|
408 val starfun_inverse2 = thm "starfun_inverse2"; |
|
409 val starfun_mem_starset = thm "starfun_mem_starset"; |
|
410 val hypreal_hrabs = thm "hypreal_hrabs"; |
|
411 val STAR_rabs_add_minus = thm "STAR_rabs_add_minus"; |
|
412 val STAR_starfun_rabs_add_minus = thm "STAR_starfun_rabs_add_minus"; |
|
413 val Infinitesimal_FreeUltrafilterNat_iff2 = thm "Infinitesimal_FreeUltrafilterNat_iff2"; |
|
414 val approx_FreeUltrafilterNat_iff = thm "approx_FreeUltrafilterNat_iff"; |
|
415 val inj_starfun = thm "inj_starfun"; |
|
416 *} |
|
417 |
|
418 end |
354 end |