# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1556466619 -3600
# Node ID 65b3bfc565b531610b42619143c82a8dc6590a66
# Parent  373eb0aa97e302dc86687edb6a5fed436f3aaccc
removal of ASCII connectives; some de-applying

diff -r 373eb0aa97e3 -r 65b3bfc565b5 src/HOL/Nonstandard_Analysis/HTranscendental.thy
--- a/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Sat Apr 27 21:56:59 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Sun Apr 28 16:50:19 2019 +0100
@@ -8,229 +8,161 @@
 section\<open>Nonstandard Extensions of Transcendental Functions\<close>
 
 theory HTranscendental
-imports Complex_Main HSeries HDeriv
+imports Complex_Main HSeries HDeriv Sketch_and_Explore
 begin
 
+
+sledgehammer_params [timeout = 90]
+
 definition
-  exphr :: "real => hypreal" where
+  exphr :: "real \<Rightarrow> hypreal" where
     \<comment> \<open>define exponential function using standard part\<close>
-  "exphr x =  st(sumhr (0, whn, %n. inverse (fact n) * (x ^ n)))"
+  "exphr x \<equiv>  st(sumhr (0, whn, \<lambda>n. inverse (fact n) * (x ^ n)))"
 
 definition
-  sinhr :: "real => hypreal" where
-  "sinhr x = st(sumhr (0, whn, %n. sin_coeff n * x ^ n))"
+  sinhr :: "real \<Rightarrow> hypreal" where
+  "sinhr x \<equiv> st(sumhr (0, whn, \<lambda>n. sin_coeff n * x ^ n))"
   
 definition
-  coshr :: "real => hypreal" where
-  "coshr x = st(sumhr (0, whn, %n. cos_coeff n * x ^ n))"
+  coshr :: "real \<Rightarrow> hypreal" where
+  "coshr x \<equiv> st(sumhr (0, whn, \<lambda>n. cos_coeff n * x ^ n))"
 
 
 subsection\<open>Nonstandard Extension of Square Root Function\<close>
 
 lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0"
-by (simp add: starfun star_n_zero_num)
+  by (simp add: starfun star_n_zero_num)
 
 lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1"
-by (simp add: starfun star_n_one_num)
+  by (simp add: starfun star_n_one_num)
 
 lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
-apply (cases x)
-apply (auto simp add: star_n_le star_n_zero_num starfun hrealpow star_n_eq_iff
-            simp del: hpowr_Suc power_Suc)
-done
-
-lemma hypreal_sqrt_gt_zero_pow2: "!!x. 0 < x ==> ( *f* sqrt) (x) ^ 2 = x"
-by (transfer, simp)
+proof (cases x)
+  case (star_n X)
+  then show ?thesis
+    by (simp add: star_n_le star_n_zero_num starfun hrealpow star_n_eq_iff del: hpowr_Suc power_Suc)
+qed
 
-lemma hypreal_sqrt_pow2_gt_zero: "0 < x ==> 0 < ( *f* sqrt) (x) ^ 2"
-by (frule hypreal_sqrt_gt_zero_pow2, auto)
+lemma hypreal_sqrt_gt_zero_pow2: "\<And>x. 0 < x \<Longrightarrow> ( *f* sqrt) (x) ^ 2 = x"
+  by transfer simp
 
-lemma hypreal_sqrt_not_zero: "0 < x ==> ( *f* sqrt) (x) \<noteq> 0"
-apply (frule hypreal_sqrt_pow2_gt_zero)
-apply (auto simp add: numeral_2_eq_2)
-done
+lemma hypreal_sqrt_pow2_gt_zero: "0 < x \<Longrightarrow> 0 < ( *f* sqrt) (x) ^ 2"
+  by (frule hypreal_sqrt_gt_zero_pow2, auto)
+
+lemma hypreal_sqrt_not_zero: "0 < x \<Longrightarrow> ( *f* sqrt) (x) \<noteq> 0"
+  using hypreal_sqrt_gt_zero_pow2 by fastforce
 
 lemma hypreal_inverse_sqrt_pow2:
-     "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"
-apply (cut_tac n = 2 and a = "( *f* sqrt) x" in power_inverse [symmetric])
-apply (auto dest: hypreal_sqrt_gt_zero_pow2)
-done
+     "0 < x \<Longrightarrow> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"
+  by (simp add: hypreal_sqrt_gt_zero_pow2 power_inverse)
 
 lemma hypreal_sqrt_mult_distrib: 
-    "!!x y. [|0 < x; 0 <y |] ==>
+    "\<And>x y. \<lbrakk>0 < x; 0 <y\<rbrakk> \<Longrightarrow>
       ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"
