1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
3 (* Section: Conclusions *)
4 (* Chapter: Local Fan *)
6 (* Author: Thomas Hales *)
8 (* ========================================================================== *)
12 module Zlzthic = struct
18 let th1 = REWRITE_RULE[MESON[]` a /\ b ==> c <=> a ==> b ==> c `] th in
19 let th2 = SPEC_ALL th1 in
22 let ASSUME_TAC2 = ASSUME_TAC o FOR_ASM;;
23 let DOWN = FIRST_X_ASSUM MP_TAC;;
24 let ATTACH thm = MATCH_MP (MESON[]` ! a b. ( a ==> b ) ==> ( a <=> a /\ b )`) thm;;
25 let NHANH tm = ONCE_REWRITE_TAC[ ATTACH (SPEC_ALL ( tm ))];;
26 let SWITCH_TAC tm = UNDISCH_TAC tm THEN DISCH_THEN (ASSUME_TAC o GSYM);;
27 let PHA = REWRITE_TAC[ MESON[] ` (a/\b)/\c <=> a/\ b /\ c `; MESON[]` a ==> b ==> c <=> a /\ b ==> c `];;
31 let NONCOLLINEAR_OPEN = Local_lemmas1.CONTINUOUS_PRESERVE_COLLINEAR;;
33 let NONPLANAR_OPEN = prove_by_refinement(
34 `!(v1:real->real^3) v2 v3 v4 t. ~coplanar {v1 t,v2 t,v3 t, v4 t} /\
35 v1 continuous atreal t /\ v2 continuous atreal t /\ v3 continuous atreal t /\
36 v4 continuous atreal t
38 (?e. &0 < e /\ !t'. abs(t - t') < e ==> ~coplanar {v1 t', v2 t' ,v3 t',v4 t'})`,
41 REWRITE_TAC[Oxlzlez.coplanar_delta_y];
42 REPEAT WEAKER_STRIP_TAC;
43 TYPIFY `(\t. delta_y (dist (v1 t,v2 t)) (dist (v1 t,v3 t)) (dist (v1 t,v4 t)) (dist (v3 t,v4 t)) (dist (v2 t,v4 t)) (dist (v2 t,v3 t))) real_continuous atreal t` ENOUGH_TO_SHOW_TAC;
44 REWRITE_TAC[real_continuous_atreal];
45 DISCH_THEN (C INTRO_TAC [`delta_y (dist (v1 t,v2 t)) (dist (v1 t,v3 t)) (dist (v1 t,v4 t)) (dist (v3 t,v4 t)) (dist (v2 t,v4 t)) (dist (v2 t,v3 t))`]);
47 REPEAT WEAKER_STRIP_TAC;
48 TYPIFY `d` EXISTS_TAC;
50 REPEAT WEAKER_STRIP_TAC;
51 FIRST_X_ASSUM (C INTRO_TAC [`t'`]);
53 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
54 REWRITE_TAC[Sphere.delta_y;Sphere.delta_x];
55 BY((REPEAT ( (MATCH_MP_TAC REAL_CONTINUOUS_ADD ORELSE MATCH_MP_TAC REAL_CONTINUOUS_SUB ORELSE MATCH_MP_TAC REAL_CONTINUOUS_MUL ORELSE MATCH_MP_TAC REAL_CONTINUOUS_NEG ORELSE MATCH_MP_TAC Local_lemmas1.CON_ATREAL_REAL_CON2_REDO) THEN (REPEAT CONJ_TAC))) THEN ASM_REWRITE_TAC[])
59 let COLL_IFF_COLL_CROSS2 = prove_by_refinement(
60 `!v w. collinear {vec 0, v, w} <=> collinear {vec 0, w, v cross w}`,
63 REPEAT WEAKER_STRIP_TAC;
64 TYPED_ABBREV_TAC `s = {vec 0,v,w}`;
65 (ONCE_REWRITE_TAC[CROSS_SKEW]);
66 ONCE_REWRITE_TAC[SET_RULE `{a,b,(c:real^3)} = {a,c,b}`];
67 (REWRITE_TAC[arith `-- (u:real^3) = (-- &1) % u`]);
68 GMATCH_SIMP_TAC COLLINEAR_SPECIAL_SCALE;
69 (ONCE_REWRITE_TAC[SET_RULE `{vec 0,a,(b:real^3)} = {vec 0,b,a}`]);
70 RULE_ASSUM_TAC( ONCE_REWRITE_RULE[SET_RULE `{a,b,(c:real^3)} = {a,c,b}`]);
71 REWRITE_TAC[arith` ~( -- &1 = &0)`];
72 BY(ASM_MESON_TAC([Local_lemmas.COLL_IFF_COLL_CROSS]))
76 let azim_cross_0 = prove_by_refinement(
77 `!v w. ~(collinear {vec 0,v,w}) ==> ~(azim (vec 0) (v cross w) v w = &0)`,
80 REPEAT WEAKER_STRIP_TAC;
81 BY(ASM_MESON_TAC[Local_lemmas1.AZIM_COND_FOR_COPLANAR;Local_lemmas.NOT_COLL_IMP_COPL;SET_RULE `{vec 0,v,w,v cross w} = {vec 0,v cross w,v,(w:real^3)}`])
85 let wedge_ge_cross = prove_by_refinement(
86 `!v w. ~collinear {vec 0,v,w} ==> wedge_ge (vec 0) (v cross w) v w = aff_ge {vec 0, v cross w} {v, w}`,
89 REPEAT WEAKER_STRIP_TAC;
90 GMATCH_SIMP_TAC Local_lemmas.WEDGE_GE_EQ_AFF_GE;
92 TYPIFY `&0 < sin(azim (vec 0) (v cross w) v w)` ENOUGH_TO_SHOW_TAC;
93 REWRITE_TAC[arith `a < pi <=> a <= pi /\ ~(a = pi)`];
96 REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_POS_PI_LT];
97 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
98 BY(ASM_MESON_TAC[SIN_PI;arith `~(&0 < &0)`]);
99 REWRITE_TAC[Local_lemmas.SIN_AZIM_MUTUAL_SROSS];
100 ONCE_REWRITE_TAC[CROSS_TRIPLE];
101 BY(ASM_REWRITE_TAC[DOT_POS_LT;CROSS_EQ_0]);
102 ONCE_REWRITE_TAC[SET_RULE `{a,b,(c:real^3)} = {a,c,b}`];
103 BY(ASM_MESON_TAC[COLL_IFF_COLL_CROSS2;Local_lemmas.COLL_IFF_COLL_CROSS])
107 let azim_lt_pi_cross = prove_by_refinement(
108 `!u1 u2 u3. (&0 < azim (vec 0) u1 u2 u3 /\ azim(vec 0) u1 u2 u3 < pi) <=> &0 < (u1 cross u2) dot u3`,
111 REPEAT WEAKER_STRIP_TAC;
112 INTRO_TAC Trigonometry.JBDNJJB [`u1`;`u2`;`u3`];
113 ONCE_REWRITE_TAC[Leaf_cell.RE_EQVL_SYM];
114 REWRITE_TAC[Trigonometry2.re_eqvl];
115 REPEAT WEAKER_STRIP_TAC;
117 ASM_CASES_TAC `&0 < sin(azim(vec 0) u1 u2 u3)`;
119 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
121 REWRITE_TAC[arith `a < pi <=> a <= pi /\ ~(a = pi)`];
122 REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_POS_PI_LT];
123 ASM_SIMP_TAC[arith `&0 < x ==> &0 <= x`];
125 DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
126 BY(ASM_MESON_TAC[SIN_PI;arith `~(&0 < &0)`]);
127 BY(ASM_MESON_TAC[Counting_spheres.AZIM_NN;SIN_0;arith `&0 < x <=> &0 <= x /\ ~(x = &0)`;arith `~(&0 < &0)`]);
128 COMMENT "other direction";
129 TYPED_ABBREV_TAC `s = sin (azim (vec 0) u1 u2 u3)`;
130 REWRITE_TAC[arith `&0 < t * s <=> ~(&0 <= t* (-- s))`];
131 GMATCH_SIMP_TAC REAL_LE_MUL;
133 BY(ASM_TAC THEN REAL_ARITH_TAC);
134 REPEAT WEAKER_STRIP_TAC;
135 FIRST_X_ASSUM_ST `~` MP_TAC;
138 BY(ASM_MESON_TAC[SIN_POS_PI])
142 let generic_alt = prove_by_refinement(
143 `!u v w. ~collinear {vec 0,v,w} /\ ~(u = vec 0) ==>
144 (aff_ge {vec 0} {v,w} INTER aff_lt {vec 0} {u} = {} <=>
145 ~coplanar {vec 0,u,v,w} \/ ((-- u) IN wedge (vec 0) (v cross w) w v))`,
148 REPEAT WEAKER_STRIP_TAC;
149 MATCH_MP_TAC (TAUT `((a ==>b) /\ (b ==> a)) ==> (a = b)`);
150 CONJ_TAC THEN STRIP_TAC;
151 MATCH_MP_TAC (TAUT `(a ==> b ) ==> (~a \/ b)`);
153 GMATCH_SIMP_TAC (GSYM Leaf_cell.WEDGE_GE_COMPLEMENT);
154 REWRITE_TAC[IN_DIFF;IN_UNIV];
155 ASM_SIMP_TAC[azim_cross_0];
156 ASM_SIMP_TAC[wedge_ge_cross];
157 COMMENT "down to three";
158 GMATCH_SIMP_TAC Marchal_cells_2_new.AFF_GE_2_2;
159 REWRITE_TAC[IN_ELIM_THM;arith `t1 % (vec 0):real^3 = vec 0`];
161 TYPIFY `DISJOINT {v, w} {vec 0} /\ ~(v cross w = v) /\ ~(v cross w = w)` ENOUGH_TO_SHOW_TAC;
162 REWRITE_TAC[DISJOINT];
165 MATCH_MP_TAC Collect_geom.COLLINEAR_DISJOINT3;
166 BY(ASM_REWRITE_TAC[]);
167 REWRITE_TAC[CROSS_EQ_SELF];
168 BY(CONJ_TAC THEN ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{vec 0,(v:real^3),vec 0} = {vec 0,v} /\ {vec 0,vec 0,(w:real^3)} = {vec 0,w}`]);
169 REPEAT WEAKER_STRIP_TAC;
170 RULE_ASSUM_TAC( REWRITE_RULE[arith `-- (u:real^3) = w <=> u = -- w`] );
171 FIRST_X_ASSUM_ST `aff_ge` MP_TAC;
172 REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER;NOT_FORALL_THM];
173 TYPIFY `-- (u:real^3)` EXISTS_TAC;
175 GMATCH_SIMP_TAC AFF_LT_1_1;
176 REWRITE_TAC[IN_ELIM_THM;DISJOINT];
178 BY(ASM_TAC THEN SET_TAC[]);
179 GEXISTL_TAC [`&2`;`-- &1`];
180 BY(REPEAT CONJ_TAC THEN TRY REAL_ARITH_TAC THEN VECTOR_ARITH_TAC);
181 RULE_ASSUM_TAC(REWRITE_RULE[GSYM Local_lemmas.CROSS_DOT_COPLANAR]);
182 RULE_ASSUM_TAC(ONCE_REWRITE_RULE[CROSS_TRIPLE]);
183 FIRST_X_ASSUM_ST `x = &0` MP_TAC;
185 REWRITE_TAC[DOT_RNEG;DOT_RADD;DOT_RMUL];
186 REWRITE_TAC[DOT_RZERO];
187 REWRITE_TAC[DOT_CROSS_SELF];
188 (REWRITE_TAC[arith `--(&0 + t2 * a + t3 * &0 + t4 * &0) = &0 <=> t2 * a = &0`]);
189 REWRITE_TAC[REAL_ENTIRE];
190 ASM_SIMP_TAC[DOT_POS_LT;CROSS_EQ_0;arith `&0 < x ==> ~(x = &0)`];
191 DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
192 REWRITE_TAC[arith `-- --(vec 0 + &0 % a + b + (c:real^3)) = b + c`];
193 GMATCH_SIMP_TAC AFF_GE_1_2;
195 ONCE_REWRITE_TAC[DISJOINT_SYM] THEN MATCH_MP_TAC Collect_geom.COLLINEAR_DISJOINT3;
196 BY(ASM_REWRITE_TAC[]);
197 REWRITE_TAC[IN_ELIM_THM];
198 GEXISTL_TAC [`t1`;`t3`;`t4`];
201 BY(ASM_TAC THEN REAL_ARITH_TAC);
202 BY(VECTOR_ARITH_TAC);
203 COMMENT "second case";
204 REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER];
205 GMATCH_SIMP_TAC AFF_GE_1_2;
207 ONCE_REWRITE_TAC[DISJOINT_SYM] THEN MATCH_MP_TAC Collect_geom.COLLINEAR_DISJOINT3;
208 BY(ASM_REWRITE_TAC[]);
209 REWRITE_TAC[IN_ELIM_THM];
210 GMATCH_SIMP_TAC Nkezbfc_local.AFF_LT_1_1;
211 ASM_REWRITE_TAC[IN_ELIM_THM];
212 REPEAT WEAKER_STRIP_TAC;
213 RULE_ASSUM_TAC(REWRITE_RULE[GSYM Local_lemmas.CROSS_DOT_COPLANAR]);
214 RULE_ASSUM_TAC(ONCE_REWRITE_RULE[CROSS_TRIPLE]);
215 TYPIFY `(v cross w) dot (t1 % vec 0 + t2 % v + t3 % w) = (v cross w) dot (t1' % vec 0 + t2' % u)` (C SUBGOAL_THEN MP_TAC);
217 REWRITE_TAC[DOT_RNEG;DOT_RADD;DOT_RMUL;DOT_RZERO;DOT_CROSS_SELF];
218 TYPIFY `~(t2' * ((v cross w) dot u) = &0)` ENOUGH_TO_SHOW_TAC;
220 ASM_REWRITE_TAC[REAL_ENTIRE];
221 BY(ASM_TAC THEN REAL_ARITH_TAC);
222 COMMENT "third and final case";
223 REWRITE_TAC[EXTENSION;NOT_IN_EMPTY;IN_INTER];
224 GMATCH_SIMP_TAC AFF_GE_1_2;
226 ONCE_REWRITE_TAC[DISJOINT_SYM] THEN MATCH_MP_TAC Collect_geom.COLLINEAR_DISJOINT3;
227 BY(ASM_REWRITE_TAC[]);
228 REWRITE_TAC[IN_ELIM_THM];
229 GMATCH_SIMP_TAC Nkezbfc_local.AFF_LT_1_1;
230 ASM_REWRITE_TAC[IN_ELIM_THM];
231 REPEAT WEAKER_STRIP_TAC;
232 TYPIFY `x IN wedge (vec 0) (v cross w) w v` (C SUBGOAL_THEN ASSUME_TAC);
233 FIRST_X_ASSUM_ST `wedge` MP_TAC;
234 REWRITE_TAC[Reuhady.WEDGE_SIMPLE;IN_ELIM_THM];
235 FIRST_X_ASSUM SUBST1_TAC;
236 TYPIFY `t1' % vec 0 + t2' % u = (-- t2') % (-- u)` (C SUBGOAL_THEN SUBST1_TAC);
237 BY(VECTOR_ARITH_TAC);
238 FIRST_X_ASSUM_ST `t < &0` MP_TAC;
239 BY(MESON_TAC[AZIM_SCALE_ALL;arith `&0 < &1`;arith `t < &0 ==> &0 < -- t`;arith `&1 % (v:real^3) = v`]);
240 FIRST_X_ASSUM_ST `x = y` kill;
241 TYPIFY `~(x IN wedge (vec 0) (v cross w) w v)` (C SUBGOAL_THEN ASSUME_TAC);
242 GMATCH_SIMP_TAC (GSYM Leaf_cell.WEDGE_GE_COMPLEMENT);
243 (REWRITE_TAC[IN_DIFF;IN_UNIV]);
244 ASM_SIMP_TAC[azim_cross_0];
245 ASM_SIMP_TAC[wedge_ge_cross];
246 GMATCH_SIMP_TAC Marchal_cells_2_new.AFF_GE_2_2;
247 REWRITE_TAC[IN_ELIM_THM];
249 TYPIFY `DISJOINT {v, w} {vec 0} /\ ~(v cross w = v) /\ ~(v cross w = w)` ENOUGH_TO_SHOW_TAC;
250 REWRITE_TAC[DISJOINT];
253 MATCH_MP_TAC Collect_geom.COLLINEAR_DISJOINT3;
254 BY(ASM_REWRITE_TAC[]);
255 REWRITE_TAC[CROSS_EQ_SELF];
256 BY(CONJ_TAC THEN ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{vec 0,(v:real^3),vec 0} = {vec 0,v} /\ {vec 0,vec 0,(w:real^3)} = {vec 0,w}`]);
257 GEXISTL_TAC [`t1`;`&0`;`t2`;`t3`];
258 REPEAT CONJ_TAC THEN ASM_TAC THEN TRY REAL_ARITH_TAC;
259 BY(REPEAT WEAKER_STRIP_TAC THEN VECTOR_ARITH_TAC);
264 let vuy1 = prove_by_refinement(
266 ~collinear {vec 0,u0,v} /\ ~collinear {vec 0,u0,u1} /\ v IN aff_ge {vec 0,u0} {u1} ==>
267 (?t0 t1. &0 < t1 /\ v = t0 % u0 + t1 % u1)`,
270 REPEAT WEAKER_STRIP_TAC;
271 FIRST_X_ASSUM_ST `aff_ge` MP_TAC;
272 GMATCH_SIMP_TAC AFF_GE_2_1;
273 REWRITE_TAC[IN_ELIM_THM];
274 REPEAT WEAKER_STRIP_TAC;
275 ASM_SIMP_TAC[Fan.th3a];
276 REPEAT WEAKER_STRIP_TAC;
278 GEXISTL_TAC [`t2`;`t3`];
281 TYPIFY `t3 = &0` (C SUBGOAL_THEN MP_TAC);
282 BY(ASM_TAC THEN REAL_ARITH_TAC);
283 DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
284 TYPIFY `v = t2 % u0` (C SUBGOAL_THEN MP_TAC);
285 BY(ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC);
286 DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
287 BY(ASM_MESON_TAC[COLLINEAR_LEMMA_ALT]);
292 let DISJOINT_PAIR = prove_by_refinement(
293 `!a b c. DISJOINT a {b,c} <=> DISJOINT a {b} /\ DISJOINT a {c}`,
296 REWRITE_TAC[DISJOINT];
301 let vuy2 = prove_by_refinement(
303 ~collinear {vec 0, u0, v} /\
304 ~collinear {vec 0, u0, u1} /\
305 v IN aff_ge {vec 0, u0} {u1} ==>
306 (u0 cross u1) dot v = &0`,
309 REPEAT WEAKER_STRIP_TAC;
310 INTRO_TAC vuy1 [`v`;`u0`;`u1`];
312 REPEAT WEAKER_STRIP_TAC;
314 REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_CROSS_SELF];
319 let vuy3 = prove_by_refinement(
320 `!v u0 u1. ~collinear {vec 0, u0, v} /\
321 ~collinear {vec 0, u0, u1} /\
322 v IN aff_ge {vec 0, u0} {u1} ==>
323 ~collinear {vec 0,u0 cross u1, v}`,
328 REWRITE_TAC[COLLINEAR_LEMMA_ALT;DE_MORGAN_THM];
330 BY(ASM_REWRITE_TAC[CROSS_EQ_0]);
331 ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
332 INTRO_TAC vuy1 [`v`;`u0`;`u1`];
334 REPEAT WEAKER_STRIP_TAC;
335 TYPIFY `v dot v = c % (u0 cross u1) dot (t0 % u0 + t1 % u1)` (C SUBGOAL_THEN MP_TAC);
337 REWRITE_TAC[DOT_RMUL;DOT_LMUL;DOT_RADD;DOT_CROSS_SELF];
338 TYPIFY ` c * (t0 * &0 + t1 * &0) = &0` (C SUBGOAL_THEN SUBST1_TAC);
340 REWRITE_TAC[DOT_EQ_0];
342 BY(ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{vec 0,u0,vec 0} = {vec 0,(u0:real^3)}`])
346 let vuy4 = prove_by_refinement(
347 `!v u0 u1. ~collinear {vec 0, u0, v} /\
348 ~collinear {vec 0, u0, u1} /\
349 v IN aff_ge {vec 0, u0} {u1} ==>
350 azim (vec 0) (u0 cross u1) u0 v < pi`,
353 REPEAT WEAKER_STRIP_TAC;
354 TYPIFY `&0 < ((u0 cross u1) cross u0) dot v` ENOUGH_TO_SHOW_TAC;
355 BY(MESON_TAC[azim_lt_pi_cross]);
356 INTRO_TAC vuy1 [`v`;`u0`;`u1`];
358 REPEAT WEAKER_STRIP_TAC;
359 ONCE_REWRITE_TAC[CROSS_TRIPLE];
361 REWRITE_TAC[CROSS_RMUL;DOT_LMUL;CROSS_RADD;DOT_CROSS_SELF;CROSS_REFL;arith `t % vec 0 + (a:real^3) = a`];
362 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
363 BY(ASM_REWRITE_TAC[DOT_POS_LT;CROSS_EQ_0])
367 let vuy5 = prove_by_refinement(
369 ~collinear {vec 0, u0, u1} ==>
370 u0 IN aff_ge {vec 0,u0} {u1}`,
373 REPEAT WEAKER_STRIP_TAC;
374 GMATCH_SIMP_TAC AFF_GE_2_1;
375 ASM_SIMP_TAC[Fan.th3a];
376 REWRITE_TAC[IN_ELIM_THM];
377 GEXISTL_TAC [`&0`;`&1`;`&0`];
378 REPEAT CONJ_TAC THEN TRY REAL_ARITH_TAC;
383 let cross_independent = prove_by_refinement(
384 `!u0 u1 a b c. ~collinear {vec 0,u0,u1} /\
385 a % (u0 cross u1) + b % u0 + c % u1 = vec 0 ==> a = &0`,
388 REPEAT WEAKER_STRIP_TAC;
389 TYPIFY ` (u0 cross u1) dot ( (--b) % u0 + (--c) % u1 ) = a * ((u0 cross u1) dot (u0 cross u1))` (C SUBGOAL_THEN MP_TAC);
390 REWRITE_TAC[GSYM DOT_RMUL];
391 TYPIFY `a % (u0 cross u1) = -- b % u0 + -- c % u1` ENOUGH_TO_SHOW_TAC;
393 BY(FIRST_X_ASSUM MP_TAC THEN VECTOR_ARITH_TAC);
394 REWRITE_TAC[DOT_RADD;DOT_RMUL;DOT_RZERO;DOT_CROSS_SELF];
395 REWRITE_TAC[arith `-- b * &0 + -- c * &0 = x <=> x = &0`];
396 REWRITE_TAC[REAL_ENTIRE;DOT_EQ_0];
397 BY(ASM_REWRITE_TAC[CROSS_EQ_0])
401 let ybt_inj = prove_by_refinement(
402 `!u0 u1 v1 v2 . ~collinear {vec 0, u0, v1} /\
403 ~collinear {vec 0, u0, v2} /\
404 ~collinear {vec 0, u0, u1} /\ ~collinear {vec 0,v1,v2} /\
405 v1 IN aff_ge {vec 0, u0} {u1} /\ v2 IN aff_ge {vec 0, u0} {u1} ==>
406 ~( azim (vec 0) (u0 cross u1) u0 v1 = azim (vec 0) (u0 cross u1) u0 v2)
410 REPEAT WEAKER_STRIP_TAC;
411 INTRO_TAC Topology.th [`(vec 0):real^3`;`u0 cross u1`;`u0`;`v2`];
412 REWRITE_TAC[EXTENSION;IN_ELIM_THM];
413 DISCH_THEN MP_TAC THEN ANTS_TAC;
415 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,(b:real^3)}`];
416 BY(ASM_MESON_TAC[Local_lemmas.COLL_IFF_COLL_CROSS]);
417 DISCH_THEN (C INTRO_TAC [`v1`]);
420 INTRO_TAC vuy1 [`v1`;`u0`;`u1`];
422 REPEAT WEAKER_STRIP_TAC;
423 FIRST_X_ASSUM_ST `aff_gt` MP_TAC;
425 GMATCH_SIMP_TAC AFF_GT_2_1;
427 REWRITE_TAC[DISJOINT;EXTENSION;IN_INTER;IN_SING;IN_INSERT;NOT_IN_EMPTY];
428 REPEAT WEAKER_STRIP_TAC;
429 FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
430 FIRST_X_ASSUM DISJ_CASES_TAC;
431 FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
432 BY(ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,a}= {a,(b:real^3)}`]);
433 FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
434 FIRST_X_ASSUM_ST `aff_ge` MP_TAC;
436 GMATCH_SIMP_TAC AFF_GE_2_1;
437 ASM_SIMP_TAC[Fan.th3a;IN_ELIM_THM];
438 REPEAT WEAKER_STRIP_TAC;
439 TYPIFY `(-- &1) % (u0 cross u1) + t2 % u0 + t3 % u1 = vec 0` (C SUBGOAL_THEN MP_TAC);
440 BY(FIRST_X_ASSUM MP_TAC THEN VECTOR_ARITH_TAC);
441 BY(ASM_MESON_TAC[cross_independent;arith `~(-- &1 = &0)`]);
442 REWRITE_TAC[IN_ELIM_THM];
443 REPEAT WEAKER_STRIP_TAC;
444 TYPIFY `v1 = t3 % v2` ENOUGH_TO_SHOW_TAC;
445 DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
446 BY(ASM_MESON_TAC[SET_RULE `{a,b,c} = {a,c,(b:real^3)}`;COLLINEAR_LEMMA_ALT]);
448 FIRST_X_ASSUM_ST `aff_ge` MP_TAC;
450 GMATCH_SIMP_TAC AFF_GE_2_1;
451 ASM_SIMP_TAC[Fan.th3a;IN_ELIM_THM];
452 REPEAT WEAKER_STRIP_TAC;
453 FIRST_X_ASSUM_ST `x:real^3` (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
454 FIRST_X_ASSUM_ST `v1 = t1' % ((vec 0):real^3) + c` (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
455 RULE_ASSUM_TAC(REWRITE_RULE[VECTOR_MUL_ASSOC;VECTOR_ADD_LDISTRIB]);
456 TYPIFY `t2 % (u0 cross u1) + (t3 * t2' - t0) % u0 + (t3*t3' - t1) % u1 = vec 0` (C SUBGOAL_THEN MP_TAC);
457 REPLICATE_TAC 2 (FIRST_X_ASSUM_ST `x:real^3` MP_TAC);
458 ONCE_REWRITE_TAC[TAUT `(a ==> b ==> c) <=> (b ==> a ==> c)`];
460 BY(VECTOR_ARITH_TAC);
462 TYPIFY `t2 = &0` (C SUBGOAL_THEN ASSUME_TAC);
463 BY(ASM_MESON_TAC[cross_independent]);
464 FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
466 FIRST_X_ASSUM_ST `x:real^3` MP_TAC;
471 let ybt_inj_0 = prove_by_refinement(
473 ~collinear {vec 0, u0, v2} /\
474 ~collinear {vec 0, u0, u1} /\
475 v2 IN aff_ge {vec 0, u0} {u1} ==>
476 ~( azim (vec 0) (u0 cross u1) u0 v2 = &0)
480 REPEAT WEAKER_STRIP_TAC;
481 FIRST_X_ASSUM MP_TAC;
482 GMATCH_SIMP_TAC Local_lemmas.AZIM_EQ_0_GE_ALT2;
484 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,(b:real^3)}`];
485 BY(ASM_MESON_TAC[Local_lemmas.COLL_IFF_COLL_CROSS]);
486 GMATCH_SIMP_TAC AFF_GE_2_1;
488 REWRITE_TAC[DISJOINT;EXTENSION;IN_INTER;IN_SING;IN_INSERT;NOT_IN_EMPTY];
489 REPEAT WEAKER_STRIP_TAC;
490 FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
491 FIRST_X_ASSUM DISJ_CASES_TAC;
492 FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
493 BY(ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{a,a,b}= {a,(b:real^3)}`]);
494 TYPIFY `u0 dot u0 = (u0 cross u1) dot u0` (C SUBGOAL_THEN MP_TAC);
496 REWRITE_TAC[DOT_CROSS_SELF];
497 REWRITE_TAC[DOT_EQ_0];
498 DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
499 BY(ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{a,a,b}= {a,(b:real^3)}`]);
500 REWRITE_TAC[IN_ELIM_THM];
501 REPEAT WEAKER_STRIP_TAC;
502 FIRST_X_ASSUM_ST `aff_ge` MP_TAC;
504 GMATCH_SIMP_TAC AFF_GE_2_1;
505 ASM_SIMP_TAC[Fan.th3a;IN_ELIM_THM];
506 REPEAT WEAKER_STRIP_TAC;
507 TYPIFY `t2 % (u0 cross u1) + (t3 - t2') % u0 + (-- t3') % u1 = vec 0` (C SUBGOAL_THEN MP_TAC);
508 BY(FIRST_X_ASSUM MP_TAC THEN VECTOR_ARITH_TAC);
510 TYPIFY `t2 = &0` (C SUBGOAL_THEN ASSUME_TAC);
511 BY(ASM_MESON_TAC[cross_independent]);
512 FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
513 REPLICATE_TAC 4 (FIRST_X_ASSUM kill);
514 TYPIFY `v2 = t3 % u0` (C SUBGOAL_THEN ASSUME_TAC);
515 BY(FIRST_X_ASSUM MP_TAC THEN VECTOR_ARITH_TAC);
516 FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
517 BY(ASM_MESON_TAC[COLLINEAR_LEMMA_ALT])
521 let ECAU_aff_ge = prove_by_refinement(
522 `!(u:num->real^3) r. (!i j. i <= r /\ j <= r /\ ~(i = j) ==> ~collinear {vec 0, u i, u j}) /\
523 (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0,u 0 } {u 1} ) ==>
524 (!i. 1 <= i /\ i <= r ==> u i IN aff_ge {vec 0,u 0 } {u 1} ) `,
527 REPEAT WEAKER_STRIP_TAC;
528 TYPIFY `u i IN aff_gt {vec 0,u 0} {u 1}` (C SUBGOAL_THEN MP_TAC);
529 ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
530 BY(FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
531 INTRO_TAC AFF_GT_SUBSET_AFF_GE [`{vec 0,u 0}`;`{u 1}`];
536 let collinear_cross = prove_by_refinement(
537 `!u i r. i <= r /\ 1 <= r /\ (!i j. i <= r /\ j <= r /\ ~(i = j) ==> ~collinear {vec 0, u i, u j}) /\
538 (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0,u 0 } {u 1} )
539 ==> ~collinear {vec 0,u 0 cross u 1,u i}`,
542 REPEAT WEAKER_STRIP_TAC;
543 FIRST_X_ASSUM MP_TAC;
545 TYPIFY `i = 0` ASM_CASES_TAC;
547 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
548 REWRITE_TAC[GSYM Local_lemmas.COLL_IFF_COLL_CROSS];
549 FIRST_X_ASSUM MATCH_MP_TAC;
550 BY(ASM_TAC THEN ARITH_TAC);
551 INTRO_TAC ECAU_aff_ge [`u`;`r`];
555 BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_TAC THEN TRY ARITH_TAC)
559 let YBTASCZ1 = prove_by_refinement(
561 (j <= r) /\ (1<= r) /\
562 (!i j. i <= r /\ j <= r /\ ~(i=j) ==> ~collinear {vec 0,u i ,u j}) /\
563 (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0,u 0 } {u 1} ) /\
564 cyclic_set {u i | i <= r} (vec 0) ((u 0) cross (u 1)) /\
565 (!i. i < r ==> azim_cycle {u i | i <= r} (vec 0) ((u 0) cross (u 1)) (u i) = u (i+1)) ==>
566 (!i. i < j ==> azim (vec 0) ((u 0) cross (u 1)) (u 0) (u i) < azim (vec 0) (u 0 cross (u 1)) (u 0) (u j))
572 INTRO_TAC ECAU_aff_ge [`u`;`r`];
577 REWRITE_TAC[arith `a < b <=> (a <= b /\ ~(a = b))`];
579 BY(REWRITE_TAC[AZIM_REFL;Local_lemmas.AZIM_RANGE]);
580 REWRITE_TAC[AZIM_REFL];
581 ONCE_REWRITE_TAC[EQ_SYM_EQ];
582 MATCH_MP_TAC ybt_inj_0;
583 ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
584 BY(REPEAT CONJ_TAC THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_TAC THEN TRY ARITH_TAC);
585 COMMENT "induction step";
586 ONCE_REWRITE_TAC[arith `a < b <=> ~(b < a) /\ ~(a = b)`];
587 REPEAT WEAKER_STRIP_TAC;
589 MATCH_MP_TAC ybt_inj;
590 ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
591 BY(REPEAT CONJ_TAC THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_TAC THEN TRY ARITH_TAC);
593 TYPIFY `i < (j:num)` (C SUBGOAL_THEN ASSUME_TAC);
594 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
595 ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
596 TYPIFY `azim_cycle {u i | i <= r} (vec 0) (u 0 cross u 1) (u i) = u (i+1)` (C SUBGOAL_THEN ASSUME_TAC);
597 FIRST_X_ASSUM MATCH_MP_TAC;
598 BY(ASM_TAC THEN ARITH_TAC);
599 INTRO_TAC (GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_PROPERTIES) [`{u i | (i:num) <= r}`;`u i`;`u 0 cross u 1`;`(vec 0):real^3`];
602 REWRITE_TAC[SUBSET;IN_ELIM_THM;IN_SING];
603 TYPIFY `1 <= r` (C SUBGOAL_THEN MP_TAC);
604 BY(ASM_REWRITE_TAC[]);
605 TYPIFY (`~(u 0 = u 1)`) ENOUGH_TO_SHOW_TAC;
606 BY(MESON_TAC[arith `1 <= r ==> 0 <= r /\ 1 <= r`]);
608 FIRST_X_ASSUM_ST `collinear` (C INTRO_TAC [`0`;`1`]);
610 BY(ASM_TAC THEN ARITH_TAC);
612 BY(MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,b}= {a,(b:real^3)}`]);
613 TYPIFY `{u i | i <= r } = IMAGE u {i | i <= (r:num)}` (C SUBGOAL_THEN SUBST1_TAC);
615 MATCH_MP_TAC FINITE_IMAGE;
616 BY(REWRITE_TAC[FINITE_NUMSEG_LE]);
618 REPEAT WEAKER_STRIP_TAC;
619 FIRST_X_ASSUM (C INTRO_TAC [`u j`]);
623 FIRST_X_ASSUM_ST `collinear` (C INTRO_TAC [`j`;`i`]);
625 BY(ASM_TAC THEN ARITH_TAC);
627 BY(MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,b}= {a,(b:real^3)}`]);
628 TYPIFY_GOAL_THEN `(j:num) <=r ==> {u i | i <= r} (u j)` MATCH_MP_TAC;
629 TYPIFY `{u i | i <= r } = IMAGE u {i | i <= (r:num)}` (C SUBGOAL_THEN SUBST1_TAC);
631 REWRITE_TAC[IMAGE;IN_ELIM_THM];
633 BY(ASM_TAC THEN ARITH_TAC);
634 REWRITE_TAC[arith `i+1 = SUC i`];
635 REWRITE_TAC[DE_MORGAN_THM];
638 FIRST_X_ASSUM_ST `(i:num) < j ==> b` MP_TAC;
643 ONCE_REWRITE_TAC[arith `a < b <=> &0 < b - a`];
644 GMATCH_SIMP_TAC Leaf_cell.AZIM_BASE_SHIFT_LE;
645 TYPIFY `u i` EXISTS_TAC;
646 (ASM_SIMP_TAC[arith `x <= x` ;arith `x < y ==> x <= y`]);
648 BY(REPEAT (GMATCH_SIMP_TAC collinear_cross) THEN REPEAT CONJ_TAC THEN TYPIFY `r` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN TRY ARITH_TAC);
649 REWRITE_TAC[arith `&0 < a - b <=> b < a`];
651 COMMENT "second shift";
652 TYPIFY `azim (vec 0) (u 0 cross u 1) (u i) (u j) < azim (vec 0) (u 0 cross u 1) (u i) (u (SUC i))` (C SUBGOAL_THEN ASSUME_TAC);
653 FIRST_X_ASSUM_ST `SUC` kill;
654 FIRST_ASSUM_ST `SUC` MP_TAC;
655 ONCE_REWRITE_TAC[arith `a < b <=> &0 < b - a`];
656 MATCH_MP_TAC (arith `a = b ==> &0 < a ==> &0 < b`);
657 MATCH_MP_TAC Leaf_cell.AZIM_BASE_SHIFT_LE;
658 (ASM_SIMP_TAC[arith `x <= x` ;arith `x < y ==> x <= y`]);
659 REWRITE_TAC[TAUT `(a /\ b /\ c) <=> ((a /\ b) /\ c)`];
661 BY(ASM_TAC THEN REAL_ARITH_TAC);
662 BY(REPEAT (GMATCH_SIMP_TAC collinear_cross) THEN REPEAT CONJ_TAC THEN TYPIFY `r` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN TRY ARITH_TAC);
663 BY(ASM_TAC THEN REAL_ARITH_TAC)
667 let YBTASCZ2 = prove_by_refinement(
669 (i < j) /\ (j <= r) /\ (1<= r) /\
670 (!i j. i <= r /\ j <= r /\ ~(i=j) ==> ~collinear {vec 0,u i ,u j}) /\
671 (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0,u 0 } {u 1} ) /\
672 cyclic_set {u i | i <= r} (vec 0) ((u 0) cross (u 1)) /\
673 (!i. i < r ==> azim_cycle {u i | i <= r} (vec 0) ((u 0) cross (u 1)) (u i) = u (i+1)) ==>
674 (azim (vec 0) ((u 0) cross (u 1)) (u i) (u j) < pi)
678 REPEAT WEAKER_STRIP_TAC;
679 INTRO_TAC YBTASCZ1 [`u`;`r`;`j`];
681 DISCH_THEN (C INTRO_TAC [`i`]);
684 INTRO_TAC Fan.sum4_azim_fan [`(vec 0):real^3`;`u 0 cross u 1`;`u 0`;`u i`;`u j`];
686 ASM_SIMP_TAC[arith `x < y ==> x <= y`];
687 BY(REPEAT CONJ_TAC THEN MATCH_MP_TAC collinear_cross THEN TYPIFY `r` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN TRY ARITH_TAC);
688 INTRO_TAC vuy4 [`u j`;`u 0`;`u 1`];
690 INTRO_TAC ECAU_aff_ge [`u`;`r`];
693 BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_TAC THEN ARITH_TAC);
694 INTRO_TAC Counting_spheres.AZIM_NN [`(vec 0):real^3`;`u 0 cross u 1`;`u 0`;`u i`];
699 let YBTASCZ3 = prove_by_refinement(
701 (i < j) /\ (j <= r) /\ (1<= r) /\
702 (!i j. i <= r /\ j <= r /\ ~(i=j) ==> ~collinear {vec 0,u i ,u j}) /\
703 (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0,u 0 } {u 1} ) /\
704 cyclic_set {u i | i <= r} (vec 0) ((u 0) cross (u 1)) /\
705 (!i. i < r ==> azim_cycle {u i | i <= r} (vec 0) ((u 0) cross (u 1)) (u i) = u (i+1)) ==>
706 (&0 < azim (vec 0) ((u 0) cross (u 1)) (u i) (u j))
710 REPEAT WEAKER_STRIP_TAC;
711 INTRO_TAC YBTASCZ1 [`u`;`r`;`j`];
713 DISCH_THEN (C INTRO_TAC [`i`]);
716 INTRO_TAC Fan.sum4_azim_fan [`(vec 0):real^3`;`u 0 cross u 1`;`u 0`;`u i`;`u j`];
718 ASM_SIMP_TAC[arith `x < y ==> x <= y`];
719 BY(REPEAT CONJ_TAC THEN MATCH_MP_TAC collinear_cross THEN TYPIFY `r` EXISTS_TAC THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN TRY ARITH_TAC);
720 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
724 let KCZXLLE = prove_by_refinement(
726 (j < k) /\ (k <= r) /\ (1<= r) /\ (i <= r) /\ ((i < j \/ k < i)) /\
727 (!i j. i <= r /\ j <= r /\ ~(i=j) ==> ~collinear {vec 0,u i ,u j}) /\
728 (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0,u 0 } {u 1} ) /\
729 cyclic_set {u i | i <= r} (vec 0) ((u 0) cross (u 1)) /\
730 (!i. i < r ==> azim_cycle {u i | i <= r} (vec 0) ((u 0) cross (u 1)) (u i) = u (i+1)) ==>
731 (azim (vec 0) (u i) (u j) (u k) = &0)
735 REPEAT WEAKER_STRIP_TAC;
736 TYPIFY `?r. j < k /\ k <= r /\ 1 <= r /\ (!i j. i <= r /\ j <= r /\ ~(i = j) ==> ~collinear {vec 0, u i, u j}) /\ (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0, u 0} {u 1}) /\ cyclic_set {u i | i <= r} (vec 0) (u 0 cross u 1) /\ (!i. i < r ==> azim_cycle {u i | i <= r} (vec 0) (u 0 cross u 1) (u i) = u (i + 1))` (C SUBGOAL_THEN ASSUME_TAC);
737 TYPIFY `r` EXISTS_TAC;
738 BY(ASM_REWRITE_TAC[]);
739 INTRO_TAC ECAU_aff_ge [`u`;`r`] THEN ASM_REWRITE_TAC[] THEN DISCH_TAC;
741 TYPIFY `!i. i <= r ==> u i IN affine hull {vec 0,u 0,u 1}` (C SUBGOAL_THEN ASSUME_TAC);
742 REPEAT WEAKER_STRIP_TAC;
743 ASM_CASES_TAC `i' = 0`;
744 MATCH_MP_TAC HULL_INC;
747 RULE_ASSUM_TAC(REWRITE_RULE[arith `~(i=0) <=> 1<= i`]);
748 REWRITE_TAC[GSYM Trigonometry.UIVNNRR2];
749 INTRO_TAC (GEN_ALL Local_lemmas.AFF_GT_MONO) [`{vec 0,u 0}`;`{u 1}`;`{u 1}`];
752 TYPIFY_GOAL_THEN `{vec 0,u 0} UNION {u 1} = {vec 0,u 0,u 1} /\ {u 1} DIFF {u 1} = {}` (unlist REWRITE_TAC);
754 TYPIFY `u i' IN aff_gt {vec 0, u 0} {u 1}` ENOUGH_TO_SHOW_TAC;
756 FIRST_X_ASSUM MATCH_MP_TAC;
757 BY(ASM_REWRITE_TAC[]);
758 COMMENT "ARITH GOES HERE";
759 TYPIFY `j <= (r:num)` (C SUBGOAL_THEN ASSUME_TAC);
760 REPLICATE_TAC 10 (FIRST_X_ASSUM kill);
761 BY(ASM_TAC THEN ARITH_TAC);
762 TYPIFY `~(i = j) /\ ~(i = k) /\ 0 <= r` (C SUBGOAL_THEN ASSUME_TAC);
763 BY(REPLICATE_TAC 6 (FIRST_X_ASSUM kill) THEN ASM_TAC THEN ARITH_TAC);
764 TYPIFY `~(0 = k) /\ (1 <= k) /\ ~(0=1)` (C SUBGOAL_THEN ASSUME_TAC);
765 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM kill) THEN ASM_TAC THEN ARITH_TAC);
766 COMMENT "other prelims here";
767 TYPIFY `~collinear {vec 0, u 0, u 1} /\ ~collinear {vec 0,u i,u j} /\ ~collinear {vec 0,u i,u k}` (C SUBGOAL_THEN ASSUME_TAC);
768 BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[arith `~(0=1)`]);
769 TYPIFY `DISJOINT {vec 0, u 0} {u 1}` (C SUBGOAL_THEN ASSUME_TAC);
770 GMATCH_SIMP_TAC Fan.th3a;
771 BY(ASM_REWRITE_TAC[]);
772 TYPIFY `~collinear {vec 0, u 0, u k} /\ ~collinear {vec 0, u 0, u 1} /\ u k IN aff_ge {vec 0, u 0} {u 1} /\ u k IN aff_gt {vec 0, u 0} {u 1}` (C SUBGOAL_THEN ASSUME_TAC);
773 BY((REPEAT CONJ_TAC) THEN (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[]);
774 TYPIFY `!i. i <= r ==> ~collinear {vec 0,u 0 cross u 1, u i}` (C SUBGOAL_THEN ASSUME_TAC);
775 REPEAT WEAKER_STRIP_TAC;
776 ASM_CASES_TAC `i' = 0`;
777 FIRST_X_ASSUM_ST `collinear` MP_TAC;
779 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
780 REWRITE_TAC[GSYM Local_lemmas.COLL_IFF_COLL_CROSS];
781 BY(ASM_REWRITE_TAC[]);
782 RULE_ASSUM_TAC (ONCE_REWRITE_RULE[arith `~(i'=0) <=> (1 <= i' /\ ~(i' = 0))`]);
783 FIRST_X_ASSUM_ST `collinear` MP_TAC;
786 BY((REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]));
788 TYPIFY `coplanar {vec 0, u i, u j, u k}` (C SUBGOAL_THEN ASSUME_TAC);
789 REWRITE_TAC[coplanar];
790 GEXISTL_TAC [`(vec 0):real^3`;`u 0`;`u 1`];
791 REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
792 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN (FIRST_X_ASSUM MATCH_MP_TAC ORELSE MATCH_MP_TAC HULL_INC) THEN ASM_REWRITE_TAC[];
793 BY(REPEAT WEAKER_STRIP_TAC THEN SET_TAC[]);
794 RULE_ASSUM_TAC(REWRITE_RULE[GSYM Local_lemmas1.AZIM_COND_FOR_COPLANAR]);
795 FIRST_X_ASSUM DISJ_CASES_TAC;
796 BY(ASM_REWRITE_TAC[]);
797 PROOF_BY_CONTR_TAC THEN FIRST_X_ASSUM kill;
798 INTRO_TAC (GEN_ALL Ldurdpn.LDURDPN) [`u i`;`u j`;`u k`];
800 BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
802 REWRITE_TAC[DE_MORGAN_THM];
804 TYPIFY `conv0 {u j,u k} SUBSET aff_gt {vec 0, u 0} {u 1}` (C SUBGOAL_THEN ASSUME_TAC);
806 ASM_REWRITE_TAC[Geomdetail.CONV0_SET2;SUBSET;IN_ELIM_THM];
807 REPEAT WEAKER_STRIP_TAC;
808 GMATCH_SIMP_TAC AFF_GT_2_1;
809 ASM_REWRITE_TAC[IN_ELIM_THM];
810 INTRO_TAC vuy1 [`u k`;`u 0`;`u 1`];
812 BY(ASM_REWRITE_TAC[]);
813 REPEAT WEAKER_STRIP_TAC;
815 GEXISTL_TAC [`&1 - a - b * (t0 + t1)`;`a + b * t0`;`b*t1`];
816 GMATCH_SIMP_TAC REAL_LT_MUL_EQ;
820 BY(VECTOR_ARITH_TAC);
822 MATCH_MP_TAC SUBSET_TRANS;
823 TYPIFY `conv {u j,u k}` EXISTS_TAC;
824 REWRITE_TAC[Geomdetail.CONV02_SU_CONV2];
825 MATCH_MP_TAC Geomdetail.CONVEX_IM_CONV2_SU;
826 ASM_REWRITE_TAC[CONVEX_AFF_GT];
827 RULE_ASSUM_TAC(REWRITE_RULE[arith `~(j=0) <=> 1<=j`]);
828 BY( FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
829 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_INTER;NOT_IN_EMPTY];
830 REWRITE_TAC[TAUT `~(a /\ b) <=> (b ==> ~a)`];
831 REPEAT WEAKER_STRIP_TAC;
832 FIRST_X_ASSUM_ST `aff` MP_TAC;
833 REWRITE_TAC[Trigonometry2.AFF2_VEC0;IN_ELIM_THM];
834 REPEAT WEAKER_STRIP_TAC;
835 TYPIFY `k' % u i IN aff_gt {vec 0, u 0} {u 1}` (C SUBGOAL_THEN MP_TAC);
836 BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN SET_TAC[]);
838 GMATCH_SIMP_TAC AFF_GT_2_1;
839 ASM_REWRITE_TAC[IN_ELIM_THM];
840 REPEAT WEAKER_STRIP_TAC;
841 TYPIFY `~(i = 0)` (C SUBGOAL_THEN ASSUME_TAC);
843 FIRST_X_ASSUM_ST `%` MP_TAC;
845 TYPIFY `~collinear {vec 0, u 0, u 1}` (C SUBGOAL_THEN MP_TAC);
846 BY(ASM_REWRITE_TAC[]);
847 REWRITE_TAC[COLLINEAR_LEMMA_ALT];
848 REWRITE_TAC[DE_MORGAN_THM;NOT_EXISTS_THM];
849 REPEAT WEAKER_STRIP_TAC;
850 FIRST_X_ASSUM (C INTRO_TAC [`(inv t3 * (k' - t2))`]);
852 TYPIFY `t3 % u 1 = t3 % (inv t3 * (k' - t2)) % u 0` ENOUGH_TO_SHOW_TAC;
853 REWRITE_TAC[VECTOR_MUL_LCANCEL];
854 DISCH_THEN DISJ_CASES_TAC;
855 BY(FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE)) THEN FIRST_X_ASSUM_ST `&0 < &0` MP_TAC THEN REAL_ARITH_TAC);
856 BY(FIRST_X_ASSUM ACCEPT_TAC);
857 FIRST_X_ASSUM MP_TAC;
858 REWRITE_TAC[VECTOR_MUL_ASSOC];
859 TYPIFY `(t3 * inv t3 * (k' - t2)) = k' - t2` (C SUBGOAL_THEN SUBST1_TAC);
860 Calc_derivative.CALC_ID_TAC;
861 BY(FIRST_X_ASSUM_ST `&0 < t3` MP_TAC THEN REAL_ARITH_TAC);
862 BY(VECTOR_ARITH_TAC);
863 TYPIFY `?t. &0 < t /\ x = t % u i` (C SUBGOAL_THEN MP_TAC);
864 FIRST_X_ASSUM_ST `aff_gt` (C INTRO_TAC [`i`]);
866 BY(RULE_ASSUM_TAC(REWRITE_RULE[arith `~(i=0) <=> 1 <= i`]) THEN ASM_REWRITE_TAC[]);
867 GMATCH_SIMP_TAC AFF_GT_2_1;
868 ASM_REWRITE_TAC[IN_ELIM_THM];
869 REPEAT WEAKER_STRIP_TAC;
870 TYPIFY `k'` EXISTS_TAC;
872 TYPIFY `k' = t3/ t3'` ENOUGH_TO_SHOW_TAC;
873 DISCH_THEN SUBST1_TAC;
874 GMATCH_SIMP_TAC REAL_LT_DIV;
875 BY(ASM_REWRITE_TAC[]);
876 FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
877 TYPIFY `t3 = k' * t3'` ENOUGH_TO_SHOW_TAC;
878 DISCH_THEN SUBST1_TAC;
879 Calc_derivative.CALC_ID_TAC;
880 BY((FIRST_X_ASSUM_ST `&0 < t` MP_TAC) THEN REAL_ARITH_TAC);
882 TYPIFY `(k'*t2' - t2) % u 0 + (k'*t3' - t3) % u 1 = vec 0` (C SUBGOAL_THEN MP_TAC);
883 BY(FIRST_X_ASSUM_ST `%` MP_TAC THEN VECTOR_ARITH_TAC);
885 TYPIFY `inv (k' * t3' - t3) % (k' * t3' - t3) % u 1 = inv(k' * t3' - t3) % (t2 - k' * t2') % u 0` (C SUBGOAL_THEN ASSUME_TAC);
886 REWRITE_TAC[VECTOR_MUL_LCANCEL];
888 BY(FIRST_X_ASSUM MP_TAC THEN VECTOR_ARITH_TAC);
889 FIRST_X_ASSUM MP_TAC;
890 REWRITE_TAC[VECTOR_MUL_ASSOC];
891 TYPIFY `inv (k' * t3' - t3) * (k' * t3' - t3) = &1` (C SUBGOAL_THEN SUBST1_TAC);
892 Calc_derivative.CALC_ID_TAC;
893 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
894 REWRITE_TAC[VECTOR_MUL_LID];
896 FIRST_X_ASSUM_ST `collinear` (C INTRO_TAC [`0`;`1`]);
898 BY(ASM_REWRITE_TAC[]);
899 BY(ASM_MESON_TAC[COLLINEAR_LEMMA_ALT]);
900 REPEAT WEAKER_STRIP_TAC;
902 TYPIFY `conv0 {u j,u k} SUBSET wedge (vec 0) (u 0 cross u 1) (u j) (u k)` (C SUBGOAL_THEN ASSUME_TAC);
903 TYPIFY `wedge (vec 0) (u 0 cross u 1) (u j) (u k) = aff_gt {vec 0,u 0 cross u 1} {u j,u k}` ENOUGH_TO_SHOW_TAC;
904 DISCH_THEN SUBST1_TAC;
905 REWRITE_TAC[CONV0_AFF_GT];
906 MATCH_MP_TAC AFF_GT_MONO_LEFT;
908 MATCH_MP_TAC WEDGE_LUNE_GT;
909 TYPIFY_GOAL_THEN `~collinear {vec 0, u 0 cross u 1, u j}` (unlist REWRITE_TAC);
910 ASM_CASES_TAC `j= 0`;
912 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
913 REWRITE_TAC[GSYM Local_lemmas.COLL_IFF_COLL_CROSS];
914 FIRST_X_ASSUM MATCH_MP_TAC;
915 BY(ASM_REWRITE_TAC[]);
916 FIRST_X_ASSUM MATCH_MP_TAC;
917 BY(ASM_REWRITE_TAC[]);
919 FIRST_X_ASSUM MATCH_MP_TAC;
920 BY(ASM_REWRITE_TAC[]);
921 GMATCH_SIMP_TAC YBTASCZ3;
923 GMATCH_SIMP_TAC YBTASCZ2;
924 BY(ASM_REWRITE_TAC[]);
925 TYPIFY `x IN wedge (vec 0) (u 0 cross u 1) (u j) (u k)` (C SUBGOAL_THEN MP_TAC);
926 BY(REPEAT (FIRST_X_ASSUM_ST `conv0` MP_TAC) THEN SET_TAC[]);
927 REWRITE_TAC[Reuhady.WEDGE_SIMPLE;IN_ELIM_THM];
928 FIRST_X_ASSUM_ST `x = (y:real^3)` SUBST1_TAC;
929 TYPIFY `azim (vec 0) (u 0 cross u 1) (u j) (t % u i) = azim (vec 0) (u 0 cross u 1) (u j) (u i)` (C SUBGOAL_THEN SUBST1_TAC);
930 FIRST_X_ASSUM_ST `&0 < t` MP_TAC;
931 BY(MESON_TAC[AZIM_SCALE_ALL;arith `&0 < &1`;arith `&1 % v = v`]);
933 REWRITE_TAC[DE_MORGAN_THM];
935 FIRST_X_ASSUM DISJ_CASES_TAC;
936 REWRITE_TAC[arith `~(a < b) <=> b <= a`];
937 MATCH_MP_TAC REAL_LE_TRANS;
938 TYPIFY `pi` EXISTS_TAC;
940 MATCH_MP_TAC (arith `x < pi ==> x <= pi`);
941 MATCH_MP_TAC YBTASCZ2;
943 BY(ASM_REWRITE_TAC[]);
945 ONCE_REWRITE_TAC[Rogers.AZIM_COMPL_EXT];
947 TYPIFY `&0 < azim (vec 0) (u 0 cross u 1) (u i) (u j)` ENOUGH_TO_SHOW_TAC;
948 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
949 MATCH_MP_TAC YBTASCZ3;
950 TYPIFY `r` EXISTS_TAC;
951 BY(ASM_REWRITE_TAC[]);
952 MATCH_MP_TAC (arith `x < pi ==> pi <= &2 * pi - x`);
953 MATCH_MP_TAC YBTASCZ2;
955 BY(ASM_REWRITE_TAC[]);
957 REWRITE_TAC[arith `~(a < b) <=> b <= a`];
958 INTRO_TAC Fan.sum3_azim_fan [`(vec 0):real^3`;`u 0 cross u 1`;`u j`;`u k`;`u i`];
961 MATCH_MP_TAC (arith `x < pi /\ y < pi ==> x + y < &2 * pi`);
962 CONJ_TAC THEN (MATCH_MP_TAC YBTASCZ2);
963 TYPIFY `r` EXISTS_TAC;
964 BY(ASM_REWRITE_TAC[]);
965 TYPIFY `r` EXISTS_TAC;
966 BY(ASM_REWRITE_TAC[]);
967 BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
968 TYPIFY `&0 <= azim (vec 0) (u 0 cross u 1) (u k) (u i)` ENOUGH_TO_SHOW_TAC;
970 BY(REWRITE_TAC[Counting_spheres.AZIM_NN])
974 let KCZXLLE_SYM = prove_by_refinement(
980 ((j < k /\ (i < j \/ k < i)) \/ (k < j /\ (i < k \/ j < i))) /\
982 i <= r /\ j <= r /\ ~(i = j) ==> ~collinear {vec 0, u i, u j}) /\
983 (!i. 1 <= i /\ i <= r ==> u i IN aff_gt {vec 0, u 0} {u 1}) /\
984 cyclic_set {u i | i <= r} (vec 0) (u 0 cross u 1) /\
986 ==> azim_cycle {u i | i <= r} (vec 0) (u 0 cross u 1) (u i) =
988 ==> azim (vec 0) (u i) (u j) (u k) = &0`,
991 REPEAT WEAKER_STRIP_TAC;
992 FIRST_X_ASSUM DISJ_CASES_TAC;
993 MATCH_MP_TAC KCZXLLE;
994 TYPIFY `r` EXISTS_TAC;
995 BY(ASM_REWRITE_TAC[]);
996 ONCE_REWRITE_TAC[Local_lemmas.AZIM_EQ_0_SYM2];
997 MATCH_MP_TAC KCZXLLE;
998 TYPIFY `r` EXISTS_TAC;
999 BY(ASM_REWRITE_TAC[])
1003 let open_continuous_eps = prove_by_refinement(
1004 `!U f t a b. (t IN real_interval (a,b)) /\ f t IN U /\
1005 (!x. x IN real_interval (a,b) ==> f real_continuous atreal x) /\ real_open U ==>
1006 (?e. &0 < e /\ (!x. abs (x-t) < e ==> f x IN U))`,
1009 REPEAT WEAKER_STRIP_TAC;
1010 INTRO_TAC Pent_hex.continuous_preimage_open [`f`;`real_interval (a,b)`;`U`];
1013 BY(ASM_SIMP_TAC[ Ocbicby.REAL_OPEN_REAL_INTERVAL;REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT ]);
1014 REWRITE_TAC[real_open;IN_ELIM_THM];
1015 DISCH_THEN (C INTRO_TAC [`t`]);
1017 REPEAT WEAKER_STRIP_TAC;
1022 let coplanar_in_affine_hull = prove_by_refinement(
1023 `!(u:real^A) v w x. ~collinear {u,v,w} /\ coplanar {x,u,v,w} ==> x IN affine hull {u,v,w}`,
1026 REPEAT WEAKER_STRIP_TAC;
1027 INTRO_TAC Counting_spheres.NOT_COLLINEAR_AFF_DIM_2 [`u`;`v`;`w`];
1028 ASM_REWRITE_TAC[] THEN DISCH_TAC;
1029 MATCH_MP_TAC Leaf_cell.COPLANAR_INSERT;
1030 BY(ASM_REWRITE_TAC[])
1034 let azim_0_as_closed = prove_by_refinement(
1035 `!(v2:real^3) v3 v4. ~collinear {vec 0, v2,v3} /\ ~collinear {vec 0,v2,v4} ==>
1036 (azim (vec 0) v2 v3 v4 = &0 <=> (coplanar {vec 0,v2,v3,v4} /\ &0 <= ((v2 cross v3) cross v2) dot v4))`,
1039 REPEAT WEAKER_STRIP_TAC;
1040 TYPIFY `~coplanar {vec 0,v2,v3,v4}` ASM_CASES_TAC THEN RULE_ASSUM_TAC(REWRITE_RULE[]) THEN ASM_REWRITE_TAC[];
1041 BY(ASM_MESON_TAC[AZIM_EQ_0_PI_IMP_COPLANAR]);
1042 INTRO_TAC coplanar_in_affine_hull [`(vec 0):real^3`;`v2`;`v3`;`v4`];
1044 ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {b,c,d,a}`];
1045 BY(ASM_REWRITE_TAC[]);
1047 INTRO_TAC Ckqowsa_4_points.in_affine_hull_lemma [`v2`;`v3`;`v4`];
1049 REPEAT WEAKER_STRIP_TAC;
1050 TYPIFY `&0 <= ((v2 cross v3) cross v2) dot v4 <=> &0 <= t2` (C SUBGOAL_THEN SUBST1_TAC);
1051 ASM_REWRITE_TAC[DOT_RADD;DOT_RMUL];
1052 ONCE_REWRITE_TAC[CROSS_TRIPLE];
1053 REWRITE_TAC[CROSS_REFL;DOT_LZERO];
1054 REWRITE_TAC[arith `t1 * &0 + c = c`];
1055 GMATCH_SIMP_TAC (CONJUNCT2 REAL_LE_MUL_EQ);
1056 REWRITE_TAC[DOT_POS_LT];
1057 BY(ASM_REWRITE_TAC[CROSS_EQ_0]);
1058 TYPIFY `azim (vec 0) v2 v3 v4 = &0 <=> ~(azim (vec 0) v2 v3 v4 = pi)` (C SUBGOAL_THEN SUBST1_TAC);
1059 BY(ASM_MESON_TAC[Local_lemmas1.AZIM_COND_FOR_COPLANAR;PI_POS;arith `&0 < pi ==> ~(&0 = pi)`]);
1060 GMATCH_SIMP_TAC Ldurdpn.LDURDPN;
1062 BY(ASM_MESON_TAC[]);
1063 TYPIFY_GOAL_THEN `(?A. plane A /\ {vec 0, v2, v3, v4} SUBSET A)` (unlist REWRITE_TAC);
1064 FIRST_X_ASSUM_ST `coplanar` MP_TAC THEN REWRITE_TAC[coplanar] THEN REPEAT WEAKER_STRIP_TAC;
1065 TYPIFY `affine hull {vec 0,v2,v3}` EXISTS_TAC;
1067 TYPIFY `v4 IN affine hull {vec 0,v2,v3} /\ {vec 0 ,v2,v3} SUBSET affine hull {vec 0,v2,v3}` ENOUGH_TO_SHOW_TAC;
1069 BY(CONJ_TAC THEN ASM_MESON_TAC[Qzksykg.SET_SUBSET_AFFINE_HULL]);
1071 BY(ASM_MESON_TAC[]);
1073 REWRITE_TAC[EXTENSION;IN_INTER;NOT_IN_EMPTY];
1074 REWRITE_TAC[Trigonometry2.AFF2_VEC0;IN_ELIM_THM;Geomdetail.CONV0_SET2;DE_MORGAN_THM;NOT_EXISTS_THM];
1075 TYPIFY `(!x. (!k. ~(x = k % v2)) \/ (!a b. ~(&0 < a) \/ ~(&0 < b) \/ ~(a + b = &1) \/ ~(x = a % v3 + b % (t1 % v2 + t2 % v3)))) <=> (!k a b. &0 < a /\ &0 < b /\ a + b = &1 ==> ~(k % v2 = a % v3 + b % (t1 % v2 + t2 % v3)))` (C SUBGOAL_THEN SUBST1_TAC);
1077 COMMENT "first case";
1078 ASM_CASES_TAC `&0 <= t2`;
1080 REPEAT WEAKER_STRIP_TAC;
1081 TYPIFY `v3 = (inv (b * t2 + a) * (-- (b * t1 - k))) % v2` ENOUGH_TO_SHOW_TAC;
1082 BY(ASM_MESON_TAC[COLLINEAR_LEMMA_ALT]);
1083 MATCH_MP_TAC VECTOR_MUL_LCANCEL_IMP;
1084 TYPIFY `(b * t2 + a)` EXISTS_TAC;
1086 MATCH_MP_TAC (arith `&0 <= b' /\ &0 < a ==> ~(b' + a = &0)`);
1087 GMATCH_SIMP_TAC REAL_LE_MUL;
1088 BY(ASM_TAC THEN REAL_ARITH_TAC);
1089 REWRITE_TAC[VECTOR_MUL_ASSOC];
1091 TYPIFY `((b * t2 + a) * inv (b * t2 + a) * --(b * t1 - k)) = -- (b * t1 - k)` (C SUBGOAL_THEN SUBST1_TAC);
1092 Calc_derivative.CALC_ID_TAC;
1093 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1094 BY(FIRST_X_ASSUM_ST `%` MP_TAC THEN VECTOR_ARITH_TAC);
1095 ASM_REWRITE_TAC[NOT_FORALL_THM];
1096 TYPIFY `~(t2 = &1)` (C SUBGOAL_THEN ASSUME_TAC);
1097 DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
1098 BY(ASM_TAC THEN REAL_ARITH_TAC);
1099 GEXISTL_TAC [`t1 / (&1 - t2)`;`-- t2 / (&1 - t2)`;`&1 / (&1 - t2)`;];
1100 DISCH_THEN MP_TAC THEN ANTS_TAC;
1101 GMATCH_SIMP_TAC REAL_LT_DIV;
1102 GMATCH_SIMP_TAC REAL_LT_DIV;
1103 TYPIFY `--t2 / (&1 - t2) + &1 / (&1 - t2) = &1` (C SUBGOAL_THEN SUBST1_TAC);
1104 Calc_derivative.CALC_ID_TAC;
1105 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1106 BY(ASM_TAC THEN REAL_ARITH_TAC);
1108 TYPIFY `&1 / (&1 - t2) % (t1 % v2 + t2 % v3) = t1 / (&1 - t2) % v2 - --t2 / (&1 - t2) % v3` ENOUGH_TO_SHOW_TAC;
1109 DISCH_THEN SUBST1_TAC;
1110 BY(VECTOR_ARITH_TAC);
1111 REWRITE_TAC[VECTOR_ADD_LDISTRIB];
1112 REWRITE_TAC[VECTOR_MUL_ASSOC];
1113 TYPIFY `(&1 / (&1 - t2) * t1) = t1 / (&1 - t2)` (C SUBGOAL_THEN SUBST1_TAC);
1115 BY(VECTOR_ARITH_TAC)
1120 let CONTINUOUS_LIFT_DOT2 = prove
1121 (`!net f:A->real^N g.
1122 f continuous net /\ g continuous net
1123 ==> (\x. lift(f x dot g x)) continuous net`,
1124 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP (MATCH_MP (REWRITE_RULE
1125 [TAUT `p /\ q /\ r ==> s <=> r ==> p /\ q ==> s`]
1126 BILINEAR_CONTINUOUS_COMPOSE) BILINEAR_DOT)) THEN REWRITE_TAC[]);;
1128 let REAL_CONTINUOUS_AT_DOT2 = prove_by_refinement(
1129 `!(f:real->real^A) g x. f continuous atreal x /\ g continuous atreal x
1130 ==> (\x. (f x dot g x)) real_continuous atreal x`,
1133 REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1];
1134 REPEAT WEAKER_STRIP_TAC;
1135 TYPIFY `lift o (\x. f x dot g x) = (\x. lift (f x dot g x))` (C SUBGOAL_THEN SUBST1_TAC);
1136 BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]);
1137 INTRO_TAC CONTINUOUS_AT_LIFT_DOT2 [`f o drop`;`g o drop`;`lift x`];
1138 TYPIFY `(\x. lift ((f o drop) x dot (g o drop) x)) = (\x. lift (f x dot g x)) o drop` (C SUBGOAL_THEN SUBST1_TAC);
1139 BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]);
1140 BY(ASM_REWRITE_TAC[GSYM (* Xbjrphc. *) CONTINUOUS_CONTINUOUS_ATREAL])
1145 let REAL_CONTINUOUS_AT_DOT2 = prove_by_refinement(
1146 `!(f:real->real^A) g x. f continuous atreal x /\ g continuous atreal x
1147 ==> (\x. (f x dot g x)) real_continuous atreal x`,
1150 REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS1];
1151 REPEAT WEAKER_STRIP_TAC;
1152 TYPIFY `lift o (\x. f x dot g x) = (\x. lift (f x dot g x))` (C SUBGOAL_THEN SUBST1_TAC);
1153 BY(REWRITE_TAC[FUN_EQ_THM;o_DEF]);
1154 MATCH_MP_TAC CONTINUOUS_LIFT_DOT2;
1159 let azim_pos_open = prove_by_refinement(
1160 `!v2 v3 v4 t a b. (!x. x IN real_interval (a,b) ==> v2 continuous (atreal x)) /\
1161 (!x. x IN real_interval (a,b) ==> v3 continuous (atreal x)) /\
1162 (!x. x IN real_interval (a,b) ==> v4 continuous (atreal x)) /\
1163 t IN real_interval(a,b) /\
1164 ~collinear {(vec 0) ,(v2 t) ,(v3 t)} /\ ~collinear {(vec 0), (v2 t), (v4 t)} /\
1165 ~(azim (vec 0) (v2 t) (v3 t) (v4 t) = &0) ==>
1166 (?e. &0 < e /\ (!t'. abs(t' - t) < e ==> ~(azim (vec 0) (v2 t') (v3 t') (v4 t') = &0)))
1170 REWRITE_TAC[real_open;IN_ELIM_THM];
1171 REPEAT WEAKER_STRIP_TAC;
1172 INTRO_TAC (GEN_ALL NONCOLLINEAR_OPEN ) [`t`;`(vec 0):real^3`;`v2`;`v3`];
1174 BY(ASM_MESON_TAC[]);
1175 REPEAT WEAKER_STRIP_TAC;
1176 INTRO_TAC (GEN_ALL NONCOLLINEAR_OPEN ) [`t`;`(vec 0):real^3`;`v2`;`v4`];
1178 BY(ASM_MESON_TAC[]);
1179 REPEAT WEAKER_STRIP_TAC;
1180 INTRO_TAC azim_0_as_closed [`v2 t`;`v3 t`;`v4 t`];
1181 ASM_REWRITE_TAC[DE_MORGAN_THM];
1183 TYPIFY `?e. &0 < e /\ (!t'. abs(t - t') < e ==> (~coplanar {vec 0, v2 t', v3 t', v4 t'} \/ ~(&0 <= ((v2 t' cross v3 t') cross v2 t') dot v4 t')))` (C SUBGOAL_THEN MP_TAC);
1184 FIRST_X_ASSUM DISJ_CASES_TAC;
1185 INTRO_TAC NONPLANAR_OPEN [`\(t:real). ((vec 0):real^3)`;`v2`;`v3`;`v4`;`t`];
1187 ASM_REWRITE_TAC[CONTINUOUS_CONST];
1188 BY(ASM_MESON_TAC[]);
1191 TYPIFY `(\t. ((v2 t cross v3 t) cross v2 t) dot -- (v4 t)) real_continuous_on ( real_interval(a,b) )` (C SUBGOAL_THEN ASSUME_TAC);
1192 GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT;
1193 REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL];
1194 REPEAT WEAKER_STRIP_TAC;
1195 MATCH_MP_TAC REAL_CONTINUOUS_AT_DOT2;
1197 MATCH_MP_TAC CONTINUOUS_NEG;
1198 BY(ASM_MESON_TAC[]);
1199 MATCH_MP_TAC (* Xbjrphc. *)CONTINUOUS_CROSS;
1201 BY(ASM_MESON_TAC[]);
1202 MATCH_MP_TAC (* Xbjrphc. *)CONTINUOUS_CROSS;
1203 BY(ASM_MESON_TAC[]);
1204 INTRO_TAC Pent_hex.continuous_preimage_open [`(\x. ((v2 x cross v3 x) cross v2 x) dot -- v4 x)`;`real_interval(a,b)`;`{u | &0 < u}`];
1206 ASM_REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL];
1207 BY(REWRITE_TAC[REAL_OPEN_HALFSPACE_GT;arith ` &0 < x <=> x > &0`]);
1208 REWRITE_TAC[IN_ELIM_THM];
1209 REWRITE_TAC[real_open;DOT_RNEG;arith `&0 < -- x <=> ~(&0 <= x)`;IN_ELIM_THM];
1210 DISCH_THEN (C INTRO_TAC [`t`]);
1212 BY(ASM_REWRITE_TAC[]);
1213 BY(MESON_TAC[arith `abs (x' - t) < e <=> abs (t - x') < e`]);
1214 REPEAT WEAKER_STRIP_TAC;
1215 TYPIFY `?e'''. e''' <= e /\ e''' <= e' /\ e''' <= e'' /\ &0 < e'''` (C SUBGOAL_THEN MP_TAC);
1216 TYPIFY `if (e'' <= e' /\ e'' <= e) then e'' else (if (e' <= e'' /\ e' <= e) then e' else e)` EXISTS_TAC;
1217 BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC) THEN REAL_ARITH_TAC);
1218 REPEAT WEAKER_STRIP_TAC;
1219 TYPIFY `e'''` EXISTS_TAC;
1223 GMATCH_SIMP_TAC azim_0_as_closed;
1224 REWRITE_TAC[DE_MORGAN_THM];
1225 BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_TAC THEN TRY REAL_ARITH_TAC)
1229 let azim_real_continuous_on = prove_by_refinement(
1231 (!x. x IN real_interval (a,b) ==> v2 continuous (atreal x)) /\
1232 (!x. x IN real_interval (a,b) ==> v3 continuous (atreal x)) /\
1233 (!x. x IN real_interval (a,b) ==> v4 continuous (atreal x)) /\
1234 t IN real_interval(a,b) /\
1235 ~collinear {(vec 0) ,(v2 t) ,(v3 t)} /\ ~collinear {(vec 0), (v2 t), (v4 t)} /\
1236 ~(azim (vec 0) (v2 t) (v3 t) (v4 t) = &0) ==>
1237 (?e. &0 < e /\ (\q. azim (vec 0) (v2 q) (v3 q) (v4 q)) real_continuous_on (real_interval (t - e, t+ e)))`,
1240 REPEAT WEAKER_STRIP_TAC;
1241 INTRO_TAC (GEN_ALL NONCOLLINEAR_OPEN) [`t`;`(vec 0):real^3`;`v2`;`v3`];
1243 BY(ASM_REWRITE_TAC[] THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
1244 REPEAT WEAKER_STRIP_TAC;
1245 INTRO_TAC (GEN_ALL NONCOLLINEAR_OPEN) [`t`;`(vec 0):real^3`;`v2`;`v4`];
1247 BY(ASM_REWRITE_TAC[] THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
1248 REPEAT WEAKER_STRIP_TAC;
1249 INTRO_TAC azim_pos_open [`v2`;`v3`;`v4`;`t`;`a`;`b`];
1251 BY(ASM_REWRITE_TAC[]);
1252 REPEAT WEAKER_STRIP_TAC;
1253 TYPIFY `?e'''. &0 < e''' /\ (!x. t - e''' < x /\ x < t + e''' ==> x IN real_interval (a,b))` (C SUBGOAL_THEN MP_TAC);
1254 TYPIFY `if (b-t <= t -a) then b - t else t - a` EXISTS_TAC;
1255 FIRST_X_ASSUM_ST `IN` MP_TAC;
1256 REWRITE_TAC[IN_REAL_INTERVAL];
1258 REPEAT WEAKER_STRIP_TAC;
1259 TYPIFY `?e''''. e'''' <= e /\ e'''' <= e' /\ e'''' <= e'' /\ e'''' <= e''' /\ &0 < e''''` (C SUBGOAL_THEN MP_TAC);
1260 INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`{e,e',e'',e'''}`];
1263 BY(MESON_TAC[FINITE_RULES]);
1265 REPEAT WEAKER_STRIP_TAC;
1266 TYPIFY `m` EXISTS_TAC;
1267 RULE_ASSUM_TAC(REWRITE_RULE[IN_INSERT;NOT_IN_EMPTY]);
1268 REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN (REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC));
1270 REPEAT WEAKER_STRIP_TAC;
1271 TYPIFY `e''''` EXISTS_TAC;
1273 GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT;
1274 REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL;IN_REAL_INTERVAL];
1275 REPEAT WEAKER_STRIP_TAC;
1276 MATCH_MP_TAC (* Xbjrphc. *)REAL_CONTINUOUS_ATREAL_AZIM_COMPOSE;
1277 ASM_REWRITE_TAC[CONTINUOUS_CONST];
1278 GMATCH_SIMP_TAC (GSYM Local_lemmas.AZIM_EQ_0_GE_ALT2);
1279 TYPIFY `x IN real_interval (a,b)` (C SUBGOAL_THEN ASSUME_TAC);
1280 FIRST_X_ASSUM MATCH_MP_TAC;
1281 BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1282 BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN (REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC)) THEN TRY REAL_ARITH_TAC)
1286 let azim_pos_iff_nz = prove_by_refinement(
1288 &0 < azim v1 v2 v3 v4 <=> ~(azim v1 v2 v3 v4 = &0)`,
1291 BY(MESON_TAC[Counting_spheres.AZIM_NN;arith `&0 < x <=> (&0 <= x /\ ~(x = &0))`])
1295 (* was NHCXLRV_PREP *)
1297 let NHCXLRV = prove_by_refinement(
1299 deformation f {w0,w1,w2,v} (a,b) /\
1300 ~collinear {vec 0, f w1 (&0), f w2 (&0)} /\
1301 ~collinear {vec 0, f w1 (&0), f w0 (&0)} /\
1302 ~collinear {vec 0, f w1 (&0), f v (&0)} /\
1303 v IN wedge (vec 0) w1 w2 w0 ==>
1305 (!t. abs t < e ==> (f v t) IN wedge (vec 0) (f w1 t) (f w2 t) (f w0 t)))`,
1308 REWRITE_TAC[Reuhady.WEDGE_SIMPLE;IN_ELIM_THM;IN_INSERT;NOT_IN_EMPTY;Localization.deformation];
1309 REPEAT WEAKER_STRIP_TAC;
1310 TYPIFY `?c. azim (vec 0) w1 w2 v < c /\ c < azim (vec 0) w1 w2 w0` (C SUBGOAL_THEN MP_TAC);
1311 TYPIFY `(azim (vec 0) w1 w2 v + azim (vec 0) w1 w2 w0)/ &2` EXISTS_TAC;
1312 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1313 REPEAT WEAKER_STRIP_TAC;
1314 TYPIFY `(?e1. &0 < e1 /\ (!t. abs t < e1 ==> &0 < azim (vec 0) (f w1 t) (f w2 t) (f v t))) /\(?e2. &0 < e2 /\ (!t. abs t < e2 ==> azim (vec 0) (f w1 t) (f w2 t) (f v t) < c)) /\ (?e3. &0 < e3 /\ (!t. abs t < e3 ==> c < azim (vec 0) (f w1 t) (f w2 t) (f w0 t)))` ENOUGH_TO_SHOW_TAC;
1315 REPEAT WEAKER_STRIP_TAC;
1316 TYPIFY `if (e1 <= e2 /\ e1 <= e3) then e1 else if (e2 <= e3 /\ e2 <= e1) then e2 else e3` EXISTS_TAC;
1318 BY(ASM_TAC THEN REAL_ARITH_TAC);
1319 REPEAT WEAKER_STRIP_TAC;
1321 FIRST_X_ASSUM MATCH_MP_TAC;
1322 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1323 MATCH_MP_TAC REAL_LT_TRANS;
1324 TYPIFY `c` EXISTS_TAC;
1325 BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
1326 INTRO_TAC azim_real_continuous_on [`f w1`;`f w2`;`f w0`;`&0`;`a`;`b`];
1328 ASM_REWRITE_TAC[GSYM azim_pos_iff_nz];
1329 FIRST_X_ASSUM_ST `\/` (REPEAT o GMATCH_SIMP_TAC);
1330 TYPIFY_GOAL_THEN `&0 < azim (vec 0) w1 w2 w0` (unlist REWRITE_TAC);
1331 BY(ASM_MESON_TAC[Counting_spheres.AZIM_NN;arith `&0 <= x /\ x < y ==> &0 < y`]);
1332 BY(REPEAT CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
1333 REPEAT WEAKER_STRIP_TAC;
1334 INTRO_TAC azim_real_continuous_on [`f w1`;`f w2`;`f v`;`&0`;`a`;`b`];
1336 ASM_REWRITE_TAC[GSYM azim_pos_iff_nz];
1337 FIRST_X_ASSUM_ST `\/` (REPEAT o GMATCH_SIMP_TAC);
1339 BY(REPEAT CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
1340 REPEAT WEAKER_STRIP_TAC;
1341 RULE_ASSUM_TAC (REWRITE_RULE[arith `&0 - e = -- e /\ &0 + e = e`]);
1342 INTRO_TAC Pent_hex.continuous_preimage_open [`(\q. azim (vec 0) (f w1 q) (f w2 q) (f v q))`;`real_interval (-- e',e')`;`{x | &0 < x}`];
1343 ASM_REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL;REAL_OPEN_HALFSPACE_GT;arith ` &0 < x <=> x > &0`];
1344 INTRO_TAC Pent_hex.continuous_preimage_open [`(\q. azim (vec 0) (f w1 q) (f w2 q) (f v q))`;`real_interval (-- e',e')`;`{x | x < c }`];
1345 ASM_REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL;REAL_OPEN_HALFSPACE_LT];
1346 INTRO_TAC Pent_hex.continuous_preimage_open [`(\q. azim (vec 0) (f w1 q) (f w2 q) (f w0 q))`;`real_interval (-- e,e)`;`{x | c < x}`];
1347 ASM_REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL;REAL_OPEN_HALFSPACE_GT;arith ` c < x <=> x > c`];
1348 REWRITE_TAC[IN_REAL_INTERVAL;IN_ELIM_THM;real_open];
1349 REWRITE_TAC[arith `x > c <=> c < x`];
1350 REPEAT (DISCH_THEN (C INTRO_TAC [`&0`]) THEN (FIRST_ASSUM_ST `\/` (REPEAT o GMATCH_SIMP_TAC)) THEN ASM_SIMP_TAC[arith `&0 < e ==> -- e < &0`] THEN DISCH_TAC);
1351 RULE_ASSUM_TAC (REWRITE_RULE[arith `x - &0 = x`]);
1356 let NHCXLRV_ALT = prove_by_refinement(
1358 deformation f {w0, w1, w2, v} (a,b) /\
1359 ~collinear {vec 0, w1, w2} /\
1360 ~collinear {vec 0, w1, w0} /\
1361 ~collinear {vec 0, w1, v} /\
1362 v IN wedge (vec 0) w1 w2 w0
1365 ==> f v t IN wedge (vec 0) (f w1 t) (f w2 t) (f w0 t)))`,
1368 REPEAT WEAKER_STRIP_TAC;
1369 MATCH_MP_TAC NHCXLRV;
1370 GEXISTL_TAC [`a`;`b`];
1372 TYPIFY `!u. u IN {w0,w1,w2,v} ==> f u (&0) = u` (C SUBGOAL_THEN ASSUME_TAC);
1373 RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation]);
1374 ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
1375 FIRST_X_ASSUM MATCH_MP_TAC;
1376 BY(ASM_REWRITE_TAC[]);
1377 FIRST_X_ASSUM (REPEAT o GMATCH_SIMP_TAC);
1383 let WNWSHJT = prove_by_refinement(
1385 deformation f {w0,w1,w2} (a,b) /\
1386 ~collinear {vec 0, f w1 (&0), f w2 (&0)} /\
1387 ~collinear {vec 0, f w1 (&0), f w0 (&0)} /\
1388 &0 < azim (vec 0) w1 w2 w0 /\
1389 azim (vec 0) w1 w2 w0 < pi ==>
1391 (!t. abs t < e ==> azim (vec 0) (f w1 t) (f w2 t) (f w0 t) < pi))`,
1394 REWRITE_TAC[IN_ELIM_THM;IN_INSERT;NOT_IN_EMPTY;Localization.deformation];
1395 REPEAT WEAKER_STRIP_TAC;
1396 INTRO_TAC azim_real_continuous_on [`f w1`;`f w2`;`f w0`;`&0`;`a`;`b`];
1398 ASM_REWRITE_TAC[GSYM azim_pos_iff_nz];
1399 FIRST_X_ASSUM_ST `\/` (REPEAT o GMATCH_SIMP_TAC);
1401 BY(REPEAT CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
1402 REPEAT WEAKER_STRIP_TAC;
1403 RULE_ASSUM_TAC (REWRITE_RULE[arith `&0 - e = -- e /\ &0 + e = e`]);
1404 INTRO_TAC Pent_hex.continuous_preimage_open [`(\q. azim (vec 0) (f w1 q) (f w2 q) (f w0 q))`;`real_interval (-- e,e)`;`{x | x < pi}`];
1405 ASM_REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL;REAL_OPEN_HALFSPACE_LT];
1406 REWRITE_TAC[IN_REAL_INTERVAL;IN_ELIM_THM;real_open];
1407 REPEAT (DISCH_THEN (C INTRO_TAC [`&0`]) THEN (FIRST_ASSUM_ST `\/` (REPEAT o GMATCH_SIMP_TAC)) THEN ASM_SIMP_TAC[arith `&0 < e ==> -- e < &0`] THEN DISCH_TAC);
1408 RULE_ASSUM_TAC (REWRITE_RULE[arith `x - &0 = x`]);
1413 let LOFA_IMP_INANGLE_EQ_AZIM = prove_by_refinement
1414 (`!V E FF v. local_fan (V,E,FF) /\ v IN V ==> interior_angle1 (vec 0) FF v = azim_in_fan (v, rho_node1 FF v) E `,
1416 REWRITE_TAC[Localization.convex_local_fan; Local_lemmas.azim_in_fan2];
1418 ASSUME_TAC2 Local_lemmas.EXISTS_INVERSE_OF_V;
1419 DOWN THEN STRIP_TAC;
1420 ASSUME_TAC2 Local_lemmas.LOFA_IMP_EE_TWO_ELMS;
1421 ASSUME_TAC2 Local_lemmas.LOFA_CARD_EE_V_1;
1422 ASSUME_TAC2 Lunar_deform.LOCAL_FAN_RHO_NODE_PROS2;
1423 DOWN THEN STRIP_TAC;
1424 UNDISCH_TAC` v:real^3 IN V `;
1427 SWITCH_TAC` EE v E = {rho_node1 FF v, vv} `;
1428 ASM_SIMP_TAC[ARITH_RULE` a = 2 ==> a > 1 `];
1430 DOWN THEN DOWN THEN PHA;
1431 ASSUME_TAC2 (SPEC `vv:real^3 ` (GEN` v:real^3 ` Local_lemmas.IVS_RHO_IDD));
1434 UNDISCH_TAC` {rho_node1 FF v, vv} = EE v E `;
1435 DISCH_THEN (SUBST1_TAC o SYM);
1438 BY(SIMP_TAC[Local_lemmas.interior_angle1; GSYM Local_lemmas.ivs_rho_node1; Local_lemmas.AZIM_CYCLE_TWO_POINT_SET])
1441 let deformation_rho_node1_equivariant1 = prove_by_refinement(
1443 deformation f V (a,b) /\
1444 local_fan (V,E,FF) /\
1446 (IMAGE (\v. f v t) V,
1447 IMAGE (\s. IMAGE (\v. f v t) s) E,
1448 IMAGE (\ (u,v). f u t,f v t) FF) /\
1450 f (rho_node1 FF v) t = rho_node1 (IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t)`,
1453 REPEAT WEAKER_STRIP_TAC;
1454 MATCH_MP_TAC EQ_SYM;
1455 MATCH_MP_TAC (GEN_ALL Local_lemmas.DETER_RHO_NODE);
1456 GEXISTL_TAC [`IMAGE (\v. f v t) V`;` IMAGE (\s. IMAGE (\v. f v t) s) E`];
1458 TYPIFY `IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` ENOUGH_TO_SHOW_TAC;
1459 DISCH_THEN (SUBST1_TAC o GSYM);
1460 BY(ASM_REWRITE_TAC[]);
1461 BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]);
1462 REWRITE_TAC[IN_IMAGE;EXISTS_PAIR_THM];
1463 GEXISTL_TAC [`v`;`rho_node1 FF v`];
1465 BY(ASM_MESON_TAC[Lunar_deform.LOCAL_FAN_RHO_NODE_PROS2])
1469 let deformation_ivs_rho_node1_equivariant1 = prove_by_refinement(
1471 deformation f V (a,b) /\
1472 local_fan (V,E,FF) /\
1474 (IMAGE (\v. f v t) V,
1475 IMAGE (\s. IMAGE (\v. f v t) s) E,
1476 IMAGE (\ (u,v). f u t,f v t) FF) /\
1478 f (ivs_rho_node1 FF v) t = ivs_rho_node1 (IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t)`,
1481 REPEAT WEAKER_STRIP_TAC;
1482 MATCH_MP_TAC EQ_SYM;
1483 MATCH_MP_TAC (GEN_ALL Local_lemmas.IVS_RHO_NODE1_DETE);
1484 GEXISTL_TAC [`IMAGE (\v. f v t) V`;` IMAGE (\s. IMAGE (\v. f v t) s) E`];
1486 TYPIFY `IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` ENOUGH_TO_SHOW_TAC;
1487 DISCH_THEN (SUBST1_TAC o GSYM);
1488 BY(ASM_REWRITE_TAC[]);
1489 BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]);
1490 REWRITE_TAC[IN_IMAGE;EXISTS_PAIR_THM];
1491 GEXISTL_TAC [`ivs_rho_node1 FF v`;`v`];
1493 BY(ASM_MESON_TAC[Lunar_deform.IVS_RHO_NODE_V_IN_FF])
1497 let deformation_rho_node1_equivariant = prove_by_refinement(
1499 deformation f V (a,b) /\
1500 local_fan (V,E,FF) /\
1503 (!t. abs t < e ==> f (rho_node1 FF v) t = rho_node1 (IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t)))`,
1506 REPEAT WEAKER_STRIP_TAC;
1507 INTRO_TAC (GEN_ALL Lunar_deform.XRECQNS_UPDATE) [`a`;`b`;`V`;`E`;`f`;`FF`];
1509 REPEAT WEAKER_STRIP_TAC;
1510 TYPIFY `e` EXISTS_TAC;
1512 REPEAT WEAKER_STRIP_TAC;
1513 FIRST_X_ASSUM (C INTRO_TAC [`t`]);
1515 BY(ASM_MESON_TAC[deformation_rho_node1_equivariant1])
1519 let deformation_subset = prove_by_refinement(
1520 `!f U V a b. U SUBSET V /\ deformation f V (a,b) ==> deformation f U (a,b)`,
1523 REWRITE_TAC[Localization.deformation;SUBSET];
1528 let EXISTS_TRIPLE_THM = prove_by_refinement(
1529 `!P. (?p1 p2 p3. P p1 p2 p3) <=> (?x. P (FST x) (FST (SND x)) (SND (SND x)))`,
1532 BY(REWRITE_TAC[EXISTS_PAIR_THM])
1536 let zlz_reduction = prove_by_refinement(
1538 convex_local_fan (V,E,FF) /\
1540 deformation f V (a,b) /\
1541 (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==>
1542 interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi) /\
1544 ?e4. v,w IN FF /\ u IN V
1546 (!t. --e4 < t /\ t < e4
1547 ==> aff_ge {vec 0} {f v t, f w t} INTER
1548 aff_lt {vec 0} {f u t} =
1552 (!t. --e3 < t /\ t < e3
1553 ==> IMAGE (\v. f v t) V SUBSET
1554 wedge_in_fan_ge (f (FST x) t,f (SND x) t)
1555 (IMAGE (IMAGE (\v. f v t)) E))) /\
1558 (!t. --e2 < t /\ t < e2
1559 ==> azim_in_fan (f (FST x) t,f (SND x) t)
1560 (IMAGE (IMAGE (\v. f v t)) E) <=
1563 (!t. --e < t /\ t < e
1564 ==> convex_local_fan
1565 (IMAGE (\v. f v t) V,
1566 IMAGE (IMAGE (\v. f v t)) E,
1567 IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) /\
1568 generic (IMAGE (\v. f v t) V)
1569 (IMAGE (IMAGE (\v. f v t)) E)))`,
1572 REPEAT WEAKER_STRIP_TAC;
1573 REWRITE_TAC[Localization.convex_local_fan];
1574 REWRITE_TAC[Localization.generic];
1575 COMMENT "preliminaries";
1576 TYPIFY `!t. IMAGE (\s. IMAGE (\v. f v t) s) E = IMAGE (IMAGE (\v. f v t)) E /\ IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` (C SUBGOAL_THEN ASSUME_TAC);
1577 BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]);
1578 INTRO_TAC (GEN_ALL Local_lemmas.CVX_LO_IMP_LO) [`V`;`E`;`FF`];
1581 TYPIFY `FINITE FF` (C SUBGOAL_THEN ASSUME_TAC);
1582 MATCH_MP_TAC Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF;
1583 BY(ASM_REWRITE_TAC[]);
1584 TYPIFY `~(FF = {})` (C SUBGOAL_THEN ASSUME_TAC);
1585 MATCH_MP_TAC Polar_fan.LOCAL_FAN_NOT_EMPTY_FF;
1586 BY(ASM_MESON_TAC[]);
1587 TYPIFY `(?e1. &0 < e1 /\ (!t. --e1 < t /\ t < e1 ==> (local_fan (IMAGE (\v. f v t) V, IMAGE (IMAGE (\v. f v t)) E, IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF)))) /\ (?e2. &0 < e2 /\ (!t. --e2 < t /\ t < e2 ==> ((!x. x IN IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF ==> azim_in_fan x (IMAGE (IMAGE (\v. f v t)) E) <= pi)))) /\ (?e3. &0 < e3 /\ (!t. --e3 < t /\ t < e3 ==> (!x. x IN IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF ==> IMAGE (\v. f v t) V SUBSET wedge_in_fan_ge x (IMAGE (IMAGE (\v. f v t)) E)))) /\ (?e4. &0 < e4 /\ (!t. --e4 < t /\ t < e4 ==> (!v w u. {v, w} IN IMAGE (IMAGE (\v. f v t)) E /\ u IN IMAGE (\v. f v t) V ==> aff_ge {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {})))` ENOUGH_TO_SHOW_TAC;
1588 REPEAT WEAKER_STRIP_TAC;
1589 TYPIFY `?e. e <= e1 /\ e <= e2 /\ e <= e3 /\ e <= e4 /\ &0 < e` (C SUBGOAL_THEN MP_TAC);
1590 INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`{e1,e2,e3,e4}`];
1593 BY(MESON_TAC[FINITE_RULES]);
1595 REPEAT WEAKER_STRIP_TAC;
1596 TYPIFY `m` EXISTS_TAC;
1597 RULE_ASSUM_TAC(REWRITE_RULE[IN_INSERT;NOT_IN_EMPTY]);
1598 REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN (REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC));
1600 REPEAT WEAKER_STRIP_TAC;
1601 TYPIFY `e` EXISTS_TAC;
1602 BY(ASM_MESON_TAC[arith `-- e < t /\ t < e /\ e <= e' ==> (-- e' < t /\ t < e')`]);
1603 COMMENT "local_fan";
1605 INTRO_TAC (GEN_ALL Lunar_deform.XRECQNS_UPDATE) [`a`;`b`;`V`;`E`;`f`;`FF`];
1607 BY(ASM_REWRITE_TAC[]);
1608 REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`];
1609 REPEAT WEAKER_STRIP_TAC;
1610 TYPIFY `e` EXISTS_TAC;
1612 REPEAT WEAKER_STRIP_TAC;
1613 FIRST_X_ASSUM (C INTRO_TAC [`t`]);
1614 BY(ASM_REWRITE_TAC[]);
1616 COMMENT "skolemize all variables";
1617 COMMENT "angle <= pi";
1618 TYPIFY_GOAL_THEN `(!x. ?e2. x IN FF ==> ( &0 < e2 /\ (!t. --e2 < t /\ t < e2 ==> azim_in_fan ( (\uv. f (FST uv) t,f (SND uv) t) x) (IMAGE (IMAGE (\v. f v t)) E) <= pi))) ==> (?e2. &0 < e2 /\ (!t. --e2 < t /\ t < e2 ==> (!x. x IN IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF ==> azim_in_fan x (IMAGE (IMAGE (\v. f v t)) E) <= pi)))` GMATCH_SIMP_TAC;
1619 REWRITE_TAC[SKOLEM_THM];
1620 REPEAT WEAKER_STRIP_TAC;
1621 TYPIFY `?e. &0 < e /\ (!x. x IN FF ==> e <= e2 x)` (C SUBGOAL_THEN MP_TAC);
1622 INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`IMAGE e2 FF`];
1625 (MATCH_MP_TAC FINITE_IMAGE);
1626 BY(ASM_REWRITE_TAC[]);
1627 (MATCH_MP_TAC Fatugpd.NOT_EMPTY_IMAGE);
1628 BY(ASM_REWRITE_TAC[]);
1629 REPEAT WEAKER_STRIP_TAC;
1630 TYPIFY `m` EXISTS_TAC;
1631 REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC);
1632 REWRITE_TAC[EXTENSION;NOT_IN_EMPTY];
1633 REWRITE_TAC[IN_IMAGE];
1635 REPEAT WEAKER_STRIP_TAC;
1636 TYPIFY `e` EXISTS_TAC;
1638 REPEAT WEAKER_STRIP_TAC;
1639 FIRST_X_ASSUM MP_TAC;
1640 REWRITE_TAC[IN_IMAGE;EXISTS_PAIR_THM];
1641 REPEAT WEAKER_STRIP_TAC;
1642 REPEAT (FIRST_X_ASSUM (C INTRO_TAC [`p1,p2`]));
1646 FIRST_X_ASSUM_ST `IMAGE` MP_TAC;
1648 REPEAT WEAKER_STRIP_TAC;
1649 FIRST_X_ASSUM (C INTRO_TAC [`t`]);
1651 BY(ASM_TAC THEN REAL_ARITH_TAC);
1653 COMMENT "skolemize wedge_in_fan";
1654 TYPIFY_GOAL_THEN `(!x. ?e3. x IN FF ==> &0 < e3 /\ (!t. --e3 < t /\ t < e3 ==> (IMAGE (\v. f v t) V SUBSET wedge_in_fan_ge (f (FST x) t, f (SND x) t) (IMAGE (IMAGE (\v. f v t)) E)))) ==> ( (?e3. &0 < e3 /\ (!t. --e3 < t /\ t < e3 ==> (!x. x IN IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF ==> IMAGE (\v. f v t) V SUBSET wedge_in_fan_ge x (IMAGE (IMAGE (\v. f v t)) E)))))` GMATCH_SIMP_TAC;
1655 REWRITE_TAC[SKOLEM_THM];
1656 REPEAT WEAKER_STRIP_TAC;
1657 TYPIFY `?e. &0 < e /\ (!x. x IN FF ==> e <= e3 x)` (C SUBGOAL_THEN MP_TAC);
1658 INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`IMAGE e3 FF`];
1661 (MATCH_MP_TAC FINITE_IMAGE);
1662 BY(ASM_REWRITE_TAC[]);
1663 (MATCH_MP_TAC Fatugpd.NOT_EMPTY_IMAGE);
1664 BY(ASM_REWRITE_TAC[]);
1665 REPEAT WEAKER_STRIP_TAC;
1666 TYPIFY `m` EXISTS_TAC;
1667 REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC);
1668 REWRITE_TAC[EXTENSION;NOT_IN_EMPTY];
1669 REWRITE_TAC[IN_IMAGE];
1671 REPEAT WEAKER_STRIP_TAC;
1672 TYPIFY `e` EXISTS_TAC;
1674 REPEAT WEAKER_STRIP_TAC;
1675 FIRST_X_ASSUM MP_TAC;
1676 REWRITE_TAC[IN_IMAGE;EXISTS_PAIR_THM];
1677 REPEAT WEAKER_STRIP_TAC;
1678 REPEAT (FIRST_X_ASSUM (C INTRO_TAC [`p1,p2`]));
1682 FIRST_X_ASSUM_ST `IMAGE` MP_TAC;
1684 REPEAT WEAKER_STRIP_TAC;
1685 FIRST_X_ASSUM (C INTRO_TAC [`t`]);
1687 BY(ASM_TAC THEN REAL_ARITH_TAC);
1689 TYPIFY_GOAL_THEN `(!u v w. ?e4. (v,w) IN FF /\ u IN V ==> &0 < e4 /\ (!t. --e4 < t /\ t < e4 ==> aff_ge {vec 0} {f v t, f w t} INTER aff_lt {vec 0} {f u t} = {})) ==> (?e4. &0 < e4 /\ (!t. --e4 < t /\ t < e4 ==> (!v w u. {v, w} IN IMAGE (IMAGE (\v. f v t)) E /\ u IN IMAGE (\v. f v t) V ==> aff_ge {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {}))) ` GMATCH_SIMP_TAC;
1690 REWRITE_TAC[SKOLEM_THM];
1691 REPEAT WEAKER_STRIP_TAC;
1692 TYPIFY `?e. &0 < e /\ (!u v w. (u,(v,w)) IN V CROSS FF ==> e <= e4 u v w)` (C SUBGOAL_THEN MP_TAC);
1693 INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`IMAGE (\ x. e4 (FST x) (FST (SND x)) (SND(SND x))) (V CROSS FF)`];
1696 (MATCH_MP_TAC FINITE_IMAGE);
1697 MATCH_MP_TAC FINITE_CROSS;
1699 BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_FINITE_V]);
1700 (MATCH_MP_TAC Fatugpd.NOT_EMPTY_IMAGE);
1701 REWRITE_TAC[CROSS_EQ_EMPTY];
1703 BY(ASM_MESON_TAC[Local_lemmas.LOFA_V_NOT_EMP]);
1704 REPEAT WEAKER_STRIP_TAC;
1705 TYPIFY `m` EXISTS_TAC;
1706 REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC);
1707 REWRITE_TAC[EXTENSION;NOT_IN_EMPTY];
1708 REWRITE_TAC[IN_IMAGE];
1709 REWRITE_TAC[EXISTS_PAIR_THM];
1710 REPEAT WEAKER_STRIP_TAC;
1711 FIRST_X_ASSUM (C INTRO_TAC [`p1`;`p1'`;`p2`]);
1713 RULE_ASSUM_TAC(REWRITE_RULE[IN_CROSS]);
1714 BY(ASM_REWRITE_TAC[]);
1715 (REPEAT WEAKER_STRIP_TAC);
1717 TYPIFY `m = e4 p1 p1' p2` UNDISCH_TAC;
1718 DISCH_THEN (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
1719 REPEAT WEAKER_STRIP_TAC;
1720 FIRST_X_ASSUM MATCH_MP_TAC;
1721 BY(ASM_MESON_TAC[IN_CROSS]);
1722 REPEAT WEAKER_STRIP_TAC;
1723 TYPIFY `e` EXISTS_TAC;
1725 REPEAT WEAKER_STRIP_TAC;
1726 FIRST_X_ASSUM MP_TAC;
1727 REWRITE_TAC[IN_IMAGE;EXISTS_PAIR_THM];
1728 REPEAT WEAKER_STRIP_TAC;
1729 FIRST_X_ASSUM_ST `IMAGE` MP_TAC;
1730 REWRITE_TAC[IN_IMAGE];
1731 REPEAT WEAKER_STRIP_TAC;
1732 TYPIFY `?v' w'. x' = {v',w'}` (C SUBGOAL_THEN MP_TAC);
1733 TYPIFY `graph E` (C SUBGOAL_THEN ASSUME_TAC);
1734 BY(ASM_MESON_TAC[Fan_defs.FAN;Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN]);
1735 RULE_ASSUM_TAC(REWRITE_RULE[Fan_defs.graph]);
1736 TYPIFY`x' HAS_SIZE 2` (C SUBGOAL_THEN ASSUME_TAC);
1737 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[IN]);
1738 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[Local_lemmas1.HAS_SIZE_2_EXISTS2]);
1739 REPEAT WEAKER_STRIP_TAC;
1740 FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
1741 FIRST_X_ASSUM_ST `IMAGE` MP_TAC;
1742 REWRITE_TAC[SET_RULE `IMAGE f {u,v} = {f u,f v}`];
1743 DISCH_THEN ( SUBST1_TAC );
1745 TYPIFY `?v'' w''. {v',w'} = {v'',w''} /\ (v'',w'') IN FF` (C SUBGOAL_THEN MP_TAC);
1746 BY(ASM_MESON_TAC[Local_lemmas.LOFA_IN_E_IMP_IN_FF;SET_RULE `{a,b} = {b,a}`]);
1747 REPEAT WEAKER_STRIP_TAC;
1748 TYPIFY `{f v' t,f w' t} = {f v'' t,f w'' t}` (C SUBGOAL_THEN SUBST1_TAC);
1749 FIRST_X_ASSUM_ST `{a,b}` MP_TAC;
1750 REWRITE_TAC[Collect_geom.PAIR_EQ_EXPAND];
1752 FIRST_X_ASSUM (C INTRO_TAC [`x`;`v''`;`w''`]);
1753 REWRITE_TAC[IN_CROSS];
1756 FIRST_X_ASSUM (C INTRO_TAC [`x`;`v''`;`w''`]);
1758 REPEAT WEAKER_STRIP_TAC;
1759 FIRST_X_ASSUM MATCH_MP_TAC;
1760 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1761 BY(ASM_REWRITE_TAC[])
1765 let real_interval_contains_0_ball = prove_by_refinement(
1766 `!a b e1. a < &0 /\ &0 < b /\ &0 < e1 ==> (?e. &0 < e /\ e <= e1 /\ (!t. abs t < e ==> t IN real_interval (a,b)))`,
1769 REPEAT WEAKER_STRIP_TAC;
1770 TYPIFY `if (b <= -- a) /\ b <= e1 then b else (if e1 <= b /\ e1 <= --a then e1 else -- a)` EXISTS_TAC;
1771 REWRITE_TAC[IN_REAL_INTERVAL];
1772 ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
1774 BY(ASM_TAC THEN REAL_ARITH_TAC);
1776 BY(ASM_TAC THEN REAL_ARITH_TAC);
1782 let zlz_azim = prove_by_refinement(
1784 convex_local_fan (V,E,FF) /\
1786 deformation f V (a,b) /\
1787 (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==>
1788 interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi) ==>
1791 (!t. --e2 < t /\ t < e2
1792 ==> azim_in_fan (f (FST x) t,f (SND x) t)
1793 (IMAGE (IMAGE (\v. f v t)) E) <=
1797 REWRITE_TAC[Localization.convex_local_fan];
1798 REWRITE_TAC[Localization.generic];
1799 REPEAT WEAKER_STRIP_TAC;
1800 COMMENT "preliminaries";
1801 TYPIFY `!t. IMAGE (\s. IMAGE (\v. f v t) s) E = IMAGE (IMAGE (\v. f v t)) E /\ IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` (C SUBGOAL_THEN ASSUME_TAC);
1802 BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]);
1803 INTRO_TAC (GEN_ALL Local_lemmas.CVX_LO_IMP_LO) [`V`;`E`;`FF`];
1805 TYPIFY `FINITE FF` (C SUBGOAL_THEN ASSUME_TAC);
1806 MATCH_MP_TAC Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF;
1807 BY(ASM_REWRITE_TAC[]);
1808 TYPIFY `~(FF = {})` (C SUBGOAL_THEN ASSUME_TAC);
1809 MATCH_MP_TAC Polar_fan.LOCAL_FAN_NOT_EMPTY_FF;
1810 BY(ASM_MESON_TAC[]);
1811 COMMENT "local_fan";
1812 INTRO_TAC (GEN_ALL Lunar_deform.XRECQNS_UPDATE) [`a`;`b`;`V`;`E`;`f`;`FF`];
1813 ASM_REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`];
1814 REPEAT WEAKER_STRIP_TAC;
1815 COMMENT "restart here";
1816 TYPIFY `?p1 p2. (x = p1,p2)` (C SUBGOAL_THEN MP_TAC);
1817 BY(REWRITE_TAC[PAIR_SURJECTIVE]);
1818 REPEAT WEAKER_STRIP_TAC;
1819 ASM_REWRITE_TAC[FST;SND];
1820 FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
1821 REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
1823 TYPIFY `p1 IN V` (C SUBGOAL_THEN ASSUME_TAC);
1824 BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V]);
1825 TYPIFY `p2 = rho_node1 FF p1` (C SUBGOAL_THEN ASSUME_TAC);
1826 MATCH_MP_TAC EQ_SYM;
1827 MATCH_MP_TAC Local_lemmas.DETER_RHO_NODE;
1828 BY(ASM_REWRITE_TAC[]);
1829 TYPIFY `interior_angle1 (vec 0) FF p1 = azim_in_fan (p1,p2) E` (C SUBGOAL_THEN ASSUME_TAC);
1830 INTRO_TAC LOFA_IMP_INANGLE_EQ_AZIM [`V`;`E`;`FF`;`p1`];
1831 BY(ASM_MESON_TAC[]);
1832 TYPIFY `?e2. &0 < e2 /\ e2 <= e /\ (!t. abs t < e2 ==> t IN real_interval (a,b))` (C SUBGOAL_THEN MP_TAC);
1833 MATCH_MP_TAC real_interval_contains_0_ball;
1834 RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_REAL_INTERVAL]);
1835 BY(ASM_REWRITE_TAC[]);
1836 REPEAT WEAKER_STRIP_TAC;
1837 COMMENT "first case";
1838 TYPIFY `interior_angle1 (vec 0) FF p1 = pi` ASM_CASES_TAC;
1839 TYPIFY `e2` EXISTS_TAC;
1841 REPEAT WEAKER_STRIP_TAC;
1842 COMMENT "new insert";
1843 TYPIFY `local_fan (IMAGE (\v. f v t) V, IMAGE (IMAGE (\v. f v t)) E, IMAGE (\uv. f (FST uv) (t),f (SND uv) (t)) FF) /\ f p1 (t) IN IMAGE (\v. f v t) V` (C SUBGOAL_THEN ASSUME_TAC);
1846 FIRST_X_ASSUM MATCH_MP_TAC;
1847 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1848 REWRITE_TAC[IN_IMAGE];
1849 TYPIFY `p1` EXISTS_TAC;
1850 BY(ASM_REWRITE_TAC[]);
1851 GMATCH_SIMP_TAC deformation_rho_node1_equivariant1;
1853 GEXISTL_TAC [`a`;`b`;`E`;`V`];
1854 BY(ASM_REWRITE_TAC[]);
1855 INTRO_TAC (GSYM LOFA_IMP_INANGLE_EQ_AZIM) [`IMAGE (\v. f v t) V`;`IMAGE (IMAGE (\v. f v t)) E`;`IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF`;`f p1 t`];
1857 BY(ASM_REWRITE_TAC[]);
1860 FIRST_X_ASSUM MATCH_MP_TAC;
1863 FIRST_X_ASSUM MATCH_MP_TAC;
1864 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1865 BY(ASM_MESON_TAC[]);
1866 COMMENT "second case here";
1867 COMMENT "case azim < pi";
1868 TYPIFY `interior_angle1 (vec 0) FF p1 < pi` (C SUBGOAL_THEN ASSUME_TAC);
1869 RULE_ASSUM_TAC (REWRITE_RULE[Localization.convex_local_fan]);
1870 FIRST_X_ASSUM_ST `wedge_in_fan_ge` MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
1871 TYPIFY `interior_angle1 (vec 0) FF p1 <= pi` ENOUGH_TO_SHOW_TAC;
1872 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1874 BY(ASM_MESON_TAC[]);
1875 INTRO_TAC WNWSHJT [`ivs_rho_node1 FF p1`;`p1`;`p2`;`f`;`a`;`b`];
1877 REPEAT (GMATCH_SIMP_TAC (GSYM Local_lemmas1.AZIM_IN_FAN_RHOND_IVS_RHOND));
1878 TYPIFY `E` EXISTS_TAC;
1880 BY(ASM_MESON_TAC[]);
1883 MATCH_MP_TAC deformation_subset;
1884 TYPIFY `V` EXISTS_TAC;
1886 REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
1887 BY(ASM_MESON_TAC[Local_lemmas1.LOCAL_FAN_IVS_IN_V;Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V]);
1888 (GMATCH_SIMP_TAC deformation_rho_node1_equivariant1);
1889 GMATCH_SIMP_TAC deformation_ivs_rho_node1_equivariant1;
1891 GEXISTL_TAC [`a`;`b`;`E`;`V`];
1893 FIRST_X_ASSUM MATCH_MP_TAC;
1894 BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e1` MP_TAC) THEN REAL_ARITH_TAC);
1896 GEXISTL_TAC [`a`;`b`;`E`;`V`];
1898 FIRST_X_ASSUM MATCH_MP_TAC;
1899 BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e1` MP_TAC) THEN REAL_ARITH_TAC);
1900 TYPIFY `!v. v IN V ==> f v (&0) = v` (C SUBGOAL_THEN ASSUME_TAC);
1901 RULE_ASSUM_TAC (REWRITE_RULE[Localization.deformation]);
1902 BY(ASM_REWRITE_TAC[]);
1903 TYPIFY `f p1 (&0) = p1` (C SUBGOAL_THEN ASSUME_TAC);
1906 TYPIFY `IMAGE (\uv. f (FST uv) (&0),f (SND uv) (&0)) FF = FF` (C SUBGOAL_THEN SUBST1_TAC);
1907 REWRITE_TAC[IN_IMAGE;EXTENSION;EXISTS_PAIR_THM];
1909 INTRO_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V) [`E`;`FF`;`FST x`;`SND x`;`V`];
1912 TYPIFY `x IN FF` ASM_CASES_TAC;
1914 GEXISTL_TAC [ `FST x`;`SND x`];
1915 BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[PAIR;FST;SND]);
1917 REWRITE_TAC[NOT_EXISTS_THM];
1918 REPEAT WEAKER_STRIP_TAC;
1919 INTRO_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IMP_IN_V) [`E`;`FF`;`p1'`;`p2'`;`V`];
1921 BY(REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[PAIR;FST;SND]);
1922 TYPIFY `p1 IN V` (C SUBGOAL_THEN ASSUME_TAC);
1923 BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V]);
1925 BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]);
1927 BY(ASM_MESON_TAC[Local_lemmas.LOFA_IMP_NOT_COLL_IVS]);
1929 INTRO_TAC (GEN_ALL Local_lemmas.INTERIOR_ANGLE1_POS) [`E`;`V`;`FF`;`p1`];
1930 BY(ASM_REWRITE_TAC[]);
1931 BY(ASM_MESON_TAC[]);
1932 REPEAT WEAKER_STRIP_TAC;
1933 TYPIFY `(!t. abs t < e ==> azim_in_fan (f p1 t,f (rho_node1 FF p1) t) (IMAGE (IMAGE (\v. f v t)) E) = azim (vec 0) (f p1 t) (f (rho_node1 FF p1) t) (f (ivs_rho_node1 FF p1) t))` (C SUBGOAL_THEN MP_TAC);
1934 REPEAT WEAKER_STRIP_TAC;
1935 GMATCH_SIMP_TAC deformation_rho_node1_equivariant1;
1937 GEXISTL_TAC [`a`;`b`;`E`;`V`];
1938 (ASM_REWRITE_TAC[]);
1939 FIRST_X_ASSUM MATCH_MP_TAC;
1940 BY(ASM_REWRITE_TAC[]);
1941 GMATCH_SIMP_TAC Local_lemmas1.AZIM_IN_FAN_RHOND_IVS_RHOND;
1943 TYPIFY `IMAGE (\v. f v t) V` EXISTS_TAC;
1945 FIRST_X_ASSUM MATCH_MP_TAC;
1946 BY(ASM_REWRITE_TAC[]);
1947 REWRITE_TAC[IN_IMAGE];
1948 TYPIFY `p1` EXISTS_TAC;
1949 BY(ASM_REWRITE_TAC[]);
1950 GMATCH_SIMP_TAC deformation_ivs_rho_node1_equivariant1;
1951 GEXISTL_TAC [`a`;`b`;`E`;`V`];
1952 (ASM_REWRITE_TAC[]);
1953 FIRST_X_ASSUM MATCH_MP_TAC;
1954 BY(ASM_REWRITE_TAC[]);
1956 TYPIFY `if (e2 <= e') then e2 else e'` EXISTS_TAC;
1958 BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC) THEN REAL_ARITH_TAC);
1959 REPEAT WEAKER_STRIP_TAC;
1960 FIRST_X_ASSUM (C INTRO_TAC [`t`]);
1962 BY(REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
1963 DISCH_THEN SUBST1_TAC;
1964 MATCH_MP_TAC (arith `x < pi ==> x <= pi`);
1965 FIRST_X_ASSUM MATCH_MP_TAC;
1966 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC)
1970 let zlz_generic = prove_by_refinement(
1972 convex_local_fan (V,E,FF) /\
1974 deformation f V (a,b) ==>
1976 ?e4. v,w IN FF /\ u IN V
1978 (!t. --e4 < t /\ t < e4
1979 ==> aff_ge {vec 0} {f v t, f w t} INTER
1980 aff_lt {vec 0} {f u t} =
1985 REPEAT WEAKER_STRIP_TAC;
1986 REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
1987 REPEAT WEAKER_STRIP_TAC;
1988 TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
1989 MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
1990 BY(ASM_REWRITE_TAC[]);
1991 TYPIFY `v IN V /\ w IN V` (C SUBGOAL_THEN ASSUME_TAC);
1992 MATCH_MP_TAC Local_lemmas.LOCAL_FAN_IMP_IN_V;
1993 BY(ASM_REWRITE_TAC[]);
1994 TYPIFY `~(u = vec 0)` (C SUBGOAL_THEN ASSUME_TAC);
1995 BY(ASM_MESON_TAC[Local_lemmas.LOFA_IMP_V_DIFF]);
1996 TYPIFY `rho_node1 FF v = w` (C SUBGOAL_THEN ASSUME_TAC);
1997 MATCH_MP_TAC Local_lemmas.DETER_RHO_NODE;
1998 BY(ASM_REWRITE_TAC[]);
1999 TYPIFY `~collinear {vec 0,v, rho_node1 FF v}` (C SUBGOAL_THEN MP_TAC);
2000 MATCH_MP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
2001 BY(ASM_REWRITE_TAC[]);
2004 COMMENT "expand generic";
2005 RULE_ASSUM_TAC(REWRITE_RULE[Localization.generic]);
2006 FIRST_X_ASSUM (C INTRO_TAC [`v`;`rho_node1 FF v`;`u`]);
2009 MATCH_MP_TAC Local_lemmas.LOCAL_FAN_IN_FF_IN_ORD_PAIRS2;
2010 BY(ASM_REWRITE_TAC[]);
2011 (GMATCH_SIMP_TAC generic_alt);
2014 TYPIFY `?e. &0 < e /\ (!t. -- e < t /\ t < e ==> ~(f u t = vec 0) /\ ~collinear {vec 0,f v t,f w t} /\ (~coplanar {vec 0,f u t,f v t,f w t} \/ -- (f u t) IN wedge (vec 0) (f v t cross f w t) (f w t) (f v t)))` ENOUGH_TO_SHOW_TAC;
2015 REPEAT WEAKER_STRIP_TAC;
2016 TYPIFY `e` EXISTS_TAC;
2018 REPEAT WEAKER_STRIP_TAC;
2019 GMATCH_SIMP_TAC generic_alt;
2020 FIRST_X_ASSUM (C INTRO_TAC [`t`]);
2022 REPEAT WEAKER_STRIP_TAC;
2023 BY(ASM_REWRITE_TAC[]);
2024 TYPIFY `?e1. &0 < e1 /\ (!t. abs t < e1 ==> ~(f u t = vec 0))` (C SUBGOAL_THEN MP_TAC);
2025 REWRITE_TAC[GSYM NORM_POS_LT];
2026 INTRO_TAC Pent_hex.continuous_preimage_open [`norm o (f u)`;`real_interval (a,b)`;`{x | &0 < x}`];
2027 REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL];
2028 REWRITE_TAC[IN_ELIM_THM;o_THM];
2030 REWRITE_TAC[REAL_OPEN_HALFSPACE_GT;arith ` &0 < x <=> x > &0`];
2031 GMATCH_SIMP_TAC REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT;
2032 REWRITE_TAC[Ocbicby.REAL_OPEN_REAL_INTERVAL];
2033 REPEAT WEAKER_STRIP_TAC;
2034 MATCH_MP_TAC REAL_CONTINUOUS_CONTINUOUS_ATREAL_COMPOSE;
2036 RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation]);
2037 BY(ASM_MESON_TAC[]);
2038 BY(REWRITE_TAC[REAL_CONTINUOUS_NORM_WITHIN]);
2039 REWRITE_TAC[real_open;IN_ELIM_THM];
2040 DISCH_THEN (C INTRO_TAC [`&0`]);
2042 RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation]);
2044 BY(ASM_MESON_TAC[NORM_POS_LT]);
2045 BY(MESON_TAC[arith `abs (x - &0) = abs x`]);
2046 REPEAT WEAKER_STRIP_TAC;
2047 COMMENT "collinearity";
2048 TYPIFY `f v (&0) = v /\ f w (&0) = w /\ f u (&0) = u /\ f v continuous atreal (&0) /\ f w continuous atreal (&0) /\ f u continuous atreal (&0)` (C SUBGOAL_THEN ASSUME_TAC);
2049 RULE_ASSUM_TAC (REWRITE_RULE[Localization.deformation]);
2050 BY(ASM_MESON_TAC[]);
2051 TYPIFY `?e2. &0 < e2 /\ (!t. abs t < e2 ==> ~collinear {vec 0,f v t, f w t})` (C SUBGOAL_THEN MP_TAC);
2052 INTRO_TAC (GEN_ALL NONCOLLINEAR_OPEN) [`&0`;`(vec 0):real^3`;`f v`;`f w`];
2054 BY(MESON_TAC[arith `abs(&0 - r') = abs(r')`]);
2055 REPEAT WEAKER_STRIP_TAC;
2056 TYPIFY `?e3. &0 < e3 /\ (!t. abs t < e3 ==> ((~coplanar {vec 0, f u t, f v t, f w t} \/ --f u t IN wedge (vec 0) (f v t cross f w t) (f w t) (f v t))))` (C SUBGOAL_THEN MP_TAC);
2057 FIRST_X_ASSUM DISJ_CASES_TAC;
2058 INTRO_TAC NONPLANAR_OPEN [`\ (t:real). (vec 0):real^3`;`f u`;`f v`;`f w`;`&0`];
2059 ASM_REWRITE_TAC[CONTINUOUS_CONST;arith `abs(&0 - t') = abs(t')`];
2061 COMMENT "disjointness";
2062 TYPIFY `~(v cross w = v) /\ ~(v cross w = w) ` (C SUBGOAL_THEN ASSUME_TAC);
2063 REWRITE_TAC[CROSS_EQ_SELF];
2064 BY(ASM_MESON_TAC[COLLINEAR_2;SET_RULE `{a,a,b} = {a,b}`;SET_RULE `{a,b,a} = {a,b}`]);
2065 TYPIFY `~(v cross w = -- u)` (C SUBGOAL_THEN ASSUME_TAC);
2066 FIRST_X_ASSUM_ST `wedge` MP_TAC;
2067 REWRITE_TAC[wedge;IN_ELIM_THM];
2068 BY(MESON_TAC[COLLINEAR_2;SET_RULE `{a,b,b}={a,b}`]);
2069 TYPIFY `~( ( -- (u:real^3) = v) \/ (-- u = w))` (C SUBGOAL_THEN MP_TAC);
2071 FIRST_X_ASSUM_ST `wedge` MP_TAC;
2072 REWRITE_TAC[Reuhady.WEDGE_SIMPLE];
2073 FIRST_X_ASSUM DISJ_CASES_TAC;
2074 ASM_REWRITE_TAC[IN_ELIM_THM];
2075 BY(REWRITE_TAC[arith `~(x < x)`]);
2076 ASM_REWRITE_TAC[IN_ELIM_THM];
2077 BY(REWRITE_TAC[AZIM_REFL;arith `~(&0 < &0)`]);
2078 REWRITE_TAC[DE_MORGAN_THM];
2079 REPEAT WEAKER_STRIP_TAC;
2081 TYPIFY `?g. deformation g {v, v cross w, w, --u} (a,b) /\ ( g (v cross w) = (\t. f v t cross f w t)) /\ (g v = f v) /\ (g w = f w) /\ (g (-- u) = (\t. -- f u t))` (C SUBGOAL_THEN MP_TAC);
2082 TYPIFY `\x. if (x = --u) then (\t. -- f u t) else if (x = v cross w) then (\t. f v t cross f w t) else f x` EXISTS_TAC;
2083 ASM_TAC THEN ASM_REWRITE_TAC[Localization.deformation;IN_INSERT;NOT_IN_EMPTY] THEN REPEAT WEAKER_STRIP_TAC THEN ASM_REWRITE_TAC[];
2085 BY(REPEAT WEAKER_STRIP_TAC THEN (REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC)) THEN ASM_REWRITE_TAC[] THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[]);
2086 REPEAT WEAKER_STRIP_TAC THEN (REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC)) THEN ASM_REWRITE_TAC[] THEN TRY (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[];
2087 BY(MATCH_MP_TAC (* Xbjrphc. *)CONTINUOUS_CROSS THEN REWRITE_TAC[ETA_AX] THEN CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
2088 MATCH_MP_TAC CONTINUOUS_NEG;
2089 BY(REWRITE_TAC[ETA_AX] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);
2090 REPEAT WEAKER_STRIP_TAC;
2091 INTRO_TAC NHCXLRV [`-- (u:real^3)`;`v`;`v cross w`;`w`;`g`;`a`;`b`];
2094 TYPIFY_GOAL_THEN `~collinear {vec 0, v cross w, --u}` (unlist REWRITE_TAC);
2095 FIRST_X_ASSUM_ST `wedge` MP_TAC;
2096 REWRITE_TAC[wedge;IN_ELIM_THM];
2098 ONCE_REWRITE_TAC[SET_RULE `{a,b,c} = {a,c,b}`];
2099 BY(ASM_REWRITE_TAC[GSYM Local_lemmas.COLL_IFF_COLL_CROSS;GSYM COLL_IFF_COLL_CROSS2]);
2101 REPEAT WEAKER_STRIP_TAC;
2102 TYPIFY `(?e. (&0 < e /\ e <= e1 /\ e <= e2 /\ e <= e3))` (C SUBGOAL_THEN MP_TAC);
2103 INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`{e1,e2,e3}`];
2106 REWRITE_TAC[FINITE_RULES];
2107 BY(REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY]);
2109 REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
2110 REPEAT WEAKER_STRIP_TAC;
2111 TYPIFY `m` EXISTS_TAC;
2113 REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC);
2114 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2115 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
2116 REPEAT WEAKER_STRIP_TAC;
2117 TYPIFY `e` EXISTS_TAC;
2118 REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`];
2120 REPEAT WEAKER_STRIP_TAC;
2121 BY(REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN (REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN TRY REAL_ARITH_TAC))
2125 let zlz_wedge_skolem = prove_by_refinement(
2127 convex_local_fan (V,E,FF) /\
2128 (!x v. ?e3. x IN FF /\ v IN V
2130 (!t. --e3 < t /\ t < e3
2132 wedge_in_fan_ge (f (FST x) t,f (SND x) t)
2133 (IMAGE (IMAGE (\v. f v t)) E)))
2137 (!t. --e3 < t /\ t < e3
2138 ==> IMAGE (\v. f v t) V SUBSET
2139 wedge_in_fan_ge (f (FST x) t,f (SND x) t)
2140 (IMAGE (IMAGE (\v. f v t)) E)))`,
2143 REPEAT WEAKER_STRIP_TAC;
2144 REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
2146 FIRST_X_ASSUM (C INTRO_TAC [`x`]);
2147 REWRITE_TAC[SKOLEM_THM];
2148 REPEAT WEAKER_STRIP_TAC;
2149 TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
2150 MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
2151 BY(ASM_REWRITE_TAC[]);
2152 TYPIFY `~(V = {})` (C SUBGOAL_THEN ASSUME_TAC);
2153 MATCH_MP_TAC Local_lemmas.LOFA_V_NOT_EMP;
2154 BY(ASM_REWRITE_TAC[]);
2155 TYPIFY `?e. &0 < e /\ (!v. v IN V ==> e <= e3 v)` (C SUBGOAL_THEN MP_TAC);
2156 INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`IMAGE e3 V`];
2159 (MATCH_MP_TAC FINITE_IMAGE);
2160 MATCH_MP_TAC Local_lemmas.LOCAL_FAN_FINITE_V;
2161 BY(ASM_REWRITE_TAC[]);
2162 (MATCH_MP_TAC Fatugpd.NOT_EMPTY_IMAGE);
2163 BY(ASM_REWRITE_TAC[]);
2164 REPEAT WEAKER_STRIP_TAC;
2165 TYPIFY `m` EXISTS_TAC;
2166 REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC);
2167 REWRITE_TAC[IN_IMAGE;EXTENSION;NOT_IN_EMPTY];
2168 REPEAT WEAKER_STRIP_TAC;
2170 FIRST_X_ASSUM_ST `wedge_in_fan_ge` (C INTRO_TAC [`x'`]);
2172 REPEAT WEAKER_STRIP_TAC;
2174 BY(ASM_MESON_TAC[]);
2175 REPEAT WEAKER_STRIP_TAC;
2176 TYPIFY `e` EXISTS_TAC;
2178 REPEAT WEAKER_STRIP_TAC;
2179 REWRITE_TAC[SUBSET;IN_IMAGE];
2180 REPEAT WEAKER_STRIP_TAC;
2182 FIRST_X_ASSUM_ST `wedge_in_fan_ge` (C INTRO_TAC [`x''`]);
2184 REPEAT WEAKER_STRIP_TAC;
2185 FIRST_X_ASSUM (C INTRO_TAC [`t`]);
2187 DISCH_THEN MATCH_MP_TAC;
2188 FIRST_X_ASSUM (C INTRO_TAC [`x''`]);
2190 BY(ASM_TAC THEN REAL_ARITH_TAC)
2194 let wedge_ge_refl = prove_by_refinement(
2195 `!v1 v2 v3 v4. v2 IN wedge_ge v1 v2 v3 v4`,
2198 REWRITE_TAC[Local_lemmas.WEDGE_GE_AZIM_LE;Local_lemmas.AZIM_SPEC_DEGENERATE];
2199 BY(REWRITE_TAC[Counting_spheres.AZIM_NN])
2203 let zlz_wedge_refl = prove_by_refinement(
2205 convex_local_fan (V,E,FF) /\
2207 deformation f V (a,b) /\
2208 (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==>
2209 interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi) ==>
2210 (!v w. (w IN V /\ v IN {w, rho_node1 FF w, ivs_rho_node1 FF w}) ==>
2211 ?e. &0 < e /\ (!t. -- e < t /\ t < e ==> f v t IN wedge_in_fan_ge (f w t , f (rho_node1 FF w) t)
2212 (IMAGE (IMAGE (\v. f v t)) E)))`,
2215 REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
2216 REPEAT WEAKER_STRIP_TAC;
2217 TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
2218 MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
2219 BY(ASM_REWRITE_TAC[]);
2220 INTRO_TAC (GEN_ALL Lunar_deform.XRECQNS_UPDATE) [`a`;`b`;`V`;`E`;`f`;`FF`];
2222 REPEAT WEAKER_STRIP_TAC;
2223 TYPIFY `!t. IMAGE (\s. IMAGE (\v. f v t) s) E = IMAGE (IMAGE (\v. f v t)) E /\ IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` (C SUBGOAL_THEN ASSUME_TAC);
2224 BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]);
2225 INTRO_TAC (GEN_ALL Local_lemmas.CVX_LO_IMP_LO) [`V`;`E`;`FF`];
2227 TYPIFY `e` EXISTS_TAC;
2229 REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`];
2230 REPEAT WEAKER_STRIP_TAC;
2231 FIRST_X_ASSUM_ST `local_fan` (C INTRO_TAC [`t`]);
2234 INTRO_TAC deformation_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`w`;`t`];
2237 INTRO_TAC deformation_ivs_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`w`;`t`];
2241 GMATCH_SIMP_TAC Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND;
2243 TYPIFY `IMAGE (\v. f v t) V` EXISTS_TAC;
2245 BY(ASM_MESON_TAC[IN_IMAGE]);
2246 REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_REWRITE_TAC[Local_lemmas1.FST_LST_IN_WEDGE_GE];
2247 BY(REWRITE_TAC[wedge_ge_refl])
2251 let zlz_wedge_open = prove_by_refinement(
2253 convex_local_fan (V,E,FF) /\
2255 deformation f V (a,b) /\
2256 (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==>
2257 interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi) ==>
2258 (!v w. (v IN V /\ w IN V /\ v IN wedge (vec 0) w (rho_node1 FF w) (ivs_rho_node1 FF w)) ==>
2259 ?e. &0 < e /\ (!t. -- e < t /\ t < e ==> f v t IN wedge_in_fan_ge (f w t , f (rho_node1 FF w) t)
2260 (IMAGE (IMAGE (\v. f v t)) E)))`,
2263 REPEAT WEAKER_STRIP_TAC;
2264 TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
2265 MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
2266 BY(ASM_REWRITE_TAC[]);
2267 INTRO_TAC (GEN_ALL Lunar_deform.XRECQNS_UPDATE) [`a`;`b`;`V`;`E`;`f`;`FF`];
2269 REPEAT WEAKER_STRIP_TAC;
2270 TYPIFY `!t. IMAGE (\s. IMAGE (\v. f v t) s) E = IMAGE (IMAGE (\v. f v t)) E /\ IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` (C SUBGOAL_THEN ASSUME_TAC);
2271 BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]);
2272 TYPIFY `v = w` ASM_CASES_TAC;
2273 INTRO_TAC zlz_wedge_refl [`a`;`b`;`V`;`E`;`FF`;`f`];
2275 DISCH_THEN (C INTRO_TAC [`w`;`w`]);
2276 BY(ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY]);
2277 INTRO_TAC NHCXLRV_ALT [`v`;`(ivs_rho_node1 FF w)`;`w`;`(rho_node1 FF w)`;`f`;`a`;`b`];
2279 TYPIFY `rho_node1 FF w IN V` (C SUBGOAL_THEN ASSUME_TAC);
2280 MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
2281 BY(ASM_REWRITE_TAC[]);
2282 TYPIFY `ivs_rho_node1 FF w IN V` (C SUBGOAL_THEN ASSUME_TAC);
2283 MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_IVS_IN_V;
2284 BY(ASM_REWRITE_TAC[]);
2285 GMATCH_SIMP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
2287 BY(ASM_MESON_TAC[]);
2288 GMATCH_SIMP_TAC Local_lemmas.LOFA_IMP_NOT_COLL_IVS;
2290 BY(ASM_MESON_TAC[]);
2293 MATCH_MP_TAC deformation_subset;
2294 TYPIFY `V` EXISTS_TAC;
2296 ASM_REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
2297 BY(ASM_MESON_TAC[]);
2298 BY(ASM_MESON_TAC[Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN]);
2299 REPEAT WEAKER_STRIP_TAC;
2300 REWRITE_TAC[arith `--e < t /\ t < e <=> abs t < e`];
2301 TYPIFY `?e''. (&0 < e'') /\ e'' <= e /\ e'' <= e'` (C SUBGOAL_THEN MP_TAC);
2302 TYPIFY `if (e <= e') then e else e'` EXISTS_TAC;
2303 BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC) THEN REAL_ARITH_TAC);
2304 REPEAT WEAKER_STRIP_TAC;
2305 TYPIFY `e''` EXISTS_TAC;
2307 REPEAT WEAKER_STRIP_TAC;
2308 FIRST_X_ASSUM_ST `local_fan` (C INTRO_TAC [`t`]);
2311 BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2313 FIRST_X_ASSUM (C INTRO_TAC [`t`]);
2315 BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2317 INTRO_TAC deformation_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`w`;`t`];
2320 INTRO_TAC deformation_ivs_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`w`;`t`];
2324 GMATCH_SIMP_TAC Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND;
2326 TYPIFY `IMAGE (\v. f v t) V` EXISTS_TAC;
2328 BY(ASM_MESON_TAC[IN_IMAGE]);
2329 FIRST_X_ASSUM_ST `wedge` MP_TAC;
2331 BY(SET_TAC[Leaf_cell.WEDGE_SUBSET_WEDGE_GE])
2335 let PROPERTIES_GENERIC_LOCAL_FAN_ALT = prove_by_refinement(
2337 local_fan (V,E,FF) /\ u IN V /\ v IN V /\ ~(u = v) /\ generic V E ==> ~collinear {vec 0,u,v}`,
2340 BY(ASM_MESON_TAC[Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN])
2344 let skolem_epsilon_old = prove_by_refinement(
2345 `!P Q s. (!e e' i. &0 < e /\ e <= e' /\ (i:A) IN s /\ P i==> (Q e' i ==> Q e i)) /\ FINITE s ==>
2346 ((!i. ?e. (i IN s /\ P i) ==> (&0 < e /\ Q e i)) <=> (?e. !i. (i IN s /\ P i) ==> (&0 < e /\ Q e i)))`,
2349 REPEAT WEAKER_STRIP_TAC;
2350 TYPIFY `~(?i. i IN s /\ P i)` ASM_CASES_TAC;
2351 BY(ASM_MESON_TAC[]);
2352 RULE_ASSUM_TAC(REWRITE_RULE[]);
2353 MATCH_MP_TAC (TAUT `((a ==>b) /\ (b ==> a)) ==> (a <=> b)`);
2355 REWRITE_TAC[SKOLEM_THM];
2356 REPEAT WEAKER_STRIP_TAC;
2357 INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`IMAGE e {i | i IN s /\ P i}`];
2360 (MATCH_MP_TAC FINITE_IMAGE);
2361 MATCH_MP_TAC FINITE_SUBSET;
2362 TYPIFY `s` EXISTS_TAC;
2365 (MATCH_MP_TAC Fatugpd.NOT_EMPTY_IMAGE);
2366 ASM_REWRITE_TAC[EXTENSION;IN_ELIM_THM;NOT_IN_EMPTY];
2367 BY(ASM_MESON_TAC[]);
2368 REPEAT WEAKER_STRIP_TAC;
2369 TYPIFY `m` EXISTS_TAC;
2370 REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC);
2371 REWRITE_TAC[IN_IMAGE;EXTENSION;NOT_IN_EMPTY;IN_ELIM_THM];
2372 REPEAT WEAKER_STRIP_TAC;
2375 BY(ASM_MESON_TAC[]);
2376 BY(ASM_MESON_TAC[]);
2377 REPEAT WEAKER_STRIP_TAC;
2382 let SKOLEM_EPSILON = prove_by_refinement(
2383 `!Q s. (!e e' i. &0 < e /\ e <= e' /\ (i:A) IN s ==> (Q e' i ==> Q e i)) /\ FINITE s ==>
2384 ((!i. ?e. (&0 < e) /\ (i IN s ==> (Q e i))) <=> (?e. !i. (&0 < e) /\ (i IN s ==> ( Q e i))))`,
2387 REPEAT WEAKER_STRIP_TAC;
2388 TYPIFY `~(?i. i IN s)` ASM_CASES_TAC;
2389 BY(ASM_MESON_TAC[]);
2390 RULE_ASSUM_TAC(REWRITE_RULE[]);
2391 MATCH_MP_TAC (TAUT `((a ==>b) /\ (b ==> a)) ==> (a <=> b)`);
2393 BY(ASM_MESON_TAC[]);
2394 REWRITE_TAC[SKOLEM_THM];
2395 REPEAT WEAKER_STRIP_TAC;
2396 INTRO_TAC Packing3.REAL_FINITE_MIN_EXISTS [`IMAGE e s`];
2399 (MATCH_MP_TAC FINITE_IMAGE);
2400 BY(ASM_REWRITE_TAC[]);
2401 (MATCH_MP_TAC Fatugpd.NOT_EMPTY_IMAGE);
2402 ASM_REWRITE_TAC[EXTENSION;IN_ELIM_THM;NOT_IN_EMPTY];
2403 BY(ASM_MESON_TAC[]);
2404 REPEAT WEAKER_STRIP_TAC;
2405 TYPIFY `m` EXISTS_TAC;
2407 REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC);
2408 REWRITE_TAC[IN_IMAGE;EXTENSION;NOT_IN_EMPTY;IN_ELIM_THM];
2409 REPEAT WEAKER_STRIP_TAC;
2415 let EXISTS_AND_IMP = prove_by_refinement(
2416 `!P Q R. (?(d:A). (P /\ Q d ==> R d)) <=> (P ==> (?d. Q d ==> R d))`,
2423 let XIV_DEFORMATION = prove_by_refinement(
2425 deformation f {w i | i <= r + 2} (a,b) /\
2426 pairwise (\i j. ~collinear {vec 0, w i, w j}) (0..(r+1)) /\
2427 pairwise (\i j. ~collinear {vec 0, w i, w j}) (1..(r+2)) /\
2428 (\ (i,j,k). dihV (vec 0) (w i) (w j) (w k)) = dh /\
2429 (!i. ?e2. i IN 1..r+1 ==> &0 < e2 /\
2430 (!t. abs t < e2 ==> azim (vec 0) (f (w i) t) (f (w (i+1)) t) (f (w (i-1)) t) <= pi)) /\
2431 (!i. i IN 1..r+1 ==> &0 < azim (vec 0) (w i) (w (i+1)) (w (i-1))) /\
2433 {p, q, q + 1} SUBSET 1..r+1 /\ ~(p = q) /\ ~(p = q + 1)
2434 ==> dh (p,q,q + 1) = &0) /\
2436 {p, p + 1, q} SUBSET 1..r+1 /\ q > p + 1 ==> dh (p,p + 1,q) = &0) /\
2437 (!p q. {p + 1, p, q} SUBSET 1..r+1 /\ q < p ==> dh (p + 1,p,q) = &0)
2438 ==> (?e. &0 < e /\ (!t. abs t < e ==>
2439 f (w 1) t IN wedge_ge (vec 0) (f (w (r+1)) t) (f (w (r+2)) t) (f (w (r)) t) /\
2440 f (w (r+1)) t IN wedge_ge (vec 0) (f (w 1) t) (f (w (2)) t) (f (w (0)) t)))`,
2443 REPEAT WEAKER_STRIP_TAC;
2445 COMMENT "find collinear epsilon";
2446 TYPIFY `!i. i <= r + 2 ==> f (w i) (&0) = w i` ((C SUBGOAL_THEN ASSUME_TAC));
2447 RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_ELIM_THM;]);
2448 BY(ASM_MESON_TAC[]);
2449 TYPIFY `!i j. i IN 0..r+2 /\ j IN 0..r+2 /\ ~collinear {vec 0,w i,w j} ==> (?dc. &0 < dc /\ (!t. abs t < dc ==> ~collinear {vec 0, f (w i) t, f (w j) t}))` (C SUBGOAL_THEN ASSUME_TAC);
2450 REPEAT WEAKER_STRIP_TAC;
2451 INTRO_TAC (GEN_ALL NONCOLLINEAR_OPEN) [`&0`;`(vec 0):real^3`;`f (w i)`;`f (w j)`];
2452 RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_ELIM_THM;IN_NUMSEG]);
2454 BY(ASM_MESON_TAC[]);
2455 BY(REWRITE_TAC[arith `abs(&0 - r') = abs r'`]);
2456 COMMENT "skolemize collinear";
2457 TYPIFY `?dc. !i. (&0 < dc) /\ (i IN 0..r+2 ==> (!j. j IN 0..r+2 /\ ~collinear {vec 0,w i,w j} ==> (!t. abs t < dc ==> ~collinear {vec 0, f (w i) t, f (w j) t})))` (C SUBGOAL_THEN ASSUME_TAC);
2458 GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON);
2459 REWRITE_TAC[FINITE_NUMSEG];
2461 REPEAT WEAKER_STRIP_TAC;
2462 FIRST_X_ASSUM (C INTRO_TAC [`j`]);
2464 BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
2465 DISCH_THEN (C INTRO_TAC [`t`]);
2467 BY(REPLICATE_TAC 8 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2468 BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[]);
2470 REWRITE_TAC[MESON [arith `&0 < &1`] `(?dc. &0 < dc /\ (a ==> (!j. b j /\ c j ==> r dc j))) <=> (a ==> (?dc. !j. &0 < dc /\ (b j ==> (c j ==> r dc j))))`];
2472 GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON);
2473 REWRITE_TAC[FINITE_NUMSEG];
2475 REPEAT WEAKER_STRIP_TAC;
2476 FIRST_X_ASSUM_ST `!` MP_TAC;
2478 BY(ASM_REWRITE_TAC[]);
2479 DISCH_THEN (C INTRO_TAC [`t`]);
2481 BY(REPLICATE_TAC 8 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2482 BY(ASM_REWRITE_TAC[]);
2483 REPEAT WEAKER_STRIP_TAC;
2484 FIRST_X_ASSUM (C INTRO_TAC [`i`;`j`]);
2485 BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[arith `&0 < &1`]);
2486 FIRST_X_ASSUM_ST `collinear` MP_TAC THEN BURY_MP_TAC;
2487 FIRST_X_ASSUM_ST `collinear` kill;
2488 COMMENT "find dih epsilon";
2489 TYPIFY `!i j k e. &0 < e /\ i IN 1..r+1 /\ j IN 1 ..r+1 /\ k IN 1..r+1 /\ ~(i=j) /\ ~(i=k) /\ dh (i,j,k) = &0 ==> (? d. &0 < d /\ (!t. abs t < d ==> dihV (vec 0) (f (w i) t) (f (w j) t) (f (w k) t) < e))` (C SUBGOAL_THEN ASSUME_TAC);
2490 EXPAND_TAC "dh" THEN REWRITE_TAC[];
2491 REPEAT WEAKER_STRIP_TAC;
2492 TYPIFY `!i. i <= r + 2 ==> f (w i) (&0) = w i` ((C SUBGOAL_THEN ASSUME_TAC));
2493 RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_ELIM_THM;]);
2494 BY(ASM_MESON_TAC[]);
2495 INTRO_TAC (* Xbjrphc. *)REAL_CONTINUOUS_ATREAL_DIHV_COMPOSE [`\(t:real). (vec 0):real^3`;`f (w i)`;`f (w j)`;`f (w k)`;`&0`];
2497 RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_ELIM_THM;pairwise]);
2498 REWRITE_TAC[CONTINUOUS_CONST];
2499 FIRST_X_ASSUM (REPEAT o GMATCH_SIMP_TAC);
2500 ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
2501 RULE_ASSUM_TAC(REWRITE_RULE[IN_NUMSEG]);
2502 TYPIFY_GOAL_THEN `k <= r + 2 /\ j <= r + 2 /\ i <= r + 2 ` (unlist REWRITE_TAC);
2504 REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN TRY ASM_ARITH_TAC;
2505 BY(TYPIFY `i` EXISTS_TAC THEN ASM_ARITH_TAC);
2506 BY(TYPIFY `j` EXISTS_TAC THEN ASM_ARITH_TAC);
2507 BY(TYPIFY `k` EXISTS_TAC THEN ASM_ARITH_TAC);
2508 REWRITE_TAC[real_continuous_atreal];
2509 DISCH_THEN (C INTRO_TAC [`e`]);
2510 ASM_REWRITE_TAC[arith `abs (x' - &0) = abs x'`] THEN REPEAT WEAKER_STRIP_TAC;
2511 TYPIFY `d` EXISTS_TAC;
2513 REPEAT WEAKER_STRIP_TAC;
2514 FIRST_X_ASSUM (C INTRO_TAC [`t`]);
2516 FIRST_X_ASSUM_ST `i <= r + 2` (REPEAT o GMATCH_SIMP_TAC);
2518 RULE_ASSUM_TAC(REWRITE_RULE[IN_NUMSEG]);
2519 ASM_SIMP_TAC[arith `i <= r + 1 ==> i <= r + 2`];
2521 COMMENT "merge dih epsilon";
2522 TYPIFY `!e. &0 < e ==> (?d. !i. (&0 < d) /\ (i IN 1..r+1 ==> (!j k. j IN 1..r+1 /\ k IN 1..r+1 /\ ~(i = j) /\ ~(i=k) /\ dh(i,j,k)= &0 ==> (!t. abs t < d ==> dihV (vec 0) (f (w i) t) (f (w j) t) (f (w k) t) < e))))` (C SUBGOAL_THEN ASSUME_TAC);
2523 REPEAT WEAKER_STRIP_TAC;
2524 GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON);
2525 REWRITE_TAC[FINITE_NUMSEG];
2527 REPEAT WEAKER_STRIP_TAC;
2528 FIRST_X_ASSUM (C INTRO_TAC [`j`;`k`]);
2530 DISCH_THEN MATCH_MP_TAC;
2531 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2533 REWRITE_TAC[MESON[arith `&0 < &1`] `(?d. &0 < d /\ (p ==> (!j k. a j /\ r j k ==> u j k d))) <=> (p ==> (?d. !j. &0 < d /\ (a j ==> (!k. r j k ==> u j k d))))`];
2535 GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON);
2536 REWRITE_TAC[FINITE_NUMSEG];
2538 REPEAT WEAKER_STRIP_TAC;
2539 FIRST_X_ASSUM (C INTRO_TAC [`k`]);
2541 DISCH_THEN MATCH_MP_TAC;
2542 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2544 REWRITE_TAC[MESON[arith `&0 < &1`] `(?d. &0 < d /\ (p ==> (!k. a k /\ r k ==> u k d))) <=> (p ==> (?d. !k. &0 < d /\ (a k ==> (r k ==> u k d))))`];
2546 GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON);
2547 REWRITE_TAC[FINITE_NUMSEG];
2549 REPEAT WEAKER_STRIP_TAC;
2550 FIRST_X_ASSUM_ST `dihV` MP_TAC;
2552 DISCH_THEN MATCH_MP_TAC;
2553 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2555 REWRITE_TAC[MESON[arith `&0 < &1`] `(?d. &0 < d /\ (a ==> b ==> c d)) <=> (a /\ b ==> (?d. &0 < d /\ c d))`];
2556 REPEAT WEAKER_STRIP_TAC;
2557 FIRST_X_ASSUM (C INTRO_TAC [`i`;`j`;`k`;`e`]);
2558 DISCH_THEN MATCH_MP_TAC;
2559 BY(ASM_REWRITE_TAC[]);
2560 FIRST_X_ASSUM MP_TAC;
2562 REPEAT WEAKER_STRIP_TAC;
2564 TYPIFY `?c. !i. (&0 < c) /\ (i IN 1..r+1 ==> c < azim (vec 0) (w i) (w (i+1)) (w (i-1)))` (C SUBGOAL_THEN ASSUME_TAC);
2565 GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON);
2566 REWRITE_TAC[FINITE_NUMSEG];
2570 REWRITE_TAC[MESON[arith `&0 < &1`] `(?c. &0 < c /\ (b ==> r c)) <=> (b ==> (?c. &0 < c /\ r c))`];
2572 TYPIFY `azim (vec 0) (w i) (w (i+1)) (w (i-1)) / &2` EXISTS_TAC;
2573 FIRST_X_ASSUM_ST `azim` (C INTRO_TAC [`i`]);
2576 FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
2577 COMMENT "azim deform lower bound";
2578 TYPIFY `!i. i IN 1..r+1 ==> (?d. &0 < d /\ (!t. abs t < d ==> (c < azim (vec 0) (f (w i) t) (f (w(i+1)) t) (f (w(i-1)) t))))` (C SUBGOAL_THEN ASSUME_TAC);
2579 REPEAT WEAKER_STRIP_TAC;
2580 TYPIFY `!i. i <= r + 2 ==> f (w i) (&0) = w i` ((C SUBGOAL_THEN ASSUME_TAC));
2581 RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_ELIM_THM;]);
2582 BY(ASM_MESON_TAC[]);
2583 INTRO_TAC (* Xbjrphc. *)REAL_CONTINUOUS_ATREAL_AZIM_COMPOSE [`\(t:real). (vec 0):real^3`;`f (w i)`;`f (w (i+1))`;`f (w (i-1))`;`&0`];
2585 RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_ELIM_THM;pairwise]);
2586 REWRITE_TAC[CONTINUOUS_CONST];
2587 FIRST_X_ASSUM (REPEAT o GMATCH_SIMP_TAC);
2588 ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
2589 RULE_ASSUM_TAC(REWRITE_RULE[IN_NUMSEG]);
2590 TYPIFY_GOAL_THEN `i - 1 <= r + 2 /\ i + 1 <= r + 2 /\ i <= r + 2` (unlist REWRITE_TAC);
2592 GMATCH_SIMP_TAC (GSYM Local_lemmas.AZIM_EQ_0_GE_ALT2);
2593 REWRITE_TAC[GSYM azim_pos_iff_nz];
2594 TYPIFY_GOAL_THEN ` ~collinear {vec 0, w i, w (i - 1)}` (unlist REWRITE_TAC);
2595 FIRST_X_ASSUM_ST `collinear` kill;
2596 BY((FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[] THEN TRY ASM_ARITH_TAC);
2597 REPEAT CONJ_TAC THEN (FIRST_X_ASSUM MATCH_MP_TAC) THEN ASM_REWRITE_TAC[] THEN TRY ASM_ARITH_TAC;
2598 BY(TYPIFY `i` EXISTS_TAC THEN ASM_ARITH_TAC);
2599 BY(TYPIFY `i+1` EXISTS_TAC THEN ASM_ARITH_TAC);
2600 BY(TYPIFY `i-1` EXISTS_TAC THEN ASM_ARITH_TAC);
2601 REWRITE_TAC[real_continuous_atreal];
2602 FIRST_X_ASSUM (REPEAT o GMATCH_SIMP_TAC);
2603 RULE_ASSUM_TAC(REWRITE_RULE[IN_NUMSEG]);
2604 TYPIFY_GOAL_THEN `i - 1 <= r + 2 /\ i + 1 <= r + 2 /\ i <= r + 2` (unlist REWRITE_TAC);
2606 DISCH_THEN (C INTRO_TAC [`abs(azim (vec 0) (w i) (w (i+1)) (w (i-1)) - c)`]);
2607 FIRST_X_ASSUM (C INTRO_TAC [`i`]);
2608 REPEAT WEAKER_STRIP_TAC;
2609 FIRST_X_ASSUM_ST `c < azim a1 a2 a3 a4` MP_TAC;
2612 FIRST_X_ASSUM_ST `abs` MP_TAC;
2614 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2615 ASM_REWRITE_TAC[arith `abs (x' - &0) = abs x'`] THEN REPEAT WEAKER_STRIP_TAC;
2616 TYPIFY `d` EXISTS_TAC;
2618 REPEAT WEAKER_STRIP_TAC;
2619 FIRST_X_ASSUM (C INTRO_TAC [`t`]);
2621 BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2622 COMMENT "skolemize the azim delta";
2623 TYPIFY `?d. !i. &0 < d /\ (i IN 1..r+1 ==> (!t. abs t < d ==> c < azim (vec 0) (f (w i) t) (f (w (i + 1)) t) (f (w (i - 1)) t)))` (C SUBGOAL_THEN ASSUME_TAC);
2624 GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON);
2625 REWRITE_TAC[FINITE_NUMSEG];
2627 REPEAT WEAKER_STRIP_TAC;
2628 FIRST_X_ASSUM (C INTRO_TAC [`t`]);
2629 DISCH_THEN MATCH_MP_TAC;
2630 BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2631 BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[arith `&0< &1`]);
2632 FIRST_X_ASSUM_ST `!i. i IN s ==> u` kill;
2633 COMMENT "skolemize azim<=pi";
2634 TYPIFY `?d2. !i. &0 < d2 /\ (i IN 1..r+1 ==> (!t. abs t < d2 ==> azim (vec 0) (f (w i) t) (f (w (i + 1)) t) (f (w (i - 1)) t) <= pi))` (C SUBGOAL_THEN ASSUME_TAC);
2635 GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON);
2636 REWRITE_TAC[FINITE_NUMSEG];
2638 REPEAT WEAKER_STRIP_TAC;
2639 FIRST_X_ASSUM (C INTRO_TAC [`t`]);
2640 DISCH_THEN MATCH_MP_TAC;
2641 BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2642 BY(FIRST_X_ASSUM_ST `azim a b c d <= pi` MP_TAC THEN MESON_TAC[arith `&0< &1`]);
2643 FIRST_X_ASSUM_ST `!i. i IN s ==> u` kill;
2645 TYPIFY `?e. &0 < e /\ &2 * e = c` (C SUBGOAL_THEN MP_TAC);
2646 RULE_ASSUM_TAC(REWRITE_RULE[MESON[] `(!i. a /\ b i) <=> (a /\ (!i. b i))`]);
2647 TYPIFY `c / &2` EXISTS_TAC;
2648 BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2649 REPEAT WEAKER_STRIP_TAC;
2650 FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE) o GSYM);
2651 FIRST_X_ASSUM (C INTRO_TAC [`e`]);
2653 REPEAT WEAKER_STRIP_TAC;
2654 ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
2655 TYPIFY `?d'3. !d''. (&0 < d'3) /\ (d'' IN {d,d',d2,dc} ==> d'3 <= d'')` (C SUBGOAL_THEN MP_TAC);
2656 GMATCH_SIMP_TAC (GSYM SKOLEM_EPSILON);
2657 REWRITE_TAC[FINITE_INSERT;FINITE_EMPTY];
2661 RULE_ASSUM_TAC(REWRITE_RULE[MESON[] `(!i. a /\ b i) <=> (a /\ (!i. b i))`]);
2662 TYPIFY `if (d'' IN {d,d',d2,dc}) then d'' else &1` EXISTS_TAC;
2664 ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
2665 BY(REPEAT (FIRST_X_ASSUM_ST `&0 < d` MP_TAC) THEN REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY] THEN REAL_ARITH_TAC);
2667 REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
2668 REPEAT WEAKER_STRIP_TAC;
2669 TYPIFY `d'3` EXISTS_TAC;
2670 RULE_ASSUM_TAC(REWRITE_RULE[MESON[] `(!i. a /\ b i) <=> (a /\ (!i. b i))`]);
2672 REPEAT WEAKER_STRIP_TAC;
2673 INTRO_TAC Xivphks.XIVPHKS_SHIFT [`\i. wedge_ge (vec 0) (f (w (i)) t) (f (w (i + 1)) t) (f (w (i-1)) t)`;`\ (i,j,k). azim (vec 0) (f (w i) t) (f (w (j)) t) (f (w (k)) t)`;`\ (i,j,k). dihV (vec 0) (f (w i) t) (f (w j) t) (f (w k) t)`;`e`;`r`;`\i. f (w i) t`];
2676 REWRITE_TAC[pairwise];
2677 RULE_ASSUM_TAC(REWRITE_RULE[pairwise]);
2678 TYPIFY `!j. j IN 0..r+1 ==> j IN 0..r+2` (C SUBGOAL_THEN ASSUME_TAC);
2679 BY(REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
2680 TYPIFY `!t. abs t < d'3 ==> abs t < dc` (C SUBGOAL_THEN ASSUME_TAC);
2681 REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REPEAT WEAKER_STRIP_TAC;
2682 FIRST_X_ASSUM (C INTRO_TAC [`dc`]);
2683 BY(FIRST_X_ASSUM MP_TAC THEN REAL_ARITH_TAC);
2685 REPEAT (FIRST_X_ASSUM_ST `azim` kill);
2686 BY(ASM_MESON_TAC[]);
2688 REPEAT (FIRST_X_ASSUM_ST `azim` kill);
2689 TYPIFY `!j. j IN 1..r+2 ==> j IN 0..r+2` (C SUBGOAL_THEN ASSUME_TAC);
2690 BY(REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
2691 BY(ASM_MESON_TAC[]);
2693 TYPIFY `abs t < d'` (C SUBGOAL_THEN ASSUME_TAC);
2694 REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN REPEAT WEAKER_STRIP_TAC;
2695 FIRST_X_ASSUM_ST `\/` (C INTRO_TAC [`d'`]);
2696 BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2697 BY(ASM_MESON_TAC[]);
2699 TYPIFY `abs t < d2` (C SUBGOAL_THEN ASSUME_TAC);
2700 REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN REPEAT WEAKER_STRIP_TAC;
2701 FIRST_X_ASSUM_ST `\/` (C INTRO_TAC [`d2`]);
2702 BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2703 BY(ASM_MESON_TAC[]);
2704 REPEAT (FIRST_X_ASSUM_ST `azim` kill);
2705 TYPIFY `abs t < d` (C SUBGOAL_THEN ASSUME_TAC);
2706 REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN REPEAT WEAKER_STRIP_TAC;
2707 FIRST_X_ASSUM_ST `\/` (C INTRO_TAC [`d`]);
2708 BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
2709 TYPIFY `!i j k. {i,j,k} SUBSET 1..r+1 ==> i IN 1..r+1 /\ j IN 1..r+1 /\ k IN 1..r+1` (C SUBGOAL_THEN ASSUME_TAC);
2712 BY(ASM_MESON_TAC[]);
2714 REPEAT (FIRST_X_ASSUM_ST `collinear` kill);
2715 BY(ASM_MESON_TAC[arith `~(p = p+1)`;arith `q > p+1 ==> ~(p = q)`]);
2716 BY(ASM_MESON_TAC[arith `~(p = p+1)`;arith `q < p ==> ~(p+1 = q)`]);
2717 REPEAT WEAKER_STRIP_TAC;
2718 FIRST_X_ASSUM (C INTRO_TAC [`r`;`1`]);
2719 FIRST_X_ASSUM (C INTRO_TAC [`r`;`1`]);
2720 REWRITE_TAC[arith `(r:num) <= r`;arith `1 + 1 = 2 /\ 1 - 1 = 0 /\ (1+r)+1 = r + 2 /\ 1 + r <= r + 1 /\ (1 + r) - 1 = r`];
2721 REWRITE_TAC[arith `1 + r = r + 1`];
2726 let XIV_ECAU = prove_by_refinement(
2728 deformation f {w i | i <= r + 2} (a,b) /\
2729 (!i. i IN 2..r+1 ==> w i IN aff_gt {vec 0,w 1 } {w 2} ) /\
2730 cyclic_set {w i | i IN 1..r+1 } (vec 0) ((w 1) cross (w 2)) /\
2731 (!i. i IN 1..r ==> azim_cycle {w i | i IN 1..r+1} (vec 0) ((w 1) cross (w 2)) (w i) = w (i+1)) /\
2732 pairwise (\i j. ~collinear {vec 0, w i, w j}) (0..(r+1)) /\
2733 pairwise (\i j. ~collinear {vec 0, w i, w j}) (1..(r+2)) /\
2734 (!i. ?e2. i IN 1..r+1 ==> &0 < e2 /\
2735 (!t. abs t < e2 ==> azim (vec 0) (f (w i) t) (f (w (i+1)) t) (f (w (i-1)) t) <= pi)) /\
2736 (!i. i IN 1..r+1 ==> &0 < azim (vec 0) (w i) (w (i+1)) (w (i-1)))
2737 ==> (?e. &0 < e /\ (!t. abs t < e ==>
2738 f (w 1) t IN wedge_ge (vec 0) (f (w (r+1)) t) (f (w (r+2)) t) (f (w (r)) t) /\
2739 f (w (r+1)) t IN wedge_ge (vec 0) (f (w 1) t) (f (w (2)) t) (f (w (0)) t)))`,
2742 REPEAT WEAKER_STRIP_TAC;
2743 MATCH_MP_TAC XIV_DEFORMATION;
2744 TYPED_ABBREV_TAC `dh = \ (i,j,k). dihV (vec 0) (w i) (w j) (w k)`;
2745 GEXISTL_TAC [`dh`;`a`;`b`];
2747 INTRO_TAC KCZXLLE_SYM [`w o SUC`;`r`];
2748 REWRITE_TAC[o_THM;arith `1 <= r+1 /\ SUC 0 = 1 /\ SUC 1 = 2`];
2749 TYPIFY `{w (SUC i) | i <= r } = {w i | i IN 1..r+1}` (C SUBGOAL_THEN SUBST1_TAC);
2750 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG];
2751 BY(MESON_TAC[arith `i <= r ==> (1 <= SUC i /\ SUC i <= r + 1)`;arith `(1 <= i /\ i <= r+1) ==> (PRE i <= r /\ SUC (PRE i) = i)`]);
2753 TYPIFY_GOAL_THEN `(!i j. i <= r /\ j <= r /\ ~(i = j) ==> ~collinear {vec 0, w (SUC i), w (SUC j)})` (unlist REWRITE_TAC);
2754 REPEAT WEAKER_STRIP_TAC;
2755 RULE_ASSUM_TAC(REWRITE_RULE[pairwise]);
2756 FIRST_X_ASSUM (C INTRO_TAC [`SUC i`;`SUC j`]);
2757 REWRITE_TAC[SUC_INJ];
2759 BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
2760 TYPIFY_GOAL_THEN ` (!i. 1 <= i /\ i <= r ==> w (SUC i) IN aff_gt {vec 0, w 1} {w 2})` (unlist REWRITE_TAC);
2761 REPEAT WEAKER_STRIP_TAC;
2762 FIRST_X_ASSUM MATCH_MP_TAC;
2763 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
2764 TYPIFY_GOAL_THEN `(!i. i < r ==> azim_cycle {w i | i IN 1..r + 1} (vec 0) (w 1 cross w 2) (w (SUC i)) = w (SUC (i + 1)))` (unlist REWRITE_TAC);
2765 REPEAT WEAKER_STRIP_TAC;
2766 REWRITE_TAC[arith `SUC (i + 1) = SUC i + 1`];
2767 FIRST_X_ASSUM MATCH_MP_TAC;
2768 BY(FIRST_X_ASSUM MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
2769 TYPIFY `!i j k. i IN 1..r+1 /\ j IN 1..r+1 /\ k IN 1..r+1 /\ ~(i = j) /\ ~(i = k) /\ azim (vec 0) (w i) (w j) (w k) = &0 ==> dihV (vec 0) (w i) (w j) (w k) = &0` (C SUBGOAL_THEN ASSUME_TAC);
2770 REPEAT WEAKER_STRIP_TAC;
2771 GMATCH_SIMP_TAC (GSYM Polar_fan.AZIM_DIHV_SAME_STRONG);
2772 RULE_ASSUM_TAC (REWRITE_RULE[pairwise]);
2773 TYPIFY_GOAL_THEN `~collinear {vec 0, w i, w j} /\ ~collinear {vec 0, w i, w k}` (unlist REWRITE_TAC);
2774 BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REPLICATE_TAC 8 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
2776 BY(MP_TAC PI_POS THEN REAL_ARITH_TAC);
2778 EXPAND_TAC "dh" THEN REWRITE_TAC[];
2779 REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
2780 FIRST_X_ASSUM MP_TAC;
2781 TYPIFY_GOAL_THEN `(!i j k. k <= r /\ j <= r /\ 1 <= r /\ i <= r /\ (j < k /\ (i < j \/ k < i) \/ k < j /\ (i < k \/ j < i)) ==> azim (vec 0) (w (SUC i)) (w (SUC j)) (w (SUC k)) = &0) <=> (!i j k. k IN 1..r+1 /\ i IN 1..r+1 /\ j IN 1..r+1 /\ (j < k /\ (i < j \/ k < i) \/ k < j /\ (i < k \/ j < i)) ==> azim (vec 0) (w (i)) (w (j)) (w ( k)) = &0)` (unlist REWRITE_TAC);
2782 REWRITE_TAC[IN_NUMSEG];
2783 MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a <=> b)`);
2784 CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC;
2785 FIRST_X_ASSUM (C INTRO_TAC [`PRE i`;`PRE j`;`PRE k`]);
2786 ASM_SIMP_TAC[arith `1 <= i ==> SUC (PRE i) = i`];
2787 DISCH_THEN MATCH_MP_TAC;
2788 BY(FIRST_X_ASSUM DISJ_CASES_TAC THEN REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
2789 FIRST_X_ASSUM MATCH_MP_TAC;
2790 BY(FIRST_X_ASSUM DISJ_CASES_TAC THEN REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
2793 REPEAT WEAKER_STRIP_TAC;
2794 FIRST_X_ASSUM MATCH_MP_TAC;
2795 FIRST_X_ASSUM_ST `azim` GMATCH_SIMP_TAC;
2796 FIRST_X_ASSUM_ST `IN` (unlist ASM_SIMP_TAC);
2797 REPLICATE_TAC 2(FIRST_X_ASSUM MP_TAC);
2800 REPEAT WEAKER_STRIP_TAC;
2801 FIRST_X_ASSUM MATCH_MP_TAC;
2802 FIRST_X_ASSUM_ST `azim` GMATCH_SIMP_TAC;
2803 FIRST_X_ASSUM_ST `IN` (unlist ASM_SIMP_TAC);
2804 BY(REPLICATE_TAC 1(FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
2805 REPEAT WEAKER_STRIP_TAC;
2806 FIRST_X_ASSUM MATCH_MP_TAC;
2807 FIRST_X_ASSUM_ST `azim` GMATCH_SIMP_TAC;
2808 FIRST_X_ASSUM_ST `IN` (unlist ASM_SIMP_TAC);
2809 BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC)
2813 (* was cycle_set_scale *)
2815 let cyclic_set_scale = prove_by_refinement(
2816 `!U t (e:real^A). ~(t = &0) ==> (cyclic_set U (vec 0) (t % e) <=> cyclic_set U (vec 0) e)`,
2819 REWRITE_TAC[Sphere.cyclic_set];
2820 REPEAT WEAKER_STRIP_TAC;
2821 TYPIFY `~FINITE U` ASM_CASES_TAC;
2822 BY(ASM_REWRITE_TAC[]);
2823 ONCE_REWRITE_TAC[varith `vec 0 = a <=> a = vec 0`];
2824 ASM_REWRITE_TAC[VECTOR_MUL_EQ_0];
2825 TYPIFY `(e = vec 0)` ASM_CASES_TAC;
2826 BY(ASM_REWRITE_TAC[]);
2827 RULE_ASSUM_TAC(REWRITE_RULE[]);
2829 TYPIFY `affine hull {vec 0, t % e} = affine hull {vec 0,e}` (C SUBGOAL_THEN SUBST1_TAC);
2830 REWRITE_TAC[AFFINE_HULL_2_ALT];
2831 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_UNIV;arith `vec 0 + a = a /\ x - vec 0 = x`];
2833 REWRITE_TAC[VECTOR_MUL_ASSOC];
2834 BY(ASM_MESON_TAC[arith `~(t = &0) ==> u = (u * inv t) * t`]);
2835 TYPIFY `~(U INTER affine hull {vec 0, e} = {})` ASM_CASES_TAC;
2836 BY(ASM_REWRITE_TAC[]);
2837 RULE_ASSUM_TAC(REWRITE_RULE[]) THEN ASM_REWRITE_TAC[];
2838 REWRITE_TAC[arith `vec 0 - x = -- x`];
2839 REWRITE_TAC[arith `-- (t % e) = t % (-- e)`];
2840 REWRITE_TAC[VECTOR_MUL_ASSOC];
2841 BY(ASM_MESON_TAC[arith `~(t = &0) ==> u = (u * inv t) * t`])
2845 let projection_scale = prove_by_refinement(
2846 `!e u t. (~(t = &0)) ==> projection (t % e) u = projection e u`,
2849 REPEAT WEAKER_STRIP_TAC;
2850 REWRITE_TAC[Sphere.projection];
2851 REWRITE_TAC[DOT_LMUL;DOT_RMUL];
2852 REWRITE_TAC[VECTOR_MUL_ASSOC];
2853 TYPIFY ` ((t * (u dot e)) / (t * t * (e dot e)) * t) = (u dot e) / (e dot e)` (C SUBGOAL_THEN SUBST1_TAC);
2854 TYPIFY `e dot e = &0` ASM_CASES_TAC;
2857 Calc_derivative.CALC_ID_TAC;
2858 BY(ASM_TAC THEN REAL_ARITH_TAC);
2863 let azim_cycle_scale = prove_by_refinement(
2864 `!U t e . (&0 < t) ==>
2865 azim_cycle U (vec 0) (t % e) = azim_cycle U (vec 0) e `,
2868 REPEAT WEAKER_STRIP_TAC;
2869 REWRITE_TAC[FUN_EQ_THM];
2871 TYPIFY `U SUBSET {x}` ASM_CASES_TAC;
2872 BY(ASM_SIMP_TAC[Wrgcvdr_cizmrrh.W_SUBSET_SINGLETON_IMP_IDE]);
2873 REWRITE_TAC[Trigonometry.YESEEWW];
2875 REWRITE_TAC[arith `x - vec 0 = x`];
2876 TYPIFY `(!x u. azim (vec 0) (t % e) x u = azim (vec 0) e x u) /\ (!u. projection (t % e) u = projection e u)` ENOUGH_TO_SHOW_TAC;
2877 BY(DISCH_THEN (unlist REWRITE_TAC));
2878 ASM_SIMP_TAC[AZIM_SPECIAL_SCALE];
2880 BY(ASM_SIMP_TAC[projection_scale;arith `&0 < t ==> ~(t = &0)`])
2884 let AZIM_CYCLE_SING_ALT = prove_by_refinement(
2885 `!x u v w. azim_cycle {v} x u w = v`,
2888 REWRITE_TAC[Sphere.azim_cycle];
2889 REPEAT WEAKER_STRIP_TAC;
2890 TYPIFY `v = w` ASM_CASES_TAC;
2891 BY(ASM_REWRITE_TAC[SUBSET_REFL]);
2892 TYPIFY_GOAL_THEN `~({v} SUBSET {w})` (unlist REWRITE_TAC);
2893 BY(FIRST_X_ASSUM MP_TAC THEN SET_TAC[]);
2894 TYPIFY_GOAL_THEN `!a b. {a} (b:real^3) <=> b IN {a}` (unlist REWRITE_TAC);
2896 REWRITE_TAC[IN_SING];
2899 FIRST_X_ASSUM_ST `azim` MP_TAC;
2901 TYPIFY `v` EXISTS_TAC;
2903 REPEAT WEAKER_STRIP_TAC;
2904 BY(ASM_REWRITE_TAC[arith `x <= x`])
2908 let IDENTIFY_AZIM_CYCLE_SIMPLE = prove_by_refinement(
2909 `!W v w p u. ~(W SUBSET {p}) /\ p IN W /\
2911 (~(u = p) /\ u IN W) /\
2912 (!q. ~(q = p) /\ q IN W /\ ~(q =u) ==> azim v w p u < azim v w p q)
2913 ==> azim_cycle W v w p = u`,
2916 REPEAT WEAKER_STRIP_TAC;
2917 MATCH_MP_TAC Wrgcvdr_cizmrrh.IDENTIFY_AZIM_CYCLE;
2920 BY(ASM_MESON_TAC [Wrgcvdr_cizmrrh.CYCLIC_SET_IMP_NOT_COLLINEAR]);
2922 BY(ASM_MESON_TAC[IN]);
2923 REPEAT WEAKER_STRIP_TAC;
2924 TYPIFY `q = u` ASM_CASES_TAC;
2926 BY(MESON_TAC[arith `x<=x`]);
2928 FIRST_X_ASSUM MATCH_MP_TAC;
2929 BY(ASM_MESON_TAC[IN])
2933 let coplanar_cross_scale = prove_by_refinement(
2934 `!u1 u2 v1 v2. coplanar {vec 0,u1,u2,v1,v2} /\ &0 < (v1 cross v2) dot (u1 cross u2) ==>
2935 (?t. &0 < t /\ v1 cross v2 = t % (u1 cross u2))`,
2938 REPEAT WEAKER_STRIP_TAC;
2939 TYPIFY `~collinear {vec 0,u1,u2}` (C SUBGOAL_THEN ASSUME_TAC);
2940 REWRITE_TAC[GSYM CROSS_EQ_0];
2942 FIRST_X_ASSUM_ST `dot` MP_TAC THEN ASM_REWRITE_TAC[];
2943 REWRITE_TAC[DOT_RZERO];
2945 INTRO_TAC coplanar_in_affine_hull [`(vec 0):real^3`;`u1`;`u2`;`v1`];
2946 INTRO_TAC coplanar_in_affine_hull [`(vec 0):real^3`;`u1`;`u2`;`v2`];
2948 TYPIFY_GOAL_THEN `coplanar {v2,vec 0,u1,u2} /\ coplanar {v1,vec 0,u1,u2} ` (unlist REWRITE_TAC);
2949 BY(ASM_MESON_TAC[COPLANAR_SUBSET;SET_RULE `{v2,v0,u1,u2} SUBSET {v0,u1,u2,v1,v2}`;SET_RULE `{v1,v0,u1,u2} SUBSET {v0,u1,u2,v1,v2}`]);
2950 REPEAT WEAKER_STRIP_TAC;
2951 INTRO_TAC Ckqowsa_4_points.in_affine_hull_lemma [`u1`;`u2`;`v1`];
2952 INTRO_TAC Ckqowsa_4_points.in_affine_hull_lemma [`u1`;`u2`;`v2`];
2954 REPEAT WEAKER_STRIP_TAC;
2955 TYPIFY `v1 cross v2 = (t1' * t2 - t2' * t1) % (u1 cross u2)` (C SUBGOAL_THEN ASSUME_TAC);
2956 ASM_REWRITE_TAC[CROSS_RADD;CROSS_LADD;CROSS_RMUL;CROSS_LMUL;CROSS_REFL];
2957 TYPIFY `u2 cross u1 = -- (u1 cross u2)` (C SUBGOAL_THEN SUBST1_TAC);
2958 BY(MESON_TAC[CROSS_SKEW]);
2959 BY(VECTOR_ARITH_TAC);
2960 TYPIFY `t1' * t2 - t2' * t1` EXISTS_TAC;
2962 FIRST_X_ASSUM_ST `dot` MP_TAC;
2963 ASM_REWRITE_TAC[DOT_LMUL];
2964 GMATCH_SIMP_TAC (CONJUNCT2 Real_ext.REAL_PROP_POS_LMUL);
2965 REWRITE_TAC[DOT_POS_LT];
2966 BY(ASM_MESON_TAC[CROSS_EQ_0])
2970 let azim_cycle_distinct = prove_by_refinement(
2971 `!U e v w. FINITE U /\ v IN U /\ w IN U /\ ~(v = w) /\
2972 (!v. v IN U ==> ~(e dot (v cross azim_cycle U (vec 0) e v) = &0)) ==>
2973 (&0 < azim (vec 0) e v w)`,
2976 REPEAT WEAKER_STRIP_TAC;
2977 TYPIFY `~(e = vec 0)` (C SUBGOAL_THEN ASSUME_TAC);
2979 FIRST_X_ASSUM (C INTRO_TAC [`v`]);
2980 BY(ASM_REWRITE_TAC[DOT_LZERO]);
2981 TYPIFY `!v. v IN U ==> ~collinear {vec 0,e,v}` (C SUBGOAL_THEN ASSUME_TAC);
2982 GEN_TAC THEN DISCH_TAC;
2983 ASM_REWRITE_TAC[COLLINEAR_LEMMA_ALT;DE_MORGAN_THM];
2984 REPEAT WEAKER_STRIP_TAC;
2985 FIRST_X_ASSUM (C INTRO_TAC [`v'`]);
2986 ASM_REWRITE_TAC[CROSS_LMUL;DOT_RMUL;DOT_CROSS_SELF];
2988 TYPIFY `~collinear {vec 0,e,azim_cycle U (vec 0) e v}` (C SUBGOAL_THEN ASSUME_TAC);
2989 BY(ASM_MESON_TAC[Polar_fan.AZIM_CYCLE_BASIC_PROPERTIES]);
2990 TYPIFY `&0 < azim (vec 0) e v (azim_cycle U (vec 0) e v)` (C SUBGOAL_THEN ASSUME_TAC);
2991 REWRITE_TAC[azim_pos_iff_nz];
2992 GMATCH_SIMP_TAC AZIM_EQ_0;
2994 GMATCH_SIMP_TAC AFF_GT_2_1;
2995 REWRITE_TAC[IN_ELIM_THM];
2997 BY(ASM_MESON_TAC[Fan.th3a]);
2998 REPEAT WEAKER_STRIP_TAC;
2999 FIRST_X_ASSUM_ST `dot` (C INTRO_TAC [`v`]);
3001 TYPED_ABBREV_TAC `u = azim_cycle U (vec 0) e v`;
3002 FIRST_X_ASSUM_ST `%` SUBST1_TAC;
3003 REWRITE_TAC[DOT_RMUL;DOT_RADD;DOT_RZERO;CROSS_LADD;CROSS_LMUL;CROSS_LZERO;CROSS_REFL;DOT_CROSS_SELF];
3005 TYPIFY `w = azim_cycle U (vec 0) e v` ASM_CASES_TAC;
3006 BY(ASM_MESON_TAC[]);
3007 INTRO_TAC Polar_fan.AZIM_CYCLE_BASIC_PROPERTIES [`U`;`(vec 0):real^3`;`e`;`v`];
3009 REPEAT WEAKER_STRIP_TAC;
3010 FIRST_X_ASSUM (C INTRO_TAC [`w`]);
3012 BY(ASM_TAC THEN REAL_ARITH_TAC)
3018 let azim_cycle_nondeg = prove_by_refinement(
3021 U = {uu i | i IN 1..r+1 } /\
3022 (!i. i IN 1..r ==> u i IN aff_gt{vec 0,u (r+1)} {u (r)} /\
3023 (!i. i IN 1..r ==> azim_cycle U (vec 0) (uu 1 cross uu 2) (uu i) = (uu (i+1))) /\
3024 azim_cycle U (vec 0) (uu 1 cross uu 2) (uu (r+1)) = u 1 /\
3025 (!i. i IN 1..r ==> &0 < (uu i cross uu (i+1)) dot (uu 1 cross uu 2))
3027 ((!i. i IN 1..r ==> ~((uu 1 cross uu 2) dot (uu i cross uu (i+1)) = &0))
3038 let azim_cycle_neg = prove_by_refinement(
3039 `!U e v w. FINITE U /\ v IN U /\ azim_cycle U (vec 0) e v = w /\
3040 (!v. v IN U ==> ~(e dot (v cross azim_cycle U (vec 0) e v) = &0)) ==>
3041 (azim_cycle U (vec 0) (-- e) w = v)`,
3044 REPEAT WEAKER_STRIP_TAC;
3045 TYPIFY `~(e = vec 0)` (C SUBGOAL_THEN ASSUME_TAC);
3047 FIRST_X_ASSUM (C INTRO_TAC [`v`]);
3048 BY(ASM_REWRITE_TAC[DOT_LZERO]);
3049 TYPIFY `!v. v IN U ==> ~collinear {vec 0,e,v}` (C SUBGOAL_THEN ASSUME_TAC);
3050 GEN_TAC THEN DISCH_TAC;
3051 ASM_REWRITE_TAC[COLLINEAR_LEMMA_ALT;DE_MORGAN_THM];
3052 REPEAT WEAKER_STRIP_TAC;
3053 FIRST_X_ASSUM (C INTRO_TAC [`v'`]);
3054 ASM_REWRITE_TAC[CROSS_LMUL;DOT_RMUL;DOT_CROSS_SELF];
3056 TYPIFY `w IN U` (C SUBGOAL_THEN ASSUME_TAC);
3057 BY(ASM_MESON_TAC[Polar_fan.AZIM_CYCLE_BASIC_PROPERTIES]);
3059 INTRO_TAC Polar_fan.AZIM_CYCLE_BASIC_PROPERTIES [`U`;`(vec 0):real^3`;`-- (e:real^3)`;`w`];
3061 REPEAT WEAKER_STRIP_TAC;
3062 TYPIFY `~(v = w)` (C SUBGOAL_THEN ASSUME_TAC);
3064 FIRST_X_ASSUM_ST `dot` (C INTRO_TAC [`v`]);
3065 BY(ASM_REWRITE_TAC[CROSS_REFL;DOT_RZERO]);
3066 TYPIFY `&0 < azim (vec 0) e v w` (C SUBGOAL_THEN ASSUME_TAC);
3067 MATCH_MP_TAC azim_cycle_distinct;
3068 BY(ASM_MESON_TAC[]);
3069 FIRST_X_ASSUM_ST `IN` (C INTRO_TAC [`v`]);
3071 TYPED_ABBREV_TAC `w' = azim_cycle U (vec 0) (-- e) w`;
3072 TYPIFY `w' IN U` (C SUBGOAL_THEN ASSUME_TAC);
3073 BY(ASM_MESON_TAC[Polar_fan.AZIM_CYCLE_BASIC_PROPERTIES]);
3074 REPEAT (GMATCH_SIMP_TAC Yxionxl2.AZIM_COMPL_NEG);
3076 BY(ASM_MESON_TAC[]);
3078 BY(ASM_MESON_TAC[]);
3080 TYPIFY `azim (vec 0) e v w' + azim (vec 0) e w' w = azim (vec 0) e v w` (C SUBGOAL_THEN ASSUME_TAC);
3081 MATCH_MP_TAC (GSYM Fan.sum5_azim_fan);
3083 INTRO_TAC Polar_fan.AZIM_CYCLE_BASIC_PROPERTIES [`U`;`(vec 0):real^3`;`(e:real^3)`;`v`];
3085 DISCH_THEN (C INTRO_TAC [`w'`]);
3088 TYPIFY `azim (vec 0) e v w + azim (vec 0) e w w' = azim (vec 0) e v w'` (C SUBGOAL_THEN ASSUME_TAC);
3089 MATCH_MP_TAC (GSYM Fan.sum4_azim_fan);
3091 TYPIFY `&0 <= azim (vec 0) e w w' /\ &0 <= azim (vec 0) e w' w` (C SUBGOAL_THEN ASSUME_TAC);
3092 BY(REWRITE_TAC[Counting_spheres.AZIM_NN]);
3093 TYPIFY `azim (vec 0) e w w' = &0` (C SUBGOAL_THEN ASSUME_TAC);
3094 BY(ASM_TAC THEN REAL_ARITH_TAC);
3095 TYPIFY `(w' = w)` (C SUBGOAL_THEN ASSUME_TAC);
3097 INTRO_TAC azim_cycle_distinct [`U`;` (e:real^3)`;`w`;`w'`];
3100 INTRO_TAC (GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_PROPERTIES) [`U`;`w`;`-- (e:real^3)`;`(vec 0):real^3`];
3102 BY(ASM_TAC THEN SET_TAC[])
3107 let azim_cycle_neg = prove_by_refinement(
3108 `!U e v w. ~(U SUBSET {w}) /\ FINITE U /\ cyclic_set U (vec 0) e /\ v IN U /\ ~(e dot (v cross w) = &0) /\
3109 azim_cycle U (vec 0) (e ) v = w ==>
3110 azim_cycle U (vec 0) (-- e) w = v`,
3114 typ `U SUBSET {v}` asmcase
3115 art[Sphere.azim_cycle]
3118 intro (GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_PROPERTIES) [`U`;`v`;`e`;`(vec 0):real^3`]
3121 mmp IDENTIFY_AZIM_CYCLE_SIMPLE
3126 rt[arith `-- e = (-- &1) % e`]
3135 repeat (gm Yxionxl2.AZIM_COMPL_NEG)
3136 typ `~collinear {vec 0, e, w} /\ ~collinear {vec 0, e, q} /\ ~collinear {vec 0, e, v}` sat
3137 ort[setr `{a,e,w} = {w,a,e}`]
3138 repeat (gm Wrgcvdr_cizmrrh.CYCLIC_SET_IMP_NOT_COLLINEAR)
3141 rt[arith `x < y <=> ~(y <= x)`]
3143 (* COME BACK. TO HERE. still problems with degenerate cases. make azim progression condition on all of U *)
3148 let XIV_ECAU_BACK = prove_by_refinement(
3150 deformation f {w i | i <= r + 2} (a,b) /\
3152 (!i. i IN 1..r ==> w i IN aff_gt {vec 0,w (r+1) } {w r} ) /\
3153 cyclic_set {w i | i IN 1..r+1 } (vec 0) ((w 1) cross (w 2)) /\
3154 // &0 < (w r cross (w (r+1))) dot (w 1 cross w 2) /\
3155 (!i. i IN 1..r ==> &0 < (w i cross (w (i+1))) dot (w 1 cross w 2)) /\
3156 {w 1, w 2} SUBSET aff_gt {vec 0,w (r+1)} {w r} /\
3157 (!i. i IN 1..r ==> azim_cycle {w i | i IN 1..r+1} (vec 0) ((w 1) cross (w 2)) (w i) = w (i+1)) /\
3158 azim_cycle {w i | i IN 1..r+1} (vec 0) ((w 1) cross (w 2)) (w (r+1)) = w 1 /\
3159 pairwise (\i j. ~collinear {vec 0, w i, w j}) (0..(r+1)) /\
3160 pairwise (\i j. ~collinear {vec 0, w i, w j}) (1..(r+2)) /\
3161 (!i. ?e2. i IN 1..r+1 ==> &0 < e2 /\
3162 (!t. abs t < e2 ==> azim (vec 0) (f (w i) t) (f (w (i+1)) t) (f (w (i-1)) t) <= pi)) /\
3163 (!i. i IN 1..r+1 ==> &0 < azim (vec 0) (w i) (w (i+1)) (w (i-1)))
3164 ==> (?e. &0 < e /\ (!t. abs t < e ==>
3165 f (w 1) t IN wedge_ge (vec 0) (f (w (r+1)) t) (f (w (r+2)) t) (f (w (r)) t) /\
3166 f (w (r+1)) t IN wedge_ge (vec 0) (f (w 1) t) (f (w (2)) t) (f (w (0)) t)))`,
3169 REPEAT WEAKER_STRIP_TAC;
3170 TYPIFY `&0 < (w r cross (w (r+1))) dot (w 1 cross w 2)` (C SUBGOAL_THEN ASSUME_TAC);
3171 FIRST_X_ASSUM MATCH_MP_TAC;
3172 REWRITE_TAC[IN_NUMSEG];
3173 BY(ASM_REWRITE_TAC[arith `r <= (r:num)`]);
3174 MATCH_MP_TAC XIV_DEFORMATION;
3175 TYPED_ABBREV_TAC `dh = \ (i,j,k). dihV (vec 0) (w i) (w j) (w k)`;
3176 GEXISTL_TAC [`dh`;`a`;`b`];
3178 INTRO_TAC KCZXLLE_SYM [`\i. w((r+1)-i) `;`r`];
3179 REWRITE_TAC[arith `1 <= r+1 /\ ((r+1)-0 = (r+1)) /\ ((r+1)-1 = r)`];
3180 TYPIFY `{w ((r+1)-i) | i | i <= r } = {w i | i IN 1..r+1}` (C SUBGOAL_THEN SUBST1_TAC);
3181 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG];
3183 MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a <=> b)`);
3184 CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC;
3186 TYPIFY `(r+1)-i` EXISTS_TAC;
3188 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
3190 TYPIFY `(r+1)-i` EXISTS_TAC;
3192 BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
3194 BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
3195 COMMENT "collinear";
3196 TYPIFY_GOAL_THEN `(!i j. i <= r /\ j <= r /\ ~(i = j) ==> ~collinear {vec 0, w ((r+1)-i), w ((r+1)-j)})` (unlist REWRITE_TAC);
3197 REPEAT WEAKER_STRIP_TAC;
3198 RULE_ASSUM_TAC(REWRITE_RULE[pairwise]);
3199 FIRST_X_ASSUM (C INTRO_TAC [`(r+1)-i`;`(r+1)-j`]);
3201 BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
3203 TYPIFY_GOAL_THEN ` (!i. 1 <= i /\ i <= r ==> w ((r+1)-i) IN aff_gt {vec 0, w (r+1)} {w r})` (unlist REWRITE_TAC);
3204 REPEAT WEAKER_STRIP_TAC;
3205 FIRST_X_ASSUM MATCH_MP_TAC;
3206 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
3207 COMMENT "cyclic set";
3208 INTRO_TAC coplanar_cross_scale [`w 1`;`w 2`;`w r`;`w (r+1)`];
3211 REWRITE_TAC[coplanar];
3212 GEXISTL_TAC [`(vec 0):real^3`;`w r`;`w (r+1)`];
3213 TYPIFY `{vec 0,w r, w (r+1)} SUBSET affine hull {vec 0, w r, w (r + 1)} /\ {w 1, w 2} SUBSET affine hull {vec 0, w r, w (r + 1)}` ENOUGH_TO_SHOW_TAC;
3216 BY(REWRITE_TAC[Qzksykg.SET_SUBSET_AFFINE_HULL]);
3217 MATCH_MP_TAC SUBSET_TRANS;
3218 TYPIFY `aff_gt {vec 0,w(r+1)} {w r}` EXISTS_TAC;
3220 BY(ASM_REWRITE_TAC[]);
3221 TYPIFY `{vec 0,w r, w(r+1)} = {vec 0,w (r+1)} UNION {w (r)}` (C SUBGOAL_THEN SUBST1_TAC);
3223 BY(REWRITE_TAC[ AFF_GT_SUBSET_AFFINE_HULL]);
3224 REPEAT WEAKER_STRIP_TAC;
3225 TYPIFY ` cyclic_set {w i | i IN 1..r + 1} (vec 0) (w (r + 1) cross w r)` (C SUBGOAL_THEN ASSUME_TAC);
3226 ONCE_REWRITE_TAC[CROSS_SKEW];
3228 REWRITE_TAC[arith `-- (t % v) = (-- t) % v`];
3229 GMATCH_SIMP_TAC cyclic_set_scale;
3231 BY(FIRST_X_ASSUM_ST `&0 < t` MP_TAC THEN REAL_ARITH_TAC);
3232 COMMENT "azim_cycle";
3233 TYPIFY `(!i. i < r ==> azim_cycle {w i | i IN 1..r + 1} (vec 0) (w (r + 1) cross w r) (w ((r + 1) - i)) = w ((r + 1) - (i + 1)))` (C SUBGOAL_THEN ASSUME_TAC);
3234 REPEAT WEAKER_STRIP_TAC;
3235 ONCE_REWRITE_TAC[CROSS_SKEW];
3237 REWRITE_TAC[arith `-- (t % v) = t % (-- v)`];
3238 GMATCH_SIMP_TAC azim_cycle_scale;
3240 MATCH_MP_TAC azim_cycle_neg;
3243 TYPIFY `{w i | i IN 1..r+1} = IMAGE w (1..r+1)` (C SUBGOAL_THEN SUBST1_TAC);
3245 MATCH_MP_TAC FINITE_IMAGE;
3246 BY(REWRITE_TAC[FINITE_NUMSEG]);
3247 TYPIFY `(r+1)-(i+1) = r - i` (C SUBGOAL_THEN SUBST1_TAC);
3248 BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
3250 REWRITE_TAC[IN_ELIM_THM;IN_NUMSEG];
3251 TYPIFY `r- (i:num)` EXISTS_TAC;
3252 BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
3254 TYPIFY `(r+1) - i = (r - i) + 1` (C SUBGOAL_THEN SUBST1_TAC);
3255 BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
3256 FIRST_X_ASSUM MATCH_MP_TAC;
3257 BY(REWRITE_TAC[IN_NUMSEG] THEN FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
3258 REWRITE_TAC[IN_NUMSEG;IN_ELIM_THM];
3259 REPEAT WEAKER_STRIP_TAC;
3260 FIRST_X_ASSUM MP_TAC;
3262 TYPIFY `(i':num) < r+1` ASM_CASES_TAC;
3263 TYPIFY `azim_cycle {w i | 1 <= i /\ i <= r + 1} (vec 0) (w 1 cross w 2) (w i') = w (i'+1)` (C SUBGOAL_THEN SUBST1_TAC);
3264 REWRITE_TAC[GSYM IN_NUMSEG];
3265 FIRST_X_ASSUM MATCH_MP_TAC;
3266 BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
3267 MATCH_MP_TAC (arith `&0 < x ==> ~(x = &0)`);
3268 REWRITE_TAC[DOT_SYM];
3269 FIRST_X_ASSUM MATCH_MP_TAC;
3270 BY(REWRITE_TAC[IN_NUMSEG] THEN REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
3271 TYPIFY `i' = r+1` (C SUBGOAL_THEN ASSUME_TAC);
3272 BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
3273 ASM_REWRITE_TAC[GSYM IN_NUMSEG];
3274 TYPIFY `w 1 IN aff_gt {vec 0, w(r+1)} {w r}` (C SUBGOAL_THEN MP_TAC);
3275 BY(FIRST_X_ASSUM_ST `aff_gt` MP_TAC THEN SET_TAC[]);
3276 GMATCH_SIMP_TAC AFF_GT_2_1;
3277 REWRITE_TAC[IN_ELIM_THM];
3279 MATCH_MP_TAC Fan.th3a;
3280 RULE_ASSUM_TAC(REWRITE_RULE[pairwise]);
3281 FIRST_X_ASSUM MATCH_MP_TAC;
3282 REWRITE_TAC[IN_NUMSEG];
3283 BY(REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
3284 REPEAT WEAKER_STRIP_TAC;
3285 TYPED_ABBREV_TAC `e = w 1 cross w 2`;
3286 FIRST_X_ASSUM_ST `dot` MP_TAC;
3288 REWRITE_TAC[CROSS_RADD;CROSS_RMUL;CROSS_RZERO;CROSS_REFL;DOT_RMUL;DOT_RADD;DOT_RZERO];
3289 REWRITE_TAC[arith `t * &0 + x = x`];
3290 ONCE_REWRITE_TAC[CROSS_SKEW];
3291 REWRITE_TAC[DOT_RNEG;REAL_ENTIRE];
3292 ONCE_REWRITE_TAC[DOT_SYM];
3293 BY(REPEAT (FIRST_X_ASSUM_ST `&0 < x` MP_TAC) THEN REAL_ARITH_TAC);
3294 FIRST_X_ASSUM_ST `!i j k. P` MP_TAC;
3296 REPLICATE_TAC 4 (FIRST_X_ASSUM kill);
3298 COMMENT "work on dihedral angles";
3299 TYPIFY `!i j k. k IN 1..r+1 /\ j IN 1..r+1 /\ i IN 1..r+1 /\ (j < k /\ (i < j \/ k < i) \/ k < j /\ (i < k \/ j < i)) ==> azim (vec 0) (w i) (w j) (w k) = &0` (C SUBGOAL_THEN ASSUME_TAC);
3300 REWRITE_TAC[IN_NUMSEG];
3301 REPEAT WEAKER_STRIP_TAC;
3302 FIRST_X_ASSUM (C INTRO_TAC [`(r+1)-i`;`(r+1)-j`;`(r+1)-k`]);
3303 ASM_SIMP_TAC[arith `i <= r+1 ==> (r+1)-((r+1)-i) = i`];
3304 DISCH_THEN MATCH_MP_TAC;
3305 BY(REPLICATE_TAC 7 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
3306 FIRST_X_ASSUM_ST `(r+1)-i` kill;
3307 TYPIFY `!i j k. i IN 1..r+1 /\ j IN 1..r+1 /\ k IN 1..r+1 /\ ~(i = j) /\ ~(i = k) /\ azim (vec 0) (w i) (w j) (w k) = &0 ==> dihV (vec 0) (w i) (w j) (w k) = &0` (C SUBGOAL_THEN ASSUME_TAC);
3308 REPEAT WEAKER_STRIP_TAC;
3309 GMATCH_SIMP_TAC (GSYM Polar_fan.AZIM_DIHV_SAME_STRONG);
3310 RULE_ASSUM_TAC (REWRITE_RULE[pairwise]);
3311 TYPIFY_GOAL_THEN `~collinear {vec 0, w i, w j} /\ ~collinear {vec 0, w i, w k}` (unlist REWRITE_TAC);
3312 BY(CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REPLICATE_TAC 8 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);
3314 BY(MP_TAC PI_POS THEN REAL_ARITH_TAC);
3315 EXPAND_TAC "dh" THEN REWRITE_TAC[];
3316 REWRITE_TAC[SUBSET;IN_INSERT;NOT_IN_EMPTY];
3317 FIRST_X_ASSUM MP_TAC;
3320 REPEAT WEAKER_STRIP_TAC;
3321 FIRST_X_ASSUM MATCH_MP_TAC;
3322 FIRST_X_ASSUM_ST `azim` GMATCH_SIMP_TAC;
3323 FIRST_X_ASSUM_ST `IN` (unlist ASM_SIMP_TAC);
3324 REPLICATE_TAC 2(FIRST_X_ASSUM MP_TAC);
3327 REPEAT WEAKER_STRIP_TAC;
3328 FIRST_X_ASSUM MATCH_MP_TAC;
3329 FIRST_X_ASSUM_ST `azim` GMATCH_SIMP_TAC;
3330 FIRST_X_ASSUM_ST `IN` (unlist ASM_SIMP_TAC);
3331 BY(REPLICATE_TAC 1(FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
3332 REPEAT WEAKER_STRIP_TAC;
3333 FIRST_X_ASSUM MATCH_MP_TAC;
3334 FIRST_X_ASSUM_ST `azim` GMATCH_SIMP_TAC;
3335 FIRST_X_ASSUM_ST `IN` (unlist ASM_SIMP_TAC);
3336 BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC)
3340 let zlz_wedge_boundary = prove_by_refinement(
3342 convex_local_fan (V,E,FF) /\
3344 deformation f V (a,b) /\
3345 (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==>
3346 interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi) ==>
3347 (!x v. ?e3. x IN FF /\ v IN V
3349 (!t. --e3 < t /\ t < e3
3351 wedge_in_fan_ge (f (FST x) t,f (SND x) t)
3352 (IMAGE (IMAGE (\v. f v t)) E)))`,
3355 COMMENT "start here";
3356 REPEAT WEAKER_STRIP_TAC;
3357 TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
3358 MATCH_MP_TAC Local_lemmas.CVX_LO_IMP_LO;
3359 BY(ASM_REWRITE_TAC[]);
3360 INTRO_TAC (GEN_ALL Lunar_deform.XRECQNS_UPDATE) [`a`;`b`;`V`;`E`;`f`;`FF`];
3362 REPEAT WEAKER_STRIP_TAC;
3363 TYPIFY `!t. IMAGE (\s. IMAGE (\v. f v t) s) E = IMAGE (IMAGE (\v. f v t)) E /\ IMAGE (\(u,v). f u t,f v t) FF = IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF` (C SUBGOAL_THEN ASSUME_TAC);
3364 BY(REWRITE_TAC[EXTENSION;IN_IMAGE;EXISTS_PAIR_THM]);
3365 REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
3366 REPEAT WEAKER_STRIP_TAC;
3367 TYPED_ABBREV_TAC `w = FST x`;
3368 TYPIFY `x = (w,rho_node1 FF w)` (C SUBGOAL_THEN ASSUME_TAC);
3369 TYPIFY `FST x,SND x = (w,rho_node1 FF w)` ENOUGH_TO_SHOW_TAC;
3370 BY(REWRITE_TAC[PAIR]);
3371 ASM_REWRITE_TAC[PAIR_EQ];
3372 MATCH_MP_TAC EQ_SYM;
3373 MATCH_MP_TAC Local_lemmas.DETER_RHO_NODE;
3374 BY(ASM_MESON_TAC[PAIR]);
3376 FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
3377 TYPIFY `w IN V` (C SUBGOAL_THEN ASSUME_TAC);
3378 BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V]);
3379 TYPIFY `v IN {w, rho_node1 FF w, ivs_rho_node1 FF w}` ASM_CASES_TAC;
3380 INTRO_TAC zlz_wedge_refl [`a`;`b`;`V`;`E`;`FF`;`f`];
3382 DISCH_THEN (C INTRO_TAC [`v`;`w`]);
3383 BY(ASM_REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY]);
3384 TYPIFY `rho_node1 FF w IN V` (C SUBGOAL_THEN ASSUME_TAC);
3385 MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
3386 BY(ASM_REWRITE_TAC[]);
3387 TYPIFY `ivs_rho_node1 FF w IN V` (C SUBGOAL_THEN ASSUME_TAC);
3388 MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_IVS_IN_V;
3389 BY(ASM_REWRITE_TAC[]);
3390 TYPIFY `v IN wedge (vec 0) w (rho_node1 FF w) (ivs_rho_node1 FF w)` ASM_CASES_TAC;
3391 INTRO_TAC zlz_wedge_open [`a`;`b`;`V`;`E`;`FF`;`f`];
3393 DISCH_THEN (C INTRO_TAC [`v`;`w`]);
3394 BY(ASM_REWRITE_TAC[]);
3395 TYPIFY `v IN wedge_ge (vec 0) w (rho_node1 FF w) (ivs_rho_node1 FF w)` (C SUBGOAL_THEN ASSUME_TAC);
3396 RULE_ASSUM_TAC(REWRITE_RULE[Localization.convex_local_fan]);
3397 ASM_TAC THEN REPEAT WEAKER_STRIP_TAC;
3398 FIRST_X_ASSUM_ST `wedge_in_fan_ge` (C INTRO_TAC [`w,rho_node1 FF w`]);
3400 REWRITE_TAC[SUBSET];
3401 REPEAT WEAKER_STRIP_TAC;
3402 FIRST_X_ASSUM (C INTRO_TAC [`v`]);
3404 GMATCH_SIMP_TAC Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND;
3405 BY(ASM_MESON_TAC[]);
3406 TYPIFY `azim (vec 0) w (rho_node1 FF w) v = &0 \/ azim (vec 0) w (rho_node1 FF w) v = azim (vec 0) w (rho_node1 FF w) (ivs_rho_node1 FF w)` (C SUBGOAL_THEN ASSUME_TAC);
3407 FIRST_X_ASSUM MP_TAC;
3408 BY(ASM_REWRITE_TAC[Reuhady.WEDGE_GE_WEDGE;IN_UNION;IN_ELIM_THM]);
3409 TYPIFY `?r. r < CARD V /\ v = ITER r (rho_node1 FF) w` (C SUBGOAL_THEN MP_TAC);
3410 INTRO_TAC (GEN_ALL Local_lemmas.LOFA_IMP_LT_CARD_SET_V) [`E`;`FF`;`V`;`w`];
3411 REWRITE_TAC[EXTENSION;IN_ELIM_THM];
3413 DISCH_THEN (C INTRO_TAC [`v`]);
3414 BY(ASM_REWRITE_TAC[]);
3415 REPEAT WEAKER_STRIP_TAC;
3417 FIRST_X_ASSUM (RULE_ASSUM_TAC o (unlist REWRITE_RULE));
3418 TYPIFY `1 < r /\ r < CARD V - 1` (C SUBGOAL_THEN ASSUME_TAC);
3419 TYPIFY `~(r = 0) /\ ~(r = 1) /\ ~(r = CARD V - 1)` ENOUGH_TO_SHOW_TAC;
3420 BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
3421 REWRITE_TAC[GSYM DE_MORGAN_THM];
3423 FIRST_X_ASSUM_ST `~(ITER r f w IN s INSERT t)` MP_TAC;
3424 REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY];
3425 REPEAT (FIRST_X_ASSUM DISJ_CASES_TAC) THEN ASM_REWRITE_TAC[ITER;ITER_1];
3426 BY(ASM_MESON_TAC[Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1]);
3427 BY(ASM_MESON_TAC[Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1]);
3428 INTRO_TAC (GEN_ALL Local_lemmas.EGHNAVX) [`E`;`V`;`(\i. azim (vec 0) w (rho_node1 FF w) (ITER i (rho_node1 FF) w))`;`FF`;`r`;`w`;`(\i. ITER i (rho_node1 FF) w)`;`CARD V` ];
3429 ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM;ITER_1];
3431 MATCH_MP_TAC Nkezbfc_local.PROPERTIES_GENERIC_LOCAL_FAN;
3432 BY(ASM_MESON_TAC[]);
3433 REWRITE_TAC[LEFT_IMP_EXISTS_THM];
3434 ASM_SIMP_TAC[arith `1 < r ==> 0 < r`];
3435 (REPEAT WEAKER_STRIP_TAC);
3436 COMMENT "added material here";
3437 COMMENT "eliminate wedge_in_fan_ge";
3438 TYPIFY `?e3. &0 < e3 /\ (!t. --e3 < t /\ t < e3 ==> f (ITER r (rho_node1 FF) w) t IN wedge_ge (vec 0) (f w t) (f (rho_node1 FF w) t) (f (ivs_rho_node1 FF w) t))` ENOUGH_TO_SHOW_TAC;
3439 REPEAT WEAKER_STRIP_TAC;
3440 TYPIFY `if (e <= e3) then e else e3` EXISTS_TAC;
3442 BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC) THEN REAL_ARITH_TAC);
3443 REPEAT WEAKER_STRIP_TAC;
3444 TYPIFY `abs t < e` (C SUBGOAL_THEN ASSUME_TAC);
3445 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
3446 FIRST_X_ASSUM_ST `local_fan` (C INTRO_TAC [`t`]);
3449 INTRO_TAC deformation_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`w`;`t`];
3452 INTRO_TAC deformation_ivs_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`w`;`t`];
3456 GMATCH_SIMP_TAC Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND;
3458 TYPIFY `IMAGE (\v. f v t) V` EXISTS_TAC;
3460 REWRITE_TAC[IN_IMAGE];
3461 TYPIFY `w` EXISTS_TAC;
3462 BY(ASM_REWRITE_TAC[]);
3463 FIRST_X_ASSUM_ST `wedge_ge` (C INTRO_TAC [`t`]);
3465 DISCH_THEN MATCH_MP_TAC;
3466 BY(REPLICATE_TAC 6 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
3467 INTRO_TAC zlz_azim [`a`;`b`;`V`;`E`;`FF`;`f`];
3469 BY(ASM_REWRITE_TAC[]);
3471 TYPIFY `!v. v IN V ==> &0 < azim (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v)` (C SUBGOAL_THEN ASSUME_TAC);
3472 REPEAT WEAKER_STRIP_TAC;
3473 INTRO_TAC (GEN_ALL Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS) [`E`;`V`;`FF`];
3475 DISCH_THEN (GMATCH_SIMP_TAC o GSYM);
3477 MATCH_MP_TAC Local_lemmas.INTERIOR_ANGLE1_POS;
3478 BY(ASM_REWRITE_TAC[]);
3479 COMMENT "azim_in_fan -> azim";
3480 TYPIFY `!v. ?e2. v IN V ==> &0 < e2 /\ (!t. --e2 < t /\ t < e2 ==> azim (vec 0) (f v t) (f (rho_node1 FF v) t) (f (ivs_rho_node1 FF v) t) <= pi)` (C SUBGOAL_THEN ASSUME_TAC);
3481 REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
3482 REPEAT WEAKER_STRIP_TAC;
3483 FIRST_X_ASSUM (C INTRO_TAC [`v', rho_node1 FF v'`]);
3484 REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
3485 GMATCH_SIMP_TAC Lunar_deform.LOCAL_FAN_RHO_NODE_PROS2;
3487 BY(ASM_MESON_TAC[]);
3488 REPEAT WEAKER_STRIP_TAC;
3489 TYPIFY `if (e <= e2) then e else e2` EXISTS_TAC;
3491 BY(REPEAT (FIRST_X_ASSUM_ST `&0 < e` MP_TAC) THEN REAL_ARITH_TAC);
3492 REPEAT WEAKER_STRIP_TAC;
3493 TYPIFY `abs t < e /\ abs t < e2` (C SUBGOAL_THEN ASSUME_TAC);
3494 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
3495 FIRST_X_ASSUM_ST `local_fan` (C INTRO_TAC [`t`]);
3498 INTRO_TAC deformation_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`v'`;`t`];
3501 INTRO_TAC deformation_ivs_rho_node1_equivariant1 [`f`;`V`;`E`;`FF`;`a`;`b`;`v'`;`t`];
3505 FIRST_X_ASSUM_ST `azim_in_fan` (C INTRO_TAC [`t`]);
3506 ASM_REWRITE_TAC[arith `-- e2 < t /\ t < e2 <=> abs t < e2`];
3507 MATCH_MP_TAC (arith `(a = b) ==> (a <= pi ==> b <= pi)`);
3509 GMATCH_SIMP_TAC Local_lemmas1.AZIM_IN_FAN_RHOND_IVS_RHOND;
3510 TYPIFY `IMAGE (\v. f v t) V` EXISTS_TAC;
3512 REWRITE_TAC[IN_IMAGE];
3513 TYPIFY `v'` EXISTS_TAC;
3514 BY(ASM_REWRITE_TAC[]);
3515 REPLICATE_TAC 2(FIRST_X_ASSUM MP_TAC THEN BURY_MP_TAC);
3517 COMMENT "end added";
3518 COMMENT "MAIN BRANCH: follow forward azim = 0";
3519 FIRST_X_ASSUM DISJ_CASES_TAC;
3520 FIRST_X_ASSUM MP_TAC;
3523 FIRST_X_ASSUM_ST `interior_angle1` MP_TAC;
3525 FIRST_X_ASSUM MP_TAC;
3526 REPLICATE_TAC 2 (FIRST_X_ASSUM kill);
3527 REPEAT WEAKER_STRIP_TAC;
3529 INTRO_TAC Local_lemmas.KOMWBWC [`E`;`V`;`affine hull {(vec 0),w,rho_node1 FF w}`;`r`;`FF`;`{ITER i (rho_node1 FF) w | i <= r}`;`w cross rho_node1 FF w`;`ITER r (rho_node1 FF) w`;`w`];
3534 GEXISTL_TAC [`(vec 0):real^3`;`w`;`rho_node1 FF w`];
3536 BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2]);
3538 MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
3540 REWRITE_TAC[SUBSET;IN_ELIM_THM];
3541 REPEAT WEAKER_STRIP_TAC;
3543 ASM_CASES_TAC `i=0`;
3544 ASM_REWRITE_TAC[ITER];
3545 MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
3547 TYPIFY `aff_gt {vec 0,w} {rho_node1 FF w} SUBSET affine hull {vec 0,w,rho_node1 FF w}` ENOUGH_TO_SHOW_TAC;
3548 FIRST_X_ASSUM (C INTRO_TAC [`ITER i (rho_node1 FF) w`;`i`]);
3549 ASM_SIMP_TAC[arith `~(i=0) ==> (0 < i)`];
3551 TYPIFY `{vec 0,w,rho_node1 FF w } = {vec 0,w} UNION {rho_node1 FF w}` (C SUBGOAL_THEN SUBST1_TAC);
3553 BY(REWRITE_TAC[AFF_GT_SUBSET_AFFINE_HULL]);
3554 REPEAT WEAKER_STRIP_TAC;
3555 COMMENT "abbreviate uu";
3556 TYPIFY `ivs_rho_node1 FF w IN V` (C SUBGOAL_THEN ASSUME_TAC);
3557 MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_IVS_IN_V;
3558 BY(ASM_REWRITE_TAC[]);
3559 TYPIFY `!i. ITER i (rho_node1 FF) (ivs_rho_node1 FF w) IN V` (C SUBGOAL_THEN ASSUME_TAC);
3560 MATCH_MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V;
3561 BY(ASM_REWRITE_TAC[]);
3562 TYPED_ABBREV_TAC `w0 = ivs_rho_node1 FF w`;
3563 TYPED_ABBREV_TAC `uu = (\i. ITER i (rho_node1 FF) w0)`;
3564 TYPIFY `!i. ITER i (rho_node1 FF) w0 = uu i` (C SUBGOAL_THEN ASSUME_TAC);
3567 TYPIFY `w0 = uu 0 /\ w = uu 1 /\ rho_node1 FF w = uu 2 /\ (!i. ITER i (rho_node1 FF) w = uu (i+1))` (C SUBGOAL_THEN ASSUME_TAC);
3569 REWRITE_TAC[ITER;ITER_1];
3571 REWRITE_TAC[arith `2 = 1+1`;GSYM ITER_ADD;ITER_1];
3572 REPEAT (GMATCH_SIMP_TAC Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS);
3573 BY(ASM_MESON_TAC[]);
3575 FIRST_X_ASSUM (fun t -> RULE_ASSUM_TAC(REWRITE_RULE[t]) THEN ASSUME_TAC t);
3576 COMMENT "apply XIV_ECAU";
3577 TYPIFY `(?e3. &0 < e3 /\ (!t. abs t < e3 ==> f (uu 1) t IN wedge_ge (vec 0) (f (uu (r + 1)) t) (f (uu (r + 2)) t) (f (uu r) t) /\ f (uu (r + 1)) t IN wedge_ge (vec 0) (f (uu 1) t) (f (uu 2) t) (f (uu 0) t)))` ENOUGH_TO_SHOW_TAC;
3578 REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`];
3580 MATCH_MP_TAC XIV_ECAU;
3581 GEXISTL_TAC [`a`;`b`];
3582 COMMENT "cyclic set condition";
3583 TYPIFY `{uu i | i IN 1 .. r+1} = {uu (i+1) | i <= r}` (C SUBGOAL_THEN SUBST1_TAC);
3584 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG];
3586 MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a <=> b)`);
3587 CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC;
3588 TYPIFY `PRE i` EXISTS_TAC;
3589 ASM_SIMP_TAC[arith `1 <= i ==> PRE i + 1 = i`];
3590 BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
3591 TYPIFY `i+1` EXISTS_TAC;
3593 BY(REPLICATE_TAC 2(FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
3595 COMMENT "deformation condition";
3597 MATCH_MP_TAC deformation_subset;
3598 TYPIFY `V` EXISTS_TAC;
3599 ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM];
3600 BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
3603 REWRITE_TAC[IN_NUMSEG];
3604 REPEAT WEAKER_STRIP_TAC;
3605 GMATCH_SIMP_TAC (arith `2 <= i ==> i = PRE i + 1`);
3607 FIRST_X_ASSUM MATCH_MP_TAC;
3608 TYPIFY `uu (PRE i + 1)` EXISTS_TAC;
3609 BY(REWRITE_TAC[] THEN (REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC));
3610 COMMENT "azim_cycle";
3612 REPEAT WEAKER_STRIP_TAC;
3613 FIRST_X_ASSUM (C INTRO_TAC [`uu i`;`PRE i`]);
3614 DISCH_THEN GMATCH_SIMP_TAC;
3616 BY(FIRST_X_ASSUM MP_TAC THEN (REWRITE_TAC[IN_NUMSEG]) THEN MESON_TAC[arith `1 <= i ==> PRE i + 1 = i`;arith `i <= r /\ 1 <= i ==> PRE i < r`]);
3617 TYPIFY `uu i = ITER i (rho_node1 FF) (uu 0) /\ uu (i+1) = ITER (i+1) (rho_node1 FF) (uu 0)` ENOUGH_TO_SHOW_TAC;
3618 DISCH_THEN (unlist REWRITE_TAC);
3619 REWRITE_TAC[arith `i + 1 = 1 +i`];
3620 BY(REWRITE_TAC[GSYM ITER_ADD;ITER_1]);
3621 BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
3622 TYPIFY `!i. 1 <= i ==> rho_node1 FF (uu i) = uu (i+1) /\ ivs_rho_node1 FF (uu i) = (uu (i-1))` (C SUBGOAL_THEN ASSUME_TAC);
3623 (FIRST_X_ASSUM_ST `ITER` kill);
3624 FIRST_X_ASSUM_ST `ITER` ((unlist ONCE_REWRITE_TAC) o GSYM);
3625 REPEAT WEAKER_STRIP_TAC;
3626 REWRITE_TAC[arith `i+1 = 1+i`];
3627 REWRITE_TAC[GSYM ITER_ADD;ITER_1];
3628 GMATCH_SIMP_TAC (arith `1 <= i ==> i = 1 + (i - 1)`);
3629 ASM_REWRITE_TAC[GSYM ITER_ADD;ITER_1];
3630 GMATCH_SIMP_TAC Local_lemmas.IVS_RHO_IDD;
3632 BY(ASM_MESON_TAC[]);
3633 REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC);
3634 BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
3636 TYPIFY_GOAL_THEN ` (!i. i IN 1..r + 1 ==> &0 < azim (vec 0) (uu i) (uu (i + 1)) (uu (i - 1)))` (unlist REWRITE_TAC);
3637 REPEAT WEAKER_STRIP_TAC;
3638 FIRST_X_ASSUM_ST `&0 < azim a b c d` (C INTRO_TAC [`uu i`]);
3640 BY(ASM_MESON_TAC[]);
3641 TYPIFY `rho_node1 FF (uu i) = uu (i+1) /\ ivs_rho_node1 FF (uu i) = (uu (i-1))` ENOUGH_TO_SHOW_TAC;
3642 BY(DISCH_THEN (unlist REWRITE_TAC));
3643 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN MESON_TAC[]);
3644 COMMENT "azim <= pi";
3645 TYPIFY_GOAL_THEN `(!i. ?e2. i IN 1..r + 1 ==> &0 < e2 /\ (!t. abs t < e2 ==> azim (vec 0) (f (uu i) t) (f (uu (i + 1)) t) (f (uu (i - 1)) t) <= pi))` (unlist REWRITE_TAC);
3647 REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
3649 FIRST_X_ASSUM_ST `azim a b c d <= pi` (C INTRO_TAC [`uu i`]);
3650 REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
3652 BY(ASM_MESON_TAC[]);
3653 (REPEAT WEAKER_STRIP_TAC);
3654 TYPIFY `e2` EXISTS_TAC;
3656 REPEAT WEAKER_STRIP_TAC;
3657 FIRST_X_ASSUM (C INTRO_TAC [`t`]);
3658 ASM_REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`];
3659 TYPIFY `rho_node1 FF (uu i) = uu(i+1) /\ ivs_rho_node1 FF (uu i) = uu (i - 1)` ENOUGH_TO_SHOW_TAC;
3660 BY(DISCH_THEN (unlist REWRITE_TAC));
3661 BY(REPLICATE_TAC 4 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN MESON_TAC[]);
3663 REWRITE_TAC[pairwise];
3664 TYPIFY `!i. uu (i) IN V` (C SUBGOAL_THEN ASSUME_TAC);
3665 BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]);
3666 TYPIFY `(!i j. i IN 0..r+1 /\ j IN 0..r+1 /\ ~(i = j)==> ~(uu i = uu j)) /\ (!i j. i IN 1..r+2 /\ j IN 1..r+2 /\ ~(i=j) ==> ~(uu i = uu j))` ENOUGH_TO_SHOW_TAC;
3667 REPEAT (FIRST_X_ASSUM_ST `azim` kill);
3668 BY(ASM_MESON_TAC[PROPERTIES_GENERIC_LOCAL_FAN_ALT]);
3670 REWRITE_TAC[IN_NUMSEG];
3671 REPEAT WEAKER_STRIP_TAC;
3672 FIRST_X_ASSUM MP_TAC;
3673 FIRST_X_ASSUM_ST `ITER` kill;
3675 FIRST_X_ASSUM_ST `ITER` ((unlist ONCE_REWRITE_TAC) o GSYM);
3676 BY(ASM_MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA;arith `i <= r+1 /\ 1 < r /\ r < CARD V - 1 ==> i < CARD V`]);
3677 TYPIFY `!i. 1 <= i ==> uu i = ITER (PRE i) (rho_node1 FF) (w)` (C SUBGOAL_THEN ASSUME_TAC);
3679 BY(MESON_TAC[arith `1 <= i ==> PRE i + 1 = i`]);
3680 REWRITE_TAC[IN_NUMSEG];
3681 REPEAT WEAKER_STRIP_TAC;
3682 FIRST_X_ASSUM MP_TAC;
3684 FIRST_X_ASSUM_ST `ITER` (REPEAT o GMATCH_SIMP_TAC);
3685 TYPIFY `w IN V` (C SUBGOAL_THEN MP_TAC);
3686 BY(ASM_REWRITE_TAC[]);
3687 TYPIFY `PRE i < CARD V /\ PRE j < CARD V` (C SUBGOAL_THEN MP_TAC);
3688 BY(REPEAT (FIRST_X_ASSUM_ST `CARD` MP_TAC) THEN REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[arith `1<= i /\ i <= r+2 /\ 1 < r /\ r < CARD V - 1 ==> PRE i < CARD V`]);
3689 REPEAT (FIRST_X_ASSUM_ST `local_fan` MP_TAC);
3690 REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC);
3691 BY(MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA;arith `1 <= i /\ 1 <= j /\ PRE i = PRE j ==> (i = j)`]);
3692 (COMMENT "SECOND MAIN BRANCH");
3693 FIRST_X_ASSUM_ST `azim a b c d = &0` kill;
3694 TYPIFY `ITER (CARD V - 1) (rho_node1 FF) w = ivs_rho_node1 FF w` (C SUBGOAL_THEN ASSUME_TAC);
3695 GMATCH_SIMP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1;
3696 BY(ASM_MESON_TAC[]);
3697 FIRST_X_ASSUM_ST `interior_angle1` MP_TAC;
3699 REPEAT WEAKER_STRIP_TAC;
3700 TYPED_ABBREV_TAC `r' = CARD V - r`;
3701 TYPED_ABBREV_TAC `w' = ITER r (rho_node1 FF) w`;
3703 INTRO_TAC Local_lemmas.KOMWBWC [`E`;`V`;`affine hull {(vec 0),w,ivs_rho_node1 FF w}`;`r'`;`FF`;`{ITER i (rho_node1 FF) w' | i <= r'}`;`w' cross rho_node1 FF w'`;`w`;`w'`];
3708 GEXISTL_TAC [`(vec 0):real^3`;`w`;`ivs_rho_node1 FF w`];
3710 BY(ASM_MESON_TAC[Local_lemmas.LOFA_IMP_NOT_COLL_IVS]);
3712 MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
3714 REWRITE_TAC[SUBSET;IN_ELIM_THM];
3715 REPEAT WEAKER_STRIP_TAC;
3718 REWRITE_TAC[ITER_ADD];
3719 ASM_CASES_TAC `(i:num)=r'`;
3721 TYPIFY `r' + r = CARD V` (C SUBGOAL_THEN SUBST1_TAC);
3722 BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN FIRST_X_ASSUM_ST `r < CARD V - 1` MP_TAC THEN ARITH_TAC);
3723 GMATCH_SIMP_TAC Local_lemmas1.LOFA_IMP_ITER_RHO_NODE_ID2;
3725 BY(ASM_MESON_TAC[]);
3726 MATCH_MP_TAC Marchal_cells_2_new.IN_AFFINE_KY_LEMMA1;
3728 TYPIFY `aff_gt {vec 0,w} {ivs_rho_node1 FF w} SUBSET affine hull {vec 0,w,ivs_rho_node1 FF w}` ENOUGH_TO_SHOW_TAC;
3729 FIRST_X_ASSUM (C INTRO_TAC [`ITER (i+r) (rho_node1 FF) w`;`i+(r:num)`]);
3731 ASM_REWRITE_TAC[arith `r <= (i:num) + r`];
3732 BY(REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN FIRST_X_ASSUM_ST `r < CARD V - 1` MP_TAC THEN ARITH_TAC);
3734 TYPIFY `{vec 0,w,ivs_rho_node1 FF w } = {vec 0,w} UNION {ivs_rho_node1 FF w}` (C SUBGOAL_THEN SUBST1_TAC);
3736 BY(REWRITE_TAC[AFF_GT_SUBSET_AFFINE_HULL]);
3737 REPEAT WEAKER_STRIP_TAC;
3738 COMMENT "abbreviate uu, forward order";
3739 TYPIFY `ivs_rho_node1 FF w' IN V` (C SUBGOAL_THEN ASSUME_TAC);
3740 MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_IVS_IN_V;
3741 BY(ASM_REWRITE_TAC[]);
3742 TYPIFY `!i. ITER i (rho_node1 FF) (ivs_rho_node1 FF w') IN V` (C SUBGOAL_THEN ASSUME_TAC);
3743 MATCH_MP_TAC Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V;
3744 BY(ASM_REWRITE_TAC[]);
3745 TYPED_ABBREV_TAC `w0 = ivs_rho_node1 FF w'`;
3746 TYPED_ABBREV_TAC `uu = (\i. ITER i (rho_node1 FF) w0)`;
3747 TYPIFY `!i. ITER i (rho_node1 FF) w0 = uu i` (C SUBGOAL_THEN ASSUME_TAC);
3750 TYPIFY `w0 = uu 0 /\ w' = uu 1 /\ rho_node1 FF w' = uu 2 /\ (!i. ITER i (rho_node1 FF) w' = uu (i+1))` (C SUBGOAL_THEN ASSUME_TAC);
3752 REWRITE_TAC[ITER;ITER_1];
3754 REWRITE_TAC[arith `2 = 1+1`;GSYM ITER_ADD;ITER_1];
3755 REPEAT (GMATCH_SIMP_TAC Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS);
3756 BY(ASM_MESON_TAC[]);
3758 FIRST_X_ASSUM (fun t -> RULE_ASSUM_TAC(REWRITE_RULE[t]) THEN ASSUME_TAC t);
3759 TYPIFY `1 < r' /\ r' < CARD V - 1` (C SUBGOAL_THEN ASSUME_TAC);
3761 BY(FIRST_X_ASSUM_ST `1 < r /\ r < CARD V - 1` MP_TAC THEN ARITH_TAC);
3762 TYPIFY `ivs_rho_node1 FF w = uu(r')` (C SUBGOAL_THEN ASSUME_TAC);
3763 TYPIFY `r' = PRE r' + 1` (C SUBGOAL_THEN SUBST1_TAC);
3764 BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
3765 TYPIFY `uu (PRE r' + 1) = ITER (PRE r') (rho_node1 FF) (ITER r (rho_node1 FF) w)` (C SUBGOAL_THEN SUBST1_TAC);
3766 BY(ASM_MESON_TAC[]);
3767 REWRITE_TAC[ITER_ADD];
3768 TYPIFY `PRE r' + r = CARD V - 1` (C SUBGOAL_THEN SUBST1_TAC);
3770 BY(REPEAT (FIRST_X_ASSUM_ST `1 < r /\ r < CARD V-1` MP_TAC) THEN ARITH_TAC);
3771 GMATCH_SIMP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1;
3772 BY(ASM_MESON_TAC[]);
3773 TYPIFY `!i j. ITER i (rho_node1 FF) (uu j) = uu (i+j)` (C SUBGOAL_THEN ASSUME_TAC);
3774 FIRST_X_ASSUM_ST `ITER` kill;
3775 FIRST_X_ASSUM_ST `ITER` ((unlist ONCE_REWRITE_TAC) o GSYM);
3776 BY(REWRITE_TAC[ITER_ADD]);
3777 TYPIFY `w = uu (r'+1)` (C SUBGOAL_THEN ASSUME_TAC);
3778 ONCE_REWRITE_TAC[arith `r' + 1 = 1 + r'`];
3779 FIRST_X_ASSUM ((unlist ONCE_REWRITE_TAC) o GSYM);
3780 REWRITE_TAC[ITER_1];
3781 FIRST_X_ASSUM ((unlist REWRITE_TAC) o GSYM);
3782 BY(ASM_MESON_TAC[Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS]);
3783 TYPIFY `rho_node1 FF w = uu (r'+2)` (C SUBGOAL_THEN ASSUME_TAC);
3784 FIRST_X_ASSUM SUBST1_TAC;
3785 REWRITE_TAC[arith `r' + 2 = 1 + (r' + 1)`];
3786 BY(FIRST_X_ASSUM MP_TAC THEN MESON_TAC[ITER_1]);
3788 COMMENT "apply XIV_ECAU";
3789 TYPIFY `(?e3. &0 < e3 /\ (!t. abs t < e3 ==> f (uu 1) t IN wedge_ge (vec 0) (f (uu (r' + 1)) t) (f (uu (r' + 2)) t) (f (uu r') t) /\ f (uu (r' + 1)) t IN wedge_ge (vec 0) (f (uu 1) t) (f (uu 2) t) (f (uu 0) t)))` ENOUGH_TO_SHOW_TAC;
3790 REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`];
3792 MATCH_MP_TAC XIV_ECAU_BACK;
3793 GEXISTL_TAC [`a`;`b`];
3794 COMMENT "cyclic set condition";
3795 TYPIFY `{uu i | i IN 1 .. r'+1} = {uu (i+1) | i <= r'}` (C SUBGOAL_THEN SUBST1_TAC);
3796 REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_NUMSEG];
3798 MATCH_MP_TAC (TAUT `((a ==> b) /\ (b ==> a)) ==> (a <=> b)`);
3799 CONJ_TAC THEN REPEAT WEAKER_STRIP_TAC;
3800 TYPIFY `PRE i` EXISTS_TAC;
3801 ASM_SIMP_TAC[arith `1 <= i ==> PRE i + 1 = i`];
3802 BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
3803 TYPIFY `i+1` EXISTS_TAC;
3805 BY(REPLICATE_TAC 2(FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
3807 COMMENT "deformation condition";
3809 MATCH_MP_TAC deformation_subset;
3810 TYPIFY `V` EXISTS_TAC;
3811 ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM];
3812 BY(REPLICATE_TAC 10 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[]);
3813 ASM_SIMP_TAC[arith `1 < r' ==> 1 <= r'`];
3815 TYPIFY `!i. uu(i+ CARD V) = uu i` (C SUBGOAL_THEN ASSUME_TAC);
3817 INTRO_TAC Localization.PERIODIC_RHO_NODE1 [`V`;`E`;`FF`;`uu 0`];
3819 BY(ASM_MESON_TAC[]);
3820 REWRITE_TAC[Oxl_def.periodic];
3823 TYPIFY `!i. r <= i ==> ITER i (rho_node1 FF) w = uu (i - (r-1))` (C SUBGOAL_THEN ASSUME_TAC);
3824 REPEAT WEAKER_STRIP_TAC;
3825 TYPIFY `ITER i = ITER ((i-r) + r)` (C SUBGOAL_THEN SUBST1_TAC);
3827 BY(FIRST_X_ASSUM MP_TAC THEN ARITH_TAC);
3829 FIRST_X_ASSUM (C INTRO_TAC [`i - (r-1)`]);
3830 DISCH_THEN (SUBST1_TAC o GSYM);
3833 BY(FIRST_X_ASSUM MP_TAC THEN REPEAT (FIRST_X_ASSUM_ST `1 < r /\ r < CARD V - 1` MP_TAC) THEN ARITH_TAC);
3835 REWRITE_TAC[IN_NUMSEG] THEN REPEAT WEAKER_STRIP_TAC;
3836 FIRST_X_ASSUM_ST `aff_gt` (C INTRO_TAC [`ITER (i+(r-1)) (rho_node1 FF) w`;`(i+(r-1))`]);
3839 REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REPEAT (FIRST_X_ASSUM_ST `1 < r /\ r < CARD V - 1` MP_TAC);
3842 TYPIFY `(i+r-1) + r'+ 1 = i+ CARD V` ENOUGH_TO_SHOW_TAC;
3843 BY(DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[]);
3844 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REPEAT (FIRST_X_ASSUM_ST `1 < r /\ r < CARD V - 1` MP_TAC) THEN EXPAND_TAC "r'" THEN ARITH_TAC);
3846 TYPIFY_GOAL_THEN `{uu 1, uu 2} SUBSET aff_gt {vec 0, uu (r' + 1)} {uu r'}` (unlist REWRITE_TAC);
3847 REWRITE_TAC[IN_INSERT;NOT_IN_EMPTY;SUBSET];
3848 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[IN_NUMSEG;arith `1 <= 1 /\ 1 <= 2`];
3849 BY(REPEAT (FIRST_X_ASSUM_ST `1 < r /\ r < CARD V - 1` MP_TAC) THEN EXPAND_TAC "r'" THEN ARITH_TAC);
3850 BY(REPEAT (FIRST_X_ASSUM_ST `1 < r /\ r < CARD V - 1` MP_TAC) THEN EXPAND_TAC "r'" THEN ARITH_TAC);
3853 REWRITE_TAC[IN_NUMSEG] THEN REPEAT WEAKER_STRIP_TAC;
3854 FIRST_X_ASSUM_ST `&0 < (a cross b) dot c` (C INTRO_TAC [`PRE i`]);
3855 TYPIFY `PRE i < r' /\ PRE i + 1 = i /\ (PRE i+1)+1 = i+1` ENOUGH_TO_SHOW_TAC;
3857 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
3858 COMMENT "azim_cycle";
3860 REPEAT WEAKER_STRIP_TAC;
3861 FIRST_X_ASSUM (C INTRO_TAC [`uu i`;`PRE i`]);
3862 DISCH_THEN GMATCH_SIMP_TAC;
3864 BY(FIRST_X_ASSUM MP_TAC THEN (REWRITE_TAC[IN_NUMSEG]) THEN MESON_TAC[arith `1 <= i ==> PRE i + 1 = i`;arith `i <= r' /\ 1 <= i ==> PRE i < r'`]);
3865 FIRST_X_ASSUM (C INTRO_TAC [`1`;`i`]);
3866 BY(REWRITE_TAC[ITER_1;arith `1 + i = i + 1`]);
3868 FIRST_X_ASSUM_ST `azim_cycle` MP_TAC;
3869 TYPIFY_GOAL_THEN `r' < CARD FF` (unlist REWRITE_TAC);
3870 GMATCH_SIMP_TAC Local_lemmas.LOFA_IMP_CARD_FF_V_EQ;
3871 TYPIFY `V` EXISTS_TAC;
3873 BY(ASM_MESON_TAC[]);
3874 BY(FIRST_X_ASSUM_ST `r' < CARD V - 1` MP_TAC THEN ARITH_TAC);
3875 BY(FIRST_X_ASSUM_ST `w = uu(r'+1)` MP_TAC THEN MESON_TAC[]);
3877 TYPIFY `!i. rho_node1 FF (uu i) = uu(i+1)` (C SUBGOAL_THEN ASSUME_TAC);
3879 FIRST_X_ASSUM (C INTRO_TAC [`1`;`i`]);
3880 BY(REWRITE_TAC[ITER_1;arith `1+i = i+1`]);
3881 TYPIFY `!i. 1 <= i ==> ivs_rho_node1 FF (uu i) = uu (i-1)` (C SUBGOAL_THEN ASSUME_TAC);
3882 REPEAT WEAKER_STRIP_TAC;
3883 TYPED_ABBREV_TAC `a = uu(i-1)`;
3884 TYPIFY `i = 1 + (i-1)` (C SUBGOAL_THEN SUBST1_TAC);
3885 BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN ARITH_TAC);
3886 FIRST_X_ASSUM (C INTRO_TAC [`1`;`i-1`]);
3887 REWRITE_TAC[ITER_1];
3888 DISCH_THEN (SUBST1_TAC o GSYM);
3890 GMATCH_SIMP_TAC Local_lemmas.IVS_RHO_IDD;
3891 BY(ASM_MESON_TAC[]);
3892 TYPIFY_GOAL_THEN ` (!i. i IN 1..r' + 1 ==> &0 < azim (vec 0) (uu i) (uu (i + 1)) (uu (i - 1)))` (unlist REWRITE_TAC);
3893 REPEAT WEAKER_STRIP_TAC;
3894 FIRST_X_ASSUM_ST `&0 < azim a b c d` (C INTRO_TAC [`uu i`]);
3896 BY(ASM_MESON_TAC[]);
3897 TYPIFY `rho_node1 FF (uu i) = uu (i+1) /\ ivs_rho_node1 FF (uu i) = (uu (i-1))` ENOUGH_TO_SHOW_TAC;
3898 BY(DISCH_THEN (unlist REWRITE_TAC));
3899 BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN MESON_TAC[]);
3900 COMMENT "azim <= pi";
3901 TYPIFY_GOAL_THEN `(!i. ?e2. i IN 1..r' + 1 ==> &0 < e2 /\ (!t. abs t < e2 ==> azim (vec 0) (f (uu i) t) (f (uu (i + 1)) t) (f (uu (i - 1)) t) <= pi))` (unlist REWRITE_TAC);
3903 REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
3905 FIRST_X_ASSUM_ST `azim a b c d <= pi` (C INTRO_TAC [`uu i`]);
3906 REWRITE_TAC[RIGHT_EXISTS_IMP_THM];
3908 BY(ASM_MESON_TAC[]);
3909 (REPEAT WEAKER_STRIP_TAC);
3910 TYPIFY `e2` EXISTS_TAC;
3912 REPEAT WEAKER_STRIP_TAC;
3913 FIRST_X_ASSUM (C INTRO_TAC [`t`]);
3914 ASM_REWRITE_TAC[arith `-- e < t /\ t < e <=> abs t < e`];
3915 TYPIFY `ivs_rho_node1 FF (uu i) = uu (i - 1)` ENOUGH_TO_SHOW_TAC;
3916 BY(DISCH_THEN (unlist REWRITE_TAC));
3917 FIRST_X_ASSUM MATCH_MP_TAC;
3918 BY(REPLICATE_TAC 3 (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IN_NUMSEG] THEN MESON_TAC[]);
3920 REWRITE_TAC[pairwise];
3921 TYPIFY `!i. uu (i) IN V` (C SUBGOAL_THEN ASSUME_TAC);
3922 BY(ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_ITER_RHO_NODE_IN_V]);
3923 TYPIFY `(!i j. i IN 0..r'+1 /\ j IN 0..r'+1 /\ ~(i = j)==> ~(uu i = uu j)) /\ (!i j. i IN 1..r'+2 /\ j IN 1..r'+2 /\ ~(i=j) ==> ~(uu i = uu j))` ENOUGH_TO_SHOW_TAC;
3924 REPEAT (FIRST_X_ASSUM_ST `azim` kill);
3925 BY(ASM_MESON_TAC[PROPERTIES_GENERIC_LOCAL_FAN_ALT]);
3927 REWRITE_TAC[IN_NUMSEG];
3928 REPEAT WEAKER_STRIP_TAC;
3929 FIRST_X_ASSUM MP_TAC;
3930 (REPLICATE_TAC 3 (FIRST_X_ASSUM_ST `ITER` kill));
3932 FIRST_X_ASSUM_ST `ITER` ((unlist ONCE_REWRITE_TAC) o GSYM);
3933 BY(ASM_MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA;arith `i <= r'+1 /\ 1 < r' /\ r' < CARD V - 1 ==> i < CARD V`]);
3934 TYPIFY `!i. 1 <= i ==> uu i = ITER (PRE i) (rho_node1 FF) (w')` (C SUBGOAL_THEN ASSUME_TAC);
3936 BY(MESON_TAC[arith `1 <= i ==> PRE i + 1 = i`]);
3937 REWRITE_TAC[IN_NUMSEG];
3938 REPEAT WEAKER_STRIP_TAC;
3939 FIRST_X_ASSUM MP_TAC;
3941 FIRST_X_ASSUM_ST `ITER` (REPEAT o GMATCH_SIMP_TAC);
3942 TYPIFY `w' IN V` (C SUBGOAL_THEN MP_TAC);
3943 BY(ASM_REWRITE_TAC[]);
3944 TYPIFY `PRE i < CARD V /\ PRE j < CARD V` (C SUBGOAL_THEN MP_TAC);
3945 BY(REPEAT (FIRST_X_ASSUM_ST `CARD` MP_TAC) THEN REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC) THEN MESON_TAC[arith `1<= i /\ i <= r'+2 /\ 1 < r' /\ r' < CARD V - 1 ==> PRE i < CARD V`]);
3946 REPEAT (FIRST_X_ASSUM_ST `local_fan` MP_TAC);
3947 REPLICATE_TAC 5 (FIRST_X_ASSUM MP_TAC);
3948 BY(MESON_TAC[Local_lemmas1.LT_CARD_MONO_LOFA;arith `1 <= i /\ 1 <= j /\ PRE i = PRE j ==> (i = j)`])
3955 convex_local_fan (V,E,FF) /\
3957 deformation f V (a,b) /\
3958 (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==>
3959 interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi)
3961 (!t. --e < t /\ t < e
3962 ==> convex_local_fan
3963 (IMAGE (\v. f v t) V,
3964 IMAGE (IMAGE (\v. f v t)) E,
3965 IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) /\
3966 generic (IMAGE (\v. f v t) V)
3967 (IMAGE (IMAGE (\v. f v t)) E)))`;;
3970 let ZLZTHIC = prove_by_refinement(
3972 convex_local_fan (V,E,FF) /\
3974 deformation f V (a,b) /\
3975 (!v t. v IN V /\ t IN real_interval (a,b) /\ interior_angle1 (vec 0) FF v = pi ==>
3976 interior_angle1 (vec 0) ( IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) (f v t) <= pi)
3978 (!t. --e < t /\ t < e
3979 ==> convex_local_fan
3980 (IMAGE (\v. f v t) V,
3981 IMAGE (IMAGE (\v. f v t)) E,
3982 IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) /\
3983 generic (IMAGE (\v. f v t) V)
3984 (IMAGE (IMAGE (\v. f v t)) E)))`,
3987 REPEAT WEAKER_STRIP_TAC;
3988 MATCH_MP_TAC zlz_reduction;
3989 GEXISTL_TAC [`a`;`b`];
3992 MATCH_MP_TAC zlz_generic;
3993 GEXISTL_TAC [`a`;`b`;`E`];
3994 BY(ASM_REWRITE_TAC[]);
3996 MATCH_MP_TAC zlz_wedge_skolem;
3998 MATCH_MP_TAC zlz_wedge_boundary;
3999 GEXISTL_TAC [`a`;`b`];
4000 BY(ASM_REWRITE_TAC[]);
4001 MATCH_MP_TAC zlz_azim;
4002 GEXISTL_TAC [`a`;`b`;`V`];
4003 BY(ASM_REWRITE_TAC[])