Quelle  Cross3.thy   Sprache: Isabelle

(* 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

open_bundle cross3_syntax
begin
notation cross3 (infixr ‹×› 80)
unbundle no set_product_syntax
end


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"
  by (simp_all add: orthogonal_def cross3_simps)

lemma  orthogonal_cross: "orthogonal (x \ y) x" "orthogonal (x \ y) y"  
                        "orthogonal y (x \ y)" "orthogonal (x \ y) x"
  by (simp_all add: orthogonal_def dot_cross_self)

lemma  cross_zero_left [simp]: "0 \ x = 0" and cross_zero_right [simp]: "x \ 0 = 0" for x::"real^3"
  by (simp_all add: cross3_simps)

lemma  cross_skew: "(x \ y) = -(y \ x)" for x::"real^3"
  by (simp add: cross3_simps)

lemma  cross_refl [simp]: "x \ x = 0" for x::"real^3"
  by (simp add: cross3_simps)

lemma  cross_add_left: "(x + y) \ z = (x \ z) + (y \ z)" for x::"real^3"
  by (simp add: cross3_simps)

lemma  cross_add_right: "x \ (y + z) = (x \ y) + (x \ z)" for x::"real^3"
  by (simp add: cross3_simps)

lemma  cross_mult_left: "(c *\<^sub>R x) \ y = c *\<^sub>R (x \ y)" for x::"real^3"
  by (simp add: cross3_simps)

lemma  cross_mult_right: "x \ (c *\<^sub>R y) = c *\<^sub>R (x \ y)" for x::"real^3"
  by (simp add: cross3_simps)

lemma  cross_minus_left [simp]: "(-x) \ y = - (x \ y)" for x::"real^3"
  by (simp add: cross3_simps)

lemma  cross_minus_right [simp]: "x \ -y = - (x \ y)" for x::"real^3"
  by (simp add: cross3_simps)

lemma  left_diff_distrib: "(x - y) \ z = x \ z - y \ z" for x::"real^3"
  by (simp add: cross3_simps)

lemma  right_diff_distrib: "x \ (y - z) = x \ y - x \ z" for x::"real^3"
  by (simp add: cross3_simps)

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"
  by (simp add: cross3_simps)

proposition Lagrange: "x \ (y \ z) = (x \ z) *\<^sub>R y - (x \ y) *\<^sub>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"
    by (simp add: x)
  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))\<^sup>2 + (x \ y)\<^sup>2 = (norm x * norm y)\<^sup>2"
  unfolding power2_norm_eq_inner power_mult_distrib
  by (simp add: cross3_simps power2_eq_square)

lemma  dot_cross_det: "x \ (y \ z) = det(vector[x,y,z])"
  by (simp add: cross3_simps) 

lemma  cross_cross_det: "(w \ x) \ (y \ z) = det(vector[w,x,z]) *\<^sub>R y - det(vector[w,x,y]) *\<^sub>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)"
  by (force simp add: cross3_simps)

proposition  norm_cross: "(norm (x \ y))\<^sup>2 = (norm x)\<^sup>2 * (norm y)\<^sup>2 - (x \ y)\<^sup>2"
  unfolding power2_norm_eq_inner power_mult_distrib
  by (simp add: cross3_simps power2_eq_square)

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)\<^sup>2 = (x \ y)\<^sup>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
  apply (simp add: cross_add_right)
  apply (simp add: cross_mult_right)
  apply (simp add: cross_add_left)
  apply (simp add: cross_mult_left)
  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 *\<^sub>R (x \ y)"
  apply (simp add: vec_eq_iff   )
  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 *\<^sub>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)"
  by (simp add: rotation_matrix_def cross_orthogonal_matrix)

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) *\<^sub>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)"
  by (simp add: cross_orthogonal_transformation orthogonal_transformation)

subsection ‹Continuity›

lemma  continuous_cross: "\continuous F f; continuous F g\ \ continuous F (\x. (f x) \ (g x))"
  apply (subst continuous_componentwise)
  apply (clarsimp simp add: cross3_simps)
  apply (intro continuous_intros; simp)
  done

lemma  continuous_on_cross:
  fixes f :: "'a::t2_space \ real^3"
  shows "\continuous_on S f; continuous_on S g\ \ continuous_on S (\x. (f x) \ (g x))"
  by (simp add: continuous_on_eq_continuous_within continuous_cross)

unbundle no cross3_syntax

end