--- a/src/HOL/Hyperreal/HTranscendental.ML Mon Mar 01 05:39:32 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,739 +0,0 @@
-(* Title : HTranscendental.ML
- Author : Jacques D. Fleuriot
- Copyright : 2001 University of Edinburgh
- Description : Nonstandard extensions of transcendental functions
-*)
-
-val hpowr_Suc= thm"hpowr_Suc";
-
-(*-------------------------------------------------------------------------*)
-(* 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 [numeral_2_eq_2]));
-qed "hypreal_sqrt_not_zero";
-
-Goal "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x";
-by (cut_inst_tac [("n1","2"),("a1","( *f* sqrt) x")] (power_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 [order_le_less]));
-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 [numeral_2_eq_2]));
-qed "hypreal_sqrt_approx_zero";
-Addsimps [hypreal_sqrt_approx_zero];
-
-Goal "0 <= x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)";
-by (auto_tac (claset(), simpset() addsimps [order_le_less]));
-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 (claset(), simpset() addsimps [zero_le_square]));
-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 (claset(), simpset() addsimps [zero_le_square]));
-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 [order_le_less ]));
-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,numeral_2_eq_2]));
-qed "hypreal_sqrt_hrabs";
-Addsimps [hypreal_sqrt_hrabs];
-
-Goal "( *f* sqrt)(x*x) = abs(x)";
-by (rtac (hrealpow_two RS subst) 1);
-by (rtac (numeral_2_eq_2 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_eq,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")] power_inject_base 1);
-by (auto_tac (claset() addSIs [st_zero_le,hypreal_sqrt_ge_zero],simpset()));
-by (rtac (st_mult RS subst) 1);
-by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 3);
-by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 5);
-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 [order_le_less]));
-by (rtac (HFinite_square_iff RS iffD1) 1);
-by (dtac hypreal_sqrt_gt_zero_pow2 1);
-by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2]));
-qed "HFinite_hypreal_sqrt";
-
-Goal "[| 0 <= x; ( *f* sqrt) x : HFinite |] ==> x : HFinite";
-by (auto_tac (claset(),simpset() addsimps [order_le_less]));
-by (dtac (HFinite_square_iff RS iffD2) 1);
-by (dtac hypreal_sqrt_gt_zero_pow2 1);
-by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2] 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 (claset(), simpset() addsimps [zero_le_square]));
-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 [order_le_less]));
-by (rtac (Infinitesimal_square_iff RS iffD2) 1);
-by (dtac hypreal_sqrt_gt_zero_pow2 1);
-by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2]));
-qed "Infinitesimal_hypreal_sqrt";
-
-Goal "[| 0 <= x; ( *f* sqrt) x : Infinitesimal |] ==> x : Infinitesimal";
-by (auto_tac (claset(),simpset() addsimps [order_le_less]));
-by (dtac (Infinitesimal_square_iff RS iffD1) 1);
-by (dtac hypreal_sqrt_gt_zero_pow2 1);
-by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2]
- 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 (claset(), simpset() addsimps [zero_le_square]));
-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 [order_le_less]));
-by (rtac (HInfinite_square_iff RS iffD1) 1);
-by (dtac hypreal_sqrt_gt_zero_pow2 1);
-by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2]));
-qed "HInfinite_hypreal_sqrt";
-
-Goal "[| 0 <= x; ( *f* sqrt) x : HInfinite |] ==> x : HInfinite";
-by (auto_tac (claset(),simpset() addsimps [order_le_less]));
-by (dtac (HInfinite_square_iff RS iffD2) 1);
-by (dtac hypreal_sqrt_gt_zero_pow2 1);
-by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2]
- 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 (claset(), simpset() addsimps [zero_le_square]));
-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 positive_imp_inverse_positive 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 (claset(),simpset() addsimps [HNatInfinite_not_eq_zero]));
-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 (claset(),simpset() addsimps [HNatInfinite_not_eq_zero]));
-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] @ 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, linorder_not_less]));
-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,numeral_2_eq_2]));
-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,
- numeral_2_eq_2]));
-qed "STAR_cos_Infinitesimal_approx2";
-
-
-
-
-
--- a/src/HOL/Hyperreal/HTranscendental.thy Mon Mar 01 05:39:32 2004 +0100
+++ b/src/HOL/Hyperreal/HTranscendental.thy Mon Mar 01 11:52:59 2004 +0100
@@ -1,23 +1,740 @@
(* Title : HTranscendental.thy
Author : Jacques D. Fleuriot
Copyright : 2001 University of Edinburgh
- Description : Nonstandard extensions of transcendental functions
+
+Converted to Isar and polished by lcp
*)
-HTranscendental = Transcendental + IntFloor +
+header{*Nonstandard Extensions of Transcendental Functions*}
+
+theory HTranscendental = Transcendental + IntFloor:
constdefs
-
- (* define exponential function using standard part *)
- exphr :: real => hypreal
+ exphr :: "real => hypreal"
+ --{*define exponential function using standard part *}
"exphr x == st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))"
- sinhr :: real => hypreal
+ sinhr :: "real => hypreal"
"sinhr x == st(sumhr (0, whn, %n. (if even(n) then 0 else
((-1) ^ ((n - 1) div 2))/(real (fact n))) * (x ^ n)))"
- coshr :: real => hypreal
+ coshr :: "real => hypreal"
"coshr x == st(sumhr (0, whn, %n. (if even(n) then
((-1) ^ (n div 2))/(real (fact n)) else 0) * x ^ n))"
-end
\ No newline at end of file
+
+
+subsection{*Nonstandard Extension of Square Root Function*}
+
+lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0"
+by (simp add: starfun hypreal_zero_num)
+
+lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1"
+by (simp add: starfun hypreal_one_num)
+
+lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
+apply (rule eq_Abs_hypreal [of x])
+apply (auto simp add: hypreal_le hypreal_zero_num starfun hrealpow
+ real_sqrt_pow2_iff
+ simp del: hpowr_Suc realpow_Suc)
+done
+
+lemma hypreal_sqrt_gt_zero_pow2: "0 < x ==> ( *f* sqrt) (x) ^ 2 = x"
+apply (rule eq_Abs_hypreal [of x])
+apply (auto intro: FreeUltrafilterNat_subset real_sqrt_gt_zero_pow2
+ simp add: hypreal_less starfun hrealpow hypreal_zero_num
+ simp del: hpowr_Suc realpow_Suc)
+done
+
+lemma hypreal_sqrt_pow2_gt_zero: "0 < x ==> 0 < ( *f* sqrt) (x) ^ 2"
+by (frule hypreal_sqrt_gt_zero_pow2, auto)
+
+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_inverse_sqrt_pow2:
+ "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"
+apply (cut_tac n1 = 2 and a1 = "( *f* sqrt) x" in power_inverse [symmetric])
+apply (auto dest: hypreal_sqrt_gt_zero_pow2)
+done
+
+lemma hypreal_sqrt_mult_distrib:
+ "[|0 < x; 0 <y |] ==> ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of y])
+apply (simp add: hypreal_zero_def starfun hypreal_mult hypreal_less hypreal_zero_num, ultra)
+apply (auto intro: real_sqrt_mult_distrib)
+done
+
+lemma hypreal_sqrt_mult_distrib2:
+ "[|0\<le>x; 0\<le>y |] ==>
+ ( *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) @= 0) = (x @= 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
+
+lemma hypreal_sqrt_approx_zero2 [simp]:
+ "0 \<le> x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
+by (auto simp add: order_le_less)
+
+lemma hypreal_sqrt_sum_squares [simp]:
+ "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)"
+apply (rule hypreal_sqrt_approx_zero2)
+apply (rule hypreal_le_add_order)+
+apply (auto simp add: zero_le_square)
+done
+
+lemma hypreal_sqrt_sum_squares2 [simp]:
+ "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)"
+apply (rule hypreal_sqrt_approx_zero2)
+apply (rule hypreal_le_add_order)
+apply (auto simp add: zero_le_square)
+done
+
+lemma hypreal_sqrt_gt_zero: "0 < x ==> 0 < ( *f* sqrt)(x)"
+apply (rule eq_Abs_hypreal [of x])
+apply (auto simp add: starfun hypreal_zero_def hypreal_less hypreal_zero_num, ultra)
+apply (auto intro: real_sqrt_gt_zero)
+done
+
+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]: "( *f* sqrt)(x ^ 2) = abs(x)"
+apply (rule eq_Abs_hypreal [of x])
+apply (simp add: starfun hypreal_hrabs hypreal_mult numeral_2_eq_2)
+done
+
+lemma hypreal_sqrt_hrabs2 [simp]: "( *f* sqrt)(x*x) = abs(x)"
+apply (rule hrealpow_two [THEN subst])
+apply (rule numeral_2_eq_2 [THEN subst])
+apply (rule hypreal_sqrt_hrabs)
+done
+
+lemma hypreal_sqrt_hyperpow_hrabs [simp]:
+ "( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"
+apply (rule eq_Abs_hypreal [of x])
+apply (simp add: starfun hypreal_hrabs hypnat_of_nat_eq hyperpow)
+done
+
+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
+
+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
+
+lemma hypreal_sqrt_sum_squares_ge1 [simp]: "x \<le> ( *f* sqrt)(x ^ 2 + y ^ 2)"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of y])
+apply (simp add: starfun hypreal_add hrealpow hypreal_le
+ del: hpowr_Suc realpow_Suc)
+done
+
+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 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
+
+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 hypreal_le_add_order)
+apply (auto simp add: zero_le_square)
+done
+
+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
+
+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
+
+lemma Infinitesimal_hypreal_sqrt_iff [simp]:
+ "0 \<le> x ==> (( *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 hypreal_le_add_order)
+apply (auto simp add: zero_le_square)
+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
+
+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
+
+lemma HInfinite_hypreal_sqrt_iff [simp]:
+ "0 \<le> x ==> (( *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 hypreal_le_add_order)
+apply (auto simp add: zero_le_square)
+done
+
+lemma HFinite_exp [simp]:
+ "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) \<in> HFinite"
+by (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq
+ simp add: starfunNat_sumr [symmetric] starfunNat hypnat_omega_def
+ convergent_NSconvergent_iff [symmetric]
+ summable_convergent_sumr_iff [symmetric] 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 (simp add: sumhr hypnat_zero_def starfunNat hypnat_one_def hypnat_add
+ hypnat_omega_def hypreal_add
+ del: hypnat_add_zero_left)
+apply (simp add: hypreal_one_num [symmetric])
+done
+
+lemma coshr_zero [simp]: "coshr 0 = 1"
+apply (simp add: coshr_def sumhr_split_add
+ [OF hypnat_one_less_hypnat_omega, symmetric])
+apply (simp add: sumhr hypnat_zero_def starfunNat hypnat_one_def
+ hypnat_add hypnat_omega_def st_add [symmetric]
+ hypreal_one_def [symmetric] hypreal_zero_def [symmetric]
+ del: hypnat_add_zero_left)
+done
+
+lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) 0 @= 1"
+by (simp add: hypreal_zero_def hypreal_one_def starfun hypreal_one_num)
+
+lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) x @= 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)
+apply (drule_tac x = x in bspec, auto)
+apply (drule_tac c = x in approx_mult1)
+apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
+ simp add: mult_assoc)
+apply (rule approx_add_right_cancel [where d="-1"])
+apply (rule approx_sym [THEN [2] approx_trans2])
+apply (auto simp add: mem_infmal_iff)
+done
+
+lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
+by (auto intro: STAR_exp_Infinitesimal)
+
+lemma STAR_exp_add: "( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
+apply (rule eq_Abs_hypreal [of x])
+apply (rule eq_Abs_hypreal [of y])
+apply (simp add: starfun hypreal_add hypreal_mult exp_add)
+done
+
+lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)"
+apply (simp add: exphr_def)
+apply (rule st_hypreal_of_real [THEN subst])
+apply (rule approx_st_eq, auto)
+apply (rule approx_minus_iff [THEN iffD2])
+apply (auto simp add: mem_infmal_iff [symmetric] hypreal_of_real_def hypnat_zero_def hypnat_omega_def sumhr hypreal_minus hypreal_add)
+apply (rule NSLIMSEQ_zero_Infinitesimal_hypreal)
+apply (insert exp_converges [of x])
+apply (simp add: sums_def)
+apply (drule LIMSEQ_const [THEN [2] LIMSEQ_add, where b = "- exp x"])
+apply (simp add: LIMSEQ_NSLIMSEQ_iff)
+done
+
+lemma starfun_exp_ge_add_one_self [simp]: "0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
+apply (rule eq_Abs_hypreal [of x])
+apply (simp add: starfun hypreal_add hypreal_le hypreal_zero_num hypreal_one_num, ultra)
+done
+
+(* exp (oo) is infinite *)
+lemma starfun_exp_HInfinite:
+ "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) x \<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: "( *f* exp) (-x) = inverse(( *f* exp) x)"
+apply (rule eq_Abs_hypreal [of x])
+apply (simp add: starfun hypreal_inverse hypreal_minus exp_minus)
+done
+
+(* exp (-oo) is infinitesimal *)
+lemma starfun_exp_Infinitesimal:
+ "[| x \<in> HInfinite; x \<le> 0 |] ==> ( *f* exp) x \<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]: "0 < x ==> 1 < ( *f* exp) x"
+apply (rule eq_Abs_hypreal [of x])
+apply (simp add: starfun hypreal_one_num hypreal_zero_num hypreal_less, ultra)
+done
+
+(* 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";
+
+*)
+
+
+lemma starfun_ln_exp [simp]: "( *f* ln) (( *f* exp) x) = x"
+apply (rule eq_Abs_hypreal [of x])
+apply (simp add: starfun)
+done
+
+lemma starfun_exp_ln_iff [simp]: "(( *f* exp)(( *f* ln) x) = x) = (0 < x)"
+apply (rule eq_Abs_hypreal [of x])
+apply (simp add: starfun hypreal_zero_num hypreal_less)
+done
+
+lemma starfun_exp_ln_eq: "( *f* exp) u = x ==> ( *f* ln) x = u"
+by (auto simp add: starfun)
+
+lemma starfun_ln_less_self [simp]: "0 < x ==> ( *f* ln) x < x"
+apply (rule eq_Abs_hypreal [of x])
+apply (simp add: starfun hypreal_zero_num hypreal_less, ultra)
+done
+
+lemma starfun_ln_ge_zero [simp]: "1 \<le> x ==> 0 \<le> ( *f* ln) x"
+apply (rule eq_Abs_hypreal [of x])
+apply (simp add: starfun hypreal_zero_num hypreal_le hypreal_one_num, ultra)
+done
+
+lemma starfun_ln_gt_zero [simp]: "1 < x ==> 0 < ( *f* ln) x"
+apply (rule eq_Abs_hypreal [of x])
+apply (simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
+done
+
+lemma starfun_ln_not_eq_zero [simp]: "[| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
+apply (rule eq_Abs_hypreal [of x])
+apply (auto simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
+apply (auto dest: ln_not_eq_zero)
+done
+
+lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* ln) x \<in> HFinite"
+apply (rule HFinite_bounded)
+apply (rule_tac [2] order_less_imp_le)
+apply (rule_tac [2] starfun_ln_less_self)
+apply (rule_tac [2] order_less_le_trans, auto)
+done
+
+lemma starfun_ln_inverse: "0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
+apply (rule eq_Abs_hypreal [of x])
+apply (simp add: starfun hypreal_zero_num hypreal_minus hypreal_inverse hypreal_less, ultra)
+apply (simp add: ln_inverse)
+done
+
+lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
+apply (rule eq_Abs_hypreal [of x])
+apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
+apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
+apply (rule_tac x = "exp u" in exI)
+apply (ultra, arith)
+done
+
+lemma starfun_exp_add_HFinite_Infinitesimal_approx:
+ "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x) @= ( *f* exp) z"
+apply (simp add: STAR_exp_add)
+apply (frule STAR_exp_Infinitesimal)
+apply (drule approx_mult2)
+apply (auto intro: starfun_exp_HFinite)
+done
+
+(* using previous result to get to result *)
+lemma starfun_ln_HInfinite:
+ "[| x \<in> HInfinite; 0 < x |] ==> ( *f* 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)
+done
+
+lemma starfun_exp_HInfinite_Infinitesimal_disj:
+ "x \<in> HInfinite ==> ( *f* exp) x \<in> HInfinite | ( *f* exp) x \<in> Infinitesimal"
+apply (insert linorder_linear [of x 0])
+apply (auto intro: starfun_exp_HInfinite starfun_exp_Infinitesimal)
+done
+
+(* check out this proof!!! *)
+lemma starfun_ln_HFinite_not_Infinitesimal:
+ "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* 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
+ del: starfun_exp_ln_iff)
+done
+
+(* we do proof by considering ln of 1/x *)
+lemma starfun_ln_Infinitesimal_HInfinite:
+ "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* 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: "[| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
+apply (rule eq_Abs_hypreal [of x])
+apply (simp add: hypreal_zero_num hypreal_one_num hypreal_less starfun, ultra)
+apply (auto intro: ln_less_zero)
+done
+
+lemma starfun_ln_Infinitesimal_less_zero:
+ "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0"
+apply (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
+apply (drule bspec [where x = 1])
+apply (auto simp add: abs_if)
+done
+
+lemma starfun_ln_HInfinite_gt_zero:
+ "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* ln) x"
+apply (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
+apply (drule bspec [where x = 1])
+apply (auto simp add: abs_if)
+done
+
+(*
+Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x"
+*)
+
+lemma HFinite_sin [simp]:
+ "sumhr (0, whn, %n. (if even(n) then 0 else
+ ((- 1) ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)
+ \<in> HFinite"
+apply (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq
+ simp add: starfunNat_sumr [symmetric] starfunNat hypnat_omega_def
+ convergent_NSconvergent_iff [symmetric]
+ summable_convergent_sumr_iff [symmetric])
+apply (simp only: One_nat_def summable_sin)
+done
+
+lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0"
+by (simp add: starfun hypreal_zero_num)
+
+lemma STAR_sin_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* sin) x @= 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 hypreal_of_real_zero)
+apply (drule bspec [where x = x], auto)
+apply (drule approx_mult1 [where c = x])
+apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
+ simp add: mult_assoc)
+done
+
+lemma HFinite_cos [simp]:
+ "sumhr (0, whn, %n. (if even(n) then
+ ((- 1) ^ (n div 2))/(real (fact n)) else
+ 0) * x ^ n) \<in> HFinite"
+by (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq
+ simp add: starfunNat_sumr [symmetric] starfunNat hypnat_omega_def
+ convergent_NSconvergent_iff [symmetric]
+ summable_convergent_sumr_iff [symmetric] summable_cos)
+
+lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1"
+by (simp add: starfun hypreal_zero_num hypreal_one_num)
+
+lemma STAR_cos_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* cos) x @= 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 hypreal_of_real_zero)
+apply (drule bspec [where x = x])
+apply (auto simp add: hypreal_of_real_zero hypreal_of_real_one)
+apply (drule approx_mult1 [where c = x])
+apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
+ simp add: mult_assoc hypreal_of_real_one)
+apply (rule approx_add_right_cancel [where d = "-1"], auto)
+done
+
+lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
+by (simp add: starfun hypreal_zero_num)
+
+lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x @= 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 hypreal_of_real_zero)
+apply (drule bspec [where x = x], auto)
+apply (drule approx_mult1 [where c = x])
+apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
+ simp add: mult_assoc)
+done
+
+lemma STAR_sin_cos_Infinitesimal_mult:
+ "x \<in> Infinitesimal ==> ( *f* sin) x * ( *f* cos) x @= x"
+apply (insert approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1])
+apply (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
+done
+
+lemma HFinite_pi: "hypreal_of_real pi \<in> HFinite"
+by simp
+
+(* lemmas *)
+
+lemma lemma_split_hypreal_of_real:
+ "N \<in> HNatInfinite
+ ==> hypreal_of_real a =
+ hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)"
+by (simp add: mult_assoc [symmetric] HNatInfinite_not_eq_zero)
+
+lemma STAR_sin_Infinitesimal_divide:
+ "[|x \<in> Infinitesimal; x \<noteq> 0 |] ==> ( *f* sin) x/x @= 1"
+apply (cut_tac x = 0 in DERIV_sin)
+apply (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero hypreal_of_real_one)
+done
+
+(*------------------------------------------------------------------------*)
+(* sin* (1/n) * 1/(1/n) @= 1 for n = oo *)
+(*------------------------------------------------------------------------*)
+
+lemma lemma_sin_pi:
+ "n \<in> HNatInfinite
+ ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) @= 1"
+apply (rule STAR_sin_Infinitesimal_divide)
+apply (auto simp add: HNatInfinite_not_eq_zero)
+done
+
+lemma STAR_sin_inverse_HNatInfinite:
+ "n \<in> HNatInfinite
+ ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1"
+apply (frule lemma_sin_pi)
+apply (simp add: divide_inverse_zero)
+done
+
+lemma Infinitesimal_pi_divide_HNatInfinite:
+ "N \<in> HNatInfinite
+ ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
+apply (simp add: divide_inverse_zero)
+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"
+by (simp add: HNatInfinite_not_eq_zero)
+
+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
+ @= hypreal_of_real pi"
+apply (frule STAR_sin_Infinitesimal_divide
+ [OF Infinitesimal_pi_divide_HNatInfinite
+ pi_divide_HNatInfinite_not_zero])
+apply (auto simp add: hypreal_inverse_distrib)
+apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
+apply (auto intro: SReal_inverse simp add: divide_inverse_zero mult_ac)
+done
+
+lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
+ "n \<in> HNatInfinite
+ ==> hypreal_of_hypnat n *
+ ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n))
+ @= hypreal_of_real pi"
+apply (rule mult_commute [THEN subst])
+apply (erule STAR_sin_pi_divide_HNatInfinite_approx_pi)
+done
+
+lemma starfunNat_pi_divide_n_Infinitesimal:
+ "N \<in> HNatInfinite ==> ( *fNat* (%x. pi / real x)) N \<in> Infinitesimal"
+by (auto intro!: Infinitesimal_HFinite_mult2
+ simp add: starfunNat_mult [symmetric] divide_inverse_zero
+ starfunNat_inverse [symmetric] starfunNat_real_of_nat)
+
+lemma STAR_sin_pi_divide_n_approx:
+ "N \<in> HNatInfinite ==>
+ ( *f* sin) (( *fNat* (%x. pi / real x)) N) @=
+ hypreal_of_real pi/(hypreal_of_hypnat N)"
+by (auto intro!: STAR_sin_Infinitesimal Infinitesimal_HFinite_mult2
+ simp add: starfunNat_mult [symmetric] divide_inverse_zero
+ starfunNat_inverse_real_of_nat_eq)
+
+lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) ----NS> pi"
+apply (auto simp add: NSLIMSEQ_def starfunNat_mult [symmetric] starfunNat_real_of_nat)
+apply (rule_tac f1 = sin in starfun_stafunNat_o2 [THEN subst])
+apply (auto simp add: starfunNat_mult [symmetric] starfunNat_real_of_nat divide_inverse_zero)
+apply (rule_tac f1 = inverse in starfun_stafunNat_o2 [THEN subst])
+apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi
+ simp add: starfunNat_real_of_nat mult_commute divide_inverse_zero)
+done
+
+lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))----NS> 1"
+apply (simp add: NSLIMSEQ_def, auto)
+apply (rule_tac f1 = cos in starfun_stafunNat_o2 [THEN subst])
+apply (rule STAR_cos_Infinitesimal)
+apply (auto intro!: Infinitesimal_HFinite_mult2
+ simp add: starfunNat_mult [symmetric] divide_inverse_zero
+ starfunNat_inverse [symmetric] starfunNat_real_of_nat)
+done
+
+lemma NSLIMSEQ_sin_cos_pi:
+ "(%n. real n * sin (pi / real n) * cos (pi / real n)) ----NS> pi"
+by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
+
+
+text{*A familiar approximation to @{term "cos x"} when @{term x} is small*}
+
+lemma STAR_cos_Infinitesimal_approx:
+ "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x ^ 2"
+apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
+apply (auto simp add: Infinitesimal_approx_minus [symmetric]
+ diff_minus add_assoc [symmetric] numeral_2_eq_2)
+done
+
+lemma STAR_cos_Infinitesimal_approx2:
+ "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x ^ 2)/2"
+apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
+apply (auto intro: Infinitesimal_SReal_divide
+ simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
+done
+
+ML
+{*
+val STAR_sqrt_zero = thm "STAR_sqrt_zero";
+val STAR_sqrt_one = thm "STAR_sqrt_one";
+val hypreal_sqrt_pow2_iff = thm "hypreal_sqrt_pow2_iff";
+val hypreal_sqrt_gt_zero_pow2 = thm "hypreal_sqrt_gt_zero_pow2";
+val hypreal_sqrt_pow2_gt_zero = thm "hypreal_sqrt_pow2_gt_zero";
+val hypreal_sqrt_not_zero = thm "hypreal_sqrt_not_zero";
+val hypreal_inverse_sqrt_pow2 = thm "hypreal_inverse_sqrt_pow2";
+val hypreal_sqrt_mult_distrib = thm "hypreal_sqrt_mult_distrib";
+val hypreal_sqrt_mult_distrib2 = thm "hypreal_sqrt_mult_distrib2";
+val hypreal_sqrt_approx_zero = thm "hypreal_sqrt_approx_zero";
+val hypreal_sqrt_approx_zero2 = thm "hypreal_sqrt_approx_zero2";
+val hypreal_sqrt_sum_squares = thm "hypreal_sqrt_sum_squares";
+val hypreal_sqrt_sum_squares2 = thm "hypreal_sqrt_sum_squares2";
+val hypreal_sqrt_gt_zero = thm "hypreal_sqrt_gt_zero";
+val hypreal_sqrt_ge_zero = thm "hypreal_sqrt_ge_zero";
+val hypreal_sqrt_hrabs = thm "hypreal_sqrt_hrabs";
+val hypreal_sqrt_hrabs2 = thm "hypreal_sqrt_hrabs2";
+val hypreal_sqrt_hyperpow_hrabs = thm "hypreal_sqrt_hyperpow_hrabs";
+val star_sqrt_HFinite = thm "star_sqrt_HFinite";
+val st_hypreal_sqrt = thm "st_hypreal_sqrt";
+val hypreal_sqrt_sum_squares_ge1 = thm "hypreal_sqrt_sum_squares_ge1";
+val HFinite_hypreal_sqrt = thm "HFinite_hypreal_sqrt";
+val HFinite_hypreal_sqrt_imp_HFinite = thm "HFinite_hypreal_sqrt_imp_HFinite";
+val HFinite_hypreal_sqrt_iff = thm "HFinite_hypreal_sqrt_iff";
+val HFinite_sqrt_sum_squares = thm "HFinite_sqrt_sum_squares";
+val Infinitesimal_hypreal_sqrt = thm "Infinitesimal_hypreal_sqrt";
+val Infinitesimal_hypreal_sqrt_imp_Infinitesimal = thm "Infinitesimal_hypreal_sqrt_imp_Infinitesimal";
+val Infinitesimal_hypreal_sqrt_iff = thm "Infinitesimal_hypreal_sqrt_iff";
+val Infinitesimal_sqrt_sum_squares = thm "Infinitesimal_sqrt_sum_squares";
+val HInfinite_hypreal_sqrt = thm "HInfinite_hypreal_sqrt";
+val HInfinite_hypreal_sqrt_imp_HInfinite = thm "HInfinite_hypreal_sqrt_imp_HInfinite";
+val HInfinite_hypreal_sqrt_iff = thm "HInfinite_hypreal_sqrt_iff";
+val HInfinite_sqrt_sum_squares = thm "HInfinite_sqrt_sum_squares";
+val HFinite_exp = thm "HFinite_exp";
+val exphr_zero = thm "exphr_zero";
+val coshr_zero = thm "coshr_zero";
+val STAR_exp_zero_approx_one = thm "STAR_exp_zero_approx_one";
+val STAR_exp_Infinitesimal = thm "STAR_exp_Infinitesimal";
+val STAR_exp_epsilon = thm "STAR_exp_epsilon";
+val STAR_exp_add = thm "STAR_exp_add";
+val exphr_hypreal_of_real_exp_eq = thm "exphr_hypreal_of_real_exp_eq";
+val starfun_exp_ge_add_one_self = thm "starfun_exp_ge_add_one_self";
+val starfun_exp_HInfinite = thm "starfun_exp_HInfinite";
+val starfun_exp_minus = thm "starfun_exp_minus";
+val starfun_exp_Infinitesimal = thm "starfun_exp_Infinitesimal";
+val starfun_exp_gt_one = thm "starfun_exp_gt_one";
+val starfun_ln_exp = thm "starfun_ln_exp";
+val starfun_exp_ln_iff = thm "starfun_exp_ln_iff";
+val starfun_exp_ln_eq = thm "starfun_exp_ln_eq";
+val starfun_ln_less_self = thm "starfun_ln_less_self";
+val starfun_ln_ge_zero = thm "starfun_ln_ge_zero";
+val starfun_ln_gt_zero = thm "starfun_ln_gt_zero";
+val starfun_ln_not_eq_zero = thm "starfun_ln_not_eq_zero";
+val starfun_ln_HFinite = thm "starfun_ln_HFinite";
+val starfun_ln_inverse = thm "starfun_ln_inverse";
+val starfun_exp_HFinite = thm "starfun_exp_HFinite";
+val starfun_exp_add_HFinite_Infinitesimal_approx = thm "starfun_exp_add_HFinite_Infinitesimal_approx";
+val starfun_ln_HInfinite = thm "starfun_ln_HInfinite";
+val starfun_exp_HInfinite_Infinitesimal_disj = thm "starfun_exp_HInfinite_Infinitesimal_disj";
+val starfun_ln_HFinite_not_Infinitesimal = thm "starfun_ln_HFinite_not_Infinitesimal";
+val starfun_ln_Infinitesimal_HInfinite = thm "starfun_ln_Infinitesimal_HInfinite";
+val starfun_ln_less_zero = thm "starfun_ln_less_zero";
+val starfun_ln_Infinitesimal_less_zero = thm "starfun_ln_Infinitesimal_less_zero";
+val starfun_ln_HInfinite_gt_zero = thm "starfun_ln_HInfinite_gt_zero";
+val HFinite_sin = thm "HFinite_sin";
+val STAR_sin_zero = thm "STAR_sin_zero";
+val STAR_sin_Infinitesimal = thm "STAR_sin_Infinitesimal";
+val HFinite_cos = thm "HFinite_cos";
+val STAR_cos_zero = thm "STAR_cos_zero";
+val STAR_cos_Infinitesimal = thm "STAR_cos_Infinitesimal";
+val STAR_tan_zero = thm "STAR_tan_zero";
+val STAR_tan_Infinitesimal = thm "STAR_tan_Infinitesimal";
+val STAR_sin_cos_Infinitesimal_mult = thm "STAR_sin_cos_Infinitesimal_mult";
+val HFinite_pi = thm "HFinite_pi";
+val lemma_split_hypreal_of_real = thm "lemma_split_hypreal_of_real";
+val STAR_sin_Infinitesimal_divide = thm "STAR_sin_Infinitesimal_divide";
+val lemma_sin_pi = thm "lemma_sin_pi";
+val STAR_sin_inverse_HNatInfinite = thm "STAR_sin_inverse_HNatInfinite";
+val Infinitesimal_pi_divide_HNatInfinite = thm "Infinitesimal_pi_divide_HNatInfinite";
+val pi_divide_HNatInfinite_not_zero = thm "pi_divide_HNatInfinite_not_zero";
+val STAR_sin_pi_divide_HNatInfinite_approx_pi = thm "STAR_sin_pi_divide_HNatInfinite_approx_pi";
+val STAR_sin_pi_divide_HNatInfinite_approx_pi2 = thm "STAR_sin_pi_divide_HNatInfinite_approx_pi2";
+val starfunNat_pi_divide_n_Infinitesimal = thm "starfunNat_pi_divide_n_Infinitesimal";
+val STAR_sin_pi_divide_n_approx = thm "STAR_sin_pi_divide_n_approx";
+val NSLIMSEQ_sin_pi = thm "NSLIMSEQ_sin_pi";
+val NSLIMSEQ_cos_one = thm "NSLIMSEQ_cos_one";
+val NSLIMSEQ_sin_cos_pi = thm "NSLIMSEQ_sin_cos_pi";
+val STAR_cos_Infinitesimal_approx = thm "STAR_cos_Infinitesimal_approx";
+val STAR_cos_Infinitesimal_approx2 = thm "STAR_cos_Infinitesimal_approx2";
+*}
+
+
+end
--- a/src/HOL/Hyperreal/HyperNat.thy Mon Mar 01 05:39:32 2004 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy Mon Mar 01 11:52:59 2004 +0100
@@ -395,6 +395,11 @@
by (simp add: hypnat_mult_less_mono2)
qed
+lemma hypnat_le_zero_cancel [iff]: "(n \<le> (0::hypnat)) = (n = 0)"
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: hypnat_zero_def hypnat_le)
+done
+
lemma hypnat_mult_is_0 [simp]: "(m*n = (0::hypnat)) = (m=0 | n=0)"
apply (rule eq_Abs_hypnat [of m])
apply (rule eq_Abs_hypnat [of n])
@@ -809,6 +814,12 @@
apply (drule_tac x = "m + 1" in spec, ultra)
done
+lemma HNatInfinite_hypreal_of_hypnat_gt_zero:
+ "N \<in> HNatInfinite ==> 0 < hypreal_of_hypnat N"
+apply (rule ccontr)
+apply (simp add: hypreal_of_hypnat_zero [symmetric] linorder_not_less)
+done
+
ML
{*
--- a/src/HOL/Hyperreal/NSA.thy Mon Mar 01 05:39:32 2004 +0100
+++ b/src/HOL/Hyperreal/NSA.thy Mon Mar 01 11:52:59 2004 +0100
@@ -1,6 +1,8 @@
(* Title : NSA.thy
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
+
+Converted to Isar and polished by lcp
*)
header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
@@ -43,9 +45,7 @@
-(*--------------------------------------------------------------------
- Closure laws for members of (embedded) set standard real Reals
- --------------------------------------------------------------------*)
+subsection{*Closure Laws for Standard Reals*}
lemma SReal_add [simp]:
"[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x + y \<in> Reals"
@@ -80,7 +80,8 @@
done
declare SReal_minus_iff [simp]
-lemma SReal_add_cancel: "[| (x::hypreal) + y \<in> Reals; y \<in> Reals |] ==> x \<in> Reals"
+lemma SReal_add_cancel:
+ "[| (x::hypreal) + y \<in> Reals; y \<in> Reals |] ==> x \<in> Reals"
apply (drule_tac x = y in SReal_minus)
apply (drule SReal_add, assumption, auto)
done
@@ -146,11 +147,12 @@
done
lemma SReal_hypreal_of_real_image:
- "[| \<exists>x. x: P; P <= Reals |] ==> \<exists>Q. P = hypreal_of_real ` Q"
+ "[| \<exists>x. x: P; P \<subseteq> Reals |] ==> \<exists>Q. P = hypreal_of_real ` Q"
apply (simp add: SReal_def, blast)
done
-lemma SReal_dense: "[| (x::hypreal) \<in> Reals; y \<in> Reals; x<y |] ==> \<exists>r \<in> Reals. x<r & r<y"
+lemma SReal_dense:
+ "[| (x::hypreal) \<in> Reals; y \<in> Reals; x<y |] ==> \<exists>r \<in> Reals. x<r & r<y"
apply (auto simp add: SReal_iff)
apply (drule real_dense, safe)
apply (rule_tac x = "hypreal_of_real r" in bexI, auto)
@@ -159,12 +161,13 @@
(*------------------------------------------------------------------
Completeness of Reals
------------------------------------------------------------------*)
-lemma SReal_sup_lemma: "P <= Reals ==> ((\<exists>x \<in> P. y < x) =
+lemma SReal_sup_lemma:
+ "P \<subseteq> Reals ==> ((\<exists>x \<in> P. y < x) =
(\<exists>X. hypreal_of_real X \<in> P & y < hypreal_of_real X))"
by (blast dest!: SReal_iff [THEN iffD1])
lemma SReal_sup_lemma2:
- "[| P <= Reals; \<exists>x. x \<in> P; \<exists>y \<in> Reals. \<forall>x \<in> P. x < y |]
+ "[| P \<subseteq> Reals; \<exists>x. x \<in> P; \<exists>y \<in> Reals. \<forall>x \<in> P. x < y |]
==> (\<exists>X. X \<in> {w. hypreal_of_real w \<in> P}) &
(\<exists>Y. \<forall>X \<in> {w. hypreal_of_real w \<in> P}. X < Y)"
apply (rule conjI)
@@ -202,10 +205,10 @@
apply (auto simp add: hypreal_of_real_isUb_iff)
done
-lemma hypreal_of_real_isLub_iff: "(isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)) =
+lemma hypreal_of_real_isLub_iff:
+ "(isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)) =
(isLub (UNIV :: real set) Q Y)"
-apply (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2)
-done
+by (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2)
(* lemmas *)
lemma lemma_isUb_hypreal_of_real:
@@ -220,16 +223,17 @@
"\<exists>Yo. isLub Reals P (hypreal_of_real Yo) ==> \<exists>Y. isLub Reals P Y"
by (auto simp add: isLub_def leastP_def isUb_def)
-lemma SReal_complete: "[| P <= Reals; \<exists>x. x \<in> P; \<exists>Y. isUb Reals P Y |]
+lemma SReal_complete:
+ "[| P \<subseteq> Reals; \<exists>x. x \<in> P; \<exists>Y. isUb Reals P Y |]
==> \<exists>t::hypreal. isLub Reals P t"
apply (frule SReal_hypreal_of_real_image)
apply (auto, drule lemma_isUb_hypreal_of_real)
apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2 simp add: hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff)
done
-(*--------------------------------------------------------------------
- Set of finite elements is a subring of the extended reals
- --------------------------------------------------------------------*)
+
+subsection{* Set of Finite Elements is a Subring of the Extended Reals*}
+
lemma HFinite_add: "[|x \<in> HFinite; y \<in> HFinite|] ==> (x+y) \<in> HFinite"
apply (simp add: HFinite_def)
apply (blast intro!: SReal_add hrabs_add_less)
@@ -243,7 +247,7 @@
lemma HFinite_minus_iff: "(-x \<in> HFinite) = (x \<in> HFinite)"
by (simp add: HFinite_def)
-lemma SReal_subset_HFinite: "Reals <= HFinite"
+lemma SReal_subset_HFinite: "Reals \<subseteq> HFinite"
apply (auto simp add: SReal_def HFinite_def)
apply (rule_tac x = "1 + abs (hypreal_of_real r) " in exI)
apply (auto simp add: hypreal_of_real_hrabs)
@@ -278,21 +282,20 @@
done
declare HFinite_1 [simp]
-lemma HFinite_bounded: "[|x \<in> HFinite; y <= x; 0 <= y |] ==> y \<in> HFinite"
-apply (case_tac "x <= 0")
+lemma HFinite_bounded: "[|x \<in> HFinite; y \<le> x; 0 \<le> y |] ==> y \<in> HFinite"
+apply (case_tac "x \<le> 0")
apply (drule_tac y = x in order_trans)
apply (drule_tac [2] hypreal_le_anti_sym)
apply (auto simp add: linorder_not_le)
apply (auto intro: order_le_less_trans simp add: abs_if HFinite_def)
done
-(*------------------------------------------------------------------
- Set of infinitesimals is a subring of the hyperreals
- ------------------------------------------------------------------*)
+
+subsection{* Set of Infinitesimals is a Subring of the Hyperreals*}
+
lemma InfinitesimalD:
"x \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> abs x < r"
-apply (simp add: Infinitesimal_def)
-done
+by (simp add: Infinitesimal_def)
lemma Infinitesimal_zero: "0 \<in> Infinitesimal"
by (simp add: Infinitesimal_def)
@@ -316,7 +319,8 @@
by (simp add: Infinitesimal_def)
declare Infinitesimal_minus_iff [simp]
-lemma Infinitesimal_diff: "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
+lemma Infinitesimal_diff:
+ "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
by (simp add: hypreal_diff_def Infinitesimal_add)
lemma Infinitesimal_mult:
@@ -326,7 +330,8 @@
apply (cut_tac [2] a = "abs x" and b = 1 and c = "abs y" and d = r in mult_strict_mono, auto)
done
-lemma Infinitesimal_HFinite_mult: "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (x * y) \<in> Infinitesimal"
+lemma Infinitesimal_HFinite_mult:
+ "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (x * y) \<in> Infinitesimal"
apply (auto dest!: HFiniteD simp add: Infinitesimal_def)
apply (frule hrabs_less_gt_zero)
apply (drule_tac x = "r/t" in bspec)
@@ -337,7 +342,8 @@
apply (auto simp add: zero_less_divide_iff)
done
-lemma Infinitesimal_HFinite_mult2: "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (y * x) \<in> Infinitesimal"
+lemma Infinitesimal_HFinite_mult2:
+ "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (y * x) \<in> Infinitesimal"
by (auto dest: Infinitesimal_HFinite_mult simp add: hypreal_mult_commute)
(*** rather long proof ***)
@@ -351,8 +357,6 @@
apply (auto simp add: SReal_inverse)
done
-
-
lemma HInfinite_mult: "[|x \<in> HInfinite;y \<in> HInfinite|] ==> (x*y) \<in> HInfinite"
apply (simp add: HInfinite_def, auto)
apply (erule_tac x = 1 in ballE)
@@ -363,32 +367,36 @@
done
lemma HInfinite_add_ge_zero:
- "[|x \<in> HInfinite; 0 <= y; 0 <= x|] ==> (x + y): HInfinite"
+ "[|x \<in> HInfinite; 0 \<le> y; 0 \<le> x|] ==> (x + y): HInfinite"
by (auto intro!: hypreal_add_zero_less_le_mono
simp add: abs_if hypreal_add_commute hypreal_le_add_order HInfinite_def)
-lemma HInfinite_add_ge_zero2: "[|x \<in> HInfinite; 0 <= y; 0 <= x|] ==> (y + x): HInfinite"
+lemma HInfinite_add_ge_zero2:
+ "[|x \<in> HInfinite; 0 \<le> y; 0 \<le> x|] ==> (y + x): HInfinite"
by (auto intro!: HInfinite_add_ge_zero simp add: hypreal_add_commute)
-lemma HInfinite_add_gt_zero: "[|x \<in> HInfinite; 0 < y; 0 < x|] ==> (x + y): HInfinite"
+lemma HInfinite_add_gt_zero:
+ "[|x \<in> HInfinite; 0 < y; 0 < x|] ==> (x + y): HInfinite"
by (blast intro: HInfinite_add_ge_zero order_less_imp_le)
lemma HInfinite_minus_iff: "(-x \<in> HInfinite) = (x \<in> HInfinite)"
by (simp add: HInfinite_def)
-lemma HInfinite_add_le_zero: "[|x \<in> HInfinite; y <= 0; x <= 0|] ==> (x + y): HInfinite"
+lemma HInfinite_add_le_zero:
+ "[|x \<in> HInfinite; y \<le> 0; x \<le> 0|] ==> (x + y): HInfinite"
apply (drule HInfinite_minus_iff [THEN iffD2])
apply (rule HInfinite_minus_iff [THEN iffD1])
apply (auto intro: HInfinite_add_ge_zero)
done
-lemma HInfinite_add_lt_zero: "[|x \<in> HInfinite; y < 0; x < 0|] ==> (x + y): HInfinite"
+lemma HInfinite_add_lt_zero:
+ "[|x \<in> HInfinite; y < 0; x < 0|] ==> (x + y): HInfinite"
by (blast intro: HInfinite_add_le_zero order_less_imp_le)
-lemma HFinite_sum_squares: "[|a: HFinite; b: HFinite; c: HFinite|]
+lemma HFinite_sum_squares:
+ "[|a: HFinite; b: HFinite; c: HFinite|]
==> a*a + b*b + c*c \<in> HFinite"
-apply (auto intro: HFinite_mult HFinite_add)
-done
+by (auto intro: HFinite_mult HFinite_add)
lemma not_Infinitesimal_not_zero: "x \<notin> Infinitesimal ==> x \<noteq> 0"
by auto
@@ -400,27 +408,27 @@
by (auto simp add: hrabs_def)
declare Infinitesimal_hrabs_iff [iff]
-lemma HFinite_diff_Infinitesimal_hrabs: "x \<in> HFinite - Infinitesimal ==> abs x \<in> HFinite - Infinitesimal"
+lemma HFinite_diff_Infinitesimal_hrabs:
+ "x \<in> HFinite - Infinitesimal ==> abs x \<in> HFinite - Infinitesimal"
by blast
lemma hrabs_less_Infinitesimal:
"[| e \<in> Infinitesimal; abs x < e |] ==> x \<in> Infinitesimal"
-apply (auto simp add: Infinitesimal_def abs_less_iff)
-done
+by (auto simp add: Infinitesimal_def abs_less_iff)
-lemma hrabs_le_Infinitesimal: "[| e \<in> Infinitesimal; abs x <= e |] ==> x \<in> Infinitesimal"
+lemma hrabs_le_Infinitesimal:
+ "[| e \<in> Infinitesimal; abs x \<le> e |] ==> x \<in> Infinitesimal"
by (blast dest: order_le_imp_less_or_eq intro: hrabs_less_Infinitesimal)
lemma Infinitesimal_interval:
"[| e \<in> Infinitesimal; e' \<in> Infinitesimal; e' < x ; x < e |]
==> x \<in> Infinitesimal"
-apply (auto simp add: Infinitesimal_def abs_less_iff)
-done
+by (auto simp add: Infinitesimal_def abs_less_iff)
-lemma Infinitesimal_interval2: "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
- e' <= x ; x <= e |] ==> x \<in> Infinitesimal"
-apply (auto intro: Infinitesimal_interval simp add: order_le_less)
-done
+lemma Infinitesimal_interval2:
+ "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
+ e' \<le> x ; x \<le> e |] ==> x \<in> Infinitesimal"
+by (auto intro: Infinitesimal_interval simp add: order_le_less)
lemma not_Infinitesimal_mult:
"[| x \<notin> Infinitesimal; y \<notin> Infinitesimal|] ==> (x*y) \<notin>Infinitesimal"
@@ -432,7 +440,8 @@
apply (cut_tac c = ra and d = "abs y" and a = r and b = "abs x" in mult_mono, auto)
done
-lemma Infinitesimal_mult_disj: "x*y \<in> Infinitesimal ==> x \<in> Infinitesimal | y \<in> Infinitesimal"
+lemma Infinitesimal_mult_disj:
+ "x*y \<in> Infinitesimal ==> x \<in> Infinitesimal | y \<in> Infinitesimal"
apply (rule ccontr)
apply (drule de_Morgan_disj [THEN iffD1])
apply (fast dest: not_Infinitesimal_mult)
@@ -441,7 +450,8 @@
lemma HFinite_Infinitesimal_not_zero: "x \<in> HFinite-Infinitesimal ==> x \<noteq> 0"
by blast
-lemma HFinite_Infinitesimal_diff_mult: "[| x \<in> HFinite - Infinitesimal;
+lemma HFinite_Infinitesimal_diff_mult:
+ "[| x \<in> HFinite - Infinitesimal;
y \<in> HFinite - Infinitesimal
|] ==> (x*y) \<in> HFinite - Infinitesimal"
apply clarify
@@ -449,20 +459,21 @@
done
lemma Infinitesimal_subset_HFinite:
- "Infinitesimal <= HFinite"
+ "Infinitesimal \<subseteq> HFinite"
apply (simp add: Infinitesimal_def HFinite_def, auto)
apply (rule_tac x = 1 in bexI, auto)
done
-lemma Infinitesimal_hypreal_of_real_mult: "x \<in> Infinitesimal ==> x * hypreal_of_real r \<in> Infinitesimal"
+lemma Infinitesimal_hypreal_of_real_mult:
+ "x \<in> Infinitesimal ==> x * hypreal_of_real r \<in> Infinitesimal"
by (erule HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult])
-lemma Infinitesimal_hypreal_of_real_mult2: "x \<in> Infinitesimal ==> hypreal_of_real r * x \<in> Infinitesimal"
+lemma Infinitesimal_hypreal_of_real_mult2:
+ "x \<in> Infinitesimal ==> hypreal_of_real r * x \<in> Infinitesimal"
by (erule HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult2])
-(*----------------------------------------------------------------------
- Infinitely close relation @=
- ----------------------------------------------------------------------*)
+
+subsection{*The Infinitely Close Relation*}
lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x @= 0)"
by (simp add: Infinitesimal_def approx_def)
@@ -631,7 +642,8 @@
apply (auto dest: approx_sym elim!: approx_trans equalityCE)
done
-lemma Infinitesimal_approx: "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x @= y"
+lemma Infinitesimal_approx:
+ "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x @= y"
apply (simp add: mem_infmal_iff)
apply (blast intro: approx_trans approx_sym)
done
@@ -676,7 +688,8 @@
lemma approx_mult_subst2: "[| u @= x*v; x @= y; v \<in> HFinite |] ==> u @= y*v"
by (blast intro: approx_mult1 approx_trans)
-lemma approx_mult_subst_SReal: "[| u @= x*hypreal_of_real v; x @= y |] ==> u @= y*hypreal_of_real v"
+lemma approx_mult_subst_SReal:
+ "[| u @= x*hypreal_of_real v; x @= y |] ==> u @= y*hypreal_of_real v"
by (auto intro: approx_mult_subst2)
lemma approx_eq_imp: "a = b ==> a @= b"
@@ -715,7 +728,8 @@
apply (erule approx_trans3 [THEN approx_sym], assumption)
done
-lemma Infinitesimal_add_right_cancel: "[| y \<in> Infinitesimal; x @= z + y|] ==> x @= z"
+lemma Infinitesimal_add_right_cancel:
+ "[| y \<in> Infinitesimal; x @= z + y|] ==> x @= z"
apply (drule_tac x = z in Infinitesimal_add_approx_self2 [THEN approx_sym])
apply (erule approx_trans3 [THEN approx_sym])
apply (simp add: hypreal_add_commute)
@@ -762,19 +776,22 @@
lemma approx_hypreal_of_real_HFinite: "x @= hypreal_of_real D ==> x \<in> HFinite"
by (rule approx_sym [THEN [2] approx_HFinite], auto)
-lemma approx_mult_HFinite: "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d"
+lemma approx_mult_HFinite:
+ "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d"
apply (rule approx_trans)
apply (rule_tac [2] approx_mult2)
apply (rule approx_mult1)
prefer 2 apply (blast intro: approx_HFinite approx_sym, auto)
done
-lemma approx_mult_hypreal_of_real: "[|a @= hypreal_of_real b; c @= hypreal_of_real d |]
+lemma approx_mult_hypreal_of_real:
+ "[|a @= hypreal_of_real b; c @= hypreal_of_real d |]
==> a*c @= hypreal_of_real b*hypreal_of_real d"
apply (blast intro!: approx_mult_HFinite approx_hypreal_of_real_HFinite HFinite_hypreal_of_real)
done
-lemma approx_SReal_mult_cancel_zero: "[| a \<in> Reals; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
+lemma approx_SReal_mult_cancel_zero:
+ "[| a \<in> Reals; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
apply (drule SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
apply (auto dest: approx_mult2 simp add: hypreal_mult_assoc [symmetric])
done
@@ -786,20 +803,23 @@
lemma approx_mult_SReal2: "[| a \<in> Reals; x @= 0 |] ==> a*x @= 0"
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)
-lemma approx_mult_SReal_zero_cancel_iff: "[|a \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
+lemma approx_mult_SReal_zero_cancel_iff:
+ "[|a \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)
declare approx_mult_SReal_zero_cancel_iff [simp]
-lemma approx_SReal_mult_cancel: "[| a \<in> Reals; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
+lemma approx_SReal_mult_cancel:
+ "[| a \<in> Reals; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
apply (drule SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
apply (auto dest: approx_mult2 simp add: hypreal_mult_assoc [symmetric])
done
-lemma approx_SReal_mult_cancel_iff1: "[| a \<in> Reals; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
+lemma approx_SReal_mult_cancel_iff1:
+ "[| a \<in> Reals; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD] intro: approx_SReal_mult_cancel)
declare approx_SReal_mult_cancel_iff1 [simp]
-lemma approx_le_bound: "[| z <= f; f @= g; g <= z |] ==> f @= z"
+lemma approx_le_bound: "[| z \<le> f; f @= g; g \<le> z |] ==> f @= z"
apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto)
apply (rule_tac x = "g+y-z" in bexI)
apply (simp (no_asm))
@@ -807,9 +827,8 @@
apply (rule_tac [2] Infinitesimal_zero, auto)
done
-(*-----------------------------------------------------------------
- Zero is the only infinitesimal that is also a real
- -----------------------------------------------------------------*)
+
+subsection{* Zero is the Only Infinitesimal that is Also a Real*}
lemma Infinitesimal_less_SReal:
"[| x \<in> Reals; y \<in> Infinitesimal; 0 < x |] ==> y < x"
@@ -817,7 +836,8 @@
apply (rule abs_ge_self [THEN order_le_less_trans], auto)
done
-lemma Infinitesimal_less_SReal2: "y \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> y < r"
+lemma Infinitesimal_less_SReal2:
+ "y \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> y < r"
by (blast intro: Infinitesimal_less_SReal)
lemma SReal_not_Infinitesimal:
@@ -826,7 +846,8 @@
apply (auto simp add: hrabs_def)
done
-lemma SReal_minus_not_Infinitesimal: "[| y < 0; y \<in> Reals |] ==> y \<notin> Infinitesimal"
+lemma SReal_minus_not_Infinitesimal:
+ "[| y < 0; y \<in> Reals |] ==> y \<notin> Infinitesimal"
apply (subst Infinitesimal_minus_iff [symmetric])
apply (rule SReal_not_Infinitesimal, auto)
done
@@ -840,20 +861,24 @@
lemma SReal_Infinitesimal_zero: "[| x \<in> Reals; x \<in> Infinitesimal|] ==> x = 0"
by (cut_tac SReal_Int_Infinitesimal_zero, blast)
-lemma SReal_HFinite_diff_Infinitesimal: "[| x \<in> Reals; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal"
+lemma SReal_HFinite_diff_Infinitesimal:
+ "[| x \<in> Reals; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal"
by (auto dest: SReal_Infinitesimal_zero SReal_subset_HFinite [THEN subsetD])
-lemma hypreal_of_real_HFinite_diff_Infinitesimal: "hypreal_of_real x \<noteq> 0 ==> hypreal_of_real x \<in> HFinite - Infinitesimal"
+lemma hypreal_of_real_HFinite_diff_Infinitesimal:
+ "hypreal_of_real x \<noteq> 0 ==> hypreal_of_real x \<in> HFinite - Infinitesimal"
by (rule SReal_HFinite_diff_Infinitesimal, auto)
-lemma hypreal_of_real_Infinitesimal_iff_0: "(hypreal_of_real x \<in> Infinitesimal) = (x=0)"
+lemma hypreal_of_real_Infinitesimal_iff_0:
+ "(hypreal_of_real x \<in> Infinitesimal) = (x=0)"
apply auto
apply (rule ccontr)
apply (rule hypreal_of_real_HFinite_diff_Infinitesimal [THEN DiffD2], auto)
done
declare hypreal_of_real_Infinitesimal_iff_0 [iff]
-lemma number_of_not_Infinitesimal: "number_of w \<noteq> (0::hypreal) ==> number_of w \<notin> Infinitesimal"
+lemma number_of_not_Infinitesimal:
+ "number_of w \<noteq> (0::hypreal) ==> number_of w \<notin> Infinitesimal"
by (fast dest: SReal_number_of [THEN SReal_Infinitesimal_zero])
declare number_of_not_Infinitesimal [simp]
@@ -870,7 +895,8 @@
apply (blast dest: approx_sym [THEN mem_infmal_iff [THEN iffD2]] SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
done
-lemma HFinite_diff_Infinitesimal_approx: "[| x @= y; y \<in> HFinite - Infinitesimal |]
+lemma HFinite_diff_Infinitesimal_approx:
+ "[| x @= y; y \<in> HFinite - Infinitesimal |]
==> x \<in> HFinite - Infinitesimal"
apply (auto intro: approx_sym [THEN [2] approx_HFinite]
simp add: mem_infmal_iff)
@@ -880,18 +906,25 @@
(*The premise y\<noteq>0 is essential; otherwise x/y =0 and we lose the
HFinite premise.*)
-lemma Infinitesimal_ratio: "[| y \<noteq> 0; y \<in> Infinitesimal; x/y \<in> HFinite |] ==> x \<in> Infinitesimal"
+lemma Infinitesimal_ratio:
+ "[| y \<noteq> 0; y \<in> Infinitesimal; x/y \<in> HFinite |] ==> x \<in> Infinitesimal"
apply (drule Infinitesimal_HFinite_mult2, assumption)
apply (simp add: hypreal_divide_def hypreal_mult_assoc)
done
+lemma Infinitesimal_SReal_divide:
+ "[| x \<in> Infinitesimal; y \<in> Reals |] ==> x/y \<in> Infinitesimal"
+apply (simp add: divide_inverse_zero)
+apply (auto intro!: Infinitesimal_HFinite_mult
+ dest!: SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
+done
+
(*------------------------------------------------------------------
Standard Part Theorem: Every finite x: R* is infinitely
close to a unique real number (i.e a member of Reals)
------------------------------------------------------------------*)
-(*------------------------------------------------------------------
- Uniqueness: Two infinitely close reals are equal
- ------------------------------------------------------------------*)
+
+subsection{* Uniqueness: Two Infinitely Close Reals are Equal*}
lemma SReal_approx_iff: "[|x \<in> Reals; y \<in> Reals|] ==> (x @= y) = (x = y)"
apply auto
@@ -903,7 +936,8 @@
apply (simp add: hypreal_eq_minus_iff [symmetric])
done
-lemma number_of_approx_iff: "(number_of v @= number_of w) = (number_of v = (number_of w :: hypreal))"
+lemma number_of_approx_iff:
+ "(number_of v @= number_of w) = (number_of v = (number_of w :: hypreal))"
by (auto simp add: SReal_approx_iff)
declare number_of_approx_iff [simp]
@@ -915,14 +949,16 @@
"~ (0 @= 1)" "~ (1 @= 0)"
by (auto simp only: SReal_number_of SReal_approx_iff Reals_0 Reals_1)
-lemma hypreal_of_real_approx_iff: "(hypreal_of_real k @= hypreal_of_real m) = (k = m)"
+lemma hypreal_of_real_approx_iff:
+ "(hypreal_of_real k @= hypreal_of_real m) = (k = m)"
apply auto
apply (rule inj_hypreal_of_real [THEN injD])
apply (rule SReal_approx_iff [THEN iffD1], auto)
done
declare hypreal_of_real_approx_iff [simp]
-lemma hypreal_of_real_approx_number_of_iff: "(hypreal_of_real k @= number_of w) = (k = number_of w)"
+lemma hypreal_of_real_approx_number_of_iff:
+ "(hypreal_of_real k @= number_of w) = (k = number_of w)"
by (subst hypreal_of_real_approx_iff [symmetric], auto)
declare hypreal_of_real_approx_number_of_iff [simp]
@@ -932,12 +968,13 @@
"(hypreal_of_real k @= 1) = (k = 1)"
by (simp_all add: hypreal_of_real_approx_iff [symmetric])
-lemma approx_unique_real: "[| r \<in> Reals; s \<in> Reals; r @= x; s @= x|] ==> r = s"
+lemma approx_unique_real:
+ "[| r \<in> Reals; s \<in> Reals; r @= x; s @= x|] ==> r = s"
by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2)
-(*------------------------------------------------------------------
- Existence of unique real infinitely close
- ------------------------------------------------------------------*)
+
+subsection{* Existence of Unique Real Infinitely Close*}
+
(* lemma about lubs *)
lemma hypreal_isLub_unique:
"[| isLub R S x; isLub R S y |] ==> x = (y::hypreal)"
@@ -946,7 +983,8 @@
apply (blast intro!: hypreal_le_anti_sym dest!: isLub_le_isUb)
done
-lemma lemma_st_part_ub: "x \<in> HFinite ==> \<exists>u. isUb Reals {s. s \<in> Reals & s < x} u"
+lemma lemma_st_part_ub:
+ "x \<in> HFinite ==> \<exists>u. isUb Reals {s. s \<in> Reals & s < x} u"
apply (drule HFiniteD, safe)
apply (rule exI, rule isUbI)
apply (auto intro: setleI isUbI simp add: abs_less_iff)
@@ -959,28 +997,31 @@
apply (auto simp add: abs_less_iff)
done
-lemma lemma_st_part_subset: "{s. s \<in> Reals & s < x} <= Reals"
+lemma lemma_st_part_subset: "{s. s \<in> Reals & s < x} \<subseteq> Reals"
by auto
-lemma lemma_st_part_lub: "x \<in> HFinite ==> \<exists>t. isLub Reals {s. s \<in> Reals & s < x} t"
+lemma lemma_st_part_lub:
+ "x \<in> HFinite ==> \<exists>t. isLub Reals {s. s \<in> Reals & s < x} t"
by (blast intro!: SReal_complete lemma_st_part_ub lemma_st_part_nonempty lemma_st_part_subset)
-lemma lemma_hypreal_le_left_cancel: "((t::hypreal) + r <= t) = (r <= 0)"
+lemma lemma_hypreal_le_left_cancel: "((t::hypreal) + r \<le> t) = (r \<le> 0)"
apply safe
apply (drule_tac c = "-t" in add_left_mono)
apply (drule_tac [2] c = t in add_left_mono)
apply (auto simp add: hypreal_add_assoc [symmetric])
done
-lemma lemma_st_part_le1: "[| x \<in> HFinite; isLub Reals {s. s \<in> Reals & s < x} t;
- r \<in> Reals; 0 < r |] ==> x <= t + r"
+lemma lemma_st_part_le1:
+ "[| x \<in> HFinite; isLub Reals {s. s \<in> Reals & s < x} t;
+ r \<in> Reals; 0 < r |] ==> x \<le> t + r"
apply (frule isLubD1a)
apply (rule ccontr, drule linorder_not_le [THEN iffD2])
apply (drule_tac x = t in SReal_add, assumption)
apply (drule_tac y = "t + r" in isLubD1 [THEN setleD], auto)
done
-lemma hypreal_setle_less_trans: "!!x::hypreal. [| S *<= x; x < y |] ==> S *<= y"
+lemma hypreal_setle_less_trans:
+ "!!x::hypreal. [| S *<= x; x < y |] ==> S *<= y"
apply (simp add: setle_def)
apply (auto dest!: bspec order_le_less_trans intro: order_less_imp_le)
done
@@ -991,20 +1032,21 @@
apply (blast intro: hypreal_setle_less_trans)
done
-lemma lemma_st_part_gt_ub: "[| x \<in> HFinite; x < y; y \<in> Reals |]
- ==> isUb Reals {s. s \<in> Reals & s < x} y"
-apply (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI)
-done
+lemma lemma_st_part_gt_ub:
+ "[| x \<in> HFinite; x < y; y \<in> Reals |]
+ ==> isUb Reals {s. s \<in> Reals & s < x} y"
+by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI)
-lemma lemma_minus_le_zero: "t <= t + -r ==> r <= (0::hypreal)"
+lemma lemma_minus_le_zero: "t \<le> t + -r ==> r \<le> (0::hypreal)"
apply (drule_tac c = "-t" in add_left_mono)
apply (auto simp add: hypreal_add_assoc [symmetric])
done
-lemma lemma_st_part_le2: "[| x \<in> HFinite;
+lemma lemma_st_part_le2:
+ "[| x \<in> HFinite;
isLub Reals {s. s \<in> Reals & s < x} t;
r \<in> Reals; 0 < r |]
- ==> t + -r <= x"
+ ==> t + -r \<le> x"
apply (frule isLubD1a)
apply (rule ccontr, drule linorder_not_le [THEN iffD1])
apply (drule SReal_minus, drule_tac x = t in SReal_add, assumption)
@@ -1014,30 +1056,33 @@
apply (auto dest: order_less_le_trans)
done
-lemma lemma_hypreal_le_swap: "((x::hypreal) <= t + r) = (x + -t <= r)"
+lemma lemma_hypreal_le_swap: "((x::hypreal) \<le> t + r) = (x + -t \<le> r)"
by auto
-lemma lemma_st_part1a: "[| x \<in> HFinite;
+lemma lemma_st_part1a:
+ "[| x \<in> HFinite;
isLub Reals {s. s \<in> Reals & s < x} t;
r \<in> Reals; 0 < r |]
- ==> x + -t <= r"
-apply (blast intro!: lemma_hypreal_le_swap [THEN iffD1] lemma_st_part_le1)
-done
+ ==> x + -t \<le> r"
+by (blast intro!: lemma_hypreal_le_swap [THEN iffD1] lemma_st_part_le1)
-lemma lemma_hypreal_le_swap2: "(t + -r <= x) = (-(x + -t) <= (r::hypreal))"
+lemma lemma_hypreal_le_swap2: "(t + -r \<le> x) = (-(x + -t) \<le> (r::hypreal))"
by auto
-lemma lemma_st_part2a: "[| x \<in> HFinite;
+lemma lemma_st_part2a:
+ "[| x \<in> HFinite;
isLub Reals {s. s \<in> Reals & s < x} t;
r \<in> Reals; 0 < r |]
- ==> -(x + -t) <= r"
+ ==> -(x + -t) \<le> r"
apply (blast intro!: lemma_hypreal_le_swap2 [THEN iffD1] lemma_st_part_le2)
done
-lemma lemma_SReal_ub: "(x::hypreal) \<in> Reals ==> isUb Reals {s. s \<in> Reals & s < x} x"
+lemma lemma_SReal_ub:
+ "(x::hypreal) \<in> Reals ==> isUb Reals {s. s \<in> Reals & s < x} x"
by (auto intro: isUbI setleI order_less_imp_le)
-lemma lemma_SReal_lub: "(x::hypreal) \<in> Reals ==> isLub Reals {s. s \<in> Reals & s < x} x"
+lemma lemma_SReal_lub:
+ "(x::hypreal) \<in> Reals ==> isLub Reals {s. s \<in> Reals & s < x} x"
apply (auto intro!: isLubI2 lemma_SReal_ub setgeI)
apply (frule isUbD2a)
apply (rule_tac x = x and y = y in linorder_cases)
@@ -1047,7 +1092,8 @@
apply (auto dest: order_less_le_trans)
done
-lemma lemma_st_part_not_eq1: "[| x \<in> HFinite;
+lemma lemma_st_part_not_eq1:
+ "[| x \<in> HFinite;
isLub Reals {s. s \<in> Reals & s < x} t;
r \<in> Reals; 0 < r |]
==> x + -t \<noteq> r"
@@ -1058,7 +1104,8 @@
apply (drule hypreal_isLub_unique, assumption, auto)
done
-lemma lemma_st_part_not_eq2: "[| x \<in> HFinite;
+lemma lemma_st_part_not_eq2:
+ "[| x \<in> HFinite;
isLub Reals {s. s \<in> Reals & s < x} t;
r \<in> Reals; 0 < r |]
==> -(x + -t) \<noteq> r"
@@ -1070,7 +1117,8 @@
apply (drule hypreal_isLub_unique, assumption, auto)
done
-lemma lemma_st_part_major: "[| x \<in> HFinite;
+lemma lemma_st_part_major:
+ "[| x \<in> HFinite;
isLub Reals {s. s \<in> Reals & s < x} t;
r \<in> Reals; 0 < r |]
==> abs (x + -t) < r"
@@ -1080,17 +1128,16 @@
apply (auto dest: lemma_st_part_not_eq1 lemma_st_part_not_eq2 simp add: abs_less_iff)
done
-lemma lemma_st_part_major2: "[| x \<in> HFinite;
- isLub Reals {s. s \<in> Reals & s < x} t |]
+lemma lemma_st_part_major2:
+ "[| x \<in> HFinite; isLub Reals {s. s \<in> Reals & s < x} t |]
==> \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"
-apply (blast dest!: lemma_st_part_major)
-done
+by (blast dest!: lemma_st_part_major)
(*----------------------------------------------
Existence of real and Standard Part Theorem
----------------------------------------------*)
-lemma lemma_st_part_Ex: "x \<in> HFinite ==>
- \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"
+lemma lemma_st_part_Ex:
+ "x \<in> HFinite ==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"
apply (frule lemma_st_part_lub, safe)
apply (frule isLubD1a)
apply (blast dest: lemma_st_part_major2)
@@ -1111,9 +1158,7 @@
apply (auto intro!: approx_unique_real)
done
-(*------------------------------------------------------------------
- Finite and Infinite --- more theorems
- ------------------------------------------------------------------*)
+subsection{* Finite, Infinite and Infinitesimal*}
lemma HFinite_Int_HInfinite_empty: "HFinite Int HInfinite = {}"
@@ -1143,17 +1188,15 @@
by (blast dest: HFinite_not_HInfinite not_HFinite_HInfinite)
lemma HFinite_HInfinite_iff: "(x \<in> HFinite) = (x \<notin> HInfinite)"
-apply (simp (no_asm) add: HInfinite_HFinite_iff)
-done
+by (simp add: HInfinite_HFinite_iff)
+
-(*------------------------------------------------------------------
- Finite, Infinite and Infinitesimal --- more theorems
- ------------------------------------------------------------------*)
-
-lemma HInfinite_diff_HFinite_Infinitesimal_disj: "x \<notin> Infinitesimal ==> x \<in> HInfinite | x \<in> HFinite - Infinitesimal"
+lemma HInfinite_diff_HFinite_Infinitesimal_disj:
+ "x \<notin> Infinitesimal ==> x \<in> HInfinite | x \<in> HFinite - Infinitesimal"
by (fast intro: not_HFinite_HInfinite)
-lemma HFinite_inverse: "[| x \<in> HFinite; x \<notin> Infinitesimal |] ==> inverse x \<in> HFinite"
+lemma HFinite_inverse:
+ "[| x \<in> HFinite; x \<notin> Infinitesimal |] ==> inverse x \<in> HFinite"
apply (cut_tac x = "inverse x" in HInfinite_HFinite_disj)
apply (auto dest!: HInfinite_inverse_Infinitesimal)
done
@@ -1162,18 +1205,21 @@
by (blast intro: HFinite_inverse)
(* stronger statement possible in fact *)
-lemma Infinitesimal_inverse_HFinite: "x \<notin> Infinitesimal ==> inverse(x) \<in> HFinite"
+lemma Infinitesimal_inverse_HFinite:
+ "x \<notin> Infinitesimal ==> inverse(x) \<in> HFinite"
apply (drule HInfinite_diff_HFinite_Infinitesimal_disj)
apply (blast intro: HFinite_inverse HInfinite_inverse_Infinitesimal Infinitesimal_subset_HFinite [THEN subsetD])
done
-lemma HFinite_not_Infinitesimal_inverse: "x \<in> HFinite - Infinitesimal ==> inverse x \<in> HFinite - Infinitesimal"
+lemma HFinite_not_Infinitesimal_inverse:
+ "x \<in> HFinite - Infinitesimal ==> inverse x \<in> HFinite - Infinitesimal"
apply (auto intro: Infinitesimal_inverse_HFinite)
apply (drule Infinitesimal_HFinite_mult2, assumption)
apply (simp add: not_Infinitesimal_not_zero hypreal_mult_inverse)
done
-lemma approx_inverse: "[| x @= y; y \<in> HFinite - Infinitesimal |]
+lemma approx_inverse:
+ "[| x @= y; y \<in> HFinite - Infinitesimal |]
==> inverse x @= inverse y"
apply (frule HFinite_diff_Infinitesimal_approx, assumption)
apply (frule not_Infinitesimal_not_zero2)
@@ -1187,18 +1233,21 @@
(*Used for NSLIM_inverse, NSLIMSEQ_inverse*)
lemmas hypreal_of_real_approx_inverse = hypreal_of_real_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
-lemma inverse_add_Infinitesimal_approx: "[| x \<in> HFinite - Infinitesimal;
+lemma inverse_add_Infinitesimal_approx:
+ "[| x \<in> HFinite - Infinitesimal;
h \<in> Infinitesimal |] ==> inverse(x + h) @= inverse x"
apply (auto intro: approx_inverse approx_sym Infinitesimal_add_approx_self)
done
-lemma inverse_add_Infinitesimal_approx2: "[| x \<in> HFinite - Infinitesimal;
+lemma inverse_add_Infinitesimal_approx2:
+ "[| x \<in> HFinite - Infinitesimal;
h \<in> Infinitesimal |] ==> inverse(h + x) @= inverse x"
apply (rule hypreal_add_commute [THEN subst])
apply (blast intro: inverse_add_Infinitesimal_approx)
done
-lemma inverse_add_Infinitesimal_approx_Infinitesimal: "[| x \<in> HFinite - Infinitesimal;
+lemma inverse_add_Infinitesimal_approx_Infinitesimal:
+ "[| x \<in> HFinite - Infinitesimal;
h \<in> Infinitesimal |] ==> inverse(x + h) + -inverse x @= h"
apply (rule approx_trans2)
apply (auto intro: inverse_add_Infinitesimal_approx simp add: mem_infmal_iff approx_minus_iff [symmetric])
@@ -1222,36 +1271,43 @@
by (auto simp add: HInfinite_HFinite_iff)
declare HInfinite_square_iff [simp]
-lemma approx_HFinite_mult_cancel: "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z"
+lemma approx_HFinite_mult_cancel:
+ "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z"
apply safe
apply (frule HFinite_inverse, assumption)
apply (drule not_Infinitesimal_not_zero)
apply (auto dest: approx_mult2 simp add: hypreal_mult_assoc [symmetric])
done
-lemma approx_HFinite_mult_cancel_iff1: "a: HFinite-Infinitesimal ==> (a * w @= a * z) = (w @= z)"
+lemma approx_HFinite_mult_cancel_iff1:
+ "a: HFinite-Infinitesimal ==> (a * w @= a * z) = (w @= z)"
by (auto intro: approx_mult2 approx_HFinite_mult_cancel)
-lemma HInfinite_HFinite_add_cancel: "[| x + y \<in> HInfinite; y \<in> HFinite |] ==> x \<in> HInfinite"
+lemma HInfinite_HFinite_add_cancel:
+ "[| x + y \<in> HInfinite; y \<in> HFinite |] ==> x \<in> HInfinite"
apply (rule ccontr)
apply (drule HFinite_HInfinite_iff [THEN iffD2])
apply (auto dest: HFinite_add simp add: HInfinite_HFinite_iff)
done
-lemma HInfinite_HFinite_add: "[| x \<in> HInfinite; y \<in> HFinite |] ==> x + y \<in> HInfinite"
+lemma HInfinite_HFinite_add:
+ "[| x \<in> HInfinite; y \<in> HFinite |] ==> x + y \<in> HInfinite"
apply (rule_tac y = "-y" in HInfinite_HFinite_add_cancel)
apply (auto simp add: hypreal_add_assoc HFinite_minus_iff)
done
-lemma HInfinite_ge_HInfinite: "[| x \<in> HInfinite; x <= y; 0 <= x |] ==> y \<in> HInfinite"
+lemma HInfinite_ge_HInfinite:
+ "[| x \<in> HInfinite; x \<le> y; 0 \<le> x |] ==> y \<in> HInfinite"
by (auto intro: HFinite_bounded simp add: HInfinite_HFinite_iff)
-lemma Infinitesimal_inverse_HInfinite: "[| x \<in> Infinitesimal; x \<noteq> 0 |] ==> inverse x \<in> HInfinite"
+lemma Infinitesimal_inverse_HInfinite:
+ "[| x \<in> Infinitesimal; x \<noteq> 0 |] ==> inverse x \<in> HInfinite"
apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
apply (auto dest: Infinitesimal_HFinite_mult2)
done
-lemma HInfinite_HFinite_not_Infinitesimal_mult: "[| x \<in> HInfinite; y \<in> HFinite - Infinitesimal |]
+lemma HInfinite_HFinite_not_Infinitesimal_mult:
+ "[| x \<in> HInfinite; y \<in> HFinite - Infinitesimal |]
==> x * y \<in> HInfinite"
apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
apply (frule HFinite_Infinitesimal_not_zero)
@@ -1260,10 +1316,10 @@
apply (auto simp add: hypreal_mult_assoc HFinite_HInfinite_iff)
done
-lemma HInfinite_HFinite_not_Infinitesimal_mult2: "[| x \<in> HInfinite; y \<in> HFinite - Infinitesimal |]
+lemma HInfinite_HFinite_not_Infinitesimal_mult2:
+ "[| x \<in> HInfinite; y \<in> HFinite - Infinitesimal |]
==> y * x \<in> HInfinite"
-apply (auto simp add: hypreal_mult_commute HInfinite_HFinite_not_Infinitesimal_mult)
-done
+by (auto simp add: hypreal_mult_commute HInfinite_HFinite_not_Infinitesimal_mult)
lemma HInfinite_gt_SReal: "[| x \<in> HInfinite; 0 < x; y \<in> Reals |] ==> y < x"
by (auto dest!: bspec simp add: HInfinite_def hrabs_def order_less_imp_le)
@@ -1277,18 +1333,13 @@
done
declare not_HInfinite_one [simp]
-(*------------------------------------------------------------------
- more about absolute value (hrabs)
- ------------------------------------------------------------------*)
-
lemma approx_hrabs_disj: "abs x @= x | abs x @= -x"
by (cut_tac x = x in hrabs_disj, auto)
-(*------------------------------------------------------------------
- Theorems about monads
- ------------------------------------------------------------------*)
-lemma monad_hrabs_Un_subset: "monad (abs x) <= monad(x) Un monad(-x)"
+subsection{*Theorems about Monads*}
+
+lemma monad_hrabs_Un_subset: "monad (abs x) \<le> monad(x) Un monad(-x)"
by (rule_tac x1 = x in hrabs_disj [THEN disjE], auto)
lemma Infinitesimal_monad_eq: "e \<in> Infinitesimal ==> monad (x+e) = monad x"
@@ -1316,12 +1367,12 @@
(*------------------------------------------------------------------
Proof that x @= y ==> abs x @= abs y
------------------------------------------------------------------*)
-lemma approx_subset_monad: "x @= y ==> {x,y}<=monad x"
+lemma approx_subset_monad: "x @= y ==> {x,y}\<le>monad x"
apply (simp (no_asm))
apply (simp add: approx_monad_iff)
done
-lemma approx_subset_monad2: "x @= y ==> {x,y}<=monad y"
+lemma approx_subset_monad2: "x @= y ==> {x,y}\<le>monad y"
apply (drule approx_sym)
apply (fast dest: approx_subset_monad)
done
@@ -1342,42 +1393,50 @@
apply (fast intro: approx_mem_monad approx_trans)
done
-lemma Infinitesimal_approx_hrabs: "[| x @= y; x \<in> Infinitesimal |] ==> abs x @= abs y"
+lemma Infinitesimal_approx_hrabs:
+ "[| x @= y; x \<in> Infinitesimal |] ==> abs x @= abs y"
apply (drule Infinitesimal_monad_zero_iff [THEN iffD1])
apply (blast intro: approx_mem_monad_zero monad_zero_hrabs_iff [THEN iffD1] mem_monad_approx approx_trans3)
done
-lemma less_Infinitesimal_less: "[| 0 < x; x \<notin>Infinitesimal; e :Infinitesimal |] ==> e < x"
+lemma less_Infinitesimal_less:
+ "[| 0 < x; x \<notin>Infinitesimal; e :Infinitesimal |] ==> e < x"
apply (rule ccontr)
apply (auto intro: Infinitesimal_zero [THEN [2] Infinitesimal_interval]
dest!: order_le_imp_less_or_eq simp add: linorder_not_less)
done
-lemma Ball_mem_monad_gt_zero: "[| 0 < x; x \<notin> Infinitesimal; u \<in> monad x |] ==> 0 < u"
+lemma Ball_mem_monad_gt_zero:
+ "[| 0 < x; x \<notin> Infinitesimal; u \<in> monad x |] ==> 0 < u"
apply (drule mem_monad_approx [THEN approx_sym])
apply (erule bex_Infinitesimal_iff2 [THEN iffD2, THEN bexE])
apply (drule_tac e = "-xa" in less_Infinitesimal_less, auto)
done
-lemma Ball_mem_monad_less_zero: "[| x < 0; x \<notin> Infinitesimal; u \<in> monad x |] ==> u < 0"
+lemma Ball_mem_monad_less_zero:
+ "[| x < 0; x \<notin> Infinitesimal; u \<in> monad x |] ==> u < 0"
apply (drule mem_monad_approx [THEN approx_sym])
apply (erule bex_Infinitesimal_iff [THEN iffD2, THEN bexE])
apply (cut_tac x = "-x" and e = xa in less_Infinitesimal_less, auto)
done
-lemma lemma_approx_gt_zero: "[|0 < x; x \<notin> Infinitesimal; x @= y|] ==> 0 < y"
+lemma lemma_approx_gt_zero:
+ "[|0 < x; x \<notin> Infinitesimal; x @= y|] ==> 0 < y"
by (blast dest: Ball_mem_monad_gt_zero approx_subset_monad)
-lemma lemma_approx_less_zero: "[|x < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0"
+lemma lemma_approx_less_zero:
+ "[|x < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0"
by (blast dest: Ball_mem_monad_less_zero approx_subset_monad)
-lemma approx_hrabs1: "[| x @= y; x < 0; x \<notin> Infinitesimal |] ==> abs x @= abs y"
+lemma approx_hrabs1:
+ "[| x @= y; x < 0; x \<notin> Infinitesimal |] ==> abs x @= abs y"
apply (frule lemma_approx_less_zero)
apply (assumption+)
apply (simp add: abs_if)
done
-lemma approx_hrabs2: "[| x @= y; 0 < x; x \<notin> Infinitesimal |] ==> abs x @= abs y"
+lemma approx_hrabs2:
+ "[| x @= y; 0 < x; x \<notin> Infinitesimal |] ==> abs x @= abs y"
apply (frule lemma_approx_gt_zero)
apply (assumption+)
apply (simp add: abs_if)
@@ -1397,17 +1456,20 @@
lemma approx_hrabs_add_Infinitesimal: "e \<in> Infinitesimal ==> abs x @= abs(x+e)"
by (fast intro: approx_hrabs Infinitesimal_add_approx_self)
-lemma approx_hrabs_add_minus_Infinitesimal: "e \<in> Infinitesimal ==> abs x @= abs(x + -e)"
+lemma approx_hrabs_add_minus_Infinitesimal:
+ "e \<in> Infinitesimal ==> abs x @= abs(x + -e)"
by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self)
-lemma hrabs_add_Infinitesimal_cancel: "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
+lemma hrabs_add_Infinitesimal_cancel:
+ "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
abs(x+e) = abs(y+e')|] ==> abs x @= abs y"
apply (drule_tac x = x in approx_hrabs_add_Infinitesimal)
apply (drule_tac x = y in approx_hrabs_add_Infinitesimal)
apply (auto intro: approx_trans2)
done
-lemma hrabs_add_minus_Infinitesimal_cancel: "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
+lemma hrabs_add_minus_Infinitesimal_cancel:
+ "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
abs(x + -e) = abs(y + -e')|] ==> abs x @= abs y"
apply (drule_tac x = x in approx_hrabs_add_minus_Infinitesimal)
apply (drule_tac x = y in approx_hrabs_add_minus_Infinitesimal)
@@ -1424,8 +1486,7 @@
"[| x < y; u \<in> Infinitesimal |]
==> hypreal_of_real x + u < hypreal_of_real y"
apply (simp add: Infinitesimal_def)
-apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec)
- apply (simp add: );
+apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp)
apply (auto simp add: add_commute abs_less_iff SReal_add SReal_minus)
apply (simp add: compare_rls)
done
@@ -1438,39 +1499,45 @@
apply (auto intro!: Infinitesimal_add_hypreal_of_real_less simp add: hypreal_of_real_hrabs)
done
-lemma Infinitesimal_add_hrabs_hypreal_of_real_less2: "[| x \<in> Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |]
+lemma Infinitesimal_add_hrabs_hypreal_of_real_less2:
+ "[| x \<in> Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |]
==> abs (x + hypreal_of_real r) < hypreal_of_real y"
apply (rule hypreal_add_commute [THEN subst])
apply (erule Infinitesimal_add_hrabs_hypreal_of_real_less, assumption)
done
-lemma hypreal_of_real_le_add_Infininitesimal_cancel: "[| u \<in> Infinitesimal; v \<in> Infinitesimal;
- hypreal_of_real x + u <= hypreal_of_real y + v |]
- ==> hypreal_of_real x <= hypreal_of_real y"
+lemma hypreal_of_real_le_add_Infininitesimal_cancel:
+ "[| u \<in> Infinitesimal; v \<in> Infinitesimal;
+ hypreal_of_real x + u \<le> hypreal_of_real y + v |]
+ ==> hypreal_of_real x \<le> hypreal_of_real y"
apply (simp add: linorder_not_less [symmetric], auto)
apply (drule_tac u = "v-u" in Infinitesimal_add_hypreal_of_real_less)
apply (auto simp add: Infinitesimal_diff)
done
-lemma hypreal_of_real_le_add_Infininitesimal_cancel2: "[| u \<in> Infinitesimal; v \<in> Infinitesimal;
- hypreal_of_real x + u <= hypreal_of_real y + v |]
- ==> x <= y"
+lemma hypreal_of_real_le_add_Infininitesimal_cancel2:
+ "[| u \<in> Infinitesimal; v \<in> Infinitesimal;
+ hypreal_of_real x + u \<le> hypreal_of_real y + v |]
+ ==> x \<le> y"
apply (blast intro!: hypreal_of_real_le_iff [THEN iffD1] hypreal_of_real_le_add_Infininitesimal_cancel)
done
-lemma hypreal_of_real_less_Infinitesimal_le_zero: "[| hypreal_of_real x < e; e \<in> Infinitesimal |] ==> hypreal_of_real x <= 0"
+lemma hypreal_of_real_less_Infinitesimal_le_zero:
+ "[| hypreal_of_real x < e; e \<in> Infinitesimal |] ==> hypreal_of_real x \<le> 0"
apply (rule linorder_not_less [THEN iffD1], safe)
apply (drule Infinitesimal_interval)
apply (drule_tac [4] SReal_hypreal_of_real [THEN SReal_Infinitesimal_zero], auto)
done
(*used once, in Lim/NSDERIV_inverse*)
-lemma Infinitesimal_add_not_zero: "[| h \<in> Infinitesimal; x \<noteq> 0 |] ==> hypreal_of_real x + h \<noteq> 0"
+lemma Infinitesimal_add_not_zero:
+ "[| h \<in> Infinitesimal; x \<noteq> 0 |] ==> hypreal_of_real x + h \<noteq> 0"
apply auto
apply (subgoal_tac "h = - hypreal_of_real x", auto)
done
-lemma Infinitesimal_square_cancel: "x*x + y*y \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
+lemma Infinitesimal_square_cancel:
+ "x*x + y*y \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
apply (rule Infinitesimal_interval2)
apply (rule_tac [3] zero_le_square, assumption)
apply (auto simp add: zero_le_square)
@@ -1483,7 +1550,8 @@
done
declare HFinite_square_cancel [simp]
-lemma Infinitesimal_square_cancel2: "x*x + y*y \<in> Infinitesimal ==> y*y \<in> Infinitesimal"
+lemma Infinitesimal_square_cancel2:
+ "x*x + y*y \<in> Infinitesimal ==> y*y \<in> Infinitesimal"
apply (rule Infinitesimal_square_cancel)
apply (rule hypreal_add_commute [THEN subst])
apply (simp (no_asm))
@@ -1497,7 +1565,8 @@
done
declare HFinite_square_cancel2 [simp]
-lemma Infinitesimal_sum_square_cancel: "x*x + y*y + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
+lemma Infinitesimal_sum_square_cancel:
+ "x*x + y*y + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
apply (rule Infinitesimal_interval2, assumption)
apply (rule_tac [2] zero_le_square, simp)
apply (insert zero_le_square [of y])
@@ -1513,25 +1582,29 @@
done
declare HFinite_sum_square_cancel [simp]
-lemma Infinitesimal_sum_square_cancel2: "y*y + x*x + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
+lemma Infinitesimal_sum_square_cancel2:
+ "y*y + x*x + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
apply (rule Infinitesimal_sum_square_cancel)
apply (simp add: add_ac)
done
declare Infinitesimal_sum_square_cancel2 [simp]
-lemma HFinite_sum_square_cancel2: "y*y + x*x + z*z \<in> HFinite ==> x*x \<in> HFinite"
+lemma HFinite_sum_square_cancel2:
+ "y*y + x*x + z*z \<in> HFinite ==> x*x \<in> HFinite"
apply (rule HFinite_sum_square_cancel)
apply (simp add: add_ac)
done
declare HFinite_sum_square_cancel2 [simp]
-lemma Infinitesimal_sum_square_cancel3: "z*z + y*y + x*x \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
+lemma Infinitesimal_sum_square_cancel3:
+ "z*z + y*y + x*x \<in> Infinitesimal ==> x*x \<in> Infinitesimal"
apply (rule Infinitesimal_sum_square_cancel)
apply (simp add: add_ac)
done
declare Infinitesimal_sum_square_cancel3 [simp]
-lemma HFinite_sum_square_cancel3: "z*z + y*y + x*x \<in> HFinite ==> x*x \<in> HFinite"
+lemma HFinite_sum_square_cancel3:
+ "z*z + y*y + x*x \<in> HFinite ==> x*x \<in> HFinite"
apply (rule HFinite_sum_square_cancel)
apply (simp add: add_ac)
done
@@ -1544,16 +1617,16 @@
apply (auto dest!: InfinitesimalD)
done
-lemma mem_monad_SReal_HFinite: "x \<in> monad (hypreal_of_real a) ==> x \<in> HFinite"
+lemma mem_monad_SReal_HFinite:
+ "x \<in> monad (hypreal_of_real a) ==> x \<in> HFinite"
apply (drule mem_monad_approx [THEN approx_sym])
apply (drule bex_Infinitesimal_iff2 [THEN iffD2])
apply (safe dest!: Infinitesimal_subset_HFinite [THEN subsetD])
apply (erule SReal_hypreal_of_real [THEN SReal_subset_HFinite [THEN subsetD], THEN HFinite_add])
done
-(*------------------------------------------------------------------
- Theorems about standard part
- ------------------------------------------------------------------*)
+
+subsection{* Theorems about Standard Part*}
lemma st_approx_self: "x \<in> HFinite ==> st x @= x"
apply (simp add: st_def)
@@ -1596,11 +1669,13 @@
by (fast elim: approx_trans approx_trans2 SReal_approx_iff [THEN iffD1])
qed
-lemma st_eq_approx_iff: "[| x \<in> HFinite; y \<in> HFinite|]
+lemma st_eq_approx_iff:
+ "[| x \<in> HFinite; y \<in> HFinite|]
==> (x @= y) = (st x = st y)"
by (blast intro: approx_st_eq st_eq_approx)
-lemma st_Infinitesimal_add_SReal: "[| x \<in> Reals; e \<in> Infinitesimal |] ==> st(x + e) = x"
+lemma st_Infinitesimal_add_SReal:
+ "[| x \<in> Reals; e \<in> Infinitesimal |] ==> st(x + e) = x"
apply (frule st_SReal_eq [THEN subst])
prefer 2 apply assumption
apply (frule SReal_subset_HFinite [THEN subsetD])
@@ -1610,16 +1685,15 @@
apply (auto intro: HFinite_add simp add: Infinitesimal_add_approx_self [THEN approx_sym])
done
-lemma st_Infinitesimal_add_SReal2: "[| x \<in> Reals; e \<in> Infinitesimal |]
- ==> st(e + x) = x"
+lemma st_Infinitesimal_add_SReal2:
+ "[| x \<in> Reals; e \<in> Infinitesimal |] ==> st(e + x) = x"
apply (rule hypreal_add_commute [THEN subst])
apply (blast intro!: st_Infinitesimal_add_SReal)
done
-lemma HFinite_st_Infinitesimal_add: "x \<in> HFinite ==>
- \<exists>e \<in> Infinitesimal. x = st(x) + e"
-apply (blast dest!: st_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2])
-done
+lemma HFinite_st_Infinitesimal_add:
+ "x \<in> HFinite ==> \<exists>e \<in> Infinitesimal. x = st(x) + e"
+by (blast dest!: st_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2])
lemma st_add:
assumes x: "x \<in> HFinite" and y: "y \<in> HFinite"
@@ -1655,8 +1729,7 @@
thus ?thesis by arith
qed
-lemma st_diff:
- "[| x \<in> HFinite; y \<in> HFinite |] ==> st (x-y) = st(x) - st(y)"
+lemma st_diff: "[| x \<in> HFinite; y \<in> HFinite |] ==> st (x-y) = st(x) - st(y)"
apply (simp add: hypreal_diff_def)
apply (frule_tac y1 = y in st_minus [symmetric])
apply (drule_tac x1 = y in HFinite_minus_iff [THEN iffD2])
@@ -1664,18 +1737,16 @@
done
(* lemma *)
-lemma lemma_st_mult: "[| x \<in> HFinite; y \<in> HFinite;
- e \<in> Infinitesimal;
- ea \<in> Infinitesimal |]
- ==> e*y + x*ea + e*ea \<in> Infinitesimal"
+lemma lemma_st_mult:
+ "[| x \<in> HFinite; y \<in> HFinite; e \<in> Infinitesimal; ea \<in> Infinitesimal |]
+ ==> e*y + x*ea + e*ea \<in> Infinitesimal"
apply (frule_tac x = e and y = y in Infinitesimal_HFinite_mult)
apply (frule_tac [2] x = ea and y = x in Infinitesimal_HFinite_mult)
apply (drule_tac [3] Infinitesimal_mult)
apply (auto intro: Infinitesimal_add simp add: add_ac mult_ac)
done
-lemma st_mult: "[| x \<in> HFinite; y \<in> HFinite |]
- ==> st (x * y) = st(x) * st(y)"
+lemma st_mult: "[| x \<in> HFinite; y \<in> HFinite |] ==> st (x * y) = st(x) * st(y)"
apply (frule HFinite_st_Infinitesimal_add)
apply (frule_tac x = y in HFinite_st_Infinitesimal_add, safe)
apply (subgoal_tac "st (x * y) = st ((st x + e) * (st y + ea))")
@@ -1697,20 +1768,23 @@
apply (subst numeral_0_eq_0 [symmetric])
apply (rule st_number_of [THEN subst])
apply (rule approx_st_eq)
-apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mem_infmal_iff [symmetric])
+apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
+ simp add: mem_infmal_iff [symmetric])
done
lemma st_not_Infinitesimal: "st(x) \<noteq> 0 ==> x \<notin> Infinitesimal"
by (fast intro: st_Infinitesimal)
-lemma st_inverse: "[| x \<in> HFinite; st x \<noteq> 0 |]
+lemma st_inverse:
+ "[| x \<in> HFinite; st x \<noteq> 0 |]
==> st(inverse x) = inverse (st x)"
apply (rule_tac c1 = "st x" in hypreal_mult_left_cancel [THEN iffD1])
apply (auto simp add: st_mult [symmetric] st_not_Infinitesimal HFinite_inverse)
apply (subst hypreal_mult_inverse, auto)
done
-lemma st_divide: "[| x \<in> HFinite; y \<in> HFinite; st y \<noteq> 0 |]
+lemma st_divide:
+ "[| x \<in> HFinite; y \<in> HFinite; st y \<noteq> 0 |]
==> st(x/y) = (st x) / (st y)"
apply (auto simp add: hypreal_divide_def st_mult st_not_Infinitesimal HFinite_inverse st_inverse)
done
@@ -1720,22 +1794,22 @@
by (blast intro: st_HFinite st_approx_self approx_st_eq)
declare st_idempotent [simp]
-(*** lemmas ***)
-lemma Infinitesimal_add_st_less: "[| x \<in> HFinite; y \<in> HFinite;
- u \<in> Infinitesimal; st x < st y
- |] ==> st x + u < st y"
+lemma Infinitesimal_add_st_less:
+ "[| x \<in> HFinite; y \<in> HFinite; u \<in> Infinitesimal; st x < st y |]
+ ==> st x + u < st y"
apply (drule st_SReal)+
apply (auto intro!: Infinitesimal_add_hypreal_of_real_less simp add: SReal_iff)
done
-lemma Infinitesimal_add_st_le_cancel: "[| x \<in> HFinite; y \<in> HFinite;
- u \<in> Infinitesimal; st x <= st y + u
- |] ==> st x <= st y"
+lemma Infinitesimal_add_st_le_cancel:
+ "[| x \<in> HFinite; y \<in> HFinite;
+ u \<in> Infinitesimal; st x \<le> st y + u
+ |] ==> st x \<le> st y"
apply (simp add: linorder_not_less [symmetric])
apply (auto dest: Infinitesimal_add_st_less)
done
-lemma st_le: "[| x \<in> HFinite; y \<in> HFinite; x <= y |] ==> st(x) <= st(y)"
+lemma st_le: "[| x \<in> HFinite; y \<in> HFinite; x \<le> y |] ==> st(x) \<le> st(y)"
apply (frule HFinite_st_Infinitesimal_add)
apply (rotate_tac 1)
apply (frule HFinite_st_Infinitesimal_add, safe)
@@ -1744,13 +1818,13 @@
apply (auto simp add: hypreal_add_assoc [symmetric])
done
-lemma st_zero_le: "[| 0 <= x; x \<in> HFinite |] ==> 0 <= st x"
+lemma st_zero_le: "[| 0 \<le> x; x \<in> HFinite |] ==> 0 \<le> st x"
apply (subst numeral_0_eq_0 [symmetric])
apply (rule st_number_of [THEN subst])
apply (rule st_le, auto)
done
-lemma st_zero_ge: "[| x <= 0; x \<in> HFinite |] ==> st x <= 0"
+lemma st_zero_ge: "[| x \<le> 0; x \<in> HFinite |] ==> st x \<le> 0"
apply (subst numeral_0_eq_0 [symmetric])
apply (rule st_number_of [THEN subst])
apply (rule st_le, auto)
@@ -1764,14 +1838,12 @@
-(*--------------------------------------------------------------------
- Alternative definitions for HFinite using Free ultrafilter
- --------------------------------------------------------------------*)
+subsection{*Alternative Definitions for @{term HFinite} using Free Ultrafilter*}
-lemma FreeUltrafilterNat_Rep_hypreal: "[| X \<in> Rep_hypreal x; Y \<in> Rep_hypreal x |]
+lemma FreeUltrafilterNat_Rep_hypreal:
+ "[| X \<in> Rep_hypreal x; Y \<in> Rep_hypreal x |]
==> {n. X n = Y n} \<in> FreeUltrafilterNat"
-apply (rule_tac z = x in eq_Abs_hypreal, auto, ultra)
-done
+by (rule_tac z = x in eq_Abs_hypreal, auto, ultra)
lemma HFinite_FreeUltrafilterNat:
"x \<in> HFinite
@@ -1793,33 +1865,37 @@
apply (auto simp add: hypreal_less SReal_iff hypreal_minus hypreal_of_real_def, ultra+)
done
-lemma HFinite_FreeUltrafilterNat_iff: "(x \<in> HFinite) = (\<exists>X \<in> Rep_hypreal x.
+lemma HFinite_FreeUltrafilterNat_iff:
+ "(x \<in> HFinite) = (\<exists>X \<in> Rep_hypreal x.
\<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat)"
apply (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite)
done
-(*--------------------------------------------------------------------
- Alternative definitions for HInfinite using Free ultrafilter
- --------------------------------------------------------------------*)
-lemma lemma_Compl_eq: "- {n. (u::real) < abs (xa n)} = {n. abs (xa n) <= u}"
+
+subsection{*Alternative Definitions for @{term HInfinite} using Free Ultrafilter*}
+
+lemma lemma_Compl_eq: "- {n. (u::real) < abs (xa n)} = {n. abs (xa n) \<le> u}"
by auto
-lemma lemma_Compl_eq2: "- {n. abs (xa n) < (u::real)} = {n. u <= abs (xa n)}"
+lemma lemma_Compl_eq2: "- {n. abs (xa n) < (u::real)} = {n. u \<le> abs (xa n)}"
by auto
-lemma lemma_Int_eq1: "{n. abs (xa n) <= (u::real)} Int {n. u <= abs (xa n)}
+lemma lemma_Int_eq1:
+ "{n. abs (xa n) \<le> (u::real)} Int {n. u \<le> abs (xa n)}
= {n. abs(xa n) = u}"
apply auto
done
-lemma lemma_FreeUltrafilterNat_one: "{n. abs (xa n) = u} <= {n. abs (xa n) < u + (1::real)}"
+lemma lemma_FreeUltrafilterNat_one:
+ "{n. abs (xa n) = u} \<le> {n. abs (xa n) < u + (1::real)}"
by auto
(*-------------------------------------
Exclude this type of sets from free
ultrafilter for Infinite numbers!
-------------------------------------*)
-lemma FreeUltrafilterNat_const_Finite: "[| xa: Rep_hypreal x;
+lemma FreeUltrafilterNat_const_Finite:
+ "[| xa: Rep_hypreal x;
{n. abs (xa n) = u} \<in> FreeUltrafilterNat
|] ==> x \<in> HFinite"
apply (rule FreeUltrafilterNat_HFinite)
@@ -1844,16 +1920,15 @@
add: HInfinite_HFinite_iff [THEN iffD1])
done
-(* yet more lemmas! *)
-lemma lemma_Int_HI: "{n. abs (Xa n) < u} Int {n. X n = Xa n}
- <= {n. abs (X n) < (u::real)}"
-apply auto
-done
+lemma lemma_Int_HI:
+ "{n. abs (Xa n) < u} Int {n. X n = Xa n} \<subseteq> {n. abs (X n) < (u::real)}"
+by auto
lemma lemma_Int_HIa: "{n. u < abs (X n)} Int {n. abs (X n) < (u::real)} = {}"
by (auto intro: order_less_asym)
-lemma FreeUltrafilterNat_HInfinite: "\<exists>X \<in> Rep_hypreal x. \<forall>u.
+lemma FreeUltrafilterNat_HInfinite:
+ "\<exists>X \<in> Rep_hypreal x. \<forall>u.
{n. u < abs (X n)} \<in> FreeUltrafilterNat
==> x \<in> HInfinite"
apply (rule HInfinite_HFinite_iff [THEN iffD2])
@@ -1866,15 +1941,13 @@
apply (auto simp add: lemma_Int_HIa FreeUltrafilterNat_empty)
done
-lemma HInfinite_FreeUltrafilterNat_iff: "(x \<in> HInfinite) = (\<exists>X \<in> Rep_hypreal x.
+lemma HInfinite_FreeUltrafilterNat_iff:
+ "(x \<in> HInfinite) = (\<exists>X \<in> Rep_hypreal x.
\<forall>u. {n. u < abs (X n)} \<in> FreeUltrafilterNat)"
-apply (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)
-done
+by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)
-(*--------------------------------------------------------------------
- Alternative definitions for Infinitesimal using Free ultrafilter
- --------------------------------------------------------------------*)
+subsection{*Alternative Definitions for @{term Infinitesimal} using Free Ultrafilter*}
lemma Infinitesimal_FreeUltrafilterNat:
"x \<in> Infinitesimal ==> \<exists>X \<in> Rep_hypreal x.
@@ -1900,7 +1973,8 @@
apply (auto simp add: hypreal_less hypreal_minus hypreal_of_real_def, ultra+)
done
-lemma Infinitesimal_FreeUltrafilterNat_iff: "(x \<in> Infinitesimal) = (\<exists>X \<in> Rep_hypreal x.
+lemma Infinitesimal_FreeUltrafilterNat_iff:
+ "(x \<in> Infinitesimal) = (\<exists>X \<in> Rep_hypreal x.
\<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat)"
apply (blast intro!: Infinitesimal_FreeUltrafilterNat FreeUltrafilterNat_Infinitesimal)
done
@@ -1909,17 +1983,19 @@
Infinitesimals as smaller than 1/n for all n::nat (> 0)
------------------------------------------------------------------------*)
-lemma lemma_Infinitesimal: "(\<forall>r. 0 < r --> x < r) = (\<forall>n. x < inverse(real (Suc n)))"
+lemma lemma_Infinitesimal:
+ "(\<forall>r. 0 < r --> x < r) = (\<forall>n. x < inverse(real (Suc n)))"
apply (auto simp add: real_of_nat_Suc_gt_zero)
apply (blast dest!: reals_Archimedean intro: order_less_trans)
done
lemma of_nat_in_Reals [simp]: "(of_nat n::hypreal) \<in> \<real>"
apply (induct n)
-apply (simp_all add: SReal_add);
+apply (simp_all add: SReal_add)
done
-lemma lemma_Infinitesimal2: "(\<forall>r \<in> Reals. 0 < r --> x < r) =
+lemma lemma_Infinitesimal2:
+ "(\<forall>r \<in> Reals. 0 < r --> x < r) =
(\<forall>n. x < inverse(hypreal_of_nat (Suc n)))"
apply safe
apply (drule_tac x = "inverse (hypreal_of_real (real (Suc n))) " in bspec)
@@ -1966,33 +2042,35 @@
apply (auto dest: order_less_trans)
done
-lemma lemma_real_le_Un_eq: "{n. f n <= u} = {n. f n < u} Un {n. u = (f n :: real)}"
+lemma lemma_real_le_Un_eq:
+ "{n. f n \<le> u} = {n. f n < u} Un {n. u = (f n :: real)}"
by (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le)
-lemma finite_real_of_nat_le_real: "finite {n::nat. real n <= u}"
+lemma finite_real_of_nat_le_real: "finite {n::nat. real n \<le> u}"
by (auto simp add: lemma_real_le_Un_eq lemma_finite_omega_set finite_real_of_nat_less_real)
-lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. abs(real n) <= u}"
+lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. abs(real n) \<le> u}"
apply (simp (no_asm) add: real_of_nat_Suc_gt_zero finite_real_of_nat_le_real)
done
-lemma rabs_real_of_nat_le_real_FreeUltrafilterNat: "{n. abs(real n) <= u} \<notin> FreeUltrafilterNat"
+lemma rabs_real_of_nat_le_real_FreeUltrafilterNat:
+ "{n. abs(real n) \<le> u} \<notin> FreeUltrafilterNat"
by (blast intro!: FreeUltrafilterNat_finite finite_rabs_real_of_nat_le_real)
lemma FreeUltrafilterNat_nat_gt_real: "{n. u < real n} \<in> FreeUltrafilterNat"
apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem)
-apply (subgoal_tac "- {n::nat. u < real n} = {n. real n <= u}")
+apply (subgoal_tac "- {n::nat. u < real n} = {n. real n \<le> u}")
prefer 2 apply force
apply (simp add: finite_real_of_nat_le_real [THEN FreeUltrafilterNat_finite])
done
(*--------------------------------------------------------------
- The complement of {n. abs(real n) <= u} =
+ The complement of {n. abs(real n) \<le> u} =
{n. u < abs (real n)} is in FreeUltrafilterNat
by property of (free) ultrafilters
--------------------------------------------------------------*)
-lemma Compl_real_le_eq: "- {n::nat. real n <= u} = {n. u < real n}"
+lemma Compl_real_le_eq: "- {n::nat. real n \<le> u} = {n. u < real n}"
by (auto dest!: order_le_less_trans simp add: linorder_not_le)
(*-----------------------------------------------
@@ -2038,8 +2116,8 @@
that \<forall>n. |X n - a| < 1/n. Used in proof of NSLIM => LIM.
-----------------------------------------------------------------------*)
-lemma real_of_nat_less_inverse_iff: "0 < u ==>
- (u < inverse (real(Suc n))) = (real(Suc n) < inverse u)"
+lemma real_of_nat_less_inverse_iff:
+ "0 < u ==> (u < inverse (real(Suc n))) = (real(Suc n) < inverse u)"
apply (simp add: inverse_eq_divide)
apply (subst pos_less_divide_eq, assumption)
apply (subst pos_less_divide_eq)
@@ -2047,18 +2125,21 @@
apply (simp add: real_mult_commute)
done
-lemma finite_inverse_real_of_posnat_gt_real: "0 < u ==> finite {n. u < inverse(real(Suc n))}"
+lemma finite_inverse_real_of_posnat_gt_real:
+ "0 < u ==> finite {n. u < inverse(real(Suc n))}"
apply (simp (no_asm_simp) add: real_of_nat_less_inverse_iff)
apply (simp (no_asm_simp) add: real_of_nat_Suc less_diff_eq [symmetric])
apply (rule finite_real_of_nat_less_real)
done
-lemma lemma_real_le_Un_eq2: "{n. u <= inverse(real(Suc n))} =
+lemma lemma_real_le_Un_eq2:
+ "{n. u \<le> inverse(real(Suc n))} =
{n. u < inverse(real(Suc n))} Un {n. u = inverse(real(Suc n))}"
apply (auto dest: order_le_imp_less_or_eq simp add: order_less_imp_le)
done
-lemma real_of_nat_inverse_le_iff: "(inverse (real(Suc n)) <= r) = (1 <= r * real(Suc n))"
+lemma real_of_nat_inverse_le_iff:
+ "(inverse (real(Suc n)) \<le> r) = (1 \<le> r * real(Suc n))"
apply (simp (no_asm) add: linorder_not_less [symmetric])
apply (simp (no_asm) add: inverse_eq_divide)
apply (subst pos_less_divide_eq)
@@ -2066,7 +2147,8 @@
apply (simp (no_asm) add: real_mult_commute)
done
-lemma real_of_nat_inverse_eq_iff: "(u = inverse (real(Suc n))) = (real(Suc n) = inverse u)"
+lemma real_of_nat_inverse_eq_iff:
+ "(u = inverse (real(Suc n))) = (real(Suc n) = inverse u)"
by (auto simp add: inverse_inverse_eq real_of_nat_Suc_gt_zero real_not_refl2 [THEN not_sym])
lemma lemma_finite_omega_set2: "finite {n::nat. u = inverse(real(Suc n))}"
@@ -2075,59 +2157,64 @@
apply (simp add: real_of_nat_Suc diff_eq_eq [symmetric] eq_commute)
done
-lemma finite_inverse_real_of_posnat_ge_real: "0 < u ==> finite {n. u <= inverse(real(Suc n))}"
+lemma finite_inverse_real_of_posnat_ge_real:
+ "0 < u ==> finite {n. u \<le> inverse(real(Suc n))}"
by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_omega_set2 finite_inverse_real_of_posnat_gt_real)
-lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat: "0 < u ==>
- {n. u <= inverse(real(Suc n))} \<notin> FreeUltrafilterNat"
-apply (blast intro!: FreeUltrafilterNat_finite finite_inverse_real_of_posnat_ge_real)
-done
+lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:
+ "0 < u ==> {n. u \<le> inverse(real(Suc n))} \<notin> FreeUltrafilterNat"
+by (blast intro!: FreeUltrafilterNat_finite finite_inverse_real_of_posnat_ge_real)
(*--------------------------------------------------------------
- The complement of {n. u <= inverse(real(Suc n))} =
+ The complement of {n. u \<le> inverse(real(Suc n))} =
{n. inverse(real(Suc n)) < u} is in FreeUltrafilterNat
by property of (free) ultrafilters
--------------------------------------------------------------*)
-lemma Compl_le_inverse_eq: "- {n. u <= inverse(real(Suc n))} =
+lemma Compl_le_inverse_eq:
+ "- {n. u \<le> inverse(real(Suc n))} =
{n. inverse(real(Suc n)) < u}"
apply (auto dest!: order_le_less_trans simp add: linorder_not_le)
done
-lemma FreeUltrafilterNat_inverse_real_of_posnat: "0 < u ==>
+lemma FreeUltrafilterNat_inverse_real_of_posnat:
+ "0 < u ==>
{n. inverse(real(Suc n)) < u} \<in> FreeUltrafilterNat"
apply (cut_tac u = u in inverse_real_of_posnat_ge_real_FreeUltrafilterNat)
apply (auto dest: FreeUltrafilterNat_Compl_mem simp add: Compl_le_inverse_eq)
done
-(*--------------------------------------------------------------
- Example where we get a hyperreal from a real sequence
+text{* Example where we get a hyperreal from a real sequence
for which a particular property holds. The theorem is
used in proofs about equivalence of nonstandard and
standard neighbourhoods. Also used for equivalence of
nonstandard ans standard definitions of pointwise
- limit (the theorem was previously in REALTOPOS.thy).
- -------------------------------------------------------------*)
+ limit.*}
+
(*-----------------------------------------------------
|X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x| \<in> Infinitesimal
-----------------------------------------------------*)
-lemma real_seq_to_hypreal_Infinitesimal: "\<forall>n. abs(X n + -x) < inverse(real(Suc n))
+lemma real_seq_to_hypreal_Infinitesimal:
+ "\<forall>n. abs(X n + -x) < inverse(real(Suc n))
==> Abs_hypreal(hyprel``{X}) + -hypreal_of_real x \<in> Infinitesimal"
apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset simp add: hypreal_minus hypreal_of_real_def hypreal_add Infinitesimal_FreeUltrafilterNat_iff hypreal_inverse)
done
-lemma real_seq_to_hypreal_approx: "\<forall>n. abs(X n + -x) < inverse(real(Suc n))
+lemma real_seq_to_hypreal_approx:
+ "\<forall>n. abs(X n + -x) < inverse(real(Suc n))
==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x"
apply (subst approx_minus_iff)
apply (rule mem_infmal_iff [THEN subst])
apply (erule real_seq_to_hypreal_Infinitesimal)
done
-lemma real_seq_to_hypreal_approx2: "\<forall>n. abs(x + -X n) < inverse(real(Suc n))
+lemma real_seq_to_hypreal_approx2:
+ "\<forall>n. abs(x + -X n) < inverse(real(Suc n))
==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x"
apply (simp add: abs_minus_add_cancel real_seq_to_hypreal_approx)
done
-lemma real_seq_to_hypreal_Infinitesimal2: "\<forall>n. abs(X n + -Y n) < inverse(real(Suc n))
+lemma real_seq_to_hypreal_Infinitesimal2:
+ "\<forall>n. abs(X n + -Y n) < inverse(real(Suc n))
==> Abs_hypreal(hyprel``{X}) +
-Abs_hypreal(hyprel``{Y}) \<in> Infinitesimal"
by (auto intro!: bexI
@@ -2351,7 +2438,3 @@
*}
end
-
-
-
-
--- a/src/HOL/IsaMakefile Mon Mar 01 05:39:32 2004 +0100
+++ b/src/HOL/IsaMakefile Mon Mar 01 11:52:59 2004 +0100
@@ -146,7 +146,8 @@
Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy \
Hyperreal/Fact.ML Hyperreal/Fact.thy Hyperreal/HLog.thy\
Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HSeries.thy\
- Hyperreal/HyperArith.thy Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy\
+ Hyperreal/HTranscendental.thy Hyperreal/HyperArith.thy\
+ Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy\
Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
Hyperreal/IntFloor.thy Hyperreal/IntFloor.ML\
Hyperreal/Lim.ML Hyperreal/Lim.thy Hyperreal/Log.thy\