# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1556798312 -3600
# Node ID 2d5b122aa0ff43bb6d1692d6c07f3ba1348b5711
# Parent  ce9134bdc1d4f1e5307f58312b71dfe809b2471f
De-applying and combining lemmas to make structured proofs

diff -r ce9134bdc1d4 -r 2d5b122aa0ff src/HOL/Nonstandard_Analysis/CLim.thy
--- 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>
diff -r ce9134bdc1d4 -r 2d5b122aa0ff src/HOL/Nonstandard_Analysis/HLim.thy
--- 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)
diff -r ce9134bdc1d4 -r 2d5b122aa0ff src/HOL/Nonstandard_Analysis/HSEQ.thy
--- 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)
diff -r ce9134bdc1d4 -r 2d5b122aa0ff src/HOL/Nonstandard_Analysis/HSeries.thy
--- 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"
diff -r ce9134bdc1d4 -r 2d5b122aa0ff src/HOL/Nonstandard_Analysis/HTranscendental.thy
--- 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
diff -r ce9134bdc1d4 -r 2d5b122aa0ff src/HOL/Nonstandard_Analysis/HyperNat.thy
--- 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)