# HG changeset patch # User paulson # Date 1052151820 -7200 # Node ID c1c67582c9b523a0e85e1d6edae8c1e3b7831809 # Parent 10dbf16be15ffddfd76490e0b7535f9788959643 New material on integration, etc. Moving Hyperreal/ex to directory Complex diff -r 10dbf16be15f -r c1c67582c9b5 src/HOL/Hyperreal/HLog.ML --- /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"; + diff -r 10dbf16be15f -r c1c67582c9b5 src/HOL/Hyperreal/HLog.thy --- /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 diff -r 10dbf16be15f -r c1c67582c9b5 src/HOL/Hyperreal/HTranscendental.ML --- /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 \ +\ ( *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"; + + + + + diff -r 10dbf16be15f -r c1c67582c9b5 src/HOL/Hyperreal/HTranscendental.thy --- /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 diff -r 10dbf16be15f -r c1c67582c9b5 src/HOL/Hyperreal/Hyperreal.thy --- 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 diff -r 10dbf16be15f -r c1c67582c9b5 src/HOL/Hyperreal/IntFloor.ML --- /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]; + diff -r 10dbf16be15f -r c1c67582c9b5 src/HOL/Hyperreal/IntFloor.thy --- /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 diff -r 10dbf16be15f -r c1c67582c9b5 src/HOL/Hyperreal/Integration.ML --- /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"; diff -r 10dbf16be15f -r c1c67582c9b5 src/HOL/Hyperreal/Integration.thy --- /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 + + diff -r 10dbf16be15f -r c1c67582c9b5 src/HOL/Hyperreal/ROOT.ML --- 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"; diff -r 10dbf16be15f -r c1c67582c9b5 src/HOL/Hyperreal/Transcendental.ML --- 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"; diff -r 10dbf16be15f -r c1c67582c9b5 src/HOL/Hyperreal/Transcendental.thy --- 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. *) diff -r 10dbf16be15f -r c1c67582c9b5 src/HOL/Hyperreal/ex/ROOT.ML --- 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"; diff -r 10dbf16be15f -r c1c67582c9b5 src/HOL/Hyperreal/ex/Sqrt.thy --- 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" ("\") - "\ \ {x. \m n. n \ 0 \ \x\ = real (m::nat) / real (n::nat)}" - -theorem rationals_rep: "x \ \ \ - \m n. n \ 0 \ \x\ = real m / real n \ gcd (m, n) = 1" -proof - - assume "x \ \" - then obtain m n :: nat where - n: "n \ 0" and x_rat: "\x\ = real m / real n" - by (unfold rationals_def) blast - let ?gcd = "gcd (m, n)" - from n have gcd: "?gcd \ 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 \ 0" - by (auto iff del: neq0_conv) - moreover - have "\x\ = 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 "\ = real m / real n" by simp - also from x_rat have "\ = \x\" .. - 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 \ \ \ - (\m n. n \ 0 \ \r\ = real m / real n \ gcd (m, n) = 1 \ C) - \ 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 \ prime \ sqrt (real p) \ \" -proof - assume p_prime: "p \ prime" - then have p: "1 < p" by (simp add: prime_def) - assume "sqrt (real p) \ \" - then obtain m n where - n: "n \ 0" and sqrt_rat: "\sqrt (real p)\ = real m / real n" - and gcd: "gcd (m, n) = 1" .. - have eq: "m\ = p * n\" - proof - - from n and sqrt_rat have "real m = \sqrt (real p)\ * real n" by simp - then have "real (m\) = (sqrt (real p))\ * real (n\)" - by (auto simp add: power_two real_power_two) - also have "(sqrt (real p))\ = real p" by simp - also have "\ * real (n\) = real (p * n\)" by simp - finally show ?thesis .. - qed - have "p dvd m \ p dvd n" - proof - from eq have "p dvd m\" .. - 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\ = p\ * k\" by (auto simp add: power_two mult_ac) - with p have "n\ = p * k\" by (simp add: power_two) - then have "p dvd n\" .. - 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 \ 1" by (simp add: dvd_imp_le) - with p show False by simp -qed - -corollary "sqrt (real (2::nat)) \ \" - 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 \ prime \ sqrt (real p) \ \" -proof - assume p_prime: "p \ prime" - then have p: "1 < p" by (simp add: prime_def) - assume "sqrt (real p) \ \" - then obtain m n where - n: "n \ 0" and sqrt_rat: "\sqrt (real p)\ = real m / real n" - and gcd: "gcd (m, n) = 1" .. - from n and sqrt_rat have "real m = \sqrt (real p)\ * real n" by simp - then have "real (m\) = (sqrt (real p))\ * real (n\)" - by (auto simp add: power_two real_power_two) - also have "(sqrt (real p))\ = real p" by simp - also have "\ * real (n\) = real (p * n\)" by simp - finally have eq: "m\ = p * n\" .. - then have "p dvd m\" .. - 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\ = p\ * k\" by (auto simp add: power_two mult_ac) - with p have "n\ = p * k\" by (simp add: power_two) - then have "p dvd n\" .. - 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 \ 1" by (simp add: dvd_imp_le) - with p show False by simp -qed - -end diff -r 10dbf16be15f -r c1c67582c9b5 src/HOL/Hyperreal/ex/Sqrt_Script.thy --- 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 \ prime \ p \ 0" - by (force simp add: prime_def) - -lemma prime_dvd_other_side: - "n * n = p * (k * k) \ p \ prime \ 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 \ prime \ - 0 < k \ k * k = p * (j * j) \ k < p * j \ 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 \ k * k = p * (j * j)" - by (simp add: mult_ac) - -lemma prime_not_square: - "p \ prime \ (\k. 0 < k \ m * m \ 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" ("\") - "\ \ {x. \m n. n \ 0 \ \x\ = 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 \ prime \ x * x = real p \ 0 \ x \ x \ \" - 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 diff -r 10dbf16be15f -r c1c67582c9b5 src/HOL/Hyperreal/ex/document/root.tex --- 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}