misc tuning and modernization;
authorwenzelm
Sun Dec 18 23:43:50 2016 +0100 (2016-12-18)
changeset 646042bf8cfc98c4d
parent 64603 a7f5e59378f7
child 64605 9c1173a7e4cb
misc tuning and modernization;
src/HOL/Nonstandard_Analysis/CStar.thy
src/HOL/Nonstandard_Analysis/HDeriv.thy
src/HOL/Nonstandard_Analysis/HLim.thy
src/HOL/Nonstandard_Analysis/HLog.thy
src/HOL/Nonstandard_Analysis/HSEQ.thy
src/HOL/Nonstandard_Analysis/HSeries.thy
     1.1 --- a/src/HOL/Nonstandard_Analysis/CStar.thy	Sun Dec 18 22:14:53 2016 +0100
     1.2 +++ b/src/HOL/Nonstandard_Analysis/CStar.thy	Sun Dec 18 23:43:50 2016 +0100
     1.3 @@ -3,37 +3,36 @@
     1.4      Copyright:  2001 University of Edinburgh
     1.5  *)
     1.6  
     1.7 -section\<open>Star-transforms in NSA, Extending Sets of Complex Numbers
     1.8 -      and Complex Functions\<close>
     1.9 +section \<open>Star-transforms in NSA, Extending Sets of Complex Numbers and Complex Functions\<close>
    1.10  
    1.11  theory CStar
    1.12 -imports NSCA
    1.13 +  imports NSCA
    1.14  begin
    1.15  
    1.16 -subsection\<open>Properties of the *-Transform Applied to Sets of Reals\<close>
    1.17 +subsection \<open>Properties of the \<open>*\<close>-Transform Applied to Sets of Reals\<close>
    1.18  
    1.19 -lemma STARC_hcomplex_of_complex_Int:
    1.20 -     "*s* X Int SComplex = hcomplex_of_complex ` X"
    1.21 -by (auto simp add: Standard_def)
    1.22 +lemma STARC_hcomplex_of_complex_Int: "*s* X \<inter> SComplex = hcomplex_of_complex ` X"
    1.23 +  by (auto simp: Standard_def)
    1.24  
    1.25 -lemma lemma_not_hcomplexA:
    1.26 -     "x \<notin> hcomplex_of_complex ` A ==> \<forall>y \<in> A. x \<noteq> hcomplex_of_complex y"
    1.27 -by auto
    1.28 +lemma lemma_not_hcomplexA: "x \<notin> hcomplex_of_complex ` A \<Longrightarrow> \<forall>y \<in> A. x \<noteq> hcomplex_of_complex y"
    1.29 +  by auto
    1.30 +
    1.31  
    1.32 -subsection\<open>Theorems about Nonstandard Extensions of Functions\<close>
    1.33 +subsection \<open>Theorems about Nonstandard Extensions of Functions\<close>
    1.34  
    1.35 -lemma starfunC_hcpow: "!!Z. ( *f* (%z. z ^ n)) Z = Z pow hypnat_of_nat n"
    1.36 -by transfer (rule refl)
    1.37 +lemma starfunC_hcpow: "\<And>Z. ( *f* (\<lambda>z. z ^ n)) Z = Z pow hypnat_of_nat n"
    1.38 +  by transfer (rule refl)
    1.39  
    1.40  lemma starfunCR_cmod: "*f* cmod = hcmod"
    1.41 -by transfer (rule refl)
    1.42 +  by transfer (rule refl)
    1.43  
    1.44 -subsection\<open>Internal Functions - Some Redundancy With *f* Now\<close>
    1.45 +
    1.46 +subsection \<open>Internal Functions - Some Redundancy With \<open>*f*\<close> Now\<close>
    1.47  
    1.48  (** subtraction: ( *fn) - ( *gn) = *(fn - gn) **)
    1.49  (*
    1.50  lemma starfun_n_diff:
    1.51 -   "( *fn* f) z - ( *fn* g) z = ( *fn* (%i x. f i x - g i x)) z"
    1.52 +   "( *fn* f) z - ( *fn* g) z = ( *fn* (\<lambda>i x. f i x - g i x)) z"
    1.53  apply (cases z)
    1.54  apply (simp add: starfun_n star_n_diff)
    1.55  done
    1.56 @@ -41,19 +40,17 @@
    1.57  (** composition: ( *fn) o ( *gn) = *(fn o gn) **)
    1.58  
    1.59  lemma starfun_Re: "( *f* (\<lambda>x. Re (f x))) = (\<lambda>x. hRe (( *f* f) x))"
    1.60 -by transfer (rule refl)
    1.61 +  by transfer (rule refl)
    1.62  
    1.63  lemma starfun_Im: "( *f* (\<lambda>x. Im (f x))) = (\<lambda>x. hIm (( *f* f) x))"
    1.64 -by transfer (rule refl)
    1.65 +  by transfer (rule refl)
    1.66  
    1.67  lemma starfunC_eq_Re_Im_iff:
    1.68 -    "(( *f* f) x = z) = ((( *f* (%x. Re(f x))) x = hRe (z)) &
    1.69 -                          (( *f* (%x. Im(f x))) x = hIm (z)))"
    1.70 -by (simp add: hcomplex_hRe_hIm_cancel_iff starfun_Re starfun_Im)
    1.71 +  "( *f* f) x = z \<longleftrightarrow> ( *f* (\<lambda>x. Re (f x))) x = hRe z \<and> ( *f* (\<lambda>x. Im (f x))) x = hIm z"
    1.72 +  by (simp add: hcomplex_hRe_hIm_cancel_iff starfun_Re starfun_Im)
    1.73  
    1.74  lemma starfunC_approx_Re_Im_iff:
    1.75 -    "(( *f* f) x \<approx> z) = ((( *f* (%x. Re(f x))) x \<approx> hRe (z)) &
    1.76 -                            (( *f* (%x. Im(f x))) x \<approx> hIm (z)))"
    1.77 -by (simp add: hcomplex_approx_iff starfun_Re starfun_Im)
    1.78 +  "( *f* f) x \<approx> z \<longleftrightarrow> ( *f* (\<lambda>x. Re (f x))) x \<approx> hRe z \<and> ( *f* (\<lambda>x. Im (f x))) x \<approx> hIm z"
    1.79 +  by (simp add: hcomplex_approx_iff starfun_Re starfun_Im)
    1.80  
    1.81  end
     2.1 --- a/src/HOL/Nonstandard_Analysis/HDeriv.thy	Sun Dec 18 22:14:53 2016 +0100
     2.2 +++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy	Sun Dec 18 23:43:50 2016 +0100
     2.3 @@ -53,7 +53,7 @@
     2.4     apply (drule (1) bspec)+
     2.5     apply (drule (1) approx_trans3)
     2.6     apply simp
     2.7 -  apply (simp add: Infinitesimal_of_hypreal Infinitesimal_epsilon)
     2.8 +  apply (simp add: Infinitesimal_of_hypreal)
     2.9    apply (simp add: of_hypreal_eq_0_iff hypreal_epsilon_not_zero)
    2.10    done
    2.11  
    2.12 @@ -75,7 +75,7 @@
    2.13  text \<open>While we're at it!\<close>
    2.14  lemma NSDERIV_iff2:
    2.15    "(NSDERIV f x :> D) \<longleftrightarrow>
    2.16 -    (\<forall>w. w \<noteq> star_of x & w \<approx> star_of x \<longrightarrow> ( *f* (%z. (f z - f x) / (z-x))) w \<approx> star_of D)"
    2.17 +    (\<forall>w. w \<noteq> star_of x \<and> w \<approx> star_of x \<longrightarrow> ( *f* (\<lambda>z. (f z - f x) / (z - x))) w \<approx> star_of D)"
    2.18    by (simp add: NSDERIV_NSLIM_iff2 NSLIM_def)
    2.19  
    2.20  (* FIXME delete *)
    2.21 @@ -91,7 +91,7 @@
    2.22    apply (drule_tac x = u in spec, auto)
    2.23    apply (drule_tac c = "u - hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1)
    2.24     apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1])
    2.25 -   apply (subgoal_tac [2] "( *f* (%z. z-x)) u \<noteq> (0::hypreal) ")
    2.26 +   apply (subgoal_tac [2] "( *f* (\<lambda>z. z - x)) u \<noteq> (0::hypreal) ")
    2.27      apply (auto simp: approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
    2.28        Infinitesimal_subset_HFinite [THEN subsetD])
    2.29    done
    2.30 @@ -290,7 +290,8 @@
    2.31    apply (case_tac "( *f* g) (star_of (x) + xa) = star_of (g x) ")
    2.32     apply (drule_tac g = g in NSDERIV_zero)
    2.33        apply (auto simp add: divide_inverse)
    2.34 -  apply (rule_tac z1 = "( *f* g) (star_of (x) + xa) - star_of (g x) " and y1 = "inverse xa" in lemma_chain [THEN ssubst])
    2.35 +  apply (rule_tac z1 = "( *f* g) (star_of (x) + xa) - star_of (g x) " and y1 = "inverse xa"
    2.36 +      in lemma_chain [THEN ssubst])
    2.37     apply (erule hypreal_not_eq_minus_iff [THEN iffD1])
    2.38    apply (rule approx_mult_star_of)
    2.39     apply (simp_all add: divide_inverse [symmetric])
     3.1 --- a/src/HOL/Nonstandard_Analysis/HLim.thy	Sun Dec 18 22:14:53 2016 +0100
     3.2 +++ b/src/HOL/Nonstandard_Analysis/HLim.thy	Sun Dec 18 23:43:50 2016 +0100
     3.3 @@ -77,7 +77,7 @@
     3.4  qed
     3.5  
     3.6  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"
     3.7 -  apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
     3.8 +  apply (drule_tac g = "\<lambda>x. l" and m = l in NSLIM_add)
     3.9     apply (auto simp add: add.assoc)
    3.10    done
    3.11  
    3.12 @@ -205,8 +205,8 @@
    3.13  lemma isCont_isNSCont: "isCont f a \<Longrightarrow> isNSCont f a"
    3.14    by (erule isNSCont_isCont_iff [THEN iffD2])
    3.15  
    3.16 -text \<open>NS continuity \<open>==>\<close> Standard continuity.\<close>
    3.17 -lemma isNSCont_isCont: "isNSCont f a ==> isCont f a"
    3.18 +text \<open>NS continuity \<open>\<Longrightarrow>\<close> Standard continuity.\<close>
    3.19 +lemma isNSCont_isCont: "isNSCont f a \<Longrightarrow> isCont f a"
    3.20    by (erule isNSCont_isCont_iff [THEN iffD1])
    3.21  
    3.22  
     4.1 --- a/src/HOL/Nonstandard_Analysis/HLog.thy	Sun Dec 18 22:14:53 2016 +0100
     4.2 +++ b/src/HOL/Nonstandard_Analysis/HLog.thy	Sun Dec 18 23:43:50 2016 +0100
     4.3 @@ -3,154 +3,134 @@
     4.4      Copyright:  2000, 2001 University of Edinburgh
     4.5  *)
     4.6  
     4.7 -section\<open>Logarithms: Non-Standard Version\<close>
     4.8 +section \<open>Logarithms: Non-Standard Version\<close>
     4.9  
    4.10  theory HLog
    4.11 -imports HTranscendental
    4.12 +  imports HTranscendental
    4.13  begin
    4.14  
    4.15  
    4.16  (* should be in NSA.ML *)
    4.17  lemma epsilon_ge_zero [simp]: "0 \<le> \<epsilon>"
    4.18 -by (simp add: epsilon_def star_n_zero_num star_n_le)
    4.19 +  by (simp add: epsilon_def star_n_zero_num star_n_le)
    4.20  
    4.21 -lemma hpfinite_witness: "\<epsilon> : {x. 0 \<le> x & x : HFinite}"
    4.22 -by auto
    4.23 +lemma hpfinite_witness: "\<epsilon> \<in> {x. 0 \<le> x \<and> x \<in> HFinite}"
    4.24 +  by auto
    4.25  
    4.26  
    4.27 -definition
    4.28 -  powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80) where
    4.29 -  [transfer_unfold]: "x powhr a = starfun2 (op powr) x a"
    4.30 -  
    4.31 -definition
    4.32 -  hlog :: "[hypreal,hypreal] => hypreal" where
    4.33 -  [transfer_unfold]: "hlog a x = starfun2 log a x"
    4.34 +definition powhr :: "hypreal \<Rightarrow> hypreal \<Rightarrow> hypreal"  (infixr "powhr" 80)
    4.35 +  where [transfer_unfold]: "x powhr a = starfun2 (op powr) x a"
    4.36 +
    4.37 +definition hlog :: "hypreal \<Rightarrow> hypreal \<Rightarrow> hypreal"
    4.38 +  where [transfer_unfold]: "hlog a x = starfun2 log a x"
    4.39 +
    4.40 +lemma powhr: "(star_n X) powhr (star_n Y) = star_n (\<lambda>n. (X n) powr (Y n))"
    4.41 +  by (simp add: powhr_def starfun2_star_n)
    4.42  
    4.43 -lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
    4.44 -by (simp add: powhr_def starfun2_star_n)
    4.45 -
    4.46 -lemma powhr_one_eq_one [simp]: "!!a. 1 powhr a = 1"
    4.47 -by (transfer, simp)
    4.48 +lemma powhr_one_eq_one [simp]: "\<And>a. 1 powhr a = 1"
    4.49 +  by transfer simp
    4.50  
    4.51 -lemma powhr_mult:
    4.52 -  "!!a x y. [| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)"
    4.53 -by (transfer, simp add: powr_mult)
    4.54 +lemma powhr_mult: "\<And>a x y. 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x * y) powhr a = (x powhr a) * (y powhr a)"
    4.55 +  by transfer (simp add: powr_mult)
    4.56  
    4.57 -lemma powhr_gt_zero [simp]: "!!a x. 0 < x powhr a \<longleftrightarrow> x \<noteq> 0"
    4.58 -by (transfer, simp)
    4.59 +lemma powhr_gt_zero [simp]: "\<And>a x. 0 < x powhr a \<longleftrightarrow> x \<noteq> 0"
    4.60 +  by transfer simp
    4.61  
    4.62  lemma powhr_not_zero [simp]: "\<And>a x. x powhr a \<noteq> 0 \<longleftrightarrow> x \<noteq> 0"
    4.63 -by transfer simp
    4.64 -
    4.65 -lemma powhr_divide:
    4.66 -  "!!a x y. [| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
    4.67 -by (transfer, rule powr_divide)
    4.68 +  by transfer simp
    4.69  
    4.70 -lemma powhr_add: "!!a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
    4.71 -by (transfer, rule powr_add)
    4.72 +lemma powhr_divide: "\<And>a x y. 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powhr a = (x powhr a) / (y powhr a)"
    4.73 +  by transfer (rule powr_divide)
    4.74  
    4.75 -lemma powhr_powhr: "!!a b x. (x powhr a) powhr b = x powhr (a * b)"
    4.76 -by (transfer, rule powr_powr)
    4.77 +lemma powhr_add: "\<And>a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
    4.78 +  by transfer (rule powr_add)
    4.79  
    4.80 -lemma powhr_powhr_swap: "!!a b x. (x powhr a) powhr b = (x powhr b) powhr a"
    4.81 -by (transfer, rule powr_powr_swap)
    4.82 +lemma powhr_powhr: "\<And>a b x. (x powhr a) powhr b = x powhr (a * b)"
    4.83 +  by transfer (rule powr_powr)
    4.84  
    4.85 -lemma powhr_minus: "!!a x. x powhr (-a) = inverse (x powhr a)"
    4.86 -by (transfer, rule powr_minus)
    4.87 +lemma powhr_powhr_swap: "\<And>a b x. (x powhr a) powhr b = (x powhr b) powhr a"
    4.88 +  by transfer (rule powr_powr_swap)
    4.89  
    4.90 -lemma powhr_minus_divide: "x powhr (-a) = 1/(x powhr a)"
    4.91 -by (simp add: divide_inverse powhr_minus)
    4.92 +lemma powhr_minus: "\<And>a x. x powhr (- a) = inverse (x powhr a)"
    4.93 +  by transfer (rule powr_minus)
    4.94  
    4.95 -lemma powhr_less_mono: "!!a b x. [| a < b; 1 < x |] ==> x powhr a < x powhr b"
    4.96 -by (transfer, simp)
    4.97 +lemma powhr_minus_divide: "x powhr (- a) = 1 / (x powhr a)"
    4.98 +  by (simp add: divide_inverse powhr_minus)
    4.99  
   4.100 -lemma powhr_less_cancel: "!!a b x. [| x powhr a < x powhr b; 1 < x |] ==> a < b"
   4.101 -by (transfer, simp)
   4.102 +lemma powhr_less_mono: "\<And>a b x. a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powhr a < x powhr b"
   4.103 +  by transfer simp
   4.104 +
   4.105 +lemma powhr_less_cancel: "\<And>a b x. x powhr a < x powhr b \<Longrightarrow> 1 < x \<Longrightarrow> a < b"
   4.106 +  by transfer simp
   4.107  
   4.108 -lemma powhr_less_cancel_iff [simp]:
   4.109 -     "1 < x ==> (x powhr a < x powhr b) = (a < b)"
   4.110 -by (blast intro: powhr_less_cancel powhr_less_mono)
   4.111 +lemma powhr_less_cancel_iff [simp]: "1 < x \<Longrightarrow> x powhr a < x powhr b \<longleftrightarrow> a < b"
   4.112 +  by (blast intro: powhr_less_cancel powhr_less_mono)
   4.113  
   4.114 -lemma powhr_le_cancel_iff [simp]:
   4.115 -     "1 < x ==> (x powhr a \<le> x powhr b) = (a \<le> b)"
   4.116 -by (simp add: linorder_not_less [symmetric])
   4.117 +lemma powhr_le_cancel_iff [simp]: "1 < x \<Longrightarrow> x powhr a \<le> x powhr b \<longleftrightarrow> a \<le> b"
   4.118 +  by (simp add: linorder_not_less [symmetric])
   4.119  
   4.120 -lemma hlog:
   4.121 -     "hlog (star_n X) (star_n Y) =  
   4.122 -      star_n (%n. log (X n) (Y n))"
   4.123 -by (simp add: hlog_def starfun2_star_n)
   4.124 +lemma hlog: "hlog (star_n X) (star_n Y) = star_n (\<lambda>n. log (X n) (Y n))"
   4.125 +  by (simp add: hlog_def starfun2_star_n)
   4.126  
   4.127 -lemma hlog_starfun_ln: "!!x. ( *f* ln) x = hlog (( *f* exp) 1) x"
   4.128 -by (transfer, rule log_ln)
   4.129 +lemma hlog_starfun_ln: "\<And>x. ( *f* ln) x = hlog (( *f* exp) 1) x"
   4.130 +  by transfer (rule log_ln)
   4.131  
   4.132 -lemma powhr_hlog_cancel [simp]:
   4.133 -     "!!a x. [| 0 < a; a \<noteq> 1; 0 < x |] ==> a powhr (hlog a x) = x"
   4.134 -by (transfer, simp)
   4.135 +lemma powhr_hlog_cancel [simp]: "\<And>a x. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> a powhr (hlog a x) = x"
   4.136 +  by transfer simp
   4.137  
   4.138 -lemma hlog_powhr_cancel [simp]:
   4.139 -     "!!a y. [| 0 < a; a \<noteq> 1 |] ==> hlog a (a powhr y) = y"
   4.140 -by (transfer, simp)
   4.141 +lemma hlog_powhr_cancel [simp]: "\<And>a y. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> hlog a (a powhr y) = y"
   4.142 +  by transfer simp
   4.143  
   4.144  lemma hlog_mult:
   4.145 -     "!!a x y. [| 0 < a; a \<noteq> 1; 0 < x; 0 < y  |]  
   4.146 -      ==> hlog a (x * y) = hlog a x + hlog a y"
   4.147 -by (transfer, rule log_mult)
   4.148 +  "\<And>a x y. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a (x * y) = hlog a x + hlog a y"
   4.149 +  by transfer (rule log_mult)
   4.150  
   4.151 -lemma hlog_as_starfun:
   4.152 -     "!!a x. [| 0 < a; a \<noteq> 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
   4.153 -by (transfer, simp add: log_def)
   4.154 +lemma hlog_as_starfun: "\<And>a x. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> hlog a x = ( *f* ln) x / ( *f* ln) a"
   4.155 +  by transfer (simp add: log_def)
   4.156  
   4.157  lemma hlog_eq_div_starfun_ln_mult_hlog:
   4.158 -     "!!a b x. [| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]  
   4.159 -      ==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x"
   4.160 -by (transfer, rule log_eq_div_ln_mult_log)
   4.161 +  "\<And>a b x. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow>
   4.162 +    hlog a x = (( *f* ln) b / ( *f* ln) a) * hlog b x"
   4.163 +  by transfer (rule log_eq_div_ln_mult_log)
   4.164  
   4.165 -lemma powhr_as_starfun: "!!a x. x powhr a = (if x=0 then 0 else ( *f* exp) (a * ( *f* real_ln) x))"
   4.166 -  by (transfer, simp add: powr_def)
   4.167 +lemma powhr_as_starfun: "\<And>a x. x powhr a = (if x = 0 then 0 else ( *f* exp) (a * ( *f* real_ln) x))"
   4.168 +  by transfer (simp add: powr_def)
   4.169  
   4.170  lemma HInfinite_powhr:
   4.171 -     "[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal;  
   4.172 -         0 < a |] ==> x powhr a : HInfinite"
   4.173 -apply (auto intro!: starfun_ln_ge_zero starfun_ln_HInfinite HInfinite_HFinite_not_Infinitesimal_mult2 starfun_exp_HInfinite 
   4.174 -       simp add: order_less_imp_le HInfinite_gt_zero_gt_one powhr_as_starfun zero_le_mult_iff)
   4.175 -done
   4.176 +  "x \<in> HInfinite \<Longrightarrow> 0 < x \<Longrightarrow> a \<in> HFinite - Infinitesimal \<Longrightarrow> 0 < a \<Longrightarrow> x powhr a \<in> HInfinite"
   4.177 +  by (auto intro!: starfun_ln_ge_zero starfun_ln_HInfinite
   4.178 +        HInfinite_HFinite_not_Infinitesimal_mult2 starfun_exp_HInfinite
   4.179 +      simp add: order_less_imp_le HInfinite_gt_zero_gt_one powhr_as_starfun zero_le_mult_iff)
   4.180  
   4.181  lemma hlog_hrabs_HInfinite_Infinitesimal:
   4.182 -     "[| x : HFinite - Infinitesimal; a : HInfinite; 0 < a |]  
   4.183 -      ==> hlog a \<bar>x\<bar> : Infinitesimal"
   4.184 -apply (frule HInfinite_gt_zero_gt_one)
   4.185 -apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
   4.186 -            HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2 
   4.187 -        simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero 
   4.188 -          hlog_as_starfun divide_inverse)
   4.189 -done
   4.190 +  "x \<in> HFinite - Infinitesimal \<Longrightarrow> a \<in> HInfinite \<Longrightarrow> 0 < a \<Longrightarrow> hlog a \<bar>x\<bar> \<in> Infinitesimal"
   4.191 +  apply (frule HInfinite_gt_zero_gt_one)
   4.192 +   apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
   4.193 +      HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2
   4.194 +      simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero
   4.195 +      hlog_as_starfun divide_inverse)
   4.196 +  done
   4.197  
   4.198 -lemma hlog_HInfinite_as_starfun:
   4.199 -     "[| a : HInfinite; 0 < a |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
   4.200 -by (rule hlog_as_starfun, auto)
   4.201 +lemma hlog_HInfinite_as_starfun: "a \<in> HInfinite \<Longrightarrow> 0 < a \<Longrightarrow> hlog a x = ( *f* ln) x / ( *f* ln) a"
   4.202 +  by (rule hlog_as_starfun) auto
   4.203  
   4.204 -lemma hlog_one [simp]: "!!a. hlog a 1 = 0"
   4.205 -by (transfer, simp)
   4.206 +lemma hlog_one [simp]: "\<And>a. hlog a 1 = 0"
   4.207 +  by transfer simp
   4.208  
   4.209 -lemma hlog_eq_one [simp]: "!!a. [| 0 < a; a \<noteq> 1 |] ==> hlog a a = 1"
   4.210 -by (transfer, rule log_eq_one)
   4.211 +lemma hlog_eq_one [simp]: "\<And>a. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> hlog a a = 1"
   4.212 +  by transfer (rule log_eq_one)
   4.213  
   4.214 -lemma hlog_inverse:
   4.215 -     "[| 0 < a; a \<noteq> 1; 0 < x |] ==> hlog a (inverse x) = - hlog a x"
   4.216 -apply (rule add_left_cancel [of "hlog a x", THEN iffD1])
   4.217 -apply (simp add: hlog_mult [symmetric])
   4.218 -done
   4.219 +lemma hlog_inverse: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> hlog a (inverse x) = - hlog a x"
   4.220 +  by (rule add_left_cancel [of "hlog a x", THEN iffD1]) (simp add: hlog_mult [symmetric])
   4.221  
   4.222 -lemma hlog_divide:
   4.223 -     "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> hlog a (x/y) = hlog a x - hlog a y"
   4.224 -by (simp add: hlog_mult hlog_inverse divide_inverse)
   4.225 +lemma hlog_divide: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a (x / y) = hlog a x - hlog a y"
   4.226 +  by (simp add: hlog_mult hlog_inverse divide_inverse)
   4.227  
   4.228  lemma hlog_less_cancel_iff [simp]:
   4.229 -     "!!a x y. [| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
   4.230 -by (transfer, simp)
   4.231 +  "\<And>a x y. 1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a x < hlog a y \<longleftrightarrow> x < y"
   4.232 +  by transfer simp
   4.233  
   4.234 -lemma hlog_le_cancel_iff [simp]:
   4.235 -     "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x \<le> hlog a y) = (x \<le> y)"
   4.236 -by (simp add: linorder_not_less [symmetric])
   4.237 +lemma hlog_le_cancel_iff [simp]: "1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a x \<le> hlog a y \<longleftrightarrow> x \<le> y"
   4.238 +  by (simp add: linorder_not_less [symmetric])
   4.239  
   4.240  end
     5.1 --- a/src/HOL/Nonstandard_Analysis/HSEQ.thy	Sun Dec 18 22:14:53 2016 +0100
     5.2 +++ b/src/HOL/Nonstandard_Analysis/HSEQ.thy	Sun Dec 18 23:43:50 2016 +0100
     5.3 @@ -15,434 +15,431 @@
     5.4    abbrevs "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
     5.5  begin
     5.6  
     5.7 -definition
     5.8 -  NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
     5.9 +definition NSLIMSEQ :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool"
    5.10      ("((_)/ \<longlonglongrightarrow>\<^sub>N\<^sub>S (_))" [60, 60] 60) where
    5.11      \<comment>\<open>Nonstandard definition of convergence of sequence\<close>
    5.12 -  "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
    5.13 +  "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
    5.14  
    5.15 -definition
    5.16 -  nslim :: "(nat => 'a::real_normed_vector) => 'a" where
    5.17 -    \<comment>\<open>Nonstandard definition of limit using choice operator\<close>
    5.18 -  "nslim X = (THE L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
    5.19 +definition nslim :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a"
    5.20 +  where "nslim X = (THE L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
    5.21 +  \<comment> \<open>Nonstandard definition of limit using choice operator\<close>
    5.22 +
    5.23  
    5.24 -definition
    5.25 -  NSconvergent :: "(nat => 'a::real_normed_vector) => bool" where
    5.26 -    \<comment>\<open>Nonstandard definition of convergence\<close>
    5.27 -  "NSconvergent X = (\<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
    5.28 +definition NSconvergent :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool"
    5.29 +  where "NSconvergent X \<longleftrightarrow> (\<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
    5.30 +  \<comment> \<open>Nonstandard definition of convergence\<close>
    5.31  
    5.32 -definition
    5.33 -  NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
    5.34 -    \<comment>\<open>Nonstandard definition for bounded sequence\<close>
    5.35 -  "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
    5.36 +definition NSBseq :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool"
    5.37 +  where "NSBseq X \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<in> HFinite)"
    5.38 +  \<comment> \<open>Nonstandard definition for bounded sequence\<close>
    5.39 +
    5.40  
    5.41 -definition
    5.42 -  NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where
    5.43 -    \<comment>\<open>Nonstandard definition\<close>
    5.44 -  "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
    5.45 +definition NSCauchy :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool"
    5.46 +  where "NSCauchy X \<longleftrightarrow> (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
    5.47 +  \<comment> \<open>Nonstandard definition\<close>
    5.48 +
    5.49  
    5.50  subsection \<open>Limits of Sequences\<close>
    5.51  
    5.52 -lemma NSLIMSEQ_iff:
    5.53 -    "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
    5.54 -by (simp add: NSLIMSEQ_def)
    5.55 +lemma NSLIMSEQ_iff: "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S L) \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
    5.56 +  by (simp add: NSLIMSEQ_def)
    5.57 +
    5.58 +lemma NSLIMSEQ_I: "(\<And>N. N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L) \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
    5.59 +  by (simp add: NSLIMSEQ_def)
    5.60  
    5.61 -lemma NSLIMSEQ_I:
    5.62 -  "(\<And>N. N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L) \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
    5.63 -by (simp add: NSLIMSEQ_def)
    5.64 +lemma NSLIMSEQ_D: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L"
    5.65 +  by (simp add: NSLIMSEQ_def)
    5.66  
    5.67 -lemma NSLIMSEQ_D:
    5.68 -  "\<lbrakk>X \<longlonglongrightarrow>\<^sub>N\<^sub>S L; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X N \<approx> star_of L"
    5.69 -by (simp add: NSLIMSEQ_def)
    5.70 +lemma NSLIMSEQ_const: "(\<lambda>n. k) \<longlonglongrightarrow>\<^sub>N\<^sub>S k"
    5.71 +  by (simp add: NSLIMSEQ_def)
    5.72  
    5.73 -lemma NSLIMSEQ_const: "(%n. k) \<longlonglongrightarrow>\<^sub>N\<^sub>S k"
    5.74 -by (simp add: NSLIMSEQ_def)
    5.75 +lemma NSLIMSEQ_add: "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"
    5.76 +  by (auto intro: approx_add simp add: NSLIMSEQ_def)
    5.77  
    5.78 -lemma NSLIMSEQ_add:
    5.79 -      "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> (%n. X n + Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + b"
    5.80 -by (auto intro: approx_add simp add: NSLIMSEQ_def starfun_add [symmetric])
    5.81 +lemma NSLIMSEQ_add_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. f n + b) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + b"
    5.82 +  by (simp only: NSLIMSEQ_add NSLIMSEQ_const)
    5.83  
    5.84 -lemma NSLIMSEQ_add_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a ==> (%n.(f n + b)) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + b"
    5.85 -by (simp only: NSLIMSEQ_add NSLIMSEQ_const)
    5.86 +lemma NSLIMSEQ_mult: "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"
    5.87 +  for a b :: "'a::real_normed_algebra"
    5.88 +  by (auto intro!: approx_mult_HFinite simp add: NSLIMSEQ_def)
    5.89  
    5.90 -lemma NSLIMSEQ_mult:
    5.91 -  fixes a b :: "'a::real_normed_algebra"
    5.92 -  shows "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> (%n. X n * Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a * b"
    5.93 -by (auto intro!: approx_mult_HFinite simp add: NSLIMSEQ_def)
    5.94 +lemma NSLIMSEQ_minus: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. - X n) \<longlonglongrightarrow>\<^sub>N\<^sub>S - a"
    5.95 +  by (auto simp add: NSLIMSEQ_def)
    5.96  
    5.97 -lemma NSLIMSEQ_minus: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a ==> (%n. -(X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S -a"
    5.98 -by (auto simp add: NSLIMSEQ_def)
    5.99 +lemma NSLIMSEQ_minus_cancel: "(\<lambda>n. - X n) \<longlonglongrightarrow>\<^sub>N\<^sub>S -a \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S a"
   5.100 +  by (drule NSLIMSEQ_minus) simp
   5.101  
   5.102 -lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S -a ==> X \<longlonglongrightarrow>\<^sub>N\<^sub>S a"
   5.103 -by (drule NSLIMSEQ_minus, simp)
   5.104 -
   5.105 -lemma NSLIMSEQ_diff:
   5.106 -     "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> (%n. X n - Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b"
   5.107 +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"
   5.108    using NSLIMSEQ_add [of X a "- Y" "- b"] by (simp add: NSLIMSEQ_minus fun_Compl_def)
   5.109  
   5.110  (* FIXME: delete *)
   5.111 -lemma NSLIMSEQ_add_minus:
   5.112 -     "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> (%n. X n + -Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + -b"
   5.113 +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"
   5.114    by (simp add: NSLIMSEQ_diff)
   5.115  
   5.116 -lemma NSLIMSEQ_diff_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a ==> (%n.(f n - b)) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b"
   5.117 -by (simp add: NSLIMSEQ_diff NSLIMSEQ_const)
   5.118 +lemma NSLIMSEQ_diff_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. f n - b) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b"
   5.119 +  by (simp add: NSLIMSEQ_diff NSLIMSEQ_const)
   5.120  
   5.121 -lemma NSLIMSEQ_inverse:
   5.122 -  fixes a :: "'a::real_normed_div_algebra"
   5.123 -  shows "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a;  a ~= 0 |] ==> (%n. inverse(X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S inverse(a)"
   5.124 -by (simp add: NSLIMSEQ_def star_of_approx_inverse)
   5.125 +lemma NSLIMSEQ_inverse: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (\<lambda>n. inverse (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S inverse a"
   5.126 +  for a :: "'a::real_normed_div_algebra"
   5.127 +  by (simp add: NSLIMSEQ_def star_of_approx_inverse)
   5.128  
   5.129 -lemma NSLIMSEQ_mult_inverse:
   5.130 -  fixes a b :: "'a::real_normed_field"
   5.131 -  shows
   5.132 -     "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a;  Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b;  b ~= 0 |] ==> (%n. X n / Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a/b"
   5.133 -by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
   5.134 +lemma NSLIMSEQ_mult_inverse: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> (\<lambda>n. X n / Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a / b"
   5.135 +  for a b :: "'a::real_normed_field"
   5.136 +  by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
   5.137  
   5.138  lemma starfun_hnorm: "\<And>x. hnorm (( *f* f) x) = ( *f* (\<lambda>x. norm (f x))) x"
   5.139 -by transfer simp
   5.140 +  by transfer simp
   5.141  
   5.142  lemma NSLIMSEQ_norm: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S norm a"
   5.143 -by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)
   5.144 -
   5.145 -text\<open>Uniqueness of limit\<close>
   5.146 -lemma NSLIMSEQ_unique: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; X \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> a = b"
   5.147 -apply (simp add: NSLIMSEQ_def)
   5.148 -apply (drule HNatInfinite_whn [THEN [2] bspec])+
   5.149 -apply (auto dest: approx_trans3)
   5.150 -done
   5.151 +  by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)
   5.152  
   5.153 -lemma NSLIMSEQ_pow [rule_format]:
   5.154 -  fixes a :: "'a::{real_normed_algebra,power}"
   5.155 -  shows "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S a) --> ((%n. (X n) ^ m) \<longlonglongrightarrow>\<^sub>N\<^sub>S a ^ m)"
   5.156 -apply (induct "m")
   5.157 -apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)
   5.158 -done
   5.159 +text \<open>Uniqueness of limit.\<close>
   5.160 +lemma NSLIMSEQ_unique: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> a = b"
   5.161 +  apply (simp add: NSLIMSEQ_def)
   5.162 +  apply (drule HNatInfinite_whn [THEN [2] bspec])+
   5.163 +  apply (auto dest: approx_trans3)
   5.164 +  done
   5.165  
   5.166 -text\<open>We can now try and derive a few properties of sequences,
   5.167 -     starting with the limit comparison property for sequences.\<close>
   5.168 +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)"
   5.169 +  for a :: "'a::{real_normed_algebra,power}"
   5.170 +  by (induct m) (auto intro: NSLIMSEQ_mult NSLIMSEQ_const)
   5.171 +
   5.172 +text \<open>We can now try and derive a few properties of sequences,
   5.173 +  starting with the limit comparison property for sequences.\<close>
   5.174  
   5.175 -lemma NSLIMSEQ_le:
   5.176 -       "[| f \<longlonglongrightarrow>\<^sub>N\<^sub>S l; g \<longlonglongrightarrow>\<^sub>N\<^sub>S m;
   5.177 -           \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n)
   5.178 -        |] ==> l \<le> (m::real)"
   5.179 -apply (simp add: NSLIMSEQ_def, safe)
   5.180 -apply (drule starfun_le_mono)
   5.181 -apply (drule HNatInfinite_whn [THEN [2] bspec])+
   5.182 -apply (drule_tac x = whn in spec)
   5.183 -apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
   5.184 -apply clarify
   5.185 -apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2)
   5.186 -done
   5.187 +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"
   5.188 +  for l m :: real
   5.189 +  apply (simp add: NSLIMSEQ_def, safe)
   5.190 +  apply (drule starfun_le_mono)
   5.191 +  apply (drule HNatInfinite_whn [THEN [2] bspec])+
   5.192 +  apply (drule_tac x = whn in spec)
   5.193 +  apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
   5.194 +  apply clarify
   5.195 +  apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2)
   5.196 +  done
   5.197  
   5.198 -lemma NSLIMSEQ_le_const: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S (r::real); \<forall>n. a \<le> X n |] ==> a \<le> r"
   5.199 -by (erule NSLIMSEQ_le [OF NSLIMSEQ_const], auto)
   5.200 +lemma NSLIMSEQ_le_const: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S r \<Longrightarrow> \<forall>n. a \<le> X n \<Longrightarrow> a \<le> r"
   5.201 +  for a r :: real
   5.202 +  by (erule NSLIMSEQ_le [OF NSLIMSEQ_const]) auto
   5.203  
   5.204 -lemma NSLIMSEQ_le_const2: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a"
   5.205 -by (erule NSLIMSEQ_le [OF _ NSLIMSEQ_const], auto)
   5.206 +lemma NSLIMSEQ_le_const2: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S r \<Longrightarrow> \<forall>n. X n \<le> a \<Longrightarrow> r \<le> a"
   5.207 +  for a r :: real
   5.208 +  by (erule NSLIMSEQ_le [OF _ NSLIMSEQ_const]) auto
   5.209  
   5.210 -text\<open>Shift a convergent series by 1:
   5.211 +text \<open>Shift a convergent series by 1:
   5.212    By the equivalence between Cauchiness and convergence and because
   5.213    the successor of an infinite hypernatural is also infinite.\<close>
   5.214  
   5.215 -lemma NSLIMSEQ_Suc: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l ==> (%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
   5.216 -apply (unfold NSLIMSEQ_def, safe)
   5.217 -apply (drule_tac x="N + 1" in bspec)
   5.218 -apply (erule HNatInfinite_add)
   5.219 -apply (simp add: starfun_shift_one)
   5.220 -done
   5.221 +lemma NSLIMSEQ_Suc: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> (\<lambda>n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
   5.222 +  apply (unfold NSLIMSEQ_def)
   5.223 +  apply safe
   5.224 +  apply (drule_tac x="N + 1" in bspec)
   5.225 +   apply (erule HNatInfinite_add)
   5.226 +  apply (simp add: starfun_shift_one)
   5.227 +  done
   5.228  
   5.229 -lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l ==> f \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
   5.230 -apply (unfold NSLIMSEQ_def, safe)
   5.231 -apply (drule_tac x="N - 1" in bspec) 
   5.232 -apply (erule Nats_1 [THEN [2] HNatInfinite_diff])
   5.233 -apply (simp add: starfun_shift_one one_le_HNatInfinite)
   5.234 -done
   5.235 +lemma NSLIMSEQ_imp_Suc: "(\<lambda>n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
   5.236 +  apply (unfold NSLIMSEQ_def)
   5.237 +  apply safe
   5.238 +  apply (drule_tac x="N - 1" in bspec)
   5.239 +   apply (erule Nats_1 [THEN [2] HNatInfinite_diff])
   5.240 +  apply (simp add: starfun_shift_one one_le_HNatInfinite)
   5.241 +  done
   5.242  
   5.243 -lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S l)"
   5.244 -by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
   5.245 +lemma NSLIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<longleftrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
   5.246 +  by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
   5.247 +
   5.248  
   5.249  subsubsection \<open>Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ}\<close>
   5.250  
   5.251  lemma LIMSEQ_NSLIMSEQ:
   5.252 -  assumes X: "X \<longlonglongrightarrow> L" shows "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
   5.253 +  assumes X: "X \<longlonglongrightarrow> L"
   5.254 +  shows "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
   5.255  proof (rule NSLIMSEQ_I)
   5.256 -  fix N assume N: "N \<in> HNatInfinite"
   5.257 +  fix N
   5.258 +  assume N: "N \<in> HNatInfinite"
   5.259    have "starfun X N - star_of L \<in> Infinitesimal"
   5.260    proof (rule InfinitesimalI2)
   5.261 -    fix r::real assume r: "0 < r"
   5.262 -    from LIMSEQ_D [OF X r]
   5.263 -    obtain no where "\<forall>n\<ge>no. norm (X n - L) < r" ..
   5.264 -    hence "\<forall>n\<ge>star_of no. hnorm (starfun X n - star_of L) < star_of r"
   5.265 +    fix r :: real
   5.266 +    assume r: "0 < r"
   5.267 +    from LIMSEQ_D [OF X r] obtain no where "\<forall>n\<ge>no. norm (X n - L) < r" ..
   5.268 +    then have "\<forall>n\<ge>star_of no. hnorm (starfun X n - star_of L) < star_of r"
   5.269        by transfer
   5.270 -    thus "hnorm (starfun X N - star_of L) < star_of r"
   5.271 +    then show "hnorm (starfun X N - star_of L) < star_of r"
   5.272        using N by (simp add: star_of_le_HNatInfinite)
   5.273    qed
   5.274 -  thus "starfun X N \<approx> star_of L"
   5.275 -    by (unfold approx_def)
   5.276 +  then show "starfun X N \<approx> star_of L"
   5.277 +    by (simp only: approx_def)
   5.278  qed
   5.279  
   5.280  lemma NSLIMSEQ_LIMSEQ:
   5.281 -  assumes X: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L" shows "X \<longlonglongrightarrow> L"
   5.282 +  assumes X: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
   5.283 +  shows "X \<longlonglongrightarrow> L"
   5.284  proof (rule LIMSEQ_I)
   5.285 -  fix r::real assume r: "0 < r"
   5.286 +  fix r :: real
   5.287 +  assume r: "0 < r"
   5.288    have "\<exists>no. \<forall>n\<ge>no. hnorm (starfun X n - star_of L) < star_of r"
   5.289    proof (intro exI allI impI)
   5.290 -    fix n assume "whn \<le> n"
   5.291 +    fix n
   5.292 +    assume "whn \<le> n"
   5.293      with HNatInfinite_whn have "n \<in> HNatInfinite"
   5.294        by (rule HNatInfinite_upward_closed)
   5.295      with X have "starfun X n \<approx> star_of L"
   5.296        by (rule NSLIMSEQ_D)
   5.297 -    hence "starfun X n - star_of L \<in> Infinitesimal"
   5.298 -      by (unfold approx_def)
   5.299 -    thus "hnorm (starfun X n - star_of L) < star_of r"
   5.300 +    then have "starfun X n - star_of L \<in> Infinitesimal"
   5.301 +      by (simp only: approx_def)
   5.302 +    then show "hnorm (starfun X n - star_of L) < star_of r"
   5.303        using r by (rule InfinitesimalD2)
   5.304    qed
   5.305 -  thus "\<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
   5.306 +  then show "\<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
   5.307      by transfer
   5.308  qed
   5.309  
   5.310 -theorem LIMSEQ_NSLIMSEQ_iff: "(f \<longlonglongrightarrow> L) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
   5.311 -by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
   5.312 +theorem LIMSEQ_NSLIMSEQ_iff: "f \<longlonglongrightarrow> L \<longleftrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
   5.313 +  by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
   5.314 +
   5.315  
   5.316  subsubsection \<open>Derived theorems about @{term NSLIMSEQ}\<close>
   5.317  
   5.318 -text\<open>We prove the NS version from the standard one, since the NS proof
   5.319 -   seems more complicated than the standard one above!\<close>
   5.320 -lemma NSLIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0) = (X \<longlonglongrightarrow>\<^sub>N\<^sub>S 0)"
   5.321 -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_norm_zero_iff)
   5.322 +text \<open>We prove the NS version from the standard one, since the NS proof
   5.323 +  seems more complicated than the standard one above!\<close>
   5.324 +lemma NSLIMSEQ_norm_zero: "(\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0 \<longleftrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   5.325 +  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_norm_zero_iff)
   5.326  
   5.327 -lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S (0::real))"
   5.328 -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_rabs_zero_iff)
   5.329 -
   5.330 -text\<open>Generalization to other limits\<close>
   5.331 -lemma NSLIMSEQ_imp_rabs: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S (l::real) ==> (%n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S \<bar>l\<bar>"
   5.332 -apply (simp add: NSLIMSEQ_def)
   5.333 -apply (auto intro: approx_hrabs 
   5.334 -            simp add: starfun_abs)
   5.335 -done
   5.336 +lemma NSLIMSEQ_rabs_zero: "(\<lambda>n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0 \<longleftrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S (0::real)"
   5.337 +  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_rabs_zero_iff)
   5.338  
   5.339 -lemma NSLIMSEQ_inverse_zero:
   5.340 -     "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n)
   5.341 -      ==> (%n. inverse(f n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   5.342 -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
   5.343 +text \<open>Generalization to other limits.\<close>
   5.344 +lemma NSLIMSEQ_imp_rabs: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> (\<lambda>n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S \<bar>l\<bar>"
   5.345 +  for l :: real
   5.346 +  by (simp add: NSLIMSEQ_def) (auto intro: approx_hrabs simp add: starfun_abs)
   5.347 +
   5.348 +lemma NSLIMSEQ_inverse_zero: "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f n \<Longrightarrow> (\<lambda>n. inverse (f n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   5.349 +  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
   5.350  
   5.351 -lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   5.352 -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat del: of_nat_Suc)
   5.353 +lemma NSLIMSEQ_inverse_real_of_nat: "(\<lambda>n. inverse (real (Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   5.354 +  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat del: of_nat_Suc)
   5.355  
   5.356 -lemma NSLIMSEQ_inverse_real_of_nat_add:
   5.357 -     "(%n. r + inverse(real(Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
   5.358 -by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add del: of_nat_Suc)
   5.359 +lemma NSLIMSEQ_inverse_real_of_nat_add: "(\<lambda>n. r + inverse (real (Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
   5.360 +  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add del: of_nat_Suc)
   5.361  
   5.362 -lemma NSLIMSEQ_inverse_real_of_nat_add_minus:
   5.363 -     "(%n. r + -inverse(real(Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
   5.364 +lemma NSLIMSEQ_inverse_real_of_nat_add_minus: "(\<lambda>n. r + - inverse (real (Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
   5.365    using LIMSEQ_inverse_real_of_nat_add_minus by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
   5.366  
   5.367  lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult:
   5.368 -     "(%n. r*( 1 + -inverse(real(Suc n)))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
   5.369 -  using LIMSEQ_inverse_real_of_nat_add_minus_mult by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
   5.370 +  "(\<lambda>n. r * (1 + - inverse (real (Suc n)))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
   5.371 +  using LIMSEQ_inverse_real_of_nat_add_minus_mult
   5.372 +  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
   5.373  
   5.374  
   5.375  subsection \<open>Convergence\<close>
   5.376  
   5.377 -lemma nslimI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L ==> nslim X = L"
   5.378 -apply (simp add: nslim_def)
   5.379 -apply (blast intro: NSLIMSEQ_unique)
   5.380 -done
   5.381 +lemma nslimI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> nslim X = L"
   5.382 +  by (simp add: nslim_def) (blast intro: NSLIMSEQ_unique)
   5.383  
   5.384  lemma lim_nslim_iff: "lim X = nslim X"
   5.385 -by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)
   5.386 +  by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)
   5.387  
   5.388 -lemma NSconvergentD: "NSconvergent X ==> \<exists>L. (X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
   5.389 -by (simp add: NSconvergent_def)
   5.390 +lemma NSconvergentD: "NSconvergent X \<Longrightarrow> \<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
   5.391 +  by (simp add: NSconvergent_def)
   5.392  
   5.393 -lemma NSconvergentI: "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S L) ==> NSconvergent X"
   5.394 -by (auto simp add: NSconvergent_def)
   5.395 +lemma NSconvergentI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> NSconvergent X"
   5.396 +  by (auto simp add: NSconvergent_def)
   5.397  
   5.398  lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X"
   5.399 -by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)
   5.400 +  by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)
   5.401  
   5.402 -lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X = (X \<longlonglongrightarrow>\<^sub>N\<^sub>S nslim X)"
   5.403 -by (auto intro: theI NSLIMSEQ_unique simp add: NSconvergent_def nslim_def)
   5.404 +lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X \<longleftrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S nslim X"
   5.405 +  by (auto intro: theI NSLIMSEQ_unique simp add: NSconvergent_def nslim_def)
   5.406  
   5.407  
   5.408  subsection \<open>Bounded Monotonic Sequences\<close>
   5.409  
   5.410 -lemma NSBseqD: "[| NSBseq X;  N: HNatInfinite |] ==> ( *f* X) N : HFinite"
   5.411 -by (simp add: NSBseq_def)
   5.412 +lemma NSBseqD: "NSBseq X \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> ( *f* X) N \<in> HFinite"
   5.413 +  by (simp add: NSBseq_def)
   5.414  
   5.415  lemma Standard_subset_HFinite: "Standard \<subseteq> HFinite"
   5.416 -unfolding Standard_def by auto
   5.417 +  by (auto simp: Standard_def)
   5.418  
   5.419  lemma NSBseqD2: "NSBseq X \<Longrightarrow> ( *f* X) N \<in> HFinite"
   5.420 -apply (cases "N \<in> HNatInfinite")
   5.421 -apply (erule (1) NSBseqD)
   5.422 -apply (rule subsetD [OF Standard_subset_HFinite])
   5.423 -apply (simp add: HNatInfinite_def Nats_eq_Standard)
   5.424 -done
   5.425 +  apply (cases "N \<in> HNatInfinite")
   5.426 +   apply (erule (1) NSBseqD)
   5.427 +  apply (rule subsetD [OF Standard_subset_HFinite])
   5.428 +  apply (simp add: HNatInfinite_def Nats_eq_Standard)
   5.429 +  done
   5.430  
   5.431 -lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite ==> NSBseq X"
   5.432 -by (simp add: NSBseq_def)
   5.433 -
   5.434 -text\<open>The standard definition implies the nonstandard definition\<close>
   5.435 +lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N \<in> HFinite \<Longrightarrow> NSBseq X"
   5.436 +  by (simp add: NSBseq_def)
   5.437  
   5.438 -lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
   5.439 -proof (unfold NSBseq_def, safe)
   5.440 +text \<open>The standard definition implies the nonstandard definition.\<close>
   5.441 +lemma Bseq_NSBseq: "Bseq X \<Longrightarrow> NSBseq X"
   5.442 +  unfolding NSBseq_def
   5.443 +proof safe
   5.444    assume X: "Bseq X"
   5.445 -  fix N assume N: "N \<in> HNatInfinite"
   5.446 -  from BseqD [OF X] obtain K where "\<forall>n. norm (X n) \<le> K" by fast
   5.447 -  hence "\<forall>N. hnorm (starfun X N) \<le> star_of K" by transfer
   5.448 -  hence "hnorm (starfun X N) \<le> star_of K" by simp
   5.449 -  also have "star_of K < star_of (K + 1)" by simp
   5.450 -  finally have "\<exists>x\<in>Reals. hnorm (starfun X N) < x" by (rule bexI, simp)
   5.451 -  thus "starfun X N \<in> HFinite" by (simp add: HFinite_def)
   5.452 +  fix N
   5.453 +  assume N: "N \<in> HNatInfinite"
   5.454 +  from BseqD [OF X] obtain K where "\<forall>n. norm (X n) \<le> K"
   5.455 +    by fast
   5.456 +  then have "\<forall>N. hnorm (starfun X N) \<le> star_of K"
   5.457 +    by transfer
   5.458 +  then have "hnorm (starfun X N) \<le> star_of K"
   5.459 +    by simp
   5.460 +  also have "star_of K < star_of (K + 1)"
   5.461 +    by simp
   5.462 +  finally have "\<exists>x\<in>Reals. hnorm (starfun X N) < x"
   5.463 +    by (rule bexI) simp
   5.464 +  then show "starfun X N \<in> HFinite"
   5.465 +    by (simp add: HFinite_def)
   5.466  qed
   5.467  
   5.468 -text\<open>The nonstandard definition implies the standard definition\<close>
   5.469 -
   5.470 +text \<open>The nonstandard definition implies the standard definition.\<close>
   5.471  lemma SReal_less_omega: "r \<in> \<real> \<Longrightarrow> r < \<omega>"
   5.472 -apply (insert HInfinite_omega)
   5.473 -apply (simp add: HInfinite_def)
   5.474 -apply (simp add: order_less_imp_le)
   5.475 -done
   5.476 +  using HInfinite_omega
   5.477 +  by (simp add: HInfinite_def) (simp add: order_less_imp_le)
   5.478  
   5.479  lemma NSBseq_Bseq: "NSBseq X \<Longrightarrow> Bseq X"
   5.480  proof (rule ccontr)
   5.481    let ?n = "\<lambda>K. LEAST n. K < norm (X n)"
   5.482    assume "NSBseq X"
   5.483 -  hence finite: "( *f* X) (( *f* ?n) \<omega>) \<in> HFinite"
   5.484 +  then have finite: "( *f* X) (( *f* ?n) \<omega>) \<in> HFinite"
   5.485      by (rule NSBseqD2)
   5.486    assume "\<not> Bseq X"
   5.487 -  hence "\<forall>K>0. \<exists>n. K < norm (X n)"
   5.488 +  then have "\<forall>K>0. \<exists>n. K < norm (X n)"
   5.489      by (simp add: Bseq_def linorder_not_le)
   5.490 -  hence "\<forall>K>0. K < norm (X (?n K))"
   5.491 +  then have "\<forall>K>0. K < norm (X (?n K))"
   5.492      by (auto intro: LeastI_ex)
   5.493 -  hence "\<forall>K>0. K < hnorm (( *f* X) (( *f* ?n) K))"
   5.494 +  then have "\<forall>K>0. K < hnorm (( *f* X) (( *f* ?n) K))"
   5.495      by transfer
   5.496 -  hence "\<omega> < hnorm (( *f* X) (( *f* ?n) \<omega>))"
   5.497 +  then have "\<omega> < hnorm (( *f* X) (( *f* ?n) \<omega>))"
   5.498      by simp
   5.499 -  hence "\<forall>r\<in>\<real>. r < hnorm (( *f* X) (( *f* ?n) \<omega>))"
   5.500 +  then have "\<forall>r\<in>\<real>. r < hnorm (( *f* X) (( *f* ?n) \<omega>))"
   5.501      by (simp add: order_less_trans [OF SReal_less_omega])
   5.502 -  hence "( *f* X) (( *f* ?n) \<omega>) \<in> HInfinite"
   5.503 +  then have "( *f* X) (( *f* ?n) \<omega>) \<in> HInfinite"
   5.504      by (simp add: HInfinite_def)
   5.505    with finite show "False"
   5.506      by (simp add: HFinite_HInfinite_iff)
   5.507  qed
   5.508  
   5.509 -text\<open>Equivalence of nonstandard and standard definitions
   5.510 -  for a bounded sequence\<close>
   5.511 -lemma Bseq_NSBseq_iff: "(Bseq X) = (NSBseq X)"
   5.512 -by (blast intro!: NSBseq_Bseq Bseq_NSBseq)
   5.513 +text \<open>Equivalence of nonstandard and standard definitions for a bounded sequence.\<close>
   5.514 +lemma Bseq_NSBseq_iff: "Bseq X = NSBseq X"
   5.515 +  by (blast intro!: NSBseq_Bseq Bseq_NSBseq)
   5.516  
   5.517 -text\<open>A convergent sequence is bounded: 
   5.518 - Boundedness as a necessary condition for convergence. 
   5.519 - The nonstandard version has no existential, as usual\<close>
   5.520 +text \<open>A convergent sequence is bounded:
   5.521 +  Boundedness as a necessary condition for convergence.
   5.522 +  The nonstandard version has no existential, as usual.\<close>
   5.523 +lemma NSconvergent_NSBseq: "NSconvergent X \<Longrightarrow> NSBseq X"
   5.524 +  by (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
   5.525 +    (blast intro: HFinite_star_of approx_sym approx_HFinite)
   5.526  
   5.527 -lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X"
   5.528 -apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
   5.529 -apply (blast intro: HFinite_star_of approx_sym approx_HFinite)
   5.530 -done
   5.531 +text \<open>Standard Version: easily now proved using equivalence of NS and
   5.532 + standard definitions.\<close>
   5.533  
   5.534 -text\<open>Standard Version: easily now proved using equivalence of NS and
   5.535 - standard definitions\<close>
   5.536 +lemma convergent_Bseq: "convergent X \<Longrightarrow> Bseq X"
   5.537 +  for X :: "nat \<Rightarrow> 'b::real_normed_vector"
   5.538 +  by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
   5.539  
   5.540 -lemma convergent_Bseq: "convergent X ==> Bseq (X::nat \<Rightarrow> _::real_normed_vector)"
   5.541 -by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
   5.542  
   5.543 -subsubsection\<open>Upper Bounds and Lubs of Bounded Sequences\<close>
   5.544 +subsubsection \<open>Upper Bounds and Lubs of Bounded Sequences\<close>
   5.545  
   5.546 -lemma NSBseq_isUb: "NSBseq X ==> \<exists>U::real. isUb UNIV {x. \<exists>n. X n = x} U"
   5.547 -by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)
   5.548 +lemma NSBseq_isUb: "NSBseq X \<Longrightarrow> \<exists>U::real. isUb UNIV {x. \<exists>n. X n = x} U"
   5.549 +  by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)
   5.550  
   5.551 -lemma NSBseq_isLub: "NSBseq X ==> \<exists>U::real. isLub UNIV {x. \<exists>n. X n = x} U"
   5.552 -by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
   5.553 +lemma NSBseq_isLub: "NSBseq X \<Longrightarrow> \<exists>U::real. isLub UNIV {x. \<exists>n. X n = x} U"
   5.554 +  by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
   5.555 +
   5.556  
   5.557 -subsubsection\<open>A Bounded and Monotonic Sequence Converges\<close>
   5.558 +subsubsection \<open>A Bounded and Monotonic Sequence Converges\<close>
   5.559  
   5.560 -text\<open>The best of both worlds: Easier to prove this result as a standard
   5.561 +text \<open>The best of both worlds: Easier to prove this result as a standard
   5.562     theorem and then use equivalence to "transfer" it into the
   5.563     equivalent nonstandard form if needed!\<close>
   5.564  
   5.565 -lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m ==> \<exists>L. (X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
   5.566 -by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
   5.567 +lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m \<Longrightarrow> \<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
   5.568 +  by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
   5.569  
   5.570 -lemma NSBseq_mono_NSconvergent:
   5.571 -     "[| NSBseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> NSconvergent (X::nat=>real)"
   5.572 -by (auto intro: Bseq_mono_convergent 
   5.573 -         simp add: convergent_NSconvergent_iff [symmetric] 
   5.574 -                   Bseq_NSBseq_iff [symmetric])
   5.575 +lemma NSBseq_mono_NSconvergent: "NSBseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> NSconvergent X"
   5.576 +  for X :: "nat \<Rightarrow> real"
   5.577 +  by (auto intro: Bseq_mono_convergent
   5.578 +      simp: convergent_NSconvergent_iff [symmetric] Bseq_NSBseq_iff [symmetric])
   5.579  
   5.580  
   5.581  subsection \<open>Cauchy Sequences\<close>
   5.582  
   5.583  lemma NSCauchyI:
   5.584 -  "(\<And>M N. \<lbrakk>M \<in> HNatInfinite; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X M \<approx> starfun X N)
   5.585 -   \<Longrightarrow> NSCauchy X"
   5.586 -by (simp add: NSCauchy_def)
   5.587 +  "(\<And>M N. M \<in> HNatInfinite \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> starfun X M \<approx> starfun X N) \<Longrightarrow> NSCauchy X"
   5.588 +  by (simp add: NSCauchy_def)
   5.589  
   5.590  lemma NSCauchyD:
   5.591 -  "\<lbrakk>NSCauchy X; M \<in> HNatInfinite; N \<in> HNatInfinite\<rbrakk>
   5.592 -   \<Longrightarrow> starfun X M \<approx> starfun X N"
   5.593 -by (simp add: NSCauchy_def)
   5.594 +  "NSCauchy X \<Longrightarrow> M \<in> HNatInfinite \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> starfun X M \<approx> starfun X N"
   5.595 +  by (simp add: NSCauchy_def)
   5.596  
   5.597 -subsubsection\<open>Equivalence Between NS and Standard\<close>
   5.598 +
   5.599 +subsubsection \<open>Equivalence Between NS and Standard\<close>
   5.600  
   5.601  lemma Cauchy_NSCauchy:
   5.602 -  assumes X: "Cauchy X" shows "NSCauchy X"
   5.603 +  assumes X: "Cauchy X"
   5.604 +  shows "NSCauchy X"
   5.605  proof (rule NSCauchyI)
   5.606 -  fix M assume M: "M \<in> HNatInfinite"
   5.607 -  fix N assume N: "N \<in> HNatInfinite"
   5.608 +  fix M
   5.609 +  assume M: "M \<in> HNatInfinite"
   5.610 +  fix N
   5.611 +  assume N: "N \<in> HNatInfinite"
   5.612    have "starfun X M - starfun X N \<in> Infinitesimal"
   5.613    proof (rule InfinitesimalI2)
   5.614 -    fix r :: real assume r: "0 < r"
   5.615 -    from CauchyD [OF X r]
   5.616 -    obtain k where "\<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r" ..
   5.617 -    hence "\<forall>m\<ge>star_of k. \<forall>n\<ge>star_of k.
   5.618 -           hnorm (starfun X m - starfun X n) < star_of r"
   5.619 +    fix r :: real
   5.620 +    assume r: "0 < r"
   5.621 +    from CauchyD [OF X r] obtain k where "\<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r" ..
   5.622 +    then have "\<forall>m\<ge>star_of k. \<forall>n\<ge>star_of k. hnorm (starfun X m - starfun X n) < star_of r"
   5.623        by transfer
   5.624 -    thus "hnorm (starfun X M - starfun X N) < star_of r"
   5.625 +    then show "hnorm (starfun X M - starfun X N) < star_of r"
   5.626        using M N by (simp add: star_of_le_HNatInfinite)
   5.627    qed
   5.628 -  thus "starfun X M \<approx> starfun X N"
   5.629 -    by (unfold approx_def)
   5.630 +  then show "starfun X M \<approx> starfun X N"
   5.631 +    by (simp only: approx_def)
   5.632  qed
   5.633  
   5.634  lemma NSCauchy_Cauchy:
   5.635 -  assumes X: "NSCauchy X" shows "Cauchy X"
   5.636 +  assumes X: "NSCauchy X"
   5.637 +  shows "Cauchy X"
   5.638  proof (rule CauchyI)
   5.639 -  fix r::real assume r: "0 < r"
   5.640 +  fix r :: real
   5.641 +  assume r: "0 < r"
   5.642    have "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. hnorm (starfun X m - starfun X n) < star_of r"
   5.643    proof (intro exI allI impI)
   5.644 -    fix M assume "whn \<le> M"
   5.645 +    fix M
   5.646 +    assume "whn \<le> M"
   5.647      with HNatInfinite_whn have M: "M \<in> HNatInfinite"
   5.648        by (rule HNatInfinite_upward_closed)
   5.649 -    fix N assume "whn \<le> N"
   5.650 +    fix N
   5.651 +    assume "whn \<le> N"
   5.652      with HNatInfinite_whn have N: "N \<in> HNatInfinite"
   5.653        by (rule HNatInfinite_upward_closed)
   5.654      from X M N have "starfun X M \<approx> starfun X N"
   5.655        by (rule NSCauchyD)
   5.656 -    hence "starfun X M - starfun X N \<in> Infinitesimal"
   5.657 -      by (unfold approx_def)
   5.658 -    thus "hnorm (starfun X M - starfun X N) < star_of r"
   5.659 +    then have "starfun X M - starfun X N \<in> Infinitesimal"
   5.660 +      by (simp only: approx_def)
   5.661 +    then show "hnorm (starfun X M - starfun X N) < star_of r"
   5.662        using r by (rule InfinitesimalD2)
   5.663    qed
   5.664 -  thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r"
   5.665 +  then show "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r"
   5.666      by transfer
   5.667  qed
   5.668  
   5.669  theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X"
   5.670 -by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
   5.671 +  by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
   5.672 +
   5.673  
   5.674  subsubsection \<open>Cauchy Sequences are Bounded\<close>
   5.675  
   5.676 -text\<open>A Cauchy sequence is bounded -- nonstandard version\<close>
   5.677 +text \<open>A Cauchy sequence is bounded -- nonstandard version.\<close>
   5.678  
   5.679 -lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X"
   5.680 -by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
   5.681 +lemma NSCauchy_NSBseq: "NSCauchy X \<Longrightarrow> NSBseq X"
   5.682 +  by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
   5.683 +
   5.684  
   5.685  subsubsection \<open>Cauchy Sequences are Convergent\<close>
   5.686  
   5.687 -text\<open>Equivalence of Cauchy criterion and convergence:
   5.688 +text \<open>Equivalence of Cauchy criterion and convergence:
   5.689    We will prove this using our NS formulation which provides a
   5.690    much easier proof than using the standard definition. We do not
   5.691    need to use properties of subsequences such as boundedness,
   5.692 @@ -453,64 +450,60 @@
   5.693    since the NS formulations do not involve existential quantifiers.\<close>
   5.694  
   5.695  lemma NSconvergent_NSCauchy: "NSconvergent X \<Longrightarrow> NSCauchy X"
   5.696 -apply (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def, safe)
   5.697 -apply (auto intro: approx_trans2)
   5.698 -done
   5.699 +  by (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def) (auto intro: approx_trans2)
   5.700  
   5.701 -lemma real_NSCauchy_NSconvergent:
   5.702 -  fixes X :: "nat \<Rightarrow> real"
   5.703 -  shows "NSCauchy X \<Longrightarrow> NSconvergent X"
   5.704 -apply (simp add: NSconvergent_def NSLIMSEQ_def)
   5.705 -apply (frule NSCauchy_NSBseq)
   5.706 -apply (simp add: NSBseq_def NSCauchy_def)
   5.707 -apply (drule HNatInfinite_whn [THEN [2] bspec])
   5.708 -apply (drule HNatInfinite_whn [THEN [2] bspec])
   5.709 -apply (auto dest!: st_part_Ex simp add: SReal_iff)
   5.710 -apply (blast intro: approx_trans3)
   5.711 -done
   5.712 +lemma real_NSCauchy_NSconvergent: "NSCauchy X \<Longrightarrow> NSconvergent X"
   5.713 +  for X :: "nat \<Rightarrow> real"
   5.714 +  apply (simp add: NSconvergent_def NSLIMSEQ_def)
   5.715 +  apply (frule NSCauchy_NSBseq)
   5.716 +  apply (simp add: NSBseq_def NSCauchy_def)
   5.717 +  apply (drule HNatInfinite_whn [THEN [2] bspec])
   5.718 +  apply (drule HNatInfinite_whn [THEN [2] bspec])
   5.719 +  apply (auto dest!: st_part_Ex simp add: SReal_iff)
   5.720 +  apply (blast intro: approx_trans3)
   5.721 +  done
   5.722  
   5.723 -lemma NSCauchy_NSconvergent:
   5.724 -  fixes X :: "nat \<Rightarrow> 'a::banach"
   5.725 -  shows "NSCauchy X \<Longrightarrow> NSconvergent X"
   5.726 -apply (drule NSCauchy_Cauchy [THEN Cauchy_convergent])
   5.727 -apply (erule convergent_NSconvergent_iff [THEN iffD1])
   5.728 -done
   5.729 +lemma NSCauchy_NSconvergent: "NSCauchy X \<Longrightarrow> NSconvergent X"
   5.730 +  for X :: "nat \<Rightarrow> 'a::banach"
   5.731 +  apply (drule NSCauchy_Cauchy [THEN Cauchy_convergent])
   5.732 +  apply (erule convergent_NSconvergent_iff [THEN iffD1])
   5.733 +  done
   5.734  
   5.735 -lemma NSCauchy_NSconvergent_iff:
   5.736 -  fixes X :: "nat \<Rightarrow> 'a::banach"
   5.737 -  shows "NSCauchy X = NSconvergent X"
   5.738 -by (fast intro: NSCauchy_NSconvergent NSconvergent_NSCauchy)
   5.739 +lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X"
   5.740 +  for X :: "nat \<Rightarrow> 'a::banach"
   5.741 +  by (fast intro: NSCauchy_NSconvergent NSconvergent_NSCauchy)
   5.742  
   5.743  
   5.744  subsection \<open>Power Sequences\<close>
   5.745  
   5.746 -text\<open>The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
   5.747 -"x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
   5.748 +text \<open>The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
   5.749 +  "x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
   5.750    also fact that bounded and monotonic sequence converges.\<close>
   5.751  
   5.752 -text\<open>We now use NS criterion to bring proof of theorem through\<close>
   5.753 +text \<open>We now use NS criterion to bring proof of theorem through.\<close>
   5.754 +lemma NSLIMSEQ_realpow_zero: "0 \<le> x \<Longrightarrow> x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   5.755 +  for x :: real
   5.756 +  apply (simp add: NSLIMSEQ_def)
   5.757 +  apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
   5.758 +  apply (frule NSconvergentD)
   5.759 +  apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfun_pow)
   5.760 +  apply (frule HNatInfinite_add_one)
   5.761 +  apply (drule bspec, assumption)
   5.762 +  apply (drule bspec, assumption)
   5.763 +  apply (drule_tac x = "N + 1" in bspec, assumption)
   5.764 +  apply (simp add: hyperpow_add)
   5.765 +  apply (drule approx_mult_subst_star_of, assumption)
   5.766 +  apply (drule approx_trans3, assumption)
   5.767 +  apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric])
   5.768 +  done
   5.769  
   5.770 -lemma NSLIMSEQ_realpow_zero:
   5.771 -  "[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   5.772 -apply (simp add: NSLIMSEQ_def)
   5.773 -apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
   5.774 -apply (frule NSconvergentD)
   5.775 -apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfun_pow)
   5.776 -apply (frule HNatInfinite_add_one)
   5.777 -apply (drule bspec, assumption)
   5.778 -apply (drule bspec, assumption)
   5.779 -apply (drule_tac x = "N + (1::hypnat) " in bspec, assumption)
   5.780 -apply (simp add: hyperpow_add)
   5.781 -apply (drule approx_mult_subst_star_of, assumption)
   5.782 -apply (drule approx_trans3, assumption)
   5.783 -apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric])
   5.784 -done
   5.785 +lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   5.786 +  for c :: real
   5.787 +  by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
   5.788  
   5.789 -lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   5.790 -by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
   5.791 -
   5.792 -lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   5.793 -by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
   5.794 +lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   5.795 +  for c :: real
   5.796 +  by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
   5.797  
   5.798  (***---------------------------------------------------------------
   5.799      Theorems proved by Harrison in HOL that we do not need
     6.1 --- a/src/HOL/Nonstandard_Analysis/HSeries.thy	Sun Dec 18 22:14:53 2016 +0100
     6.2 +++ b/src/HOL/Nonstandard_Analysis/HSeries.thy	Sun Dec 18 23:43:50 2016 +0100
     6.3 @@ -5,200 +5,177 @@
     6.4  Converted to Isar and polished by lcp
     6.5  *)
     6.6  
     6.7 -section\<open>Finite Summation and Infinite Series for Hyperreals\<close>
     6.8 +section \<open>Finite Summation and Infinite Series for Hyperreals\<close>
     6.9  
    6.10  theory HSeries
    6.11 -imports HSEQ
    6.12 +  imports HSEQ
    6.13  begin
    6.14  
    6.15 -definition
    6.16 -  sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where
    6.17 -  "sumhr =
    6.18 -      (%(M,N,f). starfun2 (%m n. sum f {m..<n}) M N)"
    6.19 +definition sumhr :: "hypnat \<times> hypnat \<times> (nat \<Rightarrow> real) \<Rightarrow> hypreal"
    6.20 +  where "sumhr = (\<lambda>(M,N,f). starfun2 (\<lambda>m n. sum f {m..<n}) M N)"
    6.21 +
    6.22 +definition NSsums :: "(nat \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool"  (infixr "NSsums" 80)
    6.23 +  where "f NSsums s = (\<lambda>n. sum f {..<n}) \<longlonglongrightarrow>\<^sub>N\<^sub>S s"
    6.24  
    6.25 -definition
    6.26 -  NSsums  :: "[nat=>real,real] => bool"     (infixr "NSsums" 80) where
    6.27 -  "f NSsums s = (%n. sum f {..<n}) \<longlonglongrightarrow>\<^sub>N\<^sub>S s"
    6.28 +definition NSsummable :: "(nat \<Rightarrow> real) \<Rightarrow> bool"
    6.29 +  where "NSsummable f \<longleftrightarrow> (\<exists>s. f NSsums s)"
    6.30  
    6.31 -definition
    6.32 -  NSsummable :: "(nat=>real) => bool" where
    6.33 -  "NSsummable f = (\<exists>s. f NSsums s)"
    6.34 +definition NSsuminf :: "(nat \<Rightarrow> real) \<Rightarrow> real"
    6.35 +  where "NSsuminf f = (THE s. f NSsums s)"
    6.36  
    6.37 -definition
    6.38 -  NSsuminf   :: "(nat=>real) => real" where
    6.39 -  "NSsuminf f = (THE s. f NSsums s)"
    6.40 +lemma sumhr_app: "sumhr (M, N, f) = ( *f2* (\<lambda>m n. sum f {m..<n})) M N"
    6.41 +  by (simp add: sumhr_def)
    6.42  
    6.43 -lemma sumhr_app: "sumhr(M,N,f) = ( *f2* (\<lambda>m n. sum f {m..<n})) M N"
    6.44 -by (simp add: sumhr_def)
    6.45 +text \<open>Base case in definition of @{term sumr}.\<close>
    6.46 +lemma sumhr_zero [simp]: "\<And>m. sumhr (m, 0, f) = 0"
    6.47 +  unfolding sumhr_app by transfer simp
    6.48  
    6.49 -text\<open>Base case in definition of @{term sumr}\<close>
    6.50 -lemma sumhr_zero [simp]: "!!m. sumhr (m,0,f) = 0"
    6.51 -unfolding sumhr_app by transfer simp
    6.52 -
    6.53 -text\<open>Recursive case in definition of @{term sumr}\<close>
    6.54 +text \<open>Recursive case in definition of @{term sumr}.\<close>
    6.55  lemma sumhr_if:
    6.56 -     "!!m n. sumhr(m,n+1,f) =
    6.57 -      (if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *f* f) n)"
    6.58 -unfolding sumhr_app by transfer simp
    6.59 +  "\<And>m n. sumhr (m, n + 1, f) = (if n + 1 \<le> m then 0 else sumhr (m, n, f) + ( *f* f) n)"
    6.60 +  unfolding sumhr_app by transfer simp
    6.61 +
    6.62 +lemma sumhr_Suc_zero [simp]: "\<And>n. sumhr (n + 1, n, f) = 0"
    6.63 +  unfolding sumhr_app by transfer simp
    6.64  
    6.65 -lemma sumhr_Suc_zero [simp]: "!!n. sumhr (n + 1, n, f) = 0"
    6.66 -unfolding sumhr_app by transfer simp
    6.67 +lemma sumhr_eq_bounds [simp]: "\<And>n. sumhr (n, n, f) = 0"
    6.68 +  unfolding sumhr_app by transfer simp
    6.69  
    6.70 -lemma sumhr_eq_bounds [simp]: "!!n. sumhr (n,n,f) = 0"
    6.71 -unfolding sumhr_app by transfer simp
    6.72 +lemma sumhr_Suc [simp]: "\<And>m. sumhr (m, m + 1, f) = ( *f* f) m"
    6.73 +  unfolding sumhr_app by transfer simp
    6.74  
    6.75 -lemma sumhr_Suc [simp]: "!!m. sumhr (m,m + 1,f) = ( *f* f) m"
    6.76 -unfolding sumhr_app by transfer simp
    6.77 +lemma sumhr_add_lbound_zero [simp]: "\<And>k m. sumhr (m + k, k, f) = 0"
    6.78 +  unfolding sumhr_app by transfer simp
    6.79  
    6.80 -lemma sumhr_add_lbound_zero [simp]: "!!k m. sumhr(m+k,k,f) = 0"
    6.81 -unfolding sumhr_app by transfer simp
    6.82 +lemma sumhr_add: "\<And>m n. sumhr (m, n, f) + sumhr (m, n, g) = sumhr (m, n, \<lambda>i. f i + g i)"
    6.83 +  unfolding sumhr_app by transfer (rule sum.distrib [symmetric])
    6.84  
    6.85 -lemma sumhr_add:
    6.86 -  "!!m n. sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
    6.87 -unfolding sumhr_app by transfer (rule sum.distrib [symmetric])
    6.88 +lemma sumhr_mult: "\<And>m n. hypreal_of_real r * sumhr (m, n, f) = sumhr (m, n, \<lambda>n. r * f n)"
    6.89 +  unfolding sumhr_app by transfer (rule sum_distrib_left)
    6.90  
    6.91 -lemma sumhr_mult:
    6.92 -  "!!m n. hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
    6.93 -unfolding sumhr_app by transfer (rule sum_distrib_left)
    6.94 +lemma sumhr_split_add: "\<And>n p. n < p \<Longrightarrow> sumhr (0, n, f) + sumhr (n, p, f) = sumhr (0, p, f)"
    6.95 +  unfolding sumhr_app by transfer (simp add: sum_add_nat_ivl)
    6.96  
    6.97 -lemma sumhr_split_add:
    6.98 -  "!!n p. n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
    6.99 -unfolding sumhr_app by transfer (simp add: sum_add_nat_ivl)
   6.100 +lemma sumhr_split_diff: "n < p \<Longrightarrow> sumhr (0, p, f) - sumhr (0, n, f) = sumhr (n, p, f)"
   6.101 +  by (drule sumhr_split_add [symmetric, where f = f]) simp
   6.102  
   6.103 -lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)"
   6.104 -by (drule_tac f = f in sumhr_split_add [symmetric], simp)
   6.105 +lemma sumhr_hrabs: "\<And>m n. \<bar>sumhr (m, n, f)\<bar> \<le> sumhr (m, n, \<lambda>i. \<bar>f i\<bar>)"
   6.106 +  unfolding sumhr_app by transfer (rule sum_abs)
   6.107  
   6.108 -lemma sumhr_hrabs: "!!m n. \<bar>sumhr(m,n,f)\<bar> \<le> sumhr(m,n,%i. \<bar>f i\<bar>)"
   6.109 -unfolding sumhr_app by transfer (rule sum_abs)
   6.110 -
   6.111 -text\<open>other general version also needed\<close>
   6.112 +text \<open>Other general version also needed.\<close>
   6.113  lemma sumhr_fun_hypnat_eq:
   6.114 -   "(\<forall>r. m \<le> r & r < n --> f r = g r) -->
   6.115 -      sumhr(hypnat_of_nat m, hypnat_of_nat n, f) =
   6.116 -      sumhr(hypnat_of_nat m, hypnat_of_nat n, g)"
   6.117 -unfolding sumhr_app by transfer simp
   6.118 +  "(\<forall>r. m \<le> r \<and> r < n \<longrightarrow> f r = g r) \<longrightarrow>
   6.119 +    sumhr (hypnat_of_nat m, hypnat_of_nat n, f) =
   6.120 +    sumhr (hypnat_of_nat m, hypnat_of_nat n, g)"
   6.121 +  unfolding sumhr_app by transfer simp
   6.122  
   6.123 -lemma sumhr_const:
   6.124 -     "!!n. sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
   6.125 -unfolding sumhr_app by transfer simp
   6.126 +lemma sumhr_const: "\<And>n. sumhr (0, n, \<lambda>i. r) = hypreal_of_hypnat n * hypreal_of_real r"
   6.127 +  unfolding sumhr_app by transfer simp
   6.128  
   6.129 -lemma sumhr_less_bounds_zero [simp]: "!!m n. n < m ==> sumhr(m,n,f) = 0"
   6.130 -unfolding sumhr_app by transfer simp
   6.131 +lemma sumhr_less_bounds_zero [simp]: "\<And>m n. n < m \<Longrightarrow> sumhr (m, n, f) = 0"
   6.132 +  unfolding sumhr_app by transfer simp
   6.133  
   6.134 -lemma sumhr_minus: "!!m n. sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
   6.135 -unfolding sumhr_app by transfer (rule sum_negf)
   6.136 +lemma sumhr_minus: "\<And>m n. sumhr (m, n, \<lambda>i. - f i) = - sumhr (m, n, f)"
   6.137 +  unfolding sumhr_app by transfer (rule sum_negf)
   6.138  
   6.139  lemma sumhr_shift_bounds:
   6.140 -  "!!m n. sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) =
   6.141 -          sumhr(m,n,%i. f(i + k))"
   6.142 -unfolding sumhr_app by transfer (rule sum_shift_bounds_nat_ivl)
   6.143 +  "\<And>m n. sumhr (m + hypnat_of_nat k, n + hypnat_of_nat k, f) =
   6.144 +    sumhr (m, n, \<lambda>i. f (i + k))"
   6.145 +  unfolding sumhr_app by transfer (rule sum_shift_bounds_nat_ivl)
   6.146  
   6.147  
   6.148 -subsection\<open>Nonstandard Sums\<close>
   6.149 +subsection \<open>Nonstandard Sums\<close>
   6.150  
   6.151 -text\<open>Infinite sums are obtained by summing to some infinite hypernatural
   6.152 - (such as @{term whn})\<close>
   6.153 -lemma sumhr_hypreal_of_hypnat_omega:
   6.154 -      "sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn"
   6.155 -by (simp add: sumhr_const)
   6.156 +text \<open>Infinite sums are obtained by summing to some infinite hypernatural
   6.157 +  (such as @{term whn}).\<close>
   6.158 +lemma sumhr_hypreal_of_hypnat_omega: "sumhr (0, whn, \<lambda>i. 1) = hypreal_of_hypnat whn"
   6.159 +  by (simp add: sumhr_const)
   6.160  
   6.161 -lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = \<omega> - 1"
   6.162 -apply (simp add: sumhr_const)
   6.163 -(* FIXME: need lemma: hypreal_of_hypnat whn = \<omega> - 1 *)
   6.164 -(* maybe define \<omega> = hypreal_of_hypnat whn + 1 *)
   6.165 -apply (unfold star_class_defs omega_def hypnat_omega_def
   6.166 -              of_hypnat_def star_of_def)
   6.167 -apply (simp add: starfun_star_n starfun2_star_n)
   6.168 -done
   6.169 +lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, \<lambda>i. 1) = \<omega> - 1"
   6.170 +  apply (simp add: sumhr_const)
   6.171 +    (* FIXME: need lemma: hypreal_of_hypnat whn = \<omega> - 1 *)
   6.172 +    (* maybe define \<omega> = hypreal_of_hypnat whn + 1 *)
   6.173 +  apply (unfold star_class_defs omega_def hypnat_omega_def of_hypnat_def star_of_def)
   6.174 +  apply (simp add: starfun_star_n starfun2_star_n)
   6.175 +  done
   6.176  
   6.177 -lemma sumhr_minus_one_realpow_zero [simp]:
   6.178 -     "!!N. sumhr(0, N + N, %i. (-1) ^ (i+1)) = 0"
   6.179 -unfolding sumhr_app
   6.180 -apply transfer
   6.181 -apply (simp del: power_Suc add: mult_2 [symmetric])
   6.182 -apply (induct_tac N)
   6.183 -apply simp_all
   6.184 -done
   6.185 +lemma sumhr_minus_one_realpow_zero [simp]: "\<And>N. sumhr (0, N + N, \<lambda>i. (-1) ^ (i + 1)) = 0"
   6.186 +  unfolding sumhr_app
   6.187 +  apply transfer
   6.188 +  apply (simp del: power_Suc add: mult_2 [symmetric])
   6.189 +  apply (induct_tac N)
   6.190 +   apply simp_all
   6.191 +  done
   6.192  
   6.193  lemma sumhr_interval_const:
   6.194 -     "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na
   6.195 -      ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) =
   6.196 -          (hypreal_of_nat (na - m) * hypreal_of_real r)"
   6.197 -unfolding sumhr_app by transfer simp
   6.198 +  "(\<forall>n. m \<le> Suc n \<longrightarrow> f n = r) \<and> m \<le> na \<Longrightarrow>
   6.199 +    sumhr (hypnat_of_nat m, hypnat_of_nat na, f) = hypreal_of_nat (na - m) * hypreal_of_real r"
   6.200 +  unfolding sumhr_app by transfer simp
   6.201  
   6.202 -lemma starfunNat_sumr: "!!N. ( *f* (%n. sum f {0..<n})) N = sumhr(0,N,f)"
   6.203 -unfolding sumhr_app by transfer (rule refl)
   6.204 +lemma starfunNat_sumr: "\<And>N. ( *f* (\<lambda>n. sum f {0..<n})) N = sumhr (0, N, f)"
   6.205 +  unfolding sumhr_app by transfer (rule refl)
   6.206  
   6.207 -lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) \<approx> sumhr(0, N, f)
   6.208 -      ==> \<bar>sumhr(M, N, f)\<bar> \<approx> 0"
   6.209 -apply (cut_tac x = M and y = N in linorder_less_linear)
   6.210 -apply (auto simp add: approx_refl)
   6.211 -apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
   6.212 -apply (auto dest: approx_hrabs
   6.213 -            simp add: sumhr_split_diff)
   6.214 -done
   6.215 +lemma sumhr_hrabs_approx [simp]: "sumhr (0, M, f) \<approx> sumhr (0, N, f) \<Longrightarrow> \<bar>sumhr (M, N, f)\<bar> \<approx> 0"
   6.216 +  using linorder_less_linear [where x = M and y = N]
   6.217 +  apply auto
   6.218 +  apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
   6.219 +  apply (auto dest: approx_hrabs simp add: sumhr_split_diff)
   6.220 +  done
   6.221 +
   6.222 +
   6.223 +subsection \<open>Infinite sums: Standard and NS theorems\<close>
   6.224  
   6.225 -(*----------------------------------------------------------------
   6.226 -      infinite sums: Standard and NS theorems
   6.227 - ----------------------------------------------------------------*)
   6.228 -lemma sums_NSsums_iff: "(f sums l) = (f NSsums l)"
   6.229 -by (simp add: sums_def NSsums_def LIMSEQ_NSLIMSEQ_iff)
   6.230 +lemma sums_NSsums_iff: "f sums l \<longleftrightarrow> f NSsums l"
   6.231 +  by (simp add: sums_def NSsums_def LIMSEQ_NSLIMSEQ_iff)
   6.232  
   6.233 -lemma summable_NSsummable_iff: "(summable f) = (NSsummable f)"
   6.234 -by (simp add: summable_def NSsummable_def sums_NSsums_iff)
   6.235 +lemma summable_NSsummable_iff: "summable f \<longleftrightarrow> NSsummable f"
   6.236 +  by (simp add: summable_def NSsummable_def sums_NSsums_iff)
   6.237  
   6.238 -lemma suminf_NSsuminf_iff: "(suminf f) = (NSsuminf f)"
   6.239 -by (simp add: suminf_def NSsuminf_def sums_NSsums_iff)
   6.240 +lemma suminf_NSsuminf_iff: "suminf f = NSsuminf f"
   6.241 +  by (simp add: suminf_def NSsuminf_def sums_NSsums_iff)
   6.242  
   6.243 -lemma NSsums_NSsummable: "f NSsums l ==> NSsummable f"
   6.244 -by (simp add: NSsums_def NSsummable_def, blast)
   6.245 +lemma NSsums_NSsummable: "f NSsums l \<Longrightarrow> NSsummable f"
   6.246 +  unfolding NSsums_def NSsummable_def by blast
   6.247  
   6.248 -lemma NSsummable_NSsums: "NSsummable f ==> f NSsums (NSsuminf f)"
   6.249 -apply (simp add: NSsummable_def NSsuminf_def NSsums_def)
   6.250 -apply (blast intro: theI NSLIMSEQ_unique)
   6.251 -done
   6.252 +lemma NSsummable_NSsums: "NSsummable f \<Longrightarrow> f NSsums (NSsuminf f)"
   6.253 +  unfolding NSsummable_def NSsuminf_def NSsums_def
   6.254 +  by (blast intro: theI NSLIMSEQ_unique)
   6.255  
   6.256 -lemma NSsums_unique: "f NSsums s ==> (s = NSsuminf f)"
   6.257 -by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)
   6.258 +lemma NSsums_unique: "f NSsums s \<Longrightarrow> s = NSsuminf f"
   6.259 +  by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)
   6.260  
   6.261 -lemma NSseries_zero:
   6.262 -  "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (sum f {..<n})"
   6.263 -by (auto simp add: sums_NSsums_iff [symmetric] not_le[symmetric] intro!: sums_finite)
   6.264 +lemma NSseries_zero: "\<forall>m. n \<le> Suc m \<longrightarrow> f m = 0 \<Longrightarrow> f NSsums (sum f {..<n})"
   6.265 +  by (auto simp add: sums_NSsums_iff [symmetric] not_le[symmetric] intro!: sums_finite)
   6.266  
   6.267  lemma NSsummable_NSCauchy:
   6.268 -     "NSsummable f =
   6.269 -      (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. \<bar>sumhr(M,N,f)\<bar> \<approx> 0)"
   6.270 -apply (auto simp add: summable_NSsummable_iff [symmetric]
   6.271 -       summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
   6.272 -       NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
   6.273 -apply (cut_tac x = M and y = N in linorder_less_linear)
   6.274 -apply auto
   6.275 -apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
   6.276 -apply (rule_tac [2] approx_minus_iff [THEN iffD2])
   6.277 -apply (auto dest: approx_hrabs_zero_cancel
   6.278 -            simp add: sumhr_split_diff atLeast0LessThan[symmetric])
   6.279 -done
   6.280 +  "NSsummable f \<longleftrightarrow> (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. \<bar>sumhr (M, N, f)\<bar> \<approx> 0)"
   6.281 +  apply (auto simp add: summable_NSsummable_iff [symmetric]
   6.282 +      summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
   6.283 +      NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
   6.284 +  apply (cut_tac x = M and y = N in linorder_less_linear)
   6.285 +  apply auto
   6.286 +   apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
   6.287 +   apply (rule_tac [2] approx_minus_iff [THEN iffD2])
   6.288 +   apply (auto dest: approx_hrabs_zero_cancel simp: sumhr_split_diff atLeast0LessThan[symmetric])
   6.289 +  done
   6.290  
   6.291 -text\<open>Terms of a convergent series tend to zero\<close>
   6.292 -lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ==> f \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   6.293 -apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
   6.294 -apply (drule bspec, auto)
   6.295 -apply (drule_tac x = "N + 1 " in bspec)
   6.296 -apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
   6.297 -done
   6.298 +text \<open>Terms of a convergent series tend to zero.\<close>
   6.299 +lemma NSsummable_NSLIMSEQ_zero: "NSsummable f \<Longrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   6.300 +  apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
   6.301 +  apply (drule bspec)
   6.302 +   apply auto
   6.303 +  apply (drule_tac x = "N + 1 " in bspec)
   6.304 +   apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
   6.305 +  done
   6.306  
   6.307 -text\<open>Nonstandard comparison test\<close>
   6.308 -lemma NSsummable_comparison_test:
   6.309 -     "[| \<exists>N. \<forall>n. N \<le> n --> \<bar>f n\<bar> \<le> g n; NSsummable g |] ==> NSsummable f"
   6.310 -apply (fold summable_NSsummable_iff)
   6.311 -apply (rule summable_comparison_test, simp, assumption)
   6.312 -done
   6.313 +text \<open>Nonstandard comparison test.\<close>
   6.314 +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"
   6.315 +  apply (fold summable_NSsummable_iff)
   6.316 +  apply (rule summable_comparison_test, simp, assumption)
   6.317 +  done
   6.318  
   6.319  lemma NSsummable_rabs_comparison_test:
   6.320 -     "[| \<exists>N. \<forall>n. N \<le> n --> \<bar>f n\<bar> \<le> g n; NSsummable g |]
   6.321 -      ==> NSsummable (%k. \<bar>f k\<bar>)"
   6.322 -apply (rule NSsummable_comparison_test)
   6.323 -apply (auto)
   6.324 -done
   6.325 +  "\<exists>N. \<forall>n. N \<le> n \<longrightarrow> \<bar>f n\<bar> \<le> g n \<Longrightarrow> NSsummable g \<Longrightarrow> NSsummable (\<lambda>k. \<bar>f k\<bar>)"
   6.326 +  by (rule NSsummable_comparison_test) auto
   6.327  
   6.328  end