*To*: "lyj238 at gmail.com" <lyj238 at gmail.com>*Subject*: Re: [isabelle] cross product in Isabelle*From*: Brian Huffman <huffman.brian.c at gmail.com>*Date*: Mon, 16 Jun 2014 11:30:05 -0700*Cc*: Johannes Hölzl <hoelzl at in.tum.de>, cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <2014061523075676668928@gmail.com>*References*: <201406121208168530088@gmail.com> <1402596792.10752.26.camel@lapnipkow5> <CAAMXsiYY8=CmTpc=A8qtntFu3yYU1v69oZvm=adPN0fUSRt=oA@mail.gmail.com> <2014061523075676668928@gmail.com>

On Sun, Jun 15, 2014 at 8:08 AM, lyj238 at gmail.com <lyj238 at gmail.com> wrote: > 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. > > In the Multivariate_Analysis theory, vectors are defined as a type class "real_vector". We also provide a hierarchy of more specific type classes, such as "real_normed_vector" for normed vector spaces, "real_inner" for inner product spaces, and "euclidean_space" for finite-dimensional inner product spaces. Most theorems in Multivariate_Analysis are proved for an arbitrary type of the appropriate class. Both "real * real * real" and "real^3" are members of the "euclidean_space" class. Theorems provided in Multivariate_Analysis apply equally to either type, so you are free to choose whichever is most convenient to work with. > 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 $. > The type "3" is a three-element type consisting of the integers modulo 3. At this type, 0 = 3, so you may use indexes {0,1,2} or {1,2,3} as you wish. However, I recommend using indexes starting with 1, for two reasons: First, most mathematical textbooks (including the one you quoted) use indexes starting with 1. Second, Multivariate_Analysis provides theorems like UNIV_3 that assume indexes starting with 1. > 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?. > To make your definitions look more like the textbook definitions, you should do two things: First, use indexes {1, 2, 3} instead of {0,1,2}. Second, define a constructor function for vectors of size three so you don't have to write if/then/else everywhere. For example: definition Vec3 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ^ 3" where "Vec3 a b c = (χ i. if i = 1 then a else if i = 2 then b else c)" lemma Vec3_simps [simp]: "Vec3 a b c $ 1 = a" "Vec3 a b c $ 2 = b" "Vec3 a b c $ 3 = c" unfolding Vec3_def by auto lemma Vec3: "Vec3 (x $ 1) (x $ 2) (x $ 3) = x" unfolding Vec3_def vec_eq_iff using UNIV_3 by auto lemma vec3_eq_iff: fixes x y :: "'a ^ 3" shows "x = y ⟷ x$1 = y$1 ∧ x$2 = y$2 ∧ x$3 = y$3" by (metis Vec3) 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)))" > You should change these to something like this: definition cross3' :: "real^3 ⇒ real^3 ⇒ real^3" where "cross3' a b = Vec 3 ..." definition vectPoint::"real^3 ⇒ real^3^3" where "vectPoint a = Vec3 (Vec3 ...) (Vec3 ...) (Vec3 ...)" > > 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. > Using lemma "UNIV_3", which states that "(UNIV :: 3 set) = {1,2,3}", should make this proof easier. - Brian

**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

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

- Previous by Date: Re: [isabelle] Code_Target.evaluator raises various exception during serialisation
- Next by Date: [isabelle] HART (Haskell and Rewriting Techniques) 2014 -- Last Call for Papers
- Previous by Thread: Re: [isabelle] cross product in Isabelle
- Next by Thread: [isabelle] VSComp - Call for Participation
- 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