100/desargues.ml

   1 (* ========================================================================= *)
   2 (* #87: Desargues's theorem.                                                 *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/cross.ml";;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* A lemma we want to justify some of the axioms.                            *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let NORMAL_EXISTS = prove
  12  (`!u v:real^3. ?w. ~(w = vec 0) /\ orthogonal u w /\ orthogonal v w`,
  13   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[ORTHOGONAL_SYM] THEN
  14   MP_TAC(ISPEC `{u:real^3,v}` ORTHOGONAL_TO_SUBSPACE_EXISTS) THEN
  15   REWRITE_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY; DIMINDEX_3] THEN
  16   DISCH_THEN MATCH_MP_TAC THEN MATCH_MP_TAC LET_TRANS THEN
  17   EXISTS_TAC `CARD {u:real^3,v}` THEN CONJ_TAC THEN
  18   SIMP_TAC[DIM_LE_CARD; FINITE_INSERT; FINITE_EMPTY] THEN
  19   SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN ARITH_TAC);;
  20
  21 (* ------------------------------------------------------------------------- *)
  22 (* Type of directions.                                                       *)
  23 (* ------------------------------------------------------------------------- *)
  24
  25 let direction_tybij = new_type_definition "direction" ("mk_dir","dest_dir")
  26  (MESON[BASIS_NONZERO; LE_REFL; DIMINDEX_GE_1] `?x:real^3. ~(x = vec 0)`);;
  27
  28 parse_as_infix("||",(11,"right"));;
  29 parse_as_infix("_|_",(11,"right"));;
  30
  31 let perpdir = new_definition
  32  `x _|_ y <=> orthogonal (dest_dir x) (dest_dir y)`;;
  33
  34 let pardir = new_definition
  35  `x || y <=> (dest_dir x) cross (dest_dir y) = vec 0`;;
  36
  37 let DIRECTION_CLAUSES = prove
  38  (`((!x. P(dest_dir x)) <=> (!x. ~(x = vec 0) ==> P x)) /\
  39    ((?x. P(dest_dir x)) <=> (?x. ~(x = vec 0) /\ P x))`,
  40   MESON_TAC[direction_tybij]);;
  41
  42 let [PARDIR_REFL; PARDIR_SYM; PARDIR_TRANS] = (CONJUNCTS o prove)
  43  (`(!x. x || x) /\
  44    (!x y. x || y <=> y || x) /\
  45    (!x y z. x || y /\ y || z ==> x || z)`,
  46   REWRITE_TAC[pardir; DIRECTION_CLAUSES] THEN VEC3_TAC);;
  47
  48 let PARDIR_EQUIV = prove
  49  (`!x y. ((||) x = (||) y) <=> x || y`,
  50   REWRITE_TAC[FUN_EQ_THM] THEN
  51   MESON_TAC[PARDIR_REFL; PARDIR_SYM; PARDIR_TRANS]);;
  52
  53 let DIRECTION_AXIOM_1 = prove
  54  (`!p p'. ~(p || p') ==> ?l. p _|_ l /\ p' _|_ l /\
  55                              !l'. p _|_ l' /\ p' _|_ l' ==> l' || l`,
  56   REWRITE_TAC[perpdir; pardir; DIRECTION_CLAUSES] THEN REPEAT STRIP_TAC THEN
  57   MP_TAC(SPECL [`p:real^3`; `p':real^3`] NORMAL_EXISTS) THEN
  58   MATCH_MP_TAC MONO_EXISTS THEN
  59   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN VEC3_TAC);;
  60
  61 let DIRECTION_AXIOM_2 = prove
  62  (`!l l'. ?p. p _|_ l /\ p _|_ l'`,
  63   REWRITE_TAC[perpdir; DIRECTION_CLAUSES] THEN
  64   MESON_TAC[NORMAL_EXISTS; ORTHOGONAL_SYM]);;
  65
  66 let DIRECTION_AXIOM_3 = prove
  67  (`?p p' p''.
  68         ~(p || p') /\ ~(p' || p'') /\ ~(p || p'') /\
  69         ~(?l. p _|_ l /\ p' _|_ l /\ p'' _|_ l)`,
  70   REWRITE_TAC[perpdir; pardir; DIRECTION_CLAUSES] THEN MAP_EVERY
  71    (fun t -> EXISTS_TAC t THEN SIMP_TAC[BASIS_NONZERO; DIMINDEX_3; ARITH])
  72    [`basis 1 :real^3`; `basis 2 : real^3`; `basis 3 :real^3`] THEN
  73   VEC3_TAC);;
  74
  75 let DIRECTION_AXIOM_4_WEAK = prove
  76  (`!l. ?p p'. ~(p || p') /\ p _|_ l /\ p' _|_ l`,
  77   REWRITE_TAC[DIRECTION_CLAUSES; pardir; perpdir] THEN REPEAT STRIP_TAC THEN
  78   SUBGOAL_THEN
  79    `orthogonal (l cross basis 1) l /\ orthogonal (l cross basis 2) l /\
  80     ~((l cross basis 1) cross (l cross basis 2) = vec 0) \/
  81     orthogonal (l cross basis 1) l /\ orthogonal (l cross basis 3) l /\
  82     ~((l cross basis 1) cross (l cross basis 3) = vec 0) \/
  83     orthogonal (l cross basis 2) l /\ orthogonal (l cross basis 3) l /\
  84     ~((l cross basis 2) cross (l cross basis 3) = vec 0)`
  85   MP_TAC THENL [POP_ASSUM MP_TAC THEN VEC3_TAC; MESON_TAC[CROSS_0]]);;
  86
  87 let ORTHOGONAL_COMBINE = prove
  88  (`!x a b. a _|_ x /\ b _|_ x /\ ~(a || b)
  89            ==> ?c. c _|_ x /\ ~(a || c) /\ ~(b || c)`,
  90   REWRITE_TAC[DIRECTION_CLAUSES; pardir; perpdir] THEN
  91   REPEAT STRIP_TAC THEN EXISTS_TAC `a + b:real^3` THEN
  92   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN VEC3_TAC);;
  93
  94 let DIRECTION_AXIOM_4 = prove
  95  (`!l. ?p p' p''. ~(p || p') /\ ~(p' || p'') /\ ~(p || p'') /\
  96                   p _|_ l /\ p' _|_ l /\ p'' _|_ l`,
  97   MESON_TAC[DIRECTION_AXIOM_4_WEAK; ORTHOGONAL_COMBINE]);;
  98
  99 let line_tybij = define_quotient_type "line" ("mk_line","dest_line") `(||)`;;
 100
 101 let PERPDIR_WELLDEF = prove
 102  (`!x y x' y'. x || x' /\ y || y' ==> (x _|_ y <=> x' _|_ y')`,
 103   REWRITE_TAC[perpdir; pardir; DIRECTION_CLAUSES] THEN VEC3_TAC);;
 104
 105 let perpl,perpl_th =
 106   lift_function (snd line_tybij) (PARDIR_REFL,PARDIR_TRANS)
 107                 "perpl" PERPDIR_WELLDEF;;
 108
 109 let line_lift_thm = lift_theorem line_tybij
 110  (PARDIR_REFL,PARDIR_SYM,PARDIR_TRANS) [perpl_th];;
 111
 112 let LINE_AXIOM_1 = line_lift_thm DIRECTION_AXIOM_1;;
 113 let LINE_AXIOM_2 = line_lift_thm DIRECTION_AXIOM_2;;
 114 let LINE_AXIOM_3 = line_lift_thm DIRECTION_AXIOM_3;;
 115 let LINE_AXIOM_4 = line_lift_thm DIRECTION_AXIOM_4;;
 116
 117 let point_tybij = new_type_definition "point" ("mk_point","dest_point")
 118  (prove(`?x:line. T`,REWRITE_TAC[]));;
 119
 120 parse_as_infix("on",(11,"right"));;
 121
 122 let on = new_definition `p on l <=> perpl (dest_point p) l`;;
 123
 124 let POINT_CLAUSES = prove
 125  (`((p = p') <=> (dest_point p = dest_point p')) /\
 126    ((!p. P (dest_point p)) <=> (!l. P l)) /\
 127    ((?p. P (dest_point p)) <=> (?l. P l))`,
 128   MESON_TAC[point_tybij]);;
 129
 130 let POINT_TAC th = REWRITE_TAC[on; POINT_CLAUSES] THEN ACCEPT_TAC th;;
 131
 132 let AXIOM_1 = prove
 133  (`!p p'. ~(p = p') ==> ?l. p on l /\ p' on l /\
 134           !l'. p on l' /\ p' on l' ==> (l' = l)`,
 135   POINT_TAC LINE_AXIOM_1);;
 136
 137 let AXIOM_2 = prove
 138  (`!l l'. ?p. p on l /\ p on l'`,
 139   POINT_TAC LINE_AXIOM_2);;
 140
 141 let AXIOM_3 = prove
 142  (`?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
 143     ~(?l. p on l /\ p' on l /\ p'' on l)`,
 144   POINT_TAC LINE_AXIOM_3);;
 145
 146 let AXIOM_4 = prove
 147  (`!l. ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
 148     p on l /\ p' on l /\ p'' on l`,
 149   POINT_TAC LINE_AXIOM_4);;
 150
 151 (* ------------------------------------------------------------------------- *)
 152 (* Mappings from vectors in R^3 to projective lines and points.              *)
 153 (* ------------------------------------------------------------------------- *)
 154
 155 let projl = new_definition
 156  `projl x = mk_line((||) (mk_dir x))`;;
 157
 158 let projp = new_definition
 159  `projp x = mk_point(projl x)`;;
 160
 161 (* ------------------------------------------------------------------------- *)
 162 (* Mappings in the other direction, to (some) homogeneous coordinates.       *)
 163 (* ------------------------------------------------------------------------- *)
 164
 165 let PROJL_TOTAL = prove
 166  (`!l. ?x. ~(x = vec 0) /\ l = projl x`,
 167   GEN_TAC THEN
 168   SUBGOAL_THEN `?d. l = mk_line((||) d)` (CHOOSE_THEN SUBST1_TAC) THENL
 169    [MESON_TAC[fst line_tybij; snd line_tybij];
 170     REWRITE_TAC[projl] THEN EXISTS_TAC `dest_dir d` THEN
 171     MESON_TAC[direction_tybij]]);;
 172
 173 let homol = new_specification ["homol"]
 174   (REWRITE_RULE[SKOLEM_THM] PROJL_TOTAL);;
 175
 176 let PROJP_TOTAL = prove
 177  (`!p. ?x. ~(x = vec 0) /\ p = projp x`,
 178   REWRITE_TAC[projp] THEN MESON_TAC[PROJL_TOTAL; point_tybij]);;
 179
 180 let homop_def = new_definition
 181  `homop p = homol(dest_point p)`;;
 182
 183 let homop = prove
 184  (`!p. ~(homop p = vec 0) /\ p = projp(homop p)`,
 185   GEN_TAC THEN REWRITE_TAC[homop_def; projp; MESON[point_tybij]
 186    `p = mk_point l <=> dest_point p = l`] THEN
 187   MATCH_ACCEPT_TAC homol);;
 188
 189 (* ------------------------------------------------------------------------- *)
 190 (* Key equivalences of concepts in projective space and homogeneous coords.  *)
 191 (* ------------------------------------------------------------------------- *)
 192
 193 let parallel = new_definition
 194  `parallel x y <=> x cross y = vec 0`;;
 195
 196 let ON_HOMOL = prove
 197  (`!p l. p on l <=> orthogonal (homop p) (homol l)`,
 198   REPEAT GEN_TAC THEN
 199   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [homop; homol] THEN
 200   REWRITE_TAC[on; projp; projl; REWRITE_RULE[] point_tybij] THEN
 201   REWRITE_TAC[GSYM perpl_th; perpdir] THEN BINOP_TAC THEN
 202   MESON_TAC[homol; homop; direction_tybij]);;
 203
 204 let EQ_HOMOL = prove
 205  (`!l l'. l = l' <=> parallel (homol l) (homol l')`,
 206   REPEAT GEN_TAC THEN
 207   GEN_REWRITE_TAC (LAND_CONV o BINOP_CONV) [homol] THEN
 208   REWRITE_TAC[projl; MESON[fst line_tybij; snd line_tybij]
 209    `mk_line((||) l) = mk_line((||) l') <=> (||) l = (||) l'`] THEN
 210   REWRITE_TAC[PARDIR_EQUIV] THEN REWRITE_TAC[pardir; parallel] THEN
 211   MESON_TAC[homol; direction_tybij]);;
 212
 213 let EQ_HOMOP = prove
 214  (`!p p'. p = p' <=> parallel (homop p) (homop p')`,
 215   REWRITE_TAC[homop_def; GSYM EQ_HOMOL] THEN
 216   MESON_TAC[point_tybij]);;
 217
 218 (* ------------------------------------------------------------------------- *)
 219 (* A "welldefinedness" result for homogeneous coordinate map.                *)
 220 (* ------------------------------------------------------------------------- *)
 221
 222 let PARALLEL_PROJL_HOMOL = prove
 223  (`!x. parallel x (homol(projl x))`,
 224   GEN_TAC THEN REWRITE_TAC[parallel] THEN ASM_CASES_TAC `x:real^3 = vec 0` THEN
 225   ASM_REWRITE_TAC[CROSS_0] THEN MP_TAC(ISPEC `projl x` homol) THEN
 226   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 227   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [projl] THEN
 228   DISCH_THEN(MP_TAC o AP_TERM `dest_line`) THEN
 229   REWRITE_TAC[MESON[fst line_tybij; snd line_tybij]
 230    `dest_line(mk_line((||) l)) = (||) l`] THEN
 231   REWRITE_TAC[PARDIR_EQUIV] THEN REWRITE_TAC[pardir] THEN
 232   ASM_MESON_TAC[direction_tybij]);;
 233
 234 let PARALLEL_PROJP_HOMOP = prove
 235  (`!x. parallel x (homop(projp x))`,
 236   REWRITE_TAC[homop_def; projp; REWRITE_RULE[] point_tybij] THEN
 237   REWRITE_TAC[PARALLEL_PROJL_HOMOL]);;
 238
 239 let PARALLEL_PROJP_HOMOP_EXPLICIT = prove
 240  (`!x. ~(x = vec 0) ==> ?a. ~(a = &0) /\ homop(projp x) = a % x`,
 241   MP_TAC PARALLEL_PROJP_HOMOP THEN MATCH_MP_TAC MONO_FORALL THEN
 242   REWRITE_TAC[parallel; CROSS_EQ_0; COLLINEAR_LEMMA] THEN
 243   GEN_TAC THEN ASM_CASES_TAC `x:real^3 = vec 0` THEN
 244   ASM_REWRITE_TAC[homop] THEN MATCH_MP_TAC MONO_EXISTS THEN
 245   X_GEN_TAC `c:real` THEN ASM_CASES_TAC `c = &0` THEN
 246   ASM_REWRITE_TAC[homop; VECTOR_MUL_LZERO]);;
 247
 248 (* ------------------------------------------------------------------------- *)
 249 (* Brackets, collinearity and their connection.                              *)
 250 (* ------------------------------------------------------------------------- *)
 251
 252 let bracket = define
 253  `bracket[a;b;c] = det(vector[homop a;homop b;homop c])`;;
 254
 255 let COLLINEAR = new_definition
 256  `COLLINEAR s <=> ?l. !p. p IN s ==> p on l`;;
 257
 258 let COLLINEAR_SINGLETON = prove
 259  (`!a. COLLINEAR {a}`,
 260   REWRITE_TAC[COLLINEAR; FORALL_IN_INSERT; NOT_IN_EMPTY] THEN
 261   MESON_TAC[AXIOM_1; AXIOM_3]);;
 262
 263 let COLLINEAR_PAIR = prove
 264  (`!a b. COLLINEAR{a,b}`,
 265   REPEAT GEN_TAC THEN ASM_CASES_TAC `a:point = b` THEN
 266   ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_SINGLETON] THEN
 267   REWRITE_TAC[COLLINEAR; FORALL_IN_INSERT; NOT_IN_EMPTY] THEN
 268   ASM_MESON_TAC[AXIOM_1]);;
 269
 270 let COLLINEAR_TRIPLE = prove
 271  (`!a b c. COLLINEAR{a,b,c} <=> ?l. a on l /\ b on l /\ c on l`,
 272   REWRITE_TAC[COLLINEAR; FORALL_IN_INSERT; NOT_IN_EMPTY]);;
 273
 274 let COLLINEAR_BRACKET = prove
 275  (`!p1 p2 p3. COLLINEAR {p1,p2,p3} <=> bracket[p1;p2;p3] = &0`,
 276   let lemma = prove
 277    (`!a b c x y.
 278           x cross y = vec 0 /\ ~(x = vec 0) /\
 279           orthogonal a x /\ orthogonal b x /\ orthogonal c x
 280           ==> orthogonal a y /\ orthogonal b y /\ orthogonal c y`,
 281     REWRITE_TAC[orthogonal] THEN VEC3_TAC) in
 282   REPEAT GEN_TAC THEN EQ_TAC THENL
 283    [REWRITE_TAC[COLLINEAR_TRIPLE; bracket; ON_HOMOL; LEFT_IMP_EXISTS_THM] THEN
 284     MP_TAC homol THEN MATCH_MP_TAC MONO_FORALL THEN
 285     GEN_TAC THEN DISCH_THEN(MP_TAC o CONJUNCT1) THEN
 286     REWRITE_TAC[DET_3; orthogonal; DOT_3; VECTOR_3; CART_EQ;
 287               DIMINDEX_3; FORALL_3; VEC_COMPONENT] THEN
 288     CONV_TAC REAL_RING;
 289     ASM_CASES_TAC `p1:point = p2` THENL
 290      [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_PAIR]; ALL_TAC] THEN
 291     POP_ASSUM MP_TAC THEN
 292     REWRITE_TAC[parallel; COLLINEAR_TRIPLE; bracket; EQ_HOMOP; ON_HOMOL] THEN
 293     REPEAT STRIP_TAC THEN
 294     EXISTS_TAC `mk_line((||) (mk_dir(homop p1 cross homop p2)))` THEN
 295     MATCH_MP_TAC lemma THEN EXISTS_TAC `homop p1 cross homop p2` THEN
 296     ASM_REWRITE_TAC[ORTHOGONAL_CROSS] THEN
 297     REWRITE_TAC[orthogonal] THEN ONCE_REWRITE_TAC[DOT_SYM] THEN
 298     ONCE_REWRITE_TAC[CROSS_TRIPLE] THEN ONCE_REWRITE_TAC[DOT_SYM] THEN
 299     ASM_REWRITE_TAC[DOT_CROSS_DET] THEN
 300     REWRITE_TAC[GSYM projl; GSYM parallel; PARALLEL_PROJL_HOMOL]]);;
 301
 302 (* ------------------------------------------------------------------------- *)
 303 (* Rather crude shuffling of bracket triple into canonical order.            *)
 304 (* ------------------------------------------------------------------------- *)
 305
 306 let BRACKET_SWAP,BRACKET_SHUFFLE = (CONJ_PAIR o prove)
 307  (`bracket[x;y;z] = --bracket[x;z;y] /\
 308    bracket[x;y;z] = bracket[y;z;x] /\
 309    bracket[x;y;z] = bracket[z;x;y]`,
 310   REWRITE_TAC[bracket; DET_3; VECTOR_3] THEN CONV_TAC REAL_RING);;
 311
 312 let BRACKET_SWAP_CONV =
 313   let conv = GEN_REWRITE_CONV I [BRACKET_SWAP] in
 314   fun tm -> let th = conv tm in
 315             let tm' = rand(rand(concl th)) in
 316             if term_order tm tm' then th else failwith "BRACKET_SWAP_CONV";;
 317
 318 (* ------------------------------------------------------------------------- *)
 319 (* Direct proof following Richter-Gebert's "Meditations on Ceva's Theorem",  *)
 320 (* except for a change of variable names. The degenerate conditions here are *)
 321 (* just those that naturally get used in the proof.                          *)
 322 (* ------------------------------------------------------------------------- *)
 323
 324 let DESARGUES_DIRECT = prove
 325  (`~COLLINEAR {A',B,S} /\
 326    ~COLLINEAR {A,P,C} /\
 327    ~COLLINEAR {A,P,R} /\
 328    ~COLLINEAR {A,C,B} /\
 329    ~COLLINEAR {A,B,R} /\
 330    ~COLLINEAR {C',P,A'} /\
 331    ~COLLINEAR {C',P,B} /\
 332    ~COLLINEAR {C',P,B'} /\
 333    ~COLLINEAR {C',A',S} /\
 334    ~COLLINEAR {C',A',B'} /\
 335    ~COLLINEAR {P,C,A'} /\
 336    ~COLLINEAR {P,C,B} /\
 337    ~COLLINEAR {P,A',R} /\
 338    ~COLLINEAR {P,B,Q} /\
 339    ~COLLINEAR {P,Q,B'} /\
 340    ~COLLINEAR {C,B,S} /\
 341    ~COLLINEAR {A',Q,B'}
 342    ==> COLLINEAR {P,A',A} /\
 343        COLLINEAR {P,B,B'} /\
 344        COLLINEAR {P,C',C} /\
 345        COLLINEAR {B,C,Q} /\
 346        COLLINEAR {B',C',Q} /\
 347        COLLINEAR {A,R,C} /\
 348        COLLINEAR {A',C',R} /\
 349        COLLINEAR {B,S,A} /\
 350        COLLINEAR {A',S,B'}
 351        ==> COLLINEAR {Q,S,R}`,
 352   REPEAT GEN_TAC THEN REWRITE_TAC[COLLINEAR_BRACKET] THEN DISCH_TAC THEN
 353   SUBGOAL_THEN
 354    `(bracket[P;A';A] = &0
 355      ==> bracket[P;A';R] * bracket[P;A;C] =
 356          bracket[P;A';C] * bracket[P;A;R]) /\
 357     (bracket[P;B;B'] = &0
 358      ==> bracket[P;B;Q] * bracket[P;B';C'] =
 359          bracket[P;B;C'] * bracket[P;B';Q]) /\
 360     (bracket[P;C';C] = &0
 361      ==> bracket[P;C';B] * bracket[P;C;A'] =
 362          bracket[P;C';A'] * bracket[P;C;B]) /\
 363     (bracket[B;C;Q] = &0
 364      ==> bracket[B;C;P] * bracket[B;Q;S] =
 365          bracket[B;C;S] * bracket[B;Q;P]) /\
 366     (bracket[B';C';Q] = &0
 367      ==> bracket[B';C';A'] * bracket[B';Q;P] =
 368          bracket[B';C';P] * bracket[B';Q;A']) /\
 369     (bracket[A;R;C] = &0
 370      ==> bracket[A;R;P] * bracket[A;C;B] =
 371          bracket[A;R;B] * bracket[A;C;P]) /\
 372     (bracket[A';C';R] = &0
 373      ==> bracket[A';C';P] * bracket[A';R;S] =
 374          bracket[A';C';S] * bracket[A';R;P]) /\
 375     (bracket[B;S;A] = &0
 376      ==> bracket[B;S;C] * bracket[B;A;R] =
 377          bracket[B;S;R] * bracket[B;A;C]) /\
 378     (bracket[A';S;B'] = &0
 379      ==> bracket[A';S;C'] * bracket[A';B';Q] =
 380          bracket[A';S;Q] * bracket[A';B';C'])`
 381   MP_TAC THENL
 382    [REWRITE_TAC[bracket; DET_3; VECTOR_3] THEN CONV_TAC REAL_RING;
 383     ALL_TAC] THEN
 384   REPEAT(MATCH_MP_TAC(TAUT
 385    `(c ==> d ==> b ==> e) ==> ((a ==> b) /\ c ==> a /\ d ==> e)`)) THEN
 386   DISCH_THEN(fun th -> DISCH_THEN(MP_TAC o MATCH_MP th)) THEN
 387   REPEAT(ONCE_REWRITE_TAC[IMP_IMP] THEN
 388          DISCH_THEN(MP_TAC o MATCH_MP (REAL_RING
 389           `a = b /\ x:real = y ==> a * x = b * y`))) THEN
 390   POP_ASSUM MP_TAC THEN REWRITE_TAC[BRACKET_SHUFFLE] THEN
 391   CONV_TAC(ONCE_DEPTH_CONV BRACKET_SWAP_CONV) THEN
 392   REWRITE_TAC[GSYM REAL_MUL_ASSOC; REAL_MUL_LNEG; REAL_MUL_RNEG] THEN
 393   REWRITE_TAC[REAL_NEG_NEG; REAL_NEG_EQ_0] THEN DISCH_TAC THEN
 394   MATCH_MP_TAC(TAUT `!b. (a ==> b) /\ (b ==> c) ==> a ==> c`) THEN
 395   EXISTS_TAC `bracket[B;Q;S] * bracket[A';R;S] =
 396               bracket[B;R;S] * bracket[A';Q;S]` THEN
 397   CONJ_TAC THENL [POP_ASSUM MP_TAC THEN CONV_TAC REAL_RING; ALL_TAC] THEN
 398   FIRST_X_ASSUM(MP_TAC o CONJUNCT1) THEN
 399   REWRITE_TAC[bracket; DET_3; VECTOR_3] THEN CONV_TAC REAL_RING);;