-apply transfer
-apply (auto intro: real_sqrt_mult) 
-done
+  by transfer (auto intro: real_sqrt_mult) 
 
 lemma hypreal_sqrt_mult_distrib2:
-     "[|0\<le>x; 0\<le>y |] ==>  
-     ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)"
+     "\<lbrakk>0\<le>x; 0\<le>y\<rbrakk> \<Longrightarrow>  ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"
 by (auto intro: hypreal_sqrt_mult_distrib simp add: order_le_less)
 
 lemma hypreal_sqrt_approx_zero [simp]:
-     "0 < x ==> (( *f* sqrt)(x) \<approx> 0) = (x \<approx> 0)"
-apply (auto simp add: mem_infmal_iff [symmetric])
-apply (rule hypreal_sqrt_gt_zero_pow2 [THEN subst])
-apply (auto intro: Infinitesimal_mult 
-            dest!: hypreal_sqrt_gt_zero_pow2 [THEN ssubst] 
-            simp add: numeral_2_eq_2)
-done
+  assumes "0 < x"
+  shows "(( *f* sqrt) x \<approx> 0) \<longleftrightarrow> (x \<approx> 0)"
+proof -
+  have "( *f* sqrt) x \<in> Infinitesimal \<longleftrightarrow> ((*f* sqrt) x)\<^sup>2 \<in> Infinitesimal"
+    by (metis Infinitesimal_hrealpow pos2 power2_eq_square Infinitesimal_square_iff)
+  also have "... \<longleftrightarrow> x \<in> Infinitesimal"
+    by (simp add: assms hypreal_sqrt_gt_zero_pow2)
+  finally show ?thesis
+    using mem_infmal_iff by blast
+qed
 
 lemma hypreal_sqrt_approx_zero2 [simp]:
-     "0 \<le> x ==> (( *f* sqrt)(x) \<approx> 0) = (x \<approx> 0)"
-by (auto simp add: order_le_less)
+  "0 \<le> x \<Longrightarrow> (( *f* sqrt)(x) \<approx> 0) = (x \<approx> 0)"
+  by (auto simp add: order_le_less)
 
-lemma hypreal_sqrt_sum_squares [simp]:
-     "(( *f* sqrt)(x*x + y*y + z*z) \<approx> 0) = (x*x + y*y + z*z \<approx> 0)"
-apply (rule hypreal_sqrt_approx_zero2)
-apply (rule add_nonneg_nonneg)+
-apply (auto)
-done
+lemma hypreal_sqrt_gt_zero: "\<And>x. 0 < x \<Longrightarrow> 0 < ( *f* sqrt)(x)"
+  by transfer (simp add: real_sqrt_gt_zero)
 
-lemma hypreal_sqrt_sum_squares2 [simp]:
-     "(( *f* sqrt)(x*x + y*y) \<approx> 0) = (x*x + y*y \<approx> 0)"
-apply (rule hypreal_sqrt_approx_zero2)
-apply (rule add_nonneg_nonneg)
-apply (auto)
-done
+lemma hypreal_sqrt_ge_zero: "0 \<le> x \<Longrightarrow> 0 \<le> ( *f* sqrt)(x)"
+  by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
 
-lemma hypreal_sqrt_gt_zero: "!!x. 0 < x ==> 0 < ( *f* sqrt)(x)"
-apply transfer
-apply (auto intro: real_sqrt_gt_zero)
-done
+lemma hypreal_sqrt_hrabs [simp]: "\<And>x. ( *f* sqrt)(x\<^sup>2) = \<bar>x\<bar>"
+  by transfer simp
 
-lemma hypreal_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> ( *f* sqrt)(x)"
-by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
-
-lemma hypreal_sqrt_hrabs [simp]: "!!x. ( *f* sqrt)(x\<^sup>2) = \<bar>x\<bar>"
-by (transfer, simp)
-
-lemma hypreal_sqrt_hrabs2 [simp]: "!!x. ( *f* sqrt)(x*x) = \<bar>x\<bar>"
-by (transfer, simp)
+lemma hypreal_sqrt_hrabs2 [simp]: "\<And>x. ( *f* sqrt)(x*x) = \<bar>x\<bar>"
+  by transfer simp
 
 lemma hypreal_sqrt_hyperpow_hrabs [simp]:
-     "!!x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = \<bar>x\<bar>"
-by (transfer, simp)
+  "\<And>x. ( *f* sqrt)(x pow (hypnat_of_nat 2)) = \<bar>x\<bar>"
+  by transfer simp
 
 lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite"
