*To*: "A.L. Hicks" <alh70 at cam.ac.uk>*Subject*: Re: [isabelle] type unification failed using an old lemma?*From*: Mark Wassell <mpwassell at gmail.com>*Date*: Fri, 5 Aug 2016 16:44:04 +0100*Cc*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <87b52048b20769f309c2b256bbb072e8@cam.ac.uk>*References*: <87b52048b20769f309c2b256bbb072e8@cam.ac.uk>

Hi, Something before your line have "((Îx. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a :: real_normed_algebra)) (at x within {a .. b})" has "given" g' the type real â real Have you perhaps said (g has_derivative g') rather than (g has_vector_derivative g') ? Mark On 5 August 2016 at 15:24, A.L. Hicks <alh70 at cam.ac.uk> wrote: > 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 > >

**References**:**[isabelle] type unification failed using an old lemma?***From:*A.L. Hicks

- Previous by Date: Re: [isabelle] Proposal: An update to Multiset theory
- Next by Date: Re: [isabelle] Proposal: An update to Multiset theory
- Previous by Thread: [isabelle] type unification failed using an old lemma?
- Next by Thread: [isabelle] New AFP Article: Ptolemy's Theorem
- Cl-isabelle-users August 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list