# HG changeset patch
# User wenzelm
# Date 1482101030 -3600
# Node ID 2bf8cfc98c4d10a1b8ff1a29783ba4a8330ec24b
# Parent  a7f5e59378f7757e025b5863e46806e5d33ba9e9
misc tuning and modernization;

diff -r a7f5e59378f7 -r 2bf8cfc98c4d src/HOL/Nonstandard_Analysis/CStar.thy
--- a/src/HOL/Nonstandard_Analysis/CStar.thy	Sun Dec 18 22:14:53 2016 +0100
+++ b/src/HOL/Nonstandard_Analysis/CStar.thy	Sun Dec 18 23:43:50 2016 +0100
@@ -3,37 +3,36 @@
     Copyright:  2001 University of Edinburgh
 *)
 
-section\<open>Star-transforms in NSA, Extending Sets of Complex Numbers
-      and Complex Functions\<close>
+section \<open>Star-transforms in NSA, Extending Sets of Complex Numbers and Complex Functions\<close>
 
 theory CStar
-imports NSCA
+  imports NSCA
 begin
 
-subsection\<open>Properties of the *-Transform Applied to Sets of Reals\<close>
+subsection \<open>Properties of the \<open>*\<close>-Transform Applied to Sets of Reals\<close>
 
-lemma STARC_hcomplex_of_complex_Int:
-     "*s* X Int SComplex = hcomplex_of_complex ` X"
-by (auto simp add: Standard_def)
+lemma STARC_hcomplex_of_complex_Int: "*s* X \<inter> SComplex = hcomplex_of_complex ` X"
+  by (auto simp: Standard_def)
 
-lemma lemma_not_hcomplexA:
-     "x \<notin> hcomplex_of_complex ` A ==> \<forall>y \<in> A. x \<noteq> hcomplex_of_complex y"
-by auto
+lemma lemma_not_hcomplexA: "x \<notin> hcomplex_of_complex ` A \<Longrightarrow> \<forall>y \<in> A. x \<noteq> hcomplex_of_complex y"
+  by auto
+
 
-subsection\<open>Theorems about Nonstandard Extensions of Functions\<close>
+subsection \<open>Theorems about Nonstandard Extensions of Functions\<close>
 
-lemma starfunC_hcpow: "!!Z. ( *f* (%z. z ^ n)) Z = Z pow hypnat_of_nat n"
-by transfer (rule refl)
+lemma starfunC_hcpow: "\<And>Z. ( *f* (\<lambda>z. z ^ n)) Z = Z pow hypnat_of_nat n"
+  by transfer (rule refl)
 
 lemma starfunCR_cmod: "*f* cmod = hcmod"
-by transfer (rule refl)
+  by transfer (rule refl)
 
-subsection\<open>Internal Functions - Some Redundancy With *f* Now\<close>
+
+subsection \<open>Internal Functions - Some Redundancy With \<open>*f*\<close> Now\<close>
 
 (** subtraction: ( *fn) - ( *gn) = *(fn - gn) **)
 (*
 lemma starfun_n_diff:
-   "( *fn* f) z - ( *fn* g) z = ( *fn* (%i x. f i x - g i x)) z"
+   "( *fn* f) z - ( *fn* g) z = ( *fn* (\<lambda>i x. f i x - g i x)) z"
 apply (cases z)
 apply (simp add: starfun_n star_n_diff)
 done
@@ -41,19 +40,17 @@
 (** composition: ( *fn) o ( *gn) = *(fn o gn) **)
 
 lemma starfun_Re: "( *f* (\<lambda>x. Re (f x))) = (\<lambda>x. hRe (( *f* f) x))"
-by transfer (rule refl)
+  by transfer (rule refl)
 
 lemma starfun_Im: "( *f* (\<lambda>x. Im (f x))) = (\<lambda>x. hIm (( *f* f) x))"
-by transfer (rule refl)
+  by transfer (rule refl)
 
 lemma starfunC_eq_Re_Im_iff:
-    "(( *f* f) x = z) = ((( *f* (%x. Re(f x))) x = hRe (z)) &
-                          (( *f* (%x. Im(f x))) x = hIm (z)))"
-by (simp add: hcomplex_hRe_hIm_cancel_iff starfun_Re starfun_Im)
+  "( *f* f) x = z \<longleftrightarrow> ( *f* (\<lambda>x. Re (f x))) x = hRe z \<and> ( *f* (\<lambda>x. Im (f x))) x = hIm z"
+  by (simp add: hcomplex_hRe_hIm_cancel_iff starfun_Re starfun_Im)
 
 lemma starfunC_approx_Re_Im_iff:
-    "(( *f* f) x \<approx> z) = ((( *f* (%x. Re(f x))) x \<approx> hRe (z)) &
-                            (( *f* (%x. Im(f x))) x \<approx> hIm (z)))"
-by (simp add: hcomplex_approx_iff starfun_Re starfun_Im)
+  "( *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"
+  by (simp add: hcomplex_approx_iff starfun_Re starfun_Im)
 
 end
diff -r a7f5e59378f7 -r 2bf8cfc98c4d src/HOL/Nonstandard_Analysis/HDeriv.thy
--- a/src/HOL/Nonstandard_Analysis/HDeriv.thy	Sun Dec 18 22:14:53 2016 +0100
+++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy	Sun Dec 18 23:43:50 2016 +0100
@@ -53,7 +53,7 @@
    apply (drule (1) bspec)+
    apply (drule (1) approx_trans3)
    apply simp
-  apply (simp add: Infinitesimal_of_hypreal Infinitesimal_epsilon)
+  apply (simp add: Infinitesimal_of_hypreal)
   apply (simp add: of_hypreal_eq_0_iff hypreal_epsilon_not_zero)
   done
 
@@ -75,7 +75,7 @@
 text \<open>While we're at it!\<close>
 lemma NSDERIV_iff2:
   "(NSDERIV f x :> D) \<longleftrightarrow>
-    (\<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)"
+    (\<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)"
   by (simp add: NSDERIV_NSLIM_iff2 NSLIM_def)
 
 (* FIXME delete *)
@@ -91,7 +91,7 @@
   apply (drule_tac x = u in spec, auto)
   apply (drule_tac c = "u - hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1)
    apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1])
-   apply (subgoal_tac [2] "( *f* (%z. z-x)) u \<noteq> (0::hypreal) ")
+   apply (subgoal_tac [2] "( *f* (\<lambda>z. z - x)) u \<noteq> (0::hypreal) ")
     apply (auto simp: approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
       Infinitesimal_subset_HFinite [THEN subsetD])
   done
@@ -290,7 +290,8 @@
   apply (case_tac "( *f* g) (star_of (x) + xa) = star_of (g x) ")
    apply (drule_tac g = g in NSDERIV_zero)
       apply (auto simp add: divide_inverse)
-  apply (rule_tac z1 = "( *f* g) (star_of (x) + xa) - star_of (g x) " and y1 = "inverse xa" in lemma_chain [THEN ssubst])
+  apply (rule_tac z1 = "( *f* g) (star_of (x) + xa) - star_of (g x) " and y1 = "inverse xa"
+      in lemma_chain [THEN ssubst])
    apply (erule hypreal_not_eq_minus_iff [THEN iffD1])
   apply (rule approx_mult_star_of)
    apply (simp_all add: divide_inverse [symmetric])
diff -r a7f5e59378f7 -r 2bf8cfc98c4d src/HOL/Nonstandard_Analysis/HLim.thy
--- a/src/HOL/Nonstandard_Analysis/HLim.thy	Sun Dec 18 22:14:53 2016 +0100
+++ b/src/HOL/Nonstandard_Analysis/HLim.thy	Sun Dec 18 23:43:50 2016 +0100
@@ -77,7 +77,7 @@
 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 = "%x. l" and m = l in NSLIM_add)
+  apply (drule_tac g = "\<lambda>x. l" and m = l in NSLIM_add)
    apply (auto simp add: add.assoc)
   done
 
@@ -205,8 +205,8 @@
 lemma isCont_isNSCont: "isCont f a \<Longrightarrow> isNSCont f a"
   by (erule isNSCont_isCont_iff [THEN iffD2])
 
-text \<open>NS continuity \<open>==>\<close> Standard continuity.\<close>
-lemma isNSCont_isCont: "isNSCont f a ==> isCont f a"
+text \<open>NS continuity \<open>\<Longrightarrow>\<close> Standard continuity.\<close>
+lemma isNSCont_isCont: "isNSCont f a \<Longrightarrow> isCont f a"
   by (erule isNSCont_isCont_iff [THEN iffD1])
 
 
diff -r a7f5e59378f7 -r 2bf8cfc98c4d src/HOL/Nonstandard_Analysis/HLog.thy
--- a/src/HOL/Nonstandard_Analysis/HLog.thy	Sun Dec 18 22:14:53 2016 +0100
+++ b/src/HOL/Nonstandard_Analysis/HLog.thy	Sun Dec 18 23:43:50 2016 +0100
@@ -3,154 +3,134 @@
     Copyright:  2000, 2001 University of Edinburgh
 *)
 
