New material on integration, etc. Moving Hyperreal/ex
to directory Complex
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/HLog.ML Mon May 05 18:23:40 2003 +0200
@@ -0,0 +1,261 @@
+(* Title : HLog.ML
+ Author : Jacques D. Fleuriot
+ Copyright : 2000,2001 University of Edinburgh
+ Description : hyperreal base logarithms
+*)
+
+Goalw [powhr_def]
+ "(Abs_hypreal(hyprel `` {X})) powhr (Abs_hypreal(hyprel `` {Y})) = \
+\ Abs_hypreal(hyprel `` {%n. (X n) powr (Y n)})";
+by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_mult,
+ powr_def]));
+qed "powhr";
+
+Goal "1 powhr a = 1";
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [powhr,hypreal_one_num]));
+qed "powhr_one_eq_one";
+Addsimps [powhr_one_eq_one];
+
+Goal "[| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [powhr,hypreal_zero_num,
+ hypreal_mult,hypreal_less]));
+by (ultra_tac (claset(),simpset() addsimps [powr_mult]) 1);
+qed "powhr_mult";
+
+Goalw [hypreal_zero_def] "0 < x powhr a";
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [powhr,hypreal_less,hypreal_zero_num]));
+qed "powhr_gt_zero";
+Addsimps [powhr_gt_zero];
+
+Goal "x powhr a ~= 0";
+by (rtac ((powhr_gt_zero RS hypreal_not_refl2) RS not_sym) 1);
+qed "powhr_not_zero";
+Addsimps [powhr_not_zero];
+
+Goalw [hypreal_divide_def]
+ "(Abs_hypreal(hyprel `` {X}))/(Abs_hypreal(hyprel `` {Y})) = \
+\ (Abs_hypreal(hyprel `` {%n. (X n)/(Y n)}))";
+by (case_tac "Abs_hypreal (hyprel `` {Y}) = 0" 1);
+by (auto_tac (claset(),simpset() addsimps [HYPREAL_DIVISION_BY_ZERO,
+ hypreal_zero_num,hypreal_inverse,hypreal_mult]));
+by (ALLGOALS(ultra_tac (claset(),simpset() addsimps [real_divide_def])));
+qed "hypreal_divide";
+
+Goal "[| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [powhr,hypreal_divide,
+ hypreal_zero_num,hypreal_less]));
+by (ultra_tac (claset(),simpset() addsimps [powr_divide]) 1);
+qed "powhr_divide";
+
+Goal "x powhr (a + b) = (x powhr a) * (x powhr b)";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","b")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [powhr,hypreal_add,hypreal_mult,
+ powr_add]));
+qed "powhr_add";
+
+Goal "(x powhr a) powhr b = x powhr (a * b)";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","b")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [powhr,hypreal_mult,
+ powr_powr]));
+qed "powhr_powhr";
+
+Goal "(x powhr a) powhr b = (x powhr b) powhr a";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","b")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [powhr,powr_powr_swap]));
+qed "powhr_powhr_swap";
+
+Goal "x powhr (-a) = inverse (x powhr a)";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [powhr,hypreal_minus,
+ hypreal_inverse,hypreal_less,powr_minus]));
+qed "powhr_minus";
+
+Goalw [hypreal_divide_def] "x powhr (-a) = 1/(x powhr a)";
+by (simp_tac (simpset() addsimps [powhr_minus]) 1);
+qed "powhr_minus_divide";
+
+Goal "[| a < b; 1 < x |] ==> x powhr a < x powhr b";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","b")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [powhr,hypreal_one_num,
+ hypreal_less]));
+by (ultra_tac (claset(),simpset() addsimps [powr_less_mono]) 1);
+qed "powhr_less_mono";
+
+Goal "[| x powhr a < x powhr b; 1 < x |] ==> a < b";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","b")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [powhr,hypreal_one_num,
+ hypreal_less]));
+by (ultra_tac (claset() addDs [powr_less_cancel],simpset()) 1);
+qed "powhr_less_cancel";
+
+Goal "1 < x ==> (x powhr a < x powhr b) = (a < b)";
+by (blast_tac (claset() addIs [powhr_less_cancel,powhr_less_mono]) 1);
+qed "powhr_less_cancel_iff";
+Addsimps [powhr_less_cancel_iff];
+
+Goal "1 < x ==> (x powhr a <= x powhr b) = (a <= b)";
+by (auto_tac (claset(),simpset() addsimps [hypreal_le_def]));
+qed "powhr_le_cancel_iff";
+Addsimps [powhr_le_cancel_iff];
+
+Goalw [hlog_def]
+ "hlog (Abs_hypreal(hyprel `` {X})) (Abs_hypreal(hyprel `` {Y})) = \
+\ Abs_hypreal(hyprel `` {%n. log (X n) (Y n)})";
+by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
+by (Auto_tac THEN Ultra_tac 1);
+qed "hlog";
+
+Goal "( *f* ln) x = hlog (( *f* exp) 1) x";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun,hlog,log_ln,
+ hypreal_one_num]));
+qed "hlog_starfun_ln";
+
+Goal "[| 0 < a; a ~= 1; 0 < x |] ==> a powhr (hlog a x) = x";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [hlog,powhr,hypreal_zero_num,
+ hypreal_less,hypreal_one_num]));
+by (Ultra_tac 1);
+qed "powhr_hlog_cancel";
+Addsimps [powhr_hlog_cancel];
+
+Goal "[| 0 < a; a ~= 1 |] ==> hlog a (a powhr y) = y";
+by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [hlog,powhr,hypreal_zero_num,
+ hypreal_less,hypreal_one_num]));
+by (ultra_tac (claset() addIs [log_powr_cancel],simpset()) 1);
+qed "hlog_powhr_cancel";
+Addsimps [hlog_powhr_cancel];
+
+Goal "[| 0 < a; a ~= 1; 0 < x; 0 < y |] \
+\ ==> hlog a (x * y) = hlog a x + hlog a y";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [hlog,powhr,hypreal_zero_num,
+ hypreal_one_num,hypreal_less,hypreal_add,hypreal_mult]));
+by (ultra_tac (claset(),simpset() addsimps [log_mult]) 1);
+qed "hlog_mult";
+
+Goal "[| 0 < a; a ~= 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [hlog,starfun,
+ hypreal_zero_num,hypreal_one_num,hypreal_divide,log_def]));
+qed "hlog_as_starfun";
+
+Goal "[| 0 < a; a ~= 1; 0 < b; b ~= 1; 0 < x |] \
+\ ==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","b")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [hlog,starfun,
+ hypreal_zero_num,hypreal_one_num,hypreal_less,
+ hypreal_divide,hypreal_mult]));
+by (ultra_tac (claset() addDs [log_eq_div_ln_mult_log],simpset()) 1);
+qed "hlog_eq_div_starfun_ln_mult_hlog";
+
+Goal "x powhr a = ( *f* exp) (a * ( *f* ln) x)";
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [powhr,starfun,
+ hypreal_mult,powr_def]));
+qed "powhr_as_starfun";
+
+Goal "[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal; \
+\ 0 < a |] ==> x powhr a : HInfinite";
+by (auto_tac (claset() addSIs [starfun_ln_ge_zero,
+ starfun_ln_HInfinite,HInfinite_HFinite_not_Infinitesimal_mult2,
+ starfun_exp_HInfinite],simpset() addsimps [order_less_imp_le,
+ HInfinite_gt_zero_gt_one,powhr_as_starfun,
+ hypreal_0_le_mult_iff]));
+qed "HInfinite_powhr";
+
+Goal "[| x : HFinite - Infinitesimal; a : HInfinite; 0 < a |] \
+\ ==> hlog a (abs x) : Infinitesimal";
+by (ftac HInfinite_gt_zero_gt_one 1);
+by (auto_tac (claset() addSIs [starfun_ln_HFinite_not_Infinitesimal,
+ HInfinite_inverse_Infinitesimal,Infinitesimal_HFinite_mult2],
+ simpset() addsimps [starfun_ln_HInfinite,not_Infinitesimal_not_zero,
+ hlog_as_starfun,hypreal_not_refl2 RS not_sym,hypreal_divide_def]));
+qed "hlog_hrabs_HInfinite_Infinitesimal";
+
+Goal "[| a : HInfinite; 0 < a |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a";
+by (rtac hlog_as_starfun 1);
+by Auto_tac;
+qed "hlog_HInfinite_as_starfun";
+
+Goal "hlog a 1 = 0";
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_one_num,
+ hypreal_zero_num,hlog]));
+qed "hlog_one";
+Addsimps [hlog_one];
+
+Goal "[| 0 < a; a ~= 1 |] ==> hlog a a = 1";
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_one_num,
+ hypreal_zero_num,hlog,hypreal_less]));
+by (ultra_tac (claset() addIs [log_eq_one],simpset()) 1);
+qed "hlog_eq_one";
+Addsimps [hlog_eq_one];
+
+Goal "[| 0 < a; a ~= 1; 0 < x |] ==> hlog a (inverse x) = - hlog a x";
+by (res_inst_tac [("x1","hlog a x")] (hypreal_add_left_cancel RS iffD1) 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_not_refl2 RS not_sym,
+ hlog_mult RS sym,hypreal_inverse_gt_0]));
+qed "hlog_inverse";
+
+Goal "[| 0 < a; a ~= 1; 0 < x; 0 < y|] \
+\ ==> hlog a (x/y) = hlog a x - hlog a y";
+by (auto_tac (claset(),simpset() addsimps [hypreal_inverse_gt_0,hlog_mult,
+ hlog_inverse,hypreal_diff_def,hypreal_divide_def]));
+qed "hlog_divide";
+
+Goal "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)";
+by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
+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 [hlog,hypreal_less,
+ hypreal_zero_num,hypreal_one_num]));
+by (ALLGOALS(Ultra_tac));
+qed "hlog_less_cancel_iff";
+Addsimps [hlog_less_cancel_iff];
+
+Goal "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x <= hlog a y) = (x <= y)";
+by (auto_tac (claset(),simpset() addsimps [hypreal_le_def]));
+qed "hlog_le_cancel_iff";
+Addsimps [hlog_le_cancel_iff];
+
+(* should be in NSA.ML *)
+goalw HLog.thy [epsilon_def] "0 <= epsilon";
+by (auto_tac (claset(),simpset() addsimps [hypreal_zero_num,hypreal_le]));
+qed "epsilon_ge_zero";
+Addsimps [epsilon_ge_zero];
+
+goal HLog.thy "epsilon : {x. 0 <= x & x : HFinite}";
+by Auto_tac;
+qed "hpfinite_witness";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/HLog.thy Mon May 05 18:23:40 2003 +0200
@@ -0,0 +1,19 @@
+(* Title : HLog.thy
+ Author : Jacques D. Fleuriot
+ Copyright : 2000,2001 University of Edinburgh
+ Description : hyperreal base logarithms
+*)
+
+HLog = Log + HTranscendental +
+
+
+constdefs
+
+ powhr :: [hypreal,hypreal] => hypreal (infixr 80)
+ "x powhr a == ( *f* exp) (a * ( *f* ln) x)"
+
+ hlog :: [hypreal,hypreal] => hypreal
+ "hlog a x == Abs_hypreal(UN A: Rep_hypreal(a).UN X: Rep_hypreal(x).
+ hyprel `` {%n. log (A n) (X n)})"
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/HTranscendental.ML Mon May 05 18:23:40 2003 +0200
@@ -0,0 +1,740 @@
+(* Title : HTranscendental.ML
+ Author : Jacques D. Fleuriot
+ Copyright : 2001 University of Edinburgh
+ Description : Nonstandard extensions of transcendental functions
+*)
+
+(*-------------------------------------------------------------------------*)
+(* NS extension of square root function *)
+(*-------------------------------------------------------------------------*)
+
+Goal "( *f* sqrt) 0 = 0";
+by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_zero_num]));
+qed "STAR_sqrt_zero";
+Addsimps [STAR_sqrt_zero];
+
+Goal "( *f* sqrt) 1 = 1";
+by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_one_num]));
+qed "STAR_sqrt_one";
+Addsimps [STAR_sqrt_one];
+
+Goal "(( *f* sqrt)(x) ^ 2 = x) = (0 <= x)";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_le,
+ hypreal_zero_num, starfun,hrealpow,real_sqrt_pow2_iff]
+ delsimps [hpowr_Suc,realpow_Suc]));
+qed "hypreal_sqrt_pow2_iff";
+
+Goal "0 < x ==> ( *f* sqrt) (x) ^ 2 = x";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset() addIs [FreeUltrafilterNat_subset,
+ real_sqrt_gt_zero_pow2],simpset() addsimps
+ [hypreal_less,starfun,hrealpow,hypreal_zero_num]
+ delsimps [hpowr_Suc,realpow_Suc]));
+qed "hypreal_sqrt_gt_zero_pow2";
+
+Goal "0 < x ==> 0 < ( *f* sqrt) (x) ^ 2";
+by (forward_tac [hypreal_sqrt_gt_zero_pow2] 1);
+by (Auto_tac);
+qed "hypreal_sqrt_pow2_gt_zero";
+
+Goal "0 < x ==> ( *f* sqrt) (x) ~= 0";
+by (forward_tac [hypreal_sqrt_pow2_gt_zero] 1);
+by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc]));
+qed "hypreal_sqrt_not_zero";
+
+Goal "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x";
+by (forward_tac [hypreal_sqrt_not_zero] 1);
+by (dres_inst_tac [("n1","2"),("r1","( *f* sqrt) x")] (hrealpow_inverse RS sym) 1);
+by (auto_tac (claset() addDs [hypreal_sqrt_gt_zero_pow2],simpset()));
+qed "hypreal_inverse_sqrt_pow2";
+
+Goalw [hypreal_zero_def]
+ "[|0 < x; 0 <y |] ==> \
+\ ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun,
+ hypreal_mult,hypreal_less,hypreal_zero_num]));
+by (ultra_tac (claset() addIs [real_sqrt_mult_distrib],simpset()) 1);
+qed "hypreal_sqrt_mult_distrib";
+
+Goal "[|0<=x; 0<=y |] ==> \
+\ ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)";
+by (auto_tac (claset() addIs [hypreal_sqrt_mult_distrib],
+ simpset() addsimps [hypreal_le_eq_less_or_eq]));
+qed "hypreal_sqrt_mult_distrib2";
+
+Goal "0 < x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)";
+by (auto_tac (claset(),simpset() addsimps [mem_infmal_iff RS sym]));
+by (rtac (hypreal_sqrt_gt_zero_pow2 RS subst) 1);
+by (auto_tac (claset() addIs [Infinitesimal_mult]
+ addSDs [(hypreal_sqrt_gt_zero_pow2 RS ssubst)],simpset() addsimps [two_eq_Suc_Suc]));
+qed "hypreal_sqrt_approx_zero";
+Addsimps [hypreal_sqrt_approx_zero];
+
+Goal "0 <= x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)";
+by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq],
+ simpset()));
+qed "hypreal_sqrt_approx_zero2";
+Addsimps [hypreal_sqrt_approx_zero2];
+
+Goal "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)";
+by (rtac hypreal_sqrt_approx_zero2 1);
+by (REPEAT(rtac hypreal_le_add_order 1));
+by Auto_tac;
+qed "hypreal_sqrt_sum_squares";
+Addsimps [hypreal_sqrt_sum_squares];
+
+Goal "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)";
+by (rtac hypreal_sqrt_approx_zero2 1);
+by (rtac hypreal_le_add_order 1);
+by Auto_tac;
+qed "hypreal_sqrt_sum_squares2";
+Addsimps [hypreal_sqrt_sum_squares2];
+
+Goal "0 < x ==> 0 < ( *f* sqrt)(x)";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps
+ [starfun,hypreal_zero_def,hypreal_less,hypreal_zero_num]));
+by (ultra_tac (claset() addIs [real_sqrt_gt_zero], simpset()) 1);
+qed "hypreal_sqrt_gt_zero";
+
+Goal "0 <= x ==> 0 <= ( *f* sqrt)(x)";
+by (auto_tac (claset() addIs [hypreal_sqrt_gt_zero],
+ simpset() addsimps [hypreal_le_eq_less_or_eq ]));
+qed "hypreal_sqrt_ge_zero";
+
+Goal "( *f* sqrt)(x ^ 2) = abs(x)";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun,
+ hypreal_hrabs,hypreal_mult,two_eq_Suc_Suc]));
+qed "hypreal_sqrt_hrabs";
+Addsimps [hypreal_sqrt_hrabs];
+
+Goal "( *f* sqrt)(x*x) = abs(x)";
+by (rtac (hrealpow_two RS subst) 1);
+by (rtac (two_eq_Suc_Suc RS subst) 1);
+by (rtac hypreal_sqrt_hrabs 1);
+qed "hypreal_sqrt_hrabs2";
+Addsimps [hypreal_sqrt_hrabs2];
+
+Goal "( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun,
+ hypreal_hrabs,hypnat_of_nat_def,hyperpow]));
+qed "hypreal_sqrt_hyperpow_hrabs";
+Addsimps [hypreal_sqrt_hyperpow_hrabs];
+
+Goal "[| x: HFinite; 0 <= x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)";
+by (res_inst_tac [("n","1")] hrealpow_Suc_cancel_eq 1);
+by (auto_tac (claset() addSIs [st_zero_le,hypreal_sqrt_ge_zero],simpset()));
+by (rtac (st_mult RS subst) 2);
+by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 4);
+by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 6);
+by (auto_tac (claset(), simpset() addsimps [st_hrabs,st_zero_le]));
+by (ALLGOALS(rtac (HFinite_square_iff RS iffD1)));
+by (auto_tac (claset(),simpset() addsimps
+ [hypreal_sqrt_mult_distrib2 RS sym]
+ delsimps [HFinite_square_iff]));
+qed "st_hypreal_sqrt";
+
+Goal "x <= ( *f* sqrt)(x ^ 2 + y ^ 2)";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_add,
+ hrealpow,hypreal_le] delsimps [hpowr_Suc,realpow_Suc]));
+qed "hypreal_sqrt_sum_squares_ge1";
+Addsimps [hypreal_sqrt_sum_squares_ge1];
+
+Goal "[| 0 <= x; x : HFinite |] ==> ( *f* sqrt) x : HFinite";
+by (auto_tac (claset(),simpset() addsimps [hypreal_le_eq_less_or_eq]));
+by (rtac (HFinite_square_iff RS iffD1) 1);
+by (dtac hypreal_sqrt_gt_zero_pow2 1);
+by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc]));
+qed "HFinite_hypreal_sqrt";
+
+Goal "[| 0 <= x; ( *f* sqrt) x : HFinite |] ==> x : HFinite";
+by (auto_tac (claset(),simpset() addsimps [hypreal_le_eq_less_or_eq]));
+by (dtac (HFinite_square_iff RS iffD2) 1);
+by (dtac hypreal_sqrt_gt_zero_pow2 1);
+by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc] delsimps [HFinite_square_iff]));
+qed "HFinite_hypreal_sqrt_imp_HFinite";
+
+Goal "0 <= x ==> (( *f* sqrt) x : HFinite) = (x : HFinite)";
+by (blast_tac (claset() addIs [HFinite_hypreal_sqrt,
+ HFinite_hypreal_sqrt_imp_HFinite]) 1);
+qed "HFinite_hypreal_sqrt_iff";
+Addsimps [HFinite_hypreal_sqrt_iff];
+
+Goal "(( *f* sqrt)(x*x + y*y) : HFinite) = (x*x + y*y : HFinite)";
+by (rtac HFinite_hypreal_sqrt_iff 1);
+by (rtac hypreal_le_add_order 1);
+by Auto_tac;
+qed "HFinite_sqrt_sum_squares";
+Addsimps [HFinite_sqrt_sum_squares];
+
+Goal "[| 0 <= x; x : Infinitesimal |] ==> ( *f* sqrt) x : Infinitesimal";
+by (auto_tac (claset(),simpset() addsimps [hypreal_le_eq_less_or_eq]));
+by (rtac (Infinitesimal_square_iff RS iffD2) 1);
+by (dtac hypreal_sqrt_gt_zero_pow2 1);
+by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc]));
+qed "Infinitesimal_hypreal_sqrt";
+
+Goal "[| 0 <= x; ( *f* sqrt) x : Infinitesimal |] ==> x : Infinitesimal";
+by (auto_tac (claset(),simpset() addsimps [hypreal_le_eq_less_or_eq]));
+by (dtac (Infinitesimal_square_iff RS iffD1) 1);
+by (dtac hypreal_sqrt_gt_zero_pow2 1);
+by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc]
+ delsimps [Infinitesimal_square_iff RS sym]));
+qed "Infinitesimal_hypreal_sqrt_imp_Infinitesimal";
+
+Goal "0 <= x ==> (( *f* sqrt) x : Infinitesimal) = (x : Infinitesimal)";
+by (blast_tac (claset() addIs [Infinitesimal_hypreal_sqrt_imp_Infinitesimal,
+ Infinitesimal_hypreal_sqrt]) 1);
+qed "Infinitesimal_hypreal_sqrt_iff";
+Addsimps [Infinitesimal_hypreal_sqrt_iff];
+
+Goal "(( *f* sqrt)(x*x + y*y) : Infinitesimal) = (x*x + y*y : Infinitesimal)";
+by (rtac Infinitesimal_hypreal_sqrt_iff 1);
+by (rtac hypreal_le_add_order 1);
+by Auto_tac;
+qed "Infinitesimal_sqrt_sum_squares";
+Addsimps [Infinitesimal_sqrt_sum_squares];
+
+Goal "[| 0 <= x; x : HInfinite |] ==> ( *f* sqrt) x : HInfinite";
+by (auto_tac (claset(),simpset() addsimps [hypreal_le_eq_less_or_eq]));
+by (rtac (HInfinite_square_iff RS iffD1) 1);
+by (dtac hypreal_sqrt_gt_zero_pow2 1);
+by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc]));
+qed "HInfinite_hypreal_sqrt";
+
+Goal "[| 0 <= x; ( *f* sqrt) x : HInfinite |] ==> x : HInfinite";
+by (auto_tac (claset(),simpset() addsimps [hypreal_le_eq_less_or_eq]));
+by (dtac (HInfinite_square_iff RS iffD2) 1);
+by (dtac hypreal_sqrt_gt_zero_pow2 1);
+by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc]
+ delsimps [HInfinite_square_iff]));
+qed "HInfinite_hypreal_sqrt_imp_HInfinite";
+
+Goal "0 <= x ==> (( *f* sqrt) x : HInfinite) = (x : HInfinite)";
+by (blast_tac (claset() addIs [HInfinite_hypreal_sqrt,
+ HInfinite_hypreal_sqrt_imp_HInfinite]) 1);
+qed "HInfinite_hypreal_sqrt_iff";
+Addsimps [HInfinite_hypreal_sqrt_iff];
+
+Goal "(( *f* sqrt)(x*x + y*y) : HInfinite) = (x*x + y*y : HInfinite)";
+by (rtac HInfinite_hypreal_sqrt_iff 1);
+by (rtac hypreal_le_add_order 1);
+by Auto_tac;
+qed "HInfinite_sqrt_sum_squares";
+Addsimps [HInfinite_sqrt_sum_squares];
+
+Goal "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) : HFinite";
+by (auto_tac (claset() addSIs [NSBseq_HFinite_hypreal,NSconvergent_NSBseq],
+ simpset() addsimps [starfunNat_sumr RS sym,starfunNat,hypnat_omega_def,
+ convergent_NSconvergent_iff RS sym, summable_convergent_sumr_iff RS sym,
+ summable_exp]));
+qed "HFinite_exp";
+Addsimps [HFinite_exp];
+
+Goalw [exphr_def] "exphr 0 = 1";
+by (res_inst_tac [("n1","1")] (sumhr_split_add RS subst) 1);
+by (res_inst_tac [("t","1")] (hypnat_add_zero_left RS subst) 2);
+by (rtac hypnat_one_less_hypnat_omega 1);
+by (auto_tac (claset(),simpset() addsimps [sumhr,hypnat_zero_def,starfunNat,
+ hypnat_one_def,hypnat_add,hypnat_omega_def,hypreal_add]
+ delsimps [hypnat_add_zero_left]));
+by (simp_tac (simpset() addsimps [hypreal_one_num RS sym]) 1);
+qed "exphr_zero";
+Addsimps [exphr_zero];
+
+Goalw [coshr_def] "coshr 0 = 1";
+by (res_inst_tac [("n1","1")] (sumhr_split_add RS subst) 1);
+by (res_inst_tac [("t","1")] (hypnat_add_zero_left RS subst) 2);
+by (rtac hypnat_one_less_hypnat_omega 1);
+by (auto_tac (claset(),simpset() addsimps [sumhr,hypnat_zero_def,starfunNat,
+ hypnat_one_def,hypnat_add,hypnat_omega_def,st_add RS sym,
+ (hypreal_one_def RS meta_eq_to_obj_eq) RS sym,
+ (hypreal_zero_def RS meta_eq_to_obj_eq) RS sym] delsimps [hypnat_add_zero_left]));
+qed "coshr_zero";
+Addsimps [coshr_zero];
+
+Goalw [hypreal_zero_def,hypreal_one_def] "( *f* exp) 0 @= 1";
+by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_one_num]));
+qed "STAR_exp_zero_approx_one";
+Addsimps [STAR_exp_zero_approx_one];
+
+Goal "x: Infinitesimal ==> ( *f* exp) x @= 1";
+by (case_tac "x = 0" 1);
+by (cut_inst_tac [("x","0")] DERIV_exp 2);
+by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym,
+ nsderiv_def]));
+by (dres_inst_tac [("x","x")] bspec 1);
+by Auto_tac;
+by (dres_inst_tac [("c","x")] approx_mult1 1);
+by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
+ simpset() addsimps [hypreal_mult_assoc]));
+by (res_inst_tac [("d","-1")] approx_add_right_cancel 1);
+by (rtac (approx_sym RSN (2,approx_trans2)) 1);
+by (auto_tac (claset(),simpset() addsimps [mem_infmal_iff]));
+qed "STAR_exp_Infinitesimal";
+
+Goal "( *f* exp) epsilon @= 1";
+by (auto_tac (claset() addIs [STAR_exp_Infinitesimal],simpset()));
+qed "STAR_exp_epsilon";
+Addsimps [STAR_exp_epsilon];
+
+Goal "( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_add,
+ hypreal_mult,exp_add]));
+qed "STAR_exp_add";
+
+Goalw [exphr_def] "exphr x = hypreal_of_real (exp x)";
+by (rtac (st_hypreal_of_real RS subst) 1);
+by (rtac approx_st_eq 1);
+by Auto_tac;
+by (rtac (approx_minus_iff RS iffD2) 1);
+by (auto_tac (claset(),simpset() addsimps [mem_infmal_iff RS sym,
+ hypreal_of_real_def,hypnat_zero_def,hypnat_omega_def,sumhr,
+ hypreal_minus,hypreal_add]));
+by (rtac NSLIMSEQ_zero_Infinitesimal_hypreal 1);
+by (cut_inst_tac [("x3","x")] (exp_converges RS ((sums_def RS
+ meta_eq_to_obj_eq) RS iffD1)) 1);
+by (dres_inst_tac [("b","- exp x")] (LIMSEQ_const RSN (2,LIMSEQ_add)) 1);
+by (auto_tac (claset(),simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]));
+qed "exphr_hypreal_of_real_exp_eq";
+
+Goal "0 <= x ==> (1 + x) <= ( *f* exp) x";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_add,
+ hypreal_le,hypreal_zero_num,hypreal_one_num]));
+by (Ultra_tac 1);
+qed "starfun_exp_ge_add_one_self";
+Addsimps [starfun_exp_ge_add_one_self];
+
+(* exp (oo) is infinite *)
+Goal "[| x : HInfinite; 0 <= x |] ==> ( *f* exp) x : HInfinite";
+by (ftac starfun_exp_ge_add_one_self 1);
+by (rtac HInfinite_ge_HInfinite 1);
+by (rtac hypreal_le_trans 2);
+by (TRYALL(assume_tac) THEN Simp_tac 1);
+qed "starfun_exp_HInfinite";
+
+Goal "( *f* exp) (-x) = inverse(( *f* exp) x)";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_inverse,
+ hypreal_minus,exp_minus]));
+qed "starfun_exp_minus";
+
+(* exp (-oo) is infinitesimal *)
+Goal "[| x : HInfinite; x <= 0 |] ==> ( *f* exp) x : Infinitesimal";
+by (subgoal_tac "EX y. x = - y" 1);
+by (res_inst_tac [("x","- x")] exI 2);
+by (auto_tac (claset() addSIs [HInfinite_inverse_Infinitesimal,
+ starfun_exp_HInfinite] addIs [(starfun_exp_minus RS ssubst)],
+ simpset() addsimps [HInfinite_minus_iff]));
+qed "starfun_exp_Infinitesimal";
+
+Goal "0 < x ==> 1 < ( *f* exp) x";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_one_num,
+ hypreal_zero_num,hypreal_less]));
+by (Ultra_tac 1);
+qed "starfun_exp_gt_one";
+Addsimps [starfun_exp_gt_one];
+
+(* needs derivative of inverse function
+ TRY a NS one today!!!
+
+Goal "x @= 1 ==> ( *f* ln) x @= 1";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_one_def]));
+
+
+Goalw [nsderiv_def] "0r < x ==> NSDERIV ln x :> inverse x";
+
+*)
+
+
+Goal "( *f* ln) (( *f* exp) x) = x";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun]));
+qed "starfun_ln_exp";
+Addsimps [starfun_ln_exp];
+
+Goal "(( *f* exp)(( *f* ln) x) = x) = (0 < x)";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun,
+ hypreal_zero_num,hypreal_less]));
+qed "starfun_exp_ln_iff";
+Addsimps [starfun_exp_ln_iff];
+
+Goal "( *f* exp) u = x ==> ( *f* ln) x = u";
+by (auto_tac (claset(),simpset() addsimps [starfun]));
+qed "starfun_exp_ln_eq";
+
+Goal "0 < x ==> ( *f* ln) x < x";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun,
+ hypreal_zero_num,hypreal_less]));
+by (Ultra_tac 1);
+qed "starfun_ln_less_self";
+Addsimps [starfun_ln_less_self];
+
+Goal "1 <= x ==> 0 <= ( *f* ln) x";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun,
+ hypreal_zero_num,hypreal_le,hypreal_one_num]));
+by (Ultra_tac 1);
+qed "starfun_ln_ge_zero";
+Addsimps [starfun_ln_ge_zero];
+
+Goal "1 < x ==> 0 < ( *f* ln) x";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun,
+ hypreal_zero_num,hypreal_less,hypreal_one_num]));
+by (Ultra_tac 1);
+qed "starfun_ln_gt_zero";
+Addsimps [starfun_ln_gt_zero];
+
+Goal "[| 0 < x; x ~= 1 |] ==> ( *f* ln) x ~= 0";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun,
+ hypreal_zero_num,hypreal_less,hypreal_one_num]));
+by (ultra_tac (claset() addIs [ccontr] addDs [ln_not_eq_zero],simpset()) 1);
+qed "starfun_ln_not_eq_zero";
+Addsimps [starfun_ln_not_eq_zero];
+
+Goal "[| x: HFinite; 1 <= x |] ==> ( *f* ln) x : HFinite";
+by (rtac HFinite_bounded 1);
+by (rtac order_less_imp_le 2);
+by (rtac starfun_ln_less_self 2);
+by (rtac order_less_le_trans 2);
+by Auto_tac;
+qed "starfun_ln_HFinite";
+
+Goal "0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun,
+ hypreal_zero_num,hypreal_minus,hypreal_inverse,
+ hypreal_less]));
+by (Ultra_tac 1);
+by (auto_tac (claset(),simpset() addsimps [ln_inverse]));
+qed "starfun_ln_inverse";
+
+Goal "x : HFinite ==> ( *f* exp) x : HFinite";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun,
+ HFinite_FreeUltrafilterNat_iff]));
+by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
+by Auto_tac;
+by (res_inst_tac [("x","exp u")] exI 1);
+by (Ultra_tac 1 THEN arith_tac 1);
+qed "starfun_exp_HFinite";
+
+Goal "[|x: Infinitesimal; z: HFinite |] ==> ( *f* exp) (z + x) @= ( *f* exp) z";
+by (simp_tac (simpset() addsimps [STAR_exp_add]) 1);
+by (ftac STAR_exp_Infinitesimal 1);
+by (dtac approx_mult2 1);
+by (auto_tac (claset() addIs [starfun_exp_HFinite],simpset()));
+qed "starfun_exp_add_HFinite_Infinitesimal_approx";
+
+(* using previous result to get to result *)
+Goal "[| x : HInfinite; 0 < x |] ==> ( *f* ln) x : HInfinite";
+by (rtac ccontr 1 THEN dtac (HFinite_HInfinite_iff RS iffD2) 1);
+by (dtac starfun_exp_HFinite 1);
+by (auto_tac (claset(),simpset() addsimps [starfun_exp_ln_iff RS iffD2,
+ HFinite_HInfinite_iff]));
+qed "starfun_ln_HInfinite";
+
+Goal "x : HInfinite ==> ( *f* exp) x : HInfinite | ( *f* exp) x : Infinitesimal";
+by (cut_inst_tac [("x","x")] (CLAIM "x <= (0::hypreal) | 0 <= x") 1);
+by (auto_tac (claset() addIs [starfun_exp_HInfinite,starfun_exp_Infinitesimal],
+ simpset()));
+qed "starfun_exp_HInfinite_Infinitesimal_disj";
+
+(* check out this proof!!! *)
+Goal "[| x : HFinite - Infinitesimal; 0 < x |] ==> ( *f* ln) x : HFinite";
+by (rtac ccontr 1 THEN dtac (HInfinite_HFinite_iff RS iffD2) 1);
+by (dtac starfun_exp_HInfinite_Infinitesimal_disj 1);
+by (auto_tac (claset(),simpset() addsimps [starfun_exp_ln_iff RS sym,
+ HInfinite_HFinite_iff] delsimps [starfun_exp_ln_iff]));
+qed "starfun_ln_HFinite_not_Infinitesimal";
+
+(* we do proof by considering ln of 1/x *)
+Goal "[| x : Infinitesimal; 0 < x |] ==> ( *f* ln) x : HInfinite";
+by (dtac Infinitesimal_inverse_HInfinite 1);
+by (ftac hypreal_inverse_gt_0 1);
+by (dtac starfun_ln_HInfinite 2);
+by (auto_tac (claset(),simpset() addsimps [starfun_ln_inverse,
+ HInfinite_minus_iff]));
+qed "starfun_ln_Infinitesimal_HInfinite";
+
+Goal "[| 0 < x; x < 1 |] ==> ( *f* ln) x < 0";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_zero_num,
+ hypreal_one_num,hypreal_less,starfun]));
+by (ultra_tac (claset() addIs [ln_less_zero],simpset()) 1);
+qed "starfun_ln_less_zero";
+
+Goal "[| x : Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0";
+by (auto_tac (claset() addSIs [starfun_ln_less_zero],simpset()
+ addsimps [Infinitesimal_def]));
+by (dres_inst_tac [("x","1")] bspec 1);
+by (auto_tac (claset(),simpset() addsimps [hrabs_def]));
+qed "starfun_ln_Infinitesimal_less_zero";
+
+Goal "[| x : HInfinite; 0 < x |] ==> 0 < ( *f* ln) x";
+by (auto_tac (claset() addSIs [starfun_ln_gt_zero],simpset()
+ addsimps [HInfinite_def]));
+by (dres_inst_tac [("x","1")] bspec 1);
+by (auto_tac (claset(),simpset() addsimps [hrabs_def]));
+qed "starfun_ln_HInfinite_gt_zero";
+
+(*
+Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x";
+*)
+
+Goal "sumhr (0, whn, %n. (if even(n) then 0 else \
+\ ((- 1) ^ ((n - 1) div 2))/(real (fact n))) * x ^ n) \
+\ : HFinite";
+by (auto_tac (claset() addSIs [NSBseq_HFinite_hypreal,NSconvergent_NSBseq],
+ simpset() addsimps [starfunNat_sumr RS sym,starfunNat,hypnat_omega_def,
+ convergent_NSconvergent_iff RS sym, summable_convergent_sumr_iff RS sym]));
+by (rtac (CLAIM "1 = Suc 0" RS ssubst) 1);
+by (rtac summable_sin 1);
+qed "HFinite_sin";
+Addsimps [HFinite_sin];
+
+Goal "( *f* sin) 0 = 0";
+by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_zero_num]));
+qed "STAR_sin_zero";
+Addsimps [STAR_sin_zero];
+
+Goal "x : Infinitesimal ==> ( *f* sin) x @= x";
+by (case_tac "x = 0" 1);
+by (cut_inst_tac [("x","0")] DERIV_sin 2);
+by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym,
+ nsderiv_def,hypreal_of_real_zero]));
+by (dres_inst_tac [("x","x")] bspec 1);
+by Auto_tac;
+by (dres_inst_tac [("c","x")] approx_mult1 1);
+by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
+ simpset() addsimps [hypreal_mult_assoc]));
+qed "STAR_sin_Infinitesimal";
+Addsimps [STAR_sin_Infinitesimal];
+
+Goal "sumhr (0, whn, %n. (if even(n) then \
+\ ((- 1) ^ (n div 2))/(real (fact n)) else \
+\ 0) * x ^ n) : HFinite";
+by (auto_tac (claset() addSIs [NSBseq_HFinite_hypreal,NSconvergent_NSBseq],
+ simpset() addsimps [starfunNat_sumr RS sym,starfunNat,hypnat_omega_def,
+ convergent_NSconvergent_iff RS sym, summable_convergent_sumr_iff RS sym,
+ summable_cos]));
+qed "HFinite_cos";
+Addsimps [HFinite_cos];
+
+Goal "( *f* cos) 0 = 1";
+by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_zero_num,
+ hypreal_one_num]));
+qed "STAR_cos_zero";
+Addsimps [STAR_cos_zero];
+
+Goal "x : Infinitesimal ==> ( *f* cos) x @= 1";
+by (case_tac "x = 0" 1);
+by (cut_inst_tac [("x","0")] DERIV_cos 2);
+by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym,
+ nsderiv_def,hypreal_of_real_zero]));
+by (dres_inst_tac [("x","x")] bspec 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_zero,
+ hypreal_of_real_one]));
+by (dres_inst_tac [("c","x")] approx_mult1 1);
+by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
+ simpset() addsimps [hypreal_mult_assoc,hypreal_of_real_one]));
+by (res_inst_tac [("d","-1")] approx_add_right_cancel 1);
+by Auto_tac;
+qed "STAR_cos_Infinitesimal";
+Addsimps [STAR_cos_Infinitesimal];
+
+Goal "( *f* tan) 0 = 0";
+by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_zero_num]));
+qed "STAR_tan_zero";
+Addsimps [STAR_tan_zero];
+
+Goal "x : Infinitesimal ==> ( *f* tan) x @= x";
+by (case_tac "x = 0" 1);
+by (cut_inst_tac [("x","0")] DERIV_tan 2);
+by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym,
+ nsderiv_def,hypreal_of_real_zero]));
+by (dres_inst_tac [("x","x")] bspec 1);
+by Auto_tac;
+by (dres_inst_tac [("c","x")] approx_mult1 1);
+by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
+ simpset() addsimps [hypreal_mult_assoc]));
+qed "STAR_tan_Infinitesimal";
+
+Goal "x : Infinitesimal ==> ( *f* sin) x * ( *f* cos) x @= x";
+by (rtac (simplify (simpset()) (read_instantiate
+ [("d","1")] approx_mult_HFinite)) 1);
+by (auto_tac (claset(),simpset() addsimps [Infinitesimal_subset_HFinite
+ RS subsetD]));
+qed "STAR_sin_cos_Infinitesimal_mult";
+
+Goal "hypreal_of_real pi : HFinite";
+by (Simp_tac 1);
+qed "HFinite_pi";
+
+(* lemmas *)
+
+Goal "N : HNatInfinite \
+\ ==> hypreal_of_real a = \
+\ hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)";
+by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,
+ HNatInfinite_not_eq_zero]));
+val lemma_split_hypreal_of_real = result();
+
+Goal "[|x : Infinitesimal; x ~= 0 |] ==> ( *f* sin) x/x @= 1";
+by (cut_inst_tac [("x","0")] DERIV_sin 1);
+by (auto_tac (claset(),simpset() addsimps [NSDERIV_DERIV_iff RS sym,
+ nsderiv_def,hypreal_of_real_zero,hypreal_of_real_one]));
+qed "STAR_sin_Infinitesimal_divide";
+
+(*------------------------------------------------------------------------*)
+(* sin* (1/n) * 1/(1/n) @= 1 for n = oo *)
+(*------------------------------------------------------------------------*)
+
+Goal "n : HNatInfinite \
+\ ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) @= 1";
+by (rtac STAR_sin_Infinitesimal_divide 1);
+by Auto_tac;
+val lemma_sin_pi = result();
+
+Goal "n : HNatInfinite \
+\ ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1";
+by (forward_tac [lemma_sin_pi] 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_divide_def]));
+qed "STAR_sin_inverse_HNatInfinite";
+
+Goalw [hypreal_divide_def]
+ "N : HNatInfinite \
+\ ==> hypreal_of_real pi/(hypreal_of_hypnat N) : Infinitesimal";
+by (auto_tac (claset() addIs [Infinitesimal_HFinite_mult2],simpset()));
+qed "Infinitesimal_pi_divide_HNatInfinite";
+
+Goal "N : HNatInfinite \
+\ ==> hypreal_of_real pi/(hypreal_of_hypnat N) ~= 0";
+by Auto_tac;
+qed "pi_divide_HNatInfinite_not_zero";
+Addsimps [pi_divide_HNatInfinite_not_zero];
+
+Goal "n : HNatInfinite \
+\ ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n \
+\ @= hypreal_of_real pi";
+by (ftac ([Infinitesimal_pi_divide_HNatInfinite,pi_divide_HNatInfinite_not_zero]
+ MRS STAR_sin_Infinitesimal_divide) 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_inverse_distrib]));
+by (res_inst_tac [("a","inverse(hypreal_of_real pi)")] approx_SReal_mult_cancel 1);
+by (auto_tac (claset() addIs [SReal_inverse],simpset() addsimps [hypreal_divide_def] @
+ hypreal_mult_ac));
+qed "STAR_sin_pi_divide_HNatInfinite_approx_pi";
+
+Goal "n : HNatInfinite \
+\ ==> hypreal_of_hypnat n * \
+\ ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) \
+\ @= hypreal_of_real pi";
+by (rtac (hypreal_mult_commute RS subst) 1);
+by (etac STAR_sin_pi_divide_HNatInfinite_approx_pi 1);
+qed "STAR_sin_pi_divide_HNatInfinite_approx_pi2";
+
+(*** more theorems ***)
+
+Goalw [real_divide_def]
+ "N : HNatInfinite \
+\ ==> ( *fNat* (%x. pi / real x)) N : Infinitesimal";
+by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2],
+ simpset() addsimps [starfunNat_mult RS sym,starfunNat_inverse RS sym,
+ starfunNat_real_of_nat]));
+qed "starfunNat_pi_divide_n_Infinitesimal";
+
+Goal "N : HNatInfinite ==> \
+\ ( *f* sin) (( *fNat* (%x. pi / real x)) N) @= \
+\ hypreal_of_real pi/(hypreal_of_hypnat N)";
+by (auto_tac (claset() addSIs [STAR_sin_Infinitesimal,
+ Infinitesimal_HFinite_mult2],simpset() addsimps [starfunNat_mult RS sym,
+ hypreal_divide_def,real_divide_def,starfunNat_inverse_real_of_nat_eq]));
+qed "STAR_sin_pi_divide_n_approx";
+
+(*** move to NSA ***)
+Goalw [hypnat_zero_def] "(n <= (0::hypnat)) = (n = 0)";
+by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
+by (auto_tac (claset(),simpset() addsimps [hypnat_le]));
+qed "hypnat_le_zero_cancel";
+AddIffs [hypnat_le_zero_cancel];
+
+Goal "N : HNatInfinite ==> 0 < hypreal_of_hypnat N";
+by (rtac ccontr 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_of_hypnat_zero RS sym,
+ symmetric hypnat_le_def]));
+qed "HNatInfinite_hypreal_of_hypnat_gt_zero";
+
+bind_thm ("HNatInfinite_hypreal_of_hypnat_not_eq_zero",
+ HNatInfinite_hypreal_of_hypnat_gt_zero RS hypreal_not_refl2 RS not_sym);
+(*** END: move to NSA ***)
+
+Goalw [NSLIMSEQ_def] "(%n. real n * sin (pi / real n)) ----NS> pi";
+by (auto_tac (claset(),simpset() addsimps [starfunNat_mult RS sym,
+ starfunNat_real_of_nat]));
+by (res_inst_tac [("f1","sin")] (starfun_stafunNat_o2 RS subst) 1);
+by (auto_tac (claset(),simpset() addsimps [starfunNat_mult RS sym,
+ starfunNat_real_of_nat,real_divide_def]));
+by (res_inst_tac [("f1","inverse")] (starfun_stafunNat_o2 RS subst) 1);
+by (auto_tac (claset() addDs [STAR_sin_pi_divide_HNatInfinite_approx_pi],
+ simpset() addsimps [starfunNat_real_of_nat,hypreal_mult_commute,
+ symmetric hypreal_divide_def]));
+qed "NSLIMSEQ_sin_pi";
+
+Goalw [NSLIMSEQ_def] "(%n. cos (pi / real n))----NS> 1";
+by Auto_tac;
+by (res_inst_tac [("f1","cos")] (starfun_stafunNat_o2 RS subst) 1);
+by (rtac STAR_cos_Infinitesimal 1);
+by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2],
+ simpset() addsimps [starfunNat_mult RS sym,real_divide_def,
+ starfunNat_inverse RS sym,starfunNat_real_of_nat]));
+qed "NSLIMSEQ_cos_one";
+
+Goal "(%n. real n * sin (pi / real n) * cos (pi / real n)) ----NS> pi";
+by (rtac (simplify (simpset())
+ ([NSLIMSEQ_sin_pi,NSLIMSEQ_cos_one] MRS NSLIMSEQ_mult)) 1);
+qed "NSLIMSEQ_sin_cos_pi";
+
+(*------------------------------------------------------------------------*)
+(* A familiar approximation to cos x when x is small *)
+(*------------------------------------------------------------------------*)
+
+Goal "x : Infinitesimal ==> ( *f* cos) x @= 1 - x ^ 2";
+by (rtac (STAR_cos_Infinitesimal RS approx_trans) 1);
+by (auto_tac (claset(),simpset() addsimps [Infinitesimal_approx_minus RS sym,
+ hypreal_diff_def,hypreal_add_assoc RS sym,two_eq_Suc_Suc]));
+qed "STAR_cos_Infinitesimal_approx";
+
+(* move to NSA *)
+Goalw [hypreal_divide_def]
+ "[| x : Infinitesimal; y : Reals; y ~= 0 |] ==> x/y : Infinitesimal";
+by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult]
+ addSDs [SReal_inverse RS (SReal_subset_HFinite RS subsetD)],simpset()));
+qed "Infinitesimal_SReal_divide";
+
+Goal "x : Infinitesimal ==> ( *f* cos) x @= 1 - (x ^ 2)/2";
+by (rtac (STAR_cos_Infinitesimal RS approx_trans) 1);
+by (auto_tac (claset() addIs [Infinitesimal_SReal_divide],
+ simpset() addsimps [Infinitesimal_approx_minus RS sym,
+ two_eq_Suc_Suc]));
+qed "STAR_cos_Infinitesimal_approx2";
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/HTranscendental.thy Mon May 05 18:23:40 2003 +0200
@@ -0,0 +1,23 @@
+(* Title : HTranscendental.thy
+ Author : Jacques D. Fleuriot
+ Copyright : 2001 University of Edinburgh
+ Description : Nonstandard extensions of transcendental functions
+*)
+
+HTranscendental = Transcendental + IntFloor +
+
+constdefs
+
+
+ (* define exponential function using standard part *)
+ exphr :: real => hypreal
+ "exphr x == st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))"
+
+ 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 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
--- a/src/HOL/Hyperreal/Hyperreal.thy Mon May 05 18:22:31 2003 +0200
+++ b/src/HOL/Hyperreal/Hyperreal.thy Mon May 05 18:23:40 2003 +0200
@@ -1,4 +1,12 @@
+(* Title: HOL/Hyperreal/Hyperreal.thy
+ ID: $Id$
+ Author: Jacques Fleuriot, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
-theory Hyperreal = Poly + MacLaurin:
+Construction of the Hyperreals by the Ultrapower Construction
+and mechanization of Nonstandard Real Analysis
+*)
+
+theory Hyperreal = Poly + MacLaurin + HLog:
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/IntFloor.ML Mon May 05 18:23:40 2003 +0200
@@ -0,0 +1,315 @@
+(* Title: IntFloor.ML
+ Author: Jacques D. Fleuriot
+ Copyright: 2001,2002 University of Edinburgh
+ Description: Floor and ceiling operations over reals
+*)
+
+Goal "((number_of n) < real (m::int)) = (number_of n < m)";
+by Auto_tac;
+by (rtac (real_of_int_less_iff RS iffD1) 1);
+by (dtac (real_of_int_less_iff RS iffD2) 2);
+by Auto_tac;
+qed "number_of_less_real_of_int_iff";
+Addsimps [number_of_less_real_of_int_iff];
+
+Goal "(real (m::int) < (number_of n)) = (m < number_of n)";
+by Auto_tac;
+by (rtac (real_of_int_less_iff RS iffD1) 1);
+by (dtac (real_of_int_less_iff RS iffD2) 2);
+by Auto_tac;
+qed "number_of_less_real_of_int_iff2";
+Addsimps [number_of_less_real_of_int_iff2];
+
+Goalw [real_le_def,zle_def]
+ "((number_of n) <= real (m::int)) = (number_of n <= m)";
+by Auto_tac;
+qed "number_of_le_real_of_int_iff";
+Addsimps [number_of_le_real_of_int_iff];
+
+Goalw [real_le_def,zle_def]
+ "(real (m::int) <= (number_of n)) = (m <= number_of n)";
+by Auto_tac;
+qed "number_of_le_real_of_int_iff2";
+Addsimps [number_of_le_real_of_int_iff2];
+
+Goalw [floor_def] "floor 0 = 0";
+by (rtac Least_equality 1);
+by Auto_tac;
+qed "floor_zero";
+Addsimps [floor_zero];
+
+Goal "floor (real (0::nat)) = 0";
+by Auto_tac;
+qed "floor_real_of_nat_zero";
+Addsimps [floor_real_of_nat_zero];
+
+Goalw [floor_def] "floor (real (n::nat)) = int n";
+by (rtac Least_equality 1);
+by (dtac (real_of_int_real_of_nat RS ssubst) 2);
+by (dtac (real_of_int_less_iff RS iffD1) 2);
+by (auto_tac (claset(),simpset() addsimps [real_of_int_real_of_nat]));
+qed "floor_real_of_nat";
+Addsimps [floor_real_of_nat];
+
+Goalw [floor_def] "floor (- real (n::nat)) = - int n";
+by (rtac Least_equality 1);
+by (dtac (real_of_int_real_of_nat RS ssubst) 2);
+by (dtac (real_of_int_minus RS subst) 2);
+by (dtac (real_of_int_less_iff RS iffD1) 2);
+by (auto_tac (claset(),simpset() addsimps [real_of_int_real_of_nat]));
+qed "floor_minus_real_of_nat";
+Addsimps [floor_minus_real_of_nat];
+
+Goalw [floor_def] "floor (real (n::int)) = n";
+by (rtac Least_equality 1);
+by (dtac (real_of_int_real_of_nat RS ssubst) 2);
+by (dtac (real_of_int_less_iff RS iffD1) 2);
+by Auto_tac;
+qed "floor_real_of_int";
+Addsimps [floor_real_of_int];
+
+Goalw [floor_def] "floor (- real (n::int)) = - n";
+by (rtac Least_equality 1);
+by (dtac (real_of_int_minus RS subst) 2);
+by (dtac (real_of_int_real_of_nat RS ssubst) 2);
+by (dtac (real_of_int_less_iff RS iffD1) 2);
+by Auto_tac;
+qed "floor_minus_real_of_int";
+Addsimps [floor_minus_real_of_int];
+
+Goal "0 <= r ==> EX (n::nat). real (n - 1) <= r & r < real (n)";
+by (cut_inst_tac [("x","r")] reals_Archimedean2 1);
+by (Step_tac 1);
+by (forw_inst_tac [("P","%k. r < real k"),("k","n"),("m","%x. x")]
+ (thm "ex_has_least_nat") 1);
+by Auto_tac;
+by (res_inst_tac [("x","x")] exI 1);
+by (dres_inst_tac [("x","x - 1")] spec 1);
+by (auto_tac (claset() addDs [ARITH_PROVE "x <= x - Suc 0 ==> x = (0::nat)"],
+ simpset()));
+qed "reals_Archimedean6";
+
+Goal "0 <= r ==> EX n. real (n) <= r & r < real (Suc n)";
+by (dtac reals_Archimedean6 1);
+by Auto_tac;
+by (res_inst_tac [("x","n - 1")] exI 1);
+by (subgoal_tac "0 < n" 1);
+by (dtac order_le_less_trans 2);
+by Auto_tac;
+qed "reals_Archimedean6a";
+
+Goal "0 <= r ==> EX n. real n <= r & r < real ((n::int) + 1)";
+by (dtac reals_Archimedean6a 1);
+by Auto_tac;
+by (res_inst_tac [("x","int n")] exI 1);
+by (auto_tac (claset(),simpset() addsimps [real_of_int_real_of_nat,
+ real_of_nat_Suc]));
+qed "reals_Archimedean_6b_int";
+
+Goal "r < 0 ==> EX n. real n <= r & r < real ((n::int) + 1)";
+by (dtac (CLAIM "r < (0::real) ==> 0 <= -r") 1);
+by (dtac reals_Archimedean_6b_int 1);
+by Auto_tac;
+by (dtac real_le_imp_less_or_eq 1 THEN Auto_tac);
+by (res_inst_tac [("x","- n - 1")] exI 1);
+by (res_inst_tac [("x","- n")] exI 2);
+by Auto_tac;
+qed "reals_Archimedean_6c_int";
+
+Goal " EX (n::int). real n <= r & r < real ((n::int) + 1)";
+by (cut_inst_tac [("r","r")] (CLAIM "0 <= r | r < (0::real)") 1);
+by (blast_tac (claset() addIs [reals_Archimedean_6b_int,
+ reals_Archimedean_6c_int]) 1);
+qed "real_lb_ub_int";
+
+Goal "[| real n <= r; r < real y + 1 |] ==> n <= (y::int)";
+by (dres_inst_tac [("x","real n"),("z","real y + 1")] order_le_less_trans 1);
+by (rotate_tac 1 2);
+by (dtac ((CLAIM "real (1::int) = 1") RS ssubst) 2);
+by (rotate_tac 1 2);
+by (dres_inst_tac [("x1","y")] (real_of_int_add RS subst) 2);
+by (dtac (real_of_int_less_iff RS iffD1) 2);
+by Auto_tac;
+val lemma_floor = result();
+
+Goalw [floor_def,Least_def] "real (floor r) <= r";
+by (cut_inst_tac [("r","r")] real_lb_ub_int 1 THEN Step_tac 1);
+by (rtac theI2 1);
+by Auto_tac;
+by (blast_tac (claset() addIs [lemma_floor]) 1);
+by (ALLGOALS(dres_inst_tac [("x","n")] spec) THEN Auto_tac);
+by (force_tac (claset() addDs [lemma_floor],simpset()) 1);
+by (dtac (real_of_int_le_iff RS iffD2) 1);
+by (blast_tac (claset() addIs [real_le_trans]) 1);
+qed "real_of_int_floor_le";
+Addsimps [real_of_int_floor_le];
+
+Goalw [floor_def,Least_def]
+ "x < y ==> floor x <= floor y";
+by (cut_inst_tac [("r","x")] real_lb_ub_int 1 THEN Step_tac 1);
+by (cut_inst_tac [("r","y")] real_lb_ub_int 1 THEN Step_tac 1);
+by (rtac theI2 1);
+by (rtac theI2 3);
+by Auto_tac;
+by (auto_tac (claset() addIs [lemma_floor],simpset()));
+by (ALLGOALS(force_tac (claset() addDs [lemma_floor],simpset())));
+qed "floor_le";
+
+Goal "x <= y ==> floor x <= floor y";
+by (auto_tac (claset() addDs [real_le_imp_less_or_eq],simpset()
+ addsimps [floor_le]));
+qed "floor_le2";
+
+Goal "real na < real (x::int) + 1 ==> na <= x";
+by (auto_tac (claset() addIs [lemma_floor],simpset()));
+val lemma_floor2 = result();
+
+Goalw [floor_def,Least_def]
+ "(real (floor x) = x) = (EX (n::int). x = real n)";
+by (cut_inst_tac [("r","x")] real_lb_ub_int 1 THEN etac exE 1);
+by (rtac theI2 1);
+by (auto_tac (claset() addIs [lemma_floor],simpset()));
+by (force_tac (claset() addDs [lemma_floor],simpset()) 1);
+by (force_tac (claset() addDs [lemma_floor2],simpset()) 1);
+qed "real_of_int_floor_cancel";
+Addsimps [real_of_int_floor_cancel];
+
+Goalw [floor_def]
+ "[| real n < x; x < real n + 1 |] ==> floor x = n";
+by (rtac Least_equality 1);
+by (auto_tac (claset() addIs [lemma_floor],simpset()));
+qed "floor_eq";
+
+Goalw [floor_def]
+ "[| real n <= x; x < real n + 1 |] ==> floor x = n";
+by (rtac Least_equality 1);
+by (auto_tac (claset() addIs [lemma_floor],simpset()));
+qed "floor_eq2";
+
+Goal "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n";
+by (rtac (inj_int RS injD) 1);
+by (rtac (CLAIM "0 <= x ==> int (nat x) = x" RS ssubst) 1);
+by (rtac floor_eq 2);
+by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc,
+ real_of_int_real_of_nat]));
+by (rtac (floor_le RSN (2,zle_trans)) 1 THEN Auto_tac);
+qed "floor_eq3";
+
+Goal "[| real n <= x; x < real (Suc n) |] ==> nat(floor x) = n";
+by (dtac order_le_imp_less_or_eq 1);
+by (auto_tac (claset() addIs [floor_eq3],simpset()));
+qed "floor_eq4";
+
+Goalw [real_number_of_def]
+ "floor(number_of n :: real) = (number_of n :: int)";
+by (rtac floor_eq2 1);
+by (rtac (CLAIM "x < x + (1::real)") 2);
+by (rtac real_le_refl 1);
+qed "floor_number_of_eq";
+Addsimps [floor_number_of_eq];
+
+Goalw [floor_def,Least_def] "r - 1 <= real(floor r)";
+by (cut_inst_tac [("r","r")] real_lb_ub_int 1 THEN Step_tac 1);
+by (rtac theI2 1);
+by (auto_tac (claset() addIs [lemma_floor],simpset()));
+by (force_tac (claset() addDs [lemma_floor],simpset()) 1);
+qed "real_of_int_floor_ge_diff_one";
+Addsimps [real_of_int_floor_ge_diff_one];
+
+Goal "r <= real(floor r) + 1";
+by (cut_inst_tac [("r","r")] real_of_int_floor_ge_diff_one 1);
+by (auto_tac (claset(),simpset() delsimps [real_of_int_floor_ge_diff_one]));
+qed "real_of_int_floor_add_one_ge";
+Addsimps [real_of_int_floor_add_one_ge];
+
+
+(*--------------------------------------------------------------------------------*)
+(* ceiling function for positive reals *)
+(*--------------------------------------------------------------------------------*)
+
+Goalw [ceiling_def] "ceiling 0 = 0";
+by Auto_tac;
+qed "ceiling_zero";
+Addsimps [ceiling_zero];
+
+Goalw [ceiling_def] "ceiling (real (n::nat)) = int n";
+by Auto_tac;
+qed "ceiling_real_of_nat";
+Addsimps [ceiling_real_of_nat];
+
+Goal "ceiling (real (0::nat)) = 0";
+by Auto_tac;
+qed "ceiling_real_of_nat_zero";
+Addsimps [ceiling_real_of_nat_zero];
+
+Goalw [ceiling_def] "ceiling (real (floor r)) = floor r";
+by Auto_tac;
+qed "ceiling_floor";
+Addsimps [ceiling_floor];
+
+Goalw [ceiling_def] "floor (real (ceiling r)) = ceiling r";
+by Auto_tac;
+qed "floor_ceiling";
+Addsimps [floor_ceiling];
+
+Goalw [ceiling_def] "r <= real (ceiling r)";
+by Auto_tac;
+by (rtac (CLAIM "x <= -y ==> (y::real) <= - x") 1);
+by Auto_tac;
+qed "real_of_int_ceiling_ge";
+Addsimps [real_of_int_ceiling_ge];
+
+Goalw [ceiling_def] "x < y ==> ceiling x <= ceiling y";
+by (auto_tac (claset() addIs [floor_le],simpset()));
+qed "ceiling_le";
+
+Goalw [ceiling_def] "x <= y ==> ceiling x <= ceiling y";
+by (auto_tac (claset() addIs [floor_le2],simpset()));
+qed "ceiling_le2";
+
+Goalw [ceiling_def] "(real (ceiling x) = x) = (EX (n::int). x = real n)";
+by Auto_tac;
+by (dtac (CLAIM "- x = y ==> (x::real) = -y") 1);
+by Auto_tac;
+by (res_inst_tac [("x","-n")] exI 1);
+by Auto_tac;
+qed "real_of_int_ceiling_cancel";
+Addsimps [real_of_int_ceiling_cancel];
+
+Goalw [ceiling_def]
+ "[| real n < x; x < real n + 1 |] ==> ceiling x = n + 1";
+by (rtac (CLAIM "x = - y ==> - (x::int) = y") 1);
+by (auto_tac (claset() addIs [floor_eq],simpset()));
+qed "ceiling_eq";
+
+Goalw [ceiling_def]
+ "[| real n < x; x <= real n + 1 |] ==> ceiling x = n + 1";
+by (rtac (CLAIM "x = - y ==> - (x::int) = y") 1);
+by (auto_tac (claset() addIs [floor_eq2],simpset()));
+qed "ceiling_eq2";
+
+Goalw [ceiling_def] "[| real n - 1 < x; x <= real n |] ==> ceiling x = n";
+by (rtac (CLAIM "x = -(y::int) ==> - x = y") 1);
+by (auto_tac (claset() addIs [floor_eq2],simpset()));
+qed "ceiling_eq3";
+
+Goalw [ceiling_def,real_number_of_def]
+ "ceiling (number_of n :: real) = (number_of n :: int)";
+by (rtac (CLAIM "x = - y ==> - (x::int) = y") 1);
+by (rtac (floor_minus_real_of_int RS ssubst) 1);
+by Auto_tac;
+qed "ceiling_number_of_eq";
+Addsimps [ceiling_number_of_eq];
+
+Goalw [ceiling_def] "real (ceiling r) - 1 <= r";
+by (rtac (CLAIM "-x <= -y ==> (y::real) <= x") 1);
+by (auto_tac (claset(),simpset() addsimps [real_diff_def]));
+qed "real_of_int_ceiling_diff_one_le";
+Addsimps [real_of_int_ceiling_diff_one_le];
+
+Goal "real (ceiling r) <= r + 1";
+by (cut_inst_tac [("r","r")] real_of_int_ceiling_diff_one_le 1);
+by (auto_tac (claset(),simpset() delsimps [real_of_int_ceiling_diff_one_le]));
+qed "real_of_int_ceiling_le_add_one";
+Addsimps [real_of_int_ceiling_le_add_one];
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/IntFloor.thy Mon May 05 18:23:40 2003 +0200
@@ -0,0 +1,17 @@
+(* Title: IntFloor.thy
+ Author: Jacques D. Fleuriot
+ Copyright: 2001,2002 University of Edinburgh
+ Description: Floor and ceiling operations over reals
+*)
+
+IntFloor = Integration +
+
+constdefs
+
+ floor :: real => int
+ "floor r == (LEAST n. r < real (n + (1::int)))"
+
+ ceiling :: real => int
+ "ceiling r == - floor (- r)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/Integration.ML Mon May 05 18:23:40 2003 +0200
@@ -0,0 +1,1070 @@
+(* Title : Integration.ML
+ Author : Jacques D. Fleuriot
+ Copyright : 2000 University of Edinburgh
+ Description : Theory of integration (c.f. Harison's HOL development)
+*)
+
+Goalw [psize_def] "a = b ==> psize (%n. if n = 0 then a else b) = 0";
+by Auto_tac;
+qed "partition_zero";
+Addsimps [partition_zero];
+
+Goalw [psize_def] "a < b ==> psize (%n. if n = 0 then a else b) = 1";
+by Auto_tac;
+by (rtac some_equality 1);
+by Auto_tac;
+by (dres_inst_tac [("x","1")] spec 1);
+by Auto_tac;
+qed "partition_one";
+Addsimps [partition_one];
+
+Goalw [partition_def]
+ "a <= b ==> partition(a,b)(%n. if n = 0 then a else b)";
+by (auto_tac (claset(),simpset() addsimps [real_le_less]));
+qed "partition_single";
+Addsimps [partition_single];
+
+Goalw [partition_def] "partition(a,b) D ==> (D(0) = a)";
+by Auto_tac;
+qed "partition_lhs";
+
+Goalw [partition_def]
+ "(partition(a,b) D) = \
+\ ((D 0 = a) & \
+\ (ALL n. n < (psize D) --> D n < D(Suc n)) & \
+\ (ALL n. (psize D) <= n --> (D n = b)))";
+by Auto_tac;
+by (ALLGOALS(subgoal_tac "psize D = N"));
+by Auto_tac;
+by (ALLGOALS(simp_tac (simpset() addsimps [psize_def])));
+by (ALLGOALS(rtac some_equality));
+by (Blast_tac 1 THEN Blast_tac 2);
+by (ALLGOALS(rtac ccontr));
+by (ALLGOALS(dtac (ARITH_PROVE "n ~= (N::nat) ==> n < N | N < n")));
+by (Step_tac 1);
+by (dres_inst_tac [("x","Na")] spec 1);
+by (rotate_tac 3 1);
+by (dres_inst_tac [("x","Suc Na")] spec 1);
+by (Asm_full_simp_tac 1);
+by (rotate_tac 2 1);
+by (dres_inst_tac [("x","N")] spec 1);
+by (Asm_full_simp_tac 1);
+by (dres_inst_tac [("x","Na")] spec 1);
+by (rotate_tac 3 1);
+by (dres_inst_tac [("x","Suc Na")] spec 1);
+by (Asm_full_simp_tac 1);
+by (rotate_tac 2 1);
+by (dres_inst_tac [("x","N")] spec 1);
+by (Asm_full_simp_tac 1);
+qed "partition";
+
+Goal "partition(a,b) D ==> (D(psize D) = b)";
+by (dtac (partition RS subst) 1);
+by (Step_tac 1);
+by (REPEAT(dres_inst_tac [("x","psize D")] spec 1));
+by Auto_tac;
+qed "partition_rhs";
+
+Goal "[|partition(a,b) D; psize D <= n |] ==> (D n = b)";
+by (dtac (partition RS subst) 1);
+by (Blast_tac 1);
+qed "partition_rhs2";
+
+Goal
+ "partition(a,b) D & m + Suc d <= n & n <= (psize D) --> D(m) < D(m + Suc d)";
+by (induct_tac "d" 1);
+by Auto_tac;
+by (ALLGOALS(dtac (partition RS subst)));
+by (Step_tac 1);
+by (ALLGOALS(dtac (ARITH_PROVE "Suc m <= n ==> m < n")));
+by (ALLGOALS(dtac less_le_trans));
+by (assume_tac 1 THEN assume_tac 2);
+by (ALLGOALS(blast_tac (claset() addIs [real_less_trans])));
+qed_spec_mp "lemma_partition_lt_gen";
+
+Goal "m < n ==> EX d. n = m + Suc d";
+by (auto_tac (claset(),simpset() addsimps [less_iff_Suc_add]));
+qed "less_eq_add_Suc";
+
+Goal "[|partition(a,b) D; m < n; n <= (psize D)|] ==> D(m) < D(n)";
+by (auto_tac (claset() addDs [less_eq_add_Suc] addIs [lemma_partition_lt_gen],
+ simpset()));
+qed "partition_lt_gen";
+
+Goal "partition(a,b) D ==> (n < (psize D) --> D(0) < D(Suc n))";
+by (dtac (partition RS subst) 1);
+by (induct_tac "n" 1);
+by (Blast_tac 1);
+by (blast_tac (claset() addSDs [leI] addDs
+ [(ARITH_PROVE "m <= n ==> m <= Suc n"),
+ le_less_trans,real_less_trans]) 1);
+qed_spec_mp "partition_lt";
+
+Goal "partition(a,b) D ==> a <= b";
+by (ftac (partition RS subst) 1);
+by (Step_tac 1);
+by (rotate_tac 2 1);
+by (dres_inst_tac [("x","psize D")] spec 1);
+by (Step_tac 1);
+by (rtac ccontr 1);
+by (case_tac "psize D = 0" 1);
+by (Step_tac 1);
+by (dres_inst_tac [("n","psize D - 1")] partition_lt 2);
+by Auto_tac;
+qed "partition_le";
+
+Goal "[|partition(a,b) D; n < (psize D)|] ==> D(n) < D(psize D)";
+by (auto_tac (claset() addIs [partition_lt_gen],simpset()));
+qed "partition_gt";
+
+Goal "partition(a,b) D ==> ((a = b) = (psize D = 0))";
+by (ftac (partition RS subst) 1);
+by (Step_tac 1);
+by (rotate_tac 2 1);
+by (dres_inst_tac [("x","psize D")] spec 1);
+by (rtac ccontr 1);
+by (dres_inst_tac [("n","psize D - 1")] partition_lt 1);
+by (Blast_tac 3 THEN Auto_tac);
+qed "partition_eq";
+
+Goal "partition(a,b) D ==> a <= D(r)";
+by (ftac (partition RS subst) 1);
+by (Step_tac 1);
+by (induct_tac "r" 1);
+by (cut_inst_tac [("m","Suc n"),("n","psize D")]
+ (ARITH_PROVE "m < n | n <= (m::nat)") 2);
+by (Step_tac 1);
+by (eres_inst_tac [("j","D n")] real_le_trans 1);
+by (dres_inst_tac [("x","n")] spec 1);
+by (blast_tac (claset() addIs [less_trans,order_less_imp_le]) 1);
+by (res_inst_tac [("j","b")] real_le_trans 1);
+by (etac partition_le 1);
+by (Blast_tac 1);
+qed "partition_lb";
+
+Goal "[| partition(a,b) D; psize D ~= 0 |] ==> a < D(Suc n)";
+by (res_inst_tac [("t","a")] (partition_lhs RS subst) 1);
+by (assume_tac 1);
+by (cut_inst_tac [("m","psize D"),("n","Suc n")]
+ (ARITH_PROVE "m < n | n <= (m::nat)") 1);
+by (ftac (partition RS subst) 1);
+by (Step_tac 1);
+by (rotate_tac 3 1);
+by (dres_inst_tac [("x","Suc n")] spec 1);
+by (etac impE 1);
+by (etac less_imp_le 1);
+by (ftac partition_rhs 1);
+by (dtac partition_gt 1 THEN assume_tac 1);
+by (Asm_simp_tac 1);
+by (blast_tac (claset() addIs [partition_lt,less_le_trans]) 1);
+qed "partition_lb_lt";
+
+Goal "partition(a,b) D ==> D(r) <= b";
+by (ftac (partition RS subst) 1);
+by (cut_inst_tac [("m","r"),("n","psize D")]
+ (ARITH_PROVE "m < n | n <= (m::nat)") 1);
+by (Step_tac 1);
+by (Blast_tac 2);
+by (subgoal_tac "ALL x. D((psize D) - x) <= b" 1);
+by (rotate_tac 4 1);
+by (dres_inst_tac [("x","psize D - r")] spec 1);
+by (dtac (ARITH_PROVE "p < m ==> m - (m - p) = (p::nat)") 1);
+by (thin_tac "ALL n. psize D <= n --> D n = b" 1);
+by (Asm_full_simp_tac 1);
+by (Step_tac 1);
+by (induct_tac "x" 1);
+by (Simp_tac 1 THEN Blast_tac 1);
+by (case_tac "psize D - Suc n = 0" 1);
+by (thin_tac "ALL n. psize D <= n --> D n = b" 1);
+by (asm_simp_tac (simpset() addsimps [partition_le]) 1);
+by (rtac real_le_trans 1 THEN assume_tac 2);
+by (rtac (ARITH_PROVE "0 < m - Suc n ==> (m - n) = Suc(m - Suc n)"
+ RS ssubst) 1);
+by (dres_inst_tac [("x","psize D - Suc n")] spec 2);
+by (thin_tac "ALL n. psize D <= n --> D n = b" 2);
+by (Asm_full_simp_tac 2);
+by (Blast_tac 1);
+qed "partition_ub";
+
+Goal "[| partition(a,b) D; n < psize D |] ==> D(n) < b";
+by (blast_tac (claset() addIs [partition_rhs RS subst] addIs
+ [partition_gt]) 1);
+qed "partition_ub_lt";
+
+Goal "[| partition (a, b) D1; partition (b, c) D2 |] \
+\ ==> (ALL n. \
+\ n < psize D1 + psize D2 --> \
+\ (if n < psize D1 then D1 n else D2 (n - psize D1)) \
+\ < (if Suc n < psize D1 then D1 (Suc n) \
+\ else D2 (Suc n - psize D1))) & \
+\ (ALL n. \
+\ psize D1 + psize D2 <= n --> \
+\ (if n < psize D1 then D1 n else D2 (n - psize D1)) = \
+\ (if psize D1 + psize D2 < psize D1 then D1 (psize D1 + psize D2) \
+\ else D2 (psize D1 + psize D2 - psize D1)))";
+by (Step_tac 1);
+by (auto_tac (claset() addIs [partition_lt_gen],simpset()));
+by (dres_inst_tac [("m","psize D1")]
+ (leI RSN(2,ARITH_PROVE "[| n < m; m <= Suc n |] ==> m = Suc n")) 1);
+by (assume_tac 1);
+by (auto_tac (claset() addSIs [partition_lt_gen],
+ simpset() addsimps [partition_lhs,partition_ub_lt]));
+by (blast_tac (claset() addIs [ARITH_PROVE "~n < m ==> n - m < Suc n - m"]) 1);
+by (auto_tac (claset(),simpset() addsimps [
+ ARITH_PROVE "~ n < m ==> (Suc n - m <= p) = (Suc n <= m + p)"]));
+by (dtac (ARITH_PROVE "p + q <= (n::nat) ==> q <= n - p") 1);
+by (auto_tac (claset() addSIs [partition_rhs2], simpset() addsimps
+ [partition_rhs]));
+qed "lemma_partition_append1";
+
+Goal "[| partition (a, b) D1; partition (b, c) D2; N < psize D1 |] \
+\ ==> D1(N) < D2 (psize D2)";
+by (res_inst_tac [("y","D1(psize D1)")] order_less_le_trans 1);
+by (etac partition_gt 1 THEN assume_tac 1);
+by (auto_tac (claset(),simpset() addsimps [partition_rhs,partition_le]));
+qed "lemma_psize1";
+
+Goal "[| partition (a, b) D1; partition (b, c) D2 |] \
+\ ==> psize (%n. if n < psize D1 then D1 n else D2 (n - psize D1)) = \
+\ psize D1 + psize D2";
+by (res_inst_tac
+ [("D2","%n. if n < psize D1 then D1 n else D2 (n - psize D1)")]
+ ((psize_def RS meta_eq_to_obj_eq) RS ssubst) 1);
+by (rtac some1_equality 1);
+by (blast_tac (claset() addSIs [lemma_partition_append1]) 2);
+by (rtac ex1I 1 THEN rtac lemma_partition_append1 1);
+by Auto_tac;
+by (rtac ccontr 1);
+by (dtac (ARITH_PROVE "m ~= n ==> m < n | n < (m::nat)") 1);
+by (Step_tac 1);
+by (rotate_tac 3 1);
+by (dres_inst_tac [("x","psize D1 + psize D2")] spec 1);
+by Auto_tac;
+by (case_tac "N < psize D1" 1);
+by (auto_tac (claset() addDs [lemma_psize1],simpset()));
+by (dtac leI 1);
+by (dtac (ARITH_PROVE "[|p <= n; n < p + m|] ==> n - p < (m::nat)") 1);
+by (assume_tac 1);
+by (dres_inst_tac [("a","b"),("b","c")] partition_gt 1);
+by Auto_tac;
+by (dres_inst_tac [("x","psize D1 + psize D2")] spec 1);
+by (auto_tac (claset(),simpset() addsimps [partition_rhs2]));
+qed "lemma_partition_append2";
+
+Goalw [tpart_def]
+"[|psize D = 0; tpart(a,b) (D,p)|] ==> a = b";
+by (auto_tac (claset(),simpset() addsimps [partition_eq]));
+qed "tpart_eq_lhs_rhs";
+
+Goalw [tpart_def] "tpart(a,b) (D,p) ==> partition(a,b) D";
+by Auto_tac;
+qed "tpart_partition";
+
+Goal "[| tpart(a,b) (D1,p1); fine(g) (D1,p1); \
+\ tpart(b,c) (D2,p2); fine(g) (D2,p2) |] \
+\ ==> EX D p. tpart(a,c) (D,p) & fine(g) (D,p)";
+by (res_inst_tac
+ [("x","%n. if n < psize D1 then D1 n else D2 (n - psize D1)")] exI 1);
+by (res_inst_tac
+ [("x","%n. if n < psize D1 then p1 n else p2 (n - psize D1)")] exI 1);
+by (cut_inst_tac [("m","psize D1")] (ARITH_PROVE "0 < (m::nat) | m = 0") 1);
+by (auto_tac (claset() addDs [tpart_eq_lhs_rhs],simpset()));
+by (asm_full_simp_tac (simpset() addsimps [fine_def,
+ [tpart_partition,tpart_partition] MRS lemma_partition_append2]) 2);
+by Auto_tac;
+by (dres_inst_tac [("m","psize D1"),("n","n")]
+ (leI RSN(2,ARITH_PROVE "[| n < m; m <= Suc n |] ==> m = Suc n")) 2);
+by Auto_tac;
+by (dtac (tpart_partition RS partition_rhs) 2);
+by (dtac (tpart_partition RS partition_lhs) 2);
+by Auto_tac;
+by (rotate_tac 3 2);
+by (dres_inst_tac [("x","n - psize D1")] spec 2);
+by (auto_tac (claset(),simpset() addsimps
+ [ARITH_PROVE "[| (0::nat) < p; p <= n |] ==> (n - p < m) = (n < p + m)",
+ ARITH_PROVE "~n < p ==> Suc n - p = Suc(n - p)"]));
+by (auto_tac (claset(),simpset() addsimps [tpart_def,
+ ARITH_PROVE "~n < p ==> Suc n - p = Suc(n - p)"]));
+by (dres_inst_tac [("m","psize D1"),("n","n")]
+ (leI RSN(2,ARITH_PROVE "[| n < m; m <= Suc n |] ==> m = Suc n")) 2);
+by Auto_tac;
+by (dtac partition_rhs 2);
+by (dtac partition_lhs 2);
+by Auto_tac;
+by (rtac (partition RS ssubst) 1);
+by (rtac (lemma_partition_append2 RS ssubst) 1);
+by (rtac conjI 3);
+by (dtac lemma_partition_append1 4);
+by (auto_tac (claset(),simpset() addsimps [partition_lhs,partition_rhs]));
+qed "partition_append";
+
+(* ------------------------------------------------------------------------ *)
+(* We can always find a division which is fine wrt any gauge *)
+(* ------------------------------------------------------------------------ *)
+
+Goal "[| a <= b; gauge(%x. a <= x & x <= b) g |] \
+\ ==> EX D p. tpart(a,b) (D,p) & fine g (D,p)";
+by (cut_inst_tac
+ [("P","%(u,v). a <= u & v <= b --> (EX D p. tpart(u,v) (D,p) & fine(g) (D,p))")]
+ lemma_BOLZANO2 1);
+by (Step_tac 1);
+by (REPEAT(blast_tac (claset() addIs [real_le_trans]) 1));
+by (auto_tac (claset() addIs [partition_append],simpset()));
+by (case_tac "a <= x & x <= b" 1);
+by (res_inst_tac [("x","1")] exI 2);
+by Auto_tac;
+by (res_inst_tac [("x","g x")] exI 1);
+by (auto_tac (claset(),simpset() addsimps [gauge_def]));
+by (res_inst_tac [("x","%n. if n = 0 then aa else ba")] exI 1);
+by (res_inst_tac [("x","%n. if n = 0 then x else ba")] exI 1);
+by (auto_tac (claset(),simpset() addsimps [tpart_def,fine_def]));
+qed "partition_exists";
+
+(* ------------------------------------------------------------------------ *)
+(* Lemmas about combining gauges *)
+(* ------------------------------------------------------------------------ *)
+
+Goalw [gauge_def]
+ "[| gauge(E) g1; gauge(E) g2 |] \
+\ ==> gauge(E) (%x. if g1(x) < g2(x) then g1(x) else g2(x))";
+by Auto_tac;
+qed "gauge_min";
+
+Goalw [fine_def]
+ "fine (%x. if g1(x) < g2(x) then g1(x) else g2(x)) (D,p) \
+\ ==> fine(g1) (D,p) & fine(g2) (D,p)";
+by (auto_tac (claset(),simpset() addsimps [split_if]));
+qed "fine_min";
+
+
+(* ------------------------------------------------------------------------ *)
+(* The integral is unique if it exists *)
+(* ------------------------------------------------------------------------ *)
+
+Goalw [Integral_def]
+ "[| a <= b; Integral(a,b) f k1; Integral(a,b) f k2 |] ==> k1 = k2";
+by Auto_tac;
+by (REPEAT(dres_inst_tac [("x","abs(k1 - k2)/2")] spec 1));
+by (Auto_tac THEN TRYALL(arith_tac));
+by (dtac gauge_min 1 THEN assume_tac 1);
+by (dres_inst_tac [("g","%x. if g x < ga x then g x else ga x")]
+ partition_exists 1 THEN assume_tac 1);
+by Auto_tac;
+by (dtac fine_min 1);
+by (REPEAT(dtac spec 1) THEN Auto_tac);
+by (subgoal_tac
+ "abs((rsum(D,p) f - k2) - (rsum(D,p) f - k1)) < abs(k1 - k2)" 1);
+by (arith_tac 1);
+by (dtac real_add_less_mono 1 THEN assume_tac 1);
+by (auto_tac (claset(),HOL_ss addsimps [real_add_mult_distrib RS sym,
+ real_mult_2_right RS sym,real_mult_less_cancel2]));
+by (ALLGOALS(arith_tac));
+qed "Integral_unique";
+
+Goalw [Integral_def] "Integral(a,a) f 0";
+by Auto_tac;
+by (res_inst_tac [("x","%x. 1")] exI 1);
+by (auto_tac (claset() addDs [partition_eq],simpset() addsimps [gauge_def,
+ tpart_def,rsum_def]));
+qed "Integral_zero";
+Addsimps [Integral_zero];
+
+Goal "sumr 0 m (%n. D (Suc n) - D n) = D(m) - D 0";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "sumr_partition_eq_diff_bounds";
+Addsimps [sumr_partition_eq_diff_bounds];
+
+Goal "a <= b ==> Integral(a,b) (%x. 1) (b - a)";
+by (dtac real_le_imp_less_or_eq 1 THEN Auto_tac);
+by (auto_tac (claset(),simpset() addsimps [rsum_def,Integral_def]));
+by (res_inst_tac [("x","%x. b - a")] exI 1);
+by (auto_tac (claset(),simpset() addsimps [gauge_def,
+ abs_interval_iff,tpart_def,partition]));
+qed "Integral_eq_diff_bounds";
+
+Goal "a <= b ==> Integral(a,b) (%x. c) (c*(b - a))";
+by (dtac real_le_imp_less_or_eq 1 THEN Auto_tac);
+by (auto_tac (claset(),simpset() addsimps [rsum_def,Integral_def]));
+by (res_inst_tac [("x","%x. b - a")] exI 1);
+by (auto_tac (claset(),simpset() addsimps
+ [sumr_mult RS sym,gauge_def,abs_interval_iff,
+ real_diff_mult_distrib2 RS sym,partition,tpart_def]));
+qed "Integral_mult_const";
+
+Goal "[| a <= b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)";
+by (dtac real_le_imp_less_or_eq 1);
+by (auto_tac (claset() addDs [[real_le_refl,Integral_zero] MRS Integral_unique],
+ simpset()));
+by (auto_tac (claset(),simpset() addsimps [rsum_def,Integral_def,
+ sumr_mult RS sym,real_mult_assoc]));
+by (res_inst_tac [("x2","c")] ((abs_ge_zero RS real_le_imp_less_or_eq)
+ RS disjE) 1);
+by (dtac sym 2);
+by (Asm_full_simp_tac 2 THEN Blast_tac 2);
+by (dres_inst_tac [("x","e/abs c")] spec 1 THEN Auto_tac);
+by (asm_full_simp_tac (simpset() addsimps [real_0_less_mult_iff,
+ real_divide_def]) 1);
+by (rtac exI 1 THEN Auto_tac);
+by (REPEAT(dtac spec 1) THEN Auto_tac);
+by (res_inst_tac [("z1","inverse(abs c)")] (real_mult_less_iff1 RS iffD1) 1);
+by (fold_tac [real_divide_def]);
+by (auto_tac (claset(),simpset() addsimps [real_diff_mult_distrib2
+ RS sym,abs_mult,real_mult_assoc RS sym,
+ ARITH_PROVE "c ~= 0 ==> abs (c::real) ~= 0",real_inverse_gt_0]));
+qed "Integral_mult";
+
+(* ------------------------------------------------------------------------ *)
+(* Fundamental theorem of calculus (Part I) *)
+(* ------------------------------------------------------------------------ *)
+
+(* "Straddle Lemma" : Swartz & Thompson: AMM 95(7) 1988 *)
+
+Goal "ALL x. P(x) --> (EX y. Q x y) ==> EX f. (ALL x. P(x) --> Q x (f x))";
+by (cut_inst_tac [("S","Collect (%x. P x)"),("Q","Q")] (CLAIM_SIMP
+ "(ALL x:S. (EX y. Q x y)) --> (EX f. (ALL x:S. Q x (f x)))" [bchoice]) 1);
+by Auto_tac;
+qed "choiceP";
+
+Goal "ALL x. P(x) --> (EX y. R(y) & (EX z. Q x y z)) ==> \
+\ EX f fa. (ALL x. P(x) --> R(f x) & Q x (f x) (fa x))";
+by (dtac (CLAIM "(ALL x. P(x) --> (EX y. R(y) & (EX z. Q x y z))) = \
+\ (ALL x. P(x) --> (EX y z. R(y) & Q x y z))" RS iffD1) 1);;
+by (dtac choiceP 1 THEN Step_tac 1);
+by (dtac choiceP 1 THEN Auto_tac);
+qed "choiceP2";
+
+Goal "ALL x. (EX y. R(y) & (EX z. Q x y z)) ==> \
+\ EX f fa. (ALL x. R(f x) & Q x (f x) (fa x))";
+by (dtac (CLAIM "(ALL x. (EX y. R(y) & (EX z. Q x y z))) = \
+\ (ALL x. (EX y z. R(y) & Q x y z))" RS iffD1) 1);;
+by (dtac choice 1 THEN Step_tac 1);
+by (dtac choice 1 THEN Auto_tac);
+qed "choice2";
+
+(* new simplifications e.g. (y < x/n) = (y * n < x) are a real nuisance
+ they break the original proofs and make new proofs longer! *)
+Goalw [gauge_def]
+ "[| ALL x. a <= x & x <= b --> DERIV f x :> f'(x); 0 < e |]\
+\ ==> EX g. gauge(%x. a <= x & x <= b) g & \
+\ (ALL x u v. a <= u & u <= x & x <= v & v <= b & (v - u) < g(x) \
+\ --> abs((f(v) - f(u)) - (f'(x) * (v - u))) <= e * (v - u))";
+by (subgoal_tac "ALL x. a <= x & x <= b --> \
+\ (EX d. 0 < d & \
+\ (ALL u v. u <= x & x <= v & (v - u) < d --> \
+\ abs((f(v) - f(u)) - (f'(x) * (v - u))) <= e * (v - u)))" 1);
+by (dtac choiceP 1);
+by Auto_tac;
+by (dtac spec 1 THEN Auto_tac);
+by (auto_tac (claset(),simpset() addsimps [DERIV_iff2,LIM_def]));
+by (dres_inst_tac [("x","e/2")] spec 1);
+by Auto_tac;
+by (subgoal_tac "ALL z. abs(z - x) < s --> \
+\ abs((f(z) - f(x)) - (f'(x) * (z - x))) <= (e / 2) * abs(z - x)" 1);
+by Auto_tac;
+by (case_tac "0 < abs(z - x)" 2);
+by (dtac (ARITH_PROVE "~ 0 < abs z ==> z = (0::real)") 3);
+by (asm_full_simp_tac (simpset() addsimps
+ [ARITH_PROVE "(z - x = 0) = (z = (x::real))"]) 3);
+by (dres_inst_tac [("x","z")] spec 2);
+by (res_inst_tac [("z1","abs(inverse(z - x))")]
+ (real_mult_le_cancel_iff2 RS iffD1) 2);
+by (Asm_full_simp_tac 2);
+by (asm_full_simp_tac (simpset() addsimps [abs_mult RS sym,
+ real_mult_assoc RS sym]) 2);
+by (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x)) = \
+\ (f z - f x)/(z - x) - f' x" 2);
+by (asm_full_simp_tac (simpset() addsimps [abs_mult RS sym] @ real_mult_ac) 2);
+by (asm_full_simp_tac (simpset() addsimps [real_diff_def]) 2);
+by (rtac (real_mult_commute RS subst) 2);
+by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib,
+ real_diff_def]) 2);
+by (dtac (CLAIM "z ~= x ==> z + -x ~= (0::real)") 2);
+by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc,
+ real_divide_def]) 2);
+by (simp_tac (simpset() addsimps [real_add_mult_distrib]) 2);
+by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac);
+by (res_inst_tac [("u1","u"),("v1","v")] (ARITH_PROVE "u < v | v <= (u::real)"
+ RS disjE) 1);
+by (dres_inst_tac [("x","v")] real_le_imp_less_or_eq 2);
+by Auto_tac;
+(*29*)
+by (res_inst_tac [("j","abs((f(v) - f(x)) - (f'(x) * (v - x))) + \
+\ abs((f(x) - f(u)) - (f'(x) * (x - u)))")] real_le_trans 1);
+by (rtac (abs_triangle_ineq RSN (2,real_le_trans)) 1);
+by (asm_full_simp_tac (simpset() addsimps [real_diff_mult_distrib2]) 1);
+by (arith_tac 1);
+by (res_inst_tac [("t","e*(v - u)")] (real_sum_of_halves RS subst) 1);
+by (rtac real_add_le_mono 1);
+by (res_inst_tac [("j","(e / 2) * abs(v - x)")] real_le_trans 1);
+
+by (Asm_full_simp_tac 2 THEN arith_tac 2);
+by (ALLGOALS (thin_tac "ALL xa. \
+\ xa ~= x & abs (xa + - x) < s --> \
+\ abs ((f xa + - f x) / (xa + - x) + - f' x) * 2 < e"));
+by (dres_inst_tac [("x","v")] spec 1 THEN Auto_tac);
+by (arith_tac 1);
+by (dres_inst_tac [("x","u")] spec 1 THEN Auto_tac);
+by (arith_tac 1);
+by (subgoal_tac "abs (f u - f x - f' x * (u - x)) = \
+\ abs (f x - f u - f' x * (x - u))" 1);
+by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2,
+ real_diff_def]) 2);
+by (arith_tac 2);
+by(rtac real_le_trans 1);
+by Auto_tac;
+by (arith_tac 1);
+qed "lemma_straddle";
+
+Goal "((number_of c - 1) * x <= 0) =((number_of c ::real) * x <= x)";
+by (rtac ((ARITH_PROVE "(x <= y) = (x - y <= (0::real))") RS ssubst) 1);
+by (simp_tac (simpset() addsimps [real_diff_mult_distrib,
+ CLAIM_SIMP "c * x - x = (c - 1) * (x::real)" [real_diff_mult_distrib]]) 1);
+qed "lemma_number_of_mult_le";
+
+
+Goal "[|a <= b; ALL x. a <= x & x <= b --> DERIV f x :> f'(x) |] \
+\ ==> Integral(a,b) f' (f(b) - f(a))";
+by (dtac real_le_imp_less_or_eq 1 THEN Auto_tac);
+by (auto_tac (claset(),simpset() addsimps [Integral_def]));
+by (rtac ccontr 1);
+by (subgoal_tac "ALL e. 0 < e --> \
+\ (EX g. gauge (%x. a <= x & x <= b) g & \
+\ (ALL D p. \
+\ tpart (a, b) (D, p) & fine g (D, p) --> \
+\ abs (rsum (D, p) f' - (f b - f a)) <= e))" 1);
+by (rotate_tac 3 1);
+by (dres_inst_tac [("x","e/2")] spec 1 THEN Auto_tac);
+by (dtac spec 1 THEN Auto_tac);
+by (REPEAT(dtac spec 1) THEN Auto_tac);
+by (dres_inst_tac [("e","ea/(b - a)")] lemma_straddle 1);
+by (auto_tac (claset(),simpset() addsimps [real_0_less_divide_iff]));
+by (rtac exI 1);
+by (auto_tac (claset(),simpset() addsimps [tpart_def,rsum_def]));
+by (subgoal_tac "sumr 0 (psize D) (%n. f(D(Suc n)) - f(D n)) = \
+\ f b - f a" 1);
+by (cut_inst_tac [("D","%n. f(D n)"),("m","psize D")]
+ sumr_partition_eq_diff_bounds 2);
+by (asm_full_simp_tac (simpset() addsimps [partition_lhs,partition_rhs]) 2);
+by (dtac sym 1 THEN Asm_full_simp_tac 1);
+by (simp_tac (simpset() addsimps [sumr_diff]) 1);
+by (rtac (sumr_rabs RS real_le_trans) 1);
+by (subgoal_tac
+ "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D(Suc n) - (D n)))" 1);
+by (asm_full_simp_tac (simpset() addsimps
+ [ARITH_PROVE "abs(y - (x::real)) = abs(x - y)"]) 1);
+by (res_inst_tac [("t","ea")] ssubst 1 THEN assume_tac 1);
+by (rtac sumr_le2 1);
+by (rtac (sumr_mult RS subst) 2);
+by (auto_tac (claset(),simpset() addsimps [partition_rhs,
+ partition_lhs,partition_lb,partition_ub,fine_def]));
+qed "FTC1";
+
+
+Goal "[| Integral(a,b) f k1; k2 = k1 |] ==> Integral(a,b) f k2";
+by (Asm_simp_tac 1);
+qed "Integral_subst";
+
+Goal "[| a <= b; b <= c; Integral(a,b) f' k1; Integral(b,c) f' k2; \
+\ ALL x. a <= x & x <= c --> DERIV f x :> f' x |] \
+\ ==> Integral(a,c) f' (k1 + k2)";
+by (rtac (FTC1 RS Integral_subst) 1);
+by Auto_tac;
+by (ftac FTC1 1 THEN Auto_tac);
+by (forw_inst_tac [("a","b")] FTC1 1 THEN Auto_tac);
+by (dres_inst_tac [("x","x")] spec 1 THEN Auto_tac);
+by (dres_inst_tac [("k2.0","f b - f a")] Integral_unique 1);
+by (dres_inst_tac [("k2.0","f c - f b")] Integral_unique 3);
+by Auto_tac;
+qed "Integral_add";
+
+Goal "partition(a,b) D ==> psize D = (LEAST n. D(n) = b)";
+by (auto_tac (claset() addSIs [Least_equality RS sym,partition_rhs],simpset()));
+by (rtac ccontr 1);
+by (dtac partition_ub_lt 1);
+by Auto_tac;
+qed "partition_psize_Least";
+
+Goal "partition (a, c) D ==> ~ (EX n. c < D(n))";
+by (Step_tac 1);
+by (dres_inst_tac [("r","n")] partition_ub 1);
+by Auto_tac;
+qed "lemma_partition_bounded";
+
+Goal "partition (a, c) D ==> D = (%n. if D n < c then D n else c)";
+by (rtac ext 1 THEN Auto_tac);
+by (auto_tac (claset() addSDs [lemma_partition_bounded],simpset()));
+by (dres_inst_tac [("x","n")] spec 1);
+by Auto_tac;
+qed "lemma_partition_eq";
+
+Goal "partition (a, c) D ==> D = (%n. if D n <= c then D n else c)";
+by (rtac ext 1 THEN Auto_tac);
+by (auto_tac (claset() addSDs [lemma_partition_bounded],simpset()));
+by (dres_inst_tac [("x","n")] spec 1);
+by Auto_tac;
+qed "lemma_partition_eq2";
+
+Goal "[| partition(a,b) D; n < psize D |] ==> D n < D (Suc n)";
+by (auto_tac (claset(),simpset() addsimps [partition]));
+qed "partition_lt_Suc";
+
+Goal "tpart(a,c) (D,p) ==> p = (%n. if D n < c then p n else c)";
+by (rtac ext 1);
+by (auto_tac (claset(),simpset() addsimps [tpart_def]));
+by (dtac real_leI 1);
+by (dres_inst_tac [("r","Suc n")] partition_ub 1);
+by (dres_inst_tac [("x","n")] spec 1);
+by Auto_tac;
+qed "tpart_tag_eq";
+
+(*----------------------------------------------------------------------------*)
+(* Lemmas for Additivity Theorem of gauge integral *)
+(*----------------------------------------------------------------------------*)
+
+Goal "[| a <= D n; D n < b; partition(a,b) D |] ==> n < psize D";
+by (dtac (partition RS iffD1) 1 THEN Step_tac 1);
+by (rtac ccontr 1 THEN dtac leI 1);
+by Auto_tac;
+val lemma_additivity1 = result();
+
+Goal "[| a <= D n; partition(a,D n) D |] ==> psize D <= n";
+by (rtac ccontr 1 THEN dtac not_leE 1);
+by (ftac (partition RS iffD1) 1 THEN Step_tac 1);
+by (forw_inst_tac [("r","Suc n")] partition_ub 1);
+by (auto_tac (claset() addSDs [spec],simpset()));
+val lemma_additivity2 = result();
+
+Goal "[| partition(a,b) D; psize D < m |] ==> D(m) = D(psize D)";
+by (auto_tac (claset(),simpset() addsimps [partition]));
+qed "partition_eq_bound";
+
+Goal "[| partition(a,b) D; psize D < m |] ==> D(r) <= D(m)";
+by (ftac (partition RS iffD1) 1 THEN Auto_tac);
+by (etac partition_ub 1);
+qed "partition_ub2";
+
+Goalw [tpart_def]
+ "[| tpart(a,b) (D,p); psize D <= m |] ==> p(m) = D(m)";
+by Auto_tac;
+by (dres_inst_tac [("x","m")] spec 1);
+by (auto_tac (claset(),simpset() addsimps [partition_rhs2]));
+qed "tag_point_eq_partition_point";
+
+Goal "[| partition(a,b) D; D m < D n |] ==> m < n";
+by (cut_inst_tac [("m","n"),("n","psize D")] less_linear 1);
+by Auto_tac;
+by (rtac ccontr 1 THEN dtac leI 1 THEN dtac le_imp_less_or_eq 1);
+by (cut_inst_tac [("m","m"),("n","psize D")] less_linear 1);
+by (auto_tac (claset() addDs [partition_gt],simpset()));
+by (dres_inst_tac [("n","m")] partition_lt_gen 1 THEN Auto_tac);
+by (ftac partition_eq_bound 1);
+by (dtac partition_gt 2);
+by Auto_tac;
+by (rtac ccontr 1 THEN dtac leI 1 THEN dtac le_imp_less_or_eq 1);
+by (auto_tac (claset() addDs [partition_eq_bound],simpset()));
+by (rtac ccontr 1 THEN dtac leI 1 THEN dtac le_imp_less_or_eq 1);
+by (ftac partition_eq_bound 1 THEN assume_tac 1);
+by (dres_inst_tac [("m","m")] partition_eq_bound 1);
+by Auto_tac;
+qed "partition_lt_cancel";
+
+Goalw [psize_def]
+ "[| a <= D n; D n < b; partition (a, b) D |] \
+\ ==> psize (%x. if D x < D n then D(x) else D n) = n";
+by (ftac lemma_additivity1 1);
+by (assume_tac 1 THEN assume_tac 1);
+by (rtac some_equality 1);
+by (auto_tac (claset() addIs [partition_lt_Suc],simpset()));
+by (dres_inst_tac [("n","n")] partition_lt_gen 1);
+by (assume_tac 1 THEN arith_tac 1 THEN arith_tac 1);
+by (cut_inst_tac [("m","na"),("n","psize D")] less_linear 1);
+by (auto_tac (claset() addDs [partition_lt_cancel],simpset()));
+by (rtac ccontr 1);
+by (dtac (ARITH_PROVE "m ~= (n::nat) ==> m < n | n < m") 1);
+by (etac disjE 1);
+by (rotate_tac 5 1);
+by (dres_inst_tac [("x","n")] spec 1);
+by Auto_tac;
+by (dres_inst_tac [("n","n")] partition_lt_gen 1);
+by Auto_tac;
+by (arith_tac 1);
+by (dres_inst_tac [("x","n")] spec 1);
+by (asm_full_simp_tac (simpset() addsimps [split_if]) 1);
+qed "lemma_additivity4_psize_eq";
+
+Goal "partition (a, b) D \
+\ ==> psize (%x. if D x < D n then D(x) else D n) <= psize D";
+by (forw_inst_tac [("r","n")] partition_ub 1);
+by (dres_inst_tac [("x","D n")] real_le_imp_less_or_eq 1);
+by (auto_tac (claset(),simpset() addsimps
+ [lemma_partition_eq RS sym]));
+by (forw_inst_tac [("r","n")] partition_lb 1);
+by (dtac lemma_additivity4_psize_eq 1);
+by (rtac ccontr 3 THEN Auto_tac);
+by (ftac (not_leE RSN (2,partition_eq_bound)) 1);
+by (auto_tac (claset(),simpset() addsimps [partition_rhs]));
+qed "lemma_psize_left_less_psize";
+
+Goal "[| partition(a,b) D; na < psize (%x. if D x < D n then D(x) else D n) |] \
+\ ==> na < psize D";
+by (etac (lemma_psize_left_less_psize RSN (2,less_le_trans)) 1);
+by (assume_tac 1);
+qed "lemma_psize_left_less_psize2";
+
+
+Goal "[| partition(a,b) D; D na < D n; D n < D (Suc na); \
+\ n < psize D |] \
+\ ==> False";
+by (cut_inst_tac [("m","n"),("n","Suc na")] less_linear 1);
+by Auto_tac;
+by (dres_inst_tac [("n","n")] partition_lt_gen 2);
+by Auto_tac;
+by (cut_inst_tac [("m","psize D"),("n","na")] less_linear 1);
+by (auto_tac (claset(),simpset() addsimps [partition_rhs2]));
+by (dtac (ARITH_PROVE "n < Suc na ==> n < na | n = na") 1);
+by Auto_tac;
+by (dres_inst_tac [("n","na")] partition_lt_gen 1);
+by Auto_tac;
+val lemma_additivity3 = result();
+
+Goalw [psize_def] "psize (%x. k) = 0";
+by Auto_tac;
+qed "psize_const";
+Addsimps [psize_const];
+
+Goal "[| partition(a,b) D; D na < D n; D n < D (Suc na); \
+\ na < psize D |] \
+\ ==> False";
+by (forw_inst_tac [("m","n")] partition_lt_cancel 1);
+by (auto_tac (claset() addIs [lemma_additivity3],simpset()));
+val lemma_additivity3a = result();
+
+Goal "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) <= psize D - n";
+by (res_inst_tac [("D2","(%x. D (x + n))")] (psize_def RS
+ meta_eq_to_obj_eq RS ssubst) 1);
+by (res_inst_tac [("a","psize D - n")] someI2 1);
+by Auto_tac;
+by (dtac (ARITH_PROVE "(m::nat) < n - p ==> m + p < n") 1);
+by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
+by (dtac (ARITH_PROVE "(m::nat) - n <= p ==> m <= p + n") 1);
+by (case_tac "psize D <= n" 1);
+by (dtac not_leE 2);
+by (asm_simp_tac (simpset() addsimps
+ [ARITH_PROVE "p <= n ==> p - n = (0::nat)"]) 1);
+by (blast_tac (claset() addDs [partition_rhs2]) 1);
+by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
+by (rtac ccontr 1 THEN dtac not_leE 1);
+by (dres_inst_tac [("x","psize D - n")] spec 1);
+by Auto_tac;
+by (ftac partition_rhs 1 THEN Step_tac 1);
+by (ftac partition_lt_cancel 1 THEN assume_tac 1);
+by (dtac (partition RS iffD1) 1 THEN Step_tac 1);
+by (subgoal_tac "~ D (psize D - n + n) < D (Suc (psize D - n + n))" 1);
+by (Blast_tac 1);
+by (rotate_tac 6 1 THEN dres_inst_tac [("x","Suc (psize D)")] spec 1);
+by (Asm_simp_tac 1);
+qed "better_lemma_psize_right_eq1";
+
+Goal "partition (a, D n) D ==> psize D <= n";
+by (rtac ccontr 1 THEN dtac not_leE 1);
+by (ftac partition_lt_Suc 1 THEN assume_tac 1);
+by (forw_inst_tac [("r","Suc n")] partition_ub 1);
+by Auto_tac;
+qed "psize_le_n";
+
+Goal "partition(a,D n) D ==> psize (%x. D (x + n)) <= psize D - n";
+by (res_inst_tac [("D2","(%x. D (x + n))")] (psize_def RS
+ meta_eq_to_obj_eq RS ssubst) 1);
+by (res_inst_tac [("a","psize D - n")] someI2 1);
+by Auto_tac;
+by (dtac (ARITH_PROVE "(m::nat) < n - p ==> m + p < n") 1);
+by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
+by (dtac (ARITH_PROVE "(m::nat) - n <= p ==> m <= p + n") 1);
+by (case_tac "psize D <= n" 1);
+by (dtac not_leE 2);
+by (asm_simp_tac (simpset() addsimps
+ [ARITH_PROVE "p <= n ==> p - n = (0::nat)"]) 1);
+by (blast_tac (claset() addDs [partition_rhs2]) 1);
+by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
+by (rtac ccontr 1 THEN dtac not_leE 1);
+by (ftac psize_le_n 1);
+by (dres_inst_tac [("x","psize D - n")] spec 1);
+by (asm_full_simp_tac (simpset() addsimps
+ [ARITH_PROVE "p <= n ==> p - n = (0::nat)"]) 1);
+by (dtac (partition RS iffD1) 1 THEN Step_tac 1);
+by (rotate_tac 5 1 THEN dres_inst_tac [("x","Suc n")] spec 1);
+by Auto_tac;
+qed "better_lemma_psize_right_eq1a";
+
+Goal "partition(a,b) D ==> psize (%x. D (x + n)) <= psize D - n";
+by (forw_inst_tac [("r1","n")] (partition_ub RS real_le_imp_less_or_eq) 1);
+by (blast_tac (claset() addIs [better_lemma_psize_right_eq1a,
+ better_lemma_psize_right_eq1]) 1);
+qed "better_lemma_psize_right_eq";
+
+Goal "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) <= psize D";
+by (res_inst_tac [("D2","(%x. D (x + n))")] (psize_def RS
+ meta_eq_to_obj_eq RS ssubst) 1);
+by (res_inst_tac [("a","psize D - n")] someI2 1);
+by Auto_tac;
+by (dtac (ARITH_PROVE "(m::nat) < n - p ==> m + p < n") 1);
+by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
+by (subgoal_tac "n <= psize D" 1);
+by (dtac (ARITH_PROVE "(m::nat) - n <= p ==> m <= p + n") 1);
+by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
+by (rtac ccontr 1 THEN dtac not_leE 1);
+by (dtac (less_imp_le RSN (2,partition_rhs2)) 1);
+by Auto_tac;
+by (rtac ccontr 1 THEN dtac not_leE 1);
+by (dres_inst_tac [("x","psize D")] spec 1);
+by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
+qed "lemma_psize_right_eq1";
+
+(* should be combined with previous theorem; also proof has redundancy *)
+Goal "partition(a,D n) D ==> psize (%x. D (x + n)) <= psize D";
+by (res_inst_tac [("D2","(%x. D (x + n))")] (psize_def RS
+ meta_eq_to_obj_eq RS ssubst) 1);
+by (res_inst_tac [("a","psize D - n")] someI2 1);
+by Auto_tac;
+by (dtac (ARITH_PROVE "(m::nat) < n - p ==> m + p < n") 1);
+by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
+by (dtac (ARITH_PROVE "(m::nat) - n <= p ==> m <= p + n") 1);
+by (case_tac "psize D <= n" 1);
+by (dtac not_leE 2);
+by (asm_simp_tac (simpset() addsimps
+ [ARITH_PROVE "p <= n ==> p - n = (0::nat)"]) 1);
+by (blast_tac (claset() addDs [partition_rhs2]) 1);
+by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
+by (rtac ccontr 1 THEN dtac not_leE 1);
+by (dres_inst_tac [("x","psize D")] spec 1);
+by (asm_full_simp_tac (simpset() addsimps [partition]) 1);
+qed "lemma_psize_right_eq1a";
+
+Goal "[| partition(a,b) D |] ==> psize (%x. D (x + n)) <= psize D";
+by (forw_inst_tac [("r1","n")] (partition_ub RS real_le_imp_less_or_eq) 1);
+by (blast_tac (claset() addIs [lemma_psize_right_eq1a,lemma_psize_right_eq1]) 1);
+qed "lemma_psize_right_eq";
+
+Goal "[| a <= D n; tpart (a, b) (D, p) |] \
+\ ==> tpart(a, D n) (%x. if D x < D n then D(x) else D n, \
+\ %x. if D x < D n then p(x) else D n)";
+by (forw_inst_tac [("r","n")] (tpart_partition RS partition_ub) 1);
+by (dres_inst_tac [("x","D n")] real_le_imp_less_or_eq 1);
+by (auto_tac (claset(),simpset() addsimps
+ [tpart_partition RS lemma_partition_eq RS sym,
+ tpart_tag_eq RS sym]));
+by (ftac (tpart_partition RSN (3,lemma_additivity1)) 1);
+by (auto_tac (claset(),simpset() addsimps [tpart_def]));
+by (dtac (real_leI RS real_le_imp_less_or_eq) 2);
+by (Auto_tac);
+by (blast_tac (claset() addDs [lemma_additivity3]) 2);
+by (dtac real_leI 2 THEN dres_inst_tac [("x","na")] spec 2);
+by (arith_tac 2);
+by (ftac lemma_additivity4_psize_eq 1);
+by (REPEAT(assume_tac 1));
+by (rtac (partition RS iffD2) 1);
+by (ftac (partition RS iffD1) 1);
+by (auto_tac (claset() addIs [partition_lt_gen],simpset() addsimps []));
+by (dres_inst_tac [("n","n")] partition_lt_gen 1);
+by (assume_tac 1 THEN arith_tac 1);
+by (Blast_tac 1);
+by (dtac partition_lt_cancel 1 THEN Auto_tac);
+qed "tpart_left1";
+
+Goal "[| a <= D n; tpart (a, b) (D, p); gauge (%x. a <= x & x <= D n) g;\
+\ fine (%x. if x < D n then min (g x) ((D n - x)/ 2) \
+\ else if x = D n then min (g (D n)) (ga (D n)) \
+\ else min (ga x) ((x - D n)/ 2)) (D, p) |] \
+\ ==> fine g \
+\ (%x. if D x < D n then D(x) else D n, \
+\ %x. if D x < D n then p(x) else D n)";
+by (auto_tac (claset(),simpset() addsimps [fine_def,tpart_def,gauge_def]));
+by (ALLGOALS (ftac lemma_psize_left_less_psize2));
+by (TRYALL(assume_tac));
+by (ALLGOALS (dres_inst_tac [("x","na")] spec) THEN Auto_tac);
+by (ALLGOALS(dres_inst_tac [("x","na")] spec));
+by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [split_if]) 1);
+by (dtac (real_leI RS real_le_imp_less_or_eq) 1);
+by (Step_tac 1);
+by (blast_tac (claset() addDs [lemma_additivity3a]) 1);
+by (dtac sym 1 THEN Auto_tac);
+qed "fine_left1";
+
+Goal "[| a <= D n; tpart (a, b) (D, p) |] \
+\ ==> tpart(D n, b) (%x. D(x + n),%x. p(x + n))";
+by (asm_full_simp_tac (simpset() addsimps [tpart_def,partition_def]) 1);
+by (Step_tac 1);
+by (res_inst_tac [("x","N - n")] exI 1 THEN Auto_tac);
+by (rotate_tac 2 1);
+by (dres_inst_tac [("x","na + n")] spec 1);
+by (rotate_tac 3 2);
+by (dres_inst_tac [("x","na + n")] spec 2);
+by (ALLGOALS(arith_tac));
+qed "tpart_right1";
+
+Goal "[| a <= D n; tpart (a, b) (D, p); gauge (%x. D n <= x & x <= b) ga;\
+\ fine (%x. if x < D n then min (g x) ((D n - x)/ 2) \
+\ else if x = D n then min (g (D n)) (ga (D n)) \
+\ else min (ga x) ((x - D n)/ 2)) (D, p) |] \
+\ ==> fine ga (%x. D(x + n),%x. p(x + n))";
+by (auto_tac (claset(),simpset() addsimps [fine_def,gauge_def]));
+by (dres_inst_tac [("x","na + n")] spec 1);
+by (forw_inst_tac [("n","n")] (tpart_partition RS better_lemma_psize_right_eq) 1);
+by Auto_tac;
+by (arith_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [tpart_def]) 1 THEN Step_tac 1);
+by (subgoal_tac "D n <= p (na + n)" 1);
+by (dres_inst_tac [("y","p (na + n)")] real_le_imp_less_or_eq 1);
+by (Step_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [split_if]) 1);
+by (Asm_full_simp_tac 1);
+by (dtac less_le_trans 1 THEN assume_tac 1);
+by (rotate_tac 5 1);
+by (dres_inst_tac [("x","na + n")] spec 1 THEN Step_tac 1);
+by (rtac real_le_trans 1 THEN assume_tac 2);
+by (case_tac "na = 0" 1 THEN Auto_tac);
+by (rtac (partition_lt_gen RS order_less_imp_le) 1);
+by Auto_tac;
+by (arith_tac 1);
+qed "fine_right1";
+
+Goalw [rsum_def]
+ "rsum (D, p) (%x. f x + g x) = rsum (D, p) f + rsum(D, p) g";
+by (auto_tac (claset(),simpset() addsimps [sumr_add,real_add_mult_distrib]));
+qed "rsum_add";
+
+(* Bartle/Sherbert: Theorem 10.1.5 p. 278 *)
+Goalw [Integral_def]
+ "[| a <= b; Integral(a,b) f k1; Integral(a,b) g k2 |] \
+\ ==> Integral(a,b) (%x. f x + g x) (k1 + k2)";
+by Auto_tac;
+by (REPEAT(dres_inst_tac [("x","e/2")] spec 1));
+by Auto_tac;
+by (dtac gauge_min 1 THEN assume_tac 1);
+by (res_inst_tac [("x","(%x. if ga x < gaa x then ga x else gaa x)")] exI 1);
+by Auto_tac;
+by (dtac fine_min 1);
+by (REPEAT(dtac spec 1) THEN Auto_tac);
+by (dres_inst_tac [("R1.0","abs (rsum (D, p) f - k1)* 2"),
+ ("R2.0","abs (rsum (D, p) g - k2) * 2")]
+ real_add_less_mono 1 THEN assume_tac 1);
+by (auto_tac (claset(),HOL_ss addsimps [rsum_add,real_add_mult_distrib RS sym,
+ real_mult_2_right RS sym,real_mult_less_iff1,CLAIM "(0::real) < 2"]));
+by (arith_tac 1);
+qed "Integral_add_fun";
+
+Goal "[| partition(a,b) D; r < psize D |] ==> 0 < D (Suc r) - D r";
+by (auto_tac (claset(),simpset() addsimps [partition]));
+qed "partition_lt_gen2";
+
+Goalw [tpart_def]
+ "[| ALL x. a <= x & x <= b --> f x <= g x; \
+\ tpart(a,b) (D,p) \
+\ |] ==> ALL n. n <= psize D --> f (p n) <= g (p n)";
+by (Auto_tac THEN ftac (partition RS iffD1) 1);
+by Auto_tac;
+by (dres_inst_tac [("x","p n")] spec 1);
+by Auto_tac;
+by (case_tac "n = 0" 1);
+by (rtac (partition_lt_gen RS order_less_le_trans RS order_less_imp_le) 2);
+by Auto_tac;
+by (dtac le_imp_less_or_eq 1 THEN Auto_tac);
+by (dres_inst_tac [("x","psize D")] spec 2 THEN Auto_tac);
+by (dres_inst_tac [("r","Suc n")] partition_ub 1);
+by (dres_inst_tac [("x","n")] spec 1);
+by Auto_tac;
+qed "lemma_Integral_le";
+
+Goalw [rsum_def]
+ "[| ALL x. a <= x & x <= b --> f x <= g x; \
+\ tpart(a,b) (D,p) \
+\ |] ==> rsum(D,p) f <= rsum(D,p) g";
+by (auto_tac (claset() addSIs [sumr_le2] addDs
+ [tpart_partition RS partition_lt_gen2] addSDs
+ [lemma_Integral_le],simpset()));
+qed "lemma_Integral_rsum_le";
+
+Goalw [Integral_def]
+ "[| a <= b; \
+\ ALL x. a <= x & x <= b --> f(x) <= g(x); \
+\ Integral(a,b) f k1; Integral(a,b) g k2 \
+\ |] ==> k1 <= k2";
+by Auto_tac;
+by (rotate_tac 2 1);
+by (dres_inst_tac [("x","abs(k1 - k2)/2")] spec 1);
+by (dres_inst_tac [("x","abs(k1 - k2)/2")] spec 1);
+by Auto_tac;
+by (dtac gauge_min 1 THEN assume_tac 1);
+by (dres_inst_tac [("g","%x. if ga x < gaa x then ga x else gaa x")]
+ partition_exists 1 THEN assume_tac 1);
+by Auto_tac;
+by (dtac fine_min 1);
+by (dres_inst_tac [("x","D")] spec 1 THEN dres_inst_tac [("x","D")] spec 1);
+by (dres_inst_tac [("x","p")] spec 1 THEN dres_inst_tac [("x","p")] spec 1);
+by Auto_tac;
+by (ftac lemma_Integral_rsum_le 1 THEN assume_tac 1);
+by (subgoal_tac
+ "abs((rsum(D,p) f - k1) - (rsum(D,p) g - k2)) < abs(k1 - k2)" 1);
+by (arith_tac 1);
+by (dtac real_add_less_mono 1 THEN assume_tac 1);
+by (auto_tac (claset(),HOL_ss addsimps [real_add_mult_distrib RS sym,
+ real_mult_2_right RS sym,real_mult_less_iff1,CLAIM "(0::real) < 2"]));
+by (arith_tac 1);
+qed "Integral_le";
+
+Goalw [Integral_def]
+ "(EX k. Integral(a,b) f k) ==> \
+\ (ALL e. 0 < e --> \
+\ (EX g. gauge (%x. a <= x & x <= b) g & \
+\ (ALL D1 D2 p1 p2. \
+\ tpart(a,b) (D1, p1) & fine g (D1,p1) & \
+\ tpart(a,b) (D2, p2) & fine g (D2,p2) --> \
+\ abs(rsum(D1,p1) f - rsum(D2,p2) f) < e)))";
+by Auto_tac;
+by (dres_inst_tac [("x","e/2")] spec 1);
+by Auto_tac;
+by (rtac exI 1 THEN Auto_tac);
+by (forw_inst_tac [("x","D1")] spec 1);
+by (forw_inst_tac [("x","D2")] spec 1);
+by (REPEAT(dtac spec 1) THEN Auto_tac);
+by (thin_tac "0 < e" 1);
+by (dtac real_add_less_mono 1 THEN assume_tac 1);
+by (auto_tac (claset(),HOL_ss addsimps [real_add_mult_distrib RS sym,
+ real_mult_2_right RS sym,real_mult_less_iff1,CLAIM "(0::real) < 2"]));
+by (arith_tac 1);
+qed "Integral_imp_Cauchy";
+
+Goalw [Cauchy_def]
+ "Cauchy X = \
+\ (ALL j. (EX M. ALL m n. M <= m & M <= n --> \
+\ abs (X m + - X n) < inverse(real (Suc j))))";
+by Auto_tac;
+by (dtac reals_Archimedean 1);
+by (Step_tac 1);
+by (dres_inst_tac [("x","n")] spec 1);
+by Auto_tac;
+by (res_inst_tac [("x","M")] exI 1);
+by Auto_tac;
+by (dres_inst_tac [("x","m")] spec 1);
+by (dres_inst_tac [("x","na")] spec 1);
+by Auto_tac;
+qed "Cauchy_iff2";
+
+Goal "[| a <= b; ALL n. gauge (%x. a <= x & x <= b) (fa n) |] \
+\ ==> ALL n. EX D p. tpart (a, b) (D, p) & fine (fa n) (D, p)";
+by (Step_tac 1);
+by (rtac partition_exists 1 THEN Auto_tac);
+qed "partition_exists2";
+
+Goal "[| a <= b; ALL c. a <= c & c <= b --> f' c <= g' c; \
+\ ALL x. DERIV f x :> f' x; ALL x. DERIV g x :> g' x \
+\ |] ==> f b - f a <= g b - g a";
+by (rtac Integral_le 1);
+by (assume_tac 1);
+by (rtac FTC1 2);
+by (rtac FTC1 4);
+by Auto_tac;
+qed "monotonic_anti_derivative";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/Integration.thy Mon May 05 18:23:40 2003 +0200
@@ -0,0 +1,58 @@
+(* Title : Integration.thy
+ Author : Jacques D. Fleuriot
+ Copyright : 2000 University of Edinburgh
+ Description : Theory of integration (cf. Harrison's HOL development)
+*)
+
+Integration = MacLaurin +
+
+
+constdefs
+
+
+(* ------------------------------------------------------------------------ *)
+(* Partitions and tagged partitions etc. *)
+(* ------------------------------------------------------------------------ *)
+
+ partition :: "[(real*real),nat => real] => bool"
+ "partition == %(a,b) D. ((D 0 = a) &
+ (EX N. ((ALL n. n < N --> D(n) < D(Suc n)) &
+ (ALL n. N <= n --> (D(n) = b)))))"
+
+ psize :: (nat => real) => nat
+ "psize D == @N. (ALL n. n < N --> D(n) < D(Suc n)) &
+ (ALL n. N <= n --> (D(n) = D(N)))"
+
+ tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool"
+ "tpart == %(a,b) (D,p). partition(a,b) D &
+ (ALL n. D(n) <= p(n) & p(n) <= D(Suc n))"
+
+(* ------------------------------------------------------------------------ *)
+(* Gauges and gauge-fine divisions *)
+(* ------------------------------------------------------------------------ *)
+
+ gauge :: [real => bool, real => real] => bool
+ "gauge E g == ALL x. E x --> 0 < g(x)"
+
+ fine :: "[real => real, ((nat => real)*(nat => real))] => bool"
+ "fine == % g (D,p). ALL n. n < (psize D) --> D(Suc n) - D(n) < g(p n)"
+
+(* ------------------------------------------------------------------------ *)
+(* Riemann sum *)
+(* ------------------------------------------------------------------------ *)
+
+ rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real"
+ "rsum == %(D,p) f. sumr 0 (psize(D)) (%n. f(p n) * (D(Suc n) - D(n)))"
+
+(* ------------------------------------------------------------------------ *)
+(* Gauge integrability (definite) *)
+(* ------------------------------------------------------------------------ *)
+
+ Integral :: "[(real*real),real=>real,real] => bool"
+ "Integral == %(a,b) f k. ALL e. 0 < e -->
+ (EX g. gauge(%x. a <= x & x <= b) g &
+ (ALL D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
+ abs(rsum(D,p) f - k) < e))"
+end
+
+
--- a/src/HOL/Hyperreal/ROOT.ML Mon May 05 18:22:31 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(* Title: HOL/Hyperreal/ROOT.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Construction of the Hyperreals by the Ultrapower Construction
-and mechanization of Nonstandard Real Analysis
-by Jacques Fleuriot
-*)
-
-time_use_thy "Hyperreal";
--- a/src/HOL/Hyperreal/Transcendental.ML Mon May 05 18:22:31 2003 +0200
+++ b/src/HOL/Hyperreal/Transcendental.ML Mon May 05 18:23:40 2003 +0200
@@ -2498,6 +2498,682 @@
qed "cos_one_sin_zero";
(*-------------------------------------------------------------------------------*)
-(* Add continuity checker in backup of theory? *)
+(* A few extra theorems *)
+(*-------------------------------------------------------------------------------*)
+
+Goal "[| 0 <= x; x < y |] ==> root(Suc n) x < root(Suc n) y";
+by (ftac order_le_less_trans 1);
+by (assume_tac 1);
+by (forw_inst_tac [("n1","n")] (real_root_pow_pos2 RS ssubst) 1);
+by (rotate_tac 1 1);
+by (assume_tac 1);
+by (forw_inst_tac [("n1","n")] (real_root_pow_pos RS ssubst) 1);
+by (rotate_tac 3 1 THEN assume_tac 1);
+by (dres_inst_tac [("y","root (Suc n) y ^ Suc n")] order_less_imp_le 1 );
+by (forw_inst_tac [("n","n")] real_root_pos_pos_le 1);
+by (forw_inst_tac [("n","n")] real_root_pos_pos 1);
+by (dres_inst_tac [("x","root (Suc n) x"),
+ ("y","root (Suc n) y")] realpow_increasing 1);
+by (assume_tac 1 THEN assume_tac 1);
+by (dres_inst_tac [("x","root (Suc n) x")] order_le_imp_less_or_eq 1);
+by Auto_tac;
+by (dres_inst_tac [("f","%x. x ^ (Suc n)")] arg_cong 1);
+by (auto_tac (claset(),simpset() addsimps [real_root_pow_pos2]
+ delsimps [realpow_Suc]));
+qed "real_root_less_mono";
+
+Goal "[| 0 <= x; x <= y |] ==> root(Suc n) x <= root(Suc n) y";
+by (dres_inst_tac [("y","y")] order_le_imp_less_or_eq 1 );
+by (auto_tac (claset() addDs [real_root_less_mono]
+ addIs [order_less_imp_le],simpset()));
+qed "real_root_le_mono";
+
+Goal "[| 0 <= x; 0 <= y |] ==> (root(Suc n) x < root(Suc n) y) = (x < y)";
+by (auto_tac (claset() addIs [real_root_less_mono],simpset()));
+by (rtac ccontr 1 THEN dtac real_leI 1);
+by (dres_inst_tac [("x","y"),("n","n")] real_root_le_mono 1);
+by Auto_tac;
+qed "real_root_less_iff";
+Addsimps [real_root_less_iff];
+
+Goal "[| 0 <= x; 0 <= y |] ==> (root(Suc n) x <= root(Suc n) y) = (x <= y)";
+by (auto_tac (claset() addIs [real_root_le_mono],simpset()));
+by (simp_tac (simpset() addsimps [real_le_def]) 1);
+by Auto_tac;
+by (dres_inst_tac [("x","y"),("n","n")] real_root_less_mono 1);
+by Auto_tac;
+qed "real_root_le_iff";
+Addsimps [real_root_le_iff];
+
+Goal "[| 0 <= x; 0 <= y |] ==> (root(Suc n) x = root(Suc n) y) = (x = y)";
+by (auto_tac (claset() addSIs [real_le_anti_sym],simpset()));
+by (res_inst_tac [("n1","n")] (real_root_le_iff RS iffD1) 1);
+by (res_inst_tac [("n1","n")] (real_root_le_iff RS iffD1) 4);
+by Auto_tac;
+qed "real_root_eq_iff";
+Addsimps [real_root_eq_iff];
+
+Goal "[| 0 <= x; 0 <= y; y ^ (Suc n) = x |] ==> root (Suc n) x = y";
+by (auto_tac (claset() addDs [real_root_pos2],
+ simpset() delsimps [realpow_Suc]));
+qed "real_root_pos_unique";
+
+Goal "[| 0 <= x; 0 <= y |]\
+\ ==> root(Suc n) (x * y) = root(Suc n) x * root(Suc n) y";
+by (rtac real_root_pos_unique 1);
+by (auto_tac (claset() addSIs [real_root_pos_pos_le],simpset()
+ addsimps [realpow_mult,real_0_le_mult_iff,
+ real_root_pow_pos2] delsimps [realpow_Suc]));
+qed "real_root_mult";
+
+Goal "0 <= x ==> (root(Suc n) (inverse x) = inverse(root(Suc n) x))";
+by (rtac real_root_pos_unique 1);
+by (auto_tac (claset() addIs [real_root_pos_pos_le],simpset()
+ addsimps [realpow_inverse RS sym,real_root_pow_pos2]
+ delsimps [realpow_Suc]));
+qed "real_root_inverse";
+
+Goalw [real_divide_def]
+ "[| 0 <= x; 0 <= y |] \
+\ ==> (root(Suc n) (x / y) = root(Suc n) x / root(Suc n) y)";
+by (auto_tac (claset(),simpset() addsimps [real_root_mult,
+ real_root_inverse]));
+qed "real_root_divide";
+
+Goalw [sqrt_def] "[| 0 <= x; x < y |] ==> sqrt(x) < sqrt(y)";
+by (auto_tac (claset() addIs [real_root_less_mono],simpset()));
+qed "real_sqrt_less_mono";
+
+Goalw [sqrt_def] "[| 0 <= x; x <= y |] ==> sqrt(x) <= sqrt(y)";
+by (auto_tac (claset() addIs [real_root_le_mono],simpset()));
+qed "real_sqrt_le_mono";
+
+Goalw [sqrt_def] "[| 0 <= x; 0 <= y |] ==> (sqrt(x) < sqrt(y)) = (x < y)";
+by Auto_tac;
+qed "real_sqrt_less_iff";
+Addsimps [real_sqrt_less_iff];
+
+Goalw [sqrt_def] "[| 0 <= x; 0 <= y |] ==> (sqrt(x) <= sqrt(y)) = (x <= y)";
+by Auto_tac;
+qed "real_sqrt_le_iff";
+Addsimps [real_sqrt_le_iff];
+
+Goalw [sqrt_def] "[| 0 <= x; 0 <= y |] ==> (sqrt(x) = sqrt(y)) = (x = y)";
+by Auto_tac;
+qed "real_sqrt_eq_iff";
+Addsimps [real_sqrt_eq_iff];
+
+Goal "(sqrt(x ^ 2 + y ^ 2) < 1) = (x ^ 2 + y ^ 2 < 1)";
+by (rtac (real_sqrt_one RS subst) 1);
+by (Step_tac 1);
+by (rtac real_sqrt_less_mono 2);
+by (dtac (rotate_prems 2 (real_sqrt_less_iff RS iffD1)) 1);
+by Auto_tac;
+qed "real_sqrt_sos_less_one_iff";
+Addsimps [real_sqrt_sos_less_one_iff];
+
+Goal "(sqrt(x ^ 2 + y ^ 2) = 1) = (x ^ 2 + y ^ 2 = 1)";
+by (rtac (real_sqrt_one RS subst) 1);
+by (Step_tac 1);
+by (dtac (rotate_prems 2 (real_sqrt_eq_iff RS iffD1)) 1);
+by Auto_tac;
+qed "real_sqrt_sos_eq_one_iff";
+Addsimps [real_sqrt_sos_eq_one_iff];
+
+Goalw [real_divide_def] "(((r::real) * a) / (r * r)) = a / r";
+by (real_div_undefined_case_tac "r=0" 1);
+by (auto_tac (claset(),simpset() addsimps [real_inverse_distrib] @ real_mult_ac));
+qed "real_divide_square_eq";
+Addsimps [real_divide_square_eq];
+
+(*-------------------------------------------------------------------------------*)
+(* More theorems about sqrt, transcendental functions etc. needed in Complex.ML *)
(*-------------------------------------------------------------------------------*)
+
+goal Real.thy "2 = Suc (Suc 0)";
+by (Simp_tac 1);
+qed "two_eq_Suc_Suc";
+
+val realpow_num_two = CLAIM "2 = Suc(Suc 0)";
+
+Goal "x ^ 2 = x * (x::real)";
+by (auto_tac (claset(),simpset() addsimps [CLAIM "2 = Suc(Suc 0)"]));
+qed "realpow_two_eq_mult";
+
+Goalw [real_divide_def]
+ "0 < x ==> 0 <= x/(sqrt (x * x + y * y))";
+by (ftac ((real_sqrt_sum_squares_ge1 RSN (2,order_less_le_trans))
+ RS (CLAIM "0 < x ==> 0 < inverse (x::real)")) 1);
+by (rtac (real_mult_order RS order_less_imp_le) 1);
+by (auto_tac (claset(),simpset() addsimps [realpow_num_two]));
+qed "lemma_real_divide_sqrt";
+
+Goal "0 < x ==> -(1::real) <= x/(sqrt (x * x + y * y))";
+by (rtac real_le_trans 1);
+by (rtac lemma_real_divide_sqrt 2);
+by Auto_tac;
+qed "lemma_real_divide_sqrt_ge_minus_one";
+
+Goal "x < 0 ==> 0 < sqrt (x * x + y * y)";
+by (rtac real_sqrt_gt_zero 1);
+by (rtac (ARITH_PROVE "[| 0 < x; 0 <= y |] ==> (0::real) < x + y") 1);
+by (auto_tac (claset(),simpset() addsimps [real_0_less_mult_iff]));
+qed "real_sqrt_sum_squares_gt_zero1";
+
+Goal "0 < x ==> 0 < sqrt (x * x + y * y)";
+by (rtac real_sqrt_gt_zero 1);
+by (rtac (ARITH_PROVE "[| 0 < x; 0 <= y |] ==> (0::real) < x + y") 1);
+by (auto_tac (claset(),simpset() addsimps [real_0_less_mult_iff]));
+qed "real_sqrt_sum_squares_gt_zero2";
+
+Goal "x ~= 0 ==> 0 < sqrt(x ^ 2 + y ^ 2)";
+by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
+by (auto_tac (claset() addIs [real_sqrt_sum_squares_gt_zero2,
+ real_sqrt_sum_squares_gt_zero1],simpset() addsimps [realpow_num_two]));
+qed "real_sqrt_sum_squares_gt_zero3";
+
+Goal "y ~= 0 ==> 0 < sqrt(x ^ 2 + y ^ 2)";
+by (dres_inst_tac [("y","x")] real_sqrt_sum_squares_gt_zero3 1);
+by (auto_tac (claset(),simpset() addsimps [real_add_commute]));
+qed "real_sqrt_sum_squares_gt_zero3a";
+
+Goal "sqrt(x ^ 2 + y ^ 2) = x ==> y = 0";
+by (rtac ccontr 1);
+by (forw_inst_tac [("x","x")] real_sum_squares_not_zero2 1);
+by (dres_inst_tac [("f","%x. x ^ 2")] arg_cong 1);
+by (forw_inst_tac [("x","x"),("y","y")] real_sum_square_gt_zero2 1);
+by (dtac real_sqrt_gt_zero_pow2 1);
+by Auto_tac;
+qed "real_sqrt_sum_squares_eq_cancel";
+Addsimps [real_sqrt_sum_squares_eq_cancel];
+
+Goal "sqrt(x ^ 2 + y ^ 2) = y ==> x = 0";
+by (res_inst_tac [("x","y")] real_sqrt_sum_squares_eq_cancel 1);
+by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
+qed "real_sqrt_sum_squares_eq_cancel2";
+Addsimps [real_sqrt_sum_squares_eq_cancel2];
+
+Goal "x < 0 ==> x/(sqrt (x * x + y * y)) <= 1";
+by (dtac (ARITH_PROVE "x < 0 ==> (0::real) < -x") 1);
+by (dres_inst_tac [("y","y")]
+ lemma_real_divide_sqrt_ge_minus_one 1);
+by (dtac (ARITH_PROVE "x <= y ==> -y <= -(x::real)") 1);
+by Auto_tac;
+qed "lemma_real_divide_sqrt_le_one";
+
+Goal "x < 0 ==> -(1::real) <= x/(sqrt (x * x + y * y))";
+by (case_tac "y = 0" 1);
+by Auto_tac;
+by (ftac abs_minus_eqI2 1);
+by (auto_tac (claset(),simpset() addsimps [real_minus_inverse]));
+by (rtac order_less_imp_le 1);
+by (res_inst_tac [("z1","sqrt(x * x + y * y)")]
+ (real_mult_less_iff1 RS iffD1) 1);
+by (forw_inst_tac [("y2","y")]
+ (real_sqrt_sum_squares_gt_zero1 RS real_not_refl2
+ RS not_sym) 2);
+by (auto_tac (claset() addIs [real_sqrt_sum_squares_gt_zero1],
+ simpset() addsimps real_mult_ac));
+by (rtac (ARITH_PROVE "-x < y ==> -y < (x::real)") 1);
+by (cut_inst_tac [("x","-x"),("y","y")] real_sqrt_sum_squares_ge1 1);
+by (dtac real_le_imp_less_or_eq 1);
+by (Step_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [realpow_num_two]) 1);
+by (dtac (sym RS real_sqrt_sum_squares_eq_cancel) 1);
+by Auto_tac;
+qed "lemma_real_divide_sqrt_ge_minus_one2";
+
+Goal "0 < x ==> x/(sqrt (x * x + y * y)) <= 1";
+by (dtac (ARITH_PROVE "0 < x ==> -x < (0::real)") 1);
+by (dres_inst_tac [("y","y")]
+ lemma_real_divide_sqrt_ge_minus_one2 1);
+by (dtac (ARITH_PROVE "x <= y ==> -y <= -(x::real)") 1);
+by Auto_tac;
+qed "lemma_real_divide_sqrt_le_one2";
+(* was qed "lemma_real_mult_self_rinv_sqrt_squared5" *)
+
+Goal "-(1::real)<= x / sqrt (x * x + y * y)";
+by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
+by (Step_tac 1);
+by (rtac lemma_real_divide_sqrt_ge_minus_one2 1);
+by (rtac lemma_real_divide_sqrt_ge_minus_one 3);
+by Auto_tac;
+qed "cos_x_y_ge_minus_one";
+Addsimps [cos_x_y_ge_minus_one];
+
+Goal "-(1::real)<= y / sqrt (x * x + y * y)";
+by (cut_inst_tac [("x","y"),("y","x")] cos_x_y_ge_minus_one 1);
+by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
+qed "cos_x_y_ge_minus_one1a";
+Addsimps [cos_x_y_ge_minus_one1a,
+ simplify (simpset()) cos_x_y_ge_minus_one1a];
+
+Goal "x / sqrt (x * x + y * y) <= 1";
+by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
+by (Step_tac 1);
+by (rtac lemma_real_divide_sqrt_le_one 1);
+by (rtac lemma_real_divide_sqrt_le_one2 3);
+by Auto_tac;
+qed "cos_x_y_le_one";
+Addsimps [cos_x_y_le_one];
+
+Goal "y / sqrt (x * x + y * y) <= 1";
+by (cut_inst_tac [("x","y"),("y","x")] cos_x_y_le_one 1);
+by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
+qed "cos_x_y_le_one2";
+Addsimps [cos_x_y_le_one2];
+
+Addsimps [[cos_x_y_ge_minus_one,cos_x_y_le_one] MRS cos_arcos];
+Addsimps [[cos_x_y_ge_minus_one,cos_x_y_le_one] MRS arcos_bounded];
+
+Addsimps [[cos_x_y_ge_minus_one1a,cos_x_y_le_one2] MRS cos_arcos];
+Addsimps [[cos_x_y_ge_minus_one1a,cos_x_y_le_one2] MRS arcos_bounded];
+
+Goal "-(1::real) <= abs(x) / sqrt (x * x + y * y)";
+by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
+by (auto_tac (claset(),simpset() addsimps [abs_minus_eqI2,abs_eqI2]));
+by (dtac lemma_real_divide_sqrt_ge_minus_one 1 THEN Force_tac 1);
+qed "cos_rabs_x_y_ge_minus_one";
+
+Addsimps [cos_rabs_x_y_ge_minus_one,
+ simplify (simpset()) cos_rabs_x_y_ge_minus_one];
+
+Goal "abs(x) / sqrt (x * x + y * y) <= 1";
+by (cut_inst_tac [("R1.0","x"),("R2.0","0")] real_linear 1);
+by (auto_tac (claset(),simpset() addsimps [abs_minus_eqI2,abs_eqI2]));
+by (dtac lemma_real_divide_sqrt_ge_minus_one2 1 THEN Force_tac 1);
+qed "cos_rabs_x_y_le_one";
+Addsimps [cos_rabs_x_y_le_one];
+
+Addsimps [[cos_rabs_x_y_ge_minus_one,cos_rabs_x_y_le_one] MRS cos_arcos];
+Addsimps [[cos_rabs_x_y_ge_minus_one,cos_rabs_x_y_le_one] MRS arcos_bounded];
+
+Goal "-pi < 0";
+by (Simp_tac 1);
+qed "minus_pi_less_zero";
+Addsimps [minus_pi_less_zero];
+Addsimps [minus_pi_less_zero RS order_less_imp_le];
+
+Goal "[| -(1::real) <= y; y <= 1 |] ==> -pi <= arcos y";
+by (rtac real_le_trans 1);
+by (rtac arcos_lbound 2);
+by Auto_tac;
+qed "arcos_ge_minus_pi";
+
+Addsimps [[cos_x_y_ge_minus_one,cos_x_y_le_one] MRS arcos_ge_minus_pi];
+
+(* How tedious! *)
+Goal "[| x + (y::real) ~= 0; 1 - z = x/(x + y) \
+\ |] ==> z = y/(x + y)";
+by (res_inst_tac [("c1","x + y")] (real_mult_right_cancel RS iffD1) 1);
+by (forw_inst_tac [("c1","x + y")] (real_mult_right_cancel RS iffD2) 2);
+by (assume_tac 2);
+by (rotate_tac 2 2);
+by (dtac (real_mult_assoc RS subst) 2);
+by (rotate_tac 2 2);
+by (ftac (real_mult_inv_left RS subst) 2);
+by (assume_tac 2);
+by (thin_tac "(1 - z) * (x + y) = x /(x + y) * (x + y)" 2);
+by (thin_tac "1 - z = x /(x + y)" 2);
+by (auto_tac (claset(),simpset() addsimps [real_mult_assoc]));
+by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib2,
+ real_diff_mult_distrib]));
+qed "lemma_divide_rearrange";
+
+Goal "[| 0 < x * x + y * y; \
+\ 1 - sin xa ^ 2 = (x / sqrt (x * x + y * y)) ^ 2 \
+\ |] ==> sin xa ^ 2 = (y / sqrt (x * x + y * y)) ^ 2";
+by (auto_tac (claset() addIs [lemma_divide_rearrange],simpset()
+ addsimps [realpow_divide,real_sqrt_gt_zero_pow2,
+ realpow_two_eq_mult RS sym]));
+qed "lemma_cos_sin_eq";
+
+Goal "[| 0 < x * x + y * y; \
+\ 1 - cos xa ^ 2 = (y / sqrt (x * x + y * y)) ^ 2 \
+\ |] ==> cos xa ^ 2 = (x / sqrt (x * x + y * y)) ^ 2";
+by (auto_tac (claset(),simpset() addsimps [realpow_divide,
+ real_sqrt_gt_zero_pow2,realpow_two_eq_mult RS sym]));
+by (rtac (real_add_commute RS subst) 1);
+by (auto_tac (claset() addIs [lemma_divide_rearrange],simpset()));
+qed "lemma_sin_cos_eq";
+
+Goal "[| x ~= 0; \
+\ cos xa = x / sqrt (x * x + y * y) \
+\ |] ==> sin xa = y / sqrt (x * x + y * y) | \
+\ sin xa = - y / sqrt (x * x + y * y)";
+by (dres_inst_tac [("f","%x. x ^ 2")] arg_cong 1);
+by (forw_inst_tac [("y","y")] real_sum_square_gt_zero 1);
+by (asm_full_simp_tac (simpset() addsimps [cos_squared_eq]) 1);
+by (subgoal_tac "sin xa ^ 2 = (y / sqrt (x * x + y * y)) ^ 2" 1);
+by (rtac lemma_cos_sin_eq 2);
+by (Force_tac 2);
+by (Asm_full_simp_tac 2);
+by (auto_tac (claset(),simpset() addsimps [realpow_two_disj,realpow_num_two]
+ delsimps [realpow_Suc]));
+qed "sin_x_y_disj";
+
+(*
+Goal "(x / sqrt (x * x + y * y)) ^ 2 = (x * x) / (x * x + y * y)";
+by Auto_tac;
+val lemma = result();
+Addsimps [lemma];
+
+Goal "(x / sqrt (x * x + y * y)) * (x / sqrt (x * x + y * y)) = \
+\ (x * x) / (x * x + y * y)";
+val lemma_too = result();
+Addsimps [lemma_too];
+*)
+
+Goal "y ~= 0 ==> x / sqrt (x * x + y * y) ~= -(1::real)";
+by Auto_tac;
+by (dres_inst_tac [("f","%x. x ^ 2")] arg_cong 1);
+by (auto_tac (claset(),simpset() addsimps [realpow_divide,
+ realpow_two_eq_mult RS sym]));
+by (forw_inst_tac [("x","x")] real_sum_squares_not_zero2 1);
+by (asm_full_simp_tac (HOL_ss addsimps [realpow_two_eq_mult RS sym]) 1);
+by (forw_inst_tac [("c1","x ^ 2 + y ^ 2")]
+ (real_mult_right_cancel RS iffD2) 1);
+by (assume_tac 1);
+by (dres_inst_tac [("y","x ^ 2 + y ^ 2"),("x","x ^ 2")]
+ (CLAIM "y ~= (0::real) ==> (x/y) * y= x") 1);
+by Auto_tac;
+qed "cos_not_eq_minus_one";
+
+Goalw [arcos_def]
+ "arcos (x / sqrt (x * x + y * y)) = pi ==> y = 0";
+by (rtac ccontr 1);
+by (rtac swap 1 THEN assume_tac 2);
+by (rtac (([cos_x_y_ge_minus_one,cos_x_y_le_one] MRS cos_total) RS
+ ((CLAIM "EX! x. P x ==> EX x. P x") RS someI2_ex)) 1);
+by (auto_tac (claset() addDs [cos_not_eq_minus_one],simpset()));
+qed "arcos_eq_pi_cancel";
+
+Goalw [real_divide_def] "x ~= 0 ==> x / sqrt (x * x + y * y) ~= 0";
+by (forw_inst_tac [("y3","y")] (real_sqrt_sum_squares_gt_zero3
+ RS real_not_refl2 RS not_sym RS real_inverse_not_zero) 1);
+by (auto_tac (claset(),simpset() addsimps [realpow_two_eq_mult]));
+qed "lemma_cos_not_eq_zero";
+
+Goal "[| x ~= 0; \
+\ sin xa = y / sqrt (x * x + y * y) \
+\ |] ==> cos xa = x / sqrt (x * x + y * y) | \
+\ cos xa = - x / sqrt (x * x + y * y)";
+by (dres_inst_tac [("f","%x. x ^ 2")] arg_cong 1);
+by (forw_inst_tac [("y","y")] real_sum_square_gt_zero 1);
+by (asm_full_simp_tac (simpset() addsimps [sin_squared_eq]
+ delsimps [realpow_Suc]) 1);
+by (subgoal_tac "cos xa ^ 2 = (x / sqrt (x * x + y * y)) ^ 2" 1);
+by (rtac lemma_sin_cos_eq 2);
+by (Force_tac 2);
+by (Asm_full_simp_tac 2);
+by (auto_tac (claset(),simpset() addsimps [realpow_two_disj,
+ realpow_num_two] delsimps [realpow_Suc]));
+qed "cos_x_y_disj";
+
+Goal "0 < y ==> - y / sqrt (x * x + y * y) < 0";
+by (case_tac "x = 0" 1);
+by (auto_tac (claset(),simpset() addsimps [abs_eqI2]));
+by (dres_inst_tac [("y","y")] real_sqrt_sum_squares_gt_zero3 1);
+by (auto_tac (claset(),simpset() addsimps [real_0_less_mult_iff,
+ real_divide_def,realpow_two_eq_mult]));
+qed "real_sqrt_divide_less_zero";
+
+Goal "[| x ~= 0; 0 < y |] ==> EX r a. x = r * cos a & y = r * sin a";
+by (res_inst_tac [("x","sqrt(x ^ 2 + y ^ 2)")] exI 1);
+by (res_inst_tac [("x","arcos(x / sqrt (x * x + y * y))")] exI 1);
+by Auto_tac;
+by (dres_inst_tac [("y2","y")] (real_sqrt_sum_squares_gt_zero3
+ RS real_not_refl2 RS not_sym) 1);
+by (auto_tac (claset(),simpset() addsimps [realpow_two_eq_mult]));
+by (rewtac arcos_def);
+by (cut_inst_tac [("x1","x"),("y1","y")] ([cos_x_y_ge_minus_one,cos_x_y_le_one]
+ MRS cos_total) 1);
+by (rtac someI2_ex 1 THEN Blast_tac 1);
+by (thin_tac
+ "EX! xa. 0 <= xa & xa <= pi & cos xa = x / sqrt (x * x + y * y)" 1);
+by (ftac sin_x_y_disj 1 THEN Blast_tac 1);
+by (dres_inst_tac [("y2","y")] (real_sqrt_sum_squares_gt_zero3
+ RS real_not_refl2 RS not_sym) 1);
+by (auto_tac (claset(),simpset() addsimps [realpow_two_eq_mult]));
+by (dtac sin_ge_zero 1 THEN assume_tac 1);
+by (dres_inst_tac [("x","x")] real_sqrt_divide_less_zero 1 THEN Auto_tac);
+qed "polar_ex1";
+
+Goal "x * x = -(y * y) ==> y = (0::real)";
+by (auto_tac (claset() addIs [real_sum_squares_cancel],simpset()));
+qed "real_sum_squares_cancel2a";
+
+Goal "[| x ~= 0; y < 0 |] ==> EX r a. x = r * cos a & y = r * sin a";
+by (cut_inst_tac [("R1.0","0"),("R2.0","x")] real_linear 1);
+by Auto_tac;
+by (res_inst_tac [("x","sqrt(x ^ 2 + y ^ 2)")] exI 1);
+by (res_inst_tac [("x","arcsin(y / sqrt (x * x + y * y))")] exI 1);
+by (auto_tac (claset() addDs [real_sum_squares_cancel2a],
+ simpset() addsimps [realpow_two_eq_mult]));
+by (rewtac arcsin_def);
+by (cut_inst_tac [("x1","x"),("y1","y")] ([cos_x_y_ge_minus_one1a,
+ cos_x_y_le_one2] MRS sin_total) 1);
+by (rtac someI2_ex 1 THEN Blast_tac 1);
+by (thin_tac "EX! xa. - (pi/2) <= xa & \
+\ xa <= pi/2 & sin xa = y / sqrt (x * x + y * y)" 1);
+by (ftac ((CLAIM "0 < x ==> (x::real) ~= 0") RS cos_x_y_disj) 1 THEN Blast_tac 1);
+by Auto_tac;
+by (dtac cos_ge_zero 1 THEN Force_tac 1);
+by (dres_inst_tac [("x","y")] real_sqrt_divide_less_zero 1);
+by (auto_tac (claset(),simpset() addsimps [real_add_commute]));
+by (dtac (ARITH_PROVE "(y::real) < 0 ==> 0 < - y") 1);
+by (dtac (CLAIM "x < (0::real) ==> x ~= 0" RS polar_ex1) 1 THEN assume_tac 1);
+by (REPEAT(etac exE 1));
+by (res_inst_tac [("x","r")] exI 1);
+by (res_inst_tac [("x","-a")] exI 1);
+by Auto_tac;
+qed "polar_ex2";
+
+Goal "EX r a. x = r * cos a & y = r * sin a";
+by (case_tac "x = 0" 1);
+by Auto_tac;
+by (res_inst_tac [("x","y")] exI 1);
+by (res_inst_tac [("x","pi/2")] exI 1 THEN Auto_tac);
+by (cut_inst_tac [("R1.0","0"),("R2.0","y")] real_linear 1);
+by Auto_tac;
+by (res_inst_tac [("x","x")] exI 2);
+by (res_inst_tac [("x","0")] exI 2 THEN Auto_tac);
+by (ALLGOALS(blast_tac (claset() addIs [polar_ex1,polar_ex2])));
+qed "polar_Ex";
+
+Goal "abs x <= sqrt (x ^ 2 + y ^ 2)";
+by (res_inst_tac [("n","1")] realpow_increasing 1);
+by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc RS sym]));
+by (simp_tac (simpset() addsimps [two_eq_Suc_Suc]) 1);
+qed "real_sqrt_ge_abs1";
+
+Goal "abs y <= sqrt (x ^ 2 + y ^ 2)";
+by (rtac (real_add_commute RS subst) 1);
+by (rtac real_sqrt_ge_abs1 1);
+qed "real_sqrt_ge_abs2";
+Addsimps [real_sqrt_ge_abs1,real_sqrt_ge_abs2];
+
+Goal "0 < sqrt 2";
+by (auto_tac (claset() addIs [real_sqrt_gt_zero],simpset()));
+qed "real_sqrt_two_gt_zero";
+Addsimps [real_sqrt_two_gt_zero];
+
+Goal "0 <= sqrt 2";
+by (auto_tac (claset() addIs [real_sqrt_ge_zero],simpset()));
+qed "real_sqrt_two_ge_zero";
+Addsimps [real_sqrt_two_ge_zero];
+
+Goal "1 < sqrt 2";
+by (res_inst_tac [("y","7/5")] order_less_le_trans 1);
+by (res_inst_tac [("n","1")] realpow_increasing 2);
+by (auto_tac (claset(),simpset() addsimps [real_sqrt_gt_zero_pow2,two_eq_Suc_Suc RS sym]
+ delsimps [realpow_Suc]));
+by (simp_tac (simpset() addsimps [two_eq_Suc_Suc]) 1);
+qed "real_sqrt_two_gt_one";
+Addsimps [real_sqrt_two_gt_one];
+
+Goal "0 < u ==> u / sqrt 2 < u";
+by (res_inst_tac [("z1","inverse u")] (real_mult_less_iff1 RS iffD1) 1);
+by Auto_tac;
+by (res_inst_tac [("z1","sqrt 2")] (real_mult_less_iff1 RS iffD1) 1);
+by Auto_tac;
+qed "lemma_real_divide_sqrt_less";
+
+(* needed for infinitely close relation over the nonstandard complex numbers *)
+Goal "[| 0 < u; x < u/2; y < u/2; 0 <= x; 0 <= y |] ==> sqrt (x ^ 2 + y ^ 2) < u";
+by (res_inst_tac [("y","u/sqrt 2")] order_le_less_trans 1);
+by (etac lemma_real_divide_sqrt_less 2);
+by (res_inst_tac [("n","1")] realpow_increasing 1);
+by (auto_tac (claset(),simpset() addsimps [real_0_le_divide_iff,realpow_divide,
+ real_sqrt_gt_zero_pow2,two_eq_Suc_Suc RS sym] delsimps [realpow_Suc]));
+by (res_inst_tac [("t","u ^ 2")] (real_sum_of_halves RS subst) 1);
+by (rtac real_add_le_mono 1);
+by (auto_tac (claset(),simpset() delsimps [realpow_Suc]));
+by (ALLGOALS(rtac ((CLAIM "(2::real) ^ 2 = 4") RS subst)));
+by (ALLGOALS(rtac (realpow_mult RS subst)));
+by (ALLGOALS(rtac realpow_le));
+by Auto_tac;
+qed "lemma_sqrt_hcomplex_capprox";
+
+Addsimps [real_sqrt_sum_squares_ge_zero RS abs_eqI1];
+
+(* A few theorems involving ln and derivatives, etc *)
+
+Goal "DERIV ln z :> l ==> DERIV (%x. exp (ln x)) z :> exp (ln z) * l";
+by (etac DERIV_fun_exp 1);
+qed "lemma_DERIV_ln";
+
+Goal "0 < z ==> ( *f* (%x. exp (ln x))) z = z";
+by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun,
+ hypreal_zero_def,hypreal_less]));
+qed "STAR_exp_ln";
+
+Goal "[|e : Infinitesimal; 0 < x |] ==> 0 < hypreal_of_real x + e";
+by (res_inst_tac [("z1","-e")] (hypreal_add_right_cancel_less RS iffD1) 1);
+by (auto_tac (claset() addIs [Infinitesimal_less_SReal],simpset()));
+qed "hypreal_add_Infinitesimal_gt_zero";
+
+Goalw [nsderiv_def,NSLIM_def] "0 < z ==> NSDERIV (%x. exp (ln x)) z :> 1";
+by Auto_tac;
+by (rtac ccontr 1);
+by (subgoal_tac "0 < hypreal_of_real z + h" 1);
+by (dtac STAR_exp_ln 1);
+by (rtac hypreal_add_Infinitesimal_gt_zero 2);
+by (dtac (CLAIM "h ~= 0 ==> h/h = (1::hypreal)") 1);
+by (auto_tac (claset(),simpset() addsimps [exp_ln_iff RS sym]
+ delsimps [exp_ln_iff]));
+qed "NSDERIV_exp_ln_one";
+
+Goal "0 < z ==> DERIV (%x. exp (ln x)) z :> 1";
+by (auto_tac (claset() addIs [NSDERIV_exp_ln_one],
+ simpset() addsimps [NSDERIV_DERIV_iff RS sym]));
+qed "DERIV_exp_ln_one";
+
+Goal "[| 0 < z; DERIV ln z :> l |] ==> exp (ln z) * l = 1";
+by (rtac DERIV_unique 1);
+by (rtac lemma_DERIV_ln 1);
+by (rtac DERIV_exp_ln_one 2);
+by Auto_tac;
+qed "lemma_DERIV_ln2";
+
+Goal "[| 0 < z; DERIV ln z :> l |] ==> l = 1/(exp (ln z))";
+by (res_inst_tac [("c1","exp(ln z)")] (real_mult_left_cancel RS iffD1) 1);
+by (auto_tac (claset() addIs [lemma_DERIV_ln2],simpset()));
+qed "lemma_DERIV_ln3";
+
+Goal "[| 0 < z; DERIV ln z :> l |] ==> l = 1/z";
+by (res_inst_tac [("t","z")] (exp_ln_iff RS iffD2 RS subst) 1);
+by (auto_tac (claset() addIs [lemma_DERIV_ln3],simpset()));
+qed "lemma_DERIV_ln4";
+
+(* need to rename second isCont_inverse *)
+
+Goal "[| 0 < d; ALL z. abs(z - x) <= d --> g(f(z)) = z; \
+\ ALL z. abs(z - x) <= d --> isCont f z |] \
+\ ==> isCont g (f x)";
+by (simp_tac (simpset() addsimps [isCont_iff,LIM_def]) 1);
+by (Step_tac 1);
+by (dres_inst_tac [("d1.0","r")] real_lbound_gt_zero 1);
+by (assume_tac 1 THEN Step_tac 1);
+by (subgoal_tac "ALL z. abs(z - x) <= e --> (g(f z) = z)" 1);
+by (Force_tac 2);
+by (subgoal_tac "ALL z. abs(z - x) <= e --> isCont f z" 1);
+by (Force_tac 2);
+by (dres_inst_tac [("d","e")] isCont_inj_range 1);
+by (assume_tac 2 THEN assume_tac 1);
+by (Step_tac 1);
+by (res_inst_tac [("x","ea")] exI 1);
+by Auto_tac;
+by (rotate_tac 4 1);
+by (dres_inst_tac [("x","f(x) + xa")] spec 1);
+by Auto_tac;
+by (dtac sym 1 THEN Auto_tac);
+by (arith_tac 1);
+qed "isCont_inv_fun";
+
+(*
+Goalw [isCont_def]
+ "[| isCont f x; f x ~= 0 |] ==> isCont (%x. inverse (f x)) x";
+by (blast_tac (claset() addIs [LIM_inverse]) 1);
+qed "isCont_inverse";
+*)
+
+
+Goal "[| 0 < d; \
+\ ALL z. abs(z - x) <= d --> g(f(z)) = z; \
+\ ALL z. abs(z - x) <= d --> isCont f z |] \
+\ ==> EX e. 0 < (e::real) & \
+\ (ALL y. 0 < abs(y - f(x::real)) & abs(y - f(x)) < e --> f(g(y)) = y)";
+by (dtac isCont_inj_range 1);
+by (assume_tac 2 THEN assume_tac 1);
+by Auto_tac;
+by (res_inst_tac [("x","e")] exI 1 THEN Auto_tac);
+by (rotate_tac 2 1);
+by (dres_inst_tac [("x","y")] spec 1 THEN Auto_tac);
+qed "isCont_inv_fun_inv";
+
+
+(* Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*)
+Goal "[| f -- c --> l; 0 < l |] \
+\ ==> EX r. 0 < r & (ALL x. x ~= c & abs (c - x) < r --> 0 < f x)";
+by (auto_tac (claset(),simpset() addsimps [LIM_def]));
+by (dres_inst_tac [("x","l/2")] spec 1);
+by (Step_tac 1);
+by (Force_tac 1);
+by (res_inst_tac [("x","s")] exI 1);
+by (Step_tac 1);
+by (rotate_tac 2 1);
+by (dres_inst_tac [("x","x")] spec 1);
+by (auto_tac (claset(),HOL_ss addsimps [abs_interval_iff]));
+by (auto_tac (claset(),simpset() addsimps [CLAIM "(l::real) + -(l/2) = l/2",
+ CLAIM "(a < f + - l) = (l + a < (f::real))"]));
+qed "LIM_fun_gt_zero";
+
+Goal "[| f -- c --> l; l < 0 |] \
+\ ==> EX r. 0 < r & (ALL x. x ~= c & abs (c - x) < r --> f x < 0)";
+by (auto_tac (claset(),simpset() addsimps [LIM_def]));
+by (dres_inst_tac [("x","-l/2")] spec 1);
+by (Step_tac 1);
+by (Force_tac 1);
+by (res_inst_tac [("x","s")] exI 1);
+by (Step_tac 1);
+by (rotate_tac 2 1);
+by (dres_inst_tac [("x","x")] spec 1);
+by (auto_tac (claset(),HOL_ss addsimps [abs_interval_iff]));
+by (auto_tac (claset(),simpset() addsimps [CLAIM "(l::real) + -(l/2) = l/2",
+ CLAIM "(f + - l < a) = ((f::real) < l + a)"]));
+qed "LIM_fun_less_zero";
+
+
+Goal "[| f -- c --> l; l ~= 0 |] \
+\ ==> EX r. 0 < r & (ALL x. x ~= c & abs (c - x) < r --> f x ~= 0)";
+by (cut_inst_tac [("R1.0","l"),("R2.0","0")] real_linear 1);
+by Auto_tac;
+by (dtac LIM_fun_less_zero 1);
+by (dtac LIM_fun_gt_zero 3);
+by Auto_tac;
+by (ALLGOALS(res_inst_tac [("x","r")] exI));
+by Auto_tac;
+qed "LIM_fun_not_zero";
--- a/src/HOL/Hyperreal/Transcendental.thy Mon May 05 18:22:31 2003 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Mon May 05 18:23:40 2003 +0200
@@ -1,7 +1,7 @@
(* Title : Transcendental.thy
Author : Jacques D. Fleuriot
Copyright : 1998,1999 University of Cambridge
- 1999 University of Edinburgh
+ 1999,2001 University of Edinburgh
Description : Power Series, transcendental functions etc.
*)
--- a/src/HOL/Hyperreal/ex/ROOT.ML Mon May 05 18:22:31 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-(* Title: HOL/Hyperreal/ex/ROOT.ML
- ID: $Id$
-
-Miscellaneous HOL-Hyperreal Examples.
-*)
-
-no_document use_thy "Primes";
-use_thy "Sqrt";
-use_thy "Sqrt_Script";
--- a/src/HOL/Hyperreal/ex/Sqrt.thy Mon May 05 18:22:31 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,147 +0,0 @@
-(* Title: HOL/Hyperreal/ex/Sqrt.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
- License: GPL (GNU GENERAL PUBLIC LICENSE)
-*)
-
-header {* Square roots of primes are irrational *}
-
-theory Sqrt = Primes + Hyperreal:
-
-subsection {* Preliminaries *}
-
-text {*
- The set of rational numbers, including the key representation
- theorem.
-*}
-
-constdefs
- rationals :: "real set" ("\<rat>")
- "\<rat> \<equiv> {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
-
-theorem rationals_rep: "x \<in> \<rat> \<Longrightarrow>
- \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real m / real n \<and> gcd (m, n) = 1"
-proof -
- assume "x \<in> \<rat>"
- then obtain m n :: nat where
- n: "n \<noteq> 0" and x_rat: "\<bar>x\<bar> = real m / real n"
- by (unfold rationals_def) blast
- let ?gcd = "gcd (m, n)"
- from n have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero)
- let ?k = "m div ?gcd"
- let ?l = "n div ?gcd"
- let ?gcd' = "gcd (?k, ?l)"
- have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m"
- by (rule dvd_mult_div_cancel)
- have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
- by (rule dvd_mult_div_cancel)
-
- from n and gcd_l have "?l \<noteq> 0"
- by (auto iff del: neq0_conv)
- moreover
- have "\<bar>x\<bar> = real ?k / real ?l"
- proof -
- from gcd have "real ?k / real ?l =
- real (?gcd * ?k) / real (?gcd * ?l)"
- by (simp add: real_mult_div_cancel1)
- also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
- also from x_rat have "\<dots> = \<bar>x\<bar>" ..
- finally show ?thesis ..
- qed
- moreover
- have "?gcd' = 1"
- proof -
- have "?gcd * ?gcd' = gcd (?gcd * ?k, ?gcd * ?l)"
- by (rule gcd_mult_distrib2)
- with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
- with gcd show ?thesis by simp
- qed
- ultimately show ?thesis by blast
-qed
-
-lemma [elim?]: "r \<in> \<rat> \<Longrightarrow>
- (\<And>m n. n \<noteq> 0 \<Longrightarrow> \<bar>r\<bar> = real m / real n \<Longrightarrow> gcd (m, n) = 1 \<Longrightarrow> C)
- \<Longrightarrow> C"
- using rationals_rep by blast
-
-
-subsection {* Main theorem *}
-
-text {*
- The square root of any prime number (including @{text 2}) is
- irrational.
-*}
-
-theorem sqrt_prime_irrational: "p \<in> prime \<Longrightarrow> sqrt (real p) \<notin> \<rat>"
-proof
- assume p_prime: "p \<in> prime"
- then have p: "1 < p" by (simp add: prime_def)
- assume "sqrt (real p) \<in> \<rat>"
- then obtain m n where
- n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
- and gcd: "gcd (m, n) = 1" ..
- have eq: "m\<twosuperior> = p * n\<twosuperior>"
- proof -
- from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
- then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"
- by (auto simp add: power_two real_power_two)
- also have "(sqrt (real p))\<twosuperior> = real p" by simp
- also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp
- finally show ?thesis ..
- qed
- have "p dvd m \<and> p dvd n"
- proof
- from eq have "p dvd m\<twosuperior>" ..
- with p_prime show "p dvd m" by (rule prime_dvd_power_two)
- then obtain k where "m = p * k" ..
- with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power_two mult_ac)
- with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power_two)
- then have "p dvd n\<twosuperior>" ..
- with p_prime show "p dvd n" by (rule prime_dvd_power_two)
- qed
- then have "p dvd gcd (m, n)" ..
- with gcd have "p dvd 1" by simp
- then have "p \<le> 1" by (simp add: dvd_imp_le)
- with p show False by simp
-qed
-
-corollary "sqrt (real (2::nat)) \<notin> \<rat>"
- by (rule sqrt_prime_irrational) (rule two_is_prime)
-
-
-subsection {* Variations *}
-
-text {*
- Here is an alternative version of the main proof, using mostly
- linear forward-reasoning. While this results in less top-down
- structure, it is probably closer to proofs seen in mathematics.
-*}
-
-theorem "p \<in> prime \<Longrightarrow> sqrt (real p) \<notin> \<rat>"
-proof
- assume p_prime: "p \<in> prime"
- then have p: "1 < p" by (simp add: prime_def)
- assume "sqrt (real p) \<in> \<rat>"
- then obtain m n where
- n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
- and gcd: "gcd (m, n) = 1" ..
- from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
- then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"
- by (auto simp add: power_two real_power_two)
- also have "(sqrt (real p))\<twosuperior> = real p" by simp
- also have "\<dots> * real (n\<twosuperior>) = real (p * n\<twosuperior>)" by simp
- finally have eq: "m\<twosuperior> = p * n\<twosuperior>" ..
- then have "p dvd m\<twosuperior>" ..
- with p_prime have dvd_m: "p dvd m" by (rule prime_dvd_power_two)
- then obtain k where "m = p * k" ..
- with eq have "p * n\<twosuperior> = p\<twosuperior> * k\<twosuperior>" by (auto simp add: power_two mult_ac)
- with p have "n\<twosuperior> = p * k\<twosuperior>" by (simp add: power_two)
- then have "p dvd n\<twosuperior>" ..
- with p_prime have "p dvd n" by (rule prime_dvd_power_two)
- with dvd_m have "p dvd gcd (m, n)" by (rule gcd_greatest)
- with gcd have "p dvd 1" by simp
- then have "p \<le> 1" by (simp add: dvd_imp_le)
- with p show False by simp
-qed
-
-end
--- a/src/HOL/Hyperreal/ex/Sqrt_Script.thy Mon May 05 18:22:31 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-(* Title: HOL/Hyperreal/ex/Sqrt_Script.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 2001 University of Cambridge
-*)
-
-header {* Square roots of primes are irrational (script version) *}
-
-theory Sqrt_Script = Primes + Hyperreal:
-
-text {*
- \medskip Contrast this linear Isabelle/Isar script with Markus
- Wenzel's more mathematical version.
-*}
-
-subsection {* Preliminaries *}
-
-lemma prime_nonzero: "p \<in> prime \<Longrightarrow> p \<noteq> 0"
- by (force simp add: prime_def)
-
-lemma prime_dvd_other_side:
- "n * n = p * (k * k) \<Longrightarrow> p \<in> prime \<Longrightarrow> p dvd n"
- apply (subgoal_tac "p dvd n * n", blast dest: prime_dvd_mult)
- apply (rule_tac j = "k * k" in dvd_mult_left, simp)
- done
-
-lemma reduction: "p \<in> prime \<Longrightarrow>
- 0 < k \<Longrightarrow> k * k = p * (j * j) \<Longrightarrow> k < p * j \<and> 0 < j"
- apply (rule ccontr)
- apply (simp add: linorder_not_less)
- apply (erule disjE)
- apply (frule mult_le_mono, assumption)
- apply auto
- apply (force simp add: prime_def)
- done
-
-lemma rearrange: "(j::nat) * (p * j) = k * k \<Longrightarrow> k * k = p * (j * j)"
- by (simp add: mult_ac)
-
-lemma prime_not_square:
- "p \<in> prime \<Longrightarrow> (\<And>k. 0 < k \<Longrightarrow> m * m \<noteq> p * (k * k))"
- apply (induct m rule: nat_less_induct)
- apply clarify
- apply (frule prime_dvd_other_side, assumption)
- apply (erule dvdE)
- apply (simp add: nat_mult_eq_cancel_disj prime_nonzero)
- apply (blast dest: rearrange reduction)
- done
-
-
-subsection {* The set of rational numbers *}
-
-constdefs
- rationals :: "real set" ("\<rat>")
- "\<rat> \<equiv> {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}"
-
-
-subsection {* Main theorem *}
-
-text {*
- The square root of any prime number (including @{text 2}) is
- irrational.
-*}
-
-theorem prime_sqrt_irrational:
- "p \<in> prime \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>"
- apply (simp add: rationals_def real_abs_def)
- apply clarify
- apply (erule_tac P = "real m / real n * ?x = ?y" in rev_mp)
- apply (simp del: real_of_nat_mult
- add: real_divide_eq_eq prime_not_square
- real_of_nat_mult [symmetric])
- done
-
-lemmas two_sqrt_irrational =
- prime_sqrt_irrational [OF two_is_prime]
-
-end
--- a/src/HOL/Hyperreal/ex/document/root.tex Mon May 05 18:22:31 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-
-\documentclass[11pt,a4paper]{article}
-\usepackage[latin1]{inputenc}
-\usepackage{isabelle,isabellesym}
-\usepackage{pdfsetup}
-
-\urlstyle{rm}
-\isabellestyle{it}
-
-\begin{document}
-
-\title{Miscellaneous HOL-Hyperreal Examples}
-\maketitle
-
-\tableofcontents
-
-\parindent 0pt\parskip 0.5ex
-\input{session}
-
-\end{document}