colo12-c703.uibk.ac.at Git - Multivariate Analysis/.git/blob - Multivariate/cross.ml

   1 (* ========================================================================= *)
   2 (* Cross products in real^3.                                                 *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/topology.ml";;
   6
   7 prioritize_vector();;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* The definition.                                                           *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 parse_as_infix("cross",(20,"right"));;
  14
  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`;;
  20
  21 (* ------------------------------------------------------------------------- *)
  22 (* Some simple automation.                                                   *)
  23 (* ------------------------------------------------------------------------- *)
  24
  25 let VEC3_TAC =
  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
  29   CONV_TAC REAL_RING;;
  30
  31 let VEC3_RULE tm = prove(tm,VEC3_TAC);;
  32
  33 (* ------------------------------------------------------------------------- *)
  34 (* Basic lemmas.                                                             *)
  35 (* ------------------------------------------------------------------------- *)
  36
  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)`,
  40   VEC3_TAC);;
  41
  42 let CROSS_LZERO = prove
  43  (`!x. (vec 0) cross x = vec 0`,
  44   VEC3_TAC);;
  45
  46 let CROSS_RZERO = prove
  47  (`!x. x cross (vec 0) = vec 0`,
  48   VEC3_TAC);;
  49
  50 let CROSS_SKEW = prove
  51  (`!x y. (x cross y) = --(y cross x)`,
  52   VEC3_TAC);;
  53
  54 let CROSS_REFL = prove
  55  (`!x. x cross x = vec 0`,
  56   VEC3_TAC);;
  57
  58 let CROSS_LADD = prove
  59  (`!x y z. (x + y) cross z = (x cross z) + (y cross z)`,
  60   VEC3_TAC);;
  61
  62 let CROSS_RADD = prove
  63  (`!x y z. x cross (y + z) = (x cross y) + (x cross z)`,
  64   VEC3_TAC);;
  65
  66 let CROSS_LMUL = prove
  67  (`!c x y. (c % x) cross y = c % (x cross y)`,
  68   VEC3_TAC);;
  69
  70 let CROSS_RMUL = prove
  71  (`!c x y. x cross (c % y) = c % (x cross y)`,
  72   VEC3_TAC);;
  73
  74 let CROSS_LNEG = prove
  75  (`!x y. (--x) cross y = --(x cross y)`,
  76   VEC3_TAC);;
  77
  78 let CROSS_RNEG = prove
  79  (`!x y. x cross (--y) = --(x cross y)`,
  80   VEC3_TAC);;
  81
  82 let CROSS_LSUB = prove
  83  (`!x y z. (x - y) cross z = x cross z - y cross z`,
  84   VEC3_TAC);;
  85
  86 let CROSS_RSUB = prove
  87  (`!x y z. x cross (y - z) = x cross y - x cross z`,
  88   VEC3_TAC);;
  89
  90 let CROSS_JACOBI = prove
  91  (`!x y z.
  92     x cross (y cross z) + y cross (z cross x) + z cross (x cross y) = vec 0`,
  93   VEC3_TAC);;
  94
  95 let CROSS_LAGRANGE = prove
  96  (`!x y z. x cross (y cross z) = (x dot z) % y - (x dot y) % z`,
  97   VEC3_TAC);;
  98
  99 let CROSS_TRIPLE = prove
 100  (`!x y z.  (x cross y) dot z = (y cross z) dot x`,
 101   VEC3_TAC);;
 102
 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)`,
 108   VEC3_TAC);;
 109
 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`,
 114   VEC3_TAC);;
 115
 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)`,
 123   VEC3_TAC);;
 124
 125 let CROSS_BASIS_NONZERO = prove
 126  (`!u. ~(u = vec 0)
 127        ==> ~(u cross basis 1 = vec 0) \/
 128            ~(u cross basis 2 = vec 0) \/
 129            ~(u cross basis 3 = vec 0)`,
 130   VEC3_TAC);;
 131
 132 let CROSS_DOT_CANCEL = prove
 133  (`!x y z.
 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
 136   VEC3_TAC);;
 137
 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);;
 141
 142 let DOT_CROSS_DET = prove
 143  (`!x y z. x dot (y cross z) = det(vector[x;y;z]:real^3^3)`,
 144   VEC3_TAC);;
 145
 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`,
 150   VEC3_TAC);;
 151
 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)`,
 155   VEC3_TAC);;
 156
 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);;
 161
 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]);;
 169
 170 let CROSS_0 = prove
 171  (`(!x. vec 0 cross x = vec 0) /\
 172    (!x. x cross vec 0 = vec 0)`,
 173   VEC3_TAC);;
 174
 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]);;
 179
 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]);;
 188
 189 let BILINEAR_CROSS = prove
 190  (`bilinear(cross)`,
 191   REWRITE_TAC[linear; bilinear; CROSS_LADD; CROSS_RADD;
 192               CROSS_LMUL; CROSS_RMUL]);;
 193
 194 (* ------------------------------------------------------------------------- *)
 195 (* Preservation by rotation, or other orthogonal transformation up to sign.  *)
 196 (* ------------------------------------------------------------------------- *)
 197
 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
 203   REAL_ARITH_TAC);;
 204
 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]);;
 215
 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]);;
 220
 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;
 225            VECTOR_MUL_LNEG]);;
 226
 227 let CROSS_ORTHOGONAL_TRANSFORMATION = prove
 228  (`!f x y.
 229         orthogonal_transformation f
 230         ==> (f x) cross (f y) = det(matrix f) % f(x cross y)`,
 231   GEN_TAC THEN
 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
 235   ANTS_TAC THENL
 236    [ASM_MESON_TAC[ORTHOGONAL_TRANSFORMATION_MATRIX;
 237                   ORTHOGONAL_TRANSFORMATION_LINEAR];
 238     ASM_SIMP_TAC[MATRIX_WORKS; ORTHOGONAL_TRANSFORMATION_LINEAR]]);;
 239
 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]);;
 245
 246 (* ------------------------------------------------------------------------- *)
 247 (* Continuity.                                                               *)
 248 (* ------------------------------------------------------------------------- *)
 249
 250 let CONTINUOUS_CROSS = prove
 251  (`!net:(A)net f g.
 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]);;
 259
 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]);;
 265
 266 (* ------------------------------------------------------------------------- *)
 267 (* Prove a weaker variant for more convenient interface with functions       *)
 268 (* intended to work in 1 dimension.                                          *)
 269 (* ------------------------------------------------------------------------- *)
 270
 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]);;
 278
 279 add_linear_invariants [CROSS_LINEAR_IMAGE_WEAK];;