*To*: "Brian Huffman" <huffman.brian.c at gmail.com>, Johannes Hölzl <hoelzl at in.tum.de>*Subject*: Re: [isabelle] cross product in Isabelle*From*: "lyj238 at gmail.com" <lyj238 at gmail.com>*Date*: Sun, 15 Jun 2014 23:08:01 +0800*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*References*: <201406121208168530088@gmail.com>, <1402596792.10752.26.camel@lapnipkow5>, <CAAMXsiYY8=CmTpc=A8qtntFu3yYU1v69oZvm=adPN0fUSRt=oA@mail.gmail.com>

Hi, Huffman: Thank you very much. In linear algebra, a vector is usually our research object. Of course, (a1,a2,a3) can be seen as a vector. But I find that a vecotor has been formalized in mutivariate_analysis lib. I want to use the formalized vetor concept to formalize the cross product by using a matrix operator and a point operator( the informal account is also in the end), which is as follows: I meets a prolem due to my knowledge on the vector: (1) the first element is count from 0 or 1: (2) the operators χ and $. Although I have tried to guess how to use them, but it is still diffcult for me to prove my definition coincides with the definition by using the vector and matrix formalization in the mutivariate libaray, can you help me?. definition cross3' :: "real^3 ⇒ real^3 ⇒ real^3" where "cross3' = (λa. λb. (χ i. if i=0 then a$1 * b$2 - a$2* b$1 else if i=1 then a$2 * b$0 - a$0 * b$2 else a$0 * b$1 - a$1 * b$0))" definition vectPoint::"real^3 ⇒ real^3^3" where "vectPoint = (λa. (χ i. if i=0 then (χ i. if i=0 then 0 else if i=1 then - a$2 else a$1) else if i=1 then (χ i. if i=0 then a $2 else if i=1 then 0 else - a$0) else (χ i. if i=0 then -a$1 else if i=1 then a$0 else 0)))" The above formalization on the cross product comes from the follwing material: Thus I want to prove the following lemma: lemma cross3Def2:"cross3' a b= (vectPoint a) *v b" apply (simp add: cross3'_def vectPoint_def matrix_vector_mult_def) apply auto proof falis here. regards！ lyj238 at gmail.com From: Brian Huffman Date: 2014-06-13 13:10 To: Johannes Hölzl; lyj238 CC: Isabelle Users ML Subject: Re: [isabelle] cross product in Isabelle 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:*Brian Huffman

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

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

**Re: [isabelle] cross product in Isabelle***From:*Brian Huffman

- Previous by Date: [isabelle] using AFP
- Next by Date: Re: [isabelle] Parsing a string to a 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