-section\<open>Logarithms: Non-Standard Version\<close>
+section \<open>Logarithms: Non-Standard Version\<close>
 
 theory HLog
-imports HTranscendental
+  imports HTranscendental
 begin
 
 
 (* should be in NSA.ML *)
 lemma epsilon_ge_zero [simp]: "0 \<le> \<epsilon>"
-by (simp add: epsilon_def star_n_zero_num star_n_le)
+  by (simp add: epsilon_def star_n_zero_num star_n_le)
 
-lemma hpfinite_witness: "\<epsilon> : {x. 0 \<le> x & x : HFinite}"
-by auto
+lemma hpfinite_witness: "\<epsilon> \<in> {x. 0 \<le> x \<and> x \<in> HFinite}"
+  by auto
 
 
-definition
-  powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80) where
-  [transfer_unfold]: "x powhr a = starfun2 (op powr) x a"
-  
-definition
-  hlog :: "[hypreal,hypreal] => hypreal" where
-  [transfer_unfold]: "hlog a x = starfun2 log a x"
+definition powhr :: "hypreal \<Rightarrow> hypreal \<Rightarrow> hypreal"  (infixr "powhr" 80)
+  where [transfer_unfold]: "x powhr a = starfun2 (op powr) x a"
+
+definition hlog :: "hypreal \<Rightarrow> hypreal \<Rightarrow> hypreal"
+  where [transfer_unfold]: "hlog a x = starfun2 log a x"
+
+lemma powhr: "(star_n X) powhr (star_n Y) = star_n (\<lambda>n. (X n) powr (Y n))"
+  by (simp add: powhr_def starfun2_star_n)
 
-lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
-by (simp add: powhr_def starfun2_star_n)
-
-lemma powhr_one_eq_one [simp]: "!!a. 1 powhr a = 1"
-by (transfer, simp)
+lemma powhr_one_eq_one [simp]: "\<And>a. 1 powhr a = 1"
+  by transfer simp
 
-lemma powhr_mult:
-  "!!a x y. [| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)"
-by (transfer, simp add: powr_mult)
+lemma powhr_mult: "\<And>a x y. 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x * y) powhr a = (x powhr a) * (y powhr a)"
+  by transfer (simp add: powr_mult)
 
-lemma powhr_gt_zero [simp]: "!!a x. 0 < x powhr a \<longleftrightarrow> x \<noteq> 0"
-by (transfer, simp)
+lemma powhr_gt_zero [simp]: "\<And>a x. 0 < x powhr a \<longleftrightarrow> x \<noteq> 0"
+  by transfer simp
 
 lemma powhr_not_zero [simp]: "\<And>a x. x powhr a \<noteq> 0 \<longleftrightarrow> x \<noteq> 0"
-by transfer simp
-
-lemma powhr_divide:
-  "!!a x y. [| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
-by (transfer, rule powr_divide)
+  by transfer simp
 
-lemma powhr_add: "!!a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
-by (transfer, rule powr_add)
+lemma powhr_divide: "\<And>a x y. 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powhr a = (x powhr a) / (y powhr a)"
+  by transfer (rule powr_divide)
 
-lemma powhr_powhr: "!!a b x. (x powhr a) powhr b = x powhr (a * b)"
-by (transfer, rule powr_powr)
+lemma powhr_add: "\<And>a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
+  by transfer (rule powr_add)
 
-lemma powhr_powhr_swap: "!!a b x. (x powhr a) powhr b = (x powhr b) powhr a"
-by (transfer, rule powr_powr_swap)
+lemma powhr_powhr: "\<And>a b x. (x powhr a) powhr b = x powhr (a * b)"
+  by transfer (rule powr_powr)
 
-lemma powhr_minus: "!!a x. x powhr (-a) = inverse (x powhr a)"
-by (transfer, rule powr_minus)
+lemma powhr_powhr_swap: "\<And>a b x. (x powhr a) powhr b = (x powhr b) powhr a"
+  by transfer (rule powr_powr_swap)
 
-lemma powhr_minus_divide: "x powhr (-a) = 1/(x powhr a)"
-by (simp add: divide_inverse powhr_minus)
+lemma powhr_minus: "\<And>a x. x powhr (- a) = inverse (x powhr a)"
+  by transfer (rule powr_minus)
 
-lemma powhr_less_mono: "!!a b x. [| a < b; 1 < x |] ==> x powhr a < x powhr b"
-by (transfer, simp)
+lemma powhr_minus_divide: "x powhr (- a) = 1 / (x powhr a)"
+  by (simp add: divide_inverse powhr_minus)
 
-lemma powhr_less_cancel: "!!a b x. [| x powhr a < x powhr b; 1 < x |] ==> a < b"
-by (transfer, simp)
+lemma powhr_less_mono: "\<And>a b x. a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powhr a < x powhr b"
+  by transfer simp
+
+lemma powhr_less_cancel: "\<And>a b x. x powhr a < x powhr b \<Longrightarrow> 1 < x \<Longrightarrow> a < b"
+  by transfer simp
 
-lemma powhr_less_cancel_iff [simp]:
-     "1 < x ==> (x powhr a < x powhr b) = (a < b)"
-by (blast intro: powhr_less_cancel powhr_less_mono)
+lemma powhr_less_cancel_iff [simp]: "1 < x \<Longrightarrow> x powhr a < x powhr b \<longleftrightarrow> a < b"
+  by (blast intro: powhr_less_cancel powhr_less_mono)
 
-lemma powhr_le_cancel_iff [simp]:
-     "1 < x ==> (x powhr a \<le> x powhr b) = (a \<le> b)"
-by (simp add: linorder_not_less [symmetric])
+lemma powhr_le_cancel_iff [simp]: "1 < x \<Longrightarrow> x powhr a \<le> x powhr b \<longleftrightarrow> a \<le> b"
+  by (simp add: linorder_not_less [symmetric])
 
-lemma hlog:
-     "hlog (star_n X) (star_n Y) =  
-      star_n (%n. log (X n) (Y n))"
-by (simp add: hlog_def starfun2_star_n)
+lemma hlog: "hlog (star_n X) (star_n Y) = star_n (\<lambda>n. log (X n) (Y n))"
+  by (simp add: hlog_def starfun2_star_n)
 
-lemma hlog_starfun_ln: "!!x. ( *f* ln) x = hlog (( *f* exp) 1) x"
-by (transfer, rule log_ln)
+lemma hlog_starfun_ln: "\<And>x. ( *f* ln) x = hlog (( *f* exp) 1) x"
+  by transfer (rule log_ln)
 
-lemma powhr_hlog_cancel [simp]:
-     "!!a x. [| 0 < a; a \<noteq> 1; 0 < x |] ==> a powhr (hlog a x) = x"
-by (transfer, simp)
+lemma powhr_hlog_cancel [simp]: "\<And>a x. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> a powhr (hlog a x) = x"
+  by transfer simp
 
-lemma hlog_powhr_cancel [simp]:
-     "!!a y. [| 0 < a; a \<noteq> 1 |] ==> hlog a (a powhr y) = y"
-by (transfer, simp)
+lemma hlog_powhr_cancel [simp]: "\<And>a y. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> hlog a (a powhr y) = y"
+  by transfer simp
 
 lemma hlog_mult:
-     "!!a x y. [| 0 < a; a \<noteq> 1; 0 < x; 0 < y  |]  
-      ==> hlog a (x * y) = hlog a x + hlog a y"
-by (transfer, rule log_mult)
+  "\<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"
+  by transfer (rule log_mult)
 
-lemma hlog_as_starfun:
-     "!!a x. [| 0 < a; a \<noteq> 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
-by (transfer, simp add: log_def)
+lemma hlog_as_starfun: "\<And>a x. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> hlog a x = ( *f* ln) x / ( *f* ln) a"
+  by transfer (simp add: log_def)
 
 lemma hlog_eq_div_starfun_ln_mult_hlog:
-     "!!a b x. [| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]  
-      ==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x"
-by (transfer, rule log_eq_div_ln_mult_log)
+  "\<And>a b x. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow>
+    hlog a x = (( *f* ln) b / ( *f* ln) a) * hlog b x"
+  by transfer (rule log_eq_div_ln_mult_log)
 
-lemma powhr_as_starfun: "!!a x. x powhr a = (if x=0 then 0 else ( *f* exp) (a * ( *f* real_ln) x))"
-  by (transfer, simp add: powr_def)
+lemma powhr_as_starfun: "\<And>a x. x powhr a = (if x = 0 then 0 else ( *f* exp) (a * ( *f* real_ln) x))"
+  by transfer (simp add: powr_def)
 
 lemma HInfinite_powhr:
-     "[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal;  
-         0 < a |] ==> x powhr a : HInfinite"
-apply (auto intro!: starfun_ln_ge_zero starfun_ln_HInfinite HInfinite_HFinite_not_Infinitesimal_mult2 starfun_exp_HInfinite 
-       simp add: order_less_imp_le HInfinite_gt_zero_gt_one powhr_as_starfun zero_le_mult_iff)
-done
+  "x \<in> HInfinite \<Longrightarrow> 0 < x \<Longrightarrow> a \<in> HFinite - Infinitesimal \<Longrightarrow> 0 < a \<Longrightarrow> x powhr a \<in> HInfinite"
+  by (auto intro!: starfun_ln_ge_zero starfun_ln_HInfinite
+        HInfinite_HFinite_not_Infinitesimal_mult2 starfun_exp_HInfinite
+      simp add: order_less_imp_le HInfinite_gt_zero_gt_one powhr_as_starfun zero_le_mult_iff)
 
 lemma hlog_hrabs_HInfinite_Infinitesimal:
-     "[| x : HFinite - Infinitesimal; a : HInfinite; 0 < a |]  
-      ==> hlog a \<bar>x\<bar> : Infinitesimal"
-apply (frule HInfinite_gt_zero_gt_one)
-apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
-            HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2 
-        simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero 
-          hlog_as_starfun divide_inverse)
-done
+  "x \<in> HFinite - Infinitesimal \<Longrightarrow> a \<in> HInfinite \<Longrightarrow> 0 < a \<Longrightarrow> hlog a \<bar>x\<bar> \<in> Infinitesimal"
+  apply (frule HInfinite_gt_zero_gt_one)
+   apply (auto intro!: starfun_ln_HFinite_not_Infinitesimal
+      HInfinite_inverse_Infinitesimal Infinitesimal_HFinite_mult2
+      simp add: starfun_ln_HInfinite not_Infinitesimal_not_zero
+      hlog_as_starfun divide_inverse)
+  done
 
-lemma hlog_HInfinite_as_starfun:
-     "[| a : HInfinite; 0 < a |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
-by (rule hlog_as_starfun, auto)
+lemma hlog_HInfinite_as_starfun: "a \<in> HInfinite \<Longrightarrow> 0 < a \<Longrightarrow> hlog a x = ( *f* ln) x / ( *f* ln) a"
+  by (rule hlog_as_starfun) auto
 
-lemma hlog_one [simp]: "!!a. hlog a 1 = 0"
-by (transfer, simp)
+lemma hlog_one [simp]: "\<And>a. hlog a 1 = 0"
+  by transfer simp
 
-lemma hlog_eq_one [simp]: "!!a. [| 0 < a; a \<noteq> 1 |] ==> hlog a a = 1"
-by (transfer, rule log_eq_one)
+lemma hlog_eq_one [simp]: "\<And>a. 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> hlog a a = 1"
+  by transfer (rule log_eq_one)
 
-lemma hlog_inverse:
-     "[| 0 < a; a \<noteq> 1; 0 < x |] ==> hlog a (inverse x) = - hlog a x"
-apply (rule add_left_cancel [of "hlog a x", THEN iffD1])
-apply (simp add: hlog_mult [symmetric])
-done
+lemma hlog_inverse: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> hlog a (inverse x) = - hlog a x"
+  by (rule add_left_cancel [of "hlog a x", THEN iffD1]) (simp add: hlog_mult [symmetric])
 
-lemma hlog_divide:
-     "[| 0 < a; a \<noteq> 1; 0 < x; 0 < y|] ==> hlog a (x/y) = hlog a x - hlog a y"
-by (simp add: hlog_mult hlog_inverse divide_inverse)
+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"
+  by (simp add: hlog_mult hlog_inverse divide_inverse)
 
 lemma hlog_less_cancel_iff [simp]:
-     "!!a x y. [| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
-by (transfer, simp)
+  "\<And>a x y. 1 < a \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> hlog a x < hlog a y \<longleftrightarrow> x < y"
+  by transfer simp
 
-lemma hlog_le_cancel_iff [simp]:
-     "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x \<le> hlog a y) = (x \<le> y)"
-by (simp add: linorder_not_less [symmetric])
+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"
+  by (simp add: linorder_not_less [symmetric])
 
 end
diff -r a7f5e59378f7 -r 2bf8cfc98c4d src/HOL/Nonstandard_Analysis/HSEQ.thy
--- a/src/HOL/Nonstandard_Analysis/HSEQ.thy	Sun Dec 18 22:14:53 2016 +0100
+++ b/src/HOL/Nonstandard_Analysis/HSEQ.thy	Sun Dec 18 23:43:50 2016 +0100
@@ -15,434 +15,431 @@
   abbrevs "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
 begin
 
-definition
-  NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
+definition NSLIMSEQ :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool"
     ("((_)/ \<longlonglongrightarrow>\<^sub>N\<^sub>S (_))" [60, 60] 60) where
     \<comment>\<open>Nonstandard definition of convergence of sequence\<close>
-  "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
+  "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
 
-definition
-  nslim :: "(nat => 'a::real_normed_vector) => 'a" where
-    \<comment>\<open>Nonstandard definition of limit using choice operator\<close>
-  "nslim X = (THE L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
+definition nslim :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a"
+  where "nslim X = (THE L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
+  \<comment> \<open>Nonstandard definition of limit using choice operator\<close>
+
 
-definition
-  NSconvergent :: "(nat => 'a::real_normed_vector) => bool" where
-    \<comment>\<open>Nonstandard definition of convergence\<close>
-  "NSconvergent X = (\<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
+definition NSconvergent :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool"
+  where "NSconvergent X \<longleftrightarrow> (\<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
+  \<comment> \<open>Nonstandard definition of convergence\<close>
 
-definition
-  NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
-    \<comment>\<open>Nonstandard definition for bounded sequence\<close>
-  "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
+definition NSBseq :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool"
+  where "NSBseq X \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<in> HFinite)"
+  \<comment> \<open>Nonstandard definition for bounded sequence\<close>
+
 
-definition
-  NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where
-    \<comment>\<open>Nonstandard definition\<close>
-  "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
+definition NSCauchy :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool"
+  where "NSCauchy X \<longleftrightarrow> (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
+  \<comment> \<open>Nonstandard definition\<close>
+
 
 subsection \<open>Limits of Sequences\<close>
 
-lemma NSLIMSEQ_iff:
-    "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
-by (simp add: NSLIMSEQ_def)
+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)
 
-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)
+lemma NSLIMSEQ_D: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L"
+  by (simp add: NSLIMSEQ_def)
 
-lemma NSLIMSEQ_D:
-  "\<lbrakk>X \<longlonglongrightarrow>\<^sub>N\<^sub>S L; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X N \<approx> star_of L"
-by (simp add: NSLIMSEQ_def)
+lemma NSLIMSEQ_const: "(\<lambda>n. k) \<longlonglongrightarrow>\<^sub>N\<^sub>S k"
+  by (simp add: NSLIMSEQ_def)
 
-lemma NSLIMSEQ_const: "(%n. k) \<longlonglongrightarrow>\<^sub>N\<^sub>S k"
-by (simp add: NSLIMSEQ_def)
+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"
+  by (auto intro: approx_add simp add: NSLIMSEQ_def)
 
-lemma NSLIMSEQ_add:
-      "[| 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"
-by (auto intro: approx_add simp add: NSLIMSEQ_def starfun_add [symmetric])
+lemma NSLIMSEQ_add_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. f n + b) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + b"
+  by (simp only: NSLIMSEQ_add NSLIMSEQ_const)
 
-lemma NSLIMSEQ_add_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a ==> (%n.(f n + b)) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + b"
-by (simp only: NSLIMSEQ_add NSLIMSEQ_const)
+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"
+  for a b :: "'a::real_normed_algebra"
+  by (auto intro!: approx_mult_HFinite simp add: NSLIMSEQ_def)
 
-lemma NSLIMSEQ_mult:
-  fixes a b :: "'a::real_normed_algebra"
-  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"
-by (auto intro!: approx_mult_HFinite simp add: NSLIMSEQ_def)
+lemma NSLIMSEQ_minus: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. - X n) \<longlonglongrightarrow>\<^sub>N\<^sub>S - a"
+  by (auto simp add: NSLIMSEQ_def)
 
-lemma NSLIMSEQ_minus: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a ==> (%n. -(X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S -a"
-by (auto simp add: NSLIMSEQ_def)
+lemma NSLIMSEQ_minus_cancel: "(\<lambda>n. - X n) \<longlonglongrightarrow>\<^sub>N\<^sub>S -a \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S a"
+  by (drule NSLIMSEQ_minus) simp
 
-lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S -a ==> X \<longlonglongrightarrow>\<^sub>N\<^sub>S a"
-by (drule NSLIMSEQ_minus, simp)
-
-lemma NSLIMSEQ_diff:
-     "[| 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"
+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; Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> (%n. X n + -Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + -b"
+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 ==> (%n.(f n - b)) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b"
-by (simp add: NSLIMSEQ_diff NSLIMSEQ_const)
+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)
 
-lemma NSLIMSEQ_inverse:
-  fixes a :: "'a::real_normed_div_algebra"
-  shows "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a;  a ~= 0 |] ==> (%n. inverse(X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S inverse(a)"
-by (simp add: NSLIMSEQ_def star_of_approx_inverse)
+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"
+  for a :: "'a::real_normed_div_algebra"
+  by (simp add: NSLIMSEQ_def star_of_approx_inverse)
 
-lemma NSLIMSEQ_mult_inverse:
-  fixes a b :: "'a::real_normed_field"
-  shows
-     "[| 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"
-by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
+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"
+  for a b :: "'a::real_normed_field"
+  by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
 
 lemma starfun_hnorm: "\<And>x. hnorm (( *f* f) x) = ( *f* (\<lambda>x. norm (f x))) x"
-by transfer simp
+  by transfer simp
 
 lemma NSLIMSEQ_norm: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S norm a"
-by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)
-
-text\<open>Uniqueness of limit\<close>
-lemma NSLIMSEQ_unique: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; X \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> a = b"
-apply (simp add: NSLIMSEQ_def)
-apply (drule HNatInfinite_whn [THEN [2] bspec])+
-apply (auto dest: approx_trans3)
-done
+  by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)
 