-apply (rule HFinite_square_iff [THEN iffD1])
-apply (simp only: hypreal_sqrt_mult_distrib2 [symmetric], simp) 
-done
+  by (metis HFinite_square_iff hypreal_sqrt_pow2_iff power2_eq_square)
 
 lemma st_hypreal_sqrt:
-     "[| x \<in> HFinite; 0 \<le> x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)"
-apply (rule power_inject_base [where n=1])
-apply (auto intro!: st_zero_le hypreal_sqrt_ge_zero)
-apply (rule st_mult [THEN subst])
-apply (rule_tac [3] hypreal_sqrt_mult_distrib2 [THEN subst])
-apply (rule_tac [5] hypreal_sqrt_mult_distrib2 [THEN subst])
-apply (auto simp add: st_hrabs st_zero_le star_sqrt_HFinite)
-done
+  assumes "x \<in> HFinite" "0 \<le> x"
+  shows "st(( *f* sqrt) x) = ( *f* sqrt)(st x)"
+proof (rule power_inject_base)
+  show "st ((*f* sqrt) x) ^ Suc 1 = (*f* sqrt) (st x) ^ Suc 1"
+    using assms hypreal_sqrt_pow2_iff [of x]
+    by (metis HFinite_square_iff hypreal_sqrt_hrabs2 power2_eq_square st_hrabs st_mult)
+  show "0 \<le> st ((*f* sqrt) x)"
+    by (simp add: assms hypreal_sqrt_ge_zero st_zero_le star_sqrt_HFinite)
+  show "0 \<le> (*f* sqrt) (st x)"
+    by (simp add: assms hypreal_sqrt_ge_zero st_zero_le)
+qed
 
-lemma hypreal_sqrt_sum_squares_ge1 [simp]: "!!x y. x \<le> ( *f* sqrt)(x\<^sup>2 + y\<^sup>2)"
-by transfer (rule real_sqrt_sum_squares_ge1)
-
-lemma HFinite_hypreal_sqrt:
-     "[| 0 \<le> x; x \<in> HFinite |] ==> ( *f* sqrt) x \<in> HFinite"
-apply (auto simp add: order_le_less)
-apply (rule HFinite_square_iff [THEN iffD1])
-apply (drule hypreal_sqrt_gt_zero_pow2)
-apply (simp add: numeral_2_eq_2)
-done
+lemma hypreal_sqrt_sum_squares_ge1 [simp]: "\<And>x y. x \<le> ( *f* sqrt)(x\<^sup>2 + y\<^sup>2)"
+  by transfer (rule real_sqrt_sum_squares_ge1)
 
 lemma HFinite_hypreal_sqrt_imp_HFinite:
-     "[| 0 \<le> x; ( *f* sqrt) x \<in> HFinite |] ==> x \<in> HFinite"
-apply (auto simp add: order_le_less)
-apply (drule HFinite_square_iff [THEN iffD2])
-apply (drule hypreal_sqrt_gt_zero_pow2)
-apply (simp add: numeral_2_eq_2 del: HFinite_square_iff)
-done
+  "\<lbrakk>0 \<le> x; ( *f* sqrt) x \<in> HFinite\<rbrakk> \<Longrightarrow> x \<in> HFinite"
+  by (metis HFinite_mult hrealpow_two hypreal_sqrt_pow2_iff numeral_2_eq_2)
 
 lemma HFinite_hypreal_sqrt_iff [simp]:
-     "0 \<le> x ==> (( *f* sqrt) x \<in> HFinite) = (x \<in> HFinite)"
-by (blast intro: HFinite_hypreal_sqrt HFinite_hypreal_sqrt_imp_HFinite)
-
-lemma HFinite_sqrt_sum_squares [simp]:
-     "(( *f* sqrt)(x*x + y*y) \<in> HFinite) = (x*x + y*y \<in> HFinite)"
-apply (rule HFinite_hypreal_sqrt_iff)
-apply (rule add_nonneg_nonneg)
-apply (auto)
-done
+  "0 \<le> x \<Longrightarrow> (( *f* sqrt) x \<in> HFinite) = (x \<in> HFinite)"
+  by (blast intro: star_sqrt_HFinite HFinite_hypreal_sqrt_imp_HFinite)
 
 lemma Infinitesimal_hypreal_sqrt:
