New material on integration, etc. Moving Hyperreal/ex
to directory Complex
(* Title : HTranscendental.ML
Author : Jacques D. Fleuriot
Copyright : 2001 University of Edinburgh
Description : Nonstandard extensions of transcendental functions
*)
(*-------------------------------------------------------------------------*)
(* NS extension of square root function *)
(*-------------------------------------------------------------------------*)
Goal "( *f* sqrt) 0 = 0";
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_zero_num]));
qed "STAR_sqrt_zero";
Addsimps [STAR_sqrt_zero];
Goal "( *f* sqrt) 1 = 1";
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_one_num]));
qed "STAR_sqrt_one";
Addsimps [STAR_sqrt_one];
Goal "(( *f* sqrt)(x) ^ 2 = x) = (0 <= x)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_le,
hypreal_zero_num, starfun,hrealpow,real_sqrt_pow2_iff]
delsimps [hpowr_Suc,realpow_Suc]));
qed "hypreal_sqrt_pow2_iff";
Goal "0 < x ==> ( *f* sqrt) (x) ^ 2 = x";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset() addIs [FreeUltrafilterNat_subset,
real_sqrt_gt_zero_pow2],simpset() addsimps
[hypreal_less,starfun,hrealpow,hypreal_zero_num]
delsimps [hpowr_Suc,realpow_Suc]));
qed "hypreal_sqrt_gt_zero_pow2";
Goal "0 < x ==> 0 < ( *f* sqrt) (x) ^ 2";
by (forward_tac [hypreal_sqrt_gt_zero_pow2] 1);
by (Auto_tac);
qed "hypreal_sqrt_pow2_gt_zero";
Goal "0 < x ==> ( *f* sqrt) (x) ~= 0";
by (forward_tac [hypreal_sqrt_pow2_gt_zero] 1);
by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc]));
qed "hypreal_sqrt_not_zero";
Goal "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x";
by (forward_tac [hypreal_sqrt_not_zero] 1);
by (dres_inst_tac [("n1","2"),("r1","( *f* sqrt) x")] (hrealpow_inverse RS sym) 1);
by (auto_tac (claset() addDs [hypreal_sqrt_gt_zero_pow2],simpset()));
qed "hypreal_inverse_sqrt_pow2";
Goalw [hypreal_zero_def]
"[|0 < x; 0 <y |] ==> \
\ ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,
hypreal_mult,hypreal_less,hypreal_zero_num]));
by (ultra_tac (claset() addIs [real_sqrt_mult_distrib],simpset()) 1);
qed "hypreal_sqrt_mult_distrib";
Goal "[|0<=x; 0<=y |] ==> \
\ ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)";
by (auto_tac (claset() addIs [hypreal_sqrt_mult_distrib],
simpset() addsimps [hypreal_le_eq_less_or_eq]));
qed "hypreal_sqrt_mult_distrib2";
Goal "0 < x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)";
by (auto_tac (claset(),simpset() addsimps [mem_infmal_iff RS sym]));
by (rtac (hypreal_sqrt_gt_zero_pow2 RS subst) 1);
by (auto_tac (claset() addIs [Infinitesimal_mult]
addSDs [(hypreal_sqrt_gt_zero_pow2 RS ssubst)],simpset() addsimps [two_eq_Suc_Suc]));
qed "hypreal_sqrt_approx_zero";
Addsimps [hypreal_sqrt_approx_zero];
Goal "0 <= x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)";
by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq],
simpset()));
qed "hypreal_sqrt_approx_zero2";
Addsimps [hypreal_sqrt_approx_zero2];
Goal "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)";
by (rtac hypreal_sqrt_approx_zero2 1);
by (REPEAT(rtac hypreal_le_add_order 1));
by Auto_tac;
qed "hypreal_sqrt_sum_squares";
Addsimps [hypreal_sqrt_sum_squares];
Goal "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)";
by (rtac hypreal_sqrt_approx_zero2 1);
by (rtac hypreal_le_add_order 1);
by Auto_tac;
qed "hypreal_sqrt_sum_squares2";
Addsimps [hypreal_sqrt_sum_squares2];
Goal "0 < x ==> 0 < ( *f* sqrt)(x)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps
[starfun,hypreal_zero_def,hypreal_less,hypreal_zero_num]));
by (ultra_tac (claset() addIs [real_sqrt_gt_zero], simpset()) 1);
qed "hypreal_sqrt_gt_zero";
Goal "0 <= x ==> 0 <= ( *f* sqrt)(x)";
by (auto_tac (claset() addIs [hypreal_sqrt_gt_zero],
simpset() addsimps [hypreal_le_eq_less_or_eq ]));
qed "hypreal_sqrt_ge_zero";
Goal "( *f* sqrt)(x ^ 2) = abs(x)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,
hypreal_hrabs,hypreal_mult,two_eq_Suc_Suc]));
qed "hypreal_sqrt_hrabs";
Addsimps [hypreal_sqrt_hrabs];
Goal "( *f* sqrt)(x*x) = abs(x)";
by (rtac (hrealpow_two RS subst) 1);
by (rtac (two_eq_Suc_Suc RS subst) 1);
by (rtac hypreal_sqrt_hrabs 1);
qed "hypreal_sqrt_hrabs2";
Addsimps [hypreal_sqrt_hrabs2];
Goal "( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,
hypreal_hrabs,hypnat_of_nat_def,hyperpow]));
qed "hypreal_sqrt_hyperpow_hrabs";
Addsimps [hypreal_sqrt_hyperpow_hrabs];
Goal "[| x: HFinite; 0 <= x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)";
by (res_inst_tac [("n","1")] hrealpow_Suc_cancel_eq 1);
by (auto_tac (claset() addSIs [st_zero_le,hypreal_sqrt_ge_zero],simpset()));
by (rtac (st_mult RS subst) 2);
by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 4);
by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 6);
by (auto_tac (claset(), simpset() addsimps [st_hrabs,st_zero_le]));
by (ALLGOALS(rtac (HFinite_square_iff RS iffD1)));
by (auto_tac (claset(),simpset() addsimps
[hypreal_sqrt_mult_distrib2 RS sym]
delsimps [HFinite_square_iff]));
qed "st_hypreal_sqrt";
Goal "x <= ( *f* sqrt)(x ^ 2 + y ^ 2)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_add,
hrealpow,hypreal_le] delsimps [hpowr_Suc,realpow_Suc]));
qed "hypreal_sqrt_sum_squares_ge1";
Addsimps [hypreal_sqrt_sum_squares_ge1];
Goal "[| 0 <= x; x : HFinite |] ==> ( *f* sqrt) x : HFinite";
by (auto_tac (claset(),simpset() addsimps [hypreal_le_eq_less_or_eq]));
by (rtac (HFinite_square_iff RS iffD1) 1);
by (dtac hypreal_sqrt_gt_zero_pow2 1);
by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc]));
qed "HFinite_hypreal_sqrt";
Goal "[| 0 <= x; ( *f* sqrt) x : HFinite |] ==> x : HFinite";
by (auto_tac (claset(),simpset() addsimps [hypreal_le_eq_less_or_eq]));
by (dtac (HFinite_square_iff RS iffD2) 1);
by (dtac hypreal_sqrt_gt_zero_pow2 1);
by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc] delsimps [HFinite_square_iff]));
qed "HFinite_hypreal_sqrt_imp_HFinite";
Goal "0 <= x ==> (( *f* sqrt) x : HFinite) = (x : HFinite)";
by (blast_tac (claset() addIs [HFinite_hypreal_sqrt,
HFinite_hypreal_sqrt_imp_HFinite]) 1);
qed "HFinite_hypreal_sqrt_iff";
Addsimps [HFinite_hypreal_sqrt_iff];
Goal "(( *f* sqrt)(x*x + y*y) : HFinite) = (x*x + y*y : HFinite)";
by (rtac HFinite_hypreal_sqrt_iff 1);
by (rtac hypreal_le_add_order 1);
by Auto_tac;
qed "HFinite_sqrt_sum_squares";
Addsimps [HFinite_sqrt_sum_squares];
Goal "[| 0 <= x; x : Infinitesimal |] ==> ( *f* sqrt) x : Infinitesimal";
by (auto_tac (claset(),simpset() addsimps [hypreal_le_eq_less_or_eq]));
by (rtac (Infinitesimal_square_iff RS iffD2) 1);
by (dtac hypreal_sqrt_gt_zero_pow2 1);
by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc]));
qed "Infinitesimal_hypreal_sqrt";
Goal "[| 0 <= x; ( *f* sqrt) x : Infinitesimal |] ==> x : Infinitesimal";
by (auto_tac (claset(),simpset() addsimps [hypreal_le_eq_less_or_eq]));
by (dtac (Infinitesimal_square_iff RS iffD1) 1);
by (dtac hypreal_sqrt_gt_zero_pow2 1);
by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc]
delsimps [Infinitesimal_square_iff RS sym]));
qed "Infinitesimal_hypreal_sqrt_imp_Infinitesimal";
Goal "0 <= x ==> (( *f* sqrt) x : Infinitesimal) = (x : Infinitesimal)";
by (blast_tac (claset() addIs [Infinitesimal_hypreal_sqrt_imp_Infinitesimal,
Infinitesimal_hypreal_sqrt]) 1);
qed "Infinitesimal_hypreal_sqrt_iff";
Addsimps [Infinitesimal_hypreal_sqrt_iff];
Goal "(( *f* sqrt)(x*x + y*y) : Infinitesimal) = (x*x + y*y : Infinitesimal)";
by (rtac Infinitesimal_hypreal_sqrt_iff 1);
by (rtac hypreal_le_add_order 1);
by Auto_tac;
qed "Infinitesimal_sqrt_sum_squares";
Addsimps [Infinitesimal_sqrt_sum_squares];
Goal "[| 0 <= x; x : HInfinite |] ==> ( *f* sqrt) x : HInfinite";
by (auto_tac (claset(),simpset() addsimps [hypreal_le_eq_less_or_eq]));
by (rtac (HInfinite_square_iff RS iffD1) 1);
by (dtac hypreal_sqrt_gt_zero_pow2 1);
by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc]));
qed "HInfinite_hypreal_sqrt";
Goal "[| 0 <= x; ( *f* sqrt) x : HInfinite |] ==> x : HInfinite";
by (auto_tac (claset(),simpset() addsimps [hypreal_le_eq_less_or_eq]));
by (dtac (HInfinite_square_iff RS iffD2) 1);
by (dtac hypreal_sqrt_gt_zero_pow2 1);
by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc]
delsimps [HInfinite_square_iff]));
qed "HInfinite_hypreal_sqrt_imp_HInfinite";
Goal "0 <= x ==> (( *f* sqrt) x : HInfinite) = (x : HInfinite)";
by (blast_tac (claset() addIs [HInfinite_hypreal_sqrt,
HInfinite_hypreal_sqrt_imp_HInfinite]) 1);
qed "HInfinite_hypreal_sqrt_iff";
Addsimps [HInfinite_hypreal_sqrt_iff];
Goal "(( *f* sqrt)(x*x + y*y) : HInfinite) = (x*x + y*y : HInfinite)";
by (rtac HInfinite_hypreal_sqrt_iff 1);
by (rtac hypreal_le_add_order 1);
by Auto_tac;
qed "HInfinite_sqrt_sum_squares";
Addsimps [HInfinite_sqrt_sum_squares];
Goal "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) : HFinite";
by (auto_tac (claset() addSIs [NSBseq_HFinite_hypreal,NSconvergent_NSBseq],
simpset() addsimps [starfunNat_sumr RS sym,starfunNat,hypnat_omega_def,
convergent_NSconvergent_iff RS sym, summable_convergent_sumr_iff RS sym,
summable_exp]));
qed "HFinite_exp";
Addsimps [HFinite_exp];
Goalw [exphr_def] "exphr 0 = 1";
by (res_inst_tac [("n1","1")] (sumhr_split_add RS subst) 1);
by (res_inst_tac [("t","1")] (hypnat_add_zero_left RS subst) 2);
by (rtac hypnat_one_less_hypnat_omega 1);
by (auto_tac (claset(),simpset() addsimps [sumhr,hypnat_zero_def,starfunNat,
hypnat_one_def,hypnat_add,hypnat_omega_def,hypreal_add]
delsimps [hypnat_add_zero_left]));
by (simp_tac (simpset() addsimps [hypreal_one_num RS sym]) 1);
qed "exphr_zero";
Addsimps [exphr_zero];
Goalw [coshr_def] "coshr 0 = 1";
by (res_inst_tac [("n1","1")] (sumhr_split_add RS subst) 1);
by (res_inst_tac [("t","1")] (hypnat_add_zero_left RS subst) 2);
by (rtac hypnat_one_less_hypnat_omega 1);
by (auto_tac (claset(),simpset() addsimps [sumhr,hypnat_zero_def,starfunNat,
hypnat_one_def,hypnat_add,hypnat_omega_def,st_add RS sym,
(hypreal_one_def RS meta_eq_to_obj_eq) RS sym,
(hypreal_zero_def RS meta_eq_to_obj_eq) RS sym] delsimps [hypnat_add_zero_left]));
qed "coshr_zero";
Addsimps [coshr_zero];
Goalw [hypreal_zero_def,hypreal_one_def] "( *f* exp) 0 @= 1";
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_one_num]));
qed "STAR_exp_zero_approx_one";
Addsimps [STAR_exp_zero_approx_one];
Goal "x: Infinitesimal ==> ( *f* exp) x @= 1";
by (case_tac "x = 0" 1);
by (cut_inst_tac [("x","0")] DERIV_exp 2);
by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym,
nsderiv_def]));
by (dres_inst_tac [("x","x")] bspec 1);
by Auto_tac;
by (dres_inst_tac [("c","x")] approx_mult1 1);
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
simpset() addsimps [hypreal_mult_assoc]));
by (res_inst_tac [("d","-1")] approx_add_right_cancel 1);
by (rtac (approx_sym RSN (2,approx_trans2)) 1);
by (auto_tac (claset(),simpset() addsimps [mem_infmal_iff]));
qed "STAR_exp_Infinitesimal";
Goal "( *f* exp) epsilon @= 1";
by (auto_tac (claset() addIs [STAR_exp_Infinitesimal],simpset()));
qed "STAR_exp_epsilon";
Addsimps [STAR_exp_epsilon];
Goal "( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_add,
hypreal_mult,exp_add]));
qed "STAR_exp_add";
Goalw [exphr_def] "exphr x = hypreal_of_real (exp x)";
by (rtac (st_hypreal_of_real RS subst) 1);
by (rtac approx_st_eq 1);
by Auto_tac;
by (rtac (approx_minus_iff RS iffD2) 1);
by (auto_tac (claset(),simpset() addsimps [mem_infmal_iff RS sym,
hypreal_of_real_def,hypnat_zero_def,hypnat_omega_def,sumhr,
hypreal_minus,hypreal_add]));
by (rtac NSLIMSEQ_zero_Infinitesimal_hypreal 1);
by (cut_inst_tac [("x3","x")] (exp_converges RS ((sums_def RS
meta_eq_to_obj_eq) RS iffD1)) 1);
by (dres_inst_tac [("b","- exp x")] (LIMSEQ_const RSN (2,LIMSEQ_add)) 1);
by (auto_tac (claset(),simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]));
qed "exphr_hypreal_of_real_exp_eq";
Goal "0 <= x ==> (1 + x) <= ( *f* exp) x";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_add,
hypreal_le,hypreal_zero_num,hypreal_one_num]));
by (Ultra_tac 1);
qed "starfun_exp_ge_add_one_self";
Addsimps [starfun_exp_ge_add_one_self];
(* exp (oo) is infinite *)
Goal "[| x : HInfinite; 0 <= x |] ==> ( *f* exp) x : HInfinite";
by (ftac starfun_exp_ge_add_one_self 1);
by (rtac HInfinite_ge_HInfinite 1);
by (rtac hypreal_le_trans 2);
by (TRYALL(assume_tac) THEN Simp_tac 1);
qed "starfun_exp_HInfinite";
Goal "( *f* exp) (-x) = inverse(( *f* exp) x)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_inverse,
hypreal_minus,exp_minus]));
qed "starfun_exp_minus";
(* exp (-oo) is infinitesimal *)
Goal "[| x : HInfinite; x <= 0 |] ==> ( *f* exp) x : Infinitesimal";
by (subgoal_tac "EX y. x = - y" 1);
by (res_inst_tac [("x","- x")] exI 2);
by (auto_tac (claset() addSIs [HInfinite_inverse_Infinitesimal,
starfun_exp_HInfinite] addIs [(starfun_exp_minus RS ssubst)],
simpset() addsimps [HInfinite_minus_iff]));
qed "starfun_exp_Infinitesimal";
Goal "0 < x ==> 1 < ( *f* exp) x";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_one_num,
hypreal_zero_num,hypreal_less]));
by (Ultra_tac 1);
qed "starfun_exp_gt_one";
Addsimps [starfun_exp_gt_one];
(* needs derivative of inverse function
TRY a NS one today!!!
Goal "x @= 1 ==> ( *f* ln) x @= 1";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_one_def]));
Goalw [nsderiv_def] "0r < x ==> NSDERIV ln x :> inverse x";
*)
Goal "( *f* ln) (( *f* exp) x) = x";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun]));
qed "starfun_ln_exp";
Addsimps [starfun_ln_exp];
Goal "(( *f* exp)(( *f* ln) x) = x) = (0 < x)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,
hypreal_zero_num,hypreal_less]));
qed "starfun_exp_ln_iff";
Addsimps [starfun_exp_ln_iff];
Goal "( *f* exp) u = x ==> ( *f* ln) x = u";
by (auto_tac (claset(),simpset() addsimps [starfun]));
qed "starfun_exp_ln_eq";
Goal "0 < x ==> ( *f* ln) x < x";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,
hypreal_zero_num,hypreal_less]));
by (Ultra_tac 1);
qed "starfun_ln_less_self";
Addsimps [starfun_ln_less_self];
Goal "1 <= x ==> 0 <= ( *f* ln) x";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,
hypreal_zero_num,hypreal_le,hypreal_one_num]));
by (Ultra_tac 1);
qed "starfun_ln_ge_zero";
Addsimps [starfun_ln_ge_zero];
Goal "1 < x ==> 0 < ( *f* ln) x";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,
hypreal_zero_num,hypreal_less,hypreal_one_num]));
by (Ultra_tac 1);
qed "starfun_ln_gt_zero";
Addsimps [starfun_ln_gt_zero];
Goal "[| 0 < x; x ~= 1 |] ==> ( *f* ln) x ~= 0";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,
hypreal_zero_num,hypreal_less,hypreal_one_num]));
by (ultra_tac (claset() addIs [ccontr] addDs [ln_not_eq_zero],simpset()) 1);
qed "starfun_ln_not_eq_zero";
Addsimps [starfun_ln_not_eq_zero];
Goal "[| x: HFinite; 1 <= x |] ==> ( *f* ln) x : HFinite";
by (rtac HFinite_bounded 1);
by (rtac order_less_imp_le 2);
by (rtac starfun_ln_less_self 2);
by (rtac order_less_le_trans 2);
by Auto_tac;
qed "starfun_ln_HFinite";
Goal "0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,
hypreal_zero_num,hypreal_minus,hypreal_inverse,
hypreal_less]));
by (Ultra_tac 1);
by (auto_tac (claset(),simpset() addsimps [ln_inverse]));
qed "starfun_ln_inverse";
Goal "x : HFinite ==> ( *f* exp) x : HFinite";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun,
HFinite_FreeUltrafilterNat_iff]));
by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
by Auto_tac;
by (res_inst_tac [("x","exp u")] exI 1);
by (Ultra_tac 1 THEN arith_tac 1);
qed "starfun_exp_HFinite";
Goal "[|x: Infinitesimal; z: HFinite |] ==> ( *f* exp) (z + x) @= ( *f* exp) z";
by (simp_tac (simpset() addsimps [STAR_exp_add]) 1);
by (ftac STAR_exp_Infinitesimal 1);
by (dtac approx_mult2 1);
by (auto_tac (claset() addIs [starfun_exp_HFinite],simpset()));
qed "starfun_exp_add_HFinite_Infinitesimal_approx";
(* using previous result to get to result *)
Goal "[| x : HInfinite; 0 < x |] ==> ( *f* ln) x : HInfinite";
by (rtac ccontr 1 THEN dtac (HFinite_HInfinite_iff RS iffD2) 1);
by (dtac starfun_exp_HFinite 1);
by (auto_tac (claset(),simpset() addsimps [starfun_exp_ln_iff RS iffD2,
HFinite_HInfinite_iff]));
qed "starfun_ln_HInfinite";
Goal "x : HInfinite ==> ( *f* exp) x : HInfinite | ( *f* exp) x : Infinitesimal";
by (cut_inst_tac [("x","x")] (CLAIM "x <= (0::hypreal) | 0 <= x") 1);
by (auto_tac (claset() addIs [starfun_exp_HInfinite,starfun_exp_Infinitesimal],
simpset()));
qed "starfun_exp_HInfinite_Infinitesimal_disj";
(* check out this proof!!! *)
Goal "[| x : HFinite - Infinitesimal; 0 < x |] ==> ( *f* ln) x : HFinite";
by (rtac ccontr 1 THEN dtac (HInfinite_HFinite_iff RS iffD2) 1);
by (dtac starfun_exp_HInfinite_Infinitesimal_disj 1);
by (auto_tac (claset(),simpset() addsimps [starfun_exp_ln_iff RS sym,
HInfinite_HFinite_iff] delsimps [starfun_exp_ln_iff]));
qed "starfun_ln_HFinite_not_Infinitesimal";
(* we do proof by considering ln of 1/x *)
Goal "[| x : Infinitesimal; 0 < x |] ==> ( *f* ln) x : HInfinite";
by (dtac Infinitesimal_inverse_HInfinite 1);
by (ftac hypreal_inverse_gt_0 1);
by (dtac starfun_ln_HInfinite 2);
by (auto_tac (claset(),simpset() addsimps [starfun_ln_inverse,
HInfinite_minus_iff]));
qed "starfun_ln_Infinitesimal_HInfinite";
Goal "[| 0 < x; x < 1 |] ==> ( *f* ln) x < 0";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_zero_num,
hypreal_one_num,hypreal_less,starfun]));
by (ultra_tac (claset() addIs [ln_less_zero],simpset()) 1);
qed "starfun_ln_less_zero";
Goal "[| x : Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0";
by (auto_tac (claset() addSIs [starfun_ln_less_zero],simpset()
addsimps [Infinitesimal_def]));
by (dres_inst_tac [("x","1")] bspec 1);
by (auto_tac (claset(),simpset() addsimps [hrabs_def]));
qed "starfun_ln_Infinitesimal_less_zero";
Goal "[| x : HInfinite; 0 < x |] ==> 0 < ( *f* ln) x";
by (auto_tac (claset() addSIs [starfun_ln_gt_zero],simpset()
addsimps [HInfinite_def]));
by (dres_inst_tac [("x","1")] bspec 1);
by (auto_tac (claset(),simpset() addsimps [hrabs_def]));
qed "starfun_ln_HInfinite_gt_zero";
(*
Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x";
*)
Goal "sumhr (0, whn, %n. (if even(n) then 0 else \
\ ((- 1) ^ ((n - 1) div 2))/(real (fact n))) * x ^ n) \
\ : HFinite";
by (auto_tac (claset() addSIs [NSBseq_HFinite_hypreal,NSconvergent_NSBseq],
simpset() addsimps [starfunNat_sumr RS sym,starfunNat,hypnat_omega_def,
convergent_NSconvergent_iff RS sym, summable_convergent_sumr_iff RS sym]));
by (rtac (CLAIM "1 = Suc 0" RS ssubst) 1);
by (rtac summable_sin 1);
qed "HFinite_sin";
Addsimps [HFinite_sin];
Goal "( *f* sin) 0 = 0";
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_zero_num]));
qed "STAR_sin_zero";
Addsimps [STAR_sin_zero];
Goal "x : Infinitesimal ==> ( *f* sin) x @= x";
by (case_tac "x = 0" 1);
by (cut_inst_tac [("x","0")] DERIV_sin 2);
by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym,
nsderiv_def,hypreal_of_real_zero]));
by (dres_inst_tac [("x","x")] bspec 1);
by Auto_tac;
by (dres_inst_tac [("c","x")] approx_mult1 1);
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
simpset() addsimps [hypreal_mult_assoc]));
qed "STAR_sin_Infinitesimal";
Addsimps [STAR_sin_Infinitesimal];
Goal "sumhr (0, whn, %n. (if even(n) then \
\ ((- 1) ^ (n div 2))/(real (fact n)) else \
\ 0) * x ^ n) : HFinite";
by (auto_tac (claset() addSIs [NSBseq_HFinite_hypreal,NSconvergent_NSBseq],
simpset() addsimps [starfunNat_sumr RS sym,starfunNat,hypnat_omega_def,
convergent_NSconvergent_iff RS sym, summable_convergent_sumr_iff RS sym,
summable_cos]));
qed "HFinite_cos";
Addsimps [HFinite_cos];
Goal "( *f* cos) 0 = 1";
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_zero_num,
hypreal_one_num]));
qed "STAR_cos_zero";
Addsimps [STAR_cos_zero];
Goal "x : Infinitesimal ==> ( *f* cos) x @= 1";
by (case_tac "x = 0" 1);
by (cut_inst_tac [("x","0")] DERIV_cos 2);
by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym,
nsderiv_def,hypreal_of_real_zero]));
by (dres_inst_tac [("x","x")] bspec 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_zero,
hypreal_of_real_one]));
by (dres_inst_tac [("c","x")] approx_mult1 1);
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
simpset() addsimps [hypreal_mult_assoc,hypreal_of_real_one]));
by (res_inst_tac [("d","-1")] approx_add_right_cancel 1);
by Auto_tac;
qed "STAR_cos_Infinitesimal";
Addsimps [STAR_cos_Infinitesimal];
Goal "( *f* tan) 0 = 0";
by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_zero_num]));
qed "STAR_tan_zero";
Addsimps [STAR_tan_zero];
Goal "x : Infinitesimal ==> ( *f* tan) x @= x";
by (case_tac "x = 0" 1);
by (cut_inst_tac [("x","0")] DERIV_tan 2);
by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym,
nsderiv_def,hypreal_of_real_zero]));
by (dres_inst_tac [("x","x")] bspec 1);
by Auto_tac;
by (dres_inst_tac [("c","x")] approx_mult1 1);
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
simpset() addsimps [hypreal_mult_assoc]));
qed "STAR_tan_Infinitesimal";
Goal "x : Infinitesimal ==> ( *f* sin) x * ( *f* cos) x @= x";
by (rtac (simplify (simpset()) (read_instantiate
[("d","1")] approx_mult_HFinite)) 1);
by (auto_tac (claset(),simpset() addsimps [Infinitesimal_subset_HFinite
RS subsetD]));
qed "STAR_sin_cos_Infinitesimal_mult";
Goal "hypreal_of_real pi : HFinite";
by (Simp_tac 1);
qed "HFinite_pi";
(* lemmas *)
Goal "N : HNatInfinite \
\ ==> hypreal_of_real a = \
\ hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)";
by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,
HNatInfinite_not_eq_zero]));
val lemma_split_hypreal_of_real = result();
Goal "[|x : Infinitesimal; x ~= 0 |] ==> ( *f* sin) x/x @= 1";
by (cut_inst_tac [("x","0")] DERIV_sin 1);
by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym,
nsderiv_def,hypreal_of_real_zero,hypreal_of_real_one]));
qed "STAR_sin_Infinitesimal_divide";
(*------------------------------------------------------------------------*)
(* sin* (1/n) * 1/(1/n) @= 1 for n = oo *)
(*------------------------------------------------------------------------*)
Goal "n : HNatInfinite \
\ ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) @= 1";
by (rtac STAR_sin_Infinitesimal_divide 1);
by Auto_tac;
val lemma_sin_pi = result();
Goal "n : HNatInfinite \
\ ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1";
by (forward_tac [lemma_sin_pi] 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_divide_def]));
qed "STAR_sin_inverse_HNatInfinite";
Goalw [hypreal_divide_def]
"N : HNatInfinite \
\ ==> hypreal_of_real pi/(hypreal_of_hypnat N) : Infinitesimal";
by (auto_tac (claset() addIs [Infinitesimal_HFinite_mult2],simpset()));
qed "Infinitesimal_pi_divide_HNatInfinite";
Goal "N : HNatInfinite \
\ ==> hypreal_of_real pi/(hypreal_of_hypnat N) ~= 0";
by Auto_tac;
qed "pi_divide_HNatInfinite_not_zero";
Addsimps [pi_divide_HNatInfinite_not_zero];
Goal "n : HNatInfinite \
\ ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n \
\ @= hypreal_of_real pi";
by (ftac ([Infinitesimal_pi_divide_HNatInfinite,pi_divide_HNatInfinite_not_zero]
MRS STAR_sin_Infinitesimal_divide) 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_inverse_distrib]));
by (res_inst_tac [("a","inverse(hypreal_of_real pi)")] approx_SReal_mult_cancel 1);
by (auto_tac (claset() addIs [SReal_inverse],simpset() addsimps [hypreal_divide_def] @
hypreal_mult_ac));
qed "STAR_sin_pi_divide_HNatInfinite_approx_pi";
Goal "n : HNatInfinite \
\ ==> hypreal_of_hypnat n * \
\ ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) \
\ @= hypreal_of_real pi";
by (rtac (hypreal_mult_commute RS subst) 1);
by (etac STAR_sin_pi_divide_HNatInfinite_approx_pi 1);
qed "STAR_sin_pi_divide_HNatInfinite_approx_pi2";
(*** more theorems ***)
Goalw [real_divide_def]
"N : HNatInfinite \
\ ==> ( *fNat* (%x. pi / real x)) N : Infinitesimal";
by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2],
simpset() addsimps [starfunNat_mult RS sym,starfunNat_inverse RS sym,
starfunNat_real_of_nat]));
qed "starfunNat_pi_divide_n_Infinitesimal";
Goal "N : HNatInfinite ==> \
\ ( *f* sin) (( *fNat* (%x. pi / real x)) N) @= \
\ hypreal_of_real pi/(hypreal_of_hypnat N)";
by (auto_tac (claset() addSIs [STAR_sin_Infinitesimal,
Infinitesimal_HFinite_mult2],simpset() addsimps [starfunNat_mult RS sym,
hypreal_divide_def,real_divide_def,starfunNat_inverse_real_of_nat_eq]));
qed "STAR_sin_pi_divide_n_approx";
(*** move to NSA ***)
Goalw [hypnat_zero_def] "(n <= (0::hypnat)) = (n = 0)";
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps [hypnat_le]));
qed "hypnat_le_zero_cancel";
AddIffs [hypnat_le_zero_cancel];
Goal "N : HNatInfinite ==> 0 < hypreal_of_hypnat N";
by (rtac ccontr 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_of_hypnat_zero RS sym,
symmetric hypnat_le_def]));
qed "HNatInfinite_hypreal_of_hypnat_gt_zero";
bind_thm ("HNatInfinite_hypreal_of_hypnat_not_eq_zero",
HNatInfinite_hypreal_of_hypnat_gt_zero RS hypreal_not_refl2 RS not_sym);
(*** END: move to NSA ***)
Goalw [NSLIMSEQ_def] "(%n. real n * sin (pi / real n)) ----NS> pi";
by (auto_tac (claset(),simpset() addsimps [starfunNat_mult RS sym,
starfunNat_real_of_nat]));
by (res_inst_tac [("f1","sin")] (starfun_stafunNat_o2 RS subst) 1);
by (auto_tac (claset(),simpset() addsimps [starfunNat_mult RS sym,
starfunNat_real_of_nat,real_divide_def]));
by (res_inst_tac [("f1","inverse")] (starfun_stafunNat_o2 RS subst) 1);
by (auto_tac (claset() addDs [STAR_sin_pi_divide_HNatInfinite_approx_pi],
simpset() addsimps [starfunNat_real_of_nat,hypreal_mult_commute,
symmetric hypreal_divide_def]));
qed "NSLIMSEQ_sin_pi";
Goalw [NSLIMSEQ_def] "(%n. cos (pi / real n))----NS> 1";
by Auto_tac;
by (res_inst_tac [("f1","cos")] (starfun_stafunNat_o2 RS subst) 1);
by (rtac STAR_cos_Infinitesimal 1);
by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2],
simpset() addsimps [starfunNat_mult RS sym,real_divide_def,
starfunNat_inverse RS sym,starfunNat_real_of_nat]));
qed "NSLIMSEQ_cos_one";
Goal "(%n. real n * sin (pi / real n) * cos (pi / real n)) ----NS> pi";
by (rtac (simplify (simpset())
([NSLIMSEQ_sin_pi,NSLIMSEQ_cos_one] MRS NSLIMSEQ_mult)) 1);
qed "NSLIMSEQ_sin_cos_pi";
(*------------------------------------------------------------------------*)
(* A familiar approximation to cos x when x is small *)
(*------------------------------------------------------------------------*)
Goal "x : Infinitesimal ==> ( *f* cos) x @= 1 - x ^ 2";
by (rtac (STAR_cos_Infinitesimal RS approx_trans) 1);
by (auto_tac (claset(),simpset() addsimps [Infinitesimal_approx_minus RS sym,
hypreal_diff_def,hypreal_add_assoc RS sym,two_eq_Suc_Suc]));
qed "STAR_cos_Infinitesimal_approx";
(* move to NSA *)
Goalw [hypreal_divide_def]
"[| x : Infinitesimal; y : Reals; y ~= 0 |] ==> x/y : Infinitesimal";
by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult]
addSDs [SReal_inverse RS (SReal_subset_HFinite RS subsetD)],simpset()));
qed "Infinitesimal_SReal_divide";
Goal "x : Infinitesimal ==> ( *f* cos) x @= 1 - (x ^ 2)/2";
by (rtac (STAR_cos_Infinitesimal RS approx_trans) 1);
by (auto_tac (claset() addIs [Infinitesimal_SReal_divide],
simpset() addsimps [Infinitesimal_approx_minus RS sym,
two_eq_Suc_Suc]));
qed "STAR_cos_Infinitesimal_approx2";