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