-     "[| 0 \<le> x; x \<in> Infinitesimal |] ==> ( *f* sqrt) x \<in> Infinitesimal"
-apply (auto simp add: order_le_less)
-apply (rule Infinitesimal_square_iff [THEN iffD2])
-apply (drule hypreal_sqrt_gt_zero_pow2)
-apply (simp add: numeral_2_eq_2)
-done
+     "\<lbrakk>0 \<le> x; x \<in> Infinitesimal\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> Infinitesimal"
+  by (simp add: mem_infmal_iff)
 
 lemma Infinitesimal_hypreal_sqrt_imp_Infinitesimal:
-     "[| 0 \<le> x; ( *f* sqrt) x \<in> Infinitesimal |] ==> x \<in> Infinitesimal"
-apply (auto simp add: order_le_less)
-apply (drule Infinitesimal_square_iff [THEN iffD1])
-apply (drule hypreal_sqrt_gt_zero_pow2)
-apply (simp add: numeral_2_eq_2 del: Infinitesimal_square_iff [symmetric])
-done
+     "\<lbrakk>0 \<le> x; ( *f* sqrt) x \<in> Infinitesimal\<rbrakk> \<Longrightarrow> x \<in> Infinitesimal"
+  using hypreal_sqrt_approx_zero2 mem_infmal_iff by blast
 
 lemma Infinitesimal_hypreal_sqrt_iff [simp]:
-     "0 \<le> x ==> (( *f* sqrt) x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
+     "0 \<le> x \<Longrightarrow> (( *f* sqrt) x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
 by (blast intro: Infinitesimal_hypreal_sqrt_imp_Infinitesimal Infinitesimal_hypreal_sqrt)
 
-lemma Infinitesimal_sqrt_sum_squares [simp]:
-     "(( *f* sqrt)(x*x + y*y) \<in> Infinitesimal) = (x*x + y*y \<in> Infinitesimal)"
-apply (rule Infinitesimal_hypreal_sqrt_iff)
-apply (rule add_nonneg_nonneg)
-apply (auto)
-done
-
 lemma HInfinite_hypreal_sqrt:
-     "[| 0 \<le> x; x \<in> HInfinite |] ==> ( *f* sqrt) x \<in> HInfinite"
-apply (auto simp add: order_le_less)
-apply (rule HInfinite_square_iff [THEN iffD1])
-apply (drule hypreal_sqrt_gt_zero_pow2)
-apply (simp add: numeral_2_eq_2)
-done
+     "\<lbrakk>0 \<le> x; x \<in> HInfinite\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HInfinite"
+  by (simp add: HInfinite_HFinite_iff)
 
 lemma HInfinite_hypreal_sqrt_imp_HInfinite:
-     "[| 0 \<le> x; ( *f* sqrt) x \<in> HInfinite |] ==> x \<in> HInfinite"
-apply (auto simp add: order_le_less)
-apply (drule HInfinite_square_iff [THEN iffD2])
-apply (drule hypreal_sqrt_gt_zero_pow2)
-apply (simp add: numeral_2_eq_2 del: HInfinite_square_iff)
-done
+     "\<lbrakk>0 \<le> x; ( *f* sqrt) x \<in> HInfinite\<rbrakk> \<Longrightarrow> x \<in> HInfinite"
+  using HFinite_hypreal_sqrt_iff HInfinite_HFinite_iff by blast
 
 lemma HInfinite_hypreal_sqrt_iff [simp]:
-     "0 \<le> x ==> (( *f* sqrt) x \<in> HInfinite) = (x \<in> HInfinite)"
+     "0 \<le> x \<Longrightarrow> (( *f* sqrt) x \<in> HInfinite) = (x \<in> HInfinite)"
 by (blast intro: HInfinite_hypreal_sqrt HInfinite_hypreal_sqrt_imp_HInfinite)
 
-lemma HInfinite_sqrt_sum_squares [simp]:
-     "(( *f* sqrt)(x*x + y*y) \<in> HInfinite) = (x*x + y*y \<in> HInfinite)"
-apply (rule HInfinite_hypreal_sqrt_iff)
-apply (rule add_nonneg_nonneg)
-apply (auto)
-done
-
 lemma HFinite_exp [simp]:
-     "sumhr (0, whn, %n. inverse (fact n) * x ^ n) \<in> HFinite"
-unfolding sumhr_app
-apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
-apply (rule NSBseqD2)
-apply (rule NSconvergent_NSBseq)
-apply (rule convergent_NSconvergent_iff [THEN iffD1])
-apply (rule summable_iff_convergent [THEN iffD1])
-apply (rule summable_exp)
-done
+  "sumhr (0, whn, \<lambda>n. inverse (fact n) * x ^ n) \<in> HFinite"
+  unfolding sumhr_app star_zero_def starfun2_star_of atLeast0LessThan
+  by (metis NSBseqD2 NSconvergent_NSBseq convergent_NSconvergent_iff summable_iff_convergent summable_exp)
 
 lemma exphr_zero [simp]: "exphr 0 = 1"
