author paulson Thu, 02 May 2019 12:58:32 +0100 changeset 70228 2d5b122aa0ff parent 70227 ce9134bdc1d4 child 70231 cdbc8d92c349 child 70232 d19266b7465f
De-applying and combining lemmas to make structured proofs
```--- 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)
-  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 (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"
+    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 @@

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])
-   apply (rule_tac x = x in star_cases)
-   apply (rule_tac [2] x = x in star_cases)
-  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"
+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"
+    then show "(*f* f) x \<approx> star_of L"
+  qed
+qed

lemma isNSCont_minus: "isNSCont f a \<Longrightarrow> isNSCont (\<lambda>x. - f x) a"
```--- 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)"
-
lemma NSLIMSEQ_I: "(\<And>N. N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L) \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"

@@ -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"
-
lemma NSLIMSEQ_diff_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. f n - b) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b"

@@ -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 (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
-  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)
-  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"
+    then show "(*f* (\<lambda>n. f (Suc n))) N \<approx> star_of l"
+  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"
```--- 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"