-lemma NSLIMSEQ_pow [rule_format]:
-  fixes a :: "'a::{real_normed_algebra,power}"
-  shows "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S a) --> ((%n. (X n) ^ m) \<longlonglongrightarrow>\<^sub>N\<^sub>S a ^ m)"
-apply (induct "m")
-apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)
-done
+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
 
-text\<open>We can now try and derive a few properties of sequences,
-     starting with the limit comparison property for sequences.\<close>
+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}"
+  by (induct m) (auto intro: NSLIMSEQ_mult NSLIMSEQ_const)
+
+text \<open>We can now try and derive a few properties of sequences,
+  starting with the limit comparison property for sequences.\<close>
 
-lemma NSLIMSEQ_le:
-       "[| f \<longlonglongrightarrow>\<^sub>N\<^sub>S l; g \<longlonglongrightarrow>\<^sub>N\<^sub>S m;
-           \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n)
-        |] ==> l \<le> (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
+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
 
-lemma NSLIMSEQ_le_const: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S (r::real); \<forall>n. a \<le> X n |] ==> a \<le> r"
-by (erule NSLIMSEQ_le [OF NSLIMSEQ_const], auto)
+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
 
-lemma NSLIMSEQ_le_const2: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a"
-by (erule NSLIMSEQ_le [OF _ NSLIMSEQ_const], auto)
+lemma NSLIMSEQ_le_const2: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S r \<Longrightarrow> \<forall>n. X n \<le> a \<Longrightarrow> r \<le> a"
+  for a r :: real
+  by (erule NSLIMSEQ_le [OF _ NSLIMSEQ_const]) auto
 
-text\<open>Shift a convergent series by 1:
+text \<open>Shift a convergent series by 1:
   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 ==> (%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
-apply (unfold NSLIMSEQ_def, safe)
-apply (drule_tac x="N + 1" in bspec)
-apply (erule HNatInfinite_add)
-apply (simp add: starfun_shift_one)
-done
+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: "(%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l ==> f \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
-apply (unfold NSLIMSEQ_def, 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_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: "((%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l) = (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"
+  by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
+
 
 subsubsection \<open>Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ}\<close>
 
 lemma LIMSEQ_NSLIMSEQ:
-  assumes X: "X \<longlonglongrightarrow> L" shows "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
+  assumes X: "X \<longlonglongrightarrow> L"
+  shows "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
 proof (rule NSLIMSEQ_I)
-  fix N assume N: "N \<in> HNatInfinite"
+  fix N
+  assume N: "N \<in> HNatInfinite"
   have "starfun X N - star_of L \<in> Infinitesimal"
   proof (rule InfinitesimalI2)
-    fix r::real assume r: "0 < r"
-    from LIMSEQ_D [OF X r]
-    obtain no where "\<forall>n\<ge>no. norm (X n - L) < r" ..
-    hence "\<forall>n\<ge>star_of no. hnorm (starfun X n - star_of L) < star_of r"
+    fix r :: real
+    assume r: "0 < r"
+    from LIMSEQ_D [OF X r] obtain no where "\<forall>n\<ge>no. norm (X n - L) < r" ..
+    then have "\<forall>n\<ge>star_of no. hnorm (starfun X n - star_of L) < star_of r"
       by transfer
-    thus "hnorm (starfun X N - star_of L) < star_of r"
+    then show "hnorm (starfun X N - star_of L) < star_of r"
       using N by (simp add: star_of_le_HNatInfinite)
   qed
-  thus "starfun X N \<approx> star_of L"
-    by (unfold approx_def)
+  then show "starfun X N \<approx> star_of L"
+    by (simp only: approx_def)
 qed
 
 lemma NSLIMSEQ_LIMSEQ:
-  assumes X: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L" shows "X \<longlonglongrightarrow> L"
+  assumes X: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
+  shows "X \<longlonglongrightarrow> L"
 proof (rule LIMSEQ_I)
-  fix r::real assume r: "0 < r"
+  fix r :: real
+  assume r: "0 < r"
   have "\<exists>no. \<forall>n\<ge>no. hnorm (starfun X n - star_of L) < star_of r"
   proof (intro exI allI impI)
-    fix n assume "whn \<le> n"
+    fix n
+    assume "whn \<le> n"
     with HNatInfinite_whn have "n \<in> HNatInfinite"
       by (rule HNatInfinite_upward_closed)
     with X have "starfun X n \<approx> star_of L"
       by (rule NSLIMSEQ_D)
-    hence "starfun X n - star_of L \<in> Infinitesimal"
-      by (unfold approx_def)
-    thus "hnorm (starfun X n - star_of L) < star_of r"
+    then have "starfun X n - star_of L \<in> Infinitesimal"
+      by (simp only: approx_def)
+    then show "hnorm (starfun X n - star_of L) < star_of r"
       using r by (rule InfinitesimalD2)
   qed
-  thus "\<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
+  then show "\<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
     by transfer
 qed
 
-theorem LIMSEQ_NSLIMSEQ_iff: "(f \<longlonglongrightarrow> L) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
-by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
+theorem LIMSEQ_NSLIMSEQ_iff: "f \<longlonglongrightarrow> L \<longleftrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
+  by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
+
 
 subsubsection \<open>Derived theorems about @{term NSLIMSEQ}\<close>
 
-text\<open>We prove the NS version from the standard one, since the NS proof
-   seems more complicated than the standard one above!\<close>
-lemma NSLIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0) = (X \<longlonglongrightarrow>\<^sub>N\<^sub>S 0)"
-by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_norm_zero_iff)
+text \<open>We prove the NS version from the standard one, since the NS proof
+  seems more complicated than the standard one above!\<close>
+lemma NSLIMSEQ_norm_zero: "(\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0 \<longleftrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
+  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_norm_zero_iff)
 
-lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S (0::real))"
-by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_rabs_zero_iff)
-
-text\<open>Generalization to other limits\<close>
-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>"
-apply (simp add: NSLIMSEQ_def)
-apply (auto intro: approx_hrabs 
-            simp add: starfun_abs)
-done
+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)"
+  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_rabs_zero_iff)
 
-lemma NSLIMSEQ_inverse_zero:
-     "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n)
-      ==> (%n. inverse(f n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
-by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
+text \<open>Generalization to other limits.\<close>
+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>"
+  for l :: real
+  by (simp add: NSLIMSEQ_def) (auto intro: approx_hrabs simp add: starfun_abs)
+
+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"
+  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
 
-lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
-by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat del: of_nat_Suc)
+lemma NSLIMSEQ_inverse_real_of_nat: "(\<lambda>n. inverse (real (Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
+  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat del: of_nat_Suc)
 
-lemma NSLIMSEQ_inverse_real_of_nat_add:
-     "(%n. r + inverse(real(Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
-by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add del: of_nat_Suc)
+lemma NSLIMSEQ_inverse_real_of_nat_add: "(\<lambda>n. r + inverse (real (Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
+  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add del: of_nat_Suc)
 
-lemma NSLIMSEQ_inverse_real_of_nat_add_minus:
-     "(%n. r + -inverse(real(Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
+lemma NSLIMSEQ_inverse_real_of_nat_add_minus: "(\<lambda>n. r + - inverse (real (Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
   using LIMSEQ_inverse_real_of_nat_add_minus by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
 
 lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult:
-     "(%n. r*( 1 + -inverse(real(Suc n)))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
-  using LIMSEQ_inverse_real_of_nat_add_minus_mult by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
+  "(\<lambda>n. r * (1 + - inverse (real (Suc n)))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
+  using LIMSEQ_inverse_real_of_nat_add_minus_mult
+  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
 
 
 subsection \<open>Convergence\<close>
 
-lemma nslimI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L ==> nslim X = L"
-apply (simp add: nslim_def)
-apply (blast intro: NSLIMSEQ_unique)
-done
+lemma nslimI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> nslim X = L"
+  by (simp add: nslim_def) (blast intro: NSLIMSEQ_unique)
 
 lemma lim_nslim_iff: "lim X = nslim X"
-by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)
+  by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)
 
-lemma NSconvergentD: "NSconvergent X ==> \<exists>L. (X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
-by (simp add: NSconvergent_def)
+lemma NSconvergentD: "NSconvergent X \<Longrightarrow> \<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
+  by (simp add: NSconvergent_def)
 
-lemma NSconvergentI: "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S L) ==> NSconvergent X"
-by (auto simp add: NSconvergent_def)
+lemma NSconvergentI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> NSconvergent X"
+  by (auto simp add: NSconvergent_def)
 
 lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X"
