Theory Cross_Product_7
section‹Vector Cross Product in 7 Dimensions›
theory Cross_Product_7
imports "HOL-Analysis.Multivariate_Analysis"
begin
subsection‹Elementary auxiliary lemmas.›
lemma exhaust_7:
fixes x :: 7
shows "x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 5 ∨ x = 6 ∨ x = 7 "
proof (induct x)
case (of_int z)
then have "0 ≤ z" and "z < 7" by simp_all
then have "z = 0 ∨ z = 1 ∨ z = 2 ∨ z = 3 ∨ z = 4 ∨ z =5∨ z = 6 ∨ z =7 " by arith
then show ?case by auto
qed
lemma forall_7: "(∀i::7. P i) ⟷ P 1 ∧ P 2 ∧ P 3∧ P 4 ∧ P 5 ∧ P 6∧ P 7 "
by (metis exhaust_7)
lemma vector_7 [simp]:
"(vector [x1,x2,x3,x4,x5,x6,x7] ::('a::zero)^7)$1 = x1"
"(vector [x1,x2,x3,x4,x5,x6,x7] ::('a::zero)^7)$2 = x2"
"(vector [x1,x2,x3,x4,x5,x6,x7] ::('a::zero)^7)$3 = x3"
"(vector [x1,x2,x3,x4,x5,x6,x7] ::('a::zero)^7)$4 = x4"
"(vector [x1,x2,x3,x4,x5,x6,x7] ::('a::zero)^7)$5 = x5"
"(vector [x1,x2,x3,x4,x5,x6,x7] ::('a::zero)^7)$6 = x6"
"(vector [x1,x2,x3,x4,x5,x6,x7] ::('a::zero)^7)$7 = x7"
unfolding vector_def by auto
lemma forall_vector_7:
"(∀v::'a::zero^7. P v) ⟷ (∀x1 x2 x3 x4 x5 x6 x7. P(vector[x1, x2, x3, x4, x5, x6, x7]))"
apply auto
apply (erule_tac x="v$1" in allE)
apply (erule_tac x="v$2" in allE)
apply (erule_tac x="v$3" in allE)
apply (erule_tac x="v$4" in allE)
apply (erule_tac x="v$5" in allE)
apply (erule_tac x="v$6" in allE)
apply (erule_tac x="v$7" in allE)
apply (subgoal_tac "vector [v$1, v$2, v$3, v$4, v$5, v$6, v$7] = v")
apply simp
apply (vector vector_def)
apply (simp add: forall_7)
done
lemma UNIV_7: "UNIV = {1::7, 2::7, 3::7, 4::7, 5::7, 6::7, 7::7}"
using exhaust_7 by auto
lemma sum_7: "sum f (UNIV::7 set) = f 1 + f 2 + f 3 + f 4 + f 5 + f 6 + f 7"
unfolding UNIV_7 by (simp add: ac_simps)
lemma not_equal_vector7 :
fixes x::"real^7" and y::"real^7"
assumes "x = vector[x1,x2,x3,x4,x5,x6,x7] " and "y= vector [y1,y2,y3,y4,y5,y6,y7]"
and "x$1 ≠ y$1 ∨ x$2 ≠ y$2 ∨ x$3 ≠ y$3 ∨ x$4 ≠ y$4 ∨ x$5 ≠ y$5 ∨ x$6 ≠ y$6 ∨ x$7 ≠ y$7 "
shows "x ≠ y" using assms by blast
lemma equal_vector7:
fixes x::"real^7" and y::"real^7"
assumes "x = vector[x1,x2,x3,x4,x5,x6,x7] " and "y= vector [y1,y2,y3,y4,y5,y6,y7]"
and "x = y"
shows "x$1 = y$1 ∧ x$2 = y$2 ∧ x$3 = y$3 ∧ x$4 = y$4 ∧ x$5 = y$5 ∧ x$6 = y$6 ∧ x$7 = y$7 "
using assms by blast
lemma numeral_4_eq_4: "4 = Suc( Suc (Suc (Suc 0)))"
by (simp add: eval_nat_numeral)
lemma numeral_5_eq_5: "5 = Suc(Suc( Suc (Suc (Suc 0))))"
by (simp add: eval_nat_numeral)
lemma numeral_6_eq_6: "6 = Suc( Suc(Suc( Suc (Suc (Suc 0)))))"
by (simp add: eval_nat_numeral)
lemma numeral_7_eq_7: "7 = Suc(Suc( Suc(Suc( Suc (Suc (Suc 0))))))"
by (simp add: eval_nat_numeral)
subsection‹The definition of the 7D cross product and related lemmas›
context includes no_Set_Product_syntax
begin
text ‹Note: in total there exist 480 equivalent multiplication tables for the definition,
the following is based on the one most widely used: ›
definition cross7 :: "[real^7, real^7] ⇒ real^7" (infixr "×⇩7" 80)
where "a ×⇩7 b ≡
vector [a$2 * b$4 - a$4 * b$2 + a$3 * b$7 - a$7 * b$3 + a$5 * b$6 - a$6 * b$5 ,
a$3 * b$5 - a$5 * b$3 + a$4 * b$1 - a$1 * b$4 + a$6 * b$7 - a$7 * b$6 ,
a$4 * b$6 - a$6 * b$4 + a$5 * b$2 - a$2 * b$5 + a$7 * b$1 - a$1 * b$7 ,
a$5 * b$7 - a$7 * b$5 + a$6 * b$3 - a$3 * b$6 + a$1 * b$2 - a$2 * b$1 ,
a$6 * b$1 - a$1 * b$6 + a$7 * b$4 - a$4 * b$7 + a$2 * b$3 - a$3 * b$2 ,
a$7 * b$2 - a$2 * b$7 + a$1 * b$5 - a$5 * b$1 + a$3 * b$4 - a$4 * b$3 ,
a$1 * b$3 - a$3 * b$1 + a$2 * b$6 - a$6 * b$2 + a$4 * b$5 - a$5 * b$4 ]"
end
bundle cross7_syntax begin
notation cross7 (infixr "×⇩7" 80)
no_notation Product_Type.Times (infixr "×⇩7" 80)
end
bundle no_cross7_syntax begin
no_notation cross7 (infixr "×⇩7" 80)
notation Product_Type.Times (infixr "×⇩7" 80)
end
unbundle cross7_syntax
lemmas cross7_simps = cross7_def inner_vec_def sum_7 det_def vec_eq_iff vector_def algebra_simps
lemma dot_cross7_self: "x ∙ (x ×⇩7 y) = 0" "x ∙ (y ×⇩7 x) = 0" "(x ×⇩7 y) ∙ y = 0" "(y ×⇩7 x) ∙ y = 0"
by (simp_all add: orthogonal_def cross7_simps)
lemma orthogonal_cross7: "orthogonal (x ×⇩7 y) x" "orthogonal (x ×⇩7 y) y"
"orthogonal y (x×⇩7 y)" "orthogonal (x ×⇩7 y) x"
by (simp_all add: orthogonal_def dot_cross7_self)
lemma cross7_zero_left [simp]: "0 ×⇩7 x = 0"
and cross7_zero_right [simp]: "x ×⇩7 0 = 0"
by (simp_all add: cross7_simps)
lemma cross7_skew: "(x ×⇩7 y) = -(y ×⇩7 x)"
by (simp add: cross7_simps)
lemma cross7_refl [simp]: "x ×⇩7 x = 0"
by (simp add: cross7_simps)
lemma cross7_add_left: "(x + y) ×⇩7 z = (x ×⇩7 z) + (y ×⇩7 z)"
and cross7_add_right: "x ×⇩7 (y + z) = (x ×⇩7 y) + (x ×⇩7 z)"
by (simp_all add: cross7_simps)
lemma cross7_mult_left: "(c *⇩R x) ×⇩7 y = c *⇩R (x ×⇩7 y)"
and cross7_mult_right: "x ×⇩7 (c *⇩R y) = c *⇩R (x ×⇩7 y)"
by (simp_all add: cross7_simps)
lemma cross7_minus_left [simp]: "(-x) ×⇩7 y = - (x ×⇩7 y)"
and cross7_minus_right [simp]: "x ×⇩7 -y = - (x ×⇩7 y)"
by (simp_all add: cross7_simps)
lemma left_diff_distrib: "(x - y) ×⇩7 z = x ×⇩7 z - y ×⇩7 z"
and right_diff_distrib: "x ×⇩7 (y - z) = x ×⇩7 y - x ×⇩7 z"
by (simp_all add: cross7_simps)
hide_fact (open) left_diff_distrib right_diff_distrib
lemma cross7_triple1: "(x ×⇩7 y) ∙ z = (y ×⇩7 z) ∙ x"
and cross7_triple2: "(x ×⇩7 y) ∙ z = x ∙ (y ×⇩7 z) "
by (simp_all add: cross7_def inner_vec_def sum_7 vec_eq_iff algebra_simps)
lemma scalar7_triple1: "x ∙ (y ×⇩7 z) = y ∙ (z ×⇩7 x)"
and scalar7_triple2: "x ∙ (y ×⇩7 z) = z ∙ (x ×⇩7 y ) "
by (simp_all add: cross7_def inner_vec_def sum_7 vec_eq_iff algebra_simps)
lemma cross7_components:
"(x ×⇩7 y)$1 = x$2 * y$4 - x$4 * y$2 + x$3 * y$7 - x$7 * y$3 + x$5 * y$6 - x$6 * y$5 "
"(x ×⇩7 y)$2 = x$4 * y$1 - x$1 * y$4 + x$3 * y$5 - x$5 * y$3 + x$6 * y$7 - x$7 * y$6 "
"(x ×⇩7 y)$3 = x$5 * y$2 - x$2 * y$5 + x$4 * y$6 - x$6 * y$4 + x$7 * y$1 - x$1 * y$7 "
"(x ×⇩7 y)$4 = x$1 * y$2 - x$2 * y$1 + x$6 * y$3 - x$3 * y$6 + x$5 * y$7 - x$7 * y$5 "
"(x ×⇩7 y)$5 = x$6 * y$1 - x$1 * y$6 + x$2 * y$3 - x$3 * y$2 + x$7 * y$4 - x$4 * y$7 "
"(x ×⇩7 y)$6 = x$1 * y$5 - x$5 * y$1 + x$7 * y$2 - x$2 * y$7 + x$3 * y$4 - x$4 * y$3 "
"(x ×⇩7 y)$7 = x$1 * y$3 - x$3 * y$1 + x$4 * y$5 - x$5 * y$4 + x$2 * y$6 - x$6 * y$2 "
by (simp_all add: cross7_def inner_vec_def sum_7 vec_eq_iff algebra_simps)
text ‹Nonassociativity of the 7D cross product showed using a counterexample›
lemma cross7_nonassociative:
" ¬ (∀ (c::real^7) (a::real^7) ( b::real^7) . c ×⇩7 (a ×⇩7 b) = (c ×⇩7 a ) ×⇩7 b) "
proof-
have *: " ∃ (c::real^7) (a::real^7) ( b::real^7) . c ×⇩7 (a ×⇩7 b) ≠ (c ×⇩7 a ) ×⇩7 b "
proof-
define f::"real^7" where "f = vector[ 0, 0, 0, 0, 0, 1, 1 ]"
define g::"real^7" where "g = vector[ 0, 0, 0, 1, 0, 0, 0 ]"
define h::"real^7" where "h = vector[ 1, 0, 1, 0, 0, 0, 0 ]"
define u where " u= (g ×⇩7 h) "
define v where " v= (f ×⇩7 g) "
have 1:" u = vector[0, 1, 0, 0, 0, -1, 0]"
unfolding cross7_def g_def h_def f_def u_def by simp
have 3:" f ×⇩7 u = vector[0, 1, 0, 0, 0, 1, -1 ] "
unfolding cross7_def f_def using 1 by simp
have 2:" v = vector[0, 0, -1, 0, 1, 0, 0]"
unfolding cross7_def g_def h_def f_def v_def by simp
have 4:" v ×⇩7 h = vector[0, -1, 0, 0, 0, -1, 1 ] "
unfolding cross7_def h_def using 2 by simp
define x::"real^7" where "x= vector[0, 1, 0, 0, 0, 1, -1] "
define y::"real^7" where "y= vector[0, -1, 0, 0, 0,-1, 1] "
have *: "x$2 = 1" unfolding x_def by simp
have **: "y$2 = -1" unfolding y_def by simp
have ***: "x ≠ y" using * ** by auto
have 5: " f ×⇩7 u ≠ v ×⇩7 h"
unfolding x_def y_def
using ***
by (simp add: "3" "4" x_def y_def)
have 6:" f ×⇩7 (g ×⇩7 h) ≠ (f ×⇩7 g ) ×⇩7 h " using 5 by (simp add: u_def v_def)
show ?thesis unfolding f_def g_def h_def using 6 by blast
qed
show ?thesis using * by blast
qed
text ‹The 7D cross product does not satisfy the Jacobi Identity(shown using a counterexample) ›
lemma cross7_not_Jacobi:
" ¬ (∀ (c::real^7) (a::real^7) ( b::real^7) . (c ×⇩7 a ) ×⇩7 b + (b ×⇩7 c) ×⇩7 a
+ (a ×⇩7 b ) ×⇩7 c =0 ) "
proof-
have *: " ∃ (c::real^7) (a::real^7) ( b::real^7) . (c ×⇩7 a ) ×⇩7 b + (b ×⇩7 c) ×⇩7 a
+ (a ×⇩7 b ) ×⇩7 c ≠0 "
proof-
define f::"real^7" where " f= vector[ 0, 0, 0, 0, 0, 1, 1 ] "
define g::"real^7" where " g= vector[ 0, 0, 0, 1, 0, 0, 0 ] "
define h::"real^7" where " h= vector[ 1, 0, 1, 0, 0, 0, 0 ] "
define u where " u= (g ×⇩7 h) "
define v where " v= (f ×⇩7 g) "
define w where " w = (h ×⇩7 f) "
have 1:" u = vector[0, 1, 0, 0, 0, -1, 0]"
unfolding cross7_def g_def h_def f_def u_def by simp
have 3:" u ×⇩7 f = vector[0,- 1, 0, 0, 0,- 1, 1 ] "
unfolding cross7_def f_def using 1 by simp
have 2:" v = vector[0, 0, -1, 0, 1, 0, 0]"
unfolding cross7_def g_def h_def f_def v_def by simp
have 4:" v ×⇩7 h = vector[0, -1, 0, 0, 0, -1, 1 ] "
unfolding cross7_def h_def using 2 by simp
have 8: " w = vector[1, 0, -1, -1, -1, 0, 0]"
unfolding cross7_def h_def f_def w_def by simp
have 9: " w ×⇩7 g = vector[0, -1, 0, 0, 0, -1, 1]"
unfolding cross7_def h_def f_def w_def g_def apply simp done
have &: "(u ×⇩7 f)$2+( v ×⇩7 h) $2+( w ×⇩7 g) $2 =-3" using 3 4 9 by simp
have &&: " u ×⇩7 f + v ×⇩7 h + w ×⇩7 g ≠ 0 " using &
by (metis vector_add_component zero_index zero_neq_neg_numeral)
show ?thesis using && u_def v_def w_def by blast
qed
show ?thesis using * by blast
qed
text‹The vector triple product property fulfilled for the 3D cross product does not hold
for the 7D cross product. Shown below with a counterexample. ›
lemma cross7_not_vectortriple:
"¬(∀ (c::real^7) (a::real^7) ( b::real^7).( c ×⇩7 a ) ×⇩7 b = (c ∙ b ) *⇩R a - (c ∙ a )*⇩R b)"
proof-
have *: "∃(c::real^7) (a::real^7) ( b::real^7). (c ×⇩7 a) ×⇩7 b ≠ (c ∙ b ) *⇩R a - (c ∙ a )*⇩R b"
proof-
define g:: "real ^ 7" where "g = vector[0, 0, 0, 1, 0, 0, 0]"
define h:: "real ^ 7" where "h = vector[1, 0, 1, 0, 0, 0, 0]"
define f:: "real ^ 7" where "f = vector[0, 0, 0, 0, 0, 1, 1]"
define u where "u = (g ×⇩7 h)"
have 1: "u = vector[0, 1, 0, 0, 0, -1, 0]"
unfolding cross7_def g_def h_def f_def u_def by simp
have 2:" u ×⇩7 f = vector[0,- 1, 0, 0, 0,- 1, 1 ]"
unfolding cross7_def f_def using 1 by simp
have 3: "(g ∙ f) *⇩R h = 0" unfolding g_def f_def inner_vec_def
by (simp add: sum_7)
have 4: "(g ∙ h) *⇩R f = 0" unfolding g_def h_def inner_vec_def
by (simp add: sum_7)
have 5: "(g ∙ f) *⇩R h -(g ∙ h) *⇩R f = 0"
using 3 4 by auto
have 6: "u ×⇩7 f ≠ 0" using 2
by (metis one_neq_zero vector_7(7) zero_index)
have 7: "(g ×⇩7 h) ×⇩7 f ≠ 0" using 2 6 u_def by blast
have 8: "(g ×⇩7 h) ×⇩7 f ≠ (g ∙ f) *⇩R h - (g ∙ h ) *⇩R f"
using 5 7 by simp
show ?thesis using 8 by auto
qed
show ?thesis using * by auto
qed
lemma axis_nth_neq [simp]: "i ≠ j ⟹ axis i x $ j = 0"
by (simp add: axis_def)
lemma cross7_basis:
"(axis 1 1) ×⇩7 (axis 2 1) = axis 4 1" "(axis 2 1) ×⇩7 (axis 1 1) = -(axis 4 1)"
"(axis 2 1) ×⇩7 (axis 3 1) = axis 5 1" "(axis 3 1) ×⇩7 (axis 2 1) = -(axis 5 1)"
"(axis 3 1) ×⇩7 (axis 4 1) = axis 6 1" "(axis 4 1) ×⇩7 (axis 3 1) = -(axis 6 1)"
"(axis 2 1) ×⇩7 (axis 4 1) = axis 1 1" "(axis 4 1) ×⇩7 (axis 2 1) = -(axis 1 1)"
"(axis 4 1) ×⇩7 (axis 5 1) = axis 7 1" "(axis 5 1) ×⇩7 (axis 4 1) = -(axis 7 1)"
"(axis 3 1) ×⇩7 (axis 5 1) = axis 2 1" "(axis 5 1) ×⇩7 (axis 3 1) = -(axis 2 1)"
"(axis 4 1) ×⇩7 (axis 6 1) = axis 3 1" "(axis 6 1) ×⇩7 (axis 4 1) = -(axis 3 1)"
"(axis 5 1) ×⇩7 (axis 7 1) = axis 4 1" "(axis 7 1) ×⇩7 (axis 5 1) = -(axis 4 1)"
"(axis 4 1) ×⇩7 (axis 1 1) = axis 2 1" "(axis 1 1) ×⇩7 (axis 4 1) = -(axis 2 1)"
"(axis 5 1) ×⇩7 (axis 2 1) = axis 3 1" "(axis 2 1) ×⇩7 (axis 5 1) = -(axis 3 1)"
"(axis 6 1) ×⇩7 (axis 3 1) = axis 4 1" "(axis 3 1) ×⇩7 (axis 6 1) = -(axis 4 1)"
"(axis 7 1) ×⇩7 (axis 4 1) = axis 5 1" "(axis 4 1) ×⇩7 (axis 7 1) = -(axis 5 1)"
"(axis 5 1) ×⇩7 (axis 6 1) = axis 1 1" "(axis 6 1) ×⇩7 (axis 5 1) = -(axis 1 1)"
"(axis 6 1) ×⇩7 (axis 7 1) = axis 2 1" "(axis 7 1) ×⇩7 (axis 6 1) = -(axis 2 1)"
"(axis 7 1) ×⇩7 (axis 1 1) = axis 3 1" "(axis 1 1) ×⇩7 (axis 7 1) = -(axis 3 1)"
"(axis 6 1) ×⇩7 (axis 1 1) = axis 5 1" "(axis 1 1) ×⇩7 (axis 6 1) = -(axis 5 1)"
"(axis 7 1) ×⇩7 (axis 2 1) = axis 6 1" "(axis 2 1) ×⇩7 (axis 7 1) = -(axis 6 1)"
"(axis 1 1) ×⇩7 (axis 3 1) = axis 7 1" "(axis 3 1) ×⇩7 (axis 1 1) = -(axis 7 1)"
"(axis 1 1) ×⇩7 (axis 5 1) = axis 6 1" "(axis 5 1) ×⇩7 (axis 1 1) = -(axis 6 1)"
"(axis 2 1) ×⇩7 (axis 6 1) = axis 7 1" "(axis 6 1) ×⇩7 (axis 2 1) = -(axis 7 1)"
"(axis 3 1) ×⇩7 (axis 7 1) = axis 1 1" "(axis 7 1) ×⇩7 (axis 3 1) = -(axis 1 1)"
by (simp_all add: vec_eq_iff forall_7 cross7_components)
lemma cross7_basis_zero:
" u=0 ⟹ (u ×⇩7 axis 1 1 = 0) ∧ (u ×⇩7 axis 2 1 = 0) ∧ (u ×⇩7 axis 3 1 = 0)
∧ (u ×⇩7 axis 4 1 = 0) ∧ (u ×⇩7 axis 5 1 = 0 ) ∧ (u ×⇩7 axis 6 1 = 0 )
∧ (u ×⇩7 axis 7 1 = 0) "
by auto
lemma cross7_basis_nonzero:
"¬ (u ×⇩7 axis 1 1 = 0) ∨ ¬ (u ×⇩7 axis 2 1 = 0) ∨ ¬ (u ×⇩7 axis 3 1 = 0)
∨ ¬ (u ×⇩7 axis 4 1 = 0) ∨ ¬ (u ×⇩7 axis 5 1 = 0 ) ∨ ¬ (u ×⇩7 axis 6 1 = 0 )
∨ ¬ (u ×⇩7 axis 7 1 = 0) ⟹ u ≠ 0"
by auto
text‹Pythagorean theorem/magnitude›
lemma norm_square_vec_eq: "norm x ^ 2 = (∑i∈UNIV. x $ i ^ 2)"
by (auto simp: norm_vec_def L2_set_def intro!: sum_nonneg)
lemma norm_cross7_dot_magnitude: "(norm (x ×⇩7 y))⇧2 = (norm x)⇧2 * (norm y)⇧2 - (x ∙ y)⇧2"
unfolding norm_square_vec_eq sum_7 cross7_components inner_vec_def real_norm_def inner_real_def
by algebra
lemma cross7_eq_0: "x ×⇩7 y = 0 ⟷ collinear {0, x, y}"
proof -
have "x ×⇩7 y = 0 ⟷ norm (x ×⇩7 y) = 0"
by simp
also have "... ⟷ (norm x * norm y)⇧2 = (x ∙ y)⇧2"
using norm_cross7_dot_magnitude [of x y] by (auto simp: power_mult_distrib)
also have "... ⟷ ¦x ∙ y¦ = norm x * norm y"
using power2_eq_iff
by (metis (mono_tags, opaque_lifting) abs_minus abs_norm_cancel
abs_power2 norm_mult power_abs real_norm_def)
also have "... ⟷ collinear {0, x, y}"
by (rule norm_cauchy_schwarz_equal)
finally show ?thesis .
qed
lemma cross7_eq_self: "x ×⇩7 y = x ⟷ x = 0" "x ×⇩7 y = y ⟷ y = 0"
apply (metis cross7_zero_left dot_cross7_self(1) inner_eq_zero_iff)
apply (metis cross7_zero_right dot_cross7_self(2) inner_eq_zero_iff)
done
lemma norm_and_cross7_eq_0:
"x ∙ y = 0 ∧ x ×⇩7 y = 0 ⟷ x = 0 ∨ y = 0" (is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
using cross7_eq_0 norm_cauchy_schwarz_equal by force
next
assume ?rhs
then show ?lhs
by auto
qed
lemma bilinear_cross7: "bilinear (×⇩7)"
apply (auto simp add: bilinear_def linear_def)
apply unfold_locales
apply (simp_all add: cross7_add_right cross7_mult_right cross7_add_left cross7_mult_left)
done
subsection‹Continuity›
lemma continuous_cross7: "⟦continuous F f; continuous F g⟧ ⟹ continuous F (λx. f x ×⇩7 g x)"
by (subst continuous_componentwise)(auto intro!: continuous_intros simp: cross7_simps)
lemma continuous_on_cross:
fixes f :: "'a::t2_space ⇒ real^7"
shows "⟦continuous_on S f; continuous_on S g⟧ ⟹ continuous_on S (λx. f x ×⇩7 g x)"
by (simp add: continuous_on_eq_continuous_within continuous_cross7)
end