--- a/src/HOL/Real/Hyperreal/HRealAbs.ML Mon Dec 18 12:21:54 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HRealAbs.ML Mon Dec 18 12:23:54 2000 +0100
@@ -63,10 +63,11 @@
hypreal_less_asym],simpset()));
qed "hrabs_ge_zero";
-Goal "abs(abs x)=abs (x::hypreal)";
+Goal "abs(abs x) = abs (x::hypreal)";
by (res_inst_tac [("r1","abs x")] (hrabs_iff RS ssubst) 1);
by (blast_tac (claset() addIs [if_P,hrabs_ge_zero]) 1);
qed "hrabs_idempotent";
+Addsimps [hrabs_idempotent];
Goalw [hrabs_def] "(x=(0::hypreal)) = (abs x = (0::hypreal))";
by (Simp_tac 1);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/Hyperreal/HSeries.ML Mon Dec 18 12:23:54 2000 +0100
@@ -0,0 +1,323 @@
+(* Title : HSeries.ML
+ Author : Jacques D. Fleuriot
+ Copyright : 1998 University of Cambridge
+ Description : Finite summation and infinite series
+ for hyperreals
+*)
+
+Goalw [sumhr_def]
+ "sumhr(M,N,f) = Abs_hypreal(UN X:Rep_hypnat(M). \
+\ UN Y: Rep_hypnat(N). \
+\ hyprel ^^{%n::nat. sumr (X n) (Y n) f})";
+by (Auto_tac);
+qed "sumhr_iff";
+
+Goalw [sumhr_def]
+ "sumhr(Abs_hypnat(hypnatrel^^{%n. M n}), \
+\ Abs_hypnat(hypnatrel^^{%n. N n}),f) = \
+\ Abs_hypreal(hyprel ^^ {%n. sumr (M n) (N n) f})";
+by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
+by (Auto_tac THEN Ultra_tac 1);
+qed "sumhr";
+
+(*-------------------------------------------------------
+ lcp's suggestion: exploit pattern matching
+ facilities and use as definition instead (to do)
+ -------------------------------------------------------*)
+Goalw [sumhr_def]
+ "sumhr p = (%(M,N,f). Abs_hypreal(UN X:Rep_hypnat(M). \
+\ UN Y: Rep_hypnat(N). \
+\ hyprel ^^{%n::nat. sumr (X n) (Y n) f})) p";
+by (res_inst_tac [("p","p")] PairE 1);
+by (res_inst_tac [("p","y")] PairE 1);
+by (Auto_tac);
+qed "sumhr_iff2";
+
+(* Theorem corresponding to base case in def of sumr *)
+Goalw [hypnat_zero_def,hypreal_zero_def]
+ "sumhr (m,0,f) = 0";
+by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
+by (auto_tac (claset(),simpset() addsimps [sumhr]));
+qed "sumhr_zero";
+Addsimps [sumhr_zero];
+
+(* Theorem corresponding to recursive case in def of sumr *)
+Goalw [hypnat_one_def,hypreal_zero_def]
+ "sumhr(m,n+1hn,f) = (if n + 1hn <= m then 0 \
+\ else sumhr(m,n,f) + (*fNat* f) n)";
+by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
+by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
+by (auto_tac (claset(),simpset() addsimps [sumhr,
+ hypnat_add,hypnat_le,starfunNat,hypreal_add]));
+by (ALLGOALS(Ultra_tac));
+qed "sumhr_if";
+
+Goalw [hypnat_one_def,hypreal_zero_def]
+ "sumhr (n + 1hn, n, f) = 0";
+by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
+by (auto_tac (claset(),simpset() addsimps [sumhr,
+ hypnat_add]));
+qed "sumhr_Suc_zero";
+Addsimps [sumhr_Suc_zero];
+
+Goalw [hypreal_zero_def]
+ "sumhr (n,n,f) = 0";
+by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
+by (auto_tac (claset(), simpset() addsimps [sumhr]));
+qed "sumhr_eq_bounds";
+Addsimps [sumhr_eq_bounds];
+
+Goalw [hypnat_one_def]
+ "sumhr (m,m + 1hn,f) = (*fNat* f) m";
+by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
+by (auto_tac (claset(),simpset() addsimps [sumhr,
+ hypnat_add,starfunNat]));
+qed "sumhr_Suc";
+Addsimps [sumhr_Suc];
+
+Goalw [hypreal_zero_def]
+ "sumhr(m+k,k,f) = 0";
+by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
+by (res_inst_tac [("z","k")] eq_Abs_hypnat 1);
+by (auto_tac (claset(),simpset() addsimps [sumhr,
+ hypnat_add]));
+qed "sumhr_add_lbound_zero";
+Addsimps [sumhr_add_lbound_zero];
+
+Goal "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)";
+by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
+by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
+by (auto_tac (claset(),simpset() addsimps [sumhr,
+ hypreal_add,sumr_add]));
+qed "sumhr_add";
+
+Goalw [hypreal_of_real_def]
+ "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)";
+by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
+by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
+by (auto_tac (claset(),simpset() addsimps [sumhr,
+ hypreal_mult,sumr_mult]));
+qed "sumhr_mult";
+
+Goalw [hypnat_zero_def]
+ "n < p ==> sumhr (0,n,f) + sumhr (n,p,f) = sumhr (0,p,f)";
+by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
+by (res_inst_tac [("z","p")] eq_Abs_hypnat 1);
+by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset],
+ simpset() addsimps [sumhr,hypreal_add,hypnat_less,
+ sumr_split_add]));
+qed "sumhr_split_add";
+
+Goal
+ "n < p ==> sumhr (0, p, f) + \
+\ - sumhr (0, n, f) = sumhr (n,p,f)";
+by (dres_inst_tac [("f1","f")] (sumhr_split_add RS sym) 1);
+by (asm_simp_tac (simpset() addsimps hypreal_add_ac) 1);
+qed "sumhr_split_add_minus";
+
+Goal "abs(sumhr(m,n,f)) <= sumhr(m,n,%i. abs(f i))";
+by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
+by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
+by (auto_tac (claset(),simpset() addsimps [sumhr,
+ hypreal_le,hypreal_hrabs,sumr_rabs]));
+qed "sumhr_hrabs";
+
+(* other general version also needed *)
+Goalw [hypnat_of_nat_def]
+ "!!f g. (ALL r. m <= r & r < n --> f r = g r) \
+\ --> sumhr(hypnat_of_nat m,hypnat_of_nat n,f) = sumhr(hypnat_of_nat m,hypnat_of_nat n,g)";
+by (Step_tac 1 THEN dtac sumr_fun_eq 1);
+by (auto_tac (claset(),simpset() addsimps [sumhr]));
+qed "sumhr_fun_hypnat_eq";
+
+Goalw [hypnat_zero_def,hypreal_of_real_def]
+ "sumhr(0,n,%i. r) = hypreal_of_hypnat n*hypreal_of_real r";
+by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
+by (asm_simp_tac (simpset() addsimps [sumhr,
+ hypreal_of_hypnat,hypreal_mult]) 1);
+qed "sumhr_const";
+
+Goalw [hypnat_zero_def,hypreal_of_real_def]
+ "sumhr(0,n,f) + -(hypreal_of_hypnat n*hypreal_of_real r) = \
+\ sumhr(0,n,%i. f i + -r)";
+by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
+by (asm_simp_tac (simpset() addsimps [sumhr,
+ hypreal_of_hypnat,hypreal_mult,hypreal_add,
+ hypreal_minus,sumr_add RS sym]) 1);
+qed "sumhr_add_mult_const";
+
+Goalw [hypreal_zero_def]
+ "n < m ==> sumhr (m,n,f) = 0";
+by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
+by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
+by (auto_tac (claset() addEs [FreeUltrafilterNat_subset],
+ simpset() addsimps [sumhr,hypnat_less]));
+qed "sumhr_less_bounds_zero";
+Addsimps [sumhr_less_bounds_zero];
+
+Goal "sumhr(m,n,%i. - f i) = - sumhr(m,n,f)";
+by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
+by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
+by (auto_tac (claset(),simpset() addsimps [sumhr,
+ hypreal_minus,sumr_minus]));
+qed "sumhr_minus";
+
+Goalw [hypnat_of_nat_def]
+ "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))";
+by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
+by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
+by (auto_tac (claset(),simpset() addsimps [sumhr,
+ hypnat_add,sumr_shift_bounds]));
+qed "sumhr_shift_bounds";
+
+(*------------------------------------------------------------------
+ Theorems about NS sums - infinite sums are obtained
+ by summing to some infinite hypernatural (such as whn)
+ -----------------------------------------------------------------*)
+Goalw [hypnat_omega_def,hypnat_zero_def]
+ "sumhr(0,whn,%i. #1) = hypreal_of_hypnat whn";
+by (auto_tac (claset(),simpset() addsimps [sumhr,
+ hypreal_of_hypnat]));
+qed "sumhr_hypreal_of_hypnat_omega";
+
+Goalw [hypnat_omega_def,hypnat_zero_def,
+ hypreal_one_def,omega_def]
+ "sumhr(0,whn,%i. #1) = whr + -1hr";
+by (auto_tac (claset(),simpset() addsimps [sumhr,
+ real_of_nat_def,hypreal_minus,hypreal_add]));
+qed "sumhr_hypreal_omega_minus_one";
+
+(***??SERIES.ML??replace old versions???*)
+Goal "sumr 0 (#2*n) (%i. (#-1) ^ Suc i) = #0";
+by (induct_tac "n" 1);
+by (Auto_tac);
+qed "sumr_minus_one_realpow_zero";
+Addsimps [sumr_minus_one_realpow_zero];
+
+Goalw [hypnat_zero_def, hypnat_omega_def, hypreal_zero_def]
+ "sumhr(0, whn + whn, %i. (-#1) ^ (i+1)) = 0";
+by (simp_tac (simpset() addsimps [sumhr,hypnat_add]
+ delsimps [realpow_Suc]) 1);
+qed "sumhr_minus_one_realpow_zero";
+Addsimps [sumhr_minus_one_realpow_zero];
+
+Goalw [hypnat_of_nat_def,hypreal_of_real_def]
+ "(ALL n. m <= Suc n --> f n = r) & m <= na \
+\ ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = \
+\ (hypreal_of_nat (na - m) * hypreal_of_real r)";
+by (auto_tac (claset() addSDs [sumr_interval_const],
+ simpset() addsimps [sumhr,hypreal_of_nat_real_of_nat,
+ hypreal_of_real_def,hypreal_mult]));
+qed "sumhr_interval_const";
+
+Goalw [hypnat_zero_def]
+ "(*fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)";
+by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
+by (asm_full_simp_tac (simpset() addsimps [starfunNat,sumhr]) 1);
+qed "starfunNat_sumr";
+
+Goal "sumhr (0, M, f) @= sumhr (0, N, f) \
+\ ==> abs (sumhr (M, N, f)) @= 0";
+by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1);
+by (auto_tac (claset(),simpset() addsimps [inf_close_refl]));
+by (dtac (inf_close_sym RS (inf_close_minus_iff RS iffD1)) 1);
+by (auto_tac (claset() addDs [inf_close_hrabs],
+ simpset() addsimps [sumhr_split_add_minus]));
+qed "sumhr_hrabs_inf_close";
+Addsimps [sumhr_hrabs_inf_close];
+
+(*----------------------------------------------------------------
+ infinite sums: Standard and NS theorems
+ ----------------------------------------------------------------*)
+Goalw [sums_def,NSsums_def] "(f sums l) = (f NSsums l)";
+by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
+qed "sums_NSsums_iff";
+
+Goalw [summable_def,NSsummable_def]
+ "(summable f) = (NSsummable f)";
+by (simp_tac (simpset() addsimps [sums_NSsums_iff]) 1);
+qed "summable_NSsummable_iff";
+
+Goalw [suminf_def,NSsuminf_def]
+ "(suminf f) = (NSsuminf f)";
+by (simp_tac (simpset() addsimps [sums_NSsums_iff]) 1);
+qed "suminf_NSsuminf_iff";
+
+Goalw [NSsums_def,NSsummable_def]
+ "f NSsums l ==> NSsummable f";
+by (Blast_tac 1);
+qed "NSsums_NSsummable";
+
+Goalw [NSsummable_def,NSsuminf_def]
+ "NSsummable f ==> f NSsums (NSsuminf f)";
+by (blast_tac (claset() addIs [someI2]) 1);
+qed "NSsummable_NSsums";
+
+Goal "f NSsums s ==> (s = NSsuminf f)";
+by (asm_full_simp_tac
+ (simpset() addsimps [suminf_NSsuminf_iff RS sym,sums_NSsums_iff,
+ sums_unique]) 1);
+qed "NSsums_unique";
+
+Goal "ALL m. n <= Suc m --> f(m) = #0 ==> f NSsums (sumr 0 n f)";
+by (asm_simp_tac (simpset() addsimps [sums_NSsums_iff RS sym, series_zero]) 1);
+qed "NSseries_zero";
+
+Goal "NSsummable f = \
+\ (ALL M: HNatInfinite. ALL N: HNatInfinite. abs (sumhr(M,N,f)) @= 0)";
+by (auto_tac (claset(),
+ simpset() addsimps [summable_NSsummable_iff RS sym,
+ summable_convergent_sumr_iff, convergent_NSconvergent_iff,
+ NSCauchy_NSconvergent_iff RS sym, NSCauchy_def,
+ starfunNat_sumr]));
+by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1);
+by (auto_tac (claset(), simpset() addsimps [inf_close_refl]));
+by (rtac ((inf_close_minus_iff RS iffD2) RS inf_close_sym) 1);
+by (rtac (inf_close_minus_iff RS iffD2) 2);
+by (auto_tac (claset() addDs [inf_close_hrabs_zero_cancel],
+ simpset() addsimps [sumhr_split_add_minus]));
+qed "NSsummable_NSCauchy";
+
+(*-------------------------------------------------------------------
+ Terms of a convergent series tend to zero
+ -------------------------------------------------------------------*)
+Goalw [NSLIMSEQ_def] "NSsummable f ==> f ----NS> #0";
+by (auto_tac (claset(), simpset() addsimps [NSsummable_NSCauchy]));
+by (dtac bspec 1 THEN Auto_tac);
+by (dres_inst_tac [("x","N + 1hn")] bspec 1);
+by (auto_tac (claset() addIs [HNatInfinite_add_one,
+ inf_close_hrabs_zero_cancel],
+ simpset() addsimps [rename_numerals hypreal_of_real_zero]));
+qed "NSsummable_NSLIMSEQ_zero";
+
+(* Easy to prove stsandard case now *)
+Goal "summable f ==> f ----> #0";
+by (auto_tac (claset(),
+ simpset() addsimps [summable_NSsummable_iff,
+ LIMSEQ_NSLIMSEQ_iff, NSsummable_NSLIMSEQ_zero]));
+qed "summable_LIMSEQ_zero";
+
+(*-------------------------------------------------------------------
+ NS Comparison test
+ -------------------------------------------------------------------*)
+
+Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \
+\ NSsummable g \
+\ |] ==> NSsummable f";
+by (auto_tac (claset() addIs [summable_comparison_test],
+ simpset() addsimps [summable_NSsummable_iff RS sym]));
+qed "NSsummable_comparison_test";
+
+Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \
+\ NSsummable g \
+\ |] ==> NSsummable (%k. abs (f k))";
+by (rtac NSsummable_comparison_test 1);
+by (auto_tac (claset(), simpset() addsimps [abs_idempotent]));
+qed "NSsummable_rabs_comparison_test";
+
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/Hyperreal/HSeries.thy Mon Dec 18 12:23:54 2000 +0100
@@ -0,0 +1,30 @@
+(* Title : HSeries.thy
+ Author : Jacques D. Fleuriot
+ Copyright : 1998 University of Cambridge
+ Description : Finite summation and infinite series
+ for hyperreals
+*)
+
+HSeries = Series +
+
+consts
+ sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
+
+defs
+ sumhr_def
+ "sumhr p
+ == Abs_hypreal(UN X:Rep_hypnat(fst p).
+ UN Y: Rep_hypnat(fst(snd p)).
+ hyprel ^^{%n::nat. sumr (X n) (Y n) (snd(snd p))})"
+
+constdefs
+ NSsums :: [nat=>real,real] => bool (infixr 80)
+ "f NSsums s == (%n. sumr 0 n f) ----NS> s"
+
+ NSsummable :: (nat=>real) => bool
+ "NSsummable f == (EX s. f NSsums s)"
+
+ NSsuminf :: (nat=>real) => real
+ "NSsuminf f == (@s. f NSsums s)"
+
+end
--- a/src/HOL/Real/Hyperreal/HyperDef.ML Mon Dec 18 12:21:54 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML Mon Dec 18 12:23:54 2000 +0100
@@ -1147,6 +1147,62 @@
simpset() addsimps [hypreal_of_real_one, hypreal_of_real_mult RS sym]));
qed "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);
+qed "hypreal_of_real_divide";
+
+
+(*** Division lemmas ***)
+
+Goal "(0::hypreal)/x = 0";
+by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
+qed "hypreal_zero_divide";
+
+Goal "x/1hr = x";
+by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
+qed "hypreal_divide_one";
+Addsimps [hypreal_zero_divide, hypreal_divide_one];
+
+Goal "(x::hypreal) * (y/z) = (x*y)/z";
+by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 1);
+qed "hypreal_times_divide1_eq";
+
+Goal "(y/z) * (x::hypreal) = (y*x)/z";
+by (simp_tac (simpset() addsimps [hypreal_divide_def]@hypreal_mult_ac) 1);
+qed "hypreal_times_divide2_eq";
+
+Addsimps [hypreal_times_divide1_eq, hypreal_times_divide2_eq];
+
+Goal "(x::hypreal) / (y/z) = (x*z)/y";
+by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib]@
+ hypreal_mult_ac) 1);
+qed "hypreal_divide_divide1_eq";
+
+Goal "((x::hypreal) / y) / z = x/(y*z)";
+by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib,
+ hypreal_mult_assoc]) 1);
+qed "hypreal_divide_divide2_eq";
+
+Addsimps [hypreal_divide_divide1_eq, hypreal_divide_divide2_eq];
+
+(** As with multiplication, pull minus signs OUT of the / operator **)
+
+Goal "(-x) / (y::hypreal) = - (x/y)";
+by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
+qed "hypreal_minus_divide_eq";
+Addsimps [hypreal_minus_divide_eq];
+
+Goal "(x / -(y::hypreal)) = - (x/y)";
+by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_minus_inverse]) 1);
+qed "hypreal_divide_minus_eq";
+Addsimps [hypreal_divide_minus_eq];
+
+Goal "(x+y)/(z::hypreal) = x/z + y/z";
+by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_add_mult_distrib]) 1);
+qed "hypreal_add_divide_distrib";
+
+
Goal "x+x=x*(1hr+1hr)";
by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1);
qed "hypreal_add_self";
--- a/src/HOL/Real/Hyperreal/Hyperreal.thy Mon Dec 18 12:21:54 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Hyperreal.thy Mon Dec 18 12:23:54 2000 +0100
@@ -1,4 +1,4 @@
-theory Hyperreal = Series:
+theory Hyperreal = HSeries:
end
--- a/src/HOL/Real/Hyperreal/Lim.ML Mon Dec 18 12:21:54 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Lim.ML Mon Dec 18 12:23:54 2000 +0100
@@ -10,27 +10,24 @@
fun ARITH_PROVE str = prove_goal thy str
(fn prems => [cut_facts_tac prems 1,arith_tac 1]);
+
+
+(***?REALARITH.ML?? also below??*)
Goal "(x + - a = (#0::real)) = (x=a)";
by (arith_tac 1);
qed "real_add_minus_iff";
Addsimps [real_add_minus_iff];
+Goal "(-b = -a) = (b = (a::real))";
+by (arith_tac 1);
+qed "real_minus_eq_cancel";
+Addsimps [real_minus_eq_cancel];
+
+
(*---------------------------------------------------------------
Theory of limits, continuity and differentiation of
real=>real functions
----------------------------------------------------------------*)
-Goalw [LIM_def] "(f -- a --> L) = (ALL r. #0 < r --> \
-\ (EX s. #0 < s & (ALL x. (x ~= a & (abs(x + -a) < s) \
-\ --> abs(f x + -L) < r))))";
-by Auto_tac;
-qed "LIM_iff";
-
-Goalw [LIM_def]
- "[| f -- a --> L; #0 < r |] \
-\ ==> (EX s. #0 < s & (ALL x. (x ~= a \
-\ & (abs(x + -a) < s) --> abs(f x + -L) < r)))";
-by Auto_tac;
-qed "LIMD";
Goalw [LIM_def] "(%x. k) -- x --> k";
by Auto_tac;
@@ -882,7 +879,6 @@
by (dres_inst_tac [("x","x + -a")] spec 1);
by (dres_inst_tac [("x","x + a")] spec 2);
by (auto_tac (claset(), simpset() addsimps real_add_ac));
-by (arith_tac 1);
qed "DERIV_LIM_iff";
Goalw [deriv_def] "(DERIV f x :> D) = \
@@ -897,7 +893,6 @@
First NSDERIV in terms of NSLIM
-------------------------------------------*)
-Addsimps [starfun_Id]; (*???????Star.ML?????*)
(*--- first equivalence ---*)
Goalw [nsderiv_def,NSLIM_def]
"(NSDERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- #0 --NS> D)";
@@ -930,29 +925,37 @@
Addsimps [inf_close_refl];
-(*FIXME: replace both of these by simprocs for cancellation of common factors*)
-Goal "h ~= (0::hypreal) ==> (x/h)*h = x";
+(*FIXME: replace by simprocs for cancellation of common factors*)
+Goal "h ~= (0::hypreal) ==> x*h/h = x";
by (asm_simp_tac
(simpset() addsimps [hypreal_divide_def, hypreal_mult_inverse_left,
hypreal_mult_assoc]) 1);
qed "hypreal_divide_mult_self_eq";
Addsimps [hypreal_divide_mult_self_eq];
-Goal "h ~= (0::real) ==> (x/h)*h = x";
-by (asm_full_simp_tac
- (simpset() addsimps [real_divide_def, real_mult_inv_left,
- real_mult_assoc]) 1);
-qed "real_divide_mult_self_eq";
-Addsimps [real_divide_mult_self_eq];
+(*FIXME: replace by simprocs for cancellation of common factors*)
+Goal "h ~= (0::hypreal) ==> (h*x)/h = x";
+by (asm_simp_tac
+ (simpset() addsimps [inst "z" "h" hypreal_mult_commute]) 1);
+qed "hypreal_times_divide_self_eq";
+Addsimps [hypreal_times_divide_self_eq];
+
+(*FIXME: replace by simprocs for cancellation of common factors*)
+Goal "h ~= (0::hypreal) ==> h/h = 1hr";
+by (asm_simp_tac
+ (simpset() addsimps [hypreal_divide_def, hypreal_mult_inverse_left]) 1);
+qed "hypreal_divide_self_eq";
+Addsimps [hypreal_divide_self_eq];
+
Goal "(NSDERIV f x :> D) ==> \
\ (ALL xa. \
\ xa @= hypreal_of_real x --> \
\ (*f* (%z. f z - f x)) xa @= hypreal_of_real D * (xa - hypreal_of_real x))";
-by (auto_tac (claset(),simpset() addsimps [NSDERIV_iff2]));
+by (auto_tac (claset(), simpset() addsimps [NSDERIV_iff2]));
by (case_tac "xa = 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, hypreal_of_real_zero]));
by (dres_inst_tac [("x","xa")] spec 1);
by Auto_tac;
by (dres_inst_tac [("c","xa - hypreal_of_real x"),("b","hypreal_of_real D")]
@@ -962,10 +965,10 @@
by (rotate_tac ~1 2);
by (auto_tac (claset(),
simpset() addsimps [starfun_divide RS sym,
- starfun_add RS sym, real_diff_def,
- hypreal_of_real_minus, hypreal_diff_def,
- (inf_close_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2),
- Infinitesimal_subset_HFinite RS subsetD]));
+ starfun_add RS sym, real_diff_def,
+ hypreal_of_real_minus, hypreal_diff_def,
+ (inf_close_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2),
+ Infinitesimal_subset_HFinite RS subsetD]));
qed "NSDERIVD5";
Goal "(NSDERIV f x :> D) ==> \
@@ -1057,52 +1060,6 @@
----------------------------------------------------*)
-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);
-qed "hypreal_of_real_divide"; (**??????HYPERDEF.ML??????*)
-
-
-(**??????HYPERDEF.ML???after inverse_distrib???*)
-Goal "(x::hypreal) * (y/z) = (x*y)/z";
-by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 1);
-qed "hypreal_times_divide1_eq";
-
-Goal "(y/z) * (x::hypreal) = (y*x)/z";
-by (simp_tac (simpset() addsimps [hypreal_divide_def]@hypreal_mult_ac) 1);
-qed "hypreal_times_divide2_eq";
-
-Addsimps [hypreal_times_divide1_eq, hypreal_times_divide2_eq];
-
-Goal "(x::hypreal) / (y/z) = (x*z)/y";
-by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib]@
- hypreal_mult_ac) 1);
-qed "hypreal_divide_divide1_eq";
-
-Goal "((x::hypreal) / y) / z = x/(y*z)";
-by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib,
- hypreal_mult_assoc]) 1);
-qed "hypreal_divide_divide2_eq";
-
-Addsimps [hypreal_divide_divide1_eq, hypreal_divide_divide2_eq];
-
-(** As with multiplication, pull minus signs OUT of the / operator **)
-
-Goal "(-x) / (y::hypreal) = - (x/y)";
-by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
-qed "hypreal_minus_divide_eq";
-Addsimps [hypreal_minus_divide_eq];
-
-Goal "(x / -(y::hypreal)) = - (x/y)";
-by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_minus_inverse]) 1);
-qed "hypreal_divide_minus_eq";
-Addsimps [hypreal_divide_minus_eq];
-
-Goal "(x+y)/(z::hypreal) = x/z + y/z";
-by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_add_mult_distrib]) 1);
-qed "hypreal_add_divide_distrib";
-
-
Goal "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] \
\ ==> NSDERIV (%x. f x + g x) x :> Da + Db";
by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff,
@@ -1134,21 +1091,6 @@
real_minus_mult_eq2 RS sym,real_mult_commute]) 1);
val lemma_nsderiv1 = result();
-(*FIXME: replace both of these by simprocs for cancellation of common factors*)
-Goal "h ~= (0::hypreal) ==> (x*h)/h = x";
-by (asm_simp_tac
- (simpset() addsimps [hypreal_divide_def, hypreal_mult_inverse_left,
- hypreal_mult_assoc]) 1);
-qed "hypreal_divide_mult2_self_eq";
-Addsimps [hypreal_divide_mult2_self_eq];
-
-Goal "h ~= (0::real) ==> (x*h)/h = x";
-by (asm_full_simp_tac
- (simpset() addsimps [real_divide_def, real_mult_inv_left,
- real_mult_assoc]) 1);
-qed "real_divide_mult2_self_eq";
-Addsimps [real_divide_mult2_self_eq];
-
Goal "[| (x + y) / z = hypreal_of_real D + yb; z ~= 0; \
\ z : Infinitesimal; yb : Infinitesimal |] \
\ ==> x + y @= 0";
@@ -1280,13 +1222,6 @@
by (etac (NSdifferentiableI RS incrementI) 1);
qed "incrementI2";
-(*FIXME: replace by simprocs for cancellation of common factors*)
-Goal "h ~= (0::hypreal) ==> h/h = 1hr";
-by (asm_simp_tac
- (simpset() addsimps [hypreal_divide_def, hypreal_mult_inverse_left]) 1);
-qed "hypreal_divide_self_eq";
-Addsimps [hypreal_divide_self_eq];
-
(* The Increment theorem -- Keisler p. 65 *)
Goal "[| NSDERIV f x :> D; h: Infinitesimal; h ~= 0 |] \
\ ==> EX e: Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h";
@@ -1328,16 +1263,6 @@
manipulation of terms.
--------------------------------------------------------------*)
-(*???HYPERDEF.ML???*)
-Goal "(0::hypreal)/x = 0";
-by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
-qed "hypreal_zero_divide";
-
-Goal "x/1hr = x";
-by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
-qed "hypreal_divide_one";
-Addsimps [hypreal_zero_divide, hypreal_divide_one];
-
(* lemmas *)
Goalw [nsderiv_def]
"[| NSDERIV g x :> D; \
@@ -1489,13 +1414,6 @@
---------------------------------------------------------------*)
-(*FIXME: replace by simprocs for cancellation of common factors*)
-Goal "h ~= (0::hypreal) ==> (h*x)/h = x";
-by (asm_simp_tac
- (simpset() addsimps [inst "z" "h" hypreal_mult_commute]) 1);
-qed "hypreal_times_divide_self_eq";
-Addsimps [hypreal_times_divide_self_eq];
-
(*Can't get rid of x ~= #0 because it isn't continuous at zero*)
Goalw [nsderiv_def]
"x ~= #0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))";
@@ -1530,7 +1448,7 @@
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 [thm "realpow_Suc"]) 1);
+ NSDERIV_DERIV_iff RS sym] delsimps [realpow_Suc]) 1);
qed "DERIV_inverse";
(*--------------------------------------------------------------
@@ -1540,7 +1458,7 @@
\ ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))";
by (rtac (real_mult_commute RS subst) 1);
by (asm_simp_tac (simpset() addsimps [real_minus_mult_eq1,
- realpow_inverse] delsimps [thm "realpow_Suc",
+ realpow_inverse] delsimps [realpow_Suc,
real_minus_mult_eq1 RS sym]) 1);
by (fold_goals_tac [o_def]);
by (blast_tac (claset() addSIs [DERIV_chain,DERIV_inverse]) 1);
@@ -1549,7 +1467,7 @@
Goal "[| NSDERIV f x :> d; f(x) ~= #0 |] \
\ ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))";
by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff,
- DERIV_inverse_fun] delsimps [thm "realpow_Suc"]) 1);
+ DERIV_inverse_fun] delsimps [realpow_Suc]) 1);
qed "NSDERIV_inverse_fun";
(*--------------------------------------------------------------
@@ -1563,7 +1481,7 @@
by (asm_full_simp_tac
(simpset() addsimps [real_divide_def, real_add_mult_distrib2,
realpow_inverse,real_minus_mult_eq1] @ real_mult_ac
- delsimps [thm "realpow_Suc", real_minus_mult_eq1 RS sym,
+ delsimps [realpow_Suc, real_minus_mult_eq1 RS sym,
real_minus_mult_eq2 RS sym]) 1);
qed "DERIV_quotient";
@@ -1571,7 +1489,7 @@
\ ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) \
\ + -(e*f(x))) / (g(x) ^ 2)";
by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff,
- DERIV_quotient] delsimps [thm "realpow_Suc"]) 1);
+ DERIV_quotient] delsimps [realpow_Suc]) 1);
qed "NSDERIV_quotient";
(* ------------------------------------------------------------------------ *)
@@ -1600,15 +1518,14 @@
Goal "(ALL z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l \
\ ==> NSDERIV f x :> l";
by (auto_tac (claset(),
- simpset() addsimps [NSDERIV_iff2, starfun_mult RS sym,
+ simpset() delsimprocs real_cancel_factor
+ addsimps [NSDERIV_iff2, starfun_mult RS sym,
starfun_divide RS sym]));
by (auto_tac (claset(),
simpset() addsimps [hypreal_mult_assoc,
starfun_diff RS sym]));
by (asm_full_simp_tac (simpset() addsimps [hypreal_eq_minus_iff3 RS sym,
hypreal_diff_def]) 1);
-by (dtac (CLAIM_SIMP "x ~= y ==> x - y ~= (0::hypreal)" [hypreal_eq_minus_iff3 RS sym,
- hypreal_diff_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [isNSCont_def]) 1);
qed "CARAT_DERIVD";
@@ -1624,60 +1541,77 @@
qed_spec_mp "lemma_f_mono_add";
-(* IMPROVE?: long proof! *)
+Goal "[| ALL n. f(n) <= f(Suc n); \
+\ ALL n. g(Suc n) <= g(n); \
+\ ALL n. f(n) <= g(n) |] \
+\ ==> Bseq f";
+by (res_inst_tac [("k","f 0"),("K","g 0")] BseqI2 1 THEN rtac allI 1);
+by (induct_tac "n" 1);
+by (auto_tac (claset() addIs [real_le_trans], simpset()));
+by (res_inst_tac [("j","g(Suc na)")] real_le_trans 1);
+by (induct_tac "na" 2);
+by (auto_tac (claset() addIs [real_le_trans], simpset()));
+qed "f_inc_g_dec_Beq_f";
+
+Goal "[| ALL n. f(n) <= f(Suc n); \
+\ ALL n. g(Suc n) <= g(n); \
+\ ALL n. f(n) <= g(n) |] \
+\ ==> Bseq g";
+by (stac (Bseq_minus_iff RS sym) 1);
+by (res_inst_tac [("g","%x. -(f x)")] f_inc_g_dec_Beq_f 1);
+by Auto_tac;
+qed "f_inc_g_dec_Beq_g";
+
+Goal "[| ALL n. f n <= f (Suc n); convergent f |] ==> f n <= lim f";
+by (rtac real_leI 1);
+by (auto_tac (claset(),
+ simpset() addsimps [convergent_LIMSEQ_iff, LIMSEQ_iff, monoseq_Suc]));
+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<=na --> ?Q na"),("x","no + n")] spec 2);
+by Auto_tac;
+by (subgoal_tac "lim f <= f(no + n)" 1);
+by (induct_tac "no" 2);
+by (auto_tac (claset() addIs [real_le_trans],
+ simpset() addsimps [real_diff_def, abs_real_def]));
+by (dres_inst_tac [("i","f(no + n)"),("no1","no")]
+ (lemma_f_mono_add RSN (2,real_less_le_trans)) 1);
+by (auto_tac (claset(), simpset() addsimps [add_commute]));
+qed "f_inc_imp_le_lim";
+
+Goal "convergent g ==> lim (%x. - g x) = - (lim g)";
+by (rtac (LIMSEQ_minus RS limI) 1);
+by (asm_full_simp_tac (simpset() addsimps [convergent_LIMSEQ_iff]) 1);
+qed "lim_uminus";
+
+Goal "[| ALL n. g(Suc n) <= g(n); convergent g |] ==> lim g <= g n";
+by (subgoal_tac "- (g n) <= - (lim g)" 1);
+by (cut_inst_tac [("f", "%x. - (g x)")] f_inc_imp_le_lim 2);
+by (auto_tac (claset(),
+ simpset() addsimps [lim_uminus, convergent_minus_iff RS sym]));
+qed "g_dec_imp_lim_le";
+
Goal "[| ALL n. f(n) <= f(Suc n); \
\ ALL n. g(Suc n) <= g(n); \
\ ALL n. f(n) <= g(n) |] \
\ ==> EX l m. l <= m & ((ALL n. f(n) <= l) & f ----> l) & \
\ ((ALL n. m <= g(n)) & g ----> m)";
-by (subgoal_tac "Bseq f" 1);
-by (res_inst_tac [("k","f 0"),("K","g 0")] BseqI2 2 THEN rtac allI 2);
-by (induct_tac "n" 2);
-by (auto_tac (claset() addIs [real_le_trans],simpset()));
-by (res_inst_tac [("j","g(Suc na)")] real_le_trans 2);
-by (induct_tac "na" 3);
-by (auto_tac (claset() addIs [real_le_trans],simpset()));
-by (subgoal_tac "monoseq f" 1);
-by (subgoal_tac "monoseq g" 1);
-by (subgoal_tac "Bseq g" 1);
-by (res_inst_tac [("k","f 0"),("K","g 0")] BseqI2 2 THEN rtac allI 2);
-by (induct_tac "n" 2);
-by (auto_tac (claset() addIs [real_le_trans],simpset()));
-by (res_inst_tac [("j","f(Suc na)")] real_le_trans 2);
-by (induct_tac "na" 2);
-by (auto_tac (claset() addIs [real_le_trans],simpset()));
+by (subgoal_tac "monoseq f & monoseq g" 1);
+by (force_tac (claset(), simpset() addsimps [LIMSEQ_iff,monoseq_Suc]) 2);
+by (subgoal_tac "Bseq f & Bseq g" 1);
+by (blast_tac (claset() addIs [f_inc_g_dec_Beq_f, f_inc_g_dec_Beq_g]) 2);
by (auto_tac (claset() addSDs [Bseq_monoseq_convergent],
- simpset() addsimps [convergent_LIMSEQ_iff]));
+ simpset() addsimps [convergent_LIMSEQ_iff]));
by (res_inst_tac [("x","lim f")] exI 1);
by (res_inst_tac [("x","lim g")] exI 1);
-by (auto_tac (claset() addIs [LIMSEQ_le],simpset()));
-by (rtac real_leI 1 THEN rtac real_leI 2);
-by (auto_tac (claset(),simpset() addsimps [LIMSEQ_iff,monoseq_Suc]));
-by (ALLGOALS (dtac real_less_sum_gt_zero));
-by (dres_inst_tac [("x","f n + - lim f")] spec 1);
-by (rotate_tac 4 2);
-by (dres_inst_tac [("x","lim g + - g n")] spec 2);
-by (Step_tac 1);
-by (ALLGOALS(rotate_tac 5));
-by (ALLGOALS(dres_inst_tac [("x","no + n")] spec));
-by (Auto_tac);
-by (subgoal_tac "0 <= f(no + n) - lim f" 1);
-by (induct_tac "no" 2);
-by (auto_tac (claset() addIs [real_le_trans],
- simpset() addsimps [real_diff_def]));
-by (asm_full_simp_tac (simpset() addsimps [inst "r" "f ?x + ?y" abs_real_def]) 1);
-by (dres_inst_tac [("i"," f (no + n)"),("no1","no")]
- (lemma_f_mono_add RSN (2,real_less_le_trans)) 1);
-by (subgoal_tac "g(no + n) <= lim g" 3);
-by (induct_tac "no" 4);
-by (auto_tac (claset() addIs [real_le_trans],
- simpset() addsimps [real_diff_def,abs_minus_add_cancel]));
-by (asm_full_simp_tac (simpset() addsimps [inst "r" "lim g + ?y" abs_real_def]) 2);
-by (cut_inst_tac [("f", "%x. -(g x)"), ("m","n"), ("no","no")]
- lemma_f_mono_add 2);
-by (auto_tac (claset(), simpset() addsimps [add_commute]));
+by (auto_tac (claset() addIs [LIMSEQ_le], simpset()));
+by (auto_tac (claset(),
+ simpset() addsimps [f_inc_imp_le_lim, g_dec_imp_lim_le,
+ convergent_LIMSEQ_iff]));
qed "lemma_nest";
+
Goal "[| ALL n. f(n) <= f(Suc n); \
\ ALL n. g(Suc n) <= g(n); \
\ ALL n. f(n) <= g(n); \
@@ -1687,7 +1621,7 @@
by (dtac lemma_nest 1 THEN Auto_tac);
by (subgoal_tac "l = m" 1);
by (dres_inst_tac [("X","f")] LIMSEQ_diff 2);
-by (auto_tac (claset() addIs [LIMSEQ_unique],simpset()));
+by (auto_tac (claset() addIs [LIMSEQ_unique], simpset()));
qed "lemma_nest_unique";
Goal "EX! fn. (fn 0 = e) & (ALL n. fn (Suc n) = f n (fn n))";
@@ -1700,7 +1634,6 @@
qed "nat_Axiom";
-(*?????????OBSOLETE????????***)
Goal "((x::real) = y / (#2 * z)) = (#2 * x = y/z)";
by Auto_tac;
by (dres_inst_tac [("f","%u. (#1/#2)*u")] arg_cong 1);
@@ -2267,24 +2200,6 @@
(* Mean value theorem *)
(*----------------------------------------------------------------------------*)
-
-(*????????TO BE OBSOLETE?????????*)
-Goal "k~=#0 ==> (k*m) / k = (m::real)";
-by (dres_inst_tac [("n","#1")] real_mult_div_cancel1 1);
-by (Asm_full_simp_tac 1);
-qed "real_mult_div_self1";
-Addsimps [real_mult_div_self1];
-
-
-(**???FIXME: replace by simproc*??*)
-Goal "h ~= (0::real) ==> (h*x)/h = x";
-by (asm_full_simp_tac
- (simpset() addsimps [real_divide_mult2_self_eq,
- real_mult_commute]) 1);
-qed "real_divide_mult3_self_eq";
-Delsimps [real_divide_mult3_self_eq];
-
-
Goal "f a - (f b - f a)/(b - a) * a = \
\ f b - (f b - f a)/(b - a) * (b::real)";
by (case_tac "a = b" 1);
@@ -2292,8 +2207,258 @@
by (res_inst_tac [("c1","b - a")] (real_mult_left_cancel RS iffD1) 1);
by (arith_tac 1);
by (auto_tac (claset(),
- simpset() addsimps [real_diff_mult_distrib2, real_diff_eq_eq,
- inst "a" "a" eq_commute]));
+ simpset() addsimps [real_diff_mult_distrib2]));
by (auto_tac (claset(),
- simpset() addsimps [real_diff_mult_distrib2, real_mult_commute]));
+ simpset() addsimps [real_diff_mult_distrib]));
qed "lemma_MVT";
+
+Goal "[| a < b; \
+\ ALL x. a <= x & x <= b --> isCont f x; \
+\ ALL x. a < x & x < b --> f differentiable x |] \
+\ ==> EX l z. a < z & z < b & DERIV f z :> l & \
+\ (f(b) - f(a) = (b - a) * l)";
+by (dres_inst_tac [("f","%x. f(x) - (((f(b) - f(a)) / (b - a)) * x)")]
+ Rolle 1);
+by (rtac lemma_MVT 1);
+by (Step_tac 1);
+by (rtac isCont_diff 1 THEN Blast_tac 1);
+by (rtac (isCont_const RS isCont_mult) 1);
+by (rtac isCont_Id 1);
+by (dres_inst_tac [("P", "%x. ?Pre x --> f differentiable x"),
+ ("x","x")] spec 1);
+by (asm_full_simp_tac (simpset() addsimps [differentiable_def]) 1);
+by (Step_tac 1);
+by (res_inst_tac [("x","xa - ((f(b) - f(a)) / (b - a))")] exI 1);
+by (rtac DERIV_diff 1 THEN assume_tac 1);
+(*derivative of a linear function is the constant...*)
+by (subgoal_tac "(%x. (f b - f a) * x / (b - a)) = \
+\ op * ((f b - f a) / (b - a))" 1);
+by (rtac ext 2 THEN Simp_tac 2);
+by (Asm_full_simp_tac 1);
+(*final case*)
+by (res_inst_tac [("x","((f(b) - f(a)) / (b - a))")] exI 1);
+by (res_inst_tac [("x","z")] exI 1);
+by (Step_tac 1);
+by (Asm_full_simp_tac 2);
+by (subgoal_tac "DERIV (%x. ((f(b) - f(a)) / (b - a)) * x) z :> \
+\ ((f(b) - f(a)) / (b - a))" 1);
+by (rtac DERIV_cmult_Id 2);
+by (dtac DERIV_add 1 THEN assume_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [real_add_assoc, real_diff_def]) 1);
+qed "MVT";
+
+(*----------------------------------------------------------------------------*)
+(* Theorem that function is constant if its derivative is 0 over an interval. *)
+(*----------------------------------------------------------------------------*)
+
+Goal "[| a < b; \
+\ ALL x. a <= x & x <= b --> isCont f x; \
+\ ALL 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);
+by (auto_tac (claset() addSDs [DERIV_unique],simpset()
+ addsimps [real_diff_eq_eq]));
+qed "DERIV_isconst_end";
+
+Goal "[| a < b; \
+\ ALL x. a <= x & x <= b --> isCont f x; \
+\ ALL x. a < x & x < b --> DERIV f x :> #0 |] \
+\ ==> ALL x. a <= x & x <= b --> f x = f a";
+by (Step_tac 1);
+by (dres_inst_tac [("x","a")] real_le_imp_less_or_eq 1);
+by (Step_tac 1);
+by (dres_inst_tac [("b","x")] DERIV_isconst_end 1);
+by (Auto_tac);
+qed "DERIV_isconst1";
+
+Goal "[| a < b; \
+\ ALL x. a <= x & x <= b --> isCont f x; \
+\ ALL x. a < x & x < b --> DERIV f x :> #0; \
+\ a <= x; x <= b |] \
+\ ==> f x = f a";
+by (blast_tac (claset() addDs [DERIV_isconst1]) 1);
+qed "DERIV_isconst2";
+
+Goal "ALL 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()));
+qed "DERIV_isconst_all";
+
+Goal "[|a ~= b; ALL x. DERIV f x :> k |] ==> (f(b) - f(a)) = (b - a) * k";
+by (res_inst_tac [("R1.0","a"),("R2.0","b")] real_linear_less2 1);
+by (Auto_tac);
+by (ALLGOALS(dres_inst_tac [("f","f")] MVT));
+by (auto_tac (claset() addDs [DERIV_isCont,DERIV_unique],simpset() addsimps
+ [differentiable_def]));
+by (auto_tac (claset() addDs [DERIV_unique],
+ simpset() addsimps [real_add_mult_distrib, real_diff_def,
+ real_minus_mult_eq1 RS sym]));
+qed "DERIV_const_ratio_const";
+
+Goal "[|a ~= b; ALL x. DERIV f x :> k |] ==> (f(b) - f(a))/(b - a) = k";
+by (res_inst_tac [("c1","b - a")] (real_mult_right_cancel RS iffD1) 1);
+by (auto_tac (claset() addSDs [DERIV_const_ratio_const],
+ simpset() addsimps [real_mult_assoc]));
+qed "DERIV_const_ratio_const2";
+
+Goal "((a + b) /#2 - a) = (b - a)/(#2::real)";
+by Auto_tac;
+qed "real_average_minus_first";
+Addsimps [real_average_minus_first];
+
+Goal "((b + a)/#2 - a) = (b - a)/(#2::real)";
+by Auto_tac;
+qed "real_average_minus_second";
+Addsimps [real_average_minus_second];
+
+
+(* Gallileo's "trick": average velocity = av. of end velocities *)
+Goal "[|a ~= (b::real); ALL x. DERIV v x :> k|] \
+\ ==> v((a + b)/#2) = (v a + v b)/#2";
+by (res_inst_tac [("R1.0","a"),("R2.0","b")] real_linear_less2 1);
+by (Auto_tac);
+by (ftac DERIV_const_ratio_const2 1 THEN assume_tac 1);
+by (ftac DERIV_const_ratio_const2 2 THEN assume_tac 2);
+by (dtac real_less_half_sum 1);
+by (dtac real_gt_half_sum 2);
+by (ftac (real_not_refl2 RS DERIV_const_ratio_const2) 1 THEN assume_tac 1);
+by (dtac ((real_not_refl2 RS not_sym) RS DERIV_const_ratio_const2) 2
+ THEN assume_tac 2);
+by (ALLGOALS (dres_inst_tac [("f","%u. (b-a)*u")] arg_cong));
+by (auto_tac (claset(), simpset() addsimps [real_inverse_eq_divide]));
+by (asm_full_simp_tac (simpset() addsimps [real_add_commute, eq_commute]) 1);
+qed "DERIV_const_average";
+
+
+(* ------------------------------------------------------------------------ *)
+(* Dull lemma that an continuous injection on an interval must have a strict*)
+(* maximum at an end point, not in the middle. *)
+(* ------------------------------------------------------------------------ *)
+
+Goal "[|#0 < d; ALL z. abs(z - x) <= d --> g(f z) = z; \
+\ ALL z. abs(z - x) <= d --> isCont f z |] \
+\ ==> ~(ALL z. abs(z - x) <= d --> f(z) <= f(x))";
+by (rtac notI 1);
+by (rotate_tac 3 1);
+by (forw_inst_tac [("x","x - d")] spec 1);
+by (forw_inst_tac [("x","x + d")] spec 1);
+by (Step_tac 1);
+by (cut_inst_tac [("x","f(x - d)"),("y","f(x + d)")]
+ (ARITH_PROVE "x <= y | y <= (x::real)") 4);
+by (etac disjE 4);
+by (REPEAT(arith_tac 1));
+by (cut_inst_tac [("f","f"),("a","x - d"),("b","x"),("y","f(x + d)")]
+ IVT_objl 1);
+by (Step_tac 1);
+by (arith_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [abs_le_interval_iff]) 1);
+by (dres_inst_tac [("f","g")] arg_cong 1);
+by (rotate_tac 2 1);
+by (forw_inst_tac [("x","xa")] spec 1);
+by (dres_inst_tac [("x","x + d")] spec 1);
+by (asm_full_simp_tac (simpset() addsimps [abs_le_interval_iff]) 1);
+(* 2nd case: similar *)
+by (cut_inst_tac [("f","f"),("a","x"),("b","x + d"),("y","f(x - d)")]
+ IVT2_objl 1);
+by (Step_tac 1);
+by (arith_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [abs_le_interval_iff]) 1);
+by (dres_inst_tac [("f","g")] arg_cong 1);
+by (rotate_tac 2 1);
+by (forw_inst_tac [("x","xa")] spec 1);
+by (dres_inst_tac [("x","x - d")] spec 1);
+by (asm_full_simp_tac (simpset() addsimps [abs_le_interval_iff]) 1);
+qed "lemma_isCont_inj";
+
+(* ------------------------------------------------------------------------ *)
+(* Similar version for lower bound *)
+(* ------------------------------------------------------------------------ *)
+
+Goal "[|#0 < d; ALL z. abs(z - x) <= d --> g(f z) = z; \
+\ ALL z. abs(z - x) <= d --> isCont f z |] \
+\ ==> ~(ALL z. abs(z - x) <= d --> f(x) <= f(z))";
+by (auto_tac (claset() addSDs [(asm_full_simplify (simpset())
+ (read_instantiate [("f","%x. - f x"),("g","%y. g(-y)"),("x","x"),("d","d")]
+ lemma_isCont_inj))],simpset() addsimps [isCont_minus]));
+qed "lemma_isCont_inj2";
+
+(* ------------------------------------------------------------------------ *)
+(* Show there's an interval surrounding f(x) in f[[x - d, x + d]] *)
+(* Also from John's theory *)
+(* ------------------------------------------------------------------------ *)
+
+Addsimps [zero_eq_numeral_0,one_eq_numeral_1];
+
+val lemma_le = ARITH_PROVE "#0 <= (d::real) ==> -d <= d";
+
+(* FIXME: awful proof - needs improvement *)
+Goal "[| #0 < d; ALL z. abs(z - x) <= d --> g(f z) = z; \
+\ ALL z. abs(z - x) <= d --> isCont f z |] \
+\ ==> EX e. #0 < e & \
+\ (ALL y. \
+\ abs(y - f(x)) <= e --> \
+\ (EX z. abs(z - x) <= d & (f z = y)))";
+by (ftac real_less_imp_le 1);
+by (dtac (lemma_le RS (asm_full_simplify (simpset()) (read_instantiate
+ [("f","f"),("a","x - d"),("b","x + d")] isCont_Lb_Ub))) 1);
+by (Step_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [abs_le_interval_iff]) 1);
+by (subgoal_tac "L <= f x & f x <= M" 1);
+by (dres_inst_tac [("P", "%v. ?P v --> ?Q v & ?R v"), ("x","x")] spec 2);
+by (Asm_full_simp_tac 2);
+by (subgoal_tac "L < f x & f x < M" 1);
+by (Step_tac 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);
+by (Step_tac 1);
+by (res_inst_tac [("x","e")] exI 1);
+by (Step_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [abs_le_interval_iff]) 1);
+by (dres_inst_tac [("P","%v. ?PP v --> (EX xa. ?Q v xa)"),("x","y")] spec 1);
+by (Step_tac 1 THEN REPEAT(arith_tac 1));
+by (res_inst_tac [("x","xa")] exI 1);
+by (arith_tac 1);
+by (ALLGOALS(etac (ARITH_PROVE "[|x <= y; x ~= y |] ==> x < (y::real)")));
+by (ALLGOALS(rotate_tac 3));
+by (dtac lemma_isCont_inj2 1);
+by (assume_tac 2);
+by (dtac lemma_isCont_inj 3);
+by (assume_tac 4);
+by (TRYALL(assume_tac));
+by (Step_tac 1);
+by (ALLGOALS(dres_inst_tac [("x","z")] spec));
+by (ALLGOALS(arith_tac));
+qed "isCont_inj_range";
+
+
+(* ------------------------------------------------------------------------ *)
+(* Continuity of inverse function *)
+(* ------------------------------------------------------------------------ *)
+
+Goal "[| #0 < d; ALL z. abs(z - x) <= d --> g(f(z)) = z; \
+\ ALL z. abs(z - x) <= d --> isCont f z |] \
+\ ==> isCont g (f x)";
+by (simp_tac (simpset() addsimps [isCont_iff,LIM_def]) 1);
+by (Step_tac 1);
+by (dres_inst_tac [("d1.0","r")] (rename_numerals real_lbound_gt_zero) 1);
+by (assume_tac 1 THEN Step_tac 1);
+by (subgoal_tac "ALL z. abs(z - x) <= e --> (g(f z) = z)" 1);
+by (Force_tac 2);
+by (subgoal_tac "ALL z. abs(z - x) <= e --> isCont f z" 1);
+by (Force_tac 2);
+by (dres_inst_tac [("d","e")] isCont_inj_range 1);
+by (assume_tac 2 THEN assume_tac 1);
+by (Step_tac 1);
+by (res_inst_tac [("x","ea")] exI 1);
+by Auto_tac;
+by (rotate_tac 4 1);
+by (dres_inst_tac [("x","f(x) + xa")] spec 1);
+by Auto_tac;
+by (dtac sym 1 THEN Auto_tac);
+by (arith_tac 1);
+qed "isCont_inverse";
+
--- a/src/HOL/Real/Hyperreal/NSA.ML Mon Dec 18 12:21:54 2000 +0100
+++ b/src/HOL/Real/Hyperreal/NSA.ML Mon Dec 18 12:23:54 2000 +0100
@@ -96,7 +96,7 @@
by (Auto_tac);
qed "SReal_UNIV_real";
-Goalw [SReal_def] "(x: SReal) = (? y. x = hypreal_of_real y)";
+Goalw [SReal_def] "(x: SReal) = (EX y. x = hypreal_of_real y)";
by (Auto_tac);
qed "SReal_iff";
@@ -125,15 +125,15 @@
(*------------------------------------------------------------------
Completeness of SReal
------------------------------------------------------------------*)
-Goal "P <= SReal ==> ((? x:P. y < x) = \
-\ (? X. hypreal_of_real X : P & y < hypreal_of_real X))";
+Goal "P <= SReal ==> ((EX x:P. y < x) = \
+\ (EX X. hypreal_of_real X : P & y < hypreal_of_real X))";
by (blast_tac (claset() addSDs [SReal_iff RS iffD1]) 1);
by (flexflex_tac );
qed "SReal_sup_lemma";
-Goal "[| P <= SReal; ? x. x: P; ? y : SReal. !x: P. x < y |] \
-\ ==> (? X. X: {w. hypreal_of_real w : P}) & \
-\ (? Y. !X: {w. hypreal_of_real w : P}. X < Y)";
+Goal "[| P <= SReal; EX x. x: P; EX y : SReal. ALL x: P. x < y |] \
+\ ==> (EX X. X: {w. hypreal_of_real w : P}) & \
+\ (EX Y. ALL X: {w. hypreal_of_real w : P}. X < Y)";
by (rtac conjI 1);
by (fast_tac (claset() addSDs [SReal_iff RS iffD1]) 1);
by (Auto_tac THEN forward_tac [subsetD] 1 THEN assume_tac 1);
@@ -254,12 +254,12 @@
by (auto_tac (claset() addDs [spec],simpset() addsimps [hrabs_idempotent]));
qed "not_HFinite_hrabs";
-goal NSA.thy "0 : HFinite";
+Goal "0 : HFinite";
by (rtac (SReal_zero RS (SReal_subset_HFinite RS subsetD)) 1);
qed "HFinite_zero";
Addsimps [HFinite_zero];
-goal NSA.thy "1hr : HFinite";
+Goal "1hr : HFinite";
by (rtac (SReal_one RS (SReal_subset_HFinite RS subsetD)) 1);
qed "HFinite_one";
Addsimps [HFinite_one];
@@ -305,11 +305,10 @@
by (full_simp_tac (simpset() addsimps [Infinitesimal_minus_iff RS sym]) 1);
qed "not_Infinitesimal_minus_iff";
-val prem1::prem2::rest =
-goal thy "[| x : Infinitesimal; y : Infinitesimal |] \
-\ ==> (x + -y):Infinitesimal";
-by (full_simp_tac (simpset() addsimps [prem1,prem2,
- (Infinitesimal_minus_iff RS iffD1),Infinitesimal_add]) 1);
+Goal "[| x : Infinitesimal; y : Infinitesimal |] ==> (x + -y):Infinitesimal";
+by (asm_simp_tac
+ (simpset() addsimps [Infinitesimal_minus_iff RS sym,
+ Infinitesimal_add]) 1);
qed "Infinitesimal_add_minus";
Goalw [Infinitesimal_def]
@@ -372,27 +371,24 @@
qed "HInfinite_mult";
Goalw [HInfinite_def]
- "[|x: HInfinite; 0 <= y; 0 <= x|] \
-\ ==> (x + y): HInfinite";
+ "[|x: HInfinite; 0 <= y; 0 <= x|] ==> (x + y): HInfinite";
by (auto_tac (claset() addSIs
[hypreal_add_zero_less_le_mono],
simpset() addsimps [hrabs_eqI1,
hypreal_add_commute,hypreal_le_add_order]));
qed "HInfinite_add_ge_zero";
-Goal "[|x: HInfinite; 0 <= y; 0 <= x|] \
-\ ==> (y + x): HInfinite";
+Goal "[|x: HInfinite; 0 <= y; 0 <= x|] ==> (y + x): HInfinite";
by (auto_tac (claset() addSIs [HInfinite_add_ge_zero],
simpset() addsimps [hypreal_add_commute]));
qed "HInfinite_add_ge_zero2";
-Goal "[|x: HInfinite; 0 < y; 0 < x|] \
-\ ==> (x + y): HInfinite";
+Goal "[|x: HInfinite; 0 < y; 0 < x|] ==> (x + y): HInfinite";
by (blast_tac (claset() addIs [HInfinite_add_ge_zero,
hypreal_less_imp_le]) 1);
qed "HInfinite_add_gt_zero";
-goalw NSA.thy [HInfinite_def]
+Goalw [HInfinite_def]
"(-x: HInfinite) = (x: HInfinite)";
by (auto_tac (claset(),simpset() addsimps
[hrabs_minus_cancel]));
@@ -594,13 +590,13 @@
by (rtac ([prem1,prem2] MRS Infinitesimal_add) 1);
qed "inf_close_add";
-Goal "!!a. a @= b ==> -a @= -b";
+Goal "a @= b ==> -a @= -b";
by (rtac ((inf_close_minus_iff RS iffD2) RS inf_close_sym) 1);
by (dtac (inf_close_minus_iff RS iffD1) 1);
by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
qed "inf_close_minus";
-Goal "!!a. -a @= -b ==> a @= b";
+Goal "-a @= -b ==> a @= b";
by (auto_tac (claset() addDs [inf_close_minus],simpset()));
qed "inf_close_minus2";
@@ -610,17 +606,17 @@
Addsimps [inf_close_minus_cancel];
-Goal "!!a. [| a @= b; c @= d |] ==> a + -c @= b + -d";
+Goal "[| a @= b; c @= d |] ==> a + -c @= b + -d";
by (blast_tac (claset() addSIs [inf_close_add,inf_close_minus]) 1);
qed "inf_close_add_minus";
-Goalw [inf_close_def] "!!a. [| a @= b; c: HFinite|] ==> a*c @= b*c";
+Goalw [inf_close_def] "[| a @= b; c: HFinite|] ==> a*c @= b*c";
by (asm_full_simp_tac (simpset() addsimps [Infinitesimal_HFinite_mult,
hypreal_minus_mult_eq1,hypreal_add_mult_distrib RS sym]
delsimps [hypreal_minus_mult_eq1 RS sym]) 1);
qed "inf_close_mult1";
-Goal "!!a. [|a @= b; c: HFinite|] ==> c*a @= c*b";
+Goal "[|a @= b; c: HFinite|] ==> c*a @= c*b";
by (asm_simp_tac (simpset() addsimps [inf_close_mult1,hypreal_mult_commute]) 1);
qed "inf_close_mult2";
@@ -630,19 +626,19 @@
([prem2,prem3] MRS inf_close_mult2),inf_close_trans]) 1);
qed "inf_close_mult_HFinite";
-Goal "!!u. [|u @= v*x; x @= y; v: HFinite|] ==> u @= v*y";
+Goal "[|u @= v*x; x @= y; v: HFinite|] ==> u @= v*y";
by (fast_tac (claset() addIs [inf_close_mult2,inf_close_trans]) 1);
qed "inf_close_mult_subst";
-Goal "!!u. [| u @= x*v; x @= y; v: HFinite |] ==> u @= y*v";
+Goal "[| u @= x*v; x @= y; v: HFinite |] ==> u @= y*v";
by (fast_tac (claset() addIs [inf_close_mult1,inf_close_trans]) 1);
qed "inf_close_mult_subst2";
-Goal "!!u. [| u @= x*hypreal_of_real v; x @= y |] ==> u @= y*hypreal_of_real v";
+Goal "[| u @= x*hypreal_of_real v; x @= y |] ==> u @= y*hypreal_of_real v";
by (auto_tac (claset() addIs [inf_close_mult_subst2],simpset()));
qed "inf_close_mult_subst_SReal";
-Goalw [inf_close_def] "!!a. a = b ==> a @= b";
+Goalw [inf_close_def] "a = b ==> a @= b";
by (Asm_simp_tac 1);
qed "inf_close_eq_imp";
@@ -667,19 +663,19 @@
hypreal_add_assoc RS sym]));
qed "Infinitesimal_add_inf_close";
-Goal "!!y. y: Infinitesimal ==> x @= x + y";
+Goal "y: Infinitesimal ==> x @= x + y";
by (rtac (bex_Infinitesimal_iff RS iffD1) 1);
by (dtac (Infinitesimal_minus_iff RS iffD1) 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_minus_add_distrib,
hypreal_add_assoc RS sym]));
qed "Infinitesimal_add_inf_close_self";
-Goal "!!y. y: Infinitesimal ==> x @= y + x";
+Goal "y: Infinitesimal ==> x @= y + x";
by (auto_tac (claset() addDs [Infinitesimal_add_inf_close_self],
simpset() addsimps [hypreal_add_commute]));
qed "Infinitesimal_add_inf_close_self2";
-Goal "!!y. y: Infinitesimal ==> x @= x + -y";
+Goal "y: Infinitesimal ==> x @= x + -y";
by (blast_tac (claset() addSIs [Infinitesimal_add_inf_close_self,
Infinitesimal_minus_iff RS iffD1]) 1);
qed "Infinitesimal_add_minus_inf_close_self";
@@ -697,27 +693,27 @@
by (etac inf_close_sym 1);
qed "Infinitesimal_add_right_cancel";
-Goal "!!a. d + b @= d + c ==> b @= c";
+Goal "d + b @= d + c ==> b @= c";
by (dtac (inf_close_minus_iff RS iffD1) 1);
by (asm_full_simp_tac (simpset() addsimps
[hypreal_minus_add_distrib,inf_close_minus_iff RS sym]
@ hypreal_add_ac) 1);
qed "inf_close_add_left_cancel";
-Goal "!!a. b + d @= c + d ==> b @= c";
+Goal "b + d @= c + d ==> b @= c";
by (rtac inf_close_add_left_cancel 1);
by (asm_full_simp_tac (simpset() addsimps
[hypreal_add_commute]) 1);
qed "inf_close_add_right_cancel";
-Goal "!!a. b @= c ==> d + b @= d + c";
+Goal "b @= c ==> d + b @= d + c";
by (rtac (inf_close_minus_iff RS iffD2) 1);
by (asm_full_simp_tac (simpset() addsimps
[hypreal_minus_add_distrib,inf_close_minus_iff RS sym]
@ hypreal_add_ac) 1);
qed "inf_close_add_mono1";
-Goal "!!a. b @= c ==> b + a @= c + a";
+Goal "b @= c ==> b + a @= c + a";
by (asm_simp_tac (simpset() addsimps
[hypreal_add_commute,inf_close_add_mono1]) 1);
qed "inf_close_add_mono2";
@@ -755,19 +751,19 @@
inf_close_hypreal_of_real_HFinite,HFinite_hypreal_of_real]) 1);
qed "inf_close_mult_hypreal_of_real";
-Goal "!!a. [| a: SReal; a ~= 0; a*x @= 0 |] ==> x @= 0";
+Goal "[| a: SReal; a ~= 0; a*x @= 0 |] ==> x @= 0";
by (dtac (SReal_inverse RS (SReal_subset_HFinite RS subsetD)) 1);
by (auto_tac (claset() addDs [inf_close_mult2],
simpset() addsimps [hypreal_mult_assoc RS sym]));
qed "inf_close_SReal_mult_cancel_zero";
(* REM comments: newly added *)
-Goal "!!a. [| a: SReal; x @= 0 |] ==> x*a @= 0";
+Goal "[| a: SReal; x @= 0 |] ==> x*a @= 0";
by (auto_tac (claset() addDs [(SReal_subset_HFinite RS subsetD),
inf_close_mult1],simpset()));
qed "inf_close_mult_SReal1";
-Goal "!!a. [| a: SReal; x @= 0 |] ==> a*x @= 0";
+Goal "[| a: SReal; x @= 0 |] ==> a*x @= 0";
by (auto_tac (claset() addDs [(SReal_subset_HFinite RS subsetD),
inf_close_mult2],simpset()));
qed "inf_close_mult_SReal2";
@@ -778,13 +774,13 @@
qed "inf_close_mult_SReal_zero_cancel_iff";
Addsimps [inf_close_mult_SReal_zero_cancel_iff];
-Goal "!!a. [| a: SReal; a ~= 0; a* w @= a*z |] ==> w @= z";
+Goal "[| a: SReal; a ~= 0; a* w @= a*z |] ==> w @= z";
by (dtac (SReal_inverse RS (SReal_subset_HFinite RS subsetD)) 1);
by (auto_tac (claset() addDs [inf_close_mult2],
simpset() addsimps [hypreal_mult_assoc RS sym]));
qed "inf_close_SReal_mult_cancel";
-Goal "!!a. [| a: SReal; a ~= 0|] ==> (a* w @= a*z) = (w @= z)";
+Goal "[| a: SReal; a ~= 0|] ==> (a* w @= a*z) = (w @= z)";
by (auto_tac (claset() addSIs [inf_close_mult2,SReal_subset_HFinite RS subsetD]
addIs [inf_close_SReal_mult_cancel],simpset()));
qed "inf_close_SReal_mult_cancel_iff1";
@@ -826,7 +822,7 @@
qed "Infinitesimal_less_SReal2";
Goalw [Infinitesimal_def]
- "!!y. [| y: SReal; 0 < y|] ==> y ~: Infinitesimal";
+ "[| y: SReal; 0 < y|] ==> y ~: Infinitesimal";
by (auto_tac (claset() addSDs [bspec] addSEs [hypreal_less_irrefl],
simpset() addsimps [hrabs_eqI2]));
qed "SReal_not_Infinitesimal";
@@ -834,7 +830,7 @@
(* [| y : SReal; 0 < y; y : Infinitesimal |] ==> R *)
bind_thm("SReal_not_InfinitesimalE", (SReal_not_Infinitesimal RS notE));
-Goal "!!y. [| y : SReal; y < 0 |] ==> y ~:Infinitesimal";
+Goal "[| y : SReal; y < 0 |] ==> y ~:Infinitesimal";
by (blast_tac (claset() addDs [(hypreal_minus_zero_less_iff RS iffD2),
SReal_minus,(Infinitesimal_minus_iff RS iffD1),SReal_not_Infinitesimal]) 1);
qed "SReal_minus_not_Infinitesimal";
@@ -934,7 +930,7 @@
Addsimps [hypreal_of_real_inf_close_iff];
-Goal "!!r. [| r: SReal; s: SReal; r @= x; s @= x|] ==> r = s";
+Goal "[| r: SReal; s: SReal; r @= x; s @= x|] ==> r = s";
by (blast_tac (claset() addIs [(SReal_inf_close_iff RS iffD1),
inf_close_trans2]) 1);
qed "inf_close_unique_real";
@@ -1008,7 +1004,7 @@
addIs [hypreal_less_imp_le] addSIs [isUbI,setleI],simpset()));
qed "lemma_st_part_gt_ub";
-Goal "!!t. t <= t + -r ==> r <= (0::hypreal)";
+Goal "t <= t + -r ==> r <= (0::hypreal)";
by (dres_inst_tac [("x","-t")] hypreal_add_left_le_mono1 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc RS sym]));
by (dres_inst_tac [("x","r")] hypreal_add_left_le_mono1 1);
@@ -1272,7 +1268,7 @@
qed "HInfinite_square_iff";
Addsimps [HInfinite_square_iff];
-Goal "!!a. [| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z";
+Goal "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z";
by (Step_tac 1);
by (ftac HFinite_inverse 1 THEN assume_tac 1);
by (dtac not_Infinitesimal_not_zero 1);
@@ -1354,7 +1350,7 @@
by (Fast_tac 1);
qed "inf_close_mem_monad";
-Goalw [monad_def] "!!u. x @= u ==> x:monad u";
+Goalw [monad_def] "x @= u ==> x:monad u";
by (blast_tac (claset() addSIs [inf_close_sym]) 1);
qed "inf_close_mem_monad2";
@@ -1502,14 +1498,14 @@
simpset() addsimps [hypreal_add_assoc]));
qed "Infinitesimal_add_cancel_hypreal_of_real_le";
-Goal "!!xa. [| xa: Infinitesimal; hypreal_of_real x + xa <= hypreal_of_real y |] \
+Goal "[| xa: Infinitesimal; hypreal_of_real x + xa <= hypreal_of_real y |] \
\ ==> x <= y";
by (blast_tac (claset() addSIs [hypreal_of_real_le_iff RS iffD2,
Infinitesimal_add_cancel_hypreal_of_real_le]) 1);
qed "Infinitesimal_add_cancel_real_le";
Goalw [hypreal_le_def]
- "!!xa. [| xa: Infinitesimal; ya: Infinitesimal; \
+ "[| 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]);
@@ -1520,7 +1516,7 @@
simpset() addsimps [hypreal_add_assoc]));
qed "hypreal_of_real_le_add_Infininitesimal_cancel";
-Goal "!!xa. [| xa: Infinitesimal; ya: Infinitesimal; \
+Goal "[| xa: Infinitesimal; ya: Infinitesimal; \
\ hypreal_of_real x + xa <= hypreal_of_real y + ya \
\ |] ==> x <= y";
by (blast_tac (claset() addSIs [hypreal_of_real_le_iff RS iffD2,
@@ -1726,7 +1722,7 @@
Addsimps [st_zero,st_one];
-Goal "!!y. y: HFinite ==> st(-y) = -st(y)";
+Goal "y: HFinite ==> st(-y) = -st(y)";
by (forward_tac [HFinite_minus_iff RS iffD1] 1);
by (rtac hypreal_add_minus_eq_minus 1);
by (dtac (st_add RS sym) 1 THEN assume_tac 1);
@@ -2192,7 +2188,7 @@
that ALL n. |X n - a| < 1/n. Used in proof of NSLIM => LIM.
-----------------------------------------------------------------------*)
-Goal "!!u. 0 < u ==> finite {n. u < inverse(real_of_posnat n)}";
+Goal "0 < u ==> finite {n. u < inverse(real_of_posnat n)}";
by (asm_simp_tac (simpset() addsimps [real_of_posnat_less_inverse_iff]) 1);
by (rtac finite_real_of_posnat_less_real 1);
qed "finite_inverse_real_of_posnat_gt_real";
@@ -2203,19 +2199,19 @@
simpset() addsimps [real_le_refl,real_less_imp_le]));
qed "lemma_real_le_Un_eq2";
-Goal "!!u. 0 < u ==> finite {n::nat. u = inverse(real_of_posnat n)}";
+Goal "0 < u ==> finite {n::nat. u = inverse(real_of_posnat n)}";
by (asm_simp_tac (simpset() addsimps [real_of_posnat_inverse_eq_iff]) 1);
by (auto_tac (claset() addIs [lemma_finite_omega_set RSN
(2,finite_subset)],simpset()));
qed "lemma_finite_omega_set2";
-Goal "!!u. 0 < u ==> finite {n. u <= inverse(real_of_posnat n)}";
+Goal "0 < u ==> finite {n. u <= inverse(real_of_posnat n)}";
by (auto_tac (claset(),simpset() addsimps
[lemma_real_le_Un_eq2,lemma_finite_omega_set2,
finite_inverse_real_of_posnat_gt_real]));
qed "finite_inverse_real_of_posnat_ge_real";
-Goal "!!u. 0 < u ==> \
+Goal "0 < u ==> \
\ {n. u <= inverse(real_of_posnat n)} ~: FreeUltrafilterNat";
by (blast_tac (claset() addSIs [FreeUltrafilterNat_finite,
finite_inverse_real_of_posnat_ge_real]) 1);
@@ -2232,7 +2228,7 @@
simpset() addsimps [not_real_leE,real_less_not_refl]));
val lemma = result();
-Goal "!!u. 0 < u ==> \
+Goal "0 < u ==> \
\ {n. inverse(real_of_posnat n) < u} : FreeUltrafilterNat";
by (cut_inst_tac [("u","u")] inverse_real_of_posnat_ge_real_FreeUltrafilterNat 1);
by (auto_tac (claset() addDs [FreeUltrafilterNat_Compl_mem],
--- a/src/HOL/Real/Hyperreal/Series.ML Mon Dec 18 12:21:54 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Series.ML Mon Dec 18 12:23:54 2000 +0100
@@ -99,6 +99,7 @@
by (Auto_tac);
qed "sumr_shift_bounds";
+(*FIXME: replace*)
Goal "sumr 0 (n + n) (%i. (- #1) ^ Suc i) = #0";
by (induct_tac "n" 1);
by (Auto_tac);
--- a/src/HOL/Real/Hyperreal/Star.ML Mon Dec 18 12:21:54 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Star.ML Mon Dec 18 12:23:54 2000 +0100
@@ -277,6 +277,7 @@
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun]));
qed "starfun_Id";
+Addsimps [starfun_Id];
(*----------------------------------------------------------------------
the *-function is a (nonstandard) extension of the function
--- a/src/HOL/Real/RealAbs.ML Mon Dec 18 12:21:54 2000 +0100
+++ b/src/HOL/Real/RealAbs.ML Mon Dec 18 12:23:54 2000 +0100
@@ -68,6 +68,7 @@
Goalw [abs_real_def] "abs(abs x)=abs (x::real)";
by (Simp_tac 1);
qed "abs_idempotent";
+Addsimps [abs_idempotent];
Goalw [abs_real_def] "(x=(#0::real)) = (abs x = #0)";
by (Full_simp_tac 1);
--- a/src/HOL/Real/RealPow.ML Mon Dec 18 12:21:54 2000 +0100
+++ b/src/HOL/Real/RealPow.ML Mon Dec 18 12:23:54 2000 +0100
@@ -5,6 +5,8 @@
Description : Natural Powers of reals theory
*)
+bind_thm ("realpow_Suc", thm "realpow_Suc");
+
Goal "(#0::real) ^ (Suc n) = #0";
by Auto_tac;
qed "realpow_zero";
@@ -121,8 +123,8 @@
Addsimps [abs_realpow_two];
Goal "abs(x::real) ^ 2 = x ^ 2";
-by (simp_tac (simpset() addsimps
- [realpow_abs,abs_eqI1] delsimps [thm "realpow_Suc"]) 1);
+by (simp_tac (simpset() addsimps [realpow_abs,abs_eqI1]
+ delsimps [realpow_Suc]) 1);
qed "realpow_two_abs";
Addsimps [realpow_two_abs];
@@ -365,15 +367,15 @@
Goalw [real_diff_def]
"(x::real) ^ 2 - y ^ 2 = (x - y) * (x + y)";
by (simp_tac (simpset() addsimps [realpow_two_add_minus]
- delsimps [thm "realpow_Suc"]) 1);
+ delsimps [realpow_Suc]) 1);
qed "realpow_two_diff";
Goalw [real_diff_def]
"((x::real) ^ 2 = y ^ 2) = (x = y | x = -y)";
-by (auto_tac (claset(),simpset() delsimps [thm "realpow_Suc"]));
+by (auto_tac (claset(),simpset() delsimps [realpow_Suc]));
by (dtac (rename_numerals (real_eq_minus_iff RS iffD1 RS sym)) 1);
by (auto_tac (claset() addDs [rename_numerals real_add_minus_eq_minus],
- simpset() addsimps [realpow_two_add_minus] delsimps [thm "realpow_Suc"]));
+ simpset() addsimps [realpow_two_add_minus] delsimps [realpow_Suc]));
qed "realpow_two_disj";
(* used in Transc *)