1 (* ========================================================================== *)
\r
2 (* FLYSPECK - BOOK FORMALIZATION *)
\r
4 (* Chapter: Local Hypermap *)
\r
5 (* Author: John Harrison *)
\r
6 (* Date: 2012-09-16 *)
\r
7 (* ========================================================================== *)
\r
10 (* ------------------------------------------------------------------------- *)
\r
11 (* Some lemmas that should probably go in the core. *)
\r
12 (* ------------------------------------------------------------------------- *)
\r
14 module Deformation = struct
\r
17 open Local_lemmas1;;
\r
18 open Ckqowsa_4_points;;
\r
21 let COMPACT_SPHERE_0 = prove
\r
22 (`!a. compact {x | norm x = a}`,
\r
23 ONCE_REWRITE_TAC[NORM_ARITH `norm x = norm(x - vec 0)`] THEN
\r
24 REWRITE_TAC[COMPACT_SPHERE]);;
\r
26 let SEPARATE_CLOSED_CONES = prove
\r
27 (`!c d:real^N->bool.
\r
28 conic c /\ closed c /\ conic d /\ closed d /\ c INTER d SUBSET {vec 0}
\r
30 !x y. x IN c /\ y IN d ==> dist(x,y)
\r
31 >= e * max (norm x) (norm y)`,
\r
34 conic c /\ closed c /\ conic d /\ closed d /\ c INTER d SUBSET {vec 0}
\r
36 !x y. x IN c /\ y IN d ==> dist(x,y)
\r
39 [REPEAT STRIP_TAC THEN REWRITE_TAC[real_ge] THEN
\r
40 MP_TAC(ISPECL [`c INTER {x:real^N | norm x = &1}`; `d:real^N->bool`]
\r
41 SEPARATE_COMPACT_CLOSED) THEN
\r
42 ASM_SIMP_TAC[CLOSED_INTER_COMPACT; COMPACT_SPHERE_0] THEN ANTS_TAC THENL
\r
43 [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (SET_RULE
\r
44 `c INTER d SUBSET {a} ==> ~(a IN s) ==> (c INTER s) INTER d = {}`)) THEN
\r
45 REWRITE_TAC[IN_ELIM_THM; NORM_0] THEN REAL_ARITH_TAC;
\r
46 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `e:real` THEN
\r
47 REWRITE_TAC[IN_INTER; IN_ELIM_THM] THEN STRIP_TAC THEN
\r
48 ASM_REWRITE_TAC[] THEN
\r
49 MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN STRIP_TAC THEN
\r
50 ASM_CASES_TAC `x:real^N = vec 0` THEN
\r
51 ASM_REWRITE_TAC[DIST_POS_LE; REAL_MUL_RZERO; NORM_0] THEN
\r
52 FIRST_X_ASSUM(MP_TAC o SPECL
\r
53 [`inv(norm x) % x:real^N`; `inv(norm(x:real^N)) % y:real^N`]) THEN
\r
54 REWRITE_TAC[dist; NORM_MUL; GSYM VECTOR_SUB_LDISTRIB] THEN
\r
55 REWRITE_TAC[REAL_ARITH `abs x * a = a * abs x`] THEN
\r
56 REWRITE_TAC[REAL_ABS_INV; GSYM real_div; REAL_ABS_NORM] THEN
\r
57 ASM_SIMP_TAC[REAL_LE_RDIV_EQ; NORM_POS_LT] THEN
\r
58 DISCH_THEN MATCH_MP_TAC THEN
\r
59 ASM_SIMP_TAC[REAL_DIV_REFL; NORM_EQ_0] THEN
\r
60 RULE_ASSUM_TAC(REWRITE_RULE[conic]) THEN
\r
61 CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
62 ASM_SIMP_TAC[REAL_LE_INV_EQ; NORM_POS_LE]];
\r
63 REPEAT STRIP_TAC THEN FIRST_X_ASSUM(fun th ->
\r
64 MP_TAC(SPECL [`c:real^N->bool`; `d:real^N->bool`] th) THEN
\r
65 MP_TAC(SPECL [`d:real^N->bool`; `c:real^N->bool`] th)) THEN
\r
66 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[INTER_COMM] THEN
\r
67 ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM; real_ge] THEN
\r
68 X_GEN_TAC `d:real` THEN STRIP_TAC THEN
\r
69 X_GEN_TAC `e:real` THEN STRIP_TAC THEN
\r
70 EXISTS_TAC `min d e:real` THEN ASM_REWRITE_TAC[REAL_LT_MIN] THEN
\r
71 MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN STRIP_TAC THEN
\r
72 REWRITE_TAC[real_max] THEN COND_CASES_TAC THEN
\r
73 MATCH_MP_TAC REAL_LE_TRANS THENL
\r
74 [EXISTS_TAC `d * norm(y:real^N)` THEN ONCE_REWRITE_TAC[DIST_SYM];
\r
75 EXISTS_TAC `e * norm(x:real^N)`] THEN
\r
76 ASM_SIMP_TAC[] THEN MATCH_MP_TAC REAL_LE_RMUL THEN NORM_ARITH_TAC]);;
\r
78 (* ------------------------------------------------------------------------- *)
\r
79 (* More Flyspeck-specific lemmas. *)
\r
80 (* ------------------------------------------------------------------------- *)
\r
82 let AFF_GE_1_2_0 = prove
\r
84 ~(v = vec 0) /\ ~(w = vec 0)
\r
85 ==> aff_ge {vec 0} {v,w} = {a % v + b % w | &0 <= a /\ &0 <= b}`,
\r
86 SIMP_TAC[Fan.AFF_GE_1_2;
\r
87 SET_RULE `DISJOINT {a} {b,c} <=> ~(b = a) /\ ~(c = a)`] THEN
\r
88 REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
\r
89 ONCE_REWRITE_TAC[MESON[]
\r
90 `(?a b c. P b c /\ Q b c /\ R a b c /\ S b c) <=>
\r
91 (?b c. P b c /\ Q b c /\ S b c /\ ?a. R a b c)`] THEN
\r
92 REWRITE_TAC[REAL_ARITH `t + s:real = &1 <=> t = &1 - s`; EXISTS_REFL] THEN
\r
95 let AFF_GE_1_1_0 = prove
\r
96 (`!v. ~(v = vec 0) ==> aff_ge {vec 0} {v} = {a % v | &0 <= a}`,
\r
97 REPEAT STRIP_TAC THEN
\r
98 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [SET_RULE `{a} = {a,a}`] THEN
\r
99 ASM_SIMP_TAC[AFF_GE_1_2_0; GSYM VECTOR_ADD_RDISTRIB] THEN
\r
100 REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
\r
101 MESON_TAC[REAL_LE_ADD; REAL_ARITH
\r
102 `&0 <= a ==> &0 <= a / &2 /\ a / &2 + a / &2 = a`]);;
\r
104 let CONIC_AFF_GE_0 = prove
\r
105 (`!s:real^N->bool. FINITE s /\ ~(vec 0 IN s) ==> conic(aff_ge {vec 0} s)`,
\r
106 REPEAT STRIP_TAC THEN ASM_SIMP_TAC[AFF_GE_0_N; conic] THEN
\r
107 REWRITE_TAC[IN_ELIM_THM] THEN GEN_TAC THEN X_GEN_TAC `c:real` THEN
\r
108 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
\r
109 DISCH_THEN(X_CHOOSE_THEN `u:real^N->real` STRIP_ASSUME_TAC) THEN
\r
110 EXISTS_TAC `\v. c * (u:real^N->real) v` THEN
\r
111 REWRITE_TAC[GSYM VECTOR_MUL_ASSOC; VSUM_LMUL] THEN
\r
112 ASM_MESON_TAC[REAL_LE_MUL]);;
\r
114 (* ------------------------------------------------------------------------- *)
\r
115 (* More economical characterization of "fan7" *)
\r
116 (* ------------------------------------------------------------------------- *)
\r
118 let GMLWKPK = prove
\r
121 ==> (fan7(x,V,E) <=>
\r
122 !e1 e2. e1 IN E UNION {{v} | v IN V} /\
\r
123 e2 IN E UNION {{v} | v IN V}
\r
124 ==> (e1 INTER e2 = {}
\r
125 ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x}) /\
\r
126 (!v. e1 INTER e2 = {v}
\r
127 ==> aff_ge {x} e1 INTER aff_ge {x} e2 =
\r
129 REPEAT STRIP_TAC THEN REWRITE_TAC[Fan.fan7] THEN EQ_TAC THENL
\r
130 [SIMP_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING]; ALL_TAC] THEN
\r
131 MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e1:real^N->bool` THEN
\r
132 MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e2:real^N->bool` THEN
\r
133 MATCH_MP_TAC(TAUT `(p ==> q ==> r) ==> (q ==> p) ==> q ==> r`) THEN
\r
134 STRIP_TAC THEN DISCH_TAC THEN
\r
135 SUBGOAL_THEN `e1 = e2 \/ e1 INTER e2 = {} \/ (?v:real^N. e1 INTER e2 = {v})`
\r
138 STRIP_TAC THEN ASM_REWRITE_TAC[INTER_IDEMPOT] THEN
\r
139 ASM_MESON_TAC[AFF_GE_EQ_AFFINE_HULL; AFFINE_HULL_SING]] THEN
\r
140 SUBGOAL_THEN `?a b:real^N c d:real^N. e1 = {a,b} /\ e2 = {c,d}` MP_TAC THENL
\r
142 DISCH_THEN(REPEAT_TCL CHOOSE_THEN (CONJUNCTS_THEN SUBST_ALL_TAC)) THEN
\r
144 FIRST_ASSUM(CONJUNCTS_THEN MP_TAC) THEN
\r
145 REWRITE_TAC[IN_UNION; IN_ELIM_THM] THEN
\r
146 SUBGOAL_THEN `!e:real^N->bool. e IN E ==> ?v w. ~(v = w) /\ e = {v,w}`
\r
147 (LABEL_TAC "*") THENL
\r
148 [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [graph]) THEN
\r
149 MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN
\r
150 MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[IN] THEN
\r
151 CONV_TAC(LAND_CONV HAS_SIZE_CONV) THEN REWRITE_TAC[];
\r
152 ASM_MESON_TAC[SET_RULE `{v,v} = {v}`]]);;
\r
154 let GMLWKPK_ALT = prove
\r
156 graph E /\ (!e. e IN E ==> ~(x IN e))
\r
157 ==> (fan7(x,V,E) <=>
\r
158 (!e1 e2. e1 IN E UNION {{v} | v IN V} /\
\r
159 e2 IN E UNION {{v} | v IN V} /\
\r
161 ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x}) /\
\r
162 (!e1 e2 v. e1 IN E /\ e2 IN E /\ e1 INTER e2 = {v}
\r
163 ==> aff_ge {x} e1 INTER aff_ge {x} e2 =
\r
165 REPEAT STRIP_TAC THEN ASM_SIMP_TAC[GMLWKPK] THEN
\r
166 EQ_TAC THEN SIMP_TAC[IN_UNION] THEN STRIP_TAC THEN
\r
167 MATCH_MP_TAC(MESON[]
\r
168 `(!x y. R x y ==> R y x) /\
\r
169 (!x y. P x /\ P y ==> R x y) /\
\r
170 (!x y. Q x /\ Q y ==> R x y) /\
\r
171 (!x y. P x /\ Q y ==> R x y)
\r
172 ==> !x y. (P x \/ Q x) /\ (P y \/ Q y) ==> R x y`) THEN
\r
173 CONJ_TAC THENL [REWRITE_TAC[INTER_ACI]; ASM_SIMP_TAC[]] THEN CONJ_TAC THEN
\r
174 REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_GSPEC] THENL
\r
175 [SIMP_TAC[SET_RULE `{a} INTER {b} = {c} <=> a = c /\ b = c`] THEN SET_TAC[];
\r
176 X_GEN_TAC `e1:real^N->bool` THEN DISCH_TAC THEN X_GEN_TAC `v:real^N`] THEN
\r
177 SUBGOAL_THEN `(e1:real^N->bool) HAS_SIZE 2` MP_TAC THENL
\r
178 [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
\r
179 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
\r
180 MAP_EVERY X_GEN_TAC [`u:real^N`; `w:real^N`] THEN
\r
181 STRIP_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
\r
182 SIMP_TAC[SET_RULE `{a,b} INTER {c} = {d} <=> d = c /\ (a = c \/ b = c)`] THEN
\r
183 REWRITE_TAC[SET_RULE `s INTER t = t <=> t SUBSET s`] THEN
\r
184 GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
\r
185 MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[]);;
\r
187 let GMLWKPK_SIMPLE = prove
\r
189 UNIONS E SUBSET V /\ graph E /\ fan6(x,V,E) /\
\r
190 (!e. e IN E ==> ~(x IN e))
\r
191 ==> (fan7 (x,V,E) <=>
\r
193 e1 IN E UNION {{v} | v IN V} /\ e2 IN E UNION {{v} | v IN V} /\
\r
195 ==> aff_ge {x} e1 INTER aff_ge {x} e2 = {x})`,
\r
198 ~collinear{x,u,v} /\ ~collinear{x,v,w}
\r
199 ==> (~(aff_ge {x} {u,v} INTER aff_ge {x} {v,w} =
\r
200 aff_ge {x} {v}) <=>
\r
201 u IN aff_ge {x} {v,w} \/ w IN aff_ge {x} {u,v})`,
\r
202 REPEAT GEN_TAC THEN GEOM_ORIGIN_TAC `x:real^N` THEN
\r
203 REPEAT GEN_TAC THEN
\r
204 MAP_EVERY (fun t ->
\r
205 ASM_CASES_TAC t THENL
\r
206 [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC])
\r
207 [`u:real^N = v`; `w:real^N = v`;
\r
208 `u:real^N = vec 0`; `v:real^N = vec 0`; `w:real^N = vec 0`] THEN
\r
209 STRIP_TAC THEN EQ_TAC THENL
\r
210 [DISCH_THEN(MP_TAC o MATCH_MP (SET_RULE
\r
212 ==> t SUBSET s /\ t SUBSET s' ==> t PSUBSET s INTER s'`)) THEN
\r
214 [CONJ_TAC THEN MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[];
\r
215 REWRITE_TAC[PSUBSET_ALT]] THEN
\r
216 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
\r
217 ASM_SIMP_TAC[AFF_GE_1_2_0; AFF_GE_1_1_0; LEFT_IMP_EXISTS_THM] THEN
\r
218 REWRITE_TAC[IN_INTER; IMP_CONJ; FORALL_IN_GSPEC] THEN
\r
219 MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN
\r
220 DISCH_TAC THEN DISCH_TAC THEN
\r
221 REWRITE_TAC[IN_ELIM_THM; LEFT_IMP_EXISTS_THM] THEN
\r
222 MAP_EVERY X_GEN_TAC [`c:real`; `d:real`] THEN STRIP_TAC THEN
\r
223 ASM_CASES_TAC `a = &0` THENL
\r
224 [ASM_MESON_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID]; ALL_TAC] THEN
\r
225 ASM_CASES_TAC `d = &0` THENL
\r
226 [ASM_MESON_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID]; ALL_TAC] THEN
\r
227 DISCH_THEN(K ALL_TAC) THEN DISJ_CASES_TAC
\r
228 (REAL_ARITH `b <= c \/ c <= b`)
\r
230 [FIRST_X_ASSUM(MP_TAC o MATCH_MP (VECTOR_ARITH
\r
231 `a % u + b % v:real^N = c % v + d % w
\r
232 ==> a % u = (c - b) % v + d % w`)) THEN
\r
233 DISCH_THEN(MP_TAC o AP_TERM `(%) (inv a):real^N->real^N`) THEN
\r
234 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
\r
235 DISCH_THEN(K ALL_TAC) THEN DISJ1_TAC THEN
\r
236 REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
\r
237 MAP_EVERY EXISTS_TAC [`inv a * (c - b):real`; `inv a * d:real`] THEN
\r
238 ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_INV_EQ; REAL_SUB_LE];
\r
239 FIRST_X_ASSUM(MP_TAC o MATCH_MP (VECTOR_ARITH
\r
240 `a % u + b % v:real^N = c % v + d % w
\r
241 ==> d % w = (b - c) % v + a % u`)) THEN
\r
242 DISCH_THEN(MP_TAC o AP_TERM `(%) (inv d):real^N->real^N`) THEN
\r
243 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID] THEN
\r
244 DISCH_THEN(K ALL_TAC) THEN DISJ2_TAC THEN
\r
245 REWRITE_TAC[VECTOR_ADD_LDISTRIB; VECTOR_MUL_ASSOC] THEN
\r
246 MAP_EVERY EXISTS_TAC [`inv d * a:real`; `inv d * (b - c):real`] THEN
\r
247 ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_INV_EQ; REAL_SUB_LE] THEN
\r
248 REWRITE_TAC[VECTOR_ADD_SYM]];
\r
249 STRIP_TAC THEN MATCH_MP_TAC(SET_RULE
\r
250 `(?x. x IN s /\ x IN t /\ ~(x IN u)) ==> ~(s INTER t = u)`)
\r
252 [EXISTS_TAC `u:real^N` THEN ASM_REWRITE_TAC[] THEN
\r
253 ASM_SIMP_TAC[AFF_GE_1_2_0; AFF_GE_1_1_0; IN_ELIM_THM] THEN
\r
255 [MAP_EVERY EXISTS_TAC [`&1`; `&0`] THEN
\r
256 REWRITE_TAC[REAL_POS] THEN VECTOR_ARITH_TAC;
\r
257 DISCH_THEN(X_CHOOSE_THEN `a:real`
\r
258 (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
\r
259 UNDISCH_TAC `~collinear{vec 0:real^N,a % v,v}` THEN
\r
261 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`] THEN
\r
262 REWRITE_TAC[COLLINEAR_LEMMA] THEN MESON_TAC[]];
\r
263 EXISTS_TAC `w:real^N` THEN ASM_REWRITE_TAC[] THEN
\r
264 ASM_SIMP_TAC[AFF_GE_1_2_0; AFF_GE_1_1_0; IN_ELIM_THM] THEN
\r
266 [MAP_EVERY EXISTS_TAC [`&0`; `&1`] THEN
\r
267 REWRITE_TAC[REAL_POS] THEN VECTOR_ARITH_TAC;
\r
268 DISCH_THEN(X_CHOOSE_THEN `a:real`
\r
269 (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC)) THEN
\r
270 UNDISCH_TAC `~collinear{vec 0:real^N,v,a % v}` THEN
\r
271 REWRITE_TAC[COLLINEAR_LEMMA] THEN MESON_TAC[]]]]) in
\r
272 REPEAT STRIP_TAC THEN ASM_SIMP_TAC[GMLWKPK] THEN
\r
273 EQ_TAC THEN SIMP_TAC[] THEN DISCH_TAC THEN
\r
274 REWRITE_TAC[IN_UNION] THEN MATCH_MP_TAC(MESON[]
\r
275 `(!x y. R x y ==> R y x) /\
\r
276 (!x. Q x ==> !y. Q y ==> R x y) /\
\r
277 (!x. P x ==> (!y. Q y ==> R x y) /\ (!y. P y ==> R x y))
\r
278 ==> (!x y. (P x \/ Q x) /\ (P y \/ Q y) ==> R x y)`) THEN
\r
279 CONJ_TAC THENL [SIMP_TAC[INTER_ACI]; ALL_TAC] THEN
\r
280 REWRITE_TAC[FORALL_IN_GSPEC] THEN CONJ_TAC THENL
\r
281 [SIMP_TAC[SET_RULE `{a} INTER {b} = {c} <=> c = a /\ b = a`] THEN
\r
282 REWRITE_TAC[INTER_IDEMPOT];
\r
284 X_GEN_TAC `ee1:real^N->bool` THEN DISCH_TAC THEN CONJ_TAC THENL
\r
285 [X_GEN_TAC `v:real^N` THEN DISCH_TAC THEN
\r
286 REWRITE_TAC[SET_RULE `s INTER {a} = {b} <=> b = a /\ a IN s`] THEN
\r
287 SIMP_TAC[IMP_CONJ; FORALL_UNWIND_THM2] THEN DISCH_TAC THEN
\r
288 REWRITE_TAC[SET_RULE `s INTER t = t <=> t SUBSET s`] THEN
\r
289 MATCH_MP_TAC AFF_GE_MONO_RIGHT THEN ASM SET_TAC[];
\r
291 X_GEN_TAC `ee2:real^N->bool` THEN DISCH_TAC THEN
\r
292 SUBGOAL_THEN `(ee1:real^N->bool) HAS_SIZE 2` MP_TAC THENL
\r
293 [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
\r
294 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
\r
295 MAP_EVERY X_GEN_TAC [`v1:real^N`; `w1:real^N`] THEN
\r
296 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
\r
297 SUBGOAL_THEN `(ee2:real^N->bool) HAS_SIZE 2` MP_TAC THENL
\r
298 [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
\r
299 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
\r
300 MAP_EVERY X_GEN_TAC [`v2:real^N`; `w2:real^N`] THEN
\r
301 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
\r
302 ONCE_REWRITE_TAC[SET_RULE
\r
303 `{a,b} INTER {c,d} = {v} <=>
\r
304 v = a /\ {a,b} INTER {c,d} = {v} \/
\r
305 v = b /\ {a,b} INTER {c,d} = {v}`] THEN
\r
307 `p /\ q \/ r /\ q ==> t <=> (p ==> q ==> t) /\ (r ==> q ==> t)`] THEN
\r
308 REWRITE_TAC[FORALL_AND_THM; FORALL_UNWIND_THM2] THEN
\r
309 MAP_EVERY UNDISCH_TAC [`{v1:real^N,w1} IN E`; `~(v1:real^N = w1)`] THEN
\r
310 MAP_EVERY (fun s -> SPEC_TAC(s,s))
\r
311 [`w1:real^N`; `v1:real^N`] THEN
\r
312 REWRITE_TAC[IMP_IMP] THEN MATCH_MP_TAC(MESON[]
\r
313 `(!v w. P v w ==> P w v) /\
\r
314 (!v w. R v w ==> Q w v) /\
\r
315 (!v w. P v w ==> R v w)
\r
316 ==> (!v w. P v w ==> Q v w /\ R v w)`) THEN
\r
317 REPEAT(CONJ_TAC THENL [SIMP_TAC[INSERT_AC]; ALL_TAC]) THEN
\r
318 MAP_EVERY X_GEN_TAC [`u:real^N`; `v:real^N`] THEN STRIP_TAC THEN
\r
319 ONCE_REWRITE_TAC[SET_RULE
\r
320 `{a,b} INTER {c,d} = {v} <=>
\r
321 v = c /\ {a,b} INTER {c,d} = {v} \/
\r
322 v = d /\ {a,b} INTER {c,d} = {v}`] THEN
\r
324 `p /\ q \/ r /\ q ==> t <=> (p ==> q ==> t) /\ (r ==> q ==> t)`] THEN
\r
325 MAP_EVERY UNDISCH_TAC [`{v2:real^N,w2} IN E`; `~(v2:real^N = w2)`] THEN
\r
326 MAP_EVERY (fun s -> SPEC_TAC(s,s)) [`w2:real^N`; `v2:real^N`] THEN
\r
327 REWRITE_TAC[IMP_IMP] THEN MATCH_MP_TAC(MESON[]
\r
328 `(!v w. P v w ==> P w v) /\
\r
329 (!v w. Q v w ==> R w v) /\
\r
330 (!v w. P v w ==> Q v w)
\r
331 ==> (!v w. P v w ==> Q v w /\ R v w)`) THEN
\r
332 REPEAT(CONJ_TAC THENL [SIMP_TAC[INSERT_AC]; ALL_TAC]) THEN
\r
333 MAP_EVERY X_GEN_TAC [`v':real^N`; `w:real^N`] THEN STRIP_TAC THEN
\r
334 ONCE_REWRITE_TAC[IMP_CONJ] THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
\r
335 ASM_CASES_TAC `u:real^N = w` THENL [ASM SET_TAC[]; ALL_TAC] THEN
\r
336 DISCH_TAC THEN W(MP_TAC o PART_MATCH (rand o lhand o rand) lemma o goal_concl) THEN
\r
338 [REWRITE_TAC[SET_RULE `{x,v,w} = {x} UNION {v,w}`] THEN
\r
339 ASM_MESON_TAC[fan6; INSERT_AC];
\r
341 MATCH_MP_TAC(TAUT `~q ==> (~p <=> q) ==> p`) THEN
\r
342 REWRITE_TAC[DE_MORGAN_THM] THEN CONJ_TAC THEN MATCH_MP_TAC(SET_RULE
\r
343 `aff_ge {x} {v} INTER aff_ge {x} s = {x} /\
\r
344 v IN aff_ge {x} {v} /\ ~(v = x)
\r
345 ==> ~(v IN aff_ge {x} s)`) THEN
\r
346 REPEAT CONJ_TAC THENL
\r
347 [FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
348 ASM_REWRITE_TAC[IN_UNION] THEN
\r
349 CONJ_TAC THENL [DISJ2_TAC; ASM SET_TAC[]] THEN
\r
350 REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `u:real^N` THEN
\r
351 REWRITE_TAC[] THEN RULE_ASSUM_TAC(REWRITE_RULE[SUBSET]) THEN
\r
352 FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
353 REWRITE_TAC[IN_UNIONS] THEN EXISTS_TAC `{u:real^N,v}` THEN
\r
355 SUBGOAL_THEN `DISJOINT {x:real^N} {u:real^N}` ASSUME_TAC THENL
\r
356 [REWRITE_TAC[SET_RULE `DISJOINT {a} {b} <=> ~(a = b)`] THEN
\r
357 ASM_MESON_TAC[IN_INSERT];
\r
358 ASM_SIMP_TAC[Fan.AFF_GE_1_1; IN_ELIM_THM] THEN
\r
359 MAP_EVERY EXISTS_TAC [`&0`; `&1`] THEN
\r
360 REPEAT(CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC]) THEN VECTOR_ARITH_TAC];
\r
361 ASM_MESON_TAC[IN_INSERT];
\r
362 FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
363 ASM_REWRITE_TAC[IN_UNION] THEN
\r
364 CONJ_TAC THENL [DISJ2_TAC; ASM SET_TAC[]] THEN
\r
365 REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `w:real^N` THEN
\r
366 REWRITE_TAC[] THEN RULE_ASSUM_TAC(REWRITE_RULE[SUBSET]) THEN
\r
367 FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
368 REWRITE_TAC[IN_UNIONS] THEN EXISTS_TAC `{v:real^N,w}` THEN
\r
370 SUBGOAL_THEN `DISJOINT {x:real^N} {w:real^N}` ASSUME_TAC THENL
\r
371 [REWRITE_TAC[SET_RULE `DISJOINT {a} {b} <=> ~(a = b)`] THEN
\r
372 ASM_MESON_TAC[IN_INSERT];
\r
373 ASM_SIMP_TAC[Fan.AFF_GE_1_1; IN_ELIM_THM] THEN
\r
374 MAP_EVERY EXISTS_TAC [`&0`; `&1`] THEN
\r
375 REPEAT(CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC]) THEN VECTOR_ARITH_TAC];
\r
376 ASM_MESON_TAC[IN_INSERT]]);;
\r
378 (* ------------------------------------------------------------------------- *)
\r
379 (* Two major lemmas in the proof. *)
\r
380 (* ------------------------------------------------------------------------- *)
\r
382 let lemma_1 = prove
\r
384 ~(x = vec 0) /\ &0 < e
\r
386 !x'. dist(x,x') < d
\r
387 ==> !z'. z' IN aff_ge {vec 0} {x'}
\r
388 ==> ?z. z IN aff_ge {vec 0} {x} /\
\r
389 norm(z' - z) <= e * norm(z)`,
\r
390 REPEAT STRIP_TAC THEN
\r
391 EXISTS_TAC `min (e * norm(x:real^N)) (norm x)` THEN
\r
392 ASM_SIMP_TAC[REAL_LT_MUL; REAL_LT_MIN; NORM_POS_LT] THEN
\r
393 X_GEN_TAC `x':real^N` THEN
\r
394 STRIP_TAC THEN FIRST_X_ASSUM(ASSUME_TAC o MATCH_MP
\r
395 (NORM_ARITH `dist(x,x') < norm(x:real^N) ==> ~(x' = vec 0)`)) THEN
\r
396 ASM_SIMP_TAC[AFF_GE_1_1_0; FORALL_IN_GSPEC; EXISTS_IN_GSPEC] THEN
\r
397 X_GEN_TAC `a:real` THEN DISCH_TAC THEN EXISTS_TAC `a:real` THEN
\r
398 ASM_REWRITE_TAC[GSYM VECTOR_SUB_LDISTRIB; NORM_MUL] THEN
\r
399 ONCE_REWRITE_TAC[REAL_ARITH `a * b * c:real = b * a * c`] THEN
\r
400 MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
\r
401 ASM_SIMP_TAC[ONCE_REWRITE_RULE[DIST_SYM] (GSYM dist); REAL_LT_IMP_LE]);;
\r
403 let lemma_2 = prove
\r
405 ~collinear{vec 0,x,y} /\ &0 < e
\r
407 !x' y'. dist(x,x') < d /\ dist(y,y') < d
\r
408 ==> !z'. z' IN aff_ge {vec 0} {x',y'}
\r
409 ==> ?z. z IN aff_ge {vec 0} {x,y} /\
\r
410 norm(z' - z) <= e * norm(z)`,
\r
411 REPEAT GEN_TAC THEN ASM_CASES_TAC `x:real^N = vec 0` THENL
\r
412 [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC] THEN
\r
413 ASM_CASES_TAC `y:real^N = vec 0` THENL
\r
414 [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC] THEN
\r
415 ASM_CASES_TAC `x:real^N = y` THENL
\r
416 [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC] THEN
\r
417 REPEAT STRIP_TAC THEN
\r
418 MP_TAC(ISPEC `(\a. a$1 % x + a$2 % y):real^2->real^N`
\r
419 LINEAR_INJECTIVE_BOUNDED_BELOW_POS) THEN
\r
420 SIMP_TAC[IMP_CONJ; LINEAR_INJECTIVE_0] THEN ANTS_TAC THENL
\r
421 [REWRITE_TAC[linear; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
\r
423 REWRITE_TAC[FORALL_VECTOR_2; VECTOR_2]] THEN
\r
425 [MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN
\r
426 GEN_REWRITE_TAC RAND_CONV [CART_EQ] THEN
\r
427 REWRITE_TAC[FORALL_2; VECTOR_2; VEC_COMPONENT; DIMINDEX_2] THEN
\r
428 ASM_CASES_TAC `a = &0` THEN
\r
429 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID; VECTOR_MUL_EQ_0] THEN
\r
430 ASM_CASES_TAC `b = &0` THEN
\r
431 ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_RID; VECTOR_MUL_EQ_0] THEN
\r
432 DISCH_THEN(MP_TAC o MATCH_MP (VECTOR_ARITH
\r
433 `a + b:real^N = vec 0 ==> b = --a`)) THEN
\r
434 DISCH_THEN(MP_TAC o AP_TERM `(%) (inv b) :real^N->real^N`) THEN
\r
435 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; VECTOR_MUL_LID; REAL_MUL_LINV] THEN
\r
437 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV
\r
438 [COLLINEAR_LEMMA]) THEN
\r
439 ASM_REWRITE_TAC[VECTOR_MUL_RNEG; VECTOR_MUL_ASSOC] THEN
\r
440 REWRITE_TAC[GSYM VECTOR_MUL_LNEG] THEN MESON_TAC[];
\r
441 DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC)] THEN
\r
442 EXISTS_TAC `min (e * B / &2) (min (norm(x:real^N)) (norm(y:real^N)))` THEN
\r
443 ASM_SIMP_TAC[REAL_LT_MUL; REAL_HALF; REAL_LT_MIN; NORM_POS_LT] THEN
\r
444 MAP_EVERY X_GEN_TAC [`x':real^N`; `y':real^N`] THEN
\r
445 REPEAT(STRIP_TAC THEN FIRST_X_ASSUM(ASSUME_TAC o MATCH_MP
\r
446 (NORM_ARITH `dist(x,x') < norm(x:real^N) ==> ~(x' = vec 0)`))) THEN
\r
447 ASM_SIMP_TAC[AFF_GE_1_2_0; FORALL_IN_GSPEC; EXISTS_IN_GSPEC] THEN
\r
448 MAP_EVERY X_GEN_TAC [`a:real`; `b:real`] THEN STRIP_TAC THEN
\r
449 MAP_EVERY EXISTS_TAC [`a:real`; `b:real`] THEN ASM_REWRITE_TAC[] THEN
\r
450 MATCH_MP_TAC(NORM_ARITH
\r
451 `norm(x' - x:real^N) <= e / &2 /\ norm(y' - y) <= e / &2
\r
452 ==> norm((x' + y') - (x + y)) <= e`) THEN
\r
453 REWRITE_TAC[GSYM VECTOR_SUB_LDISTRIB; NORM_MUL] THEN CONJ_TAC THEN
\r
454 MATCH_MP_TAC REAL_LE_TRANS THENL
\r
455 [EXISTS_TAC `abs a * e * B / &2`; EXISTS_TAC `abs b * e * B / &2`] THEN
\r
456 ASM_SIMP_TAC[REAL_LE_LMUL; REAL_LT_IMP_LE; REAL_ABS_POS;
\r
457 ONCE_REWRITE_RULE[DIST_SYM] (GSYM dist);
\r
458 REAL_ARITH `a * x / &2 <= y / &2 <=> a * x <= y`] THEN
\r
459 REWRITE_TAC[REAL_ARITH `a * e * B / &2 <= (e * n) / &2 <=>
\r
460 e * a * B <= e * n`] THEN
\r
461 ASM_SIMP_TAC[REAL_LE_LMUL_EQ] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
\r
462 EXISTS_TAC `norm(vector[a;b]:real^2) * B` THEN
\r
463 ASM_SIMP_TAC[REAL_LE_RMUL_EQ] THENL
\r
464 [MP_TAC(ISPECL [`vector[a;b]:real^2`; `1`] COMPONENT_LE_NORM);
\r
465 MP_TAC(ISPECL [`vector[a;b]:real^2`; `2`] COMPONENT_LE_NORM)] THEN
\r
466 REWRITE_TAC[VECTOR_2; DIMINDEX_2; ARITH]);;
\r
468 (* ------------------------------------------------------------------------- *)
\r
469 (* Convenient lemmas for choosing minima. *)
\r
470 (* ------------------------------------------------------------------------- *)
\r
472 let MINIMIZE_OVER_MEMBERS = prove
\r
476 ==> ?e. &0 < e /\ !t. abs(t) < e ==> P x t)
\r
477 ==> ?e. &0 < e /\ !t. abs t < e ==> !x. x IN s ==> P x t`,
\r
478 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
\r
479 ASM_CASES_TAC `s:A->bool = {}` THENL
\r
480 [ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN MESON_TAC[REAL_LT_01]; ALL_TAC] THEN
\r
481 GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV) [RIGHT_IMP_EXISTS_THM] THEN
\r
482 REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN
\r
483 X_GEN_TAC `dd:A->real` THEN DISCH_TAC THEN
\r
484 EXISTS_TAC `inf(IMAGE (dd:A->real) s)` THEN
\r
485 ASM_SIMP_TAC[REAL_LT_INF_FINITE; FINITE_IMAGE; IMAGE_EQ_EMPTY] THEN
\r
486 ASM_SIMP_TAC[FORALL_IN_IMAGE]);;
\r
488 let MINIMIZE_OVER_2 = prove
\r
489 (`!P Q. (?e. &0 < e /\ !t. abs(t) < e ==> P t) /\
\r
490 (?e. &0 < e /\ !t. abs(t) < e ==> Q t)
\r
491 ==> ?e. &0 < e /\ !t. abs(t) < e ==> P t /\ Q t`,
\r
492 REPEAT GEN_TAC THEN DISCH_THEN
\r
493 (CONJUNCTS_THEN2 (X_CHOOSE_TAC `d:real`) (X_CHOOSE_TAC `e:real`)) THEN
\r
494 EXISTS_TAC `min d e:real` THEN
\r
495 ASM_SIMP_TAC[REAL_MIN_LT; REAL_LT_MIN]);;
\r
497 let MINIMIZE_OVER_STRONGER = prove
\r
498 (`!P Q. (!t. P t ==> Q t) /\ (?e. &0 < e /\ !t. abs(t) < e ==> P t)
\r
499 ==> ?e. &0 < e /\ !t. abs(t) < e ==> Q t`,
\r
502 (* ------------------------------------------------------------------------- *)
\r
503 (* The main theorem. *)
\r
504 (* ------------------------------------------------------------------------- *)
\r
506 let deformation = new_definition
\r
507 `deformation ff V (a,b) <=> (&0) IN real_interval (a,b) /\
\r
508 (!v r. v IN V /\ r IN real_interval (a,b) ==> (ff v) continuous atreal r) /\
\r
509 (!v. v IN V ==> ff v (&0) = v )`;;
\r
511 let FAN7_SMALL_DEFORMATION = prove
\r
512 (`!V:real^N->bool E a b phii.
\r
513 deformation phii V (a,b) /\ FAN (vec 0,V,E)
\r
515 !t. --e < t /\ t < e
\r
518 IMAGE (\v. phii v t) V,
\r
519 IMAGE (IMAGE (\v. phii v t)) E)`,
\r
521 (`closed {z | collinear {vec 0:real^N,fstcart z,sndcart z}}`,
\r
522 REWRITE_TAC[GSYM NORM_CAUCHY_SCHWARZ_EQUAL] THEN
\r
523 ONCE_REWRITE_TAC[SET_RULE `{x | P x} = {x | x IN (:real^N) /\ P x}`] THEN
\r
524 ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN
\r
525 REWRITE_TAC[GSYM LIFT_EQ; LIFT_NUM] THEN
\r
526 MATCH_MP_TAC CONTINUOUS_CLOSED_PREIMAGE_CONSTANT THEN
\r
527 REWRITE_TAC[CLOSED_UNIV; LIFT_SUB] THEN MATCH_MP_TAC CONTINUOUS_ON_SUB THEN
\r
529 [REWRITE_TAC[GSYM NORM_LIFT] THEN
\r
530 MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE THEN
\r
531 MATCH_MP_TAC CONTINUOUS_ON_LIFT_DOT2;
\r
532 REWRITE_TAC[LIFT_CMUL] THEN MATCH_MP_TAC CONTINUOUS_ON_MUL THEN
\r
533 REWRITE_TAC[o_DEF] THEN CONJ_TAC THEN
\r
534 MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE] THEN
\r
535 SIMP_TAC[LINEAR_CONTINUOUS_ON; LINEAR_FSTCART; LINEAR_SNDCART]) in
\r
536 REWRITE_TAC[deformation; FAN] THEN REPEAT STRIP_TAC THEN
\r
537 SUBGOAL_THEN `FINITE(V:real^N->bool) /\ ~(V = {})` STRIP_ASSUME_TAC THENL
\r
538 [ASM_MESON_TAC[fan1; SUBSET_EMPTY]; ALL_TAC] THEN
\r
539 SUBGOAL_THEN `!e. e IN E ==> ~((vec 0:real^N) IN e)` ASSUME_TAC THENL
\r
540 [RULE_ASSUM_TAC(REWRITE_RULE[fan2]) THEN ASM SET_TAC[]; ALL_TAC] THEN
\r
541 SUBGOAL_THEN `FINITE(E:(real^N->bool)->bool)` ASSUME_TAC THENL
\r
542 [MATCH_MP_TAC FINITE_SUBSET THEN
\r
543 EXISTS_TAC `IMAGE (\(v:real^N,w). {v,w}) (V CROSS V)` THEN
\r
544 ASM_SIMP_TAC[FINITE_IMAGE; FINITE_CROSS] THEN
\r
545 REWRITE_TAC[SUBSET] THEN X_GEN_TAC `ee:real^N->bool` THEN DISCH_TAC THEN
\r
546 SUBGOAL_THEN `(ee:real^N->bool) HAS_SIZE 2` MP_TAC THENL
\r
547 [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
\r
548 REWRITE_TAC[IN_IMAGE; EXISTS_PAIR_THM; IN_CROSS] THEN
\r
549 REPEAT(MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC) THEN ASM SET_TAC[];
\r
551 UNDISCH_TAC `fan7(vec 0:real^N,V,E)` THEN
\r
552 ASM_SIMP_TAC[GMLWKPK_SIMPLE] THEN DISCH_THEN(LABEL_TAC "0") THEN
\r
556 !v:real^N t. v IN V /\ abs(t) < d ==> norm(phii v t - v) < e`
\r
558 [X_GEN_TAC `e:real` THEN DISCH_TAC THEN ONCE_REWRITE_TAC[MESON[]
\r
559 `(!v t. P v /\ Q t ==> R v t) <=> (!t. Q t ==> !v. P v ==> R v t)`] THEN
\r
560 MATCH_MP_TAC MINIMIZE_OVER_MEMBERS THEN ASM_REWRITE_TAC[] THEN
\r
561 X_GEN_TAC `v:real^N` THEN DISCH_TAC THEN
\r
562 FIRST_X_ASSUM(MP_TAC o ISPECL [`v:real^N`; `&0:real`]) THEN
\r
563 REWRITE_TAC[continuous_atreal] THEN ASM_SIMP_TAC[] THEN
\r
564 REWRITE_TAC[dist; REAL_SUB_RZERO] THEN ASM_MESON_TAC[];
\r
565 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [RIGHT_IMP_EXISTS_THM] THEN
\r
566 REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM] THEN
\r
567 REWRITE_TAC[TAUT `p ==> q /\ r <=> (p ==> q) /\ (p ==> r)`] THEN
\r
568 REWRITE_TAC[FORALL_AND_THM; RIGHT_IMP_FORALL_THM; IMP_IMP] THEN
\r
569 X_GEN_TAC `dd:real->real` THEN STRIP_TAC] THEN
\r
573 ==> graph (IMAGE (IMAGE (\v. (phii:real^N->real->real^N) v t)) E)`
\r
574 STRIP_ASSUME_TAC THENL
\r
575 [ASM_REWRITE_TAC[Fan.GRAPH; FORALL_IN_IMAGE] THEN
\r
576 MATCH_MP_TAC MINIMIZE_OVER_MEMBERS THEN ASM_REWRITE_TAC[] THEN
\r
577 X_GEN_TAC `ee:real^N->bool` THEN DISCH_TAC THEN
\r
578 SUBGOAL_THEN `(ee:real^N->bool) HAS_SIZE 2` MP_TAC THENL
\r
579 [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
\r
580 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
\r
581 MAP_EVERY X_GEN_TAC [`v:real^N`; `w:real^N`] THEN STRIP_TAC THEN
\r
582 SUBGOAL_THEN `(v:real^N) IN V /\ w IN V` STRIP_ASSUME_TAC THENL
\r
583 [ASM SET_TAC[]; ALL_TAC] THEN
\r
584 ASM_REWRITE_TAC[IMAGE_CLAUSES] THEN
\r
585 EXISTS_TAC `dd(norm(v - w:real^N) / &2):real` THEN
\r
586 ASM_SIMP_TAC[REAL_HALF; VECTOR_SUB_EQ; NORM_POS_LT] THEN
\r
587 REWRITE_TAC[Local_lemmas1.SET2_HAS_SIZE2] THEN
\r
588 GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC(NORM_ARITH
\r
589 `norm(phii v t - v) < norm(v - w) / &2 /\
\r
590 norm(phii w t - w) < norm(v - w) / &2
\r
591 ==> ~(phii v t = phii w t)`) THEN
\r
592 ASM_SIMP_TAC[REAL_HALF; VECTOR_SUB_EQ; NORM_POS_LT];
\r
597 ==> !e. e IN IMAGE (IMAGE (\v. (phii:real^N->real->real^N) v t)) E
\r
598 ==> ~((vec 0) IN e)`
\r
599 STRIP_ASSUME_TAC THENL
\r
600 [REWRITE_TAC[FORALL_IN_IMAGE] THEN MATCH_MP_TAC MINIMIZE_OVER_MEMBERS THEN
\r
601 ASM_REWRITE_TAC[] THEN X_GEN_TAC `ee:real^N->bool` THEN DISCH_TAC THEN
\r
602 SUBGOAL_THEN `(ee:real^N->bool) HAS_SIZE 2` MP_TAC THENL
\r
603 [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
\r
604 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
\r
605 MAP_EVERY X_GEN_TAC [`v:real^N`; `w:real^N`] THEN STRIP_TAC THEN
\r
606 SUBGOAL_THEN `(v:real^N) IN V /\ w IN V` STRIP_ASSUME_TAC THENL
\r
607 [ASM SET_TAC[]; ALL_TAC] THEN
\r
608 SUBGOAL_THEN `~(v:real^N = vec 0) /\ ~(w:real^N = vec 0)`
\r
609 STRIP_ASSUME_TAC THENL [ASM_MESON_TAC[fan2]; ALL_TAC] THEN
\r
610 EXISTS_TAC `dd(min (norm(v:real^N)) (norm(w:real^N))):real` THEN
\r
611 ASM_SIMP_TAC[REAL_HALF; VECTOR_SUB_EQ; NORM_POS_LT; REAL_LT_MIN] THEN
\r
612 REWRITE_TAC[IMAGE_CLAUSES; IN_INSERT; DE_MORGAN_THM; NOT_IN_EMPTY] THEN
\r
613 GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC(NORM_ARITH
\r
614 `norm(phii v t - v) < min (norm v) (norm w) /\
\r
615 norm(phii w t - w) < min (norm v) (norm w)
\r
616 ==> ~(vec 0 = phii v t) /\ ~(vec 0 = phii w t)`) THEN
\r
617 ASM_SIMP_TAC[REAL_HALF; VECTOR_SUB_EQ; NORM_POS_LT; REAL_LT_MIN];
\r
624 IMAGE (IMAGE (\v. (phii:real^N->real->real^N) v t)) E UNION
\r
625 {{v} | v IN IMAGE (\v. phii v t) V} /\
\r
627 IMAGE (IMAGE (\v. phii v t)) E UNION
\r
628 {{v} | v IN IMAGE (\v. phii v t) V} /\
\r
630 ==> aff_ge {vec 0} e1 INTER aff_ge {vec 0} e2 = {vec 0}`
\r
631 STRIP_ASSUME_TAC THENL
\r
632 [REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
\r
633 REWRITE_TAC[SET_RULE
\r
634 `x IN s UNION t ==> P x <=> (x IN s ==> P x) /\ (x IN t ==> P x)`] THEN
\r
635 REWRITE_TAC[FORALL_AND_THM; FORALL_IN_IMAGE; FORALL_IN_GSPEC] THEN
\r
636 MATCH_MP_TAC MINIMIZE_OVER_2 THEN
\r
637 CONJ_TAC THEN MATCH_MP_TAC MINIMIZE_OVER_MEMBERS THEN
\r
638 ASM_REWRITE_TAC[] THENL
\r
639 [X_GEN_TAC `ee1:real^N->bool`; X_GEN_TAC `v1:real^N`] THEN
\r
640 (DISCH_TAC THEN MATCH_MP_TAC MINIMIZE_OVER_2 THEN CONJ_TAC THEN
\r
641 MATCH_MP_TAC MINIMIZE_OVER_MEMBERS THEN ASM_REWRITE_TAC[] THENL
\r
642 [X_GEN_TAC `ee2:real^N->bool`; X_GEN_TAC `v2:real^N`]) THEN
\r
644 [SUBGOAL_THEN `(ee1:real^N->bool) HAS_SIZE 2` MP_TAC THENL
\r
645 [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
\r
646 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
\r
647 MAP_EVERY X_GEN_TAC [`v1:real^N`; `w1:real^N`] THEN
\r
648 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
\r
649 SUBGOAL_THEN `(ee2:real^N->bool) HAS_SIZE 2` MP_TAC THENL
\r
650 [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
\r
651 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
\r
652 MAP_EVERY X_GEN_TAC [`v2:real^N`; `w2:real^N`] THEN
\r
653 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
\r
654 ASM_CASES_TAC `{v1:real^N,w1} INTER {v2,w2} = {}` THENL
\r
656 EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_LT_01] THEN ASM SET_TAC[]] THEN
\r
657 SUBGOAL_THEN `~collinear{vec 0:real^N,v1,w1} /\
\r
658 ~collinear{vec 0:real^N,v2,w2}`
\r
660 [ASM_MESON_TAC[fan6; SET_RULE `{a} UNION {b,c} = {a,b,c}`];
\r
662 MAP_EVERY (fun t -> ASM_CASES_TAC t THENL
\r
663 [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC])
\r
664 [`v1:real^N = vec 0`; `w1:real^N = vec 0`;
\r
665 `v2:real^N = vec 0`; `w2:real^N = vec 0`] THEN
\r
668 [`aff_ge {vec 0:real^N} {v1,w1}`;
\r
669 `aff_ge {vec 0:real^N} {v2,w2}`] SEPARATE_CLOSED_CONES) THEN
\r
671 [SIMP_TAC[CLOSED_AFF_GE; FINITE_INSERT; FINITE_EMPTY] THEN
\r
672 ASM_SIMP_TAC[IN_UNION; SUBSET_REFL] THEN
\r
673 CONJ_TAC THEN MATCH_MP_TAC CONIC_AFF_GE_0 THEN
\r
674 REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY] THEN ASM SET_TAC[];
\r
676 SUBGOAL_THEN `(v1:real^N) IN V /\ v2 IN V /\ w1 IN V /\ w2 IN V`
\r
677 STRIP_ASSUME_TAC THENL
\r
678 [REPEAT CONJ_TAC THEN
\r
679 FIRST_X_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [SUBSET]) THEN
\r
680 REWRITE_TAC[IN_UNIONS] THEN ASM_MESON_TAC[IN_INSERT];
\r
682 DISCH_THEN(X_CHOOSE_THEN `d:real`
\r
683 (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "*"))) THEN
\r
684 MP_TAC(ISPECL [`v1:real^N`; `w1:real^N`; `d / &3`] lemma_2) THEN
\r
685 ASM_REWRITE_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`] THEN
\r
686 DISCH_THEN(X_CHOOSE_THEN `d1:real`
\r
687 (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "1"))) THEN
\r
688 MP_TAC(ISPECL [`v2:real^N`; `w2:real^N`; `d / &3`] lemma_2) THEN
\r
689 ASM_REWRITE_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`] THEN
\r
690 DISCH_THEN(X_CHOOSE_THEN `d2:real`
\r
691 (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "2"))) THEN
\r
692 EXISTS_TAC `(dd:real->real) ((min d1 d2) / &3)` THEN
\r
693 ASM_SIMP_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`; REAL_LT_MIN] THEN
\r
694 X_GEN_TAC `t:real` THEN DISCH_TAC THEN DISCH_THEN(K ALL_TAC) THEN
\r
695 REWRITE_TAC[IMAGE_CLAUSES] THEN MATCH_MP_TAC(SET_RULE
\r
696 `(v IN s /\ v IN t /\ !x. x IN s INTER t ==> x = v)
\r
697 ==> s INTER t = {v}`) THEN
\r
698 REWRITE_TAC[Ckqowsa_4_points.points_in_aff_ge_0_2; IN_INTER] THEN
\r
699 X_GEN_TAC `x:real^N` THEN STRIP_TAC THEN
\r
700 REMOVE_THEN "1" (MP_TAC o SPECL
\r
701 [`(phii:real^N->real->real^N) v1 t`;
\r
702 `(phii:real^N->real->real^N) w1 t`]) THEN
\r
704 [CONJ_TAC THEN MATCH_MP_TAC REAL_LT_TRANS THEN
\r
705 EXISTS_TAC `min d1 d2 / &3` THEN
\r
706 (CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC]) THEN
\r
707 REWRITE_TAC[ONCE_REWRITE_RULE[NORM_SUB] dist] THEN
\r
708 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
\r
709 ASM_REAL_ARITH_TAC;
\r
710 DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
\r
711 DISCH_THEN(X_CHOOSE_THEN `x1:real^N` STRIP_ASSUME_TAC)] THEN
\r
712 REMOVE_THEN "2" (MP_TAC o SPECL
\r
713 [`(phii:real^N->real->real^N) v2 t`;
\r
714 `(phii:real^N->real->real^N) w2 t`]) THEN
\r
716 [CONJ_TAC THEN MATCH_MP_TAC REAL_LT_TRANS THEN
\r
717 EXISTS_TAC `min d1 d2 / &3` THEN
\r
718 (CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC]) THEN
\r
719 REWRITE_TAC[ONCE_REWRITE_RULE[NORM_SUB] dist] THEN
\r
720 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
\r
721 ASM_REAL_ARITH_TAC;
\r
722 DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
\r
723 DISCH_THEN(X_CHOOSE_THEN `x2:real^N` STRIP_ASSUME_TAC)];
\r
725 SUBGOAL_THEN `(ee1:real^N->bool) HAS_SIZE 2` MP_TAC THENL
\r
726 [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
\r
727 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
\r
728 MAP_EVERY X_GEN_TAC [`v1:real^N`; `w1:real^N`] THEN
\r
729 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
\r
730 ASM_CASES_TAC `{v1:real^N,w1} INTER {v2} = {}` THENL
\r
732 EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_LT_01] THEN ASM SET_TAC[]] THEN
\r
733 SUBGOAL_THEN `~collinear{vec 0:real^N,v1,w1}`
\r
735 [ASM_MESON_TAC[fan6; SET_RULE `{a} UNION {b,c} = {a,b,c}`];
\r
737 MAP_EVERY (fun t -> ASM_CASES_TAC t THENL
\r
738 [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC])
\r
739 [`v1:real^N = vec 0`; `w1:real^N = vec 0`] THEN
\r
741 SUBGOAL_THEN `~(v2:real^N = vec 0)` ASSUME_TAC THENL
\r
742 [ASM_MESON_TAC[fan2]; ALL_TAC] THEN
\r
744 [`aff_ge {vec 0:real^N} {v1,w1}`;
\r
745 `aff_ge {vec 0:real^N} {v2}`] SEPARATE_CLOSED_CONES) THEN
\r
747 [SIMP_TAC[CLOSED_AFF_GE; FINITE_INSERT; FINITE_EMPTY] THEN
\r
748 REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
\r
749 [CONJ_TAC THEN MATCH_MP_TAC CONIC_AFF_GE_0 THEN
\r
750 REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY] THEN ASM SET_TAC[];
\r
751 MATCH_MP_TAC(SET_RULE `s = t ==> s SUBSET t`) THEN
\r
752 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM SET_TAC[]];
\r
754 SUBGOAL_THEN `(v1:real^N) IN V /\ w1 IN V`
\r
755 STRIP_ASSUME_TAC THENL
\r
756 [REPEAT CONJ_TAC THEN
\r
757 FIRST_X_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [SUBSET]) THEN
\r
758 REWRITE_TAC[IN_UNIONS] THEN ASM_MESON_TAC[IN_INSERT];
\r
760 DISCH_THEN(X_CHOOSE_THEN `d:real`
\r
761 (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "*"))) THEN
\r
762 MP_TAC(ISPECL [`v1:real^N`; `w1:real^N`; `d / &3`] lemma_2) THEN
\r
763 ASM_REWRITE_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`] THEN
\r
764 DISCH_THEN(X_CHOOSE_THEN `d1:real`
\r
765 (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "1"))) THEN
\r
766 MP_TAC(ISPECL [`v2:real^N`; `d / &3`] lemma_1) THEN
\r
767 ASM_REWRITE_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`] THEN
\r
768 DISCH_THEN(X_CHOOSE_THEN `d2:real`
\r
769 (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "2"))) THEN
\r
770 EXISTS_TAC `(dd:real->real) ((min d1 d2) / &3)` THEN
\r
771 ASM_SIMP_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`; REAL_LT_MIN] THEN
\r
772 X_GEN_TAC `t:real` THEN DISCH_TAC THEN DISCH_THEN(K ALL_TAC) THEN
\r
773 REWRITE_TAC[IMAGE_CLAUSES] THEN MATCH_MP_TAC(SET_RULE
\r
774 `(v IN s /\ v IN t /\ !x. x IN s INTER t ==> x = v)
\r
775 ==> s INTER t = {v}`) THEN
\r
776 REWRITE_TAC[Ckqowsa_4_points.points_in_aff_ge_0_2; IN_INTER] THEN
\r
778 [MESON_TAC[Ckqowsa_4_points.points_in_aff_ge_0_2; INSERT_AC];
\r
780 X_GEN_TAC `x:real^N` THEN STRIP_TAC THEN
\r
781 REMOVE_THEN "1" (MP_TAC o SPECL
\r
782 [`(phii:real^N->real->real^N) v1 t`;
\r
783 `(phii:real^N->real->real^N) w1 t`]) THEN
\r
785 [CONJ_TAC THEN MATCH_MP_TAC REAL_LT_TRANS THEN
\r
786 EXISTS_TAC `min d1 d2 / &3` THEN
\r
787 (CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC]) THEN
\r
788 REWRITE_TAC[ONCE_REWRITE_RULE[NORM_SUB] dist] THEN
\r
789 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
\r
790 ASM_REAL_ARITH_TAC;
\r
791 DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
\r
792 DISCH_THEN(X_CHOOSE_THEN `x1:real^N` STRIP_ASSUME_TAC)] THEN
\r
793 REMOVE_THEN "2" (MP_TAC o SPEC `(phii:real^N->real->real^N) v2 t`) THEN
\r
795 [MATCH_MP_TAC REAL_LT_TRANS THEN
\r
796 EXISTS_TAC `min d1 d2 / &3` THEN
\r
797 (CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC]) THEN
\r
798 REWRITE_TAC[ONCE_REWRITE_RULE[NORM_SUB] dist] THEN
\r
799 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
\r
800 ASM_REAL_ARITH_TAC;
\r
801 DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
\r
802 DISCH_THEN(X_CHOOSE_THEN `x2:real^N` STRIP_ASSUME_TAC)];
\r
804 SUBGOAL_THEN `(ee2:real^N->bool) HAS_SIZE 2` MP_TAC THENL
\r
805 [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
\r
806 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
\r
807 MAP_EVERY X_GEN_TAC [`v2:real^N`; `w2:real^N`] THEN
\r
808 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
\r
809 ASM_CASES_TAC `{v1} INTER {v2:real^N,w2} = {}` THENL
\r
811 EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_LT_01] THEN ASM SET_TAC[]] THEN
\r
812 SUBGOAL_THEN `~collinear{vec 0:real^N,v2,w2}`
\r
814 [ASM_MESON_TAC[fan6; SET_RULE `{a} UNION {b,c} = {a,b,c}`];
\r
816 MAP_EVERY (fun t -> ASM_CASES_TAC t THENL
\r
817 [ASM_REWRITE_TAC[INSERT_AC; COLLINEAR_2]; ALL_TAC])
\r
818 [`v2:real^N = vec 0`; `w2:real^N = vec 0`] THEN
\r
820 SUBGOAL_THEN `~(v1:real^N = vec 0)` ASSUME_TAC THENL
\r
821 [ASM_MESON_TAC[fan2]; ALL_TAC] THEN
\r
823 [`aff_ge {vec 0:real^N} {v1}`;
\r
824 `aff_ge {vec 0:real^N} {v2,w2}`] SEPARATE_CLOSED_CONES) THEN
\r
826 [SIMP_TAC[CLOSED_AFF_GE; FINITE_INSERT; FINITE_EMPTY] THEN
\r
827 REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
\r
828 [CONJ_TAC THEN MATCH_MP_TAC CONIC_AFF_GE_0 THEN
\r
829 REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY] THEN ASM SET_TAC[];
\r
830 MATCH_MP_TAC(SET_RULE `s = t ==> s SUBSET t`) THEN
\r
831 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM SET_TAC[]];
\r
833 SUBGOAL_THEN `(v2:real^N) IN V /\ w2 IN V`
\r
834 STRIP_ASSUME_TAC THENL
\r
835 [REPEAT CONJ_TAC THEN
\r
836 FIRST_X_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [SUBSET]) THEN
\r
837 REWRITE_TAC[IN_UNIONS] THEN ASM_MESON_TAC[IN_INSERT];
\r
839 DISCH_THEN(X_CHOOSE_THEN `d:real`
\r
840 (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "*"))) THEN
\r
841 MP_TAC(ISPECL [`v2:real^N`; `w2:real^N`; `d / &3`] lemma_2) THEN
\r
842 ASM_REWRITE_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`] THEN
\r
843 DISCH_THEN(X_CHOOSE_THEN `d2:real`
\r
844 (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "1"))) THEN
\r
845 MP_TAC(ISPECL [`v1:real^N`; `d / &3`] lemma_1) THEN
\r
846 ASM_REWRITE_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`] THEN
\r
847 DISCH_THEN(X_CHOOSE_THEN `d1:real`
\r
848 (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "2"))) THEN
\r
849 EXISTS_TAC `(dd:real->real) ((min d1 d2) / &3)` THEN
\r
850 ASM_SIMP_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`; REAL_LT_MIN] THEN
\r
851 X_GEN_TAC `t:real` THEN DISCH_TAC THEN DISCH_THEN(K ALL_TAC) THEN
\r
852 REWRITE_TAC[IMAGE_CLAUSES] THEN MATCH_MP_TAC(SET_RULE
\r
853 `(v IN s /\ v IN t /\ !x. x IN s INTER t ==> x = v)
\r
854 ==> s INTER t = {v}`) THEN
\r
855 REWRITE_TAC[Ckqowsa_4_points.points_in_aff_ge_0_2; IN_INTER] THEN
\r
857 [MESON_TAC[Ckqowsa_4_points.points_in_aff_ge_0_2; INSERT_AC];
\r
859 X_GEN_TAC `x:real^N` THEN STRIP_TAC THEN
\r
860 REMOVE_THEN "1" (MP_TAC o SPECL
\r
861 [`(phii:real^N->real->real^N) v2 t`;
\r
862 `(phii:real^N->real->real^N) w2 t`]) THEN
\r
864 [CONJ_TAC THEN MATCH_MP_TAC REAL_LT_TRANS THEN
\r
865 EXISTS_TAC `min d1 d2 / &3` THEN
\r
866 (CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC]) THEN
\r
867 REWRITE_TAC[ONCE_REWRITE_RULE[NORM_SUB] dist] THEN
\r
868 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
\r
869 ASM_REAL_ARITH_TAC;
\r
870 DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
\r
871 DISCH_THEN(X_CHOOSE_THEN `x1:real^N` STRIP_ASSUME_TAC)] THEN
\r
872 REMOVE_THEN "2" (MP_TAC o SPEC `(phii:real^N->real->real^N) v1 t`) THEN
\r
874 [MATCH_MP_TAC REAL_LT_TRANS THEN
\r
875 EXISTS_TAC `min d1 d2 / &3` THEN
\r
876 (CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC]) THEN
\r
877 REWRITE_TAC[ONCE_REWRITE_RULE[NORM_SUB] dist] THEN
\r
878 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
\r
879 ASM_REAL_ARITH_TAC;
\r
880 DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
\r
881 DISCH_THEN(X_CHOOSE_THEN `x2:real^N` STRIP_ASSUME_TAC)];
\r
883 ASM_CASES_TAC `{v1:real^N} INTER {v2} = {}` THENL
\r
885 EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_LT_01] THEN ASM SET_TAC[]] THEN
\r
886 SUBGOAL_THEN `~(v1:real^N = vec 0) /\ ~(v2:real^N = vec 0)`
\r
887 STRIP_ASSUME_TAC THENL
\r
888 [ASM_MESON_TAC[fan2]; ALL_TAC] THEN
\r
890 [`aff_ge {vec 0:real^N} {v1}`;
\r
891 `aff_ge {vec 0:real^N} {v2}`] SEPARATE_CLOSED_CONES) THEN
\r
893 [SIMP_TAC[CLOSED_AFF_GE; FINITE_INSERT; FINITE_EMPTY] THEN
\r
894 REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
\r
895 [CONJ_TAC THEN MATCH_MP_TAC CONIC_AFF_GE_0 THEN
\r
896 REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY] THEN ASM SET_TAC[];
\r
897 MATCH_MP_TAC(SET_RULE `s = t ==> s SUBSET t`) THEN
\r
898 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM SET_TAC[]];
\r
900 DISCH_THEN(X_CHOOSE_THEN `d:real`
\r
901 (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "*"))) THEN
\r
902 MP_TAC(ISPECL [`v1:real^N`; `d / &3`] lemma_1) THEN
\r
903 ASM_REWRITE_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`] THEN
\r
904 DISCH_THEN(X_CHOOSE_THEN `d1:real`
\r
905 (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "1"))) THEN
\r
906 MP_TAC(ISPECL [`v2:real^N`; `d / &3`] lemma_1) THEN
\r
907 ASM_REWRITE_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`] THEN
\r
908 DISCH_THEN(X_CHOOSE_THEN `d2:real`
\r
909 (CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "2"))) THEN
\r
910 EXISTS_TAC `(dd:real->real) ((min d1 d2) / &3)` THEN
\r
911 ASM_SIMP_TAC[REAL_ARITH `&0 < d / &3 <=> &0 < d`; REAL_LT_MIN] THEN
\r
912 X_GEN_TAC `t:real` THEN DISCH_TAC THEN DISCH_THEN(K ALL_TAC) THEN
\r
913 REWRITE_TAC[IMAGE_CLAUSES] THEN MATCH_MP_TAC(SET_RULE
\r
914 `(v IN s /\ v IN t /\ !x. x IN s INTER t ==> x = v)
\r
915 ==> s INTER t = {v}`) THEN
\r
916 REWRITE_TAC[Ckqowsa_4_points.points_in_aff_ge_0_2; IN_INTER] THEN
\r
917 REPEAT(CONJ_TAC THENL
\r
918 [MESON_TAC[Ckqowsa_4_points.points_in_aff_ge_0_2; INSERT_AC];
\r
920 X_GEN_TAC `x:real^N` THEN STRIP_TAC THEN
\r
921 REMOVE_THEN "1" (MP_TAC o SPEC `(phii:real^N->real->real^N) v1 t`) THEN
\r
923 [MATCH_MP_TAC REAL_LT_TRANS THEN
\r
924 EXISTS_TAC `min d1 d2 / &3` THEN
\r
925 (CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC]) THEN
\r
926 REWRITE_TAC[ONCE_REWRITE_RULE[NORM_SUB] dist] THEN
\r
927 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
\r
928 ASM_REAL_ARITH_TAC;
\r
929 DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
\r
930 DISCH_THEN(X_CHOOSE_THEN `x1:real^N` STRIP_ASSUME_TAC)] THEN
\r
931 REMOVE_THEN "2" (MP_TAC o SPEC `(phii:real^N->real->real^N) v2 t`) THEN
\r
933 [MATCH_MP_TAC REAL_LT_TRANS THEN
\r
934 EXISTS_TAC `min d1 d2 / &3` THEN
\r
935 (CONJ_TAC THENL [ALL_TAC; ASM_REAL_ARITH_TAC]) THEN
\r
936 REWRITE_TAC[ONCE_REWRITE_RULE[NORM_SUB] dist] THEN
\r
937 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
\r
938 ASM_REAL_ARITH_TAC;
\r
939 DISCH_THEN(MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN
\r
940 DISCH_THEN(X_CHOOSE_THEN `x2:real^N` STRIP_ASSUME_TAC)]] THEN
\r
943 `d * max (norm(x1:real^N)) (norm(x2:real^N))
\r
944 <= d * (norm x1 + norm x2) / &3`
\r
946 [MATCH_MP_TAC(NORM_ARITH
\r
947 `norm(x - x1) <= d / &3 * norm x1 /\
\r
948 norm(x - x2) <= d / &3 * norm x2 /\
\r
950 ==> a <= d * (norm x1 + norm x2) / &3`) THEN
\r
951 ASM_SIMP_TAC[] THEN ASM_MESON_TAC[DIST_SYM; REAL_MAX_SYM];
\r
952 ASM_SIMP_TAC[REAL_LE_LMUL_EQ] THEN
\r
953 DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
\r
954 `max x1 x2 <= (x1 + x2) / &3
\r
955 ==> &0 <= x1 /\ &0 <= x2 ==> x1 = &0 /\ x2 = &0`)) THEN
\r
956 REWRITE_TAC[NORM_POS_LE; NORM_EQ_0] THEN
\r
957 DISCH_THEN(CONJUNCTS_THEN SUBST_ALL_TAC) THEN
\r
958 RULE_ASSUM_TAC(REWRITE_RULE[NORM_0; REAL_MUL_RZERO;
\r
959 NORM_ARITH `norm(x - vec 0) <= &0 <=> x = vec 0`]) THEN
\r
960 ASM_REWRITE_TAC[]]);
\r
966 IMAGE (\v. (phii:real^N->real->real^N) v t) V,
\r
967 IMAGE (IMAGE (\v. phii v t)) E)`
\r
968 STRIP_ASSUME_TAC THENL
\r
969 [REWRITE_TAC[fan6; FORALL_IN_IMAGE] THEN
\r
970 MATCH_MP_TAC MINIMIZE_OVER_MEMBERS THEN
\r
971 ASM_REWRITE_TAC[] THEN
\r
972 X_GEN_TAC `ee:real^N->bool` THEN DISCH_TAC THEN
\r
973 SUBGOAL_THEN `(ee:real^N->bool) HAS_SIZE 2` MP_TAC THENL
\r
974 [ASM_MESON_TAC[graph; IN]; CONV_TAC(LAND_CONV HAS_SIZE_CONV)] THEN
\r
975 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
\r
976 MAP_EVERY X_GEN_TAC [`v:real^N`; `w:real^N`] THEN
\r
977 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC) THEN
\r
978 REWRITE_TAC[IMAGE_CLAUSES; SET_RULE `{a} UNION {b,c} = {a,b,c}`] THEN
\r
979 MP_TAC(ISPEC `UNIV DIFF {z | collinear{vec 0:real^N,fstcart z,sndcart z}}`
\r
981 REWRITE_TAC[lemma; GSYM closed] THEN
\r
982 DISCH_THEN(MP_TAC o SPEC `pastecart (v:real^N) (w:real^N)`) THEN
\r
983 REWRITE_TAC[IN_DIFF; IN_ELIM_THM; IN_UNIV; FSTCART_PASTECART;
\r
984 SNDCART_PASTECART] THEN
\r
986 [ASM_MESON_TAC[fan6; SET_RULE `{a} UNION {b,c} = {a,b,c}`]; ALL_TAC] THEN
\r
987 REWRITE_TAC[FORALL_PASTECART; FSTCART_PASTECART; SNDCART_PASTECART] THEN
\r
988 DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
\r
989 EXISTS_TAC `(dd:real->real) (d / &2)` THEN ASM_SIMP_TAC[REAL_HALF] THEN
\r
990 X_GEN_TAC `t:real` THEN DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
991 REWRITE_TAC[dist; PASTECART_SUB] THEN
\r
992 MATCH_MP_TAC(REAL_ARITH
\r
993 `norm x < d / &2 /\ norm y < d / &2 /\
\r
994 norm(pastecart (x:real^N) (y:real^N)) <= norm x + norm y
\r
995 ==> norm(pastecart x y) < d`) THEN
\r
996 REWRITE_TAC[NORM_PASTECART_LE] THEN
\r
997 CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
\r
998 ASM_SIMP_TAC[REAL_HALF] THEN
\r
999 FIRST_X_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [SUBSET]) THEN
\r
1000 REWRITE_TAC[IN_UNIONS] THEN ASM_MESON_TAC[IN_INSERT];
\r
1002 REWRITE_TAC[REAL_ARITH `--e < t /\ t < e <=> abs t < e`] THEN
\r
1003 EXISTS_TAC `min (e1:real) (min e2 (min e3 e4))` THEN
\r
1004 ASM_REWRITE_TAC[REAL_LT_MIN] THEN X_GEN_TAC `t:real` THEN STRIP_TAC THEN
\r
1005 W(MP_TAC o PART_MATCH (lhs o rand) GMLWKPK_SIMPLE o goal_concl) THEN
\r
1006 ASM_SIMP_TAC[] THEN ANTS_TAC THENL
\r
1007 [CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
\r
1008 REWRITE_TAC[UNIONS_SUBSET; FORALL_IN_IMAGE] THEN ASM SET_TAC[];
\r
1009 DISCH_THEN SUBST1_TAC THEN ASM_MESON_TAC[]]);;
\r
1011 let XRECQNS = prove_by_refinement(
\r
1013 deformation f V (a,b) /\ FAN (vec 0,V,E) ==>
\r
1014 (?e. &0 < e /\ (!t. --e < t /\ t < e ==>
\r
1016 IMAGE (\v. f (v:real^3) t) V,
\r
1017 IMAGE (IMAGE (\v. f v t)) E)))`,
\r
1021 REWRITE_TAC[Fan.FAN];
\r
1022 INTRO_TAC Localization.ALL_TO_THE_NONPARALLEL_PART_ALT [`a`;`b`;`V`;`E`;`f`];
\r
1023 ASM_REWRITE_TAC[];
\r
1025 INTRO_TAC FAN7_SMALL_DEFORMATION [`V`;`E`;`a`;`b`;`f`];
\r
1026 ASM_REWRITE_TAC[];
\r
1028 TYPIFY `if (e < e') then e else e'` EXISTS_TAC;
\r
1030 ASM_REWRITE_TAC[];
\r
1031 REPEAT WEAKER_STRIP_TAC;
\r
1032 BY(ASM_MESON_TAC[arith `&0 < e /\ e < e' /\ -- e < t /\ t < e ==> -- e' < t /\ t < e'`]);
\r
1033 ASM_REWRITE_TAC[];
\r
1034 REPEAT WEAKER_STRIP_TAC;
\r
1035 BY(ASM_MESON_TAC[arith `&0 < e' /\ ~(e < e') /\ -- e' < t /\ t < e' ==> -- e < t /\ t < e`])
\r
git://colo12-c703.uibk.ac.at / Flyspeck/.git / blob