1 (* ========================================================================= *)
2 (* Cross products in real^3. *)
3 (* ========================================================================= *)
5 needs "Multivariate/topology.ml";;
9 (* ------------------------------------------------------------------------- *)
11 (* ------------------------------------------------------------------------- *)
13 parse_as_infix("cross",(20,"right"));;
15 let cross = new_definition
16 `(a:real^3) cross (b:real^3) =
17 vector [a$2 * b$3 - a$3 * b$2;
18 a$3 * b$1 - a$1 * b$3;
19 a$1 * b$2 - a$2 * b$1] :real^3`;;
21 (* ------------------------------------------------------------------------- *)
22 (* Some simple automation. *)
23 (* ------------------------------------------------------------------------- *)
26 SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
27 vector_add; vec; dot; cross; orthogonal; basis; DET_3;
28 vector_neg; vector_sub; vector_mul; ARITH] THEN
31 let VEC3_RULE tm = prove(tm,VEC3_TAC);;
33 (* ------------------------------------------------------------------------- *)
35 (* ------------------------------------------------------------------------- *)
37 let ORTHOGONAL_CROSS = prove
38 (`!x y. orthogonal (x cross y) x /\ orthogonal (x cross y) y /\
39 orthogonal x (x cross y) /\ orthogonal y (x cross y)`,
42 let CROSS_LZERO = prove
43 (`!x. (vec 0) cross x = vec 0`,
46 let CROSS_RZERO = prove
47 (`!x. x cross (vec 0) = vec 0`,
50 let CROSS_SKEW = prove
51 (`!x y. (x cross y) = --(y cross x)`,
54 let CROSS_REFL = prove
55 (`!x. x cross x = vec 0`,
58 let CROSS_LADD = prove
59 (`!x y z. (x + y) cross z = (x cross z) + (y cross z)`,
62 let CROSS_RADD = prove
63 (`!x y z. x cross (y + z) = (x cross y) + (x cross z)`,
66 let CROSS_LMUL = prove
67 (`!c x y. (c % x) cross y = c % (x cross y)`,
70 let CROSS_RMUL = prove
71 (`!c x y. x cross (c % y) = c % (x cross y)`,
74 let CROSS_LNEG = prove
75 (`!x y. (--x) cross y = --(x cross y)`,
78 let CROSS_RNEG = prove
79 (`!x y. x cross (--y) = --(x cross y)`,
82 let CROSS_LSUB = prove
83 (`!x y z. (x - y) cross z = x cross z - y cross z`,
86 let CROSS_RSUB = prove
87 (`!x y z. x cross (y - z) = x cross y - x cross z`,
90 let CROSS_JACOBI = prove
92 x cross (y cross z) + y cross (z cross x) + z cross (x cross y) = vec 0`,
95 let CROSS_LAGRANGE = prove
96 (`!x y z. x cross (y cross z) = (x dot z) % y - (x dot y) % z`,
99 let CROSS_TRIPLE = prove
100 (`!x y z. (x cross y) dot z = (y cross z) dot x`,
103 let DOT_CROSS_SELF = prove
104 (`(!x y. x dot (x cross y) = &0) /\
105 (!x y. x dot (y cross x) = &0) /\
106 (!x y. (x cross y) dot y = &0) /\
107 (!x y. (y cross x) dot y = &0)`,
110 let CROSS_COMPONENTS = prove
111 (`!x y. (x cross y)$1 = x$2 * y$3 - y$2 * x$3 /\
112 (x cross y)$2 = x$3 * y$1 - y$3 * x$1 /\
113 (x cross y)$3 = x$1 * y$2 - y$1 * x$2`,
116 let CROSS_BASIS = prove
117 (`(basis 1) cross (basis 2) = basis 3 /\
118 (basis 2) cross (basis 1) = --(basis 3) /\
119 (basis 2) cross (basis 3) = basis 1 /\
120 (basis 3) cross (basis 2) = --(basis 1) /\
121 (basis 3) cross (basis 1) = basis 2 /\
122 (basis 1) cross (basis 3) = --(basis 2)`,
125 let CROSS_BASIS_NONZERO = prove
127 ==> ~(u cross basis 1 = vec 0) \/
128 ~(u cross basis 2 = vec 0) \/
129 ~(u cross basis 3 = vec 0)`,
132 let CROSS_DOT_CANCEL = prove
134 x dot y = x dot z /\ x cross y = x cross z /\ ~(x = vec 0) ==> y = z`,
135 ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN REWRITE_TAC[GSYM DOT_EQ_0] THEN
138 let NORM_CROSS_DOT = prove
139 (`!x y. norm(x cross y) pow 2 + (x dot y) pow 2 = (norm(x) * norm y) pow 2`,
140 REWRITE_TAC[REAL_POW_MUL; NORM_POW_2] THEN VEC3_TAC);;
142 let DOT_CROSS_DET = prove
143 (`!x y z. x dot (y cross z) = det(vector[x;y;z]:real^3^3)`,
146 let CROSS_CROSS_DET = prove
147 (`!w x y z. (w cross x) cross (y cross z) =
148 det(vector[w;x;z]:real^3^3) % y -
149 det(vector[w;x;y]:real^3^3) % z`,
152 let DOT_CROSS = prove
153 (`!w x y z. (w cross x) dot (y cross z) =
154 (w dot y) * (x dot z) - (w dot z) * (x dot y)`,
157 let NORM_CROSS = prove
158 (`!x y. norm(x cross y) pow 2 =
159 norm(x) pow 2 * norm(y) pow 2 - (x dot y) pow 2`,
160 REWRITE_TAC[NORM_POW_2] THEN VEC3_TAC);;
162 let CROSS_EQ_0 = prove
163 (`!x y. x cross y = vec 0 <=> collinear{vec 0,x,y}`,
164 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM NORM_EQ_0] THEN
165 ONCE_REWRITE_TAC[REAL_RING `x = &0 <=> x pow 2 = &0`] THEN
166 REWRITE_TAC[NORM_CROSS; REAL_SUB_0; GSYM REAL_POW_MUL] THEN
167 REWRITE_TAC[GSYM REAL_EQ_SQUARE_ABS; GSYM NORM_CAUCHY_SCHWARZ_EQUAL] THEN
168 SIMP_TAC[real_abs; REAL_LE_MUL; NORM_POS_LE; EQ_SYM_EQ]);;
171 (`(!x. vec 0 cross x = vec 0) /\
172 (!x. x cross vec 0 = vec 0)`,
175 let CROSS_EQ_SELF = prove
176 (`(!x y. x cross y = x <=> x = vec 0) /\
177 (!x y. x cross y = y <=> y = vec 0)`,
178 MESON_TAC[ORTHOGONAL_CROSS; CROSS_0; ORTHOGONAL_REFL]);;
180 let NORM_AND_CROSS_EQ_0 = prove
181 (`!x y. x dot y = &0 /\ x cross y = vec 0 <=> x = vec 0 \/ y = vec 0`,
182 REPEAT GEN_TAC THEN ASM_CASES_TAC `x:real^3 = vec 0` THEN
183 ASM_REWRITE_TAC[CROSS_0; DOT_LZERO] THEN ASM_CASES_TAC `y:real^3 = vec 0` THEN
184 ASM_REWRITE_TAC[CROSS_0; DOT_RZERO] THEN
185 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
186 ASM_REWRITE_TAC[GSYM DOT_EQ_0; DOT_CROSS; REAL_MUL_LZERO] THEN
187 ASM_REWRITE_TAC[REAL_SUB_RZERO; REAL_ENTIRE; DOT_EQ_0]);;
189 let BILINEAR_CROSS = prove
191 REWRITE_TAC[linear; bilinear; CROSS_LADD; CROSS_RADD;
192 CROSS_LMUL; CROSS_RMUL]);;
194 (* ------------------------------------------------------------------------- *)
195 (* Preservation by rotation, or other orthogonal transformation up to sign. *)
196 (* ------------------------------------------------------------------------- *)
198 let CROSS_MATRIX_MUL = prove
199 (`!A x y. transp A ** ((A ** x) cross (A ** y)) = det A % (x cross y)`,
200 SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; SUM_3; matrix_vector_mul;
201 CROSS_COMPONENTS; LAMBDA_BETA; ARITH; transp; DET_3;
202 VECTOR_MUL_COMPONENT] THEN
205 let CROSS_ORTHOGONAL_MATRIX = prove
206 (`!A x y. orthogonal_matrix A
207 ==> (A ** x) cross (A ** y) = det A % (A ** (x cross y))`,
208 MP_TAC CROSS_MATRIX_MUL THEN
209 REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
210 REWRITE_TAC[orthogonal_matrix] THEN
211 DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
212 DISCH_THEN(MP_TAC o AP_TERM `matrix_vector_mul (A:real^3^3)`) THEN
213 ASM_REWRITE_TAC[MATRIX_VECTOR_MUL_ASSOC; MATRIX_VECTOR_MUL_LID] THEN
214 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[MATRIX_VECTOR_MUL_RMUL]);;
216 let CROSS_ROTATION_MATRIX = prove
217 (`!A x y. rotation_matrix A
218 ==> (A ** x) cross (A ** y) = A ** (x cross y)`,
219 SIMP_TAC[rotation_matrix; CROSS_ORTHOGONAL_MATRIX; VECTOR_MUL_LID]);;
221 let CROSS_ROTOINVERSION_MATRIX = prove
222 (`!A x y. rotoinversion_matrix A
223 ==> (A ** x) cross (A ** y) = --(A ** (x cross y))`,
224 SIMP_TAC[rotoinversion_matrix; CROSS_ORTHOGONAL_MATRIX; VECTOR_MUL_LID;
227 let CROSS_ORTHOGONAL_TRANSFORMATION = prove
229 orthogonal_transformation f
230 ==> (f x) cross (f y) = det(matrix f) % f(x cross y)`,
232 MP_TAC(ISPEC `matrix(f:real^3->real^3)` CROSS_ORTHOGONAL_MATRIX) THEN
233 REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
234 DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
236 [ASM_MESON_TAC[ORTHOGONAL_TRANSFORMATION_MATRIX;
237 ORTHOGONAL_TRANSFORMATION_LINEAR];
238 ASM_SIMP_TAC[MATRIX_WORKS; ORTHOGONAL_TRANSFORMATION_LINEAR]]);;
240 let CROSS_LINEAR_IMAGE = prove
241 (`!f x y. linear f /\ (!x. norm(f x) = norm x) /\ det(matrix f) = &1
242 ==> (f x) cross (f y) = f(x cross y)`,
243 SIMP_TAC[ORTHOGONAL_TRANSFORMATION; CONJ_ASSOC; VECTOR_MUL_LID;
244 CROSS_ORTHOGONAL_TRANSFORMATION]);;
246 (* ------------------------------------------------------------------------- *)
248 (* ------------------------------------------------------------------------- *)
250 let CONTINUOUS_CROSS = prove
252 f continuous net /\ g continuous net
253 ==> (\x. (f x) cross (g x)) continuous net`,
254 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[CONTINUOUS_COMPONENTWISE_LIFT] THEN
255 REWRITE_TAC[cross; VECTOR_3; DIMINDEX_3; FORALL_3; LIFT_SUB] THEN
256 REPEAT CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_SUB THEN
257 REWRITE_TAC[LIFT_CMUL] THEN CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_MUL THEN
258 ASM_SIMP_TAC[o_DEF; CONTINUOUS_LIFT_COMPONENT_COMPOSE]);;
260 let CONTINUOUS_ON_CROSS = prove
261 (`!f:real^N->real^3 g s.
262 f continuous_on s /\ g continuous_on s
263 ==> (\x. (f x) cross (g x)) continuous_on s`,
264 SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN; CONTINUOUS_CROSS]);;
266 (* ------------------------------------------------------------------------- *)
267 (* Prove a weaker variant for more convenient interface with functions *)
268 (* intended to work in 1 dimension. *)
269 (* ------------------------------------------------------------------------- *)
271 let CROSS_LINEAR_IMAGE_WEAK = prove
272 (`!f x y. linear f /\ (!x. norm(f x) = norm x) /\
273 (2 <= dimindex(:3) ==> det(matrix f) = &1)
274 ==> (f x) cross (f y) = f(x cross y)`,
275 REWRITE_TAC[DIMINDEX_3; ARITH] THEN
276 SIMP_TAC[ORTHOGONAL_TRANSFORMATION; CONJ_ASSOC; VECTOR_MUL_LID;
277 CROSS_ORTHOGONAL_TRANSFORMATION]);;
279 add_linear_invariants [CROSS_LINEAR_IMAGE_WEAK];;