# HG changeset patch # User paulson # Date 977138634 -3600 # Node ID cd80241125b0fa79eb6f2673da6f8e9acd534ecd # Parent 5c44de6aadf44bb54a6fe435306913ad57560b80 tidying and adding new proofs diff -r 5c44de6aadf4 -r cd80241125b0 src/HOL/Real/Hyperreal/HRealAbs.ML --- 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); diff -r 5c44de6aadf4 -r cd80241125b0 src/HOL/Real/Hyperreal/HSeries.ML --- /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"; + + + + + + + diff -r 5c44de6aadf4 -r cd80241125b0 src/HOL/Real/Hyperreal/HSeries.thy --- /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 diff -r 5c44de6aadf4 -r cd80241125b0 src/HOL/Real/Hyperreal/HyperDef.ML --- 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"; diff -r 5c44de6aadf4 -r cd80241125b0 src/HOL/Real/Hyperreal/Hyperreal.thy --- 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 diff -r 5c44de6aadf4 -r cd80241125b0 src/HOL/Real/Hyperreal/Lim.ML --- 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"; + diff -r 5c44de6aadf4 -r cd80241125b0 src/HOL/Real/Hyperreal/NSA.ML --- 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], diff -r 5c44de6aadf4 -r cd80241125b0 src/HOL/Real/Hyperreal/Series.ML --- 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); diff -r 5c44de6aadf4 -r cd80241125b0 src/HOL/Real/Hyperreal/Star.ML --- 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 diff -r 5c44de6aadf4 -r cd80241125b0 src/HOL/Real/RealAbs.ML --- 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); diff -r 5c44de6aadf4 -r cd80241125b0 src/HOL/Real/RealPow.ML --- 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 *)