# Re: [isabelle] cross product in Isabelle

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

```

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