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.