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)
  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 (* 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"
  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 = (iUNIV. 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