[isabelle] type unification failed using an old lemma?



Hi,

Sorry in advance if this is some trivial error on my part.
I'd like to use the lemma has_vector_derivative_mult in the HOL library which reads:

"lemma has_vector_derivative_mult[derivative_intros]:
"(f has_vector_derivative f') (at x within s) â (g has_vector_derivative g') (at x within s) â ((Îx. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a :: real_normed_algebra)) (at x within s)" by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_mult])"

However it seems that using a statement such as

have "((Îx. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a :: real_normed_algebra)) (at x within {a .. b})"

leads to a standard type unification error:

Type unification failed: Clash of types "_ â _" and "real"
Type error in application: incompatible operand type
Operator:  op * (f x) :: real â real
Operand:   g' :: real â real
Coercion Inference:
Local coercion insertion on the operand failed:
No coercion known for type constructors: "fun" and "real"

Am I missing something or is the lemma itself flawed?

As an aside, there is a similar lemma for the has_derivative operator: has_derivative_mult
which works for statements like
have "((%x. f x * g x) has_derivative (%y. f x * g' y + f' y * g x)) (at x within {a .. b})" Say I have h=(%x. f x * g x), I can obtain h' such that h has_derivative h but can't seem to define h' explicitly.

Thanks,
Alex Hicks




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.