-apply (simp add: exphr_def sumhr_split_add [OF hypnat_one_less_hypnat_omega, symmetric])
-apply (rule st_unique, simp)
-apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
-apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
-apply (rule_tac x="whn" in spec)
-apply (unfold sumhr_app, transfer, simp add: power_0_left)
-done
+proof -
+  have "\<forall>x>1. 1 = sumhr (0, 1, \<lambda>n. inverse (fact n) * 0 ^ n) + sumhr (1, x, \<lambda>n. inverse (fact n) * 0 ^ n)"
+    unfolding sumhr_app by transfer (simp add: power_0_left)
+  then have "sumhr (0, 1, \<lambda>n. inverse (fact n) * 0 ^ n) + sumhr (1, whn, \<lambda>n. inverse (fact n) * 0 ^ n) \<approx> 1"
+    by auto
+  then show ?thesis
+    unfolding exphr_def
+    using sumhr_split_add [OF hypnat_one_less_hypnat_omega] st_unique by auto
+qed
 
 lemma coshr_zero [simp]: "coshr 0 = 1"
 apply (simp add: coshr_def sumhr_split_add
@@ -247,7 +179,7 @@
 apply (transfer, simp)
 done
 
-lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) (x::hypreal) \<approx> 1"
+lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal \<Longrightarrow> ( *f* exp) (x::hypreal) \<approx> 1"
 apply (case_tac "x = 0")
 apply (cut_tac [2] x = 0 in DERIV_exp)
 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
@@ -279,64 +211,64 @@
 apply (rule HNatInfinite_whn)
 done
 
-lemma starfun_exp_ge_add_one_self [simp]: "!!x::hypreal. 0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
+lemma starfun_exp_ge_add_one_self [simp]: "\<And>x::hypreal. 0 \<le> x \<Longrightarrow> (1 + x) \<le> ( *f* exp) x"
 by transfer (rule exp_ge_add_one_self_aux)
 
 (* exp (oo) is infinite *)
 lemma starfun_exp_HInfinite:
-     "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) (x::hypreal) \<in> HInfinite"
+     "\<lbrakk>x \<in> HInfinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* exp) (x::hypreal) \<in> HInfinite"
 apply (frule starfun_exp_ge_add_one_self)
 apply (rule HInfinite_ge_HInfinite, assumption)
 apply (rule order_trans [of _ "1+x"], auto) 
 done
 
 lemma starfun_exp_minus:
-  "!!x::'a:: {banach,real_normed_field} star. ( *f* exp) (-x) = inverse(( *f* exp) x)"
+  "\<And>x::'a:: {banach,real_normed_field} star. ( *f* exp) (-x) = inverse(( *f* exp) x)"
 by transfer (rule exp_minus)
 
 (* exp (-oo) is infinitesimal *)
 lemma starfun_exp_Infinitesimal:
-     "[| x \<in> HInfinite; x \<le> 0 |] ==> ( *f* exp) (x::hypreal) \<in> Infinitesimal"
+     "\<lbrakk>x \<in> HInfinite; x \<le> 0\<rbrakk> \<Longrightarrow> ( *f* exp) (x::hypreal) \<in> Infinitesimal"
 apply (subgoal_tac "\<exists>y. x = - y")
 apply (rule_tac [2] x = "- x" in exI)
 apply (auto intro!: HInfinite_inverse_Infinitesimal starfun_exp_HInfinite
             simp add: starfun_exp_minus HInfinite_minus_iff)
 done
 
-lemma starfun_exp_gt_one [simp]: "!!x::hypreal. 0 < x ==> 1 < ( *f* exp) x"
+lemma starfun_exp_gt_one [simp]: "\<And>x::hypreal. 0 < x \<Longrightarrow> 1 < ( *f* exp) x"
 by transfer (rule exp_gt_one)
 
 abbreviation real_ln :: "real \<Rightarrow> real" where 
   "real_ln \<equiv> ln"
 
-lemma starfun_ln_exp [simp]: "!!x. ( *f* real_ln) (( *f* exp) x) = x"
+lemma starfun_ln_exp [simp]: "\<And>x. ( *f* real_ln) (( *f* exp) x) = x"
 by transfer (rule ln_exp)
 
-lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* real_ln) x) = x) = (0 < x)"
+lemma starfun_exp_ln_iff [simp]: "\<And>x. (( *f* exp)(( *f* real_ln) x) = x) = (0 < x)"
 by transfer (rule exp_ln_iff)
 
-lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* real_ln) x = u"
+lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x \<Longrightarrow> ( *f* real_ln) x = u"
 by transfer (rule ln_unique)
 
-lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* real_ln) x < x"
+lemma starfun_ln_less_self [simp]: "\<And>x. 0 < x \<Longrightarrow> ( *f* real_ln) x < x"
 by transfer (rule ln_less_self)
 
-lemma starfun_ln_ge_zero [simp]: "!!x. 1 \<le> x ==> 0 \<le> ( *f* real_ln) x"
+lemma starfun_ln_ge_zero [simp]: "\<And>x. 1 \<le> x \<Longrightarrow> 0 \<le> ( *f* real_ln) x"
 by transfer (rule ln_ge_zero)
 
-lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* real_ln) x"
+lemma starfun_ln_gt_zero [simp]: "\<And>x .1 < x \<Longrightarrow> 0 < ( *f* real_ln) x"
 by transfer (rule ln_gt_zero)
 
-lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \<noteq> 1 |] ==> ( *f* real_ln) x \<noteq> 0"
+lemma starfun_ln_not_eq_zero [simp]: "\<And>x. \<lbrakk>0 < x; x \<noteq> 1\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<noteq> 0"
 by transfer simp
 
-lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* real_ln) x \<in> HFinite"
+lemma starfun_ln_HFinite: "\<lbrakk>x \<in> HFinite; 1 \<le> x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HFinite"
 apply (rule HFinite_bounded)
 apply assumption 
 apply (simp_all add: starfun_ln_less_self order_less_imp_le)
 done
 
-lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* real_ln) (inverse x) = -( *f* ln) x"
+lemma starfun_ln_inverse: "\<And>x. 0 < x \<Longrightarrow> ( *f* real_ln) (inverse x) = -( *f* ln) x"
 by transfer (rule ln_inverse)
 
 lemma starfun_abs_exp_cancel: "\<And>x. \<bar>( *f* exp) (x::hypreal)\<bar> = ( *f* exp) x"
@@ -345,7 +277,7 @@
 lemma starfun_exp_less_mono: "\<And>x y::hypreal. x < y \<Longrightarrow> ( *f* exp) x < ( *f* exp) y"
 by transfer (rule exp_less_mono)
 
-lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) (x::hypreal) \<in> HFinite"
+lemma starfun_exp_HFinite: "x \<in> HFinite \<Longrightarrow> ( *f* exp) (x::hypreal) \<in> HFinite"
 apply (auto simp add: HFinite_def, rename_tac u)
 apply (rule_tac x="( *f* exp) u" in rev_bexI)
 apply (simp add: Reals_eq_Standard)
@@ -354,7 +286,7 @@
 done
 
 lemma starfun_exp_add_HFinite_Infinitesimal_approx:
-     "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x::hypreal) \<approx> ( *f* exp) z"
+     "\<lbrakk>x \<in> Infinitesimal; z \<in> HFinite\<rbrakk> \<Longrightarrow> ( *f* exp) (z + x::hypreal) \<approx> ( *f* exp) z"
 apply (simp add: STAR_exp_add)
 apply (frule STAR_exp_Infinitesimal)
 apply (drule approx_mult2)
@@ -363,7 +295,7 @@
 
 (* using previous result to get to result *)
 lemma starfun_ln_HInfinite:
-     "[| x \<in> HInfinite; 0 < x |] ==> ( *f* real_ln) x \<in> HInfinite"
+     "\<lbrakk>x \<in> HInfinite; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HInfinite"
 apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
 apply (drule starfun_exp_HFinite)
 apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff)
@@ -377,7 +309,7 @@
 
 (* check out this proof!!! *)
 lemma starfun_ln_HFinite_not_Infinitesimal:
-     "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* real_ln) x \<in> HFinite"
+     "\<lbrakk>x \<in> HFinite - Infinitesimal; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HFinite"
 apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2])
 apply (drule starfun_exp_HInfinite_Infinitesimal_disj)
 apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff
@@ -386,30 +318,30 @@
 
 (* we do proof by considering ln of 1/x *)
 lemma starfun_ln_Infinitesimal_HInfinite:
-     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* real_ln) x \<in> HInfinite"
+     "\<lbrakk>x \<in> Infinitesimal; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x \<in> HInfinite"
 apply (drule Infinitesimal_inverse_HInfinite)
 apply (frule positive_imp_inverse_positive)
 apply (drule_tac [2] starfun_ln_HInfinite)
 apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff)
 done
 
-lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* real_ln) x < 0"
+lemma starfun_ln_less_zero: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> ( *f* real_ln) x < 0"
 by transfer (rule ln_less_zero)
 
 lemma starfun_ln_Infinitesimal_less_zero:
-     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* real_ln) x < 0"
+     "\<lbrakk>x \<in> Infinitesimal; 0 < x\<rbrakk> \<Longrightarrow> ( *f* real_ln) x < 0"
 by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
 
 lemma starfun_ln_HInfinite_gt_zero:
-     "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* real_ln) x"
+     "\<lbrakk>x \<in> HInfinite; 0 < x\<rbrakk> \<Longrightarrow> 0 < ( *f* real_ln) x"
 by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
 
 
 (*
-Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S ln x"
+Goalw [NSLIM_def] "(\<lambda>h. ((x powr h) - 1) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S ln x"
 *)
 
-lemma HFinite_sin [simp]: "sumhr (0, whn, %n. sin_coeff n * x ^ n) \<in> HFinite"
+lemma HFinite_sin [simp]: "sumhr (0, whn, \<lambda>n. sin_coeff n * x ^ n) \<in> HFinite"
 unfolding sumhr_app
 apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
 apply (rule NSBseqD2)
@@ -425,7 +357,7 @@
 
 lemma STAR_sin_Infinitesimal [simp]:
   fixes x :: "'a::{real_normed_field,banach} star"
-  shows "x \<in> Infinitesimal ==> ( *f* sin) x \<approx> x"
+  shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* sin) x \<approx> x"
 apply (case_tac "x = 0")
 apply (cut_tac [2] x = 0 in DERIV_sin)
 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
@@ -435,7 +367,7 @@
            simp add: mult.assoc)
 done
 
-lemma HFinite_cos [simp]: "sumhr (0, whn, %n. cos_coeff n * x ^ n) \<in> HFinite"
+lemma HFinite_cos [simp]: "sumhr (0, whn, \<lambda>n. cos_coeff n * x ^ n) \<in> HFinite"
 unfolding sumhr_app
 apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
 apply (rule NSBseqD2)
@@ -451,7 +383,7 @@
 
 lemma STAR_cos_Infinitesimal [simp]:
   fixes x :: "'a::{real_normed_field,banach} star"
-  shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1"
+  shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* cos) x \<approx> 1"
 apply (case_tac "x = 0")
 apply (cut_tac [2] x = 0 in DERIV_cos)
 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
@@ -467,7 +399,7 @@
 lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
 by transfer (rule tan_zero)
 
-lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x \<approx> x"
+lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal \<Longrightarrow> ( *f* tan) x \<approx> x"
 apply (case_tac "x = 0")
 apply (cut_tac [2] x = 0 in DERIV_tan)
 apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
@@ -479,7 +411,7 @@
 
 lemma STAR_sin_cos_Infinitesimal_mult:
   fixes x :: "'a::{real_normed_field,banach} star"
-  shows "x \<in> Infinitesimal ==> ( *f* sin) x * ( *f* cos) x \<approx> x"
+  shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* sin) x * ( *f* cos) x \<approx> x"
 using approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1] 
 by (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
 
@@ -490,13 +422,13 @@
 
 lemma lemma_split_hypreal_of_real:
      "N \<in> HNatInfinite  
-      ==> hypreal_of_real a =  
+      \<Longrightarrow> hypreal_of_real a =  
           hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)"
 by (simp add: mult.assoc [symmetric] zero_less_HNatInfinite)
 
 lemma STAR_sin_Infinitesimal_divide:
   fixes x :: "'a::{real_normed_field,banach} star"
-  shows "[|x \<in> Infinitesimal; x \<noteq> 0 |] ==> ( *f* sin) x/x \<approx> 1"
+  shows "\<lbrakk>x \<in> Infinitesimal; x \<noteq> 0\<rbrakk> \<Longrightarrow> ( *f* sin) x/x \<approx> 1"
 using DERIV_sin [of "0::'a"]
 by (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
 
@@ -506,32 +438,32 @@
 
 lemma lemma_sin_pi:
      "n \<in> HNatInfinite  
-      ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) \<approx> 1"
+      \<Longrightarrow> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) \<approx> 1"
 apply (rule STAR_sin_Infinitesimal_divide)
 apply (auto simp add: zero_less_HNatInfinite)
 done
 
 lemma STAR_sin_inverse_HNatInfinite:
      "n \<in> HNatInfinite  
-      ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n \<approx> 1"
+      \<Longrightarrow> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n \<approx> 1"
 apply (frule lemma_sin_pi)
 apply (simp add: divide_inverse)
 done
 
 lemma Infinitesimal_pi_divide_HNatInfinite: 
      "N \<in> HNatInfinite  
