src/HOL/NSA/Star.thy
changeset 60041 6c86d58ab0ca
parent 58878 f962e42e324d
child 61070 b72a990adfe2
     1.1 --- a/src/HOL/NSA/Star.thy	Sun Apr 12 11:34:09 2015 +0200
     1.2 +++ b/src/HOL/NSA/Star.thy	Sun Apr 12 11:34:16 2015 +0200
     1.3 @@ -22,8 +22,8 @@
     1.4  definition
     1.5    (* nonstandard extension of function *)
     1.6    is_starext  :: "['a star => 'a star, 'a => 'a] => bool" where
     1.7 -  "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
     1.8 -                        ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
     1.9 +  "is_starext F f =
    1.10 +    (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y). ((y = (F x)) = (eventually (\<lambda>n. Y n = f(X n)) \<U>)))"
    1.11  
    1.12  definition
    1.13    (* internal functions *)
    1.14 @@ -71,7 +71,7 @@
    1.15  lemma STAR_real_seq_to_hypreal:
    1.16      "\<forall>n. (X n) \<notin> M ==> star_n X \<notin> *s* M"
    1.17  apply (unfold starset_def star_of_def)
    1.18 -apply (simp add: Iset_star_n)
    1.19 +apply (simp add: Iset_star_n FreeUltrafilterNat.proper)
    1.20  done
    1.21  
    1.22  lemma STAR_singleton: "*s* {x} = {star_of x}"
    1.23 @@ -304,9 +304,7 @@
    1.24     In this theory since @{text hypreal_hrabs} proved here. Maybe
    1.25     move both theorems??*}
    1.26  lemma Infinitesimal_FreeUltrafilterNat_iff2:
    1.27 -     "(star_n X \<in> Infinitesimal) =
    1.28 -      (\<forall>m. {n. norm(X n) < inverse(real(Suc m))}
    1.29 -                \<in>  FreeUltrafilterNat)"
    1.30 +     "(star_n X \<in> Infinitesimal) = (\<forall>m. eventually (\<lambda>n. norm(X n) < inverse(real(Suc m))) \<U>)"
    1.31  by (simp add: Infinitesimal_hypreal_of_nat_iff star_of_def
    1.32       hnorm_def star_of_nat_def starfun_star_n
    1.33       star_n_inverse star_n_less real_of_nat_def)
    1.34 @@ -318,11 +316,11 @@
    1.35        HNatInfinite_FreeUltrafilterNat_iff
    1.36        Infinitesimal_FreeUltrafilterNat_iff2)
    1.37  apply (drule_tac x="Suc m" in spec)
    1.38 -apply (erule ultra, simp)
    1.39 +apply (auto elim!: eventually_elim1)
    1.40  done
    1.41  
    1.42  lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
    1.43 -      (\<forall>r>0. {n. norm (X n - Y n) < r} : FreeUltrafilterNat)"
    1.44 +      (\<forall>r>0. eventually (\<lambda>n. norm (X n - Y n) < r) \<U>)"
    1.45  apply (subst approx_minus_iff)
    1.46  apply (rule mem_infmal_iff [THEN subst])
    1.47  apply (simp add: star_n_diff)
    1.48 @@ -330,8 +328,7 @@
    1.49  done
    1.50  
    1.51  lemma approx_FreeUltrafilterNat_iff2: "star_n X @= star_n Y =
    1.52 -      (\<forall>m. {n. norm (X n - Y n) <
    1.53 -                  inverse(real(Suc m))} : FreeUltrafilterNat)"
    1.54 +      (\<forall>m. eventually (\<lambda>n. norm (X n - Y n) < inverse(real(Suc m))) \<U>)"
    1.55  apply (subst approx_minus_iff)
    1.56  apply (rule mem_infmal_iff [THEN subst])
    1.57  apply (simp add: star_n_diff)
    1.58 @@ -342,7 +339,7 @@
    1.59  apply (rule inj_onI)
    1.60  apply (rule ext, rule ccontr)
    1.61  apply (drule_tac x = "star_n (%n. xa)" in fun_cong)
    1.62 -apply (auto simp add: starfun star_n_eq_iff)
    1.63 +apply (auto simp add: starfun star_n_eq_iff FreeUltrafilterNat.proper)
    1.64  done
    1.65  
    1.66  end