Email Gateway (Aug 19 2022 at 14:45): Email Gateway (Aug 19 2022 at 14:45):From: lyj238 <lyj238@gmail.com>
Dear experts:
The cross product in Euclide-space is directly defined in the multivariate lib in Isabelle?
regards!
2014-06-12
lyj238
Email Gateway (Aug 19 2022 at 14:46):From: Johannes Hölzl <hoelzl@in.tum.de>
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.
Email Gateway (Aug 19 2022 at 14:46):From: Brian Huffman <huffman.brian.c@gmail.com>
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,
Email Gateway (Aug 19 2022 at 14:47):From: "lyj238@gmail.com" <lyj238@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！
Email Gateway (Aug 19 2022 at 14:48):From: Brian Huffman <huffman.brian.c@gmail.com>
On Sun, Jun 15, 2014 at 8:08 AM, lyj238@gmail.com <lyj238@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.
Last updated: Apr 30 2024 at 08:19 UTC