Email Gateway (Aug 22 2022 at 11:03): Email Gateway (Aug 22 2022 at 11:03):From: Mark Wassell <mpwassell@gmail.com>
Hello,
I have the following lemma:
lemma
fixes x :: real
assumes "0 < x + 1"
shows "(( λx. ln (x+1)) has_real_derivative 1/(x+1)) (at x within s)"
apply(rule DERIV_ln_divide[THEN DERIV_chain2, derivative_intros,
where ?g = "λx. x+1" and ?Db=1 and ?x=x and ?s=s,OF assms,
simplified])
apply(rule DERIV_add[OF DERIV_ident DERIV_const[of 1], simplified, of x s])
done
Is there a way to do this type of proof without having to make the
instantiations explicit (ie the ?Db=1 parts) and without having to match
the structure of the function being differentiated?
Cheers
Mark
Email Gateway (Aug 22 2022 at 11:03):From: Manuel Eberl <eberlm@in.tum.de>
using assms by (force intro: derivative_eq_intros)
Email Gateway (Aug 22 2022 at 11:04):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Mark,
as Manuel's proof mentions we have for this purpose the lemma collection
derivative_eq_intros
All lemmas get the form
DERIV f x :> f' ==> F' f' = y ==> DERIV (%x. F (f x)) x :> y
where F is the function the lemma es concerned, i.e. ln, or + etc. The
equation allows to add the rules as intro!:, and the rest is done by the
simplifier, maybe with the addition of field_simps, which takes care of
ac rewriting (and more).
If you want to introduce your one rules just use the attribute
derivative_intros
This automatically adds a rule to derivative_eq_intros
Last updated: Apr 19 2024 at 01:05 UTC