1 (* ========================================================================= *)
2 (* Examples of using the "without loss of generality" tactics. *)
3 (* ========================================================================= *)
5 needs "Multivariate/wlog.ml";;
7 (* ------------------------------------------------------------------------- *)
9 (* ------------------------------------------------------------------------- *)
12 (`(?y. y pow 2 = a) <=> &0 <= a`,
13 MESON_TAC[SQRT_POW_2; REAL_LE_SQUARE; REAL_POW_2]);;
16 (`!u1:real^3 u2 p a b.
20 dist(u1,u2) <= a + b /\
21 abs(a - b) < dist(u1,u2) /\
26 &1 / &2 % (d1 + d2) IN affine hull {u1, u2} /\
31 (*** First, rotate the plane p to the special case z$3 = &0 ***)
33 GEOM_HORIZONTAL_PLANE_TAC `p:real^3->bool` THEN
35 (*** Now reshuffle the goal to have explicit restricted quantifiers ***)
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
44 (*** Now replace quantifiers over real^3 with those over real^2 ***)
48 (*** Tidy the goal a little ***)
50 REWRITE_TAC[RIGHT_IMP_FORALL_THM; IMP_IMP; GSYM CONJ_ASSOC] THEN
52 (*** Choose u1 as the origin ***)
54 GEOM_ORIGIN_TAC `u1:real^2` THEN
56 (*** Rotate the point u2 onto the x-axis ***)
58 GEOM_HORIZONTAL_LINE_TAC `u2:real^2` THEN
60 (*** Only now introduce coordinates ***)
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;
72 DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o GSYM) STRIP_ASSUME_TAC) THEN
73 REWRITE_TAC[EXISTS_VECTOR_2] THEN
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
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
87 (*** Now finally dive in and solve the algebraic problem ***)
89 ASM_SIMP_TAC[REAL_FIELD
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
102 (*** Can just use SOS: this proof was found by SOS_RULE ***)
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
111 (* ------------------------------------------------------------------------- *)
112 (* Definition of "opposite" for example 2, and its invariance theorems. *)
113 (* ------------------------------------------------------------------------- *)
115 let opposite = new_definition
117 (&1 / &2 % (a + b)) IN p /\
118 (!x y:real^N. {x,y} SUBSET p ==> (x - y) dot (a - b) = &0)`;;
120 let OPPOSITE_TRANSLATION_EQ = prove
121 (`!c a b p. opposite (c + a) (c + b) (IMAGE (\x. c + x) p) <=>
123 REWRITE_TAC[opposite] THEN GEOM_TRANSLATE_TAC[]);;
125 add_translation_invariants [OPPOSITE_TRANSLATION_EQ];;
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]);;
136 add_linear_invariants [OPPOSITE_LINEAR_IMAGE_EQ];;
138 (* ------------------------------------------------------------------------- *)
140 (* ------------------------------------------------------------------------- *)
142 let AFFINE_PLANE = prove
143 (`!p. plane p ==> affine p`,
144 SIMP_TAC[plane; LEFT_IMP_EXISTS_THM; AFFINE_AFFINE_HULL]);;
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`))
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]);;
162 let TRUONG_OPPOSITE_LEMMA = prove
163 (`!p a b bb m x y:real^3.
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} = {})`,
170 (*** Make the plane p the xy-plane ***)
172 GEOM_HORIZONTAL_PLANE_TAC `p:real^3->bool` THEN
174 (*** Rewrite with explicit restricted quantifiers ***)
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
179 (*** Now replace quantifiers over real^3 with those over real^2 ***)
183 (*** Let x be the origin, and y on the x-axis ***)
185 GEOM_ORIGIN_TAC `x:real^2` THEN
186 GEOM_HORIZONTAL_LINE_TAC `y:real^2` THEN
188 (*** Make a few simplifications ***)
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
196 (*** Show aff{x,y} is now exactly the x-axis ***)
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
206 SUBGOAL_THEN `u = (&1 - u$1 / (y:real^2)$1) % vec 0 +
207 (u$1 / (y:real^2)$1) % y`
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
216 (*** Simplify a bit more ***)
218 SIMP_TAC[IN_ELIM_THM; REAL_ARITH `inv(&2) * (x + y) = &0 <=> y = --x`] THEN
219 REPEAT STRIP_TAC THEN
221 (*** Finally, make a 4-way case split then apply the lemma to each ***)
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}`]);;
230 let TRUONG_OPPOSITE_THM = prove
231 (`!a b bb x y:real^3 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]);;
253 (* ------------------------------------------------------------------------- *)
254 (* Affsign variants for example 3, and invariance theorems. *)
255 (* ------------------------------------------------------------------------- *)
257 let lin_combo = new_definition
258 `lin_combo V f = vsum V (\v. f v % (v:real^N))`;;
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))`;;
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))`;;
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`;;
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
284 let AFFSIGN_ALT = prove
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[]);;
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[]);;
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))`,
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
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
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)}`
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]]);;
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]);;
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]);;
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]);;
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]);;
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];;
385 let IN_AFFSIGN_TRANSLATION = prove
386 (`!sgn s t a v:real^N.
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
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
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[];
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
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)}`
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];
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[]);;
434 let AFFSIGN_TRANSLATION = prove
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`;
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
450 let AFF_GE_TRANSLATION = prove
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]);;
456 let AFF_GT_TRANSLATION = prove
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]);;
462 let AFF_LE_TRANSLATION = prove
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]);;
468 let AFF_LT_TRANSLATION = prove
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]);;
474 add_translation_invariants
475 [AFFSIGN_TRANSLATION;
479 AFF_LT_TRANSLATION];;
481 (* ------------------------------------------------------------------------- *)
483 (* ------------------------------------------------------------------------- *)
485 let NOT_COPLANAR_NOT_COLLINEAR = prove
486 (`!v1 v2 v3 w:real^N. ~coplanar {v1, v2, v3, w} ==> ~collinear {v1, v2, v3}`,
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
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[]);;
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
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[]);;
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} <=>
520 xx IN affine hull {v1, v2, v3} /\
522 x - xx = h % (n - n'))) /\
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
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
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];
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
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];
556 REWRITE_TAC[DEPENDENT_AFFINE_DEPENDENT_CASES] THEN
557 ASM_MESON_TAC[AFFINE_DEPENDENT_IMP_COLLINEAR_3;
558 NOT_COPLANAR_NOT_COLLINEAR];
560 SUBGOAL_THEN `affine hull {v1,v2,v3} = {z:real^3 | z$3 = &0}`
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];
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];
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]];
594 FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (REAL_ARITH
595 `~(x = &0) ==> &0 < x \/ &0 < --x`))
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
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];
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
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
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];
668 MAP_EVERY X_GEN_TAC [`a:real`; `b:real`; `c:real`; `h:real`] 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];
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
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
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]]);;
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} <=>
732 xx IN affine hull {v1, v2, v3} /\
734 x = xx + h % nor)) /\
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]);;