--- a/src/HOL/Nonstandard_Analysis/CLim.thy Thu May 02 11:43:56 2019 +0200
+++ b/src/HOL/Nonstandard_Analysis/CLim.thy Thu May 02 12:58:32 2019 +0100
@@ -100,7 +100,7 @@
subsection \<open>Continuity\<close>
lemma NSLIM_isContc_iff: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a \<longleftrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a"
- by (rule NSLIM_h_iff)
+ by (rule NSLIM_at0_iff)
subsection \<open>Functions from Complex to Reals\<close>
--- a/src/HOL/Nonstandard_Analysis/HLim.thy Thu May 02 11:43:56 2019 +0200
+++ b/src/HOL/Nonstandard_Analysis/HLim.thy Thu May 02 12:58:32 2019 +0100
@@ -62,10 +62,7 @@
lemma NSLIM_inverse: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> L \<noteq> 0 \<Longrightarrow> (\<lambda>x. inverse (f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (inverse L)"
for L :: "'a::real_normed_div_algebra"
- apply (simp add: NSLIM_def, clarify)
- apply (drule spec)
- apply (auto simp add: star_of_approx_inverse)
- done
+ unfolding NSLIM_def by (metis (no_types) star_of_approx_inverse star_of_simps(6) starfun_inverse)
lemma NSLIM_zero:
assumes f: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S l"
@@ -76,27 +73,32 @@
then show ?thesis by simp
qed
-lemma NSLIM_zero_cancel: "(\<lambda>x. f x - l) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0 \<Longrightarrow> f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l"
- apply (drule_tac g = "\<lambda>x. l" and m = l in NSLIM_add)
- apply (auto simp add: add.assoc)
- done
+lemma NSLIM_zero_cancel:
+ assumes "(\<lambda>x. f x - l) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0"
+ shows "f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l"
+proof -
+ have "(\<lambda>x. f x - l + l) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0 + l"
+ by (fast intro: assms NSLIM_const NSLIM_add)
+ then show ?thesis
+ by simp
+qed
-lemma NSLIM_const_not_eq: "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
- for a :: "'a::real_normed_algebra_1"
- apply (simp add: NSLIM_def)
- apply (rule_tac x="star_of a + of_hypreal \<epsilon>" in exI)
- apply (simp add: hypreal_epsilon_not_zero approx_def)
- done
+lemma NSLIM_const_eq:
+ fixes a :: "'a::real_normed_algebra_1"
+ assumes "(\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S l"
+ shows "k = l"
+proof -
+ have "\<not> (\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S l" if "k \<noteq> l"
+ proof -
+ have "star_of a + of_hypreal \<epsilon> \<approx> star_of a"
+ by (simp add: approx_def)
+ then show ?thesis
+ using hypreal_epsilon_not_zero that by (force simp add: NSLIM_def)
+ qed
+ with assms show ?thesis by metis
+qed
-lemma NSLIM_not_zero: "k \<noteq> 0 \<Longrightarrow> \<not> (\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S 0"
- for a :: "'a::real_normed_algebra_1"
- by (rule NSLIM_const_not_eq)
-
-lemma NSLIM_const_eq: "(\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> k = L"
- for a :: "'a::real_normed_algebra_1"
- by (rule ccontr) (blast dest: NSLIM_const_not_eq)
-
-lemma NSLIM_unique: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S M \<Longrightarrow> L = M"
+lemma NSLIM_unique: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S M \<Longrightarrow> l = M"
for a :: "'a::real_normed_algebra_1"
by (drule (1) NSLIM_diff) (auto dest!: NSLIM_const_eq)
@@ -182,10 +184,7 @@
by (simp add: isNSCont_def NSLIM_def)
lemma NSLIM_isNSCont: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a) \<Longrightarrow> isNSCont f a"
- apply (auto simp add: isNSCont_def NSLIM_def)
- apply (case_tac "y = star_of a")
- apply auto
- done
+ by (force simp add: isNSCont_def NSLIM_def)
text \<open>NS continuity can be defined using NS Limit in
similar fashion to standard definition of continuity.\<close>
@@ -214,20 +213,23 @@
text \<open>Prove equivalence between NS limits --
seems easier than using standard definition.\<close>
-lemma NSLIM_h_iff: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<longleftrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S L"
- apply (simp add: NSLIM_def, auto)
- apply (drule_tac x = "star_of a + x" in spec)
- apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
- apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
- apply (erule_tac [3] approx_minus_iff2 [THEN iffD1])
- prefer 2 apply (simp add: add.commute)
- apply (rule_tac x = x in star_cases)
- apply (rule_tac [2] x = x in star_cases)
- apply (auto simp add: starfun star_of_def star_n_minus star_n_add add.assoc star_n_zero_num)
- done
-
-lemma NSLIM_isCont_iff: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a \<longleftrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a"
- by (fact NSLIM_h_iff)
+lemma NSLIM_at0_iff: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<longleftrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S L"
+proof
+ assume "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
+ then show "(\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S L"
+ by (simp add: NSLIM_def) (metis (no_types) add_cancel_left_right approx_add_left_iff starfun_lambda_cancel)
+next
+ assume *: "(\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S L"
+ show "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
+ proof (clarsimp simp: NSLIM_def)
+ fix x
+ assume "x \<noteq> star_of a" "x \<approx> star_of a"
+ then have "(*f* (\<lambda>h. f (a + h))) (- star_of a + x) \<approx> star_of L"
+ by (metis (no_types, lifting) "*" NSLIM_D add.right_neutral add_minus_cancel approx_minus_iff2 star_zero_def)
+ then show "(*f* f) x \<approx> star_of L"
+ by (simp add: starfun_lambda_cancel)
+ qed
+qed
lemma isNSCont_minus: "isNSCont f a \<Longrightarrow> isNSCont (\<lambda>x. - f x) a"
by (simp add: isNSCont_def)
--- a/src/HOL/Nonstandard_Analysis/HSEQ.thy Thu May 02 11:43:56 2019 +0200
+++ b/src/HOL/Nonstandard_Analysis/HSEQ.thy Thu May 02 12:58:32 2019 +0100
@@ -41,9 +41,6 @@
subsection \<open>Limits of Sequences\<close>
-lemma NSLIMSEQ_iff: "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S L) \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
- by (simp add: NSLIMSEQ_def)
-
lemma NSLIMSEQ_I: "(\<And>N. N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L) \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
by (simp add: NSLIMSEQ_def)
@@ -72,10 +69,6 @@
lemma NSLIMSEQ_diff: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> (\<lambda>n. X n - Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b"
using NSLIMSEQ_add [of X a "- Y" "- b"] by (simp add: NSLIMSEQ_minus fun_Compl_def)
-(* FIXME: delete *)
-lemma NSLIMSEQ_add_minus: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> (\<lambda>n. X n + - Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + - b"
- by (simp add: NSLIMSEQ_diff)
-
lemma NSLIMSEQ_diff_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. f n - b) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b"
by (simp add: NSLIMSEQ_diff NSLIMSEQ_const)
@@ -95,10 +88,8 @@
text \<open>Uniqueness of limit.\<close>
lemma NSLIMSEQ_unique: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> a = b"
- apply (simp add: NSLIMSEQ_def)
- apply (drule HNatInfinite_whn [THEN [2] bspec])+
- apply (auto dest: approx_trans3)
- done
+ unfolding NSLIMSEQ_def
+ using HNatInfinite_whn approx_trans3 star_of_approx_iff by blast
lemma NSLIMSEQ_pow [rule_format]: "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S a) \<longrightarrow> ((\<lambda>n. (X n) ^ m) \<longlonglongrightarrow>\<^sub>N\<^sub>S a ^ m)"
for a :: "'a::{real_normed_algebra,power}"
@@ -109,15 +100,9 @@
lemma NSLIMSEQ_le: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> g \<longlonglongrightarrow>\<^sub>N\<^sub>S m \<Longrightarrow> \<exists>N. \<forall>n \<ge> N. f n \<le> g n \<Longrightarrow> l \<le> m"
for l m :: real
- apply (simp add: NSLIMSEQ_def, safe)
- apply (drule starfun_le_mono)
- apply (drule HNatInfinite_whn [THEN [2] bspec])+
- apply (drule_tac x = whn in spec)
- apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
- apply clarify
- apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2)
- done
-
+ unfolding NSLIMSEQ_def
+ by (metis HNatInfinite_whn bex_Infinitesimal_iff2 hypnat_of_nat_le_whn hypreal_of_real_le_add_Infininitesimal_cancel2 starfun_le_mono)
+
lemma NSLIMSEQ_le_const: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S r \<Longrightarrow> \<forall>n. a \<le> X n \<Longrightarrow> a \<le> r"
for a r :: real
by (erule NSLIMSEQ_le [OF NSLIMSEQ_const]) auto
@@ -130,24 +115,30 @@
By the equivalence between Cauchiness and convergence and because
the successor of an infinite hypernatural is also infinite.\<close>
-lemma NSLIMSEQ_Suc: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> (\<lambda>n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
- apply (unfold NSLIMSEQ_def)
- apply safe
- apply (drule_tac x="N + 1" in bspec)
- apply (erule HNatInfinite_add)
- apply (simp add: starfun_shift_one)
- done
-
-lemma NSLIMSEQ_imp_Suc: "(\<lambda>n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
- apply (unfold NSLIMSEQ_def)
- apply safe
- apply (drule_tac x="N - 1" in bspec)
- apply (erule Nats_1 [THEN [2] HNatInfinite_diff])
- apply (simp add: starfun_shift_one one_le_HNatInfinite)
- done
-
-lemma NSLIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<longleftrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
- by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
+lemma NSLIMSEQ_Suc_iff: "((\<lambda>n. f (Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l) \<longleftrightarrow> (f \<longlonglongrightarrow>\<^sub>N\<^sub>S l)"
+proof
+ assume *: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
+ show "(\<lambda>n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
+ proof (rule NSLIMSEQ_I)
+ fix N
+ assume "N \<in> HNatInfinite"
+ then have "(*f* f) (N + 1) \<approx> star_of l"
+ by (simp add: HNatInfinite_add NSLIMSEQ_D *)
+ then show "(*f* (\<lambda>n. f (Suc n))) N \<approx> star_of l"
+ by (simp add: starfun_shift_one)
+ qed
+next
+ assume *: "(\<lambda>n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
+ show "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
+ proof (rule NSLIMSEQ_I)
+ fix N
+ assume "N \<in> HNatInfinite"
+ then have "(*f* (\<lambda>n. f (Suc n))) (N - 1) \<approx> star_of l"
+ using * by (simp add: HNatInfinite_diff NSLIMSEQ_D)
+ then show "(*f* f) N \<approx> star_of l"
+ by (simp add: \<open>N \<in> HNatInfinite\<close> one_le_HNatInfinite starfun_shift_one)
+ qed
+qed
subsubsection \<open>Equivalence of \<^term>\<open>LIMSEQ\<close> and \<^term>\<open>NSLIMSEQ\<close>\<close>
@@ -262,11 +253,7 @@
by (auto simp: Standard_def)
lemma NSBseqD2: "NSBseq X \<Longrightarrow> ( *f* X) N \<in> HFinite"
- apply (cases "N \<in> HNatInfinite")
- apply (erule (1) NSBseqD)
- apply (rule subsetD [OF Standard_subset_HFinite])
- apply (simp add: HNatInfinite_def Nats_eq_Standard)
- done
+ using HNatInfinite_def NSBseq_def Nats_eq_Standard Standard_starfun Standard_subset_HFinite by blast
lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N \<in> HFinite \<Longrightarrow> NSBseq X"
by (simp add: NSBseq_def)
--- a/src/HOL/Nonstandard_Analysis/HSeries.thy Thu May 02 11:43:56 2019 +0200
+++ b/src/HOL/Nonstandard_Analysis/HSeries.thy Thu May 02 12:58:32 2019 +0100
@@ -155,7 +155,7 @@
text \<open>Terms of a convergent series tend to zero.\<close>
lemma NSsummable_NSLIMSEQ_zero: "NSsummable f \<Longrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
- by (metis HNatInfinite_add_one approx_hrabs_zero_cancel sumhr_Suc)
+ by (metis HNatInfinite_add approx_hrabs_zero_cancel sumhr_Suc)
text \<open>Nonstandard comparison test.\<close>
lemma NSsummable_comparison_test: "\<exists>N. \<forall>n. N \<le> n \<longrightarrow> \<bar>f n\<bar> \<le> g n \<Longrightarrow> NSsummable g \<Longrightarrow> NSsummable f"
--- a/src/HOL/Nonstandard_Analysis/HTranscendental.thy Thu May 02 11:43:56 2019 +0200
+++ b/src/HOL/Nonstandard_Analysis/HTranscendental.thy Thu May 02 12:58:32 2019 +0100
@@ -216,7 +216,7 @@
using NSsums_def sums_NSsums_iff by blast
then have "hypreal_of_real (exp x) \<approx> sumhr (0, whn, \<lambda>n. inverse (fact n) * x ^ n)"
unfolding starfunNat_sumr [symmetric] atLeast0LessThan
- using HNatInfinite_whn NSLIMSEQ_iff approx_sym by blast
+ using HNatInfinite_whn NSLIMSEQ_def approx_sym by blast
then show ?thesis
unfolding exphr_def using st_eq_approx_iff by auto
qed
@@ -354,7 +354,7 @@
have "summable (\<lambda>i. sin_coeff i * x ^ i)"
using summable_norm_sin [of x] by (simp add: summable_rabs_cancel)
then have "(*f* (\<lambda>n. \<Sum>n<n. sin_coeff n * x ^ n)) whn \<in> HFinite"
- unfolding summable_sums_iff sums_NSsums_iff NSsums_def NSLIMSEQ_iff
+ unfolding summable_sums_iff sums_NSsums_iff NSsums_def NSLIMSEQ_def
using HFinite_star_of HNatInfinite_whn approx_HFinite approx_sym by blast
then show ?thesis
unfolding sumhr_app
@@ -384,7 +384,7 @@
have "summable (\<lambda>i. cos_coeff i * x ^ i)"
using summable_norm_cos [of x] by (simp add: summable_rabs_cancel)
then have "(*f* (\<lambda>n. \<Sum>n<n. cos_coeff n * x ^ n)) whn \<in> HFinite"
- unfolding summable_sums_iff sums_NSsums_iff NSsums_def NSLIMSEQ_iff
+ unfolding summable_sums_iff sums_NSsums_iff NSsums_def NSLIMSEQ_def
using HFinite_star_of HNatInfinite_whn approx_HFinite approx_sym by blast
then show ?thesis
unfolding sumhr_app
--- a/src/HOL/Nonstandard_Analysis/HyperNat.thy Thu May 02 11:43:56 2019 +0200
+++ b/src/HOL/Nonstandard_Analysis/HyperNat.thy Thu May 02 12:58:32 2019 +0100
@@ -234,9 +234,6 @@
lemma HNatInfinite_add: "x \<in> HNatInfinite \<Longrightarrow> x + y \<in> HNatInfinite"
using HNatInfinite_upward_closed hypnat_le_add1 by blast
-lemma HNatInfinite_add_one: "x \<in> HNatInfinite \<Longrightarrow> x + 1 \<in> HNatInfinite"
- by (rule HNatInfinite_add)
-
lemma HNatInfinite_diff: "\<lbrakk>x \<in> HNatInfinite; y \<in> Nats\<rbrakk> \<Longrightarrow> x - y \<in> HNatInfinite"
by (metis HNatInfinite_not_Nats_iff Nats_add Nats_le_HNatInfinite le_add_diff_inverse)