-      ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
+      \<Longrightarrow> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
 apply (simp add: divide_inverse)
 apply (auto intro: Infinitesimal_HFinite_mult2)
 done
 
 lemma pi_divide_HNatInfinite_not_zero [simp]:
-     "N \<in> HNatInfinite ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0"
+     "N \<in> HNatInfinite \<Longrightarrow> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0"
 by (simp add: zero_less_HNatInfinite)
 
 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi:
      "n \<in> HNatInfinite  
-      ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n  
+      \<Longrightarrow> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n  
           \<approx> hypreal_of_real pi"
 apply (frule STAR_sin_Infinitesimal_divide
                [OF Infinitesimal_pi_divide_HNatInfinite 
@@ -543,7 +475,7 @@
 
 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
      "n \<in> HNatInfinite  
-      ==> hypreal_of_hypnat n *  
+      \<Longrightarrow> hypreal_of_hypnat n *  
           ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n))  
           \<approx> hypreal_of_real pi"
 apply (rule mult.commute [THEN subst])
@@ -551,14 +483,14 @@
 done
 
 lemma starfunNat_pi_divide_n_Infinitesimal: 
-     "N \<in> HNatInfinite ==> ( *f* (%x. pi / real x)) N \<in> Infinitesimal"
+     "N \<in> HNatInfinite \<Longrightarrow> ( *f* (\<lambda>x. pi / real x)) N \<in> Infinitesimal"
 by (auto intro!: Infinitesimal_HFinite_mult2 
          simp add: starfun_mult [symmetric] divide_inverse
                    starfun_inverse [symmetric] starfunNat_real_of_nat)
 
 lemma STAR_sin_pi_divide_n_approx:
-     "N \<in> HNatInfinite ==>  
-      ( *f* sin) (( *f* (%x. pi / real x)) N) \<approx>  
+     "N \<in> HNatInfinite \<Longrightarrow>  
+      ( *f* sin) (( *f* (\<lambda>x. pi / real x)) N) \<approx>  
       hypreal_of_real pi/(hypreal_of_hypnat N)"
 apply (simp add: starfunNat_real_of_nat [symmetric])
 apply (rule STAR_sin_Infinitesimal)
@@ -569,7 +501,7 @@
 apply simp
 done
 
-lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
+lemma NSLIMSEQ_sin_pi: "(\<lambda>n. real n * sin (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
 apply (auto simp add: NSLIMSEQ_def starfun_mult [symmetric] starfunNat_real_of_nat)
 apply (rule_tac f1 = sin in starfun_o2 [THEN subst])
 apply (auto simp add: starfun_mult [symmetric] starfunNat_real_of_nat divide_inverse)
@@ -578,7 +510,7 @@
             simp add: starfunNat_real_of_nat mult.commute divide_inverse)
 done
 
-lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))\<longlonglongrightarrow>\<^sub>N\<^sub>S 1"
+lemma NSLIMSEQ_cos_one: "(\<lambda>n. cos (pi / real n))\<longlonglongrightarrow>\<^sub>N\<^sub>S 1"
 apply (simp add: NSLIMSEQ_def, auto)
 apply (rule_tac f1 = cos in starfun_o2 [THEN subst])
 apply (rule STAR_cos_Infinitesimal)
@@ -588,7 +520,7 @@
 done
 
 lemma NSLIMSEQ_sin_cos_pi:
-     "(%n. real n * sin (pi / real n) * cos (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
+     "(\<lambda>n. real n * sin (pi / real n) * cos (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
 by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
 
 
@@ -596,7 +528,7 @@
 
 lemma STAR_cos_Infinitesimal_approx:
   fixes x :: "'a::{real_normed_field,banach} star"
-  shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1 - x\<^sup>2"
+  shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* cos) x \<approx> 1 - x\<^sup>2"
 apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
 apply (auto simp add: Infinitesimal_approx_minus [symmetric] 
             add.assoc [symmetric] numeral_2_eq_2)
@@ -604,7 +536,7 @@
 
 lemma STAR_cos_Infinitesimal_approx2:
   fixes x :: hypreal  \<comment> \<open>perhaps could be generalised, like many other hypreal results\<close>
-  shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1 - (x\<^sup>2)/2"
+  shows "x \<in> Infinitesimal \<Longrightarrow> ( *f* cos) x \<approx> 1 - (x\<^sup>2)/2"
 apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
 apply (auto intro: Infinitesimal_SReal_divide Infinitesimal_mult
             simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)