# Theory Cross3

```(* Title:      HOL/Analysis/Cross3.thy
Author:     L C Paulson, University of Cambridge

Ported from HOL Light
*)

section‹Vector Cross Products in 3 Dimensions›

theory "Cross3"
imports Determinants Cartesian_Euclidean_Space
begin

context includes no_Set_Product_syntax
begin ―‹locally disable syntax for set product, to avoid warnings›

definition✐‹tag important› cross3 :: "[real^3, real^3] ⇒ real^3"  (infixr "×" 80)
where "a × b ≡
vector [a\$2 * b\$3 - a\$3 * b\$2,
a\$3 * b\$1 - a\$1 * b\$3,
a\$1 * b\$2 - a\$2 * b\$1]"

end

bundle cross3_syntax begin
notation cross3 (infixr "×" 80)
no_notation Product_Type.Times (infixr "×" 80)
end

bundle no_cross3_syntax begin
no_notation cross3 (infixr "×" 80)
notation Product_Type.Times (infixr "×" 80)
end

unbundle cross3_syntax

subsection‹ Basic lemmas›

lemmas cross3_simps = cross3_def inner_vec_def sum_3 det_3 vec_eq_iff vector_def algebra_simps

lemma dot_cross_self: "x ∙ (x × y) = 0" "x ∙ (y × x) = 0" "(x × y) ∙ y = 0" "(y × x) ∙ y = 0"

lemma  orthogonal_cross: "orthogonal (x × y) x" "orthogonal (x × y) y"
"orthogonal y (x × y)" "orthogonal (x × y) x"

lemma  cross_zero_left [simp]: "0 × x = 0" and cross_zero_right [simp]: "x × 0 = 0" for x::"real^3"

lemma  cross_skew: "(x × y) = -(y × x)" for x::"real^3"

lemma  cross_refl [simp]: "x × x = 0" for x::"real^3"

lemma  cross_add_left: "(x + y) × z = (x × z) + (y × z)" for x::"real^3"

lemma  cross_add_right: "x × (y + z) = (x × y) + (x × z)" for x::"real^3"

lemma  cross_mult_left: "(c *⇩R x) × y = c *⇩R (x × y)" for x::"real^3"

lemma  cross_mult_right: "x × (c *⇩R y) = c *⇩R (x × y)" for x::"real^3"

lemma  cross_minus_left [simp]: "(-x) × y = - (x × y)" for x::"real^3"

lemma  cross_minus_right [simp]: "x × -y = - (x × y)" for x::"real^3"

lemma  left_diff_distrib: "(x - y) × z = x × z - y × z" for x::"real^3"

lemma  right_diff_distrib: "x × (y - z) = x × y - x × z" for x::"real^3"

hide_fact (open) left_diff_distrib right_diff_distrib

proposition Jacobi: "x × (y × z) + y × (z × x) + z × (x × y) = 0" for x::"real^3"

proposition Lagrange: "x × (y × z) = (x ∙ z) *⇩R y - (x ∙ y) *⇩R z"
by (simp add: cross3_simps) (metis (full_types) exhaust_3)

proposition cross_triple: "(x × y) ∙ z = (y × z) ∙ x"
by (simp add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps)

lemma  cross_components:
"(x × y)\$1 = x\$2 * y\$3 - y\$2 * x\$3" "(x × y)\$2 = x\$3 * y\$1 - y\$3 * x\$1" "(x × y)\$3 = x\$1 * y\$2 - y\$1 * x\$2"
by (simp_all add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps)

lemma  cross_basis: "(axis 1 1) × (axis 2 1) = axis 3 1" "(axis 2 1) × (axis 1 1) = -(axis 3 1)"
"(axis 2 1) × (axis 3 1) = axis 1 1" "(axis 3 1) × (axis 2 1) = -(axis 1 1)"
"(axis 3 1) × (axis 1 1) = axis 2 1" "(axis 1 1) × (axis 3 1) = -(axis 2 1)"
using exhaust_3
by (force simp add: axis_def cross3_simps)+

lemma  cross_basis_nonzero:
"u ≠ 0 ⟹ u × axis 1 1 ≠ 0 ∨ u × axis 2 1 ≠ 0 ∨ u × axis 3 1 ≠ 0"
by (clarsimp simp add: axis_def cross3_simps) (metis exhaust_3)

lemma  cross_dot_cancel:
fixes x::"real^3"
assumes deq: "x ∙ y = x ∙ z" and veq: "x × y = x × z" and x: "x ≠ 0"
shows "y = z"
proof -
have "x ∙ x ≠ 0"
then have "y - z = 0"
using veq
by (metis (no_types, lifting) Cross3.right_diff_distrib Lagrange deq eq_iff_diff_eq_0 inner_diff_right scale_eq_0_iff)
then show ?thesis
using eq_iff_diff_eq_0 by blast
qed

lemma  norm_cross_dot: "(norm (x × y))⇧2 + (x ∙ y)⇧2 = (norm x * norm y)⇧2"
unfolding power2_norm_eq_inner power_mult_distrib

lemma  dot_cross_det: "x ∙ (y × z) = det(vector[x,y,z])"

lemma  cross_cross_det: "(w × x) × (y × z) = det(vector[w,x,z]) *⇩R y - det(vector[w,x,y]) *⇩R z"
using exhaust_3 by (force simp add: cross3_simps)

proposition  dot_cross: "(w × x) ∙ (y × z) = (w ∙ y) * (x ∙ z) - (w ∙ z) * (x ∙ y)"

proposition  norm_cross: "(norm (x × y))⇧2 = (norm x)⇧2 * (norm y)⇧2 - (x ∙ y)⇧2"
unfolding power2_norm_eq_inner power_mult_distrib

lemma  cross_eq_0: "x × y = 0 ⟷ collinear{0,x,y}"
proof -
have "x × y = 0 ⟷ norm (x × y) = 0"
by simp
also have "... ⟷ (norm x * norm y)⇧2 = (x ∙ y)⇧2"
using norm_cross [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  cross_eq_self: "x × y = x ⟷ x = 0" "x × y = y ⟷ y = 0"
apply (metis cross_zero_left dot_cross_self(1) inner_eq_zero_iff)
by (metis cross_zero_right dot_cross_self(2) inner_eq_zero_iff)

lemma  norm_and_cross_eq_0:
"x ∙ y = 0 ∧ x × y = 0 ⟷ x = 0 ∨ y = 0" (is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
by (metis cross_dot_cancel cross_zero_right inner_zero_right)
qed auto

lemma  bilinear_cross: "bilinear(×)"
apply (auto simp add: bilinear_def linear_def)
apply unfold_locales
done

subsection   ‹Preservation by rotation, or other orthogonal transformation up to sign›

lemma  cross_matrix_mult: "transpose A *v ((A *v x) × (A *v y)) = det A *⇩R (x × y)"
apply (simp add: vector_matrix_mult_def matrix_vector_mult_def forall_3 cross3_simps)
done

lemma  cross_orthogonal_matrix:
assumes "orthogonal_matrix A"
shows "(A *v x) × (A *v y) = det A *⇩R (A *v (x × y))"
proof -
have "mat 1 = transpose (A ** transpose A)"
by (metis (no_types) assms orthogonal_matrix_def transpose_mat)
then show ?thesis
by (metis (no_types) vector_matrix_mul_rid vector_transpose_matrix cross_matrix_mult matrix_vector_mul_assoc matrix_vector_mult_scaleR)
qed

lemma  cross_rotation_matrix: "rotation_matrix A ⟹ (A *v x) × (A *v y) =  A *v (x × y)"

lemma  cross_rotoinversion_matrix: "rotoinversion_matrix A ⟹ (A *v x) × (A *v y) = - A *v (x × y)"
by (simp add: rotoinversion_matrix_def cross_orthogonal_matrix scaleR_matrix_vector_assoc)

lemma  cross_orthogonal_transformation:
assumes "orthogonal_transformation f"
shows   "(f x) × (f y) = det(matrix f) *⇩R f(x × y)"
proof -
have orth: "orthogonal_matrix (matrix f)"
using assms orthogonal_transformation_matrix by blast
have "matrix f *v z = f z" for z
using assms orthogonal_transformation_matrix by force
with cross_orthogonal_matrix [OF orth] show ?thesis
by simp
qed

lemma  cross_linear_image:
"⟦linear f; ⋀x. norm(f x) = norm x; det(matrix f) = 1⟧
⟹ (f x) × (f y) = f(x × y)"

subsection ‹Continuity›

lemma  continuous_cross: "⟦continuous F f; continuous F g⟧ ⟹ continuous F (λx. (f x) × (g x))"
apply (subst continuous_componentwise)