Re: [isabelle] cross product in Isabelle

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.


lyj238 at
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
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)
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> 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

JPEG image

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