(* ========================================================================= *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Authour : VU KHAC KY *) (* Book lemma: SLTSTLO *) (* Chaper : Packing (Marchal Cells) *) (* Date : June - July 2011 *) (* *) (* ========================================================================= *) module Sltstlo = struct open Rogers;; open Vukhacky_tactics;; open Pack_defs;; open Pack_concl;; open Pack1;; open Sphere;; open Marchal_cells;; open Marchal_cells_2_new;; open Emnwuus;; let seans_fn () = let (tms,tm) = top_goal () in let vss = map frees (tm::tms) in let vs = setify (flat vss) in map dest_var vs;; let NULLSET_SPHERE = prove_by_refinement (`(!P. (?(v:real^3)(r:real). (r> &0)/\ (P={w:real^3 | norm (w-v)= r})) ==> NULLSET P)`, [ X_GEN_TAC `s:real^3->bool` THEN STRIP_TAC; FIRST_X_ASSUM(MP_TAC); STRIP_TAC THEN ASM_REWRITE_TAC[GSYM dist] ; ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[NEGLIGIBLE_SPHERE]; ]);; (* =========================================================================== *) let SLTSTLO1 = prove_by_refinement ( SLTSTLO1_concl, [(REPEAT GEN_TAC THEN REPEAT STRIP_TAC); (* =================== Case 1 ============================================== *) (ASM_CASES_TAC `hl (ul:(real^3)list) < sqrt(&2)`); (EXISTS_TAC `4`); (REWRITE_TAC[ARITH_RULE `4 <= 4`]); (* New subgoal *) (SUBGOAL_THEN `mcell4 V ul = convex hull (set_of_list (ul:(real^3)list))` ASSUME_TAC); (REWRITE_TAC[mcell4]); (COND_CASES_TAC); (REFL_TAC); (SUBGOAL_THEN `F` ASSUME_TAC); (UP_ASM_TAC THEN UP_ASM_TAC THEN MESON_TAC[]); (UP_ASM_TAC THEN MESON_TAC[]); (SUBGOAL_THEN `mcell 4 V ul = mcell4 V (ul:(real^3)list)` ASSUME_TAC); (REWRITE_TAC[mcell]); (COND_CASES_TAC); (SUBGOAL_THEN `F` ASSUME_TAC); (MESON_TAC[ASSUME `4 = 0`;ARITH_RULE `~(4 = 0)`]); (UP_ASM_TAC THEN MESON_TAC[]); (COND_CASES_TAC); (SUBGOAL_THEN `F` ASSUME_TAC); (MESON_TAC[ASSUME `4 = 1`;ARITH_RULE `~(4 = 1)`]); (UP_ASM_TAC THEN MESON_TAC[]); (COND_CASES_TAC); (SUBGOAL_THEN `F` ASSUME_TAC); (MESON_TAC[ASSUME `4 = 2`;ARITH_RULE `~(4 = 2)`]); (UP_ASM_TAC THEN MESON_TAC[]); (COND_CASES_TAC); (SUBGOAL_THEN `F` ASSUME_TAC); (MESON_TAC[ASSUME `4 = 3`;ARITH_RULE `~(4 = 3)`]); (UP_ASM_TAC THEN MESON_TAC[]); (REFL_TAC); (ASM_REWRITE_TAC[]); (DEL_TAC THEN DEL_TAC); (* New subgoal *) (SUBGOAL_THEN `convex hull set_of_list (ul:(real^3)list) = UNIONS {rogers V (left_action_list p ul) | p permutes 0..3}` ASSUME_TAC); (MATCH_MP_TAC WQPRRDY); (ASM_REWRITE_TAC[IN]); (* End subgoal *) (PURE_ASM_REWRITE_TAC[]); (REWRITE_TAC[IN_UNIONS]); (EXISTS_TAC `rogers V (ul:(real^3)list)`); (ASM_REWRITE_TAC[IN_ELIM_THM]); (EXISTS_TAC `I:(num->num)`); (STRIP_TAC); (MESON_TAC[PERMUTES_I]); (AP_TERM_TAC); (REWRITE_TAC[Packing3.LEFT_ACTION_LIST_I]); (* Finish case 1 *) (* =================== Case 2 ============================================== *) (NEW_GOAL `sqrt (&2) <= hl (ul:(real^3)list)`); (UP_ASM_TAC THEN REAL_ARITH_TAC); (SUBGOAL_THEN `? u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]` CHOOSE_TAC); (MP_TAC (ASSUME `barV V 3 ul`)); (REWRITE_TAC[BARV_3_EXPLICIT]); (FIRST_X_ASSUM CHOOSE_TAC); (FIRST_X_ASSUM CHOOSE_TAC); (FIRST_X_ASSUM CHOOSE_TAC); (ASM_CASES_TAC `dist(u0:real^3, p) >= sqrt(&2)`); (EXISTS_TAC `0`); (REWRITE_TAC[ARITH_RULE `0 <= 4`]); (SUBGOAL_THEN `mcell 0 V ul = mcell0 V (ul:(real^3)list)` ASSUME_TAC); (REWRITE_TAC[mcell]); (ONCE_ASM_REWRITE_TAC[]); (REWRITE_TAC[mcell0]); (REWRITE_TAC[DIFF; IN; IN_ELIM_THM]); STRIP_TAC; (ASM_MESON_TAC[IN]); (REWRITE_TAC[ball;IN_ELIM_THM]); (SUBGOAL_THEN `HD (ul:(real^3)list) = u0` ASSUME_TAC); (ASM_REWRITE_TAC[HD]); (ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (* Finish case 2 *) (* =================== Case 3 ============================================== *) (NEW_GOAL `dist (u0, p:real^3) < sqrt (&2)`); (UP_ASM_TAC THEN REAL_ARITH_TAC); (ASM_CASES_TAC `~(p IN rcone_gt (HD (ul:(real^3)list)) (HD (TL ul)) (hl (truncate_simplex 1 ul) / sqrt (&2))) `); (EXISTS_TAC `1`); (REWRITE_TAC[ARITH_RULE `1 <= 4`]); (SUBGOAL_THEN `mcell 1 V ul = mcell1 V (ul:(real^3)list)` ASSUME_TAC); (REWRITE_TAC[mcell]); (COND_CASES_TAC); (SUBGOAL_THEN `F` MP_TAC); (UP_ASM_TAC THEN ARITH_TAC); (MESON_TAC[]); (REFL_TAC); (ONCE_ASM_REWRITE_TAC[]); (REWRITE_TAC[mcell1]); (COND_CASES_TAC); (REWRITE_TAC[IN_DIFF]); (ASM_REWRITE_TAC[IN_INTER]); (REWRITE_WITH `HD [u0;u1;u2;u3] = u0:real^3`); (REWRITE_TAC[HD]); (REWRITE_TAC[cball;IN;IN_ELIM_THM]); (ASM_REAL_ARITH_TAC); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (UP_ASM_TAC THEN MESON_TAC[]); (* Finish case 3 *) (* =================== Case 4 ============================================== *) (NEW_GOAL `p IN rcone_gt (HD (ul:(real^3)list)) (HD (TL ul)) (hl (truncate_simplex 1 ul) / sqrt (&2))`); (UP_ASM_TAC THEN MESON_TAC[]); (SWITCH_TAC THEN DEL_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[HD;TL; TRUNCATE_SIMPLEX_EXPLICIT_1]); (STRIP_TAC); (ASM_CASES_TAC `p IN aff_ge {u0:real^3, u1} {mxi V ul, omega_list_n V ul 3}`); (EXISTS_TAC `2`); (REWRITE_TAC[ARITH_RULE `2 <= 4`]); (REWRITE_TAC[MCELL_EXPLICIT; mcell2]); (COND_CASES_TAC); (LET_TAC); (REWRITE_TAC[IN_INTER]); (ASM_REWRITE_TAC[HD;TL]); (REWRITE_TAC[GSYM (ASSUME `ul = [u0; u1; u2; u3:real^3]`)]); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (REPEAT STRIP_TAC); (MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET B) ==> p IN B`)); (EXISTS_TAC `rcone_gt (u0:real^3) u1 a`); (REWRITE_TAC[RCONE_GT_SUBSET_RCONE_GE]); (ASM_MESON_TAC[]); (MATCH_MP_TAC RCONEGE_INTER_VORONOI_CLOSED_IMP_RCONEGE); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (NEW_GOAL `voronoi_nondg V (ul:(real^3)list)`); (UNDISCH_TAC `barV V 3 (ul:(real^3)list)`); (REWRITE_TAC[BARV]); (STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[LENGTH; INITIAL_SUBLIST;ARITH_RULE `0 < 3 + 1`]); (EXISTS_TAC `[]:(real^3)list`); (REWRITE_TAC[APPEND]); (UP_ASM_TAC THEN REWRITE_TAC[VORONOI_NONDG]); (ASM_REWRITE_TAC[set_of_list]); (REPEAT STRIP_TAC); (* Break into 7 subgoals *) (* Subgoal 1 & subgoal 2 *) (ASM_SET_TAC[]); (ASM_SET_TAC[]); (NEW_GOAL `&0 < hl [u0; u1:real^3]`); (REWRITE_WITH `hl [u0;u1:real^3] = hl (truncate_simplex 1 (ul:(real^3)list))`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (MATCH_MP_TAC BARV_IMP_HL_1_POS_LT); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (NEW_GOAL `hl [u0;u1:real^3] = &0`); (ASM_REWRITE_TAC[HL;set_of_list;SET_RULE `{a, a} = {a}`]); (NEW_GOAL `radV {u1:real^3} = dist (circumcenter {u1},u1)`); (NEW_GOAL `(!w. w IN {u1:real^3} ==> radV {u1} = dist (circumcenter {u1},w))`); (MATCH_MP_TAC Rogers.OAPVION2); (REWRITE_TAC[AFFINE_INDEPENDENT_1]); (FIRST_X_ASSUM MATCH_MP_TAC); (SET_TAC[]); (ASM_REWRITE_TAC[Rogers.CIRCUMCENTER_1; dist]); (NORM_ARITH_TAC); (ASM_REAL_ARITH_TAC); (EXPAND_TAC "a"); (MATCH_MP_TAC REAL_LT_DIV); (STRIP_TAC); (REWRITE_WITH `hl [u0;u1:real^3] = hl (truncate_simplex 1 (ul:(real^3)list))`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (MATCH_MP_TAC BARV_IMP_HL_1_POS_LT); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC SQRT_POS_LT); (REAL_ARITH_TAC); (EXPAND_TAC "a"); (NEW_GOAL `hl [u0; u1:real^3] / sqrt (&2) <= &1 <=> hl [u0; u1] <= &1 * sqrt (&2)`); (MATCH_MP_TAC REAL_LE_LDIV_EQ); (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC); (ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET B) ==> p IN B`)); (EXISTS_TAC `rcone_gt (u0:real^3) u1 a`); (REWRITE_TAC[RCONE_GT_SUBSET_RCONE_GE]); (ASM_MESON_TAC[]); (REWRITE_WITH `p IN voronoi_closed V (u0:real^3) <=> (?vl. vl IN barV V 3 /\ p IN rogers V vl /\ truncate_simplex 0 vl = [u0])`); (MATCH_MP_TAC Rogers.GLTVHUM); (ASM_REWRITE_TAC[]); (ASM_SET_TAC[]); (EXISTS_TAC `ul:(real^3)list`); (ASM_REWRITE_TAC[IN; TRUNCATE_SIMPLEX_EXPLICIT_0]); (UP_ASM_TAC THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (REWRITE_TAC[MESON [] `~(a /\ b) <=> ~a \/ ~ b`]); (DISCH_TAC); (NEW_GOAL `~(hl [u0; u1:real^3] < sqrt (&2))`); (ASM_MESON_TAC[]); (NEW_GOAL `hl [u0; u1:real^3] >= sqrt (&2)`); (ASM_REAL_ARITH_TAC); (ABBREV_TAC `t = hl [u0; u1:real^3] / sqrt (&2)`); (NEW_GOAL `&1 <= t`); (EXPAND_TAC "t"); (NEW_GOAL `&1 <= hl [u0; u1:real^3] / sqrt (&2) <=> &1 * sqrt (&2) <= hl [u0; u1]`); (MATCH_MP_TAC REAL_LE_RDIV_EQ); (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC); (ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (UNDISCH_TAC `p IN rcone_gt (u0:real^3) u1 t`); (REWRITE_TAC[rcone_gt;rconesgn; IN; IN_ELIM_THM; dist]); (DISCH_TAC); (NEW_GOAL `F`); (NEW_GOAL `(p - u0) dot (u1 - u0) <= norm (p - u0) * norm (u1 - u0:real^3)`); (REWRITE_TAC[NORM_CAUCHY_SCHWARZ]); (NEW_GOAL `norm (p - u0) * norm (u1 - u0) * t >= norm (p - u0) * norm (u1 - u0:real^3) `); (REWRITE_TAC[REAL_ARITH `a * b * t >= a * b <=> &0 <= (t - &1) * (a * b)`]); (MATCH_MP_TAC REAL_LE_MUL); (STRIP_TAC); (ASM_REAL_ARITH_TAC); (MATCH_MP_TAC REAL_LE_MUL); (REWRITE_TAC[NORM_POS_LE]); (ASM_REAL_ARITH_TAC); (UP_ASM_TAC THEN MESON_TAC[]); (* Finish case 4 *) (* =================== Case 5 ============================================== *) (ASM_CASES_TAC `hl (truncate_simplex 2 (ul:(real^3)list)) >= sqrt (&2)`); (NEW_GOAL `mxi V (ul:(real^3)list) = omega_list_n V ul 2`); (REWRITE_TAC[mxi]); (COND_CASES_TAC); (REFL_TAC); (NEW_GOAL `F`); (ASM_REAL_ARITH_TAC); (UP_ASM_TAC THEN MESON_TAC[]); (NEW_GOAL `p IN aff_ge {u0, u1:real^3} {mxi V ul, omega_list_n V ul 3}`); (MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET B) ==> p IN B`)); (EXISTS_TAC `rogers V (ul:(real^3)list)`); STRIP_TAC; (ASM_REWRITE_TAC[]); (MATCH_MP_TAC (SET_RULE `(?s. p SUBSET s /\ s SUBSET B) ==> p SUBSET B`)); (EXISTS_TAC `convex hull ({u0, u1:real^3} UNION {mxi V ul, omega_list_n V ul 3})`); (STRIP_TAC); (NEW_GOAL `convex hull ({u0, u1:real^3} UNION {mxi V ul, omega_list_n V ul 3}) = convex hull (convex hull ({u0, u1} UNION {mxi V ul, omega_list_n V ul 3}))`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (REWRITE_TAC[CONVEX_HULL_EQ; CONVEX_CONVEX_HULL]); (ONCE_ASM_REWRITE_TAC[]); (REWRITE_TAC[ROGERS]); (MATCH_MP_TAC CONVEX_HULL_SUBSET); (ASM_REWRITE_TAC [LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) = 4` ; SET_OF_0_TO_3]); (REWRITE_TAC[IMAGE;SUBSET;IN;IN_ELIM_THM]); (REPEAT STRIP_TAC); (ASM_CASES_TAC `x' = 0`); (REWRITE_WITH `x = u0:real^3`); (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[OMEGA_LIST_N;HD]); (ONCE_REWRITE_TAC[GSYM IN]); (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET); (SET_TAC[]); (ASM_CASES_TAC `x' = 1`); (REWRITE_WITH `x = circumcenter {u0,u1:real^3}`); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC OMEGA_LIST_1_EXPLICIT_NEW); (EXISTS_TAC `u2:real^3`); (EXISTS_TAC `u3:real^3`); (ASM_REWRITE_TAC[IN]); (STRIP_TAC); (ASM_MESON_TAC[IN]); (ASM_CASES_TAC `hl [u0; u1:real^3] < sqrt (&2)`); (ASM_REWRITE_TAC[]); (NEW_GOAL `hl [u0; u1:real^3] >= sqrt (&2)`); (ASM_REAL_ARITH_TAC); (ABBREV_TAC `t = hl [u0; u1:real^3] / sqrt (&2)`); (NEW_GOAL `&1 <= t`); (EXPAND_TAC "t"); (NEW_GOAL `&1 <= hl [u0; u1:real^3] / sqrt (&2) <=> &1 * sqrt (&2) <= hl [u0; u1]`); (MATCH_MP_TAC REAL_LE_RDIV_EQ); (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC); (ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (UNDISCH_TAC `p IN rcone_gt (u0:real^3) u1 t`); (REWRITE_TAC[rcone_gt;rconesgn; IN; IN_ELIM_THM; dist]); (DISCH_TAC); (NEW_GOAL `F`); (NEW_GOAL `(p - u0) dot (u1 - u0) <= norm (p - u0) * norm (u1 - u0:real^3)`); (REWRITE_TAC[NORM_CAUCHY_SCHWARZ]); (NEW_GOAL `norm (p - u0) * norm (u1 - u0) * t >= norm (p - u0) * norm (u1 - u0:real^3) `); (REWRITE_TAC[REAL_ARITH `a * b * t >= a * b <=> &0 <= (t - &1) * (a * b)`]); (MATCH_MP_TAC REAL_LE_MUL); (STRIP_TAC); (ASM_REAL_ARITH_TAC); (MATCH_MP_TAC REAL_LE_MUL); (REWRITE_TAC[NORM_POS_LE]); (ASM_REAL_ARITH_TAC); (UP_ASM_TAC THEN MESON_TAC[]); (ONCE_REWRITE_TAC[GSYM IN]); (MATCH_MP_TAC (SET_RULE `(?s. p IN s /\ s SUBSET B) ==> p IN B`)); (EXISTS_TAC `convex hull ({u0, u1:real^3})`); (STRIP_TAC); (REWRITE_TAC[Rogers.CIRCUMCENTER_2; midpoint;CONVEX_HULL_2;IN;IN_ELIM_THM]); (EXISTS_TAC `&1 / (&2)`); (EXISTS_TAC `&1 / (&2)`); (ASM_SIMP_TAC[REAL_LE_DIV; REAL_ARITH `&0 <= &1 /\ &0 <= &2`]); (STRIP_TAC); (REAL_ARITH_TAC); (VECTOR_ARITH_TAC); (MATCH_MP_TAC CONVEX_HULL_SUBSET); (SET_TAC[]); (ASM_CASES_TAC `x' = 2`); (ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[GSYM IN]); (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET); (SET_TAC[]); (ASM_CASES_TAC `x' = 3`); (ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[GSYM IN]); (MATCH_MP_TAC IN_SET_IMP_IN_CONVEX_HULL_SET); (SET_TAC[]); (NEW_GOAL `F`); (UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN DEL_TAC); (UP_ASM_TAC THEN TRUONG_SET_TAC[]); (UP_ASM_TAC THEN MESON_TAC[]); (ASM_REWRITE_TAC[SET_RULE `{a, b} UNION {c , d} = {a, b, c,d}`]); (REWRITE_TAC[CONVEX_HULL_4_SUBSET_AFF_GE_2_2]); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (NEW_GOAL `hl (truncate_simplex 2 (ul:(real^3)list)) < sqrt (&2)`); (ASM_REAL_ARITH_TAC); (EXISTS_TAC `3`); (REWRITE_TAC[ARITH_RULE `3 <= 4`]); (REWRITE_TAC[MCELL_EXPLICIT; mcell3]); (COND_CASES_TAC); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]); (REWRITE_TAC[SET_RULE `{a, b ,c} UNION {d} = {a, b , c, d}`]); (NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\ dist (u0,s:real^3) = sqrt (&2) /\ mxi V ul = s)`); (MATCH_MP_TAC MXI_EXPLICIT_OLD); (ASM_MESON_TAC[]); (FIRST_X_ASSUM CHOOSE_TAC); (REWRITE_WITH `mxi V [u0; u1; u2; u3] = s:real^3`); (ASM_MESON_TAC[]); (* ========================================================================= *) (ABBREV_TAC `a = omega_list_n V ul 1`); (ABBREV_TAC `b = omega_list_n V ul 2`); (ABBREV_TAC `c = omega_list_n V ul 3`); (NEW_GOAL `p IN convex hull {u0, a, b, c:real^3}`); (EXPAND_TAC "a" THEN EXPAND_TAC "b" THEN EXPAND_TAC "c"); (REWRITE_WITH `u0:real^3 = HD ul`); (ASM_REWRITE_TAC[HD]); (REWRITE_WITH `convex hull {HD ul, omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3} = rogers V ul`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (MATCH_MP_TAC ROGERS_EXPLICIT); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (NEW_GOAL `a = midpoint (u0, u1:real^3)`); (REWRITE_TAC[GSYM Rogers.CIRCUMCENTER_2]); (EXPAND_TAC "a"); (REWRITE_WITH `{u0,u1} = set_of_list [u0;(u1:real^3)]`); (MESON_TAC[set_of_list]); (REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`; OMEGA_LIST_TRUNCATE_1]); (MATCH_MP_TAC XNHPWAB1); (EXISTS_TAC `1`); (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]); (MP_TAC (ASSUME `barV V 3 ul`) THEN REWRITE_TAC[IN;BARV]); (REPEAT STRIP_TAC); (REWRITE_TAC[LENGTH;ARITH_RULE `SUC (SUC 0) = 1 + 1`]); (NEW_GOAL `initial_sublist vl (ul:(real^3)list)`); (UNDISCH_TAC `initial_sublist vl [u0:real^3; u1]`); (REWRITE_TAC[INITIAL_SUBLIST] THEN STRIP_TAC); (EXISTS_TAC `APPEND yl [u2;u3:real^3]`); (REWRITE_TAC[APPEND_ASSOC; GSYM (ASSUME `[u0:real^3; u1] = APPEND vl yl`)]); (ASM_REWRITE_TAC[APPEND]); (ASM_MESON_TAC[]); (ABBREV_TAC `sl = truncate_simplex 2 (ul:(real^3)list)`); (MATCH_MP_TAC (REAL_ARITH `hl (sl:(real^3)list) < b /\ a < hl sl ==> a < b`)); (ASM_REWRITE_TAC[]); (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 sl`); (EXPAND_TAC "sl" THEN DEL_TAC); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;TRUNCATE_SIMPLEX_EXPLICIT_1]); (EXPAND_TAC "sl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2:real^3;u3]`; TRUNCATE_SIMPLEX_EXPLICIT_2]); (REWRITE_WITH `hl ([u0;u1;u2:real^3]) = hl (truncate_simplex 2 (sl:(real^3)list))`); (AP_TERM_TAC); (ASM_MESON_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (REWRITE_WITH `[u0;u1;u2:real^3] = sl`); (ASM_MESON_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (NEW_GOAL `!i j. i < j /\ j <= 2 ==> hl (truncate_simplex i (sl:(real^3)list)) < hl (truncate_simplex j sl)`); (MATCH_MP_TAC XNHPWAB4); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (EXPAND_TAC "sl" THEN REWRITE_TAC[IN]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (FIRST_ASSUM MATCH_MP_TAC); (ARITH_TAC); (* ================================================================== *) (NEW_GOAL `p IN convex hull {b, c, u0, u1:real^3}`); (UP_ASM_TAC THEN UP_ASM_TAC); (REWRITE_TAC[CONVEX_HULL_4; midpoint; IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`); (EXISTS_TAC `u + v * inv (&2)` THEN EXISTS_TAC `v * inv (&2)`); (ASM_REWRITE_TAC[]); (NEW_GOAL `&0 <= v * inv (&2)`); (MATCH_MP_TAC REAL_LE_MUL); (ASM_REAL_ARITH_TAC); (ASM_REWRITE_TAC[REAL_ARITH `w + z + (u + v * inv (&2)) + v * inv (&2) = u + v + w + z`]); (STRIP_TAC); (MATCH_MP_TAC REAL_LE_ADD); (ASM_REWRITE_TAC[]); (VECTOR_ARITH_TAC); (NEW_GOAL `convex hull {b, c, u0, u1:real^3} = convex hull {b, s, u0, u1} UNION convex hull {s, c, u0, u1}`); (MATCH_MP_TAC CONVEX_HULL_BREAK_KY_LEMMA); (ASM_REWRITE_TAC[]); (SWITCH_TAC THEN UP_ASM_TAC THEN ASM_REWRITE_TAC[IN_UNION]); (NEW_GOAL `~(p IN convex hull {s, c, u0, u1:real^3})`); (STRIP_TAC); (NEW_GOAL `p IN aff_ge {u0, u1} {mxi V ul, c:real^3}`); (NEW_GOAL `convex hull {s, c, u0, u1} SUBSET aff_ge {u0, u1} {s, c:real^3}`); (REWRITE_WITH `{s, c, u0, u1} = {u0,u1,s, c:real^3}`); (SET_TAC[]); (REWRITE_TAC[CONVEX_HULL_4_SUBSET_AFF_GE_2_2]); (ASM_SET_TAC[]); (ASM_MESON_TAC[]); (DISCH_TAC); (NEW_GOAL `p IN convex hull {b, s, u0, u1:real^3}`); (ASM_MESON_TAC[]); (NEW_GOAL `b IN convex hull {u0,u1,u2:real^3}`); (EXPAND_TAC "b"); (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;OMEGA_LIST_TRUNCATE_2]); (ABBREV_TAC `wl = [u0;u1;u2:real^3]`); (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list wl`); (EXPAND_TAC "wl" THEN REWRITE_TAC[set_of_list]); (MATCH_MP_TAC XNHPWAB2); (EXISTS_TAC `2`); (REWRITE_WITH `wl = truncate_simplex 2 (ul:(real^3)list)`); (EXPAND_TAC "wl" THEN REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`]); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (ASM_REWRITE_TAC[IN]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_MESON_TAC[ARITH_RULE `2 <= 3`]); (UP_ASM_TAC THEN UP_ASM_TAC); (REWRITE_TAC[CONVEX_HULL_3; CONVEX_HULL_4; IN; IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `w + u * u'`); (EXISTS_TAC `z + u * v'`); (EXISTS_TAC `u * w'`); (EXISTS_TAC `v:real`); (ASM_SIMP_TAC[REAL_LE_ADD; REAL_LE_MUL]); (STRIP_TAC); (ASM_REWRITE_TAC[REAL_ARITH `(w + u * u') + (z + u * v') + u * w' + v = u * (u' + v' + w') + v + w + z`; REAL_MUL_RID]); (VECTOR_ARITH_TAC); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[])]);; (* =========================================================================== *) (* =========================================================================== *) let SLTSTLO2 = prove_by_refinement ( SLTSTLO2_concl, [(REPEAT STRIP_TAC); (ABBREV_TAC `B1 = frontier (rogers V (ul:(real^3)list))`); (ABBREV_TAC `B2 = {w| norm ((w:real^3) - (HD ul)) = sqrt (&2)}`); (ABBREV_TAC `B3 = rcone_eq (HD (ul:(real^3)list)) (HD (TL ul)) (hl (truncate_simplex 1 ul) / sqrt (&2))`); (ABBREV_TAC `B4 = affine hull {(HD (ul:(real^3)list)), (HD (TL ul)), mxi V ul}`); (ABBREV_TAC `B5 = convex hull {omega_list_n V ul 2, omega_list_n V (ul:(real^3)list) 3 }`); (ABBREV_TAC `B6 = affine hull {(HD (ul:(real^3)list)), (HD (TL ul)), (HD (TL (TL ul)))}`); (ABBREV_TAC `B7 = affine hull {omega_list_n V ul 1, omega_list_n V ul 2, omega_list_n V ul 3}`); (ABBREV_TAC `Z = B1 UNION B2 UNION B3 UNION B4 UNION (B5:real^3->bool) UNION B6 UNION B7`); (EXISTS_TAC `Z:real^3->bool`); (REPEAT STRIP_TAC); (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`); (MP_TAC (ASSUME `barV V 3 ul`)); (REWRITE_TAC[BARV_3_EXPLICIT]); (FIRST_X_ASSUM CHOOSE_TAC); (FIRST_X_ASSUM CHOOSE_TAC); (FIRST_X_ASSUM CHOOSE_TAC); (FIRST_X_ASSUM CHOOSE_TAC); (EXPAND_TAC "Z"); (MATCH_MP_TAC NEGLIGIBLE_UNION); (STRIP_TAC); (EXPAND_TAC "B1" THEN MATCH_MP_TAC NEGLIGIBLE_CONVEX_FRONTIER); (ASM_SIMP_TAC[ROGERS_EXPLICIT;CONVEX_CONVEX_HULL]); (MATCH_MP_TAC NEGLIGIBLE_UNION); (STRIP_TAC); (* revised 2013-05-25: *) (NEW_GOAL `(?(v:real^3)(r:real). (r> &0)/\ (B2 ={w:real^3 | norm (w-v)= r}))`); (EXPAND_TAC "B2"); (EXISTS_TAC `(HD ul):real^3` THEN EXISTS_TAC `sqrt(&2)`); (ASM_REWRITE_TAC[REAL_ARITH `a > &0 <=> &0 < a`]); (MATCH_MP_TAC SQRT_POS_LT); (REAL_ARITH_TAC); (ASM_SIMP_TAC[NULLSET_SPHERE]); (* end of revision *) (MATCH_MP_TAC NEGLIGIBLE_UNION); (STRIP_TAC); (EXPAND_TAC "B3"); (MATCH_MP_TAC NEGLIGIBLE_RCONE_EQ); (ASM_REWRITE_TAC[HD;TL]); (STRIP_TAC); (NEW_GOAL `aff_dim (set_of_list [u0;u1:real^3]) = &0`); (ASM_REWRITE_TAC[set_of_list; SET_RULE `{x, x} = {x}`; AFF_DIM_SING]); (NEW_GOAL `aff_dim (set_of_list [u0;u1:real^3]) = &1`); (MATCH_MP_TAC MHFTTZN1); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (REWRITE_WITH `[u0; u0:real^3] = truncate_simplex 1 ul`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3`); (ASM_REWRITE_TAC[]); (ARITH_TAC); (NEW_GOAL `&0 = &1`); (ASM_MESON_TAC[INT_OF_NUM_EQ;REAL_OF_NUM_EQ]); (UP_ASM_TAC THEN REAL_ARITH_TAC); (MATCH_MP_TAC NEGLIGIBLE_UNION); (STRIP_TAC); (EXPAND_TAC "B4"); (REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]); (MATCH_MP_TAC NEGLIGIBLE_UNION); (STRIP_TAC); (EXPAND_TAC "B5"); (ONCE_REWRITE_TAC[SET_RULE `{a,b:real^3} = {a,a,b}`]); (MESON_TAC[NEGLIGIBLE_CONVEX_HULL_3]); (MATCH_MP_TAC NEGLIGIBLE_UNION); (STRIP_TAC); (EXPAND_TAC "B6"); (REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]); (EXPAND_TAC "B7"); (REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]); (* ========================================================================= *) (NEW_GOAL `?u0 u1 u2 u3. (ul:(real^3)list) = [u0:real^3;u1;u2;u3]`); (MP_TAC (ASSUME `barV V 3 ul`)); (REWRITE_TAC[BARV_3_EXPLICIT]); (FIRST_X_ASSUM CHOOSE_TAC); (FIRST_X_ASSUM CHOOSE_TAC); (FIRST_X_ASSUM CHOOSE_TAC); (FIRST_X_ASSUM CHOOSE_TAC); (REWRITE_TAC[EXISTS_UNIQUE]); (NEW_GOAL `?i. i <= 4 /\ p IN mcell i V ul`); (MATCH_MP_TAC SLTSTLO1); (ASM_REWRITE_TAC[]); (ASM_SET_TAC[]); (FIRST_X_ASSUM CHOOSE_TAC THEN EXISTS_TAC `i:num`); (STRIP_TAC); (ASM_REWRITE_TAC[]); (* ========================================================================= *) (ASM_CASES_TAC `hl (ul:(real^3)list) < sqrt(&2)`); (NEW_GOAL ` mcell0 V ul = {} /\ mcell1 V ul = {} /\ mcell2 V ul = {} /\ mcell3 V ul = {}`); (ASM_MESON_TAC[EMNWUUS2]); (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC); (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> ~ (y = 0 \/ y = 1 \/ y = 2 \/ y = 3)`); (REPEAT STRIP_TAC); (UNDISCH_TAC `p IN mcell y V ul` THEN ASM_REWRITE_TAC[MCELL_EXPLICIT]); (SET_TAC[]); (UNDISCH_TAC `p IN mcell y V ul` THEN ASM_REWRITE_TAC[MCELL_EXPLICIT]); (SET_TAC[]); (UNDISCH_TAC `p IN mcell y V ul` THEN ASM_REWRITE_TAC[MCELL_EXPLICIT]); (SET_TAC[]); (UNDISCH_TAC `p IN mcell y V ul` THEN ASM_REWRITE_TAC[MCELL_EXPLICIT]); (SET_TAC[]); (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 4`); (GEN_TAC THEN DISCH_TAC); (NEW_GOAL `~(y = 0 \/ y = 1 \/ y = 2 \/ y = 3)`); (ASM_SIMP_TAC[]); (ASM_ARITH_TAC); (GEN_TAC THEN DISCH_TAC); (NEW_GOAL `y = 4`); (ASM_MESON_TAC[]); (NEW_GOAL `i = 4`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (NEW_GOAL `sqrt (&2) <= hl (ul:(real^3)list)`); (UP_ASM_TAC THEN REAL_ARITH_TAC); (* ========================================================================= *) (ASM_CASES_TAC `dist(u0:real^3, p) >= sqrt(&2)`); (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> ~ (y = 4 \/ y = 1 \/ y = 2 \/ y = 3)`); (REPEAT STRIP_TAC); (NEW_GOAL `mcell 4 V ul = {}`); (SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (REFL_TAC); (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 4`]); (REWRITE_TAC[ASSUME `mcell 4 V ul = {}`]); (SET_TAC[]); (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 1`; MCELL_EXPLICIT;mcell1]); (COND_CASES_TAC); (STRIP_TAC); (NEW_GOAL `~(p:real^3 IN B2)`); (UNDISCH_TAC `p IN rogers V ul DIFF Z` THEN REWRITE_TAC[IN_DIFF]); (EXPAND_TAC "Z" THEN REWRITE_TAC[IN_UNION]); (SET_TAC[]); (NEW_GOAL `p:real^3 IN cball (HD ul,sqrt (&2))`); (ASM_SET_TAC[IN_DIFF;IN_INTER]); (NEW_GOAL `~(p:real^3 IN B2 UNION ball (HD ul,sqrt (&2)))`); (ASM_REWRITE_TAC[IN_UNION;HD;ball;IN;IN_ELIM_THM]); (ASM_REAL_ARITH_TAC); (UP_ASM_TAC THEN REWRITE_WITH `B2 UNION ball (HD ul,sqrt (&2)) = cball (HD (ul:(real^3)list),sqrt (&2))`); (EXPAND_TAC "B2"); (REWRITE_TAC[SET_EQ_LEMMA; IN_UNION; cball; ball;IN;IN_ELIM_THM]); (ONCE_REWRITE_TAC[DIST_SYM]); (REWRITE_TAC[dist] THEN REAL_ARITH_TAC); (ASM_REWRITE_TAC[]); (SET_TAC[]); (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 2`; MCELL_EXPLICIT;mcell2]); (COND_CASES_TAC); (LET_TAC); (ASM_REWRITE_TAC[HD;TL] THEN STRIP_TAC); (NEW_GOAL `p:real^3 IN (rcone_ge u0 u1 a INTER rcone_ge u1 u0 a)`); (ASM_SET_TAC[IN_INTER]); (UP_ASM_TAC THEN REWRITE_TAC[IN_INTER;rcone_ge;rconesgn;IN;IN_ELIM_THM]); (REPEAT STRIP_TAC); (NEW_GOAL `(p - u0) dot (u1 - u0:real^3) + (p - u1) dot (u0 - u1) >= dist (p,u0) * dist (u1,u0) * a + dist (p,u1) * dist (u0,u1) * a`); (ASM_REAL_ARITH_TAC); (UP_ASM_TAC THEN REWRITE_TAC[DIST_SYM]); (REWRITE_WITH `(p - u0) dot (u1 - u0:real^3) + (p - u1) dot (u0 - u1) = (u0 - u1) dot (u0 - u1)`); (VECTOR_ARITH_TAC); (REWRITE_TAC[REAL_ARITH `x * a * b + y * a * b = (x + y) * a * b`; GSYM NORM_POW_2; GSYM dist]); (* ========================================================================== *) (NEW_GOAL `dist (p,u0:real^3) <= dist (p,u1) /\ a = (inv(&2) * dist (u0,u1)) / sqrt (&2)`); (REPEAT STRIP_TAC); (NEW_GOAL `p IN rogers V ul`); (ASM_SET_TAC[IN_DIFF]); (NEW_GOAL `(p:real^3) IN voronoi_closed V u0`); (NEW_GOAL `(p:real^3) IN voronoi_closed V u0 <=> (?vl. vl IN barV V 3 /\ p IN rogers V vl /\ truncate_simplex 0 vl = [u0:real^3])`); (MATCH_MP_TAC GLTVHUM); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC BARV_IMP_u0_IN_V); (EXISTS_TAC `ul:(real^3)list`); (EXISTS_TAC `u1:real^3`); (EXISTS_TAC `u2:real^3`); (EXISTS_TAC `u3:real^3`); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (EXISTS_TAC `ul:(real^3)list`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_0]); (ASM_SET_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed;IN;IN_ELIM_THM]); (DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC); (NEW_GOAL `set_of_list (ul:(real^3)list) SUBSET V`); (MATCH_MP_TAC Packing3.BARV_SUBSET); (EXISTS_TAC `3` THEN ASM_MESON_TAC[]); (UP_ASM_TAC THEN ASM_REWRITE_TAC[set_of_list]); (SET_TAC[]); (EXPAND_TAC "a"); (AP_THM_TAC); (AP_TERM_TAC); (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_1; HL;set_of_list]); (NEW_GOAL `!w. w IN {u0,u1:real^3} ==> radV {u0,u1} = dist (circumcenter {u0,u1},w)`); (MATCH_MP_TAC Rogers.OAPVION2); (REWRITE_TAC[AFFINE_INDEPENDENT_IFF_CARD]); (STRIP_TAC); (REWRITE_TAC[Geomdetail.FINITE6]); (NEW_GOAL `aff_dim {u0, u1:real^3} = &1`); (ABBREV_TAC `vl = [u0;u1:real^3]`); (REWRITE_WITH `{u0, u1:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (MATCH_MP_TAC Rogers.MHFTTZN1); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (REWRITE_WITH `vl = truncate_simplex 1 ul:(real^3)list`); (EXPAND_TAC "vl" THEN DEL_TAC); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]); (ARITH_TAC); (ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[ARITH_RULE `&1 = &(CARD {u0, u1:real^3}) - (&1):int <=> &(CARD {u0, u1:real^3}) = (&2):int`]); (ONCE_REWRITE_TAC[INT_OF_NUM_EQ]); (REWRITE_TAC[Geomdetail.CARD2]); (REPEAT STRIP_TAC); (NEW_GOAL `CARD {u0, u1:real^3} = 1`); (REWRITE_WITH `{u0, u1} = {u1:real^3}`); (ASM_SET_TAC[]); (REWRITE_TAC[Geomdetail.CARD_SING]); (NEW_GOAL `aff_dim {u0, u1} <= &(CARD {u0, u1:real^3}) - (&1):int`); (MATCH_MP_TAC AFF_DIM_LE_CARD); (REWRITE_TAC[Geomdetail.FINITE6]); (NEW_GOAL `(&2):int <= &(CARD {u0, u1:real^3})`); (ONCE_REWRITE_TAC[ARITH_RULE `(&2):int <= &(CARD {u0, u1:real^3}) <=> &1 <= &(CARD {u0, u1:real^3}) - (&1):int`]); (ASM_MESON_TAC[]); (NEW_GOAL `&(CARD {u0, u1:real^3}) <= (&2):int`); (ONCE_REWRITE_TAC[INT_OF_NUM_LE]); (REWRITE_TAC[Geomdetail.CARD2]); (NEW_GOAL `CARD {u0, u1:real^3} = 2`); (ONCE_REWRITE_TAC[GSYM INT_OF_NUM_EQ]); (ASM_ARITH_TAC); (ASM_ARITH_TAC); (REWRITE_WITH `radV {u0, u1} = dist (circumcenter {u0, u1},u0:real^3)`); (FIRST_X_ASSUM MATCH_MP_TAC); (TRUONG_SET_TAC[]); (REWRITE_TAC[CIRCUMCENTER_2;midpoint;dist; VECTOR_ARITH `inv (&2) % (u0 + u1) - u0 = inv (&2) % (u1 - u0)`]); (REWRITE_TAC[NORM_MUL]); (REWRITE_WITH `abs (inv (&2)) = inv (&2)`); (REWRITE_TAC[REAL_ABS_REFL]); (REAL_ARITH_TAC); (REWRITE_TAC[GSYM dist]); (MESON_TAC[DIST_SYM]); (UP_ASM_TAC THEN REPEAT STRIP_TAC); (NEW_GOAL `(dist (p,u0) + dist (p,u1:real^3)) * dist (u0,u1) * a >= (&2 * dist (p,u0)) * dist (u0,u1) * a`); (REWRITE_TAC[REAL_ARITH `(x + y) * a * b >= (&2 * x) * a * b <=> &0 <= (y - x) * a * b`]); (MATCH_MP_TAC REAL_LE_MUL); (STRIP_TAC); (ASM_REAL_ARITH_TAC); (MATCH_MP_TAC REAL_LE_MUL); (STRIP_TAC); (REWRITE_TAC[DIST_POS_LE]); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC REAL_LE_DIV); (STRIP_TAC); (MATCH_MP_TAC REAL_LE_MUL); (STRIP_TAC); (REAL_ARITH_TAC); (REWRITE_TAC[DIST_POS_LE]); (MATCH_MP_TAC SQRT_POS_LE); (REAL_ARITH_TAC); (NEW_GOAL `dist (u0,u1:real^3) pow 2 >= (&2 * dist (p,u0)) * dist (u0,u1) * a `); (ASM_REAL_ARITH_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (REWRITE_TAC[REAL_ARITH `(&2 * x) * a * (inv(&2) * a) / b = (x / b) * a pow 2`]); (REWRITE_TAC[REAL_ARITH `a >= x * a <=> &0 <= a * (&1 - x)`]); (DISCH_TAC); (NEW_GOAL `&0 <= dist (u0,u1) pow 2 * (&1 - dist (p,u0) / sqrt (&2)) <=> &0 <= (&1 - dist (p,u0:real^3) / sqrt (&2))`); (NEW_GOAL `&0 < dist (u0,u1:real^3) pow 2`); (REWRITE_TAC[GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT; DIST_EQ_0]); (STRIP_TAC); (NEW_GOAL `aff_dim {u0, u1:real^3} = &1`); (ABBREV_TAC `vl = [u0;u1:real^3]`); (REWRITE_WITH `{u0, u1:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (MATCH_MP_TAC Rogers.MHFTTZN1); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (REWRITE_WITH `vl = truncate_simplex 1 ul:(real^3)list`); (EXPAND_TAC "vl" THEN DEL_TAC); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]); (ARITH_TAC); (NEW_GOAL `CARD {u0, u1:real^3} = 1`); (REWRITE_WITH `{u0, u1} = {u1:real^3}`); (ASM_SET_TAC[]); (REWRITE_TAC[Geomdetail.CARD_SING]); (NEW_GOAL `aff_dim {u0, u1} <= &(CARD {u0, u1:real^3}) - (&1):int`); (MATCH_MP_TAC AFF_DIM_LE_CARD); (REWRITE_TAC[Geomdetail.FINITE6]); (UP_ASM_TAC THEN ASM_REWRITE_TAC[]); (ASM_ARITH_TAC); (ASM_MESON_TAC[REAL_LE_MUL_EQ]); (NEW_GOAL `&0 <= &1 - dist (p,u0:real^3) / sqrt (&2)`); (ASM_MESON_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]); (REWRITE_WITH `dist (p,u0:real^3) / sqrt (&2) <= &1 <=> dist (p,u0) <= &1 * sqrt (&2)`); (MATCH_MP_TAC REAL_LE_LDIV_EQ); (MATCH_MP_TAC SQRT_POS_LT); (REAL_ARITH_TAC); (REWRITE_TAC [REAL_MUL_LID]); (STRIP_TAC); (NEW_GOAL `dist (p, u0:real^3) = sqrt (&2)`); (UP_ASM_TAC THEN ONCE_REWRITE_TAC[DIST_SYM]); (ASM_REAL_ARITH_TAC); (NEW_GOAL `~(p:real^3 IN B2)`); (ASM_SET_TAC[IN_DIFF]); (UP_ASM_TAC THEN EXPAND_TAC "B2" THEN REWRITE_TAC[IN;IN_ELIM_THM]); (ASM_REWRITE_TAC[HD;GSYM dist]); (SET_TAC[]); (* ========================================================================= *) (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 3`; MCELL_EXPLICIT;mcell3]); (COND_CASES_TAC); (ASM_REWRITE_TAC[HD;TL;set_of_list]); (NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\ dist (u0,s) = sqrt (&2) /\ mxi V ul = s:real^3)`); (MATCH_MP_TAC MXI_EXPLICIT_OLD); (ASM_REWRITE_TAC[]); (FIRST_X_ASSUM CHOOSE_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]); (REWRITE_TAC[SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]); (STRIP_TAC); (SUBGOAL_THEN `p:real^3 IN rogers V ul` MP_TAC); (ASM_SET_TAC[IN_DIFF]); (ASM_SIMP_TAC[ROGERS_EXPLICIT; HD]); (ABBREV_TAC `s1 = omega_list_n V [u0; u1; u2; u3:real^3] 1`); (ABBREV_TAC `s2 = omega_list_n V [u0; u1; u2; u3:real^3] 2`); (ABBREV_TAC `s3 = omega_list_n V [u0; u1; u2; u3:real^3] 3`); (STRIP_TAC); (NEW_GOAL `?m n:real^3. between p (m,n) /\ between m (u0,s1) /\ between n (s2,s3)`); (ASM_SIMP_TAC[CONVEX_HULL_4_IMP_2_2]); (UP_ASM_TAC THEN REPEAT STRIP_TAC); (NEW_GOAL `between (p - m:real^3) (vec 0, n - m)`); (UNDISCH_TAC `between p (m,n:real^3)` THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC); (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real` THEN ASM_REWRITE_TAC[]); (REWRITE_WITH `(u % m + v % n) - m:real^3 = (u % m + v % n) - (u + v) % m`); (ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC); (VECTOR_ARITH_TAC); (NEW_GOAL `between (proj_point (s2 - m) (p - m:real^3)) (vec 0, proj_point (s2 - m) (n - m))`); (REWRITE_WITH `vec 0 = proj_point (s2 - m) (m - m:real^3)`); (REWRITE_TAC[VECTOR_SUB_REFL; PRO_EXP; DOT_LZERO; REAL_ARITH `&0 / a = &0`]); (VECTOR_ARITH_TAC); (MATCH_MP_TAC BETWEEN_PROJ_POINT); (ASM_REWRITE_TAC[VECTOR_SUB_REFL]); (ABBREV_TAC `p' = proj_point (s2 - m) (p - m:real^3)`); (ABBREV_TAC `n' = proj_point (s2 - m) (n - m:real^3)`); (* ============================================================================ *) (ABBREV_TAC `vl = [u0;u1;u2:real^3]`); (NEW_GOAL `s2:real^3 = circumcenter (set_of_list vl)`); (EXPAND_TAC "s2" THEN EXPAND_TAC "vl"); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_2]); (MATCH_MP_TAC XNHPWAB1); (EXISTS_TAC `2`); (REWRITE_WITH `[u0; u1; u2:real^3] = truncate_simplex 2 ul`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (ASM_REWRITE_TAC[IN]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3`); (ASM_MESON_TAC[ARITH_RULE `2 <= 3`]); (NEW_GOAL `s3 IN voronoi_list V (truncate_simplex 2 (ul:(real^3)list))`); (NEW_GOAL `s3 IN voronoi_list V (truncate_simplex (SUC 2) [u0:real^3; u1; u2; u3])`); (EXPAND_TAC "s3"); (REWRITE_TAC[OMEGA_LIST_N;ARITH_RULE `3 = SUC 2`]); (MATCH_MP_TAC CLOSEST_POINT_IN_SET); (REWRITE_TAC[Packing3.CLOSED_VORONOI_LIST]); (MATCH_MP_TAC Packing3.BARV_IMP_VORONOI_LIST_NOT_EMPTY); (EXISTS_TAC `3`); (REWRITE_WITH `truncate_simplex (SUC 2) [u0; u1; u2; u3:real^3] = ul`); (ASM_REWRITE_TAC[ARITH_RULE `SUC 2 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3]); (ASM_MESON_TAC[]); (UP_ASM_TAC); (REWRITE_WITH `truncate_simplex (SUC 2) [u0; u1; u2; u3:real^3] = ul`); (ASM_REWRITE_TAC[ARITH_RULE `SUC 2 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3]); (STRIP_TAC); (NEW_GOAL `voronoi_list V (ul:(real^3)list) SUBSET voronoi_list V (truncate_simplex 2 ul)`); (ASM_REWRITE_TAC[VORONOI_LIST;VORONOI_SET; SUBSET; TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list; IN_INTERS]); (EXPAND_TAC "vl" THEN REWRITE_TAC[IN; IN_ELIM_THM;set_of_list] THEN REPEAT STRIP_TAC); (FIRST_ASSUM MATCH_MP_TAC); (EXISTS_TAC `v:real^3`); (ASM_REWRITE_TAC[]); (SWITCH_TAC THEN UP_ASM_TAC THEN TRUONG_SET_TAC[]); (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[SUBSET]); (NEW_GOAL `n' = s2:real^3 - m`); (EXPAND_TAC "n'"); (UNDISCH_TAC `between n (s2,s3:real^3)` THEN REWRITE_TAC[ BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC); (REWRITE_TAC[ASSUME `n:real^3 = u % s2 + v % s3`]); (REWRITE_WITH `(u % s2 + v % s3) - m:real^3 = (s2 - m) + v % (s3 - s2)`); (REWRITE_TAC[VECTOR_ARITH `(u % s2 + v % s3) - m = s2 - m + v % (s3 - s2) <=> (u + v) % s2 = s2`]); (ASM_REWRITE_TAC[VECTOR_MUL_LID]); (REWRITE_TAC[PRO_EXP]); (REWRITE_WITH `((s2 - m + v % (s3 - s2)) dot (s2 - m)) / ((s2 - m) dot (s2 - m:real^3)) = &1`); (REWRITE_TAC[DOT_LADD; REAL_ARITH `(a + b) / c = a / c + b / c`]); (REWRITE_WITH `((s2 - m) dot (s2 - m)) / ((s2 - m) dot (s2 - m:real^3)) = &1`); (MATCH_MP_TAC REAL_DIV_REFL); (REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0;NORM_EQ_0]); (REWRITE_TAC[VECTOR_ARITH `s2 - m = vec 0 <=> s2 = m`]); (STRIP_TAC); (NEW_GOAL `between s2 (u0, s1:real^3)`); (ASM_MESON_TAC[]); (NEW_GOAL `s2 IN affine hull {u0, s1:real^3}`); (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]); (STRIP_TAC); (NEW_GOAL `convex hull {u0,s1:real^3} SUBSET affine hull {u0,s1}`); (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]); (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]); (NEW_GOAL `affine hull {u0,s1,s2} = affine hull {u0, s1:real^3}`); (MATCH_MP_TAC AFFINE_HULLS_EQ); (REWRITE_TAC[SUBSET; SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]); (ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]); (ASM_MESON_TAC[]); (UP_ASM_TAC); (REWRITE_TAC[SUBSET; SET_RULE `x IN {b,c} <=> x = b \/ x = c`]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]); (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`); (STRIP_TAC); (REAL_ARITH_TAC); (VECTOR_ARITH_TAC); (ASM_REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]); (EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0`); (STRIP_TAC); (REAL_ARITH_TAC); (VECTOR_ARITH_TAC); (NEW_GOAL `aff_dim {u0,s1,s2:real^3} <= &1`); (ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL]); (ONCE_ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[AFF_DIM_AFFINE_HULL]); (MATCH_MP_TAC (ARITH_RULE `(?x. x <= &1 /\ y <= x:int) ==> y <= &1`)); (EXISTS_TAC `&(CARD {u0,s1:real^3}):int - &1`); (STRIP_TAC); (REWRITE_TAC[ARITH_RULE `a:int - &1 <= &1 <=> a <= &2`; INT_OF_NUM_LE]); (REWRITE_TAC[Geomdetail.CARD2]); (MATCH_MP_TAC AFF_DIM_LE_CARD); (REWRITE_TAC[Geomdetail.FINITE6]); (NEW_GOAL `aff_dim {u0,s1,s2:real^3} = &2`); (NEW_GOAL `vl:(real^3)list = truncate_simplex 2 ul`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (REWRITE_WITH `aff_dim {u0,s1,s2:real^3} = aff_dim {omega_list_n V vl j | j IN 0..2}`); (AP_TERM_TAC); (REWRITE_TAC[IN_NUMSEG_0]); (REWRITE_TAC[SET_EQ_LEMMA; SET_RULE `x IN {a,b,c} <=> (x = a \/ x = b \/ x = c)`; IN;IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `0`); (REWRITE_TAC[ARITH_RULE `0 <= 2`; OMEGA_LIST_N]); (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]); (ASM_REWRITE_TAC[]); (EXISTS_TAC `1`); (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]); (EXPAND_TAC "vl"); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (DEL_TAC); (EXPAND_TAC "s1"); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]); (EXISTS_TAC `2`); (REWRITE_TAC[ARITH_RULE `2 <= 2`; ASSUME `x = s2:real^3`] THEN EXPAND_TAC "vl" THEN DEL_TAC); (EXPAND_TAC "s2"); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]); (REWRITE_TAC[set_of_list; OMEGA_LIST_TRUNCATE_2; OMEGA_LIST_TRUNCATE_2_NEW1]); (ASM_CASES_TAC `j = 0`); (DISJ1_TAC); (REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`; OMEGA_LIST_N; HD]); (EXPAND_TAC "vl"); (REWRITE_TAC[ASSUME `j = 0`]); (REWRITE_TAC[OMEGA_LIST_N; HD]); (ASM_CASES_TAC `j = 1`); (DISJ2_TAC); (DISJ1_TAC); (ASM_REWRITE_TAC[]); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]); (EXPAND_TAC "s1"); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]); (ASM_CASES_TAC `j = 2`); (DISJ2_TAC); (DISJ2_TAC); (REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`]); (EXPAND_TAC "vl"); (EXPAND_TAC "s2"); (REWRITE_TAC[ASSUME `j = 2`; OMEGA_LIST_TRUNCATE_2; OMEGA_LIST_TRUNCATE_2_NEW1]); (SUBGOAL_THEN `F` MP_TAC); (ASM_ARITH_TAC); (MESON_TAC[]); (MATCH_MP_TAC XNHPWAB3); (ASM_REWRITE_TAC[IN]); STRIP_TAC; (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (* ========================================================================= *) (* ========================================================================== *) (MATCH_MP_TAC (REAL_ARITH `x = &0 ==> a + x = a`)); (REWRITE_TAC[DOT_LMUL]); (REWRITE_WITH `(s3 - s2) dot (s2 - m:real^3) = &0`); (ONCE_REWRITE_TAC[VECTOR_ARITH `a dot (b - c) = -- (a dot (c - b))`]); (ONCE_REWRITE_TAC[REAL_ARITH `--a = &0 <=> a = &0`]); (REWRITE_TAC[ASSUME `s2:real^3 = circumcenter (set_of_list vl)`]); (MATCH_MP_TAC MHFTTZN4); (EXISTS_TAC `V:real^3->bool`); (EXISTS_TAC `2`); (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`); (EXPAND_TAC "vl" THEN DEL_TAC); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3`); (ASM_MESON_TAC[ARITH_RULE `2 <= 3`]); (* ========================================================================== *) (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (UNDISCH_TAC `between m (u0,s1:real^3)`); (REWRITE_WITH `s1 = midpoint (u0,u1:real^3)`); (EXPAND_TAC "s1"); (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 = omega_list_n V [u0; u1:real^3] 1`); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2;OMEGA_LIST_TRUNCATE_1]); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2]); (REWRITE_WITH `omega_list V [u0; u1:real^3] = circumcenter (set_of_list [u0;u1])`); (MATCH_MP_TAC XNHPWAB1); (EXISTS_TAC `1`); (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]); (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (REWRITE_TAC[IN] THEN STRIP_TAC); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `2` THEN REWRITE_TAC[ARITH_RULE `1 <= 2`]); (REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (NEW_GOAL `!i j. i < j /\ j <= 2 ==> hl (truncate_simplex i (vl:(real^3)list)) < hl (truncate_simplex j vl)`); (MATCH_MP_TAC XNHPWAB4); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[IN]); (REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (ASM_MESON_TAC[]); (NEW_GOAL `hl (truncate_simplex 1 (vl:(real^3)list)) < hl (truncate_simplex 2 vl)`); (FIRST_X_ASSUM MATCH_MP_TAC); (ARITH_TAC); (NEW_GOAL `truncate_simplex 2 vl = truncate_simplex 2 ul:(real^3)list`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (MATCH_MP_TAC (REAL_ARITH `a < hl (truncate_simplex 2 (vl:(real^3)list)) /\ hl (truncate_simplex 2 vl) < b ==> a < b`)); (ASM_REWRITE_TAC[]); (ASM_MESON_TAC[]); (REWRITE_TAC[set_of_list;Rogers.CIRCUMCENTER_2]); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2; midpoint; IN; IN_ELIM_THM; AFFINE_HULL_3]); (REPEAT STRIP_TAC); (EXISTS_TAC `u' + v' * inv (&2)`); (EXISTS_TAC `v' * inv (&2)`); (EXISTS_TAC `&0`); (STRIP_TAC); (REWRITE_TAC[REAL_ARITH `(u' + v' * inv (&2)) + v' * inv (&2) + &0 = u' + v'`]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (VECTOR_ARITH_TAC); (REWRITE_TAC[REAL_MUL_RZERO; REAL_ARITH `&0 / x = &0`]); (VECTOR_ARITH_TAC); (* ========================================================================== *) (NEW_GOAL `norm (u0 - p:real^3) pow 2 = norm ((p'+ m) - p) pow 2 + norm (u0 - (p' + m)) pow 2`); (MATCH_MP_TAC PYTHAGORAS); (REWRITE_WITH `p - (p'+ m) = projection (s2 - m) (p - m:real^3)`); (REWRITE_TAC[VECTOR_ARITH `p - (a + b:real^3) = (p - b) - a`]); (EXPAND_TAC "p'" THEN REWRITE_TAC[proj_point]); (UNDISCH_TAC `between (p - m) (vec 0,n - m:real^3)`); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;IN; IN_ELIM_THM; VECTOR_MUL_RZERO;VECTOR_ADD_LID]); (REPEAT STRIP_TAC); (VECTOR_ARITH_TAC); (NEW_GOAL `(?k. k <= &1 /\ &0 <= k /\ projection (s2 - m) (p - m:real^3) = k % projection (s2 - m) (n - m))`); (MATCH_MP_TAC PARALLEL_PROJECTION); (ASM_REWRITE_TAC[]); (STRIP_TAC); (NEW_GOAL `s2 = m:real^3`); (ASM_REWRITE_TAC[]); (SWITCH_TAC THEN DEL_TAC); (NEW_GOAL `between s2 (u0, s1:real^3)`); (ASM_MESON_TAC[]); (NEW_GOAL `s2 IN affine hull {u0, s1:real^3}`); (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]); (STRIP_TAC); (NEW_GOAL `convex hull {u0,s1:real^3} SUBSET affine hull {u0,s1}`); (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]); (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]); (NEW_GOAL `affine hull {u0,s1,s2} = affine hull {u0, s1:real^3}`); (MATCH_MP_TAC AFFINE_HULLS_EQ); (REWRITE_TAC[SUBSET; SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]); (ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]); (ASM_MESON_TAC[]); (UP_ASM_TAC); (REWRITE_TAC[SUBSET; SET_RULE `x IN {b,c} <=> x = b \/ x = c`]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]); (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`); (STRIP_TAC); (REAL_ARITH_TAC); (VECTOR_ARITH_TAC); (REWRITE_TAC[ASSUME `x = s1:real^3`;AFFINE_HULL_3;IN;IN_ELIM_THM]); (EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0`); (STRIP_TAC); (REAL_ARITH_TAC); (VECTOR_ARITH_TAC); (NEW_GOAL `aff_dim {u0,s1,s2:real^3} <= &1`); (ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL]); (ONCE_ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[AFF_DIM_AFFINE_HULL]); (MATCH_MP_TAC (ARITH_RULE `(?x. x <= &1 /\ y <= x:int) ==> y <= &1`)); (EXISTS_TAC `&(CARD {u0,s1:real^3}):int - &1`); (STRIP_TAC); (REWRITE_TAC[ARITH_RULE `a:int - &1 <= &1 <=> a <= &2`; INT_OF_NUM_LE]); (REWRITE_TAC[Geomdetail.CARD2]); (MATCH_MP_TAC AFF_DIM_LE_CARD); (REWRITE_TAC[Geomdetail.FINITE6]); (NEW_GOAL `aff_dim {u0,s1,s2:real^3} = &2`); (NEW_GOAL `vl:(real^3)list = truncate_simplex 2 ul`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (REWRITE_WITH `aff_dim {u0,s1,s2:real^3} = aff_dim {omega_list_n V vl j | j IN 0..2}`); (AP_TERM_TAC); (REWRITE_TAC[IN_NUMSEG_0]); (REWRITE_TAC[SET_EQ_LEMMA; SET_RULE `x IN {a,b,c} <=> (x = a \/ x = b \/ x = c)`; IN;IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `0`); (REWRITE_TAC[ARITH_RULE `0 <= 2`; OMEGA_LIST_N]); (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]); (ASM_REWRITE_TAC[]); (EXISTS_TAC `1`); (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]); (EXPAND_TAC "vl"); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (DEL_TAC); (EXPAND_TAC "s1"); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]); (EXISTS_TAC `2`); (REWRITE_TAC[ARITH_RULE `2 <= 2`; ASSUME `x = s2:real^3`] THEN EXPAND_TAC "vl" THEN DEL_TAC); (EXPAND_TAC "s2"); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]); (REWRITE_TAC[set_of_list; OMEGA_LIST_TRUNCATE_2; OMEGA_LIST_TRUNCATE_2_NEW1]); (ASM_CASES_TAC `j = 0`); (DISJ1_TAC); (REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`; OMEGA_LIST_N; HD]); (EXPAND_TAC "vl"); (REWRITE_TAC[ASSUME `j = 0`]); (REWRITE_TAC[OMEGA_LIST_N; HD]); (ASM_CASES_TAC `j = 1`); (DISJ2_TAC); (DISJ1_TAC); (ASM_REWRITE_TAC[]); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]); (EXPAND_TAC "s1"); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]); (ASM_CASES_TAC `j = 2`); (DISJ2_TAC); (DISJ2_TAC); (REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`]); (EXPAND_TAC "vl"); (EXPAND_TAC "s2"); (REWRITE_TAC[ASSUME `j = 2`; OMEGA_LIST_TRUNCATE_2; OMEGA_LIST_TRUNCATE_2_NEW1]); (SUBGOAL_THEN `F` MP_TAC); (ASM_ARITH_TAC); (MESON_TAC[]); (MATCH_MP_TAC XNHPWAB3); (ASM_REWRITE_TAC[IN]); STRIP_TAC; (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (FIRST_X_ASSUM CHOOSE_TAC); (UP_ASM_TAC THEN STRIP_TAC); (REWRITE_TAC[ASSUME `projection (s2 - m) (p - m:real^3) = k % projection (s2 - m) (n - m)`]); (REWRITE_TAC[projection_proj_point; orthogonal]); (REWRITE_TAC[ASSUME `proj_point (s2 - m) (n - m:real^3) = n'`]); (REWRITE_TAC[ASSUME `n' = s2 - m:real^3`; VECTOR_ARITH `n - m - (a - m:real^3) = n - a`]); (UNDISCH_TAC `between n (s2,s3:real^3)`); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC); (REWRITE_TAC[ASSUME `n = u % s2 + v % s3:real^3`]); (REWRITE_WITH `(u % s2 + v % s3:real^3) - s2 = (u % s2 + v % s3) - (u + v) % s2`); (ASM_REWRITE_TAC[VECTOR_MUL_LID]); (REWRITE_TAC[VECTOR_ARITH `(u % s2 + v % s3) - (u + v) % s2 = v % (s3 - s2:real^3)`]); (ONCE_REWRITE_TAC[VECTOR_ARITH `u0 - (p' + m) = ((u0:real^3) + s2 - (p' + m)) - s2`]); (NEW_GOAL `(s3 - s2:real^3) dot ((u0 + s2 - (p' + m)) - s2) = &0`); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC MHFTTZN4); (EXISTS_TAC `V:real^3->bool`); (EXISTS_TAC `2`); (ASM_REWRITE_TAC[]); (STRIP_TAC); (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl"); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (STRIP_TAC); (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1); (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl"); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (NEW_GOAL `!a b c m n p. m IN affine hull {a,b,c:real^3} /\ n IN affine hull {a,b,c} /\ p IN affine hull {a,b,c} ==> m + n - p IN affine hull {a,b,c}`); (REWRITE_TAC[AFFINE_HULL_3; IN;IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `(u' + u'') - u'''`); (EXISTS_TAC `(v' + v'') - v'''`); (EXISTS_TAC `(w + w') - w''`); STRIP_TAC; (ASM_REAL_ARITH_TAC); (ASM_REWRITE_TAC[]); (VECTOR_ARITH_TAC); (FIRST_X_ASSUM MATCH_MP_TAC); (REPEAT STRIP_TAC); (REWRITE_TAC[AFFINE_HULL_3; IN;IN_ELIM_THM]); (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`); STRIP_TAC; (ASM_REAL_ARITH_TAC); (VECTOR_ARITH_TAC); (MATCH_MP_TAC Rogers.OAPVION1); (STRIP_TAC); (SET_TAC[]); (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT); (EXISTS_TAC `V:real^3->bool`); (EXISTS_TAC `2`); (ASM_REWRITE_TAC[]); (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl"); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (MATCH_MP_TAC Packing3. TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (EXPAND_TAC "p'"); (REWRITE_TAC[PRO_EXP]); (ABBREV_TAC `h = ((p - m) dot (s2 - m)) / ((s2 - m) dot (s2 - m:real^3))`); (NEW_GOAL `!a b c x y r. x IN affine hull {a,b,c:real^3} /\ y IN affine hull {a,b,c} ==> r % (x - y) + y IN affine hull {a,b,c}`); (REWRITE_TAC[AFFINE_HULL_3; IN;IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `r * (u' - u'') + u''`); (EXISTS_TAC `r * (v' - v'') + v''`); (EXISTS_TAC `r * (w - w') + w'`); STRIP_TAC; (REWRITE_TAC[REAL_ARITH `(r * (u' - u'') + u'') + (r * (v' - v'') + v'') + r * (w - w') + w' = r * (u' + v' + w) - r * (u'' + v'' + w') + (u'' + v'' + w')`]); (ASM_REWRITE_TAC[REAL_MUL_RID]); (ASM_REAL_ARITH_TAC); (ASM_REWRITE_TAC[]); (VECTOR_ARITH_TAC); (FIRST_X_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (STRIP_TAC); (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (MATCH_MP_TAC Rogers.OAPVION1); (STRIP_TAC); (REWRITE_WITH `set_of_list vl = {u0, u1, u2:real^3}`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (SET_TAC[]); (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT); (EXISTS_TAC `V:real^3->bool`); (EXISTS_TAC `2`); (ASM_REWRITE_TAC[]); (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl"); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (MATCH_MP_TAC Packing3. TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (UNDISCH_TAC `between m (u0,s1:real^3)`); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2; AFFINE_HULL_3;IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC); (UP_ASM_TAC); (REWRITE_WITH `s1 = midpoint (u0,u1:real^3)`); (REWRITE_TAC[GSYM (ASSUME `omega_list_n V [u0; u1; u2; u3:real^3] 1 = s1`)]); (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 = omega_list_n V [u0; u1:real^3] 1`); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2;OMEGA_LIST_TRUNCATE_1]); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2]); (REWRITE_WITH `omega_list V [u0; u1:real^3] = circumcenter (set_of_list [u0;u1])`); (MATCH_MP_TAC XNHPWAB1); (EXISTS_TAC `1`); (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]); (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (REWRITE_TAC[IN] THEN STRIP_TAC); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `2` THEN REWRITE_TAC[ARITH_RULE `1 <= 2`]); (REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (NEW_GOAL `!i j. i < j /\ j <= 2 ==> hl (truncate_simplex i (vl:(real^3)list)) < hl (truncate_simplex j vl)`); (MATCH_MP_TAC XNHPWAB4); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[IN]); (REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (ASM_MESON_TAC[]); (NEW_GOAL `hl (truncate_simplex 1 (vl:(real^3)list)) < hl (truncate_simplex 2 vl)`); (FIRST_X_ASSUM MATCH_MP_TAC); (ARITH_TAC); (NEW_GOAL `truncate_simplex 2 vl = truncate_simplex 2 ul:(real^3)list`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (MATCH_MP_TAC (REAL_ARITH `a < hl (truncate_simplex 2 (vl:(real^3)list)) /\ hl (truncate_simplex 2 vl) < b ==> a < b`)); (ASM_REWRITE_TAC[]); (ASM_MESON_TAC[]); (REWRITE_TAC[set_of_list;Rogers.CIRCUMCENTER_2]); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2; midpoint; IN; IN_ELIM_THM; AFFINE_HULL_3]); (REPEAT STRIP_TAC); (EXISTS_TAC `u' + v' * inv (&2)`); (EXISTS_TAC `v' * inv (&2)`); (EXISTS_TAC `&0`); (STRIP_TAC); (REWRITE_TAC[REAL_ARITH `(u' + v' * inv (&2)) + v' * inv (&2) + &0 = u' + v'`]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (VECTOR_ARITH_TAC); (REWRITE_TAC[VECTOR_ARITH `a % b % c dot d = a * b * (c dot d)`]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[REAL_MUL_RZERO]); (* ========================================================================= *) (NEW_GOAL `norm (u0 - s:real^3) pow 2 = norm (s2 - s) pow 2 + norm (u0 - s2) pow 2`); (MATCH_MP_TAC PYTHAGORAS); (ASM_REWRITE_TAC[orthogonal]); (MATCH_MP_TAC MHFTTZN4); (EXISTS_TAC `V:real^3->bool`); (EXISTS_TAC `2`); (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`); (EXPAND_TAC "vl" THEN DEL_TAC); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3`); (ASM_MESON_TAC[ARITH_RULE `2 <= 3`]); (UNDISCH_TAC `between s (s2,s3:real^3)`); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]); (REPEAT STRIP_TAC); (ONCE_REWRITE_TAC [GSYM IN]); (ONCE_ASM_REWRITE_TAC[]); (NEW_GOAL `convex (affine hull voronoi_list V (truncate_simplex 2 [u0; u1; u2; u3:real^3]))`); (MATCH_MP_TAC POLYHEDRON_IMP_CONVEX); (REWRITE_TAC[POLYHEDRON_AFFINE_HULL]); (UP_ASM_TAC THEN REWRITE_TAC[convex]); (DISCH_TAC); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (REPEAT STRIP_TAC); (REWRITE_WITH `truncate_simplex 2 [u0; u1; u2; u3:real^3] = vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (NEW_GOAL `affine hull (voronoi_list V vl) INTER affine hull (set_of_list vl) = {circumcenter (set_of_list (vl:(real^3)list))}`); (MATCH_MP_TAC Rogers.MHFTTZN3); (EXISTS_TAC `2`); (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`); (EXPAND_TAC "vl" THEN DEL_TAC); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3`); (ASM_MESON_TAC[ARITH_RULE `2 <= 3`]); (UP_ASM_TAC THEN SET_TAC[]); (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1); (ASM_MESON_TAC[]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]); (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1); (SET_TAC[]); (* ======================================================================== *) (NEW_GOAL `norm (u0 - (p' + m)) pow 2 <= norm (u0 - s2:real^3) pow 2`); (REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS; REAL_ABS_NORM;GSYM dist]); (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC[dist]); (NEW_GOAL `(?y. y IN {m, s2:real^3} /\ (!x. x IN convex hull {m,s2} ==> norm (x - u0) <= norm (y - u0 )))`); (MATCH_MP_TAC SIMPLEX_FURTHEST_LE); (STRIP_TAC); (REWRITE_TAC[Geomdetail.FINITE6]); (SET_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[SET_RULE `x IN {a, b} <=> x = b \/ x = a`] THEN REPEAT STRIP_TAC); (UP_ASM_TAC THEN REWRITE_TAC[ASSUME `y' = s2:real^3`]); (DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC); (UNDISCH_TAC `between p' (vec 0,n':real^3)`); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real` THEN ASM_REWRITE_TAC[]); (REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID; VECTOR_ARITH `a % (x - y) + y = b % y + a % x <=> ((b + a) - &1) % y = vec 0`]); (ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO]); (MATCH_MP_TAC (REAL_ARITH `(?s. a <= s /\ s <= b) ==> a <= b`)); (EXISTS_TAC `norm (m - u0:real^3)`); (STRIP_TAC); (UP_ASM_TAC THEN REWRITE_TAC[ASSUME `y' = m:real^3`]); (DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC); (UNDISCH_TAC `between p' (vec 0,n':real^3)`); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `u:real` THEN EXISTS_TAC `v:real` THEN ASM_REWRITE_TAC[]); (REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID; VECTOR_ARITH `a % (x - y) + y = b % y + a % x <=> ((b + a) - &1) % y = vec 0`]); (ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO]); (MATCH_MP_TAC (REAL_ARITH `(?s. a <= s /\ s <= b) ==> a <= b`)); (EXISTS_TAC `norm (s1 - u0:real^3)`); (STRIP_TAC); (REWRITE_TAC[GSYM dist]); (ONCE_REWRITE_TAC[DIST_SYM]); (UNDISCH_TAC `between m (u0,s1:real^3)`); (REWRITE_TAC[between]); (STRIP_TAC); (ASM_REWRITE_TAC[]); (REWRITE_TAC[REAL_ARITH `a <= a + b <=> &0 <= b`; DIST_POS_LE]); (NEW_GOAL `norm (s2 - u0:real^3) pow 2 = norm (s1 - u0) pow 2 + norm (s2 - s1) pow 2`); (MATCH_MP_TAC PYTHAGORAS); (ABBREV_TAC `sl = [u0;u1:real^3]`); (NEW_GOAL `s1:real^3 = circumcenter (set_of_list sl)`); (EXPAND_TAC "s1" THEN EXPAND_TAC "sl"); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]); (MATCH_MP_TAC XNHPWAB1); (EXISTS_TAC `1`); (REWRITE_WITH `[u0; u1:real^3] = truncate_simplex 1 ul`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (ASM_REWRITE_TAC[IN]); (STRIP_TAC); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3`); (ASM_MESON_TAC[ARITH_RULE `1 <= 3`]); (DEL_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (NEW_GOAL `!i j. i < j /\ j <= 2 ==> hl (truncate_simplex i (vl:(real^3)list)) < hl (truncate_simplex j vl)`); (MATCH_MP_TAC XNHPWAB4); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[IN]); (REWRITE_WITH `vl = truncate_simplex 2 ul:(real^3)list`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (ASM_MESON_TAC[]); (NEW_GOAL `hl (truncate_simplex 1 (vl:(real^3)list)) < hl (truncate_simplex 2 vl)`); (FIRST_X_ASSUM MATCH_MP_TAC); (ARITH_TAC); (NEW_GOAL `truncate_simplex 2 vl = truncate_simplex 2 ul:(real^3)list`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (MATCH_MP_TAC (REAL_ARITH `a < hl (truncate_simplex 2 (vl:(real^3)list)) /\ hl (truncate_simplex 2 vl) < b ==> a < b`)); (ASM_REWRITE_TAC[]); (ASM_MESON_TAC[]); (REWRITE_TAC [ASSUME `s1:real^3 = circumcenter (set_of_list sl)`;orthogonal]); (ONCE_REWRITE_TAC[DOT_SYM]); (MATCH_MP_TAC MHFTTZN4); (EXISTS_TAC `V:real^3->bool`); (EXISTS_TAC `1`); (ASM_REWRITE_TAC[]); (STRIP_TAC); (REWRITE_WITH `sl:(real^3)list = truncate_simplex 1 ul`); (ASM_REWRITE_TAC[]); (EXPAND_TAC "sl"); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]); (STRIP_TAC); (NEW_GOAL `affine hull (voronoi_list V vl) SUBSET affine hull (voronoi_list V (sl:(real^3)list))`); (MATCH_MP_TAC AFFINE_SUBSET_KY_LEMMA); (EXPAND_TAC "sl" THEN EXPAND_TAC "vl" THEN REWRITE_TAC [set_of_list; SET_RULE `x IN {a, b} <=> x = a \/ x = b`; SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`; VORONOI_LIST; VORONOI_SET;voronoi_closed; SUBSET;IN_INTERS]); (REWRITE_TAC[IN;IN_ELIM_THM] THEN REPEAT STRIP_TAC); (FIRST_ASSUM MATCH_MP_TAC); (EXISTS_TAC `v:real^3`); (ASM_REWRITE_TAC[]); (FIRST_ASSUM MATCH_MP_TAC); (EXISTS_TAC `v:real^3`); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC (SET_RULE `(?C. C SUBSET B /\ s IN C ) ==> s IN B`)); (EXISTS_TAC `affine hull voronoi_list V (vl:(real^3)list)`); (ASM_REWRITE_TAC[]); (NEW_GOAL `affine hull (voronoi_list V vl) INTER affine hull (set_of_list vl) = {circumcenter (set_of_list (vl:(real^3)list))}`); (MATCH_MP_TAC Rogers.MHFTTZN3); (EXISTS_TAC `2`); (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`); (EXPAND_TAC "vl" THEN DEL_TAC); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3`); (ASM_MESON_TAC[ARITH_RULE `2 <= 3`]); (UP_ASM_TAC THEN SET_TAC[]); (EXPAND_TAC "sl" THEN REWRITE_TAC[set_of_list]); (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1); (SET_TAC[IN]); (REWRITE_WITH `norm (s1 - u0:real^3) <= norm (s2 - u0) <=> norm (s1 - u0) pow 2 <= norm (s2 - u0) pow 2`); (MATCH_MP_TAC Collect_geom.POW2_COND); (REWRITE_TAC[NORM_POS_LE]); (UP_ASM_TAC THEN MATCH_MP_TAC (REAL_ARITH `(&0 <= c) ==> (a = b + c ==> b <= a)`)); (REWRITE_TAC[REAL_LE_POW_2]); (* ==================================================================== *) (NEW_GOAL `norm (u0 - s:real^3) < norm (u0 - p)`); (MATCH_MP_TAC (REAL_ARITH `(?s. a <= s /\ s < b) ==> a < b`)); (EXISTS_TAC `sqrt (&2)`); (STRIP_TAC); (REWRITE_TAC[GSYM dist]); (ASM_REAL_ARITH_TAC); (REWRITE_TAC[GSYM dist]); (UNDISCH_TAC `dist (u0,p:real^3) >= sqrt (&2)`); (MATCH_MP_TAC (REAL_ARITH `~(a = b) ==> (a >= b ==> b < a)`)); (STRIP_TAC); (NEW_GOAL `~(p:real^3 IN B2)`); (ASM_SET_TAC[IN_DIFF]); (UP_ASM_TAC THEN EXPAND_TAC "B2" THEN REWRITE_TAC[IN;IN_ELIM_THM]); (ASM_REWRITE_TAC[HD; GSYM dist]); (ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]); (NEW_GOAL `norm (u0 - s:real^3) pow 2 < norm (u0 - p) pow 2`); (REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS; REAL_ABS_NORM]); (ASM_REWRITE_TAC[]); (NEW_GOAL `norm (s2 - s:real^3) pow 2 < norm ((p' + m) - p:real^3) pow 2`); (REWRITE_WITH `norm (s2 - s) pow 2 = norm (u0 - s:real^3) pow 2 - norm (u0 - s2) pow 2`); (ASM_REAL_ARITH_TAC); (REWRITE_WITH `norm ((p' + m) - p) pow 2 = norm (u0 - p:real^3) pow 2 - norm (u0 - (p' + m)) pow 2`); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (* ======================================================================== *) (UNDISCH_TAC `p IN convex hull {u0, u1, u2, s:real^3}`); (REWRITE_TAC[CONVEX_HULL_4; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC); (NEW_GOAL `(?m1. m1 IN convex hull {u0, u1, u2} /\ between p (m1, s:real^3))`); (ASM_CASES_TAC `(u + v + w = &0)`); (NEW_GOAL `p = s:real^3`); (ASM_REWRITE_TAC[]); (REWRITE_WITH `u = &0 /\ v = &0 /\ w = &0 /\ z = &1`); (ASM_REAL_ARITH_TAC); (VECTOR_ARITH_TAC); (NEW_GOAL `F`); (NEW_GOAL `~(p:real^3 IN B2)`); (ASM_SET_TAC[IN_DIFF]); (UP_ASM_TAC THEN EXPAND_TAC "B2" THEN REWRITE_TAC[IN;IN_ELIM_THM]); (ASM_REWRITE_TAC[HD; GSYM dist]); (REWRITE_WITH `u = &0 /\ v = &0 /\ w = &0 /\ z = &1`); (ASM_REAL_ARITH_TAC); (REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_LID; VECTOR_ADD_LID]); (ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN MESON_TAC[]); (EXISTS_TAC `(u / (u + v + w)) % u0 + (v / (u + v + w)) % u1 + (w / (u + v + w)) % u2:real^3`); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL; CONVEX_HULL_2;CONVEX_HULL_3; IN; IN_ELIM_THM] THEN REPEAT STRIP_TAC); (EXISTS_TAC `u / (u + v + w)`); (EXISTS_TAC `v / (u + v + w)`); (EXISTS_TAC `w / (u + v + w)`); (ASM_REWRITE_TAC[REAL_ARITH `a / x + b / x + c / x = (a + b + c) / x`]); (REPEAT STRIP_TAC); (MATCH_MP_TAC REAL_LE_DIV); (ASM_REAL_ARITH_TAC); (MATCH_MP_TAC REAL_LE_DIV); (ASM_REAL_ARITH_TAC); (MATCH_MP_TAC REAL_LE_DIV); (ASM_REAL_ARITH_TAC); (MATCH_MP_TAC REAL_DIV_REFL); (ASM_REAL_ARITH_TAC); (EXISTS_TAC `u + v + w:real`); (EXISTS_TAC `z:real`); (REPEAT STRIP_TAC); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (ASM_REWRITE_TAC[]); (REWRITE_TAC[VECTOR_ARITH `a % (x/ a % u0 + y / a % u1 + z / a % u2) = (a / a) % (x % u0) + (a / a) % (y % u1) + (a / a) % (z % u2)`]); (REWRITE_WITH `(u + v + w) / (u + v + w) = &1`); (ASM_SIMP_TAC [REAL_DIV_REFL]); (REWRITE_TAC[VECTOR_MUL_LID]); (VECTOR_ARITH_TAC); (UP_ASM_TAC THEN REPEAT STRIP_TAC); (* ======================================================================== *) (NEW_GOAL `(?k. k <= &1 /\ &0 <= k /\ projection (s2 - m) (p - m:real^3) = k % projection (s2 - m) (n - m))`); (MATCH_MP_TAC PARALLEL_PROJECTION); (ASM_REWRITE_TAC[]); (STRIP_TAC); (NEW_GOAL `s2 = m:real^3`); (ASM_REWRITE_TAC[]); (SWITCH_TAC THEN DEL_TAC); (NEW_GOAL `between s2 (u0, s1:real^3)`); (ASM_MESON_TAC[]); (NEW_GOAL `s2 IN affine hull {u0, s1:real^3}`); (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]); (STRIP_TAC); (NEW_GOAL `convex hull {u0,s1:real^3} SUBSET affine hull {u0,s1}`); (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]); (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]); (NEW_GOAL `affine hull {u0,s1,s2} = affine hull {u0, s1:real^3}`); (MATCH_MP_TAC AFFINE_HULLS_EQ); (REWRITE_TAC[SUBSET; SET_RULE `x IN {a,b,c} <=> x = a \/ x = b \/ x = c`]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]); (ASM_REWRITE_TAC[Trigonometry2.UV_IN_AFF2]); (ASM_MESON_TAC[]); (UP_ASM_TAC); (REWRITE_TAC[SUBSET; SET_RULE `x IN {b,c} <=> x = b \/ x = c`]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]); (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`); (STRIP_TAC); (REAL_ARITH_TAC); (VECTOR_ARITH_TAC); (REWRITE_TAC[ASSUME `x = s1:real^3`;AFFINE_HULL_3;IN;IN_ELIM_THM]); (EXISTS_TAC `&0` THEN EXISTS_TAC `&1` THEN EXISTS_TAC `&0`); (STRIP_TAC); (REAL_ARITH_TAC); (VECTOR_ARITH_TAC); (NEW_GOAL `aff_dim {u0,s1,s2:real^3} <= &1`); (ONCE_REWRITE_TAC[GSYM AFF_DIM_AFFINE_HULL]); (ONCE_ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[AFF_DIM_AFFINE_HULL]); (MATCH_MP_TAC (ARITH_RULE `(?x. x <= &1 /\ y <= x:int) ==> y <= &1`)); (EXISTS_TAC `&(CARD {u0,s1:real^3}):int - &1`); (STRIP_TAC); (REWRITE_TAC[ARITH_RULE `a:int - &1 <= &1 <=> a <= &2`; INT_OF_NUM_LE]); (REWRITE_TAC[Geomdetail.CARD2]); (MATCH_MP_TAC AFF_DIM_LE_CARD); (REWRITE_TAC[Geomdetail.FINITE6]); (NEW_GOAL `aff_dim {u0,s1,s2:real^3} = &2`); (NEW_GOAL `vl:(real^3)list = truncate_simplex 2 ul`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (REWRITE_WITH `aff_dim {u0,s1,s2:real^3} = aff_dim {omega_list_n V vl j | j IN 0..2}`); (AP_TERM_TAC); (REWRITE_TAC[IN_NUMSEG_0]); (REWRITE_TAC[SET_EQ_LEMMA; SET_RULE `x IN {a,b,c} <=> (x = a \/ x = b \/ x = c)`; IN;IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `0`); (REWRITE_TAC[ARITH_RULE `0 <= 2`; OMEGA_LIST_N]); (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]); (ASM_REWRITE_TAC[]); (EXISTS_TAC `1`); (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]); (EXPAND_TAC "vl"); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (DEL_TAC); (EXPAND_TAC "s1"); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]); (EXISTS_TAC `2`); (REWRITE_TAC[ARITH_RULE `2 <= 2`; ASSUME `x = s2:real^3`] THEN EXPAND_TAC "vl" THEN DEL_TAC); (EXPAND_TAC "s2"); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]); (REWRITE_TAC[set_of_list; OMEGA_LIST_TRUNCATE_2; OMEGA_LIST_TRUNCATE_2_NEW1]); (ASM_CASES_TAC `j = 0`); (DISJ1_TAC); (REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`; OMEGA_LIST_N; HD]); (EXPAND_TAC "vl"); (REWRITE_TAC[ASSUME `j = 0`]); (REWRITE_TAC[OMEGA_LIST_N; HD]); (ASM_CASES_TAC `j = 1`); (DISJ2_TAC); (DISJ1_TAC); (ASM_REWRITE_TAC[]); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; HD]); (EXPAND_TAC "s1"); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1; OMEGA_LIST_TRUNCATE_1_NEW1]); (ASM_CASES_TAC `j = 2`); (DISJ2_TAC); (DISJ2_TAC); (REWRITE_TAC[ASSUME `x:real^3 = omega_list_n V vl j`]); (EXPAND_TAC "vl"); (EXPAND_TAC "s2"); (REWRITE_TAC[ASSUME `j = 2`; OMEGA_LIST_TRUNCATE_2; OMEGA_LIST_TRUNCATE_2_NEW1]); (SUBGOAL_THEN `F` MP_TAC); (ASM_ARITH_TAC); (MESON_TAC[]); (MATCH_MP_TAC XNHPWAB3); (ASM_REWRITE_TAC[IN]); STRIP_TAC; (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `?h. h <= &1 /\ &0 <= h /\ projection (s2 - m1:real^3) (p - m1) = h % projection (s2 - m1) (s - m1)`); (MATCH_MP_TAC PARALLEL_PROJECTION); (ASM_REWRITE_TAC[]); (STRIP_TAC); (NEW_GOAL `s2 = m1:real^3`); (ASM_REWRITE_TAC[]); (SWITCH_TAC THEN DEL_TAC); (NEW_GOAL `between p (s2, s:real^3)`); (ASM_MESON_TAC[]); (NEW_GOAL `between p (s3, s2:real^3)`); (MATCH_MP_TAC BETWEEN_TRANS); (EXISTS_TAC `s:real^3`); (STRIP_TAC); (ASM_MESON_TAC[BETWEEN_SYM]); (ASM_MESON_TAC[BETWEEN_SYM]); (NEW_GOAL `p:real^3 IN B5`); (EXPAND_TAC "B5"); (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]); (EXPAND_TAC "s2"); (EXPAND_TAC "s3"); (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (MESON_TAC[SET_RULE `{a,b} = {b, a}`]); (NEW_GOAL `~(p:real^3 IN B5)`); (ASM_SET_TAC[IN_DIFF]); (ASM_MESON_TAC[]); (FIRST_X_ASSUM CHOOSE_TAC); (FIRST_X_ASSUM CHOOSE_TAC); (NEW_GOAL `projection (s2 - m1) (s - m1) = s - s2:real^3`); (REWRITE_TAC[projection; VECTOR_ARITH `a - b - x % (d - b) = a - d <=> (&1 - x) % (d - b:real^3) = vec 0`]); (REWRITE_WITH `&1 - ((s - m1) dot (s2 - m1:real^3)) / ((s2 - m1) dot (s2 - m1)) = &0`); (REWRITE_TAC[REAL_ARITH `&1 - a = &0 <=> a = &1`]); (REWRITE_WITH `((s - m1) dot (s2 - m1)) / ((s2 - m1) dot (s2 - m1)) = &1 <=> ((s - m1) dot (s2 - m1)) = &1 * ((s2 - m1) dot (s2 - m1:real^3))`); (MATCH_MP_TAC REAL_EQ_LDIV_EQ); (REWRITE_TAC[GSYM NORM_POW_2; GSYM Trigonometry2.NOT_ZERO_EQ_POW2_LT; NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]); (STRIP_TAC); (NEW_GOAL `between p (s2, s:real^3)`); (ASM_MESON_TAC[]); (NEW_GOAL `between p (s3, s2:real^3)`); (MATCH_MP_TAC BETWEEN_TRANS); (EXISTS_TAC `s:real^3`); (STRIP_TAC); (ASM_MESON_TAC[BETWEEN_SYM]); (ASM_MESON_TAC[BETWEEN_SYM]); (NEW_GOAL `p:real^3 IN B5`); (EXPAND_TAC "B5"); (UP_ASM_TAC THEN REWRITE_TAC[BETWEEN_IN_CONVEX_HULL]); (EXPAND_TAC "s2"); (EXPAND_TAC "s3"); (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (MESON_TAC[SET_RULE `{a,b} = {b, a}`]); (NEW_GOAL `~(p:real^3 IN B5)`); (ASM_SET_TAC[IN_DIFF]); (ASM_MESON_TAC[]); (REWRITE_TAC[REAL_MUL_LID]); (ONCE_REWRITE_TAC[REAL_ARITH `a = b <=> a - b = &0`]); (REWRITE_TAC[VECTOR_ARITH `(s - m1) dot r - (s2 - m1) dot r = (s - s2) dot r:real^3`]); (REWRITE_WITH `(s - s2) dot (s2 - m1) = --((s - s2) dot (m1 - s2:real^3))`); (VECTOR_ARITH_TAC); (ONCE_REWRITE_TAC[REAL_ARITH `-- a = &0 <=> a = &0`]); (UNDISCH_TAC `between s (s2,s3:real^3)`); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;IN;IN_ELIM_THM; CONVEX_HULL_2]); (REPEAT STRIP_TAC); (REWRITE_TAC[ASSUME `s = u' % s2 + v' % s3:real^3`]); (REWRITE_WITH `(u' % s2 + v' % s3) - s2:real^3 = (u' % s2 + v' % s3) - (u' + v') % s2`); (ASM_REWRITE_TAC[VECTOR_MUL_LID]); (REWRITE_TAC[VECTOR_ARITH `(u' % s2 + v' % s3) - (u' + v') % s2 = v' % (s3 - s2)`; DOT_LMUL]); (REWRITE_WITH `(s3 - s2) dot (m1 - s2:real^3) = &0`); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC MHFTTZN4); (EXISTS_TAC `V:real^3->bool`); (EXISTS_TAC `2`); (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`); (EXPAND_TAC "vl" THEN DEL_TAC); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3`); (ASM_MESON_TAC[ARITH_RULE `2 <= 3`]); (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1); (ONCE_ASM_REWRITE_TAC[]); (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]); (UNDISCH_TAC `m1 IN convex hull {u0, u1, u2:real^3}`); (NEW_GOAL `convex hull {u0, u1, u2:real^3} SUBSET affine hull {u0, u1, u2:real^3}`); (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]); (UP_ASM_TAC THEN SET_TAC[]); (REAL_ARITH_TAC); (VECTOR_ARITH_TAC); (ABBREV_TAC `M = projection (s2 - m1) (p - m1:real^3)`); (ABBREV_TAC `N = projection (s2 - m) (p - m:real^3)`); (NEW_GOAL `M = N:real^3`); (NEW_GOAL `?r. N = r % M:real^3`); (ASM_REWRITE_TAC[]); (NEW_GOAL `projection (s2 - m) (n - m:real^3) = n - s2`); (REWRITE_TAC[projection_proj_point; ASSUME `n' = s2 - m:real^3`; ASSUME `proj_point (s2 - m) (n - m) = n':real^3`]); (VECTOR_ARITH_TAC); (REWRITE_WITH `circumcenter (set_of_list vl) = s2:real^3`); (ASM_MESON_TAC[]); (REWRITE_TAC[ASSUME `projection (s2 - m) (n - m) = n - s2:real^3`]); (UNDISCH_TAC `between n (s2,s3:real^3)`); (UNDISCH_TAC `between s (s2,s3:real^3)`); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]); (REPEAT STRIP_TAC); (REWRITE_TAC[ASSUME `n = u'' % s2 + v'' % s3:real^3`; ASSUME `s = u' % s2 + v' % s3:real^3`]); (REWRITE_WITH `(u' % s2 + v' % s3) - s2:real^3 = (u' % s2 + v' % s3) - (u' + v') % s2 /\ (u'' % s2 + v'' % s3) - s2 = (u'' % s2 + v'' % s3) - (u'' + v'') % s2`); (ASM_REWRITE_TAC[VECTOR_MUL_LID]); (REWRITE_TAC[VECTOR_ARITH `(u % s + v % r) - (u + v) % s = v % (r - s)`]); (REWRITE_TAC[VECTOR_MUL_ASSOC]); (REWRITE_TAC[VECTOR_ARITH `a % x = b % x <=> (a - b) % x = vec 0`]); (REWRITE_TAC[REAL_ARITH `(r * h) * v' = r * (h * v')`]); (ASM_CASES_TAC `h * v' = &0`); (NEW_GOAL `F`); (ASM_CASES_TAC `h = &0`); (NEW_GOAL `M:real^3 = vec 0`); (ASM_REWRITE_TAC[VECTOR_MUL_LZERO]); (UP_ASM_TAC THEN EXPAND_TAC "M" THEN REWRITE_TAC[projection]); (ABBREV_TAC `kts = ((p - m1) dot (s2 - m1)) / ((s2 - m1) dot (s2 - m1:real^3))`); (REWRITE_TAC [VECTOR_ARITH `a - p - c = vec 0 <=> a = p + c`]); (STRIP_TAC); (NEW_GOAL `p IN affine hull {u0,u1,u2:real^3}`); (REWRITE_TAC[ASSUME `p = m1 + kts % (s2 - m1:real^3)`]); (MATCH_MP_TAC TRANSLATE_AFFINE_KY_LEMMA1); (REWRITE_TAC[MESON[] `A /\ B /\ A <=> A /\ B`]); (STRIP_TAC); (NEW_GOAL `convex hull {u0,u1,u2:real^3} SUBSET affine hull {u0, u1, u2}`); (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]); (UNDISCH_TAC `m1 IN convex hull {u0, u1, u2:real^3}`); (UP_ASM_TAC THEN SET_TAC[]); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl"); (REWRITE_TAC[set_of_list]); (MATCH_MP_TAC Rogers.OAPVION1); (STRIP_TAC); (SET_TAC[]); (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT); (EXISTS_TAC `V:real^3->bool`); (EXISTS_TAC `2`); (ASM_REWRITE_TAC[]); (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl"); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (MATCH_MP_TAC Packing3. TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (NEW_GOAL `~(p:real^3 IN B6)`); (ASM_SET_TAC[IN_DIFF]); (UP_ASM_TAC THEN EXPAND_TAC "B6"); (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;HD;TL]); (ASM_REWRITE_TAC[]); (NEW_GOAL `v' = &0`); (ASM_MESON_TAC[REAL_ENTIRE]); (NEW_GOAL `s = s2:real^3`); (ASM_REWRITE_TAC[]); (REWRITE_WITH `u' = &1`); (ASM_REAL_ARITH_TAC); (REWRITE_TAC[VECTOR_MUL_LID]); (VECTOR_ARITH_TAC); (NEW_GOAL `!w. w IN {u0,u1,u2:real^3} ==> radV {u0,u1,u2} = dist (circumcenter {u0,u1,u2},w)`); (MATCH_MP_TAC Rogers.OAPVION2); (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT); (EXISTS_TAC `V:real^3->bool`); (EXISTS_TAC `2`); (ASM_REWRITE_TAC[]); (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3`); (ASM_REWRITE_TAC[]); (ARITH_TAC); (NEW_GOAL `hl (truncate_simplex 2 (ul:(real^3)list)) = dist (s2, u0:real^3)`); (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list; HL]); (REWRITE_WITH `s2 = circumcenter {u0,u1,u2:real^3}`); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (FIRST_ASSUM MATCH_MP_TAC); (SET_TAC[]); (NEW_GOAL `hl (truncate_simplex 2 (ul:(real^3)list)) = sqrt (&2)`); (ONCE_ASM_REWRITE_TAC[]); (REWRITE_TAC[GSYM (ASSUME `s = s2:real^3`)]); (ONCE_REWRITE_TAC[DIST_SYM]); (ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (UP_ASM_TAC THEN MESON_TAC[]); (EXISTS_TAC `(k * v'') / (h * v')`); (REWRITE_TAC[REAL_ARITH `k * v'' - (k * v'') / (h * v') * h * v' = (k * v'') * (&1 - (h * v') / (h * v'))`]); (REWRITE_WITH `(h * v') / (h * v') = &1`); (MATCH_MP_TAC REAL_DIV_REFL); (ASM_REWRITE_TAC[]); (REWRITE_TAC[REAL_SUB_REFL;REAL_MUL_RZERO; VECTOR_MUL_LZERO]); (FIRST_X_ASSUM CHOOSE_TAC); (NEW_GOAL `r = &1`); (ASM_CASES_TAC `r = &1`); (ASM_REWRITE_TAC[]); (NEW_GOAL `p IN affine hull {u0,u1,u2:real^3}`); (MATCH_MP_TAC IN_AFFINE_HULL_KY_LEMMA3_alt); (EXISTS_TAC `M:real^3`); (EXISTS_TAC `r:real`); (REWRITE_WITH `p - M = (m1:real^3) + proj_point (s2 - m1) (p - m1)`); (EXPAND_TAC "M" THEN REWRITE_TAC[proj_point]); (VECTOR_ARITH_TAC); (REWRITE_WITH `p - r % M =(m:real^3) + proj_point (s2 - m) (p - m)`); (REWRITE_TAC[GSYM (ASSUME `N = r % M:real^3`)]); (EXPAND_TAC "N" THEN REWRITE_TAC[proj_point]); (VECTOR_ARITH_TAC); (REWRITE_TAC[PRO_EXP]); (REPEAT STRIP_TAC); (MATCH_MP_TAC TRANSLATE_AFFINE_KY_LEMMA1 ); (REWRITE_TAC[MESON[] `A /\ B /\ A <=> A /\ B`]); (REPEAT STRIP_TAC); (NEW_GOAL `convex hull {u0,u1,u2} SUBSET affine hull {u0,u1,u2:real^3}`); (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]); (UP_ASM_TAC THEN UNDISCH_TAC `m1:real^3 IN convex hull {u0,u1,u2}` THEN SET_TAC[]); (ASM_REWRITE_TAC[]); (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (MATCH_MP_TAC Rogers.BARV_CIRCUMCENTER_EXISTS); (EXISTS_TAC `V:real^3->bool`); (EXISTS_TAC `2`); (ASM_REWRITE_TAC[]); (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (MATCH_MP_TAC TRANSLATE_AFFINE_KY_LEMMA1); (REWRITE_TAC[MESON[] `A/\B/\A <=> A/\B`]); (STRIP_TAC); (MATCH_MP_TAC IN_AFFINE_HULL_3_KY_LEMMA2); (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `s1:real^3`); (REPEAT STRIP_TAC); (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1); (SET_TAC[]); (MATCH_MP_TAC (SET_RULE`(?s. s SUBSET b /\ a IN s) ==> a IN b`)); (EXISTS_TAC `convex hull {u0, u1,u2:real^3}`); (REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]); (MATCH_MP_TAC (SET_RULE`(?s. s SUBSET b /\ a IN s) ==> a IN b`)); (EXISTS_TAC `convex hull {u0, u1:real^3}`); (STRIP_TAC); (MATCH_MP_TAC CONVEX_HULL_SUBSET); (SET_TAC[]); (REWRITE_WITH `{u0, u1:real^3} = set_of_list [u0;u1]`); (REWRITE_TAC[set_of_list]); (EXPAND_TAC "s1"); (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 = omega_list V [u0;u1:real^3]`); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]); (MATCH_MP_TAC XNHPWAB2); (EXISTS_TAC `1`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (REWRITE_TAC[IN]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]); (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`); (EXPAND_TAC "vl"); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (MATCH_MP_TAC (REAL_ARITH `(?s. s < b /\ a <= s) ==> a < b`)); (EXISTS_TAC `hl (vl:(real^3)list)`); (STRIP_TAC); (REWRITE_WITH `vl = truncate_simplex 2 (ul:(real^3)list)`); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl"); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC Rogers.HL_DECREASE); (EXISTS_TAC `V:real^3->bool`); (EXISTS_TAC `2`); (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`;IN]); (REWRITE_WITH `vl = truncate_simplex 2 (ul:(real^3)list)`); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl"); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (MATCH_MP_TAC Rogers.BARV_CIRCUMCENTER_EXISTS); (EXISTS_TAC `V:real^3->bool`); (EXISTS_TAC `2`); (ASM_REWRITE_TAC[]); (REWRITE_WITH `vl:(real^3)list = truncate_simplex 2 ul`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[ARITH_RULE `2 <= 3`]); (ASM_MESON_TAC[]); (NEW_GOAL `~(p:real^3 IN B6)`); (ASM_SET_TAC[IN_DIFF]); (UP_ASM_TAC THEN EXPAND_TAC "B6"); (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`;HD;TL]); (STRIP_TAC); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (REWRITE_TAC[ASSUME `N = r % M:real^3`; ASSUME `r = &1`]); (VECTOR_ARITH_TAC); (NEW_GOAL `norm (M:real^3) <= norm (s2 - s:real^3)`); (REWRITE_WITH `norm (s2 - s:real^3) = norm (projection (s2 - m1) (s - m1))`); (REWRITE_WITH `norm (s2 - s:real^3) = norm (s - s2)`); (NORM_ARITH_TAC); (AP_TERM_TAC); (ASM_MESON_TAC[]); (REWRITE_TAC[ASSUME `h <= &1 /\ &0 <= h /\ M = h % projection (s2 - m1) (s - m1:real^3)`]); (REWRITE_TAC[NORM_MUL;REAL_ARITH `a * b <= b <=> &0 <= b * (&1 - a)`]); (MATCH_MP_TAC REAL_LE_MUL); (REWRITE_TAC[NORM_POS_LE; REAL_ARITH `&0 <= a - b <=> b <= a`]); (REWRITE_WITH `abs h = h`); (REWRITE_TAC[REAL_ABS_REFL]); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (NEW_GOAL `norm (s2 - s:real^3) < norm (N:real^3) `); (REWRITE_WITH `norm (s2 - s:real^3) < norm (N:real^3) <=> norm (s2 - s) pow 2 < norm (N:real^3) pow 2`); (MATCH_MP_TAC Pack1.bp_bdt); (REWRITE_TAC[NORM_POS_LE]); (REWRITE_WITH `norm (N:real^3) = norm ((p' + m) - p:real^3)`); (REWRITE_TAC[GSYM (ASSUME `projection (s2 - m) (p - m) = N:real^3`)]); (REWRITE_TAC[projection_proj_point]); (REWRITE_TAC[ASSUME `proj_point (s2 - m) (p - m) = p':real^3`]); (NORM_ARITH_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `norm (s2 - s:real^3) < norm (M:real^3)`); (ASM_MESON_TAC[]); (ASM_REAL_ARITH_TAC); (SET_TAC[]); (* ======================================================================= *) (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 0`); (REPEAT STRIP_TAC); (NEW_GOAL `~(y = 4 \/ y = 1 \/ y = 2 \/ y = 3)`); (ASM_SIMP_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `i = 0`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_SIMP_TAC[]); (REWRITE_TAC[ASSUME `i = 0`]); (ASM_REWRITE_TAC[]); (* ====================================================================== *) (NEW_GOAL `dist (u0, p:real^3) < sqrt (&2)`); (UP_ASM_TAC THEN REAL_ARITH_TAC); (ASM_CASES_TAC `~(p IN rcone_gt (HD (ul:(real^3)list)) (HD (TL ul)) (hl (truncate_simplex 1 ul) / sqrt (&2))) `); (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> ~ (y = 4 \/ y = 0 \/ y = 2 \/ y = 3)`); (REPEAT STRIP_TAC); (NEW_GOAL `mcell 4 V ul = {}`); (SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (REFL_TAC); (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 4`]); (REWRITE_TAC[ASSUME `mcell 4 V ul = {}`]); (SET_TAC[]); (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 0`; MCELL_EXPLICIT;mcell0]); (STRIP_TAC); (NEW_GOAL `~(p:real^3 IN ball (HD ul,sqrt (&2)))`); (ASM_SET_TAC[IN_DIFF]); (UP_ASM_TAC THEN ASM_REWRITE_TAC[HD;IN;ball;IN_ELIM_THM]); (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 2`; MCELL_EXPLICIT;mcell2]); (COND_CASES_TAC); (LET_TAC); (REWRITE_TAC[IN_INTER]); (REPEAT STRIP_TAC); (NEW_GOAL `p:real^3 IN rcone_gt (HD ul) (HD (TL ul)) a`); (REWRITE_TAC[RCONE_GT_GE;IN_DIFF]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[HD;TL;IN;IN_ELIM_THM]); (STRIP_TAC); (NEW_GOAL `~(p:real^3 IN B3)`); (ASM_SET_TAC[IN_DIFF]); (UP_ASM_TAC THEN EXPAND_TAC "B3" THEN REWRITE_TAC[rcone_eq;rconesgn]); (ASM_REWRITE_TAC[HD;TL;IN;IN_ELIM_THM;dist]); (ASM_MESON_TAC[]); (SET_TAC[]); (* ======================================================================= *) (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 3`; MCELL_EXPLICIT;mcell3]); (COND_CASES_TAC); (NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\ dist (u0,s) = sqrt (&2) /\ mxi V ul = s:real^3)`); (MATCH_MP_TAC MXI_EXPLICIT_OLD); (ASM_REWRITE_TAC[]); (FIRST_X_ASSUM CHOOSE_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]); (REWRITE_TAC[SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]); (STRIP_TAC); (SUBGOAL_THEN `p:real^3 IN rogers V ul` MP_TAC); (ASM_SET_TAC[IN_DIFF]); (ASM_SIMP_TAC[ROGERS_EXPLICIT; HD]); (ABBREV_TAC `s1 = omega_list_n V [u0; u1; u2; u3:real^3] 1`); (ABBREV_TAC `s2 = omega_list_n V [u0; u1; u2; u3:real^3] 2`); (ABBREV_TAC `s3 = omega_list_n V [u0; u1; u2; u3:real^3] 3`); (STRIP_TAC); (ABBREV_TAC `vl = [u0;u1;u2:real^3]`); (NEW_GOAL `vl = truncate_simplex 2 ul:(real^3)list`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2] THEN EXPAND_TAC "vl"); (NEW_GOAL `barV V 2 vl`); (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_MESON_TAC[ARITH_RULE `2 <= 3`]); (NEW_GOAL `LENGTH (vl:(real^3)list) = 3 /\ CARD {u0,u1,u2:real^3} = 3`); (REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (REWRITE_TAC[ARITH_RULE `3 = 2 + 1`]); (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (NEW_GOAL `s2:real^3 = omega_list V vl`); (EXPAND_TAC "s2" THEN EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (MESON_TAC[OMEGA_LIST_TRUNCATE_2]); (NEW_GOAL `s2 = circumcenter {u0,u1,u2:real^3}`); (REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (REWRITE_TAC[ASSUME `s2 = omega_list V vl`]); (MATCH_MP_TAC Rogers.XNHPWAB1); (EXISTS_TAC `2` THEN REWRITE_TAC[IN]); (ASM_REWRITE_TAC[]); (ASM_MESON_TAC[]); (NEW_GOAL `dist (s2,u0:real^3) = hl (truncate_simplex 2 (ul:(real^3)list))`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (REWRITE_TAC[GSYM (ASSUME `vl:(real^3)list = truncate_simplex 2 ul`)]); (REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]); (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (REWRITE_WITH `u0:real^3 = HD vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]); (MATCH_MP_TAC Rogers.HL_EQ_DIST0); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`); (ASM_REWRITE_TAC[]); (NEW_GOAL `~(s = s2:real^3)`); (STRIP_TAC); (NEW_GOAL `dist (u0,s:real^3) < sqrt (&2)`); (ONCE_REWRITE_TAC[DIST_SYM]); (REWRITE_TAC[ASSUME `s = s2:real^3`]); (ASM_MESON_TAC[]); (ASM_REAL_ARITH_TAC); (NEW_GOAL `(s2:real^3) IN voronoi_list V vl`); (SIMP_TAC[ASSUME `s2 = omega_list V vl`]); (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST); (EXISTS_TAC `2`); (ASM_REWRITE_TAC[]); (NEW_GOAL `(s3:real^3) IN voronoi_list V ul`); (REWRITE_WITH `s3 = omega_list V ul`); (EXPAND_TAC "s3" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; OMEGA_LIST]); (REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) - 1 = 3`]); (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST); (EXISTS_TAC `3`); (ASM_REWRITE_TAC[]); (NEW_GOAL `(s3:real^3) IN voronoi_list V vl`); (MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET A) ==> a IN A`)); (EXISTS_TAC `voronoi_list V ul`); (STRIP_TAC); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (REWRITE_TAC[VORONOI_LIST;VORONOI_SET;voronoi_closed;set_of_list; SUBSET; IN_INTERS]); (ONCE_REWRITE_TAC[IN]); (REWRITE_TAC[IN_ELIM_THM]); (REPEAT STRIP_TAC); (FIRST_ASSUM MATCH_MP_TAC); (EXISTS_TAC `v:real^3`); (ASM_REWRITE_TAC[]); (UNDISCH_TAC `v IN {u0, u1, u2:real^3}`); (SET_TAC[]); (NEW_GOAL `s IN voronoi_list V vl`); (NEW_GOAL `convex (voronoi_list V vl)`); (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]); (UP_ASM_TAC THEN REWRITE_TAC[convex] THEN STRIP_TAC); (UNDISCH_TAC `between s (s2,s3:real^3)`); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]); (REPEAT STRIP_TAC); (ONCE_REWRITE_TAC[GSYM IN]); (REWRITE_TAC[ASSUME `s = u % s2 + v % s3:real^3`]); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `~ (s IN affine hull {u0,u1,u2:real^3})`); STRIP_TAC; (NEW_GOAL `(s:real^3 - s2) dot (s - s2) = &0`); (REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]); (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (MATCH_MP_TAC MHFTTZN4); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (ASM_SIMP_TAC[IN_AFFINE_KY_LEMMA1]); (EXPAND_TAC "vl" THEN ASM_MESON_TAC[set_of_list]); (UP_ASM_TAC THEN REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0; NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]); (ASM_REWRITE_TAC[]); (NEW_GOAL `CARD {u0, u1, u2, s:real^3} = 4`); (ONCE_REWRITE_TAC[SET_RULE `{u0, u1, u2, s} = {s, u0, u1, u2}`]); (REWRITE_WITH `4 = SUC (CARD {u0,u1,u2:real^3})`); (ASM_REWRITE_TAC[]); (ARITH_TAC); (MATCH_MP_TAC (MESON[Geomdetail.CARD_CLAUSES_IMP] `!s a. FINITE s /\ ~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s)`)); (REWRITE_TAC[Geomdetail.FINITE6]); (STRIP_TAC); (NEW_GOAL `s IN affine hull {u0, u1, u2:real^3}`); (UP_ASM_TAC THEN REWRITE_TAC[IN_AFFINE_KY_LEMMA1]); (ASM_MESON_TAC[]); (NEW_GOAL `~affine_dependent {u0, u1, u2, s:real^3}`); (ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {d,a,b,c}`]); (MATCH_MP_TAC AFFINE_INDEPENDENT_INSERT); (ASM_REWRITE_TAC[]); (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2` THEN ASM_REWRITE_TAC[]); (NEW_GOAL `s2 IN convex hull {u0, u1, u2:real^3}`); (REWRITE_WITH `s2 = omega_list V vl /\ {u0, u1, u2:real^3} = set_of_list vl`); (EXPAND_TAC "s2" THEN EXPAND_TAC "vl"); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_2;set_of_list]); (MATCH_MP_TAC Rogers.XNHPWAB2); (EXISTS_TAC `2`); (ASM_REWRITE_TAC[IN]); (ASM_MESON_TAC[]); (NEW_GOAL `s1 = inv (&2) % (u0 + u1:real^3)`); (ONCE_REWRITE_TAC[GSYM midpoint]); (EXPAND_TAC "s1"); (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 = omega_list_n V [u0; u1:real^3] 1`); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2;OMEGA_LIST_TRUNCATE_1]); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW2]); (REWRITE_WITH `omega_list V [u0; u1:real^3] = circumcenter (set_of_list [u0;u1])`); (MATCH_MP_TAC XNHPWAB1); (EXISTS_TAC `1`); (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]); (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (REWRITE_TAC[IN] THEN STRIP_TAC); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `2` THEN REWRITE_TAC[ARITH_RULE `1 <= 2`]); (ASM_REWRITE_TAC[]); (NEW_GOAL `!i j. i < j /\ j <= 2 ==> hl (truncate_simplex i (vl:(real^3)list)) < hl (truncate_simplex j vl)`); (MATCH_MP_TAC XNHPWAB4); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[IN]); (ASM_MESON_TAC[]); (NEW_GOAL `hl (truncate_simplex 1 (vl:(real^3)list)) < hl (truncate_simplex 2 vl)`); (FIRST_X_ASSUM MATCH_MP_TAC); (ARITH_TAC); (NEW_GOAL `truncate_simplex 2 vl = truncate_simplex 2 ul:(real^3)list`); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2]); (MATCH_MP_TAC (REAL_ARITH `a < hl (truncate_simplex 2 (vl:(real^3)list)) /\ hl (truncate_simplex 2 vl) < b ==> a < b`)); (ASM_REWRITE_TAC[]); (ASM_MESON_TAC[]); (REWRITE_TAC[set_of_list;Rogers.CIRCUMCENTER_2]); (NEW_GOAL `~(s3 IN affine hull {u0,u1,u2:real^3})`); (STRIP_TAC); (NEW_GOAL `(s3 - s2) dot (s3 - s2:real^3) = &0`); (REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]); (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (MATCH_MP_TAC MHFTTZN4); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (ASM_SIMP_TAC[IN_AFFINE_KY_LEMMA1]); (EXPAND_TAC "vl" THEN ASM_MESON_TAC[set_of_list]); (UP_ASM_TAC THEN REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0; NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]); (STRIP_TAC); (UNDISCH_TAC `between s (s2,s3:real^3)`); (REWRITE_TAC[ASSUME `s3= s2:real^3`; BETWEEN_REFL_EQ]); (ASM_REWRITE_TAC[]); (NEW_GOAL `p IN convex hull {u0, u1, s2, s:real^3}`); (MATCH_MP_TAC CONVEX_HULL_KY_LEMMA_5); (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `s3:real^3`); (REPEAT STRIP_TAC); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (NEW_GOAL `~(p:real^3 IN B4)`); (ASM_SET_TAC[IN_DIFF]); (UP_ASM_TAC THEN EXPAND_TAC "B4" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; HD;TL; ASSUME `mxi V [u0; u1; u2; u3] = s:real^3`]); (ASM_MESON_TAC[]); (REWRITE_TAC[IN_INTER; ASSUME `p IN convex hull {u0, u1, u2, s:real^3}`]); (UNDISCH_TAC `p IN convex hull {u0, s1, s2, s3:real^3}`); (REWRITE_TAC[ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`; CONVEX_HULL_4;IN;IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `u + v * inv (&2)`); (EXISTS_TAC `v * inv (&2)`); (EXISTS_TAC `w:real` THEN EXISTS_TAC `z:real`); (REPEAT STRIP_TAC); (MATCH_MP_TAC REAL_LE_ADD); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC REAL_LE_MUL); (ASM_REWRITE_TAC[]); (REAL_ARITH_TAC); (MATCH_MP_TAC REAL_LE_MUL); (ASM_REWRITE_TAC[]); (REAL_ARITH_TAC); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[REAL_ARITH `(u + v * inv (&2)) + v * inv (&2) + w + z = u + v + w + z`]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[ASSUME `p = u % u0 + v % inv (&2) % (u0 + u1) + w % s2 + z % s3:real^3`]); (VECTOR_ARITH_TAC); (* ========================================================================== *) (NEW_GOAL `?m n. between p (m,n) /\ between m (u0,u1) /\ between n (s2,s:real^3)`); (UP_ASM_TAC THEN REWRITE_TAC[CONVEX_HULL_4_IMP_2_2]); (UP_ASM_TAC THEN REPEAT STRIP_TAC); (NEW_GOAL `between m (u0, s1:real^3)`); (ASM_CASES_TAC `between m (u0, s1:real^3)`); (UP_ASM_TAC THEN MESON_TAC[]); (NEW_GOAL `between m (s1, u1:real^3)`); (NEW_GOAL `between m (u0, s1) \/ between m (s1, u1:real^3)`); (MATCH_MP_TAC BETWEEN_TRANS_3_CASES); (ASM_REWRITE_TAC[]); (REWRITE_TAC[GSYM midpoint;BETWEEN_MIDPOINT]); (ASM_MESON_TAC[]); (NEW_GOAL `F`); (NEW_GOAL `between n (s2,s3:real^3)`); (ONCE_REWRITE_TAC[BETWEEN_SYM]); (MATCH_MP_TAC BETWEEN_TRANS); (EXISTS_TAC `s:real^3`); (ONCE_REWRITE_TAC[BETWEEN_SYM]); (ASM_MESON_TAC[]); (UP_ASM_TAC THEN UP_ASM_TAC THEN UNDISCH_TAC `between p (m,n:real^3)`); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]); (REPEAT STRIP_TAC); (UNDISCH_TAC `p = u % m + v % n:real^3`); (REWRITE_TAC[ASSUME `m = u' % s1 + v' % u1:real^3`; ASSUME `n = u'' % s2 + v'' % s3:real^3`]); (REWRITE_WITH `u1 = &2 % s1 - u0:real^3`); (REWRITE_TAC[ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`]); (VECTOR_ARITH_TAC); (REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]); (REWRITE_TAC [VECTOR_ARITH `((u * u') % s1 + (u * v') % (&2 % s1 - u0)) + (v * u'') % s2 + (v * v'') % s3 = (u * (-- v')) % u0 + (u * u' + v' * &2 * u) % s1 + (v * u'') % s2 + (v * v'') % s3`]); (STRIP_TAC); (NEW_GOAL `u * --v' = &0`); (MATCH_MP_TAC AFFINE_DEPENDENT_KY_LEMMA1); (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `s1:real^3`); (EXISTS_TAC `s2:real^3` THEN EXISTS_TAC `s3:real^3`); (EXISTS_TAC `p:real^3`); (EXISTS_TAC `u * u' + v' * &2 * u`); (EXISTS_TAC `v * u''`); (EXISTS_TAC `v * v''`); (NEW_GOAL `~(affine_dependent {u0,s1,s2:real^3})`); (REWRITE_WITH `{u0,s1,s2:real^3} = {omega_list_n V vl i | i <= 2}`); (EXPAND_TAC "s1" THEN EXPAND_TAC "s2"); (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 = omega_list_n V vl 1`); (EXPAND_TAC "vl" THEN REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW1; OMEGA_LIST_TRUNCATE_1]); (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 2 = omega_list_n V vl 2`); (EXPAND_TAC "vl" THEN REWRITE_TAC[OMEGA_LIST_TRUNCATE_2_NEW1; OMEGA_LIST_TRUNCATE_2]); (REWRITE_WITH `u0 = omega_list_n V vl 0`); (REWRITE_TAC[OMEGA_LIST_N]); (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]); (REWRITE_TAC[OMEGA_LIST_UP_TO_2]); (MATCH_MP_TAC Rogers.AFFINE_INDEPENDENT_OMEGA_LIST_N); (ASM_MESON_TAC[]); (* ======================================================================== *) (NEW_GOAL `~affine_dependent {u0, s1, s2, s3:real^3}`); (ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {d,a,b,c}`]); (MATCH_MP_TAC AFFINE_INDEPENDENT_INSERT); STRIP_TAC; (ASM_REWRITE_TAC[]); (NEW_GOAL `~(s3 = s2:real^3)`); (STRIP_TAC); (UNDISCH_TAC `between s (s2,s3:real^3)`); (REWRITE_TAC[ASSUME `s3= s2:real^3`; BETWEEN_REFL_EQ]); (ASM_REWRITE_TAC[]); (STRIP_TAC); (NEW_GOAL `(s3 IN affine hull {u0,u1,u2:real^3})`); (UNDISCH_TAC `s2 IN convex hull {u0,u1,u2:real^3}` THEN UP_ASM_TAC THEN REWRITE_TAC[AFFINE_HULL_3; CONVEX_HULL_3; IN;IN_ELIM_THM; ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`]); (REPEAT STRIP_TAC); (REWRITE_TAC[ASSUME `s3 = u''' % u0 + v''' % inv (&2) % (u0 + u1) + w % s2:real^3`; ASSUME `s2 = u'''' % u0 + v'''' % u1 + w' % u2:real^3`]); (EXISTS_TAC `u''' + v''' * inv (&2) + w * u''''`); (EXISTS_TAC `v''' * inv (&2) + w * v''''`); (EXISTS_TAC `w * w'`); (STRIP_TAC); (REWRITE_TAC[REAL_ARITH `(u''' + v''' * inv (&2) + w * u'''') + (v''' * inv (&2) + w * v'''') + w * w' = (u''' + v''') + w * (u'''' + v'''' + w')`]); (ASM_REWRITE_TAC[REAL_ARITH `(a + b) + c * &1 = a + b + c`]); (VECTOR_ARITH_TAC); (ASM_MESON_TAC[]); (REPEAT STRIP_TAC); (ASM_MESON_TAC[]); (ONCE_REWRITE_TAC [SET_RULE `{u0, s1, s2, s3} = {s3,u0, s1, s2}`]); (NEW_GOAL `CARD {u0,s1,s2:real^3} = 3`); (REWRITE_WITH `{u0,s1,s2:real^3} = {omega_list_n V vl i | i <= 2}`); (EXPAND_TAC "s1" THEN EXPAND_TAC "s2"); (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 1 = omega_list_n V vl 1`); (EXPAND_TAC "vl" THEN REWRITE_TAC[OMEGA_LIST_TRUNCATE_1_NEW1; OMEGA_LIST_TRUNCATE_1]); (REWRITE_WITH `omega_list_n V [u0; u1; u2; u3] 2 = omega_list_n V vl 2`); (EXPAND_TAC "vl" THEN REWRITE_TAC[OMEGA_LIST_TRUNCATE_2_NEW1; OMEGA_LIST_TRUNCATE_2]); (REWRITE_WITH `u0 = omega_list_n V vl 0`); (REWRITE_TAC[OMEGA_LIST_N]); (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]); (REWRITE_TAC[OMEGA_LIST_UP_TO_2]); (REWRITE_WITH `{omega_list_n V vl i | i <= 2} = IMAGE (omega_list_n V vl) {i | i <= 2}`); (REWRITE_TAC[IMAGE]); (SET_TAC[]); (REWRITE_TAC[NUMSEG_LE]); (REWRITE_WITH `IMAGE (omega_list_n V vl) (0..2) = {omega_list_n V vl i | i IN (0..2)}`); (REWRITE_TAC[IMAGE]); (SET_TAC[]); (NEW_GOAL `aff_dim {omega_list_n V vl j | j IN 0..2} = &2`); (MATCH_MP_TAC XNHPWAB3); (ASM_MESON_TAC[IN]); (NEW_GOAL `aff_dim {omega_list_n V vl i | i IN 0..2} <= &(CARD {omega_list_n V vl i | i IN 0..2}) - &1`); (MATCH_MP_TAC AFF_DIM_LE_CARD); (REWRITE_WITH `{omega_list_n V vl i | i IN (0..2)} = IMAGE (omega_list_n V vl) (0..2)`); (REWRITE_TAC[IMAGE]); (SET_TAC[]); (REWRITE_TAC[GSYM NUMSEG_LE]); (REWRITE_WITH `IMAGE (omega_list_n V vl) {i | i <= 2} = {omega_list_n V vl i | i <= 2}`); (REWRITE_TAC[IMAGE]); (SET_TAC[]); (REWRITE_TAC[OMEGA_LIST_UP_TO_2;Geomdetail.FINITE6]); (UP_ASM_TAC THEN REWRITE_TAC[ARITH_RULE `a:int <= b - &1 <=> a + &1 <= b`]); (REWRITE_TAC[ASSUME `aff_dim {omega_list_n V vl j | j IN 0..2} = &2`; ARITH_RULE `&2 + &1 = &3:int`; INT_OF_NUM_LE]); (STRIP_TAC); (NEW_GOAL `CARD {omega_list_n V vl i | i IN 0..2} <= 3`); (REWRITE_WITH `{omega_list_n V vl i | i IN (0..2)} = IMAGE (omega_list_n V vl) (0..2)`); (REWRITE_TAC[IMAGE]); (SET_TAC[]); (REWRITE_TAC[GSYM NUMSEG_LE]); (REWRITE_WITH `IMAGE (omega_list_n V vl) {i | i <= 2} = {omega_list_n V vl i | i <= 2}`); (REWRITE_TAC[IMAGE]); (SET_TAC[]); (REWRITE_TAC[OMEGA_LIST_UP_TO_2; Geomdetail.CARD3]); (ASM_ARITH_TAC); (REWRITE_WITH `4 = SUC (CARD {u0, s1, s2:real^3})`); (ASM_REWRITE_TAC[]); (ARITH_TAC); (MATCH_MP_TAC (MESON[Geomdetail.CARD_CLAUSES_IMP] `!a s. FINITE s /\ ~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s)`)); (REWRITE_TAC[Geomdetail.FINITE6]); (STRIP_TAC); (NEW_GOAL `~(s3 IN affine hull {u0,s1,s2:real^3})`); (STRIP_TAC); (NEW_GOAL `(s3 IN affine hull {u0,u1,u2:real^3})`); (UNDISCH_TAC `s2 IN convex hull {u0,u1,u2:real^3}` THEN UP_ASM_TAC THEN REWRITE_TAC[AFFINE_HULL_3; CONVEX_HULL_3; IN;IN_ELIM_THM; ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`]); (REPEAT STRIP_TAC); (REWRITE_TAC[ASSUME `s3 = u''' % u0 + v''' % inv (&2) % (u0 + u1) + w % s2:real^3`; ASSUME `s2 = u'''' % u0 + v'''' % u1 + w' % u2:real^3`]); (EXISTS_TAC `u''' + v''' * inv (&2) + w * u''''`); (EXISTS_TAC `v''' * inv (&2) + w * v''''`); (EXISTS_TAC `w * w'`); (STRIP_TAC); (REWRITE_TAC[REAL_ARITH `(u''' + v''' * inv (&2) + w * u'''') + (v''' * inv (&2) + w * v'''') + w * w' = (u''' + v''') + w * (u'''' + v'''' + w')`]); (ASM_REWRITE_TAC[REAL_ARITH `(a + b) + c * &1 = a + b + c`]); (VECTOR_ARITH_TAC); (ASM_MESON_TAC[]); (NEW_GOAL `s3 IN affine hull {u0, s1, s2:real^3}`); (UNDISCH_TAC `s3 IN {u0, s1, s2:real^3}` THEN REWRITE_TAC [IN_AFFINE_KY_LEMMA1]); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (REWRITE_TAC[REAL_ARITH `u * --v' + (u * u' + v' * &2 * u) + v * u'' + v * v'' = u * (u' + v') + v * (u'' + v'')`]); (ASM_REWRITE_TAC[REAL_MUL_RID]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[REAL_ARITH `a * (-- b) <= &0 <=> &0 <= a * b`]); (ASM_SIMP_TAC[REAL_LE_MUL]); (NEW_GOAL `p IN affine hull {s1, s2, s3:real^3}`); (REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]); (EXISTS_TAC `u * u' + v' * &2 * u`); (EXISTS_TAC `v * u''`); (EXISTS_TAC `v * v''`); (STRIP_TAC); (REWRITE_TAC[REAL_ARITH `(u * u' + v' * &2 * u) + v * u'' + v * v'' = (u * (u' + v') + v * (u'' + v'')) - (u * -- v')`]); (ASM_REWRITE_TAC[REAL_MUL_RID]); (REAL_ARITH_TAC); (ASM_REWRITE_TAC[]); (VECTOR_ARITH_TAC); (NEW_GOAL `~(p:real^3 IN B7)`); (ASM_SET_TAC[IN_DIFF]); (UP_ASM_TAC THEN EXPAND_TAC "B7"); (UP_ASM_TAC THEN EXPAND_TAC "s1" THEN EXPAND_TAC "s2" THEN EXPAND_TAC "s3"); (REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (UP_ASM_TAC THEN MESON_TAC[]); (* ========================================================================= *) (NEW_GOAL `?q. between p (u0,q) /\ between q (n,s1:real^3)`); (UNDISCH_TAC `between p (m,n:real^3)` THEN UP_ASM_TAC); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;IN;IN_ELIM_THM; CONVEX_HULL_2]); (REPEAT STRIP_TAC); (EXISTS_TAC `((u' * v) / (u' * v + v')) % s1 + (v' / (u' * v + v')) % n:real^3`); (NEW_GOAL `~((u' * v + v') = &0)`); (STRIP_TAC); (NEW_GOAL `p = u0:real^3`); (ASM_REWRITE_TAC[]); (NEW_GOAL `u' * v = &0 /\ v' = &0`); (NEW_GOAL `&0 <= u' * v /\ &0 <= v'`); (ASM_SIMP_TAC [REAL_LE_MUL]); (ASM_REAL_ARITH_TAC); (NEW_GOAL `u' * u = &1`); (NEW_GOAL `u' * u + (u' * v + v') = &1`); (REWRITE_TAC[REAL_ARITH `u' * u + (u' * v + v') = u' * (u + v) + v'`]); (ASM_MESON_TAC[REAL_MUL_RID]); (ASM_REAL_ARITH_TAC); (REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]); (ONCE_REWRITE_TAC[REAL_ARITH `a * b * c = (a * b) * c`]); (ASM_REWRITE_TAC[]); (VECTOR_ARITH_TAC); (NEW_GOAL `~(p:real^3 IN B6)`); (ASM_SET_TAC[IN_DIFF]); (UP_ASM_TAC THEN EXPAND_TAC "B6" THEN REWRITE_TAC[ ASSUME `ul = [u0;u1;u2;u3:real^3]`; HD; TL]); (REWRITE_TAC[ASSUME `p = u0:real^3`; AFFINE_HULL_3;IN;IN_ELIM_THM]); (EXISTS_TAC `&1` THEN EXISTS_TAC `&0` THEN EXISTS_TAC `&0`); (STRIP_TAC); (REAL_ARITH_TAC); (VECTOR_ARITH_TAC); (STRIP_TAC); (EXISTS_TAC `u' * u`); (EXISTS_TAC `u' * v + v'`); (REPEAT STRIP_TAC); (ASM_SIMP_TAC[REAL_LE_MUL]); (ASM_SIMP_TAC[REAL_LE_ADD;REAL_LE_MUL]); (ASM_REWRITE_TAC[REAL_ARITH `u' * u + u' * v + v' = u' * (u + v) + v'`; REAL_MUL_RID]); (REWRITE_TAC[ASSUME `p = u' % m + v' % n:real^3`; ASSUME `m = u % u0 + v % s1:real^3`;VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]); (REWRITE_TAC[VECTOR_ARITH `((u' * v + v') * (u' * v) / (u' * v + v')) % s1 = ((u' * v + v') / (u' * v + v')) % ((u' * v) % s1)`]); (REWRITE_TAC[VECTOR_ARITH `((u' * v + v') * v' / (u' * v + v')) % n = ((u' * v + v') / (u' * v + v')) % (v' % n)`]); (REWRITE_TAC[VECTOR_ARITH `(x + a % y) + b % z = x + m % a % y + m % b % z <=> (m - &1) % (a % y + b % z )= vec 0`]); (REWRITE_WITH `(u' * v + v') / (u' * v + v') = &1`); (MATCH_MP_TAC REAL_DIV_REFL); (ASM_REWRITE_TAC[]); (VECTOR_ARITH_TAC); (EXISTS_TAC `v' / (u' * v + v')`); (EXISTS_TAC `(u' * v) / (u' * v + v')`); (REPEAT STRIP_TAC); (ASM_SIMP_TAC[REAL_LE_DIV;REAL_LE_ADD;REAL_LE_MUL]); (ASM_SIMP_TAC[REAL_LE_DIV;REAL_LE_ADD;REAL_LE_MUL]); (REWRITE_TAC[REAL_ARITH `a / x + b / x = (b + a) / x`]); (MATCH_MP_TAC REAL_DIV_REFL); (ASM_REWRITE_TAC[]); (VECTOR_ARITH_TAC); (UP_ASM_TAC THEN REPEAT STRIP_TAC); (* ========================================================================= *) (UNDISCH_TAC `~(p:real^3 IN rcone_gt (HD ul) (HD (TL ul)) (hl (truncate_simplex 1 ul) / sqrt (&2)))`); (ASM_REWRITE_TAC[HD;TL]); (REWRITE_WITH `hl (truncate_simplex 1 [u0; u1; u2; u3:real^3]) = dist (s1, u0)`); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (REWRITE_WITH `dist (s1,u0) = dist (circumcenter (set_of_list [u0;u1:real^3]), HD [u0;u1:real^3])`); (REWRITE_TAC[HD; set_of_list; Rogers.CIRCUMCENTER_2]); (ASM_REWRITE_TAC[midpoint]); (MATCH_MP_TAC Rogers.HL_EQ_DIST0); (EXISTS_TAC `V:real^3->bool`); (EXISTS_TAC `1`); (ASM_REWRITE_TAC[]); (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `2`); (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]); (NEW_GOAL `q:real^3 IN rcone_ge u0 u1 (dist (s1,u0) / sqrt (&2))`); (REWRITE_TAC[rcone_ge; rconesgn;IN;IN_ELIM_THM]); (REWRITE_WITH `(q - u0) dot (u1 - u0) = (q - s1) dot (u1 - u0) + (s1 - u0) dot (u1 - u0:real^3)`); (VECTOR_ARITH_TAC); (REWRITE_WITH `(q - s1) dot (u1 - u0:real^3) = &0`); (REWRITE_WITH `u1 - u0 = (-- &2) % (u0:real^3 - s1)`); (ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC); (REWRITE_TAC[DOT_RMUL]); (REWRITE_WITH `(q - s1) dot (u0 - s1:real^3) = &0`); (REWRITE_WITH `s1 = circumcenter (set_of_list [u0;u1:real^3])`); (ASM_REWRITE_TAC[set_of_list; Rogers.CIRCUMCENTER_2; midpoint]); (MATCH_MP_TAC MHFTTZN4); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `1`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `2`); (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]); (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1); (NEW_GOAL `n IN voronoi_list V [u0; u1:real^3]`); (NEW_GOAL `s2 IN voronoi_list V [u0; u1:real^3]`); (NEW_GOAL `(s2:real^3) IN voronoi_list V vl`); (SIMP_TAC[ASSUME `s2 = omega_list V vl`]); (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST); (EXISTS_TAC `2`); (ASM_REWRITE_TAC[]); (MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET A) ==> a IN A`)); (EXISTS_TAC `voronoi_list V vl`); (STRIP_TAC); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl"); (REWRITE_TAC[VORONOI_LIST;VORONOI_SET;voronoi_closed;set_of_list; SUBSET; IN_INTERS]); (ONCE_REWRITE_TAC[IN]); (REWRITE_TAC[IN_ELIM_THM]); (REPEAT STRIP_TAC); (FIRST_ASSUM MATCH_MP_TAC); (EXISTS_TAC `v:real^3`); (ASM_REWRITE_TAC[]); (UNDISCH_TAC `v IN {u0, u1:real^3}`); (SET_TAC[]); (NEW_GOAL `s3 IN voronoi_list V [u0; u1]`); (MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET A) ==> a IN A`)); (EXISTS_TAC `voronoi_list V vl`); (STRIP_TAC); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl"); (REWRITE_TAC[VORONOI_LIST;VORONOI_SET;voronoi_closed;set_of_list; SUBSET; IN_INTERS]); (ONCE_REWRITE_TAC[IN]); (REWRITE_TAC[IN_ELIM_THM]); (REPEAT STRIP_TAC); (FIRST_ASSUM MATCH_MP_TAC); (EXISTS_TAC `v:real^3`); (ASM_REWRITE_TAC[]); (UNDISCH_TAC `v IN {u0, u1:real^3}`); (SET_TAC[]); (NEW_GOAL `convex (voronoi_list V [u0;u1:real^3])`); (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]); (UP_ASM_TAC THEN REWRITE_TAC[convex] THEN STRIP_TAC); (SUBGOAL_THEN `between n (s2,s3:real^3)` MP_TAC); (ONCE_REWRITE_TAC[BETWEEN_SYM]); (MATCH_MP_TAC BETWEEN_TRANS); (EXISTS_TAC `s:real^3`); (ONCE_REWRITE_TAC[BETWEEN_SYM]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]); (REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM IN]); (REWRITE_TAC[ASSUME `n = u % s2 + v % s3:real^3`]); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (UNDISCH_TAC `between q (n,s1:real^3)`); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]); (REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM IN]); (REWRITE_TAC[ASSUME `q = u % n + v % s1:real^3`]); (NEW_GOAL `convex (voronoi_list V [u0;u1:real^3])`); (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]); (UP_ASM_TAC THEN REWRITE_TAC[convex] THEN STRIP_TAC); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (REWRITE_TAC[GSYM (ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`)]); (REWRITE_WITH `s1 = omega_list V [u0;u1:real^3]`); (EXPAND_TAC "s1"); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]); (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST); (EXISTS_TAC `1`); (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 ul`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3`); (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3`]); (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1); (REWRITE_TAC[set_of_list] THEN SET_TAC[]); (REAL_ARITH_TAC); (REWRITE_WITH `(s1 - u0) dot (u1 - u0:real^3) = dist (s1,u0) * dist (u1,u0)`); (REWRITE_TAC[dist]); (REWRITE_TAC [NORM_CAUCHY_SCHWARZ_EQ]); (REWRITE_TAC[ASSUME `s1 = inv (&2) % (u0 + u1:real^3)`; VECTOR_ARITH `inv (&2) % (u0 + u1) - u0 = inv (&2) % (u1 - u0)`]); (REWRITE_TAC[NORM_MUL; VECTOR_MUL_ASSOC; REAL_ABS_MUL]); (REWRITE_WITH `abs (inv (&2)) = inv (&2)`); (REWRITE_TAC[REAL_ABS_REFL]); (REAL_ARITH_TAC); (VECTOR_ARITH_TAC); (REWRITE_TAC[REAL_ADD_LID; REAL_ARITH `a * b >= x * b * a / t <=> &0 <= a * b * (&1 - x / t)`]); (MATCH_MP_TAC REAL_LE_MUL); (STRIP_TAC); (REWRITE_TAC[DIST_POS_LE]); (MATCH_MP_TAC REAL_LE_MUL); (STRIP_TAC); (REWRITE_TAC[DIST_POS_LE]); (REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`]); (REWRITE_WITH `dist (q,u0:real^3) / sqrt (&2) <= &1 <=> dist (q,u0) <= &1 * sqrt (&2) `); (MATCH_MP_TAC REAL_LE_LDIV_EQ); (MATCH_MP_TAC SQRT_POS_LT THEN REAL_ARITH_TAC); (ONCE_REWRITE_TAC[DIST_SYM]); (ONCE_REWRITE_TAC[REAL_MUL_LID]); (NEW_GOAL `dist (u0,s1:real^3) = hl (truncate_simplex 1 [u0;u1:real^3])`); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (REWRITE_WITH `s1 = omega_list V [u0;u1:real^3]`); (EXPAND_TAC "s1"); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (ONCE_REWRITE_TAC[DIST_SYM]); (REWRITE_WITH ` dist (omega_list V [u0; u1],u0) = dist (omega_list V [u0; u1],HD [u0;u1:real^3])`); (REWRITE_TAC[HD]); (MATCH_MP_TAC Rogers.WAUFCHE2); (EXISTS_TAC `1`); (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`); (EXPAND_TAC "vl"); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (REWRITE_TAC[IN]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `2`); (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]); (NEW_GOAL `hl (truncate_simplex 1 vl) <= hl (vl:(real^3)list)`); (MATCH_MP_TAC Rogers.HL_DECREASE); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`); (ASM_REWRITE_TAC[IN; ARITH_RULE `1 <= 2`]); (NEW_GOAL `hl (vl:(real^3)list) < sqrt (&2)`); (ONCE_ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (NEW_GOAL `hl (truncate_simplex 1 [u0;u1:real^3]) <= hl (vl:(real^3)list)`); (REWRITE_WITH `truncate_simplex 1 [u0;u1:real^3] = truncate_simplex 1 vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (MATCH_MP_TAC Rogers.HL_DECREASE); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`); (ASM_REWRITE_TAC[IN; ARITH_RULE `1 <= 2`]); (NEW_GOAL `hl (vl:(real^3)list) < sqrt (&2)`); (ONCE_ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (NEW_GOAL `dist (u0,s1:real^3) < sqrt (&2)`); (ONCE_ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (NEW_GOAL `?y. y IN {n,s1:real^3} /\ (!x. x IN convex hull {n,s1} ==> norm (x - u0) <= norm (y - u0))`); (MATCH_MP_TAC SIMPLEX_FURTHEST_LE); (REWRITE_TAC[Geomdetail.FINITE6]); (SET_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC [SET_RULE `a IN {x,y} <=> a = x \/ a = y`] THEN REPEAT STRIP_TAC); (NEW_GOAL `dist (u0,q) <= dist (u0, n:real^3)`); (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC [dist; GSYM (ASSUME `y' = n:real^3`)]); (POP_ASSUM MATCH_MP_TAC); (REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]); (ASM_REWRITE_TAC[]); (NEW_GOAL `dist (u0,n:real^3) <= sqrt (&2)`); (NEW_GOAL `?y. y IN {s2,s:real^3} /\ (!x. x IN convex hull {s2,s} ==> norm (x - u0) <= norm (y - u0))`); (MATCH_MP_TAC SIMPLEX_FURTHEST_LE); (REWRITE_TAC[Geomdetail.FINITE6]); (SET_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC [SET_RULE `a IN {x,y} <=> a = x \/ a = y`] THEN REPEAT STRIP_TAC); (NEW_GOAL `dist (u0,n) <= dist (u0, s2:real^3)`); (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC [dist; GSYM (ASSUME `y'' = s2:real^3`)]); (POP_ASSUM MATCH_MP_TAC); (REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]); (ASM_REWRITE_TAC[]); (NEW_GOAL `dist (u0,s2:real^3) < sqrt (&2)`); (ONCE_REWRITE_TAC[DIST_SYM]); (ONCE_ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (NEW_GOAL `dist (u0,n) <= dist (u0, s:real^3)`); (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC [dist; GSYM (ASSUME `y'' = s:real^3`)]); (POP_ASSUM MATCH_MP_TAC); (REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]); (ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (NEW_GOAL `dist (u0,q) <= dist (u0, s1:real^3)`); (ONCE_REWRITE_TAC[DIST_SYM] THEN REWRITE_TAC [dist; GSYM (ASSUME `y' = s1:real^3`)]); (POP_ASSUM MATCH_MP_TAC); (REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]); (ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (* ========================================================================== *) (NEW_GOAL `p:real^3 IN rcone_ge u0 u1 (dist (s1,u0) / sqrt (&2))`); (UNDISCH_TAC `between p (u0,q:real^3)`); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]); (REPEAT STRIP_TAC); (ONCE_REWRITE_TAC[GSYM IN]); (REWRITE_TAC[ASSUME `p = u % u0 + v % q:real^3`]); (REWRITE_WITH `u % u0 + v % q = u0 + v % (q - u0:real^3)`); (REWRITE_TAC[VECTOR_ARITH `u % u0 + v % q = u0 + v % (q - u0) <=> ((u + v) - &1) % u0 = vec 0`]); (ASM_REWRITE_TAC[]); (VECTOR_ARITH_TAC); (MATCH_MP_TAC RCONE_GE_TRANS); (REWRITE_TAC[VECTOR_ARITH `u0 + q - u0:real^3 = q`]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[RCONE_GT_GE; IN_DIFF]); (STRIP_TAC); (ASM_REWRITE_TAC[]); (REWRITE_TAC[IN;IN_ELIM_THM]); (STRIP_TAC); (NEW_GOAL `~(p:real^3 IN B3)`); (ASM_SET_TAC[]); (UP_ASM_TAC THEN EXPAND_TAC "B3" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; HD;TL]); (REWRITE_WITH `hl (truncate_simplex 1 [u0; u1; u2; u3]) = dist (s1,u0:real^3)`); (REWRITE_WITH `truncate_simplex 1 [u0; u1; u2; u3] = truncate_simplex 1 [u0;u1:real^3]`); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (REWRITE_WITH `s1 = omega_list V [u0;u1:real^3]`); (EXPAND_TAC "s1"); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_1]); (REWRITE_WITH ` dist (omega_list V [u0; u1],u0) = dist (omega_list V [u0; u1],HD [u0;u1:real^3])`); (REWRITE_TAC[HD]); (MATCH_MP_TAC Rogers.WAUFCHE2); (EXISTS_TAC `1`); (REWRITE_WITH `[u0;u1:real^3] = truncate_simplex 1 vl`); (EXPAND_TAC "vl"); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_1]); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (REWRITE_TAC[IN]); (MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `2`); (ASM_REWRITE_TAC[ARITH_RULE `1 <= 2`]); (NEW_GOAL `hl (truncate_simplex 1 vl) <= hl (vl:(real^3)list)`); (MATCH_MP_TAC Rogers.HL_DECREASE); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`); (ASM_REWRITE_TAC[IN; ARITH_RULE `1 <= 2`]); (NEW_GOAL `hl (vl:(real^3)list) < sqrt (&2)`); (ONCE_ASM_REWRITE_TAC[]); (ASM_REAL_ARITH_TAC); (ASM_REAL_ARITH_TAC); (REWRITE_TAC[rcone_eq;rconesgn;IN;IN_ELIM_THM]); (UP_ASM_TAC THEN REWRITE_TAC[dist] THEN MESON_TAC[]); (SET_TAC[]); (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 1`); (GEN_TAC THEN STRIP_TAC); (NEW_GOAL `~(y = 4 \/ y = 0 \/ y = 2 \/ y = 3)`); (ASM_SIMP_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `i = 1`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (GEN_TAC THEN STRIP_TAC); (ASM_REWRITE_TAC[]); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (UP_ASM_TAC THEN REWRITE_TAC[MESON[] `~ ~ A <=> A`] THEN DISCH_TAC); (* ======================================================================== *) (ASM_CASES_TAC `p IN aff_ge {u0:real^3, u1} {mxi V ul, omega_list_n V ul 3}`); (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> ~ (y = 4 \/ y = 0 \/ y = 1 \/ y = 3)`); (REPEAT STRIP_TAC); (NEW_GOAL `mcell 4 V ul = {}`); (SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (REFL_TAC); (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 4`]); (REWRITE_TAC[ASSUME `mcell 4 V ul = {}`]); (SET_TAC[]); (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 0`; MCELL_EXPLICIT;mcell0]); (STRIP_TAC); (NEW_GOAL `~(p:real^3 IN ball (HD ul,sqrt (&2)))`); (ASM_SET_TAC[IN_DIFF]); (UP_ASM_TAC THEN ASM_REWRITE_TAC[HD;IN;ball;IN_ELIM_THM]); (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 1`; MCELL_EXPLICIT;mcell1]); (COND_CASES_TAC); (REWRITE_TAC[IN_DIFF]); (STRIP_TAC); (ASM_MESON_TAC[]); (SET_TAC[]); (* ======================================================================= *) (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 3`; MCELL_EXPLICIT;mcell3]); (COND_CASES_TAC); (NEW_GOAL `(?s. between s (omega_list_n V ul 2,omega_list_n V ul 3) /\ dist (u0,s) = sqrt (&2) /\ mxi V ul = s:real^3)`); (MATCH_MP_TAC MXI_EXPLICIT_OLD); (ASM_REWRITE_TAC[]); (FIRST_X_ASSUM CHOOSE_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC); (UP_ASM_TAC THEN ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2;set_of_list]); (REWRITE_TAC[SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]); (STRIP_TAC); (ABBREV_TAC `s2 = omega_list_n V [u0; u1; u2; u3:real^3] 2`); (ABBREV_TAC `s3 = omega_list_n V [u0; u1; u2; u3:real^3] 3`); (NEW_GOAL `p IN aff_ge {u0, u1} {s, s3:real^3}`); (ASM_MESON_TAC[]); (ABBREV_TAC `vl = [u0;u1;u2:real^3]`); (NEW_GOAL `vl = truncate_simplex 2 ul:(real^3)list`); (ASM_REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2] THEN EXPAND_TAC "vl"); (NEW_GOAL `barV V 2 vl`); (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC Packing3.TRUNCATE_SIMPLEX_BARV); (EXISTS_TAC `3` THEN ASM_MESON_TAC[ARITH_RULE `2 <= 3`]); (NEW_GOAL `LENGTH (vl:(real^3)list) = 3 /\ CARD {u0,u1,u2:real^3} = 3`); (REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (REWRITE_TAC[ARITH_RULE `3 = 2 + 1`]); (MATCH_MP_TAC Rogers.BARV_IMP_LENGTH_EQ_CARD); (EXISTS_TAC `V:real^3->bool`); (ASM_REWRITE_TAC[]); (NEW_GOAL `s2:real^3 = omega_list V vl`); (EXPAND_TAC "s2" THEN EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (MESON_TAC[OMEGA_LIST_TRUNCATE_2]); (NEW_GOAL `s2 = circumcenter {u0,u1,u2:real^3}`); (REWRITE_WITH `{u0,u1,u2:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (REWRITE_TAC[ASSUME `s2 = omega_list V vl`]); (MATCH_MP_TAC Rogers.XNHPWAB1); (EXISTS_TAC `2` THEN REWRITE_TAC[IN]); (ASM_REWRITE_TAC[]); (ASM_MESON_TAC[]); (NEW_GOAL `dist (s2,u0:real^3) = hl (truncate_simplex 2 (ul:(real^3)list))`); (ONCE_REWRITE_TAC[EQ_SYM_EQ]); (REWRITE_TAC[GSYM (ASSUME `vl:(real^3)list = truncate_simplex 2 ul`)]); (REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]); (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (REWRITE_WITH `u0:real^3 = HD vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[HD]); (MATCH_MP_TAC Rogers.HL_EQ_DIST0); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`); (ASM_REWRITE_TAC[]); (NEW_GOAL `~(s = s2:real^3)`); (STRIP_TAC); (NEW_GOAL `dist (u0,s:real^3) < sqrt (&2)`); (ONCE_REWRITE_TAC[DIST_SYM]); (REWRITE_TAC[ASSUME `s = s2:real^3`]); (ASM_MESON_TAC[]); (ASM_REAL_ARITH_TAC); (NEW_GOAL `(s2:real^3) IN voronoi_list V vl`); (SIMP_TAC[ASSUME `s2 = omega_list V vl`]); (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST); (EXISTS_TAC `2`); (ASM_REWRITE_TAC[]); (NEW_GOAL `(s3:real^3) IN voronoi_list V ul`); (REWRITE_WITH `s3 = omega_list V ul`); (EXPAND_TAC "s3" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; OMEGA_LIST]); (REWRITE_TAC[LENGTH; ARITH_RULE `SUC (SUC (SUC (SUC 0))) - 1 = 3`]); (MATCH_MP_TAC Packing3.OMEGA_LIST_IN_VORONOI_LIST); (EXISTS_TAC `3`); (ASM_REWRITE_TAC[]); (NEW_GOAL `(s3:real^3) IN voronoi_list V vl`); (MATCH_MP_TAC (SET_RULE `(?s. a IN s /\ s SUBSET A) ==> a IN A`)); (EXISTS_TAC `voronoi_list V ul`); (STRIP_TAC); (ASM_REWRITE_TAC[]); (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`]); (REWRITE_TAC[VORONOI_LIST;VORONOI_SET;voronoi_closed;set_of_list; SUBSET; IN_INTERS]); (ONCE_REWRITE_TAC[IN]); (REWRITE_TAC[IN_ELIM_THM]); (REPEAT STRIP_TAC); (FIRST_ASSUM MATCH_MP_TAC); (EXISTS_TAC `v:real^3`); (ASM_REWRITE_TAC[]); (UNDISCH_TAC `v IN {u0, u1, u2:real^3}`); (SET_TAC[]); (NEW_GOAL `s IN voronoi_list V vl`); (NEW_GOAL `convex (voronoi_list V vl)`); (REWRITE_TAC[Packing3.CONVEX_VORONOI_LIST]); (UP_ASM_TAC THEN REWRITE_TAC[convex] THEN STRIP_TAC); (UNDISCH_TAC `between s (s2,s3:real^3)`); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]); (REPEAT STRIP_TAC); (ONCE_REWRITE_TAC[GSYM IN]); (REWRITE_TAC[ASSUME `s = u % s2 + v % s3:real^3`]); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (NEW_GOAL `~ (s IN affine hull {u0,u1,u2:real^3})`); STRIP_TAC; (NEW_GOAL `(s:real^3 - s2) dot (s - s2) = &0`); (REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]); (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (MATCH_MP_TAC MHFTTZN4); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (ASM_SIMP_TAC[IN_AFFINE_KY_LEMMA1]); (EXPAND_TAC "vl" THEN ASM_MESON_TAC[set_of_list]); (UP_ASM_TAC THEN REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0; NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]); (ASM_REWRITE_TAC[]); (NEW_GOAL `~affine_dependent {u0, u1, u2, s:real^3}`); (ONCE_REWRITE_TAC[SET_RULE `{a,b,c,d} = {d,a,b,c}`]); (MATCH_MP_TAC AFFINE_INDEPENDENT_INSERT); (ASM_REWRITE_TAC[]); (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2` THEN ASM_REWRITE_TAC[]); (NEW_GOAL `s2 IN convex hull {u0, u1, u2:real^3}`); (REWRITE_WITH `s2 = omega_list V vl /\ {u0, u1, u2:real^3} = set_of_list vl`); (EXPAND_TAC "s2" THEN EXPAND_TAC "vl"); (REWRITE_TAC[OMEGA_LIST_TRUNCATE_2;set_of_list]); (MATCH_MP_TAC Rogers.XNHPWAB2); (EXISTS_TAC `2`); (ASM_REWRITE_TAC[IN]); (ASM_MESON_TAC[]); (NEW_GOAL `~ (s3 IN affine hull {u0,u1,u2:real^3})`); STRIP_TAC; (NEW_GOAL `(s3:real^3 - s2) dot (s3 - s2) = &0`); (REWRITE_TAC[ASSUME `s2 = circumcenter {u0, u1, u2:real^3}`]); (REWRITE_WITH `{u0, u1, u2:real^3} = set_of_list vl`); (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list]); (MATCH_MP_TAC MHFTTZN4); (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `2`); (REPEAT STRIP_TAC); (ASM_REWRITE_TAC[]); (ASM_REWRITE_TAC[]); (ASM_SIMP_TAC[IN_AFFINE_KY_LEMMA1]); (EXPAND_TAC "vl" THEN ASM_MESON_TAC[set_of_list]); (UP_ASM_TAC THEN REWRITE_TAC[GSYM NORM_POW_2; Trigonometry2.POW2_EQ_0; NORM_EQ_0; VECTOR_ARITH `a - b = vec 0 <=> a = b`]); (REPEAT STRIP_TAC); (UNDISCH_TAC `between s (s2,s3:real^3)`); (REWRITE_TAC[ASSUME `s3 = s2:real^3`]); (REWRITE_TAC[BETWEEN_REFL_EQ]); (ASM_MESON_TAC[]); (NEW_GOAL `DISJOINT {u0,u1} {s, s3:real^3}`); (REWRITE_TAC[DISJOINT]); (MATCH_MP_TAC (SET_RULE `~ (a IN s) /\ ~ (b IN s) ==> s INTER {a, b} = {}`)); (REPEAT STRIP_TAC); (NEW_GOAL `s IN affine hull {u0, u1,u2:real^3}`); (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1); (UP_ASM_TAC THEN SET_TAC[]); (ASM_MESON_TAC[]); (NEW_GOAL `s3 IN affine hull {u0, u1,u2:real^3}`); (MATCH_MP_TAC IN_AFFINE_KY_LEMMA1); (UP_ASM_TAC THEN SET_TAC[]); (ASM_MESON_TAC[]); (UNDISCH_TAC `p IN aff_ge {u0, u1} {s, s3:real^3}`); (ASM_SIMP_TAC[AFF_GE_2_2]); (REWRITE_TAC[IN;IN_ELIM_THM]); (NEW_GOAL `?k1 k2. k1 + k2 = &1 /\ k2 <= &0 /\ k1 % s + k2 % s2 = s3:real^3`); (UNDISCH_TAC `between s (s2,s3:real^3)`); (REWRITE_TAC[BETWEEN_IN_CONVEX_HULL;CONVEX_HULL_2;IN;IN_ELIM_THM]); (REPEAT STRIP_TAC); (EXISTS_TAC `&1 / v` THEN EXISTS_TAC ` -- u / v`); (NEW_GOAL `~(v = &0)`); (STRIP_TAC); (NEW_GOAL `s = s2:real^3`); (REWRITE_TAC[ASSUME `s = u % s2 + v % s3:real^3`]); (REWRITE_WITH `v = &0 /\ u = &1`); (ASM_REAL_ARITH_TAC); (VECTOR_ARITH_TAC); (ASM_MESON_TAC[]); (REPEAT STRIP_TAC); (REWRITE_TAC[REAL_ARITH `&1 / v + --u / v = (&1 - u) / v`]); (REWRITE_WITH `&1 - u = v`); (ASM_REAL_ARITH_TAC); (ASM_SIMP_TAC[REAL_DIV_REFL]); (REWRITE_TAC[REAL_ARITH `--u / v <= &0 <=> &0 <= u / v`]); (ASM_SIMP_TAC[REAL_LE_DIV]); (REWRITE_TAC[ASSUME `s = u % s2 + v % s3:real^3`]); (REWRITE_TAC[VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]); (REWRITE_TAC[VECTOR_ARITH `((&1 / v * u) % s2 + (&1 / v * v) % s3) + --u / v % s2 = s3 <=> (v / v - &1) % s3 = vec 0`]); (REWRITE_WITH `v / v = &1`); (ASM_SIMP_TAC[REAL_DIV_REFL]); (VECTOR_ARITH_TAC); (FIRST_X_ASSUM CHOOSE_TAC THEN FIRST_X_ASSUM CHOOSE_TAC); (REWRITE_WITH `s3 = k1 % s + k2 % s2:real^3`); (ASM_REWRITE_TAC[]); (UNDISCH_TAC `s2 IN convex hull {u0, u1, u2:real^3}`); (REWRITE_TAC[CONVEX_HULL_3; IN_ELIM_THM; IN]); (REPEAT STRIP_TAC); (UP_ASM_TAC THEN REWRITE_TAC[ASSUME `s2 = u % u0 + v % u1 + w % u2:real^3`]); (REWRITE_TAC [VECTOR_ADD_LDISTRIB;VECTOR_MUL_ASSOC]); (REWRITE_TAC[VECTOR_ARITH `t1 % u0 + t2 % u1 + t3 % s + (t4 * k1) % s + ((t4 * k2) * u) % u0 + ((t4 * k2) * v) % u1 + ((t4 * k2) * w) % u2 = (t4 * k2 * w) % u2 + (t1 + t4 * k2 * u) % u0 + (t2 + t4 * k2 * v) % u1 + (t3 + t4 * k1) % s`]); (STRIP_TAC); (NEW_GOAL `t4 * k2 * w = &0`); (MATCH_MP_TAC AFFINE_DEPENDENT_KY_LEMMA1); (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `s:real^3` THEN EXISTS_TAC `p:real^3`); (EXISTS_TAC `t1 + t4 * k2 * u`); (EXISTS_TAC `t2 + t4 * k2 * v`); (EXISTS_TAC `t3 + t4 * k1`); (ASM_REWRITE_TAC[]); (REPEAT STRIP_TAC); (UP_ASM_TAC THEN REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE `{u2, u0, u1, s} = {u0, u1, u2, s}`]); (ASM_REWRITE_TAC[]); (ONCE_REWRITE_TAC[SET_RULE `{u2, u0, u1, s} = {s, u0, u1, u2}`]); (REWRITE_WITH `4 = SUC (CARD {u0,u1,u2:real^3})`); (ASM_REWRITE_TAC[]); (ARITH_TAC); (MATCH_MP_TAC (MESON[Geomdetail.CARD_CLAUSES_IMP] `!s a. FINITE s /\ ~(a IN s) ==> CARD (a INSERT s) = SUC (CARD s)`)); (REWRITE_TAC[Geomdetail.FINITE6]); (STRIP_TAC); (NEW_GOAL `s IN affine hull {u0, u1, u2:real^3}`); (UP_ASM_TAC THEN REWRITE_TAC[IN_AFFINE_KY_LEMMA1]); (ASM_MESON_TAC[]); (REWRITE_TAC[GSYM (ASSUME `p = (t4 * k2 * w) % u2 + (t1 + t4 * k2 * u) % u0 + (t2 + t4 * k2 * v) % u1 + (t3 + t4 * k1) % s:real^3`)]); (ONCE_REWRITE_TAC[SET_RULE `{u2, u0, u1, s} = {u0, u1, u2,s}`]); (ASM_REWRITE_TAC[]); (REWRITE_TAC[REAL_ARITH `t4 * k2 * w + (t1 + t4 * k2 * u) + (t2 + t4 * k2 * v) + t3 + t4 * k1 = t1 + t2 + t3 + t4 * (k1 + k2 * (u + v + w))`]); (ASM_REWRITE_TAC[REAL_MUL_RID]); (NEW_GOAL `&0 <= -- k2`); (ASM_REAL_ARITH_TAC); (REWRITE_TAC[REAL_ARITH `a * b * c <= &0 <=> &0 <= a * c * (-- b)`]); (ASM_SIMP_TAC[REAL_LE_MUL]); (NEW_GOAL `p IN affine hull {u0,u1,s:real^3}`); (REWRITE_TAC[AFFINE_HULL_3;IN;IN_ELIM_THM]); (EXISTS_TAC `t1 + t4 * k2 * u`); (EXISTS_TAC `t2 + t4 * k2 * v`); (EXISTS_TAC `t3 + t4 * k1`); (ASM_REWRITE_TAC[VECTOR_MUL_LZERO;VECTOR_ADD_LID]); (REWRITE_TAC[REAL_ARITH `(t1 + t4 * k2 * u) + (t2 + t4 * k2 * v) + t3 + t4 * k1 = (t1 + t2 + t3 + t4 * (k1 + k2 * (u + v + w))) - (t4 * k2 * w)`]); (ASM_REWRITE_TAC[REAL_MUL_RID]); (REAL_ARITH_TAC); (NEW_GOAL `~(p:real^3 IN B4)`); (ASM_SET_TAC[]); (UP_ASM_TAC THEN EXPAND_TAC "B4" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; HD;TL]); (REWRITE_WITH `mxi V [u0; u1; u2; u3] = s`); (ASM_MESON_TAC[]); (ASM_REWRITE_TAC[]); (SET_TAC[]); (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 2`); (GEN_TAC THEN STRIP_TAC); (NEW_GOAL `~(y = 4 \/ y = 0 \/ y = 1 \/ y = 3)`); (ASM_SIMP_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `i = 2`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (GEN_TAC THEN STRIP_TAC); (ASM_REWRITE_TAC[]); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (* ===================================================================== *) (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> ~ (y = 4 \/ y = 0 \/ y = 1 \/ y = 2)`); (REPEAT STRIP_TAC); (NEW_GOAL `mcell 4 V ul = {}`); (SIMP_TAC[MCELL_EXPLICIT; ARITH_RULE `4 >= 4`;mcell4]); (COND_CASES_TAC); (NEW_GOAL `F`); (ASM_MESON_TAC[]); (ASM_MESON_TAC[]); (REFL_TAC); (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 4`]); (REWRITE_TAC[ASSUME `mcell 4 V ul = {}`]); (SET_TAC[]); (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 0`; MCELL_EXPLICIT;mcell0]); (STRIP_TAC); (NEW_GOAL `~(p:real^3 IN ball (HD ul,sqrt (&2)))`); (ASM_SET_TAC[IN_DIFF]); (UP_ASM_TAC THEN ASM_REWRITE_TAC[HD;IN;ball;IN_ELIM_THM]); (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 1`; MCELL_EXPLICIT;mcell1]); (COND_CASES_TAC); (REWRITE_TAC[IN_DIFF]); (STRIP_TAC); (ASM_MESON_TAC[]); (SET_TAC[]); (UNDISCH_TAC `p IN mcell y V ul` THEN REWRITE_TAC[ASSUME `y = 2`; MCELL_EXPLICIT;mcell2]); (COND_CASES_TAC); (LET_TAC); (UNDISCH_TAC `~(p IN aff_ge {u0, u1} {mxi V ul, omega_list_n V ul 3})`); (REWRITE_TAC[IN_INTER; ASSUME `ul = [u0;u1;u2;u3:real^3]`;HD;TL]); (MESON_TAC[]); (SET_TAC[]); (NEW_GOAL `!y. y <= 4 /\ p IN mcell y V ul ==> y = 3`); (GEN_TAC THEN STRIP_TAC); (NEW_GOAL `~(y = 4 \/ y = 0 \/ y = 1 \/ y = 2)`); (ASM_SIMP_TAC[]); (ASM_ARITH_TAC); (NEW_GOAL `i = 3`); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[]); (GEN_TAC THEN STRIP_TAC); (ASM_REWRITE_TAC[]); (FIRST_ASSUM MATCH_MP_TAC); (ASM_REWRITE_TAC[])]);; end;;