1.1 --- a/src/HOL/Hyperreal/Lim.ML Fri Oct 05 21:50:37 2001 +0200
1.2 +++ b/src/HOL/Hyperreal/Lim.ML Fri Oct 05 21:52:39 2001 +0200
1.3 @@ -29,7 +29,7 @@
1.4 Goalw [LIM_def]
1.5 "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)";
1.6 by (Clarify_tac 1);
1.7 -by (REPEAT(dres_inst_tac [("x","r/#2")] spec 1));
1.8 +by (REPEAT(dres_inst_tac [("x","r/# 2")] spec 1));
1.9 by (Asm_full_simp_tac 1);
1.10 by (Clarify_tac 1);
1.11 by (res_inst_tac [("R1.0","s"),("R2.0","sa")]
1.12 @@ -65,7 +65,7 @@
1.13 (*----------------------------------------------
1.14 LIM_zero
1.15 ----------------------------------------------*)
1.16 -Goal "f -- a --> l ==> (%x. f(x) + -l) -- a --> #0";
1.17 +Goal "f -- a --> l ==> (%x. f(x) + -l) -- a --> Numeral0";
1.18 by (res_inst_tac [("z1","l")] (rename_numerals (real_add_minus RS subst)) 1);
1.19 by (rtac LIM_add_minus 1 THEN Auto_tac);
1.20 qed "LIM_zero";
1.21 @@ -73,8 +73,8 @@
1.22 (*--------------------------
1.23 Limit not zero
1.24 --------------------------*)
1.25 -Goalw [LIM_def] "k \\<noteq> #0 ==> ~ ((%x. k) -- x --> #0)";
1.26 -by (res_inst_tac [("R1.0","k"),("R2.0","#0")] real_linear_less2 1);
1.27 +Goalw [LIM_def] "k \\<noteq> Numeral0 ==> ~ ((%x. k) -- x --> Numeral0)";
1.28 +by (res_inst_tac [("R1.0","k"),("R2.0","Numeral0")] real_linear_less2 1);
1.29 by (auto_tac (claset(), simpset() addsimps [real_abs_def]));
1.30 by (res_inst_tac [("x","-k")] exI 1);
1.31 by (res_inst_tac [("x","k")] exI 2);
1.32 @@ -85,7 +85,7 @@
1.33 by Auto_tac;
1.34 qed "LIM_not_zero";
1.35
1.36 -(* [| k \\<noteq> #0; (%x. k) -- x --> #0 |] ==> R *)
1.37 +(* [| k \\<noteq> Numeral0; (%x. k) -- x --> Numeral0 |] ==> R *)
1.38 bind_thm("LIM_not_zeroE", LIM_not_zero RS notE);
1.39
1.40 Goal "(%x. k) -- x --> L ==> k = L";
1.41 @@ -108,9 +108,9 @@
1.42 LIM_mult_zero
1.43 -------------*)
1.44 Goalw [LIM_def]
1.45 - "[| f -- x --> #0; g -- x --> #0 |] ==> (%x. f(x)*g(x)) -- x --> #0";
1.46 + "[| f -- x --> Numeral0; g -- x --> Numeral0 |] ==> (%x. f(x)*g(x)) -- x --> Numeral0";
1.47 by Safe_tac;
1.48 -by (dres_inst_tac [("x","#1")] spec 1);
1.49 +by (dres_inst_tac [("x","Numeral1")] spec 1);
1.50 by (dres_inst_tac [("x","r")] spec 1);
1.51 by (cut_facts_tac [real_zero_less_one] 1);
1.52 by (asm_full_simp_tac (simpset() addsimps
1.53 @@ -146,7 +146,7 @@
1.54 by (auto_tac (claset(), simpset() addsimps [real_add_minus_iff]));
1.55 qed "LIM_equal";
1.56
1.57 -Goal "[| (%x. f(x) + -g(x)) -- a --> #0; g -- a --> l |] \
1.58 +Goal "[| (%x. f(x) + -g(x)) -- a --> Numeral0; g -- a --> l |] \
1.59 \ ==> f -- a --> l";
1.60 by (dtac LIM_add 1 THEN assume_tac 1);
1.61 by (auto_tac (claset(), simpset() addsimps [real_add_assoc]));
1.62 @@ -181,7 +181,7 @@
1.63 Limit: NS definition ==> standard definition
1.64 ---------------------------------------------------------------------*)
1.65
1.66 -Goal "\\<forall>s. #0 < s --> (\\<exists>xa. xa \\<noteq> x & \
1.67 +Goal "\\<forall>s. Numeral0 < s --> (\\<exists>xa. xa \\<noteq> x & \
1.68 \ abs (xa + - x) < s & r \\<le> abs (f xa + -L)) \
1.69 \ ==> \\<forall>n::nat. \\<exists>xa. xa \\<noteq> x & \
1.70 \ abs(xa + -x) < inverse(real(Suc n)) & r \\<le> abs(f xa + -L)";
1.71 @@ -191,7 +191,7 @@
1.72 by Auto_tac;
1.73 val lemma_LIM = result();
1.74
1.75 -Goal "\\<forall>s. #0 < s --> (\\<exists>xa. xa \\<noteq> x & \
1.76 +Goal "\\<forall>s. Numeral0 < s --> (\\<exists>xa. xa \\<noteq> x & \
1.77 \ abs (xa + - x) < s & r \\<le> abs (f xa + -L)) \
1.78 \ ==> \\<exists>X. \\<forall>n::nat. X n \\<noteq> x & \
1.79 \ abs(X n + -x) < inverse(real(Suc n)) & r \\<le> abs(f (X n) + -L)";
1.80 @@ -320,7 +320,7 @@
1.81 NSLIM_inverse
1.82 -----------------------------*)
1.83 Goalw [NSLIM_def]
1.84 - "[| f -- a --NS> L; L \\<noteq> #0 |] \
1.85 + "[| f -- a --NS> L; L \\<noteq> Numeral0 |] \
1.86 \ ==> (%x. inverse(f(x))) -- a --NS> (inverse L)";
1.87 by (Clarify_tac 1);
1.88 by (dtac spec 1);
1.89 @@ -329,28 +329,28 @@
1.90 qed "NSLIM_inverse";
1.91
1.92 Goal "[| f -- a --> L; \
1.93 -\ L \\<noteq> #0 |] ==> (%x. inverse(f(x))) -- a --> (inverse L)";
1.94 +\ L \\<noteq> Numeral0 |] ==> (%x. inverse(f(x))) -- a --> (inverse L)";
1.95 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_inverse]) 1);
1.96 qed "LIM_inverse";
1.97
1.98 (*------------------------------
1.99 NSLIM_zero
1.100 ------------------------------*)
1.101 -Goal "f -- a --NS> l ==> (%x. f(x) + -l) -- a --NS> #0";
1.102 +Goal "f -- a --NS> l ==> (%x. f(x) + -l) -- a --NS> Numeral0";
1.103 by (res_inst_tac [("z1","l")] (rename_numerals (real_add_minus RS subst)) 1);
1.104 by (rtac NSLIM_add_minus 1 THEN Auto_tac);
1.105 qed "NSLIM_zero";
1.106
1.107 -Goal "f -- a --> l ==> (%x. f(x) + -l) -- a --> #0";
1.108 +Goal "f -- a --> l ==> (%x. f(x) + -l) -- a --> Numeral0";
1.109 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_zero]) 1);
1.110 qed "LIM_zero2";
1.111
1.112 -Goal "(%x. f(x) - l) -- x --NS> #0 ==> f -- x --NS> l";
1.113 +Goal "(%x. f(x) - l) -- x --NS> Numeral0 ==> f -- x --NS> l";
1.114 by (dres_inst_tac [("g","%x. l"),("m","l")] NSLIM_add 1);
1.115 by (auto_tac (claset(),simpset() addsimps [real_diff_def, real_add_assoc]));
1.116 qed "NSLIM_zero_cancel";
1.117
1.118 -Goal "(%x. f(x) - l) -- x --> #0 ==> f -- x --> l";
1.119 +Goal "(%x. f(x) - l) -- x --> Numeral0 ==> f -- x --> l";
1.120 by (dres_inst_tac [("g","%x. l"),("m","l")] LIM_add 1);
1.121 by (auto_tac (claset(),simpset() addsimps [real_diff_def, real_add_assoc]));
1.122 qed "LIM_zero_cancel";
1.123 @@ -359,17 +359,17 @@
1.124 (*--------------------------
1.125 NSLIM_not_zero
1.126 --------------------------*)
1.127 -Goalw [NSLIM_def] "k \\<noteq> #0 ==> ~ ((%x. k) -- x --NS> #0)";
1.128 +Goalw [NSLIM_def] "k \\<noteq> Numeral0 ==> ~ ((%x. k) -- x --NS> Numeral0)";
1.129 by Auto_tac;
1.130 by (res_inst_tac [("x","hypreal_of_real x + epsilon")] exI 1);
1.131 by (auto_tac (claset() addIs [Infinitesimal_add_approx_self RS approx_sym],
1.132 simpset() addsimps [rename_numerals hypreal_epsilon_not_zero]));
1.133 qed "NSLIM_not_zero";
1.134
1.135 -(* [| k \\<noteq> #0; (%x. k) -- x --NS> #0 |] ==> R *)
1.136 +(* [| k \\<noteq> Numeral0; (%x. k) -- x --NS> Numeral0 |] ==> R *)
1.137 bind_thm("NSLIM_not_zeroE", NSLIM_not_zero RS notE);
1.138
1.139 -Goal "k \\<noteq> #0 ==> ~ ((%x. k) -- x --> #0)";
1.140 +Goal "k \\<noteq> Numeral0 ==> ~ ((%x. k) -- x --> Numeral0)";
1.141 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_not_zero]) 1);
1.142 qed "LIM_not_zero2";
1.143
1.144 @@ -405,16 +405,16 @@
1.145 (*--------------------
1.146 NSLIM_mult_zero
1.147 --------------------*)
1.148 -Goal "[| f -- x --NS> #0; g -- x --NS> #0 |] \
1.149 -\ ==> (%x. f(x)*g(x)) -- x --NS> #0";
1.150 +Goal "[| f -- x --NS> Numeral0; g -- x --NS> Numeral0 |] \
1.151 +\ ==> (%x. f(x)*g(x)) -- x --NS> Numeral0";
1.152 by (dtac NSLIM_mult 1 THEN Auto_tac);
1.153 qed "NSLIM_mult_zero";
1.154
1.155 (* we can use the corresponding thm LIM_mult2 *)
1.156 (* for standard definition of limit *)
1.157
1.158 -Goal "[| f -- x --> #0; g -- x --> #0 |] \
1.159 -\ ==> (%x. f(x)*g(x)) -- x --> #0";
1.160 +Goal "[| f -- x --> Numeral0; g -- x --> Numeral0 |] \
1.161 +\ ==> (%x. f(x)*g(x)) -- x --> Numeral0";
1.162 by (dtac LIM_mult2 1 THEN Auto_tac);
1.163 qed "LIM_mult_zero2";
1.164
1.165 @@ -499,7 +499,7 @@
1.166 --------------------------------------------------------------------------*)
1.167 (* Prove equivalence between NS limits - *)
1.168 (* seems easier than using standard def *)
1.169 -Goalw [NSLIM_def] "(f -- a --NS> L) = ((%h. f(a + h)) -- #0 --NS> L)";
1.170 +Goalw [NSLIM_def] "(f -- a --NS> L) = ((%h. f(a + h)) -- Numeral0 --NS> L)";
1.171 by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_zero]));
1.172 by (dres_inst_tac [("x","hypreal_of_real a + x")] spec 1);
1.173 by (dres_inst_tac [("x","-hypreal_of_real a + x")] spec 2);
1.174 @@ -516,15 +516,15 @@
1.175 hypreal_add, real_add_assoc, approx_refl, hypreal_zero_def]));
1.176 qed "NSLIM_h_iff";
1.177
1.178 -Goal "(f -- a --NS> f a) = ((%h. f(a + h)) -- #0 --NS> f a)";
1.179 +Goal "(f -- a --NS> f a) = ((%h. f(a + h)) -- Numeral0 --NS> f a)";
1.180 by (rtac NSLIM_h_iff 1);
1.181 qed "NSLIM_isCont_iff";
1.182
1.183 -Goal "(f -- a --> f a) = ((%h. f(a + h)) -- #0 --> f(a))";
1.184 +Goal "(f -- a --> f a) = ((%h. f(a + h)) -- Numeral0 --> f(a))";
1.185 by (simp_tac (simpset() addsimps [LIM_NSLIM_iff, NSLIM_isCont_iff]) 1);
1.186 qed "LIM_isCont_iff";
1.187
1.188 -Goalw [isCont_def] "(isCont f x) = ((%h. f(x + h)) -- #0 --> f(x))";
1.189 +Goalw [isCont_def] "(isCont f x) = ((%h. f(x + h)) -- Numeral0 --> f(x))";
1.190 by (simp_tac (simpset() addsimps [LIM_isCont_iff]) 1);
1.191 qed "isCont_iff";
1.192
1.193 @@ -574,11 +574,11 @@
1.194 qed "isCont_minus";
1.195
1.196 Goalw [isCont_def]
1.197 - "[| isCont f x; f x \\<noteq> #0 |] ==> isCont (%x. inverse (f x)) x";
1.198 + "[| isCont f x; f x \\<noteq> Numeral0 |] ==> isCont (%x. inverse (f x)) x";
1.199 by (blast_tac (claset() addIs [LIM_inverse]) 1);
1.200 qed "isCont_inverse";
1.201
1.202 -Goal "[| isNSCont f x; f x \\<noteq> #0 |] ==> isNSCont (%x. inverse (f x)) x";
1.203 +Goal "[| isNSCont f x; f x \\<noteq> Numeral0 |] ==> isNSCont (%x. inverse (f x)) x";
1.204 by (auto_tac (claset() addIs [isCont_inverse],simpset() addsimps
1.205 [isNSCont_isCont_iff]));
1.206 qed "isNSCont_inverse";
1.207 @@ -690,7 +690,7 @@
1.208 by (Ultra_tac 1);
1.209 qed "isUCont_isNSUCont";
1.210
1.211 -Goal "\\<forall>s. #0 < s --> (\\<exists>z y. abs (z + - y) < s & r \\<le> abs (f z + -f y)) \
1.212 +Goal "\\<forall>s. Numeral0 < s --> (\\<exists>z y. abs (z + - y) < s & r \\<le> abs (f z + -f y)) \
1.213 \ ==> \\<forall>n::nat. \\<exists>z y. \
1.214 \ abs(z + -y) < inverse(real(Suc n)) & \
1.215 \ r \\<le> abs(f z + -f y)";
1.216 @@ -700,7 +700,7 @@
1.217 by Auto_tac;
1.218 val lemma_LIMu = result();
1.219
1.220 -Goal "\\<forall>s. #0 < s --> (\\<exists>z y. abs (z + - y) < s & r \\<le> abs (f z + -f y)) \
1.221 +Goal "\\<forall>s. Numeral0 < s --> (\\<exists>z y. abs (z + - y) < s & r \\<le> abs (f z + -f y)) \
1.222 \ ==> \\<exists>X Y. \\<forall>n::nat. \
1.223 \ abs(X n + -(Y n)) < inverse(real(Suc n)) & \
1.224 \ r \\<le> abs(f (X n) + -f (Y n))";
1.225 @@ -745,23 +745,23 @@
1.226 Derivatives
1.227 ------------------------------------------------------------------*)
1.228 Goalw [deriv_def]
1.229 - "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- #0 --> D)";
1.230 + "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- Numeral0 --> D)";
1.231 by (Blast_tac 1);
1.232 qed "DERIV_iff";
1.233
1.234 Goalw [deriv_def]
1.235 - "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- #0 --NS> D)";
1.236 + "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- Numeral0 --NS> D)";
1.237 by (simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1);
1.238 qed "DERIV_NS_iff";
1.239
1.240 Goalw [deriv_def]
1.241 "DERIV f x :> D \
1.242 -\ ==> (%h. (f(x + h) + - f(x))/h) -- #0 --> D";
1.243 +\ ==> (%h. (f(x + h) + - f(x))/h) -- Numeral0 --> D";
1.244 by (Blast_tac 1);
1.245 qed "DERIVD";
1.246
1.247 Goalw [deriv_def] "DERIV f x :> D ==> \
1.248 -\ (%h. (f(x + h) + - f(x))/h) -- #0 --NS> D";
1.249 +\ (%h. (f(x + h) + - f(x))/h) -- Numeral0 --NS> D";
1.250 by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1);
1.251 qed "NS_DERIVD";
1.252
1.253 @@ -809,7 +809,7 @@
1.254 -------------------------------------------------------*)
1.255
1.256 Goalw [LIM_def]
1.257 - "((%h. (f(a + h) + - f(a))/h) -- #0 --> D) = \
1.258 + "((%h. (f(a + h) + - f(a))/h) -- Numeral0 --> D) = \
1.259 \ ((%x. (f(x) + -f(a)) / (x + -a)) -- a --> D)";
1.260 by Safe_tac;
1.261 by (ALLGOALS(dtac spec));
1.262 @@ -836,7 +836,7 @@
1.263
1.264 (*--- first equivalence ---*)
1.265 Goalw [nsderiv_def,NSLIM_def]
1.266 - "(NSDERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- #0 --NS> D)";
1.267 + "(NSDERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- Numeral0 --NS> D)";
1.268 by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_zero]));
1.269 by (dres_inst_tac [("x","xa")] bspec 1);
1.270 by (rtac ccontr 3);
1.271 @@ -956,12 +956,12 @@
1.272 ------------------------*)
1.273
1.274 (* use simple constant nslimit theorem *)
1.275 -Goal "(NSDERIV (%x. k) x :> #0)";
1.276 +Goal "(NSDERIV (%x. k) x :> Numeral0)";
1.277 by (simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff]) 1);
1.278 qed "NSDERIV_const";
1.279 Addsimps [NSDERIV_const];
1.280
1.281 -Goal "(DERIV (%x. k) x :> #0)";
1.282 +Goal "(DERIV (%x. k) x :> Numeral0)";
1.283 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff RS sym]) 1);
1.284 qed "DERIV_const";
1.285 Addsimps [DERIV_const];
1.286 @@ -1000,7 +1000,7 @@
1.287
1.288 Goal "[| (x + y) / z = hypreal_of_real D + yb; z \\<noteq> 0; \
1.289 \ z \\<in> Infinitesimal; yb \\<in> Infinitesimal |] \
1.290 -\ ==> x + y \\<approx> #0";
1.291 +\ ==> x + y \\<approx> Numeral0";
1.292 by (forw_inst_tac [("c1","z")] (hypreal_mult_right_cancel RS iffD2) 1
1.293 THEN assume_tac 1);
1.294 by (thin_tac "(x + y) / z = hypreal_of_real D + yb" 1);
1.295 @@ -1127,7 +1127,7 @@
1.296 qed "incrementI2";
1.297
1.298 (* The Increment theorem -- Keisler p. 65 *)
1.299 -Goal "[| NSDERIV f x :> D; h \\<in> Infinitesimal; h \\<noteq> #0 |] \
1.300 +Goal "[| NSDERIV f x :> D; h \\<in> Infinitesimal; h \\<noteq> Numeral0 |] \
1.301 \ ==> \\<exists>e \\<in> Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h";
1.302 by (forw_inst_tac [("h","h")] incrementI2 1 THEN rewtac nsderiv_def);
1.303 by (dtac bspec 1 THEN Auto_tac);
1.304 @@ -1143,15 +1143,15 @@
1.305 simpset() addsimps [hypreal_add_mult_distrib]));
1.306 qed "increment_thm";
1.307
1.308 -Goal "[| NSDERIV f x :> D; h \\<approx> #0; h \\<noteq> #0 |] \
1.309 +Goal "[| NSDERIV f x :> D; h \\<approx> Numeral0; h \\<noteq> Numeral0 |] \
1.310 \ ==> \\<exists>e \\<in> Infinitesimal. increment f x h = \
1.311 \ hypreal_of_real(D)*h + e*h";
1.312 by (blast_tac (claset() addSDs [mem_infmal_iff RS iffD2]
1.313 addSIs [increment_thm]) 1);
1.314 qed "increment_thm2";
1.315
1.316 -Goal "[| NSDERIV f x :> D; h \\<approx> #0; h \\<noteq> #0 |] \
1.317 -\ ==> increment f x h \\<approx> #0";
1.318 +Goal "[| NSDERIV f x :> D; h \\<approx> Numeral0; h \\<noteq> Numeral0 |] \
1.319 +\ ==> increment f x h \\<approx> Numeral0";
1.320 by (dtac increment_thm2 1 THEN auto_tac (claset() addSIs
1.321 [Infinitesimal_HFinite_mult2,HFinite_add],simpset() addsimps
1.322 [hypreal_add_mult_distrib RS sym,mem_infmal_iff RS sym]));
1.323 @@ -1172,16 +1172,16 @@
1.324 "[| NSDERIV g x :> D; \
1.325 \ (*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);\
1.326 \ xa \\<in> Infinitesimal;\
1.327 -\ xa \\<noteq> #0 \
1.328 -\ |] ==> D = #0";
1.329 +\ xa \\<noteq> Numeral0 \
1.330 +\ |] ==> D = Numeral0";
1.331 by (dtac bspec 1);
1.332 by Auto_tac;
1.333 qed "NSDERIV_zero";
1.334
1.335 (* can be proved differently using NSLIM_isCont_iff *)
1.336 Goalw [nsderiv_def]
1.337 - "[| NSDERIV f x :> D; h \\<in> Infinitesimal; h \\<noteq> #0 |] \
1.338 -\ ==> (*f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\<approx> #0";
1.339 + "[| NSDERIV f x :> D; h \\<in> Infinitesimal; h \\<noteq> Numeral0 |] \
1.340 +\ ==> (*f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\<approx> Numeral0";
1.341 by (asm_full_simp_tac (simpset() addsimps
1.342 [mem_infmal_iff RS sym]) 1);
1.343 by (rtac Infinitesimal_ratio 1);
1.344 @@ -1214,7 +1214,7 @@
1.345 ----------------- \\<approx> Db
1.346 h
1.347 --------------------------------------------------------------*)
1.348 -Goal "[| NSDERIV g x :> Db; xa \\<in> Infinitesimal; xa \\<noteq> #0 |] \
1.349 +Goal "[| NSDERIV g x :> Db; xa \\<in> Infinitesimal; xa \\<noteq> Numeral0 |] \
1.350 \ ==> ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa \
1.351 \ \\<approx> hypreal_of_real(Db)";
1.352 by (auto_tac (claset(),
1.353 @@ -1266,7 +1266,7 @@
1.354 (*------------------------------------------------------------------
1.355 Differentiation of natural number powers
1.356 ------------------------------------------------------------------*)
1.357 -Goal "NSDERIV (%x. x) x :> #1";
1.358 +Goal "NSDERIV (%x. x) x :> Numeral1";
1.359 by (auto_tac (claset(),
1.360 simpset() addsimps [NSDERIV_NSLIM_iff,
1.361 NSLIM_def ,starfun_Id, hypreal_of_real_zero,
1.362 @@ -1275,7 +1275,7 @@
1.363 Addsimps [NSDERIV_Id];
1.364
1.365 (*derivative of the identity function*)
1.366 -Goal "DERIV (%x. x) x :> #1";
1.367 +Goal "DERIV (%x. x) x :> Numeral1";
1.368 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff RS sym]) 1);
1.369 qed "DERIV_Id";
1.370 Addsimps [DERIV_Id];
1.371 @@ -1294,7 +1294,7 @@
1.372 qed "NSDERIV_cmult_Id";
1.373 Addsimps [NSDERIV_cmult_Id];
1.374
1.375 -Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - 1'))";
1.376 +Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))";
1.377 by (induct_tac "n" 1);
1.378 by (dtac (DERIV_Id RS DERIV_mult) 2);
1.379 by (auto_tac (claset(),
1.380 @@ -1306,7 +1306,7 @@
1.381 qed "DERIV_pow";
1.382
1.383 (* NS version *)
1.384 -Goal "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - 1'))";
1.385 +Goal "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))";
1.386 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, DERIV_pow]) 1);
1.387 qed "NSDERIV_pow";
1.388
1.389 @@ -1314,9 +1314,9 @@
1.390 Power of -1
1.391 ---------------------------------------------------------------*)
1.392
1.393 -(*Can't get rid of x \\<noteq> #0 because it isn't continuous at zero*)
1.394 +(*Can't get rid of x \\<noteq> Numeral0 because it isn't continuous at zero*)
1.395 Goalw [nsderiv_def]
1.396 - "x \\<noteq> #0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))";
1.397 + "x \\<noteq> Numeral0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))";
1.398 by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1);
1.399 by (forward_tac [Infinitesimal_add_not_zero] 1);
1.400 by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 2);
1.401 @@ -1345,7 +1345,7 @@
1.402 qed "NSDERIV_inverse";
1.403
1.404
1.405 -Goal "x \\<noteq> #0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))";
1.406 +Goal "x \\<noteq> Numeral0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))";
1.407 by (asm_simp_tac (simpset() addsimps [NSDERIV_inverse,
1.408 NSDERIV_DERIV_iff RS sym] delsimps [realpow_Suc]) 1);
1.409 qed "DERIV_inverse";
1.410 @@ -1353,8 +1353,8 @@
1.411 (*--------------------------------------------------------------
1.412 Derivative of inverse
1.413 -------------------------------------------------------------*)
1.414 -Goal "[| DERIV f x :> d; f(x) \\<noteq> #0 |] \
1.415 -\ ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))";
1.416 +Goal "[| DERIV f x :> d; f(x) \\<noteq> Numeral0 |] \
1.417 +\ ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))";
1.418 by (rtac (real_mult_commute RS subst) 1);
1.419 by (asm_simp_tac (simpset() addsimps [real_minus_mult_eq1,
1.420 realpow_inverse] delsimps [realpow_Suc,
1.421 @@ -1363,8 +1363,8 @@
1.422 by (blast_tac (claset() addSIs [DERIV_chain,DERIV_inverse]) 1);
1.423 qed "DERIV_inverse_fun";
1.424
1.425 -Goal "[| NSDERIV f x :> d; f(x) \\<noteq> #0 |] \
1.426 -\ ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))";
1.427 +Goal "[| NSDERIV f x :> d; f(x) \\<noteq> Numeral0 |] \
1.428 +\ ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))";
1.429 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff,
1.430 DERIV_inverse_fun] delsimps [realpow_Suc]) 1);
1.431 qed "NSDERIV_inverse_fun";
1.432 @@ -1372,8 +1372,8 @@
1.433 (*--------------------------------------------------------------
1.434 Derivative of quotient
1.435 -------------------------------------------------------------*)
1.436 -Goal "[| DERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> #0 |] \
1.437 -\ ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) + -(e*f(x))) / (g(x) ^ 2)";
1.438 +Goal "[| DERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> Numeral0 |] \
1.439 +\ ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) + -(e*f(x))) / (g(x) ^ Suc (Suc 0))";
1.440 by (dres_inst_tac [("f","g")] DERIV_inverse_fun 1);
1.441 by (dtac DERIV_mult 2);
1.442 by (REPEAT(assume_tac 1));
1.443 @@ -1384,9 +1384,9 @@
1.444 real_minus_mult_eq2 RS sym]) 1);
1.445 qed "DERIV_quotient";
1.446
1.447 -Goal "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> #0 |] \
1.448 +Goal "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \\<noteq> Numeral0 |] \
1.449 \ ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) \
1.450 -\ + -(e*f(x))) / (g(x) ^ 2)";
1.451 +\ + -(e*f(x))) / (g(x) ^ Suc (Suc 0))";
1.452 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff,
1.453 DERIV_quotient] delsimps [realpow_Suc]) 1);
1.454 qed "NSDERIV_quotient";
1.455 @@ -1401,7 +1401,7 @@
1.456 by (res_inst_tac
1.457 [("x","%z. if z = x then l else (f(z) - f(x)) / (z - x)")] exI 1);
1.458 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,
1.459 - ARITH_PROVE "z \\<noteq> x ==> z - x \\<noteq> (#0::real)"]));
1.460 + ARITH_PROVE "z \\<noteq> x ==> z - x \\<noteq> (Numeral0::real)"]));
1.461 by (auto_tac (claset(),simpset() addsimps [isCont_iff,DERIV_iff]));
1.462 by (ALLGOALS(rtac (LIM_equal RS iffD1)));
1.463 by (auto_tac (claset(),simpset() addsimps [real_diff_def,real_mult_assoc]));
1.464 @@ -1511,7 +1511,7 @@
1.465 Goal "[| \\<forall>n. f(n) \\<le> f(Suc n); \
1.466 \ \\<forall>n. g(Suc n) \\<le> g(n); \
1.467 \ \\<forall>n. f(n) \\<le> g(n); \
1.468 -\ (%n. f(n) - g(n)) ----> #0 |] \
1.469 +\ (%n. f(n) - g(n)) ----> Numeral0 |] \
1.470 \ ==> \\<exists>l. ((\\<forall>n. f(n) \\<le> l) & f ----> l) & \
1.471 \ ((\\<forall>n. l \\<le> g(n)) & g ----> l)";
1.472 by (dtac lemma_nest 1 THEN Auto_tac);
1.473 @@ -1544,15 +1544,15 @@
1.474 simpset() addsimps [Bolzano_bisect_le, Let_def, split_def]));
1.475 qed "Bolzano_bisect_Suc_le_snd";
1.476
1.477 -Goal "((x::real) = y / (#2 * z)) = (#2 * x = y/z)";
1.478 +Goal "((x::real) = y / (# 2 * z)) = (# 2 * x = y/z)";
1.479 by Auto_tac;
1.480 -by (dres_inst_tac [("f","%u. (#1/#2)*u")] arg_cong 1);
1.481 +by (dres_inst_tac [("f","%u. (Numeral1/# 2)*u")] arg_cong 1);
1.482 by Auto_tac;
1.483 qed "eq_divide_2_times_iff";
1.484
1.485 Goal "a \\<le> b ==> \
1.486 \ snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) = \
1.487 -\ (b-a) / (#2 ^ n)";
1.488 +\ (b-a) / (# 2 ^ n)";
1.489 by (induct_tac "n" 1);
1.490 by (auto_tac (claset(),
1.491 simpset() addsimps [eq_divide_2_times_iff, real_add_divide_distrib,
1.492 @@ -1589,7 +1589,7 @@
1.493
1.494
1.495 Goal "[| \\<forall>a b c. P(a,b) & P(b,c) & a \\<le> b & b \\<le> c --> P(a,c); \
1.496 -\ \\<forall>x. \\<exists>d::real. #0 < d & \
1.497 +\ \\<forall>x. \\<exists>d::real. Numeral0 < d & \
1.498 \ (\\<forall>a b. a \\<le> x & x \\<le> b & (b - a) < d --> P(a,b)); \
1.499 \ a \\<le> b |] \
1.500 \ ==> P(a,b)";
1.501 @@ -1604,8 +1604,8 @@
1.502 by (rename_tac "l" 1);
1.503 by (dres_inst_tac [("x","l")] spec 1 THEN Clarify_tac 1);
1.504 by (rewtac LIMSEQ_def);
1.505 -by (dres_inst_tac [("P", "%r. #0<r --> ?Q r"), ("x","d/#2")] spec 1);
1.506 -by (dres_inst_tac [("P", "%r. #0<r --> ?Q r"), ("x","d/#2")] spec 1);
1.507 +by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/# 2")] spec 1);
1.508 +by (dres_inst_tac [("P", "%r. Numeral0<r --> ?Q r"), ("x","d/# 2")] spec 1);
1.509 by (dtac real_less_half_sum 1);
1.510 by Safe_tac;
1.511 (*linear arithmetic bug if we just use Asm_simp_tac*)
1.512 @@ -1626,7 +1626,7 @@
1.513
1.514
1.515 Goal "((\\<forall>a b c. (a \\<le> b & b \\<le> c & P(a,b) & P(b,c)) --> P(a,c)) & \
1.516 -\ (\\<forall>x. \\<exists>d::real. #0 < d & \
1.517 +\ (\\<forall>x. \\<exists>d::real. Numeral0 < d & \
1.518 \ (\\<forall>a b. a \\<le> x & x \\<le> b & (b - a) < d --> P(a,b)))) \
1.519 \ --> (\\<forall>a b. a \\<le> b --> P(a,b))";
1.520 by (Clarify_tac 1);
1.521 @@ -1654,14 +1654,14 @@
1.522 by (rtac ccontr 1);
1.523 by (subgoal_tac "a \\<le> x & x \\<le> b" 1);
1.524 by (Asm_full_simp_tac 2);
1.525 -by (dres_inst_tac [("P", "%d. #0<d --> ?P d"),("x","#1")] spec 2);
1.526 +by (dres_inst_tac [("P", "%d. Numeral0<d --> ?P d"),("x","Numeral1")] spec 2);
1.527 by (Step_tac 2);
1.528 by (Asm_full_simp_tac 2);
1.529 by (Asm_full_simp_tac 2);
1.530 by (REPEAT(blast_tac (claset() addIs [order_trans]) 2));
1.531 by (REPEAT(dres_inst_tac [("x","x")] spec 1));
1.532 by (Asm_full_simp_tac 1);
1.533 -by (dres_inst_tac [("P", "%r. ?P r --> (\\<exists>s. #0<s & ?Q r s)"),
1.534 +by (dres_inst_tac [("P", "%r. ?P r --> (\\<exists>s. Numeral0<s & ?Q r s)"),
1.535 ("x","abs(y - f x)")] spec 1);
1.536 by Safe_tac;
1.537 by (asm_full_simp_tac (simpset() addsimps []) 1);
1.538 @@ -1738,15 +1738,15 @@
1.539 by (cut_inst_tac [("x","xb"),("y","xa")] linorder_linear 1);
1.540 by (Force_tac 1);
1.541 by (case_tac "a \\<le> x & x \\<le> b" 1);
1.542 -by (res_inst_tac [("x","#1")] exI 2);
1.543 +by (res_inst_tac [("x","Numeral1")] exI 2);
1.544 by (Force_tac 2);
1.545 by (asm_full_simp_tac (simpset() addsimps [LIM_def,isCont_iff]) 1);
1.546 by (dres_inst_tac [("x","x")] spec 1 THEN Auto_tac);
1.547 by (thin_tac "\\<forall>M. \\<exists>x. a \\<le> x & x \\<le> b & ~ f x \\<le> M" 1);
1.548 -by (dres_inst_tac [("x","#1")] spec 1);
1.549 +by (dres_inst_tac [("x","Numeral1")] spec 1);
1.550 by Auto_tac;
1.551 by (res_inst_tac [("x","s")] exI 1 THEN Clarify_tac 1);
1.552 -by (res_inst_tac [("x","abs(f x) + #1")] exI 1 THEN Clarify_tac 1);
1.553 +by (res_inst_tac [("x","abs(f x) + Numeral1")] exI 1 THEN Clarify_tac 1);
1.554 by (dres_inst_tac [("x","xa - x")] spec 1 THEN Safe_tac);
1.555 by (arith_tac 1);
1.556 by (arith_tac 1);
1.557 @@ -1803,23 +1803,23 @@
1.558 "\\<exists>k. \\<forall>x. a \\<le> x & x \\<le> b --> (%x. inverse(M - (f x))) x \\<le> k" 1);
1.559 by (rtac isCont_bounded 2);
1.560 by Safe_tac;
1.561 -by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> #0 < inverse(M - f(x))" 1);
1.562 +by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> Numeral0 < inverse(M - f(x))" 1);
1.563 by (Asm_full_simp_tac 1);
1.564 by Safe_tac;
1.565 by (asm_full_simp_tac (simpset() addsimps [real_less_diff_eq]) 2);
1.566 by (subgoal_tac
1.567 - "\\<forall>x. a \\<le> x & x \\<le> b --> (%x. inverse(M - (f x))) x < (k + #1)" 1);
1.568 + "\\<forall>x. a \\<le> x & x \\<le> b --> (%x. inverse(M - (f x))) x < (k + Numeral1)" 1);
1.569 by Safe_tac;
1.570 by (res_inst_tac [("y","k")] order_le_less_trans 2);
1.571 by (asm_full_simp_tac (simpset() addsimps [real_zero_less_one]) 3);
1.572 by (Asm_full_simp_tac 2);
1.573 by (subgoal_tac "\\<forall>x. a \\<le> x & x \\<le> b --> \
1.574 -\ inverse(k + #1) < inverse((%x. inverse(M - (f x))) x)" 1);
1.575 +\ inverse(k + Numeral1) < inverse((%x. inverse(M - (f x))) x)" 1);
1.576 by Safe_tac;
1.577 by (rtac real_inverse_less_swap 2);
1.578 by (ALLGOALS Asm_full_simp_tac);
1.579 by (dres_inst_tac [("P", "%N. N<M --> ?Q N"),
1.580 - ("x","M - inverse(k + #1)")] spec 1);
1.581 + ("x","M - inverse(k + Numeral1)")] spec 1);
1.582 by (Step_tac 1 THEN dtac real_leI 1);
1.583 by (dtac (real_le_diff_eq RS iffD1) 1);
1.584 by (REPEAT(dres_inst_tac [("x","a")] spec 1));
1.585 @@ -1879,11 +1879,11 @@
1.586 (*----------------------------------------------------------------------------*)
1.587
1.588 Goalw [deriv_def,LIM_def]
1.589 - "[| DERIV f x :> l; #0 < l |] ==> \
1.590 -\ \\<exists>d. #0 < d & (\\<forall>h. #0 < h & h < d --> f(x) < f(x + h))";
1.591 + "[| DERIV f x :> l; Numeral0 < l |] ==> \
1.592 +\ \\<exists>d. Numeral0 < d & (\\<forall>h. Numeral0 < h & h < d --> f(x) < f(x + h))";
1.593 by (dtac spec 1 THEN Auto_tac);
1.594 by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac);
1.595 -by (subgoal_tac "#0 < l*h" 1);
1.596 +by (subgoal_tac "Numeral0 < l*h" 1);
1.597 by (asm_full_simp_tac (simpset() addsimps [real_0_less_mult_iff]) 2);
1.598 by (dres_inst_tac [("x","h")] spec 1);
1.599 by (asm_full_simp_tac
1.600 @@ -1893,11 +1893,11 @@
1.601 qed "DERIV_left_inc";
1.602
1.603 Goalw [deriv_def,LIM_def]
1.604 - "[| DERIV f x :> l; l < #0 |] ==> \
1.605 -\ \\<exists>d. #0 < d & (\\<forall>h. #0 < h & h < d --> f(x) < f(x - h))";
1.606 + "[| DERIV f x :> l; l < Numeral0 |] ==> \
1.607 +\ \\<exists>d. Numeral0 < d & (\\<forall>h. Numeral0 < h & h < d --> f(x) < f(x - h))";
1.608 by (dres_inst_tac [("x","-l")] spec 1 THEN Auto_tac);
1.609 by (res_inst_tac [("x","s")] exI 1 THEN Auto_tac);
1.610 -by (subgoal_tac "l*h < #0" 1);
1.611 +by (subgoal_tac "l*h < Numeral0" 1);
1.612 by (asm_full_simp_tac (simpset() addsimps [real_mult_less_0_iff]) 2);
1.613 by (dres_inst_tac [("x","-h")] spec 1);
1.614 by (asm_full_simp_tac
1.615 @@ -1905,7 +1905,7 @@
1.616 pos_real_less_divide_eq,
1.617 symmetric real_diff_def]
1.618 addsplits [split_if_asm]) 1);
1.619 -by (subgoal_tac "#0 < (f (x - h) - f x)/h" 1);
1.620 +by (subgoal_tac "Numeral0 < (f (x - h) - f x)/h" 1);
1.621 by (arith_tac 2);
1.622 by (asm_full_simp_tac
1.623 (simpset() addsimps [pos_real_less_divide_eq]) 1);
1.624 @@ -1913,9 +1913,9 @@
1.625
1.626
1.627 Goal "[| DERIV f x :> l; \
1.628 -\ \\<exists>d. #0 < d & (\\<forall>y. abs(x - y) < d --> f(y) \\<le> f(x)) |] \
1.629 -\ ==> l = #0";
1.630 -by (res_inst_tac [("R1.0","l"),("R2.0","#0")] real_linear_less2 1);
1.631 +\ \\<exists>d. Numeral0 < d & (\\<forall>y. abs(x - y) < d --> f(y) \\<le> f(x)) |] \
1.632 +\ ==> l = Numeral0";
1.633 +by (res_inst_tac [("R1.0","l"),("R2.0","Numeral0")] real_linear_less2 1);
1.634 by Safe_tac;
1.635 by (dtac DERIV_left_dec 1);
1.636 by (dtac DERIV_left_inc 3);
1.637 @@ -1933,8 +1933,8 @@
1.638 (*----------------------------------------------------------------------------*)
1.639
1.640 Goal "[| DERIV f x :> l; \
1.641 -\ \\<exists>d::real. #0 < d & (\\<forall>y. abs(x - y) < d --> f(x) \\<le> f(y)) |] \
1.642 -\ ==> l = #0";
1.643 +\ \\<exists>d::real. Numeral0 < d & (\\<forall>y. abs(x - y) < d --> f(x) \\<le> f(y)) |] \
1.644 +\ ==> l = Numeral0";
1.645 by (dtac (DERIV_minus RS DERIV_local_max) 1);
1.646 by Auto_tac;
1.647 qed "DERIV_local_min";
1.648 @@ -1944,8 +1944,8 @@
1.649 (*----------------------------------------------------------------------------*)
1.650
1.651 Goal "[| DERIV f x :> l; \
1.652 -\ \\<exists>d. #0 < d & (\\<forall>y. abs(x - y) < d --> f(x) = f(y)) |] \
1.653 -\ ==> l = #0";
1.654 +\ \\<exists>d. Numeral0 < d & (\\<forall>y. abs(x - y) < d --> f(x) = f(y)) |] \
1.655 +\ ==> l = Numeral0";
1.656 by (auto_tac (claset() addSDs [DERIV_local_max],simpset()));
1.657 qed "DERIV_local_const";
1.658
1.659 @@ -1954,7 +1954,7 @@
1.660 (*----------------------------------------------------------------------------*)
1.661
1.662 Goal "[| a < x; x < b |] ==> \
1.663 -\ \\<exists>d::real. #0 < d & (\\<forall>y. abs(x - y) < d --> a < y & y < b)";
1.664 +\ \\<exists>d::real. Numeral0 < d & (\\<forall>y. abs(x - y) < d --> a < y & y < b)";
1.665 by (simp_tac (simpset() addsimps [abs_interval_iff]) 1);
1.666 by (cut_inst_tac [("x","x - a"),("y","b - x")] linorder_linear 1);
1.667 by Safe_tac;
1.668 @@ -1965,7 +1965,7 @@
1.669 qed "lemma_interval_lt";
1.670
1.671 Goal "[| a < x; x < b |] ==> \
1.672 -\ \\<exists>d::real. #0 < d & (\\<forall>y. abs(x - y) < d --> a \\<le> y & y \\<le> b)";
1.673 +\ \\<exists>d::real. Numeral0 < d & (\\<forall>y. abs(x - y) < d --> a \\<le> y & y \\<le> b)";
1.674 by (dtac lemma_interval_lt 1);
1.675 by Auto_tac;
1.676 by (auto_tac (claset() addSIs [exI] ,simpset()));
1.677 @@ -1975,13 +1975,13 @@
1.678 Rolle's Theorem
1.679 If f is defined and continuous on the finite closed interval [a,b]
1.680 and differentiable a least on the open interval (a,b), and f(a) = f(b),
1.681 - then x0 \\<in> (a,b) such that f'(x0) = #0
1.682 + then x0 \\<in> (a,b) such that f'(x0) = Numeral0
1.683 ----------------------------------------------------------------------*)
1.684
1.685 Goal "[| a < b; f(a) = f(b); \
1.686 \ \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \
1.687 \ \\<forall>x. a < x & x < b --> f differentiable x \
1.688 -\ |] ==> \\<exists>z. a < z & z < b & DERIV f z :> #0";
1.689 +\ |] ==> \\<exists>z. a < z & z < b & DERIV f z :> Numeral0";
1.690 by (ftac (order_less_imp_le RS isCont_eq_Ub) 1);
1.691 by (EVERY1[assume_tac,Step_tac]);
1.692 by (ftac (order_less_imp_le RS isCont_eq_Lb) 1);
1.693 @@ -1992,7 +1992,7 @@
1.694 by (EVERY1[assume_tac,etac exE]);
1.695 by (res_inst_tac [("x","x")] exI 1 THEN Asm_full_simp_tac 1);
1.696 by (subgoal_tac "(\\<exists>l. DERIV f x :> l) & \
1.697 -\ (\\<exists>d. #0 < d & (\\<forall>y. abs(x - y) < d --> f(y) \\<le> f(x)))" 1);
1.698 +\ (\\<exists>d. Numeral0 < d & (\\<forall>y. abs(x - y) < d --> f(y) \\<le> f(x)))" 1);
1.699 by (Clarify_tac 1 THEN rtac conjI 2);
1.700 by (blast_tac (claset() addIs [differentiableD]) 2);
1.701 by (Blast_tac 2);
1.702 @@ -2004,7 +2004,7 @@
1.703 by (EVERY1[assume_tac,etac exE]);
1.704 by (res_inst_tac [("x","xa")] exI 1 THEN Asm_full_simp_tac 1);
1.705 by (subgoal_tac "(\\<exists>l. DERIV f xa :> l) & \
1.706 -\ (\\<exists>d. #0 < d & (\\<forall>y. abs(xa - y) < d --> f(xa) \\<le> f(y)))" 1);
1.707 +\ (\\<exists>d. Numeral0 < d & (\\<forall>y. abs(xa - y) < d --> f(xa) \\<le> f(y)))" 1);
1.708 by (Clarify_tac 1 THEN rtac conjI 2);
1.709 by (blast_tac (claset() addIs [differentiableD]) 2);
1.710 by (Blast_tac 2);
1.711 @@ -2030,7 +2030,7 @@
1.712 by (forw_inst_tac [("a","a"),("x","r")] lemma_interval 1);
1.713 by (EVERY1[assume_tac, etac exE]);
1.714 by (subgoal_tac "(\\<exists>l. DERIV f r :> l) & \
1.715 -\ (\\<exists>d. #0 < d & (\\<forall>y. abs(r - y) < d --> f(r) = f(y)))" 1);
1.716 +\ (\\<exists>d. Numeral0 < d & (\\<forall>y. abs(r - y) < d --> f(r) = f(y)))" 1);
1.717 by (Clarify_tac 1 THEN rtac conjI 2);
1.718 by (blast_tac (claset() addIs [differentiableD]) 2);
1.719 by (EVERY1[ftac DERIV_local_const, Blast_tac, Blast_tac]);
1.720 @@ -2098,7 +2098,7 @@
1.721
1.722 Goal "[| a < b; \
1.723 \ \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \
1.724 -\ \\<forall>x. a < x & x < b --> DERIV f x :> #0 |] \
1.725 +\ \\<forall>x. a < x & x < b --> DERIV f x :> Numeral0 |] \
1.726 \ ==> (f b = f a)";
1.727 by (dtac MVT 1 THEN assume_tac 1);
1.728 by (blast_tac (claset() addIs [differentiableI]) 1);
1.729 @@ -2108,7 +2108,7 @@
1.730
1.731 Goal "[| a < b; \
1.732 \ \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \
1.733 -\ \\<forall>x. a < x & x < b --> DERIV f x :> #0 |] \
1.734 +\ \\<forall>x. a < x & x < b --> DERIV f x :> Numeral0 |] \
1.735 \ ==> \\<forall>x. a \\<le> x & x \\<le> b --> f x = f a";
1.736 by Safe_tac;
1.737 by (dres_inst_tac [("x","a")] order_le_imp_less_or_eq 1);
1.738 @@ -2119,13 +2119,13 @@
1.739
1.740 Goal "[| a < b; \
1.741 \ \\<forall>x. a \\<le> x & x \\<le> b --> isCont f x; \
1.742 -\ \\<forall>x. a < x & x < b --> DERIV f x :> #0; \
1.743 +\ \\<forall>x. a < x & x < b --> DERIV f x :> Numeral0; \
1.744 \ a \\<le> x; x \\<le> b |] \
1.745 \ ==> f x = f a";
1.746 by (blast_tac (claset() addDs [DERIV_isconst1]) 1);
1.747 qed "DERIV_isconst2";
1.748
1.749 -Goal "\\<forall>x. DERIV f x :> #0 ==> f(x) = f(y)";
1.750 +Goal "\\<forall>x. DERIV f x :> Numeral0 ==> f(x) = f(y)";
1.751 by (res_inst_tac [("R1.0","x"),("R2.0","y")] real_linear_less2 1);
1.752 by (rtac sym 1);
1.753 by (auto_tac (claset() addIs [DERIV_isCont,DERIV_isconst_end],simpset()));
1.754 @@ -2148,12 +2148,12 @@
1.755 simpset() addsimps [real_mult_assoc]));
1.756 qed "DERIV_const_ratio_const2";
1.757
1.758 -Goal "((a + b) /#2 - a) = (b - a)/(#2::real)";
1.759 +Goal "((a + b) /# 2 - a) = (b - a)/(# 2::real)";
1.760 by Auto_tac;
1.761 qed "real_average_minus_first";
1.762 Addsimps [real_average_minus_first];
1.763
1.764 -Goal "((b + a)/#2 - a) = (b - a)/(#2::real)";
1.765 +Goal "((b + a)/# 2 - a) = (b - a)/(# 2::real)";
1.766 by Auto_tac;
1.767 qed "real_average_minus_second";
1.768 Addsimps [real_average_minus_second];
1.769 @@ -2161,7 +2161,7 @@
1.770
1.771 (* Gallileo's "trick": average velocity = av. of end velocities *)
1.772 Goal "[|a \\<noteq> (b::real); \\<forall>x. DERIV v x :> k|] \
1.773 -\ ==> v((a + b)/#2) = (v a + v b)/#2";
1.774 +\ ==> v((a + b)/# 2) = (v a + v b)/# 2";
1.775 by (res_inst_tac [("R1.0","a"),("R2.0","b")] real_linear_less2 1);
1.776 by Auto_tac;
1.777 by (ftac DERIV_const_ratio_const2 1 THEN assume_tac 1);
1.778 @@ -2182,7 +2182,7 @@
1.779 (* maximum at an end point, not in the middle. *)
1.780 (* ------------------------------------------------------------------------ *)
1.781
1.782 -Goal "[|#0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
1.783 +Goal "[|Numeral0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
1.784 \ \\<forall>z. abs(z - x) \\<le> d --> isCont f z |] \
1.785 \ ==> ~(\\<forall>z. abs(z - x) \\<le> d --> f(z) \\<le> f(x))";
1.786 by (rtac notI 1);
1.787 @@ -2221,7 +2221,7 @@
1.788 (* Similar version for lower bound *)
1.789 (* ------------------------------------------------------------------------ *)
1.790
1.791 -Goal "[|#0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
1.792 +Goal "[|Numeral0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
1.793 \ \\<forall>z. abs(z - x) \\<le> d --> isCont f z |] \
1.794 \ ==> ~(\\<forall>z. abs(z - x) \\<le> d --> f(x) \\<le> f(z))";
1.795 by (auto_tac (claset() addSDs [(asm_full_simplify (simpset())
1.796 @@ -2236,12 +2236,12 @@
1.797
1.798 Addsimps [zero_eq_numeral_0,one_eq_numeral_1];
1.799
1.800 -val lemma_le = ARITH_PROVE "#0 \\<le> (d::real) ==> -d \\<le> d";
1.801 +val lemma_le = ARITH_PROVE "Numeral0 \\<le> (d::real) ==> -d \\<le> d";
1.802
1.803 (* FIXME: awful proof - needs improvement *)
1.804 -Goal "[| #0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
1.805 +Goal "[| Numeral0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f z) = z; \
1.806 \ \\<forall>z. abs(z - x) \\<le> d --> isCont f z |] \
1.807 -\ ==> \\<exists>e. #0 < e & \
1.808 +\ ==> \\<exists>e. Numeral0 < e & \
1.809 \ (\\<forall>y. \
1.810 \ abs(y - f(x)) \\<le> e --> \
1.811 \ (\\<exists>z. abs(z - x) \\<le> d & (f z = y)))";
1.812 @@ -2255,8 +2255,8 @@
1.813 by (Asm_full_simp_tac 2);
1.814 by (subgoal_tac "L < f x & f x < M" 1);
1.815 by Safe_tac;
1.816 -by (dres_inst_tac [("x","L")] (ARITH_PROVE "x < y ==> #0 < y - (x::real)") 1);
1.817 -by (dres_inst_tac [("x","f x")] (ARITH_PROVE "x < y ==> #0 < y - (x::real)") 1);
1.818 +by (dres_inst_tac [("x","L")] (ARITH_PROVE "x < y ==> Numeral0 < y - (x::real)") 1);
1.819 +by (dres_inst_tac [("x","f x")] (ARITH_PROVE "x < y ==> Numeral0 < y - (x::real)") 1);
1.820 by (dres_inst_tac [("d1.0","f x - L"),("d2.0","M - f x")]
1.821 (rename_numerals real_lbound_gt_zero) 1);
1.822 by Safe_tac;
1.823 @@ -2284,7 +2284,7 @@
1.824 (* Continuity of inverse function *)
1.825 (* ------------------------------------------------------------------------ *)
1.826
1.827 -Goal "[| #0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f(z)) = z; \
1.828 +Goal "[| Numeral0 < d; \\<forall>z. abs(z - x) \\<le> d --> g(f(z)) = z; \
1.829 \ \\<forall>z. abs(z - x) \\<le> d --> isCont f z |] \
1.830 \ ==> isCont g (f x)";
1.831 by (simp_tac (simpset() addsimps [isCont_iff,LIM_def]) 1);