1072 (*-------------------------------- |
1072 (*-------------------------------- |
1073 Negation of function |
1073 Negation of function |
1074 -------------------------------*) |
1074 -------------------------------*) |
1075 Goal "NSDERIV f x :> D ==> NSDERIV (%x. -(f x)) x :> -D"; |
1075 Goal "NSDERIV f x :> D ==> NSDERIV (%x. -(f x)) x :> -D"; |
1076 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff]) 1); |
1076 by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff]) 1); |
1077 by (res_inst_tac [("t","f x")] (real_minus_minus RS subst) 1); |
1077 by (dtac NSLIM_minus 1); |
1078 by (subgoal_tac "(\\<lambda>h. (- f (x + h) + - (- f x)) / h) = (\\<lambda>h. - ((f (x + h) + - f x) / h))" 1); |
1078 by (subgoal_tac "ALL a::real. ALL b. - a + b = - (a + - b)" 1); |
|
1079 by (asm_full_simp_tac (HOL_ss addsimps [thm"minus_divide_left" RS sym]) 1); |
1079 by (Asm_full_simp_tac 1); |
1080 by (Asm_full_simp_tac 1); |
1080 by (etac NSLIM_minus 1); |
|
1081 by (asm_full_simp_tac (simpset() addsimps [real_minus_divide_eq RS sym]) 1); |
|
1082 qed "NSDERIV_minus"; |
1081 qed "NSDERIV_minus"; |
1083 |
1082 |
1084 Goal "DERIV f x :> D \ |
1083 Goal "DERIV f x :> D \ |
1085 \ ==> DERIV (%x. -(f x)) x :> -D"; |
1084 \ ==> DERIV (%x. -(f x)) x :> -D"; |
1086 by (asm_full_simp_tac (simpset() addsimps |
1085 by (asm_full_simp_tac (simpset() addsimps |