# HG changeset patch # User nipkow # Date 1008181262 -3600 # Node ID ea5d6da573c540fba6fa1584b636b740a1d6dad6 # Parent 32e67277a4b99b246969de0e198cc0c819f85855 mods due to reorienting and renaming of real_minus_mult_eq1/2 diff -r 32e67277a4b9 -r ea5d6da573c5 src/HOL/Hyperreal/Lim.ML --- a/src/HOL/Hyperreal/Lim.ML Wed Dec 12 19:19:59 2001 +0100 +++ b/src/HOL/Hyperreal/Lim.ML Wed Dec 12 19:21:02 2001 +0100 @@ -1050,7 +1050,7 @@ by (asm_full_simp_tac (simpset() addsimps [real_times_divide1_eq RS sym, NSDERIV_NSLIM_iff, real_minus_mult_eq2, real_add_mult_distrib2 RS sym] - delsimps [real_times_divide1_eq, real_minus_mult_eq2 RS sym]) 1); + delsimps [real_times_divide1_eq, real_mult_minus_eq2]) 1); by (etac (NSLIM_const RS NSLIM_mult) 1); qed "NSDERIV_cmult"; @@ -1063,7 +1063,7 @@ by (asm_full_simp_tac (simpset() addsimps [real_times_divide1_eq RS sym, NSDERIV_NSLIM_iff, real_minus_mult_eq2, real_add_mult_distrib2 RS sym] - delsimps [real_times_divide1_eq, real_minus_mult_eq2 RS sym]) 1); + delsimps [real_times_divide1_eq, real_mult_minus_eq2]) 1); by (etac (LIM_const RS LIM_mult2) 1); qed "DERIV_cmult"; @@ -1074,7 +1074,7 @@ by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff]) 1); by (res_inst_tac [("t","f x")] (real_minus_minus RS subst) 1); by (asm_simp_tac (simpset() addsimps [real_minus_add_distrib RS sym, - real_minus_mult_eq1 RS sym] + real_mult_minus_eq1] delsimps [real_minus_add_distrib, real_minus_minus]) 1); by (etac NSLIM_minus 1); qed "NSDERIV_minus"; @@ -1354,8 +1354,7 @@ \ ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"; by (rtac (real_mult_commute RS subst) 1); by (asm_simp_tac (simpset() addsimps [real_minus_mult_eq1, - realpow_inverse] delsimps [realpow_Suc, - real_minus_mult_eq1 RS sym]) 1); + realpow_inverse] delsimps [realpow_Suc, real_mult_minus_eq1]) 1); by (fold_goals_tac [o_def]); by (blast_tac (claset() addSIs [DERIV_chain,DERIV_inverse]) 1); qed "DERIV_inverse_fun"; @@ -1377,8 +1376,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 [realpow_Suc, real_minus_mult_eq1 RS sym, - real_minus_mult_eq2 RS sym]) 1); + delsimps [realpow_Suc, real_mult_minus_eq1, real_mult_minus_eq2]) 1); qed "DERIV_quotient"; Goal "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \\ 0 |] \ @@ -2135,8 +2133,7 @@ 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])); + simpset() addsimps [real_add_mult_distrib, real_diff_def])); qed "DERIV_const_ratio_const"; Goal "[|a \\ b; \\x. DERIV f x :> k |] ==> (f(b) - f(a))/(b - a) = k"; diff -r 32e67277a4b9 -r ea5d6da573c5 src/HOL/Hyperreal/Poly.ML --- a/src/HOL/Hyperreal/Poly.ML Wed Dec 12 19:19:59 2001 +0100 +++ b/src/HOL/Hyperreal/Poly.ML Wed Dec 12 19:21:02 2001 +0100 @@ -361,7 +361,7 @@ by (res_inst_tac [("x","r#q")] exI 1); by (res_inst_tac [("x","a*r + h")] exI 1); by (case_tac "q" 1); -by (auto_tac (claset(),simpset() addsimps [real_minus_mult_eq1 RS sym])); +by (Auto_tac); qed "lemma_poly_linear_rem"; Goal "EX q r. h#t = [r] +++ [-a, 1] *** q"; @@ -741,7 +741,7 @@ by Auto_tac; by (res_inst_tac [("x","qaa +++ -- qa")] exI 1); by (auto_tac (claset(),simpset() addsimps [poly_add,fun_eq,poly_mult, - poly_minus,real_add_mult_distrib2,real_minus_mult_eq2 RS sym, + poly_minus,real_add_mult_distrib2, ARITH_PROVE "(x = y + -z) = (z + x = (y::real))"])); qed "poly_divides_diff"; @@ -800,8 +800,7 @@ by (induct_tac "n" 1); by (asm_full_simp_tac (simpset() delsimps [pmult_Cons,pexp_Suc]) 1); by (eres_inst_tac [("Pa","poly q a = 0")] swap 1); -by (asm_full_simp_tac (simpset() addsimps [poly_add,poly_cmult, - real_minus_mult_eq1 RS sym]) 1); +by (asm_full_simp_tac (simpset() addsimps [poly_add,poly_cmult]) 1); by (rtac (pexp_Suc RS ssubst) 1); by (rtac ccontr 1); by (asm_full_simp_tac (simpset() addsimps [poly_mult_left_cancel, @@ -1014,8 +1013,8 @@ real_mult_ac) RS ssubst) 1); by (rotate_tac 2 1); by (dres_inst_tac [("x","xa")] spec 1); -by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib, - real_minus_mult_eq1 RS sym] @ real_mult_ac +by (asm_full_simp_tac (simpset() + addsimps [real_add_mult_distrib] @ real_mult_ac delsimps [pmult_Cons]) 1); qed_spec_mp "lemma_order_pderiv"; diff -r 32e67277a4b9 -r ea5d6da573c5 src/HOL/Hyperreal/Series.ML --- a/src/HOL/Hyperreal/Series.ML Wed Dec 12 19:19:59 2001 +0100 +++ b/src/HOL/Hyperreal/Series.ML Wed Dec 12 19:21:02 2001 +0100 @@ -86,7 +86,7 @@ Goal "sumr 0 n f + -(real n * r) = sumr 0 n (%i. f i + -r)"; by (full_simp_tac (simpset() addsimps [sumr_add RS sym, - real_minus_mult_eq2] delsimps [real_minus_mult_eq2 RS sym]) 1); + real_minus_mult_eq2] delsimps [real_mult_minus_eq2]) 1); qed "sumr_add_mult_const"; Goalw [real_diff_def] diff -r 32e67277a4b9 -r ea5d6da573c5 src/HOL/Hyperreal/Transcendental.ML --- a/src/HOL/Hyperreal/Transcendental.ML Wed Dec 12 19:19:59 2001 +0100 +++ b/src/HOL/Hyperreal/Transcendental.ML Wed Dec 12 19:21:02 2001 +0100 @@ -2089,7 +2089,6 @@ by (auto_tac (claset() addSIs [sin_gt_zero2,cos_gt_zero_pi] addSIs [real_mult_order, real_inverse_gt_0],simpset())); -by (rtac (CLAIM "-x < y ==> -y < (x::real)") 1 THEN Auto_tac); qed "tan_gt_zero"; Goal "[| - pi/2 < x; x < 0 |] ==> tan x < 0"; @@ -2170,7 +2169,6 @@ by (Step_tac 1); by (res_inst_tac [("x","-x")] exI 2); by (auto_tac (claset() addSIs [exI],simpset())); -by (rtac (CLAIM "-x < y ==> -y < (x::real)") 1 THEN Auto_tac); qed "lemma_tan_total1"; Goal "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"; diff -r 32e67277a4b9 -r ea5d6da573c5 src/HOL/Real/HahnBanach/Aux.thy --- a/src/HOL/Real/HahnBanach/Aux.thy Wed Dec 12 19:19:59 2001 +0100 +++ b/src/HOL/Real/HahnBanach/Aux.thy Wed Dec 12 19:21:02 2001 +0100 @@ -74,7 +74,7 @@ hence "x * (- z) \ y * (- z)" by (rule real_mult_le_le_mono2) hence "- (x * z) \ - (y * z)" - by (simp only: real_minus_mult_eq2) + by (simp only: real_mult_minus_eq2) thus ?thesis by (simp only: real_mult_commute) qed