# Theory Cross_Product_7

```(* Title:      Cross_Product_7.thy
Author:     Angeliki Koutsoukou-Argyraki, University of Cambridge
Date:       September 2018
*)
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)
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)))"
lemma numeral_5_eq_5: "5 = Suc(Suc( Suc (Suc (Suc 0))))"
lemma numeral_6_eq_6: "6 = Suc( Suc(Suc( Suc (Suc (Suc 0)))))"
lemma numeral_7_eq_7: "7 = Suc(Suc( Suc(Suc( Suc (Suc (Suc 0))))))"

subsection‹The definition of the 7D cross product and related lemmas›

context includes no_Set_Product_syntax
begin (* locally disable syntax for set product, to avoid warnings *)

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"

lemma orthogonal_cross7: "orthogonal (x ×⇩7 y) x" "orthogonal (x ×⇩7 y) y"
"orthogonal y (x×⇩7  y)" "orthogonal (x ×⇩7 y) x"

lemma cross7_zero_left [simp]:  "0 ×⇩7 x = 0"
and cross7_zero_right [simp]: "x ×⇩7 0 = 0"

lemma cross7_skew: "(x ×⇩7 y) = -(y ×⇩7 x)"

lemma cross7_refl [simp]: "x ×⇩7 x = 0"

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)"

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)"

lemma cross7_minus_left [simp]: "(-x) ×⇩7 y = - (x ×⇩7 y)"
and cross7_minus_right [simp]: "x ×⇩7 -y = - (x ×⇩7 y)"

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"

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 &

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
have 4: "(g ∙ h) *⇩R f = 0" unfolding g_def h_def  inner_vec_def
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"

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