src/HOL/Analysis/Cross3.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (3 months ago) changeset 69981 3dced198b9ec parent 69683 8b3458ca0762 child 70136 f03a01a18c6e permissions -rw-r--r--
more strict AFP properties;
```     1 (* Title:      HOL/Analysis/Cross3.thy
```
```     2    Author:     L C Paulson, University of Cambridge
```
```     3
```
```     4 Ported from HOL Light
```
```     5 *)
```
```     6
```
```     7 section\<open>Vector Cross Products in 3 Dimensions\<close>
```
```     8
```
```     9 theory "Cross3"
```
```    10   imports Determinants Cartesian_Euclidean_Space
```
```    11 begin
```
```    12
```
```    13 context includes no_Set_Product_syntax
```
```    14 begin \<comment>\<open>locally disable syntax for set product, to avoid warnings\<close>
```
```    15
```
```    16 definition%important cross3 :: "[real^3, real^3] \<Rightarrow> real^3"  (infixr "\<times>" 80)
```
```    17   where "a \<times> b \<equiv>
```
```    18     vector [a\$2 * b\$3 - a\$3 * b\$2,
```
```    19             a\$3 * b\$1 - a\$1 * b\$3,
```
```    20             a\$1 * b\$2 - a\$2 * b\$1]"
```
```    21
```
```    22 end
```
```    23
```
```    24 bundle cross3_syntax begin
```
```    25 notation cross3 (infixr "\<times>" 80)
```
```    26 no_notation Product_Type.Times (infixr "\<times>" 80)
```
```    27 end
```
```    28
```
```    29 bundle no_cross3_syntax begin
```
```    30 no_notation cross3 (infixr "\<times>" 80)
```
```    31 notation Product_Type.Times (infixr "\<times>" 80)
```
```    32 end
```
```    33
```
```    34 unbundle cross3_syntax
```
```    35
```
```    36 subsection\<open> Basic lemmas\<close>
```
```    37
```
```    38 lemmas cross3_simps = cross3_def inner_vec_def sum_3 det_3 vec_eq_iff vector_def algebra_simps
```
```    39
```
```    40 lemma dot_cross_self: "x \<bullet> (x \<times> y) = 0" "x \<bullet> (y \<times> x) = 0" "(x \<times> y) \<bullet> y = 0" "(y \<times> x) \<bullet> y = 0"
```
```    41   by (simp_all add: orthogonal_def cross3_simps)
```
```    42
```
```    43 lemma  orthogonal_cross: "orthogonal (x \<times> y) x" "orthogonal (x \<times> y) y"
```
```    44                         "orthogonal y (x \<times> y)" "orthogonal (x \<times> y) x"
```
```    45   by (simp_all add: orthogonal_def dot_cross_self)
```
```    46
```
```    47 lemma  cross_zero_left [simp]: "0 \<times> x = 0" and cross_zero_right [simp]: "x \<times> 0 = 0" for x::"real^3"
```
```    48   by (simp_all add: cross3_simps)
```
```    49
```
```    50 lemma  cross_skew: "(x \<times> y) = -(y \<times> x)" for x::"real^3"
```
```    51   by (simp add: cross3_simps)
```
```    52
```
```    53 lemma  cross_refl [simp]: "x \<times> x = 0" for x::"real^3"
```
```    54   by (simp add: cross3_simps)
```
```    55
```
```    56 lemma  cross_add_left: "(x + y) \<times> z = (x \<times> z) + (y \<times> z)" for x::"real^3"
```
```    57   by (simp add: cross3_simps)
```
```    58
```
```    59 lemma  cross_add_right: "x \<times> (y + z) = (x \<times> y) + (x \<times> z)" for x::"real^3"
```
```    60   by (simp add: cross3_simps)
```
```    61
```
```    62 lemma  cross_mult_left: "(c *\<^sub>R x) \<times> y = c *\<^sub>R (x \<times> y)" for x::"real^3"
```
```    63   by (simp add: cross3_simps)
```
```    64
```
```    65 lemma  cross_mult_right: "x \<times> (c *\<^sub>R y) = c *\<^sub>R (x \<times> y)" for x::"real^3"
```
```    66   by (simp add: cross3_simps)
```
```    67
```
```    68 lemma  cross_minus_left [simp]: "(-x) \<times> y = - (x \<times> y)" for x::"real^3"
```
```    69   by (simp add: cross3_simps)
```
```    70
```
```    71 lemma  cross_minus_right [simp]: "x \<times> -y = - (x \<times> y)" for x::"real^3"
```
```    72   by (simp add: cross3_simps)
```
```    73
```
```    74 lemma  left_diff_distrib: "(x - y) \<times> z = x \<times> z - y \<times> z" for x::"real^3"
```
```    75   by (simp add: cross3_simps)
```
```    76
```
```    77 lemma  right_diff_distrib: "x \<times> (y - z) = x \<times> y - x \<times> z" for x::"real^3"
```
```    78   by (simp add: cross3_simps)
```
```    79
```
```    80 hide_fact (open) left_diff_distrib right_diff_distrib
```
```    81
```
```    82 proposition Jacobi: "x \<times> (y \<times> z) + y \<times> (z \<times> x) + z \<times> (x \<times> y) = 0" for x::"real^3"
```
```    83   by (simp add: cross3_simps)
```
```    84
```
```    85 proposition Lagrange: "x \<times> (y \<times> z) = (x \<bullet> z) *\<^sub>R y - (x \<bullet> y) *\<^sub>R z"
```
```    86   by (simp add: cross3_simps) (metis (full_types) exhaust_3)
```
```    87
```
```    88 proposition cross_triple: "(x \<times> y) \<bullet> z = (y \<times> z) \<bullet> x"
```
```    89   by (simp add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps)
```
```    90
```
```    91 lemma  cross_components:
```
```    92    "(x \<times> y)\$1 = x\$2 * y\$3 - y\$2 * x\$3" "(x \<times> y)\$2 = x\$3 * y\$1 - y\$3 * x\$1" "(x \<times> y)\$3 = x\$1 * y\$2 - y\$1 * x\$2"
```
```    93   by (simp_all add: cross3_def inner_vec_def sum_3 vec_eq_iff algebra_simps)
```
```    94
```
```    95 lemma  cross_basis: "(axis 1 1) \<times> (axis 2 1) = axis 3 1" "(axis 2 1) \<times> (axis 1 1) = -(axis 3 1)"
```
```    96                    "(axis 2 1) \<times> (axis 3 1) = axis 1 1" "(axis 3 1) \<times> (axis 2 1) = -(axis 1 1)"
```
```    97                    "(axis 3 1) \<times> (axis 1 1) = axis 2 1" "(axis 1 1) \<times> (axis 3 1) = -(axis 2 1)"
```
```    98   using exhaust_3
```
```    99   by (force simp add: axis_def cross3_simps)+
```
```   100
```
```   101 lemma  cross_basis_nonzero:
```
```   102   "u \<noteq> 0 \<Longrightarrow> u \<times> axis 1 1 \<noteq> 0 \<or> u \<times> axis 2 1 \<noteq> 0 \<or> u \<times> axis 3 1 \<noteq> 0"
```
```   103   by (clarsimp simp add: axis_def cross3_simps) (metis vector_3 exhaust_3)
```
```   104
```
```   105 lemma  cross_dot_cancel:
```
```   106   fixes x::"real^3"
```
```   107   assumes deq: "x \<bullet> y = x \<bullet> z" and veq: "x \<times> y = x \<times> z" and x: "x \<noteq> 0"
```
```   108   shows "y = z"
```
```   109 proof -
```
```   110   have "x \<bullet> x \<noteq> 0"
```
```   111     by (simp add: x)
```
```   112   then have "y - z = 0"
```
```   113     using veq
```
```   114     by (metis (no_types, lifting) Cross3.right_diff_distrib Lagrange deq eq_iff_diff_eq_0 inner_diff_right scale_eq_0_iff)
```
```   115   then show ?thesis
```
```   116     using eq_iff_diff_eq_0 by blast
```
```   117 qed
```
```   118
```
```   119 lemma  norm_cross_dot: "(norm (x \<times> y))\<^sup>2 + (x \<bullet> y)\<^sup>2 = (norm x * norm y)\<^sup>2"
```
```   120   unfolding power2_norm_eq_inner power_mult_distrib
```
```   121   by (simp add: cross3_simps power2_eq_square)
```
```   122
```
```   123 lemma  dot_cross_det: "x \<bullet> (y \<times> z) = det(vector[x,y,z])"
```
```   124   by (simp add: cross3_simps)
```
```   125
```
```   126 lemma  cross_cross_det: "(w \<times> x) \<times> (y \<times> z) = det(vector[w,x,z]) *\<^sub>R y - det(vector[w,x,y]) *\<^sub>R z"
```
```   127   using exhaust_3 by (force simp add: cross3_simps)
```
```   128
```
```   129 proposition  dot_cross: "(w \<times> x) \<bullet> (y \<times> z) = (w \<bullet> y) * (x \<bullet> z) - (w \<bullet> z) * (x \<bullet> y)"
```
```   130   by (force simp add: cross3_simps)
```
```   131
```
```   132 proposition  norm_cross: "(norm (x \<times> y))\<^sup>2 = (norm x)\<^sup>2 * (norm y)\<^sup>2 - (x \<bullet> y)\<^sup>2"
```
```   133   unfolding power2_norm_eq_inner power_mult_distrib
```
```   134   by (simp add: cross3_simps power2_eq_square)
```
```   135
```
```   136 lemma  cross_eq_0: "x \<times> y = 0 \<longleftrightarrow> collinear{0,x,y}"
```
```   137 proof -
```
```   138   have "x \<times> y = 0 \<longleftrightarrow> norm (x \<times> y) = 0"
```
```   139     by simp
```
```   140   also have "... \<longleftrightarrow> (norm x * norm y)\<^sup>2 = (x \<bullet> y)\<^sup>2"
```
```   141     using norm_cross [of x y] by (auto simp: power_mult_distrib)
```
```   142   also have "... \<longleftrightarrow> \<bar>x \<bullet> y\<bar> = norm x * norm y"
```
```   143     using power2_eq_iff
```
```   144     by (metis (mono_tags, hide_lams) abs_minus abs_norm_cancel abs_power2 norm_mult power_abs real_norm_def)
```
```   145   also have "... \<longleftrightarrow> collinear {0, x, y}"
```
```   146     by (rule norm_cauchy_schwarz_equal)
```
```   147   finally show ?thesis .
```
```   148 qed
```
```   149
```
```   150 lemma  cross_eq_self: "x \<times> y = x \<longleftrightarrow> x = 0" "x \<times> y = y \<longleftrightarrow> y = 0"
```
```   151   apply (metis cross_zero_left dot_cross_self(1) inner_eq_zero_iff)
```
```   152   by (metis cross_zero_right dot_cross_self(2) inner_eq_zero_iff)
```
```   153
```
```   154 lemma  norm_and_cross_eq_0:
```
```   155    "x \<bullet> y = 0 \<and> x \<times> y = 0 \<longleftrightarrow> x = 0 \<or> y = 0" (is "?lhs = ?rhs")
```
```   156 proof
```
```   157   assume ?lhs
```
```   158   then show ?rhs
```
```   159     by (metis cross_dot_cancel cross_zero_right inner_zero_right)
```
```   160 qed auto
```
```   161
```
```   162 lemma  bilinear_cross: "bilinear(\<times>)"
```
```   163   apply (auto simp add: bilinear_def linear_def)
```
```   164   apply unfold_locales
```
```   165   apply (simp add: cross_add_right)
```
```   166   apply (simp add: cross_mult_right)
```
```   167   apply (simp add: cross_add_left)
```
```   168   apply (simp add: cross_mult_left)
```
```   169   done
```
```   170
```
```   171 subsection   \<open>Preservation by rotation, or other orthogonal transformation up to sign\<close>
```
```   172
```
```   173 lemma  cross_matrix_mult: "transpose A *v ((A *v x) \<times> (A *v y)) = det A *\<^sub>R (x \<times> y)"
```
```   174   apply (simp add: vec_eq_iff   )
```
```   175   apply (simp add: vector_matrix_mult_def matrix_vector_mult_def forall_3 cross3_simps)
```
```   176   done
```
```   177
```
```   178 lemma  cross_orthogonal_matrix:
```
```   179   assumes "orthogonal_matrix A"
```
```   180   shows "(A *v x) \<times> (A *v y) = det A *\<^sub>R (A *v (x \<times> y))"
```
```   181 proof -
```
```   182   have "mat 1 = transpose (A ** transpose A)"
```
```   183     by (metis (no_types) assms orthogonal_matrix_def transpose_mat)
```
```   184   then show ?thesis
```
```   185     by (metis (no_types) vector_matrix_mul_rid vector_transpose_matrix cross_matrix_mult matrix_vector_mul_assoc matrix_vector_mult_scaleR)
```
```   186 qed
```
```   187
```
```   188 lemma  cross_rotation_matrix: "rotation_matrix A \<Longrightarrow> (A *v x) \<times> (A *v y) =  A *v (x \<times> y)"
```
```   189   by (simp add: rotation_matrix_def cross_orthogonal_matrix)
```
```   190
```
```   191 lemma  cross_rotoinversion_matrix: "rotoinversion_matrix A \<Longrightarrow> (A *v x) \<times> (A *v y) = - A *v (x \<times> y)"
```
```   192   by (simp add: rotoinversion_matrix_def cross_orthogonal_matrix scaleR_matrix_vector_assoc)
```
```   193
```
```   194 lemma  cross_orthogonal_transformation:
```
```   195   assumes "orthogonal_transformation f"
```
```   196   shows   "(f x) \<times> (f y) = det(matrix f) *\<^sub>R f(x \<times> y)"
```
```   197 proof -
```
```   198   have orth: "orthogonal_matrix (matrix f)"
```
```   199     using assms orthogonal_transformation_matrix by blast
```
```   200   have "matrix f *v z = f z" for z
```
```   201     using assms orthogonal_transformation_matrix by force
```
```   202   with cross_orthogonal_matrix [OF orth] show ?thesis
```
```   203     by simp
```
```   204 qed
```
```   205
```
```   206 lemma  cross_linear_image:
```
```   207    "\<lbrakk>linear f; \<And>x. norm(f x) = norm x; det(matrix f) = 1\<rbrakk>
```
```   208            \<Longrightarrow> (f x) \<times> (f y) = f(x \<times> y)"
```
```   209   by (simp add: cross_orthogonal_transformation orthogonal_transformation)
```
```   210
```
```   211 subsection \<open>Continuity\<close>
```
```   212
```
```   213 lemma  continuous_cross: "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. (f x) \<times> (g x))"
```
```   214   apply (subst continuous_componentwise)
```
```   215   apply (clarsimp simp add: cross3_simps)
```
```   216   apply (intro continuous_intros; simp)
```
```   217   done
```
```   218
```
```   219 lemma  continuous_on_cross:
```
```   220   fixes f :: "'a::t2_space \<Rightarrow> real^3"
```
```   221   shows "\<lbrakk>continuous_on S f; continuous_on S g\<rbrakk> \<Longrightarrow> continuous_on S (\<lambda>x. (f x) \<times> (g x))"
```
```   222   by (simp add: continuous_on_eq_continuous_within continuous_cross)
```
```   223
```
```   224 unbundle no_cross3_syntax
```
```   225
```
```   226 end
```
```   227
```