*To*: Johannes Hölzl <hoelzl at in.tum.de>, lyj238 <lyj238 at gmail.com>*Subject*: Re: [isabelle] cross product in Isabelle*From*: Brian Huffman <huffman.brian.c at gmail.com>*Date*: Thu, 12 Jun 2014 22:10:42 -0700*Cc*: Isabelle Users ML <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <1402596792.10752.26.camel@lapnipkow5>*References*: <201406121208168530088@gmail.com> <1402596792.10752.26.camel@lapnipkow5>

Hi Lyj, As Johannes says, there is no cross product formalized in Multivariate_Analysis. But you can easily define one yourself, like this: theory Cross imports Multivariate_Analysis begin definition cross2 :: "real × real ⇒ real × real ⇒ real" where "cross2 = (λ(a1,a2). λ(b1,b2). a1 * b2 - a2 * b1)" definition cross3 :: "real × real × real ⇒ real × real × real ⇒ real × real × real" where "cross3 = (λ(a1,a2,a3). λ(b1,b2,b3). (a2 * b3 - a3 * b2, a3 * b1 - a1 * b3, a1 * b2 - a2 * b1))" It is then a simple matter to prove that the cross product is a bounded bilinear operator. By interpreting the "bounded_bilinear" locale you can obtain many useful lemmas automatically. lemma bounded_bilinear_cross3: "bounded_bilinear cross3" apply (rule bilinear_conv_bounded_bilinear [THEN iffD1]) apply (auto simp add: bilinear_def cross_def algebra_simps intro!: linearI) done interpretation cross: bounded_bilinear cross3 by (rule bounded_bilinear_cross3) print_theorems (* this shows lemmas about distributivity, continuity, limits, etc. *) Hope this helps, - Brian On Thu, Jun 12, 2014 at 11:13 AM, Johannes Hölzl <hoelzl at in.tum.de> wrote: > Hi Lyj, > > there isn't yet a formalization of the cross product of two vectors in > Isabelle/HOL. At least not in Multivariate_Analysis. But I'm also not > aware of any other formalization. > > - Johannes > > Am Donnerstag, den 12.06.2014, 12:08 +0800 schrieb lyj238: >> Dear experts: >> The cross product in Euclide-space is directly defined in the multivariate lib in Isabelle? >> >> >> regards! >> >> 2014-06-12 >> >> >> >> lyj238 > > >

**Follow-Ups**:**Re: [isabelle] cross product in Isabelle***From:*lyj238 at gmail.com

**References**:**[isabelle] cross product in Isabelle***From:*lyj238

**Re: [isabelle] cross product in Isabelle***From:*Johannes Hölzl

- Previous by Date: [isabelle] New AFP entry: Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
- Next by Date: [isabelle] Bound variables in Code_Evaluation.term
- Previous by Thread: Re: [isabelle] cross product in Isabelle
- Next by Thread: Re: [isabelle] cross product in Isabelle
- Cl-isabelle-users June 2014 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