tuned;
authorwenzelm
Tue Nov 01 01:04:53 2016 +0100 (2016-11-01)
changeset 64438f91cae6c1d74
parent 64437 dba2ca0e0a53
child 64439 2bafda87b524
child 64450 73859eb8d1fe
tuned;
src/HOL/Nonstandard_Analysis/HyperDef.thy
src/HOL/Nonstandard_Analysis/HyperNat.thy
src/HOL/Nonstandard_Analysis/NSA.thy
src/HOL/Nonstandard_Analysis/StarDef.thy
     1.1 --- a/src/HOL/Nonstandard_Analysis/HyperDef.thy	Tue Nov 01 00:55:52 2016 +0100
     1.2 +++ b/src/HOL/Nonstandard_Analysis/HyperDef.thy	Tue Nov 01 01:04:53 2016 +0100
     1.3 @@ -177,10 +177,10 @@
     1.4  lemma star_n_inverse: "inverse (star_n X) = star_n (\<lambda>n. inverse (X n))"
     1.5    by (simp only: star_inverse_def starfun_star_n)
     1.6  
     1.7 -lemma star_n_le: "star_n X \<le> star_n Y = eventually (\<lambda>n. X n \<le> Y n) FreeUltrafilterNat"
     1.8 +lemma star_n_le: "star_n X \<le> star_n Y = eventually (\<lambda>n. X n \<le> Y n) \<U>"
     1.9    by (simp only: star_le_def starP2_star_n)
    1.10  
    1.11 -lemma star_n_less: "star_n X < star_n Y = eventually (\<lambda>n. X n < Y n) FreeUltrafilterNat"
    1.12 +lemma star_n_less: "star_n X < star_n Y = eventually (\<lambda>n. X n < Y n) \<U>"
    1.13    by (simp only: star_less_def starP2_star_n)
    1.14  
    1.15  lemma star_n_zero_num: "0 = star_n (\<lambda>n. 0)"
    1.16 @@ -199,7 +199,7 @@
    1.17  subsection \<open>Existence of Infinite Hyperreal Number\<close>
    1.18  
    1.19  text \<open>Existence of infinite number not corresponding to any real number.
    1.20 -  Use assumption that member @{term FreeUltrafilterNat} is not finite.\<close>
    1.21 +  Use assumption that member @{term \<U>} is not finite.\<close>
    1.22  
    1.23  text \<open>A few lemmas first.\<close>
    1.24  
     2.1 --- a/src/HOL/Nonstandard_Analysis/HyperNat.thy	Tue Nov 01 00:55:52 2016 +0100
     2.2 +++ b/src/HOL/Nonstandard_Analysis/HyperNat.thy	Tue Nov 01 01:04:53 2016 +0100
     2.3 @@ -329,18 +329,18 @@
     2.4  subsubsection \<open>Alternative Characterization of @{term HNatInfinite} using Free Ultrafilter\<close>
     2.5  
     2.6  lemma HNatInfinite_FreeUltrafilterNat:
     2.7 -  "star_n X \<in> HNatInfinite \<Longrightarrow> \<forall>u. eventually (\<lambda>n. u < X n) FreeUltrafilterNat"
     2.8 +  "star_n X \<in> HNatInfinite \<Longrightarrow> \<forall>u. eventually (\<lambda>n. u < X n) \<U>"
     2.9    apply (auto simp add: HNatInfinite_iff SHNat_eq)
    2.10    apply (drule_tac x="star_of u" in spec, simp)
    2.11    apply (simp add: star_of_def star_less_def starP2_star_n)
    2.12    done
    2.13  
    2.14  lemma FreeUltrafilterNat_HNatInfinite:
    2.15 -  "\<forall>u. eventually (\<lambda>n. u < X n) FreeUltrafilterNat \<Longrightarrow> star_n X \<in> HNatInfinite"
    2.16 +  "\<forall>u. eventually (\<lambda>n. u < X n) \<U> \<Longrightarrow> star_n X \<in> HNatInfinite"
    2.17    by (auto simp add: star_less_def starP2_star_n HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
    2.18  
    2.19  lemma HNatInfinite_FreeUltrafilterNat_iff:
    2.20 -  "(star_n X \<in> HNatInfinite) = (\<forall>u. eventually (\<lambda>n. u < X n) FreeUltrafilterNat)"
    2.21 +  "(star_n X \<in> HNatInfinite) = (\<forall>u. eventually (\<lambda>n. u < X n) \<U>)"
    2.22    by (rule iffI [OF HNatInfinite_FreeUltrafilterNat FreeUltrafilterNat_HNatInfinite])
    2.23  
    2.24  
     3.1 --- a/src/HOL/Nonstandard_Analysis/NSA.thy	Tue Nov 01 00:55:52 2016 +0100
     3.2 +++ b/src/HOL/Nonstandard_Analysis/NSA.thy	Tue Nov 01 01:04:53 2016 +0100
     3.3 @@ -1767,7 +1767,7 @@
     3.4  subsubsection \<open>@{term HFinite}\<close>
     3.5  
     3.6  lemma HFinite_FreeUltrafilterNat:
     3.7 -  "star_n X \<in> HFinite \<Longrightarrow> \<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat"
     3.8 +  "star_n X \<in> HFinite \<Longrightarrow> \<exists>u. eventually (\<lambda>n. norm (X n) < u) \<U>"
     3.9    apply (auto simp add: HFinite_def SReal_def)
    3.10    apply (rule_tac x=r in exI)
    3.11    apply (simp add: hnorm_def star_of_def starfun_star_n)
    3.12 @@ -1775,7 +1775,7 @@
    3.13    done
    3.14  
    3.15  lemma FreeUltrafilterNat_HFinite:
    3.16 -  "\<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat \<Longrightarrow> star_n X \<in> HFinite"
    3.17 +  "\<exists>u. eventually (\<lambda>n. norm (X n) < u) \<U> \<Longrightarrow> star_n X \<in> HFinite"
    3.18    apply (auto simp add: HFinite_def mem_Rep_star_iff)
    3.19    apply (rule_tac x="star_of u" in bexI)
    3.20     apply (simp add: hnorm_def starfun_star_n star_of_def)
    3.21 @@ -1784,7 +1784,7 @@
    3.22    done
    3.23  
    3.24  lemma HFinite_FreeUltrafilterNat_iff:
    3.25 -  "star_n X \<in> HFinite \<longleftrightarrow> (\<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat)"
    3.26 +  "star_n X \<in> HFinite \<longleftrightarrow> (\<exists>u. eventually (\<lambda>n. norm (X n) < u) \<U>)"
    3.27    by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite)
    3.28  
    3.29  
    3.30 @@ -1804,14 +1804,14 @@
    3.31  
    3.32  text \<open>Exclude this type of sets from free ultrafilter for Infinite numbers!\<close>
    3.33  lemma FreeUltrafilterNat_const_Finite:
    3.34 -  "eventually (\<lambda>n. norm (X n) = u) FreeUltrafilterNat \<Longrightarrow> star_n X \<in> HFinite"
    3.35 +  "eventually (\<lambda>n. norm (X n) = u) \<U> \<Longrightarrow> star_n X \<in> HFinite"
    3.36    apply (rule FreeUltrafilterNat_HFinite)
    3.37    apply (rule_tac x = "u + 1" in exI)
    3.38    apply (auto elim: eventually_mono)
    3.39    done
    3.40  
    3.41  lemma HInfinite_FreeUltrafilterNat:
    3.42 -  "star_n X \<in> HInfinite \<Longrightarrow> \<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat"
    3.43 +  "star_n X \<in> HInfinite \<Longrightarrow> \<forall>u. eventually (\<lambda>n. u < norm (X n)) \<U>"
    3.44    apply (drule HInfinite_HFinite_iff [THEN iffD1])
    3.45    apply (simp add: HFinite_FreeUltrafilterNat_iff)
    3.46    apply (rule allI, drule_tac x="u + 1" in spec)
    3.47 @@ -1827,7 +1827,7 @@
    3.48    by (auto intro: order_less_asym)
    3.49  
    3.50  lemma FreeUltrafilterNat_HInfinite:
    3.51 -  "\<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat \<Longrightarrow> star_n X \<in> HInfinite"
    3.52 +  "\<forall>u. eventually (\<lambda>n. u < norm (X n)) \<U> \<Longrightarrow> star_n X \<in> HInfinite"
    3.53    apply (rule HInfinite_HFinite_iff [THEN iffD2])
    3.54    apply (safe, drule HFinite_FreeUltrafilterNat, safe)
    3.55    apply (drule_tac x = u in spec)
    3.56 @@ -1841,7 +1841,7 @@
    3.57  qed
    3.58  
    3.59  lemma HInfinite_FreeUltrafilterNat_iff:
    3.60 -  "star_n X \<in> HInfinite \<longleftrightarrow> (\<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat)"
    3.61 +  "star_n X \<in> HInfinite \<longleftrightarrow> (\<forall>u. eventually (\<lambda>n. u < norm (X n)) \<U>)"
    3.62    by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)
    3.63  
    3.64  
    3.65 @@ -1904,7 +1904,7 @@
    3.66    by (auto simp add: less_Suc_eq)
    3.67  
    3.68  
    3.69 -text \<open>Prove that any segment is finite and hence cannot belong to \<open>FreeUltrafilterNat\<close>.\<close>
    3.70 +text \<open>Prove that any segment is finite and hence cannot belong to \<open>\<U>\<close>.\<close>
    3.71  
    3.72  lemma finite_real_of_nat_segment: "finite {n::nat. real n < real (m::nat)}"
    3.73    by auto
    3.74 @@ -1925,17 +1925,17 @@
    3.75    by (simp add: finite_real_of_nat_le_real)
    3.76  
    3.77  lemma rabs_real_of_nat_le_real_FreeUltrafilterNat:
    3.78 -  "\<not> eventually (\<lambda>n. \<bar>real n\<bar> \<le> u) FreeUltrafilterNat"
    3.79 +  "\<not> eventually (\<lambda>n. \<bar>real n\<bar> \<le> u) \<U>"
    3.80    by (blast intro!: FreeUltrafilterNat.finite finite_rabs_real_of_nat_le_real)
    3.81  
    3.82 -lemma FreeUltrafilterNat_nat_gt_real: "eventually (\<lambda>n. u < real n) FreeUltrafilterNat"
    3.83 +lemma FreeUltrafilterNat_nat_gt_real: "eventually (\<lambda>n. u < real n) \<U>"
    3.84    apply (rule FreeUltrafilterNat.finite')
    3.85    apply (subgoal_tac "{n::nat. \<not> u < real n} = {n. real n \<le> u}")
    3.86     apply (auto simp add: finite_real_of_nat_le_real)
    3.87    done
    3.88  
    3.89  text \<open>The complement of \<open>{n. \<bar>real n\<bar> \<le> u} = {n. u < \<bar>real n\<bar>}\<close> is in
    3.90 -  \<open>FreeUltrafilterNat\<close> by property of (free) ultrafilters.\<close>
    3.91 +  \<open>\<U>\<close> by property of (free) ultrafilters.\<close>
    3.92  
    3.93  lemma Compl_real_le_eq: "- {n::nat. real n \<le> u} = {n. u < real n}"
    3.94    by (auto dest!: order_le_less_trans simp add: linorder_not_le)
    3.95 @@ -1991,17 +1991,17 @@
    3.96        simp del: of_nat_Suc)
    3.97  
    3.98  lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:
    3.99 -  "0 < u \<Longrightarrow> \<not> eventually (\<lambda>n. u \<le> inverse(real(Suc n))) FreeUltrafilterNat"
   3.100 +  "0 < u \<Longrightarrow> \<not> eventually (\<lambda>n. u \<le> inverse(real(Suc n))) \<U>"
   3.101    by (blast intro!: FreeUltrafilterNat.finite finite_inverse_real_of_posnat_ge_real)
   3.102  
   3.103  text \<open>The complement of \<open>{n. u \<le> inverse(real(Suc n))} = {n. inverse (real (Suc n)) < u}\<close>
   3.104 -  is in \<open>FreeUltrafilterNat\<close> by property of (free) ultrafilters.\<close>
   3.105 +  is in \<open>\<U>\<close> by property of (free) ultrafilters.\<close>
   3.106  lemma Compl_le_inverse_eq: "- {n. u \<le> inverse(real(Suc n))} = {n. inverse(real(Suc n)) < u}"
   3.107    by (auto dest!: order_le_less_trans simp add: linorder_not_le)
   3.108  
   3.109  
   3.110  lemma FreeUltrafilterNat_inverse_real_of_posnat:
   3.111 -  "0 < u \<Longrightarrow> eventually (\<lambda>n. inverse(real(Suc n)) < u) FreeUltrafilterNat"
   3.112 +  "0 < u \<Longrightarrow> eventually (\<lambda>n. inverse(real(Suc n)) < u) \<U>"
   3.113    by (drule inverse_real_of_posnat_ge_real_FreeUltrafilterNat)
   3.114      (simp add: FreeUltrafilterNat.eventually_not_iff not_le[symmetric])
   3.115  
     4.1 --- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Tue Nov 01 00:55:52 2016 +0100
     4.2 +++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Tue Nov 01 01:04:53 2016 +0100
     4.3 @@ -20,7 +20,7 @@
     4.4    apply (rule infinite_UNIV_nat)
     4.5    done
     4.6  
     4.7 -interpretation FreeUltrafilterNat: freeultrafilter FreeUltrafilterNat
     4.8 +interpretation FreeUltrafilterNat: freeultrafilter \<U>
     4.9    by (rule freeultrafilter_FreeUltrafilterNat)
    4.10  
    4.11