(* ======================================================================== *) g (mk_imp(tsk_hyp_new,`TSKAJXY_statement`));; e (STRIP_TAC);; e (REWRITE_TAC[TSKAJXY_statement; mcell_set; IN_ELIM_THM]);; e (REWRITE_TAC[IN]);; e (REPEAT STRIP_TAC);; e (ASM_CASES_TAC `NULLSET X`);; e (REWRITE_TAC[gammaX]);; e (MATCH_MP_TAC (REAL_ARITH `x = &0 /\ y = &0 /\ z = &0 ==> x - y + z >= &0`));; e (REWRITE_TAC[total_solid; REAL_ENTIRE]);; e (REPEAT STRIP_TAC);; e (MATCH_MP_TAC MEASURE_EQ_0);; e (ASM_REWRITE_TAC[]);; e (DISJ2_TAC);; e (REWRITE_WITH `VX V X = {}`);; e (REWRITE_TAC[VX]);; e (ASM_REWRITE_TAC[]);; e (REWRITE_TAC[SUM_CLAUSES]);; e (DISJ2_TAC);; e (REWRITE_WITH `edgeX V X = {}`);; e (REWRITE_TAC[edgeX]);; e (REWRITE_WITH `VX V X = {}`);; e (REWRITE_TAC[VX]);; e (ASM_REWRITE_TAC[]);; e (ONCE_REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`]);; e (SET_TAC[]);; e (REWRITE_TAC[SUM_CLAUSES]);; e (NEW_GOAL `~(X:real^3->bool = {})`);; e (STRIP_TAC THEN SWITCH_TAC THEN UP_ASM_TAC THEN REWRITE_TAC[ASSUME `X:real^3->bool = {}`; NEGLIGIBLE_EMPTY]);; (* ========================================================================= *) e (ASM_CASES_TAC `i >= 4`);; e (NEW_GOAL `X = mcell4 V ul`);; e (ASM_REWRITE_TAC[]);; e (ASM_SIMP_TAC[MCELL_EXPLICIT]);; e (UP_ASM_TAC THEN REWRITE_TAC[mcell4]);; e (COND_CASES_TAC);; e (NEW_GOAL `?u0 u1 u2 u3. ul = [u0; u1; u2; u3:real^3]`);; e (MATCH_MP_TAC BARV_3_EXPLICIT);; e (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);; e (UP_ASM_TAC THEN STRIP_TAC);; e (REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`; set_of_list]);; e (STRIP_TAC);; e (ABBREV_TAC `y1 = dist (u0:real^3, u1)`);; e (ABBREV_TAC `y2 = dist (u0:real^3, u2)`);; e (ABBREV_TAC `y3 = dist (u0:real^3, u3)`);; e (ABBREV_TAC `y4 = dist (u2:real^3, u3)`);; e (ABBREV_TAC `y5 = dist (u1:real^3, u3)`);; e (ABBREV_TAC `y6 = dist (u1:real^3, u2)`);; e (NEW_GOAL `VX V X = {u0,u1,u2,u3}`);; e (REWRITE_WITH `VX V X = V INTER X`);; e (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);; e (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);; e (ASM_REWRITE_TAC[]);; e (REWRITE_WITH `X = mcell 4 V ul`);; e (ASM_REWRITE_TAC[]);; e (MESON_TAC[ARITH_RULE `4 >= 4`; ASSUME `i >= 4`; MCELL_EXPLICIT]);; e (REWRITE_WITH `V INTER mcell 4 V ul = set_of_list (truncate_simplex (4 - 1) ul)`);; e (MATCH_MP_TAC Lepjbdj.LEPJBDJ);; e (ASM_REWRITE_TAC[ARITH_RULE `1 <= 4 /\ 4 <= 4`]);; e (REWRITE_WITH ` mcell 4 V [u0; u1; u2; u3] = X`);; e (ASM_REWRITE_TAC[]);; e (MESON_TAC[ARITH_RULE `4 >= 4`; ASSUME `i >= 4`; MCELL_EXPLICIT]);; e (ASM_REWRITE_TAC[]);; e (ASM_REWRITE_TAC[ARITH_RULE `4 - 1 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3; set_of_list]);; e (REWRITE_WITH `vol X = vol_y y1 y2 y3 y4 y5 y6 /\ gammaX V X lmfun = gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun`);; e (MATCH_MP_TAC gammaX_gamm4fgcy);; e (EXISTS_TAC `ul:(real^3)list`);; e (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);; e (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);; e (EXISTS_TAC `i:num`);; e (ASM_REWRITE_TAC[]);; (* ========================================================================= *) e (NEW_GOAL `!y1 y2 y3 y4 y5 y6. ineq [#2.0,y1,sqrt8; #2.0,y2,sqrt8; #2.0,y3,sqrt8; #2.0,y4,sqrt8; #2.0, y5, sqrt8; #2.0,y6,sqrt8] (~critical_edge_y y1 /\ ~critical_edge_y y2 /\ ~critical_edge_y y3 /\ ~critical_edge_y y4 /\ ~critical_edge_y y5 /\ ~critical_edge_y y6 /\ &0 < delta_y y1 y2 y3 y4 y5 y6 /\ rad2_y y1 y2 y3 y4 y5 y6 < &2 ==> gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun >= &0)`);; e (MATCH_MP_TAC TSKAJXY_DERIVED4);; e (ASM_REWRITE_TAC[]);; e (UP_ASM_TAC THEN REWRITE_TAC[ineq; MESON[] `a ==> b ==> c <=> (a /\ b) ==> c`] THEN STRIP_TAC);; e (FIRST_ASSUM MATCH_MP_TAC);; e (ASM_REWRITE_TAC[]);; e (NEW_GOAL `~(critical_edge_y y1) /\ ~(critical_edge_y y2) /\ ~(critical_edge_y y3) /\ ~(critical_edge_y y4) /\ ~(critical_edge_y y5) /\ ~(critical_edge_y y6) /\ &0 < delta_y y1 y2 y3 y4 y5 y6`);; e (REWRITE_TAC[critical_edge_y]);; e (REPEAT STRIP_TAC);; e (NEW_GOAL `{u0:real^3, u1} IN critical_edgeX V X`);; e (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);; e (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);; e (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);; e (REPEAT STRIP_TAC);; e (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);; e (ASM_REWRITE_TAC[]);; e (STRIP_TAC);; e (ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]);; e (STRIP_TAC);; e (ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]);; e (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y1`);; e (EXPAND_TAC "y1" THEN REWRITE_TAC[dist; ASSUME `u0:real^3 = u1`; NORM_ARITH `norm (u1 - u1) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]);; e (MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_SET_TAC[]);; e (NEW_GOAL `{u0:real^3, u2} IN critical_edgeX V X`);; e (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);; e (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u2:real^3`);; e (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);; e (REPEAT STRIP_TAC);; e (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u2:real^3`);; e (ASM_REWRITE_TAC[]);; e (STRIP_TAC);; e (ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]);; e (STRIP_TAC);; e (ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]);; e (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y2`);; e (EXPAND_TAC "y2" THEN REWRITE_TAC[dist; ASSUME `u0:real^3 = u2`; NORM_ARITH `norm (u2 - u2) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]);; e (MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_SET_TAC[]);; e (NEW_GOAL `{u0:real^3, u3} IN critical_edgeX V X`);; e (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);; e (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u3:real^3`);; e (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);; e (REPEAT STRIP_TAC);; e (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u3:real^3`);; e (ASM_REWRITE_TAC[]);; e (STRIP_TAC);; e (ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]);; e (STRIP_TAC);; e (ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]);; e (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y3`);; e (EXPAND_TAC "y3" THEN REWRITE_TAC[dist; ASSUME `u0:real^3 = u3`; NORM_ARITH `norm (u3 - u3) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]);; e (MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_SET_TAC[]);; e (NEW_GOAL `{u2:real^3, u3} IN critical_edgeX V X`);; e (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);; e (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);; e (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);; e (REPEAT STRIP_TAC);; e (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);; e (ASM_REWRITE_TAC[]);; e (STRIP_TAC);; e (ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]);; e (STRIP_TAC);; e (ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]);; e (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y4`);; e (EXPAND_TAC "y4" THEN REWRITE_TAC[dist; ASSUME `u2:real^3 = u3`; NORM_ARITH `norm (u3 - u3) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]);; e (MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_SET_TAC[]);; e (NEW_GOAL `{u1:real^3, u3} IN critical_edgeX V X`);; e (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);; e (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u3:real^3`);; e (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);; e (REPEAT STRIP_TAC);; e (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u3:real^3`);; e (ASM_REWRITE_TAC[]);; e (STRIP_TAC);; e (ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]);; e (STRIP_TAC);; e (ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]);; e (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y5`);; e (EXPAND_TAC "y5" THEN REWRITE_TAC[dist; ASSUME `u1:real^3 = u3`; NORM_ARITH `norm (u3 - u3) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]);; e (MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_SET_TAC[]);; e (NEW_GOAL `{u1:real^3, u2} IN critical_edgeX V X`);; e (REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);; e (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3`);; e (REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);; e (REPEAT STRIP_TAC);; e (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3`);; e (ASM_REWRITE_TAC[]);; e (STRIP_TAC);; e (ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]);; e (STRIP_TAC);; e (ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]);; e (STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y6`);; e (EXPAND_TAC "y6" THEN REWRITE_TAC[dist; ASSUME `u1:real^3 = u2`; NORM_ARITH `norm (u2 - u2) = &0`; REAL_ARITH `~(&2 * s <= &0) <=> &0 < s`]);; e (MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_REAL_ARITH_TAC);; e (ASM_SET_TAC[]);; e (REWRITE_WITH `&0 < delta_y y1 y2 y3 y4 y5 y6 <=> &0 < sqrt (delta_y y1 y2 y3 y4 y5 y6)`);; e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);; e (MATCH_MP_TAC SQRT_LT_0);; e (REWRITE_TAC[delta_y]);; e (ABBREV_TAC `x1 = y1 * y1` THEN ABBREV_TAC `x2 = y2 * y2`);; e (ABBREV_TAC `x3 = y3 * y3` THEN ABBREV_TAC `x4 = y4 * y4`);; e (ABBREV_TAC `x5 = y5 * y5` THEN ABBREV_TAC `x6 = y6 * y6`);; e (REWRITE_WITH `delta_x x1 x2 x3 x4 x5 x6 = (let a = u1:real^3 - u0 in let b = u2 - u0 in let c = u3 - u0 in &4 * (a$1 * b$2 * c$3 - a$1 * b$3 * c$2 - a$2 * b$1 * c$3 + a$2 * b$3 * c$1 + a$3 * b$1 * c$2 - a$3 * b$2 * c$1) pow 2)`);; e (MATCH_MP_TAC Delta_x.COMPUTE_DELTA_X);; e (REWRITE_TAC[xlist; ylist]);; e (REPEAT LET_TAC);; e (EXPAND_TAC "x1" THEN EXPAND_TAC "x2" THEN EXPAND_TAC "x3");; e (EXPAND_TAC "x4" THEN EXPAND_TAC "x5" THEN EXPAND_TAC "x6");; e (UP_ASM_TAC THEN REWRITE_TAC[PAIR_EQ; GSYM REAL_POW_2]);; e (ASM_REWRITE_TAC[]);; e (STRIP_TAC);; e (ASM_REWRITE_TAC[]);; e (REPEAT LET_TAC);; e (REWRITE_TAC[REAL_ARITH `&0 <= &4 * a <=> &0 <= a`]);; e (REWRITE_TAC[Real_ext.REAL_LE_POW_2]);; e (ONCE_REWRITE_TAC[REAL_ARITH `&0 < a <=> &0 < a / &12`]);; e (REWRITE_WITH `sqrt (delta_y y1 y2 y3 y4 y5 y6) / &12 = vol (convex hull {u0,u1,u2,u3})`);; e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);; e (REWRITE_TAC[delta_y; GSYM REAL_POW_2]);; e (EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");; e (EXPAND_TAC "y4" THEN EXPAND_TAC "y5" THEN EXPAND_TAC "y6");; e (REWRITE_TAC[VOLUME_OF_CLOSED_TETRAHEDRON]);; e (REWRITE_TAC[GSYM (ASSUME `X = convex hull {u0, u1, u2, u3:real^3}`)]);; e (REWRITE_WITH `&0 < vol X <=> ~NULLSET X`);; e (MATCH_MP_TAC MEASURABLE_MEASURE_POS_LT);; e (REWRITE_TAC[ASSUME `X = convex hull {u0, u1, u2, u3:real^3}`]);; e (MATCH_MP_TAC MEASURABLE_CONVEX_HULL);; e (MATCH_MP_TAC FINITE_IMP_BOUNDED);; e (REWRITE_TAC[Geomdetail.FINITE6]);; e (ASM_REWRITE_TAC[]);; e (ASM_REWRITE_TAC[]);; e (NEW_GOAL `!u v. {u,v} IN edgeX V X ==> (#2.0 <= dist (u,v) /\ dist(u,v) <= sqrt8)`);; e (REPEAT GEN_TAC);; e (REWRITE_TAC[edgeX; IN]);; e (REWRITE_TAC[MESON[IN] `VX V X x <=> x IN VX V X`]);; e (ASM_REWRITE_TAC[IN_ELIM_THM]);; e (STRIP_TAC);; e (MP_TAC (ASSUME `packing V`));; e (REWRITE_TAC[packing; REAL_ARITH `#2.0 = &2`] THEN STRIP_TAC);; e (STRIP_TAC);; e (FIRST_ASSUM MATCH_MP_TAC);; e (NEW_GOAL `u:real^3 IN {u0,u1,u2,u3} /\ v IN {u0,u1,u2,u3}`);; e (DEL_TAC THEN UP_ASM_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC);; e (SET_TAC[]);; e (NEW_GOAL `{u0,u1,u2,u3:real^3} SUBSET V`);; e (REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);; e (MATCH_MP_TAC BARV_SUBSET);; e (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);; e (STRIP_TAC);; e (REWRITE_TAC[MESON[IN] `(V:real^3->bool) x <=> x IN V`]);; e (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);; e (STRIP_TAC);; e (REWRITE_TAC[MESON[IN] `(V:real^3->bool) x <=> x IN V`]);; e (UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]);; e (DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC);; e (SET_TAC[]);; (* ------------------------------------------------------------------------ *) e (ABBREV_TAC `s = circumcenter {u0,u1,u2,u3:real^3}`);; e (NEW_GOAL `dist (u,v:real^3) <= dist (s,u) + dist (s, v)`);; e (NORM_ARITH_TAC);; e (NEW_GOAL `!w. w IN {u0,u1,u2,u3:real^3} ==> radV {u0,u1,u2,u3:real^3} = dist (circumcenter {u0,u1,u2,u3:real^3},w)`);; e (MATCH_MP_TAC Rogers.OAPVION2);; e (REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);; e (MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);; e (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);; e (NEW_GOAL `dist (s,u) + dist (s,v:real^3) <= sqrt8`);; e (REWRITE_TAC[Nonlinear_lemma.sqrt8_sqrt2; sqrt2]);; e (MATCH_MP_TAC (REAL_ARITH `a < x /\ b < x ==> a + b <= &2 * x`));; e (STRIP_TAC);; e (REWRITE_WITH `dist (s,u:real^3) = radV {u0,u1,u2,u3:real^3}`);; e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);; e (EXPAND_TAC "s");; e (FIRST_ASSUM MATCH_MP_TAC);; e (DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN DEL_TAC);; e (UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC);; e (SET_TAC[]);; e (REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);; e (REWRITE_TAC[GSYM HL]);; e (ASM_REWRITE_TAC[]);; e (REWRITE_WITH `dist (s,v:real^3) = radV {u0,u1,u2,u3:real^3}`);; e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);; e (EXPAND_TAC "s");; e (FIRST_ASSUM MATCH_MP_TAC);; e (DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN DEL_TAC);; e (UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC);; e (SET_TAC[]);; e (REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);; e (REWRITE_TAC[GSYM HL]);; e (ASM_REWRITE_TAC[]);; e (ASM_REAL_ARITH_TAC);; e (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} = 4`);; e (REWRITE_TAC[ARITH_RULE `4 = 3 + 1`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);; e (MATCH_MP_TAC Marchal_cells_3.BARV_CARD_LEMMA);; e (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);; e (NEW_GOAL `~(u0 = u1:real^3) /\ ~(u0 = u2) /\ ~(u0 = u3) /\ ~(u1 = u2) /\ ~(u1 = u3) /\ ~(u2 = u3)`);; e (REPEAT STRIP_TAC);; e (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);; e (REWRITE_TAC[ASSUME `u0 = u1:real^3`; SET_RULE `{u1, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]);; e (ASM_ARITH_TAC);; e (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);; e (REWRITE_TAC[ASSUME `u0 = u2:real^3`; SET_RULE `{u2, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]);; e (ASM_ARITH_TAC);; e (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);; e (REWRITE_TAC[ASSUME `u0 = u3:real^3`; SET_RULE `{u3, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]);; e (ASM_ARITH_TAC);; e (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);; e (REWRITE_TAC[ASSUME `u1 = u2:real^3`; SET_RULE `{u0, u2, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ]);; e (ASM_ARITH_TAC);; e (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);; e (REWRITE_TAC[ASSUME `u1 = u3:real^3`; SET_RULE `{u0, u3, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ]);; e (ASM_ARITH_TAC);; e (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);; e (REWRITE_TAC[ASSUME `u2 = u3:real^3`; SET_RULE `{u0, u1, u3, u3} = {u0,u1,u3}`;Geomdetail.CARD3 ]);; e (ASM_ARITH_TAC);; e (NEW_GOAL `edgeX V X = {{u0,u1:real^3}, {u0,u2}, {u0,u3}, {u1,u2}, {u1,u3}, {u2,u3}}`);; e (REWRITE_TAC[edgeX]);; e (ONCE_REWRITE_TAC[SET_EQ_LEMMA]);; e (REWRITE_TAC[IN_ELIM_THM]);; e (REPEAT STRIP_TAC);; e (UNDISCH_TAC `VX V X u` THEN UNDISCH_TAC `VX V X v`);; e (REWRITE_TAC[MESON[IN] `VX V X s <=> s IN VX V X`]);; e (ASM_REWRITE_TAC[SET_RULE `v IN {u0, u1, u2, u3} <=> v = u0 \/ v = u1 \/ v = u2 \/ v = u3`]);; e (REPEAT STRIP_TAC);; e (NEW_GOAL `F`);; e (ASM_MESON_TAC[]);; e (ASM_MESON_TAC[]);; e (REWRITE_WITH `{u,v} = {v,u:real^3}`);; e (SET_TAC[]);; e (ASM_REWRITE_TAC[] THEN SET_TAC[]);; e (REWRITE_WITH `{u,v} = {v,u:real^3}`);; e (SET_TAC[]);; e (ASM_REWRITE_TAC[] THEN SET_TAC[]);; e (REWRITE_WITH `{u,v} = {v,u:real^3}`);; e (SET_TAC[]);; e (ASM_REWRITE_TAC[] THEN SET_TAC[]);; e (ASM_REWRITE_TAC[] THEN SET_TAC[]);; e (NEW_GOAL `F`);; e (ASM_MESON_TAC[]);; e (ASM_MESON_TAC[]);; e (REWRITE_WITH `{u,v} = {v,u:real^3}`);; e (SET_TAC[]);; e (ASM_REWRITE_TAC[] THEN SET_TAC[]);; e (REWRITE_WITH `{u,v} = {v,u:real^3}`);; e (SET_TAC[]);; e (ASM_REWRITE_TAC[] THEN SET_TAC[]);; e (ASM_REWRITE_TAC[] THEN SET_TAC[]);; e (ASM_REWRITE_TAC[] THEN SET_TAC[]);; e (NEW_GOAL `F`);; e (ASM_MESON_TAC[]);; e (ASM_MESON_TAC[]);; e (REWRITE_WITH `{u,v} = {v,u:real^3}`);; e (SET_TAC[]);; e (ASM_REWRITE_TAC[] THEN SET_TAC[]);; e (ASM_REWRITE_TAC[] THEN SET_TAC[]);; e (ASM_REWRITE_TAC[] THEN SET_TAC[]);; e (ASM_REWRITE_TAC[] THEN SET_TAC[]);; e (NEW_GOAL `F`);; e (ASM_MESON_TAC[]);; e (ASM_MESON_TAC[]);; e (UP_ASM_TAC THEN REWRITE_TAC[SET_RULE `x IN {a,b,c,d,e,f} <=> x = a \/ x = b \/ x = c \/ x = d \/ x = e \/ x = f`]);; e (REWRITE_TAC[MESON[IN] `VX V X s <=> s IN VX V X`]);; e (ASM_REWRITE_TAC[SET_RULE `v IN {u0, u1, u2, u3} <=> v = u0 \/ v = u1 \/ v = u2 \/ v = u3`]);; e (REPEAT STRIP_TAC);; e (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]);; e (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u2:real^3` THEN ASM_REWRITE_TAC[]);; e (EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[]);; e (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN ASM_REWRITE_TAC[]);; e (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[]);; e (EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[]);; e (STRIP_TAC);; e (EXPAND_TAC "y1");; e (FIRST_ASSUM MATCH_MP_TAC);; e (ASM_REWRITE_TAC[] THEN SET_TAC[]);; e (STRIP_TAC);; e (EXPAND_TAC "y2");; e (FIRST_ASSUM MATCH_MP_TAC);; e (ASM_REWRITE_TAC[] THEN SET_TAC[]);; e (STRIP_TAC);; e (EXPAND_TAC "y3");; e (FIRST_ASSUM MATCH_MP_TAC);; e (ASM_REWRITE_TAC[] THEN SET_TAC[]);; e (STRIP_TAC);; e (EXPAND_TAC "y4");; e (FIRST_ASSUM MATCH_MP_TAC);; e (ASM_REWRITE_TAC[] THEN SET_TAC[]);; e (STRIP_TAC);; e (EXPAND_TAC "y5");; e (FIRST_ASSUM MATCH_MP_TAC);; e (ASM_REWRITE_TAC[] THEN SET_TAC[]);; e (STRIP_TAC);; e (EXPAND_TAC "y6");; e (FIRST_ASSUM MATCH_MP_TAC);; e (ASM_REWRITE_TAC[] THEN SET_TAC[]);; e (REWRITE_WITH `rad2_y y1 y2 y3 y4 y5 y6 = radV {u0,u1,u2,u3:real^3} pow 2`);; e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);; e (REWRITE_TAC[rad2_y; y_of_x]);; e (GMATCH_SIMP_TAC (REWRITE_RULE[LET_DEF;LET_END_DEF] Merge_ineq.GDRQXLGv2));; e (STRIP_TAC);; e (STRIP_TAC);; e (REWRITE_TAC[ARITH_RULE `4 = 3 + 1`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);; e (MATCH_MP_TAC Marchal_cells_3.BARV_CARD_LEMMA);; e (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);; e (REWRITE_TAC[coplanar_alt]);; e (REWRITE_TAC[GSYM Trigonometry2.coplanar1]);; e (REWRITE_TAC[coplanar] THEN STRIP_TAC);; e (NEW_GOAL `affine hull {u0, u1, u2, u3:real^3} SUBSET affine hull (affine hull {u, v, w})`);; e (ASM_SIMP_TAC[Marchal_cells_2.AFFINE_SUBSET_KY_LEMMA]);; e (UP_ASM_TAC THEN REWRITE_WITH `affine hull (affine hull {u, v, w}) = affine hull {u:real^3, v, w}`);; e (REWRITE_TAC[AFFINE_HULL_EQ; AFFINE_AFFINE_HULL]);; e (STRIP_TAC);; e (NEW_GOAL `NULLSET X`);; e (MATCH_MP_TAC NEGLIGIBLE_SUBSET);; e (EXISTS_TAC `affine hull {u0, u1, u2, u3:real^3}`);; e (STRIP_TAC);; e (MATCH_MP_TAC NEGLIGIBLE_SUBSET);; e (EXISTS_TAC `affine hull {u,v,w:real^3}`);; e (REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]);; e (ASM_REWRITE_TAC[]);; e (REWRITE_TAC[ASSUME `X = mcell i V ul`]);; e (REWRITE_WITH `mcell i V ul = mcell4 V ul`);; e (MESON_TAC[ARITH_RULE `4 >= 4`; MCELL_EXPLICIT; ASSUME `i >= 4`]);; e (REWRITE_TAC[mcell4]);; e (COND_CASES_TAC);; e (ASM_REWRITE_TAC[set_of_list; CONVEX_HULL_SUBSET_AFFINE_HULL]);; e (SET_TAC[]);; e (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);; e (REWRITE_TAC[GSYM REAL_POW_2]);; e (EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");; e (EXPAND_TAC "y4" THEN EXPAND_TAC "y5" THEN EXPAND_TAC "y6");; e (REWRITE_TAC[]);; e (REWRITE_WITH `radV {u0, u1, u2, u3:real^3} = hl (ul:(real^3)list)`);; e (ASM_REWRITE_TAC[HL;set_of_list]);; e (REWRITE_WITH `hl (ul:(real^3)list) pow 2 < &2 <=> sqrt (hl ul pow 2) < sqrt (&2)`);; e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);; e (MATCH_MP_TAC Real_ext.REAL_PROP_LT_SQRT);; e (REWRITE_TAC[REAL_LE_POW_2] THEN REAL_ARITH_TAC);; e (REWRITE_WITH `sqrt (hl (ul:(real^3)list) pow 2) = hl ul`);; e (MATCH_MP_TAC POW_2_SQRT);; e (MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));; e (NEW_GOAL `hl (truncate_simplex 1 ul) <= hl (ul:(real^3)list)`);; e (MATCH_MP_TAC Rogers.HL_DECREASE);; e (EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3`);; e (ASM_REWRITE_TAC[IN; ARITH_RULE `1 <= 3`]);; e (NEW_GOAL `&0 < hl (truncate_simplex 1 (ul:(real^3)list))`);; e (MATCH_MP_TAC Marchal_cells_2.BARV_IMP_HL_1_POS_LT);; e (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);; e (ASM_REAL_ARITH_TAC);; e (ASM_REWRITE_TAC[]);; e (STRIP_TAC);; e (NEW_GOAL `F`);; e (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);; e (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);; (* --- Finish the case 4-cell, the remains are 0-3 cells ------------------ *) (* ======================================================================== *) e (ASM_CASES_TAC `i = 0`);; e (NEW_GOAL `VX V X = {}`);; e (REWRITE_WITH `VX V X = V INTER X`);; e (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);; e (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);; e (ASM_REWRITE_TAC[]);; e (ASM_REWRITE_TAC[]);; e (MATCH_MP_TAC Lepjbdj.LEPJBDJ_0);; e (ASM_REWRITE_TAC[]);; e (NEW_GOAL `edgeX V X = {}`);; e (REWRITE_TAC[edgeX]);; e (ASM_REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`; SET_RULE `x IN {} <=> F`]);; e (SET_TAC[]);; e (REWRITE_TAC[gammaX]);; e (MATCH_MP_TAC (REAL_ARITH `b = &0 /\ c = &0 /\ &0 <= a ==> a - b + c >= &0`));; e (REPEAT STRIP_TAC);; e (ASM_REWRITE_TAC[total_solid; SUM_CLAUSES] THEN REAL_ARITH_TAC);; e (ASM_REWRITE_TAC[SUM_CLAUSES] THEN REAL_ARITH_TAC);; e (MATCH_MP_TAC MEASURE_POS_LE);; e (ASM_REWRITE_TAC[] THEN MATCH_MP_TAC Urrphbz1.MEASURABLE_MCELL);; e (ASM_REWRITE_TAC[]);; (* --- Finish the case 0-cell, the remains are 1-3 cells ------------------ *) (* ======================================================================== *) (* The 3-cell case *) e (ASM_CASES_TAC `i = 3`);; e (NEW_GOAL `X = mcell3 V ul`);; e (ASM_REWRITE_TAC[]);; e (ASM_SIMP_TAC[MCELL_EXPLICIT]);; e (UP_ASM_TAC THEN REWRITE_TAC[mcell3]);; e (COND_CASES_TAC);; e (STRIP_TAC);; e (NEW_GOAL `?u0 u1 u2 u3. ul = [u0; u1; u2; u3:real^3]`);; e (MATCH_MP_TAC BARV_3_EXPLICIT);; e (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);; e (UP_ASM_TAC THEN STRIP_TAC);; e (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)`);; e (MATCH_MP_TAC MXI_EXPLICIT);; e (EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);; e (ASM_REWRITE_TAC[]);; e (UP_ASM_TAC THEN STRIP_TAC);; e (ABBREV_TAC `s2 = omega_list_n V ul 2`);; e (ABBREV_TAC `s3 = omega_list_n V ul 3`);; e (ABBREV_TAC `vl = truncate_simplex 2 (ul:(real^3)list)`);; e (NEW_GOAL `s2 IN voronoi_list V vl`);; e (EXPAND_TAC "s2" THEN EXPAND_TAC "vl");; e (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);; e (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);; e (ARITH_TAC);; e (NEW_GOAL `s3 IN voronoi_list V vl`);; e (EXPAND_TAC "s3" THEN EXPAND_TAC "vl");; e (MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);; e (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);; e (ARITH_TAC);; e (NEW_GOAL `s IN voronoi_list V vl`);; e (MATCH_MP_TAC (SET_RULE `(?x. s IN x /\ x SUBSET t)==> s IN t`));; e (EXISTS_TAC `convex hull {s2,s3:real^3}`);; e (STRIP_TAC);; e (ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]);; e (NEW_GOAL `voronoi_list V vl = convex hull (voronoi_list V vl)`);; e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);; e (REWRITE_TAC[CONVEX_HULL_EQ; Packing3.CONVEX_VORONOI_LIST]);; e (ONCE_REWRITE_TAC[ASSUME `voronoi_list V vl = convex hull voronoi_list V vl`]);; e (MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);; e (ASM_SET_TAC[]);; e (MP_TAC (ASSUME `s IN voronoi_list V vl`));; e (EXPAND_TAC "vl" THEN REWRITE_TAC[ASSUME `ul = [u0;u1;u2;u3:real^3]`; TRUNCATE_SIMPLEX_EXPLICIT_2; VORONOI_LIST; VORONOI_SET; set_of_list; SET_RULE `x IN {a,b,c} <=> x=a\/x=b\/x=c`; IN_INTERS]);; e (STRIP_TAC);; e (NEW_GOAL `s IN voronoi_closed V u0 /\ s IN voronoi_closed V u1 /\ s IN voronoi_closed V (u2:real^3)`);; e (UP_ASM_TAC THEN SET_TAC[]);; e (UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM] THEN STRIP_TAC);; e (NEW_GOAL `u0 IN V /\ u1 IN V /\ u2 IN V /\ (u3:real^3) IN V`);; e (REWRITE_TAC[SET_RULE `u0 IN V /\ u1 IN V /\ u2 IN V /\ (u3:real^3) IN V <=> {u0,u1,u2,u3} SUBSET V`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);; e (MATCH_MP_TAC BARV_SUBSET);; e (EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);; e (FIRST_ASSUM MP_TAC THEN REWRITE_TAC[IN] THEN STRIP_TAC);; e (NEW_GOAL `dist (s,u1:real^3) = sqrt(&2)`);; e (REWRITE_TAC[GSYM (ASSUME `dist (u0:real^3, s) = sqrt (&2)`)]);; e (REWRITE_WITH `dist (u0,s:real^3) = dist (s,u0)`);; e (NORM_ARITH_TAC);; e (REWRITE_TAC[REAL_ARITH `a = b <=> a <= b /\ b <= a`]);; e (ASM_SIMP_TAC[]);; e (NEW_GOAL `dist (s,u2:real^3) = sqrt(&2)`);; e (REWRITE_TAC[GSYM (ASSUME `dist (u0:real^3, s) = sqrt (&2)`)]);; e (REWRITE_WITH `dist (u0,s:real^3) = dist (s,u0)`);; e (NORM_ARITH_TAC);; e (REWRITE_TAC[REAL_ARITH `a = b <=> a <= b /\ b <= a`]);; e (ASM_SIMP_TAC[]);; e (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} = 4`);; e (REWRITE_TAC[ARITH_RULE `4 = 3 + 1`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);; e (MATCH_MP_TAC Marchal_cells_3.BARV_CARD_LEMMA);; e (EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]);; e (NEW_GOAL `~(u0 = u1:real^3) /\ ~(u0 = u2) /\ ~(u0 = u3) /\ ~(u1 = u2) /\ ~(u1 = u3) /\ ~(u2 = u3)`);; e (REPEAT STRIP_TAC);; e (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);; e (REWRITE_TAC[ASSUME `u0 = u1:real^3`; SET_RULE `{u1, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]);; e (ASM_ARITH_TAC);; e (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);; e (REWRITE_TAC[ASSUME `u0 = u2:real^3`; SET_RULE `{u2, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]);; e (ASM_ARITH_TAC);; e (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);; e (REWRITE_TAC[ASSUME `u0 = u3:real^3`; SET_RULE `{u3, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]);; e (ASM_ARITH_TAC);; e (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);; e (REWRITE_TAC[ASSUME `u1 = u2:real^3`; SET_RULE `{u0, u2, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ]);; e (ASM_ARITH_TAC);; e (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);; e (REWRITE_TAC[ASSUME `u1 = u3:real^3`; SET_RULE `{u0, u3, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ]);; e (ASM_ARITH_TAC);; e (NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);; e (REWRITE_TAC[ASSUME `u2 = u3:real^3`; SET_RULE `{u0, u1, u3, u3} = {u0,u1,u3}`;Geomdetail.CARD3 ]);; e (ASM_ARITH_TAC);; e (NEW_GOAL `VX V X = {u0,u1,u2}`);; e (REWRITE_WITH `VX V X = V INTER X`);; e (MATCH_MP_TAC Hdtfnfz.HDTFNFZ);; e (EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `3`);; e (ASM_REWRITE_TAC[]);; e (REWRITE_WITH `X = mcell 3 V ul`);; e (ASM_REWRITE_TAC[]);; e (REWRITE_WITH `V INTER mcell 3 V ul = set_of_list (truncate_simplex (3 - 1) ul)`);; e (MATCH_MP_TAC Lepjbdj.LEPJBDJ);; e (ASM_REWRITE_TAC[ARITH_RULE `1 <= 3 /\ 3 <= 4`]);; e (REWRITE_WITH ` mcell 3 V [u0; u1; u2; u3] = X`);; e (ASM_REWRITE_TAC[]);; e (ASM_REWRITE_TAC[]);; e (ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`; TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]);; e (UNDISCH_TAC `X = convex hull (set_of_list vl UNION {mxi V ul})`);; e (EXPAND_TAC "vl" THEN REWRITE_TAC[set_of_list; TRUNCATE_SIMPLEX_EXPLICIT_2; ASSUME `ul = [u0;u1;u2;u3:real^3]`; SET_RULE `{a,b,c} UNION {d} = {a,b,c,d}`]);; e (REWRITE_WITH `mxi V [u0; u1; u2; u3] = s`);; e (EXPAND_TAC "s" THEN AP_TERM_TAC THEN ASM_REWRITE_TAC[]);; e (STRIP_TAC);; e (NEW_GOAL `~coplanar {u0,u1,u2,s:real^3}`);; e (ONCE_REWRITE_TAC[GSYM COPLANAR_AFFINE_HULL_COPLANAR]);; e (STRIP_TAC);; e (NEW_GOAL `NULLSET X`);; e (MATCH_MP_TAC COPLANAR_IMP_NEGLIGIBLE);; e (REWRITE_TAC[ASSUME `X = convex hull {u0, u1, u2, s:real^3}`]);; e (MATCH_MP_TAC COPLANAR_SUBSET);; e (EXISTS_TAC `affine hull {u0, u1, u2, s:real^3}`);; e (ASM_REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]);; e (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);; e (NEW_GOAL `CARD {u0, u1, u2, s:real^3} = 4`);; e (NEW_GOAL `CARD {u0, u1, u2, s:real^3} <= 4`);; e (REWRITE_TAC[Geomdetail.CARD4]);; e (ASM_CASES_TAC `CARD {u0, u1, u2, s:real^3} <= 3`);; e (NEW_GOAL `F`);; e (UNDISCH_TAC `~coplanar {u0, u1, u2, s:real^3}`);; e (REWRITE_TAC[] THEN MATCH_MP_TAC COPLANAR_SMALL);; e (ASM_REWRITE_TAC[Geomdetail.FINITE6]);; e (UP_ASM_TAC THEN MESON_TAC[]);; e (ASM_ARITH_TAC);; e (NEW_GOAL `~(u0 = s:real^3) /\ ~(u1 = s) /\ ~(u2 = s)`);; e (REPEAT STRIP_TAC);; e (NEW_GOAL `CARD {u0, u1, u2,s:real^3} <= 3`);; e (REWRITE_TAC[ASSUME `u0 = s:real^3`; SET_RULE `{s, u1, u2, s} = {s,u1,u2}`;Geomdetail.CARD3 ]);; e (ASM_ARITH_TAC);; e (NEW_GOAL `CARD {u0, u1, u2, s:real^3} <= 3`);; e (REWRITE_TAC[ASSUME `u1 = s:real^3`; SET_RULE `{u0, s, u2, s} = {u0,u2,s}`;Geomdetail.CARD3 ]);; e (ASM_ARITH_TAC);; e (NEW_GOAL `CARD {u0, u1, u2, s:real^3} <= 3`);; e (REWRITE_TAC[ASSUME `u2 = s:real^3`; SET_RULE `{u0, u1, s, s} = {u0,u1,s}`;Geomdetail.CARD3 ]);; e (ASM_ARITH_TAC);; (* ========================================================================= *) e (ABBREV_TAC `y4 = dist (u1:real^3, u2)`);; e (ABBREV_TAC `y5 = dist (u0:real^3, u2)`);; e (ABBREV_TAC `y6 = dist (u0:real^3, u1)`);; e (REWRITE_WITH `vol X = vol_y sqrt2 sqrt2 sqrt2 y4 y5 y6 /\ sol u0 X = sol_y y5 y6 sqrt2 sqrt2 sqrt2 y4 /\ sol u1 X = sol_y y6 y4 sqrt2 sqrt2 sqrt2 y5 /\ sol u2 X = sol_y y4 y5 sqrt2 sqrt2 sqrt2 y6 /\ dihX V X (u0,u1) = dih_y y6 y4 sqrt2 sqrt2 sqrt2 y5 /\ dihX V X (u0,u2) = dih_y y5 y6 sqrt2 sqrt2 sqrt2 y4 /\ dihX V X (u1,u2) = dih_y y4 y5 sqrt2 sqrt2 sqrt2 y6 /\ gammaX V X lmfun = gamma3f y4 y5 y6 sqrt2 lmfun`);; e (FIRST_ASSUM MATCH_MP_TAC);; e (MP_TAC (ASSUME `packing V`));; e (REWRITE_TAC[packing] THEN STRIP_TAC);; e (EXPAND_TAC "y4" THEN EXPAND_TAC "y5" THEN EXPAND_TAC "y6");; e (REPEAT STRIP_TAC);; e (ASM_SIMP_TAC[]);; e (ASM_SIMP_TAC[]);; e (ASM_SIMP_TAC[]);; e (NEW_GOAL `dist (u1,u2) <= dist (s,u1) + dist (s,u2:real^3)`);; e (NORM_ARITH_TAC);; e (ASM_REAL_ARITH_TAC);; e (NEW_GOAL `dist (u0,u2) <= dist (s,u2) + dist (u0,s:real^3)`);; e (NORM_ARITH_TAC);; e (ASM_REAL_ARITH_TAC);; e (NEW_GOAL `dist (u0,u1) <= dist (s,u1) + dist (u0,s:real^3)`);; e (NORM_ARITH_TAC);; e (ASM_REAL_ARITH_TAC);; e (REWRITE_TAC[GSYM d3]);; e (REWRITE_WITH `eta_y (d3 u1 u2) (d3 u0 u2) (d3 u0 u1) = radV {u0,u1,u2}`);; e (ONCE_REWRITE_TAC[EQ_SYM_EQ]);; e (MATCH_MP_TAC Collect_geom.RADV_FORMULAR);; e (MATCH_MP_TAC NOT_COPLANAR_NOT_COLLINEAR);; e (EXISTS_TAC `s:real^3`);; e (ASM_REWRITE_TAC[]);; e (REWRITE_WITH `radV {u0:real^3,u1,u2} = hl (truncate_simplex 2 (ul:(real^3)list))`);; e (REWRITE_TAC[TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list; HL; ASSUME `ul = [u0;u1;u2;u3:real^3]`]);; e (ASM_REWRITE_TAC[]);; e (STRIP_TAC);; e (NEW_GOAL `F`);; e (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);; e (UP_ASM_TAC THEN ASM_REWRITE_TAC[]);; (* --- Finish the case 3-cell, the remains are 1-cell and 2-cell ---------- *) (* ======================================================================== *)