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

   1 (* ========================================================================= *)
   2 (* Examples of using the "without loss of generality" tactics.               *)
   3 (* ========================================================================= *)
   4
   5 needs "Multivariate/wlog.ml";;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Example 1.                                                                *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let lemma = prove
  12  (`(?y. y pow 2 = a) <=> &0 <= a`,
  13   MESON_TAC[SQRT_POW_2; REAL_LE_SQUARE; REAL_POW_2]);;
  14
  15 let TRUONG_1 = prove
  16  (`!u1:real^3 u2 p a b.
  17      ~(u1 = u2) /\
  18      plane p /\
  19      {u1,u2} SUBSET p /\
  20      dist(u1,u2) <= a + b /\
  21      abs(a - b) < dist(u1,u2) /\
  22      &0 <= a /\
  23      &0 <= b
  24      ==> (?d1 d2.
  25               {d1, d2} SUBSET p /\
  26               &1 / &2 % (d1 + d2) IN affine hull {u1, u2} /\
  27               dist(d1,u1) = a /\
  28               dist(d1,u2) = b /\
  29               dist(d2,u1) = a /\
  30               dist(d2,u2) = b)`,
  31   (*** First, rotate the plane p to the special case z$3 = &0 ***)
  32
  33   GEOM_HORIZONTAL_PLANE_TAC `p:real^3->bool` THEN
  34
  35   (*** Now reshuffle the goal to have explicit restricted quantifiers ***)
  36
  37   ONCE_REWRITE_TAC[TAUT
  38    `a /\ b /\ c /\ d ==> e <=> c /\ a /\ b /\ d ==> e`] THEN
  39   REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN
  40   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
  41   REWRITE_TAC[GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM] THEN
  42   REWRITE_TAC[IN_ELIM_THM] THEN
  43
  44   (*** Now replace quantifiers over real^3 with those over real^2 ***)
  45
  46   PAD2D3D_TAC THEN
  47
  48   (*** Tidy the goal a little ***)
  49
  50   REWRITE_TAC[RIGHT_IMP_FORALL_THM; IMP_IMP; GSYM CONJ_ASSOC] THEN
  51
  52   (*** Choose u1 as the origin ***)
  53
  54   GEOM_ORIGIN_TAC `u1:real^2` THEN
  55
  56   (*** Rotate the point u2 onto the x-axis ***)
  57
  58   GEOM_HORIZONTAL_LINE_TAC `u2:real^2` THEN
  59
  60   (*** Only now introduce coordinates ***)
  61
  62   X_GEN_TAC `u2:real^2` THEN DISCH_TAC THEN
  63   MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN
  64   REWRITE_TAC[dist; VECTOR_SUB_RZERO; VECTOR_SUB_LZERO; NORM_NEG] THEN
  65   SIMP_TAC[GSYM real_gt; NORM_GT_SQUARE; NORM_EQ_SQUARE; NORM_LE_SQUARE] THEN
  66   REWRITE_TAC[real_gt; REAL_ARITH `~(abs x < &0)`] THEN
  67   ASM_SIMP_TAC[DOT_2; REAL_MUL_RZERO; REAL_ADD_RID; CART_EQ; DIMINDEX_2;
  68                FORALL_2; AFFINE_HULL_2; CART_EQ; VECTOR_MUL_COMPONENT;
  69                VECTOR_SUB_COMPONENT; VEC_COMPONENT; ARITH; IN_ELIM_THM;
  70                VECTOR_ADD_COMPONENT; REAL_SUB_RZERO; REAL_ADD_LID;
  71                REAL_POW2_ABS] THEN
  72   DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o GSYM) STRIP_ASSUME_TAC) THEN
  73   REWRITE_TAC[EXISTS_VECTOR_2] THEN
  74   MATCH_MP_TAC(MESON[]
  75    `(?x y:real. P x y x (--y)) ==> (?x y x' y'. P x y x' y')`) THEN
  76   SIMP_TAC[AFFINE_HULL_2; IN_ELIM_THM; CART_EQ; DIMINDEX_2; FORALL_2; VECTOR_2;
  77         VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; VEC_COMPONENT; ARITH] THEN
  78   ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_LID; REAL_ADD_RINV] THEN
  79   ASM_SIMP_TAC[REAL_FIELD
  80    `~(a = &0)
  81     ==> (u + v = &1 /\ b = v * a <=> u = &1 - b / a /\ v = b / a)`] THEN
  82   REWRITE_TAC[RIGHT_EXISTS_AND_THM; LEFT_EXISTS_AND_THM; EXISTS_REFL] THEN
  83   ABBREV_TAC `u = (u2:real^2)$1` THEN
  84   REWRITE_TAC[REAL_ARITH `x + --y * --y:real = x + y * y`] THEN
  85   REWRITE_TAC[TAUT `a /\ b /\ a /\ b <=> a /\ b`] THEN
  86
  87   (*** Now finally dive in and solve the algebraic problem ***)
  88
  89   ASM_SIMP_TAC[REAL_FIELD
  90    `~(u = &0)
  91     ==> (x * x + y * y = a pow 2 /\ (x - u) * (x - u) + y * y = b pow 2 <=>
  92          x = (u pow 2 + a pow 2 - b pow 2) / (&2 * u) /\
  93          y pow 2 = b pow 2 - (x - u) pow 2)`] THEN
  94   REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM2; lemma] THEN
  95   ASM_SIMP_TAC[REAL_SUB_LE; REAL_FIELD
  96    `(u pow 2 + a - b) / (&2 * u) - u = (a - b - u pow 2) / (&2 * u)`] THEN
  97   REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN
  98   ASM_SIMP_TAC[REAL_ABS_DIV; REAL_LE_LDIV_EQ;
  99                REAL_ARITH `~(u = &0) ==> &0 < abs(&2 * u)`] THEN
 100   REWRITE_TAC[GSYM REAL_ABS_MUL; REAL_LE_SQUARE_ABS] THEN
 101
 102   (*** Can just use SOS: this proof was found by SOS_RULE ***)
 103
 104   MAP_EVERY UNDISCH_TAC
 105    [`u * u <= (a + b) pow 2`; `(a - b) pow 2 < u * u`] THEN
 106   DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_IMP_LE) THEN
 107   ONCE_REWRITE_TAC[GSYM REAL_SUB_LE] THEN
 108   REWRITE_TAC[IMP_IMP] THEN DISCH_THEN(MP_TAC o MATCH_MP REAL_LE_MUL) THEN
 109   REAL_ARITH_TAC);;
 110
 111 (* ------------------------------------------------------------------------- *)
 112 (* Definition of "opposite" for example 2, and its invariance theorems.      *)
 113 (* ------------------------------------------------------------------------- *)
 114
 115 let opposite = new_definition
 116   `opposite a b p <=>
 117         (&1 / &2 % (a + b)) IN p /\
 118         (!x y:real^N. {x,y} SUBSET p ==> (x - y) dot (a - b) = &0)`;;
 119
 120 let OPPOSITE_TRANSLATION_EQ = prove
 121  (`!c a b p. opposite (c + a) (c + b) (IMAGE (\x. c + x) p) <=>
 122              opposite a b p`,
 123   REWRITE_TAC[opposite] THEN GEOM_TRANSLATE_TAC[]);;
 124
 125 add_translation_invariants [OPPOSITE_TRANSLATION_EQ];;
 126
 127 let OPPOSITE_LINEAR_IMAGE_EQ = prove
 128  (`!f a b p. linear f /\ (!x. norm(f x) = norm x)
 129              ==> (opposite (f a) (f b) (IMAGE f p) <=> opposite a b p)`,
 130   SIMP_TAC[opposite; INSERT_SUBSET; EMPTY_SUBSET; GSYM orthogonal] THEN
 131   REWRITE_TAC[IMP_CONJ; FORALL_IN_IMAGE; RIGHT_FORALL_IMP_THM] THEN
 132   SIMP_TAC[GSYM LINEAR_ADD; GSYM LINEAR_SUB; ORTHOGONAL_LINEAR_IMAGE_EQ] THEN
 133   SIMP_TAC[GSYM LINEAR_CMUL; IN_IMAGE] THEN
 134   MESON_TAC[PRESERVES_NORM_INJECTIVE]);;
 135
 136 add_linear_invariants [OPPOSITE_LINEAR_IMAGE_EQ];;
 137
 138 (* ------------------------------------------------------------------------- *)
 139 (* Example 2.                                                                *)
 140 (* ------------------------------------------------------------------------- *)
 141
 142 let AFFINE_PLANE = prove
 143  (`!p. plane p ==> affine p`,
 144   SIMP_TAC[plane; LEFT_IMP_EXISTS_THM; AFFINE_AFFINE_HULL]);;
 145
 146 let lemma = prove
 147  (`!a b:real^2.
 148         a$2 <= &0 /\ &0 <= b$2 ==> ?x. x IN convex hull {a,b} /\ x$2 = &0`,
 149   REPEAT GEN_TAC THEN DISCH_TAC THEN
 150   FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (REAL_ARITH
 151    `a <= &0 /\ &0 <= b ==> a = &0 /\ b = &0 \/ &0 < b - a`))
 152   THENL
 153    [EXISTS_TAC `a:real^2` THEN ASM_SIMP_TAC[HULL_INC; IN_INSERT];
 154     REWRITE_TAC[CONVEX_HULL_2_ALT; EXISTS_IN_GSPEC] THEN
 155     SIMP_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; VECTOR_SUB_COMPONENT;
 156              DIMINDEX_2; ARITH] THEN
 157     EXISTS_TAC `--(a$2) / ((b:real^2)$2 - (a:real^2)$2)` THEN
 158     ASM_SIMP_TAC[REAL_LT_IMP_NZ; REAL_DIV_RMUL;
 159                  REAL_LE_LDIV_EQ; REAL_LE_RDIV_EQ] THEN
 160     ASM_REAL_ARITH_TAC]);;
 161
 162 let TRUONG_OPPOSITE_LEMMA = prove
 163  (`!p a b bb m x y:real^3.
 164      plane p /\
 165      {a, b, bb, m, x, y} SUBSET p /\
 166      ~(x = y) /\ m IN affine hull {x,y} /\ midpoint(b,bb) = m
 167      ==> ~(convex hull {a, b} INTER affine hull {x, y} = {}) \/
 168          ~(convex hull {a, bb} INTER affine hull {x, y} = {})`,
 169
 170   (*** Make the plane p the xy-plane ***)
 171
 172   GEOM_HORIZONTAL_PLANE_TAC `p:real^3->bool` THEN
 173
 174   (*** Rewrite with explicit restricted quantifiers ***)
 175
 176   REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 177   REWRITE_TAC[IN_ELIM_THM] THEN DISCH_THEN(K ALL_TAC) THEN
 178
 179   (*** Now replace quantifiers over real^3 with those over real^2 ***)
 180
 181   PAD2D3D_TAC THEN
 182
 183   (*** Let x be the origin, and y on the x-axis ***)
 184
 185   GEOM_ORIGIN_TAC `x:real^2` THEN
 186   GEOM_HORIZONTAL_LINE_TAC `y:real^2` THEN
 187
 188   (*** Make a few simplifications ***)
 189
 190   GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
 191   ASM_SIMP_TAC[CART_EQ; DIMINDEX_2; FORALL_2; VEC_COMPONENT] THEN
 192   DISCH_THEN(ASSUME_TAC o GSYM) THEN
 193   SIMP_TAC[midpoint; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT;
 194            DIMINDEX_2; ARITH] THEN
 195
 196   (*** Show aff{x,y} is now exactly the x-axis ***)
 197
 198   SUBGOAL_THEN `affine hull {vec 0,y} = {u:real^2 | u$2 = &0}` SUBST1_TAC THENL
 199    [MATCH_MP_TAC HULL_UNIQUE THEN
 200     REWRITE_TAC[affine; INSERT_SUBSET; EMPTY_SUBSET; IN_ELIM_THM] THEN
 201     ASM_SIMP_TAC[VEC_COMPONENT; DIMINDEX_2; ARITH; VECTOR_ADD_COMPONENT;
 202                  VECTOR_MUL_COMPONENT; REAL_MUL_RZERO; REAL_ADD_RID] THEN
 203     X_GEN_TAC `s:real^2->bool` THEN STRIP_TAC THEN
 204     REWRITE_TAC[SUBSET; FORALL_IN_GSPEC] THEN X_GEN_TAC `u:real^2` THEN
 205     DISCH_TAC THEN
 206     SUBGOAL_THEN `u = (&1 - u$1 / (y:real^2)$1) % vec 0 +
 207                   (u$1 / (y:real^2)$1) % y`
 208     SUBST1_TAC THENL
 209      [REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
 210       ASM_SIMP_TAC[CART_EQ; VECTOR_MUL_COMPONENT; DIMINDEX_2; ARITH;
 211                    FORALL_2; REAL_MUL_RZERO; REAL_DIV_RMUL];
 212       FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
 213       REAL_ARITH_TAC];
 214     ALL_TAC] THEN
 215
 216   (*** Simplify a bit more ***)
 217
 218   SIMP_TAC[IN_ELIM_THM; REAL_ARITH `inv(&2) * (x + y) = &0 <=> y = --x`] THEN
 219   REPEAT STRIP_TAC THEN
 220
 221   (*** Finally, make a 4-way case split then apply the lemma to each ***)
 222
 223   REWRITE_TAC[SET_RULE `~(s INTER t = {}) <=> ?x. x IN s /\ x IN t`] THEN
 224   REWRITE_TAC[IN_ELIM_THM] THEN
 225   FIRST_ASSUM(MP_TAC o SPEC `(a:real^2)$2` o MATCH_MP (REAL_ARITH
 226    `b' = --b ==> !a. a <= &0 /\ &0 <= b \/ a <= &0 /\ &0 <= b' \/
 227                      b <= &0 /\ &0 <= a \/ b' <= &0 /\ &0 <= a`)) THEN
 228   MESON_TAC[lemma; SET_RULE `{a,b} = {b,a}`]);;
 229
 230 let TRUONG_OPPOSITE_THM = prove
 231  (`!a b bb x y:real^3 p.
 232      ~(x = y) /\
 233      plane p /\
 234      {a, b, x, y} SUBSET p /\
 235      opposite b bb (affine hull {x, y})
 236      ==> ~(convex hull {a, b} INTER affine hull {x, y} = {}) \/
 237          ~(convex hull {a, bb} INTER affine hull {x, y} = {})`,
 238   REWRITE_TAC[opposite; INSERT_SUBSET; EMPTY_SUBSET] THEN REPEAT STRIP_TAC THEN
 239   MATCH_MP_TAC TRUONG_OPPOSITE_LEMMA THEN
 240   MAP_EVERY EXISTS_TAC [`p:real^3->bool`; `&1 / &2 % (b + bb):real^3`] THEN
 241   ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; midpoint] THEN
 242   CONJ_TAC THENL [ALL_TAC; VECTOR_ARITH_TAC]  THEN
 243   FIRST_ASSUM(ASSUME_TAC o MATCH_MP AFFINE_PLANE) THEN
 244   MATCH_MP_TAC(TAUT `b /\ (b ==> a) ==> a /\ b`) THEN CONJ_TAC THENL
 245    [MATCH_MP_TAC(SET_RULE `!t. x IN t /\ t SUBSET s ==> x IN s`) THEN
 246     EXISTS_TAC `affine hull {x:real^3,y}` THEN ASM_REWRITE_TAC[] THEN
 247     MATCH_MP_TAC HULL_MINIMAL THEN ASM_SIMP_TAC[INSERT_SUBSET; EMPTY_SUBSET];
 248     DISCH_TAC THEN SUBST1_TAC(VECTOR_ARITH
 249       `bb:real^3 = -- &1 % b + &2 % &1 / &2 % (b + bb)`) THEN
 250     FIRST_X_ASSUM(MATCH_MP_TAC o REWRITE_RULE[affine]) THEN
 251     ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]);;
 252
 253 (* ------------------------------------------------------------------------- *)
 254 (* Affsign variants for example 3, and invariance theorems.                  *)
 255 (* ------------------------------------------------------------------------- *)
 256
 257 let lin_combo = new_definition
 258   `lin_combo V f = vsum V (\v. f v % (v:real^N))`;;
 259
 260 let affsign = new_definition
 261   `affsign sgn s t (v:real^A) <=>
 262      (?f. (v = lin_combo (s UNION t) f) /\
 263           (!w. t w ==> sgn (f w)) /\
 264           (sum (s UNION t) f = &1))`;;
 265
 266 let sgn_gt = new_definition `sgn_gt = (\t. (&0 < t))`;;
 267 let sgn_ge = new_definition `sgn_ge = (\t. (&0 <= t))`;;
 268 let sgn_lt = new_definition `sgn_lt = (\t. (t < &0))`;;
 269 let sgn_le = new_definition `sgn_le = (\t. (t <= &0))`;;
 270
 271 let aff_gt_def = new_definition `aff_gt = affsign sgn_gt`;;
 272 let aff_ge_def = new_definition `aff_ge = affsign sgn_ge`;;
 273 let aff_lt_def = new_definition `aff_lt = affsign sgn_lt`;;
 274 let aff_le_def = new_definition `aff_le = affsign sgn_le`;;
 275
 276 let AFFSIGN = prove
 277  (`affsign sgn s t =
 278         {y | ?f. y = vsum (s UNION t) (\v. f v % v) /\
 279                 (!w. w IN t ==> sgn(f w)) /\
 280                 sum (s UNION t) f = &1}`,
 281   REWRITE_TAC[FUN_EQ_THM; affsign; lin_combo; IN_ELIM_THM] THEN
 282   REWRITE_TAC[IN]);;
 283
 284 let AFFSIGN_ALT = prove
 285  (`affsign sgn s t =
 286         {y | ?f. (!w. w IN (s UNION t) ==> w IN t ==> sgn(f w)) /\
 287                  sum (s UNION t) f = &1 /\
 288                  vsum (s UNION t) (\v. f v % v) = y}`,
 289   REWRITE_TAC[SET_RULE `(w IN (s UNION t) ==> w IN t ==> P w) <=>
 290                         (w IN t ==> P w)`] THEN
 291   REWRITE_TAC[AFFSIGN; EXTENSION; IN_ELIM_THM] THEN MESON_TAC[]);;
 292
 293 let IN_AFFSIGN = prove
 294  (`y IN affsign sgn s t <=>
 295         ?u. (!x. x IN t ==> sgn(u x)) /\
 296             sum (s UNION t) u = &1 /\
 297             vsum (s UNION t) (\x. u(x) % x) = y`,
 298   REWRITE_TAC[AFFSIGN; IN_ELIM_THM] THEN SET_TAC[]);;
 299
 300 let AFFSIGN_INJECTIVE_LINEAR_IMAGE = prove
 301  (`!f:real^M->real^N sgn s t v.
 302         linear f /\ (!x y. f x = f y ==> x = y)
 303         ==> (affsign sgn (IMAGE f s) (IMAGE f t) =
 304              IMAGE f (affsign sgn s t))`,
 305   let lemma0 = prove
 306    (`vsum s (\x. u x % x) = vsum {x | x IN s /\ ~(u x = &0)} (\x. u x % x)`,
 307     MATCH_MP_TAC VSUM_SUPERSET THEN SIMP_TAC[SUBSET; IN_ELIM_THM] THEN
 308     REWRITE_TAC[TAUT `p /\ ~(p /\ ~q) <=> p /\ q`] THEN
 309     SIMP_TAC[o_THM; VECTOR_MUL_LZERO]) in
 310   let lemma1 = prove
 311    (`!f:real^M->real^N s.
 312            linear f /\ (!x y. f x = f y ==> x = y)
 313            ==> (sum(IMAGE f s) u = &1 /\ vsum(IMAGE f s) (\x. u x % x) = y <=>
 314                 sum s (u o f) = &1 /\ f(vsum s (\x. (u o f) x % x)) = y)`,
 315     REPEAT STRIP_TAC THEN
 316     W(MP_TAC o PART_MATCH (lhs o rand) SUM_IMAGE o funpow 3 lhand o snd) THEN
 317     ANTS_TAC THENL [ASM_MESON_TAC[]; DISCH_THEN SUBST1_TAC] THEN
 318     MATCH_MP_TAC(MESON[] `(p ==> z = x) ==> (p /\ x = y <=> p /\ z = y)`) THEN
 319     DISCH_TAC THEN ONCE_REWRITE_TAC[lemma0] THEN
 320     SUBGOAL_THEN
 321      `{y | y IN IMAGE (f:real^M->real^N) s /\ ~(u y = &0)} =
 322       IMAGE f {x | x IN s /\ ~(u(f x) = &0)}`
 323     SUBST1_TAC THENL [ASM SET_TAC[]; CONV_TAC SYM_CONV] THEN
 324     SUBGOAL_THEN `FINITE {x | x IN s /\ ~(u((f:real^M->real^N) x) = &0)}`
 325     ASSUME_TAC THENL
 326      [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE
 327        (LAND_CONV o RATOR_CONV o RATOR_CONV) [sum]) THEN
 328       ONCE_REWRITE_TAC[ITERATE_EXPAND_CASES] THEN
 329       REWRITE_TAC[GSYM sum; support; NEUTRAL_REAL_ADD; o_THM] THEN
 330       COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_OF_NUM_EQ; ARITH_EQ];
 331       W(MP_TAC o PART_MATCH (lhs o rand) VSUM_IMAGE o lhand o snd) THEN
 332       ANTS_TAC THENL [ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]; ALL_TAC] THEN
 333       DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[o_DEF] THEN
 334       ASM_SIMP_TAC[LINEAR_VSUM; o_DEF; GSYM LINEAR_CMUL]]) in
 335   REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[EXTENSION; IN_AFFSIGN] THEN
 336   REWRITE_TAC[FORALL_IN_IMAGE] THEN REWRITE_TAC[IN_IMAGE; IN_AFFSIGN] THEN
 337   REWRITE_TAC[GSYM IMAGE_UNION] THEN
 338   FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP lemma1 th]) THEN
 339   X_GEN_TAC `y:real^N` THEN EQ_TAC THENL
 340    [DISCH_THEN(X_CHOOSE_THEN `u:real^N->real` STRIP_ASSUME_TAC) THEN
 341     EXISTS_TAC `vsum (s UNION t) (\x. (u o (f:real^M->real^N)) x % x)` THEN
 342     ASM_REWRITE_TAC[] THEN
 343     EXISTS_TAC `(u:real^N->real) o (f:real^M->real^N)` THEN
 344     ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[o_THM];
 345     MP_TAC(ISPEC `f:real^M->real^N` LINEAR_INJECTIVE_LEFT_INVERSE) THEN
 346     ASM_REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM] THEN
 347     DISCH_THEN(X_CHOOSE_THEN `g:real^N->real^M` STRIP_ASSUME_TAC) THEN
 348     DISCH_THEN(X_CHOOSE_THEN `x:real^M`
 349      (CONJUNCTS_THEN2 SUBST1_TAC MP_TAC)) THEN
 350     DISCH_THEN(X_CHOOSE_THEN `u:real^M->real` STRIP_ASSUME_TAC) THEN
 351     EXISTS_TAC `(u:real^M->real) o (g:real^N->real^M)` THEN
 352     ASM_REWRITE_TAC[o_DEF; ETA_AX]]);;
 353
 354 let AFF_GE_INJECTIVE_LINEAR_IMAGE = prove
 355  (`!f:real^M->real^N s t.
 356         linear f /\ (!x y. f x = f y ==> x = y)
 357         ==> aff_ge (IMAGE f s) (IMAGE f t) = IMAGE f (aff_ge s t)`,
 358   REWRITE_TAC[aff_ge_def; AFFSIGN_INJECTIVE_LINEAR_IMAGE]);;
 359
 360 let AFF_GT_INJECTIVE_LINEAR_IMAGE = prove
 361  (`!f:real^M->real^N s t.
 362         linear f /\ (!x y. f x = f y ==> x = y)
 363         ==> aff_gt (IMAGE f s) (IMAGE f t) = IMAGE f (aff_gt s t)`,
 364   REWRITE_TAC[aff_gt_def; AFFSIGN_INJECTIVE_LINEAR_IMAGE]);;
 365
 366 let AFF_LE_INJECTIVE_LINEAR_IMAGE = prove
 367  (`!f:real^M->real^N s t.
 368         linear f /\ (!x y. f x = f y ==> x = y)
 369         ==> aff_le (IMAGE f s) (IMAGE f t) = IMAGE f (aff_le s t)`,
 370   REWRITE_TAC[aff_le_def; AFFSIGN_INJECTIVE_LINEAR_IMAGE]);;
 371
 372 let AFF_LT_INJECTIVE_LINEAR_IMAGE = prove
 373  (`!f:real^M->real^N s t.
 374         linear f /\ (!x y. f x = f y ==> x = y)
 375         ==> aff_lt (IMAGE f s) (IMAGE f t) = IMAGE f (aff_lt s t)`,
 376   REWRITE_TAC[aff_lt_def; AFFSIGN_INJECTIVE_LINEAR_IMAGE]);;
 377
 378 add_linear_invariants
 379   [AFFSIGN_INJECTIVE_LINEAR_IMAGE;
 380    AFF_GE_INJECTIVE_LINEAR_IMAGE;
 381    AFF_GT_INJECTIVE_LINEAR_IMAGE;
 382    AFF_LE_INJECTIVE_LINEAR_IMAGE;
 383    AFF_LT_INJECTIVE_LINEAR_IMAGE];;
 384
 385 let IN_AFFSIGN_TRANSLATION = prove
 386  (`!sgn s t a v:real^N.
 387         affsign sgn s t v
 388         ==> affsign sgn (IMAGE (\x. a + x) s) (IMAGE (\x. a + x) t) (a + v)`,
 389   REPEAT GEN_TAC THEN REWRITE_TAC[affsign; lin_combo] THEN
 390   ONCE_REWRITE_TAC[SET_RULE `(!x. s x ==> p x) <=> (!x. x IN s ==> p x)`] THEN
 391   DISCH_THEN(X_CHOOSE_THEN `f:real^N->real`
 392    (CONJUNCTS_THEN2 SUBST_ALL_TAC STRIP_ASSUME_TAC)) THEN
 393   EXISTS_TAC `\x. (f:real^N->real)(x - a)` THEN
 394   ASM_REWRITE_TAC[GSYM IMAGE_UNION] THEN REPEAT CONJ_TAC THENL
 395    [ALL_TAC;
 396     ASM_REWRITE_TAC[FORALL_IN_IMAGE; ETA_AX;
 397                     VECTOR_ARITH `(a + x) - a:real^N = x`];
 398     W(MP_TAC o PART_MATCH (lhs o rand) SUM_IMAGE o lhs o snd) THEN
 399     SIMP_TAC[VECTOR_ARITH `a + x:real^N = a + y <=> x = y`] THEN
 400     ASM_REWRITE_TAC[o_DEF; VECTOR_ADD_SUB; ETA_AX]] THEN
 401   MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
 402    `a + vsum {x | x IN s UNION t /\ ~(f x = &0)} (\v:real^N. f v % v)` THEN
 403   CONJ_TAC THENL
 404    [AP_TERM_TAC THEN MATCH_MP_TAC VSUM_SUPERSET THEN
 405     REWRITE_TAC[VECTOR_MUL_EQ_0; SUBSET; IN_ELIM_THM] THEN MESON_TAC[];
 406     ALL_TAC] THEN
 407   MATCH_MP_TAC EQ_TRANS THEN
 408   EXISTS_TAC `vsum (IMAGE (\x:real^N. a + x)
 409                           {x | x IN s UNION t /\ ~(f x = &0)})
 410                    (\v. f(v - a) % v)` THEN
 411   CONJ_TAC THENL
 412    [ALL_TAC;
 413     CONV_TAC SYM_CONV THEN MATCH_MP_TAC VSUM_SUPERSET THEN
 414     CONJ_TAC THENL [SET_TAC[]; ALL_TAC] THEN
 415     ASM_REWRITE_TAC[IMP_CONJ; FORALL_IN_IMAGE; VECTOR_MUL_EQ_0] THEN
 416     REWRITE_TAC[VECTOR_ADD_SUB] THEN SET_TAC[]] THEN
 417   SUBGOAL_THEN `FINITE {x:real^N | x IN s UNION t /\ ~(f x = &0)}`
 418   ASSUME_TAC THENL
 419    [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE
 420      (LAND_CONV o RATOR_CONV o RATOR_CONV) [sum]) THEN
 421     ONCE_REWRITE_TAC[ITERATE_EXPAND_CASES] THEN
 422     REWRITE_TAC[GSYM sum; support; NEUTRAL_REAL_ADD] THEN
 423     COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_OF_NUM_EQ; ARITH_EQ];
 424     ALL_TAC] THEN
 425   W(MP_TAC o PART_MATCH (lhs o rand) VSUM_IMAGE o rhs o snd) THEN
 426   ASM_SIMP_TAC[VECTOR_ARITH `a + x:real^N = a + y <=> x = y`] THEN
 427   DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[o_DEF; VECTOR_ADD_SUB] THEN
 428   ASM_SIMP_TAC[VECTOR_ADD_LDISTRIB; VSUM_ADD] THEN
 429   AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[VSUM_RMUL] THEN
 430   GEN_REWRITE_TAC LAND_CONV [GSYM VECTOR_MUL_LID] THEN
 431   AP_THM_TAC THEN AP_TERM_TAC THEN FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN
 432   MATCH_MP_TAC SUM_SUPERSET THEN SET_TAC[]);;
 433
 434 let AFFSIGN_TRANSLATION = prove
 435  (`!a:real^N sgn s t.
 436         affsign sgn (IMAGE (\x. a + x) s) (IMAGE (\x. a + x) t) =
 437         IMAGE (\x. a + x) (affsign sgn s t)`,
 438   REPEAT GEN_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL
 439    [REWRITE_TAC[SUBSET; IN] THEN GEN_TAC THEN
 440     DISCH_THEN(MP_TAC o SPEC `--a:real^N` o
 441       MATCH_MP IN_AFFSIGN_TRANSLATION) THEN
 442     REWRITE_TAC[GSYM IMAGE_o; o_DEF; VECTOR_ARITH `--a + a + x:real^N = x`;
 443                 IMAGE_ID] THEN
 444     DISCH_TAC THEN REWRITE_TAC[IMAGE; IN_ELIM_THM] THEN
 445     EXISTS_TAC `--a + x:real^N` THEN ASM_REWRITE_TAC[IN] THEN VECTOR_ARITH_TAC;
 446     REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN GEN_TAC THEN REWRITE_TAC[IN] THEN
 447     DISCH_THEN(MP_TAC o SPEC `a:real^N` o MATCH_MP IN_AFFSIGN_TRANSLATION) THEN
 448     REWRITE_TAC[]]);;
 449
 450 let AFF_GE_TRANSLATION = prove
 451  (`!a:real^N s t.
 452         aff_ge (IMAGE (\x. a + x) s) (IMAGE (\x. a + x) t) =
 453         IMAGE (\x. a + x) (aff_ge s t)`,
 454   REWRITE_TAC[aff_ge_def; AFFSIGN_TRANSLATION]);;
 455
 456 let AFF_GT_TRANSLATION = prove
 457  (`!a:real^N s t.
 458         aff_gt (IMAGE (\x. a + x) s) (IMAGE (\x. a + x) t) =
 459         IMAGE (\x. a + x) (aff_gt s t)`,
 460   REWRITE_TAC[aff_gt_def; AFFSIGN_TRANSLATION]);;
 461
 462 let AFF_LE_TRANSLATION = prove
 463  (`!a:real^N s t.
 464         aff_le (IMAGE (\x. a + x) s) (IMAGE (\x. a + x) t) =
 465         IMAGE (\x. a + x) (aff_le s t)`,
 466   REWRITE_TAC[aff_le_def; AFFSIGN_TRANSLATION]);;
 467
 468 let AFF_LT_TRANSLATION = prove
 469  (`!a:real^N s t.
 470         aff_lt (IMAGE (\x. a + x) s) (IMAGE (\x. a + x) t) =
 471         IMAGE (\x. a + x) (aff_lt s t)`,
 472   REWRITE_TAC[aff_lt_def; AFFSIGN_TRANSLATION]);;
 473
 474 add_translation_invariants
 475   [AFFSIGN_TRANSLATION;
 476    AFF_GE_TRANSLATION;
 477    AFF_GT_TRANSLATION;
 478    AFF_LE_TRANSLATION;
 479    AFF_LT_TRANSLATION];;
 480
 481 (* ------------------------------------------------------------------------- *)
 482 (* Example 3.                                                                *)
 483 (* ------------------------------------------------------------------------- *)
 484
 485 let NOT_COPLANAR_NOT_COLLINEAR = prove
 486  (`!v1 v2 v3 w:real^N. ~coplanar {v1, v2, v3, w} ==> ~collinear {v1, v2, v3}`,
 487   REPEAT GEN_TAC THEN
 488   REWRITE_TAC[COLLINEAR_AFFINE_HULL; coplanar; CONTRAPOS_THM] THEN
 489   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `x:real^N` THEN
 490   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `y:real^N` THEN
 491   REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET] THEN STRIP_TAC THEN
 492   EXISTS_TAC `w:real^N` THEN ASM_SIMP_TAC[HULL_INC; IN_INSERT] THEN
 493   REPEAT CONJ_TAC THEN
 494   MATCH_MP_TAC(SET_RULE `!t. t SUBSET s /\ x IN t ==> x IN s`) THEN
 495   EXISTS_TAC `affine hull {x:real^N,y}` THEN
 496   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC HULL_MONO THEN SET_TAC[]);;
 497
 498 let AFFSIGN = prove
 499  (`affsign sgn s t =
 500         {y | ?f. y = vsum (s UNION t) (\v. f v % v) /\
 501                 (!w. w IN t ==> sgn(f w)) /\
 502                 sum (s UNION t) f = &1}`,
 503   REWRITE_TAC[FUN_EQ_THM; affsign; lin_combo; IN_ELIM_THM] THEN
 504   REWRITE_TAC[IN]);;
 505
 506 let IN_AFFSIGN = prove
 507  (`y IN affsign sgn s t <=>
 508         ?u. (!x. x IN (s UNION t) ==> x IN t ==> sgn(u x)) /\
 509             sum (s UNION t) u = &1 /\
 510             vsum (s UNION t) (\x. u(x) % x) = y`,
 511   REWRITE_TAC[AFFSIGN; IN_ELIM_THM] THEN SET_TAC[]);;
 512
 513 let LEMMA = prove
 514  (`!v1 v2 v3 w:real^3 p.
 515      plane p /\ {v1, v2, v3} SUBSET p /\
 516      ~coplanar {v1, v2, v3, w}
 517      ==> (?n n'. norm(n - n') = &1 /\
 518                 (!x. x IN aff_ge {v1, v2, v3} {w} <=>
 519                      (?xx h.
 520                           xx IN affine hull {v1, v2, v3} /\
 521                           &0 <= h /\
 522                           x - xx = h % (n - n'))) /\
 523                 (!x y.
 524                      {x, y} SUBSET affine hull {v1, v2, v3}
 525                      ==> (n - n') dot (x - y) = &0))`,
 526   GEOM_HORIZONTAL_PLANE_TAC `p:real^3->bool` THEN
 527   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 528   REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_ELIM_THM] THEN
 529   MAP_EVERY (fun t ->
 530    ASM_CASES_TAC t THENL [ASM_REWRITE_TAC[INSERT_AC; COPLANAR_3]; ALL_TAC])
 531    [`v1:real^3 = v2`; `v1:real^3 = v3`; `v2:real^3 = v3`;
 532     `v1:real^3 = w`; `v2:real^3 = w`; `v3:real^3 = w`] THEN
 533   STRIP_TAC THEN
 534   ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
 535   EXISTS_TAC `vec 0:real^3` THEN REWRITE_TAC[VECTOR_SUB_RZERO] THEN
 536   SUBGOAL_THEN `~((w:real^3)$3 = &0)` ASSUME_TAC THENL
 537    [DISCH_TAC THEN UNDISCH_TAC `~coplanar{v1:real^3,v2,v3,w}` THEN
 538     REWRITE_TAC[coplanar] THEN
 539     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [plane]) THEN
 540     REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN
 541     DISCH_THEN(SUBST1_TAC o SYM o CONJUNCT2) THEN
 542     ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_ELIM_THM];
 543     ALL_TAC] THEN
 544   SUBGOAL_THEN `(vec 0:real^3) IN affine hull {v1,v2,v3}` ASSUME_TAC THENL
 545    [MP_TAC(ISPEC `{v1:real^3,v2,v3}` DEPENDENT_BIGGERSET_GENERAL) THEN
 546     ANTS_TAC THENL
 547      [DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[GT] THEN
 548       MATCH_MP_TAC LET_TRANS THEN EXISTS_TAC `dim {z:real^3 | z$3 = &0}` THEN
 549       CONJ_TAC THENL [MATCH_MP_TAC DIM_SUBSET THEN ASM SET_TAC[]; ALL_TAC] THEN
 550       SIMP_TAC[DIM_SPECIAL_HYPERPLANE; DIMINDEX_3; ARITH] THEN
 551       REWRITE_TAC[GSYM NOT_LE] THEN DISCH_TAC THEN
 552       FIRST_ASSUM(MP_TAC o MATCH_MP NOT_COPLANAR_NOT_COLLINEAR) THEN
 553       REWRITE_TAC[] THEN MATCH_MP_TAC COLLINEAR_SMALL THEN
 554       ASM_REWRITE_TAC[FINITE_INSERT; FINITE_RULES];
 555       ALL_TAC] THEN
 556     REWRITE_TAC[DEPENDENT_AFFINE_DEPENDENT_CASES] THEN
 557     ASM_MESON_TAC[AFFINE_DEPENDENT_IMP_COLLINEAR_3;
 558                   NOT_COPLANAR_NOT_COLLINEAR];
 559     ALL_TAC] THEN
 560   SUBGOAL_THEN `affine hull {v1,v2,v3} = {z:real^3 | z$3 = &0}`
 561   ASSUME_TAC THENL
 562    [ASM_SIMP_TAC[AFFINE_HULL_EQ_SPAN] THEN
 563     MATCH_MP_TAC(SET_RULE
 564      `!s. t SUBSET u /\ s SUBSET t /\ u SUBSET s ==> t = u`) THEN
 565     EXISTS_TAC `span {x - v1:real^3 | x IN {v2,v3}}` THEN CONJ_TAC THENL
 566      [REWRITE_TAC[SUBSET] THEN MATCH_MP_TAC SPAN_INDUCT THEN
 567       REWRITE_TAC[SET_RULE `(\x. x IN s) = s`] THEN
 568       SIMP_TAC[SUBSPACE_SPECIAL_HYPERPLANE; DIMINDEX_3; ARITH] THEN
 569       ASM_SIMP_TAC[FORALL_IN_INSERT; NOT_IN_EMPTY; IN_ELIM_THM];
 570       ALL_TAC] THEN
 571     CONJ_TAC THENL
 572      [GEN_REWRITE_TAC RAND_CONV [GSYM SPAN_SPAN] THEN
 573       MATCH_MP_TAC SPAN_MONO THEN
 574       REWRITE_TAC[SUBSET; FORALL_IN_GSPEC; FORALL_IN_INSERT; NOT_IN_EMPTY] THEN
 575       MESON_TAC[SPAN_SUB; SPAN_INC; IN_INSERT; SUBSET];
 576       ALL_TAC] THEN
 577     MATCH_MP_TAC CARD_GE_DIM_INDEPENDENT THEN REPEAT CONJ_TAC THENL
 578      [REWRITE_TAC[SUBSET; FORALL_IN_GSPEC; IN_ELIM_THM;
 579                   FORALL_IN_INSERT; NOT_IN_EMPTY] THEN
 580       ASM_SIMP_TAC[VECTOR_SUB_COMPONENT; DIMINDEX_3; ARITH; REAL_SUB_REFL];
 581       REWRITE_TAC[independent] THEN
 582       DISCH_THEN(MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
 583         DEPENDENT_IMP_AFFINE_DEPENDENT)) THEN
 584       ASM_REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
 585       ASM_MESON_TAC[AFFINE_DEPENDENT_IMP_COLLINEAR_3;
 586                     NOT_COPLANAR_NOT_COLLINEAR];
 587       SIMP_TAC[DIM_SPECIAL_HYPERPLANE; DIMINDEX_3; ARITH] THEN
 588       ONCE_REWRITE_TAC[SIMPLE_IMAGE] THEN
 589       SIMP_TAC[CARD_IMAGE_INJ; FINITE_INSERT; FINITE_RULES;
 590                VECTOR_ARITH `x - a:real^N = y - a <=> x = y`] THEN
 591       ASM_SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_RULES;
 592                    IN_INSERT; NOT_IN_EMPTY; ARITH]];
 593     ALL_TAC] THEN
 594   FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (REAL_ARITH
 595    `~(x = &0) ==> &0 < x \/ &0 < --x`))
 596   THENL
 597    [EXISTS_TAC `basis 3:real^3`; EXISTS_TAC `--(basis 3):real^3`] THEN
 598   ASM_SIMP_TAC[NORM_BASIS; DIMINDEX_3; ARITH; IN_ELIM_THM; DOT_BASIS;
 599                NORM_NEG; DOT_LNEG; DIMINDEX_3; ARITH; VECTOR_SUB_COMPONENT;
 600                REAL_SUB_REFL; REAL_NEG_0] THEN
 601   X_GEN_TAC `x:real^3` THEN
 602   REWRITE_TAC[aff_ge_def; IN_AFFSIGN; sgn_ge] THEN
 603   REWRITE_TAC[SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`] THEN
 604   REWRITE_TAC[SET_RULE `x IN {a} <=> a = x`] THEN
 605   SIMP_TAC[AFFINE_HULL_FINITE_STEP_GEN; REAL_LE_ADD; FINITE_INSERT;
 606            CONJUNCT1 FINITE_RULES; REAL_ARITH `&0 <= x / &2 <=> &0 <= x`;
 607            RIGHT_EXISTS_AND_THM] THEN
 608   ASM_REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN
 609   REWRITE_TAC[REAL_ARITH `x - y:real = z <=> x = y + z`] THEN
 610   REWRITE_TAC[VECTOR_ARITH `x - y:real^3 = z <=> x = y + z`] THEN
 611   REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID] THEN
 612   REWRITE_TAC[REAL_ARITH `&1 = x + y <=> x + y = &1`] THEN
 613   EQ_TAC THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THENL
 614    [MAP_EVERY X_GEN_TAC [`a:real`; `b:real`; `c:real`; `h:real`] THEN
 615     STRIP_TAC THEN
 616     EXISTS_TAC `a % v1 + b % v2 + c % v3 +
 617                 h % ((w:real^3)$1 % basis 1 + w$2 % basis 2):real^3` THEN
 618     EXISTS_TAC `h * (w:real^3)$3` THEN
 619     ASM_SIMP_TAC[REAL_LE_MUL; REAL_LT_IMP_LE] THEN
 620     ASM_SIMP_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; BASIS_COMPONENT;
 621                  DIMINDEX_3; ARITH; REAL_MUL_RZERO; REAL_ADD_RID] THEN
 622     REWRITE_TAC[GSYM VECTOR_MUL_ASSOC; GSYM VECTOR_ADD_LDISTRIB;
 623                 GSYM VECTOR_ADD_ASSOC] THEN
 624     REPLICATE_TAC 4 AP_TERM_TAC THEN
 625     GEN_REWRITE_TAC LAND_CONV [GSYM BASIS_EXPANSION] THEN
 626     REWRITE_TAC[DIMINDEX_3] THEN CONV_TAC(ONCE_DEPTH_CONV NUMSEG_CONV) THEN
 627     SIMP_TAC[VSUM_CLAUSES; FINITE_INSERT; CONJUNCT1 FINITE_RULES] THEN
 628     REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; ARITH_EQ; VECTOR_ADD_RID];
 629
 630     MAP_EVERY X_GEN_TAC [`y:real^3`; `h:real`] THEN STRIP_TAC THEN
 631     UNDISCH_TAC `(vec 0:real^3) IN affine hull {v1,v2,v3}` THEN
 632     SUBGOAL_THEN `(y - h / (w:real^3)$3 % (w$1 % basis 1 + w$2 % basis 2))
 633                   IN affine hull {v1:real^3,v2,v3}` MP_TAC THENL
 634      [ASM_SIMP_TAC[IN_ELIM_THM; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT;
 635             VECTOR_SUB_COMPONENT; BASIS_COMPONENT; ARITH; DIMINDEX_3] THEN
 636       REAL_ARITH_TAC;
 637       ALL_TAC] THEN
 638     SIMP_TAC[AFFINE_HULL_FINITE; FINITE_INSERT; CONJUNCT1 FINITE_RULES;
 639              AFFINE_HULL_FINITE_STEP; IN_ELIM_THM] THEN
 640     REWRITE_TAC[REAL_ARITH `x - y:real = z <=> x = y + z`] THEN
 641     REWRITE_TAC[VECTOR_ARITH `x - y:real^3 = z <=> x = y + z`] THEN
 642     REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID; LEFT_IMP_EXISTS_THM] THEN
 643     REWRITE_TAC[REAL_ARITH `&1 = x + y <=> x + y = &1`] THEN
 644     MAP_EVERY X_GEN_TAC [`a:real`; `b:real`; `c:real`] THEN STRIP_TAC THEN
 645     MAP_EVERY X_GEN_TAC [`a':real`; `b':real`; `c':real`] THEN
 646     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (ASSUME_TAC o SYM)) THEN
 647     MAP_EVERY EXISTS_TAC
 648      [`a + (&1 - (a + b + c + h / (w:real^3)$3)) * a'`;
 649       `b + (&1 - (a + b + c + h / (w:real^3)$3)) * b'`;
 650       `c + (&1 - (a + b + c + h / (w:real^3)$3)) * c'`; `h / (w:real^3)$3`] THEN
 651     ASM_REWRITE_TAC[REAL_ARITH
 652      `(a + x * a') + (b + x * b') + (c + x * c') + h:real =
 653       (a + b + c + h) + x * (a' + b' + c')`] THEN
 654     ASM_SIMP_TAC[REAL_LE_DIV; REAL_LT_IMP_LE] THEN
 655     CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
 656     REWRITE_TAC[VECTOR_ARITH
 657      `(a + x * a') % v1 + (b + x * b') % v2 + (c + x * c') % v3 + h:real^N =
 658       (a % v1 + b % v2 + c % v3) + x % (a' % v1 + b' % v2 + c' % v3) + h`] THEN
 659     ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
 660     REWRITE_TAC[VECTOR_ARITH `(x + a) + y:real^3 = a + z <=> x + y = z`] THEN
 661     GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM BASIS_EXPANSION] THEN
 662     REWRITE_TAC[DIMINDEX_3] THEN CONV_TAC(ONCE_DEPTH_CONV NUMSEG_CONV) THEN
 663     SIMP_TAC[VSUM_CLAUSES; FINITE_INSERT; CONJUNCT1 FINITE_RULES] THEN
 664     REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; ARITH_EQ; VECTOR_ADD_RID] THEN
 665     REWRITE_TAC[VECTOR_ADD_LDISTRIB; GSYM VECTOR_ADD_ASSOC] THEN
 666     ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_DIV_RMUL; REAL_LT_IMP_NZ];
 667
 668     MAP_EVERY X_GEN_TAC [`a:real`; `b:real`; `c:real`; `h:real`] THEN
 669     STRIP_TAC THEN
 670     EXISTS_TAC `a % v1 + b % v2 + c % v3 +
 671                 h % ((w:real^3)$1 % basis 1 + w$2 % basis 2):real^3` THEN
 672     EXISTS_TAC `h * --((w:real^3)$3)` THEN
 673     ASM_SIMP_TAC[REAL_LE_MUL; REAL_LT_IMP_LE] THEN
 674     REWRITE_TAC[VECTOR_ARITH `(x * --y) % --z:real^N = (x * y) % z`] THEN
 675     ASM_SIMP_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; BASIS_COMPONENT;
 676                  DIMINDEX_3; ARITH; REAL_MUL_RZERO; REAL_ADD_RID] THEN
 677     REWRITE_TAC[GSYM VECTOR_MUL_ASSOC; GSYM VECTOR_ADD_LDISTRIB;
 678                 GSYM VECTOR_ADD_ASSOC] THEN
 679     REPLICATE_TAC 4 AP_TERM_TAC THEN
 680     GEN_REWRITE_TAC LAND_CONV [GSYM BASIS_EXPANSION] THEN
 681     REWRITE_TAC[DIMINDEX_3] THEN CONV_TAC(ONCE_DEPTH_CONV NUMSEG_CONV) THEN
 682     SIMP_TAC[VSUM_CLAUSES; FINITE_INSERT; CONJUNCT1 FINITE_RULES] THEN
 683     REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; ARITH_EQ; VECTOR_ADD_RID];
 684
 685     MAP_EVERY X_GEN_TAC [`y:real^3`; `h:real`] THEN STRIP_TAC THEN
 686     UNDISCH_TAC `(vec 0:real^3) IN affine hull {v1,v2,v3}` THEN
 687     SUBGOAL_THEN `(y - h / --((w:real^3)$3) % (w$1 % basis 1 + w$2 % basis 2))
 688                   IN affine hull {v1:real^3,v2,v3}` MP_TAC THENL
 689      [ASM_SIMP_TAC[IN_ELIM_THM; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT;
 690             VECTOR_SUB_COMPONENT; BASIS_COMPONENT; ARITH; DIMINDEX_3] THEN
 691       REAL_ARITH_TAC;
 692       ALL_TAC] THEN
 693     SIMP_TAC[AFFINE_HULL_FINITE; FINITE_INSERT; CONJUNCT1 FINITE_RULES;
 694              AFFINE_HULL_FINITE_STEP; IN_ELIM_THM] THEN
 695     REWRITE_TAC[REAL_ARITH `x - y:real = z <=> x = y + z`] THEN
 696     REWRITE_TAC[VECTOR_ARITH `x - y:real^3 = z <=> x = y + z`] THEN
 697     REWRITE_TAC[VECTOR_ADD_RID; REAL_ADD_RID; LEFT_IMP_EXISTS_THM] THEN
 698     REWRITE_TAC[REAL_ARITH `&1 = x + y <=> x + y = &1`] THEN
 699     MAP_EVERY X_GEN_TAC [`a:real`; `b:real`; `c:real`] THEN STRIP_TAC THEN
 700     MAP_EVERY X_GEN_TAC [`a':real`; `b':real`; `c':real`] THEN
 701     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (ASSUME_TAC o SYM)) THEN
 702     MAP_EVERY EXISTS_TAC
 703      [`a + (&1 - (a + b + c + h / --((w:real^3)$3))) * a'`;
 704       `b + (&1 - (a + b + c + h / --((w:real^3)$3))) * b'`;
 705       `c + (&1 - (a + b + c + h / --((w:real^3)$3))) * c'`;
 706       `h / --((w:real^3)$3)`] THEN
 707     ASM_REWRITE_TAC[REAL_ARITH
 708      `(a + x * a') + (b + x * b') + (c + x * c') + h:real =
 709       (a + b + c + h) + x * (a' + b' + c')`] THEN
 710     ASM_SIMP_TAC[REAL_LE_DIV; REAL_LT_IMP_LE] THEN
 711     CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
 712     REWRITE_TAC[VECTOR_ARITH
 713      `(a + x * a') % v1 + (b + x * b') % v2 + (c + x * c') % v3 + h:real^N =
 714       (a % v1 + b % v2 + c % v3) + x % (a' % v1 + b' % v2 + c' % v3) + h`] THEN
 715     ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
 716     REWRITE_TAC[VECTOR_ARITH `(x + a) + y:real^3 = a + z <=> x + y = z`] THEN
 717     GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM BASIS_EXPANSION] THEN
 718     REWRITE_TAC[DIMINDEX_3] THEN CONV_TAC(ONCE_DEPTH_CONV NUMSEG_CONV) THEN
 719     SIMP_TAC[VSUM_CLAUSES; FINITE_INSERT; CONJUNCT1 FINITE_RULES] THEN
 720     REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY; ARITH_EQ; VECTOR_ADD_RID] THEN
 721     REWRITE_TAC[VECTOR_ADD_LDISTRIB; GSYM VECTOR_ADD_ASSOC] THEN
 722     REWRITE_TAC[real_div; REAL_INV_NEG; REAL_MUL_RNEG] THEN
 723     REWRITE_TAC[VECTOR_MUL_RNEG; VECTOR_MUL_LNEG; GSYM real_div] THEN
 724     ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_DIV_RMUL; REAL_LT_IMP_NZ]]);;
 725
 726 let THEOREM = prove
 727  (`!v1 v2 v3 w:real^3.
 728      ~coplanar {v1, v2, v3, w}
 729      ==> (?nor. norm nor = &1 /\
 730                 (!x. x IN aff_ge {v1, v2, v3} {w} <=>
 731                      (?xx h.
 732                           xx IN affine hull {v1, v2, v3} /\
 733                           &0 <= h /\
 734                           x = xx + h % nor)) /\
 735                 (!x y.
 736                      {x, y} SUBSET affine hull {v1, v2, v3}
 737                      ==> nor dot (x - y) = &0))`,
 738   REPEAT STRIP_TAC THEN
 739   ONCE_REWRITE_TAC[VECTOR_ARITH `x:real^3 = y + h % z <=> x - y = h % z`] THEN
 740   MATCH_MP_TAC(MESON[] `(?a b. P(a - b)) ==> ?a:real^3. P a`) THEN
 741   MATCH_MP_TAC LEMMA THEN ASM_REWRITE_TAC[] THEN
 742   EXISTS_TAC `affine hull {v1:real^3,v2,v3}` THEN
 743   REWRITE_TAC[HULL_SUBSET; plane] THEN
 744   ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);;