vectors_ext.ml

   1 (* ========================================================================= *)\r
   2 (*               Formalization of Electromagnetic Optics                     *)\r
   3 (*                                                                           *)\r
   4 (*            (c) Copyright, Sanaz Khan Afshar & Vincent Aravantinos 2011-14 *)\r
   5 (*                           Hardware Verification Group,                    *)\r
   6 (*                           Concordia University                            *)\r
   7 (*                                                                           *)\r
   8 (*                Contact:   <s_khanaf@encs.concordia.ca>                    *)\r
   9 (*                           <vincent@encs.concordia.ca>                     *)\r
  10 (*                                                                           *)\r
  11 (* Extentions of the vector library.                                         *)\r
  12 (* ========================================================================= *)\r
  13 \r
  14 \r
  15 prioritize_vector ();;\r
  16 \r
  17 (** Additions to euclidean space *)\r
  18 \r
  19 let [ORTHOGONAL_RZERO;ORTHOGONAL_RMUL;ORTHOGONAL_RNEG;ORTHOGONAL_RADD;\r
  20   ORTHOGONAL_RSUB;ORTHOGONAL_LZERO;ORTHOGONAL_LMUL;ORTHOGONAL_LNEG;\r
  21   ORTHOGONAL_LADD;ORTHOGONAL_LSUB] = \r
  22   CONJUNCTS ORTHOGONAL_CLAUSES;;\r
  23 \r
  24 let NON_VEC0 = prove\r
  25   (`!x:real^N. ~(x=vec 0) <=> ?i. 1 <= i /\ i <= dimindex(:N) /\ ~(x$i = &0)`,\r
  26   GEN_TAC THEN EQ_TAC THEN SIMP_TAC[vec;CART_EQ;LAMBDA_BETA]\r
  27   THEN ASM_MESON_TAC[]);;\r
  28 \r
  29 let NON_VEC0_DIM3 = prove\r
  30   (`!x:real^3. ~(x=vec 0) <=> ~(x$1= &0) \/ ~(x$2= &0) \/ ~(x$3= &0)`,\r
  31   REWRITE_TAC[NON_VEC0;DIMINDEX_3]\r
  32   THEN MESON_TAC[ARITH_RULE `1 <= i /\ i <= 3 <=> i = 1 \/ i = 2 \/ i = 3`]);;\r
  33 \r
  34 let ORTHOGONAL_SQR_NORM = prove\r
  35   (`!x y:real^N. orthogonal (x-y) y ==> x dot x = (x-y) dot (x-y) + y dot y`,\r
  36   REWRITE_TAC[orthogonal] THEN REPEAT STRIP_TAC\r
  37   THEN GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) \r
  38     [VECTOR_ARITH `x dot x = (x-y) dot (x-y) + y dot y + &2 * (x-y) dot y`]\r
  39   THEN ASM_REWRITE_TAC[REAL_MUL_RZERO;REAL_ADD_RID]);;\r
  40 \r
  41 let COLLINEAR_VEC0 = prove\r
  42   (`!s:real^N->bool. collinear s /\ vec 0 IN s ==> ?u. !x. x IN s\r
  43     ==> ?c. x = c %u`,\r
  44   REWRITE_TAC[collinear] THEN REPEAT (STRIP_TAC ORELSE EXISTS_TAC `u:real^N`)\r
  45   THEN ASM_MESON_TAC[VECTOR_SUB_RZERO]);;\r
  46 \r
  47 let CROSS_NORM_ORTHOGONAL = prove\r
  48   (`!x y. orthogonal x y ==> norm (x cross y) = norm x * norm y`,\r
  49   ONCE_REWRITE_TAC[GSYM (REWRITE_RULE[GSYM REAL_ABS_REFL] NORM_POS_LE)]\r
  50   THEN SIMP_TAC[GSYM REAL_ABS_MUL;REAL_EQ_SQUARE_ABS;GSYM NORM_CROSS_DOT;\r
  51     orthogonal;REAL_POW_2]\r
  52   THEN REAL_ARITH_TAC);;\r
  53 \r
  54 \r
  55 let COLLINEAR_DEPENDENT = prove\r
  56   (`!x y:real^N. ~(x=y) /\ collinear {vec 0,x,y} ==> dependent {x,y}`,\r
  57   REWRITE_TAC[collinear;dependent;IN_INSERT;IN_SING] THEN REPEAT STRIP_TAC\r
  58   THEN ASM_CASES_TAC `x=vec 0:real^N`\r
  59   THENL ON_FIRST_GOAL (ASM_MESON_TAC[SPAN_0])\r
  60   THEN ASM_CASES_TAC `y=vec 0:real^N`\r
  61   THENL ON_FIRST_GOAL (ASM_MESON_TAC[SPAN_0])\r
  62   THEN SUBGOAL_THEN `?c. x = c % y :real^N` STRIP_ASSUME_TAC THENL [\r
  63     FIRST_ASSUM (fun x -> MAP_EVERY (STRIP_ASSUME_TAC o\r
  64       REWRITE_RULE[IN_INSERT;IN_SING;VECTOR_SUB_RZERO] o C SPECL x) [\r
  65         [`x:real^N`;`vec 0:real^N`]; [`y:real^N`;`vec 0:real^N`]])\r
  66     THEN ASM_REWRITE_TAC[VECTOR_MUL_ASSOC;VECTOR_MUL_RCANCEL]\r
  67     THEN SUBGOAL_THEN `~(c'= &0)` ASSUME_TAC\r
  68     THENL [ ASM_MESON_TAC[VECTOR_MUL_LZERO]; EXISTS_TAC `c/c':real`\r
  69     THEN ASM_SIMP_TAC[REAL_DIV_RMUL] ];\r
  70     SUBGOAL_TAC "" `~(y=c%y:real^N)` [ASM_MESON_TAC[]]\r
  71     THEN EXISTS_TAC `c%y:real^N` \r
  72     THEN ASM_REWRITE_TAC[DELETE_INSERT;EMPTY_DELETE]\r
  73     THEN MESON_TAC[SUBSPACE_MUL;SUBSET;SPAN_INC;IN_SING;SUBSPACE_SPAN]\r
  74   ]);;\r
  75 \r
  76 let ORTHOGONAL_DIFFERENT = prove\r
  77   (`!x y:real^N. orthogonal x y /\ ~(x=vec 0) /\ ~(y=vec 0) ==> ~(x=y)`,\r
  78   REWRITE_TAC[orthogonal] THEN MESON_TAC[DOT_EQ_0]);;\r
  79 \r
  80 let ORTHOGONAL_NON_COLLINEAR = prove\r
  81   (`!x y:real^N. orthogonal x y /\ ~(x=vec 0) /\ ~(y=vec 0) \r
  82     ==> ~(collinear {vec 0,x,y})`,\r
  83   REPEAT STRIP_TAC\r
  84   THEN SUBGOAL_THEN `independent {x,y:real^N}` ASSUME_TAC THENL [\r
  85     MATCH_MP_TAC PAIRWISE_ORTHOGONAL_INDEPENDENT\r
  86     THEN REWRITE_TAC[pairwise;IN_INSERT;IN_SING]\r
  87     THEN ASM_MESON_TAC[ORTHOGONAL_SYM];\r
  88     POP_ASSUM (MP_TAC o REWRITE_RULE[independent])\r
  89     THEN REWRITE_TAC[] THEN MATCH_MP_TAC COLLINEAR_DEPENDENT\r
  90     THEN ASM_SIMP_TAC[ORTHOGONAL_DIFFERENT]\r
  91   ]);;\r
  92 \r
  93 (* NORMALIZING VECTORS *)\r
  94 \r
  95 let unit = new_definition `unit v = inv(norm v) % v`;;\r
  96 \r
  97 let UNIT_THM = prove\r
  98   (`!v. ~(v = vec 0) ==> norm(unit v) = &1`,\r
  99   SIMP_TAC[unit;NORM_MUL;REAL_ABS_INV;REAL_ABS_NORM;GSYM NORM_EQ_0;\r
 100     REAL_MUL_LINV]);;\r
 101 \r
 102 let UNIT_INTRO = prove\r
 103   (`!v. ~(v = vec 0) ==> v = norm v % unit v`,\r
 104   SIMP_TAC[unit;VECTOR_MUL_ASSOC;GSYM NORM_EQ_0;REAL_MUL_RINV;\r
 105     VECTOR_MUL_LID]);;\r
 106 \r
 107 let UNIT_ELIM = GSYM UNIT_INTRO;;\r
 108 \r
 109 let UNIT_ZERO = prove\r
 110   (`unit(vec 0) = vec 0`, REWRITE_TAC[unit;VECTOR_MUL_RZERO]);;\r
 111 \r
 112 let UNIT_EQ_ZERO = prove\r
 113   (`!v. unit v = vec 0 <=> v = vec 0`,\r
 114   REWRITE_TAC[unit;VECTOR_MUL_EQ_0;REAL_INV_EQ_0;NORM_EQ_0]);;\r
 115 \r
 116 let UNIT_UNIT = prove\r
 117   (`!v. ~(v = vec 0) ==> unit (unit v) = unit v`,\r
 118   SIMP_TAC[unit;UNIT_THM;REAL_INV_1;VECTOR_MUL_LID]);;\r
 119 \r
 120 let UNIT_DOT_UNIT_SELF = prove\r
 121   (`!v. ~(v = vec 0) ==> unit v dot unit v = &1`,\r
 122   SIMP_TAC[GSYM NORM_EQ_1;UNIT_THM]);;\r
 123 \r
 124 let DOT_UNIT_SELF = prove\r
 125   (`!v. ~(v=vec 0) ==> v dot unit v = norm v`,\r
 126   SIMP_TAC[MESON[UNIT_INTRO] `!v. ~(v = vec 0) ==>\r
 127     v dot unit v = (norm v % unit v) dot unit v`;DOT_LMUL;UNIT_DOT_UNIT_SELF;\r
 128       REAL_MUL_RID]);;\r
 129 \r
 130 let ORTHOGONAL_UNIT = prove\r
 131   (`!x y:real^N. (orthogonal x (unit y) <=> orthogonal x y)\r
 132     /\ (orthogonal (unit x) y <=> orthogonal x y)`,\r
 133   let common h =\r
 134     ASM_CASES_TAC h\r
 135     THENL [\r
 136       RULE_ASSUM_TAC (REWRITE_RULE[NORM_EQ_0]) THEN ASM_REWRITE_TAC[UNIT_ZERO];\r
 137       ASM_SIMP_TAC[unit;orthogonal;DOT_RMUL;DOT_LMUL;REAL_ENTIRE;REAL_INV_EQ_0]\r
 138     ]\r
 139   in\r
 140   REPEAT GEN_TAC THEN CONJ_TAC\r
 141   THENL [ common `norm (y:real^N) = &0`; common `norm (x:real^N) = &0` ]);;\r
 142 \r
 143 let ORTHOGONAL_RUNIT = prove\r
 144   (`!x y:real^N. orthogonal x (unit y) <=> orthogonal x y`,\r
 145   MESON_TAC[ORTHOGONAL_UNIT]);;\r
 146 \r
 147 let ORTHOGONAL_LUNIT = prove\r
 148   (`!x y:real^N. orthogonal (unit x) y <=> orthogonal x y`,\r
 149   MESON_TAC[ORTHOGONAL_UNIT]);;\r
 150 \r
 151 let ORTHOGONAL_LRUNIT = prove\r
 152   (`!x y:real^N. orthogonal (unit x) (unit y) <=> orthogonal x y`,\r
 153   MESON_TAC[ORTHOGONAL_UNIT]);;\r
 154 \r
 155 let COLLINEAR_UNIT = prove\r
 156   (`!x y:real^N. collinear {vec 0,x,y} <=> collinear {vec 0,unit x,unit y}`,\r
 157   REPEAT (STRIP_TAC ORELSE EQ_TAC) \r
 158   THEN ASM_CSQ_THEN (REWRITE_RULE[GSYM IMP_IMP] COLLINEAR_VEC0) \r
 159     (STRIP_ASSUME_TAC o REWRITE_RULE[IN_INSERT;IN_SING])\r
 160   THEN ASM_CSQ_THEN ~remove:true (MESON[] `(!x. x=a \/ x=b \/ x=c ==> p x) ==>\r
 161     p b /\ p c`) STRIP_ASSUME_TAC\r
 162   THENL [\r
 163     REWRITE_TAC[unit];\r
 164     MAP_EVERY ASM_CASES_TAC [`x=vec 0:real^N`;`y=vec 0:real^N`]\r
 165     THEN REPEAT (FIRST_X_ASSUM SUBST_VAR_TAC)\r
 166     THEN REWRITE_TAC[INSERT_AC;COLLINEAR_SING;COLLINEAR_2]\r
 167     THEN SUBGOAL_THEN `collinear {x:real^N, y, vec 0}\r
 168       <=> collinear {norm x % unit x, norm y % unit y, vec 0}` \r
 169       (SINGLE REWRITE_TAC)\r
 170     THENL ON_FIRST_GOAL (ASM_SIMP_TAC[GSYM UNIT_INTRO])\r
 171   ]\r
 172   THEN REWRITE_TAC[collinear;IN_INSERT;IN_SING]\r
 173   THEN EXISTS_TAC `u:real^N` THEN REPEAT STRIP_TAC\r
 174   THEN ASM_REWRITE_TAC[VECTOR_MUL_ASSOC;VECTOR_SUB_RZERO;VECTOR_SUB_LZERO;\r
 175     VECTOR_NEG_0;GSYM VECTOR_MUL_LNEG;GSYM VECTOR_SUB_RDISTRIB]\r
 176   THEN MESON_TAC[VECTOR_MUL_LZERO]);;\r
 177 \r
 178 let DOT_RUNIT_POS,DOT_LUNIT_POS = CONJ_PAIR(prove\r
 179   (`(!x y. &0 < x dot (unit y) <=> &0 < x dot y)\r
 180   /\ (!x y. &0 < (unit x) dot y <=> &0 < x dot y)`,\r
 181   REWRITE_TAC[unit;DOT_RMUL;DOT_LMUL;REAL_MUL_POS_LT;REAL_LT_INV_EQ;\r
 182     NORM_POS_LT;REWRITE_RULE[REAL_INV_NEG;REAL_NEG_GT0] \r
 183     (SPEC `--x:real` REAL_LT_INV_EQ);\r
 184     REWRITE_RULE[REWRITE_RULE[MESON[]`(p<=> ~q) <=> (q<=> ~p)`] real_lt] \r
 185     NORM_POS_LE]\r
 186   THEN MESON_TAC[DOT_RZERO;DOT_LZERO;REAL_LT_REFL]));;\r
 187 \r
 188 let DOT_RUNIT_EQ0,DOT_LUNIT_EQ0 = CONJ_PAIR(prove\r
 189   (`(!x y. x dot (unit y) = &0 <=> x dot y = &0) \r
 190   /\ (!x y. (unit x) dot y = &0 <=> x dot y = &0)`,\r
 191   REWRITE_TAC[GSYM orthogonal;ORTHOGONAL_LUNIT;ORTHOGONAL_RUNIT]));;\r
 192 \r
 193 let DOT_RUNIT_LT0,DOT_LUNIT_LT0 = CONJ_PAIR(prove\r
 194   (`(!x y. x dot (unit y) < &0 <=> x dot y < &0) \r
 195   /\ (!x y. (unit x) dot y < &0 <=> x dot y < &0)`,\r
 196   REWRITE_TAC[real_lt;MESON[] `(~p <=> ~q) <=> (p <=> q)`] \r
 197   THEN REWRITE_TAC[REAL_LE_LT]\r
 198   THEN MESON_TAC[DOT_RUNIT_EQ0;DOT_LUNIT_EQ0;DOT_RUNIT_POS;DOT_LUNIT_POS]));;\r
 199 \r
 200 let DOT_RUNIT_LE0,DOT_LUNIT_LE0 = CONJ_PAIR(prove\r
 201   (`(!x y. x dot (unit y) <= &0 <=> x dot y <= &0)\r
 202   /\ (!x y. (unit x) dot y <= &0 <=> x dot y <= &0)`,\r
 203   MESON_TAC[REAL_LE_LT;DOT_RUNIT_LT0;DOT_LUNIT_LT0;DOT_RUNIT_EQ0;\r
 204     DOT_LUNIT_EQ0]));;\r
 205 \r
 206 let DOT_RUNIT_GE0,DOT_LUNIT_GE0 = CONJ_PAIR(prove\r
 207   (`(!x y. &0 <= x dot (unit y) <=> &0 <= x dot y)\r
 208   /\ (!x y. &0 <= (unit x) dot y <=> &0 <= x dot y)`,\r
 209   REWRITE_TAC[REAL_LE_LT]\r
 210   THEN MESON_TAC[DOT_RUNIT_POS;DOT_LUNIT_POS;DOT_RUNIT_EQ0;DOT_LUNIT_EQ0]));;\r
 211 \r
 212 let DOT_RUNIT_EQ = prove\r
 213   (`!x y z:real^N. x dot (unit z) = y dot (unit z) <=> x dot z = y dot z`,\r
 214   REPEAT GEN_TAC THEN ASM_CASES_TAC `z=vec 0:real^N`\r
 215   THEN ASM_REWRITE_TAC[unit;DOT_RMUL;REAL_EQ_MUL_LCANCEL;REAL_INV_EQ_0;\r
 216     NORM_EQ_0;DOT_RZERO]);;\r
 217 \r
 218 let DOT_LUNIT_EQ = prove\r
 219   (`!x y z:real^N. (unit z) dot x = (unit z) dot y <=> z dot x = z dot y`,\r
 220   REPEAT GEN_TAC THEN ASM_CASES_TAC `z=vec 0:real^N`\r
 221   THEN ASM_REWRITE_TAC[unit;DOT_LMUL;REAL_EQ_MUL_LCANCEL;REAL_INV_EQ_0;\r
 222     NORM_EQ_0;DOT_LZERO]);;\r
 223 \r
 224 \r
 225 (* CONNECTION BETWEEN SPANS AND PLANES *)\r
 226 \r
 227 new_type_abbrev("point",`:real^3`);;\r
 228 new_type_abbrev("plane",`:point->bool`);;\r
 229 \r
 230 let PLANE_NON_EMPTY = prove\r
 231   (`!p:plane. plane p ==> ~(p={})`,\r
 232   REWRITE_TAC[plane;GSYM MEMBER_NOT_EMPTY] THEN REPEAT STRIP_TAC \r
 233   THEN EXISTS_TAC `u:point` \r
 234   THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC (REWRITE_RULE[SUBSET] HULL_SUBSET) \r
 235   THEN SET_TAC[]);;\r
 236 \r
 237 let is_plane_basis = new_definition\r
 238   `is_plane_basis s p <=>\r
 239     ?u v:real^3. s = {u,v} /\ ~(collinear {vec 0,u,v}) /\ !pt:point. pt IN p \r
 240       ==> !pt':point. pt' IN p <=> ?a b:real. pt' = pt + a % u + b % v`;;\r
 241 \r
 242 (* That theorem is (one of) the last which makes use of the affine definition of `plane` *)\r
 243 let EXISTS_PLANE_BASIS = prove\r
 244   (`!p. plane p ==> ?b. is_plane_basis b p`,\r
 245   GEN_TAC\r
 246   THEN DISCH_THEN (fun x -> \r
 247     STRIP_ASSUME_TAC (REWRITE_RULE[plane;AFFINE_HULL_3] x)\r
 248     THEN STRIP_ASSUME_TAC (MATCH_MP (REWRITE_RULE[GSYM MEMBER_NOT_EMPTY] \r
 249       PLANE_NON_EMPTY) x))\r
 250   THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[is_plane_basis] THEN DISCH_TAC\r
 251   THEN MAP_EVERY EXISTS_TAC [`{v-u,w-u:real^3}`;`v-u:real^3`; `w-u:real^3`]\r
 252   THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC \r
 253   THENL [\r
 254     ASM_MESON_TAC[INSERT_AC;COLLINEAR_3];\r
 255     POP_ASSUM MP_TAC THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT STRIP_TAC\r
 256     THEN EQ_TAC THEN STRIP_TAC\r
 257     THENL [\r
 258       RULE_ASSUM_TAC (REWRITE_RULE[REAL_ARITH `x+y+z= &1 <=> x= &1-y-z`])\r
 259       THEN MAP_EVERY EXISTS_TAC [`v''-v':real`; `w''-w':real`] \r
 260       THEN ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC;\r
 261       MAP_EVERY EXISTS_TAC [`u'-a-b:real`;`v'+a:real`;`w'+b:real`] \r
 262       THEN CONJ_TAC\r
 263       THENL [\r
 264         ASM_ARITH_TAC;\r
 265         REPLICATE_TAC 2 (POP_ASSUM MP_TAC) THEN VECTOR_ARITH_TAC]\r
 266     ]]);;\r
 267 \r
 268 \r
 269 let BASIS_NON_NULL = prove\r
 270   (`!p. plane p ==> !b. is_plane_basis b p ==> !u. u IN b ==> ~(u=vec 0)`,\r
 271   REWRITE_TAC[is_plane_basis] THEN REPEAT STRIP_TAC\r
 272   THEN SUBGOAL_THEN `(u':real^3) IN {u,v}` MP_TAC\r
 273   THENL ON_FIRST_GOAL (ASM_MESON_TAC[])\r
 274   THEN REWRITE_TAC[IN_INSERT;IN_SING]\r
 275   THEN ASM_MESON_TAC[INSERT_AC;COLLINEAR_2]);;\r
 276 \r
 277 let PAIR_SETS_EQ = prove\r
 278   (`!x y z t. {x,y} = {z,t} ==> (x=z /\ y=t) \/ (x=t /\ y=z)`,\r
 279   SET_TAC[]);;\r
 280 \r
 281 let NON_COLLINEAR3_IMPLIES_DIFFERENT = prove\r
 282   (`!x y z. ~(collinear {x,y,z}) ==> ~(x=y) /\ ~(y=z) /\ ~(x=z)`,\r
 283   MESON_TAC[COLLINEAR_2;INSERT_AC]);;\r
 284 \r
 285 let BASIS_DIFFERENT = prove\r
 286   (`!p. plane p ==> !u v. is_plane_basis {u,v} p ==> ~(u=v)`,\r
 287   REWRITE_TAC[is_plane_basis] THEN REPEAT STRIP_TAC\r
 288   THEN ASM_MESON_TAC[PAIR_SETS_EQ;NON_COLLINEAR3_IMPLIES_DIFFERENT]);;\r
 289 \r
 290 let UNIT_OF_BASIS_IS_BASIS = prove\r
 291   (`!p. plane p ==> !u v. is_plane_basis {u,v} p ==> is_plane_basis {unit u,unit v} p`,\r
 292   REPEAT STRIP_TAC THEN REWRITE_TAC[is_plane_basis]\r
 293   THEN MAP_EVERY EXISTS_TAC [`unit u:real^3`; `unit v:real^3`]\r
 294   THEN REWRITE_TAC[]\r
 295   THEN POP_ASSUM \r
 296     (DISTRIB [ASSUME_TAC;STRIP_ASSUME_TAC o REWRITE_RULE[is_plane_basis]])\r
 297   THEN ASM_REWRITE_TAC[GSYM COLLINEAR_UNIT]\r
 298   THEN ASM_CSQ_THEN ~remove:true PAIR_SETS_EQ STRIP_ASSUME_TAC\r
 299   THEN REPEAT (FIRST_X_ASSUM SUBST_VAR_TAC)\r
 300   THEN ASM_CSQ_THEN BASIS_NON_NULL (C ASM_CSQ_THEN (STRIP_ASSUME_TAC \r
 301     o REWRITE_RULE[IN_INSERT;IN_SING;\r
 302       MESON[]`(!u. u=a \/ u=b ==> p u) <=> p a /\ p b`]))\r
 303   THEN GEN_TAC \r
 304   THEN DISCH_THEN (fun x -> FIRST_X_ASSUM (ASSUME_TAC o C MATCH_MP x))\r
 305   THEN ASM_REWRITE_TAC[unit;VECTOR_MUL_ASSOC]\r
 306   THEN REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN ASM_REWRITE_TAC[]\r
 307   THENL [\r
 308     MAP_EVERY EXISTS_TAC [`a*norm(u':real^3)`;`b*norm(v':real^3)`] \r
 309     THEN RULE_ASSUM_TAC (REWRITE_RULE[GSYM NORM_EQ_0])\r
 310     THEN ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC;REAL_MUL_RINV] THEN VECTOR_ARITH_TAC;\r
 311     MESON_TAC[];\r
 312     MAP_EVERY EXISTS_TAC [`b*norm(v':real^3)`;`a*norm(u':real^3)`] \r
 313     THEN RULE_ASSUM_TAC (REWRITE_RULE[GSYM NORM_EQ_0])\r
 314     THEN ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC;REAL_MUL_RINV] THEN VECTOR_ARITH_TAC;\r
 315     MESON_TAC[VECTOR_ADD_AC];\r
 316   ]);;\r
 317 \r
 318 (* This theorem makes the connection between the (affine) notion of plane and the (vector) notion of span.\r
 319  * From now on, we can generally rely only on this result to reason about the spanning set of a plane.\r
 320  *)\r
 321 let PLANE_AS_SPAN = prove\r
 322   (`!p. plane p ==> !b. is_plane_basis b p ==> !pt:point. pt IN p \r
 323     ==> p = { pt + y | y IN span b }`,\r
 324   REWRITE_TAC[is_plane_basis] THEN REPEAT STRIP_TAC\r
 325   THEN ASM_REWRITE_TAC[EXTENSION;IN_ELIM_THM;SPAN_2;UNIV]\r
 326   THEN ASM_MESON_TAC[]);;\r
 327 \r
 328 let PLANE_SPAN = prove\r
 329   (`!p. plane p ==> !b. is_plane_basis b p ==> !pt:point. pt IN p\r
 330     ==> { pt' - pt | pt' IN p } = span b`,\r
 331   REPEAT STRIP_TAC THEN ASM_CSQ_THEN PLANE_AS_SPAN (C ASM_CSQ_THEN (C\r
 332     ASM_CSQ_THEN (SINGLE (GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV)))))\r
 333   THEN REWRITE_TAC[IN_ELIM_THM;EXTENSION] THEN GEN_TAC THEN EQ_TAC\r
 334   THENL [\r
 335     REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[VECTOR_ARITH `(x + y)-x = y:real^N`];\r
 336     DISCH_TAC THEN EXISTS_TAC `x+pt:real^3` THEN REWRITE_TAC (map VECTOR_ARITH\r
 337       [`(x + y) - y = x:real^N`; `x+z=z+y <=> x=y:real^N`]) THEN ASM_MESON_TAC[]\r
 338   ]);;\r
 339 \r
 340 let ALL_BASIS_SAME_SPAN = prove\r
 341   (`!p. plane p ==> !b1. is_plane_basis b1 p ==> !b2. is_plane_basis b2 p\r
 342     ==> span b1 = span b2`,\r
 343   REPEAT STRIP_TAC\r
 344   THEN ASM_CSQ_THEN PLANE_SPAN (fun x ->\r
 345     ASM_CSQ_THEN ~match_:false (SPEC `b1:real^3->bool` x) ASSUME_TAC\r
 346       THEN ASM_CSQ_THEN (SPEC `b2:real^3->bool` x) ASSUME_TAC)\r
 347   THEN ASM_MESON_TAC[PLANE_NON_EMPTY;MEMBER_NOT_EMPTY]);;\r
 348 \r
 349 let PLANE_SUBSPACE = prove\r
 350   (`!p. plane p ==> !pt:point. pt IN p ==> subspace { pt' - pt | pt' IN p }`,\r
 351   REPEAT STRIP_TAC THEN ASM_CSQ_THEN EXISTS_PLANE_BASIS STRIP_ASSUME_TAC\r
 352   THEN ASM_SIMP_TAC[PLANE_SPAN;SUBSPACE_SPAN]);;\r
 353 \r
 354 let PLANE_SING = prove\r
 355   (`!x:real^N. ~(plane{x})`,\r
 356   REWRITE_TAC[plane;NOT_EXISTS_THM;MESON[] `~(A/\B) <=> (A ==> ~B)`]\r
 357   THEN REPEAT STRIP_TAC \r
 358   THEN ASM_CSQ_THEN NON_COLLINEAR3_IMPLIES_DIFFERENT ASSUME_TAC\r
 359   THEN MATCH_MP_TAC (SET_RULE `~(u=v:real^N) /\ u IN {x} /\ v IN {x} ==> F`) \r
 360   THEN ASM_REWRITE_TAC[]\r
 361   THEN CONJ_TAC THEN MATCH_MP_TAC HULL_INC THEN SET_TAC[]);;\r
 362 \r
 363 let NON_COLLINEAR_INDEPENDENT = prove\r
 364   (`!x y:real^N. ~(collinear {vec 0,x,y}) ==> independent{x,y}`,\r
 365   MAP_EVERY (SINGLE ONCE_REWRITE_TAC) [independent;CONTRAPOS_THM;NOT_CLAUSES]\r
 366   THEN REPEAT GEN_TAC\r
 367   THEN ASM_CASES_TAC `x=y:real^N` THENL [\r
 368     ASM_REWRITE_TAC[INSERT_AC;COLLINEAR_2];\r
 369     REWRITE_TAC[dependent;IN_INSERT;IN_SING] THEN STRIP_TAC THENL\r
 370     let common main_var exist_list =\r
 371       POP_ASSUM MP_TAC\r
 372       THEN ASM_REWRITE_TAC[DELETE_INSERT;EMPTY_DELETE;SPAN_SING;IN_ELIM_THM;\r
 373         UNIV]\r
 374       THEN STRIP_TAC\r
 375       THEN REWRITE_TAC[collinear;IN_INSERT;IN_SING] THEN EXISTS_TAC main_var\r
 376       THEN REPEAT STRIP_TAC\r
 377       THENL map (fun t ->\r
 378         EXISTS_TAC t THEN ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC) exist_list\r
 379     in\r
 380     [ common `y:real^N`\r
 381         [`&0`;`--u:real`;`-- &1`;`u:real`;`&0`;`u- &1`;`&1`;`&1-u`;`&0`];\r
 382       common `x:real^N`\r
 383         [`&0`;`-- &1`;`--u:real`;`&1`;`&0`;`&1-u`;`u:real`;`u- &1`;`&0`]\r
 384     ]]);;\r
 385 \r
 386 let DIM_OF_PLANE_SPAN = prove\r
 387   (`!p:plane. plane p ==> !b. is_plane_basis b p ==> dim (span b) = 2`,\r
 388   REWRITE_TAC[is_plane_basis] THEN REPEAT STRIP_TAC \r
 389   THEN ASM_CSQ_THEN NON_COLLINEAR_INDEPENDENT ASSUME_TAC\r
 390   THEN ASM_CSQ_THEN NON_COLLINEAR3_IMPLIES_DIFFERENT ASSUME_TAC\r
 391   THEN SUBGOAL_THEN `{u,v:real^3} HAS_SIZE (dim (span {u,v}))` MP_TAC\r
 392   THENL [\r
 393     MATCH_MP_TAC BASIS_HAS_SIZE_DIM THEN ASM_REWRITE_TAC[];\r
 394     ASM_SIMP_TAC[HAS_SIZE;FINITE_INSERT;FINITE_EMPTY;CARD_CLAUSES;IN_INSERT;\r
 395     IN_SING;NOT_IN_EMPTY] THEN ARITH_TAC\r
 396   ]);;\r
 397 \r
 398 let DIM_OF_PLANE_SUBSPACE = prove\r
 399   (`!p. plane p ==> !pt:point. pt IN p ==> dim { pt' - pt | pt' IN p } = 2`,\r
 400   MESON_TAC[PLANE_SPAN;DIM_OF_PLANE_SPAN;EXISTS_PLANE_BASIS]);;\r
 401 \r
 402 let PLANE_SPAN_DECOMPOS = prove\r
 403   (`!p. plane p ==> !u v. is_plane_basis {u,v} p ==>\r
 404     !x. x IN span {u,v} <=> ?a b. x = a % u + b % v`,\r
 405   REPEAT STRIP_TAC THEN POP_ASSUM (SINGLE REWRITE_TAC o GSYM)\r
 406   THEN REWRITE_TAC[SPAN_2;IN_ELIM_THM;UNIV]);;\r
 407 \r
 408 let units = new_definition `units = { x | norm x = &1 }`;;\r
 409 \r
 410 let IN_UNITS = prove\r
 411   (`!x. x IN units ==> norm x = &1`,\r
 412   REWRITE_TAC[units;IN_ELIM_THM]);;\r
 413 \r
 414 let is_normal_to_plane = new_definition\r
 415   `is_normal_to_plane (n:real^3) (p:plane) <=> ~(n=vec 0)\r
 416   /\ !b. is_plane_basis b p ==> !v. v IN (span b) ==> orthogonal v n`;;\r
 417 \r
 418 let IS_NORMAL_TO_PLANE_UNIT = prove\r
 419   (`!p n. is_normal_to_plane (unit n) p <=> is_normal_to_plane n p`,\r
 420   REWRITE_TAC[is_normal_to_plane;ORTHOGONAL_RUNIT;UNIT_EQ_ZERO]);;\r
 421 \r
 422 let EXISTS_NORMAL_OF_PLANE = prove\r
 423   (`!p:plane. plane p ==> ?n:real^3. is_normal_to_plane n p`,\r
 424   REWRITE_TAC[is_normal_to_plane] THEN REPEAT STRIP_TAC\r
 425   THEN ASM_CSQ_THEN EXISTS_PLANE_BASIS (CHOOSE_THEN (fun x ->\r
 426     MAP_EVERY STRIP_ASSUME_TAC [x;REWRITE_RULE[is_plane_basis] x]))\r
 427   THEN EXISTS_TAC `u cross v` THEN ASM_REWRITE_TAC[CROSS_EQ_0] \r
 428   THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC\r
 429   THEN ASM_CSQ_THEN ALL_BASIS_SAME_SPAN (C (ASM_CSQ_THEN ~remove:true) (C\r
 430     ASM_CSQ_THEN (SINGLE REWRITE_TAC))) \r
 431   THEN ASM_REWRITE_TAC[SPAN_2;IN_ELIM_THM;UNIV]\r
 432   THEN REPEAT STRIP_TAC\r
 433   THEN ASM_REWRITE_TAC[orthogonal;DOT_LADD;DOT_LMUL;DOT_CROSS_SELF]\r
 434   THEN SIMPLE_COMPLEX_ARITH_TAC);;\r
 435 \r
 436 let NORMAL_OF_PLANE_IS_NORMAL_TO_BASIS = prove\r
 437   (`!p. plane p ==> !b. is_plane_basis b p ==> !u. u IN b ==>\r
 438     !n. is_normal_to_plane n p ==> orthogonal u n`,\r
 439   MESON_TAC[is_normal_to_plane;SPAN_SUPERSET;]);;\r
 440 \r
 441 let NORMAL_OF_PLANE_NON_NULL = prove\r
 442   (`!p. plane p ==> !n. is_normal_to_plane n p ==> ~(n=vec 0)`,\r
 443   MESON_TAC[is_normal_to_plane]);;\r
 444 \r
 445 let NORMAL_OF_PLANE_IS_ORTHOGONAL_TO_SEGMENT = prove\r
 446   (`!p. plane p ==> !n. is_normal_to_plane n p \r
 447     ==> !pt1 pt2. pt1 IN p /\ pt2 IN p ==> orthogonal (pt1-pt2) n`,\r
 448   REWRITE_TAC[is_normal_to_plane] THEN REPEAT STRIP_TAC \r
 449   THEN ASM_CSQ_THEN EXISTS_PLANE_BASIS STRIP_ASSUME_TAC\r
 450   THEN POP_ASSUM\r
 451     (fun x -> FIRST_X_ASSUM (MATCH_MP_TAC o C MATCH_MP x) THEN ASSUME_TAC x)\r
 452   THEN FIRST_X_ASSUM (STRIP_ASSUME_TAC o CONV_RULE (REWR_CONV is_plane_basis))\r
 453   THEN POP_ASSUM (C (ASM_CSQ_THEN ~remove:true) (fun x -> \r
 454     FIRST_X_ASSUM (STRIP_ASSUME_TAC o CONV_RULE (REWR_CONV x))))\r
 455   THEN ASM_REWRITE_TAC[SPAN_2;UNIV;IN_ELIM_THM;VECTOR_ARITH\r
 456     `(x+y+z)-x = y+z:real^N`]\r
 457   THEN MESON_TAC[]);;\r
 458 \r
 459 let DIM_OF_NORMAL_SPAN = prove\r
 460   (`!p:plane. plane p ==> !n. is_normal_to_plane n p ==> dim (span {n}) = 1`,\r
 461   REWRITE_TAC[is_normal_to_plane] THEN REPEAT STRIP_TAC \r
 462   THEN SUBGOAL_THEN `{n:real^3} HAS_SIZE dim (span {n})` MP_TAC \r
 463   THENL [\r
 464     MATCH_MP_TAC BASIS_HAS_SIZE_DIM \r
 465     THEN REWRITE_TAC[independent;dependent;NOT_EXISTS_THM;\r
 466       MESON[] `~(p/\q) <=> p ==> ~q`;IN_SING]\r
 467     THEN GEN_TAC THEN DISCH_TAC\r
 468     THEN ASM_REWRITE_TAC[DELETE_INSERT;EMPTY_DELETE;SPAN_EMPTY;IN_SING];\r
 469     ASM_SIMP_TAC[HAS_SIZE;FINITE_INSERT;FINITE_EMPTY;CARD_CLAUSES;IN_INSERT;\r
 470       IN_SING;NOT_IN_EMPTY]\r
 471     THEN ARITH_TAC]);;\r
 472 \r
 473 let DIM_OF_ORTHOGONAL = prove\r
 474   (`!p. plane p ==> !b. is_plane_basis b p \r
 475     ==> dim {z:real^3 | !x. x IN span b ==> orthogonal z x} = 1`,\r
 476   REPEAT STRIP_TAC\r
 477   THEN SUBGOAL_THEN\r
 478     `(:real^3) = { x+y \r
 479       | x IN span b /\ y IN {z:real^3 | !x. x IN span b ==> orthogonal z x}}`\r
 480   (ASSUME_TAC o REWRITE_RULE[DIM_UNIV;DIMINDEX_3] o \r
 481     AP_TERM `dim:(real^3->bool)->num`) \r
 482   THENL ON_FIRST_GOAL \r
 483     (REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ;SUBSET;UNIV;IN;IN_ELIM_THM] \r
 484     THEN MESON_TAC[ORTHOGONAL_SUBSPACE_DECOMP_EXISTS;IN])\r
 485   THEN SUBGOAL_THEN\r
 486     `span b\r
 487       INTER {z:real^3 | !x. x IN span b ==> orthogonal z x} SUBSET {vec 0}` \r
 488     (ASSUME_TAC o GSYM o REWRITE_RULE[GSYM DIM_EQ_0])\r
 489   THENL ON_FIRST_GOAL \r
 490     (REWRITE_TAC[INTER;SUBSET;IN_SING;IN_ELIM_THM]\r
 491     THEN MESON_TAC[ORTHOGONAL_REFL])\r
 492   THEN ASM_CSQ_THEN DIM_OF_PLANE_SPAN (fun x ->\r
 493     ASM_SIMP_TAC[ARITH_RULE `x=1 <=> 3+0=2+x`;GSYM x])\r
 494   THEN MATCH_MP_TAC DIM_SUMS_INTER\r
 495   THEN REWRITE_TAC[SUBSPACE_ORTHOGONAL_TO_VECTORS;ORTHOGONAL_SYM;\r
 496     SUBSPACE_SPAN]\r
 497   );;\r
 498 \r
 499 let NORMAL_SPAN_SUBSET_ORTHOGONAL_SUBSPACE = prove\r
 500   (`!p. plane p ==> !b. is_plane_basis b p ==> !n. is_normal_to_plane n p \r
 501     ==> span {n} SUBSET {z:real^3 | !x. x IN span b ==> orthogonal z x}`,\r
 502   REWRITE_TAC[is_normal_to_plane] THEN REPEAT STRIP_TAC \r
 503   THEN POP_ASSUM (C ASM_CSQ_THEN ASSUME_TAC)\r
 504   THEN REWRITE_TAC[SUBSET;SPAN_SING;IN_ELIM_THM;UNIV] \r
 505   THEN ASM_MESON_TAC[ORTHOGONAL_CLAUSES;ORTHOGONAL_SYM]);;\r
 506 \r
 507 let ORTHOGONAL_SUBSPACE_IS_NORMAL_SPAN = prove\r
 508   (`!p. plane p ==> !b. is_plane_basis b p ==> !n. is_normal_to_plane n p \r
 509     ==> {z:real^3 | !x. x IN span b ==> orthogonal z x} = span {n}`,\r
 510   MAP_EVERY (SINGLE ONCE_REWRITE_TAC) [\r
 511     ORTHOGONAL_SYM; MESON[SPAN_SPAN] `span{x}=span(span{x})`; \r
 512     GSYM (REWRITE_RULE[GSYM SPAN_EQ_SELF] SUBSPACE_ORTHOGONAL_TO_VECTORS)]\r
 513   THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_SYM \r
 514   THEN MATCH_MP_TAC DIM_EQ_SPAN THEN ONCE_REWRITE_TAC[ORTHOGONAL_SYM]\r
 515   THEN CONJ_TAC\r
 516   THENL ON_FIRST_GOAL (ASM_MESON_TAC[NORMAL_SPAN_SUBSET_ORTHOGONAL_SUBSPACE])\r
 517   THEN MAP_EVERY (fun x ->\r
 518     ASM_CSQ_THEN x (C ASM_CSQ_THEN (SINGLE REWRITE_TAC))) \r
 519     [DIM_OF_ORTHOGONAL;DIM_OF_NORMAL_SPAN]\r
 520   THEN ARITH_TAC);;\r
 521 \r
 522 let PLANE_DECOMP = prove\r
 523   (`!p. plane p ==> !b. is_plane_basis b p ==> !n. is_normal_to_plane n p \r
 524     ==> !v. ?w x. v = w + x % n /\ w IN span b`,\r
 525   REPEAT STRIP_TAC \r
 526   THEN MP_TAC (ISPEC `b:real^3->bool` ORTHOGONAL_SUBSPACE_DECOMP)\r
 527   THEN ASM_CSQ_THEN ORTHOGONAL_SUBSPACE_IS_NORMAL_SPAN \r
 528     (C ASM_CSQ_THEN (C ASM_CSQ_THEN (SINGLE REWRITE_TAC)))\r
 529   THEN REWRITE_TAC[SPAN_SING;IN_ELIM_THM;EXISTS_UNIQUE_DEF;EXISTS_PAIRED_THM]\r
 530   THEN MESON_TAC[]);;\r
 531 \r
 532 let NORMAL_ORTHOGONAL_IN_PLANE_SPAN = prove\r
 533   (`!p. plane p ==> !b. is_plane_basis b p ==> !n. is_normal_to_plane n p \r
 534     ==> !v. orthogonal v n <=> v IN span b`,\r
 535   let EQ_IMPLY =\r
 536     MATCH_MP (MESON[] `(!x y. p x y <=> q x y) ==> (!x y. p x y ==> q x y)`)\r
 537   in\r
 538   REPEAT STRIP_TAC\r
 539   THEN ASM_CSQ_THEN PLANE_DECOMP (C ASM_CSQ_THEN (C ASM_CSQ_THEN \r
 540     (STRIP_ASSUME_TAC o SPEC `v:real^3`)))\r
 541   THEN ASM_CSQ_THEN (EQ_IMPLY is_normal_to_plane) STRIP_ASSUME_TAC \r
 542   THEN POP_ASSUM (C ASM_CSQ_THEN ASSUME_TAC) THEN EQ_TAC THEN ASM_REWRITE_TAC[]\r
 543   THEN ASM_CSQ_THEN (EQ_IMPLY is_plane_basis) STRIP_ASSUME_TAC \r
 544   THEN RULE_ASSUM_TAC (REWRITE_RULE[orthogonal])\r
 545   THEN ASM_SIMP_TAC[orthogonal;DOT_LADD;DOT_LMUL;REAL_ADD_LID;REAL_ENTIRE;\r
 546     DOT_EQ_0;VECTOR_MUL_LZERO;VECTOR_ADD_RID] THEN ASM_MESON_TAC[]);;\r
 547 \r
 548 let PLANE_DECOMP_DOT_NORMAL = prove\r
 549   (`!p. plane p ==> !b. is_plane_basis b p ==> !n. is_normal_to_plane n p\r
 550     ==> !v. ?w. w IN span b /\ v = w + (v dot (unit n)) % (unit n)`,\r
 551   REPEAT STRIP_TAC\r
 552   THEN FIRST_ASSUM (ASSUME_TAC o CONJUNCT1 o CONV_RULE (REWR_CONV \r
 553     is_normal_to_plane))\r
 554   THEN ASM_CSQ_THEN (GSYM NORMAL_ORTHOGONAL_IN_PLANE_SPAN) (C ASM_CSQ_THEN \r
 555     (C ASM_CSQ_THEN ASSUME_TAC))\r
 556   THEN EXISTS_TAC `v - (v dot unit n) % unit n :real^3` \r
 557   THEN ASM_REWRITE_TAC[VECTOR_ARITH `x=x-y+z <=> y=z:real^N`] \r
 558   THEN ONCE_REWRITE_TAC[GSYM ORTHOGONAL_RUNIT]\r
 559   THEN REWRITE_TAC[orthogonal;DOT_LSUB;DOT_LMUL] \r
 560   THEN ASM_MESON_TAC[UNIT_DOT_UNIT_SELF;REAL_MUL_RID;REAL_SUB_0]);;\r
 561 \r
 562 let SUB_UNIT_NORMAL_IS_ORTHOGONAL_TO_NORMAL = prove\r
 563   (`!p. plane p ==> !n. is_normal_to_plane n p \r
 564     ==> !x. orthogonal (x - (x dot unit n) % unit n) n`,\r
 565   REPEAT STRIP_TAC THEN ASM_CSQ_THEN EXISTS_PLANE_BASIS STRIP_ASSUME_TAC\r
 566   THEN ASM_CSQ_THEN PLANE_DECOMP_DOT_NORMAL \r
 567     (C ASM_CSQ_THEN (C ASM_CSQ_THEN ASSUME_TAC))\r
 568   THEN RULE_ASSUM_TAC (REWRITE_RULE[VECTOR_ARITH `x=y+z <=> x-z=y`]) \r
 569   THEN ASM_MESON_TAC[NORMAL_ORTHOGONAL_IN_PLANE_SPAN]);;\r
 570 \r
 571 let is_orthogonal_plane_basis = new_definition\r
 572   `is_orthogonal_plane_basis b p \r
 573     <=> is_plane_basis b p /\ pairwise orthogonal b`;;\r
 574 \r
 575 let EXISTS_ORTHOGONAL_PLANE_BASIS = prove\r
 576   (`!p. plane p ==> ?b. is_orthogonal_plane_basis b p`,\r
 577   REWRITE_TAC[is_orthogonal_plane_basis;is_plane_basis] THEN REPEAT STRIP_TAC\r
 578   THEN ASM_CSQ_THEN EXISTS_PLANE_BASIS (CHOOSE_THEN (fun x -> ASSUME_TAC x\r
 579     THEN STRIP_ASSUME_TAC (REWRITE_RULE[is_plane_basis] x)))\r
 580   THEN ASM_CSQ_THEN EXISTS_NORMAL_OF_PLANE (CHOOSE_THEN (fun x ->\r
 581     let x' = REWRITE_RULE[is_normal_to_plane] x in\r
 582     ASSUME_TAC x THEN ASM_CSQ_THEN (CONJUNCT2 x') ASSUME_TAC\r
 583     THEN ASSUME_TAC (CONJUNCT1 x')))\r
 584   THEN SUBGOAL_TAC "" `~((u:real^3)=vec 0)` [ASM SET_TAC[BASIS_NON_NULL]]\r
 585   THEN SUBGOAL_TAC "" `orthogonal u (n:real^3)` [\r
 586     FIRST_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC SPAN_SUPERSET \r
 587     THEN ASM SET_TAC [SPAN_SUPERSET]\r
 588   ]\r
 589   THEN SUBGOAL_TAC "" `~(u cross n = vec 0)` [\r
 590     ASM_SIMP_TAC[CROSS_EQ_0;ORTHOGONAL_NON_COLLINEAR] ]\r
 591   THEN EXISTS_TAC `{u, u cross n}` THEN CONJ_TAC \r
 592   THENL [\r
 593     MAP_EVERY EXISTS_TAC [`u:real^3`;`u cross n`] THEN REWRITE_TAC[] \r
 594     THEN CONJ_TAC THENL ON_FIRST_GOAL \r
 595       (MATCH_MP_TAC ORTHOGONAL_NON_COLLINEAR \r
 596       THEN ASM_REWRITE_TAC[orthogonal;DOT_CROSS_SELF])\r
 597     THEN SUBGOAL_THEN `?a b. u cross n = a % u + b % v` STRIP_ASSUME_TAC \r
 598     THENL ON_FIRST_GOAL\r
 599       (ASM_MESON_TAC[GSYM PLANE_SPAN_DECOMPOS;\r
 600         GSYM NORMAL_ORTHOGONAL_IN_PLANE_SPAN;orthogonal;DOT_CROSS_SELF])\r
 601     THEN SUBGOAL_THEN `~(b'= &0)` (fun x -> POP_ASSUM MP_TAC THEN ASSUME_TAC x) \r
 602     THENL ON_FIRST_GOAL \r
 603       (ASM_CASES_TAC `a= &0` THENL [\r
 604         ASM_MESON_TAC[VECTOR_MUL_LZERO;VECTOR_ADD_LID];\r
 605         DISCH_THEN (fun x -> POP_ASSUM (fun y -> POP_ASSUM (MP_TAC \r
 606           o REWRITE_RULE[x;VECTOR_MUL_LZERO;VECTOR_ADD_RID]) \r
 607           THEN ASSUME_TAC y))\r
 608         THEN DISCH_THEN (MP_TAC o AP_TERM `(dot) (u:real^3)`) \r
 609         THEN REWRITE_TAC[DOT_CROSS_SELF;DOT_RMUL] \r
 610         THEN ONCE_REWRITE_TAC[EQ_SYM_EQ]\r
 611         THEN ASM_REWRITE_TAC[REAL_ENTIRE;DOT_EQ_0]\r
 612       ])\r
 613     THEN DISCH_THEN (fun x ->\r
 614       ASM_SIMP_TAC[x;VECTOR_ARITH `a%x+b%(c%x+d%y)=(a+b*c)%x+(b*d)%y`])\r
 615     THEN REPEAT STRIP_TAC THEN EQ_TAC THENL [\r
 616       REPEAT STRIP_TAC \r
 617       THEN MAP_EVERY EXISTS_TAC [`a'-b''/b'*a:real`;`b''/b':real`]\r
 618       THEN ASM_SIMP_TAC[REAL_SUB_ADD;VECTOR_ARITH `x+y=x+z <=> y=z`;\r
 619         REAL_DIV_RMUL];\r
 620       MESON_TAC[];\r
 621     ];\r
 622     REWRITE_TAC[pairwise;orthogonal] THEN SET_TAC [DOT_CROSS_SELF]\r
 623   ]);;\r
 624 \r
 625 let ORTHOGONAL_PLANE_BASIS_AS_PAIR = prove\r
 626   (`!b p. is_orthogonal_plane_basis b p ==> ?u v. is_orthogonal_plane_basis {u,v} p`,\r
 627   MESON_TAC[is_orthogonal_plane_basis;is_plane_basis]);;\r
 628 \r
 629 let BASIS_OF_PLANE_ORTHONORMAL_DECOMPOS = prove\r
 630   (`!p. plane p ==> !u v. is_orthogonal_plane_basis {u,v} p ==>\r
 631   !x. x IN span {u,v}\r
 632     <=> x = (x dot unit u) % unit u + (x dot unit v) % unit v`,\r
 633   REWRITE_TAC [is_orthogonal_plane_basis] THEN REPEAT STRIP_TAC\r
 634   THEN ASM_CSQ_THEN PLANE_SPAN_DECOMPOS (C ASM_CSQ_THEN (SINGLE REWRITE_TAC))\r
 635   THEN EQ_TAC THENL [\r
 636     REPEAT STRIP_TAC\r
 637     THEN SUBGOAL_TAC "" `~(u = vec 0:real^3) /\ ~(v = vec 0:real^3)` \r
 638       [ASM_MESON_TAC[BASIS_NON_NULL;IN_INSERT]]\r
 639     THEN SUBGOAL_THEN\r
 640       `orthogonal (u:real^3) (unit v) /\ orthogonal v (unit u)` \r
 641       (ASSUME_TAC o REWRITE_RULE[orthogonal]) \r
 642     THENL ON_FIRST_GOAL \r
 643       (RULE_ASSUM_TAC (REWRITE_RULE[pairwise;orthogonal])\r
 644       THEN REWRITE_TAC[ORTHOGONAL_UNIT;orthogonal]\r
 645       THEN SUBGOAL_TAC "" `~(u=v:real^3)` [ASM_MESON_TAC[BASIS_DIFFERENT]]\r
 646       THEN CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASSUM_LIST SET_TAC)\r
 647     THEN ASM_SIMP_TAC[DOT_LADD;DOT_LMUL;REAL_MUL_RZERO;REAL_ADD_RID;\r
 648       REAL_ADD_LID;DOT_UNIT_SELF;GSYM VECTOR_MUL_ASSOC;GSYM UNIT_INTRO];\r
 649     REWRITE_TAC[unit;VECTOR_MUL_ASSOC] THEN MESON_TAC[]\r
 650   ]);;\r
 651 \r
 652 let PLANE_DECOMP_DOT = prove\r
 653   (`!p:plane. plane p ==> !u v. is_orthogonal_plane_basis {u,v} p \r
 654     ==> !n. is_normal_to_plane n p ==> !x:real^3.\r
 655       x = (x dot unit u) % unit u + (x dot unit v) % unit v\r
 656         + (x dot unit n) % unit n`,\r
 657   REPEAT STRIP_TAC\r
 658   THEN FIRST_ASSUM (STRIP_ASSUME_TAC o CONV_RULE (REWR_CONV \r
 659     is_orthogonal_plane_basis))\r
 660   THEN ASM_CSQ_THEN PLANE_DECOMP_DOT_NORMAL \r
 661     (C ASM_CSQ_THEN (C ASM_CSQ_THEN (STRIP_ASSUME_TAC o SPEC `x:real^3`)))\r
 662   THEN SUBGOAL_THEN\r
 663     `(x:real^3) dot unit u = w dot unit u /\ x dot unit v = w dot unit v`\r
 664     ASSUME_TAC\r
 665   THENL ON_FIRST_GOAL\r
 666   begin\r
 667     SUBGOAL_THEN `(u:real^3) IN {u,v} /\ v IN {u,v}` STRIP_ASSUME_TAC \r
 668     THENL ON_FIRST_GOAL (ASSUM_LIST SET_TAC)\r
 669     THEN ASM_CSQ_THEN NORMAL_OF_PLANE_IS_NORMAL_TO_BASIS \r
 670       (C ASM_CSQ_THEN ASSUME_TAC)\r
 671     THEN POP_ASSUM (fun x -> ASM_CSQ_THEN ~remove:true x \r
 672       (C ASM_CSQ_THEN ASSUME_TAC) \r
 673       THEN ASM_CSQ_THEN x (C ASM_CSQ_THEN ASSUME_TAC))\r
 674     THEN RULE_ASSUM_TAC (REWRITE_RULE[orthogonal] \r
 675       o ONCE_REWRITE_RULE[GSYM ORTHOGONAL_LRUNIT]\r
 676       o ONCE_REWRITE_RULE[ORTHOGONAL_SYM])\r
 677     THEN ASM ONCE_REWRITE_TAC[]\r
 678     THEN ASM_REWRITE_TAC[DOT_LADD;DOT_LMUL;REAL_MUL_RZERO;REAL_ADD_RID]\r
 679   end\r
 680   THEN ASM_CSQ_THEN (REWRITE_RULE[GSYM IMP_IMP] \r
 681     BASIS_OF_PLANE_ORTHONORMAL_DECOMPOS) (C ASM_CSQ_THEN (ASSUME_TAC\r
 682       o SPEC `w:real^3`))\r
 683   THEN ASSUM_LIST (GEN_REWRITE_TAC (RATOR_CONV o DEPTH_CONV))\r
 684   THEN ASM_REWRITE_TAC[VECTOR_ARITH `x+y=z+t+y <=> x=z+t`]\r
 685   THEN ASM_MESON_TAC[]);;\r
 686 \r
 687 let UNIT_OF_ORTHOGONAL_BASIS_IS_ORTHOGONAL_BASIS = prove\r
 688   (`!p. plane p ==> !u v. is_orthogonal_plane_basis {u,v} p \r
 689     ==> is_orthogonal_plane_basis {unit u,unit v} p`,\r
 690   SIMP_TAC[is_orthogonal_plane_basis;UNIT_OF_BASIS_IS_BASIS;pairwise;IN_INSERT;\r
 691     IN_SING]\r
 692   THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]\r
 693   THEN ASM_MESON_TAC[ORTHOGONAL_LRUNIT]);;\r
 694 \r
 695 let EXISTS_UNIT_ORTHOGONAL_PLANE_BASIS = prove\r
 696   (`!p. plane p ==> ?u v. is_orthogonal_plane_basis {unit u,unit v} p`,\r
 697   REPEAT STRIP_TAC\r
 698   THEN ASM_CSQ_THEN EXISTS_ORTHOGONAL_PLANE_BASIS (CHOOSE_THEN\r
 699     (DISTRIB (map (fun xs -> STRIP_ASSUME_TAC o REWRITE_RULE xs) [\r
 700       [];\r
 701       [is_orthogonal_plane_basis];\r
 702       [is_orthogonal_plane_basis;is_plane_basis]])))\r
 703   THEN FIRST_X_ASSUM SUBST_VAR_TAC \r
 704   THEN ASM_MESON_TAC[UNIT_OF_ORTHOGONAL_BASIS_IS_ORTHOGONAL_BASIS]);;\r
 705 \r
 706 let FORALL_PLANE_THM = prove\r
 707   (`!p. plane p ==>\r
 708     ?u v. is_orthogonal_plane_basis {unit u,unit v} p /\ !P pt0. pt0 IN p \r
 709       ==> ((!pt. pt IN p ==> P pt)\r
 710         <=> (!a b. P (pt0 + a % unit u + b % unit v)))`,\r
 711   REPEAT STRIP_TAC \r
 712   THEN ASM_CSQ_THEN EXISTS_UNIT_ORTHOGONAL_PLANE_BASIS (CHOOSE_THEN \r
 713     (CHOOSE_THEN (DISTRIB (map (fun xs -> STRIP_ASSUME_TAC o REWRITE_RULE xs) [\r
 714       [];\r
 715       [is_orthogonal_plane_basis];\r
 716       [is_orthogonal_plane_basis;is_plane_basis]]))))\r
 717   THEN MAP_EVERY EXISTS_TAC [`u:real^3`;`v:real^3`]\r
 718   THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC\r
 719   THEN ASM_CSQ_THEN PAIR_SETS_EQ STRIP_ASSUME_TAC\r
 720   THEN REPEAT (FIRST_X_ASSUM SUBST_VAR_TAC)\r
 721   THEN ASM_CSQ_THEN PLANE_AS_SPAN (C ASM_CSQ_THEN (C ASM_CSQ_THEN (ASSUME_TAC\r
 722     o REWRITE_RULE[SPAN_2;UNIV;IN_ELIM_THM]))) \r
 723   THEN ASSUM_LIST SET_TAC);;\r
 724 \r
 725 let FORALL_PLANE_THM_2 = prove\r
 726   (`!p. plane p ==>\r
 727     ?u v pt0. is_orthogonal_plane_basis {unit u,unit v} p /\ pt0 IN p\r
 728     /\ !P. (!pt. pt IN p ==> P pt)\r
 729       <=> (!a b. P (pt0 + a % unit u + b % unit v))`,\r
 730   REPEAT STRIP_TAC THEN ASM_CSQ_THEN FORALL_PLANE_THM STRIP_ASSUME_TAC\r
 731   THEN ASM_CSQ_THEN PLANE_NON_EMPTY (STRIP_ASSUME_TAC o REWRITE_RULE[GSYM MEMBER_NOT_EMPTY]) THEN ASM_MESON_TAC[]);;\r
 732 \r
 733 (** Is u the projection of v on the hyperplane represented by the non-null vector w? *)\r
 734 let is_projection_on_hyperplane = new_definition\r
 735   `is_projection_on_hyperplane u v (w:real^N)\r
 736   <=> norm w = &1 ==> u = v - (v dot w) % w`;;\r
 737 \r
 738 let projection_on_hyperplane = new_definition\r
 739   `projection_on_hyperplane v w = @u. is_projection_on_hyperplane u v w`;;\r
 740 \r
 741 let PROJECTION_ON_HYPERPLANE_THM = prove\r
 742   (`!v w. norm w = &1 \r
 743     ==> projection_on_hyperplane v w = v - (v dot w) % w`,\r
 744   REWRITE_TAC[projection_on_hyperplane;is_projection_on_hyperplane]\r
 745   THEN SELECT_ELIM_TAC THEN MESON_TAC[]);;\r
 746 \r
 747 let PROJECTION_ON_HYPERPLANE_THM_LNEG = prove\r
 748   (`!v w. norm w = &1 \r
 749     ==> projection_on_hyperplane (--v) w = --(projection_on_hyperplane v w)`,\r
 750   SIMP_TAC[PROJECTION_ON_HYPERPLANE_THM;VECTOR_NEG_SUB;DOT_LNEG;\r
 751     VECTOR_MUL_LNEG]\r
 752   THEN REPEAT STRIP_TAC THEN VECTOR_ARITH_TAC);;\r
 753 \r
 754 let PROJECTION_ON_HYPERPLANE_DECOMPOS = prove\r
 755   (`!v w. norm w = &1 ==> projection_on_hyperplane v w + (v dot w) % w = v`, \r
 756   SIMP_TAC[projection_on_hyperplane;is_projection_on_hyperplane]\r
 757   THEN REPEAT STRIP_TAC THEN VECTOR_ARITH_TAC);;\r
 758 \r
 759 let symetric_vectors_wrt = new_definition\r
 760   `symetric_vectors_wrt u v (w:real^3) \r
 761     <=> norm w = &1 ==> u + v = (&2 * u dot w) % w`;;\r
 762 \r
 763 let SYMETRIC_VECTORS_WRT_SYM = prove\r
 764   (`!u v w. symetric_vectors_wrt u v w <=> symetric_vectors_wrt v u w`,\r
 765   REWRITE_TAC[symetric_vectors_wrt] THEN REPEAT GEN_TAC THEN EQ_TAC\r
 766   THEN DISCH_THEN (fun x -> DISCH_THEN (DISTRIB (map ((o) ASSUME_TAC)\r
 767     [MP x; REWRITE_RULE[NORM_EQ_1]])))\r
 768   THEN ASSUM_LIST (GEN_REWRITE_TAC (RAND_CONV o DEPTH_CONV)\r
 769     o map (REWRITE_RULE[VECTOR_ARITH `x+y=z <=> y=z-x:real^N`]))\r
 770   THEN ASM_REWRITE_TAC[DOT_LSUB;DOT_LMUL;REAL_ARITH `(&2 * x) * &1 - x = x`]\r
 771   THEN ONCE_REWRITE_TAC[VECTOR_ADD_SYM] THEN ASM_REWRITE_TAC[]);;\r
 772 \r
 773 let SYMETRIC_VECTORS_PROJECTION_ON_HYPERPLANE = prove\r
 774   (`!u v w. norm w = &1 ==> symetric_vectors_wrt u v w \r
 775     ==> --(projection_on_hyperplane v w) = projection_on_hyperplane u w`,\r
 776   ONCE_REWRITE_TAC[MATCH_MP (MESON[] `(p <=> q) ==> (p <=> p /\ q)`) \r
 777     (SPEC_ALL SYMETRIC_VECTORS_WRT_SYM)]\r
 778   THEN SIMP_TAC[symetric_vectors_wrt;projection_on_hyperplane;\r
 779     is_projection_on_hyperplane;\r
 780     VECTOR_ARITH `x = (&2 * y) % z <=> y%z = inv(&2) % x`]\r
 781   THEN REPEAT STRIP_TAC THEN VECTOR_ARITH_TAC);;\r
 782 \r
 783 let SYMETRIC_VECTORS_PROJECTION_ON_AXIS = prove\r
 784   (`!u v w. norm w = &1 ==> symetric_vectors_wrt u v w ==> u dot w = v dot w`,\r
 785   REPEAT STRIP_TAC\r
 786   THEN ASM_CSQ_THEN (GEQ_IMP SYMETRIC_VECTORS_WRT_SYM) ASSUME_TAC \r
 787   THEN REPEAT (POP_ASSUM MP_TAC) THEN SIMP_TAC[symetric_vectors_wrt]\r
 788   THEN REWRITE_TAC[IMP_IMP;GSYM CONJ_ASSOC;REAL_EQ_MUL_LCANCEL;\r
 789     VECTOR_ARITH `u+v=w /\ v+u=x <=> u+v=x /\ x=w`;VECTOR_MUL_RCANCEL]\r
 790   THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[DOT_RZERO] THEN POP_ASSUM MP_TAC\r
 791   THEN REAL_ARITH_TAC);;\r
 792 \r
 793 \r
 794 (** Additions to affine spaces *)\r
 795 \r
 796 let AFFINE_HULL_3_ZERO = prove\r
 797   (`affine hull {vec 0, a, b} = {u % a + v % b | u IN (:real) /\ v IN(:real)}`,\r
 798   REWRITE_TAC[AFFINE_HULL_3;UNIV;EXTENSION;IN_ELIM_THM;VECTOR_MUL_RZERO;\r
 799     VECTOR_ADD_LID;REAL_ARITH `x+y+z=t <=> x=t-y-z:real`]\r
 800   THEN MESON_TAC[]);;\r
 801 \r
 802 let LSUB_PLANE_EQ_RSUB_PLANE = prove\r
 803   (`!p:plane. plane p ==> !x. x IN p ==> {y - x | y IN p} = {x - y | y IN p}`,\r
 804   let COMMON_TAC t =\r
 805     EXISTS_TAC t THEN CONJ_TAC THEN TRY VECTOR_ARITH_TAC\r
 806     THEN SUBGOAL_TAC "" `(x':real^3) IN span b` [ASM SET_TAC []]\r
 807   in\r
 808   REWRITE_TAC[GSPEC;SETSPEC;FUN_EQ_THM] THEN REPEAT STRIP_TAC\r
 809   THEN ASM_CSQ_THEN EXISTS_PLANE_BASIS STRIP_ASSUME_TAC\r
 810   THEN ASM_CSQS_THEN PLANE_AS_SPAN ASSUME_TAC THEN EQ_TAC THENL [\r
 811     ASM_CSQS_THEN PLANE_SPAN ASSUME_TAC THEN STRIP_TAC \r
 812     THEN COMMON_TAC `x-x':point` THEN REWRITE_TAC[VECTOR_SUB]\r
 813     THEN POP_ASSUM (ASSUME_TAC o MATCH_MP SPAN_NEG) \r
 814     THEN ASSUM_LIST (FIRST o List.rev_map (CHANGED_TAC o SINGLE REWRITE_TAC)) \r
 815     THEN ASSUM_LIST SET_TAC;\r
 816     STRIP_TAC THEN ASM_CSQS_THEN PLANE_SPAN ASSUME_TAC \r
 817     THEN COMMON_TAC `x+x':point` THEN ASSUM_LIST SET_TAC]);;\r
 818 \r
 819 let EXISTS_MULTIPLE_OF_NORMAL_IN_PLANE = prove\r
 820   (`!p:plane. plane p ==> !n. is_normal_to_plane n p ==> ?a. a % unit n IN p`,\r
 821   REPEAT STRIP_TAC\r
 822   THEN ASM_CSQ_THEN PLANE_NON_EMPTY (STRIP_ASSUME_TAC \r
 823     o REWRITE_RULE[GSYM MEMBER_NOT_EMPTY])\r
 824   THEN ASM_CSQ_THEN EXISTS_PLANE_BASIS STRIP_ASSUME_TAC\r
 825   THEN ASM_CSQS_THEN (GSYM PLANE_SPAN) (fun x -> \r
 826     ASM_CSQS_THEN PLANE_DECOMP_DOT_NORMAL \r
 827     (MP_TAC o SPEC `x:point` o REWRITE_RULE[x]))\r
 828   THEN ASM_SIMP_TAC[LSUB_PLANE_EQ_RSUB_PLANE] THEN REWRITE_TAC[IN_ELIM_THM]\r
 829   THEN STRIP_TAC THEN EXISTS_TAC `(x:point) dot unit n`\r
 830   THEN MATCH_MP_TAC (MESON[] `(pt':point) IN p /\ pt' = y ==> y IN p`) \r
 831   THEN ASM_REWRITE_TAC[] THEN REPLICATE_TAC 2 (POP_ASSUM MP_TAC)\r
 832   THEN VECTOR_ARITH_TAC);;\r
 833 \r
 834 (* Additional functions *)\r
 835 let map_triple = new_definition `map_triple (f:A->B) (x1,x2,x3) = (f x1,f x2,f x3)`;;\r