--- a/src/HOL/Hyperreal/Lim.ML Thu Nov 01 21:12:13 2001 +0100
+++ b/src/HOL/Hyperreal/Lim.ML Fri Nov 02 17:55:24 2001 +0100
@@ -65,16 +65,16 @@
(*----------------------------------------------
LIM_zero
----------------------------------------------*)
-Goal "f -- a --> l ==> (%x. f(x) + -l) -- a --> Numeral0";
-by (res_inst_tac [("z1","l")] (rename_numerals (real_add_minus RS subst)) 1);
+Goal "f -- a --> l ==> (%x. f(x) + -l) -- a --> 0";
+by (res_inst_tac [("z1","l")] ((real_add_minus RS subst)) 1);
by (rtac LIM_add_minus 1 THEN Auto_tac);
qed "LIM_zero";
(*--------------------------
Limit not zero
--------------------------*)
-Goalw [LIM_def] "k \\<noteq> Numeral0 ==> ~ ((%x. k) -- x --> Numeral0)";
-by (res_inst_tac [("R1.0","k"),("R2.0","Numeral0")] real_linear_less2 1);
+Goalw [LIM_def] "k \\<noteq> 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 [real_abs_def]));
by (res_inst_tac [("x","-k")] exI 1);
by (res_inst_tac [("x","k")] exI 2);
@@ -85,7 +85,7 @@
by Auto_tac;
qed "LIM_not_zero";
-(* [| k \\<noteq> Numeral0; (%x. k) -- x --> Numeral0 |] ==> R *)
+(* [| k \\<noteq> 0; (%x. k) -- x --> 0 |] ==> R *)
bind_thm("LIM_not_zeroE", LIM_not_zero RS notE);
Goal "(%x. k) -- x --> L ==> k = L";
@@ -108,9 +108,9 @@
LIM_mult_zero
-------------*)
Goalw [LIM_def]
- "[| f -- x --> Numeral0; g -- x --> Numeral0 |] ==> (%x. f(x)*g(x)) -- x --> Numeral0";
+ "[| f -- x --> 0; g -- x --> 0 |] ==> (%x. f(x)*g(x)) -- x --> 0";
by Safe_tac;
-by (dres_inst_tac [("x","Numeral1")] spec 1);
+by (dres_inst_tac [("x","1")] spec 1);
by (dres_inst_tac [("x","r")] spec 1);
by (cut_facts_tac [real_zero_less_one] 1);
by (asm_full_simp_tac (simpset() addsimps
@@ -146,7 +146,7 @@
by (auto_tac (claset(), simpset() addsimps [real_add_minus_iff]));
qed "LIM_equal";
-Goal "[| (%x. f(x) + -g(x)) -- a --> Numeral0; g -- a --> l |] \
+Goal "[| (%x. f(x) + -g(x)) -- a --> 0; g -- a --> l |] \
\ ==> f -- a --> l";
by (dtac LIM_add 1 THEN assume_tac 1);
by (auto_tac (claset(), simpset() addsimps [real_add_assoc]));
@@ -181,17 +181,17 @@
Limit: NS definition ==> standard definition
---------------------------------------------------------------------*)
-Goal "\\<forall>s. Numeral0 < s --> (\\<exists>xa. xa \\<noteq> x & \
+Goal "\\<forall>s. 0 < s --> (\\<exists>xa. xa \\<noteq> x & \
\ abs (xa + - x) < s & r \\<le> abs (f xa + -L)) \
\ ==> \\<forall>n::nat. \\<exists>xa. xa \\<noteq> x & \
\ abs(xa + -x) < inverse(real(Suc n)) & r \\<le> abs(f xa + -L)";
by (Clarify_tac 1);
by (cut_inst_tac [("n1","n")]
- (real_of_nat_Suc_gt_zero RS rename_numerals real_inverse_gt_zero) 1);
+ (real_of_nat_Suc_gt_zero RS real_inverse_gt_0) 1);
by Auto_tac;
val lemma_LIM = result();
-Goal "\\<forall>s. Numeral0 < s --> (\\<exists>xa. xa \\<noteq> x & \
+Goal "\\<forall>s. 0 < s --> (\\<exists>xa. xa \\<noteq> x & \
\ abs (xa + - x) < s & r \\<le> abs (f xa + -L)) \
\ ==> \\<exists>X. \\<forall>n::nat. X n \\<noteq> x & \
\ abs(X n + -x) < inverse(real(Suc n)) & r \\<le> abs(f (X n) + -L)";
@@ -320,7 +320,7 @@
NSLIM_inverse
-----------------------------*)
Goalw [NSLIM_def]
- "[| f -- a --NS> L; L \\<noteq> Numeral0 |] \
+ "[| f -- a --NS> L; L \\<noteq> 0 |] \
\ ==> (%x. inverse(f(x))) -- a --NS> (inverse L)";
by (Clarify_tac 1);
by (dtac spec 1);
@@ -329,28 +329,28 @@
qed "NSLIM_inverse";
Goal "[| f -- a --> L; \
-\ L \\<noteq> Numeral0 |] ==> (%x. inverse(f(x))) -- a --> (inverse L)";
+\ L \\<noteq> 0 |] ==> (%x. inverse(f(x))) -- a --> (inverse L)";
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> Numeral0";
-by (res_inst_tac [("z1","l")] (rename_numerals (real_add_minus RS subst)) 1);
+Goal "f -- a --NS> l ==> (%x. f(x) + -l) -- a --NS> 0";
+by (res_inst_tac [("z1","l")] ((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 --> Numeral0";
+Goal "f -- a --> l ==> (%x. f(x) + -l) -- a --> 0";
by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_zero]) 1);
qed "LIM_zero2";
-Goal "(%x. f(x) - l) -- x --NS> Numeral0 ==> f -- x --NS> l";
+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]));
qed "NSLIM_zero_cancel";
-Goal "(%x. f(x) - l) -- x --> Numeral0 ==> f -- x --> l";
+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]));
qed "LIM_zero_cancel";
@@ -359,17 +359,17 @@
(*--------------------------
NSLIM_not_zero
--------------------------*)
-Goalw [NSLIM_def] "k \\<noteq> Numeral0 ==> ~ ((%x. k) -- x --NS> Numeral0)";
+Goalw [NSLIM_def] "k \\<noteq> 0 ==> ~ ((%x. k) -- x --NS> 0)";
by Auto_tac;
by (res_inst_tac [("x","hypreal_of_real x + epsilon")] exI 1);
by (auto_tac (claset() addIs [Infinitesimal_add_approx_self RS approx_sym],
- simpset() addsimps [rename_numerals hypreal_epsilon_not_zero]));
+ simpset() addsimps [hypreal_epsilon_not_zero]));
qed "NSLIM_not_zero";
-(* [| k \\<noteq> Numeral0; (%x. k) -- x --NS> Numeral0 |] ==> R *)
+(* [| k \\<noteq> 0; (%x. k) -- x --NS> 0 |] ==> R *)
bind_thm("NSLIM_not_zeroE", NSLIM_not_zero RS notE);
-Goal "k \\<noteq> Numeral0 ==> ~ ((%x. k) -- x --> Numeral0)";
+Goal "k \\<noteq> 0 ==> ~ ((%x. k) -- x --> 0)";
by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_not_zero]) 1);
qed "LIM_not_zero2";
@@ -405,16 +405,16 @@
(*--------------------
NSLIM_mult_zero
--------------------*)
-Goal "[| f -- x --NS> Numeral0; g -- x --NS> Numeral0 |] \
-\ ==> (%x. f(x)*g(x)) -- x --NS> Numeral0";
+Goal "[| f -- x --NS> 0; g -- x --NS> 0 |] \
+\ ==> (%x. f(x)*g(x)) -- x --NS> 0";
by (dtac NSLIM_mult 1 THEN Auto_tac);
qed "NSLIM_mult_zero";
(* we can use the corresponding thm LIM_mult2 *)
(* for standard definition of limit *)
-Goal "[| f -- x --> Numeral0; g -- x --> Numeral0 |] \
-\ ==> (%x. f(x)*g(x)) -- x --> Numeral0";
+Goal "[| f -- x --> 0; g -- x --> 0 |] \
+\ ==> (%x. f(x)*g(x)) -- x --> 0";
by (dtac LIM_mult2 1 THEN Auto_tac);
qed "LIM_mult_zero2";
@@ -499,8 +499,8 @@
--------------------------------------------------------------------------*)
(* Prove equivalence between NS limits - *)
(* seems easier than using standard def *)
-Goalw [NSLIM_def] "(f -- a --NS> L) = ((%h. f(a + h)) -- Numeral0 --NS> L)";
-by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_zero]));
+Goalw [NSLIM_def] "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)";
+by Auto_tac;
by (dres_inst_tac [("x","hypreal_of_real a + x")] spec 1);
by (dres_inst_tac [("x","-hypreal_of_real a + x")] spec 2);
by Safe_tac;
@@ -516,15 +516,15 @@
hypreal_add, real_add_assoc, approx_refl, hypreal_zero_def]));
qed "NSLIM_h_iff";
-Goal "(f -- a --NS> f a) = ((%h. f(a + h)) -- Numeral0 --NS> f a)";
+Goal "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)";
by (rtac NSLIM_h_iff 1);
qed "NSLIM_isCont_iff";
-Goal "(f -- a --> f a) = ((%h. f(a + h)) -- Numeral0 --> f(a))";
+Goal "(f -- a --> f a) = ((%h. f(a + h)) -- 0 --> f(a))";
by (simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_isCont_iff]) 1);
qed "LIM_isCont_iff";
-Goalw [isCont_def] "(isCont f x) = ((%h. f(x + h)) -- Numeral0 --> f(x))";
+Goalw [isCont_def] "(isCont f x) = ((%h. f(x + h)) -- 0 --> f(x))";
by (simp_tac (simpset() addsimps [LIM_isCont_iff]) 1);
qed "isCont_iff";
@@ -574,11 +574,11 @@
qed "isCont_minus";
Goalw [isCont_def]
- "[| isCont f x; f x \\<noteq> Numeral0 |] ==> isCont (%x. inverse (f x)) x";
+ "[| isCont f x; f x \\<noteq> 0 |] ==> isCont (%x. inverse (f x)) x";
by (blast_tac (claset() addIs [LIM_inverse]) 1);
qed "isCont_inverse";
-Goal "[| isNSCont f x; f x \\<noteq> Numeral0 |] ==> isNSCont (%x. inverse (f x)) x";
+Goal "[| isNSCont f x; f x \\<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x";
by (auto_tac (claset() addIs [isCont_inverse],simpset() addsimps
[isNSCont_isCont_iff]));
qed "isNSCont_inverse";
@@ -667,8 +667,10 @@
qed "isNSUContD";
Goalw [isUCont_def,isCont_def,LIM_def]
- "isUCont f ==> \\<exists>x. isCont f x";
-by (Force_tac 1);
+ "isUCont f ==> isCont f x";
+by (Clarify_tac 1);
+by (dtac spec 1);
+by (Blast_tac 1);
qed "isUCont_isCont";
Goalw [isNSUCont_def,isUCont_def,approx_def]
@@ -690,17 +692,17 @@
by (Ultra_tac 1);
qed "isUCont_isNSUCont";
-Goal "\\<forall>s. Numeral0 < s --> (\\<exists>z y. abs (z + - y) < s & r \\<le> abs (f z + -f y)) \
+Goal "\\<forall>s. 0 < s --> (\\<exists>z y. abs (z + - y) < s & r \\<le> abs (f z + -f y)) \
\ ==> \\<forall>n::nat. \\<exists>z y. \
\ abs(z + -y) < inverse(real(Suc n)) & \
\ r \\<le> abs(f z + -f y)";
by (Clarify_tac 1);
by (cut_inst_tac [("n1","n")]
- (real_of_nat_Suc_gt_zero RS rename_numerals real_inverse_gt_zero) 1);
+ (real_of_nat_Suc_gt_zero RS real_inverse_gt_0) 1);
by Auto_tac;
val lemma_LIMu = result();
-Goal "\\<forall>s. Numeral0 < s --> (\\<exists>z y. abs (z + - y) < s & r \\<le> abs (f z + -f y)) \
+Goal "\\<forall>s. 0 < s --> (\\<exists>z y. abs (z + - y) < s & r \\<le> abs (f z + -f y)) \
\ ==> \\<exists>X Y. \\<forall>n::nat. \
\ abs(X n + -(Y n)) < inverse(real(Suc n)) & \
\ r \\<le> abs(f (X n) + -f (Y n))";
@@ -745,23 +747,23 @@
Derivatives
------------------------------------------------------------------*)
Goalw [deriv_def]
- "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- Numeral0 --> D)";
+ "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --> D)";
by (Blast_tac 1);
qed "DERIV_iff";
Goalw [deriv_def]
- "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- Numeral0 --NS> D)";
+ "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --NS> D)";
by (simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1);
qed "DERIV_NS_iff";
Goalw [deriv_def]
"DERIV f x :> D \
-\ ==> (%h. (f(x + h) + - f(x))/h) -- Numeral0 --> D";
+\ ==> (%h. (f(x + h) + - f(x))/h) -- 0 --> D";
by (Blast_tac 1);
qed "DERIVD";
Goalw [deriv_def] "DERIV f x :> D ==> \
-\ (%h. (f(x + h) + - f(x))/h) -- Numeral0 --NS> D";
+\ (%h. (f(x + h) + - f(x))/h) -- 0 --NS> D";
by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1);
qed "NS_DERIVD";
@@ -809,7 +811,7 @@
-------------------------------------------------------*)
Goalw [LIM_def]
- "((%h. (f(a + h) + - f(a))/h) -- Numeral0 --> D) = \
+ "((%h. (f(a + h) + - f(a))/h) -- 0 --> D) = \
\ ((%x. (f(x) + -f(a)) / (x + -a)) -- a --> D)";
by Safe_tac;
by (ALLGOALS(dtac spec));
@@ -836,8 +838,8 @@
(*--- first equivalence ---*)
Goalw [nsderiv_def,NSLIM_def]
- "(NSDERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- Numeral0 --NS> D)";
-by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_zero]));
+ "(NSDERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --NS> D)";
+by Auto_tac;
by (dres_inst_tac [("x","xa")] bspec 1);
by (rtac ccontr 3);
by (dres_inst_tac [("x","h")] spec 3);
@@ -868,8 +870,7 @@
\ (*f* (%z. f z - f x)) u \\<approx> hypreal_of_real D * (u - hypreal_of_real x))";
by (auto_tac (claset(), simpset() addsimps [NSDERIV_iff2]));
by (case_tac "u = hypreal_of_real x" 1);
-by (auto_tac (claset(),
- simpset() addsimps [hypreal_diff_def, hypreal_of_real_zero]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_diff_def]));
by (dres_inst_tac [("x","u")] spec 1);
by Auto_tac;
by (dres_inst_tac [("c","u - hypreal_of_real x"),("b","hypreal_of_real D")]
@@ -956,12 +957,12 @@
------------------------*)
(* use simple constant nslimit theorem *)
-Goal "(NSDERIV (%x. k) x :> Numeral0)";
+Goal "(NSDERIV (%x. k) x :> 0)";
by (simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff]) 1);
qed "NSDERIV_const";
Addsimps [NSDERIV_const];
-Goal "(DERIV (%x. k) x :> Numeral0)";
+Goal "(DERIV (%x. k) x :> 0)";
by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff RS sym]) 1);
qed "DERIV_const";
Addsimps [DERIV_const];
@@ -1000,7 +1001,7 @@
Goal "[| (x + y) / z = hypreal_of_real D + yb; z \\<noteq> 0; \
\ z \\<in> Infinitesimal; yb \\<in> Infinitesimal |] \
-\ ==> x + y \\<approx> Numeral0";
+\ ==> x + y \\<approx> 0";
by (forw_inst_tac [("c1","z")] (hypreal_mult_right_cancel RS iffD2) 1
THEN assume_tac 1);
by (thin_tac "(x + y) / z = hypreal_of_real D + yb" 1);
@@ -1015,8 +1016,7 @@
by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def]) 1);
by (REPEAT (Step_tac 1));
by (auto_tac (claset(),
- simpset() addsimps [starfun_lambda_cancel, hypreal_of_real_zero,
- lemma_nsderiv1]));
+ simpset() addsimps [starfun_lambda_cancel, lemma_nsderiv1]));
by (simp_tac (simpset() addsimps [hypreal_add_divide_distrib]) 1);
by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1));
by (auto_tac (claset(),
@@ -1127,13 +1127,13 @@
qed "incrementI2";
(* The Increment theorem -- Keisler p. 65 *)
-Goal "[| NSDERIV f x :> D; h \\<in> Infinitesimal; h \\<noteq> Numeral0 |] \
+Goal "[| NSDERIV f x :> D; h \\<in> Infinitesimal; h \\<noteq> 0 |] \
\ ==> \\<exists>e \\<in> Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h";
by (forw_inst_tac [("h","h")] incrementI2 1 THEN rewtac nsderiv_def);
by (dtac bspec 1 THEN Auto_tac);
by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1 THEN Step_tac 1);
by (forw_inst_tac [("b1","hypreal_of_real(D) + y")]
- (rename_numerals (hypreal_mult_right_cancel RS iffD2)) 1);
+ ((hypreal_mult_right_cancel RS iffD2)) 1);
by (thin_tac "((*f* f) (hypreal_of_real(x) + h) + \
\ - hypreal_of_real (f x)) / h = hypreal_of_real(D) + y" 2);
by (assume_tac 1);
@@ -1143,15 +1143,15 @@
simpset() addsimps [hypreal_add_mult_distrib]));
qed "increment_thm";
-Goal "[| NSDERIV f x :> D; h \\<approx> Numeral0; h \\<noteq> Numeral0 |] \
+Goal "[| NSDERIV f x :> D; h \\<approx> 0; h \\<noteq> 0 |] \
\ ==> \\<exists>e \\<in> Infinitesimal. increment f x h = \
\ hypreal_of_real(D)*h + e*h";
by (blast_tac (claset() addSDs [mem_infmal_iff RS iffD2]
addSIs [increment_thm]) 1);
qed "increment_thm2";
-Goal "[| NSDERIV f x :> D; h \\<approx> Numeral0; h \\<noteq> Numeral0 |] \
-\ ==> increment f x h \\<approx> Numeral0";
+Goal "[| NSDERIV f x :> D; h \\<approx> 0; h \\<noteq> 0 |] \
+\ ==> increment f x h \\<approx> 0";
by (dtac increment_thm2 1 THEN auto_tac (claset() addSIs
[Infinitesimal_HFinite_mult2,HFinite_add],simpset() addsimps
[hypreal_add_mult_distrib RS sym,mem_infmal_iff RS sym]));
@@ -1172,16 +1172,16 @@
"[| NSDERIV g x :> D; \
\ (*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);\
\ xa \\<in> Infinitesimal;\
-\ xa \\<noteq> Numeral0 \
-\ |] ==> D = Numeral0";
+\ xa \\<noteq> 0 \
+\ |] ==> D = 0";
by (dtac bspec 1);
by Auto_tac;
qed "NSDERIV_zero";
(* can be proved differently using NSLIM_isCont_iff *)
Goalw [nsderiv_def]
- "[| NSDERIV f x :> D; h \\<in> Infinitesimal; h \\<noteq> Numeral0 |] \
-\ ==> (*f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\<approx> Numeral0";
+ "[| NSDERIV f x :> D; h \\<in> Infinitesimal; h \\<noteq> 0 |] \
+\ ==> (*f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\<approx> 0";
by (asm_full_simp_tac (simpset() addsimps
[mem_infmal_iff RS sym]) 1);
by (rtac Infinitesimal_ratio 1);
@@ -1214,12 +1214,12 @@
----------------- \\<approx> Db
h
--------------------------------------------------------------*)
-Goal "[| NSDERIV g x :> Db; xa \\<in> Infinitesimal; xa \\<noteq> Numeral0 |] \
+Goal "[| NSDERIV g x :> Db; xa \\<in> Infinitesimal; xa \\<noteq> 0 |] \
\ ==> ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa \
\ \\<approx> hypreal_of_real(Db)";
by (auto_tac (claset(),
simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def,
- hypreal_of_real_zero, mem_infmal_iff, starfun_lambda_cancel]));
+ mem_infmal_iff, starfun_lambda_cancel]));
qed "NSDERIVD2";
Goal "(z::hypreal) \\<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)";
@@ -1232,14 +1232,13 @@
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);
+ NSLIM_def,mem_infmal_iff RS sym]) 1 THEN Step_tac 1);
by (forw_inst_tac [("f","g")] NSDERIV_approx 1);
by (auto_tac (claset(),
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(),
- simpset() addsimps [hypreal_divide_def, hypreal_of_real_zero]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_divide_def]));
by (res_inst_tac [("z1","(*f* g) (hypreal_of_real(x) + xa) + -hypreal_of_real (g x)"),
("y1","inverse xa")] (lemma_chain RS ssubst) 1);
by (etac (hypreal_not_eq_minus_iff RS iffD1) 1);
@@ -1266,16 +1265,14 @@
(*------------------------------------------------------------------
Differentiation of natural number powers
------------------------------------------------------------------*)
-Goal "NSDERIV (%x. x) x :> Numeral1";
+Goal "NSDERIV (%x. x) x :> 1";
by (auto_tac (claset(),
- simpset() addsimps [NSDERIV_NSLIM_iff,
- NSLIM_def ,starfun_Id, hypreal_of_real_zero,
- hypreal_of_real_one]));
+ simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def ,starfun_Id]));
qed "NSDERIV_Id";
Addsimps [NSDERIV_Id];
(*derivative of the identity function*)
-Goal "DERIV (%x. x) x :> Numeral1";
+Goal "DERIV (%x. x) x :> 1";
by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff RS sym]) 1);
qed "DERIV_Id";
Addsimps [DERIV_Id];
@@ -1314,9 +1311,9 @@
Power of -1
---------------------------------------------------------------*)
-(*Can't get rid of x \\<noteq> Numeral0 because it isn't continuous at zero*)
+(*Can't get rid of x \\<noteq> 0 because it isn't continuous at zero*)
Goalw [nsderiv_def]
- "x \\<noteq> Numeral0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))";
+ "x \\<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))";
by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1);
by (forward_tac [Infinitesimal_add_not_zero] 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 2);
@@ -1345,7 +1342,7 @@
qed "NSDERIV_inverse";
-Goal "x \\<noteq> Numeral0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))";
+Goal "x \\<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))";
by (asm_simp_tac (simpset() addsimps [NSDERIV_inverse,
NSDERIV_DERIV_iff RS sym] delsimps [realpow_Suc]) 1);
qed "DERIV_inverse";
@@ -1353,7 +1350,7 @@
(*--------------------------------------------------------------
Derivative of inverse
-------------------------------------------------------------*)
-Goal "[| DERIV f x :> d; f(x) \\<noteq> Numeral0 |] \
+Goal "[| DERIV f x :> d; f(x) \\<noteq> 0 |] \
\ ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))";
by (rtac (real_mult_commute RS subst) 1);
by (asm_simp_tac (simpset() addsimps [real_minus_mult_eq1,
@@ -1363,7 +1360,7 @@
by (blast_tac (claset() addSIs [DERIV_chain,DERIV_inverse]) 1);
qed "DERIV_inverse_fun";
-Goal "[| NSDERIV f x :> d; f(x) \\<noteq> Numeral0 |] \
+Goal "[| NSDERIV f x :> d; f(x) \\<noteq> 0 |] \
\ ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))";
by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff,
DERIV_inverse_fun] delsimps [realpow_Suc]) 1);
@@ -1372,7 +1369,7 @@
(*--------------------------------------------------------------
Derivative of quotient
-------------------------------------------------------------*)
-Goal "[| DERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> Numeral0 |] \
+Goal "[| DERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> 0 |] \
\ ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) + -(e*f(x))) / (g(x) ^ Suc (Suc 0))";
by (dres_inst_tac [("f","g")] DERIV_inverse_fun 1);
by (dtac DERIV_mult 2);
@@ -1384,7 +1381,7 @@
real_minus_mult_eq2 RS sym]) 1);
qed "DERIV_quotient";
-Goal "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> Numeral0 |] \
+Goal "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> 0 |] \
\ ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) \
\ + -(e*f(x))) / (g(x) ^ Suc (Suc 0))";
by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff,
@@ -1401,7 +1398,7 @@
by (res_inst_tac
[("x","%z. if z = x then l else (f(z) - f(x)) / (z - x)")] exI 1);
by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,
- ARITH_PROVE "z \\<noteq> x ==> z - x \\<noteq> (Numeral0::real)"]));
+ ARITH_PROVE "z \\<noteq> x ==> z - x \\<noteq> (0::real)"]));
by (auto_tac (claset(),simpset() addsimps [isCont_iff,DERIV_iff]));
by (ALLGOALS(rtac (LIM_equal RS iffD1)));
by (auto_tac (claset(),simpset() addsimps [real_diff_def,real_mult_assoc]));
@@ -1466,7 +1463,7 @@
by (dtac real_less_sum_gt_zero 1);
by (dres_inst_tac [("x","f n + - lim f")] spec 1);
by Safe_tac;
-by (dres_inst_tac [("P","%na. no\\<le>na --> ?Q na"),("x","no + n")] spec 2);
+by (dres_inst_tac [("P","%na. no\\<le>na --> ?Q na"),("x","no + n")] spec 1);
by Auto_tac;
by (subgoal_tac "lim f \\<le> f(no + n)" 1);
by (induct_tac "no" 2);
@@ -1511,7 +1508,7 @@
Goal "[| \\<forall>n. f(n) \\<le> f(Suc n); \
\ \\<forall>n. g(Suc n) \\<le> g(n); \
\ \\<forall>n. f(n) \\<le> g(n); \
-\ (%n. f(n) - g(n)) ----> Numeral0 |] \
+\ (%n. f(n) - g(n)) ----> 0 |] \
\ ==> \\<exists>l. ((\\<forall>n. f(n) \\<le> l) & f ----> l) & \
\ ((\\<forall>n. l \\<le> g(n)) & g ----> l)";
by (dtac lemma_nest 1 THEN Auto_tac);
@@ -1546,7 +1543,7 @@
Goal "((x::real) = y / (2 * z)) = (2 * x = y/z)";
by Auto_tac;
-by (dres_inst_tac [("f","%u. (Numeral1/2)*u")] arg_cong 1);
+by (dres_inst_tac [("f","%u. (1/2)*u")] arg_cong 1);
by Auto_tac;
qed "eq_divide_2_times_iff";
@@ -1589,7 +1586,7 @@
Goal "[| \\<forall>a b c. P(a,b) & P(b,c) & a \\<le> b & b \\<le> c --> P(a,c); \
-\ \\<forall>x. \\<exists>d::real. Numeral0 < d & \
+\ \\<forall>x. \\<exists>d::real. 0 < d & \
\ (\\<forall>a b. a \\<le> x & x \\<le> b & (b - a) < d --> P(a,b)); \
\ a \\<le> b |] \
\ ==> P(a,b)";
@@ -1604,8 +1601,8 @@
by (rename_tac "l" 1);
by (dres_inst_tac [("x","l")] spec 1 THEN Clarify_tac 1);
by (rewtac LIMSEQ_def);
-by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/2")] spec 1);
-by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/2")] spec 1);
+by (dres_inst_tac [("P", "%r. 0<r --> ?Q r"), ("x","d/2")] spec 1);
+by (dres_inst_tac [("P", "%r. 0<r --> ?Q r"), ("x","d/2")] spec 1);
by (dtac real_less_half_sum 1);
by Safe_tac;
(*linear arithmetic bug if we just use Asm_simp_tac*)
@@ -1626,7 +1623,7 @@
Goal "((\\<forall>a b c. (a \\<le> b & b \\<le> c & P(a,b) & P(b,c)) --> P(a,c)) & \
-\ (\\<forall>x. \\<exists>d::real. Numeral0 < d & \
+\ (\\<forall>x. \\<exists>d::real. 0 < d & \
\ (\\<forall>a b. a \\<le> x & x \\<le> b & (b - a) < d --> P(a,b)))) \
\ --> (\\<forall>a b. a \\<le> b --> P(a,b))";
by (Clarify_tac 1);
@@ -1654,14 +1651,14 @@
by (rtac ccontr 1);
by (subgoal_tac "a \\<le> x & x \\<le> b" 1);
by (Asm_full_simp_tac 2);
-by (dres_inst_tac [("P", "%d. Numeral0<d --> ?P d"),("x","Numeral1")] spec 2);
+by (dres_inst_tac [("P", "%d. 0<d --> ?P d"),("x","1")] spec 2);
by (Step_tac 2);
by (Asm_full_simp_tac 2);
by (Asm_full_simp_tac 2);
by (REPEAT(blast_tac (claset() addIs [order_trans]) 2));
by (REPEAT(dres_inst_tac [("x","x")] spec 1));
by (Asm_full_simp_tac 1);
-by (dres_inst_tac [("P", "%r. ?P r --> (\\<exists>s. Numeral0<s & ?Q r s)"),
+by (dres_inst_tac [("P", "%r. ?P r --> (\\<exists>s. 0<s & ?Q r s)"),
("x","abs(y - f x)")] spec 1);
by Safe_tac;
by (asm_full_simp_tac (simpset() addsimps []) 1);
@@ -1738,15 +1735,15 @@
by (cut_inst_tac [("x","xb"),("y","xa")] linorder_linear 1);
by (Force_tac 1);
by (case_tac "a \\<le> x & x \\<le> b" 1);
-by (res_inst_tac [("x","Numeral1")] exI 2);
+by (res_inst_tac [("x","1")] exI 2);
by (Force_tac 2);
by (asm_full_simp_tac (simpset() addsimps [LIM_def,isCont_iff]) 1);
by (dres_inst_tac [("x","x")] spec 1 THEN Auto_tac);
by (thin_tac "\\<forall>M. \\<exists>x. a \\<le> x & x \\<le> b & ~ f x \\<le> M" 1);
-by (dres_inst_tac [("x","Numeral1")] spec 1);
+by (dres_inst_tac [("x","1")] spec 1);
by Auto_tac;
by (res_inst_tac [("x","s")] exI 1 THEN Clarify_tac 1);
-by (res_inst_tac [("x","abs(f x) + Numeral1")] exI 1 THEN Clarify_tac 1);
+by (res_inst_tac [("x","abs(f x) + 1")] exI 1 THEN Clarify_tac 1);
by (dres_inst_tac [("x","xa - x")] spec 1 THEN Safe_tac);
by (arith_tac 1);
by (arith_tac 1);
@@ -1803,23 +1800,23 @@
"\\<exists>k. \\<forall>x. a \\<le> x & x \\<le> b --> (%x. inverse(M - (f x))) x \\<le> k" 1);
by (rtac isCont_bounded 2);
by Safe_tac;
-by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> Numeral0 < inverse(M - f(x))" 1);
+by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> 0 < inverse(M - f(x))" 1);
by (Asm_full_simp_tac 1);
by Safe_tac;
by (asm_full_simp_tac (simpset() addsimps [real_less_diff_eq]) 2);
by (subgoal_tac
- "\\<forall>x. a \\<le> x & x \\<le> b --> (%x. inverse(M - (f x))) x < (k + Numeral1)" 1);
+ "\\<forall>x. a \\<le> x & x \\<le> b --> (%x. inverse(M - (f x))) x < (k + 1)" 1);
by Safe_tac;
by (res_inst_tac [("y","k")] order_le_less_trans 2);
by (asm_full_simp_tac (simpset() addsimps [real_zero_less_one]) 3);
by (Asm_full_simp_tac 2);
by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> \
-\ inverse(k + Numeral1) < inverse((%x. inverse(M - (f x))) x)" 1);
+\ inverse(k + 1) < inverse((%x. inverse(M - (f x))) x)" 1);
by Safe_tac;
by (rtac real_inverse_less_swap 2);
by (ALLGOALS Asm_full_simp_tac);
by (dres_inst_tac [("P", "%N. N<M --> ?Q N"),
- ("x","M - inverse(k + Numeral1)")] spec 1);
+ ("x","M - inverse(k + 1)")] spec 1);
by (Step_tac 1 THEN dtac real_leI 1);
by (dtac (real_le_diff_eq RS iffD1) 1);
by (REPEAT(dres_inst_tac [("x","a")] spec 1));
@@ -1879,11 +1876,11 @@
(*----------------------------------------------------------------------------*)
Goalw [deriv_def,LIM_def]
- "[| DERIV f x :> l; Numeral0 < l |] ==> \
-\ \\<exists>d. Numeral0 < d & (\\<forall>h. Numeral0 < h & h < d --> f(x) < f(x + h))";
+ "[| DERIV f x :> l; 0 < l |] \
+\ ==> \\<exists>d. 0 < d & (\\<forall>h. 0 < h & h < d --> f(x) < f(x + h))";
by (dtac spec 1 THEN Auto_tac);
by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac);
-by (subgoal_tac "Numeral0 < l*h" 1);
+by (subgoal_tac "0 < l*h" 1);
by (asm_full_simp_tac (simpset() addsimps [real_0_less_mult_iff]) 2);
by (dres_inst_tac [("x","h")] spec 1);
by (asm_full_simp_tac
@@ -1893,11 +1890,11 @@
qed "DERIV_left_inc";
Goalw [deriv_def,LIM_def]
- "[| DERIV f x :> l; l < Numeral0 |] ==> \
-\ \\<exists>d. Numeral0 < d & (\\<forall>h. Numeral0 < h & h < d --> f(x) < f(x - h))";
+ "[| DERIV f x :> l; l < 0 |] ==> \
+\ \\<exists>d. 0 < d & (\\<forall>h. 0 < h & h < d --> f(x) < f(x - h))";
by (dres_inst_tac [("x","-l")] spec 1 THEN Auto_tac);
by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac);
-by (subgoal_tac "l*h < Numeral0" 1);
+by (subgoal_tac "l*h < 0" 1);
by (asm_full_simp_tac (simpset() addsimps [real_mult_less_0_iff]) 2);
by (dres_inst_tac [("x","-h")] spec 1);
by (asm_full_simp_tac
@@ -1905,7 +1902,7 @@
pos_real_less_divide_eq,
symmetric real_diff_def]
addsplits [split_if_asm]) 1);
-by (subgoal_tac "Numeral0 < (f (x - h) - f x)/h" 1);
+by (subgoal_tac "0 < (f (x - h) - f x)/h" 1);
by (arith_tac 2);
by (asm_full_simp_tac
(simpset() addsimps [pos_real_less_divide_eq]) 1);
@@ -1913,9 +1910,9 @@
Goal "[| DERIV f x :> l; \
-\ \\<exists>d. Numeral0 < d & (\\<forall>y. abs(x - y) < d --> f(y) \\<le> f(x)) |] \
-\ ==> l = Numeral0";
-by (res_inst_tac [("R1.0","l"),("R2.0","Numeral0")] real_linear_less2 1);
+\ \\<exists>d. 0 < d & (\\<forall>y. abs(x - y) < d --> f(y) \\<le> f(x)) |] \
+\ ==> l = 0";
+by (res_inst_tac [("R1.0","l"),("R2.0","0")] real_linear_less2 1);
by Safe_tac;
by (dtac DERIV_left_dec 1);
by (dtac DERIV_left_inc 3);
@@ -1933,8 +1930,8 @@
(*----------------------------------------------------------------------------*)
Goal "[| DERIV f x :> l; \
-\ \\<exists>d::real. Numeral0 < d & (\\<forall>y. abs(x - y) < d --> f(x) \\<le> f(y)) |] \
-\ ==> l = Numeral0";
+\ \\<exists>d::real. 0 < d & (\\<forall>y. abs(x - y) < d --> f(x) \\<le> f(y)) |] \
+\ ==> l = 0";
by (dtac (DERIV_minus RS DERIV_local_max) 1);
by Auto_tac;
qed "DERIV_local_min";
@@ -1944,8 +1941,8 @@
(*----------------------------------------------------------------------------*)
Goal "[| DERIV f x :> l; \
-\ \\<exists>d. Numeral0 < d & (\\<forall>y. abs(x - y) < d --> f(x) = f(y)) |] \
-\ ==> l = Numeral0";
+\ \\<exists>d. 0 < d & (\\<forall>y. abs(x - y) < d --> f(x) = f(y)) |] \
+\ ==> l = 0";
by (auto_tac (claset() addSDs [DERIV_local_max],simpset()));
qed "DERIV_local_const";
@@ -1954,7 +1951,7 @@
(*----------------------------------------------------------------------------*)
Goal "[| a < x; x < b |] ==> \
-\ \\<exists>d::real. Numeral0 < d & (\\<forall>y. abs(x - y) < d --> a < y & y < b)";
+\ \\<exists>d::real. 0 < d & (\\<forall>y. abs(x - y) < d --> a < y & y < b)";
by (simp_tac (simpset() addsimps [abs_interval_iff]) 1);
by (cut_inst_tac [("x","x - a"),("y","b - x")] linorder_linear 1);
by Safe_tac;
@@ -1965,7 +1962,7 @@
qed "lemma_interval_lt";
Goal "[| a < x; x < b |] ==> \
-\ \\<exists>d::real. Numeral0 < d & (\\<forall>y. abs(x - y) < d --> a \\<le> y & y \\<le> b)";
+\ \\<exists>d::real. 0 < d & (\\<forall>y. abs(x - y) < d --> a \\<le> y & y \\<le> b)";
by (dtac lemma_interval_lt 1);
by Auto_tac;
by (auto_tac (claset() addSIs [exI] ,simpset()));
@@ -1975,13 +1972,13 @@
Rolle's Theorem
If f is defined and continuous on the finite closed interval [a,b]
and differentiable a least on the open interval (a,b), and f(a) = f(b),
- then x0 \\<in> (a,b) such that f'(x0) = Numeral0
+ then x0 \\<in> (a,b) such that f'(x0) = 0
----------------------------------------------------------------------*)
Goal "[| a < b; f(a) = f(b); \
\ \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \
\ \\<forall>x. a < x & x < b --> f differentiable x \
-\ |] ==> \\<exists>z. a < z & z < b & DERIV f z :> Numeral0";
+\ |] ==> \\<exists>z. a < z & z < b & DERIV f z :> 0";
by (ftac (order_less_imp_le RS isCont_eq_Ub) 1);
by (EVERY1[assume_tac,Step_tac]);
by (ftac (order_less_imp_le RS isCont_eq_Lb) 1);
@@ -1992,7 +1989,7 @@
by (EVERY1[assume_tac,etac exE]);
by (res_inst_tac [("x","x")] exI 1 THEN Asm_full_simp_tac 1);
by (subgoal_tac "(\\<exists>l. DERIV f x :> l) & \
-\ (\\<exists>d. Numeral0 < d & (\\<forall>y. abs(x - y) < d --> f(y) \\<le> f(x)))" 1);
+\ (\\<exists>d. 0 < d & (\\<forall>y. abs(x - y) < d --> f(y) \\<le> f(x)))" 1);
by (Clarify_tac 1 THEN rtac conjI 2);
by (blast_tac (claset() addIs [differentiableD]) 2);
by (Blast_tac 2);
@@ -2004,7 +2001,7 @@
by (EVERY1[assume_tac,etac exE]);
by (res_inst_tac [("x","xa")] exI 1 THEN Asm_full_simp_tac 1);
by (subgoal_tac "(\\<exists>l. DERIV f xa :> l) & \
-\ (\\<exists>d. Numeral0 < d & (\\<forall>y. abs(xa - y) < d --> f(xa) \\<le> f(y)))" 1);
+\ (\\<exists>d. 0 < d & (\\<forall>y. abs(xa - y) < d --> f(xa) \\<le> f(y)))" 1);
by (Clarify_tac 1 THEN rtac conjI 2);
by (blast_tac (claset() addIs [differentiableD]) 2);
by (Blast_tac 2);
@@ -2030,7 +2027,7 @@
by (forw_inst_tac [("a","a"),("x","r")] lemma_interval 1);
by (EVERY1[assume_tac, etac exE]);
by (subgoal_tac "(\\<exists>l. DERIV f r :> l) & \
-\ (\\<exists>d. Numeral0 < d & (\\<forall>y. abs(r - y) < d --> f(r) = f(y)))" 1);
+\ (\\<exists>d. 0 < d & (\\<forall>y. abs(r - y) < d --> f(r) = f(y)))" 1);
by (Clarify_tac 1 THEN rtac conjI 2);
by (blast_tac (claset() addIs [differentiableD]) 2);
by (EVERY1[ftac DERIV_local_const, Blast_tac, Blast_tac]);
@@ -2098,7 +2095,7 @@
Goal "[| a < b; \
\ \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \
-\ \\<forall>x. a < x & x < b --> DERIV f x :> Numeral0 |] \
+\ \\<forall>x. a < x & x < b --> DERIV f x :> 0 |] \
\ ==> (f b = f a)";
by (dtac MVT 1 THEN assume_tac 1);
by (blast_tac (claset() addIs [differentiableI]) 1);
@@ -2108,7 +2105,7 @@
Goal "[| a < b; \
\ \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \
-\ \\<forall>x. a < x & x < b --> DERIV f x :> Numeral0 |] \
+\ \\<forall>x. a < x & x < b --> DERIV f x :> 0 |] \
\ ==> \\<forall>x. a \\<le> x & x \\<le> b --> f x = f a";
by Safe_tac;
by (dres_inst_tac [("x","a")] order_le_imp_less_or_eq 1);
@@ -2119,13 +2116,13 @@
Goal "[| a < b; \
\ \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \
-\ \\<forall>x. a < x & x < b --> DERIV f x :> Numeral0; \
+\ \\<forall>x. a < x & x < b --> DERIV f x :> 0; \
\ a \\<le> x; x \\<le> b |] \
\ ==> f x = f a";
by (blast_tac (claset() addDs [DERIV_isconst1]) 1);
qed "DERIV_isconst2";
-Goal "\\<forall>x. DERIV f x :> Numeral0 ==> f(x) = f(y)";
+Goal "\\<forall>x. DERIV f x :> 0 ==> f(x) = f(y)";
by (res_inst_tac [("R1.0","x"),("R2.0","y")] real_linear_less2 1);
by (rtac sym 1);
by (auto_tac (claset() addIs [DERIV_isCont,DERIV_isconst_end],simpset()));
@@ -2182,7 +2179,7 @@
(* maximum at an end point, not in the middle. *)
(* ------------------------------------------------------------------------ *)
-Goal "[|Numeral0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
+Goal "[|0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
\ \\<forall>z. abs(z - x) \\<le> d --> isCont f z |] \
\ ==> ~(\\<forall>z. abs(z - x) \\<le> d --> f(z) \\<le> f(x))";
by (rtac notI 1);
@@ -2221,7 +2218,7 @@
(* Similar version for lower bound *)
(* ------------------------------------------------------------------------ *)
-Goal "[|Numeral0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
+Goal "[|0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
\ \\<forall>z. abs(z - x) \\<le> d --> isCont f z |] \
\ ==> ~(\\<forall>z. abs(z - x) \\<le> d --> f(x) \\<le> f(z))";
by (auto_tac (claset() addSDs [(asm_full_simplify (simpset())
@@ -2234,14 +2231,12 @@
(* Also from John's theory *)
(* ------------------------------------------------------------------------ *)
-Addsimps [zero_eq_numeral_0,one_eq_numeral_1];
-
-val lemma_le = ARITH_PROVE "Numeral0 \\<le> (d::real) ==> -d \\<le> d";
+val lemma_le = ARITH_PROVE "0 \\<le> (d::real) ==> -d \\<le> d";
(* FIXME: awful proof - needs improvement *)
-Goal "[| Numeral0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
+Goal "[| 0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
\ \\<forall>z. abs(z - x) \\<le> d --> isCont f z |] \
-\ ==> \\<exists>e. Numeral0 < e & \
+\ ==> \\<exists>e. 0 < e & \
\ (\\<forall>y. \
\ abs(y - f(x)) \\<le> e --> \
\ (\\<exists>z. abs(z - x) \\<le> d & (f z = y)))";
@@ -2255,10 +2250,10 @@
by (Asm_full_simp_tac 2);
by (subgoal_tac "L < f x & f x < M" 1);
by Safe_tac;
-by (dres_inst_tac [("x","L")] (ARITH_PROVE "x < y ==> Numeral0 < y - (x::real)") 1);
-by (dres_inst_tac [("x","f x")] (ARITH_PROVE "x < y ==> Numeral0 < y - (x::real)") 1);
+by (dres_inst_tac [("x","L")] (ARITH_PROVE "x < y ==> 0 < y - (x::real)") 1);
+by (dres_inst_tac [("x","f x")] (ARITH_PROVE "x < y ==> 0 < y - (x::real)") 1);
by (dres_inst_tac [("d1.0","f x - L"),("d2.0","M - f x")]
- (rename_numerals real_lbound_gt_zero) 1);
+ (real_lbound_gt_zero) 1);
by Safe_tac;
by (res_inst_tac [("x","e")] exI 1);
by Safe_tac;
@@ -2284,12 +2279,12 @@
(* Continuity of inverse function *)
(* ------------------------------------------------------------------------ *)
-Goal "[| Numeral0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f(z)) = z; \
+Goal "[| 0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f(z)) = z; \
\ \\<forall>z. abs(z - x) \\<le> d --> isCont f z |] \
\ ==> isCont g (f x)";
by (simp_tac (simpset() addsimps [isCont_iff,LIM_def]) 1);
by Safe_tac;
-by (dres_inst_tac [("d1.0","r")] (rename_numerals real_lbound_gt_zero) 1);
+by (dres_inst_tac [("d1.0","r")] (real_lbound_gt_zero) 1);
by (assume_tac 1 THEN Step_tac 1);
by (subgoal_tac "\\<forall>z. abs(z - x) \\<le> e --> (g(f z) = z)" 1);
by (Force_tac 2);