--- a/src/HOL/Real/Hyperreal/HyperDef.ML Thu Dec 21 16:52:10 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML Thu Dec 21 18:08:10 2000 +0100
@@ -707,19 +707,6 @@
simpset()));
qed "hypreal_mult_zero_disj";
-Goal "inverse(x*y) = inverse(x)*inverse(y::hypreal)";
-by (case_tac "x=0 | y=0" 1);
-by (force_tac (claset(), simpset() addsimps [HYPREAL_INVERSE_ZERO]) 1);
-by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
-by (auto_tac (claset(),
- simpset() addsimps [hypreal_mult_assoc RS sym, hypreal_mult_not_0]));
-by (res_inst_tac [("c1","y")] (hypreal_mult_right_cancel RS iffD1) 1);
-by (auto_tac (claset(),
- simpset() addsimps [hypreal_mult_not_0] @ hypreal_mult_ac));
-by (auto_tac (claset(),
- simpset() addsimps [hypreal_mult_assoc RS sym, hypreal_mult_not_0]));
-qed "inverse_mult_eq";
-
Goal "inverse(-x) = -inverse(x::hypreal)";
by (hypreal_div_undefined_case_tac "x=0" 1);
by (rtac (hypreal_mult_right_cancel RS iffD1) 1);
@@ -1052,21 +1039,20 @@
Goal "(0 < -R) = (R < (0::hypreal))";
by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def,
- hypreal_less,hypreal_minus]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_zero_def, hypreal_less,hypreal_minus]));
qed "hypreal_minus_zero_less_iff";
Addsimps [hypreal_minus_zero_less_iff];
Goal "(-R < 0) = ((0::hypreal) < R)";
by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def,
- hypreal_less,hypreal_minus]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_zero_def, hypreal_less,hypreal_minus]));
by (ALLGOALS(Ultra_tac));
qed "hypreal_minus_zero_less_iff2";
Goalw [hypreal_le_def] "((0::hypreal) <= -r) = (r <= (0::hypreal))";
-by (simp_tac (simpset() addsimps
- [hypreal_minus_zero_less_iff2]) 1);
+by (simp_tac (simpset() addsimps [hypreal_minus_zero_less_iff2]) 1);
qed "hypreal_minus_zero_le_iff";
Addsimps [hypreal_minus_zero_le_iff];
@@ -1074,20 +1060,19 @@
hypreal_of_real preserves field and order properties
-----------------------------------------------------------*)
Goalw [hypreal_of_real_def]
- "hypreal_of_real (z1 + z2) = \
-\ hypreal_of_real z1 + hypreal_of_real z2";
-by (asm_simp_tac (simpset() addsimps [hypreal_add,
- hypreal_add_mult_distrib]) 1);
+ "hypreal_of_real (z1 + z2) = hypreal_of_real z1 + hypreal_of_real z2";
+by (simp_tac (simpset() addsimps [hypreal_add, hypreal_add_mult_distrib]) 1);
qed "hypreal_of_real_add";
+Addsimps [hypreal_of_real_add];
Goalw [hypreal_of_real_def]
"hypreal_of_real (z1 * z2) = hypreal_of_real z1 * hypreal_of_real z2";
-by (full_simp_tac (simpset() addsimps [hypreal_mult,
- hypreal_add_mult_distrib2]) 1);
+by (simp_tac (simpset() addsimps [hypreal_mult, hypreal_add_mult_distrib2]) 1);
qed "hypreal_of_real_mult";
+Addsimps [hypreal_of_real_mult];
Goalw [hypreal_less_def,hypreal_of_real_def]
- "(z1 < z2) = (hypreal_of_real z1 < hypreal_of_real z2)";
+ "(z1 < z2) = (hypreal_of_real z1 < hypreal_of_real z2)";
by Auto_tac;
by (res_inst_tac [("x","%n. z1")] exI 1);
by (Step_tac 1);
@@ -1125,28 +1110,24 @@
simpset() addsimps [hypreal_of_real_def,
hypreal_zero_def,FreeUltrafilterNat_Nat_set]));
qed "hypreal_of_real_zero_iff";
+AddIffs [hypreal_of_real_zero_iff];
-(*FIXME: delete*)
-Goal "(hypreal_of_real r ~= 0) = (r ~= #0)";
-by (full_simp_tac (simpset() addsimps [hypreal_of_real_zero_iff]) 1);
-qed "hypreal_of_real_not_zero_iff";
-Goal "inverse (hypreal_of_real r) = hypreal_of_real (inverse r)";
+Goal "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)";
by (case_tac "r=#0" 1);
by (asm_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO, INVERSE_ZERO,
HYPREAL_INVERSE_ZERO, hypreal_of_real_zero]) 1);
by (res_inst_tac [("c1","hypreal_of_real r")]
(hypreal_mult_left_cancel RS iffD1) 1);
-by (etac (hypreal_of_real_not_zero_iff RS iffD2) 1);
-by (forward_tac [hypreal_of_real_not_zero_iff RS iffD2] 1);
-by (auto_tac (claset(),
- simpset() addsimps [hypreal_of_real_one, hypreal_of_real_mult RS sym]));
+by (stac (hypreal_of_real_mult RS sym) 2);
+by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_one]));
qed "hypreal_of_real_inverse";
+Addsimps [hypreal_of_real_inverse];
Goal "hypreal_of_real (z1 / z2) = hypreal_of_real z1 / hypreal_of_real z2";
-by (simp_tac (simpset() addsimps [hypreal_divide_def, real_divide_def,
- hypreal_of_real_mult, hypreal_of_real_inverse]) 1);
+by (simp_tac (simpset() addsimps [hypreal_divide_def, real_divide_def]) 1);
qed "hypreal_of_real_divide";
+Addsimps [hypreal_of_real_divide];
(*** Division lemmas ***)
--- a/src/HOL/Real/Hyperreal/HyperOrd.ML Thu Dec 21 16:52:10 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperOrd.ML Thu Dec 21 18:08:10 2000 +0100
@@ -501,10 +501,11 @@
pnat_add_ac) 1);
qed "hypreal_of_posnat_two";
+(*FIXME: delete this and all posnat*)
Goalw [hypreal_of_posnat_def]
- "hypreal_of_posnat n1 + hypreal_of_posnat n2 = \
-\ hypreal_of_posnat (n1 + n2) + 1hr";
-by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one RS sym,
+ "hypreal_of_posnat n1 + hypreal_of_posnat n2 = \
+\ hypreal_of_posnat (n1 + n2) + 1hr";
+by (full_simp_tac (HOL_ss addsimps [hypreal_of_posnat_one RS sym,
hypreal_of_real_add RS sym,hypreal_of_posnat_def,real_of_preal_add RS sym,
preal_of_prat_add RS sym,prat_of_pnat_add RS sym,pnat_of_nat_add]) 1);
qed "hypreal_of_posnat_add";
@@ -617,11 +618,10 @@
qed "hypreal_of_nat_one";
Goalw [hypreal_of_nat_def]
- "hypreal_of_nat n1 + hypreal_of_nat n2 = \
-\ hypreal_of_nat (n1 + n2)";
+ "hypreal_of_nat n1 + hypreal_of_nat n2 = hypreal_of_nat (n1 + n2)";
by (full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
by (simp_tac (simpset() addsimps [hypreal_of_posnat_add,
- hypreal_add_assoc RS sym]) 1);
+ hypreal_add_assoc RS sym]) 1);
qed "hypreal_of_nat_add";
Goal "hypreal_of_nat 2 = 1hr + 1hr";
--- a/src/HOL/Real/Hyperreal/HyperPow.ML Thu Dec 21 16:52:10 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperPow.ML Thu Dec 21 18:08:10 2000 +0100
@@ -20,7 +20,7 @@
by (induct_tac "n" 1);
by (Auto_tac);
by (forw_inst_tac [("n","n")] hrealpow_not_zero 1);
-by (auto_tac (claset(), simpset() addsimps [inverse_mult_eq]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_inverse_distrib]));
qed_spec_mp "hrealpow_inverse";
Goal "abs (r::hypreal) ^ n = abs (r ^ n)";
--- a/src/HOL/Real/Hyperreal/Lim.ML Thu Dec 21 16:52:10 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Lim.ML Thu Dec 21 18:08:10 2000 +0100
@@ -10,7 +10,6 @@
(fn prems => [cut_facts_tac prems 1,arith_tac 1]);
-
(*---------------------------------------------------------------
Theory of limits, continuity and differentiation of
real=>real functions
@@ -80,19 +79,18 @@
--------------------------*)
Goalw [LIM_def] "k ~= #0 ==> ~ ((%x. k) -- x --> #0)";
by (res_inst_tac [("R1.0","k"),("R2.0","#0")] real_linear_less2 1);
-by (auto_tac (claset(),simpset() addsimps [abs_minus_eqI2,abs_eqI2]));
-by (dtac (rename_numerals (real_minus_zero_less_iff RS iffD2)) 1);
+by (auto_tac (claset(), simpset() addsimps [real_abs_def]));
by (res_inst_tac [("x","-k")] exI 1);
by (res_inst_tac [("x","k")] exI 2);
by Auto_tac;
by (ALLGOALS(dres_inst_tac [("y","s")] real_dense));
-by (Step_tac 1);
+by Safe_tac;
by (ALLGOALS(res_inst_tac [("x","r + x")] exI));
-by (auto_tac (claset(),simpset() addsimps [real_add_assoc,abs_eqI2]));
+by Auto_tac;
qed "LIM_not_zero";
(* [| k ~= #0; (%x. k) -- x --> #0 |] ==> R *)
-bind_thm("LIM_not_zeroE", (LIM_not_zero RS notE));
+bind_thm("LIM_not_zeroE", LIM_not_zero RS notE);
Goal "(%x. k) -- x --> L ==> k = L";
by (rtac ccontr 1);
@@ -193,7 +191,8 @@
\ ==> ALL n::nat. EX xa. xa ~= x & \
\ abs(xa + -x) < inverse(real_of_posnat n) & r <= abs(f xa + -L)";
by (Step_tac 1);
-by (cut_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS real_inverse_gt_zero) 1);
+by (cut_inst_tac [("n1","n")]
+ (real_of_posnat_gt_zero RS real_inverse_gt_zero) 1);
by Auto_tac;
val lemma_LIM = result();
@@ -260,8 +259,7 @@
Goalw [NSLIM_def]
"[| f -- x --NS> l; g -- x --NS> m |] \
\ ==> (%x. f(x) * g(x)) -- x --NS> (l * m)";
-by (auto_tac (claset() addSIs [inf_close_mult_HFinite],
- simpset() addsimps [hypreal_of_real_mult]));
+by (auto_tac (claset() addSIs [inf_close_mult_HFinite], simpset()));
qed "NSLIM_mult";
Goal "[| f -- x --> l; g -- x --> m |] \
@@ -276,8 +274,7 @@
Goalw [NSLIM_def]
"[| f -- x --NS> l; g -- x --NS> m |] \
\ ==> (%x. f(x) + g(x)) -- x --NS> (l + m)";
-by (auto_tac (claset() addSIs [inf_close_add],
- simpset() addsimps [hypreal_of_real_add]));
+by (auto_tac (claset() addSIs [inf_close_add], simpset()));
qed "NSLIM_add";
Goal "[| f -- x --> l; g -- x --> m |] \
@@ -332,45 +329,35 @@
\ ==> (%x. inverse(f(x))) -- a --NS> (inverse L)";
by (Clarify_tac 1);
by (dtac spec 1);
-by (auto_tac (claset(),
- simpset() addsimps [hypreal_of_real_not_zero_iff RS sym,
- hypreal_of_real_inverse RS sym]));
-by (forward_tac [inf_close_hypreal_of_real_not_zero] 1 THEN assume_tac 1);
-by (dtac hypreal_of_real_HFinite_diff_Infinitesimal 1);
-by (auto_tac (claset() addSEs [inf_close_inverse],
- simpset() addsimps [hypreal_of_real_zero_iff]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_of_real_inf_close_inverse]));
qed "NSLIM_inverse";
Goal "[| f -- a --> L; \
\ L ~= #0 |] ==> (%x. inverse(f(x))) -- a --> (inverse L)";
-by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff,
- NSLIM_inverse]) 1);
+by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_inverse]) 1);
qed "LIM_inverse";
(*------------------------------
NSLIM_zero
------------------------------*)
Goal "f -- a --NS> l ==> (%x. f(x) + -l) -- a --NS> #0";
-by (res_inst_tac [("z1","l")] (rename_numerals
- (real_add_minus RS subst)) 1);
+by (res_inst_tac [("z1","l")] (rename_numerals (real_add_minus RS subst)) 1);
by (rtac NSLIM_add_minus 1 THEN Auto_tac);
qed "NSLIM_zero";
Goal "f -- a --> l ==> (%x. f(x) + -l) -- a --> #0";
-by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff,
- NSLIM_zero]) 1);
+by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_zero]) 1);
qed "LIM_zero2";
Goal "(%x. f(x) - l) -- x --NS> #0 ==> f -- x --NS> l";
by (dres_inst_tac [("g","%x. l"),("m","l")] NSLIM_add 1);
-by (auto_tac (claset(),simpset() addsimps [real_diff_def,
- real_add_assoc]));
+by (auto_tac (claset(),simpset() addsimps [real_diff_def, real_add_assoc]));
qed "NSLIM_zero_cancel";
Goal "(%x. f(x) - l) -- x --> #0 ==> f -- x --> l";
by (dres_inst_tac [("g","%x. l"),("m","l")] LIM_add 1);
-by (auto_tac (claset(),simpset() addsimps [real_diff_def,
- real_add_assoc]));
+by (auto_tac (claset(),simpset() addsimps [real_diff_def, real_add_assoc]));
qed "LIM_zero_cancel";
(*--------------------------
@@ -381,17 +368,17 @@
by (res_inst_tac [("x","hypreal_of_real x + ehr")] exI 1);
by (auto_tac (claset() addIs [Infinitesimal_add_inf_close_self
RS inf_close_sym],simpset()));
-by (dres_inst_tac [("x1","-hypreal_of_real x")] (hypreal_add_left_cancel RS iffD2) 1);
+by (dres_inst_tac [("x1","-hypreal_of_real x")]
+ (hypreal_add_left_cancel RS iffD2) 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym,
- hypreal_epsilon_not_zero]) 1);
+ hypreal_epsilon_not_zero]) 1);
qed "NSLIM_not_zero";
(* [| k ~= #0; (%x. k) -- x --NS> #0 |] ==> R *)
-bind_thm("NSLIM_not_zeroE", (NSLIM_not_zero RS notE));
+bind_thm("NSLIM_not_zeroE", NSLIM_not_zero RS notE);
Goal "k ~= #0 ==> ~ ((%x. k) -- x --> #0)";
-by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff,
- NSLIM_not_zero]) 1);
+by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_not_zero]) 1);
qed "LIM_not_zero2";
(*-------------------------------------
@@ -416,13 +403,11 @@
Goal "[| f -- x --NS> L; f -- x --NS> M |] ==> L = M";
by (dtac NSLIM_minus 1);
by (dtac NSLIM_add 1 THEN assume_tac 1);
-by (auto_tac (claset() addSDs [NSLIM_const_eq RS sym],
- simpset() addsimps [real_add_minus]));
+by (auto_tac (claset() addSDs [NSLIM_const_eq RS sym], simpset()));
qed "NSLIM_unique";
Goal "[| f -- x --> L; f -- x --> M |] ==> L = M";
-by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff,
- NSLIM_unique]) 1);
+by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_unique]) 1);
qed "LIM_unique2";
(*--------------------
@@ -560,8 +545,7 @@
------------------------*)
Goal "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) + g(x)) a";
by (auto_tac (claset() addIs [inf_close_add],
- simpset() addsimps [isNSCont_isCont_iff RS sym, isNSCont_def,
- hypreal_of_real_add]));
+ simpset() addsimps [isNSCont_isCont_iff RS sym, isNSCont_def]));
qed "isCont_add";
(*------------------------
@@ -570,7 +554,7 @@
Goal "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a";
by (auto_tac (claset() addSIs [starfun_mult_HFinite_inf_close],
simpset() delsimps [starfun_mult RS sym]
- addsimps [isNSCont_isCont_iff RS sym, isNSCont_def, hypreal_of_real_mult]));
+ addsimps [isNSCont_isCont_iff RS sym, isNSCont_def]));
qed "isCont_mult";
(*-------------------------------------------
@@ -714,21 +698,17 @@
by (Ultra_tac 1);
qed "isUCont_isNSUCont";
-Goal "ALL s. #0 < s --> \
-\ (EX xa y. abs (xa + - y) < s & \
-\ r <= abs (f xa + -f y)) ==> \
-\ ALL n::nat. EX xa y. \
-\ abs(xa + -y) < inverse(real_of_posnat n) & \
-\ r <= abs(f xa + -f y)";
+Goal "ALL s. #0 < s --> (EX z y. abs (z + - y) < s & r <= abs (f z + -f y)) \
+\ ==> ALL n::nat. EX z y. \
+\ abs(z + -y) < inverse(real_of_posnat n) & \
+\ r <= abs(f z + -f y)";
by (Step_tac 1);
by (cut_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS real_inverse_gt_zero) 1);
by Auto_tac;
val lemma_LIMu = result();
-Goal "ALL s. #0 < s --> \
-\ (EX xa y. abs (xa + - y) < s & \
-\ r <= abs (f xa + -f y)) ==> \
-\ EX X Y. ALL n::nat. \
+Goal "ALL s. #0 < s --> (EX z y. abs (z + - y) < s & r <= abs (f z + -f y)) \
+\ ==> EX X Y. ALL n::nat. \
\ abs(X n + -(Y n)) < inverse(real_of_posnat n) & \
\ r <= abs(f (X n) + -f (Y n))";
by (dtac lemma_LIMu 1);
@@ -744,30 +724,22 @@
by (Auto_tac );
val lemma_simpu = result();
-Goal "{n. f (X n) + - f(Y n) = Ya n} Int \
-\ {n. abs (X n + - Y n) < inverse (real_of_posnat n) & \
-\ r <= abs (f (X n) + - f(Y n))} <= \
-\ {n. r <= abs (Ya n)}";
-by Auto_tac;
-val lemma_Intu = result ();
-
Goalw [isNSUCont_def,isUCont_def,inf_close_def]
"isNSUCont f ==> isUCont f";
by (asm_full_simp_tac (simpset() addsimps
- [Infinitesimal_FreeUltrafilterNat_iff]) 1);
+ [Infinitesimal_FreeUltrafilterNat_iff]) 1);
by (EVERY1[Step_tac, rtac ccontr, Asm_full_simp_tac]);
by (fold_tac [real_le_def]);
by (dtac lemma_skolemize_LIM2u 1);
by (Step_tac 1);
by (dres_inst_tac [("x","Abs_hypreal(hyprel^^{X})")] spec 1);
by (dres_inst_tac [("x","Abs_hypreal(hyprel^^{Y})")] spec 1);
-by (asm_full_simp_tac (simpset() addsimps [starfun,
- hypreal_minus,hypreal_add]) 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [starfun, hypreal_minus,hypreal_add]) 1);
by Auto_tac;
by (dtac (lemma_simpu RS real_seq_to_hypreal_Infinitesimal2) 1);
by (asm_full_simp_tac (simpset() addsimps
- [Infinitesimal_FreeUltrafilterNat_iff,
- hypreal_minus,hypreal_add]) 1);
+ [Infinitesimal_FreeUltrafilterNat_iff, hypreal_minus,hypreal_add]) 1);
by (Blast_tac 1);
by (rotate_tac 2 1);
by (dres_inst_tac [("x","r")] spec 1);
@@ -808,10 +780,11 @@
Goalw [nsderiv_def]
"[| NSDERIV f x :> D; NSDERIV f x :> E |] ==> D = E";
-by (cut_facts_tac [Infinitesimal_epsilon,
- hypreal_epsilon_not_zero] 1);
-by (auto_tac (claset() addSDs [bspec] addSIs
- [inj_hypreal_of_real RS injD] addDs [inf_close_trans3],simpset()));
+by (cut_facts_tac [Infinitesimal_epsilon, hypreal_epsilon_not_zero] 1);
+by (auto_tac (claset() addSDs [inst "x" "ehr" bspec]
+ addSIs [inj_hypreal_of_real RS injD]
+ addDs [inf_close_trans3],
+ simpset()));
qed "NSDeriv_unique";
(*------------------------------------------------------------------------
@@ -1016,8 +989,7 @@
(* use simple constant nslimit theorem *)
Goal "(NSDERIV (%x. k) x :> #0)";
-by (simp_tac (simpset() addsimps
- [NSDERIV_NSLIM_iff,real_add_minus]) 1);
+by (simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff]) 1);
qed "NSDERIV_const";
Addsimps [NSDERIV_const];
@@ -1036,9 +1008,7 @@
by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff,
NSLIM_def]) 1 THEN REPEAT(Step_tac 1));
by (auto_tac (claset(),
- simpset() addsimps [hypreal_of_real_add,
- hypreal_of_real_divide,
- hypreal_add_divide_distrib]));
+ simpset() addsimps [hypreal_add_divide_distrib]));
by (thin_tac "xa @= hypreal_of_real #0" 1 THEN dtac inf_close_add 1);
by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
qed "NSDERIV_add";
@@ -1089,16 +1059,15 @@
by (dres_inst_tac [("D","Db")] lemma_nsderiv2 1);
by (dtac (inf_close_minus_iff RS iffD2 RS (bex_Infinitesimal_iff2 RS iffD2)) 4);
by (auto_tac (claset() addSIs [inf_close_add_mono1],
- simpset() addsimps [hypreal_of_real_add,hypreal_add_mult_distrib,
- hypreal_add_mult_distrib2,hypreal_of_real_mult,hypreal_mult_commute,
- hypreal_add_assoc]));
+ simpset() addsimps [hypreal_add_mult_distrib, hypreal_add_mult_distrib2,
+ hypreal_mult_commute, hypreal_add_assoc]));
by (res_inst_tac [("w1","hypreal_of_real Db * hypreal_of_real (f x)")]
(hypreal_add_commute RS subst) 1);
-by (auto_tac (claset() addSIs [Infinitesimal_add_inf_close_self2 RS
- inf_close_sym,Infinitesimal_add,Infinitesimal_mult,
- Infinitesimal_hypreal_of_real_mult,
- Infinitesimal_hypreal_of_real_mult2 ],
- simpset() addsimps [hypreal_add_assoc RS sym]));
+by (auto_tac (claset() addSIs [Infinitesimal_add_inf_close_self2 RS inf_close_sym,
+ Infinitesimal_add, Infinitesimal_mult,
+ Infinitesimal_hypreal_of_real_mult,
+ Infinitesimal_hypreal_of_real_mult2],
+ simpset() addsimps [hypreal_add_assoc RS sym]));
qed "NSDERIV_mult";
Goal "[| DERIV f x :> Da; DERIV g x :> Db |] \
@@ -1289,18 +1258,16 @@
hypreal_of_real_zero, mem_infmal_iff, starfun_lambda_cancel]));
qed "NSDERIVD2";
-(*---------------------------------------------
- This proof uses both possible definitions
- for differentiability.
- --------------------------------------------*)
+(*------------------------------------------------------
+ This proof uses both definitions of differentiability.
+ ------------------------------------------------------*)
Goal "[| NSDERIV f (g x) :> Da; NSDERIV g x :> Db |] \
\ ==> NSDERIV (f o g) x :> Da * Db";
by (asm_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff,
NSLIM_def,hypreal_of_real_zero,mem_infmal_iff RS sym]) 1 THEN Step_tac 1);
by (forw_inst_tac [("f","g")] NSDERIV_inf_close 1);
by (auto_tac (claset(),
- simpset() addsimps [hypreal_of_real_mult,
- starfun_lambda_cancel2, starfun_o RS sym]));
+ simpset() addsimps [starfun_lambda_cancel2, starfun_o RS sym]));
by (case_tac "(*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real (g x)" 1);
by (dres_inst_tac [("g","g")] NSDERIV_zero 1);
by (auto_tac (claset(),
@@ -1386,16 +1353,12 @@
by (forward_tac [Infinitesimal_add_not_zero] 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 2);
by (auto_tac (claset(),
- simpset() addsimps [starfun_inverse_inverse,
- hypreal_of_real_inverse RS sym, realpow_two,
- hypreal_of_real_mult,
- hypreal_of_real_divide]
+ simpset() addsimps [starfun_inverse_inverse, realpow_two]
delsimps [hypreal_minus_mult_eq1 RS sym,
hypreal_minus_mult_eq2 RS sym]));
-by (dtac (hypreal_of_real_not_zero_iff RS iffD2) 1);
by (asm_full_simp_tac
(simpset() addsimps [hypreal_inverse_add,
- inverse_mult_eq RS sym, hypreal_minus_inverse RS sym]
+ hypreal_inverse_distrib RS sym, hypreal_minus_inverse RS sym]
@ hypreal_add_ac @ hypreal_mult_ac
delsimps [hypreal_minus_mult_eq1 RS sym,
hypreal_minus_mult_eq2 RS sym] ) 1);
@@ -1403,22 +1366,18 @@
hypreal_add_mult_distrib2]
delsimps [hypreal_minus_mult_eq1 RS sym,
hypreal_minus_mult_eq2 RS sym]) 1);
-by (dres_inst_tac [("x3","x") ] ((HFinite_hypreal_of_real RSN
- (2,Infinitesimal_HFinite_mult2)) RS
- (Infinitesimal_minus_iff RS iffD1)) 1);
-by (forw_inst_tac [("x","hypreal_of_real x"),("y","hypreal_of_real x")]
- hypreal_mult_not_0 1);
by (res_inst_tac [("y"," inverse(- hypreal_of_real x * hypreal_of_real x)")]
- inf_close_trans 2);
-by (rtac inverse_add_Infinitesimal_inf_close2 2);
-by (auto_tac (claset() addIs [HFinite_minus_iff RS iffD1]
- addSDs [Infinitesimal_minus_iff RS iffD2,
- hypreal_of_real_HFinite_diff_Infinitesimal], simpset() addsimps
- [hypreal_minus_inverse RS sym,hypreal_of_real_mult RS sym]));
+ inf_close_trans 1);
+by (rtac inverse_add_Infinitesimal_inf_close2 1);
+by (auto_tac (claset() addSDs [hypreal_of_real_HFinite_diff_Infinitesimal],
+ simpset() addsimps [hypreal_minus_inverse RS sym,
+ HFinite_minus_iff RS sym,
+ Infinitesimal_minus_iff RS sym]));
+by (rtac Infinitesimal_HFinite_mult2 1);
+by Auto_tac;
qed "NSDERIV_inverse";
-
Goal "x ~= #0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))";
by (asm_simp_tac (simpset() addsimps [NSDERIV_inverse,
NSDERIV_DERIV_iff RS sym] delsimps [realpow_Suc]) 1);
@@ -1777,9 +1736,9 @@
by (blast_tac (claset() addIs [IVT2]) 1);
qed "IVT2_objl";
-(*----------------------------------------------------------------------------*)
-(* By bisection, function continuous on closed interval is bounded above *)
-(*----------------------------------------------------------------------------*)
+(*---------------------------------------------------------------------------*)
+(* By bisection, function continuous on closed interval is bounded above *)
+(*---------------------------------------------------------------------------*)
Goal "abs (real_of_nat x) = real_of_nat x";
by (auto_tac (claset() addIs [abs_eqI1],simpset()));
@@ -2009,7 +1968,7 @@
by (Step_tac 1);
by (dres_inst_tac [("x","x - e")] spec 1);
by (dres_inst_tac [("x","x + e")] spec 2);
-by (auto_tac (claset(), simpset() addsimps [abs_eqI2]));
+by (auto_tac (claset(), simpset() addsimps [real_abs_def]));
qed "DERIV_local_max";
(*----------------------------------------------------------------------------*)
--- a/src/HOL/Real/Hyperreal/NSA.ML Thu Dec 21 16:52:10 2000 +0100
+++ b/src/HOL/Real/Hyperreal/NSA.ML Thu Dec 21 18:08:10 2000 +0100
@@ -18,7 +18,7 @@
Goalw [SReal_def] "[| x: SReal; y: SReal |] ==> x + y: SReal";
by (Step_tac 1);
by (res_inst_tac [("x","r + ra")] exI 1);
-by (simp_tac (simpset() addsimps [hypreal_of_real_add]) 1);
+by (Simp_tac 1);
qed "SReal_add";
Goalw [SReal_def] "[| x: SReal; y: SReal |] ==> x * y: SReal";
@@ -28,7 +28,7 @@
qed "SReal_mult";
Goalw [SReal_def] "x: SReal ==> inverse x : SReal";
-by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_inverse]));
+by (blast_tac (claset() addIs [hypreal_of_real_inverse RS sym]) 1);
qed "SReal_inverse";
Goalw [SReal_def] "x: SReal ==> -x : SReal";
@@ -215,7 +215,7 @@
by (blast_tac (claset() addSIs [SReal_add,hrabs_add_less]) 1);
qed "HFinite_add";
-Goalw [HFinite_def] "[|x : HFinite;y : HFinite|] ==> (x*y) : HFinite";
+Goalw [HFinite_def] "[|x : HFinite; y : HFinite|] ==> (x*y) : HFinite";
by (blast_tac (claset() addSIs [SReal_mult,hrabs_mult_less]) 1);
qed "HFinite_mult";
@@ -224,15 +224,18 @@
qed "HFinite_minus_iff";
Goal "[| x: HFinite; y: HFinite|] ==> (x + -y): HFinite";
-by (blast_tac (claset() addDs [HFinite_minus_iff RS iffD1] addIs [HFinite_add]) 1);
+by (blast_tac (claset() addDs [HFinite_minus_iff RS iffD1]
+ addIs [HFinite_add]) 1);
qed "HFinite_add_minus";
Goalw [SReal_def,HFinite_def] "SReal <= HFinite";
by Auto_tac;
by (res_inst_tac [("x","1hr + abs(hypreal_of_real r)")] exI 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_hrabs,
- hypreal_of_real_one RS sym,hypreal_of_real_add RS sym,
- hypreal_of_real_zero RS sym]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_of_real_hrabs, hypreal_zero_less_one]));
+by (res_inst_tac [("x","#1 + abs r")] exI 1);
+by (simp_tac (simpset() addsimps [hypreal_of_real_one,
+ hypreal_of_real_zero]) 1);
qed "SReal_subset_HFinite";
Goal "hypreal_of_real x : HFinite";
@@ -285,7 +288,7 @@
Goalw [Infinitesimal_def] "0 : Infinitesimal";
by (simp_tac (simpset() addsimps [hrabs_zero]) 1);
qed "Infinitesimal_zero";
-Addsimps [Infinitesimal_zero];
+AddIffs [Infinitesimal_zero];
Goalw [Infinitesimal_def]
"[| x : Infinitesimal; y : Infinitesimal |] ==> (x + y) : Infinitesimal";
@@ -466,7 +469,7 @@
qed "Infinitesimal_interval2";
Goalw [Infinitesimal_def]
- "!! x y. [| x ~: Infinitesimal; \
+ "[| x ~: Infinitesimal; \
\ y ~: Infinitesimal|] \
\ ==> (x*y) ~:Infinitesimal";
by (Clarify_tac 1);
@@ -480,17 +483,17 @@
by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
qed "not_Infinitesimal_mult";
-Goal "!! x. x*y : Infinitesimal ==> x : Infinitesimal | y : Infinitesimal";
+Goal "x*y : Infinitesimal ==> x : Infinitesimal | y : Infinitesimal";
by (rtac ccontr 1);
by (dtac (de_Morgan_disj RS iffD1) 1);
by (fast_tac (claset() addDs [not_Infinitesimal_mult]) 1);
qed "Infinitesimal_mult_disj";
-Goal "!! x. x: HFinite-Infinitesimal ==> x ~= 0";
-by (fast_tac (claset() addIs [Infinitesimal_zero]) 1);
+Goal "x: HFinite-Infinitesimal ==> x ~= 0";
+by (Blast_tac 1);
qed "HFinite_Infinitesimal_not_zero";
-Goal "!! x. [| x : HFinite - Infinitesimal; \
+Goal "[| x : HFinite - Infinitesimal; \
\ y : HFinite - Infinitesimal \
\ |] ==> (x*y) : HFinite - Infinitesimal";
by (Clarify_tac 1);
@@ -534,7 +537,7 @@
by (Simp_tac 1);
qed "inf_close_refl";
-Goalw [inf_close_def] "!! x y. x @= y ==> y @= x";
+Goalw [inf_close_def] "x @= y ==> y @= x";
by (rtac (hypreal_minus_distrib1 RS subst) 1);
by (etac (Infinitesimal_minus_iff RS iffD1) 1);
qed "inf_close_sym";
@@ -570,7 +573,7 @@
simpset() addsimps [inf_close_refl]));
qed "inf_close_monad_iff";
-Goal "!!x y. [| x: Infinitesimal; y: Infinitesimal |] ==> x @= y";
+Goal "[| x: Infinitesimal; y: Infinitesimal |] ==> x @= y";
by (asm_full_simp_tac (simpset() addsimps [mem_infmal_iff]) 1);
by (fast_tac (claset() addIs [inf_close_trans2]) 1);
qed "Infinitesimal_inf_close";
@@ -847,13 +850,12 @@
Goal "[| x: SReal; x: Infinitesimal|] ==> x = 0";
by (cut_facts_tac [SReal_Int_Infinitesimal_zero] 1);
-by (blast_tac (claset() addEs [equalityE]) 1);
+by (Blast_tac 1);
qed "SReal_Infinitesimal_zero";
-Goal "[| x : SReal; x ~= 0 |] \
-\ ==> x : HFinite - Infinitesimal";
+Goal "[| x : SReal; x ~= 0 |] ==> x : HFinite - Infinitesimal";
by (auto_tac (claset() addDs [SReal_Infinitesimal_zero,
- SReal_subset_HFinite RS subsetD],simpset()));
+ SReal_subset_HFinite RS subsetD], simpset()));
qed "SReal_HFinite_diff_Infinitesimal";
Goal "hypreal_of_real x ~= 0 ==> hypreal_of_real x : HFinite - Infinitesimal";
@@ -861,6 +863,14 @@
by Auto_tac;
qed "hypreal_of_real_HFinite_diff_Infinitesimal";
+Goal "(hypreal_of_real x : Infinitesimal) = (x=0)";
+by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_zero]));
+by (rtac ccontr 1);
+by (rtac (hypreal_of_real_HFinite_diff_Infinitesimal RS DiffD2) 1);
+by Auto_tac;
+qed "hypreal_of_real_Infinitesimal_iff_0";
+AddIffs [hypreal_of_real_Infinitesimal_iff_0];
+
Goal "1hr+1hr ~: Infinitesimal";
by (fast_tac (claset() addDs [SReal_two RS SReal_Infinitesimal_zero]
addSEs [hypreal_two_not_zero RS notE]) 1);
@@ -1220,10 +1230,15 @@
simpset() addsimps [hypreal_mult_assoc]));
qed "inf_close_inverse";
+(*Used for NSLIM_inverse, NSLIMSEQ_inverse*)
+bind_thm ("hypreal_of_real_inf_close_inverse",
+ hypreal_of_real_HFinite_diff_Infinitesimal RSN (2, inf_close_inverse));
+
Goal "[| x: HFinite - Infinitesimal; \
-\ h : Infinitesimal |] ==> inverse(x + h) @= inverse x";
-by (auto_tac (claset() addIs [inf_close_inverse,
- Infinitesimal_add_inf_close_self,inf_close_sym],simpset()));
+\ h : Infinitesimal |] ==> inverse(x + h) @= inverse x";
+by (auto_tac (claset() addIs [inf_close_inverse, inf_close_sym,
+ Infinitesimal_add_inf_close_self],
+ simpset()));
qed "inverse_add_Infinitesimal_inf_close";
Goal "[| x: HFinite - Infinitesimal; \
@@ -1293,7 +1308,7 @@
by Auto_tac;
qed "monad_hrabs_Un_subset";
-Goal "!! e. e : Infinitesimal ==> monad (x+e) = monad x";
+Goal "e : Infinitesimal ==> monad (x+e) = monad x";
by (fast_tac (claset() addSIs [Infinitesimal_add_inf_close_self RS inf_close_sym,
inf_close_monad_iff RS iffD1]) 1);
qed "Infinitesimal_monad_eq";
@@ -1348,25 +1363,25 @@
by (blast_tac (claset() addSIs [inf_close_sym]) 1);
qed "inf_close_mem_monad2";
-Goal "!! x y. [| x @= y;x:monad 0 |] ==> y:monad 0";
+Goal "[| x @= y;x:monad 0 |] ==> y:monad 0";
by (dtac mem_monad_inf_close 1);
by (fast_tac (claset() addIs [inf_close_mem_monad,inf_close_trans]) 1);
qed "inf_close_mem_monad_zero";
-Goal "!! x y. [| x @= y; x: Infinitesimal |] ==> abs x @= abs y";
+Goal "[| x @= y; x: Infinitesimal |] ==> abs x @= abs y";
by (fast_tac (claset() addIs [(Infinitesimal_monad_zero_iff RS iffD1),
inf_close_mem_monad_zero,(monad_zero_hrabs_iff RS iffD1),
mem_monad_inf_close,inf_close_trans3]) 1);
qed "Infinitesimal_inf_close_hrabs";
-Goal "!! x. [| 0 < x; x ~:Infinitesimal |] \
+Goal "[| 0 < x; x ~:Infinitesimal |] \
\ ==> ALL e: Infinitesimal. e < x";
by (Step_tac 1 THEN rtac ccontr 1);
by (auto_tac (claset() addIs [Infinitesimal_zero RSN (2, Infinitesimal_interval)]
addSDs [hypreal_leI RS hypreal_le_imp_less_or_eq],simpset()));
qed "Ball_Infinitesimal_less";
-Goal "!! x. [| 0 < x; x ~: Infinitesimal|] \
+Goal "[| 0 < x; x ~: Infinitesimal|] \
\ ==> ALL u: monad x. 0 < u";
by (Step_tac 1);
by (dtac (mem_monad_inf_close RS inf_close_sym) 1);
@@ -1376,7 +1391,7 @@
by (auto_tac (claset(),simpset() addsimps [Infinitesimal_minus_iff RS sym]));
qed "Ball_mem_monad_gt_zero";
-Goal "!! x. [| x < 0; x ~: Infinitesimal|] \
+Goal "[| x < 0; x ~: Infinitesimal|] \
\ ==> ALL u: monad x. u < 0";
by (Step_tac 1);
by (dtac (mem_monad_inf_close RS inf_close_sym) 1);
@@ -1460,12 +1475,11 @@
by (dres_inst_tac [("x","hypreal_of_real y + -hypreal_of_real x")] bspec 1);
by (auto_tac (claset(),
simpset() addsimps [hypreal_add_commute,
- hypreal_of_real_add, hrabs_interval_iff,
+ hrabs_interval_iff,
SReal_add, SReal_minus]));
by (dres_inst_tac [("x1","xa")] (hypreal_less_minus_iff RS iffD1) 1);
by (auto_tac (claset(),
- simpset() addsimps [hypreal_minus_add_distrib,hypreal_of_real_add] @
- hypreal_add_ac));
+ simpset() addsimps [hypreal_minus_add_distrib] @ hypreal_add_ac));
qed "Infinitesimal_add_hypreal_of_real_less";
Goal "[| x: Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |] \
@@ -1501,51 +1515,49 @@
qed "Infinitesimal_add_cancel_real_le";
Goalw [hypreal_le_def]
- "[| xa: Infinitesimal; ya: Infinitesimal; \
-\ hypreal_of_real x + xa <= hypreal_of_real y + ya \
-\ |] ==> hypreal_of_real x <= hypreal_of_real y";
+ "[| xa: Infinitesimal; ya: Infinitesimal; \
+\ hypreal_of_real x + xa <= hypreal_of_real y + ya |] \
+\ ==> hypreal_of_real x <= hypreal_of_real y";
by (EVERY1[rtac notI, rtac contrapos_np, assume_tac]);
by (res_inst_tac [("C","-xa")] hypreal_less_add_right_cancel 1);
by (dtac (Infinitesimal_minus_iff RS iffD1) 1);
by (dtac Infinitesimal_add 1 THEN assume_tac 1);
by (auto_tac (claset() addIs [Infinitesimal_add_hypreal_of_real_less],
- simpset() addsimps [hypreal_add_assoc]));
+ simpset() addsimps [hypreal_add_assoc]));
qed "hypreal_of_real_le_add_Infininitesimal_cancel";
Goal "[| xa: Infinitesimal; ya: Infinitesimal; \
-\ hypreal_of_real x + xa <= hypreal_of_real y + ya \
-\ |] ==> x <= y";
+\ hypreal_of_real x + xa <= hypreal_of_real y + ya |] \
+\ ==> x <= y";
by (blast_tac (claset() addSIs [hypreal_of_real_le_iff RS iffD2,
- hypreal_of_real_le_add_Infininitesimal_cancel]) 1);
+ hypreal_of_real_le_add_Infininitesimal_cancel]) 1);
qed "hypreal_of_real_le_add_Infininitesimal_cancel2";
Goal "[| hypreal_of_real x < e; e: Infinitesimal |] ==> hypreal_of_real x <= 0";
by (rtac hypreal_leI 1 THEN Step_tac 1);
by (dtac Infinitesimal_interval 1);
by (dtac (SReal_hypreal_of_real RS SReal_Infinitesimal_zero) 4);
-by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_of_real_zero, hypreal_less_not_refl]));
qed "hypreal_of_real_less_Infinitesimal_le_zero";
-Goal "[| h: Infinitesimal; x ~= 0 |] \
-\ ==> hypreal_of_real x + h ~= 0";
+(*used once, in NSDERIV_inverse*)
+Goal "[| h: Infinitesimal; x ~= 0 |] ==> hypreal_of_real x + h ~= 0";
by (res_inst_tac [("t","h")] (hypreal_minus_minus RS subst) 1);
by (rtac (not_sym RS (hypreal_not_eq_minus_iff RS iffD1)) 1);
by (dtac (Infinitesimal_minus_iff RS iffD1) 1);
-by (auto_tac (claset() addDs [((hypreal_of_real_not_zero_iff RS iffD2) RS
- hypreal_of_real_HFinite_diff_Infinitesimal)],simpset()));
+by Auto_tac;
qed "Infinitesimal_add_not_zero";
Goal "x*x + y*y : Infinitesimal ==> x*x : Infinitesimal";
by (blast_tac (claset() addIs [hypreal_self_le_add_pos,
- Infinitesimal_interval2,hypreal_le_square,
- Infinitesimal_zero]) 1);
+ Infinitesimal_interval2, hypreal_le_square]) 1);
qed "Infinitesimal_square_cancel";
Addsimps [Infinitesimal_square_cancel];
Goal "x*x + y*y : HFinite ==> x*x : HFinite";
by (blast_tac (claset() addIs [hypreal_self_le_add_pos,
- HFinite_bounded,hypreal_le_square,
- HFinite_zero]) 1);
+ HFinite_bounded,hypreal_le_square, HFinite_zero]) 1);
qed "HFinite_square_cancel";
Addsimps [HFinite_square_cancel];
@@ -1565,8 +1577,7 @@
Goal "x*x + y*y + z*z : Infinitesimal ==> x*x : Infinitesimal";
by (blast_tac (claset() addIs [hypreal_self_le_add_pos2,
- Infinitesimal_interval2,hypreal_le_square,
- Infinitesimal_zero]) 1);
+ Infinitesimal_interval2,hypreal_le_square]) 1);
qed "Infinitesimal_sum_square_cancel";
Addsimps [Infinitesimal_sum_square_cancel];
@@ -1654,7 +1665,7 @@
addSEs [inf_close_trans3],simpset()));
qed "st_eq_inf_close";
-Goal "!! x. [| x: HFinite; y: HFinite; x @= y |] ==> st x = st y";
+Goal "[| x: HFinite; y: HFinite; x @= y |] ==> st x = st y";
by (EVERY1 [forward_tac [st_inf_close_self],
forw_inst_tac [("x","y")] st_inf_close_self,
dtac st_SReal,dtac st_SReal]);
@@ -1662,7 +1673,7 @@
inf_close_trans2,SReal_inf_close_iff RS iffD1]) 1);
qed "inf_close_st_eq";
-Goal "!! x y. [| x: HFinite; y: HFinite|] \
+Goal "[| x: HFinite; y: HFinite|] \
\ ==> (x @= y) = (st x = st y)";
by (blast_tac (claset() addIs [inf_close_st_eq,
st_eq_inf_close]) 1);
@@ -1765,7 +1776,7 @@
by (blast_tac (claset() addSIs [lemma_st_mult]) 1);
qed "st_mult";
-Goal "!! x. st(x) ~= 0 ==> x ~=0";
+Goal "st(x) ~= 0 ==> x ~=0";
by (fast_tac (claset() addIs [st_zero]) 1);
qed "st_not_zero";
@@ -1776,7 +1787,7 @@
RS subsetD],simpset() addsimps [mem_infmal_iff RS sym]));
qed "st_Infinitesimal";
-Goal "!! x. st(x) ~= 0 ==> x ~: Infinitesimal";
+Goal "st(x) ~= 0 ==> x ~: Infinitesimal";
by (fast_tac (claset() addIs [st_Infinitesimal]) 1);
qed "st_not_Infinitesimal";
@@ -2050,27 +2061,26 @@
Goal "(ALL r: SReal. 0 < r --> x < r) = \
\ (ALL n. x < inverse(hypreal_of_posnat n))";
by (Step_tac 1);
-by (dres_inst_tac [("x","hypreal_of_real (inverse(real_of_posnat n))")] bspec 1);
-by (Full_simp_tac 1);
+by (dres_inst_tac [("x","inverse (hypreal_of_real(real_of_posnat n))")]
+ bspec 1);
+by (full_simp_tac (simpset() addsimps [SReal_inverse]) 1);
by (rtac (real_of_posnat_gt_zero RS real_inverse_gt_zero RS
(hypreal_of_real_less_iff RS iffD1) RSN(2,impE)) 1);
by (assume_tac 2);
by (asm_full_simp_tac (simpset() addsimps
- [hypreal_of_real_inverse RS sym,
- rename_numerals real_of_posnat_gt_zero,hypreal_of_real_zero,
+ [rename_numerals real_of_posnat_gt_zero, hypreal_of_real_zero,
hypreal_of_real_of_posnat]) 1);
by (auto_tac (claset() addSDs [reals_Archimedean],
simpset() addsimps [SReal_iff,hypreal_of_real_zero RS sym]));
by (dtac (hypreal_of_real_less_iff RS iffD1) 1);
by (asm_full_simp_tac (simpset() addsimps
- [hypreal_of_real_inverse RS sym,
- rename_numerals real_of_posnat_gt_zero,hypreal_of_real_of_posnat])1);
+ [rename_numerals real_of_posnat_gt_zero,hypreal_of_real_of_posnat])1);
by (blast_tac (claset() addIs [hypreal_less_trans]) 1);
qed "lemma_Infinitesimal2";
Goalw [Infinitesimal_def]
- "Infinitesimal = {x. ALL n. abs x < inverse (hypreal_of_posnat n)}";
-by (auto_tac (claset(),simpset() addsimps [lemma_Infinitesimal2]));
+ "Infinitesimal = {x. ALL n. abs x < inverse (hypreal_of_posnat n)}";
+by (auto_tac (claset(), simpset() addsimps [lemma_Infinitesimal2]));
qed "Infinitesimal_hypreal_of_posnat_iff";
(*-----------------------------------------------------------------------------
--- a/src/HOL/Real/Hyperreal/SEQ.ML Thu Dec 21 16:52:10 2000 +0100
+++ b/src/HOL/Real/Hyperreal/SEQ.ML Thu Dec 21 18:08:10 2000 +0100
@@ -205,12 +205,12 @@
Goalw [NSLIMSEQ_def]
"[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b";
by (auto_tac (claset() addIs [inf_close_add],
- simpset() addsimps [starfunNat_add RS sym,hypreal_of_real_add]));
+ simpset() addsimps [starfunNat_add RS sym]));
qed "NSLIMSEQ_add";
Goal "[| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
- NSLIMSEQ_add]) 1);
+ NSLIMSEQ_add]) 1);
qed "LIMSEQ_add";
Goalw [NSLIMSEQ_def]
@@ -273,14 +273,9 @@
"[| X ----NS> a; a ~= #0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)";
by (Clarify_tac 1);
by (dtac bspec 1);
-by (auto_tac (claset(),
- simpset() addsimps [hypreal_of_real_not_zero_iff RS sym,
- hypreal_of_real_inverse RS sym]));
-by (forward_tac [inf_close_hypreal_of_real_not_zero] 1 THEN assume_tac 1);
-by (dtac hypreal_of_real_HFinite_diff_Infinitesimal 1);
-by (stac (starfunNat_inverse RS sym) 1);
-by (auto_tac (claset() addSEs [inf_close_inverse],
- simpset() addsimps [hypreal_of_real_zero_iff]));
+by (auto_tac (claset(),
+ simpset() addsimps [starfunNat_inverse RS sym,
+ hypreal_of_real_inf_close_inverse]));
qed "NSLIMSEQ_inverse";
@@ -1289,6 +1284,7 @@
(* We now use NS criterion to bring proof of theorem through *)
+
Goalw [NSLIMSEQ_def]
"[| #0 <= x; x < #1 |] ==> (%n. x ^ n) ----NS> #0";
by (auto_tac (claset() addSDs [convergent_realpow],
@@ -1305,7 +1301,8 @@
by (dtac inf_close_mult_subst_SReal 1 THEN assume_tac 1);
by (dtac inf_close_trans3 1 THEN assume_tac 1);
by (auto_tac (claset(),
- simpset() addsimps [hypreal_of_real_mult RS sym]));
+ simpset() delsimps [hypreal_of_real_mult]
+ addsimps [hypreal_of_real_mult RS sym]));
qed "NSLIMSEQ_realpow_zero";
(*--------------- standard version ---------------*)
--- a/src/HOL/Real/Hyperreal/Series.ML Thu Dec 21 16:52:10 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Series.ML Thu Dec 21 18:08:10 2000 +0100
@@ -313,12 +313,17 @@
Goalw [sums_def] "x sums x0 ==> (%n. c * x(n)) sums (c * x0)";
by (auto_tac (claset() addSIs [LIMSEQ_mult] addIs [LIMSEQ_const],
- simpset() addsimps [sumr_mult RS sym]));
+ simpset() addsimps [sumr_mult RS sym]));
qed "sums_mult";
-Goalw [sums_def] "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0 - y0)";
+Goal "x sums x' ==> (%n. x(n)/c) sums (x'/c)";
+by (asm_simp_tac (simpset() addsimps [real_divide_def, sums_mult,
+ inst "w" "inverse c" real_mult_commute]) 1);
+qed "sums_divide";
+
+Goalw [sums_def] "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0-y0)";
by (auto_tac (claset() addIs [LIMSEQ_diff],
- simpset() addsimps [sumr_diff RS sym]));
+ simpset() addsimps [sumr_diff RS sym]));
qed "sums_diff";
Goal "summable f ==> suminf f * c = suminf(%n. f n * c)";
@@ -415,7 +420,7 @@
sum of geometric progression
-------------------------------------------------------------------*)
-Goal "x ~= #1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - #1) * inverse(x - #1)";
+Goal "x ~= #1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - #1) / (x - #1)";
by (induct_tac "n" 1);
by (Auto_tac);
by (res_inst_tac [("c1","x - #1")] (real_mult_right_cancel RS iffD1) 1);
@@ -426,17 +431,18 @@
real_diff_def, real_mult_commute]));
qed "sumr_geometric";
-Goal "abs(x) < #1 ==> (%n. x ^ n) sums inverse(#1 - x)";
+Goal "abs(x) < #1 ==> (%n. x ^ n) sums (#1/(#1 - x))";
by (case_tac "x = #1" 1);
by (auto_tac (claset() addSDs [LIMSEQ_rabs_realpow_zero2],
- simpset() addsimps [sumr_geometric,abs_one,sums_def,
- real_diff_def,real_add_mult_distrib]));
-by (rtac (real_add_zero_left RS subst) 1);
-by (rtac (real_mult_0 RS subst) 1);
-by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_mult 1);
-by (auto_tac (claset() addIs [LIMSEQ_const], simpset() addsimps
- [real_minus_inverse RS sym,real_diff_def,real_add_commute,
- rename_numerals LIMSEQ_rabs_realpow_zero2]));
+ simpset() addsimps [sumr_geometric ,abs_one, sums_def,
+ real_diff_def, real_add_divide_distrib]));
+by (subgoal_tac "#1 / (#1 + - x) = #0/(x-#1) + - #1/(x-#1)" 1);
+by (asm_full_simp_tac (simpset() addsimps [real_divide_eq_cancel1,
+ real_divide_minus_eq RS sym, real_diff_def]) 2);
+by (etac ssubst 1);
+by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_divide 1);
+by (auto_tac (claset() addIs [LIMSEQ_const],
+ simpset() addsimps [real_diff_def, LIMSEQ_rabs_realpow_zero2]));
qed "geometric_sums";
(*-------------------------------------------------------------------
@@ -547,18 +553,6 @@
qed "rabs_ratiotest_lemma";
(* lemmas *)
-Goal "#0 < (r::real) ==> (x * r ^ n) * inverse (r ^ n) = x";
-by (auto_tac (claset(),simpset() addsimps
- [real_mult_assoc,rename_numerals realpow_not_zero]));
-val lemma_inverse_realpow = result();
-
-Goal "[| (c::real) ~= #0; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
-\ ==> ALL n. N <= n --> abs(f(Suc n)) <= (c * c ^ n)* (inverse(c ^ n)*abs(f n))";
-by (auto_tac (claset(),simpset() addsimps real_mult_ac));
-by (res_inst_tac [("z2.1","c ^ n")] (real_mult_left_commute RS subst) 1);
-by (auto_tac (claset(),simpset() addsimps [rename_numerals
- realpow_not_zero]));
-val lemma_inverse_realpow2 = result();
Goal "(k::nat) <= l ==> (EX n. l = k + n)";
by (dtac le_imp_less_or_eq 1);
@@ -569,29 +563,38 @@
by (auto_tac (claset(),simpset() addsimps [le_Suc_ex]));
qed "le_Suc_ex_iff";
-Goal "[| c < #1; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
-\ ==> summable f";
-by (subgoal_tac "c <= #0 | #0 < c" 1 THEN Auto_tac);
+(*All this trouble just to get #0<c *)
+Goal "[| ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
+\ ==> #0 < c | summable f";
+by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
by (asm_full_simp_tac (simpset() addsimps [summable_Cauchy]) 1);
by (Step_tac 1 THEN subgoal_tac "ALL n. N <= n --> f (Suc n) = #0" 1);
by (blast_tac (claset() addIs [rabs_ratiotest_lemma]) 2);
by (res_inst_tac [("x","Suc N")] exI 1 THEN Step_tac 1);
by (dtac Suc_le_imp_diff_ge2 1 THEN Auto_tac);
-by (res_inst_tac [("g","%n. (abs (f N)* inverse(c ^ N))*c ^ n")]
+qed "ratio_test_lemma2";
+
+
+Goal "[| c < #1; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
+\ ==> summable f";
+by (forward_tac [ratio_test_lemma2] 1);
+by Auto_tac;
+by (res_inst_tac [("g","%n. (abs (f N)/(c ^ N))*c ^ n")]
summable_comparison_test 1);
by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1);
by (dtac (le_Suc_ex_iff RS iffD1) 1);
by (auto_tac (claset(),simpset() addsimps [realpow_add,
- CLAIM_SIMP "(a * b) * (c * d) = (a * d) * (b * (c::real))" real_mult_ac,
rename_numerals realpow_not_zero]));
by (induct_tac "na" 1 THEN Auto_tac);
by (res_inst_tac [("j","c*abs(f(N + n))")] real_le_trans 1);
by (auto_tac (claset() addIs [real_mult_le_le_mono1],
- simpset() addsimps [summable_def, CLAIM_SIMP
- "a * (b * c) = b * (a * (c::real))" real_mult_ac]));
-by (res_inst_tac [("x","(abs(f N)*inverse(c ^ N))*inverse(#1 - c)")] exI 1);
-by (auto_tac (claset() addSIs [sums_mult,geometric_sums], simpset() addsimps
- [abs_eqI2]));
+ simpset() addsimps [summable_def]));
+by (asm_full_simp_tac (simpset() addsimps real_mult_ac) 1);
+by (res_inst_tac [("x","abs(f N) * (#1/(#1 - c)) / (c ^ N)")] exI 1);
+by (rtac sums_divide 1);
+by (rtac sums_mult 1);
+by (auto_tac (claset() addSIs [sums_mult,geometric_sums],
+ simpset() addsimps [real_abs_def]));
qed "ratio_test";
--- a/src/HOL/Real/Hyperreal/Star.ML Thu Dec 21 16:52:10 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Star.ML Thu Dec 21 18:08:10 2000 +0100
@@ -376,11 +376,7 @@
by (auto_tac (claset(),
simpset() addsimps [starfun, hypreal_inverse, hypreal_zero_def]));
qed "starfun_inverse_inverse";
-
-(* more specifically *)
-Goal "(*f* inverse) ehr = inverse (ehr)";
-by (rtac starfun_inverse_inverse 1);
-qed "starfun_inverse_epsilon";
+Addsimps [starfun_inverse_inverse];
Goal "inverse ((*f* f) x) = (*f* (%x. inverse (f x))) x";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
@@ -457,13 +453,14 @@
In this theory since hypreal_hrabs proved here. (To Check:) Maybe
move both if possible?
-------------------------------------------------------------------*)
-Goal "(x:Infinitesimal) = (EX X:Rep_hypreal(x). \
-\ ALL m. {n. abs(X n) < inverse(real_of_posnat m)}:FreeUltrafilterNat)";
+Goal "(x:Infinitesimal) = \
+\ (EX X:Rep_hypreal(x). \
+\ ALL m. {n. abs(X n) < inverse(real_of_posnat m)}:FreeUltrafilterNat)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl],
- simpset() addsimps [Infinitesimal_hypreal_of_posnat_iff,
- hypreal_of_real_of_posnat,hypreal_of_real_def,hypreal_inverse,
- hypreal_hrabs,hypreal_less]));
+ simpset() addsimps [Infinitesimal_hypreal_of_posnat_iff,
+ hypreal_of_real_of_posnat,hypreal_of_real_def,hypreal_inverse,
+ hypreal_hrabs,hypreal_less]));
by (dres_inst_tac [("x","n")] spec 1);
by (Fuf_tac 1);
qed "Infinitesimal_FreeUltrafilterNat_iff2";
@@ -473,8 +470,9 @@
\ inverse(real_of_posnat m)} : FreeUltrafilterNat)";
by (rtac (inf_close_minus_iff RS ssubst) 1);
by (rtac (mem_infmal_iff RS subst) 1);
-by (auto_tac (claset(), simpset() addsimps [hypreal_minus,
- hypreal_add,Infinitesimal_FreeUltrafilterNat_iff2]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_minus, hypreal_add,
+ Infinitesimal_FreeUltrafilterNat_iff2]));
by (dres_inst_tac [("x","m")] spec 1);
by (Fuf_tac 1);
qed "inf_close_FreeUltrafilterNat_iff";
--- a/src/HOL/Real/RealArith.ML Thu Dec 21 16:52:10 2000 +0100
+++ b/src/HOL/Real/RealArith.ML Thu Dec 21 18:08:10 2000 +0100
@@ -519,6 +519,11 @@
qed "real_divide_minus1";
Addsimps [real_divide_minus1];
+Goal "#-1/(x::real) = - (#1/x)";
+by (simp_tac (simpset() addsimps [real_divide_def, real_minus_inverse]) 1);
+qed "real_minus1_divide";
+Addsimps [real_minus1_divide];
+
Goal "[| (#0::real) < d1; #0 < d2 |] ==> EX e. #0 < e & e < d1 & e < d2";
by (res_inst_tac [("x","(min d1 d2)/#2")] exI 1);
by (asm_simp_tac (simpset() addsimps [min_def]) 1);