1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Local Fan *)
5 (* Author: Nguyen Quang Truong *)
6 (* Date: 2013 - 5 - 31 *)
7 (* ========================================================================== *)
10 (* ================================================================ *)
15 module Lunar_deform = struct
20 open Wrgcvdr_cizmrrh;;
30 (* ================================== *)
36 let asms_search0 sths =
37 let rec immediatesublist l1 l2 =
41 | (h1::t1,h2::t2) -> h1 = h2 & immediatesublist t1 t2 in
42 let rec sublist l1 l2 =
46 | (h1::t1,h2::t2) -> immediatesublist l1 l2 or sublist l1 t2 in
47 let exists_subterm_satisfying p (n,th) = can (find_term p) (concl th)
48 and name_contains s (n,th) = sublist (explode s) (explode n) in
49 let rec filterpred tm =
51 Comb(Var("<omit this pattern>",_),t) -> not o filterpred t
52 | Comb(Var("<match theorem name>",_),Var(pat,_)) -> name_contains pat
53 | Comb(Var("<match aconv>",_),pat) -> exists_subterm_satisfying (aconv pat)
54 | pat -> exists_subterm_satisfying (can (term_match [] pat)) in
56 let triv,nontriv = partition is_var pats in
59 ("Ignoring plain variables in search: "^
60 end_itlist (fun s t -> s^", "^t) (map (fst o dest_var) triv))
62 (if nontriv = [] & triv <> [] then []
63 else itlist (filter o filterpred) pats sths);;
66 let gstk = !current_goalstack in
69 | (meta,gl::_,just)::_
70 -> let (sths,_) = gl in
71 map snd (asms_search0 sths tms)
72 | _ -> failwith "asm_searchs: Invalid goal state";;
74 let ASMS_SEARCH_TCL (tms:(term)list) (thstac:(thm)list->tactic) : tactic =
77 let ths1 = map snd (asms_search0 sths tms) in
80 let ASM_SEARCH_TCL (tms:(term)list) (thstac:thm->tactic) : tactic =
81 let foo ths = match ths with
82 [] -> failwith "ASM_SEARCH_TCL: No matching asms found"
83 | _ -> thstac (hd ths) in
84 ASMS_SEARCH_TCL tms foo;;
86 let ASM_SEARCH_TC = asms_search;;
89 let ATTACH thm = MATCH_MP (MESON[]` ! a b. ( a ==> b ) ==> ( a <=> a /\ b )`) thm;;
91 let NHANH tm = ONCE_REWRITE_TAC[ ATTACH (SPEC_ALL ( tm ))];;
93 let PHA = REWRITE_TAC[ MESON[] ` (a/\b)/\c <=> a/\ b /\ c `; MESON[]`
94 a ==> b ==> c <=> a /\ b ==> c `];;
96 let DOWN_TAC = REPEAT (FIRST_X_ASSUM MP_TAC) THEN REWRITE_TAC[IMP_IMP] THEN PHA;;
99 let DOWN = FIRST_X_ASSUM MP_TAC;;
101 let DOWNS n = REPLICATE_TAC n DOWN THEN PHA;;
103 let REMOVE_TAC = FIRST_X_ASSUM MP_TAC THEN MATCH_MP_TAC (TAUT` a ==> b ==> a`);;
107 let types_thm th = let cl = concl th in
108 List.map dest_var (frees cl );;
111 let (tms,tm) = top_goal () in
112 let vss = map frees (tm::tms) in
113 let vs = setify (flat vss) in
120 let PAT_REWRITE_TAC tm thms =
121 (CONV_TAC (PAT_CONV tm (REWRITE_CONV thms )));;
124 let th1 = REWRITE_RULE[MESON[]` a /\ b ==> c <=>
125 a ==> b ==> c `] th in
126 let th2 = SPEC_ALL th1 in UNDISCH_ALL th2;;
128 (* change a th having form |- A ==> t to the form A |- t
129 to get ready to some other commands
137 let ASSUME_TAC2 = ASSUME_TAC o FOR_ASM;;
140 let PAT_ONCE_REWRITE_TAC tm thms =
141 (CONV_TAC (PAT_CONV tm (ONCE_REWRITE_CONV thms )));;
143 let ASM_PAT_RW_TAC tm thms = EVERY_ASSUM (fun th ->
144 (CONV_TAC (PAT_CONV tm (ONCE_REWRITE_CONV
145 ( th ::[ thms ] )))));;
147 let PAT_TH_TAC tm th =
148 (CONV_TAC (PAT_CONV tm (REWRITE_CONV[th] )));;
151 let IMP_TO_EQ_RULE th = MATCH_MP (TAUT` (a ==> b ) ==>
152 ( a <=> a /\ b )`) (SPEC_ALL th);;
154 let NHANH_PAT tm th = PAT_ONCE_REWRITE_TAC tm
155 [ IMP_TO_EQ_RULE th ];;
158 let MAKE_FIRST_TAC tm = UNDISCH_TAC tm THEN DISCH_TAC;;
161 (* ---------- BG TEST ------------- *)
165 let rec els L = match L with
167 | (x::l) -> e x; els l;;
169 let rec bls L = match L with
171 | (x::l) -> b (); bls l;;
174 (* ============================================= *)
178 let CONS_IMP_CONTINUOUS_ATREAL = prove_by_refinement(` (! t. t IN real_interval (a,b) ==> f t = (u:real^N) )
179 ==> (! t. t IN real_interval (a,b) ==> f continuous atreal t ) `,
180 [REWRITE_TAC[continuous_atreal; real_interval; IN_ELIM_THM];
182 EXISTS_TAC` min (b - t ) ( t - a ) ` ;
184 REWRITE_TAC[REAL_LT_MIN];
187 REWRITE_TAC[REAL_LT_MIN];
189 ASSUME_TAC2 (REAL_ARITH` a < t /\ t < b /\ abs (x' - t) < b - t /\ abs (x' - t) < t - a ==> x' < b /\ a < x' `);
190 SUBGOAL_THEN ` f (x':real) = (u:real^N) ` MP_TAC;
191 FIRST_X_ASSUM MATCH_MP_TAC;
193 ASM_SIMP_TAC[DIST_REFL]]);;
196 let AFF_GT_SUBSET_AFFINE_HULL21 = ISPECL [` {u, v:real^N} `;` {w:real^N } `] AFF_GT_SUBSET_AFFINE_HULL;;
200 let DISJTINCT_PROPERTY = prove_by_refinement (
202 (f : real^N -> real -> real^N) u continuous atreal (&0) /\
206 (!u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = u')
209 --e < t /\ t < e /\ u' IN V /\ ~(u' = u) ==> ~(f u t = f u' t)))`, [
211 SUBGOAL_THEN`!u'. u' IN V /\ ~(u = u') ==> (!t. t IN real_interval (a,b) ==>
212 (f: real^N -> real -> real^N) u' continuous atreal t )` ASSUME_TAC;
213 GEN_TAC THEN STRIP_TAC;
214 MATCH_MP_TAC (GEN`u: real^N ` CONS_IMP_CONTINUOUS_ATREAL);
215 EXISTS_TAC` u': real^N `;
217 FIRST_X_ASSUM MATCH_MP_TAC;
219 MP_TAC (ISPECL [` &0 `;` u:real^N `;` f: real^N -> real -> real^N `;
220 ` V:real^N -> bool `] (GEN_ALL Local_lemmas1.CONTINUOUS_FUN_DISTINCT_FINITE_SET));
226 SUBGOAL_THEN` &0 IN real_interval (a,b) ` MP_TAC;
227 ASM_REWRITE_TAC[real_interval; IN_ELIM_THM];
230 REWRITE_TAC[IN_INSERT];
233 SUBGOAL_THEN` &0 IN real_interval (a,b) ` MP_TAC;
234 ASM_REWRITE_TAC[real_interval; IN_ELIM_THM];
237 REWRITE_TAC[REAL_SUB_RZERO; GSYM REAL_BOUNDS_LT];
244 let EDGE_FORM_IN_LOCAL_FAN = prove_by_refinement(
245 ` local_fan (V,E,FF) /\ x IN E ==> ? u v. ~( u = v ) /\ {u, v} = x `,
246 [REWRITE_TAC[local_fan; FAN; graph; IN];
247 LET_TAC; STRIP_TAC; FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` x:real^3 -> bool `));
248 DOWN; REWRITE_TAC[Local_lemmas1.HAS_SIZE_2_EXISTS2]; MESON_TAC[]]);;
254 let EDGE_IN_LOCAL_FAN_DET_RHO_NODE = prove_by_refinement
255 (` local_fan (V,E,FF) /\ x IN E ==> (?v. v IN V /\ {v, rho_node1 FF v} = x) `,
256 [NHANH EDGE_FORM_IN_LOCAL_FAN;
258 UNDISCH_TAC` (x:real^3 -> bool) IN E `;
259 UNDISCH_TAC` local_fan (V,E,FF) `;
262 NHANH Local_lemmas.LOFA_IN_E_IMP_IN_FF;
265 UNDISCH_TAC` local_fan (V,E,FF) `;
267 NHANH Local_lemmas.DETER_RHO_NODE;
269 EXISTS_TAC `u: real^3 `;
271 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V; Local_lemmas.DETER_RHO_NODE; INSERT_COMM];
272 ASM_MESON_TAC[Local_lemmas.LOCAL_FAN_IMP_IN_V; Local_lemmas.DETER_RHO_NODE; INSERT_COMM]]);;
278 let TOW_POINTS_IN_IMP_AFF_GT_SUBSET = prove_by_refinement
279 (` DISJOINT {x, u} {v:real^N } /\
280 a IN aff_gt {x,u} {v} /\
281 b IN aff_gt {x, u} {v} /\
283 ==> aff_gt {x} {a,b} SUBSET aff_gt {x,u} {v} `,
287 UNDISCH_TAC` a IN aff_gt {x, u} {v:real^N }`;
288 UNDISCH_TAC` b IN aff_gt {x, u} {v:real^N }`;
289 ASM_REWRITE_TAC[IN_ELIM_THM; SUBSET];
296 REWRITE_TAC[VECTOR_ARITH` t1'' % x +
298 t2'' % (t1' % x + t2' % u + t3' % v) +
299 t3'' % (t1 % x + t2 % u + t3 % v) =
300 (t1'' + t2'' * t1' + t3'' * t1 ) % x + (t2'' * t2' + t3'' * t2) % u +
301 (t2'' * t3' + t3'' * t3 ) % v `];
303 EXISTS_TAC` (t1'' + t2'' * t1' + t3'' * t1:real) `;
304 EXISTS_TAC` t2'' * t2' + t3'' * t2:real `;
305 EXISTS_TAC` t2'' * t3' + t3'' * t3 `;
307 MATCH_MP_TAC Real_ext.REAL_PROP_POS_ADD2;
308 ASM_MESON_TAC[REAL_LT_MUL];
311 UNDISCH_TAC` t1' + t2' + t3' = &1 `;
312 UNDISCH_TAC` t1 + t2 + t3 = &1 `;
313 UNDISCH_TAC` t1'' + t2'' + t3'' = &1 `;
315 CONV_TAC REAL_RING]);;
320 let REAL_LT_MUL12 = prove(` &0 < b /\ a < &0 ==> a * b < &0 `,
321 REWRITE_TAC[REAL_ARITH` a * b < &0 <=> &0 < (-- a) * (b ) `] THEN
323 MATCH_MP_TAC REAL_LT_MUL THEN
328 let COLL_IN_AFF_GT_INTER_EMPTY = prove_by_refinement
329 (` ~ collinear {a,b,x: real^N} /\ u IN aff_gt {a,b} {x} ==>
330 aff_gt {a, b} {x} INTER aff_lt {a} {u} = {} `,
331 [NHANH Local_lemmas.COLL_IN_AFF_GT_TOO;
335 NHANH (SET_RULE` DISJOINT {a, b} {u} ==> DISJOINT {a} {u} `);
338 UNDISCH_TAC` DISJOINT {a, b} {x: real^N} `;
341 UNDISCH_TAC` u IN aff_gt {a, b} {x: real^N} `;
342 ASM_REWRITE_TAC[IN_ELIM_THM];
344 REWRITE_TAC[SET_RULE` A INTER B = {} <=> (! x. x IN B ==> ~( x IN A)) `];
345 REWRITE_TAC[IN_ELIM_THM];
346 GEN_TAC THEN STRIP_TAC;
349 REWRITE_TAC[Local_lemmas.VECTOR_ADD_LDISTRIB1];
351 SUBGOAL_THEN` (t1' + t2' * t1 ) + (t2' * t2 ) + (t2' * t3) = &1 ` ASSUME_TAC;
352 ASM_REWRITE_TAC[REAL_RING` (t1' + t2' * t1) + t2' * t2 + t2' * t3 = t1' + t2' * (t1 + t2 + t3 ) `; REAL_ARITH` a * &1 = a `];
353 ABBREV_TAC` vv: real^N = t1'' % a + t2'' % b + t3' % x ` ;
354 SUBGOAL_THEN` (vv: real^N) IN affine hull {a, b, x} ` ASSUME_TAC;
355 ASM_REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM];
357 UNDISCH_TAC` ~collinear {a, b, x:real^N} `;
359 NHANH Collect_geom.lemma11;
361 FIRST_ASSUM (MP_TAC o (SPECL [` t1'': real `;` t2'': real `;` t3': real `]));
364 FIRST_ASSUM (MP_TAC o (SPECL [` (t1': real) + t2' * t1`;`( t2': real ) * t2 `;` (t2': real) * t3 `]));
367 UNDISCH_TAC` t1' % a + (t2' * t1) % a + (t2' * t2) % b + (t2' * t3) % x = (vv: real^N) `;
369 DISCH_THEN (SUBST1_TAC o SYM);
370 CONV_TAC VECTOR_ARITH;
375 ASSUME_TAC2 (SPECL [` t2': real `;` t3: real `] (GEN_ALL REAL_LT_MUL12));
377 UNDISCH_TAC` &0 < t3' `;
385 let HKIRPEP_ALT = prove(` convex_local_fan (V,E,FF) /\ lunar (v,w) V E
386 ==> (!u. u IN V DIFF {v, w} ==> interior_angle1 (vec 0) FF u = pi) /\
387 &0 < interior_angle1 (vec 0) FF v /\
388 interior_angle1 (vec 0) FF v <= pi /\
389 interior_angle1 (vec 0) FF v = interior_angle1 (vec 0) FF w /\
390 (?i j. i + j = CARD V /\ i < CARD V /\
393 w = ITER i (rho_node1 FF) v /\
394 {ITER l (rho_node1 FF) v | 0 < l /\ l < i} =
395 aff_gt {vec 0, v} {rho_node1 FF v} INTER V /\
399 v = ITER j (rho_node1 FF) w /\
400 {ITER l (rho_node1 FF) w | 0 < l /\ l < j} =
401 aff_gt {vec 0, v} {ivs_rho_node1 FF v} INTER V) `,
402 NHANH Local_lemmas.HKIRPEP THEN
404 UNDISCH_TAC` v = ITER j (rho_node1 FF) w ` THEN
405 UNDISCH_TAC` w = ITER i (rho_node1 FF) v ` THEN
406 DISCH_THEN (ASSUME_TAC o SYM) THEN
407 DISCH_THEN (ASSUME_TAC o SYM) THEN
408 ASM_REWRITE_TAC[] THEN
409 EXISTS_TAC` i: num ` THEN
410 EXISTS_TAC` j:num ` THEN
411 ASM_REWRITE_TAC[] THEN
412 MATCH_MP_TAC (GEN_ALL Local_lemmas1.CARD_V_TWO_HAFL_CIRCLE) THEN
413 EXISTS_TAC` E: (real^3 -> bool) -> bool ` THEN
414 EXISTS_TAC` FF: real^3 # real^3 -> bool ` THEN
415 EXISTS_TAC` w:real^3 ` THEN
416 EXISTS_TAC` v: real^3 ` THEN
417 ASM_REWRITE_TAC[] THEN
418 UNDISCH_TAC` convex_local_fan (V,E,FF)` THEN
419 UNDISCH_TAC ` lunar (v,w:real^3) V E ` THEN
420 SIMP_TAC[convex_local_fan; lunar; INSERT_SUBSET]);;
427 let LUNAR_IMP_IN_TWO_HAFLS_PLANE = prove_by_refinement (` convex_local_fan (V,E,FF) /\ lunar (v,w) V E ==>
428 (! u. u IN V /\ ~( u = v ) /\ ~( u = w) ==> u IN aff_gt {vec 0, v} {rho_node1 FF v} \/ u IN aff_gt {vec 0, v} {ivs_rho_node1 FF v} ) `,
431 ASSUME_TAC2 Local_lemmas.CVX_LO_IMP_LO;
432 SUBGOAL_THEN` lunar (v,w:real^3) V E ` MP_TAC;
433 FIRST_X_ASSUM ACCEPT_TAC;
434 REWRITE_TAC[lunar; circular; INSERT_SUBSET];
436 ASSUME_TAC2 (SPEC_ALL Localization.LOFA_IMP_LT_CARD_SET_V_ALT);
437 GEN_TAC THEN STRIP_TAC;
438 UNDISCH_TAC` (u:real^3) IN V `;
440 REWRITE_TAC[IN_ELIM_THM];
442 ASM_CASES_TAC` n = 0 `;
443 FIRST_X_ASSUM (SUBST_ALL_TAC);
445 UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
446 UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
447 DISCH_THEN (ASSUME_TAC o SYM);
448 DISCH_THEN (ASSUME_TAC o SYM);
449 ASM_REWRITE_TAC[ITER];
450 ASM_CASES_TAC` n < (i:num) `;
453 UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
454 UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
455 DISCH_THEN (ASSUME_TAC o SYM);
456 DISCH_THEN (ASSUME_TAC o SYM);
459 SUBGOAL_THEN` u IN {ITER l (rho_node1 FF) v | 0 < l /\ l < i} ` MP_TAC;
460 REWRITE_TAC[IN_ELIM_THM];
461 EXISTS_TAC` n: num `;
463 UNDISCH_TAC` ~( n = 0) `;
465 ASM_SIMP_TAC[IN_INTER];
467 ASM_CASES_TAC` n = (i:num) `;
468 UNDISCH_TAC` u = ITER n (rho_node1 FF) v `;
469 UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
470 UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
471 DISCH_THEN (ASSUME_TAC o SYM);
472 DISCH_THEN (ASSUME_TAC o SYM);
476 SUBGOAL_THEN`u IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} ` MP_TAC;
477 REWRITE_TAC[IN_ELIM_THM];
478 EXISTS_TAC` n - (i:num ) `;
480 UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
481 UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
482 DISCH_THEN (ASSUME_TAC o SYM);
483 DISCH_THEN (ASSUME_TAC o SYM);
486 REWRITE_TAC[ITER_ADD];
487 ASSUME_TAC2 (ARITH_RULE` ~( n < i) ==> n - i + i = (n:num ) `);
489 ASSUME_TAC2 (ARITH_RULE` ~(n < i) ==> (n - i < j <=> (n:num) < i + j ) `);
490 ASM_REWRITE_TAC[ARITH_RULE` 0 < n - i <=> ~( n < i ) /\ ~( n = (i:num)) `];
492 UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
493 UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
494 DISCH_THEN (ASSUME_TAC o SYM);
495 DISCH_THEN (ASSUME_TAC o SYM);
497 ASM_SIMP_TAC[IN_INTER]]);;
503 let IN_CONV0_IMP_AFF_EQ1 = prove(` a IN conv0 {x, y} ==> aff {a, x} = aff {a, y} `,
504 NHANH Local_lemmas.IN_CONV0_IMP_AFF_EQ THEN
505 ONCE_REWRITE_TAC[INSERT_COMM] THEN
506 NHANH Local_lemmas.IN_CONV0_IMP_AFF_EQ THEN
507 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
508 SIMP_TAC[INSERT_COMM]);;
513 let AFF_LT_SUBSET_AFF11 = prove_by_refinement (
514 ` DISJOINT {a} {b} ==> aff_lt {a} {b} SUBSET aff {a,b:real^N} `,
516 SIMP_TAC[Collect_geom.AFF_2POINTS_INTERPRET; SUBSET; IN_ELIM_THM];
520 EXISTS_TAC` t1: real `;
521 EXISTS_TAC` t2: real `;
522 ASM_REWRITE_TAC[]]);;
527 let IN_AFF_LT_STILL_NOT_COLLINEAR = prove_by_refinement
528 (` ~ collinear {x: real^N,y,a} /\ b IN aff_lt {x, y} {a} ==>
529 ~ collinear {x,y,b} `,
531 UNDISCH_TAC` b IN aff_lt {x, y} {a: real^N} `;
533 UNDISCH_TAC ` ~collinear {x, y, a: real^N} `;
536 SIMP_TAC[IN_ELIM_THM];
538 UNDISCH_TAC` ~collinear {x, y, a:real^N} `;
540 UNDISCH_TAC` collinear {x,y,b:real^N} `;
541 REWRITE_TAC[Local_lemmas.collinear_fan22; Collect_geom.AFF_2POINTS_INTERPRET; IN_ELIM_THM];
547 VECTOR_ARITH` t1 % x + t2 % y + t3 % a = ta % x + tb % y <=> t3 % a = (ta - t1) % x + (tb - t2) % y `];
548 NHANH_PAT`\x. x ==> y ` (MESON[]` a = b ==> ( &1 / t3) % a = (&1 / t3) % b `);
549 REWRITE_TAC[Local_lemmas.VECTOR_ADD_LDISTRIB1];
550 ASSUME_TAC2 (REAL_FIELD` t3 < &0 ==> &1 / t3 * t3 = &1 `);
551 ASM_REWRITE_TAC[VECTOR_MUL_LID];
554 EXISTS_TAC` (&1 / t3 * (ta - t1)) `;
555 EXISTS_TAC` (&1 / t3 * (tb - t2)) `;
556 ASM_REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; REAL_ARITH` a - x + b - y = (a + b ) - ( x + y )`];
557 UNDISCH_TAC`t1 + t2 + t3 = &1 `;
558 ASM_SIMP_TAC[REAL_ARITH` a + b + c = &1 <=> &1 - ( a + b ) = c `];
560 ASM_REWRITE_TAC[]]);;
566 let AZIM_PI_LEMMA = prove_by_refinement
567 (` ~(aff_gt {u} s INTER aff_lt {u} {a} = {} ) /\
568 aff_gt {u} s SUBSET aff_gt {u, v} {y} /\
569 a IN aff_gt {u, v} {x} /\
570 ~ collinear {u, v, x} /\
571 ~ collinear {u, v, y}
572 ==> azim u v x y = pi `,
574 ISPECL [`{u: real^3} `;` {u, v:real^3} `; `{a: real^3 }`] AFF_LT_MONO_LEFT);
578 SUBGOAL_THEN` aff_gt {u,v} {x} = aff_gt {u,v} {a:real^3} ` MP_TAC;
579 MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
581 DISCH_THEN (ASSUME_TAC o SYM);
583 SET_RULE` ~(aff_gt {u: real^3} s INTER aff_lt {u} {a} = {}) /\
584 aff_lt {u} {a} SUBSET aff_lt {u, v} {a} /\
585 aff_gt {u} s SUBSET aff_gt {u, v} {y}
586 ==> ~ ( aff_gt {u, v} {y} INTER aff_lt {u, v} {a} = {} ) `);
588 REWRITE_TAC[SET_RULE` ~( A INTER B = {} ) <=> ? x. x IN A /\ x IN B `];
590 UNDISCH_TAC` x' IN aff_gt {u, v} {y:real^3} `;
591 UNDISCH_TAC` ~ collinear {u, v, y:real^3} `;
593 NHANH Local_lemmas.COLL_IN_AFF_GT_TOO;
595 SUBGOAL_THEN` ~ collinear {u, v, a: real^3} ` ASSUME_TAC;
596 MATCH_MP_TAC (GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO);
597 EXISTS_TAC` x: real ^3 `;
600 UNDISCH_TAC` ~collinear {u, v, x' : real^3} `;
601 UNDISCH_TAC` ~collinear {u, v, a: real^3} `;
603 NHANH AZIM_EQ_PI_ALT;
607 SUBGOAL_THEN` azim u v a x' = azim u v a y ` MP_TAC;
608 MATCH_MP_TAC AZIM_EQ_IMP;
610 FIRST_X_ASSUM (ASSUME_TAC o SYM);
613 UNDISCH_TAC` x' IN aff_lt {u, v} {a:real^3} `;
615 SUBGOAL_THEN` azim u v a y = azim u v x y ` MP_TAC;
616 ONCE_REWRITE_TAC[ Rogers.AZIM_EQ_SYM];
617 MATCH_MP_TAC (* Polar_fan. *) AZIM_EQ_IMP;
624 (* ================================================== *)
635 let SUB_LUNAR_DEFORM_LEMMA = prove_by_refinement(` FINITE V /\ convex_local_fan (V,E,FF) /\ lunar (v,w) V E /\
636 (! x. x IN E ==> x SUBSET V) /\
637 f (u:real^3) (&0 ) = u /\
638 f u continuous atreal (&0) /\
639 interior_angle1 (vec 0) FF v < pi /\
644 (!u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = u') /\
645 (!t. t IN real_interval (a,b) ==> f u t IN affine hull {vec 0, v, w, u})
648 (!t. --e < t /\ t < e
650 lunar (v,w) (IMAGE (\v. f v t) V)
651 (IMAGE (IMAGE (\v. f v t)) E)))`,
654 ASSUME_TAC2 Local_lemmas.HKIRPEP;
656 REWRITE_TAC[lunar; circular];
658 SUBGOAL_THEN` ! t. t IN real_interval (a,b) ==> {v, w} SUBSET IMAGE (\v. (f:real^3->real->real^3) v t) V ` ASSUME_TAC;
660 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_IMAGE];
662 EXISTS_TAC` v:real^3` ;
663 SUBGOAL_THEN` (v:real^3) IN V ` MP_TAC;
664 MATCH_MP_TAC (SET_RULE` {v, w:real^3} SUBSET V ==> v IN V`);
665 FIRST_X_ASSUM ACCEPT_TAC;
667 FIRST_X_ASSUM (ASSUME_TAC o (SPEC ` &0 `));
668 FIRST_X_ASSUM (ASSUME_TAC o (ISPECL[ ` v:real^3`; ` t:real `]));
670 ONCE_REWRITE_TAC[EQ_SYM_EQ];
671 FIRST_X_ASSUM MATCH_MP_TAC;
673 EXISTS_TAC` w:real^3 `;
677 SUBGOAL_THEN` (w:real^3) IN V ` ASSUME_TAC;
678 MATCH_MP_TAC (SET_RULE` {v, w} SUBSET V ==> w IN V ` );
679 FIRST_X_ASSUM ACCEPT_TAC;
680 UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
681 DISCH_THEN (ASSUME_TAC o GSYM);
686 FIRST_X_ASSUM (ASSUME_TAC o (SPEC ` &0 `)) THEN
687 FIRST_X_ASSUM (ASSUME_TAC o (SPECL[ ` w:real^3 `; ` t:real `]));
691 ONCE_REWRITE_TAC[EQ_SYM_EQ];
692 FIRST_X_ASSUM MATCH_MP_TAC THEN
695 ABBREV_TAC` CONCL = ?e. &0 < e /\
696 (!t. --e < t /\ t < e
698 {v, w} IN IMAGE (IMAGE (\v. (f:real^3 -> real -> real^3) v t)) E /\
699 u IN IMAGE (\v. f v t) V /\
700 ~(aff_gt {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {})) /\
701 {v, w} SUBSET IMAGE (\v. f v t) V /\
703 collinear {vec 0, v, w}) `;
706 MP_TAC (ISPEC`V: real^3 -> bool ` (GEN`V: real^N -> bool ` DISJTINCT_PROPERTY));
712 SUBGOAL_THEN` t IN real_interval (a,b) /\ --e < t /\ t < e
714 {v, w} IN IMAGE (IMAGE (\v. (f:real^3 -> real -> real^3) v t)) E /\
715 u' IN IMAGE (\v. f v t) V /\
716 ~( f u t IN {u' ,v, w} )
717 ==> (aff_gt {vec 0} {v, w} INTER aff_lt {vec 0} {u'} =
719 REWRITE_TAC[IN_IMAGE];
722 SUBGOAL_THEN` x SUBSET (V:real^3 -> bool ) ` ASSUME_TAC;
723 FIRST_ASSUM MATCH_MP_TAC;
724 FIRST_ASSUM ACCEPT_TAC;
725 ASM_CASES_TAC` (u:real^3) IN x `;
726 SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN {v', w'} ` ASSUME_TAC;
727 UNDISCH_TAC` {v': real^3, w'} = IMAGE (\v. (f:real^3 -> real -> real^3) v t) x `;
731 EXISTS_TAC` u:real^3 `;
734 REPLICATE_TAC 3 DOWN;
737 SUBGOAL_THEN` t IN real_interval (a, b) ==> IMAGE (\v. (f:real^3 -> real -> real^3) v t ) x = x ` MP_TAC;
739 MATCH_MP_TAC Counting_spheres.pad2d3d_dropout_lemma;
740 EXISTS_TAC` \x. (x:real^3) IN V /\ ~( x = u ) ` ;
743 REWRITE_TAC[BETA_THM];
744 DOWN THEN DOWN THEN DOWN;
748 REWRITE_TAC[BETA_THM];
750 UNDISCH_TAC` !u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> (f: real^3 -> real -> real^3) u' t = u' `;
751 DISCH_THEN MATCH_MP_TAC;
753 DISCH_THEN ASSUME_TAC2;
754 FIRST_X_ASSUM SUBST_ALL_TAC;
756 ASM_CASES_TAC` x' = (u:real^3) `;
757 FIRST_X_ASSUM SUBST_ALL_TAC;
758 UNDISCH_TAC` ~((f:real^3 -> real -> real^3 ) u t IN {u', v', w'}) ` ;
759 ASM_REWRITE_TAC[IN_INSERT];
760 SUBGOAL_THEN` (f: real^3 -> real -> real^3) x' t = x' ` MP_TAC;
761 UNDISCH_TAC` !u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> (f: real^3 -> real -> real^3 ) u' t = u' ` ;
762 DISCH_THEN MATCH_MP_TAC;
764 DISCH_THEN SUBST_ALL_TAC;
765 UNDISCH_TAC` ~(?v w u.
768 ~(aff_gt {vec 0} {v, w: real^3} INTER aff_lt {vec 0} {u} = {})) `;
770 UNDISCH_TAC` x': real^3 IN V `;
771 UNDISCH_TAC` (x: real^3 -> bool) IN E `;
776 ASSUME_TAC2 Local_lemmas.CVX_LO_IMP_LO;
777 MP_TAC (SPECL [` i:num `;` j:num `] (GENL[` n:num `;` n': num `] Local_lemmas1.CARD_V_TWO_HAFL_CIRCLE));
779 UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
780 DISCH_THEN (ASSUME_TAC o SYM);
781 UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
782 DISCH_THEN (ASSUME_TAC o SYM);
783 ASM_REWRITE_TAC[SET_RULE` x IN A /\ y IN A <=> {x,y} SUBSET A `];
785 ASSUME_TAC2 (SET_RULE` {v, w:real^3} SUBSET V ==> v IN V `);
786 ASSUME_TAC2 Localization.LOFA_IMP_LT_CARD_SET_V_ALT;
787 UNDISCH_TAC` (u:real^3) IN V `;
789 REWRITE_TAC[IN_ELIM_THM];
791 UNDISCH_TAC` v = ITER j (rho_node1 FF) w ` ;
793 DISCH_THEN (ASSUME_TAC o SYM);
794 DISCH_THEN (ASSUME_TAC o SYM);
795 UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
796 DISCH_THEN (ASSUME_TAC o SYM);
797 MP_TAC Local_lemmas.AFF_IVS_RHO_NODE_EQQ;
799 ASM_REWRITE_TAC[lunar; circular];
800 DISCH_THEN (ASSUME_TAC o SYM);
801 FIRST_X_ASSUM SUBST_ALL_TAC;
802 SUBGOAL_THEN` u IN aff_gt {vec 0, v} {rho_node1 FF v} \/ u IN aff_gt {vec 0, w} {rho_node1 FF w} ` MP_TAC;
804 ASM_CASES_TAC` (n:num) < i ` ;
806 ASM_CASES_TAC` n = 0 `;
807 FIRST_X_ASSUM SUBST_ALL_TAC;
808 REPLICATE_TAC 4 DOWN THEN PHA;
809 ASM_REWRITE_TAC[ITER];
810 SUBGOAL_THEN` u IN {ITER l (rho_node1 FF) v | 0 < l /\ l < i} ` ASSUME_TAC;
811 REWRITE_TAC[IN_ELIM_THM];
812 EXISTS_TAC` n: num `;
817 ASM_SIMP_TAC[IN_INTER];
818 ASM_CASES_TAC` (n:num) = i ` ;
819 FIRST_X_ASSUM SUBST_ALL_TAC;
820 REPLICATE_TAC 2 DOWN THEN PHA;
823 ASSUME_TAC2 (ARITH_RULE` ~( n:num < i) ==> i + ( n - i ) = n`);
824 SUBGOAL_THEN` u IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j}` MP_TAC;
825 REWRITE_TAC[IN_ELIM_THM];
826 EXISTS_TAC` (n: num) - i `;
828 ASM_REWRITE_TAC[ITER_ADD; ADD_SYM];
829 REPLICATE_TAC 3 DOWN THEN PHA;
830 SIMP_TAC[ (ARITH_RULE` ~((n:num) < i) ==> ( n - i < j <=> n < i + j ) `)];
833 ASM_SIMP_TAC[IN_INTER];
835 ASSUME_TAC2 (SET_RULE` {v, w:real^3} SUBSET V ==> w IN V `);
836 MP_TAC (SPEC` w:real^3 ` Local_lemmas.LOFA_IMP_LT_CARD_SET_V);
838 ASM_SIMP_TAC[SET_RULE` {a,b} SUBSET V ==> b IN V `];
840 SUBGOAL_THEN` u IN {ITER n (rho_node1 FF) v | n < CARD (V:real^3 -> bool)} ` ASSUME_TAC;
842 REWRITE_TAC[IN_ELIM_THM];
848 REWRITE_TAC[IN_ELIM_THM];
852 DISCH_THEN (ASSUME_TAC o SYM);
855 REWRITE_TAC[TAUT` a /\ b /\ c <=> (a /\ b) /\ c `];
856 SPEC_TAC (`n':num `,` n': num ` );
857 SPEC_TAC (`n:num `,` n: num ` );
859 SPEC_TAC (`v:real^3 `, ` v:real^3 `);
860 SPEC_TAC (`i: num `,` i:num ` );
861 SPEC_TAC (`w:real^3 `, ` w:real^3 `);
862 SPEC_TAC (`j: num `,` j:num ` );
868 MESON[]` (! j w i v n n'. P j w i v n n' ==> P i v j w n' n) /\ (! j w i v n n'. P j w i v n n' /\ u IN Q v ==> concl ) ==>
869 (! j w i v n n'. P j w i v n n'/\ (u IN Q v \/ u IN Q w ) ==> concl )`);
872 SIMP_TAC[INSERT_COMM; ADD_SYM];
876 UNDISCH_TAC` interior_angle1 (vec 0) FF v = interior_angle1 (vec 0) FF w ` ;
877 DISCH_THEN (SUBST1_TAC o SYM);
879 UNDISCH_TAC`(?e. &0 < e /\
880 (!t. --e < t /\ t < e
882 ({v, w} IN IMAGE (IMAGE (\v. f v t)) E /\
883 u IN IMAGE (\v. f v t) V) /\
884 ~(aff_gt {vec 0} {v, w} INTER aff_lt {vec 0} {u} =
886 {v, w} SUBSET IMAGE (\v. (f:real^3 -> real -> real^3) v t) V) /\
888 collinear {v, w, vec 0})) <=>
898 (* ====================================
900 prove_by_refinement (`FINITE V /\
901 convex_local_fan (V,E,FF) /\
905 ~(aff_gt {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {})) /\
908 collinear {vec 0, v, w} /\
909 (!x. x IN E ==> x SUBSET V) /\
911 f u continuous atreal (&0) /\
912 interior_angle1 (vec 0) FF v < pi /\
917 (!u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = u') /\
918 (!t. t IN real_interval (a,b) ==> f u t IN affine hull {vec 0, v, w, u}) /\
919 (!u. u IN V DIFF {v, w} ==> interior_angle1 (vec 0) FF u = pi) /\
920 &0 < interior_angle1 (vec 0) FF v /\
921 interior_angle1 (vec 0) FF v <= pi /\
922 interior_angle1 (vec 0) FF v = interior_angle1 (vec 0) FF w /\
926 {ITER l (rho_node1 FF) v | 0 < l /\ l < i} =
927 aff_gt {vec 0, v} {rho_node1 FF v} INTER V /\
931 {ITER l (rho_node1 FF) w | 0 < l /\ l < j} =
932 aff_gt {vec 0, w} {rho_node1 FF w} INTER V /\
933 (!t. t IN real_interval (a,b) ==> {v, w} SUBSET IMAGE (\v. f v t) V) /\
935 (!t. --e < t /\ t < e
937 {v, w} IN IMAGE (IMAGE (\v. f v t)) E /\
938 u IN IMAGE (\v. f v t) V /\
939 ~(aff_gt {vec 0} {v, w} INTER aff_lt {vec 0} {u} = {})) /\
940 {v, w} SUBSET IMAGE (\v. f v t) V /\
942 collinear {vec 0, v, w})) <=>
945 (!t u'. --e < t /\ t < e /\ u' IN V /\ ~(u' = u) ==> ~(f u t = f u' t)) /\
946 (t IN real_interval (a,b) /\ --e < t /\ t < e
948 {v, w} IN IMAGE (IMAGE (\v. f v t)) E /\
949 u' IN IMAGE (\v. f v t) V /\
950 ~(f u t IN {u', v, w})
951 ==> aff_gt {vec 0} {v, w} INTER aff_lt {vec 0} {u'} = {})) /\
952 local_fan (V,E,FF) /\
955 {ITER n (rho_node1 FF) v | n < CARD V} = V /\
957 ITER n (rho_node1 FF) v = u /\
958 ITER j (rho_node1 FF) w = v /\
959 ITER i (rho_node1 FF) v = w /\
961 {ITER n (rho_node1 FF) w | n < CARD V} = V /\
963 ITER n' (rho_node1 FF) w = u /\
964 u IN aff_gt {vec 0, v} {rho_node1 FF v}
970 ================================= *)
973 SUBGOAL_THEN` aff_gt {vec 0, v} {rho_node1 FF v} = aff_gt {vec 0, v} {u} ` MP_TAC;
974 MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
976 MATCH_MP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2 ;
979 ABBREV_TAC` u1 = ( (u dot v ) / ( v dot v )) % (v:real^3)`;
980 ABBREV_TAC` uh = u - (u1:real^3) `;
981 SUBGOAL_THEN` uh dot (v:real^3) = &0 ` ASSUME_TAC;
984 REWRITE_TAC[DOT_LSUB; DOT_LMUL];
985 ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
986 FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 ` ));
988 REWRITE_TAC[GSYM DOT_EQ_0];
990 SUBGOAL_THEN` (f:real^3 -> real -> real^3) u continuous atreal (&0) ` MP_TAC;
992 REWRITE_TAC[continuous_atreal];
993 DISCH_THEN (MP_TAC o (SPEC` norm (uh: real ^3)`));
995 REWRITE_TAC[NORM_POS_LT];
997 FIRST_X_ASSUM SUBST_ALL_TAC;
998 UNDISCH_TAC` (u:real^3) - u1 = vec 0 ` ;
999 REWRITE_TAC[VECTOR_SUB_EQ];
1001 ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
1002 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 `));
1003 ASSUME_TAC2 (ISPEC` v:real^3 ` (GEN_ALL Local_lemmas.COLLINEAR_ONCE_VEC_0));
1004 FIRST_X_ASSUM (MP_TAC o (SPEC` u: real^3 `));
1007 SUBGOAL_THEN` collinear {vec 0, v, u:real^3 } ` MP_TAC;
1009 DOWN THEN MESON_TAC[];
1011 MATCH_MP_TAC (GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO);
1012 EXISTS_TAC` rho_node1 FF v `;
1014 MATCH_MP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
1017 ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
1018 SUBGOAL_THEN` ~ collinear {vec 0, v, u:real^3} ` MP_TAC;
1019 MATCH_MP_TAC (GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO);
1020 EXISTS_TAC` rho_node1 FF v `;
1026 SUBGOAL_THEN` (uh: real^3) IN aff_gt {vec 0, v} {u} ` MP_TAC;
1027 ASM_REWRITE_TAC[IN_ELIM_THM];
1030 EXISTS_TAC` (u dot v) / (v dot (v:real^3))`;
1031 EXISTS_TAC` -- ((u dot v) / (v dot (v:real^3)))`;
1037 CONV_TAC VECTOR_ARITH;
1039 UNDISCH_TAC` ~collinear {vec 0, v, (u:real^3)}`;
1041 NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
1043 MP_TAC (ISPEC` {vec 0, v, u:real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL);
1044 ASSUME_TAC (ISPECL [` vec 0: real^3`;`u:real^3`] (GENL [` u:real^N `;` w:real^N `] AFF_GT_SUBSET_AFFINE_HULL21));
1046 SUBGOAL_THEN` {vec 0, v , uh:real^3} SUBSET affine hull {vec 0, v, u}` MP_TAC;
1047 MP_TAC (ISPEC` {vec 0, v, u:real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL);
1048 SIMP_TAC[INSERT_SUBSET];
1050 UNDISCH_TAC` aff_gt {vec 0, v} {u} SUBSET affine hull ({vec 0, v} UNION {u:real^3}) ` ;
1051 REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {a,b,c} `; SUBSET];
1052 DISCH_THEN MATCH_MP_TAC;
1053 FIRST_ASSUM ACCEPT_TAC;
1055 UNDISCH_TAC` uh IN aff_gt {vec 0, v} {u:real^3} `;
1056 UNDISCH_TAC` ~collinear {vec 0, v, u:real^3} `;
1058 NHANH Local_lemmas.COLL_IN_AFF_GT_TOO;
1061 UNDISCH_TAC` {vec 0, v, uh} SUBSET affine hull {vec 0, v, u:real^3} `;
1063 NHANH Local_lemmas.SUBSET_NOT_COLLINEAR_AFFINE_HULL_EQ;
1065 SUBGOAL_THEN` affine hull {vec 0, v, w, u:real^3} = affine hull {vec 0, v, u } ` ASSUME_TAC;
1066 MP_TAC (SPECL [` w:real^3 `;` {vec 0, v, u:real^3} `] Marchal_cells_3.AFFINE_HULL_3_INSERT);
1069 MP_TAC (ISPECL [` vec 0: real^3 `;` v:real^3 `; ` w:real^3 `] COLLINEAR_3_AFFINE_HULL);
1071 ONCE_REWRITE_TAC[EQ_SYM_EQ];
1073 ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
1074 FIRST_ASSUM MATCH_MP_TAC;
1075 FIRST_ASSUM ACCEPT_TAC;
1077 SUBGOAL_THEN` collinear {vec 0, v, w:real^3} ` MP_TAC;
1079 FIRST_ASSUM SUBST1_TAC;
1080 SPEC_TAC (`w:real^3 `,` w:real^3 `);
1081 REWRITE_TAC[GSYM SUBSET];
1082 MATCH_MP_TAC Marchal_cells_2_new.AFFINE_SUBSET_KY_LEMMA ;
1083 REWRITE_TAC[INSERT_SUBSET; IN_INSERT; EMPTY_SUBSET];
1084 REWRITE_TAC[INSERT_COMM];
1089 SUBGOAL_THEN` ! t. -- d < t /\ t < d /\ t IN real_interval (a,b) ==> f u t IN aff_gt {vec 0, v} {u:real^3} ` ASSUME_TAC;
1090 GEN_TAC THEN STRIP_TAC;
1091 UNDISCH_TAC` !t. t IN real_interval (a,b) ==> f u t IN affine hull {vec 0, v, w, u:real^3} ` ;
1093 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` t':real `));
1097 REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM];
1099 ASM_CASES_TAC` w' = &0 `;
1100 FIRST_X_ASSUM SUBST_ALL_TAC;
1101 UNDISCH_TAC` !x'. abs (x' - &0) < d ==> dist ((f: real^3 -> real -> real^3) u x',f u (&0)) < norm (uh: real^3) ` ;
1103 FIRST_ASSUM (MP_TAC o (SPEC` t': real `));
1104 REWRITE_TAC[REAL_SUB_RZERO; GSYM REAL_BOUNDS_LT];
1105 DISCH_THEN ASSUME_TAC2;
1107 SUBST_ALL_TAC (VECTOR_ARITH` u - u1 = (uh: real^3) <=> u = uh + u1 `);
1108 ASM_REWRITE_TAC[VECTOR_ARITH` u' % vec 0 + v' % v + &0 % uh = v' % v `];
1110 REWRITE_TAC[dist; Pack1.norm_ineq_lt; VECTOR_ARITH` a % v - ( u + b % v ) = ( a - b ) % v - u `];
1111 REWRITE_TAC[DOT_LSUB; DOT_RSUB; DOT_LMUL; DOT_RMUL];
1112 ABBREV_TAC` con1 = v' - (u dot v) / ((v:real^3) dot v) `;
1113 ASM_REWRITE_TAC[DOT_SYM; Collect_geom.ZERO_NEUTRAL; REAL_ARITH` a - ( &0 - x ) = a + x `];
1114 MP_TAC (ISPEC` v:real^3 ` DOT_POS_LE);
1115 REWRITE_TAC[REAL_ARITH` a + x < x <=> a < &0 `];
1116 MP_TAC (SPEC` con1: real` REAL_LE_SQUARE );
1119 ASSUME_TAC2 (SPECL [` con1 * (con1:real)`;` v dot (v:real^3) `] REAL_LE_MUL);
1122 ASM_CASES_TAC` w' < &0 `;
1123 UNDISCH_TAC` !x'. abs (x' - &0) < d ==> dist ((f:real^3 -> real -> real^3) u x',f u (&0)) < norm (uh: real^3) `;
1125 FIRST_ASSUM (MP_TAC o (SPEC` t': real `));
1126 REWRITE_TAC[REAL_SUB_RZERO; GSYM REAL_BOUNDS_LT];
1127 DISCH_THEN ASSUME_TAC2;
1129 SUBST_ALL_TAC (VECTOR_ARITH` u - u1 = uh <=> u = uh + (u1: real^3) `);
1130 ASM_REWRITE_TAC[dist];
1133 REWRITE_TAC[Pack1.norm_ineq_lt] ;
1135 REWRITE_TAC[VECTOR_ARITH` (u' % vec 0 + v' % v + w' % uh) - (uh + uv % v)
1136 = (v' - uv ) % v + (w' - &1) % uh `] ;
1137 ABBREV_TAC` con1 = (u dot v) / (v dot (v:real^3)) ` ;
1138 ASM_REWRITE_TAC[DOT_LADD; DOT_RADD; DOT_LMUL; DOT_RMUL; DOT_SYM; Collect_geom.ZERO_NEUTRAL] ;
1139 ASSUME_TAC (ISPEC` v:real^ 3 ` DOT_POS_LE) ;
1140 ASSUME_TAC (SPEC` v' - con1:real ` REAL_LE_SQUARE) ;
1141 ASSUME_TAC (ISPEC` uh:real^ 3 ` DOT_POS_LE) ;
1143 MP_TAC (ISPECL [` &1 `;` -- w' + &1 `] Collect_geom.POW2_COND) ;
1145 UNDISCH_TAC` w' < &0 ` ;
1148 SUBGOAL_THEN` &1 <= -- w' + &1 ` MP_TAC ;
1149 UNDISCH_TAC` w' < &0 ` ;
1153 REWRITE_TAC[REAL_ARITH` &1 pow 2 <= (--w' + &1) pow 2 <=> &0 <= (w' - &1 ) * (w' - &1 ) - &1 `] ;
1155 ASSUME_TAC2 (ISPECL[`(w' - &1) * (w' - &1) - &1 `;` (uh:real^3 ) dot uh `] REAL_LE_MUL) ;
1156 ASSUME_TAC2 (ISPECL[`(v' - con1) * (v' - con1)`;` (v:real^3 ) dot v `] REAL_LE_MUL) ;
1157 UNDISCH_TAC` (v' - con1) * (v' - con1) * ((v:real^3) dot v) +
1158 (w' - &1) * (w' - &1) * (uh dot uh) <
1159 uh dot (uh: real^3) ` ;
1162 SUBGOAL_THEN` f u (t': real) IN aff_gt {vec 0, v} {u:real^3} ` MP_TAC ;
1163 UNDISCH_TAC` aff_gt {vec 0, v} {u} = aff_gt {vec 0, v} {uh:real^3} ` ;
1164 DISCH_THEN SUBST1_TAC ;
1165 UNDISCH_TAC` ~collinear {vec 0, v, uh:real^3} ` ;
1168 SIMP_TAC[IN_ELIM_THM] ;
1170 EXISTS_TAC` u': real ` ;
1171 EXISTS_TAC` v':real ` ;
1172 EXISTS_TAC` w': real ` ;
1176 UNDISCH_TAC` ~( w' = &0 ) `;
1177 UNDISCH_TAC` ~( w' < &0 ) `;
1180 ASM_REWRITE_TAC[IN_ELIM_THM];
1183 SUBGOAL_THEN` ! t u. abs t < d /\ t IN real_interval (a,b) /\ (u:real^3) IN V ==> f u t IN aff_gt {vec 0, v} {u} ` MP_TAC;
1185 ASM_CASES_TAC` ~(u = u':real^3 )`;
1186 UNDISCH_TAC` !u' t. u' IN V /\ ~(u: real^3 = u') /\ t IN real_interval (a,b) ==> f u' t = u' `;
1187 DISCH_THEN (MP_TAC o (SPECL [` u':real^3 `;` t': real`]));
1191 MP_TAC (ISPECL [` {vec 0, v:real^3} `;` {u':real^3} `] (GEN_ALL Local_lemmas.CONV0_SUBSET_AFF_GT));
1192 SIMP_TAC[Geomdetail.CONV0_SING; INSERT_SUBSET];
1196 DISCH_THEN SUBST_ALL_TAC;
1197 FIRST_X_ASSUM MATCH_MP_TAC;
1198 ASM_REWRITE_TAC[REAL_BOUNDS_LT];
1202 SUBGOAL_THEN` ! t. abs t < d /\ t IN real_interval (a,b) ==> (! s. s IN IMAGE (IMAGE (\v. f (v:real^3) t)) E ==> aff_gt {vec 0} s SUBSET aff_gt { vec 0, v} {rho_node1 FF v } \/
1203 aff_gt {vec 0} s SUBSET aff_gt { vec 0, w} {rho_node1 FF w })` MP_TAC;
1208 REWRITE_TAC[GSYM REAL_BOUNDS_LT];
1213 GEN_TAC THEN STRIP_TAC;
1215 REWRITE_TAC[IN_IMAGE];
1218 UNDISCH_TAC` local_fan (V,E, FF) `;
1220 NHANH EDGE_IN_LOCAL_FAN_DET_RHO_NODE;
1222 UNDISCH_TAC` (v': real^3) IN V `;
1226 REWRITE_TAC[IN_ELIM_THM];
1227 ONCE_REWRITE_TAC[EQ_SYM_EQ];
1229 ASM_CASES_TAC` n'' < (j:num ) `;
1230 ASM_CASES_TAC` n'' = 0 `;
1231 FIRST_X_ASSUM SUBST_ALL_TAC;
1234 DISCH_THEN (SUBST_ALL_TAC o SYM);
1237 UNDISCH_TAC` !u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = (u': real^3) `;
1239 FIRST_ASSUM (MP_TAC o (SPECL [` w:real^3 `;` t': real `]));
1243 FIRST_ASSUM (MP_TAC o (SPECL [` t': real `;` rho_node1 FF w `]));
1245 ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT];
1246 MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
1248 MP_TAC Local_lemmas.AFF_GT_SAME_WITH_ENDS;
1250 ASM_REWRITE_TAC[lunar; circular];
1252 STRIP_TAC THEN STRIP_TAC;
1253 ASSUME_TAC2 (SPEC`w: real^3 ` (GEN`v: real^3 ` Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2));
1254 SUBGOAL_THEN` aff_gt {vec 0, w} {rho_node1 FF w} = aff_gt {vec 0, w} { f (rho_node1 FF w) (t':real)} ` MP_TAC;
1255 MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
1257 DISCH_THEN (ASSUME_TAC o SYM);
1261 MP_TAC (ISPECL [` {w:real^3} `;` {vec 0, w:real^3} `;` {(f (rho_node1 FF w) (t': real)): real^3 } `]
1262 (GEN_ALL Local_lemmas.AFF_GT_MONO_TRANS));
1264 REWRITE_TAC[IN_INSERT; INSERT_SUBSET; EMPTY_SUBSET];
1265 REWRITE_TAC[SET_RULE` A UNION {a} = a INSERT A `];
1266 ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
1267 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `));
1268 ASSUME_TAC2 (SET_RULE` ~((w:real^3) = vec 0) ==> {vec 0, w} DIFF {w} = {vec 0} `);
1269 UNDISCH_TAC` s = IMAGE (\v. (f:real^3 -> real -> real^3) v t') x `;
1270 DISCH_THEN (ASSUME_TAC o SYM);
1273 SUBGOAL_THEN` {w, f (rho_node1 FF w) (t':real)} = s ` MP_TAC;
1276 REWRITE_TAC[EXTENSION; IN_IMAGE];
1279 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY];
1281 EXISTS_TAC `w:real^3 `;
1284 EXISTS_TAC` rho_node1 FF w `;
1286 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY];
1296 ASM_CASES_TAC` n'' = j - 1 `;
1297 ASSUME_TAC2 (ARITH_RULE` ~( j = 0 ) ==> j - 1 + 1 = j`);
1298 SUBGOAL_THEN` rho_node1 FF v' = v ` MP_TAC;
1300 UNDISCH_TAC` n'' = j - 1 `;
1301 SIMP_TAC[GSYM ITER; ADD1];
1304 SUBGOAL_THEN` v' IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} ` MP_TAC;
1305 REWRITE_TAC[IN_ELIM_THM];
1306 EXISTS_TAC` n'':num `;
1307 ASM_REWRITE_TAC[ARITH_RULE` 0 < n <=> ~( n = 0) `];
1313 REWRITE_TAC[IN_INTER];
1322 SUBGOAL_THEN` IMAGE (\v. f v t') x = { f (v':real^3) (t':real), v:real^3} ` MP_TAC;
1323 REWRITE_TAC[EXTENSION];
1327 REWRITE_TAC[IN_IMAGE; IN_INSERT; NOT_IN_EMPTY];
1335 UNDISCH_TAC` !u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = (u': real^3) `;
1337 FIRST_ASSUM MATCH_MP_TAC;
1341 REWRITE_TAC[IN_IMAGE; IN_INSERT; NOT_IN_EMPTY];
1343 EXISTS_TAC `v': real^3 `;
1345 EXISTS_TAC` v: real^3 `;
1347 ONCE_REWRITE_TAC[EQ_SYM_EQ];
1348 FIRST_ASSUM MATCH_MP_TAC;
1353 FIRST_ASSUM (MP_TAC o (SPECL [` t': real`;` v': real^3 `]));
1355 ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT];
1357 MP_TAC (ISPECL [` {v:real^3 } `; `{ vec 0, v:real^3 } `;
1358 ` { (f: real^3 -> real -> real^3) v' t' } `] (GEN_ALL Local_lemmas.AFF_GT_MONO_TRANS));
1360 REWRITE_TAC[IN_INSERT; INSERT_SUBSET; EMPTY_SUBSET];
1361 ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
1362 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 `));
1364 SET_RULE` ~((v:real^3) = vec 0 ) ==> {vec 0, v} DIFF {v} = {vec 0 } `);
1365 ASM_REWRITE_TAC[SET_RULE` {a} UNION {b} = {a,b} `];
1367 MP_TAC Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI;
1369 ASM_REWRITE_TAC[lunar; circular];
1373 SPEC` w:real^3 ` (GEN` v:real^3 ` Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2));
1375 MP_TAC (GSYM Local_lemmas.AFF_GT_SAME_WITH_ENDS);
1377 ASM_REWRITE_TAC[lunar; circular];
1380 SUBGOAL_THEN` lunar (v,w:real^3) V E ` ASSUME_TAC;
1381 ASM_REWRITE_TAC[lunar; circular];
1382 ASSUME_TAC2 Local_lemmas.NOT_COLL_RHONODE_SND_POINT;
1383 UNDISCH_TAC` v' IN aff_gt {vec 0, w} {rho_node1 FF w} `;
1386 SUBGOAL_THEN` ~ collinear {vec 0, v, v':real^3 } ` MP_TAC;
1387 MATCH_MP_TAC (GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO);
1388 EXISTS_TAC` rho_node1 FF w `;
1393 UNDISCH_TAC` v' IN aff_gt {vec 0, v} {rho_node1 FF w} `;
1394 UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF w} `;
1396 NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
1398 SUBGOAL_THEN` aff_gt {vec 0, v} {f v' (t':real)} = aff_gt {vec 0, v} {v': real^3}` ASSUME_TAC;
1399 MATCH_MP_TAC (GSYM Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ);
1401 UNDISCH_TAC` aff_gt {vec 0} {f v' t', v} SUBSET aff_gt {vec 0, v} {(f: real^3 -> real -> real^3) v' t'} `;
1406 SUBGOAL_THEN` lunar (v, (w:real^3)) V E` ASSUME_TAC;
1407 ASM_REWRITE_TAC[lunar; circular];
1409 SUBGOAL_THEN` v' IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} /\
1410 rho_node1 FF v' IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} ` MP_TAC;
1412 REWRITE_TAC[IN_ELIM_THM];
1414 EXISTS_TAC`n'': num `;
1415 ASM_REWRITE_TAC[ARITH_RULE` 0 < n <=> ~( n = 0) `];
1416 EXISTS_TAC` n'' + 1 `;
1417 REWRITE_TAC[GSYM ITER; ADD1; ARITH_RULE` 0 < a + 1 `];
1418 MATCH_MP_TAC (ARITH_RULE` n'' < j /\ ~(n'' = j - 1)
1423 UNDISCH_TAC` aff_gt {vec 0, v} {u: real^3} =
1426 t1 + t2 + t3 = &1 /\
1427 y = t1 % vec 0 + t2 % v + t3 % u} `;
1428 DISCH_THEN (ASSUME_TAC o SYM);
1429 ASM_REWRITE_TAC[IN_INTER];
1433 REWRITE_TAC[IMAGE_CLAUSES];
1436 SPEC` w:real^3 ` (GEN` v: real^3 ` Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2));
1437 SUBGOAL_THEN` aff_gt {vec 0, w} {rho_node1 FF w } = aff_gt { vec 0, w} {v'} ` ASSUME_TAC;
1438 MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
1440 SUBGOAL_THEN` aff_gt {vec 0, w} {rho_node1 FF w } = aff_gt { vec 0, w} {rho_node1 FF v'} ` ASSUME_TAC;
1441 MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
1445 ASSUME_TAC2 (GSYM Local_lemmas.AFF_GT_SAME_WITH_ENDS);
1446 ASSUME_TAC2 Local_lemmas.NOT_COLL_RHONODE_SND_POINT;
1447 UNDISCH_TAC` v' IN aff_gt {vec 0, w} {rho_node1 FF w} `;
1450 SUBGOAL_THEN` aff_gt {vec 0, v} {rho_node1 FF w} = aff_gt {vec 0, v} {v'} ` ASSUME_TAC;
1451 MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
1455 SUBGOAL_THEN` f (v':real^3) (t': real) IN aff_gt {vec 0, w} {rho_node1 FF w} ` MP_TAC;
1457 FIRST_X_ASSUM MATCH_MP_TAC;
1458 ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT];
1459 SUBGOAL_THEN` f (rho_node1 FF v') (t': real) IN aff_gt {vec 0, w} {rho_node1 FF w} ` MP_TAC;
1461 UNDISCH_TAC` rho_node1 FF v' IN aff_gt {vec 0, w} {rho_node1 FF w} `;
1465 UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF w} `;
1467 NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
1470 FIRST_X_ASSUM MATCH_MP_TAC;
1471 ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT];
1475 let tt = GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO in
1476 ISPECL [` rho_node1 FF w` ;` vec 0: real^3 `;` w:real^3 `;
1477 ` (f:real^3 -> real -> real^3) v' t' `] tt);
1479 let tt = GEN_ALL Local_lemmas.COLL_IN_AFF_GT_TOO in
1480 ISPECL [` rho_node1 FF w` ;` vec 0: real^3 `;` w:real^3 `;
1481 ` (f:real^3 -> real -> real^3) (rho_node1 FF v') t' `] tt);
1485 NHANH (SET_RULE` ~( a = x ) /\ t /\ ~( a = y ) ==> DISJOINT {a} {x,y} `);
1487 UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF w} `;
1490 MATCH_MP_TAC TOW_POINTS_IN_IMP_AFF_GT_SUBSET;
1492 UNDISCH_TAC` (f: real^3 -> real -> real^3) v' t' IN aff_gt {vec 0, w} {rho_node1 FF w} `;
1493 UNDISCH_TAC` (f: real^3 -> real -> real^3) (rho_node1 FF v') t' IN aff_gt {vec 0, w} {rho_node1 FF w} `;
1497 ASM_CASES_TAC` n'' = (j:num) ` ;
1498 FIRST_X_ASSUM SUBST_ALL_TAC;
1502 REWRITE_TAC[IMAGE_CLAUSES];
1503 DISCH_THEN (SUBST_ALL_TAC o SYM);
1505 SUBGOAL_THEN` (f:real^3 -> real -> real^3) v t' = v ` ASSUME_TAC;
1506 FIRST_X_ASSUM MATCH_MP_TAC;
1512 let tt = GEN_ALL Local_lemmas.AFF_GT_MONO_TRANS in
1513 ISPECL [` {v:real^3 } `; `{vec 0, v:real^3} ` ;` { (f: real^3 -> real -> real^3) (rho_node1 FF v) t' }` ] tt);
1515 REWRITE_TAC[INSERT_SUBSET; IN_INSERT; EMPTY_SUBSET];
1516 ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
1517 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` v: real^3 `));
1518 ASSUME_TAC2 (SET_RULE` ~( v = vec 0) ==> {vec 0, v} DIFF {v} = {vec 0: real^3 }`);
1519 ASM_REWRITE_TAC[SET_RULE` {a} UNION {b} = {b,a} `];
1520 FIRST_ASSUM (MP_TAC o (ISPECL [` t': real `;` rho_node1 FF v `]));
1522 ASSUME_TAC2 Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
1524 ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT];
1527 let tt = GEN_ALL Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ in
1528 ISPECL [` rho_node1 FF v `;` vec 0: real^3 `;` v:real^3 `;` (f:real^3 -> real -> real^3) (rho_node1 FF v) t' `] tt);
1529 FIRST_X_ASSUM (SUBST1_TAC o SYM);
1535 ASM_CASES_TAC` n'' = CARD (V: real^3 -> bool) - 1 `;
1536 SUBGOAL_THEN` rho_node1 FF v' = w ` ASSUME_TAC;
1538 DOWN THEN SIMP_TAC[];
1540 REWRITE_TAC[GSYM ITER; ADD1];
1541 ASSUME_TAC2 (ARITH_RULE` n'' < CARD (V:real^3 -> bool) ==> CARD V - 1 + 1 = CARD V `);
1543 ASSUME_TAC2 Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID;
1544 FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `));
1552 ASSUME_TAC2 Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1;
1553 FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `));
1554 UNDISCH_TAC` ITER n'' (rho_node1 FF) w = v' `;
1558 SPECL [` w:real^3 `;` v:real^3 `] (GENL [` v: real^3 `;` w:real^3 `]
1559 Local_lemmas.AFF_IVS_RHO_NODE_EQQ)));
1561 ASM_REWRITE_TAC[Local_lemmas.LUNAR_COMM; lunar; circular; INSERT_SUBSET; EMPTY_SUBSET];
1562 UNDISCH_TAC` collinear {vec 0, v, w:real^3} `;
1563 SIMP_TAC[INSERT_COMM];
1569 ASM_REWRITE_TAC[IMAGE_CLAUSES];
1570 SUBGOAL_THEN` (f:real^3 -> real -> real^3 ) w t' = w ` ASSUME_TAC;
1571 FIRST_X_ASSUM MATCH_MP_TAC;
1575 FIRST_ASSUM (MP_TAC o (SPECL [` t': real `;` v': real^3 `]));
1577 ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT];
1579 ASSUME_TAC2 Polar_fan.IVS_RHO_NODE1_IN_V;
1580 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `));
1582 SUBGOAL_THEN` lunar (v,w:real^3) V E ` ASSUME_TAC;
1583 ASM_REWRITE_TAC[lunar; circular];
1584 MP_TAC Local_lemmas.IVS_RNODE_IN_AFF_V;
1588 STRIP_TAC THEN STRIP_TAC;
1590 let tt = GEN_ALL Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ in
1591 ISPECL [` rho_node1 FF v `;` vec 0: real^3 `;` v: real^3 `;` v': real^3 `] tt);
1595 UNDISCH_TAC ` ivs_rho_node1 FF w IN aff_gt {vec 0, v} {rho_node1 FF v} ` ;
1597 DISCH_THEN (SUBST_ALL_TAC o SYM);
1600 UNDISCH_TAC ` aff_gt {vec 0, v} {u: real^3} =
1603 t1 + t2 + t3 = &1 /\
1604 y = t1 % vec 0 + t2 % v + t3 % u}`;
1605 DISCH_THEN (ASSUME_TAC o SYM);
1607 SUBGOAL_THEN` aff_gt {vec 0, v} {uh: real^3} = aff_gt {vec 0, w} {ivs_rho_node1 FF w} ` MP_TAC;
1611 ASSUME_TAC2 (SPEC` w: real^3 ` Local_lemmas.LOFA_IMP_NOT_COLL_IVS);
1613 SUBGOAL_THEN` aff_gt {vec 0, w} {ivs_rho_node1 FF w} = aff_gt {vec 0, w} {(f: real^3 -> real -> real^3) v' t' } ` ASSUME_TAC;
1614 MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
1615 REPLICATE_TAC 3 DOWN THEN PHA;
1618 FIRST_X_ASSUM SUBST1_TAC;
1622 let tt = GEN_ALL Local_lemmas.AFF_GT_MONO_TRANS in
1623 ISPECL [` {w:real^3 } `;` {vec 0, w:real^3} `; `{(f: real^3 -> real -> real^3) v' t' } `] tt);
1625 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_INSERT];
1626 ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
1627 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `));
1629 SIMP_TAC[SET_RULE` ~(w = vec 0) ==> {vec 0, w} DIFF {w} = {vec 0 } `; SET_RULE` {a} UNION {b} = {a,b} `];
1631 SUBGOAL_THEN` x SUBSET {ITER l (rho_node1 FF) v | 0 < l /\ l < i} ` MP_TAC;
1633 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET; IN_ELIM_THM];
1634 ABBREV_TAC `i' = n'' - (j:num ) `;
1635 ASSUME_TAC2 (ARITH_RULE` ~( n'' < j) ==> (n'' - j) + j = (n'': num) `);
1636 SUBGOAL_THEN` ITER i' (rho_node1 FF) v = v' ` ASSUME_TAC;
1638 REWRITE_TAC[ITER_ADD];
1640 FIRST_ASSUM SUBST1_TAC;
1643 EXISTS_TAC` i': num `;
1647 UNDISCH_TAC` ~(n'' < j:num) `;
1648 UNDISCH_TAC` ~(n'' = j:num) `;
1652 UNDISCH_TAC` ~( n'' < j: num) `;
1653 SIMP_TAC[ARITH_RULE`~( n'' < j) ==> (n'' - j < i <=> n'' < i + (j:num))`];
1656 EXISTS_TAC` i' + 1 `;
1657 ASM_REWRITE_TAC[GSYM ADD1; ITER; ARITH_RULE` 0 < SUC a `];
1661 UNDISCH_TAC` ~( n'' < j: num) `;
1662 SIMP_TAC[ARITH_RULE`~( n'' < j) ==> (SUC (n'' - j) < i <=> n'' < (i + (j:num)) - 1 )`];
1665 MATCH_MP_TAC (ARITH_RULE` n < x /\ ~( n = x - 1) ==> n < x - 1 `);
1668 UNDISCH_TAC` aff_gt {vec 0, v} {rho_node1 FF v} = aff_gt {vec 0, v} {u} `;
1669 DISCH_THEN (ASSUME_TAC o SYM);
1672 REWRITE_TAC[IMAGE_CLAUSES; INSERT_SUBSET; EMPTY_SUBSET; IN_INTER];
1675 let tt = GEN_ALL Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ in
1676 ISPECL [` rho_node1 FF v `;` vec 0: real^3 `;` v:real^3 `;` v': real^3 `] tt);
1678 let tt = GEN_ALL Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ in
1679 ISPECL [` rho_node1 FF v `;` vec 0: real^3 `;` v:real^3 `;` rho_node1 FF v'`] tt);
1681 DISCH_THEN (ASSUME_TAC o SYM);
1682 DISCH_THEN (ASSUME_TAC o SYM);
1683 FIRST_ASSUM (MP_TAC o (SPECL [` t':real `;` v': real^3 `]));
1685 ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT];
1687 FIRST_ASSUM (MP_TAC o (SPECL [` t':real `;` rho_node1 FF v' `]));
1689 ASM_REWRITE_TAC[GSYM REAL_BOUNDS_LT];
1695 UNDISCH_TAC` ~ collinear {vec 0, v, rho_node1 FF v } `;
1697 NHANH Local_lemmas.COLL_IN_AFF_GT_TOO;
1704 UNDISCH_TAC` (f: real^3 -> real -> real^3) v' t' IN aff_gt {vec 0, v} {rho_node1 FF v} `;
1705 UNDISCH_TAC` ~ collinear {vec 0, v, rho_node1 FF v } `;
1707 NHANH Local_lemmas.COLL_IN_AFF_GT_TOO;
1712 MATCH_MP_TAC TOW_POINTS_IN_IMP_AFF_GT_SUBSET;
1713 ASM_REWRITE_TAC[SET_RULE` DISJOINT {a} {x,y} <=> ~( a = x ) /\ ~( a = y) `];
1717 SUBGOAL_THEN` !t. abs t < d /\ t IN real_interval (a,b)
1718 ==> (!s u. s IN IMAGE (IMAGE (\v. f v t)) E /\
1719 u IN IMAGE (\v. (f:real^3 -> real -> real^3) v t) V ==>
1720 (aff_gt {vec 0} s INTER aff_lt {vec 0} {u} =
1724 GEN_TAC THEN STRIP_TAC;
1726 GEN_TAC THEN GEN_TAC;
1727 ABBREV_TAC` vw = (aff_gt {vec 0} s SUBSET aff_gt {vec 0, v} {rho_node1 FF v} \/
1728 aff_gt {vec 0} s SUBSET aff_gt {vec 0, w} {rho_node1 FF w})`;
1732 REWRITE_TAC[IN_IMAGE];
1736 FIRST_ASSUM (MP_TAC o (SPECL [` t': real `;` x: real^3 `]));
1741 ASSUME_TAC2 Local_lemmas1.LOCAL_RHO_NODE_PAIR_E;
1743 SUBGOAL_THEN` FAN (vec 0: real^3,V,E)` MP_TAC;
1744 UNDISCH_TAC` local_fan (V: real^3 -> bool,E,FF) `;
1745 SIMP_TAC[local_fan];
1749 NHANH Topology.disjoint_fan3;
1752 ASSUME_TAC2 (SPEC` w: real^3 ` Local_lemmas1.LOCAL_RHO_NODE_PAIR_E);
1754 SUBGOAL_THEN` FAN (vec 0: real^3,V,E)` MP_TAC;
1755 UNDISCH_TAC` local_fan (V: real^3 -> bool,E,FF) `;
1756 SIMP_TAC[local_fan];
1760 NHANH Topology.disjoint_fan3;
1762 SUBGOAL_THEN` lunar (v,w:real^3) V E ` ASSUME_TAC;
1763 ASM_REWRITE_TAC[lunar; circular];
1764 ASSUME_TAC2 Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI;
1765 DOWN THEN STRIP_TAC;
1766 UNDISCH_TAC` vec 0 IN conv0 {v, w:real^3} `;
1767 NHANH IN_CONV0_IMP_AFF_EQ1;
1769 ASM_CASES_TAC ` x = v:real^3 `;
1770 FIRST_X_ASSUM SUBST_ALL_TAC;
1771 SUBGOAL_THEN` (f:real^3 -> real -> real^3) v t' = v ` MP_TAC;
1772 FIRST_ASSUM MATCH_MP_TAC;
1778 ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
1779 FIRST_ASSUM (ASSUME_TAC2 o SPEC_ALL);
1781 REWRITE_TAC[SET_RULE` ~( a = b) <=> DISJOINT {b} {a} `];
1782 NHANH AFF_LT_SUBSET_AFF11;
1783 UNDISCH_TAC` aff {vec 0, v} = aff {vec 0, w:real^3} `;
1784 UNDISCH_TAC` aff {vec 0, w} INTER aff_gt {vec 0, w} {rho_node1 FF w} = {} `;
1785 UNDISCH_TAC` aff {vec 0, v} INTER aff_gt {vec 0, v} {rho_node1 FF v} = {} `;
1786 UNDISCH_TAC` vw: bool `;
1790 MATCH_MP_TAC (SET_RULE`!A. a SUBSET A /\ x INTER A = {} ==> x INTER a = {} `);
1792 EXISTS_TAC` aff {vec 0, v:real^3} `;
1794 UNDISCH_TAC` aff_gt {vec 0} s SUBSET aff_gt {vec 0, v} {rho_node1 FF v} \/
1795 aff_gt {vec 0} s SUBSET aff_gt {vec 0, w} {rho_node1 FF w} `;
1797 MATCH_MP_TAC (SET_RULE`!A. a SUBSET A /\ x INTER A = {} ==> a INTER x = {} `);
1799 EXISTS_TAC` aff_gt {vec 0, v} {rho_node1 FF v} `;
1800 UNDISCH_TAC` aff_gt {vec 0, v} {u:real^3} =
1803 t1 + t2 + t3 = &1 /\
1804 y = t1 % vec 0 + t2 % v + t3 % u} `;
1805 DISCH_THEN (ASSUME_TAC o SYM);
1806 UNDISCH_TAC` aff_gt {vec 0, v} {rho_node1 FF v} = aff_gt {vec 0, v} {u} `;
1807 DISCH_THEN (ASSUME_TAC o SYM);
1808 UNDISCH_TAC` aff_gt {vec 0, v} {u} = aff_gt {vec 0, v} {uh: real^3} `;
1809 DISCH_THEN (ASSUME_TAC o SYM);
1813 UNDISCH_TAC` aff {vec 0, v} = aff {vec 0, w:real^3} `;
1814 DISCH_THEN (ASSUME_TAC o SYM);
1817 UNDISCH_TAC` aff {vec 0, w} INTER aff_gt {vec 0, w} {rho_node1 FF w} = {} `;
1821 ASM_CASES_TAC` x = (w:real^3) `;
1822 FIRST_X_ASSUM SUBST_ALL_TAC;
1823 SUBGOAL_THEN` (f:real^3 -> real -> real^3) w t' = w ` MP_TAC;
1824 FIRST_ASSUM MATCH_MP_TAC;
1830 UNDISCH_TAC` aff {vec 0, v} = aff {vec 0, w: real^3} `;
1831 UNDISCH_TAC` aff {vec 0, w} INTER aff_gt {vec 0, w} {rho_node1 FF w} = {} `;
1832 UNDISCH_TAC` aff {vec 0, v} INTER aff_gt {vec 0, v} {rho_node1 FF v} = {} `;
1833 ASSUME_TAC2 (Local_lemmas.LOFA_IMP_V_DIFF);
1834 FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC ` w:real^3 `));
1836 NHANH (SET_RULE` ~( a = b) ==> DISJOINT {b} {a} `);
1837 NHANH AFF_LT_SUBSET_AFF11;
1840 UNDISCH_TAC` vw: bool `;
1845 ASSUME_TAC2 LUNAR_IMP_IN_TWO_HAFLS_PLANE;
1846 FIRST_X_ASSUM (MP_TAC o (SPEC` x: real^3 `));
1850 ASSUME_TAC2 (GSYM Local_lemmas.AFF_IVS_RHO_NODE_EQQ);
1851 FIRST_ASSUM SUBST1_TAC;
1853 UNDISCH_TAC` aff_gt {vec 0, v} {rho_node1 FF v} = aff_gt {vec 0, v} {u} `;
1854 DISCH_THEN (ASSUME_TAC o SYM);
1855 ASSUME_TAC2 (GSYM Local_lemmas.AFF_GT_SAME_WITH_ENDS);
1856 UNDISCH_TAC` x IN aff_gt {vec 0, v} {rho_node1 FF v} \/
1857 x IN aff_gt {vec 0, w} {rho_node1 FF w} `;
1859 UNDISCH_TAC` vw: bool `;
1862 UNDISCH_TAC` x IN aff_gt {vec 0, v} {rho_node1 FF v} ` ;
1863 UNDISCH_TAC` ~ collinear {vec 0, v, rho_node1 FF v } `;
1865 NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
1867 FIRST_X_ASSUM (ASSUME_TAC o SYM);
1868 FIRST_ASSUM (MP_TAC o (SPECL [` t': real`;` x: real^3 `]));
1871 FIRST_ASSUM SUBST1_TAC;
1873 MATCH_MP_TAC (SET_RULE` ! s. a SUBSET s /\ s INTER b = {} ==> a INTER b = {} `);
1874 EXISTS_TAC` aff_gt {vec 0, v} {rho_node1 FF v} `;
1876 MATCH_MP_TAC COLL_IN_AFF_GT_INTER_EMPTY;
1879 ASM_CASES_TAC` aff_gt {vec 0} s INTER aff_lt {vec 0} {u': real^3} = {} `;
1880 FIRST_X_ASSUM ACCEPT_TAC;
1881 MP_TAC (ISPECL [` s: real^3 -> bool `; `u': real^3 `; `vec 0: real^3 `;
1882 `v:real^3 `; `rho_node1 FF v `; ` ivs_rho_node1 FF v `]
1883 (GEN_ALL AZIM_PI_LEMMA));
1888 STRIP_TAC THEN STRIP_TAC;
1889 ASSUME_TAC2 Local_lemmas.LOFA_IMP_NOT_COLL_IVS;
1891 SUBGOAL_THEN ` aff_gt {vec 0, v} {rho_node1 FF v} = aff_gt {vec 0, v} {x} ` ASSUME_TAC;
1892 MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
1896 UNDISCH_TAC` interior_angle1 (vec 0) FF v < pi `;
1897 ASSUME_TAC2 Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS;
1898 UNDISCH_TAC` interior_angle1 (vec 0) FF v = interior_angle1 (vec 0) FF w `;
1903 UNDISCH_TAC` vw: bool `;
1907 ASM_CASES_TAC` aff_gt {vec 0} s INTER aff_lt {vec 0} {u': real^3} = {} `;
1908 FIRST_X_ASSUM ACCEPT_TAC;
1911 let tt = GEN_ALL AZIM_PI_LEMMA in
1912 ISPECL [` s: real^3 -> bool `; `u': real^3 `;` vec 0: real^3 `;` w: real^3 `;
1913 ` rho_node1 FF w `;` ivs_rho_node1 FF w `] tt);
1918 SUBGOAL_THEN` aff_gt {vec 0, v} {rho_node1 FF v} =
1919 aff_gt {vec 0, w} {ivs_rho_node1 FF w} ` ASSUME_TAC;
1920 MATCH_MP_TAC Local_lemmas.AFF_IVS_RHO_NODE_EQQ;
1921 ASM_REWRITE_TAC[Local_lemmas.LUNAR_COMM];
1922 FIRST_X_ASSUM (ASSUME_TAC o SYM);
1926 ASSUME_TAC2 Local_lemmas.AFF_GT_SAME_WITH_ENDS;
1927 UNDISCH_TAC` x IN aff_gt {vec 0, w} {rho_node1 FF w} `;
1928 FIRST_X_ASSUM SUBST1_TAC;
1929 UNDISCH_TAC` aff_gt {vec 0, v} {ivs_rho_node1 FF v} =
1930 aff_gt {vec 0, w} {rho_node1 FF w} `;
1931 DISCH_THEN (SUBST1_TAC o SYM );
1932 ASSUME_TAC2 Local_lemmas.LOFA_IMP_NOT_COLL_IVS;
1933 ASSUME_TAC2 (SPEC` w: real^3 ` Local_lemmas.LOFA_IMP_NOT_COLL_IVS);
1936 SUBGOAL_THEN` aff_gt {vec 0, v} {ivs_rho_node1 FF v} = aff_gt {vec 0, v} {x} ` ASSUME_TAC;
1937 MATCH_MP_TAC Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
1941 MATCH_MP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
1944 UNDISCH_TAC` interior_angle1 (vec 0) FF v < pi `;
1946 ASSUME_TAC2 Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS;
1947 FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` w: real^ 3 `));
1950 MATCH_MP_TAC (SET_RULE` ! A. a SUBSET A /\ A INTER b = {} ==> a INTER b = {} `);
1951 EXISTS_TAC` aff_gt {vec 0, w} {rho_node1 FF w} `;
1954 MATCH_MP_TAC COLL_IN_AFF_GT_INTER_EMPTY;
1957 MATCH_MP_TAC Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
1959 UNDISCH_TAC` aff_gt {vec 0, w} {rho_node1 FF w} = aff_gt {vec 0, v} {rho_node1 FF w}`;
1960 ASSUME_TAC2 Local_lemmas.AFF_IVS_RHO_NODE_EQQ;
1962 FIRST_X_ASSUM SUBST1_TAC;
1963 DISCH_THEN (ASSUME_TAC o SYM);
1966 UNDISCH_TAC ` x IN aff_gt {vec 0, w} {rho_node1 FF w} `;
1967 UNDISCH_TAC` aff_gt {vec 0, v} {ivs_rho_node1 FF v} =
1968 aff_gt {vec 0, w} {rho_node1 FF w} `;
1969 DISCH_THEN (ASSUME_TAC o SYM);
1971 ASSUME_TAC2 Local_lemmas.LOFA_IMP_NOT_COLL_IVS;
1974 NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
1983 ABBREV_TAC` e1 = min ( -- a) b `;
1984 EXISTS_TAC` min e1 d `;
1988 REWRITE_TAC[REAL_LT_MIN];
1989 ASM_REWRITE_TAC[REAL_ARITH` &0 < -- a <=> a < &0 `];
1992 REWRITE_TAC[REAL_BOUNDS_LT];
1994 REWRITE_TAC[REAL_LT_MIN];
1997 REWRITE_TAC[MESON[] `
1998 ~(?v w u. P v w u /\ Q v w u /\ ~ R v w u ) <=>
1999 (! v w u. P v w u /\ Q v w u ==> R v w u ) `];
2001 FIRST_X_ASSUM (MP_TAC o (SPEC` t': real `));
2003 ASM_REWRITE_TAC[real_interval; IN_ELIM_THM];
2004 DOWN THEN DOWN THEN DOWN;
2012 FIRST_X_ASSUM MATCH_MP_TAC;
2013 DOWN THEN DOWN THEN DOWN;
2014 REWRITE_TAC[real_interval; IN_ELIM_THM];
2016 ASM_REWRITE_TAC[]]);;
2020 let LOCAL_FAN_SET_E = prove_by_refinement(` local_fan (V,E,FF) ==> {{v, rho_node1 FF v} | v IN V } = E `,
2021 [REWRITE_TAC[EXTENSION; IN_ELIM_THM];
2027 SIMP_TAC[GSYM EXTENSION];
2029 MATCH_MP_TAC Local_lemmas1.LOCAL_RHO_NODE_PAIR_E;
2031 REWRITE_TAC[GSYM EXTENSION];
2033 NHANH EDGE_IN_LOCAL_FAN_DET_RHO_NODE;
2034 SIMP_TAC[EQ_SYM_EQ]]);;
2040 let LOCAL_FAN_FACE_FF = prove_by_refinement(` local_fan (V,E,FF) ==> { v, rho_node1 FF v | v IN V } = FF `,
2041 [REWRITE_TAC[EXTENSION; IN_ELIM_THM];
2046 ASSUME_TAC2 Local_lemmas.LOCAL_FAN_RHO_NODE_PROS;
2047 DOWN THEN STRIP_TAC;
2049 FIRST_X_ASSUM MATCH_MP_TAC;
2050 FIRST_X_ASSUM ACCEPT_TAC;
2051 ASSUME_TAC2 Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2;
2052 DOWN THEN PHA THEN STRIP_TAC;
2053 FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` x: real^3 # real^3 `));
2054 EXISTS_TAC` FST (x: real^3 # real^3 ) `;
2056 ASSUME_TAC2 Local_lemmas.LOCAL_FAN_IMP_IN_V2;
2058 FIRST_X_ASSUM ACCEPT_TAC]);;
2065 let ORD_PAIRS_INJ_IMAGE = prove_by_refinement(` (! s. s IN E ==> INJ f s (IMAGE f s )) ==>
2066 ord_pairs (IMAGE (\s. IMAGE f s) E) = IMAGE (\ (x:real^N,y). (f: real^N -> real^M) x, f y) (ord_pairs E ) `,
2067 [REWRITE_TAC[EXTENSION];
2069 GEN_TAC THEN EQ_TAC;
2070 REWRITE_TAC[ord_pairs; IN_ELIM_THM; IN_IMAGE];
2071 NHANH_PAT `\x. x ==> y ` (SET_RULE` {a,b} = S ==> a IN S /\ b IN S `);
2072 REWRITE_TAC[IN_IMAGE];
2074 EXISTS_TAC` (x'': real^N, x''': real^N) `;
2077 SUBGOAL_THEN` {x'', x''': real^N} = x' ` MP_TAC;
2078 ASM_REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ; INSERT_SUBSET; EMPTY_SUBSET];
2080 FIRST_X_ASSUM NHANH;
2081 REWRITE_TAC[SUBSET; INJ];
2084 UNDISCH_TAC` !x. (x:real^N) IN x' ==> (f x):real^M IN IMAGE f x' `;
2085 DISCH_THEN (ASSUME_TAC2 o (SPEC` x'''': real^N `));
2092 REWRITE_TAC[IN_IMAGE; ord_pairs; IN_ELIM_THM];
2094 EXISTS_TAC` (f: real^N -> real^M ) a `;
2095 EXISTS_TAC` (f: real^N -> real^M ) b `;
2097 EXISTS_TAC` {a, b: real^N } `;
2098 ASM_REWRITE_TAC[IMAGE_CLAUSES]]);;
2105 prove(` s = {x,y} /\ a IN s /\ b IN s /\ ~( a = b) ==> s = {a, b} `,
2107 REPLICATE_TAC 3 DOWN THEN PHA THEN
2108 ASM_REWRITE_TAC[] THEN
2109 CONV_TAC SET_RULE);;
2113 let INSERT_UNION_CLAUSES =
2114 prove(` x INSERT S UNION U = S UNION x INSERT U /\ {} UNION U = U `,
2115 REWRITE_TAC[Local_lemmas.INSERT_UNION2; UNION_EMPTY]);;
2119 let INJ_IMP_BIJ_IMAGE = prove(` INJ f S S' ==> BIJ f S (IMAGE f S) `,
2120 SIMP_TAC[BIJ; INJ; SURJ; FUN_IN_IMAGE] THEN
2122 REWRITE_TAC[IN_IMAGE] THEN ASM_MESON_TAC[]);;
2128 let BIJ_AND_MAP_COMM = prove_by_refinement(` local_fan (V,E,FF) /\
2129 BIJ (f: real^3 -> real^3) V V' /\
2130 IMAGE (\s. IMAGE f s) E = E' /\
2131 FAN (vec 0, V', E') /\
2132 (\(x,y). f x, f y ) = ff
2133 ==> BIJ ff ( darts_of_hyp E V) (darts_of_hyp E' V') /\
2134 (!x. x IN darts_of_hyp E V
2135 ==> ff_of_hyp (vec 0,V',E') (ff x) = ff (ff_of_hyp (vec 0,V,E) x))
2139 [REWRITE_TAC[hyp_iso; local_fan];
2141 NHANH Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP;
2144 SUBGOAL_THEN` local_fan (V,E,FF) ` ASSUME_TAC;
2145 REWRITE_TAC[local_fan];
2152 EXISTS_TAC` (x: real^3 # real^3) `;
2154 UNDISCH_TAC` dart H = darts_of_hyp E (V: real^3 -> bool) `;
2155 DISCH_THEN SUBST_ALL_TAC;
2157 UNDISCH_TAC` dih2k (H:(real^3 # real^3) hypermap) (CARD (FF: real^3 # real^3 -> bool)) ` ;
2160 ASSUME_TAC2 LOCAL_FAN_SET_E;
2161 ASSUME_TAC2 Local_lemmas.LOFA_DARTS_FF_UNION_SWITCH_FF;
2162 ASSUME_TAC2 LOCAL_FAN_FACE_FF;
2164 MESON[] ` FF = face H x <=> face H x = (FF: real^3 # real^3 -> bool) `);
2168 SUBGOAL_THEN` {{(f: real^3 -> real^3) v, f (rho_node1 FF v)} | v IN V} = E' ` ASSUME_TAC;
2170 REWRITE_TAC[EXTENSION];
2173 REWRITE_TAC[IN_ELIM_THM; IN_IMAGE];
2176 EXISTS_TAC` {v, rho_node1 FF v} `;
2177 REWRITE_TAC[IMAGE_CLAUSES];
2179 EXISTS_TAC` v: real^3 `;
2183 EXISTS_TAC` v: real^3 `;
2184 ASM_REWRITE_TAC[IMAGE_CLAUSES];
2185 UNDISCH_TAC` BIJ (f: real^3 -> real^3) V V' `;
2186 PAT_REWRITE_TAC `\x. x ==> y ` [BIJ];
2187 NHANH Wrgcvdr_cizmrrh.SURJ_IMP_S2_EQ_IMAGE_S1;
2190 SUBGOAL_THEN` self_pairs E' (V': real^3 -> bool) = {} ` MP_TAC;
2191 REWRITE_TAC[self_pairs];
2194 REWRITE_TAC[IN_IMAGE];
2197 MATCH_MP_TAC (SET_RULE` (! x. ~ P x ) ==> {x,x | P x } = {} `);
2202 REWRITE_TAC[SET_RULE` ~( x = {} ) <=> ? a. a IN x `; EE; IN_ELIM_THM];
2203 EXISTS_TAC` (f: real^3 -> real^3) (rho_node1 FF x') `;
2204 EXISTS_TAC` x': real^3 `;
2208 SUBGOAL_THEN` darts_of_hyp E' V' = IMAGE (ff: real^3 # real^3 -> real^3 # real^3) (darts_of_hyp E V ) ` MP_TAC;
2210 ASM_REWRITE_TAC[darts_of_hyp; UNION_EMPTY; ord_pairs];
2212 SUBGOAL_THEN` (! s. s IN E ==> INJ (f:real^3 -> real^3) s (IMAGE f s)) ` MP_TAC;
2215 REWRITE_TAC[IN_IMAGE];
2216 EXISTS_TAC` x': real^3 `;
2218 UNDISCH_TAC` (s: real^3 -> bool) IN E `;
2220 REWRITE_TAC[IN_ELIM_THM];
2223 ASM_CASES_TAC` x' = (y:real^3) `;
2224 DOWN THEN SIMP_TAC[];
2225 REPLICATE_TAC 6 DOWN THEN PHA;
2227 MESON[SET2_DETER]` x' IN s /\
2231 s = {v, rho_node1 FF v} /\
2232 ~(x' = y) ==> s = {x', y} `);
2234 SUBGOAL_THEN` IMAGE (f: real^3 -> real^3 ) s IN E' ` ASSUME_TAC;
2236 ASM_REWRITE_TAC[IMAGE_CLAUSES];
2238 REWRITE_TAC[IN_ELIM_THM];
2240 EXISTS_TAC `v: real^3 `;
2242 UNDISCH_TAC` FAN (vec 0,V': real^3 -> bool,E') `;
2243 REWRITE_TAC[FAN; fan6];
2245 FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` IMAGE (f:real^3 -> real^3) s `));
2247 UNDISCH_TAC` s = {x', y:real^3} `;
2248 SIMP_TAC[IMAGE_CLAUSES; Local_lemmas.INSERT_UNION2; UNION_EMPTY];
2249 ASM_REWRITE_TAC[INSERT_INSERT; COLLINEAR_2];
2250 NHANH ORD_PAIRS_INJ_IMAGE;
2251 REWRITE_TAC[GSYM ord_pairs];
2262 SUBGOAL_THEN` (IMAGE (\s. IMAGE (f:real^3 -> real^3) s) E) = E': (real^3 -> bool) -> bool ` MP_TAC;
2263 REWRITE_TAC[EXTENSION; IN_IMAGE];
2267 FIRST_ASSUM (ASSUME_TAC o (SPEC` a: real^3 `));
2269 REWRITE_TAC[IN_ELIM_THM];
2272 REWRITE_TAC[IN_ELIM_THM];
2274 EXISTS_TAC` v: real^3 `;
2276 REPLICATE_TAC 4 DOWN THEN PHA;
2283 REWRITE_TAC[IN_ELIM_THM];
2285 EXISTS_TAC` {v, rho_node1 FF v }`;
2293 SUBGOAL_THEN` self_pairs E (V:real^3 -> bool) = {} ` MP_TAC;
2294 REWRITE_TAC[self_pairs; EE; SET_RULE` s = {} <=> ! x. ~ ( x IN s) `; IN_ELIM_THM];
2297 FIRST_X_ASSUM (MP_TAC o (SPEC` rho_node1 FF v `));
2300 REWRITE_TAC[IN_ELIM_THM];
2301 EXISTS_TAC` v: real^3 `;
2303 UNDISCH_TAC` darts_of_hyp E V = FF UNION {(v:real^3),w | w,v IN FF} `;
2304 DISCH_THEN (SUBST1_TAC o SYM);
2305 SIMP_TAC[darts_of_hyp; UNION_EMPTY];
2313 MATCH_MP_TAC (GEN_ALL INJ_IMP_BIJ_IMAGE);
2314 EXISTS_TAC` IMAGE (ff: real^3 # real^3 -> real^3 # real^3) (FF UNION {(v:real^3,w: real^3) | w,v IN FF} )`;
2315 REWRITE_TAC[INJ; FUN_IN_IMAGE];
2319 SUBGOAL_THEN` !x. x IN FF UNION {v,w | w,v IN FF} ==> (? a b. x = (a,b) /\ a IN V /\ b IN (V: real^3 -> bool)) ` MP_TAC;
2320 REWRITE_TAC[IN_UNION];
2324 REWRITE_TAC[IN_ELIM_THM];
2326 EXISTS_TAC` v: real^3 `;
2327 EXISTS_TAC` rho_node1 FF v `;
2329 MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
2333 REWRITE_TAC[IN_ELIM_THM];
2335 EXISTS_TAC` rho_node1 FF v' `;
2336 EXISTS_TAC` v': real^ 3 `;
2338 ASM_SIMP_TAC[PAIR_EQ];
2340 MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
2347 REWRITE_TAC[PAIR_EQ];
2348 UNDISCH_TAC` INJ (f:real^3 -> real^3) V V' `;
2350 UNDISCH_TAC` (a:real^3) IN V `;
2351 UNDISCH_TAC` (b: real^3) IN V `;
2355 UNDISCH_TAC` darts_of_hyp E V = FF UNION {v:real^3,w | w,v IN FF} `;
2356 DISCH_THEN (ASSUME_TAC2 o SYM);
2359 SUBGOAL_THEN` (ff: real^3 # real^3 -> real^3 # real^3) x' IN darts_of_hyp E' V' ` MP_TAC;
2361 MATCH_MP_TAC FUN_IN_IMAGE;
2362 FIRST_ASSUM ACCEPT_TAC;
2364 SIMP_TAC[Wrgcvdr_cizmrrh.ff_of_hyp2];
2366 FIRST_X_ASSUM (SUBST1_TAC o SYM);
2368 REWRITE_TAC[IN_UNION];
2369 STRIP_TAC THEN STRIP_TAC;
2370 UNDISCH_TAC` (x': real^3 # real^3 ) IN FF `;
2372 REWRITE_TAC[IN_ELIM_THM];
2376 REWRITE_TAC[PAIR_EQ];
2377 SUBGOAL_THEN` rho_node1 FF v IN V ` MP_TAC;
2378 MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
2380 UNDISCH_TAC` local_fan (V,E,FF) `;
2382 NHANH Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND;
2383 ASSUME_TAC2 Local_lemmas.IVS_RHO_IDD;
2385 ONCE_REWRITE_TAC[INSERT_COMM];
2386 REWRITE_TAC[Polar_fan.IVS_AZIM_CYCLE_TWO_POINT_SET];
2389 SUBGOAL_THEN` EE ((f:real^3 -> real^3) (rho_node1 FF v)) E' = { f v, f (rho_node1 FF (rho_node1 FF v )) } ` MP_TAC;
2390 REWRITE_TAC[EE; GSYM SUBSET_ANTISYM_EQ; SUBSET];
2393 REWRITE_TAC[IN_ELIM_THM];
2395 REWRITE_TAC[IN_ELIM_THM];
2398 REWRITE_TAC[Collect_geom.PAIR_EQ_EXPAND];
2400 UNDISCH_TAC` INJ (f: real^3 -> real ^3) V V' `;
2403 FIRST_ASSUM (ASSUME_TAC2 o (SPECL [`rho_node1 FF v `;` v': real^3 `]));
2407 UNDISCH_TAC` INJ (f: real^3 -> real ^3) V V' `;
2410 FIRST_ASSUM (MP_TAC o (SPECL [`rho_node1 FF v `;` rho_node1 FF v'`]));
2413 MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
2415 ASSUME_TAC2 Polar_fan.RHO_NODE1_INJECTIVE;
2416 FIRST_X_ASSUM (ASSUME_TAC2 o (SPECL[` v: real^3 `;` v': real^3 `]));
2418 REWRITE_TAC[IN_INSERT];
2419 GEN_TAC THEN REWRITE_TAC[IN_ELIM_THM];
2420 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY];
2424 REWRITE_TAC[IN_ELIM_THM];
2425 EXISTS_TAC `v: real^3 `;
2426 ASM_REWRITE_TAC[INSERT_COMM];
2429 REWRITE_TAC[IN_ELIM_THM];
2430 EXISTS_TAC` rho_node1 FF v `;
2432 SIMP_TAC[Polar_fan.IVS_AZIM_CYCLE_TWO_POINT_SET];
2436 UNDISCH_TAC` (x': real^3 # real^3) IN {v,w | w,v IN FF} `;
2438 REWRITE_TAC[IN_ELIM_THM; PAIR_EQ];
2442 REWRITE_TAC[PAIR_EQ];
2444 SPEC` v': real^3 ` (
2445 GEN`v: real^3 ` Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND));
2446 ASM_REWRITE_TAC[Polar_fan.IVS_AZIM_CYCLE_TWO_POINT_SET];
2447 SUBGOAL_THEN` EE ((f:real^3 -> real^3) v') E'= { f (rho_node1 FF v'), f (ivs_rho_node1 FF v' )} ` MP_TAC;
2448 REWRITE_TAC[EE; GSYM SUBSET_ANTISYM_EQ; SUBSET];
2450 UNDISCH_TAC` INJ (f: real^3 -> real^3) V V' `;
2457 REWRITE_TAC[IN_ELIM_THM; Collect_geom.PAIR_EQ_EXPAND];
2459 FIRST_X_ASSUM (ASSUME_TAC2 o (SPECL [` v': real^3 `;` v'': real^3 `]));
2460 ASM_REWRITE_TAC[IN_INSERT];
2462 FIRST_X_ASSUM (MP_TAC o (SPECL [` v': real^3 `;` rho_node1 FF v'' `]));
2464 ASM_REWRITE_TAC[IN_INSERT];
2465 MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
2470 SPEC ` v'': real^3 ` (
2471 GEN`v: real^3 ` Local_lemmas.IVS_RHO_IDD));
2472 ASM_REWRITE_TAC[IN_INSERT];
2474 REWRITE_TAC[IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY];
2478 REWRITE_TAC[IN_ELIM_THM];
2479 EXISTS_TAC` v': real^3 `;
2483 REWRITE_TAC[IN_ELIM_THM];
2484 EXISTS_TAC` ivs_rho_node1 FF v' `;
2486 ASSUME_TAC2 Polar_fan.IVS_RHO_NODE1_IN_V;
2488 FIRST_X_ASSUM MATCH_MP_TAC;
2489 FIRST_ASSUM ACCEPT_TAC;
2491 SPEC` v': real ^3 ` (
2492 GEN`v: real^3 ` Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS ));
2493 ASM_REWRITE_TAC[INSERT_COMM];
2494 SIMP_TAC[Polar_fan.IVS_AZIM_CYCLE_TWO_POINT_SET]]);;
2498 let NODE_EDGE_COMM_LEMMA = prove_by_refinement (` local_fan (V,E,FF) /\
2500 IMAGE (\s. IMAGE f s) E = E' /\
2501 FAN (vec 0,V',E') /\
2502 (\(x,y). f x,f y) = ff
2504 (!x. x IN darts_of_hyp E V
2505 ==> nn_of_hyp (vec 0,V',E') (ff x) =
2506 ff (nn_of_hyp (vec 0,V,E) x) /\
2507 ee_of_hyp (vec 0,V',E') (ff x) =
2508 ff (ee_of_hyp (vec 0,V,E) x) ) `,
2512 [REWRITE_TAC[hyp_iso; local_fan];
2514 NHANH Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP;
2517 SUBGOAL_THEN` local_fan (V,E,FF) ` ASSUME_TAC;
2518 REWRITE_TAC[local_fan];
2525 EXISTS_TAC` (x: real^3 # real^3) `;
2527 UNDISCH_TAC` dart H = darts_of_hyp E (V: real^3 -> bool) `;
2528 DISCH_THEN SUBST_ALL_TAC;
2530 UNDISCH_TAC` dih2k (H:(real^3 # real^3) hypermap) (CARD (FF: real^3 # real^3 -> bool)) ` ;
2533 ASSUME_TAC2 LOCAL_FAN_SET_E;
2534 ASSUME_TAC2 Local_lemmas.LOFA_DARTS_FF_UNION_SWITCH_FF;
2535 ASSUME_TAC2 LOCAL_FAN_FACE_FF;
2537 MESON[] ` FF = face H x <=> face H x = (FF: real^3 # real^3 -> bool) `);
2541 SUBGOAL_THEN` {{(f: real^3 -> real^3) v, f (rho_node1 FF v)} | v IN V} = E' ` ASSUME_TAC;
2543 REWRITE_TAC[EXTENSION];
2546 REWRITE_TAC[IN_ELIM_THM; IN_IMAGE];
2549 EXISTS_TAC` {v, rho_node1 FF v} `;
2550 REWRITE_TAC[IMAGE_CLAUSES];
2552 EXISTS_TAC` v: real^3 `;
2556 EXISTS_TAC` v: real^3 `;
2557 ASM_REWRITE_TAC[IMAGE_CLAUSES];
2558 UNDISCH_TAC` BIJ (f: real^3 -> real^3) V V' `;
2559 PAT_REWRITE_TAC `\x. x ==> y ` [BIJ];
2560 NHANH Wrgcvdr_cizmrrh.SURJ_IMP_S2_EQ_IMAGE_S1;
2563 SUBGOAL_THEN` self_pairs E' (V': real^3 -> bool) = {} ` MP_TAC;
2564 REWRITE_TAC[self_pairs];
2567 REWRITE_TAC[IN_IMAGE];
2570 MATCH_MP_TAC (SET_RULE` (! x. ~ P x ) ==> {x,x | P x } = {} `);
2575 REWRITE_TAC[SET_RULE` ~( x = {} ) <=> ? a. a IN x `; EE; IN_ELIM_THM];
2576 EXISTS_TAC` (f: real^3 -> real^3) (rho_node1 FF x') `;
2577 EXISTS_TAC` x': real^3 `;
2581 SUBGOAL_THEN` darts_of_hyp E' V' = IMAGE (ff: real^3 # real^3 -> real^3 # real^3) (darts_of_hyp E V ) ` MP_TAC;
2583 ASM_REWRITE_TAC[darts_of_hyp; UNION_EMPTY; ord_pairs];
2585 SUBGOAL_THEN` (! s. s IN E ==> INJ (f:real^3 -> real^3) s (IMAGE f s)) ` MP_TAC;
2588 REWRITE_TAC[IN_IMAGE];
2589 EXISTS_TAC` x': real^3 `;
2591 UNDISCH_TAC` (s: real^3 -> bool) IN E `;
2593 REWRITE_TAC[IN_ELIM_THM];
2596 ASM_CASES_TAC` x' = (y:real^3) `;
2597 DOWN THEN SIMP_TAC[];
2598 REPLICATE_TAC 6 DOWN THEN PHA;
2600 MESON[SET2_DETER]` x' IN s /\
2604 s = {v, rho_node1 FF v} /\
2605 ~(x' = y) ==> s = {x', y} `);
2607 SUBGOAL_THEN` IMAGE (f: real^3 -> real^3 ) s IN E' ` ASSUME_TAC;
2609 ASM_REWRITE_TAC[IMAGE_CLAUSES];
2611 REWRITE_TAC[IN_ELIM_THM];
2613 EXISTS_TAC `v: real^3 `;
2615 UNDISCH_TAC` FAN (vec 0,V': real^3 -> bool,E') `;
2616 REWRITE_TAC[FAN; fan6];
2618 FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` IMAGE (f:real^3 -> real^3) s `));
2620 UNDISCH_TAC` s = {x', y:real^3} `;
2621 SIMP_TAC[IMAGE_CLAUSES; Local_lemmas.INSERT_UNION2; UNION_EMPTY];
2622 ASM_REWRITE_TAC[INSERT_INSERT; COLLINEAR_2];
2623 NHANH ORD_PAIRS_INJ_IMAGE;
2624 REWRITE_TAC[GSYM ord_pairs];
2635 SUBGOAL_THEN` (IMAGE (\s. IMAGE (f:real^3 -> real^3) s) E) = E': (real^3 -> bool) -> bool ` MP_TAC;
2636 REWRITE_TAC[EXTENSION; IN_IMAGE];
2640 FIRST_ASSUM (ASSUME_TAC o (SPEC` a: real^3 `));
2642 REWRITE_TAC[IN_ELIM_THM];
2645 REWRITE_TAC[IN_ELIM_THM];
2647 EXISTS_TAC` v: real^3 `;
2649 REPLICATE_TAC 4 DOWN THEN PHA;
2656 REWRITE_TAC[IN_ELIM_THM];
2658 EXISTS_TAC` {v, rho_node1 FF v }`;
2666 SUBGOAL_THEN` self_pairs E (V:real^3 -> bool) = {} ` MP_TAC;
2667 REWRITE_TAC[self_pairs; EE; SET_RULE` s = {} <=> ! x. ~ ( x IN s) `; IN_ELIM_THM];
2670 FIRST_X_ASSUM (MP_TAC o (SPEC` rho_node1 FF v `));
2673 REWRITE_TAC[IN_ELIM_THM];
2674 EXISTS_TAC` v: real^3 `;
2676 UNDISCH_TAC` darts_of_hyp E V = FF UNION {(v:real^3),w | w,v IN FF} `;
2677 DISCH_THEN (SUBST1_TAC o SYM);
2678 SIMP_TAC[darts_of_hyp; UNION_EMPTY];
2681 REWRITE_TAC[Wrgcvdr_cizmrrh.nn_of_hyp2];
2682 UNDISCH_TAC` darts_of_hyp E V = FF UNION {v:real^3,w | w,v IN FF} `;
2683 DISCH_THEN (ASSUME_TAC o SYM);
2685 SUBGOAL_THEN`(! x. x IN darts_of_hyp E (V:real^3 -> bool) ==> ((ff x): real^3 # real^3) IN darts_of_hyp E' V' )` MP_TAC;
2686 ASM_REWRITE_TAC[FUN_IN_IMAGE];
2691 SUBGOAL_THEN` ! v. v IN V ==> ivs_rho_node1 FF (rho_node1 FF v) = v ` ASSUME_TAC;
2692 GEN_TAC THEN STRIP_TAC;
2693 MATCH_MP_TAC Local_lemmas.IVS_RHO_IDD;
2695 SUBGOAL_THEN` ! v. v IN V ==> rho_node1 FF (ivs_rho_node1 FF v) = v ` ASSUME_TAC;
2696 GEN_TAC THEN STRIP_TAC;
2697 MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS;
2701 SUBGOAL_THEN` !v . v IN V ==> rho_node1 FF v IN V ` ASSUME_TAC;
2702 GEN_TAC THEN STRIP_TAC;
2703 MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
2704 ASM_SIMP_TAC[Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V];
2707 SUBGOAL_THEN` !v . v IN V ==> ivs_rho_node1 FF v IN V ` ASSUME_TAC;
2708 MATCH_MP_TAC Polar_fan.IVS_RHO_NODE1_IN_V;
2709 EXISTS_TAC` E: (real^3 -> bool) -> bool `;
2714 UNDISCH_TAC` INJ (f: real^3 -> real^3) V V' `;
2719 SUBGOAL_THEN` !v. v IN V
2720 ==> EE v E = {rho_node1 FF v, (ivs_rho_node1 FF v)} ` ASSUME_TAC;
2722 MATCH_MP_TAC Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND;
2729 SUBGOAL_THEN`!v. v IN V ==> EE ((f:real^3 -> real^3) v ) E' = {f (rho_node1 FF v), f (ivs_rho_node1 FF v ) } ` ASSUME_TAC;
2731 REWRITE_TAC[EE; GSYM SUBSET_ANTISYM_EQ; SUBSET];
2733 REWRITE_TAC[IN_ELIM_THM];
2735 GEN_TAC THEN STRIP_TAC;
2737 REWRITE_TAC[Collect_geom.PAIR_EQ_EXPAND];
2739 FIRST_X_ASSUM (ASSUME_TAC2 o (SPECL [` v: real^3 `;` v': real^3 `]));
2740 ASM_REWRITE_TAC[IN_INSERT];
2741 FIRST_X_ASSUM (MP_TAC o (SPECL [` v: real^3 `;` rho_node1 FF v' `]));
2743 ASM_REWRITE_TAC[IN_INSERT];
2744 MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
2748 ASM_SIMP_TAC[IN_INSERT];
2749 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY];
2750 GEN_TAC THEN STRIP_TAC;
2751 EXISTS_TAC` v: real^3 `;
2753 EXISTS_TAC` ivs_rho_node1 FF v `;
2754 ASM_SIMP_TAC[INSERT_COMM];
2756 GEN_TAC THEN STRIP_TAC;
2757 SUBGOAL_THEN` x' IN FF UNION {v:real^3,w | w,v IN FF} ` MP_TAC;
2759 REWRITE_TAC[IN_UNION];
2763 REWRITE_TAC[IN_ELIM_THM];
2770 ASM_SIMP_TAC[PAIR_EQ];
2771 REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET];
2773 REWRITE_TAC[Wrgcvdr_cizmrrh.ee_of_hyp2];
2774 UNDISCH_TAC` x' IN darts_of_hyp E (V: real^3 -> bool) `;
2775 UNDISCH_TAC` (ff: real^3 # real^3 -> real^3 # real^3 ) x' IN IMAGE ff (darts_of_hyp E V) `;
2782 REWRITE_TAC[IN_ELIM_THM; PAIR_EQ];
2786 REWRITE_TAC[PAIR_EQ];
2788 ONCE_REWRITE_TAC[INSERT_COMM];
2789 REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET];
2791 REWRITE_TAC[Wrgcvdr_cizmrrh.ee_of_hyp2];
2792 UNDISCH_TAC` x' IN darts_of_hyp E (V: real^3 -> bool) `;
2793 UNDISCH_TAC` (ff: real^3 # real^3 -> real^3 # real^3 ) x' IN IMAGE ff (darts_of_hyp E V) `;
2802 let HYP_ISO_LEMMAA = prove_by_refinement (` local_fan (V,E,FF) /\
2804 IMAGE (\s. IMAGE f s) E = E' /\
2805 FAN (vec 0,V',E') /\
2806 (\(x,y). f x,f y) = ff
2807 ==> hyp_iso ff (hypermap (HYP (vec 0, V, E)), hypermap (HYP (vec 0, V', E')))`,
2808 [REWRITE_TAC[hyp_iso; local_fan];
2810 NHANH Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP;
2813 SUBGOAL_THEN` local_fan (V,E,FF) ` ASSUME_TAC;
2814 REWRITE_TAC[local_fan];
2821 EXISTS_TAC` (x: real^3 # real^3) `;
2823 UNDISCH_TAC` dart H = darts_of_hyp E (V: real^3 -> bool) `;
2824 DISCH_THEN SUBST_ALL_TAC;
2826 UNDISCH_TAC` dih2k (H:(real^3 # real^3) hypermap) (CARD (FF: real^3 # real^3 -> bool)) ` ;
2829 ASSUME_TAC2 LOCAL_FAN_SET_E;
2830 ASSUME_TAC2 Local_lemmas.LOFA_DARTS_FF_UNION_SWITCH_FF;
2831 ASSUME_TAC2 LOCAL_FAN_FACE_FF;
2833 MESON[] ` FF = face H x <=> face H x = (FF: real^3 # real^3 -> bool) `);
2837 SUBGOAL_THEN` {{(f: real^3 -> real^3) v, f (rho_node1 FF v)} | v IN V} = E' ` ASSUME_TAC;
2839 REWRITE_TAC[EXTENSION];
2842 REWRITE_TAC[IN_ELIM_THM; IN_IMAGE];
2845 EXISTS_TAC` {v, rho_node1 FF v} `;
2846 REWRITE_TAC[IMAGE_CLAUSES];
2848 EXISTS_TAC` v: real^3 `;
2852 EXISTS_TAC` v: real^3 `;
2853 ASM_REWRITE_TAC[IMAGE_CLAUSES];
2854 UNDISCH_TAC` BIJ (f: real^3 -> real^3) V V' `;
2855 PAT_REWRITE_TAC `\x. x ==> y ` [BIJ];
2856 NHANH Wrgcvdr_cizmrrh.SURJ_IMP_S2_EQ_IMAGE_S1;
2859 SUBGOAL_THEN` self_pairs E' (V': real^3 -> bool) = {} ` MP_TAC;
2860 REWRITE_TAC[self_pairs];
2863 REWRITE_TAC[IN_IMAGE];
2866 MATCH_MP_TAC (SET_RULE` (! x. ~ P x ) ==> {x,x | P x } = {} `);
2871 REWRITE_TAC[SET_RULE` ~( x = {} ) <=> ? a. a IN x `; EE; IN_ELIM_THM];
2872 EXISTS_TAC` (f: real^3 -> real^3) (rho_node1 FF x') `;
2873 EXISTS_TAC` x': real^3 `;
2877 SUBGOAL_THEN` darts_of_hyp E' V' = IMAGE (ff: real^3 # real^3 -> real^3 # real^3) (darts_of_hyp E V ) ` MP_TAC;
2879 ASM_REWRITE_TAC[darts_of_hyp; UNION_EMPTY; ord_pairs];
2881 SUBGOAL_THEN` (! s. s IN E ==> INJ (f:real^3 -> real^3) s (IMAGE f s)) ` MP_TAC;
2884 REWRITE_TAC[IN_IMAGE];
2885 EXISTS_TAC` x': real^3 `;
2887 UNDISCH_TAC` (s: real^3 -> bool) IN E `;
2889 REWRITE_TAC[IN_ELIM_THM];
2892 ASM_CASES_TAC` x' = (y:real^3) `;
2893 DOWN THEN SIMP_TAC[];
2894 REPLICATE_TAC 6 DOWN THEN PHA;
2896 MESON[SET2_DETER]` x' IN s /\
2900 s = {v, rho_node1 FF v} /\
2901 ~(x' = y) ==> s = {x', y} `);
2903 SUBGOAL_THEN` IMAGE (f: real^3 -> real^3 ) s IN E' ` ASSUME_TAC;
2905 ASM_REWRITE_TAC[IMAGE_CLAUSES];
2907 REWRITE_TAC[IN_ELIM_THM];
2909 EXISTS_TAC `v: real^3 `;
2911 UNDISCH_TAC` FAN (vec 0,V': real^3 -> bool,E') `;
2912 REWRITE_TAC[FAN; fan6];
2914 FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` IMAGE (f:real^3 -> real^3) s `));
2916 UNDISCH_TAC` s = {x', y:real^3} `;
2917 SIMP_TAC[IMAGE_CLAUSES; Local_lemmas.INSERT_UNION2; UNION_EMPTY];
2918 ASM_REWRITE_TAC[INSERT_INSERT; COLLINEAR_2];
2919 NHANH ORD_PAIRS_INJ_IMAGE;
2920 REWRITE_TAC[GSYM ord_pairs];
2931 SUBGOAL_THEN` (IMAGE (\s. IMAGE (f:real^3 -> real^3) s) E) = E': (real^3 -> bool) -> bool ` MP_TAC;
2932 REWRITE_TAC[EXTENSION; IN_IMAGE];
2936 FIRST_ASSUM (ASSUME_TAC o (SPEC` a: real^3 `));
2938 REWRITE_TAC[IN_ELIM_THM];
2941 REWRITE_TAC[IN_ELIM_THM];
2943 EXISTS_TAC` v: real^3 `;
2945 REPLICATE_TAC 4 DOWN THEN PHA;
2952 REWRITE_TAC[IN_ELIM_THM];
2954 EXISTS_TAC` {v, rho_node1 FF v }`;
2962 SUBGOAL_THEN` self_pairs E (V:real^3 -> bool) = {} ` MP_TAC;
2963 REWRITE_TAC[self_pairs; EE; SET_RULE` s = {} <=> ! x. ~ ( x IN s) `; IN_ELIM_THM];
2966 FIRST_X_ASSUM (MP_TAC o (SPEC` rho_node1 FF v `));
2969 REWRITE_TAC[IN_ELIM_THM];
2970 EXISTS_TAC` v: real^3 `;
2972 UNDISCH_TAC` darts_of_hyp E V = FF UNION {(v:real^3),w | w,v IN FF} `;
2973 DISCH_THEN (SUBST1_TAC o SYM);
2974 SIMP_TAC[darts_of_hyp; UNION_EMPTY];
2977 MP_TAC BIJ_AND_MAP_COMM;
2979 ASM_REWRITE_TAC[BIJ];
2981 MP_TAC NODE_EDGE_COMM_LEMMA;
2983 ASM_REWRITE_TAC[BIJ];
2988 NHANH (ISPEC `ff: real^3 # real^3 -> real^3 # real^3 ` FUN_IN_IMAGE);
2990 ASM_REWRITE_TAC[Wrgcvdr_cizmrrh.ee_of_hyp2];
2991 UNDISCH_TAC` x' IN FF UNION {v,w | w:real^3,v IN FF} `;
2992 REWRITE_TAC[IN_ELIM_THM];
2993 SUBGOAL_THEN` x' IN FF UNION {v:real^3,w | w,v IN FF} ==> ? a b. x' = (a,b) ` MP_TAC;
2995 REWRITE_TAC[IN_UNION; IN_ELIM_THM];
3008 REWRITE_RULE[IN_UNIV] (SPEC` (:A) ` Hypermap_iso.power_comm);;
3011 REWRITE_RULE[Wrgcvdr_cizmrrh.POWER_TO_ITER] POWER_COMM;;
3016 let IMAGE_FACE_F = prove_by_refinement(
3017 ` hyp_iso (f: A -> B) (H,HH) ==> ! x . x IN dart H ==> IMAGE f (face H x ) = face HH ( f x ) `,
3018 [REWRITE_TAC[hyp_iso];
3019 STRIP_TAC THEN GEN_TAC THEN STRIP_TAC;
3020 REWRITE_TAC[EXTENSION; face; orbit_map; IN_ELIM_THM];
3021 SUBGOAL_THEN`! x n. x IN dart H ==> (face_map HH POWER n) ((f:A -> B) x) =
3022 f ((face_map H POWER n) (x)) ` ASSUME_TAC;
3023 ONCE_REWRITE_TAC[EQ_SYM_EQ];
3025 REWRITE_RULE[TAUT` a ==> b ==> c <=> a /\ b ==> c `] Hypermap_iso.power_comm);
3026 ASM_SIMP_TAC[Hypermap.lemma_dart_invariant];
3029 ASM_SIMP_TAC[IN_IMAGE; IN_ELIM_THM];
3036 let COMM_BIJ_HAS_SAME_ORDS = prove_by_refinement(`BIJ f (:A) (:B) /\
3037 (! x. (f o h) x = (g o (f: A -> B)) x )
3039 ==> has_orders g k`,
3040 [REWRITE_TAC[has_orders];
3042 FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` i: num `));
3045 REWRITE_TAC[FUN_EQ_THM];
3047 UNDISCH_TAC` BIJ f (:A) (:B) `;
3048 REWRITE_TAC[BIJ; INJ];
3050 FIRST_ASSUM MATCH_MP_TAC;
3051 REWRITE_TAC[IN_UNIV];
3052 UNDISCH_TAC` !x. (f o h) x = (g o (f:A -> B)) x `;
3057 ASM_REWRITE_TAC[I_THM];
3063 SIMP_TAC[FUN_EQ_THM];
3064 UNDISCH_TAC` BIJ f (:A) (:B) `;
3065 REWRITE_TAC[BIJ; INJ; SURJ];
3068 SUBGOAL_THEN` x IN (:B) ` MP_TAC;
3069 REWRITE_TAC[IN_UNIV];
3070 FIRST_X_ASSUM NHANH;
3073 UNDISCH_TAC` !x n. f (ITER n h x) = ITER n g ((f: A -> B) x) `;
3074 ONCE_REWRITE_TAC[EQ_SYM_EQ];
3077 ASM_REWRITE_TAC[I_THM]]);;
3084 let DIH2K_HYP_ISO_LEMMA = prove_by_refinement
3085 (` BIJ f (:A) (:B) /\
3086 FINITE (dart (H: (A) hypermap) ) /\ dih2k H k /\ hyp_iso (f: A -> B) (H, HH)
3088 [NHANH IMAGE_FACE_F;
3089 REWRITE_TAC[dih2k; hyp_iso];
3092 SUBGOAL_THEN` CARD (dart (H: (A) hypermap )) = CARD (dart (HH:(B) hypermap)) ` MP_TAC;
3093 MATCH_MP_TAC (Local_lemmas.BIJ_IMP_CARD_EQ);
3102 UNDISCH_TAC` BIJ (f: A -> B) (dart H) (dart HH) `;
3103 NHANH Add_triangle.BIJ_IMAGE;
3104 REWRITE_TAC[BIJ; SURJ];
3106 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` x: B `));
3107 DOWN THEN STRIP_TAC;
3110 SUBGOAL_THEN` (let S = face (H: (A) hypermap) y in dart H = S UNION IMAGE (node_map H) S) ` MP_TAC;
3111 FIRST_ASSUM MATCH_MP_TAC;
3115 SUBGOAL_THEN` IMAGE f (face H (y:A)) = face HH ((f: A -> B) (y:A)) ` MP_TAC;
3116 FIRST_ASSUM MATCH_MP_TAC;
3117 FIRST_X_ASSUM ACCEPT_TAC;
3120 DISCH_THEN (ASSUME_TAC o SYM);
3121 ASM_REWRITE_TAC[GSYM IMAGE_o];
3122 UNDISCH_TAC` (y:A) IN dart H ` ;
3123 NHANH Hypermap.lemma_face_subset;
3126 SUBGOAL_THEN` IMAGE (node_map HH o (f: A -> B)) S' = IMAGE (f o (node_map H )) S' ` ASSUME_TAC;
3127 MATCH_MP_TAC Lvducxu.IDE_ON_S_IMP_SAME_IMAGE;
3129 ASM_SIMP_TAC[SUBSET];
3131 ASM_SIMP_TAC[o_THM];
3134 REWRITE_TAC[IMAGE_o; GSYM IMAGE_UNION];
3137 SUBGOAL_THEN`!x. (x:A) IN dart H <=> ((f x): B) IN dart HH ` ASSUME_TAC;
3138 UNDISCH_TAC` BIJ (f: A -> B) (dart H ) (dart HH ) ` ;
3139 UNDISCH_TAC ` BIJ f (:A) (:B) ` ;
3140 REWRITE_TAC[BIJ; INJ; SURJ];
3141 STRIP_TAC THEN STRIP_TAC;
3142 GEN_TAC THEN EQ_TAC;
3144 FIRST_X_ASSUM NHANH;
3146 FIRST_X_ASSUM (MP_TAC o (SPECL [` y: A `;` x: A `]));
3147 FIRST_X_ASSUM (MP_TAC o (SPECL [` y: A `;` x: A `]));
3149 ASM_REWRITE_TAC[IN_UNIV];
3151 DISCH_THEN SUBST_ALL_TAC;
3152 FIRST_ASSUM ACCEPT_TAC;
3155 MATCH_MP_TAC (GEN_ALL COMM_BIJ_HAS_SAME_ORDS);
3156 EXISTS_TAC` f: A -> B `;
3157 EXISTS_TAC` face_map (H: (A) hypermap)`;
3160 ASM_CASES_TAC` (x:A) IN dart H `;
3161 ASM_SIMP_TAC[o_THM];
3164 NHANH Lvducxu.NOT_IN_DART_IMP_IDE;
3166 NHANH Lvducxu.NOT_IN_DART_IMP_IDE;
3170 MATCH_MP_TAC (GEN_ALL COMM_BIJ_HAS_SAME_ORDS);
3171 EXISTS_TAC` f: A -> B `;
3172 EXISTS_TAC` edge_map (H: (A) hypermap)`;
3176 ASM_CASES_TAC` (x:A) IN dart H `;
3177 ASM_SIMP_TAC[o_THM];
3180 NHANH Lvducxu.NOT_IN_DART_IMP_IDE;
3182 NHANH Lvducxu.NOT_IN_DART_IMP_IDE;
3185 MATCH_MP_TAC (GEN_ALL COMM_BIJ_HAS_SAME_ORDS);
3186 EXISTS_TAC` f: A -> B `;
3187 EXISTS_TAC` node_map (H: (A) hypermap)`;
3191 ASM_CASES_TAC` (x:A) IN dart H `;
3192 ASM_SIMP_TAC[o_THM];
3195 NHANH Lvducxu.NOT_IN_DART_IMP_IDE;
3197 NHANH Lvducxu.NOT_IN_DART_IMP_IDE;
3205 let AUTOMAP_IMP_ALL_ITER_IN2 =
3206 MESON[IN; Trigonometry2.AUTOMAP_IMP_ALL_ITER_IN] `
3207 p IN W /\ (!x. x IN W ==> f x IN W) ==> ITER N f p IN W `;;
3210 let ITER_COMM_RESTRICTED = prove_by_refinement(` (!(x:A). x IN V ==> f x IN V') /\
3211 (!x. h x IN V <=> x IN V) /\
3212 (!(y:B). g y IN V' <=> y IN V') /\
3213 (!x. x IN V ==> f (h x) = g (f x))
3214 ==> ! x. x IN V ==> f (ITER n h x) = ITER n g ( f x ) `,
3217 SPEC_TAC (`n:num `,`n:num `);
3221 GEN_TAC THEN STRIP_TAC;
3223 SUBGOAL_THEN` ITER n h (x:A) IN V ` ASSUME_TAC;
3224 MATCH_MP_TAC AUTOMAP_IMP_ALL_ITER_IN2;
3226 FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` x:A `));
3227 FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` ITER n h (x:A) `));
3228 ASM_REWRITE_TAC[]]);;
3232 let HAS_THE_SAME_ORD_LEM = prove_by_refinement(` (! x. ~( x IN V ) ==> h x = x ) /\
3233 (! y. ~( y IN V') ==> g y = y ) /\
3234 BIJ (f: A -> B) V V' /\
3235 (! x. (h x IN V) <=> x IN V ) /\
3236 (! y. (g y IN V') <=> y IN V' ) /\
3237 (!x. x IN V ==> (f (h x )) = (g (f x ))) /\ has_orders h k
3238 ==> has_orders g k `,
3239 [REWRITE_TAC[BIJ; INJ; SURJ; has_orders];
3241 FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` i:num `));
3244 REWRITE_TAC[FUN_EQ_THM];
3246 ASM_CASES_TAC` (x:A) IN V `;
3247 UNDISCH_TAC` !x y. x IN V /\ y IN V /\ (f: A -> B) x = f y ==> x = y ` ;
3248 DISCH_THEN MATCH_MP_TAC;
3249 ASM_REWRITE_TAC[I_THM];
3251 MATCH_MP_TAC AUTOMAP_IMP_ALL_ITER_IN2;
3253 MP_TAC (SPEC `i:num ` (GEN `n:num ` ITER_COMM_RESTRICTED));
3256 DISCH_THEN (ASSUME_TAC2 o (SPEC` x: A `));
3257 ASM_REWRITE_TAC[I_THM];
3260 MATCH_MP_TAC ITER_FIXPOINT;
3264 REWRITE_TAC[FUN_EQ_THM; I_THM];
3266 ASM_CASES_TAC` x IN (V': B -> bool) `;
3270 UNDISCH_TAC` !x. x IN V' ==> (?y. y IN V /\ (f: A -> B) y = x) `;
3274 MP_TAC (let tt = GEN` n: num ` ITER_COMM_RESTRICTED in SPEC` k: num ` tt);
3277 DISCH_THEN (ASSUME_TAC2 o (SPEC` y: A `));
3279 ASM_REWRITE_TAC[I_THM];
3281 MATCH_MP_TAC ITER_FIXPOINT;
3287 let COMM_THEN_IMAGE_IMAGE_EQ =
3288 SET_RULE ` (! x. x IN S ==> f ( g x ) = h ( f x )) /\ A SUBSET S
3289 ==> IMAGE f ( IMAGE g A ) = IMAGE h ( IMAGE f A ) `;;
3292 let IN_DART_PRESERVED = prove(` (!x: A. face_map H x IN dart H <=> x IN dart H) /\
3293 (!x: A. node_map H x IN dart H <=> x IN dart H) /\
3294 (!x: A. edge_map H x IN dart H <=> x IN dart H)`,
3295 MESON_TAC [Hypermap_iso.h_map_outside; Hypermap.lemma_dart_invariant]);;
3298 let HYP_ISO_DIH2K_PRESERVED = prove_by_refinement
3299 (`FINITE (dart H) /\ dih2k H k /\ hyp_iso (f: A -> B) (H,HH)
3301 [NHANH Hypermap_iso.iso_components;
3302 REWRITE_TAC[dih2k; hyp_iso];
3306 let tt = GEN_ALL Local_lemmas.BIJ_IMP_CARD_EQ in
3307 ISPECL [` f: A -> B `;` dart (H: (A) hypermap) `;` dart (HH: (B) hypermap) `] tt);
3312 GEN_TAC THEN STRIP_TAC;
3314 UNDISCH_TAC ` BIJ (f: A -> B) ( dart H ) ( dart HH ) `;
3315 REWRITE_TAC[BIJ; SURJ];
3320 SUBGOAL_THEN` (let S = face H (y:A) in dart H = S UNION IMAGE (node_map H) S) ` MP_TAC;
3321 FIRST_ASSUM MATCH_MP_TAC;
3322 FIRST_ASSUM ACCEPT_TAC;
3324 SUBGOAL_THEN` node HH (f y) = IMAGE f (node H y) /\
3325 face HH (f y) = IMAGE f (face H y) /\
3326 edge HH ((f: A -> B) y) = IMAGE f (edge H y) ` MP_TAC;
3327 FIRST_ASSUM MATCH_MP_TAC;
3328 FIRST_ASSUM ACCEPT_TAC;
3333 SUBGOAL_THEN` IMAGE (f: A -> B) (IMAGE (node_map H) S') = IMAGE (node_map HH) (IMAGE f S') ` ASSUME_TAC;
3334 MATCH_MP_TAC (GEN_ALL COMM_THEN_IMAGE_IMAGE_EQ);
3335 EXISTS_TAC` dart (H: (A) hypermap ) `;
3336 UNDISCH_TAC` !x. x IN dart H
3337 ==> edge_map HH ((f: A -> B) x) = f (edge_map H x) /\
3338 node_map HH (f x) = f (node_map H x) /\
3339 face_map HH (f x) = f (face_map H x) `;
3343 MATCH_MP_TAC Hypermap.lemma_face_subset;
3345 FIRST_X_ASSUM (SUBST1_TAC o SYM);
3346 REWRITE_TAC[GSYM IMAGE_UNION];
3347 SUBGOAL_THEN` BIJ (f: A -> B) (dart H ) (dart HH ) ` MP_TAC;
3348 ASM_REWRITE_TAC[BIJ; SURJ];
3349 NHANH Add_triangle.BIJ_IMAGE;
3353 ASSUME_TAC Hypermap_iso.h_map_outside;
3356 MATCH_MP_TAC (GEN_ALL HAS_THE_SAME_ORD_LEM);
3357 EXISTS_TAC` dart (HH: (B) hypermap) `;
3358 EXISTS_TAC` dart (H: (A) hypermap) `;
3359 EXISTS_TAC` f: A -> B `;
3360 EXISTS_TAC` face_map (H: (A) hypermap ) `;
3362 DOWN THEN SIMP_TAC[];
3366 ISPECL [` HH: (B) hypermap `;` y:B `] Hypermap_iso.h_map_outside);
3367 SIMP_TAC[IN_DART_PRESERVED];
3372 MATCH_MP_TAC (GEN_ALL HAS_THE_SAME_ORD_LEM);
3373 EXISTS_TAC` dart (HH: (B) hypermap) `;
3374 EXISTS_TAC` dart (H: (A) hypermap) `;
3375 EXISTS_TAC` f: A -> B `;
3376 EXISTS_TAC` edge_map (H: (A) hypermap ) `;
3378 DOWN THEN SIMP_TAC[];
3382 ISPECL [` HH: (B) hypermap `;` y:B `] Hypermap_iso.h_map_outside);
3383 SIMP_TAC[IN_DART_PRESERVED];
3386 MATCH_MP_TAC (GEN_ALL HAS_THE_SAME_ORD_LEM);
3387 EXISTS_TAC` dart (HH: (B) hypermap) `;
3388 EXISTS_TAC` dart (H: (A) hypermap) `;
3389 EXISTS_TAC` f: A -> B `;
3390 EXISTS_TAC` node_map (H: (A) hypermap ) `;
3392 DOWN THEN SIMP_TAC[];
3396 ISPECL [` HH: (B) hypermap `;` y:B `] Hypermap_iso.h_map_outside);
3397 SIMP_TAC[IN_DART_PRESERVED];
3404 let CONT_ATREAL_INJ_PRESERVED = prove_by_refinement(
3405 ` FINITE V /\ (!v. v IN V ==> (ff: real^N -> real -> real^M) v continuous atreal r) /\
3406 INJ (\v. ff v r ) V (IMAGE (\v. ff v r ) V )
3407 ==> ? e. &0 < e /\ (! t. abs ( t - r) < e ==>
3408 INJ (\v. ff v t ) V (IMAGE (\v. ff v t ) V )) `,
3411 MP_TAC (SPEC_ALL Local_lemmas1.CONTINUOUS_ATREAL_INJ_PRESERVED);
3419 EXISTS_TAC` d : real `;
3422 FIRST_X_ASSUM NHANH;
3423 REWRITE_TAC[IN_IMAGE];
3427 let INJ_BIJ_IMAGE = prove(` INJ f S S' /\ A SUBSET S ==> BIJ f A (IMAGE f A) `,
3428 REWRITE_TAC[BIJ; INJ; SURJ] THEN CONV_TAC SET_RULE);;
3434 let XRECQNS_UPDATE = prove_by_refinement(` deformation f V (a,b) /\ local_fan (V,E,FF)
3437 ==> local_fan (IMAGE (\v. f v t) V,
3438 IMAGE (\s. IMAGE (\v. f v t) s ) E ,
3439 IMAGE (\(u,v). (f u t, f v t )) FF) )) `,
3441 [NHANH_PAT `\x. x ==> y ` Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
3443 ASSUME_TAC2 Deformation.XRECQNS;
3445 REWRITE_TAC[REAL_BOUNDS_LT];
3448 REWRITE_TAC[deformation];
3450 UNDISCH_TAC` FAN (vec 0, V:real^3 -> bool, E ) `;
3451 REWRITE_TAC[FAN; fan1; fan2];
3453 SUBGOAL_THEN` FINITE V /\
3454 (!v. v IN V ==> (f: real^3 -> real -> real^3) v continuous atreal (&0)) /\
3455 INJ (\v. f v (&0)) V (IMAGE (\v. f v (&0)) V) ` MP_TAC;
3458 GEN_TAC THEN STRIP_TAC;
3459 FIRST_ASSUM (ASSUME_TAC2 o (SPECL [` v:real^3 `;` &0 `]));
3460 DOWN THEN SIMP_TAC[];
3461 UNDISCH_TAC` !v. v IN V ==> f v (&0) = v:real^3 `;
3462 REWRITE_TAC[INJ; IN_IMAGE];
3465 ISPECL [` f: real^3 -> real -> real^3 `;` &0 `] (
3466 GENL [` ff: real^N -> real -> real^M `;` r: real `] CONT_ATREAL_INJ_PRESERVED));
3468 DOWN THEN REWRITE_TAC[REAL_ARITH` a - &0 = a `];
3470 EXISTS_TAC ` min e e' `;
3471 ASM_REWRITE_TAC[REAL_LT_MIN];
3473 SUBGOAL_THEN` ! f s. INJ (f:real^3 -> real^3) s (IMAGE f s) <=> BIJ f s (IMAGE f s ) ` ASSUME_TAC;
3474 REWRITE_TAC[BIJ; SURJ; IN_IMAGE];
3479 GEN_TAC THEN STRIP_TAC;
3480 ABBREV_TAC` V' = IMAGE (\v. (f:real^3 -> real -> real^3) v t) V `;
3481 ABBREV_TAC` E' = IMAGE (\s. IMAGE (\v. (f: real^3 -> real -> real^3) v t) s) E `;
3482 ABBREV_TAC` ff = (\(x,y). (f:real^3 -> real -> real^3) x t, f y t) `;
3484 MP_TAC (SPEC` (\v. (f:real^3 -> real -> real^3) v t ) ` (
3485 GEN ` f: real^3 -> real^3 ` HYP_ISO_LEMMAA));
3488 SUBGOAL_THEN` FAN (vec 0,IMAGE (\v. (f: real^3 -> real -> real^3) v t) V,IMAGE (IMAGE (\v. f v t)) E) ` MP_TAC;
3489 FIRST_X_ASSUM MATCH_MP_TAC;
3496 SUBGOAL_THEN` FAN (vec 0,IMAGE (\v. (f: real^3 -> real -> real^3) v t) V,IMAGE (IMAGE (\v. f v t)) E) ` MP_TAC;
3497 FIRST_X_ASSUM MATCH_MP_TAC;
3499 DOWN THEN DOWN THEN DOWN;
3500 SIMP_TAC[ETA_AX; local_fan];
3505 UNDISCH_TAC` local_fan (V,E,FF) `;
3506 REWRITE_TAC[local_fan];
3509 UNDISCH_TAC` hyp_iso (ff: real^3 # real^3 -> real^3 # real^3) (H',H) `;
3513 EXISTS_TAC ` (ff: real^3 # real^3 -> real^3 # real^3) x `;
3515 REWRITE_TAC[hyp_iso; BIJ; INJ];
3519 let tt = GEN_ALL HYP_ISO_DIH2K_PRESERVED in
3520 ISPECL [` (ff: real^3 # real^3 -> real^3 # real^3 ) `;` H': (real^3 #real^3) hypermap `; ` H: (real^3 #real^3) hypermap `; ` k: num `] tt);
3523 ASSUME_TAC2 (ISPEC` vec 0: real^3 ` (
3524 GEN` x: real^N ` Wrgcvdr_cizmrrh.FAN_IMP_FIMITE_DARTS));
3525 UNDISCH_TAC` FAN (vec 0, V:real^3 -> bool , E ) `;
3526 NHANH Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP;
3529 FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` x: real^3 # real^3 `));
3530 FIRST_X_ASSUM (SUBST1_TAC o SYM);
3531 UNDISCH_TAC` (x: real^3 # real^3) IN dart H' `;
3532 NHANH Hypermap.lemma_face_subset;
3534 SUBGOAL_THEN` FINITE (face H' (x:real^3 # real^3 )) ` MP_TAC;
3535 REWRITE_TAC[Hypermap.FACE_FINITE];
3536 UNDISCH_TAC` hyp_iso (ff: real^3 # real^3 -> real^3 # real^3 ) (H', H) `;
3537 REWRITE_TAC[hyp_iso; BIJ];
3538 NHANH INJ_IMP_BIJ_IMAGE;
3542 UNDISCH_TAC` face H' (x: real^3 # real^3) SUBSET dart H' `;
3543 UNDISCH_TAC` INJ (ff: real^3 # real^3 -> real^3 # real^3 ) (dart H') (dart H) `;
3545 NHANH INJ_BIJ_IMAGE;
3548 UNDISCH_TAC` FINITE (face H' (x: real^3 # real^3)) `;
3550 NHANH Misc_defs_and_lemmas.BIJ_CARD;
3552 FIRST_X_ASSUM (SUBST1_TAC o SYM);
3553 UNDISCH_TAC` dih2k (H': (real^3 # real^3) hypermap) (CARD (FF: real^3 # real^3 -> bool)) `;
3554 ASM_REWRITE_TAC[]]);;
3561 let NORM_CROSS_LE = prove_by_refinement(` norm ( u cross v) <= norm u * norm v `,
3562 [MP_TAC (SPEC_ALL Trigonometry1.cross_mag);
3565 ONCE_REWRITE_TAC[REAL_ARITH` a <= b <=> &0 <= b - a `];
3566 REWRITE_TAC[REAL_ARITH` a * b - a * b * c = a * b * ( &1 - c ) `];
3569 ASM_MESON_TAC[REAL_LE_MUL; NORM_POS_LE]]);;
3575 let CONT_ATREAL_REAL_CONTS = prove_by_refinement (` f continuous atreal r
3576 ==> (\r. ((f r) cross y ) dot ( x cross y)) real_continuous atreal r `,
3577 [REWRITE_TAC[real_continuous_atreal; continuous_atreal];
3579 REWRITE_TAC[GSYM DOT_LSUB];
3580 REWRITE_TAC[VEC3_RULE` x cross y - z cross y = ( x - z) cross y `];
3581 ASM_CASES_TAC` (y:real^3) = vec 0 `;
3582 ASM_REWRITE_TAC[CROSS_RZERO; DOT_RZERO; REAL_ABS_0];
3583 EXISTS_TAC` e: real `;
3585 ASM_CASES_TAC` (x:real^3) = vec 0 `;
3586 ASM_REWRITE_TAC[CROSS_LZERO; DOT_RZERO; REAL_ABS_0];
3587 EXISTS_TAC` e:real `;
3589 FIRST_X_ASSUM (MP_TAC o (SPEC` e / (norm (x:real^3) * norm (y:real^3) * norm (y:real^3) ) `));
3591 MATCH_MP_TAC REAL_LT_DIV;
3593 MATCH_MP_TAC REAL_LT_MUL;
3594 ASM_REWRITE_TAC[NORM_POS_LT];
3595 MATCH_MP_TAC REAL_LT_MUL;
3596 ASM_REWRITE_TAC[NORM_POS_LT];
3598 EXISTS_TAC` d:real `;
3599 FIRST_X_ASSUM NHANH;
3603 MP_TAC (ISPECL [` ( f (x': real) - f r ) cross y `;` x cross y `] NORM_CAUCHY_SCHWARZ_ABS);
3604 ASSUME_TAC (SPECL [` (f:real -> real^3) x' - f r `;` y: real^3 `] (GEN_ALL NORM_CROSS_LE));
3605 MATCH_MP_TAC (REAL_ARITH` b < c ==> a <= b ==> a < c `);
3607 SUBGOAL_THEN` norm ((f (x':real) - f r) cross y) * norm (x cross y) <= (norm ( f x' - f r) * norm y ) * norm (x cross y ) ` ASSUME_TAC;
3608 MATCH_MP_TAC REAL_LE_RMUL;
3609 ASM_REWRITE_TAC[NORM_POS_LE];
3612 MATCH_MP_TAC (REAL_ARITH` b < c ==> a <= b ==> a < c `);
3615 SPECL [` x:real^3 `;` y: real^3 `] (GEN_ALL NORM_CROSS_LE));
3617 SUBGOAL_THEN` &0 <= norm ((f: real -> real^3) x' - f r) * norm (y:real^3) ` ASSUME_TAC;
3618 MATCH_MP_TAC REAL_LE_MUL;
3619 REWRITE_TAC[NORM_POS_LE];
3620 UNDISCH_TAC` norm (x cross y) <= norm x * norm y `;
3622 NHANH Real_ext.REAL_LE_RMUL_IMP;
3626 ONCE_REWRITE_TAC[REAL_MUL_SYM];
3628 MATCH_MP_TAC (REAL_ARITH` b < c ==> a <= b ==> a < c `);
3629 SUBGOAL_THEN ` &0 < norm (x:real^3) /\ &0 < norm (y:real^3) ` MP_TAC;
3630 ASM_REWRITE_TAC[NORM_POS_LT];
3632 ONCE_REWRITE_TAC[REAL_ARITH` (x * y ) * a * y = a * x * y * y `];
3633 SUBGOAL_THEN` &0 < norm (x:real^3) * norm y * norm (y:real^3) ` MP_TAC;
3635 MESON_TAC[REAL_LT_MUL];
3636 UNDISCH_TAC` norm ((f:real -> real^3) x' - f r) < e / (norm (x:real^3) * norm y * norm (y:real^3)) `;
3639 STRIP_TAC THEN DOWN;
3640 ASM_SIMP_TAC[REAL_FIELD` &0 < a ==> e / a * a = e `]]);;
3649 let CONTINUOUS_POS_PRES = prove_by_refinement (
3650 ` ~ collinear {(x:real^3),y, vec 0} /\ f r = a % x + b % y /\ &0 < a /\
3651 f continuous atreal r
3652 ==> ? e. &0 < e /\ ! t. abs t < e ==> ! t1 t2. f ( r + t ) = t1 % x + t2 % y ==> &0 < t1 `,
3653 [NHANH CONT_ATREAL_REAL_CONTS;
3654 REWRITE_TAC[real_continuous_atreal];
3656 FIRST_ASSUM (MP_TAC o (SPEC` a * norm ( x cross y ) * norm ( x cross y ) `));
3658 MATCH_MP_TAC REAL_LT_MUL;
3660 MATCH_MP_TAC REAL_LT_MUL;
3661 REWRITE_TAC[TAUT` a /\ a <=> a `];
3662 REWRITE_TAC[NORM_POS_LT; CROSS_EQ_0];
3663 UNDISCH_TAC` ~collinear {x, y:real^3, vec 0} `;
3664 SIMP_TAC[INSERT_COMM];
3666 EXISTS_TAC` d: real `; ASM_REWRITE_TAC[] ;
3669 FIRST_ASSUM (MP_TAC o (SPEC` r + (t:real) `));
3671 ASM_REWRITE_TAC[REAL_ARITH` (a + b) - a = b `];
3673 ASM_REWRITE_TAC[GSYM DOT_LSUB; VEC3_RULE` x cross z - y cross z = ( x - y) cross z `];
3674 REWRITE_TAC[VECTOR_ARITH` (t1 % x + t2 % y) - (a % x + b % y) = ( t1 - a ) % x + ( t2 - b ) % y `; CROSS_LADD; CROSS_LMUL; CROSS_REFL];
3675 REWRITE_TAC[VECTOR_ARITH` x + a % vec 0 = x `; DOT_LMUL; REAL_ABS_MUL; DOT_SQUARE_NORM];
3676 SUBGOAL_THEN` &0 <= norm (x cross y) pow 2 ` MP_TAC;
3677 REWRITE_TAC[REAL_LE_POW_2];
3679 REWRITE_TAC[GSYM REAL_ABS_REFL];
3680 SIMP_TAC[REAL_POW_2];
3682 REWRITE_TAC[REAL_ABS_REFL];
3683 REWRITE_TAC[REAL_ARITH` &0 <= a <=> a = &0 \/ &0 < a `];
3687 ASM_SIMP_TAC[REAL_LT_RMUL_EQ];
3688 UNDISCH_TAC` &0 < a `;
3695 let IVS_RHO_NODE_V_IN_FF = prove_by_refinement(` local_fan (V,E,FF) /\ v IN V ==> ivs_rho_node1 FF v, v IN FF `,
3696 [NHANH Local_lemmas.LOCAL_FAN_RHO_NODE_PROS2;
3698 FIRST_X_ASSUM (MP_TAC o (SPEC`ivs_rho_node1 FF v `));
3700 MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_IVS_IN_V;
3702 ASSUME_TAC2 Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS;
3703 ASM_REWRITE_TAC[]]);;
3709 let IN_AFF_GT_IMP_AZIMEQ = prove_by_refinement(
3710 ` x IN aff_gt {u,v} {y} ==> azim u v w x = azim u v w y `,
3712 ASM_CASES_TAC` collinear {u,v,w:real^3} `;
3713 ASM_SIMP_TAC[AZIM_DEGENERATE];
3714 ASM_CASES_TAC` collinear {u,v,y:real^3} `;
3715 ASM_SIMP_TAC[AZIM_DEGENERATE];
3720 ASM_SIMP_TAC[COLLINEAR_3_AFFINE_HULL];
3721 MP_TAC (ISPECL [` {u, v:real^3} `;` {y:real^3} `] AFF_GT_SUBSET_AFFINE_HULL);
3722 REWRITE_TAC[SUBSET];
3725 SUBGOAL_THEN` affine hull ({u, v:real^3} UNION {y}) = affine hull {u,v} ` ASSUME_TAC;
3726 MATCH_MP_TAC AFFINE_HULLS_EQ;
3727 REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {c,a,b} `];
3729 ONCE_REWRITE_TAC[INSERT_SUBSET];
3731 REWRITE_TAC[Qzksykg.SET_SUBSET_AFFINE_HULL];
3732 MP_TAC (SPEC` {u,v:real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL);
3733 MATCH_MP_TAC (SET_RULE` a SUBSET b ==> c SUBSET a ==> c SUBSET b `);
3734 MATCH_MP_TAC HULL_MONO;
3736 FIRST_X_ASSUM SUBST_ALL_TAC;
3738 ASM_SIMP_TAC[GSYM COLLINEAR_3_AFFINE_HULL; AZIM_DEGENERATE];
3740 REWRITE_TAC[AZIM_EQ_IMP]]);;
3745 let IN_AFF_GT_IMP_AZIMEQ2 =
3746 MESON[IN_AFF_GT_IMP_AZIMEQ]` x IN aff_gt {u, v} {y} ==>
3747 ! w. azim u v w x = azim u v w y `;;
3753 let NOT_COLL_IMP_ZERO_DETER = prove_by_refinement(` ~ collinear {vec 0, u, v } ==>
3754 (! a b. a % u + b % v = vec 0 <=> a = &0 /\ b = &0) `,
3755 [REWRITE_TAC[Local_lemmas1.COLL_EQ_DEPENDENT];
3757 GEN_TAC THEN GEN_TAC;
3761 SIMP_TAC[VECTOR_MUL_LZERO; VECTOR_ADD_LID]]);;
3765 let CROSS_IN_SAME_DIRECTION = prove_by_refinement (` local_fan (V,E,FF) /\
3767 {ITER n (rho_node1 FF) v | n <= l} = U /\
3771 v cross rho_node1 FF v = e
3774 ITER i (rho_node1 FF) v cross ITER ( i + 1) (rho_node1 FF ) v = k % e ) `,
3775 [NHANH Local_lemmas.RHO_NODE_SET_IN_A_PLANE_IMP_POS_DIRECT;
3776 ASM_CASES_TAC` l = 0 `;
3777 ASM_REWRITE_TAC[ARITH_RULE` ~( n < 0) `];
3779 SUBGOAL_THEN` {vec 0, v, rho_node1 FF v } SUBSET P ` ASSUME_TAC;
3780 ONCE_REWRITE_TAC[INSERT_SUBSET];
3782 MATCH_MP_TAC SUBSET_TRANS;
3783 EXISTS_TAC` U: real^3 -> bool `;
3785 REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];
3787 REWRITE_TAC[IN_ELIM_THM];
3790 REWRITE_TAC[ITER; ARITH_RULE` 0 <= l `];
3793 MATCH_MP_TAC (ARITH_RULE` ~( l = 0) ==> 1 <= l `);
3795 ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
3798 UNDISCH_TAC` plane (P: real^3 -> bool) `;
3800 NHANH Local_lemmas.THREE_NOT_COLL_DETER_PLANE;
3802 NHANH (ARITH_RULE` i < (l:num) ==> i <= l /\ i + 1 <= l `);
3803 GEN_TAC THEN STRIP_TAC;
3804 SUBGOAL_THEN` ITER i (rho_node1 FF) v IN U /\ ITER (i + 1) (rho_node1 FF) v IN U` ASSUME_TAC;
3806 REWRITE_TAC[IN_ELIM_THM];
3811 UNDISCH_TAC` U SUBSET (P: real^3 -> bool) `;
3812 REWRITE_TAC[SUBSET];
3815 REWRITE_TAC[IN_ELIM_THM; AFFINE_HULL_3];
3817 FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC ` i:num `));
3819 ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID; CROSS_LADD; CROSS_RADD];
3820 REWRITE_TAC[CROSS_LMUL; CROSS_RMUL; CROSS_REFL; VECTOR_MUL_LZERO; VECTOR_MUL_RZERO];
3821 REWRITE_TAC[VECTOR_ADD_LID; VECTOR_ADD_RID];
3822 ASM_REWRITE_TAC[VECTOR_MUL_ASSOC];
3823 ONCE_REWRITE_TAC[CROSS_SKEW];
3824 ASM_REWRITE_TAC[VECTOR_ARITH` (v' * w') % e + (w * v'') % --e = ((v' * w') - (w * v'')) % e `];
3825 REWRITE_TAC[DOT_LMUL];
3826 UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF v} `;
3827 ASM_REWRITE_TAC[GSYM CROSS_EQ_0];
3828 REWRITE_TAC[GSYM DOT_POS_LT];
3829 SIMP_TAC[REAL_LT_MUL_EQ];
3837 let ITER_CROSS_SAME_DIRECTION = prove_by_refinement
3838 (`local_fan (V,E,FF) /\
3840 {ITER n (rho_node1 FF) v | n <= l} = U /\
3844 ==> (!i j. i < l /\ j < l
3846 ITER i (rho_node1 FF) v cross ITER ( i + 1) (rho_node1 FF ) v =
3847 k % (ITER j (rho_node1 FF) v cross ITER ( j + 1) (rho_node1 FF ) v) ) `,
3849 ABBREV_TAC ` e = v cross rho_node1 FF v `;
3850 ASSUME_TAC2 CROSS_IN_SAME_DIRECTION;
3851 FIRST_X_ASSUM NHANH;
3854 EXISTS_TAC` k / (k': real) `;
3856 MATCH_MP_TAC REAL_LT_DIV;
3858 ASM_SIMP_TAC[REAL_FIELD` &0 < a ==> x / a * a = x `; VECTOR_MUL_ASSOC]]);;
3862 let ITER_IN_AFF_GT_2_1 = prove_by_refinement(` local_fan (V,E,FF) /\
3864 {ITER n (rho_node1 FF) v | n <= l} = U /\
3868 ==> (! i. i < l - 1 ==>
3869 ITER ( i + 2) (rho_node1 FF) v IN aff_lt {vec 0, ITER (i + 1) (rho_node1 FF) v } {ITER i (rho_node1 FF ) v } ) `,
3871 ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE3;
3873 FIRST_X_ASSUM (ASSUME_TAC o (SPEC` i:num `));
3875 SUBGOAL_THEN` {vec 0, ITER i (rho_node1 FF) v, ITER ( i + 1) (rho_node1 FF) v} SUBSET P` ASSUME_TAC;
3876 ONCE_REWRITE_TAC[INSERT_SUBSET];
3878 MATCH_MP_TAC SUBSET_TRANS;
3879 EXISTS_TAC` U: real^3 -> bool`;
3880 ASM_REWRITE_TAC[INSERT_SUBSET; EMPTY_SUBSET];
3882 REWRITE_TAC[IN_ELIM_THM];
3884 EXISTS_TAC` i:num `;
3889 EXISTS_TAC` i + 1 `;
3893 UNDISCH_TAC` ~collinear
3894 {vec 0, ITER i (rho_node1 FF) v, ITER (i + 1) (rho_node1 FF) v} `;
3895 UNDISCH_TAC` {vec 0, ITER i (rho_node1 FF) v, ITER (i + 1) (rho_node1 FF) v} SUBSET
3897 UNDISCH_TAC` plane (P:real^3 -> bool) `;
3899 NHANH Local_lemmas.THREE_NOT_COLL_DETER_PLANE;
3901 SUBGOAL_THEN` ITER (i + 2) (rho_node1 FF) v IN U ` MP_TAC;
3903 REWRITE_TAC[IN_ELIM_THM];
3904 EXISTS_TAC` i + 2 `;
3906 UNDISCH_TAC` i < l - 1 `;
3908 UNDISCH_TAC` (U:real^3 -> bool) SUBSET P `;
3909 REWRITE_TAC[SUBSET];
3913 REWRITE_TAC[IN_ELIM_THM; AFFINE_HULL_3];
3915 MP_TAC ITER_CROSS_SAME_DIRECTION;
3917 ASM_REWRITE_TAC[SUBSET];
3918 DISCH_THEN (MP_TAC o (SPECL [` i + 1`;` i:num `]));
3919 ASSUME_TAC2 (ARITH_RULE` i < l - 1 ==> i + 1 < l `);
3920 ASSUME_TAC2 (ARITH_RULE` i < l - 1 ==> i < l `);
3923 ASM_REWRITE_TAC[ARITH_RULE` (a + 1) + 1 = a + 2 `; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
3924 REWRITE_TAC[CROSS_RADD; CROSS_RMUL; CROSS_REFL; VECTOR_MUL_RZERO; VECTOR_ADD_RID];
3927 ABBREV_TAC` e1 = ITER i (rho_node1 FF) v cross ITER (i + 1) (rho_node1 FF) v `;
3928 ONCE_REWRITE_TAC[CROSS_SKEW; VECTOR_ARITH` a % -- x = ( -- a ) % x `];
3930 SUBGOAL_THEN` ~( e1:real^3 = vec 0) ` MP_TAC;
3932 REWRITE_TAC[CROSS_EQ_0];
3934 SIMP_TAC[VECTOR_MUL_RCANCEL; VECTOR_ARITH` a % -- x = ( -- a ) % x `];
3935 STRIP_TAC THEN STRIP_TAC;
3938 UNDISCH_TAC` ~collinear
3939 {vec 0, ITER i (rho_node1 FF) v, ITER (i + 1) (rho_node1 FF) v} `;
3940 ONCE_REWRITE_TAC[Collect_geom.PER_SET2];
3943 SIMP_TAC[Collect_geom.PER_SET2];
3945 REWRITE_TAC[IN_ELIM_THM];
3946 EXISTS_TAC `u: real `;
3947 EXISTS_TAC` w: real `;
3948 EXISTS_TAC` v':real`;
3949 ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID];
3951 UNDISCH_TAC` --v' = (k: real) `;
3952 UNDISCH_TAC ` &0 < k `;
3955 UNDISCH_TAC` u + v' + w = &1 `;
3957 CONV_TAC VECTOR_ARITH]);;
3962 search[` v cross rho_node1 FF v `];;
3965 let AZIM_PI_ITER_LOCAL_FAN = prove_by_refinement
3966 (`local_fan (V,E,FF) /\
3968 {ITER n (rho_node1 FF) v | n <= l} = U /\
3973 ==> azim (vec 0) (ITER (i + 1) (rho_node1 FF ) v ) (ITER (i) (rho_node1 FF ) v ) (ITER (i + 2) (rho_node1 FF ) v ) = pi ) `,
3974 [NHANH ITER_IN_AFF_GT_2_1;
3977 FIRST_X_ASSUM NHANH;
3979 ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE3;
3980 FIRST_ASSUM (MP_TAC o (SPEC` i: num `));
3981 FIRST_ASSUM (MP_TAC o (SPEC` i + 1`));
3983 ONCE_REWRITE_TAC[Collect_geom.PER_SET2];
3986 REWRITE_TAC[ARITH_RULE` (a + 1) + 1 = a + 2 `];
3987 MESON_TAC[AZIM_EQ_PI_ALT]]);;
3992 let LOCAL_CONVEX_NOT_COLLINEAR = prove_by_refinement
3993 (`convex_local_fan (V,E,FF) /\ lunar (v,w) V E
3994 ==> (!u. u IN V /\ ~(u = v) /\ ~(u = w)
3995 ==> ~ collinear {vec 0, v, u}) `,
3996 [NHANH LUNAR_IMP_IN_TWO_HAFLS_PLANE;
3997 REWRITE_TAC[lunar; INSERT_SUBSET];
3998 NHANH Local_lemmas.CVX_LO_IMP_LO;
4000 ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE2;
4001 ASSUME_TAC2 Local_lemmas.LOFA_IMP_NOT_COLL_IVS;
4002 FIRST_X_ASSUM NHANH;
4005 MESON_TAC[Planarity.aff_gt_imp_not_collinear]]);;
4008 let LOCAL_CONVEX_NOT_COLLINEAR2 = prove(` convex_local_fan (V,E,FF) /\ lunar (v,w) V E
4009 ==> (!u. u IN V /\ ~(u = v) /\ ~(u = w) ==> ~collinear {vec 0, w, u})`,
4010 ONCE_REWRITE_TAC[Local_lemmas.LUNAR_COMM] THEN
4011 NHANH LOCAL_CONVEX_NOT_COLLINEAR THEN MESON_TAC[]);;
4015 let LOCAL_FAN_RHO_NODE_PROS2 = prove(` local_fan (V,E,FF)
4016 ==> (!x. x IN V ==> x,rho_node1 FF x IN FF) `, NHANH Local_lemmas.LOCAL_FAN_RHO_NODE_PROS THEN SIMP_TAC[]);;
4020 (* =============================
4021 -======================================
4022 ================================
4026 let MHAEYJN_CONVEX_LOCAL_FAN = prove_by_refinement (
4027 `!a b V E FF f v w u.
4028 convex_local_fan (V,E,FF) /\
4030 deformation f V (a,b) /\
4031 interior_angle1 (vec 0) FF v < pi /\
4035 (!u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = u') /\
4036 (!t. t IN real_interval (a,b) ==> f u t IN affine hull {vec 0, v, w, u})
4038 (!t. --e < t /\ t < e
4039 ==> convex_local_fan
4040 (IMAGE (\v. f v t) V,
4041 IMAGE (IMAGE (\v. f v t)) E,
4042 IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF)
4045 NHANH_PAT`\x. x ==> y ` Local_lemmas.CVX_LO_IMP_LO;
4046 NHANH_PAT`\x. x ==> y ` Local_lemmas.LOCAL_FAN_FINITE_V;
4047 NHANH Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN;
4048 REWRITE_TAC[FAN; UNIONS_SUBSET];
4050 MP_TAC SUB_LUNAR_DEFORM_LEMMA;
4053 UNDISCH_TAC` deformation f (V:real^3 -> bool) (a,b) `;
4054 REWRITE_TAC[deformation; real_interval; IN_ELIM_THM];
4056 REWRITE_TAC[REAL_BOUNDS_LT];
4058 ASSUME_TAC2 XRECQNS_UPDATE;
4059 ASSUME_TAC2 HKIRPEP_ALT;
4060 DOWN THEN DOWN THEN STRIP_TAC;
4063 SUBGOAL_THEN` ! x y. x IN V /\ y IN V /\ ~ collinear {vec 0, x, y} /\
4065 (f:real^3 -> real -> real^3) u (&0) = a % x + b % y /\ &0 < a ) ==>
4068 ==> (!t1 t2. f u (t) = t1 % x + t2 % y ==> &0 < t1))) ` ASSUME_TAC;
4070 SUBGOAL_THEN` deformation (f:real^3 -> real -> real^3) V (a,b) ` MP_TAC;
4072 REWRITE_TAC[deformation];
4074 REPEAT GEN_TAC THEN STRIP_TAC;
4075 FIRST_ASSUM (ASSUME_TAC2 o (SPECL [`u: real^3 `;` &0 `]));
4078 ONCE_REWRITE_TAC[MESON[REAL_ARITH` t = &0 + t `]` f u t = A <=> f u ( &0 + t ) = A `];
4079 MATCH_MP_TAC (GEN_ALL CONTINUOUS_POS_PRES);
4080 EXISTS_TAC` b': real `;
4081 EXISTS_TAC` a': real `;
4082 UNDISCH_TAC` ~ collinear {vec 0, x, y:real^3} `;
4083 ASM_REWRITE_TAC[INSERT_COMM];
4084 ABBREV_TAC` ss = { (x,y) | x IN V /\
4086 ~collinear {vec 0, x, y} /\
4087 (?a b. (f:real^3 -> real -> real^3) u (&0) = a % x + b % y /\ &0 < a) } ` ;
4088 SUBGOAL_THEN` ss SUBSET { (x,y) | x IN (V:real^3 -> bool) /\ y IN V} ` MP_TAC;
4092 SUBGOAL_THEN` FINITE {x,y | x IN (V:real^3 -> bool) /\ y IN V} ` ASSUME_TAC;
4093 MATCH_MP_TAC FINITE_PRODUCT;
4095 UNDISCH_TAC` ss SUBSET {x,y | x IN V /\ (y:real^3) IN V} `;
4096 UNDISCH_TAC` FINITE {x,y | x IN V /\ y:real^3 IN V} `;
4098 NHANH FINITE_SUBSET;
4101 SUBGOAL_THEN` (!x. (x:real^3 # real^3) IN ss ==>
4102 (?e. &0 < e /\ (!t. abs t < e
4103 ==> (!t1 t2. (f:real^3 -> real -> real^3) u t = t1 % (FST x) + t2 % (SND x) ==> &0 < t1))))` MP_TAC;
4105 REWRITE_TAC[IN_ELIM_THM];
4109 FIRST_X_ASSUM MATCH_MP_TAC;
4111 EXISTS_TAC` a': real `;
4112 EXISTS_TAC` b': real `;
4116 NHANH Deformation.MINIMIZE_OVER_MEMBERS;
4118 EXISTS_TAC` min b ( min (-- a) ( min e (min e' e''))) `;
4119 SUBGOAL_THEN` deformation f (V: real^3 -> bool) (a,b) ` MP_TAC;
4121 REWRITE_TAC[deformation; real_interval; IN_ELIM_THM];
4123 REWRITE_TAC[REAL_LT_MIN];
4125 ASM_REWRITE_TAC[REAL_ARITH` &0 < -- a <=> a < &0 `];
4127 REWRITE_TAC[convex_local_fan];
4128 GEN_TAC THEN STRIP_TAC;
4129 ABBREV_TAC` IV = IMAGE (\v. (f:real^3 -> real -> real^3) v t) V `;
4130 ABBREV_TAC` IE = IMAGE (IMAGE (\v. (f: real^3 -> real -> real^3) v t)) E`;
4131 ABBREV_TAC` IF = IMAGE (\uv. (f: real^3 -> real -> real^3) (FST uv) t,f (SND uv) t) FF `;
4132 SUBGOAL_THEN` local_fan (IV, IE , IF) ` MP_TAC;
4133 UNDISCH_TAC` !t. abs t < e'
4135 (IMAGE (\v. f v t) V,
4136 IMAGE (\s. IMAGE (\v. f v t) s) E,
4137 IMAGE (\(u,v). (f: real^3 -> real -> real^3) u t,f v t) FF) `;
4138 DISCH_THEN (ASSUME_TAC2 o SPEC_ALL);
4140 UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
4141 DISCH_THEN (ASSUME_TAC o SYM);
4142 ASM_REWRITE_TAC[ETA_AX];
4143 SUBGOAL_THEN`! (fg: real^3 -> real^3). (\(u:real^3,v:real^3). fg u,fg v) = (\uv. fg (FST uv),fg (SND uv)) ` ASSUME_TAC;
4144 REWRITE_TAC[FUN_EQ_THM; BETA_THM];
4145 GEN_TAC THEN GEN_TAC;
4146 PAT_ONCE_REWRITE_TAC`\x. f x = y ` [GSYM PAIR];
4147 PURE_ONCE_REWRITE_TAC[BETA_THM];
4148 ABBREV_TAC` x1 = FST (x:real^3 # real^3) `;
4149 ABBREV_TAC` x2 = SND (x:real^3 # real^3) `;
4150 REWRITE_TAC[BETA_THM];
4153 SIMP_TAC[] THEN STRIP_TAC;
4156 UNDISCH_TAC` local_fan (IV, IE, IF) `;
4157 PHA; PAT_ONCE_REWRITE_TAC`\x. y /\ x ==> z ` [GSYM PAIR];
4158 ABBREV_TAC` xx = FST (x:real^3 # real^3) `;
4159 NHANH Local_lemmas.LOCAL_FAN_IMP_IN_V;
4160 NHANH Local_lemmas.DETER_RHO_NODE;
4162 ONCE_REWRITE_TAC[GSYM PAIR];
4163 ABBREV_TAC` xy = SND (x:real^3 # real^3) `;
4164 UNDISCH_TAC` xx:real^3 IN IV `;
4165 UNDISCH_TAC` local_fan (IV,IE,IF) `;
4167 UNDISCH_TAC` rho_node1 IF xx = xy `;
4168 DISCH_THEN (ASSUME_TAC o SYM);
4172 NHANH Local_lemmas1.AZIM_IN_FAN_RHOND_IVS_RHOND;
4173 NHANH Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND;
4176 ASSUME_TAC2 LOCAL_FAN_FACE_FF;
4177 SUBGOAL_THEN` lunar (v:real^3,w) V E ` MP_TAC;
4178 FIRST_ASSUM ACCEPT_TAC;
4179 REWRITE_TAC[lunar; INSERT_SUBSET];
4181 ASSUME_TAC2 Localization.LOFA_IMP_LT_CARD_SET_V_ALT;
4182 ASSUME_TAC2 Local_lemmas.LOCAL_FAN_CHARACTER_OF_RHO_NODE;
4183 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` u: real^3 `));
4184 DOWN THEN STRIP_TAC;
4185 ASSUME_TAC2 (SPEC`u: real^3 ` Local_lemmas1.IVS_RHO_NODE_DIFF_ID);
4186 ASSUME_TAC2 Local_lemmas.LOCAL_FAN_IMP_NOT_SEMI_IDE;
4187 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` u: real^3 `));
4188 SUBGOAL_THEN`! v:real^3. v IN V ==> ivs_rho_node1 FF (rho_node1 FF v) = v ` ASSUME_TAC;
4191 MATCH_MP_TAC Local_lemmas.IVS_RHO_IDD;
4193 SUBGOAL_THEN`!v. v IN V ==> rho_node1 FF (ivs_rho_node1 FF v) = v ` MP_TAC;
4196 MATCH_MP_TAC Local_lemmas1.LOCAL_FAN_RHO_NODE_IVS;
4200 SUBGOAL_THEN` ! v. v: real^3 IN V ==> rho_node1 FF v IN V ` ASSUME_TAC;
4201 GEN_TAC THEN STRIP_TAC;
4202 MATCH_MP_TAC Local_lemmas.LOFA_IN_V_SO_DO_RHO_NODE_V;
4204 SUBGOAL_THEN` deformation f (V: real^3 -> bool) (a,b) ` MP_TAC;
4206 REWRITE_TAC[deformation];
4208 SUBGOAL_THEN` t IN real_interval (a,b) ` ASSUME_TAC;
4209 REWRITE_TAC[IN_ELIM_THM; real_interval];
4211 UNDISCH_TAC` abs t < b `;
4212 UNDISCH_TAC` abs t < -- a `;
4214 ASSUME_TAC2 Polar_fan.IVS_RHO_NODE1_IN_V;
4215 SUBGOAL_THEN` (f:real^3 -> real -> real^3) (rho_node1 FF u) t = rho_node1 FF u ` ASSUME_TAC;
4216 FIRST_ASSUM MATCH_MP_TAC;
4218 SUBGOAL_THEN` (f:real^3 -> real -> real^3) (rho_node1 FF (rho_node1 FF u)) t = rho_node1 FF (rho_node1 FF u )` ASSUME_TAC;
4219 FIRST_ASSUM MATCH_MP_TAC;
4221 SUBGOAL_THEN` (f:real^3 -> real -> real^3) (ivs_rho_node1 FF u) t = ivs_rho_node1 FF u ` ASSUME_TAC;
4222 FIRST_ASSUM MATCH_MP_TAC;
4225 ASSUME_TAC2 Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS;
4226 DOWN THEN DISCH_THEN (ASSUME_TAC o GSYM);
4227 UNDISCH_TAC` xx: real^3 IN IV `;
4229 REWRITE_TAC[IN_IMAGE];
4231 SUBGOAL_THEN` ! (v:real^3). v IN V ==> (f:real^3 -> real -> real^3) v t, f (rho_node1 FF v) t IN IF ` ASSUME_TAC;
4233 REWRITE_TAC[IN_IMAGE];
4235 REWRITE_TAC[IN_ELIM_THM];
4236 GEN_TAC THEN STRIP_TAC;
4237 EXISTS_TAC` v', rho_node1 FF v' `;
4238 UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
4239 DISCH_THEN (ASSUME_TAC o SYM);
4241 EXISTS_TAC` v': real^3 `;
4244 SUBGOAL_THEN` ! (v:real^3). v IN V ==> rho_node1 IF ((f:real^3 -> real ->
4245 real^3) v t ) = f ( rho_node1 FF v ) t ` ASSUME_TAC;
4246 GEN_TAC THEN STRIP_TAC;
4247 FIRST_X_ASSUM (ASSUME_TAC2 o (SPEC` v': real^3 `));
4249 UNDISCH_TAC` local_fan (IV, IE, IF) `;
4251 NHANH Local_lemmas.DETER_RHO_NODE;
4253 SUBGOAL_THEN` ! (v:real^3). v IN V ==> ivs_rho_node1 IF ((f:real^3 -> real ->
4254 real^3) v t ) = f ( ivs_rho_node1 FF v ) t ` ASSUME_TAC;
4255 GEN_TAC THEN STRIP_TAC;
4256 SUBGOAL_THEN` f (ivs_rho_node1 FF v') t, (f:real^3 -> real -> real^3) v' t IN IF ` ASSUME_TAC;
4257 FIRST_X_ASSUM (MP_TAC o (SPEC` ivs_rho_node1 FF v' `));
4258 FIRST_X_ASSUM (MP_TAC o (SPEC` ivs_rho_node1 FF v' `));
4263 UNDISCH_TAC` local_fan (IV, IE, IF) `;
4265 NHANH Local_lemmas.IVS_RHO_NODE1_DETE;
4267 SUBGOAL_THEN` IV SUBSET (f:real^3 -> real -> real^3) u t INSERT V ` ASSUME_TAC;
4268 REWRITE_TAC[SUBSET];
4270 REWRITE_TAC[IN_IMAGE];
4271 GEN_TAC THEN STRIP_TAC;
4272 ASM_CASES_TAC` x''' = (u: real^3) `;
4273 ASM_REWRITE_TAC[IN_INSERT];
4274 ASM_SIMP_TAC[IN_INSERT];
4276 UNDISCH_TAC` x': real^3 IN V `;
4278 SUBGOAL_THEN` (f:real^3 -> real -> real^3) (ivs_rho_node1 FF (ivs_rho_node1 FF u)) t = ivs_rho_node1 FF (ivs_rho_node1 FF u) ` ASSUME_TAC;
4279 FIRST_ASSUM MATCH_MP_TAC;
4284 UNDISCH_TAC` !v. v IN V ==> ~(rho_node1 FF (rho_node1 FF v) = v) `;
4285 DISCH_THEN (MP_TAC o (SPEC` ivs_rho_node1 FF (ivs_rho_node1 FF u) `));
4290 SUBGOAL_THEN` convex_local_fan (V,E,FF) ` MP_TAC;
4291 FIRST_X_ASSUM ACCEPT_TAC;
4292 REWRITE_TAC[convex_local_fan];
4296 ASSUME_TAC2 LOCAL_FAN_RHO_NODE_PROS2;
4297 SUBGOAL_THEN` ! v. v IN V
4298 ==> wedge_in_fan_ge (v ,rho_node1 FF v) E =
4299 wedge_ge (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) ` ASSUME_TAC;
4302 MATCH_MP_TAC Local_lemmas1.WEDGE_IN_FAN_RHOND_IVS_RHOND;
4304 SUBGOAL_THEN` ! v. v IN V
4305 ==> azim_in_fan (v,rho_node1 FF v) E =
4306 azim (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) ` ASSUME_TAC;
4309 MATCH_MP_TAC Local_lemmas1.AZIM_IN_FAN_RHOND_IVS_RHOND;
4313 ASSUME_TAC2 Local_lemmas.LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI;
4315 NHANH IN_CONV0_IMP_AFF_EQ1;
4317 SUBGOAL_THEN` w IN aff {vec 0, v:real^3 } ` ASSUME_TAC;
4318 UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `;
4319 DISCH_THEN (ASSUME_TAC o SYM);
4321 MP_TAC (SPEC` {vec 0, w:real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL);
4322 REWRITE_TAC[SUBSET; Sphere.aff];
4323 DISCH_THEN MATCH_MP_TAC;
4324 REWRITE_TAC[IN_INSERT];
4327 SUBGOAL_THEN` ! v:real^3. v IN V ==> ~collinear {vec 0, v, ivs_rho_node1 FF v} ` ASSUME_TAC;
4328 UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `;
4329 DISCH_THEN (ASSUME_TAC o SYM);
4330 GEN_TAC THEN STRIP_TAC;
4331 MATCH_MP_TAC Local_lemmas.LOFA_IMP_NOT_COLL_IVS;
4335 ASSUME_TAC2 LUNAR_IMP_IN_TWO_HAFLS_PLANE;
4336 SUBGOAL_THEN` ! x. x IN V /\ ~( x = v ) /\ ~( x = w:real^3) ==>
4337 ~ collinear {vec 0, v, x} ` ASSUME_TAC;
4345 SUBGOAL_THEN` ~collinear {vec 0, v, ivs_rho_node1 FF v} /\
4346 ~collinear {vec 0, v, rho_node1 FF v} ` MP_TAC;
4348 MESON_TAC[Planarity.aff_gt_imp_not_collinear];
4356 SUBGOAL_THEN` ! x. x IN V /\ ~( x = v ) /\ ~( x = w:real^3) ==>
4357 rho_node1 FF x IN aff_ge {vec 0, v} {x} /\ ivs_rho_node1 FF x IN aff_ge {vec 0, v} {x} ` ASSUME_TAC;
4358 DOWN THEN DOWN THEN PHA THEN STRIP_TAC;
4362 SUBGOAL_THEN` x'': real^3 IN V ` MP_TAC;
4363 FIRST_ASSUM ACCEPT_TAC;
4365 REWRITE_TAC[IN_ELIM_THM];
4367 UNDISCH_TAC` ~collinear {vec 0, v, x'':real^3} `;
4371 MP_TAC (SET_RULE` {} SUBSET {x'':real^3}`);
4373 NHANH AFF_GE_MONO_RIGHT;
4374 REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL; GSYM aff];
4376 ASM_CASES_TAC` n = 0 `;
4377 UNDISCH_TAC` x'' = ITER n (rho_node1 FF) v `;
4378 UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `;
4379 DISCH_THEN (ASSUME_TAC o SYM);
4380 ASM_REWRITE_TAC[ITER];
4381 UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `;
4382 DISCH_THEN (ASSUME_TAC o SYM);
4383 UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `;
4384 DISCH_THEN (ASSUME_TAC o SYM);
4385 ASM_CASES_TAC` n = (i:num) `;
4386 UNDISCH_TAC` x'' = ITER n (rho_node1 FF) v `;
4388 ASSUME_TAC AFF_GT_SUBSET_AFF_GE;
4391 ASM_CASES_TAC` n < (i:num) `;
4392 SUBGOAL_THEN` x'' IN {ITER l (rho_node1 FF) v | 0 < l /\ l < i} ` MP_TAC;
4393 REWRITE_TAC[IN_ELIM_THM];
4394 EXISTS_TAC` n: num` ;
4395 ASM_REWRITE_TAC[ARITH_RULE` 0 < n <=> ~( n = 0) `];
4397 ASM_REWRITE_TAC[IN_INTER];
4398 UNDISCH_TAC` x'' = ITER n (rho_node1 FF) v `;
4399 DISCH_THEN (ASSUME_TAC o SYM);
4402 SUBGOAL_THEN` ~ collinear {vec 0, v, rho_node1 FF v} ` MP_TAC;
4405 NHANH Local_lemmas1.DIJ_AFF_GE_PARTITION;
4407 UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF v} `;
4409 NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
4410 ONCE_REWRITE_TAC[EQ_SYM_EQ];
4413 SUBGOAL_THEN` ~ collinear {vec 0, v, x'': real^3} ` MP_TAC;
4416 NHANH Local_lemmas1.DIJ_AFF_GE_PARTITION;
4421 UNDISCH_TAC` aff {vec 0, v} = aff {vec 0, w: real^3} `;
4422 DISCH_THEN (ASSUME_TAC o SYM);
4425 ASM_CASES_TAC` n = (i - 1) `;
4427 REWRITE_TAC[GSYM ITER];
4428 ASM_SIMP_TAC[ARITH_RULE` ~( i = 0) ==> SUC ( i - 1) = i `; IN_UNION];
4429 SUBGOAL_THEN` rho_node1 FF x'' IN {ITER l (rho_node1 FF) v | 0 < l /\ l < i} ` MP_TAC;
4430 REWRITE_TAC[IN_ELIM_THM];
4431 EXISTS_TAC` SUC n `;
4433 REWRITE_TAC[GSYM ITER];
4434 REWRITE_TAC[ARITH_RULE` 0 < SUC n `];
4435 MATCH_MP_TAC (ARITH_RULE` n < i /\ ~( n = i - 1) ==> SUC n < i `);
4437 ASM_REWRITE_TAC[IN_UNION; IN_INTER];
4439 ASM_CASES_TAC` n = 1`;
4448 MESON_TAC[HULL_SUBSET; IN_INSERT; SUBSET];
4450 SUBGOAL_THEN` ivs_rho_node1 FF x'' IN {ITER l (rho_node1 FF) v | 0 < l /\ l < i} ` MP_TAC;
4451 REWRITE_TAC[IN_ELIM_THM];
4452 EXISTS_TAC` n - 1 `;
4454 ASSUME_TAC2 (ARITH_RULE`~( n = 0) ==> SUC ( n - 1) = n `);
4457 SUBGOAL_THEN` ITER (n - 1) (rho_node1 FF) v IN V ` ASSUME_TAC;
4458 ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER;
4462 UNDISCH_TAC` ~( n = 0) `;
4463 UNDISCH_TAC` ~( n = 1) `;
4464 UNDISCH_TAC` n < (i:num) `;
4466 ASM_REWRITE_TAC[IN_INTER; IN_UNION];
4469 ASSUME_TAC2 (ARITH_RULE` ~( n < (i:num) ) ==> (n - i) + i = n `);
4470 SUBGOAL_THEN` x'' IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} ` MP_TAC;
4471 REWRITE_TAC[IN_ELIM_THM];
4472 EXISTS_TAC` n - (i:num) `;
4475 REWRITE_TAC[GSYM ITER_ADD];
4478 UNDISCH_TAC` ~( n = (i:num)) `;
4479 UNDISCH_TAC` ~( n < (i:num)) `;
4481 ASM_SIMP_TAC[ARITH_RULE` ~( n < (i:num)) ==> ( n - i < j <=> n < i + j )`];
4483 UNDISCH_TAC` x'' = ITER n (rho_node1 FF) v `;
4484 DISCH_THEN (ASSUME_TAC o SYM);
4485 ASM_REWRITE_TAC[IN_INTER];
4487 SUBGOAL_THEN` ~ collinear {vec 0, v, ivs_rho_node1 FF v}` MP_TAC;
4490 NHANH Local_lemmas.COLL_IN_AFF_GT_AFF_GT_EQ;
4491 ONCE_REWRITE_TAC[EQ_SYM_EQ];
4493 SUBGOAL_THEN` ~ collinear {vec 0, v, x'':real^3} ` MP_TAC;
4496 NHANH Local_lemmas1.DIJ_AFF_GE_PARTITION;
4501 ASM_CASES_TAC` n = (i + j) - 1 `;
4503 REWRITE_TAC[GSYM ITER];
4505 ASSUME_TAC2 (ARITH_RULE` n < CARD (V:real^3 -> bool) ==> SUC (CARD V - 1) = CARD V `);
4507 ASSUME_TAC2 Local_lemmas.LOFA_IMP_ITER_RHO_NODE_ID;
4508 FIRST_ASSUM (ASSUME_TAC2 o SPEC_ALL);
4509 ASM_REWRITE_TAC[IN_UNION];
4510 UNDISCH_TAC` aff {vec 0, v:real^3} = aff {vec 0, w} `;
4511 DISCH_THEN (SUBST1_TAC o SYM);
4513 MESON_TAC[HULL_SUBSET; IN_INSERT; SUBSET];
4516 SUBGOAL_THEN` rho_node1 FF x'' IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} ` MP_TAC;
4517 REWRITE_TAC[IN_ELIM_THM];
4519 REWRITE_TAC[GSYM ITER];
4520 ASM_SIMP_TAC[ARITH_RULE` ~( n < i ) ==> SUC n = SUC ( n - i ) + i `];
4521 REWRITE_TAC[GSYM ITER_ADD];
4523 EXISTS_TAC ` SUC ( n - i ) `;
4525 UNDISCH_TAC` n < CARD (V:real^3 -> bool) `;
4526 UNDISCH_TAC` i + j = CARD (V: real^3 -> bool) `;
4527 DISCH_THEN (ASSUME_TAC o SYM);
4529 UNDISCH_TAC` ~( n < (i:num)) `;
4530 UNDISCH_TAC` ~ ( n = ( i + j ) - 1) `;
4532 ASM_REWRITE_TAC[IN_INTER; IN_UNION];
4535 ASM_CASES_TAC` n = i + 1 `;
4536 REWRITE_TAC[IN_UNION];
4538 FIRST_ASSUM SUBST1_TAC;
4539 REWRITE_TAC[GSYM ADD1; ITER];
4541 MESON_TAC[HULL_SUBSET; SUBSET; IN_INSERT];
4544 SUBGOAL_THEN` ivs_rho_node1 FF x'' IN {ITER l (rho_node1 FF) w | 0 < l /\ l < j} ` ASSUME_TAC;
4545 REWRITE_TAC[IN_ELIM_THM];
4547 ASSUME_TAC2 (ARITH_RULE` ~( n < (i:num) ) /\ ~(n = i + 1) /\ ~( n = i ) ==> SUC ( n - 1 - i ) + i = n `);
4549 REWRITE_TAC[GSYM ITER_ADD; ITER];
4551 SUBGOAL_THEN` ITER (n - 1 - i) (rho_node1 FF) w IN V ` ASSUME_TAC;
4553 ASSUME_TAC2 Local_lemmas.LOCAL_FAN_ORBIT_MAP_VITER;
4554 FIRST_X_ASSUM MATCH_MP_TAC;
4559 EXISTS_TAC` n - 1 - i `;
4562 UNDISCH_TAC` ~(n = i + 1) `;
4563 UNDISCH_TAC` ~( n < (i:num) ) `;
4564 UNDISCH_TAC` ~( n = (i:num)) `;
4566 UNDISCH_TAC` n < CARD (V:real^3 -> bool) `;
4567 UNDISCH_TAC` i + j = CARD (V:real^3 -> bool) `;
4568 DISCH_THEN (ASSUME_TAC o SYM);
4570 UNDISCH_TAC` ~( n < i:num ) `;
4571 UNDISCH_TAC` ~( n = i:num ) `;
4574 ASM_REWRITE_TAC[IN_INTER; IN_UNION];
4577 SUBGOAL_THEN` ! u:real^3. affine hull {vec 0, v, w, u} = affine hull {vec 0, v, u} ` ASSUME_TAC;
4579 REWRITE_TAC[GSYM SUBSET_ANTISYM_EQ];
4581 MATCH_MP_TAC HULL_MINIMAL;
4582 REWRITE_TAC[AFFINE_AFFINE_HULL];
4583 MP_TAC (SPEC` {vec 0, v, u': real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL);
4584 SIMP_TAC[INSERT_SUBSET];
4586 SUBGOAL_THEN` affine hull {vec 0, v:real^3} SUBSET affine hull {vec 0, v, u'}` MP_TAC;
4587 MATCH_MP_TAC HULL_MONO;
4589 REWRITE_TAC[SUBSET];
4590 DISCH_THEN MATCH_MP_TAC;
4591 UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `;
4592 ASM_REWRITE_TAC[GSYM aff];
4593 DISCH_THEN (ASSUME_TAC o SYM);
4594 UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `;
4595 DISCH_THEN (ASSUME_TAC o SYM);
4597 UNDISCH_TAC` aff {vec 0, v} = aff { vec 0, w:real^3} `;
4598 DISCH_THEN (SUBST1_TAC o SYM);
4602 MATCH_MP_TAC HULL_MONO;
4607 SUBGOAL_THEN`! x'. x' IN V ==> (f:real^3 -> real -> real^3) u t IN
4608 wedge_ge (vec 0) (x') (rho_node1 FF x')
4609 (ivs_rho_node1 FF x') ` ASSUME_TAC;
4612 ASM_CASES_TAC` x'' = (v:real^3) `;
4613 UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `;
4614 DISCH_THEN (ASSUME_TAC o SYM);
4616 UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `;
4617 DISCH_THEN (ASSUME_TAC o SYM);
4618 ASM_REWRITE_TAC[wedge_ge; IN_ELIM_THM];
4619 FIRST_ASSUM (MP_TAC o (SPEC` v, rho_node1 FF v ` ));
4622 REWRITE_TAC[SUBSET];
4624 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` u: real^3 `));
4626 UNDISCH_TAC` !v. v IN V
4627 ==> wedge_in_fan_ge (v,rho_node1 FF v) E =
4628 wedge_ge (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) `;
4630 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 `));
4631 ASM_REWRITE_TAC[wedge_ge; IN_ELIM_THM];
4632 SUBGOAL_THEN` ~ collinear {vec 0, v , u:real^3 } ` MP_TAC;
4635 SUBGOAL_THEN` (!x. x IN (ss:real^3 # real^3 -> bool)
4636 ==> (!t1 t2. (f:real^3 -> real -> real^3) u t = t1 % FST x + t2 % SND x ==> &0 < t1)) ` ASSUME_TAC;
4637 FIRST_X_ASSUM MATCH_MP_TAC;
4639 FIRST_ASSUM (MP_TAC o (SPEC` (u:real^3, v:real^3) `));
4642 REWRITE_TAC[IN_ELIM_THM];
4643 EXISTS_TAC` u:real^3 `;
4644 EXISTS_TAC` v: real^3 `;
4646 UNDISCH_TAC` ~collinear {vec 0, v, u:real^3} `;
4647 SIMP_TAC[INSERT_COMM];
4654 CONV_TAC VECTOR_ARITH;
4658 SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u} ` MP_TAC;
4659 FIRST_ASSUM MATCH_MP_TAC;
4662 REWRITE_TAC[IN_ELIM_THM; AFFINE_HULL_3];
4665 REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID];
4666 ONCE_REWRITE_TAC[VECTOR_ADD_SYM];
4669 UNDISCH_TAC` ~collinear {vec 0, v, u:real^3} `;
4673 SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN aff_gt {vec 0, v} {u} ` ASSUME_TAC;
4674 ASM_REWRITE_TAC[IN_ELIM_THM];
4675 EXISTS_TAC` u': real `;
4676 EXISTS_TAC` v': real `;
4677 EXISTS_TAC` w': real`;
4679 CONV_TAC VECTOR_ARITH;
4681 NHANH IN_AFF_GT_IMP_AZIMEQ2;
4683 ASM_CASES_TAC` x'' = w:real^3 `;
4684 UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
4685 DISCH_THEN (ASSUME_TAC o SYM);
4686 UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
4687 DISCH_THEN (ASSUME_TAC o SYM);
4688 ASM_REWRITE_TAC[wedge_ge; IN_ELIM_THM];
4689 FIRST_ASSUM (MP_TAC o (SPEC` w, rho_node1 FF w `));
4693 UNDISCH_TAC` !v. v IN V
4694 ==> wedge_in_fan_ge (v,rho_node1 FF v) E =
4695 wedge_ge (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) `;
4697 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` w: real^3 `));
4701 REWRITE_TAC[SUBSET];
4703 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` u:real^3 `));
4705 REWRITE_TAC[wedge_ge; IN_ELIM_THM];
4706 SUBGOAL_THEN` ~collinear {vec 0, v, u:real^3} ` MP_TAC;
4708 ASM_REWRITE_TAC[Fan.collinear_fan];
4710 SUBGOAL_THEN` ~( w = vec 0: real^3) ` MP_TAC;
4711 ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
4713 ASSUME_TAC2 Local_lemmas.LOFA_IMP_V_DIFF;
4714 ONCE_REWRITE_TAC[EQ_SYM_EQ];
4715 UNDISCH_TAC` ~(u IN aff {vec 0, w: real^3}) `;
4717 REWRITE_TAC[GSYM Fan.collinear_fan];
4721 SUBGOAL_THEN` (!x. x IN ss
4722 ==> (!t1 t2. (f: real^3 -> real -> real^3) u t = t1 % FST x + t2 % SND x ==> &0 < t1)) ` MP_TAC;
4723 FIRST_X_ASSUM MATCH_MP_TAC;
4726 FIRST_ASSUM (MP_TAC o (SPEC` (u:real^3, w:real^3) `));
4729 REWRITE_TAC[IN_ELIM_THM];
4730 EXISTS_TAC` u:real^3 `;
4731 EXISTS_TAC` w:real^3 `;
4733 UNDISCH_TAC` ~collinear {vec 0, w, u: real^3} `;
4734 SIMP_TAC[INSERT_COMM];
4742 CONV_TAC VECTOR_ARITH;
4749 SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u }` ASSUME_TAC;
4750 FIRST_X_ASSUM MATCH_MP_TAC;
4752 SUBGOAL_THEN` affine hull {vec 0, v, w, u} SUBSET affine hull {vec 0, w, u:real^3} ` MP_TAC;
4753 MATCH_MP_TAC HULL_MINIMAL;
4754 REWRITE_TAC[AFFINE_AFFINE_HULL];
4755 MP_TAC (ISPEC` {vec 0, w, u: real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL);
4756 SIMP_TAC[INSERT_SUBSET];
4758 MP_TAC (SET_RULE` {vec 0, w:real^3} SUBSET {vec 0, w, u} `);
4759 NHANH (ISPEC` affine ` HULL_MONO);
4760 REWRITE_TAC[SUBSET];
4762 FIRST_X_ASSUM MATCH_MP_TAC;
4763 UNDISCH_TAC` aff {vec 0, v} = aff {vec 0, w:real^3} `;
4765 DISCH_THEN (SUBST1_TAC o SYM);
4768 MESON_TAC[HULL_SUBSET; IN_INSERT; SUBSET];
4769 REWRITE_TAC[SUBSET];
4771 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` (f:real^3 -> real -> real^3) u t `));
4773 REWRITE_TAC[IN_ELIM_THM; AFFINE_HULL_3; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
4775 FIRST_ASSUM (MP_TAC o (SPECL [` w': real `;` v': real `]));
4778 CONV_TAC VECTOR_ARITH;
4780 SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN aff_gt {vec 0, w} {u} ` MP_TAC;
4781 ASM_REWRITE_TAC[IN_ELIM_THM];
4782 EXISTS_TAC` u': real `;
4783 EXISTS_TAC` v': real `;
4784 EXISTS_TAC` w': real `;
4786 CONV_TAC VECTOR_ARITH;
4788 UNDISCH_TAC` &0 <= azim (vec 0) w (rho_node1 FF w) u `;
4789 UNDISCH_TAC` azim (vec 0) w (rho_node1 FF w) u <=
4790 azim (vec 0) w (rho_node1 FF w) (ivs_rho_node1 FF w) `;
4793 NHANH IN_AFF_GT_IMP_AZIMEQ2;
4795 SUBGOAL_THEN` interior_angle1 (vec 0) FF x'' = pi /\
4796 rho_node1 FF x'' IN aff {x'', v, w} /\
4797 ivs_rho_node1 FF x'' IN aff {x'', v, w} ` MP_TAC;
4798 FIRST_ASSUM MATCH_MP_TAC;
4799 REWRITE_TAC[IN_DIFF; IN_INSERT; NOT_IN_EMPTY];
4801 UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
4802 DISCH_THEN (ASSUME_TAC o SYM);
4803 UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
4804 DISCH_THEN (ASSUME_TAC o SYM);
4806 SUBGOAL_THEN` azim (vec 0) x'' (rho_node1 FF x'') (ivs_rho_node1 FF x'') =
4807 interior_angle1 (vec 0) FF x'' ` MP_TAC;
4809 DISCH_THEN (SUBST1_TAC o SYM);
4810 NHANH Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT;
4813 FIRST_ASSUM (MP_TAC o (SPEC` x'', rho_node1 FF x'' `));
4817 UNDISCH_TAC` !v. v IN V
4818 ==> wedge_in_fan_ge (v,rho_node1 FF v) E =
4819 wedge_ge (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) `;
4821 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` x'': real^3 `));
4822 ASM_REWRITE_TAC[VECTOR_ARITH` x - vec 0 = x `; SUBSET; IN_ELIM_THM];
4824 ABBREV_TAC` e1 = x'' cross rho_node1 FF x'' `;
4825 SUBGOAL_THEN` e1 dot v = &0 /\ e1 dot (w:real^3) = &0 ` MP_TAC;
4826 UNDISCH_TAC` vec 0 IN conv0 {v, w:real^3} `;
4827 REWRITE_TAC[Collect_geom.CONV0_SET2; IN_ELIM_THM];
4829 MP_TAC (ISPEC` e1: real^3 ` DOT_RZERO);
4830 ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL];
4831 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` v:real^3 `));
4832 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` w:real^3 `));
4834 UNDISCH_TAC` &0 < a' `;
4835 UNDISCH_TAC` &0 < b' `;
4836 REWRITE_TAC[REAL_ARITH` &0 <= a <=> a = &0 \/ &0 < a `];
4837 MESON_TAC[REAL_LT_ADD; REAL_LT_MUL; REAL_ARITH` &0 < a ==> ~(a = &0) `; REAL_ARITH` &0 < a ==> ~( a + x * &0 = &0 \/ x * &0 + a = &0) `];
4839 UNDISCH_TAC` !u. u IN V
4842 ==> u IN aff_gt {vec 0, v} {rho_node1 FF v} \/
4843 u IN aff_gt {vec 0, v} {ivs_rho_node1 FF v} `;
4845 FIRST_ASSUM (ASSUME_TAC2 o (SPEC` u:real^3 `));
4846 SUBGOAL_THEN` rho_node1 FF v IN V /\ ivs_rho_node1 FF v IN V ` MP_TAC;
4848 SUBGOAL_THEN` ~ collinear { vec 0, v, rho_node1 FF v } /\ ~ collinear {vec 0, v, ivs_rho_node1 FF v } ` MP_TAC;
4852 DOWN THEN STRIP_TAC;
4855 UNDISCH_TAC` u IN aff_gt {vec 0, v} {rho_node1 FF v} `;
4856 ASM_REWRITE_TAC[IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
4858 SUBGOAL_THEN` (!x. x IN ss
4859 ==> (!t1 t2. (f:real^3 -> real -> real^3) u t = t1 % FST x + t2 % SND x ==> &0 < t1)) ` MP_TAC;
4860 FIRST_X_ASSUM MATCH_MP_TAC;
4865 FIRST_X_ASSUM (MP_TAC o (SPEC` rho_node1 FF v, v `));
4868 REWRITE_TAC[IN_ELIM_THM];
4869 EXISTS_TAC` rho_node1 FF v `;
4870 EXISTS_TAC` v: real^3 `;
4872 UNDISCH_TAC` ~collinear {vec 0, v, rho_node1 FF v} `;
4873 SIMP_TAC[INSERT_COMM];
4875 UNDISCH_TAC` u = t2 % v + t3 % rho_node1 FF v `;
4876 DISCH_THEN (ASSUME_TAC o SYM);
4878 EXISTS_TAC` t3: real `;
4879 EXISTS_TAC` t2:real `;
4882 CONV_TAC VECTOR_ARITH;
4884 SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u } ` MP_TAC;
4886 FIRST_X_ASSUM (ASSUME_TAC o SYM);
4888 REWRITE_TAC[IN_ELIM_THM; AFFINE_HULL_3];
4890 REWRITE_TAC[VECTOR_ARITH` u % vec 0 + v % v' + w % (t2 % v' + t3 % ax) = ( v + w * t2 ) % v' + ( w * t3) % ax`];
4892 ONCE_REWRITE_TAC[VECTOR_ARITH` a + b = b + (a:real^N) `];
4894 UNDISCH_TAC` (f:real^3 -> real -> real^3) u t = (w' * t3) % rho_node1 FF v + (v' + w' * t2) % v `;
4895 ONCE_REWRITE_TAC[VECTOR_ARITH` a + b = b + (a:real^N) `];
4897 SIMP_TAC[DOT_RADD; DOT_RMUL];
4898 ASM_REWRITE_TAC[REAL_ARITH` a * &0 + x = x `];
4900 SUBGOAL_THEN` &0 <= e1 dot rho_node1 FF v ` ASSUME_TAC;
4901 FIRST_X_ASSUM MATCH_MP_TAC;
4903 MATCH_MP_TAC REAL_LE_MUL;
4905 UNDISCH_TAC` &0 < w' * t3 `;
4906 REAL_ARITH_TAC; STRIP_TAC;
4908 UNDISCH_TAC` u IN aff_gt {vec 0, v} {ivs_rho_node1 FF v} `;
4909 ASM_REWRITE_TAC[IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
4911 SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u} ` MP_TAC;
4912 FIRST_ASSUM MATCH_MP_TAC;
4914 ASM_REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM];
4915 REWRITE_TAC[VECTOR_ARITH` u % vec 0 + v % vv + w % (t2 % vv + t3 % vc) =
4916 ( v + w * t2 ) % vv + (w * t3 ) % vc `];
4917 FIRST_X_ASSUM (ASSUME_TAC o SYM);
4920 SUBGOAL_THEN` (!x. x IN ss
4921 ==> (!t1 t2. (f:real^3 -> real -> real^3) u t = t1 % FST x + t2 % SND x ==> &0 < t1)) ` ASSUME_TAC;
4922 FIRST_X_ASSUM MATCH_MP_TAC;
4924 FIRST_X_ASSUM (MP_TAC o (SPEC` ivs_rho_node1 FF v, v `));
4927 REWRITE_TAC[IN_ELIM_THM];
4928 EXISTS_TAC` ivs_rho_node1 FF v `;
4929 EXISTS_TAC` v: real^3 `;
4932 UNDISCH_TAC` ~collinear {vec 0, v, ivs_rho_node1 FF v} `;
4933 SIMP_TAC[INSERT_COMM];
4935 EXISTS_TAC` t3: real`;
4936 EXISTS_TAC` t2: real `;
4939 CONV_TAC VECTOR_ARITH;
4941 ONCE_REWRITE_TAC[VECTOR_ADD_SYM];
4942 DISCH_THEN (ASSUME_TAC2 o (SPECL [` w' * t3: real `; ` v' + w' * t2: real`]));
4943 ASM_REWRITE_TAC[DOT_RADD; DOT_RMUL; REAL_MUL_RZERO; REAL_ADD_LID];
4944 UNDISCH_TAC` !x. x IN V ==> &0 <= e1 dot (x: real^3) `;
4945 DISCH_THEN (ASSUME_TAC2 o (SPEC` ivs_rho_node1 FF v `));
4946 MATCH_MP_TAC REAL_LE_MUL;
4948 UNDISCH_TAC` &0 < w' * t3 `;
4949 CONV_TAC REAL_ARITH;
4950 ASM_CASES_TAC` ~( x' = (u:real^3)) /\ ~( rho_node1 FF x' = u ) /\ ~( ivs_rho_node1 FF x' = u ) ` ;
4951 DOWN THEN STRIP_TAC;
4952 UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `;
4953 DISCH_THEN (ASSUME_TAC o SYM);
4954 UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `;
4955 DISCH_THEN (ASSUME_TAC o SYM);
4958 UNDISCH_TAC` !x. (x:real^3 # real^3) IN FF ==> azim_in_fan x E <= pi /\ V SUBSET wedge_in_fan_ge x E `;
4959 DISCH_THEN (MP_TAC o (SPEC` x', rho_node1 FF x' `));
4964 MATCH_MP_TAC SUBSET_TRANS;
4965 EXISTS_TAC` (f:real^3 -> real -> real^3) u t INSERT V `;
4966 ASM_REWRITE_TAC[INSERT_SUBSET];
4970 ASM_CASES_TAC` x' = u:real^3 `;
4972 SUBGOAL_THEN` rho_node1 FF u IN aff_ge {vec 0, v} {u} /\
4973 ivs_rho_node1 FF u IN aff_ge {vec 0, v} {u} ` ASSUME_TAC;
4975 SUBGOAL_THEN` ~collinear {vec 0, v, u:real^3} ` ASSUME_TAC;
4977 SUBGOAL_THEN` (f: real^3 -> real -> real^3) (ivs_rho_node1 FF u) t IN IV ` ASSUME_TAC;
4979 REWRITE_TAC[IN_IMAGE];
4980 EXISTS_TAC` ivs_rho_node1 FF u `;
4982 ABBREV_TAC` UU = {ITER n (rho_node1 IF) ( (f: real^3 -> real -> real^3) (ivs_rho_node1 FF u) t ) | n <= 2} `;
4983 ABBREV_TAC` P = affine hull {vec 0, v, u:real^3} `;
4984 ASSUME_TAC (ISPECL [` {vec 0, v:real^3 }`;` {u:real^3} `] AFF_GE_SUBSET_AFFINE_HULL);
4985 SUBGOAL_THEN` plane (P:real^3 -> bool) ` ASSUME_TAC;
4987 EXISTS_TAC` vec 0: real^3 `;
4988 EXISTS_TAC` v: real^3 `;
4989 EXISTS_TAC` u: real^3 `;
4991 SUBGOAL_THEN` vec 0 IN (P:real^3 -> bool) ` ASSUME_TAC;
4993 prove(` {vec 0, v, u:real^3} SUBSET affine hull {vec 0, v, u} `,
4994 REWRITE_TAC[HULL_SUBSET]));
4995 UNDISCH_TAC` w = ITER i (rho_node1 FF ) v ` ;
4996 DISCH_THEN (ASSUME_TAC o SYM);
4997 UNDISCH_TAC` v = ITER j (rho_node1 FF ) w ` ;
4998 DISCH_THEN (ASSUME_TAC o SYM);
4999 ASM_REWRITE_TAC[SUBSET];
5000 DISCH_THEN MATCH_MP_TAC;
5001 REWRITE_TAC[IN_INSERT];
5002 SUBGOAL_THEN` UU SUBSET (P: real^3 -> bool) ` ASSUME_TAC;
5004 REWRITE_TAC[SUBSET; IN_ELIM_THM];
5006 REWRITE_TAC[ARITH_RULE` n <= 2 <=> n = 0 \/ n = 1 \/ n = 2 `];
5009 ASM_REWRITE_TAC[ITER];
5011 UNDISCH_TAC` aff_ge {vec 0, v:real^3} {u} SUBSET affine hull ({vec 0, v} UNION {u}) `;
5012 UNDISCH_TAC` w = ITER i (rho_node1 FF) v `;
5013 DISCH_THEN (ASSUME_TAC o SYM);
5014 UNDISCH_TAC` v = ITER j (rho_node1 FF) w `;
5015 DISCH_THEN (ASSUME_TAC o SYM);
5016 ASM_REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {a,b,c} `; SUBSET];
5017 DISCH_THEN MATCH_MP_TAC;
5022 SUBGOAL_THEN` rho_node1 IF ((f: real^3 -> real -> real^3) (ivs_rho_node1 FF u) t) = f (rho_node1 FF (ivs_rho_node1 FF u)) t` MP_TAC;
5023 FIRST_X_ASSUM MATCH_MP_TAC;
5029 SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u} ` MP_TAC;
5030 FIRST_X_ASSUM MATCH_MP_TAC;
5034 UNDISCH_TAC` x'' = ITER n (rho_node1 IF) ((f: real^3 -> real -> real^3) (ivs_rho_node1 FF u) t) ` ;
5035 DOWN THEN SIMP_TAC[];
5036 REWRITE_TAC[Lvducxu.ITER12];
5037 SUBGOAL_THEN` rho_node1 IF (f (ivs_rho_node1 FF u) (t:real)) = f (rho_node1 FF (ivs_rho_node1 FF u)) t ` MP_TAC;
5038 FIRST_X_ASSUM MATCH_MP_TAC;
5043 UNDISCH_TAC` aff_ge {vec 0, v} {u} SUBSET affine hull ({vec 0, v} UNION {u:real^3}) `;
5044 UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `;
5045 DISCH_THEN (ASSUME_TAC o SYM);
5046 UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `;
5047 DISCH_THEN (ASSUME_TAC o SYM);
5048 ASM_REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {a,b,c} `; SUBSET];
5049 DISCH_THEN MATCH_MP_TAC;
5052 SPECL [` IE: (real^3 -> bool) -> bool `;` IV: real^3 -> bool `;` UU: real^3 ->
5053 bool `;` P: real^3 -> bool `;` 2 `;` IF: real^3 # real^3 -> bool `; `((f:real
5054 ^3 -> real -> real^3) (ivs_rho_node1 FF u) t) `] (GEN_ALL
5055 AZIM_PI_ITER_LOCAL_FAN));
5056 FIRST_X_ASSUM (MP_TAC o (SPEC` 0 `));
5060 UNDISCH_TAC` w = ITER i (rho_node1 FF ) v `;
5061 UNDISCH_TAC` v = ITER j (rho_node1 FF ) w `;
5062 DISCH_THEN (ASSUME_TAC o SYM);
5063 DISCH_THEN (ASSUME_TAC o SYM);
5064 REWRITE_TAC[ADD; ITER; ITER1; Lvducxu.ITER12];
5065 SUBGOAL_THEN` rho_node1 IF (f (ivs_rho_node1 FF u) (t:real)) = f (rho_node1 FF (ivs_rho_node1 FF u)) t ` MP_TAC;
5069 NHANH (MESON[PI_POS]` x = pi ==> &0 < x `);
5070 NHANH Local_lemmas1.AZIM_POS_IMP_SUM_2PI;
5073 ASM_REWRITE_TAC[REAL_ARITH` a + x = &2 * a <=> x = a `];
5074 SIMP_TAC[REAL_LE_REFL];
5079 SUBGOAL_THEN` wedge_ge (vec 0) (f u (t:real)) (rho_node1 FF u) (ivs_rho_node1 FF u) =
5080 wedge_ge (vec 0) u (rho_node1 FF u) (ivs_rho_node1 FF u) ` ASSUME_TAC;
5082 SUBGOAL_THEN` interior_angle1 (vec 0) FF u = pi ` ASSUME_TAC;
5083 FIRST_X_ASSUM MATCH_MP_TAC;
5084 ASM_REWRITE_TAC[IN_DIFF; IN_INSERT; NOT_IN_EMPTY];
5085 SUBGOAL_THEN` azim (vec 0) u (rho_node1 FF u) (ivs_rho_node1 FF u) = pi ` MP_TAC;
5088 NHANH Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT;
5089 SIMP_TAC[VECTOR_SUB_RZERO];
5091 SUBGOAL_THEN` affine hull {vec 0, v, u} = affine hull {vec 0, u, rho_node1 FF u } ` ASSUME_TAC;
5092 MATCH_MP_TAC Local_lemmas.SUBSET_NOT_COLLINEAR_AFFINE_HULL_EQ ;
5093 ASM_SIMP_TAC[INSERT_SUBSET; EMPTY_SUBSET];
5096 MP_TAC (ISPECL [` affine: (real^3 -> bool) -> bool `;
5097 ` { vec 0, v, u:real^3} `] HULL_SUBSET);
5098 REWRITE_TAC[SUBSET];
5099 DISCH_THEN MATCH_MP_TAC;
5100 REWRITE_TAC[IN_INSERT];
5101 UNDISCH_TAC` aff_ge {vec 0, v} {u} SUBSET affine hull ({vec 0, v} UNION {u:real^3}) `;
5102 REWRITE_TAC[SUBSET;SET_RULE` {a,b} UNION {c} = {a,b,c} `];
5104 DISCH_THEN MATCH_MP_TAC;
5106 SUBGOAL_THEN` f u (t:real) IN affine hull {vec 0, v, w, u:real^3} ` MP_TAC;
5107 FIRST_ASSUM MATCH_MP_TAC;
5111 SIMP_TAC[IN_ELIM_THM; AFFINE_HULL_3];
5113 SUBGOAL_THEN` (!x. x IN ss
5114 ==> (!t1 t2. (f:real^3 -> real -> real^3) u t = t1 % FST x + t2 % SND x ==> &0 < t1)) ` ASSUME_TAC;
5115 FIRST_X_ASSUM MATCH_MP_TAC;
5117 FIRST_ASSUM (MP_TAC o (SPEC` u, rho_node1 FF u `));
5120 REWRITE_TAC[IN_ELIM_THM];
5121 EXISTS_TAC` u: real^3 `;
5122 EXISTS_TAC` rho_node1 FF u `;
5128 CONV_TAC VECTOR_ARITH;
5131 DISCH_THEN (MP_TAC o (SPECL [` v': real `;` w': real `]));
5134 CONV_TAC VECTOR_ARITH;
5135 ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID; CROSS_LADD; CROSS_LMUL; CROSS_REFL; VECTOR_ADD_RID; DOT_LMUL];
5136 SIMP_TAC[REAL_LE_MUL_EQ];
5140 FIRST_ASSUM (MP_TAC o (SPEC` u, rho_node1 FF u `));
5144 UNDISCH_TAC` !v. v IN V
5145 ==> wedge_in_fan_ge (v,rho_node1 FF v) E =
5146 wedge_ge (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) `;
5147 DISCH_THEN (ASSUME_TAC2 o (SPEC` u:real^3 `));
5152 MATCH_MP_TAC SUBSET_TRANS;
5153 EXISTS_TAC` (f:real^3 -> real -> real^3) u t INSERT V `;
5155 ASM_SIMP_TAC[INSERT_SUBSET];
5156 SUBGOAL_THEN` azim_in_fan (u, rho_node1 FF u) E <= pi /\ V SUBSET wedge_in_fan_ge (u, rho_node1 FF u) E ` ASSUME_TAC;
5157 FIRST_X_ASSUM MATCH_MP_TAC;
5159 DOWN THEN STRIP_TAC;
5161 UNDISCH_TAC` wedge_in_fan_ge (u,rho_node1 FF u) E =
5162 wedge_ge (vec 0) u (rho_node1 FF u) (ivs_rho_node1 FF u) `;
5165 SUBGOAL_THEN` (!x. (x :real^3 # real^3) IN ss
5166 ==> (!t1 t2. (f:real^3 -> real -> real^3) u t = t1 % FST x + t2 % SND x ==> &0 < t1)) ` ASSUME_TAC;
5167 FIRST_X_ASSUM MATCH_MP_TAC;
5170 UNDISCH_TAC` w = ITER i (rho_node1 FF ) v ` ;
5171 UNDISCH_TAC` v = ITER j (rho_node1 FF ) w ` ;
5172 DISCH_THEN (ASSUME_TAC o SYM);
5173 DISCH_THEN (ASSUME_TAC o SYM);
5174 ASM_CASES_TAC` rho_node1 FF x' = u `;
5176 SUBGOAL_THEN` ~(rho_node1 FF (rho_node1 FF ( ivs_rho_node1 FF x')) = (ivs_rho_node1 FF x')) ` MP_TAC;
5177 FIRST_ASSUM MATCH_MP_TAC;
5180 SUBGOAL_THEN` rho_node1 FF (ivs_rho_node1 FF x') = x' ` SUBST1_TAC;
5184 SUBGOAL_THEN` affine hull {vec 0, v, u} = affine hull {vec 0, u, ivs_rho_node1 FF u }` MP_TAC;
5185 MATCH_MP_TAC Local_lemmas.SUBSET_NOT_COLLINEAR_AFFINE_HULL_EQ;
5187 ASSUME_TAC2 (ISPECL [` {vec 0, v:real^3} `;` {u:real^3} `] AFF_GE_SUBSET_AFFINE_HULL);
5188 MP_TAC (ISPECL [` affine: (real^3 -> bool) -> bool `;` {vec 0, v, u:real^3} `] HULL_SUBSET);
5189 SIMP_TAC[INSERT_SUBSET];
5191 UNDISCH_TAC` aff_ge {vec 0, v} {u} SUBSET affine hull ({vec 0, v} UNION {u: real^3}) `;
5192 REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {a,b,c} `; SUBSET];
5193 DISCH_THEN MATCH_MP_TAC;
5196 SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u} ` MP_TAC;
5197 FIRST_X_ASSUM MATCH_MP_TAC;
5199 ASM_REWRITE_TAC[IN_ELIM_THM; AFFINE_HULL_3; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
5202 SUBGOAL_THEN` ~ collinear {vec 0, u, ivs_rho_node1 FF u } ` ASSUME_TAC;
5204 FIRST_ASSUM (MP_TAC o (SPEC` u, ivs_rho_node1 FF u ` ));
5207 REWRITE_TAC[IN_ELIM_THM];
5208 EXISTS_TAC` u:real^3 `;
5209 EXISTS_TAC` ivs_rho_node1 FF u `;
5215 CONV_TAC VECTOR_ARITH;
5218 DISCH_THEN (ASSUME_TAC2 o (SPECL [` v': real `;` w': real `]));
5220 ONCE_REWRITE_TAC[SET_RULE` {a,b} = {b,a} `];
5222 SUBGOAL_THEN` ivs_rho_node1 FF u = x' ` ASSUME_TAC;
5227 SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN aff_gt {vec 0, x'} {u:real^3} ` MP_TAC;
5231 SIMP_TAC[IN_ELIM_THM];
5234 EXISTS_TAC` u': real `;
5235 EXISTS_TAC` w': real `;
5236 EXISTS_TAC` v': real` ;
5239 UNDISCH_TAC` u' + v' + w' = &1 `;
5241 CONV_TAC VECTOR_ARITH;
5242 NHANH IN_AFF_GT_IMP_AZIMEQ2;
5243 REWRITE_TAC[GSYM Rogers.AZIM_EQ_SYM];
5246 UNDISCH_TAC` !x. x IN FF ==> azim_in_fan x E <= pi /\ V SUBSET wedge_in_fan_ge x E `;
5248 FIRST_ASSUM (MP_TAC o (SPEC` x', rho_node1 FF x' `));
5252 ASM_SIMP_TAC[GSYM wedge_ge];
5253 UNDISCH_TAC` !v. v IN V
5254 ==> azim (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) =
5255 interior_angle1 (vec 0) FF v `;
5256 DISCH_THEN (ASSUME_TAC o GSYM);
5260 MATCH_MP_TAC SUBSET_TRANS;
5261 EXISTS_TAC` (f:real^3 -> real -> real^3) u t INSERT V `;
5262 UNDISCH_TAC` (f: real^3 -> real -> real^3) u t = v' % u + w' % x' `;
5263 DISCH_THEN (ASSUME_TAC o SYM);
5265 UNDISCH_TAC` rho_node1 FF x' = u `;
5266 DISCH_THEN (ASSUME_TAC o SYM);
5267 ASM_SIMP_TAC[INSERT_SUBSET];
5268 SUBGOAL_THEN` (f: real^3 -> real -> real^3) u t IN
5269 wedge_ge (vec 0) x' (rho_node1 FF x') (ivs_rho_node1 FF x') ` MP_TAC;
5270 FIRST_X_ASSUM MATCH_MP_TAC;
5271 FIRST_ASSUM ACCEPT_TAC;
5275 ASM_CASES_TAC` ivs_rho_node1 FF x' = u `;
5277 SUBGOAL_THEN` x' = rho_node1 FF u ` ASSUME_TAC;
5278 FIRST_X_ASSUM (SUBST1_TAC o SYM);
5281 UNDISCH_TAC`!x. x IN FF ==> azim_in_fan x E <= pi /\ V SUBSET wedge_in_fan_ge x E `;
5282 DISCH_THEN (MP_TAC o (SPEC` x', rho_node1 FF x' `));
5286 UNDISCH_TAC` !v. v IN V
5287 ==> azim (vec 0) v (rho_node1 FF v) (ivs_rho_node1 FF v) =
5288 interior_angle1 (vec 0) FF v `;
5289 DISCH_THEN (ASSUME_TAC2 o (SPEC` x': real^3 `));
5290 FIRST_X_ASSUM (MP_TAC o SYM);
5294 FIRST_X_ASSUM (MP_TAC o (SPEC` u, rho_node1 FF u `));
5297 REWRITE_TAC[IN_ELIM_THM];
5298 EXISTS_TAC` u: real^3 `;
5299 EXISTS_TAC` rho_node1 FF u `;
5307 CONV_TAC VECTOR_ARITH;
5311 SUBGOAL_THEN` affine hull {vec 0, v, u} = affine hull {vec 0, u, rho_node1 FF u } ` ASSUME_TAC;
5312 MATCH_MP_TAC Local_lemmas.SUBSET_NOT_COLLINEAR_AFFINE_HULL_EQ;
5314 MP_TAC (ISPEC ` {vec 0, v, u:real^3} ` Qzksykg.SET_SUBSET_AFFINE_HULL);
5315 SIMP_TAC[INSERT_SUBSET];
5318 MP_TAC (ISPECL [` {vec 0, v:real^3} `;` {u: real^3} `] AFF_GE_SUBSET_AFFINE_HULL);
5319 REWRITE_TAC[SET_RULE` {a,b} UNION {c} = {a,b,c} `; SUBSET];
5320 DISCH_THEN MATCH_MP_TAC;
5322 SUBGOAL_THEN` (f:real^3 -> real -> real^3) u t IN affine hull {vec 0, v, w, u} ` MP_TAC;
5323 FIRST_X_ASSUM MATCH_MP_TAC;
5324 FIRST_ASSUM ACCEPT_TAC;
5325 ASM_REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM; VECTOR_MUL_RZERO; VECTOR_ADD_LID];
5327 SUBGOAL_THEN` &0 < v' ` ASSUME_TAC;
5328 FIRST_X_ASSUM MATCH_MP_TAC;
5329 EXISTS_TAC` w': real`;
5331 SUBGOAL_THEN` ~ collinear {vec 0, u, rho_node1 FF u } ` MP_TAC;
5333 ONCE_REWRITE_TAC[Collect_geom.PER_SET2];
5337 SUBGOAL_THEN` (f:real ^3 -> real -> real^3) u t IN aff_gt {vec 0, rho_node1 FF u } {u} ` MP_TAC;
5338 ASM_REWRITE_TAC[IN_ELIM_THM];
5339 EXISTS_TAC` u': real `;
5340 EXISTS_TAC` w': real `;
5341 EXISTS_TAC` v': real `;
5344 UNDISCH_TAC` u' + v' + w' = &1 `;
5346 CONV_TAC VECTOR_ARITH;
5347 NHANH IN_AFF_GT_IMP_AZIMEQ2;
5349 STRIP_TAC THEN STRIP_TAC;
5350 MATCH_MP_TAC SUBSET_TRANS;
5351 EXISTS_TAC` (f: real^3 -> real -> real^3) u t INSERT V `;
5352 UNDISCH_TAC` (f: real^3 -> real -> real^3) u t = v' % u + w' % rho_node1 FF u `;
5353 DISCH_THEN (ASSUME_TAC o SYM);
5355 ASM_REWRITE_TAC[INSERT_SUBSET; wedge_ge];
5356 ASM_SIMP_TAC[GSYM wedge_ge];
5357 UNDISCH_TAC` !x'. x' IN V
5358 ==> (f: real^3 -> real -> real^3) u t IN
5359 wedge_ge (vec 0) x' (rho_node1 FF x') (ivs_rho_node1 FF x') `;
5360 DISCH_THEN (MP_TAC o (SPEC` rho_node1 FF u `));
5364 UNDISCH_TAC` ~(~(x' = u) /\ ~(rho_node1 FF x' = u) /\ ~(ivs_rho_node1 FF x' = u)) `;
5365 ASM_REWRITE_TAC[]]);;
5367 let MHAEYJN = prove_by_refinement(
5368 `!a b V E FF f v w u.
5369 convex_local_fan (V,E,FF) /\
5371 deformation f V (a,b) /\
5372 interior_angle1 (vec 0) FF v < pi /\
5376 (!u' t. u' IN V /\ ~(u = u') /\ t IN real_interval (a,b) ==> f u' t = u') /\
5377 (!t. t IN real_interval (a,b) ==> f u t IN affine hull {vec 0, v, w, u})
5379 (!t. --e < t /\ t < e
5380 ==> convex_local_fan
5381 (IMAGE (\v. f v t) V,
5382 IMAGE (IMAGE (\v. f v t)) E,
5383 IMAGE (\uv. f (FST uv) t,f (SND uv) t) FF) /\
5384 lunar (v,w) (IMAGE (\v. f v t) V)
5385 (IMAGE (IMAGE (\v. f v t)) E)))`,
5388 REPEAT WEAKER_STRIP_TAC;
5389 INTRO_TAC (GEN_ALL SUB_LUNAR_DEFORM_LEMMA) [`FF`;`a`;`b`;`u`;`v`;`w`;`V`;`f`;`E`];
5392 RULE_ASSUM_TAC(REWRITE_RULE[Localization.deformation;IN_REAL_INTERVAL]);
5394 TYPIFY `local_fan (V,E,FF)` (C SUBGOAL_THEN ASSUME_TAC);
5395 BY(ASM_SIMP_TAC[Local_lemmas.CVX_LO_IMP_LO]);
5397 MATCH_MP_TAC Local_lemmas.LOCAL_FAN_FINITE_V;
5398 BY(ASM_REWRITE_TAC[]);
5399 RULE_ASSUM_TAC(REWRITE_RULE[Localization.local_fan;Fan.FAN;LET_DEF;LET_END_DEF]);
5400 FIRST_X_ASSUM MP_TAC THEN REPEAT WEAKER_STRIP_TAC;
5401 BY(FIRST_X_ASSUM MP_TAC THEN FIRST_X_ASSUM_ST `UNIONS` MP_TAC THEN SET_TAC[]);
5402 REPEAT WEAKER_STRIP_TAC;
5403 INTRO_TAC MHAEYJN_CONVEX_LOCAL_FAN [`a`;`b`;`V`;`E`;`FF`;`f`;`v`;`w`;`u`];
5405 REPEAT WEAKER_STRIP_TAC;
5406 TYPIFY `if e < e' then e else e'` EXISTS_TAC;
5407 REPEAT WEAKER_STRIP_TAC;
5409 BY(COND_CASES_TAC THEN ASM_REWRITE_TAC[]);
5410 REPEAT WEAKER_STRIP_TAC;
5412 FIRST_X_ASSUM MATCH_MP_TAC;
5413 BY(ASM_TAC THEN REAL_ARITH_TAC);
5414 FIRST_X_ASSUM MATCH_MP_TAC;
5415 BY(ASM_TAC THEN REAL_ARITH_TAC)