(* ========================================================================= *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* *)
(* Author : VU KHAC KY *)
(* Book lemma: TSKAJXY *)
(* Chapter : Packing (Clusters) *)
(* Date: November 2013 *)
(* *)
(* ========================================================================= *)
(*
This does the special cases of Lemma TSKAJXY for 0, 3, and 4-cells
*)
module Tskajxy_034 = struct
open Sphere;;
open Euler_main_theorem;;
open Pack_defs;;
open Pack_concl;;
open Pack1;;
open Pack2;;
open Packing3;;
open Rogers;;
open Vukhacky_tactics;;
open Marchal_cells;;
open Emnwuus;;
(* open Marchal_cells_2;; *)
open Marchal_cells_2_new;;
open Urrphbz1;;
open Lepjbdj;;
open Hdtfnfz;;
open Rvfxzbu;;
open Sltstlo;;
open Urrphbz2;;
open Urrphbz3;;
open Ynhyjit;;
open Njiutiu;;
open Tezffsk;;
open Qzksykg;;
open Ddzuphj;;
open Ajripqn;;
open Qzyzmjc;;
open Upfzbzm_support_lemmas;;
open Marchal_cells_3;;
open Grutoti;;
open Kizhltl;;
open Sum_gammax_lmfun_estimate;;
open Upfzbzm;;
open Rdwkarc;;
open Ineq;;
open Merge_ineq;;
open Hales_tactic;;
open Tskajxy_lemmas;;
(* ======================================================================== *)
let cell3_from_ineq =
`!y4 y5 y6.
&2 <= y4 /\
&2 <= y5 /\
&2 <= y6 /\
y4 <= &2 * sqrt (&2) /\
y5 <= &2 * sqrt (&2) /\
y6 <= &2 * sqrt (&2) /\
eta_y y4 y5 y6 < sqrt (&2)
==> &0 <= gamma3f y4 y5 y6 sqrt2 lmfun`;;
let GRKIBMP_concl =
`!y. &2 <= y /\ y <= sqrt8 ==>
&0 <= gamma2_x_div_azim_v2 (h0cut y) (y*y)`;;
let tsk_hyp_new = mk_conj(GRKIBMP_concl,
mk_conj(cell3_from_ineq,tsk_hyp));;
g (mk_imp(tsk_hyp_new,`TSKAJXY_statement_special_case`));;
let TSKAJXY_034 = Prove_by_refinement.prove_by_refinement(
(mk_imp(tsk_hyp_new,`TSKAJXY_statement_special_case`)),
(* {{{ proof *)
[
(STRIP_TAC);
(REWRITE_TAC[TSKAJXY_statement_special_case; mcell_set; IN_ELIM_THM]);
(REWRITE_TAC[IN]);
(REPEAT STRIP_TAC);
(ASM_CASES_TAC `NULLSET X`);
(REWRITE_TAC[gammaX]);
(MATCH_MP_TAC (REAL_ARITH `x = &0 /\ y = &0 /\ z = &0 ==> x - y + z >= &0`));
(REWRITE_TAC[total_solid; REAL_ENTIRE]);
(REPEAT STRIP_TAC);
(MATCH_MP_TAC MEASURE_EQ_0);
BY((ASM_REWRITE_TAC[]));
(DISJ2_TAC);
(REWRITE_WITH `VX V X = {}`);
(REWRITE_TAC[VX]);
BY((ASM_REWRITE_TAC[]));
BY((REWRITE_TAC[SUM_CLAUSES]));
(DISJ2_TAC);
(REWRITE_WITH `edgeX V X = {}`);
(REWRITE_TAC[edgeX]);
(REWRITE_WITH `VX V X = {}`);
(REWRITE_TAC[VX]);
BY((ASM_REWRITE_TAC[]));
(ONCE_REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`]);
BY((SET_TAC[]));
BY((REWRITE_TAC[SUM_CLAUSES]));
(NEW_GOAL `~(X:real^3->bool = {})`);
BY((STRIP_TAC THEN SWITCH_TAC THEN UP_ASM_TAC THEN REWRITE_TAC[ASSUME `X:real^3->bool = {}`; NEGLIGIBLE_EMPTY]));
(ASM_CASES_TAC `i >= 4`);
(NEW_GOAL `X = mcell4 V ul`);
(ASM_REWRITE_TAC[]);
BY((ASM_SIMP_TAC[MCELL_EXPLICIT]));
(UP_ASM_TAC THEN REWRITE_TAC[mcell4]);
(COND_CASES_TAC);
(NEW_GOAL `?u0 u1 u2 u3. ul = [u0; u1; u2; u3:real^3]`);
(MATCH_MP_TAC BARV_3_EXPLICIT);
BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]));
(UP_ASM_TAC THEN STRIP_TAC);
(REWRITE_TAC[ASSUME `ul = [u0; u1; u2; u3:real^3]`; set_of_list]);
(STRIP_TAC);
(ABBREV_TAC `y1 = dist (u0:real^3, u1)`);
(ABBREV_TAC `y2 = dist (u0:real^3, u2)`);
(ABBREV_TAC `y3 = dist (u0:real^3, u3)`);
(ABBREV_TAC `y4 = dist (u2:real^3, u3)`);
(ABBREV_TAC `y5 = dist (u1:real^3, u3)`);
(ABBREV_TAC `y6 = dist (u1:real^3, u2)`);
(NEW_GOAL `VX V X = {u0,u1,u2,u3}`);
(REWRITE_WITH `VX V X = V INTER X`);
(MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
(EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
BY((ASM_REWRITE_TAC[]));
(REWRITE_WITH `X = mcell 4 V ul`);
(ASM_REWRITE_TAC[]);
BY((MESON_TAC[ARITH_RULE `4 >= 4`; ASSUME `i >= 4`; MCELL_EXPLICIT]));
(REWRITE_WITH `V INTER mcell 4 V ul = set_of_list (truncate_simplex (4 - 1) ul)`);
(MATCH_MP_TAC Lepjbdj.LEPJBDJ);
(ASM_REWRITE_TAC[ARITH_RULE `1 <= 4 /\ 4 <= 4`]);
(REWRITE_WITH ` mcell 4 V [u0; u1; u2; u3] = X`);
(ASM_REWRITE_TAC[]);
BY((MESON_TAC[ARITH_RULE `4 >= 4`; ASSUME `i >= 4`; MCELL_EXPLICIT]));
BY((ASM_REWRITE_TAC[]));
BY((ASM_REWRITE_TAC[ARITH_RULE `4 - 1 = 3`; TRUNCATE_SIMPLEX_EXPLICIT_3; set_of_list]));
(REWRITE_WITH `vol X = vol_y y1 y2 y3 y4 y5 y6 /\ gammaX V X lmfun = gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun`);
(MATCH_MP_TAC gammaX_gamm4fgcy);
(EXISTS_TAC `ul:(real^3)list`);
(EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);
(EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
(EXISTS_TAC `i:num`);
BY((ASM_REWRITE_TAC[]));
(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)`);
(MATCH_MP_TAC TSKAJXY_DERIVED4);
BY((ASM_REWRITE_TAC[]));
(UP_ASM_TAC THEN REWRITE_TAC[ineq; MESON[] `a ==> b ==> c <=> (a /\ b) ==> c`] THEN STRIP_TAC);
(FIRST_ASSUM MATCH_MP_TAC);
(ASM_REWRITE_TAC[]);
(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`);
(REWRITE_TAC[critical_edge_y]);
(REPEAT STRIP_TAC);
(NEW_GOAL `{u0:real^3, u1} IN critical_edgeX V X`);
(REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);
(EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);
(REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3`);
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
(STRIP_TAC);
BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
(STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y1`);
(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`]);
BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC));
BY((ASM_REAL_ARITH_TAC));
BY((ASM_REAL_ARITH_TAC));
BY((ASM_SET_TAC[]));
(NEW_GOAL `{u0:real^3, u2} IN critical_edgeX V X`);
(REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);
(EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u2:real^3`);
(REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u2:real^3`);
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
(STRIP_TAC);
BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
(STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y2`);
(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`]);
BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC));
BY((ASM_REAL_ARITH_TAC));
BY((ASM_REAL_ARITH_TAC));
BY((ASM_SET_TAC[]));
(NEW_GOAL `{u0:real^3, u3} IN critical_edgeX V X`);
(REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);
(EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u3:real^3`);
(REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u3:real^3`);
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
(STRIP_TAC);
BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
(STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y3`);
(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`]);
BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC));
BY((ASM_REAL_ARITH_TAC));
BY((ASM_REAL_ARITH_TAC));
BY((ASM_SET_TAC[]));
(NEW_GOAL `{u2:real^3, u3} IN critical_edgeX V X`);
(REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);
(EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
(REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
(STRIP_TAC);
BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
(STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y4`);
(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`]);
BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC));
BY((ASM_REAL_ARITH_TAC));
BY((ASM_REAL_ARITH_TAC));
BY((ASM_SET_TAC[]));
(NEW_GOAL `{u1:real^3, u3} IN critical_edgeX V X`);
(REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);
(EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u3:real^3`);
(REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u3:real^3`);
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
(STRIP_TAC);
BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
(STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y5`);
(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`]);
BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC));
BY((ASM_REAL_ARITH_TAC));
BY((ASM_REAL_ARITH_TAC));
BY((ASM_SET_TAC[]));
(NEW_GOAL `{u1:real^3, u2} IN critical_edgeX V X`);
(REWRITE_TAC[critical_edgeX; IN; IN_ELIM_THM]);
(EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3`);
(REWRITE_TAC[HL_2; edgeX; IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3`);
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
(STRIP_TAC);
BY((ONCE_REWRITE_TAC[MESON[IN] `s t <=> t IN s`] THEN SET_TAC[]));
(STRIP_TAC THEN UNDISCH_TAC `&2 * hminus <= y6`);
(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`]);
BY((MP_TAC Nonlinear_lemma.hminus_prop THEN REAL_ARITH_TAC));
BY((ASM_REAL_ARITH_TAC));
BY((ASM_REAL_ARITH_TAC));
BY((ASM_SET_TAC[]));
(REWRITE_WITH `&0 < delta_y y1 y2 y3 y4 y5 y6 <=> &0 < sqrt (delta_y y1 y2 y3 y4 y5 y6)`);
(ONCE_REWRITE_TAC[EQ_SYM_EQ]);
(MATCH_MP_TAC SQRT_LT_0);
(REWRITE_TAC[delta_y]);
(ABBREV_TAC `x1 = y1 * y1` THEN ABBREV_TAC `x2 = y2 * y2`);
(ABBREV_TAC `x3 = y3 * y3` THEN ABBREV_TAC `x4 = y4 * y4`);
(ABBREV_TAC `x5 = y5 * y5` THEN ABBREV_TAC `x6 = y6 * y6`);
(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)`);
(MATCH_MP_TAC Delta_x.COMPUTE_DELTA_X);
(REWRITE_TAC[xlist; ylist]);
(REPEAT LET_TAC);
(EXPAND_TAC "x1" THEN EXPAND_TAC "x2" THEN EXPAND_TAC "x3");
(EXPAND_TAC "x4" THEN EXPAND_TAC "x5" THEN EXPAND_TAC "x6");
(UP_ASM_TAC THEN REWRITE_TAC[PAIR_EQ; GSYM REAL_POW_2]);
(ASM_REWRITE_TAC[]);
(STRIP_TAC);
BY((ASM_REWRITE_TAC[]));
(REPEAT LET_TAC);
(REWRITE_TAC[REAL_ARITH `&0 <= &4 * a <=> &0 <= a`]);
BY((REWRITE_TAC[Real_ext.REAL_LE_POW_2]));
(ONCE_REWRITE_TAC[REAL_ARITH `&0 < a <=> &0 < a / &12`]);
(REWRITE_WITH `sqrt (delta_y y1 y2 y3 y4 y5 y6) / &12 = vol (convex hull {u0,u1,u2,u3})`);
(ONCE_REWRITE_TAC[EQ_SYM_EQ]);
(REWRITE_TAC[delta_y; GSYM REAL_POW_2]);
(EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");
(EXPAND_TAC "y4" THEN EXPAND_TAC "y5" THEN EXPAND_TAC "y6");
BY((REWRITE_TAC[VOLUME_OF_CLOSED_TETRAHEDRON]));
(REWRITE_TAC[GSYM (ASSUME `X = convex hull {u0, u1, u2, u3:real^3}`)]);
(REWRITE_WITH `&0 < vol X <=> ~NULLSET X`);
(MATCH_MP_TAC MEASURABLE_MEASURE_POS_LT);
(REWRITE_TAC[ASSUME `X = convex hull {u0, u1, u2, u3:real^3}`]);
(MATCH_MP_TAC MEASURABLE_CONVEX_HULL);
(MATCH_MP_TAC FINITE_IMP_BOUNDED);
BY((REWRITE_TAC[Geomdetail.FINITE6]));
BY((ASM_REWRITE_TAC[]));
(ASM_REWRITE_TAC[]);
(NEW_GOAL `!u v. {u,v} IN edgeX V X ==> (#2.0 <= dist (u,v) /\ dist(u,v) <= sqrt8)`);
(REPEAT GEN_TAC);
(REWRITE_TAC[edgeX; IN]);
(REWRITE_TAC[MESON[IN] `VX V X x <=> x IN VX V X`]);
(ASM_REWRITE_TAC[IN_ELIM_THM]);
(STRIP_TAC);
(MP_TAC (ASSUME `packing V`));
(REWRITE_TAC[packing; REAL_ARITH `#2.0 = &2`] THEN STRIP_TAC);
(STRIP_TAC);
(FIRST_ASSUM MATCH_MP_TAC);
(NEW_GOAL `u:real^3 IN {u0,u1,u2,u3} /\ v IN {u0,u1,u2,u3}`);
(DEL_TAC THEN UP_ASM_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC);
BY((SET_TAC[]));
(NEW_GOAL `{u0,u1,u2,u3:real^3} SUBSET V`);
(REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
(MATCH_MP_TAC BARV_SUBSET);
BY((EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]));
(STRIP_TAC);
(REWRITE_TAC[MESON[IN] `(V:real^3->bool) x <=> x IN V`]);
BY((UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]));
(STRIP_TAC);
(REWRITE_TAC[MESON[IN] `(V:real^3->bool) x <=> x IN V`]);
BY((UP_ASM_TAC THEN UP_ASM_TAC THEN SET_TAC[]));
(DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC);
BY((SET_TAC[]));
(ABBREV_TAC `s = circumcenter {u0,u1,u2,u3:real^3}`);
(NEW_GOAL `dist (u,v:real^3) <= dist (s,u) + dist (s, v)`);
BY((NORM_ARITH_TAC));
(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)`);
(MATCH_MP_TAC Rogers.OAPVION2);
(REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
(MATCH_MP_TAC Rogers.BARV_AFFINE_INDEPENDENT);
BY((EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]));
(NEW_GOAL `dist (s,u) + dist (s,v:real^3) <= sqrt8`);
(REWRITE_TAC[Nonlinear_lemma.sqrt8_sqrt2; sqrt2]);
(MATCH_MP_TAC (REAL_ARITH `a < x /\ b < x ==> a + b <= &2 * x`));
(STRIP_TAC);
(REWRITE_WITH `dist (s,u:real^3) = radV {u0,u1,u2,u3:real^3}`);
(ONCE_REWRITE_TAC[EQ_SYM_EQ]);
(EXPAND_TAC "s");
(FIRST_ASSUM MATCH_MP_TAC);
(DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN DEL_TAC);
(UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC);
BY((SET_TAC[]));
(REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
(REWRITE_TAC[GSYM HL]);
BY((ASM_REWRITE_TAC[]));
(REWRITE_WITH `dist (s,v:real^3) = radV {u0,u1,u2,u3:real^3}`);
(ONCE_REWRITE_TAC[EQ_SYM_EQ]);
(EXPAND_TAC "s");
(FIRST_ASSUM MATCH_MP_TAC);
(DEL_TAC THEN DEL_TAC THEN DEL_TAC THEN DEL_TAC);
(UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC THEN UP_ASM_TAC);
BY((SET_TAC[]));
(REWRITE_TAC[GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
(REWRITE_TAC[GSYM HL]);
BY((ASM_REWRITE_TAC[]));
BY((ASM_REAL_ARITH_TAC));
(NEW_GOAL `CARD {u0, u1, u2, u3:real^3} = 4`);
(REWRITE_TAC[ARITH_RULE `4 = 3 + 1`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
(MATCH_MP_TAC Marchal_cells_3.BARV_CARD_LEMMA);
BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]));
(NEW_GOAL `~(u0 = u1:real^3) /\ ~(u0 = u2) /\ ~(u0 = u3) /\ ~(u1 = u2) /\ ~(u1 = u3) /\ ~(u2 = u3)`);
(REPEAT STRIP_TAC);
(NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
BY((REWRITE_TAC[ASSUME `u0 = u1:real^3`; SET_RULE `{u1, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]));
BY((ASM_ARITH_TAC));
(NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
BY((REWRITE_TAC[ASSUME `u0 = u2:real^3`; SET_RULE `{u2, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]));
BY((ASM_ARITH_TAC));
(NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
BY((REWRITE_TAC[ASSUME `u0 = u3:real^3`; SET_RULE `{u3, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]));
BY((ASM_ARITH_TAC));
(NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
BY((REWRITE_TAC[ASSUME `u1 = u2:real^3`; SET_RULE `{u0, u2, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ]));
BY((ASM_ARITH_TAC));
(NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
BY((REWRITE_TAC[ASSUME `u1 = u3:real^3`; SET_RULE `{u0, u3, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ]));
BY((ASM_ARITH_TAC));
(NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
BY((REWRITE_TAC[ASSUME `u2 = u3:real^3`; SET_RULE `{u0, u1, u3, u3} = {u0,u1,u3}`;Geomdetail.CARD3 ]));
BY((ASM_ARITH_TAC));
(NEW_GOAL `edgeX V X = {{u0,u1:real^3}, {u0,u2}, {u0,u3}, {u1,u2}, {u1,u3}, {u2,u3}}`);
(REWRITE_TAC[edgeX]);
(ONCE_REWRITE_TAC[SET_EQ_LEMMA]);
(REWRITE_TAC[IN_ELIM_THM]);
(REPEAT STRIP_TAC);
(UNDISCH_TAC `VX V X u` THEN UNDISCH_TAC `VX V X v`);
(REWRITE_TAC[MESON[IN] `VX V X s <=> s IN VX V X`]);
(ASM_REWRITE_TAC[SET_RULE `v IN {u0, u1, u2, u3} <=> v = u0 \/ v = u1 \/ v = u2 \/ v = u3`]);
(REPEAT STRIP_TAC);
(NEW_GOAL `F`);
BY((ASM_MESON_TAC[]));
BY((ASM_MESON_TAC[]));
(REWRITE_WITH `{u,v} = {v,u:real^3}`);
BY((SET_TAC[]));
BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
(REWRITE_WITH `{u,v} = {v,u:real^3}`);
BY((SET_TAC[]));
BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
(REWRITE_WITH `{u,v} = {v,u:real^3}`);
BY((SET_TAC[]));
BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
(NEW_GOAL `F`);
BY((ASM_MESON_TAC[]));
BY((ASM_MESON_TAC[]));
(REWRITE_WITH `{u,v} = {v,u:real^3}`);
BY((SET_TAC[]));
BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
(REWRITE_WITH `{u,v} = {v,u:real^3}`);
BY((SET_TAC[]));
BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
(NEW_GOAL `F`);
BY((ASM_MESON_TAC[]));
BY((ASM_MESON_TAC[]));
(REWRITE_WITH `{u,v} = {v,u:real^3}`);
BY((SET_TAC[]));
BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
(NEW_GOAL `F`);
BY((ASM_MESON_TAC[]));
BY((ASM_MESON_TAC[]));
(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`]);
(REWRITE_TAC[MESON[IN] `VX V X s <=> s IN VX V X`]);
(ASM_REWRITE_TAC[SET_RULE `v IN {u0, u1, u2, u3} <=> v = u0 \/ v = u1 \/ v = u2 \/ v = u3`]);
(REPEAT STRIP_TAC);
BY((EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u1:real^3` THEN ASM_REWRITE_TAC[]));
BY((EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u2:real^3` THEN ASM_REWRITE_TAC[]));
BY((EXISTS_TAC `u0:real^3` THEN EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[]));
BY((EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN ASM_REWRITE_TAC[]));
BY((EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[]));
BY((EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3` THEN ASM_REWRITE_TAC[]));
(STRIP_TAC);
(EXPAND_TAC "y1");
(FIRST_ASSUM MATCH_MP_TAC);
BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
(STRIP_TAC);
(EXPAND_TAC "y2");
(FIRST_ASSUM MATCH_MP_TAC);
BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
(STRIP_TAC);
(EXPAND_TAC "y3");
(FIRST_ASSUM MATCH_MP_TAC);
BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
(STRIP_TAC);
(EXPAND_TAC "y4");
(FIRST_ASSUM MATCH_MP_TAC);
BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
(STRIP_TAC);
(EXPAND_TAC "y5");
(FIRST_ASSUM MATCH_MP_TAC);
BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
(STRIP_TAC);
(EXPAND_TAC "y6");
(FIRST_ASSUM MATCH_MP_TAC);
BY((ASM_REWRITE_TAC[] THEN SET_TAC[]));
(REWRITE_WITH `rad2_y y1 y2 y3 y4 y5 y6 = radV {u0,u1,u2,u3:real^3} pow 2`);
(ONCE_REWRITE_TAC[EQ_SYM_EQ]);
(REWRITE_TAC[rad2_y; y_of_x]);
(GMATCH_SIMP_TAC (REWRITE_RULE[LET_DEF;LET_END_DEF] Merge_ineq.GDRQXLGv2));
(STRIP_TAC);
(STRIP_TAC);
(REWRITE_TAC[ARITH_RULE `4 = 3 + 1`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
(MATCH_MP_TAC Marchal_cells_3.BARV_CARD_LEMMA);
BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]));
(REWRITE_TAC[Collect_geom.coplanar_alt]);
(REWRITE_TAC[GSYM Trigonometry2.coplanar1]);
(REWRITE_TAC[coplanar] THEN STRIP_TAC);
(NEW_GOAL `affine hull {u0, u1, u2, u3:real^3} SUBSET affine hull (affine hull {u, v, w})`);
BY((ASM_SIMP_TAC[Marchal_cells_2_new.AFFINE_SUBSET_KY_LEMMA]));
(UP_ASM_TAC THEN REWRITE_WITH `affine hull (affine hull {u, v, w}) = affine hull {u:real^3, v, w}`);
BY((REWRITE_TAC[AFFINE_HULL_EQ; AFFINE_AFFINE_HULL]));
(STRIP_TAC);
(NEW_GOAL `NULLSET X`);
(MATCH_MP_TAC NEGLIGIBLE_SUBSET);
(EXISTS_TAC `affine hull {u0, u1, u2, u3:real^3}`);
(STRIP_TAC);
(MATCH_MP_TAC NEGLIGIBLE_SUBSET);
(EXISTS_TAC `affine hull {u,v,w:real^3}`);
(REWRITE_TAC[NEGLIGIBLE_AFFINE_HULL_3]);
BY((ASM_REWRITE_TAC[]));
(REWRITE_TAC[ASSUME `X = mcell i V ul`]);
(REWRITE_WITH `mcell i V ul = mcell4 V ul`);
BY((MESON_TAC[ARITH_RULE `4 >= 4`; MCELL_EXPLICIT; ASSUME `i >= 4`]));
(REWRITE_TAC[mcell4]);
(COND_CASES_TAC);
BY((ASM_REWRITE_TAC[set_of_list; CONVEX_HULL_SUBSET_AFFINE_HULL]));
BY((SET_TAC[]));
BY((UP_ASM_TAC THEN ASM_REWRITE_TAC[]));
(REWRITE_TAC[GSYM REAL_POW_2]);
(EXPAND_TAC "y1" THEN EXPAND_TAC "y2" THEN EXPAND_TAC "y3");
(EXPAND_TAC "y4" THEN EXPAND_TAC "y5" THEN EXPAND_TAC "y6");
BY((REWRITE_TAC[]));
(REWRITE_WITH `radV {u0, u1, u2, u3:real^3} = hl (ul:(real^3)list)`);
BY((ASM_REWRITE_TAC[HL;set_of_list]));
(REWRITE_WITH `hl (ul:(real^3)list) pow 2 < &2 <=> sqrt (hl ul pow 2) < sqrt (&2)`);
(ONCE_REWRITE_TAC[EQ_SYM_EQ]);
(MATCH_MP_TAC Real_ext.REAL_PROP_LT_SQRT);
BY((REWRITE_TAC[REAL_LE_POW_2] THEN REAL_ARITH_TAC));
(REWRITE_WITH `sqrt (hl (ul:(real^3)list) pow 2) = hl ul`);
(MATCH_MP_TAC POW_2_SQRT);
(MATCH_MP_TAC (REAL_ARITH `&0 < a ==> &0 <= a`));
(NEW_GOAL `hl (truncate_simplex 1 ul) <= hl (ul:(real^3)list)`);
(MATCH_MP_TAC Rogers.HL_DECREASE);
(EXISTS_TAC `V:real^3->bool` THEN EXISTS_TAC `3`);
BY((ASM_REWRITE_TAC[IN; ARITH_RULE `1 <= 3`]));
(NEW_GOAL `&0 < hl (truncate_simplex 1 (ul:(real^3)list))`);
(MATCH_MP_TAC Marchal_cells_2_new.BARV_IMP_HL_1_POS_LT);
BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]));
BY((ASM_REAL_ARITH_TAC));
BY((ASM_REWRITE_TAC[]));
(STRIP_TAC);
(NEW_GOAL `F`);
BY((UP_ASM_TAC THEN ASM_REWRITE_TAC[]));
BY((UP_ASM_TAC THEN ASM_REWRITE_TAC[]));
(COMMENT "END OF 4-CELL CASE");
(ASM_CASES_TAC `i = 0`);
(NEW_GOAL `VX V X = {}`);
(REWRITE_WITH `VX V X = V INTER X`);
(MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
(EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `i:num`);
BY((ASM_REWRITE_TAC[]));
(ASM_REWRITE_TAC[]);
(MATCH_MP_TAC Lepjbdj.LEPJBDJ_0);
BY((ASM_REWRITE_TAC[]));
(NEW_GOAL `edgeX V X = {}`);
(REWRITE_TAC[edgeX]);
(ASM_REWRITE_TAC[MESON[IN] `{} x <=> x IN {}`; SET_RULE `x IN {} <=> F`]);
BY((SET_TAC[]));
(REWRITE_TAC[gammaX]);
(MATCH_MP_TAC (REAL_ARITH `b = &0 /\ c = &0 /\ &0 <= a ==> a - b + c >= &0`));
(REPEAT STRIP_TAC);
BY((ASM_REWRITE_TAC[total_solid; SUM_CLAUSES] THEN REAL_ARITH_TAC));
BY((ASM_REWRITE_TAC[SUM_CLAUSES] THEN REAL_ARITH_TAC));
(MATCH_MP_TAC MEASURE_POS_LE);
(ASM_REWRITE_TAC[] THEN MATCH_MP_TAC Urrphbz1.MEASURABLE_MCELL);
BY((ASM_REWRITE_TAC[]));
COMMENT "insert. thales. Jan 2013";
FIRST_X_ASSUM_ST `gamma3f` MP_TAC;
REPEAT (FIRST_X_ASSUM_ST `ineq` kill);
DISCH_TAC;
TYPIFY `i = 3` (C SUBGOAL_THEN ASSUME_TAC);
MATCH_MP_TAC (arith `~(i >= 4) /\ ~(i=0) /\ ~((i=1) \/ (i=2)) ==> (i = 3)`);
REPLICATE_TAC 9 (FIRST_X_ASSUM MP_TAC);
REPEAT (FIRST_X_ASSUM kill);
BY(MESON_TAC[]);
REPEAT (FIRST_X_ASSUM_ST `gamma4fgcy` kill);
COMMENT "end of insert";
(NEW_GOAL `X = mcell3 V ul`);
(ASM_REWRITE_TAC[]);
BY((ASM_SIMP_TAC[MCELL_EXPLICIT]));
(UP_ASM_TAC THEN REWRITE_TAC[mcell3]);
(COND_CASES_TAC);
(STRIP_TAC);
(NEW_GOAL `?u0 u1 u2 u3. ul = [u0; u1; u2; u3:real^3]`);
(MATCH_MP_TAC BARV_3_EXPLICIT);
BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]));
(UP_ASM_TAC THEN STRIP_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)`);
(MATCH_MP_TAC MXI_EXPLICIT);
(EXISTS_TAC `u1:real^3` THEN EXISTS_TAC `u2:real^3` THEN EXISTS_TAC `u3:real^3`);
BY((ASM_REWRITE_TAC[]));
(UP_ASM_TAC THEN STRIP_TAC);
(ABBREV_TAC `s2 = omega_list_n V ul 2`);
(ABBREV_TAC `s3 = omega_list_n V ul 3`);
(ABBREV_TAC `vl = truncate_simplex 2 (ul:(real^3)list)`);
(NEW_GOAL `s2 IN voronoi_list V vl`);
(EXPAND_TAC "s2" THEN EXPAND_TAC "vl");
(MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
BY((ARITH_TAC));
(NEW_GOAL `s3 IN voronoi_list V vl`);
(EXPAND_TAC "s3" THEN EXPAND_TAC "vl");
(MATCH_MP_TAC Rogers.OMEGA_LIST_N_IN_VORONOI_LIST_GEN);
(EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]);
BY((ARITH_TAC));
(NEW_GOAL `s IN voronoi_list V vl`);
(MATCH_MP_TAC (SET_RULE `(?x. s IN x /\ x SUBSET t)==> s IN t`));
(EXISTS_TAC `convex hull {s2,s3:real^3}`);
(STRIP_TAC);
BY((ASM_REWRITE_TAC[GSYM BETWEEN_IN_CONVEX_HULL]));
(NEW_GOAL `voronoi_list V vl = convex hull (voronoi_list V vl)`);
(ONCE_REWRITE_TAC[EQ_SYM_EQ]);
BY((REWRITE_TAC[CONVEX_HULL_EQ; Packing3.CONVEX_VORONOI_LIST]));
(ONCE_REWRITE_TAC[ASSUME `voronoi_list V vl = convex hull voronoi_list V vl`]);
(MATCH_MP_TAC Marchal_cells.CONVEX_HULL_SUBSET);
BY((ASM_SET_TAC[]));
(MP_TAC (ASSUME `s IN voronoi_list V vl`));
(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]);
(STRIP_TAC);
(NEW_GOAL `s IN voronoi_closed V u0 /\ s IN voronoi_closed V u1 /\ s IN voronoi_closed V (u2:real^3)`);
BY((UP_ASM_TAC THEN SET_TAC[]));
(UP_ASM_TAC THEN REWRITE_TAC[voronoi_closed; IN; IN_ELIM_THM] THEN STRIP_TAC);
(NEW_GOAL `u0 IN V /\ u1 IN V /\ u2 IN V /\ (u3:real^3) IN V`);
(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]`)]);
(MATCH_MP_TAC BARV_SUBSET);
BY((EXISTS_TAC `3` THEN ASM_REWRITE_TAC[]));
(FIRST_ASSUM MP_TAC THEN REWRITE_TAC[IN] THEN STRIP_TAC);
(NEW_GOAL `dist (s,u1:real^3) = sqrt(&2)`);
(REWRITE_TAC[GSYM (ASSUME `dist (u0:real^3, s) = sqrt (&2)`)]);
(REWRITE_WITH `dist (u0,s:real^3) = dist (s,u0)`);
BY((NORM_ARITH_TAC));
(REWRITE_TAC[REAL_ARITH `a = b <=> a <= b /\ b <= a`]);
BY((ASM_SIMP_TAC[]));
(NEW_GOAL `dist (s,u2:real^3) = sqrt(&2)`);
(REWRITE_TAC[GSYM (ASSUME `dist (u0:real^3, s) = sqrt (&2)`)]);
(REWRITE_WITH `dist (u0,s:real^3) = dist (s,u0)`);
BY((NORM_ARITH_TAC));
(REWRITE_TAC[REAL_ARITH `a = b <=> a <= b /\ b <= a`]);
BY((ASM_SIMP_TAC[]));
(NEW_GOAL `CARD {u0, u1, u2, u3:real^3} = 4`);
(REWRITE_TAC[ARITH_RULE `4 = 3 + 1`; GSYM set_of_list; GSYM (ASSUME `ul = [u0;u1;u2;u3:real^3]`)]);
(MATCH_MP_TAC Marchal_cells_3.BARV_CARD_LEMMA);
BY((EXISTS_TAC `V:real^3->bool` THEN ASM_REWRITE_TAC[]));
(NEW_GOAL `~(u0 = u1:real^3) /\ ~(u0 = u2) /\ ~(u0 = u3) /\ ~(u1 = u2) /\ ~(u1 = u3) /\ ~(u2 = u3)`);
(REPEAT STRIP_TAC);
(NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
BY((REWRITE_TAC[ASSUME `u0 = u1:real^3`; SET_RULE `{u1, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]));
BY((ASM_ARITH_TAC));
(NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
BY((REWRITE_TAC[ASSUME `u0 = u2:real^3`; SET_RULE `{u2, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]));
BY((ASM_ARITH_TAC));
(NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
BY((REWRITE_TAC[ASSUME `u0 = u3:real^3`; SET_RULE `{u3, u1, u2, u3} = {u1,u2,u3}`;Geomdetail.CARD3 ]));
BY((ASM_ARITH_TAC));
(NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
BY((REWRITE_TAC[ASSUME `u1 = u2:real^3`; SET_RULE `{u0, u2, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ]));
BY((ASM_ARITH_TAC));
(NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
BY((REWRITE_TAC[ASSUME `u1 = u3:real^3`; SET_RULE `{u0, u3, u2, u3} = {u0,u2,u3}`;Geomdetail.CARD3 ]));
BY((ASM_ARITH_TAC));
(NEW_GOAL `CARD {u0, u1, u2, u3:real^3} <= 3`);
BY((REWRITE_TAC[ASSUME `u2 = u3:real^3`; SET_RULE `{u0, u1, u3, u3} = {u0,u1,u3}`;Geomdetail.CARD3 ]));
BY((ASM_ARITH_TAC));
(NEW_GOAL `VX V X = {u0,u1,u2}`);
(REWRITE_WITH `VX V X = V INTER X`);
(MATCH_MP_TAC Hdtfnfz.HDTFNFZ);
(EXISTS_TAC `ul:(real^3)list` THEN EXISTS_TAC `3`);
BY((ASM_REWRITE_TAC[]));
(REWRITE_WITH `X = mcell 3 V ul`);
BY((ASM_REWRITE_TAC[]));
(REWRITE_WITH `V INTER mcell 3 V ul = set_of_list (truncate_simplex (3 - 1) ul)`);
(MATCH_MP_TAC Lepjbdj.LEPJBDJ);
(ASM_REWRITE_TAC[ARITH_RULE `1 <= 3 /\ 3 <= 4`]);
(REWRITE_WITH ` mcell 3 V [u0; u1; u2; u3] = X`);
BY((ASM_REWRITE_TAC[]));
BY((ASM_REWRITE_TAC[]));
BY((ASM_REWRITE_TAC[ARITH_RULE `3 - 1 = 2`; TRUNCATE_SIMPLEX_EXPLICIT_2; set_of_list]));
(UNDISCH_TAC `X = convex hull (set_of_list vl UNION {mxi V ul})`);
(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}`]);
(REWRITE_WITH `mxi V [u0; u1; u2; u3] = s`);
BY((EXPAND_TAC "s" THEN AP_TERM_TAC THEN ASM_REWRITE_TAC[]));
(STRIP_TAC);
(NEW_GOAL `~coplanar {u0,u1,u2,s:real^3}`);
(ONCE_REWRITE_TAC[GSYM COPLANAR_AFFINE_HULL_COPLANAR]);
(STRIP_TAC);
(NEW_GOAL `NULLSET X`);
(MATCH_MP_TAC COPLANAR_IMP_NEGLIGIBLE);
(REWRITE_TAC[ASSUME `X = convex hull {u0, u1, u2, s:real^3}`]);
(MATCH_MP_TAC COPLANAR_SUBSET);
(EXISTS_TAC `affine hull {u0, u1, u2, s:real^3}`);
BY((ASM_REWRITE_TAC[CONVEX_HULL_SUBSET_AFFINE_HULL]));
BY((UP_ASM_TAC THEN ASM_REWRITE_TAC[]));
(NEW_GOAL `CARD {u0, u1, u2, s:real^3} = 4`);
(NEW_GOAL `CARD {u0, u1, u2, s:real^3} <= 4`);
BY((REWRITE_TAC[Geomdetail.CARD4]));
(ASM_CASES_TAC `CARD {u0, u1, u2, s:real^3} <= 3`);
(NEW_GOAL `F`);
(UNDISCH_TAC `~coplanar {u0, u1, u2, s:real^3}`);
(REWRITE_TAC[] THEN MATCH_MP_TAC COPLANAR_SMALL);
BY((ASM_REWRITE_TAC[Geomdetail.FINITE6]));
BY((UP_ASM_TAC THEN MESON_TAC[]));
BY((ASM_ARITH_TAC));
(NEW_GOAL `~(u0 = s:real^3) /\ ~(u1 = s) /\ ~(u2 = s)`);
(REPEAT STRIP_TAC);
(NEW_GOAL `CARD {u0, u1, u2,s:real^3} <= 3`);
BY((REWRITE_TAC[ASSUME `u0 = s:real^3`; SET_RULE `{s, u1, u2, s} = {s,u1,u2}`;Geomdetail.CARD3 ]));
BY((ASM_ARITH_TAC));
(NEW_GOAL `CARD {u0, u1, u2, s:real^3} <= 3`);
BY((REWRITE_TAC[ASSUME `u1 = s:real^3`; SET_RULE `{u0, s, u2, s} = {u0,u2,s}`;Geomdetail.CARD3 ]));
BY((ASM_ARITH_TAC));
(NEW_GOAL `CARD {u0, u1, u2, s:real^3} <= 3`);
BY((REWRITE_TAC[ASSUME `u2 = s:real^3`; SET_RULE `{u0, u1, s, s} = {u0,u1,s}`;Geomdetail.CARD3 ]));
BY((ASM_ARITH_TAC));
(ABBREV_TAC `y4 = dist (u1:real^3, u2)`);
(ABBREV_TAC `y5 = dist (u0:real^3, u2)`);
(ABBREV_TAC `y6 = dist (u0:real^3, u1)`);
COMMENT "insert by thales, Jan 2013";
INTRO_TAC Tskajxy_lemmas.gammaX_gamma3f [`V`;`X`;`ul`;`u0`;`u1`;`u2`;`u3`;`y4`;`y5`;`y6`];
ASM_REWRITE_TAC[];
REPEAT WEAK_STRIP_TAC THEN ASM_REWRITE_TAC[arith `x >= &0 <=> &0 <= x`];
REPLICATE_TAC 8 (FIRST_X_ASSUM kill);
FIRST_X_ASSUM MATCH_MP_TAC;
TYPIFY `&2 <= y4 /\ &2 <= y5 /\ &2 <= y6` (C SUBGOAL_THEN ASSUME_TAC);
REPLICATE_TAC 3 (FIRST_X_ASSUM (SUBST1_TAC o SYM));
BY(ASM_MESON_TAC[packing]);
ASM_REWRITE_TAC[];
TYPIFY `y4 <= &2 * sqrt (&2) /\ y5 <= &2 * sqrt (&2) /\ y6 <= &2 * sqrt (&2)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
REPLICATE_TAC 3 (FIRST_X_ASSUM (SUBST1_TAC o SYM));
TYPIFY `!(u:real^3) v. (dist(u,s) = sqrt(&2) /\ dist(v,s) = sqrt(&2)) ==> (dist(u,v) <= &2 * sqrt(&2))` (C SUBGOAL_THEN ASSUME_TAC);
REPEAT WEAK_STRIP_TAC;
FIRST_X_ASSUM (ASSUME_TAC o (ONCE_REWRITE_RULE[DIST_SYM]));
INTRO_TAC DIST_TRIANGLE [`u`;`s`;`v`];
BY(REPLICATE_TAC 2 (FIRST_X_ASSUM MP_TAC) THEN REAL_ARITH_TAC);
REPEAT (FIRST_X_ASSUM_ST `x = sqrt(&2)` MP_TAC);
TYPIFY `!u. dist (s,u) = dist(u,s)` (C SUBGOAL_THEN (unlist REWRITE_TAC));
BY(MESON_TAC[DIST_SYM]);
BY(MESON_TAC[]);
INTRO_TAC Collect_geom.RADV_FORMULAR [`u0`;`u1`;`u2`];
REWRITE_TAC[Collect_geom.dist3];
ANTS_TAC;
BY(ASM_MESON_TAC[NOT_COPLANAR_NOT_COLLINEAR]);
ASM_REWRITE_TAC[];
FIRST_X_ASSUM_ST `hl vl` MP_TAC;
EXPAND_TAC "vl";
TYPIFY `hl (truncate_simplex 2 ul) = radV {u0,u1,u2}` ENOUGH_TO_SHOW_TAC;
BY(REAL_ARITH_TAC);
REWRITE_TAC[Pack_defs.HL];
AP_TERM_TAC;
GMATCH_SIMP_TAC Bump.SET_OF_LIST_TRUNCATE_2;
ASM_REWRITE_TAC[Bump.EL_EXPLICIT];
REWRITE_TAC[LENGTH];
BY(ARITH_TAC);
BY(ASM_MESON_TAC[NEGLIGIBLE_EMPTY])
]);;
(* }}} *)
(* ======================================================================== *)
(* OLD SCRIPT FOLLOWS *)
end;;