-by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)
+  by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)
 
-lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X = (X \<longlonglongrightarrow>\<^sub>N\<^sub>S nslim X)"
-by (auto intro: theI NSLIMSEQ_unique simp add: NSconvergent_def nslim_def)
+lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X \<longleftrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S nslim X"
+  by (auto intro: theI NSLIMSEQ_unique simp add: NSconvergent_def nslim_def)
 
 
 subsection \<open>Bounded Monotonic Sequences\<close>
 
-lemma NSBseqD: "[| NSBseq X;  N: HNatInfinite |] ==> ( *f* X) N : HFinite"
-by (simp add: NSBseq_def)
+lemma NSBseqD: "NSBseq X \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> ( *f* X) N \<in> HFinite"
+  by (simp add: NSBseq_def)
 
 lemma Standard_subset_HFinite: "Standard \<subseteq> HFinite"
-unfolding Standard_def by auto
+  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
+  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
 
-lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite ==> NSBseq X"
-by (simp add: NSBseq_def)
-
-text\<open>The standard definition implies the nonstandard definition\<close>
+lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N \<in> HFinite \<Longrightarrow> NSBseq X"
+  by (simp add: NSBseq_def)
 
-lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
-proof (unfold NSBseq_def, safe)
+text \<open>The standard definition implies the nonstandard definition.\<close>
+lemma Bseq_NSBseq: "Bseq X \<Longrightarrow> NSBseq X"
+  unfolding NSBseq_def
+proof safe
   assume X: "Bseq X"
-  fix N assume N: "N \<in> HNatInfinite"
-  from BseqD [OF X] obtain K where "\<forall>n. norm (X n) \<le> K" by fast
-  hence "\<forall>N. hnorm (starfun X N) \<le> star_of K" by transfer
-  hence "hnorm (starfun X N) \<le> star_of K" by simp
-  also have "star_of K < star_of (K + 1)" by simp
-  finally have "\<exists>x\<in>Reals. hnorm (starfun X N) < x" by (rule bexI, simp)
-  thus "starfun X N \<in> HFinite" by (simp add: HFinite_def)
+  fix N
+  assume N: "N \<in> HNatInfinite"
+  from BseqD [OF X] obtain K where "\<forall>n. norm (X n) \<le> K"
+    by fast
+  then have "\<forall>N. hnorm (starfun X N) \<le> star_of K"
+    by transfer
+  then have "hnorm (starfun X N) \<le> star_of K"
+    by simp
+  also have "star_of K < star_of (K + 1)"
+    by simp
+  finally have "\<exists>x\<in>Reals. hnorm (starfun X N) < x"
+    by (rule bexI) simp
+  then show "starfun X N \<in> HFinite"
+    by (simp add: HFinite_def)
 qed
 
-text\<open>The nonstandard definition implies the standard definition\<close>
-
+text \<open>The nonstandard definition implies the standard definition.\<close>
 lemma SReal_less_omega: "r \<in> \<real> \<Longrightarrow> r < \<omega>"
-apply (insert HInfinite_omega)
-apply (simp add: HInfinite_def)
-apply (simp add: order_less_imp_le)
-done
+  using HInfinite_omega
+  by (simp add: HInfinite_def) (simp add: order_less_imp_le)
 
 lemma NSBseq_Bseq: "NSBseq X \<Longrightarrow> Bseq X"
 proof (rule ccontr)
   let ?n = "\<lambda>K. LEAST n. K < norm (X n)"
   assume "NSBseq X"
-  hence finite: "( *f* X) (( *f* ?n) \<omega>) \<in> HFinite"
+  then have finite: "( *f* X) (( *f* ?n) \<omega>) \<in> HFinite"
     by (rule NSBseqD2)
   assume "\<not> Bseq X"
-  hence "\<forall>K>0. \<exists>n. K < norm (X n)"
+  then have "\<forall>K>0. \<exists>n. K < norm (X n)"
     by (simp add: Bseq_def linorder_not_le)
-  hence "\<forall>K>0. K < norm (X (?n K))"
+  then have "\<forall>K>0. K < norm (X (?n K))"
     by (auto intro: LeastI_ex)
-  hence "\<forall>K>0. K < hnorm (( *f* X) (( *f* ?n) K))"
+  then have "\<forall>K>0. K < hnorm (( *f* X) (( *f* ?n) K))"
     by transfer
-  hence "\<omega> < hnorm (( *f* X) (( *f* ?n) \<omega>))"
+  then have "\<omega> < hnorm (( *f* X) (( *f* ?n) \<omega>))"
     by simp
-  hence "\<forall>r\<in>\<real>. r < hnorm (( *f* X) (( *f* ?n) \<omega>))"
+  then have "\<forall>r\<in>\<real>. r < hnorm (( *f* X) (( *f* ?n) \<omega>))"
     by (simp add: order_less_trans [OF SReal_less_omega])
-  hence "( *f* X) (( *f* ?n) \<omega>) \<in> HInfinite"
+  then have "( *f* X) (( *f* ?n) \<omega>) \<in> HInfinite"
     by (simp add: HInfinite_def)
   with finite show "False"
     by (simp add: HFinite_HInfinite_iff)
 qed
 
-text\<open>Equivalence of nonstandard and standard definitions
-  for a bounded sequence\<close>
-lemma Bseq_NSBseq_iff: "(Bseq X) = (NSBseq X)"
-by (blast intro!: NSBseq_Bseq Bseq_NSBseq)
+text \<open>Equivalence of nonstandard and standard definitions for a bounded sequence.\<close>
+lemma Bseq_NSBseq_iff: "Bseq X = NSBseq X"
+  by (blast intro!: NSBseq_Bseq Bseq_NSBseq)
 
-text\<open>A convergent sequence is bounded: 
- Boundedness as a necessary condition for convergence. 
- The nonstandard version has no existential, as usual\<close>
+text \<open>A convergent sequence is bounded:
+  Boundedness as a necessary condition for convergence.
+  The nonstandard version has no existential, as usual.\<close>
+lemma NSconvergent_NSBseq: "NSconvergent X \<Longrightarrow> NSBseq X"
+  by (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
+    (blast intro: HFinite_star_of approx_sym approx_HFinite)
 
-lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X"
-apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
-apply (blast intro: HFinite_star_of approx_sym approx_HFinite)
-done
+text \<open>Standard Version: easily now proved using equivalence of NS and
+ standard definitions.\<close>
 
-text\<open>Standard Version: easily now proved using equivalence of NS and
- standard definitions\<close>
+lemma convergent_Bseq: "convergent X \<Longrightarrow> Bseq X"
+  for X :: "nat \<Rightarrow> 'b::real_normed_vector"
+  by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
 
-lemma convergent_Bseq: "convergent X ==> Bseq (X::nat \<Rightarrow> _::real_normed_vector)"
-by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
 
-subsubsection\<open>Upper Bounds and Lubs of Bounded Sequences\<close>
+subsubsection \<open>Upper Bounds and Lubs of Bounded Sequences\<close>
 
-lemma NSBseq_isUb: "NSBseq X ==> \<exists>U::real. isUb UNIV {x. \<exists>n. X n = x} U"
-by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)
+lemma NSBseq_isUb: "NSBseq X \<Longrightarrow> \<exists>U::real. isUb UNIV {x. \<exists>n. X n = x} U"
+  by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)
 
-lemma NSBseq_isLub: "NSBseq X ==> \<exists>U::real. isLub UNIV {x. \<exists>n. X n = x} U"
-by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
+lemma NSBseq_isLub: "NSBseq X \<Longrightarrow> \<exists>U::real. isLub UNIV {x. \<exists>n. X n = x} U"
+  by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
+
 
-subsubsection\<open>A Bounded and Monotonic Sequence Converges\<close>
+subsubsection \<open>A Bounded and Monotonic Sequence Converges\<close>
 
-text\<open>The best of both worlds: Easier to prove this result as a standard
+text \<open>The best of both worlds: Easier to prove this result as a standard
    theorem and then use equivalence to "transfer" it into the
    equivalent nonstandard form if needed!\<close>
 
-lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m ==> \<exists>L. (X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
-by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
+lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m \<Longrightarrow> \<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
+  by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
 
-lemma NSBseq_mono_NSconvergent:
-     "[| NSBseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> NSconvergent (X::nat=>real)"
-by (auto intro: Bseq_mono_convergent 
-         simp add: convergent_NSconvergent_iff [symmetric] 
-                   Bseq_NSBseq_iff [symmetric])
+lemma NSBseq_mono_NSconvergent: "NSBseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> NSconvergent X"
+  for X :: "nat \<Rightarrow> real"
+  by (auto intro: Bseq_mono_convergent
+      simp: convergent_NSconvergent_iff [symmetric] Bseq_NSBseq_iff [symmetric])
 
 
 subsection \<open>Cauchy Sequences\<close>
 
 lemma NSCauchyI:
-  "(\<And>M N. \<lbrakk>M \<in> HNatInfinite; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X M \<approx> starfun X N)
-   \<Longrightarrow> NSCauchy X"
-by (simp add: NSCauchy_def)
+  "(\<And>M N. M \<in> HNatInfinite \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> starfun X M \<approx> starfun X N) \<Longrightarrow> NSCauchy X"
+  by (simp add: NSCauchy_def)
 
 lemma NSCauchyD:
-  "\<lbrakk>NSCauchy X; M \<in> HNatInfinite; N \<in> HNatInfinite\<rbrakk>
-   \<Longrightarrow> starfun X M \<approx> starfun X N"
-by (simp add: NSCauchy_def)
+  "NSCauchy X \<Longrightarrow> M \<in> HNatInfinite \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> starfun X M \<approx> starfun X N"
+  by (simp add: NSCauchy_def)
 
-subsubsection\<open>Equivalence Between NS and Standard\<close>
+
+subsubsection \<open>Equivalence Between NS and Standard\<close>
 
 lemma Cauchy_NSCauchy:
-  assumes X: "Cauchy X" shows "NSCauchy X"
+  assumes X: "Cauchy X"
+  shows "NSCauchy X"
 proof (rule NSCauchyI)
-  fix M assume M: "M \<in> HNatInfinite"
-  fix N assume N: "N \<in> HNatInfinite"
+  fix M
+  assume M: "M \<in> HNatInfinite"
+  fix N
+  assume N: "N \<in> HNatInfinite"
   have "starfun X M - starfun X N \<in> Infinitesimal"
   proof (rule InfinitesimalI2)
-    fix r :: real assume r: "0 < r"
-    from CauchyD [OF X r]
-    obtain k where "\<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r" ..
-    hence "\<forall>m\<ge>star_of k. \<forall>n\<ge>star_of k.
-           hnorm (starfun X m - starfun X n) < star_of r"
+    fix r :: real
+    assume r: "0 < r"
+    from CauchyD [OF X r] obtain k where "\<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r" ..
+    then have "\<forall>m\<ge>star_of k. \<forall>n\<ge>star_of k. hnorm (starfun X m - starfun X n) < star_of r"
       by transfer
-    thus "hnorm (starfun X M - starfun X N) < star_of r"
+    then show "hnorm (starfun X M - starfun X N) < star_of r"
       using M N by (simp add: star_of_le_HNatInfinite)
   qed
-  thus "starfun X M \<approx> starfun X N"
-    by (unfold approx_def)
+  then show "starfun X M \<approx> starfun X N"
+    by (simp only: approx_def)
 qed
 
 lemma NSCauchy_Cauchy:
-  assumes X: "NSCauchy X" shows "Cauchy X"
+  assumes X: "NSCauchy X"
+  shows "Cauchy X"
 proof (rule CauchyI)
-  fix r::real assume r: "0 < r"
+  fix r :: real
+  assume r: "0 < r"
   have "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. hnorm (starfun X m - starfun X n) < star_of r"
   proof (intro exI allI impI)
-    fix M assume "whn \<le> M"
+    fix M
+    assume "whn \<le> M"
     with HNatInfinite_whn have M: "M \<in> HNatInfinite"
       by (rule HNatInfinite_upward_closed)
-    fix N assume "whn \<le> N"
+    fix N
+    assume "whn \<le> N"
     with HNatInfinite_whn have N: "N \<in> HNatInfinite"
       by (rule HNatInfinite_upward_closed)
     from X M N have "starfun X M \<approx> starfun X N"
       by (rule NSCauchyD)
-    hence "starfun X M - starfun X N \<in> Infinitesimal"
-      by (unfold approx_def)
-    thus "hnorm (starfun X M - starfun X N) < star_of r"
+    then have "starfun X M - starfun X N \<in> Infinitesimal"
+      by (simp only: approx_def)
+    then show "hnorm (starfun X M - starfun X N) < star_of r"
       using r by (rule InfinitesimalD2)
   qed
-  thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r"
+  then show "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r"
     by transfer
 qed
 
 theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X"
-by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
+  by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
+
 
 subsubsection \<open>Cauchy Sequences are Bounded\<close>
 
-text\<open>A Cauchy sequence is bounded -- nonstandard version\<close>
+text \<open>A Cauchy sequence is bounded -- nonstandard version.\<close>
 
-lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X"
-by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
+lemma NSCauchy_NSBseq: "NSCauchy X \<Longrightarrow> NSBseq X"
+  by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
+
 
 subsubsection \<open>Cauchy Sequences are Convergent\<close>
 
-text\<open>Equivalence of Cauchy criterion and convergence:
+text \<open>Equivalence of Cauchy criterion and convergence:
   We will prove this using our NS formulation which provides a
   much easier proof than using the standard definition. We do not
   need to use properties of subsequences such as boundedness,
@@ -453,64 +450,60 @@
   since the NS formulations do not involve existential quantifiers.\<close>
 
 lemma NSconvergent_NSCauchy: "NSconvergent X \<Longrightarrow> NSCauchy X"
-apply (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def, safe)
-apply (auto intro: approx_trans2)
-done
+  by (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def) (auto intro: approx_trans2)
 
-lemma real_NSCauchy_NSconvergent:
-  fixes X :: "nat \<Rightarrow> real"
-  shows "NSCauchy X \<Longrightarrow> NSconvergent X"
-apply (simp add: NSconvergent_def NSLIMSEQ_def)
-apply (frule NSCauchy_NSBseq)
-apply (simp add: NSBseq_def NSCauchy_def)
-apply (drule HNatInfinite_whn [THEN [2] bspec])
-apply (drule HNatInfinite_whn [THEN [2] bspec])
-apply (auto dest!: st_part_Ex simp add: SReal_iff)
-apply (blast intro: approx_trans3)
-done
+lemma real_NSCauchy_NSconvergent: "NSCauchy X \<Longrightarrow> NSconvergent X"
+  for X :: "nat \<Rightarrow> real"
+  apply (simp add: NSconvergent_def NSLIMSEQ_def)
+  apply (frule NSCauchy_NSBseq)
+  apply (simp add: NSBseq_def NSCauchy_def)
+  apply (drule HNatInfinite_whn [THEN [2] bspec])
+  apply (drule HNatInfinite_whn [THEN [2] bspec])
+  apply (auto dest!: st_part_Ex simp add: SReal_iff)
+  apply (blast intro: approx_trans3)
+  done
 
-lemma NSCauchy_NSconvergent:
-  fixes X :: "nat \<Rightarrow> 'a::banach"
-  shows "NSCauchy X \<Longrightarrow> NSconvergent X"
-apply (drule NSCauchy_Cauchy [THEN Cauchy_convergent])
-apply (erule convergent_NSconvergent_iff [THEN iffD1])
-done
+lemma NSCauchy_NSconvergent: "NSCauchy X \<Longrightarrow> NSconvergent X"
+  for X :: "nat \<Rightarrow> 'a::banach"
+  apply (drule NSCauchy_Cauchy [THEN Cauchy_convergent])
+  apply (erule convergent_NSconvergent_iff [THEN iffD1])
+  done
 
-lemma NSCauchy_NSconvergent_iff:
-  fixes X :: "nat \<Rightarrow> 'a::banach"
-  shows "NSCauchy X = NSconvergent X"
-by (fast intro: NSCauchy_NSconvergent NSconvergent_NSCauchy)
+lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X"
+  for X :: "nat \<Rightarrow> 'a::banach"
+  by (fast intro: NSCauchy_NSconvergent NSconvergent_NSCauchy)
 
 
 subsection \<open>Power Sequences\<close>
 
-text\<open>The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
-"x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
+text \<open>The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
+  "x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
   also fact that bounded and monotonic sequence converges.\<close>
 
-text\<open>We now use NS criterion to bring proof of theorem through\<close>
+text \<open>We now use NS criterion to bring proof of theorem through.\<close>
+lemma NSLIMSEQ_realpow_zero: "0 \<le> x \<Longrightarrow> x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
+  for x :: real
+  apply (simp add: NSLIMSEQ_def)
+  apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
+  apply (frule NSconvergentD)
+  apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfun_pow)
+  apply (frule HNatInfinite_add_one)
+  apply (drule bspec, assumption)
+  apply (drule bspec, assumption)
+  apply (drule_tac x = "N + 1" in bspec, assumption)
+  apply (simp add: hyperpow_add)
+  apply (drule approx_mult_subst_star_of, assumption)
+  apply (drule approx_trans3, assumption)
+  apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric])
+  done
 
-lemma NSLIMSEQ_realpow_zero:
-  "[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
-apply (simp add: NSLIMSEQ_def)
-apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
-apply (frule NSconvergentD)
-apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfun_pow)
-apply (frule HNatInfinite_add_one)
-apply (drule bspec, assumption)
-apply (drule bspec, assumption)
-apply (drule_tac x = "N + (1::hypnat) " in bspec, assumption)
-apply (simp add: hyperpow_add)
-apply (drule approx_mult_subst_star_of, assumption)
-apply (drule approx_trans3, assumption)
-apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric])
-done
+lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
+  for c :: real
+  by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
 
-lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < (1::real) ==> (%n. \<bar>c\<bar> ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
-by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
-
-lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
-by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
+lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
+  for c :: real
+  by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
 
 (***---------------------------------------------------------------
     Theorems proved by Harrison in HOL that we do not need
diff -r a7f5e59378f7 -r 2bf8cfc98c4d src/HOL/Nonstandard_Analysis/HSeries.thy
--- a/src/HOL/Nonstandard_Analysis/HSeries.thy	Sun Dec 18 22:14:53 2016 +0100
+++ b/src/HOL/Nonstandard_Analysis/HSeries.thy	Sun Dec 18 23:43:50 2016 +0100
@@ -5,200 +5,177 @@
 Converted to Isar and polished by lcp
 *)
 
-section\<open>Finite Summation and Infinite Series for Hyperreals\<close>
+section \<open>Finite Summation and Infinite Series for Hyperreals\<close>
 
 theory HSeries
-imports HSEQ
+  imports HSEQ
 begin
 
-definition
-  sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where
-  "sumhr =
-      (%(M,N,f). starfun2 (%m n. sum f {m..<n}) M N)"
+definition sumhr :: "hypnat \<times> hypnat \<times> (nat \<Rightarrow> real) \<Rightarrow> hypreal"
+  where "sumhr = (\<lambda>(M,N,f). starfun2 (\<lambda>m n. sum f {m..<n}) M N)"
+
+definition NSsums :: "(nat \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool"  (infixr "NSsums" 80)
+  where "f NSsums s = (\<lambda>n. sum f {..<n}) \<longlonglongrightarrow>\<^sub>N\<^sub>S s"
 
-definition
-  NSsums  :: "[nat=>real,real] => bool"     (infixr "NSsums" 80) where
-  "f NSsums s = (%n. sum f {..<n}) \<longlonglongrightarrow>\<^sub>N\<^sub>S s"
+definition NSsummable :: "(nat \<Rightarrow> real) \<Rightarrow> bool"
+  where "NSsummable f \<longleftrightarrow> (\<exists>s. f NSsums s)"
 
-definition
-  NSsummable :: "(nat=>real) => bool" where
-  "NSsummable f = (\<exists>s. f NSsums s)"
+definition NSsuminf :: "(nat \<Rightarrow> real) \<Rightarrow> real"
+  where "NSsuminf f = (THE s. f NSsums s)"
 
-definition
-  NSsuminf   :: "(nat=>real) => real" where
-  "NSsuminf f = (THE s. f NSsums s)"
+lemma sumhr_app: "sumhr (M, N, f) = ( *f2* (\<lambda>m n. sum f {m..<n})) M N"
+  by (simp add: sumhr_def)
 
-lemma sumhr_app: "sumhr(M,N,f) = ( *f2* (\<lambda>m n. sum f {m..<n})) M N"
-by (simp add: sumhr_def)
+text \<open>Base case in definition of @{term sumr}.\<close>
+lemma sumhr_zero [simp]: "\<And>m. sumhr (m, 0, f) = 0"
+  unfolding sumhr_app by transfer simp
 
-text\<open>Base case in definition of @{term sumr}\<close>
-lemma sumhr_zero [simp]: "!!m. sumhr (m,0,f) = 0"
-unfolding sumhr_app by transfer simp
-
-text\<open>Recursive case in definition of @{term sumr}\<close>
+text \<open>Recursive case in definition of @{term sumr}.\<close>
 lemma sumhr_if:
-     "!!m n. sumhr(m,n+1,f) =
-      (if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *f* f) n)"
-unfolding sumhr_app by transfer simp
+  "\<And>m n. sumhr (m, n + 1, f) = (if n + 1 \<le> m then 0 else sumhr (m, n, f) + ( *f* f) n)"
+  unfolding sumhr_app by transfer simp
+
+lemma sumhr_Suc_zero [simp]: "\<And>n. sumhr (n + 1, n, f) = 0"
+  unfolding sumhr_app by transfer simp
 
-lemma sumhr_Suc_zero [simp]: "!!n. sumhr (n + 1, n, f) = 0"
-unfolding sumhr_app by transfer simp
+lemma sumhr_eq_bounds [simp]: "\<And>n. sumhr (n, n, f) = 0"
+  unfolding sumhr_app by transfer simp
 
-lemma sumhr_eq_bounds [simp]: "!!n. sumhr (n,n,f) = 0"
-unfolding sumhr_app by transfer simp
+lemma sumhr_Suc [simp]: "\<And>m. sumhr (m, m + 1, f) = ( *f* f) m"
+  unfolding sumhr_app by transfer simp
 
-lemma sumhr_Suc [simp]: "!!m. sumhr (m,m + 1,f) = ( *f* f) m"
-unfolding sumhr_app by transfer simp
+lemma sumhr_add_lbound_zero [simp]: "\<And>k m. sumhr (m + k, k, f) = 0"
+  unfolding sumhr_app by transfer simp
 
-lemma sumhr_add_lbound_zero [simp]: "!!k m. sumhr(m+k,k,f) = 0"
-unfolding sumhr_app by transfer simp
+lemma sumhr_add: "\<And>m n. sumhr (m, n, f) + sumhr (m, n, g) = sumhr (m, n, \<lambda>i. f i + g i)"
+  unfolding sumhr_app by transfer (rule sum.distrib [symmetric])
 
-lemma sumhr_add:
-  "!!m n. sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
-unfolding sumhr_app by transfer (rule sum.distrib [symmetric])
+lemma sumhr_mult: "\<And>m n. hypreal_of_real r * sumhr (m, n, f) = sumhr (m, n, \<lambda>n. r * f n)"
+  unfolding sumhr_app by transfer (rule sum_distrib_left)
 
-lemma sumhr_mult:
-  "!!m n. hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
-unfolding sumhr_app by transfer (rule sum_distrib_left)
+lemma sumhr_split_add: "\<And>n p. n < p \<Longrightarrow> sumhr (0, n, f) + sumhr (n, p, f) = sumhr (0, p, f)"
+  unfolding sumhr_app by transfer (simp add: sum_add_nat_ivl)
 
-lemma sumhr_split_add:
-  "!!n p. n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
-unfolding sumhr_app by transfer (simp add: sum_add_nat_ivl)
+lemma sumhr_split_diff: "n < p \<Longrightarrow> sumhr (0, p, f) - sumhr (0, n, f) = sumhr (n, p, f)"
+  by (drule sumhr_split_add [symmetric, where f = f]) simp
 
-lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)"
-by (drule_tac f = f in sumhr_split_add [symmetric], simp)
+lemma sumhr_hrabs: "\<And>m n. \<bar>sumhr (m, n, f)\<bar> \<le> sumhr (m, n, \<lambda>i. \<bar>f i\<bar>)"
+  unfolding sumhr_app by transfer (rule sum_abs)
 
-lemma sumhr_hrabs: "!!m n. \<bar>sumhr(m,n,f)\<bar> \<le> sumhr(m,n,%i. \<bar>f i\<bar>)"
-unfolding sumhr_app by transfer (rule sum_abs)
-
-text\<open>other general version also needed\<close>
+text \<open>Other general version also needed.\<close>
 lemma sumhr_fun_hypnat_eq:
-   "(\<forall>r. m \<le> r & r < n --> f r = g r) -->
-      sumhr(hypnat_of_nat m, hypnat_of_nat n, f) =
-      sumhr(hypnat_of_nat m, hypnat_of_nat n, g)"
-unfolding sumhr_app by transfer simp
+  "(\<forall>r. m \<le> r \<and> r < n \<longrightarrow> f r = g r) \<longrightarrow>
+    sumhr (hypnat_of_nat m, hypnat_of_nat n, f) =
+    sumhr (hypnat_of_nat m, hypnat_of_nat n, g)"
+  unfolding sumhr_app by transfer simp
 
-lemma sumhr_const:
-     "!!n. sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
-unfolding sumhr_app by transfer simp
+lemma sumhr_const: "\<And>n. sumhr (0, n, \<lambda>i. r) = hypreal_of_hypnat n * hypreal_of_real r"
+  unfolding sumhr_app by transfer simp
 
-lemma sumhr_less_bounds_zero [simp]: "!!m n. n < m ==> sumhr(m,n,f) = 0"
-unfolding sumhr_app by transfer simp
+lemma sumhr_less_bounds_zero [simp]: "\<And>m n. n < m \<Longrightarrow> sumhr (m, n, f) = 0"
+  unfolding sumhr_app by transfer simp
 
-lemma sumhr_minus: "!!m n. sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
-unfolding sumhr_app by transfer (rule sum_negf)
+lemma sumhr_minus: "\<And>m n. sumhr (m, n, \<lambda>i. - f i) = - sumhr (m, n, f)"
+  unfolding sumhr_app by transfer (rule sum_negf)
 
 lemma sumhr_shift_bounds:
-  "!!m n. sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) =
-          sumhr(m,n,%i. f(i + k))"
-unfolding sumhr_app by transfer (rule sum_shift_bounds_nat_ivl)
+  "\<And>m n. sumhr (m + hypnat_of_nat k, n + hypnat_of_nat k, f) =
+    sumhr (m, n, \<lambda>i. f (i + k))"
+  unfolding sumhr_app by transfer (rule sum_shift_bounds_nat_ivl)
 
 
-subsection\<open>Nonstandard Sums\<close>
+subsection \<open>Nonstandard Sums\<close>
 
-text\<open>Infinite sums are obtained by summing to some infinite hypernatural
- (such as @{term whn})\<close>
-lemma sumhr_hypreal_of_hypnat_omega:
-      "sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn"
-by (simp add: sumhr_const)
+text \<open>Infinite sums are obtained by summing to some infinite hypernatural
+  (such as @{term whn}).\<close>
+lemma sumhr_hypreal_of_hypnat_omega: "sumhr (0, whn, \<lambda>i. 1) = hypreal_of_hypnat whn"
+  by (simp add: sumhr_const)
 
-lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = \<omega> - 1"
-apply (simp add: sumhr_const)
-(* FIXME: need lemma: hypreal_of_hypnat whn = \<omega> - 1 *)
-(* maybe define \<omega> = hypreal_of_hypnat whn + 1 *)
-apply (unfold star_class_defs omega_def hypnat_omega_def
-              of_hypnat_def star_of_def)
-apply (simp add: starfun_star_n starfun2_star_n)
-done
+lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, \<lambda>i. 1) = \<omega> - 1"
+  apply (simp add: sumhr_const)
+    (* FIXME: need lemma: hypreal_of_hypnat whn = \<omega> - 1 *)
+    (* maybe define \<omega> = hypreal_of_hypnat whn + 1 *)
+  apply (unfold star_class_defs omega_def hypnat_omega_def of_hypnat_def star_of_def)
+  apply (simp add: starfun_star_n starfun2_star_n)
+  done
 
-lemma sumhr_minus_one_realpow_zero [simp]:
-     "!!N. sumhr(0, N + N, %i. (-1) ^ (i+1)) = 0"
-unfolding sumhr_app
-apply transfer
-apply (simp del: power_Suc add: mult_2 [symmetric])
-apply (induct_tac N)
-apply simp_all
-done
+lemma sumhr_minus_one_realpow_zero [simp]: "\<And>N. sumhr (0, N + N, \<lambda>i. (-1) ^ (i + 1)) = 0"
+  unfolding sumhr_app
+  apply transfer
+  apply (simp del: power_Suc add: mult_2 [symmetric])
+  apply (induct_tac N)
+   apply simp_all
+  done
 
 lemma sumhr_interval_const:
-     "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na
-      ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) =
-          (hypreal_of_nat (na - m) * hypreal_of_real r)"
-unfolding sumhr_app by transfer simp
+  "(\<forall>n. m \<le> Suc n \<longrightarrow> f n = r) \<and> m \<le> na \<Longrightarrow>
+    sumhr (hypnat_of_nat m, hypnat_of_nat na, f) = hypreal_of_nat (na - m) * hypreal_of_real r"
+  unfolding sumhr_app by transfer simp
 
-lemma starfunNat_sumr: "!!N. ( *f* (%n. sum f {0..<n})) N = sumhr(0,N,f)"
-unfolding sumhr_app by transfer (rule refl)
+lemma starfunNat_sumr: "\<And>N. ( *f* (\<lambda>n. sum f {0..<n})) N = sumhr (0, N, f)"
+  unfolding sumhr_app by transfer (rule refl)
 
-lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) \<approx> sumhr(0, N, f)
-      ==> \<bar>sumhr(M, N, f)\<bar> \<approx> 0"
-apply (cut_tac x = M and y = N in linorder_less_linear)
-apply (auto simp add: approx_refl)
-apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
-apply (auto dest: approx_hrabs
-            simp add: sumhr_split_diff)
-done
+lemma sumhr_hrabs_approx [simp]: "sumhr (0, M, f) \<approx> sumhr (0, N, f) \<Longrightarrow> \<bar>sumhr (M, N, f)\<bar> \<approx> 0"
+  using linorder_less_linear [where x = M and y = N]
+  apply auto
+  apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
+  apply (auto dest: approx_hrabs simp add: sumhr_split_diff)
+  done
+
+
+subsection \<open>Infinite sums: Standard and NS theorems\<close>
 
-(*----------------------------------------------------------------
-      infinite sums: Standard and NS theorems
- ----------------------------------------------------------------*)
-lemma sums_NSsums_iff: "(f sums l) = (f NSsums l)"
-by (simp add: sums_def NSsums_def LIMSEQ_NSLIMSEQ_iff)
+lemma sums_NSsums_iff: "f sums l \<longleftrightarrow> f NSsums l"
+  by (simp add: sums_def NSsums_def LIMSEQ_NSLIMSEQ_iff)
 
-lemma summable_NSsummable_iff: "(summable f) = (NSsummable f)"
-by (simp add: summable_def NSsummable_def sums_NSsums_iff)
+lemma summable_NSsummable_iff: "summable f \<longleftrightarrow> NSsummable f"
+  by (simp add: summable_def NSsummable_def sums_NSsums_iff)
 
-lemma suminf_NSsuminf_iff: "(suminf f) = (NSsuminf f)"
-by (simp add: suminf_def NSsuminf_def sums_NSsums_iff)
+lemma suminf_NSsuminf_iff: "suminf f = NSsuminf f"
+  by (simp add: suminf_def NSsuminf_def sums_NSsums_iff)
 
-lemma NSsums_NSsummable: "f NSsums l ==> NSsummable f"
-by (simp add: NSsums_def NSsummable_def, blast)
+lemma NSsums_NSsummable: "f NSsums l \<Longrightarrow> NSsummable f"
+  unfolding NSsums_def NSsummable_def by blast
 
-lemma NSsummable_NSsums: "NSsummable f ==> f NSsums (NSsuminf f)"
-apply (simp add: NSsummable_def NSsuminf_def NSsums_def)
-apply (blast intro: theI NSLIMSEQ_unique)
-done
+lemma NSsummable_NSsums: "NSsummable f \<Longrightarrow> f NSsums (NSsuminf f)"
+  unfolding NSsummable_def NSsuminf_def NSsums_def
+  by (blast intro: theI NSLIMSEQ_unique)
 
-lemma NSsums_unique: "f NSsums s ==> (s = NSsuminf f)"
-by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)
+lemma NSsums_unique: "f NSsums s \<Longrightarrow> s = NSsuminf f"
+  by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)
 
-lemma NSseries_zero:
-  "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (sum f {..<n})"
-by (auto simp add: sums_NSsums_iff [symmetric] not_le[symmetric] intro!: sums_finite)
+lemma NSseries_zero: "\<forall>m. n \<le> Suc m \<longrightarrow> f m = 0 \<Longrightarrow> f NSsums (sum f {..<n})"
+  by (auto simp add: sums_NSsums_iff [symmetric] not_le[symmetric] intro!: sums_finite)
 
 lemma NSsummable_NSCauchy:
-     "NSsummable f =
-      (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. \<bar>sumhr(M,N,f)\<bar> \<approx> 0)"
-apply (auto simp add: summable_NSsummable_iff [symmetric]
-       summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
-       NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
-apply (cut_tac x = M and y = N in linorder_less_linear)
-apply auto
-apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
-apply (rule_tac [2] approx_minus_iff [THEN iffD2])
-apply (auto dest: approx_hrabs_zero_cancel
-            simp add: sumhr_split_diff atLeast0LessThan[symmetric])
-done
+  "NSsummable f \<longleftrightarrow> (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. \<bar>sumhr (M, N, f)\<bar> \<approx> 0)"
+  apply (auto simp add: summable_NSsummable_iff [symmetric]
+      summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
+      NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
+  apply (cut_tac x = M and y = N in linorder_less_linear)
+  apply auto
+   apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
+   apply (rule_tac [2] approx_minus_iff [THEN iffD2])
+   apply (auto dest: approx_hrabs_zero_cancel simp: sumhr_split_diff atLeast0LessThan[symmetric])
+  done
 
-text\<open>Terms of a convergent series tend to zero\<close>
-lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ==> f \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
-apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
-apply (drule bspec, auto)
-apply (drule_tac x = "N + 1 " in bspec)
-apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
-done
+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)
+  apply (drule bspec)
+   apply auto
+  apply (drule_tac x = "N + 1 " in bspec)
+   apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
+  done
 
-text\<open>Nonstandard comparison test\<close>
-lemma NSsummable_comparison_test:
-     "[| \<exists>N. \<forall>n. N \<le> n --> \<bar>f n\<bar> \<le> g n; NSsummable g |] ==> NSsummable f"
-apply (fold summable_NSsummable_iff)
-apply (rule summable_comparison_test, simp, assumption)
-done
+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"
+  apply (fold summable_NSsummable_iff)
+  apply (rule summable_comparison_test, simp, assumption)
+  done
 
 lemma NSsummable_rabs_comparison_test:
-     "[| \<exists>N. \<forall>n. N \<le> n --> \<bar>f n\<bar> \<le> g n; NSsummable g |]
-      ==> NSsummable (%k. \<bar>f k\<bar>)"
-apply (rule NSsummable_comparison_test)
-apply (auto)
-done
+  "\<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>)"
+  by (rule NSsummable_comparison_test) auto
 
 end